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.23  subsubsection{*Lemmas about @{text fold}*}
    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 @@
    1.35    by (simp add: fold_nest_Un_Int)
    1.36  
    1.37  lemma (in ACf) fold_reindex:
    1.38 -assumes fin: "finite B"
    1.39 -shows "inj_on h B \<Longrightarrow> fold f g z (h ` B) = fold f (g \<circ> h) z B"
    1.40 +assumes fin: "finite A"
    1.41 +shows "inj_on h A \<Longrightarrow> fold f g z (h ` A) = fold f (g \<circ> h) z A"
    1.42  using fin apply (induct)
    1.43   apply simp
    1.44  apply simp