src/HOL/Presburger.thy
author chaieb
Thu Jun 14 22:59:39 2007 +0200 (2007-06-14)
changeset 23390 01ef1135de73
parent 23389 aaca6a8e5414
child 23405 8993b3144358
permissions -rw-r--r--
Added some lemmas to default presburger simpset; 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 all_not_ex: "(ALL x. P x) = (~ (EX x. ~ P x ))"
   377 by blast
   378 
   379 lemma uminus_dvd_conv: "(d dvd (t::int)) \<equiv> (-d dvd t)" "(d dvd (t::int)) \<equiv> (d dvd -t)"
   380   by simp_all
   381 text {* \bigskip Theorems for transforming predicates on nat to predicates on @{text int}*}
   382 lemma all_nat: "(\<forall>x::nat. P x) = (\<forall>x::int. 0 <= x \<longrightarrow> P (nat x))"
   383   by (simp split add: split_nat)
   384 
   385 lemma ex_nat: "(\<exists>x::nat. P x) = (\<exists>x::int. 0 <= x \<and> P (nat x))"
   386   apply (auto split add: split_nat)
   387   apply (rule_tac x="int x" in exI, simp)
   388   apply (rule_tac x = "nat x" in exI,erule_tac x = "nat x" in allE, simp)
   389   done
   390 
   391 lemma zdiff_int_split: "P (int (x - y)) =
   392   ((y \<le> x \<longrightarrow> P (int x - int y)) \<and> (x < y \<longrightarrow> P 0))"
   393   by (case_tac "y \<le> x", simp_all)
   394 
   395 lemma number_of1: "(0::int) <= number_of n \<Longrightarrow> (0::int) <= number_of (n BIT b)" by simp
   396 lemma number_of2: "(0::int) <= Numeral0" by simp
   397 lemma Suc_plus1: "Suc n = n + 1" by simp
   398 
   399 text {*
   400   \medskip Specific instances of congruence rules, to prevent
   401   simplifier from looping. *}
   402 
   403 theorem imp_le_cong: "(0 <= x \<Longrightarrow> P = P') \<Longrightarrow> (0 <= (x::int) \<longrightarrow> P) = (0 <= x \<longrightarrow> P')" by simp
   404 
   405 theorem conj_le_cong: "(0 <= x \<Longrightarrow> P = P') \<Longrightarrow> (0 <= (x::int) \<and> P) = (0 <= x \<and> P')" 
   406   by (simp cong: conj_cong)
   407 lemma int_eq_number_of_eq:
   408   "(((number_of v)::int) = (number_of w)) = iszero ((number_of (v + (uminus w)))::int)"
   409   by simp
   410 
   411 lemma mod_eq0_dvd_iff[presburger]: "(m::nat) mod n = 0 \<longleftrightarrow> n dvd m"
   412 unfolding dvd_eq_mod_eq_0[symmetric] ..
   413 
   414 lemma zmod_eq0_zdvd_iff[presburger]: "(m::int) mod n = 0 \<longleftrightarrow> n dvd m"
   415 unfolding zdvd_iff_zmod_eq_0[symmetric] ..
   416 declare mod_1[presburger]
   417 declare mod_0[presburger]
   418 declare zmod_1[presburger]
   419 declare zmod_zero[presburger]
   420 declare zmod_self[presburger]
   421 declare mod_self[presburger]
   422 declare DIVISION_BY_ZERO_MOD[presburger]
   423 declare nat_mod_div_trivial[presburger]
   424 declare div_mod_equality2[presburger]
   425 declare div_mod_equality[presburger]
   426 declare mod_div_equality2[presburger]
   427 declare mod_div_equality[presburger]
   428 declare mod_mult_self1[presburger]
   429 declare mod_mult_self2[presburger]
   430 declare zdiv_zmod_equality2[presburger]
   431 declare zdiv_zmod_equality[presburger]
   432 declare mod2_Suc_Suc[presburger]
   433 lemma [presburger]: "(a::int) div 0 = 0" and [presburger]: "a mod 0 = a"
   434 using IntDiv.DIVISION_BY_ZERO by blast+
   435 
   436 use "Tools/Presburger/cooper.ML"
   437 oracle linzqe_oracle ("term") = Coopereif.cooper_oracle
   438 
   439 use "Tools/Presburger/presburger.ML"
   440 
   441 setup {* 
   442   arith_tactic_add 
   443     (mk_arith_tactic "presburger" (fn i => fn st =>
   444        (warning "Trying Presburger arithmetic ...";   
   445     Presburger.cooper_tac true [] [] ((ProofContext.init o theory_of_thm) st) i st)))
   446   (* FIXME!!!!!!! get the right context!!*)	
   447 *}
   448 
   449 method_setup presburger = {*
   450 let
   451  fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ()
   452  fun simple_keyword k = Scan.lift (Args.$$$ k) >> K ()
   453  val addN = "add"
   454  val delN = "del"
   455  val elimN = "elim"
   456  val any_keyword = keyword addN || keyword delN || simple_keyword elimN
   457  val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
   458 in
   459   fn src => Method.syntax 
   460    ((Scan.optional (simple_keyword elimN >> K false) true) -- 
   461     (Scan.optional (keyword addN |-- thms) []) -- 
   462     (Scan.optional (keyword delN |-- thms) [])) src 
   463   #> (fn (((elim, add_ths), del_ths),ctxt) => 
   464          Method.SIMPLE_METHOD' (Presburger.cooper_tac elim add_ths del_ths ctxt))
   465 end
   466 *} ""
   467 
   468 lemma [presburger]: "m mod 2 = (1::nat) \<longleftrightarrow> \<not> 2 dvd m " by presburger
   469 lemma [presburger]: "m mod 2 = Suc 0 \<longleftrightarrow> \<not> 2 dvd m " by presburger
   470 lemma [presburger]: "m mod (Suc (Suc 0)) = (1::nat) \<longleftrightarrow> \<not> 2 dvd m " by presburger
   471 lemma [presburger]: "m mod (Suc (Suc 0)) = Suc 0 \<longleftrightarrow> \<not> 2 dvd m " by presburger
   472 lemma [presburger]: "m mod 2 = (1::int) \<longleftrightarrow> \<not> 2 dvd m " by presburger
   473 
   474 subsection {* Code generator setup *}
   475 text {*
   476   Presburger arithmetic is convenient to prove some
   477   of the following code lemmas on integer numerals:
   478 *}
   479 
   480 lemma eq_Pls_Pls:
   481   "Numeral.Pls = Numeral.Pls \<longleftrightarrow> True" by presburger
   482 
   483 lemma eq_Pls_Min:
   484   "Numeral.Pls = Numeral.Min \<longleftrightarrow> False"
   485   unfolding Pls_def Min_def by presburger
   486 
   487 lemma eq_Pls_Bit0:
   488   "Numeral.Pls = Numeral.Bit k bit.B0 \<longleftrightarrow> Numeral.Pls = k"
   489   unfolding Pls_def Bit_def bit.cases by presburger
   490 
   491 lemma eq_Pls_Bit1:
   492   "Numeral.Pls = Numeral.Bit k bit.B1 \<longleftrightarrow> False"
   493   unfolding Pls_def Bit_def bit.cases by presburger
   494 
   495 lemma eq_Min_Pls:
   496   "Numeral.Min = Numeral.Pls \<longleftrightarrow> False"
   497   unfolding Pls_def Min_def by presburger
   498 
   499 lemma eq_Min_Min:
   500   "Numeral.Min = Numeral.Min \<longleftrightarrow> True" by presburger
   501 
   502 lemma eq_Min_Bit0:
   503   "Numeral.Min = Numeral.Bit k bit.B0 \<longleftrightarrow> False"
   504   unfolding Min_def Bit_def bit.cases by presburger
   505 
   506 lemma eq_Min_Bit1:
   507   "Numeral.Min = Numeral.Bit k bit.B1 \<longleftrightarrow> Numeral.Min = k"
   508   unfolding Min_def Bit_def bit.cases by presburger
   509 
   510 lemma eq_Bit0_Pls:
   511   "Numeral.Bit k bit.B0 = Numeral.Pls \<longleftrightarrow> Numeral.Pls = k"
   512   unfolding Pls_def Bit_def bit.cases by presburger
   513 
   514 lemma eq_Bit1_Pls:
   515   "Numeral.Bit k bit.B1 = Numeral.Pls \<longleftrightarrow> False"
   516   unfolding Pls_def Bit_def bit.cases  by presburger
   517 
   518 lemma eq_Bit0_Min:
   519   "Numeral.Bit k bit.B0 = Numeral.Min \<longleftrightarrow> False"
   520   unfolding Min_def Bit_def bit.cases  by presburger
   521 
   522 lemma eq_Bit1_Min:
   523   "(Numeral.Bit k bit.B1) = Numeral.Min \<longleftrightarrow> Numeral.Min = k"
   524   unfolding Min_def Bit_def bit.cases  by presburger
   525 
   526 lemma eq_Bit_Bit:
   527   "Numeral.Bit k1 v1 = Numeral.Bit k2 v2 \<longleftrightarrow>
   528     v1 = v2 \<and> k1 = k2" 
   529   unfolding Bit_def
   530   apply (cases v1)
   531   apply (cases v2)
   532   apply auto
   533   apply presburger
   534   apply (cases v2)
   535   apply auto
   536   apply presburger
   537   apply (cases v2)
   538   apply auto
   539 done
   540 
   541 lemma eq_number_of:
   542   "(number_of k \<Colon> int) = number_of l \<longleftrightarrow> k = l" 
   543   unfolding number_of_is_id ..
   544 
   545 
   546 lemma less_eq_Pls_Pls:
   547   "Numeral.Pls \<le> Numeral.Pls \<longleftrightarrow> True" by rule+
   548 
   549 lemma less_eq_Pls_Min:
   550   "Numeral.Pls \<le> Numeral.Min \<longleftrightarrow> False"
   551   unfolding Pls_def Min_def by presburger
   552 
   553 lemma less_eq_Pls_Bit:
   554   "Numeral.Pls \<le> Numeral.Bit k v \<longleftrightarrow> Numeral.Pls \<le> k"
   555   unfolding Pls_def Bit_def by (cases v) auto
   556 
   557 lemma less_eq_Min_Pls:
   558   "Numeral.Min \<le> Numeral.Pls \<longleftrightarrow> True"
   559   unfolding Pls_def Min_def by presburger
   560 
   561 lemma less_eq_Min_Min:
   562   "Numeral.Min \<le> Numeral.Min \<longleftrightarrow> True" by rule+
   563 
   564 lemma less_eq_Min_Bit0:
   565   "Numeral.Min \<le> Numeral.Bit k bit.B0 \<longleftrightarrow> Numeral.Min < k"
   566   unfolding Min_def Bit_def by auto
   567 
   568 lemma less_eq_Min_Bit1:
   569   "Numeral.Min \<le> Numeral.Bit k bit.B1 \<longleftrightarrow> Numeral.Min \<le> k"
   570   unfolding Min_def Bit_def by auto
   571 
   572 lemma less_eq_Bit0_Pls:
   573   "Numeral.Bit k bit.B0 \<le> Numeral.Pls \<longleftrightarrow> k \<le> Numeral.Pls"
   574   unfolding Pls_def Bit_def by simp
   575 
   576 lemma less_eq_Bit1_Pls:
   577   "Numeral.Bit k bit.B1 \<le> Numeral.Pls \<longleftrightarrow> k < Numeral.Pls"
   578   unfolding Pls_def Bit_def by auto
   579 
   580 lemma less_eq_Bit_Min:
   581   "Numeral.Bit k v \<le> Numeral.Min \<longleftrightarrow> k \<le> Numeral.Min"
   582   unfolding Min_def Bit_def by (cases v) auto
   583 
   584 lemma less_eq_Bit0_Bit:
   585   "Numeral.Bit k1 bit.B0 \<le> Numeral.Bit k2 v \<longleftrightarrow> k1 \<le> k2"
   586   unfolding Bit_def bit.cases by (cases v) auto
   587 
   588 lemma less_eq_Bit_Bit1:
   589   "Numeral.Bit k1 v \<le> Numeral.Bit k2 bit.B1 \<longleftrightarrow> k1 \<le> k2"
   590   unfolding Bit_def bit.cases by (cases v) auto
   591 
   592 lemma less_eq_Bit1_Bit0:
   593   "Numeral.Bit k1 bit.B1 \<le> Numeral.Bit k2 bit.B0 \<longleftrightarrow> k1 < k2"
   594   unfolding Bit_def by (auto split: bit.split)
   595 
   596 lemma less_eq_number_of:
   597   "(number_of k \<Colon> int) \<le> number_of l \<longleftrightarrow> k \<le> l"
   598   unfolding number_of_is_id ..
   599 
   600 
   601 lemma less_Pls_Pls:
   602   "Numeral.Pls < Numeral.Pls \<longleftrightarrow> False" by presburger 
   603 
   604 lemma less_Pls_Min:
   605   "Numeral.Pls < Numeral.Min \<longleftrightarrow> False"
   606   unfolding Pls_def Min_def  by presburger 
   607 
   608 lemma less_Pls_Bit0:
   609   "Numeral.Pls < Numeral.Bit k bit.B0 \<longleftrightarrow> Numeral.Pls < k"
   610   unfolding Pls_def Bit_def by auto
   611 
   612 lemma less_Pls_Bit1:
   613   "Numeral.Pls < Numeral.Bit k bit.B1 \<longleftrightarrow> Numeral.Pls \<le> k"
   614   unfolding Pls_def Bit_def by auto
   615 
   616 lemma less_Min_Pls:
   617   "Numeral.Min < Numeral.Pls \<longleftrightarrow> True"
   618   unfolding Pls_def Min_def by presburger 
   619 
   620 lemma less_Min_Min:
   621   "Numeral.Min < Numeral.Min \<longleftrightarrow> False"  by presburger 
   622 
   623 lemma less_Min_Bit:
   624   "Numeral.Min < Numeral.Bit k v \<longleftrightarrow> Numeral.Min < k"
   625   unfolding Min_def Bit_def by (auto split: bit.split)
   626 
   627 lemma less_Bit_Pls:
   628   "Numeral.Bit k v < Numeral.Pls \<longleftrightarrow> k < Numeral.Pls"
   629   unfolding Pls_def Bit_def by (auto split: bit.split)
   630 
   631 lemma less_Bit0_Min:
   632   "Numeral.Bit k bit.B0 < Numeral.Min \<longleftrightarrow> k \<le> Numeral.Min"
   633   unfolding Min_def Bit_def by auto
   634 
   635 lemma less_Bit1_Min:
   636   "Numeral.Bit k bit.B1 < Numeral.Min \<longleftrightarrow> k < Numeral.Min"
   637   unfolding Min_def Bit_def by auto
   638 
   639 lemma less_Bit_Bit0:
   640   "Numeral.Bit k1 v < Numeral.Bit k2 bit.B0 \<longleftrightarrow> k1 < k2"
   641   unfolding Bit_def by (auto split: bit.split)
   642 
   643 lemma less_Bit1_Bit:
   644   "Numeral.Bit k1 bit.B1 < Numeral.Bit k2 v \<longleftrightarrow> k1 < k2"
   645   unfolding Bit_def by (auto split: bit.split)
   646 
   647 lemma less_Bit0_Bit1:
   648   "Numeral.Bit k1 bit.B0 < Numeral.Bit k2 bit.B1 \<longleftrightarrow> k1 \<le> k2"
   649   unfolding Bit_def bit.cases  by arith
   650 
   651 lemma less_number_of:
   652   "(number_of k \<Colon> int) < number_of l \<longleftrightarrow> k < l"
   653   unfolding number_of_is_id ..
   654 
   655 lemmas pred_succ_numeral_code [code func] =
   656   arith_simps(5-12)
   657 
   658 lemmas plus_numeral_code [code func] =
   659   arith_simps(13-17)
   660   arith_simps(26-27)
   661   arith_extra_simps(1) [where 'a = int]
   662 
   663 lemmas minus_numeral_code [code func] =
   664   arith_simps(18-21)
   665   arith_extra_simps(2) [where 'a = int]
   666   arith_extra_simps(5) [where 'a = int]
   667 
   668 lemmas times_numeral_code [code func] =
   669   arith_simps(22-25)
   670   arith_extra_simps(4) [where 'a = int]
   671 
   672 lemmas eq_numeral_code [code func] =
   673   eq_Pls_Pls eq_Pls_Min eq_Pls_Bit0 eq_Pls_Bit1
   674   eq_Min_Pls eq_Min_Min eq_Min_Bit0 eq_Min_Bit1
   675   eq_Bit0_Pls eq_Bit1_Pls eq_Bit0_Min eq_Bit1_Min eq_Bit_Bit
   676   eq_number_of
   677 
   678 lemmas less_eq_numeral_code [code func] = less_eq_Pls_Pls less_eq_Pls_Min less_eq_Pls_Bit
   679   less_eq_Min_Pls less_eq_Min_Min less_eq_Min_Bit0 less_eq_Min_Bit1
   680   less_eq_Bit0_Pls less_eq_Bit1_Pls less_eq_Bit_Min less_eq_Bit0_Bit less_eq_Bit_Bit1 less_eq_Bit1_Bit0
   681   less_eq_number_of
   682 
   683 lemmas less_numeral_code [code func] = less_Pls_Pls less_Pls_Min less_Pls_Bit0
   684   less_Pls_Bit1 less_Min_Pls less_Min_Min less_Min_Bit less_Bit_Pls
   685   less_Bit0_Min less_Bit1_Min less_Bit_Bit0 less_Bit1_Bit less_Bit0_Bit1
   686   less_number_of
   687 
   688 end