--- a/Myhill_2.thy	Fri Aug 19 20:39:07 2011 +0000
+++ b/Myhill_2.thy	Mon Aug 22 12:49:27 2011 +0000
@@ -1,9 +1,10 @@
 theory Myhill_2
-  imports Myhill_1 
-  "~~/src/HOL/Library/List_Prefix"
+  imports Myhill_1 "~~/src/HOL/Library/List_Prefix"
 begin
 
-section {* Direction @{text "regular language \<Rightarrow> finite partition"} *}
+section {* Second direction of MN: @{text "regular language \<Rightarrow> finite partition"} *}
+
+subsection {* Tagging functions *}
 
 definition 
    tag_eq :: "('a list \<Rightarrow> 'b) \<Rightarrow> ('a list \<times> 'a list) set" ("=_=")
@@ -115,9 +116,7 @@
 qed
 
 
-subsection {* The proof *}
-
-subsubsection {* The base case for @{const "Zero"} *}
+subsection {* Base cases: @{const Zero}, @{const One} and @{const Atom} *}
 
 lemma quot_zero_eq:
   shows "UNIV // \<approx>{} = {UNIV}"
@@ -128,8 +127,6 @@
 unfolding quot_zero_eq by simp
 
 
-subsubsection {* The base case for @{const "One"} *}
-
 lemma quot_one_subset:
   shows "UNIV // \<approx>{[]} \<subseteq> {{[]}, UNIV - {[]}}"
 proof
@@ -152,8 +149,6 @@
 by (rule finite_subset[OF quot_one_subset]) (simp)
 
 
-subsubsection {* The base case for @{const "Atom"} *}
-
 lemma quot_atom_subset:
   "UNIV // (\<approx>{[c]}) \<subseteq> {{[]},{[c]}, UNIV - {[], [c]}}"
 proof 
@@ -185,7 +180,7 @@
 by (rule finite_subset[OF quot_atom_subset]) (simp)
 
 
-subsubsection {* The inductive case for @{const Plus} *}
+subsection {* Case for @{const Plus} *}
 
 definition 
   tag_Plus :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a list \<Rightarrow> ('a lang \<times> 'a lang)"
@@ -208,7 +203,7 @@
 qed
 
 
-subsubsection {* The inductive case for @{text "Times"} *}
+subsection {* Case for @{text "Times"} *}
 
 definition
   "Partitions x \<equiv> {(x\<^isub>p, x\<^isub>s). x\<^isub>p @ x\<^isub>s = x}"
@@ -313,7 +308,7 @@
 qed
 
 
-subsubsection {* The inductive case for @{const "Star"} *}
+subsection {* Case for @{const "Star"} *}
 
 lemma star_partitions_elim:
   assumes "x @ z \<in> A\<star>" "x \<noteq> []"
@@ -463,16 +458,11 @@
        (auto simp add: quotient_def)
 qed
 
-subsubsection{* The conclusion *}
+subsection {* The conclusion of the second direction *}
 
 lemma Myhill_Nerode2:
   fixes r::"'a rexp"
   shows "finite (UNIV // \<approx>(lang r))"
 by (induct r) (auto)
 
-theorem Myhill_Nerode:
-  fixes A::"('a::finite) lang"
-  shows "(\<exists>r. A = lang r) \<longleftrightarrow> finite (UNIV // \<approx>A)"
-using Myhill_Nerode1 Myhill_Nerode2 by auto
-
 end
\ No newline at end of file