741 

   741 

   742 

   742 

   743 section {* Lifting of Theorems\label{sec:lift} *}

   743 section {* Lifting of Theorems\label{sec:lift} *}

   744 

   744 

   745 text {*

   745 text {*

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

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

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

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

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

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

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

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

   755   automated mechanism.

   756   automated mechanism.

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

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

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

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

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

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

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

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

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

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

   765   can be performed independently from each other.

   766   can be performed independently from each other.

   766 

   767 

   767 *}

   768 *}

   771 text {*

   770 text {*

   772 

   771 

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

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

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

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

   775   returns the statement of the regularized version. The intuition

   774   returns the statement of the regularized version. The intuition

   823 

   822 

   824   For existential quantifiers and unique existential quantifiers it is

   823   For existential quantifiers and unique existential quantifiers it is

   825   defined similarly to the universal one.

   824   defined similarly to the universal one.

   826 

   825 

   827 *}

   826 *}

   830 

   828 

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

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

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

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

   833    variables are typed *)

   831    variables are typed *)

   834 

   832 

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

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

   858   It does not follow from the fact that @{term "\<not> (0, 0) = (1, 0)"} because

   856   It does not follow from the fact that @{term "\<not> (0, 0) = (1, 0)"} because

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

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

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

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

   861   the classes are not equal is necessary.

   859   the classes are not equal is necessary.

   866 text {*

   863 text {*

   867 

   864 

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

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

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

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

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

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

   886   The last theorem is new in comparison with Homeier's package. There the

   883   The last theorem is new in comparison with Homeier's package. There the

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

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

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

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

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

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

   890   equivalence theorem. This allows separating regularization from injection.

   887   equivalence theorem. This allows separating regularization from injection.

   893 

   890 

   894 (*

   891 (*

   895   @{thm bex_reg_eqv_range[no_vars]}

   892   @{thm bex_reg_eqv_range[no_vars]}

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

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

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

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

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

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

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

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

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

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

   901 *)

   898 *)

   902 

   899 

   905 text {*

   900 text {*

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

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

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

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

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

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

   909 

   904 

   925   two subgoals using the lemma:

   920   two subgoals using the lemma:

   926 

   921 

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

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

   928 

   923 

   929 *}

   924 *}

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

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

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

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

   936   injected theorem with the preservation theorems.

   930   injected theorem with the preservation theorems.

   937 

   931 

   938   \begin{itemize}

   932   \begin{itemize}