diff -r 32b222d77fa0 -r 6746f5e1f1f8 thys/Spec.thy
--- a/thys/Spec.thy	Fri Aug 11 20:29:01 2017 +0100
+++ b/thys/Spec.thy	Fri Aug 18 14:51:29 2017 +0100
@@ -176,35 +176,6 @@
 
 
 
-section {* Lemmas about ders *}
-
-(* not really needed *)
-
-lemma ders_ZERO:
-  shows "ders s (ZERO) = ZERO"
-apply(induct s)
-apply(simp_all)
-done
-
-lemma ders_ONE:
-  shows "ders s (ONE) = (if s = [] then ONE else ZERO)"
-apply(induct s)
-apply(simp_all add: ders_ZERO)
-done
-
-lemma ders_CHAR:
-  shows "ders s (CHAR c) = 
-           (if s = [c] then ONE else 
-           (if s = [] then (CHAR c) else ZERO))"
-apply(induct s)
-apply(simp_all add: ders_ZERO ders_ONE)
-done
-
-lemma  ders_ALT:
-  shows "ders s (ALT r1 r2) = ALT (ders s r1) (ders s r2)"
-by (induct s arbitrary: r1 r2)(simp_all)
-
-
 section {* Values *}
 
 datatype val = 
@@ -236,109 +207,33 @@
  "flat (Stars vs) = flats vs"
 by (induct vs) (auto)
 
-
-section {* Relation between values and regular expressions *}
-
-inductive 
-  Prf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<turnstile> _ : _" [100, 100] 100)
-where
- "\<lbrakk>\<turnstile> v1 : r1; \<turnstile> v2 : r2\<rbrakk> \<Longrightarrow> \<turnstile> Seq v1 v2 : SEQ r1 r2"
-| "\<turnstile> v1 : r1 \<Longrightarrow> \<turnstile> Left v1 : ALT r1 r2"
-| "\<turnstile> v2 : r2 \<Longrightarrow> \<turnstile> Right v2 : ALT r1 r2"
-| "\<turnstile> Void : ONE"
-| "\<turnstile> Char c : CHAR c"
-| "\<forall>v \<in> set vs. \<turnstile> v : r \<Longrightarrow> \<turnstile> Stars vs : STAR r"
-
-inductive_cases Prf_elims:
-  "\<turnstile> v : ZERO"
-  "\<turnstile> v : SEQ r1 r2"
-  "\<turnstile> v : ALT r1 r2"
-  "\<turnstile> v : ONE"
-  "\<turnstile> v : CHAR c"
-  "\<turnstile> vs : STAR r"
-
 lemma Star_concat:
   assumes "\<forall>s \<in> set ss. s \<in> A"  
   shows "concat ss \<in> A\<star>"
 using assms by (induct ss) (auto)
 
-lemma Star_string:
+lemma Star_cstring:
   assumes "s \<in> A\<star>"
-  shows "\<exists>ss. concat ss = s \<and> (\<forall>s \<in> set ss. s \<in> A)"
+  shows "\<exists>ss. concat ss = s \<and> (\<forall>s \<in> set ss. s \<in> A \<and> s \<noteq> [])"
 using assms
 apply(induct rule: Star.induct)
-apply(auto)
+apply(auto)[1]
 apply(rule_tac x="[]" in exI)
 apply(simp)
+apply(erule exE)
+apply(clarify)
+apply(case_tac "s1 = []")
+apply(rule_tac x="ss" in exI)
+apply(simp)
 apply(rule_tac x="s1#ss" in exI)
 apply(simp)
 done
 
-lemma Star_val:
-  assumes "\<forall>s\<in>set ss. \<exists>v. s = flat v \<and> \<turnstile> v : r"
-  shows "\<exists>vs. flats vs = concat ss \<and> (\<forall>v\<in>set vs. \<turnstile> v : r)"
-using assms
-apply(induct ss)
-apply(auto)
-apply(rule_tac x="[]" in exI)
-apply(simp)
-apply(rule_tac x="v#vs" in exI)
-apply(simp)
-done
 
-lemma Prf_Stars_append:
-  assumes "\<turnstile> Stars vs1 : STAR r" "\<turnstile> Stars vs2 : STAR r"
-  shows "\<turnstile> Stars (vs1 @ vs2) : STAR r"
-using assms
-by (auto intro!: Prf.intros elim!: Prf_elims)
-
-lemma Prf_flat_L:
-  assumes "\<turnstile> v : r" 
-  shows "flat v \<in> L r"
-using assms
-by (induct v r rule: Prf.induct)
-   (auto simp add: Sequ_def Star_concat)
-
-
-lemma L_flat_Prf1:
-  assumes "\<turnstile> v : r" 
-  shows "flat v \<in> L r"
-using assms
-by (induct) (auto simp add: Sequ_def Star_concat)
-
-lemma L_flat_Prf2:
-  assumes "s \<in> L r" 
-  shows "\<exists>v. \<turnstile> v : r \<and> flat v = s"
-using assms
-proof(induct r arbitrary: s)
-  case (STAR r s)
-  have IH: "\<And>s. s \<in> L r \<Longrightarrow> \<exists>v. \<turnstile> v : r \<and> flat v = s" by fact
-  have "s \<in> L (STAR r)" by fact
-  then obtain ss where "concat ss = s" "\<forall>s \<in> set ss. s \<in> L r"
-  using Star_string by auto
-  then obtain vs where "flats vs = s" "\<forall>v\<in>set vs. \<turnstile> v : r"
-  using IH Star_val by blast
-  then show "\<exists>v. \<turnstile> v : STAR r \<and> flat v = s"
-  using Prf.intros(6) flat_Stars by blast
-next 
-  case (SEQ r1 r2 s)
-  then show "\<exists>v. \<turnstile> v : SEQ r1 r2 \<and> flat v = s"
-  unfolding Sequ_def L.simps by (fastforce intro: Prf.intros)
-next
-  case (ALT r1 r2 s)
-  then show "\<exists>v. \<turnstile> v : ALT r1 r2 \<and> flat v = s"
-  unfolding L.simps by (fastforce intro: Prf.intros)
-qed (auto intro: Prf.intros)
-
-lemma L_flat_Prf:
-  shows "L(r) = {flat v | v. \<turnstile> v : r}"
-using L_flat_Prf1 L_flat_Prf2 by blast
-
-
-section {* Canonical Values *}
+section {* Lexical Values *}
 
 inductive 
-  CPrf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<Turnstile> _ : _" [100, 100] 100)
+  Prf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<Turnstile> _ : _" [100, 100] 100)
 where
  "\<lbrakk>\<Turnstile> v1 : r1; \<Turnstile> v2 : r2\<rbrakk> \<Longrightarrow> \<Turnstile>  Seq v1 v2 : SEQ r1 r2"
 | "\<Turnstile> v1 : r1 \<Longrightarrow> \<Turnstile> Left v1 : ALT r1 r2"
@@ -347,34 +242,92 @@
 | "\<Turnstile> Char c : CHAR c"
 | "\<forall>v \<in> set vs. \<Turnstile> v : r \<and> flat v \<noteq> [] \<Longrightarrow> \<Turnstile> Stars vs : STAR r"
 
-lemma Prf_CPrf:
-  assumes "\<Turnstile> v : r"
-  shows "\<turnstile> v : r"
-using assms
-by (induct)(auto intro: Prf.intros)
+inductive_cases Prf_elims:
+  "\<Turnstile> v : ZERO"
+  "\<Turnstile> v : SEQ r1 r2"
+  "\<Turnstile> v : ALT r1 r2"
+  "\<Turnstile> v : ONE"
+  "\<Turnstile> v : CHAR c"
+  "\<Turnstile> vs : STAR r"
 
-lemma CPrf_Stars_appendE:
+lemma Prf_Stars_appendE:
   assumes "\<Turnstile> Stars (vs1 @ vs2) : STAR r"
   shows "\<Turnstile> Stars vs1 : STAR r \<and> \<Turnstile> Stars vs2 : STAR r" 
 using assms
-apply(erule_tac CPrf.cases)
-apply(auto intro: CPrf.intros)
+by (auto intro: Prf.intros elim!: Prf_elims)
+
+
+lemma Star_cval:
+  assumes "\<forall>s\<in>set ss. \<exists>v. s = flat v \<and> \<Turnstile> v : r"
+  shows "\<exists>vs. flats vs = concat ss \<and> (\<forall>v\<in>set vs. \<Turnstile> v : r \<and> flat v \<noteq> [])"
+using assms
+apply(induct ss)
+apply(auto)
+apply(rule_tac x="[]" in exI)
+apply(simp)
+apply(case_tac "flat v = []")
+apply(rule_tac x="vs" in exI)
+apply(simp)
+apply(rule_tac x="v#vs" in exI)
+apply(simp)
 done
 
 
-section {* Sets of Lexical and Canonical Values *}
+lemma L_flat_Prf1:
+  assumes "\<Turnstile> v : r" 
+  shows "flat v \<in> L r"
+using assms
+by (induct) (auto simp add: Sequ_def Star_concat)
 
-definition 
-  LV :: "rexp \<Rightarrow> string \<Rightarrow> val set"
-where "LV r s \<equiv> {v.  \<turnstile> v : r \<and> flat v = s}"
+lemma L_flat_Prf2:
+  assumes "s \<in> L r" 
+  shows "\<exists>v. \<Turnstile> v : r \<and> flat v = s"
+using assms
+proof(induct r arbitrary: s)
+  case (STAR r s)
+  have IH: "\<And>s. s \<in> L r \<Longrightarrow> \<exists>v. \<Turnstile> v : r \<and> flat v = s" by fact
+  have "s \<in> L (STAR r)" by fact
+  then obtain ss where "concat ss = s" "\<forall>s \<in> set ss. s \<in> L r \<and> s \<noteq> []"
+  using Star_cstring by auto  
+  then obtain vs where "flats vs = s" "\<forall>v\<in>set vs. \<Turnstile> v : r \<and> flat v \<noteq> []"
+  using IH Star_cval by metis 
+  then show "\<exists>v. \<Turnstile> v : STAR r \<and> flat v = s"
+  using Prf.intros(6) flat_Stars by blast
+next 
+  case (SEQ r1 r2 s)
+  then show "\<exists>v. \<Turnstile> v : SEQ r1 r2 \<and> flat v = s"
+  unfolding Sequ_def L.simps by (fastforce intro: Prf.intros)
+next
+  case (ALT r1 r2 s)
+  then show "\<exists>v. \<Turnstile> v : ALT r1 r2 \<and> flat v = s"
+  unfolding L.simps by (fastforce intro: Prf.intros)
+qed (auto intro: Prf.intros)
+
+
+lemma L_flat_Prf:
+  shows "L(r) = {flat v | v. \<Turnstile> v : r}"
+using L_flat_Prf1 L_flat_Prf2 by blast
+
+
+
+section {* Sets of Lexical Values *}
+
+text {*
+  Shows that lexical values are finite for a given regex and string.
+*}
 
 definition
-  CV :: "rexp \<Rightarrow> string \<Rightarrow> val set"
-where  "CV r s \<equiv> {v. \<Turnstile> v : r \<and> flat v = s}"
+  LV :: "rexp \<Rightarrow> string \<Rightarrow> val set"
+where  "LV r s \<equiv> {v. \<Turnstile> v : r \<and> flat v = s}"
 
-lemma LV_CV_subset:
-  shows "CV r s \<subseteq> LV r s"
-unfolding CV_def LV_def by(auto simp add: Prf_CPrf)
+lemma LV_simps:
+  shows "LV ZERO s = {}"
+  and   "LV ONE s = (if s = [] then {Void} else {})"
+  and   "LV (CHAR c) s = (if s = [c] then {Char c} else {})"
+  and   "LV (ALT r1 r2) s = Left ` LV r1 s \<union> Right ` LV r2 s"
+unfolding LV_def
+by (auto intro: Prf.intros elim: Prf.cases)
+
 
 abbreviation
   "Prefixes s \<equiv> {s'. prefixeq s' s}"
@@ -389,13 +342,6 @@
   shows "Suffixes (c # s) = Suffixes s \<union> {c # s}"
 by (auto simp add: suffixeq_def Cons_eq_append_conv)
 
-lemma CV_simps:
-  shows "CV ZERO s = {}"
-  and   "CV ONE s = (if s = [] then {Void} else {})"
-  and   "CV (CHAR c) s = (if s = [c] then {Char c} else {})"
-  and   "CV (ALT r1 r2) s = Left ` CV r1 s \<union> Right ` CV r2 s"
-unfolding CV_def
-by (auto intro: CPrf.intros elim: CPrf.cases)
 
 lemma finite_Suffixes: 
   shows "finite (Suffixes s)"
@@ -423,34 +369,17 @@
   ultimately show "finite (Prefixes s)" by simp
 qed
 
-lemma CV_SEQ_subset:
-  "CV (SEQ r1 r2) s \<subseteq> (\<lambda>(v1,v2). Seq v1 v2) ` ((\<Union>s' \<in> Prefixes s. CV r1 s') \<times> (\<Union>s' \<in> Suffixes s. CV r2 s'))"
-unfolding image_def CV_def prefixeq_def suffixeq_def
-by (auto elim: CPrf.cases)
-
-lemma CV_STAR_subset:
-  "CV (STAR r) s \<subseteq> {Stars []} \<union>
-      (\<lambda>(v,vs). Stars (v#vs)) ` ((\<Union>s' \<in> Prefixes s. CV r s') \<times> (\<Union>s2 \<in> SSuffixes s. Stars -` (CV (STAR r) s2)))"
-unfolding image_def CV_def prefixeq_def suffix_def
-apply(auto)
-apply(erule CPrf.cases)
-apply(auto)
-apply(case_tac vs)
-apply(auto intro: CPrf.intros)
-done
-
-
-lemma CV_STAR_finite:
-  assumes "\<forall>s. finite (CV r s)"
-  shows "finite (CV (STAR r) s)"
+lemma LV_STAR_finite:
+  assumes "\<forall>s. finite (LV r s)"
+  shows "finite (LV (STAR r) s)"
 proof(induct s rule: length_induct)
   fix s::"char list"
-  assume "\<forall>s'. length s' < length s \<longrightarrow> finite (CV (STAR r) s')"
-  then have IH: "\<forall>s' \<in> SSuffixes s. finite (CV (STAR r) s')"
+  assume "\<forall>s'. length s' < length s \<longrightarrow> finite (LV (STAR r) s')"
+  then have IH: "\<forall>s' \<in> SSuffixes s. finite (LV (STAR r) s')"
     by (auto simp add: suffix_def) 
   def f \<equiv> "\<lambda>(v, vs). Stars (v # vs)"
-  def S1 \<equiv> "\<Union>s' \<in> Prefixes s. CV r s'"
-  def S2 \<equiv> "\<Union>s2 \<in> SSuffixes s. Stars -` (CV (STAR r) s2)"
+  def S1 \<equiv> "\<Union>s' \<in> Prefixes s. LV r s'"
+  def S2 \<equiv> "\<Union>s2 \<in> SSuffixes s. Stars -` (LV (STAR r) s2)"
   have "finite S1" using assms
     unfolding S1_def by (simp_all add: finite_Prefixes)
   moreover 
@@ -459,44 +388,53 @@
   ultimately 
   have "finite ({Stars []} \<union> f ` (S1 \<times> S2))" by simp
   moreover 
-  have "CV (STAR r) s \<subseteq> {Stars []} \<union> f ` (S1 \<times> S2)" unfolding S1_def S2_def f_def
-     by (rule CV_STAR_subset)
+  have "LV (STAR r) s \<subseteq> {Stars []} \<union> f ` (S1 \<times> S2)" 
+  unfolding S1_def S2_def f_def
+  unfolding LV_def image_def prefixeq_def suffix_def
+  apply(auto elim: Prf_elims)
+  apply(erule Prf_elims)
+  apply(auto)
+  apply(case_tac vs)
+  apply(auto intro: Prf.intros)
+  done  
   ultimately
-  show "finite (CV (STAR r) s)" by (simp add: finite_subset)
+  show "finite (LV (STAR r) s)" by (simp add: finite_subset)
 qed  
     
 
-lemma CV_finite:
-  shows "finite (CV r s)"
+lemma LV_finite:
+  shows "finite (LV r s)"
 proof(induct r arbitrary: s)
   case (ZERO s) 
-  show "finite (CV ZERO s)" by (simp add: CV_simps)
+  show "finite (LV ZERO s)" by (simp add: LV_simps)
 next
   case (ONE s)
-  show "finite (CV ONE s)" by (simp add: CV_simps)
+  show "finite (LV ONE s)" by (simp add: LV_simps)
 next
   case (CHAR c s)
-  show "finite (CV (CHAR c) s)" by (simp add: CV_simps)
+  show "finite (LV (CHAR c) s)" by (simp add: LV_simps)
 next 
   case (ALT r1 r2 s)
-  then show "finite (CV (ALT r1 r2) s)" by (simp add: CV_simps)
+  then show "finite (LV (ALT r1 r2) s)" by (simp add: LV_simps)
 next 
   case (SEQ r1 r2 s)
   def f \<equiv> "\<lambda>(v1, v2). Seq v1 v2"
-  def S1 \<equiv> "\<Union>s' \<in> Prefixes s. CV r1 s'"
-  def S2 \<equiv> "\<Union>s' \<in> Suffixes s. CV r2 s'"
-  have IHs: "\<And>s. finite (CV r1 s)" "\<And>s. finite (CV r2 s)" by fact+
+  def S1 \<equiv> "\<Union>s' \<in> Prefixes s. LV r1 s'"
+  def S2 \<equiv> "\<Union>s' \<in> Suffixes s. LV r2 s'"
+  have IHs: "\<And>s. finite (LV r1 s)" "\<And>s. finite (LV r2 s)" by fact+
   then have "finite S1" "finite S2" unfolding S1_def S2_def
     by (simp_all add: finite_Prefixes finite_Suffixes)
   moreover
-  have "CV (SEQ r1 r2) s \<subseteq> f ` (S1 \<times> S2)"
-    unfolding f_def S1_def S2_def by (auto simp add: CV_SEQ_subset)
+  have "LV (SEQ r1 r2) s \<subseteq> f ` (S1 \<times> S2)"
+    unfolding f_def S1_def S2_def 
+    unfolding LV_def image_def prefixeq_def suffixeq_def
+    by (auto elim: Prf.cases)
   ultimately 
-  show "finite (CV (SEQ r1 r2) s)"
+  show "finite (LV (SEQ r1 r2) s)"
     by (simp add: finite_subset)
 next
   case (STAR r s)
-  then show "finite (CV (STAR r) s)" by (simp add: CV_STAR_finite)
+  then show "finite (LV (STAR r) s)" by (simp add: LV_STAR_finite)
 qed
 
 
@@ -533,14 +471,6 @@
 by (induct s r v rule: Posix.induct)
    (auto simp add: Sequ_def)
 
-lemma Posix_Prf:
-  assumes "s \<in> r \<rightarrow> v"
-  shows "\<turnstile> v : r"
-using assms
-apply(induct s r v rule: Posix.induct)
-apply(auto intro!: Prf.intros elim!: Prf_elims)
-done
-
 text {*
   Our Posix definition determines a unique value.
 *}
@@ -616,30 +546,31 @@
   Our POSIX value is a canonical value.
 *}
 
-lemma Posix_CV:
+lemma Posix_LV:
   assumes "s \<in> r \<rightarrow> v"
-  shows "v \<in> CV r s"
+  shows "v \<in> LV r s"
 using assms
 apply(induct rule: Posix.induct)
-apply(auto simp add: CV_def intro: CPrf.intros elim: CPrf.cases)
+apply(auto simp add: LV_def intro: Prf.intros elim: Prf.cases)
 apply(rotate_tac 5)
-apply(erule CPrf.cases)
+apply(erule Prf.cases)
 apply(simp_all)
-apply(rule CPrf.intros)
+apply(rule Prf.intros)
 apply(simp_all)
 done
 
+(*
 lemma test2: 
   assumes "\<forall>v \<in> set vs. flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []"
-  shows "(Stars vs) \<in> CV (STAR r) (flat (Stars vs))" 
+  shows "(Stars vs) \<in> LV (STAR r) (flat (Stars vs))" 
 using assms
 apply(induct vs)
-apply(auto simp add: CV_def)
-apply(rule CPrf.intros)
+apply(auto simp add: LV_def)
+apply(rule Prf.intros)
 apply(simp)
-apply(rule CPrf.intros)
+apply(rule Prf.intros)
 apply(simp_all)
-by (metis (no_types, lifting) CV_def Posix_CV mem_Collect_eq)
-
+by (metis (no_types, lifting) LV_def Posix_LV mem_Collect_eq)
+*)
 
 end
\ No newline at end of file