if_weak_cong should make linear arithmetic faster
authorpaulson
Thu May 04 18:40:57 2000 +0200 (2000-05-04)
changeset 87964a3612f30865
parent 8795 3b10d24b5edd
child 8797 b55e2354d71e
if_weak_cong should make linear arithmetic faster
src/HOL/Integ/IntArith.ML
     1.1 --- a/src/HOL/Integ/IntArith.ML	Thu May 04 18:39:51 2000 +0200
     1.2 +++ b/src/HOL/Integ/IntArith.ML	Thu May 04 18:40:57 2000 +0200
     1.3 @@ -415,7 +415,8 @@
     1.4  LA_Data_Ref.add_mono_thms := !LA_Data_Ref.add_mono_thms @ add_mono_thms;
     1.5  LA_Data_Ref.lessD := !LA_Data_Ref.lessD @ [add1_zle_eq RS iffD2];
     1.6  LA_Data_Ref.ss_ref := !LA_Data_Ref.ss_ref addsimps add_rules
     1.7 -                      addsimprocs simprocs;
     1.8 +                      addsimprocs simprocs
     1.9 +                      addcongs [if_weak_cong];
    1.10  LA_Data_Ref.discrete := !LA_Data_Ref.discrete @ [("IntDef.int",true)]
    1.11  end;
    1.12  
    1.13 @@ -546,6 +547,10 @@
    1.14  by Auto_tac;
    1.15  qed "nat_eq_iff";
    1.16  
    1.17 +Goal "#0 <= w ==> (m = nat w) = (w = int m)";
    1.18 +by Auto_tac;
    1.19 +qed "nat_eq_iff2";
    1.20 +
    1.21  Goal "#0 <= w ==> (nat w < m) = (w < int m)";
    1.22  by (rtac iffI 1);
    1.23  by (asm_full_simp_tac