184 | "M (OPT r) = Suc (M r)" |
184 | "M (OPT r) = Suc (M r)" |
185 | "M (NTIMES r n) = Suc (M r) * 2 * (Suc n)" |
185 | "M (NTIMES r n) = Suc (M r) * 2 * (Suc n)" |
186 | "M (NMTIMES r n m) = Suc (Suc (M r)) * 2 * (Suc m) * (Suc (Suc m) - Suc n)" |
186 | "M (NMTIMES r n m) = Suc (Suc (M r)) * 2 * (Suc m) * (Suc (Suc m) - Suc n)" |
187 | "M (UPNTIMES r n) = Suc (M r) * 2 * (Suc n)" |
187 | "M (UPNTIMES r n) = Suc (M r) * 2 * (Suc n)" |
188 |
188 |
189 function der :: "char \<Rightarrow> rexp \<Rightarrow> rexp" |
189 fun der :: "char \<Rightarrow> rexp \<Rightarrow> rexp" |
190 where |
190 where |
191 "der c (NULL) = NULL" |
191 "der c (NULL) = NULL" |
192 | "der c (EMPTY) = NULL" |
192 | "der c (EMPTY) = NULL" |
193 | "der c (CH d) = (if c = d then EMPTY else NULL)" |
193 | "der c (CH d) = (if c = d then EMPTY else NULL)" |
194 | "der c (ALT r1 r2) = ALT (der c r1) (der c r2)" |
194 | "der c (ALT r1 r2) = ALT (der c r1) (der c r2)" |
195 | "der c (SEQ r1 r2) = ALT (SEQ (der c r1) r2) (if nullable r1 then der c r2 else NULL)" |
195 | "der c (SEQ r1 r2) = ALT (SEQ (der c r1) r2) (if nullable r1 then der c r2 else NULL)" |
196 | "der c (STAR r) = SEQ (der c r) (STAR r)" |
196 | "der c (STAR r) = SEQ (der c r) (STAR r)" |
197 | "der c (NOT r) = NOT(der c r)" |
197 | "der c (NOT r) = NOT(der c r)" |
198 | "der c (PLUS r) = SEQ (der c r) (STAR r)" |
198 | "der c (PLUS r) = SEQ (der c r) (STAR r)" |
199 | "der c (OPT r) = der c r" |
199 | "der c (OPT r) = der c r" |
200 | "der c (NTIMES r 0) = NULL" |
200 | "der c (NTIMES r n) = (if n = 0 then NULL else (SEQ (der c r) (NTIMES r (n - 1))))" |
201 | "der c (NTIMES r (Suc n)) = der c (SEQ r (NTIMES r n))" |
|
202 | "der c (NMTIMES r n m) = |
201 | "der c (NMTIMES r n m) = |
203 (if m < n then NULL else |
202 (if m = 0 then NULL else |
204 (if n = m then der c (NTIMES r n) else |
203 (if n = 0 then SEQ (der c r) (UPNTIMES r (m - 1)) |
205 ALT (der c (NTIMES r n)) (der c (NMTIMES r (Suc n) m))))" |
204 else SEQ (der c r) (NMTIMES r (n - 1) (m - 1))))" |
206 | "der c (UPNTIMES r 0) = NULL" |
205 | "der c (UPNTIMES r n) = (if n = 0 then NULL else SEQ (der c r) (UPNTIMES r (n - 1)))" |
207 | "der c (UPNTIMES r (Suc n)) = der c (ALT (NTIMES r (Suc n)) (UPNTIMES r n))" |
|
208 by pat_completeness auto |
|
209 |
|
210 lemma bigger1: |
|
211 "\<lbrakk>c < (d::nat); a < b; 0 < a; 0 < c\<rbrakk> \<Longrightarrow> c * a < d * b" |
|
212 by (metis le0 mult_strict_mono') |
|
213 |
|
214 termination der |
|
215 apply(relation "measure (\<lambda>(c, r). M r)") |
|
216 apply(simp) |
|
217 apply(simp) |
|
218 apply(simp) |
|
219 apply(simp) |
|
220 apply(simp) |
|
221 apply(simp) |
|
222 apply(simp) |
|
223 apply(simp) |
|
224 apply(simp) |
|
225 apply(simp) |
|
226 apply(simp) |
|
227 apply(simp_all del: M.simps) |
|
228 apply(simp_all only: M.simps) |
|
229 defer |
|
230 defer |
|
231 defer |
|
232 apply(subgoal_tac "Suc (Suc m) - Suc (Suc n) < Suc (Suc m) - Suc n") |
|
233 prefer 2 |
|
234 apply(auto)[1] |
|
235 |
|
236 (* |
|
237 apply (metis Suc_mult_less_cancel1 mult.assoc numeral_eq_Suc) |
|
238 apply(subgoal_tac "0 < (Suc (Suc m) - Suc n)") |
|
239 prefer 2 |
|
240 apply(auto)[1] |
|
241 apply(subgoal_tac "Suc n < Suc m") |
|
242 prefer 2 |
|
243 apply(auto)[1] |
|
244 apply(subgoal_tac "Suc (M r) * 2 * Suc n < Suc (Suc (M r)) * 2 * Suc m") |
|
245 prefer 2 |
|
246 apply(subgoal_tac "Suc (M r) * 2 < Suc (Suc (M r)) * 2") |
|
247 prefer 2 |
|
248 apply(auto)[1] |
|
249 apply(rule bigger1) |
|
250 apply(assumption) |
|
251 apply(simp) |
|
252 apply (metis zero_less_Suc) |
|
253 apply (metis mult_is_0 neq0_conv old.nat.distinct(2)) |
|
254 apply(rotate_tac 4) |
|
255 apply(drule_tac a="1" and b="(Suc (Suc m) - Suc n)" in bigger1) |
|
256 prefer 4 |
|
257 apply(simp) |
|
258 apply(simp) |
|
259 apply (metis zero_less_one) |
|
260 apply(simp) |
|
261 done |
|
262 *) |
|
263 sorry |
|
264 |
206 |
265 fun |
207 fun |
266 ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp" |
208 ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp" |
267 where |
209 where |
268 "ders [] r = r" |
210 "ders [] r = r" |
367 lemma Der_pow [simp]: |
309 lemma Der_pow [simp]: |
368 shows "Der c (A \<up> (Suc n)) = (Der c A) ;; (A \<up> n) \<union> (if [] \<in> A then Der c (A \<up> n) else {})" |
310 shows "Der c (A \<up> (Suc n)) = (Der c A) ;; (A \<up> n) \<union> (if [] \<in> A then Der c (A \<up> n) else {})" |
369 unfolding Der_def |
311 unfolding Der_def |
370 by(auto simp add: Cons_eq_append_conv Seq_def) |
312 by(auto simp add: Cons_eq_append_conv Seq_def) |
371 |
313 |
|
314 |
372 lemma Der_UNION [simp]: |
315 lemma Der_UNION [simp]: |
373 shows "Der c (\<Union>x\<in>A. B x) = (\<Union>x\<in>A. Der c (B x))" |
316 shows "Der c (\<Union>x\<in>A. B x) = (\<Union>x\<in>A. Der c (B x))" |
374 by (auto simp add: Der_def) |
317 by (auto simp add: Der_def) |
375 |
318 |
376 lemma if_f: |
319 lemma if_f: |
410 case (OPT r) |
353 case (OPT r) |
411 then show ?case by simp |
354 then show ?case by simp |
412 next |
355 next |
413 case (NTIMES r n) |
356 case (NTIMES r n) |
414 then show ?case |
357 then show ?case |
415 apply(induct n) |
358 apply(auto simp add: Seq_def) |
416 apply(simp) |
359 using Der_ntimes Matcher2.Seq_def less_iff_Suc_add apply fastforce |
417 apply(simp only: L.simps) |
360 using Der_ntimes Matcher2.Seq_def less_iff_Suc_add by auto |
418 apply(simp only: Der_pow) |
|
419 apply(simp only: der.simps L.simps) |
|
420 apply(simp only: nullable_correctness) |
|
421 apply(simp only: if_f) |
|
422 by simp |
|
423 next |
361 next |
424 case (NMTIMES r n m) |
362 case (NMTIMES r n m) |
425 then show ?case |
363 then show ?case |
|
364 apply(auto simp add: Seq_def) |
|
365 sledgeham mer[timeout=1000] |
426 apply(case_tac n) |
366 apply(case_tac n) |
427 sorry |
367 sorry |
428 next |
368 next |
429 case (UPNTIMES r x2) |
369 case (UPNTIMES r x2) |
430 then show ?case sorry |
370 then show ?case |
|
371 apply(auto simp add: Seq_def) |
|
372 apply (metis (mono_tags, lifting) Der_ntimes Matcher2.Seq_def Suc_le_mono Suc_pred atMost_iff |
|
373 mem_Collect_eq) |
|
374 sledgehammer[timeout=1000] |
|
375 sorry |
431 qed |
376 qed |
432 |
377 |
433 |
378 |
434 |
379 |
435 |
380 |