1.1 --- a/src/Tools/isac/IsacKnowledge/AlgEin.ML Wed Aug 25 15:15:01 2010 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,141 +0,0 @@
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"IsacKnowledge/AlgEin.ML";
1.9 -use"AlgEin.ML";
1.10 -
1.11 -remove_thy"Typefix";
1.12 -remove_thy"AlgEin";
1.13 -use_thy"IsacKnowledge/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"IsacKnowledge/AlgEin.ML";
1.144 - *)
1.145 \ No newline at end of file