1.1 --- a/test/Tools/isac/Knowledge/eqsystem.sml Mon Sep 16 11:28:43 2013 +0200
1.2 +++ b/test/Tools/isac/Knowledge/eqsystem.sml Mon Sep 16 12:20:00 2013 +0200
1.3 @@ -640,17 +640,17 @@
1.4 "----------- all systems from Biegelinie -------------------------";
1.5 "----------- all systems from Biegelinie -------------------------";
1.6 "----------- all systems from Biegelinie -------------------------";
1.7 -val subst = [(str2term "bdv_1", str2term "c"),
1.8 - (str2term "bdv_2", str2term "c_2"),
1.9 - (str2term "bdv_3", str2term "c_3"),
1.10 - (str2term "bdv_4", str2term "c_4")];
1.11 +val thy = @{theory Isac}
1.12 +val subst =
1.13 + [(str2term "bdv_1", str2term "c"), (str2term "bdv_2", str2term "c_2"),
1.14 + (str2term "bdv_3", str2term "c_3"), (str2term "bdv_4", str2term "c_4")];
1.15 +
1.16 "------- Bsp 7.27";
1.17 states:=[];
1.18 -CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
1.19 - "Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]",
1.20 - "FunktionsVariable x"],
1.21 - ("Biegelinie", ["Biegelinien"],
1.22 - ["IntegrierenUndKonstanteBestimmen2"]))];
1.23 +CalcTree [(
1.24 + ["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
1.25 + "Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]", "FunktionsVariable x"],
1.26 + ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]))];
1.27 moveActiveRoot 1;
1.28 (*
1.29 trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;
1.30 @@ -659,20 +659,24 @@
1.31 c c_2 c_3 c_4 c c_2 1->2: c
1.32 c_2 c_4
1.33 c c_2 c c_2 c_3 c_4 [2':c, 1:c_2, 3:c_4] -> 4:c_3*)
1.34 -val t = str2term"[0 = c_4, \
1.35 -\ 0 = c_4 + L * c_3 +(12 * L ^^^ 2 * c_2 + 4 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) / (-24 * EI), \
1.36 -\ 0 = c_2, \
1.37 -\ 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2]";
1.38 -val SOME (t',_) = rewrite_set_ thy false isolate_bdvs_4x4 t;
1.39 -term2str t';
1.40 -"[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]";
1.41 +val t = str2term
1.42 + ("[0 = c_4, " ^
1.43 + "0 = c_4 + L * c_3 +(12 * L ^^^ 2 * c_2 + 4 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) / (-24 * EI), " ^
1.44 + "0 = c_2, " ^
1.45 + "0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2]");
1.46 +val SOME (t, _) = rewrite_set_ thy false isolate_bdvs_4x4 t;
1.47 +if term2str t =
1.48 +"[c_4 = 0,\n (12 * L ^^^ 2 * c_2 + 4 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) / (-24 * EI) =\n -1 * (c_4 + L * c_3) + 0,\n c_2 = 0, (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2 = 0]"
1.49 +then () else error "Bsp 7.27";
1.50
1.51 -"----- 7.27 go through the rewrites in met_eqsys_norm_4x4";
1.52 +"----- Bsp 7.27 go through the rewrites in met_eqsys_norm_4x4";
1.53 val t = str2term "0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2";
1.54 val NONE = rewrite_set_ thy false norm_Rational t;
1.55 val SOME (t,_) =
1.56 rewrite_set_inst_ thy false subst simplify_System_parenthesized t;
1.57 -term2str t = "0 = -1 * q_0 * L ^^^ 2 / 2 + (L * c + c_2)";
1.58 +if term2str t = "0 = -1 * q_0 * L ^^^ 2 / 2 + (L * c + c_2)"
1.59 +then () else error "Bsp 7.27 go through the rewrites in met_eqsys_norm_4x4";
1.60 +
1.61 "--- isolate_bdvs_4x4";
1.62 (*
1.63 val SOME (t,_) = rewrite_set_inst_ thy false subst isolate_bdvs_4x4 t;
1.64 @@ -685,24 +689,24 @@
1.65
1.66 "------- Bsp 7.28 ---------------vvvvvvvvvvvvv Momentenlinie postponed";
1.67 states:=[];
1.68 -CalcTree [(["Traegerlaenge L","Momentenlinie (-q_0 / L * x^3 / 6)",
1.69 +CalcTree [((*WN130908 <ERROR> error in kernel </ERROR>*)
1.70 + ["Traegerlaenge L","Momentenlinie (-q_0 / L * x^^^3 / 6)",
1.71 "Biegelinie y",
1.72 "Randbedingungen [y L = 0, y' L = 0]",
1.73 "FunktionsVariable x"],
1.74 ("Biegelinie", ["vonMomentenlinieZu","Biegelinien"],
1.75 ["Biegelinien", "AusMomentenlinie"]))];
1.76 +(*
1.77 moveActiveRoot 1;
1.78 -(*
1.79 trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;
1.80 *)
1.81
1.82 "------- Bsp 7.69";
1.83 states:=[];
1.84 -CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
1.85 - "Randbedingungen [y 0 = 0, y L = 0, y' 0 = 0, y' L = 0]",
1.86 - "FunktionsVariable x"],
1.87 - ("Biegelinie", ["Biegelinien"],
1.88 - ["IntegrierenUndKonstanteBestimmen2"] ))];
1.89 +CalcTree [(
1.90 + ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
1.91 + "Randbedingungen [y 0 = 0, y L = 0, y' 0 = 0, y' L = 0]", "FunktionsVariable x"],
1.92 + ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]))];
1.93 moveActiveRoot 1;
1.94 (*
1.95 trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;
1.96 @@ -711,18 +715,18 @@
1.97 c c_2 c_3 c_4 c c_2 c_3 1:c_3 -> 2:c c_2 2: c c_2
1.98 c_3 c_4
1.99 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*)
1.100 -val t = str2term"[0 = c_4 + 0 / (-1 * EI), \
1.101 -\ 0 = c_4 + L * c_3 + (12 * L ^^^ 2 * c_2 + 4 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) / (-24 * EI), \
1.102 -\ 0 = c_3 + 0 / (-1 * EI), \
1.103 -\ 0 = c_3 + (6 * L * c_2 + 3 * L ^^^ 2 * c + -1 * L ^^^ 3 * q_0) / (-6 * EI)]";
1.104 +val t = str2term
1.105 + ("[0 = c_4 + 0 / (-1 * EI), " ^
1.106 + "0 = c_4 + L * c_3 + (12 * L ^^^ 2 * c_2 + 4 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) / (-24 * EI), " ^
1.107 + "0 = c_3 + 0 / (-1 * EI), " ^
1.108 + "0 = c_3 + (6 * L * c_2 + 3 * L ^^^ 2 * c + -1 * L ^^^ 3 * q_0) / (-6 * EI)]");
1.109
1.110 "------- Bsp 7.70";
1.111 states:=[];
1.112 -CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
1.113 - "Randbedingungen [Q 0 = q_0 * L, M_b L = 0, y 0 = 0, y' 0 = 0]",
1.114 - "FunktionsVariable x"],
1.115 - ("Biegelinie", ["Biegelinien"],
1.116 - ["IntegrierenUndKonstanteBestimmen2"] ))];
1.117 +CalcTree [(
1.118 + ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
1.119 + "Randbedingungen [Q 0 = q_0 * L, M_b L = 0, y 0 = 0, y' 0 = 0]", "FunktionsVariable x"],
1.120 + ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"] ))];
1.121 moveActiveRoot 1;
1.122 (*
1.123 trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;
1.124 @@ -732,46 +736,46 @@
1.125 c_3 |
1.126 c_4 | STOPPED.WN06? test methods @@@@@@@@@@@@@@@@@@@@@@@*)
1.127
1.128 +"----- 7.70 go through the rewrites in met_eqsys_norm_4x4";
1.129 +val t = str2term
1.130 + ("[L * q_0 = c, " ^
1.131 + "0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2, " ^
1.132 + "0 = c_4, " ^
1.133 + "0 = c_3]");
1.134 +val SOME (t,_) = rewrite_ thy e_rew_ord e_rls false (num_str @{thm commute_0_equality}) t;
1.135 +val SOME (t,_) = rewrite_ thy e_rew_ord e_rls false (num_str @{thm commute_0_equality}) t;
1.136 +val SOME (t,_) = rewrite_ thy e_rew_ord e_rls false (num_str @{thm commute_0_equality}) t;
1.137 +if term2str t =
1.138 + "[L * q_0 = c, (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2 = 0, c_4 = 0,\n c_3 = 0]"
1.139 +then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 1";
1.140
1.141 -"----- 7.70 go through the rewrites in met_eqsys_norm_4x4";
1.142 -val t = str2term"[L * q_0 = c, \
1.143 - \ 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2,\
1.144 - \ 0 = c_4, \
1.145 - \ 0 = c_3]";
1.146 -val SOME (t,_) =
1.147 - rewrite_ thy e_rew_ord e_rls false (num_str @{thm commute_0_equality}) t;
1.148 -val SOME (t,_) =
1.149 - rewrite_ thy e_rew_ord e_rls false (num_str @{thm commute_0_equality}) t;
1.150 -val SOME (t,_) =
1.151 - rewrite_ thy e_rew_ord e_rls false (num_str @{thm commute_0_equality}) t;
1.152 -term2str t =
1.153 - "[L * q_0 = c, (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2 = 0, c_4 = 0,\n c_3 = 0]";
1.154 -val SOME (t,_) =
1.155 - rewrite_set_inst_ thy false subst simplify_System_parenthesized t;
1.156 -term2str t =
1.157 -"[L * q_0 = c, -1 * q_0 * L ^^^ 2 / 2 + (L * c + c_2) = 0, c_4 = 0, c_3 = 0]";
1.158 +val SOME (t,_) = rewrite_set_inst_ thy false subst simplify_System_parenthesized t;
1.159 +if term2str t = "[L * q_0 = c, -1 * q_0 * L ^^^ 2 / 2 + (L * c + c_2) = 0, c_4 = 0, c_3 = 0]"
1.160 +then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 2";
1.161 +
1.162 val SOME (t,_) = rewrite_set_inst_ thy false subst isolate_bdvs_4x4 t;
1.163 -term2str t =
1.164 - "[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]";
1.165 -val SOME (t,_) =
1.166 - rewrite_set_inst_ thy false subst simplify_System_parenthesized t;
1.167 +if term2str t =
1.168 + "[c = (-1 * (L * q_0) + 0) / -1,\n" ^
1.169 + " L * c + c_2 = -1 * (-1 * q_0 * L ^^^ 2 / 2) + 0, c_4 = 0, c_3 = 0]"
1.170 +then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 3";
1.171
1.172 -term2str t ="[c = L * q_0, L * c + c_2 = q_0 * L ^^^ 2 / 2, c_4 = 0, c_3 = 0]";
1.173 -val SOME (t,_) = rewrite_set_ thy false order_system t;
1.174 -if term2str t ="[c = L * q_0, L * c + c_2 = q_0 * L ^^^ 2 / 2, c_3 = 0, c_4 = 0]" then ()
1.175 -else error "eqsystem.sml: exp 7.70 normalize 4x4 by rewrite changed";
1.176 +val SOME (t,_) = rewrite_set_inst_ thy false subst simplify_System_parenthesized t;
1.177 +if term2str t = "[c = -1 * L * q_0 / -1, L * c + c_2 = q_0 * L ^^^ 2 / 2, c_4 = 0, c_3 = 0]"
1.178 +then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 4";
1.179
1.180 +val SOME (t, _) = rewrite_set_ thy false order_system t;
1.181 +if term2str t = "[c = -1 * L * q_0 / -1, L * c + c_2 = q_0 * L ^^^ 2 / 2, c_3 = 0, c_4 = 0]"
1.182 +then () else error "eqsystem.sml: exp 7.70 normalize 4x4 by rewrite changed";
1.183
1.184 "----- 7.70 with met normalize: ";
1.185 -val fmz = ["equalities \
1.186 - \[L * q_0 = c, \
1.187 - \ 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2,\
1.188 - \ 0 = c_4, \
1.189 - \ 0 = c_3]",
1.190 - "solveForVars [c, c_2, c_3, c_4]", "solution LL"];
1.191 -val (dI',pI',mI') =
1.192 - ("Biegelinie",["linear", "system"],["no_met"]);
1.193 -val p = e_pos'; val c = [];
1.194 +val fmz = ["equalities" ^
1.195 + "[L * q_0 = c, " ^
1.196 + "0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2, " ^
1.197 + "0 = c_4, " ^
1.198 + "0 = c_3]", "solveForVars [c, c_2, c_3, c_4]", "solution LL"];
1.199 +val (dI',pI',mI') = ("Biegelinie",["linear", "system"], ["no_met"]);
1.200 +val p = e_pos'; val c = [];
1.201 +
1.202 (*============ inhibit exn WN120314 TODO: investigate type error (same as above)==
1.203 in next but one test below the same type error.
1.204 /-------------------------------------------------------\
1.205 @@ -790,8 +794,9 @@
1.206 case nxt of (_,Apply_Method ["EqSystem", "normalize", "4x4"]) => ()
1.207 | _ => error "eqsystem.sml [EqSystem,normalize,4x4] specify";
1.208 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.209 +
1.210 "----- outcommented before Isabelle2002 --> 2011 -------------------------";
1.211 -(*vvvWN080102 Exception- Match raised
1.212 +(*-----------------------------------vvvWN080102 Exception- Match raised
1.213 since assod Rewrite .. Rewrite'_Set
1.214 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.215