--- a/Quotient-Paper/Paper.thy Mon Jun 14 19:03:34 2010 +0200
+++ b/Quotient-Paper/Paper.thy Tue Jun 15 02:03:18 2010 +0200
@@ -8,9 +8,10 @@
begin
notation (latex output)
- rel_conj ("_ OOO _" [53, 53] 52) and
- "op -->" (infix "\<rightarrow>" 100) and
- "==>" (infix "\<Rightarrow>" 100) and
+ rel_conj ("_ \<circ>\<circ>\<circ> _" [53, 53] 52) and
+ pred_comp ("_ \<circ>\<circ> _") and
+ "op -->" (infix "\<longrightarrow>" 100) and
+ "==>" (infix "\<Longrightarrow>" 100) and
fun_map ("_ \<^raw:\mbox{\singlearr}> _" 51) and
fun_rel ("_ \<^raw:\mbox{\doublearr}> _" 51) and
list_eq (infix "\<approx>" 50) and (* Not sure if we want this notation...? *)
@@ -89,8 +90,10 @@
then be defined as the empty list and the union of two finite sets, written
@{text "\<union>"}, as list append.
- An area where quotients are ubiquitous is reasoning about programming language
- calculi. A simple example is the lambda-calculus, whose raw terms are defined as
+ Quotients are important in a variety of areas, but they are ubiquitous in
+ the area of reasoning about programming language calculi. A simple example
+ is the lambda-calculus, whose raw terms are defined as
+
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
@{text "t ::= x | t t | \<lambda>x.t"}\hfill\numbered{lambda}
@@ -185,8 +188,11 @@
Slightly more complicated is the definition of @{text "add"} having type
@{typ "int \<Rightarrow> int \<Rightarrow> int"}. Its definition is as follows
- @{text [display, indent=10] "add n m \<equiv> Abs_int (add_pair (Rep_int n) (Rep_int m))"}
-
+ \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+ @{text "add n m \<equiv> Abs_int (add_pair (Rep_int n) (Rep_int m))"}
+ \hfill\numbered{adddef}
+ \end{isabelle}
+
\noindent
where we take the representation of the arguments @{text n} and @{text m},
add them according to the function @{text "add_pair"} and then take the
@@ -210,7 +216,7 @@
terms of @{text flat}, @{text Rep_fset} and @{text Abs_fset}. The problem is
that the method used in the existing quotient
packages of just taking the representation of the arguments and then taking
- the abstraction of the result is \emph{not} enough. The reason is that case in case
+ the abstraction of the result is \emph{not} enough. The reason is that in case
of @{text "\<Union>"} we obtain the incorrect definition
@{text [display, indent=10] "\<Union> S \<equiv> Abs_fset (flat (Rep_fset S))"}
@@ -256,17 +262,16 @@
work.
*}
-
section {* Preliminaries and General Quotients\label{sec:prelims} *}
text {*
- We describe here briefly some of the most basic concepts of HOL
- we rely on and some of the important definitions given by Homeier
- \cite{Homeier05}.
-
- HOL is based on a simply-typed term-language, where types are
- annotated in Church-style (that is we can obtain immediately
- infer the type of term and its subterms).
+ We describe here briefly the most basic notions of HOL we rely on, and
+ the important definitions given by Homeier for quotients \cite{Homeier05}.
+
+ At its core HOL is based on a simply-typed term language, where types are
+ recorded in Church-style fashion (that means, we can infer the type of
+ a term and its subterms without any additional information). The grammars
+ for types and terms are as follows
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
\begin{tabular}{@ {}rl@ {\hspace{3mm}}l@ {}}
@@ -278,49 +283,92 @@
\noindent
We often write just @{text \<kappa>} for @{text "() \<kappa>"}, and use @{text "\<alpha>s"} and
- @{text "\<sigma>s"} to stand for list of type variables and types, respectively.
- The type of a term is often made explicit by writing @{text "t :: \<sigma>"} HOL
- contains a type @{typ bool} for booleans and the function type, written
- @{text "\<sigma> \<Rightarrow> \<tau>"}.
+ @{text "\<sigma>s"} to stand for collections of type variables and types,
+ respectively. The type of a term is often made explicit by writing @{text
+ "t :: \<sigma>"}. HOL contains a type @{typ bool} for booleans and the function
+ type, written @{text "\<sigma> \<Rightarrow> \<tau>"}. HOL also contains
+ many primitive and defined constants; for example equality @{text "= :: \<sigma> \<Rightarrow>
+ \<sigma> \<Rightarrow> bool"} and the identity function @{text "id :: \<sigma> => \<sigma>"} (the former
+ being primitive and the latter being defined as @{text
+ "\<lambda>x\<^sup>\<sigma>. x\<^sup>\<sigma>"}).
+ An important point to note is that theorems in HOL can be seen as a subset
+ of terms that are constructed specially (namely through axioms and prove
+ rules). As a result we are able later on to define automatic proof
+ procedures showing that one theorem implies another by decomposing the term
+ underlying the first theorem.
+
+ Like Homeier, our work relies on map-functions defined for every type constructor,
+ like @{text map} for lists. Homeier describes others for products, sums,
+ options and also the following map for function types
+
+ @{thm [display, indent=10] fun_map_def[no_vars, THEN eq_reflection]}
+
+ \noindent
+ Using this map-function, we can give the following, equivalent, but more
+ uniform, definition for @{text add} shown in \eqref{adddef}:
+ @{text [display, indent=10] "add \<equiv> (Rep_int \<singlearr> Rep_int \<singlearr> Abs_int) add_pair"}
- \begin{definition}[Quotient]
- A relation $R$ with an abstraction function $Abs$
- and a representation function $Rep$ is a \emph{quotient}
- if and only if:
+ \noindent
+ We will sometimes refer to a map-function defined for a type-constructor @{text \<kappa>}
+ as @{text "map_\<kappa>"}.
+
+ It will also be necessary to have operators, referred to as @{text "rel_\<kappa>"},
+ which define equivalence relations in terms of constituent equivalence
+ relations. For example given two equivalence relations @{text "R\<^isub>1"}
+ and @{text "R\<^isub>2"}, we can define an equivalence relations over
+ products as follows
+ %
+ @{text [display, indent=10] "(R\<^isub>1 \<tripple> R\<^isub>2) (x\<^isub>1, x\<^isub>2) (y\<^isub>1, y\<^isub>2) \<equiv> R\<^isub>1 x\<^isub>1 y\<^isub>1 \<and> R\<^isub>2 x\<^isub>2 y\<^isub>2"}
+ \noindent
+ Similarly, Homeier defines the following operator for defining equivalence
+ relations over function types:
+ %
+ @{thm [display, indent=10] fun_rel_def[of "R\<^isub>1" "R\<^isub>2", no_vars, THEN eq_reflection]}
+
+ The central definition in Homeier's work \cite{Homeier05} relates equivalence
+ relations, abstraction and representation functions:
+
+ \begin{definition}[Quotient Types]
+ Given a relation $R$, an abstraction function $Abs$
+ and a representation function $Rep$, the predicate @{term "Quotient R Abs Rep"}
+ means
\begin{enumerate}
\item @{thm (rhs1) Quotient_def[of "R", no_vars]}
\item @{thm (rhs2) Quotient_def[of "R", no_vars]}
\item @{thm (rhs3) Quotient_def[of "R", no_vars]}
\end{enumerate}
-
- \end{definition}
-
- \begin{definition}[Relation map and function map]\\
- @{thm fun_rel_def[of "R1" "R2", no_vars]}\\
- @{thm fun_map_def[no_vars]}
\end{definition}
- The main theorems for building higher order quotients is:
- \begin{lemma}[Function Quotient]
- If @{thm (prem 1) fun_quotient[no_vars]} and @{thm (prem 2) fun_quotient[no_vars]}
- then @{thm (concl) fun_quotient[no_vars]}
- \end{lemma}
-
- Higher Order Logic
-
+ \noindent
+ The value of this definition is that validity of @{text Quotient} can be
+ proved in terms of the validity of @{text "Quotient"} over the constituent types.
+ For example Homeier proves the following property for higher-order quotient
+ types:
+
+ \begin{proposition}[Function Quotient]\label{funquot}
+ @{thm[mode=IfThen] fun_quotient[where ?R1.0="R\<^isub>1" and ?R2.0="R\<^isub>2"
+ 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}
-
- {\it Say more about containers / maping functions }
+ \noindent
+ We will heavily rely on this part of Homeier's work including an extension
+ to deal with compositions of equivalence relations defined as follows
- Such maps for most common types (list, pair, sum,
- option, \ldots) are described in Homeier, and we assume that @{text "map"}
- is the function that returns a map for a given type.
+ \begin{definition}[Composition of Relations]
+ @{abbrev "rel_conj R\<^isub>1 R\<^isub>2"} where @{text "\<circ>\<circ>"} is the predicate
+ composition defined by the rule
+ %
+ @{thm [mode=Rule, display, indent=10] pred_compI[of "R\<^isub>1" "x" "y" "R\<^isub>2" "z"]}
+ \end{definition}
- {\it say something about our use of @{text "\<sigma>s"}}
-
+ \noindent
+ Unfortunately, restrictions in HOL's type-system prevent us from stating
+ and proving a quotient type theorem, like \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.
*}
section {* Quotient Types and Quotient Definitions\label{sec:type} *}
@@ -388,9 +436,9 @@
respectively. Given that @{text "R"} is an equivalence relation, the
following property
- \begin{property}
+ \begin{proposition}
@{text "Quotient R Abs_\<kappa>\<^isub>q Rep_\<kappa>\<^isub>q"}
- \end{property}
+ \end{proposition}
\noindent
holds for every quotient type defined
@@ -578,13 +626,20 @@
consequently no theorem involving this constant can be lifted to @{text
"\<alpha>"}-equated lambda terms. Homeier formulates the restrictions in terms of
the properties of \emph{respectfullness} and \emph{preservation}. We have
- to slighlty extend Homeier's definitions in order to deal with quotient
+ to slightly extend Homeier's definitions in order to deal with quotient
compositions.
To formally define what respectfulness is, we have to first define
the notion of \emph{aggregate equivalence relations}.
- @{text [display] "GIVE DEFINITION HERE"}
+ TBD
+
+ \begin{itemize}
+ \item @{text "REL(\<alpha>\<^isub>1, \<alpha>\<^isub>2)"} = @{text "op ="}
+ \item @{text "REL(\<sigma>, \<sigma>)"} = @{text "op ="}
+ \item @{text "REL((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n))\<kappa>, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>n))\<kappa>)"} = @{text "(rel \<kappa>) (REL(\<sigma>\<^isub>1,\<tau>\<^isub>1)) \<dots> (REL(\<sigma>\<^isub>n,\<tau>\<^isub>n))"}
+ \item @{text "REL((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n))\<kappa>\<^isub>1, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>m))\<kappa>\<^isub>2)"} = @{text "(rel \<kappa>\<^isub>1) (REL(\<rho>\<^isub>1,\<nu>\<^isub>1) \<dots> (REL(\<rho>\<^isub>p,\<nu>\<^isub>p) OOO Eqv_\<kappa>\<^isub>2"} provided @{text "\<eta> \<kappa>\<^isub>2 = (\<alpha>\<^isub>1\<dots>\<alpha>\<^isub>p)\<kappa>\<^isub>1 \<and> \<exists>s. s(\<sigma>s\<kappa>\<^isub>1)=\<rho>s\<kappa>\<^isub>1 \<and> s(\<tau>s\<kappa>\<^isub>2)=\<nu>s\<kappa>\<^isub>2"}
+ \end{itemize}
class returned by this constant depends only on the equivalence
classes of the arguments applied to the constant. To automatically
@@ -596,7 +651,7 @@
for example the respectfullness for @{text "append"}
can be stated as:
- @{text [display, indent=10] "(R \<doublearr> R \<doublearr> R) append append"}
+ @{text [display, indent=10] "(\<approx>\<^bsub>list\<^esub> \<doublearr> \<approx>\<^bsub>list\<^esub> \<doublearr> \<approx>\<^bsub>list\<^esub>) append append"}
\noindent
Which after unfolding the definition of @{term "op ===>"} is equivalent to:
@@ -606,21 +661,11 @@
\noindent An aggregate relation is defined in terms of relation
composition, so we define it first:
- \begin{definition}[Composition of Relations]
- @{abbrev "rel_conj R1 R2"} where @{text OO} is the predicate
- composition @{thm pred_compI[no_vars]}
- \end{definition}
+
The aggregate relation for an aggregate raw type and quotient type
is defined as:
- \begin{itemize}
- \item @{text "REL(\<alpha>\<^isub>1, \<alpha>\<^isub>2)"} = @{text "op ="}
- \item @{text "REL(\<sigma>, \<sigma>)"} = @{text "op ="}
- \item @{text "REL((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n))\<kappa>, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>n))\<kappa>)"} = @{text "(rel \<kappa>) (REL(\<sigma>\<^isub>1,\<tau>\<^isub>1)) \<dots> (REL(\<sigma>\<^isub>n,\<tau>\<^isub>n))"}
- \item @{text "REL((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n))\<kappa>\<^isub>1, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>m))\<kappa>\<^isub>2)"} = @{text "(rel \<kappa>\<^isub>1) (REL(\<rho>\<^isub>1,\<nu>\<^isub>1) \<dots> (REL(\<rho>\<^isub>p,\<nu>\<^isub>p) OOO Eqv_\<kappa>\<^isub>2"} provided @{text "\<eta> \<kappa>\<^isub>2 = (\<alpha>\<^isub>1\<dots>\<alpha>\<^isub>p)\<kappa>\<^isub>1 \<and> \<exists>s. s(\<sigma>s\<kappa>\<^isub>1)=\<rho>s\<kappa>\<^isub>1 \<and> s(\<tau>s\<kappa>\<^isub>2)=\<nu>s\<kappa>\<^isub>2"}
-
- \end{itemize}
Again, the last case is novel, so lets look at the example of
respectfullness for @{term concat}. The statement according to
@@ -642,10 +687,7 @@
element of @{term b'} is in relation with the appropriate element of
@{term b}.
-*}
-
-text {*
Sometimes a non-lifted polymorphic constant is instantiated to a
type being lifted. For example take the @{term "op #"} which inserts
an element in a list of pairs of natural numbers. When the theorem
@@ -668,11 +710,9 @@
to show that it respects the particular quotient type:
@{thm [display, indent=10] insert_preserve2[no_vars]}
-*}
-subsection {* Composition of Quotient theorems *}
+ {\it Composition of Quotient theorems}
-text {*
Given two quotients, one of which quotients a container, and the
other quotients the type in the container, we can write the
composition of those quotients. To compose two quotient theorems