24 ML {* |
24 ML {* |
25 val thy = @{theory}; |
25 val thy = @{theory}; |
26 *} |
26 *} |
27 (** problems **) |
27 (** problems **) |
28 setup {* KEStore_Elems.add_pbts |
28 setup {* KEStore_Elems.add_pbts |
29 [(Specify.prep_pbt thy "pbl_algein" [] e_pblID (["Berechnung"], [], e_rls, NONE, [])), |
29 [(Specify.prep_pbt thy "pbl_algein" [] Celem.e_pblID (["Berechnung"], [], Celem.e_rls, NONE, [])), |
30 (Specify.prep_pbt thy "pbl_algein_numsym" [] e_pblID |
30 (Specify.prep_pbt thy "pbl_algein_numsym" [] Celem.e_pblID |
31 (["numerischSymbolische", "Berechnung"], |
31 (["numerischSymbolische", "Berechnung"], |
32 [("#Given", |
32 [("#Given", |
33 ["KantenLaenge k_k","Querschnitt q__q"(*q_ in Biegelinie.thy*), "KantenUnten u_u", |
33 ["KantenLaenge k_k","Querschnitt q__q"(*q_ in Biegelinie.thy*), "KantenUnten u_u", |
34 "KantenSenkrecht s_s", "KantenOben o_o"]), |
34 "KantenSenkrecht s_s", "KantenOben o_o"]), |
35 ("#Find", ["GesamtLaenge l_l"])], |
35 ("#Find", ["GesamtLaenge l_l"])], |
36 e_rls, NONE, [["Berechnung","erstNumerisch"], ["Berechnung","erstSymbolisch"]]))]; *} |
36 Celem.e_rls, NONE, [["Berechnung","erstNumerisch"], ["Berechnung","erstSymbolisch"]]))]; *} |
37 |
37 |
38 setup {* KEStore_Elems.add_mets |
38 setup {* KEStore_Elems.add_mets |
39 [Specify.prep_met thy "met_algein" [] e_metID |
39 [Specify.prep_met thy "met_algein" [] Celem.e_metID |
40 (["Berechnung"], [], |
40 (["Berechnung"], [], |
41 {rew_ord'="tless_true", rls'= Erls, calc = [], srls = Erls, prls = Erls, crls =Erls, |
41 {rew_ord'="tless_true", rls'= Celem.Erls, calc = [], srls = Celem.Erls, prls = Celem.Erls, crls =Celem.Erls, |
42 errpats = [], nrls = Erls}, |
42 errpats = [], nrls = Celem.Erls}, |
43 "empty_script"), |
43 "empty_script"), |
44 Specify.prep_met thy "met_algein_numsym" [] e_metID |
44 Specify.prep_met thy "met_algein_numsym" [] Celem.e_metID |
45 (["Berechnung","erstNumerisch"], [], |
45 (["Berechnung","erstNumerisch"], [], |
46 {rew_ord'="tless_true", rls'= Erls, calc = [], srls = Erls, prls = Erls, crls =Erls, |
46 {rew_ord'="tless_true", rls'= Celem.Erls, calc = [], srls = Celem.Erls, prls = Celem.Erls, crls =Celem.Erls, |
47 errpats = [], nrls = Erls}, |
47 errpats = [], nrls = Celem.Erls}, |
48 "empty_script"), |
48 "empty_script"), |
49 Specify.prep_met thy "met_algein_numsym" [] e_metID |
49 Specify.prep_met thy "met_algein_numsym" [] Celem.e_metID |
50 (["Berechnung","erstNumerisch"], |
50 (["Berechnung","erstNumerisch"], |
51 [("#Given" ,["KantenLaenge k_k","Querschnitt q__q", "KantenUnten u_u", |
51 [("#Given" ,["KantenLaenge k_k","Querschnitt q__q", "KantenUnten u_u", |
52 "KantenSenkrecht s_s", "KantenOben o_o"]), |
52 "KantenSenkrecht s_s", "KantenOben o_o"]), |
53 ("#Find" ,["GesamtLaenge l_l"])], |
53 ("#Find" ,["GesamtLaenge l_l"])], |
54 {rew_ord'="tless_true", rls'= e_rls, calc = [], |
54 {rew_ord'="tless_true", rls'= Celem.e_rls, calc = [], |
55 srls = append_rls "srls_..Berechnung-erstSymbolisch" e_rls |
55 srls = Celem.append_rls "srls_..Berechnung-erstSymbolisch" Celem.e_rls |
56 [Calc ("Atools.boollist2sum", eval_boollist2sum "")], |
56 [Celem.Calc ("Atools.boollist2sum", eval_boollist2sum "")], |
57 prls = e_rls, crls =e_rls , errpats = [], nrls = norm_Rational}, |
57 prls = Celem.e_rls, crls =Celem.e_rls , errpats = [], nrls = norm_Rational}, |
58 "Script RechnenSymbolScript (k_k::bool) (q__q::bool) " ^ |
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) =" ^ |
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); " ^ |
60 " (let t_t = Take (l_l = oben + senkrecht + unten); " ^ |
61 " su_m = boollist2sum o_o; " ^ |
61 " su_m = boollist2sum o_o; " ^ |
62 " t_t = Substitute [oben = su_m] t_t; " ^ |
62 " t_t = Substitute [oben = su_m] t_t; " ^ |
72 " t_t = Substitute [unten = su_m] t_t; " ^ |
72 " t_t = Substitute [unten = su_m] t_t; " ^ |
73 " t_t = Substitute u_u t_t; " ^ |
73 " t_t = Substitute u_u t_t; " ^ |
74 " t_t = Substitute [k_k, q__q] t_t; " ^ |
74 " t_t = Substitute [k_k, q__q] t_t; " ^ |
75 " t_t = (Repeat (Try (Rewrite_Set norm_Poly False))) t_t " ^ |
75 " t_t = (Repeat (Try (Rewrite_Set norm_Poly False))) t_t " ^ |
76 " in (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 |
77 Specify.prep_met thy "met_algein_symnum" [] Celem.e_metID |
78 (["Berechnung","erstSymbolisch"], |
78 (["Berechnung","erstSymbolisch"], |
79 [("#Given" ,["KantenLaenge k_k","Querschnitt q__q", "KantenUnten u_u", |
79 [("#Given" ,["KantenLaenge k_k","Querschnitt q__q", "KantenUnten u_u", |
80 "KantenSenkrecht s_s", "KantenOben o_o"]), |
80 "KantenSenkrecht s_s", "KantenOben o_o"]), |
81 ("#Find" ,["GesamtLaenge l_l"])], |
81 ("#Find" ,["GesamtLaenge l_l"])], |
82 {rew_ord'="tless_true", rls'= e_rls, calc = [], |
82 {rew_ord'="tless_true", rls'= Celem.e_rls, calc = [], |
83 srls = append_rls "srls_..Berechnung-erstSymbolisch" e_rls |
83 srls = Celem.append_rls "srls_..Berechnung-erstSymbolisch" Celem.e_rls |
84 [Calc ("Atools.boollist2sum", eval_boollist2sum "")], |
84 [Celem.Calc ("Atools.boollist2sum", eval_boollist2sum "")], |
85 prls = e_rls, crls =e_rls , errpats = [], nrls = norm_Rational}, |
85 prls = Celem.e_rls, crls =Celem.e_rls , errpats = [], nrls = norm_Rational}, |
86 "Script RechnenSymbolScript (k_k::bool) (q__q::bool) " ^ |
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) =" ^ |
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); " ^ |
88 " (let t_t = Take (l_l = oben + senkrecht + unten); " ^ |
89 " su_m = boollist2sum o_o; " ^ |
89 " su_m = boollist2sum o_o; " ^ |
90 " t_t = Substitute [oben = su_m] t_t; " ^ |
90 " t_t = Substitute [oben = su_m] t_t; " ^ |