--- a/thys/Paper/Paper.thy	Mon May 16 12:50:37 2016 +0100
+++ b/thys/Paper/Paper.thy	Mon May 16 15:20:23 2016 +0100
@@ -927,7 +927,19 @@
   @{text "r\<^sub>s"} and a rectification function @{text "f\<^sub>r"}. The lexer
   is then recursively called with the simplified derivative, but before
   we inject the character @{term c} into the value @{term v}, we need to rectify
-  @{term v} (that is construct @{term "f\<^sub>r v"}). We can prove that
+  @{term v} (that is construct @{term "f\<^sub>r v"}). Before we can establish the correctness
+  of @{const "slexer"}, we need to show that simplification preserves the language
+  and the relation between simplification and our posix definition:
+
+  \begin{lemma}\mbox{}\smallskip\\
+  \begin{tabular}{ll}
+  (1) & @{thm L_fst_simp[symmetric]}\\
+  (2) & @{thm[mode=IfThen] Posix_simp}
+  \end{tabular}
+  \end{lemma}
+
+  \noindent
+  We can now prove that
 
   \begin{theorem}
   @{thm slexer_correctness}

--- a/thys/Simplifying.thy	Mon May 16 12:50:37 2016 +0100
+++ b/thys/Simplifying.thy	Mon May 16 15:20:23 2016 +0100
@@ -66,198 +66,79 @@
                           | Some(v) \<Rightarrow> Some(injval r c (fr v))))"
 
 
+lemma slexer_better_simp:
+  "slexer r (c#s) = (case (slexer (fst (simp (der c r))) s) of  
+                            None \<Rightarrow> None
+                          | Some(v) \<Rightarrow> Some(injval r c ((snd (simp (der c r))) v)))"
+by (auto split: prod.split option.split)
+
+
 lemma L_fst_simp:
   shows "L(r) = L(fst (simp r))"
 using assms
 by (induct r) (auto)
 
-
-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 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)
-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)
-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(induct r arbitrary: s v rule: simp.induct)
+apply(simp_all)
 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)
+using Posix_elims(1) apply blast
+apply (simp add: Posix_ALT1)
+apply (metis L.simps(1) L_fst_simp Posix_ALT2 empty_iff)
+apply (smt F_ALT.simps(1) F_ALT.simps(2) L_fst_simp Posix_ALT1 Posix_ALT2 Posix_elims(4))
+apply(auto)[1]
+apply (metis (no_types, lifting) Nil_is_append_conv Posix_SEQ Posix_elims(2))
+apply(subst append_Nil2[symmetric])
+apply(rule Posix_SEQ)
 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
+using Posix_ONE apply blast
+apply blast
+apply(subst append_Nil[symmetric])
+apply(rule Posix_SEQ)
+using Posix_ONE apply blast
+apply blast
 apply(auto)[1]
-apply (metis L_fst_simp Posix_elims(2) lexer_correct_Some)
-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 (metis L.simps(2) L_fst_simp ex_in_conv insert_iff)
+apply(erule Posix_elims)
 apply(auto)
-done
+using L_fst_simp Posix_SEQ by auto
+
 
 lemma slexer_correctness:
   shows "slexer r s = lexer r s"
-apply(induct s arbitrary: r)
-apply(simp)
-apply(auto split: option.split prod.split)
-apply (metis L_fst_simp fst_conv lexer_correct_None)
-using L_fst_simp lexer_correct_None apply fastforce
-by (metis Posix_determ Posix_simp fst_conv lexer_correct_None lexer_correct_Some option.distinct(1) option.inject snd_conv)
-
-
+proof(induct s arbitrary: r)
+  case Nil
+  show "slexer r [] = lexer r []" by simp
+next 
+  case (Cons c s r)
+  have IH: "\<And>r. slexer r s = lexer r s" by fact
+  show "slexer r (c # s) = lexer r (c # s)" 
+   proof (cases "s \<in> L (der c r)")
+     case True
+       assume a1: "s \<in> L (der c r)"
+       then obtain v1 where a2: "lexer (der c r) s = Some v1" "s \<in> der c r \<rightarrow> v1"
+         using lexer_correct_Some by auto
+       from a1 have "s \<in> L (fst (simp (der c r)))" using L_fst_simp[symmetric] by simp
+       then obtain v2 where a3: "lexer (fst (simp (der c r))) s = Some v2" "s \<in> (fst (simp (der c r))) \<rightarrow> v2"
+          using lexer_correct_Some by auto
+       then have a4: "slexer (fst (simp (der c r))) s = Some v2" using IH by simp
+       from a3(2) have "s \<in> der c r \<rightarrow> (snd (simp (der c r))) v2" using Posix_simp by simp
+       with a2(2) have "v1 = (snd (simp (der c r))) v2" using Posix_determ by simp
+       with a2(1) a4 show "slexer r (c # s) = lexer r (c # s)" by (auto split: prod.split)
+     next 
+     case False
+       assume b1: "s \<notin> L (der c r)"
+       then have "lexer (der c r) s = None" using lexer_correct_None by simp
+       moreover
+       from b1 have "s \<notin> L (fst (simp (der c r)))" using L_fst_simp[symmetric] by simp
+       then have "lexer (fst (simp (der c r))) s = None" using lexer_correct_None by simp
+       then have "slexer (fst (simp (der c r))) s = None" using IH by simp
+       ultimately show "slexer r (c # s) = lexer r (c # s)" 
+         by (simp del: slexer.simps add: slexer_better_simp)
+   qed
+qed  
 
 end
\ No newline at end of file

Binary file thys/paper.pdf has changed