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