src/HOL/Presburger.thy
author chaieb
Mon Jun 11 11:06:00 2007 +0200 (2007-06-11)
changeset 23314 6894137e854a
parent 23253 b1f3f53c60b5
child 23333 ec5b4ab52026
permissions -rw-r--r--
A new and cleaned up Theory for QE. for Presburger arithmetic
     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 method_setup presburger = {* Method.simple_args (Scan.optional (Args.$$$ "elim" >> K false) true)  
   440   (fn q => fn ctxt =>  Method.SIMPLE_METHOD' (Presburger.cooper_tac q ctxt))*} ""
   441 (*
   442 method_setup presburger = {*
   443   Method.ctxt_args (Method.SIMPLE_METHOD' o (Presburger.cooper_tac true))
   444 *} ""
   445 *)
   446 
   447 subsection {* Code generator setup *}
   448 text {*
   449   Presburger arithmetic is convenient to prove some
   450   of the following code lemmas on integer numerals:
   451 *}
   452 
   453 lemma eq_Pls_Pls:
   454   "Numeral.Pls = Numeral.Pls \<longleftrightarrow> True" by rule+
   455 
   456 lemma eq_Pls_Min:
   457   "Numeral.Pls = Numeral.Min \<longleftrightarrow> False"
   458   unfolding Pls_def Min_def by auto
   459 
   460 lemma eq_Pls_Bit0:
   461   "Numeral.Pls = Numeral.Bit k bit.B0 \<longleftrightarrow> Numeral.Pls = k"
   462   unfolding Pls_def Bit_def bit.cases by auto
   463 
   464 lemma eq_Pls_Bit1:
   465   "Numeral.Pls = Numeral.Bit k bit.B1 \<longleftrightarrow> False"
   466   unfolding Pls_def Bit_def bit.cases by arith
   467 
   468 lemma eq_Min_Pls:
   469   "Numeral.Min = Numeral.Pls \<longleftrightarrow> False"
   470   unfolding Pls_def Min_def by auto
   471 
   472 lemma eq_Min_Min:
   473   "Numeral.Min = Numeral.Min \<longleftrightarrow> True" by rule+
   474 
   475 lemma eq_Min_Bit0:
   476   "Numeral.Min = Numeral.Bit k bit.B0 \<longleftrightarrow> False"
   477   unfolding Min_def Bit_def bit.cases by arith
   478 
   479 lemma eq_Min_Bit1:
   480   "Numeral.Min = Numeral.Bit k bit.B1 \<longleftrightarrow> Numeral.Min = k"
   481   unfolding Min_def Bit_def bit.cases by auto
   482 
   483 lemma eq_Bit0_Pls:
   484   "Numeral.Bit k bit.B0 = Numeral.Pls \<longleftrightarrow> Numeral.Pls = k"
   485   unfolding Pls_def Bit_def bit.cases by auto
   486 
   487 lemma eq_Bit1_Pls:
   488   "Numeral.Bit k bit.B1 = Numeral.Pls \<longleftrightarrow> False"
   489   unfolding Pls_def Bit_def bit.cases by arith
   490 
   491 lemma eq_Bit0_Min:
   492   "Numeral.Bit k bit.B0 = Numeral.Min \<longleftrightarrow> False"
   493   unfolding Min_def Bit_def bit.cases by arith
   494 
   495 lemma eq_Bit1_Min:
   496   "(Numeral.Bit k bit.B1) = Numeral.Min \<longleftrightarrow> Numeral.Min = k"
   497   unfolding Min_def Bit_def bit.cases by auto
   498 
   499 lemma eq_Bit_Bit:
   500   "Numeral.Bit k1 v1 = Numeral.Bit k2 v2 \<longleftrightarrow>
   501     v1 = v2 \<and> k1 = k2"
   502   unfolding Bit_def
   503   apply (cases v1)
   504   apply (cases v2)
   505   apply auto
   506   apply arith
   507   apply (cases v2)
   508   apply auto
   509   apply arith
   510   apply (cases v2)
   511   apply auto
   512 done
   513 
   514 lemma eq_number_of:
   515   "(number_of k \<Colon> int) = number_of l \<longleftrightarrow> k = l"
   516   unfolding number_of_is_id ..
   517 
   518 
   519 lemma less_eq_Pls_Pls:
   520   "Numeral.Pls \<le> Numeral.Pls \<longleftrightarrow> True" by rule+
   521 
   522 lemma less_eq_Pls_Min:
   523   "Numeral.Pls \<le> Numeral.Min \<longleftrightarrow> False"
   524   unfolding Pls_def Min_def by auto
   525 
   526 lemma less_eq_Pls_Bit:
   527   "Numeral.Pls \<le> Numeral.Bit k v \<longleftrightarrow> Numeral.Pls \<le> k"
   528   unfolding Pls_def Bit_def by (cases v) auto
   529 
   530 lemma less_eq_Min_Pls:
   531   "Numeral.Min \<le> Numeral.Pls \<longleftrightarrow> True"
   532   unfolding Pls_def Min_def by auto
   533 
   534 lemma less_eq_Min_Min:
   535   "Numeral.Min \<le> Numeral.Min \<longleftrightarrow> True" by rule+
   536 
   537 lemma less_eq_Min_Bit0:
   538   "Numeral.Min \<le> Numeral.Bit k bit.B0 \<longleftrightarrow> Numeral.Min < k"
   539   unfolding Min_def Bit_def by auto
   540 
   541 lemma less_eq_Min_Bit1:
   542   "Numeral.Min \<le> Numeral.Bit k bit.B1 \<longleftrightarrow> Numeral.Min \<le> k"
   543   unfolding Min_def Bit_def by auto
   544 
   545 lemma less_eq_Bit0_Pls:
   546   "Numeral.Bit k bit.B0 \<le> Numeral.Pls \<longleftrightarrow> k \<le> Numeral.Pls"
   547   unfolding Pls_def Bit_def by simp
   548 
   549 lemma less_eq_Bit1_Pls:
   550   "Numeral.Bit k bit.B1 \<le> Numeral.Pls \<longleftrightarrow> k < Numeral.Pls"
   551   unfolding Pls_def Bit_def by auto
   552 
   553 lemma less_eq_Bit_Min:
   554   "Numeral.Bit k v \<le> Numeral.Min \<longleftrightarrow> k \<le> Numeral.Min"
   555   unfolding Min_def Bit_def by (cases v) auto
   556 
   557 lemma less_eq_Bit0_Bit:
   558   "Numeral.Bit k1 bit.B0 \<le> Numeral.Bit k2 v \<longleftrightarrow> k1 \<le> k2"
   559   unfolding Bit_def bit.cases by (cases v) auto
   560 
   561 lemma less_eq_Bit_Bit1:
   562   "Numeral.Bit k1 v \<le> Numeral.Bit k2 bit.B1 \<longleftrightarrow> k1 \<le> k2"
   563   unfolding Bit_def bit.cases by (cases v) auto
   564 
   565 lemma less_eq_Bit1_Bit0:
   566   "Numeral.Bit k1 bit.B1 \<le> Numeral.Bit k2 bit.B0 \<longleftrightarrow> k1 < k2"
   567   unfolding Bit_def by (auto split: bit.split)
   568 
   569 lemma less_eq_number_of:
   570   "(number_of k \<Colon> int) \<le> number_of l \<longleftrightarrow> k \<le> l"
   571   unfolding number_of_is_id ..
   572 
   573 
   574 lemma less_Pls_Pls:
   575   "Numeral.Pls < Numeral.Pls \<longleftrightarrow> False" by auto
   576 
   577 lemma less_Pls_Min:
   578   "Numeral.Pls < Numeral.Min \<longleftrightarrow> False"
   579   unfolding Pls_def Min_def by auto
   580 
   581 lemma less_Pls_Bit0:
   582   "Numeral.Pls < Numeral.Bit k bit.B0 \<longleftrightarrow> Numeral.Pls < k"
   583   unfolding Pls_def Bit_def by auto
   584 
   585 lemma less_Pls_Bit1:
   586   "Numeral.Pls < Numeral.Bit k bit.B1 \<longleftrightarrow> Numeral.Pls \<le> k"
   587   unfolding Pls_def Bit_def by auto
   588 
   589 lemma less_Min_Pls:
   590   "Numeral.Min < Numeral.Pls \<longleftrightarrow> True"
   591   unfolding Pls_def Min_def by auto
   592 
   593 lemma less_Min_Min:
   594   "Numeral.Min < Numeral.Min \<longleftrightarrow> False" by auto
   595 
   596 lemma less_Min_Bit:
   597   "Numeral.Min < Numeral.Bit k v \<longleftrightarrow> Numeral.Min < k"
   598   unfolding Min_def Bit_def by (auto split: bit.split)
   599 
   600 lemma less_Bit_Pls:
   601   "Numeral.Bit k v < Numeral.Pls \<longleftrightarrow> k < Numeral.Pls"
   602   unfolding Pls_def Bit_def by (auto split: bit.split)
   603 
   604 lemma less_Bit0_Min:
   605   "Numeral.Bit k bit.B0 < Numeral.Min \<longleftrightarrow> k \<le> Numeral.Min"
   606   unfolding Min_def Bit_def by auto
   607 
   608 lemma less_Bit1_Min:
   609   "Numeral.Bit k bit.B1 < Numeral.Min \<longleftrightarrow> k < Numeral.Min"
   610   unfolding Min_def Bit_def by auto
   611 
   612 lemma less_Bit_Bit0:
   613   "Numeral.Bit k1 v < Numeral.Bit k2 bit.B0 \<longleftrightarrow> k1 < k2"
   614   unfolding Bit_def by (auto split: bit.split)
   615 
   616 lemma less_Bit1_Bit:
   617   "Numeral.Bit k1 bit.B1 < Numeral.Bit k2 v \<longleftrightarrow> k1 < k2"
   618   unfolding Bit_def by (auto split: bit.split)
   619 
   620 lemma less_Bit0_Bit1:
   621   "Numeral.Bit k1 bit.B0 < Numeral.Bit k2 bit.B1 \<longleftrightarrow> k1 \<le> k2"
   622   unfolding Bit_def bit.cases by auto
   623 
   624 lemma less_number_of:
   625   "(number_of k \<Colon> int) < number_of l \<longleftrightarrow> k < l"
   626   unfolding number_of_is_id ..
   627 
   628 lemmas pred_succ_numeral_code [code func] =
   629   arith_simps(5-12)
   630 
   631 lemmas plus_numeral_code [code func] =
   632   arith_simps(13-17)
   633   arith_simps(26-27)
   634   arith_extra_simps(1) [where 'a = int]
   635 
   636 lemmas minus_numeral_code [code func] =
   637   arith_simps(18-21)
   638   arith_extra_simps(2) [where 'a = int]
   639   arith_extra_simps(5) [where 'a = int]
   640 
   641 lemmas times_numeral_code [code func] =
   642   arith_simps(22-25)
   643   arith_extra_simps(4) [where 'a = int]
   644 
   645 lemmas eq_numeral_code [code func] =
   646   eq_Pls_Pls eq_Pls_Min eq_Pls_Bit0 eq_Pls_Bit1
   647   eq_Min_Pls eq_Min_Min eq_Min_Bit0 eq_Min_Bit1
   648   eq_Bit0_Pls eq_Bit1_Pls eq_Bit0_Min eq_Bit1_Min eq_Bit_Bit
   649   eq_number_of
   650 
   651 lemmas less_eq_numeral_code [code func] = less_eq_Pls_Pls less_eq_Pls_Min less_eq_Pls_Bit
   652   less_eq_Min_Pls less_eq_Min_Min less_eq_Min_Bit0 less_eq_Min_Bit1
   653   less_eq_Bit0_Pls less_eq_Bit1_Pls less_eq_Bit_Min less_eq_Bit0_Bit less_eq_Bit_Bit1 less_eq_Bit1_Bit0
   654   less_eq_number_of
   655 
   656 lemmas less_numeral_code [code func] = less_Pls_Pls less_Pls_Min less_Pls_Bit0
   657   less_Pls_Bit1 less_Min_Pls less_Min_Min less_Min_Bit less_Bit_Pls
   658   less_Bit0_Min less_Bit1_Min less_Bit_Bit0 less_Bit1_Bit less_Bit0_Bit1
   659   less_number_of
   660 
   661 end