diff -r 97735ef233be -r da81ffac4b10 thys/ReStar.thy
--- a/thys/ReStar.thy	Fri Mar 11 10:43:44 2016 +0000
+++ b/thys/ReStar.thy	Fri Mar 11 13:53:53 2016 +0000
@@ -340,7 +340,7 @@
 section {* Our Alternative Posix definition *}
 
 inductive 
-  PMatch :: "string \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<in> _ \<rightarrow> _" [100, 100, 100] 100)
+  Posix :: "string \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<in> _ \<rightarrow> _" [100, 100, 100] 100)
 where
   "[] \<in> ONE \<rightarrow> Void"
 | "[c] \<in> (CHAR c) \<rightarrow> (Char c)"
@@ -354,75 +354,75 @@
     \<Longrightarrow> (s1 @ s2) \<in> STAR r \<rightarrow> Stars (v # vs)"
 | "[] \<in> STAR r \<rightarrow> Stars []"
 
-inductive_cases PMatch_elims:
+inductive_cases Posix_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:
+lemma Posix1:
   assumes "s \<in> r \<rightarrow> v"
   shows "s \<in> L r" "flat v = s"
 using assms
-by (induct s r v rule: PMatch.induct)
+by (induct s r v rule: Posix.induct)
    (auto simp add: Sequ_def)
 
 
-lemma PMatch1a:
+lemma Posix1a:
   assumes "s \<in> r \<rightarrow> v"
   shows "\<turnstile> v : r"
 using assms
-apply(induct s r v rule: PMatch.induct)
+apply(induct s r v rule: Posix.induct)
 apply(auto intro: Prf.intros)
 done
 
-lemma PMatch_mkeps:
+lemma Posix_mkeps:
   assumes "nullable r"
   shows "[] \<in> r \<rightarrow> mkeps r"
 using assms
 apply(induct r)
-apply(auto intro: PMatch.intros simp add: nullable_correctness Sequ_def)
+apply(auto intro: Posix.intros simp add: nullable_correctness Sequ_def)
 apply(subst append.simps(1)[symmetric])
-apply(rule PMatch.intros)
+apply(rule Posix.intros)
 apply(auto)
 done
 
 
-lemma PMatch_determ:
+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: PMatch.induct)
-apply(erule PMatch.cases)
+apply(induct s r v1 arbitrary: v2 rule: Posix.induct)
+apply(erule Posix.cases)
 apply(simp_all)[7]
-apply(erule PMatch.cases)
+apply(erule Posix.cases)
 apply(simp_all)[7]
 apply(rotate_tac 2)
-apply(erule PMatch.cases)
+apply(erule Posix.cases)
 apply(simp_all (no_asm_use))[7]
 apply(clarify)
 apply(force)
 apply(clarify)
-apply(drule PMatch1(1))
+apply(drule Posix1(1))
 apply(simp)
 apply(rotate_tac 3)
-apply(erule PMatch.cases)
+apply(erule Posix.cases)
 apply(simp_all (no_asm_use))[7]
-apply(drule PMatch1(1))+
+apply(drule Posix1(1))+
 apply(simp)
 apply(simp)
 apply(rotate_tac 5)
-apply(erule PMatch.cases)
+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 PMatch1(1) append_self_conv)
+apply (metis Posix1(1) append_self_conv)
 apply(rotate_tac 6)
-apply(erule PMatch.cases)
+apply(erule Posix.cases)
 apply(simp_all (no_asm_use))[7]
 apply(clarify)
 apply(subgoal_tac "s1 = s1a")
@@ -430,22 +430,22 @@
 apply(blast)
 apply(simp  (no_asm_use) add: append_eq_append_conv2)
 apply(clarify)
-apply (metis L.simps(6) PMatch1(1) append_self_conv)
+apply (metis L.simps(6) Posix1(1) append_self_conv)
 apply(clarify)
 apply(rotate_tac 2)
-apply(erule PMatch.cases)
+apply(erule Posix.cases)
 apply(simp_all (no_asm_use))[7]
-using PMatch1(2) apply auto[1]
-using PMatch1(2) apply blast
-apply(erule PMatch.cases)
+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: PMatch1(2))
+apply (simp add: Posix1(2))
 apply(simp)
 done
 
 (* a proof that does not need proj *)
-lemma PMatch2_roy_version:
+lemma Posix2_roy_version:
   assumes "s \<in> (der c r) \<rightarrow> v"
   shows "(c # s) \<in> r \<rightarrow> (injval r c v)"
 using assms
@@ -471,7 +471,7 @@
     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)
+    by (auto intro: Posix.intros)
   next
     case ineq
     have "s \<in> der c (CHAR d) \<rightarrow> v" by fact
@@ -493,7 +493,7 @@
     case left
     have "s \<in> der c r1 \<rightarrow> v'" by fact
     then have "(c # s) \<in> r1 \<rightarrow> injval r1 c v'" using IH1 by simp
-    then have "(c # s) \<in> ALT r1 r2 \<rightarrow> injval (ALT r1 r2) c (Left v')" by (auto intro: PMatch.intros)
+    then have "(c # s) \<in> ALT r1 r2 \<rightarrow> injval (ALT r1 r2) c (Left v')" by (auto intro: Posix.intros)
     then show "(c # s) \<in> ALT r1 r2 \<rightarrow> injval (ALT r1 r2) c v" using left by simp
   next 
     case right
@@ -503,7 +503,7 @@
     have "s \<in> der c r2 \<rightarrow> v'" by fact
     then have "(c # s) \<in> r2 \<rightarrow> injval r2 c v'" using IH2 by simp
     ultimately have "(c # s) \<in> ALT r1 r2 \<rightarrow> injval (ALT r1 r2) c (Right v')" 
-      by (auto intro: PMatch.intros)
+      by (auto intro: Posix.intros)
     then show "(c # s) \<in> ALT r1 r2 \<rightarrow> injval (ALT r1 r2) c v" using right by simp
   qed
 next
@@ -523,7 +523,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)"
-        by (force split: if_splits elim!: PMatch_elims simp add: Sequ_def der_correctness Der_def)   
+        by (force split: if_splits elim!: Posix_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
@@ -532,12 +532,12 @@
       moreover
       have "\<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)" by fact
       then have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (c # s1) @ s\<^sub>3 \<in> L r1 \<and> s\<^sub>4 \<in> L r2)" by (simp add: der_correctness Der_def)
-      ultimately have "((c # s1) @ s2) \<in> SEQ r1 r2 \<rightarrow> Seq (injval r1 c v1) v2" using left_nullable by (rule_tac PMatch.intros)
+      ultimately have "((c # s1) @ s2) \<in> SEQ r1 r2 \<rightarrow> Seq (injval r1 c v1) v2" using left_nullable by (rule_tac Posix.intros)
       then show "(c # s) \<in> SEQ r1 r2 \<rightarrow> injval (SEQ r1 r2) c v" using left_nullable by simp
     next
       case right_nullable
       have "nullable r1" by fact
-      then have "[] \<in> r1 \<rightarrow> (mkeps r1)" by (rule PMatch_mkeps)
+      then have "[] \<in> r1 \<rightarrow> (mkeps r1)" by (rule Posix_mkeps)
       moreover
       have "s \<in> der c r2 \<rightarrow> v1" by fact
       then have "(c # s) \<in> r2 \<rightarrow> (injval r2 c v1)" using IH2 by simp
@@ -546,7 +546,7 @@
       then have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = c # s \<and> [] @ s\<^sub>3 \<in> L r1 \<and> s\<^sub>4 \<in> L r2)" using right_nullable
         by(auto simp add: der_correctness Der_def append_eq_Cons_conv Sequ_def)
       ultimately have "([] @ (c # s)) \<in> SEQ r1 r2 \<rightarrow> Seq (mkeps r1) (injval r2 c v1)"
-      by(rule PMatch.intros)
+      by(rule Posix.intros)
       then show "(c # s) \<in> SEQ r1 r2 \<rightarrow> injval (SEQ r1 r2) c v" using right_nullable by simp
     next
       case not_nullable
@@ -556,7 +556,7 @@
       have "\<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)" by fact
       then have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (c # s1) @ s\<^sub>3 \<in> L r1 \<and> s\<^sub>4 \<in> L r2)" by (simp add: der_correctness Der_def)
       ultimately have "((c # s1) @ s2) \<in> SEQ r1 r2 \<rightarrow> Seq (injval r1 c v1) v2" using not_nullable 
-        by (rule_tac PMatch.intros) (simp_all) 
+        by (rule_tac Posix.intros) (simp_all) 
       then show "(c # s) \<in> SEQ r1 r2 \<rightarrow> injval (SEQ r1 r2) c v" using not_nullable by simp
     qed
 next
@@ -568,11 +568,11 @@
         "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!: PMatch_elims(1-4) simp add: der_correctness Der_def intro: PMatch.intros)
+        apply(auto elim!: Posix_elims(1-4) simp add: der_correctness Der_def intro: Posix.intros)
         apply(rotate_tac 3)
-        apply(erule_tac PMatch_elims(5))
-        apply (simp add: PMatch.intros(6))
-        using PMatch.intros(7) by blast
+        apply(erule_tac Posix_elims(5))
+        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" 
     proof (cases)
       case cons
@@ -582,14 +582,14 @@
           have "s2 \<in> STAR r \<rightarrow> Stars vs" by fact
         moreover 
           have "(c # s1) \<in> r \<rightarrow> injval r c v1" by fact 
-          then have "flat (injval r c v1) = (c # s1)" by (rule PMatch1)
+          then have "flat (injval r c v1) = (c # s1)" by (rule Posix1)
           then have "flat (injval r c v1) \<noteq> []" by simp
         moreover 
           have "\<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))" by fact
           then have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (c # s1) @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (STAR r))" 
             by (simp add: der_correctness Der_def)
         ultimately 
-        have "((c # s1) @ s2) \<in> STAR r \<rightarrow> Stars (injval r c v1 # vs)" by (rule PMatch.intros)
+        have "((c # s1) @ s2) \<in> STAR r \<rightarrow> Stars (injval r c v1 # vs)" by (rule Posix.intros)
         then show "(c # s) \<in> STAR r \<rightarrow> injval (STAR r) c v" using cons by(simp)
     qed
 qed
@@ -647,22 +647,22 @@
 using assms
 apply(induct s arbitrary: r)
 apply(simp)
-apply (metis PMatch_mkeps nullable_correctness)
+apply (metis Posix_mkeps nullable_correctness)
 apply(drule_tac x="der a r" in meta_spec)
 apply(drule meta_mp)
 apply(simp add: der_correctness Der_def)
 apply(auto)
-by (metis PMatch2_roy_version)
+by (metis Posix2_roy_version)
 
 lemma lex_correct3a:
   shows "s \<in> L r \<longleftrightarrow> (\<exists>v. lexer r s = Some(v) \<and> s \<in> r \<rightarrow> v)"
 using assms
 apply(induct s arbitrary: r)
 apply(simp)
-apply (metis PMatch_mkeps nullable_correctness)
+apply (metis Posix_mkeps nullable_correctness)
 apply(drule_tac x="der a r" in meta_spec)
 apply(auto)
-apply(metis PMatch2_roy_version)
+apply(metis Posix2_roy_version)
 apply(simp add: der_correctness Der_def)
 using lex_correct1a 
 apply fastforce
@@ -674,7 +674,7 @@
 using assms
 apply(induct s arbitrary: r)
 apply(simp)
-apply (metis PMatch_mkeps nullable_correctness)
+apply (metis Posix_mkeps nullable_correctness)
 apply(drule_tac x="der a r" in meta_spec)
 apply(simp add: der_correctness Der_def)
 apply(case_tac "lexer (der a r) s = None")
@@ -683,9 +683,9 @@
 apply(clarify)
 apply(rule iffI)
 apply(auto)
-apply(rule PMatch2_roy_version)
+apply(rule Posix2_roy_version)
 apply(simp)
-using PMatch1(1) by auto
+using Posix1(1) by auto
 
 section {* Lexer including simplifications *}