(* Title:  "Specify/specify.sml"

   Author: Walther Neuper

   (c) due to copyright terms

*)

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

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

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

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

"----------- maximum-example: Specify.finish_phase ---------------------------------------------";

"----------- maximum-example: I_Model.complete -------------------------------------------------";

"----------- specify-phase: low level functions ------------------------------------------------";

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

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

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

"----------- maximum-example: Specify.finish_phase ---------------------------------------------";

"----------- maximum-example: Specify.finish_phase ---------------------------------------------";

"----------- maximum-example: Specify.finish_phase ---------------------------------------------";

(*//-------- WAS OUT OF Test UNTIL 200209, ERROR PROBABLY FROM INTRO. OF Isabelle's funpack --\\* )

 val (p,_,f,nxt,_,pt) = 

     CalcTreeTEST 

     [(["fixedValues [r=Arbfix]", "maximum A",

	"valuesFor [a,b]",

	"relations [A=a*b, (a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]",

	"relations [A=a*b, (a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]",

	"relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",

	"boundVariable a", "boundVariable b", "boundVariable alpha",

	"interval {x::real. 0 <= x & x <= 2*r}",

	"interval {x::real. 0 <= x & x <= 2*r}",

	"interval {x::real. 0 <= x & x <= pi}",

	"errorBound (eps=(0::real))"],

       ("DiffApp",["maximum_of", "function"],["DiffApp", "max_by_calculus"])

       )];

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

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

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

 (*nxt = nxt = Add_Find "valuesFor [a]" FIXME.12.03 +handle Inc !*)

 val pits = get_obj g_pbl pt (fst p);

 writeln (I_Model.to_string ctxt pits);

(*[

(0 ,[] ,false ,#Find ,Inc valuesFor ,(??.empty, [])),

(0 ,[] ,false ,#Relate ,Inc relations [] ,(??.empty, [])),

(1 ,[1,2,3] ,true,#Given,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),

(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A]))]*) 

 val (pt,p) = Specify.finish_phase (pt,p);

 val pits = get_obj g_pbl pt (fst p);

 if I_Model.to_string ctxt pits = "[\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),\n(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),\n(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(vs_, [[a],[b]])),\n(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2] ,(rs_, [[A = a * b],[(a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]]))]" 

 then () else error "completetest.sml: new behav. in Specify.finish_phase 3";

 writeln (I_Model.to_string ctxt pits);

(*[

(1 ,[1,2,3] ,true,#Given,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),

(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),

(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(valuesFor, [[a],[b]])),

(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) \<up> 2 + (b / 2)  \<up> 

2 = r \<up> 2] ,(relations, [[A = a * b],[(a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]]))]*)

 val mits = get_obj g_met pt (fst p);

 if I_Model.to_string ctxt mits = "[\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),\n(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),\n(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(vs_, [[a],[b]])),\n(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2] ,(rs_, [[A = a * b],[(a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]])),\n(6 ,[1] ,true ,#undef ,Cor boundVariable a ,(v_, [a])),\n(9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(itv_, [{x. 0 <= x & x <= 2 * r}])),\n(11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(err_, [eps = 0]))]" 

 then () else error "completetest.sml: new behav. in Specify.finish_phase 3";

 writeln (I_Model.to_string ctxt mits);

(*[

(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),

(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),

(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(valuesFor, [[a],[b]])),

(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) \<up> 2 + (b / 2)  \<up> 

2 = r \<up> 2] ,(relations, [[A = a * b],[(a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]])),

(6 ,[1] ,true ,#undef ,Cor boundVariable a ,(boundVariable, [a])),

(9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(interval, [{x.

0 <= x & x <= 2 * r}])),

(11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(errorBound, [eps = 0]))]*)

( *\\-------- WAS OUT OF Test UNTIL 200209, ERROR PROBABLY FROM INTRO. OF Isabelle's funpack --//*)

"----------- maximum-example: I_Model.complete -------------------------------------------------";

"----------- maximum-example: I_Model.complete -------------------------------------------------";

"----------- maximum-example: I_Model.complete -------------------------------------------------";

val c = [];

 val (p,_,f,nxt,_,pt) = 

     CalcTreeTEST 

     [(["fixedValues [r=Arbfix]", "maximum A",

	"valuesFor [a,b]",

	"relations [A=a*b, (a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]",

	"relations [A=a*b, (a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]",

  "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos (alpha::real)]",

	"boundVariable a", "boundVariable b", "boundVariable alpha",

	"interval {x::real. 0 <= x & x <= 2*r}",

	"interval {x::real. 0 <= x & x <= 2*r}",

	"interval {x::real. 0 <= x & x <= pi}",

	"errorBound (eps=(0::real))"],

       ("DiffApp",["maximum_of", "function"],["DiffApp", "max_by_calculus"])

       )];

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

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

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

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

 val (p,_,f,nxt,_,pt) = (me nxt p c pt) (*handle e => OldGoals.print_exn e;*)

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

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

 (*nxt = Specify_Theory "DiffApp"*)

 val (oris, _, _) = get_obj g_origin pt (fst p);

 writeln (O_Model.to_string oris);

(*[

(1, ["1", "2", "3"], #Given,fixedValues, ["[r = Arbfix]"]),

(2, ["1", "2", "3"], #Find,maximum, ["A"]),

(3, ["1", "2", "3"], #Find,valuesFor, ["[a]", "[b]"]),

(4, ["1", "2"], #Relate,relations, ["[A = a * b]", "[(a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]"]),

(5, ["3"], #Relate,relations, ["[A = a * b]", "[a / 2 = r * sin alpha]", "[b / 2 = r * cos alpha]"]),

(6, ["1"], #undef,boundVariable, ["a"]),

(7, ["2"], #undef,boundVariable, ["b"]),

(8, ["3"], #undef,boundVariable, ["alpha"]),

(9, ["1", "2"], #undef,interval, ["{x. 0 <= x & x <= 2 * r}"]),

(10, ["3"], #undef,interval, ["{x. 0 <= x & x <= pi}"]),

(11, ["1", "2", "3"], #undef,errorBound, ["eps = 0"])]*)

 val pits = get_obj g_pbl pt (fst p);

 writeln (I_Model.to_string ctxt pits);

(*[

(1 ,[1,2,3] ,true,#Given ,Cor fixedValues [r = Arbfix],(fix_, [[r = Arbfix]])),

(2 ,[1,2,3] ,true,#Find ,Cor maximum A ,(m_, [A])),

(3 ,[1,2,3] ,true,#Find ,Cor valuesFor [a, b] ,(vs_, [[a, b]])),

(4 ,[1,2] ,true,#Relate ,Cor relations [A = a * b, (a / 2) \<up> 2 + (b / 2)  \<up> 

2 = r \<up> 2] ,(rs_, [[A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]]))]*)

 val mits = get_obj g_met pt (fst p);

 val mits = I_Model.complete oris pits [] 

			((#ppc o MethodC.from_store) ["DiffApp", "max_by_calculus"]);

 writeln (I_Model.to_string ctxt mits);

(*[

(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),

(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),

(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(vs_, [[a, b]])),

(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) \<up> 2 + (b / 2)  \<up> 

2 = r \<up> 2] ,(rs_, [[A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]])),

(6 ,[1] ,true ,#undef ,Cor boundVariable a ,(boundVariable, [a])),

(9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(interval, [{x.

0 <= x & x <= 2 * r}])),

(11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(errorBound, [eps = 0]))]*)

if I_Model.to_string ctxt mits

  = "[\n(1 ,[1, 2, 3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(f_ix, [[r = Arbfix]])), \n(2 ,[1, 2, 3] ,true ,#Find ,Cor maximum A ,(m_m, [A])), \n(3 ,[1, 2, 3] ,true ,#Find ,Cor valuesFor [a, b] ,(v_s, [[a, b]])), \n(4 ,[1, 2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2] ,(r_s, [[A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]])), \n(6 ,[1] ,true ,#undef ,Cor boundVariable a ,(v_v, [a])), \n(9 ,[1, 2] ,true ,#undef ,Cor interval {x. 0 \<le> x \<and> x \<le> 2 * r} ,(i_tv, [{x. 0 \<le> x \<and> x \<le> 2 * r}])), \n(11 ,[1, 2, 3] ,true ,#undef ,Cor errorBound (eps = 0) ,(e_rr, [eps = 0]))]"

then () else error "completetest.sml: new behav. in I_Model.complete 1";

open O_Model;

open I_Model;

open Specify_Step;

"----------- specify-phase: low level functions -----------------------------------------";

"----------- specify-phase: low level functions -----------------------------------------";

"----------- specify-phase: low level functions -----------------------------------------";

val formalise = ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",

	     "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]",

	     "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",

	     "AbleitungBiegelinie dy"];

val references = ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]);

val p = e_pos'; val c = [];

(*[], Pbl*)val (p,_,f,nxt,_,pt) = CalcTreeTEST [(formalise, references)]; (*nxt = Model_Problem*)

(*/------------------- check result of CalcTreeTEST ----------------------------------------\*)

(*+*)val (o_model, ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]), _) =

  get_obj g_origin pt (fst p);

(*+*)if O_Model.to_string o_model = "[\n" ^

  "(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^

  "(2, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^

  "(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^

  "(4, [\"1\"], #Relate, Randbedingungen, [\"[y 0 = 0]\", \"[y L = 0]\", \"[M_b 0 = 0]\", \"[M_b L = 0]\"]), \n" ^

  "(5, [\"1\"], #undef, FunktionsVariable, [\"x\"]), \n" ^

  "(6, [\"1\"], #undef, GleichungsVariablen, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"]), \n" ^

  "(7, [\"1\"], #undef, AbleitungBiegelinie, [\"dy\"])]"

then () else error "[IntegrierenUndKonstanteBestimmen2] O_Model CHANGED";

(*\------------------- check result of CalcTreeTEST ----------------------------------------/*)

(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Given "Traegerlaenge L"*)

(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Given "Streckenlast q_0"*)

(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Find "Biegelinie y"*)

(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Relation "Randbedingungen [y 0 = 0]", ERROR MISSING step: M_b 0 = 0*)

(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Relation "Randbedingungen [y L = 0, M_b 0 = 0, M_b L = 0]"*)

(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Specify_Theory "Biegelinie"*)

(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Specify_Problem ["Biegelinien"]*)

(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Specify_Method ["IntegrierenUndKonstanteBestimmen2"]*)

(*/------------------- step into whole me \<rightarrow>Specify_Method |||||||||||||||||||||||||||||||||\*)

(*[], Met*)val (p''''',_,f,nxt''''',_,pt''''') = me nxt p c pt; (*\<rightarrow>Add_Given "FunktionsVariable x"*)

(*/------------------- initial check for whole me ------------------------------------------\*)

(*+*)val Specify_Method ["IntegrierenUndKonstanteBestimmen2"] = nxt;

(*+*)val Add_Given "FunktionsVariable x" =  nxt''''';

(*+*)val {origin = (o_model, o_refs, _), probl = i_pbl, meth = i_met, spec, ...} =

  Calc.specify_data (pt, p);

(*+*)if o_refs = ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"])

(*+*)then () else error "initial o_refs CHANGED";

(*+*)if O_Model.to_string o_model = "[\n" ^

  "(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^

  "(2, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^

  "(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^

  "(4, [\"1\"], #Relate, Randbedingungen, [\"[y 0 = 0]\", \"[y L = 0]\", \"[M_b 0 = 0]\", \"[M_b L = 0]\"]), \n" ^

  "(5, [\"1\"], #undef, FunktionsVariable, [\"x\"]), \n" ^

  "(6, [\"1\"], #undef, GleichungsVariablen, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"]), \n" ^

  "(7, [\"1\"], #undef, AbleitungBiegelinie, [\"dy\"])]"

(*+*)then () else error "initial o_model CHANGED";

(*+*)if I_Model.to_string @{context} i_pbl = "[\n" ^

  "(1 ,[1] ,true ,#Given ,Cor Traegerlaenge L ,(l_l, [L])), \n" ^

  "(2 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])), \n" ^

  "(3 ,[1] ,true ,#Find ,Cor Biegelinie y ,(b_b, [y])), \n" ^

  "(4 ,[1] ,true ,#Relate ,Cor Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0] ,(r_b, [[y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]]))]"

(*+*)then () else error "initial i_pbl CHANGED";

(*+*)if I_Model.to_string @{context} i_met = "[]"

(*+*)then () else error "initial i_met CHANGED";

(*+*)val (_, ["Biegelinien"], _) = spec;

(*\------------------- initial check for whole me ------------------------------------------/*)

"~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, c, pt);

(*/------------------- step into Step.by_tactic \\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\*)

      val (pt'''''_', p'''''_') = case

      Step.by_tactic tac (pt, p) of ("ok", (_, _, ptp)) => ptp;

(*/------------------- check for entry to Step.by_tactic -----------------------------------\*)

(*+*)val Specify_Method ["IntegrierenUndKonstanteBestimmen2"] = tac;

(*+*)val {origin = (o_model, _, _), ...} = Calc.specify_data (pt, p);

(*+*)if O_Model.to_string o_model = "[\n" ^

  "(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^

  "(2, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^

  "(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^

  "(4, [\"1\"], #Relate, Randbedingungen, [\"[y 0 = 0]\", \"[y L = 0]\", \"[M_b 0 = 0]\", \"[M_b L = 0]\"]), \n" ^

(* these -------vvvvvv must be read from Model_Pattern in *)

  "(5, [\"1\"], #undef, FunktionsVariable, [\"x\"]), \n" ^

  "(6, [\"1\"], #undef, GleichungsVariablen, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"]), \n" ^

  "(7, [\"1\"], #undef, AbleitungBiegelinie, [\"dy\"])]"

(*+*)then () else error "o_model AFTER Specify_Method NOTok CHANGED";

(*\------------------- check for Step.by_tactic --------------------------------------------/*)

"~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));

  val Applicable.Yes tac' = (*case*)

      Step.check tac (pt, p) (*of*);

"~~~~~ fun check , args:"; val (tac, (ctree, pos)) = (tac, (pt, p));

  (*if*) Tactic.for_specify tac (*then*);

Specify_Step.check tac (ctree, pos);

"~~~~~ fun check , args:"; val ((Tactic.Specify_Method mID), (ctree, pos)) = (tac, (ctree, pos));

        val (o_model''''', _, i_model''''') =

           Specify_Step.complete_for mID (ctree, pos);

"~~~~~ fun complete_for , args:"; val (mID, (ctree, pos)) = (mID, (ctree, pos));

    val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, ctxt,

       ...} = Calc.specify_data (ctree, pos);

    val (dI, _, _) = References.select o_refs refs;

    val {ppc = m_patt, pre, prls, ...} = MethodC.from_store mID

    val {origin = (root_model, _, _), ...} = Calc.specify_data (ctree, ([], Pos.Und))

    val (o_model', ctxt') =

   O_Model.complete_for m_patt root_model (o_model, ctxt);

(*/------------------- check entry to O_Model.complete_for -----------------------------------------\*)

(*+*)Model_Pattern.to_string m_patt = "[\"" ^

  "(#Given, (Traegerlaenge, l))\", \"" ^

  "(#Given, (Streckenlast, q))\", \"" ^

  "(#Given, (FunktionsVariable, v))\", \"" ^

  "(#Given, (GleichungsVariablen, vs))\", \"" ^

  "(#Given, (AbleitungBiegelinie, id_abl))\", \"" ^

  "(#Find, (Biegelinie, b))\", \"" ^

  "(#Relate, (Randbedingungen, s))\"]";

(*+*) O_Model.to_string root_model = "[\n" ^ (*.. = o_model for Pos.([], _) *)

  "(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^

  "(2, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^

  "(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^

  "(4, [\"1\"], #Relate, Randbedingungen, [\"[y 0 = 0]\", \"[y L = 0]\", \"[M_b 0 = 0]\", \"[M_b L = 0]\"]), \n" ^

  "(5, [\"1\"], #undef, FunktionsVariable, [\"x\"]), \n" ^

  "(6, [\"1\"], #undef, GleichungsVariablen, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"]), \n" ^

  "(7, [\"1\"], #undef, AbleitungBiegelinie, [\"dy\"])]";

(*\------------------- check entry to O_Model.complete_for -----------------------------------------/*)

"~~~~~ fun complete_for , args:"; val (m_patt, root_model, (o_model, ctxt)) = (m_patt, root_model, (o_model, ctxt));

    val  missing = m_patt |> filter_out

      (fn (_, (descriptor, _)) => (member op = (map #4 o_model) descriptor));

    val add = (root_model

      |> filter

        (fn (_, _, _, descriptor, _) => (member op = (map (fst o snd) missing)) descriptor))

;

    ((o_model @ add)

      |> map (fn (a, b, _, descr, e) => (a, b, the (Model_Pattern.get_field descr m_patt), descr, e))

      |> map (fn (_, b, c, d, e) => (b, c, d, e))      (* for correct enumeration *)

      |> add_id                                        (* for correct enumeration *)

      |> map (fn (a, (b, c, d, e)) => (a, b, c, d, e)), (* for correct enumeration *)

    ctxt |> ContextC.add_constraints (add |> values |> TermC.vars')) (*return from O_Model.complete_for*);

"~~~~~ fun complete_for \<longrightarrow>fun Specify_Step.complete_for , return:"; val (o_model', ctxt') =

    ((o_model @ add)

      |> map (fn (a, b, _, descr, e) => (a, b, the (Model_Pattern.get_field descr m_patt), descr, e))

      |> map (fn (_, b, c, d, e) => (b, c, d, e))      (* for correct enumeration *)

      |> add_id                                        (* for correct enumeration *)

      |> map (fn (a, (b, c, d, e)) => (a, b, c, d, e)), (* for correct enumeration *)

    ctxt |> ContextC.add_constraints (add |> values |> TermC.vars'));

(*/------------------- check of result from O_Model.complete_for -----------------------------------\*)

(*+*)if O_Model.to_string o_model' = "[\n" ^

  "(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^

  "(2, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^

  "(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^

  "(4, [\"1\"], #Relate, Randbedingungen, [\"[y 0 = 0]\", \"[y L = 0]\", \"[M_b 0 = 0]\", \"[M_b L = 0]\"]), \n" ^

  "(5, [\"1\"], #Given, FunktionsVariable, [\"x\"]), \n" ^

  "(6, [\"1\"], #Given, GleichungsVariablen, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"]), \n" ^

  "(7, [\"1\"], #Given, AbleitungBiegelinie, [\"dy\"])]"

(*+*)then () else error "O_Model.complete_for: result o_model CHANGED";

(*\------------------- check of result from O_Model.complete_for -----------------------------------/*)

    val thy = ThyC.get_theory dI

    val (_, (i_model, _)) = M_Match.match_itms_oris thy i_prob (m_patt, pre, prls) o_model';

  (o_model', ctxt', i_model) (*return from Specify_Step.complete_for*);

"~~~~~ fun complete_for \<longrightarrow>fun Specify_Step.check , return:"; val (o_model, _, i_model) =

  (o_model', ctxt', i_model);

   Applicable.Yes (Tactic.Specify_Method' (mID, o_model, i_model)) (*return from Specify_Step.check*);

"~~~~~ fun Specify_Step.check \<longrightarrow>fun Step.check \<longrightarrow>fun Step.by_tactic , return:"; val (Applicable.Yes tac') =

  (Applicable.Yes (Tactic.Specify_Method' (mID, o_model, i_model)));

	    (*if*) Tactic.for_specify' tac' (*then*);

  val ("ok", ([], [], (_, _))) =

Step_Specify.by_tactic tac' ptp;

"~~~~~ fun by_tactic , args:"; val ((Tactic.Specify_Method' (mID, _, _)), (pt,pos as (p, _))) =

  (tac', ptp);

(*NEW*) val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, ctxt,

(*NEW*)    ...} = Calc.specify_data (pt, pos);

(*NEW*) val (dI, _, mID) = References.select o_refs refs;

(*NEW*) val {ppc = m_patt, pre, prls, ...} = MethodC.from_store mID

(*NEW*) val {origin = (root_model, _, _), ...} = Calc.specify_data (pt, ([], Und))

(*NEW*) val (o_model', ctxt') = O_Model.complete_for m_patt root_model (o_model, ctxt)

(*NEW*) val thy = ThyC.get_theory dI

(*NEW*) val (_, (i_model, _)) = M_Match.match_itms_oris thy i_prob (m_patt, pre, prls) o_model';

(*NEW*) val (pos, _, _, pt) = Specify_Step.add (Tactic.Specify_Method' (mID, o_model', i_model))

(*NEW*)   (Istate_Def.Uistate, ctxt') (pt, pos)

(*/------------------- check result of Step_Specify.by_tactic ------------------------------\*)

(*+*)val {origin = (o_model, _, _), meth, ...} = Calc.specify_data (pt, pos);

(*+*)O_Model.to_string o_model = "[\n" ^

  "(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^

  "(2, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^

  "(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^

  "(4, [\"1\"], #Relate, Randbedingungen, [\"[y 0 = 0]\", \"[y L = 0]\", \"[M_b 0 = 0]\", \"[M_b L = 0]\"]), \n" ^

  "(5, [\"1\"], #undef, FunktionsVariable, [\"x\"]), \n" ^

  "(6, [\"1\"], #undef, GleichungsVariablen, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"]), \n" ^

  "(7, [\"1\"], #undef, AbleitungBiegelinie, [\"dy\"])]";

(* ERROR ------- \<up> \<up> CORRECTED TO #Given *)

(*+*)if I_Model.to_string @{context} meth = "[\n" ^

  "(1 ,[1] ,true ,#Given ,Cor Traegerlaenge L ,(l_l, [L])), \n" ^

  "(2 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])), \n" ^

  "(3 ,[1] ,true ,#Find ,Cor Biegelinie y ,(b_b, [y])), \n" ^

  "(4 ,[1] ,true ,#Relate ,Cor Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0] ,(r_b, [[y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]])), \n" ^

  "(5 ,[1] ,false ,#Given ,Mis FunktionsVariable fun_var), \n" ^

  "(6 ,[1] ,false ,#Given ,Mis GleichungsVariablen vs), \n" ^

  "(7 ,[1] ,false ,#Given ,Mis AbleitungBiegelinie id_der)]"

(*+*)then () else error "result of Step_Specify.by_tactic o_model CHANGED";

(*\------------------- check result of Step_Specify.by_tactic ------------------------------/*)

(*\------------------- step into Step.by_tactic /////////////////////////////////////////////*)

val (_, ([(Add_Given "FunktionsVariable x", _, _)], _, _)) =

   Step.do_next p'''''_' ((pt'''''_', Pos.e_pos'), []) (*of*);

(*/------------------- step into Step.do_next \\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\*)

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

  (p'''''_', ((pt'''''_', Pos.e_pos'), []));

  (*if*) Pos.on_calc_end ip (*else*);

     val (_, probl_id, _) = Calc.references (pt, p);

     val _ = (*case*) tacis (*of*);

       (*if*) probl_id = Problem.id_empty (*else*);

val (_, ([(Add_Given "FunktionsVariable x", _, _)], _, _)) =

         switch_specify_solve p_ (pt, ip);

"~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));

      (*if*) Pos.on_specification ([], state_pos) (*then*);

val ("ok", ([(Add_Given "FunktionsVariable x", _, _)], [], (pt'''''_'', p'''''_''))) =

           specify_do_next (pt, input_pos);

(*/------------------- check result of specify_do_next -------------------------------------\*)

(*+*)val {origin = (ooo_mod, _, _), meth, ...} =  Calc.specify_data (pt'''''_'', p'''''_'');

(*+*)if O_Model.to_string ooo_mod = "[\n" ^

  "(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^

  "(2, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^

  "(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^

  "(4, [\"1\"], #Relate, Randbedingungen, [\"[y 0 = 0]\", \"[y L = 0]\", \"[M_b 0 = 0]\", \"[M_b L = 0]\"]), \n" ^

  "(5, [\"1\"], #Given, FunktionsVariable, [\"x\"]), \n" ^

  "(6, [\"1\"], #Given, GleichungsVariablen, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"]), \n" ^

  "(7, [\"1\"], #Given, AbleitungBiegelinie, [\"dy\"])]"

(*+*)then () else error "result of Step_Specify.by_tactic o_model CHANGED";

(*+*)if I_Model.to_string @{context} meth = "[\n" ^

  "(1 ,[1] ,true ,#Given ,Cor Traegerlaenge L ,(l_l, [L])), \n" ^

  "(2 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])), \n" ^

  "(3 ,[1] ,true ,#Find ,Cor Biegelinie y ,(b_b, [y])), \n" ^

  "(4 ,[1] ,true ,#Relate ,Cor Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0] ,(r_b, [[y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]])), \n" ^

  "(5 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(fun_var, [x])), \n" ^

  "(6 ,[1] ,false ,#Given ,Mis GleichungsVariablen vs), \n" ^

  "(7 ,[1] ,false ,#Given ,Mis AbleitungBiegelinie id_der)]"

(*+*)then () else error "result of Step_Specify.by_tactic i_model CHANGED";

(*\------------------- check result of specify_do_next -------------------------------------/*)

"~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);

(**)val (_, (p_', Add_Given "FunktionsVariable x")) =(**)

   Specify.find_next_step ptp;

"~~~~~ fun find_next_step , args:"; val (pt, (p, p_)) = (ptp);

(*.NEW*)val pblobj as {meth = met, origin = origin as (oris, (dI', pI', mI'), _),

(*.NEW*)	  probl = pbl, spec = (dI, pI, mI), ctxt, ...} = Calc.specify_data (pt, (p, p_));

(*.NEW*)(*if*) Ctree.just_created (pt, (p, p_)) andalso origin <> Ctree.e_origin (*else*);

        val cpI = if pI = Problem.id_empty then pI' else pI;

  	    val cmI = if mI = MethodC.id_empty then mI' else mI;

  	    val {ppc = pbt, prls, where_, ...} = Problem.from_store cpI;

  	    val (preok, pre) = Pre_Conds.check prls where_ pbl 0;

  	    (*FIXME.WN0308:    ~~~~~: just check true in itms of pbl/met?*)

        val mpc = (#ppc o MethodC.from_store) cmI

        val Pos.Met = (*case*) p_ (*of*);

      val NONE = (*case*) find_first (I_Model.is_error o #5) met (*of*);

(*/------------------- check within find_next_step -----------------------------------------\*)

(*+*)Model_Pattern.to_string (MethodC.from_store mI' |> #ppc) = "[\"" ^

  "(#Given, (Traegerlaenge, l))\", \"" ^

  "(#Given, (Streckenlast, q))\", \"" ^

  "(#Given, (FunktionsVariable, v))\", \"" ^   (* <---------- take m_field from here !!!*)

  "(#Given, (GleichungsVariablen, vs))\", \"" ^

  "(#Given, (AbleitungBiegelinie, id_abl))\", \"" ^

  "(#Find, (Biegelinie, b))\", \"" ^

  "(#Relate, (Randbedingungen, s))\"]";

(*\------------------- check within find_next_step -----------------------------------------/*)

    (*case*) item_to_add (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) oris mpc met (*of*);

"~~~~~ ~ fun item_to_add , args:"; val (thy, oris, _, itms) =

  ((ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)), oris, mpc, met);

(*OLD*)fun testr_vt v ori = member op= (#2 (ori : O_Model.single)) v (**)andalso (#3 ori) <> "#undef"(**)

      fun testi_vt v itm = member op= (#2 (itm : I_Model.single)) v

      fun test_id ids r = member op= ids (#1 (r : O_Model.single))

      fun test_subset itm (_, _, _, d, ts) = 

        (I_Model.d_in (#5 (itm: I_Model.single))) = d andalso subset op = (I_Model.ts_in (#5 itm), ts)

      fun false_and_not_Sup (_, _, false, _, I_Model.Sup _) = false

        | false_and_not_Sup (_, _, false, _, _) = true

        | false_and_not_Sup _ = false

      val v = if itms = [] then 1 else I_Model.max_vt itms

      val vors = if v = 0 then oris else filter (testr_vt v) oris  (* oris..vat *)

      val vits =

        if v = 0

        then itms                                 (* because of dsc without dat *)

  	    else filter (testi_vt v) itms;                             (* itms..vat *)

      val icl = filter false_and_not_Sup vits;                    (* incomplete *)

(*/------------------- check within item_to_add --------------------------------------------\*)

(*+*)if I_Model.to_string @{context} icl = "[\n" ^                      (*.. values*)

  "(5 ,[1] ,false ,#Given ,Mis FunktionsVariable fun_var), \n" ^

  "(6 ,[1] ,false ,#Given ,Mis GleichungsVariablen vs), \n" ^

  "(7 ,[1] ,false ,#Given ,Mis AbleitungBiegelinie id_der)]"

(*+*)then () else error "icl within item_to_add CHANGED";

(*+*)if O_Model.to_string vors = "[\n" ^

  "(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^

  "(2, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^

  "(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^

  "(4, [\"1\"], #Relate, Randbedingungen, [\"[y 0 = 0]\", \"[y L = 0]\", \"[M_b 0 = 0]\", \"[M_b L = 0]\"]), \n" ^

  "(5, [\"1\"], #Given, FunktionsVariable, [\"x\"]), \n" ^

  "(6, [\"1\"], #Given, GleichungsVariablen, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"]), \n" ^

  "(7, [\"1\"], #Given, AbleitungBiegelinie, [\"dy\"])]"

(*+*)then () else error "vors within item_to_add CHANGED";

(*+*)if I_Model.to_string @{context} itms = "[\n" ^

  "(1 ,[1] ,true ,#Given ,Cor Traegerlaenge L ,(l_l, [L])), \n" ^

  "(2 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])), \n" ^

  "(3 ,[1] ,true ,#Find ,Cor Biegelinie y ,(b_b, [y])), \n" ^

  "(4 ,[1] ,true ,#Relate ,Cor Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0] ,(r_b, [[y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]])), \n" ^

  "(5 ,[1] ,false ,#Given ,Mis FunktionsVariable fun_var), \n" ^   (*.. still NOT ,true ,#Given , Cor*)

  "(6 ,[1] ,false ,#Given ,Mis GleichungsVariablen vs), \n" ^

  "(7 ,[1] ,false ,#Given ,Mis AbleitungBiegelinie id_der)]"

(*+*)then () else error "i_model  within item_to_add CHANGED";

(*\------------------- check within item_to_add --------------------------------------------/*)

      (*if*) icl = [] (*else*);

        val SOME ori =(*case*) find_first (test_subset (hd icl)) vors (*of*);

(*+*)val (5, [1], "#Given", Const (\<^const_name>\<open>FunktionsVariable\<close>, _), [Free ("x", _)]) = ori

(*+*)val SOME ("#Given", "FunktionsVariable x") =

        SOME

     (I_Model.geti_ct thy ori (hd icl)) (*return from item_to_add*);

"~~~~~ ~~ fun geti_ct , args:"; val (thy, (_, _, _, d, ts), (_, _, _, fd, itm_)) = (thy, ori, (hd icl));

val rrrrr =

  (fd, ((UnparseC.term_in_thy thy) o Input_Descript.join)

    (d, subtract op = (ts_in itm_) ts)) (*return from geti_ct*);

"~~~~~ ~~ from fun geti_ct \<longrightarrow>fun item_to_add \<longrightarrow>fun find_next_step , return:"; val (SOME (fd, ct')) =

    (SOME rrrrr);

  ("dummy", (Pos.Met, P_Model.mk_additem fd ct')) (*return from find_next_step*);

(*+*)val Add_Given "FunktionsVariable x" = P_Model.mk_additem fd ct';

"~~~~~ from fun find_next_step \<longrightarrow>fun specify_do_next , return:"; val (_, (p_', tac)) =

  ("dummy", (Pos.Met, P_Model.mk_additem fd ct'));

    val ist_ctxt =  Ctree.get_loc pt (p, p_)

    val _ = (*case*) tac (*of*);

      ("dummy",

Step_Specify.by_tactic_input tac (pt, (p, p_'))) (*return from specify_do_next*);

"~~~~~ fun by_tactic_input , args:"; val ((Tactic.Add_Given ct), ptp) =

  (tac, (pt, (p, p_')));

  val ("ok", ([(Add_Given "FunktionsVariable x", _, _)], _, _)) =

     Specify.by_Add_ "#Given" ct ptp (*return from by_tactic_input*);

"~~~~~ ~ fun by_Add_ , args:"; val (m_field, ct, (pt, pos as (_, p_))) = ("#Given", ct, ptp);

    val (met, oris, (_, pI', mI'), pbl, (_, pI, mI), ctxt) = SpecificationC.get_data (pt, pos);

       (*if*) p_ = Pos.Met (*then*);

    val (i_model, m_patt) = (met,

           (if mI = MethodC.id_empty then mI' else mI) |> MethodC.from_store |> #ppc)

val Add (5, [1], true, "#Given", Cor ((Const (\<^const_name>\<open>FunktionsVariable\<close>, _), [Free ("x", _)]), (Free ("fun_var", _), [Free ("x", _)]))) =

      (*case*)

   I_Model.check_single ctxt m_field oris i_model m_patt ct (*of*);

"~~~~~ ~~ fun check_single , args:"; val (ctxt, m_field, o_model, i_model, m_patt, str) =

  (ctxt, m_field, oris, i_model, m_patt, ct);

(*.NEW*)      val SOME (t as (descriptor $ _)) = (*case*) TermC.parseNEW ctxt str (*of*);

(*.NEW*)   val SOME m_field = (*case*) Model_Pattern.get_field descriptor m_patt (*of*);

val ("", (5, [1], "#Given", Const (\<^const_name>\<open>FunktionsVariable\<close>, _), [Free ("x", _)]), [Free ("x", _)]) =

          (*case*)

       O_Model.is_known ctxt m_field o_model t (*of*);

"~~~~~ ~~~ fun is_known , args:"; val (ctxt, sel, ori, t) = (ctxt, m_field, o_model, t);

    val ots = ((distinct op =) o flat o (map #5)) ori

    val oids = ((map (fst o dest_Free)) o (distinct op =) o flat o (map TermC.vars)) ots

    val (d, ts) = Input_Descript.split t

    val ids = map (fst o dest_Free) (((distinct op =) o (flat o (map TermC.vars))) ts);

    (*if*) (subtract op = oids ids) <> [] (*else*);

	    (*if*) d = TermC.empty (*else*);

	      (*if*) member op = (map #4 ori) d (*then*);

                seek_oridts ctxt sel (d, ts) ori;

"~~~~~ ~~~~ fun seek_oridts , args:"; val (ctxt, m_field, (descript, vals), ((id, vat, m_field', descript', vals') :: oris)) =

  (ctxt, sel, (d, ts), ori);

(*/------------------- check within seek_oridts --------------------------------------------\*)

(*+*)val Add_Given "FunktionsVariable x" = tac;

(*+*)m_field = "#Given";

(*+*)val Const (\<^const_name>\<open>FunktionsVariable\<close>, _) = descript;

(*+*)val [Free ("x", _)] = vals;

(*+*)O_Model.to_string ori = "[\n" ^

  "(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^

  "(2, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^

  "(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^

  "(4, [\"1\"], #Relate, Randbedingungen, [\"[y 0 = 0]\", \"[y L = 0]\", \"[M_b 0 = 0]\", \"[M_b L = 0]\"]), \n" ^

  "(5, [\"1\"], #undef, FunktionsVariable, [\"x\"]), \n" ^

  "(6, [\"1\"], #undef, GleichungsVariablen, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"]), \n" ^

  "(7, [\"1\"], #undef, AbleitungBiegelinie, [\"dy\"])]";

(*+*)val (id, vat, m_field', descript', vals') = nth 5 ori

(*+*)val (5, [1], "#Given", Const (\<^const_name>\<open>FunktionsVariable\<close>, _), [Free ("x", _)]) =

  (id, vat, m_field', descript', vals')

(*\------------------- check within seek_oridts --------------------------------------------/*)

(*-------------------- stop step into whole me ----------------------------------------------*)

(*\------------------- step into whole me \<rightarrow>Specify_Method |||||||||||||||||||||||||||||||||/*)

(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt''''' p''''' c pt'''''; (*\<rightarrow>Add_Given "GleichungsVariablen [c, c_2, c_3, c_4]"*)

(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Given "AbleitungBiegelinie dy"*)

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

(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Model_Problem*)

(*/------------------- check entry to me Model_Problem -------------------------------------\*)

(*+*)val ([1], Pbl) = p;

(*+*)val (o_model, ("Biegelinie", ["vonBelastungZu", "Biegelinien"], ["Biegelinien", "ausBelastung"]), _) =

  get_obj g_origin pt (fst p);

(*+*)if O_Model.to_string o_model = "[\n" ^

  "(1, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^

  "(2, [\"1\"], #Given, FunktionsVariable, [\"x\"]), \n" ^

  "(3, [\"1\"], #Find, Funktionen, [\"funs'''\"])]"

(*

.. here the O_Model does NOT know, which MethodC will be chosen,

so "belastung_zu_biegelinie q__q v_v id_fun id_abl" is NOT known,

"id_fun" and "id_abl" are NOT missing.

*)

then () else error "[Biegelinien, ausBelastung] initial O_Model CHANGED";

(*\------------------- check entry to me Model_Problem -------------------------------------/*)

(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Given "Streckenlast q_0"*)

(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Given "FunktionsVariable x"*)

(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Find "Funktionen funs'''":*)

(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Specify_Theory "Biegelinie"*)

(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Specify_Problem ["vonBelastungZu", "Biegelinien"]*)

(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Specify_Method ["Biegelinien", "ausBelastung"]*)

(*[1], Met*)val (p''''',_,f,nxt''''',_,pt''''') = me nxt p c pt; (*\<rightarrow>Add_Given "Biegelinie y"*)

(*/------------------- step into me\<rightarrow>Add_Given "Biegelinie y" ||||||||||||||||||||||||||||||\*)

(*+*)val Specify_Method ["Biegelinien", "ausBelastung"] = nxt;

(*+*)(* by \<up> \<up> \<up> \<up>   "id_fun" and "id_abl" must be requested: PUT THEM INTO O_Model*)

"~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, c, pt);

  val ("ok", ([], [], (_, _))) = (*case*)

      Step.by_tactic tac (pt, p) (*of*);

"~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));

  val Applicable.Yes tac' = (*case*) check tac (pt, p) (*of*);

	    (*if*) Tactic.for_specify' tac' (*then*);

  val ("ok", ([], [], (_, _))) =

Step_Specify.by_tactic tac' ptp;

(*/------------------- initial check for Step_Specify.by_tactic ----------------------------\*)

(*+*)val (o_model, ("Biegelinie", ["vonBelastungZu", "Biegelinien"], ["Biegelinien", "ausBelastung"]), _) =

  get_obj g_origin pt (fst p);

(*+*)if O_Model.to_string o_model = "[\n" ^                                         

  "(1, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^

  "(2, [\"1\"], #Given, FunktionsVariable, [\"x\"]), \n" ^

  "(3, [\"1\"], #Find, Funktionen, [\"funs'''\"])]"

(*

.. here the MethodC has been determined by the user,

so "belastung_zu_biegelinie q__q v_v id_fun id_abl" IS KNOWN and,

"id_fun" and "id_abl" WOULD BE missing (added by O_Model.).

*)

then () else error "[Biegelinien, ausBelastung] O_Model NOT EXTENDED BY MethodC";

(*\------------------- initial check for Step_Specify.by_tactic ----------------------------/*)

"~~~ fun by_tactic , args:"; val ((Tactic.Specify_Method' (mID, _, _)), (pt, pos as (p, _))) =

  (tac', ptp);

(*.NEW*) val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, meth = i_meth, ctxt,

(*.NEW*)    ...} =Calc.specify_data (pt, pos);

(*.NEW*) val (dI, _, mID) = References.select o_refs refs;

(*.NEW*) val {ppc = m_patt, pre, prls, ...} = MethodC.from_store mID

(*.NEW*) val {origin = (root_model, _, _), ...} = Calc.specify_data (pt, ([], Und))

(*.NEW*) val (o_model', ctxt') = O_Model.complete_for m_patt root_model (o_model, ctxt);

(*/------------------- check for entry to O_Model.complete_for -----------------------------\*)

(*+*)if mID = ["Biegelinien", "ausBelastung"]

(*+*)then () else error "MethodC [Biegelinien, ausBelastung] CHANGED";

(*+*)if Model_Pattern.to_string m_patt = "[\"" ^

  "(#Given, (Streckenlast, q__q))\", \"" ^

  "(#Given, (FunktionsVariable, v_v))\", \"" ^

  "(#Given, (Biegelinie, id_fun))\", \"" ^          (*.. add value from O_Model of root-problem*)

  "(#Given, (AbleitungBiegelinie, id_der))\", \"" ^ (*.. add value from O_Model of root-problem*)

  "(#Find, (Funktionen, fun_s))\"]"

(*+*)then () else error "[Biegelinien, ausBelastung] Model_Pattern CHANGED";

(*+*)if O_Model.to_string o_model = "[\n" ^

  "(1, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^

  "(2, [\"1\"], #Given, FunktionsVariable, [\"x\"]), \n" ^

  "(3, [\"1\"], #Find, Funktionen, [\"funs'''\"])]" 

(*+*)then () else error "[Biegelinien, ausBelastung] O_Model NOT EXTENDED BY MethodC CHANGED";

(*+*)if O_Model.to_string root_model = "[\n" ^

  "(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^

  "(2, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^

  "(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^

  "(4, [\"1\"], #Relate, Randbedingungen, [\"[y 0 = 0]\", \"[y L = 0]\", \"[M_b 0 = 0]\", \"[M_b L = 0]\"]), \n" ^

  "(5, [\"1\"], #Given, FunktionsVariable, [\"x\"]), \n" ^

  "(6, [\"1\"], #Given, GleichungsVariablen, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"]), \n" ^

  "(7, [\"1\"], #Given, AbleitungBiegelinie, [\"dy\"])]"

(*+*)then () else error "[Biegelinien, ausBelastung] root O_Model CHANGED";

(*+*)if O_Model.to_string o_model' = "[\n" ^   (*.. OK: is value of O_Model.complete_for *)

  "(1, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^

  "(2, [\"1\"], #Given, FunktionsVariable, [\"x\"]), \n" ^

  "(3, [\"1\"], #Find, Funktionen, [\"funs'''\"]), \n" ^

  "(4, [\"1\"], #Given, Biegelinie, [\"y\"]), \n" ^      (*.. value from O_Model of root-problem*)

  "(5, [\"1\"], #Given, AbleitungBiegelinie, [\"dy\"])]" (*.. value from O_Model of root-problem*)

(*  \<up> ----- aim at dropping this field *)

(*+*)then () else error "[Biegelinien, ausBelastung] O_Model EXTENDED BY MethodC CHANGED";

(*\------------------- check for entry to O_Model.complete_for -----------------------------/*)

  O_Model.complete_for m_patt root_model (o_model, ctxt);

"~~~~ fun complete_for , args:"; val (m_patt, root_model, (o_model, ctxt)) =

  (m_patt, root_model, (o_model, ctxt));

    val  missing = m_patt |> filter_out

      (fn (_, (descriptor, _)) => (member op = (map #4 o_model) descriptor))

;

    val add = root_model

      |> filter

        (fn (_, _, _, descriptor, _) => (member op = (map (fst o snd) missing)) descriptor)

;

    (o_model @ add

(*NEW*)|> map (fn (a, b, _, descr, e) => (a, b, the (Model_Pattern.get_field descr m_patt), descr, e))

(*NEW*)

      |> map (fn (_, b, c, d, e) => (b, c, d, e))     

      |> add_id                                       

      |> map (fn (a, (b, c, d, e)) => (a, b, c, d, e)),

    ctxt |> ContextC.add_constraints (add |> O_Model.values |> TermC.vars')) (*return from O_Model.complete_for*);

"~~~~ from fun O_Model.complete_for \<longrightarrow>Step_Specify.by_tactic , return:"; val (o_model', ctxt') =

  ((o_model @ add)

(*NEW*)|> map (fn (a, b, _, descr, e) => (a, b, the (Model_Pattern.get_field descr m_patt), descr, e))

(*NEW*)

      |> map (fn (_, b, c, d, e) => (b, c, d, e))     

      |> add_id                                       

      |> map (fn (a, (b, c, d, e)) => (a, b, c, d, e)),

    ctxt |> ContextC.add_constraints (add |> O_Model.values |> TermC.vars'));

(*/------------------- check within O_Model.complete_for -------------------------------------------\*)

(*+*)if O_Model.to_string o_model' = "[\n" ^   (*.. OK: is return from step into *)

  "(1, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^

  "(2, [\"1\"], #Given, FunktionsVariable, [\"x\"]), \n" ^

  "(3, [\"1\"], #Find, Funktionen, [\"funs'''\"]), \n" ^

  "(4, [\"1\"], #Given, Biegelinie, [\"y\"]), \n" ^

  "(5, [\"1\"], #Given, AbleitungBiegelinie, [\"dy\"])]"

(*  \<up> ----- aim at dropping this field *)

(*+*)then () else error "[Biegelinien, ausBelastung] O_Model EXTENDED BY MethodC CHANGED";

(*\------------------- check within O_Model.complete_for -------------------------------------------/*)

(*.NEW*) val thy = ThyC.get_theory dI

(*.NEW*) val (_, (i_model, _)) = M_Match.match_itms_oris thy i_prob (m_patt, pre, prls) o_model';

(*.NEW*) val (pos, _, _, pt) = Specify_Step.add (Tactic.Specify_Method' (mID, o_model', i_model))

(*.NEW*)   (Istate_Def.Uistate, ctxt') (pt, pos)

;

(*+*)if I_Model.to_string @{context} i_model = "[\n" ^

  "(1 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])), \n" ^

  "(2 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(v_v, [x])), \n" ^

  "(3 ,[1] ,true ,#Find ,Cor Funktionen funs''' ,(funs''', [funs'''])), \n" ^

  "(4 ,[1] ,false ,#Given ,Mis Biegelinie id_fun), \n" ^

  "(5 ,[1] ,false ,#Given ,Mis AbleitungBiegelinie id_der)]"

(*+*)then () else error "[Biegelinien, ausBelastung] I_Model CHANGED 1";

(*+*)val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, meth = i_meth, ctxt, ...} =

(*+*)  Calc.specify_data (pt, pos);

(*+*)pos = ([1], Met);

         ("ok", ([], [], (pt, pos)))  (*return from Step_Specify.by_tactic*);

"~~~ from Step_Specify.by_tactic \<longrightarrow>Step.by_tactic \<longrightarrow>fun me , return:"; val ("ok", (_, _, (pt, p))) =

         ("ok", ([], [], (pt, pos)));

(*  val ("helpless", ([(xxxxx, _, _)], _, _)) =  (*case*)*)

  (*  SHOULD BE    \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> Add_Given "Biegelinie y" | Add_Given "AbleitungBiegelinie dy"*)

val ("ok", ([( Add_Given "Biegelinie y", _, _)], [], _)) =

   Step.do_next p ((pt, Pos.e_pos'), []) (*of*);

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

(*.NEW*)(*if*) on_calc_end ip (*else*);

(*.NEW*)    val (_, probl_id, _) = Calc.references (pt, p);

(*-"-*)    val _ = (*case*)  tacis (*of*);

(*.NEW*)      (*if*) probl_id = Problem.id_empty (*else*);

(*.NEW*)val ("ok", ([(Add_Given "Biegelinie y", _, _)], _, _)) =

         switch_specify_solve p_ (pt, ip);

"~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));

      (*if*) Pos.on_specification ([], state_pos) (*then*);

  val ("ok", ([(Add_Given "Biegelinie y", _, _)], _, _)) =

           specify_do_next (pt, input_pos);

"~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);

    val (_, (p_', tac)) =

   Specify.find_next_step ptp;

"~~~~~ fun find_next_step , args:"; val (pt, (p, p_)) = (ptp);

    val (pblobj, met, origin, oris, dI', pI', mI', pbl, dI, pI, mI) = 

  	  case Ctree.get_obj I pt p of

  	    pblobj as (Ctree.PblObj {meth, origin = origin as (oris, (dI', pI', mI'), _),

  		  probl, spec = (dI, pI, mI), ...}) => (pblobj, meth, origin, oris, dI', pI', mI', probl, dI, pI, mI)

      | Ctree.PrfObj _ => raise ERROR "nxt_specify_: not on PrfObj"

;

(*+*)O_Model.to_string oris = "[\n" ^

  "(1, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^

  "(2, [\"1\"], #Given, FunktionsVariable, [\"x\"]), \n" ^

  "(3, [\"1\"], #Find, Funktionen, [\"funs'''\"]), \n" ^

  "(4, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^

  "(5, [\"1\"], #Given, AbleitungBiegelinie, [\"dy\"])]";

(*+*)I_Model.is_complete pbl = true;

(*+*)I_Model.to_string @{context} met = "[\n" ^

  "(1 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])), \n" ^

  "(2 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(v_v, [x])), \n" ^

  "(3 ,[1] ,true ,#Find ,Cor Funktionen funs''' ,(funs''', [funs'''])), \n" ^

  "(4 ,[1] ,false ,#Given ,Mis Biegelinie id_fun), \n" ^

  "(5 ,[1] ,false ,#Given ,Mis AbleitungBiegelinie id_abl)]";

    (*if*) Ctree.just_created_ pblobj (*by Subproblem*) andalso origin <> Ctree.e_origin (*else*);

        val cpI = if pI = Problem.id_empty then pI' else pI;

  	    val cmI = if mI = MethodC.id_empty then mI' else mI;

  	    val {ppc = pbt, prls, where_, ...} = Problem.from_store cpI;

  	    val (preok, pre) = Pre_Conds.check prls where_ pbl 0;

  	    val preok = foldl and_ (true, map fst pre);

        val mpc = (#ppc o MethodC.from_store) cmI

      val Pos.Met = (*case*) p_ (*of*);

      val NONE = (*case*) find_first (is_error o #5) met (*of*);

      (*val SOME ("#Given", "Biegelinie y") =*)

      val SOME (fd, ct') = (*case*)

        item_to_add (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) oris mpc met (*of*);

    ("ok", (Pos.Met, P_Model.mk_additem fd ct'))   (*return from find_next_step*);

"~~~~~ from fun find_next_step \<longrightarrow>fun specify_do_next , return:"; val (_, (p_', tac)) =

  ("dummy", (Pos.Met, P_Model.mk_additem fd ct'));

(*+*)val Add_Given "Biegelinie y" = tac;

    val ist_ctxt =  Ctree.get_loc pt (p, p_)

    val _ = (*case*) tac (*of*); 

  val (_, ([(Add_Given "Biegelinie y", _, _)], _, (p'''''_'', ([1], Met)))) =

Step_Specify.by_tactic_input tac (pt, (p, p_'))

(*/------------------- check result of Step_Specify.by_tactic_input ------------------------\*)

(*+*)val {meth, ...} = Calc.specify_data (p'''''_'', ([1], Met));

(*+*)I_Model.to_string @{context} meth = "[\n" ^ (* result does NOT show Add_Given "Biegelinie y" *)

  "(1 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])), \n" ^

  "(2 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(v_v, [x])), \n" ^

  "(3 ,[1] ,true ,#Find ,Cor Funktionen funs''' ,(funs''', [funs'''])), \n" ^

  "(4 ,[1] ,false ,#Given ,Mis Biegelinie id_fun), \n" ^

  "(5 ,[1] ,false ,#Given ,Mis AbleitungBiegelinie id_abl)]";

(*\------------------- check result of Step_Specify.by_tactic_input ------------------------/*)

"~~~~ fun by_tactic_input , args:"; val ((Tactic.Add_Given ct), ptp) =   (tac, (pt, (p, p_')));

   Specify.by_Add_ "#Given" ct ptp;

"~~~~~ fun by_Add_ , args:"; val (m_field, ct, (pt, pos as (_, p_))) = ("#Given", ct, ptp);

    val (met, oris, (_, pI', mI'), pbl, (_, pI, mI), ctxt) = SpecificationC.get_data (pt, pos);

       (*if*) p_ = Pos.Met (*then*);

    val (i_model, m_patt) = (met,

           (if mI = MethodC.id_empty then mI' else mI) |> MethodC.from_store |> #ppc)

val Add (4, [1], true, "#Given", Cor ((Const (\<^const_name>\<open>Biegelinie\<close>, _), [Free ("y", _)]), (Free ("id_fun", _), [Free ("y", _)]))) =

      (*case*)

   check_single ctxt m_field oris i_model m_patt ct (*of*);

(*/------------------- check for entry to check_single -------------------------------------\*)

(*+*)if O_Model.to_string oris = "[\n" ^

  "(1, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^

  "(2, [\"1\"], #Given, FunktionsVariable, [\"x\"]), \n" ^

  "(3, [\"1\"], #Find, Funktionen, [\"funs'''\"]), \n" ^

  "(4, [\"1\"], #Given, Biegelinie, [\"y\"]), \n" ^      (*------------------- \<up> \<up> \<up>  \<up> ^*)

  "(5, [\"1\"], #Given, AbleitungBiegelinie, [\"dy\"])]"

(*+*)then () else error "[Biegelinien, ausBelastung] O_Model CHANGED for entry";

(*+*)if I_Model.to_string ctxt met = "[\n" ^

  "(1 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])), \n" ^

  "(2 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(v_v, [x])), \n" ^

  "(3 ,[1] ,true ,#Find ,Cor Funktionen funs''' ,(funs''', [funs'''])), \n" ^

  "(4 ,[1] ,false ,#Given ,Mis Biegelinie id_fun), \n" ^

  "(5 ,[1] ,false ,#Given ,Mis AbleitungBiegelinie id_der)]"

(*+*)then () else error "[Biegelinien, ausBelastung] I_Model CHANGED for entry";

(*\------------------- check for entry to check_single -------------------------------------/*)

"~~~~~ ~ fun check_single , args:"; val (ctxt, m_field, o_model, i_model, m_patt, str) =

  (ctxt, sel, oris, met, ((#ppc o MethodC.from_store) cmI), ct);

      val SOME t = (*case*) TermC.parseNEW ctxt str (*of*);

(*+*)val Const (\<^const_name>\<open>Biegelinie\<close>, _) $ Free ("y", _) = t;

(*("seek_oridts: input ('Biegelinie y') not found in oris (typed)", (0, [], "#Given", Const (\<^const_name>\<open>Biegelinie\<close>, "(real \<Rightarrow> real) \<Rightarrow> una"), [Free ("y", "real \<Rightarrow> real")]), [])*)

          (*case*)

   is_known ctxt m_field o_model t (*of*);

"~~~~~ ~~ fun is_known , args:"; val (ctxt, sel, ori, t) = (ctxt, m_field, o_model, t);

    val ots = ((distinct op =) o flat o (map #5)) ori

    val oids = ((map (fst o dest_Free)) o (distinct op =) o flat o (map TermC.vars)) ots

    val (d, ts) = Input_Descript.split t

    val ids = map (fst o dest_Free) (((distinct op =) o (flat o (map TermC.vars))) ts);

    (*if*) (subtract op = oids ids) <> [] (*else*);

	    (*if*) d = TermC.empty (*else*);

	      (*if*) not (subset op = (map typeless ts, map typeless ots)) (*else*);

  (*case*) O_Model.seek_orits ctxt sel ts ori (*of*);

"~~~~~ ~~~ fun seek_orits , args:"; val (ctxt, sel, ts, ((id, vat, sel', d, ts') :: oris)) = (ctxt, sel, ts, ori);

(*+/---------------- bypass recursion of seek_orits ----------------\*)

(*+*)O_Model.to_string oris = "[\n" ^

  "(2, [\"1\"], #Given, FunktionsVariable, [\"x\"]), \n" ^

  "(3, [\"1\"], #Find, Funktionen, [\"funs'''\"]), \n" ^

  "(4, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^

  "(5, [\"1\"], #Given, AbleitungBiegelinie, [\"dy\"])]";

(*+*)val (id, vat, sel', d, ts') = nth 3 oris; (* 3rd iteration *)

(*+\---------------- bypass recursion of seek_orits ----------------/*)

    (*if*) sel = sel' andalso (inter op = ts ts') <> [] (*else*);

(*/------------------- check within seek_orits -------------------------------\*)

(*+*)if sel = "#Given" andalso sel' = "#Given"

(*+*)then () else error "seek_orits Model_Pattern CHANGED";

(*BUT: m_field can change from root-Problem to sub-MethodC --------------------vvv*)

(* sub-vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv*)

(*+*)if (Problem.from_store ["vonBelastungZu", "Biegelinien"] |> #ppc |> Model_Pattern.to_string) = "[\"" ^

  "(#Given, (Streckenlast, q_q))\", \"" ^

  "(#Given, (FunktionsVariable, v_v))\", \"" ^

  "(#Find, (Funktionen, funs'''))\"]"

(*+*)then () else error "seek_orits Model_Pattern of Subproblem CHANGED";

(* root-vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv ------------------------------------- \<up> *)

(*+*)if (Problem.from_store ["Biegelinien"] |> #ppc |> Model_Pattern.to_string) = "[\"" ^

  "(#Given, (Traegerlaenge, l_l))\", \"" ^

  "(#Given, (Streckenlast, q_q))\", \"" ^

  "(#Find, (Biegelinie, b_b))\", \"" ^ (*------------------------------------- \<up> *)

  "(#Relate, (Randbedingungen, r_b))\"]"

(*+*)then () else error "seek_orits Model_Pattern root-problem CHANGED";

(* sub-vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv*)

(*+*)if (MethodC.from_store ["Biegelinien", "ausBelastung"] |> #ppc |> Model_Pattern.to_string) = "[\"" ^

  "(#Given, (Streckenlast, q__q))\", \"" ^

  "(#Given, (FunktionsVariable, v_v))\", \"" ^

  "(#Given, (Biegelinie, id_fun))\", \"" ^ (*--------------------------------- \<up> *)

  "(#Given, (AbleitungBiegelinie, id_der))\", \"" ^

  "(#Find, (Funktionen, fun_s))\"]"

(*+*)then () else error "seek_orits Model_Pattern CHANGED";

(*+*)if UnparseC.term d = "Biegelinie"andalso UnparseC.terms ts = "[\"y\"]"

(*+*)  andalso UnparseC.terms ts' = "[\"y\"]"

(*+*)then

(*+*)  (case (inter op = ts ts') of [Free ("y", _(*"real \<Rightarrow> real"*))] => () 

(*+*)  | _ => error "check within seek_orits CHANGED 1")

(*+*)else error "check within seek_orits CHANGED 2";

(*\------------------- check within seek_orits -------------------------------/*)

(*-------------------- stop step into me\<rightarrow>Add_Given "Biegelinie y" --------------------------*)

(*\------------------- step into me\<rightarrow>Add_Given "Biegelinie y" ||||||||||||||||||||||||||||||/*)

(*[1], Met*)val (p,_,f,nxt,_,pt) = me nxt''''' p''''' c pt'''''; (*\<rightarrow>Add_Given "AbleitungBiegelinie dy"*)

(*[1], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Apply_Method ["Biegelinien", "ausBelastung"]*)

(*[1, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Rewrite ("sym_neg_equal_iff_equal", "(?a1 = ?b1) = (- ?a1 = - ?b1)")*)

(*[1, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Rewrite ("Belastung_Querkraft", "- qq ?x = Q' ?x")*)

(*[1, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Subproblem ("Biegelinie", ["named", "integrate", "function"])*)

(*[1, 3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*\<rightarrow>Model_Problem*)

(*[1, 3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*\<rightarrow>Add_Given "functionTerm (- q_0)"*)

(*[1, 3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*\<rightarrow>Add_Given "integrateBy x"*)

(*/------------------- check result of Add_Given "functionTerm (- q_0)" --------------------\*)

if p = ([1, 3], Pbl) andalso

  f = Test_Out.PpcKF (Test_Out.Problem [], {Find = [Incompl "antiDerivativeName"],

    Given = [Incompl "integrateBy", Correct "functionTerm (- q_0)"],

    Relate = [], Where = [], With = []})

then

  (case nxt of Add_Given "integrateBy x" => () | _ => error "specify-phase: low level CHANGED 1")

else error "specify-phase: low level CHANGED 2";

(*\------------------- check result of Add_Given "functionTerm (- q_0)" --------------------/*)