# HG changeset patch # User paulson # Date 1107940629 -3600 # Node ID c09defa4c956615de07492c1f53cd253c84c0f85 # Parent 2f3186b3e4557ad8c17c9c82ece107539689a8a0 revised fold1 proofs diff -r 2f3186b3e455 -r c09defa4c956 src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Tue Feb 08 18:32:34 2005 +0100 +++ b/src/HOL/Finite_Set.thy Wed Feb 09 10:17:09 2005 +0100 @@ -758,7 +758,7 @@ lemma (in ACIf) fold_insert2: assumes finA: "finite A" -shows "fold (op \) g z (insert a A) = g a \ fold f g z A" +shows "fold f g z (insert a A) = g a \ fold f g z A" proof cases assume "a \ A" then obtain B where A: "A = insert a B" and disj: "a \ B" @@ -1742,8 +1742,6 @@ text{* Does not require start value. *} -(*FIXME: many of the proofs below are too messy!*) - consts fold1Set :: "('a => 'a => 'a) => ('a set \ 'a) set" @@ -1769,38 +1767,110 @@ lemma fold1Set_sing [iff]: "(({a},b) : fold1Set f) = (a = b)" by (blast intro: foldSet.intros elim: foldSet.cases) +lemma fold1_singleton[simp]: "fold1 f {a} = a" + by (unfold fold1_def) blast -subsubsection{* Determinacy for @{term fold1Set} *} +lemma finite_nonempty_imp_fold1Set: + "\ finite A; A \ {} \ \ EX x. (A, x) : fold1Set f" +apply (induct A rule: finite_induct) +apply (auto dest: finite_imp_foldSet [of _ f id]) +done text{*First, some lemmas about @{term foldSet}.*} -lemma (in ACf) foldSet_insert_swap [rule_format]: - "(A,y) \ foldSet f id b ==> ALL z. z \ A --> b \ A --> z \ b --> - (insert b A, z \ y) \ foldSet f id z" -apply (erule foldSet.induct) -apply (simp add: fold_insert_aux) -apply (force simp add: commute, auto) -apply (drule_tac x=z in spec, simp) -apply (subgoal_tac "(insert x (insert b A), x \ (z \ y)) \ foldSet f (\u. u) z") -prefer 2; -apply force -apply (simp add: insert_commute AC) + +lemma (in ACf) foldSet_insert_swap: +assumes fold: "(A,y) \ foldSet f id b" +shows "\ z \ A; b \ A; z \ b \ \ (insert b A, z \ y) \ foldSet f id z" +using fold +proof (induct rule: foldSet.induct) + case emptyI thus ?case by (force simp add: fold_insert_aux commute) +next + case (insertI A x y) + have "(insert x (insert b A), x \ (z \ y)) \ foldSet f (\u. u) z" + using insertI by force + thus ?case by (simp add: insert_commute AC) +qed + +lemma (in ACf) foldSet_permute_diff: +assumes fold: "(A,x) \ foldSet f id b" +shows "!!a. \a \ A; b \ A\ \ (insert b (A-{a}), x) \ foldSet f id a" +using fold +proof (induct rule: foldSet.induct) + case emptyI thus ?case by simp +next + case (insertI A x y) + show ?case + proof - + have a: "a \ insert x A" and b: "b \ insert x A" . + from a have "a = x \ a \ A" by simp + thus "(insert b (insert x A - {a}), id x \ y) \ foldSet f id a" + proof + assume "a = x" + with insertI b show ?thesis by simp (blast intro: foldSet_insert_swap) + next + assume ainA: "a \ A" + hence "(insert x (insert b (A - {a})), x \ y) \ foldSet f id a" + using insertI b by (force simp:id_def) + moreover + have "insert x (insert b (A - {a})) = insert b (insert x A - {a})" + using ainA insertI by blast + ultimately show ?thesis by simp + qed + qed +qed + +lemma (in ACf) fold1_eq_fold: + "[|finite A; a \ A|] ==> fold1 f (insert a A) = fold f id a A" +apply (simp add: fold1_def fold_def) +apply (rule the_equality) +apply (best intro: foldSet_determ theI dest: finite_imp_foldSet [of _ f id]) +apply (rule sym, clarify) +apply (case_tac "Aa=A") + apply (best intro: the_equality foldSet_determ) +apply (subgoal_tac "(A,x) \ foldSet f id a") + apply (best intro: the_equality foldSet_determ) +apply (subgoal_tac "insert aa (Aa - {a}) = A") + prefer 2 apply (blast elim: equalityE) +apply (auto dest: foldSet_permute_diff [where a=a]) +done + +lemma (in ACf) fold1_insert: + "finite A ==> x \ A ==> A \ {} \ fold1 f (insert x A) = f x (fold1 f A)" +apply (induct A rule: finite_induct, force) +apply (simp only: insert_commute, simp) +apply (erule conjE) +apply (simp add: fold1_eq_fold) +apply (subst fold1_eq_fold, auto) +done + +lemma (in ACIf) fold1_insert2 [simp]: + "finite A ==> A \ {} \ fold1 f (insert x A) = f x (fold1 f A)" +apply (induct A rule: finite_induct, force) +apply (case_tac "xa=x") + prefer 2 apply (simp add: insert_commute fold1_eq_fold fold_insert2) +apply (case_tac "F={}") +apply (simp add: idem) +apply (simp add: fold1_insert assoc [symmetric] idem) done -lemma (in ACf) foldSet_permute_diff [rule_format]: - "[|(A,x) \ foldSet f id b |] - ==> ALL a. a \ A --> b \ A --> a \ b --> (insert b (A-{a}), x) \ foldSet f id a" -apply (erule foldSet.induct, simp, clarify, auto) --{*somehow id gets unfolded??*} -apply (blast intro: foldSet_insert_swap [unfolded id_def]) -apply (drule_tac x=a in spec, simp) -apply (subgoal_tac "(insert x (insert b (A - {a})), x \ y) \ foldSet f (%u. u) a") -prefer 2; -apply force -apply (subgoal_tac "insert x (insert b (A - {a})) =insert b (insert x A - {a})") -apply simp -apply blast -done +text{* Now the recursion rules for definitions: *} + +lemma fold1_singleton_def: "g \ fold1 f \ g {a} = a" +by(simp add:fold1_singleton) + +lemma (in ACf) fold1_insert_def: + "\ g \ fold1 f; finite A; x \ A; A \ {} \ \ g(insert x A) = x \ (g A)" +by(simp add:fold1_insert) + +lemma (in ACIf) fold1_insert2_def: + "\ g \ fold1 f; finite A; A \ {} \ \ g(insert x A) = x \ (g A)" +by(simp add:fold1_insert2) + +subsubsection{* Determinacy for @{term fold1Set} *} + +text{*Not actually used!!*} lemma (in ACf) foldSet_permute: "[|(insert a A, x) \ foldSet f id b; a \ A; b \ A|] @@ -1839,65 +1909,9 @@ qed qed -lemma fold1_singleton[simp]: "fold1 f {a} = a" - by (unfold fold1_def) blast - -lemma finite_nonempty_imp_fold1Set: - "\ finite A; A \ {} \ \ EX x. (A, x) : fold1Set f" -apply (induct A rule: finite_induct) -apply (auto dest: finite_imp_foldSet [of _ f id]) -done - lemma (in ACf) fold1Set_equality: "(A, y) : fold1Set f ==> fold1 f A = y" by (unfold fold1_def) (blast intro: fold1Set_determ) -lemma (in ACf) fold1_eq_fold: - "[|finite A; a \ A|] ==> fold1 f (insert a A) = fold f id a A" -apply (simp add: fold1_def fold_def) -apply (rule the_equality) -apply (best intro: foldSet_determ theI dest: finite_imp_foldSet [of _ f id]) -apply (rule sym, clarify) -apply (case_tac "Aa=A") - apply (best intro: the_equality foldSet_determ) -apply (subgoal_tac "(A,x) \ foldSet f id a") - apply (best intro: the_equality foldSet_determ) -apply (subgoal_tac "insert aa (Aa - {a}) = A") - prefer 2 apply (blast elim: equalityE) -apply (auto dest: foldSet_permute_diff [where a=a]) -done - -lemma (in ACf) fold1_insert: - "finite A ==> x \ A ==> A \ {} \ fold1 f (insert x A) = f x (fold1 f A)" -apply (induct A rule: finite_induct, force) -apply (simp only: insert_commute, simp) -apply (erule conjE) -apply (simp add: fold1_eq_fold) -apply (subst fold1_eq_fold, auto) -done - -lemma (in ACIf) fold1_insert2 [simp]: - "finite A ==> A \ {} \ fold1 f (insert x A) = f x (fold1 f A)" -apply (induct A rule: finite_induct, force) -apply (case_tac "xa=x") - prefer 2 apply (simp add: insert_commute fold1_eq_fold fold_insert2) -apply (case_tac "F={}") -apply (simp add: idem) -apply (simp add: fold1_insert assoc [symmetric] idem) -done - -text{* Now the recursion rules for definitions: *} - -lemma fold1_singleton_def: "g \ fold1 f \ g {a} = a" -by(simp add:fold1_singleton) - -lemma (in ACf) fold1_insert_def: - "\ g \ fold1 f; finite A; x \ A; A \ {} \ \ g(insert x A) = x \ (g A)" -by(simp add:fold1_insert) - -lemma (in ACIf) fold1_insert2_def: - "\ g \ fold1 f; finite A; A \ {} \ \ g(insert x A) = x \ (g A)" -by(simp add:fold1_insert2) - declare empty_foldSetE [rule del] foldSet.intros [rule del] empty_fold1SetE [rule del] insert_fold1SetE [rule del] @@ -2025,12 +2039,12 @@ assume "a = x" thus ?thesis using insert by(simp add:below_def ACI) next assume "a \ F" - hence bel: "fold1 op \ F \ a" by(rule insert) - have "fold1 op \ (insert x F) \ a = x \ (fold1 op \ F \ a)" + hence bel: "fold1 f F \ a" by(rule insert) + have "fold1 f (insert x F) \ a = x \ (fold1 f F \ a)" using insert by(simp add:below_def ACI) - also have "fold1 op \ F \ a = fold1 op \ F" + also have "fold1 f F \ a = fold1 f F" using bel by(simp add:below_def ACI) - also have "x \ \ = fold1 op \ (insert x F)" + also have "x \ \ = fold1 f (insert x F)" using insert by(simp add:below_def ACI) finally show ?thesis by(simp add:below_def) qed