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","ba")] allE 1); 
1013 by (eres_inst_tac [("x","ba")] 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: 