src/HOL/Arith.ML
changeset 5078 7b5ea59c0275
parent 5069 3ea049f7979d
child 5143 b94cd208f073
     1.1 --- a/src/HOL/Arith.ML	Wed Jun 24 13:59:45 1998 +0200
     1.2 +++ b/src/HOL/Arith.ML	Thu Jun 25 13:57:34 1998 +0200
     1.3 @@ -118,19 +118,16 @@
     1.4  qed "add_pred";
     1.5  Addsimps [add_pred];
     1.6  
     1.7 +Goal "!!m::nat. m + n = m ==> n = 0";
     1.8 +by (dtac (add_0_right RS ssubst) 1);
     1.9 +by (asm_full_simp_tac (simpset() addsimps [add_assoc]
    1.10 +                                 delsimps [add_0_right]) 1);
    1.11 +qed "add_eq_self_zero";
    1.12 +
    1.13  
    1.14  (**** Additional theorems about "less than" ****)
    1.15  
    1.16 -Goal "i<j --> (EX k. j = Suc(i+k))";
    1.17 -by (induct_tac "j" 1);
    1.18 -by (Simp_tac 1);
    1.19 -by (blast_tac (claset() addSEs [less_SucE] 
    1.20 -                       addSIs [add_0_right RS sym, add_Suc_right RS sym]) 1);
    1.21 -val lemma = result();
    1.22 -
    1.23 -(* [| i<j;  !!x. j = Suc(i+x) ==> Q |] ==> Q *)
    1.24 -bind_thm ("less_natE", lemma RS mp RS exE);
    1.25 -
    1.26 +(*Deleted less_natE; instead use less_eq_Suc_add RS exE*)
    1.27  Goal "!!m. m<n --> (? k. n=Suc(m+k))";
    1.28  by (induct_tac "n" 1);
    1.29  by (ALLGOALS (simp_tac (simpset() addsimps [less_Suc_eq])));
    1.30 @@ -442,6 +439,12 @@
    1.31  by (ALLGOALS Asm_simp_tac);
    1.32  qed "less_imp_diff_positive";
    1.33  
    1.34 +Goal "!! (i::nat). i < j  ==> ? k. 0<k & i+k = j";
    1.35 +by (res_inst_tac [("x","j - i")] exI 1);
    1.36 +by (fast_tac (claset() addDs [less_trans, less_irrefl] 
    1.37 +   	               addIs [less_imp_diff_positive, add_diff_inverse]) 1);
    1.38 +qed "less_imp_add_positive";
    1.39 +
    1.40  Goal "Suc(m)-n = (if m<n then 0 else Suc(m-n))";
    1.41  by (simp_tac (simpset() addsimps [less_imp_diff_is_0, not_less_eq, Suc_diff_n]) 1);
    1.42  qed "if_Suc_diff_n";
    1.43 @@ -527,7 +530,7 @@
    1.44  
    1.45  (*strict, in 1st argument; proof is by induction on k>0*)
    1.46  Goal "!!i::nat. [| i<j; 0<k |] ==> k*i < k*j";
    1.47 -by (eres_inst_tac [("i","0")] less_natE 1);
    1.48 +by (eres_inst_tac [("m1","0")] (less_eq_Suc_add RS exE) 1);
    1.49  by (Asm_simp_tac 1);
    1.50  by (induct_tac "x" 1);
    1.51  by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_less_mono])));