src/HOL/Decision_Procs/mir_tac.ML
changeset 30240 5b25fee0362c
parent 29948 cdf12a1cb963
child 30242 aea5d7fa7ef5
     1.1 --- a/src/HOL/Decision_Procs/mir_tac.ML	Wed Mar 04 10:43:39 2009 +0100
     1.2 +++ b/src/HOL/Decision_Procs/mir_tac.ML	Wed Mar 04 10:45:52 2009 +0100
     1.3 @@ -46,12 +46,9 @@
     1.4  val Suc_plus1 = @{thm "Suc_plus1"};
     1.5  val imp_le_cong = @{thm "imp_le_cong"};
     1.6  val conj_le_cong = @{thm "conj_le_cong"};
     1.7 -val nat_mod_add_eq = @{thm "mod_add1_eq"} RS sym;
     1.8 -val nat_mod_add_left_eq = @{thm "mod_add_left_eq"} RS sym;
     1.9 -val nat_mod_add_right_eq = @{thm "mod_add_right_eq"} RS sym;
    1.10 -val int_mod_add_eq = @{thm "mod_add_eq"} RS sym;
    1.11 -val int_mod_add_left_eq = @{thm "zmod_zadd_left_eq"} RS sym;
    1.12 -val int_mod_add_right_eq = @{thm "zmod_zadd_right_eq"} RS sym;
    1.13 +val mod_add_eq = @{thm "mod_add_eq"} RS sym;
    1.14 +val mod_add_left_eq = @{thm "mod_add_left_eq"} RS sym;
    1.15 +val mod_add_right_eq = @{thm "mod_add_right_eq"} RS sym;
    1.16  val nat_div_add_eq = @{thm "div_add1_eq"} RS sym;
    1.17  val int_div_add_eq = @{thm "zdiv_zadd1_eq"} RS sym;
    1.18  val ZDIVISION_BY_ZERO_MOD = @{thm "DIVISION_BY_ZERO"} RS conjunct2;
    1.19 @@ -96,10 +93,10 @@
    1.20      val (t,np,nh) = prepare_for_mir thy q g
    1.21      (* Some simpsets for dealing with mod div abs and nat*)
    1.22      val mod_div_simpset = HOL_basic_ss 
    1.23 -                        addsimps [refl,nat_mod_add_eq, 
    1.24 +                        addsimps [refl, mod_add_eq, 
    1.25                                    @{thm "mod_self"}, @{thm "zmod_self"},
    1.26                                    @{thm "zdiv_zero"},@{thm "zmod_zero"},@{thm "div_0"}, @{thm "mod_0"},
    1.27 -                                  @{thm "zdiv_1"}, @{thm "zmod_1"}, @{thm "div_1"}, @{thm "mod_1"},
    1.28 +                                  @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, @{thm "mod_1"},
    1.29                                    @{thm "Suc_plus1"}]
    1.30                          addsimps @{thms add_ac}
    1.31                          addsimprocs [cancel_div_mod_proc]