wneuper/isa: test/Tools/isac/Test_Theory.thy@f10bbfb2b3bb

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

     2 theory Test_Theory imports "$ISABELLE_ISAC/Build_Isac"

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

     4 begin

     5 ML_file "$ISABELLE_ISAC/BaseDefinitions/libraryC.sml"

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

     8 text \<open>

     9   declare [[show_types]]

    10   declare [[show_sorts]]

    11   find_theorems "?a <= ?a"

    13   print_theorems

    14   print_facts

    15   print_statement ""

    16   print_theory

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

    18   declare [[ML_print_depth = 999]]

    19   declare [[ML_exception_trace]]

    20 \<close>

    21 (** )

    22   (@{print} {a = "dict_cond_ord ([], [])"}; EQUAL)

    23 ( **)

    24 ML \<open>

    25 \<close> ML \<open>

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

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

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

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

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

    31 "xx"

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

    34 \<close> ML \<open> (*--------------locate below ~~~ fun XXXXX, asap shift into separate section above ----*)

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

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

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

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

    40 \<close> ML \<open> (*//----------- setup test data for XXXXX -------------------------------------------\\*)

    41 (*//------------------ setup test data for XXXXX -------------------------------------------\\*)

    42 (*\\------------------ setup test data for XXXXX -------------------------------------------//*)

    43 \<close> ML \<open> (*\\----------- setup test data for XXXXX -------------------------------------------//*)

    45 val return_XXXXX = "XXXXX"

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

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

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

    49 (*||------------------ contine.. XXXXX -------------------------------------------------------*)

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

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

    52 val "XXXXX" = return_XXXXX;

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

    56 \<close> ML \<open>(*//############ @ {context} within fun XXXXX ----------------------------------\\*)

    57 (*//################## @ {context} within fun XXXXX ---------------------------------------\\* )

    58 (*-------------------- there must not be > ML < inbetween-------------------------------------*)

    59 ( *\\################# @ {context} within fun XXXXX ----------------------------------------//*)

    60 \<close> ML \<open>(*\\############ @ {context} within fun XXXXX -----------------------------------//*)

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

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

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

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

    68 \<close> ML \<open>

    69 \<close>

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

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

    73 ML \<open>

    74 \<close> ML \<open>

    76 \<close> ML \<open>

    77 \<close>

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

    80 section \<open>===== --- build fun item_to_add ---================================================\<close>

    81 ML \<open>

    82 \<close> ML \<open>

    83 open Ctree;

    84 open Pos;

    85 open TermC;

    86 open Istate;

    87 open Tactic;

    88 open I_Model;

    89 open P_Model

    90 open Rewrite;

    91 open Step;

    92 open LItool;

    93 open LI;

    94 open Test_Code

    95 open Specify

    96 open ME_Misc

    97 open Pre_Conds;

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

    99 (*//------------------ build fun item_to_add -----------------------------------------------\\*)

   100 \<close> ML \<open> (*shift this block up in separate section a.s.a.p*)

   101 \<close> ML \<open>

   102 \<close> ML \<open>(*\<longrightarrow> model-def.sml*)

   103 fun some_input (Cor_TEST _) = true

   104   | some_input (Inc_TEST (_, _::_)) = true

   105   | some_input (Syn_TEST _) = true

   106   | some_input _ = false

   107 ;

   108 some_input: feedback_TEST -> bool

   109 \<close> ML \<open>

   110 (*OLD*)

   111 fun cnt_corrects i_model =

   112   fold (curry op +) (map (fn (_, _, _, _, (Cor_TEST _, _)) => 1 | _ => 0) i_model) 0;

   113 (*---* )

   114 fun cnt_correct i_model =

   115   fold (curry op +) (map (fn (_, _, _, _, (feedb, _)) =>

   116     if some_input feedb then 1 else 0) i_model) 0;

   117 ( *NEW*)

   118 \<close> ML \<open>(*\<longrightarrow> model-def.sml*)

   119 fun arrange_args [] _ = []

   120   | arrange_args (sum :: ss) (cnt, all) = (sum, nth cnt all) :: (arrange_args ss (cnt + 1, all))

   121 \<close> ML \<open>

   122 \<close> ML \<open>(*\<longrightarrow> model-def.sml*)

   123 (*OLD*)

   124 (*---*)

   125 fun max_variants o_model i_model =

   126   let

   127 (*OLD*)

   128     val all_variants =

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

   130         |> flat

   131         |> distinct op =

   132 (*---* )

   133     val all_variants = (*we do not count empty items (not yet input)*)

   134         map (fn (_, _, _, _, (Inc_TEST (_, []), _)) => []

   135           | (_, variants, _, _, _) => variants) i_model

   136       |> flat

   137       |> distinct op =

   138 ( *NEW*)

   139     val variants_separated = map (filter_variants' i_model) all_variants

   140     val sums_corr = map (cnt_corrects) variants_separated

   141     val sum_variant_s = arrange_args sums_corr (1, all_variants)

   143     val max_first = rev (sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s)

   144     val maxes = filter (fn (cnt, _) => curry op = (fst (hd max_first)) cnt) max_first

   145       |> map snd

   146   in

   147     if maxes = []

   148     then map (fn (_, variants, _, _, _) => variants) o_model

   149         |> flat

   150         |> distinct op =

   151     else maxes

   152   end

   153 \<close> ML \<open> (*\<longrightarrow> model-def.sml*)

   154 fun descriptor_exists descr feedb =

   155   case get_dscr' feedb of

   156     SOME descr' => descr' = descr

   157   | NONE => raise ERROR "existing_description NONE"

   158 ;

   159 descriptor_exists: descriptor -> I_Model.feedback_TEST -> bool

   160 \<close> ML \<open>

   161 \<close> ML \<open> (*\<longrightarrow> i-model.sml*)

   162 (*in item_to_add prefers items with incomplete lists *)

   163 fun prior_to_select i_model =

   164   let

   165     (* ? problem with Const ("Input_Descript.solutions", _) ? *)

   166     val filt = (fn (_, _, _, _, (Inc_TEST (descr, _::_) , _)) => Model_Pattern.is_list_descr descr

   167       | _ => false)

   168   in

   169     (filter filt i_model) @ (filter_out filt i_model)

   170   end

   171 ;

   172 prior_to_select: I_Model.T_TEST -> I_Model.T_TEST

   173 \<close> ML \<open>

   174 (*

   175   Select an item from o_model not yet input to i_model and add it to i_model.

   176   Prefer items with incomplete lists.

   177 *)

   178 fun item_to_add ctxt o_model i_model =

   179   let

   180     val m_field = "#Given"

   181     val term_as_string = "Constants [r = 7]"

   182   in

   183     SOME (m_field, term_as_string)

   184   end

   185 \<close> ML \<open>

   186 item_to_add: Proof.context -> O_Model.T -> Model_Pattern.T ->

   187     (Model_Def.m_field * TermC.as_string) option

   188 \<close> ML \<open>

   189 \<close> ML \<open>

   190 (*\\------------------ build fun item_to_add -----------------------------------------------//*)

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

   193 \<close> ML \<open>

   194 \<close>

   196 (*ML_file "Minisubpbl/100a-init-rootpbl-Maximum.sml"*)

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

   198 section \<open>===== "Minisubpbl/100a-init-rootpbl-Maximum.sml" ==================================\<close>

   199 ML \<open>

   200 \<close> ML \<open>

   201 (* Title:  "Minisubpbl/100a-init-rootpbl-Maximum.sml"

   202    Author: Walther Neuper 1105

   203    (c) copyright due to lincense terms.

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

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

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

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

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

   212   and use Sidekick for orientation.

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

   214 *)

   216 open Ctree;

   217 open Pos;

   218 open TermC;

   219 open Istate;

   220 open Tactic;

   221 open I_Model;

   222 open P_Model

   223 open Rewrite;

   224 open Step;

   225 open LItool;

   226 open LI;

   227 open Test_Code

   228 open Specify

   229 open ME_Misc

   230 open Pre_Conds;

   232 val (_(*example text*),

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

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

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

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

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

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

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

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

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

   242    refs as ("Diff_App",

   243      ["univariate_calculus", "Optimisation"],

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

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

   247 val c = [];

   248 val return_init_calc =

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

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

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

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

   253     val thy = thy_id |> ThyC.get_theory ctxt

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

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

   256 	  val f =

   257            TESTg_form ctxt (pt,p);

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

   259     val (form, _, _) =

   260    ME_Misc.pt_extract ctxt ptp;

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

   262         val ppobj = Ctree.get_obj I pt p

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

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

   265            pt_model ppobj p_ ;

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

   267   (ppobj, p_);

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

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

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

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

   272 	          val (_, where_) =

   273  Pre_Conds.check ctxt where_rls where_

   274               (model, I_Model.OLD_to_TEST probl);

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

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

   277       val (env_model, (env_subst, env_eval)) =

   278            make_environments model_patt i_model;

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

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

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

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

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

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

   286 (*+*)val [] = probl

   288 val return_me_Model_Problem =

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

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

   291 (*/------------------- step into me_Model_Problem ------------------------------------------\\*)

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

   293       val ctxt = Ctree.get_ctxt pt p

   294 val return_by_tactic = case

   295       Step.by_tactic tac (pt,p) of

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

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

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

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

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

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

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

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

   306 Specify_Step.check tac (ctree, pos);

   307 "~~~~~ fun check , args:"; val (Tactic.Model_Problem, (pt, pos as (p, _))) =

   308   (tac, (ctree, pos));

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

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

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

   312 	      val pbl = I_Model.init_TEST o_model model_patt;

   314 val return_check =

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

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

   317 val (pt, p) = return_by_tactic;

   319 val return_do_next = (*case*)

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

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

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

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

   324     val pIopt = get_pblID (pt,ip);

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

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

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

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

   330       Step.switch_specify_solve p_ (pt, ip);

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

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

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

   335       Step.specify_do_next (pt, input_pos);

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

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

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

   340 val return_find_next_step = (*keep for continuing specify_do_next*)

   341    Specify.find_next_step ptp;

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

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

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

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

   346     val ctxt = Ctree.get_ctxt pt pos;

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

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

   350 \<close> ML \<open>

   351 val return_for_problem as ("dummy", (Pbl, Add_Given "Constants [r = 7]")) =

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

   353 \<close> ML \<open>

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

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

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

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

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

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

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

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

   363     val return_check =

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

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

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

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

   368       val return_make_environments =

   369            make_environments model_patt i_model;

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

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

   372   (model_patt, i_model);

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

   375  = i_model |> I_Model.to_string_TEST @{context}

   376     val all_variants =

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

   378         |> flat

   379         |> distinct op =

   380     val variants_separated = map (filter_variants' i_model) all_variants

   381     val sums_corr = map (Model_Def.cnt_corrects) variants_separated

   382     val sum_variant_s = Model_Def.arrange_args sums_corr (1, all_variants)

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

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

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

   386     val i_model_max =

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

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

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

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

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

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

   393 (*!!!*)val equal_descr_pairs =

   394   (patt,

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

   396   :: tl equal_descr_pairs

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

   399     val env_model = make_env_model equal_descr_pairs;

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

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

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

   404        => (mk_env_model id feedb));

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

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

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

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

   410     val subst_eval_list = make_envs_preconds equal_givens

   411 val return_make_envs_preconds =

   412            make_envs_preconds equal_givens;

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

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

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

   416 ;

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

   418 val return_discern_feedback =

   419            discern_feedback id feedb;

   420 (*nth 1 equal_descr_pairs* )

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

   422 ( *nth 2 equal_descr_pairs*)

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

   425 (*nth 1 equal_descr_pairs* )

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

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

   428 (*+*)val true = typ1 = typ2

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

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

   431 ( *nth 2 equal_descr_pairs*)

   432 (*+*)val [] = return_discern_feedback

   434 val return_discern_typ =

   435            discern_typ id (descr, ts);

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

   437 (*nth 1 equal_descr_pairs* )

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

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

   440 (*+*)val true = typ1 = typ2

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

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

   443 ( *nth 2 equal_descr_pairs*)

   444 (*+*)val [] = return_discern_typ;

   445 (**)

   446            switch_type id ts;

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

   449 (*nth 1 equal_descr_pairs* )

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

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

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

   454 ( *nth 2 equal_descr_pairs*)

   455 (*+*)val return_switch_type_TEST = descr

   456 (**)

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

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

   459     val subst_eval_list = make_envs_preconds equal_givens

   460     val (env_subst, env_eval) = split_list subst_eval_list

   461 val make_environments = (i_model_max, env_model, (env_subst, env_eval)); (*GOON*)

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

   463       val (i_model_max, env_model, (env_subst, env_eval)) = make_environments

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

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

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

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

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

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

   470       val full_subst = if env_eval = [] then pres_subst_other

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

   472       val evals = map (eval ctxt where_rls) full_subst

   473 val return_ = (i_model_max, env_subst, env_eval)

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

   475 val (preok, _) = return_check;

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

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

   479 val false =

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

   481 val false =

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

   483 val NONE =

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

   486 \<close> ML \<open>

   487 (**)val return_item_to_add =(**)

   488 (** )val SOME (fd, ct') as ("#Given", "Constants [r = 7]") =( **)

   489   (*case*) item_to_add (ThyC.get_theory ctxt

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

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

   492 (*///// /--------------- step into item_to_add -----------------------------------------------\\*)

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

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

   495 \<close> ML \<open>

   496 (*+*)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]\"]), \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\"])]"

   497  = oris |> O_Model.to_string @{context}

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

   499  = pbt |> Model_Pattern.to_string @{context}

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

   501  = itms |> I_Model.to_string @{context}

   502 \<close> ML \<open>

   503 \<close> ML \<open>

   504 "~~~~~ fun item_to_add NEW, args:"; val (ctxt, o_model, i_model) =

   505   (@{context}, oris, I_Model.OLD_to_TEST itms)

   506 \<close> ML \<open>

   507 \<close> ML \<open>

   508 \<close> ML \<open>

   509 val return_item_to_add_step = SOME (I_Model.get_field_term thy ori (hd icl));

   510 "~~~~~ fun item_to_add NEW, args:"; val (ctxt, o_model, i_model) =

   511   (@{context}, oris, I_Model.OLD_to_TEST itms);

   512 "~~~~~ fun item_to_add NEW CODE BUILD, args:"; val (ctxt, o_model, i_model) =

   513   (@{context}, oris, I_Model.OLD_to_TEST

   514     (Library.take 4 itms @

   515       [(5, [3], false, "#Relate", Inc ((@{term SideConditions},

   516         [@{term "(u::real) / 2 = r * sin \<alpha>"}]), (TermC.empty, []) ))]))

   517 \<close> ML \<open>

   518 (*+*)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, [3], false ,#Relate, (Inc_TEST SideConditions (u div 2 = r * sin \<alpha>) , pen2str, Position.T))]"

   519  = i_model |> I_Model.to_string_TEST @{context}

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

   521 (*//------------------ build fun max_variants_TEST -----------------------------------------\\*)

   522 \<close> ML \<open>

   523       val all_variants as [3] =

   524           map (fn (_, _, _, _, (Inc_TEST (_, []), _)) => []

   525             | (_, variants, _, _, _) => variants) i_model

   526         |> flat

   527         |> distinct op =

   528 \<close> ML \<open>

   529       val variants_separated = map (filter_variants' i_model) all_variants

   530 \<close> ML \<open>

   531 (*+*)length variants_separated

   532 \<close> ML \<open>

   533 \<close> ML \<open>

   534       val sums_corr as [1] = map (Model_Def.cnt_corrects) variants_separated

   535 \<close> ML \<open>

   536       val sum_variant_s as [(1, 3)] = arrange_args sums_corr (1, all_variants)

   537 \<close> ML \<open>

   538       val max_first as [(1, 3)] = rev (sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s)

   539 \<close> ML \<open>

   540       val maxes as [3] = filter (fn (cnt, _) => curry op = (fst (hd max_first)) cnt) max_first

   541         |> map snd

   542 \<close> ML \<open>

   543 val return_max_variants = maxes

   544 \<close> ML \<open>

   545 (*\\------------------ build fun max_variants_TEST -----------------------------------------//*)

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

   547 \<close> ML \<open>

   548 \<close> ML \<open>(*for that --vvvvvv--- reason we probably need a new max_variants_TEST ---^^^^^*)

   549     val max_vnt as 3 = last_elem ((*Model_Def.*)max_variants_TEST o_model i_model)

   550 \<close> ML \<open>

   551     val o_vnts = filter (fn (_, vnts, _, _, _) => member op= vnts max_vnt) o_model

   552 \<close> ML \<open>

   553     val i_to_select = i_model

   554       |> filter_out (fn (_, vnts, _, _, (Cor_TEST _, _)) => member op= vnts max_vnt | _ => false)

   555       |> prior_to_select

   556       |> hd

   557 \<close> ML \<open>

   558 get_dscr';

   559 ori_2itm: feedback -> descriptor -> Model_Def.values -> O_Model.single -> I_Model.single;

   560 \<close> text \<open>

   561 val (max_vnt, descr, ts) = (3, @{term SideConditions}, [@{term "(u::real) / 2 = r * sin \<alpha>"}])

   562 (*^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)

   563 \<close> ML \<open>

   564 "~~~~~ fun fill_from_o , args:"; val (o_model, (i, vnts, bool, m_field, (feedb, pos))) =

   565   (o_vnts, (*i_to_select*) (1, [1, 2, 3], false, "#Given", (Inc_TEST (descr, ts), Position.none)));

   566 \<close> ML \<open>

   567     val all_values =

   568       case find_first (fn (_, _, _, descr', _) => descriptor_exists descr' feedb) o_model of

   569         SOME (_, _, _, _, ts) => ts

   570       | NONE => raise ERROR "xxxxx"

   571 \<close> ML \<open>

   572 (*+*)val xxx = all_values |> UnparseC.terms @{context}

   573 \<close> text \<open>

   574       if Model_Pattern.is_list_descr descr

   575       then

   576         let

   577           val miss = subtract op= (I_Model.values_TEST feedb) (*TODO*)

   578         in

   579          []

   580         end

   581       else all_values

   582 \<close> ML \<open>

   583 \<close> ML \<open>

   584 \<close> ML \<open>

   585 \<close> ML \<open> (*if Model_Pattern.is_list_descr*)

   586 val (o_ts, i_ts) = ([1,2,3], [2,3])

   587 \<close> ML \<open>

   588     val miss = subtract op= i_ts o_ts

   589 \<close> ML \<open>

   590 \<close> ML \<open>

   591 \<close> ML \<open>

   592 \<close> ML \<open>

   593 \<close> ML \<open>

   594 (*o_model contains appropriate variants only. Observe inclomplete lists *)

   595 fun fill_from_o o_model (i, vnts, bool, m_field, (feedb, pos)) =

   596   let

   597     val all_ts =

   598       case find_first (fn (_, _, _, descr', _) => descr' = (*feedb*) descr) o_model of

   599         SOME (_, _, _, _, ts) => ts

   600       | NONE => raise ERROR "xxxxx"

   601   in

   602     123

   603   end

   604 \<close> ML \<open>

   605 \<close> ML \<open> (*----------^^^ new code --------------------------------------------------------------*)

   606 \<close> ML \<open>

   607 (*+*)val SOME ("#Given", "Constants [r = 7]") = return_item_to_add_step

   608 val true = return_item_to_add_step = return_item_to_add

   609 (*\\\\\ \------------- step into item_to_add -----------------------------------------------//*)

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

   611 val SOME (fd, ct') = return_item_to_add

   613 \<close> ML \<open>(*|||||--------- continue.. for_problem ------------------------------------------------*)

   614 (*|||||--------------- continue.. for_problem ------------------------------------------------*)

   615 val return_for_problem_step as ("dummy", (Pbl, Add_Given "Constants [r = 7]"))

   616   = ("dummy", (Pos.Pbl, P_Model.mk_additem fd ct'))

   617 (** )return_for_problem_step = return_for_problem( *..would require equality types*)

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

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

   620 val return_find_next_step = return_for_problem

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

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

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

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

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

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

   628 val _ =

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

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

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

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

   635    Specify.by_Add_ "#Given" ct ptp;

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

   637   ("#Given", ct, ptp);

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

   639     val (i_model, m_patt) =

   640        if p_ = Pos.Met then

   641          (met,

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

   643        else

   644          (pbl,

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

   647       (*case*)

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

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

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

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

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

   655         val SOME m_field' =

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

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

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

   661 val ("", ori', all) =

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   689 val return_is_notyet_input = ("",

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

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

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

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

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

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

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

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

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

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

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

   704 val tacis as (_::_) =

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

   706           val (tac, _, _) = last_elem tacis

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

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

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

   712     val (form, _, _) =

   713    ME_Misc.pt_extract ctxt ptp;

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

   715         val ppobj = Ctree.get_obj I pt p

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

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

   719            pt_model ppobj p_;

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

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

   722       val (_, _, met_id) = References.select_input o_spec spec

   723       val (allcorr, _) = Pre_Conds.check_internal ctxt (I_Model.OLD_to_TEST probl) (Pos.Met, met_id)

   724 val return_pt_model = Ctree.ModSpec (allcorr, Pos.Pbl, hdl, probl, (*where_*)[(*Problem.from_store in check*)], spec)

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

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

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

   729     Test_Out.PpcKF (  (Test_Out.Problem [],

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

   732 \<close> ML \<open>

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

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

   735     fun coll model [] = model

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

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

   739  val gfr = coll P_Model.empty itms;

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

   741   = (P_Model.empty, itms);

   743 (*+*)val 4 = length itms;

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

   746            coll P_Model.empty [itm];

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

   748   = (P_Model.empty, [itm]);

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

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

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

   754    P_Model.item_from_feedback thy itm_;

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

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

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

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

   759 (*\------------------- step into me_Model_Problem ------------------------------------------//*)

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

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

   763 val return_me_add_find_Constants = me nxt p c pt;

   764                                       val Add_Find "Maximum A" = #4 return_me_add_find_Constants;

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

   767 \<close> ML \<open>

   768 \<close>

   770 (*ML_file "Minisubpbl/150a-add-given-Maximum.sml"*)

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

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

   773 ML \<open>

   774 \<close> ML \<open>

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

   776    Author: Walther Neuper 1105

   777    (c) copyright due to lincense terms.

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

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

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

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

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

   786   and use Sidekick for orientation.

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

   788 *)

   790 open Ctree;

   791 open Pos;

   792 open TermC;

   793 open Istate;

   794 open Tactic;

   795 open I_Model;

   796 open P_Model

   797 open Rewrite;

   798 open Step;

   799 open LItool;

   800 open LI;

   801 open Test_Code

   802 open Specify

   803 open ME_Misc

   804 open Pre_Conds;

   806 val (_(*example text*),

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

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

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

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

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

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

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

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

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

   816    refs as ("Diff_App",

   817      ["univariate_calculus", "Optimisation"],

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

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

   821 val c = [];

   822 val return_init_calc =

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

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

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

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

   827     val thy = thy_id |> ThyC.get_theory ctxt

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

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

   830 	  val f =

   831            TESTg_form ctxt (pt,p);

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

   833     val (form, _, _) =

   834    ME_Misc.pt_extract ctxt ptp;

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

   836         val ppobj = Ctree.get_obj I pt p

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

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

   839            pt_model ppobj p_ ;

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

   841   (ppobj, p_);

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

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

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

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

   846 	          val (_, where_) =

   847  Pre_Conds.check ctxt where_rls where_

   848               (model, I_Model.OLD_to_TEST probl);

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

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

   851       val (env_model, (env_subst, env_eval)) =

   852            make_environments model_patt i_model;

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

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

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

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

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

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

   860 (*+*)val [] = probl

   862 val (p, _, f, nxt, _, pt) = me nxt p c pt; val Add_Given "Constants [r = 7]" = #4 return_me_Model_Problem;

   863 val return_me_add_find_Constants

   864                           = me nxt p c pt; val Add_Find "Maximum A" = #4 return_me_add_find_Constants;

   865 \<close> ML \<open>

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

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

   868   (nxt, p, c, pt);

   869       val ctxt = Ctree.get_ctxt pt p

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

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

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

   873 val return_step_by_tactic = (*case*)

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

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

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

   877 val Applicable.Yes tac' =

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

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

   880 Step_Specify.by_tactic tac' ptp;

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

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

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

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

   887 val false =

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

   889 val (i_model, m_patt) =

   890          (pbl,

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

   892 val I_Model.Add i_single =

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

   895 	          val i_model' =

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

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

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

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

   900       | eq_untouched _ _ = false

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

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

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

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

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

   908       val (pt, p) = ptp;

   909         (*case*)

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

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

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

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

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

   915 val _ =

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

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

   919            switch_specify_solve p_ (pt, ip);

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

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

   923            specify_do_next (pt, input_pos);

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

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

   926    Specify.find_next_step ptp;

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

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

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

   930     val ctxt = Ctree.get_ctxt pt pos;

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

   933   = pbl

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

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

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

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

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

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

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

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

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

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

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

   948     val (preok, _) =

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

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

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

   953       val (_, (env_subst, env_eval)) = Pre_Conds.make_environments model_patt i_model;

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

   955     val all_variants =

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

   957         |> flat

   958         |> distinct op =

   959     val variants_separated = map (filter_variants' i_model) all_variants

   960     val sums_corr = map (Model_Def.cnt_corrects) variants_separated

   961     val sum_variant_s = Model_Def.arrange_args sums_corr (1, all_variants)

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

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

   964     val i_model_max =

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

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

   967     val env_model = make_env_model equal_descr_pairs

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

   970     val subst_eval_list =

   971            make_envs_preconds equal_givens;

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

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

   974            discern_feedback id feedb)

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

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

   978            discern_typ id (descr, ts);

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

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

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

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

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

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

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

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

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

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

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

   991 val return_me_Add_Relation_SideConditions

   992                      = me nxt p c pt;

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

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

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

   996       val ctxt = Ctree.get_ctxt pt p;

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

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

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

  1001    (*case*)

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

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

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

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

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

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

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

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

  1011       Step.switch_specify_solve p_ (pt, ip);

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

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

  1014       Step.specify_do_next (pt, input_pos);

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

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

  1017             isa2: Specify_Theory "Diff_App"*)

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

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

  1020    Specify.find_next_step ptp;

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

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

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

  1024     val ctxt = Ctree.get_ctxt pt pos;

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

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

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

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

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

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

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

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

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

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

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

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

  1039   Free ("fixes", _)] = where_

  1041     val (preok, _) =

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

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

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

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

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

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

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

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

  1050  = i_model |> I_Model.to_string_TEST @{context}

  1052 val return_make_environments as (_, (env_subst, env_eval)) =

  1053            Pre_Conds.make_environments model_patt i_model

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

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

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

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

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

  1062 val (_, (env_subst, env_eval)) = return_make_environments;

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

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

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

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

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

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

  1071 (*+*)val [(true,

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

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

  1075       val evals = map (eval ctxt where_rls) full_subst

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

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

  1079     val (preok as true, _) = return_check_OLD

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

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

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

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

  1084                                       val Specify_Theory "Diff_App" = nxt;

  1086 val return_me_Specify_Theory

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

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

  1089 (*/------------------- step into me_Specify_Theory -----------------------------------------\\*)

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

  1091       val ctxt = Ctree.get_ctxt pt p;

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

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

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

  1095 val return_Step_by_tactic =

  1096       Step.by_tactic tac (pt, p);

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

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

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

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

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

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

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

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

  1108     (*case*)

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

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

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

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

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

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

  1115 val _ =

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

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

  1119       Step.switch_specify_solve p_ (pt, ip);

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

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

  1123       Step.specify_do_next (pt, input_pos);

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

  1125     val (_, (p_', tac)) = Specify.find_next_step ptp

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

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

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

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

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

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

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

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

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

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

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

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

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

  1140 (*\------------------- step into me_Specify_Theory -----------------------------------------//*)

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

  1143 val return_me_Specify_Problem (* keep for continuing me *)

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

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

  1146 (*/------------------- step into me_Specify_Problem ----------------------------------------\\*)

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

  1148       val ctxt = Ctree.get_ctxt pt p

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

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

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

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

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

  1156     (*case*)

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

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

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

  1161 Specify_Step.check tac (ctree, pos);

  1162 "~~~~~ fun check , args:"; val ((Tactic.Specify_Problem pID), (pt, pos as (p, _)))

  1163   = (tac, (ctree, pos));

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

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

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

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

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

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

  1171       (*case*)

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

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

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

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

  1176 val _ =

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

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

  1180       Step.switch_specify_solve p_ (pt, ip);

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

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

  1184       Step.specify_do_next (pt, input_pos);

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

  1186     val (_, (p_', tac)) = Specify.find_next_step ptp

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

  1188 val _ =

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

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

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

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

  1195 (**)val return_complete_for =(**)

  1196 (** )  val (o_model, ctxt, i_model) =( **)

  1197 Specify_Step.complete_for id (pt, pos);

  1198 (*//------------------ step into complete_for ----------------------------------------------\\*)

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

  1201 (*+*)val ["Optimisation", "by_univariate_calculus"] = mID

  1202 (*OLD*  )

  1203     val {origin = (o_model, _, _), probl = i_prob, ctxt,

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

  1205     val {model = m_patt, where_, where_rls, ...} = MethodC.from_store ctxt mID

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

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

  1208 ( *---*)

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

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

  1211     val ctxt = Ctree.get_ctxt ctree pos

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

  1213     val {model = m_patt, where_, where_rls, ...} = MethodC.from_store ctxt mID

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

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

  1216 (*NEW*)

  1218 (**)val return_match_itms_oris = (**)

  1219 (** )val (_, (i_model, _)) = ( **)

  1220 (*OLD* )

  1221    M_Match.match_itms_oris ctxt i_prob (m_patt, where_, where_rls) o_model';

  1222 ( *---*)

  1223      M_Match.match_itms_oris ctxt o_model' (I_Model.OLD_to_TEST i_prob, I_Model.OLD_to_TEST i_prob)

  1224               (m_patt, where_, where_rls);

  1225 (*NEW*)

  1226 \<close> ML \<open>(*//############ @ {context} within fun match_itms_oris ------------------------------\\*)

  1227 (*//################## @ {context} within fun match_itms_oris -----------------------------\\*)

  1228 (*///----------------- step into match_itms_oris -------------------------------------------\\*)

  1229 "~~~~~ fun match_itms_oris, args:"; val (ctxt, o_model, (pbl_imod, met_imod), (m_patt, where_, where_rls)) =

  1230   (ctxt, o_model', (I_Model.OLD_to_TEST i_prob, I_Model.OLD_to_TEST i_prob), (m_patt, where_, where_rls));

  1232 (**)val return_fill_method =(**)

  1233 (** )val met_imod =( **)

  1234            fill_method o_model (pbl_imod, met_imod) m_patt;

  1235 (*////--------------- step into fill_method -----------------------------------------------\\*)

  1236 "~~~~~ fun fill_method , args:"; val (o_model, (pbl_imod, met_imod), met_patt) =

  1237   (o_model, (pbl_imod, met_imod), m_patt);

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

  1240  = pbl_imod |> I_Model.to_string_TEST @{context}

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

  1242  = met_imod |> I_Model.to_string_TEST @{context}

  1244 (**)val return_max_variants =(**)

  1245 (** )val pbl_max_vnts as [2, 1] =( **)

  1246  Model_Def.max_variants o_model pbl_imod

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

  1248 (*//------------------ step into max_variants ----------------------------------------------\\*)

  1249 "~~~~~ fun max_variants , args:"; val (o_model, i_model) = (o_model, pbl_imod);

  1250 \<close> ML \<open>

  1251       val all_variants as [1, 2, 3] =

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

  1253           |> flat

  1254           |> distinct op =

  1255 \<close> ML \<open>

  1256       val variants_separated = map (filter_variants' i_model) all_variants

  1257 (*+*)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))]",

  1258           "[\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))]",

  1259           "[\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))]"]

  1260  = variants_separated |> map (I_Model.to_string_TEST @{context})

  1262       val sums_corr as [5, 5, 4] = map (cnt_corrects) variants_separated

  1263       (*----------------#--#--#*)

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

  1265       val sum_variant_s as [(5, 1), (5, 2), (4, 3)] = arrange_args sums_corr (1, all_variants)

  1266       val max_first as [(5, 2), (5, 1), (4, 3)] = rev (sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s)

  1267       (*----------------##====--##====--//////---------^^^^*)

  1268       (*------------^--^-#-------#*)

  1269       val maxes as [2, 1] = filter (fn (cnt, _) => curry op = (fst (hd max_first)) cnt) max_first

  1270         |> map snd

  1271 val return_max_variants = maxes

  1272 (*\\------------------ step into max_variants ----------------------------------------------//*)

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

  1274 val pbl_max_vnts as [2, 1] = return_max_variants;

  1276     (*probably pbl/met_imod = [], so take met_patt; if empty return Sup*)

  1277     val i_from_met = map (fn (_, (descr, _)) => (*order from met_patt*)

  1278       Pre_Conds.get_descr_vnt descr pbl_max_vnts met_imod) met_patt (*\<longrightarrow> right order for args*)

  1279 (*+MET: Sup..*)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(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)), \n(0, [], false ,i_model_empty, (Sup_TEST FunctionVariable, Position.T)), \n(0, [], false ,i_model_empty, (Sup_TEST Input_Descript.Domain, Position.T)), \n(0, [], false ,i_model_empty, (Sup_TEST ErrorBound, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T))]"

  1280   = i_from_met |> I_Model.to_string_TEST @{context}

  1282     val met_max_vnts as [2, 1] = Model_Def.max_variants o_model i_from_met;

  1283     val max_vnt as 2 = hd (inter op= pbl_max_vnts met_max_vnts);

  1284     (*add items from pbl_imod (without overwriting existing items in met_imod)*)

  1286 \<close> ML \<open>

  1287 val return_add_other = map (

  1288            add_other max_vnt pbl_imod) i_from_met;

  1289 (*+*)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(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)), \n(0, [2], false ,i_model_empty, (Sup_TEST FunctionVariable, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_TEST Input_Descript.Domain, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_TEST ErrorBound, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T))]"

  1290   = return_add_other |> I_Model.to_string_TEST @{context};

  1291 (*/////-------------- step into add_other -------------------------------------------------\\*)

  1292 "~~~~~ fun add_other_5 , args:"; val (max_vnt, i1_model, (i2, _, bool2, m_field2, (Sup_TEST (descr2, ts2), pos2))) =

  1293   (max_vnt, pbl_imod, nth 5 i_from_met);

  1295 (*+*)val Const ("Input_Descript.FunctionVariable", _) = descr2;

  1297 val (_, vnts1, _, _, (feedb1, _)) = (i2, [], bool2, m_field2, (Sup_TEST (descr2, ts2), pos2))

  1298 val SOME (descr1 as (Const ("Input_Descript.FunctionVariable", _)) ) =

  1299       get_dscr' feedb1

  1300 val true =

  1301         descr1 = descr2

  1302 val true =

  1303           Model_Def.member_vnt vnts1 max_vnt

  1304 val NONE =

  1305     find_first (fn (_, vnts1, _, _, (feedb1, _)) => case get_dscr' feedb1 of

  1306           NONE => false

  1307         | SOME descr1 => descr1 = descr2 andalso Model_Def.member_vnt vnts1 max_vnt) i1_model

  1309 val return_add_other_1 = (i2, [max_vnt], bool2, m_field2, (Sup_TEST (descr2, ts2), pos2))

  1310 val check as true = return_add_other_1 = nth 5 return_add_other

  1311 (*\\\\\-------------- step into add_other -------------------------------------------------//*)

  1312     val i_from_pbl = return_add_other

  1313 (*\\\\---------------- step into fill_method -----------------------------------------------//*)

  1314 val return_fill_method_step = filter (fn (_, vnts', _, _, _) => member op = vnts' max_vnt) i_from_met

  1316 (*+MET: dropped ALL DUE TO is_empty_single_TEST*)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(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)), \n(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T))]" =

  1317   return_fill_method_step |> I_Model.to_string_TEST @{context}

  1318 (*+*)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(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)), \n(0, [2], false ,i_model_empty, (Sup_TEST FunctionVariable, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_TEST Input_Descript.Domain, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_TEST ErrorBound, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T))]"

  1319  = return_fill_method |> I_Model.to_string_TEST @{context};

  1320 return_fill_method_step = return_fill_method; (*latter is correct, did not investigate further*)

  1321 (*\\\----------------- step into match_itms_oris -------------------------------------------//*)

  1322 (*\\################# @ {context} within fun match_itms_oris ------------------------------//*)

  1323 \<close> ML \<open>(*\\############ @ {context} within fun match_itms_oris ------------------------------//*)

  1324 val (_, (i_model, _)) = return_match_itms_oris;

  1326 (*||------------------ continue. complete_for ------------------------------------------------*)

  1327       val (o_model, ctxt, i_model) = return_complete_for

  1328 (*+isa*)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(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)), \n(0, [2], false ,i_model_empty, (Sup_TEST FunctionVariable, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_TEST Input_Descript.Domain, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_TEST ErrorBound, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T))]"

  1329  = i_model |> I_Model.to_string_TEST @{context}(*+isa*)

  1330 (*+isa2:MET.Mis* ) val "[\n(1 ,[1, 2, 3] ,true ,#Given ,Cor Constants [r = 7] , pen2str), \n(2 ,[1, 2, 3] ,true ,#Find ,Cor Maximum A , pen2str), \n(3 ,[1, 2, 3] ,true ,#Find ,Cor AdditionalValues [u, v] , pen2str), \n(4 ,[1, 2, 3] ,true ,#Relate ,Cor Extremum (A = 2 * u * v - u \<up> 2) , pen2str), \n(5 ,[1, 2] ,true ,#Relate ,Cor SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str), \n(7 ,[1] ,false ,#Given ,Mis FunctionVariable funvar), \n(10 ,[1, 2] ,false ,#Given ,Mis Input_Descript.Domain doma), \n(12 ,[1, 2, 3] ,false ,#Given ,Mis ErrorBound err)]" =

  1331   i_model |> I_Model.to_string @{context} ( *+isa2*)

  1332 (*\\------------------ step into complete_for ----------------------------------------------//*)

  1333       val (o_model, ctxt, i_model) = return_complete_for

  1335 (*|------------------- continue. complete_for ------------------------------------------------*)

  1336 val return_complete_for_step = (o_model', ctxt', i_model)

  1338 val (o_model'_step, i_model_step) = (#1 return_complete_for_step, #3 return_complete_for_step)

  1339 val (o_model', i_model) = (#1 return_complete_for, #3 return_complete_for)

  1340 ;

  1341 (*+*)if (o_model'_step, i_model_step) = (o_model', i_model)

  1342 (*+*)then () else error "return_complete_for_step <> return_complete_for";

  1343 \<close> ML \<open>(*\------------- step into me Specify_Problem ----------------------------------------//*)

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

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

  1347 val return_me_Specify_Method

  1348                      = me nxt p c pt; val Add_Given "FunctionVariable b" = #4 return_me_Specify_Method;

  1349 (*/------------------- step into me_Specify_Method -----------------------------------------\\*)

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

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

  1353 (*+isa==isa2*)val "[]" =(*+*) get_obj g_met pt (fst p) |> I_Model.to_string @{context}

  1355       val ctxt = Ctree.get_ctxt pt p

  1356       val (pt, p) =

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

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

  1360 (*quick step into --> me_Specify_Method*)

  1361 (*+*)val Specify_Method ["Optimisation", "by_univariate_calculus"] = tac;

  1362 (*    Step.by_tactic*)

  1363 "~~~~~ fun by_tactic , args:"; val () = ();

  1364 (*    Step.check*)

  1365 "~~~~~ fun check , args:"; val () = ();

  1366 (*Specify_Step.check (Tactic.Specify_Method*)

  1367 "~~~~~ fun check , args:"; val () = ();

  1368 (*Specify_Step.complete_for*)

  1369 "~~~~~ fun complete_for , args:"; val () = ();

  1370 (* M_Match.match_itms_oris*)

  1371 "~~~~~ fun match_itms_oris , args:"; val () = ();

  1373 \<close> ML \<open>

  1374 (*+isa*)val"[\n(1 ,[1, 2, 3] ,true ,#Given ,Cor Constants [r = 7] , pen2str), \n(2 ,[1, 2, 3] ,true ,#Find ,Cor Maximum A , pen2str), \n(4 ,[1, 2, 3] ,true ,#Relate ,Cor Extremum (A = 2 * u * v - u \<up> 2) , pen2str), \n(5 ,[1, 2] ,true ,#Relate ,Cor SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str), \n(0 ,[2] ,false ,i_model_empty ,Sup FunctionVariable), \n(0 ,[2] ,false ,i_model_empty ,Sup Input_Descript.Domain), \n(0 ,[2] ,false ,i_model_empty ,Sup ErrorBound), \n(3 ,[1, 2, 3] ,true ,#Find ,Cor AdditionalValues [u, v] , pen2str)]"

  1375 (*+isa*)

  1376 (*+isa2* )val "[\n(1 ,[1, 2, 3] ,true ,#Given ,Cor Constants [r = 7] , pen2str), \n(2 ,[1, 2, 3] ,true ,#Find ,Cor Maximum A , pen2str), \n(3 ,[1, 2, 3] ,true ,#Find ,Cor AdditionalValues [u, v] , pen2str), \n(4 ,[1, 2, 3] ,true ,#Relate ,Cor Extremum (A = 2 * u * v - u \<up> 2) , pen2str), \n(5 ,[1, 2] ,true ,#Relate ,Cor SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str), \n(7 ,[1] ,false ,#Given ,Mis FunctionVariable funvar), \n(10 ,[1, 2] ,false ,#Given ,Mis Input_Descript.Domain doma), \n(12 ,[1, 2, 3] ,false ,#Given ,Mis ErrorBound err)]"

  1377 ( *+isa2*)

  1378  = get_obj g_met pt (fst p) |> I_Model.to_string @{context};

  1380          (*case*)

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

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

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

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

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

  1386 val _ =

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

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

  1390       Step.switch_specify_solve p_ (pt, ip);

  1391 (*///----------------- step into Step.switch_specify_solve ---------------------------------\\*)

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

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

  1395       Step.specify_do_next (pt, input_pos);

  1396 (*////---------------- step into Step.specify_do_next --------------------------------------\\*)

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

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

  1400    Specify.find_next_step ptp;

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

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

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

  1404     val ctxt = Ctree.get_ctxt pt pos;

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

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

  1408 (*+isa*)val     "[\n(1 ,[1, 2, 3] ,true ,#Given ,Cor Constants [r = 7] , pen2str), \n(2 ,[1, 2, 3] ,true ,#Find ,Cor Maximum A , pen2str), \n(4 ,[1, 2, 3] ,true ,#Relate ,Cor Extremum (A = 2 * u * v - u \<up> 2) , pen2str), \n(5 ,[1, 2] ,true ,#Relate ,Cor SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str), \n(0 ,[2] ,false ,i_model_empty ,Sup FunctionVariable), \n(0 ,[2] ,false ,i_model_empty ,Sup Input_Descript.Domain), \n(0 ,[2] ,false ,i_model_empty ,Sup ErrorBound), \n(3 ,[1, 2, 3] ,true ,#Find ,Cor AdditionalValues [u, v] , pen2str)]"

  1409 (*+isa*)

  1410 (*isa2* )val "[\n(1 ,[1, 2, 3] ,true ,#Given ,Cor Constants [r = 7] , pen2str), \n(2 ,[1, 2, 3] ,true ,#Find ,Cor Maximum A , pen2str), \n(3 ,[1, 2, 3] ,true ,#Find ,Cor AdditionalValues [u, v] , pen2str), \n(4 ,[1, 2, 3] ,true ,#Relate ,Cor Extremum (A = 2 * u * v - u \<up> 2) , pen2str), \n(5 ,[1, 2] ,true ,#Relate ,Cor SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str), \n(7 ,[1] ,false ,#Given ,Mis FunctionVariable funvar), \n(10 ,[1, 2] ,false ,#Given ,Mis Input_Descript.Domain doma), \n(12 ,[1, 2, 3] ,false ,#Given ,Mis ErrorBound err)]"

  1411 ( *isa2*)

  1412  = met |> I_Model.to_string @{context};

  1414 (*isa2*)val ("dummy", (Met, Add_Given "FunctionVariable b")) =(*isa2*)

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

  1416 (*///// /------------- step into Step.for_method -------------------------------------------\\*)

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

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

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

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

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

  1422 val NONE =

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

  1425 (*isa2*)val SOME ("#Given", "FunctionVariable b") =(*isa2*)

  1426       (*case*)

  1427    Specify.item_to_add (ThyC.get_theory ctxt

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

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

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

  1431 (*\------------------- step into me_Specify_Method -----------------------------------------//*)

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

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

  1436 \<close> ML \<open>

  1437 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Input_Descript.Domain {0<..<r}" = nxt;

  1438 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "ErrorBound (\<epsilon> = 0)" = nxt;

  1441 \<close> ML \<open>

  1442 \<close>

  1444 (*ML_file "Minisubpbl/biegel ? ? ?.sml"*)

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

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

  1447 ML \<open>

  1448 \<close> ML \<open>

  1450 \<close> ML \<open>

  1451 \<close>

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

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

  1455 ML \<open>

  1456 \<close> ML \<open>

  1458 \<close> ML \<open>

  1459 \<close>

  1461 end

author	wneuper <Walther.Neuper@jku.at>
	Sun, 29 Oct 2023 07:14:14 +0100
changeset 60762	f10bbfb2b3bb
parent 60761	c3a97132157f
child 60763	2121f1a39a64
permissions	-rw-r--r--