--- 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"