equal
deleted
inserted
replaced
357 apply(subgoal_tac "{n..m} = {n} \<union> {Suc n..m}") |
357 apply(subgoal_tac "{n..m} = {n} \<union> {Suc n..m}") |
358 apply(auto simp add: Seq_def) |
358 apply(auto simp add: Seq_def) |
359 done |
359 done |
360 |
360 |
361 lemma L_der_NTIMES: |
361 lemma L_der_NTIMES: |
362 shows "L(der c (NTIMES r n)) = (if n = 0 then {} else if nullable r then |
362 shows "L(der c (NTIMES r n)) = L (if n = 0 then NULL else if nullable r then |
363 L(SEQ (der c r) (UPNTIMES r (n - 1))) |
363 SEQ (der c r) (UPNTIMES r (n - 1)) else SEQ (der c r) (NTIMES r (n - 1)))" |
364 else L(SEQ (der c r) (NTIMES r (n - 1))))" |
|
365 apply(induct n) |
364 apply(induct n) |
366 apply(simp) |
365 apply(simp) |
367 apply(simp) |
366 apply(simp) |
368 apply(auto) |
367 apply(auto) |
369 apply(auto simp add: Seq_def) |
368 apply(auto simp add: Seq_def) |
373 apply(simp) |
372 apply(simp) |
374 apply(simp) |
373 apply(simp) |
375 apply(rule_tac x="s1" in exI) |
374 apply(rule_tac x="s1" in exI) |
376 apply(simp) |
375 apply(simp) |
377 by (metis Suc_pred atMost_iff le_Suc_eq) |
376 by (metis Suc_pred atMost_iff le_Suc_eq) |
|
377 |
|
378 lemma "L(der c (UPNTIMES r 0)) = {}" |
|
379 by simp |
378 |
380 |
379 lemma "L(der c (UPNTIMES r (Suc n))) = L(SEQ (der c r) (UPNTIMES r n))" |
381 lemma "L(der c (UPNTIMES r (Suc n))) = L(SEQ (der c r) (UPNTIMES r n))" |
380 using assms |
382 using assms |
381 proof(induct n) |
383 proof(induct n) |
382 case 0 show ?case by simp |
384 case 0 show ?case by simp |