Fixed the natxx_cancel_numerals simprocs so that they pull out Sucs and
authorpaulson
Tue Feb 26 13:37:48 2002 +0100 (2002-02-26)
changeset 12949b94843ffc0d1
parent 12948 2e22321e34ea
child 12950 3aadb133632d
Fixed the natxx_cancel_numerals simprocs so that they pull out Sucs and
return False for e.g. Suc x = 0. Removed ad-hoc lemmas for that purpose.
src/HOL/Integ/nat_simprocs.ML
src/HOL/Nat.ML
src/HOL/arith_data.ML
     1.1 --- a/src/HOL/Integ/nat_simprocs.ML	Tue Feb 26 12:51:40 2002 +0100
     1.2 +++ b/src/HOL/Integ/nat_simprocs.ML	Tue Feb 26 13:37:48 2002 +0100
     1.3 @@ -215,10 +215,16 @@
     1.4  val mult_1s = map rename_numerals [mult_1, mult_1_right];
     1.5  
     1.6  (*Final simplification: cancel + and *; replace Numeral0 by 0 and Numeral1 by 1*)
     1.7 +
     1.8 +(*And these help the simproc return False when appropriate, which helps
     1.9 +  the arith prover.*)
    1.10 +val contra_rules = [add_Suc, add_Suc_right, Zero_not_Suc, Suc_not_Zero, 
    1.11 +                    le_0_eq];
    1.12 +
    1.13  val simplify_meta_eq =
    1.14      Int_Numeral_Simprocs.simplify_meta_eq
    1.15 -         [numeral_0_eq_0, numeral_1_eq_Suc_0, add_0, add_0_right,
    1.16 -         mult_0, mult_0_right, mult_1, mult_1_right];
    1.17 +        ([numeral_0_eq_0, numeral_1_eq_Suc_0, add_0, add_0_right,
    1.18 +          mult_0, mult_0_right, mult_1, mult_1_right] @ contra_rules);
    1.19  
    1.20  
    1.21  (** Restricted version of dest_Sucs_sum for nat_combine_numerals:
     2.1 --- a/src/HOL/Nat.ML	Tue Feb 26 12:51:40 2002 +0100
     2.2 +++ b/src/HOL/Nat.ML	Tue Feb 26 13:37:48 2002 +0100
     2.3 @@ -258,19 +258,6 @@
     2.4                                   delsimps [add_0_right]) 1);
     2.5  qed "add_eq_self_zero";
     2.6  
     2.7 -(* a rather special thm needed for arith_tac: m+n = 0 may arise where m or n
     2.8 -contain Suc. This contradiction must be detected. It cannot be detected by
     2.9 -pulling Suc outside because this interferes with simprocs on
    2.10 -numerals. Sigh. *)
    2.11 -
    2.12 -Goal "m ~= 0 ==> m+n ~= (0::nat)";
    2.13 -by(Asm_full_simp_tac 1);
    2.14 -qed "add_not_0_if_left_not_0";
    2.15 -
    2.16 -Goal "n ~= 0 ==> m+n ~= (0::nat)";
    2.17 -by(Asm_full_simp_tac 1);
    2.18 -qed "add_not_0_if_right_not_0";
    2.19 -
    2.20  (**** Additional theorems about "less than" ****)
    2.21  
    2.22  (*Deleted less_natE; instead use less_imp_Suc_add RS exE*)
     3.1 --- a/src/HOL/arith_data.ML	Tue Feb 26 12:51:40 2002 +0100
     3.2 +++ b/src/HOL/arith_data.ML	Tue Feb 26 13:37:48 2002 +0100
     3.3 @@ -368,8 +368,6 @@
     3.4  *)
     3.5  val add_rules =
     3.6   [add_0,add_0_right,Zero_not_Suc,Suc_not_Zero,le_0_eq,
     3.7 -  add_not_0_if_left_not_0,add_not_0_if_right_not_0,
     3.8 -  add_not_0_if_left_not_0 RS not_sym,add_not_0_if_right_not_0 RS not_sym,
     3.9    One_nat_def];
    3.10  
    3.11  val add_mono_thms_nat = map (fn s => prove_goal (the_context ()) s