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