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