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