src/HOL/Presburger.thy
author haftmann
Fri Apr 20 11:21:42 2007 +0200 (2007-04-20)
changeset 22744 5cbe966d67a2
parent 22394 54ea68b5a92f
child 22801 caffcb450ef4
permissions -rw-r--r--
Isar definitions are now added explicitly to code theorem table
     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 
   930 theorem zdiff_int_split: "P (int (x - y)) =
   931   ((y \<le> x \<longrightarrow> P (int x - int y)) \<and> (x < y \<longrightarrow> P 0))"
   932   apply (case_tac "y \<le> x")
   933   apply (simp_all add: zdiff_int)
   934   done
   935 
   936 
   937 theorem number_of1: "(0::int) <= number_of n \<Longrightarrow> (0::int) <= number_of (n BIT b)"
   938   by simp
   939 
   940 theorem number_of2: "(0::int) <= Numeral0" by simp
   941 
   942 theorem Suc_plus1: "Suc n = n + 1" by simp
   943 
   944 text {*
   945   \medskip Specific instances of congruence rules, to prevent
   946   simplifier from looping. *}
   947 
   948 theorem imp_le_cong: "(0 <= x \<Longrightarrow> P = P') \<Longrightarrow> (0 <= (x::int) \<longrightarrow> P) = (0 <= x \<longrightarrow> P')"
   949   by simp
   950 
   951 theorem conj_le_cong: "(0 <= x \<Longrightarrow> P = P') \<Longrightarrow> (0 <= (x::int) \<and> P) = (0 <= x \<and> P')"
   952   by (simp cong: conj_cong)
   953 
   954     (* Theorems used in presburger.ML for the computation simpset*)
   955     (* FIXME: They are present in Float.thy, so may be Float.thy should be lightened.*)
   956 
   957 lemma lift_bool: "x \<Longrightarrow> x=True"
   958   by simp
   959 
   960 lemma nlift_bool: "~x \<Longrightarrow> x=False"
   961   by simp
   962 
   963 lemma not_false_eq_true: "(~ False) = True" by simp
   964 
   965 lemma not_true_eq_false: "(~ True) = False" by simp
   966 
   967 
   968 lemma int_eq_number_of_eq:
   969   "(((number_of v)::int) = (number_of w)) = iszero ((number_of (v + (uminus w)))::int)"
   970   by simp
   971 lemma int_iszero_number_of_Pls: "iszero (Numeral0::int)" 
   972   by (simp only: iszero_number_of_Pls)
   973 
   974 lemma int_nonzero_number_of_Min: "~(iszero ((-1)::int))"
   975   by simp
   976 
   977 lemma int_iszero_number_of_0: "iszero ((number_of (w BIT bit.B0))::int) = iszero ((number_of w)::int)"
   978   by simp
   979 
   980 lemma int_iszero_number_of_1: "\<not> iszero ((number_of (w BIT bit.B1))::int)" 
   981   by simp
   982 
   983 lemma int_less_number_of_eq_neg: "(((number_of x)::int) < number_of y) = neg ((number_of (x + (uminus y)))::int)"
   984   by simp
   985 
   986 lemma int_not_neg_number_of_Pls: "\<not> (neg (Numeral0::int))" 
   987   by simp
   988 
   989 lemma int_neg_number_of_Min: "neg (-1::int)"
   990   by simp
   991 
   992 lemma int_neg_number_of_BIT: "neg ((number_of (w BIT x))::int) = neg ((number_of w)::int)"
   993   by simp
   994 
   995 lemma int_le_number_of_eq: "(((number_of x)::int) \<le> number_of y) = (\<not> neg ((number_of (y + (uminus x)))::int))"
   996   by simp
   997 lemma int_number_of_add_sym: "((number_of v)::int) + number_of w = number_of (v + w)"
   998   by simp
   999 
  1000 lemma int_number_of_diff_sym:
  1001   "((number_of v)::int) - number_of w = number_of (v + (uminus w))"
  1002   by simp
  1003 
  1004 lemma int_number_of_mult_sym:
  1005   "((number_of v)::int) * number_of w = number_of (v * w)"
  1006   by simp
  1007 
  1008 lemma int_number_of_minus_sym: "- ((number_of v)::int) = number_of (uminus v)"
  1009   by simp
  1010 lemma add_left_zero: "0 + a = (a::'a::comm_monoid_add)"
  1011   by simp
  1012 
  1013 lemma add_right_zero: "a + 0 = (a::'a::comm_monoid_add)"
  1014   by simp
  1015 
  1016 lemma mult_left_one: "1 * a = (a::'a::semiring_1)"
  1017   by simp
  1018 
  1019 lemma mult_right_one: "a * 1 = (a::'a::semiring_1)"
  1020   by simp
  1021 
  1022 lemma int_pow_0: "(a::int)^(Numeral0) = 1"
  1023   by simp
  1024 
  1025 lemma int_pow_1: "(a::int)^(Numeral1) = a"
  1026   by simp
  1027 
  1028 lemma zero_eq_Numeral0_nring: "(0::'a::number_ring) = Numeral0"
  1029   by simp
  1030 
  1031 lemma one_eq_Numeral1_nring: "(1::'a::number_ring) = Numeral1"
  1032   by simp
  1033 
  1034 lemma zero_eq_Numeral0_nat: "(0::nat) = Numeral0"
  1035   by simp
  1036 
  1037 lemma one_eq_Numeral1_nat: "(1::nat) = Numeral1"
  1038   by simp
  1039 
  1040 lemma zpower_Pls: "(z::int)^Numeral0 = Numeral1"
  1041   by simp
  1042 
  1043 lemma zpower_Min: "(z::int)^((-1)::nat) = Numeral1"
  1044 proof -
  1045   have 1:"((-1)::nat) = 0"
  1046     by simp
  1047   show ?thesis by (simp add: 1)
  1048 qed
  1049 
  1050 use "cooper_dec.ML"
  1051 use "reflected_presburger.ML" 
  1052 use "reflected_cooper.ML"
  1053 oracle
  1054   presburger_oracle ("term") = ReflectedCooper.presburger_oracle
  1055 
  1056 use "cooper_proof.ML"
  1057 use "qelim.ML"
  1058 use "presburger.ML"
  1059 
  1060 setup "Presburger.setup"
  1061 
  1062 text {* Code generator setup *}
  1063 
  1064 text {*
  1065   Presburger arithmetic is necessary (at least convenient) to prove some
  1066   of the following code lemmas on integer numerals.
  1067 *}
  1068 
  1069 lemma eq_number_of [code func]:
  1070   "((number_of k)\<Colon>int) = number_of l \<longleftrightarrow> k = l"
  1071   unfolding number_of_is_id ..
  1072 
  1073 lemma eq_Pls_Pls:
  1074   "Numeral.Pls = Numeral.Pls \<longleftrightarrow> True" by rule+
  1075 
  1076 lemma eq_Pls_Min:
  1077   "Numeral.Pls = Numeral.Min \<longleftrightarrow> False"
  1078   unfolding Pls_def Min_def by auto
  1079 
  1080 lemma eq_Pls_Bit0:
  1081   "Numeral.Pls = Numeral.Bit k bit.B0 \<longleftrightarrow> Numeral.Pls = k"
  1082   unfolding Pls_def Bit_def bit.cases by auto
  1083 
  1084 lemma eq_Pls_Bit1:
  1085   "Numeral.Pls = Numeral.Bit k bit.B1 \<longleftrightarrow> False"
  1086   unfolding Pls_def Bit_def bit.cases by arith
  1087 
  1088 lemma eq_Min_Pls:
  1089   "Numeral.Min = Numeral.Pls \<longleftrightarrow> False"
  1090   unfolding Pls_def Min_def by auto
  1091 
  1092 lemma eq_Min_Min:
  1093   "Numeral.Min = Numeral.Min \<longleftrightarrow> True" by rule+
  1094 
  1095 lemma eq_Min_Bit0:
  1096   "Numeral.Min = Numeral.Bit k bit.B0 \<longleftrightarrow> False"
  1097   unfolding Min_def Bit_def bit.cases by arith
  1098 
  1099 lemma eq_Min_Bit1:
  1100   "Numeral.Min = Numeral.Bit k bit.B1 \<longleftrightarrow> Numeral.Min = k"
  1101   unfolding Min_def Bit_def bit.cases by auto
  1102 
  1103 lemma eq_Bit0_Pls:
  1104   "Numeral.Bit k bit.B0 = Numeral.Pls \<longleftrightarrow> Numeral.Pls = k"
  1105   unfolding Pls_def Bit_def bit.cases by auto
  1106 
  1107 lemma eq_Bit1_Pls:
  1108   "Numeral.Bit k bit.B1 = Numeral.Pls \<longleftrightarrow> False"
  1109   unfolding Pls_def Bit_def bit.cases by arith
  1110 
  1111 lemma eq_Bit0_Min:
  1112   "Numeral.Bit k bit.B0 = Numeral.Min \<longleftrightarrow> False"
  1113   unfolding Min_def Bit_def bit.cases by arith
  1114 
  1115 lemma eq_Bit1_Min:
  1116   "(Numeral.Bit k bit.B1) = Numeral.Min \<longleftrightarrow> Numeral.Min = k"
  1117   unfolding Min_def Bit_def bit.cases by auto
  1118 
  1119 lemma eq_Bit_Bit:
  1120   "Numeral.Bit k1 v1 = Numeral.Bit k2 v2 \<longleftrightarrow>
  1121     v1 = v2 \<and> k1 = k2"
  1122   unfolding Bit_def
  1123   apply (cases v1)
  1124   apply (cases v2)
  1125   apply auto
  1126   apply arith
  1127   apply (cases v2)
  1128   apply auto
  1129   apply arith
  1130   apply (cases v2)
  1131   apply auto
  1132 done
  1133 
  1134 lemmas eq_numeral_code [code func] =
  1135   eq_Pls_Pls eq_Pls_Min eq_Pls_Bit0 eq_Pls_Bit1
  1136   eq_Min_Pls eq_Min_Min eq_Min_Bit0 eq_Min_Bit1
  1137   eq_Bit0_Pls eq_Bit1_Pls eq_Bit0_Min eq_Bit1_Min eq_Bit_Bit
  1138 
  1139 lemma less_eq_number_of [code func]:
  1140   "(number_of k \<Colon> int) \<le> number_of l \<longleftrightarrow> k \<le> l"
  1141   unfolding number_of_is_id ..
  1142 
  1143 lemma less_eq_Pls_Pls:
  1144   "Numeral.Pls \<le> Numeral.Pls \<longleftrightarrow> True" by rule+
  1145 
  1146 lemma less_eq_Pls_Min:
  1147   "Numeral.Pls \<le> Numeral.Min \<longleftrightarrow> False"
  1148   unfolding Pls_def Min_def by auto
  1149 
  1150 lemma less_eq_Pls_Bit:
  1151   "Numeral.Pls \<le> Numeral.Bit k v \<longleftrightarrow> Numeral.Pls \<le> k"
  1152   unfolding Pls_def Bit_def by (cases v) auto
  1153 
  1154 lemma less_eq_Min_Pls:
  1155   "Numeral.Min \<le> Numeral.Pls \<longleftrightarrow> True"
  1156   unfolding Pls_def Min_def by auto
  1157 
  1158 lemma less_eq_Min_Min:
  1159   "Numeral.Min \<le> Numeral.Min \<longleftrightarrow> True" by rule+
  1160 
  1161 lemma less_eq_Min_Bit0:
  1162   "Numeral.Min \<le> Numeral.Bit k bit.B0 \<longleftrightarrow> Numeral.Min < k"
  1163   unfolding Min_def Bit_def by auto
  1164 
  1165 lemma less_eq_Min_Bit1:
  1166   "Numeral.Min \<le> Numeral.Bit k bit.B1 \<longleftrightarrow> Numeral.Min \<le> k"
  1167   unfolding Min_def Bit_def by auto
  1168 
  1169 lemma less_eq_Bit0_Pls:
  1170   "Numeral.Bit k bit.B0 \<le> Numeral.Pls \<longleftrightarrow> k \<le> Numeral.Pls"
  1171   unfolding Pls_def Bit_def by simp
  1172 
  1173 lemma less_eq_Bit1_Pls:
  1174   "Numeral.Bit k bit.B1 \<le> Numeral.Pls \<longleftrightarrow> k < Numeral.Pls"
  1175   unfolding Pls_def Bit_def by auto
  1176 
  1177 lemma less_eq_Bit_Min:
  1178   "Numeral.Bit k v \<le> Numeral.Min \<longleftrightarrow> k \<le> Numeral.Min"
  1179   unfolding Min_def Bit_def by (cases v) auto
  1180 
  1181 lemma less_eq_Bit0_Bit:
  1182   "Numeral.Bit k1 bit.B0 \<le> Numeral.Bit k2 v \<longleftrightarrow> k1 \<le> k2"
  1183   unfolding Bit_def bit.cases by (cases v) auto
  1184 
  1185 lemma less_eq_Bit_Bit1:
  1186   "Numeral.Bit k1 v \<le> Numeral.Bit k2 bit.B1 \<longleftrightarrow> k1 \<le> k2"
  1187   unfolding Bit_def bit.cases by (cases v) auto
  1188 
  1189 lemma less_eq_Bit1_Bit0:
  1190   "Numeral.Bit k1 bit.B1 \<le> Numeral.Bit k2 bit.B0 \<longleftrightarrow> k1 < k2"
  1191   unfolding Bit_def by (auto split: bit.split)
  1192 
  1193 lemmas less_eq_numeral_code [code func] = less_eq_Pls_Pls less_eq_Pls_Min less_eq_Pls_Bit
  1194   less_eq_Min_Pls less_eq_Min_Min less_eq_Min_Bit0 less_eq_Min_Bit1
  1195   less_eq_Bit0_Pls less_eq_Bit1_Pls less_eq_Bit_Min less_eq_Bit0_Bit less_eq_Bit_Bit1 less_eq_Bit1_Bit0
  1196 
  1197 lemma less_eq_number_of [code func]:
  1198   "(number_of k \<Colon> int) < number_of l \<longleftrightarrow> k < l"
  1199   unfolding number_of_is_id ..
  1200 
  1201 lemma less_Pls_Pls:
  1202   "Numeral.Pls < Numeral.Pls \<longleftrightarrow> False" by auto
  1203 
  1204 lemma less_Pls_Min:
  1205   "Numeral.Pls < Numeral.Min \<longleftrightarrow> False"
  1206   unfolding Pls_def Min_def by auto
  1207 
  1208 lemma less_Pls_Bit0:
  1209   "Numeral.Pls < Numeral.Bit k bit.B0 \<longleftrightarrow> Numeral.Pls < k"
  1210   unfolding Pls_def Bit_def by auto
  1211 
  1212 lemma less_Pls_Bit1:
  1213   "Numeral.Pls < Numeral.Bit k bit.B1 \<longleftrightarrow> Numeral.Pls \<le> k"
  1214   unfolding Pls_def Bit_def by auto
  1215 
  1216 lemma less_Min_Pls:
  1217   "Numeral.Min < Numeral.Pls \<longleftrightarrow> True"
  1218   unfolding Pls_def Min_def by auto
  1219 
  1220 lemma less_Min_Min:
  1221   "Numeral.Min < Numeral.Min \<longleftrightarrow> False" by auto
  1222 
  1223 lemma less_Min_Bit:
  1224   "Numeral.Min < Numeral.Bit k v \<longleftrightarrow> Numeral.Min < k"
  1225   unfolding Min_def Bit_def by (auto split: bit.split)
  1226 
  1227 lemma less_Bit_Pls:
  1228   "Numeral.Bit k v < Numeral.Pls \<longleftrightarrow> k < Numeral.Pls"
  1229   unfolding Pls_def Bit_def by (auto split: bit.split)
  1230 
  1231 lemma less_Bit0_Min:
  1232   "Numeral.Bit k bit.B0 < Numeral.Min \<longleftrightarrow> k \<le> Numeral.Min"
  1233   unfolding Min_def Bit_def by auto
  1234 
  1235 lemma less_Bit1_Min:
  1236   "Numeral.Bit k bit.B1 < Numeral.Min \<longleftrightarrow> k < Numeral.Min"
  1237   unfolding Min_def Bit_def by auto
  1238 
  1239 lemma less_Bit_Bit0:
  1240   "Numeral.Bit k1 v < Numeral.Bit k2 bit.B0 \<longleftrightarrow> k1 < k2"
  1241   unfolding Bit_def by (auto split: bit.split)
  1242 
  1243 lemma less_Bit1_Bit:
  1244   "Numeral.Bit k1 bit.B1 < Numeral.Bit k2 v \<longleftrightarrow> k1 < k2"
  1245   unfolding Bit_def by (auto split: bit.split)
  1246 
  1247 lemma less_Bit0_Bit1:
  1248   "Numeral.Bit k1 bit.B0 < Numeral.Bit k2 bit.B1 \<longleftrightarrow> k1 \<le> k2"
  1249   unfolding Bit_def bit.cases by auto
  1250 
  1251 lemmas less_numeral_code [code func] = less_Pls_Pls less_Pls_Min less_Pls_Bit0
  1252   less_Pls_Bit1 less_Min_Pls less_Min_Min less_Min_Bit less_Bit_Pls
  1253   less_Bit0_Min less_Bit1_Min less_Bit_Bit0 less_Bit1_Bit less_Bit0_Bit1
  1254 
  1255 end