diff -r ec3d221bfc45 -r 09f81fee11ce thys/Simplifying.thy
--- /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