# HG changeset patch # User paulson # Date 878732987 -3600 # Node ID 47c7490c74feffcf5670469b69681cbd8e01386d # Parent 200f897f08581b3350ed8123392fd0f6657a81c3 Expandshort; new theorem le_square diff -r 200f897f0858 -r 47c7490c74fe src/HOL/Arith.ML --- a/src/HOL/Arith.ML Wed Nov 05 13:27:58 1997 +0100 +++ b/src/HOL/Arith.ML Wed Nov 05 13:29:47 1997 +0100 @@ -35,12 +35,12 @@ AddIffs [pred_le]; goalw Arith.thy [pred_def] "m<=n --> pred(m) <= pred(n)"; -by(simp_tac (simpset() addsplits [expand_nat_case]) 1); +by (simp_tac (simpset() addsplits [expand_nat_case]) 1); qed_spec_mp "pred_le_mono"; goal Arith.thy "!!n. n ~= 0 ==> pred n < n"; -by(exhaust_tac "n" 1); -by(ALLGOALS Asm_full_simp_tac); +by (exhaust_tac "n" 1); +by (ALLGOALS Asm_full_simp_tac); qed "pred_less"; Addsimps [pred_less]; @@ -327,6 +327,12 @@ qed "mult_is_0"; Addsimps [mult_is_0]; +goal Arith.thy "!!m::nat. m <= m*m"; +by (induct_tac "m" 1); +by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_assoc RS sym]))); +by (etac (le_add2 RSN (2,le_trans)) 1); +qed "le_square"; + (*** Difference ***)