diff -r ecf6c61a4541 -r 8ab3a06577cf Myhill_1.thy
--- a/Myhill_1.thy	Sun Feb 06 10:28:29 2011 +0000
+++ b/Myhill_1.thy	Sun Feb 06 11:21:12 2011 +0000
@@ -28,15 +28,14 @@
 
 types lang = "string set"
 
-text {* 
-  Sequential composition of two languages @{text "L1"} and @{text "L2"} 
-*}
+text {*  Sequential composition of two languages *}
 
 definition 
   Seq :: "lang \<Rightarrow> lang \<Rightarrow> lang" (infixr ";;" 100)
 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 {* Some properties of operator @{text ";;"}. *}
 
 lemma seq_add_left:
@@ -53,8 +52,9 @@
 unfolding Seq_def by  auto
 
 lemma seq_intro:
-  "\<lbrakk>x \<in> A; y \<in> B\<rbrakk> \<Longrightarrow> x @ y \<in> A ;; B "
-by (auto simp:Seq_def)
+  assumes a: "x \<in> A" "y \<in> B"
+  shows "x @ y \<in> A ;; B "
+using a by (auto simp: Seq_def)
 
 lemma seq_assoc:
   shows "(A ;; B) ;; C = A ;; (B ;; C)"
@@ -68,6 +68,9 @@
   and   "{[]} ;; A = A"
 by (simp_all add: Seq_def)
 
+
+text {* Power and Star of a language *}
+
 fun 
   pow :: "lang \<Rightarrow> nat \<Rightarrow> lang" (infixl "\<up>" 100)
 where
@@ -79,6 +82,7 @@
 where
   "A\<star> \<equiv> (\<Union>n. A \<up> n)"
 
+
 lemma star_start[intro]:
   shows "[] \<in> A\<star>"
 proof -
@@ -205,10 +209,8 @@
 
 section {* A slightly modified version of Arden's lemma *}
 
-text {* 
-  Arden's lemma expressed at the level of languages, rather 
-  than the level of regular expression. 
-*}
+
+text {*  A helper lemma for Arden *}
 
 lemma ardens_helper:
   assumes eq: "X = X ;; A \<union> B"
@@ -272,8 +274,8 @@
 qed
 
 
+section {* Regular Expressions *}
 
-text {* The syntax of regular expressions is defined by the datatype @{text "rexp"}. *}
 datatype rexp =
   NULL
 | EMPTY
@@ -287,14 +289,12 @@
   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"
 
+consts L:: "'a \<Rightarrow> lang"
 
-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"
+text {* The @{text "L (rexp)"} for regular expressions. *}
+
+overloading L_rexp \<equiv> "L::  rexp \<Rightarrow> lang"
 begin
 fun
   L_rexp :: "rexp \<Rightarrow> string set"
@@ -307,10 +307,13 @@
   | "L_rexp (STAR r) = (L_rexp r)\<star>"
 end
 
+
+section {* Folds for Sets *}
+
 text {*
-  To obtain equational system out of finite set of equivalent classes, a fold operation
-  on finite set @{text "folds"} is defined. The use of @{text "SOME"} makes @{text "fold"}
-  more robust than the @{text "fold"} in Isabelle library. The expression @{text "folds f"}
+  To obtain equational system out of finite set of equivalence classes, a fold operation
+  on finite sets @{text "folds"} is defined. The use of @{text "SOME"} makes @{text "folds"}
+  more robust than the @{text "fold"} in the Isabelle library. The expression @{text "folds f"}
   makes sense when @{text "f"} is not @{text "associative"} and @{text "commutitive"},
   while @{text "fold f"} does not.  
 *}
@@ -321,109 +324,126 @@
   "folds f z S \<equiv> SOME x. fold_graph f z S x"
 
 text {* 
-  The following lemma assures that the arbitrary choice made by the @{text "SOME"} in @{text "folds"}
-  does not affect the @{text "L"}-value of the resultant regular expression. 
+  The following lemma ensures that the arbitrary choice made by the 
+  @{text "SOME"} in @{text "folds"} does not affect the @{text "L"}-value 
+  of the resultant regular expression. 
   *}
+
 lemma folds_alt_simp [simp]:
-  "finite rs \<Longrightarrow> L (folds ALT NULL rs) = \<Union> (L ` rs)"
-apply (rule set_eq_intro, simp add:folds_def)
-apply (rule someI2_ex, erule finite_imp_fold_graph)
-by (erule fold_graph.induct, auto)
+  assumes a: "finite rs"
+  shows "L (folds ALT NULL rs) = \<Union> (L ` rs)"
+apply(rule set_eq_intro)
+apply(simp add: folds_def)
+apply(rule someI2_ex)
+apply(rule_tac finite_imp_fold_graph[OF a])
+apply(erule fold_graph.induct)
+apply(auto)
+done
 
-(* Just a technical lemma. *)
+
+text {* Just a technical lemma for collections and pairs *}
+
 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"}.
+  @{text "\<approx>A"} is an equivalence class defined by language @{text "A"}.
 *}
 definition
   str_eq_rel ("\<approx>_" [100] 100)
 where
-  "\<approx>Lang \<equiv> {(x, y).  (\<forall>z. x @ z \<in> Lang \<longleftrightarrow> y @ z \<in> Lang)}"
+  "\<approx>A \<equiv> {(x, y).  (\<forall>z. x @ z \<in> A \<longleftrightarrow> y @ z \<in> A)}"
 
 text {* 
-  Among equivlant clases of @{text "\<approx>Lang"}, the set @{text "finals(Lang)"} singles out 
-  those which contains strings from @{text "Lang"}.
+  Among the equivalence clases of @{text "\<approx>A"}, the set @{text "finals A"} singles out 
+  those which contains the strings from @{text "A"}.
 *}
 
 definition 
-   "finals Lang \<equiv> {\<approx>Lang `` {x} | x . x \<in> Lang}"
+   "finals A \<equiv> {\<approx>A `` {x} | x . x \<in> A}"
 
 text {* 
-  The following lemma show the relationshipt between @{text "finals(Lang)"} and @{text "Lang"}.
+  The following lemma establishes the relationshipt between 
+  @{text "finals A"} and @{text "A"}.
 *}
+
 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
+  shows "A = \<Union> finals A"
+unfolding finals_def
+unfolding Image_def
+unfolding str_eq_rel_def
+apply(auto)
+apply(drule_tac x = "[]" in spec)
+apply(auto)
+done
+
 
 section {* Direction @{text "finite partition \<Rightarrow> regular language"}*}
 
 text {* 
   The relationship between equivalent classes can be described by an
-  equational system.
-  For example, in equational system \eqref{example_eqns},  $X_0, X_1$ are equivalent 
-  classes. The first equation says every string in $X_0$ is obtained either by
-  appending one $b$ to a string in $X_0$ or by appending one $a$ to a string in
-  $X_1$ or just be an empty string (represented by the regular expression $\lambda$). Similary,
-  the second equation tells how the strings inside $X_1$ are composed.
+  equational system.  For example, in equational system \eqref{example_eqns},
+  $X_0, X_1$ are equivalent classes. The first equation says every string in
+  $X_0$ is obtained either by appending one $b$ to a string in $X_0$ or by
+  appending one $a$ to a string in $X_1$ or just be an empty string
+  (represented by the regular expression $\lambda$). Similary, the second
+  equation tells how the strings inside $X_1$ are composed.
+
   \begin{equation}\label{example_eqns}
     \begin{aligned}
       X_0 & = X_0 b + X_1 a + \lambda \\
       X_1 & = X_0 a + X_1 b
     \end{aligned}
   \end{equation}
-  The summands on the right hand side is represented by the following data type
-  @{text "rhs_item"}, mnemonic for 'right hand side item'.
-  Generally, there are two kinds of right hand side items, one kind corresponds to
-  pure regular expressions, like the $\lambda$ in \eqref{example_eqns}, the other kind corresponds to
-  transitions from one one equivalent class to another, like the $X_0 b, X_1 a$ etc.
-  *}
+
+  \noindent
+  The summands on the right hand side is represented by the following data
+  type @{text "rhs_item"}, mnemonic for 'right hand side item'.  Generally,
+  there are two kinds of right hand side items, one kind corresponds to pure
+  regular expressions, like the $\lambda$ in \eqref{example_eqns}, the other
+  kind corresponds to transitions from one one equivalent class to another,
+  like the $X_0 b, X_1 a$ etc.
+
+*}
 
 datatype rhs_item = 
-   Lam "rexp"                           (* Lambda *)
- | Trn "(string set)" "rexp"              (* Transition *)
+   Lam "rexp"            (* Lambda *)
+ | Trn "lang" "rexp"     (* Transition *)
+
 
 text {*
   In this formalization, pure regular expressions like $\lambda$ is 
-  repsented by @{text "Lam(EMPTY)"}, while transitions like $X_0 a$ is represented by $Trn~X_0~(CHAR~a)$.
-  *}
+  repsented by @{text "Lam(EMPTY)"}, while transitions like $X_0 a$ is 
+  represented by @{term "Trn X\<^isub>0 (CHAR a)"}.
+*}
 
 text {*
   The functions @{text "the_r"} and @{text "the_Trn"} are used to extract
   subcomponents from right hand side items.
   *}
 
-fun the_r :: "rhs_item \<Rightarrow> rexp"
-where "the_r (Lam r) = r"
+fun 
+  the_r :: "rhs_item \<Rightarrow> rexp"
+where 
+  "the_r (Lam r) = r"
 
-fun the_Trn:: "rhs_item \<Rightarrow> (string set \<times> rexp)"
-where "the_Trn (Trn Y r) = (Y, r)"
+fun 
+  the_Trn:: "rhs_item \<Rightarrow> (lang \<times> rexp)"
+where 
+  "the_Trn (Trn Y r) = (Y, r)"
 
 text {*
-  Every right hand side item @{text "itm"} defines a string set given 
-  @{text "L(itm)"}, defined as:
+  Every right-hand side item @{text "itm"} defines a language given 
+  by @{text "L(itm)"}, defined as:
 *}
-overloading L_rhs_e \<equiv> "L:: rhs_item \<Rightarrow> string set"
+
+overloading L_rhs_e \<equiv> "L:: rhs_item \<Rightarrow> lang"
 begin
-  fun L_rhs_e:: "rhs_item \<Rightarrow> string set"
+  fun L_rhs_e:: "rhs_item \<Rightarrow> lang"
   where
-     "L_rhs_e (Lam r) = L r" |
-     "L_rhs_e (Trn X r) = X ;; L r"
+    "L_rhs_e (Lam r) = L r" 
+  | "L_rhs_e (Trn X r) = X ;; L r"
 end
 
 text {*
@@ -432,14 +452,15 @@
   by @{text "L(itms)"}, defined as:
 *}
 
-overloading L_rhs \<equiv> "L:: rhs_item set \<Rightarrow> string set"
+overloading L_rhs \<equiv> "L:: rhs_item set \<Rightarrow> lang"
 begin
-   fun L_rhs:: "rhs_item set \<Rightarrow> string set"
-   where "L_rhs rhs = \<Union> (L ` rhs)"
+   fun L_rhs:: "rhs_item set \<Rightarrow> lang"
+   where 
+     "L_rhs rhs = \<Union> (L ` rhs)"
 end
 
 text {* 
-  Given a set of equivalent classses @{text "CS"} and one equivalent class @{text "X"} among
+  Given a set of equivalence classes @{text "CS"} and one equivalence class @{text "X"} among
   @{text "CS"}, the term @{text "init_rhs CS X"} is used to extract the right hand side of
   the equation describing the formation of @{text "X"}. The definition of @{text "init_rhs"}
   is:
@@ -464,12 +485,14 @@
   equivalent class inside @{text "CS"} is given by the following @{text "eqs(CS)"}.
   *}
 
+
 definition "eqs CS \<equiv> {(X, init_rhs CS X) | X.  X \<in> CS}"
 (************ arden's lemma variation ********************)
 
 text {* 
   The following @{text "items_of rhs X"} returns all @{text "X"}-items in @{text "rhs"}.
   *}
+
 definition
   "items_of rhs X \<equiv> {Trn X r | r. (Trn X r) \<in> rhs}"
 
@@ -505,7 +528,8 @@
   the right of right hand side item @{text "itm"}.
   *}
 
-fun attach_rexp :: "rexp \<Rightarrow> rhs_item \<Rightarrow> rhs_item"
+fun 
+  attach_rexp :: "rexp \<Rightarrow> rhs_item \<Rightarrow> rhs_item"
 where
   "attach_rexp rexp' (Lam rexp)   = Lam (SEQ rexp rexp')"
 | "attach_rexp rexp' (Trn X rexp) = Trn X (SEQ rexp rexp')"
@@ -541,6 +565,7 @@
   should be: first append $(a_1 | a_2 | \ldots | a_n)$ to every item of @{text "xrhs"} and then
   union the result with all non-@{text "X"}-items of @{text "rhs"}.
  *}
+
 definition 
   "rhs_subst rhs X xrhs \<equiv> 
         (rhs - (items_of rhs X)) \<union> (append_rhs_rexp xrhs (rexp_of rhs X))"
@@ -599,6 +624,7 @@
 definition 
   "distinct_equas ES \<equiv> 
             \<forall> X rhs rhs'. (X, rhs) \<in> ES \<and> (X, rhs') \<in> ES \<longrightarrow> rhs = rhs'"
+
 text {* 
   Every equation in @{text "ES"} (represented by @{text "(X, rhs)"}) is valid, i.e. @{text "(X = L rhs)"}.
   *}
@@ -610,6 +636,7 @@
   items of @{text "rhs"} does not contain empty string. This is necessary for
   the application of Arden's transformation to @{text "rhs"}.
   *}
+
 definition 
   "rhs_nonempty rhs \<equiv> (\<forall> Y r. Trn Y r \<in> rhs \<longrightarrow> [] \<notin> L r)"
 
@@ -617,6 +644,7 @@
   The following @{text "ardenable ES"} requires that Arden's transformation is applicable
   to every equation of equational system @{text "ES"}.
   *}
+
 definition 
   "ardenable ES \<equiv> \<forall> X rhs. (X, rhs) \<in> ES \<longrightarrow> rhs_nonempty rhs"
 
@@ -669,7 +697,8 @@
 *}
 
 lemma L_rhs_union_distrib:
-  " L (A::rhs_item set) \<union> L B = L (A \<union> B)"
+  fixes A B::"rhs_item set"
+  shows "L A \<union> L B = L (A \<union> B)"
 by simp
 
 lemma finite_snd_Trn:
@@ -717,7 +746,7 @@
 qed
 
 lemma [simp]:
-  " L (attach_rexp r xb) = L xb ;; L r"
+  "L (attach_rexp r xb) = L xb ;; L r"
 apply (cases xb, auto simp:Seq_def)
 apply(rule_tac x = "s\<^isub>1 @ s\<^isub>1'" in exI, rule_tac x = "s\<^isub>2'" in exI)
 apply(auto simp: Seq_def)
@@ -1221,31 +1250,33 @@
 qed
 
 lemma finals_in_partitions:
-  "finals Lang \<subseteq> (UNIV // (\<approx>Lang))"
-  by (auto simp:finals_def quotient_def)   
+  shows "finals A \<subseteq> (UNIV // \<approx>A)"
+unfolding finals_def
+unfolding quotient_def
+by auto
 
 theorem hard_direction: 
-  assumes finite_CS: "finite (UNIV // \<approx>Lang)"
-  shows   "\<exists> (r::rexp). Lang = L r"
+  assumes finite_CS: "finite (UNIV // \<approx>A)"
+  shows   "\<exists>r::rexp. A = L r"
 proof -
-  have "\<forall> X \<in> (UNIV // (\<approx>Lang)). \<exists> (reg::rexp). X = L reg" 
+  have "\<forall> X \<in> (UNIV // \<approx>A). \<exists>reg::rexp. X = L reg" 
     using finite_CS every_eqcl_has_reg by blast
   then obtain f 
-    where f_prop: "\<forall> X \<in> (UNIV // (\<approx>Lang)). X = L ((f X)::rexp)" 
-    by (auto dest:bchoice)
-  def rs \<equiv> "f ` (finals Lang)"  
-  have "Lang = \<Union> (finals Lang)" using lang_is_union_of_finals by auto
+    where f_prop: "\<forall> X \<in> (UNIV // \<approx>A). X = L ((f X)::rexp)"
+    by (auto dest: bchoice)
+  def rs \<equiv> "f ` (finals A)"  
+  have "A = \<Union> (finals A)" using lang_is_union_of_finals by auto
   also have "\<dots> = L (folds ALT NULL rs)" 
   proof -
     have "finite rs"
     proof -
-      have "finite (finals Lang)" 
-        using finite_CS finals_in_partitions[of "Lang"]   
+      have "finite (finals A)" 
+        using finite_CS finals_in_partitions[of "A"]   
         by (erule_tac finite_subset, simp)
       thus ?thesis using rs_def by auto
     qed
     thus ?thesis 
-      using f_prop rs_def finals_in_partitions[of "Lang"] by auto
+      using f_prop rs_def finals_in_partitions[of "A"] by auto
   qed
   finally show ?thesis by blast
 qed