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