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