80 val ll = [](*:loc_*); |
80 val ll = [](*:loc_*); |
81 (* problem with exn PTREE + eval_to ------------------------- |
81 (* problem with exn PTREE + eval_to ------------------------- |
82 "-------------- subproblem with empty formalizaton -------"; |
82 "-------------- subproblem with empty formalizaton -------"; |
83 val (mI1,m1) = |
83 val (mI1,m1) = |
84 ("Subproblem", tac2tac_ pt p |
84 ("Subproblem", tac2tac_ pt p |
85 (Subproblem (("Reals",["univar","equation","test"], |
85 (Subproblem (("Reals",["univar", "equation", "test"], |
86 (""(*"ANDERN !!!!!!!*),"no_met")),[]))); |
86 (""(*"ANDERN !!!!!!!*),"no_met")),[]))); |
87 val (mI2,m2) = (mI1,m1); |
87 val (mI2,m2) = (mI1,m1); |
88 val (mI3,m3) = |
88 val (mI3,m3) = |
89 ("Substitute", tac2tac_ pt p |
89 ("Substitute", tac2tac_ pt p |
90 (Substitute [("a","#2*r*sin alpha"),("b","#2*r*cos alpha")])); |
90 (Substitute [("a", "#2*r*sin alpha"),("b", "#2*r*cos alpha")])); |
91 "------- same_tacpbl + eval_to -------"; |
91 "------- same_tacpbl + eval_to -------"; |
92 val SOME(l1,t1) = same_tacpbl sc ll (mI1,m1); |
92 val SOME(l1,t1) = same_tacpbl sc ll (mI1,m1); |
93 loc_2str l1; |
93 loc_2str l1; |
94 (*"[R, R, D, R, D, R, D, R, D, R, D, R, D, R, D, L, R]"*) |
94 (*"[R, R, D, R, D, R, D, R, D, R, D, R, D, R, D, L, R]"*) |
95 Syntax.string_of_term (ThyC.id_to_ctxt "DiffApp") t1; |
95 Syntax.string_of_term (ThyC.id_to_ctxt "DiffApp") t1; |
116 |
116 |
117 |
117 |
118 "-------------- subproblem with formalizaton -------"; |
118 "-------------- subproblem with formalizaton -------"; |
119 val (mI,m) = |
119 val (mI,m) = |
120 ("Subproblem", tac2tac_ pt [] |
120 ("Subproblem", tac2tac_ pt [] |
121 (Subproblem (("Reals",["univar","equation","test"], |
121 (Subproblem (("Reals",["univar", "equation", "test"], |
122 (""(*"ANDERN !!!!!!!*),"no_met")), |
122 (""(*"ANDERN !!!!!!!*),"no_met")), |
123 ["a//#2=r*sin alpha","a"]))); |
123 ["a//#2=r*sin alpha", "a"]))); |
124 "------- same_tacpbl + eval_to -------"; |
124 "------- same_tacpbl + eval_to -------"; |
125 |
125 |
126 |
126 |
127 "------- eq_tacIDs + eq_consts + eval_args -------"; |
127 "------- eq_tacIDs + eq_consts + eval_args -------"; |
128 val eq_ids = eq_tacIDs [] sc (mI,m) []; |
128 val eq_ids = eq_tacIDs [] sc (mI,m) []; |
171 \ e_e = Rewrite_Set Test_simplify False e_; \ |
171 \ e_e = Rewrite_Set Test_simplify False e_; \ |
172 \ e_e = Rewrite_Set_Inst [(''bdv'',v_)] isolate_bdv False e_;\ |
172 \ e_e = Rewrite_Set_Inst [(''bdv'',v_)] isolate_bdv False e_;\ |
173 \ e_e = Rewrite_Set Test_simplify False e_e \ |
173 \ e_e = Rewrite_Set Test_simplify False e_e \ |
174 \ in [e_::bool])"; |
174 \ in [e_::bool])"; |
175 val ags = map (Thm.term_of o the o (parse Test.thy)) |
175 val ags = map (Thm.term_of o the o (parse Test.thy)) |
176 ["sqrt(#9+#4*x)=sqrt x + sqrt(#5+x)", "x::real","#0"]; |
176 ["sqrt(#9+#4*x)=sqrt x + sqrt(#5+x)", "x::real", "#0"]; |
177 val fmz = |
177 val fmz = |
178 ["equality (sqrt(#9+#4*x)=sqrt x + sqrt(#5+x))", |
178 ["equality (sqrt(#9+#4*x)=sqrt x + sqrt(#5+x))", |
179 "solveFor x","errorBound (eps = #0)","solutions v_i_"]; |
179 "solveFor x", "errorBound (eps = #0)", "solutions v_i_"]; |
180 ----------------------------------------------------------------11.5.02...*) |
180 ----------------------------------------------------------------11.5.02...*) |
181 |
181 |
182 |
182 |
183 (*################################# me raises exception with not-locatable |
183 (*################################# me raises exception with not-locatable |
184 "--------------------- Notlocatable: Free_Solve ---------------------"; |
184 "--------------------- Notlocatable: Free_Solve ---------------------"; |
185 "--------------------- Notlocatable: Free_Solve ---------------------"; |
185 "--------------------- Notlocatable: Free_Solve ---------------------"; |
186 "--------------------- Notlocatable: Free_Solve ---------------------"; |
186 "--------------------- Notlocatable: Free_Solve ---------------------"; |
187 val fmz = []; |
187 val fmz = []; |
188 val (dI',pI',mI') = |
188 val (dI',pI',mI') = |
189 ("Test",["sqroot-test","univariate","equation","test"], |
189 ("Test",["sqroot-test", "univariate", "equation", "test"], |
190 ["Test","sqrt-equ-test"]); |
190 ["Test", "sqrt-equ-test"]); |
191 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
191 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
192 val nxt = ("Model_Problem", |
192 val nxt = ("Model_Problem", |
193 Model_Problem ["sqroot-test","univariate","equation","test"]); |
193 Model_Problem ["sqroot-test", "univariate", "equation", "test"]); |
194 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
194 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
195 val nxt = |
195 val nxt = |
196 ("Add_Given", |
196 ("Add_Given", |
197 Add_Given "equality (sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x))"); |
197 Add_Given "equality (sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x))"); |
198 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
198 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
203 val nxt = ("Add_Find",Add_Find "solutions v_i_"); |
203 val nxt = ("Add_Find",Add_Find "solutions v_i_"); |
204 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
204 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
205 val nxt = ("Specify_Theory",Specify_Theory "Test"); |
205 val nxt = ("Specify_Theory",Specify_Theory "Test"); |
206 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
206 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
207 val nxt = |
207 val nxt = |
208 ("Specify_Problem",Specify_Problem ["sqroot-test","univariate","equation","test"]); |
208 ("Specify_Problem",Specify_Problem ["sqroot-test", "univariate", "equation", "test"]); |
209 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
209 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
210 val nxt = ("Specify_Method",Specify_Method ["Test","sqrt-equ-test"]); |
210 val nxt = ("Specify_Method",Specify_Method ["Test", "sqrt-equ-test"]); |
211 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
211 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
212 |
212 |
213 "--- -1 ---"; |
213 "--- -1 ---"; |
214 val nxt = ("Free_Solve",Free_Solve); |
214 val nxt = ("Free_Solve",Free_Solve); |
215 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
215 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
218 val nxt = ("Take",Take "sqrt(9+4*x)=sqrt x + sqrt(5+x)"); |
218 val nxt = ("Take",Take "sqrt(9+4*x)=sqrt x + sqrt(5+x)"); |
219 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
219 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
220 (*me ("Begin_Trans" ////*) |
220 (*me ("Begin_Trans" ////*) |
221 |
221 |
222 "--- 1 ---"; |
222 "--- 1 ---"; |
223 val nxt = ("Rewrite_Asm",Rewrite_Asm ("square_equation_left","")); |
223 val nxt = ("Rewrite_Asm",Rewrite_Asm ("square_equation_left", "")); |
224 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
224 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
225 |
225 |
226 "--- 2 ---"; |
226 "--- 2 ---"; |
227 val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify"); |
227 val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify"); |
228 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
228 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
251 \((Try (Repeat (Rewrite rroot_square_inv))) #> \ |
251 \((Try (Repeat (Rewrite rroot_square_inv))) #> \ |
252 \ (Try (Repeat (Rewrite square_equation_left))) #> \ |
252 \ (Try (Repeat (Rewrite square_equation_left))) #> \ |
253 \ (Try (Repeat (Rewrite radd_0)))))\ |
253 \ (Try (Repeat (Rewrite radd_0)))))\ |
254 \ e_e "); |
254 \ e_e "); |
255 atomty sc; |
255 atomty sc; |
256 val (dI',pI',mI') = ("Test",["sqroot-test","univariate","equation","test"], |
256 val (dI',pI',mI') = ("Test",["sqroot-test", "univariate", "equation", "test"], |
257 ["Test","sqrt-equ-test"]); |
257 ["Test", "sqrt-equ-test"]); |
258 val c = []; |
258 val c = []; |
259 val (p,_,_,_,_,pt) = CalcTreeTEST [([], (dI',pI',mI')))]; |
259 val (p,_,_,_,_,pt) = CalcTreeTEST [([], (dI',pI',mI')))]; |
260 val nxt = ("Specify_Theory",Specify_Theory "Test"); |
260 val nxt = ("Specify_Theory",Specify_Theory "Test"); |
261 val (p,_,_,_,_,pt) = me nxt p c pt; |
261 val (p,_,_,_,_,pt) = me nxt p c pt; |
262 val nxt = ("Specify_Method",Specify_Method ["Test","sqrt-equ-test"]); (*for asm in square_equation_left*) |
262 val nxt = ("Specify_Method",Specify_Method ["Test", "sqrt-equ-test"]); (*for asm in square_equation_left*) |
263 val (p,_,_,_,_,pt) = me nxt p c pt; |
263 val (p,_,_,_,_,pt) = me nxt p c pt; |
264 val p = ([1],Res):pos'; |
264 val p = ([1],Res):pos'; |
265 val eq_ = (Thm.term_of o the o (parse thy))"e_::bool"; |
265 val eq_ = (Thm.term_of o the o (parse thy))"e_::bool"; |
266 |
266 |
267 val ct = "0+(sqrt(sqrt(sqrt a))^^^2)^^^2=0"; |
267 val ct = "0+(sqrt(sqrt(sqrt a))^^^2)^^^2=0"; |
268 val ve0_= (Thm.term_of o the o (parse thy)) ct; |
268 val ve0_= (Thm.term_of o the o (parse thy)) ct; |
269 val ets0=[([],(Tac_(Program.thy,"BS","",""),[(eq_,ve0_)],[(eq_,ve0_)], |
269 val ets0=[([],(Tac_(Program.thy,"BS", "", ""),[(eq_,ve0_)],[(eq_,ve0_)], |
270 TermC.empty,TermC.empty,Safe)), |
270 TermC.empty,TermC.empty,Safe)), |
271 ([],(User', [], [], TermC.empty, TermC.empty,Sundef))]:ets; |
271 ([],(User', [], [], TermC.empty, TermC.empty,Sundef))]:ets; |
272 val l0 = []; |
272 val l0 = []; |
273 " --------------- 1. ---------------------------------------------"; |
273 " --------------- 1. ---------------------------------------------"; |
274 val (pt,_) = cappend_atomic pt[1]Istate.empty TermC.empty(Rewrite("test",""))(str2term ct,[])Complete; |
274 val (pt,_) = cappend_atomic pt[1]Istate.empty TermC.empty(Rewrite("test", ""))(str2term ct,[])Complete; |
275 (*12.10.03:*** Unknown theorem(s) "rroot_square_inv" |
275 (*12.10.03:*** Unknown theorem(s) "rroot_square_inv" |
276 val Applicable.Yes m' = Step.check (Rewrite("rroot_square_inv","")) (pt, p); |
276 val Applicable.Yes m' = Step.check (Rewrite("rroot_square_inv", "")) (pt, p); |
277 *) |
277 *) |
278 |
278 |
279 |
279 |
280 val scr as (Prog sc) = |
280 val scr as (Prog sc) = |
281 Prog (((inst_abs Test.thy) o Thm.term_of o the o (parse thy)) |
281 Prog (((inst_abs Test.thy) o Thm.term_of o the o (parse thy)) |