diff options
Diffstat (limited to 'prover_snapshots/hol4/lib/lem/lem_basic_classesScript.sml')
| -rw-r--r-- | prover_snapshots/hol4/lib/lem/lem_basic_classesScript.sml | 503 |
1 files changed, 503 insertions, 0 deletions
diff --git a/prover_snapshots/hol4/lib/lem/lem_basic_classesScript.sml b/prover_snapshots/hol4/lib/lem/lem_basic_classesScript.sml new file mode 100644 index 0000000..4788ee1 --- /dev/null +++ b/prover_snapshots/hol4/lib/lem/lem_basic_classesScript.sml @@ -0,0 +1,503 @@ +(*Generated by Lem from basic_classes.lem.*) +open HolKernel Parse boolLib bossLib; +open lem_boolTheory ternaryComparisonsTheory; + +val _ = numLib.prefer_num(); + + + +val _ = new_theory "lem_basic_classes" + +(******************************************************************************) +(* Basic Type Classes *) +(******************************************************************************) + +(*open import Bool*) + +(*open import {coq} `Coq.Strings.Ascii`*) +(*open import {hol} `ternaryComparisonsTheory`*) + +(* ========================================================================== *) +(* Equality *) +(* ========================================================================== *) + +(* Lem`s default equality (=) is defined by the following type-class Eq. + This typeclass should define equality on an abstract datatype 'a. It should + always coincide with the default equality of Coq, HOL and Isabelle. + For OCaml, it might be different, since abstract datatypes like sets + might have fancy equalities. *) + +(*class ( Eq 'a ) + val = [isEqual] : 'a -> 'a -> bool + val <> [isInequal] : 'a -> 'a -> bool +end*) + + +(* (=) should for all instances be an equivalence relation + The isEquivalence predicate of relations could be used here. + However, this would lead to a cyclic dependency. *) + +(* TODO: add later, once lemmata can be assigned to classes +lemma eq_equiv: ((forall x. (x = x)) && + (forall x y. (x = y) <-> (y = x)) && + (forall x y z. ((x = y) && (y = z)) --> (x = z))) +*) + +(* Structural equality *) + +(* Sometimes, it is also handy to be able to use structural equality. + This equality is mapped to the build-in equality of backends. This equality + differs significantly for each backend. For example, OCaml can`t check equality + of function types, whereas HOL can. When using structural equality, one should + know what one is doing. The only guarentee is that is behaves like + the native backend equality. + + A lengthy name for structural equality is used to discourage its direct use. + It also ensures that users realise it is unsafe (e.g. OCaml can`t check two functions + for equality *) +(*val unsafe_structural_equality : forall 'a. 'a -> 'a -> bool*) + +(*val unsafe_structural_inequality : forall 'a. 'a -> 'a -> bool*) +(*let unsafe_structural_inequality x y= not (unsafe_structural_equality x y)*) + + +(* ========================================================================== *) +(* Orderings *) +(* ========================================================================== *) + +(* The type-class Ord represents total orders (also called linear orders) *) +(*type ordering = LT | EQ | GT*) + +val _ = Define ` + ((orderingIsLess:ordering -> bool) LESS= T) +/\ ((orderingIsLess:ordering -> bool) _= F)`; + +val _ = Define ` + ((orderingIsGreater:ordering -> bool) GREATER= T) +/\ ((orderingIsGreater:ordering -> bool) _= F)`; + +val _ = Define ` + ((orderingIsEqual:ordering -> bool) EQUAL= T) +/\ ((orderingIsEqual:ordering -> bool) _= F)`; + + +val _ = Define ` + ((ordering_cases:ordering -> 'a -> 'a -> 'a -> 'a) r lt eq gt= + (if orderingIsLess r then lt else + if orderingIsEqual r then eq else gt))`; + + + +(*val orderingEqual : ordering -> ordering -> bool*) + +val _ = Hol_datatype ` +(* 'a *) Ord_class= <| + compare_method : 'a -> 'a -> ordering; + isLess_method : 'a -> 'a -> bool; + isLessEqual_method : 'a -> 'a -> bool; + isGreater_method : 'a -> 'a -> bool; + isGreaterEqual_method : 'a -> 'a -> bool +|>`; + + + +(* Ocaml provides default, polymorphic compare functions. Let's use them + as the default. However, because used perhaps in a typeclass they must be + defined for all targets. So, explicitly declare them as undefined for + all other targets. If explictly declare undefined, the type-checker won't complain and + an error will only be raised when trying to actually output the function for a certain + target. *) +(*val defaultCompare : forall 'a. 'a -> 'a -> ordering*) +(*val defaultLess : forall 'a. 'a -> 'a -> bool*) +(*val defaultLessEq : forall 'a. 'a -> 'a -> bool*) +(*val defaultGreater : forall 'a. 'a -> 'a -> bool*) +(*val defaultGreaterEq : forall 'a. 'a -> 'a -> bool*) + + +val _ = Define ` + ((genericCompare:('a -> 'a -> bool) ->('a -> 'a -> bool) -> 'a -> 'a -> ordering) (less: 'a -> 'a -> bool) (equal: 'a -> 'a -> bool) (x : 'a) (y : 'a)= + (if less x y then + LESS + else if equal x y then + EQUAL + else + GREATER))`; + + + +(* +(* compare should really be a total order *) +lemma ord_OK_1: ( + (forall x y. (compare x y = EQ) <-> (compare y x = EQ)) && + (forall x y. (compare x y = LT) <-> (compare y x = GT))) + +lemma ord_OK_2: ( + (forall x y z. (x <= y) && (y <= z) --> (x <= z)) && + (forall x y. (x <= y) || (y <= x)) +) +*) + +(* let's derive a compare function from the Ord type-class *) +(*val ordCompare : forall 'a. Eq 'a, Ord 'a => 'a -> 'a -> ordering*) +val _ = Define ` + ((ordCompare:'a Ord_class -> 'a -> 'a -> ordering)dict_Basic_classes_Ord_a x y= + (if ( dict_Basic_classes_Ord_a.isLess_method x y) then LESS else + if (x = y) then EQUAL else GREATER))`; + + +val _ = Hol_datatype ` +(* 'a *) OrdMaxMin_class= <| + max_method : 'a -> 'a -> 'a; + min_method : 'a -> 'a -> 'a +|>`; + + +(*val minByLessEqual : forall 'a. ('a -> 'a -> bool) -> 'a -> 'a -> 'a*) +val _ = Define ` + ((minByLessEqual:('a -> 'a -> bool) -> 'a -> 'a -> 'a) le x y= (if (le x y) then x else y))`; + + +(*val maxByLessEqual : forall 'a. ('a -> 'a -> bool) -> 'a -> 'a -> 'a*) +val _ = Define ` + ((maxByLessEqual:('a -> 'a -> bool) -> 'a -> 'a -> 'a) le x y= (if (le y x) then x else y))`; + + +(*val defaultMax : forall 'a. Ord 'a => 'a -> 'a -> 'a*) + +(*val defaultMin : forall 'a. Ord 'a => 'a -> 'a -> 'a*) + +val _ = Define ` +((instance_Basic_classes_OrdMaxMin_var_dict:'a Ord_class -> 'a OrdMaxMin_class)dict_Basic_classes_Ord_a= (<| + + max_method := (maxByLessEqual + dict_Basic_classes_Ord_a.isLessEqual_method); + + min_method := (minByLessEqual + dict_Basic_classes_Ord_a.isLessEqual_method)|>))`; + + + +(* ========================================================================== *) +(* SetTypes *) +(* ========================================================================== *) + +(* Set implementations use often an order on the elements. This allows the OCaml implementation + to use trees for implementing them. At least, one needs to be able to check equality on sets. + One could use the Ord type-class for sets. However, defining a special typeclass is cleaner + and allows more flexibility. One can make e.g. sure, that this type-class is ignored for + backends like HOL or Isabelle, which don't need it. Moreover, one is not forced to also instantiate + the functions "<", "<=" ... *) + +(*class ( SetType 'a ) + val {ocaml;coq} setElemCompare : 'a -> 'a -> ordering +end*) + +val _ = Define ` + ((boolCompare:bool -> bool -> ordering) T T= EQUAL) +/\ ((boolCompare:bool -> bool -> ordering) T F= GREATER) +/\ ((boolCompare:bool -> bool -> ordering) F T= LESS) +/\ ((boolCompare:bool -> bool -> ordering) F F= EQUAL)`; + + +(* strings *) + +(*val charEqual : char -> char -> bool*) + +(*val stringEquality : string -> string -> bool*) + +(* pairs *) + +(*val pairEqual : forall 'a 'b. Eq 'a, Eq 'b => ('a * 'b) -> ('a * 'b) -> bool*) +(*let pairEqual (a1, b1) (a2, b2)= (a1 = a2) && (b1 = b2)*) + +(*val pairEqualBy : forall 'a 'b. ('a -> 'a -> bool) -> ('b -> 'b -> bool) -> ('a * 'b) -> ('a * 'b) -> bool*) + +(*val pairCompare : forall 'a 'b. ('a -> 'a -> ordering) -> ('b -> 'b -> ordering) -> ('a * 'b) -> ('a * 'b) -> ordering*) +val _ = Define ` + ((pairCompare:('a -> 'a -> ordering) ->('b -> 'b -> ordering) -> 'a#'b -> 'a#'b -> ordering) cmpa cmpb (a1, b1) (a2, b2)= + ((case cmpa a1 a2 of + LESS => LESS + | GREATER => GREATER + | EQUAL => cmpb b1 b2 + )))`; + + +val _ = Define ` + ((pairLess:'a Ord_class -> 'b Ord_class -> 'b#'a -> 'b#'a -> bool)dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b (x1, x2) (y1, y2)= (( + dict_Basic_classes_Ord_b.isLess_method x1 y1) \/ (( dict_Basic_classes_Ord_b.isLessEqual_method x1 y1) /\ ( dict_Basic_classes_Ord_a.isLess_method x2 y2))))`; + +val _ = Define ` + ((pairLessEq:'a Ord_class -> 'b Ord_class -> 'b#'a -> 'b#'a -> bool)dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b (x1, x2) (y1, y2)= (( + dict_Basic_classes_Ord_b.isLess_method x1 y1) \/ (( dict_Basic_classes_Ord_b.isLessEqual_method x1 y1) /\ ( dict_Basic_classes_Ord_a.isLessEqual_method x2 y2))))`; + + +val _ = Define ` + ((pairGreater:'a Ord_class -> 'b Ord_class -> 'a#'b -> 'a#'b -> bool)dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b x12 y12= (pairLess + dict_Basic_classes_Ord_b dict_Basic_classes_Ord_a y12 x12))`; + +val _ = Define ` + ((pairGreaterEq:'a Ord_class -> 'b Ord_class -> 'a#'b -> 'a#'b -> bool)dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b x12 y12= (pairLessEq + dict_Basic_classes_Ord_b dict_Basic_classes_Ord_a y12 x12))`; + + +val _ = Define ` +((instance_Basic_classes_Ord_tup2_dict:'a Ord_class -> 'b Ord_class ->('a#'b)Ord_class)dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b= (<| + + compare_method := (pairCompare + dict_Basic_classes_Ord_a.compare_method dict_Basic_classes_Ord_b.compare_method); + + isLess_method := + (pairLess dict_Basic_classes_Ord_b dict_Basic_classes_Ord_a); + + isLessEqual_method := + (pairLessEq dict_Basic_classes_Ord_b dict_Basic_classes_Ord_a); + + isGreater_method := + (pairGreater dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b); + + isGreaterEqual_method := + (pairGreaterEq dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b)|>))`; + + + +(* triples *) + +(*val tripleEqual : forall 'a 'b 'c. Eq 'a, Eq 'b, Eq 'c => ('a * 'b * 'c) -> ('a * 'b * 'c) -> bool*) +(*let tripleEqual (x1, x2, x3) (y1, y2, y3)= ((Instance_Basic_classes_Eq_tup2.=) (x1, (x2, x3)) (y1, (y2, y3)))*) + +(*val tripleCompare : forall 'a 'b 'c. ('a -> 'a -> ordering) -> ('b -> 'b -> ordering) -> ('c -> 'c -> ordering) -> ('a * 'b * 'c) -> ('a * 'b * 'c) -> ordering*) +val _ = Define ` + ((tripleCompare:('a -> 'a -> ordering) ->('b -> 'b -> ordering) ->('c -> 'c -> ordering) -> 'a#'b#'c -> 'a#'b#'c -> ordering) cmpa cmpb cmpc (a1, b1, c1) (a2, b2, c2)= + (pairCompare cmpa (pairCompare cmpb cmpc) (a1, (b1, c1)) (a2, (b2, c2))))`; + + +val _ = Define ` + ((tripleLess:'a Ord_class -> 'b Ord_class -> 'c Ord_class -> 'a#'b#'c -> 'a#'b#'c -> bool)dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b dict_Basic_classes_Ord_c (x1, x2, x3) (y1, y2, y3)= (pairLess + (instance_Basic_classes_Ord_tup2_dict dict_Basic_classes_Ord_b + dict_Basic_classes_Ord_c) dict_Basic_classes_Ord_a (x1, (x2, x3)) (y1, (y2, y3))))`; + +val _ = Define ` + ((tripleLessEq:'a Ord_class -> 'b Ord_class -> 'c Ord_class -> 'a#'b#'c -> 'a#'b#'c -> bool)dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b dict_Basic_classes_Ord_c (x1, x2, x3) (y1, y2, y3)= (pairLessEq + (instance_Basic_classes_Ord_tup2_dict dict_Basic_classes_Ord_b + dict_Basic_classes_Ord_c) dict_Basic_classes_Ord_a (x1, (x2, x3)) (y1, (y2, y3))))`; + + +val _ = Define ` + ((tripleGreater:'a Ord_class -> 'b Ord_class -> 'c Ord_class -> 'c#'b#'a -> 'c#'b#'a -> bool)dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b dict_Basic_classes_Ord_c x123 y123= (tripleLess + dict_Basic_classes_Ord_c dict_Basic_classes_Ord_b dict_Basic_classes_Ord_a y123 x123))`; + +val _ = Define ` + ((tripleGreaterEq:'a Ord_class -> 'b Ord_class -> 'c Ord_class -> 'c#'b#'a -> 'c#'b#'a -> bool)dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b dict_Basic_classes_Ord_c x123 y123= (tripleLessEq + dict_Basic_classes_Ord_c dict_Basic_classes_Ord_b dict_Basic_classes_Ord_a y123 x123))`; + + +val _ = Define ` +((instance_Basic_classes_Ord_tup3_dict:'a Ord_class -> 'b Ord_class -> 'c Ord_class ->('a#'b#'c)Ord_class)dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b dict_Basic_classes_Ord_c= (<| + + compare_method := (tripleCompare + dict_Basic_classes_Ord_a.compare_method dict_Basic_classes_Ord_b.compare_method dict_Basic_classes_Ord_c.compare_method); + + isLess_method := + (tripleLess dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b + dict_Basic_classes_Ord_c); + + isLessEqual_method := + (tripleLessEq dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b + dict_Basic_classes_Ord_c); + + isGreater_method := + (tripleGreater dict_Basic_classes_Ord_c dict_Basic_classes_Ord_b + dict_Basic_classes_Ord_a); + + isGreaterEqual_method := + (tripleGreaterEq dict_Basic_classes_Ord_c dict_Basic_classes_Ord_b + dict_Basic_classes_Ord_a)|>))`; + + +(* quadruples *) + +(*val quadrupleEqual : forall 'a 'b 'c 'd. Eq 'a, Eq 'b, Eq 'c, Eq 'd => ('a * 'b * 'c * 'd) -> ('a * 'b * 'c * 'd) -> bool*) +(*let quadrupleEqual (x1, x2, x3, x4) (y1, y2, y3, y4)= ((Instance_Basic_classes_Eq_tup2.=) (x1, (x2, (x3, x4))) (y1, (y2, (y3, y4))))*) + +(*val quadrupleCompare : forall 'a 'b 'c 'd. ('a -> 'a -> ordering) -> ('b -> 'b -> ordering) -> ('c -> 'c -> ordering) -> + ('d -> 'd -> ordering) -> ('a * 'b * 'c * 'd) -> ('a * 'b * 'c * 'd) -> ordering*) +val _ = Define ` + ((quadrupleCompare:('a -> 'a -> ordering) ->('b -> 'b -> ordering) ->('c -> 'c -> ordering) ->('d -> 'd -> ordering) -> 'a#'b#'c#'d -> 'a#'b#'c#'d -> ordering) cmpa cmpb cmpc cmpd (a1, b1, c1, d1) (a2, b2, c2, d2)= + (pairCompare cmpa (pairCompare cmpb (pairCompare cmpc cmpd)) (a1, (b1, (c1, d1))) (a2, (b2, (c2, d2)))))`; + + +val _ = Define ` + ((quadrupleLess:'a Ord_class -> 'b Ord_class -> 'c Ord_class -> 'd Ord_class -> 'a#'b#'c#'d -> 'a#'b#'c#'d -> bool)dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b dict_Basic_classes_Ord_c dict_Basic_classes_Ord_d (x1, x2, x3, x4) (y1, y2, y3, y4)= (pairLess + (instance_Basic_classes_Ord_tup2_dict dict_Basic_classes_Ord_b + (instance_Basic_classes_Ord_tup2_dict dict_Basic_classes_Ord_c + dict_Basic_classes_Ord_d)) dict_Basic_classes_Ord_a (x1, (x2, (x3, x4))) (y1, (y2, (y3, y4)))))`; + +val _ = Define ` + ((quadrupleLessEq:'a Ord_class -> 'b Ord_class -> 'c Ord_class -> 'd Ord_class -> 'a#'b#'c#'d -> 'a#'b#'c#'d -> bool)dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b dict_Basic_classes_Ord_c dict_Basic_classes_Ord_d (x1, x2, x3, x4) (y1, y2, y3, y4)= (pairLessEq + (instance_Basic_classes_Ord_tup2_dict dict_Basic_classes_Ord_b + (instance_Basic_classes_Ord_tup2_dict dict_Basic_classes_Ord_c + dict_Basic_classes_Ord_d)) dict_Basic_classes_Ord_a (x1, (x2, (x3, x4))) (y1, (y2, (y3, y4)))))`; + + +val _ = Define ` + ((quadrupleGreater:'a Ord_class -> 'b Ord_class -> 'c Ord_class -> 'd Ord_class -> 'd#'c#'b#'a -> 'd#'c#'b#'a -> bool)dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b dict_Basic_classes_Ord_c dict_Basic_classes_Ord_d x1234 y1234= (quadrupleLess + dict_Basic_classes_Ord_d dict_Basic_classes_Ord_c dict_Basic_classes_Ord_b dict_Basic_classes_Ord_a y1234 x1234))`; + +val _ = Define ` + ((quadrupleGreaterEq:'a Ord_class -> 'b Ord_class -> 'c Ord_class -> 'd Ord_class -> 'd#'c#'b#'a -> 'd#'c#'b#'a -> bool)dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b dict_Basic_classes_Ord_c dict_Basic_classes_Ord_d x1234 y1234= (quadrupleLessEq + dict_Basic_classes_Ord_d dict_Basic_classes_Ord_c dict_Basic_classes_Ord_b dict_Basic_classes_Ord_a y1234 x1234))`; + + +val _ = Define ` +((instance_Basic_classes_Ord_tup4_dict:'a Ord_class -> 'b Ord_class -> 'c Ord_class -> 'd Ord_class ->('a#'b#'c#'d)Ord_class)dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b dict_Basic_classes_Ord_c dict_Basic_classes_Ord_d= (<| + + compare_method := (quadrupleCompare + dict_Basic_classes_Ord_a.compare_method dict_Basic_classes_Ord_b.compare_method dict_Basic_classes_Ord_c.compare_method dict_Basic_classes_Ord_d.compare_method); + + isLess_method := + (quadrupleLess dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b + dict_Basic_classes_Ord_c dict_Basic_classes_Ord_d); + + isLessEqual_method := + (quadrupleLessEq dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b + dict_Basic_classes_Ord_c dict_Basic_classes_Ord_d); + + isGreater_method := + (quadrupleGreater dict_Basic_classes_Ord_d dict_Basic_classes_Ord_c + dict_Basic_classes_Ord_b dict_Basic_classes_Ord_a); + + isGreaterEqual_method := + (quadrupleGreaterEq dict_Basic_classes_Ord_d dict_Basic_classes_Ord_c + dict_Basic_classes_Ord_b dict_Basic_classes_Ord_a)|>))`; + + +(* quintuples *) + +(*val quintupleEqual : forall 'a 'b 'c 'd 'e. Eq 'a, Eq 'b, Eq 'c, Eq 'd, Eq 'e => ('a * 'b * 'c * 'd * 'e) -> ('a * 'b * 'c * 'd * 'e) -> bool*) +(*let quintupleEqual (x1, x2, x3, x4, x5) (y1, y2, y3, y4, y5)= ((Instance_Basic_classes_Eq_tup2.=) (x1, (x2, (x3, (x4, x5)))) (y1, (y2, (y3, (y4, y5)))))*) + +(*val quintupleCompare : forall 'a 'b 'c 'd 'e. ('a -> 'a -> ordering) -> ('b -> 'b -> ordering) -> ('c -> 'c -> ordering) -> + ('d -> 'd -> ordering) -> ('e -> 'e -> ordering) -> ('a * 'b * 'c * 'd * 'e) -> ('a * 'b * 'c * 'd * 'e) -> ordering*) +val _ = Define ` + ((quintupleCompare:('a -> 'a -> ordering) ->('b -> 'b -> ordering) ->('c -> 'c -> ordering) ->('d -> 'd -> ordering) ->('e -> 'e -> ordering) -> 'a#'b#'c#'d#'e -> 'a#'b#'c#'d#'e -> ordering) cmpa cmpb cmpc cmpd cmpe (a1, b1, c1, d1, e1) (a2, b2, c2, d2, e2)= + (pairCompare cmpa (pairCompare cmpb (pairCompare cmpc (pairCompare cmpd cmpe))) (a1, (b1, (c1, (d1, e1)))) (a2, (b2, (c2, (d2, e2))))))`; + + +val _ = Define ` + ((quintupleLess:'a Ord_class -> 'b Ord_class -> 'c Ord_class -> 'd Ord_class -> 'e Ord_class -> 'a#'b#'c#'d#'e -> 'a#'b#'c#'d#'e -> bool)dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b dict_Basic_classes_Ord_c dict_Basic_classes_Ord_d dict_Basic_classes_Ord_e (x1, x2, x3, x4, x5) (y1, y2, y3, y4, y5)= (pairLess + (instance_Basic_classes_Ord_tup2_dict dict_Basic_classes_Ord_b + (instance_Basic_classes_Ord_tup2_dict dict_Basic_classes_Ord_c + (instance_Basic_classes_Ord_tup2_dict dict_Basic_classes_Ord_d + dict_Basic_classes_Ord_e))) dict_Basic_classes_Ord_a (x1, (x2, (x3, (x4, x5)))) (y1, (y2, (y3, (y4, y5))))))`; + +val _ = Define ` + ((quintupleLessEq:'a Ord_class -> 'b Ord_class -> 'c Ord_class -> 'd Ord_class -> 'e Ord_class -> 'a#'b#'c#'d#'e -> 'a#'b#'c#'d#'e -> bool)dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b dict_Basic_classes_Ord_c dict_Basic_classes_Ord_d dict_Basic_classes_Ord_e (x1, x2, x3, x4, x5) (y1, y2, y3, y4, y5)= (pairLessEq + (instance_Basic_classes_Ord_tup2_dict dict_Basic_classes_Ord_b + (instance_Basic_classes_Ord_tup2_dict dict_Basic_classes_Ord_c + (instance_Basic_classes_Ord_tup2_dict dict_Basic_classes_Ord_d + dict_Basic_classes_Ord_e))) dict_Basic_classes_Ord_a (x1, (x2, (x3, (x4, x5)))) (y1, (y2, (y3, (y4, y5))))))`; + + +val _ = Define ` + ((quintupleGreater:'a Ord_class -> 'b Ord_class -> 'c Ord_class -> 'd Ord_class -> 'e Ord_class -> 'e#'d#'c#'b#'a -> 'e#'d#'c#'b#'a -> bool)dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b dict_Basic_classes_Ord_c dict_Basic_classes_Ord_d dict_Basic_classes_Ord_e x12345 y12345= (quintupleLess + dict_Basic_classes_Ord_e dict_Basic_classes_Ord_d dict_Basic_classes_Ord_c dict_Basic_classes_Ord_b dict_Basic_classes_Ord_a y12345 x12345))`; + +val _ = Define ` + ((quintupleGreaterEq:'a Ord_class -> 'b Ord_class -> 'c Ord_class -> 'd Ord_class -> 'e Ord_class -> 'e#'d#'c#'b#'a -> 'e#'d#'c#'b#'a -> bool)dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b dict_Basic_classes_Ord_c dict_Basic_classes_Ord_d dict_Basic_classes_Ord_e x12345 y12345= (quintupleLessEq + dict_Basic_classes_Ord_e dict_Basic_classes_Ord_d dict_Basic_classes_Ord_c dict_Basic_classes_Ord_b dict_Basic_classes_Ord_a y12345 x12345))`; + + +val _ = Define ` +((instance_Basic_classes_Ord_tup5_dict:'a Ord_class -> 'b Ord_class -> 'c Ord_class -> 'd Ord_class -> 'e Ord_class ->('a#'b#'c#'d#'e)Ord_class)dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b dict_Basic_classes_Ord_c dict_Basic_classes_Ord_d dict_Basic_classes_Ord_e= (<| + + compare_method := (quintupleCompare + dict_Basic_classes_Ord_a.compare_method dict_Basic_classes_Ord_b.compare_method dict_Basic_classes_Ord_c.compare_method dict_Basic_classes_Ord_d.compare_method dict_Basic_classes_Ord_e.compare_method); + + isLess_method := + (quintupleLess dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b + dict_Basic_classes_Ord_c dict_Basic_classes_Ord_d + dict_Basic_classes_Ord_e); + + isLessEqual_method := + (quintupleLessEq dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b + dict_Basic_classes_Ord_c dict_Basic_classes_Ord_d + dict_Basic_classes_Ord_e); + + isGreater_method := + (quintupleGreater dict_Basic_classes_Ord_e dict_Basic_classes_Ord_d + dict_Basic_classes_Ord_c dict_Basic_classes_Ord_b + dict_Basic_classes_Ord_a); + + isGreaterEqual_method := + (quintupleGreaterEq dict_Basic_classes_Ord_e dict_Basic_classes_Ord_d + dict_Basic_classes_Ord_c dict_Basic_classes_Ord_b + dict_Basic_classes_Ord_a)|>))`; + + +(* sextuples *) + +(*val sextupleEqual : forall 'a 'b 'c 'd 'e 'f. Eq 'a, Eq 'b, Eq 'c, Eq 'd, Eq 'e, Eq 'f => ('a * 'b * 'c * 'd * 'e * 'f) -> ('a * 'b * 'c * 'd * 'e * 'f) -> bool*) +(*let sextupleEqual (x1, x2, x3, x4, x5, x6) (y1, y2, y3, y4, y5, y6)= ((Instance_Basic_classes_Eq_tup2.=) (x1, (x2, (x3, (x4, (x5, x6))))) (y1, (y2, (y3, (y4, (y5, y6))))))*) + +(*val sextupleCompare : forall 'a 'b 'c 'd 'e 'f. ('a -> 'a -> ordering) -> ('b -> 'b -> ordering) -> ('c -> 'c -> ordering) -> + ('d -> 'd -> ordering) -> ('e -> 'e -> ordering) -> ('f -> 'f -> ordering) -> + ('a * 'b * 'c * 'd * 'e * 'f) -> ('a * 'b * 'c * 'd * 'e * 'f) -> ordering*) +val _ = Define ` + ((sextupleCompare:('a -> 'a -> ordering) ->('b -> 'b -> ordering) ->('c -> 'c -> ordering) ->('d -> 'd -> ordering) ->('e -> 'e -> ordering) ->('f -> 'f -> ordering) -> 'a#'b#'c#'d#'e#'f -> 'a#'b#'c#'d#'e#'f -> ordering) cmpa cmpb cmpc cmpd cmpe cmpf (a1, b1, c1, d1, e1, f1) (a2, b2, c2, d2, e2, f2)= + (pairCompare cmpa (pairCompare cmpb (pairCompare cmpc (pairCompare cmpd (pairCompare cmpe cmpf)))) (a1, (b1, (c1, (d1, (e1, f1))))) (a2, (b2, (c2, (d2, (e2, f2)))))))`; + + +val _ = Define ` + ((sextupleLess:'a Ord_class -> 'b Ord_class -> 'c Ord_class -> 'd Ord_class -> 'e Ord_class -> 'f Ord_class -> 'a#'b#'c#'d#'e#'f -> 'a#'b#'c#'d#'e#'f -> bool)dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b dict_Basic_classes_Ord_c dict_Basic_classes_Ord_d dict_Basic_classes_Ord_e dict_Basic_classes_Ord_f (x1, x2, x3, x4, x5, x6) (y1, y2, y3, y4, y5, y6)= (pairLess + (instance_Basic_classes_Ord_tup2_dict dict_Basic_classes_Ord_b + (instance_Basic_classes_Ord_tup2_dict dict_Basic_classes_Ord_c + (instance_Basic_classes_Ord_tup2_dict dict_Basic_classes_Ord_d + (instance_Basic_classes_Ord_tup2_dict dict_Basic_classes_Ord_e + dict_Basic_classes_Ord_f)))) dict_Basic_classes_Ord_a (x1, (x2, (x3, (x4, (x5, x6))))) (y1, (y2, (y3, (y4, (y5, y6)))))))`; + +val _ = Define ` + ((sextupleLessEq:'a Ord_class -> 'b Ord_class -> 'c Ord_class -> 'd Ord_class -> 'e Ord_class -> 'f Ord_class -> 'a#'b#'c#'d#'e#'f -> 'a#'b#'c#'d#'e#'f -> bool)dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b dict_Basic_classes_Ord_c dict_Basic_classes_Ord_d dict_Basic_classes_Ord_e dict_Basic_classes_Ord_f (x1, x2, x3, x4, x5, x6) (y1, y2, y3, y4, y5, y6)= (pairLessEq + (instance_Basic_classes_Ord_tup2_dict dict_Basic_classes_Ord_b + (instance_Basic_classes_Ord_tup2_dict dict_Basic_classes_Ord_c + (instance_Basic_classes_Ord_tup2_dict dict_Basic_classes_Ord_d + (instance_Basic_classes_Ord_tup2_dict dict_Basic_classes_Ord_e + dict_Basic_classes_Ord_f)))) dict_Basic_classes_Ord_a (x1, (x2, (x3, (x4, (x5, x6))))) (y1, (y2, (y3, (y4, (y5, y6)))))))`; + + +val _ = Define ` + ((sextupleGreater:'a Ord_class -> 'b Ord_class -> 'c Ord_class -> 'd Ord_class -> 'e Ord_class -> 'f Ord_class -> 'f#'e#'d#'c#'b#'a -> 'f#'e#'d#'c#'b#'a -> bool)dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b dict_Basic_classes_Ord_c dict_Basic_classes_Ord_d dict_Basic_classes_Ord_e dict_Basic_classes_Ord_f x123456 y123456= (sextupleLess + dict_Basic_classes_Ord_f dict_Basic_classes_Ord_e dict_Basic_classes_Ord_d dict_Basic_classes_Ord_c dict_Basic_classes_Ord_b dict_Basic_classes_Ord_a y123456 x123456))`; + +val _ = Define ` + ((sextupleGreaterEq:'a Ord_class -> 'b Ord_class -> 'c Ord_class -> 'd Ord_class -> 'e Ord_class -> 'f Ord_class -> 'f#'e#'d#'c#'b#'a -> 'f#'e#'d#'c#'b#'a -> bool)dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b dict_Basic_classes_Ord_c dict_Basic_classes_Ord_d dict_Basic_classes_Ord_e dict_Basic_classes_Ord_f x123456 y123456= (sextupleLessEq + dict_Basic_classes_Ord_f dict_Basic_classes_Ord_e dict_Basic_classes_Ord_d dict_Basic_classes_Ord_c dict_Basic_classes_Ord_b dict_Basic_classes_Ord_a y123456 x123456))`; + + +val _ = Define ` +((instance_Basic_classes_Ord_tup6_dict:'a Ord_class -> 'b Ord_class -> 'c Ord_class -> 'd Ord_class -> 'e Ord_class -> 'f Ord_class ->('a#'b#'c#'d#'e#'f)Ord_class)dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b dict_Basic_classes_Ord_c dict_Basic_classes_Ord_d dict_Basic_classes_Ord_e dict_Basic_classes_Ord_f= (<| + + compare_method := (sextupleCompare + dict_Basic_classes_Ord_a.compare_method dict_Basic_classes_Ord_b.compare_method dict_Basic_classes_Ord_c.compare_method dict_Basic_classes_Ord_d.compare_method dict_Basic_classes_Ord_e.compare_method dict_Basic_classes_Ord_f.compare_method); + + isLess_method := + (sextupleLess dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b + dict_Basic_classes_Ord_c dict_Basic_classes_Ord_d + dict_Basic_classes_Ord_e dict_Basic_classes_Ord_f); + + isLessEqual_method := + (sextupleLessEq dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b + dict_Basic_classes_Ord_c dict_Basic_classes_Ord_d + dict_Basic_classes_Ord_e dict_Basic_classes_Ord_f); + + isGreater_method := + (sextupleGreater dict_Basic_classes_Ord_f dict_Basic_classes_Ord_e + dict_Basic_classes_Ord_d dict_Basic_classes_Ord_c + dict_Basic_classes_Ord_b dict_Basic_classes_Ord_a); + + isGreaterEqual_method := + (sextupleGreaterEq dict_Basic_classes_Ord_f dict_Basic_classes_Ord_e + dict_Basic_classes_Ord_d dict_Basic_classes_Ord_c + dict_Basic_classes_Ord_b dict_Basic_classes_Ord_a)|>))`; + +val _ = export_theory() + |