--- a/src/HOL/Finite_Set.thy Wed Feb 02 15:43:04 2005 +0100
+++ b/src/HOL/Finite_Set.thy Wed Feb 02 18:06:00 2005 +0100
@@ -571,7 +571,8 @@
and Afoldx: "(A, x) \<in> foldSet f g z" and Afoldy: "(A,x') \<in> foldSet f g z" .
show ?case
proof cases
- assume "EX k<n. h n = h k"
+ assume "EX k<n. h n = h k"
+ --{*@{term h} is not injective, so the cardinality has not increased*}
hence card': "A = h ` {i. i < n}"
using card by (auto simp:image_def less_Suc_eq)
show ?thesis by(rule IH[OF card' Afoldx Afoldy])
@@ -579,7 +580,7 @@
assume new: "\<not>(EX k<n. h n = h k)"
show ?thesis
proof (rule foldSet.cases[OF Afoldx])
- assume "(A, x) = ({}, z)"
+ assume "(A, x) = ({}, z)" --{*fold of a singleton set*}
thus "x' = x" using Afoldy by (auto)
next
fix B b y
@@ -770,9 +771,9 @@
subsubsection{*Lemmas about @{text fold}*}
lemma (in ACf) fold_commute:
- "finite A ==> (!!z. f (g x) (fold f g z A) = fold f g (f (g x) z) A)"
+ "finite A ==> (!!z. f x (fold f g z A) = fold f g (f x z) A)"
apply (induct set: Finites, simp)
- apply (simp add: left_commute)
+ apply (simp add: left_commute [of x])
done
lemma (in ACf) fold_nest_Un_Int:
@@ -788,8 +789,8 @@
by (simp add: fold_nest_Un_Int)
lemma (in ACf) fold_reindex:
-assumes fin: "finite B"
-shows "inj_on h B \<Longrightarrow> fold f g z (h ` B) = fold f (g \<circ> h) z B"
+assumes fin: "finite A"
+shows "inj_on h A \<Longrightarrow> fold f g z (h ` A) = fold f (g \<circ> h) z A"
using fin apply (induct)
apply simp
apply simp