(* Title:  Test for rational equations

   Author: Richard Lang 2009

   (c) copyright due to lincense terms.

*)

"-----------------------------------------------------------------";

"table of contents -----------------------------------------------";

"-----------------------------------------------------------------";

"----------- pbl: rational, univariate, equation ----------------";

"----------- solve (1/x = 5, x) by me ---------------------------";

"----------- S.68, Bsp.: 40, ((x)/(x - 8) + (x - 8)/(x) = 26/5)--";

"----------- x / (x ^ 2 - 6 * x + 9) - 1 / (x ^ 2 - 3 * x) = 1 /x";

"----------- ((5*x)/(x - 2) - x/(x+2)=(4::real)), incl. refine ---------------------------------";

"-----------------------------------------------------------------";

"-----------------------------------------------------------------";

val thy = @{theory "RatEq"};

val ctxt = Proof_Context.init_global thy;

"------------ pbl: rational, univariate, equation ----------------";

"------------ pbl: rational, univariate, equation ----------------";

"------------ pbl: rational, univariate, equation ----------------";

val t = (Thm.term_of o the o (parse thy)) "(1/b+1/x=1) is_ratequation_in  x";

val SOME (t_, _) = rewrite_set_ thy  false RatEq_prls t;

val result = UnparseC.term t_;

if result <>  "True"  then error "rateq.sml: new behaviour 1:" else ();

val t = (Thm.term_of o the o (parse thy)) "(sqrt(x)=1) is_ratequation_in  x";

val SOME (t_, _) = rewrite_set_ thy  false RatEq_prls t;

val result = UnparseC.term t_;

if result <>  "False"  then error "rateq.sml: new behaviour 2:" else ();

val t = (Thm.term_of o the o (parse thy)) "(x=-1) is_ratequation_in x";

val SOME (t_,_) = rewrite_set_ thy  false RatEq_prls t;

val result = UnparseC.term t_;

if result <>  "False"  then error "rateq.sml: new behaviour 3:" else ();

val t = (Thm.term_of o the o (parse thy)) "(3 + x^^^2 + 1/(x^^^2+3)=1) is_ratequation_in x";

val SOME (t_,_) = rewrite_set_ thy  false RatEq_prls t;

val result = UnparseC.term t_;

if result <>  "True"  then error "rateq.sml: new behaviour 4:" else ();

val result = M_Match.match_pbl ["equality (x=(1::real))","solveFor x","solutions L"] 

  (Problem.from_store ["rational","univariate","equation"]); 

case result of M_Match.NoMatch' _  => ()  | _ => error "rateq.sml: new behaviour: 5";

val result = M_Match.match_pbl ["equality (3 + x^^^2 + 1/(x^^^2+3)=1)","solveFor x","solutions L"] 

  (Problem.from_store ["rational","univariate","equation"]); 

case result of M_Match.Matches' _  => ()  | _ => error "rateq.sml: new behaviour: 6";

"------------ solve (1/x = 5, x) by me ---------------------------";

"------------ solve (1/x = 5, x) by me ---------------------------";

"------------ solve (1/x = 5, x) by me ---------------------------";

val fmz = ["equality (1/x=(5::real))","solveFor x","solutions L"];

val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]);

val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

(* val (p,_,f,nxt,_,pt) = me nxt p [1] pt;------------- now Refine_Tacitly*)

(*  nxt = ("Model_Problem",Model_Problem ["rational","univariate","equation"]) *)

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

case nxt of ("Rewrite_Set", Rewrite_Set "RatEq_eliminate") => () | _ => ((*not checked before*));

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

(*

WN120317.TODO dropped rateq: here "x ~= 0 should at_location to ctxt, but it does not:

 --- repair NO asms from rls RatEq_eliminate --- shows why.

so it needs more effort to find out, how Check_elementwise worked in 2002, see below.

*)

(* val nxt = (_,Subproblem ("RatEq",["univariate","equation"] ======= *)

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

(* val (p,_,f,nxt,_,pt) = me nxt p [1] pt;------------- now Refine_Tacitly*)

(*val nxt = ("Model_Problem", Model_Problem ["normalise","polynomial","univariate","equation"])*) 

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

(*val nxt = Apply_Method ["PolyEq", "normalise_poly"])*)

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

(* val nxt = (_,Subproblem ("PolyEq",["polynomial","univariate","equation"]=======*)

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

(*  ("Model_Problem", Model_Problem ["degree_1","polynomial","univariate","equation"])*)

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p''',_,f,nxt''',_,pt''') = me nxt p [1] pt;

f2str f = "[x = 1 / 5]";

case nxt of ("Check_elementwise", Check_elementwise "Assumptions") => () | _ => ((*not checked before*));

"~~~~~ fun me, args:"; val (tac, (p:pos'), _, (pt:ctree)) = (nxt, p, c, pt);

val (pt, p) = case Step.by_tactic tac (pt,p) of

("ok", (_, _, ptp)) => ptp | _ => error "--- solve (1/x = 5.. Step.by_tactic";

"~~~~~ fun Step.do_next, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []))

val pIopt = get_pblID (pt,ip); (*= SOME ["rational", "univariate", "equation"]

                       1-1 associated to metID ["RatEq", "solve_rat_equation"]*)

tacis; (*= []*)

Library.member op = [Pbl,Met] p_; (*= false*)

"~~~~~ fun do_next, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);

val thy' = get_obj g_domID pt (par_pblobj pt p);

val (is, sc) = resume_prog thy' (p,p_) pt; (*is: which ctxt?*)

"~~~~~ fun find_next_step, args:"; val () = ();

(*----- outcommented during cleanup of args in lucas-interpreter.sml ------------------------\\* )

"~~~~~ fun go_scan_up, args:"; val (thy, ptp, (Prog sc), E, l, ay, a, v) =

(thy, ptp, sc, E, l, true, a, v);

1 < length l; (*true*)

val up = drop_last l;

at_location up sc; (* = Const ("HOL.Let", *)

"~~~~~ fun scan_up, args:"; val (thy, ptp, (scr as (Prog sc)), E, l, ay,

 (t as Const ("HOL.Let",_) $ _), a, v) = (thy, ptp, (Prog sc), E, up, ay, (at_location up sc), a, v);

ay = Napp_; (*false*)

val up = drop_last l;

val (Const ("HOL.Let",_) $ e $ (Abs (i,T,body))) = at_location up sc; (*Const ("Prog_Tac.SubProblem",..*)

val i = mk_Free (i, T);

val E = Env.update E (i, v);

"~~~~~ fun scan_dn, args:"; val ((thy as (th,sr)), (pt, p), E, l, t, a, v) =

  (thy, ptp, E, (up@[R,D]), body, a, v);

"~~~~~ fun check_leaf, args:"; val (call, thy, srls, (E, (a, v)), t) = ("next ", th, sr, (E, (a, v)), t);

"~~~~~ fun eval_leaf, args:"; val (E, a, v, 

	  (t as (Const ("Prog_Tac.Check'_elementwise",_) $ _ $ _ ))) = (E, a, v, t);

val Program.Tac tm = Program.Tac (subst_atomic E t);

UnparseC.term tm = "Check_elementwise [x = 1 / 5] {v_v. Assumptions}";

(*                                     ------ ^^^ ----- ? "x" ?*)

"~~~~~ to check_leaf return val:"; val ((Program.Tac stac, a')) = ((Program.Tac (subst_atomic E t), NONE));

val stac' = eval_prog_expr (ThyC.get_theory thy) srls (subst_atomic (upd_env_opt E (a,v)) stac);

UnparseC.term stac' = "Check_elementwise [x = 1 / 5] {v_v. Assumptions}";

"~~~~~ to scan_dn return val:"; val ((a', Program.Tac stac)) = ((a', Program.Tac stac'));

val m = LItool.tac_from_prog pt (ThyC.get_theory th) stac;

case m of Check_elementwise "Assumptions" => () | _ => (); (*m' = Empty_Tac_ ???!??? *);

val (p''''', pt''''', m''''') = (p, pt, m);

"~~~~~ fun check , args:"; val ((p,p_), pt, (m as Check_elementwise pred)) = (p, pt, m);

Library.member op = [Pbl,Met] p_; (* = false*)

        val pp = par_pblobj pt p; 

        val thy' = (get_obj g_domID pt pp):theory';

        val thy = ThyC.get_theory thy'

        val metID = (get_obj g_metID pt pp)

        val {crls,...} =  Method.from_store metID

        val (f,asm) = case p_ of Frm => (get_obj g_form pt p , [])

                               | Res => get_obj g_result pt p;

UnparseC.term f = "[x = 1 / 5]"; (*the current formula*)

        val vp = (ThyC.to_ctxt thy, pred) |-> parseNEW |> the |> mk_set thy pt p f;

val (bdv, asms) = vp;

UnparseC.term bdv = "x";

UnparseC.terms asms = (* asms from rewriting are missing : vvv *)

  ("[\"<not> matches (?a = 0) (1 = 5 * x) | ~ lhs (1 = 5 * x) is_poly_in x\",\"x = 1 / 5\"," ^

   "\"lhs (1 + -5 * x = 0) is_poly_in x\",\"lhs (1 + -5 * x = 0) has_degree_in x = 1\"," ^

   "\"1 / x = 5 is_ratequation_in x\"]");

(*

WN120317.TODO dropped rateq: ctxt should contain "x ~= 0 here, but it does not, see above.

*)

val Applicable.Yes (Check_elementwise' (curr_form, pred, (res, asms))) = check p''''' pt''''' m''''';

UnparseC.term curr_form = "[x = 1 / 5]";

pred = "Assumptions";

res = str2term "[]::bool list";

asms = [];

val (p,_,f,nxt,_,pt) = me nxt''' p''' [] pt'''; (*<<<----- this caused the error*)

f2str f = "[]";

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

if p = ([], Res) andalso f2str f = "[x = 1 / 5]"

then case nxt of ("End_Proof'", End_Proof') => ()

  | _ => error "rateq.sml: new behaviour: [x = 1 / 5] 1"

else error "rateq.sml: new behaviour: [x = 1 / 5] 2";

( *----- outcommented during cleanup of args in lucas-interpreter.sml ------------------------//*)

"------------ S.68, Bsp.: 40, ((x)/(x - 8) + (x - 8)/(x) = 26/5)--";

"------------ S.68, Bsp.: 40, ((x)/(x - 8) + (x - 8)/(x) = 26/5)--";

"------------ S.68, Bsp.: 40, ((x)/(x - 8) + (x - 8)/(x) = 26/5)--";

(*EP Schalk_II_p68_n40*)

val fmz = ["equality ((x)/(x - 8) + (x - 8)/(x) = 26/(5::real))","solveFor x","solutions L"];

val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]);

val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

(* nxt = ("Model_Problem",Model_Problem ["rational","univariate","equation"])*)

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

(* nxt = ("Subproblem",Subproblem ("RatEq",["univariate","equation"]))*)

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

(* nxt = ("Model_Problem", Model_Problem ["normalise","polynomial","univariate","equation"])*)

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

if p = ([4, 3], Pbl) then ()

else

  (case nxt of

    ("Add_Given", Add_Given "solveFor x") =>

      (case f of

        Test_Out.PpcKF (Problem [], {Given = [Incompl "solveFor", Correct "equality (320 + 128 * x + -16 * x ^^^ 2 = 0)"], ...}) => ()

      | _ => error ("S.68, Bsp.: 40 PblObj changed"))

  | _ => error ("S.68, Bsp.: 40 changed nxt =" ^ Tactic.input_to_string (snd nxt)));

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

(* ("Subproblem", Subproblem ("PolyEq",["polynomial","univariate","equation"])) *)

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

(* nxt = ("Model_Problem", Model_Problem

     ["abcFormula","degree_2","polynomial","univariate","equation"])*)

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

if p = ([], Res) andalso f2str f = "[]" then () 

else error "rateq.sml: new behaviour: [x = -2, x = 10]";

"----------- remove x = 0 from [x = 0, x = 6 / 5] ----------------------------------------------";

"----------- remove x = 0 from [x = 0, x = 6 / 5] ----------------------------------------------";

"----------- remove x = 0 from [x = 0, x = 6 / 5] ----------------------------------------------";

(*ER-7*) (*Schalk I s.87 Bsp 55b*)

val fmz = ["equality (x/(x^^^2 - 6*x+9) - 1/(x^^^2 - 3*x) =1/x)",

	   "solveFor x","solutions L"];

val spec = ("RatEq",["univariate","equation"],["no_met"]);

val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, spec)];                          (* 0. specify-phase *)

val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;

(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;

(*+*)case nxt of  Apply_Method ["RatEq", "solve_rat_equation"] => ()

(*+*)| _ => error "55b root specification broken";

val (p,_,f,nxt,_,pt) = me nxt p [] pt;                                         (* 0. solve-phase*)

val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;

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)";

(*+*)if eq_set op = (Ctree.get_assumptions pt p |> map UnparseC.term,

(*+*)  ["x \<noteq> 0", 

(*+*)  "9 * x + -6 * x ^^^ 2 + x ^^^ 3 \<noteq> 0", 

(*+*)  "x / (x ^^^ 2 - 6 * x + 9) - 1 / (x ^^^ 2 - 3 * x) =\n1 / x is_ratequation_in x"])

(*+*)then () else error "assumptions before 1. Subproblem CHANGED";

(*+*)if p = ([3], Res) andalso f2str f = "(3 + -1 * x + x ^^^ 2) * x = 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)"

(*+*)then

(*+*)  ((case nxt of Subproblem ("PolyEq", ["normalise", "polynomial", "univariate", "equation"]) => ()

(*+*)  | _ => error ("S.68, Bsp.: 40 nxt =" ^ Tactic.input_to_string nxt)))

(*+*)else error "1. Subproblem -- call changed";

val (p,_,f,nxt,_,pt) = me nxt p [] pt;                                     (* 1. specify-phase *)

val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;

(*[4], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;

case nxt of Apply_Method ["PolyEq", "normalise_poly"] => ()

| _ => error "55b normalise_poly specification broken 1";

val (p,_,f,nxt,_,pt) = me nxt p [] pt;                                       (* 1. solve-phase *)

val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f = "-6 * x + 5 * x ^^^ 2 = 0";

if p = ([4, 3], Res) andalso f2str f = "-6 * x + 5 * x ^^^ 2 = 0"

then

  ((case nxt of Subproblem ("PolyEq", ["bdv_only", "degree_2", "polynomial", "univariate", "equation"]) => ()

  | _ => error ("S.68, Bsp.: 40 nxt =" ^ Tactic.input_to_string nxt)))

else error "xxx";

val (p,_,f,nxt,_,pt) = me nxt p [] pt;                                     (* 2. specify-phase *)

val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;

(*[4, 4], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*\<rightarrow>*)

case nxt of Apply_Method ["PolyEq", "solve_d2_polyeq_bdvonly_equation"] => ()

| _ => error "55b normalise_poly specification broken 2";

val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*f = "-6 * x + 5 * x ^^^ 2 = 0"*)    (* 2. solve-phase *)

val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;

(*[4, 4, 3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*\<rightarrow>Or_to_List*)

(*[4, 4, 4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f = "[x = 0, x = 6 / 5]";

(*[4, 4, 5], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*\<rightarrow>2. Check_Postcond ["bdv_only", "degree_2", "polynomial", "univariate", "equation"]*)

(*     *)if eq_set op = ((Ctree.get_assumptions pt p |> map UnparseC.term), [

(*0.pre*)  "x / (x ^^^ 2 - 6 * x + 9) - 1 / (x ^^^ 2 - 3 * x) =\n1 / x is_ratequation_in x",

(*1.pre*)  "\<not> matches (?a = 0)\n        ((3 + -1 * x + x ^^^ 2) * x =\n         1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) \<or>\n"

(*1.pre*)    ^ "\<not> lhs ((3 + -1 * x + x ^^^ 2) * x =\n            1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) is_poly_in x",

(*2.pre*)  "lhs (-6 * x + 5 * x ^^^ 2 = 0) is_poly_in x", 

(*2.pre*)  "lhs (-6 * x + 5 * x ^^^ 2 = 0) has_degree_in x = 2",

(*0.asm*)  "x \<noteq> 0", 

(*0.asm*)  "9 * x + -6 * x ^^^ 2 + x ^^^ 3 \<noteq> 0"

(*     *)])

(*     *)then () else error "assumptions at end 2. Subproblem CHANGED";

(*[4, 4], Res*)val (p''''',_,f,nxt''''',_,pt''''') = me nxt p [] pt;(*\<rightarrow>1. Check_Postcond ["normalise", "polynomial", "univariate", "equation"]*)

(*/--------- step into 2. Check_Postcond SEE .. ----------------------------------------------\*)

"----------- rat-equ: remove x = 0 from [x = 0, x = 6 / 5] due to contexts ---------------------";

(*\--------- step into 2. Check_Postcond -----------------------------------------------------/*)

(*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt''''' p''''' [] pt''''';(*\<rightarrow>IDLE LEGACY: Check_elementwise "Assumptions"*)

(*[], Res*)val (p,_,f,nxt,_,pt) = me nxt''''' p''''' [] pt''''';(*\<rightarrow>End_Proof'*)

(*/-------- final test -----------------------------------------------------------------------\*)

if f2str f = "[x = 6 / 5]" andalso eq_set op = (map UnparseC.term (Ctree.get_assumptions pt p),

 ["x = 6 / 5", "lhs (-6 * x + 5 * x ^^^ 2 = 0) is_poly_in x",

  "lhs (-6 * x + 5 * x ^^^ 2 = 0) has_degree_in x = 2",

  "\<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",

  "x \<noteq> 0", "9 * x + -6 * x ^^^ 2 + x ^^^ 3 \<noteq> 0",

  "x / (x ^^^ 2 - 6 * x + 9) - 1 / (x ^^^ 2 - 3 * x) =\n1 / x is_ratequation_in x"])

then () else error "test CHANGED";

"----------- ((5*x)/(x - 2) - x/(x+2)=(4::real)), incl. refine ---------------------------------";

"----------- ((5*x)/(x - 2) - x/(x+2)=(4::real)), incl. refine ---------------------------------";

"----------- ((5*x)/(x - 2) - x/(x+2)=(4::real)), incl. refine ---------------------------------";

(*was in test/../usecases.sml*)

val fmz = ["equality ((5*x)/(x - 2) - x/(x+2)=(4::real))", "solveFor x","solutions L"];

val (dI',pI',mI') = ("RatEq", ["univariate","equation"], ["no_met"]);

val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

(**)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;(**)

(**)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;(**)

(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Apply_Method ["RatEq", "solve_rat_equation"]*)

(*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Rewrite_Set "RatEq_simplify":*)

(*+*)if (get_istate_LI pt p |> Istate.string_of) (* still specify-phase: found_accept = false ---------------------------------> vvvvv*)

(*+*) = "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)"

(*+*)then () else error "rat-eq + subpbl: istate in specify-phase";

(*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Rewrite_Set "norm_Rational"*)

(*+*)if (get_istate_LI pt p |> Istate.string_of) (* solve-phase: found_accept = true -----------------------------------------------------------------------------------------------> vvvvv*)

(*+*) = "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)"

(*+*)then () else error "rat-eq + subpbl: istate after found_accept";

(*[2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Rewrite_Set "RatEq_eliminate"*)

(*^^^ 2*05*)

\<close> ML \<open>

(*[3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Subproblem ("PolyEq", ["normalise", "polynomial", "univariate", "equation"])*)

(*[4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Model_Problem*)

(**)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;(**)

(**)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;(**)

(**)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;(**)

(**)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;(**)

(*^^^ 2*10*)

(**)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;(**)

(**)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;(**)

(**)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;(**)

(**)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;(**)

(*[4,3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Specify_Method ["PolyEq", "solve_d1_polyeq_equation"]*)

(*[4,3], Met*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Apply_Method ["PolyEq", "solve_d1_polyeq_equation"]*)

(*^^^ 2*15*)

(*[4,3,1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Rewrite_Set_Inst (["(''bdv'', x)"], "d1_polyeq_simplify")*)

(*[4,3,1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Rewrite_Set "polyeq_simplify"*)

(*[4,3,2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Or_to_List*)

(*[4,3,3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Check_elementwise "Assumptions"*)

(*                       f = Test_Out.FormKF "[x = -4 / 3]" *)

(*[4, 3, 4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Check_Postcond ["degree_1", "polynomial", "univariate", "equation"]*)

(*[4, 3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Check_Postcond ["normalise", "polynomial", "univariate", "equation"]*)

(*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Check_elementwise "Assumptions"*)

(*[5], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Check_Postcond ["rational", "univariate", "equation"]*)

(*[], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*End_Proof'*)

if p = ([], Res) andalso f2str f = "[x = -4 / 3]"

then case nxt of End_Proof' => () | _ => error "rat-eq + subpbl: end CHANGED 1"

else error "rat-eq + subpbl: end CHANGED 2";