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 = UnparseC.term 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 = UnparseC.term 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 = UnparseC.term 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 = UnparseC.term 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_; (*= 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 UnparseC.term 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 UnparseC.term 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 UnparseC.term 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;
149 UnparseC.term bdv = "x";
150 UnparseC.terms 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 UnparseC.term 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 =" ^ Tactic.input_to_string (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 "----------- remove x = 0 from [x = 0, x = 6 / 5] ----------------------------------------------";
223 "----------- remove x = 0 from [x = 0, x = 6 / 5] ----------------------------------------------";
224 "----------- remove x = 0 from [x = 0, x = 6 / 5] ----------------------------------------------";
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 spec = ("RatEq",["univariate","equation"],["no_met"]);
229 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, spec)]; (* 0. specify-phase *)
230 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
231 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
232 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
234 (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;
235 (*+*)case nxt of Apply_Method ["RatEq", "solve_rat_equation"] => ()
236 (*+*)| _ => error "55b root specification broken";
238 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* 0. solve-phase*)
239 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
240 val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f = "(3 + -1 * x + x ^^^ 2) * x = 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)";
242 (*+*)if eq_set op = (Ctree.get_assumptions pt p |> map UnparseC.term,
243 (*+*) ["x \<noteq> 0",
244 (*+*) "9 * x + -6 * x ^^^ 2 + x ^^^ 3 \<noteq> 0",
245 (*+*) "x / (x ^^^ 2 - 6 * x + 9) - 1 / (x ^^^ 2 - 3 * x) =\n1 / x is_ratequation_in x"])
246 (*+*)then () else error "assumptions before 1. Subproblem CHANGED";
247 (*+*)if p = ([3], Res) andalso f2str f = "(3 + -1 * x + x ^^^ 2) * x = 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)"
249 (*+*) ((case nxt of Subproblem ("PolyEq", ["normalise", "polynomial", "univariate", "equation"]) => ()
250 (*+*) | _ => error ("S.68, Bsp.: 40 nxt =" ^ Tactic.input_to_string nxt)))
251 (*+*)else error "1. Subproblem -- call changed";
253 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* 1. specify-phase *)
254 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
255 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
256 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
258 (*[4], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;
259 case nxt of Apply_Method ["PolyEq", "normalise_poly"] => ()
260 | _ => error "55b normalise_poly specification broken 1";
262 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* 1. solve-phase *)
263 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
264 val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f = "-6 * x + 5 * x ^^^ 2 = 0";
266 if p = ([4, 3], Res) andalso f2str f = "-6 * x + 5 * x ^^^ 2 = 0"
268 ((case nxt of Subproblem ("PolyEq", ["bdv_only", "degree_2", "polynomial", "univariate", "equation"]) => ()
269 | _ => error ("S.68, Bsp.: 40 nxt =" ^ Tactic.input_to_string nxt)))
271 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* 2. specify-phase *)
272 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
273 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
274 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
276 (*[4, 4], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*\<rightarrow>*)
277 case nxt of Apply_Method ["PolyEq", "solve_d2_polyeq_bdvonly_equation"] => ()
278 | _ => error "55b normalise_poly specification broken 2";
280 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*f = "-6 * x + 5 * x ^^^ 2 = 0"*) (* 2. solve-phase *)
281 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
283 (*[4, 4, 3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*\<rightarrow>Or_to_List*)
284 (*[4, 4, 4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f = "[x = 0, x = 6 / 5]";
285 (*[4, 4, 5], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*\<rightarrow>2. Check_Postcond ["bdv_only", "degree_2", "polynomial", "univariate", "equation"]*)
287 (* *)if eq_set op = ((Ctree.get_assumptions pt p |> map UnparseC.term), [
288 (*0.pre*) "x / (x ^^^ 2 - 6 * x + 9) - 1 / (x ^^^ 2 - 3 * x) =\n1 / x is_ratequation_in x",
289 (*1.pre*) "\<not> matches (?a = 0)\n ((3 + -1 * x + x ^^^ 2) * x =\n 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) \<or>\n"
290 (*1.pre*) ^ "\<not> lhs ((3 + -1 * x + x ^^^ 2) * x =\n 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) is_poly_in x",
291 (*2.pre*) "lhs (-6 * x + 5 * x ^^^ 2 = 0) is_poly_in x",
292 (*2.pre*) "lhs (-6 * x + 5 * x ^^^ 2 = 0) has_degree_in x = 2",
293 (*0.asm*) "x \<noteq> 0",
294 (*0.asm*) "9 * x + -6 * x ^^^ 2 + x ^^^ 3 \<noteq> 0"
296 (* *)then () else error "assumptions at end 2. Subproblem CHANGED";
298 (*[4, 4], Res*)val (p''''',_,f,nxt''''',_,pt''''') = me nxt p [] pt;(*\<rightarrow>1. Check_Postcond ["normalise", "polynomial", "univariate", "equation"]*)
300 (*/--------- step into 2. Check_Postcond SEE .. ----------------------------------------------\*)
301 "----------- rat-equ: remove x = 0 from [x = 0, x = 6 / 5] due to contexts ---------------------";
302 (*\--------- step into 2. Check_Postcond -----------------------------------------------------/*)
304 (*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt''''' p''''' [] pt''''';(*\<rightarrow>IDLE LEGACY: Check_elementwise "Assumptions"*)
305 (*[], Res*)val (p,_,f,nxt,_,pt) = me nxt''''' p''''' [] pt''''';(*\<rightarrow>End_Proof'*)
307 (*/-------- final test -----------------------------------------------------------------------\*)
308 if f2str f = "[x = 6 / 5]" andalso eq_set op = (map UnparseC.term (Ctree.get_assumptions pt p),
309 ["x = 6 / 5", "lhs (-6 * x + 5 * x ^^^ 2 = 0) is_poly_in x",
310 "lhs (-6 * x + 5 * x ^^^ 2 = 0) has_degree_in x = 2",
311 "\<not> matches (?a = 0)\n ((3 + -1 * x + x ^^^ 2) * x =\n 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) \<or>\n\<not> lhs ((3 + -1 * x + x ^^^ 2) * x =\n 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) is_poly_in x",
312 "x \<noteq> 0", "9 * x + -6 * x ^^^ 2 + x ^^^ 3 \<noteq> 0",
313 "x / (x ^^^ 2 - 6 * x + 9) - 1 / (x ^^^ 2 - 3 * x) =\n1 / x is_ratequation_in x"])
314 then () else error "test CHANGED";
317 "----------- ((5*x)/(x - 2) - x/(x+2)=(4::real)), incl. refine ---------------------------------";
318 "----------- ((5*x)/(x - 2) - x/(x+2)=(4::real)), incl. refine ---------------------------------";
319 "----------- ((5*x)/(x - 2) - x/(x+2)=(4::real)), incl. refine ---------------------------------";
320 (*was in test/../usecases.sml*)
321 val fmz = ["equality ((5*x)/(x - 2) - x/(x+2)=(4::real))", "solveFor x","solutions L"];
322 val (dI',pI',mI') = ("RatEq", ["univariate","equation"], ["no_met"]);
323 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
324 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
325 (**)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;(**)
326 (**)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;(**)
327 (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Apply_Method ["RatEq", "solve_rat_equation"]*)
328 (*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Rewrite_Set "RatEq_simplify":*)
330 (*+*)if (get_istate_LI pt p |> Istate.string_of) (* still specify-phase: found_accept = false ---------------------------------> vvvvv*)
331 (*+*) = "Pstate ([\"\n(e_e, 5 * x / (x - 2) - x / (x + 2) = 4)\",\"\n(v_v, x)\"], [], Rule_Set.empty, NONE, \n??.empty, ORundef, false, true)"
332 (*+*)then () else error "rat-eq + subpbl: istate in specify-phase";
334 (*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Rewrite_Set "norm_Rational"*)
336 (*+*)if (get_istate_LI pt p |> Istate.string_of) (* solve-phase: found_accept = true -----------------------------------------------------------------------------------------------> vvvvv*)
337 (*+*) = "Pstate ([\"\n(e_e, 5 * x / (x - 2) - x / (x + 2) = 4)\",\"\n(v_v, x)\"], [R,L,R,L,L,R,R,R], Rule_Set.empty, SOME e_e, \n5 * x / (x + -1 * 2) + -1 * x / (x + 2) = 4, ORundef, true, true)"
338 (*+*)then () else error "rat-eq + subpbl: istate after found_accept";
340 (*[2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Rewrite_Set "RatEq_eliminate"*)
343 (*[3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Subproblem ("PolyEq", ["normalise", "polynomial", "univariate", "equation"])*)
344 (*[4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Model_Problem*)
346 (**)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;(**)
347 (**)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;(**)
348 (**)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;(**)
349 (**)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;(**)
351 (**)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;(**)
352 (**)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;(**)
353 (**)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;(**)
354 (**)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;(**)
356 (*[4,3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Specify_Method ["PolyEq", "solve_d1_polyeq_equation"]*)
357 (*[4,3], Met*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Apply_Method ["PolyEq", "solve_d1_polyeq_equation"]*)
359 (*[4,3,1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Rewrite_Set_Inst (["(''bdv'', x)"], "d1_polyeq_simplify")*)
360 (*[4,3,1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Rewrite_Set "polyeq_simplify"*)
361 (*[4,3,2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Or_to_List*)
362 (*[4,3,3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Check_elementwise "Assumptions"*)
363 (* f = FormKF "[x = -4 / 3]" *)
364 (*[4, 3, 4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Check_Postcond ["degree_1", "polynomial", "univariate", "equation"]*)
365 (*[4, 3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Check_Postcond ["normalise", "polynomial", "univariate", "equation"]*)
366 (*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Check_elementwise "Assumptions"*)
367 (*[5], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Check_Postcond ["rational", "univariate", "equation"]*)
368 (*[], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*End_Proof'*)
370 if p = ([], Res) andalso f2str f = "[x = -4 / 3]"
371 then case nxt of End_Proof' => () | _ => error "rat-eq + subpbl: end CHANGED 1"
372 else error "rat-eq + subpbl: end CHANGED 2";