--- 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 \<approx>) r r"
by (rule list_rel_refl) (metis equivp_def fset_equivp)
@@ -88,7 +88,7 @@
shows "(list_rel op \<approx> OOO op \<approx>) r r"
proof
have *: "r \<approx> r" by (rule equivp_reflp[OF fset_equivp])
- show "list_rel op \<approx> r r" by (rule list_rel_refl)
+ show "list_rel op \<approx> r r" by (rule list_rel_refl1)
with * show "(op \<approx> OO list_rel op \<approx>) 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 \<approx>) OOO (op \<approx>))
(abs_fset \<circ> (map abs_fset)) ((map rep_fset) \<circ> 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 \<approx> (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 \<approx> OO list_rel op \<approx>) (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 \<approx> OOO op \<approx>) (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 \<approx> OOO op \<approx>) r s = ((list_rel op \<approx> OOO op \<approx>) r r \<and>
(list_rel op \<approx> OOO op \<approx>) s s \<and> 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) \<approx> map rep_fset (map abs_fset s)"
by (rule map_rel_cong[OF d])
have y: "list_rel op \<approx> (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 \<approx> OO list_rel op \<approx>) (map rep_fset (map abs_fset r)) s"
by (rule pred_compI) (rule b, rule y)
have z: "list_rel op \<approx> 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 \<approx> OOO op \<approx>) r s"
using a c pred_compI by simp
qed
@@ -653,13 +654,13 @@
assumes a:"list_rel op \<approx> x x'"
shows "list_rel op \<approx> (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 \<approx> x x'"
shows "list_rel op \<approx> (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 "\<approx>" 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 \<approx>) r r"
+proof
+ have *: "r \<approx> r" by (rule equivp_reflp[OF fset_equivp])
+ show "list_rel R r r" by (rule list_rel_refl[OF q])
+ with * show "(op \<approx> 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 \<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_rel R (map Rep (rep_fset a)) (map Rep (rep_fset a))"
+ by (rule list_rel_refl[OF e])
+ have c: "(op \<approx> 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 \<approx>) (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 \<approx>) r s = ((list_rel R OOO op \<approx>) r r \<and>
+ (list_rel R OOO op \<approx>) s s \<and> abs_fset (map Abs r) = abs_fset (map Abs s))"
+ proof (intro iffI conjI)
+ show "(list_rel R OOO op \<approx>) r r" by (rule compose_list_refl2[OF e])
+ show "(list_rel R OOO op \<approx>) s s" by (rule compose_list_refl2[OF e])
+ next
+ assume a: "(list_rel 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_rel R r b"
+ assume d: "b \<approx> 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 \<approx> 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 \<approx>) r r \<and> (list_rel R OOO op \<approx>) s s
+ \<and> abs_fset (map Abs r) = abs_fset (map Abs s)"
+ then have s: "(list_rel 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_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 \<approx> 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 \<approx>) r s"
+ using a c pred_compI by simp
+ qed
+qed
+
+no_notation
+ list_eq (infix "\<approx>" 50)
+
+
end
--- 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 \<circ>\<circ>\<circ> \<approx>\<^bsub>list\<^esub>) (abs_fset \<circ> 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 (\<lambda>x : \<sigma>. t, \<lambda>x : \<sigma>. s)"} & $\dn$ & @{text "\<lambda>x : \<sigma>. REG (t, s)"}\\
- @{text "REG (\<lambda>x : \<sigma>. t, \<lambda>x : \<tau>. s)"} & $\dn$ & @{text "\<lambda>x : \<sigma> \<in> Res (REL (\<sigma>, \<tau>)). REG (t, s)"}\\
+ @{text "REG (\<lambda>x : \<sigma>. t, \<lambda>x : \<tau>. s)"} & $\dn$ & @{text "\<lambda>x : \<sigma> \<in> Respects (REL (\<sigma>, \<tau>)). REG (t, s)"}\\
\multicolumn{3}{@ {\hspace{-4mm}}l}{quantification (over same types and different types):}\\
@{text "REG (\<forall>x : \<sigma>. t, \<forall>x : \<sigma>. s)"} & $\dn$ & @{text "\<forall>x : \<sigma>. REG (t, s)"}\\
- @{text "REG (\<forall>x : \<sigma>. t, \<forall>x : \<tau>. s)"} & $\dn$ & @{text "\<forall>x : \<sigma> \<in> Res (REL (\<sigma>, \<tau>)). REG (t, s)"}\\
+ @{text "REG (\<forall>x : \<sigma>. t, \<forall>x : \<tau>. s)"} & $\dn$ & @{text "\<forall>x : \<sigma> \<in> Respects (REL (\<sigma>, \<tau>)). REG (t, s)"}\\
\multicolumn{3}{@ {\hspace{-4mm}}l}{equalities (with same types and different types):}\\
@{text "REG ((op =) : \<sigma>, (op =) : \<sigma>)"} & $\dn$ & @{text "(op =) : \<sigma>"}\\
@{text "REG ((op =) : \<sigma>, (op =) : \<tau>)"} & $\dn$ & @{text "REL (\<sigma>, \<tau>) : \<sigma>"}\\
@@ -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