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.14  Addsimps [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.20 +AddIffs [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.30  qed "le_add_diff";
    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";