Structure comparisonTheory

signature comparisonTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val equiv_inj_def : thm
    val good_cmp_def : thm
    val resp_equiv2_def : thm
    val resp_equiv_def : thm
  
  (*  Theorems  *)
    val TO_inv_invert : thm
    val TO_of_LinearOrder_LLEX : thm
    val TotOrd_list_cmp : thm
    val TotOrder_imp_good_cmp : thm
    val antisym_resp_equiv : thm
    val bool_cmp_antisym : thm
    val bool_cmp_def : thm
    val bool_cmp_good : thm
    val char_cmp_antisym : thm
    val char_cmp_charOrd : thm
    val char_cmp_def : thm
    val char_cmp_good : thm
    val cmp_thms : thm
    val good_cmp_Less_irrefl_trans : thm
    val good_cmp_Less_trans : thm
    val good_cmp_thm : thm
    val good_cmp_trans : thm
    val list_cmp_ListOrd : thm
    val list_cmp_antisym : thm
    val list_cmp_cong : thm
    val list_cmp_equal_list_rel : thm
    val list_cmp_good : thm
    val num_cmp_antisym : thm
    val num_cmp_def : thm
    val num_cmp_good : thm
    val num_cmp_numOrd : thm
    val option_cmp2_TO_inv : thm
    val option_cmp2_antisym : thm
    val option_cmp2_cong : thm
    val option_cmp2_def : thm
    val option_cmp2_good : thm
    val option_cmp2_ind : thm
    val option_cmp_antisym : thm
    val option_cmp_cong : thm
    val option_cmp_def : thm
    val option_cmp_good : thm
    val pair_cmp_antisym : thm
    val pair_cmp_cong : thm
    val pair_cmp_def : thm
    val pair_cmp_good : thm
    val pair_cmp_lexTO : thm
    val string_cmp_antisym : thm
    val string_cmp_def : thm
    val string_cmp_good : thm
    val string_cmp_stringto : thm
  
  val comparison_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [toto] Parent theory of "comparison"
   
   [equiv_inj_def]  Definition
      
      ⊢ ∀cmp cmp2 f.
            equiv_inj cmp cmp2 f ⇔
            ∀k1 k2. cmp2 (f k1) (f k2) = Equal ⇒ cmp k1 k2 = Equal
   
   [good_cmp_def]  Definition
      
      ⊢ ∀cmp.
            good_cmp cmp ⇔
            (∀x. cmp x x = Equal) ∧
            (∀x y. cmp x y = Equal ⇒ cmp y x = Equal) ∧
            (∀x y. cmp x y = Greater ⇔ cmp y x = Less) ∧
            (∀x y z. cmp x y = Equal ∧ cmp y z = Less ⇒ cmp x z = Less) ∧
            (∀x y z. cmp x y = Less ∧ cmp y z = Equal ⇒ cmp x z = Less) ∧
            (∀x y z. cmp x y = Equal ∧ cmp y z = Equal ⇒ cmp x z = Equal) ∧
            ∀x y z. cmp x y = Less ∧ cmp y z = Less ⇒ cmp x z = Less
   
   [resp_equiv2_def]  Definition
      
      ⊢ ∀cmp cmp2 f.
            resp_equiv2 cmp cmp2 f ⇔
            ∀k1 k2. cmp k1 k2 = Equal ⇒ cmp2 (f k1) (f k2) = Equal
   
   [resp_equiv_def]  Definition
      
      ⊢ ∀cmp f.
            resp_equiv cmp f ⇔
            ∀k1 k2 v. cmp k1 k2 = Equal ⇒ f k1 v = f k2 v
   
   [TO_inv_invert]  Theorem
      
      ⊢ ∀c. TotOrd c ⇒ TO_inv c = CURRY (invert ∘ UNCURRY c)
   
   [TO_of_LinearOrder_LLEX]  Theorem
      
      ⊢ ∀R.
            irreflexive R ⇒
            TO_of_LinearOrder (LLEX R) = list_cmp (TO_of_LinearOrder R)
   
   [TotOrd_list_cmp]  Theorem
      
      ⊢ ∀c. TotOrd c ⇒ TotOrd (list_cmp c)
   
   [TotOrder_imp_good_cmp]  Theorem
      
      ⊢ ∀cmp. TotOrd cmp ⇒ good_cmp cmp
   
   [antisym_resp_equiv]  Theorem
      
      ⊢ ∀cmp f.
            (∀x y. cmp x y = Equal ⇒ x = y) ⇒
            resp_equiv cmp f ∧
            ∀cmp2. good_cmp cmp2 ⇒ resp_equiv2 cmp cmp2 f
   
   [bool_cmp_antisym]  Theorem
      
      ⊢ ∀x y. bool_cmp x y = Equal ⇔ (x ⇔ y)
   
   [bool_cmp_def]  Theorem
      
      ⊢ bool_cmp T T = Equal ∧ bool_cmp F F = Equal ∧
        bool_cmp T F = Greater ∧ bool_cmp F T = Less
   
   [bool_cmp_good]  Theorem
      
      ⊢ good_cmp bool_cmp
   
   [char_cmp_antisym]  Theorem
      
      ⊢ ∀x y. char_cmp x y = Equal ⇔ x = y
   
   [char_cmp_charOrd]  Theorem
      
      ⊢ char_cmp = charOrd
   
   [char_cmp_def]  Theorem
      
      ⊢ ∀c1 c2. char_cmp c1 c2 = num_cmp (ORD c1) (ORD c2)
   
   [char_cmp_good]  Theorem
      
      ⊢ good_cmp char_cmp
   
   [cmp_thms]  Theorem
      
      ⊢ (Less ≠ Equal ∧ Less ≠ Greater ∧ Equal ≠ 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) ∧ (∀a. a = Less ∨ a = Equal ∨ a = Greater) ∧
        ∀cmp.
            good_cmp cmp ⇔
            (∀x. cmp x x = Equal) ∧
            (∀x y. cmp x y = Equal ⇒ cmp y x = Equal) ∧
            (∀x y. cmp x y = Greater ⇔ cmp y x = Less) ∧
            (∀x y z. cmp x y = Equal ∧ cmp y z = Less ⇒ cmp x z = Less) ∧
            (∀x y z. cmp x y = Less ∧ cmp y z = Equal ⇒ cmp x z = Less) ∧
            (∀x y z. cmp x y = Equal ∧ cmp y z = Equal ⇒ cmp x z = Equal) ∧
            ∀x y z. cmp x y = Less ∧ cmp y z = Less ⇒ cmp x z = Less
   
   [good_cmp_Less_irrefl_trans]  Theorem
      
      ⊢ ∀cmp.
            good_cmp cmp ⇒
            irreflexive (λk k'. cmp k k' = Less) ∧
            transitive (λk k'. cmp k k' = Less)
   
   [good_cmp_Less_trans]  Theorem
      
      ⊢ ∀cmp. good_cmp cmp ⇒ transitive (λk k'. cmp k k' = Less)
   
   [good_cmp_thm]  Theorem
      
      ⊢ ∀cmp.
            good_cmp cmp ⇔
            (∀x. cmp x x = Equal) ∧
            ∀x y z.
                (cmp x y = Greater ⇔ cmp y x = Less) ∧
                (cmp x y = Less ∧ cmp y z = Equal ⇒ cmp x z = Less) ∧
                (cmp x y = Less ∧ cmp y z = Less ⇒ cmp x z = Less)
   
   [good_cmp_trans]  Theorem
      
      ⊢ ∀cmp. good_cmp cmp ⇒ transitive (λ(k,v) (k',v'). cmp k k' = Less)
   
   [list_cmp_ListOrd]  Theorem
      
      ⊢ ∀c. TotOrd c ⇒ list_cmp c = ListOrd (TO c)
   
   [list_cmp_antisym]  Theorem
      
      ⊢ ∀cmp x y.
            (∀x y. cmp x y = Equal ⇔ x = y) ⇒
            (list_cmp cmp x y = Equal ⇔ x = y)
   
   [list_cmp_cong]  Theorem
      
      ⊢ ∀cmp l1 l2 cmp' l1' l2'.
            l1 = l1' ∧ l2 = l2' ∧
            (∀x x'. MEM x l1' ∧ MEM x' l2' ⇒ cmp x x' = cmp' x x') ⇒
            list_cmp cmp l1 l2 = list_cmp cmp' l1' l2'
   
   [list_cmp_equal_list_rel]  Theorem
      
      ⊢ ∀cmp l1 l2.
            list_cmp cmp l1 l2 = Equal ⇔
            LIST_REL (λx y. cmp x y = Equal) l1 l2
   
   [list_cmp_good]  Theorem
      
      ⊢ ∀cmp. good_cmp cmp ⇒ good_cmp (list_cmp cmp)
   
   [num_cmp_antisym]  Theorem
      
      ⊢ ∀x y. num_cmp x y = Equal ⇔ x = y
   
   [num_cmp_def]  Theorem
      
      ⊢ ∀n1 n2.
            num_cmp n1 n2 =
            if n1 = n2 then Equal else if n1 < n2 then Less else Greater
   
   [num_cmp_good]  Theorem
      
      ⊢ good_cmp num_cmp
   
   [num_cmp_numOrd]  Theorem
      
      ⊢ num_cmp = numOrd
   
   [option_cmp2_TO_inv]  Theorem
      
      ⊢ ∀c. option_cmp2 c = TO_inv (option_cmp (TO_inv c))
   
   [option_cmp2_antisym]  Theorem
      
      ⊢ ∀cmp x y.
            (∀x y. cmp x y = Equal ⇔ x = y) ⇒
            (option_cmp2 cmp x y = Equal ⇔ x = y)
   
   [option_cmp2_cong]  Theorem
      
      ⊢ ∀cmp v1 v2 cmp' v1' v2'.
            v1 = v1' ∧ v2 = v2' ∧
            (∀x x'. v1' = SOME x ∧ v2' = SOME x' ⇒ cmp x x' = cmp' x x') ⇒
            option_cmp2 cmp v1 v2 = option_cmp2 cmp' v1' v2'
   
   [option_cmp2_def]  Theorem
      
      ⊢ option_cmp2 cmp NONE NONE = Equal ∧
        option_cmp2 cmp NONE (SOME x') = Greater ∧
        option_cmp2 cmp (SOME x) NONE = Less ∧
        option_cmp2 cmp (SOME x) (SOME y) = cmp x y
   
   [option_cmp2_good]  Theorem
      
      ⊢ ∀cmp. good_cmp cmp ⇒ good_cmp (option_cmp2 cmp)
   
   [option_cmp2_ind]  Theorem
      
      ⊢ ∀P.
            (∀cmp. P cmp NONE NONE) ∧ (∀cmp x. P cmp NONE (SOME x)) ∧
            (∀cmp x. P cmp (SOME x) NONE) ∧
            (∀cmp x y. P cmp (SOME x) (SOME y)) ⇒
            ∀v v1 v2. P v v1 v2
   
   [option_cmp_antisym]  Theorem
      
      ⊢ ∀cmp x y.
            (∀x y. cmp x y = Equal ⇔ x = y) ⇒
            (option_cmp cmp x y = Equal ⇔ x = y)
   
   [option_cmp_cong]  Theorem
      
      ⊢ ∀cmp v1 v2 cmp' v1' v2'.
            v1 = v1' ∧ v2 = v2' ∧
            (∀x x'. v1' = SOME x ∧ v2' = SOME x' ⇒ cmp x x' = cmp' x x') ⇒
            option_cmp cmp v1 v2 = option_cmp cmp' v1' v2'
   
   [option_cmp_def]  Theorem
      
      ⊢ option_cmp c NONE NONE = Equal ∧
        option_cmp c NONE (SOME v0) = Less ∧
        option_cmp c (SOME v3) NONE = Greater ∧
        option_cmp c (SOME v1) (SOME v2) = c v1 v2
   
   [option_cmp_good]  Theorem
      
      ⊢ ∀cmp. good_cmp cmp ⇒ good_cmp (option_cmp cmp)
   
   [pair_cmp_antisym]  Theorem
      
      ⊢ ∀cmp1 cmp2 x y.
            (∀x y. cmp1 x y = Equal ⇔ x = y) ∧
            (∀x y. cmp2 x y = Equal ⇔ x = y) ⇒
            (pair_cmp cmp1 cmp2 x y = Equal ⇔ x = y)
   
   [pair_cmp_cong]  Theorem
      
      ⊢ ∀cmp1 cmp2 v1 v2 cmp1' cmp2' v1' v2'.
            v1 = v1' ∧ v2 = v2' ∧
            (∀a b c d. v1' = (a,b) ∧ v2' = (c,d) ⇒ cmp1 a c = cmp1' a c) ∧
            (∀a b c d. v1' = (a,b) ∧ v2' = (c,d) ⇒ cmp2 b d = cmp2' b d) ⇒
            pair_cmp cmp1 cmp2 v1 v2 = pair_cmp cmp1' cmp2' v1' v2'
   
   [pair_cmp_def]  Theorem
      
      ⊢ pair_cmp c1 c2 x y =
        case c1 (FST x) (FST y) of
          Less => Less
        | Equal => c2 (SND x) (SND y)
        | Greater => Greater
   
   [pair_cmp_good]  Theorem
      
      ⊢ ∀cmp1 cmp2.
            good_cmp cmp1 ∧ good_cmp cmp2 ⇒ good_cmp (pair_cmp cmp1 cmp2)
   
   [pair_cmp_lexTO]  Theorem
      
      ⊢ ∀R V. TotOrd R ∧ TotOrd V ⇒ pair_cmp R V = R lexTO V
   
   [string_cmp_antisym]  Theorem
      
      ⊢ ∀x y. string_cmp x y = Equal ⇔ x = y
   
   [string_cmp_def]  Theorem
      
      ⊢ string_cmp = list_cmp char_cmp
   
   [string_cmp_good]  Theorem
      
      ⊢ good_cmp string_cmp
   
   [string_cmp_stringto]  Theorem
      
      ⊢ string_cmp = apto stringto
   
   
*)
end

HOL 4, Kananaskis-13