src/HOL/Presburger.thy
changeset 20595 db6bedfba498
parent 20485 3078fd2eec7b
child 21046 fe1db2f991a7
     1.1 --- a/src/HOL/Presburger.thy	Tue Sep 19 15:21:55 2006 +0200
     1.2 +++ b/src/HOL/Presburger.thy	Tue Sep 19 15:21:58 2006 +0200
     1.3 @@ -1086,4 +1086,137 @@
     1.4  
     1.5  setup "Presburger.setup"
     1.6  
     1.7 +text {* Code generator setup *}
     1.8 +
     1.9 +text {*
    1.10 +  Presburger arithmetic is neccesary to prove some
    1.11 +  of the following code lemmas on integer numerals.
    1.12 +*}
    1.13 +
    1.14 +lemma eq_number_of [code func]:
    1.15 +  "OperationalEquality.eq ((number_of k)\<Colon>int) (number_of l) \<longleftrightarrow> OperationalEquality.eq k l"
    1.16 +  unfolding number_of_is_id ..
    1.17 +
    1.18 +lemma less_eq_number_of [code func]:
    1.19 +  "((number_of k)\<Colon>int) <= number_of l \<longleftrightarrow> k <= l"
    1.20 +  unfolding number_of_is_id ..
    1.21 +
    1.22 +lemma eq_Pls_Pls:
    1.23 +  "OperationalEquality.eq Numeral.Pls Numeral.Pls"
    1.24 +  unfolding eq_def ..
    1.25 +
    1.26 +lemma eq_Pls_Min:
    1.27 +  "\<not> OperationalEquality.eq Numeral.Pls Numeral.Min"
    1.28 +  unfolding eq_def Pls_def Min_def by auto
    1.29 +
    1.30 +lemma eq_Pls_Bit0:
    1.31 +  "OperationalEquality.eq Numeral.Pls (Numeral.Bit k bit.B0) \<longleftrightarrow> OperationalEquality.eq Numeral.Pls k"
    1.32 +  unfolding eq_def Pls_def Bit_def bit.cases by auto
    1.33 +
    1.34 +lemma eq_Pls_Bit1:
    1.35 +  "\<not> OperationalEquality.eq Numeral.Pls (Numeral.Bit k bit.B1)"
    1.36 +  unfolding eq_def Pls_def Bit_def bit.cases by arith
    1.37 +
    1.38 +lemma eq_Min_Pls:
    1.39 +  "\<not> OperationalEquality.eq Numeral.Min Numeral.Pls"
    1.40 +  unfolding eq_def Pls_def Min_def by auto
    1.41 +
    1.42 +lemma eq_Min_Min:
    1.43 +  "OperationalEquality.eq Numeral.Min Numeral.Min"
    1.44 +  unfolding eq_def ..
    1.45 +
    1.46 +lemma eq_Min_Bit0:
    1.47 +  "\<not> OperationalEquality.eq Numeral.Min (Numeral.Bit k bit.B0)"
    1.48 +  unfolding eq_def Min_def Bit_def bit.cases by arith
    1.49 +
    1.50 +lemma eq_Min_Bit1:
    1.51 +  "OperationalEquality.eq Numeral.Min (Numeral.Bit k bit.B1) \<longleftrightarrow> OperationalEquality.eq Numeral.Min k"
    1.52 +  unfolding eq_def Min_def Bit_def bit.cases by auto
    1.53 +
    1.54 +lemma eq_Bit0_Pls:
    1.55 +  "OperationalEquality.eq (Numeral.Bit k bit.B0) Numeral.Pls \<longleftrightarrow> OperationalEquality.eq Numeral.Pls k"
    1.56 +  unfolding eq_def Pls_def Bit_def bit.cases by auto
    1.57 +
    1.58 +lemma eq_Bit1_Pls:
    1.59 +  "\<not> OperationalEquality.eq (Numeral.Bit k bit.B1) Numeral.Pls"
    1.60 +  unfolding eq_def Pls_def Bit_def bit.cases by arith
    1.61 +
    1.62 +lemma eq_Bit0_Min:
    1.63 +  "\<not> OperationalEquality.eq (Numeral.Bit k bit.B0) Numeral.Min"
    1.64 +  unfolding eq_def Min_def Bit_def bit.cases by arith
    1.65 +
    1.66 +lemma eq_Bit1_Min:
    1.67 +  "OperationalEquality.eq (Numeral.Bit k bit.B1) Numeral.Min \<longleftrightarrow> OperationalEquality.eq Numeral.Min k"
    1.68 +  unfolding eq_def Min_def Bit_def bit.cases by auto
    1.69 +
    1.70 +lemma eq_Bit_Bit:
    1.71 +  "OperationalEquality.eq (Numeral.Bit k1 v1) (Numeral.Bit k2 v2) \<longleftrightarrow>
    1.72 +    OperationalEquality.eq v1 v2 \<and> OperationalEquality.eq k1 k2"
    1.73 +  unfolding eq_def Bit_def
    1.74 +  apply (cases v1)
    1.75 +  apply (cases v2)
    1.76 +  apply auto
    1.77 +  apply arith
    1.78 +  apply (cases v2)
    1.79 +  apply auto
    1.80 +  apply arith
    1.81 +  apply (cases v2)
    1.82 +  apply auto
    1.83 +done
    1.84 +
    1.85 +lemmas eq_numeral_code [code func] =
    1.86 +  eq_Pls_Pls eq_Pls_Min eq_Pls_Bit0 eq_Pls_Bit1
    1.87 +  eq_Min_Pls eq_Min_Min eq_Min_Bit0 eq_Min_Bit1
    1.88 +  eq_Bit0_Pls eq_Bit1_Pls eq_Bit0_Min eq_Bit1_Min eq_Bit_Bit
    1.89 +
    1.90 +lemma less_eq_Pls_Pls:
    1.91 +  "Numeral.Pls \<le> Numeral.Pls" ..
    1.92 +
    1.93 +lemma less_eq_Pls_Min:
    1.94 +  "\<not> (Numeral.Pls \<le> Numeral.Min)"
    1.95 +  unfolding Pls_def Min_def by auto
    1.96 +
    1.97 +lemma less_eq_Pls_Bit:
    1.98 +  "Numeral.Pls \<le> Numeral.Bit k v \<longleftrightarrow> Numeral.Pls \<le> k"
    1.99 +  unfolding Pls_def Bit_def by (cases v) auto
   1.100 +
   1.101 +lemma less_eq_Min_Pls:
   1.102 +  "Numeral.Min \<le> Numeral.Pls"
   1.103 +  unfolding Pls_def Min_def by auto
   1.104 +
   1.105 +lemma less_eq_Min_Min:
   1.106 +  "Numeral.Min \<le> Numeral.Min" ..
   1.107 +
   1.108 +lemma less_eq_Min_Bit0:
   1.109 +  "Numeral.Min \<le> Numeral.Bit k bit.B0 \<longleftrightarrow> Numeral.Min < k"
   1.110 +  unfolding Min_def Bit_def by auto
   1.111 +
   1.112 +lemma less_eq_Min_Bit1:
   1.113 +  "Numeral.Min \<le> Numeral.Bit k bit.B1 \<longleftrightarrow> Numeral.Min \<le> k"
   1.114 +  unfolding Min_def Bit_def by auto
   1.115 +
   1.116 +lemma less_eq_Bit0_Pls:
   1.117 +  "Numeral.Bit k bit.B0 \<le> Numeral.Pls \<longleftrightarrow> k \<le> Numeral.Pls"
   1.118 +  unfolding Pls_def Bit_def by simp
   1.119 +
   1.120 +lemma less_eq_Bit1_Pls:
   1.121 +  "Numeral.Bit k bit.B1 \<le> Numeral.Pls \<longleftrightarrow> k < Numeral.Pls"
   1.122 +  unfolding Pls_def Bit_def by auto
   1.123 +
   1.124 +lemma less_eq_Bit_Min:
   1.125 +  "Numeral.Bit k v \<le> Numeral.Min \<longleftrightarrow> k \<le> Numeral.Min"
   1.126 +  unfolding Min_def Bit_def by (cases v) auto
   1.127 +
   1.128 +lemma less_eq_Bit0_Bit:
   1.129 +  "Numeral.Bit k1 bit.B0 \<le> Numeral.Bit k2 v \<longleftrightarrow> k1 \<le> k2"
   1.130 +  unfolding Min_def Bit_def bit.cases by (cases v) auto
   1.131 +
   1.132 +lemma less_eq_Bit_Bit1:
   1.133 +  "Numeral.Bit k1 v \<le> Numeral.Bit k2 bit.B1 \<longleftrightarrow> k1 \<le> k2"
   1.134 +  unfolding Min_def Bit_def bit.cases by (cases v) auto
   1.135 +
   1.136 +lemmas less_eq_numeral_code [code func] = less_eq_Pls_Pls less_eq_Pls_Min less_eq_Pls_Bit
   1.137 +  less_eq_Min_Pls less_eq_Min_Min less_eq_Min_Bit0 less_eq_Min_Bit1
   1.138 +  less_eq_Bit0_Pls less_eq_Bit1_Pls less_eq_Bit_Min less_eq_Bit0_Bit less_eq_Bit_Bit1
   1.139 +
   1.140  end