quotient/Manual/quotient.tex

40 \def\HOL{{\small HOL}}
201 We reinterpret this idea for Higher Order Logic (HOL), where types are
206 new types in the HOL logic,
264 Isabelle/HOL
287 HOL
437 its formulation in HOL and its lifting by quotients over alpha-equivalence.
524 represented in HOL as a curried function
589 %in the HOL logic
965 This relationship is defined in the HOL logic as a new predicate:
979 expressed in HOL as
1044 New types may be defined in HOL
1075 The HOL tool
1078 %in the HOL logic
1255 %The axiom in HOL about the behavior of {\tt @} is
1256 {\tt @} satisfies the HOL axiom
1647 {\tt identity\_quotient} function, which takes any HOL type and
1662 quotient theorems and an HOL type, and returns a quotient theorem for
1724 They are created either in the quotient package or in standard HOL.
1821 %are simple type variables in the HOL logic.
2570 provers like HOL which admit the Hilbert choice operator,
2675 {\it func\/} is an HOL term, which must be a single constant, which is the
2678 {\it fixity\/} is the HOL fixity of the new constant being created,
2679 as specified in the HOL structure {\tt Parse}.
2726 polymorphic constants in the HOL logic
2765 for many standard polymorphic operators of those theories in HOL.
2916 the HOL logic.  It also defines the mapping functions between the
2932 %making use of the HOL primitive, {\tt new\_type\_definition}.
2933 All definitions are accomplished as definitional extensions of HOL,
2935 preserve HOL's consistency.
2999 in the HOL logic as the quotient type $\tau / {\it R}$,
3066 Here {\it function} is an HOL term which is a single existing constant
3067 of the HOL logic.
3814 standard polymorphic functions of the HOL logic have been proven already and
4226 standard polymorphic functions of the HOL logic have been proven already and
4431 In order to use this notation, in each HOL session
4836 ! HOL\_ERR  \\
4848 ! HOL\_ERR  \\
4865 ! HOL\_ERR
5065 \section{The Pre-Sigma Calculus in HOL}
5069 HOL supports the definition of new nested mutually recursive types
5072 %(HOL System Description Manual, section 5.2.1).
5073 %as described in section 5.2.1 of the HOL System Description Manual.
5087 %as a definitional extension of the HOL logic.
5210 %and we can use all of the well-developed support in HOL to deal with
5258 \section{The Pure Sigma Calculus in HOL}
5262 We here define the pure sigma calculus in HOL.
5663 within the HOL logic, as intended.
5675 which is a conservative, definitional extension of the HOL logic.
5963 {\it Introduction to HOL.}
6019 {\it Isabelle/HOL.}
6053 `Higher Order Quotients and their Implementation in Isabelle HOL', in