quotient/Manual/quotient.tex

198 The quotient operation is a standard feature of set theory, where
236 The quotient operation is a standard feature of mathematics,
259 The ubiquity of quotients has recommended their investigation
263 The first to appear was Ton Kalker's 1989 package for HOL88 \cite{Kal89}.
348 The relationship between these \quotient{} relations and their
354 The precise definition of the quotient relationship between the
382 The system is thus extensible, both in terms of new operators, and even
393 The structure of this paper is as follows.  In section \ref{quotientsets}
404 %The quotient extension theorem for function types
414 The next several sections discuss
463 The following description is abstracted from \cite{End77}.
489 The {\it quotient set\/} $S / \mathbin{\sim}$ is defined as
673 The operator definitions
790 The reason involves forming quotients of higher order types, that is,
796 The reason is that not all functions which are elements of the function
890 The resulting
962 The precise definition of this quotient relationship
976 The relationship that {\it R\/} with {\it abs\/} and {\it rep\/}
987 The identity is
992 The traditional construction requires the elements of the
999 %The above definition is a fundamental revision of the notion of quotients.
1011 The user may specify a quotient of a type $\tau$ by a relation $R$
1039 The first follows immediately.
1075 The HOL tool
1126 %(The `${}_c$' is notation.)
1141 %The left conjunct comes directly from Definition \ref{abs_rep_classes}.
1205 The right-to-left implication of the biconditional is trivial.
1219 The functions
1244 The {\tt @} operator
1254 (The {\tt \$} converts an operator to prefix syntax.)
1255 %The axiom in HOL about the behavior of {\tt @} is
1298 The axiom for the {\tt @} operator is
1569 %The definition of the function relation operator is:
1632 The first five functions all take as arguments quotient theorems
1634 to the aggregate type operator.  The last two take an {\tt hol\_type} as
1681 The quotient theorems
1723 The definitions of the above operators are indicated below.
1763 The
1780 The identity quotient map operator is the identity operator
1795 %The map operator definitions
1807 %%The
1967 The equality here is between functions, and by extension, true if
2017 The last conjunct on the right side is equality between functions, so by extension this is
2069 %The equality at the end of the first line is between booleans.
2209 \section{The Axiom of Choice}
2262 The $\iota$-operator yields the single element of a singleton set,
2269 %The $\varepsilon$-operator is weaker than the Axiom of Choice, as
2274 The $\iota$-operator is
2278 %The Hilbert $\varepsilon$-operator
2341 The quotients for new quotient types
2352 The identity quotient is
2392 The critical quotient extension
2421 %The two properties of Definition \ref{quotientdef_ac}
2472 The right conjunct is
2528 The operator $c$ is
2551 The operator $c$ is then taken as ${\tt SND} \circ g$,
2557 The significance of Theorem \ref{hilbertchoice}
2579 The main design presented earlier is much simpler to automate.
2589 The definition of new types corresponding to the quotients of
2594 visible at the higher level.  The logic is simplified.
2683 The
2716 The rest of the arguments refer to the general process of lifting theorems
2773 The function {\tt define\_quotient\_types\_full\_rule}
2841 The ``{\tt std}'' functions may be the easiest to use, providing much of the
2931 %The new type is created by the quotient type package by internally
2944 %The equivalence relation should be
2952 %The user should prove that {\it R\/} is indeed an equivalence relation,
3017 The {\tt define\_quotient\_types} tool proves
3036 The previous section
3068 The new constant {\it fname} is given the fixity specified as {\it fixity};
3073 The definition of the new constant is stored in the current theory
3076 The theorem which is produced as the definition of the new constant
3172 The last four fields of the argument to {\tt define\_quotient\_types}
3173 are lists of theorems.  The last field ({\tt old\_thms})
3177 The meanings of the other three fields
3181 %The theory {\tt quotientTheory} provides a number
3216 The respectfulness of each function involved must be
3251 The two variables {\tt xi} and {\tt yi} may be combined into one,
3253 The antecedent conjunct {\tt $R_i$ xi yi}, which here is {\tt xi = yi},
3258 the user to provide.  The package will compensate by automatically
3274 The function {\tt Var1 : var -> term1} is used to construct
3276 The respectfulness theorem for {\tt Var1} is
3290 The result type is {\tt term1}, so the \quotient{} relation for the
3293 The function {\tt App1 : term1 -> term1 -> term1}
3295 The respectfulness theorem for {\tt App1} is
3303 The first argument has type {\tt term1},
3305 The second argument also has type {\tt term1},
3307 The result type is {\tt term1}, so the \quotient{} relation for the
3310 The function {\tt HEIGHT1 : term1 -> num}
3312 The respectfulness theorem for {\tt HEIGHT1} is
3320 The result type is {\tt num}, which is not being lifted,
3323 The function {\tt FV1 : term1 -> (var -> bool)}
3325 The respectfulness theorem for {\tt FV1} is
3333 The result type is {\tt var -> bool}.
3338 The function {\tt <[ : term1 -> (var \# term1) list -> term1}
3342 The respectfulness theorem for {\tt <[} is
3350 The first argument has type {\tt term1},
3352 The second argument is a substitution, which has type {\tt (var \# term1) list},
3354 The result type is {\tt term1}, so the \quotient{} relation for the
3440 of the function.  The arguments which have types not being lifted
3468 The
3496 The last version has higher order and lesser arity than the
3501 The earlier versions may be easier to understand and prove than the
3523 The equalities are conditioned on the component types being quotients.
3594 The preservation theorem for {\tt NIL} is
3600 The operator {\tt NIL} has polymorphic type {\tt ('a)list}.
3603 The result type is
3606 %The lifted version of this type is
3614 The preservation theorem for {\tt LENGTH} is
3620 The operator {\tt LENGTH} has polymorphic type {\tt ('a)list -> num}.
3623 The argument type is
3630 The result type is
3634 %The lifted versions of these types are
3642 The preservation theorem for {\tt CONS} is
3648 The operator {\tt CONS} has polymorphic type {\tt 'a -> ('a)list -> ('a)list}.
3651 The first argument type is
3658 The second argument type is
3665 The result type is
3672 %The lifted versions of these types are
3677 The preservation theorem for {\tt FST} is
3684 The operator {\tt FST} has polymorphic type {\tt ('a \# 'b) -> 'a}.
3687 The argument type is
3694 The result type is
3701 %The lifted versions of these types are
3706 The preservation theorem for the composition operator {\tt o} is
3715 The operator {\tt o} has type
3720 The first argument type is
3727 The second argument type is
3734 The result type is
3741 %The lifted versions of these types are
3788 proper quotients.  The conditions follow the form
3849 The last version has higher order and lesser arity than the
3852 The earlier versions may be easier to understand and prove than the
3857 % The entire collection of versions is
3987 quotients.  The conditioning is the same as that described
4044 The respectfulness theorem for {\tt NIL} is
4050 The operator {\tt NIL} has polymorphic type {\tt ('a)list}.
4053 The result type is
4056 %The lifted version of this type is
4064 The respectfulness theorem for {\tt LENGTH} is
4071 The operator {\tt LENGTH} has polymorphic type {\tt ('a)list -> num}.
4074 The argument type is
4081 The result type is
4088 %The lifted versions of these types are
4092 The respectfulness theorem for {\tt CONS} is
4100 The operator {\tt CONS} has polymorphic type {\tt 'a -> ('a)list -> ('a)list}.
4103 The first argument type is
4110 The second argument type is
4117 The result type is
4124 %The lifted versions of these types are
4129 The respectfulness theorem for {\tt FST} is
4137 The operator {\tt FST} has polymorphic type {\tt ('a \# 'b) -> 'a}.
4140 The argument type is
4147 The result type is
4154 %The lifted versions of these types are
4158 The respectfulness theorem for the composition operator {\tt o} is
4168 The operator {\tt o} has type
4173 The first argument type is
4180 The second argument type is
4187 The result type is
4194 %The lifted versions of these types are
4215 The last version has higher order and lesser arity than the
4220 The earlier versions may be easier to understand and prove than the
4243 The constants involved must respect
4248 The constants must also be either constants being lifted, or else constants
4275 The first issue is that the normal equality relation ($=$) between elements
4287 The second issue is that the universal and existential quantification
4330 The point is that if such non-respectful functions are considered as
4333 The higher version of the theorem will describe quantification over
4363 The rephrased induction theorem
4415 The first argument {\tt R} is the \quotient{} relation for
4420 %The meaning of
4428 new restricted quantification binder, $\exists$!!.  The parser will translate
4551 The {\tt define\_quotient\_types} tool
4567 The tool recognizes this common case and automatically proves
4590 The proper form is automatically proven and then lifted.
4613 The tool will first automatically prove the proper version:
4637 proper form.  The user should prove the proper version manually
4666 The error message associated with the exception thrown may help localize
4668 The process of the quotient operation may be observed in more detail
4682 The facilities provided so far for higher order quotients are flexible
4717 The associated abstraction function
4797 The polymorphic preservation and respectfulness theorems for all these
4976 \section{The Sigma Calculus}
4980 The untyped sigma calculus was introduced by Abadi and Cardelli in
4994 The pre-sigma calculus contains terms denoting objects and methods.
5017 The form $a.l$ denotes the invocation of the method labelled $l$ in the
5018 object $a$.  The form $a.l \Lleftarrow m$ denotes the update of the object
5020 method $m$.  The form $\varsigma(x)a$ denotes a method with one formal
5053 %actually more deep than might at first appear.  The list structure
5060 %The mutual recursion inherent in these
5065 \section{The Pre-Sigma Calculus in HOL}
5094 The syntax
5128 The definition above goes beyond
5139 The {\tt Hol\_definition} tool automatically compensates for this
5207 %The nested version is advantageous over the larger,
5214 %The constructors for {\tt obj1} and {\tt method1}
5258 \section{The Pure Sigma Calculus in HOL}
5361 The old theorems to be lifted are too many to list, but some will
5388 The tool is able to lift many theorems to the abstract, quotient level.
5439 The following regular version was quietly proven and then lifted:
5476 The following regular version was quietly proven and then lifted:
5676 The package automatically lifts not only types,
5695 The relationship between the lower type and the
5708 The Axiom of Choice was used in this design.  We showed that an alternative
5735 %The size of these grammars means that the number
5934 {\it The\,Lambda\,Calculus,\,Syntax\,and\,Semantics.}