--- a/thys/Sulzmann.thy	Wed Aug 15 13:48:57 2018 +0100
+++ b/thys/Sulzmann.thy	Thu Aug 16 01:12:00 2018 +0100
@@ -167,16 +167,16 @@
 
 
 fun 
- aders :: "string \<Rightarrow> arexp \<Rightarrow> arexp"
+  aders :: "arexp \<Rightarrow> string \<Rightarrow> arexp"
 where
-  "aders [] r = r"
-| "aders (c # s) r = aders s (ader c r)"
+  "aders r [] = r"
+| "aders r (c#s) = aders (ader c r) s"
 
-fun 
-  alex :: "arexp \<Rightarrow> string \<Rightarrow> arexp"
-where
-  "alex r [] = r"
-| "alex r (c#s) = alex (ader c r) s"
+lemma aders_append:
+  "aders r (s1 @ s2) = aders (aders r s1) s2"
+  apply(induct s1 arbitrary: r s2)
+  apply(simp_all)
+  done
 
 lemma anullable_correctness:
   shows "nullable (aerase r) = anullable r"
@@ -190,6 +190,11 @@
   apply(simp_all)
   done
 
+lemma aerase_internalise:
+  shows "aerase (internalise r) = r"
+  apply(induct r)
+  apply(simp_all add: aerase_fuse)
+  done
 
 lemma aerase_ader:
   shows "aerase (ader a r) = der a (aerase r)"
@@ -197,15 +202,8 @@
   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)"
+lemma aerase_aders:
+  shows "aerase (aders r s) = ders s (aerase r)"
   apply(induct s arbitrary: r )
   apply(simp_all add: aerase_ader)
   done
@@ -255,18 +253,6 @@
   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
-
 
 
 
@@ -275,7 +261,7 @@
   shows "\<Turnstile> v : r"
   using assms
   apply(induct) 
-  apply(auto intro: Prf.intros)
+        apply(auto intro: Prf.intros)
   by (metis Prf.intros(6) Prf_elims(6) insert_iff list.simps(15) val.inject(5))
 
 lemma Qa:
@@ -320,38 +306,34 @@
   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"
+  shows "code (flex r id s v) = retrieve (aders (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(induct s arbitrary: v rule: rev_induct)
+  apply(simp)
+  apply(simp add: retrieve_encode)
+  apply(simp add: flex_append aders_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(simp add: aerase_internalise ders_append aerase_aders)
+  apply(simp add: aerase_aders aerase_internalise)
   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 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)"
+ "alexer r s = (if anullable (aders (internalise r) s) then 
+                decode (amkeps (aders (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
+  apply(auto simp add: lexer_flex)
+  apply (smt MAIN Q00 Qa aerase_aders aerase_internalise decode_code lexer_correctness(1) lexer_flex mkeps_nullable)
+  apply (metis aerase_aders aerase_internalise anullable_correctness)
+  using aerase_aders aerase_internalise anullable_correctness by force
 
 unused_thms