src/HOL/Presburger.thy
changeset 22801 caffcb450ef4
parent 22744 5cbe966d67a2
child 23146 0bc590051d95
     1.1 --- a/src/HOL/Presburger.thy	Thu Apr 26 13:33:04 2007 +0200
     1.2 +++ b/src/HOL/Presburger.thy	Thu Apr 26 13:33:05 2007 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4  header {* Presburger Arithmetic: Cooper's Algorithm *}
     1.5  
     1.6  theory Presburger
     1.7 -imports NatSimprocs
     1.8 +imports NatSimprocs "../SetInterval"
     1.9  uses
    1.10    ("cooper_dec.ML") ("cooper_proof.ML") ("qelim.ML") 
    1.11    ("reflected_presburger.ML") ("reflected_cooper.ML") ("presburger.ML")
    1.12 @@ -1059,17 +1059,14 @@
    1.13  
    1.14  setup "Presburger.setup"
    1.15  
    1.16 -text {* Code generator setup *}
    1.17 +
    1.18 +subsection {* Code generator setup *}
    1.19  
    1.20  text {*
    1.21 -  Presburger arithmetic is necessary (at least convenient) to prove some
    1.22 -  of the following code lemmas on integer numerals.
    1.23 +  Presburger arithmetic is convenient to prove some
    1.24 +  of the following code lemmas on integer numerals:
    1.25  *}
    1.26  
    1.27 -lemma eq_number_of [code func]:
    1.28 -  "((number_of k)\<Colon>int) = number_of l \<longleftrightarrow> k = l"
    1.29 -  unfolding number_of_is_id ..
    1.30 -
    1.31  lemma eq_Pls_Pls:
    1.32    "Numeral.Pls = Numeral.Pls \<longleftrightarrow> True" by rule+
    1.33  
    1.34 @@ -1131,14 +1128,10 @@
    1.35    apply auto
    1.36  done
    1.37  
    1.38 -lemmas eq_numeral_code [code func] =
    1.39 -  eq_Pls_Pls eq_Pls_Min eq_Pls_Bit0 eq_Pls_Bit1
    1.40 -  eq_Min_Pls eq_Min_Min eq_Min_Bit0 eq_Min_Bit1
    1.41 -  eq_Bit0_Pls eq_Bit1_Pls eq_Bit0_Min eq_Bit1_Min eq_Bit_Bit
    1.42 +lemma eq_number_of:
    1.43 +  "(number_of k \<Colon> int) = number_of l \<longleftrightarrow> k = l"
    1.44 +  unfolding number_of_is_id ..
    1.45  
    1.46 -lemma less_eq_number_of [code func]:
    1.47 -  "(number_of k \<Colon> int) \<le> number_of l \<longleftrightarrow> k \<le> l"
    1.48 -  unfolding number_of_is_id ..
    1.49  
    1.50  lemma less_eq_Pls_Pls:
    1.51    "Numeral.Pls \<le> Numeral.Pls \<longleftrightarrow> True" by rule+
    1.52 @@ -1190,13 +1183,10 @@
    1.53    "Numeral.Bit k1 bit.B1 \<le> Numeral.Bit k2 bit.B0 \<longleftrightarrow> k1 < k2"
    1.54    unfolding Bit_def by (auto split: bit.split)
    1.55  
    1.56 -lemmas less_eq_numeral_code [code func] = less_eq_Pls_Pls less_eq_Pls_Min less_eq_Pls_Bit
    1.57 -  less_eq_Min_Pls less_eq_Min_Min less_eq_Min_Bit0 less_eq_Min_Bit1
    1.58 -  less_eq_Bit0_Pls less_eq_Bit1_Pls less_eq_Bit_Min less_eq_Bit0_Bit less_eq_Bit_Bit1 less_eq_Bit1_Bit0
    1.59 +lemma less_eq_number_of:
    1.60 +  "(number_of k \<Colon> int) \<le> number_of l \<longleftrightarrow> k \<le> l"
    1.61 +  unfolding number_of_is_id ..
    1.62  
    1.63 -lemma less_eq_number_of [code func]:
    1.64 -  "(number_of k \<Colon> int) < number_of l \<longleftrightarrow> k < l"
    1.65 -  unfolding number_of_is_id ..
    1.66  
    1.67  lemma less_Pls_Pls:
    1.68    "Numeral.Pls < Numeral.Pls \<longleftrightarrow> False" by auto
    1.69 @@ -1248,8 +1238,42 @@
    1.70    "Numeral.Bit k1 bit.B0 < Numeral.Bit k2 bit.B1 \<longleftrightarrow> k1 \<le> k2"
    1.71    unfolding Bit_def bit.cases by auto
    1.72  
    1.73 +lemma less_number_of:
    1.74 +  "(number_of k \<Colon> int) < number_of l \<longleftrightarrow> k < l"
    1.75 +  unfolding number_of_is_id ..
    1.76 +
    1.77 +
    1.78 +lemmas pred_succ_numeral_code [code func] =
    1.79 +  arith_simps(5-12)
    1.80 +
    1.81 +lemmas plus_numeral_code [code func] =
    1.82 +  arith_simps(13-17)
    1.83 +  arith_simps(26-27)
    1.84 +  arith_extra_simps(1) [where 'a = int]
    1.85 +
    1.86 +lemmas minus_numeral_code [code func] =
    1.87 +  arith_simps(18-21)
    1.88 +  arith_extra_simps(2) [where 'a = int]
    1.89 +  arith_extra_simps(5) [where 'a = int]
    1.90 +
    1.91 +lemmas times_numeral_code [code func] =
    1.92 +  arith_simps(22-25)
    1.93 +  arith_extra_simps(4) [where 'a = int]
    1.94 +
    1.95 +lemmas eq_numeral_code [code func] =
    1.96 +  eq_Pls_Pls eq_Pls_Min eq_Pls_Bit0 eq_Pls_Bit1
    1.97 +  eq_Min_Pls eq_Min_Min eq_Min_Bit0 eq_Min_Bit1
    1.98 +  eq_Bit0_Pls eq_Bit1_Pls eq_Bit0_Min eq_Bit1_Min eq_Bit_Bit
    1.99 +  eq_number_of
   1.100 +
   1.101 +lemmas less_eq_numeral_code [code func] = less_eq_Pls_Pls less_eq_Pls_Min less_eq_Pls_Bit
   1.102 +  less_eq_Min_Pls less_eq_Min_Min less_eq_Min_Bit0 less_eq_Min_Bit1
   1.103 +  less_eq_Bit0_Pls less_eq_Bit1_Pls less_eq_Bit_Min less_eq_Bit0_Bit less_eq_Bit_Bit1 less_eq_Bit1_Bit0
   1.104 +  less_eq_number_of
   1.105 +
   1.106  lemmas less_numeral_code [code func] = less_Pls_Pls less_Pls_Min less_Pls_Bit0
   1.107    less_Pls_Bit1 less_Min_Pls less_Min_Min less_Min_Bit less_Bit_Pls
   1.108    less_Bit0_Min less_Bit1_Min less_Bit_Bit0 less_Bit1_Bit less_Bit0_Bit1
   1.109 +  less_number_of
   1.110  
   1.111  end