(* use this theory for tests before Build_Isac.thy has succeeded *)

theory Test_Theory imports "$ISABELLE_ISAC/Build_Isac"

  "$ISABELLE_ISAC_TEST/Tools/isac/Specify/refine"        (* setup for refine.sml   *)

begin                                                                            

ML_file "$ISABELLE_ISAC/BaseDefinitions/libraryC.sml"

section \<open>code for copy & paste ===============================================================\<close>

text \<open>

  declare [[show_types]] 

  declare [[show_sorts]]

  find_theorems "?a <= ?a"

  print_theorems

  print_facts

  print_statement ""

  print_theory

  ML_command \<open>Pretty.writeln prt\<close>

  declare [[ML_print_depth = 999]]

  declare [[ML_exception_trace]]

\<close>

ML \<open>

\<close> ML \<open>

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

"~~~~~ and xxx , args:"; val () = ();

"~~~~~ from fun xxx \<longrightarrow>fun yyy \<longrightarrow>fun zzz , return:"; val () = ();

"~~~~~ continue fun xxx"; val () = ();

(*if*) (*then*); (*else*); (*andalso*)  (*case*) (*of*);  (*return value*); (*in*) (*end*);

"xx"

^ "xxx"   (*+*) (*+++*) (*keep for continuing YYYYY*) (*isa*) (*isa2*) (**)

\<close> ML \<open> (*//----------- build fun XXXXX -----------------------------------------------------\\*)

(*//------------------ build fun XXXXX -----------------------------------------------------\\*)

(*\\------------------ build fun XXXXX -----------------------------------------------------//*)

\<close> ML \<open> (*\\----------- build fun XXXXX -----------------------------------------------------//*)

val return_XXXXX = "XXXXX"

\<close> ML \<open> (*//----------- step into XXXXX -----------------------------------------------------\\*)

(*//------------------ step into XXXXX -----------------------------------------------------\\*)

\<close> ML \<open> (*||----------- contine XXXXX ---------------------------------------------------------*)

(*||------------------ contine XXXXX ---------------------------------------------------------*)

(*\\------------------ step into XXXXX -----------------------------------------------------//*)

\<close> ML \<open> (*\\----------- step into XXXXX -----------------------------------------------------//*)

val "XXXXX" = return_XXXXX;

(* final test ... ----------------------------------------------------------------------------*)

\<close> ML \<open> (*//----------- inserted hidden code ------------------------------------------------\\*)

(*//------------------ inserted hidden code ------------------------------------------------\\*)

(*\\------------------ inserted hidden code ------------------------------------------------//*)

\<close> ML \<open> (*\\----------- inserted hidden code ------------------------------------------------//*)

\<close> ML \<open>

\<close>

section \<open>===================================================================================\<close>

section \<open>=====  ============================================================================\<close>

ML \<open>

\<close> ML \<open>

\<close> ML \<open>

\<close>

section \<open>===================================================================================\<close>

section \<open>===== src/../pre-conditions.sml ===================================================\<close>

ML \<open>

open Model_Def

open Pre_Conds

open I_Model

\<close> ML \<open>

fun of_max_variant _ [] = ((false, 0, []), [], ([], []))

  | of_max_variant model_patt i_model =

 let

    val all_variants =

        map (fn (_, variants, _, _, _) => variants) i_model

        |> flat

        |> distinct op =

    val variants_separated = map (filter_variants' i_model) all_variants

    val sums_corr = map (cnt_corrects) variants_separated

    val sum_variant_s = arrange_args sums_corr (1, all_variants)

    val (_, max_variant) = hd (*..crude decision, up to improvement *)

      (sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s)

    val i_model_max =

      filter (fn (_, variants, _ , _ ,_) => member (op =) variants max_variant) i_model

    val equal_descr_pairs = map (get_equal_descr i_model) model_patt |> flat

    val env_model = make_env_model equal_descr_pairs

    val equal_givens = filter (fn ((m_field, _), _) => m_field = "#Given") equal_descr_pairs

    val subst_eval_list = make_envs_preconds equal_givens

    val (env_subst, env_eval) = split_list subst_eval_list

  in

    ((length (filter (fn (_, _, _, _, (Cor_TEST _, _)) => true | _ => false) i_model_max)

        = length model_patt, max_variant, i_model_max),

      env_model, (env_subst, env_eval))

  end

\<close> ML \<open>

of_max_variant:

   Model_Pattern.single list ->

     (int * variant list * bool * m_field * (i_model_feedback_TEST * Position.T)) list ->

       (bool * variant * (int * variant list * bool * m_field * (i_model_feedback_TEST * Position.T)) list) * (term * term) list * ((term * term) list * (term * term) list)

\<close> ML \<open>

of_max_variant: Model_Pattern.single list -> Model_Def.i_model_TEST ->

       (bool * variant * Model_Def.i_model_TEST) * Env.T * (env_subst * env_eval)

\<close> ML \<open>

\<close> ML \<open>

\<close>

(**)ML_file "Minisubpbl/150a-add-given-Maximum.sml" (** )check file with test under repair below( **)

section \<open>===================================================================================\<close>

section \<open>===== Minisubpbl/150a-add-given-Maximum.sml  ======================================\<close>

ML \<open>

\<close> ML \<open>

(* Title:  "Minisubpbl/150a-add-given-Maximum.sml"

   Author: Walther Neuper 1105

   (c) copyright due to lincense terms.

COMPARE Specify/specify.sml --- specify-phase: low level functions ---

ATTENTION: the file creates buffer overflow if copied in one piece !

Note: This test --- steps into me --- more than once, to a somewhat extreme extent;

  in order not to get lost while working in Test_Some etc, 

  re-introduce  ML (*--- step into XXXXX ---*) and Co.

  and use Sidekick for orientation.

  Nesting is indicated by  /---   //--   ///-  at the left margin of the comments.

*)

open Ctree;

open Pos;

open TermC;

open Istate;

open Tactic;

open I_Model;

open P_Model

open Rewrite;

open Step;

open LItool;

open LI;

open Test_Code

open Specify

open ME_Misc

open Pre_Conds;

val (_(*example text*),

  (model as ("Constants [r = (7::real)]" :: "Maximum A" :: "AdditionalValues [u, v]" :: 

     "Extremum (A = 2 * u * v - u \<up> 2)" :: 

     "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" :: 

     "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" :: 

     "SideConditions [(u::real) / 2 = r * sin \<alpha>, 2 / v = r * cos \<alpha>]" :: (*INCORRECT 2 / v*)

(*---------------------------------------------,(v::real) / 2 = r * cos \<alpha>]" --- ERROR in example*)

     "FunctionVariable a" :: "FunctionVariable b" :: "FunctionVariable \<alpha>" :: 

     "Domain {0 <..< r}" :: "Domain {0 <..< r}" :: "Domain {0 <..< \<pi> / 2}" ::

     "ErrorBound (\<epsilon> = (0::real))" :: []), 

   refs as ("Diff_App", 

     ["univariate_calculus", "Optimisation"],

     ["Optimisation", "by_univariate_calculus"])))

  = Store.get (Know_Store.get_expls @{theory}) ["Diff_App-No.123a"] ["Diff_App-No.123a"];

val c = [];

val return_init_calc = 

 Test_Code.init_calc @{context} [(model, refs)]; (*val Model_Problem = nxt;*)

(*/------------------- step into init_calc -------------------------------------------------\\*)

"~~~~~ fun init_calc , args:"; val (ctxt, [(model, refs as (thy_id, _, _))]) =

  (@{context}, [(model, refs)]);

    val thy = thy_id |> ThyC.get_theory ctxt

    val ((pt, p), tacis) = Step_Specify.initialise' thy (model, refs)

	  val tac = case tacis of [] => Tactic.Empty_Tac | _ => (#1 o hd) tacis

	  val f = 

           TESTg_form ctxt (pt,p);

"~~~~~ fun TESTg_form , args:"; val (ctxt, ptp) = (ctxt, (pt,p));

    val (form, _, _) =

   ME_Misc.pt_extract ctxt ptp;

"~~~~~ fun pt_extract , args:"; val (ctxt, (pt, (p, p_ as Pbl(*Frm,Pbl*)))) = (ctxt, ptp);

        val ppobj = Ctree.get_obj I pt p

        val f = if Ctree.is_pblobj ppobj then pt_model ppobj p_ else Ctree.get_obj pt_form pt p;

            (*if*) Ctree.is_pblobj ppobj (*then*);

           pt_model ppobj p_ ;

"~~~~~ fun pt_model , args:"; val ((Ctree.PblObj {probl, spec, origin = (_, spec', hdl), ctxt, ...}), Pbl_) =

  (ppobj, p_);

      val (_, pI, _) = Ctree.get_somespec' spec spec';

(*    val where_ = if pI = Problem.id_empty then []*)

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

	          val {where_rls, where_, model, ...} = Problem.from_store ctxt pI

	          val (_, where_) = 

 Pre_Conds.check ctxt where_rls where_

              (model, I_Model.OLD_to_TEST probl);

"~~~~~ fun check , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =

  (ctxt, where_rls, where_, (model, I_Model.OLD_to_TEST probl));

      val (_, _, (env_subst, env_eval)) =

           of_max_variant model_patt i_model;

"~~~~~ fun of_max_variant , args:"; val (_, []) = (model_patt, i_model);

(*\------------------- step into init_calc -------------------------------------------------//*)

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

(*+*)val PblObj {ctxt, probl, ...} = get_obj I pt [];

(*+*)Proof_Context.theory_of ctxt (*= {Pure, .., Diff_App}*);

(*+*)val Free ("r", Type ("Real.real", [])) = Syntax.read_term ctxt "r"

(*+*)val [] = probl

val return_me_Model_Problem = 

           me nxt p c pt; val Add_Given "Constants [r = 7]" = #4 return_me_Model_Problem;

(*/------------------- step into me Model_Problem ------------------------------------------\\*)

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

      val ctxt = Ctree.get_ctxt pt p

val return_by_tactic = case

      Step.by_tactic tac (pt,p) of

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

(*//------------------ step into 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*);

(*+*)val Model_Problem' _ = tac';

"~~~~~ 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.Model_Problem, (pt, pos as (p, _))) =

  (tac, (ctree, pos));

        val (o_model, pI', ctxt) = case Ctree.get_obj I pt p of

          Ctree.PblObj {origin = (o_model, (_, pI', _), _), ctxt, ...} => (o_model, pI', ctxt)

	      val {model = model_patt, ...} = Problem.from_store (Ctree.get_ctxt pt pos) pI'

	      val pbl = I_Model.init_TEST o_model model_patt;

val return_check =

    Applicable.Yes (Tactic.Model_Problem' (pI', I_Model.TEST_to_OLD pbl, []));

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

val (pt, p) = return_by_tactic;

val return_do_next = (*case*)

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

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

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

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

    val pIopt = get_pblID (pt,ip);

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

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

      val SOME _ = (*case*) pIopt (*of*);

    val ("ok", ([(Add_Given "Constants [r = 7]", _, _)], [], _)) =

      Step.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 "Constants [r = 7]", _, _)], [], _)) =

      Step.specify_do_next (pt, input_pos);

(*///----------------- step into specify_do_next -------------------------------------------\\*)

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

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

val return_find_next_step = (*keep for continuing specify_do_next*)

   Specify.find_next_step ptp;

(*////---------------- step into find_next_step --------------------------------------------\\*)

"~~~~~ fun find_next_step , args:"; val ((pt, pos as (_, p_))) = (ptp);

    val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,

      spec = refs, ...} = Calc.specify_data (pt, pos);

    val ctxt = Ctree.get_ctxt pt pos;

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

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

   Specify.for_problem ctxt oris (o_refs, refs) (pbl, met);

(*/////--------------- step into for_problem -----------------------------------------------\\*)

"~~~~~ fun for_problem , args:"; val (ctxt, oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met))

  = (ctxt, oris, (o_refs, refs), (pbl, met));

    val cdI = if dI = ThyC.id_empty then dI' else dI;

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

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

    val {model = pbt, where_rls, where_, ...} = Problem.from_store ctxt cpI;

    val {model = mpc, ...} = MethodC.from_store ctxt cmI;

    val return_check_OLD =

           check ctxt where_rls where_ (pbt, I_Model.OLD_to_TEST pbl);

(*//////-------------- step into check -------------------------------------------------\\*)

"~~~~~ fun check , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =

  (ctxt, where_rls, where_, (pbt, I_Model.OLD_to_TEST pbl));

      val return_of_max_variant =

           of_max_variant model_patt i_model;

\<close> ML \<open>(*///// //------ step into of_max_variant --------------------------------------------\\*)

(*///// //------------ step into of_max_variant --------------------------------------------\\*)

"~~~~~ fun of_max_variant , args:"; val (model_patt, i_model) =

  (model_patt, i_model);

(*+*)val "[\n(1, [1, 2, 3], false ,#Given, (Inc_TEST Constants [] [__=__, __=__], Position.T)), \n(2, [1, 2, 3], false ,#Find, (Inc_TEST Maximum __, Position.T)), \n(3, [1, 2, 3], false ,#Find, (Inc_TEST AdditionalValues [] [__, __], Position.T)), \n(4, [1, 2, 3], false ,#Relate, (Inc_TEST Extremum (__=__), Position.T)), \n(5, [1, 2], false ,#Relate, (Inc_TEST SideConditions [] [__=__, __=__], Position.T))]"

 = i_model |> I_Model.to_string_TEST @{context}

    val all_variants =

        map (fn (_, variants, _, _, _) => variants) i_model

        |> flat

        |> distinct op =

    val variants_separated = map (filter_variants' i_model) all_variants

    val sums_corr = map (cnt_corrects) variants_separated

    val sum_variant_s = arrange_args sums_corr (1, all_variants)

(*+*)val [(0, 1), (0, 2), (0, 3)] = sum_variant_s

    val (_, max_variant) = hd (*..crude decision, up to improvement *)

      (sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s)

    val i_model_max =

      filter (fn (_, variants, _ , _ ,_) => member (op =) variants max_variant) i_model

    val equal_descr_pairs = map (get_equal_descr i_model) model_patt |> flat

(*for building make_env_s -------------------------------------------------------------------\*)

(*!!!*) val ("#Given", (descr, term), pos) =

  Model_Pattern.split_descriptor ctxt ("#Given", @{term "Constants [r = (7::real)]"}, Position.none)

(*!!!*) val patt = equal_descr_pairs |> hd |> #1

(*!!!*)val equal_descr_pairs =

  (patt,

  (1, [1, 2, 3], true, "#Given", (Cor_TEST ((descr, (*!*)TermC.isalist2list(*!*) term), 

                                                     (TermC.empty, [])), pos)))

  :: tl equal_descr_pairs

(*for building make_env_s -------------------------------------------------------------------/*)

    val env_model = make_env_model equal_descr_pairs;

(*///// ///----------- step into make_env_model --------------------------------------------\\*)

"~~~~~ fun make_env_model , args:"; val (equal_descr_pairs) = (equal_descr_pairs);

val xxx = (fn ((_, (_, id)), (_, _, _, _, (feedb, _)))

       => (mk_env_model id feedb));

val ((_, (_, id)), (_, _, _, _, (feedb, _))) = nth 4 equal_descr_pairs;

(*\\\\\ \\\----------- step into make_env_model --------------------------------------------//*)

\<close> ML \<open>(*||||| ||------ contine of_max_variant ------------------------------------------------*)

(*||||| ||------------ contine of_max_variant ------------------------------------------------*)

    val equal_givens = filter (fn ((m_field, _), _) => m_field = "#Given") equal_descr_pairs

    val subst_eval_list = make_envs_preconds equal_givens

val return_make_envs_preconds =

           make_envs_preconds equal_givens;

(*///// ///----------- step into make_envs_preconds ----------------------------------------\\*)

"~~~~~ fun make_envs_preconds , args:"; val (equal_givens) = (equal_givens);

val xxx = (fn ((_, (_, id)), (_, _, _, _, (feedb, _))) => discern_feedback id feedb)

;

xxx: (Model_Pattern.single * I_Model.single_TEST) -> ((term * term) * (term * term)) list;

val return_discern_feedback =

           discern_feedback id feedb;

(*nth 1 equal_descr_pairs* )

"~~~~~ fun discern_feedback , args:"; val (id, (Model_Def.Cor_TEST ((descr, ts), _))) = (id, feedb);

( *nth 2 equal_descr_pairs*)

"~~~~~ fun discern_feedback , args:"; val (id, (Model_Def.Inc_TEST ((descr, ts), _))) = (id, feedb);

(*nth 1 equal_descr_pairs* )

(*+*)val [((Const ("fixes", typ1), Free ("r", typ2)),

           (Free ("r", typ3), value))] = return_discern_feedback

(*+*)val true = typ1 = typ2

(*+*)val true = typ3 = HOLogic.realT

(*+*)val "7" = UnparseC.term @{context} value

( *nth 2 equal_descr_pairs*)

(*+*)val [] = return_discern_feedback

val return_discern_typ =

           discern_typ id (descr, ts);

"~~~~~ fun discern_typ , args:"; val (id, (descr, ts)) = (id, (descr, ts));

(*nth 1 equal_descr_pairs* )

(*+*)val [((Const ("fixes", typ1), Free ("r", typ2)),

           (Free ("r", typ3), value))] = return_discern_typ

(*+*)val true = typ1 = typ2

(*+*)val true = typ3 = HOLogic.realT

(*+*)val "7" = UnparseC.term @{context} value

( *nth 2 equal_descr_pairs*)

(*+*)val [] = return_discern_typ;

(**)

           switch_type id ts;

"~~~~~ fun switch_type , args:"; val (Const (descr_string, _), ts) = (descr, ts);

(*nth 1 equal_descr_pairs* )

val return_switch_type_TEST = Const (descr_string, ts |> hd |> TermC.lhs |> type_of)

(*+*)val Const ("Input_Descript.Constants", typ) = return_switch_type_TEST

(*+*)val Type ("Real.real", []) = typ

( *nth 2 equal_descr_pairs*)

(*+*)val return_switch_type_TEST = descr

(**)

(*\\\\\ \\\----------- step into make_envs_preconds ----------------------------------------//*)

\<close> ML \<open>(*||||| ||------ contine of_max_variant ------------------------------------------------*)

(*||||| ||------------ contine of_max_variant ------------------------------------------------*)

    val subst_eval_list = make_envs_preconds equal_givens

    val (env_subst, env_eval) = split_list subst_eval_list

\<close> ML \<open>

val xxx = (fn (_, _, _, _, (Cor_TEST _, _)) => true | _ => false)

\<close> ML \<open>

xxx: I_Model.single_TEST -> bool

\<close> ML \<open>

i_model_max

\<close> ML \<open>

length (filter (fn (_, _, _, _, (Cor_TEST _, _)) => true | _ => false) i_model_max)

= length model_patt

\<close> ML \<open>

\<close> ML \<open>

val return_of_max_variant = ((length (filter (fn (_, _, _, _, (Cor_TEST _, _)) => true | _ => false) i_model_max)

        = length model_patt, max_variant, i_model_max),

      env_model, (env_subst, env_eval));

\<close> ML \<open>

return_of_max_variant: (bool * variant * T_TEST) * Env.T * (env_subst * env_eval)

\<close> ML \<open>

\<close> ML \<open>(*\\\\\ \\------ step into of_max_variant --------------------------------------------//*)

(*\\\\\ \\------------ step into of_max_variant --------------------------------------------//*)

      val (i_model_max, env_model, (env_subst, env_eval)) = return_of_max_variant

(*!!!/----- we had a helpful argument for constructing env_model and (env_subst, env_eval)---\*)

      val (i_max_variant, env_model, (env_subst, env_eval)) = (i_model_max, [], ([], []))

(*!!!\----- we had a helpful argument for constructing env_model and (env_subst, env_eval)---/*) 

(*||||||-------------- contine check -----------------------------------------------------*)

      val pres_subst = map (TermC.subst_atomic_all env_subst) pres;

      val pres_subst_other = map (TermC.subst_atomic_all env_model) (map #2 pres_subst);

      val full_subst = if env_eval = [] then pres_subst_other

        else map (TermC.subst_atomic_all env_eval) (map #2 pres_subst_other)

      val evals = map (eval ctxt where_rls) full_subst

val return_ = (i_model_max, env_subst, env_eval)

(*\\\\\\\------------- step into check -------------------------------------------------//*)

val (preok, _) = return_check_OLD;

(*|||||--------------- contine for_problem ---------------------------------------------------*)

    (*if*) dI' = ThyC.id_empty andalso dI = ThyC.id_empty (*else*);

      (*if*) pI' = Problem.id_empty andalso pI = Problem.id_empty (*else*);

val NONE =

     (*case*) find_first (I_Model.is_error o #5) pbl (*of*);

        (*case*)

   Specify.item_to_add (ThyC.get_theory ctxt

            (if dI = ThyC.id_empty then dI' else dI)) oris pbt pbl (*of*);

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

  = ((ThyC.get_theory ctxt (if dI = ThyC.id_empty then dI' else dI)), oris, pbt, pbl);

      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 Pre_Conds.max_variant itms

      val vors = if v = 0 then oris

        else filter ((fn variant =>

            fn (_, variants, m_field, _, _) => member op= variants variant andalso m_field <> "#undef")

          v) oris

(*+*)val "[\n(1, [\"1\", \"2\", \"3\"], #Given, Constants, [\"[r = 7]\"]), \n(2, [\"1\", \"2\", \"3\"], #Find, Maximum, [\"A\"]), \n(3, [\"1\", \"2\", \"3\"], #Find, AdditionalValues, [\"[u]\", \"[v]\"]), \n(4, [\"1\", \"2\", \"3\"], #Relate, Extremum, [\"A = 2 * u * v - u \<up> 2\"]), \n(5, [\"1\", \"2\"], #Relate, SideConditions, [\"[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]\"])]"

(*+*)  = vors |> O_Model.to_string @{context}

      val vits = if v = 0 then itms               (* because of dsc without dat *)

  	    else filter ((fn variant =>

            fn (_, variants, _, _, _) => member op= variants variant)

          v) itms;                                (* itms..vat *)

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

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

(*+*)val "[\n(1 ,[1, 2, 3] ,false ,#Given ,Inc Constants [] , pen2str), \n(2 ,[1, 2, 3] ,false ,#Find ,Inc Maximum , pen2str), \n(3 ,[1, 2, 3] ,false ,#Find ,Inc AdditionalValues [] , pen2str), \n(4 ,[1, 2, 3] ,false ,#Relate ,Inc Extremum , pen2str), \n(5 ,[1, 2] ,false ,#Relate ,Inc SideConditions [] , pen2str)]"

 = icl |> I_Model.to_string @{context}

(*+*)val "(1 ,[1, 2, 3] ,false ,#Given ,Inc Constants [] , pen2str)"

 = hd icl |> I_Model.single_to_string @{context}

(*++*)val feedback = (fn (_, _, _, _, feedback) => feedback) (hd icl)

(*++*)val Const ("Input_Descript.Constants", _) = I_Model.descriptor feedback

(*++*)val [] = I_Model.o_model_values feedback

(*+*)val "[\n(1, [\"1\", \"2\", \"3\"], #Given, Constants, [\"[r = 7]\"]), \n(2, [\"1\", \"2\", \"3\"], #Find, Maximum, [\"A\"]), \n(3, [\"1\", \"2\", \"3\"], #Find, AdditionalValues, [\"[u]\", \"[v]\"]), \n(4, [\"1\", \"2\", \"3\"], #Relate, Extremum, [\"A = 2 * u * v - u \<up> 2\"]), \n(5, [\"1\", \"2\"], #Relate, SideConditions, [\"[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]\"])]"

(*+*)  = vors |> O_Model.to_string @{context}

val SOME ori =

        (*case*) find_first ((fn (_, _, _, _, feedback) => fn (_, _, _, d, ts) =>

           d = I_Model.descriptor feedback andalso subset op = (I_Model.o_model_values feedback, ts))

         (hd icl)) vors (*of*);

(*+*)val "(1, [\"1\", \"2\", \"3\"], #Given, Constants, [\"[r = 7]\"])" =

(*+*)  ori |> O_Model.single_to_string @{context}

(*\\\\\--------------- step into for_problem -----------------------------------------------//*)

(*\\\\---------------- step into find_next_step --------------------------------------------//*)

(*|||----------------- continuing specify_do_next --------------------------------------------*)

val (_, (p_', tac)) = return_find_next_step (*kept for continuing specify_do_next*)

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

(*+*)val Add_Given "Constants [r = 7]" = tac

val _ =

    (*case*) tac (*of*);

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

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

    val (i_model, m_patt) =

       if p_ = Pos.Met then

         (met,

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

       else

         (pbl,

           (if pI = Problem.id_empty then pI' else pI) |> Problem.from_store ctxt |> #model);

      (*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(*, pos*))) =

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

        val (t as (descriptor $ _)) = Syntax.read_term ctxt str

(*+*)val "Constants [r = 7]" = UnparseC.term @{context} t;

        val SOME m_field' =

          (*case*) Model_Pattern.get_field descriptor m_patt (*of*);

           (*if*) m_field <> m_field' (*else*);

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

val ("", ori', all) =

          (*case*) O_Model.contains ctxt m_field o_model t (*of*);

(*+*)val (_, _, _, _, vals) = hd o_model;

(*+*)val "Constants [r = 7]" = UnparseC.term @{context} (@{term Constants} $ (hd vals));

(*+*)if "[\n(1, [\"1\", \"2\", \"3\"], #Given, Constants, [\"[r = 7]\"]), " ^ 

(*+*)    "\n(2, [\"1\", \"2\", \"3\"], #Find, Maximum, [\"A\"]), " ^ 

(*+*)    "\n(3, [\"1\", \"2\", \"3\"], #Find, AdditionalValues, [\"[u]\", \"[v]\"]), " ^ 

(*+*)    "\n(4, [\"1\", \"2\", \"3\"], #Relate, Extremum, [\"A = 2 * u * v - u \<up> 2\"]), " ^ 

(*+*)    "\n(5, [\"1\", \"2\"], #Relate, SideConditions, [\"[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]\"]), " ^ 

(*+*)    "\n(6, [\"3\"], #Relate, SideConditions, [\"[u / 2 = r * sin \<alpha>]\", \"[2 / v = r * cos \<alpha>]\"]), " ^ 

(*+*)    "\n(7, [\"1\"], #undef, FunctionVariable, [\"a\"]), " ^ 

(*+*)    "\n(8, [\"2\"], #undef, FunctionVariable, [\"b\"]), \n(9, [\"3\"], #undef, FunctionVariable, [\"\<alpha>\"]), " ^ 

(*+*)    "\n(10, [\"1\", \"2\"], #undef, Input_Descript.Domain, [\"{0<..<r}\"]), " ^ 

(*+*)    "\n(11, [\"3\"], #undef, Input_Descript.Domain, [\"{0<..<\<pi> / 2}\"]), " ^ 

(*+*)    "\n(12, [\"1\", \"2\", \"3\"], #undef, ErrorBound, [\"\<epsilon> = 0\"])]"

(*+*)= O_Model.to_string @{context} o_model then () else error "o_model CHANGED";

  (*case*) is_notyet_input ctxt i_model all ori' m_patt (*of*);

"~~~~~ fun is_notyet_input , args:"; val (ctxt, itms, all, (i, v, f, d, ts), pbt) =

  (ctxt, i_model, all, ori', m_patt);

val SOME (_, (_, pid)) =

  (*case*) find_first (eq1 d) pbt (*of*);

(*local*)fun eq3 f d (_, _, _, f', itm_) = f = f' andalso d = (I_Model.descriptor itm_);(*local*)

val SOME (_, _, _, _, itm_) =

    (*case*) find_first (eq3 f d) itms (*of*);

val ts' = inter op = (o_model_values itm_) ts;

            (*if*) subset op = (ts, ts') (*else*);

val return_is_notyet_input = ("", 

           ori_2itm itm_ pid all (i, v, f, d, subtract op = ts' ts));

"~~~~~ fun ori_2itm , args:"; val (itm_, pid, all, (id, vt, fd, d, ts)) =

  (itm_, pid, all, (i, v, f, d, subtract op = ts' ts));

    val ts' = union op = (o_model_values itm_) ts;

    val pval = [Input_Descript.join'''' (d, ts')]

    val complete = if eq_set op = (ts', all) then true else false

(*+*)val "Inc Constants [] , pen2str" = itm_ |> I_Model.feedback_to_string @{context}

(*\\\----------------- step into specify_do_next -------------------------------------------//*)

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

val ("ok", (ts as (_, _, _) :: _, _, (pt, p))) = return_do_next

(*|------------------- continue with me_Model_Problem ----------------------------------------*)

val tacis as (_::_) =

        (*case*) ts (*of*);

          val (tac, _, _) = last_elem tacis

val return_Model_Problem = (p, [] : NEW, TESTg_form ctxt (pt, p), tac, Celem.Sundef, pt);

(*//------------------ step into TESTg_form ------------------------------------------------\\*)

"~~~~~ fun TESTg_form , args:"; val (ctxt, ptp) = (ctxt, (pt, p));

    val (form, _, _) =

   ME_Misc.pt_extract ctxt ptp;

"~~~~~ fun pt_extract , args:"; val (ctxt, (pt, (p, p_(*Frm,Pbl*)))) = (ctxt, ptp);

        val ppobj = Ctree.get_obj I pt p

        val f = if Ctree.is_pblobj ppobj then pt_model ppobj p_ else Ctree.get_obj pt_form pt p;

          (*if*) Ctree.is_pblobj ppobj (*then*);

           pt_model ppobj p_;

"~~~~~ fun pt_model , args:"; val ((Ctree.PblObj {probl, spec, origin = (_, spec', hdl), ctxt, ...}), 

  Pbl(*Frm,Pbl*)) = (ppobj, p_);

      val (_, pI, _) = Ctree.get_somespec' spec spec';

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

(*    val where_ = if pI = Problem.id_empty then []*)

(*      else                                       *)

(*        let                                      *)

	          val {where_rls, where_, model, ...} = Problem.from_store ctxt pI

	          val (_, where_) = (*Pre_Conds.*)check ctxt where_rls where_ (model, I_Model.OLD_to_TEST probl)

(*        in where_ end                           *)

	    val allcorrect = I_Model.is_complete probl andalso foldl and_ (true, (map #1 where_))

val return_pt_model = Ctree.ModSpec (allcorrect, Pos.Pbl, hdl, probl, where_, spec)

(*|------------------- continue with TESTg_form ----------------------------------------------*)

val Ctree.ModSpec (spec as (_, p_, _, gfr, where_, _)) =

    (*case*) form (*of*);

    Test_Out.PpcKF (  (Test_Out.Problem [],

 			P_Model.from (Proof_Context.theory_of ctxt) gfr where_));

   P_Model.from (Proof_Context.theory_of ctxt) gfr where_;

"~~~~~ fun from , args:"; val (thy, itms, where_) = ((Proof_Context.theory_of ctxt), gfr, where_);

    fun coll model [] = model

      | coll model ((_, _, _, field, itm_) :: itms) =

        coll (add_sel_ppc thy field model (item_from_feedback thy itm_)) itms;

 val gfr = coll P_Model.empty itms;

"~~~~~ fun coll , args:"; val (model, ((aaa, bbb_,ccc_, field, itm_) :: itms))

  = (P_Model.empty, itms);

(*+*)val 4 = length itms;

(*+*)val itm = nth 1 itms;

           coll P_Model.empty [itm];

"~~~~~ fun coll , iterate:"; val (model, ((aaa, bbb_,ccc_, field, itm_) :: []))

  = (P_Model.empty, [itm]);

          (add_sel_ppc thy field model (item_from_feedback thy itm_));

"~~~~~ fun add_sel_ppc , args:"; val ((_: theory), sel, {Given = gi, Where = wh, Find = fi, With = wi, Relate = re}, x )

  = (thy, field, model, (item_from_feedback thy itm_));

   P_Model.item_from_feedback thy itm_;

"~~~~~ fun item_from_feedback , args:"; val (thy, (I_Model.Inc ((d, ts), _))) = (thy, itm_);

   P_Model.Incompl (UnparseC.term_in_thy thy (Input_Descript.join (d, ts)));

(*\\------------------ step into TESTg_form ------------------------------------------------//*)

(*\------------------- step into me Model_Problem ------------------------------------------//*)

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

(*-------------------- contine me's ----------------------------------------------------------*)

val return_me_add_find_Constants = me nxt p c pt;

                                      val Add_Find "Maximum A" = #4 return_me_add_find_Constants;

(*/------------------- step into me_add_find_Constants -------------------------------------\\*)

"~~~~~ fun me , args:"; val (tac as Add_Given "Constants [r = 7]", p, _(*NEW remove*), pt) =

  (nxt, p, c, pt);

      val ctxt = Ctree.get_ctxt pt p

(*+*)val PblObj {probl = (1, [1, 2, 3], false, "#Given", Inc 

    ((Const ("Input_Descript.Constants", _), []), _)) :: _, ...}  = get_obj I pt (fst p)

(*-------------------------------------------^^--*)

val return_step_by_tactic = (*case*) 

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

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

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

val Applicable.Yes tac' =

    (*case*) Specify_Step.check tac (pt, p) (*of*);

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

Step_Specify.by_tactic tac' ptp;

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

   Specify.by_Add_ "#Given" ct (pt, p);

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

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

(*  val (i_model, m_patt) =*)

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

val return_by_Add_ =

         (pbl,

           (if pI = Problem.id_empty then pI' else pI) |> Problem.from_store ctxt |> #model)

val I_Model.Add i_single =

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

	          val i_model' =

   I_Model.add_single (Proof_Context.theory_of ctxt) i_single i_model;

"~~~~~ fun add_single , args:"; val (thy, itm, model) =

  ((Proof_Context.theory_of ctxt), i_single, i_model);

    fun eq_untouched d (0, _, _, _, itm_) = (d = I_Model.descriptor itm_)

      | eq_untouched _ _ = false

    val model' = case I_Model.seek_ppc (#1 itm) model of

      SOME _ => overwrite_ppc thy itm model (*itm updated in is_notyet_input WN.11.03*)

(*||------------------ contine Step.by_tactic ------------------------------------------------*)

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

val ("ok", (_, _, ptp)) = return_step_by_tactic;

      val (pt, p) = ptp;

        (*case*) 

      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'), []));

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

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

           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, pos as (_, p_)) = (ptp);

    val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,

      spec = refs, ...} = Calc.specify_data (pt, pos);

    val ctxt = Ctree.get_ctxt pt pos;

(*+*)val (1, [1, 2, 3], true, "#Given", Cor ((Const ("Input_Descript.Constants", _), ts ), _)) :: _

  = pbl

(*+*)val "[[r = 7]]" = UnparseC.terms @{context} ts;

(*-----ML-^------^-HOL*)

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

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

           for_problem ctxt oris (o_refs, refs) (pbl, met);

"~~~~~ fun for_problem , args:"; val (ctxt, oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met)) =

  (ctxt, oris, (o_refs, refs), (pbl, met));

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

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

    val {model = pbt, where_rls, where_, ...} = Problem.from_store ctxt cpI;

    val {model = mpc, ...} = MethodC.from_store ctxt cmI

    val (preok, _) =

Pre_Conds.check ctxt where_rls where_ (pbt, I_Model.OLD_to_TEST pbl);

"~~~~~ fun check , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =

  (ctxt, where_rls, where_, (pbt, I_Model.OLD_to_TEST pbl));

      val (_, _, (env_subst, env_eval)) = of_max_variant model_patt i_model;

"~~~~~ fun of_max_variant , args:"; val (model_patt, i_model) = (model_patt, i_model);

    val all_variants =

        map (fn (_, variants, _, _, _) => variants) i_model

        |> flat

        |> distinct op =

    val variants_separated = map (filter_variants' i_model) all_variants

    val sums_corr = map (cnt_corrects) variants_separated

    val sum_variant_s = arrange_args sums_corr (1, all_variants)

    val (_, max_variant) = hd (*..crude decision, up to improvement *)

      (sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s)

    val i_model_max =

      filter (fn (_, variants, _ , _ ,_) => member (op =) variants max_variant) i_model

    val equal_descr_pairs = map (get_equal_descr i_model) model_patt |> flat

    val env_model = make_env_model equal_descr_pairs

    val equal_givens = filter (fn ((m_field, _), _) => m_field = "#Given") equal_descr_pairs

    val subst_eval_list =

           make_envs_preconds equal_givens;

"~~~~~ fun make_envs_preconds , args:"; val (equal_givens) = (equal_givens);

val xxx = (fn ((_, (_, id)), (_, _, _, _, (feedb, _))) =>

           discern_feedback id feedb)

val           ((_, (_, id)), (_, _, _, _, (feedb, _))) = nth 1 equal_givens;

"~~~~~ fun discern_feedback , args:"; val (id, (Model_Def.Cor_TEST ((descr, ts), _))) = (id, feedb);

           discern_typ id (descr, ts);

"~~~~~ fun discern_typ , args:"; val (id, (descr, ts)) = (id, (descr, ts));

(*|------------------- contine me_add_find_Constants -----------------------------------------*)

(*\------------------- step into me_add_find_Constants -------------------------------------//*)

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

(*/########################## before destroying elementwise input of lists ##################\* )

val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "AdditionalValues [u]" = nxt;

val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "AdditionalValues [v]" = nxt;

( *\########################## before destroying elementwise input of lists ##################/*)

val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "AdditionalValues [u, v]" = nxt;

val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Relation "Extremum (A = 2 * u * v - u \<up> 2)" = nxt;

val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Relation "SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" = nxt;

val return_me_Add_Relation_SideConditions

                     = me nxt p c pt;

(*+*)val (_, _, _, Specify_Theory "Diff_App", _, _) = return_me_Add_Relation_SideConditions; (*###############*)

(*/------------------- step into me Add_Relation_SideConditions ----------------------------\\*)

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

      val ctxt = Ctree.get_ctxt pt p;

(**)  val (pt, p) = (**) 

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

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

   (*case*)

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

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

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

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

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

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

      (*case*) tacis (*of*);

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

      Step.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*);

      Step.specify_do_next (pt, input_pos);

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

(*isa------ERROR: Refine_Problem INSTEAD 

            isa2: Specify_Theory "Diff_App"*)

    val (_, (p_', tac as Specify_Theory "Diff_App")) =

(*ERROR------------------^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)

   Specify.find_next_step ptp;

"~~~~~ fun find_next_step , args:"; val (pt, pos as (_, p_)) = (ptp);

    val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,

      spec = refs, ...} = Calc.specify_data (pt, pos);

    val ctxt = Ctree.get_ctxt pt pos;

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

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

val ("dummy", (Pbl, tac as Specify_Theory "Diff_App")) =

(*ERROR------------------^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)

          for_problem ctxt oris (o_refs, refs) (pbl, met);

"~~~~~ fun for_problem , args:"; val (ctxt, oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met)) =

  (ctxt, oris, (o_refs, refs), (pbl, met));

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

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

    val {model = pbt, where_rls, where_, ...} = Problem.from_store ctxt cpI;

    val {model = mpc, ...} = MethodC.from_store ctxt cmI

(*+*)val [Const ("Orderings.ord_class.less", _) $ Const ("Groups.zero_class.zero", _) $

  Free ("fixes", _)] = where_

    val (preok, _) =

 Pre_Conds.check ctxt where_rls where_ (pbt, I_Model.OLD_to_TEST pbl);

(*///----------------- step into check -------------------------------------------------\\*)

"~~~~~ fun check , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =

  (ctxt, where_rls, where_, (pbt, I_Model.OLD_to_TEST pbl));

(*+*)val "[0 < fixes]" = pres |> UnparseC.terms @{context}

(*+*)val "[\"(#Given, (Constants, fixes))\", \"(#Find, (Maximum, maxx))\", \"(#Find, (AdditionalValues, vals))\", \"(#Relate, (Extremum, extr))\", \"(#Relate, (SideConditions, sideconds))\"]"

(*+*)  = model_patt |> Model_Pattern.to_string @{context}

(*+*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor_TEST Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A , pen2str, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T))]"

 = i_model |> I_Model.to_string_TEST @{context}

val return_of_max_variant as (_, _, (env_subst, env_eval)) =

           of_max_variant model_patt i_model

(*+*)val [(Free ("fixes", T1), Free ("r", T2))] = env_subst (*?!? Const*)

(*+*)val Type ("Real.real", []) = T1

(*+*)val Type ("Real.real", []) = T2

(*+*)val [(Free ("r", T2), Const ("Num.numeral_class.numeral", _) $ _)] = env_eval

(*+*)val Type ("Real.real", []) = T2

val (_, _, (env_subst, env_eval)) = return_of_max_variant;

(*|||----------------- contine check -----------------------------------------------------*)

      val pres_subst = map (TermC.subst_atomic_all env_subst) pres;

(*|||----------------- contine check -----------------------------------------------------*)

(*+*)val [(true, Const ("Orderings.ord_class.less", _) $

  Const ("Groups.zero_class.zero", _) $ Free ("r", _))] = pres_subst

      val full_subst = map (fn (bool, t) => (bool, subst_atomic env_eval t)) pres_subst

(*+*)val [(true,

     Const ("Orderings.ord_class.less", _) $ Const ("Groups.zero_class.zero", _) $

       (Const ("Num.numeral_class.numeral", _) $ _))] = full_subst

      val evals = map (eval ctxt where_rls) full_subst

val return_check_OLD = (foldl and_ (true, map fst evals), pres_subst)

(*\\\----------------- step into check -------------------------------------------------\\*)

    val (preok as true, _) = return_check_OLD

(*+---------------^^^^*)

(*\\------------------ step into do_next ---------------------------------------------------\\*)

(*\------------------- step into me_Add_Relation_SideConditions ----------------------------//*)

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

                                      val Specify_Theory "Diff_App" = nxt;

val return_me_Specify_Theory

                     = me nxt p c pt; val Specify_Problem ["univariate_calculus", "Optimisation"] = #4 return_me_Specify_Theory;

(*/------------------- step into me Specify_Theory -----------------------------------------\\*)

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

      val ctxt = Ctree.get_ctxt pt p;

(*      val (pt, p) = *)

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

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

val return_Step_by_tactic =

      Step.by_tactic tac (pt, p);

(*//------------------ step into Step_by_tactic --------------------------------------------\\*)

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

    (*case*) Specify_Step.check tac (pt, p) (*of*);

(*||------------------ contine Step_by_tactic ------------------------------------------------*)

(*\\------------------ step into Step_by_tactic --------------------------------------------//*)

val ("ok", (_, _, ptp)) = return_Step_by_tactic;

(*|------------------- continue me Specify_Theory --------------------------------------------*)

val ("ok", (ts as (_, _, _) :: _, _, _)) =

    (*case*)

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

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

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

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

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

      Step.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*);

      Step.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

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

    (*case*) tac (*of*);

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

(*+*)val Specify_Theory "Diff_App" = tac;

"~~~~~ fun by_tactic_input , args:"; val ((Tactic.Specify_Theory dI), (pt, pos as (_, Pbl)))

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

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

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

          (oris, dI, dI', pI', probl, ctxt)

	    val thy = ThyC.get_theory ctxt (if dI' = ThyC.id_empty then dI else dI');

      val {model, where_, where_rls,...} = Problem.from_store (Ctree.get_ctxt pt pos) pI

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

(*\------------------- step into me Specify_Theory -----------------------------------------//*)

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

val return_me_Specify_Problem (* keep for continuing me *)

                     = me nxt p c pt; val Specify_Method ["Optimisation", "by_univariate_calculus"] = #4 return_me_Specify_Problem;

(*/------------------- step into me Specify_Problem ----------------------------------------\\*)

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

      val ctxt = Ctree.get_ctxt pt p

(** )  val ("ok", (_, _, ptp as (pt, p))) =( **)

(**)    val return_by_tactic =(**) (*case*)

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

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

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

    (*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_Problem pID), (pt, pos as (p, _)))

  = (tac, (ctree, pos));

		    val (oris, dI, pI, dI', pI', itms) = case Ctree.get_obj I pt p of

		      Ctree.PblObj {origin = (oris, (dI, pI, _), _), spec = (dI', pI', _), probl = itms, ...}

		        => (oris, dI, pI, dI', pI', itms)

	      val thy = ThyC.get_theory ctxt (if dI' = ThyC.id_empty then dI else dI');

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

val ("ok", (_, _, ptp as (pt, p))) = return_by_tactic (* kept for continuing me *);

      (*case*)

      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'), []));

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

      Step.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*);

      Step.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

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

val _ =

    (*case*) tac (*of*);

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

"~~~~~ fun by_tactic_input , args:"; val ((Tactic.Specify_Method id), (pt, pos))

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

      val (o_model, ctxt, i_model) =

Specify_Step.complete_for id (pt, pos);

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

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

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

    val ctxt = Ctree.get_ctxt ctree pos

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

    val {model = m_patt, where_, where_rls, ...} = MethodC.from_store ctxt 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)

    val thy = ThyC.get_theory ctxt dI

    val (_, (i_model, _)) = M_Match.match_itms_oris ctxt i_prob (m_patt, where_, where_rls) o_model';

(*\------------------- step into me Specify_Problem ----------------------------------------//*)

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

val return_me_Add_Given_FunctionVariable

                     = me nxt p c pt; val Add_Given "FunctionVariable a" = #4 return_me_Add_Given_FunctionVariable;

(*/------------------- step into me Specify_Method -----------------------------------------\\*)

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

      val ctxt = Ctree.get_ctxt pt p

      val (pt, p) = 

  	    (*Step.by_tactic is here for testing by me; do_next would suffice in me*)

  	    case Step.by_tactic tac (pt, p) of

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

         (*case*)

      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'), []));

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

      Step.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*);

      Step.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, pos as (_, p_))) = (ptp);

    val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,

      spec = refs, ...} = Calc.specify_data (pt, pos);

    val ctxt = Ctree.get_ctxt pt pos;

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

        (*if*) p_ = Pos.Pbl (*else*);

   Specify.for_method ctxt oris (o_refs, refs) (pbl, met);

"~~~~~ fun for_method , args:"; val (ctxt, oris, ((dI', pI', mI'), (dI, pI, mI)), (_, met))

  = (ctxt, oris, (o_refs, refs), (pbl, met));

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

    val {model, where_rls, where_, ...} = MethodC.from_store ctxt cmI;    (*..MethodC ?*)

    val (preok, _) = Pre_Conds.check ctxt where_rls where_ (model, I_Model.OLD_to_TEST met);

val NONE =

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

      (*case*)

   Specify.item_to_add (ThyC.get_theory ctxt 

     (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 ctxt (if dI = ThyC.id_empty then dI' else dI)), oris, mpc, met);

(*\------------------- step into me Specify_Method -----------------------------------------//*)