--- a/Derivatives.thy	Thu Jul 28 14:22:10 2011 +0000
+++ b/Derivatives.thy	Thu Jul 28 17:52:36 2011 +0000
@@ -66,8 +66,8 @@
     apply(auto simp add: Cons_eq_append_conv)
     done
     
-  have "Der c (A\<star>) = Der c ({[]} \<union> A \<cdot> A\<star>)"
-    by (simp only: star_cases[symmetric])
+  have "Der c (A\<star>) = Der c (A \<cdot> A\<star> \<union> {[]})"
+    by (simp only: star_unfold_left[symmetric])
   also have "... = Der c (A \<cdot> A\<star>)"
     by (simp only: Der_union Der_one) (simp)
   also have "... = (Der c A) \<cdot> A\<star> \<union> (Delta A \<cdot> Der c (A\<star>))"
@@ -157,7 +157,7 @@
   pders :: "'a list \<Rightarrow> 'a rexp \<Rightarrow> ('a rexp) set"
 where
   "pders [] r = {r}"
-| "pders (c # s) r = (\<Union>r'\<in> (pder c r). (pders s r'))"
+| "pders (c # s) r = \<Union> (pders s) ` (pder c r)"
 
 abbreviation
   "pders_set A r \<equiv> \<Union>s \<in> A. pders s r"

--- a/Journal/Paper.thy	Thu Jul 28 14:22:10 2011 +0000
+++ b/Journal/Paper.thy	Thu Jul 28 17:52:36 2011 +0000
@@ -67,7 +67,8 @@
   tag_str_Star ("tag\<^isub>S\<^isub>T\<^isub>A\<^isub>R _ _" [100, 100] 100) and
   tag_eq_rel ("\<^raw:$\threesim$>\<^bsub>_\<^esub>") and
   Delta ("\<Delta>'(_')") and
-  nullable ("\<delta>'(_')")
+  nullable ("\<delta>'(_')") and
+  Cons ("_ :: _" [100, 100] 100)
 
 lemma meta_eq_app:
   shows "f \<equiv> \<lambda>x. g x \<Longrightarrow> f x \<equiv> g x"
@@ -389,7 +390,7 @@
   
   \begin{prpstn}\label{langprops}\mbox{}\\
   \begin{tabular}{@ {}ll}
-  (i)   & @{thm star_cases}     \\ 
+  (i)   & @{thm star_unfold_left}     \\ 
   (ii)  & @{thm[mode=IfThen] pow_length}\\
   (iii) & @{thm conc_Union_left} \\ 
   \end{tabular}
@@ -1098,8 +1099,38 @@
   Much more interesting, however, are the inductive cases. They seem hard to solve 
   directly. The reader is invited to try. 
 
-  Constable et al \cite{Constable00} give the following suggestive picture about
-  equivalence classes:
+  In order how to see how our first proof proceeds we use the following suggestive picture 
+  from Constable et al \cite{Constable00}:
+
+  \begin{center}
+  \begin{tabular}{c@ {\hspace{10mm}}c@ {\hspace{10mm}}c}
+  \begin{tikzpicture}[scale=1]
+  %Circle
+  \draw[thick] (0,0) circle (1.1);    
+  \end{tikzpicture}
+  &
+  \begin{tikzpicture}[scale=1]
+  %Circle
+  \draw[thick] (0,0) circle (1.1);    
+  %Main rays
+  \foreach \a in {0, 90,...,359}
+    \draw[very thick] (0, 0) -- (\a:1.1);
+  \foreach \a / \l in {45/1, 135/2, 225/3, 315/4}
+      \draw (\a: 0.65) node {$a_\l$};
+  \end{tikzpicture}
+  &
+  \begin{tikzpicture}[scale=1]
+  %Circle
+  \draw[thick] (0,0) circle (1.1);    
+  %Main rays
+  \foreach \a in {0, 45,...,359}
+     \draw[very thick] (0, 0) -- (\a:1.1);
+  \foreach \a / \l in {22.5/1.1, 67.5/1.2, 112.5/2.1, 157.5/2.2, 202.4/3.1, 247.5/3.2, 292.5/4.1, 337.5/4.2}
+      \draw (\a: 0.77) node {$a_{\l}$};
+  \end{tikzpicture}\\
+  @{term UNIV} & @{term "UNIV // (\<approx>(lang r))"} & @{term "UNIV // R"}
+  \end{tabular}
+  \end{center}
 
   Our first proof will rely on some
   \emph{tagging-functions} defined over strings. Given the inductive hypothesis, it will 

--- a/More_Regular_Set.thy	Thu Jul 28 14:22:10 2011 +0000
+++ b/More_Regular_Set.thy	Thu Jul 28 17:52:36 2011 +0000
@@ -9,25 +9,6 @@
   conc (infixr "\<cdot>" 100) and
   star ("_\<star>" [101] 102)
 
-lemma conc_add_left:
-  assumes a: "A = B"
-  shows "C \<cdot> A = C \<cdot> B"
-using a by simp
-
-lemma star_cases:
-  shows "A\<star> =  {[]} \<union> A \<cdot> A\<star>"
-proof
-  { fix x
-    have "x \<in> A\<star> \<Longrightarrow> x \<in> {[]} \<union> A \<cdot> A\<star>"
-      unfolding conc_def
-    by (induct rule: star_induct) (auto)
-  }
-  then show "A\<star> \<subseteq> {[]} \<union> A \<cdot> A\<star>" by auto
-next
-  show "{[]} \<union> A \<cdot> A\<star> \<subseteq> A\<star>"
-    unfolding conc_def by auto
-qed
-
 lemma star_decom: 
   assumes a: "x \<in> A\<star>" "x \<noteq> []"
   shows "\<exists>a b. x = a @ b \<and> a \<noteq> [] \<and> a \<in> A \<and> b \<in> A\<star>"
@@ -109,9 +90,9 @@
   assume eq: "X = B \<cdot> A\<star>"
   have "A\<star> = {[]} \<union> A\<star> \<cdot> A" 
     unfolding conc_star_comm[symmetric]
-    by (rule star_cases)
+    by(metis Un_commute star_unfold_left)
   then have "B \<cdot> A\<star> = B \<cdot> ({[]} \<union> A\<star> \<cdot> A)"
-    by (rule conc_add_left)
+    by metis
   also have "\<dots> = B \<union> B \<cdot> (A\<star> \<cdot> A)"
     unfolding conc_Un_distrib by simp
   also have "\<dots> = B \<union> (B \<cdot> A\<star>) \<cdot> A" 

--- a/Myhill_2.thy	Thu Jul 28 14:22:10 2011 +0000
+++ b/Myhill_2.thy	Thu Jul 28 17:52:36 2011 +0000
@@ -399,7 +399,7 @@
         proof -
           from h1 have "(x - xa_max) @ z \<noteq> []" 
             by (auto simp:strict_prefix_def elim:prefixE)
-          from star_decom [OF h3 this]
+	  from star_decom [OF h3 this]
           obtain a b where a_in: "a \<in> L\<^isub>1" 
             and a_neq: "a \<noteq> []" and b_in: "b \<in> L\<^isub>1\<star>" 
             and ab_max: "(x - xa_max) @ z = a @ b" by blast