# HG changeset patch
# User paulson
# Date 1108036906 -3600
# Node ID 0ed33cd8f238c87024610573889af7fcea98a37b
# Parent  7751ed89ab502bb29abe77d9ae1db644ebd32b12
simplified a key lemma for foldSet

diff -r 7751ed89ab50 -r 0ed33cd8f238 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Thu Feb 10 12:06:40 2005 +0100
+++ b/src/HOL/Finite_Set.thy	Thu Feb 10 13:01:46 2005 +0100
@@ -550,41 +550,22 @@
   have mlessn: "m<n" by (simp add: nSuc)
   have "a \<in> h ` {i. i < n}" using aA by blast
   then obtain k where hkeq: "h k = a" and klessn: "k<n" by blast
+  let ?hm = "swap k m h"
+  have inj_hm: "inj_on ?hm {i. i < n}" using klessn mlessn 
+    by (simp add: inj_on_swap_iff inj_on)
   show ?thesis
-  proof cases
-    assume eq: "k=m"
-    show ?thesis
-    proof (intro exI conjI)
-      show "inj_on h {i::nat. i<m}" using inj_on
-	by (simp add: nSuc inj_on_def) 
-      show "m<n" by (rule mlessn)
-      show "A = h ` {i. i < m}" using aA anot nSuc hkeq eq inj_on
-	by (rules intro: insert_image_inj_on_eq) 
-    qed
-  next
-    assume diff: "k~=m"
-    hence klessm: "k<m" using nSuc klessn by arith
-    have hdiff: "h k ~= h m" using diff inj_on klessn mlessn
-	by (auto simp add: inj_on_def) 
-    let ?hm = "swap k m h"
-    have inj_onhm_n: "inj_on ?hm {i. i < n}" using klessn mlessn 
-      by (simp add: inj_on_swap_iff inj_on)
-    hence inj_onhm_m: "inj_on ?hm {i. i < m}"
+  proof (intro exI conjI)
+    show "inj_on ?hm {i. i < m}" using inj_hm
       by (auto simp add: nSuc less_Suc_eq intro: subset_inj_on)
-    show ?thesis
-    proof (intro exI conjI)
-      show "inj_on ?hm {i. i < m}" by (rule inj_onhm_m)
-      show "m<n" by (simp add: nSuc)
-      show "A = ?hm ` {i. i < m}" 
-      proof (rule insert_image_inj_on_eq)
-	show "inj_on (swap k m h) {i. i < Suc m}" using inj_onhm_n
-	  by (simp add: nSuc)
-        show "?hm m \<notin> A" by (simp add: swap_def hkeq anot) 
-        show "insert (?hm m) A = ?hm ` {i. i < Suc m}"
-          using aA hkeq diff hdiff nSuc
-	  by (auto simp add: swap_def image_less_Suc fun_upd_image klessm 
-                             inj_on_image_set_diff [OF inj_on])
-      qed
+    show "m<n" by (rule mlessn)
+    show "A = ?hm ` {i. i < m}" 
+    proof (rule insert_image_inj_on_eq)
+      show "inj_on (swap k m h) {i. i < Suc m}" using inj_hm nSuc by simp
+      show "?hm m \<notin> A" by (simp add: swap_def hkeq anot) 
+      show "insert (?hm m) A = ?hm ` {i. i < Suc m}"
+	using aA hkeq nSuc klessn
+	by (auto simp add: swap_def image_less_Suc fun_upd_image 
+			   less_Suc_eq inj_on_image_set_diff [OF inj_on])
     qed
   qed
 qed