1.1 --- a/src/Tools/isac/Interpret/mathengine.sml Thu Mar 08 14:33:34 2012 +0100
1.2 +++ b/src/Tools/isac/Interpret/mathengine.sml Sat Mar 10 09:41:09 2012 +0100
1.3 @@ -398,7 +398,7 @@
1.4 | ("not-applicable",_) => (pt, p)
1.5 | ("end-of-calculation", (_, _, ptp)) => ptp
1.6 | ("failure",_) => error "sys-error";
1.7 - val (_, ts) = (*WN101102 TODO: locatetac + step create _same_ (pt,p) ?*)
1.8 + val (_, ts) =
1.9 (case step p ((pt, e_pos'),[]) of
1.10 ("ok", (ts as (tac,_,_)::_, _, _)) => ("",ts)
1.11 | ("helpless",_) => ("helpless: cannot propose tac", [])
2.1 --- a/src/Tools/isac/Interpret/script.sml Thu Mar 08 14:33:34 2012 +0100
2.2 +++ b/src/Tools/isac/Interpret/script.sml Sat Mar 10 09:41:09 2012 +0100
2.3 @@ -1068,22 +1068,17 @@
2.4
2.5 | ass_up (ysa as (y,ctxt,s,Script sc,d)) (is as (E,l,a,v,S,b),ss)
2.6 (Const ("Script.Seq",_) $ _ ) = (*2*: comes from e1, goes to e2*)
2.7 - (* val ((ysa as (y,s,Script sc,d)), (is as (E,l,a,v,S,b),ss),
2.8 - (Const ("Script.Seq",_) $ _ )) =
2.9 - (ys, ((E,up,a,v,S,b),ss), (go up sc));
2.10 - *)
2.11 - let val up = drop_last l;
2.12 - val Const ("Script.Seq",_) $ _ $ e2 = go up sc
2.13 - (*val _= tracing("### ass_up Seq$e: is=")
2.14 - val _= tracing(istate2str (ScrState is))*)
2.15 - in case assy (y,ctxt,s,d,Aundef) ((E, up@[R], a,v,S,b),ss) e2 of
2.16 - NasNap (v,E) => astep_up ysa ((E,up,a,v,S,b),ss)
2.17 - | NasApp iss => astep_up ysa iss
2.18 - | ay => ay end
2.19 + let
2.20 + val up = drop_last l;
2.21 + val Const ("Script.Seq",_) $ _ $ e2 = go up sc
2.22 + (*val _= tracing("### ass_up Seq$e: is=")
2.23 + val _= tracing(istate2str (ScrState is))*)
2.24 + in
2.25 + case assy (y,ctxt,s,d,Aundef) ((E, up@[R], a,v,S,b),ss) e2 of
2.26 + NasNap (v,E) => astep_up ysa ((E,up,a,v,S,b),ss)
2.27 + | NasApp iss => astep_up ysa iss
2.28 + | ay => ay end
2.29
2.30 - (* val (ysa, iss, (Const ("Script.Try",_) $ e $ _)) =
2.31 - (ys, ((E,up,a,v,S,b),ss), (go up sc));
2.32 - *)
2.33 | ass_up ysa iss (Const ("Script.Try",_) $ e $ _) =
2.34 astep_up ysa iss
2.35
3.1 --- a/src/Tools/isac/Knowledge/Biegelinie.thy Thu Mar 08 14:33:34 2012 +0100
3.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy Sat Mar 10 09:41:09 2012 +0100
3.3 @@ -228,125 +228,123 @@
3.4
3.5 ML {*
3.6 store_met
3.7 - (prep_met thy "met_biege" [] e_metID
3.8 - (["IntegrierenUndKonstanteBestimmen"],
3.9 - [("#Given" ,["Traegerlaenge l_l", "Streckenlast q_q",
3.10 - "FunktionsVariable v_v"]),
3.11 + (prep_met thy "met_biege" [] e_metID
3.12 + (["IntegrierenUndKonstanteBestimmen"],
3.13 + [("#Given" ,["Traegerlaenge l_l", "Streckenlast q__q", "FunktionsVariable v_v"]),
3.14 (*("#Where",["0 < l_l"]), ...wait for < and handling Arbfix*)
3.15 - ("#Find" ,["Biegelinie b_b"]),
3.16 - ("#Relate",["RandbedingungenBiegung r_b",
3.17 - "RandbedingungenMoment r_m"])
3.18 - ],
3.19 - {rew_ord'="tless_true",
3.20 - rls' = append_rls "erls_IntegrierenUndK.." e_rls
3.21 - [Calc ("Atools.ident",eval_ident "#ident_"),
3.22 - Thm ("not_true",num_str @{thm not_true}),
3.23 - Thm ("not_false",num_str @{thm not_false})],
3.24 - calc = [], srls = srls, prls = Erls,
3.25 - crls = Atools_erls, nrls = Erls},
3.26 -"Script BiegelinieScript " ^
3.27 -"(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) " ^
3.28 -"(r_b::bool list) (r_m::bool list) = " ^
3.29 -" (let q___q = Take (q_q v_v = q__q); " ^
3.30 -" q___q = ((Rewrite sym_real_minus_eq_cancel True) @@ " ^
3.31 -" (Rewrite Belastung_Querkraft True)) q___q; " ^
3.32 -" (Q__Q:: bool) = " ^
3.33 -" (SubProblem (Biegelinie',[named,integrate,function], " ^
3.34 -" [diff,integration,named]) " ^
3.35 + ("#Find" ,["Biegelinie b_b"]),
3.36 + ("#Relate",["RandbedingungenBiegung r_b", "RandbedingungenMoment r_m"])],
3.37 + {rew_ord'="tless_true",
3.38 + rls' = append_rls "erls_IntegrierenUndK.." e_rls
3.39 + [Calc ("Atools.ident",eval_ident "#ident_"),
3.40 + Thm ("not_true",num_str @{thm not_true}),
3.41 + Thm ("not_false",num_str @{thm not_false})],
3.42 + calc = [], srls = srls, prls = Erls, crls = Atools_erls, nrls = Erls},
3.43 +"Script BiegelinieScript " ^
3.44 +"(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) " ^
3.45 +"(r_b::bool list) (r_m::bool list) = " ^
3.46 +" (let q___q = Take (qq v_v = q__q); " ^
3.47 +" q___q = ((Rewrite sym_neg_equal_iff_equal True) @@ " ^
3.48 +" (Rewrite Belastung_Querkraft True)) q___q; " ^
3.49 +" (Q__Q:: bool) = " ^
3.50 +" (SubProblem (Biegelinie',[named,integrate,function], " ^
3.51 +" [diff,integration,named]) " ^
3.52 " [REAL (rhs q___q), REAL v_v, REAL_REAL Q]); " ^
3.53 -" Q__Q = Rewrite Querkraft_Moment True Q__Q; " ^
3.54 -" (M__M::bool) = " ^
3.55 -" (SubProblem (Biegelinie',[named,integrate,function], " ^
3.56 -" [diff,integration,named]) " ^
3.57 +" Q__Q = Rewrite Querkraft_Moment True Q__Q; " ^
3.58 +" (M__M::bool) = " ^
3.59 +" (SubProblem (Biegelinie',[named,integrate,function], " ^
3.60 +" [diff,integration,named]) " ^
3.61 " [REAL (rhs Q__Q), REAL v_v, REAL_REAL M_b]); " ^
3.62 + (*([5], Res), M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2*)
3.63 " e__1 = NTH 1 r_m; " ^
3.64 -" (x__1::real) = argument_in (lhs e__1); " ^
3.65 -" (M__1::bool) = (Substitute [v_v = x__1]) M__M; " ^
3.66 -" M__1 = (Substitute [e__1]) M__1 ; " ^
3.67 -" M__2 = Take M__M; " ^
3.68 -(*without this Take 'Substitute [v_v = x__2]' takes _last formula from ctree_*)
3.69 +" (x__1::real) = argument_in (lhs e__1); " ^
3.70 +" (M__1::bool) = (Substitute [v_v = x__1]) M__M; " ^
3.71 + (*([6], Res), M_b 0 = c_2 + c * 0 + -1 * q_0 / 2 * 0 ^^^ 2*)
3.72 +" M__1 = (Substitute [e__1]) M__1; " ^
3.73 + (*([7], Res), 0 = c_2 + c * 0 + -1 * q_0 / 2 * 0 ^^^ 2*)
3.74 +" M__2 = Take M__M; " ^
3.75 + (*([8], Frm), M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2*)
3.76 +(*without above Take 'Substitute [v_v = x__2]' takes _last formula from ctree_*)
3.77 " e__2 = NTH 2 r_m; " ^
3.78 -" (x__2::real) = argument_in (lhs e__2); " ^
3.79 -" (M__2::bool) = ((Substitute [v_v = x__2]) @@ " ^
3.80 -" (Substitute [e__2])) M__2; " ^
3.81 -" (c_1_2::bool list) = " ^
3.82 -" (SubProblem (Biegelinie',[linear,system],[no_met]) " ^
3.83 -" [BOOL_LIST [M__1, M__2], REAL_LIST [c,c_2]]); " ^
3.84 -" M__M = Take M__M; " ^
3.85 +" (x__2::real) = argument_in (lhs e__2); " ^
3.86 +" (M__2::bool) = (Substitute [v_v = x__2]) M__M; " ^
3.87 + (*([8], Res), M_b L = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2*)
3.88 +" M__2 = (Substitute [e__2]) M__2; " ^
3.89 + (**)
3.90 +" (c_1_2::bool list) = " ^
3.91 +" (SubProblem (Biegelinie',[linear,system],[no_met]) " ^
3.92 +" [BOOL_LIST [M__1, M__2], REAL_LIST [c,c_2]]); " ^
3.93 +" M__M = Take M__M; " ^
3.94 " M__M = ((Substitute c_1_2) @@ " ^
3.95 -" (Try (Rewrite_Set_Inst [(bdv_1, c),(bdv_2, c_2)]" ^
3.96 -" simplify_System False)) @@ " ^
3.97 -" (Rewrite Moment_Neigung False) @@ " ^
3.98 -" (Rewrite make_fun_explicit False)) M__M; " ^
3.99 +" (Try (Rewrite_Set_Inst [(bdv_1, c),(bdv_2, c_2)] " ^
3.100 +" simplify_System False)) @@ " ^
3.101 +" (Rewrite Moment_Neigung False) @@ " ^
3.102 +" (Rewrite make_fun_explicit False)) M__M; " ^
3.103 (*----------------------- and the same once more ------------------------*)
3.104 -" (N__N:: bool) = " ^
3.105 -" (SubProblem (Biegelinie',[named,integrate,function], " ^
3.106 -" [diff,integration,named]) " ^
3.107 +" (N__N:: bool) = " ^
3.108 +" (SubProblem (Biegelinie',[named,integrate,function], " ^
3.109 +" [diff,integration,named]) " ^
3.110 " [REAL (rhs M__M), REAL v_v, REAL_REAL y']); " ^
3.111 -" (B__B:: bool) = " ^
3.112 -" (SubProblem (Biegelinie',[named,integrate,function], " ^
3.113 -" [diff,integration,named]) " ^
3.114 +" (B__B:: bool) = " ^
3.115 +" (SubProblem (Biegelinie',[named,integrate,function], " ^
3.116 +" [diff,integration,named]) " ^
3.117 " [REAL (rhs N__N), REAL v_v, REAL_REAL y]); " ^
3.118 " e__1 = NTH 1 r_b; " ^
3.119 -" (x__1::real) = argument_in (lhs e__1); " ^
3.120 -" (B__1::bool) = (Substitute [v_v = x__1]) B__B; " ^
3.121 -" B__1 = (Substitute [e__1]) B__1 ; " ^
3.122 -" B__2 = Take B__B; " ^
3.123 +" (x__1::real) = argument_in (lhs e__1); " ^
3.124 +" (B__1::bool) = (Substitute [v_v = x__1]) B__B; " ^
3.125 +" B__1 = (Substitute [e__1]) B__1 ; " ^
3.126 +" B__2 = Take B__B; " ^
3.127 " e__2 = NTH 2 r_b; " ^
3.128 -" (x__2::real) = argument_in (lhs e__2); " ^
3.129 -" (B__2::bool) = ((Substitute [v_v = x__2]) @@ " ^
3.130 -" (Substitute [e__2])) B__2; " ^
3.131 -" (c_1_2::bool list) = " ^
3.132 -" (SubProblem (Biegelinie',[linear,system],[no_met]) " ^
3.133 -" [BOOL_LIST [B__1, B__2], REAL_LIST [c,c_2]]); " ^
3.134 -" B__B = Take B__B; " ^
3.135 +" (x__2::real) = argument_in (lhs e__2); " ^
3.136 +" (B__2::bool) = (Substitute [v_v = x__2]) B__B; " ^
3.137 +" B__2 = (Substitute [e__2]) B__2 ; " ^
3.138 +" (c_1_2::bool list) = " ^
3.139 +" (SubProblem (Biegelinie',[linear,system],[no_met]) " ^
3.140 +" [BOOL_LIST [B__1, B__2], REAL_LIST [c,c_2]]); " ^
3.141 +" B__B = Take B__B; " ^
3.142 " B__B = ((Substitute c_1_2) @@ " ^
3.143 -" (Rewrite_Set_Inst [(bdv, x)] make_ratpoly_in False)) B__B " ^
3.144 +" (Rewrite_Set_Inst [(bdv, x)] make_ratpoly_in False)) B__B " ^
3.145 " in B__B)"
3.146 ));
3.147 *}
3.148 ML {*
3.149 -
3.150 store_met
3.151 - (prep_met thy "met_biege_2" [] e_metID
3.152 - (["IntegrierenUndKonstanteBestimmen2"],
3.153 - [("#Given" ,["Traegerlaenge l_l", "Streckenlast q__q",
3.154 - "FunktionsVariable v_v"]),
3.155 + (prep_met thy "met_biege_2" [] e_metID
3.156 + (["IntegrierenUndKonstanteBestimmen2"],
3.157 + [("#Given" ,["Traegerlaenge l_l", "Streckenlast q__q", "FunktionsVariable v_v"]),
3.158 (*("#Where",["0 < l_l"]), ...wait for < and handling Arbfix*)
3.159 - ("#Find" ,["Biegelinie b_b"]),
3.160 - ("#Relate",["Randbedingungen r_b"])
3.161 - ],
3.162 - {rew_ord'="tless_true",
3.163 - rls' = append_rls "erls_IntegrierenUndK.." e_rls
3.164 - [Calc ("Atools.ident",eval_ident "#ident_"),
3.165 - Thm ("not_true",num_str @{thm not_true}),
3.166 - Thm ("not_false",num_str @{thm not_false})],
3.167 - calc = [],
3.168 - srls = append_rls "erls_IntegrierenUndK.." e_rls
3.169 - [Calc("Tools.rhs", eval_rhs"eval_rhs_"),
3.170 - Calc ("Atools.ident",eval_ident "#ident_"),
3.171 - Thm ("last_thmI",num_str @{thm last_thmI}),
3.172 - Thm ("if_True",num_str @{thm if_True}),
3.173 - Thm ("if_False",num_str @{thm if_False})
3.174 - ],
3.175 - prls = Erls, crls = Atools_erls, nrls = Erls},
3.176 -"Script Biegelinie2Script " ^
3.177 + ("#Find" ,["Biegelinie b_b"]),
3.178 + ("#Relate",["Randbedingungen r_b"])],
3.179 + {rew_ord'="tless_true",
3.180 + rls' = append_rls "erls_IntegrierenUndK.." e_rls
3.181 + [Calc ("Atools.ident",eval_ident "#ident_"),
3.182 + Thm ("not_true",num_str @{thm not_true}),
3.183 + Thm ("not_false",num_str @{thm not_false})],
3.184 + calc = [],
3.185 + srls = append_rls "erls_IntegrierenUndK.." e_rls
3.186 + [Calc("Tools.rhs", eval_rhs"eval_rhs_"),
3.187 + Calc ("Atools.ident",eval_ident "#ident_"),
3.188 + Thm ("last_thmI",num_str @{thm last_thmI}),
3.189 + Thm ("if_True",num_str @{thm if_True}),
3.190 + Thm ("if_False",num_str @{thm if_False})],
3.191 + prls = Erls, crls = Atools_erls, nrls = Erls},
3.192 +"Script Biegelinie2Script " ^
3.193 "(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) (r_b::bool list) = " ^
3.194 -" (let " ^
3.195 -" (fun_s:: bool list) = " ^
3.196 -" (SubProblem (Biegelinie',[vonBelastungZu,Biegelinien], " ^
3.197 -" [Biegelinien,ausBelastung]) " ^
3.198 -" [REAL q__q, REAL v_v]); " ^
3.199 -" (equ_s::bool list) = " ^
3.200 -" (SubProblem (Biegelinie',[setzeRandbedingungen,Biegelinien]," ^
3.201 -" [Biegelinien,setzeRandbedingungenEin]) " ^
3.202 +" (let " ^
3.203 +" (fun_s:: bool list) = " ^
3.204 +" (SubProblem (Biegelinie',[vonBelastungZu,Biegelinien], " ^
3.205 +" [Biegelinien,ausBelastung]) " ^
3.206 +" [REAL q__q, REAL v_v]); " ^
3.207 +" (equ_s::bool list) = " ^
3.208 +" (SubProblem (Biegelinie',[setzeRandbedingungen,Biegelinien], " ^
3.209 +" [Biegelinien,setzeRandbedingungenEin]) " ^
3.210 " [BOOL_LIST fun_s, BOOL_LIST r_b]); " ^
3.211 -" (con_s::bool list) = " ^
3.212 -" (SubProblem (Biegelinie',[linear,system],[no_met]) " ^
3.213 -" [BOOL_LIST equ_s, REAL_LIST [c,c_2,c_3,c_4]]); " ^
3.214 +" (con_s::bool list) = " ^
3.215 +" (SubProblem (Biegelinie',[linear,system],[no_met]) " ^
3.216 +" [BOOL_LIST equ_s, REAL_LIST [c,c_2,c_3,c_4]]); " ^
3.217 " B_B = Take (lastI fun_s); " ^
3.218 " B_B = ((Substitute con_s) @@ " ^
3.219 -" (Rewrite_Set_Inst [(bdv, v_v)] make_ratpoly_in False)) B_B " ^
3.220 +" (Rewrite_Set_Inst [(bdv, v_v)] make_ratpoly_in False)) B_B " ^
3.221 " in B_B)"
3.222 ));
3.223
3.224 @@ -399,42 +397,42 @@
3.225 *}
3.226 ML {*
3.227 store_met
3.228 - (prep_met thy "met_biege_ausbelast" [] e_metID
3.229 - (["Biegelinien","ausBelastung"],
3.230 - [("#Given" ,["Streckenlast q__q","FunktionsVariable v_v"]),
3.231 - ("#Find" ,["Funktionen fun_s"])],
3.232 - {rew_ord'="tless_true",
3.233 - rls' = append_rls "erls_ausBelastung" e_rls
3.234 - [Calc ("Atools.ident",eval_ident "#ident_"),
3.235 - Thm ("not_true",num_str @{thm not_true}),
3.236 - Thm ("not_false",num_str @{thm not_false})],
3.237 - calc = [],
3.238 - srls = append_rls "srls_ausBelastung" e_rls
3.239 - [Calc("Tools.rhs", eval_rhs"eval_rhs_")],
3.240 - prls = e_rls, crls = Atools_erls, nrls = e_rls},
3.241 -"Script Belastung2BiegelScript (q__q::real) (v_v::real) = " ^
3.242 -" (let q___q = Take (q_q v_v = q__q); " ^
3.243 -" q___q = ((Rewrite sym_real_minus_eq_cancel True) @@ " ^
3.244 -" (Rewrite Belastung_Querkraft True)) q___q; " ^
3.245 -" (Q__Q:: bool) = " ^
3.246 -" (SubProblem (Biegelinie',[named,integrate,function], " ^
3.247 -" [diff,integration,named]) " ^
3.248 -" [REAL (rhs q___q), REAL v_v, REAL_REAL Q]); " ^
3.249 -" M__M = Rewrite Querkraft_Moment True Q__Q; " ^
3.250 -" (M__M::bool) = " ^
3.251 -" (SubProblem (Biegelinie',[named,integrate,function], " ^
3.252 -" [diff,integration,named]) " ^
3.253 -" [REAL (rhs M__M), REAL v_v, REAL_REAL M_b]); " ^
3.254 -" N__N = ((Rewrite Moment_Neigung False) @@ " ^
3.255 -" (Rewrite make_fun_explicit False)) M__M; " ^
3.256 -" (N__N:: bool) = " ^
3.257 -" (SubProblem (Biegelinie',[named,integrate,function], " ^
3.258 -" [diff,integration,named]) " ^
3.259 -" [REAL (rhs N__N), REAL v_v, REAL_REAL y']); " ^
3.260 -" (B__B:: bool) = " ^
3.261 -" (SubProblem (Biegelinie',[named,integrate,function], " ^
3.262 -" [diff,integration,named]) " ^
3.263 -" [REAL (rhs N__N), REAL v_v, REAL_REAL y]) " ^
3.264 + (prep_met thy "met_biege_ausbelast" [] e_metID
3.265 + (["Biegelinien", "ausBelastung"],
3.266 + [("#Given" ,["Streckenlast q__q", "FunktionsVariable v_v"]),
3.267 + ("#Find" ,["Funktionen fun_s"])],
3.268 + {rew_ord'="tless_true",
3.269 + rls' = append_rls "erls_ausBelastung" e_rls
3.270 + [Calc ("Atools.ident", eval_ident "#ident_"),
3.271 + Thm ("not_true", num_str @{thm not_true}),
3.272 + Thm ("not_false", num_str @{thm not_false})],
3.273 + calc = [],
3.274 + srls = append_rls "srls_ausBelastung" e_rls
3.275 + [Calc ("Tools.rhs", eval_rhs "eval_rhs_")],
3.276 + prls = e_rls, crls = Atools_erls, nrls = e_rls},
3.277 +"Script Belastung2BiegelScript (q__q::real) (v_v::real) = " ^
3.278 +" (let q___q = Take (qq v_v = q__q); " ^
3.279 +" q___q = ((Rewrite sym_neg_equal_iff_equal True) @@ " ^
3.280 +" (Rewrite Belastung_Querkraft True)) q___q; " ^
3.281 +" (Q__Q:: bool) = " ^
3.282 +" (SubProblem (Biegelinie',[named,integrate,function], " ^
3.283 +" [diff,integration,named]) " ^
3.284 +" [REAL (rhs q___q), REAL v_v, REAL_REAL Q]); " ^
3.285 +" M__M = Rewrite Querkraft_Moment True Q__Q; " ^
3.286 +" (M__M::bool) = " ^
3.287 +" (SubProblem (Biegelinie',[named,integrate,function], " ^
3.288 +" [diff,integration,named]) " ^
3.289 +" [REAL (rhs M__M), REAL v_v, REAL_REAL M_b]); " ^
3.290 +" N__N = ((Rewrite Moment_Neigung False) @@ " ^
3.291 +" (Rewrite make_fun_explicit False)) M__M; " ^
3.292 +" (N__N:: bool) = " ^
3.293 +" (SubProblem (Biegelinie',[named,integrate,function], " ^
3.294 +" [diff,integration,named]) " ^
3.295 +" [REAL (rhs N__N), REAL v_v, REAL_REAL y']); " ^
3.296 +" (B__B:: bool) = " ^
3.297 +" (SubProblem (Biegelinie',[named,integrate,function], " ^
3.298 +" [diff,integration,named]) " ^
3.299 +" [REAL (rhs N__N), REAL v_v, REAL_REAL y]) " ^
3.300 " in [Q__Q, M__M, N__N, B__B])"
3.301 ));
3.302
3.303 @@ -442,9 +440,9 @@
3.304 ML {*
3.305 store_met
3.306 (prep_met thy "met_biege_setzrand" [] e_metID
3.307 - (["Biegelinien","setzeRandbedingungenEin"],
3.308 - [("#Given" ,["Funktionen fun_s","Randbedingungen r_b"]),
3.309 - ("#Find" ,["Gleichungen equs'''"])],
3.310 + (["Biegelinien", "setzeRandbedingungenEin"],
3.311 + [("#Given" , ["Funktionen fun_s", "Randbedingungen r_b"]),
3.312 + ("#Find" , ["Gleichungen equs'''"])],
3.313 {rew_ord'="tless_true", rls'=Erls, calc = [],
3.314 srls = srls2,
3.315 prls=e_rls,
3.316 @@ -474,7 +472,7 @@
3.317 " (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
3.318 " [Equation,fromFunction]) " ^
3.319 " [BOOL (hd f_s), BOOL b_4]) " ^
3.320 -" in [e_1,e_2,e_3,e_4])"
3.321 +" in [e_1, e_2, e_3, e_4])"
3.322 (* filter requires more than 1 sec !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
3.323 "Script SetzeRandbedScript (fun_s::bool list) (r_b::bool list) = " ^
3.324 " (let b_1 = NTH 1 r_b; " ^
3.325 @@ -507,17 +505,15 @@
3.326 *}
3.327 ML {*
3.328 store_met
3.329 - (prep_met thy "met_equ_fromfun" [] e_metID
3.330 - (["Equation","fromFunction"],
3.331 - [("#Given" ,["functionEq fu_n","substitution su_b"]),
3.332 - ("#Find" ,["equality equ'''"])],
3.333 - {rew_ord'="tless_true", rls'=Erls, calc = [],
3.334 - srls = append_rls "srls_in_EquationfromFunc" e_rls
3.335 - [Calc("Tools.lhs", eval_lhs"eval_lhs_"),
3.336 - Calc("Atools.argument'_in",
3.337 - eval_argument_in
3.338 - "Atools.argument'_in")],
3.339 - prls=e_rls, crls = Atools_erls, nrls = e_rls},
3.340 + (prep_met thy "met_equ_fromfun" [] e_metID
3.341 + (["Equation","fromFunction"],
3.342 + [("#Given" ,["functionEq fu_n","substitution su_b"]),
3.343 + ("#Find" ,["equality equ'''"])],
3.344 + {rew_ord'="tless_true", rls'=Erls, calc = [],
3.345 + srls = append_rls "srls_in_EquationfromFunc" e_rls
3.346 + [Calc("Tools.lhs", eval_lhs"eval_lhs_"),
3.347 + Calc("Atools.argument'_in", eval_argument_in "Atools.argument'_in")],
3.348 + prls=e_rls, crls = Atools_erls, nrls = e_rls},
3.349 (*(M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2) (M_b L = 0) -->
3.350 0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2*)
3.351 "Script Function2Equality (fu_n::bool) (su_b::bool) =" ^
3.352 @@ -525,8 +521,9 @@
3.353 " bd_v = argument_in (lhs fu_n); " ^
3.354 " va_l = argument_in (lhs su_b); " ^
3.355 " eq_u = (Substitute [bd_v = va_l]) fu_n; " ^
3.356 -" eq_u = (Substitute [su_b]) fu_n " ^
3.357 -" in (Rewrite_Set norm_Rational False) eq_u) "
3.358 + (*([1], Res), M_b L = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2*)
3.359 +" eq_u = (Substitute [su_b]) eq_u " ^
3.360 +" in (Rewrite_Set norm_Rational False) eq_u) "
3.361 ));
3.362 *}
3.363
4.1 --- a/src/Tools/isac/Knowledge/Partial_Fractions.thy Thu Mar 08 14:33:34 2012 +0100
4.2 +++ b/src/Tools/isac/Knowledge/Partial_Fractions.thy Sat Mar 10 09:41:09 2012 +0100
4.3 @@ -105,12 +105,32 @@
4.4 equival_trans_4th_order: "(n/(a*b*c*d) = A/a + B/b + C/c + D/d) =
4.5 (n = A*b*c*d + B*a*c*d + C*a*b*d + D*a*b*c)" and
4.6 (*version 2: not yet used, see partial_fractions.sml*)
4.7 + multiply_2nd_order: "(n/x = A/a + B/b) = (a*b*n/x = A*b + B*a)" and
4.8 + multiply_3rd_order: "(n/x = A/a + B/b + C/c) = (a*b*c*n/x = A*b*c + B*a*c + C*a*b)" and
4.9 + multiply_4th_order:
4.10 + "(n/x = A/a + B/b + C/c + D/d) = (a*b*c*d*n/x = A*b*c*d + B*a*c*d + C*a*b*d + D*a*b*c)"
4.11 +
4.12 +text {* Probably the optimal formalization woudl be ...
4.13 +
4.14 multiply_2nd_order: "x = a*b ==> (n/x = A/a + B/b) = (a*b*n/x = A*b + B*a)" and
4.15 multiply_3rd_order: "x = a*b*c ==>
4.16 (n/x = A/a + B/b + C/c) = (a*b*c*n/x = A*b*c + B*a*c + C*a*b)" and
4.17 multiply_4th_order: "x = a*b*c*d ==>
4.18 (n/x = A/a + B/b + C/c + D/d) = (a*b*c*d*n/x = A*b*c*d + B*a*c*d + C*a*b*d + D*a*b*c)"
4.19
4.20 +... because it would allow to start the ansatz as follows
4.21 +(1) 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z))) = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))
4.22 +(2) 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z))) = AA / (z - 1 / 2) + BB / (z - -1 / 4)
4.23 +(3) (z - 1 / 2) * (z - -1 / 4) * 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z))) =
4.24 + (z - 1 / 2) * (z - -1 / 4) * AA / (z - 1 / 2) + BB / (z - -1 / 4)
4.25 +(4) 3 = A * (z - -1 / 4) + B * (z - 1 / 2)
4.26 +
4.27 +... (1==>2) ansatz
4.28 + (2==>3) multiply_*
4.29 + (3==>4) norm_Rational
4.30 +TODOs for this version ar in partial_fractions.sml "--- progr.vers.2: "
4.31 +*}
4.32 +
4.33 ML {*
4.34 val ansatz_rls = prep_rls(
4.35 Rls {id = "ansatz_rls", preconds = [], rew_ord = ("dummy_ord",dummy_ord),
5.1 --- a/test/Tools/isac/CLEANUP Thu Mar 08 14:33:34 2012 +0100
5.2 +++ b/test/Tools/isac/CLEANUP Sat Mar 10 09:41:09 2012 +0100
5.3 @@ -4,94 +4,100 @@
5.4 rm .#*
5.5 rm *.orig*
5.6 cd ADDTESTS
5.7 - rm *~
5.8 - rm #*
5.9 - rm .#*
5.10 - rm *.tar*
5.11 - rm *.orig*
5.12 - cd course
5.13 - rm *~
5.14 - rm #*
5.15 - rm .#*
5.16 - rm *.tar*
5.17 - rm *.orig*
5.18 - cd
5.19 - cd ml_quickstart
5.20 - rm *~
5.21 - rm #*
5.22 - rm .#*
5.23 - rm *.tar*
5.24 - rm *.orig*
5.25 - cd ..
5.26 - cd phst11
5.27 - rm *~
5.28 - rm #*
5.29 - rm .#*
5.30 - rm *.tar*
5.31 - rm *.orig*
5.32 - cd ..
5.33 - cd SignalProcess
5.34 - rm *~
5.35 - rm #*
5.36 - rm .#*
5.37 - rm *.tar*
5.38 - rm *.orig*
5.39 - cd ..
5.40 - cd ..
5.41 - cd file-depend
5.42 - rm *~
5.43 - rm #*
5.44 - rm .#*
5.45 - rm *.tar*
5.46 - rm *.orig*
5.47 - cd ..
5.48 - cd test-depend
5.49 - rm *~
5.50 - rm #*
5.51 - rm .#*
5.52 - rm *.tar*
5.53 - rm *.orig*
5.54 - cd ..
5.55 - cd ..
5.56 + rm *~
5.57 + rm #*
5.58 + rm .#*
5.59 + rm *.tar*
5.60 + rm *.orig*
5.61 + cd course
5.62 + rm *~
5.63 + rm #*
5.64 + rm .#*
5.65 + rm *.tar*
5.66 + rm *.orig*
5.67 + cd ml_quickstart
5.68 + rm *~
5.69 + rm #*
5.70 + rm .#*
5.71 + rm *.tar*
5.72 + rm *.orig*
5.73 + cd ..
5.74 + cd phst11
5.75 + rm *~
5.76 + rm #*
5.77 + rm .#*
5.78 + rm *.tar*
5.79 + rm *.orig*
5.80 + cd ..
5.81 + cd SignalProcess
5.82 + rm *~
5.83 + rm #*
5.84 + rm .#*
5.85 + rm *.tar*
5.86 + rm *.orig*
5.87 + cd ..
5.88 + cd ..
5.89 + cd file-depend
5.90 + rm *~
5.91 + rm #*
5.92 + rm .#*
5.93 + rm *.tar*
5.94 + rm *.orig*
5.95 + cd ..
5.96 + cd test-depend
5.97 + rm *~
5.98 + rm #*
5.99 + rm .#*
5.100 + rm *.tar*
5.101 + rm *.orig*
5.102 + cd ..
5.103 + cd ..
5.104 cd ProgLang
5.105 - rm *~
5.106 - rm #*
5.107 - rm .#*
5.108 - rm *.tar*
5.109 - rm *.orig*
5.110 - cd ..
5.111 + rm *~
5.112 + rm #*
5.113 + rm .#*
5.114 + rm *.tar*
5.115 + rm *.orig*
5.116 + cd ..
5.117 cd Minisubpbl
5.118 - rm *~
5.119 - rm #*
5.120 - rm .#*
5.121 - rm *.tar*
5.122 - rm *.orig*
5.123 - cd ..
5.124 + rm *~
5.125 + rm #*
5.126 + rm .#*
5.127 + rm *.tar*
5.128 + rm *.orig*
5.129 + cd ..
5.130 +cd OLDTESTS
5.131 + rm *~
5.132 + rm #*
5.133 + rm .#*
5.134 + rm *.tar*
5.135 + rm *.orig*
5.136 + cd ..
5.137 cd Interpret
5.138 - rm *~
5.139 - rm #*
5.140 - rm .#*
5.141 - rm *.tar*
5.142 - rm *.orig*
5.143 - cd ..
5.144 + rm *~
5.145 + rm #*
5.146 + rm .#*
5.147 + rm *.tar*
5.148 + rm *.orig*
5.149 + cd ..
5.150 cd xmlsrc
5.151 - rm *~
5.152 - rm #*
5.153 - rm .#*
5.154 - rm *.tar*
5.155 - rm *.orig*
5.156 - cd ..
5.157 + rm *~
5.158 + rm #*
5.159 + rm .#*
5.160 + rm *.tar*
5.161 + rm *.orig*
5.162 + cd ..
5.163 cd Frontend
5.164 - rm *~
5.165 - rm #*
5.166 - rm .#*
5.167 - rm *.tar*
5.168 - rm *.orig*
5.169 - cd ..
5.170 + rm *~
5.171 + rm #*
5.172 + rm .#*
5.173 + rm *.tar*
5.174 + rm *.orig*
5.175 + cd ..
5.176 cd Knowledge
5.177 - rm *~
5.178 - rm #*
5.179 - rm .#*
5.180 - rm *.tar*
5.181 - rm *.orig*
5.182 - cd ..
5.183 + rm *~
5.184 + rm #*
5.185 + rm .#*
5.186 + rm *.tar*
5.187 + rm *.orig*
5.188 + cd ..
6.1 --- a/test/Tools/isac/Interpret/script.sml Thu Mar 08 14:33:34 2012 +0100
6.2 +++ b/test/Tools/isac/Interpret/script.sml Sat Mar 10 09:41:09 2012 +0100
6.3 @@ -135,10 +135,9 @@
6.4 val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.5 case nxt of (_, Apply_Method ["IntegrierenUndKonstanteBestimmen"]) => ()
6.6 | _ => error "script.sml, doesnt find Substitute #2";
6.7 -
6.8 -(*========== inhibit exn AK110721 ================================================
6.9 (* ERROR: caused by f2str f *)
6.10 trace_rewrite:=true;
6.11 +
6.12 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f(*------------------------*);
6.13 trace_rewrite:=false;
6.14 (*Exception TYPE raised:
6.15 @@ -155,22 +154,12 @@
6.16 ... this was because eval_argument_in took "argument_in (lhs (M_b 0 = 0))"
6.17 ie. the argument had not been simplified before ^^^^^^^^^^^^^^^
6.18 thus corrected eval_argument_in OK*)
6.19 -========== inhibit exn AK110721 ================================================*)
6.20 -
6.21 val {srls,...} = get_met ["IntegrierenUndKonstanteBestimmen"];
6.22 -val e1__e1 = str2term "nth_nth 1 [M_b 0 = 0, M_b L = 0]";
6.23 +val e1__e1 = str2term "NTH 1 [M_b 0 = 0, M_b L = 0]";
6.24 val e1__e1 = eval_listexpr_ @{theory Biegelinie} srls e1__e1; term2str e1__e1;
6.25 -
6.26 -(*========== inhibit exn 110721 ================================================
6.27 -(*AK110722
6.28 - TRIAL: Should be the same
6.29 - term2str e1__e1 = "M_b 0 = 0";
6.30 - term2str e1__e1;*)
6.31 -
6.32 if term2str e1__e1 = "M_b 0 = 0"
6.33 then ()
6.34 else error"script.sml diff.beh. eval_listexpr_ nth_nth 1 [...";
6.35 -========== inhibit exn 110721 ================================================*)
6.36
6.37 (*TODO.WN050913 ??? doesnt eval_listexpr_ go into subterms ???...
6.38 val x1__ = str2term"argument_in (lhs (M_b 0 = 0))";
6.39 @@ -180,16 +169,13 @@
6.40 val SOME (str, t) = eval_lhs 0 "Tools.lhs" (str2term"lhs (M_b 0 = 0)") 0;*)
6.41
6.42 val l__l = str2term "lhs (M_b 0 = 0)";
6.43 -(*AK110722 eval_listexpr_ is prob. without _ ????*)
6.44 val l__l = eval_listexpr_ @{theory Biegelinie} srls l__l; term2str l__l;
6.45 val SOME (str, t) = eval_lhs 0 "Tools.lhs" (str2term "lhs (M_b 0 = 0)") 0;
6.46 -(*========== inhibit exn 110721 ================================================
6.47 -trace_rewrite:=true;
6.48 +
6.49 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f (*------------------------*);
6.50 -trace_rewrite:=false;
6.51 -========== inhibit exn 110721 ================================================*)
6.52 +if nxt = ("Rewrite", Rewrite ("Belastung_Querkraft", "Biegelinie.Belastung_Querkraft"))
6.53 +then () else error "";
6.54
6.55 -show_mets();
6.56
6.57 "----------- fun sel_appl_atomic_tacs ----------------------------";
6.58 "----------- fun sel_appl_atomic_tacs ----------------------------";
7.1 --- a/test/Tools/isac/Knowledge/biegelinie.sml Thu Mar 08 14:33:34 2012 +0100
7.2 +++ b/test/Tools/isac/Knowledge/biegelinie.sml Sat Mar 10 09:41:09 2012 +0100
7.3 @@ -14,7 +14,6 @@
7.4 "----------- SubProblem (_,[vonBelastungZu,Biegelinien] ----------";
7.5 "----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
7.6 "----------- method [Biegelinien,setzeRandbedingungenEin] + exec -";
7.7 -"----------- method [Biegelinien,setzeRandbedingungenEin]FAST ----";
7.8 "----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. --------";
7.9 "----------- investigate normalforms in biegelinien --------------";
7.10 "-----------------------------------------------------------------";
7.11 @@ -136,7 +135,6 @@
7.12 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
7.13 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
7.14
7.15 -(*=== inhibit exn 110722=============================================================
7.16 case nxt of
7.17 (_,Subproblem ("Biegelinie", ["named", "integrate", "function"])) => ()
7.18 | _ => error "biegelinie.sml: Bsp 7.27 #4c";
7.19 @@ -325,7 +323,6 @@
7.20 else error "biegelinie.sml: Bsp 7.27 #24 f";
7.21 case nxt of ("End_Proof'", End_Proof') => ()
7.22 | _ => error "biegelinie.sml: Bsp 7.27 #24";
7.23 -=== inhibit exn 110722=============================================================*)
7.24
7.25 show_pt pt;
7.26 (*(([], Frm), Problem (Biegelinie.thy, [MomentBestimmte, Biegelinien])),
7.27 @@ -397,12 +394,10 @@
7.28
7.29 autoCalculate 1 CompleteCalc;
7.30 val ((pt,p),_) = get_calc 1;
7.31 -(*=== inhibit exn 110722=============================================================
7.32 if p = ([], Res) andalso length (children pt) = 23 andalso
7.33 term2str (get_obj g_res pt (fst p)) =
7.34 "y x =\n-1 * q_0 * L ^^^ 4 / (-24 * EI * L) * x +\n(2 * L * q_0 / (-1 * 24 * EI) * x ^^^ 3 +\n -1 * q_0 / (-1 * 24 * EI) * x ^^^ 4)"
7.35 then () else error "biegelinie.sml: 1st biegelin.7.27 changed";
7.36 -=== inhibit exn 110722=============================================================*)
7.37
7.38 val (unc, del, gen) = (([],Pbl), ([],Pbl), ([],Res));
7.39 getFormulaeFromTo 1 unc gen 1 (*only level 1*) false;
7.40 @@ -436,7 +431,7 @@
7.41 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.42 if nxt = ("Apply_Method", Apply_Method ["Biegelinien", "ausBelastung"])
7.43 then () else error "biegelinie.sml met2 b";
7.44 -(*=== inhibit exn 110722=============================================================
7.45 +(*=== inhibit exn 110722=============================================================*)
7.46
7.47 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "q_ x = q_0";
7.48 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "- q_ x = - q_0";
7.49 @@ -496,58 +491,14 @@
7.50 if nxt = ("End_Proof'", End_Proof') andalso f2str f =
7.51 "[Q x = c + -1 * q_0 * x, M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2,\n y' x =\n c_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3),\n y x =\n c_4 + c_3 * x +\n 1 / (-1 * EI) *\n (c_2 / 2 * x ^^^ 2 + c / 6 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)]" then ()
7.52 else error "biegelinie.sml met2 e";
7.53 -=== inhibit exn 110722=============================================================*)
7.54 -
7.55
7.56
7.57 "----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
7.58 "----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
7.59 "----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
7.60 -val str =
7.61 -"Script Function2Equality (fun_::bool) (sub_::bool) =\
7.62 -\(equ___::bool)"
7.63 -;
7.64 -(*=== inhibit exn 110722=============================================================
7.65 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
7.66 -val str =
7.67 -"Script Function2Equality (fun_::bool) (sub_::bool) =\
7.68 -\ (let v_v = argument_in (lhs fun_)\
7.69 -\ in (equ___::bool))"
7.70 -;
7.71 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
7.72 -val str =
7.73 -"Script Function2Equality (fun_::bool) (sub_::bool) =\
7.74 -\ (let v_v = argument_in (lhs fun_);\
7.75 -\ (equ_) = (Substitute [sub_]) fun_\
7.76 -\ in (equ_::bool))"
7.77 -;
7.78 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
7.79 -val str =
7.80 -"Script Function2Equality (fun_::bool) (sub_::bool) =\
7.81 -\ (let v_v = argument_in (lhs fun_);\
7.82 -\ equ_ = (Substitute [sub_]) fun_\
7.83 -\ in (Rewrite_Set_Inst [(bdv, v_v)] make_ratpoly_in False) equ_)"
7.84 -;
7.85 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
7.86 -=== inhibit exn 110722=============================================================*)
7.87 -
7.88 -val str =
7.89 -(*(M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2) (M_b L = 0) -->
7.90 - 0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2*)
7.91 -"Script Function2Equality (fun_::bool) (sub_::bool) =\
7.92 -\ (let bdv_ = argument_in (lhs fun_);\
7.93 -\ val_ = argument_in (lhs sub_);\
7.94 -\ equ_ = (Substitute [bdv_ = val_]) fun_;\
7.95 -\ equ_ = (Substitute [sub_]) fun_\
7.96 -\ in (Rewrite_Set_Inst [(bdv_, v_v)] make_ratpoly_in False) equ_)"
7.97 -;
7.98 -(*=== inhibit exn 110722=============================================================
7.99 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
7.100 -atomty sc;
7.101 -
7.102 val fmz = ["functionEq (M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2)",
7.103 "substitution (M_b L = 0)",
7.104 - "equality equ___"];
7.105 + "equality equ_equ"];
7.106 val (dI',pI',mI') = ("Biegelinie", ["makeFunctionTo","equation"],
7.107 ["Equation","fromFunction"]);
7.108 val p = e_pos'; val c = [];
7.109 @@ -570,80 +521,23 @@
7.110 CHANGE NOT considered, already on leave*)
7.111 f2str f = "0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2"
7.112 then () else error "biegelinie.sml: SubProblem (_,[setzeRandbed";
7.113 -=== inhibit exn 110722=============================================================*)
7.114
7.115
7.116 "----------- method [Biegelinien,setzeRandbedingungenEin] + exec -";
7.117 "----------- method [Biegelinien,setzeRandbedingungenEin] + exec -";
7.118 "----------- method [Biegelinien,setzeRandbedingungenEin] + exec -";
7.119 "----- check the scripts syntax";
7.120 -val str =
7.121 -"Script SetzeRandbedScript (funs_::bool list) (beds_::bool list) =\
7.122 -\ (let b1 = Take (nth_ 1 beds_)\
7.123 -\ in (equs_::bool list))"
7.124 -;
7.125 -(*=== inhibit exn 110722=============================================================
7.126 -
7.127 -(*show_types := true;*)
7.128 -val funs_ = str2term "funs_::bool list";
7.129 -val funs = str2term
7.130 - "[Q x = c + -1 * q_0 * x,\
7.131 - \M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2,\
7.132 - \y' x = c_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3),\
7.133 - \y x = c_4 + c_3 * x + 1 / (-1 * EI) * (c_2 / 2 * x ^^^ 2 + c / 6 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)]";
7.134 -val rb_ = str2term "rb_::bool list";
7.135 -val rb = str2term "[y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]";
7.136 -
7.137 -"--- script expression 1";
7.138 -val screxp1_ = str2term "Take (nth_ 1 (rb_::bool list))";
7.139 -val screxp1 = subst_atomic [(rb_, rb)] screxp1_; term2str screxp1;
7.140 -val SOME (b1,_) = rewrite_set_ (theory "Isac") false srls2 screxp1; term2str b1;
7.141 -if term2str b1 = "Take (y 0 = 0)" then ()
7.142 -else error "biegelinie.sml: rew. Bieglie2 --1";
7.143 -val b1 = str2term "(y 0 = 0)";
7.144 -
7.145 -"--- script expression 2";
7.146 -val screxp2_ = str2term "filter (sameFunId (lhs b1_)) funs_";
7.147 -val b1_ = str2term "b1_::bool";
7.148 -val screxp2 = subst_atomic [(b1_,b1),(funs_,funs)] screxp2_; term2str screxp2;
7.149 -val SOME (fs,_) = rewrite_set_ (theory "Isac") false srls2 screxp2; term2str fs;
7.150 -if term2str fs = "[y x =\n c_4 + c_3 * x +\n 1 / (-1 * EI) *\n (c_2 / 2 * x ^^^ 2 + c / 6 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)]" then ()
7.151 -else error "biegelinie.sml: rew. Bieglie2 --2";
7.152 -
7.153 -"--- script expression 3";
7.154 -val screxp3_ = str2term "SubProblem (Biegelinie_,[makeFunctionTo,equation],\
7.155 -\ [Equation,fromFunction]) \
7.156 -\ [BOOL (hd fs_), BOOL b1_]";
7.157 -val fs_ = str2term "fs_::bool list";
7.158 -val screxp3 = subst_atomic [(fs_,fs),(b1_,b1)] screxp3_;
7.159 -writeln (term2str screxp3);
7.160 -val SOME (equ,_) = rewrite_set_ (theory "Isac") false srls2 screxp3;
7.161 -if term2str equ = "SubProblem\n (Biegelinie_, [makeFunctionTo, equation], [Equation, fromFunction])\n [BOOL\n (y x =\n c_4 + c_3 * x +\n 1 / (-1 * EI) *\n (c_2 / 2 * x ^^^ 2 + c / 6 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)),\n BOOL (y 0 = 0)]" then ()
7.162 -else error "biegelinie.sml: rew. Bieglie2 --3";
7.163 -writeln (term2str equ);
7.164 -(*SubProblem
7.165 - (Biegelinie_, [makeFunctionTo, equation], [Equation, fromFunction])
7.166 - [BOOL
7.167 - (y x =
7.168 - c_4 + c_3 * x +
7.169 - 1 / (-1 * EI) *
7.170 - (c_2 / 2 * x ^^^ 2 + c / 6 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)),
7.171 - BOOL (y 0 = 0)]*)
7.172 -show_types := false;
7.173 -=== inhibit exn 110722=============================================================*)
7.174 -
7.175 -
7.176 +(*WN120309 deleted*)
7.177 "----- execute script by interpreter: setzeRandbedingungenEin";
7.178 -val fmz = ["Funktionen [Q x = c + -1 * q_0 * x,\
7.179 - \M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2,\
7.180 - \y' x = c_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3),\
7.181 - \y x = c_4 + c_3 * x + 1 / (-1 * EI) * (c_2 / 2 * x ^^^ 2 + c / 6 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)]",
7.182 +val fmz = ["Funktionen [Q x = c + -1 * q_0 * x," ^
7.183 + "M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2," ^
7.184 + "y' x = c_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)," ^
7.185 + "y x = c_4 + c_3 * x + 1 / (-1 * EI) * (c_2 / 2 * x ^^^ 2 + c / 6 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)]",
7.186 "Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]",
7.187 - "Gleichungen equs___"];
7.188 + "Gleichungen equ_s"];
7.189 val (dI',pI',mI') = ("Biegelinie", ["setzeRandbedingungen","Biegelinien"],
7.190 ["Biegelinien","setzeRandbedingungenEin"]);
7.191 val p = e_pos'; val c = [];
7.192 -(*=== inhibit exn 110722=============================================================
7.193 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
7.194 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.195 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.196 @@ -657,8 +551,9 @@
7.197 "----- Randbedingung y 0 = 0 in SUBpbl with met [Equation, fromFunction]";
7.198 val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.199 if (#1 o (get_obj g_fmz pt)) (fst p) =
7.200 - ["functionEq\n (y x =\n c_4 + c_3 * x +\n 1 / (-1 * EI) *\n (c_2 / 2 * x ^^^ 2 + c / 6 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4))",
7.201 - "substitution (y 0 = 0)", "equality equ___"] then ()
7.202 + ["functionEq\n (y x =\n c_4 + c_3 * x +\n 1 / (-1 * EI) *" ^
7.203 + "\n (c_2 / 2 * x ^^^ 2 + c / 6 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4))",
7.204 + "substitution (y 0 = 0)", "equality equ'''"] then ()
7.205 else error "biegelinie.sml met setzeRandbed*Ein bb";
7.206 (writeln o istate2str) (get_istate pt p);
7.207 "--- after 1.subpbl [Equation, fromFunction]";
7.208 @@ -685,7 +580,7 @@
7.209 val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.210 if (#1 o (get_obj g_fmz pt)) (fst p) =
7.211 ["functionEq\n (y x =\n c_4 + c_3 * x +\n 1 / (-1 * EI) *\n (c_2 / 2 * x ^^^ 2 + c / 6 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4))",
7.212 - "substitution (y L = 0)", "equality equ___"] then ()
7.213 + "substitution (y L = 0)", "equality equ'''"] then ()
7.214 else error "biegelinie.sml metsetzeRandbed*Ein bb ";
7.215 val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.216 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.217 @@ -736,63 +631,10 @@
7.218 (* "[0 = c_4,\n 0 =\n c_4 + L * c_3 +\n (12 * L ^^^ 2 * c_2 + 4 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) / (-24 * EI),\n 0 = c_2, 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2]" *)
7.219 "[0 = c_4,\n 0 =\n c_4 + L * c_3 +\n (12 * L ^^^ 2 * c_2 + 4 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) /\n (-1 * EI * 24),\n 0 = c_2, 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2]"
7.220 then () else error "biegelinie.sml met2 oo";
7.221 -=== inhibit exn 110722=============================================================*)
7.222 -
7.223 -(*
7.224 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
7.225 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.226 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.227 -*)
7.228 -
7.229 -"----------- method [Biegelinien,setzeRandbedingungenEin]FAST ----";
7.230 -"----------- method [Biegelinien,setzeRandbedingungenEin]FAST ----";
7.231 -"----------- method [Biegelinien,setzeRandbedingungenEin]FAST ----";
7.232 -val str =
7.233 -"Script SetzeRandbedScript (funs_::bool list) (rb_::bool list) = \
7.234 -\ (let b1_ = nth_ 1 rb_; \
7.235 -\ (fs_::bool list) = filter_sameFunId (lhs b1_) funs_; \
7.236 -\ (e1_::bool) = \
7.237 -\ (SubProblem (Biegelinie_,[makeFunctionTo,equation],\
7.238 -\ [Equation,fromFunction]) \
7.239 -\ [BOOL (hd fs_), BOOL b1_]) \
7.240 -\ in [e1_,e2_,e3_,e4_])"
7.241 -;
7.242 -
7.243 -
7.244
7.245 "----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. --------";
7.246 "----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. --------";
7.247 "----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. --------";
7.248 -"----- script ";
7.249 -val str =
7.250 -"Script Belastung2BiegelScript (q__::real) (v_v::real) = \
7.251 -\ (let q___ = Take (q_ v_v = q__); \
7.252 -\ q___ = ((Rewrite sym_real_minus_eq_cancel True) @@ \
7.253 -\ (Rewrite Belastung_Querkraft True)) q___; \
7.254 -\ (Q__:: bool) = \
7.255 -\ (SubProblem (Biegelinie_,[named,integrate,function], \
7.256 -\ [diff,integration,named]) \
7.257 -\ [REAL (rhs q___), REAL v_v, real_REAL Q]); \
7.258 -\ M__ = Rewrite Querkraft_Moment True Q__; \
7.259 -\ (M__::bool) = \
7.260 -\ (SubProblem (Biegelinie_,[named,integrate,function], \
7.261 -\ [diff,integration,named]) \
7.262 -\ [REAL (rhs M__), REAL v_v, real_REAL M_b]); \
7.263 -\ N__ = ((Rewrite Moment_Neigung False) @@ \
7.264 -\ (Rewrite make_fun_explicit False)) M__; \
7.265 -\ (N__:: bool) = \
7.266 -\ (SubProblem (Biegelinie_,[named,integrate,function], \
7.267 -\ [diff,integration,named]) \
7.268 -\ [REAL (rhs N__), REAL v_v, real_REAL y']); \
7.269 -\ (B__:: bool) = \
7.270 -\ (SubProblem (Biegelinie_,[named,integrate,function], \
7.271 -\ [diff,integration,named]) \
7.272 -\ [REAL (rhs N__), REAL v_v, real_REAL y]) \
7.273 -\ in [Q__, M__, N__, B__])"
7.274 -;
7.275 -(*=== inhibit exn 110722=============================================================
7.276 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
7.277 -
7.278 "----- Bsp 7.70 with me";
7.279 val fmz = ["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
7.280 "Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]",
7.281 @@ -812,21 +654,21 @@
7.282 (*** actual arg(s) missing for '["(#Find, (Funktionen, funs_))"]' i.e. should be 'copy-named' by '*_._'
7.283 ... THIS MEANS:
7.284 #a# "Script Biegelinie2Script ..
7.285 -\ ... (SubProblem (Biegelinie_,[vonBelastungZu,Biegelinien], \
7.286 -\ [Biegelinien,ausBelastung]) \
7.287 -\ [REAL q__, REAL v_]); \
7.288 +" ... (SubProblem (Biegelinie_,[vonBelastungZu,Biegelinien], " ^
7.289 +" [Biegelinien,ausBelastung]) " ^
7.290 +" [REAL q__, REAL v_]); "
7.291
7.292 #b# prep_met ... (["Biegelinien","ausBelastung"],
7.293 ... ("#Given" ,["Streckenlast q__","FunktionsVariable v_v"]),
7.294 - "Script Belastung2BiegelScript (q__::real) (v_v::real) = \
7.295 + "Script Belastung2BiegelScript (q__::real) (v_v::real) = "
7.296
7.297 #a#b# BOTH HAVE 2 ARGUMENTS q__ and v_v ...OK
7.298 ##########################################################################
7.299 BUT THE (#Find, (Funktionen, funs_)) IS NOT COPYNAMED BY funs___ !!!3*_!!!
7.300 ##########################################################################*)
7.301 -=== inhibit exn 110722=============================================================*)
7.302 -"further 'me' see ----- SubProblem (_,[vonBelastungZu,Biegelinien] -------\
7.303 -\ ----- SubProblem (_,[setzeRandbedingungen,Biegelinien] -";
7.304 +"further 'me' see ----- SubProblem (_,[vonBelastungZu,Biegelinien] -------" ^
7.305 +" ----- SubProblem (_,[setzeRandbedingungen,Biegelinien] -";
7.306 +
7.307 DEconstrCalcTree 1;
7.308 "----- Bsp 7.70 with autoCalculate";
7.309 CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
7.310 @@ -837,23 +679,21 @@
7.311 moveActiveRoot 1;
7.312 autoCalculate 1 CompleteCalc;
7.313 val ((pt,p),_) = get_calc 1; show_pt pt;
7.314 -(*=== inhibit exn 110722=============================================================
7.315 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) =
7.316 "y x =\n-6 * q_0 * L ^^^ 2 / (-24 * EI) * x ^^^ 2 +\n4 * L * q_0 / (-24 * EI) * x ^^^ 3 +\n-1 * q_0 / (-24 * EI) * x ^^^ 4" then ()
7.317 else error "biegelinie.sml: diff.behav.7.70 with autoCalculate";
7.318 -===== inhibit exn 110722===========================================================*)
7.319
7.320 val is = get_istate pt ([],Res); writeln (istate2str is);
7.321 -val t = str2term " last \
7.322 -\[Q x = L * q_0 + -1 * q_0 * x, \
7.323 -\ M_b x = -1 * q_0 * L ^^^ 2 / 2 + q_0 * L / 1 * x + -1 * q_0 / 2 * x ^^^ 2,\
7.324 -\ y' x = \
7.325 -\ -3 * q_0 * L ^^^ 2 / (-6 * EI) * x + 3 * L * q_0 / (-6 * EI) * x ^^^ 2 +\
7.326 -\ -1 * q_0 / (-6 * EI) * x ^^^ 3, \
7.327 -\ y x = \
7.328 -\ -6 * q_0 * L ^^^ 2 / (-24 * EI) * x ^^^ 2 + \
7.329 -\ 4 * L * q_0 / (-24 * EI) * x ^^^ 3 + \
7.330 -\ -1 * q_0 / (-24 * EI) * x ^^^ 4]";
7.331 +val t = str2term (" last " ^
7.332 +"[Q x = L * q_0 + -1 * q_0 * x, " ^
7.333 +" M_b x = -1 * q_0 * L ^^^ 2 / 2 + q_0 * L / 1 * x + -1 * q_0 / 2 * x ^^^ 2," ^
7.334 +" y' x = " ^
7.335 +" -3 * q_0 * L ^^^ 2 / (-6 * EI) * x + 3 * L * q_0 / (-6 * EI) * x ^^^ 2 +" ^
7.336 +" -1 * q_0 / (-6 * EI) * x ^^^ 3, " ^
7.337 +" y x = " ^
7.338 +" -6 * q_0 * L ^^^ 2 / (-24 * EI) * x ^^^ 2 + " ^
7.339 +" 4 * L * q_0 / (-24 * EI) * x ^^^ 3 + " ^
7.340 +" -1 * q_0 / (-24 * EI) * x ^^^ 4]");
7.341 val srls = append_rls "erls_IntegrierenUndK.." e_rls
7.342 [Calc("Tools.rhs", eval_rhs"eval_rhs_"),
7.343 Calc ("Atools.ident",eval_ident "#ident_"),
7.344 @@ -868,8 +708,6 @@
7.345 trace_rewrite := false;
7.346 term2str e1__;
7.347
7.348 -trace_script := true;
7.349 -trace_script := false;
7.350
7.351 "----------- investigate normalforms in biegelinien --------------";
7.352 "----------- investigate normalforms in biegelinien --------------";
8.1 --- a/test/Tools/isac/Knowledge/polyeq.sml Thu Mar 08 14:33:34 2012 +0100
8.2 +++ b/test/Tools/isac/Knowledge/polyeq.sml Sat Mar 10 09:41:09 2012 +0100
8.3 @@ -200,15 +200,15 @@
8.4 l = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*false*);
8.5 (*WAS val NasApp _ =(astep_up (thy',srls,scr,d) ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]) )
8.6 ... Assoc ... is correct*)
8.7 -"~~~~~ and astep_up, args:"; val ((ys as (_,_,Script sc,_)), ((E,l,a,v,S,b),ss)) =
8.8 - ((thy',srls,scr,d), ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]));
8.9 +"~~~~~ and astep_up, args:"; val ((ys as (_,_,_,Script sc,_)), ((E,l,a,v,S,b),ss)) =
8.10 + ((thy',ctxt,srls,scr,d), ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]));
8.11 1 < length l (*true*);
8.12 val up = drop_last l;
8.13 term2str (go up sc);
8.14 (go up sc);
8.15 (*WAS val NasNap _ = ass_up ys ((E,up,a,v,S,b),ss) (go up sc)
8.16 ... ???? ... is correct*)
8.17 -"~~~~~ fun ass_up, args:"; val ((ys as (y,s,Script sc,d)), (is as (E,l,a,v,S,b),ss),
8.18 +"~~~~~ fun ass_up, args:"; val ((ys as (y,ctxt,s,Script sc,d)), (is as (E,l,a,v,S,b),ss),
8.19 (Const ("HOL.Let",_) $ _)) = (ys, ((E,up,a,v,S,b),ss), (go up sc));
8.20 val l = drop_last l; (*comes from e, goes to Abs*)
8.21 val (Const ("HOL.Let",_) $ e $ (Abs (i,T,body))) = go l sc;
9.1 --- a/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml Thu Mar 08 14:33:34 2012 +0100
9.2 +++ b/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml Sat Mar 10 09:41:09 2012 +0100
9.3 @@ -34,6 +34,7 @@
9.4 val ctxt = get_ctxt pt p;
9.5 val SOME t = parseNEW ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
9.6 get_loc pt p |> snd |> is_e_ctxt; (*false*)
9.7 +
9.8 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*);
9.9 get_ctxt pt p |> is_e_ctxt; (*false*)
9.10 val ctxt = get_ctxt pt p;
10.1 --- a/test/Tools/isac/Test_Isac.thy Thu Mar 08 14:33:34 2012 +0100
10.2 +++ b/test/Tools/isac/Test_Isac.thy Sat Mar 10 09:41:09 2012 +0100
10.3 @@ -22,7 +22,7 @@
10.4 "../../Pure/Isar/Test_Parsers"
10.5 (*"../../Pure/Isar/Pure/Isar/Struct_Deriv" update 2009-2-->2011*)
10.6 "../../Pure/Isar/Test_Parse_Term"
10.7 -
10.8 +
10.9 uses
10.10 ( "library.sml")
10.11 ( "calcelems.sml")
10.12 @@ -174,7 +174,7 @@
10.13 use "Knowledge/polyminus.sml" (*part.*)
10.14 use "Knowledge/vect.sml"
10.15 use "Knowledge/diffapp.sml" (*part.*)
10.16 - use "Knowledge/biegelinie.sml" (*part.*)
10.17 + use "Knowledge/biegelinie.sml"
10.18 use "Knowledge/algein.sml"
10.19 use "Knowledge/diophanteq.sml"
10.20 use "Knowledge/isac.sml" (*part.*)
11.1 --- a/test/Tools/isac/Test_Some.thy Thu Mar 08 14:33:34 2012 +0100
11.2 +++ b/test/Tools/isac/Test_Some.thy Sat Mar 10 09:41:09 2012 +0100
11.3 @@ -5,22 +5,8 @@
11.4
11.5 ML {*
11.6 *}
11.7 -ML {*
11.8 -*}
11.9 -ML {*
11.10 -*}
11.11 -ML {*
11.12 -*}
11.13 -ML {*
11.14 -*}
11.15 -ML {*
11.16 -*}
11.17 ML {* (*==================*)
11.18 *}
11.19 -ML {*
11.20 -*}
11.21 -ML {*
11.22 -*}
11.23 ML {*
11.24 *}
11.25 ML {*
11.26 @@ -31,15 +17,15 @@
11.27 *}
11.28 ML {*
11.29 *}
11.30 -ML {*
11.31 +ML {* (*==================*)
11.32 *}
11.33 ML {*
11.34 "~~~~~ fun , args:"; val () = ();
11.35 *}
11.36 end
11.37
11.38 -(*============ inhibit exn WN120306 ==============================================
11.39 -============ inhibit exn WN120306 ==============================================*)
11.40 +(*============ inhibit exn WN120309 ==============================================
11.41 +============ inhibit exn WN120309 ==============================================*)
11.42
11.43 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
11.44 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
12.1 --- a/test/Tools/isac/thms-survey-Isa02-Isa09-2.sml Thu Mar 08 14:33:34 2012 +0100
12.2 +++ b/test/Tools/isac/thms-survey-Isa02-Isa09-2.sml Sat Mar 10 09:41:09 2012 +0100
12.3 @@ -74,14 +74,17 @@
12.4 ("sym_rmult_assoc", "?m1 * (?n1 * ?k1) = ?m1 * ?n1 * ?k1" [.])] + see sym_real_mult_assoc
12.5 : (thmID * Thm.thm) list
12.6 "real_divide_minus1", "?x / -1 = - ?x" Int.divide_minus1
12.7 + "real_minus_eq_cancel", "(- ?a = - ?b) = (?a = ?b)" Groups.group_add_class.neg_equal_iff_equal:
12.8
12.9 -find_theorems
12.10 +-----------------------------------------------------------------------------------------------------------------
12.11 +find_theorems: in emacs
12.12 (999) name :
12.13 (999) simp : "?a * (?b + ?c)"
12.14 Tobias Nipkow 'searched for' ... "_ + _ + _ = _ + (_ + _)"
12.15 "_ + (_ + (_::nat)) = _ + _ + _"
12.16
12.17
12.18 +-----------------------------------------------------------------------------------------------------------------
12.19 list funs:
12.20 nth_Cons_ NTH_CONS
12.21 nth_Nil_ NTH_NIL