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