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