diff -r d40031f786f0 -r 72ce58b76c3b Quotient-Paper/Paper.thy
--- 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