neuper@37906
|
1 |
(* tests for ME/script.sml
|
neuper@37906
|
2 |
WN.13.3.00
|
neuper@37906
|
3 |
|
neuper@37906
|
4 |
WN050908 OLD FILE, MERGE WITH smltest/ME/script.sml
|
neuper@37906
|
5 |
|
neuper@37906
|
6 |
use"systest/script.sml";
|
neuper@37906
|
7 |
use"script.sml";
|
neuper@37906
|
8 |
*)
|
neuper@37906
|
9 |
|
neuper@37906
|
10 |
|
neuper@37906
|
11 |
" scripts: Variante 'funktional' ";
|
neuper@37906
|
12 |
"############## Make_fun_by_new_variable ##############";
|
neuper@37906
|
13 |
"############## Make_fun_by_explicit ##############";
|
neuper@37906
|
14 |
"################ Solve_root_equation #################";
|
neuper@37906
|
15 |
"------- Notlocatable: Free_Solve -------";
|
neuper@37906
|
16 |
|
neuper@37906
|
17 |
" --- test100: nxt_tac order------------------------------------ ";
|
neuper@37906
|
18 |
" --- test100: order 1 3 1 2 ----------------------------------- ";
|
neuper@37906
|
19 |
" --- test200: nxt_tac order ------------------------------------- ";
|
neuper@37906
|
20 |
" --- test200: order 3 1 1 2 --------------------------------- ";
|
neuper@37906
|
21 |
|
neuper@37906
|
22 |
" --- root-equation: nxt_tac order------------------------------ ";
|
neuper@37906
|
23 |
" --- root-equation: 1.norm_equation ------------------------------ ";
|
neuper@37906
|
24 |
(* --- test200: calculate -----------------------------------------*)
|
neuper@37906
|
25 |
" --- check_elementwise ------------------------------ ";
|
neuper@37906
|
26 |
|
neuper@37906
|
27 |
" --- test 30.4.02 Testterm: Repeat Repeat Or ------------------ ";
|
neuper@37906
|
28 |
" --- test 9.5.02 Testeq: While Try Repeat @@ ------------------ ";
|
neuper@37906
|
29 |
|
neuper@37906
|
30 |
"--------- sel_rules ---------------------------------------------";
|
neuper@37906
|
31 |
"-----------------------------------------------------------------";
|
neuper@37906
|
32 |
|
neuper@37906
|
33 |
|
neuper@37906
|
34 |
|
neuper@37906
|
35 |
|
neuper@37906
|
36 |
|
neuper@37906
|
37 |
" ################################################# 6.5.03";
|
neuper@37906
|
38 |
" scripts: Variante 'funktional' 6.5.03";
|
neuper@37906
|
39 |
" ################################################# 6.5.03 ";
|
neuper@37906
|
40 |
|
neuper@37906
|
41 |
val c = (the o (parse DiffApp.thy))
|
neuper@37906
|
42 |
"Script Maximum_value(fix_::bool list)(m_::real) (rs_::bool list)\
|
neuper@37906
|
43 |
\ (v_::real) (itv_::real set) (err_::bool) = \
|
neuper@37981
|
44 |
\ (let e_e = (hd o (filterVar m_)) rs_; \
|
neuper@37906
|
45 |
\ t_ = (if 1 < length_ rs_ \
|
neuper@37906
|
46 |
\ then (SubProblem (Reals_,[make,function],[no_met])\
|
neuper@37981
|
47 |
\ [real_ m_, real_ v_v, bool_list_ rs_])\
|
neuper@37906
|
48 |
\ else (hd rs_)); \
|
neuper@37906
|
49 |
\ (mx_::real) = SubProblem (Reals_,[on_interval,max_of,function], \
|
neuper@37906
|
50 |
\ [Isac,maximum_on_interval])\
|
neuper@37981
|
51 |
\ [bool_ t_, real_ v_v, real_set_ itv_]\
|
neuper@37906
|
52 |
\ in ((SubProblem (Reals_,[find_values,tool],[Isac,find_values]) \
|
neuper@37981
|
53 |
\ [real_ mx_, real_ (Rhs t_), real_ v_v, real_ m_, \
|
neuper@37981
|
54 |
\ bool_list_ (dropWhile (ident e_e) rs_)])::bool list))";
|
neuper@37906
|
55 |
|
neuper@37906
|
56 |
|
neuper@37906
|
57 |
"################################################### 6.5.03";
|
neuper@37906
|
58 |
"############## Make_fun_by_new_variable ########### 6.5.03";
|
neuper@37906
|
59 |
"################################################### 6.5.03";
|
neuper@37906
|
60 |
|
neuper@37906
|
61 |
val sc = (the o (parse DiffApp.thy)) (*start interpretieren*)
|
neuper@37906
|
62 |
"Script Make_fun_by_new_variable (f_::real) (v_::real) \
|
neuper@37906
|
63 |
\ (eqs_::bool list) = \
|
neuper@37906
|
64 |
\(let h_ = (hd o (filterVar f_)) eqs_; \
|
neuper@37906
|
65 |
\ es_ = dropWhile (ident h_) eqs_; \
|
neuper@37906
|
66 |
\ vs_ = dropWhile (ident f_) (Vars h_); \
|
neuper@37906
|
67 |
\ v_1 = nth_ 1 vs_; \
|
neuper@37906
|
68 |
\ v_2 = nth_ 2 vs_; \
|
neuper@37906
|
69 |
\ e_1 = (hd o (filterVar v_1)) es_; \
|
neuper@37906
|
70 |
\ e_2 = (hd o (filterVar v_2)) es_; \
|
neuper@37906
|
71 |
\ (s_1::bool list) = (SubProblem (Reals_,[univar,equation],[no_met])\
|
neuper@37906
|
72 |
\ [bool_ e_1, real_ v_1]);\
|
neuper@37906
|
73 |
\ (s_2::bool list) = (SubProblem (Reals_,[univar,equation],[no_met])\
|
neuper@37906
|
74 |
\ [bool_ e_2, real_ v_2])\
|
neuper@37906
|
75 |
\in Substitute [(v_1 = (rhs o hd) s_1),(v_2 = (rhs o hd) s_2)] h_)";
|
neuper@37906
|
76 |
|
neuper@37906
|
77 |
val ags = map (term_of o the o (parse DiffApp.thy))
|
neuper@37906
|
78 |
["A::real", "alpha::real",
|
neuper@37906
|
79 |
"[A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]"];
|
neuper@37906
|
80 |
val ll = [](*:loc_*);
|
neuper@37906
|
81 |
(* problem with exn PTREE + eval_to -------------------------
|
neuper@37906
|
82 |
"-------------- subproblem with empty formalizaton -------";
|
neuper@37906
|
83 |
val (mI1,m1) =
|
neuper@37906
|
84 |
("Subproblem", tac2tac_ pt p
|
neuper@37906
|
85 |
(Subproblem (("Reals",["univar","equation","test"],
|
neuper@37906
|
86 |
(""(*"ANDERN !!!!!!!*),"no_met")),[])));
|
neuper@37906
|
87 |
val (mI2,m2) = (mI1,m1);
|
neuper@37906
|
88 |
val (mI3,m3) =
|
neuper@37906
|
89 |
("Substitute", tac2tac_ pt p
|
neuper@37906
|
90 |
(Substitute [("a","#2*r*sin alpha"),("b","#2*r*cos alpha")]));
|
neuper@37906
|
91 |
"------- same_tacpbl + eval_to -------";
|
neuper@37926
|
92 |
val SOME(l1,t1) = same_tacpbl sc ll (mI1,m1);
|
neuper@37906
|
93 |
loc_2str l1;
|
neuper@37906
|
94 |
(*"[R, R, D, R, D, R, D, R, D, R, D, R, D, R, D, L, R]"*)
|
neuper@37934
|
95 |
Syntax.string_of_term (thy2ctxt' "DiffApp") t1;
|
neuper@37906
|
96 |
(*"solve_univar (Reals, [univar, equation], no_met) B.1 B.3 "?6 ?4 *)
|
neuper@37906
|
97 |
|
neuper@37926
|
98 |
val SOME(l2,t2) = same_tacpbl sc l1 (mI2,m2);
|
neuper@37906
|
99 |
loc_2str l2;
|
neuper@37906
|
100 |
(*"[R, R, D, R, D, R, D, R, D, R, D, R, D, R, D, R, D, L, R]"*)
|
neuper@37934
|
101 |
Syntax.string_of_term (thy2ctxt' "DiffApp") t2;
|
neuper@37906
|
102 |
(*"solve_univar (Reals, [univar, equation], no_met) B.1 B.3 "?7 ?3 *)
|
neuper@37906
|
103 |
|
neuper@37926
|
104 |
val SOME(l3,t3) = same_tacpbl sc l2 (mI3,m3);
|
neuper@37906
|
105 |
loc_2str l3;
|
neuper@37906
|
106 |
(*"[R, R, D, R, D, R, D, R, D, R, D, R, D, R, D, R, D, R, D]"*)
|
neuper@37934
|
107 |
Syntax.string_of_term (thy2ctxt' "DiffApp") t3;
|
neuper@37906
|
108 |
(*"Substitute [(v_1, (Rhs o hd) B.1), (v_2, (Rhs o hd) B.0)] B.8"*)
|
neuper@37906
|
109 |
|
neuper@37906
|
110 |
|
neuper@37906
|
111 |
"------- eq_tacIDs + eq_consts + eval_args -------";
|
neuper@37906
|
112 |
val eq_ids = eq_tacIDs (*start-loc_*)[] sc (mI,m) [];
|
neuper@37906
|
113 |
val eq_cons = filter (eq_consts m) eq_ids;
|
neuper@37906
|
114 |
val Ready (l,(_,m)::_,_) = eval_args sc (mI,m) [(1,ags)] eq_cons;
|
neuper@37906
|
115 |
"------- locate -------";
|
neuper@37906
|
116 |
|
neuper@37906
|
117 |
|
neuper@37906
|
118 |
"-------------- subproblem with formalizaton -------";
|
neuper@37906
|
119 |
val (mI,m) =
|
neuper@37906
|
120 |
("Subproblem", tac2tac_ pt []
|
neuper@37906
|
121 |
(Subproblem (("Reals",["univar","equation","test"],
|
neuper@37906
|
122 |
(""(*"ANDERN !!!!!!!*),"no_met")),
|
neuper@37906
|
123 |
["a//#2=r*sin alpha","a"])));
|
neuper@37906
|
124 |
"------- same_tacpbl + eval_to -------";
|
neuper@37906
|
125 |
|
neuper@37906
|
126 |
|
neuper@37906
|
127 |
"------- eq_tacIDs + eq_consts + eval_args -------";
|
neuper@37906
|
128 |
val eq_ids = eq_tacIDs [] sc (mI,m) [];
|
neuper@37906
|
129 |
val eq_cons = filter (eq_consts m) eq_ids;
|
neuper@37906
|
130 |
val Ready (l,(_,m)::_,_) = eval_args sc (mI,m) [(1,ags)] eq_cons;
|
neuper@37906
|
131 |
|
neuper@37906
|
132 |
|
neuper@37906
|
133 |
"------- locate -------";
|
neuper@37906
|
134 |
-------------------------------------------------------*)
|
neuper@37906
|
135 |
(* use"ME/script.sml";
|
neuper@37906
|
136 |
use"test-script.sml";
|
neuper@37906
|
137 |
*)
|
neuper@37906
|
138 |
|
neuper@37906
|
139 |
|
neuper@37906
|
140 |
|
neuper@37906
|
141 |
"############## Make_fun_by_explicit ############## 6.5.03";
|
neuper@37906
|
142 |
"############## Make_fun_by_explicit ############## 6.5.03";
|
neuper@37906
|
143 |
"############## Make_fun_by_explicit ############## 6.5.03";
|
neuper@37906
|
144 |
val c = (the o (parse DiffApp.thy))
|
neuper@37906
|
145 |
"Script Make_fun_by_explicit (f_::real) (v_::real) \
|
neuper@37906
|
146 |
\ (eqs_::bool list) = \
|
neuper@37906
|
147 |
\ (let h_ = (hd o (filterVar f_)) eqs_; \
|
neuper@37906
|
148 |
\ e_1 = hd (dropWhile (ident h_) eqs_); \
|
neuper@37906
|
149 |
\ vs_ = dropWhile (ident f_) (Vars h_); \
|
neuper@37981
|
150 |
\ v_1 = hd (dropWhile (ident v_v) vs_); \
|
neuper@37906
|
151 |
\ (s_1::bool list)=(SubProblem(Reals_,[univar,equation],[no_met])\
|
neuper@37906
|
152 |
\ [bool_ e_1, real_ v_1])\
|
neuper@37906
|
153 |
\ in Substitute [(v_1 = (rhs o hd) s_1)] h_)";
|
neuper@37906
|
154 |
|
neuper@37906
|
155 |
|
neuper@37906
|
156 |
(*#####################################################--------11.5.02
|
neuper@37906
|
157 |
"################ Solve_root_equation #################";
|
neuper@37906
|
158 |
(*#####################################################*)
|
neuper@37906
|
159 |
val sc = (term_of o the o (parse Test.thy))
|
neuper@37906
|
160 |
"Script Solve_root_equation (eq_::bool) (v_::real) (err_::bool) =\
|
neuper@37981
|
161 |
\ (let e_e = Rewrite square_equation_left True eq_; \
|
neuper@37981
|
162 |
\ e_e = Rewrite_Set Test_simplify False e_; \
|
neuper@37981
|
163 |
\ e_e = Rewrite_Set rearrange_assoc False e_; \
|
neuper@37981
|
164 |
\ e_e = Rewrite_Set isolate_root False e_; \
|
neuper@37981
|
165 |
\ e_e = Rewrite_Set Test_simplify False e_; \
|
neuper@37906
|
166 |
|
neuper@37981
|
167 |
\ e_e = Rewrite square_equation_left True e_; \
|
neuper@37981
|
168 |
\ e_e = Rewrite_Set Test_simplify False e_; \
|
neuper@37906
|
169 |
|
neuper@37981
|
170 |
\ e_e = Rewrite_Set norm_equation False e_; \
|
neuper@37981
|
171 |
\ e_e = Rewrite_Set Test_simplify False e_; \
|
neuper@37981
|
172 |
\ e_e = Rewrite_Set_Inst [(bdv,v_)] isolate_bdv False e_;\
|
neuper@37981
|
173 |
\ e_e = Rewrite_Set Test_simplify False e_e \
|
neuper@37906
|
174 |
\ in [e_::bool])";
|
neuper@37906
|
175 |
val ags = map (term_of o the o (parse Test.thy))
|
neuper@37906
|
176 |
["sqrt(#9+#4*x)=sqrt x + sqrt(#5+x)", "x::real","#0"];
|
neuper@37906
|
177 |
val fmz =
|
neuper@37906
|
178 |
["equality (sqrt(#9+#4*x)=sqrt x + sqrt(#5+x))",
|
neuper@37906
|
179 |
"solveFor x","errorBound (eps = #0)","solutions v_i_"];
|
neuper@37906
|
180 |
----------------------------------------------------------------11.5.02...*)
|
neuper@37906
|
181 |
|
neuper@37906
|
182 |
|
neuper@37906
|
183 |
(*################################# meNEW raises exception with not-locatable
|
neuper@37906
|
184 |
"--------------------- Notlocatable: Free_Solve ---------------------";
|
neuper@37906
|
185 |
"--------------------- Notlocatable: Free_Solve ---------------------";
|
neuper@37906
|
186 |
"--------------------- Notlocatable: Free_Solve ---------------------";
|
neuper@37906
|
187 |
val fmz = [];
|
neuper@37906
|
188 |
val (dI',pI',mI') =
|
neuper@37906
|
189 |
("Test.thy",["sqroot-test","univariate","equation","test"],
|
neuper@37906
|
190 |
["Test","sqrt-equ-test"]);
|
neuper@37906
|
191 |
(*val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
|
neuper@37906
|
192 |
val (p,_,f,nxt,_,pt) = me (mI,m) e_pos'[1] EmptyPtree;*)
|
neuper@37906
|
193 |
|
neuper@37906
|
194 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
neuper@37906
|
195 |
val nxt = ("Model_Problem",
|
neuper@37906
|
196 |
Model_Problem ["sqroot-test","univariate","equation","test"]);
|
neuper@37906
|
197 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@37906
|
198 |
val nxt =
|
neuper@37906
|
199 |
("Add_Given",
|
neuper@37906
|
200 |
Add_Given "equality (sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x))");
|
neuper@37906
|
201 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@37906
|
202 |
val nxt = ("Add_Given",Add_Given "solveFor x");
|
neuper@37906
|
203 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@37906
|
204 |
val nxt = ("Add_Given",Add_Given "errorBound (eps = 0)");
|
neuper@37906
|
205 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@37906
|
206 |
val nxt = ("Add_Find",Add_Find "solutions v_i_");
|
neuper@37906
|
207 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@37906
|
208 |
val nxt = ("Specify_Theory",Specify_Theory "Test.thy");
|
neuper@37906
|
209 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@37906
|
210 |
val nxt =
|
neuper@37906
|
211 |
("Specify_Problem",Specify_Problem ["sqroot-test","univariate","equation","test"]);
|
neuper@37906
|
212 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@37906
|
213 |
val nxt = ("Specify_Method",Specify_Method ["Test","sqrt-equ-test"]);
|
neuper@37906
|
214 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
neuper@37906
|
215 |
|
neuper@37906
|
216 |
"--- -1 ---";
|
neuper@37906
|
217 |
val nxt = ("Free_Solve",Free_Solve);
|
neuper@37906
|
218 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
219 |
|
neuper@37906
|
220 |
"--- 0 ---";
|
neuper@37906
|
221 |
val nxt = ("Take",Take "sqrt(9+4*x)=sqrt x + sqrt(5+x)");
|
neuper@37906
|
222 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
223 |
(*me ("Begin_Trans" ////*)
|
neuper@37906
|
224 |
|
neuper@37906
|
225 |
"--- 1 ---";
|
neuper@37906
|
226 |
val nxt = ("Rewrite_Asm",Rewrite_Asm ("square_equation_left",""));
|
neuper@37906
|
227 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
228 |
|
neuper@37906
|
229 |
"--- 2 ---";
|
neuper@37906
|
230 |
val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");
|
neuper@37906
|
231 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
232 |
|
neuper@37906
|
233 |
"--- 3 ---";
|
neuper@37906
|
234 |
val nxt = ("Rewrite_Set",Rewrite_Set "rearrange_assoc");
|
neuper@37906
|
235 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
neuper@37906
|
236 |
if f = Form'
|
neuper@37906
|
237 |
(FormKF
|
neuper@37906
|
238 |
(~1,EdUndef,1,Nundef,
|
neuper@37906
|
239 |
"9 + 4 * x = 5 + 2 * x + 2 * sqrt (x ^^^ 2 + 5 * x)"))
|
neuper@37906
|
240 |
then () else raise error "behaviour in root-expl. Free_Solve changed";
|
neuper@37906
|
241 |
writeln (pr_ptree pr_short pt);
|
neuper@37906
|
242 |
---------------------------------meNEW raises exception with not-locatable*)
|
neuper@37906
|
243 |
|
neuper@37906
|
244 |
|
neuper@37906
|
245 |
val d = e_rls;
|
neuper@37906
|
246 |
|
neuper@37906
|
247 |
" --- test100: nxt_tac order------------------------------------ ";
|
neuper@37906
|
248 |
" --- test100: nxt_tac order------------------------------------ ";
|
neuper@37906
|
249 |
|
neuper@37906
|
250 |
val scr as (Script sc) = Script (((inst_abs Test.thy)
|
neuper@37906
|
251 |
o term_of o the o (parse thy))
|
neuper@37982
|
252 |
"Script Testeq (e_e::bool) = \
|
neuper@37981
|
253 |
\(While (contains_root e_e) Do \
|
neuper@37906
|
254 |
\((Try (Repeat (Rewrite rroot_square_inv False))) @@ \
|
neuper@37906
|
255 |
\ (Try (Repeat (Rewrite square_equation_left True))) @@ \
|
neuper@37906
|
256 |
\ (Try (Repeat (Rewrite radd_0 False)))))\
|
neuper@37981
|
257 |
\ e_e ");
|
neuper@37906
|
258 |
atomty sc;
|
neuper@37906
|
259 |
val (dI',pI',mI') = ("Test.thy",["sqroot-test","univariate","equation","test"],
|
neuper@37906
|
260 |
["Test","sqrt-equ-test"]);
|
neuper@37906
|
261 |
val p = e_pos'; val c = [];
|
neuper@37906
|
262 |
val (mI,m) = ("Init_Proof",Init_Proof ([], (dI',pI',mI')));
|
neuper@37906
|
263 |
val (p,_,_,_,_,pt) = me (mI,m) p c EmptyPtree;
|
neuper@37906
|
264 |
val nxt = ("Specify_Theory",Specify_Theory "Test.thy");
|
neuper@37906
|
265 |
val (p,_,_,_,_,pt) = me nxt p c pt;
|
neuper@37906
|
266 |
val nxt = ("Specify_Method",Specify_Method ["Test","sqrt-equ-test"]); (*for asm in square_equation_left*)
|
neuper@37906
|
267 |
val (p,_,_,_,_,pt) = me nxt p c pt;
|
neuper@37906
|
268 |
val p = ([1],Res):pos';
|
neuper@37906
|
269 |
val eq_ = (term_of o the o (parse thy))"e_::bool";
|
neuper@37906
|
270 |
|
neuper@37906
|
271 |
val ct = "0+(sqrt(sqrt(sqrt a))^^^2)^^^2=0";
|
neuper@37906
|
272 |
val ve0_= (term_of o the o (parse thy)) ct;
|
neuper@37906
|
273 |
val ets0=[([],(Tac_(Script.thy,"BS","",""),[(eq_,ve0_)],[(eq_,ve0_)],
|
neuper@37906
|
274 |
e_term,e_term,Safe)),
|
neuper@37906
|
275 |
([],(User', [], [], e_term, e_term,Sundef))]:ets;
|
neuper@37906
|
276 |
val l0 = [];
|
neuper@37906
|
277 |
" --------------- 1. ---------------------------------------------";
|
neuper@37906
|
278 |
val (pt,_) = cappend_atomic pt[1]e_istate e_term(Rewrite("test",""))(str2term ct,[])Complete;
|
neuper@37906
|
279 |
(*12.10.03:*** Unknown theorem(s) "rroot_square_inv"
|
neuper@37906
|
280 |
val Appl m'=applicable_in p pt (Rewrite("rroot_square_inv",""));
|
neuper@37906
|
281 |
*)
|
neuper@37906
|
282 |
|
neuper@37906
|
283 |
|
neuper@37906
|
284 |
val scr as (Script sc) =
|
neuper@37906
|
285 |
Script (((inst_abs Test.thy) o term_of o the o (parse thy))
|
neuper@37906
|
286 |
"Script Testterm (g_::real) = (Calculate cancel g_)");
|
neuper@37906
|
287 |
(*
|
neuper@37906
|
288 |
val scr as (Script sc) =
|
neuper@37906
|
289 |
Script (((inst_abs Test.thy) o term_of o the o (parse thy))
|
neuper@37906
|
290 |
"Script Testterm (g_::real) = (Calculate power g_)");
|
neuper@37906
|
291 |
val scr as (Script sc) =
|
neuper@37906
|
292 |
Script (((inst_abs Test.thy) o term_of o the o (parse thy))
|
neuper@37906
|
293 |
"Script Testterm (g_::real) = (Calculate pow g_)");
|
neuper@37906
|
294 |
..............................................................*)
|
neuper@37906
|
295 |
writeln
|
neuper@37906
|
296 |
"%%%%%%%%%%TODO 7.9.00---vvvvvv--- conflicts with Isa-types \n\
|
neuper@37906
|
297 |
\ (Repeat (Calculate cancel g_)) Or \n\
|
neuper@37906
|
298 |
\ (Repeat (Calculate power g_)) Or \n\
|
neuper@37906
|
299 |
\%%%%%%%%%%%%%%%%%%%%%---^^^^^^--- conflicts with Isa-types \n\
|
neuper@37906
|
300 |
\%%%%%%%%%%%%%%%%%%%%%TODO before Detail Rewrite_Set";
|
neuper@37906
|
301 |
|
neuper@37906
|
302 |
|
neuper@37906
|
303 |
"--------- sel_rules ---------------------------------------------";
|
neuper@37906
|
304 |
"--------- sel_rules ---------------------------------------------";
|
neuper@37906
|
305 |
"--------- sel_rules ---------------------------------------------";
|
neuper@37906
|
306 |
states:=[];
|
neuper@37906
|
307 |
CalcTree
|
neuper@37906
|
308 |
[(["equality (x+1=2)", "solveFor x","solutions L"],
|
neuper@37906
|
309 |
("Test.thy",
|
neuper@37906
|
310 |
["sqroot-test","univariate","equation","test"],
|
neuper@37906
|
311 |
["Test","squ-equ-test-subpbl1"]))];
|
neuper@37906
|
312 |
Iterator 1;
|
neuper@37906
|
313 |
moveActiveRoot 1;
|
neuper@37906
|
314 |
autoCalculate 1 CompleteCalc;
|
neuper@37906
|
315 |
val ((pt,_),_) = get_calc 1;
|
neuper@37906
|
316 |
show_pt pt;
|
neuper@37906
|
317 |
|
neuper@37906
|
318 |
val tacs = sel_rules pt ([],Pbl);
|
neuper@37906
|
319 |
if tacs = [Apply_Method ["Test", "squ-equ-test-subpbl1"]] then ()
|
neuper@37906
|
320 |
else raise error "script.sml: diff.behav. in sel_rules ([],Pbl)";
|
neuper@37906
|
321 |
|
neuper@37906
|
322 |
val tacs = sel_rules pt ([1],Res);
|
neuper@37906
|
323 |
if tacs = [Rewrite_Set "norm_equation", Rewrite_Set "Test_simplify",
|
neuper@37906
|
324 |
Subproblem ("Test.thy", ["linear", "univariate", "equation", "test"]),
|
neuper@37906
|
325 |
Check_elementwise "Assumptions"] then ()
|
neuper@37906
|
326 |
else raise error "script.sml: diff.behav. in sel_rules ([1],Res)";
|
neuper@37906
|
327 |
|
neuper@37906
|
328 |
val tacs = sel_rules pt ([3],Pbl);
|
neuper@37906
|
329 |
if tacs = [Apply_Method ["Test", "solve_linear"]] then ()
|
neuper@37906
|
330 |
else raise error "script.sml: diff.behav. in sel_rules ([3],Pbl)";
|
neuper@37906
|
331 |
|
neuper@37906
|
332 |
val tacs = sel_rules pt ([3,1],Res);
|
neuper@37906
|
333 |
if tacs = [Rewrite_Set_Inst (["(bdv, x)"], "isolate_bdv"),
|
neuper@37906
|
334 |
Rewrite_Set "Test_simplify"] then ()
|
neuper@37906
|
335 |
else raise error "script.sml: diff.behav. in sel_rules ([3,1],Res)";
|
neuper@37906
|
336 |
|
neuper@37906
|
337 |
val tacs = sel_rules pt ([3],Res);
|
neuper@37906
|
338 |
if tacs = [Rewrite_Set "norm_equation", Rewrite_Set "Test_simplify",
|
neuper@37906
|
339 |
Subproblem ("Test.thy", ["linear", "univariate", "equation", "test"]),
|
neuper@37906
|
340 |
Check_elementwise "Assumptions"] then ()
|
neuper@37906
|
341 |
else raise error "script.sml: diff.behav. in sel_rules ([3],Res)";
|
neuper@37906
|
342 |
|
neuper@37906
|
343 |
val tacs = (sel_rules pt ([],Res)) handle PTREE str => [Tac str];
|
neuper@37906
|
344 |
if tacs = [Tac "no tactics applicable at the end of a calculation"] then ()
|
neuper@37906
|
345 |
else raise error "script.sml: diff.behav. in sel_rules ([],Res)";
|