# HG changeset patch # User urbanc # Date 1311862930 0 # Node ID edacc141060f4a9253382bc741ce95fc4a188c7b # Parent c6ebfe052109dfac16069c2648eb6771dade1197 small improvements diff -r c6ebfe052109 -r edacc141060f Derivatives.thy --- a/Derivatives.thy Thu Jul 28 11:56:25 2011 +0000 +++ b/Derivatives.thy Thu Jul 28 14:22:10 2011 +0000 @@ -14,7 +14,7 @@ definition Der :: "'a \ 'a lang \ 'a lang" where - "Der c A \ {s. [c] @ s \ A}" + "Der c A \ {s'. [c] @ s' \ A}" definition Ders :: "'a list \ 'a lang \ 'a lang" @@ -77,25 +77,19 @@ finally show "Der c (A\) = (Der c A) \ A\" . qed +lemma Ders_nil [simp]: + shows "Ders [] A = A" +unfolding Ders_def by simp -lemma Ders_singleton: - shows "Ders [c] A = Der c A" -unfolding Der_def Ders_def -by simp +lemma Ders_cons [simp]: + shows "Ders (c # s) A = Ders s (Der c A)" +unfolding Ders_def Der_def by auto -lemma Ders_append: +lemma Ders_append [simp]: shows "Ders (s1 @ s2) A = Ders s2 (Ders s1 A)" unfolding Ders_def by simp -text {* Relating the Myhill-Nerode relation with left-quotients. *} - -lemma MN_Rel_Ders: - shows "x \A y \ Ders x A = Ders y A" -unfolding Ders_def str_eq_def str_eq_rel_def -by auto - - subsection {* Brozowsky's derivatives of regular expressions *} fun @@ -119,15 +113,12 @@ (if nullable r1 then Plus (Times (der c r1) r2) (der c r2) else Times (der c r1) r2)" | "der c (Star r) = Times (der c r) (Star r)" -function +fun ders :: "'a list \ 'a rexp \ 'a rexp" where "ders [] r = r" -| "ders (s @ [c]) r = der c (ders s r)" -by (auto) (metis rev_cases) +| "ders (c # s) r = ders s (der c r)" -termination - by (relation "measure (length o fst)") (auto) lemma Delta_nullable: shows "Delta (lang r) = (if nullable r then {[]} else {})" @@ -140,13 +131,7 @@ lemma Ders_ders: shows "Ders s (lang r) = lang (ders s r)" -apply(induct s rule: rev_induct) -apply(simp add: Ders_def) -apply(simp only: ders.simps) -apply(simp only: Ders_append) -apply(simp only: Ders_singleton) -apply(simp only: Der_der) -done +by (induct s arbitrary: r) (simp_all add: Der_der) subsection {* Antimirov's Partial Derivatives *} @@ -161,40 +146,29 @@ | "pder c One = {Zero}" | "pder c (Atom c') = (if c = c' then {One} else {Zero})" | "pder c (Plus r1 r2) = (pder c r1) \ (pder c r2)" -| "pder c (Times r1 r2) = Times_set (pder c r1) r2 \ (if nullable r1 then pder c r2 else {})" +| "pder c (Times r1 r2) = + (if nullable r1 then Times_set (pder c r1) r2 \ pder c r2 else Times_set (pder c r1) r2)" | "pder c (Star r) = Times_set (pder c r) (Star r)" abbreviation "pder_set c rs \ \r \ rs. pder c r" -function +fun pders :: "'a list \ 'a rexp \ ('a rexp) set" where "pders [] r = {r}" -| "pders (s @ [c]) r = pder_set c (pders s r)" -by (auto) (metis rev_cases) - -termination - by (relation "measure (length o fst)") (auto) +| "pders (c # s) r = (\r'\ (pder c r). (pders s r'))" abbreviation "pders_set A r \ \s \ A. pders s r" lemma pders_append: "pders (s1 @ s2) r = \ (pders s2) ` (pders s1 r)" -apply(induct s2 arbitrary: s1 r rule: rev_induct) -apply(simp) -apply(subst append_assoc[symmetric]) -apply(simp only: pders.simps) -apply(auto) -done +by (induct s1 arbitrary: r) (simp_all) -lemma pders_singleton: - "pders [c] r = pder c r" -apply(subst append_Nil[symmetric]) -apply(simp only: pders.simps) -apply(simp) -done +lemma pders_snoc: + shows "pders (s @ [c]) r = pder_set c (pders s r)" +by (simp add: pders_append) lemma pders_set_lang: shows "(\ (lang ` pder_set c rs)) = (\r \ rs. (\lang ` (pder c r)))" @@ -203,19 +177,19 @@ lemma pders_Zero [simp]: shows "pders s Zero = {Zero}" -by (induct s rule: rev_induct) (simp_all) +by (induct s) (simp_all) lemma pders_One [simp]: shows "pders s One = (if s = [] then {One} else {Zero})" -by (induct s rule: rev_induct) (auto) +by (induct s) (auto) lemma pders_Atom [simp]: shows "pders s (Atom c) = (if s = [] then {Atom c} else (if s = [c] then {One} else {Zero}))" -by (induct s rule: rev_induct) (auto) +by (induct s) (auto) lemma pders_Plus [simp]: shows "pders s (Plus r1 r2) = (if s = [] then {Plus r1 r2} else (pders s r1) \ (pders s r2))" -by (induct s rule: rev_induct) (auto) +by (induct s) (auto) text {* Non-empty suffixes of a string *} @@ -237,7 +211,8 @@ case (snoc c s) have ih: "pders s (Times r1 r2) \ Times_set (pders s r1) r2 \ (\v \ Suf s. pders v r2)" by fact - have "pders (s @ [c]) (Times r1 r2) = pder_set c (pders s (Times r1 r2))" by simp + have "pders (s @ [c]) (Times r1 r2) = pder_set c (pders s (Times r1 r2))" + by (simp add: pders_snoc) also have "\ \ pder_set c (Times_set (pders s r1) r2 \ (\v \ Suf s. pders v r2))" using ih by (auto) (blast) also have "\ = pder_set c (Times_set (pders s r1) r2) \ pder_set c (\v \ Suf s. pders v r2)" @@ -245,15 +220,11 @@ also have "\ = pder_set c (Times_set (pders s r1) r2) \ (\v \ Suf s. pder_set c (pders v r2))" by (simp) also have "\ \ pder_set c (Times_set (pders s r1) r2) \ (pder c r2) \ (\v \ Suf s. pders (v @ [c]) r2)" - by (auto) + by (auto simp add: pders_snoc) also have "\ \ Times_set (pder_set c (pders s r1)) r2 \ (pder c r2) \ (\v \ Suf s. pders (v @ [c]) r2)" by (auto simp add: if_splits) (blast) also have "\ = Times_set (pders (s @ [c]) r1) r2 \ (\v \ Suf (s @ [c]). pders v r2)" - apply(subst (2) pders.simps) - apply(simp only: Suf) - apply(simp add: Suf_Union pders_singleton) - apply(auto) - done + by (auto simp add: pders_snoc Suf Suf_Union) finally show ?case . qed (simp) @@ -265,7 +236,7 @@ case (snoc c s) have ih: "s \ [] \ pders s (Star r) \ (\v\Suf s. Times_set (pders v r) (Star r))" by fact { assume asm: "s \ []" - have "pders (s @ [c]) (Star r) = pder_set c (pders s (Star r))" by simp + have "pders (s @ [c]) (Star r) = pder_set c (pders s (Star r))" by (simp add: pders_snoc) also have "\ \ (pder_set c (\v\Suf s. Times_set (pders v r) (Star r)))" using ih[OF asm] by blast also have "\ = (\v\Suf s. pder_set c (Times_set (pders v r) (Star r)))" @@ -275,52 +246,46 @@ also have "\ = (\v\Suf s. (Times_set (pder_set c (pders v r)) (Star r))) \ pder c (Star r)" using asm by (auto simp add: Suf_def) also have "\ = (\v\Suf s. (Times_set (pders (v @ [c]) r) (Star r))) \ (Times_set (pder c r) (Star r))" - by simp + by (simp add: pders_snoc) also have "\ = (\v\Suf (s @ [c]). (Times_set (pders v r) (Star r)))" - apply(simp only: Suf) - apply(simp add: Suf_Union pders_singleton) - apply(auto) - done + by (auto simp add: Suf Suf_Union pders_snoc) finally have ?case . } moreover { assume asm: "s = []" then have ?case - apply(simp add: pders_singleton Suf_def) - apply(auto) - apply(rule_tac x="[c]" in exI) - apply(simp add: pders_singleton) - done + by (auto simp add: pders_snoc Suf_def) } ultimately show ?case by blast qed (simp) -abbreviation +definition "UNIV1 \ UNIV - {[]}" lemma pders_set_Zero: shows "pders_set UNIV1 Zero = {Zero}" -by auto +unfolding UNIV1_def by auto lemma pders_set_One: shows "pders_set UNIV1 One = {Zero}" -by (auto split: if_splits) +unfolding UNIV1_def by (auto split: if_splits) lemma pders_set_Atom: shows "pders_set UNIV1 (Atom c) \ {One, Zero}" -by (auto split: if_splits) +unfolding UNIV1_def by (auto split: if_splits) lemma pders_set_Plus: shows "pders_set UNIV1 (Plus r1 r2) = pders_set UNIV1 r1 \ pders_set UNIV1 r2" -by auto +unfolding UNIV1_def by auto lemma pders_set_Times_aux: assumes a: "s \ UNIV1" shows "pders_set (Suf s) r2 \ pders_set UNIV1 r2" -using a by (auto simp add: Suf_def) +using a unfolding UNIV1_def Suf_def by (auto) lemma pders_set_Times: shows "pders_set UNIV1 (Times r1 r2) \ Times_set (pders_set UNIV1 r1) r2 \ pders_set UNIV1 r2" +unfolding UNIV1_def apply(rule UN_least) apply(rule subset_trans) apply(rule pders_Times) @@ -329,11 +294,12 @@ apply(auto)[1] apply(rule subset_trans) apply(rule pders_set_Times_aux) -apply(auto) +apply(auto simp add: UNIV1_def) done lemma pders_set_Star: shows "pders_set UNIV1 (Star r) \ Times_set (pders_set UNIV1 r) (Star r)" +unfolding UNIV1_def apply(rule UN_least) apply(rule subset_trans) apply(rule pders_Star) @@ -369,6 +335,7 @@ lemma pders_set_UNIV_UNIV1: shows "pders_set UNIV r = pders [] r \ pders_set UNIV1 r" +unfolding UNIV1_def apply(auto) apply(rule_tac x="[]" in exI) apply(simp) @@ -418,7 +385,7 @@ have "Ders (s @ [c]) (lang r) = Ders [c] (Ders s (lang r))" by (simp add: Ders_append) also have "\ = Der c (\ lang ` (pders s r))" using ih - by (simp add: Ders_singleton) + by (simp) also have "\ = (\r\pders s r. Der c (lang r))" unfolding Der_def image_def by auto also have "\ = (\r\pders s r. (\ lang ` (pder c r)))" @@ -426,7 +393,7 @@ also have "\ = (\lang ` (pder_set c (pders s r)))" by (simp add: pders_set_lang) also have "\ = (\lang ` (pders (s @ [c]) r))" - by simp + by (simp add: pders_snoc) finally show "Ders (s @ [c]) (lang r) = \ lang ` pders (s @ [c]) r" . qed (simp add: Ders_def) @@ -446,6 +413,12 @@ unfolding Ders_ders[symmetric] Ders_pders by simp +text {* Relating the Myhill-Nerode relation with left-quotients. *} + +lemma MN_Rel_Ders: + shows "x \A y \ Ders x A = Ders y A" +unfolding Ders_def str_eq_def str_eq_rel_def +by auto subsection {* The second direction of the Myhill-Nerode theorem using @@ -488,4 +461,5 @@ by (rule refined_partition_finite) qed + end \ No newline at end of file diff -r c6ebfe052109 -r edacc141060f Journal/Paper.thy --- a/Journal/Paper.thy Thu Jul 28 11:56:25 2011 +0000 +++ b/Journal/Paper.thy Thu Jul 28 14:22:10 2011 +0000 @@ -779,8 +779,8 @@ \begin{lmm}\label{ardenable} Given an equation @{text "X = rhs"}. If @{text "X = \\ ` rhs"}, - @{thm (prem 2) Arden_keeps_eq}, and - @{thm (prem 3) Arden_keeps_eq}, then + @{thm (prem 2) Arden_preserves_soundness}, and + @{thm (prem 3) Arden_preserves_soundness}, then @{text "X = \\ ` (Arden X rhs)"}. \end{lmm} @@ -1098,6 +1098,9 @@ Much more interesting, however, are the inductive cases. They seem hard to solve directly. The reader is invited to try. + Constable et al \cite{Constable00} give the following suggestive picture about + equivalence classes: + Our first proof will rely on some \emph{tagging-functions} defined over strings. Given the inductive hypothesis, it will be easy to prove that the \emph{range} of these tagging-functions is finite. diff -r c6ebfe052109 -r edacc141060f Myhill_1.thy --- a/Myhill_1.thy Thu Jul 28 11:56:25 2011 +0000 +++ b/Myhill_1.thy Thu Jul 28 14:22:10 2011 +0000 @@ -5,7 +5,7 @@ section {* Direction @{text "finite partition \ regular language"} *} -lemma Pair_Collect[simp]: +lemma Pair_Collect [simp]: shows "(x, y) \ {(x, y). P x y} \ P x y" by simp @@ -57,7 +57,6 @@ by (auto) lemma lang_rhs_union_distrib: - fixes A B::"('a trm) set" shows "lang_rhs A \ lang_rhs B = lang_rhs (A \ B)" by simp @@ -350,7 +349,7 @@ subsubsection {* Interation step *} -lemma Arden_keeps_eq: +lemma Arden_preserves_soundness: assumes l_eq_r: "X = lang_rhs rhs" and not_empty: "ardenable rhs" and finite: "finite rhs" @@ -379,37 +378,37 @@ finally show "X = lang_rhs (Arden X rhs)" by simp qed -lemma Append_keeps_finite: +lemma Append_preserves_finite: "finite rhs \ finite (Append_rexp_rhs rhs r)" by (auto simp: Append_rexp_rhs_def) -lemma Arden_keeps_finite: +lemma Arden_preserves_finite: "finite rhs \ finite (Arden X rhs)" -by (auto simp: Arden_def Append_keeps_finite) +by (auto simp: Arden_def Append_preserves_finite) -lemma Append_keeps_nonempty: +lemma Append_preserves_ardenable: "ardenable rhs \ ardenable (Append_rexp_rhs rhs r)" apply (auto simp: ardenable_def Append_rexp_rhs_def) by (case_tac x, auto simp: conc_def) -lemma nonempty_set_sub: +lemma ardenable_set_sub: "ardenable rhs \ ardenable (rhs - A)" by (auto simp:ardenable_def) -lemma nonempty_set_union: +lemma ardenable_set_union: "\ardenable rhs; ardenable rhs'\ \ ardenable (rhs \ rhs')" by (auto simp:ardenable_def) -lemma Arden_keeps_nonempty: +lemma Arden_preserves_ardenable: "ardenable rhs \ ardenable (Arden X rhs)" -by (simp only:Arden_def Append_keeps_nonempty nonempty_set_sub) +by (simp only:Arden_def Append_preserves_ardenable ardenable_set_sub) -lemma Subst_keeps_nonempty: +lemma Subst_preserves_ardenable: "\ardenable rhs; ardenable xrhs\ \ ardenable (Subst rhs X xrhs)" -by (simp only: Subst_def Append_keeps_nonempty nonempty_set_union nonempty_set_sub) +by (simp only: Subst_def Append_preserves_ardenable ardenable_set_union ardenable_set_sub) -lemma Subst_keeps_eq: +lemma Subst_preserves_soundness: assumes substor: "X = lang_rhs xrhs" and finite: "finite rhs" shows "lang_rhs (Subst rhs X xrhs) = lang_rhs rhs" (is "?Left = ?Right") @@ -433,11 +432,11 @@ ultimately show ?thesis by simp qed -lemma Subst_keeps_finite_rhs: +lemma Subst_preserves_finite_rhs: "\finite rhs; finite yrhs\ \ finite (Subst rhs Y yrhs)" -by (auto simp: Subst_def Append_keeps_finite) +by (auto simp: Subst_def Append_preserves_finite) -lemma Subst_all_keeps_finite: +lemma Subst_all_preserves_finite: assumes finite: "finite ES" shows "finite (Subst_all ES Y yrhs)" proof - @@ -450,11 +449,11 @@ show "finite (Subst_all ES Y yrhs)" by simp qed -lemma Subst_all_keeps_finite_rhs: +lemma Subst_all_preserves_finite_rhs: "\finite_rhs ES; finite yrhs\ \ finite_rhs (Subst_all ES Y yrhs)" -by (auto intro:Subst_keeps_finite_rhs simp add:Subst_all_def finite_rhs_def) +by (auto intro:Subst_preserves_finite_rhs simp add:Subst_all_def finite_rhs_def) -lemma append_rhs_keeps_cls: +lemma append_rhs_preserves_cls: "rhss (Append_rexp_rhs rhs r) = rhss rhs" apply (auto simp: rhss_def Append_rexp_rhs_def) apply (case_tac xa, auto simp: image_def) @@ -462,20 +461,20 @@ lemma Arden_removes_cl: "rhss (Arden Y yrhs) = rhss yrhs - {Y}" -apply (simp add:Arden_def append_rhs_keeps_cls) +apply (simp add:Arden_def append_rhs_preserves_cls) by (auto simp: rhss_def) -lemma lhss_keeps_cls: +lemma lhss_preserves_cls: "lhss (Subst_all ES Y yrhs) = lhss ES" by (auto simp: lhss_def Subst_all_def) lemma Subst_updates_cls: "X \ rhss xrhs \ rhss (Subst rhs X xrhs) = rhss rhs \ rhss xrhs - {X}" -apply (simp only:Subst_def append_rhs_keeps_cls rhss_union_distrib) +apply (simp only:Subst_def append_rhs_preserves_cls rhss_union_distrib) by (auto simp: rhss_def) -lemma Subst_all_keeps_validity: +lemma Subst_all_preserves_validity: assumes sc: "validity (ES \ {(Y, yrhs)})" (is "validity ?A") shows "validity (Subst_all ES Y (Arden Y yrhs))" (is "validity ?B") proof - @@ -516,24 +515,24 @@ using invariant_ES by (simp only:invariant_def soundness_def, blast) have finite_yrhs: "finite yrhs" using invariant_ES by (auto simp:invariant_def finite_rhs_def) - have nonempty_yrhs: "ardenable yrhs" + have ardenable_yrhs: "ardenable yrhs" using invariant_ES by (auto simp:invariant_def ardenable_all_def) show "soundness (Subst_all ES Y (Arden Y yrhs))" proof - have "Y = lang_rhs (Arden Y yrhs)" using Y_eq_yrhs invariant_ES finite_yrhs using finite_Trn[OF finite_yrhs] - apply(rule_tac Arden_keeps_eq) + apply(rule_tac Arden_preserves_soundness) apply(simp_all) unfolding invariant_def ardenable_all_def ardenable_def apply(auto) done thus ?thesis using invariant_ES unfolding invariant_def finite_rhs_def2 soundness_def Subst_all_def - by (auto simp add: Subst_keeps_eq simp del: lang_rhs.simps) + by (auto simp add: Subst_preserves_soundness simp del: lang_rhs.simps) qed show "finite (Subst_all ES Y (Arden Y yrhs))" - using invariant_ES by (simp add:invariant_def Subst_all_keeps_finite) + using invariant_ES by (simp add:invariant_def Subst_all_preserves_finite) show "distinctness (Subst_all ES Y (Arden Y yrhs))" using invariant_ES unfolding distinctness_def Subst_all_def invariant_def by auto @@ -543,10 +542,10 @@ assume "(X, rhs) \ ES" hence "ardenable rhs" using invariant_ES by (auto simp add:invariant_def ardenable_all_def) - with nonempty_yrhs + with ardenable_yrhs have "ardenable (Subst rhs Y (Arden Y yrhs))" - by (simp add:nonempty_yrhs - Subst_keeps_nonempty Arden_keeps_nonempty) + by (simp add:ardenable_yrhs + Subst_preserves_ardenable Arden_preserves_ardenable) } thus ?thesis by (auto simp add:ardenable_all_def Subst_all_def) qed show "finite_rhs (Subst_all ES Y (Arden Y yrhs))" @@ -557,13 +556,13 @@ proof - have "finite yrhs" using invariant_ES by (auto simp:invariant_def finite_rhs_def) - thus ?thesis using Arden_keeps_finite by auto + thus ?thesis using Arden_preserves_finite by auto qed ultimately show ?thesis - by (simp add:Subst_all_keeps_finite_rhs) + by (simp add:Subst_all_preserves_finite_rhs) qed show "validity (Subst_all ES Y (Arden Y yrhs))" - using invariant_ES Subst_all_keeps_validity by (auto simp add: invariant_def) + using invariant_ES Subst_all_preserves_validity by (auto simp add: invariant_def) qed lemma Remove_in_card_measure: @@ -734,14 +733,14 @@ 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 + using Arden_preserves_finite by auto then have fin: "finite {r. Lam r \ A}" by (rule finite_Lam) have "X = lang_rhs xrhs" using Inv_ES unfolding invariant_def soundness_def by simp then have "X = lang_rhs A" using Inv_ES unfolding A_def invariant_def ardenable_all_def finite_rhs_def - by (rule_tac Arden_keeps_eq) (simp_all add: finite_Trn) + by (rule_tac Arden_preserves_soundness) (simp_all add: finite_Trn) then have "X = lang_rhs {Lam r | r. Lam r \ A}" using eq by simp then have "X = lang (\{r. Lam r \ A})" using fin by auto then show "\r. X = lang r" by blast