|
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', [("AlgEin.thy",AlgEin.thy)]); |
|
16 |
|
17 (** problems **) |
|
18 |
|
19 store_pbt |
|
20 (prep_pbt AlgEin.thy "pbl_algein" [] e_pblID |
|
21 (["Berechnung"], [], e_rls, NONE, |
|
22 [])); |
|
23 (* WN070405 |
|
24 store_pbt |
|
25 (prep_pbt AlgEin.thy "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 AlgEin.thy "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 AlgEin.thy "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 AlgEin.thy "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 AlgEin.thy "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 AlgEin.thy "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 *) |
|
140 (* use"Knowledge/AlgEin.ML"; |
|
141 *) |