nominal2: comparison Quotient-Paper/Paper.thy

equal deleted inserted replaced

-:58e60df1ff79
+:b29eb13d3f9d
 %%% FIXME: Referee 1 says:
 %%% Diagram is unclear.  Firstly, isn't an existing type a "set (not sets) of raw elements"?
 %%% Secondly, isn't the _set of_ equivalence classes mapped to and from the new type?
 %%% Thirdly, what do the words "non-empty subset" refer to ?
+%%% Cezary: I like the diagram, maybe 'new type' could be outside, but otherwise
+%%% I wouldn't change it.
 \begin{center}
 \mbox{}\hspace{20mm}\begin{tikzpicture}
 %%\draw[step=2mm] (-4,-1) grid (4,1);
 The need for aggregate map-functions can be seen in cases where we build quotients,
 say @{text "(\<alpha>, \<beta>) \<kappa>\<^isub>q"}, out of compound raw types, say @{text "(\<alpha> list) \<times> \<beta>"}.
 In this case @{text MAP} generates  the
 aggregate map-function:
+%%% FIXME: Reviewer 2 asks: last two lines defining ABS and REP for
+%%% unequal type constructors: How are the $\varrho$s defined? The
+%%% following paragraph mentions them, but this paragraph is unclear,
+%%% since it then mentions $\alpha$s, which do not seem to be defined
+%%% either. As a result, I do not understand the first two sentences
+%%% in this paragraph. I can imagine roughly what the following
+%%% sentence `The $\sigma$s' are given by the matchers for the
+%%% $\alpha$s$ when matching $\varrho$s $\kappa$ against $\sigma$s
+%%% $\kappa$.' means, but also think that it is too vague.
 @{text [display, indent=10] "\<lambda>a b. map_prod (map_list a) b"}
 \noindent
 which is essential in order to define the corresponding aggregate
 abstraction and representation functions.
 "\<alpha>"}-equated lambda terms. Homeier formulates the restrictions in terms of
 the properties of \emph{respectfulness} and \emph{preservation}. We have
 to slightly extend Homeier's definitions in order to deal with quotient
 compositions.
+%%% FIXME: Reviewer 3 asks why are the definitions that follow enough to deal
+%%% with quotient composition.
 To formally define what respectfulness is, we have to first define
 the notion of \emph{aggregate equivalence relations} using the function @{text "REL(\<sigma>, \<tau>)"}
 The idea behind this function is to simultaneously descend into the raw types
 @{text \<sigma>} and quotient types @{text \<tau>}, and generate the appropriate
 quotient equivalence relations in places where the types differ and equalities
 to lift such theorems, we need a \emph{preservation property} for @{text
 cons}. Assuming we have a polymorphic raw constant @{text "c\<^isub>r :: \<sigma>"}
 and a corresponding quotient constant @{text "c\<^isub>q :: \<tau>"}, then a
 preservation property is as follows
+%%% FIXME: Reviewer 2 asks: You say what a preservation theorem is,
+%%% but not which preservation theorems you assume. Do you generate a
+%%% proof obligation for a preservation theorem for each raw constant
+%%% and its corresponding lifted constant?
+%%% Cezary: I think this would be a nice thing to do but we have not
+%%% done it, the theorems need to be 'guessed' from the remaining obligations
 @{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"}
 \noindent
 where the @{text "\<alpha>s"} stand for the type variables in the type of @{text "c\<^isub>r"}.
 section {* Lifting of Theorems\label{sec:lift} *}
 text {*
+%%% FIXME Reviewer 3 asks: Section 5 shows the technicalities of
+%%% lifting theorems. But there is no clarification about the
+%%% correctness. A reader would also be interested in seeing some
+%%% discussions about the generality and limitation of the approach
+%%% proposed there
 The main benefit of a quotient package is to lift automatically theorems over raw
 types to theorems over quotient types. We will perform this lifting in
 three phases, called \emph{regularization},
 \emph{injection} and \emph{cleaning} according to procedures in Homeier's ML-code.
 and @{term Abs} of appropriate types in front of constants and variables
 of the raw type so that they can be replaced by the corresponding constants from the
 quotient type. The purpose of cleaning is to bring the theorem derived in the
 first two phases into the form the user has specified. Abstractly, our
 package establishes the following three proof steps:
+%%% FIXME: Reviewer 1 complains that the reader needs to guess the
+%%% meaning of reg_thm and inj_thm, as well as the arguments of REG
+%%% which are given above. I wouldn't change it.
 \begin{center}
 \begin{tabular}{l@ {\hspace{4mm}}l}
 1.) Regularization & @{text "raw_thm \<longrightarrow> reg_thm"}\\
 2.) Injection & @{text "reg_thm \<longleftrightarrow> inj_thm"}\\
 \noindent
 In this definition we again omitted the cases for existential and unique existential
 quantifiers.
+%%% FIXME: Reviewer2 citing following sentence: You mention earlier
+%%% that this implication may fail to be true. Does that meant that
+%%% the `first proof step' is a heuristic that proves the implication
+%%% raw_thm \implies reg_thm in some instances, but fails in others?
+%%% You should clarify under which circumstances the implication is
+%%% being proved here.
+%%% Cezary: It would be nice to cite Homeiers discussions in the
+%%% Quotient Package manual from HOL (the longer paper), do you agree?
 In the first proof step, establishing @{text "raw_thm \<longrightarrow> reg_thm"}, we always
 start with an implication. Isabelle provides \emph{mono} rules that can split up
 the implications into simpler implicational subgoals. This succeeds for every
 monotone connective, except in places where the function @{text REG} replaced,
 for instance, a quantifier by a bounded quantifier. In this case we have
 @{text [display, indent=10] "\<forall>x \<in> Respects R. P x = \<forall>x. P x"}
 \noindent
 If @{term R\<^isub>2} is an equivalence relation, we can prove that for any predicate @{term P}
+%%% FIXME Reviewer 1 claims the theorem is obviously false so maybe we
+%%% should include a proof sketch?
 @{thm [display, indent=10] (concl) ball_reg_eqv_range[of R\<^isub>1 R\<^isub>2, no_vars]}
 \noindent
 The last theorem is new in comparison with Homeier's package. There the
 *}
 section {* Examples \label{sec:examples} *}
-(* Mention why equivalence *)
 text {*
+%%% FIXME Reviewer 1 would like an example of regularized and injected
+%%% statements. He asks for the examples twice, but I would still ignore
+%%% it due to lack of space...
 In this section we will show a sequence of declarations for defining the
 type of integers by quotienting pairs of natural numbers, and
 lifting one theorem.
 only exist in \cite{Homeier05} as ML-code, not included in the paper.
 Like Homeier's, our quotient package can deal with partial equivalence
 relations, but for lack of space we do not describe the mechanisms
 needed for this kind of quotient constructions.
+%%% FIXME Reviewer 3 would like to know more about the lifting in Coq and PVS,
+%%% and some comparison. I don't think we have the space for any additions...
 One feature of our quotient package is that when lifting theorems, the user
 can precisely specify what the lifted theorem should look like. This feature
 is necessary, for example, when lifting an induction principle for two
 lists.  Assuming this principle has as the conclusion a predicate of the

changeset 2429	b29eb13d3f9d
parent 2423	f5cbf74d4ec5
child 2437	319f469b8b67