854 regularized theorem based on @{text "raw_thm"} and |
854 regularized theorem based on @{text "raw_thm"} and |
855 @{text "quot_thm"}. Then we define the statement of the injected theorem, based |
855 @{text "quot_thm"}. Then we define the statement of the injected theorem, based |
856 on @{text "reg_thm"} and @{text "quot_thm"}. We then show the three proof steps, |
856 on @{text "reg_thm"} and @{text "quot_thm"}. We then show the three proof steps, |
857 which can all be performed independently from each other. |
857 which can all be performed independently from each other. |
858 |
858 |
859 We first define the function @{text REG}, which takes terms of the |
859 We first define the function @{text REG}, which takes the terms of the |
860 @{text "raw_thm"} and @{text "quot_thm"} as input and returns |
860 @{text "raw_thm"} and @{text "quot_thm"} as input and returns |
861 @{text "reg_thm"}. The intuition |
861 @{text "reg_thm"}. The idea |
862 behind this function is that it replaces quantifiers and |
862 behind this function is that it replaces quantifiers and |
863 abstractions involving raw types by bounded ones, and equalities |
863 abstractions involving raw types by bounded ones, and equalities |
864 involving raw types are replaced by appropriate aggregate |
864 involving raw types by appropriate aggregate |
865 equivalence relations. It is defined by simultaneously recursing on |
865 equivalence relations. It is defined by simultaneously recursing on |
866 the structure of @{text "raw_thm"} and @{text "quot_thm"} as follows: |
866 the structure of @{text "raw_thm"} and @{text "quot_thm"} as follows: |
867 |
867 |
868 \begin{center} |
868 \begin{center} |
869 \begin{tabular}{rcl} |
869 \begin{tabular}{rcl} |
991 variables that include raw types with respects by quantifiers |
991 variables that include raw types with respects by quantifiers |
992 over variables that include quotient types. We show here only |
992 over variables that include quotient types. We show here only |
993 the lambda preservation theorem. Given |
993 the lambda preservation theorem. Given |
994 @{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: |
994 @{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: |
995 |
995 |
996 @{thm [display, indent=10] (concl) lambda_prs[of _ "Abs\<^isub>1" "Rep\<^isub>1" "Abs\<^isub>2" "Rep\<^isub>2", no_vars]} |
996 @{thm [display, indent=10] (concl) lambda_prs[of _ "Abs\<^isub>1" "Rep\<^isub>1" _ "Abs\<^isub>2" "Rep\<^isub>2", no_vars]} |
997 |
997 |
998 \noindent |
998 \noindent |
999 Next, relations over lifted types are folded to equalities. |
999 Next, relations over lifted types are folded to equalities. |
1000 For this the following theorem has been shown by Homeier~\cite{Homeier05}: |
1000 For this the following theorem has been shown by Homeier~\cite{Homeier05}: |
1001 |
1001 |