\<close> ML \<open>

 \<close>

 ML \<open>

 \<close> ML \<open>

 \<close>

 text \<open>

   declare [[show_types]] 

   declare [[show_sorts]]

   find_theorems "?a <= ?a"

   print_theorems

   print_facts

   print_statement ""

   print_theory

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

   declare [[ML_print_depth = 999]]                 

   declare [[ML_exception_trace]]

 open TermC;

 open Model_Pattern;

 open Pre_Conds;

 \<close> ML \<open>

 \<close> ML \<open> (*//----------- adhoc inserted fun check_OLD ----------------------------------------\\*)

 (*//------------------ adhoc inserted fun check_OLD ----------------------------------------\\*)

 (*T_TESTold* )

 fun all_lhs_atoms ts = fold (curry and_) (map (fn t =>

   if can TermC.lhs t then TermC.is_atom (TermC.lhs t) else false) ts) true

 ( *T_TEST*)

 fun all_lhs_atoms ts = fold (curry and_) (map (fn t =>

   if can TermC.lhs t andalso not (TermC.is_num (TermC.lhs t))

   then TermC.is_atom (TermC.lhs t)

   else false) ts) true

 (*T_TESTnew*)

 (*T_TESTold* )

 fun handle_lists id (descr, ts) =

   if Model_Pattern.is_list_descr descr

   then if length ts > 1         (*list with more than 1 element needs to collect by [.., .., ..]*)

     then [(id, TermC.list2isalist (Model_Pattern.typ_of_element descr) ts)] (*AdditValues [u, v]*)

     else if TermC.is_atom (Library.the_single ts)

       then [(id, Library.the_single ts)]                                     (* solutions L, ...*)

       else [(id, TermC.list2isalist (Model_Pattern.typ_of_element descr) ts)](*Constants [r = 7]*)

   else [(id, Library.the_single ts)]                           (* solveFor x, Extremum (A = ...)*)

 ( *T_TEST***)

 fun handle_lists id (descr, ts) =

   if Model_Pattern.is_list_descr descr

   then if length ts > 1         (*list with more than 1 element needs to collect by [.., .., ..]*)

     then if TermC.is_list (hd ts) (*---broken elementwise input to lists---*)

       then [(id, TermC.list2isalist (Model_Pattern.typ_of_element descr) (map TermC.the_single ts))]

       else [(id, TermC.list2isalist (Model_Pattern.typ_of_element descr) ts)] (*AdditValues [u, v]*)

     else if TermC.is_atom (Library.the_single ts)

       then [(id, Library.the_single ts)]                                     (* solutions L, ...*)

       else [(id, TermC.list2isalist (Model_Pattern.typ_of_element descr) ts)](*Constants [r = 7]*)

   else [(id, Library.the_single ts)]                           (* solveFor x, Extremum (A = ...)*)

 (*T_TESTnew*)

 ;

 handle_lists: term -> descriptor * term list -> (term * term) list;

 fun mk_env_model _ (Model_Def.Cor_TEST ((_, []), _)) = []

   | mk_env_model id (Model_Def.Cor_TEST ((descr, ts), _)) = 

 (*T_TEST.150* )

     if Model_Pattern.is_list_descr descr 

     then [(id, TermC.list2isalist (Model_Pattern.typ_of_element descr) ts)]

     else [(id, hd ts)]

 ( *T_TEST*)

     handle_lists id (descr, ts)

 (*T_TEST.100*)

   | mk_env_model _ (Model_Def.Syn_TEST _) = [] (*TODO handle correct list elements*)

   | mk_env_model _ (Model_Def.Inc_TEST ((_, []), _)) = []

   | mk_env_model id (Model_Def.Inc_TEST ((descr, ts), _)) = 

 (*T_TEST.150* )

     if Model_Pattern.is_list_descr descr 

     then [(id, TermC.list2isalist (Model_Pattern.typ_of_element descr) ts)]

     else [(id, hd ts)]

 ( *T_TEST*)

     handle_lists id (descr, ts)

 (*T_TEST.100*)

   | mk_env_model _ (Model_Def.Sup_TEST _) = []

 ;

 mk_env_model: term -> Model_Def.i_model_feedback_TEST -> Env.T;

 val (id, (descr, ts)) = (@{term "v_v'i'::bool list"}, (@{term solutions}, [@{term "L::bool list"}]));

 is_atom (Library.the_single [@{term "r = (7::real)"}]);

 (*  vvvvvvvvvvvv-- REPLACES mk_env_subst_DEL, THUS THE LATTER IS UNCHANGED*)

 fun make_env_model equal_descr_pairs =

   map (fn ((_, (_, id)), (_, _, _, _, (feedb, _)))

         => (mk_env_model id feedb)) equal_descr_pairs

   |> flat

 ;

 make_env_model: (Model_Pattern.single * Model_Def.i_model_single_TEST) list -> Env.T;

 fun switch_type_TEST descr [] = descr

   | switch_type_TEST (Free (id_string, _)) ts =

     Free (id_string, ts |> hd |> TermC.lhs |> type_of)

   | switch_type_TEST descr _ = raise ERROR ("switch_type_TEST undefined argument " ^

       quote (UnparseC.term (ContextC.for_ERROR ()) descr))

 ;

 switch_type_TEST: descriptor -> term list -> descriptor;

 (*T_TESTold* )

 fun discern_typ _ (_, []) = []

   | discern_typ id (descr, ts) =

 (*TODO.md "review (descriptor, ts)" REMOVE--------------------------------------\*)

     let

       val ts = if Model_Pattern.is_list_descr descr andalso TermC.is_list (hd ts)

         then TermC.isalist2list (hd ts)

         else ts

     in

 (*TODO.md "review (descriptor, ts)" REMOVE--------------------------------------/*)

   if Model_Pattern.typ_of_element descr = HOLogic.boolT

     andalso ts |> map TermC.lhs |> all_atoms

   then

     if length ts > 1

     then raise ERROR "model items of type 'bool' in lists with 'lengt ts > 1' NOT YET IMPLEMENTED"

     else [((switch_type_TEST id ts, TermC.lhs (hd ts)), 

            (TermC.lhs (hd ts), TermC.rhs (hd ts)))]

   else []

 (*TODO.md "review (descriptor, ts)" REMOVE--------------------------------------\*)

     end

 (*TODO.md "review (descriptor, ts)" REMOVE--------------------------------------/*)

 ( *T_TEST*)

 fun discern_typ _ (_, []) = []

   | discern_typ id (descr, ts) =

 (*TODO.md "review (descriptor, ts)" REMOVE--------------------------------------\*)

     let

       val ts = if Model_Pattern.is_list_descr descr

         then if TermC.is_list (hd ts)

           then ts |> map TermC.isalist2list |> flat

           else ts

         else ts

     in

 (*TODO.md "review (descriptor, ts)" REMOVE--------------------------------------/*)

   if Model_Pattern.typ_of_element descr = HOLogic.boolT andalso all_lhs_atoms ts

   then

     if length ts > 1

     then (writeln "model items of type 'bool' in lists with 'lengt ts > 1' NOT YET IMPLEMENTED";

       [])

     else [((switch_type_TEST id ts, TermC.lhs (hd ts)), 

            (TermC.lhs (hd ts), TermC.rhs (hd ts)))]

   else []

 (*TODO.md "review (descriptor, ts)" REMOVE--------------------------------------\*)

     end

 (*TODO.md "review (descriptor, ts)" REMOVE--------------------------------------/*)

 ;

 discern_typ: term -> descriptor * term list -> ((term * term) * (term * term)) list;

 (*T_TESTnew*)

 fun discern_feedback id (Model_Def.Cor_TEST ((descr, ts), _)) = discern_typ id (descr, ts)

   | discern_feedback _ (Model_Def.Syn_TEST _) = [] (*TODO: handle correct elements*)

   | discern_feedback id (Model_Def.Inc_TEST ((descr, ts), _)) = discern_typ id (descr, ts)

   | discern_feedback _ (Model_Def.Sup_TEST _) = []

 ;

 discern_feedback: term -> I_Model.feedback_TEST -> ((term * term) * (term * term)) list;

 fun make_envs_preconds equal_givens =

   map (fn ((_, (_, id)), (_, _, _, _, (feedb, _))) => discern_feedback id feedb) equal_givens

   |> flat

 ;

 make_envs_preconds: (Model_Pattern.single * I_Model.single_TEST) list ->

     ((term * term) * (term * term)) list;

 (*T_TESTold* )

 fun of_max_variant model_patt i_model =

 ( *T_TEST*)

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

   | of_max_variant model_patt i_model =

 (*T_TESTnew*)

   let

     val all_variants =

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

         |> flat

         |> distinct op =

     val variants_separated = map (filter_variants' i_model) all_variants

     val sums_corr = map (cnt_corrects) variants_separated

     val sum_variant_s = arrange_args1 sums_corr (1, all_variants)

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

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

     val i_model_max =

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

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

 (*T_TESTold* )

     val env_subst = mk_env_subst_DEL equal_descr_pairs

     val env_eval = mk_env_eval_DEL i_model_max

   in

     (i_model_max, env_subst, env_eval)

   end

 ( *T_TEST*)

     val env_model = make_env_model equal_descr_pairs

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

     val subst_eval_list = make_envs_preconds equal_givens

     val (env_subst, env_eval) = split_list subst_eval_list

   in

     (i_model_max, env_model, (env_subst, env_eval))

   end

 (*T_TESTnew*)

 ;

 of_max_variant: Model_Pattern.T -> Model_Def.i_model_TEST ->

        Model_Def.i_model_TEST * Env.T * (env_subst * env_eval);

 fun check_OLD _ _ [] _  = (true, [])

   | check_OLD ctxt where_rls pres (model_patt, i_model) =

     let

 (*T_TESTold* )

       val (env_subst, env_eval) = sep_variants_envs_OLD model_patt i_model

 ( *NEW*)  

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

 (*NEW*)

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

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

       val full_subst = if env_eval = [] then pres_subst_other

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

       val evals = map (eval ctxt where_rls) full_subst

     in

       (foldl and_ (true, map fst evals), pres_subst_other)

     end

 ;

 check_OLD: Proof.context -> Rule_Def.rule_set -> term list -> Model_Pattern.T * I_Model.T_TEST ->

   checked;

 \<close> ML \<open>

 \<close> ML \<open>

 (*T_TESTold*)

 fun check_from_store ctxt where_rls pres env_subst env_eval =

   let

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

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

     val evals = map (eval ctxt where_rls) full_subst

   in

     (foldl and_ (true, map fst evals), pres_subst)

   end

 (*T_TEST*)

 fun check_envs_TEST ctxt where_rls where_ (env_model, (env_subst, env_eval)) =

   let

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

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

       val full_subst = if env_eval = [] then pres_subst_other

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

       val evals = map (eval ctxt where_rls) full_subst

   in

       (foldl and_ (true, map fst evals), pres_subst_other)

   end

 ;

   check_envs_TEST: Proof.context -> Rule_Set.T -> unchecked -> Env.T * (env_subst * env_eval)

     -> checked

 (*T_TESTnew*)

 (*\\------------------ adhoc inserted fun check_OLD ----------------------------------------//*)

 \<close> ML \<open> (*\\----------- adhoc inserted fun check_OLD ----------------------------------------//*)

 (*//------------------ new code for repair Biegelinie SubProblem ---------------------------\\*)

 \<close> ML \<open> (*//----------- new code for repair Biegelinie SubProblem ---------------------------\\*)

 \<close> ML \<open>

 \<close> ML \<open>

 \<close> ML \<open>

 \<close> ML \<open>

 \<close> ML \<open>

 \<close> ML \<open>

 \<close> ML \<open>

 (*\\------------------ new code for repair Biegelinie SubProblem ---------------------------//*)

 \<close> ML \<open> (*\\----------- new code for repair Biegelinie SubProblem ---------------------------//*)

 \<close> ML \<open>

 ML \<open>

   Know_Store.set_ref_last_thy @{theory};

   (*otherwise ERRORs in pbl-met-hierarchy.sml, refine.sml, evaluate.sml*)

 \<close>

   ML_file "Specify/refine.sml"        (* requires setup from refine.thy *)

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

 section \<open>=====AUFRÄUMEN refine.sml =========================================================\<close>

 ML \<open>

 \<close> ML \<open>

 (* Title:  "Specify/refine.sml"

    Author: Walther Neuper

    (c) due to copyright terms

 *)

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

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

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

 "refine.thy: store test-pbtyps by 'setup' ------------------------------------------------------";

 "----------- testdata for refin, Refine.refine_ori --------------------------------------------";

 (*"----------- refin test-pbtyps -------requires specific 'setup'-------------------------------";*)

 "----------- Refine.refine_ori test-pbtyps --requires 'setup'-----------------------------------";

 "----------- refine test-pbtyps ------requires 'setup'------------------------------------------";

 "----------- refine_ori' [0 = - 1 * c_4 / - 1, 0 =\n (- 24 * c_4.., ..] ------------------------";

 "----------- Refine_Problem (from subp-rooteq.sml) ---------------------------------------------";

 "----------- equation with CalcTree [ = 6 / 5] for timing: with/out adapt_to_type --------------";

 "----------- refine ad-hoc equation for timing: with/out adapt_to_type -------------------------";

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

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

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

 \<close> ML \<open>

 @{theory}(*val it =

    {Pure, Isac.VSCode_Example, Interpret.Interpret, Isac.MathEngine, Isac.Test_Code,

      Isac.BridgeLibisabelle, Isac.Base_Tools, Isac.Simplify, Isac.Poly, Isac.GCD_Poly_ML,

      Isac.Rational, Isac.Root, Isac.Equation, Isac.LinEq, Isac.RootEq, Isac.RatEq, Isac.RootRat,

      Isac.RootRatEq, Isac.PolyEq, Isac.Calculus, Isac.Trig, Isac.LogExp, Isac.Diff, Isac.Integrate,

      Isac.EqSystem, Isac.Test, Isac.Diff_App, Isac.Partial_Fractions, Isac.PolyMinus, Isac.Vect,

      Isac.Biegelinie, Isac.AlgEin, Isac.InsSort, Isac.DiophantEq, Isac.Inverse_Z_Transform,

      Tools.Code_Generator, HOL.HOL, HOL.Orderings, HOL.Groups, HOL.Lattices, HOL.Boolean_Algebras,

      HOL.Set, HOL.Fun, HOL.Complete_Lattices, HOL.Ctr_Sugar, HOL.Typedef, HOL.Inductive, HOL.Rings,

      HOL.Nat, HOL.Product_Type, HOL.Sum_Type, HOL.Fields, HOL.Finite_Set, HOL.Relation,

      HOL.Transitive_Closure, HOL.Wellfounded, HOL.Wfrec, HOL.Order_Relation, HOL.Hilbert_Choice,

      HOL.BNF_Wellorder_Relation, HOL.BNF_Wellorder_Embedding, HOL.Zorn,

      HOL.BNF_Wellorder_Constructions, HOL.BNF_Cardinal_Order_Relation, HOL.BNF_Cardinal_Arithmetic,

      HOL.Fun_Def_Base, HOL.BNF_Def, HOL.BNF_Composition, HOL.Basic_BNFs, HOL.BNF_Fixpoint_Base,

      HOL.BNF_Least_Fixpoint, HOL.Meson, HOL.ATP, HOL.Basic_BNF_LFPs, HOL.Metis, HOL.Equiv_Relations,

      HOL.Transfer, HOL.Lifting, HOL.Num, HOL.Power, HOL.Complete_Partial_Order, HOL.Option, HOL.Argo,

      HOL.Partial_Function, HOL.SAT, HOL.Quotient, HOL.Groups_Big, HOL.Fun_Def, HOL.Int,

      HOL.Lattices_Big, HOL.Euclidean_Division, HOL.Parity, HOL.Numeral_Simprocs,

      HOL.Semiring_Normalization, HOL.Groebner_Basis, HOL.Set_Interval, HOL.Divides, HOL.Presburger,

      HOL.SMT, HOL.Sledgehammer, HOL.Lifting_Set, HOL.List, HOL.Groups_List, HOL.Bit_Operations,

      HOL.Code_Numeral, HOL.Map, HOL.Enum, HOL.String, HOL.Predicate, HOL.Lazy_Sequence, HOL.Typerep,

      HOL.Limited_Sequence, HOL.Random, HOL.Code_Evaluation, HOL.Quickcheck_Random, HOL.Random_Pred,

      HOL.Random_Sequence, HOL.Quickcheck_Exhaustive, HOL.Predicate_Compile, HOL.Record, HOL.GCD,

      HOL.Nitpick, HOL.Factorial, HOL.Quickcheck_Narrowing, HOL.Mirabelle, HOL.Extraction, HOL.Nunchaku,

      HOL.BNF_Greatest_Fixpoint, HOL.Filter, HOL.Conditionally_Complete_Lattices, HOL.Binomial, Main,

      HOL.Archimedean_Field, HOL.Rat, HOL.Hull, HOL.Modules, HOL.Real, HOL.Topological_Spaces,

      HOL.Vector_Spaces, HOL.Real_Vector_Spaces, HOL.Limits, HOL.Inequalities, HOL.Deriv, HOL.Series,

      HOL.NthRoot, HOL.Transcendental, HOL.Complex, HOL.MacLaurin, Complex_Main, Specify.Know_Store,

      Specify.BaseDefinitions, Specify.Calc_Binop, Specify.ListC, Specify.Program, Specify.Prog_Tac,

      Specify.Tactical, Specify.Prog_Expr, Specify.Auto_Prog, Specify.ProgLang, Isac.Isac_Knowledge,

      Isac.Test_Build_Thydata, Isac.BridgeJEdit, Isac.Build_Thydata, Isac.Build_Isac, Isac_Test.refine,

      Isac_Test.Test_Theory:544}:

    theory*)

 \<close> ML \<open>

 \<close> ML \<open>

 open Test_Tool;

 \<close> ML \<open>"----- testdata for refin, Refine.refine_ori --------------------------------------------";

 "----------- testdata for refin, Refine.refine_ori --------------------------------------------";

 "----------- testdata for refin, Refine.refine_ori --------------------------------------------";

 Test_Tool.show_ptyps();

 val thy = @{theory "Isac_Knowledge"};

 val ctxt = Proof_Context.init_global @{theory "Isac_Knowledge"};

 (*case 1: no refinement *)

 val (d1,ts1) = Input_Descript.split (ParseC.parse_test ctxt "fixedValues [aaa = 0]");

 val (d2,ts2) = Input_Descript.split (ParseC.parse_test ctxt "errorBound (ddd = 0)");

 val ori1 = [(1,[1],"#Given",d1,ts1), (2,[1],"#Given",d2,ts2)]: O_Model.T;

 (*case 2: refined to pbt without children *)

 val (d2,ts2) = Input_Descript.split (ParseC.parse_test ctxt "relations [aaa333]");

 val ori2 = [(1,[1],"#Given",d1,ts1), (2,[1],"#Given",d2,ts2)]:O_Model.T;

 (*case 3: refined to pbt with children *)

 val (d2,ts2) = Input_Descript.split (ParseC.parse_test ctxt "valuesFor [aaa222]");

 val ori3 = [(1,[1],"#Given",d1,ts1), (2,[1],"#Given",d2,ts2)]:O_Model.T;

 (*case 4: refined to children (without child)*)

 val (d3,ts3) = Input_Descript.split (ParseC.parse_test ctxt "boundVariable aaa222yyy");

 val ori4 = [(1,[1],"#Given",d1,ts1), (2,[1],"#Given",d2,ts2), (3,[1],"#Given",d3,ts3)]:O_Model.T;

 (*=================================================================

 This test expects pbls at a certain position in the tree.

 Since parallel evaluation (i.e. Theory_Data) this cannot be expected.

 Solutions would be

 * provide an access function for a branch (not only leaves)

 * sort the tree of pbls.

 "----------- refin test-pbtyps -------requires specific 'setup'-------------------------------";

 "----------- refin test-pbtyps -------requires specific 'setup'-------------------------------";

 "----------- refin test-pbtyps -------requires specific 'setup'-------------------------------";

 (* fragile test setup: expects ptyps as fixed *)

 val level_1 = case nth 9 (get_pbls ()) of

 Store.Node ("test", _, level_1) => level_1 | _ => error "refin broken: root-branch in ptyps changed?"

 val level_2 = case nth 4 level_1 of

 Store.Node ("refine", _, level_2) => level_2 | _ => error "refin broken: lev1-branch in ptyps changed?"

 val pbla_branch = case level_2 of 

 [Store.Node ("pbla", _, _)] => level_2 | _ => error "refin broken: lev2-branch in ptyps changed?";

 (*case 1: no refinement *)

 case refin [] ori1 (hd pbla_branch) of 

   SOME ["pbla"] => () | _ => error "refin case 1 broken";

 (*case 2: refined to pbt without children *)

 case refin [] ori2 (hd pbla_branch) of 

   SOME ["pbla", "pbla3"] => () | _ => error "refin case 2 broken";

 (*case 3: refined to pbt with children *)

 case refin [] ori3 (hd pbla_branch) of 

   SOME ["pbla", "pbla2"] => () | _ => error "refin case 3 broken";

 (*case 4: refined to children (without child)*)

 case refin [] ori4 (hd pbla_branch) of 

   SOME ["pbla", "pbla2", "pbla2y"] => () | _ => error "refin case 4 broken";

 (*case 5: start refinement somewhere in ptyps*)

 val [Store.Node ("pbla",_,[_, ppp as Store.Node ("pbla2",_,_), _])] = pbla_branch;

 case refin ["pbla"] ori4 ppp of 

   SOME ["pbla", "pbla2", "pbla2y"] => () | _ => error "refin case 5 broken";

 ==================================================================*)

 \<close> ML \<open>"----- ERR Refine.refine_ori test-pbtyps --requires 'setup'----------------------------------";

 "----------- Refine.refine_ori test-pbtyps --requires 'setup'----------------------------------";

 "----------- Refine.refine_ori test-pbtyps --requires 'setup'----------------------------------";

 (*case 1: no refinement *)

 case Refine.refine_ori @{context} ori1 ["pbla", "refine", "test"] of 

   NONE => () | _ => error "Refine.refine_ori case 1 broken";

 (*case 2: refined to pbt without children *)

 case Refine.refine_ori @{context} ori2 ["pbla", "refine", "test"] of 

   SOME ["pbla3", "pbla", "refine", "test"] => () | _ => error "Refine.refine_ori case 2 broken";

 (*case 3: refined to pbt with children *)

 case Refine.refine_ori @{context} ori3 ["pbla", "refine", "test"] of 

   SOME ["pbla2", "pbla", "refine", "test"] => () | _ => error "Refine.refine_ori case 3 broken";

 (*case 4: refined to children (without child)*)

 case Refine.refine_ori @{context} ori4 ["pbla", "refine", "test"] of 

   SOME ["pbla2y", "pbla2", "pbla", "refine", "test"] => () | _ => error "Refine.refine_ori case 4 broken";

 (*case 5: start refinement somewhere in ptyps*)

 case Refine.refine_ori @{context} ori4 ["pbla2", "pbla", "refine", "test"] of 

   SOME ["pbla2y", "pbla2", "pbla", "refine", "test"] => () | _ => error "Refine.refine_ori case 5 broken";

 \<close> ML \<open>"----- refine test-pbtyps ------requires 'setup'------------------------------------------";

 "----------- refine test-pbtyps ------requires 'setup'------------------------------------------";

 "----------- refine test-pbtyps ------requires 'setup'------------------------------------------";

 val fmz1 = ["fixedValues [aaa=0]", "errorBound (ddd=0)"];

 val fmz2 = ["fixedValues [aaa=0]", "relations aaa333"];

 val fmz3 = ["fixedValues [aaa=0]", "valuesFor [aaa222]"];

 val fmz4 = ["fixedValues [aaa=0]", "valuesFor [aaa222]",

 	    "boundVariable aaa222yyy"];

 (*case 1: no refinement *)

 case Refine.xxxxx @{context} fmz1 ["pbla", "refine", "test"] of

   [M_Match.Matches (["pbla", "refine", "test"], _), 

    M_Match.NoMatch (["pbla1", "pbla", "refine", "test"], _), 

    M_Match.NoMatch (["pbla2", "pbla", "refine", "test"], _), 

    M_Match.NoMatch (["pbla3", "pbla", "refine", "test"], _)] => ()

  | _ => error "--- Refine.refine test-pbtyps --- broken with case 1";

 (* 

 *** pass ["pbla"]

 *** pass ["pbla", "pbla1"]

 *** pass ["pbla", "pbla2"]

 *** pass ["pbla", "pbla3"]

 val it =

   [M_Match.Matches

      (["pbla"],

       {Find=[],

        Given=[Correct "fixedValues [aaa = #0]",

               Superfl "errorBound (ddd = #0)"],Relate=[],Where=[],With=[]}),

    M_Match.NoMatch

      (["pbla1", "pbla"],

       {Find=[],

        Given=[Correct "fixedValues [aaa = #0]",Missing "maximum a1_",

               Superfl "errorBound (ddd = #0)"],Relate=[],Where=[],With=[]}),

    M_Match.NoMatch

      (["pbla2", "pbla"],

       {Find=[],

        Given=[Correct "fixedValues [aaa = #0]",Missing "valuesFor a2_",

               Superfl "errorBound (ddd = #0)"],Relate=[],Where=[],With=[]}),

    M_Match.NoMatch

      (["pbla3", "pbla"],

       {Find=[],

        Given=[Correct "fixedValues [aaa = #0]",Missing "relations a3_",

               Superfl "errorBound (ddd = #0)"],Relate=[],Where=[],With=[]})]

   : match list*)

 (*case 2: refined to pbt without children *)

 case Refine.xxxxx @{context} fmz2 ["pbla", "refine", "test"] of

   [M_Match.Matches (["pbla", "refine", "test"], _),

    M_Match.NoMatch (["pbla1", "pbla", "refine", "test"], _),

    M_Match.NoMatch (["pbla2", "pbla", "refine", "test"], _),

    M_Match.Matches (["pbla3", "pbla", "refine", "test"], _)] => ()

  | _ => error "--- Refine.refine test-pbtyps --- broken with case 2";

 (* 

 *** pass ["pbla"]

 *** pass ["pbla", "pbla1"]

 *** pass ["pbla", "pbla2"]

 *** pass ["pbla", "pbla3"]

 val it =

   [M_Match.Matches

      (["pbla"],

       {Find=[],

        Given=[Correct "fixedValues [aaa = #0]",Superfl "relations aaa333"],

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

    M_Match.NoMatch

      (["pbla1", "pbla"],

       {Find=[],

        Given=[Correct "fixedValues [aaa = #0]",Missing "maximum a1_",

               Superfl "relations aaa333"],Relate=[],Where=[],With=[]}),

    M_Match.NoMatch

      (["pbla2", "pbla"],

       {Find=[],

        Given=[Correct "fixedValues [aaa = #0]",Missing "valuesFor a2_",

               Superfl "relations aaa333"],Relate=[],Where=[],With=[]}),

    M_Match.Matches

      (["pbla3", "pbla"],

       {Find=[],

        Given=[Correct "fixedValues [aaa = #0]",Correct "relations aaa333"],

        Relate=[],Where=[],With=[]})] : match list*)

 (*case 3: refined to pbt with children *)

 case Refine.xxxxx @{context} fmz3 ["pbla", "refine", "test"] of

   [M_Match.Matches (["pbla", "refine", "test"], _),

    M_Match.NoMatch (["pbla1", "pbla", "refine", "test"], _),

    M_Match.Matches (["pbla2", "pbla", "refine", "test"], _),

    M_Match.NoMatch (["pbla2x", "pbla2", "pbla", "refine", "test"], _),

    M_Match.NoMatch (["pbla2y", "pbla2", "pbla", "refine", "test"], _),

    M_Match.NoMatch (["pbla2z", "pbla2", "pbla", "refine", "test"], _),

    M_Match.NoMatch (["pbla3", "pbla", "refine", "test"], _)] => ()

  | _ => error "--- Refine.refine test-pbtyps --- broken with case 3";

 (* 

 *** pass ["pbla"]

 *** pass ["pbla", "pbla1"]

 *** pass ["pbla", "pbla2"]

 *** pass ["pbla", "pbla2", "pbla2x"]

 *** pass ["pbla", "pbla2", "pbla2y"]

 *** pass ["pbla", "pbla2", "pbla2z"]

 *** pass ["pbla", "pbla3"]

 val it =

   [M_Match.Matches

      (["pbla"],

       {Find=[],

        Given=[Correct "fixedValues [aaa = #0]",Superfl "valuesFor aaa222"],

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

    M_Match.NoMatch

      (["pbla1", "pbla"],

       {Find=[],

        Given=[Correct "fixedValues [aaa = #0]",Missing "maximum a1_",

               Superfl "valuesFor aaa222"],Relate=[],Where=[],With=[]}),

    M_Match.Matches

      (["pbla2", "pbla"],

       {Find=[],

        Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222"],

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

    M_Match.NoMatch

      (["pbla2x", "pbla2", "pbla"],

       {Find=[],

        Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",

               Missing "functionOf a2x_"],Relate=[],Where=[],With=[]}),

    M_Match.NoMatch

      (["pbla2y", "pbla2", "pbla"],

       {Find=[],

        Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",

               Missing "boundVariable a2y_"],Relate=[],Where=[],With=[]}),

    M_Match.NoMatch

      (["pbla2z", "pbla2", "pbla"],

       {Find=[],

        Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",

               Missing "interval a2z_"],Relate=[],Where=[],With=[]}),

    M_Match.NoMatch

      (["pbla3", "pbla"],

       {Find=[],

        Given=[Correct "fixedValues [aaa = #0]",Missing "relations a3_",

               Superfl "valuesFor aaa222"],Relate=[],Where=[],With=[]})]

   : match list*)

 (*case 4: refined to children (without child)*)

 case Refine.xxxxx @{context} fmz4 ["pbla", "refine", "test"] of

     [M_Match.Matches (["pbla", "refine", "test"], _), 

      M_Match.NoMatch (["pbla1", "pbla", "refine", "test"], _), 

      M_Match.Matches (["pbla2", "pbla", "refine", "test"], _), 

      M_Match.NoMatch (["pbla2x", "pbla2", "pbla", "refine", "test"], _), 

      M_Match.Matches (["pbla2y", "pbla2", "pbla", "refine", "test"], _)] => ()

   | _ => error "--- Refine.refine test-pbtyps --- broken with case 4";

 (* 

 *** pass ["pbla"]

 *** pass ["pbla", "pbla1"]

 *** pass ["pbla", "pbla2"]

 *** pass ["pbla", "pbla2", "pbla2x"]

 *** pass ["pbla", "pbla2", "pbla2y"]

 val it =

   [M_Match.Matches

      (["pbla"],

       {Find=[],

        Given=[Correct "fixedValues [aaa = #0]",Superfl "valuesFor aaa222",

               Superfl "boundVariable aaa222yyy"],Relate=[],Where=[],With=[]}),

    M_Match.NoMatch

      (["pbla1", "pbla"],

       {Find=[],

        Given=[Correct "fixedValues [aaa = #0]",Missing "maximum a1_",

               Superfl "valuesFor aaa222",Superfl "boundVariable aaa222yyy"],

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

    M_Match.Matches

      (["pbla2", "pbla"],

       {Find=[],

        Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",

               Superfl "boundVariable aaa222yyy"],Relate=[],Where=[],With=[]}),

    M_Match.NoMatch

      (["pbla2x", "pbla2", "pbla"],

       {Find=[],

        Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",

               Missing "functionOf a2x_",Superfl "boundVariable aaa222yyy"],

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

    M_Match.Matches

      (["pbla2y", "pbla2", "pbla"],

       {Find=[],

        Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",

               Correct "boundVariable aaa222yyy"],Relate=[],Where=[],With=[]})]

   : match list*)

 (*case 5: start refinement somewhere in ptyps*)

 case Refine.xxxxx @{context} fmz4 ["pbla2", "pbla", "refine", "test"] of

     [M_Match.Matches (["pbla2", "pbla", "refine", "test"], _), 

      M_Match.NoMatch (["pbla2x", "pbla2", "pbla", "refine", "test"], _), 

      M_Match.Matches (["pbla2y", "pbla2", "pbla", "refine", "test"], _)] => ()

   | _ => error "--- Refine.refine test-pbtyps --- broken with case 5";

 (* 

 *** pass ["pbla", "pbla2"]

 *** pass ["pbla", "pbla2", "pbla2x"]

 *** pass ["pbla", "pbla2", "pbla2y"]

 val it =

   [M_Match.Matches

      (["pbla2", "pbla"],

       {Find=[],

        Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",

               Superfl "boundVariable aaa222yyy"],Relate=[],Where=[],With=[]}),

    M_Match.NoMatch

      (["pbla2x", "pbla2", "pbla"],

       {Find=[],

        Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",

               Missing "functionOf a2x_",Superfl "boundVariable aaa222yyy"],

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

    M_Match.Matches

      (["pbla2y", "pbla2", "pbla"],

       {Find=[],

        Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",

               Correct "boundVariable aaa222yyy"],Relate=[],Where=[],With=[]})]

   : match list*)

 \<close> ML \<open>"----- refine_ori' [0 = - 1 * c_4 / - 1, 0 =\n (- 24 * c_4.., ..] ------------------------";

 "----------- refine_ori' [0 = - 1 * c_4 / - 1, 0 =\n (- 24 * c_4.., ..] ------------------------";

 "----------- refine_ori' [0 = - 1 * c_4 / - 1, 0 =\n (- 24 * c_4.., ..] ------------------------";

 (*overwrites NEW funs in Test_Theory ABOVE* )

 open Refine

 open M_Match

 open Pre_Conds

 ( *overwrites NEW funs in Test_Theory ABOVE*)

 (*

   refinement of the first eqsystem in Biegelinie, IntegrierenUndKonstanteBestimmen2;

   this example was the demonstrator;

   respective data are in ~/proto4/../exp_Statics_Biegel_Timischl_7-70.xml.

   Data for this test are from biegelinie-5.sml, --- me IntegrierenUndKonstanteBestimmen2 ALL ---

 *)

 (*+*)val o_model = [

 (1, [1], "#Given", @{term "equalities"},

   [@{term "[(0::real) = - 1 * c_4 / - 1]"},

    @{term "[(0::real) = (- 24 * c_4 + - 24 * L * c_3 + 12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c +  - 1 * L \<up> 4 * q_0) / - 24]"},

    @{term "[(0::real) = c_2]"},

    @{term "[(0::real) = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]"}] ),

 (*Const ("List.list.Cons", "real \<Rightarrow> real list \<Rightarrow> real list") $ Free ("c", "real") $ Const ("List.list.Nil", "real list"),*)

 (2, [1], "#Given", @{term "solveForVars"},

   [@{term "[c]  ::real list"},

    @{term "[c_2]::real list"},

    @{term "[c_3]::real list"},

    @{term "[c_4]::real list"}] ),

 (3, [1], "#Find",  @{term "solution"},  [@{term "ss'''::bool list"}] )]

 ;

 val SOME ["normalise", "4x4", "LINEAR", "system"] =

            refine_ori @{context} o_model ["LINEAR", "system"];

 "~~~~~ fun refine_ori , args:"; val (ctxt, oris, pblID) =

   (@{context}, o_model, ["LINEAR", "system"]);

     val opt as SOME ["system", "LINEAR", "4x4", "normalise"]

     = app_ptyp (refin ctxt ((rev o tl) pblID) oris) pblID (rev pblID);

 (*

   app_ptyp works strangely, parameter passing is awkward.

   Present refin knows structure of Store.T, thus we bypass app_ptyp

 *)

 (*!*)val pblID = ["LINEAR", "system"];(**)

 val return_refin as SOME ["system", "LINEAR", "LINEAR", "4x4", "normalise"] = (**)

            refin ctxt (rev pblID) oris (Store.get_node (rev pblID) pblID (get_pbls ()));

 "~~~~~ fun refin , args:"; val (ctxt, pblRD, ori, (Store.Node (pI, [py], pys)))

   = (ctxt, (rev pblID), oris, Store.get_node (rev pblID) pblID (get_pbls ()));

       val {where_rls, model, where_, ...} = py: Problem.T

       val model = map (Model_Pattern.adapt_to_type ctxt) model

       val where_ = map (ParseC.adapt_term_to_type ctxt) where_;

       (*if*) M_Match.match_oris ctxt where_rls ori (model, where_) (*then*);

 val return_refin as SOME ["system", "LINEAR"] = SOME (pblRD (** )@ [pI]( **))

 (*follow the trace created in parallel by writeln in Store.get_node and Refine.refin*)

 (*!*)val pblID = ["4x4", "LINEAR", "system"];(**)

 val return_refin as SOME ["system", "LINEAR", "4x4", "4x4", "normalise"] =

           refin ctxt (rev pblID) oris (Store.get_node (rev pblID) pblID (get_pbls ()));

 "~~~~~ fun refin , args:"; val (ctxt, pblRD, ori, (Store.Node (pI, [py], pys)))

   = (ctxt, (rev pblID), oris, Store.get_node (rev pblID) pblID (get_pbls ()));

       val {where_rls, model, where_, ...} = py: Problem.T

       val model = map (Model_Pattern.adapt_to_type ctxt) model

       val where_ = map (ParseC.adapt_term_to_type ctxt) where_

 (*+*)val (**)true(** )false( **) = (*if*)

    M_Match.match_oris ctxt where_rls o_model (model, where_);

 "~~~~~ fun match_oris , args:"; val (ctxt, where_rls, o_model, (model_pattern, where_)) =

   (ctxt, where_rls, o_model, (model, where_));

     val i_model = (flat o (map (chk1_ model_pattern))) o_model;

 (*+*)val "[\n(1, [\"1\"], #Given, equalities, [\"[0 = - 1 * c_4 / - 1]\", \"[0 =\n (- 24 * c_4 + - 24 * L * c_3 + 12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c +\n  - 1 * L \<up> 4 * q_0) /\n - 24]\", \"[0 = c_2]\", \"[0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]\"]), \n(2, [\"1\"], #Given, solveForVars, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"]), \n(3, [\"1\"], #Find, solution, [\"ss'''\"])]"

   = o_model |> O_Model.to_string @{context};

 (*+*)if "[\n" ^

   "(1 ,[1] ,true ,#Given ,Cor equalities\n [0 = - 1 * c_4 / - 1,\n  0 =\n  (- 24 * c_4 + - 24 * L * c_3 + 12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c +\n   - 1 * L \<up> 4 * q_0) /\n  - 24,\n  0 = c_2, 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2] ,(e_s, [[0 = - 1 * c_4 / - 1,\n 0 =\n (- 24 * c_4 + - 24 * L * c_3 + 12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c +\n  - 1 * L \<up> 4 * q_0) /\n - 24,\n 0 = c_2, 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]])), \n" ^

   "(2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2, c_3, c_4] ,(v_s, [[c, c_2, c_3, c_4]])), \n" ^

   "(3 ,[1] ,true ,#Find ,Cor solution ss''' ,(ss''', [ss''']))]"

  = (i_model |> I_Model.to_string @{context}) then () else raise error "i_model CAHNGED";

 (*+*)val "[\"(#Given, (equalities, e_s))\", \"(#Given, (solveForVars, v_s))\", \"(#Find, (solution, ss'''))\"]"

   = model_pattern |> Model_Pattern.to_string @{context}

 (*+*)val "[Length e_s = 4, Length v_s = 4]" = where_ |> UnparseC.terms @{context}

    val mvat = I_Model.variables_TEST model_pattern (I_Model.OLD_to_TEST i_model)

     val complete = chk1_mis mvat i_model model_pattern;

     val (pb as true, (** )_( **)where_'(**)) =

  Pre_Conds.check_OLD ctxt where_rls where_ (model_pattern, I_Model.OLD_to_TEST i_model);

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

   (ctxt, where_rls, where_, (model_pattern, I_Model.OLD_to_TEST i_model));

 (*+*)val [(true, xxx), (true, yyy)] = where_'

 (*+*)val "[Length\n [0 = - 1 * c_4 / - 1,\n  0 =\n  (- 24 * c_4 + - 24 * L * c_3 + 12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c +\n   - 1 * L \<up> 4 * q_0) /\n  - 24,\n  0 = c_2, 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2] =\n4, Length [c, c_2, c_3, c_4] = 4]"

  = where_' |> map #2 |> UnparseC.terms @{context}

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

            of_max_variant model_patt i_model;

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

     val all_variants =

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

         |> flat

         |> distinct op =

     val variants_separated = map (filter_variants' i_model) all_variants

     val sums_corr = map (cnt_corrects) variants_separated

     val sum_variant_s = arrange_args1 sums_corr (1, all_variants)

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

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

     val i_model_max =

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

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

     val env_model = make_env_model equal_descr_pairs

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

     val subst_eval_list =

            make_envs_preconds equal_givens;

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

 "~~~~~ fun xxx , args:"; val ((_, (_, id)), (_, _, _, _, (feedb, _))) = (nth 1 equal_givens);

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

   (id, feedb);

 val return_discern_typ as [] =

            discern_typ id (descr, ts);

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

 (*+*)val "[[0 = - 1 * c_4 / - 1], [0 =\n (- 24 * c_4 + - 24 * L * c_3 + 12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c +\n  - 1 * L \<up> 4 * q_0) /\n - 24], [0 = c_2], [0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]]"

  = ts |> UnparseC.terms @{context}

       val ts = if Model_Pattern.is_list_descr descr

         then if TermC.is_list (hd ts)

           then ts |> map TermC.isalist2list |> flat

           else ts

         else ts

 (*+*)val "[0 = - 1 * c_4 / - 1, 0 =\n(- 24 * c_4 + - 24 * L * c_3 + 12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c +\n - 1 * L \<up> 4 * q_0) /\n- 24, 0 = c_2, 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]"

  = ts |> UnparseC.terms @{context};

   (*if*)  Model_Pattern.typ_of_element descr = HOLogic.boolT (*then*);

 (*+*)val false = all_lhs_atoms ts

 (*-------------------- contine check_OLD -----------------------------------------------------*)

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

 (*+*)if "[\"\n" ^

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

   "(v_s, [c, c_2, c_3, c_4])\", \"\n(ss''', ss''')\"]"

  = (env_model |> Subst.to_string @{context}) then () else error "env_model CAHNGED";

 (*+*)val "[]" = env_eval |> Subst.to_string @{context} (*GOON \<rightarrow> []*)

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

       val full_subst = if env_eval = [] then pres_subst_other

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

       val evals = map (eval ctxt where_rls) full_subst

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

 val return_refin as SOME ["system", "LINEAR", "4x4"] = SOME (pblRD(** ) @ [pI]( **))

 (*follow the trace created in parallel by writeln in Store.get_node and Refine.refin*)

 (*!*)val pblID = ["normalise", "4x4", "LINEAR", "system"];(**)

 val return_refin as SOME ["system", "LINEAR", "4x4", "normalise", "normalise"] =

           refin ctxt (rev pblID) oris (Store.get_node (rev pblID) pblID (get_pbls ()));

 \<close> ML \<open>"----- Refine_Problem (from subp-rooteq.sml) ---------------------------------------------";

 "----------- Refine_Problem (from subp-rooteq.sml) ---------------------------------------------";

 "----------- Refine_Problem (from subp-rooteq.sml) ---------------------------------------------";

 (*

   By child of 2d962612dd0a this test case revealed an undetected failure

   of Specify.find_next_step -- for_problem: these propose Tactic.Refine_Problem,

   but Step_Specify.by_tactic_input (Refine_Problem ["sqroot-test", "univariate", "equation", "test"]..

   encounters "case Refine.problem ... of NONE".

   The failure might be caused by inappropriate problem-hierarchy.

 *)

 val c = [];

 val fmz = ["equality ((x+1)*(x+2)=x \<up> 2+(8::real))", "solveFor x",

 	   "errorBound (eps=0)", "solutions L"];

 val (dI',pI',mI') = ("Test",["sqroot-test", "univariate", "equation", "test"],

 		     ["Test", "squ-equ-test-subpbl1"]);

 (*[], Pbl*)val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))];

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

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

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

 (*=== specify a not-matching problem ---vvvvvvvvvvvvvvvvvvvvvvvvvvvv*)

 val nxt = (Specify_Problem ["LINEAR", "univariate", "equation", "test"]);

 (*=== specify a not-matching problem --- \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> ^*)

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

 val www =

 case f of Test_Out.PpcKF (Test_Out.Problem [],

   {Find = [Incompl "solutions []"], With = [],

    Given = [Correct "equality ((x + 1) * (x + 2) = x \<up> 2 + 8)", Correct "solveFor x"],

    Where = [Correct(*WAS False*) www(*! ! ! ! ! !*)],

    Relate = [],...}) => www(*! ! !*)

 | _ => error "--- Refine_Problem broken 1";

 if www = "matches (x = 0) ((x + 1) * (x + 2) = x \<up> 2 + 8) \<or>\nmatches (?b * x = 0) ((x + 1) * (x + 2) = x \<up> 2 + 8) \<or>\nmatches (?a + x = 0) ((x + 1) * (x + 2) = x \<up> 2 + 8) \<or>\nmatches (?a + ?b * x = 0) ((x + 1) * (x + 2) = x \<up> 2 + 8)"

 then () else error "--- Refine_Problem broken 2";

 (*ML> f; 

 val it = Form' (Test_Out.PpcKF (0,EdUndef,0,Nundef,

         (Problem ["LINEAR", "univariate", "equation", "test"],   <<<<<===== diff.to above WN120313

          {Find=[Incompl "solutions []"],

           Given=[Correct "equality ((x + #1) * (x + #2) = x \<up> #2 + #8)",

                  Correct "solveFor x"],Relate=[],

           Where=[False "matches (x = #0) ((x + #1) * (x + #2) = x \<up> #2 + #8)

                 |\nmatches (?b * x = #0) ((x + #1) * (x + #2) = x \<up> #2 + #8)

                 |\nmatches (?a + x = #0) ((x + #1) * (x + #2) = x \<up> #2 + #8)

         |\nmatches (?a + ?b * x = #0) ((x + #1) * (x + #2) = x \<up> #2 + #8)"],

           With=[]}))) : mout

 *)

 (*/------------------- step into me Add_Find "solutions L" ---------------------------------\*)

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

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

 (*+*)val Add_Find "solutions L" = tac;

       val (pt, p) =

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

   	    case Step.by_tactic tac (pt, p) of

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

   	    | ("unsafe-ok", (_, _, ptp)) => ptp

   	    | ("not-applicable",_) => (pt, p)

   	    | ("end-of-calculation", (_, _, ptp)) => ptp

   	    | ("failure", _) => raise ERROR "sys-raise ERROR"

   	    | _ => raise ERROR "me: uncovered case Step.by_tactic"

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

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

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

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

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

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

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

            switch_specify_solve p_ (pt, ip) (*return from Step.do_next*);

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

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

   val ("ok", ([(Add_Find "solutions L", _, _)], [], _)) =

            specify_do_next (pt, input_pos);

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

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

   Specify.find_next_step ptp;

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

 (*+ store for continuation after find_next_step*)val (p_'_'''''_', tac'''''_') = (p_', tac);

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

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

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

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

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

   val ("dummy", (Pbl, Add_Find "solutions L")) =

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

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

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

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

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

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

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

     val (preok, _) = Pre_Conds.check_OLD ctxt where_rls where_ (pbt, I_Model.OLD_to_TEST pbl);

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

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

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

       val SOME ("#Find", "solutions L") = (*case*)

         item_to_add (ThyC.get_theory @{context} (if dI = ThyC.id_empty then dI' else dI)) oris pbt pbl (*of*);

       (*if*) not preok (*then*);

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

   "(false, matches (x = 0) ((x + 1) * (x + 2) = x \<up> 2 + 8) \<or>\n" ^

     "matches (?b * x = 0) ((x + 1) * (x + 2) = x \<up> 2 + 8) \<or>\n" ^

     "matches (?a + x = 0) ((x + 1) * (x + 2) = x \<up> 2 + 8) \<or>\n" ^

     "matches (?a + ?b * x = 0) ((x + 1) * (x + 2) = x \<up> 2 + 8))]";

   (*TermC.matches  \<up> \<up> \<up> \<up>  \<up> ^ NONE, ok: why then NONE = Refine.problem below?*)

 (*-------------------- stop step into find_next_step ----------------------------------------*)

 (*+ continue after find_next_step*)val (p_', tac) = (p_'_'''''_', tac'''''_')

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

 (*-------------------- contiue step into specify_do_next ------------------------------------*)

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

 val Add_Find "solutions L" =

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

   val ("ok", ([(Add_Find "solutions L", _, _)], [], _)) =

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

 "~~~~~ fun by_tactic_input , args:"; val ((Tactic.Add_Find  ct), (ptp as (pt, pos as (p,_)))) =

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

    Specify.by_Add_ "#Find" ct ptp;

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

   ("#Find", ct, ptp);

 (*-------------------- stop step into -------------------------------------------------------*)

 val (p,f,nxt,pt) = (p''''',f''''',nxt''''',pt'''''); val Add_Find "solutions L" = nxt;

 (*\------------------- step into me Add_Find "solutions L" ---------------------------------/*)

 (*

   WN230814

   repaired 'step into me Add_Find "solutions L"' above (ERROR was Tactic.Refine);

   But with the repair the subsequent steps repeatedly led to Add_Find "solutions L" --

   -- which was NOT repaird, too.

   So we kept the old test code below, because it leads to the correct result "[x = 2]".

 ---------------------- old test code from before above repair -------------------------------

 (*=== refine problem -----vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv*)

 val nxt = (Refine_Problem ["univariate", "equation", "test"]);

 (*=== refine problem ----- \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up>  \<up> ^^*)

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

 (*("Specify_Problem", Specify_Problem ["normalise", "univariate", ...])*)

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

 (*nxt = ("Specify_Theory", Specify_Theory "Test")*)

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

 (*nxt = ("Specify_Method", Specify_Method ["Test", "squ-equ-test-subpbl1"]*)

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

 (*nxt = ("Apply_Method", *)

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

 (*nxt = ("Rewrite_Set", Rewrite_Set "norm_equation")*)

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

 (*nxt = ("Rewrite_Set", Rewrite_Set "Test_simplify")*)

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

 (*Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]*)

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

 (*nxt = Model_Problem ["LINEAR", "univariate", "equation", "test"]*)

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

 (*nxt = ("Add_Given", Add_Given "equality (-6 + 3 * x = 0)"*)

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

 (**)

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

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

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

 (*nxt = Specify_Problem ["LINEAR", "univariate", "equation", "test"])*)

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

 (*xt = ("Specify_Method", Specify_Method ["Test", "solve_linear"])*)

 val nxt = (Refine_Problem ["univariate", "equation", "test"]);

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

 (*("Specify_Problem", Specify_Problem ["LINEAR", "univariate", ...])*)

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

 (*val nxt = ("Specify_Method",Specify_Method ("Test", "solve_linear"))*)

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

 (*val nxt = ("Apply_Method",Apply_Method ("Test", "solve_linear"))*)

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

 (*val nxt = ("Rewrite_Set_Inst",Rewrite_Set_Inst ([#],"isolate_bdv"))*)

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

 (*val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify")*)

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

 (*val nxt = ("Check_Postcond",Check_Postcond ["LINEAR", "univariate", "eq*)

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

 (*val nxt = ("Check_elementwise",Check_elementwise "Assumptions")*)

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

 (*Check_Postcond ["normalise", "univariate", "equation", "test"])*)

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

 val Test_Out.FormKF res = f;

 if res = "[x = 2]"

 then case nxt of End_Proof' => ()

   | _ => error "new behaviour in test:refine.sml:miniscript with mini-subpb 1"

 else error "new behaviour in test:refine.sml:miniscript with mini-subpb 2" 

 *)

 \<close> ML \<open>"----- equation with CalcTree [ = 6 / 5] for timing: with/out adapt_to_type --------------";

 "----------- equation with CalcTree [ = 6 / 5] for timing: with/out adapt_to_type --------------";

 "----------- equation with CalcTree [ = 6 / 5] for timing: with/out adapt_to_type --------------";

 (*for timing copy to Test_Some.thy*)

 States.reset ();

 val model = ["equality (x/(x \<up> 2 - 6*x+9) - 1/(x \<up> 2 - 3*x) =1/x)", "solveFor x", "solutions L"];

 val refs = ("PolyEq"(**), ["univariate", "equation"], ["no_met"]);

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

 Iterator 1;

 moveActiveRoot 1;

 autoCalculate 1 CompleteCalc;

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

 val p = States.get_pos 1 1;

 val (Form f, tac, asms) = ME_Misc.pt_extract ctxt (pt, p);

 if UnparseC.term @{context} f = "[x = 6 / 5]" then () else error "equation for timing CHANGED"

 \<close> ML \<open>"----- refine ad-hoc equation for timing: with/out adapt_to_type -------------------------";

 "----------- refine ad-hoc equation for timing: with/out adapt_to_type -------------------------";

 "----------- refine ad-hoc equation for timing: with/out adapt_to_type -------------------------";

 (*for timing copy to Test_Some.thy*)

 val model = ["equality ((x \<up> 2 - 6*x+9) - (x \<up> 2 - 3*x) = x)", "solveFor x", "solutions L"];

 val (_, pbl_id, _) = ("PolyEq", ["univariate", "equation"], ["no_met"]);

 Refine.xxxxx @{context} model pbl_id;

 (*

 *** pass ["equation", "univariate"] 

 *** pass ["equation", "univariate", "rootX"] 

 *** pass ["equation", "univariate", "LINEAR"] 

 *** pass ["equation", "univariate", "rational"] 

 *** pass ["equation", "univariate", "polynomial"] 

 *** pass ["equation", "univariate", "polynomial", "degree_0"] 

 *** pass ["equation", "univariate", "polynomial", "degree_1"] 

 *** pass ["equation", "univariate", "polynomial", "degree_2"] 

 *** pass ["equation", "univariate", "polynomial", "degree_3"] 

 *** pass ["equation", "univariate", "polynomial", "degree_4"] 

 *** pass ["equation", "univariate", "polynomial", "normalise"] 

 *)

 \<close> ML \<open>

 \<close>

 section \<open>=====eqsy refine_ori' [0 = - 1 * c_4 / - 1, 0 =\n (- 24 * c_4.., ..] ==================\<close>

 ML \<open> (*\<longrightarrow> refine.sml*)

 \<close> ML \<open>"----- refine_ori' [0 = - 1 * c_4 / - 1, 0 =\n (- 24 * c_4.., ..] ------------------------";

 "----------- refine_ori' [0 = - 1 * c_4 / - 1, 0 =\n (- 24 * c_4.., ..] ------------------------";

 "----------- refine_ori' [0 = - 1 * c_4 / - 1, 0 =\n (- 24 * c_4.., ..] ------------------------";

 (*overwrites NEW funs in Test_Theory ABOVE*)

 open Refine

 open M_Match

 open Pre_Conds

 (*overwrites NEW funs in Test_Theory ABOVE*)

 (*

   refinement of the first eqsystem in Biegelinie, IntegrierenUndKonstanteBestimmen2;

   this example was the demonstrator;

   respective data are in ~/proto4/../exp_Statics_Biegel_Timischl_7-70.xml.

   Data for this test are from biegelinie-5.sml, --- me IntegrierenUndKonstanteBestimmen2 ALL ---

 *)

 \<close> ML \<open>

 (*+*)val o_model = [

 (1, [1], "#Given", @{term "equalities"},

   [@{term "[(0::real) = - 1 * c_4 / - 1]"},

    @{term "[(0::real) = (- 24 * c_4 + - 24 * L * c_3 + 12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c +  - 1 * L \<up> 4 * q_0) / - 24]"},

    @{term "[(0::real) = c_2]"},

    @{term "[(0::real) = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]"}] ),

 (*Const ("List.list.Cons", "real \<Rightarrow> real list \<Rightarrow> real list") $ Free ("c", "real") $ Const ("List.list.Nil", "real list"),*)

 (2, [1], "#Given", @{term "solveForVars"},

   [@{term "[c]  ::real list"},

    @{term "[c_2]::real list"},

    @{term "[c_3]::real list"},

    @{term "[c_4]::real list"}] ),

 (3, [1], "#Find",  @{term "solution"},  [@{term "ss'''::bool list"}] )]

 ;

 val SOME ["normalise", "4x4", "LINEAR", "system"] =

            refine_ori @{context} o_model ["LINEAR", "system"];

 \<close> ML \<open>

 "~~~~~ fun refine_ori , args:"; val (ctxt, oris, pblID) =

   (@{context}, o_model, ["LINEAR", "system"]);

     val opt as SOME ["system", "LINEAR", "4x4", "normalise"]

     = app_ptyp (refin ctxt ((rev o tl) pblID) oris) pblID (rev pblID);

 \<close> ML \<open>

 (*

   app_ptyp works strangely, parameter passing is awkward.

   Present refin knows structure of Store.T, thus we bypass app_ptyp

 *)

 (*!*)val pblID = ["LINEAR", "system"];(**)