src/HOL/Arith.ML
 changeset 3484 1e93eb09ebb9 parent 3457 a8ab7c64817c child 3718 d78cf498a88c
```     1.1 --- a/src/HOL/Arith.ML	Tue Jul 01 17:59:36 1997 +0200
1.2 +++ b/src/HOL/Arith.ML	Wed Jul 02 11:59:10 1997 +0200
1.3 @@ -7,8 +7,6 @@
1.4  Some from the Hoare example from Norbert Galm
1.5  *)
1.6
1.7 -open Arith;
1.8 -
1.9  (*** Basic rewrite rules for the arithmetic operators ***)
1.10
1.11  goalw Arith.thy [pred_def] "pred 0 = 0";
1.12 @@ -30,6 +28,16 @@
1.13  qed "Suc_pred";
1.15
1.16 +goal Arith.thy "pred(n) <= (n::nat)";
1.17 +by (res_inst_tac [("n","n")] natE 1);
1.18 +by (ALLGOALS Asm_simp_tac);
1.19 +qed "pred_le";
1.21 +
1.22 +goalw Arith.thy [pred_def] "m<=n --> pred(m) <= pred(n)";
1.23 +by(simp_tac (!simpset setloop (split_tac[expand_nat_case])) 1);
1.24 +qed_spec_mp "pred_le_mono";
1.25 +
1.26  (** Difference **)
1.27
1.28  qed_goalw "diff_0_eq_0" Arith.thy [pred_def]
1.29 @@ -605,3 +613,28 @@
1.31
1.32
1.33 +(** (Anti)Monotonicity of subtraction -- by Stefan Merz **)
1.34 +
1.35 +(* Monotonicity of subtraction in first argument *)
1.36 +goal Arith.thy "!!n::nat. m<=n --> (m-l) <= (n-l)";
1.37 +by (induct_tac "n" 1);
1.38 +by (Simp_tac 1);
1.39 +by (simp_tac (!simpset addsimps [le_Suc_eq]) 1);
1.40 +by (rtac impI 1);
1.41 +by (etac impE 1);
1.42 +by (atac 1);
1.43 +by (etac le_trans 1);
1.44 +by (res_inst_tac [("m1","n")] (pred_Suc_diff RS subst) 1);
1.45 +by (rtac pred_le 1);
1.46 +qed_spec_mp "diff_le_mono";
1.47 +
1.48 +goal Arith.thy "!!n::nat. m<=n ==> (l-n) <= (l-m)";
1.49 +by (induct_tac "l" 1);
1.50 +by (Simp_tac 1);
1.51 +by (case_tac "n <= l" 1);
1.52 +by (subgoal_tac "m <= l" 1);
1.53 +by (asm_simp_tac (!simpset addsimps [Suc_diff_le]) 1);
1.54 +by (fast_tac (!claset addEs [le_trans]) 1);
1.55 +by (dtac not_leE 1);
1.56 +by (asm_simp_tac (!simpset addsimps [if_Suc_diff_n]) 1);
1.57 +qed_spec_mp "diff_le_mono2";
```