1.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml Wed Apr 29 12:30:51 2020 +0200
1.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml Fri May 01 15:28:40 2020 +0200
1.3 @@ -350,71 +350,13 @@
1.4
1.5 (*[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2] TODO sqrt*)
1.6 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt =..,Check_elementwise "Assumptions")*)
1.7 -"~~~~~ fun me, args:"; val (tac, (p:pos'), _, (pt:ctree)) = (nxt, p, [], pt);
1.8 -"~~~~~ fun Step.by_tactic, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
1.9 -val Applicable.Yes m = applicable_in p pt tac;
1.10 -val Check_elementwise' (trm1, str, (trm2, trms)) = m;
1.11 -UnparseC.term trm1 = "[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2]";
1.12 -str = "Assumptions";
1.13 -UnparseC.term trm2 = "[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2]";
1.14 -UnparseC.terms trms = "[\"lhs (-1 / 8 + -1 * (1 / 8 + sqrt (9 / 16) / 2) / 4 +\n "^
1.15 - " (1 / 8 + sqrt (9 / 16) / 2) ^^^ 2 =\n 0) is_poly_in 1 / 8 + sqrt (9 / 16) / 2\","^
1.16 - "\"lhs (-1 / 8 + -1 * (1 / 8 + sqrt (9 / 16) / 2) / 4 +\n (1 / 8 + sqrt (9 / 16) / 2) ^^^ 2 =\n 0) "^
1.17 - "has_degree_in 1 / 8 + sqrt (9 / 16) / 2 =\n2\","^
1.18 - "\"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\","^
1.19 - "\"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\"]";
1.20 -(*TODO simplify assumptions (sqrt!) and check ERROR in has_degree_in*);
1.21 - (*if*) Tactic.for_specify' m; (*false*)
1.22 -(*loc_solve_ (mI,m) ptp;
1.23 - WAS: not-found-in-program: NotLocatable from Term_Val1 (Const ("List...*)
1.24 -"~~~~~ fun loc_solve_, args:"; val (m, (pt,pos)) = (m, ptp);
1.25 -(*solve m (pt, pos);
1.26 - WAS: not-found-in-program: NotLocatable from Term_Val1 (Const ("List...*)
1.27 -"~~~~~ fun Step_Solve.by_tactic , args:"; val (m, (pt, po as (p,p_))) = (m, (pt, pos));
1.28 -Method.id_empty = get_obj g_metID pt (par_pblobj pt p) (*false*);
1.29 - val thy' = get_obj g_domID pt (par_pblobj pt p);
1.30 - val (is, sc) = resume_prog thy' (p,p_) pt;
1.31 - val d = Rule_Set.empty;
1.32 -(*locate_input_tactic (thy',srls) m (pt,(p,p_)) (sc,d) is;
1.33 - WAS: not-found-in-program: NotLocatable from Term_Val1 (Const ("List...*)
1.34 -"~~~~~ fun locate_input_tactic, args:"; val () = ();
1.35 -(*----- outcommented during cleanup of args in lucas-interpreter.sml ------------------------\\* )
1.36 -l = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*false*);
1.37 -(*WAS val Reject_Tac1 _ =(go_scan_up1 (thy',srls,scr,d) ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]) )
1.38 - ... Accept_Tac1 ... is correct*)
1.39 -"~~~~~ and go_scan_up1, args:"; val ((ys as (_,_,_,Prog sc,_)), ((E,l,a,v,S,b),ss)) =
1.40 - ((thy',ctxt,srls,scr,d), ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]));
1.41 -1 < length l (*true*);
1.42 -val up = drop_last l;
1.43 - UnparseC.term (at_location up sc);
1.44 - (at_location up sc);
1.45 -(*WAS val Term_Val1 _ = scan_up1 ys ((E,up,a,v,S,b),ss) (at_location up sc)
1.46 - ... ???? ... is correct*)
1.47 -"~~~~~ fun scan_up1, args:"; val ((ys as (y,ctxt,s,Prog sc,d)), (is as (E,l,a,v,S,b),ss),
1.48 - (Const ("HOL.Let",_) $ _)) = (ys, ((E,up,a,v,S,b),ss:step list), (at_location up sc));
1.49 - val l = drop_last l; (*comes from e, goes to Abs*)
1.50 - val (Const ("HOL.Let",_) $ e $ (Abs (i,T,body))) = at_location l sc;
1.51 - val i = mk_Free (i, T);
1.52 - val E = Env.update E (i, v);
1.53 -(*Type error ...: Can't unify _a to pos * pos_ (Incompatible types)*)
1.54 -val [(tac_, mout, ctree, pos', xxx)] = ss;
1.55 -val ss = [(tac_, mout, ctree, pos', []:(pos * pos_) list)];
1.56 -(*WAS val Reject_Tac1 iss = scan_dn1 (((y,s),d),ORundef) ((E, l@[R,D], a,v,S,b),ss) body
1.57 - ... Accept_Tac1 ... is correct*)
1.58 -"~~~~~ fun scan_dn1, args:"; val ((((thy',sr),d),ap), (is as (E,l,a,v,S,b), (m,_,pt,(p,p_),c)::ss), t) =
1.59 - ((((y,s),d),ORundef), ((E, l@[R,D], a,v,S,b),ss), body);
1.60 -val (Program.Tac stac, a') = check_leaf "locate" thy' sr (E, (a, v)) t
1.61 - val ctxt = get_ctxt pt (p,p_)
1.62 - val p' = lev_on p : pos;
1.63 -(* WAS val Not_Associated = associate pt d (m, stac)
1.64 - ... Associated ... is correct*)
1.65 -"~~~~~ fun associate, args:"; val (pt, _, (m as Check_elementwise' (consts,_,(consts_chkd,_))),
1.66 - (Const ("Prog_Tac.Check'_elementwise",_) $ consts' $ _)) = (pt, d, m, stac);
1.67 -UnparseC.term consts;
1.68 -UnparseC.term consts';
1.69 -if consts = consts' (*WAS false*) then () else error "Check_elementwise changed";
1.70 -(*[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2] TODO sqrt*)
1.71 -( *----- outcommented during cleanup of args in lucas-interpreter.sml ------------------------//*)
1.72 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.73 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.74 +
1.75 +if p = ([], Res) andalso
1.76 + f2str f = "[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2]" then
1.77 + case nxt of End_Proof' => () | _ => error "(-1/8 + (-1/4)*z + z^^^2 = (0::real)) CHANGED 1"
1.78 +else error "(-1/8 + (-1/4)*z + z^^^2 = (0::real)) CHANGED 2";
1.79
1.80 "----------- equality (2 +(-1)*x + x^^^2 = (0::real)) ----------------------------------------";
1.81 "----------- equality (2 +(-1)*x + x^^^2 = (0::real)) ----------------------------------------";