# HG changeset patch # User Christian Urban # Date 1276587856 -7200 # Node ID 4ae32dd02d14f7ff36f59e874f2757c600295482 # Parent e4699a240d2ca01e3e450c1500f04794ac014ee1# Parent 1fd6809f5a44a0f6c9d7984336957992c0db7925 merged diff -r e4699a240d2c -r 4ae32dd02d14 Nominal/FSet.thy --- a/Nominal/FSet.thy Tue Jun 15 08:56:13 2010 +0200 +++ b/Nominal/FSet.thy Tue Jun 15 09:44:16 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 e4699a240d2c -r 4ae32dd02d14 Quotient-Paper/Paper.thy --- a/Quotient-Paper/Paper.thy Tue Jun 15 08:56:13 2010 +0200 +++ b/Quotient-Paper/Paper.thy Tue Jun 15 09:44:16 2010 +0200 @@ -357,6 +357,10 @@ and ?abs1.0="Abs\<^isub>1" and ?abs2.0="Abs\<^isub>2" and ?rep1.0="Rep\<^isub>1" and ?rep2.0="Rep\<^isub>2"]} \end{proposition} + \begin{definition}[Respects] + An element @{text "x"} respects a relation @{text "R"} if and only if @{text "R x x"}. + \end{definition} + \noindent As a result, Homeier was able to build an automatic prover that can nearly always discharge a proof obligation involving @{text "Quotient"}. Our quotient @@ -372,10 +376,12 @@ \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} *} @@ -739,9 +745,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 @@ -792,10 +801,10 @@ \begin{tabular}{rcl} \multicolumn{3}{@ {\hspace{-4mm}}l}{abstractions (with same types and different types):}\\ @{text "REG (\x : \. t, \x : \. s)"} & $\dn$ & @{text "\x : \. REG (t, s)"}\\ - @{text "REG (\x : \. t, \x : \. s)"} & $\dn$ & @{text "\x : \ \ Res (REL (\, \)). REG (t, s)"}\\ + @{text "REG (\x : \. t, \x : \. s)"} & $\dn$ & @{text "\x : \ \ Respects (REL (\, \)). REG (t, s)"}\\ \multicolumn{3}{@ {\hspace{-4mm}}l}{quantification (over same types and different types):}\\ @{text "REG (\x : \. t, \x : \. s)"} & $\dn$ & @{text "\x : \. REG (t, s)"}\\ - @{text "REG (\x : \. t, \x : \. s)"} & $\dn$ & @{text "\x : \ \ Res (REL (\, \)). REG (t, s)"}\\ + @{text "REG (\x : \. t, \x : \. s)"} & $\dn$ & @{text "\x : \ \ Respects (REL (\, \)). REG (t, s)"}\\ \multicolumn{3}{@ {\hspace{-4mm}}l}{equalities (with same types and different types):}\\ @{text "REG ((op =) : \, (op =) : \)"} & $\dn$ & @{text "(op =) : \"}\\ @{text "REG ((op =) : \, (op =) : \)"} & $\dn$ & @{text "REL (\, \) : \"}\\ @@ -1036,27 +1045,8 @@ text {* - Oscar Slotosch~\cite{Slotosch97} implemented a mechanism that automatically - defines quotient types for Isabelle/HOL. It did not include theorem lifting. - John Harrison's quotient package~\cite{harrison-thesis} is the first one to - lift theorems, however only first order. There is work on quotient types in - non-HOL based systems and logical frameworks, namely theory interpretations - in PVS~\cite{PVS:Interpretations}, new types in MetaPRL~\cite{Nogin02}, or - the use of setoids in Coq, with some higher order issues~\cite{ChicliPS02}. - Larry Paulson shows a construction of quotients that does not require the - Hilbert Choice operator, again only first order~\cite{Paulson06}. - - The closest to our package is the package for HOL4 by Peter Homeier~\cite{Homeier05}, - which is the first one to support lifting of higher order theorems. In - comparison with this package we explore the notion of composition of quotients, - which allows lifting constants like @{term "concat"} and theorems about it. - The HOL4 package requires a big lists of constants, theorems to lift, - respectfullness conditions as input. Our package is modularized, so that - single definitions, single theorems or single respectfullness conditions etc - can be added, which allows a natural use of the quotient package together - with type-classes and locales. - - The code of the quotient package described here is already included in the + The code of the quotient package and the examples described here are + already included in the standard distribution of Isabelle.\footnote{Available from \href{http://isabelle.in.tum.de/}{http://isabelle.in.tum.de/}.} It is heavily used in Nominal Isabelle, which provides a convenient reasoning @@ -1067,38 +1057,42 @@ concurrency \cite{BengtsonParow09} and a strong normalisation result for cut-elimination in classical logic \cite{UrbanZhu08}. -*} + Oscar Slotosch~\cite{Slotosch97} implemented a mechanism that automatically + defines quotient types for Isabelle/HOL. It did not include theorem lifting. + John Harrison's quotient package~\cite{harrison-thesis} is the first one to + lift theorems, however only first order. There is work on quotient types in + non-HOL based systems and logical frameworks, namely theory interpretations + in PVS~\cite{PVS:Interpretations}, new types in MetaPRL~\cite{Nogin02}, or + the use of setoids in Coq, with some higher order issues~\cite{ChicliPS02}. + Larry Paulson shows a construction of quotients that does not require the + Hilbert Choice operator, again only first order~\cite{Paulson06}. + The closest to our package is the package for HOL4 by Peter Homeier~\cite{Homeier05}, + which is the first one to support lifting of higher order theorems. -subsection {* Contributions *} - -text {* - We present the detailed lifting procedure, which was not shown before. - - The quotient package presented in this paper has the following - advantages over existing packages: - \begin{itemize} - - \item We define quotient composition, function map composition and - relation map composition. This lets lifting polymorphic types with - subtypes quotiented as well. We extend the notions of - respectfulness and preservation to cope with quotient - composition. + Our quotient package for the first time explore the notion of + composition of quotients, which allows lifting constants like @{term + "concat"} and theorems about it. We defined the composition of + relations and showed examples of compositions of quotients which + allows lifting polymorphic types with subtypes quotiented as well. + We extended the notions of respectfullness and preservation; + with quotient compositions there is more than one condition needed + for a constant. - \item We allow lifting only some occurrences of quotiented - types. Rsp/Prs extended. (used in nominal) + Our package is modularized, so that single definitions, single + theorems or single respectfullness conditions etc can be added, + which allows the use of the quotient package together with + type-classes and locales. This has the advantage over packages + requiring big lists as input for the user of being able to develop + a theory progressively. - \item The quotient package is very modular. Definitions can be added - separately, rsp and prs can be proved separately, Quotients and maps - can be defined separately and theorems can - be lifted on a need basis. (useful with type-classes). - - \item Can be used both manually (attribute, separate tactics, - rsp/prs databases) and programatically (automated definition of - lifted constants, the rsp proof obligations and theorem statement - translation according to given quotients). - - \end{itemize} + We allow lifting only some occurrences of quotiented types, which + is useful in Nominal. The package can be used automatically with + an attribute, manually with separate tactics for parts of the lifting + procedure, and programatically. Automated definitions of constants + and respectfulness proof obligations are used in Nominal. Finally + we streamlined and showed the detailed lifting procedure, which + has not been presented before. \medskip \noindent