--- 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