1004 solver all the time rather than add the additional check. *) |
1004 solver all the time rather than add the additional check. *) |
1005 |
1005 |
1006 simpset_ref () := (simpset() addSolver |
1006 simpset_ref () := (simpset() addSolver |
1007 (mk_solver "lin. arith." Fast_Arith.cut_lin_arith_tac)); |
1007 (mk_solver "lin. arith." Fast_Arith.cut_lin_arith_tac)); |
1008 |
1008 |
1009 (*Elimination of `-' on nat due to John Harrison. An alternative is to |
1009 (*Elimination of `-' on nat due to John Harrison. *) |
1010 replace b=a+d by a<b; not clear that it makes much difference. *) |
|
1011 Goal "P(a - b::nat) = (ALL d. (b = a + d --> P 0) & (a = b + d --> P d))"; |
1010 Goal "P(a - b::nat) = (ALL d. (b = a + d --> P 0) & (a = b + d --> P d))"; |
1012 by (case_tac "a <= b" 1); |
1011 by (case_tac "a <= b" 1); |
1013 by Auto_tac; |
1012 by Auto_tac; |
1014 by (eres_inst_tac [("x","b-a")] allE 1); |
1013 by (eres_inst_tac [("x","b-a")] allE 1); |
1015 by (asm_simp_tac (simpset() addsimps [diff_is_0_eq RS iffD2]) 1); |
1014 by (asm_simp_tac (simpset() addsimps [diff_is_0_eq RS iffD2]) 1); |
1016 qed "nat_diff_split"; |
1015 qed "nat_diff_split"; |
|
1016 |
|
1017 (*LCP's version, replacing b=a+d by a<b, which sometimes works better*) |
|
1018 Goal "P(a - b::nat) = (ALL d. (a<b --> P 0) & (a = b + d --> P d))"; |
|
1019 by (auto_tac (claset(), simpset() addsplits [nat_diff_split])); |
|
1020 qed "nat_diff_split'"; |
1017 |
1021 |
1018 |
1022 |
1019 (* FIXME: K true should be replaced by a sensible test to speed things up |
1023 (* FIXME: K true should be replaced by a sensible test to speed things up |
1020 in case there are lots of irrelevant terms involved; |
1024 in case there are lots of irrelevant terms involved; |
1021 elimination of min/max can be optimized: |
1025 elimination of min/max can be optimized: |