Theory "Encode"

Parents rich_list

Signature

Type	Arity
tree	1
listEncode0	1
Constant	Type
wf_pred_bnum	:num -> (num -> bool) -> bool
wf_pred	:('a -> bool) -> bool
wf_encoder	:('a -> bool) -> ('a -> bool list) -> bool
tree_size	:('a -> num) -> 'a tree -> num
tree_case	:('a -> 'a tree list -> 'b) -> 'a tree -> 'b
tree1_size	:('a -> num) -> 'a tree list -> num
mk_tree	:'a recspace -> 'a tree
mk_listEncode0	:'a recspace -> 'a listEncode0
lift_tree_tupled	:('a -> bool) # 'a tree -> bool
lift_tree	:('a -> bool) -> 'a tree -> bool
lift_sum	:('a -> bool) -> ('b -> bool) -> 'a + 'b -> bool
lift_prod	:('a -> bool) -> ('b -> bool) -> 'a # 'b -> bool
lift_option	:('a -> bool) -> 'a option -> bool
lift_blist	:num -> ('a -> bool) -> 'a list -> bool
encode_unit	:one -> bool list
encode_tree_tupled	:('a -> bool list) # 'a tree -> bool list
encode_tree	:('a -> bool list) -> 'a tree -> bool list
encode_sum	:('a -> bool list) -> ('b -> bool list) -> 'a + 'b -> bool list
encode_prod	:('a -> bool list) -> ('b -> bool list) -> 'a # 'b -> bool list
encode_option	:('a -> bool list) -> 'a option -> bool list
encode_num	:num -> bool list
encode_list	:('a -> bool list) -> 'a list -> bool list
encode_bool	:bool -> bool list
encode_bnum	:num -> num -> bool list
encode_blist	:num -> ('b -> 'a list) -> 'b list -> 'a list
dest_tree	:'a tree -> 'a recspace
dest_listEncode0	:'a listEncode0 -> 'a recspace
collision_free	:num -> (num -> bool) -> bool
biprefix	:'a list -> 'a list -> bool
Node	:'a -> 'a tree list -> 'a tree
Encode4	:'a -> 'a tree list -> 'a tree
Encode3	:'a tree -> 'a listEncode0 -> 'a listEncode0
Encode2	:'a listEncode0
Encode1	:'a -> 'a listEncode0 -> 'a tree

Definitions

biprefix_def

|- !a b. biprefix a b = IS_PREFIX a b \/ IS_PREFIX b a

wf_pred_def

|- !p. wf_pred p = ?x. p x

wf_encoder_def

|- !p e.
     wf_encoder p e = !x y. p x /\ p y /\ IS_PREFIX (e x) (e y) ==> (x = y)

encode_unit_def

|- !v0. encode_unit v0 = []

encode_bool_def

|- !x. encode_bool x = [x]

encode_prod_def

|- !xb yb x y. encode_prod xb yb (x,y) = xb x ++ yb y

lift_prod_def

|- !p1 p2 x. lift_prod p1 p2 x = p1 (FST x) /\ p2 (SND x)

encode_sum_def

|- (!xb yb x. encode_sum xb yb (INL x) = T::xb x) /\
   !xb yb y. encode_sum xb yb (INR y) = F::yb y

lift_sum_def

|- !p1 p2 x. lift_sum p1 p2 x = case x of INL x1 -> p1 x1 || INR x2 -> p2 x2

encode_option_def

|- (!xb. encode_option xb NONE = [F]) /\
   !xb x. encode_option xb (SOME x) = T::xb x

lift_option_def

|- !p x. lift_option p x = case x of NONE -> T || SOME y -> p y

encode_list_def

|- (!xb. encode_list xb [] = [F]) /\
   !xb x xs. encode_list xb (x::xs) = T::(xb x ++ encode_list xb xs)

encode_blist_def

|- (!e l. encode_blist 0 e l = []) /\
   !m e l. encode_blist (SUC m) e l = e (HD l) ++ encode_blist m e (TL l)

lift_blist_def

|- !m p x. lift_blist m p x = EVERY p x /\ (LENGTH x = m)

encode_num_primitive_def

|- encode_num =
   WFREC
     (@R.
        WF R /\ (!n. ~(n = 0) /\ EVEN n ==> R ((n - 2) DIV 2) n) /\
        !n. ~(n = 0) /\ ~EVEN n ==> R ((n - 1) DIV 2) n)
     (\encode_num n.
        I
          (if n = 0 then
             [T; T]
           else
             (if EVEN n then
                F::encode_num ((n - 2) DIV 2)
              else
                T::F::encode_num ((n - 1) DIV 2))))

encode_bnum_def

|- (!n. encode_bnum 0 n = []) /\
   !m n. encode_bnum (SUC m) n = ~EVEN n::encode_bnum m (n DIV 2)

collision_free_def

|- !m p.
     collision_free m p =
     !x y. p x /\ p y /\ (x MOD 2 ** m = y MOD 2 ** m) ==> (x = y)

wf_pred_bnum_def

|- !m p. wf_pred_bnum m p = wf_pred p /\ !x. p x ==> x < 2 ** m

tree_TY_DEF

|- ?rep.
     TYPE_DEFINITION
       (\a0'.
          !'tree' 'listEncode0'.
            (!a0'.
               (?a0 a1.
                  (a0' =
                   (\a0 a1.
                      ind_type$CONSTR 0 a0 (FCONS a1 (\n. ind_type$BOTTOM)))
                     a0 a1) /\ 'listEncode0' a1) ==>
               'tree' a0') /\
            (!a1'.
               (a1' =
                ind_type$CONSTR (SUC 0) (@v. T) (\n. ind_type$BOTTOM)) \/
               (?a0 a1.
                  (a1' =
                   (\a0 a1.
                      ind_type$CONSTR (SUC (SUC 0)) (@v. T)
                        (FCONS a0 (FCONS a1 (\n. ind_type$BOTTOM)))) a0 a1) /\
                  'tree' a0 /\ 'listEncode0' a1) ==>
               'listEncode0' a1') ==>
            'tree' a0') rep

tree_repfns

|- (!a. mk_tree (dest_tree a) = a) /\
   !r.
     (\a0'.
        !'tree' 'listEncode0'.
          (!a0'.
             (?a0 a1.
                (a0' =
                 (\a0 a1.
                    ind_type$CONSTR 0 a0 (FCONS a1 (\n. ind_type$BOTTOM))) a0
                   a1) /\ 'listEncode0' a1) ==>
             'tree' a0') /\
          (!a1'.
             (a1' = ind_type$CONSTR (SUC 0) (@v. T) (\n. ind_type$BOTTOM)) \/
             (?a0 a1.
                (a1' =
                 (\a0 a1.
                    ind_type$CONSTR (SUC (SUC 0)) (@v. T)
                      (FCONS a0 (FCONS a1 (\n. ind_type$BOTTOM)))) a0 a1) /\
                'tree' a0 /\ 'listEncode0' a1) ==>
             'listEncode0' a1') ==>
          'tree' a0') r =
     (dest_tree (mk_tree r) = r)

listEncode0_TY_DEF

|- ?rep.
     TYPE_DEFINITION
       (\a1'.
          !'tree' 'listEncode0'.
            (!a0'.
               (?a0 a1.
                  (a0' =
                   (\a0 a1.
                      ind_type$CONSTR 0 a0 (FCONS a1 (\n. ind_type$BOTTOM)))
                     a0 a1) /\ 'listEncode0' a1) ==>
               'tree' a0') /\
            (!a1'.
               (a1' =
                ind_type$CONSTR (SUC 0) (@v. T) (\n. ind_type$BOTTOM)) \/
               (?a0 a1.
                  (a1' =
                   (\a0 a1.
                      ind_type$CONSTR (SUC (SUC 0)) (@v. T)
                        (FCONS a0 (FCONS a1 (\n. ind_type$BOTTOM)))) a0 a1) /\
                  'tree' a0 /\ 'listEncode0' a1) ==>
               'listEncode0' a1') ==>
            'listEncode0' a1') rep

listEncode0_repfns

|- (!a. mk_listEncode0 (dest_listEncode0 a) = a) /\
   !r.
     (\a1'.
        !'tree' 'listEncode0'.
          (!a0'.
             (?a0 a1.
                (a0' =
                 (\a0 a1.
                    ind_type$CONSTR 0 a0 (FCONS a1 (\n. ind_type$BOTTOM))) a0
                   a1) /\ 'listEncode0' a1) ==>
             'tree' a0') /\
          (!a1'.
             (a1' = ind_type$CONSTR (SUC 0) (@v. T) (\n. ind_type$BOTTOM)) \/
             (?a0 a1.
                (a1' =
                 (\a0 a1.
                    ind_type$CONSTR (SUC (SUC 0)) (@v. T)
                      (FCONS a0 (FCONS a1 (\n. ind_type$BOTTOM)))) a0 a1) /\
                'tree' a0 /\ 'listEncode0' a1) ==>
             'listEncode0' a1') ==>
          'listEncode0' a1') r =
     (dest_listEncode0 (mk_listEncode0 r) = r)

Encode1_def

|- Encode1 =
   (\a0 a1.
      mk_tree
        ((\a0 a1. ind_type$CONSTR 0 a0 (FCONS a1 (\n. ind_type$BOTTOM))) a0
           (dest_listEncode0 a1)))

Encode2_def

|- Encode2 =
   mk_listEncode0 (ind_type$CONSTR (SUC 0) (@v. T) (\n. ind_type$BOTTOM))

Encode3_def

|- Encode3 =
   (\a0 a1.
      mk_listEncode0
        ((\a0 a1.
            ind_type$CONSTR (SUC (SUC 0)) (@v. T)
              (FCONS a0 (FCONS a1 (\n. ind_type$BOTTOM)))) (dest_tree a0)
           (dest_listEncode0 a1)))

Encode4

|- Encode4 =
   (\a0 a1.
      Encode1 a0
        ((@fn. (fn [] = Encode2) /\ !a0 a1. fn (a0::a1) = Encode3 a0 (fn a1))
           a1))

Node

|- Node = Encode4

tree_case_def

|- !f a0 a1. tree_case f (Node a0 a1) = f a0 a1

tree_size_def

|- (!f a0 a1. tree_size f (Node a0 a1) = 1 + (f a0 + tree1_size f a1)) /\
   (!f. tree1_size f [] = 0) /\
   !f a0 a1. tree1_size f (a0::a1) = 1 + (tree_size f a0 + tree1_size f a1)

encode_tree_tupled_primitive_def

|- encode_tree_tupled =
   WFREC (@R. WF R /\ !a e ts a'. MEM a' ts ==> R (e,a') (e,Node a ts))
     (\encode_tree_tupled a'.
        case a' of
           (e,Node a ts) ->
             I (e a ++ encode_list (\a. encode_tree_tupled (e,a)) ts))

encode_tree_curried_def

|- !x x1. encode_tree x x1 = encode_tree_tupled (x,x1)

lift_tree_tupled_primitive_def

|- lift_tree_tupled =
   WFREC (@R. WF R /\ !a p ts a'. MEM a' ts ==> R (p,a') (p,Node a ts))
     (\lift_tree_tupled a'.
        case a' of
           (p,Node a ts) -> I (p a /\ EVERY (\a. lift_tree_tupled (p,a)) ts))

lift_tree_curried_def

|- !x x1. lift_tree x x1 = lift_tree_tupled (x,x1)

Theorems

biprefix_refl

|- !x. biprefix x x

biprefix_sym

|- !x y. biprefix x y ==> biprefix y x

biprefix_append

|- !a b c d. biprefix (a ++ b) (c ++ d) ==> biprefix a c

biprefix_cons

|- !a b c d. biprefix (a::b) (c::d) = (a = c) /\ biprefix b d

biprefix_appends

|- !a b c. biprefix (a ++ b) (a ++ c) = biprefix b c

wf_encoder_alt

|- wf_encoder p e = !x y. p x /\ p y /\ biprefix (e x) (e y) ==> (x = y)

wf_encoder_eq

|- !p e f. wf_encoder p e /\ (!x. p x ==> (e x = f x)) ==> wf_encoder p f

wf_encoder_total

|- !p e. wf_encoder (K T) e ==> wf_encoder p e

wf_encode_unit

|- !p. wf_encoder p encode_unit

wf_encode_bool

|- !p. wf_encoder p encode_bool

encode_prod_alt

|- !xb yb p. encode_prod xb yb p = xb (FST p) ++ yb (SND p)

wf_encode_prod

|- !p1 p2 e1 e2.
     wf_encoder p1 e1 /\ wf_encoder p2 e2 ==>
     wf_encoder (lift_prod p1 p2) (encode_prod e1 e2)

wf_encode_sum

|- !p1 p2 e1 e2.
     wf_encoder p1 e1 /\ wf_encoder p2 e2 ==>
     wf_encoder (lift_sum p1 p2) (encode_sum e1 e2)

wf_encode_option

|- !p e. wf_encoder p e ==> wf_encoder (lift_option p) (encode_option e)

wf_encode_list

|- !p e. wf_encoder p e ==> wf_encoder (EVERY p) (encode_list e)

encode_list_cong

|- !l1 l2 f1 f2.
     (l1 = l2) /\ (!x. MEM x l2 ==> (f1 x = f2 x)) ==>
     (encode_list f1 l1 = encode_list f2 l2)

lift_blist_suc

|- !n p h t. lift_blist (SUC n) p (h::t) = p h /\ lift_blist n p t

wf_encode_blist

|- !m p e. wf_encoder p e ==> wf_encoder (lift_blist m p) (encode_blist m e)

encode_num_def

|- encode_num n =
   (if n = 0 then
      [T; T]
    else
      (if EVEN n then
         F::encode_num ((n - 2) DIV 2)
       else
         T::F::encode_num ((n - 1) DIV 2)))

encode_num_ind

|- !P.
     (!n.
        (~(n = 0) /\ EVEN n ==> P ((n - 2) DIV 2)) /\
        (~(n = 0) /\ ~EVEN n ==> P ((n - 1) DIV 2)) ==>
        P n) ==>
     !v. P v

wf_encode_num

|- !p. wf_encoder p encode_num

wf_pred_bnum_total

|- !m. wf_pred_bnum m (\x. x < 2 ** m)

wf_pred_bnum

|- !m p. wf_pred_bnum m p ==> collision_free m p

encode_bnum_length

|- !m n. LENGTH (encode_bnum m n) = m

encode_bnum_inj

|- !m x y.
     x < 2 ** m /\ y < 2 ** m /\ (encode_bnum m x = encode_bnum m y) ==>
     (x = y)

wf_encode_bnum_collision_free

|- !m p. wf_encoder p (encode_bnum m) = collision_free m p

wf_encode_bnum

|- !m p. wf_pred_bnum m p ==> wf_encoder p (encode_bnum m)

datatype_tree

|- DATATYPE (tree Node)

tree_11

|- !a0 a1 a0' a1'. (Node a0 a1 = Node a0' a1') = (a0 = a0') /\ (a1 = a1')

tree_case_cong

|- !M M' f.
     (M = M') /\ (!a0 a1. (M' = Node a0 a1) ==> (f a0 a1 = f' a0 a1)) ==>
     (tree_case f M = tree_case f' M')

tree_nchotomy

|- !t. ?a l. t = Node a l

tree_Axiom

|- !f0 f1 f2.
     ?fn0 fn1.
       (!a0 a1. fn0 (Node a0 a1) = f0 a0 a1 (fn1 a1)) /\ (fn1 [] = f1) /\
       !a0 a1. fn1 (a0::a1) = f2 a0 a1 (fn0 a0) (fn1 a1)

tree_induction

|- !P0 P1.
     (!l. P1 l ==> !a. P0 (Node a l)) /\ P1 [] /\
     (!t l. P0 t /\ P1 l ==> P1 (t::l)) ==>
     (!t. P0 t) /\ !l. P1 l

tree_ind

|- !p. (!a ts. (!t. MEM t ts ==> p t) ==> p (Node a ts)) ==> !t. p t

encode_tree_def

|- encode_tree e (Node a ts) = e a ++ encode_list (encode_tree e) ts

lift_tree_def

|- lift_tree p (Node a ts) = p a /\ EVERY (lift_tree p) ts

wf_encode_tree

|- !p e. wf_encoder p e ==> wf_encoder (lift_tree p) (encode_tree e)