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 \) 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 \ OOO op \) r r" + assumes q: "equivp R" + shows "(list_all2 R OOO op \) r r" proof have *: "r \ r" by (rule equivp_reflp[OF fset_equivp]) - show "list_all2 op \ r r" by (rule list_all2_refl') - with * show "(op \ OO list_all2 op \) r r" .. + show "list_all2 R r r" by (rule list_all2_refl'[OF q]) + with * show "(op \ OO list_all2 R) r r" .. qed -lemma Quotient_fset_list: - shows "Quotient (list_all2 op \) (map abs_fset) (map rep_fset)" - by (fact list_quotient[OF Quotient_fset]) - lemma map_list_eq_cong: "b \ ba \ map f b \ map f ba" unfolding list_eq.simps by (simp only: set_map) -lemma quotient_compose_list[quot_thm]: - shows "Quotient ((list_all2 op \) OOO (op \)) - (abs_fset \ (map abs_fset)) ((map rep_fset) \ rep_fset)" +lemma quotient_compose_list_g: + assumes q: "Quotient R Abs Rep" + and e: "equivp R" + shows "Quotient ((list_all2 R) OOO (op \)) + (abs_fset \ (map Abs)) ((map Rep) \ 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 \ (map rep_fset (rep_fset a)) (map rep_fset (rep_fset a))" - by (rule list_all2_refl') - have c: "(op \ OO list_all2 op \) (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 \ 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 \ OOO op \) (map rep_fset (rep_fset a)) (map rep_fset (rep_fset a))" - by (rule, rule list_all2_refl') (rule c) - show "(list_all2 op \ OOO op \) r s = ((list_all2 op \ OOO op \) r r \ - (list_all2 op \ OOO op \) s s \ abs_fset (map abs_fset r) = abs_fset (map abs_fset s))" + show "(list_all2 R OOO op \) (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 \) r s = ((list_all2 R OOO op \) r r \ + (list_all2 R OOO op \) s s \ abs_fset (map Abs r) = abs_fset (map Abs s))" proof (intro iffI conjI) - show "(list_all2 op \ OOO op \) r r" by (rule compose_list_refl) - show "(list_all2 op \ OOO op \) s s" by (rule compose_list_refl) + show "(list_all2 R OOO op \) r r" by (rule compose_list_refl[OF e]) + show "(list_all2 R OOO op \) s s" by (rule compose_list_refl[OF e]) next - assume a: "(list_all2 op \ OOO op \) r s" - then have b: "map abs_fset r \ map abs_fset s" + assume a: "(list_all2 R OOO op \) r s" + then have b: "map Abs r \ map Abs s" proof (elim pred_compE) fix b ba - assume c: "list_all2 op \ r b" + assume c: "list_all2 R r b" assume d: "b \ ba" - assume e: "list_all2 op \ 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 \ 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 \ 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 \ OOO op \) r r \ (list_all2 op \ OOO op \) s s - \ abs_fset (map abs_fset r) = abs_fset (map abs_fset s)" - then have s: "(list_all2 op \ OOO op \) s s" by simp - have d: "map abs_fset r \ map abs_fset s" + assume a: "(list_all2 R OOO op \) r r \ (list_all2 R OOO op \) s s + \ abs_fset (map Abs r) = abs_fset (map Abs s)" + then have s: "(list_all2 R OOO op \) s s" by simp + have d: "map Abs r \ map Abs s" by (subst Quotient_rel[OF Quotient_fset]) (simp add: a) - have b: "map rep_fset (map abs_fset r) \ map rep_fset (map abs_fset s)" + have b: "map Rep (map Abs r) \ map Rep (map Abs s)" by (rule map_list_eq_cong[OF d]) - have y: "list_all2 op \ (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 \ OO list_all2 op \) (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 \ OO list_all2 R) (map Rep (map Abs r)) s" by (rule pred_compI) (rule b, rule y) - have z: "list_all2 op \ 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 \ OOO op \) 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 \) r s" using a c pred_compI by simp qed qed +lemma quotient_compose_list[quot_thm]: + shows "Quotient ((list_all2 op \) OOO (op \)) + (abs_fset \ (map abs_fset)) ((map rep_fset) \ 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 \ OOO op \) Nil Nil" - by (fact compose_list_refl) + by (rule compose_list_refl, rule list_eq_equivp) lemma Cons_rsp2 [quot_respect]: shows "(op \ ===> list_all2 op \ OOO op \ ===> list_all2 op \ OOO op \) Cons Cons" @@ -470,13 +474,13 @@ assumes a:"list_all2 op \ x x'" shows "list_all2 op \ (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 \ x x'" shows "list_all2 op \ (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 \) r r" -proof - have *: "r \ r" by (rule equivp_reflp[OF fset_equivp]) - show "list_all2 R r r" by (rule list_all2_refl''[OF q]) - with * show "(op \ 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 \)) - (abs_fset \ (map Abs)) ((map Rep) \ 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 \ 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 \) (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 \) r s = ((list_all2 R OOO op \) r r \ - (list_all2 R OOO op \) s s \ abs_fset (map Abs r) = abs_fset (map Abs s))" - proof (intro iffI conjI) - show "(list_all2 R OOO op \) r r" by (rule compose_list_refl2[OF e]) - show "(list_all2 R OOO op \) s s" by (rule compose_list_refl2[OF e]) - next - assume a: "(list_all2 R OOO op \) r s" - then have b: "map Abs r \ map Abs s" - proof (elim pred_compE) - fix b ba - assume c: "list_all2 R r b" - assume d: "b \ 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 \ 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 \) r r \ (list_all2 R OOO op \) s s - \ abs_fset (map Abs r) = abs_fset (map Abs s)" - then have s: "(list_all2 R OOO op \) s s" by simp - have d: "map Abs r \ map Abs s" - by (subst Quotient_rel[OF Quotient_fset]) (simp add: a) - have b: "map Rep (map Abs r) \ 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 \ 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 \) 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], []);