# HG changeset patch # User paulson # Date 941021448 -7200 # Node ID 3aca6352f063ae946600e039f06baa616954e069 # Parent cc1930ad1a88ab31bc14d797c5da052ea5b55337 got rid of split_diff, which duplicated nat_diff_split, and also disposed of remove_diff_ss diff -r cc1930ad1a88 -r 3aca6352f063 src/HOL/Arith.ML --- a/src/HOL/Arith.ML Wed Oct 27 11:15:35 1999 +0200 +++ b/src/HOL/Arith.ML Wed Oct 27 12:50:48 1999 +0200 @@ -132,13 +132,6 @@ qed "add_gr_0"; AddIffs [add_gr_0]; -(* FIXME: really needed?? *) -Goal "((m+n)-1 = 0) = (m=0 & n-1 = 0 | m-1 = 0 & n=0)"; -by (exhaust_tac "m" 1); -by (ALLGOALS (fast_tac (claset() addss (simpset())))); -qed "pred_add_is_0"; -(*Addsimps [pred_add_is_0];*) - (* Could be generalized, eg to "k m+(n-(Suc k)) = (m+n)-(Suc k)" *) Goal "0 m + (n-1) = (m+n)-1"; by (exhaust_tac "m" 1); @@ -1013,14 +1006,16 @@ simpset_ref () := (simpset() addSolver (mk_solver "lin. arith." Fast_Arith.cut_lin_arith_tac)); -(* Elimination of `-' on nat due to John Harrison *) -Goal "P(a - b::nat) = (!d. (b = a + d --> P 0) & (a = b + d --> P d))"; +(*Elimination of `-' on nat due to John Harrison. An alternative is to + replace b=a+d by a P 0) & (a = b + d --> P d))"; by (case_tac "a <= b" 1); by Auto_tac; by (eres_inst_tac [("x","b-a")] allE 1); by (asm_simp_tac (simpset() addsimps [diff_is_0_eq RS iffD2]) 1); qed "nat_diff_split"; + (* FIXME: K true should be replaced by a sensible test to speed things up in case there are lots of irrelevant terms involved; elimination of min/max can be optimized: @@ -1120,38 +1115,24 @@ (*** Reducting subtraction to addition ***) -(*Intended for use with linear arithmetic, but useful in its own right*) -Goal "P (x-y) = (ALL z. (x P 0) & (x = y+z --> P z))"; -by (case_tac "x Suc l - n + m = Suc (l - n + m)"; -by (simp_tac remove_diff_ss 1); +by (simp_tac (simpset() addsplits [nat_diff_split]) 1); qed_spec_mp "Suc_diff_add_le"; Goal "i n - Suc i < n - i"; -by (asm_simp_tac remove_diff_ss 1); +by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1); qed "diff_Suc_less_diff"; Goal "Suc(m)-n = (if m (m-k) - (n-k) = m-(n::nat)"; -by (asm_simp_tac remove_diff_ss 1); +by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1); qed "diff_right_cancel"; @@ -1159,18 +1140,17 @@ (* Monotonicity of subtraction in first argument *) Goal "m <= (n::nat) ==> (m-l) <= (n-l)"; -by (asm_simp_tac remove_diff_ss 1); +by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1); qed "diff_le_mono"; Goal "m <= (n::nat) ==> (l-n) <= (l-m)"; -by (asm_simp_tac remove_diff_ss 1); +by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1); qed "diff_le_mono2"; -(*This proof requires natdiff_cancel_sums*) Goal "[| m < (n::nat); m (l-n) < (l-m)"; -by (asm_simp_tac remove_diff_ss 1); +by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1); qed "diff_less_mono2"; Goal "[| m-n = 0; n-m = 0 |] ==> m=n"; -by (asm_full_simp_tac remove_diff_ss 1); +by (asm_full_simp_tac (simpset() addsplits [nat_diff_split]) 1); qed "diffs0_imp_equal";