src/HOL/Presburger.thy
author haftmann
Tue Jul 10 09:23:11 2007 +0200 (2007-07-10)
changeset 23685 1b0f4071946c
parent 23477 f4b83f03cac9
child 23856 ebec38420a85
permissions -rw-r--r--
moved lemma zdvd_period here
     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 lemma zdvd_period:
   477   fixes a d :: int
   478   assumes advdd: "a dvd d"
   479   shows "a dvd (x + t) \<longleftrightarrow> a dvd ((x + c * d) + t)"
   480 proof-
   481   {
   482     fix x k
   483     from inf_period(3) [OF advdd, rule_format, where x=x and k="-k"]  
   484     have "a dvd (x + t) \<longleftrightarrow> a dvd (x + k * d + t)" by simp
   485   }
   486   hence "\<forall>x.\<forall>k. ((a::int) dvd (x + t)) = (a dvd (x+k*d + t))"  by simp
   487   then show ?thesis by simp
   488 qed
   489 
   490 
   491 subsection {* Code generator setup *}
   492 
   493 text {*
   494   Presburger arithmetic is convenient to prove some
   495   of the following code lemmas on integer numerals:
   496 *}
   497 
   498 lemma eq_Pls_Pls:
   499   "Numeral.Pls = Numeral.Pls \<longleftrightarrow> True" by presburger
   500 
   501 lemma eq_Pls_Min:
   502   "Numeral.Pls = Numeral.Min \<longleftrightarrow> False"
   503   unfolding Pls_def Numeral.Min_def by presburger
   504 
   505 lemma eq_Pls_Bit0:
   506   "Numeral.Pls = Numeral.Bit k bit.B0 \<longleftrightarrow> Numeral.Pls = k"
   507   unfolding Pls_def Bit_def bit.cases by presburger
   508 
   509 lemma eq_Pls_Bit1:
   510   "Numeral.Pls = Numeral.Bit k bit.B1 \<longleftrightarrow> False"
   511   unfolding Pls_def Bit_def bit.cases by presburger
   512 
   513 lemma eq_Min_Pls:
   514   "Numeral.Min = Numeral.Pls \<longleftrightarrow> False"
   515   unfolding Pls_def Numeral.Min_def by presburger
   516 
   517 lemma eq_Min_Min:
   518   "Numeral.Min = Numeral.Min \<longleftrightarrow> True" by presburger
   519 
   520 lemma eq_Min_Bit0:
   521   "Numeral.Min = Numeral.Bit k bit.B0 \<longleftrightarrow> False"
   522   unfolding Numeral.Min_def Bit_def bit.cases by presburger
   523 
   524 lemma eq_Min_Bit1:
   525   "Numeral.Min = Numeral.Bit k bit.B1 \<longleftrightarrow> Numeral.Min = k"
   526   unfolding Numeral.Min_def Bit_def bit.cases by presburger
   527 
   528 lemma eq_Bit0_Pls:
   529   "Numeral.Bit k bit.B0 = Numeral.Pls \<longleftrightarrow> Numeral.Pls = k"
   530   unfolding Pls_def Bit_def bit.cases by presburger
   531 
   532 lemma eq_Bit1_Pls:
   533   "Numeral.Bit k bit.B1 = Numeral.Pls \<longleftrightarrow> False"
   534   unfolding Pls_def Bit_def bit.cases  by presburger
   535 
   536 lemma eq_Bit0_Min:
   537   "Numeral.Bit k bit.B0 = Numeral.Min \<longleftrightarrow> False"
   538   unfolding Numeral.Min_def Bit_def bit.cases  by presburger
   539 
   540 lemma eq_Bit1_Min:
   541   "(Numeral.Bit k bit.B1) = Numeral.Min \<longleftrightarrow> Numeral.Min = k"
   542   unfolding Numeral.Min_def Bit_def bit.cases  by presburger
   543 
   544 lemma eq_Bit_Bit:
   545   "Numeral.Bit k1 v1 = Numeral.Bit k2 v2 \<longleftrightarrow>
   546     v1 = v2 \<and> k1 = k2" 
   547   unfolding Bit_def
   548   apply (cases v1)
   549   apply (cases v2)
   550   apply auto
   551   apply presburger
   552   apply (cases v2)
   553   apply auto
   554   apply presburger
   555   apply (cases v2)
   556   apply auto
   557   done
   558 
   559 lemma eq_number_of:
   560   "(number_of k \<Colon> int) = number_of l \<longleftrightarrow> k = l" 
   561   unfolding number_of_is_id ..
   562 
   563 
   564 lemma less_eq_Pls_Pls:
   565   "Numeral.Pls \<le> Numeral.Pls \<longleftrightarrow> True" by rule+
   566 
   567 lemma less_eq_Pls_Min:
   568   "Numeral.Pls \<le> Numeral.Min \<longleftrightarrow> False"
   569   unfolding Pls_def Numeral.Min_def by presburger
   570 
   571 lemma less_eq_Pls_Bit:
   572   "Numeral.Pls \<le> Numeral.Bit k v \<longleftrightarrow> Numeral.Pls \<le> k"
   573   unfolding Pls_def Bit_def by (cases v) auto
   574 
   575 lemma less_eq_Min_Pls:
   576   "Numeral.Min \<le> Numeral.Pls \<longleftrightarrow> True"
   577   unfolding Pls_def Numeral.Min_def by presburger
   578 
   579 lemma less_eq_Min_Min:
   580   "Numeral.Min \<le> Numeral.Min \<longleftrightarrow> True" by rule+
   581 
   582 lemma less_eq_Min_Bit0:
   583   "Numeral.Min \<le> Numeral.Bit k bit.B0 \<longleftrightarrow> Numeral.Min < k"
   584   unfolding Numeral.Min_def Bit_def by auto
   585 
   586 lemma less_eq_Min_Bit1:
   587   "Numeral.Min \<le> Numeral.Bit k bit.B1 \<longleftrightarrow> Numeral.Min \<le> k"
   588   unfolding Numeral.Min_def Bit_def by auto
   589 
   590 lemma less_eq_Bit0_Pls:
   591   "Numeral.Bit k bit.B0 \<le> Numeral.Pls \<longleftrightarrow> k \<le> Numeral.Pls"
   592   unfolding Pls_def Bit_def by simp
   593 
   594 lemma less_eq_Bit1_Pls:
   595   "Numeral.Bit k bit.B1 \<le> Numeral.Pls \<longleftrightarrow> k < Numeral.Pls"
   596   unfolding Pls_def Bit_def by auto
   597 
   598 lemma less_eq_Bit_Min:
   599   "Numeral.Bit k v \<le> Numeral.Min \<longleftrightarrow> k \<le> Numeral.Min"
   600   unfolding Numeral.Min_def Bit_def by (cases v) auto
   601 
   602 lemma less_eq_Bit0_Bit:
   603   "Numeral.Bit k1 bit.B0 \<le> Numeral.Bit k2 v \<longleftrightarrow> k1 \<le> k2"
   604   unfolding Bit_def bit.cases by (cases v) auto
   605 
   606 lemma less_eq_Bit_Bit1:
   607   "Numeral.Bit k1 v \<le> Numeral.Bit k2 bit.B1 \<longleftrightarrow> k1 \<le> k2"
   608   unfolding Bit_def bit.cases by (cases v) auto
   609 
   610 lemma less_eq_Bit1_Bit0:
   611   "Numeral.Bit k1 bit.B1 \<le> Numeral.Bit k2 bit.B0 \<longleftrightarrow> k1 < k2"
   612   unfolding Bit_def by (auto split: bit.split)
   613 
   614 lemma less_eq_number_of:
   615   "(number_of k \<Colon> int) \<le> number_of l \<longleftrightarrow> k \<le> l"
   616   unfolding number_of_is_id ..
   617 
   618 
   619 lemma less_Pls_Pls:
   620   "Numeral.Pls < Numeral.Pls \<longleftrightarrow> False" by simp 
   621 
   622 lemma less_Pls_Min:
   623   "Numeral.Pls < Numeral.Min \<longleftrightarrow> False"
   624   unfolding Pls_def Numeral.Min_def  by presburger 
   625 
   626 lemma less_Pls_Bit0:
   627   "Numeral.Pls < Numeral.Bit k bit.B0 \<longleftrightarrow> Numeral.Pls < k"
   628   unfolding Pls_def Bit_def by auto
   629 
   630 lemma less_Pls_Bit1:
   631   "Numeral.Pls < Numeral.Bit k bit.B1 \<longleftrightarrow> Numeral.Pls \<le> k"
   632   unfolding Pls_def Bit_def by auto
   633 
   634 lemma less_Min_Pls:
   635   "Numeral.Min < Numeral.Pls \<longleftrightarrow> True"
   636   unfolding Pls_def Numeral.Min_def by presburger 
   637 
   638 lemma less_Min_Min:
   639   "Numeral.Min < Numeral.Min \<longleftrightarrow> False"  by simp
   640 
   641 lemma less_Min_Bit:
   642   "Numeral.Min < Numeral.Bit k v \<longleftrightarrow> Numeral.Min < k"
   643   unfolding Numeral.Min_def Bit_def by (auto split: bit.split)
   644 
   645 lemma less_Bit_Pls:
   646   "Numeral.Bit k v < Numeral.Pls \<longleftrightarrow> k < Numeral.Pls"
   647   unfolding Pls_def Bit_def by (auto split: bit.split)
   648 
   649 lemma less_Bit0_Min:
   650   "Numeral.Bit k bit.B0 < Numeral.Min \<longleftrightarrow> k \<le> Numeral.Min"
   651   unfolding Numeral.Min_def Bit_def by auto
   652 
   653 lemma less_Bit1_Min:
   654   "Numeral.Bit k bit.B1 < Numeral.Min \<longleftrightarrow> k < Numeral.Min"
   655   unfolding Numeral.Min_def Bit_def by auto
   656 
   657 lemma less_Bit_Bit0:
   658   "Numeral.Bit k1 v < Numeral.Bit k2 bit.B0 \<longleftrightarrow> k1 < k2"
   659   unfolding Bit_def by (auto split: bit.split)
   660 
   661 lemma less_Bit1_Bit:
   662   "Numeral.Bit k1 bit.B1 < Numeral.Bit k2 v \<longleftrightarrow> k1 < k2"
   663   unfolding Bit_def by (auto split: bit.split)
   664 
   665 lemma less_Bit0_Bit1:
   666   "Numeral.Bit k1 bit.B0 < Numeral.Bit k2 bit.B1 \<longleftrightarrow> k1 \<le> k2"
   667   unfolding Bit_def bit.cases  by arith
   668 
   669 lemma less_number_of:
   670   "(number_of k \<Colon> int) < number_of l \<longleftrightarrow> k < l"
   671   unfolding number_of_is_id ..
   672 
   673 lemmas pred_succ_numeral_code [code func] =
   674   arith_simps(5-12)
   675 
   676 lemmas plus_numeral_code [code func] =
   677   arith_simps(13-17)
   678   arith_simps(26-27)
   679   arith_extra_simps(1) [where 'a = int]
   680 
   681 lemmas minus_numeral_code [code func] =
   682   arith_simps(18-21)
   683   arith_extra_simps(2) [where 'a = int]
   684   arith_extra_simps(5) [where 'a = int]
   685 
   686 lemmas times_numeral_code [code func] =
   687   arith_simps(22-25)
   688   arith_extra_simps(4) [where 'a = int]
   689 
   690 lemmas eq_numeral_code [code func] =
   691   eq_Pls_Pls eq_Pls_Min eq_Pls_Bit0 eq_Pls_Bit1
   692   eq_Min_Pls eq_Min_Min eq_Min_Bit0 eq_Min_Bit1
   693   eq_Bit0_Pls eq_Bit1_Pls eq_Bit0_Min eq_Bit1_Min eq_Bit_Bit
   694   eq_number_of
   695 
   696 lemmas less_eq_numeral_code [code func] = less_eq_Pls_Pls less_eq_Pls_Min less_eq_Pls_Bit
   697   less_eq_Min_Pls less_eq_Min_Min less_eq_Min_Bit0 less_eq_Min_Bit1
   698   less_eq_Bit0_Pls less_eq_Bit1_Pls less_eq_Bit_Min less_eq_Bit0_Bit less_eq_Bit_Bit1 less_eq_Bit1_Bit0
   699   less_eq_number_of
   700 
   701 lemmas less_numeral_code [code func] = less_Pls_Pls less_Pls_Min less_Pls_Bit0
   702   less_Pls_Bit1 less_Min_Pls less_Min_Min less_Min_Bit less_Bit_Pls
   703   less_Bit0_Min less_Bit1_Min less_Bit_Bit0 less_Bit1_Bit less_Bit0_Bit1
   704   less_number_of
   705 
   706 end