# HG changeset patch
# User paulson
# Date 932563226 -7200
# Node ID 522a7013d7df1926edb472d16cda019824bd047a
# Parent  91764e88d93222e51674d04c7b727d9abd6c60e9
more existing theorems renamed to use #0; also new results

diff -r 91764e88d932 -r 522a7013d7df src/HOL/Integ/NatBin.ML
--- a/src/HOL/Integ/NatBin.ML	Wed Jul 21 15:18:36 1999 +0200
+++ b/src/HOL/Integ/NatBin.ML	Wed Jul 21 15:20:26 1999 +0200
@@ -292,17 +292,31 @@
   NOT suitable for rewriting because n recurs in the condition.*)
 bind_thm ("expand_Suc", inst "n" "number_of ?v" Suc_pred');
 
+(** NatDef & Nat **)
+
+Addsimps (map (rename_numerals thy) 
+	  [min_0L, min_0R, max_0L, max_0R]);
+
+AddIffs (map (rename_numerals thy) 
+	 [Suc_not_Zero, Zero_not_Suc, zero_less_Suc, not_less0, less_one, 
+	  le0, le_0_eq, 
+	  neq0_conv, zero_neq_conv, not_gr0]);
+
 (** Arith **)
 
 Addsimps (map (rename_numerals thy) 
 	  [diff_0_eq_0, add_0, add_0_right, add_pred, 
-	   diff_is_0_eq RS iffD2, zero_less_diff,
+	   diff_is_0_eq, zero_is_diff_eq, zero_less_diff,
 	   mult_0, mult_0_right, mult_1, mult_1_right, 
 	   mult_is_0, zero_less_mult_iff,
 	   mult_eq_1_iff]);
 
 AddIffs (map (rename_numerals thy) [add_is_0, zero_is_add, add_gr_0]);
 
+Goal "Suc n = n + #1";
+by (asm_simp_tac numeral_ss 1);
+qed "Suc_eq_add_numeral_1";
+
 (* These two can be useful when m = number_of... *)
 
 Goal "(m::nat) + n = (if m=#0 then n else Suc ((m - #1) + n))";
@@ -315,6 +329,17 @@
 by (ALLGOALS (asm_simp_tac numeral_ss));
 qed "mult_eq_if";
 
+Goal "(p ^ m :: nat) = (if m=#0 then #1 else p * (p ^ (m - #1)))";
+by (exhaust_tac "m" 1);
+by (ALLGOALS (asm_simp_tac numeral_ss));
+qed "power_eq_if";
+
+Goal "[| #0<n; #0<m |] ==> m - n < (m::nat)";
+by (asm_full_simp_tac (numeral_ss addsimps [diff_less]) 1);
+qed "diff_less'";
+
+Addsimps [inst "n" "number_of ?v" diff_less'];
+
 (*various theorems that aren't in the default simpset*)
 val add_is_one' = rename_numerals thy add_is_1;
 val one_is_add' = rename_numerals thy one_is_add;