summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/Arith.ML

changeset 8252 | af44242c5e7a |

parent 8100 | 6186ee807f2e |

child 8352 | 0fda5ba36934 |

--- a/src/HOL/Arith.ML Fri Feb 18 15:20:44 2000 +0100 +++ b/src/HOL/Arith.ML Fri Feb 18 15:28:32 2000 +0100 @@ -1006,8 +1006,7 @@ simpset_ref () := (simpset() addSolver (mk_solver "lin. arith." Fast_Arith.cut_lin_arith_tac)); -(*Elimination of `-' on nat due to John Harrison. An alternative is to - replace b=a+d by a<b; not clear that it makes much difference. *) +(*Elimination of `-' on nat due to John Harrison. *) Goal "P(a - b::nat) = (ALL d. (b = a + d --> P 0) & (a = b + d --> P d))"; by (case_tac "a <= b" 1); by Auto_tac; @@ -1015,6 +1014,11 @@ by (asm_simp_tac (simpset() addsimps [diff_is_0_eq RS iffD2]) 1); qed "nat_diff_split"; +(*LCP's version, replacing b=a+d by a<b, which sometimes works better*) +Goal "P(a - b::nat) = (ALL d. (a<b --> P 0) & (a = b + d --> P d))"; +by (auto_tac (claset(), simpset() addsplits [nat_diff_split])); +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;