--- a/thys/Sulzmann.thy	Wed Mar 16 10:02:19 2016 +0000
+++ b/thys/Sulzmann.thy	Fri Mar 18 01:26:14 2016 +0000
@@ -45,6 +45,78 @@
 *)
 
 
+section {* Bit-Encodings *}
+
+
+fun 
+  code :: "val \<Rightarrow> rexp \<Rightarrow> bool list"
+where
+  "code Void ONE = []"
+| "code (Char c) (CHAR d) = []"
+| "code (Left v) (ALT r1 r2) = False # (code v r1)"
+| "code (Right v) (ALT r1 r2) = True # (code v r2)"
+| "code (Seq v1 v2) (SEQ r1 r2) = (code v1 r1) @ (code v2 r2)"
+| "code (Stars []) (STAR r) = [True]"
+| "code (Stars (v # vs)) (STAR r) =  False # (code v r) @ code (Stars vs) (STAR r)"
+
+fun 
+  Stars_add :: "val \<Rightarrow> val \<Rightarrow> val"
+where
+  "Stars_add v (Stars vs) = Stars (v # vs)"
+
+function
+  decode' :: "bool list \<Rightarrow> rexp \<Rightarrow> (val * bool list)"
+where
+  "decode' ds ZERO = (Void, [])"
+| "decode' ds ONE = (Void, ds)"
+| "decode' ds (CHAR d) = (Char d, ds)"
+| "decode' [] (ALT r1 r2) = (Void, [])"
+| "decode' (False # ds) (ALT r1 r2) = (let (v, ds') = decode' ds r1 in (Left v, ds'))"
+| "decode' (True # ds) (ALT r1 r2) = (let (v, ds') = decode' ds r2 in (Right v, ds'))"
+| "decode' ds (SEQ r1 r2) = (let (v1, ds') = decode' ds r1 in
+                             let (v2, ds'') = decode' ds' r2 in (Seq v1 v2, ds''))"
+| "decode' [] (STAR r) = (Void, [])"
+| "decode' (True # ds) (STAR r) = (Stars [], ds)"
+| "decode' (False # ds) (STAR r) = (let (v, ds') = decode' ds r in
+                                    let (vs, ds'') = decode' ds' (STAR r) 
+                                    in (Stars_add v vs, ds''))"
+by pat_completeness auto
+
+term "inv_image (measure(%cs. size cs) <*lex*> measure(%s. size s)) (%(ds,r). (r,ds))"
+
+lemma decode'_smaller:
+  assumes "decode'_dom (ds, r)"
+  shows "length (snd (decode' ds r)) \<le> length ds"
+using assms
+apply(induct ds r)
+apply(auto simp add: decode'.psimps split: prod.split)
+using dual_order.trans apply blast
+by (meson dual_order.trans le_SucI)
+
+termination "decode'"  
+apply(relation "inv_image (measure(%cs. size cs) <*lex*> measure(%s. size s)) (%(ds,r). (r,ds))") 
+apply(auto dest!: decode'_smaller)
+by (metis less_Suc_eq_le snd_conv)
+
+fun 
+  decode :: "bool list \<Rightarrow> rexp \<Rightarrow> val option"
+where
+  "decode ds r = (let (v, ds') = decode' ds r 
+                  in (if ds' = [] then Some v else None))"
+
+lemma decode'_code:
+  assumes "\<turnstile> v : r"
+  shows "decode' ((code v r) @ ds) r = (v, ds)"
+using assms
+by (induct v r arbitrary: ds) (auto)
+
+
+lemma decode_code:
+  assumes "\<turnstile> v : r"
+  shows "decode (code v r) r = Some v"
+using assms decode'_code[of _ _ "[]"]
+by auto
+
 
 
 end
\ No newline at end of file