diff -r 702ed601349b -r ec3d221bfc45 thys/ReStar.thy
--- a/thys/ReStar.thy	Sun Mar 13 01:07:34 2016 +0000
+++ b/thys/ReStar.thy	Mon Mar 14 15:15:29 2016 +0000
@@ -355,6 +355,7 @@
 | "[] \<in> STAR r \<rightarrow> Stars []"
 
 inductive_cases Posix_elims:
+  "s \<in> ZERO \<rightarrow> v"
   "s \<in> ONE \<rightarrow> v"
   "s \<in> CHAR c \<rightarrow> v"
   "s \<in> ALT r1 r2 \<rightarrow> v"
@@ -388,6 +389,123 @@
 apply(auto)
 done
 
+(*
+lemma Posix_determ:
+  assumes "s \<in> r \<rightarrow> v1" "s \<in> r \<rightarrow> v2"
+  shows "v1 = v2"
+using assms
+
+
+
+proof (induct s r v1 arbitrary: v2 rule: Posix.induct)
+  case (1 v2)lemma Posix_determ:
+  assumes "s \<in> r \<rightarrow> v1" "s \<in> r \<rightarrow> v2"
+  shows "v1 = v2"
+using assms
+apply(induct s r v1 arbitrary: v2 rule: Posix.induct)
+apply(erule Posix.cases)
+apply(simp_all)[7]
+apply(erule Posix.cases)
+apply(simp_all)[7]
+apply(rotate_tac 2)
+apply(erule Posix.cases)
+apply(simp_all (no_asm_use))[7]
+apply(clarify)
+apply(force)
+apply(clarify)
+apply(drule Posix1(1))
+apply(simp)
+apply(rotate_tac 3)
+apply(erule Posix.cases)
+apply(simp_all (no_asm_use))[7]
+apply(drule Posix1(1))+
+apply(simp)
+apply(simp)
+apply(rotate_tac 5)
+apply(erule Posix.cases)
+apply(simp_all (no_asm_use))[7]
+apply(clarify)
+apply(subgoal_tac "s1 = s1a")
+apply(blast)
+apply(simp add: append_eq_append_conv2)
+apply(clarify)
+apply (metis Posix1(1) append_self_conv)
+apply(rotate_tac 6)
+apply(erule Posix.cases)
+apply(simp_all (no_asm_use))[7]
+apply(clarify)
+apply(subgoal_tac "s1 = s1a")
+apply(simp)
+apply(blast)
+apply(simp  (no_asm_use) add: append_eq_append_conv2)
+apply(clarify)
+apply (metis L.simps(6) Posix1(1) append_self_conv)
+apply(clarify)
+apply(rotate_tac 2)
+apply(erule Posix.cases)
+apply(simp_all (no_asm_use))[7]
+using Posix1(2) apply auto[1]
+using Posix1(2) apply blast
+apply(erule Posix.cases)
+apply(simp_all (no_asm_use))[7]
+apply(clarify)
+apply (simp add: Posix1(2))
+apply(simp)
+done
+  then have "[] \<in> ONE \<rightarrow> v2" by simp
+  then show "Void = v2"
+  apply(auto: elim Posix_elims)[1]  
+
+apply(erule Posix.cases)
+apply(simp_all)[7]
+apply(erule Posix.cases)
+apply(simp_all)[7]
+apply(rotate_tac 2)
+apply(erule Posix.cases)
+apply(simp_all (no_asm_use))[7]
+apply(clarify)
+apply(force)
+apply(clarify)
+apply(drule Posix1(1))
+apply(simp)
+apply(rotate_tac 3)
+apply(erule Posix.cases)
+apply(simp_all (no_asm_use))[7]
+apply(drule Posix1(1))+
+apply(simp)
+apply(simp)
+apply(rotate_tac 5)
+apply(erule Posix.cases)
+apply(simp_all (no_asm_use))[7]
+apply(clarify)
+apply(subgoal_tac "s1 = s1a")
+apply(blast)
+apply(simp add: append_eq_append_conv2)
+apply(clarify)
+apply (metis Posix1(1) append_self_conv)
+apply(rotate_tac 6)
+apply(erule Posix.cases)
+apply(simp_all (no_asm_use))[7]
+apply(clarify)
+apply(subgoal_tac "s1 = s1a")
+apply(simp)
+apply(blast)
+apply(simp  (no_asm_use) add: append_eq_append_conv2)
+apply(clarify)
+apply (metis L.simps(6) Posix1(1) append_self_conv)
+apply(clarify)
+apply(rotate_tac 2)
+apply(erule Posix.cases)
+apply(simp_all (no_asm_use))[7]
+using Posix1(2) apply auto[1]
+using Posix1(2) apply blast
+apply(erule Posix.cases)
+apply(simp_all (no_asm_use))[7]
+apply(clarify)
+apply (simp add: Posix1(2))
+apply(simp)
+done
+*)
 
 lemma Posix_determ:
   assumes "s \<in> r \<rightarrow> v1" "s \<in> r \<rightarrow> v2"
@@ -568,9 +686,9 @@
         "v = Seq v1 (Stars vs)" "s = s1 @ s2" 
         "s1 \<in> der c r \<rightarrow> v1" "s2 \<in> (STAR r) \<rightarrow> (Stars vs)"
         "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L (der c r) \<and> s\<^sub>4 \<in> L (STAR r))" 
-        apply(auto elim!: Posix_elims(1-4) simp add: der_correctness Der_def intro: Posix.intros)
+        apply(auto elim!: Posix_elims(1-5) simp add: der_correctness Der_def intro: Posix.intros)
         apply(rotate_tac 3)
-        apply(erule_tac Posix_elims(5))
+        apply(erule_tac Posix_elims(6))
         apply (simp add: Posix.intros(6))
         using Posix.intros(7) by blast
     then show "(c # s) \<in> STAR r \<rightarrow> injval (STAR r) c v" 
@@ -698,7 +816,9 @@
 
 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 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)"
@@ -708,6 +828,7 @@
 
 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)"
@@ -719,6 +840,75 @@
 | "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
@@ -735,4 +925,203 @@
                             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