src/HOL/arith_data.ML
changeset 5771 7c2c8cf20221
parent 5591 fbb4e1ac234d
child 5983 79e301a6a51b
     1.1 --- a/src/HOL/arith_data.ML	Mon Oct 26 13:05:08 1998 +0100
     1.2 +++ b/src/HOL/arith_data.ML	Wed Oct 28 11:25:38 1998 +0100
     1.3 @@ -232,3 +232,21 @@
     1.4  by (asm_simp_tac (simpset() addsimps [diff_Suc_le_Suc_diff RS le_less_trans,
     1.5  				      Suc_diff_le, less_imp_le]) 1);
     1.6  qed_spec_mp "diff_less_mono2";
     1.7 +
     1.8 +(** Elimination of - on nat due to John Harrison **)
     1.9 +(*This proof requires natle_cancel_sums*)
    1.10 +
    1.11 +Goal "P(a - b::nat) = (!d. (b = a + d --> P 0) & (a = b + d --> P d))";
    1.12 +by(case_tac "a <= b" 1);
    1.13 +by(Auto_tac);
    1.14 +by(eres_inst_tac [("x","b-a")] allE 1);
    1.15 +by(Auto_tac);
    1.16 +qed "nat_diff_split";
    1.17 +
    1.18 +(*
    1.19 +This is an example of the power of nat_diff_split. Many of the `-' thms in
    1.20 +Arith.ML could take advantage of this, but would need to be moved.
    1.21 +*)
    1.22 +Goal "m-n = 0  -->  n-m = 0  -->  m=n";
    1.23 +by(simp_tac (simpset() addsplits [nat_diff_split]) 1);
    1.24 +qed_spec_mp "diffs0_imp_equal";