author | wenzelm |
Thu, 31 May 2007 18:16:52 +0200 | |
changeset 23164 | 69e55066dbca |
parent 23148 | ef3fa1386102 |
child 23253 | b1f3f53c60b5 |
permissions | -rw-r--r-- |
23148 | 1 |
(* Title: HOL/Presburger.thy |
13876 | 2 |
ID: $Id$ |
3 |
Author: Amine Chaieb, Tobias Nipkow and Stefan Berghofer, TU Muenchen |
|
4 |
||
5 |
File containing necessary theorems for the proof |
|
6 |
generation for Cooper Algorithm |
|
7 |
*) |
|
8 |
||
15131 | 9 |
header {* Presburger Arithmetic: Cooper's Algorithm *} |
14577 | 10 |
|
15131 | 11 |
theory Presburger |
23164 | 12 |
imports NatSimprocs SetInterval |
21046
fe1db2f991a7
moved HOL code generator setup to Code_Generator
haftmann
parents:
20595
diff
changeset
|
13 |
uses |
23146 | 14 |
("Tools/Presburger/cooper_dec.ML") |
15 |
("Tools/Presburger/cooper_proof.ML") |
|
16 |
("Tools/Presburger/qelim.ML") |
|
17 |
("Tools/Presburger/reflected_presburger.ML") |
|
18 |
("Tools/Presburger/reflected_cooper.ML") |
|
19 |
("Tools/Presburger/presburger.ML") |
|
15131 | 20 |
begin |
13876 | 21 |
|
14577 | 22 |
text {* Theorem for unitifying the coeffitients of @{text x} in an existential formula*} |
13876 | 23 |
|
24 |
theorem unity_coeff_ex: "(\<exists>x::int. P (l * x)) = (\<exists>x. l dvd (1*x+0) \<and> P x)" |
|
25 |
apply (rule iffI) |
|
26 |
apply (erule exE) |
|
27 |
apply (rule_tac x = "l * x" in exI) |
|
28 |
apply simp |
|
29 |
apply (erule exE) |
|
30 |
apply (erule conjE) |
|
31 |
apply (erule dvdE) |
|
32 |
apply (rule_tac x = k in exI) |
|
33 |
apply simp |
|
34 |
done |
|
35 |
||
36 |
lemma uminus_dvd_conv: "(d dvd (t::int)) = (-d dvd t)" |
|
37 |
apply(unfold dvd_def) |
|
38 |
apply(rule iffI) |
|
39 |
apply(clarsimp) |
|
40 |
apply(rename_tac k) |
|
41 |
apply(rule_tac x = "-k" in exI) |
|
42 |
apply simp |
|
43 |
apply(clarsimp) |
|
44 |
apply(rename_tac k) |
|
45 |
apply(rule_tac x = "-k" in exI) |
|
46 |
apply simp |
|
47 |
done |
|
48 |
||
49 |
lemma uminus_dvd_conv': "(d dvd (t::int)) = (d dvd -t)" |
|
50 |
apply(unfold dvd_def) |
|
51 |
apply(rule iffI) |
|
52 |
apply(clarsimp) |
|
53 |
apply(rule_tac x = "-k" in exI) |
|
54 |
apply simp |
|
55 |
apply(clarsimp) |
|
56 |
apply(rule_tac x = "-k" in exI) |
|
57 |
apply simp |
|
58 |
done |
|
59 |
||
60 |
||
61 |
||
14577 | 62 |
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}.*} |
13876 | 63 |
|
64 |
theorem eq_minf_conjI: "\<exists>z1::int. \<forall>x. x < z1 \<longrightarrow> (A1 x = A2 x) \<Longrightarrow> |
|
65 |
\<exists>z2::int. \<forall>x. x < z2 \<longrightarrow> (B1 x = B2 x) \<Longrightarrow> |
|
66 |
\<exists>z::int. \<forall>x. x < z \<longrightarrow> ((A1 x \<and> B1 x) = (A2 x \<and> B2 x))" |
|
67 |
apply (erule exE)+ |
|
68 |
apply (rule_tac x = "min z1 z2" in exI) |
|
69 |
apply simp |
|
70 |
done |
|
71 |
||
72 |
||
73 |
theorem eq_minf_disjI: "\<exists>z1::int. \<forall>x. x < z1 \<longrightarrow> (A1 x = A2 x) \<Longrightarrow> |
|
74 |
\<exists>z2::int. \<forall>x. x < z2 \<longrightarrow> (B1 x = B2 x) \<Longrightarrow> |
|
75 |
\<exists>z::int. \<forall>x. x < z \<longrightarrow> ((A1 x \<or> B1 x) = (A2 x \<or> B2 x))" |
|
76 |
||
77 |
apply (erule exE)+ |
|
78 |
apply (rule_tac x = "min z1 z2" in exI) |
|
79 |
apply simp |
|
80 |
done |
|
81 |
||
82 |
||
14577 | 83 |
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}.*} |
13876 | 84 |
|
85 |
theorem eq_pinf_conjI: "\<exists>z1::int. \<forall>x. z1 < x \<longrightarrow> (A1 x = A2 x) \<Longrightarrow> |
|
86 |
\<exists>z2::int. \<forall>x. z2 < x \<longrightarrow> (B1 x = B2 x) \<Longrightarrow> |
|
87 |
\<exists>z::int. \<forall>x. z < x \<longrightarrow> ((A1 x \<and> B1 x) = (A2 x \<and> B2 x))" |
|
88 |
apply (erule exE)+ |
|
89 |
apply (rule_tac x = "max z1 z2" in exI) |
|
90 |
apply simp |
|
91 |
done |
|
92 |
||
93 |
||
94 |
theorem eq_pinf_disjI: "\<exists>z1::int. \<forall>x. z1 < x \<longrightarrow> (A1 x = A2 x) \<Longrightarrow> |
|
95 |
\<exists>z2::int. \<forall>x. z2 < x \<longrightarrow> (B1 x = B2 x) \<Longrightarrow> |
|
96 |
\<exists>z::int. \<forall>x. z < x \<longrightarrow> ((A1 x \<or> B1 x) = (A2 x \<or> B2 x))" |
|
97 |
apply (erule exE)+ |
|
98 |
apply (rule_tac x = "max z1 z2" in exI) |
|
99 |
apply simp |
|
100 |
done |
|
14577 | 101 |
|
102 |
text {* |
|
103 |
\medskip Theorems for the combination of proofs of the modulo @{text |
|
104 |
D} property for @{text "P plusinfinity"} |
|
105 |
||
106 |
FIXME: This is THE SAME theorem as for the @{text minusinf} version, |
|
107 |
but with @{text "+k.."} instead of @{text "-k.."} In the future |
|
108 |
replace these both with only one. *} |
|
13876 | 109 |
|
110 |
theorem modd_pinf_conjI: "\<forall>(x::int) k. A x = A (x+k*d) \<Longrightarrow> |
|
111 |
\<forall>(x::int) k. B x = B (x+k*d) \<Longrightarrow> |
|
112 |
\<forall>(x::int) (k::int). (A x \<and> B x) = (A (x+k*d) \<and> B (x+k*d))" |
|
113 |
by simp |
|
114 |
||
115 |
theorem modd_pinf_disjI: "\<forall>(x::int) k. A x = A (x+k*d) \<Longrightarrow> |
|
116 |
\<forall>(x::int) k. B x = B (x+k*d) \<Longrightarrow> |
|
117 |
\<forall>(x::int) (k::int). (A x \<or> B x) = (A (x+k*d) \<or> B (x+k*d))" |
|
118 |
by simp |
|
119 |
||
14577 | 120 |
text {* |
121 |
This is one of the cases where the simplifed formula is prooved to |
|
122 |
habe some property (in relation to @{text P_m}) but we need to prove |
|
123 |
the property for the original formula (@{text P_m}) |
|
124 |
||
125 |
FIXME: This is exaclty the same thm as for @{text minusinf}. *} |
|
126 |
||
13876 | 127 |
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)) " |
14577 | 128 |
by blast |
13876 | 129 |
|
130 |
||
14577 | 131 |
text {* |
132 |
\medskip Theorems for the combination of proofs of the modulo @{text D} |
|
133 |
property for @{text "P minusinfinity"} *} |
|
13876 | 134 |
|
135 |
theorem modd_minf_conjI: "\<forall>(x::int) k. A x = A (x-k*d) \<Longrightarrow> |
|
136 |
\<forall>(x::int) k. B x = B (x-k*d) \<Longrightarrow> |
|
137 |
\<forall>(x::int) (k::int). (A x \<and> B x) = (A (x-k*d) \<and> B (x-k*d))" |
|
138 |
by simp |
|
139 |
||
140 |
theorem modd_minf_disjI: "\<forall>(x::int) k. A x = A (x-k*d) \<Longrightarrow> |
|
141 |
\<forall>(x::int) k. B x = B (x-k*d) \<Longrightarrow> |
|
142 |
\<forall>(x::int) (k::int). (A x \<or> B x) = (A (x-k*d) \<or> B (x-k*d))" |
|
143 |
by simp |
|
144 |
||
14577 | 145 |
text {* |
146 |
This is one of the cases where the simplifed formula is prooved to |
|
147 |
have some property (in relation to @{text P_m}) but we need to |
|
148 |
prove the property for the original formula (@{text P_m}). *} |
|
13876 | 149 |
|
150 |
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)) " |
|
14577 | 151 |
by blast |
13876 | 152 |
|
14577 | 153 |
text {* |
154 |
Theorem needed for proving at runtime divide properties using the |
|
155 |
arithmetic tactic (which knows only about modulo = 0). *} |
|
13876 | 156 |
|
157 |
lemma zdvd_iff_zmod_eq_0: "(m dvd n) = (n mod m = (0::int))" |
|
14577 | 158 |
by(simp add:dvd_def zmod_eq_0_iff) |
13876 | 159 |
|
14577 | 160 |
text {* |
161 |
\medskip Theorems used for the combination of proof for the |
|
162 |
backwards direction of Cooper's Theorem. They rely exclusively on |
|
163 |
Predicate calculus.*} |
|
13876 | 164 |
|
165 |
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)) |
|
166 |
==> |
|
167 |
(ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a - j)) --> P2(x) --> P2(x + d)) |
|
168 |
==> |
|
169 |
(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))) " |
|
14577 | 170 |
by blast |
13876 | 171 |
|
172 |
||
173 |
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)) |
|
174 |
==> |
|
175 |
(ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a - j)) --> P2(x) --> P2(x + d)) |
|
176 |
==> |
|
177 |
(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) |
|
178 |
\<and> P2(x + d))) " |
|
14577 | 179 |
by blast |
13876 | 180 |
|
181 |
lemma not_ast_p_Q_elim: " |
|
182 |
(ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a - j)) -->P(x) --> P(x + d)) |
|
183 |
==> ( P = Q ) |
|
184 |
==> (ALL x. ~(EX (j::int) : {1..d}. EX (a::int) : A. P(a - j)) -->P(x) --> P(x + d))" |
|
14577 | 185 |
by blast |
13876 | 186 |
|
14577 | 187 |
text {* |
188 |
\medskip Theorems used for the combination of proof for the |
|
189 |
backwards direction of Cooper's Theorem. They rely exclusively on |
|
190 |
Predicate calculus.*} |
|
13876 | 191 |
|
192 |
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)) |
|
193 |
==> |
|
194 |
(ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (b::int) : B. Q(b+j)) --> P2(x) --> P2(x - d)) |
|
195 |
==> |
|
196 |
(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) |
|
197 |
\<or> P2(x-d))) " |
|
14577 | 198 |
by blast |
13876 | 199 |
|
200 |
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)) |
|
201 |
==> |
|
202 |
(ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (b::int) : B. Q(b+j)) --> P2(x) --> P2(x - d)) |
|
203 |
==> |
|
204 |
(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) |
|
205 |
\<and> P2(x-d))) " |
|
14577 | 206 |
by blast |
13876 | 207 |
|
208 |
lemma not_bst_p_Q_elim: " |
|
209 |
(ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (b::int) : B. Q(b+j)) -->P(x) --> P(x - d)) |
|
210 |
==> ( P = Q ) |
|
211 |
==> (ALL x. ~(EX (j::int) : {1..d}. EX (b::int) : B. P(b+j)) -->P(x) --> P(x - d))" |
|
14577 | 212 |
by blast |
13876 | 213 |
|
14577 | 214 |
text {* \medskip This is the first direction of Cooper's Theorem. *} |
13876 | 215 |
lemma cooper_thm: "(R --> (EX x::int. P x)) ==> (Q -->(EX x::int. P x )) ==> ((R|Q) --> (EX x::int. P x )) " |
14577 | 216 |
by blast |
13876 | 217 |
|
14577 | 218 |
text {* |
219 |
\medskip The full Cooper's Theorem in its equivalence Form. Given |
|
220 |
the premises it is trivial too, it relies exclusively on prediacte calculus.*} |
|
13876 | 221 |
lemma cooper_eq_thm: "(R --> (EX x::int. P x)) ==> (Q -->(EX x::int. P x )) ==> ((~Q) |
222 |
--> (EX x::int. P x ) --> R) ==> (EX x::int. P x) = R|Q " |
|
14577 | 223 |
by blast |
13876 | 224 |
|
14577 | 225 |
text {* |
226 |
\medskip Some of the atomic theorems generated each time the atom |
|
227 |
does not depend on @{text x}, they are trivial.*} |
|
13876 | 228 |
|
229 |
lemma fm_eq_minf: "EX z::int. ALL x. x < z --> (P = P) " |
|
14577 | 230 |
by blast |
13876 | 231 |
|
232 |
lemma fm_modd_minf: "ALL (x::int). ALL (k::int). (P = P)" |
|
14577 | 233 |
by blast |
13876 | 234 |
|
235 |
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" |
|
14577 | 236 |
by blast |
13876 | 237 |
|
238 |
lemma fm_eq_pinf: "EX z::int. ALL x. z < x --> (P = P) " |
|
14577 | 239 |
by blast |
13876 | 240 |
|
14577 | 241 |
text {* The next two thms are the same as the @{text minusinf} version. *} |
242 |
||
13876 | 243 |
lemma fm_modd_pinf: "ALL (x::int). ALL (k::int). (P = P)" |
14577 | 244 |
by blast |
13876 | 245 |
|
246 |
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" |
|
14577 | 247 |
by blast |
13876 | 248 |
|
14577 | 249 |
text {* Theorems to be deleted from simpset when proving simplified formulaes. *} |
13876 | 250 |
|
251 |
lemma P_eqtrue: "(P=True) = P" |
|
17589 | 252 |
by iprover |
13876 | 253 |
|
254 |
lemma P_eqfalse: "(P=False) = (~P)" |
|
17589 | 255 |
by iprover |
13876 | 256 |
|
14577 | 257 |
text {* |
258 |
\medskip Theorems for the generation of the bachwards direction of |
|
259 |
Cooper's Theorem. |
|
13876 | 260 |
|
14577 | 261 |
These are the 6 interesting atomic cases which have to be proved relying on the |
262 |
properties of B-set and the arithmetic and contradiction proofs. *} |
|
13876 | 263 |
|
264 |
lemma not_bst_p_lt: "0 < (d::int) ==> |
|
265 |
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 )" |
|
14577 | 266 |
by arith |
13876 | 267 |
|
268 |
lemma not_bst_p_gt: "\<lbrakk> (g::int) \<in> B; g = -a \<rbrakk> \<Longrightarrow> |
|
269 |
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)" |
|
270 |
apply clarsimp |
|
271 |
apply(rule ccontr) |
|
272 |
apply(drule_tac x = "x+a" in bspec) |
|
273 |
apply(simp add:atLeastAtMost_iff) |
|
274 |
apply(drule_tac x = "-a" in bspec) |
|
275 |
apply assumption |
|
276 |
apply(simp) |
|
277 |
done |
|
278 |
||
279 |
lemma not_bst_p_eq: "\<lbrakk> 0 < d; (g::int) \<in> B; g = -a - 1 \<rbrakk> \<Longrightarrow> |
|
280 |
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 )" |
|
281 |
apply clarsimp |
|
282 |
apply(subgoal_tac "x = -a") |
|
283 |
prefer 2 apply arith |
|
284 |
apply(drule_tac x = "1" in bspec) |
|
285 |
apply(simp add:atLeastAtMost_iff) |
|
286 |
apply(drule_tac x = "-a- 1" in bspec) |
|
287 |
apply assumption |
|
288 |
apply(simp) |
|
289 |
done |
|
290 |
||
291 |
||
292 |
lemma not_bst_p_ne: "\<lbrakk> 0 < d; (g::int) \<in> B; g = -a \<rbrakk> \<Longrightarrow> |
|
293 |
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)" |
|
294 |
apply clarsimp |
|
295 |
apply(subgoal_tac "x = -a+d") |
|
296 |
prefer 2 apply arith |
|
297 |
apply(drule_tac x = "d" in bspec) |
|
298 |
apply(simp add:atLeastAtMost_iff) |
|
299 |
apply(drule_tac x = "-a" in bspec) |
|
300 |
apply assumption |
|
301 |
apply(simp) |
|
302 |
done |
|
303 |
||
304 |
||
305 |
lemma not_bst_p_dvd: "(d1::int) dvd d ==> |
|
306 |
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 )" |
|
307 |
apply(clarsimp simp add:dvd_def) |
|
308 |
apply(rename_tac m) |
|
309 |
apply(rule_tac x = "m - k" in exI) |
|
310 |
apply(simp add:int_distrib) |
|
311 |
done |
|
312 |
||
313 |
lemma not_bst_p_ndvd: "(d1::int) dvd d ==> |
|
314 |
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 ))" |
|
315 |
apply(clarsimp simp add:dvd_def) |
|
316 |
apply(rename_tac m) |
|
317 |
apply(erule_tac x = "m + k" in allE) |
|
318 |
apply(simp add:int_distrib) |
|
319 |
done |
|
320 |
||
14577 | 321 |
text {* |
322 |
\medskip Theorems for the generation of the bachwards direction of |
|
323 |
Cooper's Theorem. |
|
13876 | 324 |
|
14577 | 325 |
These are the 6 interesting atomic cases which have to be proved |
326 |
relying on the properties of A-set ant the arithmetic and |
|
327 |
contradiction proofs. *} |
|
13876 | 328 |
|
329 |
lemma not_ast_p_gt: "0 < (d::int) ==> |
|
330 |
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 )" |
|
14577 | 331 |
by arith |
13876 | 332 |
|
333 |
lemma not_ast_p_lt: "\<lbrakk>0 < d ;(t::int) \<in> A \<rbrakk> \<Longrightarrow> |
|
334 |
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)" |
|
335 |
apply clarsimp |
|
336 |
apply (rule ccontr) |
|
337 |
apply (drule_tac x = "t-x" in bspec) |
|
338 |
apply simp |
|
339 |
apply (drule_tac x = "t" in bspec) |
|
340 |
apply assumption |
|
341 |
apply simp |
|
342 |
done |
|
343 |
||
344 |
lemma not_ast_p_eq: "\<lbrakk> 0 < d; (g::int) \<in> A; g = -t + 1 \<rbrakk> \<Longrightarrow> |
|
345 |
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 )" |
|
346 |
apply clarsimp |
|
347 |
apply (drule_tac x="1" in bspec) |
|
348 |
apply simp |
|
349 |
apply (drule_tac x="- t + 1" in bspec) |
|
350 |
apply assumption |
|
351 |
apply(subgoal_tac "x = -t") |
|
352 |
prefer 2 apply arith |
|
353 |
apply simp |
|
354 |
done |
|
355 |
||
356 |
lemma not_ast_p_ne: "\<lbrakk> 0 < d; (g::int) \<in> A; g = -t \<rbrakk> \<Longrightarrow> |
|
357 |
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)" |
|
358 |
apply clarsimp |
|
359 |
apply (subgoal_tac "x = -t-d") |
|
360 |
prefer 2 apply arith |
|
361 |
apply (drule_tac x = "d" in bspec) |
|
362 |
apply simp |
|
363 |
apply (drule_tac x = "-t" in bspec) |
|
364 |
apply assumption |
|
365 |
apply simp |
|
366 |
done |
|
367 |
||
368 |
lemma not_ast_p_dvd: "(d1::int) dvd d ==> |
|
369 |
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 )" |
|
370 |
apply(clarsimp simp add:dvd_def) |
|
371 |
apply(rename_tac m) |
|
372 |
apply(rule_tac x = "m + k" in exI) |
|
373 |
apply(simp add:int_distrib) |
|
374 |
done |
|
375 |
||
376 |
lemma not_ast_p_ndvd: "(d1::int) dvd d ==> |
|
377 |
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 ))" |
|
378 |
apply(clarsimp simp add:dvd_def) |
|
379 |
apply(rename_tac m) |
|
380 |
apply(erule_tac x = "m - k" in allE) |
|
381 |
apply(simp add:int_distrib) |
|
382 |
done |
|
383 |
||
14577 | 384 |
text {* |
385 |
\medskip These are the atomic cases for the proof generation for the |
|
386 |
modulo @{text D} property for @{text "P plusinfinity"} |
|
13876 | 387 |
|
14577 | 388 |
They are fully based on arithmetics. *} |
13876 | 389 |
|
390 |
lemma dvd_modd_pinf: "((d::int) dvd d1) ==> |
|
391 |
(ALL (x::int). ALL (k::int). (((d::int) dvd (x + t)) = (d dvd (x+k*d1 + t))))" |
|
392 |
apply(clarsimp simp add:dvd_def) |
|
393 |
apply(rule iffI) |
|
394 |
apply(clarsimp) |
|
395 |
apply(rename_tac n m) |
|
396 |
apply(rule_tac x = "m + n*k" in exI) |
|
397 |
apply(simp add:int_distrib) |
|
398 |
apply(clarsimp) |
|
399 |
apply(rename_tac n m) |
|
400 |
apply(rule_tac x = "m - n*k" in exI) |
|
14271 | 401 |
apply(simp add:int_distrib mult_ac) |
13876 | 402 |
done |
403 |
||
404 |
lemma not_dvd_modd_pinf: "((d::int) dvd d1) ==> |
|
405 |
(ALL (x::int). ALL k. (~((d::int) dvd (x + t))) = (~(d dvd (x+k*d1 + t))))" |
|
406 |
apply(clarsimp simp add:dvd_def) |
|
407 |
apply(rule iffI) |
|
408 |
apply(clarsimp) |
|
409 |
apply(rename_tac n m) |
|
410 |
apply(erule_tac x = "m - n*k" in allE) |
|
14271 | 411 |
apply(simp add:int_distrib mult_ac) |
13876 | 412 |
apply(clarsimp) |
413 |
apply(rename_tac n m) |
|
414 |
apply(erule_tac x = "m + n*k" in allE) |
|
14271 | 415 |
apply(simp add:int_distrib mult_ac) |
13876 | 416 |
done |
417 |
||
14577 | 418 |
text {* |
419 |
\medskip These are the atomic cases for the proof generation for the |
|
420 |
equivalence of @{text P} and @{text "P plusinfinity"} for integers |
|
421 |
@{text x} greater than some integer @{text z}. |
|
422 |
||
423 |
They are fully based on arithmetics. *} |
|
13876 | 424 |
|
425 |
lemma eq_eq_pinf: "EX z::int. ALL x. z < x --> (( 0 = x +t ) = False )" |
|
426 |
apply(rule_tac x = "-t" in exI) |
|
427 |
apply simp |
|
428 |
done |
|
429 |
||
430 |
lemma neq_eq_pinf: "EX z::int. ALL x. z < x --> ((~( 0 = x +t )) = True )" |
|
431 |
apply(rule_tac x = "-t" in exI) |
|
432 |
apply simp |
|
433 |
done |
|
434 |
||
435 |
lemma le_eq_pinf: "EX z::int. ALL x. z < x --> ( 0 < x +t = True )" |
|
436 |
apply(rule_tac x = "-t" in exI) |
|
437 |
apply simp |
|
438 |
done |
|
439 |
||
440 |
lemma len_eq_pinf: "EX z::int. ALL x. z < x --> (0 < -x +t = False )" |
|
441 |
apply(rule_tac x = "t" in exI) |
|
442 |
apply simp |
|
443 |
done |
|
444 |
||
445 |
lemma dvd_eq_pinf: "EX z::int. ALL x. z < x --> ((d dvd (x + t)) = (d dvd (x + t))) " |
|
14577 | 446 |
by simp |
13876 | 447 |
|
448 |
lemma not_dvd_eq_pinf: "EX z::int. ALL x. z < x --> ((~(d dvd (x + t))) = (~(d dvd (x + t)))) " |
|
14577 | 449 |
by simp |
13876 | 450 |
|
14577 | 451 |
text {* |
452 |
\medskip These are the atomic cases for the proof generation for the |
|
453 |
modulo @{text D} property for @{text "P minusinfinity"}. |
|
454 |
||
455 |
They are fully based on arithmetics. *} |
|
13876 | 456 |
|
457 |
lemma dvd_modd_minf: "((d::int) dvd d1) ==> |
|
458 |
(ALL (x::int). ALL (k::int). (((d::int) dvd (x + t)) = (d dvd (x-k*d1 + t))))" |
|
459 |
apply(clarsimp simp add:dvd_def) |
|
460 |
apply(rule iffI) |
|
461 |
apply(clarsimp) |
|
462 |
apply(rename_tac n m) |
|
463 |
apply(rule_tac x = "m - n*k" in exI) |
|
464 |
apply(simp add:int_distrib) |
|
465 |
apply(clarsimp) |
|
466 |
apply(rename_tac n m) |
|
467 |
apply(rule_tac x = "m + n*k" in exI) |
|
14271 | 468 |
apply(simp add:int_distrib mult_ac) |
13876 | 469 |
done |
470 |
||
471 |
||
472 |
lemma not_dvd_modd_minf: "((d::int) dvd d1) ==> |
|
473 |
(ALL (x::int). ALL k. (~((d::int) dvd (x + t))) = (~(d dvd (x-k*d1 + t))))" |
|
474 |
apply(clarsimp simp add:dvd_def) |
|
475 |
apply(rule iffI) |
|
476 |
apply(clarsimp) |
|
477 |
apply(rename_tac n m) |
|
478 |
apply(erule_tac x = "m + n*k" in allE) |
|
14271 | 479 |
apply(simp add:int_distrib mult_ac) |
13876 | 480 |
apply(clarsimp) |
481 |
apply(rename_tac n m) |
|
482 |
apply(erule_tac x = "m - n*k" in allE) |
|
14271 | 483 |
apply(simp add:int_distrib mult_ac) |
13876 | 484 |
done |
485 |
||
14577 | 486 |
text {* |
487 |
\medskip These are the atomic cases for the proof generation for the |
|
488 |
equivalence of @{text P} and @{text "P minusinfinity"} for integers |
|
489 |
@{text x} less than some integer @{text z}. |
|
13876 | 490 |
|
14577 | 491 |
They are fully based on arithmetics. *} |
13876 | 492 |
|
493 |
lemma eq_eq_minf: "EX z::int. ALL x. x < z --> (( 0 = x +t ) = False )" |
|
494 |
apply(rule_tac x = "-t" in exI) |
|
495 |
apply simp |
|
496 |
done |
|
497 |
||
498 |
lemma neq_eq_minf: "EX z::int. ALL x. x < z --> ((~( 0 = x +t )) = True )" |
|
499 |
apply(rule_tac x = "-t" in exI) |
|
500 |
apply simp |
|
501 |
done |
|
502 |
||
503 |
lemma le_eq_minf: "EX z::int. ALL x. x < z --> ( 0 < x +t = False )" |
|
504 |
apply(rule_tac x = "-t" in exI) |
|
505 |
apply simp |
|
506 |
done |
|
507 |
||
508 |
||
509 |
lemma len_eq_minf: "EX z::int. ALL x. x < z --> (0 < -x +t = True )" |
|
510 |
apply(rule_tac x = "t" in exI) |
|
511 |
apply simp |
|
512 |
done |
|
513 |
||
514 |
lemma dvd_eq_minf: "EX z::int. ALL x. x < z --> ((d dvd (x + t)) = (d dvd (x + t))) " |
|
14577 | 515 |
by simp |
13876 | 516 |
|
517 |
lemma not_dvd_eq_minf: "EX z::int. ALL x. x < z --> ((~(d dvd (x + t))) = (~(d dvd (x + t)))) " |
|
14577 | 518 |
by simp |
13876 | 519 |
|
14577 | 520 |
text {* |
521 |
\medskip This Theorem combines whithnesses about @{text "P |
|
522 |
minusinfinity"} to show one component of the equivalence proof for |
|
523 |
Cooper's Theorem. |
|
13876 | 524 |
|
14577 | 525 |
FIXME: remove once they are part of the distribution. *} |
526 |
||
13876 | 527 |
theorem int_ge_induct[consumes 1,case_names base step]: |
528 |
assumes ge: "k \<le> (i::int)" and |
|
529 |
base: "P(k)" and |
|
530 |
step: "\<And>i. \<lbrakk>k \<le> i; P i\<rbrakk> \<Longrightarrow> P(i+1)" |
|
531 |
shows "P i" |
|
532 |
proof - |
|
533 |
{ fix n have "\<And>i::int. n = nat(i-k) \<Longrightarrow> k <= i \<Longrightarrow> P i" |
|
534 |
proof (induct n) |
|
535 |
case 0 |
|
536 |
hence "i = k" by arith |
|
537 |
thus "P i" using base by simp |
|
538 |
next |
|
539 |
case (Suc n) |
|
540 |
hence "n = nat((i - 1) - k)" by arith |
|
541 |
moreover |
|
542 |
have ki1: "k \<le> i - 1" using Suc.prems by arith |
|
543 |
ultimately |
|
544 |
have "P(i - 1)" by(rule Suc.hyps) |
|
545 |
from step[OF ki1 this] show ?case by simp |
|
546 |
qed |
|
547 |
} |
|
548 |
from this ge show ?thesis by fast |
|
549 |
qed |
|
550 |
||
551 |
theorem int_gr_induct[consumes 1,case_names base step]: |
|
552 |
assumes gr: "k < (i::int)" and |
|
553 |
base: "P(k+1)" and |
|
554 |
step: "\<And>i. \<lbrakk>k < i; P i\<rbrakk> \<Longrightarrow> P(i+1)" |
|
555 |
shows "P i" |
|
556 |
apply(rule int_ge_induct[of "k + 1"]) |
|
557 |
using gr apply arith |
|
558 |
apply(rule base) |
|
559 |
apply(rule step) |
|
560 |
apply simp+ |
|
561 |
done |
|
562 |
||
563 |
lemma decr_lemma: "0 < (d::int) \<Longrightarrow> x - (abs(x-z)+1) * d < z" |
|
564 |
apply(induct rule: int_gr_induct) |
|
565 |
apply simp |
|
566 |
apply (simp add:int_distrib) |
|
567 |
done |
|
568 |
||
569 |
lemma incr_lemma: "0 < (d::int) \<Longrightarrow> z < x + (abs(x-z)+1) * d" |
|
570 |
apply(induct rule: int_gr_induct) |
|
571 |
apply simp |
|
572 |
apply (simp add:int_distrib) |
|
573 |
done |
|
574 |
||
575 |
lemma minusinfinity: |
|
576 |
assumes "0 < d" and |
|
577 |
P1eqP1: "ALL x k. P1 x = P1(x - k*d)" and |
|
578 |
ePeqP1: "EX z::int. ALL x. x < z \<longrightarrow> (P x = P1 x)" |
|
579 |
shows "(EX x. P1 x) \<longrightarrow> (EX x. P x)" |
|
580 |
proof |
|
581 |
assume eP1: "EX x. P1 x" |
|
582 |
then obtain x where P1: "P1 x" .. |
|
583 |
from ePeqP1 obtain z where P1eqP: "ALL x. x < z \<longrightarrow> (P x = P1 x)" .. |
|
584 |
let ?w = "x - (abs(x-z)+1) * d" |
|
585 |
show "EX x. P x" |
|
586 |
proof |
|
587 |
have w: "?w < z" by(rule decr_lemma) |
|
588 |
have "P1 x = P1 ?w" using P1eqP1 by blast |
|
589 |
also have "\<dots> = P(?w)" using w P1eqP by blast |
|
590 |
finally show "P ?w" using P1 by blast |
|
591 |
qed |
|
592 |
qed |
|
593 |
||
14577 | 594 |
text {* |
595 |
\medskip This Theorem combines whithnesses about @{text "P |
|
596 |
minusinfinity"} to show one component of the equivalence proof for |
|
597 |
Cooper's Theorem. *} |
|
13876 | 598 |
|
599 |
lemma plusinfinity: |
|
600 |
assumes "0 < d" and |
|
601 |
P1eqP1: "ALL (x::int) (k::int). P1 x = P1 (x + k * d)" and |
|
602 |
ePeqP1: "EX z::int. ALL x. z < x --> (P x = P1 x)" |
|
603 |
shows "(EX x::int. P1 x) --> (EX x::int. P x)" |
|
604 |
proof |
|
605 |
assume eP1: "EX x. P1 x" |
|
606 |
then obtain x where P1: "P1 x" .. |
|
607 |
from ePeqP1 obtain z where P1eqP: "ALL x. z < x \<longrightarrow> (P x = P1 x)" .. |
|
608 |
let ?w = "x + (abs(x-z)+1) * d" |
|
609 |
show "EX x. P x" |
|
610 |
proof |
|
611 |
have w: "z < ?w" by(rule incr_lemma) |
|
612 |
have "P1 x = P1 ?w" using P1eqP1 by blast |
|
613 |
also have "\<dots> = P(?w)" using w P1eqP by blast |
|
614 |
finally show "P ?w" using P1 by blast |
|
615 |
qed |
|
616 |
qed |
|
617 |
||
14577 | 618 |
text {* |
619 |
\medskip Theorem for periodic function on discrete sets. *} |
|
13876 | 620 |
|
621 |
lemma minf_vee: |
|
622 |
assumes dpos: "(0::int) < d" and modd: "ALL x k. P x = P(x - k*d)" |
|
623 |
shows "(EX x. P x) = (EX j : {1..d}. P j)" |
|
624 |
(is "?LHS = ?RHS") |
|
625 |
proof |
|
626 |
assume ?LHS |
|
627 |
then obtain x where P: "P x" .. |
|
628 |
have "x mod d = x - (x div d)*d" |
|
14271 | 629 |
by(simp add:zmod_zdiv_equality mult_ac eq_diff_eq) |
13876 | 630 |
hence Pmod: "P x = P(x mod d)" using modd by simp |
631 |
show ?RHS |
|
632 |
proof (cases) |
|
633 |
assume "x mod d = 0" |
|
634 |
hence "P 0" using P Pmod by simp |
|
635 |
moreover have "P 0 = P(0 - (-1)*d)" using modd by blast |
|
636 |
ultimately have "P d" by simp |
|
637 |
moreover have "d : {1..d}" using dpos by(simp add:atLeastAtMost_iff) |
|
638 |
ultimately show ?RHS .. |
|
639 |
next |
|
640 |
assume not0: "x mod d \<noteq> 0" |
|
641 |
have "P(x mod d)" using dpos P Pmod by(simp add:pos_mod_sign pos_mod_bound) |
|
642 |
moreover have "x mod d : {1..d}" |
|
643 |
proof - |
|
644 |
have "0 \<le> x mod d" by(rule pos_mod_sign) |
|
645 |
moreover have "x mod d < d" by(rule pos_mod_bound) |
|
646 |
ultimately show ?thesis using not0 by(simp add:atLeastAtMost_iff) |
|
647 |
qed |
|
648 |
ultimately show ?RHS .. |
|
649 |
qed |
|
650 |
next |
|
651 |
assume ?RHS thus ?LHS by blast |
|
652 |
qed |
|
653 |
||
14577 | 654 |
text {* |
655 |
\medskip Theorem for periodic function on discrete sets. *} |
|
656 |
||
13876 | 657 |
lemma pinf_vee: |
658 |
assumes dpos: "0 < (d::int)" and modd: "ALL (x::int) (k::int). P x = P (x+k*d)" |
|
659 |
shows "(EX x::int. P x) = (EX (j::int) : {1..d} . P j)" |
|
660 |
(is "?LHS = ?RHS") |
|
661 |
proof |
|
662 |
assume ?LHS |
|
663 |
then obtain x where P: "P x" .. |
|
664 |
have "x mod d = x + (-(x div d))*d" |
|
14271 | 665 |
by(simp add:zmod_zdiv_equality mult_ac eq_diff_eq) |
13876 | 666 |
hence Pmod: "P x = P(x mod d)" using modd by (simp only:) |
667 |
show ?RHS |
|
668 |
proof (cases) |
|
669 |
assume "x mod d = 0" |
|
670 |
hence "P 0" using P Pmod by simp |
|
671 |
moreover have "P 0 = P(0 + 1*d)" using modd by blast |
|
672 |
ultimately have "P d" by simp |
|
673 |
moreover have "d : {1..d}" using dpos by(simp add:atLeastAtMost_iff) |
|
674 |
ultimately show ?RHS .. |
|
675 |
next |
|
676 |
assume not0: "x mod d \<noteq> 0" |
|
677 |
have "P(x mod d)" using dpos P Pmod by(simp add:pos_mod_sign pos_mod_bound) |
|
678 |
moreover have "x mod d : {1..d}" |
|
679 |
proof - |
|
680 |
have "0 \<le> x mod d" by(rule pos_mod_sign) |
|
681 |
moreover have "x mod d < d" by(rule pos_mod_bound) |
|
682 |
ultimately show ?thesis using not0 by(simp add:atLeastAtMost_iff) |
|
683 |
qed |
|
684 |
ultimately show ?RHS .. |
|
685 |
qed |
|
686 |
next |
|
687 |
assume ?RHS thus ?LHS by blast |
|
688 |
qed |
|
689 |
||
690 |
lemma decr_mult_lemma: |
|
691 |
assumes dpos: "(0::int) < d" and |
|
692 |
minus: "ALL x::int. P x \<longrightarrow> P(x - d)" and |
|
693 |
knneg: "0 <= k" |
|
694 |
shows "ALL x. P x \<longrightarrow> P(x - k*d)" |
|
695 |
using knneg |
|
696 |
proof (induct rule:int_ge_induct) |
|
697 |
case base thus ?case by simp |
|
698 |
next |
|
699 |
case (step i) |
|
700 |
show ?case |
|
701 |
proof |
|
702 |
fix x |
|
703 |
have "P x \<longrightarrow> P (x - i * d)" using step.hyps by blast |
|
704 |
also have "\<dots> \<longrightarrow> P(x - (i + 1) * d)" |
|
705 |
using minus[THEN spec, of "x - i * d"] |
|
14738 | 706 |
by (simp add:int_distrib OrderedGroup.diff_diff_eq[symmetric]) |
13876 | 707 |
ultimately show "P x \<longrightarrow> P(x - (i + 1) * d)" by blast |
708 |
qed |
|
709 |
qed |
|
710 |
||
711 |
lemma incr_mult_lemma: |
|
712 |
assumes dpos: "(0::int) < d" and |
|
713 |
plus: "ALL x::int. P x \<longrightarrow> P(x + d)" and |
|
714 |
knneg: "0 <= k" |
|
715 |
shows "ALL x. P x \<longrightarrow> P(x + k*d)" |
|
716 |
using knneg |
|
717 |
proof (induct rule:int_ge_induct) |
|
718 |
case base thus ?case by simp |
|
719 |
next |
|
720 |
case (step i) |
|
721 |
show ?case |
|
722 |
proof |
|
723 |
fix x |
|
724 |
have "P x \<longrightarrow> P (x + i * d)" using step.hyps by blast |
|
725 |
also have "\<dots> \<longrightarrow> P(x + (i + 1) * d)" |
|
726 |
using plus[THEN spec, of "x + i * d"] |
|
727 |
by (simp add:int_distrib zadd_ac) |
|
728 |
ultimately show "P x \<longrightarrow> P(x + (i + 1) * d)" by blast |
|
729 |
qed |
|
730 |
qed |
|
731 |
||
732 |
lemma cpmi_eq: "0 < D \<Longrightarrow> (EX z::int. ALL x. x < z --> (P x = P1 x)) |
|
733 |
==> ALL x.~(EX (j::int) : {1..D}. EX (b::int) : B. P(b+j)) --> P (x) --> P (x - D) |
|
734 |
==> (ALL (x::int). ALL (k::int). ((P1 x)= (P1 (x-k*D)))) |
|
735 |
==> (EX (x::int). P(x)) = ((EX (j::int) : {1..D} . (P1(j))) | (EX (j::int) : {1..D}. EX (b::int) : B. P (b+j)))" |
|
736 |
apply(rule iffI) |
|
737 |
prefer 2 |
|
738 |
apply(drule minusinfinity) |
|
739 |
apply assumption+ |
|
740 |
apply(fastsimp) |
|
741 |
apply clarsimp |
|
742 |
apply(subgoal_tac "!!k. 0<=k \<Longrightarrow> !x. P x \<longrightarrow> P (x - k*D)") |
|
743 |
apply(frule_tac x = x and z=z in decr_lemma) |
|
744 |
apply(subgoal_tac "P1(x - (\<bar>x - z\<bar> + 1) * D)") |
|
745 |
prefer 2 |
|
746 |
apply(subgoal_tac "0 <= (\<bar>x - z\<bar> + 1)") |
|
747 |
prefer 2 apply arith |
|
748 |
apply fastsimp |
|
749 |
apply(drule (1) minf_vee) |
|
750 |
apply blast |
|
751 |
apply(blast dest:decr_mult_lemma) |
|
752 |
done |
|
753 |
||
14577 | 754 |
text {* Cooper Theorem, plus infinity version. *} |
13876 | 755 |
lemma cppi_eq: "0 < D \<Longrightarrow> (EX z::int. ALL x. z < x --> (P x = P1 x)) |
756 |
==> ALL x.~(EX (j::int) : {1..D}. EX (a::int) : A. P(a - j)) --> P (x) --> P (x + D) |
|
757 |
==> (ALL (x::int). ALL (k::int). ((P1 x)= (P1 (x+k*D)))) |
|
758 |
==> (EX (x::int). P(x)) = ((EX (j::int) : {1..D} . (P1(j))) | (EX (j::int) : {1..D}. EX (a::int) : A. P (a - j)))" |
|
759 |
apply(rule iffI) |
|
760 |
prefer 2 |
|
761 |
apply(drule plusinfinity) |
|
762 |
apply assumption+ |
|
763 |
apply(fastsimp) |
|
764 |
apply clarsimp |
|
765 |
apply(subgoal_tac "!!k. 0<=k \<Longrightarrow> !x. P x \<longrightarrow> P (x + k*D)") |
|
766 |
apply(frule_tac x = x and z=z in incr_lemma) |
|
767 |
apply(subgoal_tac "P1(x + (\<bar>x - z\<bar> + 1) * D)") |
|
768 |
prefer 2 |
|
769 |
apply(subgoal_tac "0 <= (\<bar>x - z\<bar> + 1)") |
|
770 |
prefer 2 apply arith |
|
771 |
apply fastsimp |
|
772 |
apply(drule (1) pinf_vee) |
|
773 |
apply blast |
|
774 |
apply(blast dest:incr_mult_lemma) |
|
775 |
done |
|
776 |
||
777 |
||
14577 | 778 |
text {* |
779 |
\bigskip Theorems for the quantifier elminination Functions. *} |
|
13876 | 780 |
|
781 |
lemma qe_ex_conj: "(EX (x::int). A x) = R |
|
782 |
==> (EX (x::int). P x) = (Q & (EX x::int. A x)) |
|
783 |
==> (EX (x::int). P x) = (Q & R)" |
|
784 |
by blast |
|
785 |
||
786 |
lemma qe_ex_nconj: "(EX (x::int). P x) = (True & Q) |
|
787 |
==> (EX (x::int). P x) = Q" |
|
788 |
by blast |
|
789 |
||
790 |
lemma qe_conjI: "P1 = P2 ==> Q1 = Q2 ==> (P1 & Q1) = (P2 & Q2)" |
|
791 |
by blast |
|
792 |
||
793 |
lemma qe_disjI: "P1 = P2 ==> Q1 = Q2 ==> (P1 | Q1) = (P2 | Q2)" |
|
794 |
by blast |
|
795 |
||
796 |
lemma qe_impI: "P1 = P2 ==> Q1 = Q2 ==> (P1 --> Q1) = (P2 --> Q2)" |
|
797 |
by blast |
|
798 |
||
799 |
lemma qe_eqI: "P1 = P2 ==> Q1 = Q2 ==> (P1 = Q1) = (P2 = Q2)" |
|
800 |
by blast |
|
801 |
||
802 |
lemma qe_Not: "P = Q ==> (~P) = (~Q)" |
|
803 |
by blast |
|
804 |
||
805 |
lemma qe_ALL: "(EX x. ~P x) = R ==> (ALL x. P x) = (~R)" |
|
806 |
by blast |
|
807 |
||
14577 | 808 |
text {* \bigskip Theorems for proving NNF *} |
13876 | 809 |
|
810 |
lemma nnf_im: "((~P) = P1) ==> (Q=Q1) ==> ((P --> Q) = (P1 | Q1))" |
|
811 |
by blast |
|
812 |
||
813 |
lemma nnf_eq: "((P & Q) = (P1 & Q1)) ==> (((~P) & (~Q)) = (P2 & Q2)) ==> ((P = Q) = ((P1 & Q1)|(P2 & Q2)))" |
|
814 |
by blast |
|
815 |
||
816 |
lemma nnf_nn: "(P = Q) ==> ((~~P) = Q)" |
|
817 |
by blast |
|
818 |
lemma nnf_ncj: "((~P) = P1) ==> ((~Q) = Q1) ==> ((~(P & Q)) = (P1 | Q1))" |
|
819 |
by blast |
|
820 |
||
821 |
lemma nnf_ndj: "((~P) = P1) ==> ((~Q) = Q1) ==> ((~(P | Q)) = (P1 & Q1))" |
|
822 |
by blast |
|
823 |
lemma nnf_nim: "(P = P1) ==> ((~Q) = Q1) ==> ((~(P --> Q)) = (P1 & Q1))" |
|
824 |
by blast |
|
825 |
lemma nnf_neq: "((P & (~Q)) = (P1 & Q1)) ==> (((~P) & Q) = (P2 & Q2)) ==> ((~(P = Q)) = ((P1 & Q1)|(P2 & Q2)))" |
|
826 |
by blast |
|
827 |
lemma nnf_sdj: "((A & (~B)) = (A1 & B1)) ==> ((C & (~D)) = (C1 & D1)) ==> (A = (~C)) ==> ((~((A & B) | (C & D))) = ((A1 & B1) | (C1 & D1)))" |
|
828 |
by blast |
|
829 |
||
830 |
||
831 |
lemma qe_exI2: "A = B ==> (EX (x::int). A(x)) = (EX (x::int). B(x))" |
|
832 |
by simp |
|
833 |
||
834 |
lemma qe_exI: "(!!x::int. A x = B x) ==> (EX (x::int). A(x)) = (EX (x::int). B(x))" |
|
17589 | 835 |
by iprover |
13876 | 836 |
|
837 |
lemma qe_ALLI: "(!!x::int. A x = B x) ==> (ALL (x::int). A(x)) = (ALL (x::int). B(x))" |
|
17589 | 838 |
by iprover |
13876 | 839 |
|
840 |
lemma cp_expand: "(EX (x::int). P (x)) = (EX (j::int) : {1..d}. EX (b::int) : B. (P1 (j) | P(b+j))) |
|
841 |
==>(EX (x::int). P (x)) = (EX (j::int) : {1..d}. EX (b::int) : B. (P1 (j) | P(b+j))) " |
|
842 |
by blast |
|
843 |
||
844 |
lemma cppi_expand: "(EX (x::int). P (x)) = (EX (j::int) : {1..d}. EX (a::int) : A. (P1 (j) | P(a - j))) |
|
845 |
==>(EX (x::int). P (x)) = (EX (j::int) : {1..d}. EX (a::int) : A. (P1 (j) | P(a - j))) " |
|
846 |
by blast |
|
847 |
||
848 |
||
849 |
lemma simp_from_to: "{i..j::int} = (if j < i then {} else insert i {i+1..j})" |
|
850 |
apply(simp add:atLeastAtMost_def atLeast_def atMost_def) |
|
851 |
apply(fastsimp) |
|
852 |
done |
|
853 |
||
14577 | 854 |
text {* \bigskip Theorems required for the @{text adjustcoeffitienteq} *} |
13876 | 855 |
|
856 |
lemma ac_dvd_eq: assumes not0: "0 ~= (k::int)" |
|
857 |
shows "((m::int) dvd (c*n+t)) = (k*m dvd ((k*c)*n+(k*t)))" (is "?P = ?Q") |
|
858 |
proof |
|
859 |
assume ?P |
|
860 |
thus ?Q |
|
861 |
apply(simp add:dvd_def) |
|
862 |
apply clarify |
|
863 |
apply(rename_tac d) |
|
864 |
apply(drule_tac f = "op * k" in arg_cong) |
|
865 |
apply(simp only:int_distrib) |
|
866 |
apply(rule_tac x = "d" in exI) |
|
14271 | 867 |
apply(simp only:mult_ac) |
13876 | 868 |
done |
869 |
next |
|
870 |
assume ?Q |
|
871 |
then obtain d where "k * c * n + k * t = (k*m)*d" by(fastsimp simp:dvd_def) |
|
14271 | 872 |
hence "(c * n + t) * k = (m*d) * k" by(simp add:int_distrib mult_ac) |
13876 | 873 |
hence "((c * n + t) * k) div k = ((m*d) * k) div k" by(rule arg_cong[of _ _ "%t. t div k"]) |
874 |
hence "c*n+t = m*d" by(simp add: zdiv_zmult_self1[OF not0[symmetric]]) |
|
875 |
thus ?P by(simp add:dvd_def) |
|
876 |
qed |
|
877 |
||
878 |
lemma ac_lt_eq: assumes gr0: "0 < (k::int)" |
|
879 |
shows "((m::int) < (c*n+t)) = (k*m <((k*c)*n+(k*t)))" (is "?P = ?Q") |
|
880 |
proof |
|
881 |
assume P: ?P |
|
14271 | 882 |
show ?Q using zmult_zless_mono2[OF P gr0] by(simp add: int_distrib mult_ac) |
13876 | 883 |
next |
884 |
assume ?Q |
|
14271 | 885 |
hence "0 < k*(c*n + t - m)" by(simp add: int_distrib mult_ac) |
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14271
diff
changeset
|
886 |
with gr0 have "0 < (c*n + t - m)" by(simp add: zero_less_mult_iff) |
13876 | 887 |
thus ?P by(simp) |
888 |
qed |
|
889 |
||
890 |
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") |
|
891 |
proof |
|
892 |
assume ?P |
|
893 |
thus ?Q |
|
894 |
apply(drule_tac f = "op * k" in arg_cong) |
|
895 |
apply(simp only:int_distrib) |
|
896 |
done |
|
897 |
next |
|
898 |
assume ?Q |
|
14271 | 899 |
hence "m * k = (c*n + t) * k" by(simp add:int_distrib mult_ac) |
13876 | 900 |
hence "((m) * k) div k = ((c*n + t) * k) div k" by(rule arg_cong[of _ _ "%t. t div k"]) |
901 |
thus ?P by(simp add: zdiv_zmult_self1[OF not0[symmetric]]) |
|
902 |
qed |
|
903 |
||
904 |
lemma ac_pi_eq: assumes gr0: "0 < (k::int)" shows "(~((0::int) < (c*n + t))) = (0 < ((-k)*c)*n + ((-k)*t + k))" |
|
905 |
proof - |
|
906 |
have "(~ (0::int) < (c*n + t)) = (0<1-(c*n + t))" by arith |
|
14271 | 907 |
also have "(1-(c*n + t)) = (-1*c)*n + (-t+1)" by(simp add: int_distrib mult_ac) |
13876 | 908 |
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]) |
14271 | 909 |
also have "(k*(-1*c)*n) + (k*(-t+1)) = ((-k)*c)*n + ((-k)*t + k)" by(simp add: int_distrib mult_ac) |
13876 | 910 |
finally show ?thesis . |
911 |
qed |
|
912 |
||
913 |
lemma binminus_uminus_conv: "(a::int) - b = a + (-b)" |
|
914 |
by arith |
|
915 |
||
916 |
lemma linearize_dvd: "(t::int) = t1 ==> (d dvd t) = (d dvd t1)" |
|
917 |
by simp |
|
918 |
||
919 |
lemma lf_lt: "(l::int) = ll ==> (r::int) = lr ==> (l < r) =(ll < lr)" |
|
920 |
by simp |
|
921 |
||
922 |
lemma lf_eq: "(l::int) = ll ==> (r::int) = lr ==> (l = r) =(ll = lr)" |
|
923 |
by simp |
|
924 |
||
925 |
lemma lf_dvd: "(l::int) = ll ==> (r::int) = lr ==> (l dvd r) =(ll dvd lr)" |
|
926 |
by simp |
|
927 |
||
14577 | 928 |
text {* \bigskip Theorems for transforming predicates on nat to predicates on @{text int}*} |
13876 | 929 |
|
930 |
theorem all_nat: "(\<forall>x::nat. P x) = (\<forall>x::int. 0 <= x \<longrightarrow> P (nat x))" |
|
931 |
by (simp split add: split_nat) |
|
932 |
||
933 |
||
934 |
theorem zdiff_int_split: "P (int (x - y)) = |
|
935 |
((y \<le> x \<longrightarrow> P (int x - int y)) \<and> (x < y \<longrightarrow> P 0))" |
|
936 |
apply (case_tac "y \<le> x") |
|
937 |
apply (simp_all add: zdiff_int) |
|
938 |
done |
|
939 |
||
940 |
||
941 |
theorem number_of1: "(0::int) <= number_of n \<Longrightarrow> (0::int) <= number_of (n BIT b)" |
|
942 |
by simp |
|
943 |
||
15013 | 944 |
theorem number_of2: "(0::int) <= Numeral0" by simp |
13876 | 945 |
|
946 |
theorem Suc_plus1: "Suc n = n + 1" by simp |
|
947 |
||
14577 | 948 |
text {* |
949 |
\medskip Specific instances of congruence rules, to prevent |
|
950 |
simplifier from looping. *} |
|
13876 | 951 |
|
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14738
diff
changeset
|
952 |
theorem imp_le_cong: "(0 <= x \<Longrightarrow> P = P') \<Longrightarrow> (0 <= (x::int) \<longrightarrow> P) = (0 <= x \<longrightarrow> P')" |
13876 | 953 |
by simp |
954 |
||
14758
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14738
diff
changeset
|
955 |
theorem conj_le_cong: "(0 <= x \<Longrightarrow> P = P') \<Longrightarrow> (0 <= (x::int) \<and> P) = (0 <= x \<and> P')" |
af3b71a46a1c
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
chaieb
parents:
14738
diff
changeset
|
956 |
by (simp cong: conj_cong) |
13876 | 957 |
|
18202
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
958 |
(* Theorems used in presburger.ML for the computation simpset*) |
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
959 |
(* FIXME: They are present in Float.thy, so may be Float.thy should be lightened.*) |
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
960 |
|
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
961 |
lemma lift_bool: "x \<Longrightarrow> x=True" |
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
962 |
by simp |
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
963 |
|
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
964 |
lemma nlift_bool: "~x \<Longrightarrow> x=False" |
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
965 |
by simp |
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
966 |
|
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
967 |
lemma not_false_eq_true: "(~ False) = True" by simp |
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
968 |
|
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
969 |
lemma not_true_eq_false: "(~ True) = False" by simp |
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
970 |
|
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
971 |
|
20485 | 972 |
lemma int_eq_number_of_eq: |
973 |
"(((number_of v)::int) = (number_of w)) = iszero ((number_of (v + (uminus w)))::int)" |
|
18202
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
974 |
by simp |
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
975 |
lemma int_iszero_number_of_Pls: "iszero (Numeral0::int)" |
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
976 |
by (simp only: iszero_number_of_Pls) |
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
977 |
|
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
978 |
lemma int_nonzero_number_of_Min: "~(iszero ((-1)::int))" |
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
979 |
by simp |
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
980 |
|
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
981 |
lemma int_iszero_number_of_0: "iszero ((number_of (w BIT bit.B0))::int) = iszero ((number_of w)::int)" |
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
982 |
by simp |
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
983 |
|
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
984 |
lemma int_iszero_number_of_1: "\<not> iszero ((number_of (w BIT bit.B1))::int)" |
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
985 |
by simp |
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
986 |
|
20485 | 987 |
lemma int_less_number_of_eq_neg: "(((number_of x)::int) < number_of y) = neg ((number_of (x + (uminus y)))::int)" |
18202
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
988 |
by simp |
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
989 |
|
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
990 |
lemma int_not_neg_number_of_Pls: "\<not> (neg (Numeral0::int))" |
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
991 |
by simp |
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
992 |
|
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
993 |
lemma int_neg_number_of_Min: "neg (-1::int)" |
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
994 |
by simp |
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
995 |
|
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
996 |
lemma int_neg_number_of_BIT: "neg ((number_of (w BIT x))::int) = neg ((number_of w)::int)" |
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
997 |
by simp |
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
998 |
|
20485 | 999 |
lemma int_le_number_of_eq: "(((number_of x)::int) \<le> number_of y) = (\<not> neg ((number_of (y + (uminus x)))::int))" |
18202
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
1000 |
by simp |
20485 | 1001 |
lemma int_number_of_add_sym: "((number_of v)::int) + number_of w = number_of (v + w)" |
18202
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
1002 |
by simp |
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
1003 |
|
20485 | 1004 |
lemma int_number_of_diff_sym: |
1005 |
"((number_of v)::int) - number_of w = number_of (v + (uminus w))" |
|
18202
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
1006 |
by simp |
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
1007 |
|
20485 | 1008 |
lemma int_number_of_mult_sym: |
1009 |
"((number_of v)::int) * number_of w = number_of (v * w)" |
|
18202
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
1010 |
by simp |
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
1011 |
|
20485 | 1012 |
lemma int_number_of_minus_sym: "- ((number_of v)::int) = number_of (uminus v)" |
18202
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
1013 |
by simp |
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
1014 |
lemma add_left_zero: "0 + a = (a::'a::comm_monoid_add)" |
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
1015 |
by simp |
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
1016 |
|
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
1017 |
lemma add_right_zero: "a + 0 = (a::'a::comm_monoid_add)" |
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
1018 |
by simp |
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
1019 |
|
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
1020 |
lemma mult_left_one: "1 * a = (a::'a::semiring_1)" |
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
1021 |
by simp |
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
1022 |
|
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
1023 |
lemma mult_right_one: "a * 1 = (a::'a::semiring_1)" |
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
1024 |
by simp |
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
1025 |
|
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
1026 |
lemma int_pow_0: "(a::int)^(Numeral0) = 1" |
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
1027 |
by simp |
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
1028 |
|
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
1029 |
lemma int_pow_1: "(a::int)^(Numeral1) = a" |
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
1030 |
by simp |
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
1031 |
|
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
1032 |
lemma zero_eq_Numeral0_nring: "(0::'a::number_ring) = Numeral0" |
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
1033 |
by simp |
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
1034 |
|
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
1035 |
lemma one_eq_Numeral1_nring: "(1::'a::number_ring) = Numeral1" |
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
1036 |
by simp |
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
1037 |
|
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
1038 |
lemma zero_eq_Numeral0_nat: "(0::nat) = Numeral0" |
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
1039 |
by simp |
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
1040 |
|
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
1041 |
lemma one_eq_Numeral1_nat: "(1::nat) = Numeral1" |
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
1042 |
by simp |
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
1043 |
|
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
1044 |
lemma zpower_Pls: "(z::int)^Numeral0 = Numeral1" |
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
1045 |
by simp |
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
1046 |
|
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
1047 |
lemma zpower_Min: "(z::int)^((-1)::nat) = Numeral1" |
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
1048 |
proof - |
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
1049 |
have 1:"((-1)::nat) = 0" |
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
1050 |
by simp |
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
1051 |
show ?thesis by (simp add: 1) |
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
1052 |
qed |
46af82efd311
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
chaieb
parents:
17589
diff
changeset
|
1053 |
|
23146 | 1054 |
use "Tools/Presburger/cooper_dec.ML" |
1055 |
use "Tools/Presburger/reflected_presburger.ML" |
|
1056 |
use "Tools/Presburger/reflected_cooper.ML" |
|
14941 | 1057 |
oracle |
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
16836
diff
changeset
|
1058 |
presburger_oracle ("term") = ReflectedCooper.presburger_oracle |
14941 | 1059 |
|
23146 | 1060 |
use "Tools/Presburger/cooper_proof.ML" |
1061 |
use "Tools/Presburger/qelim.ML" |
|
1062 |
use "Tools/Presburger/presburger.ML" |
|
13876 | 1063 |
|
1064 |
setup "Presburger.setup" |
|
1065 |
||
22801 | 1066 |
|
1067 |
subsection {* Code generator setup *} |
|
20595 | 1068 |
|
1069 |
text {* |
|
22801 | 1070 |
Presburger arithmetic is convenient to prove some |
1071 |
of the following code lemmas on integer numerals: |
|
20595 | 1072 |
*} |
1073 |
||
1074 |
lemma eq_Pls_Pls: |
|
22744
5cbe966d67a2
Isar definitions are now added explicitly to code theorem table
haftmann
parents:
22394
diff
changeset
|
1075 |
"Numeral.Pls = Numeral.Pls \<longleftrightarrow> True" by rule+ |
20595 | 1076 |
|
1077 |
lemma eq_Pls_Min: |
|
22744
5cbe966d67a2
Isar definitions are now added explicitly to code theorem table
haftmann
parents:
22394
diff
changeset
|
1078 |
"Numeral.Pls = Numeral.Min \<longleftrightarrow> False" |
21454 | 1079 |
unfolding Pls_def Min_def by auto |
20595 | 1080 |
|
1081 |
lemma eq_Pls_Bit0: |
|
21454 | 1082 |
"Numeral.Pls = Numeral.Bit k bit.B0 \<longleftrightarrow> Numeral.Pls = k" |
1083 |
unfolding Pls_def Bit_def bit.cases by auto |
|
20595 | 1084 |
|
1085 |
lemma eq_Pls_Bit1: |
|
22744
5cbe966d67a2
Isar definitions are now added explicitly to code theorem table
haftmann
parents:
22394
diff
changeset
|
1086 |
"Numeral.Pls = Numeral.Bit k bit.B1 \<longleftrightarrow> False" |
21454 | 1087 |
unfolding Pls_def Bit_def bit.cases by arith |
20595 | 1088 |
|
1089 |
lemma eq_Min_Pls: |
|
22744
5cbe966d67a2
Isar definitions are now added explicitly to code theorem table
haftmann
parents:
22394
diff
changeset
|
1090 |
"Numeral.Min = Numeral.Pls \<longleftrightarrow> False" |
21454 | 1091 |
unfolding Pls_def Min_def by auto |
20595 | 1092 |
|
1093 |
lemma eq_Min_Min: |
|
22744
5cbe966d67a2
Isar definitions are now added explicitly to code theorem table
haftmann
parents:
22394
diff
changeset
|
1094 |
"Numeral.Min = Numeral.Min \<longleftrightarrow> True" by rule+ |
20595 | 1095 |
|
1096 |
lemma eq_Min_Bit0: |
|
22744
5cbe966d67a2
Isar definitions are now added explicitly to code theorem table
haftmann
parents:
22394
diff
changeset
|
1097 |
"Numeral.Min = Numeral.Bit k bit.B0 \<longleftrightarrow> False" |
21454 | 1098 |
unfolding Min_def Bit_def bit.cases by arith |
20595 | 1099 |
|
1100 |
lemma eq_Min_Bit1: |
|
21454 | 1101 |
"Numeral.Min = Numeral.Bit k bit.B1 \<longleftrightarrow> Numeral.Min = k" |
1102 |
unfolding Min_def Bit_def bit.cases by auto |
|
20595 | 1103 |
|
1104 |
lemma eq_Bit0_Pls: |
|
21454 | 1105 |
"Numeral.Bit k bit.B0 = Numeral.Pls \<longleftrightarrow> Numeral.Pls = k" |
1106 |
unfolding Pls_def Bit_def bit.cases by auto |
|
20595 | 1107 |
|
1108 |
lemma eq_Bit1_Pls: |
|
22744
5cbe966d67a2
Isar definitions are now added explicitly to code theorem table
haftmann
parents:
22394
diff
changeset
|
1109 |
"Numeral.Bit k bit.B1 = Numeral.Pls \<longleftrightarrow> False" |
21454 | 1110 |
unfolding Pls_def Bit_def bit.cases by arith |
20595 | 1111 |
|
1112 |
lemma eq_Bit0_Min: |
|
22744
5cbe966d67a2
Isar definitions are now added explicitly to code theorem table
haftmann
parents:
22394
diff
changeset
|
1113 |
"Numeral.Bit k bit.B0 = Numeral.Min \<longleftrightarrow> False" |
21454 | 1114 |
unfolding Min_def Bit_def bit.cases by arith |
20595 | 1115 |
|
1116 |
lemma eq_Bit1_Min: |
|
21454 | 1117 |
"(Numeral.Bit k bit.B1) = Numeral.Min \<longleftrightarrow> Numeral.Min = k" |
1118 |
unfolding Min_def Bit_def bit.cases by auto |
|
20595 | 1119 |
|
1120 |
lemma eq_Bit_Bit: |
|
21454 | 1121 |
"Numeral.Bit k1 v1 = Numeral.Bit k2 v2 \<longleftrightarrow> |
1122 |
v1 = v2 \<and> k1 = k2" |
|
1123 |
unfolding Bit_def |
|
20595 | 1124 |
apply (cases v1) |
1125 |
apply (cases v2) |
|
1126 |
apply auto |
|
1127 |
apply arith |
|
1128 |
apply (cases v2) |
|
1129 |
apply auto |
|
1130 |
apply arith |
|
1131 |
apply (cases v2) |
|
1132 |
apply auto |
|
1133 |
done |
|
1134 |
||
22801 | 1135 |
lemma eq_number_of: |
1136 |
"(number_of k \<Colon> int) = number_of l \<longleftrightarrow> k = l" |
|
1137 |
unfolding number_of_is_id .. |
|
20595 | 1138 |
|
22394 | 1139 |
|
20595 | 1140 |
lemma less_eq_Pls_Pls: |
22744
5cbe966d67a2
Isar definitions are now added explicitly to code theorem table
haftmann
parents:
22394
diff
changeset
|
1141 |
"Numeral.Pls \<le> Numeral.Pls \<longleftrightarrow> True" by rule+ |
20595 | 1142 |
|
1143 |
lemma less_eq_Pls_Min: |
|
22744
5cbe966d67a2
Isar definitions are now added explicitly to code theorem table
haftmann
parents:
22394
diff
changeset
|
1144 |
"Numeral.Pls \<le> Numeral.Min \<longleftrightarrow> False" |
20595 | 1145 |
unfolding Pls_def Min_def by auto |
1146 |
||
1147 |
lemma less_eq_Pls_Bit: |
|
1148 |
"Numeral.Pls \<le> Numeral.Bit k v \<longleftrightarrow> Numeral.Pls \<le> k" |
|
1149 |
unfolding Pls_def Bit_def by (cases v) auto |
|
1150 |
||
1151 |
lemma less_eq_Min_Pls: |
|
22744
5cbe966d67a2
Isar definitions are now added explicitly to code theorem table
haftmann
parents:
22394
diff
changeset
|
1152 |
"Numeral.Min \<le> Numeral.Pls \<longleftrightarrow> True" |
20595 | 1153 |
unfolding Pls_def Min_def by auto |
1154 |
||
1155 |
lemma less_eq_Min_Min: |
|
22744
5cbe966d67a2
Isar definitions are now added explicitly to code theorem table
haftmann
parents:
22394
diff
changeset
|
1156 |
"Numeral.Min \<le> Numeral.Min \<longleftrightarrow> True" by rule+ |
20595 | 1157 |
|
1158 |
lemma less_eq_Min_Bit0: |
|
1159 |
"Numeral.Min \<le> Numeral.Bit k bit.B0 \<longleftrightarrow> Numeral.Min < k" |
|
1160 |
unfolding Min_def Bit_def by auto |
|
1161 |
||
1162 |
lemma less_eq_Min_Bit1: |
|
1163 |
"Numeral.Min \<le> Numeral.Bit k bit.B1 \<longleftrightarrow> Numeral.Min \<le> k" |
|
1164 |
unfolding Min_def Bit_def by auto |
|
1165 |
||
1166 |
lemma less_eq_Bit0_Pls: |
|
1167 |
"Numeral.Bit k bit.B0 \<le> Numeral.Pls \<longleftrightarrow> k \<le> Numeral.Pls" |
|
1168 |
unfolding Pls_def Bit_def by simp |
|
1169 |
||
1170 |
lemma less_eq_Bit1_Pls: |
|
1171 |
"Numeral.Bit k bit.B1 \<le> Numeral.Pls \<longleftrightarrow> k < Numeral.Pls" |
|
1172 |
unfolding Pls_def Bit_def by auto |
|
1173 |
||
1174 |
lemma less_eq_Bit_Min: |
|
1175 |
"Numeral.Bit k v \<le> Numeral.Min \<longleftrightarrow> k \<le> Numeral.Min" |
|
1176 |
unfolding Min_def Bit_def by (cases v) auto |
|
1177 |
||
1178 |
lemma less_eq_Bit0_Bit: |
|
1179 |
"Numeral.Bit k1 bit.B0 \<le> Numeral.Bit k2 v \<longleftrightarrow> k1 \<le> k2" |
|
22394 | 1180 |
unfolding Bit_def bit.cases by (cases v) auto |
20595 | 1181 |
|
1182 |
lemma less_eq_Bit_Bit1: |
|
1183 |
"Numeral.Bit k1 v \<le> Numeral.Bit k2 bit.B1 \<longleftrightarrow> k1 \<le> k2" |
|
22394 | 1184 |
unfolding Bit_def bit.cases by (cases v) auto |
1185 |
||
1186 |
lemma less_eq_Bit1_Bit0: |
|
1187 |
"Numeral.Bit k1 bit.B1 \<le> Numeral.Bit k2 bit.B0 \<longleftrightarrow> k1 < k2" |
|
1188 |
unfolding Bit_def by (auto split: bit.split) |
|
20595 | 1189 |
|
22801 | 1190 |
lemma less_eq_number_of: |
1191 |
"(number_of k \<Colon> int) \<le> number_of l \<longleftrightarrow> k \<le> l" |
|
1192 |
unfolding number_of_is_id .. |
|
22394 | 1193 |
|
1194 |
||
1195 |
lemma less_Pls_Pls: |
|
22744
5cbe966d67a2
Isar definitions are now added explicitly to code theorem table
haftmann
parents:
22394
diff
changeset
|
1196 |
"Numeral.Pls < Numeral.Pls \<longleftrightarrow> False" by auto |
22394 | 1197 |
|
1198 |
lemma less_Pls_Min: |
|
22744
5cbe966d67a2
Isar definitions are now added explicitly to code theorem table
haftmann
parents:
22394
diff
changeset
|
1199 |
"Numeral.Pls < Numeral.Min \<longleftrightarrow> False" |
22394 | 1200 |
unfolding Pls_def Min_def by auto |
1201 |
||
1202 |
lemma less_Pls_Bit0: |
|
1203 |
"Numeral.Pls < Numeral.Bit k bit.B0 \<longleftrightarrow> Numeral.Pls < k" |
|
1204 |
unfolding Pls_def Bit_def by auto |
|
1205 |
||
1206 |
lemma less_Pls_Bit1: |
|
1207 |
"Numeral.Pls < Numeral.Bit k bit.B1 \<longleftrightarrow> Numeral.Pls \<le> k" |
|
1208 |
unfolding Pls_def Bit_def by auto |
|
1209 |
||
1210 |
lemma less_Min_Pls: |
|
22744
5cbe966d67a2
Isar definitions are now added explicitly to code theorem table
haftmann
parents:
22394
diff
changeset
|
1211 |
"Numeral.Min < Numeral.Pls \<longleftrightarrow> True" |
22394 | 1212 |
unfolding Pls_def Min_def by auto |
1213 |
||
1214 |
lemma less_Min_Min: |
|
22744
5cbe966d67a2
Isar definitions are now added explicitly to code theorem table
haftmann
parents:
22394
diff
changeset
|
1215 |
"Numeral.Min < Numeral.Min \<longleftrightarrow> False" by auto |
22394 | 1216 |
|
1217 |
lemma less_Min_Bit: |
|
1218 |
"Numeral.Min < Numeral.Bit k v \<longleftrightarrow> Numeral.Min < k" |
|
1219 |
unfolding Min_def Bit_def by (auto split: bit.split) |
|
1220 |
||
1221 |
lemma less_Bit_Pls: |
|
1222 |
"Numeral.Bit k v < Numeral.Pls \<longleftrightarrow> k < Numeral.Pls" |
|
1223 |
unfolding Pls_def Bit_def by (auto split: bit.split) |
|
1224 |
||
1225 |
lemma less_Bit0_Min: |
|
1226 |
"Numeral.Bit k bit.B0 < Numeral.Min \<longleftrightarrow> k \<le> Numeral.Min" |
|
1227 |
unfolding Min_def Bit_def by auto |
|
1228 |
||
1229 |
lemma less_Bit1_Min: |
|
1230 |
"Numeral.Bit k bit.B1 < Numeral.Min \<longleftrightarrow> k < Numeral.Min" |
|
1231 |
unfolding Min_def Bit_def by auto |
|
1232 |
||
1233 |
lemma less_Bit_Bit0: |
|
1234 |
"Numeral.Bit k1 v < Numeral.Bit k2 bit.B0 \<longleftrightarrow> k1 < k2" |
|
1235 |
unfolding Bit_def by (auto split: bit.split) |
|
1236 |
||
1237 |
lemma less_Bit1_Bit: |
|
1238 |
"Numeral.Bit k1 bit.B1 < Numeral.Bit k2 v \<longleftrightarrow> k1 < k2" |
|
1239 |
unfolding Bit_def by (auto split: bit.split) |
|
1240 |
||
1241 |
lemma less_Bit0_Bit1: |
|
1242 |
"Numeral.Bit k1 bit.B0 < Numeral.Bit k2 bit.B1 \<longleftrightarrow> k1 \<le> k2" |
|
1243 |
unfolding Bit_def bit.cases by auto |
|
1244 |
||
22801 | 1245 |
lemma less_number_of: |
1246 |
"(number_of k \<Colon> int) < number_of l \<longleftrightarrow> k < l" |
|
1247 |
unfolding number_of_is_id .. |
|
1248 |
||
1249 |
||
1250 |
lemmas pred_succ_numeral_code [code func] = |
|
1251 |
arith_simps(5-12) |
|
1252 |
||
1253 |
lemmas plus_numeral_code [code func] = |
|
1254 |
arith_simps(13-17) |
|
1255 |
arith_simps(26-27) |
|
1256 |
arith_extra_simps(1) [where 'a = int] |
|
1257 |
||
1258 |
lemmas minus_numeral_code [code func] = |
|
1259 |
arith_simps(18-21) |
|
1260 |
arith_extra_simps(2) [where 'a = int] |
|
1261 |
arith_extra_simps(5) [where 'a = int] |
|
1262 |
||
1263 |
lemmas times_numeral_code [code func] = |
|
1264 |
arith_simps(22-25) |
|
1265 |
arith_extra_simps(4) [where 'a = int] |
|
1266 |
||
1267 |
lemmas eq_numeral_code [code func] = |
|
1268 |
eq_Pls_Pls eq_Pls_Min eq_Pls_Bit0 eq_Pls_Bit1 |
|
1269 |
eq_Min_Pls eq_Min_Min eq_Min_Bit0 eq_Min_Bit1 |
|
1270 |
eq_Bit0_Pls eq_Bit1_Pls eq_Bit0_Min eq_Bit1_Min eq_Bit_Bit |
|
1271 |
eq_number_of |
|
1272 |
||
1273 |
lemmas less_eq_numeral_code [code func] = less_eq_Pls_Pls less_eq_Pls_Min less_eq_Pls_Bit |
|
1274 |
less_eq_Min_Pls less_eq_Min_Min less_eq_Min_Bit0 less_eq_Min_Bit1 |
|
1275 |
less_eq_Bit0_Pls less_eq_Bit1_Pls less_eq_Bit_Min less_eq_Bit0_Bit less_eq_Bit_Bit1 less_eq_Bit1_Bit0 |
|
1276 |
less_eq_number_of |
|
1277 |
||
22394 | 1278 |
lemmas less_numeral_code [code func] = less_Pls_Pls less_Pls_Min less_Pls_Bit0 |
1279 |
less_Pls_Bit1 less_Min_Pls less_Min_Min less_Min_Bit less_Bit_Pls |
|
1280 |
less_Bit0_Min less_Bit1_Min less_Bit_Bit0 less_Bit1_Bit less_Bit0_Bit1 |
|
22801 | 1281 |
less_number_of |
20595 | 1282 |
|
13876 | 1283 |
end |