Theory "Coder"

Parents Decode

Signature

Constant	Type
wf_coder	:('a -> bool) # ('a -> bool list) # (bool list -> ('a # bool list) option) -> bool
unit_coder	:(one -> bool) -> (one -> bool) # (one -> bool list) # (bool list -> (one # bool list) option)
tree_coder	:('a -> bool) # ('b -> bool list) # (bool list -> ('a # bool list) option) -> ('a tree -> bool) # ('b tree -> bool list) # (bool list -> ('a tree # bool list) option)
sum_coder	:('a -> bool) # ('c -> bool list) # (bool list -> ('a # bool list) option) -> ('b -> bool) # ('d -> bool list) # (bool list -> ('b # bool list) option) -> ('a + 'b -> bool) # ('c + 'd -> bool list) # (bool list -> (('a + 'b) # bool list) option)
prod_coder	:('a -> bool) # ('c -> bool list) # (bool list -> ('a # bool list) option) -> ('b -> bool) # ('d -> bool list) # (bool list -> ('b # bool list) option) -> ('a # 'b -> bool) # ('c # 'd -> bool list) # (bool list -> (('a # 'b) # bool list) option)
option_coder	:('a -> bool) # ('b -> bool list) # (bool list -> ('a # bool list) option) -> ('a option -> bool) # ('b option -> bool list) # (bool list -> ('a option # bool list) option)
num_coder	:(num -> bool) -> (num -> bool) # (num -> bool list) # (bool list -> (num # bool list) option)
list_coder	:('a -> bool) # ('b -> bool list) # (bool list -> ('a # bool list) option) -> ('a list -> bool) # ('b list -> bool list) # (bool list -> ('a list # bool list) option)
encoder	:('a -> bool) # ('a -> bool list) # (bool list -> ('a # bool list) option) -> 'a -> bool list
domain	:('a -> bool) # ('a -> bool list) # (bool list -> ('a # bool list) option) -> 'a -> bool
decoder	:('a -> bool) # ('a -> bool list) # (bool list -> ('a # bool list) option) -> bool list -> 'a
decode	:('a -> bool) -> (bool list -> ('a # bool list) option) -> bool list -> 'a
bool_coder	:(bool -> bool) -> (bool -> bool) # (bool -> bool list) # (bool list -> (bool # bool list) option)
bnum_coder	:num -> (num -> bool) -> (num -> bool) # (num -> bool list) # (bool list -> (num # bool list) option)
blist_coder	:num -> ('a -> bool) # ('b -> 'c list) # (bool list -> ('a # bool list) option) -> ('a list -> bool) # ('b list -> 'c list) # (bool list -> ('a list # bool list) option)

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)