# HG changeset patch
# User paulson
# Date 1108047798 -3600
# Node ID 1ffd04343ac91fce0407f728ba40ad17737ccc0f
# Parent  0ed33cd8f238c87024610573889af7fcea98a37b
non-inductive fold1Set proofs

diff -r 0ed33cd8f238 -r 1ffd04343ac9 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Thu Feb 10 13:01:46 2005 +0100
+++ b/src/HOL/Finite_Set.thy	Thu Feb 10 16:03:18 2005 +0100
@@ -1699,17 +1699,16 @@
 
 text{*First, some lemmas about @{term foldSet}.*}
 
-
 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"
+shows "b \<notin> A \<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
+      using insertI by force  --{*how does @{term id} get unfolded?*}
     thus ?case by (simp add: insert_commute AC)
 qed
 
@@ -1721,23 +1720,20 @@
   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
+  have "a = x \<or> a \<in> A" using insertI by simp
+  thus ?case
+  proof
+    assume "a = x"
+    with insertI show ?thesis
+      by (simp add: id_def [symmetric], 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 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 add: id_def)
   qed
 qed
 
@@ -1756,24 +1752,47 @@
 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) 
+lemma nonempty_iff: "(A \<noteq> {}) = (\<exists>x B. A = insert x B & x \<notin> B)"
+apply safe
+apply simp 
+apply (drule_tac x=x in spec)
+apply (drule_tac x="A-{x}" in spec, auto) 
 done
 
+lemma (in ACf) fold1_insert:
+  assumes nonempty: "A \<noteq> {}" and A: "finite A" "x \<notin> A"
+  shows "fold1 f (insert x A) = f x (fold1 f A)"
+proof -
+  from nonempty obtain a A' where "A = insert a A' & a ~: A'" 
+    by (auto simp add: nonempty_iff)
+  with A show ?thesis
+    by (simp add: insert_commute [of x] fold1_eq_fold eq_commute) 
+qed
+
 lemma (in ACIf) fold1_insert_idem [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_insert_idem) 
-apply (case_tac "F={}") 
-apply (simp add: idem) 
-apply (simp add: fold1_insert assoc [symmetric] idem) 
-done
+  assumes nonempty: "A \<noteq> {}" and A: "finite A" 
+  shows "fold1 f (insert x A) = f x (fold1 f A)"
+proof -
+  from nonempty obtain a A' where A': "A = insert a A' & a ~: A'" 
+    by (auto simp add: nonempty_iff)
+  show ?thesis
+  proof cases
+    assume "a = x"
+    thus ?thesis 
+    proof cases
+      assume "A' = {}"
+      with prems show ?thesis by (simp add: idem) 
+    next
+      assume "A' \<noteq> {}"
+      with prems show ?thesis
+	by (simp add: fold1_insert assoc [symmetric] idem) 
+    qed
+  next
+    assume "a \<noteq> x"
+    with prems show ?thesis
+      by (simp add: insert_commute fold1_eq_fold fold_insert_idem)
+  qed
+qed
 
 
 text{* Now the recursion rules for definitions: *}