1.1 --- a/src/sml/ROOT.ML Mon Dec 10 14:18:49 2007 +0100
1.2 +++ b/src/sml/ROOT.ML Thu Dec 27 12:25:27 2007 +0100
1.3 @@ -146,7 +146,7 @@
1.4 use"complex.sml";
1.5 use"diff.sml";
1.6 use"diffapp.sml";
1.7 - use"integrate.sml";
1.8 + (*use"integrate.sml";TODO.new_c: cvs before 071227, 11:50*)
1.9 use"equation.sml";
1.10 (*use"inssort.sml"; problems with recdef in Isabelle2002*)
1.11 use"logexp.sml";
1.12 @@ -166,7 +166,7 @@
1.13 use"vect.sml";
1.14 use"wn.sml";
1.15 use"eqsystem.sml";
1.16 - use"biegelinie.sml";
1.17 + (*use"biegelinie.sml";TODO.new_c: cvs before 071227, 11:50*)
1.18 use"algein.sml";
1.19 cd "../..";
1.20 "**** run tests on IsacKnowledge complete ****************";
2.1 --- a/src/sml/RTEST-root.sml Mon Dec 10 14:18:49 2007 +0100
2.2 +++ b/src/sml/RTEST-root.sml Thu Dec 27 12:25:27 2007 +0100
2.3 @@ -56,7 +56,7 @@
2.4 use"complex.sml";
2.5 use"diff.sml";
2.6 use"diffapp.sml";
2.7 - use"integrate.sml";
2.8 + (*use"integrate.sml";TODO.new_c: cvs before 071227, 11:50*)
2.9 use"equation.sml";
2.10 (*use"inssort.sml"; problems with recdef in Isabelle2002*)
2.11 use"logexp.sml";
2.12 @@ -76,7 +76,7 @@
2.13 use"vect.sml";
2.14 use"wn.sml";
2.15 use"eqsystem.sml";
2.16 - use"biegelinie.sml";
2.17 + (*use"biegelinie.sml";TODO.new_c: cvs before 071227, 11:50*)
2.18 use"algein.sml";
2.19 cd "../..";
2.20 "**** run tests on IsacKnowledge complete ****************";
3.1 --- a/src/sml/Scripts/rewrite.sml Mon Dec 10 14:18:49 2007 +0100
3.2 +++ b/src/sml/Scripts/rewrite.sml Thu Dec 27 12:25:27 2007 +0100
3.3 @@ -34,7 +34,7 @@
3.4 (((inst_bdv bdv) o norm o #prop o rep_thm) thm), ct);
3.5 *)
3.6 and rew_sub thy i bdv tless rls put_asm lrd r t =
3.7 - (((*writeln ("@@@ rew_sub begin: t = "^(term2str t));*)
3.8 + ((*TODO.new_c:( *)(*writeln ("@@@ rew_sub begin: t = "^(term2str t));*)
3.9 let (* copy from Pure/thm.ML: fun rewritec *)
3.10 val (lhs,rhs) = (dest_equals' o strip_trueprop
3.11 o Logic.strip_imp_concl) r;
3.12 @@ -69,7 +69,7 @@
3.13 else ((*writeln("##@ rew_sub: (t''= "^(term2str t'')^
3.14 ", p'' ="^(terms2str p'')^", true)");*)
3.15 (t'',p'',[],true))
3.16 - end) handle STOP_REW_SUB => (t,[],[],false)
3.17 + end(*TODO.new_c:) handle STOP_REW_SUB => (t,[],[],false)*)
3.18 ) handle _ (*NO_REWRITE WN050820 causes diff.behav. in tests + MATCH!*) =>
3.19 ((*writeln ("@@@ rew_sub gosub: t = "^(term2str t));*)
3.20 case t of
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/src/smltest/IsacKnowledge/eqsystem.sml Thu Dec 27 12:25:27 2007 +0100
4.3 @@ -0,0 +1,1435 @@
4.4 +(* tests on systems of equations
4.5 + author: Walther Neuper
4.6 + 050826,
4.7 + (c) due to copyright terms
4.8 +
4.9 +use"../smltest/IsacKnowledge/eqsystem.sml";
4.10 +use"eqsystem.sml";
4.11 +*)
4.12 +val thy = EqSystem.thy;
4.13 +
4.14 +"-----------------------------------------------------------------";
4.15 +"table of contents -----------------------------------------------";
4.16 +"-----------------------------------------------------------------";
4.17 +"----------- occur_exactly_in ------------------------------------";
4.18 +"----------- problems --------------------------------------------";
4.19 +"----------- rewrite-order ord_simplify_System -------------------";
4.20 +"----------- rewrite in [EqSystem,normalize,2x2] -----------------";
4.21 +"----------- rewrite example from 2nd [EqSystem,normalize,2x2] ---";
4.22 +"----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
4.23 +"----------- rewrite in [EqSystem,normalize,4x4] -----------------";
4.24 +"----------- script [EqSystem,normalize,2x2] ---------------------";
4.25 +"----------- script [EqSystem,top_down_substitution,2x2] Vers.1 --";
4.26 +"----------- script [EqSystem,top_down_substitution,2x2] Vers.2 --";
4.27 +"----------- refine [linear,system]-------------------------------";
4.28 +"----------- refine [2x2,linear,system] search error--------------";
4.29 +"----------- me [EqSystem,normalize,2x2] -------------------------";
4.30 +"----------- me [linear,system] ..normalize..top_down_sub..-------";
4.31 +"----------- all systems from Biegelinie -------------------------";
4.32 +"----------- 4x4 systems from Biegelinie -------------------------";
4.33 +"-----------------------------------------------------------------";
4.34 +"-----------------------------------------------------------------";
4.35 +"-----------------------------------------------------------------";
4.36 +
4.37 +
4.38 +"----------- occur_exactly_in ------------------------------------";
4.39 +"----------- occur_exactly_in ------------------------------------";
4.40 +"----------- occur_exactly_in ------------------------------------";
4.41 +val all = [str2term"c", str2term"c_2", str2term"c_3"];
4.42 +val t = str2term"0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2";
4.43 +
4.44 +if occur_exactly_in [str2term"c", str2term"c_2"] all t
4.45 +then () else raise error "eqsystem.sml occur_exactly_in 1";
4.46 +
4.47 +if not (occur_exactly_in [str2term"c", str2term"c_2", str2term"c_3"] all t)
4.48 +then () else raise error "eqsystem.sml occur_exactly_in 2";
4.49 +
4.50 +if not (occur_exactly_in [str2term"c_2"] all t)
4.51 +then () else raise error "eqsystem.sml occur_exactly_in 3";
4.52 +
4.53 +
4.54 +val t = str2term"[c,c_2] from_ [c,c_2,c_3] occur_exactly_in \
4.55 + \-1 * q_0 * L ^^^ 2 / 2 + L * c + c_2";
4.56 +val Some (str, t') = eval_occur_exactly_in 0 "EqSystem.occur'_exactly'_in" t 0;
4.57 +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 ()
4.58 +else raise error "eval_occur_exactly_in [c, c_2]";
4.59 +
4.60 +val t = str2term"[c,c_2,c_3] from_ [c,c_2,c_3] occur_exactly_in \
4.61 + \-1 * q_0 * L ^^^ 2 / 2 + L * c + c_2";
4.62 +val Some (str, t') = eval_occur_exactly_in 0 "EqSystem.occur'_exactly'_in" t 0;
4.63 +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 ()
4.64 +else raise error "eval_occur_exactly_in [c, c_2, c_3]";
4.65 +
4.66 +val t = str2term"[c_2] from_ [c,c_2,c_3] occur_exactly_in \
4.67 + \-1 * q_0 * L ^^^ 2 / 2 + L * c + c_2";
4.68 +val Some (str, t') = eval_occur_exactly_in 0 "EqSystem.occur'_exactly'_in" t 0;
4.69 +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 ()
4.70 +else raise error "eval_occur_exactly_in [c, c_2, c_3]";
4.71 +
4.72 +val t = str2term"[] from_ [c,c_2,c_3] occur_exactly_in 0";
4.73 +val Some (str, t') = eval_occur_exactly_in 0 "EqSystem.occur'_exactly'_in" t 0;
4.74 +if str = "[] from_ [c, c_2, c_3] occur_exactly_in 0 = True" then ()
4.75 +else raise error "eval_occur_exactly_in [c, c_2, c_3]";
4.76 +
4.77 +val t =
4.78 + str2term
4.79 + "[] from_ [c, c_2, c_3, c_4] occur_exactly_in -1 * (q_0 * L ^^^ 2) /2";
4.80 +val Some (str, t') = eval_occur_exactly_in 0 "EqSystem.occur'_exactly'_in" t 0;
4.81 +if str = "[] from_ [c, c_2, c_3, c_4] occur_exactly_in \
4.82 + \-1 * (q_0 * L ^^^ 2) / 2 = True" then ()
4.83 +else raise error "eval_occur_exactly_in [c, c_2, c_3, c_4]";
4.84 +
4.85 +
4.86 +"----------- problems --------------------------------------------";
4.87 +"----------- problems --------------------------------------------";
4.88 +"----------- problems --------------------------------------------";
4.89 +val t = str2term "length_ [x+y=1,y=2] = 2";
4.90 +atomty t;
4.91 +val testrls = append_rls "testrls" e_rls
4.92 + [(Thm ("length_Nil_",num_str length_Nil_)),
4.93 + (Thm ("length_Cons_",num_str length_Cons_)),
4.94 + Calc ("op +", eval_binop "#add_"),
4.95 + Calc ("op =",eval_equal "#equal_")
4.96 + ];
4.97 +val Some (t',_) = rewrite_set_ thy false testrls t;
4.98 +if term2str t' = "True" then ()
4.99 +else raise error "eqsystem.sml: length_ [x+y=1,y=2] = 2";
4.100 +
4.101 +val Some t = parse EqSystem.thy "solution L";
4.102 +atomty (term_of t);
4.103 +val Some t = parse Biegelinie.thy "solution L";
4.104 +atomty (term_of t);
4.105 +
4.106 +val t = str2term
4.107 +"(tl (tl (tl vs_))) from_ vs_ occur_exactly_in (nth_ 1 (es_::bool list))";
4.108 +atomty t;
4.109 +val t = str2term
4.110 +"(tl (tl (tl [c,c_2,c_3,c_4]))) from_ [c,c_2,c_3,c_4] occur_exactly_in \
4.111 +\(nth_ 1 [c_4 = 1, 2=2,3=3,4=4])";
4.112 +val Some (t,_) =
4.113 + rewrite_set_ thy true
4.114 + (append_rls "prls_" e_rls
4.115 + [Thm ("nth_Cons_",num_str nth_Cons_),
4.116 + Thm ("nth_Nil_",num_str nth_Nil_),
4.117 + Thm ("tl_Cons",num_str tl_Cons),
4.118 + Thm ("tl_Nil",num_str tl_Nil),
4.119 + Calc ("EqSystem.occur'_exactly'_in",
4.120 + eval_occur_exactly_in
4.121 + "#eval_occur_exactly_in_")
4.122 + ]) t;
4.123 +if t = HOLogic.true_const then ()
4.124 +else raise error "eqsystem.sml ..occur_exactly_in (nth_ 1 [c_4..";
4.125 +
4.126 +
4.127 +"----------- rewrite-order ord_simplify_System -------------------";
4.128 +"----------- rewrite-order ord_simplify_System -------------------";
4.129 +"----------- rewrite-order ord_simplify_System -------------------";
4.130 +"M_b x = c * x + -1 * q_0 * (x ^^^ 2 / 2) + c_2";
4.131 +"--- add_commute ---";
4.132 +if ord_simplify_System false thy [] (str2term"-1 * q_0 * (x ^^^ 2 / 2)",
4.133 + str2term"c * x") then ()
4.134 +else raise error "integrate.sml, (-1 * q_0 * (x ^^^ 2 / 2)) < (c * x) not#1";
4.135 +
4.136 +if ord_simplify_System false thy [] (str2term"-1 * q_0 * (x ^^^ 2 / 2)",
4.137 + str2term"c_2") then ()
4.138 +else raise error "integrate.sml, (-1 * q_0 * (x ^^^ 2 / 2)) < (c_2) not#2";
4.139 +
4.140 +if ord_simplify_System false thy [] (str2term"c * x",
4.141 + str2term"c_2") then ()
4.142 +else raise error "integrate.sml, (c * x) < (c_2) not#3";
4.143 +
4.144 +"--- mult_commute ---";
4.145 +if ord_simplify_System false thy [] (str2term"x * c",
4.146 + str2term"c * x") then ()
4.147 +else raise error "integrate.sml, (x * c) < (c * x) not#4";
4.148 +
4.149 +if ord_simplify_System false thy [] (str2term"-1 * q_0 * (x ^^^ 2 / 2) * c",
4.150 + str2term"-1 * q_0 * c * (x ^^^ 2 / 2)")
4.151 +then () else raise error "integrate.sml, (. * .) < (. * .) not#5";
4.152 +
4.153 +if ord_simplify_System false thy [] (str2term"-1 * q_0 * (x ^^^ 2 / 2) * c",
4.154 + str2term"c * -1 * q_0 * (x ^^^ 2 / 2)")
4.155 +then () else raise error "integrate.sml, (. * .) < (. * .) not#6";
4.156 +
4.157 +
4.158 +"----------- rewrite in [EqSystem,normalize,2x2] -----------------";
4.159 +"----------- rewrite in [EqSystem,normalize,2x2] -----------------";
4.160 +"----------- rewrite in [EqSystem,normalize,2x2] -----------------";
4.161 +val t = str2term"[0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2,\
4.162 + \0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2]";
4.163 +val bdvs = [(str2term"bdv_1",str2term"c"),
4.164 + (str2term"bdv_2",str2term"c_2")];
4.165 +val Some(t,_)= rewrite_set_inst_ thy true bdvs simplify_System_parenthesized t;
4.166 +if term2str t = "[0 = -1 * q_0 * L ^^^ 2 / 2 + (L * c + c_2), 0 = c_2]"
4.167 +then () else raise error "eqsystem.sml rewrite in 2x2 simplify_System_par.1";
4.168 +
4.169 +val Some (t,_) = rewrite_set_inst_ thy true bdvs isolate_bdvs t;
4.170 +if term2str t = "[L * c + c_2 = 0 + -1 * (-1 * q_0 * L ^^^ 2 / 2), c_2 = 0]"
4.171 +then () else raise error "eqsystem.sml rewrite in 2x2 isolate_bdvs";
4.172 +
4.173 +val Some(t,_)= rewrite_set_inst_ thy true bdvs simplify_System t;
4.174 +if term2str t = "[L * c + c_2 = q_0 * L ^^^ 2 / 2, c_2 = 0]"
4.175 +then () else raise error "eqsystem.sml rewrite in 2x2 simplify_System_par.2";
4.176 +
4.177 +val Some (t,_) = rewrite_set_ thy true order_system t;
4.178 +if term2str t = "[c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]"
4.179 +then () else raise error "eqsystem.sml rewrite in 2x2 simplify_System_par.3";
4.180 +
4.181 +
4.182 +"----------- rewrite example from 2nd [EqSystem,normalize,2x2] ---";
4.183 +"----------- rewrite example from 2nd [EqSystem,normalize,2x2] ---";
4.184 +"----------- rewrite example from 2nd [EqSystem,normalize,2x2] ---";
4.185 +val thy = Isac.thy (*because of Undeclared constant "Biegelinie.EI*);
4.186 +val t =
4.187 + str2term"[0 = c_2 + c * 0 + 1 / EI * (L * q_0 / 12 * 0 ^^^ 3 + \
4.188 + \ -1 * q_0 / 24 * 0 ^^^ 4),\
4.189 + \ 0 = c_2 + c * L + 1 / EI * (L * q_0 / 12 * L ^^^ 3 + \
4.190 + \ -1 * q_0 / 24 * L ^^^ 4)]";
4.191 +val Some (t,_) = rewrite_set_ thy true norm_Rational t;
4.192 +if term2str t="[0 = c_2, 0 = c_2 + L * c + L ^^^ 4 * q_0 / (EI * 24)]"
4.193 +then () else raise error "eqsystem.sml rewrite in 2x2 simplify_System_par.0b";
4.194 +
4.195 +val Some(t,_)= rewrite_set_inst_ thy true bdvs simplify_System_parenthesized t;
4.196 +if term2str t = "[0 = c_2, 0 = q_0 * L ^^^ 4 / (24 * EI) + (L * c + c_2)]"
4.197 +then () else raise error "eqsystem.sml rewrite in 2x2 simplify_System_par.1b";
4.198 +
4.199 +val Some (t,_) = rewrite_set_inst_ thy true bdvs isolate_bdvs t;
4.200 +if term2str t = "[c_2 = 0, L * c + c_2 = 0 + -1 * (q_0 * L ^^^ 4 / (24 * EI))]"
4.201 +then () else raise error "eqsystem.sml rewrite in 2x2 isolate_bdvs b";
4.202 +
4.203 +val Some(t,_)= rewrite_set_inst_ thy true bdvs simplify_System t;
4.204 +if term2str t = "[c_2 = 0, L * c + c_2 = -1 * q_0 * L ^^^ 4 / (24 * EI)]"
4.205 +then () else raise error "eqsystem.sml rewrite in 2x2 simplify_System.2b";
4.206 +
4.207 +val xxx = rewrite_set_ thy true order_system t;
4.208 +if is_none xxx
4.209 +then () else raise error "eqsystem.sml rewrite in 2x2 simplify_System.3b";
4.210 +
4.211 +
4.212 +"----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
4.213 +"----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
4.214 +"----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
4.215 +val e1__ = str2term "c_2 = 77";
4.216 +val e2__ = str2term "L * c + c_2 = q_0 * L ^^^ 2 / 2";
4.217 +val bdvs = [(str2term"bdv_1",str2term"c"),
4.218 + (str2term"bdv_2",str2term"c_2")];
4.219 +val Some (e2__,_) = rewrite_terms_ thy dummy_ord Erls [e1__] e2__;
4.220 +if term2str e2__ = "L * c + 77 = q_0 * L ^^^ 2 / 2" then ()
4.221 +else raise error "eqsystem.sml top_down_substitution,2x2] subst";
4.222 +
4.223 +val Some (e2__,_) =
4.224 + rewrite_set_inst_ thy true bdvs simplify_System_parenthesized e2__;
4.225 +if term2str e2__ = "77 + L * c = q_0 * L ^^^ 2 / 2" then ()
4.226 +else raise error "eqsystem.sml top_down_substitution,2x2] simpl_par";
4.227 +
4.228 +val Some (e2__,_) = rewrite_set_inst_ thy true bdvs isolate_bdvs e2__;
4.229 +if term2str e2__ = "c = (q_0 * L ^^^ 2 / 2 + -1 * 77) / L" then ()
4.230 +else raise error "eqsystem.sml top_down_substitution,2x2] isolate";
4.231 +
4.232 +val t = str2term "[c_2 = 77, c = (q_0 * L ^^^ 2 / 2 + -1 * 77) / L]";
4.233 +val Some (t,_) = rewrite_set_ thy true order_system t;
4.234 +if term2str t = "[c = (q_0 * L ^^^ 2 / 2 + -1 * 77) / L, c_2 = 77]" then ()
4.235 +else raise error "eqsystem.sml top_down_substitution,2x2] order_system";
4.236 +
4.237 +if not (ord_simplify_System
4.238 + false thy []
4.239 + (str2term"[c_2 = 77, c = (q_0 * L ^^^ 2 / 2 + -1 * 77) / L]",
4.240 + str2term"[c = (q_0 * L ^^^ 2 / 2 + -1 * 77) / L, c_2 = 77]"))
4.241 +then () else raise error "eqsystem.sml, order_result rew_ord";
4.242 +
4.243 +trace_rewrite:=true;
4.244 +trace_rewrite:=false;
4.245 +
4.246 +
4.247 +"----------- rewrite in [EqSystem,normalize,4x4] -----------------";
4.248 +"----------- rewrite in [EqSystem,normalize,4x4] -----------------";
4.249 +"----------- rewrite in [EqSystem,normalize,4x4] -----------------";
4.250 +(*GOON??: revise rewrite in [EqSystem,normalize,4x4] from before 0609*)
4.251 +val t = str2term"[0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c_3 + c_4,\
4.252 + \0 = -1 * q_0 * L ^^^ 2 / 2 + L * c_3 + c_4,\
4.253 + \c + c_2 + c_3 + c_4 = 0,\
4.254 + \c_2 + c_3 + c_4 = 0]";
4.255 +val bdvs = [(str2term"bdv_1",str2term"c"),
4.256 + (str2term"bdv_2",str2term"c_2"),
4.257 + (str2term"bdv_3",str2term"c_3"),
4.258 + (str2term"bdv_4",str2term"c_4")];
4.259 +val Some (t,_) =
4.260 + rewrite_set_inst_ thy true bdvs simplify_System_parenthesized t;
4.261 +if term2str t = "[0 = c_4, 0 = -1 * q_0 * L ^^^ 2 / 2 + (L * c_3 + c_4),\n\
4.262 + \ c + (c_2 + (c_3 + c_4)) = 0, c_2 + (c_3 + c_4) = 0]"
4.263 +then () else raise error "eqsystem.sml rewrite in 4x4 simplify_System_paren";
4.264 +
4.265 +val Some (t,_) = rewrite_set_inst_ thy true bdvs isolate_bdvs t;
4.266 +if term2str t = "[c_4 = 0, \
4.267 + \L * c_3 + c_4 = 0 + -1 * (-1 * q_0 * L ^^^ 2 / 2),\n \
4.268 + \c + (c_2 + (c_3 + c_4)) = 0, c_2 + (c_3 + c_4) = 0]"
4.269 +then () else raise error "eqsystem.sml rewrite in 4x4 isolate_bdvs";
4.270 +
4.271 +val Some(t,_)= rewrite_set_inst_ thy true bdvs simplify_System_parenthesized t;
4.272 +if term2str t = "[c_4 = 0,\
4.273 + \ L * c_3 + c_4 = q_0 * L ^^^ 2 / 2,\
4.274 + \ c + (c_2 + (c_3 + c_4)) = 0,\n\
4.275 + \ c_2 + (c_3 + c_4) = 0]"
4.276 +then () else raise error "eqsystem.sml rewrite in 4x4 simplify_System_p..2";
4.277 +
4.278 +val Some (t,_) = rewrite_set_ thy true order_system t;
4.279 +if term2str t = "[c_4 = 0,\
4.280 + \ L * c_3 + c_4 = q_0 * L ^^^ 2 / 2,\
4.281 + \ c_2 + (c_3 + c_4) = 0,\n\
4.282 + \ c + (c_2 + (c_3 + c_4)) = 0]"
4.283 +then () else raise error "eqsystem.sml rewrite in 4x4 order_system";
4.284 +
4.285 +
4.286 +"----------- script [EqSystem,normalize,2x2] ---------------------";
4.287 +"----------- script [EqSystem,normalize,2x2] ---------------------";
4.288 +"----------- script [EqSystem,normalize,2x2] ---------------------";
4.289 +val str =
4.290 +"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
4.291 +\ (let es__ = (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
4.292 +\ simplify_System_parenthesized False) es_ \
4.293 +\ in ([]))";
4.294 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
4.295 +val str =
4.296 +"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
4.297 +\ (let es__ = (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
4.298 +\ simplify_System_parenthesized False) es_ \
4.299 +\ in (SubProblem (Biegelinie_,[linear,system],[no_met])\
4.300 +\ []))";
4.301 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
4.302 +val str =
4.303 +"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
4.304 +\ (let es__ = (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
4.305 +\ simplify_System_parenthesized False) es_ \
4.306 +\ in (SubProblem (Biegelinie_,[linear,system],[no_met])\
4.307 +\ [bool_list_ es__, real_list_ vs_]))"
4.308 +;
4.309 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
4.310 +val str =
4.311 +"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
4.312 +\ (let es__ = Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
4.313 +\ simplify_System_parenthesized False) es_ \
4.314 +\ in (SubProblem (Biegelinie_,[linear,system],[no_met])\
4.315 +\ [bool_list_ es__, real_list_ vs_]))"
4.316 +;
4.317 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
4.318 +val str =
4.319 +"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
4.320 +\ (let es__ = (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
4.321 +\ simplify_System_parenthesized False)) es_ \
4.322 +\ in (SubProblem (Biegelinie_,[linear,system],[no_met])\
4.323 +\ [bool_list_ es__, real_list_ vs_]))"
4.324 +;
4.325 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
4.326 +val str =
4.327 +"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
4.328 +\ (let es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
4.329 +\ simplify_System_parenthesized False)) @@\
4.330 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
4.331 +\ simplify_System_parenthesized False))) es_\
4.332 +\ in (SubProblem (Biegelinie_,[linear,system],[no_met])\
4.333 +\ [bool_list_ es__, real_list_ vs_]))"
4.334 +;
4.335 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
4.336 +val str =
4.337 +"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
4.338 +\ (let es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
4.339 +\ simplify_System_parenthesized False)) @@\
4.340 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
4.341 +\ simplify_System_parenthesized False)) @@\
4.342 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
4.343 +\ simplify_System_parenthesized False))) es_\
4.344 +\ in (SubProblem (Biegelinie_,[linear,system],[no_met])\
4.345 +\ [bool_list_ es__, real_list_ vs_]))"
4.346 +;
4.347 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
4.348 +val str =
4.349 +"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
4.350 +\ (let es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
4.351 +\ simplify_System_parenthesized False)) @@\
4.352 +\ (Try (Rewrite_Set_Inst [] isolate_bdvs False)) @@\
4.353 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
4.354 +\ simplify_System_parenthesized False)) @@\
4.355 +\ (Try (Rewrite_Set order_system False))) es_\
4.356 +\ in (SubProblem (Biegelinie_,[linear,system],[no_met])\
4.357 +\ [bool_list_ es__, real_list_ vs_]))"
4.358 +;
4.359 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
4.360 +val str =
4.361 +"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
4.362 +\ (let es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
4.363 +\ simplify_System_parenthesized False)) @@\
4.364 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_)]\
4.365 +\ isolate_bdvs False)) @@\
4.366 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
4.367 +\ simplify_System_parenthesized False)) @@\
4.368 +\ (Try (Rewrite_Set order_system False))) es_\
4.369 +\ in (SubProblem (Biegelinie_,[linear,system],[no_met])\
4.370 +\ [bool_list_ es__, real_list_ vs_]))"
4.371 +;
4.372 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
4.373 +val str =
4.374 +"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
4.375 +\ (let es__ = ((Try (Rewrite_Set simplify_System_parenthesized False)) @@\
4.376 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
4.377 +\ isolate_bdvs False)) @@\
4.378 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
4.379 +\ simplify_System_parenthesized False)) @@\
4.380 +\ (Try (Rewrite_Set order_system False))) es_\
4.381 +\ in (SubProblem (Biegelinie_,[linear,system],[no_met])\
4.382 +\ [bool_list_ es__, real_list_ vs_]))"
4.383 +;
4.384 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
4.385 +(*---^^^-OK-----------------------------------------------------------------*)
4.386 +(*---vvv-NOT ok-------------------------------------------------------------*)
4.387 +
4.388 +
4.389 +"----------- script [EqSystem,top_down_substitution,2x2] Vers.1 --";
4.390 +"----------- script [EqSystem,top_down_substitution,2x2] Vers.1 --";
4.391 +"----------- script [EqSystem,top_down_substitution,2x2] Vers.1 --";
4.392 +val str =
4.393 +"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
4.394 +\ (let es__ = (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
4.395 +\ simplify_System_parenthesized False) es_ \
4.396 +\ in ([]))";
4.397 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
4.398 +val str =
4.399 +"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
4.400 +\ (let e1__ = Take (hd es_) \
4.401 +\ in ([]))";
4.402 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
4.403 +val str =
4.404 +"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
4.405 +\ (let e1__ = Take (hd es_); \
4.406 +\ e1__ = Take (hd es_) \
4.407 +\ in ([]))";
4.408 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
4.409 +val str =
4.410 +"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
4.411 +\ (let e1__ = Take (hd es_); \
4.412 +\ e1__ = (Take (hd es_))\
4.413 +\ in ([]))";
4.414 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
4.415 +val str =
4.416 +"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
4.417 +\ (let e1__ = Take (hd es_); \
4.418 +\ e1__ = ((Rewrite_Set order_system False)) e1__\
4.419 +\ in ([]))";
4.420 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
4.421 +(*--------------------------------------------------------------------------*)
4.422 +val str =
4.423 +"(Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
4.424 +\ isolate_bdvs False) (e1__::bool)";
4.425 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
4.426 +(*--------------------------------------------------------------------------*)
4.427 +val str =
4.428 +"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
4.429 +\ (let e1__ = Take (hd es_); \
4.430 +\ e1__ = ((Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
4.431 +\ isolate_bdvs False)) e1__\
4.432 +\ in ([]))";
4.433 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
4.434 +val str =
4.435 +"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
4.436 +\ (let e1__ = Take (hd es_); \
4.437 +\ e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
4.438 +\ isolate_bdvs False)) @@\
4.439 +\ (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
4.440 +\ simplify_System False)) e1__\
4.441 +\ in ([]))";
4.442 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
4.443 +val str =
4.444 +"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
4.445 +\ (let e1__ = Take (hd es_); \
4.446 +\ e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
4.447 +\ isolate_bdvs False)) @@\
4.448 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
4.449 +\ simplify_System False))) e1__\
4.450 +\ in ([]))";
4.451 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
4.452 +val str =
4.453 +"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
4.454 +\ (let e1__ = Take (hd es_); \
4.455 +\ e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
4.456 +\ isolate_bdvs False)) @@ \
4.457 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
4.458 +\ simplify_System False))) e1__; \
4.459 +\ e2__ = Take (hd (tl es_)) \
4.460 +\ in ([]))";
4.461 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
4.462 +val str =
4.463 +"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
4.464 +\ (let e1__ = Take (hd es_); \
4.465 +\ e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
4.466 +\ isolate_bdvs False)) @@ \
4.467 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
4.468 +\ simplify_System False))) e1__; \
4.469 +\ e2__ = Take (hd (tl es_)); \
4.470 +\ e2__ = Substitute [e1__] e2__ \
4.471 +\ in ([]))";
4.472 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
4.473 +val str =
4.474 +"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
4.475 +\ (let e1__ = Take (hd es_); \
4.476 +\ e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
4.477 +\ isolate_bdvs False)) @@ \
4.478 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
4.479 +\ simplify_System False))) e1__; \
4.480 +\ e2__ = Take (hd (tl es_)); \
4.481 +\ e2__ = ((Substitute [e1__])) e2__ \
4.482 +\ in ([]))";
4.483 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
4.484 +val str =
4.485 +"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
4.486 +\ (let e1__ = Take (hd es_); \
4.487 +\ e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
4.488 +\ isolate_bdvs False)) @@ \
4.489 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
4.490 +\ simplify_System False))) e1__; \
4.491 +\ e2__ = Take (hd (tl es_)); \
4.492 +\ e2__ = ((Substitute [e1__]) @@ \
4.493 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
4.494 +\ isolate_bdvs False)) @@ \
4.495 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
4.496 +\ simplify_System False))) e2__ \
4.497 +\ in [e1__, e2__])"
4.498 +;
4.499 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
4.500 +val str =
4.501 +"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
4.502 +\ (let e1__ = Take (hd es_); \
4.503 +\ e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
4.504 +\ isolate_bdvs False)) @@ \
4.505 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
4.506 +\ simplify_System False))) e1__; \
4.507 +\ e2__ = Take (hd (tl es_)); \
4.508 +\ e2__ = ((Substitute [e1__]) @@ \
4.509 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
4.510 +\ simplify_System_parenthesized False)) @@ \
4.511 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
4.512 +\ isolate_bdvs False)) @@ \
4.513 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
4.514 +\ simplify_System False)) @@ \
4.515 +\ (Try (Rewrite_Set order_system False))) e2__ \
4.516 +\ in [e1__, e2__])"
4.517 +;
4.518 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
4.519 +(*---^^^-OK-----------------------------------------------------------------*)
4.520 +val str =
4.521 +"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
4.522 +\ (let e1__ = Take (hd es_); \
4.523 +\ e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
4.524 +\ isolate_bdvs False)) @@ \
4.525 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
4.526 +\ simplify_System False))) e1__; \
4.527 +\ e2__ = Take (hd (tl es_)); \
4.528 +\ e2__ = ((Substitute [e1__]) @@ \
4.529 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
4.530 +\ simplify_System_parenthesized False)) @@ \
4.531 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
4.532 +\ isolate_bdvs False)) @@ \
4.533 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
4.534 +\ simplify_System False))) e2__; \
4.535 +\ es__ = Take [e1__, e2__]\
4.536 +\ in (Try (Rewrite_Set order_system False)) es__)"
4.537 +;
4.538 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
4.539 +(*---vvv-NOT ok-------------------------------------------------------------*)
4.540 +atomty sc;
4.541 +
4.542 +"----------- script [EqSystem,top_down_substitution,2x2] Vers.2 --";
4.543 +"----------- script [EqSystem,top_down_substitution,2x2] Vers.2 --";
4.544 +"----------- script [EqSystem,top_down_substitution,2x2] Vers.2 --";
4.545 +val str =
4.546 +"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
4.547 +\ (let es__ = Take es_; \
4.548 +\ e1__ = hd es__\
4.549 +\ in ([]))"
4.550 +;
4.551 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
4.552 +val str =
4.553 +"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
4.554 +\ (let es__ = Take es_; \
4.555 +\ e1__ = hd es__; \
4.556 +\ e2__ = hd (tl es__)\
4.557 +\ in ([]))"
4.558 +;
4.559 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
4.560 +val str =
4.561 +"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
4.562 +\ (let es__ = Take es_; \
4.563 +\ e1__ = hd es__; \
4.564 +\ e2__ = hd (tl es__);\
4.565 +\ es__ = [1=2,3=4]\
4.566 +\ in ([]))"
4.567 +;
4.568 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
4.569 +val str =
4.570 +"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
4.571 +\ (let es__ = Take es_; \
4.572 +\ e1__ = hd es__; \
4.573 +\ e2__ = hd (tl es__);\
4.574 +\ es__ = [e1__,e2__]\
4.575 +\ in ([]))"
4.576 +;
4.577 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
4.578 +val str =
4.579 +"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
4.580 +\ (let es__ = Take es_; \
4.581 +\ e1__ = hd es__; \
4.582 +\ e2__ = hd (tl es__);\
4.583 +\ es__ = [e1__, Substitute [e1__] e2__];\
4.584 +\ es__ = (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
4.585 +\ simplify_System False)) es__ \
4.586 +\ in ([]))"
4.587 +;
4.588 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
4.589 +val str =
4.590 +"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
4.591 +\ (let es__ = Take es_; \
4.592 +\ e1__ = hd es__; \
4.593 +\ e2__ = hd (tl es__);\
4.594 +\ es__ = [e1__, Substitute [e1__] e2__];\
4.595 +\ es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
4.596 +\ isolate_bdvs False)) @@ \
4.597 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
4.598 +\ simplify_System False))) es__ \
4.599 +\ in ([]))"
4.600 +;
4.601 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
4.602 +val str =
4.603 +"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
4.604 +\ (let es__ = Take es_; \
4.605 +\ e1__ = hd es__; \
4.606 +\ e2__ = hd (tl es__);\
4.607 +\ es__ = [e1__, Substitute [e1__] e2__];\
4.608 +\ es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
4.609 +\ simplify_System_parenthesized False)) @@ \
4.610 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
4.611 +\ isolate_bdvs False)) @@ \
4.612 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
4.613 +\ simplify_System False))) es__ \
4.614 +\ in ([]))"
4.615 +;
4.616 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
4.617 +val str =
4.618 +"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
4.619 +\ (let es__ = Take es_; \
4.620 +\ e1__ = hd es__; \
4.621 +\ e2__ = hd (tl es__); \
4.622 +\ es__ = [e1__, Substitute [e1__] e2__]; \
4.623 +\ es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
4.624 +\ simplify_System_parenthesized False)) @@ \
4.625 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
4.626 +\ isolate_bdvs False)) @@ \
4.627 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
4.628 +\ simplify_System False))) es__ \
4.629 +\ in es__)"
4.630 +;
4.631 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
4.632 +val str =
4.633 +"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
4.634 +\ (let es__ = Take es_; \
4.635 +\ e1__ = hd es__; \
4.636 +\ e2__ = hd (tl es__); \
4.637 +\ es__ = [e1__, Substitute [e1__] e2__] \
4.638 +\ in ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
4.639 +\ simplify_System_parenthesized False)) @@ \
4.640 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))] \
4.641 +\ isolate_bdvs False)) @@ \
4.642 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
4.643 +\ simplify_System False))) es__)"
4.644 +;
4.645 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
4.646 +(*---^^^-OK-----------------------------------------------------------------*)
4.647 +val str =
4.648 +"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
4.649 +\ (let es__ = Take es_; \
4.650 +\ e1__ = hd es__; \
4.651 +\ e2__ = hd (tl es__); \
4.652 +\ es__ = [e1__, Substitute [e1__] e2__] "^
4.653 +(* this ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ is a script-'Expr'
4.654 + which is not yet searched for 'STac's; thus this script does not yet work*)
4.655 +" in ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
4.656 +\ simplify_System_parenthesized False)) @@ \
4.657 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))] \
4.658 +\ isolate_bdvs False)) @@ \
4.659 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
4.660 +\ simplify_System False))) es__)"
4.661 +;
4.662 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
4.663 +(*---vvv-NOT ok-------------------------------------------------------------*)
4.664 +atomty sc;
4.665 +
4.666 +
4.667 +"----------- refine [linear,system]-------------------------------";
4.668 +"----------- refine [linear,system]-------------------------------";
4.669 +"----------- refine [linear,system]-------------------------------";
4.670 +val fmz = ["equalities [0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2,\
4.671 + \0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2]",
4.672 + "solveForVars [c, c_2]", "solution L"];
4.673 +val matches = refine fmz ["linear","system"];
4.674 +case matches of [_,_,_,
4.675 + Matches (["normalize", "2x2", "linear", "system"],
4.676 + {Find = [Correct "solution L"],
4.677 + With = [],
4.678 + Given =
4.679 + [Correct
4.680 + "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]",
4.681 + Correct "solveForVars [c, c_2]"],
4.682 + Where = [],
4.683 + Relate = []})] => ()
4.684 + | _ => raise error "eqsystem.sml refine ['normalize','2x2'...]";
4.685 +
4.686 +
4.687 +val fmz = ["equalities [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]",
4.688 + "solveForVars [c, c_2]", "solution L"];
4.689 +val matches = refine fmz ["linear","system"];
4.690 +case matches of [_,_,
4.691 + Matches
4.692 + (["triangular", "2x2", "linear", "system"],
4.693 + {Find = [Correct "solution L"],
4.694 + With = [],
4.695 + Given =
4.696 + [Correct
4.697 + "equalities [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]",
4.698 + Correct "solveForVars [c, c_2]"],
4.699 + Where =
4.700 + [Correct
4.701 + "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]",
4.702 + Correct
4.703 + "[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]"],
4.704 + Relate = []})] => ()
4.705 + | _ => raise error "eqsystem.sml refine ['triangular','2x2'...]";
4.706 +
4.707 +
4.708 +(*WN051014----------------------------------------------------------------
4.709 + the above 'val matches = refine fmz ["linear","system"]'
4.710 + didn't work anymore; we investigated in these steps:*)
4.711 +val fmz = ["equalities [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]",
4.712 + "solveForVars [c, c_2]", "solution L"];
4.713 +val matches = refine fmz ["triangular", "2x2", "linear","system"];
4.714 +(*... resulted in
4.715 + False "[c, c_2] from_ [c, c_2] occur_exactly_in nth_ 2\n
4.716 + [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]"]*)
4.717 +
4.718 +val t = str2term"[c, c_2] from_ [c, c_2] occur_exactly_in nth_ 2\
4.719 + \[c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]";
4.720 +trace_rewrite:=true;
4.721 +val Some (t',_) = rewrite_set_ thy false prls_triangular t;
4.722 +(*found:...
4.723 +## try thm: nth_Cons_
4.724 +### eval asms: 1 < 2 + - 1
4.725 +==> nth_ (2 + - 1) [L * c + c_2 = q_0 * L ^^^ 2 / 2] =
4.726 + nth_ (2 + - 1 + - 1) []
4.727 +#### rls: erls_prls_triangular on: 1 < 2 + - 1
4.728 +##### try calc: op <'
4.729 +### asms accepted: ["1 < 2 + - 1"] stored: ["1 < 2 + -1"]
4.730 +
4.731 +... i.e Calc ("op +", eval_binop "#add_") was missing in erls_prls_triangular*)
4.732 +trace_rewrite:=false;
4.733 +(*WN051014------------------------------------------------------------------*)
4.734 +
4.735 +"----- relaxed preconditions for triangular system";
4.736 +val fmz = ["equalities [L * q_0 = c, \
4.737 + \ 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2,\
4.738 + \ 0 = c_4, \
4.739 + \ 0 = c_3]",
4.740 + "solveForVars [c, c_2, c_3, c_4]", "solution L"];
4.741 +val matches = refine fmz ["linear","system"];
4.742 +(* trace_rewrite := true;
4.743 + trace_rewrite := false;
4.744 + *)
4.745 +(*print_depth 6; matches; print_depth 3;*)
4.746 +case matches of
4.747 + [Matches (["linear", "system"], _),
4.748 + NoMatch (["2x2", "linear", "system"], _),
4.749 + NoMatch (["3x3", "linear", "system"], _),
4.750 + Matches (["4x4", "linear", "system"], _),
4.751 + NoMatch (["triangular", "4x4", "linear", "system"], _),
4.752 + Matches (["normalize", "4x4", "linear", "system"], _)] => ()
4.753 + | _ => raise error "eqsystem.sml: refine relaxed triangular sys NoMatch";
4.754 +(*WN060914 does NOT match, because 3rd and 4th equ are not ordered*)
4.755 +
4.756 +val fmz = ["equalities [L * q_0 = c, \
4.757 + \ 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2,\
4.758 + \ 0 = c_3, \
4.759 + \ 0 = c_4]",
4.760 + "solveForVars [c, c_2, c_3, c_4]", "solution L"];
4.761 +val matches = refine fmz ["triangular", "4x4", "linear","system"];
4.762 +(* print_depth 11; matches; print_depth 3;
4.763 + *)
4.764 +case matches of
4.765 + [Matches (["triangular", "4x4", "linear", "system"], _)] => ()
4.766 + | _ => raise error "eqsystem.sml: refine relaxed triangular sys Matches";
4.767 +val matches = refine fmz ["linear","system"];
4.768 +
4.769 +
4.770 +"----------- refine [2x2,linear,system] search error--------------";
4.771 +"----------- refine [2x2,linear,system] search error--------------";
4.772 +"----------- refine [2x2,linear,system] search error--------------";
4.773 +(*didn't go into ["2x2", "linear", "system"];
4.774 + we investigated in these steps:*)
4.775 +val fmz = ["equalities [0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2,\
4.776 + \0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2]",
4.777 + "solveForVars [c, c_2]", "solution L"];
4.778 +trace_rewrite:=true;
4.779 +val matches = refine fmz ["2x2", "linear","system"];
4.780 +trace_rewrite:=false;
4.781 +print_depth 11; matches; print_depth 3;
4.782 +(*brought: 'False "length_ es_ = 2"'*)
4.783 +
4.784 +(*-----fun refin' (pblRD:pblRD) fmz pbls ((Ptyp (pI,[py],[])):pbt ptyp) =
4.785 +(* val ((pblRD:pblRD), fmz, pbls, ((Ptyp (pI,[py],[])):pbt ptyp)) =
4.786 + (rev ["linear","system"], fmz, [(*match list*)],
4.787 + ((Ptyp ("2x2",[get_pbt ["2x2","linear","system"]],[])):pbt ptyp));
4.788 + *)
4.789 +> show_types:=true; term2str (hd where_); show_types:=false;
4.790 +val it = "length_ (es_::real list) = (2::real)" : string
4.791 +
4.792 +=========================================================================\
4.793 +-------fun prep_pbt
4.794 +(* val (thy, (pblID, dsc_dats: (string * (string list)) list,
4.795 + ev:rls, ca: string option, metIDs:metID list)) =
4.796 + (EqSystem.thy, (["system"],
4.797 + [("#Given" ,["equalities es_", "solveForVars vs_"]),
4.798 + ("#Find" ,["solution ss___"](*___ is copy-named*))
4.799 + ],
4.800 + append_rls "e_rls" e_rls [(*for preds in where_*)],
4.801 + Some "solveSystem es_ vs_",
4.802 + []));
4.803 + *)
4.804 +> val [("#Given", [equalities_es_, "solveForVars vs_"])] = gi;
4.805 +val equalities_es_ = "equalities es_" : string
4.806 +> val (dd, ii) = (split_did o term_of o the o (parse thy)) equalities_es_;
4.807 +> show_types:=true; term2str ii; show_types:=false;
4.808 +val it = "es_::bool list" : string
4.809 +~~~~~~~~~~~~~~~^^^^^^^^^ OK~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
4.810 +
4.811 +> val {where_,...} = get_pbt ["2x2", "linear","system"];
4.812 +> show_types:=true; term2str (hd where_); show_types:=false;
4.813 +
4.814 +=========================================================================/
4.815 +
4.816 +
4.817 +
4.818 +-----fun refin' ff:
4.819 +> (writeln o (itms2str Isac.thy)) itms;
4.820 +[
4.821 +(1 ,[1] ,true ,#Given ,Cor equalities
4.822 + [0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2,
4.823 + 0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2] ,(es_, [[0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2,
4.824 + 0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2]])),
4.825 +(2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(vs_, [[c, c_2]])),
4.826 +(3 ,[1] ,true ,#Find ,Cor solution L ,(ss___, [L]))]
4.827 +
4.828 +> (writeln o pres2str) pre';
4.829 +[
4.830 +(false, length_ es_ = 2),
4.831 +(true, length_ [c, c_2] = 2)]
4.832 +
4.833 +----- fun match_oris':
4.834 +> (writeln o (itms2str Isac.thy)) itms;
4.835 +> (writeln o pres2str) pre';
4.836 +..as in refin'
4.837 +
4.838 +----- fun check_preconds'
4.839 +> (writeln o env2str) env;
4.840 +["
4.841 +(es_, [0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2,
4.842 + 0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2])","
4.843 +(vs_, [c, c_2])","
4.844 +(ss___, L)"]
4.845 +
4.846 +> val es_ = (fst o hd) env;
4.847 +val es_ = Free ("es_", "bool List.list") : Term.term
4.848 +
4.849 +> val pre1 = hd pres;
4.850 +atomty pre1;
4.851 +***
4.852 +*** Const (op =, [real, real] => bool)
4.853 +*** . Const (ListG.length_, real list => real)
4.854 +*** . . Free (es_, real list)
4.855 +~~~~~~~~~~~~~~~~~~~^^^^^^^^^ should be bool list~~~~~~~~~~~~~~~~~~~
4.856 +*** . Free (2, real)
4.857 +***
4.858 +
4.859 +THE REASON WAS A non-type-constrained variable IN #WHERE OF PROBLEM
4.860 +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
4.861 +*)
4.862 +
4.863 +
4.864 +"----------- me [EqSystem,normalize,2x2] -------------------------";
4.865 +"----------- me [EqSystem,normalize,2x2] -------------------------";
4.866 +"----------- me [EqSystem,normalize,2x2] -------------------------";
4.867 +val fmz = ["equalities [0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2,\
4.868 + \0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2]",
4.869 + "solveForVars [c, c_2]", "solution L"];
4.870 +val (dI',pI',mI') =
4.871 + ("Biegelinie.thy",["normalize", "2x2", "linear", "system"],
4.872 + ["EqSystem","normalize","2x2"]);
4.873 +val p = e_pos'; val c = [];
4.874 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
4.875 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.876 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.877 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.878 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.879 +case nxt of ("Specify_Method",_) => ()
4.880 + | _ => raise error "eqsystem.sml [EqSystem,normalize,2x2] specify";
4.881 +
4.882 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.883 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
4.884 +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*);
4.885 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
4.886 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
4.887 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
4.888 +case nxt of
4.889 + (_, Subproblem ("Biegelinie.thy", ["triangular", "2x2", "linear",_])) => ()
4.890 + | _ => raise error "eqsystem.sml me [EqSystem,normalize,2x2] SubProblem";
4.891 +
4.892 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.893 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.894 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.895 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.896 +case nxt of
4.897 + (_, Specify_Method ["EqSystem", "top_down_substitution", "2x2"]) => ()
4.898 + | _ => raise error "eqsystem.sml me [EqSys...2x2] top_down_substitution";
4.899 +
4.900 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.901 +val PblObj {probl,...} = get_obj I pt [5];(writeln o(itms2str Isac.thy)) probl;
4.902 +(*[
4.903 +(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]])),
4.904 +(2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(vs_, [[c, c_2]])),
4.905 +(3 ,[1] ,true ,#Find ,Cor solution ss___ ,(ss___, [ss___]))]
4.906 +*)
4.907 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
4.908 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
4.909 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
4.910 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
4.911 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
4.912 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
4.913 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
4.914 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
4.915 +case nxt of
4.916 + (_, Check_Postcond ["triangular", "2x2", "linear", "system"]) => ()
4.917 + | _ => raise error "eqsystem.sml me Subpbl .[EqSys...2x2] finished";
4.918 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
4.919 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
4.920 +if f2str f = "[c = L * q_0 / 2, c_2 = 0]" then ()
4.921 +else raise error "eqsystem.sml me [EqSys...2x2] finished f2str f";
4.922 +case nxt of
4.923 + (_, End_Proof') => ()
4.924 + | _ => raise error "eqsystem.sml me [EqSys...2x2] finished End_Proof'";
4.925 +
4.926 +
4.927 +"----------- me [linear,system] ..normalize..top_down_sub..-------";
4.928 +"----------- me [linear,system] ..normalize..top_down_sub..-------";
4.929 +"----------- me [linear,system] ..normalize..top_down_sub..-------";
4.930 +val fmz =
4.931 + ["equalities\
4.932 + \[0 = c_2 + c * 0 + 1 / EI * (L * q_0 / 12 * 0 ^^^ 3 + \
4.933 + \ -1 * q_0 / 24 * 0 ^^^ 4),\
4.934 + \ 0 = c_2 + c * L + 1 / EI * (L * q_0 / 12 * L ^^^ 3 + \
4.935 + \ -1 * q_0 / 24 * L ^^^ 4)]",
4.936 + "solveForVars [c, c_2]", "solution L"];
4.937 +val (dI',pI',mI') =
4.938 + ("Biegelinie.thy",["linear", "system"], ["no_met"]);
4.939 +val p = e_pos'; val c = [];
4.940 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
4.941 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.942 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.943 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.944 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.945 +case nxt of (_,Specify_Method ["EqSystem", "normalize", "2x2"]) => ()
4.946 + | _ => raise error "eqsystem.sml [linear,system] specify b";
4.947 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.948 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
4.949 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
4.950 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
4.951 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
4.952 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
4.953 +if f2str f =
4.954 +"[c_2 = 0, L * c + c_2 = -1 * q_0 * L ^^^ 4 / (24 * EI)]"
4.955 +then () else raise error "eqsystem.sml me simpl. before SubProblem b";
4.956 +case nxt of
4.957 + (_, Subproblem ("Biegelinie.thy", ["triangular", "2x2", "linear",_])) => ()
4.958 + | _ => raise error "eqsystem.sml me [linear,system] SubProblem b";
4.959 +
4.960 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.961 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.962 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.963 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.964 +case nxt of
4.965 + (_, Specify_Method ["EqSystem", "top_down_substitution", "2x2"]) => ()
4.966 + | _ => raise error "eqsystem.sml me [EqSys...2x2] top_down_substitution b";
4.967 +
4.968 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.969 +val PblObj {probl,...} = get_obj I pt [5];(writeln o(itms2str Isac.thy)) probl;
4.970 +(*[
4.971 +(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]])),
4.972 +(2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(vs_, [[c, c_2]])),
4.973 +(3 ,[1] ,true ,#Find ,Cor solution ss___ ,(ss___, [ss___]))]
4.974 +*)
4.975 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
4.976 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
4.977 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
4.978 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
4.979 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
4.980 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
4.981 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
4.982 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
4.983 +case nxt of
4.984 + (_, Check_Postcond ["triangular", "2x2", "linear", "system"]) => ()
4.985 + | _ => raise error "eqsystem.sml me Subpbl .[EqSys...2x2] finished b";
4.986 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
4.987 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
4.988 +if f2str f =
4.989 +"[c = -1 * q_0 * L ^^^ 4 / (24 * EI * L), c_2 = 0]"
4.990 +then () else raise error "eqsystem.sml me [EqSys...2x2] finished f2str f b";
4.991 +case nxt of
4.992 + (_, End_Proof') => ()
4.993 + | _ => raise error "eqsystem.sml me [EqSys...2x2] finished End_Proof'" b;
4.994 +
4.995 +
4.996 +"----------- all systems from Biegelinie -------------------------";
4.997 +"----------- all systems from Biegelinie -------------------------";
4.998 +"----------- all systems from Biegelinie -------------------------";
4.999 +val subst = [(str2term "bdv_1", str2term "c"),
4.1000 + (str2term "bdv_2", str2term "c_2"),
4.1001 + (str2term "bdv_3", str2term "c_3"),
4.1002 + (str2term "bdv_4", str2term "c_4")];
4.1003 +"------- Bsp 7.27";
4.1004 +states:=[];
4.1005 +CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
4.1006 + "Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]",
4.1007 + "FunktionsVariable x"],
4.1008 + ("Biegelinie.thy", ["Biegelinien"],
4.1009 + ["IntegrierenUndKonstanteBestimmen2"]))];
4.1010 +moveActiveRoot 1;
4.1011 +(*
4.1012 +trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;
4.1013 +##7.27## ordered substs
4.1014 + c_4 c_2
4.1015 +c c_2 c_3 c_4 c c_2 1->2: c
4.1016 + c_2 c_4
4.1017 +c c_2 c c_2 c_3 c_4 [2':c, 1:c_2, 3:c_4] -> 4:c_3*)
4.1018 +val t = str2term"[0 = c_4, \
4.1019 +\ 0 = c_4 + L * c_3 +(12 * L ^^^ 2 * c_2 + 4 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) / (-24 * EI), \
4.1020 +\ 0 = c_2, \
4.1021 +\ 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2]";
4.1022 +val Some (t',_) = rewrite_set_ thy false isolate_bdvs_4x4 t;
4.1023 +term2str t';
4.1024 +"[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]";
4.1025 +
4.1026 +
4.1027 +"----- 7.27 go through the rewrites in met_eqsys_norm_4x4";
4.1028 +val t = str2term "0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2";
4.1029 +val None = rewrite_set_ thy false norm_Rational t;
4.1030 +val Some (t,_) =
4.1031 + rewrite_set_inst_ thy false subst simplify_System_parenthesized t;
4.1032 +term2str t = "0 = -1 * q_0 * L ^^^ 2 / 2 + (L * c + c_2)";
4.1033 +"--- isolate_bdvs_4x4";
4.1034 +(*
4.1035 +val Some (t,_) = rewrite_set_inst_ thy false subst isolate_bdvs_4x4 t;
4.1036 +term2str t;
4.1037 +val Some (t,_) = rewrite_set_inst_ thy false subst simplify_System t;
4.1038 +term2str t;
4.1039 +val Some (t,_) = rewrite_set_ thy false order_system t;
4.1040 +term2str t;
4.1041 +*)
4.1042 +
4.1043 +"------- Bsp 7.28 ---------------vvvvvvvvvvvvv Momentenlinie postponed";
4.1044 +states:=[];
4.1045 +CalcTree [(["Traegerlaenge L","Momentenlinie (-q_0 / L * x^3 / 6)",
4.1046 + "Biegelinie y",
4.1047 + "Randbedingungen [y L = 0, y' L = 0]",
4.1048 + "FunktionsVariable x"],
4.1049 + ("Biegelinie.thy", ["vonMomentenlinieZu","Biegelinien"],
4.1050 + ["Biegelinien", "AusMomentenlinie"]))];
4.1051 +moveActiveRoot 1;
4.1052 +(*
4.1053 +trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;
4.1054 +*)
4.1055 +
4.1056 +"------- Bsp 7.69";
4.1057 +states:=[];
4.1058 +CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
4.1059 + "Randbedingungen [y 0 = 0, y L = 0, y' 0 = 0, y' L = 0]",
4.1060 + "FunktionsVariable x"],
4.1061 + ("Biegelinie.thy", ["Biegelinien"],
4.1062 + ["IntegrierenUndKonstanteBestimmen2"] ))];
4.1063 +moveActiveRoot 1;
4.1064 +(*
4.1065 +trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;
4.1066 +##7.69## ordered subst 2x2
4.1067 + c_4 c_3
4.1068 +c c_2 c_3 c_4 c c_2 c_3 1:c_3 -> 2:c c_2 2: c c_2
4.1069 + c_3 c_4
4.1070 +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*)
4.1071 +val t = str2term"[0 = c_4 + 0 / (-1 * EI), \
4.1072 +\ 0 = c_4 + L * c_3 + (12 * L ^^^ 2 * c_2 + 4 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) / (-24 * EI), \
4.1073 +\ 0 = c_3 + 0 / (-1 * EI), \
4.1074 +\ 0 = c_3 + (6 * L * c_2 + 3 * L ^^^ 2 * c + -1 * L ^^^ 3 * q_0) / (-6 * EI)]";
4.1075 +
4.1076 +"------- Bsp 7.70";
4.1077 +states:=[];
4.1078 +CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
4.1079 + "Randbedingungen [Q 0 = q_0 * L, M_b L = 0, y 0 = 0, y' 0 = 0]",
4.1080 + "FunktionsVariable x"],
4.1081 + ("Biegelinie.thy", ["Biegelinien"],
4.1082 + ["IntegrierenUndKonstanteBestimmen2"] ))];
4.1083 +moveActiveRoot 1;
4.1084 +(*
4.1085 +trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;
4.1086 +##7.70## |subst
4.1087 +c |
4.1088 +c c_2 |1:c -> 2:c_2
4.1089 + c_3 |
4.1090 + c_4 | GOON test methods @@@@@@@@@@@@@@@@@@@@@@@@@@@*)
4.1091 +
4.1092 +"----- 7.70 go through the rewrites in met_eqsys_norm_4x4";
4.1093 +val t = str2term"[L * q_0 = c, \
4.1094 + \ 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2,\
4.1095 + \ 0 = c_4, \
4.1096 + \ 0 = c_3]";
4.1097 +val Some (t,_) =
4.1098 + rewrite_ thy e_rew_ord e_rls false (num_str commute_0_equality) t;
4.1099 +val Some (t,_) =
4.1100 + rewrite_ thy e_rew_ord e_rls false (num_str commute_0_equality) t;
4.1101 +val Some (t,_) =
4.1102 + rewrite_ thy e_rew_ord e_rls false (num_str commute_0_equality) t;
4.1103 +term2str t =
4.1104 + "[L * q_0 = c, (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2 = 0, c_4 = 0,\n c_3 = 0]";
4.1105 +val Some (t,_) =
4.1106 + rewrite_set_inst_ thy false subst simplify_System_parenthesized t;
4.1107 +term2str t =
4.1108 +"[L * q_0 = c, -1 * q_0 * L ^^^ 2 / 2 + (L * c + c_2) = 0, c_4 = 0, c_3 = 0]";
4.1109 +val Some (t,_) = rewrite_set_inst_ thy false subst isolate_bdvs_4x4 t;
4.1110 +term2str t =
4.1111 + "[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]";
4.1112 +val Some (t,_) =
4.1113 + rewrite_set_inst_ thy false subst simplify_System_parenthesized t;
4.1114 +term2str t ="[c = L * q_0, L * c + c_2 = q_0 * L ^^^ 2 / 2, c_4 = 0, c_3 = 0]";
4.1115 +val Some (t,_) = rewrite_set_ thy false order_system t;
4.1116 +if term2str t ="[c = L * q_0, L * c + c_2 = q_0 * L ^^^ 2 / 2, c_3 = 0, c_4 = 0]" then ()
4.1117 +else raise error "eqsystem.sml: exp 7.70 normalize 4x4 by rewrite changed";
4.1118 +
4.1119 +
4.1120 +"----- 7.70 with met normalize: ";
4.1121 +val fmz = ["equalities \
4.1122 + \[L * q_0 = c, \
4.1123 + \ 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2,\
4.1124 + \ 0 = c_4, \
4.1125 + \ 0 = c_3]",
4.1126 + "solveForVars [c, c_2, c_3, c_4]", "solution L"];
4.1127 +val (dI',pI',mI') =
4.1128 + ("Biegelinie.thy",["linear", "system"],["no_met"]);
4.1129 +val p = e_pos'; val c = [];
4.1130 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
4.1131 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.1132 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.1133 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.1134 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.1135 +case nxt of (_,Apply_Method ["EqSystem", "normalize", "4x4"]) => ()
4.1136 + | _ => raise error "eqsystem.sml [EqSystem,normalize,4x4] specify";
4.1137 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
4.1138 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
4.1139 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
4.1140 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
4.1141 +
4.1142 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
4.1143 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
4.1144 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
4.1145 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
4.1146 +if f2str f ="[c = L * q_0, L * c + c_2 = q_0 * L ^^^ 2 / 2, c_3 = 0, c_4 = 0]"
4.1147 +then () else raise error "eqsystem.sml: exp 7.70 normalize 4x4 by met changed";
4.1148 +
4.1149 +"----- 7.70 with met top_down_: ";
4.1150 +"--- scr [EqSystem,top_down_substitution,4x4] -- a saved trial";
4.1151 +(*---vvv-this script failed with if ?!?-------------------------------------*)
4.1152 +val str =
4.1153 +"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
4.1154 +\ (let e1_ = hd es_; \
4.1155 +\ v1_ = hd vs_; \
4.1156 +\ xxx = if lhs e1_ =!= v1_ \
4.1157 +\ then 0=0 \
4.1158 +\ else let e1_ = Take e1_; \
4.1159 +\ e1_ = (Rewrite_Set_Inst [(bdv_1, hd vs_), \
4.1160 +\ (bdv_2, hd (tl vs_))] \
4.1161 +\ isolate_bdvs False) e1_; \
4.1162 +\ e2_ = Take (hd (tl es_)); \
4.1163 +\ e2_ = (Substitute [e1__]) e2_ \
4.1164 +\ in [e1_, e2_])";
4.1165 +(*val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;*)
4.1166 +val str =
4.1167 +"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
4.1168 +\ (let e1_ = hd es_; \
4.1169 +\ v1_ = hd vs_; \
4.1170 +\ e2_ = Take (hd (tl es_)); \
4.1171 +\ e2_ = (Substitute [e1__]) e2_ \
4.1172 +\ in [e1_, e2_])";
4.1173 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
4.1174 +(*---^^^-OK-----------------------------------------------------------------*)
4.1175 +(*---vvv-NOT ok-------------------------------------------------------------*)
4.1176 +val str =
4.1177 +"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
4.1178 +\ (let e1_ = hd es_; \
4.1179 +\ v1_ = hd vs_; \
4.1180 +\ xxx = if ((lhs e1_) =!= v1_) then 1 else 2; \
4.1181 +\ e2_ = Take (hd (tl es_)); \
4.1182 +\ e2_ = (Substitute [e1__]) e2_ \
4.1183 +\ in [e1_, e2_])";
4.1184 +(*val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;*)
4.1185 +val str = "if lhs e1_ =!= v1_ then 1 else 2";
4.1186 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
4.1187 +
4.1188 +val str = "let xxx = (if lhs e1_ =!= v1_ then 1 else 2) in xxx";
4.1189 +(*val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;*)
4.1190 +atomty sc; term2str sc;
4.1191 +
4.1192 +"--- scr [EqSystem,top_down_substitution,4x4] -- adapted only to 7.70";
4.1193 +val str =
4.1194 +"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
4.1195 +\ (let e2__ = Take (hd (tl es_)); \
4.1196 +\ e2__ = ((Substitute [e1__]) @@ \
4.1197 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
4.1198 +\ simplify_System_parenthesized False)) @@ \
4.1199 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
4.1200 +\ isolate_bdvs False)) @@ \
4.1201 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
4.1202 +\ simplify_System False))) e2__;\
4.1203 +\ es__ = Take [e1__, e2__] \
4.1204 +\ in (Try (Rewrite_Set order_system False)) es__)"
4.1205 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
4.1206 +val str =
4.1207 +"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
4.1208 +\ (let e2__ = Take (nth_ 2 es_); \
4.1209 +\ e2__ = ((Substitute [e1__]) @@ \
4.1210 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
4.1211 +\ simplify_System_parenthesized False)) @@ \
4.1212 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
4.1213 +\ isolate_bdvs False)) @@ \
4.1214 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
4.1215 +\ simplify_System False))) e2__;\
4.1216 +\ es__ = Take [e1__, e2__] \
4.1217 +\ in (Try (Rewrite_Set order_system False)) es__)"
4.1218 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
4.1219 +val str =
4.1220 +"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
4.1221 +\ (let e2__ = Take (nth_ 2 es_); \
4.1222 +\ e2__ = ((Substitute [e1__]) @@ \
4.1223 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, nth_ 2 vs_)] \
4.1224 +\ simplify_System_parenthesized False)) @@ \
4.1225 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, nth_ 2 vs_)]\
4.1226 +\ isolate_bdvs False)) @@ \
4.1227 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, nth_ 2 vs_)]\
4.1228 +\ simplify_System False))) e2__;\
4.1229 +\ es__ = Take [e1__, e2__] \
4.1230 +\ in (Try (Rewrite_Set order_system False)) es__)"
4.1231 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
4.1232 +val str =
4.1233 +"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
4.1234 +\ (let e2__ = Take (nth_ 2 es_); \
4.1235 +\ e2__ = ((Substitute [e1__]) @@ \
4.1236 +\ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 vs_),(bdv_2,nth_ 2 vs_),\
4.1237 +\ (bdv_3,nth_ 3 vs_),(bdv_4,nth_ 4 vs_)]\
4.1238 +\ simplify_System_parenthesized False)) @@ \
4.1239 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, nth_ 2 vs_)] \
4.1240 +\ isolate_bdvs False)) @@ \
4.1241 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, nth_ 2 vs_)] \
4.1242 +\ norm_Rational False))) e2__; \
4.1243 +\ es__ = Take [e1__, e2__] \
4.1244 +\ in [])"
4.1245 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
4.1246 +val str =
4.1247 +"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
4.1248 +\ (let e2_ = Take (nth_ 2 es_); \
4.1249 +\ e2_ = ((Substitute [e1_]) @@ \
4.1250 +\ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 vs_),(bdv_2,nth_ 2 vs_),\
4.1251 +\ (bdv_3,nth_ 3 vs_),(bdv_4,nth_ 4 vs_)]\
4.1252 +\ simplify_System_parenthesized False)) @@ \
4.1253 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, nth_ 2 vs_)] \
4.1254 +\ isolate_bdvs False)) @@ \
4.1255 +\ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, nth_ 2 vs_)] \
4.1256 +\ norm_Rational False))) e2_; \
4.1257 +\ es_ = Take [e1_, e2_] \
4.1258 +\ in [e1_, e2_,e3_, e4_])"
4.1259 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
4.1260 +val str =
4.1261 +"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
4.1262 +\ (let e2_ = Take (nth_ 2 es_); \
4.1263 +\ e2_ = ((Substitute [e1_]) @@ \
4.1264 +\ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 vs_),(bdv_2,nth_ 2 vs_),\
4.1265 +\ (bdv_3,nth_ 3 vs_),(bdv_4,nth_ 4 vs_)]\
4.1266 +\ simplify_System_parenthesized False)) @@ \
4.1267 +\ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 vs_),(bdv_2,nth_ 2 vs_),\
4.1268 +\ (bdv_3,nth_ 3 vs_),(bdv_4,nth_ 4 vs_)]\
4.1269 +\ isolate_bdvs False)) @@ \
4.1270 +\ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 vs_),(bdv_2,nth_ 2 vs_),\
4.1271 +\ (bdv_3,nth_ 3 vs_),(bdv_4,nth_ 4 vs_)]\
4.1272 +\ norm_Rational False))) e2_; \
4.1273 +\ es_ = Take [e1_, e2_] \
4.1274 +\ in [e1_, e2_,e3_, e4_])"
4.1275 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
4.1276 +(*---^^^-OK-----------------------------------------------------------------*)
4.1277 +val str =
4.1278 +"Script SolveSystemScript (es_::bool list) (vs_::real list) = \
4.1279 +\ (let e2_ = Take (nth_ 2 es_); \
4.1280 +\ e2_ = ((Substitute [e1_]) @@ \
4.1281 +\ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 vs_),(bdv_2,nth_ 2 vs_),\
4.1282 +\ (bdv_3,nth_ 3 vs_),(bdv_4,nth_ 4 vs_)]\
4.1283 +\ simplify_System_parenthesized False)) @@ \
4.1284 +\ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 vs_),(bdv_2,nth_ 2 vs_),\
4.1285 +\ (bdv_3,nth_ 3 vs_),(bdv_4,nth_ 4 vs_)]\
4.1286 +\ isolate_bdvs False)) @@ \
4.1287 +\ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 vs_),(bdv_2,nth_ 2 vs_),\
4.1288 +\ (bdv_3,nth_ 3 vs_),(bdv_4,nth_ 4 vs_)]\
4.1289 +\ norm_Rational False))) e2_ \
4.1290 +\ in [e1_, e2_, nth_ 3 es_, nth_ 4 es_])"
4.1291 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
4.1292 +(*---vvv-NOT ok-------------------------------------------------------------*)
4.1293 +atomty sc; term2str sc;
4.1294 +
4.1295 +
4.1296 +"----- 7.70 with met top_down_: me";
4.1297 +val fmz = ["equalities \
4.1298 + \[c = L * q_0, L * c + c_2 = q_0 * L ^^^ 2 / 2, c_3 = 0, c_4 = 0]",
4.1299 + "solveForVars [c, c_2, c_3, c_4]", "solution L"];
4.1300 +val (dI',pI',mI') =
4.1301 + ("Biegelinie.thy",["linear", "system"],["no_met"]);
4.1302 +val p = e_pos'; val c = [];
4.1303 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
4.1304 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.1305 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.1306 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.1307 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.1308 +case nxt of (_,Apply_Method ["EqSystem", "top_down_substitution", "4x4"]) => ()
4.1309 + | _ => raise error "eqsystem.sml [EqSystem,top_down_,4x4] specify";
4.1310 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
4.1311 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
4.1312 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
4.1313 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
4.1314 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
4.1315 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
4.1316 +if nxt = ("End_Proof'", End_Proof') andalso
4.1317 + f2str f = "[c = L * q_0, c_2 = -1 * L ^^^ 2 * q_0 / 2, c_3 = 0, c_4 = 0]"
4.1318 +then () else raise error "eqsystem.sml: 7.70 with met top_down_: me";
4.1319 +
4.1320 +
4.1321 +"------- Bsp 7.71";
4.1322 +states:=[];
4.1323 +CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
4.1324 + "Randbedingungen [M_b L = 0, y 0 = 0, y L = 0, y' 0 = 0]",
4.1325 + "FunktionsVariable x"],
4.1326 + ("Biegelinie.thy", ["Biegelinien"],
4.1327 + ["IntegrierenUndKonstanteBestimmen2"] ))];
4.1328 +moveActiveRoot 1;
4.1329 +(*
4.1330 +trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;
4.1331 +##7.71## |ordered |subst.singles (recurs) |2x2 |diagonal
4.1332 +c c_2 |c c_2 |1' |1': c c_2 |
4.1333 + c_4 | c_3 |2:c_3 -> 4' :c c_2 c_4 | |
4.1334 +c c_2 c_3 c_4 | c_4 |3' | |
4.1335 + c_3 |c c_2 c_3 c_4 |3:c_4 -> 4'':c c_2 |4'':c c_2 | *)
4.1336 +val t = str2term"[0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2, \
4.1337 +\ 0 = c_4 + 0 / (-1 * EI), \
4.1338 +\ 0 = c_4 + L * c_3 +(12 * L ^^^ 2 * c_2 + 4 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) /(-24 * EI),\
4.1339 +\ 0 = c_3 + 0 / (-1 * EI)]";
4.1340 +
4.1341 +"------- Bsp 7.72a ---------------vvvvvvvvvvvvv Momentenlinie postponed";
4.1342 +states:=[];
4.1343 +CalcTree [(["Traegerlaenge L",
4.1344 + "Momentenlinie ((q_0 * L)/ 6 * x - q_0 /(6 * L) * x^3)",
4.1345 + "Biegelinie y",
4.1346 + "Randbedingungen [y 0 = 0, y L = 0]",
4.1347 + "FunktionsVariable x"],
4.1348 + ("Biegelinie.thy", ["vonMomentenlinieZu","Biegelinien"],
4.1349 + ["Biegelinien", "AusMomentenlinie"]))];
4.1350 +moveActiveRoot 1;
4.1351 +(*
4.1352 +trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;
4.1353 +*)
4.1354 +
4.1355 +"------- Bsp 7.72b";
4.1356 +states:=[];
4.1357 +CalcTree [(["Traegerlaenge L","Streckenlast (q_0 / L * x)","Biegelinie y",
4.1358 + "Randbedingungen [M_b 0 = 0, M_b L = 0, y 0 = 0, y L = 0]",
4.1359 + "FunktionsVariable x"],
4.1360 + ("Biegelinie.thy", ["Biegelinien"],
4.1361 + ["IntegrierenUndKonstanteBestimmen2"] ))];
4.1362 +moveActiveRoot 1;
4.1363 +(*
4.1364 +trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;
4.1365 +##7.72b## |ord. |subst.singles |ord.triang.
4.1366 + c_2 | | |c_2
4.1367 +c c_2 | |1:c_2 -> 2':c |c_2 c
4.1368 + c_4 | | |
4.1369 +c c_2 c_3 c_4 | |3:c_4 -> 4':c c_2 c_3 |c_2 c c_3*)
4.1370 +val t = str2term"[0 = c_2, \
4.1371 +\ 0 = (6 * c_2 + 6 * L * c + -1 * L ^^^ 2 * q_0) / 6, \
4.1372 +\ 0 = c_4 + 0 / (-1 * EI), \
4.1373 +\ 0 = c_4 + L * c_3 + (60 * L ^^^ 2 * c_2 + 20 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) / (-120 * EI)]";
4.1374 +
4.1375 +"------- Bsp 7.73 ---------------vvvvvvvvvvvvv Momentenlinie postponed";
4.1376 +states:=[];
4.1377 +CalcTree [(["Traegerlaenge L","Momentenlinie ???",(*description unclear*)
4.1378 + "Biegelinie y",
4.1379 + "Randbedingungen [y L = 0, y' L = 0]",
4.1380 + "FunktionsVariable x"],
4.1381 + ("Biegelinie.thy", ["vonMomentenlinieZu","Biegelinien"],
4.1382 + ["Biegelinien", "AusMomentenlinie"]))];
4.1383 +moveActiveRoot 1;
4.1384 +(*
4.1385 +trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;
4.1386 +*)
4.1387 +
4.1388 +
4.1389 +"----------- 4x4 systems from Biegelinie -------------------------";
4.1390 +"----------- 4x4 systems from Biegelinie -------------------------";
4.1391 +"----------- 4x4 systems from Biegelinie -------------------------";
4.1392 +(*GOON replace this test with 7.70 @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@2*)
4.1393 +"----- Bsp 7.27";
4.1394 +val fmz = ["equalities \
4.1395 + \[0 = c_4, \
4.1396 + \ 0 = c_4 + L * c_3 +(12 * L ^^^ 2 * c_2 + 4 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) / (-24 * EI), \
4.1397 + \ 0 = c_2, \
4.1398 + \ 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2]",
4.1399 + "solveForVars [c, c_2, c_3, c_4]", "solution L"];
4.1400 +val (dI',pI',mI') =
4.1401 + ("Biegelinie.thy",["normalize", "4x4", "linear", "system"],
4.1402 + ["EqSystem","normalize","4x4"]);
4.1403 +val p = e_pos'; val c = [];
4.1404 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
4.1405 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.1406 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.1407 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.1408 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.1409 +"------------------------------------------- Apply_Method...";
4.1410 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
4.1411 +"[0 = c_4, \
4.1412 +\ 0 = c_4 + L * c_3 +\n (12 * L ^^^ 2 * c_2 + 4 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) / (-24 * EI), \
4.1413 +\ 0 = c_2, \
4.1414 +\ 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2]";
4.1415 +"------------------------------------------- simplify_System_parenthesized...";
4.1416 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
4.1417 +"[0 = c_4, \
4.1418 +\ 0 = -1 * q_0 * L ^^^ 4 / (-24 * EI) + \
4.1419 +\ (4 * L ^^^ 3 * c / (-24 * EI) + \
4.1420 +\ (12 * L ^^^ 2 * c_2 / (-24 * EI) + \
4.1421 +\ (L * c_3 + c_4))), \
4.1422 +\ 0 = c_2, \
4.1423 +\ 0 = -1 * q_0 * L ^^^ 2 / 2 + (L * c + c_2)]";
4.1424 +(*? "(4 * L ^^^ 3 / (-24 * EI) * c" statt "(4 * L ^^^ 3 * c / (-24 * EI)" ?*)
4.1425 +"------------------------------------------- isolate_bdvs...";
4.1426 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
4.1427 +"[c_4 = 0,\
4.1428 +\ 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),\
4.1429 +\ c_2 = 0, \
4.1430 +\ c_2 = 0 + -1 * (-1 * q_0 * L ^^^ 2 / 2) + -1 * (L * c)]";
4.1431 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
4.1432 +
4.1433 +
4.1434 +
4.1435 +(*
4.1436 +use"../smltest/IsacKnowledge/eqsystem.sml";
4.1437 +use"eqsystem.sml";
4.1438 +*)
5.1 --- a/src/smltest/IsacKnowledge/rational.sml Mon Dec 10 14:18:49 2007 +0100
5.2 +++ b/src/smltest/IsacKnowledge/rational.sml Thu Dec 27 12:25:27 2007 +0100
5.3 @@ -1649,15 +1649,15 @@
5.4 val t = str2term "(a - (a*b+b^^^2)/(a+b))/(b+(a - b)/(1+(a+b)/(a - b))) / \
5.5 \((a - a^^^2/(a+b))/(a+(a*b)/(a - b)))";
5.6 val Some (t',_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
5.7 -(* WN050820 was OK until STOP_REW_SUB introduced -- the ONLY change !!!
5.8 - ????SK ???MG
5.9 if term2str t' =
5.10 "(2 * a ^^^ 3 + 2 * a ^^^ 2 * b) / (a ^^^ 2 * b + b ^^^ 3)"
5.11 then ()
5.12 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 51";
5.13 ------------------------------------------------------------------------*)
5.14 +
5.15 +(* TODO.new_c:WN050820 STOP_REW_SUB introduced gave ...
5.16 if term2str t' = "(a ^^^ 4 + -1 * a ^^^ 2 * b ^^^ 2) /\n(a * b * (b + (a * (a + -1 * b) + -1 * b * (a + -1 * b)) / (2 * a)) *\n (a + -1 * b))" then ()
5.17 else raise error "rational.sml: works again";
5.18 +re-outcommented with TODO.new_c: cvs before 071227, 11:50*)
5.19
5.20
5.21
6.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
6.2 +++ b/src/smltest/ME/rewtools.sml Thu Dec 27 12:25:27 2007 +0100
6.3 @@ -0,0 +1,497 @@
6.4 +(* test for sml/ME/rewtools.sml
6.5 + authors: Walther Neuper 2000, 2006
6.6 + (c) due to copyright terms
6.7 +
6.8 +use"../smltest/ME/rewtools.sml";
6.9 +use"rewtools.sml";
6.10 +*)
6.11 +
6.12 +"-----------------------------------------------------------------";
6.13 +"table of contents -----------------------------------------------";
6.14 +"-----------------------------------------------------------------";
6.15 +"----------- fun collect_isab_thys -------------------------------";
6.16 +"----------- fun thy_containing_thm ------------------------------";
6.17 +"----------- fun thy_containing_rls ------------------------------";
6.18 +"----------- fun thy_containing_cal ------------------------------";
6.19 +"----------- initContext Thy_ Integration-demo -------------------";
6.20 +"----------- initContext..Thy_, fun context_thm ------------------";
6.21 +"----------- initContext..Thy_, fun context_rls ------------------";
6.22 +"----------- checkContext..Thy_, fun context_thy -----------------";
6.23 +"----------- checkContext..Thy_, fun context_rls -----------------";
6.24 +"----------- checkContext..Thy_ on last formula ------------------";
6.25 +"----------- fun guh2theID ---------------------------------------";
6.26 +"----------- debugging on Tests/solve_linear_as_rootpbl ----------";
6.27 +"-----------------------------------------------------------------";
6.28 +"----------- fun string_of_thmI for_[.]_) ------------------------";
6.29 +"----------- (sym_real_minus_eq_cancel, (?b1 = ?a1) ..._[.]_)-----";
6.30 +"-----------------------------------------------------------------";
6.31 +"-----------------------------------------------------------------";
6.32 +
6.33 +
6.34 +
6.35 +"----------- fun collect_isab_thys -------------------------------";
6.36 +"----------- fun collect_isab_thys -------------------------------";
6.37 +"----------- fun collect_isab_thys -------------------------------";
6.38 +val thy = first_isac_thy (*def. in Script/ListG.ML*);
6.39 +val {ancestors,...} = rep_theory thy;
6.40 +print_depth 99; map string_of_thy ancestors; print_depth 3;
6.41 +length ancestors;
6.42 +val ancestors = (#ancestors o rep_theory) first_isac_thy;
6.43 +length ancestors;
6.44 +print_depth 99; map theory2theory' ancestors; print_depth 3;
6.45 +val isabthms = (flat o (map thms_of)) ancestors;
6.46 +length isabthms;
6.47 +
6.48 +val isacrules = (flat o (map (thms_of_rls o #2 o #2))) (!ruleset');
6.49 +(*thms from rulesets*)
6.50 +val isacrlsthms = ((map rep_thm_G') o flat o
6.51 + (map (thms_of_rls o #2 o #2))) (!ruleset');
6.52 +length isacrlsthms;
6.53 +(*takes a few seconds...
6.54 +val isacrlsthms = gen_distinct eq_thmI isacrlsthms;
6.55 +length isacrlsthms;
6.56 +"----- theorems used in isac's rulesets -----vvvvvvvvvvvvvvvvvvvvv";
6.57 +print_depth 99; map #1 isacrlsthms; print_depth 3;
6.58 +"----- theorems used in isac's rulesets -----^^^^^^^^^^^^^^^^^^^^^";
6.59 +...*)
6.60 +
6.61 +(!theory');
6.62 +map #2 (!theory');
6.63 +map (thms_of o #2) (!theory');
6.64 +val isacthms = (flat o (map (thms_of o #2))) (!theory');
6.65 +(*takes a few seconds...
6.66 +val rlsthmsNOTisac = gen_diff eq_thmI (isacrlsthms, isacthms);
6.67 +length rlsthmsNOTisac;
6.68 +"----- theorems from rulesets NOT def. in isac -----vvvvvvvvvvvvvv";
6.69 +print_depth 99; map #1 rlsthmsNOTisac; print_depth 3;
6.70 +"----- theorems from rulesets NOT def. in isac -----^^^^^^^^^^^^^^";
6.71 +...*)
6.72 +
6.73 +"----- for 'fun make_isab_thm_thy'";
6.74 +gen_inter eq_thmI (isacrlsthms, (thms_of (nth 1 ancestors)));
6.75 +gen_inter eq_thmI;
6.76 +curry (gen_inter eq_thmI);
6.77 +curry (gen_inter eq_thmI) isacrlsthms;
6.78 +(*takes a few seconds...
6.79 +curry (gen_inter eq_thmI) isacrlsthms (thms_of (nth 9 ancestors));
6.80 +
6.81 +val thy = (nth 52 ancestors);
6.82 +val sec = (curry (gen_inter eq_thmI) isacrlsthms o thms_of) (nth 52 ancestors);
6.83 +length (thms_of (nth 9 ancestors));
6.84 +length sec;
6.85 +...*)
6.86 +
6.87 +(*takes 1 minute...
6.88 +print_depth 99;
6.89 +map (curry (gen_inter eq_thmI) rlsthmsNOTisac o thms_of) ancestors;
6.90 +print_depth 3;
6.91 +*)
6.92 +
6.93 +(*takes some seconds...
6.94 +val isab_thm_thy = (flat o (map (make_isab_thm_thy rlsthmsNOTisac)))
6.95 + ((#ancestors o rep_theory) first_isac_thy);
6.96 +print_depth 99; isab_thm_thy; print_depth 3;
6.97 +*)
6.98 +
6.99 +
6.100 +"----------- fun thy_containing_thm ------------------------------";
6.101 +"----------- fun thy_containing_thm ------------------------------";
6.102 +"----------- fun thy_containing_thm ------------------------------";
6.103 +val (str, (thy', thy)) = ("real_diff_minus",("Root.thy", Root.thy));
6.104 +if thy_contains_thm str ("XXX",thy) then ()
6.105 +else raise error "rewtools.sml: NOT thy_contains_thm \
6.106 + \(real_diff_minus,(Root.thy,.";
6.107 +(rev (!theory'));
6.108 +dropuntil (curry op= thy');
6.109 +dropuntil ((curry op= thy') o (#1:theory' * theory -> theory'));
6.110 +val startsearch = dropuntil ((curry op= thy') o
6.111 + (#1:theory' * theory -> theory'))
6.112 + (rev (!theory'));
6.113 +if thy_containing_thm thy' str = ("IsacKnowledge", "Root.thy") then ()
6.114 +else raise error "rewtools.sml: NOT thy_containin_thm \
6.115 + \(real_diff_minus,(Root.thy,.";
6.116 +
6.117 +"----- search the same theorem somewhere further below in the list";
6.118 +if thy_contains_thm str ("XXX",Poly.thy) then ()
6.119 +else raise error "rewtools.sml: NOT thy_contains_thm \
6.120 + \(real_diff_minus,(Poly.thy,.";
6.121 +if thy_containing_thm "LinEq.thy" str = ("IsacKnowledge", "Poly.thy") then ()
6.122 +else raise error "rewtools.sml: NOT thy_containing_thm \
6.123 + \(real_diff_minus,(Poly.thy,.";
6.124 +
6.125 +"----- second test -------------------------------";
6.126 +show_thes();
6.127 +(*args vor thy_containing_thm...*)
6.128 +val (thy',str) = ("Test.thy", "radd_commute");
6.129 +val startsearch = dropuntil ((curry op= thy') o
6.130 + (#1:theory' * theory -> theory'))
6.131 + (rev (!theory'));
6.132 +length (!theory');
6.133 +length startsearch;
6.134 +if thy_containing_thm thy' str = ("IsacKnowledge", "Test.thy") then ()
6.135 +else raise error "rewtools.sml: diff.behav. in \
6.136 + \thy_containing_thm Test radd_commute";
6.137 +
6.138 +
6.139 +"----------- fun thy_containing_rls ------------------------------";
6.140 +"----------- fun thy_containing_rls ------------------------------";
6.141 +"----------- fun thy_containing_rls ------------------------------";
6.142 +val thy' = "Biegelinie.thy";
6.143 +val dropthys = takewhile [] (not o (curry op= thy') o
6.144 + (#1:theory' * theory -> theory'))
6.145 + (rev (!theory'));
6.146 +if length (!theory') <> length dropthys then ()
6.147 +else raise error "rewtools.sml: diff.behav. in thy_containing_rls 1";
6.148 +val dropthy's = map (get_thy o (#1 : (theory' * theory) -> theory'))
6.149 + dropthys;
6.150 +print_depth 99; dropthy's; print_depth 3;
6.151 +
6.152 +"Isac" mem dropthy's;
6.153 +op mem ("Isac", dropthy's);
6.154 +(op mem) o swap;
6.155 +((op mem) o swap) (dropthy's, "Isac");
6.156 +curry ((op mem) o swap);
6.157 +curry ((op mem) o swap) dropthy's "Isac";
6.158 +val startsearch = filter_out ((curry ((op mem) o swap) dropthy's) o
6.159 + ((#1 o #2) : rls' * (theory' * rls) -> theory'))
6.160 + (rev (!ruleset'));
6.161 +print_depth 99; map (#1 o #2) startsearch; print_depth 3;
6.162 +if length (!ruleset') <> length startsearch then ()
6.163 +else raise error "rewtools.sml: diff.behav. in thy_containing_rls 2";
6.164 +
6.165 +val rls' = "norm_Poly";
6.166 +case assoc (startsearch, rls') of
6.167 + Some (thy', _) => thyID2theory' thy'
6.168 + | _ => raise error ("thy_containing_rls : rls '"^str^
6.169 + "' not in !rulset' und thy '"^thy'^"'");
6.170 +
6.171 +if thy_containing_rls thy' rls' = ("IsacKnowledge", "Poly.thy") then ()
6.172 +else raise error "rewtools.sml: diff.behav. in thy_containing_rls 3";
6.173 +
6.174 +
6.175 +"----------- fun thy_containing_cal ------------------------------";
6.176 +"----------- fun thy_containing_cal ------------------------------";
6.177 +"----------- fun thy_containing_cal ------------------------------";
6.178 +val thy' = "Atools.thy";
6.179 +val dropthys = takewhile [] (not o (curry op= thy') o
6.180 + (#1:theory' * theory -> theory'))
6.181 + (rev (!theory'));
6.182 +length dropthys <> length (!theory');
6.183 +val dropthy's = map (get_thy o (#1 : (theory' * theory) -> theory'))
6.184 + dropthys;
6.185 +
6.186 +(rev (!calclist'));
6.187 +map #1 (rev (!calclist'));
6.188 +map (#1 : calc -> string) (rev (!calclist'));
6.189 +val startsearch = filter_out ((curry ((op mem) o swap) dropthy's) o
6.190 + (#1 : calc -> string)) (rev (!calclist'));
6.191 +
6.192 +"----------- initContext Thy_ Integration-demo -------------------";
6.193 +"----------- initContext Thy_ Integration-demo -------------------";
6.194 +"----------- initContext Thy_ Integration-demo -------------------";
6.195 +states:=[];
6.196 +CalcTree
6.197 +[(["functionTerm (2 * x)","integrateBy x","antiDerivative FF"],
6.198 + ("Integrate.thy",["integrate","function"],
6.199 + ["diff","integration"]))];
6.200 +Iterator 1;
6.201 +moveActiveRoot 1;
6.202 +(*TODO.new_c: cvs before 071227, 11:50------------------
6.203 +autoCalculate 1 CompleteCalc;
6.204 +interSteps 1 ([1],Res);
6.205 +interSteps 1 ([1,1],Res);
6.206 +val ((pt,p),_) = get_calc 1; show_pt pt;
6.207 +if existpt' ([1,1,1], Frm) pt then ()
6.208 +else raise error "integrate.sml: interSteps on Rewrite_Set_Inst 1";
6.209 +
6.210 +initContext 1 Thy_ ([1,1,1], Frm);
6.211 +--------------------TODO.new_c: cvs before 071227, 11:50*)
6.212 +
6.213 +"----------- initContext..Thy_, fun context_thm ------------------";
6.214 +"----------- initContext..Thy_, fun context_thm ------------------";
6.215 +"----------- initContext..Thy_, fun context_thm ------------------";
6.216 +states:=[];
6.217 +CalcTree (*start of calculation, return No.1*)
6.218 +[(["equality (x+1=2)", "solveFor x","solutions L"],
6.219 + ("Test.thy",
6.220 + ["sqroot-test","univariate","equation","test"],
6.221 + ["Test","squ-equ-test-subpbl1"]))];
6.222 +Iterator 1; moveActiveRoot 1;
6.223 +autoCalculate 1 CompleteCalc;
6.224 +
6.225 +"----- no thy-context at result -----";
6.226 +val p = ([], Res);
6.227 +initContext 1 Thy_ p;
6.228 +
6.229 +
6.230 +interSteps 1 ([2], Res);
6.231 +interSteps 1 ([3,1], Res);
6.232 +val ((pt,_),_) = get_calc 1; show_pt pt;
6.233 +
6.234 +val p = ([2,4], Res);
6.235 +val tac = Rewrite ("radd_left_commute","");
6.236 +initContext 1 Thy_ p;
6.237 +(*Res->Res, Rewrite "radd_left_commute 1 + (-2 + x) = 0 -> -2 + (1 + x) = 0
6.238 + --- in initContext..Thy_ ---*)
6.239 +val ContThm {thm,result,...} = context_thy (pt,p) tac;
6.240 +if thm = "thy_isac_Test-thm-radd_left_commute"
6.241 + andalso term2str result = "-2 + (1 + x) = 0" then ()
6.242 +else raise error"rewtools.sml initContext..Th_ thy_Test-thm-radd_left_commute";
6.243 +
6.244 +val p = ([3,1,1], Frm);
6.245 +val tac = Rewrite_Inst (["(bdv, x)"],("risolate_bdv_add",""));
6.246 +initContext 1 Thy_ p;
6.247 +(*Frm->Res, Rewrite_Inst "risolate_bdv_add" -1 + x = 0 -> x = 0 + -1 * -1
6.248 + --- in initContext..Thy_ ---*)
6.249 +val ContThmInst {thm,result,...} = context_thy (pt,p) tac;
6.250 +if thm = "thy_isac_Test-thm-risolate_bdv_add"
6.251 + andalso term2str result = "x = 0 + -1 * -1" then ()
6.252 +else raise error "rewtools.sml initContext..Th_ thy_Test-thm-risolate_bdv_add";
6.253 +
6.254 +initContext 1 Thy_ ([2,5], Res);
6.255 +(*Res->Res, Calculate "plus" -2 + (1 + x) = 0 -> -1 + x = 0
6.256 + --- in initContext..Thy_ ---*)
6.257 +
6.258 +
6.259 +"----------- initContext..Thy_, fun context_rls ------------------";
6.260 +"----------- initContext..Thy_, fun context_rls ------------------";
6.261 +"----------- initContext..Thy_, fun context_rls ------------------";
6.262 +(*using pt from above*)
6.263 +val p = ([1], Res);
6.264 +val tac = Rewrite_Set "Test_simplify";
6.265 +initContext 1 Thy_ p;
6.266 +(*Res->Res, Rewrite_Set "Test_simplify" x + 1 + -1 * 2 = 0 -> -1 + x = 0
6.267 + --- in initContext..Thy_ ---*)
6.268 +val ContRls {rls,result,...} = context_thy (pt,p) tac;
6.269 +if rls = "thy_isac_Test-rls-Test_simplify"
6.270 + andalso term2str result = "-1 + x = 0" then ()
6.271 +else raise error "rewtools.sml initContext..Th_ thy_Test-thm-risolate_bdv_add";
6.272 +
6.273 +val p = ([3,1], Frm);
6.274 +val tac = Rewrite_Set_Inst (["(bdv, x)"],"isolate_bdv");
6.275 +initContext 1 Thy_ p;
6.276 +(*Frm->Res, Rewrite_Set_Inst "isolate_bdv" -1 + x = 0 -> x = 0 + -1 * -1
6.277 + --- in initContext..Thy_ ---*)
6.278 +val ContRlsInst {rls,result,...} = context_thy (pt,p) tac;
6.279 +if rls = "thy_isac_Test-rls-isolate_bdv"
6.280 + andalso term2str result = "x = 0 + -1 * -1" then ()
6.281 +else raise error "rewtools.sml initContext..Th_ thy_Test-thm-risolate_bdv_add";
6.282 +
6.283 +
6.284 +
6.285 +"----------- checkContext..Thy_, fun context_thy -----------------";
6.286 +"----------- checkContext..Thy_, fun context_thy -----------------";
6.287 +"----------- checkContext..Thy_, fun context_thy -----------------";
6.288 +(*using pt from above*)
6.289 +
6.290 +val p = ([2,4], Res);
6.291 +val tac = Rewrite ("radd_left_commute","");
6.292 +checkContext 1 p "thy_Test-thm-radd_left_commute";
6.293 +(* radd_left_commute: 1 + (-2 + x) = 0 -> -2 + (1 + x) = 0
6.294 + --- in checkContext..Thy_ ---*)
6.295 +val ContThm {thm,result,...} = context_thy (pt,p) tac;
6.296 +if thm = "thy_isac_Test-thm-radd_left_commute"
6.297 + andalso term2str result = "-2 + (1 + x) = 0" then ()
6.298 +else raise error "rewtools.sml checkContext.._ thy_Test-thm-radd_left_commute";
6.299 +
6.300 +val p = ([3,1,1], Frm);
6.301 +val tac = Rewrite_Inst (["(bdv,x)"],("risolate_bdv_add",""));
6.302 +checkContext 1 p "thy_Test-thm-risolate_bdv_add";
6.303 +(* risolate_bdv_add: -1 + x = 0 -> x = 0 + -1 * -1
6.304 + --- in checkContext..Thy_ ---*)
6.305 +val ContThmInst {thm,result,...} = context_thy (pt,p) tac;
6.306 +if thm = "thy_isac_Test-thm-risolate_bdv_add"
6.307 + andalso term2str result = "x = 0 + -1 * -1" then ()
6.308 +else raise error "rewtools.sml checkContext..T_ thy_Test-thm-risolate_bdv_add";
6.309 +
6.310 +val p = ([2,5], Res);
6.311 +val tac = Calculate "plus";
6.312 +(*checkContext..Thy_ 1 ([2,5], Res);*)
6.313 +(*FIXXXME #######################vvvvv kestoreID !!!!!!!!!!!!!!!!*)
6.314 +checkContext 1 p ;
6.315 +(* Calculate "plus" -2 + (1 + x) = 0 -> -1 + x = 0
6.316 + --- in checkContext..Thy_ ---*)
6.317 +
6.318 +
6.319 +"----------- checkContext..Thy_, fun context_rls -----------------";
6.320 +"----------- checkContext..Thy_, fun context_rls -----------------";
6.321 +"----------- checkContext..Thy_, fun context_rls -----------------";
6.322 +(*using pt from above*)
6.323 +show_pt pt;
6.324 +
6.325 +val p = ([1], Res);
6.326 +val tac = Rewrite_Set "Test_simplify";
6.327 +checkContext 1 p "thy_isac_Test-rls-Test_simplify";
6.328 +(*Res->Res, Rewrite_Set "Test_simplify" x + 1 + -1 * 2 = 0 -> -1 + x = 0
6.329 + --- in checkContext..Thy_ ---*)
6.330 +val ContRls {rls,result,...} = context_thy (pt,p) tac;
6.331 +if rls = "thy_isac_Test-rls-Test_simplify"
6.332 + andalso term2str result = "-1 + x = 0" then ()
6.333 +else raise error "rewtools.sml checkContext..Thy_ thy_Test-rls-Test_simplify";
6.334 +
6.335 +val p = ([3,1], Frm);
6.336 +val tac = Rewrite_Set_Inst (["(bdv, x)"],"isolate_bdv");
6.337 +checkContext 1 p "thy_Test-rls-isolate_bdv";
6.338 +val ContRlsInst {rls,result,...} = context_thy (pt,p) tac;
6.339 +if rls = "thy_isac_Test-rls-isolate_bdv"
6.340 + andalso term2str result = "x = 0 + -1 * -1" then ()
6.341 +else raise error "rewtools.sml checkContext..Thy_ thy_Test-thm-isolate_bdv";
6.342 +
6.343 +
6.344 +"----------- checkContext..Thy_ on last formula ------------------";
6.345 +"----------- checkContext..Thy_ on last formula ------------------";
6.346 +"----------- checkContext..Thy_ on last formula ------------------";
6.347 +states:=[];
6.348 +CalcTree (*start of calculation, return No.1*)
6.349 +[(["equality (x+1=2)", "solveFor x","solutions L"],
6.350 + ("Test.thy",
6.351 + ["sqroot-test","univariate","equation","test"],
6.352 + ["Test","squ-equ-test-subpbl1"]))];
6.353 +Iterator 1; moveActiveRoot 1;
6.354 +
6.355 +autoCalculate 1 CompleteCalcHead;
6.356 +autoCalculate 1 (Step 1);
6.357 +val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;
6.358 +initContext 1 Thy_ ([1], Frm);
6.359 +checkContext 1 ([1], Frm) "thy_isac_Test-thm-radd_left_commute";
6.360 +
6.361 +autoCalculate 1 (Step 1);
6.362 +val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;
6.363 +initContext 1 Thy_ ([1], Res);
6.364 +checkContext 1 ([1], Res) "thy_isac_Test-rls-Test_simplify";
6.365 +
6.366 +
6.367 +
6.368 +"----------- fun guh2theID ---------------------------------------";
6.369 +"----------- fun guh2theID ---------------------------------------";
6.370 +"----------- fun guh2theID ---------------------------------------";
6.371 +val guh = "thy_scri_ListG-thm-zip_Nil";
6.372 +
6.373 +take_fromto 1 4 (explode guh);
6.374 +take_fromto 5 9 (explode guh);
6.375 +val rest = takerest (9,(explode guh));
6.376 +
6.377 +separate "-" rest;
6.378 +space_implode "-" rest;
6.379 +commas rest;
6.380 +
6.381 +val delim = "-";
6.382 +val thyID = takewhile [] (not o (curry op= delim)) rest;
6.383 +val rest' = dropuntil (curry op= delim) rest;
6.384 +val setc = take_fromto 1 5 rest';
6.385 +val xstr = takerest (5, rest');
6.386 +
6.387 +if guh2theID guh = ["IsacScripts", "ListG", "Theorems", "zip_Nil"] then ()
6.388 +else raise error "rewtools.sml: guh2theID thy_scri_ListG-thm-zip_Nil changed";
6.389 +
6.390 +
6.391 +"----------- debugging on Tests/solve_linear_as_rootpbl ----------";
6.392 +"----------- debugging on Tests/solve_linear_as_rootpbl ----------";
6.393 +"----------- debugging on Tests/solve_linear_as_rootpbl ----------";
6.394 +"----- initContext -----";
6.395 +states:=[];
6.396 +CalcTree
6.397 + [(["equality (1+-1*2+x=0)", "solveFor x", "solutions L"],
6.398 + ("Test.thy",
6.399 + ["linear","univariate","equation","test"],
6.400 + ["Test","solve_linear"]))];
6.401 +Iterator 1; moveActiveRoot 1;
6.402 +autoCalculate 1 CompleteCalcHead;
6.403 +
6.404 +autoCalculate 1 (Step 1); val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;
6.405 +if is_curr_endof_calc pt ([1],Frm) then ()
6.406 +else raise error "rewtools.sml is_curr_endof_calc ([1],Frm)";
6.407 +
6.408 +autoCalculate 1 (Step 1); val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;
6.409 +if not (is_curr_endof_calc pt ([1],Frm)) then ()
6.410 +else raise error "rewtools.sml is_curr_endof_calc ([1],Frm) not";
6.411 +if is_curr_endof_calc pt ([1],Res) then ()
6.412 +else raise error "rewtools.sml is_curr_endof_calc ([1],Res)";
6.413 +
6.414 +initContext 1 Thy_ ([1],Res);
6.415 +
6.416 +"----- checkContext -----";
6.417 +states:=[];
6.418 +CalcTree
6.419 + [(["equality (1+-1*2+x=0)", "solveFor x", "solutions L"],
6.420 + ("Test.thy",
6.421 + ["linear","univariate","equation","test"],
6.422 + ["Test","solve_linear"]))];
6.423 +Iterator 1; moveActiveRoot 1;
6.424 +autoCalculate 1 CompleteCalc;
6.425 +interSteps 1 ([1],Res);
6.426 +val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;
6.427 +
6.428 +checkContext 1 ([1],Res) "thy_isac_Test-rls-Test_simplify";
6.429 +
6.430 +interSteps 1 ([2],Res);
6.431 +val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;
6.432 +
6.433 +checkContext 1 ([2,1],Res) "thy_isac_Test-rls-Test_simplify";
6.434 +checkContext 1 ([2,2],Res) "thy_isac_Test-rls-Test_simplify";
6.435 +
6.436 +
6.437 +"----------- fun string_of_thmI for_[.]_) ------------------------";
6.438 +"----------- fun string_of_thmI for_[.]_) ------------------------";
6.439 +"----------- fun string_of_thmI for_[.]_) ------------------------";
6.440 +"----- these work ?!?";
6.441 +val th = sym_thm real_minus_eq_cancel;
6.442 +val Th = sym_Thm (Thm ("real_minus_eq_cancel", real_minus_eq_cancel));
6.443 +val th'= mk_thm Isac.thy ((de_quote o string_of_thm) real_minus_eq_cancel);
6.444 +val th'= mk_thm Biegelinie.thy((de_quote o string_of_thm)real_minus_eq_cancel);
6.445 +
6.446 +"----- DIFFERENCE TO ABOVE ?!?: this is still ok, when called in next_tac...";
6.447 +val ((pt,(p,p_)), _) = get_calc 1; show_pt pt;
6.448 +val Appl (Rewrite' (_,_,_,_,thm',_,_)) =
6.449 + applicable_in (p,p_) pt (Rewrite ("sym_real_minus_eq_cancel",""));
6.450 +"- compose stac as done in | appy (*leaf*) by handle_leaf";
6.451 +val (th, sr, E, a, v, t) =
6.452 + ("Biegelinie.thy",
6.453 + (#srls o get_met) ["IntegrierenUndKonstanteBestimmen"],
6.454 + [(str2term "q__::bool", str2term "q x = q_0")],
6.455 + Some (str2term "q x = q_0"),
6.456 + str2term "q__::bool",
6.457 + str2term "(Rewrite sym_real_minus_eq_cancel False) (q__::bool)");
6.458 +val (a', STac stac) = handle_leaf "next " th sr E a v t;
6.459 +term2str stac;
6.460 +"--- but this \"m\" is already corrupted";
6.461 +val (m,_) = stac2tac_ EmptyPtree (assoc_thy th) stac;
6.462 +"- because in assoc_thm'...";
6.463 +val (thy, (thmid, ct')) = (Biegelinie.thy, ("sym_real_minus_eq_cancel",""));
6.464 +val "s"::"y"::"m"::"_"::id = explode thmid;
6.465 +((num_str o (get_thm thy)) (implode id)) RS sym;
6.466 +((get_thm thy) (implode id)) RS sym;
6.467 +"... this creates [.]";
6.468 +((get_thm thy) (implode id));
6.469 +"... while this has _NO_ [.]";
6.470 +
6.471 +"----- thus we repair the [.] in string_of_thmI...";
6.472 +val thm = ((num_str o (get_thm thy)) (implode id)) RS sym;
6.473 +if string_of_thmI thm = "(?b1 = ?a1) = (- ?b1 = - ?a1)" then ()
6.474 +else raise error ("rewtools.sml: string_of_thmI " ^ string_of_thm thm ^
6.475 + " = " ^ string_of_thmI thm);
6.476 +
6.477 +
6.478 +"----------- (sym_real_minus_eq_cancel, (?b1 = ?a1) ..._[.]_)-----";
6.479 +"----------- (sym_real_minus_eq_cancel, (?b1 = ?a1) ..._[.]_)-----";
6.480 +"----------- (sym_real_minus_eq_cancel, (?b1 = ?a1) ..._[.]_)-----";
6.481 +states:=[];
6.482 +CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
6.483 + "RandbedingungenBiegung [y 0 = 0, y L = 0]",
6.484 + "RandbedingungenMoment [M_b 0 = 0, M_b L = 0]",
6.485 + "FunktionsVariable x"],
6.486 + ("Biegelinie.thy",
6.487 + ["MomentBestimmte","Biegelinien"],
6.488 + ["IntegrierenUndKonstanteBestimmen"]))];
6.489 +moveActiveRoot 1;
6.490 +autoCalculate 1 CompleteCalcHead;
6.491 +autoCalculate 1 (Step 1) (*Apply_Method*);
6.492 +autoCalculate 1 (Step 1) (*->GENERATED ([1], Frm)*);
6.493 +"--- this was corrupted before 'fun string_of_thmI'";
6.494 +val ((pt,(p,p_)), _) = get_calc 1; show_pt pt;
6.495 +if get_obj g_tac pt p = Rewrite ("sym_real_minus_eq_cancel",
6.496 + "(?b1 = ?a1) = (- ?b1 = - ?a1)") then ()
6.497 +else raise error "rewtools.sml: string_of_thmI ?!?";
6.498 +
6.499 +getTactic 1 ([1],Frm);
6.500 +