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