Theory "prelim"

Parents list

Signature

Type	Arity
ordering	0
Constant	Type
ordering_size	:ordering -> num
ordering_case	:'a -> 'a -> 'a -> ordering -> 'a
ordering2num	:ordering -> num
num2ordering	:num -> ordering
list_merge_tupled	:('a -> 'a -> bool) # 'a list # 'a list -> 'a list
list_merge	:('a -> 'a -> bool) -> 'a list -> 'a list -> 'a list
list_compare_tupled	:('a -> 'b -> ordering) # 'a list # 'b list -> ordering
list_compare	:('a -> 'b -> ordering) -> 'a list -> 'b list -> ordering
compare	:ordering -> 'a -> 'a -> 'a -> 'a
LESS	:ordering
GREATER	:ordering
EQUAL	:ordering

Definitions

ordering_TY_DEF

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

ordering_BIJ

|- (!a. num2ordering (ordering2num a) = a) /\
   !r. (\n. n < 3) r = (ordering2num (num2ordering r) = r)

LESS_def

|- LESS = num2ordering 0

EQUAL_def

|- EQUAL = num2ordering 1

GREATER_def

|- GREATER = num2ordering 2

ordering_size_def

|- !x. ordering_size x = 0

ordering_case

|- !v0 v1 v2 x.
     (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)

compare_def

|- (!lt eq gt. compare LESS lt eq gt = lt) /\
   (!lt eq gt. compare EQUAL lt eq gt = eq) /\
   !lt eq gt. compare GREATER lt eq gt = gt

list_compare_tupled_primitive_def

|- list_compare_tupled =
   WFREC (@R. WF R /\ !y x l2 l1 cmp. R (cmp,l1,l2) (cmp,x::l1,y::l2))
     (\list_compare_tupled a.
        case a of
           (cmp,[],[]) -> I EQUAL
        || (cmp,[],v10::v11) -> I LESS
        || (cmp,x::l1,[]) -> I GREATER
        || (cmp,x::l1,y::l2) ->
             I
               (compare (cmp x y) LESS (list_compare_tupled (cmp,l1,l2))
                  GREATER))

list_compare_curried_def

|- !x x1 x2. list_compare x x1 x2 = list_compare_tupled (x,x1,x2)

list_merge_tupled_primitive_def

|- list_merge_tupled =
   WFREC
     (@R.
        WF R /\
        (!l2 l1 y x a_lt.
           ~a_lt x y ==> R (a_lt,x::l1,l2) (a_lt,x::l1,y::l2)) /\
        !l2 l1 y x a_lt. a_lt x y ==> R (a_lt,l1,y::l2) (a_lt,x::l1,y::l2))
     (\list_merge_tupled a.
        case a of
           (a_lt,[],[]) -> I []
        || (a_lt,[],v10::v11) -> I (v10::v11)
        || (a_lt,x::l1,[]) -> I (x::l1)
        || (a_lt,x::l1,y::l2) ->
             I
               (if a_lt x y then
                  x::list_merge_tupled (a_lt,l1,y::l2)
                else
                  y::list_merge_tupled (a_lt,x::l1,l2)))

list_merge_curried_def

|- !x x1 x2. list_merge x x1 x2 = list_merge_tupled (x,x1,x2)

Theorems

num2ordering_ordering2num

|- !a. num2ordering (ordering2num a) = a

ordering2num_num2ordering

|- !r. r < 3 = (ordering2num (num2ordering r) = r)

num2ordering_11

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

ordering2num_11

|- !a a'. (ordering2num a = ordering2num a') = (a = a')

num2ordering_ONTO

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

ordering2num_ONTO

|- !r. r < 3 = ?a. r = ordering2num a

num2ordering_thm

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

ordering2num_thm

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

ordering_EQ_ordering

|- !a a'. (a = a') = (ordering2num a = ordering2num a')

ordering_case_def

|- (!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

datatype_ordering

|- DATATYPE (ordering LESS EQUAL GREATER)

ordering_distinct

|- ~(LESS = EQUAL) /\ ~(LESS = GREATER) /\ ~(EQUAL = GREATER)

ordering_case_cong

|- !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_nchotomy

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

ordering_Axiom

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

ordering_induction

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

ordering_eq_dec

|- (!x. (x = x) = T) /\ ((LESS = EQUAL) = F) /\ ((LESS = GREATER) = F) /\
   ((EQUAL = GREATER) = F) /\ ((EQUAL = LESS) = F) /\
   ((GREATER = LESS) = F) /\ ((GREATER = EQUAL) = F)

list_compare_ind

|- !P.
     (!cmp. P cmp [] []) /\ (!cmp v8 v9. P cmp [] (v8::v9)) /\
     (!cmp v4 v5. P cmp (v4::v5) []) /\
     (!cmp x l1 y l2. P cmp l1 l2 ==> P cmp (x::l1) (y::l2)) ==>
     !v v1 v2. P v v1 v2

list_compare_def

|- (list_compare cmp [] [] = EQUAL) /\
   (list_compare cmp [] (v8::v9) = LESS) /\
   (list_compare cmp (v4::v5) [] = GREATER) /\
   (list_compare cmp (x::l1) (y::l2) =
    compare (cmp x y) LESS (list_compare cmp l1 l2) GREATER)

compare_equal

|- (!x y. (cmp x y = EQUAL) = (x = y)) ==>
   !l1 l2. (list_compare cmp l1 l2 = EQUAL) = (l1 = l2)

list_merge_ind

|- !P.
     (!a_lt v4 v5. P a_lt (v4::v5) []) /\ (!a_lt. P a_lt [] []) /\
     (!a_lt v8 v9. P a_lt [] (v8::v9)) /\
     (!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

list_merge_def

|- (list_merge a_lt (v4::v5) [] = v4::v5) /\ (list_merge a_lt [] [] = []) /\
   (list_merge a_lt [] (v8::v9) = v8::v9) /\
   (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))