# HG changeset patch
# User nipkow
# Date 1106923443 -3600
# Node ID fbc473ea9d3ca11077a75b97580cbb976210e163
# Parent  045647dfca9c95b428bfa10ec250820d8078f69c
proof simpification

diff -r 045647dfca9c -r fbc473ea9d3c src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Fri Jan 28 04:35:51 2005 +0100
+++ b/src/HOL/Finite_Set.thy	Fri Jan 28 15:44:03 2005 +0100
@@ -487,6 +487,60 @@
 
 subsubsection{*From @{term foldSet} to @{term fold}*}
 
+(* only used in the next lemma, but in there twice *)
+lemma card_lemma: assumes A1: "A = insert b B" and notinB: "b \<notin> B" and
+  card: "A = h`{i. i<Suc n}" and new: "\<not>(EX k<n. h n = h k)"
+shows "EX h. B = h`{i. i<n}" (is "EX h. ?P h")
+proof
+  let ?h = "%i. if h i = b then h n else h i"
+  show "B = ?h`{i. i<n}" (is "_ = ?r")
+  proof
+    show "B \<subseteq> ?r"
+    proof
+      fix u assume "u \<in> B"
+      hence uinA: "u \<in> A" and unotb: "u \<noteq> b" using A1 notinB by blast+
+      then obtain i\<^isub>u where below: "i\<^isub>u < Suc n" and [simp]: "u = h i\<^isub>u"
+	using card by(auto simp:image_def)
+      show "u \<in> ?r"
+      proof cases
+	assume "i\<^isub>u < n"
+	thus ?thesis using unotb by(fastsimp)
+      next
+	assume "\<not> i\<^isub>u < n"
+	with below have [simp]: "i\<^isub>u = n" by arith
+	obtain i\<^isub>k where i\<^isub>k: "i\<^isub>k < Suc n" and [simp]: "b = h i\<^isub>k"
+	  using A1 card by blast
+	have "i\<^isub>k < n"
+	proof (rule ccontr)
+	  assume "\<not> i\<^isub>k < n"
+	  hence "i\<^isub>k = n" using i\<^isub>k by arith
+	  thus False using unotb by simp
+	qed
+	thus ?thesis by(auto simp add:image_def)
+      qed
+    qed
+  next
+    show "?r \<subseteq> B"
+    proof
+      fix u assume "u \<in> ?r"
+      then obtain i\<^isub>u where below: "i\<^isub>u < n" and
+        or: "b = h i\<^isub>u \<and> u = h n \<or> h i\<^isub>u \<noteq> b \<and> h i\<^isub>u = u"
+	by(auto simp:image_def)
+      from or show "u \<in> B"
+      proof
+	assume [simp]: "b = h i\<^isub>u \<and> u = h n"
+	have "u \<in> A" using card by auto
+        moreover have "u \<noteq> b" using new below by auto
+	ultimately show "u \<in> B" using A1 by blast
+      next
+	assume "h i\<^isub>u \<noteq> b \<and> h i\<^isub>u = u"
+	moreover hence "u \<in> A" using card below by auto
+	ultimately show "u \<in> B" using A1 by blast
+      qed
+    qed
+  qed
+qed
+
 lemma (in ACf) foldSet_determ_aux:
   "!!A x x' h. \<lbrakk> A = h`{i::nat. i<n}; (A,x) : foldSet f g e; (A,x') : foldSet f g e \<rbrakk>
    \<Longrightarrow> x' = x"
@@ -523,58 +577,15 @@
 	assume eq2: "(A,x') = (insert c C, g c \<cdot> z)"
 	  and z: "(C,z) \<in> foldSet f g e" and notinC: "c \<notin> C"
 	hence A2: "A = insert c C" and x': "x' = g c \<cdot> z" by auto
-	let ?h = "%i. if h i = b then h n else h i"
-	have less: "B = ?h`{i. i<n}" (is "_ = ?r")
-	proof
-	  show "B \<subseteq> ?r"
-	  proof
-	    fix u assume "u \<in> B"
-	    hence uinA: "u \<in> A" and unotb: "u \<noteq> b" using A1 notinB by blast+
-	    then obtain i\<^isub>u where below: "i\<^isub>u < Suc n" and [simp]: "u = h i\<^isub>u"
-	      using card by(auto simp:image_def)
-	    show "u \<in> ?r"
-	    proof cases
-	      assume "i\<^isub>u < n"
-	      thus ?thesis using unotb by(fastsimp)
-	    next
-	      assume "\<not> i\<^isub>u < n"
-	      with below have [simp]: "i\<^isub>u = n" by arith
-	      obtain i\<^isub>k where i\<^isub>k: "i\<^isub>k < Suc n" and [simp]: "b = h i\<^isub>k"
-		using A1 card by blast
-	      have "i\<^isub>k < n"
-	      proof (rule ccontr)
-		assume "\<not> i\<^isub>k < n"
-		hence "i\<^isub>k = n" using i\<^isub>k by arith
-		thus False using unotb by simp
-	      qed
-	      thus ?thesis by(auto simp add:image_def)
-	    qed
-	  qed
-	next
-	  show "?r \<subseteq> B"
-	  proof
-	    fix u assume "u \<in> ?r"
-	    then obtain i\<^isub>u where below: "i\<^isub>u < n" and
-              or: "b = h i\<^isub>u \<and> u = h n \<or> h i\<^isub>u \<noteq> b \<and> h i\<^isub>u = u"
-	      by(auto simp:image_def)
-	    from or show "u \<in> B"
-	    proof
-	      assume [simp]: "b = h i\<^isub>u \<and> u = h n"
-	      have "u \<in> A" using card by auto
-              moreover have "u \<noteq> b" using new below by auto
-	      ultimately show "u \<in> B" using A1 by blast
-	    next
-	      assume "h i\<^isub>u \<noteq> b \<and> h i\<^isub>u = u"
-	      moreover hence "u \<in> A" using card below by auto
-	      ultimately show "u \<in> B" using A1 by blast
-	    qed
-	  qed
-	qed
+	obtain hB where lessB: "B = hB ` {i. i<n}"
+	  using card_lemma[OF A1 notinB card new] by auto
+	obtain hC where lessC: "C = hC ` {i. i<n}"
+	  using card_lemma[OF A2 notinC card new] by auto
 	show ?thesis
 	proof cases
 	  assume "b = c"
 	  then moreover have "B = C" using A1 A2 notinB notinC by auto
-	  ultimately show ?thesis using IH[OF less] y z x x' by auto
+	  ultimately show ?thesis using IH[OF lessB] y z x x' by auto
 	next
 	  assume diff: "b \<noteq> c"
 	  let ?D = "B - {c}"
@@ -587,58 +598,9 @@
 	  moreover have cinB: "c \<in> B" using B by(auto)
 	  ultimately have "(B,g c \<cdot> d) \<in> foldSet f g e"
 	    by(rule Diff1_foldSet)
-	  hence "g c \<cdot> d = y" by(rule IH[OF less y])
+	  hence "g c \<cdot> d = y" by(rule IH[OF lessB y])
           moreover have "g b \<cdot> d = z"
-	  proof (rule IH[OF _ z])
-	    let ?h = "%i. if h i = c then h n else h i"
-	    show "C = ?h`{i. i<n}" (is "_ = ?r")
-	    proof
-	      show "C \<subseteq> ?r"
-	      proof
-		fix u assume "u \<in> C"
-		hence uinA: "u \<in> A" and unotc: "u \<noteq> c"
-		  using A2 notinC by blast+
-		then obtain i\<^isub>u where below: "i\<^isub>u < Suc n" and [simp]: "u = h i\<^isub>u"
-		  using card by(auto simp:image_def)
-		show "u \<in> ?r"
-		proof cases
-		  assume "i\<^isub>u < n"
-		  thus ?thesis using unotc by(fastsimp)
-		next
-		  assume "\<not> i\<^isub>u < n"
-		  with below have [simp]: "i\<^isub>u = n" by arith
-		  obtain i\<^isub>k where i\<^isub>k: "i\<^isub>k < Suc n" and [simp]: "c = h i\<^isub>k"
-		    using A2 card by blast
-		  have "i\<^isub>k < n"
-		  proof (rule ccontr)
-		    assume "\<not> i\<^isub>k < n"
-		    hence "i\<^isub>k = n" using i\<^isub>k by arith
-		    thus False using unotc by simp
-		  qed
-		  thus ?thesis by(auto simp add:image_def)
-		qed
-	      qed
-	    next
-	      show "?r \<subseteq> C"
-	      proof
-		fix u assume "u \<in> ?r"
-		then obtain i\<^isub>u where below: "i\<^isub>u < n" and
-		  or: "c = h i\<^isub>u \<and> u = h n \<or> h i\<^isub>u \<noteq> c \<and> h i\<^isub>u = u"
-		  by(auto simp:image_def)
-		from or show "u \<in> C"
-		proof
-		  assume [simp]: "c = h i\<^isub>u \<and> u = h n"
-		  have "u \<in> A" using card by auto
-		  moreover have "u \<noteq> c" using new below by auto
-		  ultimately show "u \<in> C" using A2 by blast
-		next
-		  assume "h i\<^isub>u \<noteq> c \<and> h i\<^isub>u = u"
-		  moreover hence "u \<in> A" using card below by auto
-		  ultimately show "u \<in> C" using A2 by blast
-		qed
-	      qed
-	    qed
-	  next
+	  proof (rule IH[OF lessC z])
 	    show "(C,g b \<cdot> d) \<in> foldSet f g e" using C notinB Dfoldd
 	      by fastsimp
 	  qed