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 "-----------------------------------------------------------------";
14 "-----------------------------------------------------------------";
16 val thy = @{theory "RatEq"};
17 val ctxt = ProofContext.init_global thy;
19 "------------ pbl: rational, univariate, equation ----------------";
20 "------------ pbl: rational, univariate, equation ----------------";
21 "------------ pbl: rational, univariate, equation ----------------";
22 val t = (term_of o the o (parse thy)) "(1/b+1/x=1) is_ratequation_in x";
23 val SOME (t_, _) = rewrite_set_ thy false RatEq_prls t;
24 val result = term2str t_;
25 if result <> "True" then error "rateq.sml: new behaviour 1:" else ();
27 val t = (term_of o the o (parse thy)) "(sqrt(x)=1) is_ratequation_in x";
28 val SOME (t_, _) = rewrite_set_ thy false RatEq_prls t;
29 val result = term2str t_;
30 if result <> "False" then error "rateq.sml: new behaviour 2:" else ();
32 val t = (term_of o the o (parse thy)) "(x=-1) is_ratequation_in x";
33 val SOME (t_,_) = rewrite_set_ thy false RatEq_prls t;
34 val result = term2str t_;
35 if result <> "False" then error "rateq.sml: new behaviour 3:" else ();
37 val t = (term_of o the o (parse thy)) "(3 + x^^^2 + 1/(x^^^2+3)=1) is_ratequation_in x";
38 val SOME (t_,_) = rewrite_set_ thy false RatEq_prls t;
39 val result = term2str t_;
40 if result <> "True" then error "rateq.sml: new behaviour 4:" else ();
42 val result = match_pbl ["equality (x=(1::real))","solveFor x","solutions L"]
43 (get_pbt ["rational","univariate","equation"]);
44 case result of NoMatch' _ => () | _ => error "rateq.sml: new behaviour: 5";
46 val result = match_pbl ["equality (3 + x^^^2 + 1/(x^^^2+3)=1)","solveFor x","solutions L"]
47 (get_pbt ["rational","univariate","equation"]);
48 case result of Matches' _ => () | _ => error "rateq.sml: new behaviour: 6";
50 "------------ solve (1/x = 5, x) by me ---------------------------";
51 "------------ solve (1/x = 5, x) by me ---------------------------";
52 "------------ solve (1/x = 5, x) by me ---------------------------";
53 val fmz = ["equality (1/x=(5::real))","solveFor x","solutions L"];
54 val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]);
55 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
56 (* val (p,_,f,nxt,_,pt) = me nxt p [1] pt;------------- now Refine_Tacitly*)
57 (* nxt = ("Model_Problem",Model_Problem ["rational","univariate","equation"]) *)
58 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
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;
63 nxt = ("Rewrite_Set", Rewrite_Set "RatEq_eliminate");
64 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
66 WN120317.TODO dropped rateq: here "x ~= 0 should go to ctxt, but it does not:
67 --- repair NO asms from rls RatEq_eliminate --- shows why.
68 so it needs more effort to find out, how Check_elementwise worked in 2002, see below.
71 (* val nxt = (_,Subproblem ("RatEq",["univariate","equation"] ======= *)
72 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
73 (* val (p,_,f,nxt,_,pt) = me nxt p [1] pt;------------- now Refine_Tacitly*)
74 (*val nxt = ("Model_Problem", Model_Problem ["normalize","polynomial","univariate","equation"])*)
75 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
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;
79 (*val nxt = Apply_Method ["PolyEq", "normalize_poly"])*)
80 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
81 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
82 (* val nxt = (_,Subproblem ("PolyEq",["polynomial","univariate","equation"]=======*)
83 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
84 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
85 (* ("Model_Problem", Model_Problem ["degree_1","polynomial","univariate","equation"])*)
86 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
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;
93 f2str f = "[x = 1 / 5]";
94 nxt = ("Check_elementwise", Check_elementwise "Assumptions");
95 "~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), _, (pt:ptree)) = (nxt, p, c, pt);
96 val (pt, p) = case locatetac tac (pt,p) of
97 ("ok", (_, _, ptp)) => ptp | _ => error "--- solve (1/x = 5.. locatetac";
98 "~~~~~ fun step, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []))
99 val pIopt = get_pblID (pt,ip); (*= SOME ["rational", "univariate", "equation"]
100 1-1 associated to metID ["RatEq", "solve_rat_equation"]*)
102 member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= false*)
103 "~~~~~ fun nxt_solve_, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
104 val thy' = get_obj g_domID pt (par_pblobj pt p);
105 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; (*is: which ctxt?*)
106 "~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt, pos as (p, _)):ptree * pos'),
107 (sc as Script (h $ body)),
108 (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);
109 "~~~~~ fun nstep_up, args:"; val (thy, ptp, (Script sc), E, l, ay, a, v) =
110 (thy, ptp, sc, E, l, Skip_, a, v);
111 1 < length l; (*true*)
112 val up = drop_last l;
113 go up sc; (* = Const ("HOL.Let", *)
114 "~~~~~ fun nxt_up, args:"; val (thy, ptp, (scr as (Script sc)), E, l, ay,
115 (t as Const ("HOL.Let",_) $ _), a, v) = (thy, ptp, (Script sc), E, up, ay, (go up sc), a, v);
116 ay = Napp_; (*false*)
117 val up = drop_last l;
118 val (Const ("HOL.Let",_) $ e $ (Abs (i,T,body))) = go up sc; (*Const ("Script.SubProblem",..*)
119 val i = mk_Free (i, T);
120 val E = upd_env E (i, v);
121 "~~~~~ fun appy, 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 handle_leaf, args:"; val (call, thy, srls, E, a, v, t) = ("next ", th, sr, E, a, v, t);
124 "~~~~~ fun subst_stacexpr, args:"; val (E, a, v,
125 (t as (Const ("Script.Check'_elementwise",_) $ _ $ _ ))) = (E, a, v, t);
126 val STac tm = STac (subst_atomic E t);
127 term2str tm = "Check_elementwise [x = 1 / 5] {v_v. Assumptions}";
128 (* ------ ^^^ ----- ? "x" ?*)
129 "~~~~~ to handle_leaf return val:"; val ((a', STac stac)) = ((NONE, STac (subst_atomic E t)));
130 val stac' = eval_listexpr_ (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 appy return val:"; val ((a', STac stac)) = ((a', STac stac'));
133 val (m,m') = stac2tac_ pt (assoc_thy th) stac;
134 m = 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 = (* GOON: asms from rewriting are missing : vvv *)
151 ("[\"~ 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 (*============ inhibit exn WN120316 ==============================================
169 if p = ([], Res) andalso nxt = ("End_Proof'", End_Proof') andalso f2str f = "[x = 1 / 5]" then ()
170 else error "rateq.sml: new behaviour: [x = 1 / 5]";
171 (*WN120317.TODO dropped rateq*)
172 ============ inhibit exn WN120316 ==============================================*)
173 if p = ([], Res) andalso nxt = ("End_Proof'", End_Proof') andalso f2str f = "[]" then ()
174 else error "rateq.sml: new behaviour: [x = 1 / 5]";
176 "------------ S.68, Bsp.: 40, ((x)/(x - 8) + (x - 8)/(x) = 26/5)--";
177 "------------ S.68, Bsp.: 40, ((x)/(x - 8) + (x - 8)/(x) = 26/5)--";
178 "------------ S.68, Bsp.: 40, ((x)/(x - 8) + (x - 8)/(x) = 26/5)--";
179 (*EP Schalk_II_p68_n40*)
180 val fmz = ["equality ((x)/(x - 8) + (x - 8)/(x) = 26/(5::real))","solveFor x","solutions L"];
181 val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]);
182 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
183 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
184 (* nxt = ("Model_Problem",Model_Problem ["rational","univariate","equation"])*)
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 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
190 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
191 (* nxt = ("Subproblem",Subproblem ("RatEq",["univariate","equation"]))*)
192 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
193 (* nxt = ("Model_Problem", Model_Problem ["normalize","polynomial","univariate","equation"])*)
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;
197 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
198 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
199 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
200 (* ("Subproblem", Subproblem ("PolyEq",["polynomial","univariate","equation"])) *)
201 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
202 (* nxt = ("Model_Problem", Model_Problem
203 ["abcFormula","degree_2","polynomial","univariate","equation"])*)
204 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
205 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
206 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
207 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
208 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
209 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
210 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
211 (*============ inhibit exn WN120316 ==============================================
212 if mout2str(f) = "Form' FormKF (~1,EdUndef,0,Nundef,([x = -2, x = 10])" then()
213 else error "rateq.sml: new behaviour: [x = -2, x = 10]";
214 (*WN120317.TODO dropped rateq*)
215 ============ inhibit exn WN120316 ==============================================*)
216 if f2str f = "[]" then ()
217 else error "rateq.sml: new behaviour: [x = -2, x = 10]";
219 "------------ x / (x ^ 2 - 6 * x + 9) - 1 / (x ^ 2 - 3 * x) = 1 /x";
220 "------------ x / (x ^ 2 - 6 * x + 9) - 1 / (x ^ 2 - 3 * x) = 1 /x";
221 "------------ x / (x ^ 2 - 6 * x + 9) - 1 / (x ^ 2 - 3 * x) = 1 /x";
222 (*ER-7*) (*Schalk I s.87 Bsp 55b*)
223 val fmz = ["equality (x/(x^^^2 - 6*x+9) - 1/(x^^^2 - 3*x) =1/x)",
224 "solveFor x","solutions L"];
225 val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]);
226 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
227 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
228 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
229 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
230 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
231 if nxt = ("Apply_Method", Apply_Method ["RatEq", "solve_rat_equation"]) then ()
232 else error "55b root specification broken";
233 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
234 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
235 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
236 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; 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;
240 if nxt = ("Apply_Method", Apply_Method ["PolyEq", "normalize_poly"]) then ()
241 else error "55b normalize_poly specification broken";
242 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
243 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
244 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
245 if f= Form' (FormKF (~1, EdUndef, 0, Nundef, "-6 * x + 5 * x ^^^ 2 = 0")) then()
246 else error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 55b";
247 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
248 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
249 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
250 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
251 if nxt = ("Apply_Method", Apply_Method ["PolyEq", "solve_d2_polyeq_bdvonly_equation"]) then ()
252 else error "55b normalize_poly specification broken";
253 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
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;
258 f2str f = "[x = 0, x = 6 / 5]"; (*= GUI*)
259 snd nxt = Check_elementwise "Assumptions"; (*= GUI*)
260 if terms2str (get_assumptions_ pt p) =
261 ("[\"~ matches (?a = 0)\n" ^
262 " ((3 + -1 * x + x ^^^ 2) * x = 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) |\n" ^
263 "~ lhs ((3 + -1 * x + x ^^^ 2) * x =\n " ^
264 " 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) is_poly_in x\"," ^
267 "\"lhs (-6 * x + 5 * x ^^^ 2 = 0) is_poly_in x\"," ^
268 "\"lhs (-6 * x + 5 * x ^^^ 2 = 0) has_degree_in x = 2\"," ^
269 "\"9 * x + -6 * x ^^^ 2 + x ^^^ 3 ~= 0\"," ^
270 "\"x / (x ^^^ 2 - 6 * x + 9) - 1 / (x ^^^ 2 - 3 * x) =\n1 / x is_ratequation_in x\"]")
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):tac'_), (p:pos'), _, (pt:ptree)) = (nxt, p, c, pt);
281 val (pt, p) = case locatetac tac (pt,p) of
282 ("ok", (_, _, ptp)) => ptp | _ => error "error in test setup";
283 "~~~~~ step, 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 nxt_solve_, 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 (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
293 "~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt, pos as (p, _)):ptree * pos'),
294 (sc as Script (h $ body)), (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);
296 "~~~~~ and nstep_up, args:"; val (thy, ptp, (Script sc), E, l, ay, a, v) =
297 (thy, ptp, sc, E, l, Skip_, a, v);
298 1 < length l; (* = true*)
299 val up = drop_last l;
300 (*val (t as Abs (_,_,_)) = *)(go up sc);
301 "~~~~~ fun nxt_up, args:"; val (thy, ptp, scr, E, l, ay, (t as Abs (_,_,_)), a, v) =
302 (thy, ptp, (Script sc), E, up, ay, (go up sc), a, v);
303 term2str t = "%L_La. Check_elementwise L_L {v_v. Assumptions}";
304 "~~~~~ and nstep_up, args:"; val (thy, ptp, (Script sc), E, l, ay, a, v) =
305 (thy, ptp, scr, E, l, ay, a, v);
306 1 < length l; (* = true*)
307 val up = drop_last l;
308 (*val (t as Const ("HOL.Let",_) $ e $ (Abs (i,T,b))) = *)(go up sc);
309 "~~~~~ fun nxt_up, args:"; val (thy, ptp, scr, E, l, ay,
310 (t as Const ("HOL.Let",_) $ e $ (Abs (i,T,b))), a, v) = (thy, ptp, (Script sc), E, up, ay, (go up sc), a, v);
312 term2str t = "let L_La =\n SubProblem (RatEq', [univariate, equation], [no_met])\n [BOOL e_e, REAL v_v]\nin Check_elementwise L_L {v_v. Assumptions}";
314 (* comment from BEFORE Isabelle2002 --> 2011:
315 nxt_up thy ptp (Script sc) E up ay (go up sc) a v;
316 nstep_up thy ptp scr E l ay a v;
317 nxt_up thy ptp (Script sc) E up ay (go up sc) a v;
318 nstep_up thy ptp sc E l Skip_ a v;
319 next_tac (thy',srls) (pt,pos) sc is;
321 step p ((pt, e_pos'),[]);
323 val (p,_,f,nxt,_,pt) = me nxt p''' [1] pt''';
324 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
326 (*============ inhibit exn WN120316 ==============================================
327 if p = ([], Res) andalso nxt = ("End_Proof'", End_Proof') andalso f2str f = [x = 6 / 5] then ()
328 else error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 55b [x = 6 / 5]";
329 (*WN120317.TODO dropped rateq*)
330 ============ inhibit exn WN120316 ==============================================*)
331 if p = ([], Res) andalso nxt = ("End_Proof'", End_Proof') andalso f2str f = "[]" then ()
332 else error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 55b [x = 6 / 5]";