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)