src/HOL/Arith.ML
 changeset 8252 af44242c5e7a parent 8100 6186ee807f2e child 8352 0fda5ba36934
equal inserted replaced
8251:9be357df93d4 8252:af44242c5e7a
`  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:`