771   @{thm [display, indent=10] insert_preserve2[no_vars]}

   771   %%%@ {thm [display, indent=10] insert_preserve2[no_vars]}

   812   (Definition \ref{def:respects} states what respects means). The purpose of injection is supposed to add @{term Rep}

   812   (Definition \ref{def:respects} states what respects means). The purpose of injection is to add @{term Rep}

   815   quotient type. Cleaning rewrites the obtained injected theorem with

   815   quotient type. The purpose of cleaning is to bring the theorem derived in the

   816   preservation rules obtaining the desired goal theorem.

   816   first two phases into the form the user has specified. Abstractly, our

   817 

   817   package establishes the following three proof steps:

   818   Most quotient packages take only an original theorem involving raw

   818 

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

   819   \begin{center}

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

   820   \begin{tabular}{r@ {\hspace{4mm}}l}

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

   821   1.) & @{text "raw_thm \<longrightarrow> reg_thm"}\\

   822   package we additionally provide an automated statement translation

   822   2.) & @{text "reg_thm \<longleftrightarrow> inj_thm"}\\

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

   823   3.) & @{text "inj_thm \<longleftrightarrow> quot_thm"}\\

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

   824   \end{tabular}

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

   825   \end{center}

   826   complete lifted goal instead of using the automated mechanism.

   826 

   827   \noindent

   828   In contrast to other quotient packages, our package requires

   829   the \emph{term} of the @{text "quot_thm"} to be given by the user.\footnote{Though we

   830   also provide a fully automated mode, where the @{text "quot_thm"} is guessed

   831   from @{text "raw_thm"}.} As a result, it is possible that a user can lift only some

   832   occurrences of a raw type. 

   833 

   834   The second and third proof step will always succeed if the appropriate

   835   respectfulness and preservation theorems are given. In contrast, the first

   836   proof step can fail: a theorem given by the user does not always

   837   imply a regularized version and a stronger one needs to be proved. This

   838   is outside of the scope where the quotient package can help. An example

   839   for the failure is the simple statement for integers @{text "0 \<noteq> 1"}.

   840   It does not follow by lifting from the fact that @{text "(0, 0) \<noteq> (1, 0)"}. 

   841   The raw theorem only shows that particular element in the

   842   equivalence classes are not equal. A more general statement saying that

   843   the equivalence classes are not equal is necessary.

   829   regularized theorem based on the original theorem and the goal

   846   regularized theorem based on @{text "raw_thm"} and the 

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

   847   @{text "quot_thm"}. Then we define the statement of the injected theorem, based

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

   848   on @{text "reg_thm"} theorem and @{text "quot_thm"}. We then show the 3 proofs,

   832   all three can be performed independently from each other.

   849   which can all be performed independently from each other.

   833 

   850 

   834   We define the function @{text REG}, which takes the statements

   851   We define the function @{text REG}. The intuition

   835   of the raw theorem and the lifted theorem (both as terms) and

   836   returns the statement of the regularized version. The intuition

   873   Next we define the function @{text INJ} which takes the statement of

   889 

   874   the regularized theorems and the statement of the lifted theorem both as

   890   Next we define the function @{text INJ} which takes as argument

   875   terms and returns the statement of the injected theorem:

   891   @{text "reg_thm"} and @{text "quot_thm"} (both as

   892   terms) and returns @{text "inj_thm"}:

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

   922   \noindent 

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

   923   where again the cases for existential quantifiers and unique existential

   907 

   924   quantifiers have been omitted.

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

   925 

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

   926   In the first proof step, establishing @{text "raw_thm \<longrightarrow> reg_thm"}, we always 

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

   927   start with an implication. Isabelle provides \emph{mono} rules that can split up 

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

   928   the implications into simpler implication subgoals. This succeeds for every

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

   929   monotone connectives, except in places wher the function @{text REG} inserted,

   913   the three tactics provided for these three subgoals.

   930   for example, a quantifier by a bounded quantifier. In this case we have 

   914 

   931   rules of the form

   915   The injection and cleaning subgoals are always solved if the appropriate

   932 

   916   respectfulness and preservation theorems are given. It is not the case

   933   @{text [display, indent=10] "(\<forall>x. R x \<longrightarrow> (P x \<longrightarrow> Q x)) \<longrightarrow> (\<forall>x. P x \<longrightarrow> \<forall>x \<in> R. Q x)"}

   917   with regularization; sometimes a theorem given by the user does not

   934 

   918   imply a regularized version and a stronger one needs to be proved. This

   935   \noindent

   919   is outside of the scope of the quotient package, so such obligations are

   936   They decompose a bounded quantifier on the right-hand side, but are only applicable

   920   left to the user. Take a simple statement for integers @{text "0 \<noteq> 1"}.

   937   if we can prove that

   921   It does not follow from the fact that @{text "(0, 0) \<noteq> (1, 0)"} because

   938 

   922   of regularization. The raw theorem only shows that particular items in the

   939   @{text [display, indent=10] "\<forall>x \<in> Respects R. P x = \<forall>x. P x"}    

   923   equivalence classes are not equal. A more general statement saying that

   940 

   924   the classes are not equal is necessary.

   941   \noindent

   925 

   942   And finally it can be removed anywhere if @{term R\<^isub>2} is an equivalence relation

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

   943   and we can prove

   927   Isabelle provides a set of \emph{mono} rules, that are used to split implications

   928   of similar statements into simpler implication subgoals. These are enhanced

   929   with special quotient theorem in the regularization proof. Below we only show

   930   the versions for the universal quantifier. For the existential quantifier

   931   and abstraction they are analogous.

   932 

   933   First, bounded universal quantifiers can be removed on the right:

   934 

   935   @{thm [display, indent=10] ball_reg_right_unfolded[no_vars]}

   936 

   937   They can be removed anywhere if the relation is an equivalence relation:

   938 

   939   @{thm [display, indent=10] (concl) ball_reg_eqv[no_vars]}

   940 

   941   And finally it can be removed anywhere if @{term R\<^isub>2} is an equivalence relation:

   946   injection procedure would be used to prove goals with such shape, and there

   949   injection procedure would be used to prove such goals, and there

   947   the equivalence assumption would be used. We use the above theorem directly

   950   the assumption about the equivalence relation would be used. We use the above theorem directly,

   948   also for composed relations where the range type is a type for which we know an

   951   because this allows us to completely separate the first and the second

   949   equivalence theorem. This allows separating regularization from injection.

   952   proof step into independent ``units''.

   950 

   953 

   951   The injection proof starts with an equality between the regularized theorem

   954   The secon proof step, establishing @{text "reg_thm \<longleftrightarrow> inj_thm"},  starts with an equality. 

   952   and the injected version. The proof again follows by the structure of the

   955   The proof again follows the structure of the

   953   two terms, and is defined for a goal being a relation between these two terms.

   956   two underlying terms, and is defined for a goal being a relation between these two terms.

   956   \item For two constants, an appropriate constant respectfulness assumption is used.

   959   \item For two constants an appropriate constant respectfulness lemma is applied.

   957   \item For two variables, we use the assumptions proved in regularization.

   960   \item For two variables, we use the assumptions proved in the regularization step.

   958   \item For two abstractions, they are eta-expanded and beta-reduced.

   961   \item For two abstractions, we @{text "\<eta>"}-expand and @{text "\<beta>"}-reduce them.

   959   \item For two applications, if the right side is an application of

   962   \item For two applications, we check that the right-hand side is an application of

   960     @{term Rep} to an @{term Abs} and @{term "Quotient R Rep Abs"} we

   963     @{term Rep} to an @{term Abs} and @{term "Quotient R Rep Abs"}. If yes then we

   961     can reduce the injected pair using the theorem:

   964     can apply the theorem:

   965     otherwise we introduce an appropriate relation between the subterms

   968     Otherwise we introduce an appropriate relation between the subterms

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

   974   We defined the theorem @{text "inj_thm"} in such a way that

   973   establishing the goal theorem now consists only on rewriting the

   975   establishing the equivalence @{text "inj_thm \<longleftrightarrow> quot_thm"} can be

   974   injected theorem with the preservation theorems and quotient

   976   achieved by rewriting @{text "inj_thm"} with the preservation theorems and quotient

   975   definitions. First for all lifted constants, their definitions

   977   definitions. Then all lifted constants, their definitions

   977   all lambda abstractions and quantifications the lambda and

   979   all abstractions and quantifiers the lambda and

   979   variables that include raw types with respects by quantification

   981   variables that include raw types with respects by quantifiers

   981   the lambda preservation theorem; assuming

   983   the lambda preservation theorem. Given

   982   @{term "Quotient R\<^isub>1 Abs\<^isub>1 Rep\<^isub>1"} and @{term "Quotient R\<^isub>2 Abs\<^isub>2 Rep\<^isub>2"}

   984   @{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:

   983   hold, we have:

   985 

   984 

   986     @{thm [display, indent=10] (concl) lambda_prs[of _ "Abs\<^isub>1" "Rep\<^isub>1" "Abs\<^isub>2" "Rep\<^isub>2", no_vars]}

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

   987 

   986 

   988   \noindent

   987   \noindent

   989   Next, relations over lifted types are folded to equalities.

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

   990   For this the following theorem has been shown in Homeier~\cite{Homeier05}:

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

   994   Finally the user given preservation theorems, that allow using

   995   Finally, we rewrite with the preservation theorems. This will result

   995   higher level operations and containers of types being lifted.

   996   in two equal terms that can be solved by reflexivity.

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

   997   that @{term "Quotient R\<^isub>1 Abs\<^isub>1 Rep\<^isub>1"} and @{term "Quotient R\<^isub>2 Abs\<^isub>2 Rep\<^isub>2"} hold,

   998   we have:

   999 

  1000   @{thm [display, indent=10] (concl) map_prs(1)[of R\<^isub>1 Abs\<^isub>1 Rep\<^isub>1 R\<^isub>2 Abs\<^isub>2 Rep\<^isub>2]}

  1001 

  1012   lifting theorems to integers. Our quotient package is fully compatible with

  1007   lifting theorems to integers. Oeur quotient package is fully compatible with

  1019   the same integer relation as the one presented in the introduction:

  1014   the same integer relation as the one presented in \eqref{natpairequiv}:

  1020 

  1021   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %

  1022   \isacommand{fun}~~@{text "int_rel"}~~\isacommand{where}~~%

  1023   @{text "(m :: nat, n) int_rel (p, q) = (m + q = n + p)"}

  1024   \end{isabelle}

  1025 

  1026   \noindent

  1027   Next the quotient type is defined. This leaves a proof obligation that the

  1028   relation is an equivalence relation which is solved automatically using the

  1029   definitions:

  1030 

  1031   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %

  1032   \isacommand{quotient\_type}~~@{text "int"}~~\isacommand{=}~~@{text "(nat \<times> nat)"}~~\isacommand{/}~~@{text "int_rel"}

  1033   \end{isabelle}

  1034 

  1035   \noindent

  1036   The user can then specify the constants on the quotient type:

  1040   \isacommand{quotient\_definition}~~@{text "0 :: int"}~~\isacommand{is}~~@{text "(0 :: nat, 0 :: nat)"}\\

  1018   \isacommand{fun}~~@{text "int_rel :: (nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"}\\

  1019   \isacommand{where}~~@{text "int_rel (m, n) (p, q) = (m + q = n + p)"}

  1020   \end{tabular}

  1021   \end{isabelle}

  1022 

  1023   \noindent

  1024   Next the quotient type is defined. This generates a proof obligation that the

  1025   relation is an equivalence relation, which is solved automatically using the

  1026   definition and extensionality:

  1027 

  1028   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %

  1029   \begin{tabular}{@ {}l}

  1030   \isacommand{quotient\_type}~~@{text "int"}~~\isacommand{=}~~@{text "(nat \<times> nat)"}~~\isacommand{/}~~@{text "int_rel"}\\

  1031   \hspace{5mm}@{text "by (auto simp add: equivp_def expand_fun_eq)"}

  1032   \end{tabular}

  1033   \end{isabelle}

  1034 

  1035   \noindent

  1036   The user can then specify the constants on the quotient type:

  1037 

  1038   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %

  1039   \begin{tabular}{@ {}l}

  1040   \isacommand{quotient\_definition}~~@{text "0 :: int"}~~\isacommand{is}~~@{text "(0 :: nat, 0 :: nat)"}\\[3mm]

  1049   Lets first take a simple theorem about addition on the raw level:

  1049   The following theorem about addition on the raw level can be proved.

  1056   When the user tries to lift a theorem about integer addition, the respectfulness

  1056   If the user attempts to lift this theorem, all proof obligations are 

  1057   proof obligation is left, so let us prove it first:

  1057   automatically discharged, except the respectfulness

  1058   proof for @{text "plus_raw"}:

  1060   \isacommand{lemma}~~@{text "[quot_respect]: 

  1061   \begin{tabular}{@ {}l}

  1062   \isacommand{lemma}~~@{text "[quot_respect]:\\ 

  1062   \end{isabelle}

  1064   \end{tabular}

  1063 

  1065   \end{isabelle}

  1064   \noindent

  1066 

  1065   Can be proved automatically by the system just by unfolding the definition

  1067   \noindent

  1068   This can be dischaged automatically by Isabelle when telling it to unfold the definition

  1067   Now the user can either prove a lifted lemma explicitly:

  1070   After this, the user can prove the lifted lemma explicitly:

  1074   Or in this simple case use the automated translation mechanism:

  1077   or by the completely automated mode by stating:

  1081   obtaining the same result.

  1084   Both methods give the same result, namely

  1085 

  1086   @{text [display, indent=10] "0 + x = x"}

  1087 

  1088   \noindent

  1089   Although seemingly simple, arriving at this result without the help of a quotient

  1090   package requires substantial reasoning effort.