(* Title: Knowledge/eqsystem-1.sml

   author: Walther Neuper 050826,

   (c) due to copyright terms

*)

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

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

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

"----------- occur_exactly_in ---------------------------------------------------equsystem-1.sml";

"----------- problems -----------------------------------------------------------equsystem-1.sml";

"----------- rewrite-order ord_simplify_System ----------------------------------equsystem-1.sml";

"----------- rewrite in [EqSystem,normalise,2x2] --------------------------------equsystem-1.sml";

"----------- rewrite example from 2nd [EqSystem,normalise,2x2] ------------------equsystem-1.sml";

"----------- rewrite in [EqSystem,top_down_substitution,2x2] --------------------equsystem-1.sml";

"----------- rewrite in [EqSystem,normalise,4x4] --------------------------------equsystem-1.sml";

"----------- script [EqSystem,top_down_substitution,2x2] Vers.1 -----------------equsystem-1.sml";

"----------- refine [linear,system]----------------------------------------------equsystem-1.sml";

"----------- refine [2x2,linear,system] search error-----------------------------equsystem-1.sml";

"----------- me [EqSystem,normalise,2x2], refine Subproblem ---------------------equsystem-1.sml";

"----------- me [EqSystem,normalise,2x2], refine Subproblem, step into istate---equsystem-1a.sml";

"----------- me [linear,system] ..normalise..top_down_sub..----------------------equsystem-2.sml";

"----------- all systems from Biegelinie ----------------------------------------equsystem-2.sml";

"----------- 4x4 systems from Biegelinie ----------------------------------------equsystem-2.sml";

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

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

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

val thy = @{theory "EqSystem"};

val ctxt = Proof_Context.init_global thy;

"----------- occur_exactly_in ------------------------------------";

"----------- occur_exactly_in ------------------------------------";

"----------- occur_exactly_in ------------------------------------";

val all = [TermC.parse_test @{context}"c", TermC.parse_test @{context}"c_2", TermC.parse_test @{context}"c_3"];

val t = TermC.parse_test @{context}"0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2";

if occur_exactly_in [TermC.parse_test @{context}"c", TermC.parse_test @{context}"c_2"] all t

then () else error "eqsystem.sml occur_exactly_in 1";

if not (occur_exactly_in [TermC.parse_test @{context}"c", TermC.parse_test @{context}"c_2", TermC.parse_test @{context}"c_3"] all t)

then () else error "eqsystem.sml occur_exactly_in 2";

if not (occur_exactly_in [TermC.parse_test @{context}"c_2"] all t)

then () else error "eqsystem.sml occur_exactly_in 3";

val t = TermC.parse_test @{context}"[c,c_2] from [c,c_2,c_3] occur_exactly_in - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2";

eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;

val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;

if str = "[c, c_2] from [c, c_2,\n" ^

  "               c_3] occur_exactly_in - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2 = True"

then () else error "eval_occur_exactly_in [c, c_2]";

val t = TermC.parse_test @{context} ("[c,c_2,c_3] from [c,c_2,c_3] occur_exactly_in " ^

		  "- 1 * q_0 * L \<up> 2 / 2 + L * c + c_2");

val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;

if str = "[c, c_2,\n c_3] from [c, c_2,\n" ^

"            c_3] occur_exactly_in - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2 = False"

then () else error "eval_occur_exactly_in [c, c_2, c_3]";

val t = TermC.parse_test @{context}"[c_2] from [c,c_2,c_3] occur_exactly_in \

		\- 1 * q_0 * L \<up> 2 / 2 + L * c + c_2";

val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;

if str = "[c_2] from [c, c_2,\n" ^

  "            c_3] occur_exactly_in - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2 = False"

then () else error "eval_occur_exactly_in [c, c_2, c_3]";

val t = TermC.parse_test @{context}"[] from [c,c_2,c_3] occur_exactly_in 0";

val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;

if str = "[] from [c, c_2, c_3] occur_exactly_in 0 = True" then ()

else error "eval_occur_exactly_in [c, c_2, c_3]";

val t = 

    TermC.parse_test @{context}

	"[] from [c, c_2, c_3, c_4] occur_exactly_in - 1 * (q_0 * L \<up> 2) /2";

val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;

if str = "[] from [c, c_2, c_3, c_4] occur_exactly_in \

	 \- 1 * (q_0 * L \<up> 2) / 2 = True" then ()

else error "eval_occur_exactly_in [c, c_2, c_3, c_4]";

"----------- problems --------------------------------------------";

"----------- problems --------------------------------------------";

"----------- problems --------------------------------------------";

val t = TermC.parse_test @{context} "Length [x+y=1,y=2] = 2";

TermC.atom_trace_detail @{context} t;

val testrls = Rule_Set.append_rules "testrls" Rule_Set.empty 

			 [(Thm ("LENGTH_NIL", @{thm LENGTH_NIL})),

			  (Thm ("LENGTH_CONS", @{thm LENGTH_CONS})),

			  Eval (\<^const_name>\<open>plus\<close>, Calc_Binop.numeric "#add_"),

			  Eval (\<^const_name>\<open>HOL.eq\<close>,eval_equal "#equal_")

			  ];

val SOME (t',_) = rewrite_set_ ctxt false testrls t;

if UnparseC.term t' = "True" then () 

else error "eqsystem.sml: length_ [x+y=1,y=2] = 2";

val SOME t = TermC.parseNEW ctxt "solution LL";

TermC.atom_trace_detail @{context} t;

val SOME t = TermC.parseNEW ctxt "solution LL";

TermC.atom_trace_detail @{context} t;

val t = TermC.parse_test @{context} 

"(tl (tl (tl v_s))) from v_s occur_exactly_in (NTH 1 (e_s::bool list))";

TermC.atom_trace_detail @{context} t;

val t = TermC.parse_test @{context} ("(tl (tl (tl [c, c_2, c_3, c_4]))) from [c, c_2, c_3, c_4] occur_exactly_in " ^

  "(NTH 1 [c_4 = 1, 2 = 2, 3 = 3, 4 = 4])");

(*----- broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite -----\\

        assume flawed test setup hidden by "handle _ => ..."

        ERROR rewrite__set_ called with 'Erls' for '1 < 1'

val SOME (t,_) = 

    rewrite_set_ ctxt true 

		 (Rule_Set.append_rules "prls_" Rule_Set.empty 

			     [Thm ("NTH_CONS",ThmC.numerals_to_Free @{thm NTH_CONS}),

			      Thm ("NTH_NIL",ThmC.numerals_to_Free @{thm NTH_NIL}),

			      Thm ("TL_CONS",ThmC.numerals_to_Free @{thm tl_Cons}),

			      Thm ("TL_NIL",ThmC.numerals_to_Free @{thm tl_Nil}),

			      Eval ("EqSystem.occur_exactly_in", eval_occur_exactly_in "#eval_occur_exactly_in_")

			      ]) t;

if t = @{term True} then () 

else error "eqsystem.sml ..occur_exactly_in (nth_ 1 [c_4..";

        broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite ---//*)

"----------- rewrite-order ord_simplify_System -------------------";

"----------- rewrite-order ord_simplify_System -------------------";

"----------- rewrite-order ord_simplify_System -------------------";

"M_b x = c * x + - 1 * q_0 * (x \<up> 2 / 2) + c_2";

"--- add.commute ---"; (* ... add.commute cf. b42e334c97ee *)

if ord_simplify_System false ctxt [] (TermC.parse_test @{context}"- 1 * q_0 * (x \<up> 2 / 2)", 

				       TermC.parse_test @{context}"c * x") then ()

else error "integrate.sml, (- 1 * q_0 * (x \<up> 2 / 2)) < (c * x) not#1";

if ord_simplify_System false ctxt [] (TermC.parse_test @{context}"- 1 * q_0 * (x \<up> 2 / 2)", 

				       TermC.parse_test @{context}"c_2") then ()

else error "integrate.sml, (- 1 * q_0 * (x \<up> 2 / 2)) < (c_2) not#2";

if ord_simplify_System false ctxt [] (TermC.parse_test @{context}"c * x", 

				       TermC.parse_test @{context}"c_2") then ()

else error "integrate.sml, (c * x) < (c_2) not#3";

"--- mult.commute ---";

if ord_simplify_System false ctxt [] (TermC.parse_test @{context}"x * c", 

				       TermC.parse_test @{context}"c * x") then ()

else error "integrate.sml, (x * c) < (c * x) not#4";

if ord_simplify_System false ctxt [] (TermC.parse_test @{context}"- 1 * q_0 * (x \<up> 2 / 2) * c", 

				       TermC.parse_test @{context}"- 1 * q_0 * c * (x \<up> 2 / 2)") 

then () else error "integrate.sml, (. * .) < (. * .) not#5";

if ord_simplify_System false ctxt [] (TermC.parse_test @{context}"- 1 * q_0 * (x \<up> 2 / 2) * c", 

				       TermC.parse_test @{context}"c * - 1 * q_0 * (x \<up> 2 / 2)") 

then () else error "integrate.sml, (. * .) < (. * .) not#6";

"----------- rewrite in [EqSystem,normalise,2x2] -----------------";

"----------- rewrite in [EqSystem,normalise,2x2] -----------------";

"----------- rewrite in [EqSystem,normalise,2x2] -----------------";

val t = TermC.parse_test @{context}"[0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2,\

	        \0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2]";

val bdvs = [(TermC.parse_test @{context}"bdv_1",TermC.parse_test @{context}"c"),

	    (TermC.parse_test @{context}"bdv_2",TermC.parse_test @{context}"c_2")];

val SOME (t,_) = rewrite_set_inst_ ctxt true bdvs simplify_System_parenthesized t;

if UnparseC.term t = "[0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c + c_2), 0 = c_2]"

then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.1";

val SOME (t,_) = rewrite_set_inst_ ctxt true bdvs isolate_bdvs t;

if UnparseC.term t = "[L * c + c_2 = 0 + - 1 * (- 1 * q_0 * L \<up> 2 / 2), c_2 = 0]"

then () else error "eqsystem.sml rewrite in 2x2 isolate_bdvs";

val SOME (t,_)= rewrite_set_inst_ ctxt true bdvs simplify_System t;

if UnparseC.term t = "[L * c + c_2 = q_0 * L \<up> 2 / 2, c_2 = 0]"

then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.2";

"--- 3--- see EqSystem.thy (*..if replaced by 'and' ...*)";

val SOME (t,_) = rewrite_set_ ctxt true order_system t;

if UnparseC.term t = "[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]"

then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.3";

"----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";

"----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";

"----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";

val thy = @{theory "Isac_Knowledge"} (*because of Undeclared constant "Biegelinie.EI*);

val ctxt = Proof_Context.init_global thy;

val t = 

    TermC.parse_test @{context}"[0 = c_2 + c * 0 + 1 / EI * (L * q_0 / 12 * 0 \<up> 3 +         \

	    \                                     - 1 * q_0 / 24 * 0 \<up> 4),\

	    \ 0 = c_2 + c * L + 1 / EI * (L * q_0 / 12 * L \<up> 3 +         \

	    \                                     - 1 * q_0 / 24 * L \<up> 4)]";

val SOME (t, _) = rewrite_set_ ctxt true norm_Rational t;

if UnparseC.term t = (*BEFORE "eliminate ThmC.numerals_to_Free"..

                      "[c_2 = 0, 0 = q_0 * L \<up> 4 / (24 * EI) + (L * c + c_2)]"*)

                      "[0 = c_2, 0 = (24 * c_2 + 24 * L * c + L \<up> 4 * q_0) / 24]"

then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.0b";

val SOME(t, _)= rewrite_set_inst_ ctxt true bdvs simplify_System_parenthesized t;

if UnparseC.term t = (*BEFORE "eliminate ThmC.numerals_to_Free"..

                       "[c_2 = 0, 0 = q_0 * L \<up> 4 / (24 * EI) + (L * c + c_2)]"*)

                       "[0 = c_2, 0 = q_0 * L \<up> 4 / 24 + (L * c + c_2)]"

then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.1b";

val SOME (t,_) = rewrite_set_inst_ ctxt true bdvs isolate_bdvs t;

if UnparseC.term t = (*BEFORE "eliminate ThmC.numerals_to_Free"..

                       "[c_2 = 0, L * c + c_2 = 0 + - 1 * (q_0 * L \<up> 4 / (24 * EI))]"*)

                       "[c_2 = 0, L * c + c_2 = 0 + - 1 * (q_0 * L \<up> 4 / 24)]"

then () else error "eqsystem.sml rewrite in 2x2 isolate_bdvs b";

val SOME(t,_)= rewrite_set_inst_ ctxt true bdvs simplify_System t;

if UnparseC.term t = (*BEFORE "eliminate ThmC.numerals_to_Free"..

                       "[c_2 = 0, L * c + c_2 = - 1 * q_0 * L \<up> 4 / (24 * EI)]"*)

                       "[c_2 = 0, L * c + c_2 = - 1 * q_0 * L \<up> 4 / 24]"

then () else error "eqsystem.sml rewrite in 2x2 simplify_System.2b";

val xxx = rewrite_set_ ctxt true order_system t;

if is_none xxx

then () else error "eqsystem.sml rewrite in 2x2 simplify_System.3b";

"----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";

"----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";

"----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";

val e1__ = TermC.parse_test @{context} "c_2 = 77";

val e2__ = TermC.parse_test @{context} "L * c + c_2 = q_0 * L \<up> 2 / 2";

val bdvs = [(TermC.parse_test @{context}"bdv_1",TermC.parse_test @{context}"c"),

	    (TermC.parse_test @{context}"bdv_2",TermC.parse_test @{context}"c_2")];

val SOME (e2__,_) = rewrite_terms_ ctxt Rewrite_Ord.function_empty Rule_Set.Empty [e1__] e2__;

if UnparseC.term e2__ = "L * c + 77 = q_0 * L \<up> 2 / 2" then ()

else error "eqsystem.sml top_down_substitution,2x2] subst";

val SOME (e2__,_) = 

    rewrite_set_inst_ ctxt true bdvs simplify_System_parenthesized e2__;

if UnparseC.term e2__ = "77 + L * c = q_0 * L \<up> 2 / 2" then ()

else error "eqsystem.sml top_down_substitution,2x2] simpl_par";

val SOME (e2__,_) = rewrite_set_inst_ ctxt true bdvs isolate_bdvs e2__;

if UnparseC.term e2__ = "c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L" then ()

else error "eqsystem.sml top_down_substitution,2x2] isolate";

val t = TermC.parse_test @{context} "[c_2 = 77, c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L]";

val SOME (t,_) = rewrite_set_ ctxt true order_system t;

if UnparseC.term t = "[c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L, c_2 = 77]" then ()

else error "eqsystem.sml top_down_substitution,2x2] order_system";

if not (ord_simplify_System

	    false ctxt [] 

	    (TermC.parse_test @{context}"[c_2 = 77, c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L]", 

	     TermC.parse_test @{context}"[c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L, c_2 = 77]")) 

then () else error "eqsystem.sml, order_result rew_ord";

"----------- rewrite in [EqSystem,normalise,4x4] -----------------";

"----------- rewrite in [EqSystem,normalise,4x4] -----------------";

"----------- rewrite in [EqSystem,normalise,4x4] -----------------";

(*STOPPED.WN06?: revise rewrite in [EqSystem,normalise,4x4] from before 0609*)

val t = TermC.parse_test @{context} (

  "[(0::real) = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c_3 + c_4, " ^ 

  "(0::real) = - 1 * q_0 * L \<up> 2 / 2 + L * c_3 + c_4, " ^ 

  "c + c_2 + c_3 + c_4 = 0, " ^ 

  "c_2 + c_3 + c_4 = 0]");

val bdvs = [(TermC.parse_test @{context}"bdv_1::real",TermC.parse_test @{context}"c::real"),

	    (TermC.parse_test @{context}"bdv_2::real",TermC.parse_test @{context}"c_2::real"),

	    (TermC.parse_test @{context}"bdv_3::real",TermC.parse_test @{context}"c_3::real"),

	    (TermC.parse_test @{context}"bdv_4::real",TermC.parse_test @{context}"c_4::real")];

val SOME (t, _) = 

    rewrite_set_inst_ ctxt true bdvs simplify_System_parenthesized t;

if UnparseC.term t = "[0 = c_4, 0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c_3 + c_4),\n c + (c_2 + (c_3 + c_4)) = 0, c_2 + (c_3 + c_4) = 0]"

then () else error "eqsystem.sml rewrite in 4x4 simplify_System_paren";

val SOME (t, _) = rewrite_set_inst_ ctxt true bdvs isolate_bdvs t;

if UnparseC.term t = "[c_4 = 0, \

	        \L * c_3 + c_4 = 0 + - 1 * (- 1 * q_0 * L \<up> 2 / 2),\n \

		\c + (c_2 + (c_3 + c_4)) = 0, c_2 + (c_3 + c_4) = 0]"

then () else error "eqsystem.sml rewrite in 4x4 isolate_bdvs";

val SOME(t, _)= rewrite_set_inst_ ctxt true bdvs simplify_System_parenthesized t;

if UnparseC.term t = "[c_4 = 0,\

		\ L * c_3 + c_4 = q_0 * L \<up> 2 / 2,\

		\ c + (c_2 + (c_3 + c_4)) = 0,\n\

		\ c_2 + (c_3 + c_4) = 0]"

then () else error "eqsystem.sml rewrite in 4x4 simplify_System_p..2";

val SOME (t, _) = rewrite_set_ ctxt true order_system t;

if UnparseC.term t = "[c_4 = 0,\

		\ L * c_3 + c_4 = q_0 * L \<up> 2 / 2,\

		\ c_2 + (c_3 + c_4) = 0,\n\

		\ c + (c_2 + (c_3 + c_4)) = 0]"

then () else error "eqsystem.sml rewrite in 4x4 order_system";

"----------- refine [linear,system]-------------------------------";

"----------- refine [linear,system]-------------------------------";

"----------- refine [linear,system]-------------------------------";

val fmz =

  ["equalities [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2," ^

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

	   "solveForVars [c, c_2]", "solution LL"];

(*WN120313 in "solution L" above "Refine.xxxxx @{context} fmz ["LINEAR", "system"]" caused an error...*)

"~~~~~ fun Refine.refine , args:"; val ((fmz: Formalise.model), (pblID:Problem.id)) = (fmz, ["LINEAR", "system"]);

"~~~~~ fun refin' , args:"; val ((pblRD: Problem.id_reverse), fmz, pbls, ((Store.Node (pI, [py], [])): Problem.T Store.node)) =

   ((rev o tl) pblID, fmz, [(*match list*)],

     ((Store.Node ("LINEAR", [Problem.from_store ctxt ["LINEAR", "system"]], [])): Problem.T Store.node));

      val {thy, model, where_, where_rls, ...} = py ;

"~~~~~ fun O_Model.init, args:"; val (thy, fmz, pbt) = (thy, fmz, model);

        val ctxt = Proof_Context.init_global thy;

"~~~~~ fun declare_constraints, args:"; val (t, ctxt) = (nth 1 fmz, ctxt);

      fun get_vars ((v,T)::vs) = (case raw_explode v |> Library.read_int of

              (_, _::_) => (Free (v,T)::get_vars vs)

            | (_, []  ) => get_vars vs) (*filter out nums as long as 

                                          we have Free ("123",_)*)

        | get_vars [] = [];

                                        t = "equalities [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,"^

                                            "0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + (c_2::real)]";

      val ts = Term.add_frees (Syntax.read_term ctxt t) [] |> get_vars;

val ctxt = Variable.declare_constraints (nth 1 ts) ctxt;

val ctxt = Variable.declare_constraints (nth 2 ts) ctxt;

val ctxt = Variable.declare_constraints (nth 3 ts) ctxt;

val ctxt = Variable.declare_constraints (nth 4 ts) ctxt;

                                        val t = nth 2 fmz; t = "solveForVars [c, c_2]";

      val ts = Term.add_frees (Syntax.read_term ctxt t) [] |> get_vars;

val ctxt = Variable.declare_constraints (nth 1 ts) ctxt;

                                        val t = nth 3 fmz; t = "solution LL";

      (*(Syntax.read_term ctxt t); 

Type unification failed: Clash of types "real" and "_ list"

Type error in application: incompatible operand type

Operator:  solution :: bool list \<Rightarrow> toreall

Operand:   L :: real                 ========== L was already present in equalities ========== *)

"===== case 1 =====";

val matches = Refine.xxxxx @{context} fmz ["LINEAR", "system"];

case matches of 

 [M_Match.Matches (["LINEAR", "system"], _),                      (*Matches*)

  M_Match.Matches (["2x2", "LINEAR", "system"], _),               (*NoMatch ! GOON !*)

  M_Match.NoMatch (["triangular", "2x2", "LINEAR", "system"], _), (**)

  M_Match.Matches (["normalise", "2x2", "LINEAR", "system"],      (**)

    {Find = [Correct "solution LL"], With = [],                   (**)

    Given = [Correct "equalities\n [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n  0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]",

             Correct "solveForVars [c, c_2]"],

    Where = [],

    Relate = []})] => ()

| _ => error "eqsystem.sml Refine.refine ['normalise','2x2'...]";

"===== case 2 =====";

val fmz = ["equalities [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]", 

	   "solveForVars [c, c_2]", "solution LL"];

val matches = Refine.xxxxx @{context} fmz ["LINEAR", "system"];

case matches of [_,_,

		  M_Match.Matches

		    (["triangular", "2x2", "LINEAR", "system"],

		      {Find = [Correct "solution LL"],

		       With = [],

		       Given =

		        [Correct "equalities [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]",

		         Correct "solveForVars [c, c_2]"],

		       Where = [Correct

			"tl [c, c_2] from [c, c_2] occur_exactly_in NTH 1\n      [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]",

			                Correct

				"[c, c_2] from [c, c_2] occur_exactly_in NTH 2\n   [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]"],

		       Relate = []})] => ()

| _ => error "eqsystem.sml Refine.refine ['triangular','2x2'...]";

(*WN051014-----------------------------------------------------------------------------------\\

  the above 'val matches = Refine.xxxxx @{context} fmz ["LINEAR", "system"]'

  didn't work anymore; we investigated in these steps:*)

val fmz = ["equalities [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]", 

	  "solveForVars [c, c_2]", "solution LL"];

val matches = Refine.xxxxx @{context} fmz ["triangular", "2x2", "LINEAR", "system"];

(*... resulted in 

   False "[c, c_2] from_ [c, c_2] occur_exactly_in nth_ 2\n    

          [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]"]*)

val t = TermC.parse_test @{context} ("[c, c_2] from [c, c_2] occur_exactly_in NTH 2" ^   

		  "[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]");

val SOME (t', _) = rewrite_set_ ctxt false prls_triangular t;

(*found:...

##  try thm: NTH_CONS

###  eval asms: 1 < 2 + - 1

==> nth_ (2 + - 1) [L * c + c_2 = q_0 * L \<up> 2 / 2] =

    nth_ (2 + - 1 + - 1) []

####  rls: erls_prls_triangular on: 1 < 2 + - 1

#####  try calc: op <'

###  asms accepted: ["1 < 2 + - 1"]   stored: ["1 < 2 + - 1"]

... i.e Eval ("Groups.plus_class.plus", Calc_Binop.numeric "#add_") was missing in erls_prls_triangular*)

(*--------------------------------------------------------------------------------------------//*)

"===== case 3: relaxed preconditions for triangular system =====";

val fmz = ["equalities [L * q_0 = c,                               \

	   \            0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2,\

	   \            0 = c_4,                                           \

	   \            0 = c_3]", 

	   "solveForVars [c, c_2, c_3, c_4]", "solution LL"];

(*============ inhibit exn WN120314 TODO: investigate type error (same) in these 2 cases:

probably exn thrown by fun declare_constraints

/-------------------------------------------------------\

Type unification failed

Type error in application: incompatible operand type

Operator:  op # c_3 :: 'a list \<Rightarrow> 'a list

Operand:   [c_4] :: 'b list

\-------------------------------------------------------/

val TermC.matches = Refine.refine fmz ["LINEAR", "system"];

case TermC.matches of 

    [M_Match.Matches (["LINEAR", "system"], _),

     M_Match.NoMatch (["2x2", "LINEAR", "system"], _),

     M_Match.NoMatch (["3x3", "LINEAR", "system"], _),

     M_Match.Matches (["4x4", "LINEAR", "system"], _),

     M_Match.NoMatch (["triangular", "4x4", "LINEAR", "system"], _),

     M_Match.Matches (["normalise", "4x4", "LINEAR", "system"], _)] => ()

  | _ => error "eqsystem.sml: Refine.refine relaxed triangular sys M_Match.NoMatch";

(*WN060914 does NOT match, because 3rd and 4th equ are not ordered*)

"===== case 4 =====";

val fmz = ["equalities [L * q_0 = c,                                       \

	   \            0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2,\

	   \            0 = c_3,                           \

	   \            0 = c_4]", 

	   "solveForVars [c, c_2, c_3, c_4]", "solution LL"];

val TermC.matches = Refine.refine fmz ["triangular", "4x4", "LINEAR", "system"];

case TermC.matches of 

    [M_Match.Matches (["triangular", "4x4", "LINEAR", "system"], _)] => ()

  | _ => error "eqsystem.sml: Refine.refine relaxed triangular sys M_Match.NoMatch";

val TermC.matches = Refine.refine fmz ["LINEAR", "system"];

============ inhibit exn WN120314 ==============================================*)

"----------- Refine.refine [2x2,linear,system] search error--------------";

"----------- Refine.refine [2x2,linear,system] search error--------------";

"----------- Refine.refine [2x2,linear,system] search error--------------";

(*didn't go into ["2x2", "LINEAR", "system"]; 

  we investigated in these steps:*)

val fmz = ["equalities [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\

	               \0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]", 

	   "solveForVars [c, c_2]", "solution LL"];

val matches = Refine.xxxxx @{context} fmz ["2x2", "LINEAR", "system"];

(*default_print_depth 11;*) TermC.matches; (*default_print_depth 3;*)

(*brought: 'False "length_ es_ = 2"'*)

(*-----fun refin' (pblRD:Problem.id_reverse) fmz pbls ((Store.Node (pI,[py],[])):pbt Store.store) =

(* val ((pblRD:Problem.id_reverse), fmz, pbls, ((Store.Node (pI,[py],[])):pbt Store.store)) =

       (rev ["LINEAR", "system"], fmz, [(*match list*)],

	((Store.Node ("2x2",[Problem.from_store ["2x2", "LINEAR", "system"]],[])):pbt Store.store));

   *)

> show_types:=true; UnparseC.term (hd where_); show_types:=false;

val it = "length_ (es_::real list) = (2::real)" : string

=========================================================================\

-------fun Problem.prep_input

(* val (thy, (pblID, dsc_dats: (string * (string list)) list, 

		  ev:rls, ca: string option, metIDs:metID list)) =

       (EqSystem.thy, (["system"],

		       [("#Given" ,["equalities es_", "solveForVars v_s"]),

			("#Find"  ,["solution ss___"](*___ is copy-named*))

			],

		       Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)], 

		       SOME "solveSystem es_ v_s", 

		       []));

   *)

> val [("#Given", [equalities_es_, "solveForVars v_s"])] = gi;

val equalities_es_ = "equalities es_" : string

> val (dd, ii) = ((Model_Pattern.split_descriptor ctxt)  o Thm.term_of o the o (TermC.parse thy)) equalities_es_;

> show_types:=true; UnparseC.term ii; show_types:=false;

val it = "es_::bool list" : string

~~~~~~~~~~~~~~~ \<up> \<up> \<up>  OK~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

> val {where_,...} = Problem.from_store ["2x2", "LINEAR", "system"];

> show_types:=true; UnparseC.term (hd where_); show_types:=false;

=========================================================================/

-----fun refin' ff:

> (writeln o (I_Model.to_string (Proof_Context.init_global @{theory Isac_Knowledge}))) itms;

[

(1 ,[1] ,true ,#Given ,Cor equalities

 [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,

  0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2] ,(es_, [[0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,

 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]])),

(2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(v_s, [[c, c_2]])),

(3 ,[1] ,true ,#Find ,Cor solution L ,(ss___, [L]))]

> (writeln o pres2str) pre';

[

(false, length_ es_ = 2),

(true, length_ [c, c_2] = 2)]

----- fun match_oris':

> (writeln o (I_Model.to_string (Proof_Context.init_global @{theory Isac_Knowledge}))) itms;

> (writeln o pres2str) pre';

..as in refin'

----- fun check in Pre_Conds.

> (writeln o env2str) env;

["

(es_, [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,

 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2])", "

(v_s, [c, c_2])", "

(ss___, L)"]

> val es_ = (fst o hd) env;

val es_ = Free ("es_", "bool List.list") : Term.term

> val pre1 = hd pres;

TermC.atom_trace_detail @{context} pre1;

***

*** Const (op =, [real, real] => bool)

*** . Const (ListG.length_, real list => real)

*** . . Free (es_, real list)

~~~~~~~~~~~~~~~~~~~ \<up> \<up> \<up>  should be bool list~~~~~~~~~~~~~~~~~~~

*** . Free (2, real)

***

THE REASON WAS A non-type-constrained variable IN #WHERE OF PROBLEM

~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

*)

"----------- me [EqSystem,normalise,2x2], refine Subproblem ------------------------------------";

"----------- me [EqSystem,normalise,2x2], refine Subproblem ------------------------------------";

"----------- me [EqSystem,normalise,2x2], refine Subproblem ------------------------------------";

val fmz = ["equalities [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2," ^

                       "0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]", 

	   "solveForVars [c, c_2]", "solution LL"];

val (dI',pI',mI') =

  ("Biegelinie",["normalise", "2x2", "LINEAR", "system"],

   ["EqSystem", "normalise", "2x2"]);

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

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

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

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

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

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

case nxt of Specify_Method ["EqSystem", "normalise", "2x2"] => ()

	  | _ => error "eqsystem.sml [EqSystem,normalise,2x2] specify";

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

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

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

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

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

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

case nxt of

    (Subproblem ("Biegelinie", ["triangular", "2x2", "LINEAR",_])) => ()

  | _ => error "eqsystem.sml me [EqSystem,normalise,2x2] SubProblem";

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

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

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

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

case nxt of

    (Specify_Method ["EqSystem", "top_down_substitution", "2x2"]) => ()

  | _ => error "eqsystem.sml me [EqSys...2x2] top_down_substitution";

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

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

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

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

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

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

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

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

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

case nxt of

    (Check_Postcond ["triangular", "2x2", "LINEAR", "system"]) => ()

  | _ => error "eqsystem.sml me Subpbl .[EqSys...2x2] finished";

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

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

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

if f2str f = "[c = L * q_0 / 2, c_2 = 0]" then ()

else error "eqsystem.sml me [EqSys...2x2] finished f2str f";

case nxt of

    (End_Proof') => ()

  | _ => error "eqsystem.sml me [EqSys...2x2] finished End_Proof'";

Test_Tool.show_pt pt (*[

(([], Frm), solveSystem

 [[0 = - 1 * q_0 * 0 \<up> 2 div 2 + 0 * c + c_2],

  [0 = - 1 * q_0 * L \<up> 2 div 2 + L * c + c_2]]

 [[c], [c_2]]), 

(([1], Frm), [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,

 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]), 

(([1], Res), [0 = c_2, 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]), 

(([2], Res), [0 = c_2, 0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c + c_2)]), 

(([3], Res), [c_2 = 0, L * c + c_2 = 0 + - 1 * (- 1 * q_0 * L \<up> 2 / 2)]), 

(([4], Res), [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]), 

(([5], Pbl), solveSystem [L * c + c_2 = q_0 * L \<up> 2 / 2] [c_2]), 

(([5, 1], Frm), L * c + c_2 = q_0 * L \<up> 2 / 2), 

(([5, 1], Res), L * c + 0 = q_0 * L \<up> 2 / 2), 

(([5, 2], Res), L * c = q_0 * L \<up> 2 / 2), 

(([5, 3], Res), c = q_0 * L \<up> 2 / 2 / L), 

(([5, 4], Res), c = L * q_0 / 2), 

(([5, 5], Frm), [c_2 = 0, c = L * q_0 / 2]), 

(([5, 5], Res), [c = L * q_0 / 2, c_2 = 0]), 

(([5], Res), [c = L * q_0 / 2, c_2 = 0]), 

(([], Res), [c = L * q_0 / 2, c_2 = 0])] 

*)