1.1 --- a/src/Tools/isac/Knowledge/Diff.thy Mon Sep 06 15:53:18 2010 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Diff.thy Mon Sep 06 16:56:22 2010 +0200
1.3 @@ -48,46 +48,46 @@
1.4
1.5 axioms (*stated as axioms, todo: prove as theorems
1.6 'bdv' is a constant on the meta-level *)
1.7 - diff_const "[| Not (bdv occurs_in a) |] ==> d_d bdv a = 0"
1.8 - diff_var "d_d bdv bdv = 1"
1.9 - diff_prod_const"[| Not (bdv occurs_in u) |] ==>
1.10 + diff_const: "[| Not (bdv occurs_in a) |] ==> d_d bdv a = 0"
1.11 + diff_var: "d_d bdv bdv = 1"
1.12 + diff_prod_const:"[| Not (bdv occurs_in u) |] ==>
1.13 d_d bdv (u * v) = u * d_d bdv v"
1.14
1.15 - diff_sum "d_d bdv (u + v) = d_d bdv u + d_d bdv v"
1.16 - diff_dif "d_d bdv (u - v) = d_d bdv u - d_d bdv v"
1.17 - diff_prod "d_d bdv (u * v) = d_d bdv u * v + u * d_d bdv v"
1.18 - diff_quot "Not (v = 0) ==> (d_d bdv (u / v) =
1.19 + diff_sum: "d_d bdv (u + v) = d_d bdv u + d_d bdv v"
1.20 + diff_dif: "d_d bdv (u - v) = d_d bdv u - d_d bdv v"
1.21 + diff_prod: "d_d bdv (u * v) = d_d bdv u * v + u * d_d bdv v"
1.22 + diff_quot: "Not (v = 0) ==> (d_d bdv (u / v) =
1.23 (d_d bdv u * v - u * d_d bdv v) / v ^^^ 2)"
1.24
1.25 - diff_sin "d_d bdv (sin bdv) = cos bdv"
1.26 - diff_sin_chain "d_d bdv (sin u) = cos u * d_d bdv u"
1.27 - diff_cos "d_d bdv (cos bdv) = - sin bdv"
1.28 - diff_cos_chain "d_d bdv (cos u) = - sin u * d_d bdv u"
1.29 - diff_pow "d_d bdv (bdv ^^^ n) = n * (bdv ^^^ (n - 1))"
1.30 - diff_pow_chain "d_d bdv (u ^^^ n) = n * (u ^^^ (n - 1)) * d_d bdv u"
1.31 - diff_ln "d_d bdv (ln bdv) = 1 / bdv"
1.32 - diff_ln_chain "d_d bdv (ln u) = d_d bdv u / u"
1.33 - diff_exp "d_d bdv (exp bdv) = exp bdv"
1.34 - diff_exp_chain "d_d bdv (exp u) = exp u * d_d x u"
1.35 + diff_sin: "d_d bdv (sin bdv) = cos bdv"
1.36 + diff_sin_chain: "d_d bdv (sin u) = cos u * d_d bdv u"
1.37 + diff_cos: "d_d bdv (cos bdv) = - sin bdv"
1.38 + diff_cos_chain: "d_d bdv (cos u) = - sin u * d_d bdv u"
1.39 + diff_pow: "d_d bdv (bdv ^^^ n) = n * (bdv ^^^ (n - 1))"
1.40 + diff_pow_chain: "d_d bdv (u ^^^ n) = n * (u ^^^ (n - 1)) * d_d bdv u"
1.41 + diff_ln: "d_d bdv (ln bdv) = 1 / bdv"
1.42 + diff_ln_chain: "d_d bdv (ln u) = d_d bdv u / u"
1.43 + diff_exp: "d_d bdv (exp bdv) = exp bdv"
1.44 + diff_exp_chain: "d_d bdv (exp u) = exp u * d_d x u"
1.45 (*
1.46 diff_sqrt "d_d bdv (sqrt bdv) = 1 / (2 * sqrt bdv)"
1.47 diff_sqrt_chain"d_d bdv (sqrt u) = d_d bdv u / (2 * sqrt u)"
1.48 *)
1.49 (*...*)
1.50
1.51 - frac_conv "[| bdv occurs_in b; 0 < n |] ==>
1.52 + frac_conv: "[| bdv occurs_in b; 0 < n |] ==>
1.53 a / (b ^^^ n) = a * b ^^^ (-n)"
1.54 - frac_sym_conv "n < 0 ==> a * b ^^^ n = a / b ^^^ (-n)"
1.55 + frac_sym_conv: "n < 0 ==> a * b ^^^ n = a / b ^^^ (-n)"
1.56
1.57 - sqrt_conv_bdv "sqrt bdv = bdv ^^^ (1 / 2)"
1.58 - sqrt_conv_bdv_n "sqrt (bdv ^^^ n) = bdv ^^^ (n / 2)"
1.59 - sqrt_conv "bdv occurs_in u ==> sqrt u = u ^^^ (1 / 2)"
1.60 - sqrt_sym_conv "u ^^^ (a / 2) = sqrt (u ^^^ a)"
1.61 + sqrt_conv_bdv: "sqrt bdv = bdv ^^^ (1 / 2)"
1.62 + sqrt_conv_bdv_n: "sqrt (bdv ^^^ n) = bdv ^^^ (n / 2)"
1.63 + sqrt_conv: "bdv occurs_in u ==> sqrt u = u ^^^ (1 / 2)"
1.64 + sqrt_sym_conv: "u ^^^ (a / 2) = sqrt (u ^^^ a)"
1.65
1.66 - root_conv "bdv occurs_in u ==> nroot n u = u ^^^ (1 / n)"
1.67 - root_sym_conv "u ^^^ (a / b) = nroot b (u ^^^ a)"
1.68 + root_conv: "bdv occurs_in u ==> nroot n u = u ^^^ (1 / n)"
1.69 + root_sym_conv: "u ^^^ (a / b) = nroot b (u ^^^ a)"
1.70
1.71 - realpow_pow_bdv "(bdv ^^^ b) ^^^ c = bdv ^^^ (b * c)"
1.72 + realpow_pow_bdv: "(bdv ^^^ b) ^^^ c = bdv ^^^ (b * c)"
1.73
1.74 ML {*
1.75 val thy = @{theory};