594 The need for aggregate map-functions can be seen in cases where we build quotients, |
594 The need for aggregate map-functions can be seen in cases where we build quotients, |
595 say @{text "(\<alpha>, \<beta>) \<kappa>\<^isub>q"}, out of compound raw types, say @{text "(\<alpha> list) \<times> \<beta>"}. |
595 say @{text "(\<alpha>, \<beta>) \<kappa>\<^isub>q"}, out of compound raw types, say @{text "(\<alpha> list) \<times> \<beta>"}. |
596 In this case @{text MAP} generates the |
596 In this case @{text MAP} generates the |
597 aggregate map-function: |
597 aggregate map-function: |
598 |
598 |
|
599 %%% FIXME: Reviewer 2 asks: last two lines defining ABS and REP for |
|
600 %%% unequal type constructors: How are the $\varrho$s defined? The |
|
601 %%% following paragraph mentions them, but this paragraph is unclear, |
|
602 %%% since it then mentions $\alpha$s, which do not seem to be defined |
|
603 %%% either. As a result, I do not understand the first two sentences |
|
604 %%% in this paragraph. I can imagine roughly what the following |
|
605 %%% sentence `The $\sigma$s' are given by the matchers for the |
|
606 %%% $\alpha$s$ when matching $\varrho$s $\kappa$ against $\sigma$s |
|
607 %%% $\kappa$.' means, but also think that it is too vague. |
|
608 |
599 @{text [display, indent=10] "\<lambda>a b. map_prod (map_list a) b"} |
609 @{text [display, indent=10] "\<lambda>a b. map_prod (map_list a) b"} |
600 |
610 |
601 \noindent |
611 \noindent |
602 which is essential in order to define the corresponding aggregate |
612 which is essential in order to define the corresponding aggregate |
603 abstraction and representation functions. |
613 abstraction and representation functions. |
775 to lift such theorems, we need a \emph{preservation property} for @{text |
785 to lift such theorems, we need a \emph{preservation property} for @{text |
776 cons}. Assuming we have a polymorphic raw constant @{text "c\<^isub>r :: \<sigma>"} |
786 cons}. Assuming we have a polymorphic raw constant @{text "c\<^isub>r :: \<sigma>"} |
777 and a corresponding quotient constant @{text "c\<^isub>q :: \<tau>"}, then a |
787 and a corresponding quotient constant @{text "c\<^isub>q :: \<tau>"}, then a |
778 preservation property is as follows |
788 preservation property is as follows |
779 |
789 |
|
790 %%% FIXME: Reviewer 2 asks: You say what a preservation theorem is, |
|
791 %%% but not which preservation theorems you assume. Do you generate a |
|
792 %%% proof obligation for a preservation theorem for each raw constant |
|
793 %%% and its corresponding lifted constant? |
|
794 |
|
795 %%% Cezary: I think this would be a nice thing to do but we have not |
|
796 %%% done it, the theorems need to be 'guessed' from the remaining obligations |
780 |
797 |
781 @{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"} |
798 @{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"} |
782 |
799 |
783 \noindent |
800 \noindent |
784 where the @{text "\<alpha>s"} stand for the type variables in the type of @{text "c\<^isub>r"}. |
801 where the @{text "\<alpha>s"} stand for the type variables in the type of @{text "c\<^isub>r"}. |
838 of the raw type so that they can be replaced by the corresponding constants from the |
855 of the raw type so that they can be replaced by the corresponding constants from the |
839 quotient type. The purpose of cleaning is to bring the theorem derived in the |
856 quotient type. The purpose of cleaning is to bring the theorem derived in the |
840 first two phases into the form the user has specified. Abstractly, our |
857 first two phases into the form the user has specified. Abstractly, our |
841 package establishes the following three proof steps: |
858 package establishes the following three proof steps: |
842 |
859 |
|
860 %%% FIXME: Reviewer 1 complains that the reader needs to guess the |
|
861 %%% meaning of reg_thm and inj_thm, as well as the arguments of REG |
|
862 %%% which are given above. I wouldn't change it. |
|
863 |
843 \begin{center} |
864 \begin{center} |
844 \begin{tabular}{l@ {\hspace{4mm}}l} |
865 \begin{tabular}{l@ {\hspace{4mm}}l} |
845 1.) Regularization & @{text "raw_thm \<longrightarrow> reg_thm"}\\ |
866 1.) Regularization & @{text "raw_thm \<longrightarrow> reg_thm"}\\ |
846 2.) Injection & @{text "reg_thm \<longleftrightarrow> inj_thm"}\\ |
867 2.) Injection & @{text "reg_thm \<longleftrightarrow> inj_thm"}\\ |
847 3.) Cleaning & @{text "inj_thm \<longleftrightarrow> quot_thm"}\\ |
868 3.) Cleaning & @{text "inj_thm \<longleftrightarrow> quot_thm"}\\ |
949 |
970 |
950 \noindent |
971 \noindent |
951 In this definition we again omitted the cases for existential and unique existential |
972 In this definition we again omitted the cases for existential and unique existential |
952 quantifiers. |
973 quantifiers. |
953 |
974 |
|
975 %%% FIXME: Reviewer2 citing following sentence: You mention earlier |
|
976 %%% that this implication may fail to be true. Does that meant that |
|
977 %%% the `first proof step' is a heuristic that proves the implication |
|
978 %%% raw_thm \implies reg_thm in some instances, but fails in others? |
|
979 %%% You should clarify under which circumstances the implication is |
|
980 %%% being proved here. |
|
981 %%% It would be nice to cite Homeiers discussions in the Quotient |
|
982 %%% Package manual from HOL (the longer paper), do you agree? |
|
983 |
954 In the first proof step, establishing @{text "raw_thm \<longrightarrow> reg_thm"}, we always |
984 In the first proof step, establishing @{text "raw_thm \<longrightarrow> reg_thm"}, we always |
955 start with an implication. Isabelle provides \emph{mono} rules that can split up |
985 start with an implication. Isabelle provides \emph{mono} rules that can split up |
956 the implications into simpler implicational subgoals. This succeeds for every |
986 the implications into simpler implicational subgoals. This succeeds for every |
957 monotone connective, except in places where the function @{text REG} replaced, |
987 monotone connective, except in places where the function @{text REG} replaced, |
958 for instance, a quantifier by a bounded quantifier. In this case we have |
988 for instance, a quantifier by a bounded quantifier. In this case we have |
968 |
998 |
969 @{text [display, indent=10] "\<forall>x \<in> Respects R. P x = \<forall>x. P x"} |
999 @{text [display, indent=10] "\<forall>x \<in> Respects R. P x = \<forall>x. P x"} |
970 |
1000 |
971 \noindent |
1001 \noindent |
972 If @{term R\<^isub>2} is an equivalence relation, we can prove that for any predicate @{term P} |
1002 If @{term R\<^isub>2} is an equivalence relation, we can prove that for any predicate @{term P} |
|
1003 |
|
1004 %%% FIXME Reviewer 1 claims the theorem is obviously false so maybe we |
|
1005 %%% should include a proof sketch? |
973 |
1006 |
974 @{thm [display, indent=10] (concl) ball_reg_eqv_range[of R\<^isub>1 R\<^isub>2, no_vars]} |
1007 @{thm [display, indent=10] (concl) ball_reg_eqv_range[of R\<^isub>1 R\<^isub>2, no_vars]} |
975 |
1008 |
976 \noindent |
1009 \noindent |
977 The last theorem is new in comparison with Homeier's package. There the |
1010 The last theorem is new in comparison with Homeier's package. There the |
1028 *} |
1061 *} |
1029 |
1062 |
1030 |
1063 |
1031 section {* Examples \label{sec:examples} *} |
1064 section {* Examples \label{sec:examples} *} |
1032 |
1065 |
1033 (* Mention why equivalence *) |
|
1034 |
|
1035 text {* |
1066 text {* |
|
1067 |
|
1068 %%% FIXME Reviewer 1 would like an example of regularized and injected |
|
1069 %%% statements. He asks for the examples twice, but I would still ignore |
|
1070 %%% it due to lack of space... |
1036 |
1071 |
1037 In this section we will show a sequence of declarations for defining the |
1072 In this section we will show a sequence of declarations for defining the |
1038 type of integers by quotienting pairs of natural numbers, and |
1073 type of integers by quotienting pairs of natural numbers, and |
1039 lifting one theorem. |
1074 lifting one theorem. |
1040 |
1075 |