Theory "EncodeVar"

Parents     Coder

Signature

Constant Type
of_length :num -> 'a list -> bool
fixed_width :num -> ('a -> bool) # ('a -> bool list) # (bool list -> ('a # bool list) option) -> bool

Definitions

fixed_width_def 
|- !n c. fixed_width n c = !x. domain c x ==> (LENGTH (encoder c x) = n)
of_length_def 
|- !l n. l IN of_length n = (LENGTH l = n)

Theorems

fixed_width_univ 
|- !phi c n.
     wf_coder c /\ fixed_width n c ==>
     ((!x. domain c x ==> phi x) = !w::of_length n. phi (decoder c w))
of_length_univ_suc 
|- !phi n. (!w::of_length (SUC n). phi w) = !x (w::of_length n). phi (x::w)
of_length_univ_zero 
|- !phi. (!w::of_length 0. phi w) = phi []
fixed_width_exists 
|- !phi c n.
     wf_coder c /\ fixed_width n c ==>
     ((?x. domain c x /\ phi x) = ?w::of_length n. phi (decoder c w))
of_length_exists_suc 
|- !phi n. (?w::of_length (SUC n). phi w) = ?x (w::of_length n). phi (x::w)
of_length_exists_zero 
|- !phi. (?w::of_length 0. phi w) = phi []
fixed_width_unit 
|- !p. fixed_width 0 (unit_coder p)
fixed_width_bool 
|- !p. fixed_width 1 (bool_coder p)
fixed_width_prod 
|- !c1 c2 n1 n2.
     fixed_width n1 c1 /\ fixed_width n2 c2 ==>
     fixed_width (n1 + n2) (prod_coder c1 c2)
fixed_width_sum 
|- !c1 c2 n.
     fixed_width n c1 /\ fixed_width n c2 ==>
     fixed_width (SUC n) (sum_coder c1 c2)
fixed_width_bnum 
|- !m p. fixed_width m (bnum_coder m p)