diff -r d71424eb5d0c -r b3898315e687 Myhill_1.thy
--- a/Myhill_1.thy	Mon Jan 31 14:51:47 2011 +0000
+++ b/Myhill_1.thy	Wed Feb 02 06:05:12 2011 +0000
@@ -36,18 +36,12 @@
 where 
   "A ;; B = {s\<^isub>1 @ s\<^isub>2 | s\<^isub>1 s\<^isub>2. s\<^isub>1 \<in> A \<and> s\<^isub>2 \<in> B}"
 
-text {* 
-  Transitive closure of language @{text "L"}. 
-*}
+text {* Some properties of operator @{text ";;"}. *}
 
-inductive_set
-  Star :: "lang \<Rightarrow> lang" ("_\<star>" [101] 102)
-  for L 
-where
-  start[intro]: "[] \<in> L\<star>"
-| step[intro]:  "\<lbrakk>s1 \<in> L; s2 \<in> L\<star>\<rbrakk> \<Longrightarrow> s1@s2 \<in> L\<star>" 
-
-text {* Some properties of operator @{text ";;"}. *}
+lemma seq_add_left:
+  assumes a: "A = B"
+  shows "C ;; A = C ;; B"
+using a by simp
 
 lemma seq_union_distrib_right:
   shows "(A \<union> B) ;; C = (A ;; C) \<union> (B ;; C)"
@@ -73,21 +67,73 @@
   and   "{[]} ;; A = A"
 by (simp_all add: Seq_def)
 
+fun 
+  pow :: "lang \<Rightarrow> nat \<Rightarrow> lang" (infixl "\<up>" 100)
+where
+  "A \<up> 0 = {[]}"
+| "A \<up> (Suc n) =  A ;; (A \<up> n)" 
 
-lemma star_intro1[rule_format]: 
-  "x \<in> lang\<star> \<Longrightarrow> \<forall> y. y \<in> lang\<star> \<longrightarrow> x @ y \<in> lang\<star>"
-by (erule Star.induct, auto)
+definition
+  Star :: "lang \<Rightarrow> lang" ("_\<star>" [101] 102)
+where
+  "A\<star> \<equiv> (\<Union>n. A \<up> n)"
+
+lemma star_start[intro]:
+  shows "[] \<in> A\<star>"
+proof -
+  have "[] \<in> A \<up> 0" by auto
+  then show "[] \<in> A\<star>" unfolding Star_def by blast
+qed
+
+lemma star_step [intro]:
+  assumes a: "s1 \<in> A" 
+  and     b: "s2 \<in> A\<star>"
+  shows "s1 @ s2 \<in> A\<star>"
+proof -
+  from b obtain n where "s2 \<in> A \<up> n" unfolding Star_def by auto
+  then have "s1 @ s2 \<in> A \<up> (Suc n)" using a by (auto simp add: Seq_def)
+  then show "s1 @ s2 \<in> A\<star>" unfolding Star_def by blast
+qed
 
-lemma star_intro2: "y \<in> lang \<Longrightarrow> y \<in> lang\<star>"
-by (drule step[of y lang "[]"], auto simp:start)
+lemma star_induct[consumes 1, case_names start step]:
+  assumes a: "x \<in> A\<star>" 
+  and     b: "P []"
+  and     c: "\<And>s1 s2. \<lbrakk>s1 \<in> A; s2 \<in> A\<star>; P s2\<rbrakk> \<Longrightarrow> P (s1 @ s2)"
+  shows "P x"
+proof -
+  from a obtain n where "x \<in> A \<up> n" unfolding Star_def by auto
+  then show "P x"
+    by (induct n arbitrary: x)
+       (auto intro!: b c simp add: Seq_def Star_def)
+qed
+    
+lemma star_intro1:
+  assumes a: "x \<in> A\<star>"
+  and     b: "y \<in> A\<star>"
+  shows "x @ y \<in> A\<star>"
+using a b
+by (induct rule: star_induct) (auto)
 
-lemma star_intro3[rule_format]: 
-  "x \<in> lang\<star> \<Longrightarrow> \<forall>y . y \<in> lang \<longrightarrow> x @ y \<in> lang\<star>"
-by (erule Star.induct, auto intro:star_intro2)
+lemma star_intro2: 
+  assumes a: "y \<in> A"
+  shows "y \<in> A\<star>"
+proof -
+  from a have "y @ [] \<in> A\<star>" by blast
+  then show "y \<in> A\<star>" by simp
+qed
+
+lemma star_intro3:
+  assumes a: "x \<in> A\<star>"
+  and     b: "y \<in> A"
+  shows "x @ y \<in> A\<star>"
+using a b by (blast intro: star_intro1 star_intro2)
 
 lemma star_decom: 
-  "\<lbrakk>x \<in> lang\<star>; x \<noteq> []\<rbrakk> \<Longrightarrow>(\<exists> a b. x = a @ b \<and> a \<noteq> [] \<and> a \<in> lang \<and> b \<in> lang\<star>)"
-by (induct x rule: Star.induct, simp, blast)
+  "\<lbrakk>x \<in> A\<star>; x \<noteq> []\<rbrakk> \<Longrightarrow>(\<exists> a b. x = a @ b \<and> a \<noteq> [] \<and> a \<in> A \<and> b \<in> A\<star>)"
+apply(induct rule: star_induct)
+apply(simp)
+apply(blast)
+done
 
 lemma lang_star_cases:
   shows "L\<star> =  {[]} \<union> L ;; L\<star>"
@@ -95,50 +141,14 @@
   { fix x
     have "x \<in> L\<star> \<Longrightarrow> x \<in> {[]} \<union> L ;; L\<star>"
       unfolding Seq_def
-    by (induct rule: Star.induct) (auto)
+    by (induct rule: star_induct) (auto)
   }
   then show "L\<star> \<subseteq> {[]} \<union> L ;; L\<star>" by auto
 next
-  show "{[]} \<union> L ;; L\<star> \<subseteq> L\<star>" 
+  show "{[]} \<union> L ;; L\<star> \<subseteq> L\<star>"
     unfolding Seq_def by auto
 qed
 
-fun 
-  pow :: "lang \<Rightarrow> nat \<Rightarrow> lang" (infixl "\<up>" 100)
-where
-  "A \<up> 0 = {[]}"
-| "A \<up> (Suc n) =  A ;; (A \<up> n)" 
-
-lemma star_pow_eq:
-  shows "A\<star> = (\<Union>n. A \<up> n)"
-proof -
-  { fix n x
-    assume "x \<in> (A \<up> n)"
-    then have "x \<in> A\<star>"
-      by (induct n arbitrary: x) (auto simp add: Seq_def)
-  }
-  moreover
-  { fix x
-    assume "x \<in> A\<star>"
-    then have "\<exists>n. x \<in> A \<up> n"
-    proof (induct rule: Star.induct)
-      case start
-      have "[] \<in> A \<up> 0" by auto
-      then show "\<exists>n. [] \<in> A \<up> n" by blast
-    next
-      case (step s1 s2)
-      have "s1 \<in> A" by fact
-      moreover
-      have "\<exists>n. s2 \<in> A \<up> n" by fact
-      then obtain n where "s2 \<in> A \<up> n" by blast
-      ultimately
-      have "s1 @ s2 \<in> A \<up> (Suc n)" by (auto simp add: Seq_def)
-      then show "\<exists>n. s1 @ s2 \<in> A \<up> n" by blast
-    qed
-  }
-  ultimately show "A\<star> = (\<Union>n. A \<up> n)" by auto
-qed
-
 lemma
   shows seq_Union_left:  "B ;; (\<Union>n. A \<up> n) = (\<Union>n. B ;; (A \<up> n))"
   and   seq_Union_right: "(\<Union>n. A \<up> n) ;; B = (\<Union>n. (A \<up> n) ;; B)"
@@ -150,7 +160,7 @@
 
 lemma seq_star_comm:
   shows "A ;; A\<star> = A\<star> ;; A"
-unfolding star_pow_eq
+unfolding Star_def
 unfolding seq_Union_left
 unfolding seq_pow_comm
 unfolding seq_Union_right 
@@ -226,8 +236,8 @@
   have "A\<star> = {[]} \<union> A\<star> ;; A" 
     unfolding seq_star_comm[symmetric]
     by (rule lang_star_cases)
-  then have "B ;; A\<star> = B ;; ({[]} \<union> A\<star> ;; A)" 
-    unfolding Seq_def by simp
+  then have "B ;; A\<star> = B ;; ({[]} \<union> A\<star> ;; A)"
+    by (rule seq_add_left)
   also have "\<dots> = B \<union> B ;; (A\<star> ;; A)"
     unfolding seq_union_distrib_left by simp
   also have "\<dots> = B \<union> (B ;; A\<star>) ;; A" 
@@ -238,8 +248,9 @@
   assume eq: "X = X ;; A \<union> B"
   { fix n::nat
     have "B ;; (A \<up> n) \<subseteq> X" using ardens_helper[OF eq, of "n"] by auto }
-  then have "B ;; A\<star> \<subseteq> X" unfolding star_pow_eq Seq_def
-    by (auto simp add: UNION_def)
+  then have "B ;; A\<star> \<subseteq> X" 
+    unfolding Seq_def Star_def UNION_def
+    by auto
   moreover
   { fix s::string
     obtain k where "k = length s" by auto
@@ -252,7 +263,8 @@
     moreover
     have "(\<Union>m\<in>{0..k}. B ;; (A \<up> m)) \<subseteq> (\<Union>n. B ;; (A \<up> n))" by auto
     ultimately 
-    have "s \<in> B ;; A\<star>" unfolding star_pow_eq seq_Union_left
+    have "s \<in> B ;; A\<star>" 
+      unfolding seq_Union_left Star_def
       by auto }
   then have "X \<subseteq> B ;; A\<star>" by auto
   ultimately