src/HOL/Finite_Set.thy
 changeset 15487 55497029b255 parent 15484 2636ec211ec8 child 15497 53bca254719a
```     1.1 --- a/src/HOL/Finite_Set.thy	Wed Feb 02 15:43:04 2005 +0100
1.2 +++ b/src/HOL/Finite_Set.thy	Wed Feb 02 18:06:00 2005 +0100
1.3 @@ -571,7 +571,8 @@
1.4    and Afoldx: "(A, x) \<in> foldSet f g z" and Afoldy: "(A,x') \<in> foldSet f g z" .
1.5    show ?case
1.6    proof cases
1.7 -    assume "EX k<n. h n = h k"
1.8 +    assume "EX k<n. h n = h k"
1.9 +      --{*@{term h} is not injective, so the cardinality has not increased*}
1.10      hence card': "A = h ` {i. i < n}"
1.11        using card by (auto simp:image_def less_Suc_eq)
1.12      show ?thesis by(rule IH[OF card' Afoldx Afoldy])
1.13 @@ -579,7 +580,7 @@
1.14      assume new: "\<not>(EX k<n. h n = h k)"
1.15      show ?thesis
1.16      proof (rule foldSet.cases[OF Afoldx])
1.17 -      assume "(A, x) = ({}, z)"
1.18 +      assume "(A, x) = ({}, z)"  --{*fold of a singleton set*}
1.19        thus "x' = x" using Afoldy by (auto)
1.20      next
1.21        fix B b y
1.22 @@ -770,9 +771,9 @@
1.24
1.25  lemma (in ACf) fold_commute:
1.26 -  "finite A ==> (!!z. f (g x) (fold f g z A) = fold f g (f (g x) z) A)"
1.27 +  "finite A ==> (!!z. f x (fold f g z A) = fold f g (f x z) A)"
1.28    apply (induct set: Finites, simp)
1.29 -  apply (simp add: left_commute)
1.30 +  apply (simp add: left_commute [of x])
1.31    done
1.32
1.33  lemma (in ACf) fold_nest_Un_Int:
1.34 @@ -788,8 +789,8 @@