nominal2: comparison Quotient-Paper/Paper.thy

equal deleted inserted replaced

-:d40031f786f0
+:72ce58b76c3b
 "LaTeXsugar"
 "../Nominal/FSet"
 begin
 notation (latex output)
-rel_conj ("_ OOO _" [53, 53] 52) and
+rel_conj ("_ \<circ>\<circ>\<circ> _" [53, 53] 52) and
-"op -->" (infix "\<rightarrow>" 100) and
+pred_comp ("_ \<circ>\<circ> _") and
-"==>" (infix "\<Rightarrow>" 100) 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...? *)
 fempty ("\<emptyset>") and
 funion ("_ \<union> _") and
 which states that two lists are equivalent if every element in one list is
 also member in the other. The empty finite set, written @{term "{||}"}, can
 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
+Quotients are important in a variety of areas, but they are ubiquitous in
-calculi. A simple example is the lambda-calculus, whose raw terms are defined as
+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}
 \end{isabelle}
 \noindent
 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
 abstraction of the result.  This is all straightforward and the existing
 quotient packages can deal with such definitions. But what is surprising
 \noindent
 The quotient package should automatically provide us with a definition for @{text "\<Union>"} in
 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))"}
 \noindent
 and preservation; Section \ref{sec:lift} describes the lifting of theorems,
 and Section \ref{sec:conc} concludes and compares our results to existing
 work.
 *}
 section {* Preliminaries and General Quotients\label{sec:prelims} *}
 text {*
-We describe here briefly some of the most basic concepts of HOL
+We describe here briefly the most basic notions of HOL we rely on, and
-we rely on and some of the important definitions given by Homeier
+the important definitions given by Homeier for quotients \cite{Homeier05}.
-\cite{Homeier05}.
+At its core HOL is based on a simply-typed term language, where types are
-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
-annotated in Church-style (that is we can obtain immediately
+a term and its subterms without any additional information). The grammars
-infer the type of term and its subterms).
+for types and terms are as follows
 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
 \begin{tabular}{@ {}rl@ {\hspace{3mm}}l@ {}}
 @{text "\<sigma>, \<tau> ::="} & @{text "\<alpha> | (\<sigma>,\<dots>, \<sigma>) \<kappa>"} & (type variables and type constructors)\\
 @{text "t, s ::="} & @{text "x\<^isup>\<sigma> | c\<^isup>\<sigma> | t t | \<lambda>x\<^isup>\<sigma>. t"} &
 \end{tabular}
 \end{isabelle}
 \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.
+@{text "\<sigma>s"} to stand for collections of type variables and types,
-The type of a term is often made explicit by writing @{text "t :: \<sigma>"} HOL
+respectively.  The type of a term is often made explicit by writing @{text
-contains a type @{typ bool} for booleans and the function type, written
+"t :: \<sigma>"}. HOL contains a type @{typ bool} for booleans and the function
-@{text "\<sigma> \<Rightarrow> \<tau>"}.
+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
-\begin{definition}[Quotient]
+"\<lambda>x\<^sup>\<sigma>. x\<^sup>\<sigma>"}).
-A relation $R$ with an abstraction function $Abs$
-and a representation function $Rep$ is a \emph{quotient}
+An important point to note is that theorems in HOL can be seen as a subset
-if and only if:
+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"}
+\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]\\
+\noindent
-@{thm fun_rel_def[of "R1" "R2", no_vars]}\\
+The value of this definition is that validity of @{text Quotient} can be
-@{thm fun_map_def[no_vars]}
+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}
+\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
+\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}
-The main theorems for building higher order quotients is:
+\noindent
-\begin{lemma}[Function Quotient]
+Unfortunately, restrictions in HOL's type-system prevent us from stating
-If @{thm (prem 1) fun_quotient[no_vars]} and @{thm (prem 2) fun_quotient[no_vars]}
+and proving a quotient type theorem, like \ref{funquot}, for compositions
-then @{thm (concl) fun_quotient[no_vars]}
+of relations. However, we can prove all instances where @{text R\<^isub>1} and
-\end{lemma}
+@{text "R\<^isub>2"} are built up by constituent equivalence relations.
-Higher Order Logic
-{\it Say more about containers / maping functions }
-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.
-{\it say something about our use of @{text "\<sigma>s"}}
 *}
 section {* Quotient Types and Quotient Definitions\label{sec:type} *}
 text {*
 quotient type and the raw type directly, as can be seen from their type,
 namely @{text "\<sigma> \<Rightarrow> \<alpha>s \<kappa>\<^isub>q"} and @{text "\<alpha>s \<kappa>\<^isub>q \<Rightarrow> \<sigma>"},
 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
 as above (for the proof see \cite{Homeier05}).
 \noindent
 This constant just does not respect @{text "\<alpha>"}-equivalence and as
 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
-class returned by this constant depends only on the equivalence
-classes of the arguments applied to the constant. To automatically
-lift a theorem that talks about a raw constant, to a theorem about
-the quotient type a respectfulness theorem is required.
-A respectfulness condition for a constant can be expressed in
-terms of an aggregate relation between the constant and itself,
-for example the respectfullness for @{text "append"}
-can be stated as:
-@{text [display, indent=10] "(R \<doublearr> R \<doublearr> R) append append"}
-\noindent
-Which after unfolding the definition of @{term "op ===>"} is equivalent to:
-@{thm [display, indent=10] append_rsp_unfolded[no_vars]}
-\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}
+class returned by this constant depends only on the equivalence
+classes of the arguments applied to the constant. To automatically
+lift a theorem that talks about a raw constant, to a theorem about
+the quotient type a respectfulness theorem is required.
+A respectfulness condition for a constant can be expressed in
+terms of an aggregate relation between the constant and itself,
+for example the respectfullness for @{text "append"}
+can be stated as:
+@{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:
+@{thm [display, indent=10] append_rsp_unfolded[no_vars]}
+\noindent An aggregate relation is defined in terms of relation
+composition, so we define it first:
+The aggregate relation for an aggregate raw type and quotient type
+is defined as:
 Again, the last case is novel, so lets look at the example of
 respectfullness for @{term concat}. The statement according to
 the definition above is:
 such that each element of @{term a} is in the relation with an appropriate
 element of @{term a'}, @{term a'} is in relation with @{term b'} and each
 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
 is lifted, the pairs of natural numbers are to become integers, but
 the head constant is still supposed to be the head constant, just
 For some constants (for example empty list) it is possible to show a
 general compositional theorem, but for @{term "op #"} it is necessary
 to show that it respects the particular quotient type:
 @{thm [display, indent=10] insert_preserve2[no_vars]}
-*}
+{\it Composition of Quotient theorems}
-subsection {* 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
 we compose the relations with relation composition as defined above
 and the abstraction and relation functions are the ones of the sub

changeset 2258	72ce58b76c3b
parent 2257	d40031f786f0
child 2259	85291ef50354