1 (* Title: HOL/Presburger.thy |
1 (* Title: HOL/Presburger.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Amine Chaieb, Tobias Nipkow and Stefan Berghofer, TU Muenchen |
3 Author: Amine Chaieb, TU Muenchen |
4 *) |
4 *) |
5 |
|
6 header {* Presburger Arithmetic: Cooper's Algorithm *} |
|
7 |
5 |
8 theory Presburger |
6 theory Presburger |
9 imports NatSimprocs SetInterval |
7 imports NatSimprocs SetInterval |
10 uses |
8 uses "Tools/Presburger/cooper_data" "Tools/Presburger/qelim" |
11 ("Tools/Presburger/cooper_dec.ML") |
9 "Tools/Presburger/generated_cooper.ML" |
12 ("Tools/Presburger/cooper_proof.ML") |
10 ("Tools/Presburger/cooper.ML") ("Tools/Presburger/presburger.ML") |
13 ("Tools/Presburger/qelim.ML") |
11 |
14 ("Tools/Presburger/reflected_presburger.ML") |
|
15 ("Tools/Presburger/reflected_cooper.ML") |
|
16 ("Tools/Presburger/presburger.ML") |
|
17 begin |
12 begin |
18 |
13 setup {* Cooper_Data.setup*} |
19 text {* Theorem for unitifying the coeffitients of @{text x} in an existential formula*} |
14 |
20 |
15 section{* The @{text "-\<infinity>"} and @{text "+\<infinity>"} Properties *} |
21 theorem unity_coeff_ex: "(\<exists>x::int. P (l * x)) = (\<exists>x. l dvd (1*x+0) \<and> P x)" |
16 |
22 apply (rule iffI) |
17 lemma minf: |
23 apply (erule exE) |
18 "\<lbrakk>\<exists>(z ::'a::linorder).\<forall>x<z. P x = P' x; \<exists>z.\<forall>x<z. Q x = Q' x\<rbrakk> |
24 apply (rule_tac x = "l * x" in exI) |
19 \<Longrightarrow> \<exists>z.\<forall>x<z. (P x \<and> Q x) = (P' x \<and> Q' x)" |
25 apply simp |
20 "\<lbrakk>\<exists>(z ::'a::linorder).\<forall>x<z. P x = P' x; \<exists>z.\<forall>x<z. Q x = Q' x\<rbrakk> |
26 apply (erule exE) |
21 \<Longrightarrow> \<exists>z.\<forall>x<z. (P x \<or> Q x) = (P' x \<or> Q' x)" |
27 apply (erule conjE) |
22 "\<exists>(z ::'a::{linorder}).\<forall>x<z.(x = t) = False" |
28 apply (erule dvdE) |
23 "\<exists>(z ::'a::{linorder}).\<forall>x<z.(x \<noteq> t) = True" |
29 apply (rule_tac x = k in exI) |
24 "\<exists>(z ::'a::{linorder}).\<forall>x<z.(x < t) = True" |
30 apply simp |
25 "\<exists>(z ::'a::{linorder}).\<forall>x<z.(x \<le> t) = True" |
31 done |
26 "\<exists>(z ::'a::{linorder}).\<forall>x<z.(x > t) = False" |
32 |
27 "\<exists>(z ::'a::{linorder}).\<forall>x<z.(x \<ge> t) = False" |
33 lemma uminus_dvd_conv: "(d dvd (t::int)) = (-d dvd t)" |
28 "\<exists>z.\<forall>(x::'a::{linorder,plus,times})<z. (d dvd x + s) = (d dvd x + s)" |
34 apply(unfold dvd_def) |
29 "\<exists>z.\<forall>(x::'a::{linorder,plus,times})<z. (\<not> d dvd x + s) = (\<not> d dvd x + s)" |
35 apply(rule iffI) |
30 "\<exists>z.\<forall>x<z. F = F" |
36 apply(clarsimp) |
31 by ((erule exE, erule exE,rule_tac x="min z za" in exI,simp)+, (rule_tac x="t" in exI,fastsimp)+) simp_all |
37 apply(rename_tac k) |
32 |
38 apply(rule_tac x = "-k" in exI) |
33 lemma pinf: |
39 apply simp |
34 "\<lbrakk>\<exists>(z ::'a::linorder).\<forall>x>z. P x = P' x; \<exists>z.\<forall>x>z. Q x = Q' x\<rbrakk> |
40 apply(clarsimp) |
35 \<Longrightarrow> \<exists>z.\<forall>x>z. (P x \<and> Q x) = (P' x \<and> Q' x)" |
41 apply(rename_tac k) |
36 "\<lbrakk>\<exists>(z ::'a::linorder).\<forall>x>z. P x = P' x; \<exists>z.\<forall>x>z. Q x = Q' x\<rbrakk> |
42 apply(rule_tac x = "-k" in exI) |
37 \<Longrightarrow> \<exists>z.\<forall>x>z. (P x \<or> Q x) = (P' x \<or> Q' x)" |
43 apply simp |
38 "\<exists>(z ::'a::{linorder}).\<forall>x>z.(x = t) = False" |
44 done |
39 "\<exists>(z ::'a::{linorder}).\<forall>x>z.(x \<noteq> t) = True" |
45 |
40 "\<exists>(z ::'a::{linorder}).\<forall>x>z.(x < t) = False" |
46 lemma uminus_dvd_conv': "(d dvd (t::int)) = (d dvd -t)" |
41 "\<exists>(z ::'a::{linorder}).\<forall>x>z.(x \<le> t) = False" |
47 apply(unfold dvd_def) |
42 "\<exists>(z ::'a::{linorder}).\<forall>x>z.(x > t) = True" |
48 apply(rule iffI) |
43 "\<exists>(z ::'a::{linorder}).\<forall>x>z.(x \<ge> t) = True" |
49 apply(clarsimp) |
44 "\<exists>z.\<forall>(x::'a::{linorder,plus,times})>z. (d dvd x + s) = (d dvd x + s)" |
50 apply(rule_tac x = "-k" in exI) |
45 "\<exists>z.\<forall>(x::'a::{linorder,plus,times})>z. (\<not> d dvd x + s) = (\<not> d dvd x + s)" |
51 apply simp |
46 "\<exists>z.\<forall>x>z. F = F" |
52 apply(clarsimp) |
47 by ((erule exE, erule exE,rule_tac x="max z za" in exI,simp)+,(rule_tac x="t" in exI,fastsimp)+) simp_all |
53 apply(rule_tac x = "-k" in exI) |
48 |
54 apply simp |
49 lemma inf_period: |
55 done |
50 "\<lbrakk>\<forall>x k. P x = P (x - k*D); \<forall>x k. Q x = Q (x - k*D)\<rbrakk> |
56 |
51 \<Longrightarrow> \<forall>x k. (P x \<and> Q x) = (P (x - k*D) \<and> Q (x - k*D))" |
57 |
52 "\<lbrakk>\<forall>x k. P x = P (x - k*D); \<forall>x k. Q x = Q (x - k*D)\<rbrakk> |
58 |
53 \<Longrightarrow> \<forall>x k. (P x \<or> Q x) = (P (x - k*D) \<or> Q (x - k*D))" |
59 text {*Theorems for the combination of proofs of the equality of @{text P} and @{text P_m} for integers @{text x} less than some integer @{text z}.*} |
54 "(d::'a::{comm_ring}) dvd D \<Longrightarrow> \<forall>x k. (d dvd x + t) = (d dvd (x - k*D) + t)" |
60 |
55 "(d::'a::{comm_ring}) dvd D \<Longrightarrow> \<forall>x k. (\<not>d dvd x + t) = (\<not>d dvd (x - k*D) + t)" |
61 theorem eq_minf_conjI: "\<exists>z1::int. \<forall>x. x < z1 \<longrightarrow> (A1 x = A2 x) \<Longrightarrow> |
56 "\<forall>x k. F = F" |
62 \<exists>z2::int. \<forall>x. x < z2 \<longrightarrow> (B1 x = B2 x) \<Longrightarrow> |
57 by simp_all |
63 \<exists>z::int. \<forall>x. x < z \<longrightarrow> ((A1 x \<and> B1 x) = (A2 x \<and> B2 x))" |
58 (clarsimp simp add: dvd_def, rule iffI, clarsimp,rule_tac x = "kb - ka*k" in exI, |
64 apply (erule exE)+ |
59 simp add: ring_eq_simps, clarsimp,rule_tac x = "kb + ka*k" in exI,simp add: ring_eq_simps)+ |
65 apply (rule_tac x = "min z1 z2" in exI) |
60 |
66 apply simp |
61 section{* The A and B sets *} |
67 done |
62 lemma bset: |
68 |
63 "\<lbrakk>\<forall>x.(\<forall>j \<in> {1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> P x \<longrightarrow> P(x - D) ; |
69 |
64 \<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> Q x \<longrightarrow> Q(x - D)\<rbrakk> \<Longrightarrow> |
70 theorem eq_minf_disjI: "\<exists>z1::int. \<forall>x. x < z1 \<longrightarrow> (A1 x = A2 x) \<Longrightarrow> |
65 \<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j) \<longrightarrow> (P x \<and> Q x) \<longrightarrow> (P(x - D) \<and> Q (x - D))" |
71 \<exists>z2::int. \<forall>x. x < z2 \<longrightarrow> (B1 x = B2 x) \<Longrightarrow> |
66 "\<lbrakk>\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> P x \<longrightarrow> P(x - D) ; |
72 \<exists>z::int. \<forall>x. x < z \<longrightarrow> ((A1 x \<or> B1 x) = (A2 x \<or> B2 x))" |
67 \<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> Q x \<longrightarrow> Q(x - D)\<rbrakk> \<Longrightarrow> |
73 |
68 \<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (P x \<or> Q x) \<longrightarrow> (P(x - D) \<or> Q (x - D))" |
74 apply (erule exE)+ |
69 "\<lbrakk>D>0; t - 1\<in> B\<rbrakk> \<Longrightarrow> (\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (x = t) \<longrightarrow> (x - D = t))" |
75 apply (rule_tac x = "min z1 z2" in exI) |
70 "\<lbrakk>D>0 ; t \<in> B\<rbrakk> \<Longrightarrow>(\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (x \<noteq> t) \<longrightarrow> (x - D \<noteq> t))" |
76 apply simp |
71 "D>0 \<Longrightarrow> (\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (x < t) \<longrightarrow> (x - D < t))" |
77 done |
72 "D>0 \<Longrightarrow> (\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (x \<le> t) \<longrightarrow> (x - D \<le> t))" |
78 |
73 "\<lbrakk>D>0 ; t \<in> B\<rbrakk> \<Longrightarrow>(\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (x > t) \<longrightarrow> (x - D > t))" |
79 |
74 "\<lbrakk>D>0 ; t - 1 \<in> B\<rbrakk> \<Longrightarrow>(\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (x \<ge> t) \<longrightarrow> (x - D \<ge> t))" |
80 text {*Theorems for the combination of proofs of the equality of @{text P} and @{text P_m} for integers @{text x} greather than some integer @{text z}.*} |
75 "d dvd D \<Longrightarrow>(\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (d dvd x+t) \<longrightarrow> (d dvd (x - D) + t))" |
81 |
76 "d dvd D \<Longrightarrow>(\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (\<not>d dvd x+t) \<longrightarrow> (\<not> d dvd (x - D) + t))" |
82 theorem eq_pinf_conjI: "\<exists>z1::int. \<forall>x. z1 < x \<longrightarrow> (A1 x = A2 x) \<Longrightarrow> |
77 "\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j) \<longrightarrow> F \<longrightarrow> F" |
83 \<exists>z2::int. \<forall>x. z2 < x \<longrightarrow> (B1 x = B2 x) \<Longrightarrow> |
78 proof (blast, blast) |
84 \<exists>z::int. \<forall>x. z < x \<longrightarrow> ((A1 x \<and> B1 x) = (A2 x \<and> B2 x))" |
79 assume dp: "D > 0" and tB: "t - 1\<in> B" |
85 apply (erule exE)+ |
80 show "(\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (x = t) \<longrightarrow> (x - D = t))" |
86 apply (rule_tac x = "max z1 z2" in exI) |
81 apply (rule allI, rule impI,erule ballE[where x="1"],erule ballE[where x="t - 1"]) |
87 apply simp |
82 using dp tB by simp_all |
88 done |
83 next |
89 |
84 assume dp: "D > 0" and tB: "t \<in> B" |
90 |
85 show "(\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (x \<noteq> t) \<longrightarrow> (x - D \<noteq> t))" |
91 theorem eq_pinf_disjI: "\<exists>z1::int. \<forall>x. z1 < x \<longrightarrow> (A1 x = A2 x) \<Longrightarrow> |
86 apply (rule allI, rule impI,erule ballE[where x="D"],erule ballE[where x="t"]) |
92 \<exists>z2::int. \<forall>x. z2 < x \<longrightarrow> (B1 x = B2 x) \<Longrightarrow> |
87 using dp tB by simp_all |
93 \<exists>z::int. \<forall>x. z < x \<longrightarrow> ((A1 x \<or> B1 x) = (A2 x \<or> B2 x))" |
88 next |
94 apply (erule exE)+ |
89 assume dp: "D > 0" thus "(\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (x < t) \<longrightarrow> (x - D < t))" by arith |
95 apply (rule_tac x = "max z1 z2" in exI) |
90 next |
96 apply simp |
91 assume dp: "D > 0" thus "\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (x \<le> t) \<longrightarrow> (x - D \<le> t)" by arith |
97 done |
92 next |
98 |
93 assume dp: "D > 0" and tB:"t \<in> B" |
99 text {* |
94 {fix x assume nob: "\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j" and g: "x > t" and ng: "\<not> (x - D) > t" |
100 \medskip Theorems for the combination of proofs of the modulo @{text |
95 hence "x -t \<le> D" and "1 \<le> x - t" by simp+ |
101 D} property for @{text "P plusinfinity"} |
96 hence "\<exists>j \<in> {1 .. D}. x - t = j" by auto |
102 |
97 hence "\<exists>j \<in> {1 .. D}. x = t + j" by (simp add: ring_eq_simps) |
103 FIXME: This is THE SAME theorem as for the @{text minusinf} version, |
98 with nob tB have "False" by simp} |
104 but with @{text "+k.."} instead of @{text "-k.."} In the future |
99 thus "\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (x > t) \<longrightarrow> (x - D > t)" by blast |
105 replace these both with only one. *} |
100 next |
106 |
101 assume dp: "D > 0" and tB:"t - 1\<in> B" |
107 theorem modd_pinf_conjI: "\<forall>(x::int) k. A x = A (x+k*d) \<Longrightarrow> |
102 {fix x assume nob: "\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j" and g: "x \<ge> t" and ng: "\<not> (x - D) \<ge> t" |
108 \<forall>(x::int) k. B x = B (x+k*d) \<Longrightarrow> |
103 hence "x - (t - 1) \<le> D" and "1 \<le> x - (t - 1)" by simp+ |
109 \<forall>(x::int) (k::int). (A x \<and> B x) = (A (x+k*d) \<and> B (x+k*d))" |
104 hence "\<exists>j \<in> {1 .. D}. x - (t - 1) = j" by auto |
110 by simp |
105 hence "\<exists>j \<in> {1 .. D}. x = (t - 1) + j" by (simp add: ring_eq_simps) |
111 |
106 with nob tB have "False" by simp} |
112 theorem modd_pinf_disjI: "\<forall>(x::int) k. A x = A (x+k*d) \<Longrightarrow> |
107 thus "\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (x \<ge> t) \<longrightarrow> (x - D \<ge> t)" by blast |
113 \<forall>(x::int) k. B x = B (x+k*d) \<Longrightarrow> |
108 next |
114 \<forall>(x::int) (k::int). (A x \<or> B x) = (A (x+k*d) \<or> B (x+k*d))" |
109 assume d: "d dvd D" |
115 by simp |
110 {fix x assume H: "d dvd x + t" with d have "d dvd (x - D) + t" |
116 |
111 by (clarsimp simp add: dvd_def,rule_tac x= "ka - k" in exI,simp add: ring_eq_simps)} |
117 text {* |
112 thus "\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (d dvd x+t) \<longrightarrow> (d dvd (x - D) + t)" by simp |
118 This is one of the cases where the simplifed formula is prooved to |
113 next |
119 habe some property (in relation to @{text P_m}) but we need to prove |
114 assume d: "d dvd D" |
120 the property for the original formula (@{text P_m}) |
115 {fix x assume H: "\<not>(d dvd x + t)" with d have "\<not>d dvd (x - D) + t" |
121 |
116 by (clarsimp simp add: dvd_def,erule_tac x= "ka + k" in allE,simp add: ring_eq_simps)} |
122 FIXME: This is exaclty the same thm as for @{text minusinf}. *} |
117 thus "\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (\<not>d dvd x+t) \<longrightarrow> (\<not>d dvd (x - D) + t)" by auto |
123 |
118 qed blast |
124 lemma pinf_simp_eq: "ALL x. P(x) = Q(x) ==> (EX (x::int). P(x)) --> (EX (x::int). F(x)) ==> (EX (x::int). Q(x)) --> (EX (x::int). F(x)) " |
119 |
125 by blast |
120 lemma aset: |
126 |
121 "\<lbrakk>\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> P x \<longrightarrow> P(x + D) ; |
127 |
122 \<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> Q x \<longrightarrow> Q(x + D)\<rbrakk> \<Longrightarrow> |
128 text {* |
123 \<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j) \<longrightarrow> (P x \<and> Q x) \<longrightarrow> (P(x + D) \<and> Q (x + D))" |
129 \medskip Theorems for the combination of proofs of the modulo @{text D} |
124 "\<lbrakk>\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> P x \<longrightarrow> P(x + D) ; |
130 property for @{text "P minusinfinity"} *} |
125 \<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> Q x \<longrightarrow> Q(x + D)\<rbrakk> \<Longrightarrow> |
131 |
126 \<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> (P x \<or> Q x) \<longrightarrow> (P(x + D) \<or> Q (x + D))" |
132 theorem modd_minf_conjI: "\<forall>(x::int) k. A x = A (x-k*d) \<Longrightarrow> |
127 "\<lbrakk>D>0; t + 1\<in> A\<rbrakk> \<Longrightarrow> (\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> (x = t) \<longrightarrow> (x + D = t))" |
133 \<forall>(x::int) k. B x = B (x-k*d) \<Longrightarrow> |
128 "\<lbrakk>D>0 ; t \<in> A\<rbrakk> \<Longrightarrow>(\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> (x \<noteq> t) \<longrightarrow> (x + D \<noteq> t))" |
134 \<forall>(x::int) (k::int). (A x \<and> B x) = (A (x-k*d) \<and> B (x-k*d))" |
129 "\<lbrakk>D>0; t\<in> A\<rbrakk> \<Longrightarrow>(\<forall>(x::int). (\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> (x < t) \<longrightarrow> (x + D < t))" |
135 by simp |
130 "\<lbrakk>D>0; t + 1 \<in> A\<rbrakk> \<Longrightarrow> (\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> (x \<le> t) \<longrightarrow> (x + D \<le> t))" |
136 |
131 "D>0 \<Longrightarrow>(\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> (x > t) \<longrightarrow> (x + D > t))" |
137 theorem modd_minf_disjI: "\<forall>(x::int) k. A x = A (x-k*d) \<Longrightarrow> |
132 "D>0 \<Longrightarrow>(\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> (x \<ge> t) \<longrightarrow> (x + D \<ge> t))" |
138 \<forall>(x::int) k. B x = B (x-k*d) \<Longrightarrow> |
133 "d dvd D \<Longrightarrow>(\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> (d dvd x+t) \<longrightarrow> (d dvd (x + D) + t))" |
139 \<forall>(x::int) (k::int). (A x \<or> B x) = (A (x-k*d) \<or> B (x-k*d))" |
134 "d dvd D \<Longrightarrow>(\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> (\<not>d dvd x+t) \<longrightarrow> (\<not> d dvd (x + D) + t))" |
140 by simp |
135 "\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j) \<longrightarrow> F \<longrightarrow> F" |
141 |
136 proof (blast, blast) |
142 text {* |
137 assume dp: "D > 0" and tA: "t + 1 \<in> A" |
143 This is one of the cases where the simplifed formula is prooved to |
138 show "(\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> (x = t) \<longrightarrow> (x + D = t))" |
144 have some property (in relation to @{text P_m}) but we need to |
139 apply (rule allI, rule impI,erule ballE[where x="1"],erule ballE[where x="t + 1"]) |
145 prove the property for the original formula (@{text P_m}). *} |
140 using dp tA by simp_all |
146 |
141 next |
147 lemma minf_simp_eq: "ALL x. P(x) = Q(x) ==> (EX (x::int). P(x)) --> (EX (x::int). F(x)) ==> (EX (x::int). Q(x)) --> (EX (x::int). F(x)) " |
142 assume dp: "D > 0" and tA: "t \<in> A" |
148 by blast |
143 show "(\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> (x \<noteq> t) \<longrightarrow> (x + D \<noteq> t))" |
149 |
144 apply (rule allI, rule impI,erule ballE[where x="D"],erule ballE[where x="t"]) |
150 text {* |
145 using dp tA by simp_all |
151 Theorem needed for proving at runtime divide properties using the |
146 next |
152 arithmetic tactic (which knows only about modulo = 0). *} |
147 assume dp: "D > 0" thus "(\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> (x > t) \<longrightarrow> (x + D > t))" by arith |
153 |
148 next |
154 lemma zdvd_iff_zmod_eq_0: "(m dvd n) = (n mod m = (0::int))" |
149 assume dp: "D > 0" thus "\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> (x \<ge> t) \<longrightarrow> (x + D \<ge> t)" by arith |
155 by(simp add:dvd_def zmod_eq_0_iff) |
150 next |
156 |
151 assume dp: "D > 0" and tA:"t \<in> A" |
157 text {* |
152 {fix x assume nob: "\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j" and g: "x < t" and ng: "\<not> (x + D) < t" |
158 \medskip Theorems used for the combination of proof for the |
153 hence "t - x \<le> D" and "1 \<le> t - x" by simp+ |
159 backwards direction of Cooper's Theorem. They rely exclusively on |
154 hence "\<exists>j \<in> {1 .. D}. t - x = j" by auto |
160 Predicate calculus.*} |
155 hence "\<exists>j \<in> {1 .. D}. x = t - j" by (auto simp add: ring_eq_simps) |
161 |
156 with nob tA have "False" by simp} |
162 lemma not_ast_p_disjI: "(ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a - j)) --> P1(x) --> P1(x + d)) |
157 thus "\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> (x < t) \<longrightarrow> (x + D < t)" by blast |
163 ==> |
158 next |
164 (ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a - j)) --> P2(x) --> P2(x + d)) |
159 assume dp: "D > 0" and tA:"t + 1\<in> A" |
165 ==> |
160 {fix x assume nob: "\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j" and g: "x \<le> t" and ng: "\<not> (x + D) \<le> t" |
166 (ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a - j)) -->(P1(x) \<or> P2(x)) --> (P1(x + d) \<or> P2(x + d))) " |
161 hence "(t + 1) - x \<le> D" and "1 \<le> (t + 1) - x" by (simp_all add: ring_eq_simps) |
167 by blast |
162 hence "\<exists>j \<in> {1 .. D}. (t + 1) - x = j" by auto |
168 |
163 hence "\<exists>j \<in> {1 .. D}. x = (t + 1) - j" by (auto simp add: ring_eq_simps) |
169 |
164 with nob tA have "False" by simp} |
170 lemma not_ast_p_conjI: "(ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a- j)) --> P1(x) --> P1(x + d)) |
165 thus "\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> (x \<le> t) \<longrightarrow> (x + D \<le> t)" by blast |
171 ==> |
166 next |
172 (ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a - j)) --> P2(x) --> P2(x + d)) |
167 assume d: "d dvd D" |
173 ==> |
168 {fix x assume H: "d dvd x + t" with d have "d dvd (x + D) + t" |
174 (ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a - j)) -->(P1(x) \<and> P2(x)) --> (P1(x + d) |
169 by (clarsimp simp add: dvd_def,rule_tac x= "ka + k" in exI,simp add: ring_eq_simps)} |
175 \<and> P2(x + d))) " |
170 thus "\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> (d dvd x+t) \<longrightarrow> (d dvd (x + D) + t)" by simp |
176 by blast |
171 next |
177 |
172 assume d: "d dvd D" |
178 lemma not_ast_p_Q_elim: " |
173 {fix x assume H: "\<not>(d dvd x + t)" with d have "\<not>d dvd (x + D) + t" |
179 (ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a - j)) -->P(x) --> P(x + d)) |
174 by (clarsimp simp add: dvd_def,erule_tac x= "ka - k" in allE,simp add: ring_eq_simps)} |
180 ==> ( P = Q ) |
175 thus "\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> (\<not>d dvd x+t) \<longrightarrow> (\<not>d dvd (x + D) + t)" by auto |
181 ==> (ALL x. ~(EX (j::int) : {1..d}. EX (a::int) : A. P(a - j)) -->P(x) --> P(x + d))" |
176 qed blast |
182 by blast |
177 |
183 |
178 section{* Cooper's Theorem @{text "-\<infinity>"} and @{text "+\<infinity>"} Version *} |
184 text {* |
179 |
185 \medskip Theorems used for the combination of proof for the |
180 subsection{* First some trivial facts about periodic sets or predicates *} |
186 backwards direction of Cooper's Theorem. They rely exclusively on |
181 lemma periodic_finite_ex: |
187 Predicate calculus.*} |
|
188 |
|
189 lemma not_bst_p_disjI: "(ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (b::int) : B. Q(b+j)) --> P1(x) --> P1(x - d)) |
|
190 ==> |
|
191 (ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (b::int) : B. Q(b+j)) --> P2(x) --> P2(x - d)) |
|
192 ==> |
|
193 (ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (b::int) : B. Q(b+j)) -->(P1(x) \<or> P2(x)) --> (P1(x - d) |
|
194 \<or> P2(x-d))) " |
|
195 by blast |
|
196 |
|
197 lemma not_bst_p_conjI: "(ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (b::int) : B. Q(b+j)) --> P1(x) --> P1(x - d)) |
|
198 ==> |
|
199 (ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (b::int) : B. Q(b+j)) --> P2(x) --> P2(x - d)) |
|
200 ==> |
|
201 (ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (b::int) : B. Q(b+j)) -->(P1(x) \<and> P2(x)) --> (P1(x - d) |
|
202 \<and> P2(x-d))) " |
|
203 by blast |
|
204 |
|
205 lemma not_bst_p_Q_elim: " |
|
206 (ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (b::int) : B. Q(b+j)) -->P(x) --> P(x - d)) |
|
207 ==> ( P = Q ) |
|
208 ==> (ALL x. ~(EX (j::int) : {1..d}. EX (b::int) : B. P(b+j)) -->P(x) --> P(x - d))" |
|
209 by blast |
|
210 |
|
211 text {* \medskip This is the first direction of Cooper's Theorem. *} |
|
212 lemma cooper_thm: "(R --> (EX x::int. P x)) ==> (Q -->(EX x::int. P x )) ==> ((R|Q) --> (EX x::int. P x )) " |
|
213 by blast |
|
214 |
|
215 text {* |
|
216 \medskip The full Cooper's Theorem in its equivalence Form. Given |
|
217 the premises it is trivial too, it relies exclusively on prediacte calculus.*} |
|
218 lemma cooper_eq_thm: "(R --> (EX x::int. P x)) ==> (Q -->(EX x::int. P x )) ==> ((~Q) |
|
219 --> (EX x::int. P x ) --> R) ==> (EX x::int. P x) = R|Q " |
|
220 by blast |
|
221 |
|
222 text {* |
|
223 \medskip Some of the atomic theorems generated each time the atom |
|
224 does not depend on @{text x}, they are trivial.*} |
|
225 |
|
226 lemma fm_eq_minf: "EX z::int. ALL x. x < z --> (P = P) " |
|
227 by blast |
|
228 |
|
229 lemma fm_modd_minf: "ALL (x::int). ALL (k::int). (P = P)" |
|
230 by blast |
|
231 |
|
232 lemma not_bst_p_fm: "ALL (x::int). Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (b::int) : B. Q(b+j)) --> fm --> fm" |
|
233 by blast |
|
234 |
|
235 lemma fm_eq_pinf: "EX z::int. ALL x. z < x --> (P = P) " |
|
236 by blast |
|
237 |
|
238 text {* The next two thms are the same as the @{text minusinf} version. *} |
|
239 |
|
240 lemma fm_modd_pinf: "ALL (x::int). ALL (k::int). (P = P)" |
|
241 by blast |
|
242 |
|
243 lemma not_ast_p_fm: "ALL (x::int). Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a - j)) --> fm --> fm" |
|
244 by blast |
|
245 |
|
246 text {* Theorems to be deleted from simpset when proving simplified formulaes. *} |
|
247 |
|
248 lemma P_eqtrue: "(P=True) = P" |
|
249 by iprover |
|
250 |
|
251 lemma P_eqfalse: "(P=False) = (~P)" |
|
252 by iprover |
|
253 |
|
254 text {* |
|
255 \medskip Theorems for the generation of the bachwards direction of |
|
256 Cooper's Theorem. |
|
257 |
|
258 These are the 6 interesting atomic cases which have to be proved relying on the |
|
259 properties of B-set and the arithmetic and contradiction proofs. *} |
|
260 |
|
261 lemma not_bst_p_lt: "0 < (d::int) ==> |
|
262 ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (b::int) : B. Q(b+j)) --> ( 0 < -x + a) --> (0 < -(x - d) + a )" |
|
263 by arith |
|
264 |
|
265 lemma not_bst_p_gt: "\<lbrakk> (g::int) \<in> B; g = -a \<rbrakk> \<Longrightarrow> |
|
266 ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (b::int) : B. Q(b+j)) --> (0 < (x) + a) --> ( 0 < (x - d) + a)" |
|
267 apply clarsimp |
|
268 apply(rule ccontr) |
|
269 apply(drule_tac x = "x+a" in bspec) |
|
270 apply(simp add:atLeastAtMost_iff) |
|
271 apply(drule_tac x = "-a" in bspec) |
|
272 apply assumption |
|
273 apply(simp) |
|
274 done |
|
275 |
|
276 lemma not_bst_p_eq: "\<lbrakk> 0 < d; (g::int) \<in> B; g = -a - 1 \<rbrakk> \<Longrightarrow> |
|
277 ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (b::int) : B. Q(b+j)) --> (0 = x + a) --> (0 = (x - d) + a )" |
|
278 apply clarsimp |
|
279 apply(subgoal_tac "x = -a") |
|
280 prefer 2 apply arith |
|
281 apply(drule_tac x = "1" in bspec) |
|
282 apply(simp add:atLeastAtMost_iff) |
|
283 apply(drule_tac x = "-a- 1" in bspec) |
|
284 apply assumption |
|
285 apply(simp) |
|
286 done |
|
287 |
|
288 |
|
289 lemma not_bst_p_ne: "\<lbrakk> 0 < d; (g::int) \<in> B; g = -a \<rbrakk> \<Longrightarrow> |
|
290 ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (b::int) : B. Q(b+j)) --> ~(0 = x + a) --> ~(0 = (x - d) + a)" |
|
291 apply clarsimp |
|
292 apply(subgoal_tac "x = -a+d") |
|
293 prefer 2 apply arith |
|
294 apply(drule_tac x = "d" in bspec) |
|
295 apply(simp add:atLeastAtMost_iff) |
|
296 apply(drule_tac x = "-a" in bspec) |
|
297 apply assumption |
|
298 apply(simp) |
|
299 done |
|
300 |
|
301 |
|
302 lemma not_bst_p_dvd: "(d1::int) dvd d ==> |
|
303 ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (b::int) : B. Q(b+j)) --> d1 dvd (x + a) --> d1 dvd ((x - d) + a )" |
|
304 apply(clarsimp simp add:dvd_def) |
|
305 apply(rename_tac m) |
|
306 apply(rule_tac x = "m - k" in exI) |
|
307 apply(simp add:int_distrib) |
|
308 done |
|
309 |
|
310 lemma not_bst_p_ndvd: "(d1::int) dvd d ==> |
|
311 ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (b::int) : B. Q(b+j)) --> ~(d1 dvd (x + a)) --> ~(d1 dvd ((x - d) + a ))" |
|
312 apply(clarsimp simp add:dvd_def) |
|
313 apply(rename_tac m) |
|
314 apply(erule_tac x = "m + k" in allE) |
|
315 apply(simp add:int_distrib) |
|
316 done |
|
317 |
|
318 text {* |
|
319 \medskip Theorems for the generation of the bachwards direction of |
|
320 Cooper's Theorem. |
|
321 |
|
322 These are the 6 interesting atomic cases which have to be proved |
|
323 relying on the properties of A-set ant the arithmetic and |
|
324 contradiction proofs. *} |
|
325 |
|
326 lemma not_ast_p_gt: "0 < (d::int) ==> |
|
327 ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a - j)) --> ( 0 < x + t) --> (0 < (x + d) + t )" |
|
328 by arith |
|
329 |
|
330 lemma not_ast_p_lt: "\<lbrakk>0 < d ;(t::int) \<in> A \<rbrakk> \<Longrightarrow> |
|
331 ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a - j)) --> (0 < -x + t) --> ( 0 < -(x + d) + t)" |
|
332 apply clarsimp |
|
333 apply (rule ccontr) |
|
334 apply (drule_tac x = "t-x" in bspec) |
|
335 apply simp |
|
336 apply (drule_tac x = "t" in bspec) |
|
337 apply assumption |
|
338 apply simp |
|
339 done |
|
340 |
|
341 lemma not_ast_p_eq: "\<lbrakk> 0 < d; (g::int) \<in> A; g = -t + 1 \<rbrakk> \<Longrightarrow> |
|
342 ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a - j)) --> (0 = x + t) --> (0 = (x + d) + t )" |
|
343 apply clarsimp |
|
344 apply (drule_tac x="1" in bspec) |
|
345 apply simp |
|
346 apply (drule_tac x="- t + 1" in bspec) |
|
347 apply assumption |
|
348 apply(subgoal_tac "x = -t") |
|
349 prefer 2 apply arith |
|
350 apply simp |
|
351 done |
|
352 |
|
353 lemma not_ast_p_ne: "\<lbrakk> 0 < d; (g::int) \<in> A; g = -t \<rbrakk> \<Longrightarrow> |
|
354 ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a - j)) --> ~(0 = x + t) --> ~(0 = (x + d) + t)" |
|
355 apply clarsimp |
|
356 apply (subgoal_tac "x = -t-d") |
|
357 prefer 2 apply arith |
|
358 apply (drule_tac x = "d" in bspec) |
|
359 apply simp |
|
360 apply (drule_tac x = "-t" in bspec) |
|
361 apply assumption |
|
362 apply simp |
|
363 done |
|
364 |
|
365 lemma not_ast_p_dvd: "(d1::int) dvd d ==> |
|
366 ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a - j)) --> d1 dvd (x + t) --> d1 dvd ((x + d) + t )" |
|
367 apply(clarsimp simp add:dvd_def) |
|
368 apply(rename_tac m) |
|
369 apply(rule_tac x = "m + k" in exI) |
|
370 apply(simp add:int_distrib) |
|
371 done |
|
372 |
|
373 lemma not_ast_p_ndvd: "(d1::int) dvd d ==> |
|
374 ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a - j)) --> ~(d1 dvd (x + t)) --> ~(d1 dvd ((x + d) + t ))" |
|
375 apply(clarsimp simp add:dvd_def) |
|
376 apply(rename_tac m) |
|
377 apply(erule_tac x = "m - k" in allE) |
|
378 apply(simp add:int_distrib) |
|
379 done |
|
380 |
|
381 text {* |
|
382 \medskip These are the atomic cases for the proof generation for the |
|
383 modulo @{text D} property for @{text "P plusinfinity"} |
|
384 |
|
385 They are fully based on arithmetics. *} |
|
386 |
|
387 lemma dvd_modd_pinf: "((d::int) dvd d1) ==> |
|
388 (ALL (x::int). ALL (k::int). (((d::int) dvd (x + t)) = (d dvd (x+k*d1 + t))))" |
|
389 apply(clarsimp simp add:dvd_def) |
|
390 apply(rule iffI) |
|
391 apply(clarsimp) |
|
392 apply(rename_tac n m) |
|
393 apply(rule_tac x = "m + n*k" in exI) |
|
394 apply(simp add:int_distrib) |
|
395 apply(clarsimp) |
|
396 apply(rename_tac n m) |
|
397 apply(rule_tac x = "m - n*k" in exI) |
|
398 apply(simp add:int_distrib mult_ac) |
|
399 done |
|
400 |
|
401 lemma not_dvd_modd_pinf: "((d::int) dvd d1) ==> |
|
402 (ALL (x::int). ALL k. (~((d::int) dvd (x + t))) = (~(d dvd (x+k*d1 + t))))" |
|
403 apply(clarsimp simp add:dvd_def) |
|
404 apply(rule iffI) |
|
405 apply(clarsimp) |
|
406 apply(rename_tac n m) |
|
407 apply(erule_tac x = "m - n*k" in allE) |
|
408 apply(simp add:int_distrib mult_ac) |
|
409 apply(clarsimp) |
|
410 apply(rename_tac n m) |
|
411 apply(erule_tac x = "m + n*k" in allE) |
|
412 apply(simp add:int_distrib mult_ac) |
|
413 done |
|
414 |
|
415 text {* |
|
416 \medskip These are the atomic cases for the proof generation for the |
|
417 equivalence of @{text P} and @{text "P plusinfinity"} for integers |
|
418 @{text x} greater than some integer @{text z}. |
|
419 |
|
420 They are fully based on arithmetics. *} |
|
421 |
|
422 lemma eq_eq_pinf: "EX z::int. ALL x. z < x --> (( 0 = x +t ) = False )" |
|
423 apply(rule_tac x = "-t" in exI) |
|
424 apply simp |
|
425 done |
|
426 |
|
427 lemma neq_eq_pinf: "EX z::int. ALL x. z < x --> ((~( 0 = x +t )) = True )" |
|
428 apply(rule_tac x = "-t" in exI) |
|
429 apply simp |
|
430 done |
|
431 |
|
432 lemma le_eq_pinf: "EX z::int. ALL x. z < x --> ( 0 < x +t = True )" |
|
433 apply(rule_tac x = "-t" in exI) |
|
434 apply simp |
|
435 done |
|
436 |
|
437 lemma len_eq_pinf: "EX z::int. ALL x. z < x --> (0 < -x +t = False )" |
|
438 apply(rule_tac x = "t" in exI) |
|
439 apply simp |
|
440 done |
|
441 |
|
442 lemma dvd_eq_pinf: "EX z::int. ALL x. z < x --> ((d dvd (x + t)) = (d dvd (x + t))) " |
|
443 by simp |
|
444 |
|
445 lemma not_dvd_eq_pinf: "EX z::int. ALL x. z < x --> ((~(d dvd (x + t))) = (~(d dvd (x + t)))) " |
|
446 by simp |
|
447 |
|
448 text {* |
|
449 \medskip These are the atomic cases for the proof generation for the |
|
450 modulo @{text D} property for @{text "P minusinfinity"}. |
|
451 |
|
452 They are fully based on arithmetics. *} |
|
453 |
|
454 lemma dvd_modd_minf: "((d::int) dvd d1) ==> |
|
455 (ALL (x::int). ALL (k::int). (((d::int) dvd (x + t)) = (d dvd (x-k*d1 + t))))" |
|
456 apply(clarsimp simp add:dvd_def) |
|
457 apply(rule iffI) |
|
458 apply(clarsimp) |
|
459 apply(rename_tac n m) |
|
460 apply(rule_tac x = "m - n*k" in exI) |
|
461 apply(simp add:int_distrib) |
|
462 apply(clarsimp) |
|
463 apply(rename_tac n m) |
|
464 apply(rule_tac x = "m + n*k" in exI) |
|
465 apply(simp add:int_distrib mult_ac) |
|
466 done |
|
467 |
|
468 |
|
469 lemma not_dvd_modd_minf: "((d::int) dvd d1) ==> |
|
470 (ALL (x::int). ALL k. (~((d::int) dvd (x + t))) = (~(d dvd (x-k*d1 + t))))" |
|
471 apply(clarsimp simp add:dvd_def) |
|
472 apply(rule iffI) |
|
473 apply(clarsimp) |
|
474 apply(rename_tac n m) |
|
475 apply(erule_tac x = "m + n*k" in allE) |
|
476 apply(simp add:int_distrib mult_ac) |
|
477 apply(clarsimp) |
|
478 apply(rename_tac n m) |
|
479 apply(erule_tac x = "m - n*k" in allE) |
|
480 apply(simp add:int_distrib mult_ac) |
|
481 done |
|
482 |
|
483 text {* |
|
484 \medskip These are the atomic cases for the proof generation for the |
|
485 equivalence of @{text P} and @{text "P minusinfinity"} for integers |
|
486 @{text x} less than some integer @{text z}. |
|
487 |
|
488 They are fully based on arithmetics. *} |
|
489 |
|
490 lemma eq_eq_minf: "EX z::int. ALL x. x < z --> (( 0 = x +t ) = False )" |
|
491 apply(rule_tac x = "-t" in exI) |
|
492 apply simp |
|
493 done |
|
494 |
|
495 lemma neq_eq_minf: "EX z::int. ALL x. x < z --> ((~( 0 = x +t )) = True )" |
|
496 apply(rule_tac x = "-t" in exI) |
|
497 apply simp |
|
498 done |
|
499 |
|
500 lemma le_eq_minf: "EX z::int. ALL x. x < z --> ( 0 < x +t = False )" |
|
501 apply(rule_tac x = "-t" in exI) |
|
502 apply simp |
|
503 done |
|
504 |
|
505 |
|
506 lemma len_eq_minf: "EX z::int. ALL x. x < z --> (0 < -x +t = True )" |
|
507 apply(rule_tac x = "t" in exI) |
|
508 apply simp |
|
509 done |
|
510 |
|
511 lemma dvd_eq_minf: "EX z::int. ALL x. x < z --> ((d dvd (x + t)) = (d dvd (x + t))) " |
|
512 by simp |
|
513 |
|
514 lemma not_dvd_eq_minf: "EX z::int. ALL x. x < z --> ((~(d dvd (x + t))) = (~(d dvd (x + t)))) " |
|
515 by simp |
|
516 |
|
517 text {* |
|
518 \medskip This Theorem combines whithnesses about @{text "P |
|
519 minusinfinity"} to show one component of the equivalence proof for |
|
520 Cooper's Theorem. |
|
521 |
|
522 FIXME: remove once they are part of the distribution. *} |
|
523 |
|
524 theorem int_ge_induct[consumes 1,case_names base step]: |
|
525 assumes ge: "k \<le> (i::int)" and |
|
526 base: "P(k)" and |
|
527 step: "\<And>i. \<lbrakk>k \<le> i; P i\<rbrakk> \<Longrightarrow> P(i+1)" |
|
528 shows "P i" |
|
529 proof - |
|
530 { fix n have "\<And>i::int. n = nat(i-k) \<Longrightarrow> k <= i \<Longrightarrow> P i" |
|
531 proof (induct n) |
|
532 case 0 |
|
533 hence "i = k" by arith |
|
534 thus "P i" using base by simp |
|
535 next |
|
536 case (Suc n) |
|
537 hence "n = nat((i - 1) - k)" by arith |
|
538 moreover |
|
539 have ki1: "k \<le> i - 1" using Suc.prems by arith |
|
540 ultimately |
|
541 have "P(i - 1)" by(rule Suc.hyps) |
|
542 from step[OF ki1 this] show ?case by simp |
|
543 qed |
|
544 } |
|
545 from this ge show ?thesis by fast |
|
546 qed |
|
547 |
|
548 theorem int_gr_induct[consumes 1,case_names base step]: |
|
549 assumes gr: "k < (i::int)" and |
|
550 base: "P(k+1)" and |
|
551 step: "\<And>i. \<lbrakk>k < i; P i\<rbrakk> \<Longrightarrow> P(i+1)" |
|
552 shows "P i" |
|
553 apply(rule int_ge_induct[of "k + 1"]) |
|
554 using gr apply arith |
|
555 apply(rule base) |
|
556 apply(rule step) |
|
557 apply simp+ |
|
558 done |
|
559 |
|
560 lemma decr_lemma: "0 < (d::int) \<Longrightarrow> x - (abs(x-z)+1) * d < z" |
|
561 apply(induct rule: int_gr_induct) |
|
562 apply simp |
|
563 apply (simp add:int_distrib) |
|
564 done |
|
565 |
|
566 lemma incr_lemma: "0 < (d::int) \<Longrightarrow> z < x + (abs(x-z)+1) * d" |
|
567 apply(induct rule: int_gr_induct) |
|
568 apply simp |
|
569 apply (simp add:int_distrib) |
|
570 done |
|
571 |
|
572 lemma minusinfinity: |
|
573 assumes "0 < d" and |
|
574 P1eqP1: "ALL x k. P1 x = P1(x - k*d)" and |
|
575 ePeqP1: "EX z::int. ALL x. x < z \<longrightarrow> (P x = P1 x)" |
|
576 shows "(EX x. P1 x) \<longrightarrow> (EX x. P x)" |
|
577 proof |
|
578 assume eP1: "EX x. P1 x" |
|
579 then obtain x where P1: "P1 x" .. |
|
580 from ePeqP1 obtain z where P1eqP: "ALL x. x < z \<longrightarrow> (P x = P1 x)" .. |
|
581 let ?w = "x - (abs(x-z)+1) * d" |
|
582 show "EX x. P x" |
|
583 proof |
|
584 have w: "?w < z" by(rule decr_lemma) |
|
585 have "P1 x = P1 ?w" using P1eqP1 by blast |
|
586 also have "\<dots> = P(?w)" using w P1eqP by blast |
|
587 finally show "P ?w" using P1 by blast |
|
588 qed |
|
589 qed |
|
590 |
|
591 text {* |
|
592 \medskip This Theorem combines whithnesses about @{text "P |
|
593 minusinfinity"} to show one component of the equivalence proof for |
|
594 Cooper's Theorem. *} |
|
595 |
|
596 lemma plusinfinity: |
|
597 assumes "0 < d" and |
|
598 P1eqP1: "ALL (x::int) (k::int). P1 x = P1 (x + k * d)" and |
|
599 ePeqP1: "EX z::int. ALL x. z < x --> (P x = P1 x)" |
|
600 shows "(EX x::int. P1 x) --> (EX x::int. P x)" |
|
601 proof |
|
602 assume eP1: "EX x. P1 x" |
|
603 then obtain x where P1: "P1 x" .. |
|
604 from ePeqP1 obtain z where P1eqP: "ALL x. z < x \<longrightarrow> (P x = P1 x)" .. |
|
605 let ?w = "x + (abs(x-z)+1) * d" |
|
606 show "EX x. P x" |
|
607 proof |
|
608 have w: "z < ?w" by(rule incr_lemma) |
|
609 have "P1 x = P1 ?w" using P1eqP1 by blast |
|
610 also have "\<dots> = P(?w)" using w P1eqP by blast |
|
611 finally show "P ?w" using P1 by blast |
|
612 qed |
|
613 qed |
|
614 |
|
615 text {* |
|
616 \medskip Theorem for periodic function on discrete sets. *} |
|
617 |
|
618 lemma minf_vee: |
|
619 assumes dpos: "(0::int) < d" and modd: "ALL x k. P x = P(x - k*d)" |
182 assumes dpos: "(0::int) < d" and modd: "ALL x k. P x = P(x - k*d)" |
620 shows "(EX x. P x) = (EX j : {1..d}. P j)" |
183 shows "(EX x. P x) = (EX j : {1..d}. P j)" |
621 (is "?LHS = ?RHS") |
184 (is "?LHS = ?RHS") |
622 proof |
185 proof |
623 assume ?LHS |
186 assume ?LHS |
624 then obtain x where P: "P x" .. |
187 then obtain x where P: "P x" .. |
625 have "x mod d = x - (x div d)*d" |
188 have "x mod d = x - (x div d)*d" by(simp add:zmod_zdiv_equality mult_ac eq_diff_eq) |
626 by(simp add:zmod_zdiv_equality mult_ac eq_diff_eq) |
|
627 hence Pmod: "P x = P(x mod d)" using modd by simp |
189 hence Pmod: "P x = P(x mod d)" using modd by simp |
628 show ?RHS |
190 show ?RHS |
629 proof (cases) |
191 proof (cases) |
630 assume "x mod d = 0" |
192 assume "x mod d = 0" |
631 hence "P 0" using P Pmod by simp |
193 hence "P 0" using P Pmod by simp |
642 moreover have "x mod d < d" by(rule pos_mod_bound) |
204 moreover have "x mod d < d" by(rule pos_mod_bound) |
643 ultimately show ?thesis using not0 by(simp add:atLeastAtMost_iff) |
205 ultimately show ?thesis using not0 by(simp add:atLeastAtMost_iff) |
644 qed |
206 qed |
645 ultimately show ?RHS .. |
207 ultimately show ?RHS .. |
646 qed |
208 qed |
647 next |
209 qed auto |
648 assume ?RHS thus ?LHS by blast |
210 |
|
211 subsection{* The @{text "-\<infinity>"} Version*} |
|
212 |
|
213 lemma decr_lemma: "0 < (d::int) \<Longrightarrow> x - (abs(x-z)+1) * d < z" |
|
214 by(induct rule: int_gr_induct,simp_all add:int_distrib) |
|
215 |
|
216 lemma incr_lemma: "0 < (d::int) \<Longrightarrow> z < x + (abs(x-z)+1) * d" |
|
217 by(induct rule: int_gr_induct, simp_all add:int_distrib) |
|
218 |
|
219 theorem int_induct[case_names base step1 step2]: |
|
220 assumes |
|
221 base: "P(k::int)" and step1: "\<And>i. \<lbrakk>k \<le> i; P i\<rbrakk> \<Longrightarrow> P(i+1)" and |
|
222 step2: "\<And>i. \<lbrakk>k \<ge> i; P i\<rbrakk> \<Longrightarrow> P(i - 1)" |
|
223 shows "P i" |
|
224 proof - |
|
225 have "i \<le> k \<or> i\<ge> k" by arith |
|
226 thus ?thesis using prems int_ge_induct[where P="P" and k="k" and i="i"] int_le_induct[where P="P" and k="k" and i="i"] by blast |
649 qed |
227 qed |
650 |
228 |
651 text {* |
|
652 \medskip Theorem for periodic function on discrete sets. *} |
|
653 |
|
654 lemma pinf_vee: |
|
655 assumes dpos: "0 < (d::int)" and modd: "ALL (x::int) (k::int). P x = P (x+k*d)" |
|
656 shows "(EX x::int. P x) = (EX (j::int) : {1..d} . P j)" |
|
657 (is "?LHS = ?RHS") |
|
658 proof |
|
659 assume ?LHS |
|
660 then obtain x where P: "P x" .. |
|
661 have "x mod d = x + (-(x div d))*d" |
|
662 by(simp add:zmod_zdiv_equality mult_ac eq_diff_eq) |
|
663 hence Pmod: "P x = P(x mod d)" using modd by (simp only:) |
|
664 show ?RHS |
|
665 proof (cases) |
|
666 assume "x mod d = 0" |
|
667 hence "P 0" using P Pmod by simp |
|
668 moreover have "P 0 = P(0 + 1*d)" using modd by blast |
|
669 ultimately have "P d" by simp |
|
670 moreover have "d : {1..d}" using dpos by(simp add:atLeastAtMost_iff) |
|
671 ultimately show ?RHS .. |
|
672 next |
|
673 assume not0: "x mod d \<noteq> 0" |
|
674 have "P(x mod d)" using dpos P Pmod by(simp add:pos_mod_sign pos_mod_bound) |
|
675 moreover have "x mod d : {1..d}" |
|
676 proof - |
|
677 have "0 \<le> x mod d" by(rule pos_mod_sign) |
|
678 moreover have "x mod d < d" by(rule pos_mod_bound) |
|
679 ultimately show ?thesis using not0 by(simp add:atLeastAtMost_iff) |
|
680 qed |
|
681 ultimately show ?RHS .. |
|
682 qed |
|
683 next |
|
684 assume ?RHS thus ?LHS by blast |
|
685 qed |
|
686 |
|
687 lemma decr_mult_lemma: |
229 lemma decr_mult_lemma: |
688 assumes dpos: "(0::int) < d" and |
230 assumes dpos: "(0::int) < d" and minus: "\<forall>x. P x \<longrightarrow> P(x - d)" and knneg: "0 <= k" |
689 minus: "ALL x::int. P x \<longrightarrow> P(x - d)" and |
|
690 knneg: "0 <= k" |
|
691 shows "ALL x. P x \<longrightarrow> P(x - k*d)" |
231 shows "ALL x. P x \<longrightarrow> P(x - k*d)" |
692 using knneg |
232 using knneg |
693 proof (induct rule:int_ge_induct) |
233 proof (induct rule:int_ge_induct) |
694 case base thus ?case by simp |
234 case base thus ?case by simp |
695 next |
235 next |
696 case (step i) |
236 case (step i) |
697 show ?case |
237 {fix x |
698 proof |
|
699 fix x |
|
700 have "P x \<longrightarrow> P (x - i * d)" using step.hyps by blast |
238 have "P x \<longrightarrow> P (x - i * d)" using step.hyps by blast |
701 also have "\<dots> \<longrightarrow> P(x - (i + 1) * d)" |
239 also have "\<dots> \<longrightarrow> P(x - (i + 1) * d)" using minus[THEN spec, of "x - i * d"] |
702 using minus[THEN spec, of "x - i * d"] |
|
703 by (simp add:int_distrib OrderedGroup.diff_diff_eq[symmetric]) |
240 by (simp add:int_distrib OrderedGroup.diff_diff_eq[symmetric]) |
704 ultimately show "P x \<longrightarrow> P(x - (i + 1) * d)" by blast |
241 ultimately have "P x \<longrightarrow> P(x - (i + 1) * d)" by blast} |
705 qed |
242 thus ?case .. |
706 qed |
243 qed |
707 |
244 |
|
245 lemma minusinfinity: |
|
246 assumes "0 < d" and |
|
247 P1eqP1: "ALL x k. P1 x = P1(x - k*d)" and ePeqP1: "EX z::int. ALL x. x < z \<longrightarrow> (P x = P1 x)" |
|
248 shows "(EX x. P1 x) \<longrightarrow> (EX x. P x)" |
|
249 proof |
|
250 assume eP1: "EX x. P1 x" |
|
251 then obtain x where P1: "P1 x" .. |
|
252 from ePeqP1 obtain z where P1eqP: "ALL x. x < z \<longrightarrow> (P x = P1 x)" .. |
|
253 let ?w = "x - (abs(x-z)+1) * d" |
|
254 have w: "?w < z" by(rule decr_lemma) |
|
255 have "P1 x = P1 ?w" using P1eqP1 by blast |
|
256 also have "\<dots> = P(?w)" using w P1eqP by blast |
|
257 finally have "P ?w" using P1 by blast |
|
258 thus "EX x. P x" .. |
|
259 qed |
|
260 |
|
261 lemma cpmi: |
|
262 assumes dp: "0 < D" and p1:"\<exists>z. \<forall> x< z. P x = P' x" |
|
263 and nb:"\<forall>x.(\<forall> j\<in> {1..D}. \<forall>(b::int) \<in> B. x \<noteq> b+j) --> P (x) --> P (x - D)" |
|
264 and pd: "\<forall> x k. P' x = P' (x-k*D)" |
|
265 shows "(\<exists>x. P x) = ((\<exists> j\<in> {1..D} . P' j) | (\<exists> j \<in> {1..D}.\<exists> b\<in> B. P (b+j)))" |
|
266 (is "?L = (?R1 \<or> ?R2)") |
|
267 proof- |
|
268 {assume "?R2" hence "?L" by blast} |
|
269 moreover |
|
270 {assume H:"?R1" hence "?L" using minusinfinity[OF dp pd p1] periodic_finite_ex[OF dp pd] by simp} |
|
271 moreover |
|
272 { fix x |
|
273 assume P: "P x" and H: "\<not> ?R2" |
|
274 {fix y assume "\<not> (\<exists>j\<in>{1..D}. \<exists>b\<in>B. P (b + j))" and P: "P y" |
|
275 hence "~(EX (j::int) : {1..D}. EX (b::int) : B. y = b+j)" by auto |
|
276 with nb P have "P (y - D)" by auto } |
|
277 hence "ALL x.~(EX (j::int) : {1..D}. EX (b::int) : B. P(b+j)) --> P (x) --> P (x - D)" by blast |
|
278 with H P have th: " \<forall>x. P x \<longrightarrow> P (x - D)" by auto |
|
279 from p1 obtain z where z: "ALL x. x < z --> (P x = P' x)" by blast |
|
280 let ?y = "x - (\<bar>x - z\<bar> + 1)*D" |
|
281 have zp: "0 <= (\<bar>x - z\<bar> + 1)" by arith |
|
282 from dp have yz: "?y < z" using decr_lemma[OF dp] by simp |
|
283 from z[rule_format, OF yz] decr_mult_lemma[OF dp th zp, rule_format, OF P] have th2: " P' ?y" by auto |
|
284 with periodic_finite_ex[OF dp pd] |
|
285 have "?R1" by blast} |
|
286 ultimately show ?thesis by blast |
|
287 qed |
|
288 |
|
289 subsection {* The @{text "+\<infinity>"} Version*} |
|
290 |
|
291 lemma plusinfinity: |
|
292 assumes "(0::int) < d" and |
|
293 P1eqP1: "\<forall>x k. P' x = P'(x - k*d)" and ePeqP1: "\<exists> z. \<forall> x>z. P x = P' x" |
|
294 shows "(\<exists> x. P' x) \<longrightarrow> (\<exists> x. P x)" |
|
295 proof |
|
296 assume eP1: "EX x. P' x" |
|
297 then obtain x where P1: "P' x" .. |
|
298 from ePeqP1 obtain z where P1eqP: "\<forall>x>z. P x = P' x" .. |
|
299 let ?w' = "x + (abs(x-z)+1) * d" |
|
300 let ?w = "x - (-(abs(x-z) + 1))*d" |
|
301 have ww'[simp]: "?w = ?w'" by (simp add: ring_eq_simps) |
|
302 have w: "?w > z" by(simp only: ww', rule incr_lemma) |
|
303 hence "P' x = P' ?w" using P1eqP1 by blast |
|
304 also have "\<dots> = P(?w)" using w P1eqP by blast |
|
305 finally have "P ?w" using P1 by blast |
|
306 thus "EX x. P x" .. |
|
307 qed |
|
308 |
708 lemma incr_mult_lemma: |
309 lemma incr_mult_lemma: |
709 assumes dpos: "(0::int) < d" and |
310 assumes dpos: "(0::int) < d" and plus: "ALL x::int. P x \<longrightarrow> P(x + d)" and knneg: "0 <= k" |
710 plus: "ALL x::int. P x \<longrightarrow> P(x + d)" and |
|
711 knneg: "0 <= k" |
|
712 shows "ALL x. P x \<longrightarrow> P(x + k*d)" |
311 shows "ALL x. P x \<longrightarrow> P(x + k*d)" |
713 using knneg |
312 using knneg |
714 proof (induct rule:int_ge_induct) |
313 proof (induct rule:int_ge_induct) |
715 case base thus ?case by simp |
314 case base thus ?case by simp |
716 next |
315 next |
717 case (step i) |
316 case (step i) |
718 show ?case |
317 {fix x |
719 proof |
|
720 fix x |
|
721 have "P x \<longrightarrow> P (x + i * d)" using step.hyps by blast |
318 have "P x \<longrightarrow> P (x + i * d)" using step.hyps by blast |
722 also have "\<dots> \<longrightarrow> P(x + (i + 1) * d)" |
319 also have "\<dots> \<longrightarrow> P(x + (i + 1) * d)" using plus[THEN spec, of "x + i * d"] |
723 using plus[THEN spec, of "x + i * d"] |
|
724 by (simp add:int_distrib zadd_ac) |
320 by (simp add:int_distrib zadd_ac) |
725 ultimately show "P x \<longrightarrow> P(x + (i + 1) * d)" by blast |
321 ultimately have "P x \<longrightarrow> P(x + (i + 1) * d)" by blast} |
726 qed |
322 thus ?case .. |
727 qed |
323 qed |
728 |
324 |
729 lemma cpmi_eq: "0 < D \<Longrightarrow> (EX z::int. ALL x. x < z --> (P x = P1 x)) |
325 lemma cppi: |
730 ==> ALL x.~(EX (j::int) : {1..D}. EX (b::int) : B. P(b+j)) --> P (x) --> P (x - D) |
326 assumes dp: "0 < D" and p1:"\<exists>z. \<forall> x> z. P x = P' x" |
731 ==> (ALL (x::int). ALL (k::int). ((P1 x)= (P1 (x-k*D)))) |
327 and nb:"\<forall>x.(\<forall> j\<in> {1..D}. \<forall>(b::int) \<in> A. x \<noteq> b - j) --> P (x) --> P (x + D)" |
732 ==> (EX (x::int). P(x)) = ((EX (j::int) : {1..D} . (P1(j))) | (EX (j::int) : {1..D}. EX (b::int) : B. P (b+j)))" |
328 and pd: "\<forall> x k. P' x= P' (x-k*D)" |
733 apply(rule iffI) |
329 shows "(\<exists>x. P x) = ((\<exists> j\<in> {1..D} . P' j) | (\<exists> j \<in> {1..D}.\<exists> b\<in> A. P (b - j)))" (is "?L = (?R1 \<or> ?R2)") |
734 prefer 2 |
330 proof- |
735 apply(drule minusinfinity) |
331 {assume "?R2" hence "?L" by blast} |
736 apply assumption+ |
332 moreover |
737 apply(fastsimp) |
333 {assume H:"?R1" hence "?L" using plusinfinity[OF dp pd p1] periodic_finite_ex[OF dp pd] by simp} |
738 apply clarsimp |
334 moreover |
739 apply(subgoal_tac "!!k. 0<=k \<Longrightarrow> !x. P x \<longrightarrow> P (x - k*D)") |
335 { fix x |
740 apply(frule_tac x = x and z=z in decr_lemma) |
336 assume P: "P x" and H: "\<not> ?R2" |
741 apply(subgoal_tac "P1(x - (\<bar>x - z\<bar> + 1) * D)") |
337 {fix y assume "\<not> (\<exists>j\<in>{1..D}. \<exists>b\<in>A. P (b - j))" and P: "P y" |
742 prefer 2 |
338 hence "~(EX (j::int) : {1..D}. EX (b::int) : A. y = b - j)" by auto |
743 apply(subgoal_tac "0 <= (\<bar>x - z\<bar> + 1)") |
339 with nb P have "P (y + D)" by auto } |
744 prefer 2 apply arith |
340 hence "ALL x.~(EX (j::int) : {1..D}. EX (b::int) : A. P(b-j)) --> P (x) --> P (x + D)" by blast |
745 apply fastsimp |
341 with H P have th: " \<forall>x. P x \<longrightarrow> P (x + D)" by auto |
746 apply(drule (1) minf_vee) |
342 from p1 obtain z where z: "ALL x. x > z --> (P x = P' x)" by blast |
747 apply blast |
343 let ?y = "x + (\<bar>x - z\<bar> + 1)*D" |
748 apply(blast dest:decr_mult_lemma) |
344 have zp: "0 <= (\<bar>x - z\<bar> + 1)" by arith |
749 done |
345 from dp have yz: "?y > z" using incr_lemma[OF dp] by simp |
750 |
346 from z[rule_format, OF yz] incr_mult_lemma[OF dp th zp, rule_format, OF P] have th2: " P' ?y" by auto |
751 text {* Cooper Theorem, plus infinity version. *} |
347 with periodic_finite_ex[OF dp pd] |
752 lemma cppi_eq: "0 < D \<Longrightarrow> (EX z::int. ALL x. z < x --> (P x = P1 x)) |
348 have "?R1" by blast} |
753 ==> ALL x.~(EX (j::int) : {1..D}. EX (a::int) : A. P(a - j)) --> P (x) --> P (x + D) |
349 ultimately show ?thesis by blast |
754 ==> (ALL (x::int). ALL (k::int). ((P1 x)= (P1 (x+k*D)))) |
350 qed |
755 ==> (EX (x::int). P(x)) = ((EX (j::int) : {1..D} . (P1(j))) | (EX (j::int) : {1..D}. EX (a::int) : A. P (a - j)))" |
|
756 apply(rule iffI) |
|
757 prefer 2 |
|
758 apply(drule plusinfinity) |
|
759 apply assumption+ |
|
760 apply(fastsimp) |
|
761 apply clarsimp |
|
762 apply(subgoal_tac "!!k. 0<=k \<Longrightarrow> !x. P x \<longrightarrow> P (x + k*D)") |
|
763 apply(frule_tac x = x and z=z in incr_lemma) |
|
764 apply(subgoal_tac "P1(x + (\<bar>x - z\<bar> + 1) * D)") |
|
765 prefer 2 |
|
766 apply(subgoal_tac "0 <= (\<bar>x - z\<bar> + 1)") |
|
767 prefer 2 apply arith |
|
768 apply fastsimp |
|
769 apply(drule (1) pinf_vee) |
|
770 apply blast |
|
771 apply(blast dest:incr_mult_lemma) |
|
772 done |
|
773 |
|
774 |
|
775 text {* |
|
776 \bigskip Theorems for the quantifier elminination Functions. *} |
|
777 |
|
778 lemma qe_ex_conj: "(EX (x::int). A x) = R |
|
779 ==> (EX (x::int). P x) = (Q & (EX x::int. A x)) |
|
780 ==> (EX (x::int). P x) = (Q & R)" |
|
781 by blast |
|
782 |
|
783 lemma qe_ex_nconj: "(EX (x::int). P x) = (True & Q) |
|
784 ==> (EX (x::int). P x) = Q" |
|
785 by blast |
|
786 |
|
787 lemma qe_conjI: "P1 = P2 ==> Q1 = Q2 ==> (P1 & Q1) = (P2 & Q2)" |
|
788 by blast |
|
789 |
|
790 lemma qe_disjI: "P1 = P2 ==> Q1 = Q2 ==> (P1 | Q1) = (P2 | Q2)" |
|
791 by blast |
|
792 |
|
793 lemma qe_impI: "P1 = P2 ==> Q1 = Q2 ==> (P1 --> Q1) = (P2 --> Q2)" |
|
794 by blast |
|
795 |
|
796 lemma qe_eqI: "P1 = P2 ==> Q1 = Q2 ==> (P1 = Q1) = (P2 = Q2)" |
|
797 by blast |
|
798 |
|
799 lemma qe_Not: "P = Q ==> (~P) = (~Q)" |
|
800 by blast |
|
801 |
|
802 lemma qe_ALL: "(EX x. ~P x) = R ==> (ALL x. P x) = (~R)" |
|
803 by blast |
|
804 |
|
805 text {* \bigskip Theorems for proving NNF *} |
|
806 |
|
807 lemma nnf_im: "((~P) = P1) ==> (Q=Q1) ==> ((P --> Q) = (P1 | Q1))" |
|
808 by blast |
|
809 |
|
810 lemma nnf_eq: "((P & Q) = (P1 & Q1)) ==> (((~P) & (~Q)) = (P2 & Q2)) ==> ((P = Q) = ((P1 & Q1)|(P2 & Q2)))" |
|
811 by blast |
|
812 |
|
813 lemma nnf_nn: "(P = Q) ==> ((~~P) = Q)" |
|
814 by blast |
|
815 lemma nnf_ncj: "((~P) = P1) ==> ((~Q) = Q1) ==> ((~(P & Q)) = (P1 | Q1))" |
|
816 by blast |
|
817 |
|
818 lemma nnf_ndj: "((~P) = P1) ==> ((~Q) = Q1) ==> ((~(P | Q)) = (P1 & Q1))" |
|
819 by blast |
|
820 lemma nnf_nim: "(P = P1) ==> ((~Q) = Q1) ==> ((~(P --> Q)) = (P1 & Q1))" |
|
821 by blast |
|
822 lemma nnf_neq: "((P & (~Q)) = (P1 & Q1)) ==> (((~P) & Q) = (P2 & Q2)) ==> ((~(P = Q)) = ((P1 & Q1)|(P2 & Q2)))" |
|
823 by blast |
|
824 lemma nnf_sdj: "((A & (~B)) = (A1 & B1)) ==> ((C & (~D)) = (C1 & D1)) ==> (A = (~C)) ==> ((~((A & B) | (C & D))) = ((A1 & B1) | (C1 & D1)))" |
|
825 by blast |
|
826 |
|
827 |
|
828 lemma qe_exI2: "A = B ==> (EX (x::int). A(x)) = (EX (x::int). B(x))" |
|
829 by simp |
|
830 |
|
831 lemma qe_exI: "(!!x::int. A x = B x) ==> (EX (x::int). A(x)) = (EX (x::int). B(x))" |
|
832 by iprover |
|
833 |
|
834 lemma qe_ALLI: "(!!x::int. A x = B x) ==> (ALL (x::int). A(x)) = (ALL (x::int). B(x))" |
|
835 by iprover |
|
836 |
|
837 lemma cp_expand: "(EX (x::int). P (x)) = (EX (j::int) : {1..d}. EX (b::int) : B. (P1 (j) | P(b+j))) |
|
838 ==>(EX (x::int). P (x)) = (EX (j::int) : {1..d}. EX (b::int) : B. (P1 (j) | P(b+j))) " |
|
839 by blast |
|
840 |
|
841 lemma cppi_expand: "(EX (x::int). P (x)) = (EX (j::int) : {1..d}. EX (a::int) : A. (P1 (j) | P(a - j))) |
|
842 ==>(EX (x::int). P (x)) = (EX (j::int) : {1..d}. EX (a::int) : A. (P1 (j) | P(a - j))) " |
|
843 by blast |
|
844 |
|
845 |
351 |
846 lemma simp_from_to: "{i..j::int} = (if j < i then {} else insert i {i+1..j})" |
352 lemma simp_from_to: "{i..j::int} = (if j < i then {} else insert i {i+1..j})" |
847 apply(simp add:atLeastAtMost_def atLeast_def atMost_def) |
353 apply(simp add:atLeastAtMost_def atLeast_def atMost_def) |
848 apply(fastsimp) |
354 apply(fastsimp) |
849 done |
355 done |
850 |
356 |
851 text {* \bigskip Theorems required for the @{text adjustcoeffitienteq} *} |
357 theorem unity_coeff_ex: "(\<exists>(x::'a::{semiring_0}). P (l * x)) \<equiv> (\<exists>x. l dvd (x + 0) \<and> P x)" |
852 |
358 apply (rule eq_reflection[symmetric]) |
853 lemma ac_dvd_eq: assumes not0: "0 ~= (k::int)" |
359 apply (rule iffI) |
854 shows "((m::int) dvd (c*n+t)) = (k*m dvd ((k*c)*n+(k*t)))" (is "?P = ?Q") |
360 defer |
855 proof |
361 apply (erule exE) |
856 assume ?P |
362 apply (rule_tac x = "l * x" in exI) |
857 thus ?Q |
363 apply (simp add: dvd_def) |
858 apply(simp add:dvd_def) |
364 apply (rule_tac x="x" in exI, simp) |
859 apply clarify |
365 apply (erule exE) |
860 apply(rename_tac d) |
366 apply (erule conjE) |
861 apply(drule_tac f = "op * k" in arg_cong) |
367 apply (erule dvdE) |
862 apply(simp only:int_distrib) |
368 apply (rule_tac x = k in exI) |
863 apply(rule_tac x = "d" in exI) |
369 apply simp |
864 apply(simp only:mult_ac) |
370 done |
865 done |
371 |
866 next |
372 lemma zdvd_mono: assumes not0: "(k::int) \<noteq> 0" |
867 assume ?Q |
373 shows "((m::int) dvd t) \<equiv> (k*m dvd k*t)" |
868 then obtain d where "k * c * n + k * t = (k*m)*d" by(fastsimp simp:dvd_def) |
374 using not0 by (simp add: dvd_def) |
869 hence "(c * n + t) * k = (m*d) * k" by(simp add:int_distrib mult_ac) |
375 |
870 hence "((c * n + t) * k) div k = ((m*d) * k) div k" by(rule arg_cong[of _ _ "%t. t div k"]) |
376 lemma all_not_ex: "(ALL x. P x) = (~ (EX x. ~ P x ))" |
871 hence "c*n+t = m*d" by(simp add: zdiv_zmult_self1[OF not0[symmetric]]) |
377 by blast |
872 thus ?P by(simp add:dvd_def) |
378 |
873 qed |
379 lemma uminus_dvd_conv: "(d dvd (t::int)) \<equiv> (-d dvd t)" "(d dvd (t::int)) \<equiv> (d dvd -t)" |
874 |
380 by simp_all |
875 lemma ac_lt_eq: assumes gr0: "0 < (k::int)" |
|
876 shows "((m::int) < (c*n+t)) = (k*m <((k*c)*n+(k*t)))" (is "?P = ?Q") |
|
877 proof |
|
878 assume P: ?P |
|
879 show ?Q using zmult_zless_mono2[OF P gr0] by(simp add: int_distrib mult_ac) |
|
880 next |
|
881 assume ?Q |
|
882 hence "0 < k*(c*n + t - m)" by(simp add: int_distrib mult_ac) |
|
883 with gr0 have "0 < (c*n + t - m)" by(simp add: zero_less_mult_iff) |
|
884 thus ?P by(simp) |
|
885 qed |
|
886 |
|
887 lemma ac_eq_eq : assumes not0: "0 ~= (k::int)" shows "((m::int) = (c*n+t)) = (k*m =((k*c)*n+(k*t)) )" (is "?P = ?Q") |
|
888 proof |
|
889 assume ?P |
|
890 thus ?Q |
|
891 apply(drule_tac f = "op * k" in arg_cong) |
|
892 apply(simp only:int_distrib) |
|
893 done |
|
894 next |
|
895 assume ?Q |
|
896 hence "m * k = (c*n + t) * k" by(simp add:int_distrib mult_ac) |
|
897 hence "((m) * k) div k = ((c*n + t) * k) div k" by(rule arg_cong[of _ _ "%t. t div k"]) |
|
898 thus ?P by(simp add: zdiv_zmult_self1[OF not0[symmetric]]) |
|
899 qed |
|
900 |
|
901 lemma ac_pi_eq: assumes gr0: "0 < (k::int)" shows "(~((0::int) < (c*n + t))) = (0 < ((-k)*c)*n + ((-k)*t + k))" |
|
902 proof - |
|
903 have "(~ (0::int) < (c*n + t)) = (0<1-(c*n + t))" by arith |
|
904 also have "(1-(c*n + t)) = (-1*c)*n + (-t+1)" by(simp add: int_distrib mult_ac) |
|
905 also have "0<(-1*c)*n + (-t+1) = (0 < (k*(-1*c)*n) + (k*(-t+1)))" by(rule ac_lt_eq[of _ 0,OF gr0,simplified]) |
|
906 also have "(k*(-1*c)*n) + (k*(-t+1)) = ((-k)*c)*n + ((-k)*t + k)" by(simp add: int_distrib mult_ac) |
|
907 finally show ?thesis . |
|
908 qed |
|
909 |
|
910 lemma binminus_uminus_conv: "(a::int) - b = a + (-b)" |
|
911 by arith |
|
912 |
|
913 lemma linearize_dvd: "(t::int) = t1 ==> (d dvd t) = (d dvd t1)" |
|
914 by simp |
|
915 |
|
916 lemma lf_lt: "(l::int) = ll ==> (r::int) = lr ==> (l < r) =(ll < lr)" |
|
917 by simp |
|
918 |
|
919 lemma lf_eq: "(l::int) = ll ==> (r::int) = lr ==> (l = r) =(ll = lr)" |
|
920 by simp |
|
921 |
|
922 lemma lf_dvd: "(l::int) = ll ==> (r::int) = lr ==> (l dvd r) =(ll dvd lr)" |
|
923 by simp |
|
924 |
|
925 text {* \bigskip Theorems for transforming predicates on nat to predicates on @{text int}*} |
381 text {* \bigskip Theorems for transforming predicates on nat to predicates on @{text int}*} |
926 |
382 lemma all_nat: "(\<forall>x::nat. P x) = (\<forall>x::int. 0 <= x \<longrightarrow> P (nat x))" |
927 theorem all_nat: "(\<forall>x::nat. P x) = (\<forall>x::int. 0 <= x \<longrightarrow> P (nat x))" |
|
928 by (simp split add: split_nat) |
383 by (simp split add: split_nat) |
929 |
384 |
930 |
385 lemma ex_nat: "(\<exists>x::nat. P x) = (\<exists>x::int. 0 <= x \<and> P (nat x))" |
931 theorem zdiff_int_split: "P (int (x - y)) = |
386 by (auto split add: split_nat) |
|
387 (rule_tac x = "nat x" in exI,erule_tac x = "nat x" in allE, simp) |
|
388 |
|
389 lemma zdiff_int_split: "P (int (x - y)) = |
932 ((y \<le> x \<longrightarrow> P (int x - int y)) \<and> (x < y \<longrightarrow> P 0))" |
390 ((y \<le> x \<longrightarrow> P (int x - int y)) \<and> (x < y \<longrightarrow> P 0))" |
933 apply (case_tac "y \<le> x") |
391 by (case_tac "y \<le> x",simp_all add: zdiff_int) |
934 apply (simp_all add: zdiff_int) |
392 |
|
393 lemma zdvd_int: "(x dvd y) = (int x dvd int y)" |
|
394 apply (simp only: dvd_def ex_nat int_int_eq [symmetric] zmult_int [symmetric] |
|
395 nat_0_le cong add: conj_cong) |
|
396 apply (rule iffI) |
|
397 apply iprover |
|
398 apply (erule exE) |
|
399 apply (case_tac "x=0") |
|
400 apply (rule_tac x=0 in exI) |
|
401 apply simp |
|
402 apply (case_tac "0 \<le> k") |
|
403 apply iprover |
|
404 apply (simp add: linorder_not_le) |
|
405 apply (drule mult_strict_left_mono_neg [OF iffD2 [OF zero_less_int_conv]]) |
|
406 apply assumption |
|
407 apply (simp add: mult_ac) |
935 done |
408 done |
936 |
409 |
937 |
410 lemma number_of1: "(0::int) <= number_of n \<Longrightarrow> (0::int) <= number_of (n BIT b)" by simp |
938 theorem number_of1: "(0::int) <= number_of n \<Longrightarrow> (0::int) <= number_of (n BIT b)" |
411 lemma number_of2: "(0::int) <= Numeral0" by simp |
939 by simp |
412 lemma Suc_plus1: "Suc n = n + 1" by simp |
940 |
|
941 theorem number_of2: "(0::int) <= Numeral0" by simp |
|
942 |
|
943 theorem Suc_plus1: "Suc n = n + 1" by simp |
|
944 |
413 |
945 text {* |
414 text {* |
946 \medskip Specific instances of congruence rules, to prevent |
415 \medskip Specific instances of congruence rules, to prevent |
947 simplifier from looping. *} |
416 simplifier from looping. *} |
948 |
417 |
949 theorem imp_le_cong: "(0 <= x \<Longrightarrow> P = P') \<Longrightarrow> (0 <= (x::int) \<longrightarrow> P) = (0 <= x \<longrightarrow> P')" |
418 theorem imp_le_cong: "(0 <= x \<Longrightarrow> P = P') \<Longrightarrow> (0 <= (x::int) \<longrightarrow> P) = (0 <= x \<longrightarrow> P')" by simp |
950 by simp |
419 |
951 |
420 theorem conj_le_cong: "(0 <= x \<Longrightarrow> P = P') \<Longrightarrow> (0 <= (x::int) \<and> P) = (0 <= x \<and> P')" |
952 theorem conj_le_cong: "(0 <= x \<Longrightarrow> P = P') \<Longrightarrow> (0 <= (x::int) \<and> P) = (0 <= x \<and> P')" |
|
953 by (simp cong: conj_cong) |
421 by (simp cong: conj_cong) |
954 |
|
955 (* Theorems used in presburger.ML for the computation simpset*) |
|
956 (* FIXME: They are present in Float.thy, so may be Float.thy should be lightened.*) |
|
957 |
|
958 lemma lift_bool: "x \<Longrightarrow> x=True" |
|
959 by simp |
|
960 |
|
961 lemma nlift_bool: "~x \<Longrightarrow> x=False" |
|
962 by simp |
|
963 |
|
964 lemma not_false_eq_true: "(~ False) = True" by simp |
|
965 |
|
966 lemma not_true_eq_false: "(~ True) = False" by simp |
|
967 |
|
968 |
|
969 lemma int_eq_number_of_eq: |
422 lemma int_eq_number_of_eq: |
970 "(((number_of v)::int) = (number_of w)) = iszero ((number_of (v + (uminus w)))::int)" |
423 "(((number_of v)::int) = (number_of w)) = iszero ((number_of (v + (uminus w)))::int)" |
971 by simp |
424 by simp |
972 lemma int_iszero_number_of_Pls: "iszero (Numeral0::int)" |
425 |
973 by (simp only: iszero_number_of_Pls) |
426 |
974 |
427 use "Tools/Presburger/cooper.ML" |
975 lemma int_nonzero_number_of_Min: "~(iszero ((-1)::int))" |
428 oracle linzqe_oracle ("term") = Coopereif.cooper_oracle |
976 by simp |
429 |
977 |
|
978 lemma int_iszero_number_of_0: "iszero ((number_of (w BIT bit.B0))::int) = iszero ((number_of w)::int)" |
|
979 by simp |
|
980 |
|
981 lemma int_iszero_number_of_1: "\<not> iszero ((number_of (w BIT bit.B1))::int)" |
|
982 by simp |
|
983 |
|
984 lemma int_less_number_of_eq_neg: "(((number_of x)::int) < number_of y) = neg ((number_of (x + (uminus y)))::int)" |
|
985 by simp |
|
986 |
|
987 lemma int_not_neg_number_of_Pls: "\<not> (neg (Numeral0::int))" |
|
988 by simp |
|
989 |
|
990 lemma int_neg_number_of_Min: "neg (-1::int)" |
|
991 by simp |
|
992 |
|
993 lemma int_neg_number_of_BIT: "neg ((number_of (w BIT x))::int) = neg ((number_of w)::int)" |
|
994 by simp |
|
995 |
|
996 lemma int_le_number_of_eq: "(((number_of x)::int) \<le> number_of y) = (\<not> neg ((number_of (y + (uminus x)))::int))" |
|
997 by simp |
|
998 lemma int_number_of_add_sym: "((number_of v)::int) + number_of w = number_of (v + w)" |
|
999 by simp |
|
1000 |
|
1001 lemma int_number_of_diff_sym: |
|
1002 "((number_of v)::int) - number_of w = number_of (v + (uminus w))" |
|
1003 by simp |
|
1004 |
|
1005 lemma int_number_of_mult_sym: |
|
1006 "((number_of v)::int) * number_of w = number_of (v * w)" |
|
1007 by simp |
|
1008 |
|
1009 lemma int_number_of_minus_sym: "- ((number_of v)::int) = number_of (uminus v)" |
|
1010 by simp |
|
1011 lemma add_left_zero: "0 + a = (a::'a::comm_monoid_add)" |
|
1012 by simp |
|
1013 |
|
1014 lemma add_right_zero: "a + 0 = (a::'a::comm_monoid_add)" |
|
1015 by simp |
|
1016 |
|
1017 lemma mult_left_one: "1 * a = (a::'a::semiring_1)" |
|
1018 by simp |
|
1019 |
|
1020 lemma mult_right_one: "a * 1 = (a::'a::semiring_1)" |
|
1021 by simp |
|
1022 |
|
1023 lemma int_pow_0: "(a::int)^(Numeral0) = 1" |
|
1024 by simp |
|
1025 |
|
1026 lemma int_pow_1: "(a::int)^(Numeral1) = a" |
|
1027 by simp |
|
1028 |
|
1029 lemma zero_eq_Numeral0_nring: "(0::'a::number_ring) = Numeral0" |
|
1030 by simp |
|
1031 |
|
1032 lemma one_eq_Numeral1_nring: "(1::'a::number_ring) = Numeral1" |
|
1033 by simp |
|
1034 |
|
1035 lemma zero_eq_Numeral0_nat: "(0::nat) = Numeral0" |
|
1036 by simp |
|
1037 |
|
1038 lemma one_eq_Numeral1_nat: "(1::nat) = Numeral1" |
|
1039 by simp |
|
1040 |
|
1041 lemma zpower_Pls: "(z::int)^Numeral0 = Numeral1" |
|
1042 by simp |
|
1043 |
|
1044 lemma zpower_Min: "(z::int)^((-1)::nat) = Numeral1" |
|
1045 proof - |
|
1046 have 1:"((-1)::nat) = 0" |
|
1047 by simp |
|
1048 show ?thesis by (simp add: 1) |
|
1049 qed |
|
1050 |
|
1051 use "Tools/Presburger/cooper_dec.ML" |
|
1052 use "Tools/Presburger/reflected_presburger.ML" |
|
1053 use "Tools/Presburger/reflected_cooper.ML" |
|
1054 oracle |
|
1055 presburger_oracle ("term") = ReflectedCooper.presburger_oracle |
|
1056 |
|
1057 use "Tools/Presburger/cooper_proof.ML" |
|
1058 use "Tools/Presburger/qelim.ML" |
|
1059 use "Tools/Presburger/presburger.ML" |
430 use "Tools/Presburger/presburger.ML" |
1060 |
431 |
1061 setup "Presburger.setup" |
432 setup {* |
1062 |
433 arith_tactic_add |
|
434 (mk_arith_tactic "presburger" (fn i => fn st => |
|
435 (warning "Trying Presburger arithmetic ..."; |
|
436 Presburger.cooper_tac true ((ProofContext.init o theory_of_thm) st) i st))) |
|
437 (* FIXME!!!!!!! get the right context!!*) |
|
438 *} |
|
439 method_setup presburger = {* Method.simple_args (Scan.optional (Args.$$$ "elim" >> K false) true) |
|
440 (fn q => fn ctxt => Method.SIMPLE_METHOD' (Presburger.cooper_tac q ctxt))*} "" |
|
441 (* |
|
442 method_setup presburger = {* |
|
443 Method.ctxt_args (Method.SIMPLE_METHOD' o (Presburger.cooper_tac true)) |
|
444 *} "" |
|
445 *) |
1063 |
446 |
1064 subsection {* Code generator setup *} |
447 subsection {* Code generator setup *} |
1065 |
|
1066 text {* |
448 text {* |
1067 Presburger arithmetic is convenient to prove some |
449 Presburger arithmetic is convenient to prove some |
1068 of the following code lemmas on integer numerals: |
450 of the following code lemmas on integer numerals: |
1069 *} |
451 *} |
1070 |
452 |