(* tests on systems of equations

    author: Walther Neuper

    050826,

    (c) due to copyright terms

 use"../smltest/IsacKnowledge/eqsystem.sml";

 use"eqsystem.sml";

 *)

 val thy = EqSystem.thy;

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

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

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

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

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

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

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

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

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

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

 "----------- script [EqSystem,normalize,2x2] ---------------------";

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

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

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

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

 "----------- me [EqSystem,normalize,2x2] -------------------------";

 "----------- me [linear,system] ..normalize..top_down_sub..-------";

 "----------- all systems from Biegelinie -------------------------";

 "----------- 4x4 systems from Biegelinie -------------------------";

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

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

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

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

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

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

 val all = [str2term"c", str2term"c_2", str2term"c_3"];

 val t = str2term"0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2";

 if occur_exactly_in [str2term"c", str2term"c_2"] all t

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

 if not (occur_exactly_in [str2term"c", str2term"c_2", str2term"c_3"] all t)

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

 if not (occur_exactly_in [str2term"c_2"] all t)

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

 val t = str2term"[c,c_2] from_ [c,c_2,c_3] occur_exactly_in \

 		\-1 * q_0 * L ^^^ 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] from_ [c, c_2,\n                c_3] occur_exactly_in -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2 = True" then ()

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

 val t = str2term"[c,c_2,c_3] from_ [c,c_2,c_3] occur_exactly_in \

 		\-1 * q_0 * L ^^^ 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 ^^^ 2 / 2 + L * c + c_2 = False" then ()

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

 val t = str2term"[c_2] from_ [c,c_2,c_3] occur_exactly_in \

 		\-1 * q_0 * L ^^^ 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 ^^^ 2 / 2 + L * c + c_2 = False" then ()

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

 val t = str2term"[] 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 raise error "eval_occur_exactly_in [c, c_2, c_3]";

 val t = 

     str2term

 	"[] from_ [c, c_2, c_3, c_4] occur_exactly_in -1 * (q_0 * L ^^^ 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 ^^^ 2) / 2 = True" then ()

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

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

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

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

 val t = str2term "length_ [x+y=1,y=2] = 2";

 atomty t;

 val testrls = append_rls "testrls" e_rls 

 			 [(Thm ("length_Nil_",num_str length_Nil_)),

 			  (Thm ("length_Cons_",num_str length_Cons_)),

 			  Calc ("op +", eval_binop "#add_"),

 			  Calc ("op =",eval_equal "#equal_")

 			  ];

 val Some (t',_) = rewrite_set_ thy false testrls t;

 if term2str t' = "True" then () 

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

 val Some t = parse EqSystem.thy "solution L";

 atomty (term_of t);

 val Some t = parse Biegelinie.thy "solution L";

 atomty (term_of t);

 val t = str2term 

 "(tl (tl (tl vs_))) from_ vs_ occur_exactly_in (nth_ 1 (es_::bool list))";

 atomty t;

 val t = str2term 

 "(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])";

 val Some (t,_) = 

     rewrite_set_ thy true 

 		 (append_rls "prls_" e_rls 

 			     [Thm ("nth_Cons_",num_str nth_Cons_),

 			      Thm ("nth_Nil_",num_str nth_Nil_),

 			      Thm ("tl_Cons",num_str tl_Cons),

 			      Thm ("tl_Nil",num_str tl_Nil),

 			      Calc ("EqSystem.occur'_exactly'_in", 

 				    eval_occur_exactly_in 

 					"#eval_occur_exactly_in_")

 			      ]) t;

 if t = HOLogic.true_const then () 

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

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

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

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

 "M_b x = c * x + -1 * q_0 * (x ^^^ 2 / 2) + c_2";

 "--- add_commute ---";

 if ord_simplify_System false thy [] (str2term"-1 * q_0 * (x ^^^ 2 / 2)", 

 				       str2term"c * x") then ()

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

 if ord_simplify_System false thy [] (str2term"-1 * q_0 * (x ^^^ 2 / 2)", 

 				       str2term"c_2") then ()

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

 if ord_simplify_System false thy [] (str2term"c * x", 

 				       str2term"c_2") then ()

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

 "--- mult_commute ---";

 if ord_simplify_System false thy [] (str2term"x * c", 

 				       str2term"c * x") then ()

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

 if ord_simplify_System false thy [] (str2term"-1 * q_0 * (x ^^^ 2 / 2) * c", 

 				       str2term"-1 * q_0 * c * (x ^^^ 2 / 2)") 

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

 if ord_simplify_System false thy [] (str2term"-1 * q_0 * (x ^^^ 2 / 2) * c", 

 				       str2term"c * -1 * q_0 * (x ^^^ 2 / 2)") 

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

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

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

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

 val t = str2term"[0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2,\

 	        \0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2]";

 val bdvs = [(str2term"bdv_1",str2term"c"),

 	    (str2term"bdv_2",str2term"c_2")];

 val Some(t,_)= rewrite_set_inst_ thy true bdvs simplify_System_parenthesized t;

 if term2str t = "[0 = -1 * q_0 * L ^^^ 2 / 2 + (L * c + c_2), 0 = c_2]"

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

 val Some (t,_) = rewrite_set_inst_ thy true bdvs isolate_bdvs t;

 if term2str t = "[L * c + c_2 = 0 + -1 * (-1 * q_0 * L ^^^ 2 / 2), c_2 = 0]"

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

 val Some(t,_)= rewrite_set_inst_ thy true bdvs simplify_System t;

 if term2str t = "[L * c + c_2 = q_0 * L ^^^ 2 / 2, c_2 = 0]"

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

 val Some (t,_) = rewrite_set_ thy true order_system t;

 if term2str t = "[c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]"

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

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

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

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

 val thy = Isac.thy (*because of Undeclared constant "Biegelinie.EI*);

 val t = 

     str2term"[0 = c_2 + c * 0 + 1 / EI * (L * q_0 / 12 * 0 ^^^ 3 +         \

 	    \                                     -1 * q_0 / 24 * 0 ^^^ 4),\

 	    \ 0 = c_2 + c * L + 1 / EI * (L * q_0 / 12 * L ^^^ 3 +         \

 	    \                                     -1 * q_0 / 24 * L ^^^ 4)]";

 val Some (t,_) = rewrite_set_ thy true norm_Rational t;

 if term2str t="[0 = c_2, 0 = c_2 + L * c + L ^^^ 4 * q_0 / (EI * 24)]"

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

 val Some(t,_)= rewrite_set_inst_ thy true bdvs simplify_System_parenthesized t;

 if term2str t = "[0 = c_2, 0 = q_0 * L ^^^ 4 / (24 * EI) + (L * c + c_2)]"

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

 val Some (t,_) = rewrite_set_inst_ thy true bdvs isolate_bdvs t;

 if term2str t = "[c_2 = 0, L * c + c_2 = 0 + -1 * (q_0 * L ^^^ 4 / (24 * EI))]"

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

 val Some(t,_)= rewrite_set_inst_ thy true bdvs simplify_System t;

 if term2str t = "[c_2 = 0, L * c + c_2 = -1 * q_0 * L ^^^ 4 / (24 * EI)]"

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

 val xxx = rewrite_set_ thy true order_system t;

 if is_none xxx

 then () else raise 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__ = str2term "c_2 = 77";

 val e2__ = str2term "L * c + c_2 = q_0 * L ^^^ 2 / 2";

 val bdvs = [(str2term"bdv_1",str2term"c"),

 	    (str2term"bdv_2",str2term"c_2")];

 val Some (e2__,_) = rewrite_terms_ thy dummy_ord Erls [e1__] e2__;

 if term2str e2__ = "L * c + 77 = q_0 * L ^^^ 2 / 2" then ()

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

 val Some (e2__,_) = 

     rewrite_set_inst_ thy true bdvs simplify_System_parenthesized e2__;

 if term2str e2__ = "77 + L * c = q_0 * L ^^^ 2 / 2" then ()

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

 val Some (e2__,_) = rewrite_set_inst_ thy true bdvs isolate_bdvs e2__;

 if term2str e2__ = "c = (q_0 * L ^^^ 2 / 2 + -1 * 77) / L" then ()

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

 val t = str2term "[c_2 = 77, c = (q_0 * L ^^^ 2 / 2 + -1 * 77) / L]";

 val Some (t,_) = rewrite_set_ thy true order_system t;

 if term2str t = "[c = (q_0 * L ^^^ 2 / 2 + -1 * 77) / L, c_2 = 77]" then ()

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

 if not (ord_simplify_System

 	    false thy [] 

 	    (str2term"[c_2 = 77, c = (q_0 * L ^^^ 2 / 2 + -1 * 77) / L]", 

 	     str2term"[c = (q_0 * L ^^^ 2 / 2 + -1 * 77) / L, c_2 = 77]")) 

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

 trace_rewrite:=true;

 trace_rewrite:=false;

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

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

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

 (*GOON??: revise rewrite in [EqSystem,normalize,4x4] from before 0609*)

 val t = str2term"[0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c_3 + c_4,\

 	        \0 = -1 * q_0 * L ^^^ 2 / 2 + L * c_3 + c_4,\

 		\c + c_2 + c_3 + c_4 = 0,\

 		\c_2 + c_3 + c_4 = 0]";

 val bdvs = [(str2term"bdv_1",str2term"c"),

 	    (str2term"bdv_2",str2term"c_2"),

 	    (str2term"bdv_3",str2term"c_3"),

 	    (str2term"bdv_4",str2term"c_4")];

 val Some (t,_) = 

     rewrite_set_inst_ thy true bdvs simplify_System_parenthesized t;

 if term2str t = "[0 = c_4, 0 = -1 * q_0 * L ^^^ 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 raise error "eqsystem.sml rewrite in 4x4 simplify_System_paren";

 val Some (t,_) = rewrite_set_inst_ thy true bdvs isolate_bdvs t;

 if term2str t = "[c_4 = 0, \

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

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

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

 val Some(t,_)= rewrite_set_inst_ thy true bdvs simplify_System_parenthesized t;

 if term2str t = "[c_4 = 0,\

 		\ L * c_3 + c_4 = q_0 * L ^^^ 2 / 2,\

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

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

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

 val Some (t,_) = rewrite_set_ thy true order_system t;

 if term2str t = "[c_4 = 0,\

 		\ L * c_3 + c_4 = q_0 * L ^^^ 2 / 2,\

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

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

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

 "----------- script [EqSystem,normalize,2x2] ---------------------";

 "----------- script [EqSystem,normalize,2x2] ---------------------";

 "----------- script [EqSystem,normalize,2x2] ---------------------";

 val str = 

 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \

 \  (let es__ = (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\

 \                                simplify_System_parenthesized False) es_  \

 \   in ([]))";

 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

 val str = 

 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \

 \  (let es__ = (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\

 \                                 simplify_System_parenthesized False) es_  \

 \   in (SubProblem (Biegelinie_,[linear,system],[no_met])\

 \                  []))";

 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

 val str = 

 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \

 \  (let es__ = (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\

 \                                 simplify_System_parenthesized False) es_  \

 \   in (SubProblem (Biegelinie_,[linear,system],[no_met])\

 \                  [bool_list_ es__, real_list_ vs_]))"

 ;

 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

 val str = 

 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \

 \  (let es__ = Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\

 \                                 simplify_System_parenthesized False) es_  \

 \   in (SubProblem (Biegelinie_,[linear,system],[no_met])\

 \                  [bool_list_ es__, real_list_ vs_]))"

 ;

 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

 val str = 

 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \

 \  (let es__ = (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\

 \                                 simplify_System_parenthesized False)) es_  \

 \   in (SubProblem (Biegelinie_,[linear,system],[no_met])\

 \                  [bool_list_ es__, real_list_ vs_]))"

 ;

 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

 val str = 

 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \

 \  (let es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\

 \                                 simplify_System_parenthesized False)) @@\

 \               (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\

 \                                 simplify_System_parenthesized False))) es_\

 \   in (SubProblem (Biegelinie_,[linear,system],[no_met])\

 \                  [bool_list_ es__, real_list_ vs_]))"

 ;

 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

 val str = 

 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \

 \  (let es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\

 \                                 simplify_System_parenthesized False)) @@\

 \               (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\

 \                                 simplify_System_parenthesized False)) @@\

 \               (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\

 \                                 simplify_System_parenthesized False))) es_\

 \   in (SubProblem (Biegelinie_,[linear,system],[no_met])\

 \                  [bool_list_ es__, real_list_ vs_]))"

 ;

 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

 val str = 

 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \

 \  (let es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\

 \                                 simplify_System_parenthesized False)) @@\

 \               (Try (Rewrite_Set_Inst [] isolate_bdvs False)) @@\

 \               (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\

 \                                 simplify_System_parenthesized False)) @@\

 \               (Try (Rewrite_Set order_system False))) es_\

 \   in (SubProblem (Biegelinie_,[linear,system],[no_met])\

 \                  [bool_list_ es__, real_list_ vs_]))"

 ;

 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

 val str = 

 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \

 \  (let es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\

 \                                 simplify_System_parenthesized False)) @@\

 \               (Try (Rewrite_Set_Inst [(bdv_1, hd vs_)]\

 \                                                    isolate_bdvs False)) @@\

 \               (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\

 \                                 simplify_System_parenthesized False)) @@\

 \               (Try (Rewrite_Set order_system False))) es_\

 \   in (SubProblem (Biegelinie_,[linear,system],[no_met])\

 \                  [bool_list_ es__, real_list_ vs_]))"

 ;

 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

 val str = 

 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \

 \  (let es__ = ((Try (Rewrite_Set simplify_System_parenthesized False)) @@\

 \               (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\

 \                                                    isolate_bdvs False)) @@\

 \               (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\

 \                                 simplify_System_parenthesized False)) @@\

 \               (Try (Rewrite_Set order_system False))) es_\

 \   in (SubProblem (Biegelinie_,[linear,system],[no_met])\

 \                  [bool_list_ es__, real_list_ vs_]))"

 ;

 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

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

 (*---vvv-NOT ok-------------------------------------------------------------*)

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

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

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

 val str = 

 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \

 \  (let es__ = (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\

 \                                 simplify_System_parenthesized False) es_  \

 \   in ([]))";

 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

 val str = 

 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \

 \  (let e1__ = Take (hd es_)                \

 \   in ([]))";

 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

 val str = 

 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \

 \  (let e1__ = Take (hd es_);               \

 \       e1__ = Take (hd es_)                \

 \   in ([]))";

 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

 val str = 

 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \

 \  (let e1__ = Take (hd es_);               \

 \       e1__ = (Take (hd es_))\

 \   in ([]))";

 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

 val str = 

 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \

 \  (let e1__ = Take (hd es_);               \

 \       e1__ = ((Rewrite_Set order_system False)) e1__\

 \   in ([]))";

 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

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

 val str = 

 "(Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\

 \                                           isolate_bdvs False) (e1__::bool)";

 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

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

 val str = 

 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \

 \  (let e1__ = Take (hd es_);               \

 \       e1__ = ((Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\

 \                                           isolate_bdvs False)) e1__\

 \   in ([]))";

 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

 val str = 

 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \

 \  (let e1__ = Take (hd es_);               \

 \       e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\

 \                                           isolate_bdvs False)) @@\

 \               (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\

 \                                 simplify_System False)) e1__\

 \   in ([]))";

 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

 val str = 

 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \

 \  (let e1__ = Take (hd es_);               \

 \       e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\

 \                                           isolate_bdvs False)) @@\

 \               (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\

 \                                 simplify_System False))) e1__\

 \   in ([]))";

 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

 val str = 

 "Script SolveSystemScript (es_::bool list) (vs_::real list) =                \

 \  (let e1__ = Take (hd es_);                                                \

 \       e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\

 \                                           isolate_bdvs False)) @@          \

 \               (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\

 \                                 simplify_System False))) e1__;           \

 \       e2__ = Take (hd (tl es_))                                            \

 \   in ([]))";

 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

 val str = 

 "Script SolveSystemScript (es_::bool list) (vs_::real list) =                \

 \  (let e1__ = Take (hd es_);                                                \

 \       e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\

 \                                           isolate_bdvs False)) @@          \

 \               (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\

 \                                 simplify_System False))) e1__;           \

 \       e2__ = Take (hd (tl es_));                                           \

 \       e2__ = Substitute [e1__] e2__                                       \

 \   in ([]))";

 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

 val str = 

 "Script SolveSystemScript (es_::bool list) (vs_::real list) =                \

 \  (let e1__ = Take (hd es_);                                                \

 \       e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\

 \                                           isolate_bdvs False)) @@          \

 \               (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\

 \                                 simplify_System False))) e1__;           \

 \       e2__ = Take (hd (tl es_));                                           \

 \       e2__ = ((Substitute [e1__])) e2__                                  \

 \   in ([]))";

 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

 val str = 

 "Script SolveSystemScript (es_::bool list) (vs_::real list) =                \

 \  (let e1__ = Take (hd es_);                                                \

 \       e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\

 \                                      isolate_bdvs False)) @@               \

 \               (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\

 \                                 simplify_System False))) e1__;           \

 \       e2__ = Take (hd (tl es_));                                           \

 \       e2__ = ((Substitute [e1__]) @@                                       \

 \               (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\

 \                                      isolate_bdvs False)) @@               \

 \               (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\

 \                                 simplify_System False))) e2__            \

 \   in [e1__, e2__])"

 ;

 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

 val str = 

 "Script SolveSystemScript (es_::bool list) (vs_::real list) =                \

 \  (let e1__ = Take (hd es_);                                                \

 \       e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\

 \                                      isolate_bdvs False)) @@               \

 \               (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\

 \                                 simplify_System False))) e1__;           \

 \       e2__ = Take (hd (tl es_));                                           \

 \       e2__ = ((Substitute [e1__]) @@                                       \

 \               (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\

 \                                 simplify_System_parenthesized False)) @@ \

 \               (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\

 \                                      isolate_bdvs False)) @@               \

 \               (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\

 \                                 simplify_System False)) @@               \

 \               (Try (Rewrite_Set order_system False))) e2__                 \

 \   in [e1__, e2__])"

 ;

 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

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

 val str = 

 "Script SolveSystemScript (es_::bool list) (vs_::real list) =                \

 \  (let e1__ = Take (hd es_);                                                \

 \       e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\

 \                                      isolate_bdvs False)) @@               \

 \               (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\

 \                                 simplify_System False))) e1__;           \

 \       e2__ = Take (hd (tl es_));                                           \

 \       e2__ = ((Substitute [e1__]) @@                                       \

 \               (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\

 \                                 simplify_System_parenthesized False)) @@ \

 \               (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\

 \                                      isolate_bdvs False)) @@               \

 \               (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\

 \                                 simplify_System False))) e2__;           \

 \       es__ = Take [e1__, e2__]\

 \   in (Try (Rewrite_Set order_system False)) es__)"

 ;

 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

 (*---vvv-NOT ok-------------------------------------------------------------*)

 atomty sc;

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

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

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

 val str = 

 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \

 \  (let es__ = Take es_;   \

 \       e1__ = hd es__\

 \   in ([]))"

 ;

 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

 val str = 

 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \

 \  (let es__ = Take es_;   \

 \       e1__ = hd es__;    \

 \       e2__ = hd (tl es__)\

 \   in ([]))"

 ;

 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

 val str = 

 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \

 \  (let es__ = Take es_;   \

 \       e1__ = hd es__;    \

 \       e2__ = hd (tl es__);\

 \       es__ = [1=2,3=4]\

 \   in ([]))"

 ;

 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

 val str = 

 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \

 \  (let es__ = Take es_;   \

 \       e1__ = hd es__;    \

 \       e2__ = hd (tl es__);\

 \       es__ = [e1__,e2__]\

 \   in ([]))"

 ;

 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

 val str = 

 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \

 \  (let es__ = Take es_;   \

 \       e1__ = hd es__;    \

 \       e2__ = hd (tl es__);\

 \       es__ = [e1__, Substitute [e1__] e2__];\

 \       es__ = (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\

 \                                 simplify_System False)) es__            \

 \   in ([]))"

 ;

 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

 val str = 

 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \

 \  (let es__ = Take es_;   \

 \       e1__ = hd es__;    \

 \       e2__ = hd (tl es__);\

 \       es__ = [e1__, Substitute [e1__] e2__];\

 \       es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\

 \                                      isolate_bdvs False)) @@               \

 \               (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\

 \                                 simplify_System False))) es__            \

 \   in ([]))"

 ;

 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

 val str = 

 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \

 \  (let es__ = Take es_;   \

 \       e1__ = hd es__;    \

 \       e2__ = hd (tl es__);\

 \       es__ = [e1__, Substitute [e1__] e2__];\

 \       es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\

 \                                 simplify_System_parenthesized False)) @@  \

 \               (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\

 \                                      isolate_bdvs False)) @@               \

 \               (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\

 \                                 simplify_System False))) es__            \

 \   in ([]))"

 ;

 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

 val str = 

 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \

 \  (let es__ = Take es_;                                                     \

 \       e1__ = hd es__;                                                      \

 \       e2__ = hd (tl es__);                                                 \

 \       es__ = [e1__, Substitute [e1__] e2__];                               \

 \       es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\

 \                                 simplify_System_parenthesized False)) @@  \

 \               (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\

 \                                      isolate_bdvs False))              @@  \

 \               (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\

 \                                 simplify_System False))) es__            \

 \   in es__)"

 ;

 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

 val str = 

 "Script SolveSystemScript (es_::bool list) (vs_::real list) =         \

 \  (let es__ = Take es_;                                              \

 \       e1__ = hd es__;                                               \

 \       e2__ = hd (tl es__);                                          \

 \       es__ = [e1__, Substitute [e1__] e2__]                         \

 \   in ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\

 \                                 simplify_System_parenthesized False)) @@   \

 \       (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))] \

 \                              isolate_bdvs False))              @@   \

 \       (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\

 \                                 simplify_System False))) es__)"

 ;

 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

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

 val str = 

 "Script SolveSystemScript (es_::bool list) (vs_::real list) =         \

 \  (let es__ = Take es_;                                              \

 \       e1__ = hd es__;                                               \

 \       e2__ = hd (tl es__);                                          \

 \       es__ = [e1__, Substitute [e1__] e2__]                         "^

 (* this        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ is a script-'Expr'

    which is not yet searched for 'STac's; thus this script does not yet work*)

 "   in ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\

 \                                 simplify_System_parenthesized False)) @@   \

 \       (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))] \

 \                              isolate_bdvs False))              @@   \

 \       (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\

 \                                 simplify_System False))) es__)"

 ;

 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

 (*---vvv-NOT ok-------------------------------------------------------------*)

 atomty sc;

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

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

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

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

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

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

 val matches = refine fmz ["linear","system"];

 case matches of [_,_,_,

 		 Matches (["normalize", "2x2", "linear", "system"],

 			  {Find = [Correct "solution L"],

 			   With = [],

 			   Given =

 			   [Correct

 				"equalities\n [0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2,\n  0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2]",

 				Correct "solveForVars [c, c_2]"],

 			   Where = [],

 			   Relate = []})] => ()

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

 val fmz = ["equalities [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]", 

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

 val matches = refine fmz ["linear","system"];

 case matches of [_,_,

 		 Matches

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

 		      {Find = [Correct "solution L"],

 		       With = [],

 		       Given =

 		       [Correct

 			    "equalities [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 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 ^^^ 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 ^^^ 2 / 2]"],

 		       Relate = []})] => ()

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

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

   the above 'val matches = refine 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 ^^^ 2 / 2]", 

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

 val matches = refine 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 ^^^ 2 / 2]"]*)

 val t = str2term"[c, c_2] from_ [c, c_2] occur_exactly_in nth_ 2\   

 		\[c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]";

 trace_rewrite:=true;

 val Some (t',_) = rewrite_set_ thy false prls_triangular t;

 (*found:...

 ##  try thm: nth_Cons_

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

 ==> nth_ (2 + - 1) [L * c + c_2 = q_0 * L ^^^ 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 Calc ("op +", eval_binop "#add_") was missing in erls_prls_triangular*)

 trace_rewrite:=false;

 (*WN051014------------------------------------------------------------------*)

 "----- relaxed preconditions for triangular system";

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

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

 	   \            0 = c_4,                           \

 	   \            0 = c_3]", 

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

 val matches = refine fmz ["linear","system"];

 (* trace_rewrite := true;

    trace_rewrite := false;

    *)

 (*print_depth 6; matches; print_depth 3;*)

 case matches of 

     [Matches (["linear", "system"], _),

      NoMatch (["2x2", "linear", "system"], _),

      NoMatch (["3x3", "linear", "system"], _),

      Matches (["4x4", "linear", "system"], _),

      NoMatch (["triangular", "4x4", "linear", "system"], _),

      Matches (["normalize", "4x4", "linear", "system"], _)] => ()

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

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

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

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

 	   \            0 = c_3,                           \

 	   \            0 = c_4]", 

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

 val matches = refine fmz ["triangular", "4x4", "linear","system"];

 (* print_depth 11; matches; print_depth 3;

    *)

 case matches of 

     [Matches (["triangular", "4x4", "linear", "system"], _)] => ()

   | _ => raise error "eqsystem.sml: refine relaxed triangular sys Matches";

 val matches = refine fmz ["linear","system"];

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

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

 "----------- 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 ^^^ 2 / 2 + 0 * c + c_2,\

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

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

 trace_rewrite:=true;

 val matches = refine fmz ["2x2", "linear","system"];

 trace_rewrite:=false;

 print_depth 11; matches; print_depth 3;

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

 (*-----fun refin' (pblRD:pblRD) fmz pbls ((Ptyp (pI,[py],[])):pbt ptyp) =

 (* val ((pblRD:pblRD), fmz, pbls, ((Ptyp (pI,[py],[])):pbt ptyp)) =

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

 	((Ptyp ("2x2",[get_pbt ["2x2","linear","system"]],[])):pbt ptyp));

    *)

 > show_types:=true; term2str (hd where_); show_types:=false;

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

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

 -------fun prep_pbt

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

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

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

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

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

 			],

 		       append_rls "e_rls" e_rls [(*for preds in where_*)], 

 		       Some "solveSystem es_ vs_", 

 		       []));

    *)

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

 val equalities_es_ = "equalities es_" : string

 > val (dd, ii) = (split_did o term_of o the o (parse thy)) equalities_es_;

 > show_types:=true; term2str ii; show_types:=false;

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

 ~~~~~~~~~~~~~~~^^^^^^^^^ OK~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

 > val {where_,...} = get_pbt ["2x2", "linear","system"];

 > show_types:=true; term2str (hd where_); show_types:=false;

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

 -----fun refin' ff:

 > (writeln o (itms2str Isac.thy)) itms;

 [

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

  [0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2,

   0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2] ,(es_, [[0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2,

  0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2]])),

 (2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(vs_, [[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 (itms2str Isac.thy)) itms;

 > (writeln o pres2str) pre';

 ..as in refin'

 ----- fun check_preconds'

 > (writeln o env2str) env;

 ["

 (es_, [0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2,

  0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2])","

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

 (ss___, L)"]

 > val es_ = (fst o hd) env;

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

 > val pre1 = hd pres;

 atomty pre1;

 ***

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

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

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

 ~~~~~~~~~~~~~~~~~~~^^^^^^^^^ should be bool list~~~~~~~~~~~~~~~~~~~

 *** . Free (2, real)

 ***

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

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

 *)

 "----------- me [EqSystem,normalize,2x2] -------------------------";

 "----------- me [EqSystem,normalize,2x2] -------------------------";

 "----------- me [EqSystem,normalize,2x2] -------------------------";

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

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

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

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

   ("Biegelinie.thy",["normalize", "2x2", "linear", "system"],

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

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

 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(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",_) => ()

 	  | _ => raise error "eqsystem.sml [EqSystem,normalize,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(*["(bdv_1, c)", "(bdv_2, hd (tl [c, c_2] ... corrected srls; ran only AFTER use"RCODE-root.sml", store_met was NOT SUFFICIENT*);

 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.thy", ["triangular", "2x2", "linear",_])) => ()

   | _ => raise error "eqsystem.sml me [EqSystem,normalize,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"]) => ()

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

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

 val PblObj {probl,...} = get_obj I pt [5];(writeln o(itms2str Isac.thy)) probl;

 (*[

 (1 ,[1] ,true ,#Given ,Cor equalities [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2] ,(es_, [[c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]])),

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

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

 *)

 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"]) => ()

   | _ => raise 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;

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

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

 case nxt of

     (_, End_Proof') => ()

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

 "----------- me [linear,system] ..normalize..top_down_sub..-------";

 "----------- me [linear,system] ..normalize..top_down_sub..-------";

 "----------- me [linear,system] ..normalize..top_down_sub..-------";

 val fmz = 

     ["equalities\

      \[0 = c_2 + c * 0 + 1 / EI * (L * q_0 / 12 * 0 ^^^ 3 +                \

      \                                            -1 * q_0 / 24 * 0 ^^^ 4),\

      \ 0 = c_2 + c * L + 1 / EI * (L * q_0 / 12 * L ^^^ 3 +                \

      \                                            -1 * q_0 / 24 * L ^^^ 4)]",

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

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

   ("Biegelinie.thy",["linear", "system"], ["no_met"]);

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

 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(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", "normalize", "2x2"]) => ()

 	  | _ => raise error "eqsystem.sml [linear,system] specify b";

 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;

 if f2str f = 

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

 then () else raise error "eqsystem.sml me simpl. before SubProblem b";

 case nxt of

     (_, Subproblem ("Biegelinie.thy", ["triangular", "2x2", "linear",_])) => ()

   | _ => raise error "eqsystem.sml me [linear,system] SubProblem b";

 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"]) => ()

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

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

 val PblObj {probl,...} = get_obj I pt [5];(writeln o(itms2str Isac.thy)) probl;

 (*[

 (1 ,[1] ,true ,#Given ,Cor equalities [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2] ,(es_, [[c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]])),

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

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

 *)

 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"]) => ()

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

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

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

 if f2str f = 

 "[c = -1 * q_0 * L ^^^ 4 / (24 * EI * L), c_2 = 0]"

 then () else raise error "eqsystem.sml me [EqSys...2x2] finished f2str f b";

 case nxt of

     (_, End_Proof') => ()

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

 "----------- all systems from Biegelinie -------------------------";

 "----------- all systems from Biegelinie -------------------------";

 "----------- all systems from Biegelinie -------------------------";

 val subst = [(str2term "bdv_1", str2term "c"),

 	     (str2term "bdv_2", str2term "c_2"),

 	     (str2term "bdv_3", str2term "c_3"),

 	     (str2term "bdv_4", str2term "c_4")]; 

 "------- Bsp 7.27";

 states:=[];

 CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y",

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

 	     "FunktionsVariable x"],

 	    ("Biegelinie.thy", ["Biegelinien"],

 		     ["IntegrierenUndKonstanteBestimmen2"]))];

 moveActiveRoot 1;

 (*

 trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;

 ##7.27##          ordered           substs

           c_4       c_2           

 c c_2 c_3 c_4     c c_2             1->2: c

   c_2                       c_4	  

 c c_2             c c_2 c_3 c_4     [2':c, 1:c_2, 3:c_4] -> 4:c_3*)

 val t = str2term"[0 = c_4,                           \

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

 \ 0 = c_2,                                           \

 \ 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2]";

 val Some (t',_) = rewrite_set_ thy false isolate_bdvs_4x4 t;

 term2str t';

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

 "----- 7.27 go through the rewrites in met_eqsys_norm_4x4";

 val t = str2term "0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2";

 val None = rewrite_set_ thy false norm_Rational t;

 val Some (t,_) = 

     rewrite_set_inst_ thy false subst simplify_System_parenthesized t;

 term2str t = "0 = -1 * q_0 * L ^^^ 2 / 2 + (L * c + c_2)";

 "--- isolate_bdvs_4x4";

 (*

 val Some (t,_) = rewrite_set_inst_ thy false subst isolate_bdvs_4x4 t;

 term2str t;

 val Some (t,_) = rewrite_set_inst_ thy false subst simplify_System t;

 term2str t;

 val Some (t,_) = rewrite_set_ thy false order_system t;

 term2str t;

 *)

 "------- Bsp 7.28 ---------------vvvvvvvvvvvvv Momentenlinie postponed";

 states:=[];

 CalcTree [(["Traegerlaenge L","Momentenlinie (-q_0 / L * x^3 / 6)",

 	    "Biegelinie y",

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

 	    "FunktionsVariable x"],

 	   ("Biegelinie.thy", ["vonMomentenlinieZu","Biegelinien"],

 	    ["Biegelinien", "AusMomentenlinie"]))];

 moveActiveRoot 1;

 (*

 trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;

 *)

 "------- Bsp 7.69";

 states:=[];

 CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y",

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

 	     "FunktionsVariable x"],

 	    ("Biegelinie.thy", ["Biegelinien"],

 	     ["IntegrierenUndKonstanteBestimmen2"] ))];

 moveActiveRoot 1;

 (*

 trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;

 ##7.69##          ordered           subst                   2x2

           c_4           c_3         

 c c_2 c_3 c_4     c c_2 c_3	    1:c_3 -> 2:c c_2        2:         c c_2

       c_3                   c_4	 			   

 c c_2 c_3         c c_2 c_3 c_4     3:c_4 -> 4:c c_2 c_3    1:c_3 -> 4:c c_2*)

 val t = str2term"[0 = c_4 + 0 / (-1 * EI),                                   \

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

 \ 0 = c_3 + 0 / (-1 * EI),                                                   \

 \ 0 = c_3 + (6 * L * c_2 + 3 * L ^^^ 2 * c + -1 * L ^^^ 3 * q_0) / (-6 * EI)]";

 "------- Bsp 7.70";

 states:=[];

 CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y",

 	     "Randbedingungen [Q 0 = q_0 * L, M_b L = 0, y 0 = 0, y' 0 = 0]",

 	     "FunktionsVariable x"],

 	    ("Biegelinie.thy", ["Biegelinien"],

 	     ["IntegrierenUndKonstanteBestimmen2"] ))];

 moveActiveRoot 1;

 (*

 trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;

 ##7.70##        |subst

 c		|

 c c_2           |1:c -> 2:c_2

       c_3	|

           c_4   |            GOON test methods @@@@@@@@@@@@@@@@@@@@@@@@@@@*)

 "----- 7.70 go through the rewrites in met_eqsys_norm_4x4";

 val t = str2term"[L * q_0 = c,                       \

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

 		\ 0 = c_4,                           \

 		\ 0 = c_3]";

 val Some (t,_) =

     rewrite_ thy e_rew_ord e_rls false (num_str commute_0_equality) t;

 val Some (t,_) =

     rewrite_ thy e_rew_ord e_rls false (num_str commute_0_equality) t;

 val Some (t,_) =

     rewrite_ thy e_rew_ord e_rls false (num_str commute_0_equality) t;

 term2str t =

    "[L * q_0 = c, (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2 = 0, c_4 = 0,\n c_3 = 0]";

 val Some (t,_) = 

     rewrite_set_inst_ thy false subst simplify_System_parenthesized t;

 term2str t =

 "[L * q_0 = c, -1 * q_0 * L ^^^ 2 / 2 + (L * c + c_2) = 0, c_4 = 0, c_3 = 0]";

 val Some (t,_) = rewrite_set_inst_ thy false subst isolate_bdvs_4x4 t;

 term2str t =

    "[c = (-1 * (L * q_0) + 0) / -1,\n L * c + c_2 = -1 * (-1 * q_0 * L ^^^ 2 / 2) + 0, c_4 = 0, c_3 = 0]";

 val Some (t,_) = 

     rewrite_set_inst_ thy false subst simplify_System_parenthesized t;

 term2str t ="[c = L * q_0, L * c + c_2 = q_0 * L ^^^ 2 / 2, c_4 = 0, c_3 = 0]";

 val Some (t,_) = rewrite_set_ thy false order_system t;

 if term2str t ="[c = L * q_0, L * c + c_2 = q_0 * L ^^^ 2 / 2, c_3 = 0, c_4 = 0]" then ()

 else raise error "eqsystem.sml: exp 7.70 normalize 4x4 by rewrite changed";

 "----- 7.70 with met normalize: ";

 val fmz = ["equalities                                         \

 	    \[L * q_0 = c,                       \

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

 		\ 0 = c_4,                           \

 		\ 0 = c_3]", 

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

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

   ("Biegelinie.thy",["linear", "system"],["no_met"]);

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

 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(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;val (p,_,f,nxt,_,pt) = me nxt p c pt;

 case nxt of (_,Apply_Method ["EqSystem", "normalize", "4x4"]) => ()

 	  | _ => raise error "eqsystem.sml [EqSystem,normalize,4x4] specify";

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