diff -r b794db0b79db -r b1258b7d2789 Myhill_2.thy
--- a/Myhill_2.thy	Fri Jun 03 13:59:21 2011 +0000
+++ b/Myhill_2.thy	Mon Jul 25 13:33:38 2011 +0000
@@ -6,7 +6,7 @@
 section {* Direction @{text "regular language \<Rightarrow> finite partition"} *}
 
 definition
-  str_eq :: "string \<Rightarrow> lang \<Rightarrow> string \<Rightarrow> bool" ("_ \<approx>_ _")
+  str_eq :: "'a list \<Rightarrow> 'a lang \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<approx>_ _")
 where
   "x \<approx>A y \<equiv> (x, y) \<in> (\<approx>A)"
 
@@ -16,7 +16,7 @@
 by simp
 
 definition 
-   tag_eq_rel :: "(string \<Rightarrow> 'b) \<Rightarrow> (string \<times> string) set" ("=_=")
+   tag_eq_rel :: "('a list \<Rightarrow> 'b) \<Rightarrow> ('a list \<times> 'a list) set" ("=_=")
 where
    "=tag= \<equiv> {(x, y). tag x = tag y}"
 
@@ -116,20 +116,20 @@
 
 subsection {* The proof *}
 
-subsubsection {* The base case for @{const "NULL"} *}
+subsubsection {* The base case for @{const "Zero"} *}
 
-lemma quot_null_eq:
+lemma quot_zero_eq:
   shows "UNIV // \<approx>{} = {UNIV}"
 unfolding quotient_def Image_def str_eq_rel_def by auto
 
-lemma quot_null_finiteI [intro]:
+lemma quot_zero_finiteI [intro]:
   shows "finite (UNIV // \<approx>{})"
-unfolding quot_null_eq by simp
+unfolding quot_zero_eq by simp
 
 
-subsubsection {* The base case for @{const "EMPTY"} *}
+subsubsection {* The base case for @{const "One"} *}
 
-lemma quot_empty_subset:
+lemma quot_one_subset:
   shows "UNIV // \<approx>{[]} \<subseteq> {{[]}, UNIV - {[]}}"
 proof
   fix x
@@ -148,14 +148,14 @@
   qed
 qed
 
-lemma quot_empty_finiteI [intro]:
+lemma quot_one_finiteI [intro]:
   shows "finite (UNIV // \<approx>{[]})"
-by (rule finite_subset[OF quot_empty_subset]) (simp)
+by (rule finite_subset[OF quot_one_subset]) (simp)
 
 
-subsubsection {* The base case for @{const "CHAR"} *}
+subsubsection {* The base case for @{const "Atom"} *}
 
-lemma quot_char_subset:
+lemma quot_atom_subset:
   "UNIV // (\<approx>{[c]}) \<subseteq> {{[]},{[c]}, UNIV - {[], [c]}}"
 proof 
   fix x 
@@ -181,43 +181,43 @@
   qed
 qed
 
-lemma quot_char_finiteI [intro]:
+lemma quot_atom_finiteI [intro]:
   shows "finite (UNIV // \<approx>{[c]})"
-by (rule finite_subset[OF quot_char_subset]) (simp)
+by (rule finite_subset[OF quot_atom_subset]) (simp)
 
 
-subsubsection {* The inductive case for @{const ALT} *}
+subsubsection {* The inductive case for @{const Plus} *}
 
 definition 
-  tag_str_ALT :: "lang \<Rightarrow> lang \<Rightarrow> string \<Rightarrow> (lang \<times> lang)"
+  tag_str_Plus :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a list \<Rightarrow> ('a lang \<times> 'a lang)"
 where
-  "tag_str_ALT A B \<equiv> (\<lambda>x. (\<approx>A `` {x}, \<approx>B `` {x}))"
+  "tag_str_Plus A B \<equiv> (\<lambda>x. (\<approx>A `` {x}, \<approx>B `` {x}))"
 
 lemma quot_union_finiteI [intro]:
   assumes finite1: "finite (UNIV // \<approx>A)"
   and     finite2: "finite (UNIV // \<approx>B)"
   shows "finite (UNIV // \<approx>(A \<union> B))"
-proof (rule_tac tag = "tag_str_ALT A B" in tag_finite_imageD)
+proof (rule_tac tag = "tag_str_Plus A B" in tag_finite_imageD)
   have "finite ((UNIV // \<approx>A) \<times> (UNIV // \<approx>B))" 
     using finite1 finite2 by auto
-  then show "finite (range (tag_str_ALT A B))"
-    unfolding tag_str_ALT_def quotient_def
+  then show "finite (range (tag_str_Plus A B))"
+    unfolding tag_str_Plus_def quotient_def
     by (rule rev_finite_subset) (auto)
 next
-  show "\<And>x y. tag_str_ALT A B x = tag_str_ALT A B y \<Longrightarrow> x \<approx>(A \<union> B) y"
-    unfolding tag_str_ALT_def
+  show "\<And>x y. tag_str_Plus A B x = tag_str_Plus A B y \<Longrightarrow> x \<approx>(A \<union> B) y"
+    unfolding tag_str_Plus_def
     unfolding str_eq_def
     unfolding str_eq_rel_def
     by auto
 qed
 
 
-subsubsection {* The inductive case for @{text "SEQ"}*}
+subsubsection {* The inductive case for @{text "Times"}*}
 
 definition 
-  tag_str_SEQ :: "lang \<Rightarrow> lang \<Rightarrow> string \<Rightarrow> (lang \<times> lang set)"
+  tag_str_Times :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a list \<Rightarrow> ('a lang \<times> 'a lang set)"
 where
-  "tag_str_SEQ L1 L2 \<equiv>
+  "tag_str_Times L1 L2 \<equiv>
      (\<lambda>x. (\<approx>L1 `` {x}, {(\<approx>L2 `` {x - xa}) | xa.  xa \<le> x \<and> xa \<in> L1}))"
 
 lemma Seq_in_cases:
@@ -225,16 +225,16 @@
   shows "(\<exists> x' \<le> x. x' \<in> A \<and> (x - x') @ z \<in> B) \<or> 
          (\<exists> z' \<le> z. (x @ z') \<in> A \<and> (z - z') \<in> B)"
 using assms
-unfolding Seq_def prefix_def
+unfolding conc_def prefix_def
 by (auto simp add: append_eq_append_conv2)
 
-lemma tag_str_SEQ_injI:
-  assumes eq_tag: "tag_str_SEQ A B x = tag_str_SEQ A B y" 
+lemma tag_str_Times_injI:
+  assumes eq_tag: "tag_str_Times A B x = tag_str_Times A B y" 
   shows "x \<approx>(A \<cdot> B) y"
 proof -
   { fix x y z
     assume xz_in_seq: "x @ z \<in> A \<cdot> B"
-    and tag_xy: "tag_str_SEQ A B x = tag_str_SEQ A B y"
+    and tag_xy: "tag_str_Times A B x = tag_str_Times A B y"
     have"y @ z \<in> A \<cdot> B" 
     proof -
       { (* first case with x' in A and (x - x') @ z in B *)
@@ -247,7 +247,7 @@
         proof -
           have "{\<approx>B `` {x - x'} |x'. x' \<le> x \<and> x' \<in> A} = 
                 {\<approx>B `` {y - y'} |y'. y' \<le> y \<and> y' \<in> A}" (is "?Left = ?Right")
-            using tag_xy unfolding tag_str_SEQ_def by simp
+            using tag_xy unfolding tag_str_Times_def by simp
           moreover 
 	  have "\<approx>B `` {x - x'} \<in> ?Left" using h1 h2 by auto
           ultimately 
@@ -271,11 +271,11 @@
         fix z'
         assume h1: "z' \<le> z" and h2: "(x @ z') \<in> A" and h3: "z - z' \<in> B"
 	 have "\<approx>A `` {x} = \<approx>A `` {y}" 
-           using tag_xy unfolding tag_str_SEQ_def by simp
+           using tag_xy unfolding tag_str_Times_def by simp
          with h2 have "y @ z' \<in> A"
             unfolding Image_def str_eq_rel_def str_eq_def by auto
         with h1 h3 have "y @ z \<in> A \<cdot> B"
-	  unfolding prefix_def Seq_def
+	  unfolding prefix_def conc_def
 	  by (auto) (metis append_assoc)
       }
       ultimately show "y @ z \<in> A \<cdot> B" 
@@ -287,30 +287,30 @@
 qed 
 
 lemma quot_seq_finiteI [intro]:
-  fixes L1 L2::"lang"
+  fixes L1 L2::"'a lang"
   assumes fin1: "finite (UNIV // \<approx>L1)" 
   and     fin2: "finite (UNIV // \<approx>L2)" 
   shows "finite (UNIV // \<approx>(L1 \<cdot> L2))"
-proof (rule_tac tag = "tag_str_SEQ L1 L2" in tag_finite_imageD)
-  show "\<And>x y. tag_str_SEQ L1 L2 x = tag_str_SEQ L1 L2 y \<Longrightarrow> x \<approx>(L1 \<cdot> L2) y"
-    by (rule tag_str_SEQ_injI)
+proof (rule_tac tag = "tag_str_Times L1 L2" in tag_finite_imageD)
+  show "\<And>x y. tag_str_Times L1 L2 x = tag_str_Times L1 L2 y \<Longrightarrow> x \<approx>(L1 \<cdot> L2) y"
+    by (rule tag_str_Times_injI)
 next
   have *: "finite ((UNIV // \<approx>L1) \<times> (Pow (UNIV // \<approx>L2)))" 
     using fin1 fin2 by auto
-  show "finite (range (tag_str_SEQ L1 L2))" 
-    unfolding tag_str_SEQ_def
+  show "finite (range (tag_str_Times L1 L2))" 
+    unfolding tag_str_Times_def
     apply(rule finite_subset[OF _ *])
     unfolding quotient_def
     by auto
 qed
 
 
-subsubsection {* The inductive case for @{const "STAR"} *}
+subsubsection {* The inductive case for @{const "Star"} *}
 
 definition 
-  tag_str_STAR :: "lang \<Rightarrow> string \<Rightarrow> lang set"
+  tag_str_Star :: "'a lang \<Rightarrow> 'a list \<Rightarrow> ('a lang) set"
 where
-  "tag_str_STAR L1 \<equiv> (\<lambda>x. {\<approx>L1 `` {x - xa} | xa. xa < x \<and> xa \<in> L1\<star>})"
+  "tag_str_Star L1 \<equiv> (\<lambda>x. {\<approx>L1 `` {x - xa} | xa. xa < x \<and> xa \<in> L1\<star>})"
 
 text {* A technical lemma. *}
 lemma finite_set_has_max: "\<lbrakk>finite A; A \<noteq> {}\<rbrakk> \<Longrightarrow> 
@@ -342,31 +342,33 @@
 
 text {* The following is a technical lemma, which helps to show the range finiteness of tag function. *}
 
-lemma finite_strict_prefix_set: "finite {xa. xa < (x::string)}"
+lemma finite_strict_prefix_set: 
+  shows "finite {xa. xa < (x::'a list)}"
 apply (induct x rule:rev_induct, simp)
 apply (subgoal_tac "{xa. xa < xs @ [x]} = {xa. xa < xs} \<union> {xs}")
 by (auto simp:strict_prefix_def)
 
 
-lemma tag_str_STAR_injI:
-  assumes eq_tag: "tag_str_STAR L\<^isub>1 v = tag_str_STAR L\<^isub>1 w"
+lemma tag_str_Star_injI:
+  fixes L\<^isub>1::"('a::finite) lang"
+  assumes eq_tag: "tag_str_Star L\<^isub>1 v = tag_str_Star L\<^isub>1 w"
   shows "v \<approx>(L\<^isub>1\<star>) w"
 proof-
   { fix x y z
     assume xz_in_star: "x @ z \<in> L\<^isub>1\<star>" 
-      and tag_xy: "tag_str_STAR L\<^isub>1 x = tag_str_STAR L\<^isub>1 y"
+      and tag_xy: "tag_str_Star L\<^isub>1 x = tag_str_Star L\<^isub>1 y"
     have "y @ z \<in> L\<^isub>1\<star>"
     proof(cases "x = []")
       case True
       with tag_xy have "y = []" 
-        by (auto simp add: tag_str_STAR_def strict_prefix_def)
+        by (auto simp add: tag_str_Star_def strict_prefix_def)
       thus ?thesis using xz_in_star True by simp
     next
       case False
-      let ?S = "{xa. xa < x \<and> xa \<in> L\<^isub>1\<star> \<and> (x - xa) @ z \<in> L\<^isub>1\<star>}"
+      let ?S = "{xa::('a::finite) list. xa < x \<and> xa \<in> L\<^isub>1\<star> \<and> (x - xa) @ z \<in> L\<^isub>1\<star>}"
       have "finite ?S"
-        by (rule_tac B = "{xa. xa < x}" in finite_subset, 
-          auto simp:finite_strict_prefix_set)
+	by (rule_tac B = "{xa. xa < x}" in finite_subset)
+	   (auto simp: finite_strict_prefix_set)
       moreover have "?S \<noteq> {}" using False xz_in_star
         by (simp, rule_tac x = "[]" in exI, auto simp:strict_prefix_def)
       ultimately have "\<exists> xa_max \<in> ?S. \<forall> xa \<in> ?S. length xa \<le> length xa_max" 
@@ -384,7 +386,7 @@
       proof-
         from tag_xy have "{\<approx>L\<^isub>1 `` {x - xa} |xa. xa < x \<and> xa \<in> L\<^isub>1\<star>} = 
           {\<approx>L\<^isub>1 `` {y - xa} |xa. xa < y \<and> xa \<in> L\<^isub>1\<star>}" (is "?left = ?right")
-          by (auto simp:tag_str_STAR_def)
+          by (auto simp:tag_str_Star_def)
         moreover have "\<approx>L\<^isub>1 `` {x - xa_max} \<in> ?left" using h1 h2 by auto
         ultimately have "\<approx>L\<^isub>1 `` {x - xa_max} \<in> ?right" by simp
         thus ?thesis using that 
@@ -417,7 +419,7 @@
                 have "?xa_max' < x" 
                   using np h1 by (clarsimp simp:strict_prefix_def diff_prefix) 
                 moreover have "?xa_max' \<in> L\<^isub>1\<star>" 
-                  using a_in h2 by (simp add:star_intro3) 
+                  using a_in h2 by (auto)
                 moreover have "(x - ?xa_max') @ z \<in> L\<^isub>1\<star>" 
                   using b_eqs b_in np h1 by (simp add:diff_diff_append)
                 moreover have "\<not> (length ?xa_max' \<le> length xa_max)" 
@@ -432,11 +434,12 @@
            with eq_z and b_in 
           show ?thesis using that by blast
         qed
-        have "((y - ya) @ za) @ zb \<in> L\<^isub>1\<star>" using  l_za ls_zb by blast
+        have "((y - ya) @ za) @ zb \<in> L\<^isub>1\<star>" using  l_za ls_zb 
+	  by (rule_tac append_in_starI) (auto)
         with eq_zab show ?thesis by simp
       qed
-      with h5 h6 show ?thesis 
-        by (drule_tac star_intro1) (auto simp:strict_prefix_def elim: prefixE)
+      with h5 h6 show ?thesis 	
+        by (auto simp:strict_prefix_def elim: prefixE)
     qed
   } 
   from this [OF _ eq_tag] and this [OF _ eq_tag [THEN sym]]
@@ -444,16 +447,17 @@
 qed
 
 lemma quot_star_finiteI [intro]:
+   fixes A::"('a::finite) lang"
   assumes finite1: "finite (UNIV // \<approx>A)"
   shows "finite (UNIV // \<approx>(A\<star>))"
-proof (rule_tac tag = "tag_str_STAR A" in tag_finite_imageD)
-  show "\<And>x y. tag_str_STAR A x = tag_str_STAR A y \<Longrightarrow> x \<approx>(A\<star>) y"
-    by (rule tag_str_STAR_injI)
+proof (rule_tac tag = "tag_str_Star A" in tag_finite_imageD)
+  show "\<And>x y. tag_str_Star A x = tag_str_Star A y \<Longrightarrow> x \<approx>(A\<star>) y"
+    by (rule tag_str_Star_injI)
 next
   have *: "finite (Pow (UNIV // \<approx>A))" 
     using finite1 by auto
-  show "finite (range (tag_str_STAR A))"
-    unfolding tag_str_STAR_def
+  show "finite (range (tag_str_Star A))"
+    unfolding tag_str_Star_def
     apply(rule finite_subset[OF _ *])
     unfolding quotient_def
     by auto
@@ -462,12 +466,13 @@
 subsubsection{* The conclusion *}
 
 lemma Myhill_Nerode2:
-  shows "finite (UNIV // \<approx>(L_rexp r))"
+  fixes r::"('a::finite) rexp"
+  shows "finite (UNIV // \<approx>(lang r))"
 by (induct r) (auto)
 
-
 theorem Myhill_Nerode:
-  shows "(\<exists>r. A = L_rexp r) \<longleftrightarrow> finite (UNIV // \<approx>A)"
+  fixes A::"('a::finite) lang"
+  shows "(\<exists>r. A = lang r) \<longleftrightarrow> finite (UNIV // \<approx>A)"
 using Myhill_Nerode1 Myhill_Nerode2 by auto
 
 end