equal
deleted
inserted
replaced
558 using bsimp_ASEQ1 by presburger |
558 using bsimp_ASEQ1 by presburger |
559 |
559 |
560 |
560 |
561 lemma scompsize_aux: |
561 lemma scompsize_aux: |
562 shows "s_complexity (AALTs bs (rs1 @ distinctWith rs2 eq1 (set rs1))) \<le> s_complexity (AALTs bs (rs1 @ rs2))" |
562 shows "s_complexity (AALTs bs (rs1 @ distinctWith rs2 eq1 (set rs1))) \<le> s_complexity (AALTs bs (rs1 @ rs2))" |
563 sorry |
563 apply(induct rs2 arbitrary: rs1) |
|
564 apply simp |
|
565 apply simp |
|
566 apply(case_tac "\<exists>x \<in> set rs1. a ~1 x") |
|
567 using trans_le_add2 apply blast |
|
568 apply simp |
|
569 |
|
570 by (metis List.set_insert) |
|
571 |
|
572 |
564 |
573 |
565 |
574 |
566 |
575 |
567 lemma scomp_size_reduction: |
576 lemma scomp_size_reduction: |
568 shows "r1 \<le>1 r2 \<Longrightarrow> s_complexity r1 \<le> s_complexity r2" |
577 shows "r1 \<le>1 r2 \<Longrightarrow> s_complexity r1 \<le> s_complexity r2" |
587 apply simp |
596 apply simp |
588 apply(case_tac "list") |
597 apply(case_tac "list") |
589 apply auto |
598 apply auto |
590 by (metis eq_imp_le le_imp_less_Suc less_imp_le_nat rerase_fuse scomp_rerase2) |
599 by (metis eq_imp_le le_imp_less_Suc less_imp_le_nat rerase_fuse scomp_rerase2) |
591 |
600 |
592 |
601 lemma prf22: |
|
602 shows "\<lbrakk>r1 \<le>1 r2; \<not> r1 ~1 r2\<rbrakk> \<Longrightarrow> s_complexity r1 \<noteq> s_complexity r2" |
|
603 apply(induct rule:eq1.induct) |
|
604 apply simp+ |
|
605 apply auto |
|
606 |
|
607 sorry |
|
608 |
|
609 |
|
610 |
|
611 lemma compl_rrewrite_down1: |
|
612 shows "r1 \<le>1 r2 \<Longrightarrow> r1 ~1 r2 \<or> s_complexity r1 < s_complexity r2" |
|
613 apply(subgoal_tac "s_complexity r1 \<le> s_complexity r2") |
|
614 apply(case_tac "r1 ~1 r2") |
|
615 apply simp |
|
616 apply(subgoal_tac "s_complexity r1 \<noteq> s_complexity r2") |
|
617 apply simp |
|
618 using prf22 apply blast |
|
619 by (simp add: scomp_size_reduction) |
|
620 |
|
621 lemma leq1_eq1_equal: |
|
622 shows "\<lbrakk>r1 \<le>1 r2; |
593 |
623 |
594 |
624 |
595 |
625 |
596 |
626 |
597 |
627 |
598 |
628 |
599 lemma compl_rrewrite_down: |
629 lemma compl_rrewrite_down: |
600 shows "r1 \<le>1 r2 \<Longrightarrow>r1 = r2 \<or> s_complexity r1 < s_complexity r2" |
630 shows "r1 \<le>1 r2 \<Longrightarrow>r1 = r2 \<or> s_complexity r1 < s_complexity r2" |
|
631 apply(subgoal_tac "s_complexity r1 \<le> s_complexity r2") |
601 |
632 |
602 apply(induct rule: leq1.induct) |
633 apply(induct rule: leq1.induct) |
603 apply simp |
634 apply simp |
604 apply simp |
635 apply simp |
605 apply simp |
636 apply simp |