1.1 --- a/src/Tools/isac/Knowledge/Biegelinie.thy Sun Feb 02 02:45:11 2014 +0100
1.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy Sun Feb 02 03:09:40 2014 +0100
1.3 @@ -188,307 +188,6 @@
1.4 scr = EmptyScr};
1.5 *}
1.6
1.7 -ML {*
1.8 -store_met
1.9 - (prep_met thy "met_biege" [] e_metID
1.10 - (["IntegrierenUndKonstanteBestimmen"],
1.11 - [("#Given" ,["Traegerlaenge l_l", "Streckenlast q__q", "FunktionsVariable v_v"]),
1.12 - (*("#Where",["0 < l_l"]), ...wait for < and handling Arbfix*)
1.13 - ("#Find" ,["Biegelinie b_b"]),
1.14 - ("#Relate",["RandbedingungenBiegung r_b", "RandbedingungenMoment r_m"])],
1.15 - {rew_ord'="tless_true",
1.16 - rls' = append_rls "erls_IntegrierenUndK.." e_rls
1.17 - [Calc ("Atools.ident",eval_ident "#ident_"),
1.18 - Thm ("not_true",num_str @{thm not_true}),
1.19 - Thm ("not_false",num_str @{thm not_false})],
1.20 - calc = [], srls = srls, prls = Erls, crls = Atools_erls, errpats = [], nrls = Erls},
1.21 -"Script BiegelinieScript " ^
1.22 -"(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) " ^
1.23 -"(r_b::bool list) (r_m::bool list) = " ^
1.24 -" (let q___q = Take (qq v_v = q__q); " ^
1.25 -" q___q = ((Rewrite sym_neg_equal_iff_equal True) @@ " ^
1.26 -" (Rewrite Belastung_Querkraft True)) q___q; " ^
1.27 -" (Q__Q:: bool) = " ^
1.28 -" (SubProblem (Biegelinie',[named,integrate,function], " ^
1.29 -" [diff,integration,named]) " ^
1.30 -" [REAL (rhs q___q), REAL v_v, REAL_REAL Q]); " ^
1.31 -" Q__Q = Rewrite Querkraft_Moment True Q__Q; " ^
1.32 -" (M__M::bool) = " ^
1.33 -" (SubProblem (Biegelinie',[named,integrate,function], " ^
1.34 -" [diff,integration,named]) " ^
1.35 -" [REAL (rhs Q__Q), REAL v_v, REAL_REAL M_b]); " ^
1.36 - (*([5], Res), M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2*)
1.37 -" e__1 = NTH 1 r_m; " ^
1.38 -" (x__1::real) = argument_in (lhs e__1); " ^
1.39 -" (M__1::bool) = (Substitute [v_v = x__1]) M__M; " ^
1.40 - (*([6], Res), M_b 0 = c_2 + c * 0 + -1 * q_0 / 2 * 0 ^^^ 2*)
1.41 -" M__1 = (Substitute [e__1]) M__1; " ^
1.42 - (*([7], Res), 0 = c_2 + c * 0 + -1 * q_0 / 2 * 0 ^^^ 2*)
1.43 -" M__2 = Take M__M; " ^
1.44 - (*([8], Frm), M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2*)
1.45 -(*without above Take 'Substitute [v_v = x__2]' takes _last formula from ctree_*)
1.46 -" e__2 = NTH 2 r_m; " ^
1.47 -" (x__2::real) = argument_in (lhs e__2); " ^
1.48 -" (M__2::bool) = (Substitute [v_v = x__2]) M__M; " ^
1.49 - (*([8], Res), M_b L = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2*)
1.50 -" M__2 = (Substitute [e__2]) M__2; " ^
1.51 - (**)
1.52 -" (c_1_2::bool list) = " ^
1.53 -" (SubProblem (Biegelinie',[LINEAR,system],[no_met]) " ^
1.54 -" [BOOL_LIST [M__1, M__2], REAL_LIST [c,c_2]]); " ^
1.55 -" M__M = Take M__M; " ^
1.56 -" M__M = ((Substitute c_1_2) @@ " ^
1.57 -" (Try (Rewrite_Set_Inst [(bdv_1, c),(bdv_2, c_2)] " ^
1.58 -" simplify_System False)) @@ " ^
1.59 -" (Rewrite Moment_Neigung False) @@ " ^
1.60 -" (Rewrite make_fun_explicit False)) M__M; " ^
1.61 -(*----------------------- and the same once more ------------------------*)
1.62 -" (N__N:: bool) = " ^
1.63 -" (SubProblem (Biegelinie',[named,integrate,function], " ^
1.64 -" [diff,integration,named]) " ^
1.65 -" [REAL (rhs M__M), REAL v_v, REAL_REAL y']); " ^
1.66 -" (B__B:: bool) = " ^
1.67 -" (SubProblem (Biegelinie',[named,integrate,function], " ^
1.68 -" [diff,integration,named]) " ^
1.69 -" [REAL (rhs N__N), REAL v_v, REAL_REAL y]); " ^
1.70 -" e__1 = NTH 1 r_b; " ^
1.71 -" (x__1::real) = argument_in (lhs e__1); " ^
1.72 -" (B__1::bool) = (Substitute [v_v = x__1]) B__B; " ^
1.73 -" B__1 = (Substitute [e__1]) B__1 ; " ^
1.74 -" B__2 = Take B__B; " ^
1.75 -" e__2 = NTH 2 r_b; " ^
1.76 -" (x__2::real) = argument_in (lhs e__2); " ^
1.77 -" (B__2::bool) = (Substitute [v_v = x__2]) B__B; " ^
1.78 -" B__2 = (Substitute [e__2]) B__2 ; " ^
1.79 -" (c_1_2::bool list) = " ^
1.80 -" (SubProblem (Biegelinie',[LINEAR,system],[no_met]) " ^
1.81 -" [BOOL_LIST [B__1, B__2], REAL_LIST [c,c_2]]); " ^
1.82 -" B__B = Take B__B; " ^
1.83 -" B__B = ((Substitute c_1_2) @@ " ^
1.84 -" (Rewrite_Set_Inst [(bdv, x)] make_ratpoly_in False)) B__B " ^
1.85 -" in B__B)"
1.86 -));
1.87 -*}
1.88 -ML {*
1.89 -store_met
1.90 - (prep_met thy "met_biege_2" [] e_metID
1.91 - (["IntegrierenUndKonstanteBestimmen2"],
1.92 - [("#Given" ,["Traegerlaenge l_l", "Streckenlast q__q", "FunktionsVariable v_v"]),
1.93 - (*("#Where",["0 < l_l"]), ...wait for < and handling Arbfix*)
1.94 - ("#Find" ,["Biegelinie b_b"]),
1.95 - ("#Relate",["Randbedingungen r_b"])],
1.96 - {rew_ord'="tless_true",
1.97 - rls' = append_rls "erls_IntegrierenUndK.." e_rls
1.98 - [Calc ("Atools.ident",eval_ident "#ident_"),
1.99 - Thm ("not_true",num_str @{thm not_true}),
1.100 - Thm ("not_false",num_str @{thm not_false})],
1.101 - calc = [],
1.102 - srls = append_rls "erls_IntegrierenUndK.." e_rls
1.103 - [Calc("Tools.rhs", eval_rhs"eval_rhs_"),
1.104 - Calc ("Atools.ident",eval_ident "#ident_"),
1.105 - Thm ("last_thmI",num_str @{thm last_thmI}),
1.106 - Thm ("if_True",num_str @{thm if_True}),
1.107 - Thm ("if_False",num_str @{thm if_False})],
1.108 - prls = Erls, crls = Atools_erls, errpats = [], nrls = Erls},
1.109 -"Script Biegelinie2Script " ^
1.110 -"(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) (r_b::bool list) = " ^
1.111 -" (let " ^
1.112 -" (fun_s:: bool list) = " ^
1.113 -" (SubProblem (Biegelinie',[vonBelastungZu,Biegelinien], " ^
1.114 -" [Biegelinien,ausBelastung]) " ^
1.115 -" [REAL q__q, REAL v_v]); " ^
1.116 -" (equ_s::bool list) = " ^
1.117 -" (SubProblem (Biegelinie',[setzeRandbedingungen,Biegelinien], " ^
1.118 -" [Biegelinien,setzeRandbedingungenEin]) " ^
1.119 -" [BOOL_LIST fun_s, BOOL_LIST r_b]); " ^
1.120 -" (con_s::bool list) = " ^
1.121 -" (SubProblem (Biegelinie',[LINEAR,system],[no_met]) " ^
1.122 -" [BOOL_LIST equ_s, REAL_LIST [c,c_2,c_3,c_4]]); " ^
1.123 -" B_B = Take (lastI fun_s); " ^
1.124 -" B_B = ((Substitute con_s) @@ " ^
1.125 -" (Rewrite_Set_Inst [(bdv, v_v)] make_ratpoly_in False)) B_B " ^
1.126 -" in B_B)"
1.127 -));
1.128 -
1.129 -*}
1.130 -ML {*
1.131 -store_met
1.132 - (prep_met thy "met_biege_intconst_2" [] e_metID
1.133 - (["IntegrierenUndKonstanteBestimmen","2xIntegrieren"],
1.134 - [],
1.135 - {rew_ord'="tless_true", rls'=Erls, calc = [],
1.136 - srls = e_rls,
1.137 - prls=e_rls,
1.138 - crls = Atools_erls, errpats = [], nrls = e_rls},
1.139 -"empty_script"
1.140 -));
1.141 -
1.142 -store_met
1.143 - (prep_met thy "met_biege_intconst_4" [] e_metID
1.144 - (["IntegrierenUndKonstanteBestimmen","4x4System"],
1.145 - [],
1.146 - {rew_ord'="tless_true", rls'=Erls, calc = [],
1.147 - srls = e_rls,
1.148 - prls=e_rls,
1.149 - crls = Atools_erls, errpats = [], nrls = e_rls},
1.150 -"empty_script"
1.151 -));
1.152 -
1.153 -store_met
1.154 - (prep_met thy "met_biege_intconst_1" [] e_metID
1.155 - (["IntegrierenUndKonstanteBestimmen","1xIntegrieren"],
1.156 - [],
1.157 - {rew_ord'="tless_true", rls'=Erls, calc = [],
1.158 - srls = e_rls,
1.159 - prls=e_rls,
1.160 - crls = Atools_erls, errpats = [], nrls = e_rls},
1.161 -"empty_script"
1.162 -));
1.163 -
1.164 -store_met
1.165 - (prep_met thy "met_biege2" [] e_metID
1.166 - (["Biegelinien"],
1.167 - [],
1.168 - {rew_ord'="tless_true", rls'=Erls, calc = [],
1.169 - srls = e_rls,
1.170 - prls=e_rls,
1.171 - crls = Atools_erls, errpats = [], nrls = e_rls},
1.172 -"empty_script"
1.173 -));
1.174 -
1.175 -*}
1.176 -ML {*
1.177 -store_met
1.178 - (prep_met thy "met_biege_ausbelast" [] e_metID
1.179 - (["Biegelinien", "ausBelastung"],
1.180 - [("#Given" ,["Streckenlast q__q", "FunktionsVariable v_v"]),
1.181 - ("#Find" ,["Funktionen fun_s"])],
1.182 - {rew_ord'="tless_true",
1.183 - rls' = append_rls "erls_ausBelastung" e_rls
1.184 - [Calc ("Atools.ident", eval_ident "#ident_"),
1.185 - Thm ("not_true", num_str @{thm not_true}),
1.186 - Thm ("not_false", num_str @{thm not_false})],
1.187 - calc = [],
1.188 - srls = append_rls "srls_ausBelastung" e_rls
1.189 - [Calc ("Tools.rhs", eval_rhs "eval_rhs_")],
1.190 - prls = e_rls, crls = Atools_erls, errpats = [], nrls = e_rls},
1.191 -"Script Belastung2BiegelScript (q__q::real) (v_v::real) = " ^
1.192 -" (let q___q = Take (qq v_v = q__q); " ^
1.193 -" q___q = ((Rewrite sym_neg_equal_iff_equal True) @@ " ^
1.194 -" (Rewrite Belastung_Querkraft True)) q___q; " ^
1.195 -" (Q__Q:: bool) = " ^
1.196 -" (SubProblem (Biegelinie',[named,integrate,function], " ^
1.197 -" [diff,integration,named]) " ^
1.198 -" [REAL (rhs q___q), REAL v_v, REAL_REAL Q]); " ^
1.199 -" M__M = Rewrite Querkraft_Moment True Q__Q; " ^
1.200 -" (M__M::bool) = " ^
1.201 -" (SubProblem (Biegelinie',[named,integrate,function], " ^
1.202 -" [diff,integration,named]) " ^
1.203 -" [REAL (rhs M__M), REAL v_v, REAL_REAL M_b]); " ^
1.204 -" N__N = ((Rewrite Moment_Neigung False) @@ " ^
1.205 -" (Rewrite make_fun_explicit False)) M__M; " ^
1.206 -" (N__N:: bool) = " ^
1.207 -" (SubProblem (Biegelinie',[named,integrate,function], " ^
1.208 -" [diff,integration,named]) " ^
1.209 -" [REAL (rhs N__N), REAL v_v, REAL_REAL y']); " ^
1.210 -" (B__B:: bool) = " ^
1.211 -" (SubProblem (Biegelinie',[named,integrate,function], " ^
1.212 -" [diff,integration,named]) " ^
1.213 -" [REAL (rhs N__N), REAL v_v, REAL_REAL y]) " ^
1.214 -" in [Q__Q, M__M, N__N, B__B])"
1.215 -));
1.216 -
1.217 -*}
1.218 -ML {*
1.219 -store_met
1.220 - (prep_met thy "met_biege_setzrand" [] e_metID
1.221 - (["Biegelinien", "setzeRandbedingungenEin"],
1.222 - [("#Given" , ["Funktionen fun_s", "Randbedingungen r_b"]),
1.223 - ("#Find" , ["Gleichungen equs'''"])],
1.224 - {rew_ord'="tless_true", rls'=Erls, calc = [],
1.225 - srls = srls2,
1.226 - prls=e_rls,
1.227 - crls = Atools_erls, errpats = [], nrls = e_rls},
1.228 -"Script SetzeRandbedScript (fun_s::bool list) (r_b::bool list) = " ^
1.229 -" (let b_1 = NTH 1 r_b; " ^
1.230 -" f_s = filter_sameFunId (lhs b_1) fun_s; " ^
1.231 -" (e_1::bool) = " ^
1.232 -" (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
1.233 -" [Equation,fromFunction]) " ^
1.234 -" [BOOL (hd f_s), BOOL b_1]); " ^
1.235 -" b_2 = NTH 2 r_b; " ^
1.236 -" f_s = filter_sameFunId (lhs b_2) fun_s; " ^
1.237 -" (e_2::bool) = " ^
1.238 -" (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
1.239 -" [Equation,fromFunction]) " ^
1.240 -" [BOOL (hd f_s), BOOL b_2]); " ^
1.241 -" b_3 = NTH 3 r_b; " ^
1.242 -" f_s = filter_sameFunId (lhs b_3) fun_s; " ^
1.243 -" (e_3::bool) = " ^
1.244 -" (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
1.245 -" [Equation,fromFunction]) " ^
1.246 -" [BOOL (hd f_s), BOOL b_3]); " ^
1.247 -" b_4 = NTH 4 r_b; " ^
1.248 -" f_s = filter_sameFunId (lhs b_4) fun_s; " ^
1.249 -" (e_4::bool) = " ^
1.250 -" (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
1.251 -" [Equation,fromFunction]) " ^
1.252 -" [BOOL (hd f_s), BOOL b_4]) " ^
1.253 -" in [e_1, e_2, e_3, e_4])"
1.254 -(* filter requires more than 1 sec !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
1.255 -"Script SetzeRandbedScript (fun_s::bool list) (r_b::bool list) = " ^
1.256 -" (let b_1 = NTH 1 r_b; " ^
1.257 -" f_s = filter (sameFunId (lhs b_1)) fun_s; " ^
1.258 -" (e_1::bool) = " ^
1.259 -" (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
1.260 -" [Equation,fromFunction]) " ^
1.261 -" [BOOL (hd f_s), BOOL b_1]); " ^
1.262 -" b_2 = NTH 2 r_b; " ^
1.263 -" f_s = filter (sameFunId (lhs b_2)) fun_s; " ^
1.264 -" (e_2::bool) = " ^
1.265 -" (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
1.266 -" [Equation,fromFunction]) " ^
1.267 -" [BOOL (hd f_s), BOOL b_2]); " ^
1.268 -" b_3 = NTH 3 r_b; " ^
1.269 -" f_s = filter (sameFunId (lhs b_3)) fun_s; " ^
1.270 -" (e_3::bool) = " ^
1.271 -" (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
1.272 -" [Equation,fromFunction]) " ^
1.273 -" [BOOL (hd f_s), BOOL b_3]); " ^
1.274 -" b_4 = NTH 4 r_b; " ^
1.275 -" f_s = filter (sameFunId (lhs b_4)) fun_s; " ^
1.276 -" (e_4::bool) = " ^
1.277 -" (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
1.278 -" [Equation,fromFunction]) " ^
1.279 -" [BOOL (hd f_s), BOOL b_4]) " ^
1.280 -" in [e_1,e_2,e_3,e_4])"*)
1.281 -));
1.282 -
1.283 -*}
1.284 -ML {*
1.285 -store_met
1.286 - (prep_met thy "met_equ_fromfun" [] e_metID
1.287 - (["Equation","fromFunction"],
1.288 - [("#Given" ,["functionEq fu_n","substitution su_b"]),
1.289 - ("#Find" ,["equality equ'''"])],
1.290 - {rew_ord'="tless_true", rls'=Erls, calc = [],
1.291 - srls = append_rls "srls_in_EquationfromFunc" e_rls
1.292 - [Calc("Tools.lhs", eval_lhs"eval_lhs_"),
1.293 - Calc("Atools.argument'_in", eval_argument_in "Atools.argument'_in")],
1.294 - prls=e_rls, crls = Atools_erls, errpats = [], nrls = e_rls},
1.295 -(*(M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2) (M_b L = 0) -->
1.296 - 0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2*)
1.297 -"Script Function2Equality (fu_n::bool) (su_b::bool) =" ^
1.298 -" (let fu_n = Take fu_n; " ^
1.299 -" bd_v = argument_in (lhs fu_n); " ^
1.300 -" va_l = argument_in (lhs su_b); " ^
1.301 -" eq_u = (Substitute [bd_v = va_l]) fu_n; " ^
1.302 - (*([1], Res), M_b L = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2*)
1.303 -" eq_u = (Substitute [su_b]) eq_u " ^
1.304 -" in (Rewrite_Set norm_Rational False) eq_u) "
1.305 -));
1.306 -*}
1.307 -
1.308 setup {* KEStore_Elems.add_mets
1.309 [prep_met thy "met_biege" [] e_metID
1.310 (["IntegrierenUndKonstanteBestimmen"],