quotient/Manual/quotient.tex

211 %in particular lists, pairs, sums, options, and function types.
344 of function types.
357 for a function type,
360 for the function's domain and range, are the heart of this paper,
399 their extension for aggregate and function types,
402 for lifting aggregate and function types.
404 %The quotient extension theorem for function types
524 represented in HOL as a curried function
796 The reason is that not all functions which are elements of the function
802 the set of functions from $\tau$ to $\tau$ may contain a function
809 correspond to any function at the abstract quotient level.
844 Any equivalence relation $E^2$ for the function type
884 %Ordinary function application would be intractable.
888 %cannot be fully reflexive if its domain is a function type.
910 abstraction function {\it abs\/}
911 and representation function {\it rep\/}
1002 function type, given quotient theorems for the domain and the range.
1045 using the function {\tt new\_type\_definition}
1048 This function requires us to
1080 %function $\lceil \_ \rceil_c
1082 %and a representation function $\lfloor \_ \rfloor_c
1085 a function
1518 %However, we will see that within the {\tt define\_quotient\_types} function,
1555 In addition, for function types, the following is added:
1569 %The definition of the function relation operator is:
1584 It is reflexive at a function $f$,
1601 necessary quotient theorems for lists, pairs, sums, options, and function types,
1626 %as that returned by the function {\tt define\_quotient\_type}
1647 {\tt identity\_quotient} function, which takes any HOL type and
1649 using equality and the identity function,
1650 %using simple equality ({\tt =}) and the identity function {\tt I},
1660 the {\tt make\_quotient} function takes a list of
1765 function map operator definition is of special interest:
1790 abstraction function, and representation function properly relate together
1810 %%function supports the extension of quotients
1841 %%or earlier in this section for the operator {\tt ===>} for function types,
1856 %yields either an abstraction or representation function
1938 abstraction function ${\it rep}_1$ {\tt -->} ${\it abs}_2$
1939 and representation function
1950 %abstraction function ${\it rep}_1$ {\tt -->} ${\it abs}_2$
1951 %and representation function
1960 % abstraction function ${\it rep}_1$ {\tt -->} ${\it abs}_2$
1961 % and representation function ${\it abs}_1$ {\tt -->} ${\it rep}_2$:
2307 abstraction function {\it abs\/}
2308 % and representation function {\it rep\/}
2344 where the representation function {\it rep\/} is omitted
2411 %If $f{\tt :} \alpha \rightarrow \beta$ is any function,
2412 If $f$ is any function from type $\alpha$ to $\beta$,
2418 with abstraction function $f$ is a quotient ($\langle R,f \rangle$).
2430 If $f$ is any function from type $\alpha$ to $\beta$, and $Q$ is any
2433 then there exists a function $g$ such that
2445 Assuming the function quotient extension theorem
2520 there exists a function $g$ such that
2547 Therefore there exists a function $g$ such that
2559 this point, it is not possible to prove the function quotient extension
2750 A similar function,
2753 and returns an SML function of type {\tt thm -> thm}.
2763 to the list, pair, sum, option, and function type operators, along with
2770 %This function is limited to a single quotient type, but may be
2773 The function {\tt define\_quotient\_types\_full\_rule}
2847 the {\tt define\_quotient\_types\_std} function
2864 the following function is also provided:
2880 %This function is limited to a single quotient type, but may be
2883 This function is defined in terms of {\tt define\_quotient\_types} as
2912 the function {\tt define\_quotient\_types} creates new quotient types.
3058 func \ \ \ \ = {\it function}, \\
3065 as a lifted version of the existing constant {\it function}.
3066 Here {\it function} is an HOL term which is a single existing constant
3183 %many common operators for lists, products, sums, options, and function types.
3204 considered as a function,
3216 The respectfulness of each function involved must be
3274 The function {\tt Var1 : var -> term1} is used to construct
3293 The function {\tt App1 : term1 -> term1 -> term1}
3294 is used to construct terms which are applications of a function to an argument.
3310 The function {\tt HEIGHT1 : term1 -> num}
3323 The function {\tt FV1 : term1 -> (var -> bool)}
3338 The function {\tt <[ : term1 -> (var \# term1) list -> term1}
3440 of the function.  The arguments which have types not being lifted
3445 function is of a type being lifted or not.  There is a direct one-to-one
3457 arguments and the value returned by a function are all of types
3459 for that function.
3461 Also, where a function has an argument of an aggregate type,
3520 equality between the value of the function applied to arguments of
3521 lifted types, and the lifted version of the value of the same function
3551 ({\tt C} is a curried function of $k$ arguments, with a return value of
3560 ({\tt C'} is a curried function of $k$ arguments, with a return value of
3585 may be the identity function {\tt I}, in which case they disappear,
3609 the abstraction function
3627 the representation function
3637 the abstraction function
3655 the representation function
3662 the representation function
3669 the abstraction function
3691 the representation function
3698 the abstraction function
3724 the representation function
3731 the representation function
3738 the abstraction function
3748 %the third argument is {\tt 'a}, for which the representation function
3750 %abstraction function is {\tt abs3}.  This choice would give rise to
3781 express the use of each polymorphic function at the
3791 instead of for a specific type.  If the function is polymorphic in more
3817 polymorphic function not covered by these, the corresponding
3918 % function application & & & {\tt APPLY\_PRS} & {\tt APPLY\_RSP} \\
4022 ({\tt C} is a curried function of $k$ arguments, with a return value of
4229 polymorphic function not covered by these, the corresponding respectfulness
4276 of a lower type is a function that does not respect the equivalence
4292 In particular, quantification over function types
4315 For example, consider the particular function {\tt P1} defined by
4337 {\bf no} corresponding function at the higher level.  So the statement of the
4449 the function existence theorem proposed by Gordon and
4663 and the associated relation and map function simplification theorems
4672 function it returns may be applied to candidate lower theorems individually
4691 new type is used here, but sets are represented by the function type
4695 function.  Nevertheless, it is helpful and intuitive at times to think
4706 function quotient extension theorem, where the domain is the base type of $R$
4717 The associated abstraction function
4719 and the associated representation function
5070 by the {\tt Hol\_datatype} function in the
5085 %All of the type definition, constructor function definition, and
5125 It also creates associated theorems for induction, function existance,
5135 the {\tt OBJ1} constructor function, the type {\tt method1} is nested,
5436 operator, which is higher-order, taking a function as an argument.
5500 Finally, the most difficult theorem to lift is the function existance
5504 where the unique existance is not of a simple function,
5698 is characterized by the \quotient{} relation, the abstraction function,
5699 and the representation function.