Theory "Decode"

Parents Encode

Signature

Constant	Type
wf_decoder	:('a -> bool) -> (bool list -> ('a # bool list) option) -> bool
enc2dec	:('a -> bool) -> ('a -> bool list) -> bool list -> ('a # bool list) option
decode_unit	:(one -> bool) -> bool list -> (one # bool list) option
decode_tree	:('a tree -> bool) -> (bool list -> ('a # bool list) option) -> bool list -> ('a tree # bool list) option
decode_sum	:('a + 'b -> bool) -> (bool list -> ('a # bool list) option) -> (bool list -> ('b # bool list) option) -> bool list -> (('a + 'b) # bool list) option
decode_prod	:('a # 'b -> bool) -> (bool list -> ('a # bool list) option) -> (bool list -> ('b # bool list) option) -> bool list -> (('a # 'b) # bool list) option
decode_option	:('a option -> bool) -> (bool list -> ('a # bool list) option) -> bool list -> ('a option # bool list) option
decode_num	:(num -> bool) -> bool list -> (num # bool list) option
decode_list	:('a list -> bool) -> (bool list -> ('a # bool list) option) -> bool list -> ('a list # bool list) option
decode_bool	:(bool -> bool) -> bool list -> (bool # bool list) option
decode_bnum	:num -> (num -> bool) -> bool list -> (num # bool list) option
decode_blist	:('a list -> bool) -> num -> (bool list -> ('a # bool list) option) -> bool list -> ('a list # bool list) option
dec_bnum	:num -> bool list -> (num # bool list) option
dec2enc	:(bool list -> ('a # bool list) option) -> 'a -> bool list

Definitions

wf_decoder_def

|- !p d.
     wf_decoder p d =
     !x.
       (if p x then
          ?a. !b c. (d b = SOME (x,c)) = (b = a ++ c)
        else
          !a b. ~(d a = SOME (x,b)))

enc2dec_def

|- !p e l.
     enc2dec p e l =
     (if ?x t. p x /\ (l = e x ++ t) then
        SOME @(x,t). p x /\ (l = e x ++ t)
      else
        NONE)

dec2enc_def

|- !d x. dec2enc d x = @l. d l = SOME (x,[])

decode_unit_def

|- !p. decode_unit p = enc2dec p encode_unit

decode_bool_def

|- !p. decode_bool p = enc2dec p encode_bool

decode_prod_def

|- !p d1 d2.
     decode_prod p d1 d2 = enc2dec p (encode_prod (dec2enc d1) (dec2enc d2))

decode_sum_def

|- !p d1 d2.
     decode_sum p d1 d2 = enc2dec p (encode_sum (dec2enc d1) (dec2enc d2))

decode_option_def

|- !p d. decode_option p d = enc2dec p (encode_option (dec2enc d))

decode_list_def

|- !p d. decode_list p d = enc2dec p (encode_list (dec2enc d))

decode_blist_def

|- !p m d. decode_blist p m d = enc2dec p (encode_blist m (dec2enc d))

decode_num_def

|- !p. decode_num p = enc2dec p encode_num

decode_bnum_def

|- !m p. decode_bnum m p = enc2dec p (encode_bnum m)

dec_bnum_def

|- (!l. dec_bnum 0 l = SOME (0,l)) /\
   !m l.
     dec_bnum (SUC m) l =
     case l of
        [] -> NONE
     || h::t ->
          case dec_bnum m t of
             NONE -> NONE
          || SOME (n,t') -> SOME (2 * n + (if h then 1 else 0),t')

decode_tree_def

|- !p d. decode_tree p d = enc2dec p (encode_tree (dec2enc d))

Theorems

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_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'))