# HG changeset patch # User urbanc # Date 1313058379 0 # Node ID f6a603be52d6dad560a90ceb3d30e0b13952ee2a # Parent b73478aaf33e178eeac057865d3b89ebc8dfa6e7 slight polishing diff -r b73478aaf33e -r f6a603be52d6 Closures.thy --- a/Closures.thy Tue Aug 09 22:15:11 2011 +0000 +++ b/Closures.thy Thu Aug 11 10:26:19 2011 +0000 @@ -153,7 +153,7 @@ have fin: "finite (pders_lang B r)" by (rule finite_pders_lang) have "Ders_lang B (lang r) = (\<Union> lang ` (pders_lang B r))" - by (simp add: Ders_pders) + by (simp add: Ders_pders pders_lang_def) also have "\<dots> = lang (\<Uplus>(pders_lang B r))" using fin by simp finally have "Ders_lang B A = lang (\<Uplus>(pders_lang B r))" using eq by simp diff -r b73478aaf33e -r f6a603be52d6 Derivatives.thy --- a/Derivatives.thy Tue Aug 09 22:15:11 2011 +0000 +++ b/Derivatives.thy Thu Aug 11 10:26:19 2011 +0000 @@ -184,10 +184,39 @@ subsection {* There are only finitely many partial derivatives for a language *} -abbreviation +definition "pders_lang A r \<equiv> \<Union>s \<in> A. pders s r" -text {* Non-empty suffixes of a string *} +lemma pders_lang_subsetI [intro]: + assumes "\<And>s. s \<in> A \<Longrightarrow> pders s r \<subseteq> C" + shows "pders_lang A r \<subseteq> C" +using assms unfolding pders_lang_def by (rule UN_least) + +lemma pders_lang_union: + shows "pders_lang (A \<union> B) r = (pders_lang A r \<union> pders_lang B r)" +by (simp add: pders_lang_def) + +definition + "UNIV1 \<equiv> UNIV - {[]}" + +lemma pders_lang_Zero [simp]: + shows "pders_lang UNIV1 Zero = {Zero}" +unfolding UNIV1_def pders_lang_def by auto + +lemma pders_lang_One [simp]: + shows "pders_lang UNIV1 One = {Zero}" +unfolding UNIV1_def pders_lang_def by (auto split: if_splits) + +lemma pders_lang_Atom: + shows "pders_lang UNIV1 (Atom c) \<subseteq> {One, Zero}" +unfolding UNIV1_def pders_lang_def by (auto split: if_splits) + +lemma pders_lang_Plus [simp]: + shows "pders_lang UNIV1 (Plus r1 r2) = pders_lang UNIV1 r1 \<union> pders_lang UNIV1 r2" +unfolding UNIV1_def pders_lang_def by auto + + +text {* Non-empty suffixes of a string (needed for teh cases of @{const Times} and @{const Star} *} definition "Suf s \<equiv> {v. v \<noteq> [] \<and> (\<exists>u. u @ v = s)}" @@ -203,6 +232,7 @@ lemma pders_lang_snoc: shows "pders_lang (Suf s \<cdot> {[c]}) r = (pder_set c (pders_lang (Suf s) r))" +unfolding pders_lang_def by (simp add: Suf_Union pders_snoc) lemma pders_Times: @@ -226,10 +256,29 @@ also have "\<dots> = Timess (pders (s @ [c]) r1) r2 \<union> pder c r2 \<union> pders_lang (Suf s \<cdot> {[c]}) r2" by (simp add: pders_snoc) also have "\<dots> \<subseteq> Timess (pders (s @ [c]) r1) r2 \<union> pders_lang (Suf (s @ [c])) r2" - by (auto simp add: Suf_snoc) + unfolding pders_lang_def by (auto simp add: Suf_snoc) finally show ?case . qed (simp) +lemma pders_lang_Times_aux1: + assumes a: "s \<in> UNIV1" + shows "pders_lang (Suf s) r \<subseteq> pders_lang UNIV1 r" +using a unfolding UNIV1_def Suf_def pders_lang_def by auto + +lemma pders_lang_Times_aux2: + assumes a: "s \<in> UNIV1" + shows "Timess (pders s r1) r2 \<subseteq> Timess (pders_lang UNIV1 r1) r2" +using a unfolding pders_lang_def by auto + +lemma pders_lang_Times [intro]: + shows "pders_lang UNIV1 (Times r1 r2) \<subseteq> Timess (pders_lang UNIV1 r1) r2 \<union> pders_lang UNIV1 r2" +apply(rule pders_lang_subsetI) +apply(rule subset_trans) +apply(rule pders_Times) +using pders_lang_Times_aux1 pders_lang_Times_aux2 +apply(blast) +done + lemma pders_Star: assumes a: "s \<noteq> []" shows "pders s (Star r) \<subseteq> Timess (pders_lang (Suf s) r) (Star r)" @@ -244,15 +293,16 @@ also have "\<dots> \<subseteq> Timess (pder_set c (pders_lang (Suf s) r)) (Star r) \<union> pder c (Star r)" by (auto split: if_splits) (blast)+ also have "\<dots> \<subseteq> Timess (pders_lang (Suf (s @ [c])) r) (Star r) \<union> (Timess (pder c r) (Star r))" - by (auto simp add: Suf_snoc pders_lang_snoc) + by (simp only: Suf_snoc pders_lang_snoc pders_lang_union) + (auto simp add: pders_lang_def) also have "\<dots> = Timess (pders_lang (Suf (s @ [c])) r) (Star r)" - by (auto simp add: Suf_snoc Suf_Union pders_snoc) + by (auto simp add: Suf_snoc Suf_Union pders_snoc pders_lang_def) finally have ?case . } moreover { assume asm: "s = []" then have ?case - apply (auto simp add: pders_snoc Suf_def) + apply (auto simp add: pders_lang_def pders_snoc Suf_def) apply(rule_tac x = "[c]" in exI) apply(auto) done @@ -260,56 +310,17 @@ ultimately show ?case by blast qed (simp) -definition - "UNIV1 \<equiv> UNIV - {[]}" - -lemma pders_lang_Zero [simp]: - shows "pders_lang UNIV1 Zero = {Zero}" -unfolding UNIV1_def by auto - -lemma pders_lang_One [simp]: - shows "pders_lang UNIV1 One = {Zero}" -unfolding UNIV1_def by (auto split: if_splits) - -lemma pders_lang_Atom: - shows "pders_lang UNIV1 (Atom c) \<subseteq> {One, Zero}" -unfolding UNIV1_def by (auto split: if_splits) - -lemma pders_lang_Plus: - shows "pders_lang UNIV1 (Plus r1 r2) = pders_lang UNIV1 r1 \<union> pders_lang UNIV1 r2" -unfolding UNIV1_def by auto - -lemma pders_lang_Times_aux: - assumes a: "s \<in> UNIV1" - shows "pders_lang (Suf s) r \<subseteq> pders_lang UNIV1 r" -using a unfolding UNIV1_def Suf_def by auto - -lemma pders_lang_Times [intro]: - shows "pders_lang UNIV1 (Times r1 r2) \<subseteq> Timess (pders_lang UNIV1 r1) r2 \<union> pders_lang UNIV1 r2" -unfolding UNIV1_def -apply(rule UN_least) +lemma pders_lang_Star [intro]: + shows "pders_lang UNIV1 (Star r) \<subseteq> Timess (pders_lang UNIV1 r) (Star r)" +apply(rule pders_lang_subsetI) apply(rule subset_trans) -apply(rule pders_Times) -apply(simp) -apply(rule conjI) -apply(auto)[1] -apply(rule subset_trans) -apply(rule pders_lang_Times_aux) -apply(auto simp add: UNIV1_def) +apply(rule pders_Star) +apply(simp add: UNIV1_def) +apply(simp add: UNIV1_def Suf_def) +apply(auto simp add: pders_lang_def) done -lemma pders_lang_Star [intro]: - shows "pders_lang UNIV1 (Star r) \<subseteq> Timess (pders_lang UNIV1 r) (Star r)" -unfolding UNIV1_def -apply(rule UN_least) -apply(rule subset_trans) -apply(rule pders_Star) -apply(simp) -apply(simp add: Suf_def) -apply(auto) -done - -lemma finite_Timess: +lemma finite_Timess [simp]: assumes a: "finite A" shows "finite (Timess A r)" using a by auto @@ -318,60 +329,33 @@ shows "finite (pders_lang UNIV1 r)" apply(induct r) apply(simp) -apply(simp only: pders_lang_One) apply(simp) -apply(rule finite_subset) -apply(rule pders_lang_Atom) +apply(rule finite_subset[OF pders_lang_Atom]) apply(simp) -apply(simp only: pders_lang_Plus) apply(simp) -apply(rule finite_subset) -apply(rule pders_lang_Times) -apply(simp only: finite_Timess finite_Un) +apply(rule finite_subset[OF pders_lang_Times]) apply(simp) -apply(rule finite_subset) -apply(rule pders_lang_Star) -apply(simp only: finite_Timess) +apply(rule finite_subset[OF pders_lang_Star]) +apply(simp) done -lemma pders_lang_UNIV_UNIV1: +lemma pders_lang_UNIV: shows "pders_lang UNIV r = pders [] r \<union> pders_lang UNIV1 r" -unfolding UNIV1_def -apply(auto) -apply(rule_tac x="[]" in exI) -apply(simp) -done +unfolding UNIV1_def pders_lang_def +by blast lemma finite_pders_lang_UNIV: shows "finite (pders_lang UNIV r)" -unfolding pders_lang_UNIV_UNIV1 +unfolding pders_lang_UNIV by (simp add: finite_pders_lang_UNIV1) lemma finite_pders_lang: shows "finite (pders_lang A r)" apply(rule rev_finite_subset) apply(rule_tac r="r" in finite_pders_lang_UNIV) -apply(auto) +apply(auto simp add: pders_lang_def) done -lemma finite_pders: - shows "finite (pders s r)" -using finite_pders_lang[where A="{s}" and r="r"] -by simp - -lemma finite_pders2: - shows "finite {pders s r | s. s \<in> A}" -proof - - have "{pders s r | s. s \<in> A} \<subseteq> Pow (pders_lang A r)" by auto - moreover - have "finite (Pow (pders_lang A r))" - using finite_pders_lang by simp - ultimately - show "finite {pders s r | s. s \<in> A}" - by(rule finite_subset) -qed - - text {* Relating the Myhill-Nerode relation with left-quotients. *} lemma MN_Rel_Ders: @@ -390,12 +374,13 @@ proof - have "finite (UNIV // =(\<lambda>x. pders x r)=)" proof - - have "range (\<lambda>x. pders x r) = {pders s r | s. s \<in> UNIV}" by auto + have "range (\<lambda>x. pders x r) \<subseteq> Pow (pders_lang UNIV r)" + unfolding pders_lang_def by auto moreover - have "finite {pders s r | s. s \<in> UNIV}" by (rule finite_pders2) + have "finite (Pow (pders_lang UNIV r))" by (simp add: finite_pders_lang) ultimately have "finite (range (\<lambda>x. pders x r))" - by simp + by (simp add: finite_subset) then show "finite (UNIV // =(\<lambda>x. pders x r)=)" by (rule finite_eq_tag_rel) qed