nominal2: comparison Quotient-Paper/Paper.thy

equal deleted inserted replaced

-:c0c5bc4ee8cb
+:bf3a29ea74f6
 "../Nominal/FSet"
 begin
 notation (latex output)
 rel_conj ("_ \<circ>\<circ>\<circ> _" [53, 53] 52) and
-pred_comp ("_ \<circ>\<circ> _") and
+pred_comp ("_ \<circ>\<circ> _" [1, 1] 30) 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...? *)
 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.
-Quotients are important in a variety of areas, but they are ubiquitous in
+Quotients are important in a variety of areas, but they are really 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}\ \ \ \ \ \ \ \ \ \ %%%
 \end{tikzpicture}
 \end{center}
 \noindent
 The starting point is an existing type, to which we refer as the
-\emph{raw type}, over which an equivalence relation given by the user is
+\emph{raw type} and over which an equivalence relation given by the user is
 defined. With this input the package introduces a new type, to which we
 refer as the \emph{quotient type}. This type comes with an
 \emph{abstraction} and a \emph{representation} function, written @{text Abs}
 and @{text Rep}.\footnote{Actually slightly more basic functions are given;
 the functions @{text Abs} and @{text Rep} need to be derived from them. We
-will show the details later. } These functions relate elements in the
+will show the details later. } They relate elements in the
-existing type to elements in the new type and vice versa; they can be uniquely
+existing type to elements in the new type and vice versa, and can be uniquely
 identified by their quotient type. For example for the integer quotient construction
 the types of @{text Abs} and @{text Rep} are
 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
 *}
 section {* Preliminaries and General Quotients\label{sec:prelims} *}
 text {*
-We describe here briefly the most basic notions of HOL we rely on, and
+We describe in this section 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
+recorded in Church-style fashion (that means, we can always 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@ {}}
 \noindent
 We often write just @{text \<kappa>} for @{text "() \<kappa>"}, and use @{text "\<alpha>s"} and
 @{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
+"t :: \<sigma>"}. HOL includes 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>
+many primitive and defined constants; this includes equality, with type @{text "= :: \<sigma> \<Rightarrow>
-\<sigma> \<Rightarrow> bool"} and the identity function @{text "id :: \<sigma> => \<sigma>"} (the former
+\<sigma> \<Rightarrow> bool"}, and the identity function, with type @{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
+rules). As a result we are able 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,
+like @{text map} for lists. Homeier describes in \cite{Homeier05} map-functions
+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
 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>}
+Using extensionality and unfolding the definition, we can get back to \eqref{adddef}.
-as @{text "map_\<kappa>"}.
+In what follows we shall use the terminology @{text "map_\<kappa>"} for a map-function
+defined for the type-constructor @{text \<kappa>}. In our implementation we have
+a database of map-functions that can be dynamically extended.
 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
+Homeier gives also the following operator for defining equivalence
-relations over function types:
+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:
 \item @{thm (rhs3) Quotient_def[of "R", no_vars]}
 \end{enumerate}
 \end{definition}
 \noindent
-The value of this definition is that validity of @{text Quotient} can be
+The value of this definition is that validity of @{text "Quotient R Abs Rep"} can
-proved in terms of the validity of @{text "Quotient"} over the constituent types.
+often be proved in terms of the validity of @{text "Quotient"} over the constituent
+types of @{text "R"}, @{text Abs} and @{text Rep}.
 For example Homeier proves the following property for higher-order quotient
 types:
-\begin{proposition}[Function Quotient]\label{funquot}
+\begin{proposition}\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}
 \begin{definition}[Respects]\label{def:respects}
 An element @{text "x"} respects a relation @{text "R"} if and only if @{text "R x x"}.
 \end{definition}
 \noindent
-We will heavily rely on this part of Homeier's work including an extension
+As a result, Homeier was able to build an automatic prover that can nearly
+always discharge a proof obligation involving @{text "Quotient"}. Our quotient
+package makes heavy
+use of 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
 text {*
 The first step in a quotient construction is to take a name for the new
 type, say @{text "\<kappa>\<^isub>q"}, and an equivalence relation, say @{text R},
 defined over a raw type, say @{text "\<sigma>"}. The type of the equivalence
-relation must be of type @{text "\<sigma> \<Rightarrow> \<sigma> \<Rightarrow> bool"}. The user-visible part of
+relation must be @{text "\<sigma> \<Rightarrow> \<sigma> \<Rightarrow> bool"}. The user-visible part of
-the declaration is therefore
+the quotient type declaration is therefore
 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
-\isacommand{quotient\_type}~~@{text "\<alpha>s \<kappa>\<^isub>q = \<sigma> / R"}
+\isacommand{quotient\_type}~~@{text "\<alpha>s \<kappa>\<^isub>q = \<sigma> / R"}\hfill\numbered{typedecl}
 \end{isabelle}
 \noindent
 and a proof that @{text "R"} is indeed an equivalence relation. Two concrete
 examples are
 \end{isabelle}
 \noindent
 which introduce the type of integers and of finite sets using the
 equivalence relations @{text "\<approx>\<^bsub>nat \<times> nat\<^esub>"} and @{text
-"\<approx>\<^bsub>list\<^esub>"} defined earlier in \eqref{natpairequiv} and
+"\<approx>\<^bsub>list\<^esub>"} defined in \eqref{natpairequiv} and
 \eqref{listequiv}, respectively (the proofs about being equivalence
-relations is omitted).  Given this data, we declare internally
+relations is omitted).  Given this data, we declare for \eqref{typedecl} internally
 the quotient types as
 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
 \isacommand{typedef}~~@{text "\<alpha>s \<kappa>\<^isub>q = {c. \<exists>x. c = R x}"}
 \end{isabelle}
 \noindent
 where the right-hand side is the (non-empty) set of equivalence classes of
 @{text "R"}. The restriction in this declaration is that the type variables
 in the raw type @{text "\<sigma>"} must be included in the type variables @{text
 "\<alpha>s"} declared for @{text "\<kappa>\<^isub>q"}. HOL will provide us with the following
-abstraction and representation functions having the type
+abstraction and representation functions
 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
 @{text "abs_\<kappa>\<^isub>q :: \<sigma> set \<Rightarrow> \<alpha>s \<kappa>\<^isub>q"}\hspace{10mm}@{text "rep_\<kappa>\<^isub>q :: \<alpha>s \<kappa>\<^isub>q \<Rightarrow> \<sigma> set"}
 \end{isabelle}
 \noindent
-They relate the new quotient type and equivalence classes of the raw
+As can be seen from the type, they relate the new quotient type and equivalence classes of the raw
 type. However, as Homeier \cite{Homeier05} noted, it is much more convenient
 to work with the following derived abstraction and representation functions
 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
 @{text "Abs_\<kappa>\<^isub>q x \<equiv> abs_\<kappa>\<^isub>q (R x)"}\hspace{10mm}@{text "Rep_\<kappa>\<^isub>q x \<equiv> \<epsilon> (rep_\<kappa>\<^isub>q x)"}
 as above (for the proof see \cite{Homeier05}).
 The next step in a quotient construction is to introduce definitions of new constants
 involving the quotient type. These definitions need to be given in terms of concepts
 of the raw type (remember this is the only way how to extend HOL
-with new definitions). For the user visible is the declaration
+with new definitions). For the user the visible part of such definitions is the declaration
 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
 \isacommand{quotient\_definition}~~@{text "c :: \<tau>"}~~\isacommand{is}~~@{text "t :: \<sigma>"}
 \end{isabelle}
 \noindent
 where @{text t} is the definiens (its type @{text \<sigma>} can always be inferred)
 and @{text "c"} is the name of definiendum, whose type @{text "\<tau>"} needs to be
 given explicitly (the point is that @{text "\<tau>"} and @{text "\<sigma>"} can only differ
-in places where a quotient and raw type are involved). Two concrete examples are
+in places where a quotient and raw type is involved). Two concrete examples are
 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
 \begin{tabular}{@ {}l}
 \isacommand{quotient\_definition}~~@{text "0 :: int"}~~\isacommand{is}~~@{text "(0::nat, 0::nat)"}\\
 \isacommand{quotient\_definition}~~@{text "\<Union> :: (\<alpha> fset) fset \<Rightarrow> \<alpha> fset"}~~%
 abstraction} and \emph{representation functions} using the functions @{text "ABS (\<sigma>,
 \<tau>)"} and @{text "REP (\<sigma>, \<tau>)"} whose clauses we give below. The idea behind
 these two functions is to recursively descend into the raw types @{text \<sigma>} and
 quotient types @{text \<tau>}, and generate the appropriate
 @{text "Abs"} and @{text "Rep"} in places where the types differ. Therefore
-we generate just the identity whenever the types are equal. All clauses
+we generate just the identity whenever the types are equal. On the ``way'' down,
-are as follows:
+however we might have to use map-functions to let @{text Abs} and @{text Rep} act
+over the appropriate types. The clauses of @{text ABS} and @{text REP}
+are as follows (where we use the short-hand notation @{text "ABS (\<sigma>s, \<tau>s)"} to mean
+@{text "ABS (\<sigma>\<^isub>1, \<tau>\<^isub>1)\<dots>ABS (\<sigma>\<^isub>i, \<tau>\<^isub>i)"}; similarly for @{text REP}):
 \begin{center}
 \hfill
 \begin{tabular}{rcl}
 \multicolumn{3}{@ {\hspace{-4mm}}l}{equal types:}\\
 @{text "REP (\<sigma>s \<kappa>, \<tau>s \<kappa>\<^isub>q)"} & $\dn$ & @{text "(MAP(\<rho>s \<kappa>) (REP (\<sigma>s', \<tau>s))) \<circ> Rep_\<kappa>\<^isub>q"}
 \end{tabular}\hfill\numbered{ABSREP}
 \end{center}
 %
 \noindent
-where in the last two clauses we have that the quotient type @{text "\<alpha>s
+where in the last two clauses we have that the type @{text "\<alpha>s
 \<kappa>\<^isub>q"} is the quotient of the raw type @{text "\<rho>s \<kappa>"} (for example
 @{text "int"} and @{text "nat \<times> nat"}, or @{text "\<alpha> fset"} and @{text "\<alpha>
 list"}). The quotient construction ensures that the type variables in @{text
 "\<rho>s"} must be among the @{text "\<alpha>s"}. The @{text "\<sigma>s'"} are given by the
 matchers for the @{text "\<alpha>s"} when matching @{text "\<rho>s \<kappa>"} against
 aggregate map-function:
 @{text [display, indent=10] "\<lambda>a b. map_prod (map a) b"}
 \noindent
-which we need to define the aggregate abstraction and representation functions.
+which we need in order to define the aggregate abstraction and representation
+functions.
 To see how these definitions pan out in practise, let us return to our
 example about @{term "concat"} and @{term "fconcat"}, where we have the raw type
 @{text "(\<alpha> list) list \<Rightarrow> \<alpha> list"} and the quotient type @{text "(\<alpha> fset) fset \<Rightarrow> \<alpha>
 fset"}. Feeding them into @{text ABS} gives us (after some @{text "\<beta>"}-simplifications)
 then @{text "Abs"} is of type @{text "\<sigma> \<Rightarrow> \<tau>"} and @{text "Rep"} of type
 @{text "\<tau> \<Rightarrow> \<sigma>"}.
 \end{lemma}
 \begin{proof}
-By induction and analysing the definitions of @{text "ABS"}, @{text "REP"}
+By mutual induction and analysing the definitions of @{text "ABS"}, @{text "REP"}
 and @{text "MAP"}. The cases of equal types and function types are
 straightforward (the latter follows from @{text "\<singlearr>"} having the
 type @{text "(\<alpha> \<Rightarrow> \<beta>) \<Rightarrow> (\<gamma> \<Rightarrow> \<delta>) \<Rightarrow> (\<beta> \<Rightarrow> \<gamma>) \<Rightarrow> (\<alpha> \<Rightarrow> \<delta>)"}). In case of equal type
 constructors we can observe that a map-function after applying the functions
 @{text "ABS (\<sigma>s, \<tau>s)"} produces a term of type @{text "\<sigma>s \<kappa> \<Rightarrow> \<tau>s \<kappa>"}.  The

changeset 2272	bf3a29ea74f6
parent 2271	c0c5bc4ee8cb
parent 2270	4ae32dd02d14
child 2273	d62c082cb56b