# HG changeset patch
# User paulson
# Date 1107363960 -3600
# Node ID 55497029b25517964bd1e7a1b10c7cd2f4cd1b33
# Parent  06a32fe35ec34af77de422626146fd87402d8d46
generalization and tidying

diff -r 06a32fe35ec3 -r 55497029b255 src/HOL/Finite_Set.thy
--- 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