equal
deleted
inserted
replaced
31 val nat_diff_split = thm "nat_diff_split"; |
31 val nat_diff_split = thm "nat_diff_split"; |
32 val nat_diff_split_asm = thm "nat_diff_split_asm"; |
32 val nat_diff_split_asm = thm "nat_diff_split_asm"; |
33 *} |
33 *} |
34 (* Careful: arith_tac produces counter examples! |
34 (* Careful: arith_tac produces counter examples! |
35 fun add_arith cs = cs addafter ("arith_tac", arith_tac); |
35 fun add_arith cs = cs addafter ("arith_tac", arith_tac); |
36 TODO: use arith_tac for force_tac in Provers/clasip.ML *) |
36 TODO: use arith_tac for force_tac in Provers/clasimp.ML *) |
37 |
37 |
38 lemmas [arith_split] = nat_diff_split split_min split_max |
38 lemmas [arith_split] = nat_diff_split split_min split_max |
39 |
39 |
40 |
40 |
41 subsubsection {* Generic summation indexed over natural numbers *} |
41 subsection {* Generic summation indexed over natural numbers *} |
42 |
42 |
43 consts |
43 consts |
44 Summation :: "(nat => 'a::{zero, plus}) => nat => 'a" |
44 Summation :: "(nat => 'a::{zero, plus}) => nat => 'a" |
45 primrec |
45 primrec |
46 "Summation f 0 = 0" |
46 "Summation f 0 = 0" |