Expandshort; new theorem le_square
authorpaulson
Wed Nov 05 13:29:47 1997 +0100 (1997-11-05)
changeset 415847c7490c74fe
parent 4157 200f897f0858
child 4159 4aff9b7e5597
Expandshort; new theorem le_square
src/HOL/Arith.ML
     1.1 --- a/src/HOL/Arith.ML	Wed Nov 05 13:27:58 1997 +0100
     1.2 +++ b/src/HOL/Arith.ML	Wed Nov 05 13:29:47 1997 +0100
     1.3 @@ -35,12 +35,12 @@
     1.4  AddIffs [pred_le];
     1.5  
     1.6  goalw Arith.thy [pred_def] "m<=n --> pred(m) <= pred(n)";
     1.7 -by(simp_tac (simpset() addsplits [expand_nat_case]) 1);
     1.8 +by (simp_tac (simpset() addsplits [expand_nat_case]) 1);
     1.9  qed_spec_mp "pred_le_mono";
    1.10  
    1.11  goal Arith.thy "!!n. n ~= 0 ==> pred n < n";
    1.12 -by(exhaust_tac "n" 1);
    1.13 -by(ALLGOALS Asm_full_simp_tac);
    1.14 +by (exhaust_tac "n" 1);
    1.15 +by (ALLGOALS Asm_full_simp_tac);
    1.16  qed "pred_less";
    1.17  Addsimps [pred_less];
    1.18  
    1.19 @@ -327,6 +327,12 @@
    1.20  qed "mult_is_0";
    1.21  Addsimps [mult_is_0];
    1.22  
    1.23 +goal Arith.thy "!!m::nat. m <= m*m";
    1.24 +by (induct_tac "m" 1);
    1.25 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_assoc RS sym])));
    1.26 +by (etac (le_add2 RSN (2,le_trans)) 1);
    1.27 +qed "le_square";
    1.28 +
    1.29  
    1.30  (*** Difference ***)
    1.31