1.1 --- a/src/Tools/isac/Knowledge/AlgEin.thy Fri Aug 27 10:39:12 2010 +0200
1.2 +++ b/src/Tools/isac/Knowledge/AlgEin.thy Fri Aug 27 14:56:54 2010 +0200
1.3 @@ -1,16 +1,9 @@
1.4 (* Algebra Einf"uhrung, Unterrichtsversuch IMST-Projekt
1.5 author: Walther Neuper 2007
1.6 (c) due to copyright terms
1.7 -
1.8 -remove_thy"AlgEin";
1.9 -use_thy"Knowledge/AlgEin";
1.10 -use_thy_only"Knowledge/AlgEin";
1.11 -
1.12 -remove_thy"AlgEin";
1.13 -use_thy"Knowledge/Isac";
1.14 *)
1.15
1.16 -AlgEin = Rational +
1.17 +theory AlgEin imports Rational begin
1.18 (*Poly + ..shouldbe sufficient, but norm_Poly *)
1.19
1.20 consts
1.21 @@ -28,10 +21,127 @@
1.22 bool] => bool"
1.23 ("((Script RechnenSymbolScript (_ _ _ _ _ _ =))// (_))" 9)
1.24
1.25 -(*
1.26 -rules
1.27 - (*this axiom creates a contradictory formal system,
1.28 - see problem TOOODO *)
1.29 +ML {*
1.30 +(** problems **)
1.31 +
1.32 +store_pbt
1.33 + (prep_pbt (theory "AlgEin") "pbl_algein" [] e_pblID
1.34 + (["Berechnung"], [], e_rls, NONE,
1.35 + []));
1.36 +(* WN070405
1.37 +store_pbt
1.38 + (prep_pbt (theory "AlgEin") "pbl_algein_num" [] e_pblID
1.39 + (["numerische", "Berechnung"],
1.40 + [("#Given" ,["KantenUnten u_", "KantenSenkrecht s_", "KantenOben o_"]),
1.41 + ("#Find" ,["GesamtLaenge l_"])
1.42 + ],
1.43 + append_rls "e_rls" e_rls [],
1.44 + NONE,
1.45 + []));
1.46 *)
1.47 +store_pbt
1.48 + (prep_pbt (theory "AlgEin") "pbl_algein_numsym" [] e_pblID
1.49 + (["numerischSymbolische", "Berechnung"],
1.50 + [("#Given" ,["KantenLaenge k_","Querschnitt q__"(*q_ in Biegelinie.thy*),
1.51 + "KantenUnten u_", "KantenSenkrecht s_", "KantenOben o_"]),
1.52 + ("#Find" ,["GesamtLaenge l_"])
1.53 + ],
1.54 + e_rls,
1.55 + NONE,
1.56 + [["Berechnung","erstNumerisch"],["Berechnung","erstSymbolisch"]]));
1.57 +
1.58 +(* show_ptyps();
1.59 + *)
1.60 +
1.61 +
1.62 +(** methods **)
1.63 +
1.64 +store_met
1.65 + (prep_met (theory "AlgEin") "met_algein" [] e_metID
1.66 + (["Berechnung"],
1.67 + [],
1.68 + {rew_ord'="tless_true", rls'= Erls, calc = [],
1.69 + srls = Erls, prls = Erls,
1.70 + crls =Erls , nrls = Erls},
1.71 +"empty_script"
1.72 +));
1.73 +
1.74 +store_met
1.75 + (prep_met (theory "AlgEin") "met_algein_numsym" [] e_metID
1.76 + (["Berechnung","erstNumerisch"],
1.77 + [],
1.78 + {rew_ord'="tless_true", rls'= Erls, calc = [],
1.79 + srls = Erls, prls = Erls,
1.80 + crls =Erls , nrls = Erls},
1.81 +"empty_script"
1.82 +));
1.83 +
1.84 +store_met
1.85 + (prep_met (theory "AlgEin") "met_algein_numsym" [] e_metID
1.86 + (["Berechnung","erstNumerisch"],
1.87 + [("#Given" ,["KantenLaenge k_","Querschnitt q__",
1.88 + "KantenUnten u_", "KantenSenkrecht s_",
1.89 + "KantenOben o_"]),
1.90 + ("#Find" ,["GesamtLaenge l_"])
1.91 + ],
1.92 + {rew_ord'="tless_true", rls'= e_rls, calc = [],
1.93 + srls = append_rls "srls_..Berechnung-erstSymbolisch" e_rls
1.94 + [Calc ("Atools.boollist2sum",
1.95 + eval_boollist2sum "")],
1.96 + prls = e_rls, crls =e_rls , nrls = norm_Rational},
1.97 +"Script RechnenSymbolScript (k_::bool) (q__::bool) " ^
1.98 +"(u_::bool list) (s_::bool list) (o_::bool list) (l_::real) =" ^
1.99 +" (let t_ = Take (l_ = oben + senkrecht + unten); " ^
1.100 +" sum_ = boollist2sum o_; " ^
1.101 +" t_ = Substitute [oben = sum_] t_; " ^
1.102 +" t_ = Substitute o_ t_; " ^
1.103 +" t_ = Substitute [k_, q__] t_; " ^
1.104 +" t_ = (Repeat (Try (Rewrite_Set norm_Poly False))) t_; " ^
1.105 +" sum_ = boollist2sum s_; " ^
1.106 +" t_ = Substitute [senkrecht = sum_] t_; " ^
1.107 +" t_ = Substitute s_ t_; " ^
1.108 +" t_ = Substitute [k_, q__] t_; " ^
1.109 +" t_ = (Repeat (Try (Rewrite_Set norm_Poly False))) t_; " ^
1.110 +" sum_ = boollist2sum u_; " ^
1.111 +" t_ = Substitute [unten = sum_] t_; " ^
1.112 +" t_ = Substitute u_ t_; " ^
1.113 +" t_ = Substitute [k_, q__] t_; " ^
1.114 +" t_ = (Repeat (Try (Rewrite_Set norm_Poly False))) t_ " ^
1.115 +" in (Try (Rewrite_Set norm_Poly False)) t_) "
1.116 +));
1.117 +
1.118 +store_met
1.119 + (prep_met (theory "AlgEin") "met_algein_symnum" [] e_metID
1.120 + (["Berechnung","erstSymbolisch"],
1.121 + [("#Given" ,["KantenLaenge k_","Querschnitt q__",
1.122 + "KantenUnten u_", "KantenSenkrecht s_",
1.123 + "KantenOben o_"]),
1.124 + ("#Find" ,["GesamtLaenge l_"])
1.125 + ],
1.126 + {rew_ord'="tless_true", rls'= e_rls, calc = [],
1.127 + srls = append_rls "srls_..Berechnung-erstSymbolisch" e_rls
1.128 + [Calc ("Atools.boollist2sum",
1.129 + eval_boollist2sum "")],
1.130 + prls = e_rls,
1.131 + crls =e_rls , nrls = norm_Rational},
1.132 +"Script RechnenSymbolScript (k_::bool) (q__::bool) " ^
1.133 +"(u_::bool list) (s_::bool list) (o_::bool list) (l_::real) =" ^
1.134 +" (let t_ = Take (l_ = oben + senkrecht + unten); " ^
1.135 +" sum_ = boollist2sum o_; " ^
1.136 +" t_ = Substitute [oben = sum_] t_; " ^
1.137 +" t_ = Substitute o_ t_; " ^
1.138 +" t_ = (Repeat (Try (Rewrite_Set norm_Poly False))) t_; " ^
1.139 +" sum_ = boollist2sum s_; " ^
1.140 +" t_ = Substitute [senkrecht = sum_] t_; " ^
1.141 +" t_ = Substitute s_ t_; " ^
1.142 +" t_ = (Repeat (Try (Rewrite_Set norm_Poly False))) t_; " ^
1.143 +" sum_ = boollist2sum u_; " ^
1.144 +" t_ = Substitute [unten = sum_] t_; " ^
1.145 +" t_ = Substitute u_ t_; " ^
1.146 +" t_ = (Repeat (Try (Rewrite_Set norm_Poly False))) t_; " ^
1.147 +" t_ = Substitute [k_, q__] t_ " ^
1.148 +" in (Try (Rewrite_Set norm_Poly False)) t_) "
1.149 +));
1.150 +*}
1.151
1.152 end