diff -r 4e00dd2398ac -r 940530087f30 thys/Sulzmann.thy
--- a/thys/Sulzmann.thy	Fri Apr 01 16:29:33 2016 +0100
+++ b/thys/Sulzmann.thy	Tue Apr 05 09:27:36 2016 +0100
@@ -117,6 +117,91 @@
 using assms decode'_code[of _ _ "[]"]
 by auto
 
+datatype arexp =
+  AZERO
+| AONE "bool list"
+| ACHAR "bool list" char
+| ASEQ "bool list" arexp arexp
+| AALT "bool list" arexp arexp
+| ASTAR "bool list" arexp
+
+fun fuse :: "bool list \<Rightarrow> arexp \<Rightarrow> arexp" where
+  "fuse bs AZERO = AZERO"
+| "fuse bs (AONE cs) = AONE (bs @ cs)" 
+| "fuse bs (ACHAR cs c) = ACHAR (bs @ cs) c"
+| "fuse bs (AALT cs r1 r2) = AALT (bs @ cs) r1 r2"
+| "fuse bs (ASEQ cs r1 r2) = ASEQ (bs @ cs) r1 r2"
+| "fuse bs (ASTAR cs r) = ASTAR (bs @ cs) r"
+
+fun internalise :: "rexp \<Rightarrow> arexp" where
+  "internalise ZERO = AZERO"
+| "internalise ONE = AONE []"
+| "internalise (CHAR c) = ACHAR [] c"
+| "internalise (ALT r1 r2) = AALT [] (fuse [False] (internalise r1)) 
+                                     (fuse [True]  (internalise r2))"
+| "internalise (SEQ r1 r2) = ASEQ [] (internalise r1) (internalise r2)"
+| "internalise (STAR r) = ASTAR [] (internalise r)"
+
+fun retrieve :: "arexp \<Rightarrow> val \<Rightarrow> bool list" where
+  "retrieve (AONE bs) Void = bs"
+| "retrieve (ACHAR bs c) (Char d) = bs"
+| "retrieve (AALT bs r1 r2) (Left v) = bs @ retrieve r1 v"
+| "retrieve (AALT bs r1 r2) (Right v) = bs @ retrieve r2 v"
+| "retrieve (ASEQ bs r1 r2) (Seq v1 v2) = bs @ retrieve r1 v1 @ retrieve r2 v2"
+| "retrieve (ASTAR bs r) (Stars []) = bs @ [True]"
+| "retrieve (ASTAR bs r) (Stars (v#vs)) = 
+     bs @ [False] @ retrieve r v @ retrieve (ASTAR [] r) (Stars vs)"
+
+fun
+ anullable :: "arexp \<Rightarrow> bool"
+where
+  "anullable (AZERO) = False"
+| "anullable (AONE bs) = True"
+| "anullable (ACHAR bs c) = False"
+| "anullable (AALT bs r1 r2) = (anullable r1 \<or> anullable r2)"
+| "anullable (ASEQ bs r1 r2) = (anullable r1 \<and> anullable r2)"
+| "anullable (ASTAR bs r) = True"
+
+fun 
+  amkeps :: "arexp \<Rightarrow> bool list"
+where
+  "amkeps(AONE bs) = bs"
+| "amkeps(ASEQ bs r1 r2) = bs @ (amkeps r1) @ (amkeps r2)"
+| "amkeps(AALT bs r1 r2) = (if anullable(r1) then bs @ (amkeps r1) else bs @ (amkeps r2))"
+| "amkeps(ASTAR bs r) = bs @ [True]"
 
 
+fun
+ ader :: "char \<Rightarrow> arexp \<Rightarrow> arexp"
+where
+  "ader c (AZERO) = AZERO"
+| "ader c (AONE bs) = AZERO"
+| "ader c (ACHAR bs d) = (if c = d then AONE bs else AZERO)"
+| "ader c (AALT bs r1 r2) = AALT bs (ader c r1) (ader c r2)"
+| "ader c (ASEQ bs r1 r2) = 
+     (if anullable r1
+      then AALT bs (ASEQ [] (ader c r1) r2) (fuse (amkeps r1) (ader c r2))
+      else ASEQ bs (ader c r1) r2)"
+| "ader c (ASTAR bs r) = ASEQ bs (fuse [False] (ader c r)) (ASTAR [] r)"
+
+lemma
+  assumes "\<turnstile> v : der c r"
+  shows "Some (injval r c v) = decode (retrieve (ader c (internalise r)) v) r"
+using assms
+apply(induct c r arbitrary: v rule: der.induct)
+apply(simp_all)
+apply(erule Prf_elims)
+apply(erule Prf_elims)
+apply(case_tac "c = d")
+apply(simp)
+apply(erule Prf_elims)
+apply(simp)
+apply(simp)
+apply(erule Prf_elims)
+apply(simp)
+apply(erule Prf_elims)
+apply(simp)
+apply(auto split: prod.splits)[1]
+oops
+
 end
\ No newline at end of file