- enc2dec_none
-
|- ∀p e l. (enc2dec p e l = NONE) ⇔ ∀x t. p x ⇒ l ≠ e x ++ t
- enc2dec_some
-
|- ∀p e l x t.
wf_encoder p e ⇒ ((enc2dec p e l = SOME (x,t)) ⇔ p x ∧ (l = e x ++ t))
- enc2dec_some_alt
-
|- ∀p e l x.
wf_encoder p e ⇒
((enc2dec p e l = SOME x) ⇔ p (FST x) ∧ (l = e (FST x) ++ SND x))
- wf_enc2dec
-
|- ∀p e. wf_encoder p e ⇒ wf_decoder p (enc2dec p e)
- dec2enc_some
-
|- ∀p d x l. wf_decoder p d ⇒ ((dec2enc d x = l) ∧ p x ⇔ (d l = SOME (x,[])))
- decode_dec2enc
-
|- ∀p d x. wf_decoder p d ∧ p x ⇒ (d (dec2enc d x) = SOME (x,[]))
- decode_dec2enc_append
-
|- ∀p d x t. wf_decoder p d ∧ p x ⇒ (d (dec2enc d x ++ t) = SOME (x,t))
- wf_dec2enc
-
|- ∀p d. wf_decoder p d ⇒ wf_encoder p (dec2enc d)
- dec2enc_enc2dec
-
|- ∀p e x. wf_encoder p e ∧ p x ⇒ (dec2enc (enc2dec p e) x = e x)
- enc2dec_dec2enc
-
|- ∀p d. wf_decoder p d ⇒ (enc2dec p (dec2enc d) = d)
- wf_decode_unit
-
|- wf_decoder p (decode_unit p)
- dec2enc_decode_unit
-
|- ∀p x. p x ⇒ (dec2enc (decode_unit p) x = encode_unit x)
- decode_unit
-
|- decode_unit p l = if p () then SOME ((),l) else NONE
- wf_decode_bool
-
|- ∀p. wf_decoder p (decode_bool p)
- dec2enc_decode_bool
-
|- ∀p x. p x ⇒ (dec2enc (decode_bool p) x = encode_bool x)
- decode_bool
-
|- decode_bool p l =
case l of [] => NONE | h::t => if p h then SOME (h,t) else NONE
- wf_decode_prod
-
|- ∀p1 p2 d1 d2.
wf_decoder p1 d1 ∧ wf_decoder p2 d2 ⇒
wf_decoder (lift_prod p1 p2) (decode_prod (lift_prod p1 p2) d1 d2)
- dec2enc_decode_prod
-
|- ∀p1 p2 d1 d2 x.
wf_decoder p1 d1 ∧ wf_decoder p2 d2 ∧ lift_prod p1 p2 x ⇒
(dec2enc (decode_prod (lift_prod p1 p2) d1 d2) x =
encode_prod (dec2enc d1) (dec2enc d2) x)
- encode_then_decode_prod
-
|- ∀p1 p2 e1 e2 l t.
wf_encoder p1 e1 ∧ wf_encoder p2 e2 ∧ lift_prod p1 p2 l ⇒
(decode_prod (lift_prod p1 p2) (enc2dec p1 e1) (enc2dec p2 e2)
(encode_prod e1 e2 l ++ t) =
SOME (l,t))
- decode_prod
-
|- wf_decoder p1 d1 ∧ wf_decoder p2 d2 ⇒
(decode_prod (lift_prod p1 p2) d1 d2 l =
case d1 l of
NONE => NONE
| SOME (x,t) =>
case d2 t of NONE => NONE | SOME (y,t') => SOME ((x,y),t'))
- wf_decode_sum
-
|- ∀p1 p2 d1 d2.
wf_decoder p1 d1 ∧ wf_decoder p2 d2 ⇒
wf_decoder (lift_sum p1 p2) (decode_sum (lift_sum p1 p2) d1 d2)
- dec2enc_decode_sum
-
|- ∀p1 p2 d1 d2 x.
wf_decoder p1 d1 ∧ wf_decoder p2 d2 ∧ lift_sum p1 p2 x ⇒
(dec2enc (decode_sum (lift_sum p1 p2) d1 d2) x =
encode_sum (dec2enc d1) (dec2enc d2) x)
- encode_then_decode_sum
-
|- ∀p1 p2 e1 e2 l t.
wf_encoder p1 e1 ∧ wf_encoder p2 e2 ∧ lift_sum p1 p2 l ⇒
(decode_sum (lift_sum p1 p2) (enc2dec p1 e1) (enc2dec p2 e2)
(encode_sum e1 e2 l ++ t) =
SOME (l,t))
- decode_sum
-
|- wf_decoder p1 d1 ∧ wf_decoder p2 d2 ⇒
(decode_sum (lift_sum p1 p2) d1 d2 l =
case l of
[] => NONE
| T::t => (case d1 t of NONE => NONE | SOME (x,t') => SOME (INL x,t'))
| F::t => case d2 t of NONE => NONE | SOME (x,t') => SOME (INR x,t'))
- wf_decode_option
-
|- ∀p d.
wf_decoder p d ⇒
wf_decoder (lift_option p) (decode_option (lift_option p) d)
- dec2enc_decode_option
-
|- ∀p d x.
wf_decoder p d ∧ lift_option p x ⇒
(dec2enc (decode_option (lift_option p) d) x =
encode_option (dec2enc d) x)
- encode_then_decode_option
-
|- ∀p e l t.
wf_encoder p e ∧ lift_option p l ⇒
(decode_option (lift_option p) (enc2dec p e) (encode_option e l ++ t) =
SOME (l,t))
- decode_option
-
|- wf_decoder p d ⇒
(decode_option (lift_option p) d l =
case l of
[] => NONE
| T::t => (case d t of NONE => NONE | SOME (x,t') => SOME (SOME x,t'))
| F::t => SOME (NONE,t))
- wf_decode_list
-
|- ∀p d. wf_decoder p d ⇒ wf_decoder (EVERY p) (decode_list (EVERY p) d)
- dec2enc_decode_list
-
|- ∀p d x.
wf_decoder p d ∧ EVERY p x ⇒
(dec2enc (decode_list (EVERY p) d) x = encode_list (dec2enc d) x)
- encode_then_decode_list
-
|- ∀p e l t.
wf_encoder p e ∧ EVERY p l ⇒
(decode_list (EVERY p) (enc2dec p e) (encode_list e l ++ t) = SOME (l,t))
- decode_list
-
|- wf_decoder p d ⇒
(decode_list (EVERY p) d l =
case l of
[] => NONE
| T::t =>
(case d t of
NONE => NONE
| SOME (x,t') =>
case decode_list (EVERY p) d t' of
NONE => NONE
| SOME (xs,t'') => SOME (x::xs,t''))
| F::t => SOME ([],t))
- wf_decode_blist
-
|- ∀m p d.
wf_decoder p d ⇒
wf_decoder (lift_blist m p) (decode_blist (lift_blist m p) m d)
- dec2enc_decode_blist
-
|- ∀m p d l.
wf_decoder p d ∧ lift_blist m p l ⇒
(dec2enc (decode_blist (lift_blist m p) m d) l =
encode_blist m (dec2enc d) l)
- encode_then_decode_blist
-
|- ∀m p e l t.
wf_encoder p e ∧ lift_blist m p l ⇒
(decode_blist (lift_blist m p) m (enc2dec p e)
(encode_blist m e l ++ t) =
SOME (l,t))
- decode_blist
-
|- wf_decoder p d ⇒
(decode_blist (lift_blist m p) m d l =
case m of
0 => SOME ([],l)
| SUC n =>
case d l of
NONE => NONE
| SOME (x,t) =>
case decode_blist (lift_blist n p) n d t of
NONE => NONE
| SOME (xs,t') => SOME (x::xs,t'))
- wf_decode_num
-
|- ∀p. wf_decoder p (decode_num p)
- dec2enc_decode_num
-
|- ∀p x. p x ⇒ (dec2enc (decode_num p) x = encode_num x)
- decode_num_total
-
|- decode_num (K T) l =
case l of
[] => NONE
| [T] => NONE
| T::T::t => SOME (0,t)
| T::F::t =>
(case decode_num (K T) t of
NONE => NONE
| SOME (v,t') => SOME (2 * v + 1,t'))
| F::t' =>
case decode_num (K T) t' of
NONE => NONE
| SOME (v,t') => SOME (2 * v + 2,t')
- decode_num
-
|- decode_num p l =
case l of
[] => NONE
| [T] => NONE
| T::T::t => if p 0 then SOME (0,t) else NONE
| T::F::t =>
(case decode_num (K T) t of
NONE => NONE
| SOME (v,t') => if p (2 * v + 1) then SOME (2 * v + 1,t') else NONE)
| F::t' =>
case decode_num (K T) t' of
NONE => NONE
| SOME (v,t') => if p (2 * v + 2) then SOME (2 * v + 2,t') else NONE
- dec_bnum_def_compute
-
|- (∀l. dec_bnum 0 l = SOME (0,l)) ∧
(∀m l.
dec_bnum (NUMERAL (BIT1 m)) l =
case l of
[] => NONE
| h::t =>
case dec_bnum (NUMERAL (BIT1 m) − 1) t of
NONE => NONE
| SOME (n,t') => SOME (2 * n + if h then 1 else 0,t')) ∧
∀m l.
dec_bnum (NUMERAL (BIT2 m)) l =
case l of
[] => NONE
| h::t =>
case dec_bnum (NUMERAL (BIT1 m)) t of
NONE => NONE
| SOME (n,t') => SOME (2 * n + if h then 1 else 0,t')
- dec_bnum_lt
-
|- ∀m l n t. (dec_bnum m l = SOME (n,t)) ⇒ n < 2 ** m
- dec_bnum_inj
-
|- ∀m l n t. (dec_bnum m l = SOME (n,t)) ⇒ (l = encode_bnum m n ++ t)
- wf_decode_bnum
-
|- ∀m p. wf_pred_bnum m p ⇒ wf_decoder p (decode_bnum m p)
- dec2enc_decode_bnum
-
|- ∀m p x.
wf_pred_bnum m p ∧ p x ⇒ (dec2enc (decode_bnum m p) x = encode_bnum m x)
- decode_bnum
-
|- wf_pred_bnum m p ⇒
(decode_bnum m p l =
case dec_bnum m l of
NONE => NONE
| SOME (n,t) => if p n then SOME (n,t) else NONE)
- wf_decode_tree
-
|- ∀p d.
wf_decoder p d ⇒ wf_decoder (lift_tree p) (decode_tree (lift_tree p) d)
- decode_tree
-
|- wf_decoder p d ⇒
(decode_tree (lift_tree p) d l =
case d l of
NONE => NONE
| SOME (a,t) =>
case
decode_list (EVERY (lift_tree p)) (decode_tree (lift_tree p) d) t
of
NONE => NONE
| SOME (ts,t') => SOME (Node a ts,t'))