120 

   120 datatype arexp =

   121   AZERO

   122 | AONE "bool list"

   123 | ACHAR "bool list" char

   124 | ASEQ "bool list" arexp arexp

   125 | AALT "bool list" arexp arexp

   126 | ASTAR "bool list" arexp

   127 

   128 fun fuse :: "bool list \<Rightarrow> arexp \<Rightarrow> arexp" where

   129   "fuse bs AZERO = AZERO"

   130 | "fuse bs (AONE cs) = AONE (bs @ cs)" 

   131 | "fuse bs (ACHAR cs c) = ACHAR (bs @ cs) c"

   132 | "fuse bs (AALT cs r1 r2) = AALT (bs @ cs) r1 r2"

   133 | "fuse bs (ASEQ cs r1 r2) = ASEQ (bs @ cs) r1 r2"

   134 | "fuse bs (ASTAR cs r) = ASTAR (bs @ cs) r"

   135 

   136 fun internalise :: "rexp \<Rightarrow> arexp" where

   137   "internalise ZERO = AZERO"

   138 | "internalise ONE = AONE []"

   139 | "internalise (CHAR c) = ACHAR [] c"

   140 | "internalise (ALT r1 r2) = AALT [] (fuse [False] (internalise r1)) 

   141                                      (fuse [True]  (internalise r2))"

   142 | "internalise (SEQ r1 r2) = ASEQ [] (internalise r1) (internalise r2)"

   143 | "internalise (STAR r) = ASTAR [] (internalise r)"

   144 

   145 fun retrieve :: "arexp \<Rightarrow> val \<Rightarrow> bool list" where

   146   "retrieve (AONE bs) Void = bs"

   147 | "retrieve (ACHAR bs c) (Char d) = bs"

   148 | "retrieve (AALT bs r1 r2) (Left v) = bs @ retrieve r1 v"

   149 | "retrieve (AALT bs r1 r2) (Right v) = bs @ retrieve r2 v"

   150 | "retrieve (ASEQ bs r1 r2) (Seq v1 v2) = bs @ retrieve r1 v1 @ retrieve r2 v2"

   151 | "retrieve (ASTAR bs r) (Stars []) = bs @ [True]"

   152 | "retrieve (ASTAR bs r) (Stars (v#vs)) = 

   153      bs @ [False] @ retrieve r v @ retrieve (ASTAR [] r) (Stars vs)"

   154 

   155 fun

   156  anullable :: "arexp \<Rightarrow> bool"

   157 where

   158   "anullable (AZERO) = False"

   159 | "anullable (AONE bs) = True"

   160 | "anullable (ACHAR bs c) = False"

   161 | "anullable (AALT bs r1 r2) = (anullable r1 \<or> anullable r2)"

   162 | "anullable (ASEQ bs r1 r2) = (anullable r1 \<and> anullable r2)"

   163 | "anullable (ASTAR bs r) = True"

   164 

   165 fun 

   166   amkeps :: "arexp \<Rightarrow> bool list"

   167 where

   168   "amkeps(AONE bs) = bs"

   169 | "amkeps(ASEQ bs r1 r2) = bs @ (amkeps r1) @ (amkeps r2)"

   170 | "amkeps(AALT bs r1 r2) = (if anullable(r1) then bs @ (amkeps r1) else bs @ (amkeps r2))"

   171 | "amkeps(ASTAR bs r) = bs @ [True]"

   172 

   173 

   174 fun

   175  ader :: "char \<Rightarrow> arexp \<Rightarrow> arexp"

   176 where

   177   "ader c (AZERO) = AZERO"

   178 | "ader c (AONE bs) = AZERO"

   179 | "ader c (ACHAR bs d) = (if c = d then AONE bs else AZERO)"

   180 | "ader c (AALT bs r1 r2) = AALT bs (ader c r1) (ader c r2)"

   181 | "ader c (ASEQ bs r1 r2) = 

   182      (if anullable r1

   183       then AALT bs (ASEQ [] (ader c r1) r2) (fuse (amkeps r1) (ader c r2))

   184       else ASEQ bs (ader c r1) r2)"

   185 | "ader c (ASTAR bs r) = ASEQ bs (fuse [False] (ader c r)) (ASTAR [] r)"

   186 

   187 lemma

   188   assumes "\<turnstile> v : der c r"

   189   shows "Some (injval r c v) = decode (retrieve (ader c (internalise r)) v) r"

   190 using assms

   191 apply(induct c r arbitrary: v rule: der.induct)

   192 apply(simp_all)

   193 apply(erule Prf_elims)

   194 apply(erule Prf_elims)

   195 apply(case_tac "c = d")

   196 apply(simp)

   197 apply(erule Prf_elims)

   198 apply(simp)

   199 apply(simp)

   200 apply(erule Prf_elims)

   201 apply(simp)

   202 apply(erule Prf_elims)

   203 apply(simp)

   204 apply(auto split: prod.splits)[1]

   205 oops