1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/sml/IsacKnowledge/Descript.thy Thu Apr 17 18:01:03 2003 +0200
1.3 @@ -0,0 +1,38 @@
1.4 +(* descriptions for items in problem-types
1.5 + WN 1.3.00
1.6 +*)
1.7 +
1.8 +Descript = Script +
1.9 +
1.10 +consts
1.11 +
1.12 + additionalRels :: bool list => una
1.13 + boundVariable :: real => una
1.14 +(*derivative :: 'a => toreal 28.11.00*)
1.15 + derivative :: real => una
1.16 + equalities :: bool list => una
1.17 + equality :: bool => una
1.18 + errorBound :: bool => nam
1.19 +
1.20 + fixedValues :: bool list => nam
1.21 + functionOf :: real => una
1.22 +(*functionTerm :: 'a => toreal 28.11.00*)
1.23 + functionTerm :: real => una
1.24 + interval :: real set => una
1.25 + maxArgument :: bool => toreal
1.26 + maximum :: bool => toreal
1.27 +
1.28 + relations :: bool list => una
1.29 + solutions :: bool list => toreall
1.30 + solution :: bool => toreal
1.31 + solveFor :: real => una
1.32 + differentiateFor:: real => una
1.33 + unknown :: 'a => unknow
1.34 + valuesFor :: bool list => toreall
1.35 +
1.36 + realTestGiven :: real => una
1.37 + realTestFind :: real => una
1.38 + boolTestGiven :: bool => una
1.39 + boolTestFind :: bool => una
1.40 +
1.41 +end
1.42 \ No newline at end of file
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/src/sml/IsacKnowledge/Diff.ML Thu Apr 17 18:01:03 2003 +0200
2.3 @@ -0,0 +1,122 @@
2.4 +(* tools for differentiation
2.5 + WN.11.99
2.6 + use"../knowledge/Diff.ML";
2.7 + use"knowledge/Diff.ML";
2.8 + use"Diff.ML";
2.9 + *)
2.10 +
2.11 +
2.12 +(** interface isabelle -- isac **)
2.13 +
2.14 +theory' := overwritel (!theory', [("Diff.thy",Diff.thy)]);
2.15 +
2.16 +theorem' := overwritel (!theorem',
2.17 +[("diff_const",num_str diff_const),
2.18 + ("diff_prod_const",num_str diff_prod_const),
2.19 + ("diff_var",num_str diff_var),
2.20 + ("diff_sum",num_str diff_sum),
2.21 + ("diff_quot",num_str diff_quot),
2.22 + ("diff_sin",num_str diff_sin),
2.23 + ("diff_sin_chain",num_str diff_sin_chain),
2.24 + ("diff_cos",num_str diff_cos),
2.25 + ("diff_cos_chain",num_str diff_cos_chain),
2.26 + ("diff_pow",num_str diff_pow),
2.27 + ("diff_pow_chain",num_str diff_pow_chain),
2.28 + ("diff_ln",num_str diff_ln),
2.29 + ("diff_ln_chain",num_str diff_ln_chain),
2.30 + ("diff_exp",num_str diff_exp),
2.31 + ("diff_exp_chain",num_str diff_exp_chain),
2.32 + ("diff_sqrt",num_str diff_sqrt),
2.33 + ("diff_sqrt_chain",num_str diff_sqrt_chain)
2.34 +]);
2.35 +
2.36 +
2.37 +(** problem types **)
2.38 +
2.39 +store_pbt
2.40 + (prep_pbt Diff.thy
2.41 + (["function"],
2.42 + [("#Given" ,["functionTerm f_","differentiateFor v_"]),
2.43 + ("#Find" ,["derivative f_'_"])
2.44 + ],
2.45 + append_rls "e_rls" e_rls [], None, []));
2.46 +
2.47 +store_pbt
2.48 + (prep_pbt Diff.thy
2.49 + (["derivative_of","function"],
2.50 + [("#Given" ,["functionTerm f_","differentiateFor v_"]),
2.51 + ("#Find" ,["derivative f_'_"])
2.52 + ],
2.53 + append_rls "e_rls" e_rls [], None, []));
2.54 +
2.55 +
2.56 +(** methods **)
2.57 +
2.58 +methods:= overwritel (!methods,
2.59 +[
2.60 + prep_met
2.61 + (("Diff.thy","differentiate_on_R"),
2.62 + [("#Given" ,["functionTerm f_","differentiateFor v_"]),
2.63 + ("#Find" ,["derivative f_'_"])
2.64 + ],
2.65 + {rew_ord'="tless_true",rls'=atools_erls,calc = [], srls = e_rls, prls=e_rls,
2.66 + asm_rls=[],asm_thm=[("diff_quot","")]},
2.67 + "Script Differentiate (f_::real) (v_::real) = \
2.68 + \((Try (Repeat (Rewrite frac_conv False))) @@ \
2.69 + \ (Try (Repeat (Rewrite root_conv False))) @@ \
2.70 + \ (Try (Repeat (Rewrite realpow_pow False))) @@ \
2.71 + \ (Repeat \
2.72 + \ ((Repeat (Rewrite_Inst [(bdv,v_)] diff_sum False)) Or \
2.73 + \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod_const False)) Or \
2.74 + \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod False)) Or \
2.75 + \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_quot True )) Or \
2.76 + \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin False)) Or \
2.77 + \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin_chain False)) Or \
2.78 + \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos False)) Or \
2.79 + \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos_chain False)) Or \
2.80 + \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow False)) Or \
2.81 + \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow_chain False)) Or \
2.82 + \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln False)) Or \
2.83 + \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln_chain False)) Or \
2.84 + \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp False)) Or \
2.85 + \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp_chain False)) Or \
2.86 + \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_sqrt False)) Or \
2.87 + \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_sqrt_chain False)) Or \
2.88 + \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_const False)) Or \
2.89 + \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_var False)) Or \
2.90 + \ (Repeat (Rewrite_Set make_polynomial False)))) @@ \
2.91 + \ (Try (Repeat (Rewrite sym_frac_conv False))) @@ \
2.92 + \ (Try (Repeat (Rewrite sym_root_conv False)))) (f_::real)"
2.93 + )
2.94 +,
2.95 + prep_met
2.96 + (("Diff.thy","diff_simpl"),
2.97 + [("#Given" ,["functionTerm f_","differentiateFor v_"]),
2.98 + ("#Find" ,["derivative f_'_"])
2.99 + ],
2.100 + {rew_ord'="tless_true",rls'=atools_erls, calc = [], srls = e_rls,prls=e_rls,
2.101 + asm_rls=[],asm_thm=[("diff_quot","")]},
2.102 + "Script Differentiate (f_::real) (v_::real) = \
2.103 + \(Repeat \
2.104 + \ ((Repeat (Rewrite_Inst [(bdv,v_)] diff_sum False)) Or \
2.105 + \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod_const False)) Or \
2.106 + \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod False)) Or \
2.107 + \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_quot True )) Or \
2.108 + \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin False)) Or \
2.109 + \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin_chain False)) Or \
2.110 + \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos False)) Or \
2.111 + \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos_chain False)) Or \
2.112 + \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow False)) Or \
2.113 + \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow_chain False)) Or \
2.114 + \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln False)) Or \
2.115 + \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln_chain False)) Or \
2.116 + \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp False)) Or \
2.117 + \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp_chain False)) Or \
2.118 + \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_sqrt False)) Or \
2.119 + \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_sqrt_chain False)) Or \
2.120 + \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_const False)) Or \
2.121 + \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_var False)) Or \
2.122 + \ (Repeat (Rewrite_Set make_polynomial False)))) \
2.123 + \ (f_::real)"
2.124 + )
2.125 +]);
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/src/sml/IsacKnowledge/Diff.thy Thu Apr 17 18:01:03 2003 +0200
3.3 @@ -0,0 +1,63 @@
3.4 +(* differentiation over the reals
3.5 + WN.16.5.00
3.6 + *)
3.7 +
3.8 +Diff = Calculus + Trig + LogExp + Rational + Root + Poly + Atools +
3.9 +
3.10 +consts
3.11 +
3.12 + d_d :: "[real, real]=> real"
3.13 + sin, cos :: "real => real"
3.14 + log, ln :: "real => real"
3.15 + nlog :: "[real, real] => real"
3.16 + exp :: "real => real" ("e ^^^ _" 80)
3.17 +
3.18 +(*subproblem and script-name*)
3.19 + differentiate :: "[ID * (ID list) * ID, real,real] => real"
3.20 + ("(differentiate (_)/ (_ _ ))" 9)
3.21 + Differentiate :: "[real,real, real] => real"
3.22 + ("((Script Differentiate (_ _ =))// (_))" 9)
3.23 +
3.24 +
3.25 +rules (*stated as axioms, todo: prove as theorems
3.26 + 'bdv' is a constant on the meta-level *)
3.27 + diff_const "[| a is_const; (Not (bdv =!= a)) |] ==> d_d bdv a = 0"
3.28 + diff_var "d_d bdv bdv = 1"
3.29 + diff_prod_const"u is_const ==> d_d bdv (u * v) = u * d_d bdv v"
3.30 +
3.31 + diff_sum "d_d bdv (u + v) = d_d bdv u + d_d bdv v"
3.32 + diff_prod "d_d bdv (u * v) = d_d bdv u * v + u * d_d bdv v"
3.33 + diff_quot "Not (v = 0) ==> (d_d bdv (u / v) = \
3.34 + \(d_d bdv u * v - u * d_d bdv v) / v ^^^ 2)"
3.35 +
3.36 + diff_sin "d_d bdv (sin bdv) = cos bdv"
3.37 + diff_sin_chain "d_d bdv (sin u) = cos u * d_d bdv u"
3.38 + diff_cos "d_d bdv (cos bdv) = - sin bdv"
3.39 + diff_cos_chain "d_d bdv (cos u) = - sin u * d_d bdv u"
3.40 + diff_pow "d_d bdv (bdv ^^^ n) = n * (bdv ^^^ (n - 1))"
3.41 + diff_pow_chain "d_d bdv (u ^^^ n) = n * (u ^^^ (n - 1)) * d_d bdv u"
3.42 + diff_ln "d_d bdv (ln bdv) = 1 / bdv"
3.43 + diff_ln_chain "d_d bdv (ln u) = d_d bdv u / u"
3.44 + diff_exp "d_d bdv (exp bdv) = exp bdv"
3.45 + diff_exp_chain "d_d bdv (exp u) = exp u * d_d x u"
3.46 + diff_sqrt "d_d bdv (sqrt bdv) = 1 / (2 * sqrt bdv)"
3.47 + diff_sqrt_chain"d_d bdv (sqrt u) = d_d bdv u / (2 * sqrt u)"
3.48 + (*...*)
3.49 +
3.50 + frac_conv "a is_const ==> a / b = a * b ^^^ (-1)"
3.51 + root_conv "nroot n u = u ^^^ (1 / n)"
3.52 +
3.53 +end
3.54 +
3.55 +(* a variant of the derivatives defintion:
3.56 +
3.57 + d_d :: "(real => real) => (real => real)"
3.58 +
3.59 + advantages:
3.60 +(1) no variable 'bdv' on the meta-level required
3.61 +(2) chain_rule "d_d (%x. (u (v x))) = (%x. (d_d u)) (v x) * d_d v"
3.62 +(3) and no specialized chain-rules required like
3.63 + diff_sin_chain "d_d bdv (sin u) = cos u * d_d bdv u"
3.64 +
3.65 + disadvantage: d_d (%x. 1 + x^2) = ... differs from high-school notation
3.66 +*)