solved the problem that Larry's simproce cancle_numerals(?) returns
authornipkow
Mon Feb 25 10:42:34 2002 +0100 (2002-02-25)
changeset 129312c0251fada94
parent 12930 c1f3ff5feff1
child 12932 3bda5306d262
solved the problem that Larry's simproce cancle_numerals(?) returns
inconsistent inequality w/o rewriting it to False.
src/HOL/Nat.ML
src/HOL/arith_data.ML
     1.1 --- a/src/HOL/Nat.ML	Sun Feb 24 21:47:33 2002 +0100
     1.2 +++ b/src/HOL/Nat.ML	Mon Feb 25 10:42:34 2002 +0100
     1.3 @@ -258,6 +258,18 @@
     1.4                                   delsimps [add_0_right]) 1);
     1.5  qed "add_eq_self_zero";
     1.6  
     1.7 +(* a rather special thm needed for arith_tac: m+n = 0 may arise where m or n
     1.8 +contain Suc. This contradiction must be detected. It cannot be detected by
     1.9 +pulling Suc outside because this interferes with simprocs on
    1.10 +numerals. Sigh. *)
    1.11 +
    1.12 +Goal "m ~= 0 ==> m+n ~= (0::nat)";
    1.13 +by(Asm_full_simp_tac 1);
    1.14 +qed "add_not_0_if_left_not_0";
    1.15 +
    1.16 +Goal "n ~= 0 ==> m+n ~= (0::nat)";
    1.17 +by(Asm_full_simp_tac 1);
    1.18 +qed "add_not_0_if_right_not_0";
    1.19  
    1.20  (**** Additional theorems about "less than" ****)
    1.21  
     2.1 --- a/src/HOL/arith_data.ML	Sun Feb 24 21:47:33 2002 +0100
     2.2 +++ b/src/HOL/arith_data.ML	Mon Feb 25 10:42:34 2002 +0100
     2.3 @@ -366,7 +366,11 @@
     2.4  (* reduce contradictory <= to False.
     2.5     Most of the work is done by the cancel tactics.
     2.6  *)
     2.7 -val add_rules = [add_0,add_0_right,Zero_not_Suc,Suc_not_Zero,le_0_eq,One_nat_def];
     2.8 +val add_rules =
     2.9 + [add_0,add_0_right,Zero_not_Suc,Suc_not_Zero,le_0_eq,
    2.10 +  add_not_0_if_left_not_0,add_not_0_if_right_not_0,
    2.11 +  add_not_0_if_left_not_0 RS not_sym,add_not_0_if_right_not_0 RS not_sym,
    2.12 +  One_nat_def];
    2.13  
    2.14  val add_mono_thms_nat = map (fn s => prove_goal (the_context ()) s
    2.15   (fn prems => [cut_facts_tac prems 1,