nominal2: comparison Quotient-Paper/Paper.thy

equal deleted inserted replaced

-:4da5c5c29009
+:ad03df7e8056
+(* How to change the notation for \<lbrakk> \<rbrakk> meta-level implications? *)
 (*<*)
 theory Paper
 imports "Quotient"
 "LaTeXsugar"
 "../Nominal/FSet"
 begin
+print_syntax
 notation (latex output)
 rel_conj ("_ OOO _" [53, 53] 52)
 and
-fun_map ("_ ---> _" [51, 51] 50)
+"op -->" (infix "\<rightarrow>" 100)
 and
-fun_rel ("_ ===> _" [51, 51] 50)
+"==>" (infix "\<Rightarrow>" 100)
+and
+fun_map (infix "\<longrightarrow>" 51)
+and
+fun_rel (infix "\<Longrightarrow>" 51)
 and
 list_eq (infix "\<approx>" 50) (* Not sure if we want this notation...? *)
 ML {*
 fun nth_conj n (_, r) = nth (HOLogic.dest_conj r) n;
 (*>*)
 section {* Introduction *}
 text {*
-{\hfill quote by Larry}\bigskip
+\begin{flushright}
+{\em ``Not using a [quotient] package has its advantages: we do not have to\\
+collect all the theorems we shall ever want into one giant list;''}\\
+Larry Paulson \cite{Paulson06}
+\end{flushright}\smallskip
 \noindent
 Isabelle is a generic theorem prover in which many logics can be implemented.
 The most widely used one, however, is
 Higher-Order Logic (HOL). This logic 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. It is well understood
-to use both mechanism for dealing with quotient constructions in HOL (cite Larry).
+to use both mechanisms for dealing with quotient constructions in HOL (see for example
+\cite{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
 % I would avoid substraction for natural numbers.
 \item We allow lifting only some occurrences of quotiented
 types. Rsp/Prs extended. (used in nominal)
 \item The quotient package is very modular. Definitions can be added
-separately, rsp and prs can be proved separately and theorems can
+separately, rsp and prs can be proved separately, Quotients and maps
-be lifted on a need basis. (useful with type-classes).
+can be defined separately and theorems can
+be lifted on a need basis. (useful with type-classes).
 \item Can be used both manually (attribute, separate tactics,
 rsp/prs databases) and programatically (automated definition of
 lifted constants, the rsp proof obligations and theorem statement
 translation according to given quotients).
 \begin{itemize}
 \item @{text "ABS(\<alpha>\<^isub>1, \<alpha>\<^isub>2)"} = @{text "id"}
 \item @{text "REP(\<alpha>\<^isub>1, \<alpha>\<^isub>2)"}  =  @{text "id"}
 \item @{text "ABS(\<sigma>, \<sigma>)"}  =  @{text "id"}
 \item @{text "REP(\<sigma>, \<sigma>)"}  =  @{text "id"}
-\item @{text "ABS(\<sigma>\<^isub>1\<rightarrow>\<sigma>\<^isub>2,\<tau>\<^isub>1\<rightarrow>\<tau>\<^isub>2)"}  =  @{text "REP(\<sigma>\<^isub>1,\<tau>\<^isub>1) ---> ABS(\<sigma>\<^isub>2,\<tau>\<^isub>2)"}
+\item @{text "ABS(\<sigma>\<^isub>1\<rightarrow>\<sigma>\<^isub>2,\<tau>\<^isub>1\<rightarrow>\<tau>\<^isub>2)"}  =  @{text "REP(\<sigma>\<^isub>1,\<tau>\<^isub>1) \<longrightarrow> ABS(\<sigma>\<^isub>2,\<tau>\<^isub>2)"}
-\item @{text "REP(\<sigma>\<^isub>1\<rightarrow>\<sigma>\<^isub>2,\<tau>\<^isub>1\<rightarrow>\<tau>\<^isub>2)"}  =  @{text "ABS(\<sigma>\<^isub>1,\<tau>\<^isub>1) ---> REP(\<sigma>\<^isub>2,\<tau>\<^isub>2)"}
+\item @{text "REP(\<sigma>\<^isub>1\<rightarrow>\<sigma>\<^isub>2,\<tau>\<^isub>1\<rightarrow>\<tau>\<^isub>2)"}  =  @{text "ABS(\<sigma>\<^isub>1,\<tau>\<^isub>1) \<longrightarrow> REP(\<sigma>\<^isub>2,\<tau>\<^isub>2)"}
 \item @{text "ABS((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n))\<kappa>, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>n))\<kappa>)"}  =  @{text "(map \<kappa>) (ABS(\<sigma>\<^isub>1,\<tau>\<^isub>1)) \<dots> (ABS(\<sigma>\<^isub>n,\<tau>\<^isub>n))"}
 \item @{text "REP((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n))\<kappa>, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>n))\<kappa>)"}  =  @{text "(map \<kappa>) (REP(\<sigma>\<^isub>1,\<tau>\<^isub>1)) \<dots> (REP(\<sigma>\<^isub>n,\<tau>\<^isub>n))"}
 \item @{text "ABS((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n))\<kappa>\<^isub>1, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>m))\<kappa>\<^isub>2)"}  =  @{text "Abs_\<kappa>\<^isub>2 \<circ> (map \<kappa>\<^isub>1) (ABS(\<rho>\<^isub>1,\<nu>\<^isub>1) \<dots> (ABS(\<rho>\<^isub>p,\<nu>\<^isub>p)"} provided @{text "\<eta> \<kappa>\<^isub>2 = (\<alpha>\<^isub>1\<dots>\<alpha>\<^isub>p)\<kappa>\<^isub>1 \<and> \<exists>s. s(\<sigma>s\<kappa>\<^isub>1)=\<rho>s\<kappa>\<^isub>1 \<and> s(\<tau>s\<kappa>\<^isub>2)=\<nu>s\<kappa>\<^isub>2"}
 \item @{text "REP((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n))\<kappa>\<^isub>1, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>m))\<kappa>\<^isub>2)"}  =  @{text "(map \<kappa>\<^isub>1) (REP(\<rho>\<^isub>1,\<nu>\<^isub>1) \<dots> (REP(\<rho>\<^isub>p,\<nu>\<^isub>p) \<circ> Rep_\<kappa>\<^isub>2"} provided @{text "\<eta> \<kappa>\<^isub>2 = (\<alpha>\<^isub>1\<dots>\<alpha>\<^isub>p)\<kappa>\<^isub>1 \<and> \<exists>s. s(\<sigma>s\<kappa>\<^isub>1)=\<rho>s\<kappa>\<^isub>1 \<and> s(\<tau>s\<kappa>\<^isub>2)=\<nu>s\<kappa>\<^isub>2"}
 \end{itemize}
 Apart from the last 2 points the definition is same as the one implemented in
-in Homeier's HOL package, below is the definition of @{term fconcat}
+in Homeier's HOL package. Adding composition in last two cases is necessary
-that shows the last points:
+for compositional quotients. We ilustrate the different behaviour of the
+definition by showing the derived definition of @{term fconcat}:
 @{thm fconcat_def[no_vars]}
 The aggregate @{term Abs} function takes a finite set of finite sets
 and applies @{term "map rep_fset"} composed with @{term rep_fset} to
 text {*
 A respectfulness lemma for a constant states that the equivalence
 class returned by this constant depends only on the equivalence
-classes of the arguments applied to the constant. This can be
+classes of the arguments applied to the constant. To automatically
-expressed in terms of an aggregate relation between the constant
+lift a theorem that talks about a raw constant, to a theorem about
-and itself, for example the respectfullness for @{term "append"}
+the quotient type a respectfulness theorem is required.
+A respectfulness condition for a constant can be expressed in
+terms of an aggregate relation between the constant and itself,
+for example the respectfullness for @{term "append"}
 can be stated as:
 @{thm [display] append_rsp[no_vars]}
 \noindent
-Which is equivalent to:
+Which after unfolding @{term "op \<Longrightarrow>"} is equivalent to:
 @{thm [display] append_rsp_unfolded[no_vars]}
-Below we show the algorithm for finding the aggregate relation.
+An aggregate relation is defined in terms of relation composition,
-This algorithm uses
+so we define it first:
-the relation composition which we define as:
 \begin{definition}[Composition of Relations]
 @{abbrev "rel_conj R1 R2"} where @{text OO} is the predicate
 composition @{thm pred_compI[no_vars]}
 \end{definition}
-Given an aggregate raw type and quotient type:
+The aggregate relation for an aggregate raw type and quotient type
+is defined as:
-\begin{itemize}
-\item For equal types or free type variables return equality
+\begin{itemize}
+\item @{text "REL(\<alpha>\<^isub>1, \<alpha>\<^isub>2)"} = @{text "op ="}
-\item For equal type constructors use the appropriate rel
+\item @{text "REL(\<sigma>, \<sigma>)"}  =  @{text "op ="}
-function applied to the results for the argument pairs
+\item @{text "REL((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n))\<kappa>, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>n))\<kappa>)"}  =  @{text "(rel \<kappa>) (REL(\<sigma>\<^isub>1,\<tau>\<^isub>1)) \<dots> (REL(\<sigma>\<^isub>n,\<tau>\<^isub>n))"}
+\item @{text "REL((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n))\<kappa>\<^isub>1, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>m))\<kappa>\<^isub>2)"}  =  @{text "(rel \<kappa>\<^isub>1) (REL(\<rho>\<^isub>1,\<nu>\<^isub>1) \<dots> (REL(\<rho>\<^isub>p,\<nu>\<^isub>p) OOO Eqv_\<kappa>\<^isub>2"} provided @{text "\<eta> \<kappa>\<^isub>2 = (\<alpha>\<^isub>1\<dots>\<alpha>\<^isub>p)\<kappa>\<^isub>1 \<and> \<exists>s. s(\<sigma>s\<kappa>\<^isub>1)=\<rho>s\<kappa>\<^isub>1 \<and> s(\<tau>s\<kappa>\<^isub>2)=\<nu>s\<kappa>\<^isub>2"}
-\item For unequal type constructors, look in the quotients information
-for a quotient type that matches the type constructor, and instantiate
+\end{itemize}
-the type appropriately getting back an instantiation environment. We
-apply the environment to the arguments and recurse composing it with
+Again, the last case is novel, so lets look at the example of
-the aggregate relation function.
+respectfullness for @{term concat}. The statement according to
+the definition above is:
-\end{itemize}
-Again, the the behaviour of our algorithm in the last situation is
-novel, so lets look at the example of respectfullness for @{term concat}.
-The statement as computed by the algorithm above is:
 @{thm [display] concat_rsp[no_vars]}
 \noindent
 By unfolding the definition of relation composition and relation map
 text {*
 Given two quotients, one of which quotients a container, and the
 other quotients the type in the container, we can write the
 composition of those quotients. To compose two quotient theorems
-we compose the relations with relation composition
+we compose the relations with relation composition as defined above
-and the abstraction and relation functions with function composition.
+and the abstraction and relation functions are the ones of the sub
-The @{term "Rep"} and @{term "Abs"} functions that we obtain are
+quotients composed with the usual function composition.
-the same as the ones created by in the aggregate functions and the
+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 concat}. To be able to lift
-theorems that talk about it we will first prove the composition
+theorems that talk about it we provide the composition quotient
-quotient theorems, which then lets us perform the lifting procedure
+theorems, which then lets us perform the lifting procedure in an
-in an unchanged way:
+unchanged way:
 @{thm [display] quotient_compose_list[no_vars]}
 *}
 text {*
 The core of the quotient package takes an original theorem that
 talks about the raw types, and the statement of the theorem that
 it is supposed to produce. This is different from other existing
-quotient packages, where only the raw theorems was necessary.
+quotient packages, where only the raw theorems were necessary.
 We notice that in some cases only some occurrences of the raw
 types need to be lifted. This is for example the case in the
 new Nominal package, where a raw datatype that talks about
 pairs of natural numbers or strings (being lists of characters)
 should not be changed to a quotient datatype with constructors
 implementation.
 We first define the statement of the regularized theorem based
 on the original theorem and the goal theorem. Then we define
 the statement of the injected theorem, based on the regularized
-theorem and the goal. We then show the 3 proofs, and all three
+theorem and the goal. We then show the 3 proofs, as all three
 can be performed independently from each other.
 *}
 subsection {* Regularization and Injection statements *}
 text {*
-The function that gives the statement of the regularized theorem
+We first define the function @{text REG}, which takes the statements
-takes the statement of the raw theorem (a term) and the statement
+of the raw theorem and the lifted theorem (both as terms) and
-of the lifted theorem. The intuition behind the procedure is that
+returns the statement of the regularized version. The intuition
-it replaces quantifiers and abstractions involving raw types
+behind this function is that it replaces quantifiers and
-by bounded ones, and equalities involving raw types are replaced
+abstractions involving raw types by bounded ones, and equalities
-by appropriate aggregate relations. It is defined as follows:
+involving raw types are replaced by appropriate aggregate
+relations. It is defined as follows:
 \begin{itemize}
 \item @{text "REG (\<lambda>x : \<sigma>. t, \<lambda>x : \<sigma>. s) = \<lambda>x : \<sigma>. REG (t, s)"}
 \item @{text "REG (\<lambda>x : \<sigma>. t, \<lambda>x : \<tau>. s) = \<lambda>x : \<sigma> \<in> Res (REL (\<sigma>, \<tau>)). REG (t, s)"}
 \item @{text "REG (\<forall>x : \<sigma>. t, \<forall>x : \<sigma>. s) = \<forall>x : \<sigma>. REG (t, s)"}
 \item @{text "REG (t\<^isub>1 t\<^isub>2, s\<^isub>1 s\<^isub>2) = REG (t\<^isub>1, s\<^isub>1) REG (t\<^isub>2, s\<^isub>2)"}
 \item @{text "REG (v\<^isub>1, v\<^isub>2) = v\<^isub>1"}
 \item @{text "REG (c\<^isub>1, c\<^isub>2) = c\<^isub>1"}
 \end{itemize}
-Existential quantifiers and unique existential quantifiers are defined
+In the above definition we ommited the cases for existential quantifiers
-similarily to the universal one.
+and unique existential quantifiers, as they are very similar to the cases
+for the universal quantifier.
-The function that gives the statment of the injected theorem
-takes the statement of the regularized theorems and the statement
+Next we define the function @{text INJ} which takes the statement of
-of the lifted theorem both as terms.
+the regularized theorems and the statement of the lifted theorem both as
+terms and returns the statment of the injected theorem:
 \begin{itemize}
 \item @{text "INJ ((\<lambda>x. t) : \<sigma>, (\<lambda>x. s) : \<sigma>) = \<lambda>x. (INJ (t, s)"}
 \item @{text "INJ ((\<lambda>x. t) : \<sigma>, (\<lambda>x. s) : \<tau>) = REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (\<lambda>x. (INJ (t, s))))"}
 \item @{text "INJ ((\<lambda>x \<in> R. t) : \<sigma>, (\<lambda>x. s) : \<tau>) = REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (\<lambda>x \<in> R. (INJ (t, s))))"}
 For existential quantifiers and unique existential quantifiers it is
 defined similarily to the universal one.
 *}
-subsection {* Proof of Regularization *}
+subsection {* Proof procedure *}
-text {*
+(* In the below the type-guiding 'QuotTrue' assumption is removed; since we
-Example of non-regularizable theorem ($0 = 1$).
+present in a paper a version with typed-variables it is not necessary *)
+text {*
-Separtion of regularization from injection thanks to the following 2 lemmas:
-\begin{lemma}
+With the above definitions of @{text "REG"} and @{text "INJ"} we can show
-If @{term R2} is an equivalence relation, then:
+how the proof is performed. The first step is always the application of
-\begin{eqnarray}
+of the following lemma:
-@{thm (rhs) ball_reg_eqv_range[no_vars]} & = & @{thm (lhs) ball_reg_eqv_range[no_vars]}\\
-@{thm (rhs) bex_reg_eqv_range[no_vars]} & = & @{thm (lhs) bex_reg_eqv_range[no_vars]}
+@{term "[|A; A --> B; B = C; C = D|] ==> D"}
-\end{eqnarray}
-\end{lemma}
+With @{text A} instantiated to the original raw theorem,
+@{text B} instantiated to @{text "REG(A)"},
-Other lemmas used in regularization:
+@{text C} instantiated to @{text "INJ(REG(A))"},
+and @{text D} instantiated to the statement of the lifted theorem.
+The first assumption can be immediately discharged using the original
+theorem and the three left subgoals are exactly the subgoals of regularization,
+injection and cleaning. The three can be proved independently by the
+framework and in case there are non-solved subgoals they can be left
+to the user.
+The injection and cleaning subgoals are always solved if the appropriate
+respectfulness and preservation theorems are given. It is not the case
+with regularization; sometimes a theorem given by the user does not
+imply a regularized version and a stronger one needs to be proved. This
+is outside of the scope of the quotient package, so the user is then left
+with such obligations. As an example lets see the simplest possible
+non-liftable theorem for integers: When we want to prove @{term "0 \<noteq> 1"}
+on integers the fact that @{term "\<not> (0, 0) = (1, 0)"} is not enough. It
+only shows that particular items in the equivalence classes are not equal,
+a more general statement saying that the classes are not equal is necessary.
+*}
+subsection {* Proving Regularization *}
+text {*
+Isabelle provides a set of \emph{mono} rules, that are used to split implications
+of similar statements into simpler implication subgoals. These are enchanced
+with special quotient theorem in the regularization goal. Below we only show
+the versions for the universal quantifier. For the existential quantifier
+and abstraction they are analoguous with some symmetry.
+First, bounded universal quantifiers can be removed on the right:
+@{thm [display] ball_reg_right[no_vars]}
+They can be removed anywhere if the relation is an equivalence relation:
 @{thm [display] ball_reg_eqv[no_vars]}
+And finally it can be removed anywhere if @{term R2} is an equivalence relation, then:
+\[
+@{thm (rhs) ball_reg_eqv_range[no_vars]} = @{thm (lhs) ball_reg_eqv_range[no_vars]}
+\]
+The last theorem is new in comparison with Homeier's package; it allows separating
+regularization from injection.
+*}
+(*
+@{thm (rhs) bex_reg_eqv_range[no_vars]} = @{thm (lhs) bex_reg_eqv_range[no_vars]}
+@{thm [display] bex_reg_left[no_vars]}
+@{thm [display] bex1_bexeq_reg[no_vars]}
 @{thm [display] bex_reg_eqv[no_vars]}
 @{thm [display] babs_reg_eqv[no_vars]}
 @{thm [display] babs_simp[no_vars]}
+*)
-@{thm [display] ball_reg_right[no_vars]}
-@{thm [display] bex_reg_left[no_vars]}
-@{thm [display] bex1_bexeq_reg[no_vars]}
-*}
 subsection {* Injection *}
 text {*
+The injection proof starts with an equality between the regularized theorem
-The 2 key lemmas are:
+and the injected version. The proof again follows by the structure of the
+two term, and is defined for a goal being a relation between the two terms.
+\begin{itemize}
+\item For two constants, an appropriate constant respectfullness assumption is used.
+\item For two variables, the regularization assumptions state that they are related.
+\item For two abstractions, they are eta-expanded and beta-reduced.
+\end{itemize}
+Otherwise the two terms are applications. There are two cases: If there is a REP/ABS
+in the injected theorem we can use the theorem:
+@{thm [display] rep_abs_rsp[no_vars]}
+and continue the proof.
+Otherwise we introduce an appropriate relation between the subterms and continue with
+two subgoals using the lemma:
 @{thm [display] apply_rsp[no_vars]}
-@{thm [display] rep_abs_rsp[no_vars]}
+*}
-*}
 subsection {* Cleaning *}
-text {* Preservation of quantifiers, abstractions, relations, quotient-constants
+text {*
-(definitions) and user given constant preservation lemmas *}
+The @{text REG} and @{text INJ} functions have been defined in such a way
+that establishing the goal theorem now consists only on rewriting the
+injected theorem with the preservation theorems.
+\begin{itemize}
+\item First for lifted constants, their definitions are the preservation rules for
+them.
+\item For lambda abstractions lambda preservation establishes
+the equality between the injected theorem and the goal. This allows both
+abstraction and quantification over lifted types.
+@{thm [display] lambda_prs[no_vars]}
+\item Relations over lifted types are folded with:
+@{thm [display] Quotient_rel_rep[no_vars]}
+\item User given preservation theorems, that allow using higher level operations
+and containers of types being lifted. An example may be
+@{thm [display] map_prs(1)[no_vars]}
+\end{itemize}
+Preservation of relations and user given constant preservation lemmas *}
 section {* Examples *}
+(* Mention why equivalence *)
+text {*
+A user of our quotient package first needs to define an equivalence relation:
+@{text "fun \<approx> where (x, y) \<approx> (u, v) = (x + v = u + y)"}
+Then the user defines a quotient type:
+@{text "quotient_type int = (nat \<times> nat) / \<approx>"}
+Which leaves a proof obligation that the relation is an equivalence relation,
+that can be solved with the automatic tactic with two definitions.
+The user can then specify the constants on the quotient type:
+@{text "quotient_definition 0 \<Colon> int is (0\<Colon>nat, 0\<Colon>nat)"}
+@{text "fun plus_raw where plus_raw (x, y) (u, v) = (x + u, y + v)"}
+@{text "quotient_definition (op +) \<Colon> (int \<Rightarrow> int \<Rightarrow> int) is plus_raw"}
+Lets first take a simple theorem about addition on the raw level:
+@{text "lemma plus_zero_raw: plus_raw (0, 0) i \<approx> i"}
+When the user tries to lift a theorem about integer addition, the respectfulness
+proof obligation is left, so let us prove it first:
+@{text "lemma (op \<approx> \<Longrightarrow> op \<approx> \<Longrightarrow> op \<approx>) plus_raw plus_raw"}
+Can be proved automatically by the system just by unfolding the definition
+of @{term "op \<Longrightarrow>"}.
+Now the user can either prove a lifted lemma explicitely:
+@{text "lemma 0 + i = i by lifting plus_zero_raw"}
+Or in this simple case use the automated translation mechanism:
+@{text "thm plus_zero_raw[quot_lifted]"}
+obtaining the same result.
+*}
 section {* Related Work *}
 text {*
 \begin{itemize}
 \item Setoids in Coq and \cite{ChicliPS02}
 \end{itemize}
 *}
+section {* Conclusion *}
 (*<*)
 end
 (*>*)

changeset 2312	ad03df7e8056
parent 2213	231a20534950
child 2214	02e03d4287ec