solved the problem that Larry's simproce cancle_numerals(?) returns
inconsistent inequality w/o rewriting it to False.
--- a/src/HOL/Nat.ML Sun Feb 24 21:47:33 2002 +0100
+++ b/src/HOL/Nat.ML Mon Feb 25 10:42:34 2002 +0100
@@ -258,6 +258,18 @@
delsimps [add_0_right]) 1);
qed "add_eq_self_zero";
+(* a rather special thm needed for arith_tac: m+n = 0 may arise where m or n
+contain Suc. This contradiction must be detected. It cannot be detected by
+pulling Suc outside because this interferes with simprocs on
+numerals. Sigh. *)
+
+Goal "m ~= 0 ==> m+n ~= (0::nat)";
+by(Asm_full_simp_tac 1);
+qed "add_not_0_if_left_not_0";
+
+Goal "n ~= 0 ==> m+n ~= (0::nat)";
+by(Asm_full_simp_tac 1);
+qed "add_not_0_if_right_not_0";
(**** Additional theorems about "less than" ****)
--- a/src/HOL/arith_data.ML Sun Feb 24 21:47:33 2002 +0100
+++ b/src/HOL/arith_data.ML Mon Feb 25 10:42:34 2002 +0100
@@ -366,7 +366,11 @@
(* reduce contradictory <= to False.
Most of the work is done by the cancel tactics.
*)
-val add_rules = [add_0,add_0_right,Zero_not_Suc,Suc_not_Zero,le_0_eq,One_nat_def];
+val add_rules =
+ [add_0,add_0_right,Zero_not_Suc,Suc_not_Zero,le_0_eq,
+ add_not_0_if_left_not_0,add_not_0_if_right_not_0,
+ add_not_0_if_left_not_0 RS not_sym,add_not_0_if_right_not_0 RS not_sym,
+ One_nat_def];
val add_mono_thms_nat = map (fn s => prove_goal (the_context ()) s
(fn prems => [cut_facts_tac prems 1,