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