# HG changeset patch # User urbanc # Date 1297766276 0 # Node ID ae6ad1363eb9a1be039f3045b66e443e1f90a5fb # Parent 5bd73aa805a785b4a1a218fe1dedb5e125e9794b updated paper diff -r 5bd73aa805a7 -r ae6ad1363eb9 Myhill_1.thy --- a/Myhill_1.thy Tue Feb 15 08:08:04 2011 +0000 +++ b/Myhill_1.thy Tue Feb 15 10:37:56 2011 +0000 @@ -742,18 +742,16 @@ assumes finite: "finite CS" shows "finite (Init_rhs CS X)" proof- - have "finite {Trn Y (CHAR c) |Y c. Y \ CS \ Y ;; {[c]} \ X}" (is "finite ?A") - proof - - def S \ "{(Y, c)| Y c. Y \ CS \ Y ;; {[c]} \ X}" - def h \ "\ (Y, c). Trn Y (CHAR c)" - have "finite (CS \ (UNIV::char set))" using finite by auto - hence "finite S" using S_def - by (rule_tac B = "CS \ UNIV" in finite_subset, auto) - moreover have "?A = h ` S" by (auto simp: S_def h_def image_def) - ultimately show ?thesis - by auto - qed - thus ?thesis by (simp add:Init_rhs_def transition_def) + def S \ "{(Y, c)| Y c. Y \ CS \ Y ;; {[c]} \ X}" + def h \ "\ (Y, c). Trn Y (CHAR c)" + have "finite (CS \ (UNIV::char set))" using finite by auto + then have "finite S" using S_def + by (rule_tac B = "CS \ UNIV" in finite_subset) (auto) + moreover have "{Trn Y (CHAR c) |Y c. Y \ CS \ Y ;; {[c]} \ X} = h ` S" + unfolding S_def h_def image_def by auto + ultimately + have "finite {Trn Y (CHAR c) |Y c. Y \ CS \ Y ;; {[c]} \ X}" by auto + then show "finite (Init_rhs CS X)" unfolding Init_rhs_def transition_def by simp qed lemma Init_ES_satisfies_invariant: @@ -1045,33 +1043,33 @@ lemma iteration_step_measure: assumes Inv_ES: "invariant ES" and X_in_ES: "(X, xrhs) \ ES" - and not_T: "Cond ES " + and Cnd: "Cond ES " shows "(Iter X ES, ES) \ measure card" proof - - have finite_ES: "finite ES" using Inv_ES by (simp add: invariant_def) + have fin: "finite ES" using Inv_ES unfolding invariant_def by simp then obtain Y yrhs where Y_in_ES: "(Y, yrhs) \ ES" and not_eq: "(X, xrhs) \ (Y, yrhs)" - using not_T X_in_ES by (drule_tac card_noteq_1_has_more) (auto) + using Cnd X_in_ES by (drule_tac card_noteq_1_has_more) (auto) then have "(Y, yrhs) \ ES " "X \ Y" using X_in_ES Inv_ES unfolding invariant_def distinct_equas_def by auto then show "(Iter X ES, ES) \ measure card" apply(rule IterI2) apply(rule Remove_in_card_measure) - apply(simp_all add: finite_ES) + apply(simp_all add: fin) done qed lemma iteration_step_invariant: assumes Inv_ES: "invariant ES" and X_in_ES: "(X, xrhs) \ ES" - and not_T: "Cond ES" + and Cnd: "Cond ES" shows "invariant (Iter X ES)" proof - have finite_ES: "finite ES" using Inv_ES by (simp add: invariant_def) then obtain Y yrhs where Y_in_ES: "(Y, yrhs) \ ES" and not_eq: "(X, xrhs) \ (Y, yrhs)" - using not_T X_in_ES by (drule_tac card_noteq_1_has_more) (auto) + using Cnd X_in_ES by (drule_tac card_noteq_1_has_more) (auto) then have "(Y, yrhs) \ ES" "X \ Y" using X_in_ES Inv_ES unfolding invariant_def distinct_equas_def by auto @@ -1088,13 +1086,13 @@ lemma iteration_step_ex: assumes Inv_ES: "invariant ES" and X_in_ES: "(X, xrhs) \ ES" - and not_T: "Cond ES" + and Cnd: "Cond ES" shows "\xrhs'. (X, xrhs') \ (Iter X ES)" proof - have finite_ES: "finite ES" using Inv_ES by (simp add: invariant_def) then obtain Y yrhs where Y_in_ES: "(Y, yrhs) \ ES" and not_eq: "(X, xrhs) \ (Y, yrhs)" - using not_T X_in_ES by (drule_tac card_noteq_1_has_more) (auto) + using Cnd X_in_ES by (drule_tac card_noteq_1_has_more) (auto) then have "(Y, yrhs) \ ES " "X \ Y" using X_in_ES Inv_ES unfolding invariant_def distinct_equas_def by auto @@ -1155,38 +1153,25 @@ shows "\r::rexp. L r = X" proof- def A \ "Arden X xrhs" - have eq: "{Lam r | r. Lam r \ A} = A" - proof - - have "rhss A = {}" using Inv_ES - unfolding A_def valid_eqs_def invariant_def lhss_def - by (simp add: Arden_removes_cl) - thus ?thesis unfolding A_def rhss_def - apply(auto simp only:) - apply(case_tac x) - apply(auto) - done - qed + have "rhss xrhs \ {X}" using Inv_ES + unfolding valid_eqs_def invariant_def rhss_def lhss_def + by auto + then have "rhss A = {}" unfolding A_def + by (simp add: Arden_removes_cl) + then have eq: "{Lam r | r. Lam r \ A} = A" unfolding rhss_def + by (auto, case_tac x, auto) + have "finite A" using Inv_ES unfolding A_def invariant_def finite_rhs_def using Arden_keeps_finite by auto - then have "finite {r. Lam r \ A}" by (rule finite_Lam) - then have "L (\{r. Lam r \ A}) = L ({Lam r | r. Lam r \ A})" - by auto - also have "\ = L A" by (simp add: eq) - also have "\ = X" - proof - - have "X = L xrhs" using Inv_ES unfolding invariant_def sound_eqs_def - by auto - moreover - from Inv_ES have "[] \ L (\{r. Trn X r \ xrhs})" - unfolding invariant_def ardenable_def finite_rhs_def - by(simp add: rexp_of_empty) - moreover - from Inv_ES have "finite xrhs" unfolding invariant_def finite_rhs_def - by simp - ultimately show "L A = X" unfolding A_def - by (rule Arden_keeps_eq[symmetric]) - qed - finally have "L (\{r. Lam r \ A}) = X" . + then have fin: "finite {r. Lam r \ A}" by (rule finite_Lam) + + have "X = L xrhs" using Inv_ES unfolding invariant_def sound_eqs_def + by simp + then have "X = L A" using Inv_ES + unfolding A_def invariant_def ardenable_def finite_rhs_def rhs_nonempty_def + by (rule_tac Arden_keeps_eq) (simp_all add: finite_Trn) + then have "X = L {Lam r | r. Lam r \ A}" using eq by simp + then have "X = L (\{r. Lam r \ A})" using fin by auto then show "\r::rexp. L r = X" by blast qed @@ -1216,14 +1201,14 @@ assumes finite_CS: "finite (UNIV // \A)" shows "\r::rexp. A = L r" proof - - have f: "finite (finals A)" + have fin: "finite (finals A)" using finals_in_partitions finite_CS by (rule finite_subset) have "\X \ (UNIV // \A). \r::rexp. X = L r" using finite_CS every_eqcl_has_reg by blast then have a: "\X \ finals A. \r::rexp. X = L r" using finals_in_partitions by auto then obtain rs::"rexp set" where "\ (finals A) = \(L ` rs)" "finite rs" - using f by (auto dest: bchoice_finite_set) + using fin by (auto dest: bchoice_finite_set) then have "A = L (\rs)" unfolding lang_is_union_of_finals[symmetric] by simp then show "\r::rexp. A = L r" by blast diff -r 5bd73aa805a7 -r ae6ad1363eb9 Paper/Paper.thy --- a/Paper/Paper.thy Tue Feb 15 08:08:04 2011 +0000 +++ b/Paper/Paper.thy Tue Feb 15 10:37:56 2011 +0000 @@ -667,10 +667,21 @@ The first two ensure that the equational system is always finite (number of equations and number of terms in each equation); \ldots + It is straightforward to prove that the inital equational system satisfies the + invariant. + \begin{lemma} @{thm[mode=IfThen] Init_ES_satisfies_invariant} \end{lemma} + \begin{proof} + Finiteness is given by the assumption and the way how we set up the + initial equational system. Soundness is proved in Lem.~\ref{inv}. Distinctness + follows from the fact that the equivalence classes are disjoint. The ardenable + property also follows from the setup of the equational system as does + validity.\qed + \end{proof} + \begin{lemma} @{thm[mode=IfThen] iteration_step_invariant[where xrhs="rhs"]} \end{lemma} @@ -679,15 +690,54 @@ @{thm[mode=IfThen] iteration_step_measure[simplified (no_asm), where xrhs="rhs"]} \end{lemma} + \begin{proof} + By assumption we know that @{text "ES"} is finite and has more than one element. + Therefore there must be an element @{term "(Y, yrhs) \ ES"} with + @{term "(Y, yrhs) \ (X, rhs)"}. Using the distictness property we can infer + that @{term "Y \ X"}. We further know that @{text "Remove ES Y yrhs"} + removes the equation @{text "Y = yrhs"} from the system, and therefore + the cardinality of @{const Iter} strictly decreases.\qed + \end{proof} + \begin{lemma} If @{thm (prem 1) Solve} and @{thm (prem 2) Solve} then there exists a @{text rhs} such that @{term "Solve X (Init (UNIV // \A)) = {(X, rhs)}"} and @{term "invariant {(X, rhs)}"}. \end{lemma} + \begin{lemma}\label{every_eqcl_has_reg} + @{thm[mode=IfThen] every_eqcl_has_reg} + \end{lemma} + + \begin{proof} + By the preceeding Lemma, we know that there exists a @{text "rhs"} such + that @{term "Solve X (Init (UNIV // \A))"} returns the equation @{text "X = rhs"}, + and that the invariant holds for this equation. That means we + know @{text "X = \\ ` rhs"}. We further know that + this is equal to @{text "\\ ` (Arden X rhs)"} using ???. + + \end{proof} + \begin{theorem} @{thm[mode=IfThen] Myhill_Nerode1} \end{theorem} + + \begin{proof} + By Lem.~\ref{every_eqcl_has_reg} we know that there exists a regular language for + every equivalence class in @{term "UNIV // \A"}. Since @{text "finals A"} is + a subset of @{term "UNIV // \A"}, we also know that for every equvalence class + in @{term "finals A"} there exists a regular language. Moreover by assumption + we know that @{term "finals A"} must be finite, therefore there must be a finite + set of regular expressions @{text "rs"} such that + + \begin{center} + @{term "\(finals A) = L (\rs)"} + \end{center} + + \noindent + Since the left-hand side is equal to @{text A}, we can use @{term "\rs"} + as the regular expression that solves the goal.\qed + \end{proof} *}