
diff -r ffca58ce9fbc -r 3641d055b260 Nominal/FSet.thy
--- a/Nominal/FSet.thy	Thu Apr 22 17:27:24 2010 +0200
+++ b/Nominal/FSet.thy	Fri Apr 23 09:54:42 2010 +0200
@@ -73,18 +73,18 @@
 
 text {* Composition Quotient *}
 
+lemma list_rel_refl:
+  shows "(list_rel op \<approx>) r r"
+  by (rule list_rel_refl) (metis equivp_def fset_equivp)
+
 lemma compose_list_refl:
   shows "(list_rel op \<approx> OOO op \<approx>) r r"
 proof
-  show c: "list_rel op \<approx> r r" by (rule list_rel_refl) (metis equivp_def fset_equivp)
+  show c: "list_rel op \<approx> r r" by (rule list_rel_refl)
   have d: "r \<approx> r" by (rule equivp_reflp[OF fset_equivp])
   show b: "(op \<approx> OO list_rel op \<approx>) r r" by (rule pred_compI) (rule d, rule c)
 qed
 
-lemma list_rel_refl:
-  shows "(list_rel op \<approx>) r r"
-  by (rule list_rel_refl)(metis equivp_def fset_equivp)
-
 lemma Quotient_fset_list:
   shows "Quotient (list_rel op \<approx>) (map abs_fset) (map rep_fset)"
   by (fact list_quotient[OF Quotient_fset])
@@ -123,13 +123,14 @@
       assume d: "b \<approx> ba"
       assume e: "list_rel op \<approx> ba s"
       have f: "map abs_fset r = map abs_fset b"
-        by (metis Quotient_rel[OF Quotient_fset_list] c)
-      have g: "map abs_fset s = map abs_fset ba"
-        by (metis Quotient_rel[OF Quotient_fset_list] e)
-      show "map abs_fset r \<approx> map abs_fset s" using d f g map_rel_cong by simp
+        using Quotient_rel[OF Quotient_fset_list] c by blast
+      have "map abs_fset ba = map abs_fset s"
+        using Quotient_rel[OF Quotient_fset_list] e by blast
+      then have g: "map abs_fset s = map abs_fset ba" by simp
+      then show "map abs_fset r \<approx> map abs_fset s" using d f map_rel_cong by simp
     qed
     then show "abs_fset (map abs_fset r) = abs_fset (map abs_fset s)"
-      by (metis Quotient_rel[OF Quotient_fset])
+      using Quotient_rel[OF Quotient_fset] by blast
   next
     assume a: "(list_rel op \<approx> OOO op \<approx>) r r \<and> (list_rel op \<approx> OOO op \<approx>) s s
       \<and> abs_fset (map abs_fset r) = abs_fset (map abs_fset s)"
@@ -256,7 +257,7 @@
   apply (induct b)
   apply (simp_all add: not_memb_nil)
   apply (auto)
-  apply (simp_all add: memb_delete_raw not_memb_delete_raw_ident  rsp_fold_def  memb_cons_iff)
+  apply (simp_all add: memb_delete_raw not_memb_delete_raw_ident rsp_fold_def  memb_cons_iff)
   done
 
 lemma ffold_raw_rsp_pre:
@@ -486,12 +487,12 @@
   "{|x|}"     == "CONST finsert x {||}"
 
 quotient_definition
-  fin ("_ |\<in>| _" [50, 51] 50)
+  fin (infix "|\<in>|" 50)
 where
   "fin :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" is "memb"
 
 abbreviation
-  fnotin :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ |\<notin>| _" [50, 51] 50)
+  fnotin :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<notin>|" 50)
 where
   "x |\<notin>| S \<equiv> \<not> (x |\<in>| S)"
 
@@ -527,7 +528,7 @@
 text {* Compositional Respectfullness and Preservation *}
 
 lemma [quot_respect]: "(list_rel op \<approx> OOO op \<approx>) [] []"
-  by (metis nil_rsp list_rel.simps(1) pred_compI)
+  by (fact compose_list_refl)
 
 lemma [quot_preserve]: "(abs_fset \<circ> map f) [] = abs_fset []"
   by simp
@@ -548,7 +549,7 @@
       abs_o_rep[OF Quotient_fset] map_id finsert_def)
 
 lemma [quot_preserve]:
-  "((map rep_fset \<circ> rep_fset) ---> (map rep_fset \<circ> rep_fset) ---> abs_fset \<circ> map abs_fset) op @ = funion"
+  "((map rep_fset \<circ> rep_fset) ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) op @ = funion"
   by (simp add: expand_fun_eq Quotient_abs_rep[OF Quotient_fset]
       abs_o_rep[OF Quotient_fset] map_id sup_fset_def)
 
@@ -556,15 +557,13 @@
   assumes a: "reflp R"
   and b: "list_rel R l r"
   shows "list_rel R (z @ l) (z @ r)"
-  by (induct z) (simp_all add: b, metis a reflp_def)
+  by (induct z) (simp_all add: b rev_iffD1[OF a meta_eq_to_obj_eq[OF reflp_def]])
 
 lemma append_rsp2_pre0:
   assumes a:"list_rel op \<approx> x x'"
   shows "list_rel op \<approx> (x @ z) (x' @ z)"
   using a apply (induct x x' rule: list_induct2')
-  apply simp_all
-  apply (rule list_rel_refl)
-  done
+  by simp_all (rule list_rel_refl)
 
 lemma append_rsp2_pre1:
   assumes a:"list_rel op \<approx> x x'"
@@ -672,11 +671,7 @@
   assumes a: "fcard_raw A = Suc n"
   shows "\<exists>a. memb a A"
   using a
-  apply (induct A)
-  apply simp
-  apply (rule_tac x="a" in exI)
-  apply (simp add: memb_def)
-  done
+  by (induct A) (auto simp add: memb_def)
 
 lemma memb_card_not_0:
   assumes a: "memb a A"
@@ -781,8 +776,6 @@
   apply (simp_all)
   apply (case_tac "memb a A")
   apply (auto simp add: memb_def)[2]
-  apply (case_tac "list_eq2 (a # A) A")
-  apply (metis list_eq2.intros(3) list_eq2.intros(6))
   apply (metis list_eq2.intros(3) list_eq2.intros(4) list_eq2.intros(5) list_eq2.intros(6))
   apply (metis list_eq2.intros(1) list_eq2.intros(5) list_eq2.intros(6))
   apply (auto simp add: list_eq2_refl not_memb_delete_raw_ident)
@@ -798,39 +791,41 @@
   "xs \<approx> ys \<Longrightarrow> delete_raw xs x \<approx> delete_raw ys x"
   by (simp add: memb_def[symmetric] memb_delete_raw)
 
-lemma list_eq2_equiv_aux:
-  assumes a: "fcard_raw l = n"
-  and b: "l \<approx> r"
-  shows "list_eq2 l r"
-using a b
-proof (induct n arbitrary: l r)
-  case 0
-  have "fcard_raw l = 0" by fact
-  then have "\<forall>x. \<not> memb x l" using memb_card_not_0[of _ l] by auto
-  then have z: "l = []" using no_memb_nil by auto
-  then have "r = []" using `l \<approx> r` by simp
-  then show ?case using z list_eq2_refl by simp
-next
-  case (Suc m)
-  have b: "l \<approx> r" by fact
-  have d: "fcard_raw l = Suc m" by fact
-  have "\<exists>a. memb a l" by (rule fcard_raw_suc_memb[OF d])
-  then obtain a where e: "memb a l" by auto
-  then have e': "memb a r" using list_eq.simps[simplified memb_def[symmetric], of l r] b by auto
-  have f: "fcard_raw (delete_raw l a) = m" using fcard_raw_delete[of l a] e d by simp
-  have g: "delete_raw l a \<approx> delete_raw r a" using delete_raw_rsp[OF b] by simp
-  have g': "list_eq2 (delete_raw l a) (delete_raw r a)" by (rule Suc.hyps[OF f g])
-  have h: "list_eq2 (a # delete_raw l a) (a # delete_raw r a)" by (rule list_eq2.intros(5)[OF g'])
-  have i: "list_eq2 l (a # delete_raw l a)" by (rule list_eq2.intros(3)[OF memb_delete_list_eq2[OF e]])
-  have "list_eq2 l (a # delete_raw r a)" by (rule list_eq2.intros(6)[OF i h])
-  then show ?case using list_eq2.intros(6)[OF _ memb_delete_list_eq2[OF e']] by simp
-qed
-
 lemma list_eq2_equiv:
   "(l \<approx> r) \<longleftrightarrow> (list_eq2 l r)"
 proof
   show "list_eq2 l r \<Longrightarrow> l \<approx> r" by (induct rule: list_eq2.induct) auto
-  show "l \<approx> r \<Longrightarrow> list_eq2 l r" using list_eq2_equiv_aux by blast
+next
+  {
+    fix n
+    assume a: "fcard_raw l = n" and b: "l \<approx> r"
+    have "list_eq2 l r"
+      using a b
+    proof (induct n arbitrary: l r)
+      case 0
+      have "fcard_raw l = 0" by fact
+      then have "\<forall>x. \<not> memb x l" using memb_card_not_0[of _ l] by auto
+      then have z: "l = []" using no_memb_nil by auto
+      then have "r = []" using `l \<approx> r` by simp
+      then show ?case using z list_eq2_refl by simp
+    next
+      case (Suc m)
+      have b: "l \<approx> r" by fact
+      have d: "fcard_raw l = Suc m" by fact
+      have "\<exists>a. memb a l" by (rule fcard_raw_suc_memb[OF d])
+      then obtain a where e: "memb a l" by auto
+      then have e': "memb a r" using list_eq.simps[simplified memb_def[symmetric], of l r] b by auto
+      have f: "fcard_raw (delete_raw l a) = m" using fcard_raw_delete[of l a] e d by simp
+      have g: "delete_raw l a \<approx> delete_raw r a" using delete_raw_rsp[OF b] by simp
+      have g': "list_eq2 (delete_raw l a) (delete_raw r a)" by (rule Suc.hyps[OF f g])
+      have h: "list_eq2 (a # delete_raw l a) (a # delete_raw r a)" by (rule list_eq2.intros(5)[OF g'])
+      have i: "list_eq2 l (a # delete_raw l a)"
+        by (rule list_eq2.intros(3)[OF memb_delete_list_eq2[OF e]])
+      have "list_eq2 l (a # delete_raw r a)" by (rule list_eq2.intros(6)[OF i h])
+      then show ?case using list_eq2.intros(6)[OF _ memb_delete_list_eq2[OF e']] by simp
+    qed
+    }
+  then show "l \<approx> r \<Longrightarrow> list_eq2 l r" by blast
 qed
 
 text {* Lifted theorems *}
@@ -936,10 +931,6 @@
   shows "S |\<union>| {||} = S"
   by (lifting append_Nil2)
 
-thm sup.commute[where 'a="'a fset"]
-
-thm sup.assoc[where 'a="'a fset"]
-
 lemma singleton_union_left:
   "{|a|} |\<union>| S = finsert a S"
   by simp
@@ -973,15 +964,7 @@
   case (finsert x S)
   have asm: "P S" by fact
   show "P (finsert x S)"
-  proof(cases "x |\<in>| S")
-    case True
-    have "x |\<in>| S" by fact
-    then show "P (finsert x S)" using asm by simp
-  next
-    case False
-    have "x |\<notin>| S" by fact
-    then show "P (finsert x S)" using prem2 asm by simp
-  qed
+    by (cases "x |\<in>| S") (simp_all add: asm prem2)
 qed
 
 lemma fset_induct2:




