# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1454888674 0
# Node ID 38696f516c6b784a5e70b61b15c1560d230da1b2
# Parent  c3d7125f9950c7cec292eb0edb5e6fd5c7b872ff
updated

diff -r c3d7125f9950 -r 38696f516c6b thys/Paper/Paper.thy
--- a/thys/Paper/Paper.thy	Fri Feb 05 10:16:41 2016 +0000
+++ b/thys/Paper/Paper.thy	Sun Feb 07 23:44:34 2016 +0000
@@ -2,11 +2,219 @@
 theory Paper
 imports "../ReStar" "~~/src/HOL/Library/LaTeXsugar"
 begin
+
+declare [[show_question_marks = false]]
+
+notation (latex output)
+   If  ("(\<^raw:\textrm{>if\<^raw:}> (_)/ \<^raw:\textrm{>then\<^raw:}> (_)/ \<^raw:\textrm{>else\<^raw:}> (_))" 10) and
+  Cons ("_::_" [78,77] 73) and
+  val.Char ("Char _" [1000] 78) and
+  val.Left ("Left _" [1000] 78) and
+  val.Right ("Right _" [1000] 78) and
+  L ("L _" [1000] 0) and
+  flat ("|_|" [70] 73) and
+  Sequ ("_ @ _" [78,77] 63) and
+  injval ("inj _ _ _" [1000,77,1000] 77) and 
+  length ("len _" [78] 73) and
+  ValOrd ("_ \<succeq>\<^bsub>_\<^esub> _" [78,77,77] 73)
 (*>*)
 
 section {* Introduction *}
 
- 
+text {*
+
+  \noindent
+  Regular exprtessions
+
+  \begin{center}
+  @{text "r :="}
+  @{const "NULL"} $\mid$
+  @{const "EMPTY"} $\mid$
+  @{term "CHAR c"} $\mid$
+  @{term "ALT r\<^sub>1 r\<^sub>2"} $\mid$
+  @{term "SEQ r\<^sub>1 r\<^sub>2"} $\mid$
+  @{term "STAR r"} 
+  \end{center}
+
+  \noindent
+  Values
+
+  \begin{center}
+  @{text "v :="}
+  @{const "Void"} $\mid$
+  @{term "val.Char c"} $\mid$
+  @{term "Left v"} $\mid$
+  @{term "Right v"} $\mid$
+  @{term "Seq v\<^sub>1 v\<^sub>2"} $\mid$ 
+  @{term "Stars vs"} 
+  \end{center}  
+
+  \noindent
+  The language of a regular expression
+
+  \begin{center}
+  \begin{tabular}{lcl}
+  @{thm (lhs) L.simps(1)} & $\dn$ & @{thm (rhs) L.simps(1)}\\
+  @{thm (lhs) L.simps(2)} & $\dn$ & @{thm (rhs) L.simps(2)}\\
+  @{thm (lhs) L.simps(3)} & $\dn$ & @{thm (rhs) L.simps(3)}\\
+  @{thm (lhs) L.simps(4)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) L.simps(4)[of "r\<^sub>1" "r\<^sub>2"]}\\
+  @{thm (lhs) L.simps(5)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) L.simps(5)[of "r\<^sub>1" "r\<^sub>2"]}\\
+  @{thm (lhs) L.simps(6)} & $\dn$ & @{thm (rhs) L.simps(6)}\\
+  \end{tabular}
+  \end{center}
+
+  \noindent
+  The nullable function
+
+  \begin{center}
+  \begin{tabular}{lcl}
+  @{thm (lhs) nullable.simps(1)} & $\dn$ & @{thm (rhs) nullable.simps(1)}\\
+  @{thm (lhs) nullable.simps(2)} & $\dn$ & @{thm (rhs) nullable.simps(2)}\\
+  @{thm (lhs) nullable.simps(3)} & $\dn$ & @{thm (rhs) nullable.simps(3)}\\
+  @{thm (lhs) nullable.simps(4)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) nullable.simps(4)[of "r\<^sub>1" "r\<^sub>2"]}\\
+  @{thm (lhs) nullable.simps(5)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) nullable.simps(5)[of "r\<^sub>1" "r\<^sub>2"]}\\
+  @{thm (lhs) nullable.simps(6)} & $\dn$ & @{thm (rhs) nullable.simps(6)}\\
+  \end{tabular}
+  \end{center}
+
+  \noindent
+  The derivative function for characters and strings
+
+  \begin{center}
+  \begin{tabular}{lcp{7.5cm}}
+  @{thm (lhs) der.simps(1)} & $\dn$ & @{thm (rhs) der.simps(1)}\\
+  @{thm (lhs) der.simps(2)} & $\dn$ & @{thm (rhs) der.simps(2)}\\
+  @{thm (lhs) der.simps(3)} & $\dn$ & @{thm (rhs) der.simps(3)}\\
+  @{thm (lhs) der.simps(4)[of c "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) der.simps(4)[of c "r\<^sub>1" "r\<^sub>2"]}\\
+  @{thm (lhs) der.simps(5)[of c "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) der.simps(5)[of c "r\<^sub>1" "r\<^sub>2"]}\\
+  @{thm (lhs) der.simps(6)} & $\dn$ & @{thm (rhs) der.simps(6)}\medskip\\
+
+  @{thm (lhs) ders.simps(1)} & $\dn$ & @{thm (rhs) ders.simps(1)}\\
+  @{thm (lhs) ders.simps(2)} & $\dn$ & @{thm (rhs) ders.simps(2)}\\
+  \end{tabular}
+  \end{center}
+
+  \noindent
+  The @{const flat} function for values
+
+  \begin{center}
+  \begin{tabular}{lcl}
+  @{thm (lhs) flat.simps(1)} & $\dn$ & @{thm (rhs) flat.simps(1)}\\
+  @{thm (lhs) flat.simps(2)} & $\dn$ & @{thm (rhs) flat.simps(2)}\\
+  @{thm (lhs) flat.simps(3)} & $\dn$ & @{thm (rhs) flat.simps(3)}\\
+  @{thm (lhs) flat.simps(4)} & $\dn$ & @{thm (rhs) flat.simps(4)}\\
+  @{thm (lhs) flat.simps(5)[of "v\<^sub>1" "v\<^sub>2"]} & $\dn$ & @{thm (rhs) flat.simps(5)[of "v\<^sub>1" "v\<^sub>2"]}\\
+  @{thm (lhs) flat.simps(6)} & $\dn$ & @{thm (rhs) flat.simps(6)}\\
+  @{thm (lhs) flat.simps(7)} & $\dn$ & @{thm (rhs) flat.simps(7)}\\
+  \end{tabular}
+  \end{center}
+
+  \noindent
+  The @{const mkeps} function
+
+  \begin{center}
+  \begin{tabular}{lcl}
+  @{thm (lhs) mkeps.simps(1)} & $\dn$ & @{thm (rhs) mkeps.simps(1)}\\
+  @{thm (lhs) mkeps.simps(2)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) mkeps.simps(2)[of "r\<^sub>1" "r\<^sub>2"]}\\
+  @{thm (lhs) mkeps.simps(3)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) mkeps.simps(3)[of "r\<^sub>1" "r\<^sub>2"]}\\
+  @{thm (lhs) mkeps.simps(4)} & $\dn$ & @{thm (rhs) mkeps.simps(4)}\\
+  \end{tabular}
+  \end{center}
+
+  \noindent
+  The @{text inj} function
+
+  \begin{center}
+  \begin{tabular}{lcl}
+  @{thm (lhs) injval.simps(1)} & $\dn$ & @{thm (rhs) injval.simps(1)}\\
+  @{thm (lhs) injval.simps(2)} & $\dn$ & @{thm (rhs) injval.simps(2)}\\
+  @{thm (lhs) injval.simps(3)} & $\dn$ & @{thm (rhs) injval.simps(3)}\\
+  @{thm (lhs) injval.simps(4)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1"]} & $\dn$ & 
+      @{thm (rhs) injval.simps(4)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1"]}\\
+  @{thm (lhs) injval.simps(5)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]} & $\dn$ & 
+      @{thm (rhs) injval.simps(5)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]}\\
+  @{thm (lhs) injval.simps(6)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]} & $\dn$ 
+      & @{thm (rhs) injval.simps(6)[of "r\<^sub>1" "c" "v\<^sub>1" "v\<^sub>2"]}\\
+  @{thm (lhs) injval.simps(7)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]} & $\dn$ 
+      & @{thm (rhs) injval.simps(7)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]}\\
+  @{thm (lhs) injval.simps(8)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]} & $\dn$ 
+      & @{thm (rhs) injval.simps(8)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]}\\
+  @{thm (lhs) injval.simps(9)[of "r" "c" "v" "vs"]} & $\dn$ 
+      & @{thm (rhs) injval.simps(9)[of "r" "c" "v" "vs"]}\\
+  \end{tabular}
+  \end{center}
+
+  \noindent
+  The inhabitation relation:
+
+  \begin{center}
+  \begin{tabular}{c}
+  @{thm[mode=Rule] Prf.intros(1)[of "v\<^sub>1" "r\<^sub>1" "v\<^sub>2" "r\<^sub>2"]}\medskip\\ 
+  @{thm[mode=Rule] Prf.intros(2)[of "v\<^sub>1" "r\<^sub>1" "r\<^sub>2"]} \qquad 
+  @{thm[mode=Rule] Prf.intros(3)[of "v\<^sub>2" "r\<^sub>1" "r\<^sub>2"]}\medskip\\
+  @{thm[mode=Axiom] Prf.intros(4)} \qquad 
+  @{thm[mode=Axiom] Prf.intros(5)[of "c"]}\medskip\\
+  @{thm[mode=Axiom] Prf.intros(6)[of "r"]} \qquad 
+  @{thm[mode=Rule] Prf.intros(7)[of "v" "r" "vs"]}\medskip\\
+  \end{tabular}
+  \end{center}
+
+  \noindent
+  We have also introduced a slightly restricted version of this relation
+  where the last rule is restricted so that @{term "flat v \<noteq> []"}.
+  This relation for \emph{non-problematic} is written @{term "\<Turnstile> v : r"}.
+  \bigskip
+
+
+  \noindent
+  Our Posix relation @{term "s \<in> r \<rightarrow> v"}
+
+  \begin{center}
+  \begin{tabular}{c}
+  @{thm[mode=Axiom] PMatch.intros(1)} \qquad
+  @{thm[mode=Axiom] PMatch.intros(2)}\medskip\\
+  @{thm[mode=Rule] PMatch.intros(3)[of "s" "r\<^sub>1" "v" "r\<^sub>2"]}\qquad
+  @{thm[mode=Rule] PMatch.intros(4)[of "s" "r\<^sub>2" "v" "r\<^sub>1"]}\medskip\\
+  \multicolumn{1}{p{5cm}}{@{thm[mode=Rule] PMatch.intros(5)[of "s\<^sub>1" "r\<^sub>1" "v\<^sub>1" "s\<^sub>2" "r\<^sub>2" "v\<^sub>2"]}}\medskip\\
+  @{thm[mode=Rule] PMatch.intros(6)[of "s\<^sub>1" "r" "v" "s\<^sub>2" "vs"]} \qquad
+  @{thm[mode=Axiom] PMatch.intros(7)}\medskip\\
+  \end{tabular}
+  \end{center}
+
+  \noindent
+  Our version of Sulzmann's ordering relation
+
+  \begin{center}
+  \begin{tabular}{c}
+  @{thm[mode=Rule] ValOrd.intros(2)[of "v\<^sub>1" "r\<^sub>1" "v\<^sub>1'" "v\<^sub>2" "r\<^sub>2" "v\<^sub>2'"]} \qquad
+  @{thm[mode=Rule] ValOrd.intros(1)[of "v\<^sub>2" "r\<^sub>2" "v\<^sub>2'" "v\<^sub>1" "r\<^sub>1"]}\medskip\\
+  @{thm[mode=Rule] ValOrd.intros(3)[of "v\<^sub>1" "v\<^sub>2" "r\<^sub>1" "r\<^sub>2"]} \qquad
+  @{thm[mode=Rule] ValOrd.intros(4)[of "v\<^sub>2" "v\<^sub>1" "r\<^sub>1" "r\<^sub>2"]}\medskip\\ 
+  @{thm[mode=Rule] ValOrd.intros(5)[of "v\<^sub>2" "r\<^sub>2" "v\<^sub>2'" "r\<^sub>1"]} \qquad
+  @{thm[mode=Rule] ValOrd.intros(6)[of "v\<^sub>1" "r\<^sub>1" "v\<^sub>1'"  "r\<^sub>2"]} \medskip\\
+  @{thm[mode=Axiom] ValOrd.intros(7)}\qquad
+  @{thm[mode=Axiom] ValOrd.intros(8)[of "c"]}\medskip\\
+  @{thm[mode=Rule] ValOrd.intros(9)[of "v" "vs" "r"]}\qquad
+  @{thm[mode=Rule] ValOrd.intros(10)[of "v" "vs" "r"]}\medskip\\
+  @{thm[mode=Rule] ValOrd.intros(11)[of "v\<^sub>1" "r" "v\<^sub>2" "vs\<^sub>1" "vs\<^sub>2"]}\medskip\\
+  @{thm[mode=Rule] ValOrd.intros(12)[of "vs\<^sub>1" "r" "vs\<^sub>2" "v"]}\qquad
+  @{thm[mode=Axiom] ValOrd.intros(13)[of "r"]}\medskip\\
+  \end{tabular}
+  \end{center}
+*} 
+
+text {* 
+  \noindent
+  Some lemmas
+  
+
+  @{thm[mode=IfThen] mkeps_nullable}
+
+  @{thm[mode=IfThen] mkeps_flat}
+
+  \ldots
+*}
+
 
 text {*
   %\noindent
diff -r c3d7125f9950 -r 38696f516c6b thys/ReStar.thy
--- a/thys/ReStar.thy	Fri Feb 05 10:16:41 2016 +0000
+++ b/thys/ReStar.thy	Sun Feb 07 23:44:34 2016 +0000
@@ -146,7 +146,7 @@
 | "nullable (CHAR c) = False"
 | "nullable (ALT r1 r2) = (nullable r1 \<or> nullable r2)"
 | "nullable (SEQ r1 r2) = (nullable r1 \<and> nullable r2)"
-| "nullable (STAR r1) = True"
+| "nullable (STAR r) = True"
 
 lemma nullable_correctness:
   shows "nullable r  \<longleftrightarrow> [] \<in> (L r)"
@@ -162,7 +162,7 @@
 | Seq val val
 | Right val
 | Left val
-| Star "val list"
+| Stars "val list"
 
 section {* The string behind a value *}
 
@@ -174,11 +174,11 @@
 | "flat (Left v) = flat v"
 | "flat (Right v) = flat v"
 | "flat (Seq v1 v2) = (flat v1) @ (flat v2)"
-| "flat (Star []) = []"
-| "flat (Star (v#vs)) = (flat v) @ (flat (Star vs))" 
+| "flat (Stars []) = []"
+| "flat (Stars (v#vs)) = (flat v) @ (flat (Stars vs))" 
 
 lemma [simp]:
- "flat (Star vs) = concat (map flat vs)"
+ "flat (Stars vs) = concat (map flat vs)"
 apply(induct vs)
 apply(auto)
 done
@@ -193,8 +193,8 @@
 | "\<Turnstile> v2 : r2 \<Longrightarrow> \<Turnstile> Right v2 : ALT r1 r2"
 | "\<Turnstile> Void : EMPTY"
 | "\<Turnstile> Char c : CHAR c"
-| "\<Turnstile> Star [] : STAR r"
-| "\<lbrakk>\<Turnstile> v : r; \<Turnstile> Star vs : STAR r; flat v \<noteq> []\<rbrakk> \<Longrightarrow> \<Turnstile> Star (v # vs) : STAR r"
+| "\<Turnstile> Stars [] : STAR r"
+| "\<lbrakk>\<Turnstile> v : r; \<Turnstile> Stars vs : STAR r; flat v \<noteq> []\<rbrakk> \<Longrightarrow> \<Turnstile> Stars (v # vs) : STAR r"
 
 inductive 
   Prf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<turnstile> _ : _" [100, 100] 100)
@@ -204,8 +204,8 @@
 | "\<turnstile> v2 : r2 \<Longrightarrow> \<turnstile> Right v2 : ALT r1 r2"
 | "\<turnstile> Void : EMPTY"
 | "\<turnstile> Char c : CHAR c"
-| "\<turnstile> Star [] : STAR r"
-| "\<lbrakk>\<turnstile> v : r; \<turnstile> Star vs : STAR r\<rbrakk> \<Longrightarrow> \<turnstile> Star (v # vs) : STAR r"
+| "\<turnstile> Stars [] : STAR r"
+| "\<lbrakk>\<turnstile> v : r; \<turnstile> Stars vs : STAR r\<rbrakk> \<Longrightarrow> \<turnstile> Stars (v # vs) : STAR r"
 
 lemma NPrf_imp_Prf:
   assumes "\<Turnstile> v : r" 
@@ -217,7 +217,7 @@
 
 lemma NPrf_Prf_val:
   shows "\<turnstile> v : r \<Longrightarrow> \<exists>v'. flat v' = flat v \<and> \<Turnstile> v' : r"
-  and   "\<turnstile> Star vs : r \<Longrightarrow> \<exists>vs'. flat (Star vs') = flat (Star vs) \<and> \<Turnstile> Star vs' : r"
+  and   "\<turnstile> Stars vs : r \<Longrightarrow> \<exists>vs'. flat (Stars vs') = flat (Stars vs) \<and> \<Turnstile> Stars vs' : r"
 using assms
 apply(induct v and vs arbitrary: r and r rule: val.inducts)
 apply(auto)[1]
@@ -262,7 +262,7 @@
 apply(drule_tac x="r" in meta_spec)
 apply(simp)
 apply(auto)[1]
-apply(rule_tac x="Star vs'" in exI)
+apply(rule_tac x="Stars vs'" in exI)
 apply(simp)
 apply(rule_tac x="[]" in exI)
 apply(simp)
@@ -313,9 +313,9 @@
 using assms
 by (metis NPrf_imp_Prf Prf_flat_L)
 
-lemma Prf_Star:
+lemma Prf_Stars:
   assumes "\<forall>v \<in> set vs. \<turnstile> v : r"
-  shows "\<turnstile> Star vs : STAR r"
+  shows "\<turnstile> Stars vs : STAR r"
 using assms
 apply(induct vs)
 apply (metis Prf.intros(6))
@@ -364,9 +364,9 @@
 apply(auto)
 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="Star vs" in exI)
+apply(rule_tac x="Stars vs" in exI)
 apply(simp)
-apply(rule Prf_Star)
+apply(rule Prf_Stars)
 apply(simp)
 apply(drule Star_string)
 apply(auto)
@@ -390,7 +390,7 @@
 apply(rule_tac x="Suc x" in exI)
 apply(auto simp add: Sequ_def)
 apply(rule_tac x="flat v" in exI)
-apply(rule_tac x="flat (Star vs)" in exI)
+apply(rule_tac x="flat (Stars vs)" in exI)
 apply(auto)
 by (metis Prf_flat_L)
 
@@ -502,7 +502,7 @@
   "NValues r s \<equiv> {v. \<Turnstile> v : r \<and> flat v \<sqsubseteq> s}"
 
 lemma NValues_STAR_Nil:
-  "NValues (STAR r) [] = {Star []}"
+  "NValues (STAR r) [] = {Stars []}"
 apply(auto simp add: NValues_def prefix_def)
 apply(erule NPrf.cases)
 apply(auto)
@@ -541,7 +541,7 @@
   "Values (ALT r1 r2) s = {Left v | v. v \<in> Values r1 s} \<union> {Right v | v. v \<in> Values r2 s}"
   "Values (SEQ r1 r2) s = {Seq v1 v2 | v1 v2. v1 \<in> Values r1 s \<and> v2 \<in> Values r2 (rest v1 s)}"
   "Values (STAR r) s = 
-      {Star []} \<union> {Star (v # vs) | v vs. v \<in> Values r s \<and> Star vs \<in> Values (STAR r) (rest v s)}"
+      {Stars []} \<union> {Stars (v # vs) | v vs. v \<in> Values r s \<and> Stars vs \<in> Values (STAR r) (rest v s)}"
 unfolding Values_def
 apply(auto)
 (*NULL*)
@@ -590,7 +590,7 @@
   "NValues (ALT r1 r2) s = {Left v | v. v \<in> NValues r1 s} \<union> {Right v | v. v \<in> NValues r2 s}"
   "NValues (SEQ r1 r2) s = {Seq v1 v2 | v1 v2. v1 \<in> NValues r1 s \<and> v2 \<in> NValues r2 (rest v1 s)}"
   "NValues (STAR r) s = 
-  {Star []} \<union> {Star (v # vs) | v vs. v \<in> NValues r s \<and> flat v \<noteq> [] \<and>  Star vs \<in> NValues (STAR r) (rest v s)}"
+  {Stars []} \<union> {Stars (v # vs) | v vs. v \<in> NValues r s \<and> flat v \<noteq> [] \<and>  Stars vs \<in> NValues (STAR r) (rest v s)}"
 unfolding NValues_def
 apply(auto)
 (*NULL*)
@@ -663,15 +663,15 @@
 apply(clarify)
 apply(subst NValues_recs)
 apply(simp)
-apply(rule_tac f="\<lambda>(v, vs). Star (v # vs)" and 
-               A="{(v, vs) | v vs. v \<in> NValues rexp b \<and> (flat v \<noteq> [] \<and> Star vs \<in> NValues (STAR rexp) (rest v b))}" in finite_surj)
+apply(rule_tac f="\<lambda>(v, vs). Stars (v # vs)" and 
+               A="{(v, vs) | v vs. v \<in> NValues rexp b \<and> (flat v \<noteq> [] \<and> Stars vs \<in> NValues (STAR rexp) (rest v b))}" in finite_surj)
 prefer 2
 apply(auto)[1]
 apply(auto)
 apply(case_tac b)
 apply(simp)
 defer
-apply(rule_tac B="\<Union>sp \<in> SSuffixes b. {(v, vs) | v vs. v \<in> NValues rexp b \<and> Star vs \<in> NValues (STAR rexp) sp}" in finite_subset)
+apply(rule_tac B="\<Union>sp \<in> SSuffixes b. {(v, vs) | v vs. v \<in> NValues rexp b \<and> Stars vs \<in> NValues (STAR rexp) sp}" in finite_subset)
 apply(auto)[1]
 apply(rule_tac x="rest aa (a # list)" in bexI)
 apply(simp)
@@ -696,7 +696,7 @@
 apply(simp)
 apply(rule finite_cartesian_product)
 apply(simp)
-apply(rule_tac f="Star" in finite_imageD)
+apply(rule_tac f="Stars" in finite_imageD)
 prefer 2
 apply(auto simp add: inj_on_def)[1]
 apply (metis finite_subset image_Collect_subsetI)
@@ -723,7 +723,7 @@
   "mkeps(EMPTY) = Void"
 | "mkeps(SEQ r1 r2) = Seq (mkeps r1) (mkeps r2)"
 | "mkeps(ALT r1 r2) = (if nullable(r1) then Left (mkeps r1) else Right (mkeps r2))"
-| "mkeps(STAR r) = Star []"
+| "mkeps(STAR r) = Stars []"
 
 section {* Derivatives *}
 
@@ -756,11 +756,10 @@
 | "injval (CHAR d) c (Char c') = Seq (Char d) (Char c')"
 | "injval (ALT r1 r2) c (Left v1) = Left(injval r1 c v1)"
 | "injval (ALT r1 r2) c (Right v2) = Right(injval r2 c v2)"
-| "injval (SEQ r1 r2) c (Char c') = Seq (Char c) (Char c')"
 | "injval (SEQ r1 r2) c (Seq v1 v2) = Seq (injval r1 c v1) v2"
 | "injval (SEQ r1 r2) c (Left (Seq v1 v2)) = Seq (injval r1 c v1) v2"
 | "injval (SEQ r1 r2) c (Right v2) = Seq (mkeps r1) (injval r2 c v2)"
-| "injval (STAR r) c (Seq v (Star vs)) = Star ((injval r c v) # vs)" 
+| "injval (STAR r) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)" 
 
 fun 
   lex :: "rexp \<Rightarrow> string \<Rightarrow> val option"
@@ -788,7 +787,7 @@
      (if flat v1 = [] then Right(projval r2 c v2) 
       else if nullable r1 then Left (Seq (projval r1 c v1) v2)
                           else Seq (projval r1 c v1) v2)"
-| "projval (STAR r) c (Star (v # vs)) = Seq (projval r c v) (Star vs)"
+| "projval (STAR r) c (Stars (v # vs)) = Seq (projval r c v) (Stars vs)"
 
 
 
@@ -888,7 +887,7 @@
 apply(rule NPrf.intros)
 apply (metis Cons_eq_append_conv)
 apply(simp)
-(* Star case *)
+(* Stars case *)
 apply(rule NPrf.intros)
 apply (metis Cons_eq_append_conv)
 apply(auto)
@@ -977,11 +976,11 @@
 | "s \<in> r1 \<rightarrow> v \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Left v)"
 | "\<lbrakk>s \<in> r2 \<rightarrow> v; s \<notin> L(r1)\<rbrakk> \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Right v)"
 | "\<lbrakk>s1 \<in> r1 \<rightarrow> v1; s2 \<in> r2 \<rightarrow> v2;
-    \<not>(\<exists>s3 s4. s3 \<noteq> [] \<and> s3 @ s4 = s2 \<and> (s1 @ s3) \<in> L r1 \<and> s4 \<in> L r2)\<rbrakk> \<Longrightarrow> 
+    \<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 r1 \<and> s\<^sub>4 \<in> L r2)\<rbrakk> \<Longrightarrow> 
     (s1 @ s2) \<in> (SEQ r1 r2) \<rightarrow> (Seq v1 v2)"
-| "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> STAR r \<rightarrow> Star vs; flat v \<noteq> []\<rbrakk>
-    \<Longrightarrow> (s1 @ s2) \<in> STAR r \<rightarrow> Star (v # vs)"
-| "[] \<in> STAR r \<rightarrow> Star []"
+| "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> STAR r \<rightarrow> Stars vs; flat v \<noteq> []\<rbrakk>
+    \<Longrightarrow> (s1 @ s2) \<in> STAR r \<rightarrow> Stars (v # vs)"
+| "[] \<in> STAR r \<rightarrow> Stars []"
 
 lemma PMatch_mkeps:
   assumes "nullable r"
@@ -1093,7 +1092,7 @@
 apply(auto)[1]
 apply(frule_tac c="c" in v3_proj)
 apply metis
-apply(drule_tac x="s3" in spec)
+apply(drule_tac x="s\<^sub>3" in spec)
 apply(drule mp)
 apply(rule_tac x="projval r1 c v" in exI)
 apply(rule conjI)
@@ -1116,7 +1115,7 @@
 apply(auto)[1]
 apply(frule_tac c="c" in v3_proj)
 apply metis
-apply(drule_tac x="s3" in spec)
+apply(drule_tac x="s\<^sub>3" in spec)
 apply(drule mp)
 apply (metis NPrf_imp_Prf v4_proj2)
 apply(simp)
@@ -1144,7 +1143,7 @@
 apply(rule v3_proj)
 apply(simp)
 apply (metis Cons_eq_append_conv)
-(* Star case *)
+(* Stars case *)
 apply(erule PMatch.cases)
 apply(simp_all)[7]
 apply(clarify)
@@ -1275,11 +1274,11 @@
 | "v1 \<succ>r1 v1' \<Longrightarrow> (Left v1) \<succ>(ALT r1 r2) (Left v1')"
 | "Void \<succ>EMPTY Void"
 | "(Char c) \<succ>(CHAR c) (Char c)"
-| "flat (Star (v # vs)) = [] \<Longrightarrow> (Star []) \<succ>(STAR r) (Star (v # vs))"
-| "flat (Star (v # vs)) \<noteq> [] \<Longrightarrow> (Star (v # vs)) \<succ>(STAR r) (Star [])"
-| "v1 \<succ>r v2 \<Longrightarrow> (Star (v1 # vs1)) \<succ>(STAR r) (Star (v2 # vs2))"
-| "(Star vs1) \<succ>(STAR r) (Star vs2) \<Longrightarrow> (Star (v # vs1)) \<succ>(STAR r) (Star (v # vs2))"
-| "(Star []) \<succ>(STAR r) (Star [])"
+| "flat (Stars (v # vs)) = [] \<Longrightarrow> (Stars []) \<succ>(STAR r) (Stars (v # vs))"
+| "flat (Stars (v # vs)) \<noteq> [] \<Longrightarrow> (Stars (v # vs)) \<succ>(STAR r) (Stars [])"
+| "v1 \<succ>r v2 \<Longrightarrow> (Stars (v1 # vs1)) \<succ>(STAR r) (Stars (v2 # vs2))"
+| "(Stars vs1) \<succ>(STAR r) (Stars vs2) \<Longrightarrow> (Stars (v # vs1)) \<succ>(STAR r) (Stars (v # vs2))"
+| "(Stars []) \<succ>(STAR r) (Stars [])"
 
 (*
 
@@ -1313,7 +1312,7 @@
 apply (metis PMatch1(2) ValOrd.intros(3) length_sprefix less_imp_le_nat order_refl sprefix_def)
 apply(clarify)
 apply (metis ValOrd.intros(5))
-(* Star case *)
+(* Stars case *)
 apply(erule Prf.cases)
 apply(simp_all)[7]
 apply(erule PMatch.cases)
@@ -2915,4 +2914,5 @@
 oops
 *)
 
+
 end
\ No newline at end of file
diff -r c3d7125f9950 -r 38696f516c6b thys/paper.pdf
Binary file thys/paper.pdf has changed