
diff -r 8537493c039f -r 3b24b5d2b68c Nominal/FSet.thy
--- a/Nominal/FSet.thy	Sun Oct 17 21:40:23 2010 +0100
+++ b/Nominal/FSet.thy	Mon Oct 18 14:13:28 2010 +0900
@@ -69,80 +69,84 @@
 section {* Quotient composition lemmas *}
 
 lemma list_all2_refl':
-  shows "(list_all2 op \<approx>) r r"
-  by (rule list_all2_refl) (metis equivp_def fset_equivp)
+  assumes q: "equivp R"
+  shows "(list_all2 R) r r"
+  by (rule list_all2_refl) (metis equivp_def q)
 
 lemma compose_list_refl:
-  shows "(list_all2 op \<approx> OOO op \<approx>) r r"
+  assumes q: "equivp R"
+  shows "(list_all2 R OOO op \<approx>) r r"
 proof
   have *: "r \<approx> r" by (rule equivp_reflp[OF fset_equivp])
-  show "list_all2 op \<approx> r r" by (rule list_all2_refl')
-  with * show "(op \<approx> OO list_all2 op \<approx>) r r" ..
+  show "list_all2 R r r" by (rule list_all2_refl'[OF q])
+  with * show "(op \<approx> OO list_all2 R) r r" ..
 qed
 
-lemma Quotient_fset_list:
-  shows "Quotient (list_all2 op \<approx>) (map abs_fset) (map rep_fset)"
-  by (fact list_quotient[OF Quotient_fset])
-
 lemma map_list_eq_cong: "b \<approx> ba \<Longrightarrow> map f b \<approx> map f ba"
   unfolding list_eq.simps
   by (simp only: set_map)
 
-lemma quotient_compose_list[quot_thm]:
-  shows  "Quotient ((list_all2 op \<approx>) OOO (op \<approx>))
-    (abs_fset \<circ> (map abs_fset)) ((map rep_fset) \<circ> rep_fset)"
+lemma quotient_compose_list_g:
+  assumes q: "Quotient R Abs Rep"
+  and     e: "equivp R"
+  shows  "Quotient ((list_all2 R) OOO (op \<approx>))
+    (abs_fset \<circ> (map Abs)) ((map Rep) \<circ> rep_fset)"
   unfolding Quotient_def comp_def
 proof (intro conjI allI)
   fix a r s
-  show "abs_fset (map abs_fset (map rep_fset (rep_fset a))) = a"
-    by (simp add: abs_o_rep[OF Quotient_fset] Quotient_abs_rep[OF Quotient_fset] map_id)
-  have b: "list_all2 op \<approx> (map rep_fset (rep_fset a)) (map rep_fset (rep_fset a))"
-    by (rule list_all2_refl')
-  have c: "(op \<approx> OO list_all2 op \<approx>) (map rep_fset (rep_fset a)) (map rep_fset (rep_fset a))"
+  show "abs_fset (map Abs (map Rep (rep_fset a))) = a"
+    by (simp add: abs_o_rep[OF q] Quotient_abs_rep[OF Quotient_fset] map_id)
+  have b: "list_all2 R (map Rep (rep_fset a)) (map Rep (rep_fset a))"
+    by (rule list_all2_refl'[OF e])
+  have c: "(op \<approx> OO list_all2 R) (map Rep (rep_fset a)) (map Rep (rep_fset a))"
     by (rule, rule equivp_reflp[OF fset_equivp]) (rule b)
-  show "(list_all2 op \<approx> OOO op \<approx>) (map rep_fset (rep_fset a)) (map rep_fset (rep_fset a))"
-    by (rule, rule list_all2_refl') (rule c)
-  show "(list_all2 op \<approx> OOO op \<approx>) r s = ((list_all2 op \<approx> OOO op \<approx>) r r \<and>
-        (list_all2 op \<approx> OOO op \<approx>) s s \<and> abs_fset (map abs_fset r) = abs_fset (map abs_fset s))"
+  show "(list_all2 R OOO op \<approx>) (map Rep (rep_fset a)) (map Rep (rep_fset a))"
+    by (rule, rule list_all2_refl'[OF e]) (rule c)
+  show "(list_all2 R OOO op \<approx>) r s = ((list_all2 R OOO op \<approx>) r r \<and>
+        (list_all2 R OOO op \<approx>) s s \<and> abs_fset (map Abs r) = abs_fset (map Abs s))"
   proof (intro iffI conjI)
-    show "(list_all2 op \<approx> OOO op \<approx>) r r" by (rule compose_list_refl)
-    show "(list_all2 op \<approx> OOO op \<approx>) s s" by (rule compose_list_refl)
+    show "(list_all2 R OOO op \<approx>) r r" by (rule compose_list_refl[OF e])
+    show "(list_all2 R OOO op \<approx>) s s" by (rule compose_list_refl[OF e])
   next
-    assume a: "(list_all2 op \<approx> OOO op \<approx>) r s"
-    then have b: "map abs_fset r \<approx> map abs_fset s"
+    assume a: "(list_all2 R OOO op \<approx>) r s"
+    then have b: "map Abs r \<approx> map Abs s"
     proof (elim pred_compE)
       fix b ba
-      assume c: "list_all2 op \<approx> r b"
+      assume c: "list_all2 R r b"
       assume d: "b \<approx> ba"
-      assume e: "list_all2 op \<approx> ba s"
-      have f: "map abs_fset r = map abs_fset b"
-        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_list_eq_cong by simp
+      assume e: "list_all2 R ba s"
+      have f: "map Abs r = map Abs b"
+        using Quotient_rel[OF list_quotient[OF q]] c by blast
+      have "map Abs ba = map Abs s"
+        using Quotient_rel[OF list_quotient[OF q]] e by blast
+      then have g: "map Abs s = map Abs ba" by simp
+      then show "map Abs r \<approx> map Abs s" using d f map_list_eq_cong by simp
     qed
-    then show "abs_fset (map abs_fset r) = abs_fset (map abs_fset s)"
+    then show "abs_fset (map Abs r) = abs_fset (map Abs s)"
       using Quotient_rel[OF Quotient_fset] by blast
   next
-    assume a: "(list_all2 op \<approx> OOO op \<approx>) r r \<and> (list_all2 op \<approx> OOO op \<approx>) s s
-      \<and> abs_fset (map abs_fset r) = abs_fset (map abs_fset s)"
-    then have s: "(list_all2 op \<approx> OOO op \<approx>) s s" by simp
-    have d: "map abs_fset r \<approx> map abs_fset s"
+    assume a: "(list_all2 R OOO op \<approx>) r r \<and> (list_all2 R OOO op \<approx>) s s
+      \<and> abs_fset (map Abs r) = abs_fset (map Abs s)"
+    then have s: "(list_all2 R OOO op \<approx>) s s" by simp
+    have d: "map Abs r \<approx> map Abs s"
       by (subst Quotient_rel[OF Quotient_fset]) (simp add: a)
-    have b: "map rep_fset (map abs_fset r) \<approx> map rep_fset (map abs_fset s)"
+    have b: "map Rep (map Abs r) \<approx> map Rep (map Abs s)"
       by (rule map_list_eq_cong[OF d])
-    have y: "list_all2 op \<approx> (map rep_fset (map abs_fset s)) s"
-      by (fact rep_abs_rsp_left[OF Quotient_fset_list, OF list_all2_refl'[of s]])
-    have c: "(op \<approx> OO list_all2 op \<approx>) (map rep_fset (map abs_fset r)) s"
+    have y: "list_all2 R (map Rep (map Abs s)) s"
+      by (fact rep_abs_rsp_left[OF list_quotient[OF q], OF list_all2_refl'[OF e, of s]])
+    have c: "(op \<approx> OO list_all2 R) (map Rep (map Abs r)) s"
       by (rule pred_compI) (rule b, rule y)
-    have z: "list_all2 op \<approx> r (map rep_fset (map abs_fset r))"
-      by (fact rep_abs_rsp[OF Quotient_fset_list, OF list_all2_refl'[of r]])
-    then show "(list_all2 op \<approx> OOO op \<approx>) r s"
+    have z: "list_all2 R r (map Rep (map Abs r))"
+      by (fact rep_abs_rsp[OF list_quotient[OF q], OF list_all2_refl'[OF e, of r]])
+    then show "(list_all2 R OOO op \<approx>) r s"
       using a c pred_compI by simp
   qed
 qed
 
+lemma quotient_compose_list[quot_thm]:
+  shows  "Quotient ((list_all2 op \<approx>) OOO (op \<approx>))
+    (abs_fset \<circ> (map abs_fset)) ((map rep_fset) \<circ> rep_fset)"
+  by (rule quotient_compose_list_g, rule Quotient_fset, rule list_eq_equivp)
 
 subsection {* Respectfulness lemmas for list operations *}
 
@@ -434,7 +438,7 @@
 
 lemma Nil_rsp2 [quot_respect]: 
   shows "(list_all2 op \<approx> OOO op \<approx>) Nil Nil"
-  by (fact compose_list_refl)
+  by (rule compose_list_refl, rule list_eq_equivp)
 
 lemma Cons_rsp2 [quot_respect]:
   shows "(op \<approx> ===> list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx>) Cons Cons"
@@ -470,13 +474,13 @@
   assumes a:"list_all2 op \<approx> x x'"
   shows "list_all2 op \<approx> (x @ z) (x' @ z)"
   using a apply (induct x x' rule: list_induct2')
-  by simp_all (rule list_all2_refl')
+  by simp_all (rule list_all2_refl'[OF list_eq_equivp])
 
 lemma append_rsp2_pre1:
   assumes a:"list_all2 op \<approx> x x'"
   shows "list_all2 op \<approx> (z @ x) (z @ x')"
   using a apply (induct x x' arbitrary: z rule: list_induct2')
-  apply (rule list_all2_refl')
+  apply (rule list_all2_refl'[OF list_eq_equivp])
   apply (simp_all del: list_eq.simps)
   apply (rule list_all2_app_l)
   apply (simp_all add: reflp_def)
@@ -491,7 +495,7 @@
   apply (rule a)
   using b apply (induct z z' rule: list_induct2')
   apply (simp_all only: append_Nil2)
-  apply (rule list_all2_refl')
+  apply (rule list_all2_refl'[OF list_eq_equivp])
   apply simp_all
   apply (rule append_rsp2_pre1)
   apply simp
@@ -1140,78 +1144,6 @@
   using assms
   by (lifting list_eq2.induct[simplified list_eq2_equiv[symmetric]])
 
-lemma list_all2_refl'':
-  assumes q: "equivp R"
-  shows "(list_all2 R) r r"
-  by (rule list_all2_refl) (metis equivp_def q)
-
-lemma compose_list_refl2:
-  assumes q: "equivp R"
-  shows "(list_all2 R OOO op \<approx>) r r"
-proof
-  have *: "r \<approx> r" by (rule equivp_reflp[OF fset_equivp])
-  show "list_all2 R r r" by (rule list_all2_refl''[OF q])
-  with * show "(op \<approx> OO list_all2 R) r r" ..
-qed
-
-lemma quotient_compose_list_g:
-  assumes q: "Quotient R Abs Rep"
-  and     e: "equivp R"
-  shows  "Quotient ((list_all2 R) OOO (op \<approx>))
-    (abs_fset \<circ> (map Abs)) ((map Rep) \<circ> rep_fset)"
-  unfolding Quotient_def comp_def
-proof (intro conjI allI)
-  fix a r s
-  show "abs_fset (map Abs (map Rep (rep_fset a))) = a"
-    by (simp add: abs_o_rep[OF q] Quotient_abs_rep[OF Quotient_fset] map_id)
-  have b: "list_all2 R (map Rep (rep_fset a)) (map Rep (rep_fset a))"
-    by (rule list_all2_refl''[OF e])
-  have c: "(op \<approx> OO list_all2 R) (map Rep (rep_fset a)) (map Rep (rep_fset a))"
-    by (rule, rule equivp_reflp[OF fset_equivp]) (rule b)
-  show "(list_all2 R OOO op \<approx>) (map Rep (rep_fset a)) (map Rep (rep_fset a))"
-    by (rule, rule list_all2_refl''[OF e]) (rule c)
-  show "(list_all2 R OOO op \<approx>) r s = ((list_all2 R OOO op \<approx>) r r \<and>
-        (list_all2 R OOO op \<approx>) s s \<and> abs_fset (map Abs r) = abs_fset (map Abs s))"
-  proof (intro iffI conjI)
-    show "(list_all2 R OOO op \<approx>) r r" by (rule compose_list_refl2[OF e])
-    show "(list_all2 R OOO op \<approx>) s s" by (rule compose_list_refl2[OF e])
-  next
-    assume a: "(list_all2 R OOO op \<approx>) r s"
-    then have b: "map Abs r \<approx> map Abs s"
-    proof (elim pred_compE)
-      fix b ba
-      assume c: "list_all2 R r b"
-      assume d: "b \<approx> ba"
-      assume e: "list_all2 R ba s"
-      have f: "map Abs r = map Abs b"
-        using Quotient_rel[OF list_quotient[OF q]] c by blast
-      have "map Abs ba = map Abs s"
-        using Quotient_rel[OF list_quotient[OF q]] e by blast
-      then have g: "map Abs s = map Abs ba" by simp
-      then show "map Abs r \<approx> map Abs s" using d f map_list_eq_cong by simp
-    qed
-    then show "abs_fset (map Abs r) = abs_fset (map Abs s)"
-      using Quotient_rel[OF Quotient_fset] by blast
-  next
-    assume a: "(list_all2 R OOO op \<approx>) r r \<and> (list_all2 R OOO op \<approx>) s s
-      \<and> abs_fset (map Abs r) = abs_fset (map Abs s)"
-    then have s: "(list_all2 R OOO op \<approx>) s s" by simp
-    have d: "map Abs r \<approx> map Abs s"
-      by (subst Quotient_rel[OF Quotient_fset]) (simp add: a)
-    have b: "map Rep (map Abs r) \<approx> map Rep (map Abs s)"
-      by (rule map_list_eq_cong[OF d])
-    have y: "list_all2 R (map Rep (map Abs s)) s"
-      by (fact rep_abs_rsp_left[OF list_quotient[OF q], OF list_all2_refl''[OF e, of s]])
-    have c: "(op \<approx> OO list_all2 R) (map Rep (map Abs r)) s"
-      by (rule pred_compI) (rule b, rule y)
-    have z: "list_all2 R r (map Rep (map Abs r))"
-      by (fact rep_abs_rsp[OF list_quotient[OF q], OF list_all2_refl''[OF e, of r]])
-    then show "(list_all2 R OOO op \<approx>) r s"
-      using a c pred_compI by simp
-  qed
-qed
-
-
 ML {*
 fun dest_fsetT (Type (@{type_name fset}, [T])) = T
   | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []);




