607 | "simpfm (Gt a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v > 0) then T else F | _ \<Rightarrow> Gt a')" |
613 | "simpfm (Gt a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v > 0) then T else F | _ \<Rightarrow> Gt a')" |
608 | "simpfm (Ge a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v \<ge> 0) then T else F | _ \<Rightarrow> Ge a')" |
614 | "simpfm (Ge a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v \<ge> 0) then T else F | _ \<Rightarrow> Ge a')" |
609 | "simpfm (Eq a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v = 0) then T else F | _ \<Rightarrow> Eq a')" |
615 | "simpfm (Eq a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v = 0) then T else F | _ \<Rightarrow> Eq a')" |
610 | "simpfm (NEq a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v \<noteq> 0) then T else F | _ \<Rightarrow> NEq a')" |
616 | "simpfm (NEq a) = (let a' = simpnum a in case a' of C v \<Rightarrow> if (v \<noteq> 0) then T else F | _ \<Rightarrow> NEq a')" |
611 | "simpfm (Dvd i a) = |
617 | "simpfm (Dvd i a) = |
612 (if i=0 then simpfm (Eq a) |
618 (if i = 0 then simpfm (Eq a) |
613 else if (abs i = 1) then T |
619 else if abs i = 1 then T |
614 else let a' = simpnum a in case a' of C v \<Rightarrow> if (i dvd v) then T else F | _ \<Rightarrow> Dvd i a')" |
620 else let a' = simpnum a in case a' of C v \<Rightarrow> if (i dvd v) then T else F | _ \<Rightarrow> Dvd i a')" |
615 | "simpfm (NDvd i a) = |
621 | "simpfm (NDvd i a) = |
616 (if i=0 then simpfm (NEq a) |
622 (if i = 0 then simpfm (NEq a) |
617 else if (abs i = 1) then F |
623 else if abs i = 1 then F |
618 else let a' = simpnum a in case a' of C v \<Rightarrow> if (\<not>(i dvd v)) then T else F | _ \<Rightarrow> NDvd i a')" |
624 else let a' = simpnum a in case a' of C v \<Rightarrow> if (\<not>(i dvd v)) then T else F | _ \<Rightarrow> NDvd i a')" |
619 | "simpfm p = p" |
625 | "simpfm p = p" |
620 by pat_completeness auto |
626 by pat_completeness auto |
621 termination by (relation "measure fmsize") auto |
627 termination by (relation "measure fmsize") auto |
622 |
628 |
623 lemma simpfm: "Ifm bbs bs (simpfm p) = Ifm bbs bs p" |
629 lemma simpfm: "Ifm bbs bs (simpfm p) = Ifm bbs bs p" |
624 proof (induct p rule: simpfm.induct) |
630 proof (induct p rule: simpfm.induct) |
625 case (6 a) |
631 case (6 a) |
626 let ?sa = "simpnum a" |
632 let ?sa = "simpnum a" |
627 from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp |
633 from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp |
628 { fix v assume "?sa = C v" hence ?case using sa by simp } |
634 { fix v assume "?sa = C v" then have ?case using sa by simp } |
629 moreover { |
635 moreover { |
630 assume "\<not> (\<exists>v. ?sa = C v)" |
636 assume "\<not> (\<exists>v. ?sa = C v)" |
631 hence ?case using sa by (cases ?sa) (simp_all add: Let_def) |
637 then have ?case using sa by (cases ?sa) (simp_all add: Let_def) |
632 } |
638 } |
633 ultimately show ?case by blast |
639 ultimately show ?case by blast |
634 next |
640 next |
635 case (7 a) |
641 case (7 a) |
636 let ?sa = "simpnum a" |
642 let ?sa = "simpnum a" |
637 from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp |
643 from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp |
638 { fix v assume "?sa = C v" hence ?case using sa by simp } |
644 { fix v assume "?sa = C v" then have ?case using sa by simp } |
639 moreover { |
645 moreover { |
640 assume "\<not> (\<exists>v. ?sa = C v)" |
646 assume "\<not> (\<exists>v. ?sa = C v)" |
641 hence ?case using sa by (cases ?sa) (simp_all add: Let_def) |
647 then have ?case using sa by (cases ?sa) (simp_all add: Let_def) |
642 } |
648 } |
643 ultimately show ?case by blast |
649 ultimately show ?case by blast |
644 next |
650 next |
645 case (8 a) |
651 case (8 a) |
646 let ?sa = "simpnum a" |
652 let ?sa = "simpnum a" |
647 from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp |
653 from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp |
648 { fix v assume "?sa = C v" hence ?case using sa by simp } |
654 { fix v assume "?sa = C v" then have ?case using sa by simp } |
649 moreover { |
655 moreover { |
650 assume "\<not> (\<exists>v. ?sa = C v)" |
656 assume "\<not> (\<exists>v. ?sa = C v)" |
651 hence ?case using sa by (cases ?sa) (simp_all add: Let_def) |
657 then have ?case using sa by (cases ?sa) (simp_all add: Let_def) |
652 } |
658 } |
653 ultimately show ?case by blast |
659 ultimately show ?case by blast |
654 next |
660 next |
655 case (9 a) |
661 case (9 a) |
656 let ?sa = "simpnum a" |
662 let ?sa = "simpnum a" |
657 from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp |
663 from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp |
658 { fix v assume "?sa = C v" hence ?case using sa by simp } |
664 { fix v assume "?sa = C v" then have ?case using sa by simp } |
659 moreover { |
665 moreover { |
660 assume "\<not> (\<exists>v. ?sa = C v)" |
666 assume "\<not> (\<exists>v. ?sa = C v)" |
661 hence ?case using sa by (cases ?sa) (simp_all add: Let_def) |
667 then have ?case using sa by (cases ?sa) (simp_all add: Let_def) |
662 } |
668 } |
663 ultimately show ?case by blast |
669 ultimately show ?case by blast |
664 next |
670 next |
665 case (10 a) |
671 case (10 a) |
666 let ?sa = "simpnum a" |
672 let ?sa = "simpnum a" |
667 from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp |
673 from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp |
668 { fix v assume "?sa = C v" hence ?case using sa by simp } |
674 { fix v assume "?sa = C v" then have ?case using sa by simp } |
669 moreover { |
675 moreover { |
670 assume "\<not> (\<exists>v. ?sa = C v)" |
676 assume "\<not> (\<exists>v. ?sa = C v)" |
671 hence ?case using sa by (cases ?sa) (simp_all add: Let_def) |
677 then have ?case using sa by (cases ?sa) (simp_all add: Let_def) |
672 } |
678 } |
673 ultimately show ?case by blast |
679 ultimately show ?case by blast |
674 next |
680 next |
675 case (11 a) |
681 case (11 a) |
676 let ?sa = "simpnum a" |
682 let ?sa = "simpnum a" |
677 from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp |
683 from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp |
678 { fix v assume "?sa = C v" hence ?case using sa by simp } |
684 { fix v assume "?sa = C v" then have ?case using sa by simp } |
679 moreover { |
685 moreover { |
680 assume "\<not> (\<exists>v. ?sa = C v)" |
686 assume "\<not> (\<exists>v. ?sa = C v)" |
681 hence ?case using sa by (cases ?sa) (simp_all add: Let_def) |
687 then have ?case using sa by (cases ?sa) (simp_all add: Let_def) |
682 } |
688 } |
683 ultimately show ?case by blast |
689 ultimately show ?case by blast |
684 next |
690 next |
685 case (12 i a) |
691 case (12 i a) |
686 let ?sa = "simpnum a" |
692 let ?sa = "simpnum a" |
687 from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp |
693 from simpnum_ci have sa: "Inum bs ?sa = Inum bs a" by simp |
688 { assume "i=0" hence ?case using "12.hyps" by (simp add: dvd_def Let_def) } |
694 { assume "i=0" then have ?case using "12.hyps" by (simp add: dvd_def Let_def) } |
689 moreover |
695 moreover |
690 { assume i1: "abs i = 1" |
696 { assume i1: "abs i = 1" |
691 from one_dvd[of "Inum bs a"] uminus_dvd_conv[where d="1" and t="Inum bs a"] |
697 from one_dvd[of "Inum bs a"] uminus_dvd_conv[where d="1" and t="Inum bs a"] |
692 have ?case using i1 |
698 have ?case using i1 |
693 apply (cases "i=0", simp_all add: Let_def) |
699 apply (cases "i=0", simp_all add: Let_def) |
720 done |
726 done |
721 } |
727 } |
722 moreover |
728 moreover |
723 { assume inz: "i\<noteq>0" and cond: "abs i \<noteq> 1" |
729 { assume inz: "i\<noteq>0" and cond: "abs i \<noteq> 1" |
724 { fix v assume "?sa = C v" |
730 { fix v assume "?sa = C v" |
725 hence ?case using sa[symmetric] inz cond |
731 then have ?case using sa[symmetric] inz cond |
726 by (cases "abs i = 1") auto } |
732 by (cases "abs i = 1") auto } |
727 moreover { |
733 moreover { |
728 assume "\<not> (\<exists>v. ?sa = C v)" |
734 assume "\<not> (\<exists>v. ?sa = C v)" |
729 hence "simpfm (NDvd i a) = NDvd i ?sa" using inz cond |
735 then have "simpfm (NDvd i a) = NDvd i ?sa" using inz cond |
730 by (cases ?sa) (auto simp add: Let_def) |
736 by (cases ?sa) (auto simp add: Let_def) |
731 hence ?case using sa by simp } |
737 then have ?case using sa by simp } |
732 ultimately have ?case by blast } |
738 ultimately have ?case by blast } |
733 ultimately show ?case by blast |
739 ultimately show ?case by blast |
734 qed (simp_all add: conj disj imp iff not) |
740 qed (simp_all add: conj disj imp iff not) |
735 |
741 |
736 lemma simpfm_bound0: "bound0 p \<Longrightarrow> bound0 (simpfm p)" |
742 lemma simpfm_bound0: "bound0 p \<Longrightarrow> bound0 (simpfm p)" |
737 proof (induct p rule: simpfm.induct) |
743 proof (induct p rule: simpfm.induct) |
738 case (6 a) hence nb: "numbound0 a" by simp |
744 case (6 a) then have nb: "numbound0 a" by simp |
739 hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb]) |
745 then have "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb]) |
740 thus ?case by (cases "simpnum a") (auto simp add: Let_def) |
746 then show ?case by (cases "simpnum a") (auto simp add: Let_def) |
741 next |
747 next |
742 case (7 a) hence nb: "numbound0 a" by simp |
748 case (7 a) then have nb: "numbound0 a" by simp |
743 hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb]) |
749 then have "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb]) |
744 thus ?case by (cases "simpnum a") (auto simp add: Let_def) |
750 then show ?case by (cases "simpnum a") (auto simp add: Let_def) |
745 next |
751 next |
746 case (8 a) hence nb: "numbound0 a" by simp |
752 case (8 a) then have nb: "numbound0 a" by simp |
747 hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb]) |
753 then have "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb]) |
748 thus ?case by (cases "simpnum a") (auto simp add: Let_def) |
754 then show ?case by (cases "simpnum a") (auto simp add: Let_def) |
749 next |
755 next |
750 case (9 a) hence nb: "numbound0 a" by simp |
756 case (9 a) then have nb: "numbound0 a" by simp |
751 hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb]) |
757 then have "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb]) |
752 thus ?case by (cases "simpnum a") (auto simp add: Let_def) |
758 then show ?case by (cases "simpnum a") (auto simp add: Let_def) |
753 next |
759 next |
754 case (10 a) hence nb: "numbound0 a" by simp |
760 case (10 a) then have nb: "numbound0 a" by simp |
755 hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb]) |
761 then have "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb]) |
756 thus ?case by (cases "simpnum a") (auto simp add: Let_def) |
762 then show ?case by (cases "simpnum a") (auto simp add: Let_def) |
757 next |
763 next |
758 case (11 a) hence nb: "numbound0 a" by simp |
764 case (11 a) then have nb: "numbound0 a" by simp |
759 hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb]) |
765 then have "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb]) |
760 thus ?case by (cases "simpnum a") (auto simp add: Let_def) |
766 then show ?case by (cases "simpnum a") (auto simp add: Let_def) |
761 next |
767 next |
762 case (12 i a) hence nb: "numbound0 a" by simp |
768 case (12 i a) then have nb: "numbound0 a" by simp |
763 hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb]) |
769 then have "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb]) |
764 thus ?case by (cases "simpnum a") (auto simp add: Let_def) |
770 then show ?case by (cases "simpnum a") (auto simp add: Let_def) |
765 next |
771 next |
766 case (13 i a) hence nb: "numbound0 a" by simp |
772 case (13 i a) then have nb: "numbound0 a" by simp |
767 hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb]) |
773 then have "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb]) |
768 thus ?case by (cases "simpnum a") (auto simp add: Let_def) |
774 then show ?case by (cases "simpnum a") (auto simp add: Let_def) |
769 qed (auto simp add: disj_def imp_def iff_def conj_def not_bn) |
775 qed (auto simp add: disj_def imp_def iff_def conj_def not_bn) |
770 |
776 |
771 lemma simpfm_qf: "qfree p \<Longrightarrow> qfree (simpfm p)" |
777 lemma simpfm_qf: "qfree p \<Longrightarrow> qfree (simpfm p)" |
772 by (induct p rule: simpfm.induct, auto simp add: disj_qf imp_qf iff_qf conj_qf not_qf Let_def) |
778 by (induct p rule: simpfm.induct, auto simp add: disj_qf imp_qf iff_qf conj_qf not_qf Let_def) |
773 (case_tac "simpnum a", auto)+ |
779 (case_tac "simpnum a", auto)+ |
785 | "qelim p = (\<lambda>y. simpfm p)" |
791 | "qelim p = (\<lambda>y. simpfm p)" |
786 by pat_completeness auto |
792 by pat_completeness auto |
787 termination by (relation "measure fmsize") auto |
793 termination by (relation "measure fmsize") auto |
788 |
794 |
789 lemma qelim_ci: |
795 lemma qelim_ci: |
790 assumes qe_inv: "\<forall>bs p. qfree p \<longrightarrow> qfree (qe p) \<and> (Ifm bbs bs (qe p) = Ifm bbs bs (E p))" |
796 assumes qe_inv: "\<forall>bs p. qfree p \<longrightarrow> qfree (qe p) \<and> Ifm bbs bs (qe p) = Ifm bbs bs (E p)" |
791 shows "\<And>bs. qfree (qelim p qe) \<and> (Ifm bbs bs (qelim p qe) = Ifm bbs bs p)" |
797 shows "\<And>bs. qfree (qelim p qe) \<and> Ifm bbs bs (qelim p qe) = Ifm bbs bs p" |
792 using qe_inv DJ_qe[OF qe_inv] |
798 using qe_inv DJ_qe[OF qe_inv] |
793 by(induct p rule: qelim.induct) |
799 by(induct p rule: qelim.induct) |
794 (auto simp add: not disj conj iff imp not_qf disj_qf conj_qf imp_qf iff_qf |
800 (auto simp add: not disj conj iff imp not_qf disj_qf conj_qf imp_qf iff_qf |
795 simpfm simpfm_qf simp del: simpfm.simps) |
801 simpfm simpfm_qf simp del: simpfm.simps) |
796 |
802 |
797 text {* Linearity for fm where Bound 0 ranges over @{text "\<int>"} *} |
803 text {* Linearity for fm where Bound 0 ranges over @{text "\<int>"} *} |
798 |
804 |
799 fun zsplit0 :: "num \<Rightarrow> int \<times> num" -- {* splits the bounded from the unbounded part *} |
805 fun zsplit0 :: "num \<Rightarrow> int \<times> num" -- {* splits the bounded from the unbounded part *} |
800 where |
806 where |
801 "zsplit0 (C c) = (0,C c)" |
807 "zsplit0 (C c) = (0, C c)" |
802 | "zsplit0 (Bound n) = (if n=0 then (1, C 0) else (0,Bound n))" |
808 | "zsplit0 (Bound n) = (if n = 0 then (1, C 0) else (0, Bound n))" |
803 | "zsplit0 (CN n i a) = |
809 | "zsplit0 (CN n i a) = |
804 (let (i',a') = zsplit0 a |
810 (let (i', a') = zsplit0 a |
805 in if n=0 then (i+i', a') else (i',CN n i a'))" |
811 in if n = 0 then (i + i', a') else (i', CN n i a'))" |
806 | "zsplit0 (Neg a) = (let (i',a') = zsplit0 a in (-i', Neg a'))" |
812 | "zsplit0 (Neg a) = (let (i', a') = zsplit0 a in (-i', Neg a'))" |
807 | "zsplit0 (Add a b) = (let (ia,a') = zsplit0 a ; |
813 | "zsplit0 (Add a b) = |
808 (ib,b') = zsplit0 b |
814 (let |
809 in (ia+ib, Add a' b'))" |
815 (ia, a') = zsplit0 a; |
810 | "zsplit0 (Sub a b) = (let (ia,a') = zsplit0 a ; |
816 (ib, b') = zsplit0 b |
811 (ib,b') = zsplit0 b |
817 in (ia + ib, Add a' b'))" |
812 in (ia-ib, Sub a' b'))" |
818 | "zsplit0 (Sub a b) = |
813 | "zsplit0 (Mul i a) = (let (i',a') = zsplit0 a in (i*i', Mul i a'))" |
819 (let |
|
820 (ia, a') = zsplit0 a; |
|
821 (ib, b') = zsplit0 b |
|
822 in (ia - ib, Sub a' b'))" |
|
823 | "zsplit0 (Mul i a) = (let (i', a') = zsplit0 a in (i*i', Mul i a'))" |
814 |
824 |
815 lemma zsplit0_I: |
825 lemma zsplit0_I: |
816 shows "\<And>n a. zsplit0 t = (n,a) \<Longrightarrow> (Inum ((x::int) #bs) (CN 0 n a) = Inum (x #bs) t) \<and> numbound0 a" |
826 shows "\<And>n a. zsplit0 t = (n,a) \<Longrightarrow> (Inum ((x::int) #bs) (CN 0 n a) = Inum (x #bs) t) \<and> numbound0 a" |
817 (is "\<And>n a. ?S t = (n,a) \<Longrightarrow> (?I x (CN 0 n a) = ?I x t) \<and> ?N a") |
827 (is "\<And>n a. ?S t = (n,a) \<Longrightarrow> (?I x (CN 0 n a) = ?I x t) \<and> ?N a") |
818 proof (induct t rule: zsplit0.induct) |
828 proof (induct t rule: zsplit0.induct) |
1423 proof(clarsimp) |
1431 proof(clarsimp) |
1424 fix x assume "x < (- Inum (a#bs) e)" and"x + Inum (x#bs) e = 0" |
1432 fix x assume "x < (- Inum (a#bs) e)" and"x + Inum (x#bs) e = 0" |
1425 with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"] |
1433 with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"] |
1426 show "False" by simp |
1434 show "False" by simp |
1427 qed |
1435 qed |
1428 thus ?case by auto |
1436 then show ?case by auto |
1429 next |
1437 next |
1430 case (5 c e) hence c1: "c=1" and nb: "numbound0 e" by simp_all |
1438 case (5 c e) then have c1: "c=1" and nb: "numbound0 e" by simp_all |
1431 fix a |
1439 fix a |
1432 from 5 have "\<forall>x<(- Inum (a#bs) e). c*x + Inum (x#bs) e < 0" |
1440 from 5 have "\<forall>x<(- Inum (a#bs) e). c*x + Inum (x#bs) e < 0" |
1433 proof(clarsimp) |
1441 proof(clarsimp) |
1434 fix x assume "x < (- Inum (a#bs) e)" |
1442 fix x assume "x < (- Inum (a#bs) e)" |
1435 with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"] |
1443 with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"] |
1436 show "x + Inum (x#bs) e < 0" by simp |
1444 show "x + Inum (x#bs) e < 0" by simp |
1437 qed |
1445 qed |
1438 thus ?case by auto |
1446 then show ?case by auto |
1439 next |
1447 next |
1440 case (6 c e) hence c1: "c=1" and nb: "numbound0 e" by simp_all |
1448 case (6 c e) then have c1: "c=1" and nb: "numbound0 e" by simp_all |
1441 fix a |
1449 fix a |
1442 from 6 have "\<forall>x<(- Inum (a#bs) e). c*x + Inum (x#bs) e \<le> 0" |
1450 from 6 have "\<forall>x<(- Inum (a#bs) e). c*x + Inum (x#bs) e \<le> 0" |
1443 proof(clarsimp) |
1451 proof(clarsimp) |
1444 fix x assume "x < (- Inum (a#bs) e)" |
1452 fix x assume "x < (- Inum (a#bs) e)" |
1445 with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"] |
1453 with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"] |
1446 show "x + Inum (x#bs) e \<le> 0" by simp |
1454 show "x + Inum (x#bs) e \<le> 0" by simp |
1447 qed |
1455 qed |
1448 thus ?case by auto |
1456 then show ?case by auto |
1449 next |
1457 next |
1450 case (7 c e) hence c1: "c=1" and nb: "numbound0 e" by simp_all |
1458 case (7 c e) then have c1: "c=1" and nb: "numbound0 e" by simp_all |
1451 fix a |
1459 fix a |
1452 from 7 have "\<forall>x<(- Inum (a#bs) e). \<not> (c*x + Inum (x#bs) e > 0)" |
1460 from 7 have "\<forall>x<(- Inum (a#bs) e). \<not> (c*x + Inum (x#bs) e > 0)" |
1453 proof(clarsimp) |
1461 proof(clarsimp) |
1454 fix x assume "x < (- Inum (a#bs) e)" and"x + Inum (x#bs) e > 0" |
1462 fix x assume "x < (- Inum (a#bs) e)" and"x + Inum (x#bs) e > 0" |
1455 with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"] |
1463 with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"] |
1456 show "False" by simp |
1464 show "False" by simp |
1457 qed |
1465 qed |
1458 thus ?case by auto |
1466 then show ?case by auto |
1459 next |
1467 next |
1460 case (8 c e) hence c1: "c=1" and nb: "numbound0 e" by simp_all |
1468 case (8 c e) then have c1: "c=1" and nb: "numbound0 e" by simp_all |
1461 fix a |
1469 fix a |
1462 from 8 have "\<forall>x<(- Inum (a#bs) e). \<not> (c*x + Inum (x#bs) e \<ge> 0)" |
1470 from 8 have "\<forall>x<(- Inum (a#bs) e). \<not> (c*x + Inum (x#bs) e \<ge> 0)" |
1463 proof(clarsimp) |
1471 proof(clarsimp) |
1464 fix x assume "x < (- Inum (a#bs) e)" and"x + Inum (x#bs) e \<ge> 0" |
1472 fix x assume "x < (- Inum (a#bs) e)" and"x + Inum (x#bs) e \<ge> 0" |
1465 with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"] |
1473 with numbound0_I[OF nb, where bs="bs" and b="a" and b'="x"] |
1466 show "False" by simp |
1474 show "False" by simp |
1467 qed |
1475 qed |
1468 thus ?case by auto |
1476 then show ?case by auto |
1469 qed auto |
1477 qed auto |
1470 |
1478 |
1471 lemma minusinf_repeats: |
1479 lemma minusinf_repeats: |
1472 assumes d: "d_\<delta> p d" and linp: "iszlfm p" |
1480 assumes d: "d_\<delta> p d" and linp: "iszlfm p" |
1473 shows "Ifm bbs ((x - k*d)#bs) (minusinf p) = Ifm bbs (x #bs) (minusinf p)" |
1481 shows "Ifm bbs ((x - k*d)#bs) (minusinf p) = Ifm bbs (x #bs) (minusinf p)" |
1474 using linp d |
1482 using linp d |
1475 proof (induct p rule: iszlfm.induct) |
1483 proof (induct p rule: iszlfm.induct) |
1476 case (9 i c e) |
1484 case (9 i c e) |
1477 hence nbe: "numbound0 e" and id: "i dvd d" by simp_all |
1485 then have nbe: "numbound0 e" and id: "i dvd d" by simp_all |
1478 hence "\<exists>k. d=i*k" by (simp add: dvd_def) |
1486 then have "\<exists>k. d=i*k" by (simp add: dvd_def) |
1479 then obtain "di" where di_def: "d=i*di" by blast |
1487 then obtain "di" where di_def: "d=i*di" by blast |
1480 show ?case |
1488 show ?case |
1481 proof (simp add: numbound0_I[OF nbe,where bs="bs" and b="x - k * d" and b'="x"] right_diff_distrib, |
1489 proof (simp add: numbound0_I[OF nbe,where bs="bs" and b="x - k * d" and b'="x"] right_diff_distrib, |
1482 rule iffI) |
1490 rule iffI) |
1483 assume "i dvd c * x - c*(k*d) + Inum (x # bs) e" |
1491 assume "i dvd c * x - c*(k*d) + Inum (x # bs) e" |
1484 (is "?ri dvd ?rc*?rx - ?rc*(?rk*?rd) + ?I x e" is "?ri dvd ?rt") |
1492 (is "?ri dvd ?rc*?rx - ?rc*(?rk*?rd) + ?I x e" is "?ri dvd ?rt") |
1485 hence "\<exists>(l::int). ?rt = i * l" by (simp add: dvd_def) |
1493 then have "\<exists>(l::int). ?rt = i * l" by (simp add: dvd_def) |
1486 hence "\<exists>(l::int). c*x+ ?I x e = i*l+c*(k * i*di)" |
1494 then have "\<exists>(l::int). c*x+ ?I x e = i*l+c*(k * i*di)" |
1487 by (simp add: algebra_simps di_def) |
1495 by (simp add: algebra_simps di_def) |
1488 hence "\<exists>(l::int). c*x+ ?I x e = i*(l + c*k*di)" |
1496 then have "\<exists>(l::int). c*x+ ?I x e = i*(l + c*k*di)" |
1489 by (simp add: algebra_simps) |
1497 by (simp add: algebra_simps) |
1490 hence "\<exists>(l::int). c*x+ ?I x e = i*l" by blast |
1498 then have "\<exists>(l::int). c*x+ ?I x e = i*l" by blast |
1491 thus "i dvd c*x + Inum (x # bs) e" by (simp add: dvd_def) |
1499 then show "i dvd c*x + Inum (x # bs) e" by (simp add: dvd_def) |
1492 next |
1500 next |
1493 assume "i dvd c*x + Inum (x # bs) e" (is "?ri dvd ?rc*?rx+?e") |
1501 assume "i dvd c*x + Inum (x # bs) e" (is "?ri dvd ?rc*?rx+?e") |
1494 hence "\<exists>(l::int). c*x+?e = i*l" by (simp add: dvd_def) |
1502 then have "\<exists>(l::int). c*x+?e = i*l" by (simp add: dvd_def) |
1495 hence "\<exists>(l::int). c*x - c*(k*d) +?e = i*l - c*(k*d)" by simp |
1503 then have "\<exists>(l::int). c*x - c*(k*d) +?e = i*l - c*(k*d)" by simp |
1496 hence "\<exists>(l::int). c*x - c*(k*d) +?e = i*l - c*(k*i*di)" by (simp add: di_def) |
1504 then have "\<exists>(l::int). c*x - c*(k*d) +?e = i*l - c*(k*i*di)" by (simp add: di_def) |
1497 hence "\<exists>(l::int). c*x - c*(k*d) +?e = i*((l - c*k*di))" by (simp add: algebra_simps) |
1505 then have "\<exists>(l::int). c*x - c*(k*d) +?e = i*((l - c*k*di))" by (simp add: algebra_simps) |
1498 hence "\<exists>(l::int). c*x - c * (k*d) +?e = i*l" by blast |
1506 then have "\<exists>(l::int). c*x - c * (k*d) +?e = i*l" by blast |
1499 thus "i dvd c*x - c*(k*d) + Inum (x # bs) e" by (simp add: dvd_def) |
1507 then show "i dvd c*x - c*(k*d) + Inum (x # bs) e" by (simp add: dvd_def) |
1500 qed |
1508 qed |
1501 next |
1509 next |
1502 case (10 i c e) |
1510 case (10 i c e) |
1503 hence nbe: "numbound0 e" and id: "i dvd d" by simp_all |
1511 then have nbe: "numbound0 e" and id: "i dvd d" by simp_all |
1504 hence "\<exists>k. d=i*k" by (simp add: dvd_def) |
1512 then have "\<exists>k. d=i*k" by (simp add: dvd_def) |
1505 then obtain "di" where di_def: "d=i*di" by blast |
1513 then obtain "di" where di_def: "d=i*di" by blast |
1506 show ?case |
1514 show ?case |
1507 proof(simp add: numbound0_I[OF nbe,where bs="bs" and b="x - k * d" and b'="x"] right_diff_distrib, rule iffI) |
1515 proof(simp add: numbound0_I[OF nbe,where bs="bs" and b="x - k * d" and b'="x"] right_diff_distrib, rule iffI) |
1508 assume "i dvd c * x - c*(k*d) + Inum (x # bs) e" |
1516 assume "i dvd c * x - c*(k*d) + Inum (x # bs) e" |
1509 (is "?ri dvd ?rc*?rx - ?rc*(?rk*?rd) + ?I x e" is "?ri dvd ?rt") |
1517 (is "?ri dvd ?rc*?rx - ?rc*(?rk*?rd) + ?I x e" is "?ri dvd ?rt") |
1510 hence "\<exists>(l::int). ?rt = i * l" by (simp add: dvd_def) |
1518 then have "\<exists>(l::int). ?rt = i * l" by (simp add: dvd_def) |
1511 hence "\<exists>(l::int). c*x+ ?I x e = i*l+c*(k * i*di)" |
1519 then have "\<exists>(l::int). c*x+ ?I x e = i*l+c*(k * i*di)" |
1512 by (simp add: algebra_simps di_def) |
1520 by (simp add: algebra_simps di_def) |
1513 hence "\<exists>(l::int). c*x+ ?I x e = i*(l + c*k*di)" |
1521 then have "\<exists>(l::int). c*x+ ?I x e = i*(l + c*k*di)" |
1514 by (simp add: algebra_simps) |
1522 by (simp add: algebra_simps) |
1515 hence "\<exists>(l::int). c*x+ ?I x e = i*l" by blast |
1523 then have "\<exists>(l::int). c*x+ ?I x e = i*l" by blast |
1516 thus "i dvd c*x + Inum (x # bs) e" by (simp add: dvd_def) |
1524 then show "i dvd c*x + Inum (x # bs) e" by (simp add: dvd_def) |
1517 next |
1525 next |
1518 assume |
1526 assume |
1519 "i dvd c*x + Inum (x # bs) e" (is "?ri dvd ?rc*?rx+?e") |
1527 "i dvd c*x + Inum (x # bs) e" (is "?ri dvd ?rc*?rx+?e") |
1520 hence "\<exists>(l::int). c*x+?e = i*l" by (simp add: dvd_def) |
1528 then have "\<exists>(l::int). c*x+?e = i*l" by (simp add: dvd_def) |
1521 hence "\<exists>(l::int). c*x - c*(k*d) +?e = i*l - c*(k*d)" by simp |
1529 then have "\<exists>(l::int). c*x - c*(k*d) +?e = i*l - c*(k*d)" by simp |
1522 hence "\<exists>(l::int). c*x - c*(k*d) +?e = i*l - c*(k*i*di)" by (simp add: di_def) |
1530 then have "\<exists>(l::int). c*x - c*(k*d) +?e = i*l - c*(k*i*di)" by (simp add: di_def) |
1523 hence "\<exists>(l::int). c*x - c*(k*d) +?e = i*((l - c*k*di))" by (simp add: algebra_simps) |
1531 then have "\<exists>(l::int). c*x - c*(k*d) +?e = i*((l - c*k*di))" by (simp add: algebra_simps) |
1524 hence "\<exists>(l::int). c*x - c * (k*d) +?e = i*l" |
1532 then have "\<exists>(l::int). c*x - c * (k*d) +?e = i*l" |
1525 by blast |
1533 by blast |
1526 thus "i dvd c*x - c*(k*d) + Inum (x # bs) e" by (simp add: dvd_def) |
1534 then show "i dvd c*x - c*(k*d) + Inum (x # bs) e" by (simp add: dvd_def) |
1527 qed |
1535 qed |
1528 qed (auto simp add: gr0_conv_Suc numbound0_I[where bs="bs" and b="x - k*d" and b'="x"]) |
1536 qed (auto simp add: gr0_conv_Suc numbound0_I[where bs="bs" and b="x - k*d" and b'="x"]) |
1529 |
1537 |
1530 lemma mirror_\<alpha>_\<beta>: |
1538 lemma mirror_\<alpha>_\<beta>: |
1531 assumes lp: "iszlfm p" |
1539 assumes lp: "iszlfm p" |
1611 assumes linp: "iszlfm p" and d: "d_\<beta> p l" and lp: "l > 0" |
1619 assumes linp: "iszlfm p" and d: "d_\<beta> p l" and lp: "l > 0" |
1612 shows "iszlfm (a_\<beta> p l) \<and> d_\<beta> (a_\<beta> p l) 1 \<and> (Ifm bbs (l*x #bs) (a_\<beta> p l) = Ifm bbs (x#bs) p)" |
1620 shows "iszlfm (a_\<beta> p l) \<and> d_\<beta> (a_\<beta> p l) 1 \<and> (Ifm bbs (l*x #bs) (a_\<beta> p l) = Ifm bbs (x#bs) p)" |
1613 using linp d |
1621 using linp d |
1614 proof (induct p rule: iszlfm.induct) |
1622 proof (induct p rule: iszlfm.induct) |
1615 case (5 c e) |
1623 case (5 c e) |
1616 hence cp: "c>0" and be: "numbound0 e" and d': "c dvd l" by simp_all |
1624 then have cp: "c>0" and be: "numbound0 e" and d': "c dvd l" by simp_all |
1617 from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp]) |
1625 from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp]) |
1618 from cp have cnz: "c \<noteq> 0" by simp |
1626 from cp have cnz: "c \<noteq> 0" by simp |
1619 have "c div c\<le> l div c" |
1627 have "c div c\<le> l div c" |
1620 by (simp add: zdiv_mono1[OF clel cp]) |
1628 by (simp add: zdiv_mono1[OF clel cp]) |
1621 then have ldcp:"0 < l div c" |
1629 then have ldcp:"0 < l div c" |
1622 by (simp add: div_self[OF cnz]) |
1630 by (simp add: div_self[OF cnz]) |
1623 have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] |
1631 have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] |
1624 by simp |
1632 by simp |
1625 hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] |
1633 then have cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] |
1626 by simp |
1634 by simp |
1627 hence "(l*x + (l div c) * Inum (x # bs) e < 0) = |
1635 then have "(l*x + (l div c) * Inum (x # bs) e < 0) = |
1628 ((c * (l div c)) * x + (l div c) * Inum (x # bs) e < 0)" |
1636 ((c * (l div c)) * x + (l div c) * Inum (x # bs) e < 0)" |
1629 by simp |
1637 by simp |
1630 also have "\<dots> = ((l div c) * (c*x + Inum (x # bs) e) < (l div c) * 0)" |
1638 also have "\<dots> = ((l div c) * (c*x + Inum (x # bs) e) < (l div c) * 0)" |
1631 by (simp add: algebra_simps) |
1639 by (simp add: algebra_simps) |
1632 also have "\<dots> = (c*x + Inum (x # bs) e < 0)" |
1640 also have "\<dots> = (c*x + Inum (x # bs) e < 0)" |
1633 using mult_less_0_iff [where a="(l div c)" and b="c*x + Inum (x # bs) e"] ldcp by simp |
1641 using mult_less_0_iff [where a="(l div c)" and b="c*x + Inum (x # bs) e"] ldcp by simp |
1634 finally show ?case |
1642 finally show ?case |
1635 using numbound0_I[OF be,where b="l*x" and b'="x" and bs="bs"] be by simp |
1643 using numbound0_I[OF be,where b="l*x" and b'="x" and bs="bs"] be by simp |
1636 next |
1644 next |
1637 case (6 c e) |
1645 case (6 c e) |
1638 hence cp: "c>0" and be: "numbound0 e" and d': "c dvd l" by simp_all |
1646 then have cp: "c>0" and be: "numbound0 e" and d': "c dvd l" by simp_all |
1639 from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp]) |
1647 from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp]) |
1640 from cp have cnz: "c \<noteq> 0" by simp |
1648 from cp have cnz: "c \<noteq> 0" by simp |
1641 have "c div c\<le> l div c" |
1649 have "c div c\<le> l div c" |
1642 by (simp add: zdiv_mono1[OF clel cp]) |
1650 by (simp add: zdiv_mono1[OF clel cp]) |
1643 then have ldcp:"0 < l div c" |
1651 then have ldcp:"0 < l div c" |
1644 by (simp add: div_self[OF cnz]) |
1652 by (simp add: div_self[OF cnz]) |
1645 have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] |
1653 have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] |
1646 by simp |
1654 by simp |
1647 hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] |
1655 then have cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] |
1648 by simp |
1656 by simp |
1649 hence "(l*x + (l div c) * Inum (x# bs) e \<le> 0) = |
1657 then have "(l*x + (l div c) * Inum (x# bs) e \<le> 0) = |
1650 ((c * (l div c)) * x + (l div c) * Inum (x # bs) e \<le> 0)" by simp |
1658 ((c * (l div c)) * x + (l div c) * Inum (x # bs) e \<le> 0)" by simp |
1651 also have "\<dots> = ((l div c) * (c * x + Inum (x # bs) e) \<le> ((l div c)) * 0)" |
1659 also have "\<dots> = ((l div c) * (c * x + Inum (x # bs) e) \<le> ((l div c)) * 0)" |
1652 by (simp add: algebra_simps) |
1660 by (simp add: algebra_simps) |
1653 also have "\<dots> = (c*x + Inum (x # bs) e \<le> 0)" |
1661 also have "\<dots> = (c*x + Inum (x # bs) e \<le> 0)" |
1654 using mult_le_0_iff [where a="(l div c)" and b="c*x + Inum (x # bs) e"] ldcp by simp |
1662 using mult_le_0_iff [where a="(l div c)" and b="c*x + Inum (x # bs) e"] ldcp by simp |
1655 finally show ?case |
1663 finally show ?case |
1656 using numbound0_I[OF be,where b="l*x" and b'="x" and bs="bs"] be by simp |
1664 using numbound0_I[OF be,where b="l*x" and b'="x" and bs="bs"] be by simp |
1657 next |
1665 next |
1658 case (7 c e) |
1666 case (7 c e) |
1659 hence cp: "c>0" and be: "numbound0 e" and d': "c dvd l" by simp_all |
1667 then have cp: "c>0" and be: "numbound0 e" and d': "c dvd l" by simp_all |
1660 from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp]) |
1668 from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp]) |
1661 from cp have cnz: "c \<noteq> 0" by simp |
1669 from cp have cnz: "c \<noteq> 0" by simp |
1662 have "c div c\<le> l div c" |
1670 have "c div c\<le> l div c" |
1663 by (simp add: zdiv_mono1[OF clel cp]) |
1671 by (simp add: zdiv_mono1[OF clel cp]) |
1664 then have ldcp:"0 < l div c" |
1672 then have ldcp:"0 < l div c" |
1665 by (simp add: div_self[OF cnz]) |
1673 by (simp add: div_self[OF cnz]) |
1666 have "c * (l div c) = c* (l div c) + l mod c" |
1674 have "c * (l div c) = c* (l div c) + l mod c" |
1667 using d' dvd_eq_mod_eq_0[of "c" "l"] by simp |
1675 using d' dvd_eq_mod_eq_0[of "c" "l"] by simp |
1668 hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] |
1676 then have cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] |
1669 by simp |
1677 by simp |
1670 hence "(l*x + (l div c)* Inum (x # bs) e > 0) = |
1678 then have "(l*x + (l div c)* Inum (x # bs) e > 0) = |
1671 ((c * (l div c)) * x + (l div c) * Inum (x # bs) e > 0)" by simp |
1679 ((c * (l div c)) * x + (l div c) * Inum (x # bs) e > 0)" by simp |
1672 also have "\<dots> = ((l div c) * (c * x + Inum (x # bs) e) > ((l div c)) * 0)" |
1680 also have "\<dots> = ((l div c) * (c * x + Inum (x # bs) e) > ((l div c)) * 0)" |
1673 by (simp add: algebra_simps) |
1681 by (simp add: algebra_simps) |
1674 also have "\<dots> = (c * x + Inum (x # bs) e > 0)" |
1682 also have "\<dots> = (c * x + Inum (x # bs) e > 0)" |
1675 using zero_less_mult_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e"] ldcp by simp |
1683 using zero_less_mult_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e"] ldcp by simp |
1676 finally show ?case |
1684 finally show ?case |
1677 using numbound0_I[OF be,where b="(l * x)" and b'="x" and bs="bs"] be by simp |
1685 using numbound0_I[OF be,where b="(l * x)" and b'="x" and bs="bs"] be by simp |
1678 next |
1686 next |
1679 case (8 c e) |
1687 case (8 c e) |
1680 hence cp: "c>0" and be: "numbound0 e" and d': "c dvd l" by simp_all |
1688 then have cp: "c>0" and be: "numbound0 e" and d': "c dvd l" by simp_all |
1681 from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp]) |
1689 from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp]) |
1682 from cp have cnz: "c \<noteq> 0" by simp |
1690 from cp have cnz: "c \<noteq> 0" by simp |
1683 have "c div c\<le> l div c" |
1691 have "c div c\<le> l div c" |
1684 by (simp add: zdiv_mono1[OF clel cp]) |
1692 by (simp add: zdiv_mono1[OF clel cp]) |
1685 then have ldcp:"0 < l div c" |
1693 then have ldcp:"0 < l div c" |
1686 by (simp add: div_self[OF cnz]) |
1694 by (simp add: div_self[OF cnz]) |
1687 have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] |
1695 have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] |
1688 by simp |
1696 by simp |
1689 hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] |
1697 then have cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] |
1690 by simp |
1698 by simp |
1691 hence "(l*x + (l div c)* Inum (x # bs) e \<ge> 0) = |
1699 then have "(l*x + (l div c)* Inum (x # bs) e \<ge> 0) = |
1692 ((c*(l div c))*x + (l div c)* Inum (x # bs) e \<ge> 0)" by simp |
1700 ((c*(l div c))*x + (l div c)* Inum (x # bs) e \<ge> 0)" by simp |
1693 also have "\<dots> = ((l div c)*(c*x + Inum (x # bs) e) \<ge> ((l div c)) * 0)" |
1701 also have "\<dots> = ((l div c)*(c*x + Inum (x # bs) e) \<ge> ((l div c)) * 0)" |
1694 by (simp add: algebra_simps) |
1702 by (simp add: algebra_simps) |
1695 also have "\<dots> = (c*x + Inum (x # bs) e \<ge> 0)" |
1703 also have "\<dots> = (c*x + Inum (x # bs) e \<ge> 0)" |
1696 using ldcp zero_le_mult_iff [where a="l div c" and b="c*x + Inum (x # bs) e"] by simp |
1704 using ldcp zero_le_mult_iff [where a="l div c" and b="c*x + Inum (x # bs) e"] by simp |
1697 finally show ?case |
1705 finally show ?case |
1698 using be numbound0_I[OF be,where b="l*x" and b'="x" and bs="bs"] by simp |
1706 using be numbound0_I[OF be,where b="l*x" and b'="x" and bs="bs"] by simp |
1699 next |
1707 next |
1700 case (3 c e) |
1708 case (3 c e) |
1701 hence cp: "c>0" and be: "numbound0 e" and d': "c dvd l" by simp_all |
1709 then have cp: "c>0" and be: "numbound0 e" and d': "c dvd l" by simp_all |
1702 from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp]) |
1710 from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp]) |
1703 from cp have cnz: "c \<noteq> 0" by simp |
1711 from cp have cnz: "c \<noteq> 0" by simp |
1704 have "c div c\<le> l div c" |
1712 have "c div c\<le> l div c" |
1705 by (simp add: zdiv_mono1[OF clel cp]) |
1713 by (simp add: zdiv_mono1[OF clel cp]) |
1706 then have ldcp:"0 < l div c" |
1714 then have ldcp:"0 < l div c" |
1707 by (simp add: div_self[OF cnz]) |
1715 by (simp add: div_self[OF cnz]) |
1708 have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] |
1716 have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] |
1709 by simp |
1717 by simp |
1710 hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] |
1718 then have cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] |
1711 by simp |
1719 by simp |
1712 hence "(l * x + (l div c) * Inum (x # bs) e = 0) = |
1720 then have "(l * x + (l div c) * Inum (x # bs) e = 0) = |
1713 ((c * (l div c)) * x + (l div c) * Inum (x # bs) e = 0)" by simp |
1721 ((c * (l div c)) * x + (l div c) * Inum (x # bs) e = 0)" by simp |
1714 also have "\<dots> = ((l div c) * (c * x + Inum (x # bs) e) = ((l div c)) * 0)" |
1722 also have "\<dots> = ((l div c) * (c * x + Inum (x # bs) e) = ((l div c)) * 0)" |
1715 by (simp add: algebra_simps) |
1723 by (simp add: algebra_simps) |
1716 also have "\<dots> = (c * x + Inum (x # bs) e = 0)" |
1724 also have "\<dots> = (c * x + Inum (x # bs) e = 0)" |
1717 using mult_eq_0_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e"] ldcp by simp |
1725 using mult_eq_0_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e"] ldcp by simp |
1718 finally show ?case |
1726 finally show ?case |
1719 using numbound0_I[OF be,where b="(l * x)" and b'="x" and bs="bs"] be by simp |
1727 using numbound0_I[OF be,where b="(l * x)" and b'="x" and bs="bs"] be by simp |
1720 next |
1728 next |
1721 case (4 c e) |
1729 case (4 c e) |
1722 hence cp: "c>0" and be: "numbound0 e" and d': "c dvd l" by simp_all |
1730 then have cp: "c>0" and be: "numbound0 e" and d': "c dvd l" by simp_all |
1723 from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp]) |
1731 from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp]) |
1724 from cp have cnz: "c \<noteq> 0" by simp |
1732 from cp have cnz: "c \<noteq> 0" by simp |
1725 have "c div c\<le> l div c" |
1733 have "c div c\<le> l div c" |
1726 by (simp add: zdiv_mono1[OF clel cp]) |
1734 by (simp add: zdiv_mono1[OF clel cp]) |
1727 then have ldcp:"0 < l div c" |
1735 then have ldcp:"0 < l div c" |
1728 by (simp add: div_self[OF cnz]) |
1736 by (simp add: div_self[OF cnz]) |
1729 have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] |
1737 have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] |
1730 by simp |
1738 by simp |
1731 hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] |
1739 then have cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] |
1732 by simp |
1740 by simp |
1733 hence "(l * x + (l div c) * Inum (x # bs) e \<noteq> 0) = |
1741 then have "(l * x + (l div c) * Inum (x # bs) e \<noteq> 0) = |
1734 ((c * (l div c)) * x + (l div c) * Inum (x # bs) e \<noteq> 0)" by simp |
1742 ((c * (l div c)) * x + (l div c) * Inum (x # bs) e \<noteq> 0)" by simp |
1735 also have "\<dots> = ((l div c) * (c * x + Inum (x # bs) e) \<noteq> ((l div c)) * 0)" |
1743 also have "\<dots> = ((l div c) * (c * x + Inum (x # bs) e) \<noteq> ((l div c)) * 0)" |
1736 by (simp add: algebra_simps) |
1744 by (simp add: algebra_simps) |
1737 also have "\<dots> = (c * x + Inum (x # bs) e \<noteq> 0)" |
1745 also have "\<dots> = (c * x + Inum (x # bs) e \<noteq> 0)" |
1738 using zero_le_mult_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e"] ldcp by simp |
1746 using zero_le_mult_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e"] ldcp by simp |
1739 finally show ?case |
1747 finally show ?case |
1740 using numbound0_I[OF be,where b="(l * x)" and b'="x" and bs="bs"] be by simp |
1748 using numbound0_I[OF be,where b="(l * x)" and b'="x" and bs="bs"] be by simp |
1741 next |
1749 next |
1742 case (9 j c e) |
1750 case (9 j c e) |
1743 hence cp: "c>0" and be: "numbound0 e" and jp: "j > 0" and d': "c dvd l" by simp_all |
1751 then have cp: "c>0" and be: "numbound0 e" and jp: "j > 0" and d': "c dvd l" by simp_all |
1744 from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp]) |
1752 from lp cp have clel: "c\<le>l" by (simp add: zdvd_imp_le [OF d' lp]) |
1745 from cp have cnz: "c \<noteq> 0" by simp |
1753 from cp have cnz: "c \<noteq> 0" by simp |
1746 have "c div c\<le> l div c" |
1754 have "c div c\<le> l div c" |
1747 by (simp add: zdiv_mono1[OF clel cp]) |
1755 by (simp add: zdiv_mono1[OF clel cp]) |
1748 then have ldcp:"0 < l div c" |
1756 then have ldcp:"0 < l div c" |
1749 by (simp add: div_self[OF cnz]) |
1757 by (simp add: div_self[OF cnz]) |
1750 have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] |
1758 have "c * (l div c) = c* (l div c) + l mod c" using d' dvd_eq_mod_eq_0[of "c" "l"] |
1751 by simp |
1759 by simp |
1752 hence cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] |
1760 then have cl:"c * (l div c) =l" using zmod_zdiv_equality[where a="l" and b="c", symmetric] |
1753 by simp |
1761 by simp |
1754 hence "(\<exists>(k::int). l * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k) = |
1762 then have "(\<exists>(k::int). l * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k) = |
1755 (\<exists>(k::int). (c * (l div c)) * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k)" by simp |
1763 (\<exists>(k::int). (c * (l div c)) * x + (l div c) * Inum (x # bs) e = ((l div c) * j) * k)" by simp |
1756 also have "\<dots> = (\<exists>(k::int). (l div c) * (c * x + Inum (x # bs) e - j * k) = (l div c)*0)" |
1764 also have "\<dots> = (\<exists>(k::int). (l div c) * (c * x + Inum (x # bs) e - j * k) = (l div c)*0)" |
1757 by (simp add: algebra_simps) |
1765 by (simp add: algebra_simps) |
1758 also have "\<dots> = (\<exists>(k::int). c * x + Inum (x # bs) e - j * k = 0)" |
1766 also have "\<dots> = (\<exists>(k::int). c * x + Inum (x # bs) e - j * k = 0)" |
1759 using zero_le_mult_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e - j * k"] ldcp |
1767 using zero_le_mult_iff [where a="(l div c)" and b="c * x + Inum (x # bs) e - j * k"] ldcp |
1792 finally show ?thesis . |
1803 finally show ?thesis . |
1793 qed |
1804 qed |
1794 |
1805 |
1795 lemma \<beta>: |
1806 lemma \<beta>: |
1796 assumes lp: "iszlfm p" |
1807 assumes lp: "iszlfm p" |
1797 and u: "d_\<beta> p 1" |
1808 and u: "d_\<beta> p 1" |
1798 and d: "d_\<delta> p d" |
1809 and d: "d_\<delta> p d" |
1799 and dp: "d > 0" |
1810 and dp: "d > 0" |
1800 and nob: "\<not>(\<exists>(j::int) \<in> {1 .. d}. \<exists>b\<in> (Inum (a#bs)) ` set(\<beta> p). x = b + j)" |
1811 and nob: "\<not>(\<exists>(j::int) \<in> {1 .. d}. \<exists>b\<in> (Inum (a#bs)) ` set(\<beta> p). x = b + j)" |
1801 and p: "Ifm bbs (x#bs) p" (is "?P x") |
1812 and p: "Ifm bbs (x#bs) p" (is "?P x") |
1802 shows "?P (x - d)" |
1813 shows "?P (x - d)" |
1803 using lp u d dp nob p |
1814 using lp u d dp nob p |
1804 proof(induct p rule: iszlfm.induct) |
1815 proof (induct p rule: iszlfm.induct) |
1805 case (5 c e) hence c1: "c=1" and bn:"numbound0 e" by simp_all |
1816 case (5 c e) |
|
1817 then have c1: "c = 1" and bn: "numbound0 e" |
|
1818 by simp_all |
1806 with dp p c1 numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] 5 |
1819 with dp p c1 numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] 5 |
1807 show ?case by simp |
1820 show ?case by simp |
1808 next |
1821 next |
1809 case (6 c e) hence c1: "c=1" and bn:"numbound0 e" by simp_all |
1822 case (6 c e) |
|
1823 then have c1: "c = 1" and bn: "numbound0 e" |
|
1824 by simp_all |
1810 with dp p c1 numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] 6 |
1825 with dp p c1 numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] 6 |
1811 show ?case by simp |
1826 show ?case by simp |
1812 next |
1827 next |
1813 case (7 c e) hence p: "Ifm bbs (x #bs) (Gt (CN 0 c e))" and c1: "c=1" and bn:"numbound0 e" by simp_all |
1828 case (7 c e) |
|
1829 then have p: "Ifm bbs (x #bs) (Gt (CN 0 c e))" and c1: "c=1" and bn: "numbound0 e" |
|
1830 by simp_all |
1814 let ?e = "Inum (x # bs) e" |
1831 let ?e = "Inum (x # bs) e" |
1815 {assume "(x-d) +?e > 0" hence ?case using c1 |
1832 { |
1816 numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] by simp} |
1833 assume "(x-d) +?e > 0" |
|
1834 then have ?case |
|
1835 using c1 numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] by simp |
|
1836 } |
1817 moreover |
1837 moreover |
1818 {assume H: "\<not> (x-d) + ?e > 0" |
1838 { |
|
1839 assume H: "\<not> (x-d) + ?e > 0" |
1819 let ?v="Neg e" |
1840 let ?v="Neg e" |
1820 have vb: "?v \<in> set (\<beta> (Gt (CN 0 c e)))" by simp |
1841 have vb: "?v \<in> set (\<beta> (Gt (CN 0 c e)))" by simp |
1821 from 7(5)[simplified simp_thms Inum.simps \<beta>.simps set_simps bex_simps numbound0_I[OF bn,where b="a" and b'="x" and bs="bs"]] |
1842 from 7(5)[simplified simp_thms Inum.simps \<beta>.simps set_simps bex_simps numbound0_I[OF bn,where b="a" and b'="x" and bs="bs"]] |
1822 have nob: "\<not> (\<exists>j\<in> {1 ..d}. x = - ?e + j)" by auto |
1843 have nob: "\<not> (\<exists>j\<in> {1 ..d}. x = - ?e + j)" |
1823 from H p have "x + ?e > 0 \<and> x + ?e \<le> d" by (simp add: c1) |
1844 by auto |
1824 hence "x + ?e \<ge> 1 \<and> x + ?e \<le> d" by simp |
1845 from H p have "x + ?e > 0 \<and> x + ?e \<le> d" |
1825 hence "\<exists>(j::int) \<in> {1 .. d}. j = x + ?e" by simp |
1846 by (simp add: c1) |
1826 hence "\<exists>(j::int) \<in> {1 .. d}. x = (- ?e + j)" |
1847 then have "x + ?e \<ge> 1 \<and> x + ?e \<le> d" |
|
1848 by simp |
|
1849 then have "\<exists>(j::int) \<in> {1 .. d}. j = x + ?e" |
|
1850 by simp |
|
1851 then have "\<exists>(j::int) \<in> {1 .. d}. x = (- ?e + j)" |
1827 by (simp add: algebra_simps) |
1852 by (simp add: algebra_simps) |
1828 with nob have ?case by auto} |
1853 with nob have ?case |
1829 ultimately show ?case by blast |
1854 by auto |
1830 next |
1855 } |
1831 case (8 c e) hence p: "Ifm bbs (x #bs) (Ge (CN 0 c e))" and c1: "c=1" and bn:"numbound0 e" |
1856 ultimately show ?case |
|
1857 by blast |
|
1858 next |
|
1859 case (8 c e) |
|
1860 then have p: "Ifm bbs (x # bs) (Ge (CN 0 c e))" and c1: "c = 1" and bn: "numbound0 e" |
1832 by simp_all |
1861 by simp_all |
1833 let ?e = "Inum (x # bs) e" |
1862 let ?e = "Inum (x # bs) e" |
1834 {assume "(x-d) +?e \<ge> 0" hence ?case using c1 |
1863 { |
1835 numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] |
1864 assume "(x - d) + ?e \<ge> 0" |
1836 by simp} |
1865 then have ?case |
1837 moreover |
1866 using c1 numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] |
1838 {assume H: "\<not> (x-d) + ?e \<ge> 0" |
1867 by simp |
1839 let ?v="Sub (C -1) e" |
1868 } |
1840 have vb: "?v \<in> set (\<beta> (Ge (CN 0 c e)))" by simp |
1869 moreover |
1841 from 8(5)[simplified simp_thms Inum.simps \<beta>.simps set_simps bex_simps numbound0_I[OF bn,where b="a" and b'="x" and bs="bs"]] |
1870 { |
1842 have nob: "\<not> (\<exists>j\<in> {1 ..d}. x = - ?e - 1 + j)" by auto |
1871 assume H: "\<not> (x - d) + ?e \<ge> 0" |
1843 from H p have "x + ?e \<ge> 0 \<and> x + ?e < d" by (simp add: c1) |
1872 let ?v = "Sub (C -1) e" |
1844 hence "x + ?e +1 \<ge> 1 \<and> x + ?e + 1 \<le> d" by simp |
1873 have vb: "?v \<in> set (\<beta> (Ge (CN 0 c e)))" |
1845 hence "\<exists>(j::int) \<in> {1 .. d}. j = x + ?e + 1" by simp |
1874 by simp |
1846 hence "\<exists>(j::int) \<in> {1 .. d}. x= - ?e - 1 + j" by (simp add: algebra_simps) |
1875 from 8(5)[simplified simp_thms Inum.simps \<beta>.simps set_simps bex_simps numbound0_I[OF bn,where b="a" and b'="x" and bs="bs"]] |
1847 with nob have ?case by simp } |
1876 have nob: "\<not> (\<exists>j\<in> {1 ..d}. x = - ?e - 1 + j)" |
1848 ultimately show ?case by blast |
1877 by auto |
1849 next |
1878 from H p have "x + ?e \<ge> 0 \<and> x + ?e < d" |
1850 case (3 c e) hence p: "Ifm bbs (x #bs) (Eq (CN 0 c e))" (is "?p x") and c1: "c=1" and bn:"numbound0 e" by simp_all |
1879 by (simp add: c1) |
1851 let ?e = "Inum (x # bs) e" |
1880 then have "x + ?e +1 \<ge> 1 \<and> x + ?e + 1 \<le> d" |
1852 let ?v="(Sub (C -1) e)" |
1881 by simp |
1853 have vb: "?v \<in> set (\<beta> (Eq (CN 0 c e)))" by simp |
1882 then have "\<exists>(j::int) \<in> {1 .. d}. j = x + ?e + 1" |
1854 from p have "x= - ?e" by (simp add: c1) with 3(5) show ?case using dp |
1883 by simp |
1855 by simp (erule ballE[where x="1"], |
1884 then have "\<exists>(j::int) \<in> {1 .. d}. x= - ?e - 1 + j" |
1856 simp_all add:algebra_simps numbound0_I[OF bn,where b="x"and b'="a"and bs="bs"]) |
1885 by (simp add: algebra_simps) |
1857 next |
1886 with nob have ?case |
1858 case (4 c e)hence p: "Ifm bbs (x #bs) (NEq (CN 0 c e))" (is "?p x") and c1: "c=1" and bn:"numbound0 e" by simp_all |
1887 by simp |
1859 let ?e = "Inum (x # bs) e" |
1888 } |
1860 let ?v="Neg e" |
1889 ultimately show ?case |
1861 have vb: "?v \<in> set (\<beta> (NEq (CN 0 c e)))" by simp |
1890 by blast |
1862 {assume "x - d + Inum (((x -d)) # bs) e \<noteq> 0" |
1891 next |
1863 hence ?case by (simp add: c1)} |
1892 case (3 c e) |
1864 moreover |
1893 then |
1865 {assume H: "x - d + Inum (((x -d)) # bs) e = 0" |
1894 have p: "Ifm bbs (x #bs) (Eq (CN 0 c e))" (is "?p x") |
1866 hence "x = - Inum (((x -d)) # bs) e + d" by simp |
1895 and c1: "c=1" |
1867 hence "x = - Inum (a # bs) e + d" |
1896 and bn: "numbound0 e" |
1868 by (simp add: numbound0_I[OF bn,where b="x - d"and b'="a"and bs="bs"]) |
1897 by simp_all |
1869 with 4(5) have ?case using dp by simp} |
1898 let ?e = "Inum (x # bs) e" |
1870 ultimately show ?case by blast |
1899 let ?v="(Sub (C -1) e)" |
1871 next |
1900 have vb: "?v \<in> set (\<beta> (Eq (CN 0 c e)))" |
1872 case (9 j c e) hence p: "Ifm bbs (x #bs) (Dvd j (CN 0 c e))" (is "?p x") and c1: "c=1" and bn:"numbound0 e" by simp_all |
1901 by simp |
1873 let ?e = "Inum (x # bs) e" |
1902 from p have "x= - ?e" by (simp add: c1) with 3(5) show ?case |
1874 from 9 have id: "j dvd d" by simp |
1903 using dp |
1875 from c1 have "?p x = (j dvd (x+ ?e))" by simp |
1904 by simp (erule ballE[where x="1"], |
1876 also have "\<dots> = (j dvd x - d + ?e)" |
1905 simp_all add:algebra_simps numbound0_I[OF bn,where b="x"and b'="a"and bs="bs"]) |
1877 using zdvd_period[OF id, where x="x" and c="-1" and t="?e"] by simp |
1906 next |
1878 finally show ?case |
1907 case (4 c e) |
1879 using numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] c1 p by simp |
1908 then |
1880 next |
1909 have p: "Ifm bbs (x #bs) (NEq (CN 0 c e))" (is "?p x") |
1881 case (10 j c e) hence p: "Ifm bbs (x #bs) (NDvd j (CN 0 c e))" (is "?p x") and c1: "c=1" and bn:"numbound0 e" by simp_all |
1910 and c1: "c = 1" |
1882 let ?e = "Inum (x # bs) e" |
1911 and bn: "numbound0 e" |
1883 from 10 have id: "j dvd d" by simp |
1912 by simp_all |
1884 from c1 have "?p x = (\<not> j dvd (x+ ?e))" by simp |
1913 let ?e = "Inum (x # bs) e" |
1885 also have "\<dots> = (\<not> j dvd x - d + ?e)" |
1914 let ?v="Neg e" |
1886 using zdvd_period[OF id, where x="x" and c="-1" and t="?e"] by simp |
1915 have vb: "?v \<in> set (\<beta> (NEq (CN 0 c e)))" by simp |
1887 finally show ?case using numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] c1 p by simp |
1916 { |
|
1917 assume "x - d + Inum (((x -d)) # bs) e \<noteq> 0" |
|
1918 then have ?case by (simp add: c1) |
|
1919 } |
|
1920 moreover |
|
1921 { |
|
1922 assume H: "x - d + Inum (((x -d)) # bs) e = 0" |
|
1923 then have "x = - Inum (((x -d)) # bs) e + d" |
|
1924 by simp |
|
1925 then have "x = - Inum (a # bs) e + d" |
|
1926 by (simp add: numbound0_I[OF bn,where b="x - d"and b'="a"and bs="bs"]) |
|
1927 with 4(5) have ?case |
|
1928 using dp by simp |
|
1929 } |
|
1930 ultimately show ?case |
|
1931 by blast |
|
1932 next |
|
1933 case (9 j c e) |
|
1934 then |
|
1935 have p: "Ifm bbs (x # bs) (Dvd j (CN 0 c e))" (is "?p x") |
|
1936 and c1: "c = 1" |
|
1937 and bn: "numbound0 e" |
|
1938 by simp_all |
|
1939 let ?e = "Inum (x # bs) e" |
|
1940 from 9 have id: "j dvd d" |
|
1941 by simp |
|
1942 from c1 have "?p x = (j dvd (x + ?e))" |
|
1943 by simp |
|
1944 also have "\<dots> = (j dvd x - d + ?e)" |
|
1945 using zdvd_period[OF id, where x="x" and c="-1" and t="?e"] |
|
1946 by simp |
|
1947 finally show ?case |
|
1948 using numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] c1 p |
|
1949 by simp |
|
1950 next |
|
1951 case (10 j c e) |
|
1952 then |
|
1953 have p: "Ifm bbs (x #bs) (NDvd j (CN 0 c e))" (is "?p x") |
|
1954 and c1: "c = 1" |
|
1955 and bn: "numbound0 e" |
|
1956 by simp_all |
|
1957 let ?e = "Inum (x # bs) e" |
|
1958 from 10 have id: "j dvd d" |
|
1959 by simp |
|
1960 from c1 have "?p x = (\<not> j dvd (x + ?e))" |
|
1961 by simp |
|
1962 also have "\<dots> = (\<not> j dvd x - d + ?e)" |
|
1963 using zdvd_period[OF id, where x="x" and c="-1" and t="?e"] |
|
1964 by simp |
|
1965 finally show ?case |
|
1966 using numbound0_I[OF bn,where b="(x-d)" and b'="x" and bs="bs"] c1 p |
|
1967 by simp |
1888 qed (auto simp add: numbound0_I[where bs="bs" and b="(x - d)" and b'="x"] gr0_conv_Suc) |
1968 qed (auto simp add: numbound0_I[where bs="bs" and b="(x - d)" and b'="x"] gr0_conv_Suc) |
1889 |
1969 |
1890 lemma \<beta>': |
1970 lemma \<beta>': |
1891 assumes lp: "iszlfm p" |
1971 assumes lp: "iszlfm p" |
1892 and u: "d_\<beta> p 1" |
1972 and u: "d_\<beta> p 1" |
1893 and d: "d_\<delta> p d" |
1973 and d: "d_\<delta> p d" |
1894 and dp: "d > 0" |
1974 and dp: "d > 0" |
1895 shows "\<forall>x. \<not>(\<exists>(j::int) \<in> {1 .. d}. \<exists>b\<in> set(\<beta> p). Ifm bbs ((Inum (a#bs) b + j) #bs) p) \<longrightarrow> Ifm bbs (x#bs) p \<longrightarrow> Ifm bbs ((x - d)#bs) p" (is "\<forall>x. ?b \<longrightarrow> ?P x \<longrightarrow> ?P (x - d)") |
1975 shows "\<forall>x. \<not> (\<exists>(j::int) \<in> {1 .. d}. \<exists>b\<in> set(\<beta> p). Ifm bbs ((Inum (a#bs) b + j) #bs) p) \<longrightarrow> |
1896 proof(clarify) |
1976 Ifm bbs (x#bs) p \<longrightarrow> Ifm bbs ((x - d)#bs) p" (is "\<forall>x. ?b \<longrightarrow> ?P x \<longrightarrow> ?P (x - d)") |
|
1977 proof clarify |
1897 fix x |
1978 fix x |
1898 assume nb:"?b" and px: "?P x" |
1979 assume nb: "?b" |
1899 hence nb2: "\<not>(\<exists>(j::int) \<in> {1 .. d}. \<exists>b\<in> (Inum (a#bs)) ` set(\<beta> p). x = b + j)" |
1980 and px: "?P x" |
|
1981 then have nb2: "\<not>(\<exists>(j::int) \<in> {1 .. d}. \<exists>b\<in> (Inum (a#bs)) ` set(\<beta> p). x = b + j)" |
1900 by auto |
1982 by auto |
1901 from \<beta>[OF lp u d dp nb2 px] show "?P (x -d )" . |
1983 from \<beta>[OF lp u d dp nb2 px] show "?P (x -d )" . |
1902 qed |
1984 qed |
1903 lemma cpmi_eq: "0 < D \<Longrightarrow> (EX z::int. ALL x. x < z --> (P x = P1 x)) |
1985 |
1904 ==> ALL x.~(EX (j::int) : {1..D}. EX (b::int) : B. P(b+j)) --> P (x) --> P (x - D) |
1986 lemma cpmi_eq: |
1905 ==> (ALL (x::int). ALL (k::int). ((P1 x)= (P1 (x-k*D)))) |
1987 "0 < D \<Longrightarrow> (\<exists>z::int. \<forall>x. x < z \<longrightarrow> P x = P1 x) |
1906 ==> (EX (x::int). P(x)) = ((EX (j::int) : {1..D} . (P1(j))) | (EX (j::int) : {1..D}. EX (b::int) : B. P (b+j)))" |
1988 \<Longrightarrow> \<forall>x. \<not>(\<exists>(j::int) \<in> {1..D}. \<exists>(b::int) \<in> B. P (b + j)) \<longrightarrow> P x \<longrightarrow> P (x - D) |
1907 apply(rule iffI) |
1989 \<Longrightarrow> (\<forall>(x::int). \<forall>(k::int). P1 x = (P1 (x - k * D))) |
1908 prefer 2 |
1990 \<Longrightarrow> (\<exists>(x::int). P x) = ((\<exists>(j::int) \<in> {1..D}. P1 j) \<or> (\<exists>(j::int) \<in> {1..D}. \<exists>(b::int) \<in> B. P (b + j)))" |
1909 apply(drule minusinfinity) |
1991 apply(rule iffI) |
1910 apply assumption+ |
1992 prefer 2 |
1911 apply(fastforce) |
1993 apply(drule minusinfinity) |
1912 apply clarsimp |
1994 apply assumption+ |
1913 apply(subgoal_tac "!!k. 0<=k \<Longrightarrow> !x. P x \<longrightarrow> P (x - k*D)") |
1995 apply(fastforce) |
1914 apply(frule_tac x = x and z=z in decr_lemma) |
1996 apply clarsimp |
1915 apply(subgoal_tac "P1(x - (\<bar>x - z\<bar> + 1) * D)") |
1997 apply(subgoal_tac "!!k. 0<=k \<Longrightarrow> !x. P x \<longrightarrow> P (x - k*D)") |
1916 prefer 2 |
1998 apply(frule_tac x = x and z=z in decr_lemma) |
1917 apply(subgoal_tac "0 <= (\<bar>x - z\<bar> + 1)") |
1999 apply(subgoal_tac "P1(x - (\<bar>x - z\<bar> + 1) * D)") |
1918 prefer 2 apply arith |
2000 prefer 2 |
1919 apply fastforce |
2001 apply(subgoal_tac "0 <= (\<bar>x - z\<bar> + 1)") |
1920 apply(drule (1) periodic_finite_ex) |
2002 prefer 2 apply arith |
1921 apply blast |
2003 apply fastforce |
1922 apply(blast dest:decr_mult_lemma) |
2004 apply(drule (1) periodic_finite_ex) |
1923 done |
2005 apply blast |
|
2006 apply(blast dest:decr_mult_lemma) |
|
2007 done |
1924 |
2008 |
1925 theorem cp_thm: |
2009 theorem cp_thm: |
1926 assumes lp: "iszlfm p" |
2010 assumes lp: "iszlfm p" |
1927 and u: "d_\<beta> p 1" |
2011 and u: "d_\<beta> p 1" |
1928 and d: "d_\<delta> p d" |
2012 and d: "d_\<delta> p d" |
1929 and dp: "d > 0" |
2013 and dp: "d > 0" |
1930 shows "(\<exists>(x::int). Ifm bbs (x #bs) p) = (\<exists>j\<in> {1.. d}. Ifm bbs (j #bs) (minusinf p) \<or> (\<exists>b \<in> set (\<beta> p). Ifm bbs ((Inum (i#bs) b + j) #bs) p))" |
2014 shows "(\<exists>(x::int). Ifm bbs (x #bs) p) = (\<exists>j\<in> {1.. d}. Ifm bbs (j #bs) (minusinf p) \<or> (\<exists>b \<in> set (\<beta> p). Ifm bbs ((Inum (i#bs) b + j) #bs) p))" |
1931 (is "(\<exists>(x::int). ?P (x)) = (\<exists>j\<in> ?D. ?M j \<or> (\<exists>b\<in> ?B. ?P (?I b + j)))") |
2015 (is "(\<exists>(x::int). ?P (x)) = (\<exists>j\<in> ?D. ?M j \<or> (\<exists>b\<in> ?B. ?P (?I b + j)))") |
1932 proof- |
2016 proof - |
1933 from minusinf_inf[OF lp u] |
2017 from minusinf_inf[OF lp u] |
1934 have th: "\<exists>(z::int). \<forall>x<z. ?P (x) = ?M x" by blast |
2018 have th: "\<exists>(z::int). \<forall>x<z. ?P (x) = ?M x" |
|
2019 by blast |
1935 let ?B' = "{?I b | b. b\<in> ?B}" |
2020 let ?B' = "{?I b | b. b\<in> ?B}" |
1936 have BB': "(\<exists>j\<in>?D. \<exists>b\<in> ?B. ?P (?I b +j)) = (\<exists>j \<in> ?D. \<exists>b \<in> ?B'. ?P (b + j))" by auto |
2021 have BB': "(\<exists>j\<in>?D. \<exists>b\<in> ?B. ?P (?I b +j)) = (\<exists>j \<in> ?D. \<exists>b \<in> ?B'. ?P (b + j))" |
1937 hence th2: "\<forall>x. \<not> (\<exists>j \<in> ?D. \<exists>b \<in> ?B'. ?P ((b + j))) \<longrightarrow> ?P (x) \<longrightarrow> ?P ((x - d))" |
2022 by auto |
|
2023 then have th2: "\<forall>x. \<not> (\<exists>j \<in> ?D. \<exists>b \<in> ?B'. ?P ((b + j))) \<longrightarrow> ?P (x) \<longrightarrow> ?P ((x - d))" |
1938 using \<beta>'[OF lp u d dp, where a="i" and bbs = "bbs"] by blast |
2024 using \<beta>'[OF lp u d dp, where a="i" and bbs = "bbs"] by blast |
1939 from minusinf_repeats[OF d lp] |
2025 from minusinf_repeats[OF d lp] |
1940 have th3: "\<forall>x k. ?M x = ?M (x-k*d)" by simp |
2026 have th3: "\<forall>x k. ?M x = ?M (x-k*d)" |
1941 from cpmi_eq[OF dp th th2 th3] BB' show ?thesis by blast |
2027 by simp |
|
2028 from cpmi_eq[OF dp th th2 th3] BB' show ?thesis |
|
2029 by blast |
1942 qed |
2030 qed |
1943 |
2031 |
1944 (* Implement the right hand sides of Cooper's theorem and Ferrante and Rackoff. *) |
2032 (* Implement the right hand sides of Cooper's theorem and Ferrante and Rackoff. *) |
1945 lemma mirror_ex: |
2033 lemma mirror_ex: |
1946 assumes lp: "iszlfm p" |
2034 assumes lp: "iszlfm p" |
1947 shows "(\<exists>x. Ifm bbs (x#bs) (mirror p)) = (\<exists>x. Ifm bbs (x#bs) p)" |
2035 shows "(\<exists>x. Ifm bbs (x#bs) (mirror p)) = (\<exists>x. Ifm bbs (x#bs) p)" |
1948 (is "(\<exists>x. ?I x ?mp) = (\<exists>x. ?I x p)") |
2036 (is "(\<exists>x. ?I x ?mp) = (\<exists>x. ?I x p)") |
1949 proof(auto) |
2037 proof(auto) |
1950 fix x assume "?I x ?mp" hence "?I (- x) p" using mirror[OF lp] by blast |
2038 fix x assume "?I x ?mp" then have "?I (- x) p" using mirror[OF lp] by blast |
1951 thus "\<exists>x. ?I x p" by blast |
2039 then show "\<exists>x. ?I x p" by blast |
1952 next |
2040 next |
1953 fix x assume "?I x p" hence "?I (- x) ?mp" |
2041 fix x assume "?I x p" then have "?I (- x) ?mp" |
1954 using mirror[OF lp, where x="- x", symmetric] by auto |
2042 using mirror[OF lp, where x="- x", symmetric] by auto |
1955 thus "\<exists>x. ?I x ?mp" by blast |
2043 then show "\<exists>x. ?I x ?mp" by blast |
1956 qed |
2044 qed |
1957 |
2045 |
1958 |
2046 |
1959 lemma cp_thm': |
2047 lemma cp_thm': |
1960 assumes lp: "iszlfm p" |
2048 assumes lp: "iszlfm p" |