Theory "Encode"

Parents rich_list

Signature

Type	Arity
tree	1
Constant	Type
Node	:α -> α tree list -> α tree
biprefix	:α list reln
collision_free	:num -> (num -> bool) -> bool
encode_blist	:num -> (β -> α list) -> β list -> α list
encode_bnum	:num -> num -> bitstring
encode_bool	:bool -> bitstring
encode_list	:(α -> bitstring) -> α list -> bitstring
encode_num	:num -> bitstring
encode_option	:(α -> bitstring) -> α option -> bitstring
encode_prod	:(α -> bitstring) -> (β -> bitstring) -> α # β -> bitstring
encode_sum	:(α -> bitstring) -> (β -> bitstring) -> α + β -> bitstring
encode_tree	:(α -> bitstring) -> α tree -> bitstring
encode_tree_tupled	:(α -> bitstring) # α tree -> bitstring
encode_unit	:unit -> bitstring
lift_blist	:num -> (α -> bool) -> α list -> bool
lift_option	:(α -> bool) -> α option -> bool
lift_prod	:(α -> bool) -> (β -> bool) -> α # β -> bool
lift_sum	:(α -> bool) -> (β -> bool) -> α + β -> bool
lift_tree	:(α -> bool) -> α tree -> bool
lift_tree_tupled	:(α -> bool) # α tree -> bool
tree1_size	:(α -> num) -> α tree list -> num
tree_CASE	:α tree -> (α -> α tree list -> β) -> β
tree_size	:(α -> num) -> α tree -> num
wf_encoder	:(α -> bool) -> (α -> bitstring) -> bool
wf_pred	:(α -> bool) -> bool
wf_pred_bnum	:num -> (num -> bool) -> bool

Definitions

biprefix_def

|- ∀a b. biprefix a b ⇔ b ≼ a ∨ a ≼ b

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 ∧ e y ≼ e x ⇒ (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' 'list @ind_typeEncode0' .
            (∀a0'.
               (∃a0 a1.
                  (a0' =
                   (λa0 a1.
                      ind_type$CONSTR 0 a0
                        (ind_type$FCONS a1 (λn. ind_type$BOTTOM))) a0 a1) ∧
                  'list @ind_typeEncode0' a1) ⇒
               'tree' a0') ∧
            (∀a1'.
               (a1' = ind_type$CONSTR (SUC 0) ARB (λn. ind_type$BOTTOM)) ∨
               (∃a0 a1.
                  (a1' =
                   (λa0 a1.
                      ind_type$CONSTR (SUC (SUC 0)) ARB
                        (ind_type$FCONS a0
                           (ind_type$FCONS a1 (λn. ind_type$BOTTOM)))) a0
                     a1) ∧ 'tree' a0 ∧ 'list @ind_typeEncode0' a1) ⇒
               'list @ind_typeEncode0' a1') ⇒
            'tree' a0') rep

tree_case_def

|- ∀a0 a1 f. tree_CASE (Node a0 a1) f = 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)

encode_blist_def_compute

|- (∀e l. encode_blist 0 e l = []) ∧
   (∀m e l.
      encode_blist (NUMERAL (BIT1 m)) e l =
      e (HD l) ++ encode_blist (NUMERAL (BIT1 m) − 1) e (TL l)) ∧
   ∀m e l.
     encode_blist (NUMERAL (BIT2 m)) e l =
     e (HD l) ++ encode_blist (NUMERAL (BIT1 m)) e (TL l)

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

encode_bnum_def_compute

|- (∀n. encode_bnum 0 n = []) ∧
   (∀m n.
      encode_bnum (NUMERAL (BIT1 m)) n =
      ¬EVEN n::encode_bnum (NUMERAL (BIT1 m) − 1) (n DIV 2)) ∧
   ∀m n.
     encode_bnum (NUMERAL (BIT2 m)) n =
     ¬EVEN n::encode_bnum (NUMERAL (BIT1 m)) (n DIV 2)

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 M f = tree_CASE M' f')

tree_nchotomy

|- ∀tt. ∃a l. tt = 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)