Theory: prelim

Parents

Types

ordering(Arity = 0)

Constants

list_compare_tupled :('a -> 'b -> ordering) # 'a list # 'b list -> ordering
ii_internal_dest_ordering :ordering -> bool recspace
LESS :ordering
list_compare :('a -> 'b -> ordering) -> 'a list -> 'b list -> ordering
GREATER :ordering
EQUAL :ordering
ordering_size :ordering -> num
compare :ordering -> 'a -> 'a -> 'a -> 'a
list_merge :('a -> 'a -> bool) -> 'a list -> 'a list -> 'a list
ordering_case :'a -> 'a -> 'a -> ordering -> 'a
ii_internalprelim0 :ordering
ii_internalprelim1 :ordering
ii_internalprelim2 :ordering
ii_internal_mk_ordering :bool recspace -> ordering
list_merge_tupled :('a -> 'a -> bool) # 'a list # 'a list -> 'a list

Definitions

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

EQUAL_def

|- EQUAL = ii_internalprelim1

GREATER_def

|- GREATER = ii_internalprelim2

ii_internalprelim0_def

|- ii_internalprelim0 =
   ii_internal_mk_ordering (CONSTR 0 (@x. T) (\n. BOTTOM))

ii_internalprelim1_def

|- ii_internalprelim1 =
   ii_internal_mk_ordering (CONSTR (SUC 0) (@x. T) (\n. BOTTOM))

ii_internalprelim2_def

|- ii_internalprelim2 =
   ii_internal_mk_ordering (CONSTR (SUC (SUC 0)) (@x. T) (\n. BOTTOM))

LESS_def

|- LESS = ii_internalprelim0

list_compare_arg_munge_def

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

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.
        pair_case
          (\v v1.
             pair_case
               (\v2 v3.
                  list_case (list_case EQUAL (\v10 v11. LESS) v3)
                    (\v6 v7.
                       list_case GREATER
                         (\v12 v13.
                            compare (v v6 v12) LESS
                              (list_compare_tupled' (v,v7,v13)) GREATER) v3)
                    v2) v1) a)

list_merge_arg_munge_def

|- !x x1 x2. list_merge x x1 x2 = list_merge_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,l1,y::l2) (a_lt,x::l1,y::l2)) /\
        !l2 l1 y x a_lt. ~a_lt x y ==> R (a_lt,x::l1,l2) (a_lt,x::l1,y::l2))
     (\list_merge_tupled' a.
        pair_case
          (\v v1.
             pair_case
               (\v2 v3.
                  list_case (list_case [] (\v10 v11. v10::v11) v3)
                    (\v6 v7.
                       list_case (v6::v7)
                         (\v12 v13.
                            (if v v6 v12 then
                               v6::list_merge_tupled' (v,v7,v12::v13)
                             else
                               v12::list_merge_tupled' (v,v6::v7,v13))) v3)
                    v2) v1) a)

ordering_case_def

|- (!v v1 v2. ordering_case v v1 v2 LESS = v) /\
   (!v v1 v2. ordering_case v v1 v2 EQUAL = v1) /\
   !v v1 v2. ordering_case v v1 v2 GREATER = v2

ordering_repfns

|- (!a. ii_internal_mk_ordering (ii_internal_dest_ordering a) = a) /\
   !r.
     (\a0.
        !'ordering'.
          (!a0.
             (a0 = CONSTR 0 (@x. T) (\n. BOTTOM)) \/
             (a0 = CONSTR (SUC 0) (@x. T) (\n. BOTTOM)) \/
             (a0 = CONSTR (SUC (SUC 0)) (@x. T) (\n. BOTTOM)) ==>
             'ordering' a0) ==>
          'ordering' a0) r =
     (ii_internal_dest_ordering (ii_internal_mk_ordering r) = r)

ordering_size_def

|- (ordering_size LESS = 0) /\ (ordering_size EQUAL = 0) /\
   (ordering_size GREATER = 0)

ordering_TY_DEF

|- ?rep.
     TYPE_DEFINITION
       (\a0.
          !'ordering'.
            (!a0.
               (a0 = CONSTR 0 (@x. T) (\n. BOTTOM)) \/
               (a0 = CONSTR (SUC 0) (@x. T) (\n. BOTTOM)) \/
               (a0 = CONSTR (SUC (SUC 0)) (@x. T) (\n. BOTTOM)) ==>
               'ordering' a0) ==>
            'ordering' a0) rep

Theorems

compare_equal

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

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)

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

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 l1 (y::l2)) /\
        (~a_lt x y ==> P a_lt (x::l1) l2) ==>
        P a_lt (x::l1) (y::l2)) ==>
     !v v1 v2. P v v1 v2

ordering_Axiom

|- !f0 f1 f2. ?fn. (fn LESS = f0) /\ (fn EQUAL = f1) /\ (fn GREATER = f2)

ordering_case_cong

|- !v2' v2 v1' v1 v' v M' M.
     (M = M') /\ ((M' = LESS) ==> (v = v')) /\
     ((M' = EQUAL) ==> (v1 = v1')) /\ ((M' = GREATER) ==> (v2 = v2')) ==>
     (ordering_case v v1 v2 M = ordering_case v' v1' v2' M')

ordering_distinct

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

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)

ordering_induction

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

ordering_nchotomy

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