1 (* Algebra Einf"uhrung, Unterrichtsversuch IMST-Projekt
2 author: Walther Neuper 2007
3 (c) due to copyright terms
6 theory AlgEin imports Rational begin
7 (*Poly + ..shouldbe sufficient, but norm_Poly required*)
11 (*new Descriptions in the related problems*)
12 KantenUnten :: "bool list => una"
13 KantenSenkrecht :: "bool list => una"
14 KantenOben :: "bool list => una"
15 KantenLaenge :: "bool => una"
16 Querschnitt :: "bool => una"
17 GesamtLaenge :: "real => una"
20 RechnenSymbolScript :: "[bool,bool,bool list,bool list,bool list,real,
22 ("((Script RechnenSymbolScript (_ _ _ _ _ _ =))// (_))" 9)
28 setup {* KEStore_Elems.add_pbts
29 [(Specify.prep_pbt thy "pbl_algein" [] e_pblID (["Berechnung"], [], e_rls, NONE, [])),
30 (Specify.prep_pbt thy "pbl_algein_numsym" [] e_pblID
31 (["numerischSymbolische", "Berechnung"],
33 ["KantenLaenge k_k","Querschnitt q__q"(*q_ in Biegelinie.thy*), "KantenUnten u_u",
34 "KantenSenkrecht s_s", "KantenOben o_o"]),
35 ("#Find", ["GesamtLaenge l_l"])],
36 e_rls, NONE, [["Berechnung","erstNumerisch"], ["Berechnung","erstSymbolisch"]]))]; *}
38 setup {* KEStore_Elems.add_mets
39 [Specify.prep_met thy "met_algein" [] e_metID
41 {rew_ord'="tless_true", rls'= Erls, calc = [], srls = Erls, prls = Erls, crls =Erls,
42 errpats = [], nrls = Erls},
44 Specify.prep_met thy "met_algein_numsym" [] e_metID
45 (["Berechnung","erstNumerisch"], [],
46 {rew_ord'="tless_true", rls'= Erls, calc = [], srls = Erls, prls = Erls, crls =Erls,
47 errpats = [], nrls = Erls},
49 Specify.prep_met thy "met_algein_numsym" [] e_metID
50 (["Berechnung","erstNumerisch"],
51 [("#Given" ,["KantenLaenge k_k","Querschnitt q__q", "KantenUnten u_u",
52 "KantenSenkrecht s_s", "KantenOben o_o"]),
53 ("#Find" ,["GesamtLaenge l_l"])],
54 {rew_ord'="tless_true", rls'= e_rls, calc = [],
55 srls = append_rls "srls_..Berechnung-erstSymbolisch" e_rls
56 [Calc ("Atools.boollist2sum", eval_boollist2sum "")],
57 prls = e_rls, crls =e_rls , errpats = [], nrls = norm_Rational},
58 "Script RechnenSymbolScript (k_k::bool) (q__q::bool) " ^
59 "(u_u::bool list) (s_s::bool list) (o_o::bool list) (l_l::real) =" ^
60 " (let t_t = Take (l_l = oben + senkrecht + unten); " ^
61 " su_m = boollist2sum o_o; " ^
62 " t_t = Substitute [oben = su_m] t_t; " ^
63 " t_t = Substitute o_o t_t; " ^
64 " t_t = Substitute [k_k, q__q] t_t; " ^
65 " t_t = (Repeat (Try (Rewrite_Set norm_Poly False))) t_t; " ^
66 " su_m = boollist2sum s_s; " ^
67 " t_t = Substitute [senkrecht = su_m] t_t; " ^
68 " t_t = Substitute s_s t_t; " ^
69 " t_t = Substitute [k_k, q__q] t_t; " ^
70 " t_t = (Repeat (Try (Rewrite_Set norm_Poly False))) t_t; " ^
71 " su_m = boollist2sum u_u; " ^
72 " t_t = Substitute [unten = su_m] t_t; " ^
73 " t_t = Substitute u_u t_t; " ^
74 " t_t = Substitute [k_k, q__q] t_t; " ^
75 " t_t = (Repeat (Try (Rewrite_Set norm_Poly False))) t_t " ^
76 " in (Try (Rewrite_Set norm_Poly False)) t_t) "),
77 Specify.prep_met thy "met_algein_symnum" [] e_metID
78 (["Berechnung","erstSymbolisch"],
79 [("#Given" ,["KantenLaenge k_k","Querschnitt q__q", "KantenUnten u_u",
80 "KantenSenkrecht s_s", "KantenOben o_o"]),
81 ("#Find" ,["GesamtLaenge l_l"])],
82 {rew_ord'="tless_true", rls'= e_rls, calc = [],
83 srls = append_rls "srls_..Berechnung-erstSymbolisch" e_rls
84 [Calc ("Atools.boollist2sum", eval_boollist2sum "")],
85 prls = e_rls, crls =e_rls , errpats = [], nrls = norm_Rational},
86 "Script RechnenSymbolScript (k_k::bool) (q__q::bool) " ^
87 "(u_u::bool list) (s_s::bool list) (o_o::bool list) (l_l::real) =" ^
88 " (let t_t = Take (l_l = oben + senkrecht + unten); " ^
89 " su_m = boollist2sum o_o; " ^
90 " t_t = Substitute [oben = su_m] t_t; " ^
91 " t_t = Substitute o_o t_t; " ^
92 " t_t = (Repeat (Try (Rewrite_Set norm_Poly False))) t_t; " ^
93 " su_m = boollist2sum s_s; " ^
94 " t_t = Substitute [senkrecht = su_m] t_t; " ^
95 " t_t = Substitute s_s t_t; " ^
96 " t_t = (Repeat (Try (Rewrite_Set norm_Poly False))) t_t; " ^
97 " su_m = boollist2sum u_u; " ^
98 " t_t = Substitute [unten = su_m] t_t; " ^
99 " t_t = Substitute u_u t_t; " ^
100 " t_t = (Repeat (Try (Rewrite_Set norm_Poly False))) t_t; " ^
101 " t_t = Substitute [k_k, q__q] t_t " ^
102 " in (Try (Rewrite_Set norm_Poly False)) t_t) ")]