src/HOL/Presburger.thy
author wenzelm
Thu Jun 21 15:42:14 2007 +0200 (2007-06-21)
changeset 23460 f9ae34d5f8da
parent 23438 dd824e86fa8a
permissions -rw-r--r--
adapted tool setup;
     1 (*  Title:      HOL/Presburger.thy
     2     ID:         $Id$
     3     Author:     Amine Chaieb, TU Muenchen
     4 *)
     5 
     6 header {* Decision Procedure for Presburger Arithmetic *}
     7 
     8 theory Presburger
     9 imports NatSimprocs SetInterval
    10 uses
    11   "Tools/Presburger/cooper_data.ML"
    12   "Tools/Presburger/generated_cooper.ML"
    13   ("Tools/Presburger/cooper.ML")
    14   ("Tools/Presburger/presburger.ML") 
    15 begin
    16 
    17 setup CooperData.setup
    18 
    19 
    20 subsection{* The @{text "-\<infinity>"} and @{text "+\<infinity>"} Properties *}
    21 
    22 lemma minf:
    23   "\<lbrakk>\<exists>(z ::'a::linorder).\<forall>x<z. P x = P' x; \<exists>z.\<forall>x<z. Q x = Q' x\<rbrakk> 
    24      \<Longrightarrow> \<exists>z.\<forall>x<z. (P x \<and> Q x) = (P' x \<and> Q' x)"
    25   "\<lbrakk>\<exists>(z ::'a::linorder).\<forall>x<z. P x = P' x; \<exists>z.\<forall>x<z. Q x = Q' x\<rbrakk> 
    26      \<Longrightarrow> \<exists>z.\<forall>x<z. (P x \<or> Q x) = (P' x \<or> Q' x)"
    27   "\<exists>(z ::'a::{linorder}).\<forall>x<z.(x = t) = False"
    28   "\<exists>(z ::'a::{linorder}).\<forall>x<z.(x \<noteq> t) = True"
    29   "\<exists>(z ::'a::{linorder}).\<forall>x<z.(x < t) = True"
    30   "\<exists>(z ::'a::{linorder}).\<forall>x<z.(x \<le> t) = True"
    31   "\<exists>(z ::'a::{linorder}).\<forall>x<z.(x > t) = False"
    32   "\<exists>(z ::'a::{linorder}).\<forall>x<z.(x \<ge> t) = False"
    33   "\<exists>z.\<forall>(x::'a::{linorder,plus,times})<z. (d dvd x + s) = (d dvd x + s)"
    34   "\<exists>z.\<forall>(x::'a::{linorder,plus,times})<z. (\<not> d dvd x + s) = (\<not> d dvd x + s)"
    35   "\<exists>z.\<forall>x<z. F = F"
    36   by ((erule exE, erule exE,rule_tac x="min z za" in exI,simp)+, (rule_tac x="t" in exI,fastsimp)+) simp_all
    37 
    38 lemma pinf:
    39   "\<lbrakk>\<exists>(z ::'a::linorder).\<forall>x>z. P x = P' x; \<exists>z.\<forall>x>z. Q x = Q' x\<rbrakk> 
    40      \<Longrightarrow> \<exists>z.\<forall>x>z. (P x \<and> Q x) = (P' x \<and> Q' x)"
    41   "\<lbrakk>\<exists>(z ::'a::linorder).\<forall>x>z. P x = P' x; \<exists>z.\<forall>x>z. Q x = Q' x\<rbrakk> 
    42      \<Longrightarrow> \<exists>z.\<forall>x>z. (P x \<or> Q x) = (P' x \<or> Q' x)"
    43   "\<exists>(z ::'a::{linorder}).\<forall>x>z.(x = t) = False"
    44   "\<exists>(z ::'a::{linorder}).\<forall>x>z.(x \<noteq> t) = True"
    45   "\<exists>(z ::'a::{linorder}).\<forall>x>z.(x < t) = False"
    46   "\<exists>(z ::'a::{linorder}).\<forall>x>z.(x \<le> t) = False"
    47   "\<exists>(z ::'a::{linorder}).\<forall>x>z.(x > t) = True"
    48   "\<exists>(z ::'a::{linorder}).\<forall>x>z.(x \<ge> t) = True"
    49   "\<exists>z.\<forall>(x::'a::{linorder,plus,times})>z. (d dvd x + s) = (d dvd x + s)"
    50   "\<exists>z.\<forall>(x::'a::{linorder,plus,times})>z. (\<not> d dvd x + s) = (\<not> d dvd x + s)"
    51   "\<exists>z.\<forall>x>z. F = F"
    52   by ((erule exE, erule exE,rule_tac x="max z za" in exI,simp)+,(rule_tac x="t" in exI,fastsimp)+) simp_all
    53 
    54 lemma inf_period:
    55   "\<lbrakk>\<forall>x k. P x = P (x - k*D); \<forall>x k. Q x = Q (x - k*D)\<rbrakk> 
    56     \<Longrightarrow> \<forall>x k. (P x \<and> Q x) = (P (x - k*D) \<and> Q (x - k*D))"
    57   "\<lbrakk>\<forall>x k. P x = P (x - k*D); \<forall>x k. Q x = Q (x - k*D)\<rbrakk> 
    58     \<Longrightarrow> \<forall>x k. (P x \<or> Q x) = (P (x - k*D) \<or> Q (x - k*D))"
    59   "(d::'a::{comm_ring}) dvd D \<Longrightarrow> \<forall>x k. (d dvd x + t) = (d dvd (x - k*D) + t)"
    60   "(d::'a::{comm_ring}) dvd D \<Longrightarrow> \<forall>x k. (\<not>d dvd x + t) = (\<not>d dvd (x - k*D) + t)"
    61   "\<forall>x k. F = F"
    62 by simp_all
    63   (clarsimp simp add: dvd_def, rule iffI, clarsimp,rule_tac x = "kb - ka*k" in exI,
    64     simp add: ring_eq_simps, clarsimp,rule_tac x = "kb + ka*k" in exI,simp add: ring_eq_simps)+
    65 
    66 section{* The A and B sets *}
    67 lemma bset:
    68   "\<lbrakk>\<forall>x.(\<forall>j \<in> {1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> P x \<longrightarrow> P(x - D) ;
    69      \<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> Q x \<longrightarrow> Q(x - D)\<rbrakk> \<Longrightarrow> 
    70   \<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j) \<longrightarrow> (P x \<and> Q x) \<longrightarrow> (P(x - D) \<and> Q (x - D))"
    71   "\<lbrakk>\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> P x \<longrightarrow> P(x - D) ;
    72      \<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> Q x \<longrightarrow> Q(x - D)\<rbrakk> \<Longrightarrow> 
    73   \<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (P x \<or> Q x) \<longrightarrow> (P(x - D) \<or> Q (x - D))"
    74   "\<lbrakk>D>0; t - 1\<in> B\<rbrakk> \<Longrightarrow> (\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (x = t) \<longrightarrow> (x - D = t))"
    75   "\<lbrakk>D>0 ; t \<in> B\<rbrakk> \<Longrightarrow>(\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (x \<noteq> t) \<longrightarrow> (x - D \<noteq> t))"
    76   "D>0 \<Longrightarrow> (\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (x < t) \<longrightarrow> (x - D < t))"
    77   "D>0 \<Longrightarrow> (\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (x \<le> t) \<longrightarrow> (x - D \<le> t))"
    78   "\<lbrakk>D>0 ; t \<in> B\<rbrakk> \<Longrightarrow>(\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (x > t) \<longrightarrow> (x - D > t))"
    79   "\<lbrakk>D>0 ; t - 1 \<in> B\<rbrakk> \<Longrightarrow>(\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (x \<ge> t) \<longrightarrow> (x - D \<ge> t))"
    80   "d dvd D \<Longrightarrow>(\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (d dvd x+t) \<longrightarrow> (d dvd (x - D) + t))"
    81   "d dvd D \<Longrightarrow>(\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (\<not>d dvd x+t) \<longrightarrow> (\<not> d dvd (x - D) + t))"
    82   "\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j) \<longrightarrow> F \<longrightarrow> F"
    83 proof (blast, blast)
    84   assume dp: "D > 0" and tB: "t - 1\<in> B"
    85   show "(\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (x = t) \<longrightarrow> (x - D = t))" 
    86     apply (rule allI, rule impI,erule ballE[where x="1"],erule ballE[where x="t - 1"])
    87     using dp tB by simp_all
    88 next
    89   assume dp: "D > 0" and tB: "t \<in> B"
    90   show "(\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (x \<noteq> t) \<longrightarrow> (x - D \<noteq> t))" 
    91     apply (rule allI, rule impI,erule ballE[where x="D"],erule ballE[where x="t"])
    92     using dp tB by simp_all
    93 next
    94   assume dp: "D > 0" thus "(\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (x < t) \<longrightarrow> (x - D < t))" by arith
    95 next
    96   assume dp: "D > 0" thus "\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (x \<le> t) \<longrightarrow> (x - D \<le> t)" by arith
    97 next
    98   assume dp: "D > 0" and tB:"t \<in> B"
    99   {fix x assume nob: "\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j" and g: "x > t" and ng: "\<not> (x - D) > t"
   100     hence "x -t \<le> D" and "1 \<le> x - t" by simp+
   101       hence "\<exists>j \<in> {1 .. D}. x - t = j" by auto
   102       hence "\<exists>j \<in> {1 .. D}. x = t + j" by (simp add: ring_eq_simps)
   103       with nob tB have "False" by simp}
   104   thus "\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (x > t) \<longrightarrow> (x - D > t)" by blast
   105 next
   106   assume dp: "D > 0" and tB:"t - 1\<in> B"
   107   {fix x assume nob: "\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j" and g: "x \<ge> t" and ng: "\<not> (x - D) \<ge> t"
   108     hence "x - (t - 1) \<le> D" and "1 \<le> x - (t - 1)" by simp+
   109       hence "\<exists>j \<in> {1 .. D}. x - (t - 1) = j" by auto
   110       hence "\<exists>j \<in> {1 .. D}. x = (t - 1) + j" by (simp add: ring_eq_simps)
   111       with nob tB have "False" by simp}
   112   thus "\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (x \<ge> t) \<longrightarrow> (x - D \<ge> t)" by blast
   113 next
   114   assume d: "d dvd D"
   115   {fix x assume H: "d dvd x + t" with d have "d dvd (x - D) + t"
   116       by (clarsimp simp add: dvd_def,rule_tac x= "ka - k" in exI,simp add: ring_eq_simps)}
   117   thus "\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (d dvd x+t) \<longrightarrow> (d dvd (x - D) + t)" by simp
   118 next
   119   assume d: "d dvd D"
   120   {fix x assume H: "\<not>(d dvd x + t)" with d have "\<not>d dvd (x - D) + t"
   121       by (clarsimp simp add: dvd_def,erule_tac x= "ka + k" in allE,simp add: ring_eq_simps)}
   122   thus "\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (\<not>d dvd x+t) \<longrightarrow> (\<not>d dvd (x - D) + t)" by auto
   123 qed blast
   124 
   125 lemma aset:
   126   "\<lbrakk>\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> P x \<longrightarrow> P(x + D) ;
   127      \<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> Q x \<longrightarrow> Q(x + D)\<rbrakk> \<Longrightarrow> 
   128   \<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j) \<longrightarrow> (P x \<and> Q x) \<longrightarrow> (P(x + D) \<and> Q (x + D))"
   129   "\<lbrakk>\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> P x \<longrightarrow> P(x + D) ;
   130      \<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> Q x \<longrightarrow> Q(x + D)\<rbrakk> \<Longrightarrow> 
   131   \<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> (P x \<or> Q x) \<longrightarrow> (P(x + D) \<or> Q (x + D))"
   132   "\<lbrakk>D>0; t + 1\<in> A\<rbrakk> \<Longrightarrow> (\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> (x = t) \<longrightarrow> (x + D = t))"
   133   "\<lbrakk>D>0 ; t \<in> A\<rbrakk> \<Longrightarrow>(\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> (x \<noteq> t) \<longrightarrow> (x + D \<noteq> t))"
   134   "\<lbrakk>D>0; t\<in> A\<rbrakk> \<Longrightarrow>(\<forall>(x::int). (\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> (x < t) \<longrightarrow> (x + D < t))"
   135   "\<lbrakk>D>0; t + 1 \<in> A\<rbrakk> \<Longrightarrow> (\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> (x \<le> t) \<longrightarrow> (x + D \<le> t))"
   136   "D>0 \<Longrightarrow>(\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> (x > t) \<longrightarrow> (x + D > t))"
   137   "D>0 \<Longrightarrow>(\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> (x \<ge> t) \<longrightarrow> (x + D \<ge> t))"
   138   "d dvd D \<Longrightarrow>(\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> (d dvd x+t) \<longrightarrow> (d dvd (x + D) + t))"
   139   "d dvd D \<Longrightarrow>(\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> (\<not>d dvd x+t) \<longrightarrow> (\<not> d dvd (x + D) + t))"
   140   "\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j) \<longrightarrow> F \<longrightarrow> F"
   141 proof (blast, blast)
   142   assume dp: "D > 0" and tA: "t + 1 \<in> A"
   143   show "(\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> (x = t) \<longrightarrow> (x + D = t))" 
   144     apply (rule allI, rule impI,erule ballE[where x="1"],erule ballE[where x="t + 1"])
   145     using dp tA by simp_all
   146 next
   147   assume dp: "D > 0" and tA: "t \<in> A"
   148   show "(\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> (x \<noteq> t) \<longrightarrow> (x + D \<noteq> t))" 
   149     apply (rule allI, rule impI,erule ballE[where x="D"],erule ballE[where x="t"])
   150     using dp tA by simp_all
   151 next
   152   assume dp: "D > 0" thus "(\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> (x > t) \<longrightarrow> (x + D > t))" by arith
   153 next
   154   assume dp: "D > 0" thus "\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> (x \<ge> t) \<longrightarrow> (x + D \<ge> t)" by arith
   155 next
   156   assume dp: "D > 0" and tA:"t \<in> A"
   157   {fix x assume nob: "\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j" and g: "x < t" and ng: "\<not> (x + D) < t"
   158     hence "t - x \<le> D" and "1 \<le> t - x" by simp+
   159       hence "\<exists>j \<in> {1 .. D}. t - x = j" by auto
   160       hence "\<exists>j \<in> {1 .. D}. x = t - j" by (auto simp add: ring_eq_simps) 
   161       with nob tA have "False" by simp}
   162   thus "\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> (x < t) \<longrightarrow> (x + D < t)" by blast
   163 next
   164   assume dp: "D > 0" and tA:"t + 1\<in> A"
   165   {fix x assume nob: "\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j" and g: "x \<le> t" and ng: "\<not> (x + D) \<le> t"
   166     hence "(t + 1) - x \<le> D" and "1 \<le> (t + 1) - x" by (simp_all add: ring_eq_simps)
   167       hence "\<exists>j \<in> {1 .. D}. (t + 1) - x = j" by auto
   168       hence "\<exists>j \<in> {1 .. D}. x = (t + 1) - j" by (auto simp add: ring_eq_simps)
   169       with nob tA have "False" by simp}
   170   thus "\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> (x \<le> t) \<longrightarrow> (x + D \<le> t)" by blast
   171 next
   172   assume d: "d dvd D"
   173   {fix x assume H: "d dvd x + t" with d have "d dvd (x + D) + t"
   174       by (clarsimp simp add: dvd_def,rule_tac x= "ka + k" in exI,simp add: ring_eq_simps)}
   175   thus "\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> (d dvd x+t) \<longrightarrow> (d dvd (x + D) + t)" by simp
   176 next
   177   assume d: "d dvd D"
   178   {fix x assume H: "\<not>(d dvd x + t)" with d have "\<not>d dvd (x + D) + t"
   179       by (clarsimp simp add: dvd_def,erule_tac x= "ka - k" in allE,simp add: ring_eq_simps)}
   180   thus "\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> (\<not>d dvd x+t) \<longrightarrow> (\<not>d dvd (x + D) + t)" by auto
   181 qed blast
   182 
   183 subsection{* Cooper's Theorem @{text "-\<infinity>"} and @{text "+\<infinity>"} Version *}
   184 
   185 subsubsection{* First some trivial facts about periodic sets or predicates *}
   186 lemma periodic_finite_ex:
   187   assumes dpos: "(0::int) < d" and modd: "ALL x k. P x = P(x - k*d)"
   188   shows "(EX x. P x) = (EX j : {1..d}. P j)"
   189   (is "?LHS = ?RHS")
   190 proof
   191   assume ?LHS
   192   then obtain x where P: "P x" ..
   193   have "x mod d = x - (x div d)*d" by(simp add:zmod_zdiv_equality mult_ac eq_diff_eq)
   194   hence Pmod: "P x = P(x mod d)" using modd by simp
   195   show ?RHS
   196   proof (cases)
   197     assume "x mod d = 0"
   198     hence "P 0" using P Pmod by simp
   199     moreover have "P 0 = P(0 - (-1)*d)" using modd by blast
   200     ultimately have "P d" by simp
   201     moreover have "d : {1..d}" using dpos by(simp add:atLeastAtMost_iff)
   202     ultimately show ?RHS ..
   203   next
   204     assume not0: "x mod d \<noteq> 0"
   205     have "P(x mod d)" using dpos P Pmod by(simp add:pos_mod_sign pos_mod_bound)
   206     moreover have "x mod d : {1..d}"
   207     proof -
   208       from dpos have "0 \<le> x mod d" by(rule pos_mod_sign)
   209       moreover from dpos have "x mod d < d" by(rule pos_mod_bound)
   210       ultimately show ?thesis using not0 by(simp add:atLeastAtMost_iff)
   211     qed
   212     ultimately show ?RHS ..
   213   qed
   214 qed auto
   215 
   216 subsubsection{* The @{text "-\<infinity>"} Version*}
   217 
   218 lemma decr_lemma: "0 < (d::int) \<Longrightarrow> x - (abs(x-z)+1) * d < z"
   219 by(induct rule: int_gr_induct,simp_all add:int_distrib)
   220 
   221 lemma incr_lemma: "0 < (d::int) \<Longrightarrow> z < x + (abs(x-z)+1) * d"
   222 by(induct rule: int_gr_induct, simp_all add:int_distrib)
   223 
   224 theorem int_induct[case_names base step1 step2]:
   225   assumes 
   226   base: "P(k::int)" and step1: "\<And>i. \<lbrakk>k \<le> i; P i\<rbrakk> \<Longrightarrow> P(i+1)" and
   227   step2: "\<And>i. \<lbrakk>k \<ge> i; P i\<rbrakk> \<Longrightarrow> P(i - 1)"
   228   shows "P i"
   229 proof -
   230   have "i \<le> k \<or> i\<ge> k" by arith
   231   thus ?thesis using prems int_ge_induct[where P="P" and k="k" and i="i"] int_le_induct[where P="P" and k="k" and i="i"] by blast
   232 qed
   233 
   234 lemma decr_mult_lemma:
   235   assumes dpos: "(0::int) < d" and minus: "\<forall>x. P x \<longrightarrow> P(x - d)" and knneg: "0 <= k"
   236   shows "ALL x. P x \<longrightarrow> P(x - k*d)"
   237 using knneg
   238 proof (induct rule:int_ge_induct)
   239   case base thus ?case by simp
   240 next
   241   case (step i)
   242   {fix x
   243     have "P x \<longrightarrow> P (x - i * d)" using step.hyps by blast
   244     also have "\<dots> \<longrightarrow> P(x - (i + 1) * d)" using minus[THEN spec, of "x - i * d"]
   245       by (simp add:int_distrib OrderedGroup.diff_diff_eq[symmetric])
   246     ultimately have "P x \<longrightarrow> P(x - (i + 1) * d)" by blast}
   247   thus ?case ..
   248 qed
   249 
   250 lemma  minusinfinity:
   251   assumes dpos: "0 < d" and
   252     P1eqP1: "ALL x k. P1 x = P1(x - k*d)" and ePeqP1: "EX z::int. ALL x. x < z \<longrightarrow> (P x = P1 x)"
   253   shows "(EX x. P1 x) \<longrightarrow> (EX x. P x)"
   254 proof
   255   assume eP1: "EX x. P1 x"
   256   then obtain x where P1: "P1 x" ..
   257   from ePeqP1 obtain z where P1eqP: "ALL x. x < z \<longrightarrow> (P x = P1 x)" ..
   258   let ?w = "x - (abs(x-z)+1) * d"
   259   from dpos have w: "?w < z" by(rule decr_lemma)
   260   have "P1 x = P1 ?w" using P1eqP1 by blast
   261   also have "\<dots> = P(?w)" using w P1eqP by blast
   262   finally have "P ?w" using P1 by blast
   263   thus "EX x. P x" ..
   264 qed
   265 
   266 lemma cpmi: 
   267   assumes dp: "0 < D" and p1:"\<exists>z. \<forall> x< z. P x = P' x"
   268   and nb:"\<forall>x.(\<forall> j\<in> {1..D}. \<forall>(b::int) \<in> B. x \<noteq> b+j) --> P (x) --> P (x - D)"
   269   and pd: "\<forall> x k. P' x = P' (x-k*D)"
   270   shows "(\<exists>x. P x) = ((\<exists> j\<in> {1..D} . P' j) | (\<exists> j \<in> {1..D}.\<exists> b\<in> B. P (b+j)))" 
   271          (is "?L = (?R1 \<or> ?R2)")
   272 proof-
   273  {assume "?R2" hence "?L"  by blast}
   274  moreover
   275  {assume H:"?R1" hence "?L" using minusinfinity[OF dp pd p1] periodic_finite_ex[OF dp pd] by simp}
   276  moreover 
   277  { fix x
   278    assume P: "P x" and H: "\<not> ?R2"
   279    {fix y assume "\<not> (\<exists>j\<in>{1..D}. \<exists>b\<in>B. P (b + j))" and P: "P y"
   280      hence "~(EX (j::int) : {1..D}. EX (b::int) : B. y = b+j)" by auto
   281      with nb P  have "P (y - D)" by auto }
   282    hence "ALL x.~(EX (j::int) : {1..D}. EX (b::int) : B. P(b+j)) --> P (x) --> P (x - D)" by blast
   283    with H P have th: " \<forall>x. P x \<longrightarrow> P (x - D)" by auto
   284    from p1 obtain z where z: "ALL x. x < z --> (P x = P' x)" by blast
   285    let ?y = "x - (\<bar>x - z\<bar> + 1)*D"
   286    have zp: "0 <= (\<bar>x - z\<bar> + 1)" by arith
   287    from dp have yz: "?y < z" using decr_lemma[OF dp] by simp   
   288    from z[rule_format, OF yz] decr_mult_lemma[OF dp th zp, rule_format, OF P] have th2: " P' ?y" by auto
   289    with periodic_finite_ex[OF dp pd]
   290    have "?R1" by blast}
   291  ultimately show ?thesis by blast
   292 qed
   293 
   294 subsubsection {* The @{text "+\<infinity>"} Version*}
   295 
   296 lemma  plusinfinity:
   297   assumes dpos: "(0::int) < d" and
   298     P1eqP1: "\<forall>x k. P' x = P'(x - k*d)" and ePeqP1: "\<exists> z. \<forall> x>z. P x = P' x"
   299   shows "(\<exists> x. P' x) \<longrightarrow> (\<exists> x. P x)"
   300 proof
   301   assume eP1: "EX x. P' x"
   302   then obtain x where P1: "P' x" ..
   303   from ePeqP1 obtain z where P1eqP: "\<forall>x>z. P x = P' x" ..
   304   let ?w' = "x + (abs(x-z)+1) * d"
   305   let ?w = "x - (-(abs(x-z) + 1))*d"
   306   have ww'[simp]: "?w = ?w'" by (simp add: ring_eq_simps)
   307   from dpos have w: "?w > z" by(simp only: ww' incr_lemma)
   308   hence "P' x = P' ?w" using P1eqP1 by blast
   309   also have "\<dots> = P(?w)" using w P1eqP by blast
   310   finally have "P ?w" using P1 by blast
   311   thus "EX x. P x" ..
   312 qed
   313 
   314 lemma incr_mult_lemma:
   315   assumes dpos: "(0::int) < d" and plus: "ALL x::int. P x \<longrightarrow> P(x + d)" and knneg: "0 <= k"
   316   shows "ALL x. P x \<longrightarrow> P(x + k*d)"
   317 using knneg
   318 proof (induct rule:int_ge_induct)
   319   case base thus ?case by simp
   320 next
   321   case (step i)
   322   {fix x
   323     have "P x \<longrightarrow> P (x + i * d)" using step.hyps by blast
   324     also have "\<dots> \<longrightarrow> P(x + (i + 1) * d)" using plus[THEN spec, of "x + i * d"]
   325       by (simp add:int_distrib zadd_ac)
   326     ultimately have "P x \<longrightarrow> P(x + (i + 1) * d)" by blast}
   327   thus ?case ..
   328 qed
   329 
   330 lemma cppi: 
   331   assumes dp: "0 < D" and p1:"\<exists>z. \<forall> x> z. P x = P' x"
   332   and nb:"\<forall>x.(\<forall> j\<in> {1..D}. \<forall>(b::int) \<in> A. x \<noteq> b - j) --> P (x) --> P (x + D)"
   333   and pd: "\<forall> x k. P' x= P' (x-k*D)"
   334   shows "(\<exists>x. P x) = ((\<exists> j\<in> {1..D} . P' j) | (\<exists> j \<in> {1..D}.\<exists> b\<in> A. P (b - j)))" (is "?L = (?R1 \<or> ?R2)")
   335 proof-
   336  {assume "?R2" hence "?L"  by blast}
   337  moreover
   338  {assume H:"?R1" hence "?L" using plusinfinity[OF dp pd p1] periodic_finite_ex[OF dp pd] by simp}
   339  moreover 
   340  { fix x
   341    assume P: "P x" and H: "\<not> ?R2"
   342    {fix y assume "\<not> (\<exists>j\<in>{1..D}. \<exists>b\<in>A. P (b - j))" and P: "P y"
   343      hence "~(EX (j::int) : {1..D}. EX (b::int) : A. y = b - j)" by auto
   344      with nb P  have "P (y + D)" by auto }
   345    hence "ALL x.~(EX (j::int) : {1..D}. EX (b::int) : A. P(b-j)) --> P (x) --> P (x + D)" by blast
   346    with H P have th: " \<forall>x. P x \<longrightarrow> P (x + D)" by auto
   347    from p1 obtain z where z: "ALL x. x > z --> (P x = P' x)" by blast
   348    let ?y = "x + (\<bar>x - z\<bar> + 1)*D"
   349    have zp: "0 <= (\<bar>x - z\<bar> + 1)" by arith
   350    from dp have yz: "?y > z" using incr_lemma[OF dp] by simp
   351    from z[rule_format, OF yz] incr_mult_lemma[OF dp th zp, rule_format, OF P] have th2: " P' ?y" by auto
   352    with periodic_finite_ex[OF dp pd]
   353    have "?R1" by blast}
   354  ultimately show ?thesis by blast
   355 qed
   356 
   357 lemma simp_from_to: "{i..j::int} = (if j < i then {} else insert i {i+1..j})"
   358 apply(simp add:atLeastAtMost_def atLeast_def atMost_def)
   359 apply(fastsimp)
   360 done
   361 
   362 theorem unity_coeff_ex: "(\<exists>(x::'a::{semiring_0}). P (l * x)) \<equiv> (\<exists>x. l dvd (x + 0) \<and> P x)"
   363   apply (rule eq_reflection[symmetric])
   364   apply (rule iffI)
   365   defer
   366   apply (erule exE)
   367   apply (rule_tac x = "l * x" in exI)
   368   apply (simp add: dvd_def)
   369   apply (rule_tac x="x" in exI, simp)
   370   apply (erule exE)
   371   apply (erule conjE)
   372   apply (erule dvdE)
   373   apply (rule_tac x = k in exI)
   374   apply simp
   375   done
   376 
   377 lemma zdvd_mono: assumes not0: "(k::int) \<noteq> 0"
   378 shows "((m::int) dvd t) \<equiv> (k*m dvd k*t)" 
   379   using not0 by (simp add: dvd_def)
   380 
   381 lemma uminus_dvd_conv: "(d dvd (t::int)) \<equiv> (-d dvd t)" "(d dvd (t::int)) \<equiv> (d dvd -t)"
   382   by simp_all
   383 text {* \bigskip Theorems for transforming predicates on nat to predicates on @{text int}*}
   384 lemma all_nat: "(\<forall>x::nat. P x) = (\<forall>x::int. 0 <= x \<longrightarrow> P (nat x))"
   385   by (simp split add: split_nat)
   386 
   387 lemma ex_nat: "(\<exists>x::nat. P x) = (\<exists>x::int. 0 <= x \<and> P (nat x))"
   388   apply (auto split add: split_nat)
   389   apply (rule_tac x="int x" in exI, simp)
   390   apply (rule_tac x = "nat x" in exI,erule_tac x = "nat x" in allE, simp)
   391   done
   392 
   393 lemma zdiff_int_split: "P (int (x - y)) =
   394   ((y \<le> x \<longrightarrow> P (int x - int y)) \<and> (x < y \<longrightarrow> P 0))"
   395   by (case_tac "y \<le> x", simp_all add: zdiff_int)
   396 
   397 lemma number_of1: "(0::int) <= number_of n \<Longrightarrow> (0::int) <= number_of (n BIT b)" by simp
   398 lemma number_of2: "(0::int) <= Numeral0" by simp
   399 lemma Suc_plus1: "Suc n = n + 1" by simp
   400 
   401 text {*
   402   \medskip Specific instances of congruence rules, to prevent
   403   simplifier from looping. *}
   404 
   405 theorem imp_le_cong: "(0 <= x \<Longrightarrow> P = P') \<Longrightarrow> (0 <= (x::int) \<longrightarrow> P) = (0 <= x \<longrightarrow> P')" by simp
   406 
   407 theorem conj_le_cong: "(0 <= x \<Longrightarrow> P = P') \<Longrightarrow> (0 <= (x::int) \<and> P) = (0 <= x \<and> P')" 
   408   by (simp cong: conj_cong)
   409 lemma int_eq_number_of_eq:
   410   "(((number_of v)::int) = (number_of w)) = iszero ((number_of (v + (uminus w)))::int)"
   411   by simp
   412 
   413 lemma mod_eq0_dvd_iff[presburger]: "(m::nat) mod n = 0 \<longleftrightarrow> n dvd m"
   414 unfolding dvd_eq_mod_eq_0[symmetric] ..
   415 
   416 lemma zmod_eq0_zdvd_iff[presburger]: "(m::int) mod n = 0 \<longleftrightarrow> n dvd m"
   417 unfolding zdvd_iff_zmod_eq_0[symmetric] ..
   418 declare mod_1[presburger]
   419 declare mod_0[presburger]
   420 declare zmod_1[presburger]
   421 declare zmod_zero[presburger]
   422 declare zmod_self[presburger]
   423 declare mod_self[presburger]
   424 declare DIVISION_BY_ZERO_MOD[presburger]
   425 declare nat_mod_div_trivial[presburger]
   426 declare div_mod_equality2[presburger]
   427 declare div_mod_equality[presburger]
   428 declare mod_div_equality2[presburger]
   429 declare mod_div_equality[presburger]
   430 declare mod_mult_self1[presburger]
   431 declare mod_mult_self2[presburger]
   432 declare zdiv_zmod_equality2[presburger]
   433 declare zdiv_zmod_equality[presburger]
   434 declare mod2_Suc_Suc[presburger]
   435 lemma [presburger]: "(a::int) div 0 = 0" and [presburger]: "a mod 0 = a"
   436 using IntDiv.DIVISION_BY_ZERO by blast+
   437 
   438 use "Tools/Presburger/cooper.ML"
   439 oracle linzqe_oracle ("term") = Coopereif.cooper_oracle
   440 
   441 use "Tools/Presburger/presburger.ML"
   442 
   443 setup {* 
   444   arith_tactic_add 
   445     (mk_arith_tactic "presburger" (fn i => fn st =>
   446        (warning "Trying Presburger arithmetic ...";   
   447     Presburger.cooper_tac true [] [] ((ProofContext.init o theory_of_thm) st) i st)))
   448   (* FIXME!!!!!!! get the right context!!*)	
   449 *}
   450 
   451 method_setup presburger = {*
   452 let
   453  fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ()
   454  fun simple_keyword k = Scan.lift (Args.$$$ k) >> K ()
   455  val addN = "add"
   456  val delN = "del"
   457  val elimN = "elim"
   458  val any_keyword = keyword addN || keyword delN || simple_keyword elimN
   459  val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
   460 in
   461   fn src => Method.syntax 
   462    ((Scan.optional (simple_keyword elimN >> K false) true) -- 
   463     (Scan.optional (keyword addN |-- thms) []) -- 
   464     (Scan.optional (keyword delN |-- thms) [])) src 
   465   #> (fn (((elim, add_ths), del_ths),ctxt) => 
   466          Method.SIMPLE_METHOD' (Presburger.cooper_tac elim add_ths del_ths ctxt))
   467 end
   468 *} "Cooper's algorithm for Presburger arithmetic"
   469 
   470 lemma [presburger]: "m mod 2 = (1::nat) \<longleftrightarrow> \<not> 2 dvd m " by presburger
   471 lemma [presburger]: "m mod 2 = Suc 0 \<longleftrightarrow> \<not> 2 dvd m " by presburger
   472 lemma [presburger]: "m mod (Suc (Suc 0)) = (1::nat) \<longleftrightarrow> \<not> 2 dvd m " by presburger
   473 lemma [presburger]: "m mod (Suc (Suc 0)) = Suc 0 \<longleftrightarrow> \<not> 2 dvd m " by presburger
   474 lemma [presburger]: "m mod 2 = (1::int) \<longleftrightarrow> \<not> 2 dvd m " by presburger
   475 
   476 
   477 subsection {* Code generator setup *}
   478 
   479 text {*
   480   Presburger arithmetic is convenient to prove some
   481   of the following code lemmas on integer numerals:
   482 *}
   483 
   484 lemma eq_Pls_Pls:
   485   "Numeral.Pls = Numeral.Pls \<longleftrightarrow> True" by presburger
   486 
   487 lemma eq_Pls_Min:
   488   "Numeral.Pls = Numeral.Min \<longleftrightarrow> False"
   489   unfolding Pls_def Numeral.Min_def by presburger
   490 
   491 lemma eq_Pls_Bit0:
   492   "Numeral.Pls = Numeral.Bit k bit.B0 \<longleftrightarrow> Numeral.Pls = k"
   493   unfolding Pls_def Bit_def bit.cases by presburger
   494 
   495 lemma eq_Pls_Bit1:
   496   "Numeral.Pls = Numeral.Bit k bit.B1 \<longleftrightarrow> False"
   497   unfolding Pls_def Bit_def bit.cases by presburger
   498 
   499 lemma eq_Min_Pls:
   500   "Numeral.Min = Numeral.Pls \<longleftrightarrow> False"
   501   unfolding Pls_def Numeral.Min_def by presburger
   502 
   503 lemma eq_Min_Min:
   504   "Numeral.Min = Numeral.Min \<longleftrightarrow> True" by presburger
   505 
   506 lemma eq_Min_Bit0:
   507   "Numeral.Min = Numeral.Bit k bit.B0 \<longleftrightarrow> False"
   508   unfolding Numeral.Min_def Bit_def bit.cases by presburger
   509 
   510 lemma eq_Min_Bit1:
   511   "Numeral.Min = Numeral.Bit k bit.B1 \<longleftrightarrow> Numeral.Min = k"
   512   unfolding Numeral.Min_def Bit_def bit.cases by presburger
   513 
   514 lemma eq_Bit0_Pls:
   515   "Numeral.Bit k bit.B0 = Numeral.Pls \<longleftrightarrow> Numeral.Pls = k"
   516   unfolding Pls_def Bit_def bit.cases by presburger
   517 
   518 lemma eq_Bit1_Pls:
   519   "Numeral.Bit k bit.B1 = Numeral.Pls \<longleftrightarrow> False"
   520   unfolding Pls_def Bit_def bit.cases  by presburger
   521 
   522 lemma eq_Bit0_Min:
   523   "Numeral.Bit k bit.B0 = Numeral.Min \<longleftrightarrow> False"
   524   unfolding Numeral.Min_def Bit_def bit.cases  by presburger
   525 
   526 lemma eq_Bit1_Min:
   527   "(Numeral.Bit k bit.B1) = Numeral.Min \<longleftrightarrow> Numeral.Min = k"
   528   unfolding Numeral.Min_def Bit_def bit.cases  by presburger
   529 
   530 lemma eq_Bit_Bit:
   531   "Numeral.Bit k1 v1 = Numeral.Bit k2 v2 \<longleftrightarrow>
   532     v1 = v2 \<and> k1 = k2" 
   533   unfolding Bit_def
   534   apply (cases v1)
   535   apply (cases v2)
   536   apply auto
   537   apply presburger
   538   apply (cases v2)
   539   apply auto
   540   apply presburger
   541   apply (cases v2)
   542   apply auto
   543   done
   544 
   545 lemma eq_number_of:
   546   "(number_of k \<Colon> int) = number_of l \<longleftrightarrow> k = l" 
   547   unfolding number_of_is_id ..
   548 
   549 
   550 lemma less_eq_Pls_Pls:
   551   "Numeral.Pls \<le> Numeral.Pls \<longleftrightarrow> True" by rule+
   552 
   553 lemma less_eq_Pls_Min:
   554   "Numeral.Pls \<le> Numeral.Min \<longleftrightarrow> False"
   555   unfolding Pls_def Numeral.Min_def by presburger
   556 
   557 lemma less_eq_Pls_Bit:
   558   "Numeral.Pls \<le> Numeral.Bit k v \<longleftrightarrow> Numeral.Pls \<le> k"
   559   unfolding Pls_def Bit_def by (cases v) auto
   560 
   561 lemma less_eq_Min_Pls:
   562   "Numeral.Min \<le> Numeral.Pls \<longleftrightarrow> True"
   563   unfolding Pls_def Numeral.Min_def by presburger
   564 
   565 lemma less_eq_Min_Min:
   566   "Numeral.Min \<le> Numeral.Min \<longleftrightarrow> True" by rule+
   567 
   568 lemma less_eq_Min_Bit0:
   569   "Numeral.Min \<le> Numeral.Bit k bit.B0 \<longleftrightarrow> Numeral.Min < k"
   570   unfolding Numeral.Min_def Bit_def by auto
   571 
   572 lemma less_eq_Min_Bit1:
   573   "Numeral.Min \<le> Numeral.Bit k bit.B1 \<longleftrightarrow> Numeral.Min \<le> k"
   574   unfolding Numeral.Min_def Bit_def by auto
   575 
   576 lemma less_eq_Bit0_Pls:
   577   "Numeral.Bit k bit.B0 \<le> Numeral.Pls \<longleftrightarrow> k \<le> Numeral.Pls"
   578   unfolding Pls_def Bit_def by simp
   579 
   580 lemma less_eq_Bit1_Pls:
   581   "Numeral.Bit k bit.B1 \<le> Numeral.Pls \<longleftrightarrow> k < Numeral.Pls"
   582   unfolding Pls_def Bit_def by auto
   583 
   584 lemma less_eq_Bit_Min:
   585   "Numeral.Bit k v \<le> Numeral.Min \<longleftrightarrow> k \<le> Numeral.Min"
   586   unfolding Numeral.Min_def Bit_def by (cases v) auto
   587 
   588 lemma less_eq_Bit0_Bit:
   589   "Numeral.Bit k1 bit.B0 \<le> Numeral.Bit k2 v \<longleftrightarrow> k1 \<le> k2"
   590   unfolding Bit_def bit.cases by (cases v) auto
   591 
   592 lemma less_eq_Bit_Bit1:
   593   "Numeral.Bit k1 v \<le> Numeral.Bit k2 bit.B1 \<longleftrightarrow> k1 \<le> k2"
   594   unfolding Bit_def bit.cases by (cases v) auto
   595 
   596 lemma less_eq_Bit1_Bit0:
   597   "Numeral.Bit k1 bit.B1 \<le> Numeral.Bit k2 bit.B0 \<longleftrightarrow> k1 < k2"
   598   unfolding Bit_def by (auto split: bit.split)
   599 
   600 lemma less_eq_number_of:
   601   "(number_of k \<Colon> int) \<le> number_of l \<longleftrightarrow> k \<le> l"
   602   unfolding number_of_is_id ..
   603 
   604 
   605 lemma less_Pls_Pls:
   606   "Numeral.Pls < Numeral.Pls \<longleftrightarrow> False" by simp 
   607 
   608 lemma less_Pls_Min:
   609   "Numeral.Pls < Numeral.Min \<longleftrightarrow> False"
   610   unfolding Pls_def Numeral.Min_def  by presburger 
   611 
   612 lemma less_Pls_Bit0:
   613   "Numeral.Pls < Numeral.Bit k bit.B0 \<longleftrightarrow> Numeral.Pls < k"
   614   unfolding Pls_def Bit_def by auto
   615 
   616 lemma less_Pls_Bit1:
   617   "Numeral.Pls < Numeral.Bit k bit.B1 \<longleftrightarrow> Numeral.Pls \<le> k"
   618   unfolding Pls_def Bit_def by auto
   619 
   620 lemma less_Min_Pls:
   621   "Numeral.Min < Numeral.Pls \<longleftrightarrow> True"
   622   unfolding Pls_def Numeral.Min_def by presburger 
   623 
   624 lemma less_Min_Min:
   625   "Numeral.Min < Numeral.Min \<longleftrightarrow> False"  by simp
   626 
   627 lemma less_Min_Bit:
   628   "Numeral.Min < Numeral.Bit k v \<longleftrightarrow> Numeral.Min < k"
   629   unfolding Numeral.Min_def Bit_def by (auto split: bit.split)
   630 
   631 lemma less_Bit_Pls:
   632   "Numeral.Bit k v < Numeral.Pls \<longleftrightarrow> k < Numeral.Pls"
   633   unfolding Pls_def Bit_def by (auto split: bit.split)
   634 
   635 lemma less_Bit0_Min:
   636   "Numeral.Bit k bit.B0 < Numeral.Min \<longleftrightarrow> k \<le> Numeral.Min"
   637   unfolding Numeral.Min_def Bit_def by auto
   638 
   639 lemma less_Bit1_Min:
   640   "Numeral.Bit k bit.B1 < Numeral.Min \<longleftrightarrow> k < Numeral.Min"
   641   unfolding Numeral.Min_def Bit_def by auto
   642 
   643 lemma less_Bit_Bit0:
   644   "Numeral.Bit k1 v < Numeral.Bit k2 bit.B0 \<longleftrightarrow> k1 < k2"
   645   unfolding Bit_def by (auto split: bit.split)
   646 
   647 lemma less_Bit1_Bit:
   648   "Numeral.Bit k1 bit.B1 < Numeral.Bit k2 v \<longleftrightarrow> k1 < k2"
   649   unfolding Bit_def by (auto split: bit.split)
   650 
   651 lemma less_Bit0_Bit1:
   652   "Numeral.Bit k1 bit.B0 < Numeral.Bit k2 bit.B1 \<longleftrightarrow> k1 \<le> k2"
   653   unfolding Bit_def bit.cases  by arith
   654 
   655 lemma less_number_of:
   656   "(number_of k \<Colon> int) < number_of l \<longleftrightarrow> k < l"
   657   unfolding number_of_is_id ..
   658 
   659 lemmas pred_succ_numeral_code [code func] =
   660   arith_simps(5-12)
   661 
   662 lemmas plus_numeral_code [code func] =
   663   arith_simps(13-17)
   664   arith_simps(26-27)
   665   arith_extra_simps(1) [where 'a = int]
   666 
   667 lemmas minus_numeral_code [code func] =
   668   arith_simps(18-21)
   669   arith_extra_simps(2) [where 'a = int]
   670   arith_extra_simps(5) [where 'a = int]
   671 
   672 lemmas times_numeral_code [code func] =
   673   arith_simps(22-25)
   674   arith_extra_simps(4) [where 'a = int]
   675 
   676 lemmas eq_numeral_code [code func] =
   677   eq_Pls_Pls eq_Pls_Min eq_Pls_Bit0 eq_Pls_Bit1
   678   eq_Min_Pls eq_Min_Min eq_Min_Bit0 eq_Min_Bit1
   679   eq_Bit0_Pls eq_Bit1_Pls eq_Bit0_Min eq_Bit1_Min eq_Bit_Bit
   680   eq_number_of
   681 
   682 lemmas less_eq_numeral_code [code func] = less_eq_Pls_Pls less_eq_Pls_Min less_eq_Pls_Bit
   683   less_eq_Min_Pls less_eq_Min_Min less_eq_Min_Bit0 less_eq_Min_Bit1
   684   less_eq_Bit0_Pls less_eq_Bit1_Pls less_eq_Bit_Min less_eq_Bit0_Bit less_eq_Bit_Bit1 less_eq_Bit1_Bit0
   685   less_eq_number_of
   686 
   687 lemmas less_numeral_code [code func] = less_Pls_Pls less_Pls_Min less_Pls_Bit0
   688   less_Pls_Bit1 less_Min_Pls less_Min_Min less_Min_Bit less_Bit_Pls
   689   less_Bit0_Min less_Bit1_Min less_Bit_Bit0 less_Bit1_Bit less_Bit0_Bit1
   690   less_number_of
   691 
   692 end