Theory "Coder"

Parents Decode

Signature

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