Structure ternaryComparisonsTheory

signature ternaryComparisonsTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val char_compare_def : thm
    val invert_comparison_def : thm
    val num_compare_def : thm
    val ordering_BIJ : thm
    val ordering_CASE : thm
    val ordering_TY_DEF : thm
    val ordering_size_def : thm
    val pair_compare_def : thm
    val string_compare_def : thm
  
  (*  Theorems  *)
    val bool_compare_def : thm
    val bool_compare_ind : thm
    val compare_equal : thm
    val datatype_ordering : thm
    val invert_eq_EQUAL : thm
    val list_compare_def : thm
    val list_compare_ind : thm
    val list_merge_def : thm
    val list_merge_ind : thm
    val num2ordering_11 : thm
    val num2ordering_ONTO : thm
    val num2ordering_ordering2num : thm
    val num2ordering_thm : thm
    val option_compare_def : thm
    val option_compare_ind : thm
    val ordering2num_11 : thm
    val ordering2num_ONTO : thm
    val ordering2num_num2ordering : thm
    val ordering2num_thm : thm
    val ordering_Axiom : thm
    val ordering_EQ_ordering : thm
    val ordering_case_cong : thm
    val ordering_case_def : thm
    val ordering_case_eq : thm
    val ordering_distinct : thm
    val ordering_eq_dec : thm
    val ordering_induction : thm
    val ordering_nchotomy : thm
  
  val ternaryComparisons_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [string] Parent theory of "ternaryComparisons"
   
   [char_compare_def]  Definition
      
      ⊢ ∀c1 c2. char_compare c1 c2 = num_compare (ORD c1) (ORD c2)
   
   [invert_comparison_def]  Definition
      
      ⊢ (invert_comparison GREATER = LESS) ∧
        (invert_comparison LESS = GREATER) ∧
        (invert_comparison EQUAL = EQUAL)
   
   [num_compare_def]  Definition
      
      ⊢ ∀n1 n2.
            num_compare n1 n2 =
            if n1 = n2 then EQUAL
            else if n1 < n2 then LESS
            else GREATER
   
   [ordering_BIJ]  Definition
      
      ⊢ (∀a. num2ordering (ordering2num a) = a) ∧
        ∀r. (λn. n < 3) r ⇔ (ordering2num (num2ordering r) = r)
   
   [ordering_CASE]  Definition
      
      ⊢ ∀x v0 v1 v2.
            (case x of LESS => v0 | EQUAL => v1 | GREATER => v2) =
            (λm. if m < 1 then v0 else if m = 1 then v1 else v2)
              (ordering2num x)
   
   [ordering_TY_DEF]  Definition
      
      ⊢ ∃rep. TYPE_DEFINITION (λn. n < 3) rep
   
   [ordering_size_def]  Definition
      
      ⊢ ∀x. ordering_size x = 0
   
   [pair_compare_def]  Definition
      
      ⊢ ∀c1 c2 a b x y.
            pair_compare c1 c2 (a,b) (x,y) =
            case c1 a x of
              LESS => LESS
            | EQUAL => c2 b y
            | GREATER => GREATER
   
   [string_compare_def]  Definition
      
      ⊢ string_compare = list_compare char_compare
   
   [bool_compare_def]  Theorem
      
      ⊢ (bool_compare T T = EQUAL) ∧ (bool_compare F F = EQUAL) ∧
        (bool_compare T F = GREATER) ∧ (bool_compare F T = LESS)
   
   [bool_compare_ind]  Theorem
      
      ⊢ ∀P. P T T ∧ P F F ∧ P T F ∧ P F T ⇒ ∀v v1. P v v1
   
   [compare_equal]  Theorem
      
      ⊢ (∀x y. (cmp x y = EQUAL) ⇔ (x = y)) ⇒
        ∀l1 l2. (list_compare cmp l1 l2 = EQUAL) ⇔ (l1 = l2)
   
   [datatype_ordering]  Theorem
      
      ⊢ DATATYPE (ordering LESS EQUAL GREATER)
   
   [invert_eq_EQUAL]  Theorem
      
      ⊢ ∀x. (invert_comparison x = EQUAL) ⇔ (x = EQUAL)
   
   [list_compare_def]  Theorem
      
      ⊢ (∀cmp. list_compare cmp [] [] = EQUAL) ∧
        (∀v9 v8 cmp. list_compare cmp [] (v8::v9) = LESS) ∧
        (∀v5 v4 cmp. list_compare cmp (v4::v5) [] = GREATER) ∧
        ∀y x l2 l1 cmp.
            list_compare cmp (x::l1) (y::l2) =
            case cmp x y of
              LESS => LESS
            | EQUAL => list_compare cmp l1 l2
            | GREATER => GREATER
   
   [list_compare_ind]  Theorem
      
      ⊢ ∀P.
            (∀cmp. P cmp [] []) ∧ (∀cmp v8 v9. P cmp [] (v8::v9)) ∧
            (∀cmp v4 v5. P cmp (v4::v5) []) ∧
            (∀cmp x l1 y l2.
                 ((cmp x y = EQUAL) ⇒ P cmp l1 l2) ⇒ P cmp (x::l1) (y::l2)) ⇒
            ∀v v1 v2. P v v1 v2
   
   [list_merge_def]  Theorem
      
      ⊢ (∀l1 a_lt. list_merge a_lt l1 [] = l1) ∧
        (∀v5 v4 a_lt. list_merge a_lt [] (v4::v5) = v4::v5) ∧
        ∀y x l2 l1 a_lt.
            list_merge a_lt (x::l1) (y::l2) =
            if a_lt x y then x::list_merge a_lt l1 (y::l2)
            else y::list_merge a_lt (x::l1) l2
   
   [list_merge_ind]  Theorem
      
      ⊢ ∀P.
            (∀a_lt l1. P a_lt l1 []) ∧ (∀a_lt v4 v5. P a_lt [] (v4::v5)) ∧
            (∀a_lt x l1 y l2.
                 (¬a_lt x y ⇒ P a_lt (x::l1) l2) ∧
                 (a_lt x y ⇒ P a_lt l1 (y::l2)) ⇒
                 P a_lt (x::l1) (y::l2)) ⇒
            ∀v v1 v2. P v v1 v2
   
   [num2ordering_11]  Theorem
      
      ⊢ ∀r r'.
            r < 3 ⇒
            r' < 3 ⇒
            ((num2ordering r = num2ordering r') ⇔ (r = r'))
   
   [num2ordering_ONTO]  Theorem
      
      ⊢ ∀a. ∃r. (a = num2ordering r) ∧ r < 3
   
   [num2ordering_ordering2num]  Theorem
      
      ⊢ ∀a. num2ordering (ordering2num a) = a
   
   [num2ordering_thm]  Theorem
      
      ⊢ (num2ordering 0 = LESS) ∧ (num2ordering 1 = EQUAL) ∧
        (num2ordering 2 = GREATER)
   
   [option_compare_def]  Theorem
      
      ⊢ (option_compare c NONE NONE = EQUAL) ∧
        (option_compare c NONE (SOME v0) = LESS) ∧
        (option_compare c (SOME v3) NONE = GREATER) ∧
        (option_compare c (SOME v1) (SOME v2) = c v1 v2)
   
   [option_compare_ind]  Theorem
      
      ⊢ ∀P.
            (∀c. P c NONE NONE) ∧ (∀c v0. P c NONE (SOME v0)) ∧
            (∀c v3. P c (SOME v3) NONE) ∧
            (∀c v1 v2. P c (SOME v1) (SOME v2)) ⇒
            ∀v v1 v2. P v v1 v2
   
   [ordering2num_11]  Theorem
      
      ⊢ ∀a a'. (ordering2num a = ordering2num a') ⇔ (a = a')
   
   [ordering2num_ONTO]  Theorem
      
      ⊢ ∀r. r < 3 ⇔ ∃a. r = ordering2num a
   
   [ordering2num_num2ordering]  Theorem
      
      ⊢ ∀r. r < 3 ⇔ (ordering2num (num2ordering r) = r)
   
   [ordering2num_thm]  Theorem
      
      ⊢ (ordering2num LESS = 0) ∧ (ordering2num EQUAL = 1) ∧
        (ordering2num GREATER = 2)
   
   [ordering_Axiom]  Theorem
      
      ⊢ ∀x0 x1 x2. ∃f. (f LESS = x0) ∧ (f EQUAL = x1) ∧ (f GREATER = x2)
   
   [ordering_EQ_ordering]  Theorem
      
      ⊢ ∀a a'. (a = a') ⇔ (ordering2num a = ordering2num a')
   
   [ordering_case_cong]  Theorem
      
      ⊢ ∀M M' v0 v1 v2.
            (M = M') ∧ ((M' = LESS) ⇒ (v0 = v0')) ∧
            ((M' = EQUAL) ⇒ (v1 = v1')) ∧ ((M' = GREATER) ⇒ (v2 = v2')) ⇒
            ((case M of LESS => v0 | EQUAL => v1 | GREATER => v2) =
             case M' of LESS => v0' | EQUAL => v1' | GREATER => v2')
   
   [ordering_case_def]  Theorem
      
      ⊢ (∀v0 v1 v2.
             (case LESS of LESS => v0 | EQUAL => v1 | GREATER => v2) = v0) ∧
        (∀v0 v1 v2.
             (case EQUAL of LESS => v0 | EQUAL => v1 | GREATER => v2) = v1) ∧
        ∀v0 v1 v2.
            (case GREATER of LESS => v0 | EQUAL => v1 | GREATER => v2) = v2
   
   [ordering_case_eq]  Theorem
      
      ⊢ ((case x of LESS => v0 | EQUAL => v1 | GREATER => v2) = v) ⇔
        (x = LESS) ∧ (v0 = v) ∨ (x = EQUAL) ∧ (v1 = v) ∨
        (x = GREATER) ∧ (v2 = v)
   
   [ordering_distinct]  Theorem
      
      ⊢ LESS ≠ EQUAL ∧ LESS ≠ GREATER ∧ EQUAL ≠ GREATER
   
   [ordering_eq_dec]  Theorem
      
      ⊢ (∀x. (x = x) ⇔ T) ∧ ((LESS = EQUAL) ⇔ F) ∧ ((LESS = GREATER) ⇔ F) ∧
        ((EQUAL = GREATER) ⇔ F) ∧ ((EQUAL = LESS) ⇔ F) ∧
        ((GREATER = LESS) ⇔ F) ∧ ((GREATER = EQUAL) ⇔ F) ∧
        ((ordering2num LESS = 0) ∧ (ordering2num EQUAL = 1) ∧
         (ordering2num GREATER = 2)) ∧
        ((num2ordering 0 = LESS) ∧ (num2ordering 1 = EQUAL) ∧
         (num2ordering 2 = GREATER)) ∧
        ((∀v0 v1 v2.
              (case LESS of LESS => v0 | EQUAL => v1 | GREATER => v2) = v0) ∧
         (∀v0 v1 v2.
              (case EQUAL of LESS => v0 | EQUAL => v1 | GREATER => v2) = v1) ∧
         ∀v0 v1 v2.
             (case GREATER of LESS => v0 | EQUAL => v1 | GREATER => v2) =
             v2) ∧ ((LESS = EQUAL) ⇔ F) ∧ ((LESS = GREATER) ⇔ F) ∧
        ((EQUAL = GREATER) ⇔ F) ∧ ((EQUAL = LESS) ⇔ F) ∧
        ((GREATER = LESS) ⇔ F) ∧ ((GREATER = EQUAL) ⇔ F)
   
   [ordering_induction]  Theorem
      
      ⊢ ∀P. P EQUAL ∧ P GREATER ∧ P LESS ⇒ ∀a. P a
   
   [ordering_nchotomy]  Theorem
      
      ⊢ ∀a. (a = LESS) ∨ (a = EQUAL) ∨ (a = GREATER)
   
   
*)
end

HOL 4, Kananaskis-11