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