Mercurial Mercurial > hg > lexing / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
updated
authorChristian Urban <christian dot urban at kcl dot ac dot uk>
Mon, 14 Mar 2016 23:08:58 +0000
changeset 150 09f81fee11ce
parent 149 ec3d221bfc45
child 151 5a1196466a9c
updated
thys/Paper/Paper.thy file | annotate | diff | comparison | revisions
thys/ROOT file | annotate | diff | comparison | revisions
thys/ReStar.thy file | annotate | diff | comparison | revisions
thys/Simplifying.thy file | annotate | diff | comparison | revisions 
--- a/thys/Paper/Paper.thy	Mon Mar 14 15:15:29 2016 +0000
+++ b/thys/Paper/Paper.thy	Mon Mar 14 23:08:58 2016 +0000
@@ -2,6 +2,7 @@
 theory Paper
 imports 
    "../ReStar"
+   "../Simplifying" 
    "../Sulzmann" 
    "~~/src/HOL/Library/LaTeXsugar"
 begin
--- a/thys/ROOT	Mon Mar 14 15:15:29 2016 +0000
+++ b/thys/ROOT	Mon Mar 14 23:08:58 2016 +0000
@@ -1,6 +1,7 @@
 session "Lex" = HOL +
   theories [document = false]
 	"ReStar" 
+        "Simplifying"
         "Sulzmann" 
 
 
--- a/thys/ReStar.thy	Mon Mar 14 15:15:29 2016 +0000
+++ b/thys/ReStar.thy	Mon Mar 14 23:08:58 2016 +0000
@@ -805,322 +805,6 @@
 apply(simp)
 using Posix1(1) by auto
 
-section {* Lexer including simplifications *}
-
-
-fun F_RIGHT where
-  "F_RIGHT f v = Right (f v)"
-
-fun F_LEFT where
-  "F_LEFT f v = Left (f v)"
-
-fun F_ALT where
-  "F_ALT f\<^sub>1 f\<^sub>2 (Right v) = Right (f\<^sub>2 v)"
-| "F_ALT f\<^sub>1 f\<^sub>2 (Left v) = Left (f\<^sub>1 v)"  
-| "F_ALT f1 f2 v = v"
-
-
-fun F_SEQ1 where
-  "F_SEQ1 f\<^sub>1 f\<^sub>2 v = Seq (f\<^sub>1 Void) (f\<^sub>2 v)"
-
-fun F_SEQ2 where 
-  "F_SEQ2 f\<^sub>1 f\<^sub>2 v = Seq (f\<^sub>1 v) (f\<^sub>2 Void)"
-
-fun F_SEQ where 
-  "F_SEQ f\<^sub>1 f\<^sub>2 (Seq v\<^sub>1 v\<^sub>2) = Seq (f\<^sub>1 v\<^sub>1) (f\<^sub>2 v\<^sub>2)"
-| "F_SEQ f1 f2 v = v"
-
-fun simp_ALT where
-  "simp_ALT (ZERO, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (r\<^sub>2, F_RIGHT f\<^sub>2)"
-| "simp_ALT (r\<^sub>1, f\<^sub>1) (ZERO, f\<^sub>2) = (r\<^sub>1, F_LEFT f\<^sub>1)"
-| "simp_ALT (r\<^sub>1, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (ALT r\<^sub>1 r\<^sub>2, F_ALT f\<^sub>1 f\<^sub>2)"
-
-fun simp_SEQ where
-  "simp_SEQ (ONE, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (r\<^sub>2, F_SEQ1 f\<^sub>1 f\<^sub>2)"
-| "simp_SEQ (r\<^sub>1, f\<^sub>1) (ONE, f\<^sub>2) = (r\<^sub>1, F_SEQ2 f\<^sub>1 f\<^sub>2)"
-| "simp_SEQ (r\<^sub>1, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (SEQ r\<^sub>1 r\<^sub>2, F_SEQ f\<^sub>1 f\<^sub>2)"  
- 
-lemma simp_SEQ_simps:
-  "simp_SEQ p1 p2 = (if (fst p1 = ONE) then (fst p2, F_SEQ1 (snd p1) (snd p2))
-                    else (if (fst p2 = ONE) then (fst p1, F_SEQ2 (snd p1) (snd p2))
-                    else (SEQ (fst p1) (fst p2), F_SEQ (snd p1) (snd p2))))"
-apply(auto)
-apply(case_tac p1)
-apply(case_tac p2)
-apply(simp)
-apply(case_tac p1)
-apply(case_tac p2)
-apply(simp)
-apply(case_tac a)
-apply(simp_all)
-apply(case_tac p1)
-apply(case_tac p2)
-apply(simp)
-apply(case_tac p1)
-apply(case_tac p2)
-apply(simp)
-apply(case_tac a)
-apply(simp_all)
-apply(case_tac aa)
-apply(simp_all)
-apply(auto)
-apply(case_tac aa)
-apply(simp_all)
-apply(case_tac aa)
-apply(simp_all)
-apply(case_tac aa)
-apply(simp_all)
-apply(case_tac aa)
-apply(simp_all)
-done
-
-lemma simp_ALT_simps:
-  "simp_ALT p1 p2 = (if (fst p1 = ZERO) then (fst p2, F_RIGHT (snd p2))
-                    else (if (fst p2 = ZERO) then (fst p1, F_LEFT (snd p1))
-                    else (ALT (fst p1) (fst p2), F_ALT (snd p1) (snd p2))))"
-apply(auto)
-apply(case_tac p1)
-apply(case_tac p2)
-apply(simp)
-apply(case_tac p1)
-apply(case_tac p2)
-apply(simp)
-apply(case_tac a)
-apply(simp_all)
-apply(case_tac p1)
-apply(case_tac p2)
-apply(simp)
-apply(case_tac p1)
-apply(case_tac p2)
-apply(simp)
-apply(case_tac a)
-apply(simp_all)
-apply(case_tac aa)
-apply(simp_all)
-apply(auto)
-apply(case_tac aa)
-apply(simp_all)
-apply(case_tac aa)
-apply(simp_all)
-apply(case_tac aa)
-apply(simp_all)
-apply(case_tac aa)
-apply(simp_all)
-done
-
-
-fun 
-  simp :: "rexp \<Rightarrow> rexp * (val \<Rightarrow> val)"
-where
-  "simp (ALT r1 r2) = simp_ALT (simp r1) (simp r2)" 
-| "simp (SEQ r1 r2) = simp_SEQ (simp r1) (simp r2)" 
-| "simp r = (r, id)"
-
-fun 
-  slexer :: "rexp \<Rightarrow> string \<Rightarrow> val option"
-where
-  "slexer r [] = (if nullable r then Some(mkeps r) else None)"
-| "slexer r (c#s) = (let (rs, fr) = simp (der c r) in
-                         (case (slexer rs s) of  
-                            None \<Rightarrow> None
-                          | Some(v) \<Rightarrow> Some(injval r c (fr v))))"
-
-
-lemma L_fst_simp:
-  shows "L(r) = L(fst (simp r))"
-using assms
-apply(induct r rule: rexp.induct)
-apply(auto simp add: simp_SEQ_simps simp_ALT_simps)
-done
-
-lemma 
-  shows "\<turnstile> ((snd (simp r)) v) : r \<longleftrightarrow> \<turnstile> v : (fst (simp r))"
-using assms
-apply(induct r arbitrary: v rule: simp.induct)
-apply(auto simp add: simp_SEQ_simps simp_ALT_simps intro: Prf.intros)
-using Prf_elims(3) apply blast
-apply(erule Prf_elims)
-apply(simp)
-apply(clarify)
-apply(blast)
-apply(simp)
-apply(erule Prf_elims)
-apply(simp)
-apply(simp)
-apply(clarify)
-apply(blast)
-apply(erule Prf_elims)
-apply(case_tac v)
-apply(simp_all)
-apply(rule Prf.intros)
-apply(clarify)
-apply(simp)
-apply(case_tac v)
-apply(simp_all)
-apply(rule Prf.intros)
-apply(clarify)
-apply(simp)
-apply(erule Prf_elims)
-apply(simp)
-apply(rule Prf.intros)
-apply(simp)
-apply(simp)
-apply(rule Prf.intros)
-apply(simp)
-apply(erule Prf_elims)
-apply(simp)
-apply(blast)
-apply(rule Prf.intros)
-apply(erule Prf_elims)
-apply(simp)
-apply(rule Prf.intros)
-apply(erule Prf_elims)
-apply(simp)
-apply(rule Prf.intros)
-apply(erule Prf_elims)
-apply(simp)
-apply(clarify)
-apply(blast)
-apply(rule Prf.intros)
-apply(blast)
-using Prf.intros(4) apply blast
-apply(erule Prf_elims)
-apply(simp)
-apply(clarify)
-apply(blast)
-apply(rule Prf.intros)
-using Prf.intros(4) apply blast
-apply blast
-apply(erule Prf_elims)
-apply(case_tac v)
-apply(simp_all)
-apply(rule Prf.intros)
-apply(clarify)
-apply(simp)
-apply(clarify)
-apply(blast)
-apply(erule Prf_elims)
-apply(case_tac v)
-apply(simp_all)
-apply(rule Prf.intros)
-apply(clarify)
-apply(simp)
-apply(simp)
-done
-
-lemma Posix_simp_nullable:
-  assumes "nullable r" "[] \<in> (fst (simp r)) \<rightarrow> v"
-  shows "((snd (simp r)) v) = mkeps r"
-using assms 
-apply(induct r arbitrary: v)
-apply(auto simp add: simp_SEQ_simps simp_ALT_simps)
-apply(erule Posix_elims)
-apply(simp)
-apply(erule Posix_elims)
-apply(clarify)
-using Posix.intros(1) apply blast
-using Posix.intros(1) apply blast
-using Posix.intros(1) apply blast
-apply(erule Posix_elims)
-apply(simp)
-apply(erule Posix_elims)
-apply (metis L_fst_simp nullable.simps(1) nullable_correctness)
-apply(erule Posix_elims)
-apply(clarify)
-apply(simp)
-apply(clarify)
-apply(simp)
-apply(simp only: L_fst_simp[symmetric])
-apply (simp add: nullable_correctness)
-apply(erule Posix_elims)
-using L_fst_simp Posix1(1) nullable_correctness apply blast
-apply (metis L.simps(1) L_fst_simp Prf_flat_L empty_iff mkeps_nullable)
-apply(erule Posix_elims)
-apply(clarify)
-apply(simp)
-apply(simp only: L_fst_simp[symmetric])
-apply (simp add: nullable_correctness)
-apply(erule Posix_elims)
-apply(clarify)
-apply(simp)
-using L_fst_simp Posix1(1) nullable_correctness apply blast
-apply(simp)
-apply(erule Posix_elims)
-apply(clarify)
-apply(simp)
-using Posix1(2) apply auto[1]
-apply(simp)
-done
-
-lemma Posix_simp:
-  assumes "s \<in> (fst (simp r)) \<rightarrow> v" 
-  shows "s \<in> r \<rightarrow> ((snd (simp r)) v)"
-using assms
-apply(induct r arbitrary: s v rule: rexp.induct) 
-apply(auto split: if_splits simp add: simp_SEQ_simps simp_ALT_simps)
-prefer 3
-apply(erule Posix_elims)
-apply(clarify)
-apply(simp)
-apply(rule Posix.intros)
-apply(blast)
-apply(blast)
-apply(auto)[1]
-apply(simp add: L_fst_simp[symmetric])
-apply(auto)[1]
-prefer 3
-apply(rule Posix.intros)
-apply(blast)
-apply (metis L.simps(1) L_fst_simp equals0D)
-prefer 3
-apply(rule Posix.intros)
-apply(blast)
-prefer 3
-apply(erule Posix_elims)
-apply(clarify)
-apply(simp)
-apply(rule Posix.intros)
-apply(blast)
-apply(simp)
-apply(rule Posix.intros)
-apply(blast)
-apply(simp add: L_fst_simp[symmetric])
-apply(subst append.simps[symmetric])
-apply(rule Posix.intros)
-prefer 2
-apply(blast)
-prefer 2
-apply(auto)[1]
-apply (metis L_fst_simp Posix_elims(2) lex_correct3a)
-apply(subst Posix_simp_nullable)
-using Posix.intros(1) Posix1(1) nullable_correctness apply blast
-apply(simp)
-apply(rule Posix.intros)
-apply(rule Posix_mkeps)
-using Posix.intros(1) Posix1(1) nullable_correctness apply blast
-apply(subst append_Nil2[symmetric])
-apply(rule Posix.intros)
-apply(blast)
-apply(subst Posix_simp_nullable)
-using Posix.intros(1) Posix1(1) nullable_correctness apply blast
-apply(simp)
-apply(rule Posix.intros)
-apply(rule Posix_mkeps)
-using Posix.intros(1) Posix1(1) nullable_correctness apply blast
-apply(auto)
-done
-
-lemma slexer_correctness:
-  shows "slexer r s = lexer r s"
-apply(induct s arbitrary: r)
-apply(simp)
-apply(simp)
-apply(auto split: option.split prod.split)
-apply (metis L_fst_simp fst_conv lex_correct1a)
-using L_fst_simp lex_correct1a apply fastforce
-by (metis Posix_determ Posix_simp fst_conv lex_correct1 lex_correct3a option.distinct(1) option.inject snd_conv)
-
-
 
 
 
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/thys/Simplifying.thy	Mon Mar 14 23:08:58 2016 +0000
@@ -0,0 +1,322 @@
+theory Simplifying
+  imports "ReStar" 
+begin
+
+section {* Lexer including simplifications *}
+
+
+fun F_RIGHT where
+  "F_RIGHT f v = Right (f v)"
+
+fun F_LEFT where
+  "F_LEFT f v = Left (f v)"
+
+fun F_ALT where
+  "F_ALT f\<^sub>1 f\<^sub>2 (Right v) = Right (f\<^sub>2 v)"
+| "F_ALT f\<^sub>1 f\<^sub>2 (Left v) = Left (f\<^sub>1 v)"  
+| "F_ALT f1 f2 v = v"
+
+
+fun F_SEQ1 where
+  "F_SEQ1 f\<^sub>1 f\<^sub>2 v = Seq (f\<^sub>1 Void) (f\<^sub>2 v)"
+
+fun F_SEQ2 where 
+  "F_SEQ2 f\<^sub>1 f\<^sub>2 v = Seq (f\<^sub>1 v) (f\<^sub>2 Void)"
+
+fun F_SEQ where 
+  "F_SEQ f\<^sub>1 f\<^sub>2 (Seq v\<^sub>1 v\<^sub>2) = Seq (f\<^sub>1 v\<^sub>1) (f\<^sub>2 v\<^sub>2)"
+| "F_SEQ f1 f2 v = v"
+
+fun simp_ALT where
+  "simp_ALT (ZERO, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (r\<^sub>2, F_RIGHT f\<^sub>2)"
+| "simp_ALT (r\<^sub>1, f\<^sub>1) (ZERO, f\<^sub>2) = (r\<^sub>1, F_LEFT f\<^sub>1)"
+| "simp_ALT (r\<^sub>1, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (ALT r\<^sub>1 r\<^sub>2, F_ALT f\<^sub>1 f\<^sub>2)"
+
+fun simp_SEQ where
+  "simp_SEQ (ONE, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (r\<^sub>2, F_SEQ1 f\<^sub>1 f\<^sub>2)"
+| "simp_SEQ (r\<^sub>1, f\<^sub>1) (ONE, f\<^sub>2) = (r\<^sub>1, F_SEQ2 f\<^sub>1 f\<^sub>2)"
+| "simp_SEQ (r\<^sub>1, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (SEQ r\<^sub>1 r\<^sub>2, F_SEQ f\<^sub>1 f\<^sub>2)"  
+ 
+lemma simp_SEQ_simps:
+  "simp_SEQ p1 p2 = (if (fst p1 = ONE) then (fst p2, F_SEQ1 (snd p1) (snd p2))
+                    else (if (fst p2 = ONE) then (fst p1, F_SEQ2 (snd p1) (snd p2))
+                    else (SEQ (fst p1) (fst p2), F_SEQ (snd p1) (snd p2))))"
+apply(auto)
+apply(case_tac p1)
+apply(case_tac p2)
+apply(simp)
+apply(case_tac p1)
+apply(case_tac p2)
+apply(simp)
+apply(case_tac a)
+apply(simp_all)
+apply(case_tac p1)
+apply(case_tac p2)
+apply(simp)
+apply(case_tac p1)
+apply(case_tac p2)
+apply(simp)
+apply(case_tac a)
+apply(simp_all)
+apply(case_tac aa)
+apply(simp_all)
+apply(auto)
+apply(case_tac aa)
+apply(simp_all)
+apply(case_tac aa)
+apply(simp_all)
+apply(case_tac aa)
+apply(simp_all)
+apply(case_tac aa)
+apply(simp_all)
+done
+
+lemma simp_ALT_simps:
+  "simp_ALT p1 p2 = (if (fst p1 = ZERO) then (fst p2, F_RIGHT (snd p2))
+                    else (if (fst p2 = ZERO) then (fst p1, F_LEFT (snd p1))
+                    else (ALT (fst p1) (fst p2), F_ALT (snd p1) (snd p2))))"
+apply(auto)
+apply(case_tac p1)
+apply(case_tac p2)
+apply(simp)
+apply(case_tac p1)
+apply(case_tac p2)
+apply(simp)
+apply(case_tac a)
+apply(simp_all)
+apply(case_tac p1)
+apply(case_tac p2)
+apply(simp)
+apply(case_tac p1)
+apply(case_tac p2)
+apply(simp)
+apply(case_tac a)
+apply(simp_all)
+apply(case_tac aa)
+apply(simp_all)
+apply(auto)
+apply(case_tac aa)
+apply(simp_all)
+apply(case_tac aa)
+apply(simp_all)
+apply(case_tac aa)
+apply(simp_all)
+apply(case_tac aa)
+apply(simp_all)
+done
+
+
+fun 
+  simp :: "rexp \<Rightarrow> rexp * (val \<Rightarrow> val)"
+where
+  "simp (ALT r1 r2) = simp_ALT (simp r1) (simp r2)" 
+| "simp (SEQ r1 r2) = simp_SEQ (simp r1) (simp r2)" 
+| "simp r = (r, id)"
+
+fun 
+  slexer :: "rexp \<Rightarrow> string \<Rightarrow> val option"
+where
+  "slexer r [] = (if nullable r then Some(mkeps r) else None)"
+| "slexer r (c#s) = (let (rs, fr) = simp (der c r) in
+                         (case (slexer rs s) of  
+                            None \<Rightarrow> None
+                          | Some(v) \<Rightarrow> Some(injval r c (fr v))))"
+
+
+lemma L_fst_simp:
+  shows "L(r) = L(fst (simp r))"
+using assms
+apply(induct r rule: rexp.induct)
+apply(auto simp add: simp_SEQ_simps simp_ALT_simps)
+done
+
+lemma 
+  shows "\<turnstile> ((snd (simp r)) v) : r \<longleftrightarrow> \<turnstile> v : (fst (simp r))"
+using assms
+apply(induct r arbitrary: v rule: simp.induct)
+apply(auto simp add: simp_SEQ_simps simp_ALT_simps intro: Prf.intros)
+using Prf_elims(3) apply blast
+apply(erule Prf_elims)
+apply(simp)
+apply(clarify)
+apply(blast)
+apply(simp)
+apply(erule Prf_elims)
+apply(simp)
+apply(simp)
+apply(clarify)
+apply(blast)
+apply(erule Prf_elims)
+apply(case_tac v)
+apply(simp_all)
+apply(rule Prf.intros)
+apply(clarify)
+apply(simp)
+apply(case_tac v)
+apply(simp_all)
+apply(rule Prf.intros)
+apply(clarify)
+apply(simp)
+apply(erule Prf_elims)
+apply(simp)
+apply(rule Prf.intros)
+apply(simp)
+apply(simp)
+apply(rule Prf.intros)
+apply(simp)
+apply(erule Prf_elims)
+apply(simp)
+apply(blast)
+apply(rule Prf.intros)
+apply(erule Prf_elims)
+apply(simp)
+apply(rule Prf.intros)
+apply(erule Prf_elims)
+apply(simp)
+apply(rule Prf.intros)
+apply(erule Prf_elims)
+apply(simp)
+apply(clarify)
+apply(blast)
+apply(rule Prf.intros)
+apply(blast)
+using Prf.intros(4) apply blast
+apply(erule Prf_elims)
+apply(simp)
+apply(clarify)
+apply(blast)
+apply(rule Prf.intros)
+using Prf.intros(4) apply blast
+apply blast
+apply(erule Prf_elims)
+apply(case_tac v)
+apply(simp_all)
+apply(rule Prf.intros)
+apply(clarify)
+apply(simp)
+apply(clarify)
+apply(blast)
+apply(erule Prf_elims)
+apply(case_tac v)
+apply(simp_all)
+apply(rule Prf.intros)
+apply(clarify)
+apply(simp)
+apply(simp)
+done
+
+lemma Posix_simp_nullable:
+  assumes "nullable r" "[] \<in> (fst (simp r)) \<rightarrow> v"
+  shows "((snd (simp r)) v) = mkeps r"
+using assms 
+apply(induct r arbitrary: v)
+apply(auto simp add: simp_SEQ_simps simp_ALT_simps)
+apply(erule Posix_elims)
+apply(simp)
+apply(erule Posix_elims)
+apply(clarify)
+using Posix.intros(1) apply blast
+using Posix.intros(1) apply blast
+using Posix.intros(1) apply blast
+apply(erule Posix_elims)
+apply(simp)
+apply(erule Posix_elims)
+apply (metis L_fst_simp nullable.simps(1) nullable_correctness)
+apply(erule Posix_elims)
+apply(clarify)
+apply(simp)
+apply(clarify)
+apply(simp)
+apply(simp only: L_fst_simp[symmetric])
+apply (simp add: nullable_correctness)
+apply(erule Posix_elims)
+using L_fst_simp Posix1(1) nullable_correctness apply blast
+apply (metis L.simps(1) L_fst_simp Prf_flat_L empty_iff mkeps_nullable)
+apply(erule Posix_elims)
+apply(clarify)
+apply(simp)
+apply(simp only: L_fst_simp[symmetric])
+apply (simp add: nullable_correctness)
+apply(erule Posix_elims)
+apply(clarify)
+apply(simp)
+using L_fst_simp Posix1(1) nullable_correctness apply blast
+apply(simp)
+apply(erule Posix_elims)
+apply(clarify)
+apply(simp)
+using Posix1(2) apply auto[1]
+apply(simp)
+done
+
+lemma Posix_simp:
+  assumes "s \<in> (fst (simp r)) \<rightarrow> v" 
+  shows "s \<in> r \<rightarrow> ((snd (simp r)) v)"
+using assms
+apply(induct r arbitrary: s v rule: rexp.induct) 
+apply(auto split: if_splits simp add: simp_SEQ_simps simp_ALT_simps)
+prefer 3
+apply(erule Posix_elims)
+apply(clarify)
+apply(simp)
+apply(rule Posix.intros)
+apply(blast)
+apply(blast)
+apply(auto)[1]
+apply(simp add: L_fst_simp[symmetric])
+apply(auto)[1]
+prefer 3
+apply(rule Posix.intros)
+apply(blast)
+apply (metis L.simps(1) L_fst_simp equals0D)
+prefer 3
+apply(rule Posix.intros)
+apply(blast)
+prefer 3
+apply(erule Posix_elims)
+apply(clarify)
+apply(simp)
+apply(rule Posix.intros)
+apply(blast)
+apply(simp)
+apply(rule Posix.intros)
+apply(blast)
+apply(simp add: L_fst_simp[symmetric])
+apply(subst append.simps[symmetric])
+apply(rule Posix.intros)
+prefer 2
+apply(blast)
+prefer 2
+apply(auto)[1]
+apply (metis L_fst_simp Posix_elims(2) lex_correct3a)
+apply(subst Posix_simp_nullable)
+using Posix.intros(1) Posix1(1) nullable_correctness apply blast
+apply(simp)
+apply(rule Posix.intros)
+apply(rule Posix_mkeps)
+using Posix.intros(1) Posix1(1) nullable_correctness apply blast
+apply(subst append_Nil2[symmetric])
+apply(rule Posix.intros)
+apply(blast)
+apply(subst Posix_simp_nullable)
+using Posix.intros(1) Posix1(1) nullable_correctness apply blast
+apply(simp)
+apply(rule Posix.intros)
+apply(rule Posix_mkeps)
+using Posix.intros(1) Posix1(1) nullable_correctness apply blast
+apply(auto)
+done
+
+lemma slexer_correctness:
+  shows "slexer r s = lexer r s"
+apply(induct s arbitrary: r)
+apply(simp)
+apply(simp)
+apply(auto split: option.split prod.split)
+apply (metis L_fst_simp fst_conv lex_correct1a)
+using L_fst_simp lex_correct1a apply fastforce
+by (metis Posix_determ Posix_simp fst_conv lex_correct1 lex_correct3a option.distinct(1) option.inject snd_conv)
+
+
+
+end
\ No newline at end of file
lexing