equal
deleted
inserted
replaced
709 @{text [display, indent=10] "(\<approx>\<^isub>\<alpha> \<doublearr> =) bn bn"} |
709 @{text [display, indent=10] "(\<approx>\<^isub>\<alpha> \<doublearr> =) bn bn"} |
710 |
710 |
711 \noindent |
711 \noindent |
712 and the user cannot discharge it---because it is not true. To see this, |
712 and the user cannot discharge it---because it is not true. To see this, |
713 we can just unfold the definition of @{text "\<doublearr>"} \eqref{relfun} |
713 we can just unfold the definition of @{text "\<doublearr>"} \eqref{relfun} |
714 using extensionality to obtain |
714 using extensionally to obtain |
715 |
715 |
716 @{text [display, indent=10] "\<forall>t\<^isub>1 t\<^isub>2. if t\<^isub>1 \<approx>\<^isub>\<alpha> t\<^isub>2 implies bn(t\<^isub>1) = bn(t\<^isub>2)"} |
716 @{text [display, indent=10] "\<forall>t\<^isub>1 t\<^isub>2. if t\<^isub>1 \<approx>\<^isub>\<alpha> t\<^isub>2 implies bn(t\<^isub>1) = bn(t\<^isub>2)"} |
717 |
717 |
718 \noindent |
718 \noindent |
719 In contrast, if we lift a theorem about @{text "append"} to a theorem describing |
719 In contrast, if we lift a theorem about @{text "append"} to a theorem describing |
738 type being quotient. For example, take the @{term "cons"} to |
738 type being quotient. For example, take the @{term "cons"} to |
739 add a pair of natural numbers to a list. The pair of natural numbers |
739 add a pair of natural numbers to a list. The pair of natural numbers |
740 is to become an integer. But we still want to use @{text cons} for |
740 is to become an integer. But we still want to use @{text cons} for |
741 adding integers to lists---just with a different type. |
741 adding integers to lists---just with a different type. |
742 To be able to lift such theorems, we need a \emph{preservation theorem} |
742 To be able to lift such theorems, we need a \emph{preservation theorem} |
743 for @{text cons}. Assuming we have a poplymorphic raw constant |
743 for @{text cons}. Assuming we have a polymorphic raw constant |
744 @{text "c\<^isub>r :: \<sigma>"} and a corresponding quotient constant @{text "c\<^isub>q :: \<tau>"}, |
744 @{text "c\<^isub>r :: \<sigma>"} and a corresponding quotient constant @{text "c\<^isub>q :: \<tau>"}, |
745 then a preservation theorem is as follows |
745 then a preservation theorem is as follows |
746 |
746 |
747 @{text [display, indent=10] "Quotient R\<^bsub>\<alpha>s\<^esub> Abs\<^bsub>\<alpha>s\<^esub> Rep\<^bsub>\<alpha>s\<^esub> implies ABS (\<sigma>, \<tau>) c\<^isub>r = c\<^isub>r"} |
747 @{text [display, indent=10] "Quotient R\<^bsub>\<alpha>s\<^esub> Abs\<^bsub>\<alpha>s\<^esub> Rep\<^bsub>\<alpha>s\<^esub> implies ABS (\<sigma>, \<tau>) c\<^isub>r = c\<^isub>r"} |
748 |
748 |
797 |
797 |
798 section {* Lifting of Theorems\label{sec:lift} *} |
798 section {* Lifting of Theorems\label{sec:lift} *} |
799 |
799 |
800 text {* |
800 text {* |
801 |
801 |
802 The core of a quotient package lifts an original theorem to a lifted |
802 The main purpose of the quotient package is to lifts an theorem over raw |
803 version. We will perform this operation in three phases. In the |
803 types to a theorem over quotient types. We will perform this operation in |
804 following we call these phases \emph{regularization}, |
804 three phases. In the following we call these phases \emph{regularization}, |
805 \emph{injection} and \emph{cleaning} following the names used in |
805 \emph{injection} and \emph{cleaning} following the names Homeier used |
806 Homeier's HOL4 implementation. |
806 in his implementation. |
807 |
807 |
808 Regularization is supposed to change the quantifications and abstractions |
808 Regularization is supposed to change the quantifications and abstractions |
809 in the theorem to quantification over variables that respect the relation |
809 in the theorem to quantification over variables that respect the relation |
810 (definition \ref{def:respects}). Injection is supposed to add @{term Rep} |
810 (definition \ref{def:respects}). Injection is supposed to add @{term Rep} |
811 and @{term Abs} of appropriate types in front of constants and variables |
811 and @{term Abs} of appropriate types in front of constants and variables |