1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/Tools/isac/Knowledge/AlgEin.ML Wed Aug 25 16:20:07 2010 +0200
1.3 @@ -0,0 +1,141 @@
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 +use"Knowledge/AlgEin.ML";
1.9 +use"AlgEin.ML";
1.10 +
1.11 +remove_thy"Typefix";
1.12 +remove_thy"AlgEin";
1.13 +use_thy"Knowledge/Isac";
1.14 +*)
1.15 +
1.16 +(** interface isabelle -- isac **)
1.17 +
1.18 +theory' := overwritel (!theory', [("AlgEin.thy",AlgEin.thy)]);
1.19 +
1.20 +(** problems **)
1.21 +
1.22 +store_pbt
1.23 + (prep_pbt AlgEin.thy "pbl_algein" [] e_pblID
1.24 + (["Berechnung"], [], e_rls, NONE,
1.25 + []));
1.26 +(* WN070405
1.27 +store_pbt
1.28 + (prep_pbt AlgEin.thy "pbl_algein_num" [] e_pblID
1.29 + (["numerische", "Berechnung"],
1.30 + [("#Given" ,["KantenUnten u_", "KantenSenkrecht s_", "KantenOben o_"]),
1.31 + ("#Find" ,["GesamtLaenge l_"])
1.32 + ],
1.33 + append_rls "e_rls" e_rls [],
1.34 + NONE,
1.35 + []));
1.36 +*)
1.37 +store_pbt
1.38 + (prep_pbt AlgEin.thy "pbl_algein_numsym" [] e_pblID
1.39 + (["numerischSymbolische", "Berechnung"],
1.40 + [("#Given" ,["KantenLaenge k_","Querschnitt q__"(*q_ in Biegelinie.thy*),
1.41 + "KantenUnten u_", "KantenSenkrecht s_", "KantenOben o_"]),
1.42 + ("#Find" ,["GesamtLaenge l_"])
1.43 + ],
1.44 + e_rls,
1.45 + NONE,
1.46 + [["Berechnung","erstNumerisch"],["Berechnung","erstSymbolisch"]]));
1.47 +
1.48 +(* show_ptyps();
1.49 + *)
1.50 +
1.51 +
1.52 +(** methods **)
1.53 +
1.54 +store_met
1.55 + (prep_met AlgEin.thy "met_algein" [] e_metID
1.56 + (["Berechnung"],
1.57 + [],
1.58 + {rew_ord'="tless_true", rls'= Erls, calc = [],
1.59 + srls = Erls, prls = Erls,
1.60 + crls =Erls , nrls = Erls},
1.61 +"empty_script"
1.62 +));
1.63 +
1.64 +store_met
1.65 + (prep_met AlgEin.thy "met_algein_numsym" [] e_metID
1.66 + (["Berechnung","erstNumerisch"],
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 AlgEin.thy "met_algein_numsym" [] e_metID
1.76 + (["Berechnung","erstNumerisch"],
1.77 + [("#Given" ,["KantenLaenge k_","Querschnitt q__",
1.78 + "KantenUnten u_", "KantenSenkrecht s_",
1.79 + "KantenOben o_"]),
1.80 + ("#Find" ,["GesamtLaenge l_"])
1.81 + ],
1.82 + {rew_ord'="tless_true", rls'= e_rls, calc = [],
1.83 + srls = append_rls "srls_..Berechnung-erstSymbolisch" e_rls
1.84 + [Calc ("Atools.boollist2sum",
1.85 + eval_boollist2sum "")],
1.86 + prls = e_rls, crls =e_rls , nrls = norm_Rational},
1.87 +"Script RechnenSymbolScript (k_::bool) (q__::bool) \
1.88 +\(u_::bool list) (s_::bool list) (o_::bool list) (l_::real) =\
1.89 +\ (let t_ = Take (l_ = oben + senkrecht + unten); \
1.90 +\ sum_ = boollist2sum o_;\
1.91 +\ t_ = Substitute [oben = sum_] t_;\
1.92 +\ t_ = Substitute o_ t_;\
1.93 +\ t_ = Substitute [k_, q__] t_;\
1.94 +\ t_ = (Repeat (Try (Rewrite_Set norm_Poly False))) t_;\
1.95 +\ sum_ = boollist2sum s_;\
1.96 +\ t_ = Substitute [senkrecht = sum_] t_;\
1.97 +\ t_ = Substitute s_ t_;\
1.98 +\ t_ = Substitute [k_, q__] t_;\
1.99 +\ t_ = (Repeat (Try (Rewrite_Set norm_Poly False))) t_;\
1.100 +\ sum_ = boollist2sum u_;\
1.101 +\ t_ = Substitute [unten = sum_] t_;\
1.102 +\ t_ = Substitute u_ t_;\
1.103 +\ t_ = Substitute [k_, q__] t_;\
1.104 +\ t_ = (Repeat (Try (Rewrite_Set norm_Poly False))) t_\
1.105 +\ in (Try (Rewrite_Set norm_Poly False)) t_)"
1.106 +));
1.107 +
1.108 +store_met
1.109 + (prep_met AlgEin.thy "met_algein_symnum" [] e_metID
1.110 + (["Berechnung","erstSymbolisch"],
1.111 + [("#Given" ,["KantenLaenge k_","Querschnitt q__",
1.112 + "KantenUnten u_", "KantenSenkrecht s_",
1.113 + "KantenOben o_"]),
1.114 + ("#Find" ,["GesamtLaenge l_"])
1.115 + ],
1.116 + {rew_ord'="tless_true", rls'= e_rls, calc = [],
1.117 + srls = append_rls "srls_..Berechnung-erstSymbolisch" e_rls
1.118 + [Calc ("Atools.boollist2sum",
1.119 + eval_boollist2sum "")],
1.120 + prls = e_rls,
1.121 + crls =e_rls , nrls = norm_Rational},
1.122 +"Script RechnenSymbolScript (k_::bool) (q__::bool) \
1.123 +\(u_::bool list) (s_::bool list) (o_::bool list) (l_::real) =\
1.124 +\ (let t_ = Take (l_ = oben + senkrecht + unten); \
1.125 +\ sum_ = boollist2sum o_;\
1.126 +\ t_ = Substitute [oben = sum_] t_;\
1.127 +\ t_ = Substitute o_ t_;\
1.128 +\ t_ = (Repeat (Try (Rewrite_Set norm_Poly False))) t_;\
1.129 +\ sum_ = boollist2sum s_;\
1.130 +\ t_ = Substitute [senkrecht = sum_] t_;\
1.131 +\ t_ = Substitute s_ t_;\
1.132 +\ t_ = (Repeat (Try (Rewrite_Set norm_Poly False))) t_;\
1.133 +\ sum_ = boollist2sum u_;\
1.134 +\ t_ = Substitute [unten = sum_] t_;\
1.135 +\ t_ = Substitute u_ t_;\
1.136 +\ t_ = (Repeat (Try (Rewrite_Set norm_Poly False))) t_;\
1.137 +\ t_ = Substitute [k_, q__] t_\
1.138 +\ in (Try (Rewrite_Set norm_Poly False)) t_)"
1.139 +));
1.140 +
1.141 +(* show_mets();
1.142 + *)
1.143 +(* use"Knowledge/AlgEin.ML";
1.144 + *)
1.145 \ No newline at end of file