1 (* Title: "Minisubpbl/530-error-Check_Elementwise.sml"
2 Author: Walther Neuper 1105
3 (c) copyright due to lincense terms.
6 "----------- Minisubplb/530-error-Check_Elementwise.sml ----------";
7 "----------- Minisubplb/530-error-Check_Elementwise.sml ----------";
8 "----------- Minisubplb/530-error-Check_Elementwise.sml ----------";
9 (*see also --- x / (x ^ 2 - 6 * x + 9) - 1 / (x ^ 2 - 3 * x) = 1 /x" by me ---*)
10 val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"];
12 ("Test", ["sqroot-test", "univariate", "equation", "test"],
13 ["Test", "squ-equ-test-subpbl1"]);
14 val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))];
15 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
16 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
17 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
18 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
19 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
20 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
21 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val Apply_Method ["Test", "squ-equ-test-subpbl1"] = nxt;
22 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
23 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
24 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]) = nxt;
25 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
26 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
27 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
28 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
29 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
30 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
31 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
32 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val Apply_Method ["Test", "solve_linear"] = nxt;
34 val return_me_Rewrite_Set_Inst = me nxt p [] pt;
35 (*//------------------ step into me_Rewrite_Set_Inst ---------------------------------------\\*)
36 get_ctxt pt p |> ContextC.is_empty; (*OKfalse*)
37 val ctxt = get_ctxt pt p;
38 val SOME t = ParseC.term_opt ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
39 get_loc pt p |> snd |> ContextC.is_empty; (**OKfalse*)
40 (*\\------------------ step into me_Rewrite_Set_Inst ---------------------------------------//*)
41 val (p,_,f,nxt,_,pt) = return_me_Rewrite_Set_Inst;
42 val Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv") = nxt;
44 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val Rewrite_Set "Test_simplify" = nxt;
46 (*+*)get_ctxt pt p |> ContextC.is_empty; (*false*)
47 (*+*)val ctxt = get_ctxt pt p;
48 (*+*)val SOME t = ParseC.term_opt ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
49 (*+*)get_loc pt p |> snd |> ContextC.is_empty; (*false*)
51 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val Check_Postcond ["LINEAR", "univariate", "equation", "test"] = nxt;
53 val return_me_Rewrite_Set = me nxt p [] pt;
54 (*//------------------ step into me_Rewrite_Set --------------------------------------------\\*)
55 "~~~~~ fun me, args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, [], pt);
56 val (pt, p) = case Step.by_tactic tac (pt,p) of
57 ("ok", (_, _, ptp)) => ptp | _ => error "script.sml Step.by_tactic";
58 Test_Tool.show_pt pt; (*...(([3], Res), [x = 1])]... back in root, OK *)
59 "~~~~~ fun do_next, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []))
60 val pIopt = get_pblID (pt,ip); (*= SOME ["sqroot-test", "univariate", ...]*)
62 member op = [Pbl,Met] p_; (*= false*)
63 "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
64 (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
65 val thy' = get_obj g_domID pt (par_pblobj pt p);
66 val ((ist, ctxt), sc) = LItool.resume_prog (p,p_) pt;
68 val Next_Step (_, _, Check_elementwise' _) =
69 (*case*) LI.find_next_step sc (pt, pos) ist ctxt (*of*);
70 "~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as (pt, (p, _))), Istate.Pstate ist, ctxt)
71 = (sc, (pt, pos), ist, ctxt);
74 scan_to_tactic (prog, (ptp, ctxt)) (Istate.Pstate ist) (*of*);
75 "~~~~~ fun scan_to_tactic , args:"; val ((prog, cct), (Istate.Pstate (ist as {path, ...})))
76 = ((prog, (ptp, ctxt)), (Istate.Pstate ist));
77 (*if*) 0 = length path (*else*);
79 go_scan_up (prog, cct) (trans_scan_up ist |> set_found);
80 "~~~~~ and go_scan_up , args:"; val ((yyy as (prog, _)), (ist as {env, path, found_accept, ...}))
81 = ((prog, cct), (trans_scan_up ist |> set_found));
82 (*if*) 1 < length path (*then*);
84 scan_up yyy (ist |> path_up) (go_up ctxt path prog);
85 "~~~~~ fun scan_up , args:"; val ((yyy as (prog, xxx)), (ist as {found_accept, ...}), (Const (\<^const_name>\<open>Let\<close>(*1*), _) $ _))
86 = (yyy, (ist |> path_up), (go_up ctxt path prog));
87 (*if* ) found_accept = Napp_ ( *else*);
88 val (i, body) = check_Let_up ctxt ist prog;
91 scan_dn xxx (ist |> path_up_down [R, D] |> upd_env i) body (*of*);
92 (*========== a leaf has been found ==========*)
93 "~~~~~ fun scan_dn , args:"; val (((pt, p), ctxt), (ist as {env, eval, ...}), t)
94 = (xxx, (ist |> path_up_down [R, D] |> upd_env i), body);
95 val (Program.Tac stac, a') = (*case*)
96 check_leaf "next " ctxt eval (get_subst ist) t;
98 val Check_elementwise "Assumptions" =
99 LItool.tac_from_prog (pt, p) stac;
100 "~~~~~ fun tac_from_prog , args:"; val (pt, thy, (Const (\<^const_name>\<open>Check_elementwise\<close>, _) $ _ $
101 (set as Const (\<^const_name>\<open>Collect\<close>,_) $ Abs (_,_,pred))))
102 = (pt, (Proof_Context.theory_of ctxt), stac);
103 (*\\------------------ step into me_Rewrite_Set --------------------------------------------//*)
104 val (p,_,f,nxt,_,pt) = return_me_Rewrite_Set;
105 val Check_elementwise "Assumptions" = nxt;
107 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val Check_Postcond ["sqroot-test", "univariate", "equation", "test"] = nxt;