356   \begin{definition}[Respects]

   354   \begin{definition}[Respects]\label{def:respects}

   755   The core of our quotient package takes an original theorem

   752 

   756   involving raw types and a statement of the theorem that

   753   The core of a quotient package lifts an original theorem to a lifted

   757   it is supposed to produce. This is different from existing

   754   version. We will perform this operation in three phases. In the

   758   quotient packages, where only the raw theorems are necessary.

   755   following we call these phases \emph{regularization},

   759   To simplify the use of the quotient package we additionally provide

   756   \emph{injection} and \emph{cleaning} following the names used in

   760   an automated statement translation mechanism which can produce

   757   Homeier's HOL4 implementation.

   761   the latter automatically given a list of quotient types.

   758 

   762   It is possible that a user wants

   759   Regularization is supposed to change the quantifications and abstractions

   763   to lift only some occurrences of a raw type. In this case

   760   in the theorem to quantification over variables that respect the relation

   764   the user specifies the complete lifted goal instead of using the

   761   (definition \ref{def:respects}). Injection is supposed to add @{term Rep}

   765   automated mechanism.

   762   and @{term Abs} of appropriate types in front of constants and variables

   766   Lifting the theorems is performed in three steps. In the following

   763   of the raw type so that they can be replaced by the ones that include the

   767   we call these steps \emph{regularization}, \emph{injection} and

   764   quotient type. Cleaning rewrites the obtained injected theorem with

   768   \emph{cleaning} following the names used in Homeier's HOL4

   765   preservation rules obtaining the desired goal theorem.

   769   implementation.

   766 

   770 

   767   Most quotient packages take only an original theorem involving raw

   771   We first define the statement of the regularized theorem based

   768   types and lift it. The procedure in our package takes both an

   772   on the original theorem and the goal theorem. Then we define

   769   original theorem involving raw types and a statement of the theorem

   773   the statement of the injected theorem, based on the regularized

   770   that it is supposed to produce. To simplify the use of the quotient

   774   theorem and the goal. We then show the 3 proofs, as all three

   771   package we additionally provide an automated statement translation

   775   can be performed independently from each other.

   772   mechanism which can produce the latter automatically given a list of

   776 

   773   quotient types.  It is possible that a user wants to lift only some

   777 *}

   774   occurrences of a raw type. In this case the user specifies the

   778 text {* \textit{Regularization and Injection statements} *}

   775   complete lifted goal instead of using the automated mechanism.

   779 text {*

   776 

   777   In the following we will first define the statement of the

   778   regularized theorem based on the original theorem and the goal

   779   theorem. Then we define the statement of the injected theorem, based

   780   on the regularized theorem and the goal. We then show the 3 proofs,

   781   all three can be performed independently from each other.

   832   For existential quantifiers and unique existential quantifiers it is

   834   \noindent where the cases for existential quantifiers and unique existential

   833   defined similarly to the universal one.

   835   quantifiers have been omitted for clarity; are similar to universal quantifier.

   834 

   836 

   835 *}

   837   We can now define the subgoals that will imply the lifted theorem. Given

   836 text {*\textit{Proof Procedure}*}

   838   the statement of the original theorem @{term t} and the statement of the

   837 

   839   goal @{term g} the regularization subgoal is @{term "t \<longrightarrow> REG(t, g)"},

   838 (* In the below the type-guiding 'QuotTrue' assumption is removed. We need it

   840   the injection subgoal is @{term "REG(t, g) = INJ(REG(t, g), g)"} and the

   839    only for bound variables without types, while in the paper presentation

   841   cleaning subgoal is @{term "INJ(REG(t, g), g) = g"}. We will now describe

   840    variables are typed *)

   842   the three tactics provided for these three subgoals.

   841 

   842 text {*

   843 

   844   When lifting a theorem we first apply the following rule

   845 

   846   @{term [display, indent=10] "[|A; A --> B; B = C; C = D|] ==> D"}

   847 

   848   \noindent

   849   with @{text A} instantiated to the original raw theorem, 

   850        @{text B} instantiated to @{text "REG(A)"},

   851        @{text C} instantiated to @{text "INJ(REG(A))"},

   852    and @{text D} instantiated to the statement of the lifted theorem.

   853   The first assumption can be immediately discharged using the original

   854   theorem and the three left subgoals are exactly the subgoals of regularization,

   855   injection and cleaning. The three can be proved independently by the

   856   framework and in case there are non-solved subgoals they can be left

   857   to the user.

   870 *}

   855   In the proof of the regularization subgoal we always start with an implication.

   871 text {* \textit{Proving Regularization} *}

   872 text {*

   873 

   897 *}

   879 

   898 text {* \textit{Proving Rep/Abs Injection} *}

   899 

   900 (*

   901   @{thm bex_reg_eqv_range[no_vars]}

   902   @{thm [display] bex_reg_left[no_vars]}

   903   @{thm [display] bex1_bexeq_reg[no_vars]}

   904   @{thm [display] bex_reg_eqv[no_vars]}

   905   @{thm [display] babs_reg_eqv[no_vars]}

   906   @{thm [display] babs_simp[no_vars]}

   907 *)

   908 

   909 text {*

   920   Otherwise the two terms are applications. There are two cases: If there is a REP/ABS

   901   The cleaning subgoal has been defined in such a way that

   921   in the injected theorem we can use the theorem:

   902   establishing the goal theorem now consists only on rewriting the

   922 

   903   injected theorem with the preservation theorems and quotient

   923   @{thm [display, indent=10] rep_abs_rsp[no_vars]}

   904   definitions. First for all lifted constants, their definitions

   924 

   905   are used to fold the @{term Rep} with the raw constant. Next for

   925   \noindent

   906   all lambda abstractions and quantifications the lambda and

   926   and continue the proof.

   907   quantifier preservation theorems are used to replace the

   927 

   908   variables that include raw types with respects by quantification

   928   Otherwise we introduce an appropriate relation between the subterms and continue with

   909   over variables that include quotient types. We show here only

   929   two subgoals using the lemma:

   910   the lambda preservation theorem; assuming

   930 

   911   @{term "Quotient R1 Abs1 Rep1"} and @{term "Quotient R2 Abs2 Rep2"}

   931   @{thm [display, indent=10] apply_rsp[no_vars]}

   912   we have:

   932 

   913 

   933 *}

   914     @{thm [display, indent=10] (concl) lambda_prs[no_vars]}

   934 text {* \textit{Cleaning} *}

   915 

   935 text {*

   916   \noindent

   936 

   917   holds. Next relations over lifted types are folded to equality.

   937   The @{text REG} and @{text INJ} functions have been defined in such a way

   918   The following theorem has been shown in Homeier~\cite{Homeier05}:

   938   that establishing the goal theorem now consists only on rewriting the

   919 

   939   injected theorem with the preservation theorems.

   920     @{thm [display, indent=10] (concl) Quotient_rel_rep[no_vars]}

   940 

   921 

   941   \begin{itemize}

   922   \noindent

   942   \item First for lifted constants, their definitions are the preservation rules for

   923   Finally the user given preservation theorems, that allow using

   943     them.

   924   higher level operations and containers of types being lifted.

   944   \item For lambda abstractions lambda preservation establishes

   925   We show the preservation theorem for @{term map}. Again assuming

   945     the equality between the injected theorem and the goal. This allows both

   926   that @{term "Quotient R1 Abs1 Rep1"} and @{term "Quotient R2 Abs2 Rep2"}

   946     abstraction and quantification over lifted types.

   927   we have:

   947     @{thm [display] (concl) lambda_prs[no_vars]}

   928 

   948   \item Relations over lifted types are folded with:

   929   @{thm [display, indent=10] (concl) map_prs(1)[of R1 Abs1 Rep1 R2 Abs2 Rep2,no_vars]}

   949     @{thm [display] (concl) Quotient_rel_rep[no_vars]}

   950   \item User given preservation theorems, that allow using higher level operations

   951     and containers of types being lifted. An example may be

   952     @{thm [display] (concl) map_prs(1)[of R1 Abs1 Rep1 R2 Abs2 Rep2,no_vars]}

   953   \end{itemize}