# HG changeset patch # User urbanc # Date 1297180226 0 # Node ID bba9c80735f9fb9fea854dbd9bce5fe59aa70480 # Parent 77583805123d93e1b79debb6fdbf51f1e556a05f started to define things more directly diff -r 77583805123d -r bba9c80735f9 Myhill_1.thy --- 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 \ UNIV // \A" +lemma finals_in_partitions: + shows "finals A \ (UNIV // \A)" unfolding finals_def unfolding quotient_def by auto - section {* Direction @{text "finite partition \ regular language"}*} text {* @@ -445,9 +444,9 @@ "the_r (Lam r) = r" fun - the_Trn:: "rhs_item \ (lang \ rexp)" + the_trn_rexp:: "rhs_item \ 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 \ {Trn X r | r. (Trn X r) \ rhs}" + "trns_of rhs X \ {Trn X r | r. Trn X r \ 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 \ \((snd o the_Trn) ` items_of rhs X)" + "rexp_of rhs X \ \ {r. Trn X r \ 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 \ \(the_r ` lam_of rhs)" + "rexp_of_lam rhs \ \ {r. Lam r \ rhs}" text {* The following @{text "attach_rexp rexp' itm"} attach @@ -578,7 +577,7 @@ definition "arden_variate X rhs \ - append_rhs_rexp (rhs - items_of rhs X) (STAR (rexp_of rhs X))" + append_rhs_rexp (rhs - trns_of rhs X) (STAR (\ {r. Trn X r \ rhs}))" (*********** substitution of ES *************) @@ -594,7 +593,7 @@ definition "rhs_subst rhs X xrhs \ - (rhs - (items_of rhs X)) \ (append_rhs_rexp xrhs (rexp_of rhs X))" + (rhs - (trns_of rhs X)) \ (append_rhs_rexp xrhs (\ {r. Trn X r \ rhs}))" text {* Suppose the equation defining @{text "X"} is $X = xrhs$, the follwing @@ -728,53 +727,72 @@ shows "L A \ L B = L (A \ B)" by simp -lemma finite_snd_Trn: - assumes finite:"finite rhs" - shows "finite {r\<^isub>2. Trn Y r\<^isub>2 \ rhs}" (is "finite ?B") -proof- - def rhs' \ "{e \ rhs. \ 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 \ rhs}" +proof - + have "finite {Trn Y r | Y r. Trn Y r \ rhs}" + by (rule rev_finite_subset[OF fin]) (auto) + then have "finite (the_trn_rexp ` {Trn Y r | Y r. Trn Y r \ rhs})" + by auto + then show "finite {r. Trn Y r \ 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 \ rhs}" +proof - + have "finite {Lam r | r. Lam r \ rhs}" + by (rule rev_finite_subset[OF fin]) (auto) + then have "finite (the_r ` {Lam r | r. Lam r \ rhs})" + by auto + then show "finite {r. Lam r \ 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 "[] \ L (rexp_of rhs X)" + shows "[] \ L (\ {r. Trn X r \ 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) \ (\a. (\r. a = Trn X r \ P a))" by auto -lemma finite_items_of: - "finite rhs \ 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 \ rhs}) = X ;; (L (\{r. Trn X r \ rhs}))" proof - - have "finite ((snd \ 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 \ 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 (\{r. Lam r \ rhs}) = L ({Lam r | r. Lam r \ rhs})" proof - - have "finite (the_r ` {Lam r |r. Lam r \ 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 \ 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: "[] \ L (rexp_of rhs X)" + and not_empty: "[] \ L (\{r. Trn X r \ rhs})" and finite: "finite rhs" shows "X = L (arden_variate X rhs)" proof - - def A \ "L (rexp_of rhs X)" - def b \ "rhs - items_of rhs X" + thm rexp_of_def + def A \ "L (\{r. Trn X r \ rhs})" + def b \ "rhs - trns_of rhs X" def B \ "L b" have "X = B ;; A\" proof- - have "rhs = items_of rhs X \ b" by (auto simp:b_def items_of_def) - hence "L rhs = L(items_of rhs X \ b)" by simp - hence "L rhs = L(items_of rhs X) \ B" by (simp only:L_rhs_union_distrib B_def) - with lang_of_rexp_of - have "L rhs = X ;; A \ B " using finite by (simp only:B_def b_def A_def) - thus ?thesis + have "L rhs = L(trns_of rhs X \ b)" by (auto simp: b_def trns_of_def) + also have "\ = X ;; A \ 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\)" (is "?L = ?R") + moreover have "L (arden_variate X rhs) = (B ;; A\)" 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 \ "L (rhs - items_of rhs X)" - have "?Left = A \ 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 \ L (items_of rhs X)" + def A \ "L (rhs - trns_of rhs X)" + have "?Left = A \ L (append_rhs_rexp xrhs (\{r. Trn X r \ rhs}))" + unfolding rhs_subst_def + unfolding L_rhs_union_distrib[symmetric] + by (simp add: A_def) + moreover have "?Right = A \ L ({Trn X r | r. Trn X r \ rhs})" proof- - have "rhs = (rhs - items_of rhs X) \ (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) \ (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 (\{r. Trn X r \ rhs})) = L ({Trn X r | r. Trn X r \ 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 \ 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 "\ (r::rexp). L r = X" (is "\ r. ?P r") proof- - let ?A = "arden_variate X xrhs" - have "?P (rexp_of_lam ?A)" + def A \ "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 (\{r. Lam r \ A}) = L ({Lam r | r. Lam r \ 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 "\ = L ?A" + also have "\ = 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 "\ = 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 "[] \ L (rexp_of xrhs X)" + from Inv_ES ES_single show "[] \ L (\{r. Trn X r \ 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 \ (UNIV // \A)" -unfolding finals_def -unfolding quotient_def -by auto - theorem hard_direction: assumes finite_CS: "finite (UNIV // \A)" shows "\r::rexp. A = L r" diff -r 77583805123d -r bba9c80735f9 Paper/Paper.thy --- 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 % diff -r 77583805123d -r bba9c80735f9 tphols-2011/myhill.pdf Binary file tphols-2011/myhill.pdf has changed