# HG changeset patch # User Cezary Kaliszyk # Date 1276585974 -7200 # Node ID dcffc2f132c991d5e165e13a6459c77a09a3e605 # Parent 9c44db3eef95cf5143f3df94370e882b0854fb1b Qpaper / Clarify the typing system and composition of quotients issue. diff -r 9c44db3eef95 -r dcffc2f132c9 Nominal/FSet.thy --- a/Nominal/FSet.thy Tue Jun 15 07:58:33 2010 +0200 +++ b/Nominal/FSet.thy Tue Jun 15 09:12:54 2010 +0200 @@ -80,7 +80,7 @@ text {* Composition Quotient *} -lemma list_rel_refl: +lemma list_rel_refl1: shows "(list_rel op \) r r" by (rule list_rel_refl) (metis equivp_def fset_equivp) @@ -88,7 +88,7 @@ shows "(list_rel op \ OOO op \) r r" proof have *: "r \ r" by (rule equivp_reflp[OF fset_equivp]) - show "list_rel op \ r r" by (rule list_rel_refl) + show "list_rel op \ r r" by (rule list_rel_refl1) with * show "(op \ OO list_rel op \) r r" .. qed @@ -103,6 +103,7 @@ unfolding list_eq.simps by (simp only: set_map set_in_eq) + lemma quotient_compose_list[quot_thm]: shows "Quotient ((list_rel op \) OOO (op \)) (abs_fset \ (map abs_fset)) ((map rep_fset) \ rep_fset)" @@ -112,11 +113,11 @@ 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_rel op \ (map rep_fset (rep_fset a)) (map rep_fset (rep_fset a))" - by (rule list_rel_refl) + by (rule list_rel_refl1) have c: "(op \ OO list_rel op \) (map rep_fset (rep_fset a)) (map rep_fset (rep_fset a))" by (rule, rule equivp_reflp[OF fset_equivp]) (rule b) show "(list_rel op \ OOO op \) (map rep_fset (rep_fset a)) (map rep_fset (rep_fset a))" - by (rule, rule list_rel_refl) (rule c) + by (rule, rule list_rel_refl1) (rule c) show "(list_rel op \ OOO op \) r s = ((list_rel op \ OOO op \) r r \ (list_rel op \ OOO op \) s s \ abs_fset (map abs_fset r) = abs_fset (map abs_fset s))" proof (intro iffI conjI) @@ -148,11 +149,11 @@ have b: "map rep_fset (map abs_fset r) \ map rep_fset (map abs_fset s)" by (rule map_rel_cong[OF d]) have y: "list_rel op \ (map rep_fset (map abs_fset s)) s" - by (fact rep_abs_rsp_left[OF Quotient_fset_list, OF list_rel_refl[of s]]) + by (fact rep_abs_rsp_left[OF Quotient_fset_list, OF list_rel_refl1[of s]]) have c: "(op \ OO list_rel op \) (map rep_fset (map abs_fset r)) s" by (rule pred_compI) (rule b, rule y) have z: "list_rel op \ r (map rep_fset (map abs_fset r))" - by (fact rep_abs_rsp[OF Quotient_fset_list, OF list_rel_refl[of r]]) + by (fact rep_abs_rsp[OF Quotient_fset_list, OF list_rel_refl1[of r]]) then show "(list_rel op \ OOO op \) r s" using a c pred_compI by simp qed @@ -653,13 +654,13 @@ assumes a:"list_rel op \ x x'" shows "list_rel op \ (x @ z) (x' @ z)" using a apply (induct x x' rule: list_induct2') - by simp_all (rule list_rel_refl) + by simp_all (rule list_rel_refl1) lemma append_rsp2_pre1: assumes a:"list_rel op \ x x'" shows "list_rel op \ (z @ x) (z @ x')" using a apply (induct x x' arbitrary: z rule: list_induct2') - apply (rule list_rel_refl) + apply (rule list_rel_refl1) apply (simp_all del: list_eq.simps) apply (rule list_rel_app_l) apply (simp_all add: reflp_def) @@ -674,7 +675,7 @@ apply (rule a) using b apply (induct z z' rule: list_induct2') apply (simp_all only: append_Nil2) - apply (rule list_rel_refl) + apply (rule list_rel_refl1) apply simp_all apply (rule append_rsp2_pre1) apply simp @@ -1414,9 +1415,6 @@ | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []); *} -no_notation - list_eq (infix "\" 50) - ML {* open Quotient_Info; @@ -1678,4 +1676,79 @@ apply auto done +lemma list_rel_refl: + assumes q: "equivp R" + shows "(list_rel R) r r" + by (rule list_rel_refl) (metis equivp_def fset_equivp q) + +lemma compose_list_refl2: + assumes q: "equivp R" + shows "(list_rel R OOO op \) r r" +proof + have *: "r \ r" by (rule equivp_reflp[OF fset_equivp]) + show "list_rel R r r" by (rule list_rel_refl[OF q]) + with * show "(op \ OO list_rel R) r r" .. +qed + +lemma quotient_compose_list_g[quot_thm]: + assumes q: "Quotient R Abs Rep" + and e: "equivp R" + shows "Quotient ((list_rel 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_rel R (map Rep (rep_fset a)) (map Rep (rep_fset a))" + by (rule list_rel_refl[OF e]) + have c: "(op \ OO list_rel R) (map Rep (rep_fset a)) (map Rep (rep_fset a))" + by (rule, rule equivp_reflp[OF fset_equivp]) (rule b) + show "(list_rel R OOO op \) (map Rep (rep_fset a)) (map Rep (rep_fset a))" + by (rule, rule list_rel_refl[OF e]) (rule c) + show "(list_rel R OOO op \) r s = ((list_rel R OOO op \) r r \ + (list_rel R OOO op \) s s \ abs_fset (map Abs r) = abs_fset (map Abs s))" + proof (intro iffI conjI) + show "(list_rel R OOO op \) r r" by (rule compose_list_refl2[OF e]) + show "(list_rel R OOO op \) s s" by (rule compose_list_refl2[OF e]) + next + assume a: "(list_rel R OOO op \) r s" + then have b: "map Abs r \ map Abs s" + proof (elim pred_compE) + fix b ba + assume c: "list_rel R r b" + assume d: "b \ ba" + assume e: "list_rel 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_rel_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_rel R OOO op \) r r \ (list_rel R OOO op \) s s + \ abs_fset (map Abs r) = abs_fset (map Abs s)" + then have s: "(list_rel 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_rel_cong[OF d]) + have y: "list_rel R (map Rep (map Abs s)) s" + by (fact rep_abs_rsp_left[OF list_quotient[OF q], OF list_rel_refl[OF e, of s]]) + have c: "(op \ OO list_rel R) (map Rep (map Abs r)) s" + by (rule pred_compI) (rule b, rule y) + have z: "list_rel R r (map Rep (map Abs r))" + by (fact rep_abs_rsp[OF list_quotient[OF q], OF list_rel_refl[OF e, of r]]) + then show "(list_rel R OOO op \) r s" + using a c pred_compI by simp + qed +qed + +no_notation + list_eq (infix "\" 50) + + end diff -r 9c44db3eef95 -r dcffc2f132c9 Quotient-Paper/Paper.thy --- a/Quotient-Paper/Paper.thy Tue Jun 15 07:58:33 2010 +0200 +++ b/Quotient-Paper/Paper.thy Tue Jun 15 09:12:54 2010 +0200 @@ -365,10 +365,11 @@ \end{definition} \noindent - Unfortunately, restrictions in HOL's type-system prevent us from stating - and proving a quotient type theorem, like Proposition \ref{funquot}, for compositions - of relations. However, we can prove all instances where @{text R\<^isub>1} and - @{text "R\<^isub>2"} are built up by constituent equivalence relations. + Unfortunately a quotient type theorem, like Proposition \ref{funquot}, for + the composition of any two quotients in not true (it is not even typable in + the HOL type system). However, we can prove useful instances for compatible + containers. We will show such example in Section \ref{sec:resp}. + *} section {* Quotient Types and Quotient Definitions\label{sec:type} *} @@ -728,9 +729,12 @@ Lets take again the example of @{term flat}. To be able to lift theorems that talk about it we provide the composition quotient - theorem: + theorem which allows quotienting inside the container: - @{thm [display, indent=10] quotient_compose_list[no_vars]} + If @{term R} is an equivalence relation and @{term "Quotient R Abs Rep"} + then + + @{text [display, indent=10] "Quotient (list_rel R \\\ \\<^bsub>list\<^esub>) (abs_fset \ map Abs) (map Rep o rep_fset)"} \noindent this theorem will then instantiate the quotients needed in the