1 (* Algebra Einf"uhrung, Unterrichtsversuch IMST-Projekt |
|
2 author: Walther Neuper 2007 |
|
3 (c) due to copyright terms |
|
4 |
|
5 use"Knowledge/AlgEin.ML"; |
|
6 use"AlgEin.ML"; |
|
7 |
|
8 remove_thy"Typefix"; |
|
9 remove_thy"AlgEin"; |
|
10 use_thy"Knowledge/Isac"; |
|
11 *) |
|
12 |
|
13 (** interface isabelle -- isac **) |
|
14 |
|
15 theory' := overwritel (!theory', [("(theory "AlgEin")",(theory "AlgEin"))]); |
|
16 |
|
17 (** problems **) |
|
18 |
|
19 store_pbt |
|
20 (prep_pbt (theory "AlgEin") "pbl_algein" [] e_pblID |
|
21 (["Berechnung"], [], e_rls, NONE, |
|
22 [])); |
|
23 (* WN070405 |
|
24 store_pbt |
|
25 (prep_pbt (theory "AlgEin") "pbl_algein_num" [] e_pblID |
|
26 (["numerische", "Berechnung"], |
|
27 [("#Given" ,["KantenUnten u_", "KantenSenkrecht s_", "KantenOben o_"]), |
|
28 ("#Find" ,["GesamtLaenge l_"]) |
|
29 ], |
|
30 append_rls "e_rls" e_rls [], |
|
31 NONE, |
|
32 [])); |
|
33 *) |
|
34 store_pbt |
|
35 (prep_pbt (theory "AlgEin") "pbl_algein_numsym" [] e_pblID |
|
36 (["numerischSymbolische", "Berechnung"], |
|
37 [("#Given" ,["KantenLaenge k_","Querschnitt q__"(*q_ in Biegelinie.thy*), |
|
38 "KantenUnten u_", "KantenSenkrecht s_", "KantenOben o_"]), |
|
39 ("#Find" ,["GesamtLaenge l_"]) |
|
40 ], |
|
41 e_rls, |
|
42 NONE, |
|
43 [["Berechnung","erstNumerisch"],["Berechnung","erstSymbolisch"]])); |
|
44 |
|
45 (* show_ptyps(); |
|
46 *) |
|
47 |
|
48 |
|
49 (** methods **) |
|
50 |
|
51 store_met |
|
52 (prep_met (theory "AlgEin") "met_algein" [] e_metID |
|
53 (["Berechnung"], |
|
54 [], |
|
55 {rew_ord'="tless_true", rls'= Erls, calc = [], |
|
56 srls = Erls, prls = Erls, |
|
57 crls =Erls , nrls = Erls}, |
|
58 "empty_script" |
|
59 )); |
|
60 |
|
61 store_met |
|
62 (prep_met (theory "AlgEin") "met_algein_numsym" [] e_metID |
|
63 (["Berechnung","erstNumerisch"], |
|
64 [], |
|
65 {rew_ord'="tless_true", rls'= Erls, calc = [], |
|
66 srls = Erls, prls = Erls, |
|
67 crls =Erls , nrls = Erls}, |
|
68 "empty_script" |
|
69 )); |
|
70 |
|
71 store_met |
|
72 (prep_met (theory "AlgEin") "met_algein_numsym" [] e_metID |
|
73 (["Berechnung","erstNumerisch"], |
|
74 [("#Given" ,["KantenLaenge k_","Querschnitt q__", |
|
75 "KantenUnten u_", "KantenSenkrecht s_", |
|
76 "KantenOben o_"]), |
|
77 ("#Find" ,["GesamtLaenge l_"]) |
|
78 ], |
|
79 {rew_ord'="tless_true", rls'= e_rls, calc = [], |
|
80 srls = append_rls "srls_..Berechnung-erstSymbolisch" e_rls |
|
81 [Calc ("Atools.boollist2sum", |
|
82 eval_boollist2sum "")], |
|
83 prls = e_rls, crls =e_rls , nrls = norm_Rational}, |
|
84 "Script RechnenSymbolScript (k_::bool) (q__::bool) " ^ |
|
85 "(u_::bool list) (s_::bool list) (o_::bool list) (l_::real) =" ^ |
|
86 " (let t_ = Take (l_ = oben + senkrecht + unten); " ^ |
|
87 " sum_ = boollist2sum o_; " ^ |
|
88 " t_ = Substitute [oben = sum_] t_; " ^ |
|
89 " t_ = Substitute o_ t_; " ^ |
|
90 " t_ = Substitute [k_, q__] t_; " ^ |
|
91 " t_ = (Repeat (Try (Rewrite_Set norm_Poly False))) t_; " ^ |
|
92 " sum_ = boollist2sum s_; " ^ |
|
93 " t_ = Substitute [senkrecht = sum_] t_; " ^ |
|
94 " t_ = Substitute s_ t_; " ^ |
|
95 " t_ = Substitute [k_, q__] t_; " ^ |
|
96 " t_ = (Repeat (Try (Rewrite_Set norm_Poly False))) t_; " ^ |
|
97 " sum_ = boollist2sum u_; " ^ |
|
98 " t_ = Substitute [unten = sum_] t_; " ^ |
|
99 " t_ = Substitute u_ t_; " ^ |
|
100 " t_ = Substitute [k_, q__] t_; " ^ |
|
101 " t_ = (Repeat (Try (Rewrite_Set norm_Poly False))) t_ " ^ |
|
102 " in (Try (Rewrite_Set norm_Poly False)) t_) " |
|
103 )); |
|
104 |
|
105 store_met |
|
106 (prep_met (theory "AlgEin") "met_algein_symnum" [] e_metID |
|
107 (["Berechnung","erstSymbolisch"], |
|
108 [("#Given" ,["KantenLaenge k_","Querschnitt q__", |
|
109 "KantenUnten u_", "KantenSenkrecht s_", |
|
110 "KantenOben o_"]), |
|
111 ("#Find" ,["GesamtLaenge l_"]) |
|
112 ], |
|
113 {rew_ord'="tless_true", rls'= e_rls, calc = [], |
|
114 srls = append_rls "srls_..Berechnung-erstSymbolisch" e_rls |
|
115 [Calc ("Atools.boollist2sum", |
|
116 eval_boollist2sum "")], |
|
117 prls = e_rls, |
|
118 crls =e_rls , nrls = norm_Rational}, |
|
119 "Script RechnenSymbolScript (k_::bool) (q__::bool) " ^ |
|
120 "(u_::bool list) (s_::bool list) (o_::bool list) (l_::real) =" ^ |
|
121 " (let t_ = Take (l_ = oben + senkrecht + unten); " ^ |
|
122 " sum_ = boollist2sum o_; " ^ |
|
123 " t_ = Substitute [oben = sum_] t_; " ^ |
|
124 " t_ = Substitute o_ t_; " ^ |
|
125 " t_ = (Repeat (Try (Rewrite_Set norm_Poly False))) t_; " ^ |
|
126 " sum_ = boollist2sum s_; " ^ |
|
127 " t_ = Substitute [senkrecht = sum_] t_; " ^ |
|
128 " t_ = Substitute s_ t_; " ^ |
|
129 " t_ = (Repeat (Try (Rewrite_Set norm_Poly False))) t_; " ^ |
|
130 " sum_ = boollist2sum u_; " ^ |
|
131 " t_ = Substitute [unten = sum_] t_; " ^ |
|
132 " t_ = Substitute u_ t_; " ^ |
|
133 " t_ = (Repeat (Try (Rewrite_Set norm_Poly False))) t_; " ^ |
|
134 " t_ = Substitute [k_, q__] t_ " ^ |
|
135 " in (Try (Rewrite_Set norm_Poly False)) t_) " |
|
136 )); |
|
137 |
|
138 (* show_mets(); |
|
139 *) |
|