197 "\"lhs (-1 / 8 + -1 * (1 / 8 + -1 * sqrt (9 / 16) / 2) / 4 +\n (1 / 8 + -1 * sqrt (9 / 16) / 2) ^^^ 2 =\n 0) is_poly_in 1 / 8 + -1 * sqrt (9 / 16) / 2\","^ |
197 "\"lhs (-1 / 8 + -1 * (1 / 8 + -1 * sqrt (9 / 16) / 2) / 4 +\n (1 / 8 + -1 * sqrt (9 / 16) / 2) ^^^ 2 =\n 0) is_poly_in 1 / 8 + -1 * sqrt (9 / 16) / 2\","^ |
198 "\"lhs (-1 / 8 + -1 * (1 / 8 + -1 * sqrt (9 / 16) / 2) / 4 +\n (1 / 8 + -1 * sqrt (9 / 16) / 2) ^^^ 2 =\n 0) has_degree_in 1 / 8 + -1 * sqrt (9 / 16) / 2 =\n2\"]"; |
198 "\"lhs (-1 / 8 + -1 * (1 / 8 + -1 * sqrt (9 / 16) / 2) / 4 +\n (1 / 8 + -1 * sqrt (9 / 16) / 2) ^^^ 2 =\n 0) has_degree_in 1 / 8 + -1 * sqrt (9 / 16) / 2 =\n2\"]"; |
199 (*TODO simplify assumptions (sqrt!) and check ERROR in has_degree_in*); |
199 (*TODO simplify assumptions (sqrt!) and check ERROR in has_degree_in*); |
200 member op = specsteps mI (*false*); |
200 member op = specsteps mI (*false*); |
201 (*loc_solve_ (mI,m) ptp; |
201 (*loc_solve_ (mI,m) ptp; |
202 WAS: not-found-in-script: NotLocatable from Skip1 (Const ("List...*) |
202 WAS: not-found-in-script: NotLocatable from Term_Val1 (Const ("List...*) |
203 "~~~~~ fun loc_solve_, args:"; val (m, (pt,pos)) = ((mI,m), ptp); |
203 "~~~~~ fun loc_solve_, args:"; val (m, (pt,pos)) = ((mI,m), ptp); |
204 (*solve m (pt, pos); |
204 (*solve m (pt, pos); |
205 WAS: not-found-in-script: NotLocatable from Skip1 (Const ("List...*) |
205 WAS: not-found-in-script: NotLocatable from Term_Val1 (Const ("List...*) |
206 "~~~~~ fun solve, args:"; val ((mI,m), (pt, po as (p,p_))) = (m, (pt, pos)); |
206 "~~~~~ fun solve, args:"; val ((mI,m), (pt, po as (p,p_))) = (m, (pt, pos)); |
207 e_metID = get_obj g_metID pt (par_pblobj pt p) (*false*); |
207 e_metID = get_obj g_metID pt (par_pblobj pt p) (*false*); |
208 val thy' = get_obj g_domID pt (par_pblobj pt p); |
208 val thy' = get_obj g_domID pt (par_pblobj pt p); |
209 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; |
209 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; |
210 val d = e_rls; |
210 val d = e_rls; |
211 (*locate_input_tactic (thy',srls) m (pt,(p,p_)) (sc,d) is; |
211 (*locate_input_tactic (thy',srls) m (pt,(p,p_)) (sc,d) is; |
212 WAS: not-found-in-script: NotLocatable from Skip1 (Const ("List...*) |
212 WAS: not-found-in-script: NotLocatable from Term_Val1 (Const ("List...*) |
213 "~~~~~ fun locate_input_tactic, args:"; val () = (); |
213 "~~~~~ fun locate_input_tactic, args:"; val () = (); |
214 (*----- outcommented during cleanup of args in lucas-interpreter.sml ------------------------\\* ) |
214 (*----- outcommented during cleanup of args in lucas-interpreter.sml ------------------------\\* ) |
215 l = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*false*); |
215 l = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*false*); |
216 (*WAS val NasApp _ =(go_scan_up1 (thy',srls,scr,d) ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]) ) |
216 (*WAS val Reject_Tac1 _ =(go_scan_up1 (thy',srls,scr,d) ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]) ) |
217 ... Assoc ... is correct*) |
217 ... Ackn_Tac1 ... is correct*) |
218 "~~~~~ and go_scan_up1, args:"; val ((ys as (_,_,_,Prog sc,_)), ((E,l,a,v,S,b),ss)) = |
218 "~~~~~ and go_scan_up1, args:"; val ((ys as (_,_,_,Prog sc,_)), ((E,l,a,v,S,b),ss)) = |
219 ((thy',ctxt,srls,scr,d), ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])])); |
219 ((thy',ctxt,srls,scr,d), ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])])); |
220 1 < length l (*true*); |
220 1 < length l (*true*); |
221 val up = drop_last l; |
221 val up = drop_last l; |
222 term2str (go up sc); |
222 term2str (go up sc); |
223 (go up sc); |
223 (go up sc); |
224 (*WAS val Skip1 _ = scan_up1 ys ((E,up,a,v,S,b),ss) (go up sc) |
224 (*WAS val Term_Val1 _ = scan_up1 ys ((E,up,a,v,S,b),ss) (go up sc) |
225 ... ???? ... is correct*) |
225 ... ???? ... is correct*) |
226 "~~~~~ fun scan_up1, args:"; val ((ys as (y,ctxt,s,Prog sc,d)), (is as (E,l,a,v,S,b),ss), |
226 "~~~~~ fun scan_up1, args:"; val ((ys as (y,ctxt,s,Prog sc,d)), (is as (E,l,a,v,S,b),ss), |
227 (Const ("HOL.Let",_) $ _)) = (ys, ((E,up,a,v,S,b),ss:step list), (go up sc)); |
227 (Const ("HOL.Let",_) $ _)) = (ys, ((E,up,a,v,S,b),ss:step list), (go up sc)); |
228 val l = drop_last l; (*comes from e, goes to Abs*) |
228 val l = drop_last l; (*comes from e, goes to Abs*) |
229 val (Const ("HOL.Let",_) $ e $ (Abs (i,T,body))) = go l sc; |
229 val (Const ("HOL.Let",_) $ e $ (Abs (i,T,body))) = go l sc; |
230 val i = mk_Free (i, T); |
230 val i = mk_Free (i, T); |
231 val E = Env.update E (i, v); |
231 val E = Env.update E (i, v); |
232 (*Type error ...: Can't unify _a to pos * pos_ (Incompatible types)*) |
232 (*Type error ...: Can't unify _a to pos * pos_ (Incompatible types)*) |
233 val [(tac_, mout, ctree, pos', xxx)] = ss; |
233 val [(tac_, mout, ctree, pos', xxx)] = ss; |
234 val ss = [(tac_, mout, ctree, pos', []:(pos * pos_) list)]; |
234 val ss = [(tac_, mout, ctree, pos', []:(pos * pos_) list)]; |
235 (*WAS val NasApp iss = scan_dn1 (((y,s),d),Aundef) ((E, l@[R,D], a,v,S,b),ss) body |
235 (*WAS val Reject_Tac1 iss = scan_dn1 (((y,s),d),Aundef) ((E, l@[R,D], a,v,S,b),ss) body |
236 ... Assoc ... is correct*) |
236 ... Ackn_Tac1 ... is correct*) |
237 "~~~~~ fun scan_dn1, args:"; val ((((thy',sr),d),ap), (is as (E,l,a,v,S,b), (m,_,pt,(p,p_),c)::ss), t) = |
237 "~~~~~ fun scan_dn1, args:"; val ((((thy',sr),d),ap), (is as (E,l,a,v,S,b), (m,_,pt,(p,p_),c)::ss), t) = |
238 ((((y,s),d),Aundef), ((E, l@[R,D], a,v,S,b),ss), body); |
238 ((((y,s),d),Aundef), ((E, l@[R,D], a,v,S,b),ss), body); |
239 val (a', STac stac) = handle_leaf "locate" thy' sr (E, (a, v)) t |
239 val (a', STac stac) = handle_leaf "locate" thy' sr (E, (a, v)) t |
240 val ctxt = get_ctxt pt (p,p_) |
240 val ctxt = get_ctxt pt (p,p_) |
241 val p' = lev_on p : pos; |
241 val p' = lev_on p : pos; |