(* 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";

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

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

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 = term2str 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 = term2str 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 = term2str 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 = term2str t_;

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

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

  (get_pbt ["rational","univariate","equation"]); 

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

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

  (get_pbt ["rational","univariate","equation"]); 

case result of 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 go 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 ["normalize","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", "normalize_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):tac'_), (p:pos'), _, (pt:ctree)) = (nxt, p, c, pt);

val (pt, p) = case locatetac tac (pt,p) of

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

"~~~~~ fun step, 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; (*= []*)

member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= false*)

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

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

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

"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt, pos as (p, _)):ctree * pos'),

  (sc as Prog (h $ body)),

(ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);

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

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

1 < length l; (*true*)

val up = drop_last l;

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

"~~~~~ fun nxt_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, (go up sc), a, v);

ay = Napp_; (*false*)

val up = drop_last l;

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

val i = mk_Free (i, T);

val E = upd_env E (i, v);

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

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

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

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

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

val STac tm = STac (subst_atomic E t);

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

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

"~~~~~ to handle_leaf return val:"; val ((a', STac stac)) = ((NONE, STac (subst_atomic E t)));

val stac' = eval_listexpr_ (assoc_thy thy) srls (subst_atomic (upd_env_opt E (a,v)) stac);

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

"~~~~~ to appy return val:"; val ((a', STac stac)) = ((a', STac stac'));

val (m,m') = stac2tac_ pt (assoc_thy th) stac;

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

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

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

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

        val pp = par_pblobj pt p; 

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

        val thy = assoc_thy thy'

        val metID = (get_obj g_metID pt pp)

        val {crls,...} =  get_met metID

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

                               | Res => get_obj g_result pt p;

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

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

val (bdv, asms) = vp;

term2str bdv = "x";

terms2str asms = (* GOON: asms from rewriting are missing : vvv *)

  ("[\"~ 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 Appl (Check_elementwise' (curr_form, pred, (res, asms))) = applicable_in p''''' pt''''' m''''';

term2str 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;

(*============ inhibit exn WN120316 ==============================================

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

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

(*WN120317.TODO dropped rateq*)

============ inhibit exn WN120316 ==============================================*)

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

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" 

"------------ 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 ["normalize","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;

(* ("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;

(*============ inhibit exn WN120316 ==============================================

if mout2str(f) = "Form' FormKF (~1,EdUndef,0,Nundef,([x = -2, x = 10])" then() 

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

(*WN120317.TODO dropped rateq*)

============ inhibit exn WN120316 ==============================================*)

if f2str f = "[]" then () 

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

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

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

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

(*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 (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; 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 ("Apply_Method", Apply_Method ["RatEq", "solve_rat_equation"]) => ()

| _ => error "55b root specification broken";

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;

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

| _ => error "55b normalize_poly specification broken";

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  f of FormKF "-6 * x + 5 * x ^^^ 2 = 0" => ()

| _ => error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 55b";

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 ("Apply_Method", Apply_Method ["PolyEq", "solve_d2_polyeq_bdvonly_equation"]) => ()

| _ => error "55b normalize_poly specification broken";

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 = 0, x = 6 / 5]";                                                        (*= GUI*)

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

if terms2str (get_assumptions_ pt p) =

("[\"~ matches (?a = 0)\n" ^

   "   ((3 + -1 * x + x ^^^ 2) * x = 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) |\n" ^

   "~ lhs ((3 + -1 * x + x ^^^ 2) * x =\n   " ^

   "    1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) is_poly_in x\"," ^

   "\"x = 6 / 5\"," ^

   "\"x = 0\"," ^

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

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

   "\"9 * x + -6 * x ^^^ 2 + x ^^^ 3 ~= 0\"," ^

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

then () else error "rateq.sml: diff.behav. in I s.87 Bsp 55b [x = 6 / 5], asms";

(*

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

The step-into-source contains an error; this error can be detected by

test --- 'trace_script' from outside 'fun me '---

*)

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

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

    val (pt, p) = case locatetac tac (pt,p) of

		      ("ok", (_, _, ptp)) => ptp  | _ => error "error in test setup";

"~~~~~ step, args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):calcstate)) =

  (p, ((pt, e_pos'),[]));

val pIopt = get_pblID (pt,ip);

ip = ([],Res); (* = false*)

tacis; (* = []*)

member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (* = false*)

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

e_metID = get_obj g_metID pt (par_pblobj pt p); (* = false*)

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

	        val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;

"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt, pos as (p, _)):ctree * pos'),

  (sc as Prog (h $ body)), (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);

l = []; (* = false*)

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

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

1 < length l; (* = true*)

val up = drop_last l; 

(*val (t as Abs (_,_,_)) = *)(go up sc); 

"~~~~~ fun nxt_up, args:"; val (thy, ptp, scr, E, l, ay, (t as Abs (_,_,_)), a, v) =

  (thy, ptp, (Prog sc), E, up, ay, (go up sc), a, v);

term2str t = "%L_La. Check_elementwise L_L {v_v. Assumptions}";

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

  (thy, ptp, scr, E, l, ay, a, v);

1 < length l; (* = true*)

val up = drop_last l; 

(*val (t as Const ("HOL.Let",_) $ e $ (Abs (i,T,b))) = *)(go up sc);

"~~~~~ fun nxt_up, args:"; val (thy, ptp, scr, E, l, ay,

    (t as Const ("HOL.Let",_) $ e $ (Abs (i,T,b))), a, v) = (thy, ptp, (Prog sc), E, up, ay, (go up sc), a, v);

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

(* comment from BEFORE Isabelle2002 --> 2011:

nxt_up thy ptp (Prog sc) E up ay (go up sc) a v;

nstep_up thy ptp scr E l ay a v;

nxt_up thy ptp (Prog sc) E up ay (go up sc) a v;

nstep_up thy ptp sc E l Skip_ a v;

next_tac (thy',srls) (pt,pos) sc is;

nxt_solve_ (pt,ip);

step p ((pt, e_pos'),[]);

*)

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

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

(*============ inhibit exn WN120316 ==============================================

if p = ([], Res) andalso nxt = ("End_Proof'", End_Proof') andalso f2str f = [x = 6 / 5] then ()

else error "rlang.sml: diff.behav. in  Schalk I s.87 Bsp 55b [x = 6 / 5]";

(*WN120317.TODO dropped rateq*)

============ inhibit exn WN120316 ==============================================*)

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

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

    | _ => error "rlang.sml: diff.behav. in  Schalk I s.87 Bsp 55b [x = 6 / 5] 1"

  else error "rlang.sml: diff.behav. in  Schalk I s.87 Bsp 55b [x = 6 / 5] 2";