# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1457653384 0
# Node ID 08dcf0d20f15cf7c1d1492cc1529e89e3627e5cd
# Parent  879d43256063dd39f16938ad21e3d44b33c986e1
updated

diff -r 879d43256063 -r 08dcf0d20f15 thys/ReStar.thy
--- a/thys/ReStar.thy	Wed Mar 09 10:33:26 2016 +0000
+++ b/thys/ReStar.thy	Thu Mar 10 23:43:04 2016 +0000
@@ -157,9 +157,7 @@
 
 lemma der_correctness:
   shows "L (der c r) = Der c (L r)"
-apply(induct r) 
-apply(simp_all add: nullable_correctness)
-done
+by (induct r) (simp_all add: nullable_correctness)
 
 
 section {* Values *}
@@ -206,11 +204,15 @@
 | "\<turnstile> Stars [] : STAR r"
 | "\<lbrakk>\<turnstile> v : r; \<turnstile> Stars vs : STAR r\<rbrakk> \<Longrightarrow> \<turnstile> Stars (v # vs) : STAR r"
 
-lemma not_nullable_flat:
-  assumes "\<turnstile> v : r" "\<not> nullable r"
-  shows "flat v \<noteq> []"
-using assms
-by (induct) (auto)
+inductive_cases Prf_elims:
+  "\<turnstile> v : ZERO"
+  "\<turnstile> v : SEQ r1 r2"
+  "\<turnstile> v : ALT r1 r2"
+  "\<turnstile> v : ONE"
+  "\<turnstile> v : CHAR c"
+(*  "\<turnstile> vs : STAR r"*)
+
+
 
 lemma Prf_flat_L:
   assumes "\<turnstile> v : r" shows "flat v \<in> L r"
@@ -239,6 +241,7 @@
 apply(simp)
 done
 
+
 lemma Star_val:
   assumes "\<forall>s\<in>set ss. \<exists>v. s = flat v \<and> \<turnstile> v : r"
   shows "\<exists>vs. concat (map flat vs) = concat ss \<and> (\<forall>v\<in>set vs. \<turnstile> v : r)"
@@ -258,8 +261,7 @@
 apply (metis Prf.intros(1) flat.simps(5))
 apply (metis Prf.intros(2) flat.simps(3))
 apply (metis Prf.intros(3) flat.simps(4))
-apply(erule Prf.cases)
-apply(auto)
+apply(auto elim!: Prf_elims)
 apply(subgoal_tac "\<exists>vs::val list. concat (map flat vs) = x \<and> (\<forall>v \<in> set vs. \<turnstile> v : r)")
 apply(auto)[1]
 apply(rule_tac x="Stars vs" in exI)
@@ -304,13 +306,6 @@
                     None \<Rightarrow> None
                   | Some(v) \<Rightarrow> Some(injval r c v))"
 
-fun 
-  matcher2 :: "rexp \<Rightarrow> string \<Rightarrow> val"
-where
-  "matcher2 r [] = mkeps r"
-| "matcher2 r (c#s) = injval r c (matcher2 (der c r) s)"
-
-
 
 section {* Mkeps, injval *}
 
@@ -318,67 +313,23 @@
   assumes "nullable(r)" 
   shows "\<turnstile> mkeps r : r"
 using assms
-apply(induct rule: nullable.induct)
-apply(auto intro: Prf.intros)
-done
+by (induct rule: nullable.induct) 
+   (auto intro: Prf.intros)
 
 lemma mkeps_flat:
   assumes "nullable(r)" 
   shows "flat (mkeps r) = []"
 using assms
-apply(induct rule: nullable.induct)
-apply(auto)
-done
+by (induct rule: nullable.induct) (auto)
+
 
 lemma Prf_injval:
   assumes "\<turnstile> v : der c r" 
   shows "\<turnstile> (injval r c v) : r"
 using assms
 apply(induct r arbitrary: c v rule: rexp.induct)
-apply(simp_all)
-(* ZERO *)
-apply(erule Prf.cases)
-apply(simp_all)[7]
-(* ONE *)
-apply(erule Prf.cases)
-apply(simp_all)[7]
-(* CHAR *)
-apply(case_tac "c = x")
-apply(simp)
-apply(erule Prf.cases)
-apply(simp_all)[7]
-apply(rule Prf.intros(5))
-apply(simp)
-apply(erule Prf.cases)
-apply(simp_all)[7]
-(* SEQ *)
-apply(case_tac "nullable x1")
-apply(simp)
-apply(erule Prf.cases)
-apply(simp_all)[7]
-apply(auto)[1]
-apply(erule Prf.cases)
-apply(simp_all)[7]
-apply(auto)[1]
-apply(rule Prf.intros)
-apply(auto)[2]
-apply (metis Prf.intros(1) mkeps_nullable)
-apply(simp)
-apply(erule Prf.cases)
-apply(simp_all)[7]
-apply(auto)[1]
-apply(rule Prf.intros)
-apply(auto)[2]
-(* ALT *)
-apply(erule Prf.cases)
-apply(simp_all)[7]
-apply(clarify)
-apply (metis Prf.intros(2))
-apply (metis Prf.intros(3))
+apply(auto intro!: Prf.intros mkeps_nullable elim!: Prf_elims split: if_splits)
 (* STAR *)
-apply(erule Prf.cases)
-apply(simp_all)[7]
-apply(clarify)
 apply(rotate_tac 2)
 apply(erule Prf.cases)
 apply(simp_all)[7]
@@ -479,6 +430,15 @@
 apply(auto)
 done
 
+inductive_cases PMatch_elims:
+  "s \<in> ONE \<rightarrow> v"
+  "s \<in> CHAR c \<rightarrow> v"
+  "s \<in> ALT r1 r2 \<rightarrow> v"
+  "s \<in> SEQ r1 r2 \<rightarrow> v"
+  "s \<in> STAR r \<rightarrow> v"
+
+thm PMatch_elims
+
 lemma PMatch_determ:
   assumes "s \<in> r \<rightarrow> v1" "s \<in> r \<rightarrow> v2"
   shows "v1 = v2"
@@ -560,7 +520,8 @@
     have "s \<in> der c (CHAR d) \<rightarrow> v" by fact
     then have "s \<in> ONE \<rightarrow> v" using eq by simp
     then have eqs: "s = [] \<and> v = Void" by cases simp
-    show "(c # s) \<in> CHAR d \<rightarrow> injval (CHAR d) c v" using eq eqs by (auto intro: PMatch.intros)
+    show "(c # s) \<in> CHAR d \<rightarrow> injval (CHAR d) c v" using eq eqs 
+    by (auto intro: PMatch.intros)
   next
     case ineq
     have "s \<in> der c (CHAR d) \<rightarrow> v" by fact
@@ -612,9 +573,7 @@
         "v = Seq v1 v2" "s = s1 @ s2" 
         "s1 \<in> der c r1 \<rightarrow> v1" "s2 \<in> r2 \<rightarrow> v2" "\<not>nullable r1" 
         "\<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 r1) \<and> s\<^sub>4 \<in> L r2)"
-       apply(auto split: if_splits simp add: Sequ_def) apply(erule PMatch.cases) 
-       apply(auto elim: PMatch.cases simp add: Sequ_def der_correctness Der_def)
-       by fastforce   
+        by (force split: if_splits elim!: PMatch_elims simp add: Sequ_def der_correctness Der_def)   
   then show "(c # s) \<in> SEQ r1 r2 \<rightarrow> injval (SEQ r1 r2) c v" 
     proof (cases)
       case left_nullable
@@ -659,11 +618,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(erule_tac PMatch.cases)
-        apply(auto)
-        apply(rotate_tac 4)
-        apply(erule_tac PMatch.cases)
-        apply(auto)
+        apply(auto elim!: PMatch_elims(1-4) simp add: der_correctness Der_def intro: PMatch.intros)
+        apply(rotate_tac 3)
+        apply(erule_tac PMatch_elims(5))
         apply (simp add: PMatch.intros(6))
         using PMatch.intros(7) by blast
     then show "(c # s) \<in> STAR r \<rightarrow> injval (STAR r) c v" 
@@ -777,25 +734,6 @@
 apply(simp)
 using PMatch1(1) by auto
 
-lemma lex_correct5:
-  assumes "s \<in> L r"
-  shows "s \<in> r \<rightarrow> (matcher2 r s)"
-using assms
-apply(induct s arbitrary: r)
-apply(simp)
-apply (metis PMatch_mkeps nullable_correctness)
-apply(simp)
-apply(rule PMatch2_roy_version)
-apply(drule_tac x="der a r" in meta_spec)
-apply(drule meta_mp)
-apply(simp add: der_correctness Der_def)
-apply(auto)
-done
-
-lemma 
-  "matcher2 (ALT (CHAR a) (ALT (CHAR b) (SEQ (CHAR a) (CHAR b)))) [a,b] = Right (Right (Seq (Char a) (Char b)))"
-apply(simp)
-done
 
 fun F_RIGHT where
   "F_RIGHT f v = Right (f v)"