113 "Timess rs r \<equiv> {Times r' r | r'. r' \<in> rs}" |
113 "Timess rs r \<equiv> {Times r' r | r'. r' \<in> rs}" |
114 |
114 |
115 fun |
115 fun |
116 pder :: "'a \<Rightarrow> 'a rexp \<Rightarrow> ('a rexp) set" |
116 pder :: "'a \<Rightarrow> 'a rexp \<Rightarrow> ('a rexp) set" |
117 where |
117 where |
118 "pder c Zero = {Zero}" |
118 "pder c Zero = {}" |
119 | "pder c One = {Zero}" |
119 | "pder c One = {}" |
120 | "pder c (Atom c') = (if c = c' then {One} else {Zero})" |
120 | "pder c (Atom c') = (if c = c' then {One} else {})" |
121 | "pder c (Plus r1 r2) = (pder c r1) \<union> (pder c r2)" |
121 | "pder c (Plus r1 r2) = (pder c r1) \<union> (pder c r2)" |
122 | "pder c (Times r1 r2) = |
122 | "pder c (Times r1 r2) = |
123 (if nullable r1 then Timess (pder c r1) r2 \<union> pder c r2 else Timess (pder c r1) r2)" |
123 (if nullable r1 then Timess (pder c r1) r2 \<union> pder c r2 else Timess (pder c r1) r2)" |
124 | "pder c (Star r) = Timess (pder c r) (Star r)" |
124 | "pder c (Star r) = Timess (pder c r) (Star r)" |
125 |
125 |
126 abbreviation |
126 abbreviation |
127 "pder_set c rs \<equiv> \<Union> pder c ` rs" |
127 "pder_set c rs \<equiv> \<Union> pder c ` rs" |
128 |
128 |
142 lemma pders_snoc: |
142 lemma pders_snoc: |
143 shows "pders (s @ [c]) r = pder_set c (pders s r)" |
143 shows "pders (s @ [c]) r = pder_set c (pders s r)" |
144 by (simp add: pders_append) |
144 by (simp add: pders_append) |
145 |
145 |
146 lemma pders_simps [simp]: |
146 lemma pders_simps [simp]: |
147 shows "pders s Zero = {Zero}" |
147 shows "pders s Zero = (if s= [] then {Zero} else {})" |
148 and "pders s One = (if s = [] then {One} else {Zero})" |
148 and "pders s One = (if s = [] then {One} else {})" |
149 and "pders s (Atom c) = (if s = [] then {Atom c} else (if s = [c] then {One} else {Zero}))" |
|
150 and "pders s (Plus r1 r2) = (if s = [] then {Plus r1 r2} else (pders s r1) \<union> (pders s r2))" |
149 and "pders s (Plus r1 r2) = (if s = [] then {Plus r1 r2} else (pders s r1) \<union> (pders s r2))" |
151 by (induct s) (auto) |
150 by (induct s) (simp_all) |
|
151 |
|
152 lemma pders_Atom [intro]: |
|
153 shows "pders s (Atom c) \<subseteq> {Atom c, One}" |
|
154 by (induct s) (simp_all) |
152 |
155 |
153 subsection {* Relating left-quotients and partial derivatives *} |
156 subsection {* Relating left-quotients and partial derivatives *} |
154 |
157 |
155 lemma Der_pder: |
158 lemma Der_pder: |
156 shows "Der c (lang r) = \<Union> lang ` (pder c r)" |
159 shows "Der c (lang r) = \<Union> lang ` (pder c r)" |
183 |
186 |
184 |
187 |
185 subsection {* There are only finitely many partial derivatives for a language *} |
188 subsection {* There are only finitely many partial derivatives for a language *} |
186 |
189 |
187 definition |
190 definition |
188 "pders_lang A r \<equiv> \<Union>s \<in> A. pders s r" |
191 "pders_lang A r \<equiv> \<Union>x \<in> A. pders x r" |
189 |
192 |
190 lemma pders_lang_subsetI [intro]: |
193 lemma pders_lang_subsetI [intro]: |
191 assumes "\<And>s. s \<in> A \<Longrightarrow> pders s r \<subseteq> C" |
194 assumes "\<And>s. s \<in> A \<Longrightarrow> pders s r \<subseteq> C" |
192 shows "pders_lang A r \<subseteq> C" |
195 shows "pders_lang A r \<subseteq> C" |
193 using assms unfolding pders_lang_def by (rule UN_least) |
196 using assms unfolding pders_lang_def by (rule UN_least) |
194 |
197 |
195 lemma pders_lang_union: |
198 lemma pders_lang_union: |
196 shows "pders_lang (A \<union> B) r = (pders_lang A r \<union> pders_lang B r)" |
199 shows "pders_lang (A \<union> B) r = (pders_lang A r \<union> pders_lang B r)" |
197 by (simp add: pders_lang_def) |
200 by (simp add: pders_lang_def) |
198 |
201 |
|
202 lemma pders_lang_subset: |
|
203 shows "A \<subseteq> B \<Longrightarrow> pders_lang A r \<subseteq> pders_lang B r" |
|
204 by (auto simp add: pders_lang_def) |
|
205 |
199 definition |
206 definition |
200 "UNIV1 \<equiv> UNIV - {[]}" |
207 "UNIV1 \<equiv> UNIV - {[]}" |
201 |
208 |
202 lemma pders_lang_Zero [simp]: |
209 lemma pders_lang_Zero [simp]: |
203 shows "pders_lang UNIV1 Zero = {Zero}" |
210 shows "pders_lang UNIV1 Zero = {}" |
204 unfolding UNIV1_def pders_lang_def by auto |
211 unfolding UNIV1_def pders_lang_def by auto |
205 |
212 |
206 lemma pders_lang_One [simp]: |
213 lemma pders_lang_One [simp]: |
207 shows "pders_lang UNIV1 One = {Zero}" |
214 shows "pders_lang UNIV1 One = {}" |
208 unfolding UNIV1_def pders_lang_def by (auto split: if_splits) |
215 unfolding UNIV1_def pders_lang_def by (auto split: if_splits) |
209 |
216 |
210 lemma pders_lang_Atom: |
217 lemma pders_lang_Atom [simp]: |
211 shows "pders_lang UNIV1 (Atom c) \<subseteq> {One, Zero}" |
218 shows "pders_lang UNIV1 (Atom c) = {One}" |
212 unfolding UNIV1_def pders_lang_def by (auto split: if_splits) |
219 unfolding UNIV1_def pders_lang_def |
|
220 apply(auto) |
|
221 apply(frule rev_subsetD) |
|
222 apply(rule pders_Atom) |
|
223 apply(simp) |
|
224 apply(case_tac xa) |
|
225 apply(auto split: if_splits) |
|
226 done |
213 |
227 |
214 lemma pders_lang_Plus [simp]: |
228 lemma pders_lang_Plus [simp]: |
215 shows "pders_lang UNIV1 (Plus r1 r2) = pders_lang UNIV1 r1 \<union> pders_lang UNIV1 r2" |
229 shows "pders_lang UNIV1 (Plus r1 r2) = pders_lang UNIV1 r1 \<union> pders_lang UNIV1 r2" |
216 unfolding UNIV1_def pders_lang_def by auto |
230 unfolding UNIV1_def pders_lang_def by auto |
217 |
231 |
326 using a by auto |
340 using a by auto |
327 |
341 |
328 lemma finite_pders_lang_UNIV1: |
342 lemma finite_pders_lang_UNIV1: |
329 shows "finite (pders_lang UNIV1 r)" |
343 shows "finite (pders_lang UNIV1 r)" |
330 apply(induct r) |
344 apply(induct r) |
331 apply(simp) |
345 apply(simp_all add: |
332 apply(simp) |
346 finite_subset[OF pders_lang_Times] |
333 apply(rule finite_subset[OF pders_lang_Atom]) |
347 finite_subset[OF pders_lang_Star]) |
334 apply(simp) |
|
335 apply(simp) |
|
336 apply(rule finite_subset[OF pders_lang_Times]) |
|
337 apply(simp) |
|
338 apply(rule finite_subset[OF pders_lang_Star]) |
|
339 apply(simp) |
|
340 done |
348 done |
341 |
349 |
342 lemma pders_lang_UNIV: |
350 lemma pders_lang_UNIV: |
343 shows "pders_lang UNIV r = pders [] r \<union> pders_lang UNIV1 r" |
351 shows "pders_lang UNIV r = pders [] r \<union> pders_lang UNIV1 r" |
344 unfolding UNIV1_def pders_lang_def |
352 unfolding UNIV1_def pders_lang_def |
349 unfolding pders_lang_UNIV |
357 unfolding pders_lang_UNIV |
350 by (simp add: finite_pders_lang_UNIV1) |
358 by (simp add: finite_pders_lang_UNIV1) |
351 |
359 |
352 lemma finite_pders_lang: |
360 lemma finite_pders_lang: |
353 shows "finite (pders_lang A r)" |
361 shows "finite (pders_lang A r)" |
354 apply(rule rev_finite_subset) |
362 apply(rule rev_finite_subset[OF finite_pders_lang_UNIV]) |
355 apply(rule_tac r="r" in finite_pders_lang_UNIV) |
363 apply(rule pders_lang_subset) |
356 apply(auto simp add: pders_lang_def) |
364 apply(simp) |
357 done |
365 done |
358 |
366 |
359 text {* Relating the Myhill-Nerode relation with left-quotients. *} |
367 text {* Relating the Myhill-Nerode relation with left-quotients. *} |
360 |
368 |
361 lemma MN_Rel_Ders: |
369 lemma MN_Rel_Ders: |