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

diff -r 08dcf0d20f15 -r 1e7b36450d9a thys/ReStar.thy
--- a/thys/ReStar.thy	Thu Mar 10 23:43:04 2016 +0000
+++ b/thys/ReStar.thy	Fri Mar 11 00:38:38 2016 +0000
@@ -403,13 +403,20 @@
     \<Longrightarrow> (s1 @ s2) \<in> STAR r \<rightarrow> Stars (v # vs)"
 | "[] \<in> STAR r \<rightarrow> Stars []"
 
+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"
+
 lemma PMatch1:
   assumes "s \<in> r \<rightarrow> v"
   shows "s \<in> L r" "flat v = s"
 using assms
-apply(induct s r v rule: PMatch.induct)
-apply(auto simp add: Sequ_def)
-done
+by (induct s r v rule: PMatch.induct)
+   (auto simp add: Sequ_def)
+
 
 lemma PMatch1a:
   assumes "s \<in> r \<rightarrow> v"
@@ -430,14 +437,6 @@
 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"
@@ -497,24 +496,24 @@
 (* a proof that does not need proj *)
 lemma PMatch2_roy_version:
   assumes "s \<in> (der c r) \<rightarrow> v"
-  shows "(c#s) \<in> r \<rightarrow> (injval r c v)"
+  shows "(c # s) \<in> r \<rightarrow> (injval r c v)"
 using assms
 proof(induct r arbitrary: s v rule: rexp.induct)
   case ZERO
   have "s \<in> der c ZERO \<rightarrow> v" by fact
   then have "s \<in> ZERO \<rightarrow> v" by simp
   then have "False" by cases
-  then show "(c#s) \<in> ZERO \<rightarrow> (injval ZERO c v)" by simp
+  then show "(c # s) \<in> ZERO \<rightarrow> (injval ZERO c v)" by simp
 next
   case ONE
   have "s \<in> der c ONE \<rightarrow> v" by fact
   then have "s \<in> ZERO \<rightarrow> v" by simp
   then have "False" by cases
-  then show "(c#s) \<in> ONE \<rightarrow> (injval ONE c v)" by simp
+  then show "(c # s) \<in> ONE \<rightarrow> (injval ONE c v)" by simp
 next 
   case (CHAR d)
   consider (eq) "c = d" | (ineq) "c \<noteq> d" by blast
-  then show "(c#s) \<in> (CHAR d) \<rightarrow> (injval (CHAR d) c v)"
+  then show "(c # s) \<in> (CHAR d) \<rightarrow> (injval (CHAR d) c v)"
   proof (cases)
     case eq
     have "s \<in> der c (CHAR d) \<rightarrow> v" by fact
@@ -649,28 +648,18 @@
   shows "matcher r s = None"
 using assms
 apply(induct s arbitrary: r)
-apply(simp)
-apply (metis nullable_correctness)
-apply(auto)
+apply(simp add: nullable_correctness)
 apply(drule_tac x="der a r" in meta_spec)
-apply(drule meta_mp)
-apply(auto)
-apply(simp add: der_correctness Der_def)
+apply(auto simp add: der_correctness Der_def)
 done
 
 lemma lex_correct1a:
   shows "s \<notin> L r \<longleftrightarrow> matcher r s = None"
 using assms
 apply(induct s arbitrary: r)
-apply(simp)
-apply (metis nullable_correctness)
-apply(auto)
+apply(simp add: nullable_correctness)
 apply(drule_tac x="der a r" in meta_spec)
-apply(auto)
-apply(simp add: der_correctness Der_def)
-apply(drule_tac x="der a r" in meta_spec)
-apply(auto)
-apply(simp add: der_correctness Der_def)
+apply(auto simp add: der_correctness Der_def)
 done
 
 lemma lex_correct2: