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"
23 RechnenSymbolScript :: "[bool,bool,bool list,bool list,bool list,real,
25 ("((Script RechnenSymbolScript (_ _ _ _ _ _ =))// (_))" 9)
31 setup \<open>KEStore_Elems.add_pbts
32 [(Specify.prep_pbt thy "pbl_algein" [] Celem.e_pblID (["Berechnung"], [], Rule.e_rls, NONE, [])),
33 (Specify.prep_pbt thy "pbl_algein_numsym" [] Celem.e_pblID
34 (["numerischSymbolische", "Berechnung"],
36 ["KantenLaenge k_k","Querschnitt q__q"(*q_ in Biegelinie.thy*), "KantenUnten u_u",
37 "KantenSenkrecht s_s", "KantenOben o_o"]),
38 ("#Find", ["GesamtLaenge l_l"])],
39 Rule.e_rls, NONE, [["Berechnung","erstNumerisch"], ["Berechnung","erstSymbolisch"]]))];\<close>
41 setup \<open>KEStore_Elems.add_mets
42 [Specify.prep_met thy "met_algein" [] Celem.e_metID
44 {rew_ord'="tless_true", rls'= Rule.Erls, calc = [], srls = Rule.Erls, prls = Rule.Erls, crls =Rule.Erls,
45 errpats = [], nrls = Rule.Erls},
47 Specify.prep_met thy "met_algein_numsym" [] Celem.e_metID
48 (["Berechnung","erstNumerisch"], [],
49 {rew_ord'="tless_true", rls'= Rule.Erls, calc = [], srls = Rule.Erls, prls = Rule.Erls, crls =Rule.Erls,
50 errpats = [], nrls = Rule.Erls},
54 partial_function (tailrec) symbolisch_rechnen :: "bool \<Rightarrow> bool \<Rightarrow> bool list \<Rightarrow> bool list \<Rightarrow> bool list \<Rightarrow> real \<Rightarrow> bool"
56 "symbolisch_rechnen k_k q__q u_u s_s o_o l_l =
57 (let t_t = Take (l_l = oben + senkrecht + unten);
58 su_m = boollist2sum o_o;
59 t_t = Substitute [oben = su_m] t_t; \<comment> \<open>PROG consts\<close>
60 t_t = Substitute o_o t_t;
61 t_t = Substitute [k_k, q__q] t_t;
62 t_t = Repeat (Try (Rewrite_Set ''norm_Poly'' False)) t_t;
63 su_m = boollist2sum s_s;
64 t_t = Substitute [senkrecht = su_m] t_t; \<comment> \<open>PROG consts\<close>
65 t_t = Substitute s_s t_t;
66 t_t = Substitute [k_k, q__q] t_t;
67 t_t = Repeat (Try (Rewrite_Set ''norm_Poly'' False)) t_t;
68 su_m = boollist2sum u_u;
69 t_t = Substitute [unten = su_m] t_t; \<comment> \<open>PROG consts\<close>
70 t_t = Substitute u_u t_t;
71 t_t = Substitute [k_k, q__q] t_t;
72 t_t = Repeat (Try (Rewrite_Set ''norm_Poly'' False)) t_t
73 in Try (Rewrite_Set ''norm_Poly'' False) t_t)"
74 setup \<open>KEStore_Elems.add_mets
75 [Specify.prep_met thy "met_algein_numsym_1num" [] Celem.e_metID
76 (["Berechnung","erstNumerisch"],
77 [("#Given" ,["KantenLaenge k_k","Querschnitt q__q", "KantenUnten u_u",
78 "KantenSenkrecht s_s", "KantenOben o_o"]),
79 ("#Find" ,["GesamtLaenge l_l"])],
80 {rew_ord'="tless_true", rls'= Rule.e_rls, calc = [],
81 srls = Rule.append_rls "srls_..Berechnung-erstSymbolisch" Rule.e_rls
82 [Rule.Calc ("Atools.boollist2sum", eval_boollist2sum "")],
83 prls = Rule.e_rls, crls =Rule.e_rls , errpats = [], nrls = norm_Rational},
84 @{thm symbolisch_rechnen.simps}
85 (*"Script RechnenSymbolScript (k_k::bool) (q__q::bool) " ^
86 "(u_u::bool list) (s_s::bool list) (o_o::bool list) (l_l::real) =" ^
87 " (let t_t = Take (l_l = oben + senkrecht + unten); " ^
88 " su_m = boollist2sum o_o; " ^
89 " t_t = Substitute [oben = su_m] t_t; " ^
90 " t_t = Substitute o_o t_t; " ^
91 " t_t = Substitute [k_k, q__q] 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 = Substitute [k_k, q__q] t_t; " ^
97 " t_t = (Repeat (Try (Rewrite_Set ''norm_Poly'' False))) t_t; " ^
98 " su_m = boollist2sum u_u; " ^
99 " t_t = Substitute [unten = su_m] t_t; " ^
100 " t_t = Substitute u_u t_t; " ^
101 " t_t = Substitute [k_k, q__q] t_t; " ^
102 " t_t = (Repeat (Try (Rewrite_Set ''norm_Poly'' False))) t_t " ^
103 " in (Try (Rewrite_Set ''norm_Poly'' False)) t_t) "*))]
106 partial_function (tailrec) symbolisch_rechnen_2 :: "bool \<Rightarrow> bool \<Rightarrow> bool list \<Rightarrow> bool list \<Rightarrow> bool list \<Rightarrow> real \<Rightarrow> bool"
108 "symbolisch_rechnen (k_k::bool) (q__q::bool)
109 (u_u::bool list) (s_s::bool list) (o_o::bool list) (l_l::real) =
110 (let t_t = Take (l_l = oben + senkrecht + unten);
111 su_m = boollist2sum o_o;
112 t_t = Substitute [oben = su_m] t_t; \<comment> \<open>PROG consts\<close>
113 t_t = Substitute o_o t_t;
114 t_t = Repeat (Try (Rewrite_Set ''norm_Poly'' False)) t_t;
115 su_m = boollist2sum s_s;
116 t_t = Substitute [senkrecht = su_m] t_t; \<comment> \<open>PROG consts\<close>
117 t_t = Substitute s_s t_t;
118 t_t = Repeat (Try (Rewrite_Set ''norm_Poly'' False)) t_t;
119 su_m = boollist2sum u_u;
120 t_t = Substitute [unten = su_m] t_t; \<comment> \<open>PROG consts\<close>
121 t_t = Substitute u_u t_t;
122 t_t = Repeat (Try (Rewrite_Set ''norm_Poly'' False)) t_t;
123 t_t = Substitute [k_k, q__q] t_t
124 in (Try (Rewrite_Set ''norm_Poly'' False)) t_t)"
125 setup \<open>KEStore_Elems.add_mets
126 [Specify.prep_met thy "met_algein_symnum" [] Celem.e_metID
127 (["Berechnung","erstSymbolisch"],
128 [("#Given" ,["KantenLaenge k_k","Querschnitt q__q", "KantenUnten u_u",
129 "KantenSenkrecht s_s", "KantenOben o_o"]),
130 ("#Find" ,["GesamtLaenge l_l"])],
131 {rew_ord'="tless_true", rls'= Rule.e_rls, calc = [],
132 srls = Rule.append_rls "srls_..Berechnung-erstSymbolisch" Rule.e_rls
133 [Rule.Calc ("Atools.boollist2sum", eval_boollist2sum "")],
134 prls = Rule.e_rls, crls =Rule.e_rls , errpats = [], nrls = norm_Rational},
135 @{thm symbolisch_rechnen.simps}
136 (*"Script RechnenSymbolScript (k_k::bool) (q__q::bool) " ^
137 "(u_u::bool list) (s_s::bool list) (o_o::bool list) (l_l::real) =" ^
138 " (let t_t = Take (l_l = oben + senkrecht + unten); " ^
139 " su_m = boollist2sum o_o; " ^
140 " t_t = Substitute [oben = su_m] t_t; " ^
141 " t_t = Substitute o_o t_t; " ^
142 " t_t = (Repeat (Try (Rewrite_Set ''norm_Poly'' False))) t_t; " ^
143 " su_m = boollist2sum s_s; " ^
144 " t_t = Substitute [senkrecht = su_m] t_t; " ^
145 " t_t = Substitute s_s t_t; " ^
146 " t_t = (Repeat (Try (Rewrite_Set ''norm_Poly'' False))) t_t; " ^
147 " su_m = boollist2sum u_u; " ^
148 " t_t = Substitute [unten = su_m] t_t; " ^
149 " t_t = Substitute u_u t_t; " ^
150 " t_t = (Repeat (Try (Rewrite_Set ''norm_Poly'' False))) t_t; " ^
151 " t_t = Substitute [k_k, q__q] t_t " ^
152 " in (Try (Rewrite_Set ''norm_Poly'' False)) t_t) "*))]