# 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 \<cdot>) g z (insert a A) = g a \<cdot> fold f g z A"
+shows "fold f g z (insert a A) = g a \<cdot> fold f g z A"
 proof cases
   assume "a \<in> A"
   then obtain B where A: "A = insert a B" and disj: "a \<notin> 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 \<times> '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:
+  "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> 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) \<in> foldSet f id b ==> ALL z. z \<notin> A --> b \<notin> A --> z \<noteq> b -->
-       (insert b A, z \<cdot> y) \<in> 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 \<cdot> (z \<cdot> y)) \<in> foldSet f (\<lambda>u. u) z")
-prefer 2;
-apply force 
-apply (simp add: insert_commute AC) 
+
+lemma (in ACf) foldSet_insert_swap:
+assumes fold: "(A,y) \<in> foldSet f id b"
+shows "\<lbrakk> z \<notin> A; b \<notin> A; z \<noteq> b \<rbrakk> \<Longrightarrow> (insert b A, z \<cdot> y) \<in> 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 \<cdot> (z \<cdot> y)) \<in> foldSet f (\<lambda>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) \<in> foldSet f id b"
+shows "!!a. \<lbrakk>a \<in> A; b \<notin> A\<rbrakk> \<Longrightarrow> (insert b (A-{a}), x) \<in> 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 \<in> insert x A" and b: "b \<notin> insert x A" .
+    from a have "a = x \<or> a \<in> A" by simp
+    thus "(insert b (insert x A - {a}), id x \<cdot> y) \<in> foldSet f id a"
+    proof
+      assume "a = x"
+      with insertI b show ?thesis by simp (blast intro: foldSet_insert_swap)
+    next
+      assume ainA: "a \<in> A"
+      hence "(insert x (insert b (A - {a})), x \<cdot> y) \<in> 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 \<notin> 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) \<in> 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 \<notin> A ==> A \<noteq> {} \<Longrightarrow> 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 \<noteq> {} \<Longrightarrow> 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) \<in> foldSet f id b |]
-   ==> ALL a. a \<in> A --> b \<notin> A --> a \<noteq> b --> (insert b (A-{a}), x) \<in> 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 \<cdot> y) \<in> 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 \<equiv> fold1 f \<Longrightarrow> g {a} = a"
+by(simp add:fold1_singleton)
+
+lemma (in ACf) fold1_insert_def:
+  "\<lbrakk> g \<equiv> fold1 f; finite A; x \<notin> A; A \<noteq> {} \<rbrakk> \<Longrightarrow> g(insert x A) = x \<cdot> (g A)"
+by(simp add:fold1_insert)
+
+lemma (in ACIf) fold1_insert2_def:
+  "\<lbrakk> g \<equiv> fold1 f; finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> g(insert x A) = x \<cdot> (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) \<in> foldSet f id b; a \<notin> A; b \<notin> 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:
-  "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> 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 \<notin> 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) \<in> 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 \<notin> A ==> A \<noteq> {} \<Longrightarrow> 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 \<noteq> {} \<Longrightarrow> 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 \<equiv> fold1 f \<Longrightarrow> g {a} = a"
-by(simp add:fold1_singleton)
-
-lemma (in ACf) fold1_insert_def:
-  "\<lbrakk> g \<equiv> fold1 f; finite A; x \<notin> A; A \<noteq> {} \<rbrakk> \<Longrightarrow> g(insert x A) = x \<cdot> (g A)"
-by(simp add:fold1_insert)
-
-lemma (in ACIf) fold1_insert2_def:
-  "\<lbrakk> g \<equiv> fold1 f; finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> g(insert x A) = x \<cdot> (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 \<in> F"
-    hence bel: "fold1 op \<cdot> F \<sqsubseteq> a" by(rule insert)
-    have "fold1 op \<cdot> (insert x F) \<cdot> a = x \<cdot> (fold1 op \<cdot> F \<cdot> a)"
+    hence bel: "fold1 f F \<sqsubseteq> a" by(rule insert)
+    have "fold1 f (insert x F) \<cdot> a = x \<cdot> (fold1 f F \<cdot> a)"
       using insert by(simp add:below_def ACI)
-    also have "fold1 op \<cdot> F \<cdot> a = fold1 op \<cdot> F"
+    also have "fold1 f F \<cdot> a = fold1 f F"
       using bel  by(simp add:below_def ACI)
-    also have "x \<cdot> \<dots> = fold1 op \<cdot> (insert x F)"
+    also have "x \<cdot> \<dots> = fold1 f (insert x F)"
       using insert by(simp add:below_def ACI)
     finally show ?thesis  by(simp add:below_def)
   qed