nominal2: comparison Quotient-Paper/Paper.thy

equal deleted inserted replaced

-:229660b9f2fc
+:0f3c497fb3b0
 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.
+%%% FIXME: First-order ones exist, for example in HOL-Light the lift_theorem function
+%%% takes all the prerequisites and one single theorem to lift.
 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?
+%%% FIXME the example is gone from the paper? Maybe we can just put it here?
 *}
 section {* Quotient Types and Quotient Definitions\label{sec:type} *}
 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 connective, except in places wher the function @{text REG} inserted,
+monotone connective, except in places where 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)"}
 text {*
 In this section we will show, a complete interaction with the quotient package
 for defining the type of integers by quotienting pairs of natural numbers and
-lifting theorems to integers. Oeur quotient package is fully compatible with
+lifting theorems to integers. Our quotient package is fully compatible with
 Isabelle type classes, but for clarity we will not use them in this example.
 In a larger formalization of integers using the type class mechanism would
 provide many algebraic properties ``for free''.
 A user of our quotient package first needs to define a relation on
 (int_rel \<doublearr> int_rel \<doublearr> int_rel) plus_raw plus_raw"}
 \end{tabular}
 \end{isabelle}
 \noindent
-This can be dischaged automatically by Isabelle when telling it to unfold the definition
+This can be discharged automatically by Isabelle when telling it to unfold the definition
 of @{text "\<doublearr>"}.
 After this, the user can prove the lifted lemma explicitly:
 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
 \isacommand{lemma}~~@{text "0 + (x :: int) = x"}~~\isacommand{by}~~@{text "lifting plus_zero_raw"}
 quotients in theorem provers.
 Slotosch~\cite{Slotosch97} implemented a mechanism that automatically
 defines quotient types for Isabelle/HOL. But he did not include theorem lifting.
 Harrison's quotient package~\cite{harrison-thesis} is the first one that is
 able to automatically lift theorems, however only first-order theorems (that is theorems
-where abstractions, quantifiers and variables do not involve the quotient type).
+where abstractions, quantifiers and variables do not involve functions that
+include the quotient type).
 There is also some work on quotient types in
 non-HOL based systems and logical frameworks, including theory interpretations
 in PVS~\cite{PVS:Interpretations}, new types in MetaPRL~\cite{Nogin02},
 and setoids in Coq \cite{ChicliPS02}.
 Paulson showed a construction of quotients that does not require the
-Hilbert Choice operator, but also only first-order theorems to be lifted~\cite{Paulson06}.
+Hilbert Choice operator, but also only first-order theorems can be lifted~\cite{Paulson06}.
 The most related work to our package is the package for HOL4 by Homeier~\cite{Homeier05}.
 He introduced most of the abstract notions about quotients and also deals with the
 lifting of higher-order theorems. However, he cannot deal with quotient compositions (needed
 for lifting theorems about @{text flat}. Also, a number of his definitions, like @{text ABS},
 @{text REP} and @{text INJ} etc only exist in ML-code. On the other hand, Homeier

changeset 2281	0f3c497fb3b0
parent 2280	229660b9f2fc
child 2282	fab7f09dda22