48 section {* Bit-Encodings *}

    49 

    50 

    51 fun 

    52   code :: "val \<Rightarrow> rexp \<Rightarrow> bool list"

    53 where

    54   "code Void ONE = []"

    55 | "code (Char c) (CHAR d) = []"

    56 | "code (Left v) (ALT r1 r2) = False # (code v r1)"

    57 | "code (Right v) (ALT r1 r2) = True # (code v r2)"

    58 | "code (Seq v1 v2) (SEQ r1 r2) = (code v1 r1) @ (code v2 r2)"

    59 | "code (Stars []) (STAR r) = [True]"

    60 | "code (Stars (v # vs)) (STAR r) =  False # (code v r) @ code (Stars vs) (STAR r)"

    61 

    62 fun 

    63   Stars_add :: "val \<Rightarrow> val \<Rightarrow> val"

    64 where

    65   "Stars_add v (Stars vs) = Stars (v # vs)"

    66 

    67 function

    68   decode' :: "bool list \<Rightarrow> rexp \<Rightarrow> (val * bool list)"

    69 where

    70   "decode' ds ZERO = (Void, [])"

    71 | "decode' ds ONE = (Void, ds)"

    72 | "decode' ds (CHAR d) = (Char d, ds)"

    73 | "decode' [] (ALT r1 r2) = (Void, [])"

    74 | "decode' (False # ds) (ALT r1 r2) = (let (v, ds') = decode' ds r1 in (Left v, ds'))"

    75 | "decode' (True # ds) (ALT r1 r2) = (let (v, ds') = decode' ds r2 in (Right v, ds'))"

    76 | "decode' ds (SEQ r1 r2) = (let (v1, ds') = decode' ds r1 in

    77                              let (v2, ds'') = decode' ds' r2 in (Seq v1 v2, ds''))"

    78 | "decode' [] (STAR r) = (Void, [])"

    79 | "decode' (True # ds) (STAR r) = (Stars [], ds)"

    80 | "decode' (False # ds) (STAR r) = (let (v, ds') = decode' ds r in

    81                                     let (vs, ds'') = decode' ds' (STAR r) 

    82                                     in (Stars_add v vs, ds''))"

    83 by pat_completeness auto

    84 

    85 term "inv_image (measure(%cs. size cs) <*lex*> measure(%s. size s)) (%(ds,r). (r,ds))"

    86 

    87 lemma decode'_smaller:

    88   assumes "decode'_dom (ds, r)"

    89   shows "length (snd (decode' ds r)) \<le> length ds"

    90 using assms

    91 apply(induct ds r)

    92 apply(auto simp add: decode'.psimps split: prod.split)

    93 using dual_order.trans apply blast

    94 by (meson dual_order.trans le_SucI)

    95 

    96 termination "decode'"  

    97 apply(relation "inv_image (measure(%cs. size cs) <*lex*> measure(%s. size s)) (%(ds,r). (r,ds))") 

    98 apply(auto dest!: decode'_smaller)

    99 by (metis less_Suc_eq_le snd_conv)

   100 

   101 fun 

   102   decode :: "bool list \<Rightarrow> rexp \<Rightarrow> val option"

   103 where

   104   "decode ds r = (let (v, ds') = decode' ds r 

   105                   in (if ds' = [] then Some v else None))"

   106 

   107 lemma decode'_code:

   108   assumes "\<turnstile> v : r"

   109   shows "decode' ((code v r) @ ds) r = (v, ds)"

   110 using assms

   111 by (induct v r arbitrary: ds) (auto)

   112 

   113 

   114 lemma decode_code:

   115   assumes "\<turnstile> v : r"

   116   shows "decode (code v r) r = Some v"

   117 using assms decode'_code[of _ _ "[]"]

   118 by auto

   119