Structure DecodeTheory

signature DecodeTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val dec2enc_def : thm
    val dec_bnum_def : thm
    val decode_blist_def : thm
    val decode_bnum_def : thm
    val decode_bool_def : thm
    val decode_list_def : thm
    val decode_num_def : thm
    val decode_option_def : thm
    val decode_prod_def : thm
    val decode_sum_def : thm
    val decode_tree_def : thm
    val decode_unit_def : thm
    val enc2dec_def : thm
    val wf_decoder_def : thm
  
  (*  Theorems  *)
    val dec2enc_decode_blist : thm
    val dec2enc_decode_bnum : thm
    val dec2enc_decode_bool : thm
    val dec2enc_decode_list : thm
    val dec2enc_decode_num : thm
    val dec2enc_decode_option : thm
    val dec2enc_decode_prod : thm
    val dec2enc_decode_sum : thm
    val dec2enc_decode_unit : thm
    val dec2enc_enc2dec : thm
    val dec2enc_some : thm
    val dec_bnum_compute : thm
    val dec_bnum_inj : thm
    val dec_bnum_lt : thm
    val decode_blist : thm
    val decode_bnum : thm
    val decode_bool : thm
    val decode_dec2enc : thm
    val decode_dec2enc_append : thm
    val decode_list : thm
    val decode_num : thm
    val decode_num_total : thm
    val decode_option : thm
    val decode_prod : thm
    val decode_sum : thm
    val decode_tree : thm
    val decode_unit : thm
    val enc2dec_dec2enc : thm
    val enc2dec_none : thm
    val enc2dec_some : thm
    val enc2dec_some_alt : thm
    val encode_then_decode_blist : thm
    val encode_then_decode_list : thm
    val encode_then_decode_option : thm
    val encode_then_decode_prod : thm
    val encode_then_decode_sum : thm
    val wf_dec2enc : thm
    val wf_decode_blist : thm
    val wf_decode_bnum : thm
    val wf_decode_bool : thm
    val wf_decode_list : thm
    val wf_decode_num : thm
    val wf_decode_option : thm
    val wf_decode_prod : thm
    val wf_decode_sum : thm
    val wf_decode_tree : thm
    val wf_decode_unit : thm
    val wf_enc2dec : thm
  
  val Decode_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [Encode] Parent theory of "Decode"
   
   [dec2enc_def]  Definition
      
      ⊢ ∀d x. dec2enc d x = @l. d l = SOME (x,[])
   
   [dec_bnum_def]  Definition
      
      ⊢ (∀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_blist_def]  Definition
      
      ⊢ ∀p m d. decode_blist p m d = enc2dec p (encode_blist m (dec2enc d))
   
   [decode_bnum_def]  Definition
      
      ⊢ ∀m p. decode_bnum m p = enc2dec p (encode_bnum m)
   
   [decode_bool_def]  Definition
      
      ⊢ ∀p. decode_bool p = enc2dec p encode_bool
   
   [decode_list_def]  Definition
      
      ⊢ ∀p d. decode_list p d = enc2dec p (encode_list (dec2enc d))
   
   [decode_num_def]  Definition
      
      ⊢ ∀p. decode_num p = enc2dec p encode_num
   
   [decode_option_def]  Definition
      
      ⊢ ∀p d. decode_option p d = enc2dec p (encode_option (dec2enc d))
   
   [decode_prod_def]  Definition
      
      ⊢ ∀p d1 d2.
          decode_prod p d1 d2 =
          enc2dec p (encode_prod (dec2enc d1) (dec2enc d2))
   
   [decode_sum_def]  Definition
      
      ⊢ ∀p d1 d2.
          decode_sum p d1 d2 =
          enc2dec p (encode_sum (dec2enc d1) (dec2enc d2))
   
   [decode_tree_def]  Definition
      
      ⊢ ∀p d. decode_tree p d = enc2dec p (encode_tree (dec2enc d))
   
   [decode_unit_def]  Definition
      
      ⊢ ∀p. decode_unit p = enc2dec p encode_unit
   
   [enc2dec_def]  Definition
      
      ⊢ ∀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
   
   [wf_decoder_def]  Definition
      
      ⊢ ∀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)
   
   [dec2enc_decode_blist]  Theorem
      
      ⊢ ∀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
   
   [dec2enc_decode_bnum]  Theorem
      
      ⊢ ∀m p x.
          wf_pred_bnum m p ∧ p x ⇒
          dec2enc (decode_bnum m p) x = encode_bnum m x
   
   [dec2enc_decode_bool]  Theorem
      
      ⊢ ∀p x. p x ⇒ dec2enc (decode_bool p) x = encode_bool x
   
   [dec2enc_decode_list]  Theorem
      
      ⊢ ∀p d x.
          wf_decoder p d ∧ EVERY p x ⇒
          dec2enc (decode_list (EVERY p) d) x = encode_list (dec2enc d) x
   
   [dec2enc_decode_num]  Theorem
      
      ⊢ ∀p x. p x ⇒ dec2enc (decode_num p) x = encode_num x
   
   [dec2enc_decode_option]  Theorem
      
      ⊢ ∀p d x.
          wf_decoder p d ∧ lift_option p x ⇒
          dec2enc (decode_option (lift_option p) d) x =
          encode_option (dec2enc d) x
   
   [dec2enc_decode_prod]  Theorem
      
      ⊢ ∀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
   
   [dec2enc_decode_sum]  Theorem
      
      ⊢ ∀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
   
   [dec2enc_decode_unit]  Theorem
      
      ⊢ ∀p x. p x ⇒ dec2enc (decode_unit p) x = encode_unit x
   
   [dec2enc_enc2dec]  Theorem
      
      ⊢ ∀p e x. wf_encoder p e ∧ p x ⇒ dec2enc (enc2dec p e) x = e x
   
   [dec2enc_some]  Theorem
      
      ⊢ ∀p d x l.
          wf_decoder p d ⇒ (dec2enc d x = l ∧ p x ⇔ d l = SOME (x,[]))
   
   [dec_bnum_compute]  Theorem
      
      ⊢ (∀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_inj]  Theorem
      
      ⊢ ∀m l n t. dec_bnum m l = SOME (n,t) ⇒ l = encode_bnum m n ⧺ t
   
   [dec_bnum_lt]  Theorem
      
      ⊢ ∀m l n t. dec_bnum m l = SOME (n,t) ⇒ n < 2 ** m
   
   [decode_blist]  Theorem
      
      ⊢ 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')
   
   [decode_bnum]  Theorem
      
      ⊢ 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
   
   [decode_bool]  Theorem
      
      ⊢ decode_bool p l =
        case l of [] => NONE | h::t => if p h then SOME (h,t) else NONE
   
   [decode_dec2enc]  Theorem
      
      ⊢ ∀p d x. wf_decoder p d ∧ p x ⇒ d (dec2enc d x) = SOME (x,[])
   
   [decode_dec2enc_append]  Theorem
      
      ⊢ ∀p d x t. wf_decoder p d ∧ p x ⇒ d (dec2enc d x ⧺ t) = SOME (x,t)
   
   [decode_list]  Theorem
      
      ⊢ 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)
   
   [decode_num]  Theorem
      
      ⊢ 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
   
   [decode_num_total]  Theorem
      
      ⊢ 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_option]  Theorem
      
      ⊢ 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)
   
   [decode_prod]  Theorem
      
      ⊢ 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')
   
   [decode_sum]  Theorem
      
      ⊢ 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')
   
   [decode_tree]  Theorem
      
      ⊢ 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')
   
   [decode_unit]  Theorem
      
      ⊢ decode_unit p l = if p () then SOME ((),l) else NONE
   
   [enc2dec_dec2enc]  Theorem
      
      ⊢ ∀p d. wf_decoder p d ⇒ enc2dec p (dec2enc d) = d
   
   [enc2dec_none]  Theorem
      
      ⊢ ∀p e l. enc2dec p e l = NONE ⇔ ∀x t. p x ⇒ l ≠ e x ⧺ t
   
   [enc2dec_some]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀p e l x.
          wf_encoder p e ⇒
          (enc2dec p e l = SOME x ⇔ p (FST x) ∧ l = e (FST x) ⧺ SND x)
   
   [encode_then_decode_blist]  Theorem
      
      ⊢ ∀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)
   
   [encode_then_decode_list]  Theorem
      
      ⊢ ∀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)
   
   [encode_then_decode_option]  Theorem
      
      ⊢ ∀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)
   
   [encode_then_decode_prod]  Theorem
      
      ⊢ ∀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)
   
   [encode_then_decode_sum]  Theorem
      
      ⊢ ∀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)
   
   [wf_dec2enc]  Theorem
      
      ⊢ ∀p d. wf_decoder p d ⇒ wf_encoder p (dec2enc d)
   
   [wf_decode_blist]  Theorem
      
      ⊢ ∀m p d.
          wf_decoder p d ⇒
          wf_decoder (lift_blist m p) (decode_blist (lift_blist m p) m d)
   
   [wf_decode_bnum]  Theorem
      
      ⊢ ∀m p. wf_pred_bnum m p ⇒ wf_decoder p (decode_bnum m p)
   
   [wf_decode_bool]  Theorem
      
      ⊢ ∀p. wf_decoder p (decode_bool p)
   
   [wf_decode_list]  Theorem
      
      ⊢ ∀p d.
          wf_decoder p d ⇒ wf_decoder (EVERY p) (decode_list (EVERY p) d)
   
   [wf_decode_num]  Theorem
      
      ⊢ ∀p. wf_decoder p (decode_num p)
   
   [wf_decode_option]  Theorem
      
      ⊢ ∀p d.
          wf_decoder p d ⇒
          wf_decoder (lift_option p) (decode_option (lift_option p) d)
   
   [wf_decode_prod]  Theorem
      
      ⊢ ∀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)
   
   [wf_decode_sum]  Theorem
      
      ⊢ ∀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)
   
   [wf_decode_tree]  Theorem
      
      ⊢ ∀p d.
          wf_decoder p d ⇒
          wf_decoder (lift_tree p) (decode_tree (lift_tree p) d)
   
   [wf_decode_unit]  Theorem
      
      ⊢ wf_decoder p (decode_unit p)
   
   [wf_enc2dec]  Theorem
      
      ⊢ ∀p e. wf_encoder p e ⇒ wf_decoder p (enc2dec p e)
   
   
*)
end

HOL 4, Trindemossen-1