--- a/Quotient-Paper-jv/Paper.thy Tue Feb 19 05:38:46 2013 +0000
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,1675 +0,0 @@
-(*<*)
-theory Paper
-imports "Quotient"
- "~~/src/HOL/Library/Quotient_Syntax"
- "~~/src/HOL/Library/LaTeXsugar"
- "~~/src/HOL/Quotient_Examples/FSet"
-begin
-
-notation (latex output)
- rel_conj ("_ \<circ>\<circ>\<circ> _" [53, 53] 52) and
- pred_comp ("_ \<circ>\<circ> _" [1, 1] 30) and
- implies (infix "\<longrightarrow>" 100) and
- "==>" (infix "\<Longrightarrow>" 100) and
- map_fun ("_ \<singlearr> _" 51) and
- fun_rel ("_ \<doublearr> _" 51) and
- list_eq (infix "\<approx>" 50) and (* Not sure if we want this notation...? *)
- empty_fset ("\<emptyset>") and
- union_fset ("_ \<union> _") and
- insert_fset ("{_} \<union> _") and
- Cons ("_::_") and
- concat ("flat") and
- concat_fset ("\<Union>") and
- Quotient ("Quot _ _ _")
-
-declare [[show_question_marks = false]]
-
-ML {*
-fun nth_conj n (_, r) = nth (HOLogic.dest_conj r) n;
-
-fun style_lhs_rhs proj = Scan.succeed (fn ctxt => fn t =>
- let
- val concl =
- Object_Logic.drop_judgment (Proof_Context.theory_of ctxt) (Logic.strip_imp_concl t)
- in
- case concl of (_ $ l $ r) => proj (l, r)
- | _ => error ("Binary operator expected in term: " ^ Syntax.string_of_term ctxt concl)
- end);
-*}
-
-setup {*
- Term_Style.setup "rhs1" (style_lhs_rhs (nth_conj 0)) #>
- Term_Style.setup "rhs2" (style_lhs_rhs (nth_conj 1)) #>
- Term_Style.setup "rhs3" (style_lhs_rhs (nth_conj 2))
-*}
-
-fun add_pair :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
-where "add_pair (n1, m1) (n2, m2) = (n1 + n2, m1 + m2)"
-
-fun minus_pair :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
-where "minus_pair (n, m) = (m, n)"
-
-fun
- intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" ("_ \<approx> _" [50, 50] 50)
-where
- "intrel (x, y) (u, v) = (x + v = u + y)"
-
-(*>*)
-
-section {* Introduction *}
-
-text {*
- \noindent
- One might think quotients have been studied to death, but in the
- context of theorem provers a number questions concerning them are
- far from settled. In this paper we address the question of how to
- establish a convenient reasoning infrastructure for quotient
- constructions in the Isabelle/HOL theorem prover. Higher-Order Logic
- (HOL) consists of a small number of axioms and inference rules over
- a simply-typed term-language. Safe reasoning in HOL is ensured by
- two very restricted mechanisms for extending the logic: one is the
- definition of new constants in terms of existing ones; the other is
- the introduction of new types by identifying non-empty subsets in
- existing types. Previous work has shown how to use both mechanisms
- for dealing with quotient constructions in HOL (see
- \cite{Homeier05,Paulson06}). For example the integers in
- Isabelle/HOL are constructed by a quotient construction over the
- type @{typ "nat \<times> nat"} and the equivalence relation
-
-
- \begin{isabelle}\ \ \ \ \ %%%
- @{text "(n\<^isub>1, n\<^isub>2) \<approx> (m\<^isub>1, m\<^isub>2) \<equiv> n\<^isub>1 + m\<^isub>2 = m\<^isub>1 + n\<^isub>2"}\hfill\numbered{natpairequiv}
- \end{isabelle}
-
- \noindent
- This constructions yields the new type @{typ int}, and definitions for @{text
- "0"} and @{text "1"} of type @{typ int} can be given in terms of pairs of
- natural numbers (namely @{text "(0, 0)"} and @{text "(1, 0)"}). Operations
- such as @{text "add"} with type @{typ "int \<Rightarrow> int \<Rightarrow> int"} can be defined
- in terms of operations on pairs of natural numbers:
-
- \begin{isabelle}\ \ \ \ \ %%%
- @{thm add_pair.simps[where ?n1.0="n\<^isub>1" and ?n2.0="n\<^isub>2" and ?m1.0="m\<^isub>1" and ?m2.0="m\<^isub>2", THEN eq_reflection]}%
- \hfill\numbered{addpair}
- \end{isabelle}
-
- \noindent
- Negation on integers is defined in terms of swapping of pairs:
-
- \begin{isabelle}\ \ \ \ \ %%%
- @{thm minus_pair.simps[where ?n="n" and ?m="m", THEN eq_reflection]}%
- \hfill\numbered{minuspair}
- \end{isabelle}
-
- \noindent
- Similarly one can construct the type of finite sets, written @{term
- "\<alpha> fset"}, by quotienting the type @{text "\<alpha> list"} according to the
- equivalence relation
-
- \begin{isabelle}\ \ \ \ \ %%%
- @{text "xs \<approx> ys \<equiv> (\<forall>x. memb x xs \<longleftrightarrow> memb x ys)"}\hfill\numbered{listequiv}
- \end{isabelle}
-
- \noindent
- which states that two lists are equivalent if every element in one
- list is also member in the other, and vice versa. 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 really ubiquitous in
- the area of reasoning about programming language calculi. A simple example
- is the lambda-calculus, whose raw, or un-quotient, terms are defined as
-
- \begin{isabelle}\ \ \ \ \ %%%
- @{text "t ::= x | t t | \<lambda>x.t"}%\hfill\numbered{lambda}
- \end{isabelle}
-
- \noindent
- The problem with this definition arises from the need to reason
- modulo $\alpha$-equivalence, for instance, when one attempts to
- prove formally the substitution lemma \cite{Barendregt81} by
- induction over the structure of terms. This can be fiendishly
- complicated (see \cite[Pages 94--104]{CurryFeys58} for some
- ``rough'' sketches of a proof about raw lambda-terms). In contrast,
- if we reason about $\alpha$-equated lambda-terms, that means terms
- quotient according to $\alpha$-equivalence, then the reasoning
- infrastructure provided, for example, by Nominal Isabelle
- \cite{UrbanKaliszyk11} makes the formal proof of the substitution
- lemma almost trivial. The fundamental reason is that in case of
- $\alpha$-equated terms, equality coincides with $\alpha$-equivalence and
- we can use for reasoning HOL's built-in notion of ``replacing equals by equals''.
-
- There is also often a need to consider quotients of parial equivalence relations. For
- example the rational numbers
- can be constructed using pairs of integers and the partial equivalence relation
-
- \begin{isabelle}\ \ \ \ \ %%%
- @{text "(n\<^isub>1, n\<^isub>2) \<approx> (m\<^isub>1, m\<^isub>2) \<equiv> n\<^isub>1 * m\<^isub>2 = m\<^isub>1 * n\<^isub>2"}\hfill\numbered{ratpairequiv}
- \end{isabelle}
-
- \noindent
- where @{text "n\<^isub>2"} and @{text "m\<^isub>2"} are not allowed to be zero.
-
- The difficulty is that in order to be able to reason about integers,
- finite sets, etc.~one needs to establish a reasoning infrastructure
- by transferring, or \emph{lifting}, definitions and theorems from
- the raw type @{typ "nat \<times> nat"} to the quotient type @{typ int}
- (similarly for finite sets, $\alpha$-equated lambda-terms and
- rational numbers). This lifting usually requires a reasoning effort
- that can be rather repetitive and involves explicit conversions
- between the quotient and raw level in form of abstraction and
- representation functions \cite{Paulson06}. In principle it is feasible to do this
- work manually if one has only a few quotient constructions at
- hand. But if they have to be done over and over again, as in Nominal
- Isabelle, then manual reasoning is not an option.
-
- The purpose of a \emph{quotient package} is to ease the lifting of
- theorems and automate the reasoning as much as possible. Before we
- delve into the details, let us show how the user interacts with our
- quotient package when defining integers. We assume the definitions
- involving pairs of natural numbers shown in \eqref{natpairequiv},
- \eqref{addpair} and \eqref{minuspair} have already been made. A
- quotient can then be introduced by declaring the new type (in this case
- @{typ int}), the raw type (that is @{typ "nat \<times> nat"}) and the
- equivalence relation (that is @{text intrel} defined in
- \eqref{natpairequiv}).
-*}
-
- quotient_type int = "nat \<times> nat" / intrel
-
-txt {*
- \noindent
- This declaration requires the user to prove that @{text intrel} is
- indeed an equivalence relation, whereby an equivalence
- relation is defined as one that is reflexive, symmetric and
- transitive. This proof obligation can thus be discharged by
- unfolding the definitions and using the standard automatic proving
- tactic in Isabelle/HOL.
-*}
- unfolding equivp_reflp_symp_transp
- unfolding reflp_def symp_def transp_def
- by auto
-(*<*)
- instantiation int :: "{zero, one, plus, uminus}"
- begin
-(*>*)
-text {*
- \noindent
- Next we can declare the constants @{text "0"} and @{text "1"} for the
- quotient type @{text int}.
-*}
- quotient_definition
- "0 \<Colon> int" is "(0\<Colon>nat, 0\<Colon>nat)" .
-
- quotient_definition
- "1 \<Colon> int" is "(1\<Colon>nat, 0\<Colon>nat)" .
-
-text {*
- \noindent
- To be useful, we can also need declare two operations for adding two
- integers (written @{text plus}) and negating an integer
- (written @{text "uminus"}).
-*}
-
- quotient_definition
- "plus \<Colon> int \<Rightarrow> int \<Rightarrow> int" is add_pair
- by auto
-
- quotient_definition
- "uminus \<Colon> int \<Rightarrow> int" is minus_pair
- by auto
-(*<*)
- instance ..
-
- end
-(*>*)
-
-text {*
- \noindent
- Isabelle/HOL can introduce some convenient short-hand notation for these
- operations allowing the user to write
- addition as infix operation, for example @{text "i + j"}, and
- negation as prefix operation, for example @{text "- i"}. In both
- cases, however, the declaration requires the user to discharge a
- proof-obligation which ensures that the operations a
- \emph{respectful}. This property ensures that the operations are
- well-defined on the quotient level (a formal definition of
- respectfulness will be given later). Both proofs can be solved by
- the automatic proving tactic in Isabelle/HOL.
-
- Besides helping with declarations of quotient types and definitions
- of constants, the point of a quotient package is to help with
- proving properties about quotient types. For example we might be
- interested in the usual property that zero is an ???. This property
- can be stated as follows:
-*}
-
- lemma zero_add:
- shows "0 + i = (i::int)"
- proof(descending)
-txt {*
- \noindent
- The tactic @{text "descending"} automatically transfers this property of integers
- to a proof-obligation involving pairs of @{typ nat}s. (There is also
- a tactic, called @{text lifting}, which automatically transfers properties
- from the raw level to the quotient type.) In case of lemma @{text "zero_add"}
- we obtain the subgoal
-
- \begin{isabelle}\ \ \ \ \ %%%
- @{text "add_pair (0, 0) i \<approx> i"}
- \end{isabelle}
-
- \noindent
- which can be solved again by the automatic proving tactic @{text "auto"}, as follows
-*}
- qed(auto)
-
-text {*
- In this simple example the task of the user is to state the property for integers
- and use the quotient package and automatic proving tools of Isabelle/HOL to do
- the ``rest''. A more interesting example is to establish an induction principle for
- integers. For this we first establish the following induction principle where the
- induction proceeds over two natural numbers.
-*}
-
- lemma nat_induct2:
- assumes "P 0 0"
- and "\<And>n m. P n m \<Longrightarrow> P (Suc n) m"
- and "\<And>n m. P n m \<Longrightarrow> P n (Suc m)"
- shows "P n m"
- using assms
- by (induction_schema) (pat_completeness, lexicographic_order)
-
-text {*
- \noindent
- The symbol @{text "\<And>"} stands for Isabelle/HOL's universal quantifier and
- @{text "\<Longrightarrow>"} for its implication.
- As can be seen, this induction principle can be conveniently established using the
- reasoning infrastructure of the function package \cite{???}, which
- provides the tactics @{text "induction_schema"}, @{text "pat_completeness"}
- and @{text "lexicographic_order"}. These tactics enable Isabelle/HOL
- to use well-founded induction to prove @{text "nat_induct2"}. Our
- quotient package can now be used to prove the following property:
-*}
-
- lemma int_induct:
- assumes "P 0"
- and "\<And>i. P i \<Longrightarrow> P (i + 1)"
- and "\<And>i. P i \<Longrightarrow> P (i + (- 1))"
- shows "P (j::int)"
- using assms
- proof (descending)
-
-txt {*
- \noindent
- The @{text descending} tactic transfers it to the following proof
- obligation on the raw level.
-
- @{subgoals[display]}
-
- \noindent
- Note that the variable @{text "j"} in this subgoal is of type
- @{text "nat \<times> nat"}. This subgoal cannot be proved automatically by
- @{text auto}, but if we give it the hint to use @{text nat_induct2},
- then @{text auto} can discharge it as follows.
-
-*}
- qed (auto intro: nat_induct2)
-
-text {*
- This completes the proof of the induction principle
- for integers. Isabelle/HOL would allow us to inspect the
- detailed reasoning steps involved which would confirm that
- @{text "int_induct"} has been proved from ``first-principles''
- by transforming the property over the quotient type @{text int}
- to a corresponding property one on the raw level.
-
-
- In the
- context of HOL, there have been a few quotient packages already
- \cite{harrison-thesis,Slotosch97}. The most notable one is by Homeier
- \cite{Homeier05} implemented in HOL4. The fundamental construction these
- quotient packages perform can be illustrated by the following picture:
-
-%%% FIXME: Referee 1 says:
-%%% Diagram is unclear. Firstly, isn't an existing type a "set (not sets) of raw elements"?
-%%% Secondly, isn't the _set of_ equivalence classes mapped to and from the new type?
-%%% Thirdly, what do the words "non-empty subset" refer to ?
-
-%%% Cezary: I like the diagram, maybe 'new type' could be outside, but otherwise
-%%% I wouldn't change it.
-
- \begin{center}
- \mbox{}\hspace{20mm}\begin{tikzpicture}[scale=1.1]
- %%\draw[step=2mm] (-4,-1) grid (4,1);
-
- \draw[very thick] (0.7,0.3) circle (4.85mm);
- \draw[rounded corners=1mm, very thick] ( 0.0,-0.9) rectangle ( 1.8, 0.9);
- \draw[rounded corners=1mm, very thick] (-1.95,0.8) rectangle (-2.9,-0.195);
-
- \draw (-2.0, 0.8) -- (0.7,0.8);
- \draw (-2.0,-0.195) -- (0.7,-0.195);
-
- \draw ( 0.7, 0.23) node {\begin{tabular}{@ {}c@ {}}equiv-\\[-1mm]clas.\end{tabular}};
- \draw (-2.45, 0.35) node {\begin{tabular}{@ {}c@ {}}new\\[-1mm]type\end{tabular}};
- \draw (1.8, 0.35) node[right=-0.1mm]
- {\begin{tabular}{@ {}l@ {}}existing\\[-1mm] type\\ (sets of raw elements)\end{tabular}};
- \draw (0.9, -0.55) node {\begin{tabular}{@ {}l@ {}}non-empty\\[-1mm]subset\end{tabular}};
-
- \draw[->, very thick] (-1.8, 0.36) -- (-0.1,0.36);
- \draw[<-, very thick] (-1.8, 0.16) -- (-0.1,0.16);
- \draw (-0.95, 0.26) node[above=0.4mm] {@{text Rep}};
- \draw (-0.95, 0.26) node[below=0.4mm] {@{text Abs}};
- \end{tikzpicture}
- \end{center}
-
- \noindent
- The starting point is an existing type, to which we refer as the
- \emph{raw type} and over which an equivalence relation is given by the user.
- 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. } They relate elements in the
- 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}\ \ \ \ \ %%%
- @{text "Abs :: nat \<times> nat \<Rightarrow> int"}\hspace{10mm}@{text "Rep :: int \<Rightarrow> nat \<times> nat"}
- \end{isabelle}
-
- \noindent
- We therefore often write @{text Abs_int} and @{text Rep_int} if the
- typing information is important.
-
- Every abstraction and representation function stands for an isomorphism
- between the non-empty subset and elements in the new type. They are
- necessary for making definitions involving the new type. For example @{text
- "0"} and @{text "1"} of type @{typ int} can be defined as
-
-
- \begin{isabelle}\ \ \ \ \ %%%
- @{text "0 \<equiv> Abs_int (0, 0)"}\hspace{10mm}@{text "1 \<equiv> Abs_int (1, 0)"}
- \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
-
- \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 is
- that none of them can deal with slightly more complicated definitions involving
- \emph{compositions} of quotients. Such compositions are needed for example
- in case of quotienting lists to yield finite sets and the operator that
- flattens lists of lists, defined as follows
-
- \begin{isabelle}\ \ \ \ \ %%%
- \begin{tabular}{@ {}l}
- @{thm concat.simps(1)[THEN eq_reflection]}\\
- @{thm concat.simps(2)[THEN eq_reflection, where x1="x" and xs1="xs"]}
- \end{tabular}
- \end{isabelle}
-
- \noindent
- where @{text "@"} is the usual
- list append. We expect that the corresponding
- operator on finite sets, written @{term "fconcat"},
- builds finite unions of finite sets:
-
- \begin{isabelle}\ \ \ \ \ %%%
- \begin{tabular}{@ {}l}
- @{thm concat_empty_fset[THEN eq_reflection]}\\
- @{thm concat_insert_fset[THEN eq_reflection, where x1="x" and S1="S"]}
- \end{tabular}
- \end{isabelle}
-
- \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 in case
- of @{text "\<Union>"} we obtain the incorrect definition
-
- \begin{isabelle}\ \ \ \ \ %%%
- @{text "\<Union> S \<equiv> Abs_fset (flat (Rep_fset S))"}
- \end{isabelle}
-
- \noindent
- where the right-hand side is not even typable! This problem can be remedied in the
- existing quotient packages by introducing an intermediate step and reasoning
- about flattening of lists of finite sets. However, this remedy is rather
- cumbersome and inelegant in light of our work, which can deal with such
- definitions directly. The solution is that we need to build aggregate
- representation and abstraction functions, which in case of @{text "\<Union>"}
- generate the %%%following
- definition
-
- \begin{isabelle}\ \ \ \ \ %%%
- @{text "\<Union> S \<equiv> Abs_fset (flat ((map_list Rep_fset \<circ> Rep_fset) S))"}
- \end{isabelle}
-
- \noindent
- where @{term map_list} is the usual mapping function for lists. In this paper we
- will present a formal definition of our aggregate abstraction and
- representation functions (this definition was omitted in \cite{Homeier05}).
- They generate definitions, like the one above for @{text "\<Union>"},
- according to the type of the raw constant and the type
- of the quotient constant. This means we also have to extend the notions
- of \emph{aggregate equivalence relation}, \emph{respectfulness} and \emph{preservation}
- from Homeier \cite{Homeier05}.
-
- {\bf EXAMPLE BY HUFFMAN @{thm map_concat_fset}}
-
-%%%TODO Update the contents.
-
- In addition we are able to clearly specify what is involved
- in the lifting process (this was only hinted at in \cite{Homeier05} and
- implemented as a ``rough recipe'' in ML-code). A pleasing side-result
- is that our procedure for lifting theorems is completely deterministic
- following the structure of the theorem being lifted and the theorem
- on the quotient level. {\it Space constraints, unfortunately, allow us to only
- sketch this part of our work in Section 5 and we defer the reader to a longer
- version for the details.} However, we will give in Section 3 and 4 all
- definitions that specify the input and output data of our three-step
- lifting procedure. Appendix A gives an example how our quotient
- package works in practise.
-*}
-
-section {* Preliminaries and General Quotients\label{sec:prelims} *}
-
-text {*
- \noindent
- We will give in this section a crude overview of HOL and describe the main
- 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 always infer the type of
- a term and its subterms without any additional information). The grammars
- for types and terms are
-
- \begin{isabelle}\ \ \ \ \ %%%
- \begin{tabular}{@ {}c@ {\hspace{10mm}}c@ {}}
- @{text "\<sigma>, \<tau> ::= \<alpha> | (\<sigma>,\<dots>, \<sigma>) \<kappa>"} &
- @{text "t, s ::= x\<^isup>\<sigma> | c\<^isup>\<sigma> | t t | \<lambda>x\<^isup>\<sigma>. t"}\\
- \end{tabular}
- \end{isabelle}
-
- \noindent
- with types being either type variables or type constructors and terms
- being variables, constants, applications or abstractions.
- 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 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, a primitive constant is equality, with type @{text "= :: \<sigma> \<Rightarrow> \<sigma> \<Rightarrow>
- bool"}, and the identity function with type @{text "id :: \<sigma> \<Rightarrow> \<sigma>"} is
- 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 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's, our work relies on map-functions defined for every type
- constructor taking some arguments, for example @{text map_list} for lists. Homeier
- describes in \cite{Homeier05} map-functions for products, sums, options and
- also the following map for function types
-
- \begin{isabelle}\ \ \ \ \ %%%
- @{thm map_fun_def[THEN eq_reflection]}
- \end{isabelle}
-
- \noindent
- Using this map-function, we can give the following, equivalent, but more
- uniform definition for @{text add} shown in \eqref{adddef}:
-
- \begin{isabelle}\ \ \ \ \ %%%
- @{text "add \<equiv> (Rep_int \<singlearr> Rep_int \<singlearr> Abs_int) add_pair"}
- \end{isabelle}
-
- \noindent
- Using extensionality and unfolding the definition of @{text "\<singlearr>"},
- we can get back to \eqref{adddef}.
- In what follows we shall use the convention to write @{text "map_\<kappa>"} for a map-function
- of the type-constructor @{text \<kappa>}.
- %% a general type for map all types is difficult to give (algebraic types are
- %% easy, but for example the function type is not algebraic
- %For a type @{text \<kappa>} with arguments @{text "\<alpha>\<^isub>1\<^isub>\<dots>\<^isub>n"} the
- %type of the function @{text "map_\<kappa>"} has to be @{text "\<alpha>\<^isub>1\<Rightarrow>\<dots>\<Rightarrow>\<alpha>\<^isub>n\<Rightarrow>\<alpha>\<^isub>1\<dots>\<alpha>\<^isub>n \<kappa>"}.
- %For example @{text "map_list"}
- %has to have the type @{text "\<alpha>\<Rightarrow>\<alpha> list"}.
- In our implementation we maintain
- a database of these 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
-
- \begin{isabelle}\ \ \ \ \ %%%
- @{text "(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"}
- \end{isabelle}
-
- \noindent
- Homeier gives also the following operator for defining equivalence
- relations over function types
- %
- \begin{isabelle}\ \ \ \ \ %%%
- @{thm fun_rel_def[of "R\<^isub>1" "R\<^isub>2", THEN eq_reflection]}
- \hfill\numbered{relfun}
- \end{isabelle}
-
- \noindent
- In the context of quotients, the following two notions from \cite{Homeier05}
- are needed later on.
-
- \begin{definition}[Respects]\label{def:respects}
- An element @{text "x"} respects a relation @{text "R"} provided @{text "R x x"}.
- \end{definition}
-
- \begin{definition}[Bounded $\forall$ and $\lambda$]\label{def:babs}
- @{text "\<forall>x \<in> S. P x"} holds if for all @{text x}, @{text "x \<in> S"} implies @{text "P x"};
- and @{text "(\<lambda>x \<in> S. f x) x = f x"} provided @{text "x \<in> S"}.
- \end{definition}
-
- 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"}
- holds if and only if
- \begin{isabelle}\ \ \ \ \ %%%%
- \begin{tabular}{rl}
- (i) & \begin{isa}@{thm (rhs1) Quotient_def[of "R"]}\end{isa}\\
- (ii) & \begin{isa}@{thm (rhs2) Quotient_def[of "R"]}\end{isa}\\
- (iii) & \begin{isa}@{thm (rhs3) Quotient_def[of "R"]}\end{isa}\\
- \end{tabular}
- \end{isabelle}
- \end{definition}
-
- \noindent
- The value of this definition lies in the fact that validity of @{term "Quotient R Abs Rep"} can
- often be proved in terms of the validity of @{term "Quot"} 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}\label{funquot}
- \begin{isa}
- @{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{isa}
- \end{proposition}
-
- \noindent
- As a result, Homeier is able to build an automatic prover that can nearly
- always discharge a proof obligation involving @{text "Quot"}. Our quotient
- package makes heavy
- use of this part of Homeier's work including an extension
- for dealing with \emph{conjugations} of equivalence relations\footnote{That are
- symmetric by definition.} defined as follows:
-
-%%% FIXME Referee 2 claims that composition-of-relations means OO, and this is also
-%%% what wikipedia says. Any idea for a different name? Conjugation of Relations?
-
- \begin{definition}%%[Composition of Relations]
- @{abbrev "rel_conj R\<^isub>1 R\<^isub>2"} where @{text "\<circ>\<circ>"} is the predicate
- composition defined by
- @{thm (concl) pred_compI[of "R\<^isub>1" "x" "y" "R\<^isub>2" "z"]}
- holds if and only if there exists a @{text y} such that @{thm (prem 1) pred_compI[of "R\<^isub>1" "x" "y" "R\<^isub>2" "z"]} and
- @{thm (prem 2) pred_compI[of "R\<^isub>1" "x" "y" "R\<^isub>2" "z"]}.
- \end{definition}
-
- \noindent
- Unfortunately a general quotient theorem for @{text "\<circ>\<circ>\<circ>"}, analogous to the one
- for @{text "\<singlearr>"} given in Proposition \ref{funquot}, would not be true
- in general. It cannot even be stated inside HOL, because of restrictions on types.
- However, we can prove specific instances of a
- quotient theorem for composing particular quotient relations.
- For example, to lift theorems involving @{term flat} the quotient theorem for
- composing @{text "\<approx>\<^bsub>list\<^esub>"} will be necessary: given @{term "Quotient R Abs Rep"}
- with @{text R} being an equivalence relation, then
-
- \begin{isabelle}\ \ \ \ \ %%%
- \begin{tabular}{r@ {\hspace{1mm}}l}
- @{text "Quot"} & @{text "(rel_list R \<circ>\<circ>\<circ> \<approx>\<^bsub>list\<^esub>)"}\\
- & @{text "(Abs_fset \<circ> map_list Abs)"} @{text "(map_list Rep \<circ> Rep_fset)"}\\
- \end{tabular}
- \end{isabelle}
-*}
-
-section {* Quotient Types and Quotient Definitions\label{sec:type} *}
-
-text {*
- \noindent
- 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 @{text "\<sigma> \<Rightarrow> \<sigma> \<Rightarrow> bool"}. The user-visible part of
- the quotient type declaration is therefore
-
- \begin{isabelle}\ \ \ \ \ %%%
- \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. The @{text "\<alpha>s"}
- indicate the arity of the new type and the type-variables of @{text "\<sigma>"} can only
- be contained in @{text "\<alpha>s"}. Two concrete
- examples are
-
-
- \begin{isabelle}\ \ \ \ \ %%%
- \begin{tabular}{@ {}l}
- \isacommand{quotient\_type}~~@{text "int = nat \<times> nat / \<approx>\<^bsub>nat \<times> nat\<^esub>"}\\
- \isacommand{quotient\_type}~~@{text "\<alpha> fset = \<alpha> list / \<approx>\<^bsub>list\<^esub>"}
- \end{tabular}
- \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 in \eqref{natpairequiv} and
- \eqref{listequiv}, respectively (the proofs about being equivalence
- relations are omitted). Given this data, we define for declarations shown in
- \eqref{typedecl} the quotient types internally 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 constraint 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 then provide us with the following
- 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
- 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)"}
- \end{isabelle}
-
- \noindent
- on the expense of having to use Hilbert's choice operator @{text "\<epsilon>"} in the
- definition of @{text "Rep_\<kappa>\<^isub>q"}. These derived notions relate the
- 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 holds for every quotient type
- (for the proof see \cite{Homeier05}).
-
- \begin{proposition}
- \begin{isa}@{term "Quotient R Abs_\<kappa>\<^isub>q Rep_\<kappa>\<^isub>q"}.\end{isa}
- \end{proposition}
-
- 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 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 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"}~~%
- \isacommand{is}~~@{text "flat"}
- \end{tabular}
- \end{isabelle}
-
- \noindent
- The first one declares zero for integers and the second the operator for
- building unions of finite sets (@{text "flat"} having the type
- @{text "(\<alpha> list) list \<Rightarrow> \<alpha> list"}).
-
- From such declarations given by the user, the quotient package needs to derive proper
- definitions using @{text "Abs"} and @{text "Rep"}. The data we rely on is the given quotient type
- @{text "\<tau>"} and the raw type @{text "\<sigma>"}. They allow us to define \emph{aggregate
- abstraction} and \emph{representation functions} using the functions @{text "ABS (\<sigma>,
- \<tau>)"} and @{text "REP (\<sigma>, \<tau>)"} whose clauses we shall give below. The idea behind
- these two functions is to simultaneously 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. On the ``way'' down,
- however we might have to use map-functions to let @{text Abs} and @{text Rep} act
- over the appropriate types. In what follows 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>n, \<tau>\<^isub>n)"}; similarly
- for @{text REP}.
- %
- \begin{center}
- \hfill
- \begin{tabular}{@ {\hspace{2mm}}l@ {}}
- \multicolumn{1}{@ {}l}{equal types:}\\
- @{text "ABS (\<sigma>, \<sigma>)"} $\dn$ @{text "id :: \<sigma> \<Rightarrow> \<sigma>"}\hspace{5mm}%\\
- @{text "REP (\<sigma>, \<sigma>)"} $\dn$ @{text "id :: \<sigma> \<Rightarrow> \<sigma>"}\smallskip\\
- \multicolumn{1}{@ {}l}{function types:}\\
- @{text "ABS (\<sigma>\<^isub>1 \<Rightarrow> \<sigma>\<^isub>2, \<tau>\<^isub>1 \<Rightarrow> \<tau>\<^isub>2)"} $\dn$ @{text "REP (\<sigma>\<^isub>1, \<tau>\<^isub>1) \<singlearr> ABS (\<sigma>\<^isub>2, \<tau>\<^isub>2)"}\\
- @{text "REP (\<sigma>\<^isub>1 \<Rightarrow> \<sigma>\<^isub>2, \<tau>\<^isub>1 \<Rightarrow> \<tau>\<^isub>2)"} $\dn$ @{text "ABS (\<sigma>\<^isub>1, \<tau>\<^isub>1) \<singlearr> REP (\<sigma>\<^isub>2, \<tau>\<^isub>2)"}\smallskip\\
- \multicolumn{1}{@ {}l}{equal type constructors:}\\
- @{text "ABS (\<sigma>s \<kappa>, \<tau>s \<kappa>)"} $\dn$ @{text "map_\<kappa> (ABS (\<sigma>s, \<tau>s))"}\\
- @{text "REP (\<sigma>s \<kappa>, \<tau>s \<kappa>)"} $\dn$ @{text "map_\<kappa> (REP (\<sigma>s, \<tau>s))"}\smallskip\\
- \multicolumn{1}{@ {}l}{unequal type constructors:}\\
- @{text "ABS (\<sigma>s \<kappa>, \<tau>s \<kappa>\<^isub>q)"} $\dn$ @{text "Abs_\<kappa>\<^isub>q \<circ> (MAP(\<rho>s \<kappa>) (ABS (\<sigma>s', \<tau>s)))"}\\
- @{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
- In the last two clauses are subtle. We rely in them on the fact 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"}). This data is given by declarations shown in \eqref{typedecl}.
- The quotient construction ensures that the type variables in @{text
- "\<rho>s \<kappa>"} must be among the @{text "\<alpha>s"}. The @{text "\<sigma>s'"} are given by the
- substitutions for the @{text "\<alpha>s"} when matching @{text "\<sigma>s \<kappa>"} against
- @{text "\<rho>s \<kappa>"}. This calculation determines what are the types in place
- of the type variables @{text "\<alpha>s"} in the instance of
- quotient type @{text "\<alpha>s \<kappa>\<^isub>q"}---namely @{text "\<tau>s"}, and the corresponding
- types in place of the @{text "\<alpha>s"} in the raw type @{text "\<rho>s \<kappa>"}---namely @{text "\<sigma>s'"}. The
- function @{text "MAP"} calculates an \emph{aggregate map-function} for a raw
- type as follows:
- %
- \begin{center}
- \begin{tabular}{r@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
- @{text "MAP' (\<alpha>)"} & $\dn$ & @{text "a\<^sup>\<alpha>"}\\
- @{text "MAP' (\<kappa>)"} & $\dn$ & @{text "id :: \<kappa> \<Rightarrow> \<kappa>"}\\
- @{text "MAP' (\<sigma>s \<kappa>)"} & $\dn$ & @{text "map_\<kappa> (MAP'(\<sigma>s))"}\smallskip\\
- @{text "MAP (\<sigma>)"} & $\dn$ & @{text "\<lambda>as. MAP'(\<sigma>)"}
- \end{tabular}
- \end{center}
- %
- \noindent
- In this definition we rely on the fact that in the first clause we can interpret type-variables @{text \<alpha>} as
- term variables @{text a}. In the last clause we build an abstraction over all
- term-variables of the map-function generated by the auxiliary function
- @{text "MAP'"}.
- The need for aggregate map-functions can be seen in cases where we build quotients,
- say @{text "(\<alpha>, \<beta>) \<kappa>\<^isub>q"}, out of compound raw types, say @{text "(\<alpha> list) \<times> \<beta>"}.
- In this case @{text MAP} generates the
- aggregate map-function:
-
-%%% FIXME: Reviewer 2 asks: last two lines defining ABS and REP for
-%%% unequal type constructors: How are the $\varrho$s defined? The
-%%% following paragraph mentions them, but this paragraph is unclear,
-%%% since it then mentions $\alpha$s, which do not seem to be defined
-%%% either. As a result, I do not understand the first two sentences
-%%% in this paragraph. I can imagine roughly what the following
-%%% sentence `The $\sigma$s' are given by the matchers for the
-%%% $\alpha$s$ when matching $\varrho$s $\kappa$ against $\sigma$s
-%%% $\kappa$.' means, but also think that it is too vague.
-
- \begin{isabelle}\ \ \ \ \ %%%
- @{text "\<lambda>a b. map_prod (map_list a) b"}
- \end{isabelle}
-
- \noindent
- which is essential in order to define the corresponding 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 these types into @{text ABS} gives us (after some @{text "\<beta>"}-simplifications)
- the abstraction function
-
- \begin{isabelle}\ \ \ %%%
- \begin{tabular}{l}
- @{text "(map_list (map_list id \<circ> Rep_fset) \<circ> Rep_fset) \<singlearr>"}\\
- \mbox{}\hspace{4.5cm}@{text " Abs_fset \<circ> map_list id"}
- \end{tabular}
- \end{isabelle}
-
- \noindent
- In our implementation we further
- simplify this function by rewriting with the usual laws about @{text
- "map"}s and @{text "id"}, for example @{term "map_list id = id"} and @{text "f \<circ> id =
- id \<circ> f = f"}. This gives us the simpler abstraction function
-
- \begin{isabelle}\ \ \ \ \ %%%
- @{text "(map_list Rep_fset \<circ> Rep_fset) \<singlearr> Abs_fset"}
- \end{isabelle}
-
- \noindent
- which we can use for defining @{term "fconcat"} as follows
-
- \begin{isabelle}\ \ \ \ \ %%%
- @{text "\<Union> \<equiv> ((map_list Rep_fset \<circ> Rep_fset) \<singlearr> Abs_fset) flat"}
- \end{isabelle}
-
- \noindent
- Note that by using the operator @{text "\<singlearr>"} and special clauses
- for function types in \eqref{ABSREP}, we do not have to
- distinguish between arguments and results, but can deal with them uniformly.
- Consequently, all definitions in the quotient package
- are of the general form
-
- \begin{isabelle}\ \ \ \ \ %%%
- \mbox{@{text "c \<equiv> ABS (\<sigma>, \<tau>) t"}}
- \end{isabelle}
-
- \noindent
- where @{text \<sigma>} is the type of the definiens @{text "t"} and @{text "\<tau>"} the
- type of the defined quotient constant @{text "c"}. This data can be easily
- generated from the declaration given by the user.
- To increase the confidence in this way of making definitions, we can prove
- that the terms involved are all typable.
-
- \begin{lemma}
- If @{text "ABS (\<sigma>, \<tau>)"} returns some abstraction function @{text "Abs"}
- and @{text "REP (\<sigma>, \<tau>)"} some representation function @{text "Rep"},
- then @{text "Abs"} is of type @{text "\<sigma> \<Rightarrow> \<tau>"} and @{text "Rep"} of type
- @{text "\<tau> \<Rightarrow> \<sigma>"}.
- \end{lemma}
-
- \begin{proof}
- By mutual induction and analysing the definitions of @{text "ABS"} and @{text "REP"}.
- 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
- interesting case is the one with unequal type constructors. Since we know
- the quotient is between @{text "\<alpha>s \<kappa>\<^isub>q"} and @{text "\<rho>s \<kappa>"}, we have
- that @{text "Abs_\<kappa>\<^isub>q"} is of type @{text "\<rho>s \<kappa> \<Rightarrow> \<alpha>s
- \<kappa>\<^isub>q"}. This type can be more specialised to @{text "\<rho>s[\<tau>s] \<kappa> \<Rightarrow> \<tau>s
- \<kappa>\<^isub>q"} where the type variables @{text "\<alpha>s"} are instantiated with the
- @{text "\<tau>s"}. The complete type can be calculated by observing that @{text
- "MAP (\<rho>s \<kappa>)"}, after applying the functions @{text "ABS (\<sigma>s', \<tau>s)"} to it,
- returns a term of type @{text "\<rho>s[\<sigma>s'] \<kappa> \<Rightarrow> \<rho>s[\<tau>s] \<kappa>"}. This type is
- equivalent to @{text "\<sigma>s \<kappa> \<Rightarrow> \<rho>s[\<tau>s] \<kappa>"}, which we just have to compose with
- @{text "\<rho>s[\<tau>s] \<kappa> \<Rightarrow> \<tau>s \<kappa>\<^isub>q"} according to the type of @{text "\<circ>"}.\qed
- \end{proof}
-*}
-
-section {* Respectfulness and Preservation \label{sec:resp} *}
-
-text {*
- \noindent
- The main point of the quotient package is to automatically ``lift'' theorems
- involving constants over the raw type to theorems involving constants over
- the quotient type. Before we can describe this lifting process, we need to impose
- two restrictions in form of proof obligations that arise during the
- lifting. The reason is that even if definitions for all raw constants
- can be given, \emph{not} all theorems can be lifted to the quotient type. Most
- notable is the bound variable function, that is the constant @{text bn},
- defined
- for raw lambda-terms as follows
-
- \begin{isabelle}
- \begin{center}
- @{text "bn (x) \<equiv> \<emptyset>"}\hspace{4mm}
- @{text "bn (t\<^isub>1 t\<^isub>2) \<equiv> bn (t\<^isub>1) \<union> bn (t\<^isub>2)"}\smallskip\\
- @{text "bn (\<lambda>x. t) \<equiv> {x} \<union> bn (t)"}
- \end{center}
- \end{isabelle}
-
- \noindent
- We can generate a definition for this constant using @{text ABS} and @{text REP}.
- But this constant does \emph{not} respect @{text "\<alpha>"}-equivalence and
- 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{respectfulness} and \emph{preservation}. We have
- to slightly extend Homeier's definitions in order to deal with quotient
- compositions.
-
-%%% FIXME: Reviewer 3 asks why are the definitions that follow enough to deal
-%%% with quotient composition.
-
- To formally define what respectfulness is, we have to first define
- the notion of \emph{aggregate equivalence relations} using the function @{text "REL(\<sigma>, \<tau>)"}
- The idea behind this function is to simultaneously descend into the raw types
- @{text \<sigma>} and quotient types @{text \<tau>}, and generate the appropriate
- quotient equivalence relations in places where the types differ and equalities
- elsewhere.
-
- \begin{center}
- \hfill
- \begin{tabular}{l}
- \multicolumn{1}{@ {}l}{equal types:}
- @{text "REL (\<sigma>, \<sigma>)"} $\dn$ @{text "= :: \<sigma> \<Rightarrow> \<sigma> \<Rightarrow> bool"}\smallskip\\
- \multicolumn{1}{@ {}l}{equal type constructors:}\\
- @{text "REL (\<sigma>s \<kappa>, \<tau>s \<kappa>)"} $\dn$ @{text "rel_\<kappa> (REL (\<sigma>s, \<tau>s))"}\smallskip\\
- \multicolumn{1}{@ {}l}{unequal type constructors:}\\
- @{text "REL (\<sigma>s \<kappa>, \<tau>s \<kappa>\<^isub>q)"} $\dn$ @{text "rel_\<kappa>\<^isub>q (REL (\<sigma>s', \<tau>s))"}\\
- \end{tabular}\hfill\numbered{REL}
- \end{center}
-
- \noindent
- The @{text "\<sigma>s'"} in the last clause are calculated as in \eqref{ABSREP}:
- again we know that type @{text "\<alpha>s \<kappa>\<^isub>q"} is the quotient of the raw type
- @{text "\<rho>s \<kappa>"}. The @{text "\<sigma>s'"} are the substitutions for @{text "\<alpha>s"} obtained by matching
- @{text "\<rho>s \<kappa>"} and @{text "\<sigma>s \<kappa>"}.
-
- Let us return to the lifting procedure of theorems. Assume we have a theorem
- that contains the raw constant @{text "c\<^isub>r :: \<sigma>"} and which we want to
- lift to a theorem where @{text "c\<^isub>r"} is replaced by the corresponding
- constant @{text "c\<^isub>q :: \<tau>"} defined over a quotient type. In this situation
- we generate the following proof obligation
-
- \begin{isabelle}\ \ \ \ \ %%%
- @{text "REL (\<sigma>, \<tau>) c\<^isub>r c\<^isub>r"}.
- \end{isabelle}
-
- \noindent
- Homeier calls these proof obligations \emph{respectfulness
- theorems}. However, unlike his quotient package, we might have several
- respectfulness theorems for one constant---he has at most one.
- The reason is that because of our quotient compositions, the types
- @{text \<sigma>} and @{text \<tau>} are not completely determined by @{text "c\<^bsub>r\<^esub>"}.
- And for every instantiation of the types, a corresponding
- respectfulness theorem is necessary.
-
- Before lifting a theorem, we require the user to discharge
- respectfulness proof obligations. In case of @{text bn}
- this obligation is %%as follows
-
- \begin{isabelle}\ \ \ \ \ %%%
- @{text "(\<approx>\<^isub>\<alpha> \<doublearr> =) bn bn"}
- \end{isabelle}
-
- \noindent
- and the point is that the user cannot discharge it: because it is not true. To see this,
- we can just unfold the definition of @{text "\<doublearr>"} \eqref{relfun}
- using extensionality to obtain the false statement
-
- \begin{isabelle}\ \ \ \ \ %%%
- @{text "\<forall>t\<^isub>1 t\<^isub>2. if t\<^isub>1 \<approx>\<^isub>\<alpha> t\<^isub>2 then bn(t\<^isub>1) = bn(t\<^isub>2)"}
- \end{isabelle}
-
- \noindent
- In contrast, lifting a theorem about @{text "append"} to a theorem describing
- the union of finite sets will mean to discharge the proof obligation
-
- \begin{isabelle}\ \ \ \ \ %%%
- @{text "(\<approx>\<^bsub>list\<^esub> \<doublearr> \<approx>\<^bsub>list\<^esub> \<doublearr> \<approx>\<^bsub>list\<^esub>) append append"}
- \end{isabelle}
-
- \noindent
- To do so, we have to establish
-
- \begin{isabelle}\ \ \ \ \ %%%
- if @{text "xs \<approx>\<^bsub>list\<^esub> ys"} and @{text "us \<approx>\<^bsub>list\<^esub> vs"}
- then @{text "xs @ us \<approx>\<^bsub>list\<^esub> ys @ vs"}
- \end{isabelle}
-
- \noindent
- which is straightforward given the definition shown in \eqref{listequiv}.
-
- The second restriction we have to impose arises from non-lifted polymorphic
- constants, which are instantiated to a type being quotient. For example,
- take the @{term "cons"}-constructor to add a pair of natural numbers to a
- list, whereby we assume the pair of natural numbers turns into an integer in
- the quotient construction. The point is that we still want to use @{text
- cons} for adding integers to lists---just with a different type. To be able
- to lift such theorems, we need a \emph{preservation property} for @{text
- cons}. Assuming we have a polymorphic raw constant @{text "c\<^isub>r :: \<sigma>"}
- and a corresponding quotient constant @{text "c\<^isub>q :: \<tau>"}, then a
- preservation property is as follows
-
-%%% FIXME: Reviewer 2 asks: You say what a preservation theorem is,
-%%% but not which preservation theorems you assume. Do you generate a
-%%% proof obligation for a preservation theorem for each raw constant
-%%% and its corresponding lifted constant?
-
-%%% Cezary: I think this would be a nice thing to do but we have not
-%%% done it, the theorems need to be 'guessed' from the remaining obligations
-
- \begin{isabelle}\ \ \ \ \ %%%
- @{text "Quot R\<^bsub>\<alpha>s\<^esub> Abs\<^bsub>\<alpha>s\<^esub> Rep\<^bsub>\<alpha>s\<^esub> implies ABS (\<sigma>, \<tau>) c\<^isub>r = c\<^isub>r"}
- \end{isabelle}
-
- \noindent
- where the @{text "\<alpha>s"} stand for the type variables in the type of @{text "c\<^isub>r"}.
- In case of @{text cons} (which has type @{text "\<alpha> \<Rightarrow> \<alpha> list \<Rightarrow> \<alpha> list"}) we have
-
- \begin{isabelle}\ \ \ \ \ %%%
- @{text "(Rep \<singlearr> map_list Rep \<singlearr> map_list Abs) cons = cons"}
- \end{isabelle}
-
- \noindent
- under the assumption @{term "Quotient R Abs Rep"}. The point is that if we have
- an instance of @{text cons} where the type variable @{text \<alpha>} is instantiated
- with @{text "nat \<times> nat"} and we also quotient this type to yield integers,
- then we need to show this preservation property.
-
- %%%@ {thm [display, indent=10] Cons_prs2}
-
- %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
- %quotients composed with the usual function composition.
- %The @ {term "Rep"} and @ {term "Abs"} functions that we obtain agree
- %with the definition of aggregate Abs/Rep functions and the
- %relation is the same as the one given by aggregate relations.
- %This becomes especially interesting
- %when we compose the quotient with itself, as there is no simple
- %intermediate step.
- %
- %Lets take again the example of @ {term flat}. To be able to lift
- %theorems that talk about it we provide the composition quotient
- %theorem which allows quotienting inside the container:
- %
- %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_list Abs) (map_list Rep o rep_fset)"}
- %%%
- %%%\noindent
- %%%this theorem will then instantiate the quotients needed in the
- %%%injection and cleaning proofs allowing the lifting procedure to
- %%%proceed in an unchanged way.
-*}
-
-section {* Lifting of Theorems\label{sec:lift} *}
-
-text {*
-
-%%% FIXME Reviewer 3 asks: Section 5 shows the technicalities of
-%%% lifting theorems. But there is no clarification about the
-%%% correctness. A reader would also be interested in seeing some
-%%% discussions about the generality and limitation of the approach
-%%% proposed there
-
-%%% TODO: This introduction is same as the introduction to the previous section.
-
- \noindent
- The main benefit of a quotient package is to lift automatically theorems over raw
- types to theorems over quotient types. We will perform this lifting in
- three phases, called \emph{regularization},
- \emph{injection} and \emph{cleaning} according to procedures in Homeier's ML-code.
- Space restrictions, unfortunately, prevent us from giving anything but a sketch of these three
- phases. However, we will precisely define the input and output data of these phases
- (this was omitted in \cite{Homeier05}).
-
- The purpose of regularization is to change the quantifiers and abstractions
- in a ``raw'' theorem to quantifiers over variables that respect their respective relations
- (Definition \ref{def:respects} states what respects means). The purpose of injection is to add @{term Rep}
- and @{term Abs} of appropriate types in front of constants and variables
- of the raw type so that they can be replaced by the corresponding constants from the
- quotient type. The purpose of cleaning is to bring the theorem derived in the
- first two phases into the form the user has specified. Abstractly, our
- package establishes the following three proof steps:
-
-%%% FIXME: Reviewer 1 complains that the reader needs to guess the
-%%% meaning of reg_thm and inj_thm, as well as the arguments of REG
-%%% which are given above. I wouldn't change it.
-
- \begin{center}
- \begin{tabular}{l@ {\hspace{4mm}}l}
- 1.) Regularization & @{text "raw_thm \<longrightarrow> reg_thm"}\\
- 2.) Injection & @{text "reg_thm \<longleftrightarrow> inj_thm"}\\
- 3.) Cleaning & @{text "inj_thm \<longleftrightarrow> quot_thm"}\\
- \end{tabular}
- \end{center}
-
- \noindent
- which means, stringed together, the raw theorem implies the quotient theorem.
- The core of the quotient package requires both the @{text "raw_thm"} (as a
- theorem) and the \emph{term} of the @{text "quot_thm"}. This lets the user
- have a finer control over which parts of a raw theorem should be lifted.
- We also provide more automated modes where either the @{text "quot_thm"}
- is guessed from the form of @{text "raw_thm"} or the @{text "raw_thm"} is
- guessed from the current goal and these are described in Section \ref{sec:descending}.
-
- The second and third proof step performed in package will always succeed if the appropriate
- respectfulness and preservation theorems are given. In contrast, the first
- proof step can fail: a theorem given by the user does not always
- imply a regularized version and a stronger one needs to be proved. An example
- for this kind of failure is the simple statement for integers @{text "0 \<noteq> 1"}.
- One might hope that it can be proved by lifting @{text "(0, 0) \<noteq> (1, 0)"},
- but this raw theorem only shows that two particular elements in the
- equivalence classes are not equal. In order to obtain @{text "0 \<noteq> 1"}, a
- more general statement stipulating that the equivalence classes are not
- equal is necessary. This kind of failure is beyond the scope where the
- quotient package can help: the user has to provide a raw theorem that
- can be regularized automatically, or has to provide an explicit proof
- for the first proof step. Homeier gives more details about this issue
- in the long version of \cite{Homeier05}.
-
- In the following we will first define the statement of the
- regularized theorem based on @{text "raw_thm"} and
- @{text "quot_thm"}. Then we define the statement of the injected theorem, based
- on @{text "reg_thm"} and @{text "quot_thm"}. We then show the three proof steps,
- which can all be performed independently from each other.
-
- We first define the function @{text REG}, which takes the terms of the
- @{text "raw_thm"} and @{text "quot_thm"} as input and returns
- @{text "reg_thm"}. The idea
- behind this function is that it replaces quantifiers and
- abstractions involving raw types by bounded ones, and equalities
- involving raw types by appropriate aggregate
- equivalence relations. It is defined by simultaneous recursion on
- the structure of the terms of @{text "raw_thm"} and @{text "quot_thm"} as follows:
- %
- \begin{center}
- \begin{tabular}{@ {}l@ {}}
- \multicolumn{1}{@ {}l@ {}}{abstractions:}\\%%\smallskip\\
- @{text "REG (\<lambda>x\<^sup>\<sigma>. t, \<lambda>x\<^sup>\<tau>. s)"} $\dn$
- $\begin{cases}
- @{text "\<lambda>x\<^sup>\<sigma>. REG (t, s)"} \quad\mbox{provided @{text "\<sigma> = \<tau>"}}\\
- @{text "\<lambda>x\<^sup>\<sigma> \<in> Resp (REL (\<sigma>, \<tau>)). REG (t, s)"}
- \end{cases}$\\%%\smallskip\\
- \multicolumn{1}{@ {}l@ {}}{universal quantifiers:}\\
- @{text "REG (\<forall>x\<^sup>\<sigma>. t, \<forall>x\<^sup>\<tau>. s)"} $\dn$
- $\begin{cases}
- @{text "\<forall>x\<^sup>\<sigma>. REG (t, s)"} \quad\mbox{provided @{text "\<sigma> = \<tau>"}}\\
- @{text "\<forall>x\<^sup>\<sigma> \<in> Resp (REL (\<sigma>, \<tau>)). REG (t, s)"}
- \end{cases}$\\%%\smallskip\\
- \multicolumn{1}{@ {}l@ {}}{equality: \hspace{3mm}%%}\smallskip\\
- %% REL of two equal types is the equality so we do not need a separate case
- @{text "REG (=\<^bsup>\<sigma>\<Rightarrow>\<sigma>\<Rightarrow>bool\<^esup>, =\<^bsup>\<tau>\<Rightarrow>\<tau>\<Rightarrow>bool\<^esup>)"} $\dn$ @{text "REL (\<sigma>, \<tau>)"}}\smallskip\\
- \multicolumn{1}{@ {}l@ {}}{applications, variables and constants:}\\
- @{text "REG (t\<^isub>1 t\<^isub>2, s\<^isub>1 s\<^isub>2)"} $\dn$ @{text "REG (t\<^isub>1, s\<^isub>1) REG (t\<^isub>2, s\<^isub>2)"}\\
- @{text "REG (x\<^isub>1, x\<^isub>2)"} $\dn$ @{text "x\<^isub>1"}\\
- @{text "REG (c\<^isub>1, c\<^isub>2)"} $\dn$ @{text "c\<^isub>1"}\\
- \end{tabular}
- \end{center}
- %
- \noindent
- In the above definition we omitted the cases for existential quantifiers
- and unique existential quantifiers, as they are very similar to the cases
- for the universal quantifier.
-
- Next we define the function @{text INJ} which takes as argument
- @{text "reg_thm"} and @{text "quot_thm"} (both as
- terms) and returns @{text "inj_thm"}:
-
- \begin{center}
- \begin{tabular}{l}
- \multicolumn{1}{@ {}l}{abstractions:}\\
- @{text "INJ (\<lambda>x. t :: \<sigma>, \<lambda>x. s :: \<tau>) "} $\dn$\\
- \hspace{18mm}$\begin{cases}
- @{text "\<lambda>x. INJ (t, s)"} \quad\mbox{provided @{text "\<sigma> = \<tau>"}}\\
- @{text "REP (\<sigma>, \<tau>) (ABS (\<sigma>, \<tau>) (\<lambda>x. INJ (t, s)))"}
- \end{cases}$\smallskip\\
- @{text "INJ (\<lambda>x \<in> R. t :: \<sigma>, \<lambda>x. s :: \<tau>) "} $\dn$\\
- \hspace{18mm}@{text "REP (\<sigma>, \<tau>) (ABS (\<sigma>, \<tau>) (\<lambda>x \<in> R. INJ (t, s)))"}\smallskip\\
- \multicolumn{1}{@ {}l}{universal quantifiers:}\\
- @{text "INJ (\<forall> t, \<forall> s) "} $\dn$ @{text "\<forall> INJ (t, s)"}\\
- @{text "INJ (\<forall> t \<in> R, \<forall> s) "} $\dn$ @{text "\<forall> INJ (t, s) \<in> R"}\smallskip\\
- \multicolumn{1}{@ {}l}{applications, variables and constants:}\smallskip\\
- @{text "INJ (t\<^isub>1 t\<^isub>2, s\<^isub>1 s\<^isub>2) "} $\dn$ @{text " INJ (t\<^isub>1, s\<^isub>1) INJ (t\<^isub>2, s\<^isub>2)"}\\
- @{text "INJ (x\<^isub>1\<^sup>\<sigma>, x\<^isub>2\<^sup>\<tau>) "} $\dn$
- $\begin{cases}
- @{text "x\<^isub>1"} \quad\mbox{provided @{text "\<sigma> = \<tau>"}}\\
- @{text "REP (\<sigma>, \<tau>) (ABS (\<sigma>, \<tau>) x\<^isub>1)"}\\
- \end{cases}$\\
- @{text "INJ (c\<^isub>1\<^sup>\<sigma>, c\<^isub>2\<^sup>\<tau>) "} $\dn$
- $\begin{cases}
- @{text "c\<^isub>1"} \quad\mbox{provided @{text "\<sigma> = \<tau>"}}\\
- @{text "REP (\<sigma>, \<tau>) (ABS (\<sigma>, \<tau>) c\<^isub>1)"}\\
- \end{cases}$\\
- \end{tabular}
- \end{center}
-
- \noindent
- In this definition we again omitted the cases for existential and unique existential
- quantifiers.
-
-%%% FIXME: Reviewer2 citing following sentence: You mention earlier
-%%% that this implication may fail to be true. Does that meant that
-%%% the `first proof step' is a heuristic that proves the implication
-%%% raw_thm \implies reg_thm in some instances, but fails in others?
-%%% You should clarify under which circumstances the implication is
-%%% being proved here.
-%%% Cezary: It would be nice to cite Homeiers discussions in the
-%%% Quotient Package manual from HOL (the longer paper), do you agree?
-
- In the first phase, establishing @{text "raw_thm \<longrightarrow> reg_thm"}, we always
- start with an implication. Isabelle provides \emph{mono} rules that can split up
- the implications into simpler implicational subgoals. This succeeds for every
- monotone connective, except in places where the function @{text REG} replaced,
- for instance, a quantifier by a bounded quantifier. To decompose them, we have
- to prove that the relations involved are aggregate equivalence relations.
-
-
- %In this case we have
- %rules of the form
- %
- % \begin{isabelle}\ \ \ \ \ %%%
- %@{text "(\<forall>x. R x \<longrightarrow> (P x \<longrightarrow> Q x)) \<longrightarrow> (\<forall>x. P x \<longrightarrow> \<forall>x \<in> R. Q x)"}
- %\end{isabelle}
-
- %\noindent
- %They decompose a bounded quantifier on the right-hand side. We can decompose a
- %bounded quantifier anywhere if R is an equivalence relation or
- %if it is a relation over function types with the range being an equivalence
- %relation. If @{text R} is an equivalence relation we can prove that
-
- %\begin{isabelle}\ \ \ \ \ %%%
- %@{text "\<forall>x \<in> Resp R. P x = \<forall>x. P x"}
- %\end{isabelle}
-
- %\noindent
- %If @{term R\<^isub>2} is an equivalence relation, we can prove that for any predicate @{term P}
-
-%%% FIXME Reviewer 1 claims the theorem is obviously false so maybe we
-%%% should include a proof sketch?
-
- %\begin{isabelle}\ \ \ \ \ %%%
- %@{thm (concl) ball_reg_eqv_range[of R\<^isub>1 R\<^isub>2]}
- %\end{isabelle}
-
- %\noindent
- %The last theorem is new in comparison with Homeier's package. There the
- %injection procedure would be used to prove such goals and
- %the assumption about the equivalence relation would be used. We use the above theorem directly,
- %because this allows us to completely separate the first and the second
- %proof step into two independent ``units''.
-
- The second phase, establishing @{text "reg_thm \<longleftrightarrow> inj_thm"}, starts with an equality
- between the terms of the regularized theorem and the injected theorem.
- The proof again follows the structure of the
- two underlying terms taking respectfulness theorems into account.
-
- %\begin{itemize}
- %\item For two constants an appropriate respectfulness theorem is applied.
- %\item For two variables, we use the assumptions proved in the regularization step.
- %\item For two abstractions, we @{text "\<eta>"}-expand and @{text "\<beta>"}-reduce them.
- %\item For two applications, we check that the right-hand side is an application of
- % @{term Rep} to an @{term Abs} and @{term "Quotient R Rep Abs"} holds. If yes then we
- % can apply the theorem:
-
- %\begin{isabelle}\ \ \ \ \ %%%
- % @{term "R x y \<longrightarrow> R x (Rep (Abs y))"}
- %\end{isabelle}
-
- % Otherwise we introduce an appropriate relation between the subterms
- % and continue with two subgoals using the lemma:
-
- %\begin{isabelle}\ \ \ \ \ %%%
- % @{text "(R\<^isub>1 \<doublearr> R\<^isub>2) f g \<longrightarrow> R\<^isub>1 x y \<longrightarrow> R\<^isub>2 (f x) (g y)"}
- %\end{isabelle}
- %\end{itemize}
-
- We defined the theorem @{text "inj_thm"} in such a way that
- establishing in the third phase the equivalence @{text "inj_thm \<longleftrightarrow> quot_thm"} can be
- achieved by rewriting @{text "inj_thm"} with the preservation theorems and quotient
- definitions. This step also requires that the definitions of all lifted constants
- are used to fold the @{term Rep} with the raw constants. We will give more details
- about our lifting procedure in a longer version of this paper.
-
- %Next for
- %all abstractions and quantifiers the lambda and
- %quantifier preservation theorems are used to replace the
- %variables that include raw types with respects by quantifiers
- %over variables that include quotient types. We show here only
- %the lambda preservation theorem. Given
- %@{term "Quotient R\<^isub>1 Abs\<^isub>1 Rep\<^isub>1"} and @{term "Quotient R\<^isub>2 Abs\<^isub>2 Rep\<^isub>2"}, we have:
-
- %\begin{isabelle}\ \ \ \ \ %%%
- %@{thm (concl) lambda_prs[of _ "Abs\<^isub>1" "Rep\<^isub>1" _ "Abs\<^isub>2" "Rep\<^isub>2"]}
- %\end{isabelle}
-
- %\noindent
- %Next, relations over lifted types can be rewritten to equalities
- %over lifted type. Rewriting is performed with the following theorem,
- %which has been shown by Homeier~\cite{Homeier05}:
-
- %\begin{isabelle}\ \ \ \ \ %%%
- %@{thm (concl) Quotient_rel_rep}
- %\end{isabelle}
-
-
- %Finally, we rewrite with the preservation theorems. This will result
- %in two equal terms that can be solved by reflexivity.
-*}
-
-section {* Derivation of the shape of lifted and raw theorems\label{sec:descending} *}
-
-text {*
- In the previous sections we have assumed, that the user specifies
- both the raw theorem and the statement of the quotient one.
- This allows complete flexibility, as to which parts of the statement
- are lifted to the quotient level and which are intact. In
- other implementations of automatic quotients (for example Homeier's
- package) only the raw theorem is given to the quotient package and
- the package is able to guess the quotient one. In this
- section we give examples where there are multiple possible valid lifted
- theorems starting from a raw one. We also show a heuristic for
- computing the quotient theorem from a raw one, and a mechanism for
- guessing a raw theorem starting with a quotient one.
-*}
-
-subsection {* Multiple lifted theorems *}
-
-text {*
- There are multiple reasons why multiple valid lifted theorems can arize.
- Below we describe three possible scenarios: multiple raw variable,
- multiple quotients for the same raw type and multiple quotients.
-
- Given a raw theorem there are often several variables that include
- a raw type. It this case, one can choose which of the variables to
- lift. In certain cases this can lead to a number of valid theorem
- statements, however type constraints may disallow certain combinations.
- Lets see an example where multiple variables can have different types.
- The Isabelle/HOL induction principle for two lists is:
- \begin{isabelle}\ \ \ \ \ %%%
- @{thm list_induct2'}
- \end{isabelle}
-
- the conclusion is a predicate of the form @{text "P xs ys"}, where
- the two variables are lists. When lifting such theorem to the quotient
- type one can choose if one want to quotient @{text "xs"} or @{text "ys"}, or
- both. All these give rise to valid quotiented theorems, however the
- automatic mode (or other quotient packages) would derive only the version
- with both being quotiented, namely:
- \begin{isabelle}\ \ \ \ \ %%%
- @{thm list_induct2'[quot_lifted]}
- \end{isabelle}
-
- A second scenario, where multiple possible quotient theorems arise is
- when a single raw type is used in two quotients. Consider three quotients
- of the list type: finite sets, finite multisets and lists with distinct
- elements. We have developed all three types with the help of the quotient
- package. Given a theorem that talks about lists --- for example the regular
- induction principle --- one can lift it to three possible theorems: the
- induction principle for finite sets, induction principle for finite
- multisets or the induction principle for distinct lists. Again given an
- induction principle for two lists this gives rise to 15 possible valid
- lifted theorems.
-
- In our developments using the quotient package we also encountered a
- scenario where multiple valid theorem statements arise, but the raw
- types are not identical. Consider the type of lambda terms, where the
- variables are indexed with strings. Quotienting lambda terms by alpha
- equivalence gives rise to a Nominal construction~\cite{Nominal}. However
- at the same time the type of strings being a list of characters can
- lift to theorems about finite sets of characters.
-*}
-
-subsection {* Derivation of the shape of theorems *}
-
-text {*
- To derive a the shape of a lifted or raw theorem the quotient package
- first builds a type and term substitution.
-
- The list of type substitution is created by taking the pairs
- @{text "(raw_type, quotient_type)"} for every user defined quotient.
- The term substitutions are of two types: First for every user-defined
- quotient constant, the pair @{text "(raw_term, quotient_constant)"}
- is included in the substitution. Second, for every quotient relation
- @{text "\<approx>"} the pair @{text "(\<approx>, =)"} with the equality being the
- equality on the defined quotient type is included in the substitution.
-
- The derivation function next traverses the theorem statement expressed
- as a term and replaces the types of all free variables and of all
- lambda-abstractions using the type substitution. For every constant
- is not matched by the term substitution and we perform the type substitution
- on the type of the constant (this is necessary for quotienting theorems
- with polymorphic constants) or the type of the substitution is matched
- and the match is returned.
-
- The heuristic defined above is greedy and according to our experience
- this is what the user wants. The procedure may in some cases produce
- theorem statements that do not type-check. However verifying all
- possible theorem statements is too costly in general.
-*}
-
-subsection {* Interaction modes and derivation of the the shape of theorems *}
-
-text {*
- In the quotient package we provide three interaction modes, that use
- can the procedure procedure defined in the previous subsection.
-
- First, the completely manual mode which we implemented as the
- Isabelle method @{text lifting}. In this mode the user first
- proves the raw theorem. Then the lifted theorem can be proved
- by the method lifting, that takes the reference to the raw theorem
- (or theorem list) as an argument. Such completely manual mode is
- necessary for theorems where the specification of the lifted theorem
- from the raw one is not unique, which we discussed in the previous
- subsection.
-
- Next, we provide a mode for automatically lifting a given
- raw theorem. We implemented this mode as an isabelle attribute,
- so given the raw theorem @{text thm}, the user can refer to the
- theorem @{text "thm[quot_lifted]"}.
-
- Finally we provie a method for translating a given quotient
- level theorem to a raw one. We implemented this as an Isabelle
- method @{text descending}. The user starts with expressing a
- quotient level theorem statement and applies this method.
- The quotient package derives a raw level statement and assumes
- it as a subgoal. Given that this subgoal is proved, the quotient
- package can lift the raw theorem fulfilling the proof of the
- original lifted theorem statement.
-*}
-
-section {* Conclusion and Related Work\label{sec:conc}*}
-
-text {*
-
- \noindent
- 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/}.}
- The package is
- heavily used in the new version of Nominal Isabelle, which provides a
- convenient reasoning infrastructure for programming language calculi
- involving general binders. To achieve this, it builds types representing
- @{text \<alpha>}-equivalent terms. Earlier versions of Nominal Isabelle have been
- used successfully in formalisations of an equivalence checking algorithm for
- LF \cite{UrbanCheneyBerghofer08}, Typed
- Scheme~\cite{TobinHochstadtFelleisen08}, several calculi for concurrency
- \cite{BengtsonParow09} and a strong normalisation result for cut-elimination
- in classical logic \cite{UrbanZhu08}.
-
- {\bf INSTEAD OF NOMINAL WORK, GIVE WORK BY BULWAHN ET AL?}
-
- There is a wide range of existing literature for dealing with quotients
- in theorem provers. Slotosch~\cite{Slotosch97} implemented a mechanism that
- automatically defines quotient types for Isabelle/HOL. But he did not
- include theorem lifting. Harrison's quotient package~\cite{harrison-thesis}
- is the first one that is able to automatically lift theorems, however only
- first-order theorems (that is theorems where abstractions, quantifiers and
- variables do not involve functions that include the quotient type). There is
- also some work on quotient types in non-HOL based systems and logical
- frameworks, including theory interpretations in
- PVS~\cite{PVS:Interpretations}, new types in MetaPRL~\cite{Nogin02}, and
- setoids in Coq \cite{ChicliPS02}. Paulson showed a construction of
- quotients that does not require the Hilbert Choice operator, but also only
- first-order theorems can be lifted~\cite{Paulson06}. The most related work
- to our package is the package for HOL4 by Homeier~\cite{Homeier05}. He
- introduced most of the abstract notions about quotients and also deals with
- lifting of higher-order theorems. However, he cannot deal with quotient
- compositions (needed for lifting theorems about @{text flat}). Also, a
- number of his definitions, like @{text ABS}, @{text REP} and @{text INJ} etc
- only exist in \cite{Homeier05} as ML-code, not included in the paper.
- Like Homeier's, our quotient package can deal with partial equivalence
- relations, but for lack of space we do not describe the mechanisms
- needed for this kind of quotient constructions.
-
-%%% FIXME Reviewer 3 would like to know more about the lifting in Coq and PVS,
-%%% and some comparison. I don't think we have the space for any additions...
-
- One feature of our quotient package is that when lifting theorems, the user
- can precisely specify what the lifted theorem should look like. This feature
- is necessary, for example, when lifting an induction principle for two
- lists. Assuming this principle has as the conclusion a predicate of the
- form @{text "P xs ys"}, then we can precisely specify whether we want to
- quotient @{text "xs"} or @{text "ys"}, or both. We found this feature very
- useful in the new version of Nominal Isabelle, where such a choice is
- required to generate a reasoning infrastructure for alpha-equated terms.
-%%
-%% give an example for this
-%%
- \smallskip
-
- \noindent
- {\bf Acknowledgements:} We would like to thank Peter Homeier for the many
- discussions about his HOL4 quotient package and explaining to us
- some of its finer points in the implementation. Without his patient
- help, this work would have been impossible. We would like to thank
- Andreas Lochbiler for his comments on the first version of the quotient
- package, in particular for the suggestions about the descending method.
-
-*}
-
-text_raw {*
- %%\bibliographystyle{abbrv}
- \bibliography{root}
-
- \appendix
-
-*}
-
-section {* Examples \label{sec:examples} *}
-
-text {*
-
-%%% FIXME Reviewer 1 would like an example of regularized and injected
-%%% statements. He asks for the examples twice, but I would still ignore
-%%% it due to lack of space...
-
- \noindent
- In this appendix we will show a sequence of declarations for defining the
- type of integers by quotienting pairs of natural numbers, and
- lifting one theorem.
-
- A user of our quotient package first needs to define a relation on
- the raw type with which the quotienting will be performed. We give
- the same integer relation as the one presented in \eqref{natpairequiv}:
-
- \begin{isabelle}\ \ \ \ \ %
- \begin{tabular}{@ {}l}
- \isacommand{fun}~~@{text "int_rel :: (nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"}\\
- \isacommand{where}~~@{text "int_rel (m, n) (p, q) = (m + q = n + p)"}
- \end{tabular}
- \end{isabelle}
-
- \noindent
- Next the quotient type must be defined. This generates a proof obligation that the
- relation is an equivalence relation, which is solved automatically using the
- definition of equivalence and extensionality:
-
- \begin{isabelle}\ \ \ \ \ %
- \begin{tabular}{@ {}l}
- \isacommand{quotient\_type}~~@{text "int"}~~\isacommand{=}~~@{text "(nat \<times> nat)"}~~\isacommand{/}~~@{text "int_rel"}\\
- \hspace{5mm}@{text "by (auto simp add: equivp_def expand_fun_eq)"}
- \end{tabular}
- \end{isabelle}
-
- \noindent
- The user can then specify the constants on the quotient type:
-
- \begin{isabelle}\ \ \ \ \ %
- \begin{tabular}{@ {}l}
- \isacommand{quotient\_definition}~~@{text "0 :: int"}~~\isacommand{is}~~@{text "(0 :: nat, 0 :: nat)"}\\[3mm]
- \isacommand{fun}~~@{text "add_pair"}\\
- \isacommand{where}~~%
- @{text "add_pair (m, n) (p, q) \<equiv> (m + p :: nat, n + q :: nat)"}\\
- \isacommand{quotient\_definition}~~@{text "+ :: int \<Rightarrow> int \<Rightarrow> int"}~~%
- \isacommand{is}~~@{text "add_pair"}\\
- \end{tabular}
- \end{isabelle}
-
- \noindent
- The following theorem about addition on the raw level can be proved.
-
- \begin{isabelle}\ \ \ \ \ %
- \isacommand{lemma}~~@{text "add_pair_zero: int_rel (add_pair (0, 0) x) x"}
- \end{isabelle}
-
- \noindent
- If the user lifts this theorem, the quotient package performs all the lifting
- automatically leaving the respectfulness proof for the constant @{text "add_pair"}
- as the only remaining proof obligation. This property needs to be proved by the user:
-
- \begin{isabelle}\ \ \ \ \ %
- \begin{tabular}{@ {}l}
- \isacommand{lemma}~~@{text "[quot_respect]:"}\\
- @{text "(int_rel \<doublearr> int_rel \<doublearr> int_rel) add_pair add_pair"}
- \end{tabular}
- \end{isabelle}
-
- \noindent
- It can be discharged automatically by Isabelle when hinting to unfold the definition
- of @{text "\<doublearr>"}.
- After this, the user can prove the lifted lemma as follows:
-
- \begin{isabelle}\ \ \ \ \ %
- \isacommand{lemma}~~@{text "0 + (x :: int) = x"}~~\isacommand{by}~~@{text "lifting add_pair_zero"}
- \end{isabelle}
-
- \noindent
- or by using the completely automated mode stating just:
-
- \begin{isabelle}\ \ \ \ \ %
- \isacommand{thm}~~@{text "add_pair_zero[quot_lifted]"}
- \end{isabelle}
-
- \noindent
- Both methods give the same result, namely @{text "0 + x = x"}
- where @{text x} is of type integer.
- Although seemingly simple, arriving at this result without the help of a quotient
- package requires a substantial reasoning effort (see \cite{Paulson06}).
-
- {\bf \begin{itemize}
- \item explain how Quotient R Abs Rep is proved
- \item Type maps and Relation maps (show the case for functions)
- \item Quotient extensions (quot\_thms)
- \item Respectfulness and preservation
- - Show special cases for quantifiers and lambda
- - How do prs theorems look like for quotient compositions
- \item Quotient-type locale
- - Show the proof as much simpler than Homeier's one
- \item ??? Infrastructure for storing theorems (rsp, prs, eqv, quot and idsimp)
- \item Lifting vs Descending vs quot\_lifted
- - automatic theorem translation heuristic
- \item Partial equivalence quotients
- - Bounded abstraction
- - Respects
- - partial descending
- \item The heuristics for automatic regularization, injection and cleaning.
- \item A complete example of a lifted theorem together with the regularized
- injected and cleaned statement
- \item Examples of quotients and properties that we used the package for.
- \item co/contra-variance from Ondrej should be taken into account
- \item give an example where precise specification of goal is necessary
- \item mention multiple map\_prs2 theorems for compositional quotients
- \end{itemize}}
-*}
-
-
-
-(*<*)
-end
-(*>*)