# HG changeset patch # User nipkow # Date 1014630154 -3600 # Node ID 2c0251fada947f77b2cabe2ff894fb96f5a704fd # Parent c1f3ff5feff174e941d1a4eafb7f855fde67ba30 solved the problem that Larry's simproce cancle_numerals(?) returns inconsistent inequality w/o rewriting it to False. diff -r c1f3ff5feff1 -r 2c0251fada94 src/HOL/Nat.ML --- 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" ****) diff -r c1f3ff5feff1 -r 2c0251fada94 src/HOL/arith_data.ML --- 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,