528 by (simp add: Suc_leI length_Cons less_add_Suc1) |
528 by (simp add: Suc_leI length_Cons less_add_Suc1) |
529 |
529 |
530 |
530 |
531 |
531 |
532 lemma good_flatten_aux: |
532 lemma good_flatten_aux: |
533 shows " \<lbrakk>\<forall>r\<in>set rs. good r; \<forall>r\<in>set rsa. good r; \<forall>r\<in>set rsb. good r; |
533 shows " \<lbrakk>\<forall>r\<in>set rs. good r \<or> r = RZERO; \<forall>r\<in>set rsa . good r \<or> r = RZERO; |
|
534 \<forall>r\<in>set rsb. good r \<or> r = RZERO; |
534 rsimp (RALTS (rsa @ rs @ rsb)) = rsimp_ALTs (rdistinct (rflts (rsa @ rs @ rsb)) {}); |
535 rsimp (RALTS (rsa @ rs @ rsb)) = rsimp_ALTs (rdistinct (rflts (rsa @ rs @ rsb)) {}); |
535 rsimp (RALTS (rsa @ [RALTS rs] @ rsb)) = |
536 rsimp (RALTS (rsa @ [RALTS rs] @ rsb)) = |
536 rsimp_ALTs (rdistinct (rflts (rsa @ [rsimp (RALTS rs)] @ rsb)) {}); |
537 rsimp_ALTs (rdistinct (rflts (rsa @ [rsimp (RALTS rs)] @ rsb)) {}); |
537 map rsimp rsa = rsa; map rsimp rsb = rsb; map rsimp rs = rs; |
538 map rsimp rsa = rsa; map rsimp rsb = rsb; map rsimp rs = rs; |
538 rdistinct (rflts rsa @ rflts rs @ rflts rsb) {} = |
539 rdistinct (rflts rsa @ rflts rs @ rflts rsb) {} = |
551 apply (metis append_Cons append_Nil flts_append list.set(1) list.simps(15) nonalt.simps(1) nonalt0_flts_keeps nonalt_flts_rd qqq1 rdistinct.simps(2) rdistinct_set_equality singleton_iff) |
552 apply (metis append_Cons append_Nil flts_append list.set(1) list.simps(15) nonalt.simps(1) nonalt0_flts_keeps nonalt_flts_rd qqq1 rdistinct.simps(2) rdistinct_set_equality singleton_iff) |
552 apply simp |
553 apply simp |
553 apply (metis Un_insert_left append_Cons append_Nil ex_in_conv flts_single1 insertI1 list.simps(15) nonalt_flts_rd nonazero.elims(3) qqq1 rdistinct.simps(2) sup_bot_left) |
554 apply (metis Un_insert_left append_Cons append_Nil ex_in_conv flts_single1 insertI1 list.simps(15) nonalt_flts_rd nonazero.elims(3) qqq1 rdistinct.simps(2) sup_bot_left) |
554 apply(subgoal_tac "\<forall>r \<in> set (rflts rs). good r \<and> r \<noteq> RZERO \<and> nonalt r") |
555 apply(subgoal_tac "\<forall>r \<in> set (rflts rs). good r \<and> r \<noteq> RZERO \<and> nonalt r") |
555 prefer 2 |
556 prefer 2 |
556 apply (metis flts3 nn1b nn1c qqq1 test) |
557 apply (metis flts3 nonalt_flts_rd qqq1 rdistinct_set_equality) |
557 apply(subgoal_tac "\<forall>r \<in> set (rflts rsb). good r \<and> r \<noteq> RZERO \<and> nonalt r") |
558 apply(subgoal_tac "\<forall>r \<in> set (rflts rsb). good r \<and> r \<noteq> RZERO \<and> nonalt r") |
558 prefer 2 |
559 prefer 2 |
559 apply (metis flts3 nn1b nn1c qqq1 test) |
560 apply (metis flts3 nonalt_flts_rd qqq1 rdistinct_set_equality) |
560 by (smt (verit, ccfv_threshold) good_flatten_aux_aux) |
561 by (smt (verit, ccfv_threshold) good_flatten_aux_aux) |
561 |
562 |
562 |
563 |
563 |
564 |
564 |
565 |
565 lemma good_flatten_middle: |
566 lemma good_flatten_middle: |
566 shows "\<lbrakk>\<forall>r \<in> set rs. good r; \<forall>r \<in> set rsa. good r; \<forall>r \<in> set rsb. good r\<rbrakk> \<Longrightarrow> |
567 shows "\<lbrakk>\<forall>r \<in> set rs. good r \<or> r = RZERO; \<forall>r \<in> set rsa. good r \<or> r = RZERO; \<forall>r \<in> set rsb. good r \<or> r = RZERO\<rbrakk> \<Longrightarrow> |
567 rsimp (RALTS (rsa @ rs @ rsb)) = rsimp (RALTS (rsa @ [RALTS rs] @ rsb))" |
568 rsimp (RALTS (rsa @ rs @ rsb)) = rsimp (RALTS (rsa @ [RALTS rs] @ rsb))" |
568 apply(subgoal_tac "rsimp (RALTS (rsa @ rs @ rsb)) = rsimp_ALTs (rdistinct (rflts (map rsimp rsa @ |
569 apply(subgoal_tac "rsimp (RALTS (rsa @ rs @ rsb)) = rsimp_ALTs (rdistinct (rflts (map rsimp rsa @ |
569 map rsimp rs @ map rsimp rsb)) {})") |
570 map rsimp rs @ map rsimp rsb)) {})") |
570 prefer 2 |
571 prefer 2 |
571 apply simp |
572 apply simp |
575 prefer 2 |
576 prefer 2 |
576 apply simp |
577 apply simp |
577 apply(simp only:) |
578 apply(simp only:) |
578 apply(subgoal_tac "map rsimp rsa = rsa") |
579 apply(subgoal_tac "map rsimp rsa = rsa") |
579 prefer 2 |
580 prefer 2 |
580 apply (simp add: map_idI test) |
581 apply (metis map_idI rsimp.simps(3) test) |
581 apply(simp only:) |
582 apply(simp only:) |
582 apply(subgoal_tac "map rsimp rsb = rsb") |
583 apply(subgoal_tac "map rsimp rsb = rsb") |
583 prefer 2 |
584 prefer 2 |
584 apply (meson map_idI test) |
585 apply (metis map_idI rsimp.simps(3) test) |
585 apply(simp only:) |
586 apply(simp only:) |
586 apply(subst k00)+ |
587 apply(subst k00)+ |
587 apply(subgoal_tac "map rsimp rs = rs") |
588 apply(subgoal_tac "map rsimp rs = rs") |
588 apply(simp only:) |
589 apply(simp only:) |
589 prefer 2 |
590 prefer 2 |
590 apply (meson map_idI test) |
591 apply (metis map_idI rsimp.simps(3) test) |
591 apply(subgoal_tac "rdistinct (rflts rsa @ rflts rs @ rflts rsb) {} = |
592 apply(subgoal_tac "rdistinct (rflts rsa @ rflts rs @ rflts rsb) {} = |
592 rdistinct (rflts rsa) {} @ rdistinct (rflts rs @ rflts rsb) (set (rflts rsa))") |
593 rdistinct (rflts rsa) {} @ rdistinct (rflts rs @ rflts rsb) (set (rflts rsa))") |
593 apply(simp only:) |
594 apply(simp only:) |
594 prefer 2 |
595 prefer 2 |
595 using rdistinct_concat_general apply blast |
596 using rdistinct_concat_general apply blast |
598 apply(simp only:) |
599 apply(simp only:) |
599 prefer 2 |
600 prefer 2 |
600 using rdistinct_concat_general apply blast |
601 using rdistinct_concat_general apply blast |
601 apply(subgoal_tac "rdistinct (rflts rs @ rflts rsb) (set (rflts rsa)) = |
602 apply(subgoal_tac "rdistinct (rflts rs @ rflts rsb) (set (rflts rsa)) = |
602 rdistinct (rflts [rsimp (RALTS rs)] @ rflts rsb) (set (rflts rsa))") |
603 rdistinct (rflts [rsimp (RALTS rs)] @ rflts rsb) (set (rflts rsa))") |
603 apply presburger |
604 apply presburger |
604 using good_flatten_aux by blast |
605 using good_flatten_aux by blast |
605 |
606 |
606 |
607 |
607 lemma simp_flatten3: |
608 lemma simp_flatten3: |
608 shows "rsimp (RALTS (rsa @ [RALTS rs] @ rsb)) = rsimp (RALTS (rsa @ rs @ rsb))" |
609 shows "rsimp (RALTS (rsa @ [RALTS rs] @ rsb)) = rsimp (RALTS (rsa @ rs @ rsb))" |
618 apply(simp only:) |
619 apply(simp only:) |
619 apply(subgoal_tac "rsimp (RALTS (map rsimp rsa @ map rsimp rs @ map rsimp rsb)) = |
620 apply(subgoal_tac "rsimp (RALTS (map rsimp rsa @ map rsimp rs @ map rsimp rsb)) = |
620 rsimp (RALTS (map rsimp rsa @ [RALTS (map rsimp rs)] @ map rsimp rsb))") |
621 rsimp (RALTS (map rsimp rsa @ [RALTS (map rsimp rs)] @ map rsimp rsb))") |
621 |
622 |
622 apply (metis (no_types, lifting) head_one_more_simp map_append simp_flatten_aux0) |
623 apply (metis (no_types, lifting) head_one_more_simp map_append simp_flatten_aux0) |
623 apply(subgoal_tac "\<forall>r \<in> set (map rsimp rsa). good r") |
624 apply(subgoal_tac "\<forall>r \<in> set (map rsimp rsa). good r \<or> r = RZERO") |
624 apply(subgoal_tac "\<forall>r \<in> set (map rsimp rs). good r") |
625 apply(subgoal_tac "\<forall>r \<in> set (map rsimp rs). good r \<or> r = RZERO") |
625 apply(subgoal_tac "\<forall>r \<in> set (map rsimp rsb). good r") |
626 apply(subgoal_tac "\<forall>r \<in> set (map rsimp rsb). good r \<or> r = RZERO") |
626 |
627 |
627 using good_flatten_middle apply presburger |
628 using good_flatten_middle apply presburger |
628 |
629 |
629 |
630 apply (simp add: good1) |
630 sorry |
631 apply (simp add: good1) |
|
632 apply (simp add: good1) |
|
633 |
|
634 done |
631 |
635 |
632 |
636 |
633 |
637 |
634 |
638 |
635 |
639 |