nominal2: comparison Quotient-Paper/Paper.thy

equal deleted inserted replaced

-:63f0e7f914dd
+:1341a2d7570f
 \noindent
 Using extensionality and unfolding the definition of @{text "\<singlearr>"},
 we can get back to \eqref{adddef}.
 In what follows we shall use the convention to write @{text "map_\<kappa>"} for a map-function
-of the type-constructor @{text \<kappa>}. In our implementation we maintain
+of the type-constructor @{text \<kappa>}. For a type @{text \<kappa>} with arguments @{text "\<alpha>\<^isub>1\<^isub>\<dots>\<^isub>n"} the
+type of @{text "map_\<kappa>"} has to be @{text "\<alpha>\<^isub>1\<Rightarrow>\<dots>\<Rightarrow>\<alpha>\<^isub>n\<Rightarrow>\<alpha>\<^isub>1\<dots>\<alpha>\<^isub>n \<kappa>"}. For example @{text "map_list"}
+has to have the type @{text "\<alpha>\<Rightarrow>\<alpha> list"}.
+In our implementation we maintain
 a database of these map-functions that can be dynamically extended.
 It will also be necessary to have operators, referred to as @{text "rel_\<kappa>"},
 which define equivalence relations in terms of constituent equivalence
 relations. For example given two equivalence relations @{text "R\<^isub>1"}
 relations, abstraction and representation functions:
 \begin{definition}[Quotient Types]
 Given a relation $R$, an abstraction function $Abs$
 and a representation function $Rep$, the predicate @{term "Quotient R Abs Rep"}
-means
+holds if and only if
 \begin{enumerate}
 \item @{thm (rhs1) Quotient_def[of "R", no_vars]}
 \item @{thm (rhs2) Quotient_def[of "R", no_vars]}
 \item @{thm (rhs3) Quotient_def[of "R", no_vars]}
 \end{enumerate}
 holds if and only if there exists a @{text y} such that @{thm (prem 1) pred_compI[of "R\<^isub>1" "x" "y" "R\<^isub>2" "z"]} and
 @{thm (prem 2) pred_compI[of "R\<^isub>1" "x" "y" "R\<^isub>2" "z"]}.
 \end{definition}
 \noindent
-Unfortunately, there are two predicaments with compositions of relations.
+Unfortunately a general quotient theorem for @{text "\<circ>\<circ>\<circ>"}, analogous to the one
-First, a general quotient theorem for @{text "\<circ>\<circ>\<circ>"}, like the one for @{text "\<singlearr>"}
+for @{text "\<singlearr>"} given in Proposition \ref{funquot}, would not be true
-given in Proposition \ref{funquot},
+in general. It cannot even be stated inside HOL, because of restrictions on types.
-cannot be stated inside HOL, because of restrictions on types.
+However, we can prove specific instances of a
-Second, even if we were able to state such a quotient theorem, it
-would not be true in general. However, we can prove specific instances of a
 quotient theorem for composing particular quotient relations.
 For example, to lift theorems involving @{term flat} the quotient theorem for
 composing @{text "\<approx>\<^bsub>list\<^esub>"} will be necessary: given @{term "Quotient R Abs Rep"}
 with @{text R} being an equivalence relation, then
 \noindent
 The first one declares zero for integers and the second the operator for
 building unions of finite sets (@{text "flat"} having the type
 @{text "(\<alpha> list) list \<Rightarrow> \<alpha> list"}).
-The problem for us is that from such declarations we need to derive proper
+From such declarations given by the user, the quotient package needs to derive proper
 definitions using @{text "Abs"} and @{text "Rep"}. The data we rely on is the given quotient type
 @{text "\<tau>"} and the raw type @{text "\<sigma>"}.  They allow us to define \emph{aggregate
 abstraction} and \emph{representation functions} using the functions @{text "ABS (\<sigma>,
 \<tau>)"} and @{text "REP (\<sigma>, \<tau>)"} whose clauses we shall give below. The idea behind
 these two functions is to simultaneously descend into the raw types @{text \<sigma>} and
 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
 \isacommand{lemma}~~@{text "add_pair_zero: int_rel (add_pair (0, 0) x) x"}
 \end{isabelle}
 \noindent
-If the user lifts this theorem, all proof obligations are
+If the user lifts this theorem, the quotient package performs all the lifting
-automatically discharged, except the respectfulness
+automatically leaving the respectfulness proof for the constant @{text "add_pair"}
-proof for @{text "add_pair"}:
+as the only remaining proof obligation. This property needs to be proved by the user:
 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
 \begin{tabular}{@ {}l}
 \isacommand{lemma}~~@{text "[quot_respect]:"}\\
 @{text "(int_rel \<doublearr> int_rel \<doublearr> int_rel) add_pair add_pair"}
 \end{tabular}
 \end{isabelle}
 \noindent
-This property needs to be proved by the user. It
+It can be discharged automatically by Isabelle when hinting to unfold the definition
-can be discharged automatically by Isabelle when hinting to unfold the definition
 of @{text "\<doublearr>"}.
 After this, the user can prove the lifted lemma as follows:
 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
 \isacommand{lemma}~~@{text "0 + (x :: int) = x"}~~\isacommand{by}~~@{text "lifting add_pair_zero"}

changeset 2413	1341a2d7570f
parent 2412	63f0e7f914dd
child 2414	67e57fc3cd2a