723 behind this function is that it replaces quantifiers and |
723 behind this function is that it replaces quantifiers and |
724 abstractions involving raw types by bounded ones, and equalities |
724 abstractions involving raw types by bounded ones, and equalities |
725 involving raw types are replaced by appropriate aggregate |
725 involving raw types are replaced by appropriate aggregate |
726 relations. It is defined as follows: |
726 relations. It is defined as follows: |
727 |
727 |
728 \begin{itemize} |
728 \begin{center} |
729 \item @{text "REG (\<lambda>x : \<sigma>. t, \<lambda>x : \<sigma>. s) = \<lambda>x : \<sigma>. REG (t, s)"} |
729 \begin{tabular}{rcl} |
730 \item @{text "REG (\<lambda>x : \<sigma>. t, \<lambda>x : \<tau>. s) = \<lambda>x : \<sigma> \<in> Res (REL (\<sigma>, \<tau>)). REG (t, s)"} |
730 \multicolumn{3}{@ {\hspace{-4mm}}l}{abstractions (with same types and different types):}\\ |
731 \item @{text "REG (\<forall>x : \<sigma>. t, \<forall>x : \<sigma>. s) = \<forall>x : \<sigma>. REG (t, s)"} |
731 @{text "REG (\<lambda>x : \<sigma>. t, \<lambda>x : \<sigma>. s)"} & $\dn$ & @{text "\<lambda>x : \<sigma>. REG (t, s)"}\\ |
732 \item @{text "REG (\<forall>x : \<sigma>. t, \<forall>x : \<tau>. s) = \<forall>x : \<sigma> \<in> Res (REL (\<sigma>, \<tau>)). REG (t, s)"} |
732 @{text "REG (\<lambda>x : \<sigma>. t, \<lambda>x : \<tau>. s)"} & $\dn$ & @{text "\<lambda>x : \<sigma> \<in> Res (REL (\<sigma>, \<tau>)). REG (t, s)"}\\ |
733 \item @{text "REG ((op =) : \<sigma>, (op =) : \<sigma>) = (op =) : \<sigma>"} |
733 \multicolumn{3}{@ {\hspace{-4mm}}l}{quantification (over same types and different types):}\\ |
734 \item @{text "REG ((op =) : \<sigma>, (op =) : \<tau>) = REL (\<sigma>, \<tau>) : \<sigma>"} |
734 @{text "REG (\<forall>x : \<sigma>. t, \<forall>x : \<sigma>. s)"} & $\dn$ & @{text "\<forall>x : \<sigma>. REG (t, s)"}\\ |
735 \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)"} |
735 @{text "REG (\<forall>x : \<sigma>. t, \<forall>x : \<tau>. s)"} & $\dn$ & @{text "\<forall>x : \<sigma> \<in> Res (REL (\<sigma>, \<tau>)). REG (t, s)"}\\ |
736 \item @{text "REG (v\<^isub>1, v\<^isub>2) = v\<^isub>1"} |
736 \multicolumn{3}{@ {\hspace{-4mm}}l}{equalities (with same types and different types):}\\ |
737 \item @{text "REG (c\<^isub>1, c\<^isub>2) = c\<^isub>1"} |
737 @{text "REG ((op =) : \<sigma>, (op =) : \<sigma>)"} & $\dn$ & @{text "(op =) : \<sigma>"}\\ |
738 \end{itemize} |
738 @{text "REG ((op =) : \<sigma>, (op =) : \<tau>)"} & $\dn$ & @{text "REL (\<sigma>, \<tau>) : \<sigma>"}\\ |
|
739 \multicolumn{3}{@ {\hspace{-4mm}}l}{applications, variables, constants:}\\ |
|
740 @{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)"}\\ |
|
741 @{text "REG (v\<^isub>1, v\<^isub>2)"} & $\dn$ & @{text "v\<^isub>1"}\\ |
|
742 @{text "REG (c\<^isub>1, c\<^isub>2)"} & $\dn$ & @{text "c\<^isub>1"}\\ |
|
743 \end{tabular} |
|
744 \end{center} |
739 |
745 |
740 In the above definition we omitted the cases for existential quantifiers |
746 In the above definition we omitted the cases for existential quantifiers |
741 and unique existential quantifiers, as they are very similar to the cases |
747 and unique existential quantifiers, as they are very similar to the cases |
742 for the universal quantifier. |
748 for the universal quantifier. |
743 |
749 |
744 Next we define the function @{text INJ} which takes the statement of |
750 Next we define the function @{text INJ} which takes the statement of |
745 the regularized theorems and the statement of the lifted theorem both as |
751 the regularized theorems and the statement of the lifted theorem both as |
746 terms and returns the statement of the injected theorem: |
752 terms and returns the statement of the injected theorem: |
747 |
753 |
748 \begin{itemize} |
754 \begin{center} |
749 \item @{text "INJ ((\<lambda>x. t) : \<sigma>, (\<lambda>x. s) : \<sigma>) = \<lambda>x. (INJ (t, s)"} |
755 \begin{tabular}{rcl} |
750 \item @{text "INJ ((\<lambda>x. t) : \<sigma>, (\<lambda>x. s) : \<tau>) = REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (\<lambda>x. (INJ (t, s))))"} |
756 \multicolumn{3}{@ {\hspace{-4mm}}l}{abstractions (with same types and different types):}\\ |
751 \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))))"} |
757 @{text "INJ ((\<lambda>x. t) : \<sigma>, (\<lambda>x. s) : \<sigma>) "} & $\dn$ & @{text "\<lambda>x. INJ (t, s)"}\\ |
752 \item @{text "INJ (\<forall> t, \<forall> s) = \<forall> (INJ (t, s)"} |
758 @{text "INJ ((\<lambda>x. t) : \<sigma>, (\<lambda>x. s) : \<tau>) "} & $\dn$ & @{text "REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (\<lambda>x. (INJ (t, s))))"}\\ |
753 \item @{text "INJ (\<forall> t \<in> R, \<forall> s) = \<forall> (INJ (t, s) \<in> R"} |
759 @{text "INJ ((\<lambda>x \<in> R. t) : \<sigma>, (\<lambda>x. s) : \<tau>) "} & $\dn$ & @{text "REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (\<lambda>x \<in> R. (INJ (t, s))))"}\\ |
754 \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)"} |
760 \multicolumn{3}{@ {\hspace{-4mm}}l}{quantification (over same types and different types):}\\ |
755 \item @{text "INJ (v\<^isub>1 : \<sigma>, v\<^isub>2 : \<sigma>) = v\<^isub>1"} |
761 @{text "INJ (\<forall> t, \<forall> s) "} & $\dn$ & @{text "\<forall> (INJ (t, s))"}\\ |
756 \item @{text "INJ (v\<^isub>1 : \<sigma>, v\<^isub>2 : \<tau>) = REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (v\<^isub>1))"} |
762 @{text "INJ (\<forall> t \<in> R, \<forall> s) "} & $\dn$ & @{text "\<forall> INJ (t, s) \<in> R"}\\ |
757 \item @{text "INJ (c\<^isub>1 : \<sigma>, c\<^isub>2 : \<sigma>) = c\<^isub>1"} |
763 \multicolumn{3}{@ {\hspace{-4mm}}l}{applications, variables, constants:}\\ |
758 \item @{text "INJ (c\<^isub>1 : \<sigma>, c\<^isub>2 : \<tau>) = REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (c\<^isub>1))"} |
764 @{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)"}\\ |
759 \end{itemize} |
765 @{text "INJ (v\<^isub>1 : \<sigma>, v\<^isub>2 : \<sigma>) "} & $\dn$ & @{text "v\<^isub>1"}\\ |
|
766 @{text "INJ (v\<^isub>1 : \<sigma>, v\<^isub>2 : \<tau>) "} & $\dn$ & @{text "REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (v\<^isub>1))"}\\ |
|
767 @{text "INJ (c\<^isub>1 : \<sigma>, c\<^isub>2 : \<sigma>) "} & $\dn$ & @{text "c\<^isub>1"}\\ |
|
768 @{text "INJ (c\<^isub>1 : \<sigma>, c\<^isub>2 : \<tau>) "} & $\dn$ & @{text "REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (c\<^isub>1))"}\\ |
|
769 \end{tabular} |
|
770 \end{center} |
760 |
771 |
761 For existential quantifiers and unique existential quantifiers it is |
772 For existential quantifiers and unique existential quantifiers it is |
762 defined similarly to the universal one. |
773 defined similarly to the universal one. |
763 |
774 |
764 *} |
775 *} |
877 \item First for lifted constants, their definitions are the preservation rules for |
888 \item First for lifted constants, their definitions are the preservation rules for |
878 them. |
889 them. |
879 \item For lambda abstractions lambda preservation establishes |
890 \item For lambda abstractions lambda preservation establishes |
880 the equality between the injected theorem and the goal. This allows both |
891 the equality between the injected theorem and the goal. This allows both |
881 abstraction and quantification over lifted types. |
892 abstraction and quantification over lifted types. |
882 @{thm [display] lambda_prs[no_vars]} |
893 @{thm [display] (concl) lambda_prs[no_vars]} |
883 \item Relations over lifted types are folded with: |
894 \item Relations over lifted types are folded with: |
884 @{thm [display] Quotient_rel_rep[no_vars]} |
895 @{thm [display] (concl) Quotient_rel_rep[no_vars]} |
885 \item User given preservation theorems, that allow using higher level operations |
896 \item User given preservation theorems, that allow using higher level operations |
886 and containers of types being lifted. An example may be |
897 and containers of types being lifted. An example may be |
887 @{thm [display] map_prs(1)[of R1 Abs1 Rep1 R2 Abs2 Rep2,no_vars]} |
898 @{thm [display] (concl) map_prs(1)[of R1 Abs1 Rep1 R2 Abs2 Rep2,no_vars]} |
888 \end{itemize} |
899 \end{itemize} |
889 |
900 |
890 Preservation of relations and user given constant preservation lemmas *} |
901 *} |
891 |
902 |
892 section {* Examples *} |
903 section {* Examples *} |
893 |
904 |
894 (* Mention why equivalence *) |
905 (* Mention why equivalence *) |
895 |
906 |