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