make Check_elementwise' idle wrt. Calc.T
Note: kept for covering general case in Ctree (step between two Check_Postcond)
1 (* Title: Test for rational equations
2 Author: Richard Lang 2009
3 (c) copyright due to lincense terms.
6 "-----------------------------------------------------------------";
7 "table of contents -----------------------------------------------";
8 "-----------------------------------------------------------------";
9 "----------- pbl: rational, univariate, equation ----------------";
10 "----------- solve (1/x = 5, x) by me ---------------------------";
11 "----------- S.68, Bsp.: 40, ((x)/(x - 8) + (x - 8)/(x) = 26/5)--";
12 "----------- x / (x ^ 2 - 6 * x + 9) - 1 / (x ^ 2 - 3 * x) = 1 /x";
13 "----------- ((5*x)/(x - 2) - x/(x+2)=(4::real)), incl. refine ---------------------------------";
14 "-----------------------------------------------------------------";
15 "-----------------------------------------------------------------";
17 val thy = @{theory "RatEq"};
18 val ctxt = Proof_Context.init_global thy;
20 "------------ pbl: rational, univariate, equation ----------------";
21 "------------ pbl: rational, univariate, equation ----------------";
22 "------------ pbl: rational, univariate, equation ----------------";
23 val t = (Thm.term_of o the o (parse thy)) "(1/b+1/x=1) is_ratequation_in x";
24 val SOME (t_, _) = rewrite_set_ thy false RatEq_prls t;
25 val result = term2str t_;
26 if result <> "True" then error "rateq.sml: new behaviour 1:" else ();
28 val t = (Thm.term_of o the o (parse thy)) "(sqrt(x)=1) is_ratequation_in x";
29 val SOME (t_, _) = rewrite_set_ thy false RatEq_prls t;
30 val result = term2str t_;
31 if result <> "False" then error "rateq.sml: new behaviour 2:" else ();
33 val t = (Thm.term_of o the o (parse thy)) "(x=-1) is_ratequation_in x";
34 val SOME (t_,_) = rewrite_set_ thy false RatEq_prls t;
35 val result = term2str t_;
36 if result <> "False" then error "rateq.sml: new behaviour 3:" else ();
38 val t = (Thm.term_of o the o (parse thy)) "(3 + x^^^2 + 1/(x^^^2+3)=1) is_ratequation_in x";
39 val SOME (t_,_) = rewrite_set_ thy false RatEq_prls t;
40 val result = term2str t_;
41 if result <> "True" then error "rateq.sml: new behaviour 4:" else ();
43 val result = match_pbl ["equality (x=(1::real))","solveFor x","solutions L"]
44 (get_pbt ["rational","univariate","equation"]);
45 case result of NoMatch' _ => () | _ => error "rateq.sml: new behaviour: 5";
47 val result = match_pbl ["equality (3 + x^^^2 + 1/(x^^^2+3)=1)","solveFor x","solutions L"]
48 (get_pbt ["rational","univariate","equation"]);
49 case result of Matches' _ => () | _ => error "rateq.sml: new behaviour: 6";
51 "------------ solve (1/x = 5, x) by me ---------------------------";
52 "------------ solve (1/x = 5, x) by me ---------------------------";
53 "------------ solve (1/x = 5, x) by me ---------------------------";
54 val fmz = ["equality (1/x=(5::real))","solveFor x","solutions L"];
55 val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]);
56 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
57 (* val (p,_,f,nxt,_,pt) = me nxt p [1] pt;------------- now Refine_Tacitly*)
58 (* nxt = ("Model_Problem",Model_Problem ["rational","univariate","equation"]) *)
59 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
60 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
61 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
62 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
64 case nxt of ("Rewrite_Set", Rewrite_Set "RatEq_eliminate") => () | _ => ((*not checked before*));
65 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
67 WN120317.TODO dropped rateq: here "x ~= 0 should at_location to ctxt, but it does not:
68 --- repair NO asms from rls RatEq_eliminate --- shows why.
69 so it needs more effort to find out, how Check_elementwise worked in 2002, see below.
72 (* val nxt = (_,Subproblem ("RatEq",["univariate","equation"] ======= *)
73 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
74 (* val (p,_,f,nxt,_,pt) = me nxt p [1] pt;------------- now Refine_Tacitly*)
75 (*val nxt = ("Model_Problem", Model_Problem ["normalise","polynomial","univariate","equation"])*)
76 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
77 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
78 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
79 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
80 (*val nxt = Apply_Method ["PolyEq", "normalise_poly"])*)
81 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
82 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
83 (* val nxt = (_,Subproblem ("PolyEq",["polynomial","univariate","equation"]=======*)
84 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
85 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
86 (* ("Model_Problem", Model_Problem ["degree_1","polynomial","univariate","equation"])*)
87 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
88 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
89 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
90 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
91 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
92 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
93 val (p''',_,f,nxt''',_,pt''') = me nxt p [1] pt;
94 f2str f = "[x = 1 / 5]";
95 case nxt of ("Check_elementwise", Check_elementwise "Assumptions") => () | _ => ((*not checked before*));
96 "~~~~~ fun me, args:"; val (tac, (p:pos'), _, (pt:ctree)) = (nxt, p, c, pt);
97 val (pt, p) = case Step.by_tactic tac (pt,p) of
98 ("ok", (_, _, ptp)) => ptp | _ => error "--- solve (1/x = 5.. Step.by_tactic";
99 "~~~~~ fun Step.do_next, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []))
100 val pIopt = get_pblID (pt,ip); (*= SOME ["rational", "univariate", "equation"]
101 1-1 associated to metID ["RatEq", "solve_rat_equation"]*)
103 member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= false*)
104 "~~~~~ fun do_next, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
105 val thy' = get_obj g_domID pt (par_pblobj pt p);
106 val (is, sc) = resume_prog thy' (p,p_) pt; (*is: which ctxt?*)
107 "~~~~~ fun find_next_step, args:"; val () = ();
108 (*----- outcommented during cleanup of args in lucas-interpreter.sml ------------------------\\* )
109 "~~~~~ fun go_scan_up, args:"; val (thy, ptp, (Prog sc), E, l, ay, a, v) =
110 (thy, ptp, sc, E, l, true, a, v);
111 1 < length l; (*true*)
112 val up = drop_last l;
113 at_location up sc; (* = Const ("HOL.Let", *)
114 "~~~~~ fun scan_up, args:"; val (thy, ptp, (scr as (Prog sc)), E, l, ay,
115 (t as Const ("HOL.Let",_) $ _), a, v) = (thy, ptp, (Prog sc), E, up, ay, (at_location up sc), a, v);
116 ay = Napp_; (*false*)
117 val up = drop_last l;
118 val (Const ("HOL.Let",_) $ e $ (Abs (i,T,body))) = at_location up sc; (*Const ("Prog_Tac.SubProblem",..*)
119 val i = mk_Free (i, T);
120 val E = Env.update E (i, v);
121 "~~~~~ fun scan_dn, args:"; val ((thy as (th,sr)), (pt, p), E, l, t, a, v) =
122 (thy, ptp, E, (up@[R,D]), body, a, v);
123 "~~~~~ fun check_leaf, args:"; val (call, thy, srls, (E, (a, v)), t) = ("next ", th, sr, (E, (a, v)), t);
124 "~~~~~ fun eval_leaf, args:"; val (E, a, v,
125 (t as (Const ("Prog_Tac.Check'_elementwise",_) $ _ $ _ ))) = (E, a, v, t);
126 val Program.Tac tm = Program.Tac (subst_atomic E t);
127 term2str tm = "Check_elementwise [x = 1 / 5] {v_v. Assumptions}";
128 (* ------ ^^^ ----- ? "x" ?*)
129 "~~~~~ to check_leaf return val:"; val ((Program.Tac stac, a')) = ((Program.Tac (subst_atomic E t), NONE));
130 val stac' = eval_prog_expr (assoc_thy thy) srls (subst_atomic (upd_env_opt E (a,v)) stac);
131 term2str stac' = "Check_elementwise [x = 1 / 5] {v_v. Assumptions}";
132 "~~~~~ to scan_dn return val:"; val ((a', Program.Tac stac)) = ((a', Program.Tac stac'));
133 val m = LItool.tac_from_prog pt (assoc_thy th) stac;
134 case m of Check_elementwise "Assumptions" => () | _ => (); (*m' = Empty_Tac_ ???!??? *);
135 val (p''''', pt''''', m''''') = (p, pt, m);
136 "~~~~~ fun applicable_in, args:"; val ((p,p_), pt, (m as Check_elementwise pred)) = (p, pt, m);
137 member op = [Pbl,Met] p_; (* = false*)
138 val pp = par_pblobj pt p;
139 val thy' = (get_obj g_domID pt pp):theory';
140 val thy = assoc_thy thy'
141 val metID = (get_obj g_metID pt pp)
142 val {crls,...} = get_met metID
143 val (f,asm) = case p_ of Frm => (get_obj g_form pt p , [])
144 | Res => get_obj g_result pt p;
145 term2str f = "[x = 1 / 5]"; (*the current formula*)
146 val vp = (thy2ctxt thy, pred) |-> parseNEW |> the |> mk_set thy pt p f;
147 val (bdv, asms) = vp;
150 terms2str asms = (* asms from rewriting are missing : vvv *)
151 ("[\"<not> matches (?a = 0) (1 = 5 * x) | ~ lhs (1 = 5 * x) is_poly_in x\",\"x = 1 / 5\"," ^
152 "\"lhs (1 + -5 * x = 0) is_poly_in x\",\"lhs (1 + -5 * x = 0) has_degree_in x = 1\"," ^
153 "\"1 / x = 5 is_ratequation_in x\"]");
155 WN120317.TODO dropped rateq: ctxt should contain "x ~= 0 here, but it does not, see above.
158 val Appl (Check_elementwise' (curr_form, pred, (res, asms))) = applicable_in p''''' pt''''' m''''';
159 term2str curr_form = "[x = 1 / 5]";
160 pred = "Assumptions";
161 res = str2term "[]::bool list";
164 val (p,_,f,nxt,_,pt) = me nxt''' p''' [] pt'''; (*<<<----- this caused the error*)
166 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
168 if p = ([], Res) andalso f2str f = "[x = 1 / 5]"
169 then case nxt of ("End_Proof'", End_Proof') => ()
170 | _ => error "rateq.sml: new behaviour: [x = 1 / 5] 1"
171 else error "rateq.sml: new behaviour: [x = 1 / 5] 2";
172 ( *----- outcommented during cleanup of args in lucas-interpreter.sml ------------------------//*)
174 "------------ S.68, Bsp.: 40, ((x)/(x - 8) + (x - 8)/(x) = 26/5)--";
175 "------------ S.68, Bsp.: 40, ((x)/(x - 8) + (x - 8)/(x) = 26/5)--";
176 "------------ S.68, Bsp.: 40, ((x)/(x - 8) + (x - 8)/(x) = 26/5)--";
177 (*EP Schalk_II_p68_n40*)
178 val fmz = ["equality ((x)/(x - 8) + (x - 8)/(x) = 26/(5::real))","solveFor x","solutions L"];
179 val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]);
180 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
181 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
182 (* nxt = ("Model_Problem",Model_Problem ["rational","univariate","equation"])*)
183 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
184 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
185 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
186 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
187 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
188 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
189 (* nxt = ("Subproblem",Subproblem ("RatEq",["univariate","equation"]))*)
190 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
191 (* nxt = ("Model_Problem", Model_Problem ["normalise","polynomial","univariate","equation"])*)
192 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
193 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
194 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
195 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
196 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
198 if p = ([4, 3], Pbl) then ()
201 ("Add_Given", Add_Given "solveFor x") =>
203 PpcKF (Problem [], {Given = [Incompl "solveFor", Correct "equality (320 + 128 * x + -16 * x ^^^ 2 = 0)"], ...}) => ()
204 | _ => error ("S.68, Bsp.: 40 PblObj changed"))
205 | _ => error ("S.68, Bsp.: 40 changed nxt =" ^ tac2str (snd nxt)));
207 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
208 (* ("Subproblem", Subproblem ("PolyEq",["polynomial","univariate","equation"])) *)
209 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
210 (* nxt = ("Model_Problem", Model_Problem
211 ["abcFormula","degree_2","polynomial","univariate","equation"])*)
212 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
213 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
214 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
215 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
216 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
217 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
218 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
219 if p = ([], Res) andalso f2str f = "[]" then ()
220 else error "rateq.sml: new behaviour: [x = -2, x = 10]";
222 "------------ x / (x ^ 2 - 6 * x + 9) - 1 / (x ^ 2 - 3 * x) = 1 /x";
223 "------------ x / (x ^ 2 - 6 * x + 9) - 1 / (x ^ 2 - 3 * x) = 1 /x";
224 "------------ x / (x ^ 2 - 6 * x + 9) - 1 / (x ^ 2 - 3 * x) = 1 /x";
225 (*ER-7*) (*Schalk I s.87 Bsp 55b*)
226 val fmz = ["equality (x/(x^^^2 - 6*x+9) - 1/(x^^^2 - 3*x) =1/x)",
227 "solveFor x","solutions L"];
228 val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]);
229 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
230 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
231 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
232 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
233 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
234 case nxt of ("Apply_Method", Apply_Method ["RatEq", "solve_rat_equation"]) => ()
235 | _ => error "55b root specification broken";
236 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
237 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
238 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
239 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
240 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
241 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
242 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
243 case nxt of ("Apply_Method", Apply_Method ["PolyEq", "normalise_poly"]) => ()
244 | _ => error "55b normalise_poly specification broken 1";
245 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
246 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
247 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
248 if p = ([4, 3], Res) andalso f2str f = "-6 * x + 5 * x ^^^ 2 = 0"
251 ("Subproblem", Subproblem ("PolyEq", ["bdv_only", "degree_2", "polynomial", "univariate", "equation"])) => ()
252 | _ => error ("S.68, Bsp.: 40 nxt =" ^ tac2str (snd nxt))))
254 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
255 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
256 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
257 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
258 case nxt of ("Apply_Method", Apply_Method ["PolyEq", "solve_d2_polyeq_bdvonly_equation"]) => ()
259 | _ => error "55b normalise_poly specification broken 2";
260 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
261 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
262 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
263 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
265 f2str f = "[x = 0, x = 6 / 5]"; (*= GUI*)
266 case snd nxt of Check_elementwise "Assumptions" => () | _ => ((*not checked before*)); (*= GUI*)
267 if terms2str (get_assumptions_ pt p) = "[\"x = 6 / 5\"," ^
269 "\"lhs (-6 * x + 5 * x ^^^ 2 = 0) is_poly_in x\"," ^
270 "\"lhs (-6 * x + 5 * x ^^^ 2 = 0) has_degree_in x = 2\"]"
271 then () else error "rateq.sml: diff.behav. in I s.87 Bsp 55b [x = 6 / 5], asms";
274 WN120317.TODO dropped rateq: ctxt should contain "x ~= 0 here, but it does not.
276 The step-into-source contains an error; this error can be detected by
277 test --- 'trace_script' from outside 'fun me '---
279 val (pt''', p''') = (pt, p);
280 "~~~~~ fun me, args:"; val (tac, (p:pos'), _, (pt:ctree)) = (nxt, p, c, pt);
281 val (pt, p) = case Step.by_tactic tac (pt,p) of
282 ("ok", (_, _, ptp)) => ptp | _ => error "error in test setup";
283 "~~~~~ Step.do_next, args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):calcstate)) =
284 (p, ((pt, e_pos'),[]));
285 val pIopt = get_pblID (pt,ip);
286 ip = ([],Res); (* = false*)
288 member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (* = false*)
289 "~~~~~ and do_next, args:"; val ((ptp as (pt, pos as (p,p_)))) = ((pt,ip));
290 e_metID = get_obj g_metID pt (par_pblobj pt p); (* = false*)
291 val thy' = get_obj g_domID pt (par_pblobj pt p);
292 val (is, sc) = resume_prog thy' (p,p_) pt;
293 "~~~~~ fun find_next_step, args:"; val (thy, (ptp as (pt, pos as (p, _)):ctree * pos'),
294 (sc as Prog (h $ body)), (Pstate (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);
295 (*----- outcommented during cleanup of args in lucas-interpreter.sml ------------------------\\* )
297 "~~~~~ and go_scan_up, args:"; val (thy, ptp, (Prog sc), E, l, ay, a, v) =
298 (thy, ptp, sc, E, l, true, a, v);
299 1 < length l; (* = true*)
300 val up = drop_last l;
301 (*val (t as Abs (_,_,_)) = *)(at_location up sc);
302 "~~~~~ fun scan_up, args:"; val (thy, ptp, scr, E, l, ay, (t as Abs (_,_,_)), a, v) =
303 (thy, ptp, (Prog sc), E, up, ay, (at_location up sc), a, v);
304 term2str t = "%L_La. Check_elementwise L_L {v_v. Assumptions}";
305 "~~~~~ and go_scan_up, args:"; val (thy, ptp, (Prog sc), E, l, ay, a, v) =
306 (thy, ptp, scr, E, l, ay, a, v);
307 1 < length l; (* = true*)
308 val up = drop_last l;
309 (*val (t as Const ("HOL.Let",_) $ e $ (Abs (i,T,b))) = *)(at_location up sc);
310 "~~~~~ fun scan_up, args:"; val (thy, ptp, scr, E, l, ay,
311 (t as Const ("HOL.Let",_) $ e $ (Abs (i,T,b))), a, v) = (thy, ptp, (Prog sc), E, up, ay, (at_location up sc), a, v);
313 term2str t = "let L_La =\n SubProblem (RatEqX, [univariate, equation], [no_met])\n [BOOL e_e, REAL v_v]\nin Check_elementwise L_L {v_v. Assumptions}";
315 (* comment from BEFORE Isabelle2002 --> 2011:
316 scan_up thy ptp (Prog sc) E up ay (at_location up sc) a v;
317 go_scan_up thy ptp scr E l ay a v;
318 scan_up thy ptp (Prog sc) E up ay (at_location up sc) a v;
319 go_scan_up thy ptp sc E l true a v;
320 find_next_step sc (pt,pos) is (*is as (ist, ctxt) ---> ist ctxt*);
321 Step_Solve.do_next (pt,ip);
322 Step.do_next p ((pt, e_pos'),[]);
324 val (p,_,f,nxt,_,pt) = me nxt p''' [1] pt''';
325 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
327 if p = ([], Res) andalso f2str f = "[]"
328 then case nxt of ("End_Proof'", End_Proof') => ()
329 | _ => error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 55b [x = 6 / 5] 1"
330 else error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 55b [x = 6 / 5] 2";
331 ( *----- outcommented during cleanup of args in lucas-interpreter.sml ------------------------//*)
334 "----------- ((5*x)/(x - 2) - x/(x+2)=(4::real)), incl. refine ---------------------------------";
335 "----------- ((5*x)/(x - 2) - x/(x+2)=(4::real)), incl. refine ---------------------------------";
336 "----------- ((5*x)/(x - 2) - x/(x+2)=(4::real)), incl. refine ---------------------------------";
337 (*was in test/../usecases.sml*)
338 val fmz = ["equality ((5*x)/(x - 2) - x/(x+2)=(4::real))", "solveFor x","solutions L"];
339 val (dI',pI',mI') = ("RatEq", ["univariate","equation"], ["no_met"]);
340 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
341 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
342 (**)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;(**)
343 (**)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;(**)
344 (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Apply_Method ["RatEq", "solve_rat_equation"]*)
345 (*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Rewrite_Set "RatEq_simplify":*)
347 (*+*)if (get_istate_LI pt p |> istate2str) (* still specify-phase: found_accept = false ---------------------------------> vvvvv*)
348 (*+*) = "Pstate ([\"\n(e_e, 5 * x / (x - 2) - x / (x + 2) = 4)\",\"\n(v_v, x)\"], [], e_rls, NONE, \n??.empty, ORundef, false, true)"
349 (*+*)then () else error "rat-eq + subpbl: istate in specify-phase";
351 (*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Rewrite_Set "norm_Rational"*)
353 (*+*)if (get_istate_LI pt p |> istate2str) (* solve-phase: found_accept = true -----------------------------------------------------------------------------------------------> vvvvv*)
354 (*+*) = "Pstate ([\"\n(e_e, 5 * x / (x - 2) - x / (x + 2) = 4)\",\"\n(v_v, x)\"], [R,L,R,L,L,R,R,R], e_rls, SOME e_e, \n5 * x / (x + -1 * 2) + -1 * x / (x + 2) = 4, ORundef, true, true)"
355 (*+*)then () else error "rat-eq + subpbl: istate after found_accept";
357 (*[2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Rewrite_Set "RatEq_eliminate"*)
360 (*[3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Subproblem ("PolyEq", ["normalise", "polynomial", "univariate", "equation"])*)
361 (*[4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Model_Problem*)
363 (**)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;(**)
364 (**)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;(**)
365 (**)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;(**)
366 (**)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;(**)
368 (**)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;(**)
369 (**)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;(**)
370 (**)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;(**)
371 (**)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;(**)
373 (*[4,3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Specify_Method ["PolyEq", "solve_d1_polyeq_equation"]*)
374 (*[4,3], Met*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Apply_Method ["PolyEq", "solve_d1_polyeq_equation"]*)
376 (*[4,3,1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Rewrite_Set_Inst (["(''bdv'', x)"], "d1_polyeq_simplify")*)
377 (*[4,3,1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Rewrite_Set "polyeq_simplify"*)
378 (*[4,3,2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Or_to_List*)
379 (*[4,3,3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Check_elementwise "Assumptions"*)
380 (* f = FormKF "[x = -4 / 3]" *)
381 (*[4, 3, 4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Check_Postcond ["degree_1", "polynomial", "univariate", "equation"]*)
382 (*[4, 3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Check_Postcond ["normalise", "polynomial", "univariate", "equation"]*)
383 (*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Check_elementwise "Assumptions"*)
384 (*[5], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Check_Postcond ["rational", "univariate", "equation"]*)
385 (*[], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*End_Proof'*)
387 if p = ([], Res) andalso f2str f = "[x = -4 / 3]"
388 then case nxt of End_Proof' => () | _ => error "rat-eq + subpbl: end CHANGED 1"
389 else error "rat-eq + subpbl: end CHANGED 2";