# HG changeset patch # User paulson # Date 957458457 -7200 # Node ID 4a3612f30865071d47465f56c845230c7e96c188 # Parent 3b10d24b5eddfa13404ddae42310788577c98f88 if_weak_cong should make linear arithmetic faster diff -r 3b10d24b5edd -r 4a3612f30865 src/HOL/Integ/IntArith.ML --- a/src/HOL/Integ/IntArith.ML Thu May 04 18:39:51 2000 +0200 +++ b/src/HOL/Integ/IntArith.ML Thu May 04 18:40:57 2000 +0200 @@ -415,7 +415,8 @@ LA_Data_Ref.add_mono_thms := !LA_Data_Ref.add_mono_thms @ add_mono_thms; LA_Data_Ref.lessD := !LA_Data_Ref.lessD @ [add1_zle_eq RS iffD2]; LA_Data_Ref.ss_ref := !LA_Data_Ref.ss_ref addsimps add_rules - addsimprocs simprocs; + addsimprocs simprocs + addcongs [if_weak_cong]; LA_Data_Ref.discrete := !LA_Data_Ref.discrete @ [("IntDef.int",true)] end; @@ -546,6 +547,10 @@ by Auto_tac; qed "nat_eq_iff"; +Goal "#0 <= w ==> (m = nat w) = (w = int m)"; +by Auto_tac; +qed "nat_eq_iff2"; + Goal "#0 <= w ==> (nat w < m) = (w < int m)"; by (rtac iffI 1); by (asm_full_simp_tac