author paulson Wed, 09 Feb 2005 10:17:09 +0100 changeset 15508 c09defa4c956 parent 15507 2f3186b3e455 child 15509 c54970704285
revised fold1 proofs
 src/HOL/Finite_Set.thy file | annotate | diff | comparison | revisions
```--- 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 (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
+
+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 (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 (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: 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"
+
+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)"
+
+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)"
+
+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 (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 (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: 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"
-
-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)"
-
-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)"
-
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)"