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

diff -r e85099ac4c6c -r 692b62426677 thys/Journal/Paper.thy
--- a/thys/Journal/Paper.thy	Wed Sep 06 00:52:08 2017 +0100
+++ b/thys/Journal/Paper.thy	Fri Sep 22 12:25:25 2017 +0100
@@ -16,7 +16,7 @@
 declare [[show_question_marks = false]]
 
 syntax (latex output)
-  "_Collect" :: "pttrn => bool => 'a set"              ("(1{_ \<^raw:\mbox{\boldmath$\mid$}> _})")
+  "_Collect" :: "pttrn => bool => 'a set"              ("(1{_ \<^latex>\<open>\\mbox{\\boldmath$\\mid$}\<close> _})")
   "_CollectIn" :: "pttrn => 'a set => bool => 'a set"   ("(1{_ \<in> _ |e _})")
 
 syntax
@@ -38,8 +38,8 @@
 
 
 notation (latex output)
-  If  ("(\<^raw:\textrm{>if\<^raw:}> (_)/ \<^raw:\textrm{>then\<^raw:}> (_)/ \<^raw:\textrm{>else\<^raw:}> (_))" 10) and
-  Cons ("_\<^raw:\mbox{$\,$}>::\<^raw:\mbox{$\,$}>_" [75,73] 73) and  
+  If  ("(\<^latex>\<open>\\textrm{\<close>if\<^latex>\<open>}\<close> (_)/ \<^latex>\<open>\\textrm{\<close>then\<^latex>\<open>}\<close> (_)/ \<^latex>\<open>\\textrm{\<close>else\<^latex>\<open>}\<close> (_))" 10) and
+  Cons ("_\<^latex>\<open>\\mbox{$\\,$}\<close>::\<^latex>\<open>\\mbox{$\\,$}\<close>_" [75,73] 73) and  
 
   ZERO ("\<^bold>0" 81) and 
   ONE ("\<^bold>1" 81) and 
@@ -82,15 +82,15 @@
   simp_ALT ("simp\<^bsub>Alt\<^esub> _ _" [1000, 1000] 1) and
   slexer ("lexer\<^sup>+" 1000) and
 
-  at ("_\<^raw:\mbox{$\downharpoonleft$}>\<^bsub>_\<^esub>") and
+  at ("_\<^latex>\<open>\\mbox{$\\downharpoonleft$}\<close>\<^bsub>_\<^esub>") and
   lex_list ("_ \<prec>\<^bsub>lex\<^esub> _") and
   PosOrd ("_ \<prec>\<^bsub>_\<^esub> _" [77,77,77] 77) and
   PosOrd_ex ("_ \<prec> _" [77,77] 77) and
-  PosOrd_ex_eq ("_ \<^raw:\mbox{$\preccurlyeq$}> _" [77,77] 77) and
+  PosOrd_ex_eq ("_ \<^latex>\<open>\\mbox{$\\preccurlyeq$}\<close> _" [77,77] 77) and
   pflat_len ("\<parallel>_\<parallel>\<^bsub>_\<^esub>") and
-  nprec ("_ \<^raw:\mbox{$\not\prec$}> _" [77,77] 77) and
+  nprec ("_ \<^latex>\<open>\\mbox{$\\not\\prec$}\<close> _" [77,77] 77) and
 
-  DUMMY ("\<^raw:\underline{\hspace{2mm}}>")
+  DUMMY ("\<^latex>\<open>\\underline{\\hspace{2mm}}\<close>")
 
 
 definition 
diff -r e85099ac4c6c -r 692b62426677 thys/Spec.thy
--- a/thys/Spec.thy	Wed Sep 06 00:52:08 2017 +0100
+++ b/thys/Spec.thy	Fri Sep 22 12:25:25 2017 +0100
@@ -330,17 +330,17 @@
 
 
 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: 
@@ -351,7 +351,7 @@
   shows "finite (SSuffixes s)"
 proof -
   have "SSuffixes s \<subseteq> Suffixes s"
-   unfolding suffix_def suffixeq_def by auto
+   unfolding strict_suffix_def suffix_def by auto
   then show "finite (SSuffixes s)"
    using finite_Suffixes finite_subset by blast
 qed
@@ -364,7 +364,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
@@ -376,10 +376,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 
@@ -390,13 +390,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  
@@ -418,17 +427,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)
diff -r e85099ac4c6c -r 692b62426677 thys/SpecExt.thy
--- a/thys/SpecExt.thy	Wed Sep 06 00:52:08 2017 +0100
+++ b/thys/SpecExt.thy	Fri Sep 22 12:25:25 2017 +0100
@@ -516,6 +516,8 @@
 using assms
 by (auto intro: Prf.intros elim!: Prf_elims)
 
+
+
 lemma flats_empty:
   assumes "(\<forall>v\<in>set vs. flat v = [])"
   shows "flats vs = []"
@@ -734,8 +736,8 @@
   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)
-
+apply(auto intro: Prf.intros elim: Prf.cases)
+done
 
 abbreviation
   "Prefixes s \<equiv> {s'. prefixeq s' s}"
@@ -813,6 +815,109 @@
   "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 []}"
+unfolding LV_def
+apply(auto elim: Prf_elims)
+done
+
+lemma LV_NTIMES_1:
+  shows "LV (NTIMES r 1) s \<subseteq> (\<lambda>v. Stars [v]) ` (LV r s)"
+unfolding LV_def
+apply(auto elim!: Prf_elims)
+apply(case_tac vs1)
+apply(simp)
+apply(case_tac vs2)
+apply(simp)
+apply(simp)
+apply(simp)
+done
+
+lemma LV_NTIMES_2:
+  shows "LV (NTIMES r 2) [] \<subseteq> (\<lambda>(v1,v2). Stars [v1,v2]) ` (LV r [] \<times> LV r [])"
+unfolding LV_def
+apply(auto elim!: Prf_elims simp add: image_def)
+apply(case_tac vs1)
+apply(auto)
+apply(case_tac vs2)
+apply(auto)
+apply(case_tac list)
+apply(auto)
+done
+
+lemma LV_NTIMES_3:
+  shows "LV (NTIMES r (Suc n)) [] = (\<lambda>(v,vs). Stars (v#vs)) ` (LV r [] \<times> (Stars -` (LV (NTIMES r n) [])))"
+unfolding LV_def
+apply(auto elim!: Prf_elims simp add: image_def)
+apply(case_tac vs1)
+apply(auto)
+apply(case_tac vs2)
+apply(auto)
+apply(subst append.simps(1)[symmetric])
+apply(rule Prf.intros)
+apply(auto)
+apply(subst append.simps(1)[symmetric])
+apply(rule Prf.intros)
+apply(auto)
+done
+
+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 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)
+apply(rule Prf.intros)
+oops
+
 lemma LV_FROMNTIMES_STAR:
   "LV (FROMNTIMES r n) s \<subseteq> LV (STAR r) s"
 apply(auto simp add: LV_def intro: Prf.intros elim!: Prf_elims)
@@ -852,10 +957,15 @@
   case (STAR r s)
   then show "finite (LV (STAR r) s)" by (simp add: LV_STAR_finite)
 next 
-  case (NTIMES r n s)
+  case (UPNTIMES r n s)
   have "\<And>s. finite (LV r s)" by fact
-  then show "finite (LV (NTIMES r n) s)"
-  apply(simp add: LV_def)
+  then show "finite (LV (UPNTIMES r n) s)"
+  by (meson LV_STAR_finite LV_UPNTIMES_STAR rev_finite_subset)
+next 
+  case (FROMNTIMES r n s)
+  have "\<And>s. finite (LV r s)" by fact
+  then show "finite (LV (FROMNTIMES r n) s)"
+  
 qed