wneuper/isac: src/smltest/IsacKnowledge/eqsystem.sml@f3181c8e796b (annotated)

wneuper@344	1	(* tests on systems of equations
wneuper@344	2	author: Walther Neuper
wneuper@344	3	050826,
wneuper@344	4	(c) due to copyright terms
wneuper@344	5
wneuper@408	6	use"../smltest/IsacKnowledge/eqsystem.sml";
wneuper@408	7	use"eqsystem.sml";
wneuper@344	8	*)
wneuper@403	9	val thy = EqSystem.thy;
wneuper@403	10
wneuper@403	11	"-----------------------------------------------------------------";
wneuper@403	12	"table of contents -----------------------------------------------";
wneuper@403	13	"-----------------------------------------------------------------";
wneuper@403	14	"----------- occur_exactly_in ------------------------------------";
wneuper@408	15	"----------- problems --------------------------------------------";
wneuper@454	16	"----------- rewrite-order ord_simplify_System -------------------";
wneuper@414	17	"----------- rewrite in [EqSystem,normalize,2x2] -----------------";
wneuper@457	18	"----------- rewrite example from 2nd [EqSystem,normalize,2x2] ---";
wneuper@447	19	"----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
wneuper@418	20	"----------- rewrite in [EqSystem,normalize,4x4] -----------------";
wneuper@412	21	"----------- script [EqSystem,normalize,2x2] ---------------------";
wneuper@446	22	"----------- script [EqSystem,top_down_substitution,2x2] Vers.1 --";
wneuper@446	23	"----------- script [EqSystem,top_down_substitution,2x2] Vers.2 --";
wneuper@445	24	"----------- refine [linear,system]-------------------------------";
wneuper@445	25	"----------- refine [2x2,linear,system] search error--------------";
wneuper@411	26	"----------- me [EqSystem,normalize,2x2] -------------------------";
wneuper@453	27	"----------- me [linear,system] ..normalize..top_down_sub..-------";
wneuper@657	28	"----------- all systems from Biegelinie -------------------------";
wneuper@658	29	"----------- 4x4 systems from Biegelinie -------------------------";
wneuper@403	30	"-----------------------------------------------------------------";
wneuper@403	31	"-----------------------------------------------------------------";
wneuper@403	32	"-----------------------------------------------------------------";
wneuper@403	33
wneuper@403	34
wneuper@403	35	"----------- occur_exactly_in ------------------------------------";
wneuper@403	36	"----------- occur_exactly_in ------------------------------------";
wneuper@403	37	"----------- occur_exactly_in ------------------------------------";
wneuper@403	38	val all = [str2term"c", str2term"c_2", str2term"c_3"];
wneuper@403	39	val t = str2term"0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2";
wneuper@403	40
wneuper@404	41	if occur_exactly_in [str2term"c", str2term"c_2"] all t
wneuper@403	42	then () else raise error "eqsystem.sml occur_exactly_in 1";
wneuper@403	43
wneuper@404	44	if not (occur_exactly_in [str2term"c", str2term"c_2", str2term"c_3"] all t)
wneuper@403	45	then () else raise error "eqsystem.sml occur_exactly_in 2";
wneuper@403	46
wneuper@404	47	if not (occur_exactly_in [str2term"c_2"] all t)
wneuper@403	48	then () else raise error "eqsystem.sml occur_exactly_in 3";
wneuper@403	49
wneuper@403	50
wneuper@404	51	val t = str2term"[c,c_2] from_ [c,c_2,c_3] occur_exactly_in \
wneuper@404	52	\-1 * q_0 * L ^^^ 2 / 2 + L * c + c_2";
wneuper@404	53	val Some (str, t') = eval_occur_exactly_in 0 "EqSystem.occur'_exactly'_in" t 0;
wneuper@404	54	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 ()
wneuper@404	55	else raise error "eval_occur_exactly_in [c, c_2]";
wneuper@404	56
wneuper@404	57	val t = str2term"[c,c_2,c_3] from_ [c,c_2,c_3] occur_exactly_in \
wneuper@404	58	\-1 * q_0 * L ^^^ 2 / 2 + L * c + c_2";
wneuper@404	59	val Some (str, t') = eval_occur_exactly_in 0 "EqSystem.occur'_exactly'_in" t 0;
wneuper@404	60	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 ()
wneuper@404	61	else raise error "eval_occur_exactly_in [c, c_2, c_3]";
wneuper@404	62
wneuper@404	63	val t = str2term"[c_2] from_ [c,c_2,c_3] occur_exactly_in \
wneuper@404	64	\-1 * q_0 * L ^^^ 2 / 2 + L * c + c_2";
wneuper@404	65	val Some (str, t') = eval_occur_exactly_in 0 "EqSystem.occur'_exactly'_in" t 0;
wneuper@404	66	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 ()
wneuper@404	67	else raise error "eval_occur_exactly_in [c, c_2, c_3]";
wneuper@404	68
wneuper@408	69	val t = str2term"[] from_ [c,c_2,c_3] occur_exactly_in 0";
wneuper@408	70	val Some (str, t') = eval_occur_exactly_in 0 "EqSystem.occur'_exactly'_in" t 0;
wneuper@408	71	if str = "[] from_ [c, c_2, c_3] occur_exactly_in 0 = True" then ()
wneuper@408	72	else raise error "eval_occur_exactly_in [c, c_2, c_3]";
wneuper@408	73
wneuper@418	74	val t =
wneuper@418	75	str2term
wneuper@418	76	"[] from_ [c, c_2, c_3, c_4] occur_exactly_in -1 * (q_0 * L ^^^ 2) /2";
wneuper@418	77	val Some (str, t') = eval_occur_exactly_in 0 "EqSystem.occur'_exactly'_in" t 0;
wneuper@418	78	if str = "[] from_ [c, c_2, c_3, c_4] occur_exactly_in \
wneuper@418	79	\-1 * (q_0 * L ^^^ 2) / 2 = True" then ()
wneuper@418	80	else raise error "eval_occur_exactly_in [c, c_2, c_3, c_4]";
wneuper@418	81
wneuper@408	82
wneuper@408	83	"----------- problems --------------------------------------------";
wneuper@408	84	"----------- problems --------------------------------------------";
wneuper@408	85	"----------- problems --------------------------------------------";
wneuper@408	86	val t = str2term "length_ [x+y=1,y=2] = 2";
wneuper@408	87	atomty t;
wneuper@408	88	val testrls = append_rls "testrls" e_rls
wneuper@408	89	[(Thm ("length_Nil_",num_str length_Nil_)),
wneuper@408	90	(Thm ("length_Cons_",num_str length_Cons_)),
wneuper@408	91	Calc ("op +", eval_binop "#add_"),
wneuper@408	92	Calc ("op =",eval_equal "#equal_")
wneuper@408	93	];
wneuper@408	94	val Some (t',_) = rewrite_set_ thy false testrls t;
wneuper@408	95	if term2str t' = "True" then ()
wneuper@408	96	else raise error "eqsystem.sml: length_ [x+y=1,y=2] = 2";
wneuper@408	97
wneuper@411	98	val Some t = parse EqSystem.thy "solution L";
wneuper@411	99	atomty (term_of t);
wneuper@411	100	val Some t = parse Biegelinie.thy "solution L";
wneuper@411	101	atomty (term_of t);
wneuper@408	102
wneuper@425	103	val t = str2term
wneuper@425	104	"(tl (tl (tl vs_))) from_ vs_ occur_exactly_in (nth_ 1 (es_::bool list))";
wneuper@425	105	atomty t;
wneuper@426	106	val t = str2term
wneuper@426	107	"(tl (tl (tl [c,c_2,c_3,c_4]))) from_ [c,c_2,c_3,c_4] occur_exactly_in \
wneuper@426	108	\(nth_ 1 [c_4 = 1, 2=2,3=3,4=4])";
wneuper@426	109	val Some (t,_) =
wneuper@426	110	rewrite_set_ thy true
wneuper@426	111	(append_rls "prls_" e_rls
wneuper@426	112	[Thm ("nth_Cons_",num_str nth_Cons_),
wneuper@426	113	Thm ("nth_Nil_",num_str nth_Nil_),
wneuper@426	114	Thm ("tl_Cons",num_str tl_Cons),
wneuper@426	115	Thm ("tl_Nil",num_str tl_Nil),
wneuper@426	116	Calc ("EqSystem.occur'_exactly'_in",
wneuper@426	117	eval_occur_exactly_in
wneuper@426	118	"#eval_occur_exactly_in_")
wneuper@426	119	]) t;
wneuper@426	120	if t = HOLogic.true_const then ()
wneuper@426	121	else raise error "eqsystem.sml ..occur_exactly_in (nth_ 1 [c_4..";
wneuper@425	122
wneuper@411	123
wneuper@454	124	"----------- rewrite-order ord_simplify_System -------------------";
wneuper@454	125	"----------- rewrite-order ord_simplify_System -------------------";
wneuper@454	126	"----------- rewrite-order ord_simplify_System -------------------";
wneuper@454	127	"M_b x = c * x + -1 * q_0 * (x ^^^ 2 / 2) + c_2";
wneuper@454	128	"--- add_commute ---";
wneuper@454	129	if ord_simplify_System false thy [] (str2term"-1 * q_0 * (x ^^^ 2 / 2)",
wneuper@454	130	str2term"c * x") then ()
wneuper@454	131	else raise error "integrate.sml, (-1 * q_0 * (x ^^^ 2 / 2)) < (c * x) not#1";
wneuper@454	132
wneuper@454	133	if ord_simplify_System false thy [] (str2term"-1 * q_0 * (x ^^^ 2 / 2)",
wneuper@454	134	str2term"c_2") then ()
wneuper@454	135	else raise error "integrate.sml, (-1 * q_0 * (x ^^^ 2 / 2)) < (c_2) not#2";
wneuper@454	136
wneuper@454	137	if ord_simplify_System false thy [] (str2term"c * x",
wneuper@454	138	str2term"c_2") then ()
wneuper@454	139	else raise error "integrate.sml, (c * x) < (c_2) not#3";
wneuper@454	140
wneuper@454	141	"--- mult_commute ---";
wneuper@454	142	if ord_simplify_System false thy [] (str2term"x * c",
wneuper@454	143	str2term"c * x") then ()
wneuper@454	144	else raise error "integrate.sml, (x * c) < (c * x) not#4";
wneuper@454	145
wneuper@454	146	if ord_simplify_System false thy [] (str2term"-1 * q_0 * (x ^^^ 2 / 2) * c",
wneuper@454	147	str2term"-1 * q_0 * c * (x ^^^ 2 / 2)")
wneuper@454	148	then () else raise error "integrate.sml, (. * .) < (. * .) not#5";
wneuper@454	149
wneuper@454	150	if ord_simplify_System false thy [] (str2term"-1 * q_0 * (x ^^^ 2 / 2) * c",
wneuper@454	151	str2term"c * -1 * q_0 * (x ^^^ 2 / 2)")
wneuper@454	152	then () else raise error "integrate.sml, (. * .) < (. * .) not#6";
wneuper@454	153
wneuper@454	154
wneuper@414	155	"----------- rewrite in [EqSystem,normalize,2x2] -----------------";
wneuper@414	156	"----------- rewrite in [EqSystem,normalize,2x2] -----------------";
wneuper@414	157	"----------- rewrite in [EqSystem,normalize,2x2] -----------------";
wneuper@424	158	val t = str2term"[0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2,\
wneuper@424	159	\0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2]";
wneuper@422	160	val bdvs = [(str2term"bdv_1",str2term"c"),
wneuper@422	161	(str2term"bdv_2",str2term"c_2")];
wneuper@454	162	val Some(t,_)= rewrite_set_inst_ thy true bdvs simplify_System_parenthesized t;
wneuper@454	163	if term2str t = "[0 = -1 * q_0 * L ^^^ 2 / 2 + (L * c + c_2), 0 = c_2]"
wneuper@450	164	then () else raise error "eqsystem.sml rewrite in 2x2 simplify_System_par.1";
wneuper@416	165
wneuper@422	166	val Some (t,_) = rewrite_set_inst_ thy true bdvs isolate_bdvs t;
wneuper@454	167	if term2str t = "[L * c + c_2 = 0 + -1 * (-1 * q_0 * L ^^^ 2 / 2), c_2 = 0]"
wneuper@424	168	then () else raise error "eqsystem.sml rewrite in 2x2 isolate_bdvs";
wneuper@422	169
wneuper@457	170	val Some(t,_)= rewrite_set_inst_ thy true bdvs simplify_System t;
wneuper@424	171	if term2str t = "[L * c + c_2 = q_0 * L ^^^ 2 / 2, c_2 = 0]"
wneuper@450	172	then () else raise error "eqsystem.sml rewrite in 2x2 simplify_System_par.2";
wneuper@416	173
wneuper@424	174	val Some (t,_) = rewrite_set_ thy true order_system t;
wneuper@424	175	if term2str t = "[c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]"
wneuper@457	176	then () else raise error "eqsystem.sml rewrite in 2x2 simplify_System_par.3";
wneuper@457	177
wneuper@457	178
wneuper@457	179	"----------- rewrite example from 2nd [EqSystem,normalize,2x2] ---";
wneuper@457	180	"----------- rewrite example from 2nd [EqSystem,normalize,2x2] ---";
wneuper@457	181	"----------- rewrite example from 2nd [EqSystem,normalize,2x2] ---";
wneuper@457	182	val thy = Isac.thy (because of Undeclared constant "Biegelinie.EI);
wneuper@457	183	val t =
wneuper@457	184	str2term"[0 = c_2 + c * 0 + 1 / EI * (L * q_0 / 12 * 0 ^^^ 3 + \
wneuper@457	185	\ -1 * q_0 / 24 * 0 ^^^ 4),\
wneuper@457	186	\ 0 = c_2 + c * L + 1 / EI * (L * q_0 / 12 * L ^^^ 3 + \
wneuper@457	187	\ -1 * q_0 / 24 * L ^^^ 4)]";
wneuper@457	188	val Some (t,_) = rewrite_set_ thy true norm_Rational t;
wneuper@660	189	if term2str t="[0 = c_2, 0 = c_2 + L * c + L ^^^ 4 * q_0 / (24 * EI)]"
wneuper@457	190	then () else raise error "eqsystem.sml rewrite in 2x2 simplify_System_par.0b";
wneuper@457	191
wneuper@457	192	val Some(t,_)= rewrite_set_inst_ thy true bdvs simplify_System_parenthesized t;
wneuper@457	193	if term2str t = "[0 = c_2, 0 = q_0 * L ^^^ 4 / (24 * EI) + (L * c + c_2)]"
wneuper@457	194	then () else raise error "eqsystem.sml rewrite in 2x2 simplify_System_par.1b";
wneuper@457	195
wneuper@457	196	val Some (t,_) = rewrite_set_inst_ thy true bdvs isolate_bdvs t;
wneuper@457	197	if term2str t = "[c_2 = 0, L * c + c_2 = 0 + -1 * (q_0 * L ^^^ 4 / (24 * EI))]"
wneuper@457	198	then () else raise error "eqsystem.sml rewrite in 2x2 isolate_bdvs b";
wneuper@457	199
wneuper@457	200	val Some(t,_)= rewrite_set_inst_ thy true bdvs simplify_System t;
wneuper@457	201	if term2str t = "[c_2 = 0, L * c + c_2 = -1 * q_0 * L ^^^ 4 / (24 * EI)]"
wneuper@457	202	then () else raise error "eqsystem.sml rewrite in 2x2 simplify_System.2b";
wneuper@457	203
wneuper@457	204	val xxx = rewrite_set_ thy true order_system t;
wneuper@457	205	if is_none xxx
wneuper@457	206	then () else raise error "eqsystem.sml rewrite in 2x2 simplify_System.3b";
wneuper@415	207
wneuper@414	208
wneuper@447	209	"----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
wneuper@447	210	"----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
wneuper@447	211	"----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
wneuper@447	212	val e1__ = str2term "c_2 = 77";
wneuper@447	213	val e2__ = str2term "L * c + c_2 = q_0 * L ^^^ 2 / 2";
wneuper@447	214	val bdvs = [(str2term"bdv_1",str2term"c"),
wneuper@447	215	(str2term"bdv_2",str2term"c_2")];
wneuper@447	216	val Some (e2__,_) = rewrite_terms_ thy dummy_ord Erls [e1__] e2__;
wneuper@447	217	if term2str e2__ = "L * c + 77 = q_0 * L ^^^ 2 / 2" then ()
wneuper@447	218	else raise error "eqsystem.sml top_down_substitution,2x2] subst";
wneuper@447	219
wneuper@454	220	val Some (e2__,_) =
wneuper@454	221	rewrite_set_inst_ thy true bdvs simplify_System_parenthesized e2__;
wneuper@447	222	if term2str e2__ = "77 + L * c = q_0 * L ^^^ 2 / 2" then ()
wneuper@447	223	else raise error "eqsystem.sml top_down_substitution,2x2] simpl_par";
wneuper@447	224
wneuper@447	225	val Some (e2__,_) = rewrite_set_inst_ thy true bdvs isolate_bdvs e2__;
wneuper@447	226	if term2str e2__ = "c = (q_0 * L ^^^ 2 / 2 + -1 * 77) / L" then ()
wneuper@447	227	else raise error "eqsystem.sml top_down_substitution,2x2] isolate";
wneuper@447	228
wneuper@447	229	val t = str2term "[c_2 = 77, c = (q_0 * L ^^^ 2 / 2 + -1 * 77) / L]";
wneuper@447	230	val Some (t,_) = rewrite_set_ thy true order_system t;
wneuper@447	231	if term2str t = "[c = (q_0 * L ^^^ 2 / 2 + -1 * 77) / L, c_2 = 77]" then ()
wneuper@447	232	else raise error "eqsystem.sml top_down_substitution,2x2] order_system";
wneuper@447	233
wneuper@450	234	if not (ord_simplify_System
wneuper@447	235	false thy []
wneuper@447	236	(str2term"[c_2 = 77, c = (q_0 * L ^^^ 2 / 2 + -1 * 77) / L]",
wneuper@447	237	str2term"[c = (q_0 * L ^^^ 2 / 2 + -1 * 77) / L, c_2 = 77]"))
wneuper@447	238	then () else raise error "eqsystem.sml, order_result rew_ord";
wneuper@447	239
wneuper@447	240	trace_rewrite:=true;
wneuper@447	241	trace_rewrite:=false;
wneuper@447	242
wneuper@447	243
wneuper@418	244	"----------- rewrite in [EqSystem,normalize,4x4] -----------------";
wneuper@418	245	"----------- rewrite in [EqSystem,normalize,4x4] -----------------";
wneuper@418	246	"----------- rewrite in [EqSystem,normalize,4x4] -----------------";
wneuper@663	247	(GOON??: revise rewrite in [EqSystem,normalize,4x4] from before 0609)
wneuper@418	248	val t = str2term"[0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c_3 + c_4,\
wneuper@418	249	\0 = -1 * q_0 * L ^^^ 2 / 2 + L * c_3 + c_4,\
wneuper@418	250	\c + c_2 + c_3 + c_4 = 0,\
wneuper@418	251	\c_2 + c_3 + c_4 = 0]";
wneuper@422	252	val bdvs = [(str2term"bdv_1",str2term"c"),
wneuper@422	253	(str2term"bdv_2",str2term"c_2"),
wneuper@422	254	(str2term"bdv_3",str2term"c_3"),
wneuper@422	255	(str2term"bdv_4",str2term"c_4")];
wneuper@454	256	val Some (t,_) =
wneuper@454	257	rewrite_set_inst_ thy true bdvs simplify_System_parenthesized t;
wneuper@454	258	if term2str t = "[0 = c_4, 0 = -1 * q_0 * L ^^^ 2 / 2 + (L * c_3 + c_4),\n\
wneuper@454	259	\ c + (c_2 + (c_3 + c_4)) = 0, c_2 + (c_3 + c_4) = 0]"
wneuper@450	260	then () else raise error "eqsystem.sml rewrite in 4x4 simplify_System_paren";
wneuper@418	261
wneuper@422	262	val Some (t,_) = rewrite_set_inst_ thy true bdvs isolate_bdvs t;
wneuper@454	263	if term2str t = "[c_4 = 0, \
wneuper@454	264	\L * c_3 + c_4 = 0 + -1 * (-1 * q_0 * L ^^^ 2 / 2),\n \
wneuper@454	265	\c + (c_2 + (c_3 + c_4)) = 0, c_2 + (c_3 + c_4) = 0]"
wneuper@422	266	then () else raise error "eqsystem.sml rewrite in 4x4 isolate_bdvs";
wneuper@422	267
wneuper@454	268	val Some(t,_)= rewrite_set_inst_ thy true bdvs simplify_System_parenthesized t;
wneuper@422	269	if term2str t = "[c_4 = 0,\
wneuper@422	270	\ L * c_3 + c_4 = q_0 * L ^^^ 2 / 2,\
wneuper@422	271	\ c + (c_2 + (c_3 + c_4)) = 0,\n\
wneuper@422	272	\ c_2 + (c_3 + c_4) = 0]"
wneuper@450	273	then () else raise error "eqsystem.sml rewrite in 4x4 simplify_System_p..2";
wneuper@422	274
wneuper@422	275	val Some (t,_) = rewrite_set_ thy true order_system t;
wneuper@424	276	if term2str t = "[c_4 = 0,\
wneuper@424	277	\ L * c_3 + c_4 = q_0 * L ^^^ 2 / 2,\
wneuper@424	278	\ c_2 + (c_3 + c_4) = 0,\n\
wneuper@424	279	\ c + (c_2 + (c_3 + c_4)) = 0]"
wneuper@424	280	then () else raise error "eqsystem.sml rewrite in 4x4 order_system";
wneuper@414	281
wneuper@447	282
wneuper@412	283	"----------- script [EqSystem,normalize,2x2] ---------------------";
wneuper@412	284	"----------- script [EqSystem,normalize,2x2] ---------------------";
wneuper@412	285	"----------- script [EqSystem,normalize,2x2] ---------------------";
wneuper@412	286	val str =
wneuper@445	287	"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
wneuper@454	288	\ (let es__ = (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
wneuper@454	289	\ simplify_System_parenthesized False) es_ \
wneuper@412	290	\ in ([]))";
wneuper@412	291	val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
wneuper@412	292	val str =
wneuper@445	293	"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
wneuper@454	294	\ (let es__ = (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
wneuper@454	295	\ simplify_System_parenthesized False) es_ \
wneuper@412	296	\ in (SubProblem (Biegelinie_,[linear,system],[no_met])\
wneuper@412	297	\ []))";
wneuper@412	298	val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
wneuper@412	299	val str =
wneuper@445	300	"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
wneuper@454	301	\ (let es__ = (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
wneuper@454	302	\ simplify_System_parenthesized False) es_ \
wneuper@412	303	\ in (SubProblem (Biegelinie_,[linear,system],[no_met])\
wneuper@412	304	\ [bool_list_ es__, real_list_ vs_]))"
wneuper@412	305	;
wneuper@412	306	val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
wneuper@416	307	val str =
wneuper@445	308	"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
wneuper@454	309	\ (let es__ = Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
wneuper@454	310	\ simplify_System_parenthesized False) es_ \
wneuper@416	311	\ in (SubProblem (Biegelinie_,[linear,system],[no_met])\
wneuper@416	312	\ [bool_list_ es__, real_list_ vs_]))"
wneuper@416	313	;
wneuper@416	314	val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
wneuper@416	315	val str =
wneuper@445	316	"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
wneuper@454	317	\ (let es__ = (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
wneuper@454	318	\ simplify_System_parenthesized False)) es_ \
wneuper@425	319	\ in (SubProblem (Biegelinie_,[linear,system],[no_met])\
wneuper@416	320	\ [bool_list_ es__, real_list_ vs_]))"
wneuper@416	321	;
wneuper@416	322	val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
wneuper@417	323	val str =
wneuper@445	324	"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
wneuper@454	325	\ (let es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
wneuper@454	326	\ simplify_System_parenthesized False)) @@\
wneuper@454	327	\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
wneuper@454	328	\ simplify_System_parenthesized False))) es_\
wneuper@425	329	\ in (SubProblem (Biegelinie_,[linear,system],[no_met])\
wneuper@417	330	\ [bool_list_ es__, real_list_ vs_]))"
wneuper@417	331	;
wneuper@417	332	val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
wneuper@417	333	val str =
wneuper@445	334	"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
wneuper@454	335	\ (let es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
wneuper@454	336	\ simplify_System_parenthesized False)) @@\
wneuper@454	337	\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
wneuper@454	338	\ simplify_System_parenthesized False)) @@\
wneuper@454	339	\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
wneuper@454	340	\ simplify_System_parenthesized False))) es_\
wneuper@425	341	\ in (SubProblem (Biegelinie_,[linear,system],[no_met])\
wneuper@417	342	\ [bool_list_ es__, real_list_ vs_]))"
wneuper@417	343	;
wneuper@417	344	val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
wneuper@425	345	val str =
wneuper@445	346	"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
wneuper@454	347	\ (let es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
wneuper@454	348	\ simplify_System_parenthesized False)) @@\
wneuper@425	349	\ (Try (Rewrite_Set_Inst [] isolate_bdvs False)) @@\
wneuper@454	350	\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
wneuper@454	351	\ simplify_System_parenthesized False)) @@\
wneuper@425	352	\ (Try (Rewrite_Set order_system False))) es_\
wneuper@425	353	\ in (SubProblem (Biegelinie_,[linear,system],[no_met])\
wneuper@425	354	\ [bool_list_ es__, real_list_ vs_]))"
wneuper@425	355	;
wneuper@425	356	val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
wneuper@425	357	val str =
wneuper@445	358	"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
wneuper@454	359	\ (let es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
wneuper@454	360	\ simplify_System_parenthesized False)) @@\
wneuper@425	361	\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_)]\
wneuper@425	362	\ isolate_bdvs False)) @@\
wneuper@454	363	\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
wneuper@454	364	\ simplify_System_parenthesized False)) @@\
wneuper@425	365	\ (Try (Rewrite_Set order_system False))) es_\
wneuper@425	366	\ in (SubProblem (Biegelinie_,[linear,system],[no_met])\
wneuper@425	367	\ [bool_list_ es__, real_list_ vs_]))"
wneuper@425	368	;
wneuper@425	369	val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
wneuper@425	370	val str =
wneuper@445	371	"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
wneuper@450	372	\ (let es__ = ((Try (Rewrite_Set simplify_System_parenthesized False)) @@\
wneuper@425	373	\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
wneuper@425	374	\ isolate_bdvs False)) @@\
wneuper@454	375	\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
wneuper@454	376	\ simplify_System_parenthesized False)) @@\
wneuper@425	377	\ (Try (Rewrite_Set order_system False))) es_\
wneuper@425	378	\ in (SubProblem (Biegelinie_,[linear,system],[no_met])\
wneuper@425	379	\ [bool_list_ es__, real_list_ vs_]))"
wneuper@425	380	;
wneuper@425	381	val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
wneuper@425	382	(---^^^-OK-----------------------------------------------------------------)
wneuper@425	383	(---vvv-NOT ok-------------------------------------------------------------)
wneuper@412	384
wneuper@412	385
wneuper@446	386	"----------- script [EqSystem,top_down_substitution,2x2] Vers.1 --";
wneuper@446	387	"----------- script [EqSystem,top_down_substitution,2x2] Vers.1 --";
wneuper@446	388	"----------- script [EqSystem,top_down_substitution,2x2] Vers.1 --";
wneuper@445	389	val str =
wneuper@445	390	"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
wneuper@454	391	\ (let es__ = (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
wneuper@454	392	\ simplify_System_parenthesized False) es_ \
wneuper@445	393	\ in ([]))";
wneuper@445	394	val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
wneuper@445	395	val str =
wneuper@445	396	"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
wneuper@445	397	\ (let e1__ = Take (hd es_) \
wneuper@445	398	\ in ([]))";
wneuper@445	399	val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
wneuper@445	400	val str =
wneuper@445	401	"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
wneuper@445	402	\ (let e1__ = Take (hd es_); \
wneuper@445	403	\ e1__ = Take (hd es_) \
wneuper@445	404	\ in ([]))";
wneuper@445	405	val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
wneuper@445	406	val str =
wneuper@445	407	"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
wneuper@445	408	\ (let e1__ = Take (hd es_); \
wneuper@445	409	\ e1__ = (Take (hd es_))\
wneuper@445	410	\ in ([]))";
wneuper@445	411	val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
wneuper@445	412	val str =
wneuper@445	413	"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
wneuper@445	414	\ (let e1__ = Take (hd es_); \
wneuper@445	415	\ e1__ = ((Rewrite_Set order_system False)) e1__\
wneuper@445	416	\ in ([]))";
wneuper@445	417	val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
wneuper@445	418	(--------------------------------------------------------------------------)
wneuper@445	419	val str =
wneuper@445	420	"(Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
wneuper@445	421	\ isolate_bdvs False) (e1__::bool)";
wneuper@445	422	val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
wneuper@445	423	(--------------------------------------------------------------------------)
wneuper@445	424	val str =
wneuper@445	425	"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
wneuper@445	426	\ (let e1__ = Take (hd es_); \
wneuper@445	427	\ e1__ = ((Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
wneuper@445	428	\ isolate_bdvs False)) e1__\
wneuper@445	429	\ in ([]))";
wneuper@445	430	val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
wneuper@445	431	val str =
wneuper@445	432	"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
wneuper@445	433	\ (let e1__ = Take (hd es_); \
wneuper@445	434	\ e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
wneuper@445	435	\ isolate_bdvs False)) @@\
wneuper@454	436	\ (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
wneuper@454	437	\ simplify_System False)) e1__\
wneuper@445	438	\ in ([]))";
wneuper@445	439	val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
wneuper@445	440	val str =
wneuper@445	441	"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
wneuper@445	442	\ (let e1__ = Take (hd es_); \
wneuper@445	443	\ e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
wneuper@445	444	\ isolate_bdvs False)) @@\
wneuper@454	445	\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
wneuper@454	446	\ simplify_System False))) e1__\
wneuper@445	447	\ in ([]))";
wneuper@445	448	val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
wneuper@445	449	val str =
wneuper@445	450	"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
wneuper@445	451	\ (let e1__ = Take (hd es_); \
wneuper@445	452	\ e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
wneuper@445	453	\ isolate_bdvs False)) @@ \
wneuper@454	454	\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
wneuper@454	455	\ simplify_System False))) e1__; \
wneuper@445	456	\ e2__ = Take (hd (tl es_)) \
wneuper@445	457	\ in ([]))";
wneuper@445	458	val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
wneuper@445	459	val str =
wneuper@445	460	"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
wneuper@445	461	\ (let e1__ = Take (hd es_); \
wneuper@445	462	\ e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
wneuper@445	463	\ isolate_bdvs False)) @@ \
wneuper@454	464	\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
wneuper@454	465	\ simplify_System False))) e1__; \
wneuper@445	466	\ e2__ = Take (hd (tl es_)); \
wneuper@445	467	\ e2__ = Substitute [e1__] e2__ \
wneuper@445	468	\ in ([]))";
wneuper@445	469	val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
wneuper@445	470	val str =
wneuper@445	471	"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
wneuper@445	472	\ (let e1__ = Take (hd es_); \
wneuper@445	473	\ e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
wneuper@445	474	\ isolate_bdvs False)) @@ \
wneuper@454	475	\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
wneuper@454	476	\ simplify_System False))) e1__; \
wneuper@445	477	\ e2__ = Take (hd (tl es_)); \
wneuper@445	478	\ e2__ = ((Substitute [e1__])) e2__ \
wneuper@445	479	\ in ([]))";
wneuper@445	480	val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
wneuper@445	481	val str =
wneuper@445	482	"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
wneuper@445	483	\ (let e1__ = Take (hd es_); \
wneuper@445	484	\ e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
wneuper@445	485	\ isolate_bdvs False)) @@ \
wneuper@454	486	\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
wneuper@454	487	\ simplify_System False))) e1__; \
wneuper@445	488	\ e2__ = Take (hd (tl es_)); \
wneuper@445	489	\ e2__ = ((Substitute [e1__]) @@ \
wneuper@445	490	\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
wneuper@445	491	\ isolate_bdvs False)) @@ \
wneuper@454	492	\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
wneuper@454	493	\ simplify_System False))) e2__ \
wneuper@445	494	\ in [e1__, e2__])"
wneuper@445	495	;
wneuper@445	496	val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
wneuper@447	497	val str =
wneuper@447	498	"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
wneuper@447	499	\ (let e1__ = Take (hd es_); \
wneuper@447	500	\ e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
wneuper@447	501	\ isolate_bdvs False)) @@ \
wneuper@454	502	\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
wneuper@454	503	\ simplify_System False))) e1__; \
wneuper@447	504	\ e2__ = Take (hd (tl es_)); \
wneuper@447	505	\ e2__ = ((Substitute [e1__]) @@ \
wneuper@454	506	\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
wneuper@454	507	\ simplify_System_parenthesized False)) @@ \
wneuper@447	508	\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
wneuper@447	509	\ isolate_bdvs False)) @@ \
wneuper@454	510	\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
wneuper@454	511	\ simplify_System False)) @@ \
wneuper@447	512	\ (Try (Rewrite_Set order_system False))) e2__ \
wneuper@447	513	\ in [e1__, e2__])"
wneuper@447	514	;
wneuper@447	515	val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
wneuper@447	516	(---^^^-OK-----------------------------------------------------------------)
wneuper@447	517	val str =
wneuper@447	518	"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
wneuper@447	519	\ (let e1__ = Take (hd es_); \
wneuper@447	520	\ e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
wneuper@447	521	\ isolate_bdvs False)) @@ \
wneuper@454	522	\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
wneuper@454	523	\ simplify_System False))) e1__; \
wneuper@447	524	\ e2__ = Take (hd (tl es_)); \
wneuper@447	525	\ e2__ = ((Substitute [e1__]) @@ \
wneuper@454	526	\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
wneuper@454	527	\ simplify_System_parenthesized False)) @@ \
wneuper@447	528	\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
wneuper@447	529	\ isolate_bdvs False)) @@ \
wneuper@454	530	\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
wneuper@454	531	\ simplify_System False))) e2__; \
wneuper@447	532	\ es__ = Take [e1__, e2__]\
wneuper@447	533	\ in (Try (Rewrite_Set order_system False)) es__)"
wneuper@447	534	;
wneuper@447	535	val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
wneuper@445	536	(---vvv-NOT ok-------------------------------------------------------------)
wneuper@445	537	atomty sc;
wneuper@403	538
wneuper@446	539	"----------- script [EqSystem,top_down_substitution,2x2] Vers.2 --";
wneuper@446	540	"----------- script [EqSystem,top_down_substitution,2x2] Vers.2 --";
wneuper@446	541	"----------- script [EqSystem,top_down_substitution,2x2] Vers.2 --";
wneuper@446	542	val str =
wneuper@446	543	"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
wneuper@446	544	\ (let es__ = Take es_; \
wneuper@446	545	\ e1__ = hd es__\
wneuper@446	546	\ in ([]))"
wneuper@446	547	;
wneuper@446	548	val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
wneuper@446	549	val str =
wneuper@446	550	"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
wneuper@446	551	\ (let es__ = Take es_; \
wneuper@446	552	\ e1__ = hd es__; \
wneuper@446	553	\ e2__ = hd (tl es__)\
wneuper@446	554	\ in ([]))"
wneuper@446	555	;
wneuper@446	556	val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
wneuper@446	557	val str =
wneuper@446	558	"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
wneuper@446	559	\ (let es__ = Take es_; \
wneuper@446	560	\ e1__ = hd es__; \
wneuper@446	561	\ e2__ = hd (tl es__);\
wneuper@446	562	\ es__ = [1=2,3=4]\
wneuper@446	563	\ in ([]))"
wneuper@446	564	;
wneuper@446	565	val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
wneuper@446	566	val str =
wneuper@446	567	"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
wneuper@446	568	\ (let es__ = Take es_; \
wneuper@446	569	\ e1__ = hd es__; \
wneuper@446	570	\ e2__ = hd (tl es__);\
wneuper@446	571	\ es__ = [e1__,e2__]\
wneuper@446	572	\ in ([]))"
wneuper@446	573	;
wneuper@446	574	val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
wneuper@446	575	val str =
wneuper@446	576	"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
wneuper@446	577	\ (let es__ = Take es_; \
wneuper@446	578	\ e1__ = hd es__; \
wneuper@446	579	\ e2__ = hd (tl es__);\
wneuper@446	580	\ es__ = [e1__, Substitute [e1__] e2__];\
wneuper@454	581	\ es__ = (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
wneuper@454	582	\ simplify_System False)) es__ \
wneuper@446	583	\ in ([]))"
wneuper@446	584	;
wneuper@446	585	val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
wneuper@446	586	val str =
wneuper@446	587	"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
wneuper@446	588	\ (let es__ = Take es_; \
wneuper@446	589	\ e1__ = hd es__; \
wneuper@446	590	\ e2__ = hd (tl es__);\
wneuper@446	591	\ es__ = [e1__, Substitute [e1__] e2__];\
wneuper@446	592	\ es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
wneuper@446	593	\ isolate_bdvs False)) @@ \
wneuper@454	594	\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
wneuper@454	595	\ simplify_System False))) es__ \
wneuper@446	596	\ in ([]))"
wneuper@446	597	;
wneuper@446	598	val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
wneuper@446	599	val str =
wneuper@446	600	"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
wneuper@446	601	\ (let es__ = Take es_; \
wneuper@446	602	\ e1__ = hd es__; \
wneuper@446	603	\ e2__ = hd (tl es__);\
wneuper@446	604	\ es__ = [e1__, Substitute [e1__] e2__];\
wneuper@454	605	\ es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
wneuper@454	606	\ simplify_System_parenthesized False)) @@ \
wneuper@446	607	\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
wneuper@446	608	\ isolate_bdvs False)) @@ \
wneuper@454	609	\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
wneuper@454	610	\ simplify_System False))) es__ \
wneuper@446	611	\ in ([]))"
wneuper@446	612	;
wneuper@446	613	val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
wneuper@446	614	val str =
wneuper@446	615	"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
wneuper@446	616	\ (let es__ = Take es_; \
wneuper@446	617	\ e1__ = hd es__; \
wneuper@446	618	\ e2__ = hd (tl es__); \
wneuper@446	619	\ es__ = [e1__, Substitute [e1__] e2__]; \
wneuper@454	620	\ es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
wneuper@454	621	\ simplify_System_parenthesized False)) @@ \
wneuper@446	622	\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
wneuper@446	623	\ isolate_bdvs False)) @@ \
wneuper@454	624	\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
wneuper@454	625	\ simplify_System False))) es__ \
wneuper@446	626	\ in es__)"
wneuper@446	627	;
wneuper@446	628	val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
wneuper@446	629	val str =
wneuper@446	630	"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
wneuper@446	631	\ (let es__ = Take es_; \
wneuper@446	632	\ e1__ = hd es__; \
wneuper@446	633	\ e2__ = hd (tl es__); \
wneuper@446	634	\ es__ = [e1__, Substitute [e1__] e2__] \
wneuper@454	635	\ in ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
wneuper@454	636	\ simplify_System_parenthesized False)) @@ \
wneuper@446	637	\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))] \
wneuper@446	638	\ isolate_bdvs False)) @@ \
wneuper@454	639	\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
wneuper@454	640	\ simplify_System False))) es__)"
wneuper@446	641	;
wneuper@446	642	val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
wneuper@446	643	(---^^^-OK-----------------------------------------------------------------)
wneuper@447	644	val str =
wneuper@447	645	"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
wneuper@447	646	\ (let es__ = Take es_; \
wneuper@447	647	\ e1__ = hd es__; \
wneuper@447	648	\ e2__ = hd (tl es__); \
wneuper@447	649	\ es__ = [e1__, Substitute [e1__] e2__] "^
wneuper@447	650	(* this ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ is a script-'Expr'
wneuper@447	651	which is not yet searched for 'STac's; thus this script does not yet work*)
wneuper@454	652	" in ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
wneuper@454	653	\ simplify_System_parenthesized False)) @@ \
wneuper@447	654	\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))] \
wneuper@447	655	\ isolate_bdvs False)) @@ \
wneuper@454	656	\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
wneuper@454	657	\ simplify_System False))) es__)"
wneuper@447	658	;
wneuper@447	659	val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
wneuper@446	660	(---vvv-NOT ok-------------------------------------------------------------)
wneuper@446	661	atomty sc;
wneuper@446	662
wneuper@403	663
wneuper@430	664	"----------- refine [linear,system]-------------------------------";
wneuper@430	665	"----------- refine [linear,system]-------------------------------";
wneuper@430	666	"----------- refine [linear,system]-------------------------------";
wneuper@430	667	val fmz = ["equalities [0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2,\
wneuper@430	668	\0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2]",
wneuper@430	669	"solveForVars [c, c_2]", "solution L"];
wneuper@430	670	val matches = refine fmz ["linear","system"];
wneuper@430	671	case matches of [_,_,_,
wneuper@430	672	Matches (["normalize", "2x2", "linear", "system"],
wneuper@430	673	{Find = [Correct "solution L"],
wneuper@430	674	With = [],
wneuper@430	675	Given =
wneuper@430	676	[Correct
wneuper@430	677	"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]",
wneuper@430	678	Correct "solveForVars [c, c_2]"],
wneuper@430	679	Where = [],
wneuper@430	680	Relate = []})] => ()
wneuper@430	681	\| _ => raise error "eqsystem.sml refine ['normalize','2x2'...]";
wneuper@430	682
wneuper@430	683
wneuper@430	684	val fmz = ["equalities [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]",
wneuper@430	685	"solveForVars [c, c_2]", "solution L"];
wneuper@430	686	val matches = refine fmz ["linear","system"];
wneuper@430	687	case matches of [_,_,
wneuper@430	688	Matches
wneuper@430	689	(["triangular", "2x2", "linear", "system"],
wneuper@430	690	{Find = [Correct "solution L"],
wneuper@430	691	With = [],
wneuper@430	692	Given =
wneuper@430	693	[Correct
wneuper@430	694	"equalities [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]",
wneuper@430	695	Correct "solveForVars [c, c_2]"],
wneuper@430	696	Where =
wneuper@430	697	[Correct
wneuper@430	698	"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]",
wneuper@430	699	Correct
wneuper@430	700	"[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]"],
wneuper@430	701	Relate = []})] => ()
wneuper@430	702	\| _ => raise error "eqsystem.sml refine ['triangular','2x2'...]";
wneuper@445	703
wneuper@438	704
wneuper@438	705	(*WN051014----------------------------------------------------------------
wneuper@438	706	the above 'val matches = refine fmz ["linear","system"]'
wneuper@438	707	didn't work anymore; we investigated in these steps:*)
wneuper@438	708	val fmz = ["equalities [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]",
wneuper@438	709	"solveForVars [c, c_2]", "solution L"];
wneuper@438	710	val matches = refine fmz ["triangular", "2x2", "linear","system"];
wneuper@438	711	(*... resulted in
wneuper@438	712	False "[c, c_2] from_ [c, c_2] occur_exactly_in nth_ 2\n
wneuper@438	713	[c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]"]*)
wneuper@438	714
wneuper@438	715	val t = str2term"[c, c_2] from_ [c, c_2] occur_exactly_in nth_ 2\
wneuper@438	716	\[c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]";
wneuper@438	717	trace_rewrite:=true;
wneuper@438	718	val Some (t',_) = rewrite_set_ thy false prls_triangular t;
wneuper@438	719	(*found:...
wneuper@438	720	## try thm: nth_Cons_
wneuper@438	721	### eval asms: 1 < 2 + - 1
wneuper@438	722	==> nth_ (2 + - 1) [L * c + c_2 = q_0 * L ^^^ 2 / 2] =
wneuper@438	723	nth_ (2 + - 1 + - 1) []
wneuper@438	724	#### rls: erls_prls_triangular on: 1 < 2 + - 1
wneuper@438	725	##### try calc: op <'
wneuper@438	726	### asms accepted: ["1 < 2 + - 1"] stored: ["1 < 2 + -1"]
wneuper@438	727
wneuper@438	728	... i.e Calc ("op +", eval_binop "#add_") was missing in erls_prls_triangular*)
wneuper@438	729	trace_rewrite:=false;
wneuper@438	730	(WN051014------------------------------------------------------------------)
wneuper@445	731
wneuper@661	732	"----- relaxed preconditions for triangular system";
wneuper@661	733	val fmz = ["equalities [L * q_0 = c, \
wneuper@661	734	\ 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2,\
wneuper@663	735	\ 0 = c_4, \
wneuper@663	736	\ 0 = c_3]",
wneuper@661	737	"solveForVars [c, c_2, c_3, c_4]", "solution L"];
wneuper@661	738	val matches = refine fmz ["linear","system"];
wneuper@663	739	(* trace_rewrite := true;
wneuper@663	740	trace_rewrite := false;
wneuper@663	741	*)
wneuper@663	742	(print_depth 6; matches; print_depth 3;)
wneuper@663	743	case matches of
wneuper@663	744	[Matches (["linear", "system"], _),
wneuper@663	745	NoMatch (["2x2", "linear", "system"], _),
wneuper@663	746	NoMatch (["3x3", "linear", "system"], _),
wneuper@663	747	Matches (["4x4", "linear", "system"], _),
wneuper@663	748	NoMatch (["triangular", "4x4", "linear", "system"], _),
wneuper@663	749	Matches (["normalize", "4x4", "linear", "system"], _)] => ()
wneuper@663	750	\| _ => raise error "eqsystem.sml: refine relaxed triangular sys NoMatch";
wneuper@663	751	(WN060914 does NOT match, because 3rd and 4th equ are not ordered)
wneuper@661	752
wneuper@663	753	val fmz = ["equalities [L * q_0 = c, \
wneuper@663	754	\ 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2,\
wneuper@663	755	\ 0 = c_3, \
wneuper@663	756	\ 0 = c_4]",
wneuper@663	757	"solveForVars [c, c_2, c_3, c_4]", "solution L"];
wneuper@663	758	val matches = refine fmz ["triangular", "4x4", "linear","system"];
wneuper@663	759	(* print_depth 11; matches; print_depth 3;
wneuper@663	760	*)
wneuper@663	761	case matches of
wneuper@663	762	[Matches (["triangular", "4x4", "linear", "system"], _)] => ()
wneuper@663	763	\| _ => raise error "eqsystem.sml: refine relaxed triangular sys Matches";
wneuper@663	764	val matches = refine fmz ["linear","system"];
wneuper@661	765
wneuper@445	766
wneuper@445	767	"----------- refine [2x2,linear,system] search error--------------";
wneuper@445	768	"----------- refine [2x2,linear,system] search error--------------";
wneuper@445	769	"----------- refine [2x2,linear,system] search error--------------";
wneuper@445	770	(*didn't go into ["2x2", "linear", "system"];
wneuper@445	771	we investigated in these steps:*)
wneuper@445	772	val fmz = ["equalities [0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2,\
wneuper@445	773	\0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2]",
wneuper@445	774	"solveForVars [c, c_2]", "solution L"];
wneuper@445	775	trace_rewrite:=true;
wneuper@445	776	val matches = refine fmz ["2x2", "linear","system"];
wneuper@445	777	trace_rewrite:=false;
wneuper@445	778	print_depth 11; matches; print_depth 3;
wneuper@445	779	(brought: 'False "length_ es_ = 2"')
wneuper@445	780
wneuper@445	781	(*-----fun refin' (pblRD:pblRD) fmz pbls ((Ptyp (pI,[py],[])):pbt ptyp) =
wneuper@445	782	(* val ((pblRD:pblRD), fmz, pbls, ((Ptyp (pI,[py],[])):pbt ptyp)) =
wneuper@445	783	(rev ["linear","system"], fmz, [(match list)],
wneuper@445	784	((Ptyp ("2x2",[get_pbt ["2x2","linear","system"]],[])):pbt ptyp));
wneuper@445	785	*)
wneuper@445	786	> show_types:=true; term2str (hd where_); show_types:=false;
wneuper@445	787	val it = "length_ (es_::real list) = (2::real)" : string
wneuper@445	788
wneuper@445	789	=========================================================================\
wneuper@445	790	-------fun prep_pbt
wneuper@445	791	(* val (thy, (pblID, dsc_dats: (string * (string list)) list,
wneuper@445	792	ev:rls, ca: string option, metIDs:metID list)) =
wneuper@445	793	(EqSystem.thy, (["system"],
wneuper@445	794	[("#Given" ,["equalities es_", "solveForVars vs_"]),
wneuper@445	795	("#Find" ,["solution ss___"](___ is copy-named))
wneuper@445	796	],
wneuper@445	797	append_rls "e_rls" e_rls [(for preds in where_)],
wneuper@445	798	Some "solveSystem es_ vs_",
wneuper@445	799	[]));
wneuper@445	800	*)
wneuper@445	801	> val [("#Given", [equalities_es_, "solveForVars vs_"])] = gi;
wneuper@445	802	val equalities_es_ = "equalities es_" : string
wneuper@445	803	> val (dd, ii) = (split_did o term_of o the o (parse thy)) equalities_es_;
wneuper@445	804	> show_types:=true; term2str ii; show_types:=false;
wneuper@445	805	val it = "es_::bool list" : string
wneuper@445	806	~~~~~~~~~~~~~~~^^^^^^^^^ OK~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
wneuper@445	807
wneuper@445	808	> val {where_,...} = get_pbt ["2x2", "linear","system"];
wneuper@445	809	> show_types:=true; term2str (hd where_); show_types:=false;
wneuper@445	810
wneuper@445	811	=========================================================================/
wneuper@445	812
wneuper@445	813
wneuper@445	814
wneuper@445	815	-----fun refin' ff:
wneuper@445	816	> (writeln o (itms2str Isac.thy)) itms;
wneuper@445	817	[
wneuper@445	818	(1 ,[1] ,true ,#Given ,Cor equalities
wneuper@445	819	[0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2,
wneuper@445	820	0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2] ,(es_, [[0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2,
wneuper@445	821	0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2]])),
wneuper@445	822	(2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(vs_, [[c, c_2]])),
wneuper@445	823	(3 ,[1] ,true ,#Find ,Cor solution L ,(ss___, [L]))]
wneuper@445	824
wneuper@445	825	> (writeln o pres2str) pre';
wneuper@445	826	[
wneuper@445	827	(false, length_ es_ = 2),
wneuper@445	828	(true, length_ [c, c_2] = 2)]
wneuper@445	829
wneuper@445	830	----- fun match_oris':
wneuper@445	831	> (writeln o (itms2str Isac.thy)) itms;
wneuper@445	832	> (writeln o pres2str) pre';
wneuper@445	833	..as in refin'
wneuper@445	834
wneuper@445	835	----- fun check_preconds'
wneuper@445	836	> (writeln o env2str) env;
wneuper@445	837	["
wneuper@445	838	(es_, [0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2,
wneuper@445	839	0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2])","
wneuper@445	840	(vs_, [c, c_2])","
wneuper@445	841	(ss___, L)"]
wneuper@445	842
wneuper@445	843	> val es_ = (fst o hd) env;
wneuper@445	844	val es_ = Free ("es_", "bool List.list") : Term.term
wneuper@445	845
wneuper@445	846	> val pre1 = hd pres;
wneuper@445	847	atomty pre1;
wneuper@445	848	***
wneuper@445	849	*** Const (op =, [real, real] => bool)
wneuper@445	850	*** . Const (ListG.length_, real list => real)
wneuper@445	851	*** . . Free (es_, real list)
wneuper@445	852	~~~~~~~~~~~~~~~~~~~^^^^^^^^^ should be bool list~~~~~~~~~~~~~~~~~~~
wneuper@445	853	*** . Free (2, real)
wneuper@445	854	***
wneuper@445	855
wneuper@445	856	THE REASON WAS A non-type-constrained variable IN #WHERE OF PROBLEM
wneuper@445	857	~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
wneuper@445	858	*)
wneuper@445	859
wneuper@445	860
wneuper@445	861	"----------- me [EqSystem,normalize,2x2] -------------------------";
wneuper@445	862	"----------- me [EqSystem,normalize,2x2] -------------------------";
wneuper@445	863	"----------- me [EqSystem,normalize,2x2] -------------------------";
wneuper@445	864	val fmz = ["equalities [0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2,\
wneuper@445	865	\0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2]",
wneuper@445	866	"solveForVars [c, c_2]", "solution L"];
wneuper@445	867	val (dI',pI',mI') =
wneuper@453	868	("Biegelinie.thy",["normalize", "2x2", "linear", "system"],
wneuper@453	869	["EqSystem","normalize","2x2"]);
wneuper@445	870	val p = e_pos'; val c = [];
wneuper@445	871	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
wneuper@445	872	val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
wneuper@445	873	val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
wneuper@445	874	val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
wneuper@445	875	val (p,_,f,nxt,_,pt) = me nxt p c pt;
wneuper@445	876	case nxt of ("Specify_Method",_) => ()
wneuper@445	877	\| _ => raise error "eqsystem.sml [EqSystem,normalize,2x2] specify";
wneuper@445	878
wneuper@445	879	val (p,_,f,nxt,_,pt) = me nxt p c pt;
wneuper@445	880	val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
wneuper@445	881	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);
wneuper@445	882	val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
wneuper@445	883	val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
wneuper@457	884	val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
wneuper@445	885	case nxt of
wneuper@445	886	(_, Subproblem ("Biegelinie.thy", ["triangular", "2x2", "linear",_])) => ()
wneuper@445	887	\| _ => raise error "eqsystem.sml me [EqSystem,normalize,2x2] SubProblem";
wneuper@445	888
wneuper@445	889	val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
wneuper@445	890	val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
wneuper@445	891	val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
wneuper@445	892	val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
wneuper@445	893	case nxt of
wneuper@445	894	(_, Specify_Method ["EqSystem", "top_down_substitution", "2x2"]) => ()
wneuper@445	895	\| _ => raise error "eqsystem.sml me [EqSys...2x2] top_down_substitution";
wneuper@445	896
wneuper@445	897	val (p,_,f,nxt,_,pt) = me nxt p c pt;
wneuper@457	898	val PblObj {probl,...} = get_obj I pt [5];(writeln o(itms2str Isac.thy)) probl;
wneuper@445	899	(*[
wneuper@445	900	(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]])),
wneuper@445	901	(2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(vs_, [[c, c_2]])),
wneuper@445	902	(3 ,[1] ,true ,#Find ,Cor solution ss___ ,(ss___, [ss___]))]
wneuper@445	903	*)
wneuper@445	904	val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
wneuper@445	905	val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
wneuper@447	906	val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
wneuper@447	907	val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
wneuper@447	908	val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
wneuper@447	909	val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
wneuper@447	910	val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
wneuper@447	911	val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
wneuper@447	912	case nxt of
wneuper@447	913	(_, Check_Postcond ["triangular", "2x2", "linear", "system"]) => ()
wneuper@447	914	\| _ => raise error "eqsystem.sml me Subpbl .[EqSys...2x2] finished";
wneuper@447	915	val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
wneuper@447	916	val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
wneuper@447	917	if f2str f = "[c = L * q_0 / 2, c_2 = 0]" then ()
wneuper@447	918	else raise error "eqsystem.sml me [EqSys...2x2] finished f2str f";
wneuper@447	919	case nxt of
wneuper@447	920	(_, End_Proof') => ()
wneuper@447	921	\| _ => raise error "eqsystem.sml me [EqSys...2x2] finished End_Proof'";
wneuper@445	922
wneuper@445	923
wneuper@453	924	"----------- me [linear,system] ..normalize..top_down_sub..-------";
wneuper@453	925	"----------- me [linear,system] ..normalize..top_down_sub..-------";
wneuper@453	926	"----------- me [linear,system] ..normalize..top_down_sub..-------";
wneuper@453	927	val fmz =
wneuper@453	928	["equalities\
wneuper@453	929	\[0 = c_2 + c * 0 + 1 / EI * (L * q_0 / 12 * 0 ^^^ 3 + \
wneuper@453	930	\ -1 * q_0 / 24 * 0 ^^^ 4),\
wneuper@453	931	\ 0 = c_2 + c * L + 1 / EI * (L * q_0 / 12 * L ^^^ 3 + \
wneuper@453	932	\ -1 * q_0 / 24 * L ^^^ 4)]",
wneuper@453	933	"solveForVars [c, c_2]", "solution L"];
wneuper@453	934	val (dI',pI',mI') =
wneuper@453	935	("Biegelinie.thy",["linear", "system"], ["no_met"]);
wneuper@453	936	val p = e_pos'; val c = [];
wneuper@453	937	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
wneuper@453	938	val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
wneuper@453	939	val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
wneuper@453	940	val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
wneuper@453	941	val (p,_,f,nxt,_,pt) = me nxt p c pt;
wneuper@457	942	case nxt of (_,Specify_Method ["EqSystem", "normalize", "2x2"]) => ()
wneuper@457	943	\| _ => raise error "eqsystem.sml [linear,system] specify b";
wneuper@453	944	val (p,_,f,nxt,_,pt) = me nxt p c pt;
wneuper@453	945	val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
wneuper@453	946	val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
wneuper@453	947	val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
wneuper@453	948	val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
wneuper@457	949	val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
wneuper@453	950	if f2str f =
wneuper@457	951	"[c_2 = 0, L * c + c_2 = -1 * q_0 * L ^^^ 4 / (24 * EI)]"
wneuper@457	952	then () else raise error "eqsystem.sml me simpl. before SubProblem b";
wneuper@453	953	case nxt of
wneuper@453	954	(_, Subproblem ("Biegelinie.thy", ["triangular", "2x2", "linear",_])) => ()
wneuper@457	955	\| _ => raise error "eqsystem.sml me [linear,system] SubProblem b";
wneuper@453	956
wneuper@453	957	val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
wneuper@453	958	val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
wneuper@453	959	val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
wneuper@453	960	val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
wneuper@453	961	case nxt of
wneuper@453	962	(_, Specify_Method ["EqSystem", "top_down_substitution", "2x2"]) => ()
wneuper@457	963	\| _ => raise error "eqsystem.sml me [EqSys...2x2] top_down_substitution b";
wneuper@453	964
wneuper@453	965	val (p,_,f,nxt,_,pt) = me nxt p c pt;
wneuper@457	966	val PblObj {probl,...} = get_obj I pt [5];(writeln o(itms2str Isac.thy)) probl;
wneuper@453	967	(*[
wneuper@453	968	(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]])),
wneuper@453	969	(2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(vs_, [[c, c_2]])),
wneuper@453	970	(3 ,[1] ,true ,#Find ,Cor solution ss___ ,(ss___, [ss___]))]
wneuper@453	971	*)
wneuper@453	972	val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
wneuper@453	973	val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
wneuper@453	974	val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
wneuper@453	975	val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
wneuper@453	976	val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
wneuper@453	977	val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
wneuper@453	978	val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
wneuper@453	979	val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
wneuper@453	980	case nxt of
wneuper@453	981	(_, Check_Postcond ["triangular", "2x2", "linear", "system"]) => ()
wneuper@457	982	\| _ => raise error "eqsystem.sml me Subpbl .[EqSys...2x2] finished b";
wneuper@453	983	val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
wneuper@453	984	val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
wneuper@456	985	if f2str f =
wneuper@457	986	"[c = -1 * q_0 * L ^^^ 4 / (24 * EI * L), c_2 = 0]"
wneuper@457	987	then () else raise error "eqsystem.sml me [EqSys...2x2] finished f2str f b";
wneuper@453	988	case nxt of
wneuper@453	989	(_, End_Proof') => ()
wneuper@457	990	\| _ => raise error "eqsystem.sml me [EqSys...2x2] finished End_Proof'" b;
wneuper@453	991
wneuper@453	992
wneuper@657	993	"----------- all systems from Biegelinie -------------------------";
wneuper@657	994	"----------- all systems from Biegelinie -------------------------";
wneuper@657	995	"----------- all systems from Biegelinie -------------------------";
wneuper@659	996	val subst = [(str2term "bdv_1", str2term "c"),
wneuper@659	997	(str2term "bdv_2", str2term "c_2"),
wneuper@659	998	(str2term "bdv_3", str2term "c_3"),
wneuper@659	999	(str2term "bdv_4", str2term "c_4")];
wneuper@660	1000	"------- Bsp 7.27";
wneuper@657	1001	states:=[];
wneuper@657	1002	CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
wneuper@657	1003	"Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]",
wneuper@657	1004	"FunktionsVariable x"],
wneuper@657	1005	("Biegelinie.thy", ["Biegelinien"],
wneuper@657	1006	["IntegrierenUndKonstanteBestimmen2"]))];
wneuper@657	1007	moveActiveRoot 1;
wneuper@657	1008	(*
wneuper@658	1009	trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;
wneuper@660	1010	##7.27## ordered substs
wneuper@660	1011	c_4 c_2
wneuper@660	1012	c c_2 c_3 c_4 c c_2 1->2: c
wneuper@660	1013	c_2 c_4
wneuper@660	1014	c c_2 c c_2 c_3 c_4 [2':c, 1:c_2, 3:c_4] -> 4:c_3*)
wneuper@659	1015	val t = str2term"[0 = c_4, \
wneuper@658	1016	\ 0 = c_4 + L * c_3 +(12 * L ^^^ 2 * c_2 + 4 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) / (-24 * EI), \
wneuper@658	1017	\ 0 = c_2, \
wneuper@658	1018	\ 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2]";
wneuper@659	1019	val Some (t',_) = rewrite_set_ thy false isolate_bdvs_4x4 t;
wneuper@659	1020	term2str t';
wneuper@659	1021	"[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]";
wneuper@659	1022
wneuper@659	1023
wneuper@664	1024	"----- 7.27 go through the rewrites in met_eqsys_norm_4x4";
wneuper@659	1025	val t = str2term "0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2";
wneuper@659	1026	val None = rewrite_set_ thy false norm_Rational t;
wneuper@659	1027	val Some (t,_) =
wneuper@659	1028	rewrite_set_inst_ thy false subst simplify_System_parenthesized t;
wneuper@660	1029	term2str t = "0 = -1 * q_0 * L ^^^ 2 / 2 + (L * c + c_2)";
wneuper@660	1030	"--- isolate_bdvs_4x4";
wneuper@661	1031	(*
wneuper@659	1032	val Some (t,_) = rewrite_set_inst_ thy false subst isolate_bdvs_4x4 t;
wneuper@659	1033	term2str t;
wneuper@659	1034	val Some (t,_) = rewrite_set_inst_ thy false subst simplify_System t;
wneuper@659	1035	term2str t;
wneuper@659	1036	val Some (t,_) = rewrite_set_ thy false order_system t;
wneuper@659	1037	term2str t;
wneuper@659	1038	*)
wneuper@658	1039
wneuper@660	1040	"------- Bsp 7.28 ---------------vvvvvvvvvvvvv Momentenlinie postponed";
wneuper@658	1041	states:=[];
wneuper@658	1042	CalcTree [(["Traegerlaenge L","Momentenlinie (-q_0 / L * x^3 / 6)",
wneuper@658	1043	"Biegelinie y",
wneuper@658	1044	"Randbedingungen [y L = 0, y' L = 0]",
wneuper@658	1045	"FunktionsVariable x"],
wneuper@658	1046	("Biegelinie.thy", ["vonMomentenlinieZu","Biegelinien"],
wneuper@658	1047	["Biegelinien", "AusMomentenlinie"]))];
wneuper@658	1048	moveActiveRoot 1;
wneuper@658	1049	(*
wneuper@658	1050	trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;
wneuper@657	1051	*)
wneuper@657	1052
wneuper@660	1053	"------- Bsp 7.69";
wneuper@658	1054	states:=[];
wneuper@658	1055	CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
wneuper@658	1056	"Randbedingungen [y 0 = 0, y L = 0, y' 0 = 0, y' L = 0]",
wneuper@658	1057	"FunktionsVariable x"],
wneuper@658	1058	("Biegelinie.thy", ["Biegelinien"],
wneuper@658	1059	["IntegrierenUndKonstanteBestimmen2"] ))];
wneuper@658	1060	moveActiveRoot 1;
wneuper@658	1061	(*
wneuper@658	1062	trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;
wneuper@660	1063	##7.69## ordered subst 2x2
wneuper@660	1064	c_4 c_3
wneuper@660	1065	c c_2 c_3 c_4 c c_2 c_3 1:c_3 -> 2:c c_2 2: c c_2
wneuper@660	1066	c_3 c_4
wneuper@660	1067	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*)
wneuper@660	1068	val t = str2term"[0 = c_4 + 0 / (-1 * EI), \
wneuper@658	1069	\ 0 = c_4 + L * c_3 + (12 * L ^^^ 2 * c_2 + 4 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) / (-24 * EI), \
wneuper@658	1070	\ 0 = c_3 + 0 / (-1 * EI), \
wneuper@658	1071	\ 0 = c_3 + (6 * L * c_2 + 3 * L ^^^ 2 * c + -1 * L ^^^ 3 * q_0) / (-6 * EI)]";
wneuper@657	1072
wneuper@660	1073	"------- Bsp 7.70";
wneuper@658	1074	states:=[];
wneuper@658	1075	CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
wneuper@658	1076	"Randbedingungen [Q 0 = q_0 * L, M_b L = 0, y 0 = 0, y' 0 = 0]",
wneuper@658	1077	"FunktionsVariable x"],
wneuper@658	1078	("Biegelinie.thy", ["Biegelinien"],
wneuper@658	1079	["IntegrierenUndKonstanteBestimmen2"] ))];
wneuper@658	1080	moveActiveRoot 1;
wneuper@658	1081	(*
wneuper@658	1082	trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;
wneuper@660	1083	##7.70## \|subst
wneuper@660	1084	c \|
wneuper@660	1085	c c_2 \|1:c -> 2:c_2
wneuper@660	1086	c_3 \|
wneuper@663	1087	c_4 \| GOON test methods @@@@@@@@@@@@@@@@@@@@@@@@@@@*)
wneuper@660	1088
wneuper@664	1089	"----- 7.70 go through the rewrites in met_eqsys_norm_4x4";
wneuper@660	1090	val t = str2term"[L * q_0 = c, \
wneuper@664	1091	\ 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2,\
wneuper@664	1092	\ 0 = c_4, \
wneuper@664	1093	\ 0 = c_3]";
wneuper@660	1094	val Some (t,_) =
wneuper@660	1095	rewrite_ thy e_rew_ord e_rls false (num_str commute_0_equality) t;
wneuper@660	1096	val Some (t,_) =
wneuper@660	1097	rewrite_ thy e_rew_ord e_rls false (num_str commute_0_equality) t;
wneuper@660	1098	val Some (t,_) =
wneuper@660	1099	rewrite_ thy e_rew_ord e_rls false (num_str commute_0_equality) t;
wneuper@664	1100	term2str t =
wneuper@664	1101	"[L * q_0 = c, (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2 = 0, c_4 = 0,\n c_3 = 0]";
wneuper@660	1102	val Some (t,_) =
wneuper@660	1103	rewrite_set_inst_ thy false subst simplify_System_parenthesized t;
wneuper@664	1104	term2str t =
wneuper@664	1105	"[L * q_0 = c, -1 * q_0 * L ^^^ 2 / 2 + (L * c + c_2) = 0, c_4 = 0, c_3 = 0]";
wneuper@660	1106	val Some (t,_) = rewrite_set_inst_ thy false subst isolate_bdvs_4x4 t;
wneuper@664	1107	term2str t =
wneuper@664	1108	"[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]";
wneuper@664	1109	val Some (t,_) =
wneuper@664	1110	rewrite_set_inst_ thy false subst simplify_System_parenthesized t;
wneuper@664	1111	term2str t ="[c = L * q_0, L * c + c_2 = q_0 * L ^^^ 2 / 2, c_4 = 0, c_3 = 0]";
wneuper@664	1112	val Some (t,_) = rewrite_set_ thy false order_system t;
wneuper@664	1113	if term2str t ="[c = L * q_0, L * c + c_2 = q_0 * L ^^^ 2 / 2, c_3 = 0, c_4 = 0]" then ()
wneuper@664	1114	else raise error "eqsystem.sml: exp 7.70 normalize 4x4 by rewrite changed";
wneuper@660	1115
wneuper@660	1116
wneuper@664	1117	"----- 7.70 with met normalize: ";
wneuper@663	1118	val fmz = ["equalities \
wneuper@664	1119	\[L * q_0 = c, \
wneuper@664	1120	\ 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2,\
wneuper@664	1121	\ 0 = c_4, \
wneuper@664	1122	\ 0 = c_3]",
wneuper@663	1123	"solveForVars [c, c_2, c_3, c_4]", "solution L"];
wneuper@663	1124	val (dI',pI',mI') =
wneuper@663	1125	("Biegelinie.thy",["linear", "system"],["no_met"]);
wneuper@663	1126	val p = e_pos'; val c = [];
wneuper@663	1127	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
wneuper@664	1128	val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
wneuper@664	1129	val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
wneuper@664	1130	val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
wneuper@664	1131	val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
wneuper@664	1132	case nxt of (_,Apply_Method ["EqSystem", "normalize", "4x4"]) => ()
wneuper@664	1133	\| _ => raise error "eqsystem.sml [EqSystem,normalize,4x4] specify";
wneuper@664	1134	val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
wneuper@664	1135	val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
wneuper@664	1136	val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
wneuper@664	1137	val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
wneuper@664	1138
wneuper@664	1139	val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
wneuper@664	1140	val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
wneuper@664	1141	val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
wneuper@664	1142	val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
wneuper@664	1143	if f2str f ="[c = L * q_0, L * c + c_2 = q_0 * L ^^^ 2 / 2, c_3 = 0, c_4 = 0]"
wneuper@664	1144	then () else raise error "eqsystem.sml: exp 7.70 normalize 4x4 by met changed";
wneuper@664	1145
wneuper@664	1146	"----- 7.70 with met top_down_: ";
wneuper@665	1147	"--- scr [EqSystem,top_down_substitution,4x4] -- a saved trial";
wneuper@665	1148	(---vvv-this script failed with if ?!?-------------------------------------)
wneuper@665	1149	val str =
wneuper@665	1150	"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
wneuper@665	1151	\ (let e1_ = hd es_; \
wneuper@665	1152	\ v1_ = hd vs_; \
wneuper@665	1153	\ xxx = if lhs e1_ =!= v1_ \
wneuper@665	1154	\ then 0=0 \
wneuper@665	1155	\ else let e1_ = Take e1_; \
wneuper@665	1156	\ e1_ = (Rewrite_Set_Inst [(bdv_1, hd vs_), \
wneuper@665	1157	\ (bdv_2, hd (tl vs_))] \
wneuper@665	1158	\ isolate_bdvs False) e1_; \
wneuper@665	1159	\ e2_ = Take (hd (tl es_)); \
wneuper@665	1160	\ e2_ = (Substitute [e1__]) e2_ \
wneuper@665	1161	\ in [e1_, e2_])";
wneuper@665	1162	(val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;)
wneuper@665	1163	val str =
wneuper@665	1164	"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
wneuper@665	1165	\ (let e1_ = hd es_; \
wneuper@665	1166	\ v1_ = hd vs_; \
wneuper@665	1167	\ e2_ = Take (hd (tl es_)); \
wneuper@665	1168	\ e2_ = (Substitute [e1__]) e2_ \
wneuper@665	1169	\ in [e1_, e2_])";
wneuper@665	1170	val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
wneuper@665	1171	(---^^^-OK-----------------------------------------------------------------)
wneuper@665	1172	(---vvv-NOT ok-------------------------------------------------------------)
wneuper@665	1173	val str =
wneuper@665	1174	"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
wneuper@665	1175	\ (let e1_ = hd es_; \
wneuper@665	1176	\ v1_ = hd vs_; \
wneuper@665	1177	\ xxx = if ((lhs e1_) =!= v1_) then 1 else 2; \
wneuper@665	1178	\ e2_ = Take (hd (tl es_)); \
wneuper@665	1179	\ e2_ = (Substitute [e1__]) e2_ \
wneuper@665	1180	\ in [e1_, e2_])";
wneuper@665	1181	(val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;)
wneuper@665	1182	val str = "if lhs e1_ =!= v1_ then 1 else 2";
wneuper@665	1183	val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
wneuper@665	1184
wneuper@665	1185	val str = "let xxx = (if lhs e1_ =!= v1_ then 1 else 2) in xxx";
wneuper@665	1186	(val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;)
wneuper@665	1187	atomty sc; term2str sc;
wneuper@665	1188
wneuper@665	1189	"--- scr [EqSystem,top_down_substitution,4x4] -- adapted only to 7.70";
wneuper@665	1190	val str =
wneuper@665	1191	"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
wneuper@665	1192	\ (let e2__ = Take (hd (tl es_)); \
wneuper@665	1193	\ e2__ = ((Substitute [e1__]) @@ \
wneuper@665	1194	\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
wneuper@665	1195	\ simplify_System_parenthesized False)) @@ \
wneuper@665	1196	\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
wneuper@665	1197	\ isolate_bdvs False)) @@ \
wneuper@665	1198	\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
wneuper@665	1199	\ simplify_System False))) e2__;\
wneuper@665	1200	\ es__ = Take [e1__, e2__] \
wneuper@665	1201	\ in (Try (Rewrite_Set order_system False)) es__)"
wneuper@665	1202	val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
wneuper@665	1203	val str =
wneuper@665	1204	"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
wneuper@665	1205	\ (let e2__ = Take (nth_ 2 es_); \
wneuper@665	1206	\ e2__ = ((Substitute [e1__]) @@ \
wneuper@665	1207	\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
wneuper@665	1208	\ simplify_System_parenthesized False)) @@ \
wneuper@665	1209	\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
wneuper@665	1210	\ isolate_bdvs False)) @@ \
wneuper@665	1211	\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
wneuper@665	1212	\ simplify_System False))) e2__;\
wneuper@665	1213	\ es__ = Take [e1__, e2__] \
wneuper@665	1214	\ in (Try (Rewrite_Set order_system False)) es__)"
wneuper@665	1215	val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
wneuper@665	1216	val str =
wneuper@665	1217	"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
wneuper@665	1218	\ (let e2__ = Take (nth_ 2 es_); \
wneuper@665	1219	\ e2__ = ((Substitute [e1__]) @@ \
wneuper@665	1220	\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, nth_ 2 vs_)] \
wneuper@665	1221	\ simplify_System_parenthesized False)) @@ \
wneuper@665	1222	\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, nth_ 2 vs_)]\
wneuper@665	1223	\ isolate_bdvs False)) @@ \
wneuper@665	1224	\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, nth_ 2 vs_)]\
wneuper@665	1225	\ simplify_System False))) e2__;\
wneuper@665	1226	\ es__ = Take [e1__, e2__] \
wneuper@665	1227	\ in (Try (Rewrite_Set order_system False)) es__)"
wneuper@665	1228	val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
wneuper@665	1229	val str =
wneuper@665	1230	"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
wneuper@665	1231	\ (let e2__ = Take (nth_ 2 es_); \
wneuper@665	1232	\ e2__ = ((Substitute [e1__]) @@ \
wneuper@665	1233	\ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 vs_),(bdv_2,nth_ 2 vs_),\
wneuper@665	1234	\ (bdv_3,nth_ 3 vs_),(bdv_4,nth_ 4 vs_)]\
wneuper@665	1235	\ simplify_System_parenthesized False)) @@ \
wneuper@665	1236	\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, nth_ 2 vs_)] \
wneuper@665	1237	\ isolate_bdvs False)) @@ \
wneuper@665	1238	\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, nth_ 2 vs_)] \
wneuper@665	1239	\ norm_Rational False))) e2__; \
wneuper@665	1240	\ es__ = Take [e1__, e2__] \
wneuper@665	1241	\ in [])"
wneuper@665	1242	val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
wneuper@665	1243	val str =
wneuper@665	1244	"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
wneuper@665	1245	\ (let e2_ = Take (nth_ 2 es_); \
wneuper@665	1246	\ e2_ = ((Substitute [e1_]) @@ \
wneuper@665	1247	\ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 vs_),(bdv_2,nth_ 2 vs_),\
wneuper@665	1248	\ (bdv_3,nth_ 3 vs_),(bdv_4,nth_ 4 vs_)]\
wneuper@665	1249	\ simplify_System_parenthesized False)) @@ \
wneuper@665	1250	\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, nth_ 2 vs_)] \
wneuper@665	1251	\ isolate_bdvs False)) @@ \
wneuper@665	1252	\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, nth_ 2 vs_)] \
wneuper@665	1253	\ norm_Rational False))) e2_; \
wneuper@665	1254	\ es_ = Take [e1_, e2_] \
wneuper@665	1255	\ in [e1_, e2_,e3_, e4_])"
wneuper@665	1256	val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
wneuper@665	1257	val str =
wneuper@665	1258	"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
wneuper@665	1259	\ (let e2_ = Take (nth_ 2 es_); \
wneuper@665	1260	\ e2_ = ((Substitute [e1_]) @@ \
wneuper@665	1261	\ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 vs_),(bdv_2,nth_ 2 vs_),\
wneuper@665	1262	\ (bdv_3,nth_ 3 vs_),(bdv_4,nth_ 4 vs_)]\
wneuper@665	1263	\ simplify_System_parenthesized False)) @@ \
wneuper@665	1264	\ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 vs_),(bdv_2,nth_ 2 vs_),\
wneuper@665	1265	\ (bdv_3,nth_ 3 vs_),(bdv_4,nth_ 4 vs_)]\
wneuper@665	1266	\ isolate_bdvs False)) @@ \
wneuper@665	1267	\ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 vs_),(bdv_2,nth_ 2 vs_),\
wneuper@665	1268	\ (bdv_3,nth_ 3 vs_),(bdv_4,nth_ 4 vs_)]\
wneuper@665	1269	\ norm_Rational False))) e2_; \
wneuper@665	1270	\ es_ = Take [e1_, e2_] \
wneuper@665	1271	\ in [e1_, e2_,e3_, e4_])"
wneuper@665	1272	val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
wneuper@665	1273	(---^^^-OK-----------------------------------------------------------------)
wneuper@665	1274	val str =
wneuper@665	1275	"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
wneuper@665	1276	\ (let e2_ = Take (nth_ 2 es_); \
wneuper@665	1277	\ e2_ = ((Substitute [e1_]) @@ \
wneuper@665	1278	\ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 vs_),(bdv_2,nth_ 2 vs_),\
wneuper@665	1279	\ (bdv_3,nth_ 3 vs_),(bdv_4,nth_ 4 vs_)]\
wneuper@665	1280	\ simplify_System_parenthesized False)) @@ \
wneuper@665	1281	\ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 vs_),(bdv_2,nth_ 2 vs_),\
wneuper@665	1282	\ (bdv_3,nth_ 3 vs_),(bdv_4,nth_ 4 vs_)]\
wneuper@665	1283	\ isolate_bdvs False)) @@ \
wneuper@665	1284	\ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 vs_),(bdv_2,nth_ 2 vs_),\
wneuper@665	1285	\ (bdv_3,nth_ 3 vs_),(bdv_4,nth_ 4 vs_)]\
wneuper@665	1286	\ norm_Rational False))) e2_ \
wneuper@665	1287	\ in [e1_, e2_, nth_ 3 es_, nth_ 4 es_])"
wneuper@665	1288	val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
wneuper@665	1289	(---vvv-NOT ok-------------------------------------------------------------)
wneuper@665	1290	atomty sc; term2str sc;
wneuper@665	1291
wneuper@665	1292
wneuper@665	1293	"----- 7.70 with met top_down_: me";
wneuper@664	1294	val fmz = ["equalities \
wneuper@664	1295	\[c = L * q_0, L * c + c_2 = q_0 * L ^^^ 2 / 2, c_3 = 0, c_4 = 0]",
wneuper@664	1296	"solveForVars [c, c_2, c_3, c_4]", "solution L"];
wneuper@664	1297	val (dI',pI',mI') =
wneuper@664	1298	("Biegelinie.thy",["linear", "system"],["no_met"]);
wneuper@664	1299	val p = e_pos'; val c = [];
wneuper@664	1300	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
wneuper@664	1301	val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
wneuper@664	1302	val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
wneuper@664	1303	val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
wneuper@664	1304	val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
wneuper@664	1305	case nxt of (_,Apply_Method ["EqSystem", "top_down_substitution", "4x4"]) => ()
wneuper@664	1306	\| _ => raise error "eqsystem.sml [EqSystem,top_down_,4x4] specify";
wneuper@664	1307	val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
wneuper@665	1308	val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
wneuper@665	1309	val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
wneuper@665	1310	val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
wneuper@665	1311	val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
wneuper@665	1312	val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
wneuper@665	1313	if nxt = ("End_Proof'", End_Proof') andalso
wneuper@665	1314	f2str f = "[c = L * q_0, c_2 = -1 * L ^^^ 2 * q_0 / 2, c_3 = 0, c_4 = 0]"
wneuper@665	1315	then () else raise error "eqsystem.sml: 7.70 with met top_down_: me";
wneuper@660	1316
wneuper@660	1317
wneuper@660	1318	"------- Bsp 7.71";
wneuper@658	1319	states:=[];
wneuper@658	1320	CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
wneuper@658	1321	"Randbedingungen [M_b L = 0, y 0 = 0, y L = 0, y' 0 = 0]",
wneuper@658	1322	"FunktionsVariable x"],
wneuper@658	1323	("Biegelinie.thy", ["Biegelinien"],
wneuper@658	1324	["IntegrierenUndKonstanteBestimmen2"] ))];
wneuper@658	1325	moveActiveRoot 1;
wneuper@658	1326	(*
wneuper@658	1327	trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;
wneuper@660	1328	##7.71## \|ordered \|subst.singles (recurs) \|2x2 \|diagonal
wneuper@660	1329	c c_2 \|c c_2 \|1' \|1': c c_2 \|
wneuper@660	1330	c_4 \| c_3 \|2:c_3 -> 4' :c c_2 c_4 \| \|
wneuper@660	1331	c c_2 c_3 c_4 \| c_4 \|3' \| \|
wneuper@660	1332	c_3 \|c c_2 c_3 c_4 \|3:c_4 -> 4'':c c_2 \|4'':c c_2 \| *)
wneuper@659	1333	val t = str2term"[0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2, \
wneuper@658	1334	\ 0 = c_4 + 0 / (-1 * EI), \
wneuper@658	1335	\ 0 = c_4 + L * c_3 +(12 * L ^^^ 2 * c_2 + 4 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) /(-24 * EI),\
wneuper@658	1336	\ 0 = c_3 + 0 / (-1 * EI)]";
wneuper@658	1337
wneuper@660	1338	"------- Bsp 7.72a ---------------vvvvvvvvvvvvv Momentenlinie postponed";
wneuper@658	1339	states:=[];
wneuper@658	1340	CalcTree [(["Traegerlaenge L",
wneuper@658	1341	"Momentenlinie ((q_0 * L)/ 6 * x - q_0 /(6 * L) * x^3)",
wneuper@658	1342	"Biegelinie y",
wneuper@658	1343	"Randbedingungen [y 0 = 0, y L = 0]",
wneuper@658	1344	"FunktionsVariable x"],
wneuper@658	1345	("Biegelinie.thy", ["vonMomentenlinieZu","Biegelinien"],
wneuper@658	1346	["Biegelinien", "AusMomentenlinie"]))];
wneuper@658	1347	moveActiveRoot 1;
wneuper@658	1348	(*
wneuper@658	1349	trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;
wneuper@658	1350	*)
wneuper@658	1351
wneuper@660	1352	"------- Bsp 7.72b";
wneuper@658	1353	states:=[];
wneuper@658	1354	CalcTree [(["Traegerlaenge L","Streckenlast (q_0 / L * x)","Biegelinie y",
wneuper@658	1355	"Randbedingungen [M_b 0 = 0, M_b L = 0, y 0 = 0, y L = 0]",
wneuper@658	1356	"FunktionsVariable x"],
wneuper@658	1357	("Biegelinie.thy", ["Biegelinien"],
wneuper@658	1358	["IntegrierenUndKonstanteBestimmen2"] ))];
wneuper@658	1359	moveActiveRoot 1;
wneuper@658	1360	(*
wneuper@658	1361	trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;
wneuper@660	1362	##7.72b## \|ord. \|subst.singles \|ord.triang.
wneuper@660	1363	c_2 \| \| \|c_2
wneuper@660	1364	c c_2 \| \|1:c_2 -> 2':c \|c_2 c
wneuper@660	1365	c_4 \| \| \|
wneuper@660	1366	c c_2 c_3 c_4 \| \|3:c_4 -> 4':c c_2 c_3 \|c_2 c c_3*)
wneuper@659	1367	val t = str2term"[0 = c_2, \
wneuper@658	1368	\ 0 = (6 * c_2 + 6 * L * c + -1 * L ^^^ 2 * q_0) / 6, \
wneuper@658	1369	\ 0 = c_4 + 0 / (-1 * EI), \
wneuper@658	1370	\ 0 = c_4 + L * c_3 + (60 * L ^^^ 2 * c_2 + 20 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) / (-120 * EI)]";
wneuper@658	1371
wneuper@660	1372	"------- Bsp 7.73 ---------------vvvvvvvvvvvvv Momentenlinie postponed";
wneuper@658	1373	states:=[];
wneuper@658	1374	CalcTree [(["Traegerlaenge L","Momentenlinie ???",(description unclear)
wneuper@658	1375	"Biegelinie y",
wneuper@658	1376	"Randbedingungen [y L = 0, y' L = 0]",
wneuper@658	1377	"FunktionsVariable x"],
wneuper@658	1378	("Biegelinie.thy", ["vonMomentenlinieZu","Biegelinien"],
wneuper@658	1379	["Biegelinien", "AusMomentenlinie"]))];
wneuper@658	1380	moveActiveRoot 1;
wneuper@658	1381	(*
wneuper@658	1382	trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;
wneuper@658	1383	*)
wneuper@658	1384
wneuper@658	1385
wneuper@658	1386	"----------- 4x4 systems from Biegelinie -------------------------";
wneuper@658	1387	"----------- 4x4 systems from Biegelinie -------------------------";
wneuper@658	1388	"----------- 4x4 systems from Biegelinie -------------------------";
wneuper@663	1389	(GOON replace this test with 7.70 @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@2)
wneuper@658	1390	"----- Bsp 7.27";
wneuper@658	1391	val fmz = ["equalities \
wneuper@658	1392	\[0 = c_4, \
wneuper@658	1393	\ 0 = c_4 + L * c_3 +(12 * L ^^^ 2 * c_2 + 4 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) / (-24 * EI), \
wneuper@658	1394	\ 0 = c_2, \
wneuper@658	1395	\ 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2]",
wneuper@658	1396	"solveForVars [c, c_2, c_3, c_4]", "solution L"];
wneuper@658	1397	val (dI',pI',mI') =
wneuper@658	1398	("Biegelinie.thy",["normalize", "4x4", "linear", "system"],
wneuper@658	1399	["EqSystem","normalize","4x4"]);
wneuper@658	1400	val p = e_pos'; val c = [];
wneuper@658	1401	val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
wneuper@658	1402	val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
wneuper@658	1403	val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
wneuper@658	1404	val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
wneuper@658	1405	val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
wneuper@658	1406	"------------------------------------------- Apply_Method...";
wneuper@658	1407	val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
wneuper@658	1408	"[0 = c_4, \
wneuper@658	1409	\ 0 = c_4 + L * c_3 +\n (12 * L ^^^ 2 * c_2 + 4 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) / (-24 * EI), \
wneuper@658	1410	\ 0 = c_2, \
wneuper@658	1411	\ 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2]";
wneuper@658	1412	"------------------------------------------- simplify_System_parenthesized...";
wneuper@658	1413	val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
wneuper@658	1414	"[0 = c_4, \
wneuper@658	1415	\ 0 = -1 * q_0 * L ^^^ 4 / (-24 * EI) + \
wneuper@658	1416	\ (4 * L ^^^ 3 * c / (-24 * EI) + \
wneuper@658	1417	\ (12 * L ^^^ 2 * c_2 / (-24 * EI) + \
wneuper@658	1418	\ (L * c_3 + c_4))), \
wneuper@658	1419	\ 0 = c_2, \
wneuper@658	1420	\ 0 = -1 * q_0 * L ^^^ 2 / 2 + (L * c + c_2)]";
wneuper@658	1421	(? "(4 L ^^^ 3 / (-24 * EI) * c" statt "(4 * L ^^^ 3 * c / (-24 * EI)" ?*)
wneuper@658	1422	"------------------------------------------- isolate_bdvs...";
wneuper@658	1423	val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
wneuper@658	1424	"[c_4 = 0,\
wneuper@658	1425	\ 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),\
wneuper@658	1426	\ c_2 = 0, \
wneuper@658	1427	\ c_2 = 0 + -1 * (-1 * q_0 * L ^^^ 2 / 2) + -1 * (L * c)]";
wneuper@658	1428	val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
wneuper@657	1429
wneuper@657	1430
wneuper@657	1431
wneuper@445	1432	(*
wneuper@445	1433	use"../smltest/IsacKnowledge/eqsystem.sml";
wneuper@445	1434	use"eqsystem.sml";
wneuper@445	1435	*)

author	wneuper
	Sat, 16 Sep 2006 23:07:37 +0200
branch	start_Take
changeset 665	f3181c8e796b
parent 664	88b6105a0c06
permissions	-rw-r--r--