equal
deleted
inserted
replaced
525 |
525 |
526 |
526 |
527 lemma frewrite_append: |
527 lemma frewrite_append: |
528 shows "\<lbrakk> rsa \<leadsto>f rsb \<rbrakk> \<Longrightarrow> rs @ rsa \<leadsto>f rs @ rsb" |
528 shows "\<lbrakk> rsa \<leadsto>f rsb \<rbrakk> \<Longrightarrow> rs @ rsa \<leadsto>f rs @ rsb" |
529 apply(induct rs) |
529 apply(induct rs) |
530 apply simp+ |
530 apply simp+ |
531 oops |
531 using frewrite.intros(3) by blast |
|
532 |
532 |
533 |
533 |
534 |
534 lemma frewrites_cons: |
535 lemma frewrites_cons: |
535 shows "\<lbrakk> rsa \<leadsto>f* rsb \<rbrakk> \<Longrightarrow> r # rsa \<leadsto>f* r # rsb" |
536 shows "\<lbrakk> rsa \<leadsto>f* rsb \<rbrakk> \<Longrightarrow> r # rsa \<leadsto>f* r # rsb" |
536 |
537 apply(induct rsa rsb rule: frewrites.induct) |
537 oops |
538 apply simp |
|
539 using frewrite.intros(3) by blast |
|
540 |
538 |
541 |
539 lemma frewrites_append: |
542 lemma frewrites_append: |
540 shows " \<lbrakk>rsa \<leadsto>f* rsb\<rbrakk> \<Longrightarrow> (rs @ rsa) \<leadsto>f* (rs @ rsb)" |
543 shows " \<lbrakk>rsa \<leadsto>f* rsb\<rbrakk> \<Longrightarrow> (rs @ rsa) \<leadsto>f* (rs @ rsb)" |
541 apply(induct rsa rsb rule: frewrites.induct) |
544 apply(induct rs) |
542 apply simp |
545 apply simp |
543 oops |
546 by (simp add: frewrites_cons) |
544 |
547 |
545 |
548 |
546 |
549 |
547 lemma frewrites_concat: |
550 lemma frewrites_concat: |
548 shows "\<lbrakk>rs1 \<leadsto>f rs2; rsa \<leadsto>f* rsb \<rbrakk> \<Longrightarrow> (rs1 @ rsa) \<leadsto>f* (rs2 @ rsb)" |
551 shows "\<lbrakk>rs1 \<leadsto>f rs2; rsa \<leadsto>f* rsb \<rbrakk> \<Longrightarrow> (rs1 @ rsa) \<leadsto>f* (rs2 @ rsb)" |
551 apply(subgoal_tac "(RZERO # rs @ rsa) \<leadsto>f (rs @ rsa)") |
554 apply(subgoal_tac "(RZERO # rs @ rsa) \<leadsto>f (rs @ rsa)") |
552 prefer 2 |
555 prefer 2 |
553 using frewrite.intros(1) apply blast |
556 using frewrite.intros(1) apply blast |
554 apply(subgoal_tac "(rs @ rsa) \<leadsto>f* (rs @ rsb)") |
557 apply(subgoal_tac "(rs @ rsa) \<leadsto>f* (rs @ rsb)") |
555 using many_steps_later apply blast |
558 using many_steps_later apply blast |
556 |
559 apply (simp add: frewrites_append) |
557 |
560 apply (metis append.assoc append_Cons frewrite.intros(2) frewrites_append many_steps_later) |
558 |
561 using frewrites_cons by auto |
559 |
562 |
560 |
563 |
561 |
564 |
562 |
565 |
563 lemma many_steps_later1: |
566 lemma many_steps_later1: |
571 apply simp |
574 apply simp |
572 apply(case_tac a) |
575 apply(case_tac a) |
573 apply simp+ |
576 apply simp+ |
574 using frewrite.intros(1) many_steps_later apply blast |
577 using frewrite.intros(1) many_steps_later apply blast |
575 apply(case_tac "x = x3") |
578 apply(case_tac "x = x3") |
576 apply simp |
579 apply simp |
577 |
580 |
|
581 using frewrites_cons apply presburger |
|
582 using frewrite.intros(1) many_steps_later apply fastforce |
|
583 apply(case_tac "rnullable x41") |
|
584 apply simp |
578 |
585 |
579 |
586 |
580 |
587 |
581 |
588 |
582 fun alt_set:: "rrexp \<Rightarrow> rrexp set" |
589 fun alt_set:: "rrexp \<Rightarrow> rrexp set" |