(* How to change the notation for \<lbrakk> \<rbrakk> meta-level implications? *)(*<*)theory Paperimports "Quotient" "LaTeXsugar" "../Nominal/FSet"beginprint_syntaxnotation (latex output) rel_conj ("_ OOO _" [53, 53] 52) and "op -->" (infix "\<rightarrow>" 100) and "==>" (infix "\<Rightarrow>" 100) and fun_map (infix "\<longrightarrow>" 51) and fun_rel (infix "\<Longrightarrow>" 51) and list_eq (infix "\<approx>" 50) and (* Not sure if we want this notation...? *) fempty ("\<emptyset>\<^isub>f") and funion ("_ \<union>\<^isub>f _") and Cons ("_::_") 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 (ProofContext.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))*}(*>*)section {* Introduction *}text {* \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 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 @{text [display, indent=10] "(n\<^isub>1, n\<^isub>2) \<approx> (m\<^isub>1, m\<^isub>2) \<equiv> n\<^isub>1 + n\<^isub>2 = m\<^isub>1 + m\<^isub>2"} \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 (namely @{text "add\<^bsub>nat\<times>nat\<^esub> (x\<^isub>1, y\<^isub>1) (x\<^isub>2, y\<^isub>2) \<equiv> (x\<^isub>1 + x\<^isub>2, y\<^isub>1 + y\<^isub>2)"}). Similarly one can construct the type of finite sets by quotienting lists according to the equivalence relation @{text [display, indent=10] "xs \<approx> ys \<equiv> (\<forall>x. x \<in> xs \<longleftrightarrow> x \<in> ys)"} \noindent which states that two lists are equivalent if every element in one list is also member in the other (@{text "\<in>"} stands here for membership in lists). The empty finite set, written @{term "{||}"} can then be defined as the empty list and union of two finite sets, written @{text "\<union>\<^isub>f"}, as list append. Another important area of quotients is reasoning about programming language calculi. A simple example are lambda-terms defined as \begin{center} @{text "t ::= x | t t | \<lambda>x.t"} \end{center} \noindent The difficulty with this definition of lambda-terms arises when, for example, proving formally the substitution lemma ... On the other hand if we reason about alpha-equated lambda-terms, that means terms quotient according to alpha-equivalence, then reasoning infrastructure can be introduced that make the formal proof of the substitution lemma almost trivial. The problem is that in order to be able to reason about integers, finite sets and alpha-equated lambda-terms 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 @{text "\<alpha> list"} and finite sets of type @{text "\<alpha>"}, and also for raw lambda-terms and alpha-equated lambda-terms). This lifting usually requires a \emph{lot} of tedious reasoning effort. The purpose of a \emph{quotient package} is to ease the lifting and automate the reasoning as much as possible. While for integers and finite sets teh tedious reasoning needs to be done only once, Nominal Isabelle providing a reasoning infrastructure for binders and @{text "\<alpha>"}-equated terms it needs to be done over and over again. Such a package is a central component of the new version of Nominal Isabelle where representations of alpha-equated terms are constructed according to specifications given by the user. In the context of HOL, there have been several quotient packages (...). The most notable is the one by Homeier (...) implemented in HOL4. However, what is surprising, none of them can deal compositions of quotients, for example with lifting theorems about @{text "concat"}: @{thm [display] concat.simps(1)} @{thm [display] concat.simps(2)[no_vars]} \noindent One would like to lift this definition to the operation: @{thm [display] fconcat_empty[no_vars]} @{thm [display] fconcat_insert[no_vars]} \noindent What is special about this operation is that we have as input lists of lists which after lifting turn into finite sets of finite sets.*}subsection {* Contributions *}text {* We present the detailed lifting procedure, which was not shown before. The quotient package presented in this paper has the following advantages over existing packages: \begin{itemize} \item We define quotient composition, function map composition and relation map composition. This lets lifting polymorphic types with subtypes quotiented as well. We extend the notions of respectfulness and preservation to cope with quotient composition. \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, Quotients and maps 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). \end{itemize}*}section {* Quotient Type*}text {* In this section we present the definitions of a quotient that follow those by Homeier, the proofs can be found there. \begin{definition}[Quotient] A relation $R$ with an abstraction function $Abs$ and a representation function $Rep$ is a \emph{quotient} if and only if: \begin{enumerate} \item @{thm (rhs1) Quotient_def[of "R", no_vars]} \item @{thm (rhs2) Quotient_def[of "R", no_vars]} \item @{thm (rhs3) Quotient_def[of "R", no_vars]} \end{enumerate} \end{definition} \begin{definition}[Relation map and function map]\\ @{thm fun_rel_def[of "R1" "R2", no_vars]}\\ @{thm fun_map_def[no_vars]} \end{definition} The main theorems for building higher order quotients is: \begin{lemma}[Function Quotient] If @{thm (prem 1) fun_quotient[no_vars]} and @{thm (prem 2) fun_quotient[no_vars]} then @{thm (concl) fun_quotient[no_vars]} \end{lemma}*}subsection {* Higher Order Logic *}text {* Types: \begin{eqnarray}\nonumber @{text "\<sigma> ::="} & @{text "\<alpha>"} & \textrm{(type variable)} \\ \nonumber @{text "|"} & @{text "(\<sigma>,\<dots>,\<sigma>)\<kappa>"} & \textrm{(type construction)} \end{eqnarray} Terms: \begin{eqnarray}\nonumber @{text "t ::="} & @{text "x\<^isup>\<sigma>"} & \textrm{(variable)} \\ \nonumber @{text "|"} & @{text "c\<^isup>\<sigma>"} & \textrm{(constant)} \\ \nonumber @{text "|"} & @{text "t t"} & \textrm{(application)} \\ \nonumber @{text "|"} & @{text "\<lambda>x\<^isup>\<sigma>. t"} & \textrm{(abstraction)} \\ \nonumber \end{eqnarray}*}section {* Constants *}(* Say more about containers? *)text {* To define a constant on the lifted type, an aggregate abstraction function is applied to the raw constant. Below we describe the operation that generates an aggregate @{term "Abs"} or @{term "Rep"} function given the compound raw type and the compound quotient type. This operation will also be used in translations of theorem statements and in the lifting procedure. The operation is additionally able to descend into types for which maps are known. Such maps for most common types (list, pair, sum, option, \ldots) are described in Homeier, and we assume that @{text "map"} is the function that returns a map for a given type. Then REP/ABS is defined as follows: \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) \<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) \<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. Adding composition in last two cases is necessary 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 its input, obtaining a list of lists, passes the result to @{term concat} obtaining a list and applies @{term abs_fset} obtaining the composed finite set.*}subsection {* Respectfulness *}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. To automatically lift a theorem that talks about a raw constant, to a theorem about the quotient type a respectfulness theorem is required. A respectfulness condition for a constant can be expressed in terms of an aggregate relation between the constant and itself, for example the respectfullness for @{term "append"} can be stated as: @{thm [display] append_rsp[no_vars]} \noindent Which after unfolding @{term "op \<Longrightarrow>"} is equivalent to: @{thm [display] append_rsp_unfolded[no_vars]} An aggregate relation is defined in terms of relation composition, so we define it first: \begin{definition}[Composition of Relations] @{abbrev "rel_conj R1 R2"} where @{text OO} is the predicate composition @{thm pred_compI[no_vars]} \end{definition} The aggregate relation for an aggregate raw type and quotient type is defined as: \begin{itemize} \item @{text "REL(\<alpha>\<^isub>1, \<alpha>\<^isub>2)"} = @{text "op ="} \item @{text "REL(\<sigma>, \<sigma>)"} = @{text "op ="} \item @{text "REL((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n))\<kappa>, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>n))\<kappa>)"} = @{text "(rel \<kappa>) (REL(\<sigma>\<^isub>1,\<tau>\<^isub>1)) \<dots> (REL(\<sigma>\<^isub>n,\<tau>\<^isub>n))"} \item @{text "REL((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n))\<kappa>\<^isub>1, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>m))\<kappa>\<^isub>2)"} = @{text "(rel \<kappa>\<^isub>1) (REL(\<rho>\<^isub>1,\<nu>\<^isub>1) \<dots> (REL(\<rho>\<^isub>p,\<nu>\<^isub>p) OOO Eqv_\<kappa>\<^isub>2"} provided @{text "\<eta> \<kappa>\<^isub>2 = (\<alpha>\<^isub>1\<dots>\<alpha>\<^isub>p)\<kappa>\<^isub>1 \<and> \<exists>s. s(\<sigma>s\<kappa>\<^isub>1)=\<rho>s\<kappa>\<^isub>1 \<and> s(\<tau>s\<kappa>\<^isub>2)=\<nu>s\<kappa>\<^isub>2"} \end{itemize} Again, the last case is novel, so lets look at the example of respectfullness for @{term concat}. The statement according to the definition above is: @{thm [display] concat_rsp[no_vars]} \noindent By unfolding the definition of relation composition and relation map we can see the equivalent statement just using the primitive list equivalence relation: @{thm [display] concat_rsp_unfolded[of "a" "a'" "b'" "b", no_vars]} The statement reads that, for any lists of lists @{term a} and @{term b} if there exist intermediate lists of lists @{term "a'"} and @{term "b'"} such that each element of @{term a} is in the relation with an appropriate element of @{term a'}, @{term a'} is in relation with @{term b'} and each element of @{term b'} is in relation with the appropriate element of @{term b}.*}subsection {* Preservation *}text {* To be able to lift theorems that talk about constants that are not lifted but whose type changes when lifting is performed additionally preservation theorems are needed. To lift theorems that talk about insertion in lists of lifted types we need to know that for any quotient type with the abstraction and representation functions @{text "Abs"} and @{text Rep} we have: @{thm [display] (concl) cons_prs[no_vars]} This is not enough to lift theorems that talk about quotient compositions. For some constants (for example empty list) it is possible to show a general compositional theorem, but for @{term "op #"} it is necessary to show that it respects the particular quotient type: @{thm [display] insert_preserve2[no_vars]}*}subsection {* Composition of Quotient theorems *}text {* Given two quotients, one of which quotients a container, and the other quotients the type in the container, we can write the composition of those quotients. To compose two quotient theorems we compose the relations with relation composition as defined above and the abstraction and relation functions are the ones of the sub 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 concat}. To be able to lift theorems that talk about it we provide the composition quotient theorems, which then lets us perform the lifting procedure in an unchanged way: @{thm [display] quotient_compose_list[no_vars]}*}section {* Lifting Theorems *}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 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 taking integers or finite sets of characters. To simplify the use of the quotient package we additionally provide an automated statement translation mechanism that replaces occurrences of types that match given quotients by appropriate lifted types. Lifting the theorems is performed in three steps. In the following we call these steps \emph{regularization}, \emph{injection} and \emph{cleaning} following the names used in Homeier's HOL 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, as all three can be performed independently from each other.*}subsection {* Regularization and Injection statements *}text {* We first define the function @{text REG}, which takes the statements of the raw theorem and the lifted theorem (both as terms) and returns the statement of the regularized version. The intuition behind this function is that it replaces quantifiers and abstractions involving raw types by bounded ones, and equalities 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 (\<forall>x : \<sigma>. t, \<forall>x : \<tau>. s) = \<forall>x : \<sigma> \<in> Res (REL (\<sigma>, \<tau>)). REG (t, s)"} \item @{text "REG ((op =) : \<sigma>, (op =) : \<sigma>) = (op =) : \<sigma>"} \item @{text "REG ((op =) : \<sigma>, (op =) : \<tau>) = REL (\<sigma>, \<tau>) : \<sigma>"} \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} In the above definition we ommited 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 the statement of 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))))"} \item @{text "INJ (\<forall> t, \<forall> s) = \<forall> (INJ (t, s)"} \item @{text "INJ (\<forall> t \<in> R, \<forall> s) = \<forall> (INJ (t, s) \<in> R"} \item @{text "INJ (t\<^isub>1 t\<^isub>2, s\<^isub>1 s\<^isub>2) = INJ (t\<^isub>1, s\<^isub>1) INJ (t\<^isub>2, s\<^isub>2)"} \item @{text "INJ (v\<^isub>1 : \<sigma>, v\<^isub>2 : \<sigma>) = v\<^isub>1"} \item @{text "INJ (v\<^isub>1 : \<sigma>, v\<^isub>2 : \<tau>) = REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (v\<^isub>1))"} \item @{text "INJ (c\<^isub>1 : \<sigma>, c\<^isub>2 : \<sigma>) = c\<^isub>1"} \item @{text "INJ (c\<^isub>1 : \<sigma>, c\<^isub>2 : \<tau>) = REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (c\<^isub>1))"} \end{itemize} For existential quantifiers and unique existential quantifiers it is defined similarily to the universal one.*}subsection {* Proof procedure *}(* In the below the type-guiding 'QuotTrue' assumption is removed; since we present in a paper a version with typed-variables it is not necessary *)text {* With the above definitions of @{text "REG"} and @{text "INJ"} we can show how the proof is performed. The first step is always the application of of the following lemma: @{term "[|A; A --> B; B = C; C = D|] ==> D"} With @{text A} instantiated to the original raw theorem, @{text B} instantiated to @{text "REG(A)"}, @{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]}*)subsection {* Injection *}text {* The injection proof starts with an equality between the regularized theorem 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]}*}subsection {* Cleaning *}text {* 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 Peter Homeier's package~\cite{Homeier05} (and related work from there) \item John Harrison's one~\cite{harrison-thesis} is the first one to lift theorems but only first order. \item PVS~\cite{PVS:Interpretations} \item MetaPRL~\cite{Nogin02} \item Manually defined quotients in Isabelle/HOL Library (Markus's Quotient\_Type, Dixon's FSet, \ldots) \item Oscar Slotosch defines quotient-type automatically but no lifting~\cite{Slotosch97}. \item PER. And how to avoid it. \item Necessity of Hilbert Choice op and Larry's quotients~\cite{Paulson06} \item Setoids in Coq and \cite{ChicliPS02} \end{itemize}*}section {* Conclusion *}(*<*)end(*>*)