neuper@37906
|
1 |
(* tests on AlgEin, Algebra Einf"uhrung, , Unterrichtsversuch IMST-Projekt
|
neuper@37906
|
2 |
author: Walther Neuper 2007
|
neuper@37906
|
3 |
(c) due to copyright terms
|
neuper@37906
|
4 |
|
neuper@37906
|
5 |
use"../smltest/IsacKnowledge/algein.sml";
|
neuper@37906
|
6 |
use"algein.sml";
|
neuper@37906
|
7 |
*)
|
neuper@37906
|
8 |
val thy = AlgEin.thy;
|
neuper@37906
|
9 |
|
neuper@37906
|
10 |
"-----------------------------------------------------------------";
|
neuper@37906
|
11 |
"table of contents -----------------------------------------------";
|
neuper@37906
|
12 |
"-----------------------------------------------------------------";
|
neuper@37906
|
13 |
"----------- build method 'Berechnung' 'erstSymbolisch' ----------";
|
neuper@37906
|
14 |
"----------- me 'Berechnung' 'erstNumerisch' ---------------------";
|
neuper@37906
|
15 |
"----------- auto 'Berechnung' 'erstSymbolisch' ------------------";
|
neuper@37906
|
16 |
"----------- Widerspruch 3 = 777 ---------------------------------";
|
neuper@37906
|
17 |
"-----------------------------------------------------------------";
|
neuper@37906
|
18 |
"-----------------------------------------------------------------";
|
neuper@37906
|
19 |
"-----------------------------------------------------------------";
|
neuper@37906
|
20 |
|
neuper@37906
|
21 |
|
neuper@37906
|
22 |
|
neuper@37906
|
23 |
(* use"../smltest/IsacKnowledge/algein.sml";
|
neuper@37906
|
24 |
*)
|
neuper@37906
|
25 |
|
neuper@37906
|
26 |
"----------- build method 'Berechnung' 'erstSymbolisch' ----------";
|
neuper@37906
|
27 |
"----------- build method 'Berechnung' 'erstSymbolisch' ----------";
|
neuper@37906
|
28 |
"----------- build method 'Berechnung' 'erstSymbolisch' ----------";
|
neuper@37906
|
29 |
val str =
|
neuper@37906
|
30 |
"Script RechnenSymbolScript (k_::bool) (q__::bool) \
|
neuper@37906
|
31 |
\(u_::bool list) (s_::bool list) (o_::bool list) (l_::real) =\
|
neuper@37906
|
32 |
\ (let t_ = (l_ = 1)\
|
neuper@37906
|
33 |
\ in t_)"
|
neuper@37906
|
34 |
;
|
neuper@37906
|
35 |
val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
|
neuper@37906
|
36 |
(*---^^^-OK-----------------------------------------------------------------*)
|
neuper@37906
|
37 |
val str =
|
neuper@37906
|
38 |
"Script RechnenSymbolScript (k_::bool) (q__::bool) \
|
neuper@37906
|
39 |
\(u_::bool list) (s_::bool list) (o_::bool list) (l_::real) =\
|
neuper@37906
|
40 |
\ (let t_ = Take (l_ = Oben + Senkrecht + Unten); \
|
neuper@37906
|
41 |
\ sum_ = boollist2sum o_;\
|
neuper@37906
|
42 |
\ t_ = Substitute [Oben = sum_] t_;\
|
neuper@37906
|
43 |
\ t_ = Substitute o_ t_;\
|
neuper@37906
|
44 |
\ t_ = Substitute [k_, q__] t_;\
|
neuper@37906
|
45 |
\ t_ = Repeat (Try (Rewrite_Set norm_Poly False)) t_\
|
neuper@37906
|
46 |
\ in t_)"
|
neuper@37906
|
47 |
;
|
neuper@37906
|
48 |
val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
|
neuper@37906
|
49 |
(*---vvv-NOTok--------------------------------------------------------------*)
|
neuper@37906
|
50 |
|
neuper@37906
|
51 |
|
neuper@37906
|
52 |
|
neuper@37906
|
53 |
atomty sc;
|
neuper@37906
|
54 |
atomt sc;
|
neuper@37906
|
55 |
|
neuper@37906
|
56 |
|
neuper@37906
|
57 |
"----------- me 'Berechnung' 'erstNumerisch' ---------------------";
|
neuper@37906
|
58 |
"----------- me 'Berechnung' 'erstNumerisch' ---------------------";
|
neuper@37906
|
59 |
"----------- me 'Berechnung' 'erstNumerisch' ---------------------";
|
neuper@37906
|
60 |
val fmz =
|
neuper@37906
|
61 |
["KantenLaenge (k=10)","Querschnitt (q=1)",
|
neuper@37906
|
62 |
"KantenUnten [b1 = k - 2*q, b2 = k - 2*q, b3 = k - 2*q, b4 = k - 2*q ]",
|
neuper@37906
|
63 |
"KantenSenkrecht [v1 = k, v2 = k, v3 = k, v4 = k]",
|
neuper@37906
|
64 |
"KantenOben [t1 = k - 2*q, t2 = k - 2*q, t3 = k - 2*q, t4 = k - 2*q ]",
|
neuper@37906
|
65 |
"GesamtLaenge L"];
|
neuper@37906
|
66 |
val (dI',pI',mI') =
|
neuper@37906
|
67 |
("Isac.thy",["numerischSymbolische", "Berechnung"],
|
neuper@37906
|
68 |
["Berechnung","erstNumerisch"]);
|
neuper@37906
|
69 |
val p = e_pos'; val c = [];
|
neuper@37906
|
70 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))](*nxt = ("Model_Pr*);
|
neuper@37906
|
71 |
val (p,_,f,nxt,_,pt) = me nxt p c pt(*Add_Given "KantenLaenge (k = 10)"*);
|
neuper@37906
|
72 |
val (p,_,f,nxt,_,pt) = me nxt p c pt(*Add_Given "Querschnitt (q = 1)"*);
|
neuper@37906
|
73 |
val (p,_,f,nxt,_,pt) = me nxt p c pt(*Add_Given "KantenUnten [b1 = k - 2*q]"*);
|
neuper@37906
|
74 |
val (p,_,f,nxt,_,pt) = me nxt p c pt(*..KantenUnten [b2 = k - 2 * q, b3=..b4*);
|
neuper@37906
|
75 |
val (p,_,f,nxt,_,pt) = me nxt p c pt(*Add_Given "KantenSenkrecht [v1 = k]"*);
|
neuper@37906
|
76 |
val (p,_,f,nxt,_,pt) = me nxt p c pt(*..KantenSenkrecht [v2 = k, v3 = k, v4]*);
|
neuper@37906
|
77 |
val (p,_,f,nxt,_,pt) = me nxt p c pt(*Add_Given "KantenOben [b1 = k - 2 *q])*);
|
neuper@37906
|
78 |
val (p,_,f,nxt,_,pt) = me nxt p c pt(*..KantenOben [b2 = k - 2 * q, b3 =, b4*);
|
neuper@37906
|
79 |
val (p,_,f,nxt,_,pt) = me nxt p c pt(*Add_Find "GesamtLaenge L"*);
|
neuper@37906
|
80 |
val (p,_,f,nxt,_,pt) = me nxt p c pt(*Specify_Theory "AlgEin.thy"*);
|
neuper@37906
|
81 |
val (p,_,f,nxt,_,pt) = me nxt p c pt(*Specify_Problem ["numerischSymbolis,Be*);
|
neuper@37906
|
82 |
val (p,_,f,nxt,_,pt) = me nxt p c pt(*Specify_Method ["Berechnung", "erstSym*);
|
neuper@37906
|
83 |
val (p,_,f,nxt,_,pt) = me nxt p c pt(*Apply_Method*);
|
neuper@37906
|
84 |
val (p,_,f,nxt,_,pt) = me nxt p c pt(*Substitute["Oben = boollist2sum [b1 =*);
|
neuper@37906
|
85 |
f2str f;
|
neuper@37906
|
86 |
val (p,_,f,nxt,_,pt) = me nxt p c pt(*Substitute ["t1 = k - 2 * q", *);f2str f;
|
neuper@37906
|
87 |
val (p,_,f,nxt,_,pt) = me nxt p c pt(*Substitute ["k = 10", "q = 1"]*);f2str f;
|
neuper@37906
|
88 |
val (p,_,f,nxt,_,pt) = me nxt p c pt(*Rewrite_Set "norm_Rational"*);f2str f;
|
neuper@37906
|
89 |
val (p,_,f,nxt,_,pt) = me nxt p c pt(**);
|
neuper@37906
|
90 |
if f2str f = "L = 32 + senkrecht + unten" then ()
|
neuper@37906
|
91 |
else raise error "algein.sml diff.behav. in erstSymbolisch 1";
|
neuper@37906
|
92 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val(p,_,f,nxt,_,pt)=me nxt p c pt;f2str f;
|
neuper@37906
|
93 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val(p,_,f,nxt,_,pt)=me nxt p c pt;f2str f;
|
neuper@37906
|
94 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val(p,_,f,nxt,_,pt)=me nxt p c pt;f2str f;
|
neuper@37906
|
95 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val(p,_,f,nxt,_,pt)=me nxt p c pt;f2str f;
|
neuper@37906
|
96 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
neuper@37906
|
97 |
if f2str f = "L = 104" andalso nxt = ("End_Proof'", End_Proof') then ()
|
neuper@37906
|
98 |
else raise error "algein.sml diff.behav. in erstSymbolisch 99";
|
neuper@37906
|
99 |
|
neuper@37906
|
100 |
|
neuper@37906
|
101 |
"----------- auto 'Berechnung' 'erstSymbolisch' ------------------";
|
neuper@37906
|
102 |
"----------- auto 'Berechnung' 'erstSymbolisch' ------------------";
|
neuper@37906
|
103 |
"----------- auto 'Berechnung' 'erstSymbolisch' ------------------";
|
neuper@37906
|
104 |
states:=[];
|
neuper@37906
|
105 |
CalcTree
|
neuper@37906
|
106 |
[(["KantenLaenge (k=10)","Querschnitt (q=1)",
|
neuper@37906
|
107 |
"KantenUnten [b1 = k - 2*q, b2 = k - 2*q, b3 = k - 2*q, b4 = k - 2*q ]",
|
neuper@37906
|
108 |
"KantenSenkrecht [v1 = k, v2 = k, v3 = k, v4 = k]",
|
neuper@37906
|
109 |
"KantenOben [t1 = k - 2*q, t2 = k - 2*q, t3 = k - 2*q, t4 = k - 2*q ]",
|
neuper@37906
|
110 |
"GesamtLaenge L"],
|
neuper@37906
|
111 |
("Isac.thy",["numerischSymbolische", "Berechnung"],
|
neuper@37906
|
112 |
["Berechnung","erstSymbolisch"]))];
|
neuper@37906
|
113 |
Iterator 1;
|
neuper@37906
|
114 |
moveActiveRoot 1;
|
neuper@37906
|
115 |
autoCalculate 1 CompleteCalc;
|
neuper@37906
|
116 |
val ((pt,p),_) = get_calc 1; show_pt pt;
|
neuper@37906
|
117 |
if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = "L = 104" then()
|
neuper@37906
|
118 |
else raise error "algein.sml: 'Berechnung' 'erstSymbolisch' changed";
|
neuper@37906
|
119 |
|
neuper@37906
|
120 |
(*
|
neuper@37906
|
121 |
show_pt pt;
|
neuper@37906
|
122 |
trace_rewrite:=true;
|
neuper@37906
|
123 |
trace_rewrite:=false;
|
neuper@37906
|
124 |
trace_script:=true;
|
neuper@37906
|
125 |
trace_script:=false;
|
neuper@37906
|
126 |
*)
|
neuper@37906
|
127 |
|
neuper@37906
|
128 |
"----------- Widerspruch 3 = 777 ---------------------------------";
|
neuper@37906
|
129 |
"----------- Widerspruch 3 = 777 ---------------------------------";
|
neuper@37906
|
130 |
"----------- Widerspruch 3 = 777 ---------------------------------";
|
neuper@37906
|
131 |
val thy = Isac.thy;
|
neuper@37906
|
132 |
val rew_ord = dummy_ord;
|
neuper@37906
|
133 |
val erls = Erls;
|
neuper@37906
|
134 |
|
neuper@37906
|
135 |
val thm = assoc_thm' thy ("sym_real_mult_0_right","");
|
neuper@37906
|
136 |
val t = str2term "0 = 0";
|
neuper@37906
|
137 |
val Some (t',_) = rewrite_ thy rew_ord erls false thm t;
|
neuper@37906
|
138 |
term2str t';
|
neuper@37906
|
139 |
(********"0 = ?z1 * 0"*)
|
neuper@37906
|
140 |
|
neuper@37906
|
141 |
(*testing code in ME/appl.sml*)
|
neuper@37906
|
142 |
val sube = ["?z1 = 3"];
|
neuper@37906
|
143 |
val subte = sube2subte sube;
|
neuper@37906
|
144 |
val subst = sube2subst thy sube;
|
neuper@37906
|
145 |
foldl and_ (true, map contains_Var subte);
|
neuper@37906
|
146 |
|
neuper@37906
|
147 |
val t'' = subst_atomic subst t';
|
neuper@37906
|
148 |
term2str t'';
|
neuper@37906
|
149 |
(********"0 = 3 * 0"*)
|
neuper@37906
|
150 |
|
neuper@37906
|
151 |
val thm = assoc_thm' thy ("sym","");
|
neuper@37906
|
152 |
(*----- GOON Widerspruch 3 = 777: sym contains "==>" instead of "=" !!!
|
neuper@37906
|
153 |
val Some (t''',_) = rewrite_ thy rew_ord erls false thm t'';
|
neuper@37906
|
154 |
*)
|
neuper@37906
|
155 |
|
neuper@37906
|
156 |
(* use"../smltest/IsacKnowledge/algein.sml";
|
neuper@37906
|
157 |
*)
|
neuper@37906
|
158 |
|