Mercurial Mercurial > hg > regexp / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Derivatives.thy
changeset 179 edacc141060f
parent 174 2b414a8a7132
child 180 b755090d0f3d
equal deleted inserted replaced
178:c6ebfe052109 179:edacc141060f 
    12   "Delta A = (if [] \<in> A then {[]} else {})"
 
    12   "Delta A = (if [] \<in> A then {[]} else {})"
 
    13 
    13 
    14 definition
 
    14 definition
 
    15   Der :: "'a \<Rightarrow> 'a lang \<Rightarrow> 'a lang"
 
    15   Der :: "'a \<Rightarrow> 'a lang \<Rightarrow> 'a lang"
 
    16 where
 
    16 where
 
    17   "Der c A \<equiv> {s. [c] @ s \<in> A}"
 
    17   "Der c A \<equiv> {s'. [c] @ s' \<in> A}"
 
    18 
    18 
    19 definition
 
    19 definition
 
    20   Ders :: "'a list \<Rightarrow> 'a lang \<Rightarrow> 'a lang"
 
    20   Ders :: "'a list \<Rightarrow> 'a lang \<Rightarrow> 'a lang"
 
    21 where
 
    21 where
 
    22   "Ders s A \<equiv> {s'. s @ s' \<in> A}"
 
    22   "Ders s A \<equiv> {s'. s @ s' \<in> A}"
 
    75   also have "... =  (Der c A) \<cdot> A\<star>"
 
    75   also have "... =  (Der c A) \<cdot> A\<star>"
 
    76     using incl by auto
 
    76     using incl by auto
 
    77   finally show "Der c (A\<star>) = (Der c A) \<cdot> A\<star>" . 
    77   finally show "Der c (A\<star>) = (Der c A) \<cdot> A\<star>" . 
    78 qed
 
    78 qed
 
    79 
    79 
    80 
    80 lemma Ders_nil [simp]:
 
    81 lemma Ders_singleton:
 
    81   shows "Ders [] A = A"
 
    82   shows "Ders [c] A = Der c A"
 
    82 unfolding Ders_def by simp
 
    83 unfolding Der_def Ders_def
 
    83 
    84 by simp
 
    84 lemma Ders_cons [simp]:
 
    85 
    85   shows "Ders (c # s) A = Ders s (Der c A)"
 
    86 lemma Ders_append:
 
    86 unfolding Ders_def Der_def by auto
 
       
    87 
       
    88 lemma Ders_append [simp]:
 
    87   shows "Ders (s1 @ s2) A = Ders s2 (Ders s1 A)"
 
    89   shows "Ders (s1 @ s2) A = Ders s2 (Ders s1 A)"
 
    88 unfolding Ders_def by simp 
    90 unfolding Ders_def by simp 
    89 
       
    90 
       
    91 text {* Relating the Myhill-Nerode relation with left-quotients. *}
 
       
    92 
       
    93 lemma MN_Rel_Ders:
 
       
    94   shows "x \<approx>A y \<longleftrightarrow> Ders x A = Ders y A"
 
       
    95 unfolding Ders_def str_eq_def str_eq_rel_def
 
       
    96 by auto
 
       
    97 
    91 
    98 
    92 
    99 subsection {* Brozowsky's derivatives of regular expressions *}
 
    93 subsection {* Brozowsky's derivatives of regular expressions *}
 
   100 
    94 
   101 fun
 
    95 fun
 
   117 | "der c (Plus r1 r2) = Plus (der c r1) (der c r2)"
 
   111 | "der c (Plus r1 r2) = Plus (der c r1) (der c r2)"
 
   118 | "der c (Times r1 r2) = 
   112 | "der c (Times r1 r2) = 
   119     (if nullable r1 then Plus (Times (der c r1) r2) (der c r2) else Times (der c r1) r2)"
 
   113     (if nullable r1 then Plus (Times (der c r1) r2) (der c r2) else Times (der c r1) r2)"
 
   120 | "der c (Star r) = Times (der c r) (Star r)"
 
   114 | "der c (Star r) = Times (der c r) (Star r)"
 
   121 
   115 
   122 function 
   116 fun 
   123   ders :: "'a list \<Rightarrow> 'a rexp \<Rightarrow> 'a rexp"
 
   117   ders :: "'a list \<Rightarrow> 'a rexp \<Rightarrow> 'a rexp"
 
   124 where
 
   118 where
 
   125   "ders [] r = r"
 
   119   "ders [] r = r"
 
   126 | "ders (s @ [c]) r = der c (ders s r)"
 
   120 | "ders (c # s) r = ders s (der c r)"
 
   127 by (auto) (metis rev_cases)
 
   121 
   128 
       
   129 termination
 
       
   130   by (relation "measure (length o fst)") (auto)
 
       
   131 
   122 
   132 lemma Delta_nullable:
 
   123 lemma Delta_nullable:
 
   133   shows "Delta (lang r) = (if nullable r then {[]} else {})"
 
   124   shows "Delta (lang r) = (if nullable r then {[]} else {})"
 
   134 unfolding Delta_def
 
   125 unfolding Delta_def
 
   135 by (induct r) (auto simp add: conc_def split: if_splits)
 
   126 by (induct r) (auto simp add: conc_def split: if_splits)
 
   138   shows "Der c (lang r) = lang (der c r)"
 
   129   shows "Der c (lang r) = lang (der c r)"
 
   139 by (induct r) (simp_all add: Delta_nullable)
 
   130 by (induct r) (simp_all add: Delta_nullable)
 
   140 
   131 
   141 lemma Ders_ders:
 
   132 lemma Ders_ders:
 
   142   shows "Ders s (lang r) = lang (ders s r)"
 
   133   shows "Ders s (lang r) = lang (ders s r)"
 
   143 apply(induct s rule: rev_induct)
 
   134 by (induct s arbitrary: r) (simp_all add: Der_der)
 
   144 apply(simp add: Ders_def)
 
       
   145 apply(simp only: ders.simps)
 
       
   146 apply(simp only: Ders_append)
 
       
   147 apply(simp only: Ders_singleton)
 
       
   148 apply(simp only: Der_der)
 
       
   149 done
 
       
   150 
   135 
   151 
   136 
   152 subsection {* Antimirov's Partial Derivatives *}
 
   137 subsection {* Antimirov's Partial Derivatives *}
 
   153 
   138 
   154 abbreviation
 
   139 abbreviation
 
   159 where
 
   144 where
 
   160   "pder c Zero = {Zero}"
 
   145   "pder c Zero = {Zero}"
 
   161 | "pder c One = {Zero}"
 
   146 | "pder c One = {Zero}"
 
   162 | "pder c (Atom c') = (if c = c' then {One} else {Zero})"
 
   147 | "pder c (Atom c') = (if c = c' then {One} else {Zero})"
 
   163 | "pder c (Plus r1 r2) = (pder c r1) \<union> (pder c r2)"
 
   148 | "pder c (Plus r1 r2) = (pder c r1) \<union> (pder c r2)"
 
   164 | "pder c (Times r1 r2) = Times_set (pder c r1) r2 \<union> (if nullable r1 then pder c r2 else {})"
 
   149 | "pder c (Times r1 r2) = 
       
   150     (if nullable r1 then Times_set (pder c r1) r2 \<union>  pder c r2 else Times_set (pder c r1) r2)"
 
   165 | "pder c (Star r) = Times_set (pder c r) (Star r)"
 
   151 | "pder c (Star r) = Times_set (pder c r) (Star r)"
 
   166 
   152 
   167 abbreviation
 
   153 abbreviation
 
   168   "pder_set c rs \<equiv> \<Union>r \<in> rs. pder c r"
 
   154   "pder_set c rs \<equiv> \<Union>r \<in> rs. pder c r"
 
   169 
   155 
   170 function 
   156 fun
 
   171   pders :: "'a list \<Rightarrow> 'a rexp \<Rightarrow> ('a rexp) set"
 
   157   pders :: "'a list \<Rightarrow> 'a rexp \<Rightarrow> ('a rexp) set"
 
   172 where
 
   158 where
 
   173   "pders [] r = {r}"
 
   159   "pders [] r = {r}"
 
   174 | "pders (s @ [c]) r = pder_set c (pders s r)"
 
   160 | "pders (c # s) r = (\<Union>r'\<in> (pder c r). (pders s r'))"
 
   175 by (auto) (metis rev_cases)
 
       
   176 
       
   177 termination
 
       
   178   by (relation "measure (length o fst)") (auto)
 
       
   179 
   161 
   180 abbreviation
 
   162 abbreviation
 
   181   "pders_set A r \<equiv> \<Union>s \<in> A. pders s r"
 
   163   "pders_set A r \<equiv> \<Union>s \<in> A. pders s r"
 
   182 
   164 
   183 lemma pders_append:
 
   165 lemma pders_append:
 
   184   "pders (s1 @ s2) r = \<Union> (pders s2) ` (pders s1 r)"
 
   166   "pders (s1 @ s2) r = \<Union> (pders s2) ` (pders s1 r)"
 
   185 apply(induct s2 arbitrary: s1 r rule: rev_induct)
 
   167 by (induct s1 arbitrary: r) (simp_all)
 
   186 apply(simp)
 
   168 
   187 apply(subst append_assoc[symmetric])
 
   169 lemma pders_snoc:
 
   188 apply(simp only: pders.simps)
 
   170   shows "pders (s @ [c]) r = pder_set c (pders s r)"
 
   189 apply(auto)
 
   171 by (simp add: pders_append)
 
   190 done
 
       
   191 
       
   192 lemma pders_singleton:
 
       
   193   "pders [c] r = pder c r"
 
       
   194 apply(subst append_Nil[symmetric])
 
       
   195 apply(simp only: pders.simps)
 
       
   196 apply(simp)
 
       
   197 done
 
       
   198 
   172 
   199 lemma pders_set_lang:
 
   173 lemma pders_set_lang:
 
   200   shows "(\<Union> (lang ` pder_set c rs)) = (\<Union>r \<in> rs. (\<Union>lang ` (pder c r)))"
 
   174   shows "(\<Union> (lang ` pder_set c rs)) = (\<Union>r \<in> rs. (\<Union>lang ` (pder c r)))"
 
   201 unfolding image_def 
   175 unfolding image_def 
   202 by auto
 
   176 by auto
 
   203 
   177 
   204 lemma pders_Zero [simp]:
 
   178 lemma pders_Zero [simp]:
 
   205   shows "pders s Zero = {Zero}"
 
   179   shows "pders s Zero = {Zero}"
 
   206 by (induct s rule: rev_induct) (simp_all)
 
   180 by (induct s) (simp_all)
 
   207 
   181 
   208 lemma pders_One [simp]:
 
   182 lemma pders_One [simp]:
 
   209   shows "pders s One = (if s = [] then {One} else {Zero})"
 
   183   shows "pders s One = (if s = [] then {One} else {Zero})"
 
   210 by (induct s rule: rev_induct) (auto)
 
   184 by (induct s) (auto)
 
   211 
   185 
   212 lemma pders_Atom [simp]:
 
   186 lemma pders_Atom [simp]:
 
   213   shows "pders s (Atom c) = (if s = [] then {Atom c} else (if s = [c] then {One} else {Zero}))"
 
   187   shows "pders s (Atom c) = (if s = [] then {Atom c} else (if s = [c] then {One} else {Zero}))"
 
   214 by (induct s rule: rev_induct) (auto)
 
   188 by (induct s) (auto)
 
   215 
   189 
   216 lemma pders_Plus [simp]:
 
   190 lemma pders_Plus [simp]:
 
   217   shows "pders s (Plus r1 r2) = (if s = [] then {Plus r1 r2} else (pders s r1) \<union> (pders s r2))"
 
   191   shows "pders s (Plus r1 r2) = (if s = [] then {Plus r1 r2} else (pders s r1) \<union> (pders s r2))"
 
   218 by (induct s rule: rev_induct) (auto)
 
   192 by (induct s) (auto)
 
   219 
   193 
   220 text {* Non-empty suffixes of a string *}
 
   194 text {* Non-empty suffixes of a string *}
 
   221 
   195 
   222 definition
 
   196 definition
 
   223   "Suf s \<equiv> {v. v \<noteq> [] \<and> (\<exists>u. u @ v = s)}"
 
   197   "Suf s \<equiv> {v. v \<noteq> [] \<and> (\<exists>u. u @ v = s)}"
 
   235   shows "pders s (Times r1 r2) \<subseteq> Times_set (pders s r1) r2 \<union> (\<Union>v \<in> Suf s. pders v r2)"
 
   209   shows "pders s (Times r1 r2) \<subseteq> Times_set (pders s r1) r2 \<union> (\<Union>v \<in> Suf s. pders v r2)"
 
   236 proof (induct s rule: rev_induct)
 
   210 proof (induct s rule: rev_induct)
 
   237   case (snoc c s)
 
   211   case (snoc c s)
 
   238   have ih: "pders s (Times r1 r2) \<subseteq> Times_set (pders s r1) r2 \<union> (\<Union>v \<in> Suf s. pders v r2)" 
   212   have ih: "pders s (Times r1 r2) \<subseteq> Times_set (pders s r1) r2 \<union> (\<Union>v \<in> Suf s. pders v r2)" 
   239     by fact
 
   213     by fact
 
   240   have "pders (s @ [c]) (Times r1 r2) = pder_set c (pders s (Times r1 r2))" by simp
 
   214   have "pders (s @ [c]) (Times r1 r2) = pder_set c (pders s (Times r1 r2))" 
       
   215     by (simp add: pders_snoc)
 
   241   also have "\<dots> \<subseteq> pder_set c (Times_set (pders s r1) r2 \<union> (\<Union>v \<in> Suf s. pders v r2))"
 
   216   also have "\<dots> \<subseteq> pder_set c (Times_set (pders s r1) r2 \<union> (\<Union>v \<in> Suf s. pders v r2))"
 
   242     using ih by (auto) (blast)
 
   217     using ih by (auto) (blast)
 
   243   also have "\<dots> = pder_set c (Times_set (pders s r1) r2) \<union> pder_set c (\<Union>v \<in> Suf s. pders v r2)"
 
   218   also have "\<dots> = pder_set c (Times_set (pders s r1) r2) \<union> pder_set c (\<Union>v \<in> Suf s. pders v r2)"
 
   244     by (simp)
 
   219     by (simp)
 
   245   also have "\<dots> = pder_set c (Times_set (pders s r1) r2) \<union> (\<Union>v \<in> Suf s. pder_set c (pders v r2))"
 
   220   also have "\<dots> = pder_set c (Times_set (pders s r1) r2) \<union> (\<Union>v \<in> Suf s. pder_set c (pders v r2))"
 
   246     by (simp)
 
   221     by (simp)
 
   247   also have "\<dots> \<subseteq> pder_set c (Times_set (pders s r1) r2) \<union> (pder c r2) \<union> (\<Union>v \<in> Suf s. pders (v @ [c]) r2)"
 
   222   also have "\<dots> \<subseteq> pder_set c (Times_set (pders s r1) r2) \<union> (pder c r2) \<union> (\<Union>v \<in> Suf s. pders (v @ [c]) r2)"
 
   248     by (auto)
 
   223     by (auto simp add: pders_snoc)
 
   249   also have "\<dots> \<subseteq> Times_set (pder_set c (pders s r1)) r2 \<union> (pder c r2) \<union> (\<Union>v \<in> Suf s. pders (v @ [c]) r2)"
 
   224   also have "\<dots> \<subseteq> Times_set (pder_set c (pders s r1)) r2 \<union> (pder c r2) \<union> (\<Union>v \<in> Suf s. pders (v @ [c]) r2)"
 
   250     by (auto simp add: if_splits) (blast)
 
   225     by (auto simp add: if_splits) (blast)
 
   251   also have "\<dots> = Times_set (pders (s @ [c]) r1) r2 \<union> (\<Union>v \<in> Suf (s @ [c]). pders v r2)"
 
   226   also have "\<dots> = Times_set (pders (s @ [c]) r1) r2 \<union> (\<Union>v \<in> Suf (s @ [c]). pders v r2)"
 
   252     apply(subst (2) pders.simps)
 
   227     by (auto simp add: pders_snoc Suf Suf_Union)
 
   253     apply(simp only: Suf)
 
       
   254     apply(simp add: Suf_Union pders_singleton)
 
       
   255     apply(auto)
 
       
   256     done
 
       
   257   finally show ?case .
 
   228   finally show ?case .
 
   258 qed (simp)
 
   229 qed (simp)
 
   259 
   230 
   260 lemma pders_Star:
 
   231 lemma pders_Star:
 
   261   assumes a: "s \<noteq> []"
 
   232   assumes a: "s \<noteq> []"
 
   263 using a
 
   234 using a
 
   264 proof (induct s rule: rev_induct)
 
   235 proof (induct s rule: rev_induct)
 
   265   case (snoc c s)
 
   236   case (snoc c s)
 
   266   have ih: "s \<noteq> [] \<Longrightarrow> pders s (Star r) \<subseteq> (\<Union>v\<in>Suf s. Times_set (pders v r) (Star r))" by fact
 
   237   have ih: "s \<noteq> [] \<Longrightarrow> pders s (Star r) \<subseteq> (\<Union>v\<in>Suf s. Times_set (pders v r) (Star r))" by fact
 
   267   { assume asm: "s \<noteq> []"
 
   238   { assume asm: "s \<noteq> []"
 
   268     have "pders (s @ [c]) (Star r) = pder_set c (pders s (Star r))" by simp
 
   239     have "pders (s @ [c]) (Star r) = pder_set c (pders s (Star r))" by (simp add: pders_snoc)
 
   269     also have "\<dots> \<subseteq> (pder_set c (\<Union>v\<in>Suf s. Times_set (pders v r) (Star r)))"
 
   240     also have "\<dots> \<subseteq> (pder_set c (\<Union>v\<in>Suf s. Times_set (pders v r) (Star r)))"
 
   270       using ih[OF asm] by blast
 
   241       using ih[OF asm] by blast
 
   271     also have "\<dots> = (\<Union>v\<in>Suf s. pder_set c (Times_set (pders v r) (Star r)))"
 
   242     also have "\<dots> = (\<Union>v\<in>Suf s. pder_set c (Times_set (pders v r) (Star r)))"
 
   272       by simp
 
   243       by simp
 
   273     also have "\<dots> \<subseteq> (\<Union>v\<in>Suf s. (Times_set (pder_set c (pders v r)) (Star r) \<union> pder c (Star r)))"
 
   244     also have "\<dots> \<subseteq> (\<Union>v\<in>Suf s. (Times_set (pder_set c (pders v r)) (Star r) \<union> pder c (Star r)))"
 
   274       by (auto split: if_splits) 
   245       by (auto split: if_splits) 
   275     also have "\<dots> = (\<Union>v\<in>Suf s. (Times_set (pder_set c (pders v r)) (Star r))) \<union> pder c (Star r)"
 
   246     also have "\<dots> = (\<Union>v\<in>Suf s. (Times_set (pder_set c (pders v r)) (Star r))) \<union> pder c (Star r)"
 
   276       using asm by (auto simp add: Suf_def)
 
   247       using asm by (auto simp add: Suf_def)
 
   277     also have "\<dots> = (\<Union>v\<in>Suf s. (Times_set (pders (v @ [c]) r) (Star r))) \<union> (Times_set (pder c r) (Star r))"
 
   248     also have "\<dots> = (\<Union>v\<in>Suf s. (Times_set (pders (v @ [c]) r) (Star r))) \<union> (Times_set (pder c r) (Star r))"
 
   278       by simp
 
   249       by (simp add: pders_snoc)
 
   279     also have "\<dots> = (\<Union>v\<in>Suf (s @ [c]). (Times_set (pders v r) (Star r)))"
 
   250     also have "\<dots> = (\<Union>v\<in>Suf (s @ [c]). (Times_set (pders v r) (Star r)))"
 
   280       apply(simp only: Suf)
 
   251       by (auto simp add: Suf Suf_Union pders_snoc)
 
   281       apply(simp add: Suf_Union pders_singleton)
 
       
   282       apply(auto)
 
       
   283       done
 
       
   284     finally have ?case .
 
   252     finally have ?case .
 
   285   }
 
   253   }
 
   286   moreover
 
   254   moreover
 
   287   { assume asm: "s = []"
 
   255   { assume asm: "s = []"
 
   288     then have ?case
 
   256     then have ?case
 
   289       apply(simp add: pders_singleton Suf_def)
 
   257       by (auto simp add: pders_snoc Suf_def)
 
   290       apply(auto)
 
       
   291       apply(rule_tac x="[c]" in exI)
 
       
   292       apply(simp add: pders_singleton)
 
       
   293       done
 
       
   294   }
 
   258   }
 
   295   ultimately show ?case by blast
 
   259   ultimately show ?case by blast
 
   296 qed (simp)
 
   260 qed (simp)
 
   297 
   261 
   298 abbreviation 
   262 definition
 
   299   "UNIV1 \<equiv> UNIV - {[]}"
 
   263   "UNIV1 \<equiv> UNIV - {[]}"
 
   300 
   264 
   301 lemma pders_set_Zero:
 
   265 lemma pders_set_Zero:
 
   302   shows "pders_set UNIV1 Zero = {Zero}"
 
   266   shows "pders_set UNIV1 Zero = {Zero}"
 
   303 by auto
 
   267 unfolding UNIV1_def by auto
 
   304 
   268 
   305 lemma pders_set_One:
 
   269 lemma pders_set_One:
 
   306   shows "pders_set UNIV1 One = {Zero}"
 
   270   shows "pders_set UNIV1 One = {Zero}"
 
   307 by (auto split: if_splits)
 
   271 unfolding UNIV1_def by (auto split: if_splits)
 
   308 
   272 
   309 lemma pders_set_Atom:
 
   273 lemma pders_set_Atom:
 
   310   shows "pders_set UNIV1 (Atom c) \<subseteq> {One, Zero}"
 
   274   shows "pders_set UNIV1 (Atom c) \<subseteq> {One, Zero}"
 
   311 by (auto split: if_splits)
 
   275 unfolding UNIV1_def by (auto split: if_splits)
 
   312 
   276 
   313 lemma pders_set_Plus:
 
   277 lemma pders_set_Plus:
 
   314   shows "pders_set UNIV1 (Plus r1 r2) = pders_set UNIV1 r1 \<union> pders_set UNIV1 r2"
 
   278   shows "pders_set UNIV1 (Plus r1 r2) = pders_set UNIV1 r1 \<union> pders_set UNIV1 r2"
 
   315 by auto
 
   279 unfolding UNIV1_def by auto
 
   316 
   280 
   317 lemma pders_set_Times_aux:
 
   281 lemma pders_set_Times_aux:
 
   318   assumes a: "s \<in> UNIV1"
 
   282   assumes a: "s \<in> UNIV1"
 
   319   shows "pders_set (Suf s) r2 \<subseteq> pders_set UNIV1 r2"
 
   283   shows "pders_set (Suf s) r2 \<subseteq> pders_set UNIV1 r2"
 
   320 using a by (auto simp add: Suf_def)
 
   284 using a unfolding UNIV1_def Suf_def by (auto)
 
   321 
   285 
   322 lemma pders_set_Times:
 
   286 lemma pders_set_Times:
 
   323   shows "pders_set UNIV1 (Times r1 r2) \<subseteq> Times_set (pders_set UNIV1 r1) r2 \<union> pders_set UNIV1 r2"
 
   287   shows "pders_set UNIV1 (Times r1 r2) \<subseteq> Times_set (pders_set UNIV1 r1) r2 \<union> pders_set UNIV1 r2"
 
       
   288 unfolding UNIV1_def
 
   324 apply(rule UN_least)
 
   289 apply(rule UN_least)
 
   325 apply(rule subset_trans)
 
   290 apply(rule subset_trans)
 
   326 apply(rule pders_Times)
 
   291 apply(rule pders_Times)
 
   327 apply(simp)
 
   292 apply(simp)
 
   328 apply(rule conjI) 
   293 apply(rule conjI) 
   329 apply(auto)[1]
 
   294 apply(auto)[1]
 
   330 apply(rule subset_trans)
 
   295 apply(rule subset_trans)
 
   331 apply(rule pders_set_Times_aux)
 
   296 apply(rule pders_set_Times_aux)
 
   332 apply(auto)
 
   297 apply(auto simp add: UNIV1_def)
 
   333 done
 
   298 done
 
   334 
   299 
   335 lemma pders_set_Star:
 
   300 lemma pders_set_Star:
 
   336   shows "pders_set UNIV1 (Star r) \<subseteq> Times_set (pders_set UNIV1 r) (Star r)"
 
   301   shows "pders_set UNIV1 (Star r) \<subseteq> Times_set (pders_set UNIV1 r) (Star r)"
 
       
   302 unfolding UNIV1_def
 
   337 apply(rule UN_least)
 
   303 apply(rule UN_least)
 
   338 apply(rule subset_trans)
 
   304 apply(rule subset_trans)
 
   339 apply(rule pders_Star)
 
   305 apply(rule pders_Star)
 
   340 apply(simp)
 
   306 apply(simp)
 
   341 apply(simp add: Suf_def)
 
   307 apply(simp add: Suf_def)
 
   367 apply(simp only: finite_Times_set)
 
   333 apply(simp only: finite_Times_set)
 
   368 done
 
   334 done
 
   369     
   335     
   370 lemma pders_set_UNIV_UNIV1:
 
   336 lemma pders_set_UNIV_UNIV1:
 
   371   shows "pders_set UNIV r = pders [] r \<union> pders_set UNIV1 r"
 
   337   shows "pders_set UNIV r = pders [] r \<union> pders_set UNIV1 r"
 
       
   338 unfolding UNIV1_def
 
   372 apply(auto)
 
   339 apply(auto)
 
   373 apply(rule_tac x="[]" in exI)
 
   340 apply(rule_tac x="[]" in exI)
 
   374 apply(simp)
 
   341 apply(simp)
 
   375 done
 
   342 done
 
   376 
   343 
   416   case (snoc c s)
 
   383   case (snoc c s)
 
   417   have ih: "Ders s (lang r) = \<Union> lang ` (pders s r)" by fact
 
   384   have ih: "Ders s (lang r) = \<Union> lang ` (pders s r)" by fact
 
   418   have "Ders (s @ [c]) (lang r) = Ders [c] (Ders s (lang r))"
 
   385   have "Ders (s @ [c]) (lang r) = Ders [c] (Ders s (lang r))"
 
   419     by (simp add: Ders_append)
 
   386     by (simp add: Ders_append)
 
   420   also have "\<dots> = Der c (\<Union> lang ` (pders s r))" using ih
 
   387   also have "\<dots> = Der c (\<Union> lang ` (pders s r))" using ih
 
   421     by (simp add: Ders_singleton)
 
   388     by (simp)
 
   422   also have "\<dots> = (\<Union>r\<in>pders s r. Der c (lang r))" 
   389   also have "\<dots> = (\<Union>r\<in>pders s r. Der c (lang r))" 
   423     unfolding Der_def image_def by auto
 
   390     unfolding Der_def image_def by auto
 
   424   also have "\<dots> = (\<Union>r\<in>pders s r. (\<Union> lang `  (pder c r)))"
 
   391   also have "\<dots> = (\<Union>r\<in>pders s r. (\<Union> lang `  (pder c r)))"
 
   425     by (simp add: Der_pder)
 
   392     by (simp add: Der_pder)
 
   426   also have "\<dots> = (\<Union>lang ` (pder_set c (pders s r)))"
 
   393   also have "\<dots> = (\<Union>lang ` (pder_set c (pders s r)))"
 
   427     by (simp add: pders_set_lang)
 
   394     by (simp add: pders_set_lang)
 
   428   also have "\<dots> = (\<Union>lang ` (pders (s @ [c]) r))"
 
   395   also have "\<dots> = (\<Union>lang ` (pders (s @ [c]) r))"
 
   429     by simp
 
   396     by (simp add: pders_snoc)
 
   430   finally show "Ders (s @ [c]) (lang r) = \<Union> lang ` pders (s @ [c]) r" .
 
   397   finally show "Ders (s @ [c]) (lang r) = \<Union> lang ` pders (s @ [c]) r" .
 
   431 qed (simp add: Ders_def)
 
   398 qed (simp add: Ders_def)
 
   432 
   399 
   433 lemma Ders_set_pders_set:
 
   400 lemma Ders_set_pders_set:
 
   434   shows "Ders_set A (lang r) = (\<Union> lang ` (pders_set A r))"
 
   401   shows "Ders_set A (lang r) = (\<Union> lang ` (pders_set A r))"
 
   444 lemma
 
   411 lemma
 
   445   shows "(\<Union> lang ` (pders s r)) = lang (ders s r)"
 
   412   shows "(\<Union> lang ` (pders s r)) = lang (ders s r)"
 
   446 unfolding Ders_ders[symmetric] Ders_pders by simp
 
   413 unfolding Ders_ders[symmetric] Ders_pders by simp
 
   447 
   414 
   448 
   415 
       
   416 text {* Relating the Myhill-Nerode relation with left-quotients. *}
 
       
   417 
       
   418 lemma MN_Rel_Ders:
 
       
   419   shows "x \<approx>A y \<longleftrightarrow> Ders x A = Ders y A"
 
       
   420 unfolding Ders_def str_eq_def str_eq_rel_def
 
       
   421 by auto
 
   449 
   422 
   450 subsection {*
 
   423 subsection {*
 
   451   The second direction of the Myhill-Nerode theorem using
 
   424   The second direction of the Myhill-Nerode theorem using
 
   452   partial derivatives.
 
   425   partial derivatives.
 
   453 *}
 
   426 *}
 
   486     by auto
 
   459     by auto
 
   487   ultimately show "finite (UNIV // \<approx>(lang r))" 
   460   ultimately show "finite (UNIV // \<approx>(lang r))" 
   488     by (rule refined_partition_finite)
 
   461     by (rule refined_partition_finite)
 
   489 qed
 
   462 qed
 
   490 
   463 
       
   464 
   491 end
 
   465 end
regexp