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