--- a/Myhill_1.thy	Fri Jan 28 19:17:40 2011 +0000
+++ b/Myhill_1.thy	Sat Jan 29 11:41:17 2011 +0000
@@ -82,6 +82,87 @@
 apply (simp, (erule exE| erule conjE)+)
 by (rule_tac x = "s1 @ a" in exI, rule_tac x = b in exI, simp add:step)
 
+
+text {* The syntax of regular expressions is defined by the datatype @{text "rexp"}. *}
+datatype rexp =
+  NULL
+| EMPTY
+| CHAR char
+| SEQ rexp rexp
+| ALT rexp rexp
+| STAR rexp
+
+
+text {* 
+  The following @{text "L"} is an overloaded operator, where @{text "L(x)"} evaluates to 
+  the language represented by the syntactic object @{text "x"}.
+*}
+consts L:: "'a \<Rightarrow> string set"
+
+
+text {* 
+  The @{text "L(rexp)"} for regular expression @{text "rexp"} is defined by the 
+  following overloading function @{text "L_rexp"}.
+*}
+overloading L_rexp \<equiv> "L::  rexp \<Rightarrow> string set"
+begin
+fun
+  L_rexp :: "rexp \<Rightarrow> string set"
+where
+    "L_rexp (NULL) = {}"
+  | "L_rexp (EMPTY) = {[]}"
+  | "L_rexp (CHAR c) = {[c]}"
+  | "L_rexp (SEQ r1 r2) = (L_rexp r1) ;; (L_rexp r2)"
+  | "L_rexp (ALT r1 r2) = (L_rexp r1) \<union> (L_rexp r2)"
+  | "L_rexp (STAR r) = (L_rexp r)\<star>"
+end
+
+(* Just a technical lemma. *)
+lemma [simp]:
+  shows "(x, y) \<in> {(x, y). P x y} \<longleftrightarrow> P x y"
+by simp
+
+text {*
+  @{text "\<approx>L"} is an equivalent class defined by language @{text "Lang"}.
+*}
+definition
+  str_eq_rel ("\<approx>_" [100] 100)
+where
+  "\<approx>Lang \<equiv> {(x, y).  (\<forall>z. x @ z \<in> Lang \<longleftrightarrow> y @ z \<in> Lang)}"
+
+text {* 
+  Among equivlant clases of @{text "\<approx>Lang"}, the set @{text "finals(Lang)"} singles out 
+  those which contains strings from @{text "Lang"}.
+*}
+
+definition 
+   "finals Lang \<equiv> {\<approx>Lang `` {x} | x . x \<in> Lang}"
+
+text {* 
+  The following lemma show the relationshipt between @{text "finals(Lang)"} and @{text "Lang"}.
+*}
+lemma lang_is_union_of_finals: 
+  "Lang = \<Union> finals(Lang)"
+proof 
+  show "Lang \<subseteq> \<Union> (finals Lang)"
+  proof
+    fix x
+    assume "x \<in> Lang"   
+    thus "x \<in> \<Union> (finals Lang)"
+      apply (simp add:finals_def, rule_tac x = "(\<approx>Lang) `` {x}" in exI)
+      by (auto simp:Image_def str_eq_rel_def)    
+  qed
+next
+  show "\<Union> (finals Lang) \<subseteq> Lang"
+    apply (clarsimp simp:finals_def str_eq_rel_def)
+    by (drule_tac x = "[]" in spec, auto)
+qed
+
+section {* Direction @{text "finite partition \<Rightarrow> regular language"}*}
+
+subsection {*
+  Ardens lemma
+  *}
 text {* Ardens lemma expressed at the level of language, rather than the level of regular expression. *}
 
 theorem ardens_revised:
@@ -144,40 +225,9 @@
   qed
 qed
 
-
-text {* The syntax of regular expressions is defined by the datatype @{text "rexp"}. *}
-datatype rexp =
-  NULL
-| EMPTY
-| CHAR char
-| SEQ rexp rexp
-| ALT rexp rexp
-| STAR rexp
-
-
-text {* 
-  The following @{text "L"} is an overloaded operator, where @{text "L(x)"} evaluates to 
-  the language represented by the syntactic object @{text "x"}.
-*}
-consts L:: "'a \<Rightarrow> string set"
-
-
-text {* 
-  The @{text "L(rexp)"} for regular expression @{text "rexp"} is defined by the 
-  following overloading function @{text "L_rexp"}.
-*}
-overloading L_rexp \<equiv> "L::  rexp \<Rightarrow> string set"
-begin
-fun
-  L_rexp :: "rexp \<Rightarrow> string set"
-where
-    "L_rexp (NULL) = {}"
-  | "L_rexp (EMPTY) = {[]}"
-  | "L_rexp (CHAR c) = {[c]}"
-  | "L_rexp (SEQ r1 r2) = (L_rexp r1) ;; (L_rexp r2)"
-  | "L_rexp (ALT r1 r2) = (L_rexp r1) \<union> (L_rexp r2)"
-  | "L_rexp (STAR r) = (L_rexp r)\<star>"
-end
+subsection {*
+  Defintions peculiar to this direction
+  *}
 
 text {*
   To obtain equational system out of finite set of equivalent classes, a fold operation
@@ -202,49 +252,6 @@
 apply (rule someI2_ex, erule finite_imp_fold_graph)
 by (erule fold_graph.induct, auto)
 
-(* Just a technical lemma. *)
-lemma [simp]:
-  shows "(x, y) \<in> {(x, y). P x y} \<longleftrightarrow> P x y"
-by simp
-
-text {*
-  @{text "\<approx>L"} is an equivalent class defined by language @{text "Lang"}.
-*}
-definition
-  str_eq_rel ("\<approx>_" [100] 100)
-where
-  "\<approx>Lang \<equiv> {(x, y).  (\<forall>z. x @ z \<in> Lang \<longleftrightarrow> y @ z \<in> Lang)}"
-
-text {* 
-  Among equivlant clases of @{text "\<approx>Lang"}, the set @{text "finals(Lang)"} singles out 
-  those which contains strings from @{text "Lang"}.
-*}
-
-definition 
-   "finals Lang \<equiv> {\<approx>Lang `` {x} | x . x \<in> Lang}"
-
-text {* 
-  The following lemma show the relationshipt between @{text "finals(Lang)"} and @{text "Lang"}.
-*}
-lemma lang_is_union_of_finals: 
-  "Lang = \<Union> finals(Lang)"
-proof 
-  show "Lang \<subseteq> \<Union> (finals Lang)"
-  proof
-    fix x
-    assume "x \<in> Lang"   
-    thus "x \<in> \<Union> (finals Lang)"
-      apply (simp add:finals_def, rule_tac x = "(\<approx>Lang) `` {x}" in exI)
-      by (auto simp:Image_def str_eq_rel_def)    
-  qed
-next
-  show "\<Union> (finals Lang) \<subseteq> Lang"
-    apply (clarsimp simp:finals_def str_eq_rel_def)
-    by (drule_tac x = "[]" in spec, auto)
-qed
-
-section {* Direction @{text "finite partition \<Rightarrow> regular language"}*}
-
 text {* 
   The relationship between equivalent classes can be described by an
   equational system.