--- 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], []);