46 disadvantage: d_d (%x. 1 + x^2) = ... differs from high-school notation |
46 disadvantage: d_d (%x. 1 + x^2) = ... differs from high-school notation |
47 *} |
47 *} |
48 |
48 |
49 axioms (*stated as axioms, todo: prove as theorems |
49 axioms (*stated as axioms, todo: prove as theorems |
50 'bdv' is a constant on the meta-level *) |
50 'bdv' is a constant on the meta-level *) |
51 diff_const "[| Not (bdv occurs_in a) |] ==> d_d bdv a = 0" |
51 diff_const: "[| Not (bdv occurs_in a) |] ==> d_d bdv a = 0" |
52 diff_var "d_d bdv bdv = 1" |
52 diff_var: "d_d bdv bdv = 1" |
53 diff_prod_const"[| Not (bdv occurs_in u) |] ==> |
53 diff_prod_const:"[| Not (bdv occurs_in u) |] ==> |
54 d_d bdv (u * v) = u * d_d bdv v" |
54 d_d bdv (u * v) = u * d_d bdv v" |
55 |
55 |
56 diff_sum "d_d bdv (u + v) = d_d bdv u + d_d bdv v" |
56 diff_sum: "d_d bdv (u + v) = d_d bdv u + d_d bdv v" |
57 diff_dif "d_d bdv (u - v) = d_d bdv u - d_d bdv v" |
57 diff_dif: "d_d bdv (u - v) = d_d bdv u - d_d bdv v" |
58 diff_prod "d_d bdv (u * v) = d_d bdv u * v + u * d_d bdv v" |
58 diff_prod: "d_d bdv (u * v) = d_d bdv u * v + u * d_d bdv v" |
59 diff_quot "Not (v = 0) ==> (d_d bdv (u / v) = |
59 diff_quot: "Not (v = 0) ==> (d_d bdv (u / v) = |
60 (d_d bdv u * v - u * d_d bdv v) / v ^^^ 2)" |
60 (d_d bdv u * v - u * d_d bdv v) / v ^^^ 2)" |
61 |
61 |
62 diff_sin "d_d bdv (sin bdv) = cos bdv" |
62 diff_sin: "d_d bdv (sin bdv) = cos bdv" |
63 diff_sin_chain "d_d bdv (sin u) = cos u * d_d bdv u" |
63 diff_sin_chain: "d_d bdv (sin u) = cos u * d_d bdv u" |
64 diff_cos "d_d bdv (cos bdv) = - sin bdv" |
64 diff_cos: "d_d bdv (cos bdv) = - sin bdv" |
65 diff_cos_chain "d_d bdv (cos u) = - sin u * d_d bdv u" |
65 diff_cos_chain: "d_d bdv (cos u) = - sin u * d_d bdv u" |
66 diff_pow "d_d bdv (bdv ^^^ n) = n * (bdv ^^^ (n - 1))" |
66 diff_pow: "d_d bdv (bdv ^^^ n) = n * (bdv ^^^ (n - 1))" |
67 diff_pow_chain "d_d bdv (u ^^^ n) = n * (u ^^^ (n - 1)) * d_d bdv u" |
67 diff_pow_chain: "d_d bdv (u ^^^ n) = n * (u ^^^ (n - 1)) * d_d bdv u" |
68 diff_ln "d_d bdv (ln bdv) = 1 / bdv" |
68 diff_ln: "d_d bdv (ln bdv) = 1 / bdv" |
69 diff_ln_chain "d_d bdv (ln u) = d_d bdv u / u" |
69 diff_ln_chain: "d_d bdv (ln u) = d_d bdv u / u" |
70 diff_exp "d_d bdv (exp bdv) = exp bdv" |
70 diff_exp: "d_d bdv (exp bdv) = exp bdv" |
71 diff_exp_chain "d_d bdv (exp u) = exp u * d_d x u" |
71 diff_exp_chain: "d_d bdv (exp u) = exp u * d_d x u" |
72 (* |
72 (* |
73 diff_sqrt "d_d bdv (sqrt bdv) = 1 / (2 * sqrt bdv)" |
73 diff_sqrt "d_d bdv (sqrt bdv) = 1 / (2 * sqrt bdv)" |
74 diff_sqrt_chain"d_d bdv (sqrt u) = d_d bdv u / (2 * sqrt u)" |
74 diff_sqrt_chain"d_d bdv (sqrt u) = d_d bdv u / (2 * sqrt u)" |
75 *) |
75 *) |
76 (*...*) |
76 (*...*) |
77 |
77 |
78 frac_conv "[| bdv occurs_in b; 0 < n |] ==> |
78 frac_conv: "[| bdv occurs_in b; 0 < n |] ==> |
79 a / (b ^^^ n) = a * b ^^^ (-n)" |
79 a / (b ^^^ n) = a * b ^^^ (-n)" |
80 frac_sym_conv "n < 0 ==> a * b ^^^ n = a / b ^^^ (-n)" |
80 frac_sym_conv: "n < 0 ==> a * b ^^^ n = a / b ^^^ (-n)" |
81 |
81 |
82 sqrt_conv_bdv "sqrt bdv = bdv ^^^ (1 / 2)" |
82 sqrt_conv_bdv: "sqrt bdv = bdv ^^^ (1 / 2)" |
83 sqrt_conv_bdv_n "sqrt (bdv ^^^ n) = bdv ^^^ (n / 2)" |
83 sqrt_conv_bdv_n: "sqrt (bdv ^^^ n) = bdv ^^^ (n / 2)" |
84 sqrt_conv "bdv occurs_in u ==> sqrt u = u ^^^ (1 / 2)" |
84 sqrt_conv: "bdv occurs_in u ==> sqrt u = u ^^^ (1 / 2)" |
85 sqrt_sym_conv "u ^^^ (a / 2) = sqrt (u ^^^ a)" |
85 sqrt_sym_conv: "u ^^^ (a / 2) = sqrt (u ^^^ a)" |
86 |
86 |
87 root_conv "bdv occurs_in u ==> nroot n u = u ^^^ (1 / n)" |
87 root_conv: "bdv occurs_in u ==> nroot n u = u ^^^ (1 / n)" |
88 root_sym_conv "u ^^^ (a / b) = nroot b (u ^^^ a)" |
88 root_sym_conv: "u ^^^ (a / b) = nroot b (u ^^^ a)" |
89 |
89 |
90 realpow_pow_bdv "(bdv ^^^ b) ^^^ c = bdv ^^^ (b * c)" |
90 realpow_pow_bdv: "(bdv ^^^ b) ^^^ c = bdv ^^^ (b * c)" |
91 |
91 |
92 ML {* |
92 ML {* |
93 val thy = @{theory}; |
93 val thy = @{theory}; |
94 |
94 |
95 (** eval functions **) |
95 (** eval functions **) |