author paulson Wed, 02 Feb 2005 18:06:00 +0100 changeset 15487 55497029b255 parent 15486 06a32fe35ec3 child 15488 7c638a46dcbb
generalization and tidying
 src/HOL/Finite_Set.thy file | annotate | diff | comparison | revisions
```--- 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 @@

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 [of x])
done

lemma (in ACf) fold_nest_Un_Int:
@@ -788,8 +789,8 @@