equal
deleted
inserted
replaced
113 lemma Derivs_derivs: |
113 lemma Derivs_derivs: |
114 shows "Derivs s (lang r) = lang (derivs s r)" |
114 shows "Derivs s (lang r) = lang (derivs s r)" |
115 by (induct s arbitrary: r) (simp_all add: Deriv_deriv) |
115 by (induct s arbitrary: r) (simp_all add: Deriv_deriv) |
116 |
116 |
117 |
117 |
118 subsection {* Antimirov's partial derivivatives *} |
118 subsection {* Antimirov's partial derivatives *} |
119 |
119 |
120 abbreviation |
120 abbreviation |
121 "Timess rs r \<equiv> {Times r' r | r'. r' \<in> rs}" |
121 "Timess rs r \<equiv> {Times r' r | r'. r' \<in> rs}" |
122 |
122 |
123 fun |
123 fun |
163 |
163 |
164 lemma pderivs_Atom: |
164 lemma pderivs_Atom: |
165 shows "pderivs s (Atom c) \<subseteq> {Atom c, One}" |
165 shows "pderivs s (Atom c) \<subseteq> {Atom c, One}" |
166 by (induct s) (simp_all) |
166 by (induct s) (simp_all) |
167 |
167 |
168 subsection {* Relating left-quotients and partial derivivatives *} |
168 subsection {* Relating left-quotients and partial derivatives *} |
169 |
169 |
170 lemma Deriv_pderiv: |
170 lemma Deriv_pderiv: |
171 shows "Deriv c (lang r) = \<Union> lang ` (pderiv c r)" |
171 shows "Deriv c (lang r) = \<Union> lang ` (pderiv c r)" |
172 by (induct r) (auto simp add: nullable_iff conc_UNION_distrib) |
172 by (induct r) (auto simp add: nullable_iff conc_UNION_distrib) |
173 |
173 |
184 using ih by auto |
184 using ih by auto |
185 also have "\<dots> = \<Union> lang ` (pderivs (c # s) r)" by simp |
185 also have "\<dots> = \<Union> lang ` (pderivs (c # s) r)" by simp |
186 finally show "Derivs (c # s) (lang r) = \<Union> lang ` pderivs (c # s) r" . |
186 finally show "Derivs (c # s) (lang r) = \<Union> lang ` pderivs (c # s) r" . |
187 qed (simp add: Derivs_def) |
187 qed (simp add: Derivs_def) |
188 |
188 |
189 subsection {* Relating derivivatives and partial derivivatives *} |
189 subsection {* Relating derivatives and partial derivatives *} |
190 |
190 |
191 lemma deriv_pderiv: |
191 lemma deriv_pderiv: |
192 shows "(\<Union> lang ` (pderiv c r)) = lang (deriv c r)" |
192 shows "(\<Union> lang ` (pderiv c r)) = lang (deriv c r)" |
193 unfolding Deriv_deriv[symmetric] Deriv_pderiv by simp |
193 unfolding Deriv_deriv[symmetric] Deriv_pderiv by simp |
194 |
194 |
195 lemma derivs_pderivs: |
195 lemma derivs_pderivs: |
196 shows "(\<Union> lang ` (pderivs s r)) = lang (derivs s r)" |
196 shows "(\<Union> lang ` (pderivs s r)) = lang (derivs s r)" |
197 unfolding Derivs_derivs[symmetric] Derivs_pderivs by simp |
197 unfolding Derivs_derivs[symmetric] Derivs_pderivs by simp |
198 |
198 |
199 |
199 |
200 subsection {* Finiteness property of partial derivivatives *} |
200 subsection {* Finiteness property of partial derivatives *} |
201 |
201 |
202 definition |
202 definition |
203 pderivs_lang :: "'a lang \<Rightarrow> 'a rexp \<Rightarrow> 'a rexp set" |
203 pderivs_lang :: "'a lang \<Rightarrow> 'a rexp \<Rightarrow> 'a rexp set" |
204 where |
204 where |
205 "pderivs_lang A r \<equiv> \<Union>x \<in> A. pderivs x r" |
205 "pderivs_lang A r \<equiv> \<Union>x \<in> A. pderivs x r" |
242 lemma pderivs_lang_Plus [simp]: |
242 lemma pderivs_lang_Plus [simp]: |
243 shows "pderivs_lang UNIV1 (Plus r1 r2) = pderivs_lang UNIV1 r1 \<union> pderivs_lang UNIV1 r2" |
243 shows "pderivs_lang UNIV1 (Plus r1 r2) = pderivs_lang UNIV1 r1 \<union> pderivs_lang UNIV1 r2" |
244 unfolding UNIV1_def pderivs_lang_def by auto |
244 unfolding UNIV1_def pderivs_lang_def by auto |
245 |
245 |
246 |
246 |
247 text {* Non-empty suffixes of a string (needed for teh cases of @{const Times} and @{const Star} *} |
247 text {* Non-empty suffixes of a string (needed for the cases of @{const Times} and @{const Star} below) *} |
248 |
248 |
249 definition |
249 definition |
250 "PSuf s \<equiv> {v. v \<noteq> [] \<and> (\<exists>u. u @ v = s)}" |
250 "PSuf s \<equiv> {v. v \<noteq> [] \<and> (\<exists>u. u @ v = s)}" |
251 |
251 |
252 lemma PSuf_snoc: |
252 lemma PSuf_snoc: |