src/HOL/Num.thy
changeset 47209 4893907fe872
parent 47207 9368aa814518
child 47211 e1b0c8236ae4
     1.1 --- a/src/HOL/Num.thy	Fri Mar 30 08:11:52 2012 +0200
     1.2 +++ b/src/HOL/Num.thy	Fri Mar 30 09:08:29 2012 +0200
     1.3 @@ -863,6 +863,12 @@
     1.4  lemma Suc_numeral [simp]: "Suc (numeral n) = numeral (n + One)"
     1.5    unfolding numeral_plus_one [symmetric] by simp
     1.6  
     1.7 +definition pred_numeral :: "num \<Rightarrow> nat"
     1.8 +  where [code del]: "pred_numeral k = numeral k - 1"
     1.9 +
    1.10 +lemma numeral_eq_Suc: "numeral k = Suc (pred_numeral k)"
    1.11 +  unfolding pred_numeral_def by simp
    1.12 +
    1.13  lemma nat_number:
    1.14    "1 = Suc 0"
    1.15    "numeral One = Suc 0"
    1.16 @@ -870,6 +876,13 @@
    1.17    "numeral (Bit1 n) = Suc (numeral (Bit0 n))"
    1.18    by (simp_all add: numeral.simps BitM_plus_one)
    1.19  
    1.20 +lemma pred_numeral_simps [simp]:
    1.21 +  "pred_numeral Num.One = 0"
    1.22 +  "pred_numeral (Num.Bit0 k) = numeral (Num.BitM k)"
    1.23 +  "pred_numeral (Num.Bit1 k) = numeral (Num.Bit0 k)"
    1.24 +  unfolding pred_numeral_def nat_number
    1.25 +  by (simp_all only: diff_Suc_Suc diff_0)
    1.26 +
    1.27  lemma numeral_2_eq_2: "2 = Suc (Suc 0)"
    1.28    by (simp add: nat_number(2-4))
    1.29  
    1.30 @@ -886,6 +899,42 @@
    1.31  (*Maps #n to n for n = 1, 2*)
    1.32  lemmas numerals = numeral_One [where 'a=nat] numeral_2_eq_2
    1.33  
    1.34 +text {* Comparisons involving @{term Suc}. *}
    1.35 +
    1.36 +lemma eq_numeral_Suc [simp]: "numeral k = Suc n \<longleftrightarrow> pred_numeral k = n"
    1.37 +  by (simp add: numeral_eq_Suc)
    1.38 +
    1.39 +lemma Suc_eq_numeral [simp]: "Suc n = numeral k \<longleftrightarrow> n = pred_numeral k"
    1.40 +  by (simp add: numeral_eq_Suc)
    1.41 +
    1.42 +lemma less_numeral_Suc [simp]: "numeral k < Suc n \<longleftrightarrow> pred_numeral k < n"
    1.43 +  by (simp add: numeral_eq_Suc)
    1.44 +
    1.45 +lemma less_Suc_numeral [simp]: "Suc n < numeral k \<longleftrightarrow> n < pred_numeral k"
    1.46 +  by (simp add: numeral_eq_Suc)
    1.47 +
    1.48 +lemma le_numeral_Suc [simp]: "numeral k \<le> Suc n \<longleftrightarrow> pred_numeral k \<le> n"
    1.49 +  by (simp add: numeral_eq_Suc)
    1.50 +
    1.51 +lemma le_Suc_numeral [simp]: "Suc n \<le> numeral k \<longleftrightarrow> n \<le> pred_numeral k"
    1.52 +  by (simp add: numeral_eq_Suc)
    1.53 +
    1.54 +lemma max_Suc_numeral [simp]:
    1.55 +  "max (Suc n) (numeral k) = Suc (max n (pred_numeral k))"
    1.56 +  by (simp add: numeral_eq_Suc)
    1.57 +
    1.58 +lemma max_numeral_Suc [simp]:
    1.59 +  "max (numeral k) (Suc n) = Suc (max (pred_numeral k) n)"
    1.60 +  by (simp add: numeral_eq_Suc)
    1.61 +
    1.62 +lemma min_Suc_numeral [simp]:
    1.63 +  "min (Suc n) (numeral k) = Suc (min n (pred_numeral k))"
    1.64 +  by (simp add: numeral_eq_Suc)
    1.65 +
    1.66 +lemma min_numeral_Suc [simp]:
    1.67 +  "min (numeral k) (Suc n) = Suc (min (pred_numeral k) n)"
    1.68 +  by (simp add: numeral_eq_Suc)
    1.69 +
    1.70  
    1.71  subsection {* Numeral equations as default simplification rules *}
    1.72