Theory "Coder"

Parents Decode

Signature

Constant	Type
blist_coder	:num -> (α -> bool) # (β -> γ list) # (bitstring, α) state_option -> (α list -> bool) # (β list -> γ list) # (bitstring, α list) state_option
bnum_coder	:num -> (num -> bool) -> (num -> bool) # (num -> bitstring) # (bitstring, num) state_option
bool_coder	:(bool -> bool) -> (bool -> bool) # (bool -> bitstring) # (bitstring, bool) state_option
decode	:(α -> bool) -> (bitstring, α) state_option -> bitstring -> α
decoder	:(α -> bool) # (α -> bitstring) # (bitstring, α) state_option -> bitstring -> α
domain	:(α -> bool) # (α -> bitstring) # (bitstring, α) state_option -> α -> bool
encoder	:(α -> bool) # (α -> bitstring) # (bitstring, α) state_option -> α -> bitstring
list_coder	:(α -> bool) # (β -> bitstring) # (bitstring, α) state_option -> (α list -> bool) # (β list -> bitstring) # (bitstring, α list) state_option
num_coder	:(num -> bool) -> (num -> bool) # (num -> bitstring) # (bitstring, num) state_option
option_coder	:(α -> bool) # (β -> bitstring) # (bitstring, α) state_option -> (α option -> bool) # (β option -> bitstring) # (bitstring, α option) state_option
prod_coder	:(α -> bool) # (γ -> bitstring) # (bitstring, α) state_option -> (β -> bool) # (δ -> bitstring) # (bitstring, β) state_option -> (α # β -> bool) # (γ # δ -> bitstring) # (bitstring, α # β) state_option
sum_coder	:(α -> bool) # (γ -> bitstring) # (bitstring, α) state_option -> (β -> bool) # (δ -> bitstring) # (bitstring, β) state_option -> (α + β -> bool) # (γ + δ -> bitstring) # (bitstring, α + β) state_option
tree_coder	:(α -> bool) # (β -> bitstring) # (bitstring, α) state_option -> (α tree -> bool) # (β tree -> bitstring) # (bitstring, α tree) state_option
unit_coder	:(unit -> bool) -> (unit -> bool) # (unit -> bitstring) # (bitstring, unit) state_option
wf_coder	:(α -> bool) # (α -> bitstring) # (bitstring, α) state_option -> bool

Definitions

decode_def

|- ∀p d l. decode p d l = case d l of NONE => @x. p x | SOME (x,v2) => x

wf_coder_def

|- ∀p e d. wf_coder (p,e,d) ⇔ wf_pred p ∧ wf_encoder p e ∧ (d = enc2dec p e)

domain_def

|- ∀p e d. domain (p,e,d) = p

encoder_def

|- ∀p e d. encoder (p,e,d) = e

decoder_def

|- ∀p e d. decoder (p,e,d) = decode p d

unit_coder_def

|- ∀p. unit_coder p = (p,encode_unit,decode_unit p)

bool_coder_def

|- ∀p. bool_coder p = (p,encode_bool,decode_bool p)

prod_coder_def

|- ∀p1 e1 d1 p2 e2 d2.
     prod_coder (p1,e1,d1) (p2,e2,d2) =
     (lift_prod p1 p2,encode_prod e1 e2,decode_prod (lift_prod p1 p2) d1 d2)

sum_coder_def

|- ∀p1 e1 d1 p2 e2 d2.
     sum_coder (p1,e1,d1) (p2,e2,d2) =
     (lift_sum p1 p2,encode_sum e1 e2,decode_sum (lift_sum p1 p2) d1 d2)

option_coder_def

|- ∀p e d.
     option_coder (p,e,d) =
     (lift_option p,encode_option e,decode_option (lift_option p) d)

list_coder_def

|- ∀p e d.
     list_coder (p,e,d) = (EVERY p,encode_list e,decode_list (EVERY p) d)

blist_coder_def

|- ∀m p e d.
     blist_coder m (p,e,d) =
     (lift_blist m p,encode_blist m e,decode_blist (lift_blist m p) m d)

num_coder_def

|- ∀p. num_coder p = (p,encode_num,decode_num p)

bnum_coder_def

|- ∀m p. bnum_coder m p = (p,encode_bnum m,decode_bnum m p)

tree_coder_def

|- ∀p e d.
     tree_coder (p,e,d) =
     (lift_tree p,encode_tree e,decode_tree (lift_tree p) d)

Theorems

decode_encode

|- ∀p e x. wf_encoder p e ∧ p x ⇒ (decode p (enc2dec p e) (e x) = x)

wf_coder

|- ∀c. wf_coder c ⇒ ∀x. domain c x ⇒ (decoder c (encoder c x) = x)

wf_coder_closed

|- ∀c. wf_coder c ⇒ ∀l. domain c (decoder c l)

wf_coder_op

|- ∀p e f.
     (∃x. p x) ∧ wf_encoder p e ∧ (∀x. p x ⇒ (e x = f x)) ⇒
     wf_coder (p,e,enc2dec p f)

wf_coder_unit

|- ∀p. wf_pred p ⇒ wf_coder (unit_coder p)

wf_coder_bool

|- ∀p. wf_pred p ⇒ wf_coder (bool_coder p)

wf_coder_prod

|- ∀c1 c2. wf_coder c1 ∧ wf_coder c2 ⇒ wf_coder (prod_coder c1 c2)

wf_coder_sum

|- ∀c1 c2. wf_coder c1 ∧ wf_coder c2 ⇒ wf_coder (sum_coder c1 c2)

wf_coder_option

|- ∀c. wf_coder c ⇒ wf_coder (option_coder c)

wf_coder_list

|- ∀c. wf_coder c ⇒ wf_coder (list_coder c)

wf_coder_blist

|- ∀m c. wf_coder c ⇒ wf_coder (blist_coder m c)

wf_coder_num

|- ∀p. wf_pred p ⇒ wf_coder (num_coder p)

wf_coder_bnum

|- ∀m p. wf_pred_bnum m p ⇒ wf_coder (bnum_coder m p)

wf_coder_tree

|- ∀c. wf_coder c ⇒ wf_coder (tree_coder c)