tuned code theorems for ord on integers
authorhaftmann
Fri Mar 02 15:43:25 2007 +0100 (2007-03-02)
changeset 2239454ea68b5a92f
parent 22393 9859d69101eb
child 22395 b573f1f566e1
tuned code theorems for ord on integers
src/HOL/Integ/Presburger.thy
src/HOL/Presburger.thy
src/HOL/ex/NormalForm.thy
     1.1 --- a/src/HOL/Integ/Presburger.thy	Fri Mar 02 15:43:24 2007 +0100
     1.2 +++ b/src/HOL/Integ/Presburger.thy	Fri Mar 02 15:43:25 2007 +0100
     1.3 @@ -1069,11 +1069,6 @@
     1.4  lemma eq_number_of [code func]:
     1.5    "((number_of k)\<Colon>int) = number_of l \<longleftrightarrow> k = l"
     1.6    unfolding number_of_is_id ..
     1.7 -
     1.8 -lemma less_eq_number_of [code func]:
     1.9 -  "((number_of k)\<Colon>int) <= number_of l \<longleftrightarrow> k <= l"
    1.10 -  unfolding number_of_is_id ..
    1.11 -
    1.12  lemma eq_Pls_Pls:
    1.13    "Numeral.Pls = Numeral.Pls" ..
    1.14  
    1.15 @@ -1140,6 +1135,10 @@
    1.16    eq_Min_Pls eq_Min_Min eq_Min_Bit0 eq_Min_Bit1
    1.17    eq_Bit0_Pls eq_Bit1_Pls eq_Bit0_Min eq_Bit1_Min eq_Bit_Bit
    1.18  
    1.19 +lemma less_eq_number_of [code func]:
    1.20 +  "(number_of k \<Colon> int) \<le> number_of l \<longleftrightarrow> k \<le> l"
    1.21 +  unfolding number_of_is_id ..
    1.22 +
    1.23  lemma less_eq_Pls_Pls:
    1.24    "Numeral.Pls \<le> Numeral.Pls" ..
    1.25  
    1.26 @@ -1180,14 +1179,76 @@
    1.27  
    1.28  lemma less_eq_Bit0_Bit:
    1.29    "Numeral.Bit k1 bit.B0 \<le> Numeral.Bit k2 v \<longleftrightarrow> k1 \<le> k2"
    1.30 -  unfolding Min_def Bit_def bit.cases by (cases v) auto
    1.31 +  unfolding Bit_def bit.cases by (cases v) auto
    1.32  
    1.33  lemma less_eq_Bit_Bit1:
    1.34    "Numeral.Bit k1 v \<le> Numeral.Bit k2 bit.B1 \<longleftrightarrow> k1 \<le> k2"
    1.35 -  unfolding Min_def Bit_def bit.cases by (cases v) auto
    1.36 +  unfolding Bit_def bit.cases by (cases v) auto
    1.37 +
    1.38 +lemma less_eq_Bit1_Bit0:
    1.39 +  "Numeral.Bit k1 bit.B1 \<le> Numeral.Bit k2 bit.B0 \<longleftrightarrow> k1 < k2"
    1.40 +  unfolding Bit_def by (auto split: bit.split)
    1.41  
    1.42  lemmas less_eq_numeral_code [code func] = less_eq_Pls_Pls less_eq_Pls_Min less_eq_Pls_Bit
    1.43    less_eq_Min_Pls less_eq_Min_Min less_eq_Min_Bit0 less_eq_Min_Bit1
    1.44 -  less_eq_Bit0_Pls less_eq_Bit1_Pls less_eq_Bit_Min less_eq_Bit0_Bit less_eq_Bit_Bit1
    1.45 +  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.46 +
    1.47 +lemma less_eq_number_of [code func]:
    1.48 +  "(number_of k \<Colon> int) < number_of l \<longleftrightarrow> k < l"
    1.49 +  unfolding number_of_is_id ..
    1.50 +
    1.51 +lemma less_Pls_Pls:
    1.52 +  "\<not> (Numeral.Pls < Numeral.Pls)" by auto
    1.53 +
    1.54 +lemma less_Pls_Min:
    1.55 +  "\<not> (Numeral.Pls < Numeral.Min)"
    1.56 +  unfolding Pls_def Min_def by auto
    1.57 +
    1.58 +lemma less_Pls_Bit0:
    1.59 +  "Numeral.Pls < Numeral.Bit k bit.B0 \<longleftrightarrow> Numeral.Pls < k"
    1.60 +  unfolding Pls_def Bit_def by auto
    1.61 +
    1.62 +lemma less_Pls_Bit1:
    1.63 +  "Numeral.Pls < Numeral.Bit k bit.B1 \<longleftrightarrow> Numeral.Pls \<le> k"
    1.64 +  unfolding Pls_def Bit_def by auto
    1.65 +
    1.66 +lemma less_Min_Pls:
    1.67 +  "Numeral.Min < Numeral.Pls"
    1.68 +  unfolding Pls_def Min_def by auto
    1.69 +
    1.70 +lemma less_Min_Min:
    1.71 +  "\<not> (Numeral.Min < Numeral.Min)" by auto
    1.72 +
    1.73 +lemma less_Min_Bit:
    1.74 +  "Numeral.Min < Numeral.Bit k v \<longleftrightarrow> Numeral.Min < k"
    1.75 +  unfolding Min_def Bit_def by (auto split: bit.split)
    1.76 +
    1.77 +lemma less_Bit_Pls:
    1.78 +  "Numeral.Bit k v < Numeral.Pls \<longleftrightarrow> k < Numeral.Pls"
    1.79 +  unfolding Pls_def Bit_def by (auto split: bit.split)
    1.80 +
    1.81 +lemma less_Bit0_Min:
    1.82 +  "Numeral.Bit k bit.B0 < Numeral.Min \<longleftrightarrow> k \<le> Numeral.Min"
    1.83 +  unfolding Min_def Bit_def by auto
    1.84 +
    1.85 +lemma less_Bit1_Min:
    1.86 +  "Numeral.Bit k bit.B1 < Numeral.Min \<longleftrightarrow> k < Numeral.Min"
    1.87 +  unfolding Min_def Bit_def by auto
    1.88 +
    1.89 +lemma less_Bit_Bit0:
    1.90 +  "Numeral.Bit k1 v < Numeral.Bit k2 bit.B0 \<longleftrightarrow> k1 < k2"
    1.91 +  unfolding Bit_def by (auto split: bit.split)
    1.92 +
    1.93 +lemma less_Bit1_Bit:
    1.94 +  "Numeral.Bit k1 bit.B1 < Numeral.Bit k2 v \<longleftrightarrow> k1 < k2"
    1.95 +  unfolding Bit_def by (auto split: bit.split)
    1.96 +
    1.97 +lemma less_Bit0_Bit1:
    1.98 +  "Numeral.Bit k1 bit.B0 < Numeral.Bit k2 bit.B1 \<longleftrightarrow> k1 \<le> k2"
    1.99 +  unfolding Bit_def bit.cases by auto
   1.100 +
   1.101 +lemmas less_numeral_code [code func] = less_Pls_Pls less_Pls_Min less_Pls_Bit0
   1.102 +  less_Pls_Bit1 less_Min_Pls less_Min_Min less_Min_Bit less_Bit_Pls
   1.103 +  less_Bit0_Min less_Bit1_Min less_Bit_Bit0 less_Bit1_Bit less_Bit0_Bit1
   1.104  
   1.105  end
     2.1 --- a/src/HOL/Presburger.thy	Fri Mar 02 15:43:24 2007 +0100
     2.2 +++ b/src/HOL/Presburger.thy	Fri Mar 02 15:43:25 2007 +0100
     2.3 @@ -1069,11 +1069,6 @@
     2.4  lemma eq_number_of [code func]:
     2.5    "((number_of k)\<Colon>int) = number_of l \<longleftrightarrow> k = l"
     2.6    unfolding number_of_is_id ..
     2.7 -
     2.8 -lemma less_eq_number_of [code func]:
     2.9 -  "((number_of k)\<Colon>int) <= number_of l \<longleftrightarrow> k <= l"
    2.10 -  unfolding number_of_is_id ..
    2.11 -
    2.12  lemma eq_Pls_Pls:
    2.13    "Numeral.Pls = Numeral.Pls" ..
    2.14  
    2.15 @@ -1140,6 +1135,10 @@
    2.16    eq_Min_Pls eq_Min_Min eq_Min_Bit0 eq_Min_Bit1
    2.17    eq_Bit0_Pls eq_Bit1_Pls eq_Bit0_Min eq_Bit1_Min eq_Bit_Bit
    2.18  
    2.19 +lemma less_eq_number_of [code func]:
    2.20 +  "(number_of k \<Colon> int) \<le> number_of l \<longleftrightarrow> k \<le> l"
    2.21 +  unfolding number_of_is_id ..
    2.22 +
    2.23  lemma less_eq_Pls_Pls:
    2.24    "Numeral.Pls \<le> Numeral.Pls" ..
    2.25  
    2.26 @@ -1180,14 +1179,76 @@
    2.27  
    2.28  lemma less_eq_Bit0_Bit:
    2.29    "Numeral.Bit k1 bit.B0 \<le> Numeral.Bit k2 v \<longleftrightarrow> k1 \<le> k2"
    2.30 -  unfolding Min_def Bit_def bit.cases by (cases v) auto
    2.31 +  unfolding Bit_def bit.cases by (cases v) auto
    2.32  
    2.33  lemma less_eq_Bit_Bit1:
    2.34    "Numeral.Bit k1 v \<le> Numeral.Bit k2 bit.B1 \<longleftrightarrow> k1 \<le> k2"
    2.35 -  unfolding Min_def Bit_def bit.cases by (cases v) auto
    2.36 +  unfolding Bit_def bit.cases by (cases v) auto
    2.37 +
    2.38 +lemma less_eq_Bit1_Bit0:
    2.39 +  "Numeral.Bit k1 bit.B1 \<le> Numeral.Bit k2 bit.B0 \<longleftrightarrow> k1 < k2"
    2.40 +  unfolding Bit_def by (auto split: bit.split)
    2.41  
    2.42  lemmas less_eq_numeral_code [code func] = less_eq_Pls_Pls less_eq_Pls_Min less_eq_Pls_Bit
    2.43    less_eq_Min_Pls less_eq_Min_Min less_eq_Min_Bit0 less_eq_Min_Bit1
    2.44 -  less_eq_Bit0_Pls less_eq_Bit1_Pls less_eq_Bit_Min less_eq_Bit0_Bit less_eq_Bit_Bit1
    2.45 +  less_eq_Bit0_Pls less_eq_Bit1_Pls less_eq_Bit_Min less_eq_Bit0_Bit less_eq_Bit_Bit1 less_eq_Bit1_Bit0
    2.46 +
    2.47 +lemma less_eq_number_of [code func]:
    2.48 +  "(number_of k \<Colon> int) < number_of l \<longleftrightarrow> k < l"
    2.49 +  unfolding number_of_is_id ..
    2.50 +
    2.51 +lemma less_Pls_Pls:
    2.52 +  "\<not> (Numeral.Pls < Numeral.Pls)" by auto
    2.53 +
    2.54 +lemma less_Pls_Min:
    2.55 +  "\<not> (Numeral.Pls < Numeral.Min)"
    2.56 +  unfolding Pls_def Min_def by auto
    2.57 +
    2.58 +lemma less_Pls_Bit0:
    2.59 +  "Numeral.Pls < Numeral.Bit k bit.B0 \<longleftrightarrow> Numeral.Pls < k"
    2.60 +  unfolding Pls_def Bit_def by auto
    2.61 +
    2.62 +lemma less_Pls_Bit1:
    2.63 +  "Numeral.Pls < Numeral.Bit k bit.B1 \<longleftrightarrow> Numeral.Pls \<le> k"
    2.64 +  unfolding Pls_def Bit_def by auto
    2.65 +
    2.66 +lemma less_Min_Pls:
    2.67 +  "Numeral.Min < Numeral.Pls"
    2.68 +  unfolding Pls_def Min_def by auto
    2.69 +
    2.70 +lemma less_Min_Min:
    2.71 +  "\<not> (Numeral.Min < Numeral.Min)" by auto
    2.72 +
    2.73 +lemma less_Min_Bit:
    2.74 +  "Numeral.Min < Numeral.Bit k v \<longleftrightarrow> Numeral.Min < k"
    2.75 +  unfolding Min_def Bit_def by (auto split: bit.split)
    2.76 +
    2.77 +lemma less_Bit_Pls:
    2.78 +  "Numeral.Bit k v < Numeral.Pls \<longleftrightarrow> k < Numeral.Pls"
    2.79 +  unfolding Pls_def Bit_def by (auto split: bit.split)
    2.80 +
    2.81 +lemma less_Bit0_Min:
    2.82 +  "Numeral.Bit k bit.B0 < Numeral.Min \<longleftrightarrow> k \<le> Numeral.Min"
    2.83 +  unfolding Min_def Bit_def by auto
    2.84 +
    2.85 +lemma less_Bit1_Min:
    2.86 +  "Numeral.Bit k bit.B1 < Numeral.Min \<longleftrightarrow> k < Numeral.Min"
    2.87 +  unfolding Min_def Bit_def by auto
    2.88 +
    2.89 +lemma less_Bit_Bit0:
    2.90 +  "Numeral.Bit k1 v < Numeral.Bit k2 bit.B0 \<longleftrightarrow> k1 < k2"
    2.91 +  unfolding Bit_def by (auto split: bit.split)
    2.92 +
    2.93 +lemma less_Bit1_Bit:
    2.94 +  "Numeral.Bit k1 bit.B1 < Numeral.Bit k2 v \<longleftrightarrow> k1 < k2"
    2.95 +  unfolding Bit_def by (auto split: bit.split)
    2.96 +
    2.97 +lemma less_Bit0_Bit1:
    2.98 +  "Numeral.Bit k1 bit.B0 < Numeral.Bit k2 bit.B1 \<longleftrightarrow> k1 \<le> k2"
    2.99 +  unfolding Bit_def bit.cases by auto
   2.100 +
   2.101 +lemmas less_numeral_code [code func] = less_Pls_Pls less_Pls_Min less_Pls_Bit0
   2.102 +  less_Pls_Bit1 less_Min_Pls less_Min_Min less_Min_Bit less_Bit_Pls
   2.103 +  less_Bit0_Min less_Bit1_Min less_Bit_Bit0 less_Bit1_Bit less_Bit0_Bit1
   2.104  
   2.105  end
     3.1 --- a/src/HOL/ex/NormalForm.thy	Fri Mar 02 15:43:24 2007 +0100
     3.2 +++ b/src/HOL/ex/NormalForm.thy	Fri Mar 02 15:43:25 2007 +0100
     3.3 @@ -104,11 +104,9 @@
     3.4  lemma "(2::int) <= 3" by normalization
     3.5  lemma "abs ((-4::int) + 2 * 1) = 2" by normalization
     3.6  lemma "4 - 42 * abs (3 + (-7\<Colon>int)) = -164" by normalization
     3.7 -normal_form "min 0 x"
     3.8 -normal_form "min 0 (x::nat)"
     3.9  lemma "(if (0\<Colon>nat) \<le> (x\<Colon>nat) then 0\<Colon>nat else x) = 0" by normalization
    3.10 -
    3.11 -normal_form "nat 4 = Suc (Suc (Suc (Suc 0)))"
    3.12 +lemma "4 = Suc (Suc (Suc (Suc 0)))" by normalization
    3.13 +lemma "nat 4 = Suc (Suc (Suc (Suc 0)))" by normalization
    3.14  
    3.15  normal_form "Suc 0 \<in> set ms"
    3.16