diff -r acc027964d10 -r 804fbb227568 thys/Sulzmann.thy
--- a/thys/Sulzmann.thy	Wed May 16 20:58:39 2018 +0100
+++ b/thys/Sulzmann.thy	Wed Aug 15 13:48:57 2018 +0100
@@ -1,346 +1,21 @@
    
 theory Sulzmann
-  imports "Positions" 
+  imports "Lexer" 
 begin
 
-
-section {* Sulzmann's "Ordering" of Values *}
-
-inductive ValOrd :: "val \<Rightarrow> val \<Rightarrow> bool" ("_ \<prec> _" [100, 100] 100)
-where
-  MY0: "length (flat v2) < length (flat v1) \<Longrightarrow> v1 \<prec> v2" 
-| C2: "\<lbrakk>v1 \<prec> v1'; flat (Seq v1 v2) = flat (Seq v1' v2')\<rbrakk> \<Longrightarrow> (Seq v1 v2) \<prec> (Seq v1' v2')" 
-| C1: "\<lbrakk>v2 \<prec> v2'; flat v2 = flat v2'\<rbrakk> \<Longrightarrow> (Seq v1 v2) \<prec> (Seq v1 v2')" 
-| A2: "flat v1 = flat v2 \<Longrightarrow> (Left v1) \<prec> (Right v2)"
-| A3: "\<lbrakk>v2 \<prec> v2'; flat v2 = flat v2'\<rbrakk> \<Longrightarrow> (Right v2) \<prec> (Right v2')"
-| A4: "\<lbrakk>v1 \<prec> v1'; flat v1 = flat v1'\<rbrakk> \<Longrightarrow> (Left v1) \<prec> (Left v1')"
-| K1: "flat (Stars (v#vs)) = [] \<Longrightarrow> (Stars []) \<prec> (Stars (v#vs))"
-| K3: "\<lbrakk>v1 \<prec> v2; flat (Stars (v1#vs1)) = flat (Stars (v2#vs2))\<rbrakk> \<Longrightarrow> (Stars (v1#vs1)) \<prec> (Stars (v2#vs2))"
-| K4: "\<lbrakk>(Stars vs1) \<prec> (Stars vs2); flat (Stars vs1) = flat (Stars vs2)\<rbrakk>  \<Longrightarrow> (Stars (v#vs1)) \<prec> (Stars (v#vs2))"
-
-
-(*
-inductive ValOrd :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<preceq>_ _" [100, 100, 100] 100)
-where
-  C2: "v1 \<preceq>r1 v1' \<Longrightarrow> (Seq v1 v2) \<preceq>(SEQ r1 r2) (Seq v1' v2')" 
-| C1: "v2 \<preceq>r2 v2' \<Longrightarrow> (Seq v1 v2) \<preceq>(SEQ r1 r2) (Seq v1 v2')" 
-| A1: "length (flat v2) > length (flat v1) \<Longrightarrow> (Right v2) \<preceq>(ALT r1 r2) (Left v1)"
-| A2: "length (flat v1) \<ge> length (flat v2) \<Longrightarrow> (Left v1) \<preceq>(ALT r1 r2) (Right v2)"
-| A3: "v2 \<preceq>r2 v2' \<Longrightarrow> (Right v2) \<preceq>(ALT r1 r2) (Right v2')"
-| A4: "v1 \<preceq>r1 v1' \<Longrightarrow> (Left v1) \<preceq>(ALT r1 r2) (Left v1')"
-| K1: "flat (Stars (v # vs)) = [] \<Longrightarrow> (Stars []) \<preceq>(STAR r) (Stars (v # vs))"
-| K2: "flat (Stars (v # vs)) \<noteq> [] \<Longrightarrow> (Stars (v # vs)) \<preceq>(STAR r) (Stars [])"
-| K3: "v1 \<preceq>r v2 \<Longrightarrow> (Stars (v1 # vs1)) \<preceq>(STAR r) (Stars (v2 # vs2))"
-| K4: "(Stars vs1) \<preceq>(STAR r) (Stars vs2) \<Longrightarrow> (Stars (v # vs1)) \<preceq>(STAR r) (Stars (v # vs2))"
-*)
-(*| MY1: "Void \<preceq>ONE Void" 
-| MY2: "(Char c) \<preceq>(CHAR c) (Char c)" 
-| MY3: "(Stars []) \<preceq>(STAR r) (Stars [])" 
-*)
-
-(*
-lemma ValOrd_refl: 
-  assumes "\<turnstile> v : r" 
-  shows "v \<preceq>r v"
-using assms
-apply(induct r rule: Prf.induct)
-apply(rule ValOrd.intros)
-apply(simp)
-apply(rule ValOrd.intros)
-apply(simp)
-apply(rule ValOrd.intros)
-apply(simp)
-apply(rule ValOrd.intros)
-apply(rule ValOrd.intros)
-apply(rule ValOrd.intros)
-apply(rule ValOrd.intros)
-apply(simp)
-done
-*)
-
-lemma ValOrd_irrefl: 
-  assumes "\<turnstile> v : r"  "v \<prec> v" 
-  shows "False"
-using assms
-apply(induct v r rule: Prf.induct)
-apply(erule ValOrd.cases)
-apply(simp_all)
-apply(erule ValOrd.cases)
-apply(simp_all)
-apply(erule ValOrd.cases)
-apply(simp_all)
-apply(erule ValOrd.cases)
-apply(simp_all)
-apply(erule ValOrd.cases)
-apply(simp_all)
-apply(erule ValOrd.cases)
-apply(simp_all)
-apply(erule ValOrd.cases)
-apply(simp_all)
-done
-
-lemma prefix_sprefix:
-  shows "xs \<sqsubseteq>pre ys \<longleftrightarrow> (xs = ys \<or> xs \<sqsubset>spre ys)"
-apply(auto simp add: sprefix_list_def prefix_list_def)
-done
-
-
-
-lemma Posix_CPT2:
-  assumes "v1 \<prec> v2" 
-  shows "v1 :\<sqsubset>val v2" 
-using assms
-apply(induct v1 v2 arbitrary: rule: ValOrd.induct)
-apply(rule val_ord_shorterI)
-apply(simp)
-apply(rule val_ord_SeqI1)
-apply(simp)
-apply(simp)
-apply(rule val_ord_SeqI2)
-apply(simp)
-apply(simp)
-apply(simp add: val_ord_ex_def)
-apply(rule_tac x="[0]" in exI)
-apply(auto simp add: val_ord_def Pos_empty pflat_len_simps)[1]
-apply(smt inlen_bigger)
-apply(rule val_ord_RightI)
-apply(simp)
-apply(simp)
-apply(rule val_ord_LeftI)
-apply(simp)
-apply(simp)
-defer
-apply(rule val_ord_StarsI)
-apply(simp)
-apply(simp)
-apply(rule val_ord_StarsI2)
-apply(simp)
-apply(simp)
-oops
-
-lemma QQ: 
-  shows "x \<le> (y::nat) \<longleftrightarrow> x = y \<or> x < y"
-  by auto
-
-lemma Posix_CPT2:
-  assumes "v1 :\<sqsubset>val v2" "v1 \<in> CPTpre r s" "v2 \<in> CPTpre r s"
-  shows "v1 \<prec> v2"
-using assms
-apply(induct r arbitrary: v1 v2 s)  
-apply(auto simp add: CPTpre_def)[1]
-apply(erule CPrf.cases)
-apply(simp_all)[7]
-apply(auto simp add: CPTpre_def)[1]
-apply(erule CPrf.cases)
-apply(simp_all)[7]
-apply(auto simp add: CPTpre_def)[1]
-apply(erule CPrf.cases)
-apply(simp_all)[7]
-apply(simp add: val_ord_ex_def)
-apply(auto simp add: val_ord_def)[1]
-apply(auto simp add: CPTpre_def)[1]
-apply(erule CPrf.cases)
-apply(simp_all)[7]
-apply(erule CPrf.cases)
-apply(simp_all)[7]
-apply(auto simp add: val_ord_ex_def val_ord_def)[1]
-(* SEQ case *)
-apply(subst (asm) (5) CPTpre_def)
-apply(subst (asm) (5) CPTpre_def)
-apply(auto)[1]
-apply(erule CPrf.cases)
-apply(simp_all)[7]
-apply(erule CPrf.cases)
-apply(simp_all)[7]
-apply(clarify)
-apply(frule val_ord_shorterE)
-apply(subst (asm) QQ)
-apply(erule disjE)
-apply(drule val_ord_SeqE)
-apply(erule disjE)
-apply(drule_tac x="v1a" in meta_spec)
-apply(rotate_tac 8)
-apply(drule_tac x="v1b" in meta_spec)
-apply(drule_tac x="flat v1a @ flat v2a @ s'" in meta_spec)
-apply(simp)
-apply(drule meta_mp)
-apply(auto simp add: CPTpre_def)[1]
-apply(drule meta_mp)
-apply(auto simp add: CPTpre_def)[1]
-apply(rule ValOrd.intros(2))
-apply(assumption)
-apply(frule val_ord_shorterE)
-apply(subst (asm) append_eq_append_conv_if)
-apply(simp)
-apply (metis append_assoc append_eq_append_conv_if length_append)
-
-
-thm le
-apply(clarify)
-apply(rule ValOrd.intros)
-apply(simp)
-
-apply(subst (asm) (3) CPTpre_def)
-apply(subst (asm) (3) CPTpre_def)
-apply(auto)[1]
-apply(drule_tac meta_mp)
-apply(auto simp add: CPTpre_def)[1]
-apply(erule CPrf.cases)
-apply(simp_all)[7]
-apply(erule CPrf.cases)
-apply(simp_all)[7]
-apply(clarify)
-apply(drule val_ord_SeqE)
-apply(erule disjE)
-apply(simp add: append_eq_append_conv2)
-apply(auto)
-prefer 2
-apply(rule  ValOrd.intros(2))
-prefer 2
-apply(simp)
-thm ValOrd.intros
-apply(case_tac "flat v1b = flat v1a")
-apply(rule ValOrd.intros)
-apply(simp)
-apply(simp)
-
-
-
-
-lemma Posix_CPT:
-  assumes "v1 :\<sqsubset>val v2" "v1 \<in> CPT r s" "v2 \<in> CPT r s"
-  shows "v1 \<preceq>r v2" 
-using assms
-apply(induct r arbitrary: v1 v2 s rule: rexp.induct)
-apply(simp add: CPT_def)
-apply(clarify)
-apply(erule CPrf.cases)
-apply(simp_all)
-apply(simp add: CPT_def)
-apply(clarify)
-apply(erule CPrf.cases)
-apply(simp_all)
-apply(erule CPrf.cases)
-apply(simp_all)
-apply(rule ValOrd.intros)
-apply(simp add: CPT_def)
-apply(clarify)
-apply(erule CPrf.cases)
-apply(simp_all)
-apply(erule CPrf.cases)
-apply(simp_all)
-apply(rule ValOrd.intros)
-(*SEQ case *)
-apply(simp add: CPT_def)
-apply(clarify)
-apply(erule CPrf.cases)
-apply(simp_all)
-apply(clarify)
-apply(erule CPrf.cases)
-apply(simp_all)
-apply(clarify)
-thm val_ord_SEQ
-apply(drule_tac r="r1a" in  val_ord_SEQ)
-apply(simp)
-using Prf_CPrf apply blast
-using Prf_CPrf apply blast
-apply(erule disjE)
-apply(rule C2)
-prefer 2
-apply(simp)
-apply(rule C1)
-apply blast
-
-apply(simp add: append_eq_append_conv2)
-apply(clarify)
-apply(auto)[1]
-apply(drule_tac x="v1a" in meta_spec)
-apply(rotate_tac 8)
-apply(drule_tac x="v1b" in meta_spec)
-apply(rotate_tac 8)
-apply(simp)
-
-(* HERE *)
-apply(subst (asm) (3) val_ord_ex_def)
-apply(clarify)
-apply(subst (asm) val_ord_def)
-apply(clarify)
-apply(rule ValOrd.intros)
-
-
-apply(simp add: val_ord_ex_def)
-oops
-
-
-lemma ValOrd_trans:
-  assumes "x \<preceq>r y" "y \<preceq>r z"
-  and "x \<in> CPT r s" "y \<in> CPT r s" "z \<in> CPT r s"
-  shows "x \<preceq>r z"
-using assms
-apply(induct x r y arbitrary: s z rule: ValOrd.induct)
-apply(rotate_tac 2)
-apply(erule ValOrd.cases)
-apply(simp_all)[13]
-apply(rule ValOrd.intros)
-apply(drule_tac x="s" in meta_spec)
-apply(drule_tac x="v1'a" in meta_spec)
-apply(drule_tac meta_mp)
-apply(simp)
-apply(drule_tac meta_mp)
-apply(simp add: CPT_def)
-oops
-
-lemma ValOrd_preorder:
-  "preorder_on (CPT r s) {(v1, v2). v1 \<preceq>r v2 \<and> v1 \<in> (CPT r s) \<and> v2 \<in> (CPT r s)}"
-apply(simp add: preorder_on_def)
-apply(rule conjI)
-apply(simp add: refl_on_def)
-apply(auto)
-apply(rule ValOrd_refl)
-apply(simp add: CPT_def)
-apply(rule Prf_CPrf)
-apply(auto)[1]
-apply(simp add: trans_def)
-apply(auto)
-
-definition ValOrdEq :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<ge>_ _" [100, 100, 100] 100)
-where 
-  "v\<^sub>1 \<ge>r v\<^sub>2 \<equiv> v\<^sub>1 = v\<^sub>2 \<or> (v\<^sub>1 >r v\<^sub>2 \<and> flat v\<^sub>1 = flat v\<^sub>2)"
-
-(*
-
-
-inductive ValOrd :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<succ>_ _" [100, 100, 100] 100)
-where
-  "v2 \<succ>r2 v2' \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1 v2')" 
-| "\<lbrakk>v1 \<succ>r1 v1'; v1 \<noteq> v1'\<rbrakk> \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1' v2')" 
-| "length (flat v1) \<ge> length (flat v2) \<Longrightarrow> (Left v1) \<succ>(ALT r1 r2) (Right v2)"
-| "length (flat v2) > length (flat v1) \<Longrightarrow> (Right v2) \<succ>(ALT r1 r2) (Left v1)"
-| "v2 \<succ>r2 v2' \<Longrightarrow> (Right v2) \<succ>(ALT r1 r2) (Right v2')"
-| "v1 \<succ>r1 v1' \<Longrightarrow> (Left v1) \<succ>(ALT r1 r2) (Left v1')"
-| "Void \<succ>EMPTY Void"
-| "(Char c) \<succ>(CHAR c) (Char c)"
-| "flat (Stars (v # vs)) = [] \<Longrightarrow> (Stars []) \<succ>(STAR r) (Stars (v # vs))"
-| "flat (Stars (v # vs)) \<noteq> [] \<Longrightarrow> (Stars (v # vs)) \<succ>(STAR r) (Stars [])"
-| "\<lbrakk>v1 \<succ>r v2; v1 \<noteq> v2\<rbrakk> \<Longrightarrow> (Stars (v1 # vs1)) \<succ>(STAR r) (Stars (v2 # vs2))"
-| "(Stars vs1) \<succ>(STAR r) (Stars vs2) \<Longrightarrow> (Stars (v # vs1)) \<succ>(STAR r) (Stars (v # vs2))"
-| "(Stars []) \<succ>(STAR r) (Stars [])"
-*)
-
-
 section {* Bit-Encodings *}
 
-
 fun 
-  code :: "val \<Rightarrow> rexp \<Rightarrow> bool list"
+  code :: "val \<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)"
+  "code Void = []"
+| "code (Char c) = []"
+| "code (Left v) = False # (code v)"
+| "code (Right v) = True # (code v)"
+| "code (Seq v1 v2) = (code v1) @ (code v2)"
+| "code (Stars []) = [True]"
+| "code (Stars (v # vs)) =  False # (code v) @ code (Stars vs)"
+
 
 fun 
   Stars_add :: "val \<Rightarrow> val \<Rightarrow> val"
@@ -365,12 +40,6 @@
                                     in (Stars_add v vs, ds''))"
 by pat_completeness auto
 
-termination
-apply(size_change)
-oops
-
-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"
@@ -385,24 +54,35 @@
 apply(auto dest!: decode'_smaller)
 by (metis less_Suc_eq_le snd_conv)
 
-fun 
+definition
   decode :: "bool list \<Rightarrow> rexp \<Rightarrow> val option"
 where
-  "decode ds r = (let (v, ds') = decode' ds r 
+  "decode ds r \<equiv> (let (v, ds') = decode' ds r 
                   in (if ds' = [] then Some v else None))"
 
+lemma decode'_code_Stars:
+  assumes "\<forall>v\<in>set vs. \<Turnstile> v : r \<and> (\<forall>x. decode' (code v @ x) r = (v, x)) \<and> flat v \<noteq> []" 
+  shows "decode' (code (Stars vs) @ ds) (STAR r) = (Stars vs, ds)"
+  using assms
+  apply(induct vs)
+  apply(auto)
+  done
+
 lemma decode'_code:
-  assumes "\<turnstile> v : r"
-  shows "decode' ((code v r) @ ds) r = (v, ds)"
+  assumes "\<Turnstile> v : r"
+  shows "decode' ((code v) @ ds) r = (v, ds)"
 using assms
-by (induct v r arbitrary: ds) (auto)
+  apply(induct v r arbitrary: ds) 
+  apply(auto)
+  using decode'_code_Stars by blast
 
 
 lemma decode_code:
-  assumes "\<turnstile> v : r"
-  shows "decode (code v r) r = Some v"
-using assms decode'_code[of _ _ "[]"]
-by auto
+  assumes "\<Turnstile> v : r"
+  shows "decode (code v) r = Some v"
+  using assms unfolding decode_def
+  by (smt append_Nil2 decode'_code old.prod.case)
+
 
 datatype arexp =
   AZERO
@@ -429,6 +109,7 @@
 | "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"
@@ -439,6 +120,19 @@
 | "retrieve (ASTAR bs r) (Stars (v#vs)) = 
      bs @ [False] @ retrieve r v @ retrieve (ASTAR [] r) (Stars vs)"
 
+
+fun 
+  aerase :: "arexp \<Rightarrow> rexp"
+where
+  "aerase AZERO = ZERO"
+| "aerase (AONE _) = ONE"
+| "aerase (ACHAR _ c) = CHAR c"
+| "aerase (AALT _ r1 r2) = ALT (aerase r1) (aerase r2)"
+| "aerase (ASEQ _ r1 r2) = SEQ (aerase r1) (aerase r2)"
+| "aerase (ASTAR _ r) = STAR (aerase r)"
+
+
+
 fun
  anullable :: "arexp \<Rightarrow> bool"
 where
@@ -471,21 +165,194 @@
       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(auto split: prod.splits)[1]
-oops
+
+fun 
+ aders :: "string \<Rightarrow> arexp \<Rightarrow> arexp"
+where
+  "aders [] r = r"
+| "aders (c # s) r = aders s (ader c r)"
+
+fun 
+  alex :: "arexp \<Rightarrow> string \<Rightarrow> arexp"
+where
+  "alex r [] = r"
+| "alex r (c#s) = alex (ader c r) s"
+
+lemma anullable_correctness:
+  shows "nullable (aerase r) = anullable r"
+  apply(induct r)
+  apply(simp_all)
+  done
+
+lemma aerase_fuse:
+  shows "aerase (fuse bs r) = aerase r"
+  apply(induct r)
+  apply(simp_all)
+  done
+
+
+lemma aerase_ader:
+  shows "aerase (ader a r) = der a (aerase r)"
+  apply(induct r)
+  apply(simp_all add: aerase_fuse anullable_correctness)
+  done
+
+lemma aerase_internalise:
+  shows "aerase (internalise r) = r"
+  apply(induct r)
+  apply(simp_all add: aerase_fuse)
+  done
+
+
+lemma aerase_alex:
+  shows "aerase (alex r s) = ders s (aerase r)"
+  apply(induct s arbitrary: r )
+  apply(simp_all add: aerase_ader)
+  done
+
+lemma retrieve_encode_STARS:
+  assumes "\<forall>v\<in>set vs. \<Turnstile> v : r \<and> code v = retrieve (internalise r) v"
+  shows "code (Stars vs) = retrieve (ASTAR [] (internalise r)) (Stars vs)"
+  using assms
+  apply(induct vs)
+  apply(simp)
+  apply(simp)
+  done
+
+lemma retrieve_afuse2:
+  assumes "\<Turnstile> v : (aerase r)"
+  shows "retrieve (fuse bs r) v = bs @ retrieve r v"
+  using assms
+  apply(induct r arbitrary: v bs)
+  apply(auto)
+  using Prf_elims(1) apply blast
+  using Prf_elims(4) apply fastforce
+  using Prf_elims(5) apply fastforce
+  apply (smt Prf_elims(2) append_assoc retrieve.simps(5))
+   apply(erule Prf_elims)
+    apply(simp)
+   apply(simp)
+  apply(erule Prf_elims)
+  apply(simp)
+  apply(case_tac vs)
+   apply(simp)
+  apply(simp)
+  done
+
+lemma retrieve_afuse:
+  assumes "\<Turnstile> v : r"
+  shows "retrieve (fuse bs (internalise r)) v = bs @ retrieve (internalise r) v"
+  using assms 
+  by (simp_all add: retrieve_afuse2 aerase_internalise)
+
+
+lemma retrieve_encode:
+  assumes "\<Turnstile> v : r"
+  shows "code v = retrieve (internalise r) v"
+  using assms
+  apply(induct v r)
+  apply(simp_all add: retrieve_afuse retrieve_encode_STARS)
+  done
+
+
+lemma alex_append:
+  "alex r (s1 @ s2) = alex (alex r s1) s2"
+  apply(induct s1 arbitrary: r s2)
+   apply(simp_all)
+  done
 
+lemma ders_append:
+  shows "ders (s1 @ s2) r = ders s2 (ders s1 r)"
+  apply(induct s1 arbitrary: s2 r)
+  apply(auto)
+  done
+
+
+
+
+lemma Q00:
+  assumes "s \<in> r \<rightarrow> v"
+  shows "\<Turnstile> v : r"
+  using assms
+  apply(induct) 
+  apply(auto intro: Prf.intros)
+  by (metis Prf.intros(6) Prf_elims(6) insert_iff list.simps(15) val.inject(5))
+
+lemma Qa:
+  assumes "anullable r"
+  shows "retrieve r (mkeps (aerase r)) = amkeps r"
+  using assms
+  apply(induct r)
+       apply(auto)
+  using anullable_correctness apply auto[1]
+  apply (simp add: anullable_correctness)
+  by (simp add: anullable_correctness)
+
+  
+lemma Qb:
+  assumes "\<Turnstile> v : der c (aerase r)"
+  shows "retrieve (ader c r) v = retrieve r (injval (aerase r) c v)"
+  using assms
+  apply(induct r arbitrary: v c)
+       apply(simp_all)
+  using Prf_elims(1) apply blast
+  using Prf_elims(1) apply blast
+     apply(auto)[1]
+  using Prf_elims(4) apply fastforce
+  using Prf_elims(1) apply blast
+    apply(auto split: if_splits)[1]
+  apply(auto elim!: Prf_elims)[1]
+       apply(rotate_tac 1)
+       apply(drule_tac x="v2" in meta_spec)
+       apply(drule_tac x="c" in meta_spec)
+       apply(drule meta_mp)
+        apply(simp)
+       apply(drule sym)
+       apply(simp)
+       apply(subst retrieve_afuse2)
+        apply (simp add: aerase_ader)
+       apply (simp add: Qa)
+  using anullable_correctness apply auto[1]
+     apply(auto elim!: Prf_elims)[1]
+  using anullable_correctness apply auto[1]
+    apply(auto elim!: Prf_elims)[1]
+   apply(auto elim!: Prf_elims)[1]
+  apply(auto elim!: Prf_elims)[1]
+  by (simp add: retrieve_afuse2 aerase_ader)
+
+
+
+
+lemma MAIN:
+  assumes "\<Turnstile> v : ders s r"
+  shows "code (flex r id s v) = retrieve (alex (internalise r) s) v"
+  using assms
+  apply(induct s arbitrary: r v rule: rev_induct)
+   apply(simp)
+   apply (simp add: retrieve_encode)
+  apply(simp add: flex_append alex_append)
+  apply(subst Qb)
+  apply (simp add: aerase_internalise ders_append aerase_alex)
+  apply(simp add: aerase_alex aerase_internalise)
+  apply(drule_tac x="r" in meta_spec)
+  apply(drule_tac x="injval (ders xs r) x v" in meta_spec)
+  apply(drule meta_mp)
+   apply (simp add: Prf_injval ders_append)
+  apply(simp)
+  done
+
+fun alexer where
+ "alexer r s = (if anullable (alex (internalise r) s) then 
+                decode (amkeps (alex (internalise r) s)) r else None)"
+
+
+lemma FIN:
+  "alexer r s = lexer r s"
+  apply(auto split: prod.splits)
+  apply (smt MAIN Q00 Qa aerase_alex aerase_internalise anullable_correctness decode_code lexer_correctness(1) lexer_flex mkeps_nullable)
+  apply (simp add: aerase_internalise anullable_correctness[symmetric] lexer_flex aerase_alex)
+  done
+
+unused_thms
+  
 end
\ No newline at end of file