1.1 --- a/src/Tools/isac/Build_Isac.thy Wed Sep 08 16:54:15 2010 +0200
1.2 +++ b/src/Tools/isac/Build_Isac.thy Wed Sep 08 17:17:29 2010 +0200
1.3 @@ -77,8 +77,9 @@
1.4 use_thy "Knowledge/Vect"
1.5 use_thy "Knowledge/Calculus"
1.6 use_thy "Knowledge/Trig"
1.7 +use_thy "Knowledge/LogExp"
1.8
1.9 -use_thy "Knowledge/LogExp"
1.10 +use_thy "Knowledge/Diff"
1.11
1.12 ML {*
1.13 *}
1.14 @@ -86,7 +87,6 @@
1.15
1.16 text {*------------------------------------------*}
1.17 (*
1.18 -use_thy "Knowledge/Diff"
1.19 use_thy "Knowledge/DiffApp"
1.20 use_thy "Knowledge/Integrate"
1.21 use_thy "Knowledge/EqSystem"
2.1 --- a/src/Tools/isac/Knowledge/Diff.thy Wed Sep 08 16:54:15 2010 +0200
2.2 +++ b/src/Tools/isac/Knowledge/Diff.thy Wed Sep 08 17:17:29 2010 +0200
2.3 @@ -5,17 +5,21 @@
2.4
2.5 theory Diff imports Calculus Trig LogExp Rational Root Poly Atools begin
2.6
2.7 +ML {*
2.8 +@{term "sin x"}
2.9 +*}
2.10 +
2.11 consts
2.12
2.13 d_d :: "[real, real]=> real"
2.14 - sin, cos :: "real => real"
2.15 +(*sin, cos :: "real => real" already in Isabelle2009-2*)
2.16 (*
2.17 log, ln :: "real => real"
2.18 nlog :: "[real, real] => real"
2.19 exp :: "real => real" ("E'_ ^^^ _" 80)
2.20 *)
2.21 (*descriptions in the related problems*)
2.22 - derivativeEq :: bool => una
2.23 + derivativeEq :: "bool => una"
2.24
2.25 (*predicates*)
2.26 primed :: "'a => 'a" (*"primed A" -> "A'"*)
2.27 @@ -30,7 +34,7 @@
2.28 ("(differentiate (_)/ (_ _ ))" 9)
2.29 DiffScr :: "[real,real, real] => real"
2.30 ("((Script DiffScr (_ _ =))// (_))" 9)
2.31 - DiffEqScr :: "[bool,real, bool] => bool"
2.32 + DiffEqScr :: "[bool,real, bool] => bool"
2.33 ("((Script DiffEqScr (_ _ =))// (_))" 9)
2.34
2.35 text {*a variant of the derivatives defintion:
2.36 @@ -107,8 +111,8 @@
2.37 calclist':= overwritel (!calclist',
2.38 [("primed", ("Diff.primed", eval_primed "#primed"))
2.39 ]);
2.40 -
2.41 -
2.42 +*}
2.43 +ML {*
2.44 (** rulesets **)
2.45
2.46 (*.converts a term such that differentiation works optimally.*)
2.47 @@ -122,7 +126,7 @@
2.48 Thm ("not_false",num_str @{thm not_false}),
2.49 Calc ("op <",eval_equ "#less_"),
2.50 Thm ("and_true",num_str @{thm and_true}),
2.51 - Thm ("and_false",num_str @{thm and_false)
2.52 + Thm ("and_false",num_str @{thm and_false})
2.53 ],
2.54 srls = Erls, calc = [],
2.55 rules = [Thm ("frac_conv", num_str @{thm frac_conv}),
2.56 @@ -138,11 +142,10 @@
2.57 (*?x * (?y / ?z) = ?x * ?y / ?z*)
2.58 Thm ("times_divide_eq_left",num_str @{thm times_divide_eq_left})
2.59 (*?y / ?z * ?x = ?y * ?x / ?z*)
2.60 - (*
2.61 - Thm ("", num_str @{}),*)
2.62 ],
2.63 scr = EmptyScr};
2.64 -
2.65 +*}
2.66 +ML {*
2.67 (*.beautifies a term after differentiation.*)
2.68 val diff_sym_conv =
2.69 Rls {id="diff_sym_conv",
2.70 @@ -180,7 +183,8 @@
2.71 Calc("Diff.primed", eval_primed "Diff.primed")
2.72 ],
2.73 scr = EmptyScr};
2.74 -
2.75 +*}
2.76 +ML {*
2.77 (*..*)
2.78 val erls_diff =
2.79 append_rls "erls_differentiate.." e_rls
2.80 @@ -220,7 +224,8 @@
2.81 Thm ("diff_var",num_str @{thm diff_var})
2.82 ],
2.83 scr = EmptyScr};
2.84 -
2.85 +*}
2.86 +ML {*
2.87 (*.normalisation for checking user-input.*)
2.88 val norm_diff =
2.89 Rls {id="diff_rls", preconds = [], rew_ord = ("termlessI",termlessI),
2.90 @@ -237,7 +242,8 @@
2.91 ("diff_sym_conv", prep_rls diff_sym_conv)
2.92 ]);
2.93
2.94 -
2.95 +*}
2.96 +ML {*
2.97 (** problem types **)
2.98
2.99 store_pbt
2.100 @@ -247,23 +253,24 @@
2.101 store_pbt
2.102 (prep_pbt thy "pbl_fun_deriv" [] e_pblID
2.103 (["derivative_of","function"],
2.104 - [("#Given" ,["functionTerm f_","differentiateFor v_v"]),
2.105 - ("#Find" ,["derivative f_'_"])
2.106 + [("#Given" ,["functionTerm f_f","differentiateFor v_v"]),
2.107 + ("#Find" ,["derivative f_f'"])
2.108 ],
2.109 append_rls "e_rls" e_rls [],
2.110 - SOME "Diff (f_, v_v)", [["diff","differentiate_on_R"],
2.111 + SOME "Diff (f_f, v_v)", [["diff","differentiate_on_R"],
2.112 ["diff","after_simplification"]]));
2.113
2.114 (*here "named" is used differently from Integration"*)
2.115 store_pbt
2.116 (prep_pbt thy "pbl_fun_deriv_nam" [] e_pblID
2.117 (["named","derivative_of","function"],
2.118 - [("#Given" ,["functionEq f_","differentiateFor v_v"]),
2.119 - ("#Find" ,["derivativeEq f_'_"])
2.120 + [("#Given" ,["functionEq f_f","differentiateFor v_v"]),
2.121 + ("#Find" ,["derivativeEq f_f'"])
2.122 ],
2.123 append_rls "e_rls" e_rls [],
2.124 - SOME "Differentiate (f_, v_v)", [["diff","differentiate_equality"]]));
2.125 -
2.126 + SOME "Differentiate (f_f, v_v)", [["diff","differentiate_equality"]]));
2.127 +*}
2.128 +ML {*
2.129
2.130 (** methods **)
2.131
2.132 @@ -276,13 +283,13 @@
2.133 store_met
2.134 (prep_met thy "met_diff_onR" [] e_metID
2.135 (["diff","differentiate_on_R"],
2.136 - [("#Given" ,["functionTerm f_","differentiateFor v_v"]),
2.137 - ("#Find" ,["derivative f_'_"])
2.138 + [("#Given" ,["functionTerm f_f","differentiateFor v_v"]),
2.139 + ("#Find" ,["derivative f_f'"])
2.140 ],
2.141 {rew_ord'="tless_true", rls' = erls_diff, calc = [], srls = e_rls,
2.142 prls=e_rls, crls = Atools_erls, nrls = norm_diff},
2.143 -"Script DiffScr (f_::real) (v_v::real) = " ^
2.144 -" (let f'_ = Take (d_d v_v f_) " ^
2.145 +"Script DiffScr (f_f::real) (v_v::real) = " ^
2.146 +" (let f_f' = Take (d_d v_v f_f) " ^
2.147 " in (((Try (Rewrite_Set_Inst [(bdv,v_v)] diff_conv False)) @@ " ^
2.148 " (Repeat " ^
2.149 " ((Repeat (Rewrite_Inst [(bdv,v_v)] diff_sum False)) Or " ^
2.150 @@ -302,19 +309,20 @@
2.151 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_const False)) Or " ^
2.152 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_var False)) Or " ^
2.153 " (Repeat (Rewrite_Set make_polynomial False)))) @@ " ^
2.154 -" (Try (Rewrite_Set_Inst [(bdv,v_v)] diff_sym_conv False)))) f'_)"
2.155 +" (Try (Rewrite_Set_Inst [(bdv,v_v)] diff_sym_conv False)))) f_f')"
2.156 ));
2.157 -
2.158 +*}
2.159 +ML {*
2.160 store_met
2.161 (prep_met thy "met_diff_simpl" [] e_metID
2.162 (["diff","diff_simpl"],
2.163 - [("#Given" ,["functionTerm f_","differentiateFor v_v"]),
2.164 - ("#Find" ,["derivative f_'_"])
2.165 + [("#Given" ,["functionTerm f_f","differentiateFor v_v"]),
2.166 + ("#Find" ,["derivative f_f'"])
2.167 ],
2.168 {rew_ord'="tless_true", rls' = erls_diff, calc = [], srls = e_rls,
2.169 prls=e_rls, crls = Atools_erls, nrls = norm_diff},
2.170 -"Script DiffScr (f_::real) (v_v::real) = " ^
2.171 -" (let f'_ = Take (d_d v_v f_) " ^
2.172 +"Script DiffScr (f_f::real) (v_v::real) = " ^
2.173 +" (let f_f' = Take (d_d v_v f_f) " ^
2.174 " in (( " ^
2.175 " (Repeat " ^
2.176 " ((Repeat (Rewrite_Inst [(bdv,v_v)] diff_sum False)) Or " ^
2.177 @@ -334,19 +342,19 @@
2.178 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_const False)) Or " ^
2.179 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_var False)) Or " ^
2.180 " (Repeat (Rewrite_Set make_polynomial False)))) " ^
2.181 -" )) f'_)"
2.182 +" )) f_f')"
2.183 ));
2.184
2.185 store_met
2.186 (prep_met thy "met_diff_equ" [] e_metID
2.187 (["diff","differentiate_equality"],
2.188 - [("#Given" ,["functionEq f_","differentiateFor v_v"]),
2.189 - ("#Find" ,["derivativeEq f_'_"])
2.190 + [("#Given" ,["functionEq f_f","differentiateFor v_v"]),
2.191 + ("#Find" ,["derivativeEq f_f'"])
2.192 ],
2.193 {rew_ord'="tless_true", rls' = erls_diff, calc = [],
2.194 srls = srls_diff, prls=e_rls, crls=Atools_erls, nrls = norm_diff},
2.195 -"Script DiffEqScr (f_::bool) (v_v::real) = " ^
2.196 -" (let f'_ = Take ((primed (lhs f_)) = d_d v_v (rhs f_)) " ^
2.197 +"Script DiffEqScr (f_f::bool) (v_v::real) = " ^
2.198 +" (let f_f' = Take ((primed (lhs f_f)) = d_d v_v (rhs f_f)) " ^
2.199 " in (((Try (Rewrite_Set_Inst [(bdv,v_v)] diff_conv False)) @@ " ^
2.200 " (Repeat " ^
2.201 " ((Repeat (Rewrite_Inst [(bdv,v_v)] diff_sum False)) Or " ^
2.202 @@ -367,24 +375,24 @@
2.203 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_const False)) Or " ^
2.204 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_var False)) Or " ^
2.205 " (Repeat (Rewrite_Set make_polynomial False)))) @@ " ^
2.206 -" (Try (Rewrite_Set_Inst [(bdv,v_v)] diff_sym_conv False)))) f'_)"
2.207 +" (Try (Rewrite_Set_Inst [(bdv,v_v)] diff_sym_conv False)))) f_f')"
2.208 ));
2.209
2.210 store_met
2.211 (prep_met thy "met_diff_after_simp" [] e_metID
2.212 (["diff","after_simplification"],
2.213 - [("#Given" ,["functionTerm f_","differentiateFor v_v"]),
2.214 - ("#Find" ,["derivative f_'_"])
2.215 + [("#Given" ,["functionTerm f_f","differentiateFor v_v"]),
2.216 + ("#Find" ,["derivative f_f'"])
2.217 ],
2.218 {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls, prls=e_rls,
2.219 crls=Atools_erls, nrls = norm_Rational},
2.220 -"Script DiffScr (f_::real) (v_v::real) = " ^
2.221 -" (let f'_ = Take (d_d v_v f_) " ^
2.222 +"Script DiffScr (f_f::real) (v_v::real) = " ^
2.223 +" (let f_f' = Take (d_d v_v f_f) " ^
2.224 " in ((Try (Rewrite_Set norm_Rational False)) @@ " ^
2.225 " (Try (Rewrite_Set_Inst [(bdv,v_v)] diff_conv False)) @@ " ^
2.226 " (Try (Rewrite_Set_Inst [(bdv,v_v)] norm_diff False)) @@ " ^
2.227 " (Try (Rewrite_Set_Inst [(bdv,v_v)] diff_sym_conv False)) @@ " ^
2.228 -" (Try (Rewrite_Set norm_Rational False))) f'_)"
2.229 +" (Try (Rewrite_Set norm_Rational False))) f_f')"
2.230 ));
2.231
2.232
2.233 @@ -398,7 +406,7 @@
2.234 [((term_of o the o (parse thy)) "functionTerm", [t]),
2.235 ((term_of o the o (parse thy)) "differentiateFor", [bdv]),
2.236 ((term_of o the o (parse thy)) "derivative",
2.237 - [(term_of o the o (parse thy)) "f_'_"])
2.238 + [(term_of o the o (parse thy)) "f_f'"])
2.239 ]
2.240 | argl2dtss _ = raise error "Diff.ML: wrong argument for argl2dtss";
2.241 castab :=
2.242 @@ -416,7 +424,7 @@
2.243 [((term_of o the o (parse thy)) "functionEq", [t]),
2.244 ((term_of o the o (parse thy)) "differentiateFor", [bdv]),
2.245 ((term_of o the o (parse thy)) "derivativeEq",
2.246 - [(term_of o the o (parse thy)) "f_'_::bool"])
2.247 + [(term_of o the o (parse thy)) "f_f'::bool"])
2.248 ]
2.249 | argl2dtss _ = raise error "Diff.ML: wrong argument for argl2dtss";
2.250 castab :=