--- a/Myhill_1.thy	Tue Feb 08 12:01:28 2011 +0000
+++ b/Myhill_1.thy	Tue Feb 08 15:50:26 2011 +0000
@@ -335,7 +335,7 @@
   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]:
   assumes a: "finite rs"
@@ -388,13 +388,12 @@
 apply(auto)
 done
 
-lemma finals_included_in_UNIV:
-  shows "finals A \<subseteq> UNIV // \<approx>A"
+lemma finals_in_partitions:
+  shows "finals A \<subseteq> (UNIV // \<approx>A)"
 unfolding finals_def
 unfolding quotient_def
 by auto
 
-
 section {* Direction @{text "finite partition \<Rightarrow> regular language"}*}
 
 text {* 
@@ -445,9 +444,9 @@
   "the_r (Lam r) = r"
 
 fun 
-  the_Trn:: "rhs_item \<Rightarrow> (lang \<times> rexp)"
+  the_trn_rexp:: "rhs_item \<Rightarrow> rexp"
 where 
-  "the_Trn (Trn Y r) = (Y, r)"
+  "the_trn_rexp (Trn Y r) = r"
 
 text {*
   Every right-hand side item @{text "itm"} defines a language given 
@@ -514,11 +513,11 @@
 (************ arden's lemma variation ********************)
 
 text {* 
-  The following @{text "items_of rhs X"} returns all @{text "X"}-items in @{text "rhs"}.
+  The following @{text "trns_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}"
+  "trns_of rhs X \<equiv> {Trn X r | r. Trn X r \<in> rhs}"
 
 text {* 
   The following @{text "rexp_of rhs X"} combines all regular expressions in @{text "X"}-items
@@ -527,10 +526,10 @@
   *}
 
 definition 
-  "rexp_of rhs X \<equiv> \<Uplus>((snd o the_Trn) ` items_of rhs X)"
+  "rexp_of rhs X \<equiv> \<Uplus> {r. Trn X r \<in> rhs}"
 
 text {* 
-  The following @{text "lam_of rhs"} returns all pure regular expression items in @{text "rhs"}.
+  The following @{text "lam_of rhs"} returns all pure regular expression trns in @{text "rhs"}.
 *}
 
 definition
@@ -545,7 +544,7 @@
 
 
 definition
-  "rexp_of_lam rhs \<equiv> \<Uplus>(the_r ` lam_of rhs)"
+  "rexp_of_lam rhs \<equiv> \<Uplus> {r. Lam r \<in> rhs}"
 
 text {*
   The following @{text "attach_rexp rexp' itm"} attach 
@@ -578,7 +577,7 @@
 
 definition 
   "arden_variate X rhs \<equiv> 
-        append_rhs_rexp (rhs - items_of rhs X) (STAR (rexp_of rhs X))"
+        append_rhs_rexp (rhs - trns_of rhs X) (STAR (\<Uplus> {r. Trn X r \<in> rhs}))"
 
 
 (*********** substitution of ES *************)
@@ -594,7 +593,7 @@
 
 definition 
   "rhs_subst rhs X xrhs \<equiv> 
-        (rhs - (items_of rhs X)) \<union> (append_rhs_rexp xrhs (rexp_of rhs X))"
+        (rhs - (trns_of rhs X)) \<union> (append_rhs_rexp xrhs (\<Uplus> {r. Trn X r \<in> rhs}))"
 
 text {*
   Suppose the equation defining @{text "X"} is $X = xrhs$, the follwing
@@ -728,53 +727,72 @@
   shows "L A \<union> L B = L (A \<union> B)"
 by simp
 
-lemma finite_snd_Trn:
-  assumes finite:"finite rhs"
-  shows "finite {r\<^isub>2. Trn Y r\<^isub>2 \<in> rhs}" (is "finite ?B")
-proof-
-  def rhs' \<equiv> "{e \<in> rhs. \<exists> r. e = Trn Y r}"
-  have "?B = (snd o the_Trn) ` rhs'" using rhs'_def by (auto simp:image_def)
-  moreover have "finite rhs'" using finite rhs'_def by auto
-  ultimately show ?thesis by simp
+lemma finite_Trn:
+  assumes fin: "finite rhs"
+  shows "finite {r. Trn Y r \<in> rhs}"
+proof -
+  have "finite {Trn Y r | Y r. Trn Y r \<in> rhs}"
+    by (rule rev_finite_subset[OF fin]) (auto)
+  then have "finite (the_trn_rexp ` {Trn Y r | Y r. Trn Y r \<in> rhs})"
+    by auto
+  then show "finite {r. Trn Y r \<in> rhs}"
+    apply(erule_tac rev_finite_subset)
+    apply(auto simp add: image_def)
+    apply(rule_tac x="Trn Y x" in exI)
+    apply(auto)
+    done
+qed
+
+lemma finite_Lam:
+  assumes fin:"finite rhs"
+  shows "finite {r. Lam r \<in> rhs}"
+proof -
+  have "finite {Lam r | r. Lam r \<in> rhs}"
+    by (rule rev_finite_subset[OF fin]) (auto)
+  then have "finite (the_r ` {Lam r | r. Lam r \<in> rhs})"
+    by auto
+  then show "finite {r. Lam r \<in> rhs}"
+    apply(erule_tac rev_finite_subset)
+    apply(auto simp add: image_def)
+    done
 qed
 
 lemma rexp_of_empty:
   assumes finite:"finite rhs"
   and nonempty:"rhs_nonempty rhs"
-  shows "[] \<notin> L (rexp_of rhs X)"
+  shows "[] \<notin> L (\<Uplus> {r. Trn X r \<in> rhs})"
 using finite nonempty rhs_nonempty_def
-by (drule_tac finite_snd_Trn[where Y = X], auto simp:rexp_of_def items_of_def)
+using finite_Trn[OF finite]
+by (auto)
 
 lemma [intro!]:
   "P (Trn X r) \<Longrightarrow> (\<exists>a. (\<exists>r. a = Trn X r \<and> P a))" by auto
 
-lemma finite_items_of:
-  "finite rhs \<Longrightarrow> finite (items_of rhs X)"
-by (auto simp:items_of_def intro:finite_subset)
-
 lemma lang_of_rexp_of:
   assumes finite:"finite rhs"
-  shows "L (items_of rhs X) = X ;; (L (rexp_of rhs X))"
+  shows "L ({Trn X r| r. Trn X r \<in> rhs}) = X ;; (L (\<Uplus>{r. Trn X r \<in> rhs}))"
 proof -
-  have "finite ((snd \<circ> the_Trn) ` items_of rhs X)" using finite_items_of[OF finite] by auto
-  thus ?thesis
-    apply (auto simp:rexp_of_def Seq_def items_of_def)
-    apply (rule_tac x = "s\<^isub>1" in exI, rule_tac x = "s\<^isub>2" in exI, auto)
-    by (rule_tac x= "Trn X r" in exI, auto simp:Seq_def)
+  have "finite {r. Trn X r \<in> rhs}" 
+    by (rule finite_Trn[OF finite]) 
+  then show ?thesis
+    apply(auto simp add: Seq_def)
+    apply(rule_tac x = "s\<^isub>1" in exI, rule_tac x = "s\<^isub>2" in exI, auto)
+    apply(rule_tac x= "Trn X xa" in exI)
+    apply(auto simp: Seq_def)
+    done
 qed
 
 lemma rexp_of_lam_eq_lam_set:
-  assumes finite: "finite rhs"
-  shows "L (rexp_of_lam rhs) = L (lam_of rhs)"
+  assumes fin: "finite rhs"
+  shows "L (\<Uplus>{r. Lam r \<in> rhs}) = L ({Lam r | r. Lam r \<in> rhs})"
 proof -
-  have "finite (the_r ` {Lam r |r. Lam r \<in> rhs})" using finite
-    by (rule_tac finite_imageI, auto intro:finite_subset)
-  thus ?thesis by (auto simp:rexp_of_lam_def lam_of_def)
+  have "finite ({r. Lam r \<in> rhs})" using fin by (rule finite_Lam)
+  then show ?thesis by auto
 qed
 
 lemma [simp]:
   "L (attach_rexp r xb) = L xb ;; L r"
-apply (cases xb, auto simp:Seq_def)
+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)
 done
@@ -916,26 +934,29 @@
 
 lemma arden_variate_keeps_eq:
   assumes l_eq_r: "X = L rhs"
-  and not_empty: "[] \<notin> L (rexp_of rhs X)"
+  and not_empty: "[] \<notin> L (\<Uplus>{r. Trn X r \<in> rhs})"
   and finite: "finite rhs"
   shows "X = L (arden_variate X rhs)"
 proof -
-  def A \<equiv> "L (rexp_of rhs X)"
-  def b \<equiv> "rhs - items_of rhs X"
+  thm rexp_of_def
+  def A \<equiv> "L (\<Uplus>{r. Trn X r \<in> rhs})"
+  def b \<equiv> "rhs - trns_of rhs X"
   def B \<equiv> "L b" 
   have "X = B ;; A\<star>"
   proof-
-    have "rhs = items_of rhs X \<union> b" by (auto simp:b_def items_of_def)
-    hence "L rhs = L(items_of rhs X \<union> b)" by simp
-    hence "L rhs = L(items_of rhs X) \<union> B" by (simp only:L_rhs_union_distrib B_def)
-    with lang_of_rexp_of
-    have "L rhs = X ;; A \<union> B " using finite by (simp only:B_def b_def A_def)
-    thus ?thesis
+    have "L rhs = L(trns_of rhs X \<union> b)" by (auto simp: b_def trns_of_def)
+    also have "\<dots> = X ;; A \<union> B"
+      unfolding trns_of_def
+      unfolding L_rhs_union_distrib[symmetric]
+      by (simp only: lang_of_rexp_of finite B_def A_def)
+    finally show ?thesis
       using l_eq_r not_empty
-      apply (drule_tac B = B and X = X in ardens_revised)
-      by (auto simp:A_def simp del:L_rhs.simps)
+      apply(rule_tac ardens_revised[THEN iffD1])
+      apply(simp add: A_def)
+      apply(simp)
+      done
   qed
-  moreover have "L (arden_variate X rhs) = (B ;; A\<star>)" (is "?L = ?R")
+  moreover have "L (arden_variate X rhs) = (B ;; A\<star>)"
     by (simp only:arden_variate_def L_rhs_union_distrib lang_of_append_rhs 
                   B_def A_def b_def L_rexp.simps seq_union_distrib_left)
    ultimately show ?thesis by simp
@@ -976,15 +997,21 @@
   and finite: "finite rhs"
   shows "L (rhs_subst rhs X xrhs) = L rhs" (is "?Left = ?Right")
 proof-
-  def A \<equiv> "L (rhs - items_of rhs X)"
-  have "?Left = A \<union> L (append_rhs_rexp xrhs (rexp_of rhs X))"
-    by (simp only:rhs_subst_def L_rhs_union_distrib A_def)
-  moreover have "?Right = A \<union> L (items_of rhs X)"
+  def A \<equiv> "L (rhs - trns_of rhs X)"
+  have "?Left = A \<union> L (append_rhs_rexp xrhs (\<Uplus>{r. Trn X r \<in> rhs}))"
+    unfolding rhs_subst_def
+    unfolding L_rhs_union_distrib[symmetric]
+    by (simp add: A_def)
+  moreover have "?Right = A \<union> L ({Trn X r | r. Trn X r \<in> rhs})"
   proof-
-    have "rhs = (rhs - items_of rhs X) \<union> (items_of rhs X)" by (auto simp:items_of_def)
-    thus ?thesis by (simp only:L_rhs_union_distrib A_def)
+    have "rhs = (rhs - trns_of rhs X) \<union> (trns_of rhs X)" by (auto simp add: trns_of_def)
+    thus ?thesis 
+      unfolding A_def
+      unfolding L_rhs_union_distrib
+      unfolding trns_of_def
+      by simp
   qed
-  moreover have "L (append_rhs_rexp xrhs (rexp_of rhs X)) = L (items_of rhs X)" 
+  moreover have "L (append_rhs_rexp xrhs (\<Uplus>{r. Trn X r \<in> rhs})) = L ({Trn X r | r. Trn X r \<in> rhs})" 
     using finite substor  by (simp only:lang_of_append_rhs lang_of_rexp_of)
   ultimately show ?thesis by simp
 qed
@@ -1021,7 +1048,7 @@
 
 lemma arden_variate_removes_cl:
   "classes_of (arden_variate Y yrhs) = classes_of yrhs - {Y}"
-apply (simp add:arden_variate_def append_rhs_keeps_cls items_of_def)
+apply (simp add:arden_variate_def append_rhs_keeps_cls trns_of_def)
 by (auto simp:classes_of_def)
 
 lemma lefts_of_keeps_cls:
@@ -1033,7 +1060,7 @@
       classes_of (rhs_subst rhs X xrhs) = classes_of rhs \<union> classes_of xrhs - {X}"
 apply (simp only:rhs_subst_def append_rhs_keeps_cls 
                               classes_of_union_distrib[THEN sym])
-by (auto simp:classes_of_def items_of_def)
+by (auto simp:classes_of_def trns_of_def)
 
 lemma eqs_subst_keeps_self_contained:
   fixes Y
@@ -1223,39 +1250,46 @@
   and Inv_ES: "Inv ES"
   shows "\<exists> (r::rexp). L r = X" (is "\<exists> r. ?P r")
 proof-
-  let ?A = "arden_variate X xrhs"
-  have "?P (rexp_of_lam ?A)"
+  def A \<equiv> "arden_variate X xrhs"
+  have "?P (rexp_of_lam A)"
   proof -
-    have "L (rexp_of_lam ?A) = L (lam_of ?A)"
+    thm lam_of_def
+    thm rexp_of_lam_def
+    have "L (\<Uplus>{r. Lam r \<in> A}) = L ({Lam r | r. Lam r \<in>  A})"
     proof(rule rexp_of_lam_eq_lam_set)
-      show "finite (arden_variate X xrhs)" using Inv_ES ES_single 
-        by (rule_tac arden_variate_keeps_finite, 
-                       auto simp add:Inv_def finite_rhs_def)
+      show "finite A" 
+	unfolding A_def
+	using Inv_ES ES_single 
+        by (rule_tac arden_variate_keeps_finite) 
+           (auto simp add: Inv_def finite_rhs_def)
     qed
-    also have "\<dots> = L ?A"
+    also have "\<dots> = L A"
     proof-
-      have "lam_of ?A = ?A"
+      have "lam_of A = A"
       proof-
-        have "classes_of ?A = {}" using Inv_ES ES_single
+        have "classes_of A = {}" using Inv_ES ES_single
+	  unfolding A_def
           by (simp add:arden_variate_removes_cl 
                        self_contained_def Inv_def lefts_of_def) 
-        thus ?thesis 
+        thus ?thesis
+	  unfolding A_def
           by (auto simp only:lam_of_def classes_of_def, case_tac x, auto)
       qed
-      thus ?thesis by simp
+      thus ?thesis unfolding lam_of_def by simp
     qed
     also have "\<dots> = X"
+    unfolding A_def
     proof(rule arden_variate_keeps_eq [THEN sym])
       show "X = L xrhs" using Inv_ES ES_single 
         by (auto simp only:Inv_def valid_eqns_def)  
     next
-      from Inv_ES ES_single show "[] \<notin> L (rexp_of xrhs X)"
+      from Inv_ES ES_single show "[] \<notin> L (\<Uplus>{r. Trn X r \<in> xrhs})"
         by(simp add:Inv_def ardenable_def rexp_of_empty finite_rhs_def)
     next
       from Inv_ES ES_single show "finite xrhs" 
         by (simp add:Inv_def finite_rhs_def)
     qed
-    finally show ?thesis by simp
+    finally show ?thesis unfolding rexp_of_lam_def by simp
   qed
   thus ?thesis by auto
 qed
@@ -1278,12 +1312,6 @@
     by (rule last_cl_exists_rexp)
 qed
 
-lemma finals_in_partitions:
-  shows "finals A \<subseteq> (UNIV // \<approx>A)"
-unfolding finals_def
-unfolding quotient_def
-by auto
-
 theorem hard_direction: 
   assumes finite_CS: "finite (UNIV // \<approx>A)"
   shows   "\<exists>r::rexp. A = L r"

--- a/Paper/Paper.thy	Tue Feb 08 12:01:28 2011 +0000
+++ b/Paper/Paper.thy	Tue Feb 08 15:50:26 2011 +0000
@@ -327,7 +327,7 @@
 
   \noindent
   It is straightforward to show that @{thm lang_is_union_of_finals} and 
-  @{thm finals_included_in_UNIV} hold. 
+  @{thm finals_in_partitions} hold. 
   Therefore if we know that there exists a regular expression for every
   equivalence class in @{term "finals A"} (which by assumption must be
   a finite set), then we can combine these regular expressions with @{const ALT}
@@ -335,7 +335,7 @@
 
 
   We prove Thm.~\ref{myhillnerodeone} by giving a method that can calculate a
-  regular expression for \emph{every} equivalence classe, not just the ones 
+  regular expression for \emph{every} equivalence class, not just the ones 
   in @{term "finals A"}. We
   first define a notion of \emph{transition} between equivalence classes
   %

Binary file tphols-2011/myhill.pdf has changed