29 axioms |
29 axioms |
30 (*stated as axioms, todo: prove as theorems |
30 (*stated as axioms, todo: prove as theorems |
31 'bdv' is a constant handled on the meta-level |
31 'bdv' is a constant handled on the meta-level |
32 specifically as a 'bound variable' *) |
32 specifically as a 'bound variable' *) |
33 |
33 |
34 integral_const "Not (bdv occurs_in u) ==> Integral u D bdv = u * bdv" |
34 integral_const: "Not (bdv occurs_in u) ==> Integral u D bdv = u * bdv" |
35 integral_var "Integral bdv D bdv = bdv ^^^ 2 / 2" |
35 integral_var: "Integral bdv D bdv = bdv ^^^ 2 / 2" |
36 |
36 |
37 integral_add "Integral (u + v) D bdv = |
37 integral_add: "Integral (u + v) D bdv = |
38 (Integral u D bdv) + (Integral v D bdv)" |
38 (Integral u D bdv) + (Integral v D bdv)" |
39 integral_mult "[| Not (bdv occurs_in u); bdv occurs_in v |] ==> |
39 integral_mult: "[| Not (bdv occurs_in u); bdv occurs_in v |] ==> |
40 Integral (u * v) D bdv = u * (Integral v D bdv)" |
40 Integral (u * v) D bdv = u * (Integral v D bdv)" |
41 (*WN080222: this goes into sub-terms, too ... |
41 (*WN080222: this goes into sub-terms, too ... |
42 call_for_new_c "[| Not (matches (u + new_c v) a); Not (a is_f_x) |] ==> |
42 call_for_new_c: "[| Not (matches (u + new_c v) a); Not (a is_f_x) |] ==> |
43 a = a + new_c a" |
43 a = a + new_c a" |
44 *) |
44 *) |
45 integral_pow "Integral bdv ^^^ n D bdv = bdv ^^^ (n+1) / (n + 1)" |
45 integral_pow: "Integral bdv ^^^ n D bdv = bdv ^^^ (n+1) / (n + 1)" |
46 |
46 |
47 ML {* |
47 ML {* |
48 val thy = @{theory}; |
48 val thy = @{theory}; |
49 |
49 |
50 (** eval functions **) |
50 (** eval functions **) |