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