(* "Knowledge/biegelinie-3.sml"

   author: Walther Neuper 190515

   (c) due to copyright terms

*)

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

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

"----------- see biegelinie-1.sml---------------------------------";

(* problems with generalised handling of meths which extend the model of a probl

   since 98298342fb6d: wait for review of whole model-specify phase *)

"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. me -----";

"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. auto ---";

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

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

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

"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. me -----";

"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. me -----";

"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. me -----";

"----- Bsp 7.70 with me";

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

	     "Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]",

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

       "AbleitungBiegelinie dy"];

val (dI',pI',mI') = ("Biegelinie", ["Biegelinien"],

		     ["IntegrierenUndKonstanteBestimmen2"]);

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

(*//----------------------------------vvv CalcTreeTEST ----------------------------------------\\*)

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

(*+*)val PblObj {probl, meth, spec = (thy, _ , metID), origin = (oris, _, _), ...} = get_obj I pt (fst p);

(*+*)writeln (oris2str oris); (*[

(1, ["1"], #Given,Traegerlaenge, ["L"]),

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

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

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

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

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

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

(*+*)itms2str_ @{context} probl = "[]";

(*+*)itms2str_ @{context} meth = "[]";

(*\\----------------------------------^^^ CalcTreeTEST ----------------------------------------//*)

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

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

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

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

(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = 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; (*nxt = Specify_Theory "Biegelinie"*)

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

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

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

(*----------- 10 -----------*)

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

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

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

(*//----------------------------------vvv Apply_Method ["IntegrierenUndKonstanteBestimmen2"----\\*)

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

(*AMBIGUITY in creating the environment from formal args. of partial_function "Biegelinie.Biegelinie2Script"

and the actual args., ie. items of the guard of "["IntegrierenUndKonstanteBestimmen2"]" by "assoc_by_type":

formal arg. "b" type-matches with several...actual args. "["dy","y"]"

selected "dy"

with

formals: ["l","q","v","b","s","vs","id_abl"]

actuals: ["L","q_0","x","[c, c_2, c_3, c_4]","dy","y","[y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]"]*)

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

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

	    (*locatetac is here for testing by me; step would suffice in me*)

	    case locatetac tac (pt,p) of

		    ("ok", (_, _, ptp)) => ptp

;

(*+*)p    = ([], Met);

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

(*+*)val PblObj {meth, probl, spec = (thy, _ , metID), origin = (oris, _, _), ...} = get_obj I pt''' (fst p''');

(*+*)(*MISSING after locatetac:*)

(*+*)writeln (oris2str oris); (*[

(1, ["1"], #Given,Streckenlast, ["q_0"]),

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

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

MISSING:

                 Biegelinie

                 AbleitungBiegelinie

*)

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

      val (mI, m) = Solve.mk_tac'_ tac;

val Appl m = (*case*) Applicable.applicable_in p pt m (*of*);

(*if*) member op = Solve.specsteps mI = false; (*else*)

loc_solve_ (mI,m) ptp;

"~~~~~ fun loc_solve_ , args:"; val (m, (pt, pos)) = ((mI,m), ptp);

Solve.solve m (pt, pos);

"~~~~~ fun solve , args:"; val (("Apply_Method", m as Tac.Apply_Method' (mI, _, _, _)), (pt, (pos as (p, _)))) =

  (m, (pt, pos));

val {srls, ...} = Specify.get_met mI;

      val itms = case get_obj I pt p of

        PblObj {meth=itms, ...} => itms

      | _ => error "solve Apply_Method: uncovered case get_obj"

      val thy' = get_obj g_domID pt p;

      val thy = Celem.assoc_thy thy';

      val (is, env, ctxt, sc) = case Lucin.init_scrstate thy itms mI of

        (is as Selem.ScrState (env,_,_,_,_,_), ctxt, sc) =>  (is, env, ctxt, sc)

      | _ => error "solve Apply_Method: uncovered case init_scrstate"

      val ini = Lucin.init_form thy sc env;

      val p = lev_dn p;

val NONE = (*case*) ini (*of*);

            val (m', (is', ctxt'), _) = Lucin.next_tac (thy', srls) (pt, (p, Res)) sc (is, ctxt);

	          val d = Rule.e_rls (*FIXME: get simplifier from domID*);

val Steps (_, ss as (_, _, pt', p', c') :: _) =

(*case*) Lucin.locate_gen (thy',srls) m' (pt,(p, Res)) (sc,d) (is', ctxt') (*of*);

(*+*)val PblObj {meth, probl, spec = (thy, _ , metID), origin = (oris, _, _), ...} = get_obj I pt' (fst p');

(*+*)(*MISSING after locate_gen:*)

(*+*)writeln (oris2str oris); (*[

(1, ["1"], #Given,Streckenlast, ["q_0"]),

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

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

MISSING:

                 Biegelinie

                 AbleitungBiegelinie

*)

"~~~~~ fun locate_gen , args:"; val ((thy', srls), m, (pt, p),

	    (scr as Rule.Prog sc, d), (Selem.ScrState (E,l,a,v,S,b), ctxt)) =

  ((thy',srls), m', (pt,(p, Res)), (sc,d), (is', ctxt'));

val thy = Celem.assoc_thy thy';

(*if*) l = [] orelse (

		  (*init.in solve..Apply_Method...*)(last_elem o fst) p = 0 andalso snd p = Res) = true;(*then*)

(assy (thy',ctxt,srls,d,Aundef) ((E,[Celem.R],a,v,S,b), [(m,Generate.EmptyMout,pt,p,[])]) (body_of sc));

"~~~~~ fun assy , args:"; val (ya, ((E,l,a,v,S,b),ss:step list), (Const ("HOL.Let",_) $ e $ (Abs (id,T,body)))) =

  ((thy',ctxt,srls,d,Aundef), ((E,[Celem.R],a,v,S,b), [(m,Generate.EmptyMout,pt,p,[])]), (body_of sc));

(*case*) assy ya ((E , l @ [Celem.L, Celem.R], a,v,S,b), ss) e (*of*);

"~~~~~ fun assy , args:"; val ((thy',ctxt,sr,d,ap), ((E,l,a,v,S,_), (m,_,pt,(p,p_),c)::ss), t) =

  (ya, ((E , l @ [Celem.L, Celem.R], a,v,S,b), ss), e);

val (a', LTool.STac stac) = (*case*) handle_leaf "locate" thy' sr E a v t (*of*);

(*+*)writeln (term2str stac); (*SubProblem

 (''Biegelinie'', [''vonBelastungZu'', ''Biegelinien''],

  [''Biegelinien'', ''ausBelastung''])

 [REAL q_0, REAL x, REAL_REAL y, REAL_REAL dy] *)

           val p' = 

             case p_ of Frm => p 

             | Res => lev_on p

		         | _ => error ("assy: call by " ^ pos'2str (p,p_));

     val Ass (m,v') = (*case*) assod pt d m stac (*of*);

"~~~~~ fun assod , args:"; val (pt, _, (Tac.Subproblem' ((domID, pblID, _), _, _, _, _, _)),

      (stac as Const ("Script.SubProblem", _) $ (Const ("Product_Type.Pair", _) $ 

        dI' $ (Const ("Product_Type.Pair", _) $ pI' $ mI')) $ ags')) =

  (pt, d, m, stac);

      val dI = HOLogic.dest_string dI';

      val thy = Stool.common_subthy (Celem.assoc_thy dI, rootthy pt);

	    val pI = pI' |> HOLogic.dest_list |> map HOLogic.dest_string;

	    val mI = mI' |> HOLogic.dest_list |> map HOLogic.dest_string;

	    val ags = TermC.isalist2list ags';

(*if*) mI = ["no_met"] = false; (*else*)

(*    val (pI, pors, mI) = *)

	      (pI, (Chead.match_ags thy ((#ppc o Specify.get_pbt) pI) ags)

		      handle ERROR "actual args do not match formal args"

		      => (Chead.match_ags_msg pI stac ags(*raise exn*); []), mI);

"~~~~~ fun match_ags , args:"; val (thy, pbt, ags) = (thy, ((#ppc o Specify.get_pbt) pI), ags);

(*+*)pbt;

    fun flattup (i, (var, bool, str, itm_)) = (i, var, bool, str, itm_)

    val pbt' = filter_out is_copy_named pbt

    val cy = filter is_copy_named pbt

    val oris' = matc thy pbt' ags []

    val cy' = map (cpy_nam pbt' oris') cy

    val ors = Specify.add_id (oris' @ cy') (*...appended in order to get into the model-items *)

(*+*)val c = [];

(*\\----------------------------------^^^ Apply_Method ["IntegrierenUndKonstanteBestimmen2"----//*)

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

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

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

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

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

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

(*----------- 20 -----------*)

(*//------------------------------------------------vvv Specify_Method ["Biegelinien", "ausBelastung"]-\\*)

(*[1], Pbl*)(*ERROR val (p,_,f,nxt,_,pt) = me nxt''''' p''''' c pt'''''; (*nxt = Apply_Method ["Biegelinien", "ausBelastung"]*)

ERROR itms2args: 'Biegelinie' not in itms*)

(*SubProblem (_, [''vonBelastungZu'', ''Biegelinien''], _)

    [REAL q, REAL v, REAL_REAL b, REAL_REAL id_abl]

                     ^^^^^^^^^^^ ..ERROR itms2args: 'Biegelinie' not in itms*)

(*+*)val PblObj {meth, probl, spec = (thy, _ , metID), origin = (oris, _, _), ...} = get_obj I pt''''' (fst p''''');

(*+*)if oris2str oris =

(*+*)  "[\n(1, [\"1\"], #Given,Streckenlast, [\"q_0\"]),\n(2, [\"1\"], #Given,FunktionsVariable, [\"x\"]),\n(3, [\"1\"], #Find,Funktionen, [\"funs'''\"])]"

(*+*)then () else error "([1], Pbl) Specify_Problem ['vonBelastungZu', 'Biegelinien'] changed oris";

writeln (oris2str oris); (*[

(1, ["1"], #Given,Streckenlast, ["q_0"]),

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

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

(*+*)if itms2str_ @{context} probl = "[\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''']))]"

(*+*)then () else error "([1], Pbl) Specify_Problem ['vonBelastungZu', 'Biegelinien'] changed probl";

writeln (itms2str_ @{context} probl); (*[

(1 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])),

(2 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(v_v, [x])),

(3 ,[1] ,true ,#Find ,Cor Funktionen funs''' ,(funs''', [funs''']))]*)

(*+*)if itms2str_ @{context} meth = "[]"

(*+*)then () else error "([1], Pbl) Specify_Problem ['vonBelastungZu', 'Biegelinien'] changed meth";

writeln (itms2str_ @{context} meth); (*[]*)

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

(*  val (pt, p) = *)

	    (*locatetac is here for testing by me; step would suffice in me*)

	    case locatetac tac (pt,p) of

		    ("ok", (_, _, ptp)) => ptp

;

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

      val (mI, m) = Solve.mk_tac'_ tac;

val Chead.Appl m = (*case*) Applicable.applicable_in p pt m (*of*);

(*if*) member op = Solve.specsteps mI = true; (*then*)

(*val Updated (_, _, (ctree, pos')) =*) loc_specify_ m ptp; (*creates meth-itms*)

"~~~~~ fun loc_specify_ , args:"; val (m, (pt, pos)) = (m, ptp);

(*    val (p, _, f, _, _, pt) =*) Chead.specify m pos [] pt;

"~~~~~ fun specify , args:"; val ((Tac.Specify_Method' (mID, _, _)), (pos as (p, _)), _, pt) = (m, pos, [], pt);

        val (oris, dI', pI', mI', dI, pI, pbl, met, ctxt) = case get_obj I pt p of

          PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, pI, _), probl = pbl, meth = met, ctxt, ...} =>

             (oris, dI', pI', mI', dI, pI, pbl, met, ctxt)

        val {ppc, pre, prls,...} = Specify.get_met mID

        val thy = Celem.assoc_thy dI

        val dI'' = if dI = Rule.e_domID then dI' else dI

        val pI'' = if pI = Celem.e_pblID then pI' else pI

;

(*+*)writeln (oris2str oris); (*[

(1, ["1"], #Given,Streckenlast, ["q_0"]),

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

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

(*+*)writeln (pats2str' ppc);

(*["(#Given, (Streckenlast, q__q))

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

","(#Given, (Biegelinie, id_fun))

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

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

(*+*)writeln (pats2str' ((#ppc o Specify.get_pbt) pI));

(*["(#Given, (Streckenlast, q_q))

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

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

        val oris = Specify.add_field' thy ppc oris

        val met = if met = [] then pbl else met

        val (_, (itms, pre')) = Specify.match_itms_oris thy met (ppc, pre, prls ) oris

;

(*+*)writeln (itms2str_ @{context} itms); (*[

(1 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])),

(2 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(v_v, [x])),

(3 ,[1] ,true ,#Find ,Cor Funktionen funs''' ,(funs''', [funs''']))] *)

(*//----------- hack for funpack: generalise handling of meths which extend problem items -----\\*)

val itms =

  if mI' = ["Biegelinien", "ausBelastung"]

  then itms @

    [(4, [1], true, "#Given", Cor ((Const ("Biegelinie.Biegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Tools.una", [])])),

        [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),

      (Free ("id_fun", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),

        [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] ))),

    (5, [1], true, "#Given", Cor ((Const ("Biegelinie.AbleitungBiegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Tools.una", [])])),

        [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),

      (Free ("id_abl", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),

        [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] )))]

  else itms

(*\\----------- hack for funpack: generalise handling of meths which extend problem items -----//*)

val itms' = itms @

  [(4, [1], true, "#Given", Cor ((@{term "Biegelinie"},

      [@{term "y::real \<Rightarrow> real"}]),

    (@{term "id_fun::real \<Rightarrow> real"},

      [@{term "y::real \<Rightarrow> real"}] ))),

  (5, [1], true, "#Given", Cor ((@{term "AbleitungBiegelinie"},

      [@{term "dy::real \<Rightarrow> real"}]),

    (@{term "id_abl::real \<Rightarrow> real"},

      [@{term "dy::real \<Rightarrow> real"}] )))]

val itms'' = itms @

  [(4, [1], true, "#Given", Cor ((Const ("Biegelinie.Biegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Tools.una", [])])),

      [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),

    (Free ("id_fun", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),

      [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] ))),

  (5, [1], true, "#Given", Cor ((Const ("Biegelinie.AbleitungBiegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Tools.una", [])])),

      [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),

    (Free ("id_abl", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),

      [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] )))]

;

if itms' = itms'' then () else error "itms BUIT BY HAND ARE BROKEN";

(*//-----------------------------------------^^^ Specify_Method ["Biegelinien", "ausBelastung"]-\\*)

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

(*----------- 30 -----------*)

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

(*----------- 40 -----------*)

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

(*----------- 50 -----------*)

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

(*----------- 60 -----------*)

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

(*----------- 70 -----------*)

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

(*----------- 80 -----------*)

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;

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

  f = PpcKF (Problem [], {Find = [Incompl "equality"], Given = [Incompl "functionEq", Incompl "substitution"], Relate = [], Where = [], With = []})

then

  case nxt of

    ("Add_Given", Add_Given "functionEq (hd [])") => ((*here is an error in partial_function*))

  | _ => error "me biegelinie changed 1"

else error "me biegelinie changed 2";

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

nxt;(* = ("Tac ", Tac "[error] appl_add: is_known: seek_oridts: input ('substitution (NTH (1 + -4) [])') not found in oris (typed)")*)

(*----- due to problems with generalised handling of meths which extend the model of a probl

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;

(*----------- 90 -----------*)

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

(*---------- 100 -----------*)

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

(*---------- 110 -----------*)

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

(*---------- 120 -----------*)

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

(*---------- 130 -----------*)

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

if p = ([3], Pbl)

then

  case nxt of

    ("Add_Given", Add_Given "solveForVars [c_2, c_3, c_4]") => 

    (case f of

      PpcKF

          (Problem [],

           {Find = [Incompl "solution []"], Given =

            [Correct

              "equalities\n [0 = -1 * c_4 / -1,\n  0 =\n  (-24 * c_4 * EI + -24 * L * c_3 * EI + 12 * L ^^^ 2 * c_2 +\n   4 * L ^^^ 3 * c +\n   -1 * L ^^^ 4 * q_0) /\n  (-24 * EI),\n  0 = c_2, 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2]",

             Incompl "solveForVars [c]"],

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

    | _ => error "Bsp.7.70 me changed 1")

  | _ => error "Bsp.7.70 me changed 2"

else error "Bsp.7.70 me changed 3";

-----*)

(* NOTE: ^^^^^^^^^^^^^^^^^ no progress already in isabisac15, but not noticed ^^^^^^^^^^^^^^^^^ *)

"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. auto ---";

"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. auto ---";

"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. auto ---";

(* the error in this test might be independent from introduction of y, dy

   as arguments in IntegrierenUndKonstanteBestimmen2,

   rather due to so far untested use of "auto" *)

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

	     "Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]",

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

       "AbleitungBiegelinie dy"];

val (dI',pI',mI') = ("Biegelinie", ["Biegelinien"],

		     ["IntegrierenUndKonstanteBestimmen2"]);

reset_states ();

CalcTree [(fmz, (dI',pI',mI'))];

Iterator 1;

moveActiveRoot 1;

(*[], Met*)autoCalculate 1 CompleteCalcHead;

(*[1], Pbl*)autoCalculate 1 (Step 1); (* into SubProblem *)

(*[1], Res*)autoCalculate 1 CompleteSubpbl; (**)

(*[2], Pbl*)autoCalculate 1 (Step 1); (* out of SubProblem *)

(*[2], Res*)autoCalculate 1 CompleteSubpbl;

(*[3], Pbl*)autoCalculate 1 (Step 1); (* out of SubProblem *)

(*[3], Met*)autoCalculate 1 CompleteCalcHead;

(*[3, 1], Frm*)autoCalculate 1 (Step 1); (* solve SubProblem *)

(*(**)autoCalculate 1 CompleteSubpbl;  error in kernel 4: generate1: not impl.for Empty_Tac_*)

(*[3, 1], Res*)autoCalculate 1 (Step 1); (* solve SubProblem *)

(*[3, 2], Res*)autoCalculate 1 (Step 1); (* solve SubProblem *)

(*[3, 3], Res*)autoCalculate 1 (Step 1); (* solve SubProblem *)

(*[3, 4], Res*)autoCalculate 1 (Step 1); (* solve SubProblem *)

(*[3, 5], Res*)autoCalculate 1 (Step 1); (* solve SubProblem *)

(*[3, 6], Res*)autoCalculate 1 (Step 1); (* solve SubProblem *)

(*[3, 7], Res*)autoCalculate 1 (Step 1); (* solve SubProblem *)

(*[3, 8], Pbl*)autoCalculate 1 (Step 1); (* solve SubProblem *)

(*[3, 8], Met*)autoCalculate 1 CompleteCalcHead;

(*[3, 8, 1], Frm*)autoCalculate 1 (Step 1); (* solve SubProblem *)

(*[3, 8, 1], Res*)autoCalculate 1 (Step 1); (* solve SubProblem *)

(*(**)autoCalculate 1 (Step 1); 

*** generate1: not impl.for Empty_Tac_ 

val it = <AUTOCALC><CALCID>1</CALCID><CALCMESSAGE>helpless</CALCMESSAGE></AUTOCALC>: XML.tree *)

val ((pt,_),_) = get_calc 1;

val ip = get_pos 1 1;

val (Form f, tac, asms) = pt_extract (pt, ip);

if ip = ([2, 1, 1], Frm) andalso 

term2str f  = "hd []"

then 

  case tac of

    SOME Empty_Tac => ()

  | _ => error "ERROR biegel.7.70 changed 1"

else error "ERROR biegel.7.70 changed 2";

(*----- this state has been reached shortly after 98298342fb6d:

if ip = ([3, 8, 1], Res) andalso 

term2str f = "[-1 * c_4 / -1 = 0,\n (6 * c_4 * EI + 6 * L * c_3 * EI + -3 * L ^^^ 2 * c_2 + -1 * L ^^^ 3 * c) /\n (6 * EI) =\n L ^^^ 4 * q_0 / (-24 * EI),\n c_2 = 0, c_2 + L * c = L ^^^ 2 * q_0 / 2]"

then 

  case tac of

    SOME (Check_Postcond ["normalise", "4x4", "LINEAR", "system"]) => ()

  | _ => error "ERROR biegel.7.70 changed 1"

else error "ERROR biegel.7.70 changed 2";

*)