nominal2: comparison Quotient-Paper/Paper.thy

equal deleted inserted replaced

-:2cbcdaba795a
+:229660b9f2fc
 In addition we are able to address the criticism by Paulson \cite{Paulson06} cited
 at the beginning of this section about having to collect theorems that are
 lifted from the raw level to the quotient level into one giant list. Our
 quotient package is the first one that is modular so that it allows to lift
+%%% FIXME: First-order ones exist, HOL-Light one lifts theorems separately.
 single theorems separately. This has the advantage for the user of being able to develop a
 formal theory interactively as a natural progression. A pleasing side-result of
 the modularity is that we are able to clearly specify what is involved
 in the lifting process (this was only hinted at in \cite{Homeier05} and
 implemented as a ``rough recipe'' in ML-code).
 cannot be stated inside HOL, because of the restriction on types.
 Second, even if we were able to state such a quotient theorem, it
 would not be true in general. However, we can prove specific and useful
 instances of the quotient theorem. We will
 show an example in Section \ref{sec:resp}.
+%%% FIXME the example is gone from the paper?
 *}
 section {* Quotient Types and Quotient Definitions\label{sec:type} *}
 The raw theorem only shows that particular element in the
 equivalence classes are not equal. A more general statement saying that
 the equivalence classes are not equal is necessary.
 In the following we will first define the statement of the
-regularized theorem based on @{text "raw_thm"} and the
+regularized theorem based on @{text "raw_thm"} and
 @{text "quot_thm"}. Then we define the statement of the injected theorem, based
 on @{text "reg_thm"} theorem and @{text "quot_thm"}. We then show the 3 proofs,
 which can all be performed independently from each other.
 We define the function @{text REG}. The intuition
 $\begin{cases}
 @{text "\<forall>x\<^sup>\<sigma>. REG (t, s)"} \quad\mbox{provided @{text "\<sigma> = \<tau>"}}\\
 @{text "\<forall>x\<^sup>\<sigma> \<in> Respects (REL (\<sigma>, \<tau>)). REG (t, s)"}
 \end{cases}$\smallskip\\
 \multicolumn{3}{@ {}l}{equality:}\smallskip\\
-@{text "REG (=\<^bsup>\<sigma>\<Rightarrow>\<sigma>\<Rightarrow>bool\<^esup>, =\<^bsup>\<tau>\<Rightarrow>\<tau>\<Rightarrow>bool\<^esup>)"} & $\dn$ &
+%% REL of two equal types is the equality so we do not need a separate case
-$\begin{cases}
+@{text "REG (=\<^bsup>\<sigma>\<Rightarrow>\<sigma>\<Rightarrow>bool\<^esup>, =\<^bsup>\<tau>\<Rightarrow>\<tau>\<Rightarrow>bool\<^esup>)"} & $\dn$ & @{text "REL (\<sigma>, \<tau>)"}\\\smallskip\\
-@{text "="} \quad\mbox{provided @{text "\<sigma> = \<tau>"}}\\
-@{text "REL (\<sigma>, \<tau>)"}\\
-\end{cases}$\\
 \multicolumn{3}{@ {}l}{applications, variables and constants:}\\
 @{text "REG (t\<^isub>1 t\<^isub>2, s\<^isub>1 s\<^isub>2)"} & $\dn$ & @{text "REG (t\<^isub>1, s\<^isub>1) REG (t\<^isub>2, s\<^isub>2)"}\\
 @{text "REG (x\<^isub>1, x\<^isub>2)"} & $\dn$ & @{text "x\<^isub>1"}\\
 @{text "REG (c\<^isub>1, c\<^isub>2)"} & $\dn$ & @{text "c\<^isub>1"}\\[-5mm]
 \end{longtable}
 quantifiers have been omitted.
 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 implication subgoals. This succeeds for every
-monotone connectives, except in places wher the function @{text REG} inserted,
+monotone connective, except in places wher the function @{text REG} inserted,
 for example, a quantifier by a bounded quantifier. In this case we have
 rules of the form
 @{text [display, indent=10] "(\<forall>x. R x \<longrightarrow> (P x \<longrightarrow> Q x)) \<longrightarrow> (\<forall>x. P x \<longrightarrow> \<forall>x \<in> R. Q x)"}
 \noindent
-They decompose a bounded quantifier on the right-hand side, but are only applicable
+They decompose a bounded quantifier on the right-hand side. We can decompose a
-if we can prove that
+bounded quantifier anywhere if R is an equivalence relation or
+if it is a relation over function types with the range being an equivalence
+relation. If @{text R} is an equivalence relation we can prove that
 @{text [display, indent=10] "\<forall>x \<in> Respects R. P x = \<forall>x. P x"}
 \noindent
-And finally it can be removed anywhere if @{term R\<^isub>2} is an equivalence relation
+And when @{term R\<^isub>2} is an equivalence relation and we can prove
-and we can prove
 @{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
 injection procedure would be used to prove such goals, and there
 the assumption about the equivalence relation would be used. We use the above theorem directly,
 because this allows us to completely separate the first and the second
 proof step into independent ``units''.
-The secon proof step, establishing @{text "reg_thm \<longleftrightarrow> inj_thm"},  starts with an equality.
+The second proof step, establishing @{text "reg_thm \<longleftrightarrow> inj_thm"},  starts with an equality.
 The proof again follows the structure of the
 two underlying terms, and is defined for a goal being a relation between these two terms.
 \begin{itemize}
 \item For two constants an appropriate constant respectfulness lemma is applied.

changeset 2280	229660b9f2fc
parent 2279	2cbcdaba795a
child 2281	0f3c497fb3b0