270 then ALT (SEQ (der c r1) r2) (der c r2) |
270 then ALT (SEQ (der c r1) r2) (der c r2) |
271 else SEQ (der c r1) r2)" |
271 else SEQ (der c r1) r2)" |
272 | "der c (STAR r) = SEQ (der c r) (STAR r)" |
272 | "der c (STAR r) = SEQ (der c r) (STAR r)" |
273 | "der c (UPNTIMES r n) = (if n = 0 then ZERO else SEQ (der c r) (UPNTIMES r (n - 1)))" |
273 | "der c (UPNTIMES r n) = (if n = 0 then ZERO else SEQ (der c r) (UPNTIMES r (n - 1)))" |
274 | "der c (NTIMES r n) = (if n = 0 then ZERO else SEQ (der c r) (NTIMES r (n - 1)))" |
274 | "der c (NTIMES r n) = (if n = 0 then ZERO else SEQ (der c r) (NTIMES r (n - 1)))" |
275 | "der c (FROMNTIMES r n) = |
275 | "der c (FROMNTIMES r n) = |
276 (if n = 0 |
276 (if n = 0 |
277 then SEQ (der c r) (STAR r) |
277 then SEQ (der c r) (STAR r) |
278 else SEQ (der c r) (FROMNTIMES r (n - 1)))" |
278 else SEQ (der c r) (FROMNTIMES r (n - 1)))" |
279 | "der c (NMTIMES r n m) = |
279 | "der c (NMTIMES r n m) = |
280 (if m < n then ZERO |
280 (if m < n then ZERO |
281 else (if n = 0 then (if m = 0 then ZERO else |
281 else (if n = 0 then (if m = 0 then ZERO else |
282 SEQ (der c r) (UPNTIMES r (m - 1))) else |
282 SEQ (der c r) (UPNTIMES r (m - 1))) else |
283 SEQ (der c r) (NMTIMES r (n - 1) (m - 1))))" |
283 SEQ (der c r) (NMTIMES r (n - 1) (m - 1))))" |
|
284 |
|
285 lemma |
|
286 "L(der c (UPNTIMES r m)) = |
|
287 L(if (m = 0) then ZERO else ALT ONE (SEQ(der c r) (UPNTIMES r (m - 1))))" |
|
288 apply(case_tac m) |
|
289 apply(simp) |
|
290 apply(simp del: der.simps) |
|
291 apply(simp only: der.simps) |
|
292 apply(simp add: Sequ_def) |
|
293 apply(auto) |
|
294 defer |
|
295 apply blast |
|
296 oops |
|
297 |
|
298 lemma pow_add: |
|
299 assumes "s1 \<in> A \<up> n" "s2 \<in> A \<up> m" |
|
300 shows "s1 @ s2 \<in> A \<up> (n + m)" |
|
301 using assms |
|
302 apply(induct n arbitrary: m s1 s2) |
|
303 apply(auto simp add: Sequ_def) |
|
304 by blast |
|
305 |
|
306 lemma pow_add2: |
|
307 assumes "x \<in> A \<up> (m + n)" |
|
308 shows "x \<in> A \<up> m ;; A \<up> n" |
|
309 using assms |
|
310 apply(induct m arbitrary: n x) |
|
311 apply(auto simp add: Sequ_def) |
|
312 by (metis append.assoc) |
|
313 |
|
314 |
|
315 |
|
316 lemma |
|
317 "L(FROMNTIMES r n) = L(SEQ (NTIMES r n) (STAR r))" |
|
318 apply(auto simp add: Sequ_def) |
|
319 defer |
|
320 apply(subgoal_tac "\<exists>m. s2 \<in> (L r) \<up> m") |
|
321 prefer 2 |
|
322 apply (simp add: Star_Pow) |
|
323 apply(auto) |
|
324 apply(rule_tac x="n + m" in bexI) |
|
325 apply (simp add: pow_add) |
|
326 apply simp |
|
327 apply(subgoal_tac "\<exists>m. m + n = xa") |
|
328 apply(auto) |
|
329 prefer 2 |
|
330 using le_add_diff_inverse2 apply auto[1] |
|
331 by (smt Pow_Star Sequ_def add.commute mem_Collect_eq pow_add2) |
|
332 |
|
333 lemma |
|
334 "L (der c (FROMNTIMES r n)) = |
|
335 L (SEQ (der c r) (FROMNTIMES r (n - 1)))" |
|
336 apply(auto simp add: Sequ_def) |
|
337 using Star_Pow apply blast |
|
338 using Pow_Star by blast |
|
339 |
|
340 lemma |
|
341 "L (der c (UPNTIMES r n)) = |
|
342 L(if n = 0 then ZERO else |
|
343 ALT (der c r) (SEQ (der c r) (UPNTIMES r (n - 1))))" |
|
344 apply(auto simp add: Sequ_def) |
|
345 using SpecExt.Pow_empty by blast |
284 |
346 |
285 fun |
347 fun |
286 ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp" |
348 ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp" |
287 where |
349 where |
288 "ders [] r = r" |
350 "ders [] r = r" |