# HG changeset patch
# User huffman
# Date 1333091309 -7200
# Node ID 4893907fe872a076bc32581e40a89a54f411e802
# Parent  9a91b163bb719d2aa654d6a53d7fe0fb0168784f
add constant pred_numeral k = numeral k - (1::nat);
replace several simp rules from Nat_Numeral.thy with new ones that use pred_numeral

diff -r 9a91b163bb71 -r 4893907fe872 src/HOL/Nat_Numeral.thy
--- a/src/HOL/Nat_Numeral.thy	Fri Mar 30 08:11:52 2012 +0200
+++ b/src/HOL/Nat_Numeral.thy	Fri Mar 30 09:08:29 2012 +0200
@@ -42,45 +42,6 @@
 lemma power_eq_if: "(p ^ m :: nat) = (if m=0 then 1 else p * (p ^ (m - 1)))"
   unfolding One_nat_def by (cases m) simp_all
 
-
-subsection{*Comparisons involving  @{term Suc} *}
-
-lemma eq_numeral_Suc [simp]: "numeral v = Suc n \<longleftrightarrow> nat (numeral v - 1) = n"
-  by (subst expand_Suc, simp only: nat.inject nat_numeral_diff_1)
-
-lemma Suc_eq_numeral [simp]: "Suc n = numeral v \<longleftrightarrow> n = nat (numeral v - 1)"
-  by (subst expand_Suc, simp only: nat.inject nat_numeral_diff_1)
-
-lemma less_numeral_Suc [simp]: "numeral v < Suc n \<longleftrightarrow> nat (numeral v - 1) < n"
-  by (subst expand_Suc, simp only: Suc_less_eq nat_numeral_diff_1)
-
-lemma less_Suc_numeral [simp]: "Suc n < numeral v \<longleftrightarrow> n < nat (numeral v - 1)"
-  by (subst expand_Suc, simp only: Suc_less_eq nat_numeral_diff_1)
-
-lemma le_numeral_Suc [simp]: "numeral v \<le> Suc n \<longleftrightarrow> nat (numeral v - 1) \<le> n"
-  by (subst expand_Suc, simp only: Suc_le_mono nat_numeral_diff_1)
-
-lemma le_Suc_numeral [simp]: "Suc n \<le> numeral v \<longleftrightarrow> n \<le> nat (numeral v - 1)"
-  by (subst expand_Suc, simp only: Suc_le_mono nat_numeral_diff_1)
-
-
-subsection{*Max and Min Combined with @{term Suc} *}
-
-lemma max_Suc_numeral [simp]:
-  "max (Suc n) (numeral v) = Suc (max n (nat (numeral v - 1)))"
-  by (subst expand_Suc, simp only: max_Suc_Suc nat_numeral_diff_1)
-
-lemma max_numeral_Suc [simp]:
-  "max (numeral v) (Suc n) = Suc (max (nat (numeral v - 1)) n)"
-  by (subst expand_Suc, simp only: max_Suc_Suc nat_numeral_diff_1)
-
-lemma min_Suc_numeral [simp]:
-  "min (Suc n) (numeral v) = Suc (min n (nat (numeral v - 1)))"
-  by (subst expand_Suc, simp only: min_Suc_Suc nat_numeral_diff_1)
-
-lemma min_numeral_Suc [simp]:
-  "min (numeral v) (Suc n) = Suc (min (nat (numeral v - 1)) n)"
-  by (subst expand_Suc, simp only: min_Suc_Suc nat_numeral_diff_1)
  
 subsection{*Literal arithmetic involving powers*}
 
diff -r 9a91b163bb71 -r 4893907fe872 src/HOL/Num.thy
--- a/src/HOL/Num.thy	Fri Mar 30 08:11:52 2012 +0200
+++ b/src/HOL/Num.thy	Fri Mar 30 09:08:29 2012 +0200
@@ -863,6 +863,12 @@
 lemma Suc_numeral [simp]: "Suc (numeral n) = numeral (n + One)"
   unfolding numeral_plus_one [symmetric] by simp
 
+definition pred_numeral :: "num \<Rightarrow> nat"
+  where [code del]: "pred_numeral k = numeral k - 1"
+
+lemma numeral_eq_Suc: "numeral k = Suc (pred_numeral k)"
+  unfolding pred_numeral_def by simp
+
 lemma nat_number:
   "1 = Suc 0"
   "numeral One = Suc 0"
@@ -870,6 +876,13 @@
   "numeral (Bit1 n) = Suc (numeral (Bit0 n))"
   by (simp_all add: numeral.simps BitM_plus_one)
 
+lemma pred_numeral_simps [simp]:
+  "pred_numeral Num.One = 0"
+  "pred_numeral (Num.Bit0 k) = numeral (Num.BitM k)"
+  "pred_numeral (Num.Bit1 k) = numeral (Num.Bit0 k)"
+  unfolding pred_numeral_def nat_number
+  by (simp_all only: diff_Suc_Suc diff_0)
+
 lemma numeral_2_eq_2: "2 = Suc (Suc 0)"
   by (simp add: nat_number(2-4))
 
@@ -886,6 +899,42 @@
 (*Maps #n to n for n = 1, 2*)
 lemmas numerals = numeral_One [where 'a=nat] numeral_2_eq_2
 
+text {* Comparisons involving @{term Suc}. *}
+
+lemma eq_numeral_Suc [simp]: "numeral k = Suc n \<longleftrightarrow> pred_numeral k = n"
+  by (simp add: numeral_eq_Suc)
+
+lemma Suc_eq_numeral [simp]: "Suc n = numeral k \<longleftrightarrow> n = pred_numeral k"
+  by (simp add: numeral_eq_Suc)
+
+lemma less_numeral_Suc [simp]: "numeral k < Suc n \<longleftrightarrow> pred_numeral k < n"
+  by (simp add: numeral_eq_Suc)
+
+lemma less_Suc_numeral [simp]: "Suc n < numeral k \<longleftrightarrow> n < pred_numeral k"
+  by (simp add: numeral_eq_Suc)
+
+lemma le_numeral_Suc [simp]: "numeral k \<le> Suc n \<longleftrightarrow> pred_numeral k \<le> n"
+  by (simp add: numeral_eq_Suc)
+
+lemma le_Suc_numeral [simp]: "Suc n \<le> numeral k \<longleftrightarrow> n \<le> pred_numeral k"
+  by (simp add: numeral_eq_Suc)
+
+lemma max_Suc_numeral [simp]:
+  "max (Suc n) (numeral k) = Suc (max n (pred_numeral k))"
+  by (simp add: numeral_eq_Suc)
+
+lemma max_numeral_Suc [simp]:
+  "max (numeral k) (Suc n) = Suc (max (pred_numeral k) n)"
+  by (simp add: numeral_eq_Suc)
+
+lemma min_Suc_numeral [simp]:
+  "min (Suc n) (numeral k) = Suc (min n (pred_numeral k))"
+  by (simp add: numeral_eq_Suc)
+
+lemma min_numeral_Suc [simp]:
+  "min (numeral k) (Suc n) = Suc (min (pred_numeral k) n)"
+  by (simp add: numeral_eq_Suc)
+
 
 subsection {* Numeral equations as default simplification rules *}
 
diff -r 9a91b163bb71 -r 4893907fe872 src/HOL/Power.thy
--- a/src/HOL/Power.thy	Fri Mar 30 08:11:52 2012 +0200
+++ b/src/HOL/Power.thy	Fri Mar 30 09:08:29 2012 +0200
@@ -115,7 +115,7 @@
   by (induct n) (simp_all add: of_nat_mult)
 
 lemma power_zero_numeral [simp]: "(0::'a) ^ numeral k = 0"
-  by (cases "numeral k :: nat", simp_all)
+  by (simp add: numeral_eq_Suc)
 
 lemma zero_power2: "0\<twosuperior> = 0" (* delete? *)
   by (rule power_zero_numeral)
diff -r 9a91b163bb71 -r 4893907fe872 src/HOL/Tools/int_arith.ML
--- a/src/HOL/Tools/int_arith.ML	Fri Mar 30 08:11:52 2012 +0200
+++ b/src/HOL/Tools/int_arith.ML	Fri Mar 30 09:08:29 2012 +0200
@@ -86,6 +86,7 @@
   Lin_Arith.add_inj_thms [@{thm zle_int} RS iffD2, @{thm int_int_eq} RS iffD2]
   #> Lin_Arith.add_lessD @{thm zless_imp_add1_zle}
   #> Lin_Arith.add_simps (@{thms simp_thms} @ @{thms arith_simps} @ @{thms rel_simps}
+      @ @{thms pred_numeral_simps}
       @ @{thms arith_special} @ @{thms int_arith_rules})
   #> Lin_Arith.add_simprocs [zero_one_idom_simproc]
   #> Lin_Arith.set_number_of number_of