--- a/thys/Paper/Paper.thy	Fri Mar 11 10:43:44 2016 +0000
+++ b/thys/Paper/Paper.thy	Fri Mar 11 13:53:53 2016 +0000
@@ -39,7 +39,7 @@
   length ("len _" [78] 73) and
  
   Prf ("_ : _" [75,75] 75) and  
-  PMatch ("'(_, _') \<rightarrow> _" [63,75,75] 75) and
+  Posix ("'(_, _') \<rightarrow> _" [63,75,75] 75) and
  
   lexer ("lexer _ _" [78,78] 77) and 
   F_RIGHT ("F\<^bsub>Right\<^esub> _") and
@@ -586,24 +586,24 @@
 
   \begin{center}
   \begin{tabular}{c}
-  @{thm[mode=Axiom] PMatch.intros(1)}@{text "P"}@{term "ONE"} \qquad
-  @{thm[mode=Axiom] PMatch.intros(2)}@{text "P"}@{term "c"}\bigskip\\
-  @{thm[mode=Rule] PMatch.intros(3)[of "s" "r\<^sub>1" "v" "r\<^sub>2"]}@{text "P+L"}\qquad
-  @{thm[mode=Rule] PMatch.intros(4)[of "s" "r\<^sub>2" "v" "r\<^sub>1"]}@{text "P+R"}\bigskip\\
+  @{thm[mode=Axiom] Posix.intros(1)}@{text "P"}@{term "ONE"} \qquad
+  @{thm[mode=Axiom] Posix.intros(2)}@{text "P"}@{term "c"}\bigskip\\
+  @{thm[mode=Rule] Posix.intros(3)[of "s" "r\<^sub>1" "v" "r\<^sub>2"]}@{text "P+L"}\qquad
+  @{thm[mode=Rule] Posix.intros(4)[of "s" "r\<^sub>2" "v" "r\<^sub>1"]}@{text "P+R"}\bigskip\\
   $\mprset{flushleft}
    \inferrule
-   {@{thm (prem 1) PMatch.intros(5)[of "s\<^sub>1" "r\<^sub>1" "v\<^sub>1" "s\<^sub>2" "r\<^sub>2" "v\<^sub>2"]} \qquad
-    @{thm (prem 2) PMatch.intros(5)[of "s\<^sub>1" "r\<^sub>1" "v\<^sub>1" "s\<^sub>2" "r\<^sub>2" "v\<^sub>2"]} \\\\
-    @{thm (prem 3) PMatch.intros(5)[of "s\<^sub>1" "r\<^sub>1" "v\<^sub>1" "s\<^sub>2" "r\<^sub>2" "v\<^sub>2"]}}
-   {@{thm (concl) PMatch.intros(5)[of "s\<^sub>1" "r\<^sub>1" "v\<^sub>1" "s\<^sub>2" "r\<^sub>2" "v\<^sub>2"]}}$@{text "PS"}\\
-  @{thm[mode=Axiom] PMatch.intros(7)}@{text "P[]"}\bigskip\\
+   {@{thm (prem 1) Posix.intros(5)[of "s\<^sub>1" "r\<^sub>1" "v\<^sub>1" "s\<^sub>2" "r\<^sub>2" "v\<^sub>2"]} \qquad
+    @{thm (prem 2) Posix.intros(5)[of "s\<^sub>1" "r\<^sub>1" "v\<^sub>1" "s\<^sub>2" "r\<^sub>2" "v\<^sub>2"]} \\\\
+    @{thm (prem 3) Posix.intros(5)[of "s\<^sub>1" "r\<^sub>1" "v\<^sub>1" "s\<^sub>2" "r\<^sub>2" "v\<^sub>2"]}}
+   {@{thm (concl) Posix.intros(5)[of "s\<^sub>1" "r\<^sub>1" "v\<^sub>1" "s\<^sub>2" "r\<^sub>2" "v\<^sub>2"]}}$@{text "PS"}\\
+  @{thm[mode=Axiom] Posix.intros(7)}@{text "P[]"}\bigskip\\
   $\mprset{flushleft}
    \inferrule
-   {@{thm (prem 1) PMatch.intros(6)[of "s\<^sub>1" "r" "v" "s\<^sub>2" "vs"]} \qquad
-    @{thm (prem 2) PMatch.intros(6)[of "s\<^sub>1" "r" "v" "s\<^sub>2" "vs"]} \qquad
-    @{thm (prem 3) PMatch.intros(6)[of "s\<^sub>1" "r" "v" "s\<^sub>2" "vs"]} \\\\
-    @{thm (prem 4) PMatch.intros(6)[of "s\<^sub>1" "r" "v" "s\<^sub>2" "vs"]}}
-   {@{thm (concl) PMatch.intros(6)[of "s\<^sub>1" "r" "v" "s\<^sub>2" "vs"]}}$@{text "P\<star>"}
+   {@{thm (prem 1) Posix.intros(6)[of "s\<^sub>1" "r" "v" "s\<^sub>2" "vs"]} \qquad
+    @{thm (prem 2) Posix.intros(6)[of "s\<^sub>1" "r" "v" "s\<^sub>2" "vs"]} \qquad
+    @{thm (prem 3) Posix.intros(6)[of "s\<^sub>1" "r" "v" "s\<^sub>2" "vs"]} \\\\
+    @{thm (prem 4) Posix.intros(6)[of "s\<^sub>1" "r" "v" "s\<^sub>2" "vs"]}}
+   {@{thm (concl) Posix.intros(6)[of "s\<^sub>1" "r" "v" "s\<^sub>2" "vs"]}}$@{text "P\<star>"}
   \end{tabular}
   \end{center}
 
@@ -645,13 +645,13 @@
    v"}.
 
   \begin{theorem}
-  @{thm[mode=IfThen] PMatch_determ(1)[of _ _ "v\<^sub>1" "v\<^sub>2"]}
+  @{thm[mode=IfThen] Posix_determ(1)[of _ _ "v\<^sub>1" "v\<^sub>2"]}
   \end{theorem}
 
   \begin{proof} By induction on the definition of @{term "s \<in> r \<rightarrow> v\<^sub>1"} and
   a case analysis of @{term "s \<in> r \<rightarrow> v\<^sub>2"}. This proof requires the
-  auxiliary lemma that @{thm (prem 1) PMatch1(1)} implies @{thm (concl)
-  PMatch1(1)} and @{thm (concl) PMatch1(2)}, which are both easily
+  auxiliary lemma that @{thm (prem 1) Posix1(1)} implies @{thm (concl)
+  Posix1(1)} and @{thm (concl) Posix1(2)}, which are both easily
   established by inductions.\qed \end{proof}
 
   \noindent
@@ -659,7 +659,7 @@
   the POSIX value for the empty string and a nullable regular expression.
 
   \begin{lemma}\label{lemmkeps}
-  @{thm[mode=IfThen] PMatch_mkeps}
+  @{thm[mode=IfThen] Posix_mkeps}
   \end{lemma}
 
   \begin{proof}
@@ -670,8 +670,8 @@
   The central lemma for our POSIX relation is that the @{text inj}-function
   preserves POSIX values.
 
-  \begin{lemma}\label{PMatch2}
-  @{thm[mode=IfThen] PMatch2_roy_version}
+  \begin{lemma}\label{Posix2}
+  @{thm[mode=IfThen] Posix2_roy_version}
   \end{lemma}
 
   \begin{proof}
@@ -730,7 +730,7 @@
   \end{proof}
 
   \noindent
-  With Lem.~\ref{PMatch2} in place, it is completely routine to establish
+  With Lem.~\ref{Posix2} in place, it is completely routine to establish
   that the Sulzmann and Lu lexer satisfies our specification (returning
   an ``error'' iff the string is not in the language of the regular expression,
   and returning a unique POSIX value iff the string \emph{is} in the language):
@@ -743,7 +743,7 @@
   \end{theorem}
 
   \begin{proof}
-  By induction on @{term s} using Lem.~\ref{lemmkeps} and \ref{PMatch2}.\qed  
+  By induction on @{term s} using Lem.~\ref{lemmkeps} and \ref{Posix2}.\qed  
   \end{proof}
 
   \noindent This concludes our correctness proof. Note that we have not

--- 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 *}
 

Binary file thys/paper.pdf has changed