# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1507203913 -3600
# Node ID deea42c83c9e541ca8649ea0302299a1fa8976ea
# Parent  692b62426677dd485e22d93fb379d5300d6aac07
updated

diff -r 692b62426677 -r deea42c83c9e thys/Journal/Paper.thy
--- a/thys/Journal/Paper.thy	Fri Sep 22 12:25:25 2017 +0100
+++ b/thys/Journal/Paper.thy	Thu Oct 05 12:45:13 2017 +0100
@@ -223,10 +223,10 @@
 \noindent where @{const Stars}, @{text Left}, @{text Right} and @{text
 Char} are constructors for values. @{text Stars} records how many
 iterations were used; @{text Left}, respectively @{text Right}, which
-alternative is used. This `tree view' leads naturally to the
-idea that regular expressions act as types and values as inhabiting
-those types. This view was first put forward by ???. The value for the
-single `iteration', i.e.~the POSIX value, would look as follows
+alternative is used. This `tree view' leads naturally to the idea that
+regular expressions act as types and values as inhabiting those types
+(see, for example, \cite{HosoyaVouillonPierce2005}).  The value for
+the single `iteration', i.e.~the POSIX value, would look as follows
 
 \begin{center}
 @{term "Stars [Seq (Char x) (Char y)]"}
@@ -1253,8 +1253,8 @@
   being inhabited by the same regular expression. The
   complexity of the proofs involved seems to not justify such a
   `cleaner' single statement. The statements given are just the properties that
-  allow us to establish our theorems. The proofs for Proposition~\ref{ordintros}
-  are routine.
+  allow us to establish our theorems without any difficulty. The proofs 
+  for Proposition~\ref{ordintros} are routine.
  
 
   Next we establish how Okui and Suzuki's orderings relate to our
diff -r 692b62426677 -r deea42c83c9e thys/Journal/document/root.bib
--- a/thys/Journal/document/root.bib	Fri Sep 22 12:25:25 2017 +0100
+++ b/thys/Journal/document/root.bib	Thu Oct 05 12:45:13 2017 +0100
@@ -1,4 +1,12 @@
-
+@article{HosoyaVouillonPierce2005,
+  author = {H.~Hosoya and J.~Vouillon and B.~C.~Pierce},
+  title = {{R}egular {E}xpression {T}ypes for {XML}},
+  journal = {ACM Transactions on Programming Languages and Systems (TOPLAS)},
+  year = {2005},
+  volume = 27,
+  number = 1,
+  pages = {46--90}
+}
 
 
 @Misc{POSIX,
diff -r 692b62426677 -r deea42c83c9e thys/Journal/document/root.tex
--- a/thys/Journal/document/root.tex	Fri Sep 22 12:25:25 2017 +0100
+++ b/thys/Journal/document/root.tex	Thu Oct 05 12:45:13 2017 +0100
@@ -72,7 +72,7 @@
 in order to deal with POSIX matching, which is the underlying
 disambiguation strategy for regular expressions needed in lexers.
 Their algorithm generates POSIX values which encode the information of
-\emph{how} a regular expression matched a string---that is, which part
+\emph{how} a regular expression matches a string---that is, which part
 of the string is matched by which part of the regular expression.  In
 this paper we give our inductive definition of what a POSIX value is
 and show $(i)$ that such a value is unique (for given regular
diff -r 692b62426677 -r deea42c83c9e thys/SpecExt.thy
--- a/thys/SpecExt.thy	Fri Sep 22 12:25:25 2017 +0100
+++ b/thys/SpecExt.thy	Thu Oct 05 12:45:13 2017 +0100
@@ -493,11 +493,15 @@
     length (vs1 @ vs2) = n\<rbrakk> \<Longrightarrow> \<Turnstile> Stars (vs1 @ vs2) : NTIMES r n"
 | "\<lbrakk>\<forall>v \<in> set vs1. \<Turnstile> v : r  \<and> flat v \<noteq> []; 
     \<forall>v \<in> set vs2. \<Turnstile> v : r \<and> flat v = []; 
-    length (vs1 @ vs2) \<ge> n\<rbrakk> \<Longrightarrow> \<Turnstile> Stars (vs1 @ vs2) : FROMNTIMES r n"
+    length (vs1 @ vs2) = n\<rbrakk> \<Longrightarrow> \<Turnstile> Stars (vs1 @ vs2) : FROMNTIMES r n"
+| "\<lbrakk>\<forall>v \<in> set vs. \<Turnstile> v : r  \<and> flat v \<noteq> []; length vs > n\<rbrakk> \<Longrightarrow> \<Turnstile> Stars vs : FROMNTIMES r n"
 | "\<lbrakk>\<forall>v \<in> set vs1. \<Turnstile> v : r \<and> flat v \<noteq> [];
     \<forall>v \<in> set vs2. \<Turnstile> v : r \<and> flat v = []; 
-    length (vs1 @ vs2) \<ge> n; length (vs1 @ vs2) \<le> m\<rbrakk> \<Longrightarrow> \<Turnstile> Stars (vs1 @ vs2) : NMTIMES r n m"
+    length (vs1 @ vs2) = n; length (vs1 @ vs2) \<le> m\<rbrakk> \<Longrightarrow> \<Turnstile> Stars (vs1 @ vs2) : NMTIMES r n m"
+| "\<lbrakk>\<forall>v \<in> set vs. \<Turnstile> v : r \<and> flat v \<noteq> [];
+    length vs > n; length vs \<le> m\<rbrakk> \<Longrightarrow> \<Turnstile> Stars vs : NMTIMES r n m"
 
+  
 inductive_cases Prf_elims:
   "\<Turnstile> v : ZERO"
   "\<Turnstile> v : SEQ r1 r2"
@@ -602,8 +606,12 @@
 apply(auto simp add: Sequ_def Star_concat Pow_flats)
 apply(meson Pow_flats atMost_iff)
 using Pow_flats_appends apply blast
-apply(meson Pow_flats_appends atLeast_iff)
+using Pow_flats_appends apply blast
+apply (meson Pow_flats atLeast_iff less_imp_le)
+apply(rule_tac x="length vs1 + length vs2" in  bexI)
 apply(meson Pow_flats_appends atLeastAtMost_iff)
+apply(simp)
+apply(meson Pow_flats atLeastAtMost_iff less_or_eq_imp_le)
 done
 
 lemma L_flat_Prf2:
@@ -655,9 +663,9 @@
   case (FROMNTIMES r n)
   have IH: "\<And>s. s \<in> L r \<Longrightarrow> \<exists>v. \<Turnstile> v : r \<and> flat v = s" by fact
   have "s \<in> L (FROMNTIMES r n)" by fact 
-  then obtain ss1 ss2 m where "concat (ss1 @ ss2) = s" "length (ss1 @ ss2) = m" "n \<le> m" 
+  then obtain ss1 ss2 m where "concat (ss1 @ ss2) = s" "length (ss1 @ ss2) = m"  "n \<le> m"
     "\<forall>s \<in> set ss1. s \<in> L r \<and> s \<noteq> []" "\<forall>s \<in> set ss2. s \<in> L r \<and> s = []"
-  using Pow_cstring by auto blast
+    using Pow_cstring by force 
   then obtain vs1 vs2 where "flats (vs1 @ vs2) = s" "length (vs1 @ vs2) = m" "n \<le> m"
       "\<forall>v\<in>set vs1. \<Turnstile> v : r \<and> flat v \<noteq> []" "\<forall>v\<in>set vs2. \<Turnstile> v : r \<and> flat v = []"
   using IH flats_cval 
@@ -673,7 +681,26 @@
   apply(simp)
   done
   then show "\<exists>v. \<Turnstile> v : FROMNTIMES r n \<and> flat v = s"
-  using Prf.intros(9) flat_Stars by blast
+  apply(case_tac "length vs1 \<le> n")
+  apply(rule_tac x="Stars (vs1 @ take (n - length vs1) vs2)" in exI)
+  apply(simp)
+  apply(subgoal_tac "flats (take (n - length vs1) vs2) = []")
+  prefer 2
+  apply (meson flats_empty in_set_takeD)
+  apply(clarify)
+    apply(rule conjI)
+      apply(rule Prf.intros)
+        apply(simp)
+       apply (meson in_set_takeD)
+      apply(simp)
+     apply(simp)
+     apply (simp add: flats_empty)
+      apply(rule_tac x="Stars vs1" in exI)
+  apply(simp)
+    apply(rule conjI)
+     apply(rule Prf.intros(10))
+      apply(auto)
+  done    
 next 
   case (NMTIMES r n m)
   have IH: "\<And>s. s \<in> L r \<Longrightarrow> \<exists>v. \<Turnstile> v : r \<and> flat v = s" by fact
@@ -699,8 +726,8 @@
   apply(rule_tac x="Stars (vs1 @ vs2)" in exI)
   apply(simp)
   apply(rule Prf.intros)
-  apply(auto) 
-  done
+       apply(auto) 
+  sorry
 next 
   case (UPNTIMES r n s)
   have IH: "\<And>s. s \<in> L r \<Longrightarrow> \<exists>v. \<Turnstile> v : r \<and> flat v = s" by fact
@@ -740,17 +767,17 @@
 done
 
 abbreviation
-  "Prefixes s \<equiv> {s'. prefixeq s' s}"
+  "Prefixes s \<equiv> {s'. prefix s' s}"
 
 abbreviation
-  "Suffixes s \<equiv> {s'. suffixeq s' s}"
+  "Suffixes s \<equiv> {s'. suffix s' s}"
 
 abbreviation
-  "SSuffixes s \<equiv> {s'. suffix s' s}"
+  "SSuffixes s \<equiv> {s'. strict_suffix s' s}"
 
 lemma Suffixes_cons [simp]:
   shows "Suffixes (c # s) = Suffixes s \<union> {c # s}"
-by (auto simp add: suffixeq_def Cons_eq_append_conv)
+by (auto simp add: suffix_def Cons_eq_append_conv)
 
 
 lemma finite_Suffixes: 
@@ -761,7 +788,7 @@
   shows "finite (SSuffixes s)"
 proof -
   have "SSuffixes s \<subseteq> Suffixes s"
-   unfolding suffix_def suffixeq_def by auto
+   unfolding suffix_def strict_suffix_def by auto
   then show "finite (SSuffixes s)"
    using finite_Suffixes finite_subset by blast
 qed
@@ -774,7 +801,7 @@
   then have "finite (rev ` Suffixes (rev s))" by simp
   moreover
   have "rev ` (Suffixes (rev s)) = Prefixes s"
-  unfolding suffixeq_def prefixeq_def image_def
+  unfolding suffix_def prefix_def image_def
    by (auto)(metis rev_append rev_rev_ident)+
   ultimately show "finite (Prefixes s)" by simp
 qed
@@ -786,10 +813,10 @@
   fix s::"char list"
   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. LV r s'"
-  def S2 \<equiv> "\<Union>s2 \<in> SSuffixes s. Stars -` (LV (STAR r) s2)"
+    by (auto simp add: strict_suffix_def) 
+  define f where "f \<equiv> \<lambda>(v, vs). Stars (v # vs)"
+  define S1 where "S1 \<equiv> \<Union>s' \<in> Prefixes s. LV r s'"
+  define S2 where "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 
@@ -800,13 +827,22 @@
   moreover 
   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
+  unfolding LV_def image_def prefix_def strict_suffix_def
+  apply(auto)
+  apply(case_tac x)
   apply(auto elim: Prf_elims)
   apply(erule Prf_elims)
   apply(auto)
   apply(case_tac vs)
-  apply(auto intro: Prf.intros)
-  done  
+  apply(auto intro: Prf.intros)  
+  apply(rule exI)
+  apply(rule conjI)
+  apply(rule_tac x="flat a" in exI)
+  apply(rule conjI)
+  apply(rule_tac x="flats list" in exI)
+  apply(simp)
+  apply(blast)
+  using Prf.intros(6) by blast  
   ultimately
   show "finite (LV (STAR r) s)" by (simp add: finite_subset)
 qed  
@@ -815,40 +851,6 @@
   "LV (UPNTIMES r n) s \<subseteq> LV (STAR r) s"
 by(auto simp add: LV_def intro: Prf.intros elim: Prf_elims)
 
-(*
-lemma LV_NTIMES_finite:
-  assumes "\<forall>s. finite (LV r s)"
-  shows "finite (LV (NTIMES r n) s)"
-proof(induct s rule: length_induct)
-  fix s::"char list"
-  assume "\<forall>s'. length s' < length s \<longrightarrow> finite (LV (NTIMES r n) s')"
-  then have IH: "\<forall>s' \<in> SSuffixes s. finite (LV (NTIMES r n) s')"
-    by (auto simp add: suffix_def) 
-  def f \<equiv> "\<lambda>(v, vs). Stars (v # vs)"
-  def S1 \<equiv> "\<Union>s' \<in> Prefixes s. LV r s'"
-  def S2 \<equiv> "\<Union>s2 \<in> SSuffixes s. Stars -` (LV (NTIMES r n) s2)"
-  have "finite S1" using assms
-    unfolding S1_def by (simp_all add: finite_Prefixes)
-  moreover 
-  with IH have "finite S2" unfolding S2_def
-    by (auto simp add: finite_SSuffixes inj_on_def finite_vimageI)
-  ultimately 
-  have "finite ({Stars []} \<union> f ` (S1 \<times> S2))" by simp
-  moreover 
-  have "LV (NTIMES r n) 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 vs1)
-  apply(auto intro: Prf.intros)
-  
-  done  
-  ultimately
-  show "finite (LV (STAR r) s)" by (simp add: finite_subset)
-qed  
-*)
 
 lemma LV_NTIMES_0:
   shows "LV (NTIMES r 0) s \<subseteq> {Stars []}"
@@ -898,20 +900,51 @@
 
 thm card_cartesian_product
 
-lemma LV_empty_finite:
-  shows "card (LV (NTIMES r n) []) \<le> ((card (LV r [])) ^ n)"
-apply(induct n arbitrary:)
-using LV_NTIMES_0
-apply (metis card_empty card_insert_disjoint card_mono empty_iff finite.emptyI finite.insertI nat_power_eq_Suc_0_iff)
-apply(simp add: LV_NTIMES_3)
-apply(subst card_image)
-apply(simp add: inj_on_def)
-apply(subst card_cartesian_product)
-apply(subst card_vimage_inj)
-apply(simp add: inj_on_def)
-apply(auto simp add: LV_def elim: Prf_elims)[1]
-using nat_mult_le_cancel_disj by blast
+lemma finite_list:
+  assumes "finite A"
+  shows "finite {vs. \<forall>v\<in>set vs. v \<in> A \<and> length vs = n}"
+  apply(induct n)
+   apply(simp)
+   apply (smt Collect_cong empty_iff finite.emptyI finite.insertI 
+   in_listsI list.set(1) lists_empty mem_Collect_eq singleton_conv2)
+  apply(rule_tac B="{[]} \<union> (\<lambda>(v,vs). v # vs) `(A \<times> {vs. \<forall>v\<in>set vs. v \<in> A \<and> length vs = n})" in finite_subset)  
+   apply(auto simp add: image_def)[1]
+   apply(case_tac x)
+    apply(simp)
+   apply(simp)
+  apply(simp)
+  apply(rule finite_imageI)
+    using assms
+    apply(simp)
+    done
+      
+lemma test:
+  "LV (NTIMES r n) [] \<subseteq> Stars ` {vs. \<forall>v \<in> set vs. v \<in> LV r [] \<and> length vs = n}"
+apply(auto simp add: LV_def elim: Prf_elims)
+done
+    
+lemma test3:
+  "LV (FROMNTIMES r n) [] \<subseteq> Stars ` {vs. \<forall>v \<in> set vs. v \<in> LV r [] \<and> length vs = n}"
+  apply(auto simp add: image_def LV_def elim!: Prf_elims)
+   apply blast
+  apply(case_tac vs)
+    apply(auto)
+  done   
+    
+    
 
+lemma LV_NTIMES_empty_finite:
+  assumes "finite (LV r [])"
+  shows "finite (LV (NTIMES r n) [])"
+  using assms
+  apply -  
+  apply(rule finite_subset)
+   apply(rule test)
+  apply(rule finite_imageI)
+    apply(rule finite_list)
+   apply(simp)
+  done
+    
 lemma LV_NTIMES_STAR:
   "LV (NTIMES r n) s \<subseteq> LV (STAR r) s"
 apply(auto simp add: LV_def intro: Prf.intros elim!: Prf_elims)
@@ -939,17 +972,18 @@
   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. LV r1 s'"
-  def S2 \<equiv> "\<Union>s' \<in> Suffixes s. LV r2 s'"
+  define f where "f \<equiv> \<lambda>(v1, v2). Seq v1 v2"
+  define S1 where "S1 \<equiv> \<Union>s' \<in> Prefixes s. LV r1 s'"
+  define S2 where "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 "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)
+    unfolding LV_def image_def prefix_def suffix_def
+    apply (auto elim!: Prf_elims)
+    by (metis (mono_tags, lifting) mem_Collect_eq)
   ultimately 
   show "finite (LV (SEQ r1 r2) s)"
     by (simp add: finite_subset)