nominal2: comparison Quotient-Paper/Paper.thy

equal deleted inserted replaced

-:5606de1e5034
+:d769c24094cf
 in particular preservation for quotient
 compositions
 - explain how Quotient R Abs Rep is proved (j-version)
 - give an example where precise specification helps (core Haskell in nominal?)
-- Quote from Peter:
-One might think quotient have been studied to death, but
 - Mention Andreas Lochbiler in Acknowledgements and 'desceding'.
 *)
 notation (latex output)
 rel_conj ("_ \<circ>\<circ>\<circ> _" [53, 53] 52) and
 pred_comp ("_ \<circ>\<circ> _" [1, 1] 30) and
 "op -->" (infix "\<longrightarrow>" 100) and
 "==>" (infix "\<Longrightarrow>" 100) and
-fun_map ("_ \<^raw:\mbox{\singlearr}> _" 51) and
+fun_map ("_ \<singlearr> _" 51) and
-fun_rel ("_ \<^raw:\mbox{\doublearr}> _" 51) and
+fun_rel ("_ \<doublearr> _" 51) and
 list_eq (infix "\<approx>" 50) and (* Not sure if we want this notation...? *)
 fempty ("\<emptyset>") and
 funion ("_ \<union> _") and
 finsert ("{_} \<union> _") and
 Cons ("_::_") and
 concat ("flat") and
-fconcat ("\<Union>")
+fconcat ("\<Union>") and
+Quotient ("Quot _ _ _")
 ML {*
 fun nth_conj n (_, r) = nth (HOLogic.dest_conj r) n;
 \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>}. 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"}
+type of the function @{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>"},
 \begin{definition}[Respects]\label{def:respects}
 An element @{text "x"} respects a relation @{text "R"} provided @{text "R x x"}.
 \end{definition}
-\begin{definition}[Bounded Quantification and Bounded Abstractions]\label{def:babs}
+\begin{definition}[Bounded $\forall$ and $\lambda$]\label{def:babs}
 @{text "\<forall>x \<in> S. P x"} holds if for all @{text x}, @{text "x \<in> S"} implies @{text "P x"};
 and @{text "(\<lambda>x \<in> S. f x) = f x"} provided @{text "x \<in> S"}.
 \end{definition}
 The central definition in Homeier's work \cite{Homeier05} relates equivalence
 \begin{definition}[Quotient Types]
 Given a relation $R$, an abstraction function $Abs$
 and a representation function $Rep$, the predicate @{term "Quotient R Abs Rep"}
 holds if and only if
-\begin{enumerate}
+\begin{isabelle}\ \ \ \ \ %%%%
-\item @{thm (rhs1) Quotient_def[of "R", no_vars]}
+\begin{tabular}{rl}
-\item @{thm (rhs2) Quotient_def[of "R", no_vars]}
+(i) & \begin{isa}@{thm (rhs1) Quotient_def[of "R", no_vars]}\end{isa}\\
-\item @{thm (rhs3) Quotient_def[of "R", no_vars]}
+(ii) & \begin{isa}@{thm (rhs2) Quotient_def[of "R", no_vars]}\end{isa}\\
-\end{enumerate}
+(iii) & \begin{isa}@{thm (rhs3) Quotient_def[of "R", no_vars]}\end{isa}\\
+\end{tabular}
+\end{isabelle}
 \end{definition}
 \noindent
-The value of this definition lies in the fact that validity of @{text "Quotient R Abs Rep"} can
+The value of this definition lies in the fact that validity of @{term "Quotient R Abs Rep"} can
-often be proved in terms of the validity of @{text "Quotient"} over the constituent
+often be proved in terms of the validity of @{term "Quot"} over the constituent
 types of @{text "R"}, @{text Abs} and @{text Rep}.
 For example Homeier proves the following property for higher-order quotient
 types:
 \begin{proposition}\label{funquot}
+\begin{isa}
 @{thm[mode=IfThen] fun_quotient[where ?R1.0="R\<^isub>1" and ?R2.0="R\<^isub>2"
 and ?abs1.0="Abs\<^isub>1" and ?abs2.0="Abs\<^isub>2" and ?rep1.0="Rep\<^isub>1" and ?rep2.0="Rep\<^isub>2"]}
+\end{isa}
 \end{proposition}
 \noindent
 As a result, Homeier is able to build an automatic prover that can nearly
-always discharge a proof obligation involving @{text "Quotient"}. Our quotient
+always discharge a proof obligation involving @{text "Quot"}. Our quotient
 package makes heavy
 use of this part of Homeier's work including an extension
 for dealing with compositions of equivalence relations defined as follows:
 %%% FIXME Referee 2 claims that composition-of-relations means OO, and this is also
 %%% what wikipedia says. Any idea for a different name? Conjugation of Relations?
-\begin{definition}[Composition of Relations]
+\begin{definition}%%[Composition of Relations]
 @{abbrev "rel_conj R\<^isub>1 R\<^isub>2"} where @{text "\<circ>\<circ>"} is the predicate
 composition defined by
 @{thm (concl) pred_compI[of "R\<^isub>1" "x" "y" "R\<^isub>2" "z"]}
 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"]}.
 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
 \begin{isabelle}\ \ \ \ \ %%%
-@{text  "Quotient (rel_list R \<circ>\<circ>\<circ> \<approx>\<^bsub>list\<^esub>) (Abs_fset \<circ> map_list Abs) (map_list Rep \<circ> Rep_fset)"}
+\begin{tabular}{r@ {\hspace{1mm}}l}
+@{text  "Quot"} & @{text "(rel_list R \<circ>\<circ>\<circ> \<approx>\<^bsub>list\<^esub>)"}\\
+& @{text "(Abs_fset \<circ> map_list Abs)"}\\
+& @{text "(map_list Rep \<circ> Rep_fset)"}\\
+\end{tabular}
 \end{isabelle}
 *}
-section {* Quotient Types and Quotient Definitions\label{sec:type} *}
+section {* Quotient Types and Quotient\\ Definitions\label{sec:type} *}
 text {*
 The first step in a quotient construction is to take a name for the new
 type, say @{text "\<kappa>\<^isub>q"}, and an equivalence relation, say @{text R},
 defined over a raw type, say @{text "\<sigma>"}. The type of the equivalence
 respectively.  Given that @{text "R"} is an equivalence relation, the
 following property holds  for every quotient type
 (for the proof see \cite{Homeier05}).
 \begin{proposition}
-@{text "Quotient R Abs_\<kappa>\<^isub>q Rep_\<kappa>\<^isub>q"}.
+@{term "Quotient R Abs_\<kappa>\<^isub>q Rep_\<kappa>\<^isub>q"}.
 \end{proposition}
 The next step in a quotient construction is to introduce definitions of new constants
 involving the quotient type. These definitions need to be given in terms of concepts
 of the raw type (remember this is the only way how to extend HOL
 @{text "ABS (\<sigma>s, \<tau>s)"} to mean @{text "ABS (\<sigma>\<^isub>1, \<tau>\<^isub>1)\<dots>ABS (\<sigma>\<^isub>n, \<tau>\<^isub>n)"}; similarly
 for @{text REP}.
 %
 \begin{center}
 \hfill
-\begin{tabular}{rcl}
+\begin{tabular}{@ {\hspace{2mm}}l@ {}}
-\multicolumn{3}{@ {\hspace{-4mm}}l}{equal types:}\\
+\multicolumn{1}{@ {}l}{equal types:}\\
-@{text "ABS (\<sigma>, \<sigma>)"} & $\dn$ & @{text "id :: \<sigma> \<Rightarrow> \<sigma>"}\\
+@{text "ABS (\<sigma>, \<sigma>)"} $\dn$ @{text "id :: \<sigma> \<Rightarrow> \<sigma>"}\\
-@{text "REP (\<sigma>, \<sigma>)"} & $\dn$ & @{text "id :: \<sigma> \<Rightarrow> \<sigma>"}\smallskip\\
+@{text "REP (\<sigma>, \<sigma>)"} $\dn$ @{text "id :: \<sigma> \<Rightarrow> \<sigma>"}\smallskip\\
-\multicolumn{3}{@ {\hspace{-4mm}}l}{function types:}\\
+\multicolumn{1}{@ {}l}{function types:}\\
-@{text "ABS (\<sigma>\<^isub>1 \<Rightarrow> \<sigma>\<^isub>2, \<tau>\<^isub>1 \<Rightarrow> \<tau>\<^isub>2)"} & $\dn$ & @{text "REP (\<sigma>\<^isub>1, \<tau>\<^isub>1) \<singlearr> ABS (\<sigma>\<^isub>2, \<tau>\<^isub>2)"}\\
+@{text "ABS (\<sigma>\<^isub>1 \<Rightarrow> \<sigma>\<^isub>2, \<tau>\<^isub>1 \<Rightarrow> \<tau>\<^isub>2)"} $\dn$ @{text "REP (\<sigma>\<^isub>1, \<tau>\<^isub>1) \<singlearr> ABS (\<sigma>\<^isub>2, \<tau>\<^isub>2)"}\\
-@{text "REP (\<sigma>\<^isub>1 \<Rightarrow> \<sigma>\<^isub>2, \<tau>\<^isub>1 \<Rightarrow> \<tau>\<^isub>2)"} & $\dn$ & @{text "ABS (\<sigma>\<^isub>1, \<tau>\<^isub>1) \<singlearr> REP (\<sigma>\<^isub>2, \<tau>\<^isub>2)"}\smallskip\\
+@{text "REP (\<sigma>\<^isub>1 \<Rightarrow> \<sigma>\<^isub>2, \<tau>\<^isub>1 \<Rightarrow> \<tau>\<^isub>2)"} $\dn$ @{text "ABS (\<sigma>\<^isub>1, \<tau>\<^isub>1) \<singlearr> REP (\<sigma>\<^isub>2, \<tau>\<^isub>2)"}\smallskip\\
-\multicolumn{3}{@ {\hspace{-4mm}}l}{equal type constructors:}\\
+\multicolumn{1}{@ {}l}{equal type constructors:}\\
-@{text "ABS (\<sigma>s \<kappa>, \<tau>s \<kappa>)"} & $\dn$ & @{text "map_\<kappa> (ABS (\<sigma>s, \<tau>s))"}\\
+@{text "ABS (\<sigma>s \<kappa>, \<tau>s \<kappa>)"} $\dn$ @{text "map_\<kappa> (ABS (\<sigma>s, \<tau>s))"}\\
-@{text "REP (\<sigma>s \<kappa>, \<tau>s \<kappa>)"} & $\dn$ & @{text "map_\<kappa> (REP (\<sigma>s, \<tau>s))"}\smallskip\\
+@{text "REP (\<sigma>s \<kappa>, \<tau>s \<kappa>)"} $\dn$ @{text "map_\<kappa> (REP (\<sigma>s, \<tau>s))"}\smallskip\\
-\multicolumn{3}{@ {\hspace{-4mm}}l}{unequal type constructors with @{text "\<alpha>s
+\multicolumn{1}{@ {}l}{unequal type constructors:}\\
-\<kappa>\<^isub>q"} being the quotient of the raw type @{text "\<rho>s \<kappa>"}:}\\
+@{text "ABS (\<sigma>s \<kappa>, \<tau>s \<kappa>\<^isub>q)"} $\dn$ @{text "Abs_\<kappa>\<^isub>q \<circ> (MAP(\<rho>s \<kappa>) (ABS (\<sigma>s', \<tau>s)))"}\\
-@{text "ABS (\<sigma>s \<kappa>, \<tau>s \<kappa>\<^isub>q)"} & $\dn$ & @{text "Abs_\<kappa>\<^isub>q \<circ> (MAP(\<rho>s \<kappa>) (ABS (\<sigma>s', \<tau>s)))"}\\
+@{text "REP (\<sigma>s \<kappa>, \<tau>s \<kappa>\<^isub>q)"} $\dn$ @{text "(MAP(\<rho>s \<kappa>) (REP (\<sigma>s', \<tau>s))) \<circ> Rep_\<kappa>\<^isub>q"}
-@{text "REP (\<sigma>s \<kappa>, \<tau>s \<kappa>\<^isub>q)"} & $\dn$ & @{text "(MAP(\<rho>s \<kappa>) (REP (\<sigma>s', \<tau>s))) \<circ> Rep_\<kappa>\<^isub>q"}
 \end{tabular}\hfill\numbered{ABSREP}
 \end{center}
 %
 \noindent
 In the last two clauses we rely on the fact that the type @{text "\<alpha>s
 @{text "\<rho>s \<kappa>"}.  The
 function @{text "MAP"} calculates an \emph{aggregate map-function} for a raw
 type as follows:
 %
 \begin{center}
-\begin{tabular}{rcl}
+\begin{tabular}{r@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
 @{text "MAP' (\<alpha>)"} & $\dn$ & @{text "a\<^sup>\<alpha>"}\\
 @{text "MAP' (\<kappa>)"} & $\dn$ & @{text "id :: \<kappa> \<Rightarrow> \<kappa>"}\\
 @{text "MAP' (\<sigma>s \<kappa>)"} & $\dn$ & @{text "map_\<kappa> (MAP'(\<sigma>s))"}\smallskip\\
 @{text "MAP (\<sigma>)"} & $\dn$ & @{text "\<lambda>as. MAP'(\<sigma>)"}
 \end{tabular}
 @{text "(\<alpha> list) list \<Rightarrow> \<alpha> list"} and the quotient type @{text "(\<alpha> fset) fset \<Rightarrow> \<alpha>
 fset"}. Feeding these types into @{text ABS} gives us (after some @{text "\<beta>"}-simplifications)
 the abstraction function
 \begin{isabelle}\ \ \ \ \ %%%
-@{text "(map_list (map_list id \<circ> Rep_fset) \<circ> Rep_fset) \<singlearr> Abs_fset \<circ> map_list id"}
+\begin{tabular}{l}
+@{text "(map_list (map_list id \<circ> Rep_fset) \<circ> Rep_fset) \<singlearr>"}\\
+\mbox{}\hspace{4.5cm}@{text " Abs_fset \<circ> map_list id"}
+\end{tabular}
 \end{isabelle}
 \noindent
 In our implementation we further
 simplify this function by rewriting with the usual laws about @{text
 equivalent to @{text "\<sigma>s \<kappa> \<Rightarrow> \<rho>s[\<tau>s] \<kappa>"}, which we just have to compose with
 @{text "\<rho>s[\<tau>s] \<kappa> \<Rightarrow> \<tau>s \<kappa>\<^isub>q"} according to the type of @{text "\<circ>"}.\qed
 \end{proof}
 *}
-section {* Respectfulness and Preservation \label{sec:resp} *}
+section {* Respectfulness and\\ Preservation \label{sec:resp} *}
 text {*
 The main point of the quotient package is to automatically ``lift'' theorems
 involving constants over the raw type to theorems involving constants over
 the quotient type. Before we can describe this lifting process, we need to impose
 lifting. The reason is that even if definitions for all raw constants
 can be given, \emph{not} all theorems can be lifted to the quotient type. Most
 notable is the bound variable function, that is the constant @{text bn}, defined
 for raw lambda-terms as follows
-\begin{isabelle}\ \ \ \ \ %%%
+\begin{isabelle}
+\begin{center}
 @{text "bn (x) \<equiv> \<emptyset>"}\hspace{4mm}
-@{text "bn (t\<^isub>1 t\<^isub>2) \<equiv> bn (t\<^isub>1) \<union> bn (t\<^isub>2)"}\hspace{4mm}
+@{text "bn (t\<^isub>1 t\<^isub>2) \<equiv> bn (t\<^isub>1) \<union> bn (t\<^isub>2)"}\smallskip\\
 @{text "bn (\<lambda>x. t) \<equiv> {x} \<union> bn (t)"}
+\end{center}
 \end{isabelle}
 \noindent
 We can generate a definition for this constant using @{text ABS} and @{text REP}.
 But this constant does \emph{not} respect @{text "\<alpha>"}-equivalence and
 quotient equivalence relations in places where the types differ and equalities
 elsewhere.
 \begin{center}
 \hfill
-\begin{tabular}{rcl}
+\begin{tabular}{l}
-\multicolumn{3}{@ {\hspace{-4mm}}l}{equal types:}\\
+\multicolumn{1}{@ {}l}{equal types:}\\
-@{text "REL (\<sigma>, \<sigma>)"} & $\dn$ & @{text "= :: \<sigma> \<Rightarrow> \<sigma> \<Rightarrow> bool"}\smallskip\\
+@{text "REL (\<sigma>, \<sigma>)"} $\dn$ @{text "= :: \<sigma> \<Rightarrow> \<sigma> \<Rightarrow> bool"}\smallskip\\
-\multicolumn{3}{@ {\hspace{-4mm}}l}{equal type constructors:}\\
+\multicolumn{1}{@ {}l}{equal type constructors:}\\
-@{text "REL (\<sigma>s \<kappa>, \<tau>s \<kappa>)"} & $\dn$ & @{text "rel_\<kappa> (REL (\<sigma>s, \<tau>s))"}\smallskip\\
+@{text "REL (\<sigma>s \<kappa>, \<tau>s \<kappa>)"} $\dn$ @{text "rel_\<kappa> (REL (\<sigma>s, \<tau>s))"}\smallskip\\
-\multicolumn{3}{@ {\hspace{-4mm}}l}{unequal type constructors with @{text "\<alpha>s
+\multicolumn{1}{@ {}l}{unequal type constructors:}\\
-\<kappa>\<^isub>q"} being the quotient of the raw type @{text "\<rho>s \<kappa>"}:}\smallskip\\
+@{text "REL (\<sigma>s \<kappa>, \<tau>s \<kappa>\<^isub>q)"} $\dn$ @{text "rel_\<kappa>\<^isub>q (REL (\<sigma>s', \<tau>s))"}\\
-@{text "REL (\<sigma>s \<kappa>, \<tau>s \<kappa>\<^isub>q)"} & $\dn$ & @{text "rel_\<kappa>\<^isub>q (REL (\<sigma>s', \<tau>s))"}\\
 \end{tabular}\hfill\numbered{REL}
 \end{center}
 \noindent
 The @{text "\<sigma>s'"} in the last clause are calculated as in \eqref{ABSREP}:
-we know that type @{text "\<alpha>s \<kappa>\<^isub>q"} is the quotient of the raw type
+again we know that type @{text "\<alpha>s \<kappa>\<^isub>q"} is the quotient of the raw type
 @{text "\<rho>s \<kappa>"}. The @{text "\<sigma>s'"} are the substitutions for @{text "\<alpha>s"} obtained by matching
 @{text "\<rho>s \<kappa>"} and @{text "\<sigma>s \<kappa>"}.
 Let us return to the lifting procedure of theorems. Assume we have a theorem
 that contains the raw constant @{text "c\<^isub>r :: \<sigma>"} and which we want to
 involving raw types by appropriate aggregate
 equivalence relations. It is defined by simultaneously recursing on
 the structure of  @{text "raw_thm"} and @{text "quot_thm"} as follows:
 \begin{center}
-\begin{tabular}{rcl}
+\begin{tabular}{l}
-\multicolumn{3}{@ {}l}{abstractions:}\smallskip\\
+\multicolumn{1}{@ {}l}{abstractions:}\smallskip\\
-@{text "REG (\<lambda>x\<^sup>\<sigma>. t, \<lambda>x\<^sup>\<tau>. s)"} & $\dn$ &
+@{text "REG (\<lambda>x\<^sup>\<sigma>. t, \<lambda>x\<^sup>\<tau>. s)"} $\dn$
 $\begin{cases}
 @{text "\<lambda>x\<^sup>\<sigma>. REG (t, s)"} \quad\mbox{provided @{text "\<sigma> = \<tau>"}}\\
 @{text "\<lambda>x\<^sup>\<sigma> \<in> Respects (REL (\<sigma>, \<tau>)). REG (t, s)"}
 \end{cases}$\smallskip\\
 \\
-\multicolumn{3}{@ {}l}{universal quantifiers:}\\
+\multicolumn{1}{@ {}l}{universal quantifiers:}\\
-@{text "REG (\<forall>x\<^sup>\<sigma>. t, \<forall>x\<^sup>\<tau>. s)"} & $\dn$ &
+@{text "REG (\<forall>x\<^sup>\<sigma>. t, \<forall>x\<^sup>\<tau>. s)"} $\dn$
 $\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\\
+\multicolumn{1}{@ {}l}{equality:}\smallskip\\
 %% REL of two equal types is the equality so we do not need a separate case
-@{text "REG (=\<^bsup>\<sigma>\<Rightarrow>\<sigma>\<Rightarrow>bool\<^esup>, =\<^bsup>\<tau>\<Rightarrow>\<tau>\<Rightarrow>bool\<^esup>)"} & $\dn$ & @{text "REL (\<sigma>, \<tau>)"}\\\smallskip\\
+@{text "REG (=\<^bsup>\<sigma>\<Rightarrow>\<sigma>\<Rightarrow>bool\<^esup>, =\<^bsup>\<tau>\<Rightarrow>\<tau>\<Rightarrow>bool\<^esup>)"} $\dn$ @{text "REL (\<sigma>, \<tau>)"}\\\smallskip\\
-\multicolumn{3}{@ {}l}{applications, variables and constants:}\\
+\multicolumn{1}{@ {}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 (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 (x\<^isub>1, x\<^isub>2)"} $\dn$ @{text "x\<^isub>1"}\\
-@{text "REG (c\<^isub>1, c\<^isub>2)"} & $\dn$ & @{text "c\<^isub>1"}\\
+@{text "REG (c\<^isub>1, c\<^isub>2)"} $\dn$ @{text "c\<^isub>1"}\\
 \end{tabular}
 \end{center}
 %
 \noindent
 In the above definition we omitted the cases for existential quantifiers
 Next we define the function @{text INJ} which takes as argument
 @{text "reg_thm"} and @{text "quot_thm"} (both as
 terms) and returns @{text "inj_thm"}:
 \begin{center}
-\begin{tabular}{rcl}
+\begin{tabular}{l}
-\multicolumn{3}{@ {\hspace{-4mm}}l}{abstractions:}\\
+\multicolumn{1}{@ {}l}{abstractions:}\\
-@{text "INJ (\<lambda>x. t :: \<sigma>, \<lambda>x. s :: \<tau>) "} & $\dn$ &
+@{text "INJ (\<lambda>x. t :: \<sigma>, \<lambda>x. s :: \<tau>) "} $\dn$\\
-$\begin{cases}
+\hspace{18mm}$\begin{cases}
 @{text "\<lambda>x. INJ (t, s)"} \quad\mbox{provided @{text "\<sigma> = \<tau>"}}\\
 @{text "REP (\<sigma>, \<tau>) (ABS (\<sigma>, \<tau>) (\<lambda>x. INJ (t, s)))"}
-\end{cases}$\\
+\end{cases}$\smallskip\\
-@{text "INJ (\<lambda>x \<in> R. t :: \<sigma>, \<lambda>x. s :: \<tau>) "} & $\dn$
+@{text "INJ (\<lambda>x \<in> R. t :: \<sigma>, \<lambda>x. s :: \<tau>) "} $\dn$\\
-& @{text "REP (\<sigma>, \<tau>) (ABS (\<sigma>, \<tau>) (\<lambda>x \<in> R. INJ (t, s)))"}\smallskip\\
+\hspace{18mm}@{text "REP (\<sigma>, \<tau>) (ABS (\<sigma>, \<tau>) (\<lambda>x \<in> R. INJ (t, s)))"}\smallskip\\
-\multicolumn{3}{@ {\hspace{-4mm}}l}{universal quantifiers:}\\
+\multicolumn{1}{@ {}l}{universal quantifiers:}\\
-@{text "INJ (\<forall> t, \<forall> s) "} & $\dn$ & @{text "\<forall> INJ (t, s)"}\\
+@{text "INJ (\<forall> t, \<forall> s) "} $\dn$ @{text "\<forall> INJ (t, s)"}\\
-@{text "INJ (\<forall> t \<in> R, \<forall> s) "} & $\dn$ & @{text "\<forall> INJ (t, s) \<in> R"}\smallskip\\
+@{text "INJ (\<forall> t \<in> R, \<forall> s) "} $\dn$ @{text "\<forall> INJ (t, s) \<in> R"}\smallskip\\
-\multicolumn{3}{@ {\hspace{-4mm}}l}{applications, variables and constants:}\smallskip\\
+\multicolumn{1}{@ {}l}{applications, variables and constants:}\smallskip\\
-@{text "INJ (t\<^isub>1 t\<^isub>2, s\<^isub>1 s\<^isub>2) "} & $\dn$ & @{text " INJ (t\<^isub>1, s\<^isub>1) INJ (t\<^isub>2, s\<^isub>2)"}\\
+@{text "INJ (t\<^isub>1 t\<^isub>2, s\<^isub>1 s\<^isub>2) "} $\dn$ @{text " INJ (t\<^isub>1, s\<^isub>1) INJ (t\<^isub>2, s\<^isub>2)"}\\
-@{text "INJ (x\<^isub>1\<^sup>\<sigma>, x\<^isub>2\<^sup>\<tau>) "} & $\dn$ &
+@{text "INJ (x\<^isub>1\<^sup>\<sigma>, x\<^isub>2\<^sup>\<tau>) "} $\dn$
 $\begin{cases}
 @{text "x\<^isub>1"} \quad\mbox{provided @{text "\<sigma> = \<tau>"}}\\
 @{text "REP (\<sigma>, \<tau>) (ABS (\<sigma>, \<tau>) x\<^isub>1)"}\\
 \end{cases}$\\
-@{text "INJ (c\<^isub>1\<^sup>\<sigma>, c\<^isub>2\<^sup>\<tau>) "} & $\dn$ &
+@{text "INJ (c\<^isub>1\<^sup>\<sigma>, c\<^isub>2\<^sup>\<tau>) "} $\dn$
 $\begin{cases}
 @{text "c\<^isub>1"} \quad\mbox{provided @{text "\<sigma> = \<tau>"}}\\
 @{text "REP (\<sigma>, \<tau>) (ABS (\<sigma>, \<tau>) c\<^isub>1)"}\\
 \end{cases}$\\
 \end{tabular}

changeset 2444	d769c24094cf
parent 2443	5606de1e5034
child 2445	10148a447359