walther@60347: (* Title: Knowledge/eqsystem-1.sml
walther@60347:    author: Walther Neuper 050826,
walther@60347:    (c) due to copyright terms
walther@60347: *)
walther@60347: 
Walther@60567: "-----------------------------------------------------------------------------------------------";
Walther@60567: "table of contents -----------------------------------------------------------------------------";
Walther@60567: "-----------------------------------------------------------------------------------------------";
Walther@60567: "----------- occur_exactly_in ---------------------------------------------------equsystem-1.sml";
Walther@60567: "----------- problems -----------------------------------------------------------equsystem-1.sml";
Walther@60567: "----------- rewrite-order ord_simplify_System ----------------------------------equsystem-1.sml";
Walther@60567: "----------- rewrite in [EqSystem,normalise,2x2] --------------------------------equsystem-1.sml";
Walther@60567: "----------- rewrite example from 2nd [EqSystem,normalise,2x2] ------------------equsystem-1.sml";
Walther@60567: "----------- rewrite in [EqSystem,top_down_substitution,2x2] --------------------equsystem-1.sml";
Walther@60567: "----------- rewrite in [EqSystem,normalise,4x4] --------------------------------equsystem-1.sml";
Walther@60567: "----------- script [EqSystem,top_down_substitution,2x2] Vers.1 -----------------equsystem-1.sml";
Walther@60567: "----------- refine [linear,system]----------------------------------------------equsystem-1.sml";
Walther@60567: "----------- refine [2x2,linear,system] search error-----------------------------equsystem-1.sml";
Walther@60567: "----------- me [EqSystem,normalise,2x2], refine Subproblem ---------------------equsystem-1.sml";
Walther@60567: "----------- me [EqSystem,normalise,2x2], refine Subproblem, step into istate---equsystem-1a.sml";
Walther@60567: "----------- me [linear,system] ..normalise..top_down_sub..----------------------equsystem-2.sml";
Walther@60567: "----------- all systems from Biegelinie ----------------------------------------equsystem-2.sml";
Walther@60567: "----------- 4x4 systems from Biegelinie ----------------------------------------equsystem-2.sml";
Walther@60567: "-----------------------------------------------------------------------------------------------";
Walther@60567: "-----------------------------------------------------------------------------------------------";
Walther@60567: "-----------------------------------------------------------------------------------------------";
walther@60347: 
walther@60347: val thy = @{theory "EqSystem"};
walther@60347: val ctxt = Proof_Context.init_global thy;
walther@60347: 
walther@60347: "----------- occur_exactly_in ------------------------------------";
walther@60347: "----------- occur_exactly_in ------------------------------------";
walther@60347: "----------- occur_exactly_in ------------------------------------";
Walther@60565: val all = [TermC.parse_test @{context}"c", TermC.parse_test @{context}"c_2", TermC.parse_test @{context}"c_3"];
Walther@60565: val t = TermC.parse_test @{context}"0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2";
walther@60347: 
Walther@60565: if occur_exactly_in [TermC.parse_test @{context}"c", TermC.parse_test @{context}"c_2"] all t
walther@60347: then () else error "eqsystem.sml occur_exactly_in 1";
walther@60347: 
Walther@60565: if not (occur_exactly_in [TermC.parse_test @{context}"c", TermC.parse_test @{context}"c_2", TermC.parse_test @{context}"c_3"] all t)
walther@60347: then () else error "eqsystem.sml occur_exactly_in 2";
walther@60347: 
Walther@60565: if not (occur_exactly_in [TermC.parse_test @{context}"c_2"] all t)
walther@60347: then () else error "eqsystem.sml occur_exactly_in 3";
walther@60347: 
Walther@60565: val t = TermC.parse_test @{context}"[c,c_2] from [c,c_2,c_3] occur_exactly_in - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2";
walther@60347: eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
walther@60347: val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
walther@60347: if str = "[c, c_2] from [c, c_2,\n" ^
walther@60347:   "               c_3] occur_exactly_in - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2 = True"
walther@60347: then () else error "eval_occur_exactly_in [c, c_2]";
walther@60347: 
Walther@60565: val t = TermC.parse_test @{context} ("[c,c_2,c_3] from [c,c_2,c_3] occur_exactly_in " ^
walther@60347: 		  "- 1 * q_0 * L \<up> 2 / 2 + L * c + c_2");
walther@60347: val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
walther@60347: if str = "[c, c_2,\n c_3] from [c, c_2,\n" ^
walther@60347: "            c_3] occur_exactly_in - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2 = False"
walther@60347: then () else error "eval_occur_exactly_in [c, c_2, c_3]";
walther@60347: 
Walther@60565: val t = TermC.parse_test @{context}"[c_2] from [c,c_2,c_3] occur_exactly_in \
walther@60347: 		\- 1 * q_0 * L \<up> 2 / 2 + L * c + c_2";
walther@60347: val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
walther@60347: if str = "[c_2] from [c, c_2,\n" ^
walther@60347:   "            c_3] occur_exactly_in - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2 = False"
walther@60347: then () else error "eval_occur_exactly_in [c, c_2, c_3]";
walther@60347: 
Walther@60565: val t = TermC.parse_test @{context}"[] from [c,c_2,c_3] occur_exactly_in 0";
walther@60347: val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
walther@60347: if str = "[] from [c, c_2, c_3] occur_exactly_in 0 = True" then ()
walther@60347: else error "eval_occur_exactly_in [c, c_2, c_3]";
walther@60347: 
walther@60347: val t = 
Walther@60565:     TermC.parse_test @{context}
walther@60347: 	"[] from [c, c_2, c_3, c_4] occur_exactly_in - 1 * (q_0 * L \<up> 2) /2";
walther@60347: val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
walther@60347: if str = "[] from [c, c_2, c_3, c_4] occur_exactly_in \
walther@60347: 	 \- 1 * (q_0 * L \<up> 2) / 2 = True" then ()
walther@60347: else error "eval_occur_exactly_in [c, c_2, c_3, c_4]";
walther@60347: 
walther@60347: "----------- problems --------------------------------------------";
walther@60347: "----------- problems --------------------------------------------";
walther@60347: "----------- problems --------------------------------------------";
Walther@60565: val t = TermC.parse_test @{context} "Length [x+y=1,y=2] = 2";
Walther@60650: TermC.atom_trace_detail @{context} t;
walther@60347: val testrls = Rule_Set.append_rules "testrls" Rule_Set.empty 
walther@60347: 			 [(Thm ("LENGTH_NIL", @{thm LENGTH_NIL})),
walther@60347: 			  (Thm ("LENGTH_CONS", @{thm LENGTH_CONS})),
Walther@60516: 			  Eval (\<^const_name>\<open>plus\<close>, Calc_Binop.numeric "#add_"),
walther@60347: 			  Eval (\<^const_name>\<open>HOL.eq\<close>,eval_equal "#equal_")
walther@60347: 			  ];
Walther@60500: val SOME (t',_) = rewrite_set_ ctxt false testrls t;
walther@60347: if UnparseC.term t' = "True" then () 
walther@60347: else error "eqsystem.sml: length_ [x+y=1,y=2] = 2";
walther@60347: 
Walther@60424: val SOME t = TermC.parseNEW ctxt "solution LL";
Walther@60650: TermC.atom_trace_detail @{context} t;
Walther@60424: val SOME t = TermC.parseNEW ctxt "solution LL";
Walther@60650: TermC.atom_trace_detail @{context} t;
walther@60347: 
Walther@60565: val t = TermC.parse_test @{context} 
walther@60347: "(tl (tl (tl v_s))) from v_s occur_exactly_in (NTH 1 (e_s::bool list))";
Walther@60650: TermC.atom_trace_detail @{context} t;
Walther@60565: val t = TermC.parse_test @{context} ("(tl (tl (tl [c, c_2, c_3, c_4]))) from [c, c_2, c_3, c_4] occur_exactly_in " ^
walther@60347:   "(NTH 1 [c_4 = 1, 2 = 2, 3 = 3, 4 = 4])");
walther@60347: (*----- broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite -----\\
walther@60347:         assume flawed test setup hidden by "handle _ => ..."
walther@60347:         ERROR rewrite__set_ called with 'Erls' for '1 < 1'
walther@60347: val SOME (t,_) = 
Walther@60500:     rewrite_set_ ctxt true 
walther@60347: 		 (Rule_Set.append_rules "prls_" Rule_Set.empty 
walther@60347: 			     [Thm ("NTH_CONS",ThmC.numerals_to_Free @{thm NTH_CONS}),
walther@60347: 			      Thm ("NTH_NIL",ThmC.numerals_to_Free @{thm NTH_NIL}),
walther@60347: 			      Thm ("TL_CONS",ThmC.numerals_to_Free @{thm tl_Cons}),
walther@60347: 			      Thm ("TL_NIL",ThmC.numerals_to_Free @{thm tl_Nil}),
walther@60347: 			      Eval ("EqSystem.occur_exactly_in", eval_occur_exactly_in "#eval_occur_exactly_in_")
walther@60347: 			      ]) t;
walther@60347: if t = @{term True} then () 
walther@60347: else error "eqsystem.sml ..occur_exactly_in (nth_ 1 [c_4..";
walther@60347:         broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite ---//*)
walther@60347: 
walther@60347: 
walther@60347: "----------- rewrite-order ord_simplify_System -------------------";
walther@60347: "----------- rewrite-order ord_simplify_System -------------------";
walther@60347: "----------- rewrite-order ord_simplify_System -------------------";
walther@60347: "M_b x = c * x + - 1 * q_0 * (x \<up> 2 / 2) + c_2";
walther@60347: "--- add.commute ---"; (* ... add.commute cf. b42e334c97ee *)
Walther@60594: if ord_simplify_System false ctxt [] (TermC.parse_test @{context}"- 1 * q_0 * (x \<up> 2 / 2)", 
Walther@60565: 				       TermC.parse_test @{context}"c * x") then ()
walther@60347: else error "integrate.sml, (- 1 * q_0 * (x \<up> 2 / 2)) < (c * x) not#1";
walther@60347: 
Walther@60594: if ord_simplify_System false ctxt [] (TermC.parse_test @{context}"- 1 * q_0 * (x \<up> 2 / 2)", 
Walther@60565: 				       TermC.parse_test @{context}"c_2") then ()
walther@60347: else error "integrate.sml, (- 1 * q_0 * (x \<up> 2 / 2)) < (c_2) not#2";
walther@60347: 
Walther@60594: if ord_simplify_System false ctxt [] (TermC.parse_test @{context}"c * x", 
Walther@60565: 				       TermC.parse_test @{context}"c_2") then ()
walther@60347: else error "integrate.sml, (c * x) < (c_2) not#3";
walther@60347: 
walther@60347: "--- mult.commute ---";
Walther@60594: if ord_simplify_System false ctxt [] (TermC.parse_test @{context}"x * c", 
Walther@60565: 				       TermC.parse_test @{context}"c * x") then ()
walther@60347: else error "integrate.sml, (x * c) < (c * x) not#4";
walther@60347: 
Walther@60594: if ord_simplify_System false ctxt [] (TermC.parse_test @{context}"- 1 * q_0 * (x \<up> 2 / 2) * c", 
Walther@60565: 				       TermC.parse_test @{context}"- 1 * q_0 * c * (x \<up> 2 / 2)") 
walther@60347: then () else error "integrate.sml, (. * .) < (. * .) not#5";
walther@60347: 
Walther@60594: if ord_simplify_System false ctxt [] (TermC.parse_test @{context}"- 1 * q_0 * (x \<up> 2 / 2) * c", 
Walther@60565: 				       TermC.parse_test @{context}"c * - 1 * q_0 * (x \<up> 2 / 2)") 
walther@60347: then () else error "integrate.sml, (. * .) < (. * .) not#6";
walther@60347: 
walther@60347: 
walther@60347: "----------- rewrite in [EqSystem,normalise,2x2] -----------------";
walther@60347: "----------- rewrite in [EqSystem,normalise,2x2] -----------------";
walther@60347: "----------- rewrite in [EqSystem,normalise,2x2] -----------------";
Walther@60565: val t = TermC.parse_test @{context}"[0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2,\
walther@60347: 	        \0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2]";
Walther@60565: val bdvs = [(TermC.parse_test @{context}"bdv_1",TermC.parse_test @{context}"c"),
Walther@60565: 	    (TermC.parse_test @{context}"bdv_2",TermC.parse_test @{context}"c_2")];
Walther@60556: val SOME (t,_) = rewrite_set_inst_ ctxt true bdvs simplify_System_parenthesized t;
walther@60347: if UnparseC.term t = "[0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c + c_2), 0 = c_2]"
walther@60347: then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.1";
walther@60347: 
Walther@60500: val SOME (t,_) = rewrite_set_inst_ ctxt true bdvs isolate_bdvs t;
walther@60347: if UnparseC.term t = "[L * c + c_2 = 0 + - 1 * (- 1 * q_0 * L \<up> 2 / 2), c_2 = 0]"
walther@60347: then () else error "eqsystem.sml rewrite in 2x2 isolate_bdvs";
walther@60347: 
Walther@60556: val SOME (t,_)= rewrite_set_inst_ ctxt true bdvs simplify_System t;
walther@60347: if UnparseC.term t = "[L * c + c_2 = q_0 * L \<up> 2 / 2, c_2 = 0]"
walther@60347: then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.2";
walther@60347: 
walther@60347: "--- 3--- see EqSystem.thy (*..if replaced by 'and' ...*)";
Walther@60500: val SOME (t,_) = rewrite_set_ ctxt true order_system t;
walther@60347: if UnparseC.term t = "[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]"
walther@60347: then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.3";
walther@60347: 
Walther@60567: 
walther@60347: "----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";
walther@60347: "----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";
walther@60347: "----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";
walther@60347: val thy = @{theory "Isac_Knowledge"} (*because of Undeclared constant "Biegelinie.EI*);
Walther@60500: val ctxt = Proof_Context.init_global thy;
walther@60347: val t = 
Walther@60565:     TermC.parse_test @{context}"[0 = c_2 + c * 0 + 1 / EI * (L * q_0 / 12 * 0 \<up> 3 +         \
walther@60347: 	    \                                     - 1 * q_0 / 24 * 0 \<up> 4),\
walther@60347: 	    \ 0 = c_2 + c * L + 1 / EI * (L * q_0 / 12 * L \<up> 3 +         \
walther@60347: 	    \                                     - 1 * q_0 / 24 * L \<up> 4)]";
Walther@60500: val SOME (t, _) = rewrite_set_ ctxt true norm_Rational t;
walther@60347: if UnparseC.term t = (*BEFORE "eliminate ThmC.numerals_to_Free"..
walther@60347:                       "[c_2 = 0, 0 = q_0 * L \<up> 4 / (24 * EI) + (L * c + c_2)]"*)
walther@60347:                       "[0 = c_2, 0 = (24 * c_2 + 24 * L * c + L \<up> 4 * q_0) / 24]"
walther@60347: then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.0b";
walther@60347: 
Walther@60500: val SOME(t, _)= rewrite_set_inst_ ctxt true bdvs simplify_System_parenthesized t;
walther@60347: if UnparseC.term t = (*BEFORE "eliminate ThmC.numerals_to_Free"..
walther@60347:                        "[c_2 = 0, 0 = q_0 * L \<up> 4 / (24 * EI) + (L * c + c_2)]"*)
walther@60347:                        "[0 = c_2, 0 = q_0 * L \<up> 4 / 24 + (L * c + c_2)]"
walther@60347: then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.1b";
walther@60347: 
Walther@60500: val SOME (t,_) = rewrite_set_inst_ ctxt true bdvs isolate_bdvs t;
walther@60347: if UnparseC.term t = (*BEFORE "eliminate ThmC.numerals_to_Free"..
walther@60347:                        "[c_2 = 0, L * c + c_2 = 0 + - 1 * (q_0 * L \<up> 4 / (24 * EI))]"*)
walther@60347:                        "[c_2 = 0, L * c + c_2 = 0 + - 1 * (q_0 * L \<up> 4 / 24)]"
walther@60347: then () else error "eqsystem.sml rewrite in 2x2 isolate_bdvs b";
walther@60347: 
Walther@60500: val SOME(t,_)= rewrite_set_inst_ ctxt true bdvs simplify_System t;
walther@60347: if UnparseC.term t = (*BEFORE "eliminate ThmC.numerals_to_Free"..
walther@60347:                        "[c_2 = 0, L * c + c_2 = - 1 * q_0 * L \<up> 4 / (24 * EI)]"*)
walther@60347:                        "[c_2 = 0, L * c + c_2 = - 1 * q_0 * L \<up> 4 / 24]"
walther@60347: then () else error "eqsystem.sml rewrite in 2x2 simplify_System.2b";
walther@60347: 
Walther@60500: val xxx = rewrite_set_ ctxt true order_system t;
walther@60347: if is_none xxx
walther@60347: then () else error "eqsystem.sml rewrite in 2x2 simplify_System.3b";
walther@60347: 
walther@60347: 
walther@60347: "----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
walther@60347: "----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
walther@60347: "----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
Walther@60565: val e1__ = TermC.parse_test @{context} "c_2 = 77";
Walther@60565: val e2__ = TermC.parse_test @{context} "L * c + c_2 = q_0 * L \<up> 2 / 2";
Walther@60565: val bdvs = [(TermC.parse_test @{context}"bdv_1",TermC.parse_test @{context}"c"),
Walther@60565: 	    (TermC.parse_test @{context}"bdv_2",TermC.parse_test @{context}"c_2")];
Walther@60509: val SOME (e2__,_) = rewrite_terms_ ctxt Rewrite_Ord.function_empty Rule_Set.Empty [e1__] e2__;
walther@60347: if UnparseC.term e2__ = "L * c + 77 = q_0 * L \<up> 2 / 2" then ()
walther@60347: else error "eqsystem.sml top_down_substitution,2x2] subst";
walther@60347: 
walther@60347: val SOME (e2__,_) = 
Walther@60500:     rewrite_set_inst_ ctxt true bdvs simplify_System_parenthesized e2__;
walther@60347: if UnparseC.term e2__ = "77 + L * c = q_0 * L \<up> 2 / 2" then ()
walther@60347: else error "eqsystem.sml top_down_substitution,2x2] simpl_par";
walther@60347: 
Walther@60500: val SOME (e2__,_) = rewrite_set_inst_ ctxt true bdvs isolate_bdvs e2__;
walther@60347: if UnparseC.term e2__ = "c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L" then ()
walther@60347: else error "eqsystem.sml top_down_substitution,2x2] isolate";
walther@60347: 
Walther@60565: val t = TermC.parse_test @{context} "[c_2 = 77, c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L]";
Walther@60500: val SOME (t,_) = rewrite_set_ ctxt true order_system t;
walther@60347: if UnparseC.term t = "[c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L, c_2 = 77]" then ()
walther@60347: else error "eqsystem.sml top_down_substitution,2x2] order_system";
walther@60347: 
walther@60347: if not (ord_simplify_System
Walther@60594: 	    false ctxt [] 
Walther@60565: 	    (TermC.parse_test @{context}"[c_2 = 77, c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L]", 
Walther@60565: 	     TermC.parse_test @{context}"[c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L, c_2 = 77]")) 
walther@60347: then () else error "eqsystem.sml, order_result rew_ord";
walther@60347: 
walther@60347: 
walther@60347: "----------- rewrite in [EqSystem,normalise,4x4] -----------------";
walther@60347: "----------- rewrite in [EqSystem,normalise,4x4] -----------------";
walther@60347: "----------- rewrite in [EqSystem,normalise,4x4] -----------------";
walther@60347: (*STOPPED.WN06?: revise rewrite in [EqSystem,normalise,4x4] from before 0609*)
Walther@60565: val t = TermC.parse_test @{context} (
walther@60347:   "[(0::real) = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c_3 + c_4, " ^ 
walther@60347:   "(0::real) = - 1 * q_0 * L \<up> 2 / 2 + L * c_3 + c_4, " ^ 
walther@60347:   "c + c_2 + c_3 + c_4 = 0, " ^ 
walther@60347:   "c_2 + c_3 + c_4 = 0]");
Walther@60565: val bdvs = [(TermC.parse_test @{context}"bdv_1::real",TermC.parse_test @{context}"c::real"),
Walther@60565: 	    (TermC.parse_test @{context}"bdv_2::real",TermC.parse_test @{context}"c_2::real"),
Walther@60565: 	    (TermC.parse_test @{context}"bdv_3::real",TermC.parse_test @{context}"c_3::real"),
Walther@60565: 	    (TermC.parse_test @{context}"bdv_4::real",TermC.parse_test @{context}"c_4::real")];
walther@60347: val SOME (t, _) = 
Walther@60500:     rewrite_set_inst_ ctxt true bdvs simplify_System_parenthesized t;
walther@60347: if UnparseC.term t = "[0 = c_4, 0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c_3 + c_4),\n c + (c_2 + (c_3 + c_4)) = 0, c_2 + (c_3 + c_4) = 0]"
walther@60347: then () else error "eqsystem.sml rewrite in 4x4 simplify_System_paren";
walther@60347: 
Walther@60500: val SOME (t, _) = rewrite_set_inst_ ctxt true bdvs isolate_bdvs t;
walther@60347: if UnparseC.term t = "[c_4 = 0, \
walther@60347: 	        \L * c_3 + c_4 = 0 + - 1 * (- 1 * q_0 * L \<up> 2 / 2),\n \
walther@60347: 		\c + (c_2 + (c_3 + c_4)) = 0, c_2 + (c_3 + c_4) = 0]"
walther@60347: then () else error "eqsystem.sml rewrite in 4x4 isolate_bdvs";
walther@60347: 
Walther@60500: val SOME(t, _)= rewrite_set_inst_ ctxt true bdvs simplify_System_parenthesized t;
walther@60347: if UnparseC.term t = "[c_4 = 0,\
walther@60347: 		\ L * c_3 + c_4 = q_0 * L \<up> 2 / 2,\
walther@60347: 		\ c + (c_2 + (c_3 + c_4)) = 0,\n\
walther@60347: 		\ c_2 + (c_3 + c_4) = 0]"
walther@60347: then () else error "eqsystem.sml rewrite in 4x4 simplify_System_p..2";
walther@60347: 
Walther@60500: val SOME (t, _) = rewrite_set_ ctxt true order_system t;
walther@60347: if UnparseC.term t = "[c_4 = 0,\
walther@60347: 		\ L * c_3 + c_4 = q_0 * L \<up> 2 / 2,\
walther@60347: 		\ c_2 + (c_3 + c_4) = 0,\n\
walther@60347: 		\ c + (c_2 + (c_3 + c_4)) = 0]"
walther@60347: then () else error "eqsystem.sml rewrite in 4x4 order_system";
walther@60347: 
Walther@60567: 
Walther@60567: 
walther@60347: "----------- refine [linear,system]-------------------------------";
walther@60347: "----------- refine [linear,system]-------------------------------";
walther@60347: "----------- refine [linear,system]-------------------------------";
walther@60347: val fmz =
walther@60347:   ["equalities [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2," ^
walther@60347:                "0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + (c_2::real)]", 
walther@60347: 	   "solveForVars [c, c_2]", "solution LL"];
walther@60347: 
Walther@60575: (*WN120313 in "solution L" above "Refine.xxxxx @{context} fmz ["LINEAR", "system"]" caused an error...*)
Walther@60556: "~~~~~ fun Refine.refine , args:"; val ((fmz: Formalise.model), (pblID:Problem.id)) = (fmz, ["LINEAR", "system"]);
Walther@60556: "~~~~~ fun refin' , args:"; val ((pblRD: Problem.id_reverse), fmz, pbls, ((Store.Node (pI, [py], [])): Problem.T Store.node)) =
walther@60347:    ((rev o tl) pblID, fmz, [(*match list*)],
Walther@60559:      ((Store.Node ("LINEAR", [Problem.from_store ctxt ["LINEAR", "system"]], [])): Problem.T Store.node));
Walther@60586:       val {thy, model, where_, where_rls, ...} = py ;
Walther@60586: "~~~~~ fun O_Model.init, args:"; val (thy, fmz, pbt) = (thy, fmz, model);
walther@60347:         val ctxt = Proof_Context.init_global thy;
walther@60347: "~~~~~ fun declare_constraints, args:"; val (t, ctxt) = (nth 1 fmz, ctxt);
walther@60347:       fun get_vars ((v,T)::vs) = (case raw_explode v |> Library.read_int of
walther@60347:               (_, _::_) => (Free (v,T)::get_vars vs)
walther@60347:             | (_, []  ) => get_vars vs) (*filter out nums as long as 
walther@60347:                                           we have Free ("123",_)*)
walther@60347:         | get_vars [] = [];
walther@60347:                                         t = "equalities [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,"^
walther@60347:                                             "0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + (c_2::real)]";
walther@60347:       val ts = Term.add_frees (Syntax.read_term ctxt t) [] |> get_vars;
walther@60347: val ctxt = Variable.declare_constraints (nth 1 ts) ctxt;
walther@60347: val ctxt = Variable.declare_constraints (nth 2 ts) ctxt;
walther@60347: val ctxt = Variable.declare_constraints (nth 3 ts) ctxt;
walther@60347: val ctxt = Variable.declare_constraints (nth 4 ts) ctxt;
walther@60347:                                         val t = nth 2 fmz; t = "solveForVars [c, c_2]";
walther@60347:       val ts = Term.add_frees (Syntax.read_term ctxt t) [] |> get_vars;
walther@60347: val ctxt = Variable.declare_constraints (nth 1 ts) ctxt;
walther@60347:                                         val t = nth 3 fmz; t = "solution LL";
walther@60347:       (*(Syntax.read_term ctxt t); 
walther@60347: Type unification failed: Clash of types "real" and "_ list"
walther@60347: Type error in application: incompatible operand type
walther@60347: 
walther@60347: Operator:  solution :: bool list \<Rightarrow> toreall
walther@60347: Operand:   L :: real                 ========== L was already present in equalities ========== *)
walther@60347: 
walther@60347: "===== case 1 =====";
Walther@60575: val matches = Refine.xxxxx @{context} fmz ["LINEAR", "system"];
walther@60347: case matches of 
Walther@60556:  [M_Match.Matches (["LINEAR", "system"], _),                      (*Matches*)
Walther@60556:   M_Match.Matches (["2x2", "LINEAR", "system"], _),               (*NoMatch ! GOON !*)
Walther@60556:   M_Match.NoMatch (["triangular", "2x2", "LINEAR", "system"], _), (**)
Walther@60556:   M_Match.Matches (["normalise", "2x2", "LINEAR", "system"],      (**)
Walther@60556:     {Find = [Correct "solution LL"], With = [],                   (**)
Walther@60556:     Given = [Correct "equalities\n [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n  0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]",
Walther@60556:              Correct "solveForVars [c, c_2]"],
Walther@60556:     Where = [],
Walther@60556:     Relate = []})] => ()
walther@60347: | _ => error "eqsystem.sml Refine.refine ['normalise','2x2'...]";
walther@60347: 
walther@60347: "===== case 2 =====";
walther@60347: val fmz = ["equalities [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]", 
walther@60347: 	   "solveForVars [c, c_2]", "solution LL"];
Walther@60575: val matches = Refine.xxxxx @{context} fmz ["LINEAR", "system"];
walther@60347: case matches of [_,_,
walther@60347: 		  M_Match.Matches
walther@60347: 		    (["triangular", "2x2", "LINEAR", "system"],
walther@60347: 		      {Find = [Correct "solution LL"],
walther@60347: 		       With = [],
walther@60347: 		       Given =
walther@60347: 		        [Correct "equalities [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]",
walther@60347: 		         Correct "solveForVars [c, c_2]"],
walther@60347: 		       Where = [Correct
walther@60347: 			"tl [c, c_2] from [c, c_2] occur_exactly_in NTH 1\n      [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]",
walther@60347: 			                Correct
walther@60347: 				"[c, c_2] from [c, c_2] occur_exactly_in NTH 2\n   [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]"],
walther@60347: 		       Relate = []})] => ()
walther@60347: | _ => error "eqsystem.sml Refine.refine ['triangular','2x2'...]";
walther@60347: 
walther@60347: (*WN051014-----------------------------------------------------------------------------------\\
Walther@60575:   the above 'val matches = Refine.xxxxx @{context} fmz ["LINEAR", "system"]'
walther@60347:   didn't work anymore; we investigated in these steps:*)
walther@60347: val fmz = ["equalities [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]", 
walther@60347: 	  "solveForVars [c, c_2]", "solution LL"];
Walther@60575: val matches = Refine.xxxxx @{context} fmz ["triangular", "2x2", "LINEAR", "system"];
walther@60347: (*... resulted in 
walther@60347:    False "[c, c_2] from_ [c, c_2] occur_exactly_in nth_ 2\n    
walther@60347:           [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]"]*)
Walther@60565: val t = TermC.parse_test @{context} ("[c, c_2] from [c, c_2] occur_exactly_in NTH 2" ^   
walther@60347: 		  "[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]");
Walther@60500: 
Walther@60500: val SOME (t', _) = rewrite_set_ ctxt false prls_triangular t;
walther@60347: (*found:...
walther@60347: ##  try thm: NTH_CONS
walther@60347: ###  eval asms: 1 < 2 + - 1
walther@60347: ==> nth_ (2 + - 1) [L * c + c_2 = q_0 * L \<up> 2 / 2] =
walther@60347:     nth_ (2 + - 1 + - 1) []
walther@60347: ####  rls: erls_prls_triangular on: 1 < 2 + - 1
walther@60347: #####  try calc: op <'
walther@60347: ###  asms accepted: ["1 < 2 + - 1"]   stored: ["1 < 2 + - 1"]
walther@60347: 
Walther@60516: ... i.e Eval ("Groups.plus_class.plus", Calc_Binop.numeric "#add_") was missing in erls_prls_triangular*)
walther@60347: (*--------------------------------------------------------------------------------------------//*)
walther@60347: 
walther@60347: 
walther@60347: "===== case 3: relaxed preconditions for triangular system =====";
walther@60347: val fmz = ["equalities [L * q_0 = c,                               \
walther@60347: 	   \            0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2,\
walther@60347: 	   \            0 = c_4,                                           \
walther@60347: 	   \            0 = c_3]", 
walther@60347: 	   "solveForVars [c, c_2, c_3, c_4]", "solution LL"];
walther@60347: (*============ inhibit exn WN120314 TODO: investigate type error (same) in these 2 cases:
walther@60347: probably exn thrown by fun declare_constraints
walther@60347: /-------------------------------------------------------\
walther@60347: Type unification failed
walther@60347: Type error in application: incompatible operand type
walther@60347: 
walther@60347: Operator:  op # c_3 :: 'a list \<Rightarrow> 'a list
walther@60347: Operand:   [c_4] :: 'b list
walther@60347: \-------------------------------------------------------/
walther@60347: val TermC.matches = Refine.refine fmz ["LINEAR", "system"];
walther@60347: case TermC.matches of 
walther@60347:     [M_Match.Matches (["LINEAR", "system"], _),
walther@60347:      M_Match.NoMatch (["2x2", "LINEAR", "system"], _),
walther@60347:      M_Match.NoMatch (["3x3", "LINEAR", "system"], _),
walther@60347:      M_Match.Matches (["4x4", "LINEAR", "system"], _),
walther@60347:      M_Match.NoMatch (["triangular", "4x4", "LINEAR", "system"], _),
walther@60347:      M_Match.Matches (["normalise", "4x4", "LINEAR", "system"], _)] => ()
walther@60347:   | _ => error "eqsystem.sml: Refine.refine relaxed triangular sys M_Match.NoMatch";
walther@60347: (*WN060914 does NOT match, because 3rd and 4th equ are not ordered*)
walther@60347: 
walther@60347: "===== case 4 =====";
walther@60347: val fmz = ["equalities [L * q_0 = c,                                       \
walther@60347: 	   \            0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2,\
walther@60347: 	   \            0 = c_3,                           \
walther@60347: 	   \            0 = c_4]", 
walther@60347: 	   "solveForVars [c, c_2, c_3, c_4]", "solution LL"];
walther@60347: val TermC.matches = Refine.refine fmz ["triangular", "4x4", "LINEAR", "system"];
walther@60347: case TermC.matches of 
walther@60347:     [M_Match.Matches (["triangular", "4x4", "LINEAR", "system"], _)] => ()
walther@60347:   | _ => error "eqsystem.sml: Refine.refine relaxed triangular sys M_Match.NoMatch";
walther@60347: val TermC.matches = Refine.refine fmz ["LINEAR", "system"];
walther@60347: ============ inhibit exn WN120314 ==============================================*)
walther@60347: 
Walther@60567: 
Walther@60567: 
walther@60347: "----------- Refine.refine [2x2,linear,system] search error--------------";
walther@60347: "----------- Refine.refine [2x2,linear,system] search error--------------";
walther@60347: "----------- Refine.refine [2x2,linear,system] search error--------------";
walther@60347: (*didn't go into ["2x2", "LINEAR", "system"]; 
walther@60347:   we investigated in these steps:*)
walther@60347: val fmz = ["equalities [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\
walther@60347: 	               \0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]", 
walther@60347: 	   "solveForVars [c, c_2]", "solution LL"];
Walther@60575: val matches = Refine.xxxxx @{context} fmz ["2x2", "LINEAR", "system"];
walther@60347: (*default_print_depth 11;*) TermC.matches; (*default_print_depth 3;*)
walther@60347: (*brought: 'False "length_ es_ = 2"'*)
walther@60347: 
walther@60347: (*-----fun refin' (pblRD:Problem.id_reverse) fmz pbls ((Store.Node (pI,[py],[])):pbt Store.store) =
walther@60347: (* val ((pblRD:Problem.id_reverse), fmz, pbls, ((Store.Node (pI,[py],[])):pbt Store.store)) =
walther@60347:        (rev ["LINEAR", "system"], fmz, [(*match list*)],
walther@60347: 	((Store.Node ("2x2",[Problem.from_store ["2x2", "LINEAR", "system"]],[])):pbt Store.store));
walther@60347:    *)
walther@60347: > show_types:=true; UnparseC.term (hd where_); show_types:=false;
walther@60347: val it = "length_ (es_::real list) = (2::real)" : string
walther@60347: 
walther@60347: =========================================================================\
walther@60347: -------fun Problem.prep_input
walther@60347: (* val (thy, (pblID, dsc_dats: (string * (string list)) list, 
walther@60347: 		  ev:rls, ca: string option, metIDs:metID list)) =
walther@60347:        (EqSystem.thy, (["system"],
walther@60347: 		       [("#Given" ,["equalities es_", "solveForVars v_s"]),
walther@60347: 			("#Find"  ,["solution ss___"](*___ is copy-named*))
walther@60347: 			],
walther@60347: 		       Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)], 
walther@60347: 		       SOME "solveSystem es_ v_s", 
walther@60347: 		       []));
walther@60347:    *)
walther@60347: > val [("#Given", [equalities_es_, "solveForVars v_s"])] = gi;
walther@60347: val equalities_es_ = "equalities es_" : string
Walther@60583: > val (dd, ii) = ((Model_Pattern.split_descriptor ctxt)  o Thm.term_of o the o (TermC.parse thy)) equalities_es_;
walther@60347: > show_types:=true; UnparseC.term ii; show_types:=false;
walther@60347: val it = "es_::bool list" : string
walther@60347: ~~~~~~~~~~~~~~~ \<up> \<up> \<up>  OK~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
walther@60347: 
walther@60347: > val {where_,...} = Problem.from_store ["2x2", "LINEAR", "system"];
walther@60347: > show_types:=true; UnparseC.term (hd where_); show_types:=false;
walther@60347: 
walther@60347: =========================================================================/
walther@60347: 
walther@60347: -----fun refin' ff:
walther@60360: > (writeln o (I_Model.to_string (Proof_Context.init_global @{theory Isac_Knowledge}))) itms;
walther@60347: [
walther@60347: (1 ,[1] ,true ,#Given ,Cor equalities
walther@60347:  [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,
walther@60347:   0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2] ,(es_, [[0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,
walther@60347:  0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]])),
walther@60347: (2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(v_s, [[c, c_2]])),
walther@60347: (3 ,[1] ,true ,#Find ,Cor solution L ,(ss___, [L]))]
walther@60347: 
walther@60347: > (writeln o pres2str) pre';
walther@60347: [
walther@60347: (false, length_ es_ = 2),
walther@60347: (true, length_ [c, c_2] = 2)]
walther@60347: 
walther@60347: ----- fun match_oris':
walther@60360: > (writeln o (I_Model.to_string (Proof_Context.init_global @{theory Isac_Knowledge}))) itms;
walther@60347: > (writeln o pres2str) pre';
walther@60347: ..as in refin'
walther@60347: 
walther@60347: ----- fun check in Pre_Conds.
walther@60347: > (writeln o env2str) env;
walther@60347: ["
walther@60347: (es_, [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,
walther@60347:  0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2])", "
walther@60347: (v_s, [c, c_2])", "
walther@60347: (ss___, L)"]
walther@60347: 
walther@60347: > val es_ = (fst o hd) env;
walther@60347: val es_ = Free ("es_", "bool List.list") : Term.term
walther@60347: 
walther@60347: > val pre1 = hd pres;
Walther@60650: TermC.atom_trace_detail @{context} pre1;
walther@60347: ***
walther@60347: *** Const (op =, [real, real] => bool)
walther@60347: *** . Const (ListG.length_, real list => real)
walther@60347: *** . . Free (es_, real list)
walther@60347: ~~~~~~~~~~~~~~~~~~~ \<up> \<up> \<up>  should be bool list~~~~~~~~~~~~~~~~~~~
walther@60347: *** . Free (2, real)
walther@60347: ***
walther@60347: 
walther@60347: THE REASON WAS A non-type-constrained variable IN #WHERE OF PROBLEM
walther@60347: ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
walther@60347: *)
walther@60347: 
Walther@60567: 
Walther@60556: "----------- me [EqSystem,normalise,2x2], refine Subproblem ------------------------------------";
Walther@60556: "----------- me [EqSystem,normalise,2x2], refine Subproblem ------------------------------------";
Walther@60556: "----------- me [EqSystem,normalise,2x2], refine Subproblem ------------------------------------";
Walther@60567: val fmz = ["equalities [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2," ^
Walther@60567:                        "0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]", 
walther@60347: 	   "solveForVars [c, c_2]", "solution LL"];
walther@60347: val (dI',pI',mI') =
walther@60347:   ("Biegelinie",["normalise", "2x2", "LINEAR", "system"],
walther@60347:    ["EqSystem", "normalise", "2x2"]);
walther@60347: val p = e_pos'; val c = []; 
Walther@60571: val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))];
walther@60347: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
walther@60347: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
walther@60347: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
walther@60347: val (p,_,f,nxt,_,pt) = me nxt p c pt;
walther@60347: case nxt of Specify_Method ["EqSystem", "normalise", "2x2"] => ()
walther@60347: 	  | _ => error "eqsystem.sml [EqSystem,normalise,2x2] specify";
walther@60347: 
walther@60347: val (p,_,f,nxt,_,pt) = me nxt p c pt;
walther@60347: val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
Walther@60567: val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
walther@60347: val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
walther@60347: val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
walther@60347: val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
walther@60347: case nxt of
walther@60347:     (Subproblem ("Biegelinie", ["triangular", "2x2", "LINEAR",_])) => ()
walther@60347:   | _ => error "eqsystem.sml me [EqSystem,normalise,2x2] SubProblem";
walther@60347: 
walther@60347: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
walther@60347: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
walther@60347: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
walther@60347: val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
walther@60347: case nxt of
walther@60347:     (Specify_Method ["EqSystem", "top_down_substitution", "2x2"]) => ()
walther@60347:   | _ => error "eqsystem.sml me [EqSys...2x2] top_down_substitution";
walther@60347: 
walther@60347: val (p,_,f,nxt,_,pt) = me nxt p c pt;
walther@60347: val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
walther@60347: val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
walther@60347: val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
walther@60347: val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
walther@60347: val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
walther@60347: val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
walther@60347: val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
walther@60347: val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
walther@60347: case nxt of
walther@60347:     (Check_Postcond ["triangular", "2x2", "LINEAR", "system"]) => ()
walther@60347:   | _ => error "eqsystem.sml me Subpbl .[EqSys...2x2] finished";
walther@60347: val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
walther@60347: val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
Walther@60567: (* final test ... ----------------------------------------------------------------------------*)
walther@60347: if f2str f = "[c = L * q_0 / 2, c_2 = 0]" then ()
walther@60347: else error "eqsystem.sml me [EqSys...2x2] finished f2str f";
Walther@60567: 
walther@60347: case nxt of
walther@60347:     (End_Proof') => ()
walther@60347:   | _ => error "eqsystem.sml me [EqSys...2x2] finished End_Proof'";
Walther@60567: 
Walther@60567: Test_Tool.show_pt pt (*[
Walther@60567: (([], Frm), solveSystem
Walther@60567:  [[0 = - 1 * q_0 * 0 \<up> 2 div 2 + 0 * c + c_2],
Walther@60567:   [0 = - 1 * q_0 * L \<up> 2 div 2 + L * c + c_2]]
Walther@60567:  [[c], [c_2]]), 
Walther@60567: (([1], Frm), [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,
Walther@60567:  0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]), 
Walther@60567: (([1], Res), [0 = c_2, 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]), 
Walther@60567: (([2], Res), [0 = c_2, 0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c + c_2)]), 
Walther@60567: (([3], Res), [c_2 = 0, L * c + c_2 = 0 + - 1 * (- 1 * q_0 * L \<up> 2 / 2)]), 
Walther@60567: (([4], Res), [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]), 
Walther@60567: (([5], Pbl), solveSystem [L * c + c_2 = q_0 * L \<up> 2 / 2] [c_2]), 
Walther@60567: (([5, 1], Frm), L * c + c_2 = q_0 * L \<up> 2 / 2), 
Walther@60567: (([5, 1], Res), L * c + 0 = q_0 * L \<up> 2 / 2), 
Walther@60567: (([5, 2], Res), L * c = q_0 * L \<up> 2 / 2), 
Walther@60567: (([5, 3], Res), c = q_0 * L \<up> 2 / 2 / L), 
Walther@60567: (([5, 4], Res), c = L * q_0 / 2), 
Walther@60567: (([5, 5], Frm), [c_2 = 0, c = L * q_0 / 2]), 
Walther@60567: (([5, 5], Res), [c = L * q_0 / 2, c_2 = 0]), 
Walther@60567: (([5], Res), [c = L * q_0 / 2, c_2 = 0]), 
Walther@60567: (([], Res), [c = L * q_0 / 2, c_2 = 0])] 
Walther@60567: *)