add constant pred_numeral k = numeral k - (1::nat);
authorhuffman
Fri Mar 30 09:08:29 2012 +0200 (2012-03-30)
changeset 472094893907fe872
parent 47208 9a91b163bb71
child 47210 b1dd32b2a505
add constant pred_numeral k = numeral k - (1::nat);
replace several simp rules from Nat_Numeral.thy with new ones that use pred_numeral
src/HOL/Nat_Numeral.thy
src/HOL/Num.thy
src/HOL/Power.thy
src/HOL/Tools/int_arith.ML
     1.1 --- a/src/HOL/Nat_Numeral.thy	Fri Mar 30 08:11:52 2012 +0200
     1.2 +++ b/src/HOL/Nat_Numeral.thy	Fri Mar 30 09:08:29 2012 +0200
     1.3 @@ -42,45 +42,6 @@
     1.4  lemma power_eq_if: "(p ^ m :: nat) = (if m=0 then 1 else p * (p ^ (m - 1)))"
     1.5    unfolding One_nat_def by (cases m) simp_all
     1.6  
     1.7 -
     1.8 -subsection{*Comparisons involving  @{term Suc} *}
     1.9 -
    1.10 -lemma eq_numeral_Suc [simp]: "numeral v = Suc n \<longleftrightarrow> nat (numeral v - 1) = n"
    1.11 -  by (subst expand_Suc, simp only: nat.inject nat_numeral_diff_1)
    1.12 -
    1.13 -lemma Suc_eq_numeral [simp]: "Suc n = numeral v \<longleftrightarrow> n = nat (numeral v - 1)"
    1.14 -  by (subst expand_Suc, simp only: nat.inject nat_numeral_diff_1)
    1.15 -
    1.16 -lemma less_numeral_Suc [simp]: "numeral v < Suc n \<longleftrightarrow> nat (numeral v - 1) < n"
    1.17 -  by (subst expand_Suc, simp only: Suc_less_eq nat_numeral_diff_1)
    1.18 -
    1.19 -lemma less_Suc_numeral [simp]: "Suc n < numeral v \<longleftrightarrow> n < nat (numeral v - 1)"
    1.20 -  by (subst expand_Suc, simp only: Suc_less_eq nat_numeral_diff_1)
    1.21 -
    1.22 -lemma le_numeral_Suc [simp]: "numeral v \<le> Suc n \<longleftrightarrow> nat (numeral v - 1) \<le> n"
    1.23 -  by (subst expand_Suc, simp only: Suc_le_mono nat_numeral_diff_1)
    1.24 -
    1.25 -lemma le_Suc_numeral [simp]: "Suc n \<le> numeral v \<longleftrightarrow> n \<le> nat (numeral v - 1)"
    1.26 -  by (subst expand_Suc, simp only: Suc_le_mono nat_numeral_diff_1)
    1.27 -
    1.28 -
    1.29 -subsection{*Max and Min Combined with @{term Suc} *}
    1.30 -
    1.31 -lemma max_Suc_numeral [simp]:
    1.32 -  "max (Suc n) (numeral v) = Suc (max n (nat (numeral v - 1)))"
    1.33 -  by (subst expand_Suc, simp only: max_Suc_Suc nat_numeral_diff_1)
    1.34 -
    1.35 -lemma max_numeral_Suc [simp]:
    1.36 -  "max (numeral v) (Suc n) = Suc (max (nat (numeral v - 1)) n)"
    1.37 -  by (subst expand_Suc, simp only: max_Suc_Suc nat_numeral_diff_1)
    1.38 -
    1.39 -lemma min_Suc_numeral [simp]:
    1.40 -  "min (Suc n) (numeral v) = Suc (min n (nat (numeral v - 1)))"
    1.41 -  by (subst expand_Suc, simp only: min_Suc_Suc nat_numeral_diff_1)
    1.42 -
    1.43 -lemma min_numeral_Suc [simp]:
    1.44 -  "min (numeral v) (Suc n) = Suc (min (nat (numeral v - 1)) n)"
    1.45 -  by (subst expand_Suc, simp only: min_Suc_Suc nat_numeral_diff_1)
    1.46   
    1.47  subsection{*Literal arithmetic involving powers*}
    1.48  
     2.1 --- a/src/HOL/Num.thy	Fri Mar 30 08:11:52 2012 +0200
     2.2 +++ b/src/HOL/Num.thy	Fri Mar 30 09:08:29 2012 +0200
     2.3 @@ -863,6 +863,12 @@
     2.4  lemma Suc_numeral [simp]: "Suc (numeral n) = numeral (n + One)"
     2.5    unfolding numeral_plus_one [symmetric] by simp
     2.6  
     2.7 +definition pred_numeral :: "num \<Rightarrow> nat"
     2.8 +  where [code del]: "pred_numeral k = numeral k - 1"
     2.9 +
    2.10 +lemma numeral_eq_Suc: "numeral k = Suc (pred_numeral k)"
    2.11 +  unfolding pred_numeral_def by simp
    2.12 +
    2.13  lemma nat_number:
    2.14    "1 = Suc 0"
    2.15    "numeral One = Suc 0"
    2.16 @@ -870,6 +876,13 @@
    2.17    "numeral (Bit1 n) = Suc (numeral (Bit0 n))"
    2.18    by (simp_all add: numeral.simps BitM_plus_one)
    2.19  
    2.20 +lemma pred_numeral_simps [simp]:
    2.21 +  "pred_numeral Num.One = 0"
    2.22 +  "pred_numeral (Num.Bit0 k) = numeral (Num.BitM k)"
    2.23 +  "pred_numeral (Num.Bit1 k) = numeral (Num.Bit0 k)"
    2.24 +  unfolding pred_numeral_def nat_number
    2.25 +  by (simp_all only: diff_Suc_Suc diff_0)
    2.26 +
    2.27  lemma numeral_2_eq_2: "2 = Suc (Suc 0)"
    2.28    by (simp add: nat_number(2-4))
    2.29  
    2.30 @@ -886,6 +899,42 @@
    2.31  (*Maps #n to n for n = 1, 2*)
    2.32  lemmas numerals = numeral_One [where 'a=nat] numeral_2_eq_2
    2.33  
    2.34 +text {* Comparisons involving @{term Suc}. *}
    2.35 +
    2.36 +lemma eq_numeral_Suc [simp]: "numeral k = Suc n \<longleftrightarrow> pred_numeral k = n"
    2.37 +  by (simp add: numeral_eq_Suc)
    2.38 +
    2.39 +lemma Suc_eq_numeral [simp]: "Suc n = numeral k \<longleftrightarrow> n = pred_numeral k"
    2.40 +  by (simp add: numeral_eq_Suc)
    2.41 +
    2.42 +lemma less_numeral_Suc [simp]: "numeral k < Suc n \<longleftrightarrow> pred_numeral k < n"
    2.43 +  by (simp add: numeral_eq_Suc)
    2.44 +
    2.45 +lemma less_Suc_numeral [simp]: "Suc n < numeral k \<longleftrightarrow> n < pred_numeral k"
    2.46 +  by (simp add: numeral_eq_Suc)
    2.47 +
    2.48 +lemma le_numeral_Suc [simp]: "numeral k \<le> Suc n \<longleftrightarrow> pred_numeral k \<le> n"
    2.49 +  by (simp add: numeral_eq_Suc)
    2.50 +
    2.51 +lemma le_Suc_numeral [simp]: "Suc n \<le> numeral k \<longleftrightarrow> n \<le> pred_numeral k"
    2.52 +  by (simp add: numeral_eq_Suc)
    2.53 +
    2.54 +lemma max_Suc_numeral [simp]:
    2.55 +  "max (Suc n) (numeral k) = Suc (max n (pred_numeral k))"
    2.56 +  by (simp add: numeral_eq_Suc)
    2.57 +
    2.58 +lemma max_numeral_Suc [simp]:
    2.59 +  "max (numeral k) (Suc n) = Suc (max (pred_numeral k) n)"
    2.60 +  by (simp add: numeral_eq_Suc)
    2.61 +
    2.62 +lemma min_Suc_numeral [simp]:
    2.63 +  "min (Suc n) (numeral k) = Suc (min n (pred_numeral k))"
    2.64 +  by (simp add: numeral_eq_Suc)
    2.65 +
    2.66 +lemma min_numeral_Suc [simp]:
    2.67 +  "min (numeral k) (Suc n) = Suc (min (pred_numeral k) n)"
    2.68 +  by (simp add: numeral_eq_Suc)
    2.69 +
    2.70  
    2.71  subsection {* Numeral equations as default simplification rules *}
    2.72  
     3.1 --- a/src/HOL/Power.thy	Fri Mar 30 08:11:52 2012 +0200
     3.2 +++ b/src/HOL/Power.thy	Fri Mar 30 09:08:29 2012 +0200
     3.3 @@ -115,7 +115,7 @@
     3.4    by (induct n) (simp_all add: of_nat_mult)
     3.5  
     3.6  lemma power_zero_numeral [simp]: "(0::'a) ^ numeral k = 0"
     3.7 -  by (cases "numeral k :: nat", simp_all)
     3.8 +  by (simp add: numeral_eq_Suc)
     3.9  
    3.10  lemma zero_power2: "0\<twosuperior> = 0" (* delete? *)
    3.11    by (rule power_zero_numeral)
     4.1 --- a/src/HOL/Tools/int_arith.ML	Fri Mar 30 08:11:52 2012 +0200
     4.2 +++ b/src/HOL/Tools/int_arith.ML	Fri Mar 30 09:08:29 2012 +0200
     4.3 @@ -86,6 +86,7 @@
     4.4    Lin_Arith.add_inj_thms [@{thm zle_int} RS iffD2, @{thm int_int_eq} RS iffD2]
     4.5    #> Lin_Arith.add_lessD @{thm zless_imp_add1_zle}
     4.6    #> Lin_Arith.add_simps (@{thms simp_thms} @ @{thms arith_simps} @ @{thms rel_simps}
     4.7 +      @ @{thms pred_numeral_simps}
     4.8        @ @{thms arith_special} @ @{thms int_arith_rules})
     4.9    #> Lin_Arith.add_simprocs [zero_one_idom_simproc]
    4.10    #> Lin_Arith.set_number_of number_of