equal
deleted
inserted
replaced
12 (*elimination of `-' on nat*) |
12 (*elimination of `-' on nat*) |
13 lemma nat_diff_split: |
13 lemma nat_diff_split: |
14 "P(a - b::nat) = ((a<b --> P 0) & (ALL d. a = b + d --> P d))" |
14 "P(a - b::nat) = ((a<b --> P 0) & (ALL d. a = b + d --> P d))" |
15 by (cases "a < b" rule: case_split) (auto simp add: diff_is_0_eq [THEN iffD2]) |
15 by (cases "a < b" rule: case_split) (auto simp add: diff_is_0_eq [THEN iffD2]) |
16 |
16 |
17 ML {* val nat_diff_split = thm "nat_diff_split" *} |
17 ML {* |
|
18 val nat_diff_split = thm "nat_diff_split"; |
|
19 |
|
20 (* TODO: use this for force_tac in Provers/clasip.ML *) |
|
21 fun add_arith cs = cs addaltern ("arith_tac", arith_tac); |
|
22 *} |
18 |
23 |
19 lemmas [arith_split] = nat_diff_split split_min split_max |
24 lemmas [arith_split] = nat_diff_split split_min split_max |
20 |
25 |
|
26 |
21 end |
27 end |