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