512 Int_Numeral_Simprocs.cancel_numerals; |
512 Int_Numeral_Simprocs.cancel_numerals; |
513 |
513 |
514 in |
514 in |
515 |
515 |
516 val int_arith_setup = |
516 val int_arith_setup = |
517 [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} => |
517 [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} => |
518 {add_mono_thms = add_mono_thms, |
518 {add_mono_thms = add_mono_thms, |
519 mult_mono_thms = [mult_strict_left_mono,mult_left_mono] @ mult_mono_thms, |
519 mult_mono_thms = [mult_strict_left_mono,mult_left_mono] @ mult_mono_thms, |
520 inj_thms = [zle_int RS iffD2,int_int_eq RS iffD2] @ inj_thms, |
520 inj_thms = [zle_int RS iffD2,int_int_eq RS iffD2] @ inj_thms, |
521 lessD = lessD @ [zless_imp_add1_zle], |
521 lessD = lessD @ [zless_imp_add1_zle], |
|
522 neqE = thm "linorder_neqE_int" :: neqE, |
522 simpset = simpset addsimps add_rules |
523 simpset = simpset addsimps add_rules |
523 addsimprocs simprocs |
524 addsimprocs simprocs |
524 addcongs [if_weak_cong]}), |
525 addcongs [if_weak_cong]}), |
525 arith_inj_const ("IntDef.of_nat", HOLogic.natT --> HOLogic.intT), |
526 arith_inj_const ("IntDef.of_nat", HOLogic.natT --> HOLogic.intT), |
526 arith_inj_const ("IntDef.int", HOLogic.natT --> HOLogic.intT), |
527 arith_inj_const ("IntDef.int", HOLogic.natT --> HOLogic.intT), |