diff -r 37e3f1174974 -r 5b01f7c233f8 thys/ReStar.thy
--- a/thys/ReStar.thy	Mon Feb 01 22:30:27 2016 +0000
+++ b/thys/ReStar.thy	Tue Feb 02 02:27:16 2016 +0000
@@ -115,21 +115,6 @@
 by (induct x\<equiv>"c # x" rule: Star.induct) 
    (auto simp add: append_eq_Cons_conv)
 
-(*
-lemma star_induct[consumes 1, case_names Nil append, induct set: Star]:
-assumes "w \<in> A\<star>"
-  and "P []"
-  and step: "\<And>u v. u \<in> A \<Longrightarrow> v \<in> A\<star> \<Longrightarrow> P v \<Longrightarrow> P (u @ v)"
-shows "P w"
-proof -
-  { fix n have "w \<in> A \<up> n \<Longrightarrow> P w"
-      apply(induct n arbitrary: w) 
-      apply(auto intro: `P []` step star2 simp add: Sequ_def)
-      done
-  }
-  with `w \<in> A\<star>` show "P w" by (auto simp: star3)
-qed
-*)
 
 section {* Regular Expressions *}
 
@@ -459,12 +444,24 @@
 definition Suffixes :: "string \<Rightarrow> string set" where
   "Suffixes s \<equiv> rev ` (Prefixes (rev s))"
 
+definition SPrefixes :: "string \<Rightarrow> string set" where
+  "SPrefixes s \<equiv> {sp. sp \<sqsubset> s}"
+
+definition SSuffixes :: "string \<Rightarrow> string set" where
+  "SSuffixes s \<equiv> rev ` (SPrefixes (rev s))"
+
 lemma Suffixes_in: 
   "\<exists>s1. s1 @ s2 = s3 \<Longrightarrow> s2 \<in> Suffixes s3"
 unfolding Suffixes_def Prefixes_def prefix_def image_def
 apply(auto)
 by (metis rev_rev_ident)
 
+lemma SSuffixes_in: 
+  "\<exists>s1. s1 \<noteq> [] \<and> s1 @ s2 = s3 \<Longrightarrow> s2 \<in> SSuffixes s3"
+unfolding SSuffixes_def Suffixes_def SPrefixes_def Prefixes_def sprefix_def prefix_def image_def
+apply(auto)
+by (metis append_self_conv rev.simps(1) rev_rev_ident)
+
 lemma Prefixes_Cons:
   "Prefixes (c # s) = {[]} \<union> {c # sp | sp. sp \<in> Prefixes s}"
 unfolding Prefixes_def prefix_def
@@ -501,14 +498,41 @@
 definition Values :: "rexp \<Rightarrow> string \<Rightarrow> val set" where
   "Values r s \<equiv> {v. \<turnstile> v : r \<and> flat v \<sqsubseteq> s}"
 
+definition NValues :: "rexp \<Rightarrow> string \<Rightarrow> val set" where
+  "NValues r s \<equiv> {v. \<Turnstile> v : r \<and> flat v \<sqsubseteq> s}"
+
+lemma NValues_STAR_Nil:
+  "NValues (STAR r) [] = {Star []}"
+apply(auto simp add: NValues_def prefix_def)
+apply(erule NPrf.cases)
+apply(auto)
+by (metis NPrf.intros(6))
+
+
 definition rest :: "val \<Rightarrow> string \<Rightarrow> string" where
   "rest v s \<equiv> drop (length (flat v)) s"
 
+lemma rest_Nil:
+  "rest v [] = []"
+apply(simp add: rest_def)
+done
+
 lemma rest_Suffixes:
   "rest v s \<in> Suffixes s"
 unfolding rest_def
 by (metis Suffixes_in append_take_drop_id)
 
+lemma rest_SSuffixes:
+  assumes "flat v \<noteq> []" "s \<noteq> []"
+  shows "rest v s \<in> SSuffixes s"
+using assms
+unfolding rest_def
+thm SSuffixes_in
+apply(rule_tac SSuffixes_in)
+apply(rule_tac x="take (length (flat v)) s" in exI)
+apply(simp add: sprefix_def)
+done
+
 
 lemma Values_recs:
   "Values (NULL) s = {}"
@@ -516,6 +540,8 @@
   "Values (CHAR c) s = (if [c] \<sqsubseteq> s then {Char c} else {})" 
   "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)}"
 unfolding Values_def
 apply(auto)
 (*NULL*)
@@ -543,26 +569,151 @@
 apply (simp add: append_eq_conv_conj prefix_def rest_def)
 apply (metis Prf.intros(1))
 apply (simp add: append_eq_conv_conj prefix_def rest_def)
-done
+(*STAR*)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(rule conjI)
+apply(simp add: prefix_def)
+apply(auto)[1]
+apply(simp add: prefix_def)
+apply(auto)[1]
+apply (metis append_eq_conv_conj rest_def)
+apply (metis Prf.intros(6))
+apply (metis append_Nil prefix_def)
+apply (metis Prf.intros(7))
+by (metis append_eq_conv_conj prefix_append prefix_def rest_def)
 
-(* This lemma needs to be adapted to Star
-lemma Values_finite:
-  "finite (Values r s)"
-apply(induct r arbitrary: s)
-apply(simp_all add: Values_recs)
-thm finite_surj
+lemma NValues_recs:
+  "NValues (NULL) s = {}"
+  "NValues (EMPTY) s = {Void}"
+  "NValues (CHAR c) s = (if [c] \<sqsubseteq> s then {Char c} else {})" 
+  "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)}"
+unfolding NValues_def
+apply(auto)
+(*NULL*)
+apply(erule NPrf.cases)
+apply(simp_all)[7]
+(*EMPTY*)
+apply(erule NPrf.cases)
+apply(simp_all)[7]
+apply(rule NPrf.intros)
+apply (metis append_Nil prefix_def)
+(*CHAR*)
+apply(erule NPrf.cases)
+apply(simp_all)[7]
+apply(rule NPrf.intros)
+apply(erule NPrf.cases)
+apply(simp_all)[7]
+(*ALT*)
+apply(erule NPrf.cases)
+apply(simp_all)[7]
+apply (metis NPrf.intros(2))
+apply (metis NPrf.intros(3))
+(*SEQ*)
+apply(erule NPrf.cases)
+apply(simp_all)[7]
+apply (simp add: append_eq_conv_conj prefix_def rest_def)
+apply (metis NPrf.intros(1))
+apply (simp add: append_eq_conv_conj prefix_def rest_def)
+(*STAR*)
+apply(erule NPrf.cases)
+apply(simp_all)
+apply(rule conjI)
+apply(simp add: prefix_def)
+apply(auto)[1]
+apply(simp add: prefix_def)
+apply(auto)[1]
+apply (metis append_eq_conv_conj rest_def)
+apply (metis NPrf.intros(6))
+apply (metis append_Nil prefix_def)
+apply (metis NPrf.intros(7))
+by (metis append_eq_conv_conj prefix_append prefix_def rest_def)
+
+
+lemma finite_image_set2:
+  "finite {x. P x} \<Longrightarrow> finite {y. Q y} \<Longrightarrow> finite {(x, y) | x y. P x \<and> Q y}"
+  by (rule finite_subset [where B = "\<Union>x \<in> {x. P x}. \<Union>y \<in> {y. Q y}. {(x, y)}"]) auto
+
+
+lemma NValues_finite_aux:
+  "(\<lambda>(r, s). finite (NValues r s)) (r, s)"
+apply(rule wf_induct[of "measure size <*lex*> measure length",where P="\<lambda>(r, s). finite (NValues r s)"])
+apply (metis wf_lex_prod wf_measure)
+apply(auto)
+apply(case_tac a)
+apply(simp_all)
+apply(simp add: NValues_recs)
+apply(simp add: NValues_recs)
+apply(simp add: NValues_recs)
+apply(simp add: NValues_recs)
 apply(rule_tac f="\<lambda>(x, y). Seq x y" and 
-               A="{(v1, v2) | v1 v2. v1 \<in> Values r1 s \<and> v2 \<in> Values r2 (rest v1 s)}" in finite_surj)
+               A="{(v1, v2) | v1 v2. v1 \<in> NValues rexp1 b \<and> v2 \<in> NValues rexp2 (rest v1 b)}" in finite_surj)
 prefer 2
 apply(auto)[1]
-apply(rule_tac B="\<Union>sp \<in> Suffixes s. {(v1, v2). v1 \<in> Values r1 s \<and> v2 \<in> Values r2 sp}" in finite_subset)
+apply(rule_tac B="\<Union>sp \<in> Suffixes b. {(v1, v2). v1 \<in> NValues rexp1 b \<and> v2 \<in> NValues rexp2 sp}" in finite_subset)
 apply(auto)[1]
 apply (metis rest_Suffixes)
 apply(rule finite_UN_I)
 apply(rule finite_Suffixes)
 apply(simp)
+apply(simp add: NValues_recs)
+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)
+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(auto)[1]
+apply(rule_tac x="rest aa (a # list)" in bexI)
+apply(simp)
+apply (rule rest_SSuffixes)
+apply(simp)
+apply(simp)
+apply(rule finite_UN_I)
+defer
+apply(frule_tac x="rexp" in spec)
+apply(drule_tac x="b" in spec)
+apply(drule conjunct1)
+apply(drule mp)
+apply(simp)
+apply(drule_tac x="STAR rexp" in spec)
+apply(drule_tac x="sp" in spec)
+apply(drule conjunct2)
+apply(drule mp)
+apply(simp)
+apply(simp add: prefix_def SPrefixes_def SSuffixes_def)
+apply(auto)[1]
+apply (metis length_Cons length_rev length_sprefix rev.simps(2))
+apply(simp)
+apply(rule finite_cartesian_product)
+apply(simp)
+apply(rule_tac f="Star" in finite_imageD)
+prefer 2
+apply(auto simp add: inj_on_def)[1]
+apply (metis finite_subset image_Collect_subsetI)
+apply(simp add: rest_Nil)
+apply(simp add: NValues_STAR_Nil)
+apply(rule_tac B="{(v, vs). v \<in> NValues rexp [] \<and> vs = []}" in finite_subset)
+apply(auto)[1]
+apply(simp)
+apply(rule_tac B="Suffixes b" in finite_subset)
+apply(auto simp add: SSuffixes_def Suffixes_def Prefixes_def SPrefixes_def sprefix_def)[1]
+by (metis finite_Suffixes)
+
+lemma NValues_finite:
+  "finite (NValues r s)"
+using NValues_finite_aux
+apply(simp)
 done
-*)
 
 section {* Sulzmann functions *}