178 |
178 |
179 subsection\<open>Cooper's Theorem \<open>-\<infinity>\<close> and \<open>+\<infinity>\<close> Version\<close> |
179 subsection\<open>Cooper's Theorem \<open>-\<infinity>\<close> and \<open>+\<infinity>\<close> Version\<close> |
180 |
180 |
181 subsubsection\<open>First some trivial facts about periodic sets or predicates\<close> |
181 subsubsection\<open>First some trivial facts about periodic sets or predicates\<close> |
182 lemma periodic_finite_ex: |
182 lemma periodic_finite_ex: |
183 assumes dpos: "(0::int) < d" and modd: "ALL x k. P x = P(x - k*d)" |
183 assumes dpos: "(0::int) < d" and modd: "\<forall>x k. P x = P(x - k*d)" |
184 shows "(EX x. P x) = (EX j : {1..d}. P j)" |
184 shows "(\<exists>x. P x) = (\<exists>j \<in> {1..d}. P j)" |
185 (is "?LHS = ?RHS") |
185 (is "?LHS = ?RHS") |
186 proof |
186 proof |
187 assume ?LHS |
187 assume ?LHS |
188 then obtain x where P: "P x" .. |
188 then obtain x where P: "P x" .. |
189 have "x mod d = x - (x div d)*d" by(simp add:mult_div_mod_eq [symmetric] ac_simps eq_diff_eq) |
189 have "x mod d = x - (x div d)*d" by(simp add:mult_div_mod_eq [symmetric] ac_simps eq_diff_eq) |
217 lemma incr_lemma: "0 < (d::int) \<Longrightarrow> z < x + (\<bar>x - z\<bar> + 1) * d" |
217 lemma incr_lemma: "0 < (d::int) \<Longrightarrow> z < x + (\<bar>x - z\<bar> + 1) * d" |
218 by (induct rule: int_gr_induct) (simp_all add: int_distrib) |
218 by (induct rule: int_gr_induct) (simp_all add: int_distrib) |
219 |
219 |
220 lemma decr_mult_lemma: |
220 lemma decr_mult_lemma: |
221 assumes dpos: "(0::int) < d" and minus: "\<forall>x. P x \<longrightarrow> P(x - d)" and knneg: "0 <= k" |
221 assumes dpos: "(0::int) < d" and minus: "\<forall>x. P x \<longrightarrow> P(x - d)" and knneg: "0 <= k" |
222 shows "ALL x. P x \<longrightarrow> P(x - k*d)" |
222 shows "\<forall>x. P x \<longrightarrow> P(x - k*d)" |
223 using knneg |
223 using knneg |
224 proof (induct rule:int_ge_induct) |
224 proof (induct rule:int_ge_induct) |
225 case base thus ?case by simp |
225 case base thus ?case by simp |
226 next |
226 next |
227 case (step i) |
227 case (step i) |
233 thus ?case .. |
233 thus ?case .. |
234 qed |
234 qed |
235 |
235 |
236 lemma minusinfinity: |
236 lemma minusinfinity: |
237 assumes dpos: "0 < d" and |
237 assumes dpos: "0 < d" and |
238 P1eqP1: "ALL x k. P1 x = P1(x - k*d)" and ePeqP1: "EX z::int. ALL x. x < z \<longrightarrow> (P x = P1 x)" |
238 P1eqP1: "\<forall>x k. P1 x = P1(x - k*d)" and ePeqP1: "\<exists>z::int. \<forall>x. x < z \<longrightarrow> (P x = P1 x)" |
239 shows "(EX x. P1 x) \<longrightarrow> (EX x. P x)" |
239 shows "(\<exists>x. P1 x) \<longrightarrow> (\<exists>x. P x)" |
240 proof |
240 proof |
241 assume eP1: "EX x. P1 x" |
241 assume eP1: "\<exists>x. P1 x" |
242 then obtain x where P1: "P1 x" .. |
242 then obtain x where P1: "P1 x" .. |
243 from ePeqP1 obtain z where P1eqP: "ALL x. x < z \<longrightarrow> (P x = P1 x)" .. |
243 from ePeqP1 obtain z where P1eqP: "\<forall>x. x < z \<longrightarrow> (P x = P1 x)" .. |
244 let ?w = "x - (\<bar>x - z\<bar> + 1) * d" |
244 let ?w = "x - (\<bar>x - z\<bar> + 1) * d" |
245 from dpos have w: "?w < z" by(rule decr_lemma) |
245 from dpos have w: "?w < z" by(rule decr_lemma) |
246 have "P1 x = P1 ?w" using P1eqP1 by blast |
246 have "P1 x = P1 ?w" using P1eqP1 by blast |
247 also have "\<dots> = P(?w)" using w P1eqP by blast |
247 also have "\<dots> = P(?w)" using w P1eqP by blast |
248 finally have "P ?w" using P1 by blast |
248 finally have "P ?w" using P1 by blast |
249 thus "EX x. P x" .. |
249 thus "\<exists>x. P x" .. |
250 qed |
250 qed |
251 |
251 |
252 lemma cpmi: |
252 lemma cpmi: |
253 assumes dp: "0 < D" and p1:"\<exists>z. \<forall> x< z. P x = P' x" |
253 assumes dp: "0 < D" and p1:"\<exists>z. \<forall> x< z. P x = P' x" |
254 and nb:"\<forall>x.(\<forall> j\<in> {1..D}. \<forall>(b::int) \<in> B. x \<noteq> b+j) --> P (x) --> P (x - D)" |
254 and nb:"\<forall>x.(\<forall> j\<in> {1..D}. \<forall>(b::int) \<in> B. x \<noteq> b+j) \<longrightarrow> P (x) \<longrightarrow> P (x - D)" |
255 and pd: "\<forall> x k. P' x = P' (x-k*D)" |
255 and pd: "\<forall> x k. P' x = P' (x-k*D)" |
256 shows "(\<exists>x. P x) = ((\<exists> j\<in> {1..D} . P' j) | (\<exists> j \<in> {1..D}.\<exists> b\<in> B. P (b+j)))" |
256 shows "(\<exists>x. P x) = ((\<exists>j \<in> {1..D} . P' j) \<or> (\<exists>j \<in> {1..D}. \<exists> b \<in> B. P (b+j)))" |
257 (is "?L = (?R1 \<or> ?R2)") |
257 (is "?L = (?R1 \<or> ?R2)") |
258 proof- |
258 proof- |
259 {assume "?R2" hence "?L" by blast} |
259 {assume "?R2" hence "?L" by blast} |
260 moreover |
260 moreover |
261 {assume H:"?R1" hence "?L" using minusinfinity[OF dp pd p1] periodic_finite_ex[OF dp pd] by simp} |
261 {assume H:"?R1" hence "?L" using minusinfinity[OF dp pd p1] periodic_finite_ex[OF dp pd] by simp} |
262 moreover |
262 moreover |
263 { fix x |
263 { fix x |
264 assume P: "P x" and H: "\<not> ?R2" |
264 assume P: "P x" and H: "\<not> ?R2" |
265 {fix y assume "\<not> (\<exists>j\<in>{1..D}. \<exists>b\<in>B. P (b + j))" and P: "P y" |
265 {fix y assume "\<not> (\<exists>j\<in>{1..D}. \<exists>b\<in>B. P (b + j))" and P: "P y" |
266 hence "~(EX (j::int) : {1..D}. EX (b::int) : B. y = b+j)" by auto |
266 hence "\<not>(\<exists>(j::int) \<in> {1..D}. \<exists>(b::int) \<in> B. y = b+j)" by auto |
267 with nb P have "P (y - D)" by auto } |
267 with nb P have "P (y - D)" by auto } |
268 hence "ALL x.~(EX (j::int) : {1..D}. EX (b::int) : B. P(b+j)) --> P (x) --> P (x - D)" by blast |
268 hence "\<forall>x. \<not>(\<exists>(j::int) \<in> {1..D}. \<exists>(b::int) \<in> B. P(b+j)) \<longrightarrow> P (x) \<longrightarrow> P (x - D)" by blast |
269 with H P have th: " \<forall>x. P x \<longrightarrow> P (x - D)" by auto |
269 with H P have th: " \<forall>x. P x \<longrightarrow> P (x - D)" by auto |
270 from p1 obtain z where z: "ALL x. x < z --> (P x = P' x)" by blast |
270 from p1 obtain z where z: "\<forall>x. x < z \<longrightarrow> (P x = P' x)" by blast |
271 let ?y = "x - (\<bar>x - z\<bar> + 1)*D" |
271 let ?y = "x - (\<bar>x - z\<bar> + 1)*D" |
272 have zp: "0 <= (\<bar>x - z\<bar> + 1)" by arith |
272 have zp: "0 <= (\<bar>x - z\<bar> + 1)" by arith |
273 from dp have yz: "?y < z" using decr_lemma[OF dp] by simp |
273 from dp have yz: "?y < z" using decr_lemma[OF dp] by simp |
274 from z[rule_format, OF yz] decr_mult_lemma[OF dp th zp, rule_format, OF P] have th2: " P' ?y" by auto |
274 from z[rule_format, OF yz] decr_mult_lemma[OF dp th zp, rule_format, OF P] have th2: " P' ?y" by auto |
275 with periodic_finite_ex[OF dp pd] |
275 with periodic_finite_ex[OF dp pd] |
282 lemma plusinfinity: |
282 lemma plusinfinity: |
283 assumes dpos: "(0::int) < d" and |
283 assumes dpos: "(0::int) < d" and |
284 P1eqP1: "\<forall>x k. P' x = P'(x - k*d)" and ePeqP1: "\<exists> z. \<forall> x>z. P x = P' x" |
284 P1eqP1: "\<forall>x k. P' x = P'(x - k*d)" and ePeqP1: "\<exists> z. \<forall> x>z. P x = P' x" |
285 shows "(\<exists> x. P' x) \<longrightarrow> (\<exists> x. P x)" |
285 shows "(\<exists> x. P' x) \<longrightarrow> (\<exists> x. P x)" |
286 proof |
286 proof |
287 assume eP1: "EX x. P' x" |
287 assume eP1: "\<exists>x. P' x" |
288 then obtain x where P1: "P' x" .. |
288 then obtain x where P1: "P' x" .. |
289 from ePeqP1 obtain z where P1eqP: "\<forall>x>z. P x = P' x" .. |
289 from ePeqP1 obtain z where P1eqP: "\<forall>x>z. P x = P' x" .. |
290 let ?w' = "x + (\<bar>x - z\<bar> + 1) * d" |
290 let ?w' = "x + (\<bar>x - z\<bar> + 1) * d" |
291 let ?w = "x - (- (\<bar>x - z\<bar> + 1)) * d" |
291 let ?w = "x - (- (\<bar>x - z\<bar> + 1)) * d" |
292 have ww'[simp]: "?w = ?w'" by (simp add: algebra_simps) |
292 have ww'[simp]: "?w = ?w'" by (simp add: algebra_simps) |
293 from dpos have w: "?w > z" by(simp only: ww' incr_lemma) |
293 from dpos have w: "?w > z" by(simp only: ww' incr_lemma) |
294 hence "P' x = P' ?w" using P1eqP1 by blast |
294 hence "P' x = P' ?w" using P1eqP1 by blast |
295 also have "\<dots> = P(?w)" using w P1eqP by blast |
295 also have "\<dots> = P(?w)" using w P1eqP by blast |
296 finally have "P ?w" using P1 by blast |
296 finally have "P ?w" using P1 by blast |
297 thus "EX x. P x" .. |
297 thus "\<exists>x. P x" .. |
298 qed |
298 qed |
299 |
299 |
300 lemma incr_mult_lemma: |
300 lemma incr_mult_lemma: |
301 assumes dpos: "(0::int) < d" and plus: "ALL x::int. P x \<longrightarrow> P(x + d)" and knneg: "0 <= k" |
301 assumes dpos: "(0::int) < d" and plus: "\<forall>x::int. P x \<longrightarrow> P(x + d)" and knneg: "0 <= k" |
302 shows "ALL x. P x \<longrightarrow> P(x + k*d)" |
302 shows "\<forall>x. P x \<longrightarrow> P(x + k*d)" |
303 using knneg |
303 using knneg |
304 proof (induct rule:int_ge_induct) |
304 proof (induct rule:int_ge_induct) |
305 case base thus ?case by simp |
305 case base thus ?case by simp |
306 next |
306 next |
307 case (step i) |
307 case (step i) |
313 thus ?case .. |
313 thus ?case .. |
314 qed |
314 qed |
315 |
315 |
316 lemma cppi: |
316 lemma cppi: |
317 assumes dp: "0 < D" and p1:"\<exists>z. \<forall> x> z. P x = P' x" |
317 assumes dp: "0 < D" and p1:"\<exists>z. \<forall> x> z. P x = P' x" |
318 and nb:"\<forall>x.(\<forall> j\<in> {1..D}. \<forall>(b::int) \<in> A. x \<noteq> b - j) --> P (x) --> P (x + D)" |
318 and nb:"\<forall>x.(\<forall> j\<in> {1..D}. \<forall>(b::int) \<in> A. x \<noteq> b - j) \<longrightarrow> P (x) \<longrightarrow> P (x + D)" |
319 and pd: "\<forall> x k. P' x= P' (x-k*D)" |
319 and pd: "\<forall> x k. P' x= P' (x-k*D)" |
320 shows "(\<exists>x. P x) = ((\<exists> j\<in> {1..D} . P' j) | (\<exists> j \<in> {1..D}.\<exists> b\<in> A. P (b - j)))" (is "?L = (?R1 \<or> ?R2)") |
320 shows "(\<exists>x. P x) = ((\<exists>j \<in> {1..D} . P' j) \<or> (\<exists> j \<in> {1..D}. \<exists> b\<in> A. P (b - j)))" (is "?L = (?R1 \<or> ?R2)") |
321 proof- |
321 proof- |
322 {assume "?R2" hence "?L" by blast} |
322 {assume "?R2" hence "?L" by blast} |
323 moreover |
323 moreover |
324 {assume H:"?R1" hence "?L" using plusinfinity[OF dp pd p1] periodic_finite_ex[OF dp pd] by simp} |
324 {assume H:"?R1" hence "?L" using plusinfinity[OF dp pd p1] periodic_finite_ex[OF dp pd] by simp} |
325 moreover |
325 moreover |
326 { fix x |
326 { fix x |
327 assume P: "P x" and H: "\<not> ?R2" |
327 assume P: "P x" and H: "\<not> ?R2" |
328 {fix y assume "\<not> (\<exists>j\<in>{1..D}. \<exists>b\<in>A. P (b - j))" and P: "P y" |
328 {fix y assume "\<not> (\<exists>j\<in>{1..D}. \<exists>b\<in>A. P (b - j))" and P: "P y" |
329 hence "~(EX (j::int) : {1..D}. EX (b::int) : A. y = b - j)" by auto |
329 hence "\<not>(\<exists>(j::int) \<in> {1..D}. \<exists>(b::int) \<in> A. y = b - j)" by auto |
330 with nb P have "P (y + D)" by auto } |
330 with nb P have "P (y + D)" by auto } |
331 hence "ALL x.~(EX (j::int) : {1..D}. EX (b::int) : A. P(b-j)) --> P (x) --> P (x + D)" by blast |
331 hence "\<forall>x. \<not>(\<exists>(j::int) \<in> {1..D}. \<exists>(b::int) \<in> A. P(b-j)) \<longrightarrow> P (x) \<longrightarrow> P (x + D)" by blast |
332 with H P have th: " \<forall>x. P x \<longrightarrow> P (x + D)" by auto |
332 with H P have th: " \<forall>x. P x \<longrightarrow> P (x + D)" by auto |
333 from p1 obtain z where z: "ALL x. x > z --> (P x = P' x)" by blast |
333 from p1 obtain z where z: "\<forall>x. x > z \<longrightarrow> (P x = P' x)" by blast |
334 let ?y = "x + (\<bar>x - z\<bar> + 1)*D" |
334 let ?y = "x + (\<bar>x - z\<bar> + 1)*D" |
335 have zp: "0 <= (\<bar>x - z\<bar> + 1)" by arith |
335 have zp: "0 <= (\<bar>x - z\<bar> + 1)" by arith |
336 from dp have yz: "?y > z" using incr_lemma[OF dp] by simp |
336 from dp have yz: "?y > z" using incr_lemma[OF dp] by simp |
337 from z[rule_format, OF yz] incr_mult_lemma[OF dp th zp, rule_format, OF P] have th2: " P' ?y" by auto |
337 from z[rule_format, OF yz] incr_mult_lemma[OF dp th zp, rule_format, OF P] have th2: " P' ?y" by auto |
338 with periodic_finite_ex[OF dp pd] |
338 with periodic_finite_ex[OF dp pd] |