(* tests on systems of equations

   author: Walther Neuper 050826,

   (c) due to copyright terms

*)

trace_rewrite := false;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

val thy = @{theory "EqSystem"};

val ctxt = Proof_Context.init_global thy;

"----------- 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 error "eqsystem.sml occur_exactly_in 1";

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

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

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

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

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 ^^^ 2 / 2 + L * c + c_2 = True"

then () else 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 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 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 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 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 @{thm LENGTH_NIL})),

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

			  Calc ("Groups.plus_class.plus", eval_binop "#add_"),

			  Calc ("HOL.eq",eval_equal "#equal_")

			  ];

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

if term2str t' = "True" then () 

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

val SOME t = parse thy "solution LL";

atomty (Thm.term_of t);

val SOME t = parse thy "solution LL";

atomty (Thm.term_of t);

val t = str2term 

"(tl (tl (tl v_s))) from v_s occur_exactly_in (NTH 1 (e_s::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 @{thm NTH_CONS}),

			      Thm ("NTH_NIL",num_str @{thm NTH_NIL}),

			      Thm ("TL_CONS",num_str @{thm tl_Cons}),

			      Thm ("TL_NIL",num_str @{thm tl_Nil}),

			      Calc ("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..";

"----------- 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 ---"; (* ... add_commute cf. b42e334c97ee *)

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

				       str2term"c * x") then ()

else 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 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 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 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 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 error "integrate.sml, (. * .) < (. * .) not#6";

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

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

"----------- rewrite in [EqSystem,normalise,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 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 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 error "eqsystem.sml rewrite in 2x2 simplify_System_par.2";

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

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 error "eqsystem.sml rewrite in 2x2 simplify_System_par.3";

"--- 4---";

"----------- 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 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 = (24 * c_2 * EI + 24 * L * c * EI + L ^^^ 4 * q_0) / (24 * EI)]"

then () else 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 = 0 / EI + c_2, 0 = q_0 * L ^^^ 4 / (24 * EI) + (L * c + c_2)]"*)

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

then () else 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 + -1 * (0 / EI),\n L * c + c_2 = 0 + -1 * (q_0 * L ^^^ 4 / (24 * EI))]"*)

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

then () else 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 / EI, L * c + c_2 = -1 * q_0 * L ^^^ 4 / (24 * EI)]"*)

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

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

val xxx = rewrite_set_ thy 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__ = 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 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 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 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 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 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 = 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 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 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 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 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 ^^^ 2 / 2 + 0 * c + c_2," ^

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

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

(*WN120313 in "solution L" above "refine fmz ["LINEAR","system"]" caused an error...*)

"~~~~~ fun refine, args:"; val ((fmz:fmz_), (pblID:pblID)) = (fmz, ["LINEAR","system"]);

"~~~~~ fun refin', args:"; val ((pblRD: pblRD), fmz, pbls, ((Ptyp (pI, [py], [])): pbt ptyp)) =

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

     ((Ptyp ("LINEAR", [get_pbt ["LINEAR","system"]], [])): pbt ptyp));

      val {thy, ppc, where_, prls, ...} = py ;

"~~~~~ fun prep_ori, args:"; val (fmz, thy, pbt) = (fmz, thy, ppc);

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

                                            "0 = -1 * q_0 * L ^^^ 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 fmz ["LINEAR","system"];

case matches of 

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

  Matches (["2x2", "LINEAR", "system"], _),

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

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

			    {Find = [Correct "solution LL"],

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

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

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

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

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

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

case matches of [_,_,

		  Matches

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

		      {Find = [Correct "solution LL"],

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

| _ => 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 LL"];

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 := false;

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 ("Groups.plus_class.plus", eval_binop "#add_") was missing in erls_prls_triangular*)

trace_rewrite:=false;

"===== case 3: 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 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 matches = refine fmz ["LINEAR","system"];

case matches of 

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

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

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

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

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

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

  | _ => error "eqsystem.sml: refine relaxed triangular sys 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 ^^^ 2 * q_0) / 2,\

	   \            0 = c_3,                           \

	   \            0 = c_4]", 

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

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

case matches of 

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

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

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

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

"----------- 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 LL"];

trace_rewrite := false;

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

trace_rewrite:=false;

(*default_print_depth 11;*) matches; (*default_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 v_s"]),

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

			],

		       append_rls "e_rls" e_rls [(*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) = (split_did o Thm.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_ (thy2ctxt @{theory Isac_Knowledge}))) 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] ,(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 (itms2str_ (thy2ctxt @{theory Isac_Knowledge}))) 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])","

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

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,normalise,2x2] -------------------------";

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

"----------- me [EqSystem,normalise,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 LL"];

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

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

   ["EqSystem","normalise","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 ["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(*["(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", ["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 PblObj {probl,...} = get_obj I pt [5];

    (writeln o (itms2str_ (thy2ctxt @{theory Isac_Knowledge}))) 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] ,(v_s, [[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"]) => ()

  | _ => 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 error "eqsystem.sml me [EqSys...2x2] finished f2str f";

case nxt of

    (End_Proof') => ()

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

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

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

"----------- me [linear,system] ..normalise..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 LL"];

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

  ("Biegelinie",["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", "normalise", "2x2"]) => ()

	  | _ => 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 error "eqsystem.sml me simpl. before SubProblem b";

case nxt of

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

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

  | _ => 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_ (thy2ctxt @{theory Isac_Knowledge}))) 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] ,(v_s, [[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"]) => ()

  | _ => 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 ^^^ 3 / (24 * EI), c_2 = 0]"

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

case nxt of

    (End_Proof') => ()

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

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

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

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

val thy = @{theory Isac_Knowledge}

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

reset_states ();

CalcTree [(

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

	  "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]", "FunktionsVariable x"],

	("Biegelinie", ["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;

if term2str t =

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

then () else error "Bsp 7.27";

"----- Bsp 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;

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

then () else error "Bsp 7.27 go through the rewrites in met_eqsys_norm_4x4";

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

reset_states ();

CalcTree [((*WN130908  <ERROR> error in kernel </ERROR>*)

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

	    "Biegelinie y",

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

	    "FunktionsVariable x"],

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

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

(*

moveActiveRoot 1;

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

*)

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

reset_states ();

CalcTree [(

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

	  "Randbedingungen [y 0 = (0::real), y L = 0, y' 0 = 0, y' L = 0]", "FunktionsVariable x"],

	("Biegelinie", ["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";

reset_states ();

CalcTree [(

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

	  "Randbedingungen [Q 0 = q_0 * L, M_b L = 0, y 0 = (0::real), y' 0 = 0]", "FunktionsVariable x"],

	("Biegelinie", ["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   |            STOPPED.WN06? 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 @{thm commute_0_equality}) t;

val SOME (t,_) = rewrite_ thy e_rew_ord e_rls false (num_str @{thm commute_0_equality}) t;

val SOME (t,_) = rewrite_ thy e_rew_ord e_rls false (num_str @{thm commute_0_equality}) t;

if 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]"

then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 1";

val SOME (t,_) = rewrite_set_inst_ thy false subst simplify_System_parenthesized t;

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

then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 2";

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

if 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]"

then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 3";

val SOME (t,_) = rewrite_set_inst_ thy false subst simplify_System_parenthesized t;

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

then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 4";

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

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

then () else error "eqsystem.sml: exp 7.70 normalise 4x4 by rewrite changed";

"----- 7.70 with met normalise: ";

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 LL"];

val (dI',pI',mI') = ("Biegelinie",["LINEAR", "system"], ["no_met"]);

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

(*============ inhibit exn WN120314 TODO: investigate type error (same as above)==

  in next but one test below the same type error.

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

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 (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", "normalise", "4x4"]) => ()

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

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

"----- outcommented before Isabelle2002 --> 2011 -------------------------";

(*-----------------------------------vvvWN080102 Exception- Match raised 

  since associate Rewrite .. Rewrite'_Set

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;

if f2str f ="[c = L * q_0, L * c + c_2 = q_0 * L ^^^ 2 / 2, c_3 = 0, c_4 = 0]" 

then () else error "eqsystem.sml: exp 7.70 normalise 4x4 by met changed";

--------------------------------------------------------------------------*)

"----- 7.70 with met top_down_: me";

val fmz = ["equalities                                         \

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

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

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

  ("Biegelinie",["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", "top_down_substitution", "4x4"]) => ()

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

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;

if nxt = ("End_Proof'", End_Proof') andalso

   f2str f = "[c = L * q_0, c_2 = -1 * L ^^^ 2 * q_0 / 2, c_3 = 0, c_4 = 0]"

then () else error "eqsystem.sml: 7.70 with met top_down_: me";

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

"------- Bsp 7.71";

reset_states ();

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

	     "Randbedingungen [M_b L = 0, y 0 = (0::real), y L = 0, y' 0 = 0]",

	     "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",

	     "AbleitungBiegelinie dy"],

	    ("Biegelinie", ["Biegelinien"],

	     ["IntegrierenUndKonstanteBestimmen2"] ))];

moveActiveRoot 1;

(*

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

##7.71##       |ordered       |subst.singles (recurs) |2x2       |diagonal

c c_2          |c c_2	      |1'		      |1': c c_2 |

          c_4  |      c_3     |2:c_3 -> 4' :c c_2 c_4 |	         |

c c_2 c_3 c_4  |          c_4 |3'                     |	         |

      c_3      |c c_2 c_3 c_4 |3:c_4 -> 4'':c c_2     |4'':c c_2 |      *)

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

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

"------- Bsp 7.72a ---------------vvvvvvvvvvvvv Momentenlinie postponed";

reset_states ();

CalcTree [(["Traegerlaenge L",

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

	    "Biegelinie y",

	    "Randbedingungen [y 0 = (0::real), y L = 0]",

	    "FunktionsVariable x"],

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

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

moveActiveRoot 1;

(*

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

*)

"------- Bsp 7.72b";

reset_states ();

CalcTree [(["Traegerlaenge L","Streckenlast (q_0 / L * x)","Biegelinie y",

	    "Randbedingungen [M_b 0 = 0, M_b L = 0, y 0 = (0::real), y L = 0]",

	    "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",

	    "AbleitungBiegelinie dy"],

	   ("Biegelinie", ["Biegelinien"],

	    ["IntegrierenUndKonstanteBestimmen2"] ))];

moveActiveRoot 1;

(*

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

##7.72b##      |ord. |subst.singles         |ord.triang.

  c_2          |     |			    |c_2  

c c_2	       |     |1:c_2 -> 2':c	    |c_2 c

          c_4  |     |			    |

c c_2 c_3 c_4  |     |3:c_4 -> 4':c c_2 c_3 |c_2 c c_3*)

val t = str2term"[0 = c_2,                                            \

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

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

\ 0 = c_4 + L * c_3 + (60 * L ^^^ 2 * c_2 + 20 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) / (-120 * EI)]";

"------- Bsp 7.73 ---------------vvvvvvvvvvvvv Momentenlinie postponed";

reset_states ();

CalcTree [(["Traegerlaenge L","Momentenlinie ???",(*description unclear*)

	    "Biegelinie y",

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

	    "FunktionsVariable x"],

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

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

moveActiveRoot 1;

(*

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

*)

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

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

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

(*STOPPED.WN08?? replace this test with 7.70 *)

"----- Bsp 7.27";

val fmz = ["equalities \

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

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

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

  ("Biegelinie",["normalise", "4x4", "LINEAR", "system"],

   ["EqSystem","normalise","4x4"]);

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;

"------------------------------------------- Apply_Method...";

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

"[0 = c_4,                                          \

\ 0 = c_4 + L * c_3 +\n (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]";

(*vvvWN080102 Exception- Match raised 

  since associate Rewrite .. Rewrite'_Set

"------------------------------------------- simplify_System_parenthesized...";

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

"[0 = c_4,                                  \

\ 0 = -1 * q_0 * L ^^^ 4 / (-24 * EI) +     \

\     (4 * L ^^^ 3 * c / (-24 * EI) +       \

\     (12 * L ^^^ 2 * c_2 / (-24 * EI) +    \

\     (L * c_3 + c_4))),                    \

\ 0 = c_2,                                  \

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

(*? "(4 * L ^^^ 3 / (-24 * EI) * c" statt "(4 * L ^^^ 3 * c / (-24 * EI)" ?*)

"------------------------------------------- isolate_bdvs...";

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

"[c_4 = 0,\

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

\ c_2 = 0, \

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

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

---------------------------------------------------------------------*)