Theory "EncodeVar"

Parents Coder

Signature

Constant	Type
fixed_width	:num -> (α -> bool) # (α -> bitstring) # (bitstring, α) state_option -> bool
of_length	:num -> α list -> bool

fixed_width_def

|- ∀n c. fixed_width n c ⇔ ∀x. domain c x ⇒ (LENGTH (encoder c x) = n)

of_length_def

|- ∀l n. l ∈ of_length n ⇔ (LENGTH l = n)

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)