149 |
149 |
150 %%% FIXME: Referee 1 says: |
150 %%% FIXME: Referee 1 says: |
151 %%% Diagram is unclear. Firstly, isn't an existing type a "set (not sets) of raw elements"? |
151 %%% Diagram is unclear. Firstly, isn't an existing type a "set (not sets) of raw elements"? |
152 %%% Secondly, isn't the _set of_ equivalence classes mapped to and from the new type? |
152 %%% Secondly, isn't the _set of_ equivalence classes mapped to and from the new type? |
153 %%% Thirdly, what do the words "non-empty subset" refer to ? |
153 %%% Thirdly, what do the words "non-empty subset" refer to ? |
|
154 |
|
155 %%% Cezary: I like the diagram, maybe 'new type' could be outside, but otherwise |
|
156 %%% I wouldn't change it. |
154 |
157 |
155 \begin{center} |
158 \begin{center} |
156 \mbox{}\hspace{20mm}\begin{tikzpicture} |
159 \mbox{}\hspace{20mm}\begin{tikzpicture} |
157 %%\draw[step=2mm] (-4,-1) grid (4,1); |
160 %%\draw[step=2mm] (-4,-1) grid (4,1); |
158 |
161 |
985 %%% that this implication may fail to be true. Does that meant that |
988 %%% that this implication may fail to be true. Does that meant that |
986 %%% the `first proof step' is a heuristic that proves the implication |
989 %%% the `first proof step' is a heuristic that proves the implication |
987 %%% raw_thm \implies reg_thm in some instances, but fails in others? |
990 %%% raw_thm \implies reg_thm in some instances, but fails in others? |
988 %%% You should clarify under which circumstances the implication is |
991 %%% You should clarify under which circumstances the implication is |
989 %%% being proved here. |
992 %%% being proved here. |
990 %%% It would be nice to cite Homeiers discussions in the Quotient |
993 %%% Cezary: It would be nice to cite Homeiers discussions in the |
991 %%% Package manual from HOL (the longer paper), do you agree? |
994 %%% Quotient Package manual from HOL (the longer paper), do you agree? |
992 |
995 |
993 In the first proof step, establishing @{text "raw_thm \<longrightarrow> reg_thm"}, we always |
996 In the first proof step, establishing @{text "raw_thm \<longrightarrow> reg_thm"}, we always |
994 start with an implication. Isabelle provides \emph{mono} rules that can split up |
997 start with an implication. Isabelle provides \emph{mono} rules that can split up |
995 the implications into simpler implicational subgoals. This succeeds for every |
998 the implications into simpler implicational subgoals. This succeeds for every |
996 monotone connective, except in places where the function @{text REG} replaced, |
999 monotone connective, except in places where the function @{text REG} replaced, |