src/HOL/Presburger.thy
author chaieb
Wed May 19 11:23:59 2004 +0200 (2004-05-19)
changeset 14758 af3b71a46a1c
parent 14738 83f1a514dcb4
child 14941 1edb674e0c33
permissions -rw-r--r--
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
the tactic has also changed and allows the abstaction over fuction occurences whose type is nat or int.
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"}.
wenzelm@14577
   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. *}
wenzelm@14577
   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
chaieb@14758
   981
theorem imp_le_cong: "(0 <= x \<Longrightarrow> P = P') \<Longrightarrow> (0 <= (x::int) \<longrightarrow> P) = (0 <= x \<longrightarrow> P')"
berghofe@13876
   982
  by simp
berghofe@13876
   983
chaieb@14758
   984
theorem conj_le_cong: "(0 <= x \<Longrightarrow> P = P') \<Longrightarrow> (0 <= (x::int) \<and> P) = (0 <= x \<and> P')"
chaieb@14758
   985
  by (simp cong: conj_cong)
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