Structure totoTheory


Source File Identifier index Theory binding index

signature totoTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val ListOrd : thm
    val StrongLinearOrder_of_TO : thm
    val TO_inv : thm
    val TO_of_LinearOrder : thm
    val TotOrd : thm
    val WeakLinearOrder_of_TO : thm
    val charOrd : thm
    val charto : thm
    val imageOrd : thm
    val lexTO : thm
    val lextoto : thm
    val listoto : thm
    val numOrd : thm
    val num_dt_TY_DEF : thm
    val num_dt_case_def : thm
    val num_dt_size_def : thm
    val num_to_dt_primitive : thm
    val numto : thm
    val qk_numOrd_def : thm
    val qk_numto : thm
    val stringto : thm
    val to_bij : thm
    val toto_TY_DEF : thm
    val toto_inv : thm
    val toto_of_LinearOrder : thm
  
  (*  Theorems  *)
    val LEX_ALT : thm
    val ListOrd_THM : thm
    val NOT_EQ_LESS_IMP : thm
    val SLO_LEX : thm
    val SLO_listorder : thm
    val SPLIT_PAIRS : thm
    val STRORD_SLO : thm
    val StrongLinearOrderExists : thm
    val StrongLinearOrder_LESS : thm
    val StrongLinearOrder_of_TO_TO_of_LinearOrder : thm
    val StrongOrder_ALT : thm
    val Strong_Strong_of : thm
    val Strong_Strong_of_TO : thm
    val Strong_toto_inv : thm
    val Strong_toto_thm : thm
    val Strongof_toto_STRORD : thm
    val TO_11 : thm
    val TO_ListOrd : thm
    val TO_antisym : thm
    val TO_apto_ID : thm
    val TO_apto_TO_ID : thm
    val TO_apto_TO_IMP : thm
    val TO_charOrd : thm
    val TO_cpn_eqn : thm
    val TO_equal_eq : thm
    val TO_exists : thm
    val TO_injection : thm
    val TO_inv_Ord : thm
    val TO_inv_TO_inv : thm
    val TO_lexTO : thm
    val TO_numOrd : thm
    val TO_of_LinearOrder_LEX : thm
    val TO_of_greater_ler : thm
    val TO_of_less_rel : thm
    val TO_onto : thm
    val TO_qk_numOrd : thm
    val TO_refl : thm
    val TotOrd_TO_of_LO : thm
    val TotOrd_TO_of_Strong : thm
    val TotOrd_TO_of_Weak : thm
    val TotOrd_apto : thm
    val TotOrd_inv : thm
    val Weak_Weak_of : thm
    val Weak_toto_inv : thm
    val Weak_toto_thm : thm
    val all_cpn_distinct : thm
    val ap_qk_numto_thm : thm
    val apcharto_thm : thm
    val aplextoto : thm
    val aplistoto : thm
    val apnumto_thm : thm
    val apto_inv : thm
    val charOrd_eq_lem : thm
    val charOrd_gt_lem : thm
    val charOrd_lt_lem : thm
    val charOrd_thm : thm
    val datatype_num_dt : thm
    val inv_TO : thm
    val lexTO_ALT : thm
    val lexTO_thm : thm
    val listorder : thm
    val listorder_ind : thm
    val num_dtOrd : thm
    val num_dtOrd_ind : thm
    val num_dt_11 : thm
    val num_dt_Axiom : thm
    val num_dt_case_cong : thm
    val num_dt_case_eq : thm
    val num_dt_distinct : thm
    val num_dt_induction : thm
    val num_dt_nchotomy : thm
    val numeralOrd : thm
    val onto_apto : thm
    val pre_aplextoto : thm
    val qk_numeralOrd : thm
    val totoEEtrans : thm
    val totoELtrans : thm
    val totoGGtrans : thm
    val totoGLtrans : thm
    val totoLEtrans : thm
    val totoLGtrans : thm
    val totoLLtrans : thm
    val toto_Strong_thm : thm
    val toto_Weak_thm : thm
    val toto_antisym : thm
    val toto_cpn_eqn : thm
    val toto_equal_eq : thm
    val toto_equal_imp : thm
    val toto_equal_imp_eq : thm
    val toto_equal_sym : thm
    val toto_glneq : thm
    val toto_inv_toto_inv : thm
    val toto_not_less_refl : thm
    val toto_refl : thm
    val toto_swap_cases : thm
    val toto_thm : thm
    val toto_trans_less : thm
    val toto_unequal_imp : thm
    val trichotomous_ALT : thm
  
  val toto_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [ternaryComparisons] Parent theory of "toto"
   
   [wot] Parent theory of "toto"
   
   [ListOrd]  Definition
      
      |- !c.
             ListOrd c =
             TO_of_LinearOrder
               (listorder (StrongLinearOrder_of_TO (apto c)))
   
   [StrongLinearOrder_of_TO]  Definition
      
      |- !c x y.
             StrongLinearOrder_of_TO c x y <=>
             case c x y of LESS => T | EQUAL => F | GREATER => F
   
   [TO_inv]  Definition
      
      |- !c x y. TO_inv c x y = c y x
   
   [TO_of_LinearOrder]  Definition
      
      |- !r x y.
             TO_of_LinearOrder r x y =
             if x = y then EQUAL else if r x y then LESS else GREATER
   
   [TotOrd]  Definition
      
      |- !c.
             TotOrd c <=>
             (!x y. (c x y = EQUAL) <=> (x = y)) /\
             (!x y. (c x y = GREATER) <=> (c y x = LESS)) /\
             !x y z. (c x y = LESS) /\ (c y z = LESS) ==> (c x z = LESS)
   
   [WeakLinearOrder_of_TO]  Definition
      
      |- !c x y.
             WeakLinearOrder_of_TO c x y <=>
             case c x y of LESS => T | EQUAL => T | GREATER => F
   
   [charOrd]  Definition
      
      |- !a b. charOrd a b = numOrd (ORD a) (ORD b)
   
   [charto]  Definition
      
      |- charto = TO charOrd
   
   [imageOrd]  Definition
      
      |- !f cp a b. imageOrd f cp a b = cp (f a) (f b)
   
   [lexTO]  Definition
      
      |- !R V.
             R lexTO V =
             TO_of_LinearOrder
               (StrongLinearOrder_of_TO R LEX StrongLinearOrder_of_TO V)
   
   [lextoto]  Definition
      
      |- !c v. c lextoto v = TO (apto c lexTO apto v)
   
   [listoto]  Definition
      
      |- !c. listoto c = TO (ListOrd c)
   
   [numOrd]  Definition
      
      |- numOrd = TO_of_LinearOrder $<
   
   [num_dt_TY_DEF]  Definition
      
      |- ?rep.
             TYPE_DEFINITION
               (\a0.
                    ! $var$('num_dt').
                        (!a0.
                             (a0 =
                              ind_type$CONSTR 0 ARB (\n. ind_type$BOTTOM)) \/
                             (?a.
                                  (a0 =
                                   (\a.
                                        ind_type$CONSTR (SUC 0) ARB
                                          (ind_type$FCONS a
                                             (\n. ind_type$BOTTOM))) a) /\
                                  $var$('num_dt') a) \/
                             (?a.
                                  (a0 =
                                   (\a.
                                        ind_type$CONSTR (SUC (SUC 0)) ARB
                                          (ind_type$FCONS a
                                             (\n. ind_type$BOTTOM))) a) /\
                                  $var$('num_dt') a) ==>
                             $var$('num_dt') a0) ==>
                        $var$('num_dt') a0) rep
   
   [num_dt_case_def]  Definition
      
      |- (!v f f1. num_dt_CASE zer v f f1 = v) /\
         (!a v f f1. num_dt_CASE (bit1 a) v f f1 = f a) /\
         !a v f f1. num_dt_CASE (bit2 a) v f f1 = f1 a
   
   [num_dt_size_def]  Definition
      
      |- (num_dt_size zer = 0) /\
         (!a. num_dt_size (bit1 a) = 1 + num_dt_size a) /\
         !a. num_dt_size (bit2 a) = 1 + num_dt_size a
   
   [num_to_dt_primitive]  Definition
      
      |- num_to_dt =
         WFREC
           (@R.
                WF R /\ (!n. n <> 0 /\ ODD n ==> R (DIV2 (n - 1)) n) /\
                !n. n <> 0 /\ ~ODD n ==> R (DIV2 (n - 2)) n)
           (\num_to_dt a.
                I
                  (if a = 0 then zer
                   else if ODD a then bit1 (num_to_dt (DIV2 (a - 1)))
                   else bit2 (num_to_dt (DIV2 (a - 2)))))
   
   [numto]  Definition
      
      |- numto = TO numOrd
   
   [qk_numOrd_def]  Definition
      
      |- !m n. qk_numOrd m n = num_dtOrd (num_to_dt m) (num_to_dt n)
   
   [qk_numto]  Definition
      
      |- qk_numto = TO qk_numOrd
   
   [stringto]  Definition
      
      |- stringto = listoto charto
   
   [to_bij]  Definition
      
      |- (!a. TO (apto a) = a) /\ !r. TotOrd r <=> (apto (TO r) = r)
   
   [toto_TY_DEF]  Definition
      
      |- ?rep. TYPE_DEFINITION TotOrd rep
   
   [toto_inv]  Definition
      
      |- !c. toto_inv c = TO (TO_inv (apto c))
   
   [toto_of_LinearOrder]  Definition
      
      |- !r. toto_of_LinearOrder r = TO (TO_of_LinearOrder r)
   
   [LEX_ALT]  Theorem
      
      |- !R U c d.
             (R LEX U) c d <=>
             R (FST c) (FST d) \/ (FST c = FST d) /\ U (SND c) (SND d)
   
   [ListOrd_THM]  Theorem
      
      |- !c.
             (ListOrd c [] [] = EQUAL) /\
             (!b y. ListOrd c [] (b::y) = LESS) /\
             (!a x. ListOrd c (a::x) [] = GREATER) /\
             !a x b y.
                 ListOrd c (a::x) (b::y) =
                 case apto c a b of
                   LESS => LESS
                 | EQUAL => ListOrd c x y
                 | GREATER => GREATER
   
   [NOT_EQ_LESS_IMP]  Theorem
      
      |- !cmp x y.
             apto cmp x y <> LESS ==> (x = y) \/ (apto cmp y x = LESS)
   
   [SLO_LEX]  Theorem
      
      |- !R V.
             StrongLinearOrder R /\ StrongLinearOrder V ==>
             StrongLinearOrder (R LEX V)
   
   [SLO_listorder]  Theorem
      
      |- !V. StrongLinearOrder V ==> StrongLinearOrder (listorder V)
   
   [SPLIT_PAIRS]  Theorem
      
      |- !x y. (x = y) <=> (FST x = FST y) /\ (SND x = SND y)
   
   [STRORD_SLO]  Theorem
      
      |- !R. WeakLinearOrder R ==> StrongLinearOrder (STRORD R)
   
   [StrongLinearOrderExists]  Theorem
      
      |- ?R. StrongLinearOrder R
   
   [StrongLinearOrder_LESS]  Theorem
      
      |- StrongLinearOrder $<
   
   [StrongLinearOrder_of_TO_TO_of_LinearOrder]  Theorem
      
      |- !R.
             irreflexive R ==>
             (StrongLinearOrder_of_TO (TO_of_LinearOrder R) = R)
   
   [StrongOrder_ALT]  Theorem
      
      |- !Z. StrongOrder Z <=> irreflexive Z /\ transitive Z
   
   [Strong_Strong_of]  Theorem
      
      |- !c. StrongLinearOrder (StrongLinearOrder_of_TO (apto c))
   
   [Strong_Strong_of_TO]  Theorem
      
      |- !c. TotOrd c ==> StrongLinearOrder (StrongLinearOrder_of_TO c)
   
   [Strong_toto_inv]  Theorem
      
      |- !c.
             StrongLinearOrder_of_TO (apto (toto_inv c)) =
             relinv (StrongLinearOrder_of_TO (apto c))
   
   [Strong_toto_thm]  Theorem
      
      |- !r.
             StrongLinearOrder r ==>
             (StrongLinearOrder_of_TO (apto (toto_of_LinearOrder r)) = r)
   
   [Strongof_toto_STRORD]  Theorem
      
      |- !c.
             StrongLinearOrder_of_TO (apto c) =
             STRORD (WeakLinearOrder_of_TO (apto c))
   
   [TO_11]  Theorem
      
      |- !r r'. TotOrd r ==> TotOrd r' ==> ((TO r = TO r') <=> (r = r'))
   
   [TO_ListOrd]  Theorem
      
      |- !c. TotOrd (ListOrd c)
   
   [TO_antisym]  Theorem
      
      |- !c. TotOrd c ==> !x y. (c x y = GREATER) <=> (c y x = LESS)
   
   [TO_apto_ID]  Theorem
      
      |- !a. TO (apto a) = a
   
   [TO_apto_TO_ID]  Theorem
      
      |- !r. TotOrd r <=> (apto (TO r) = r)
   
   [TO_apto_TO_IMP]  Theorem
      
      |- !r. TotOrd r ==> (apto (TO r) = r)
   
   [TO_charOrd]  Theorem
      
      |- TotOrd charOrd
   
   [TO_cpn_eqn]  Theorem
      
      |- !c.
             TotOrd c ==>
             (!x y. (c x y = LESS) ==> x <> y) /\
             (!x y. (c x y = GREATER) ==> x <> y) /\
             !x y. (c x y = EQUAL) ==> (x = y)
   
   [TO_equal_eq]  Theorem
      
      |- !c. TotOrd c ==> !x y. (c x y = EQUAL) <=> (x = y)
   
   [TO_exists]  Theorem
      
      |- ?x. TotOrd x
   
   [TO_injection]  Theorem
      
      |- !cp. TotOrd cp ==> !f. ONE_ONE f ==> TotOrd (imageOrd f cp)
   
   [TO_inv_Ord]  Theorem
      
      |- !r. TO_of_LinearOrder (relinv r) = TO_inv (TO_of_LinearOrder r)
   
   [TO_inv_TO_inv]  Theorem
      
      |- !c. TO_inv (TO_inv c) = c
   
   [TO_lexTO]  Theorem
      
      |- !R V. TotOrd R /\ TotOrd V ==> TotOrd (R lexTO V)
   
   [TO_numOrd]  Theorem
      
      |- TotOrd numOrd
   
   [TO_of_LinearOrder_LEX]  Theorem
      
      |- !R V.
             irreflexive R /\ irreflexive V ==>
             (TO_of_LinearOrder (R LEX V) =
              TO_of_LinearOrder R lexTO TO_of_LinearOrder V)
   
   [TO_of_greater_ler]  Theorem
      
      |- !r.
             StrongLinearOrder r ==>
             !x y. (TO_of_LinearOrder r x y = GREATER) <=> r y x
   
   [TO_of_less_rel]  Theorem
      
      |- !r.
             StrongLinearOrder r ==>
             !x y. (TO_of_LinearOrder r x y = LESS) <=> r x y
   
   [TO_onto]  Theorem
      
      |- !a. ?r. (a = TO r) /\ TotOrd r
   
   [TO_qk_numOrd]  Theorem
      
      |- TotOrd qk_numOrd
   
   [TO_refl]  Theorem
      
      |- !c. TotOrd c ==> !x. c x x = EQUAL
   
   [TotOrd_TO_of_LO]  Theorem
      
      |- !r. LinearOrder r ==> TotOrd (TO_of_LinearOrder r)
   
   [TotOrd_TO_of_Strong]  Theorem
      
      |- !r. StrongLinearOrder r ==> TotOrd (TO_of_LinearOrder r)
   
   [TotOrd_TO_of_Weak]  Theorem
      
      |- !r. WeakLinearOrder r ==> TotOrd (TO_of_LinearOrder r)
   
   [TotOrd_apto]  Theorem
      
      |- !c. TotOrd (apto c)
   
   [TotOrd_inv]  Theorem
      
      |- !c. TotOrd c ==> TotOrd (TO_inv c)
   
   [Weak_Weak_of]  Theorem
      
      |- !c. WeakLinearOrder (WeakLinearOrder_of_TO (apto c))
   
   [Weak_toto_inv]  Theorem
      
      |- !c.
             WeakLinearOrder_of_TO (apto (toto_inv c)) =
             relinv (WeakLinearOrder_of_TO (apto c))
   
   [Weak_toto_thm]  Theorem
      
      |- !r.
             WeakLinearOrder r ==>
             (WeakLinearOrder_of_TO (apto (toto_of_LinearOrder r)) = r)
   
   [all_cpn_distinct]  Theorem
      
      |- (LESS <> EQUAL /\ LESS <> GREATER /\ EQUAL <> GREATER) /\
         EQUAL <> LESS /\ GREATER <> LESS /\ GREATER <> EQUAL
   
   [ap_qk_numto_thm]  Theorem
      
      |- apto qk_numto = qk_numOrd
   
   [apcharto_thm]  Theorem
      
      |- apto charto = charOrd
   
   [aplextoto]  Theorem
      
      |- !c v x1 x2 y1 y2.
             apto (c lextoto v) (x1,x2) (y1,y2) =
             case apto c x1 y1 of
               LESS => LESS
             | EQUAL => apto v x2 y2
             | GREATER => GREATER
   
   [aplistoto]  Theorem
      
      |- !c.
             (apto (listoto c) [] [] = EQUAL) /\
             (!b y. apto (listoto c) [] (b::y) = LESS) /\
             (!a x. apto (listoto c) (a::x) [] = GREATER) /\
             !a x b y.
                 apto (listoto c) (a::x) (b::y) =
                 case apto c a b of
                   LESS => LESS
                 | EQUAL => apto (listoto c) x y
                 | GREATER => GREATER
   
   [apnumto_thm]  Theorem
      
      |- apto numto = numOrd
   
   [apto_inv]  Theorem
      
      |- !c. apto (toto_inv c) = TO_inv (apto c)
   
   [charOrd_eq_lem]  Theorem
      
      |- !a b. (numOrd a b = EQUAL) ==> (charOrd (CHR a) (CHR b) = EQUAL)
   
   [charOrd_gt_lem]  Theorem
      
      |- !a b.
             (numOrd a b = GREATER) ==>
             (a < 256 <=> T) ==>
             (charOrd (CHR a) (CHR b) = GREATER)
   
   [charOrd_lt_lem]  Theorem
      
      |- !a b.
             (numOrd a b = LESS) ==>
             (b < 256 <=> T) ==>
             (charOrd (CHR a) (CHR b) = LESS)
   
   [charOrd_thm]  Theorem
      
      |- charOrd = TO_of_LinearOrder $<
   
   [datatype_num_dt]  Theorem
      
      |- DATATYPE (num_dt zer bit1 bit2)
   
   [inv_TO]  Theorem
      
      |- !r. TotOrd r ==> (toto_inv (TO r) = TO (TO_inv r))
   
   [lexTO_ALT]  Theorem
      
      |- !R V.
             TotOrd R /\ TotOrd V ==>
             !(r,u) (r',u').
                 (R lexTO V) (r,u) (r',u') =
                 case R r r' of
                   LESS => LESS
                 | EQUAL => V u u'
                 | GREATER => GREATER
   
   [lexTO_thm]  Theorem
      
      |- !R V.
             TotOrd R /\ TotOrd V ==>
             !x y.
                 (R lexTO V) x y =
                 case R (FST x) (FST y) of
                   LESS => LESS
                 | EQUAL => V (SND x) (SND y)
                 | GREATER => GREATER
   
   [listorder]  Theorem
      
      |- (!l V. listorder V l [] <=> F) /\
         (!s m V. listorder V [] (s::m) <=> T) /\
         !s r m l V.
             listorder V (r::l) (s::m) <=>
             V r s \/ (r = s) /\ listorder V l m
   
   [listorder_ind]  Theorem
      
      |- !P.
             (!V l. P V l []) /\ (!V s m. P V [] (s::m)) /\
             (!V r l s m. P V l m ==> P V (r::l) (s::m)) ==>
             !v v1 v2. P v v1 v2
   
   [num_dtOrd]  Theorem
      
      |- (num_dtOrd zer zer = EQUAL) /\
         (!x. num_dtOrd zer (bit1 x) = LESS) /\
         (!x. num_dtOrd zer (bit2 x) = LESS) /\
         (!x. num_dtOrd (bit1 x) zer = GREATER) /\
         (!x. num_dtOrd (bit2 x) zer = GREATER) /\
         (!y x. num_dtOrd (bit1 x) (bit2 y) = LESS) /\
         (!y x. num_dtOrd (bit2 x) (bit1 y) = GREATER) /\
         (!y x. num_dtOrd (bit1 x) (bit1 y) = num_dtOrd x y) /\
         !y x. num_dtOrd (bit2 x) (bit2 y) = num_dtOrd x y
   
   [num_dtOrd_ind]  Theorem
      
      |- !P.
             P zer zer /\ (!x. P zer (bit1 x)) /\ (!x. P zer (bit2 x)) /\
             (!x. P (bit1 x) zer) /\ (!x. P (bit2 x) zer) /\
             (!x y. P (bit1 x) (bit2 y)) /\ (!x y. P (bit2 x) (bit1 y)) /\
             (!x y. P x y ==> P (bit1 x) (bit1 y)) /\
             (!x y. P x y ==> P (bit2 x) (bit2 y)) ==>
             !v v1. P v v1
   
   [num_dt_11]  Theorem
      
      |- (!a a'. (bit1 a = bit1 a') <=> (a = a')) /\
         !a a'. (bit2 a = bit2 a') <=> (a = a')
   
   [num_dt_Axiom]  Theorem
      
      |- !f0 f1 f2.
             ?fn.
                 (fn zer = f0) /\ (!a. fn (bit1 a) = f1 a (fn a)) /\
                 !a. fn (bit2 a) = f2 a (fn a)
   
   [num_dt_case_cong]  Theorem
      
      |- !M M' v f f1.
             (M = M') /\ ((M' = zer) ==> (v = v')) /\
             (!a. (M' = bit1 a) ==> (f a = f' a)) /\
             (!a. (M' = bit2 a) ==> (f1 a = f1' a)) ==>
             (num_dt_CASE M v f f1 = num_dt_CASE M' v' f' f1')
   
   [num_dt_case_eq]  Theorem
      
      |- (num_dt_CASE x v f f1 = v') <=>
         (x = zer) /\ (v = v') \/ (?n. (x = bit1 n) /\ (f n = v')) \/
         ?n. (x = bit2 n) /\ (f1 n = v')
   
   [num_dt_distinct]  Theorem
      
      |- (!a. zer <> bit1 a) /\ (!a. zer <> bit2 a) /\
         !a' a. bit1 a <> bit2 a'
   
   [num_dt_induction]  Theorem
      
      |- !P.
             P zer /\ (!n. P n ==> P (bit1 n)) /\ (!n. P n ==> P (bit2 n)) ==>
             !n. P n
   
   [num_dt_nchotomy]  Theorem
      
      |- !nn. (nn = zer) \/ (?n. nn = bit1 n) \/ ?n. nn = bit2 n
   
   [numeralOrd]  Theorem
      
      |- !x y.
             (numOrd ZERO ZERO = EQUAL) /\ (numOrd ZERO (BIT1 y) = LESS) /\
             (numOrd ZERO (BIT2 y) = LESS) /\
             (numOrd (BIT1 x) ZERO = GREATER) /\
             (numOrd (BIT2 x) ZERO = GREATER) /\
             (numOrd (BIT1 x) (BIT1 y) = numOrd x y) /\
             (numOrd (BIT2 x) (BIT2 y) = numOrd x y) /\
             (numOrd (BIT1 x) (BIT2 y) =
              case numOrd x y of
                LESS => LESS
              | EQUAL => LESS
              | GREATER => GREATER) /\
             (numOrd (BIT2 x) (BIT1 y) =
              case numOrd x y of
                LESS => LESS
              | EQUAL => GREATER
              | GREATER => GREATER)
   
   [onto_apto]  Theorem
      
      |- !r. TotOrd r <=> ?a. r = apto a
   
   [pre_aplextoto]  Theorem
      
      |- !c v x y.
             apto (c lextoto v) x y =
             case apto c (FST x) (FST y) of
               LESS => LESS
             | EQUAL => apto v (SND x) (SND y)
             | GREATER => GREATER
   
   [qk_numeralOrd]  Theorem
      
      |- !x y.
             (qk_numOrd ZERO ZERO = EQUAL) /\
             (qk_numOrd ZERO (BIT1 y) = LESS) /\
             (qk_numOrd ZERO (BIT2 y) = LESS) /\
             (qk_numOrd (BIT1 x) ZERO = GREATER) /\
             (qk_numOrd (BIT2 x) ZERO = GREATER) /\
             (qk_numOrd (BIT1 x) (BIT1 y) = qk_numOrd x y) /\
             (qk_numOrd (BIT2 x) (BIT2 y) = qk_numOrd x y) /\
             (qk_numOrd (BIT1 x) (BIT2 y) = LESS) /\
             (qk_numOrd (BIT2 x) (BIT1 y) = GREATER)
   
   [totoEEtrans]  Theorem
      
      |- !c x y z.
             ((apto c x y = EQUAL) /\ (apto c y z = EQUAL) ==>
              (apto c x z = EQUAL)) /\
             ((apto c x y = EQUAL) /\ (apto c z y = EQUAL) ==>
              (apto c x z = EQUAL))
   
   [totoELtrans]  Theorem
      
      |- !c x y z.
             (apto c x y = EQUAL) /\ (apto c y z = LESS) ==>
             (apto c x z = LESS)
   
   [totoGGtrans]  Theorem
      
      |- !c x y z.
             (apto c y x = GREATER) /\ (apto c z y = GREATER) ==>
             (apto c x z = LESS)
   
   [totoGLtrans]  Theorem
      
      |- !c x y z.
             (apto c y x = GREATER) /\ (apto c y z = LESS) ==>
             (apto c x z = LESS)
   
   [totoLEtrans]  Theorem
      
      |- !c x y z.
             (apto c x y = LESS) /\ (apto c y z = EQUAL) ==>
             (apto c x z = LESS)
   
   [totoLGtrans]  Theorem
      
      |- !c x y z.
             (apto c x y = LESS) /\ (apto c z y = GREATER) ==>
             (apto c x z = LESS)
   
   [totoLLtrans]  Theorem
      
      |- !c x y z.
             (apto c x y = LESS) /\ (apto c y z = LESS) ==>
             (apto c x z = LESS)
   
   [toto_Strong_thm]  Theorem
      
      |- !c. toto_of_LinearOrder (StrongLinearOrder_of_TO (apto c)) = c
   
   [toto_Weak_thm]  Theorem
      
      |- !c. toto_of_LinearOrder (WeakLinearOrder_of_TO (apto c)) = c
   
   [toto_antisym]  Theorem
      
      |- !c x y. (apto c x y = GREATER) <=> (apto c y x = LESS)
   
   [toto_cpn_eqn]  Theorem
      
      |- (!c x y. (apto c x y = EQUAL) ==> (x = y)) /\
         (!c x y. (apto c x y = LESS) ==> x <> y) /\
         !c x y. (apto c x y = GREATER) ==> x <> y
   
   [toto_equal_eq]  Theorem
      
      |- !c x y. (apto c x y = EQUAL) <=> (x = y)
   
   [toto_equal_imp]  Theorem
      
      |- !cmp phi.
             LinearOrder phi /\ (cmp = toto_of_LinearOrder phi) ==>
             !x y. ((x = y) <=> T) ==> (apto cmp x y = EQUAL)
   
   [toto_equal_imp_eq]  Theorem
      
      |- !c x y. (apto c x y = EQUAL) ==> (x = y)
   
   [toto_equal_sym]  Theorem
      
      |- !c x y. (apto c x y = EQUAL) <=> (apto c y x = EQUAL)
   
   [toto_glneq]  Theorem
      
      |- (!c x y. (apto c x y = LESS) ==> x <> y) /\
         !c x y. (apto c x y = GREATER) ==> x <> y
   
   [toto_inv_toto_inv]  Theorem
      
      |- !c. toto_inv (toto_inv c) = c
   
   [toto_not_less_refl]  Theorem
      
      |- !cmp h. (apto cmp h h = LESS) <=> F
   
   [toto_refl]  Theorem
      
      |- !c x. apto c x x = EQUAL
   
   [toto_swap_cases]  Theorem
      
      |- !c x y.
             apto c y x =
             case apto c x y of
               LESS => GREATER
             | EQUAL => EQUAL
             | GREATER => LESS
   
   [toto_thm]  Theorem
      
      |- !c.
             (!x y. (apto c x y = EQUAL) <=> (x = y)) /\
             (!x y. (apto c x y = GREATER) <=> (apto c y x = LESS)) /\
             !x y z.
                 (apto c x y = LESS) /\ (apto c y z = LESS) ==>
                 (apto c x z = LESS)
   
   [toto_trans_less]  Theorem
      
      |- (!c x y z.
              (apto c x y = LESS) /\ (apto c y z = LESS) ==>
              (apto c x z = LESS)) /\
         (!c x y z.
              (apto c x y = LESS) /\ (apto c z y = GREATER) ==>
              (apto c x z = LESS)) /\
         (!c x y z.
              (apto c y x = GREATER) /\ (apto c z y = GREATER) ==>
              (apto c x z = LESS)) /\
         (!c x y z.
              (apto c y x = GREATER) /\ (apto c y z = LESS) ==>
              (apto c x z = LESS)) /\
         (!c x y z.
              (apto c x y = LESS) /\ (apto c y z = EQUAL) ==>
              (apto c x z = LESS)) /\
         !c x y z.
             (apto c x y = EQUAL) /\ (apto c y z = LESS) ==>
             (apto c x z = LESS)
   
   [toto_unequal_imp]  Theorem
      
      |- !cmp phi.
             LinearOrder phi /\ (cmp = toto_of_LinearOrder phi) ==>
             !x y.
                 ((x = y) <=> F) ==>
                 if phi x y then apto cmp x y = LESS
                 else apto cmp x y = GREATER
   
   [trichotomous_ALT]  Theorem
      
      |- !R. trichotomous R <=> !x y. ~R x y /\ ~R y x ==> (x = y)
   
   
*)
end


Source File Identifier index Theory binding index

HOL 4, Kananaskis-13