798   abstractions involving raw types by bounded ones, and equalities

   798   abstractions involving raw types by bounded ones, and equalities

   799   involving raw types are replaced by appropriate aggregate

   799   involving raw types are replaced by appropriate aggregate

   800   equivalence relations. It is defined as follows:

   800   equivalence relations. It is defined as follows:

   801 

   801 

   802   \begin{center}

   802   \begin{center}

   814   @{text "REG (t\<^isub>1 t\<^isub>2, s\<^isub>1 s\<^isub>2)"} & $\dn$ & @{text "REG (t\<^isub>1, s\<^isub>1) REG (t\<^isub>2, s\<^isub>2)"}\\

   823   @{text "REG (t\<^isub>1 t\<^isub>2, s\<^isub>1 s\<^isub>2)"} & $\dn$ & @{text "REG (t\<^isub>1, s\<^isub>1) REG (t\<^isub>2, s\<^isub>2)"}\\

   818   \end{center}

   827   \end{center}

   820   In the above definition we omitted the cases for existential quantifiers

   830   In the above definition we omitted the cases for existential quantifiers

   821   and unique existential quantifiers, as they are very similar to the cases

   831   and unique existential quantifiers, as they are very similar to the cases

   822   for the universal quantifier.

   832   for the universal quantifier.

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

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

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

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

   825   terms and returns the statement of the injected theorem:

   835   terms and returns the statement of the injected theorem:

   826 

   836 

   827   \begin{center}

   837   \begin{center}

   828   \begin{tabular}{rcl}

   838   \begin{tabular}{rcl}

   837   @{text "INJ (t\<^isub>1 t\<^isub>2, s\<^isub>1 s\<^isub>2) "} & $\dn$ & @{text " INJ (t\<^isub>1, s\<^isub>1) INJ (t\<^isub>2, s\<^isub>2)"}\\

   851   @{text "INJ (t\<^isub>1 t\<^isub>2, s\<^isub>1 s\<^isub>2) "} & $\dn$ & @{text " INJ (t\<^isub>1, s\<^isub>1) INJ (t\<^isub>2, s\<^isub>2)"}\\

   842   \end{tabular}

   862   \end{tabular}

   843   \end{center}

   863   \end{center}

   844 

   864 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   864   the classes are not equal is necessary.

   884   the classes are not equal is necessary.

   865 

   885 

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

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

   876 

   896 

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

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

   878 

   898 

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

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

   880 

   900 

   884 

   904 

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

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

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

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

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

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

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

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

   903     @{term [display, indent=10] "R x y \<longrightarrow> R x (Rep (Abs y))"}

   923     @{term [display, indent=10] "R x y \<longrightarrow> R x (Rep (Abs y))"}

   904 

   924 

   905     otherwise we introduce an appropriate relation between the subterms

   925     otherwise we introduce an appropriate relation between the subterms

   906     and continue with two subgoals using the lemma:

   926     and continue with two subgoals using the lemma:

   907 

   927 

   909 

   929 

   910   \end{itemize}

   930   \end{itemize}

   911 

   931 

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

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

   913   establishing the goal theorem now consists only on rewriting the

   933   establishing the goal theorem now consists only on rewriting the

   917   all lambda abstractions and quantifications the lambda and

   937   all lambda abstractions and quantifications the lambda and

   918   quantifier preservation theorems are used to replace the

   938   quantifier preservation theorems are used to replace the

   919   variables that include raw types with respects by quantification

   939   variables that include raw types with respects by quantification

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

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

   921   the lambda preservation theorem; assuming

   941   the lambda preservation theorem; assuming

   924 

   944 

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

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

   926 

   946 

   927   \noindent

   947   \noindent

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

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

   932 

   952 

   933   \noindent

   953   \noindent

   934   Finally the user given preservation theorems, that allow using

   954   Finally the user given preservation theorems, that allow using

   935   higher level operations and containers of types being lifted.

   955   higher level operations and containers of types being lifted.

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

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

   938   we have:

   958   we have:

   939 

   959 

   941 

   961 

   942   *}

   962   *}

   943 

   963 

   944 section {* Examples *}

   964 section {* Examples *}

   945 

   965 

   957   A user of our quotient package first needs to define a relation on

   977   A user of our quotient package first needs to define a relation on

   958   the raw type, by which the quotienting will be performed. We give

   978   the raw type, by which the quotienting will be performed. We give

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

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

   960 

   980 

   961   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %

   981   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %

   963   \end{isabelle}

   984   \end{isabelle}

   964 

   985 

   965   \noindent

   986   \noindent

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

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

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

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

   974   \noindent

   995   \noindent

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

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

   976 

   997 

   977   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %

   998   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %

   978   \begin{tabular}{@ {}l}

   999   \begin{tabular}{@ {}l}

   982   \end{tabular}

  1005   \end{tabular}

   983   \end{isabelle}

  1006   \end{isabelle}

   984 

  1007 

   985   \noindent

  1008   \noindent

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

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

   992   \noindent

  1015   \noindent

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

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

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

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

   995 

  1018 

   996   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %

  1019   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %

   998   \end{isabelle}

  1022   \end{isabelle}

   999 

  1023 

  1000   \noindent

  1024   \noindent

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

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

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

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

  1004 

  1028 

  1005   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %

  1029   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %

  1006   \isacommand{lemma}~~@{text "0 + (x :: int) = x"}~~\isacommand{by}~~@{text "lifting plus_zero_raw"}

  1030   \isacommand{lemma}~~@{text "0 + (x :: int) = x"}~~\isacommand{by}~~@{text "lifting plus_zero_raw"}

  1007   \end{isabelle}

  1031   \end{isabelle}

  1031   of an equivalence checking algorithm for LF \cite{UrbanCheneyBerghofer08},

  1055   of an equivalence checking algorithm for LF \cite{UrbanCheneyBerghofer08},

  1032   Typed Scheme~\cite{TobinHochstadtFelleisen08}, several calculi for

  1056   Typed Scheme~\cite{TobinHochstadtFelleisen08}, several calculi for

  1033   concurrency \cite{BengtsonParow09} and a strong normalisation result for

  1057   concurrency \cite{BengtsonParow09} and a strong normalisation result for

  1034   cut-elimination in classical logic \cite{UrbanZhu08}.

  1058   cut-elimination in classical logic \cite{UrbanZhu08}.

  1035 

  1059 

  1037   defines quotient types for Isabelle/HOL. It did not include theorem lifting.

  1061   defines quotient types for Isabelle/HOL. It did not include theorem lifting.

  1039   lift theorems, however only first order. There is work on quotient types in

  1063   lift theorems, however only first order. There is work on quotient types in

  1040   non-HOL based systems and logical frameworks, namely theory interpretations

  1064   non-HOL based systems and logical frameworks, namely theory interpretations

  1041   in PVS~\cite{PVS:Interpretations}, new types in MetaPRL~\cite{Nogin02}, or

  1065   in PVS~\cite{PVS:Interpretations}, new types in MetaPRL~\cite{Nogin02}, or

  1042   the use of setoids in Coq, with some higher order issues~\cite{ChicliPS02}.

  1066   the use of setoids in Coq, with some higher order issues~\cite{ChicliPS02}.

  1044   Hilbert Choice operator, again only first order~\cite{Paulson06}.

  1068   Hilbert Choice operator, again only first order~\cite{Paulson06}.

  1046   which is the first one to support lifting of higher order theorems.

  1070   which is the first one to support lifting of higher order theorems.

  1047 

  1071 

  1048 

  1072 

  1049   Our quotient package for the first time explore the notion of

  1073   Our quotient package for the first time explore the notion of

  1050   composition of quotients, which allows lifting constants like @{term

  1074   composition of quotients, which allows lifting constants like @{term

  1061   type-classes and locales. This has the advantage over packages

  1085   type-classes and locales. This has the advantage over packages

  1062   requiring big lists as input for the user of being able to develop

  1086   requiring big lists as input for the user of being able to develop

  1063   a theory progressively.

  1087   a theory progressively.

  1064 

  1088 

  1065   We allow lifting only some occurrences of quotiented types, which

  1089   We allow lifting only some occurrences of quotiented types, which

  1067   an attribute, manually with separate tactics for parts of the lifting

  1091   an attribute, manually with separate tactics for parts of the lifting

  1068   procedure, and programatically. Automated definitions of constants

  1092   procedure, and programatically. Automated definitions of constants

  1069   and respectfulness proof obligations are used in Nominal. Finally

  1093   and respectfulness proof obligations are used in Nominal. Finally

  1070   we streamlined and showed the detailed lifting procedure, which

  1094   we streamlined and showed the detailed lifting procedure, which

  1071   has not been presented before.

  1095   has not been presented before.

  1072 

  1096 

  1073   \medskip

  1097   \medskip

  1074   \noindent

  1098   \noindent

  1075   {\bf Acknowledgements:} We would like to thank Peter Homeier for the

  1099   {\bf Acknowledgements:} We would like to thank Peter Homeier for the

  1078 

  1102 

  1079 *}

  1103 *}

  1080 

  1104 

  1081 

  1105 

  1082 

  1106