Remoaved a few now redundant rewrite rules.
authornipkow
Sat Jan 09 17:55:54 1999 +0100 (1999-01-09)
changeset 6075c148037f53c6
parent 6074 34242451bc91
child 6076 560396301672
Remoaved a few now redundant rewrite rules.
src/HOL/Arith.ML
src/HOL/NatDef.ML
     1.1 --- a/src/HOL/Arith.ML	Sat Jan 09 15:25:44 1999 +0100
     1.2 +++ b/src/HOL/Arith.ML	Sat Jan 09 17:55:54 1999 +0100
     1.3 @@ -124,12 +124,12 @@
     1.4  by (exhaust_tac "m" 1);
     1.5  by (ALLGOALS (fast_tac (claset() addss (simpset()))));
     1.6  qed "pred_add_is_0";
     1.7 -Addsimps [pred_add_is_0];
     1.8 +(*Addsimps [pred_add_is_0];*)
     1.9  
    1.10  (* Could be generalized, eg to "k<n ==> m+(n-(Suc k)) = (m+n)-(Suc k)" *)
    1.11  Goal "0<n ==> m + (n-1) = (m+n)-1";
    1.12  by (exhaust_tac "m" 1);
    1.13 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_Suc]
    1.14 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_Suc, Suc_n_not_n]
    1.15                                        addsplits [nat.split])));
    1.16  qed "add_pred";
    1.17  Addsimps [add_pred];
    1.18 @@ -365,7 +365,7 @@
    1.19  
    1.20  Goal "m - n <= (m::nat)";
    1.21  by (res_inst_tac [("m","m"), ("n","n")] diff_induct 1);
    1.22 -by (ALLGOALS Asm_simp_tac);
    1.23 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [le_SucI])));
    1.24  qed "diff_le_self";
    1.25  Addsimps [diff_le_self];
    1.26  
    1.27 @@ -929,8 +929,7 @@
    1.28  fun prep_pat s = Thm.read_cterm (sign_of Arith.thy) (s, HOLogic.boolT);
    1.29  
    1.30  val pats = map prep_pat
    1.31 -  ["(m::nat) < n","(m::nat) <= n", "~ (m::nat) < n","~ (m::nat) <= n",
    1.32 -   "(m::nat) = n"]
    1.33 +  ["(m::nat) < n","(m::nat) <= n", "(m::nat) = n"]
    1.34  
    1.35  in
    1.36  val fast_nat_arith_simproc =
     2.1 --- a/src/HOL/NatDef.ML	Sat Jan 09 15:25:44 1999 +0100
     2.2 +++ b/src/HOL/NatDef.ML	Sat Jan 09 17:55:54 1999 +0100
     2.3 @@ -283,7 +283,7 @@
     2.4  Goal "~(Suc(n) < n)";
     2.5  by (blast_tac (claset() addEs [Suc_lessD RS less_irrefl]) 1);
     2.6  qed "not_Suc_n_less_n";
     2.7 -Addsimps [not_Suc_n_less_n];
     2.8 +(*Addsimps [not_Suc_n_less_n];*)
     2.9  
    2.10  Goal "i<j ==> j<k --> Suc i < k";
    2.11  by (nat_ind_tac "k" 1);
    2.12 @@ -318,6 +318,7 @@
    2.13  Goalw [le_def] "0 <= n";
    2.14  by (rtac not_less0 1);
    2.15  qed "le0";
    2.16 +AddIffs [le0];
    2.17  
    2.18  Goalw [le_def] "~ Suc n <= n";
    2.19  by (Simp_tac 1);
    2.20 @@ -329,10 +330,6 @@
    2.21  qed "le_0_eq";
    2.22  AddIffs [le_0_eq];
    2.23  
    2.24 -Addsimps [(*less_Suc_eq, makes simpset non-confluent*) le0, le_0_eq,
    2.25 -          Suc_n_not_le_n,
    2.26 -          n_not_Suc_n, Suc_n_not_n];
    2.27 -
    2.28  Goal "(m <= Suc(n)) = (m<=n | m = Suc n)";
    2.29  by (simp_tac (simpset() delsimps [less_Suc_eq_le]
    2.30  			addsimps [less_Suc_eq_le RS sym, less_Suc_eq]) 1);