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 cpn_BIJ : thm
    val cpn_CASE : thm
    val cpn_TY_DEF : thm
    val cpn_size_def : thm
    val imageOrd : thm
    val lexTO : thm
    val lextoto : thm
    val listorder_curried : thm
    val listorder_tupled_primitive : thm
    val listoto : thm
    val numOrd : thm
    val num_dtOrd_curried : thm
    val num_dtOrd_tupled_primitive : 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 NOT_EQ_LESS_IMP : thm
    val StrongOrder_ALT : thm
    val TO_11 : thm
    val TO_apto_ID : thm
    val TO_apto_TO_ID : thm
    val TO_apto_TO_IMP : thm
    val TO_numOrd : thm
    val TO_onto : thm
    val TO_qk_numOrd : thm
    val TO_refl : thm
    val TotOrd_TO_of_Strong : thm
    val TotOrd_apto : 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 charOrd_eq_lem : thm
    val charOrd_gt_lem : thm
    val charOrd_lt_lem : thm
    val cpn2num_11 : thm
    val cpn2num_ONTO : thm
    val cpn2num_num2cpn : thm
    val cpn2num_thm : thm
    val cpn_Axiom : thm
    val cpn_EQ_cpn : thm
    val cpn_case_cong : thm
    val cpn_case_def : thm
    val cpn_distinct : thm
    val cpn_induction : thm
    val cpn_nchotomy : thm
    val datatype_cpn : thm
    val datatype_num_dt : thm
    val listorder : thm
    val listorder_ind : thm
    val num2cpn_11 : thm
    val num2cpn_ONTO : thm
    val num2cpn_cpn2num : thm
    val num2cpn_thm : 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_distinct : thm
    val num_dt_induction : thm
    val num_dt_nchotomy : thm
    val numeralOrd : thm
    val onto_apto : 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_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_not_less_refl : thm
    val toto_refl : thm
    val toto_swap_cases : thm
    val toto_trans_less : thm
    val toto_unequal_imp : thm

  val toto_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [string] 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 | _ => 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 GREATER => F | _ => T

   [charOrd]  Definition

      |- !a b. charOrd a b = numOrd (ORD a) (ORD b)

   [charto]  Definition

      |- charto = TO charOrd

   [cpn_BIJ]  Definition

      |- (!a. num2cpn (cpn2num a) = a) /\
         !r. (\n. n < 3) r <=> (cpn2num (num2cpn r) = r)

   [cpn_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) (cpn2num x)

   [cpn_TY_DEF]  Definition

      |- ?rep. TYPE_DEFINITION (\n. n < 3) rep

   [cpn_size_def]  Definition

      |- !x. cpn_size x = 0

   [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)

   [listorder_curried]  Definition

      |- !x x1 x2. listorder x x1 x2 <=> listorder_tupled (x,x1,x2)

   [listorder_tupled_primitive]  Definition

      |- listorder_tupled =
         WFREC (@R. WF R /\ !s r m l V. R (V,l,m) (V,r::l,s::m))
           (\listorder_tupled a.
              case a of
                (V,l,[]) => I F
              | (V,[],s::m) => I T
              | (V,r::l',s::m) =>
                  I (V r s \/ (r = s) /\ listorder_tupled (V,l',m)))

   [listoto]  Definition

      |- !c. listoto c = TO (ListOrd c)

   [numOrd]  Definition

      |- numOrd = TO_of_LinearOrder $<

   [num_dtOrd_curried]  Definition

      |- !x x1. num_dtOrd x x1 = num_dtOrd_tupled (x,x1)

   [num_dtOrd_tupled_primitive]  Definition

      |- num_dtOrd_tupled =
         WFREC
           (@R.
              WF R /\ (!y x. R (x,y) (bit1 x,bit1 y)) /\
              !y x. R (x,y) (bit2 x,bit2 y))
           (\num_dtOrd_tupled a.
              case a of
                (zer,zer) => I EQUAL
              | (zer,bit1 x) => I LESS
              | (zer,bit2 x') => I LESS
              | (bit1 x'',zer) => I GREATER
              | (bit1 x'',bit1 y'') => I (num_dtOrd_tupled (x'',y''))
              | (bit1 x'',bit2 y) => I LESS
              | (bit2 x''',zer) => I GREATER
              | (bit2 x''',bit1 y') => I GREATER
              | (bit2 x''',bit2 y''') => I (num_dtOrd_tupled (x''',y''')))

   [num_dt_TY_DEF]  Definition

      |- ?rep.
           TYPE_DEFINITION
             (\a0.
                !'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) /\ 'num_dt' a) \/
                     (?a.
                        (a0 =
                         (\a.
                            ind_type$CONSTR (SUC (SUC 0)) ARB
                              (ind_type$FCONS a (\n. ind_type$BOTTOM)))
                           a) /\ 'num_dt' a) ==>
                     'num_dt' a0) ==>
                  '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 n.
              I
                (if n = 0 then zer
                 else if ODD n then bit1 (num_to_dt (DIV2 (n - 1)))
                 else bit2 (num_to_dt (DIV2 (n - 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)

   [NOT_EQ_LESS_IMP]  Theorem

      |- !cmp x y.
           apto cmp x y <> LESS ==> (x = y) \/ (apto cmp y x = LESS)

   [StrongOrder_ALT]  Theorem

      |- !Z. StrongOrder Z <=> irreflexive Z /\ transitive Z

   [TO_11]  Theorem

      |- !r r'. TotOrd r ==> TotOrd r' ==> ((TO r = TO r') <=> (r = r'))

   [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_numOrd]  Theorem

      |- TotOrd numOrd

   [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_Strong]  Theorem

      |- !r. StrongLinearOrder r ==> TotOrd (TO_of_LinearOrder r)

   [TotOrd_apto]  Theorem

      |- !c. TotOrd (apto c)

   [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

   [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)

   [cpn2num_11]  Theorem

      |- !a a'. (cpn2num a = cpn2num a') <=> (a = a')

   [cpn2num_ONTO]  Theorem

      |- !r. r < 3 <=> ?a. r = cpn2num a

   [cpn2num_num2cpn]  Theorem

      |- !r. r < 3 <=> (cpn2num (num2cpn r) = r)

   [cpn2num_thm]  Theorem

      |- (cpn2num LESS = 0) /\ (cpn2num EQUAL = 1) /\ (cpn2num GREATER = 2)

   [cpn_Axiom]  Theorem

      |- !x0 x1 x2. ?f. (f LESS = x0) /\ (f EQUAL = x1) /\ (f GREATER = x2)

   [cpn_EQ_cpn]  Theorem

      |- !a a'. (a = a') <=> (cpn2num a = cpn2num a')

   [cpn_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')

   [cpn_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

   [cpn_distinct]  Theorem

      |- LESS <> EQUAL /\ LESS <> GREATER /\ EQUAL <> GREATER

   [cpn_induction]  Theorem

      |- !P. P EQUAL /\ P GREATER /\ P LESS ==> !a. P a

   [cpn_nchotomy]  Theorem

      |- !a. (a = LESS) \/ (a = EQUAL) \/ (a = GREATER)

   [datatype_cpn]  Theorem

      |- DATATYPE (cpn LESS EQUAL GREATER)

   [datatype_num_dt]  Theorem

      |- DATATYPE (num_dt zer bit1 bit2)

   [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

   [num2cpn_11]  Theorem

      |- !r r'.
           r < 3 ==> r' < 3 ==> ((num2cpn r = num2cpn r') <=> (r = r'))

   [num2cpn_ONTO]  Theorem

      |- !a. ?r. (a = num2cpn r) /\ r < 3

   [num2cpn_cpn2num]  Theorem

      |- !a. num2cpn (cpn2num a) = a

   [num2cpn_thm]  Theorem

      |- (num2cpn 0 = LESS) /\ (num2cpn 1 = EQUAL) /\ (num2cpn 2 = GREATER)

   [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_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 GREATER => GREATER | _ => LESS) /\
           (numOrd (BIT2 x) (BIT1 y) =
            case numOrd x y of LESS => LESS | _ => GREATER)

   [onto_apto]  Theorem

      |- !r. TotOrd r <=> ?a. r = apto a

   [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_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_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_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


*)
end


Source File Identifier index Theory binding index

HOL 4, Kananaskis-10