1.1 --- a/src/Tools/isac/Interpret/ctree.sml Wed Mar 07 15:58:18 2012 +0100
1.2 +++ b/src/Tools/isac/Interpret/ctree.sml Sat Mar 10 14:38:18 2012 +0100
1.3 @@ -226,8 +226,8 @@
1.4 val subte2sube = map term2str;
1.5 val subst2subs = map (pair2str o (apfst term2str) o (apsnd term2str));
1.6 val subst2subs' = map ((apfst term2str) o (apsnd term2str));
1.7 -fun subs2subst thy s = map (isapair2pair o term_of o the o (parse thy)) s;
1.8 -fun sube2subst thy s = map (dest_equals' o term_of o the o (parse thy)) s;
1.9 +fun subs2subst thy s = map (isapair2pair o (parse_patt thy)) s;
1.10 +fun sube2subst thy s = map (dest_equals' o (parse_patt thy)) s;
1.11 val sube2subte = map str2term;
1.12 val subte2subst = map HOLogic.dest_eq;
1.13
2.1 --- a/src/Tools/isac/Interpret/mathengine.sml Wed Mar 07 15:58:18 2012 +0100
2.2 +++ b/src/Tools/isac/Interpret/mathengine.sml Sat Mar 10 14:38:18 2012 +0100
2.3 @@ -398,7 +398,7 @@
2.4 | ("not-applicable",_) => (pt, p)
2.5 | ("end-of-calculation", (_, _, ptp)) => ptp
2.6 | ("failure",_) => error "sys-error";
2.7 - val (_, ts) = (*WN101102 TODO: locatetac + step create _same_ (pt,p) ?*)
2.8 + val (_, ts) =
2.9 (case step p ((pt, e_pos'),[]) of
2.10 ("ok", (ts as (tac,_,_)::_, _, _)) => ("",ts)
2.11 | ("helpless",_) => ("helpless: cannot propose tac", [])
3.1 --- a/src/Tools/isac/Interpret/script.sml Wed Mar 07 15:58:18 2012 +0100
3.2 +++ b/src/Tools/isac/Interpret/script.sml Sat Mar 10 14:38:18 2012 +0100
3.3 @@ -1068,22 +1068,17 @@
3.4
3.5 | ass_up (ysa as (y,ctxt,s,Script sc,d)) (is as (E,l,a,v,S,b),ss)
3.6 (Const ("Script.Seq",_) $ _ ) = (*2*: comes from e1, goes to e2*)
3.7 - (* val ((ysa as (y,s,Script sc,d)), (is as (E,l,a,v,S,b),ss),
3.8 - (Const ("Script.Seq",_) $ _ )) =
3.9 - (ys, ((E,up,a,v,S,b),ss), (go up sc));
3.10 - *)
3.11 - let val up = drop_last l;
3.12 - val Const ("Script.Seq",_) $ _ $ e2 = go up sc
3.13 - (*val _= tracing("### ass_up Seq$e: is=")
3.14 - val _= tracing(istate2str (ScrState is))*)
3.15 - in case assy (y,ctxt,s,d,Aundef) ((E, up@[R], a,v,S,b),ss) e2 of
3.16 - NasNap (v,E) => astep_up ysa ((E,up,a,v,S,b),ss)
3.17 - | NasApp iss => astep_up ysa iss
3.18 - | ay => ay end
3.19 + let
3.20 + val up = drop_last l;
3.21 + val Const ("Script.Seq",_) $ _ $ e2 = go up sc
3.22 + (*val _= tracing("### ass_up Seq$e: is=")
3.23 + val _= tracing(istate2str (ScrState is))*)
3.24 + in
3.25 + case assy (y,ctxt,s,d,Aundef) ((E, up@[R], a,v,S,b),ss) e2 of
3.26 + NasNap (v,E) => astep_up ysa ((E,up,a,v,S,b),ss)
3.27 + | NasApp iss => astep_up ysa iss
3.28 + | ay => ay end
3.29
3.30 - (* val (ysa, iss, (Const ("Script.Try",_) $ e $ _)) =
3.31 - (ys, ((E,up,a,v,S,b),ss), (go up sc));
3.32 - *)
3.33 | ass_up ysa iss (Const ("Script.Try",_) $ e $ _) =
3.34 astep_up ysa iss
3.35
4.1 --- a/src/Tools/isac/Knowledge/Biegelinie.thy Wed Mar 07 15:58:18 2012 +0100
4.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy Sat Mar 10 14:38:18 2012 +0100
4.3 @@ -8,7 +8,7 @@
4.4
4.5 consts
4.6
4.7 - q_ :: "real => real" ("q'_") (* Streckenlast *)
4.8 + qq :: "real => real" (* Streckenlast *)
4.9 Q :: "real => real" (* Querkraft *)
4.10 Q' :: "real => real" (* Ableitung der Querkraft *)
4.11 M'_b :: "real => real" ("M'_b") (* Biegemoment *)
4.12 @@ -58,8 +58,8 @@
4.13
4.14 axioms(*axiomatization where*)
4.15
4.16 - Querkraft_Belastung: "Q' x = -q_ x" (*and*)
4.17 - Belastung_Querkraft: "-q_ x = Q' x" (*and*)
4.18 + Querkraft_Belastung: "Q' x = -qq x" (*and*)
4.19 + Belastung_Querkraft: "-qq x = Q' x" (*and*)
4.20
4.21 Moment_Querkraft: "M_b' x = Q x" (*and*)
4.22 Querkraft_Moment: "Q x = M_b' x" (*and*)
4.23 @@ -228,125 +228,123 @@
4.24
4.25 ML {*
4.26 store_met
4.27 - (prep_met thy "met_biege" [] e_metID
4.28 - (["IntegrierenUndKonstanteBestimmen"],
4.29 - [("#Given" ,["Traegerlaenge l_l", "Streckenlast q_q",
4.30 - "FunktionsVariable v_v"]),
4.31 + (prep_met thy "met_biege" [] e_metID
4.32 + (["IntegrierenUndKonstanteBestimmen"],
4.33 + [("#Given" ,["Traegerlaenge l_l", "Streckenlast q__q", "FunktionsVariable v_v"]),
4.34 (*("#Where",["0 < l_l"]), ...wait for < and handling Arbfix*)
4.35 - ("#Find" ,["Biegelinie b_b"]),
4.36 - ("#Relate",["RandbedingungenBiegung r_b",
4.37 - "RandbedingungenMoment r_m"])
4.38 - ],
4.39 - {rew_ord'="tless_true",
4.40 - rls' = append_rls "erls_IntegrierenUndK.." e_rls
4.41 - [Calc ("Atools.ident",eval_ident "#ident_"),
4.42 - Thm ("not_true",num_str @{thm not_true}),
4.43 - Thm ("not_false",num_str @{thm not_false})],
4.44 - calc = [], srls = srls, prls = Erls,
4.45 - crls = Atools_erls, nrls = Erls},
4.46 -"Script BiegelinieScript " ^
4.47 -"(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) " ^
4.48 -"(r_b::bool list) (r_m::bool list) = " ^
4.49 -" (let q___q = Take (q_q v_v = q__q); " ^
4.50 -" q___q = ((Rewrite sym_real_minus_eq_cancel True) @@ " ^
4.51 -" (Rewrite Belastung_Querkraft True)) q___q; " ^
4.52 -" (Q__Q:: bool) = " ^
4.53 -" (SubProblem (Biegelinie',[named,integrate,function], " ^
4.54 -" [diff,integration,named]) " ^
4.55 + ("#Find" ,["Biegelinie b_b"]),
4.56 + ("#Relate",["RandbedingungenBiegung r_b", "RandbedingungenMoment r_m"])],
4.57 + {rew_ord'="tless_true",
4.58 + rls' = append_rls "erls_IntegrierenUndK.." e_rls
4.59 + [Calc ("Atools.ident",eval_ident "#ident_"),
4.60 + Thm ("not_true",num_str @{thm not_true}),
4.61 + Thm ("not_false",num_str @{thm not_false})],
4.62 + calc = [], srls = srls, prls = Erls, crls = Atools_erls, nrls = Erls},
4.63 +"Script BiegelinieScript " ^
4.64 +"(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) " ^
4.65 +"(r_b::bool list) (r_m::bool list) = " ^
4.66 +" (let q___q = Take (qq v_v = q__q); " ^
4.67 +" q___q = ((Rewrite sym_neg_equal_iff_equal True) @@ " ^
4.68 +" (Rewrite Belastung_Querkraft True)) q___q; " ^
4.69 +" (Q__Q:: bool) = " ^
4.70 +" (SubProblem (Biegelinie',[named,integrate,function], " ^
4.71 +" [diff,integration,named]) " ^
4.72 " [REAL (rhs q___q), REAL v_v, REAL_REAL Q]); " ^
4.73 -" Q__Q = Rewrite Querkraft_Moment True Q__Q; " ^
4.74 -" (M__M::bool) = " ^
4.75 -" (SubProblem (Biegelinie',[named,integrate,function], " ^
4.76 -" [diff,integration,named]) " ^
4.77 +" Q__Q = Rewrite Querkraft_Moment True Q__Q; " ^
4.78 +" (M__M::bool) = " ^
4.79 +" (SubProblem (Biegelinie',[named,integrate,function], " ^
4.80 +" [diff,integration,named]) " ^
4.81 " [REAL (rhs Q__Q), REAL v_v, REAL_REAL M_b]); " ^
4.82 + (*([5], Res), M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2*)
4.83 " e__1 = NTH 1 r_m; " ^
4.84 -" (x__1::real) = argument_in (lhs e__1); " ^
4.85 -" (M__1::bool) = (Substitute [v_v = x__1]) M__M; " ^
4.86 -" M__1 = (Substitute [e__1]) M__1 ; " ^
4.87 -" M__2 = Take M__M; " ^
4.88 -(*without this Take 'Substitute [v_v = x__2]' takes _last formula from ctree_*)
4.89 +" (x__1::real) = argument_in (lhs e__1); " ^
4.90 +" (M__1::bool) = (Substitute [v_v = x__1]) M__M; " ^
4.91 + (*([6], Res), M_b 0 = c_2 + c * 0 + -1 * q_0 / 2 * 0 ^^^ 2*)
4.92 +" M__1 = (Substitute [e__1]) M__1; " ^
4.93 + (*([7], Res), 0 = c_2 + c * 0 + -1 * q_0 / 2 * 0 ^^^ 2*)
4.94 +" M__2 = Take M__M; " ^
4.95 + (*([8], Frm), M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2*)
4.96 +(*without above Take 'Substitute [v_v = x__2]' takes _last formula from ctree_*)
4.97 " e__2 = NTH 2 r_m; " ^
4.98 -" (x__2::real) = argument_in (lhs e__2); " ^
4.99 -" (M__2::bool) = ((Substitute [v_v = x__2]) @@ " ^
4.100 -" (Substitute [e__2])) M__2; " ^
4.101 -" (c_1_2::bool list) = " ^
4.102 -" (SubProblem (Biegelinie',[linear,system],[no_met]) " ^
4.103 -" [BOOL_LIST [M__1, M__2], REAL_LIST [c,c_2]]); " ^
4.104 -" M__M = Take M__M; " ^
4.105 +" (x__2::real) = argument_in (lhs e__2); " ^
4.106 +" (M__2::bool) = (Substitute [v_v = x__2]) M__M; " ^
4.107 + (*([8], Res), M_b L = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2*)
4.108 +" M__2 = (Substitute [e__2]) M__2; " ^
4.109 + (**)
4.110 +" (c_1_2::bool list) = " ^
4.111 +" (SubProblem (Biegelinie',[linear,system],[no_met]) " ^
4.112 +" [BOOL_LIST [M__1, M__2], REAL_LIST [c,c_2]]); " ^
4.113 +" M__M = Take M__M; " ^
4.114 " M__M = ((Substitute c_1_2) @@ " ^
4.115 -" (Try (Rewrite_Set_Inst [(bdv_1, c),(bdv_2, c_2)]" ^
4.116 -" simplify_System False)) @@ " ^
4.117 -" (Rewrite Moment_Neigung False) @@ " ^
4.118 -" (Rewrite make_fun_explicit False)) M__M; " ^
4.119 +" (Try (Rewrite_Set_Inst [(bdv_1, c),(bdv_2, c_2)] " ^
4.120 +" simplify_System False)) @@ " ^
4.121 +" (Rewrite Moment_Neigung False) @@ " ^
4.122 +" (Rewrite make_fun_explicit False)) M__M; " ^
4.123 (*----------------------- and the same once more ------------------------*)
4.124 -" (N__N:: bool) = " ^
4.125 -" (SubProblem (Biegelinie',[named,integrate,function], " ^
4.126 -" [diff,integration,named]) " ^
4.127 +" (N__N:: bool) = " ^
4.128 +" (SubProblem (Biegelinie',[named,integrate,function], " ^
4.129 +" [diff,integration,named]) " ^
4.130 " [REAL (rhs M__M), REAL v_v, REAL_REAL y']); " ^
4.131 -" (B__B:: bool) = " ^
4.132 -" (SubProblem (Biegelinie',[named,integrate,function], " ^
4.133 -" [diff,integration,named]) " ^
4.134 +" (B__B:: bool) = " ^
4.135 +" (SubProblem (Biegelinie',[named,integrate,function], " ^
4.136 +" [diff,integration,named]) " ^
4.137 " [REAL (rhs N__N), REAL v_v, REAL_REAL y]); " ^
4.138 " e__1 = NTH 1 r_b; " ^
4.139 -" (x__1::real) = argument_in (lhs e__1); " ^
4.140 -" (B__1::bool) = (Substitute [v_v = x__1]) B__B; " ^
4.141 -" B__1 = (Substitute [e__1]) B__1 ; " ^
4.142 -" B__2 = Take B__B; " ^
4.143 +" (x__1::real) = argument_in (lhs e__1); " ^
4.144 +" (B__1::bool) = (Substitute [v_v = x__1]) B__B; " ^
4.145 +" B__1 = (Substitute [e__1]) B__1 ; " ^
4.146 +" B__2 = Take B__B; " ^
4.147 " e__2 = NTH 2 r_b; " ^
4.148 -" (x__2::real) = argument_in (lhs e__2); " ^
4.149 -" (B__2::bool) = ((Substitute [v_v = x__2]) @@ " ^
4.150 -" (Substitute [e__2])) B__2; " ^
4.151 -" (c_1_2::bool list) = " ^
4.152 -" (SubProblem (Biegelinie',[linear,system],[no_met]) " ^
4.153 -" [BOOL_LIST [B__1, B__2], REAL_LIST [c,c_2]]); " ^
4.154 -" B__B = Take B__B; " ^
4.155 +" (x__2::real) = argument_in (lhs e__2); " ^
4.156 +" (B__2::bool) = (Substitute [v_v = x__2]) B__B; " ^
4.157 +" B__2 = (Substitute [e__2]) B__2 ; " ^
4.158 +" (c_1_2::bool list) = " ^
4.159 +" (SubProblem (Biegelinie',[linear,system],[no_met]) " ^
4.160 +" [BOOL_LIST [B__1, B__2], REAL_LIST [c,c_2]]); " ^
4.161 +" B__B = Take B__B; " ^
4.162 " B__B = ((Substitute c_1_2) @@ " ^
4.163 -" (Rewrite_Set_Inst [(bdv, x)] make_ratpoly_in False)) B__B " ^
4.164 +" (Rewrite_Set_Inst [(bdv, x)] make_ratpoly_in False)) B__B " ^
4.165 " in B__B)"
4.166 ));
4.167 *}
4.168 ML {*
4.169 -
4.170 store_met
4.171 - (prep_met thy "met_biege_2" [] e_metID
4.172 - (["IntegrierenUndKonstanteBestimmen2"],
4.173 - [("#Given" ,["Traegerlaenge l_l", "Streckenlast q__q",
4.174 - "FunktionsVariable v_v"]),
4.175 + (prep_met thy "met_biege_2" [] e_metID
4.176 + (["IntegrierenUndKonstanteBestimmen2"],
4.177 + [("#Given" ,["Traegerlaenge l_l", "Streckenlast q__q", "FunktionsVariable v_v"]),
4.178 (*("#Where",["0 < l_l"]), ...wait for < and handling Arbfix*)
4.179 - ("#Find" ,["Biegelinie b_b"]),
4.180 - ("#Relate",["Randbedingungen r_b"])
4.181 - ],
4.182 - {rew_ord'="tless_true",
4.183 - rls' = append_rls "erls_IntegrierenUndK.." e_rls
4.184 - [Calc ("Atools.ident",eval_ident "#ident_"),
4.185 - Thm ("not_true",num_str @{thm not_true}),
4.186 - Thm ("not_false",num_str @{thm not_false})],
4.187 - calc = [],
4.188 - srls = append_rls "erls_IntegrierenUndK.." e_rls
4.189 - [Calc("Tools.rhs", eval_rhs"eval_rhs_"),
4.190 - Calc ("Atools.ident",eval_ident "#ident_"),
4.191 - Thm ("last_thmI",num_str @{thm last_thmI}),
4.192 - Thm ("if_True",num_str @{thm if_True}),
4.193 - Thm ("if_False",num_str @{thm if_False})
4.194 - ],
4.195 - prls = Erls, crls = Atools_erls, nrls = Erls},
4.196 -"Script Biegelinie2Script " ^
4.197 + ("#Find" ,["Biegelinie b_b"]),
4.198 + ("#Relate",["Randbedingungen r_b"])],
4.199 + {rew_ord'="tless_true",
4.200 + rls' = append_rls "erls_IntegrierenUndK.." e_rls
4.201 + [Calc ("Atools.ident",eval_ident "#ident_"),
4.202 + Thm ("not_true",num_str @{thm not_true}),
4.203 + Thm ("not_false",num_str @{thm not_false})],
4.204 + calc = [],
4.205 + srls = append_rls "erls_IntegrierenUndK.." e_rls
4.206 + [Calc("Tools.rhs", eval_rhs"eval_rhs_"),
4.207 + Calc ("Atools.ident",eval_ident "#ident_"),
4.208 + Thm ("last_thmI",num_str @{thm last_thmI}),
4.209 + Thm ("if_True",num_str @{thm if_True}),
4.210 + Thm ("if_False",num_str @{thm if_False})],
4.211 + prls = Erls, crls = Atools_erls, nrls = Erls},
4.212 +"Script Biegelinie2Script " ^
4.213 "(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) (r_b::bool list) = " ^
4.214 -" (let " ^
4.215 -" (fun_s:: bool list) = " ^
4.216 -" (SubProblem (Biegelinie',[vonBelastungZu,Biegelinien], " ^
4.217 -" [Biegelinien,ausBelastung]) " ^
4.218 -" [REAL q__q, REAL v_v]); " ^
4.219 -" (equ_s::bool list) = " ^
4.220 -" (SubProblem (Biegelinie',[setzeRandbedingungen,Biegelinien]," ^
4.221 -" [Biegelinien,setzeRandbedingungenEin]) " ^
4.222 +" (let " ^
4.223 +" (fun_s:: bool list) = " ^
4.224 +" (SubProblem (Biegelinie',[vonBelastungZu,Biegelinien], " ^
4.225 +" [Biegelinien,ausBelastung]) " ^
4.226 +" [REAL q__q, REAL v_v]); " ^
4.227 +" (equ_s::bool list) = " ^
4.228 +" (SubProblem (Biegelinie',[setzeRandbedingungen,Biegelinien], " ^
4.229 +" [Biegelinien,setzeRandbedingungenEin]) " ^
4.230 " [BOOL_LIST fun_s, BOOL_LIST r_b]); " ^
4.231 -" (con_s::bool list) = " ^
4.232 -" (SubProblem (Biegelinie',[linear,system],[no_met]) " ^
4.233 -" [BOOL_LIST equ_s, REAL_LIST [c,c_2,c_3,c_4]]); " ^
4.234 +" (con_s::bool list) = " ^
4.235 +" (SubProblem (Biegelinie',[linear,system],[no_met]) " ^
4.236 +" [BOOL_LIST equ_s, REAL_LIST [c,c_2,c_3,c_4]]); " ^
4.237 " B_B = Take (lastI fun_s); " ^
4.238 " B_B = ((Substitute con_s) @@ " ^
4.239 -" (Rewrite_Set_Inst [(bdv, v_v)] make_ratpoly_in False)) B_B " ^
4.240 +" (Rewrite_Set_Inst [(bdv, v_v)] make_ratpoly_in False)) B_B " ^
4.241 " in B_B)"
4.242 ));
4.243
4.244 @@ -399,42 +397,42 @@
4.245 *}
4.246 ML {*
4.247 store_met
4.248 - (prep_met thy "met_biege_ausbelast" [] e_metID
4.249 - (["Biegelinien","ausBelastung"],
4.250 - [("#Given" ,["Streckenlast q__q","FunktionsVariable v_v"]),
4.251 - ("#Find" ,["Funktionen fun_s"])],
4.252 - {rew_ord'="tless_true",
4.253 - rls' = append_rls "erls_ausBelastung" e_rls
4.254 - [Calc ("Atools.ident",eval_ident "#ident_"),
4.255 - Thm ("not_true",num_str @{thm not_true}),
4.256 - Thm ("not_false",num_str @{thm not_false})],
4.257 - calc = [],
4.258 - srls = append_rls "srls_ausBelastung" e_rls
4.259 - [Calc("Tools.rhs", eval_rhs"eval_rhs_")],
4.260 - prls = e_rls, crls = Atools_erls, nrls = e_rls},
4.261 -"Script Belastung2BiegelScript (q__q::real) (v_v::real) = " ^
4.262 -" (let q___q = Take (q_q v_v = q__q); " ^
4.263 -" q___q = ((Rewrite sym_real_minus_eq_cancel True) @@ " ^
4.264 -" (Rewrite Belastung_Querkraft True)) q___q; " ^
4.265 -" (Q__Q:: bool) = " ^
4.266 -" (SubProblem (Biegelinie',[named,integrate,function], " ^
4.267 -" [diff,integration,named]) " ^
4.268 -" [REAL (rhs q___q), REAL v_v, REAL_REAL Q]); " ^
4.269 -" M__M = Rewrite Querkraft_Moment True Q__Q; " ^
4.270 -" (M__M::bool) = " ^
4.271 -" (SubProblem (Biegelinie',[named,integrate,function], " ^
4.272 -" [diff,integration,named]) " ^
4.273 -" [REAL (rhs M__M), REAL v_v, REAL_REAL M_b]); " ^
4.274 -" N__N = ((Rewrite Moment_Neigung False) @@ " ^
4.275 -" (Rewrite make_fun_explicit False)) M__M; " ^
4.276 -" (N__N:: bool) = " ^
4.277 -" (SubProblem (Biegelinie',[named,integrate,function], " ^
4.278 -" [diff,integration,named]) " ^
4.279 -" [REAL (rhs N__N), REAL v_v, REAL_REAL y']); " ^
4.280 -" (B__B:: bool) = " ^
4.281 -" (SubProblem (Biegelinie',[named,integrate,function], " ^
4.282 -" [diff,integration,named]) " ^
4.283 -" [REAL (rhs N__N), REAL v_v, REAL_REAL y]) " ^
4.284 + (prep_met thy "met_biege_ausbelast" [] e_metID
4.285 + (["Biegelinien", "ausBelastung"],
4.286 + [("#Given" ,["Streckenlast q__q", "FunktionsVariable v_v"]),
4.287 + ("#Find" ,["Funktionen fun_s"])],
4.288 + {rew_ord'="tless_true",
4.289 + rls' = append_rls "erls_ausBelastung" e_rls
4.290 + [Calc ("Atools.ident", eval_ident "#ident_"),
4.291 + Thm ("not_true", num_str @{thm not_true}),
4.292 + Thm ("not_false", num_str @{thm not_false})],
4.293 + calc = [],
4.294 + srls = append_rls "srls_ausBelastung" e_rls
4.295 + [Calc ("Tools.rhs", eval_rhs "eval_rhs_")],
4.296 + prls = e_rls, crls = Atools_erls, nrls = e_rls},
4.297 +"Script Belastung2BiegelScript (q__q::real) (v_v::real) = " ^
4.298 +" (let q___q = Take (qq v_v = q__q); " ^
4.299 +" q___q = ((Rewrite sym_neg_equal_iff_equal True) @@ " ^
4.300 +" (Rewrite Belastung_Querkraft True)) q___q; " ^
4.301 +" (Q__Q:: bool) = " ^
4.302 +" (SubProblem (Biegelinie',[named,integrate,function], " ^
4.303 +" [diff,integration,named]) " ^
4.304 +" [REAL (rhs q___q), REAL v_v, REAL_REAL Q]); " ^
4.305 +" M__M = Rewrite Querkraft_Moment True Q__Q; " ^
4.306 +" (M__M::bool) = " ^
4.307 +" (SubProblem (Biegelinie',[named,integrate,function], " ^
4.308 +" [diff,integration,named]) " ^
4.309 +" [REAL (rhs M__M), REAL v_v, REAL_REAL M_b]); " ^
4.310 +" N__N = ((Rewrite Moment_Neigung False) @@ " ^
4.311 +" (Rewrite make_fun_explicit False)) M__M; " ^
4.312 +" (N__N:: bool) = " ^
4.313 +" (SubProblem (Biegelinie',[named,integrate,function], " ^
4.314 +" [diff,integration,named]) " ^
4.315 +" [REAL (rhs N__N), REAL v_v, REAL_REAL y']); " ^
4.316 +" (B__B:: bool) = " ^
4.317 +" (SubProblem (Biegelinie',[named,integrate,function], " ^
4.318 +" [diff,integration,named]) " ^
4.319 +" [REAL (rhs N__N), REAL v_v, REAL_REAL y]) " ^
4.320 " in [Q__Q, M__M, N__N, B__B])"
4.321 ));
4.322
4.323 @@ -442,9 +440,9 @@
4.324 ML {*
4.325 store_met
4.326 (prep_met thy "met_biege_setzrand" [] e_metID
4.327 - (["Biegelinien","setzeRandbedingungenEin"],
4.328 - [("#Given" ,["Funktionen fun_s","Randbedingungen r_b"]),
4.329 - ("#Find" ,["Gleichungen equs'''"])],
4.330 + (["Biegelinien", "setzeRandbedingungenEin"],
4.331 + [("#Given" , ["Funktionen fun_s", "Randbedingungen r_b"]),
4.332 + ("#Find" , ["Gleichungen equs'''"])],
4.333 {rew_ord'="tless_true", rls'=Erls, calc = [],
4.334 srls = srls2,
4.335 prls=e_rls,
4.336 @@ -474,7 +472,7 @@
4.337 " (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
4.338 " [Equation,fromFunction]) " ^
4.339 " [BOOL (hd f_s), BOOL b_4]) " ^
4.340 -" in [e_1,e_2,e_3,e_4])"
4.341 +" in [e_1, e_2, e_3, e_4])"
4.342 (* filter requires more than 1 sec !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
4.343 "Script SetzeRandbedScript (fun_s::bool list) (r_b::bool list) = " ^
4.344 " (let b_1 = NTH 1 r_b; " ^
4.345 @@ -507,17 +505,15 @@
4.346 *}
4.347 ML {*
4.348 store_met
4.349 - (prep_met thy "met_equ_fromfun" [] e_metID
4.350 - (["Equation","fromFunction"],
4.351 - [("#Given" ,["functionEq fu_n","substitution su_b"]),
4.352 - ("#Find" ,["equality equ'''"])],
4.353 - {rew_ord'="tless_true", rls'=Erls, calc = [],
4.354 - srls = append_rls "srls_in_EquationfromFunc" e_rls
4.355 - [Calc("Tools.lhs", eval_lhs"eval_lhs_"),
4.356 - Calc("Atools.argument'_in",
4.357 - eval_argument_in
4.358 - "Atools.argument'_in")],
4.359 - prls=e_rls, crls = Atools_erls, nrls = e_rls},
4.360 + (prep_met thy "met_equ_fromfun" [] e_metID
4.361 + (["Equation","fromFunction"],
4.362 + [("#Given" ,["functionEq fu_n","substitution su_b"]),
4.363 + ("#Find" ,["equality equ'''"])],
4.364 + {rew_ord'="tless_true", rls'=Erls, calc = [],
4.365 + srls = append_rls "srls_in_EquationfromFunc" e_rls
4.366 + [Calc("Tools.lhs", eval_lhs"eval_lhs_"),
4.367 + Calc("Atools.argument'_in", eval_argument_in "Atools.argument'_in")],
4.368 + prls=e_rls, crls = Atools_erls, nrls = e_rls},
4.369 (*(M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2) (M_b L = 0) -->
4.370 0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2*)
4.371 "Script Function2Equality (fu_n::bool) (su_b::bool) =" ^
4.372 @@ -525,8 +521,9 @@
4.373 " bd_v = argument_in (lhs fu_n); " ^
4.374 " va_l = argument_in (lhs su_b); " ^
4.375 " eq_u = (Substitute [bd_v = va_l]) fu_n; " ^
4.376 -" eq_u = (Substitute [su_b]) fu_n " ^
4.377 -" in (Rewrite_Set norm_Rational False) eq_u) "
4.378 + (*([1], Res), M_b L = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2*)
4.379 +" eq_u = (Substitute [su_b]) eq_u " ^
4.380 +" in (Rewrite_Set norm_Rational False) eq_u) "
4.381 ));
4.382 *}
4.383
5.1 --- a/src/Tools/isac/Knowledge/Partial_Fractions.thy Wed Mar 07 15:58:18 2012 +0100
5.2 +++ b/src/Tools/isac/Knowledge/Partial_Fractions.thy Sat Mar 10 14:38:18 2012 +0100
5.3 @@ -99,10 +99,37 @@
5.4 ansatz_2nd_order: "n / (a*b) = A/a + B/b" and
5.5 ansatz_3rd_order: "n / (a*b*c) = A/a + B/b + C/c" and
5.6 ansatz_4th_order: "n / (a*b*c*d) = A/a + B/b + C/c + D/d" and
5.7 + (*version 1*)
5.8 equival_trans_2nd_order: "(n/(a*b) = A/a + B/b) = (n = A*b + B*a)" and
5.9 equival_trans_3rd_order: "(n/(a*b*c) = A/a + B/b + C/c) = (n = A*b*c + B*a*c + C*a*b)" and
5.10 equival_trans_4th_order: "(n/(a*b*c*d) = A/a + B/b + C/c + D/d) =
5.11 - (n = A*b*c*d + B*a*c*d + C*a*b*d + D*a*b*c)"
5.12 + (n = A*b*c*d + B*a*c*d + C*a*b*d + D*a*b*c)" and
5.13 + (*version 2: not yet used, see partial_fractions.sml*)
5.14 + multiply_2nd_order: "(n/x = A/a + B/b) = (a*b*n/x = A*b + B*a)" and
5.15 + 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
5.16 + multiply_4th_order:
5.17 + "(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)"
5.18 +
5.19 +text {* Probably the optimal formalization woudl be ...
5.20 +
5.21 + multiply_2nd_order: "x = a*b ==> (n/x = A/a + B/b) = (a*b*n/x = A*b + B*a)" and
5.22 + multiply_3rd_order: "x = a*b*c ==>
5.23 + (n/x = A/a + B/b + C/c) = (a*b*c*n/x = A*b*c + B*a*c + C*a*b)" and
5.24 + multiply_4th_order: "x = a*b*c*d ==>
5.25 + (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)"
5.26 +
5.27 +... because it would allow to start the ansatz as follows
5.28 +(1) 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z))) = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))
5.29 +(2) 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z))) = AA / (z - 1 / 2) + BB / (z - -1 / 4)
5.30 +(3) (z - 1 / 2) * (z - -1 / 4) * 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z))) =
5.31 + (z - 1 / 2) * (z - -1 / 4) * AA / (z - 1 / 2) + BB / (z - -1 / 4)
5.32 +(4) 3 = A * (z - -1 / 4) + B * (z - 1 / 2)
5.33 +
5.34 +... (1==>2) ansatz
5.35 + (2==>3) multiply_*
5.36 + (3==>4) norm_Rational
5.37 +TODOs for this version ar in partial_fractions.sml "--- progr.vers.2: "
5.38 +*}
5.39
5.40 ML {*
5.41 val ansatz_rls = prep_rls(
5.42 @@ -113,9 +140,7 @@
5.43 Thm ("ansatz_3rd_order",num_str @{thm ansatz_3rd_order})
5.44 ],
5.45 scr = EmptyScr}:rls);
5.46 -*}
5.47
5.48 -ML {*
5.49 val equival_trans = prep_rls(
5.50 Rls {id = "equival_trans", preconds = [], rew_ord = ("dummy_ord",dummy_ord),
5.51 erls = Erls, srls = Erls, calc = [],
5.52 @@ -124,12 +149,22 @@
5.53 Thm ("equival_trans_3rd_order",num_str @{thm equival_trans_3rd_order})
5.54 ],
5.55 scr = EmptyScr}:rls);
5.56 +
5.57 +val multiply_ansatz = prep_rls(
5.58 + Rls {id = "multiply_ansatz", preconds = [], rew_ord = ("dummy_ord",dummy_ord),
5.59 + erls = Erls,
5.60 + srls = Erls, calc = [],
5.61 + rules =
5.62 + [Thm ("multiply_2nd_order",num_str @{thm multiply_2nd_order})
5.63 + ],
5.64 + scr = EmptyScr}:rls);
5.65 *}
5.66
5.67 text {*store the rule set for math engine*}
5.68 ML {*
5.69 ruleset' := overwritelthy @{theory} (!ruleset',
5.70 [("ansatz_rls", ansatz_rls),
5.71 + ("multiply_ansatz", multiply_ansatz),
5.72 ("equival_trans", equival_trans)
5.73 ]);
5.74 *}
5.75 @@ -140,6 +175,7 @@
5.76 decomposedFunction :: "real => una"
5.77
5.78 ML {*
5.79 +check_guhs_unique := false; (*WN120307 REMOVE after editing*)
5.80 store_pbt
5.81 (prep_pbt @{theory} "pbl_simp_rat_partfrac" [] e_pblID
5.82 (["partial_fraction", "rational", "simplification"],
6.1 --- a/src/Tools/isac/Knowledge/Rational2.thy Wed Mar 07 15:58:18 2012 +0100
6.2 +++ b/src/Tools/isac/Knowledge/Rational2.thy Sat Mar 10 14:38:18 2012 +0100
6.3 @@ -6,48 +6,147 @@
6.4 10 20 30 40 50 60 70 80 90 100
6.5 *)
6.6
6.7 -theory Rational2 imports Poly begin
6.8 +theory Rational2 imports Complex_Main begin
6.9
6.10
6.11 -ML {*member op= [1,2,3,4,5] 3;
6.12 -union op= [1,2,3,4,5] [4,5,6,7]*}
6.13 +
6.14 +ML{*(*use modinv(r,m) to get rinv= r^-1 mod m*)
6.15 +fun modi (r, rold, m, rinv) =
6.16 + if rinv < m
6.17 + then
6.18 + if r mod m = 1
6.19 + then ( rinv + 1;
6.20 + rinv)
6.21 + else modi (rold * (rinv+1),rold,m,rinv+1)
6.22 +else (0)
6.23 +(*Errormeldung? es gibt kein Inverses sind nicht Teilerfremd!! schon zu Beginn darauf überprüfen!!*)
6.24 +
6.25 +fun modinv (r,m) = modi (r, r, m, 0);
6.26 +
6.27 +*}
6.28 +
6.29 +ML{*
6.30 +infix modinvWN;
6.31 +fun r modinvWN m = modi (r, r, m, 0);
6.32 +(* chinese remainder theorem *)
6.33 +fun CRA_2WN r1 r2 m1 m2 =
6.34 + (r1 mod m1) + ((r2 - (r1 mod m1)) * (m1 modinvWN m2) mod m2) * m1;
6.35 +*}
6.36 +
6.37 +ML{*
6.38 +modinv(2,5);
6.39 +modinv(3,5);
6.40 +modinv(4,339);
6.41 +4*85
6.42 +*}
6.43 +
6.44 +ML{*
6.45 +(* chinese remainder theorem *)
6.46 +fun CRA_2 (r1 : int, r2 : int, m1 : int, m2 : int)=
6.47 +(*c=m1^-1 mod m2
6.48 + r1'=r1 mod m1
6.49 + s=(r2-r1')*c mod m2
6.50 + r= r1'+s*m1
6.51 + return r*)
6.52 + (r1 mod m1) + ((r2 - (r1 mod m1)) * (modinv (m1, m2)) mod m2) * m1
6.53 +*}
6.54 +ML{*
6.55 +
6.56 +*}
6.57 +ML{*
6.58 +(* old style -- above is better !!! NEW STYLE |> see test/Pure/General/Basics.thy
6.59 +*)
6.60 +fun CRA_2' (r1 : int, r2 : int, m1 : int, m2 : int)=
6.61 + let
6.62 + val c= modinv (m1, m2)
6.63 + val r1'=r1 mod m1
6.64 + val s=(r2-r1')*c mod m2
6.65 + val r= r1'+s*m1
6.66 + in r end;
6.67 +*}
6.68 +ML{*
6.69 +
6.70 +*}
6.71 +ML{*
6.72 +print_depth 999;
6.73 +print_depth 999;
6.74 +*}
6.75 +ML{*
6.76 +CRA_2WN;
6.77 +val intermed_res = CRA_2WN 1 2 3 ;
6.78 +fun yyy f z = f z;
6.79 +yyy;
6.80 +yyy intermed_res; (*evaluation postponed to where it is required*)
6.81 +yyy intermed_res 4;
6.82 +*}
6.83 +ML{*
6.84 +modinv;
6.85 +yyy modinv ;
6.86 +yyy modinv (2 ,3);
6.87 +*}
6.88 +ML{*
6.89 +(1,2) |> modinv
6.90 + |> (curry op+ 2)
6.91 +*}
6.92 +
6.93 +ML{*
6.94 +(*. univariate polynomials (uv) .*)
6.95 +(*. univariate polynomials are represented as a list
6.96 + of the coefficent in reverse maximum degree order .*)
6.97 +(*. 5 * x^5 + 4 * x^3 + 2 * x^2 + x + 19 => [19,1,2,4,0,5] .*)
6.98 +type uv_poly = int list;
6.99 +
6.100 +*}
6.101 +
6.102 +ML{*
6.103 +*}
6.104 +ML{*
6.105 +3 mod 2;
6.106 +((3+5)*5)mod 9;
6.107 +*}
6.108 +ML{*
6.109 +CRA_2(2,6,2,5);
6.110 +modinv(2,5);
6.111 +modinv(3,5);
6.112 +CRA_2(2,6,3,5);
6.113 +6 mod 5;
6.114 +
6.115 +*}
6.116 +ML{*
6.117 +
6.118 +*}
6.119 +
6.120 +
6.121 ML {*
6.122 -type uv_poly = int list;
6.123 +fun div_3_by d = 3 div d;
6.124 +div_3_by 3;
6.125 +(*div_3_by 0*)
6.126 +can;
6.127 +div_3_by;
6.128 +can div_3_by;
6.129 +can div_3_by 0;
6.130 +fun xxx x =
6.131 + if can div_3_by x then div_3_by x else 9999999;
6.132 +xxx 1;
6.133 +xxx 0;
6.134 *}
6.135 ML {*
6.136 -fun uv_mod_null (p1 : int list, 0) = p1
6.137 - | uv_mod_null (p1 : int list, n1 : int) = uv_mod_null (p1, n1 - 1) @ [0];
6.138 +op div;
6.139 +curry op div;
6.140 +fun div' a b =
6.141 + if can (curry op div a) b then SOME (a div b) else NONE
6.142 *}
6.143 ML {*
6.144 -type mv_monom =
6.145 - (int * (* coefficient or the monom *)
6.146 - int list); (* list of exponents) *)
6.147 +perhaps;
6.148 +div' 128;
6.149 +perhaps (div' 128) 8;
6.150 +perhaps (div' 128) 0;
6.151 *}
6.152 ML {*
6.153 -type mv_poly = mv_monom list;
6.154 +val x = SOME 123;
6.155 + the x
6.156 *}
6.157 ML {*
6.158 -EQUAL (* !!! isac --- Isabelle2011 ????*)
6.159 -*}
6.160 -ML {* (*name?*)
6.161 -fun mv_mg_hlp [] = EQUAL
6.162 - | mv_mg_hlp (x :: xs) =
6.163 - if x < 0 then LESS
6.164 - else if x > 0 then GREATER
6.165 - else mv_mg_hlp (xs : uv_poly);
6.166 -*}
6.167 -ML {*
6.168 -mv_mg_hlp [0,0,1,0];
6.169 -mv_mg_hlp [0,0,~1,0];
6.170 -mv_mg_hlp [0,0,0,0];
6.171 -mv_mg_hlp [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,999];
6.172 -mv_mg_hlp [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,~999];
6.173 -*}
6.174 -ML {*
6.175 -mem
6.176 -*}
6.177 -ML {*
6.178 -union
6.179 *}
6.180 ML {*
6.181 *}
7.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Wed Mar 07 15:58:18 2012 +0100
7.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Sat Mar 10 14:38:18 2012 +0100
7.3 @@ -90,7 +90,7 @@
7.4 *)
7.5 *}
7.6
7.7 -ML {* val (thy, ro, er) = (@{theory Isac}, tless_true, eval_rls); *}
7.8 +ML {* val (thy, ro, er) = (@{theory}, tless_true, eval_rls); *}
7.9 ML {*
7.10 val SOME (t, asm1) =
7.11 rewrite_ thy ro er true (num_str @{thm rule3}) t;
7.12 @@ -127,7 +127,7 @@
7.13 text{*\noindent We try two different notations and check which of them
7.14 Isabelle can handle best.*}
7.15 ML {*
7.16 - val ctxt = ProofContext.init_global @{theory Isac};
7.17 + val ctxt = ProofContext.init_global @{theory};
7.18 val ctxt = declare_constraints' [@{term "z::real"}] ctxt;
7.19
7.20 val SOME fun1 =
7.21 @@ -146,21 +146,21 @@
7.22 ruleZY: "(X z = a / b) = (X' z = a / (z * b))"
7.23
7.24 ML {*
7.25 - val (thy, ro, er) = (@{theory Isac}, tless_true, eval_rls);
7.26 + val (thy, ro, er) = (@{theory}, tless_true, eval_rls);
7.27 val SOME (fun2, asm1) =
7.28 rewrite_ thy ro er true @{thm ruleZY} fun1; term2str fun2;
7.29 val SOME (fun2', asm1) =
7.30 rewrite_ thy ro er true @{thm ruleZY} fun1'; term2str fun2';
7.31
7.32 val SOME (fun3,_) =
7.33 - rewrite_set_ @{theory Isac} false norm_Rational fun2;
7.34 + rewrite_set_ @{theory} false norm_Rational fun2;
7.35 term2str fun3;
7.36 (*
7.37 * Fails on x^^^(-1)
7.38 * We solve this problem by using 1/x as a workaround.
7.39 *)
7.40 val SOME (fun3',_) =
7.41 - rewrite_set_ @{theory Isac} false norm_Rational fun2';
7.42 + rewrite_set_ @{theory} false norm_Rational fun2';
7.43 term2str fun3';
7.44 (*
7.45 * OK - workaround!
7.46 @@ -624,7 +624,7 @@
7.47
7.48 ML {*
7.49 val SOME (t1,_) =
7.50 - rewrite_ @{theory Isac} e_rew_ord e_rls false
7.51 + rewrite_ @{theory} e_rew_ord e_rls false
7.52 @{thm ansatz_2nd_order} expr';
7.53 term2str t1; atomty t1;
7.54 val eq1 = HOLogic.mk_eq (expr', t1);
7.55 @@ -639,7 +639,7 @@
7.56
7.57 ML {*
7.58 val SOME (eq2,_) =
7.59 - rewrite_ @{theory Isac} e_rew_ord e_rls false
7.60 + rewrite_ @{theory} e_rew_ord e_rls false
7.61 @{thm equival_trans_2nd_order} eq1;
7.62 term2str eq2;
7.63 *}
7.64 @@ -648,7 +648,7 @@
7.65 for simplifications on expressions.*}
7.66
7.67 ML {*
7.68 - val SOME (eq3,_) = rewrite_set_ @{theory Isac} false norm_Rational eq2;
7.69 + val SOME (eq3,_) = rewrite_set_ @{theory} false norm_Rational eq2;
7.70 term2str eq3;
7.71 (*
7.72 * ?A ?B not simplified
7.73 @@ -666,7 +666,7 @@
7.74 * A B !
7.75 *)
7.76 val SOME (fract2,_) =
7.77 - rewrite_set_ @{theory Isac} false norm_Rational fract1;
7.78 + rewrite_set_ @{theory} false norm_Rational fract1;
7.79 term2str fract2 = "(A + -2 * B + 4 * A * z + 4 * B * z) / 4";
7.80 (*
7.81 * term2str fract2 = "A * (1 / 4 + z) + B * (-1 / 2 + z)"
7.82 @@ -687,7 +687,7 @@
7.83 * MANDATORY: simplify (and remove denominator) otherwise 3 = 0
7.84 *)
7.85 val SOME (eq3'' ,_) =
7.86 - rewrite_set_ @{theory Isac} false norm_Rational eq3';
7.87 + rewrite_set_ @{theory} false norm_Rational eq3';
7.88 term2str eq3'';
7.89 *}
7.90
7.91 @@ -718,7 +718,7 @@
7.92
7.93 ML {*
7.94 val SOME (ttttt,_) =
7.95 - rewrite_set_ @{theory Isac} false ansatz_rls expr';
7.96 + rewrite_set_ @{theory} false ansatz_rls expr';
7.97 *}
7.98
7.99 text{*\noindent And check the output\ldots*}
7.100 @@ -739,10 +739,10 @@
7.101
7.102 ML {*
7.103 val SOME (eq4_1,_) =
7.104 - rewrite_terms_ @{theory Isac} e_rew_ord e_rls [s_1] eq3'';
7.105 + rewrite_terms_ @{theory} e_rew_ord e_rls [s_1] eq3'';
7.106 term2str eq4_1;
7.107 val SOME (eq4_2,_) =
7.108 - rewrite_set_ @{theory Isac} false norm_Rational eq4_1;
7.109 + rewrite_set_ @{theory} false norm_Rational eq4_1;
7.110 term2str eq4_2;
7.111
7.112 val fmz = ["equality (3=3*A/(4::real))", "solveFor A","solutions L"];
7.113 @@ -819,10 +819,10 @@
7.114
7.115 ML {*
7.116 val SOME (eq4b_1,_) =
7.117 - rewrite_terms_ @{theory Isac} e_rew_ord e_rls [s_2] eq3'';
7.118 + rewrite_terms_ @{theory} e_rew_ord e_rls [s_2] eq3'';
7.119 term2str eq4b_1;
7.120 val SOME (eq4b_2,_) =
7.121 - rewrite_set_ @{theory Isac} false norm_Rational eq4b_1;
7.122 + rewrite_set_ @{theory} false norm_Rational eq4b_1;
7.123 term2str eq4b_2;
7.124
7.125 val fmz = ["equality (3= -3*B/(4::real))", "solveFor B","solutions L"];
7.126 @@ -1580,7 +1580,7 @@
7.127 \item Then we add line by line. Already the first line causes the error.
7.128 So we investigate it by
7.129 \begin{verbatim}
7.130 - val ctxt = ProofContext.init_global @ { theory } ;
7.131 + val ctxt = ProofContext.init_global @{theory} ;
7.132 val SOME t =
7.133 parseNEW ctxt "(num_orig::real) =
7.134 get_numerator(rhs f_f)";
7.135 @@ -1595,7 +1595,7 @@
7.136 get_met ["simplification",
7.137 "of_rationals",
7.138 "to_partial_fraction"];
7.139 - atomty_thy @ { theory } t ;
7.140 + atomty_thy @{theory} t ;
7.141 \end{verbatim}
7.142 \item We check if the \textbf{semantics of the program} by stepwise evaluation
7.143 of the program. Evaluation is done by the Lucas-Interpreter, which works
7.144 @@ -1607,7 +1607,7 @@
7.145
7.146 subsection {* Transfer to Inverse\_Z\_Transform.thy *}
7.147 text {*
7.148 - Unfortunately it was not possible to complete this task. Because we ran out of time\ldots
7.149 + It was not possible to complete this task, because we ran out of time.
7.150 *}
7.151
7.152
8.1 --- a/test/Tools/isac/CLEANUP Wed Mar 07 15:58:18 2012 +0100
8.2 +++ b/test/Tools/isac/CLEANUP Sat Mar 10 14:38:18 2012 +0100
8.3 @@ -4,94 +4,100 @@
8.4 rm .#*
8.5 rm *.orig*
8.6 cd ADDTESTS
8.7 - rm *~
8.8 - rm #*
8.9 - rm .#*
8.10 - rm *.tar*
8.11 - rm *.orig*
8.12 - cd course
8.13 - rm *~
8.14 - rm #*
8.15 - rm .#*
8.16 - rm *.tar*
8.17 - rm *.orig*
8.18 - cd
8.19 - cd ml_quickstart
8.20 - rm *~
8.21 - rm #*
8.22 - rm .#*
8.23 - rm *.tar*
8.24 - rm *.orig*
8.25 - cd ..
8.26 - cd phst11
8.27 - rm *~
8.28 - rm #*
8.29 - rm .#*
8.30 - rm *.tar*
8.31 - rm *.orig*
8.32 - cd ..
8.33 - cd SignalProcess
8.34 - rm *~
8.35 - rm #*
8.36 - rm .#*
8.37 - rm *.tar*
8.38 - rm *.orig*
8.39 - cd ..
8.40 - cd ..
8.41 - cd file-depend
8.42 - rm *~
8.43 - rm #*
8.44 - rm .#*
8.45 - rm *.tar*
8.46 - rm *.orig*
8.47 - cd ..
8.48 - cd test-depend
8.49 - rm *~
8.50 - rm #*
8.51 - rm .#*
8.52 - rm *.tar*
8.53 - rm *.orig*
8.54 - cd ..
8.55 - cd ..
8.56 + rm *~
8.57 + rm #*
8.58 + rm .#*
8.59 + rm *.tar*
8.60 + rm *.orig*
8.61 + cd course
8.62 + rm *~
8.63 + rm #*
8.64 + rm .#*
8.65 + rm *.tar*
8.66 + rm *.orig*
8.67 + cd ml_quickstart
8.68 + rm *~
8.69 + rm #*
8.70 + rm .#*
8.71 + rm *.tar*
8.72 + rm *.orig*
8.73 + cd ..
8.74 + cd phst11
8.75 + rm *~
8.76 + rm #*
8.77 + rm .#*
8.78 + rm *.tar*
8.79 + rm *.orig*
8.80 + cd ..
8.81 + cd SignalProcess
8.82 + rm *~
8.83 + rm #*
8.84 + rm .#*
8.85 + rm *.tar*
8.86 + rm *.orig*
8.87 + cd ..
8.88 + cd ..
8.89 + cd file-depend
8.90 + rm *~
8.91 + rm #*
8.92 + rm .#*
8.93 + rm *.tar*
8.94 + rm *.orig*
8.95 + cd ..
8.96 + cd test-depend
8.97 + rm *~
8.98 + rm #*
8.99 + rm .#*
8.100 + rm *.tar*
8.101 + rm *.orig*
8.102 + cd ..
8.103 + cd ..
8.104 cd ProgLang
8.105 - rm *~
8.106 - rm #*
8.107 - rm .#*
8.108 - rm *.tar*
8.109 - rm *.orig*
8.110 - cd ..
8.111 + rm *~
8.112 + rm #*
8.113 + rm .#*
8.114 + rm *.tar*
8.115 + rm *.orig*
8.116 + cd ..
8.117 cd Minisubpbl
8.118 - rm *~
8.119 - rm #*
8.120 - rm .#*
8.121 - rm *.tar*
8.122 - rm *.orig*
8.123 - cd ..
8.124 + rm *~
8.125 + rm #*
8.126 + rm .#*
8.127 + rm *.tar*
8.128 + rm *.orig*
8.129 + cd ..
8.130 +cd OLDTESTS
8.131 + rm *~
8.132 + rm #*
8.133 + rm .#*
8.134 + rm *.tar*
8.135 + rm *.orig*
8.136 + cd ..
8.137 cd Interpret
8.138 - rm *~
8.139 - rm #*
8.140 - rm .#*
8.141 - rm *.tar*
8.142 - rm *.orig*
8.143 - cd ..
8.144 + rm *~
8.145 + rm #*
8.146 + rm .#*
8.147 + rm *.tar*
8.148 + rm *.orig*
8.149 + cd ..
8.150 cd xmlsrc
8.151 - rm *~
8.152 - rm #*
8.153 - rm .#*
8.154 - rm *.tar*
8.155 - rm *.orig*
8.156 - cd ..
8.157 + rm *~
8.158 + rm #*
8.159 + rm .#*
8.160 + rm *.tar*
8.161 + rm *.orig*
8.162 + cd ..
8.163 cd Frontend
8.164 - rm *~
8.165 - rm #*
8.166 - rm .#*
8.167 - rm *.tar*
8.168 - rm *.orig*
8.169 - cd ..
8.170 + rm *~
8.171 + rm #*
8.172 + rm .#*
8.173 + rm *.tar*
8.174 + rm *.orig*
8.175 + cd ..
8.176 cd Knowledge
8.177 - rm *~
8.178 - rm #*
8.179 - rm .#*
8.180 - rm *.tar*
8.181 - rm *.orig*
8.182 - cd ..
8.183 + rm *~
8.184 + rm #*
8.185 + rm .#*
8.186 + rm *.tar*
8.187 + rm *.orig*
8.188 + cd ..
9.1 --- a/test/Tools/isac/Interpret/script.sml Wed Mar 07 15:58:18 2012 +0100
9.2 +++ b/test/Tools/isac/Interpret/script.sml Sat Mar 10 14:38:18 2012 +0100
9.3 @@ -135,10 +135,9 @@
9.4 val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.5 case nxt of (_, Apply_Method ["IntegrierenUndKonstanteBestimmen"]) => ()
9.6 | _ => error "script.sml, doesnt find Substitute #2";
9.7 -
9.8 -(*========== inhibit exn AK110721 ================================================
9.9 (* ERROR: caused by f2str f *)
9.10 trace_rewrite:=true;
9.11 +
9.12 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f(*------------------------*);
9.13 trace_rewrite:=false;
9.14 (*Exception TYPE raised:
9.15 @@ -155,22 +154,12 @@
9.16 ... this was because eval_argument_in took "argument_in (lhs (M_b 0 = 0))"
9.17 ie. the argument had not been simplified before ^^^^^^^^^^^^^^^
9.18 thus corrected eval_argument_in OK*)
9.19 -========== inhibit exn AK110721 ================================================*)
9.20 -
9.21 val {srls,...} = get_met ["IntegrierenUndKonstanteBestimmen"];
9.22 -val e1__e1 = str2term "nth_nth 1 [M_b 0 = 0, M_b L = 0]";
9.23 +val e1__e1 = str2term "NTH 1 [M_b 0 = 0, M_b L = 0]";
9.24 val e1__e1 = eval_listexpr_ @{theory Biegelinie} srls e1__e1; term2str e1__e1;
9.25 -
9.26 -(*========== inhibit exn 110721 ================================================
9.27 -(*AK110722
9.28 - TRIAL: Should be the same
9.29 - term2str e1__e1 = "M_b 0 = 0";
9.30 - term2str e1__e1;*)
9.31 -
9.32 if term2str e1__e1 = "M_b 0 = 0"
9.33 then ()
9.34 else error"script.sml diff.beh. eval_listexpr_ nth_nth 1 [...";
9.35 -========== inhibit exn 110721 ================================================*)
9.36
9.37 (*TODO.WN050913 ??? doesnt eval_listexpr_ go into subterms ???...
9.38 val x1__ = str2term"argument_in (lhs (M_b 0 = 0))";
9.39 @@ -180,16 +169,13 @@
9.40 val SOME (str, t) = eval_lhs 0 "Tools.lhs" (str2term"lhs (M_b 0 = 0)") 0;*)
9.41
9.42 val l__l = str2term "lhs (M_b 0 = 0)";
9.43 -(*AK110722 eval_listexpr_ is prob. without _ ????*)
9.44 val l__l = eval_listexpr_ @{theory Biegelinie} srls l__l; term2str l__l;
9.45 val SOME (str, t) = eval_lhs 0 "Tools.lhs" (str2term "lhs (M_b 0 = 0)") 0;
9.46 -(*========== inhibit exn 110721 ================================================
9.47 -trace_rewrite:=true;
9.48 +
9.49 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f (*------------------------*);
9.50 -trace_rewrite:=false;
9.51 -========== inhibit exn 110721 ================================================*)
9.52 +if nxt = ("Rewrite", Rewrite ("Belastung_Querkraft", "Biegelinie.Belastung_Querkraft"))
9.53 +then () else error "";
9.54
9.55 -show_mets();
9.56
9.57 "----------- fun sel_appl_atomic_tacs ----------------------------";
9.58 "----------- fun sel_appl_atomic_tacs ----------------------------";
10.1 --- a/test/Tools/isac/Knowledge/Rational_Test.thy Wed Mar 07 15:58:18 2012 +0100
10.2 +++ b/test/Tools/isac/Knowledge/Rational_Test.thy Sat Mar 10 14:38:18 2012 +0100
10.3 @@ -1,3 +1,7 @@
10.4 +(* code describing task of Diana Meindl
10.5 + TODO transfer where to ?
10.6 +*)
10.7 +
10.8 theory Rational_Test imports Complex_Main begin
10.9
10.10 lemma cancel_2011:
11.1 --- a/test/Tools/isac/Knowledge/algein.sml Wed Mar 07 15:58:18 2012 +0100
11.2 +++ b/test/Tools/isac/Knowledge/algein.sml Sat Mar 10 14:38:18 2012 +0100
11.3 @@ -1,9 +1,6 @@
11.4 (* tests on AlgEin, Algebra Einf"uhrung, , Unterrichtsversuch IMST-Projekt
11.5 author: Walther Neuper 2007
11.6 (c) due to copyright terms
11.7 -
11.8 -use"../smltest/IsacKnowledge/algein.sml";
11.9 -use"algein.sml";
11.10 *)
11.11
11.12 "-----------------------------------------------------------------";
11.13 @@ -27,37 +24,28 @@
11.14 "----------- build method 'Berechnung' 'erstSymbolisch' ----------";
11.15 "----------- build method 'Berechnung' 'erstSymbolisch' ----------";
11.16 val str =
11.17 -"Script RechnenSymbolScript (k_::bool) (q__::bool) \
11.18 -\(u_::bool list) (s_::bool list) (o_::bool list) (l_::real) =\
11.19 -\ (let t_ = (l_ = 1)\
11.20 -\ in t_)"
11.21 +"Script RechnenSymbolScript (k_k::bool) (q__q::bool) \
11.22 +\(u_u::bool list) (s_s::bool list) (o_o::bool list) (l_l::real) =\
11.23 +\ (let t_t = (l_l = 1)\
11.24 +\ in t_t)"
11.25 ;
11.26 -(*=== inhibit exn 110722=============================================================
11.27 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
11.28 -=== inhibit exn 110722=============================================================*)
11.29 -
11.30 -
11.31 -(*=== inhibit exn 110722=============================================================
11.32 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
11.33 -
11.34 atomty sc;
11.35 atomt sc;
11.36 -=== inhibit exn 110722=============================================================*)
11.37
11.38 "----------- me 'Berechnung' 'erstNumerisch' ---------------------";
11.39 "----------- me 'Berechnung' 'erstNumerisch' ---------------------";
11.40 "----------- me 'Berechnung' 'erstNumerisch' ---------------------";
11.41 val fmz =
11.42 - ["KantenLaenge (k=10)","Querschnitt (q=1)",
11.43 - "KantenUnten [b1 = k - 2*q, b2 = k - 2*q, b3 = k - 2*q, b4 = k - 2*q ]",
11.44 - "KantenSenkrecht [v1 = k, v2 = k, v3 = k, v4 = k]",
11.45 - "KantenOben [t1 = k - 2*q, t2 = k - 2*q, t3 = k - 2*q, t4 = k - 2*q ]",
11.46 + ["KantenLaenge (k=(10::real))","Querschnitt (q=(1::real))",
11.47 + "KantenUnten [b1 = k - 2*(q::real), b2 = k - 2*(q::real), b3 = k - 2*(q::real), b4 = k - 2*(q::real) ]",
11.48 + "KantenSenkrecht [v1 = (k::real), v2 = (k::real), v3 = (k::real), v4 = (k::real)]",
11.49 + "KantenOben [t1 = k - 2*(q::real), t2 = k - 2*(q::real), t3 = k - 2*(q::real), t4 = k - 2*(q::real) ]",
11.50 "GesamtLaenge L"];
11.51 val (dI',pI',mI') =
11.52 ("Isac",["numerischSymbolische", "Berechnung"],
11.53 ["Berechnung","erstNumerisch"]);
11.54 val p = e_pos'; val c = [];
11.55 -(*=== inhibit exn 110722=============================================================
11.56 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))](*nxt = ("Model_Pr*);
11.57 val (p,_,f,nxt,_,pt) = me nxt p c pt(*Add_Given "KantenLaenge (k = 10)"*);
11.58 val (p,_,f,nxt,_,pt) = me nxt p c pt(*Add_Given "Querschnitt (q = 1)"*);
11.59 @@ -88,63 +76,48 @@
11.60 if f2str f = "L = 104" andalso nxt = ("End_Proof'", End_Proof') then ()
11.61 else error "algein.sml diff.behav. in erstSymbolisch 99";
11.62 DEconstrCalcTree 1;
11.63 -=== inhibit exn 110722=============================================================*)
11.64
11.65 "----------- auto 'Berechnung' 'erstSymbolisch' ------------------";
11.66 "----------- auto 'Berechnung' 'erstSymbolisch' ------------------";
11.67 "----------- auto 'Berechnung' 'erstSymbolisch' ------------------";
11.68 CalcTree
11.69 -[(["KantenLaenge (k=10)","Querschnitt (q=1)",
11.70 - "KantenUnten [b1 = k - 2*q, b2 = k - 2*q, b3 = k - 2*q, b4 = k - 2*q ]",
11.71 - "KantenSenkrecht [v1 = k, v2 = k, v3 = k, v4 = k]",
11.72 - "KantenOben [t1 = k - 2*q, t2 = k - 2*q, t3 = k - 2*q, t4 = k - 2*q ]",
11.73 - "GesamtLaenge L"],
11.74 +[(["KantenLaenge (k=(10::real))","Querschnitt (q=(1::real))",
11.75 + "KantenUnten [b1 = k - 2*(q::real), b2 = k - 2*(q::real), b3 = k - 2*(q::real), b4 = k - 2*(q::real) ]",
11.76 + "KantenSenkrecht [v1 = (k::real), v2 = (k::real), v3 = (k::real), v4 = (k::real)]",
11.77 + "KantenOben [t1 = k - 2*(q::real), t2 = k - 2*(q::real), t3 = k - 2*(q::real), t4 = k - 2*(q::real) ]",
11.78 + "GesamtLaenge L"],
11.79 ("Isac",["numerischSymbolische", "Berechnung"],
11.80 ["Berechnung","erstSymbolisch"]))];
11.81 Iterator 1;
11.82 moveActiveRoot 1;
11.83 autoCalculate 1 CompleteCalc;
11.84 val ((pt,p),_) = get_calc 1; show_pt pt;
11.85 -(*=== inhibit exn 110722=============================================================
11.86 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = "L = 104" then()
11.87 else error "algein.sml: 'Berechnung' 'erstSymbolisch' changed";
11.88 -===== inhibit exn 110722===========================================================*)
11.89 -(*
11.90 -show_pt pt;
11.91 -trace_rewrite:=true;
11.92 -trace_rewrite:=false;
11.93 -trace_script:=true;
11.94 -trace_script:=false;
11.95 -*)
11.96 +
11.97 "----------- Widerspruch 3 = 777 ---------------------------------";
11.98 "----------- Widerspruch 3 = 777 ---------------------------------";
11.99 "----------- Widerspruch 3 = 777 ---------------------------------";
11.100 val thy = @{theory "Isac"};
11.101 val rew_ord = dummy_ord;
11.102 val erls = Erls;
11.103 -(*===== inhibit exn 110722===========================================================
11.104 -val thm = assoc_thm' thy ("sym_real_mult_0_right","");
11.105 -val t = str2term "0 = 0";
11.106 +val thm = assoc_thm' thy ("sym_mult_zero_right","");
11.107 +val t = str2term "0 = (0::real)";
11.108 val SOME (t',_) = rewrite_ thy rew_ord erls false thm t;
11.109 -term2str t';
11.110 -(********"0 = ?z1 * 0"*)
11.111 +term2str t' = "0 = ?a1 * 0"; (* = true*)
11.112
11.113 (*testing code in ME/appl.sml*)
11.114 -val sube = ["?z1 = 3"];
11.115 +val sube = ["?a1 = (3::real)"];
11.116 val subte = sube2subte sube;
11.117 +terms2str' subte = "[?a1 = 3]"; (* = true*)
11.118 val subst = sube2subst thy sube;
11.119 foldl and_ (true, map contains_Var subte);
11.120
11.121 val t'' = subst_atomic subst t';
11.122 -term2str t'';
11.123 -(********"0 = 3 * 0"*)
11.124 -===== inhibit exn 110722===========================================================*)
11.125 +term2str t'' = "0 = 3 * 0"; (* = true*)
11.126
11.127 val thm = assoc_thm' thy ("sym","");
11.128 (*----- STOPPED.WN0x?: Widerspruch 3 = 777: sym contains "==>" instead of "=" !!!
11.129 val SOME (t''',_) = rewrite_ thy rew_ord erls false thm t'';
11.130 *)
11.131
11.132 -(* use"../smltest/IsacKnowledge/algein.sml";
11.133 - *)
11.134 -
12.1 --- a/test/Tools/isac/Knowledge/biegelinie.sml Wed Mar 07 15:58:18 2012 +0100
12.2 +++ b/test/Tools/isac/Knowledge/biegelinie.sml Sat Mar 10 14:38:18 2012 +0100
12.3 @@ -1,9 +1,6 @@
12.4 (* tests on biegelinie
12.5 author: Walther Neuper 050826
12.6 (c) due to copyright terms
12.7 -
12.8 -use"../smltest/IsacKnowledge/biegelinie.sml";
12.9 -use"biegelinie.sml";
12.10 *)
12.11
12.12 "-----------------------------------------------------------------";
12.13 @@ -17,7 +14,6 @@
12.14 "----------- SubProblem (_,[vonBelastungZu,Biegelinien] ----------";
12.15 "----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
12.16 "----------- method [Biegelinien,setzeRandbedingungenEin] + exec -";
12.17 -"----------- method [Biegelinien,setzeRandbedingungenEin]FAST ----";
12.18 "----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. --------";
12.19 "----------- investigate normalforms in biegelinien --------------";
12.20 "-----------------------------------------------------------------";
12.21 @@ -25,51 +21,42 @@
12.22 "-----------------------------------------------------------------";
12.23
12.24 val thy = @{theory "Biegelinie"};
12.25 -(*=== inhibit exn 110722=============================================================
12.26 +val ctxt = thy2ctxt' "Biegelinie";
12.27 +fun str2term str = (term_of o the o (parse thy)) str;
12.28 +fun term2s t = Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt' "Biegelinie")) t;
12.29 +fun rewrit thm str =
12.30 + fst (the (rewrite_ thy tless_true e_rls true thm str));
12.31
12.32 "----------- the rules -------------------------------------------";
12.33 "----------- the rules -------------------------------------------";
12.34 "----------- the rules -------------------------------------------";
12.35 -fun str2term str = (term_of o the o (parse thy)) str;
12.36 -fun term2s t = Syntax.string_of_term (thy2ctxt' "Biegelinie") t;
12.37 -fun rewrit thm str =
12.38 - fst (the (rewrite_ Biegelinie.thy tless_true e_rls true thm str));
12.39 -
12.40 -val t = rewrit Belastung_Querkraft (str2term "- q_ x = - q_0"); term2s t;
12.41 +val t = rewrit @{thm Belastung_Querkraft} (str2term "- qq x = - q_0"); term2s t;
12.42 if term2s t = "Q' x = - q_0" then ()
12.43 else error "/biegelinie.sml: Belastung_Querkraft";
12.44
12.45 -val t = rewrit Querkraft_Moment (str2term "Q x = - q_0 * x + c"); term2s t;
12.46 +val t = rewrit @{thm Querkraft_Moment} (str2term "Q x = - q_0 * x + c"); term2s t;
12.47 if term2s t = "M_b' x = - q_0 * x + c" then ()
12.48 else error "/biegelinie.sml: Querkraft_Moment";
12.49
12.50 -val t = rewrit Moment_Neigung (str2term "M_b x = -q_0 * x^^^2/2 + q_0/2 *L*x");
12.51 +val t = rewrit @{thm Moment_Neigung} (str2term "M_b x = -q_0 * x^^^2/2 + q_0/2 *L*x");
12.52 term2s t;
12.53 if term2s t = "- EI * y'' x = - q_0 * x ^^^ 2 / 2 + q_0 / 2 * L * x" then ()
12.54 else error "biegelinie.sml: Moment_Neigung";
12.55 -=== inhibit exn 110722=============================================================*)
12.56 -
12.57 -
12.58 -(*=== inhibit exn 110722=============================================================
12.59 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
12.60 -
12.61 -atomty sc;
12.62 -atomt sc;
12.63 -=== inhibit exn 110722=============================================================*)
12.64 -
12.65 -(* use"../smltest/IsacKnowledge/biegelinie.sml";
12.66 - *)
12.67
12.68 "----------- IntegrierenUndKonstanteBestimmen by rewriting -------";
12.69 "----------- IntegrierenUndKonstanteBestimmen by rewriting -------";
12.70 "----------- IntegrierenUndKonstanteBestimmen by rewriting -------";
12.71 +"----------- IntegrierenUndKonstanteBestimmen by rewriting -------";
12.72 val t = str2term "M_b x = L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2";
12.73 -(*=== inhibit exn 110722=============================================================
12.74 -val t = rewrit Moment_Neigung t; term2s t;
12.75 -(*was "EI * ?y'' x = L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2"
12.76 - ### before declaring "y''" as a constant *)
12.77 -val t = rewrit make_fun_explicit t; term2s t;
12.78 +val t = rewrit @{thm Moment_Neigung} t;
12.79 +if term2s t = "- EI * y'' x = L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2" then ()
12.80 +else error "Moment_Neigung broken";
12.81 +(* was I * ?y'' x = L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2"
12.82 + before declaring "y''" as a constant *)
12.83
12.84 +val t = rewrit @{thm make_fun_explicit} t;
12.85 +if term2s t = "y'' x = 1 / - EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)" then ()
12.86 +else error "make_fun_explicit broken";
12.87
12.88 "----------- simplify_leaf for this script -----------------------";
12.89 "----------- simplify_leaf for this script -----------------------";
12.90 @@ -78,42 +65,35 @@
12.91 preconds = [],
12.92 rew_ord = ("termlessI",termlessI),
12.93 erls = append_rls "erls_in_srls_IntegrierenUnd.." e_rls
12.94 - [(*for asm in nth_Cons_ ...*)
12.95 + [(*for asm in NTH_CONS ...*)
12.96 Calc ("Orderings.ord_class.less",eval_equ "#less_"),
12.97 - (*2nd nth_Cons_ pushes n+-1 into asms*)
12.98 + (*2nd NTH_CONS pushes n+-1 into asms*)
12.99 Calc("Groups.plus_class.plus", eval_binop "#add_")
12.100 ],
12.101 srls = Erls, calc = [],
12.102 - rules = [Thm ("nth_Cons_",num_str @{thm nth_Cons_}),
12.103 + rules = [Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
12.104 Calc("Groups.plus_class.plus", eval_binop "#add_"),
12.105 - Thm ("nth_Nil_",num_str @{thm nth_Nil_}),
12.106 - Calc("Tools.lhs", eval_lhs"eval_lhs_"),
12.107 - Calc("Tools.rhs", eval_rhs"eval_rhs_"),
12.108 - Calc("Atools.argument'_in",
12.109 - eval_argument_in "Atools.argument'_in")
12.110 + Thm ("NTH_NIL",num_str @{thm NTH_NIL}),
12.111 + Calc("Tools.lhs", eval_lhs "eval_lhs_"),
12.112 + Calc("Tools.rhs", eval_rhs "eval_rhs_"),
12.113 + Calc("Atools.argument'_in", eval_argument_in "Atools.argument'_in")
12.114 ],
12.115 scr = EmptyScr};
12.116 -=== inhibit exn 110722=============================================================*)
12.117 val rm_ = str2term"[M_b 0 = 0, M_b L = 0]";
12.118 val M__ = str2term"M_b x = -1 * x ^^^ 2 / 2 + x * c + c_2";
12.119 -(*=== inhibit exn 110722=============================================================
12.120 -val SOME (e1__l,_) =
12.121 - rewrite_set_ thy false srls
12.122 - (str2term"(nth_::[real,bool list]=>bool) 1 " $ rm_);
12.123 -if term2str e1__ = "M_b 0 = 0" then ()
12.124 -else error "biegelinie.sml simplify nth_ 1 rm_";
12.125 +val SOME (e1__,_) = rewrite_set_ thy false srls
12.126 + (str2term "(NTH::[real,bool list]=>bool) 1 " $ rm_);
12.127 +if term2str e1__ = "M_b 0 = 0" then () else error "biegelinie.sml simplify NTH 1 rm_";
12.128
12.129 val SOME (x1__,_) =
12.130 rewrite_set_ thy false srls
12.131 (str2term"argument_in (lhs (M_b 0 = 0))");
12.132 if term2str x1__ = "0" then ()
12.133 else error "biegelinie.sml simplify argument_in (lhs (M_b 0 = 0)";
12.134 -=== inhibit exn 110722=============================================================*)
12.135
12.136 trace_rewrite:=true;
12.137 trace_rewrite:=false;
12.138
12.139 -
12.140 "----------- Bsp 7.27 me -----------------------------------------";
12.141 "----------- Bsp 7.27 me -----------------------------------------";
12.142 "----------- Bsp 7.27 me -----------------------------------------";
12.143 @@ -141,13 +121,14 @@
12.144 val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.145 case nxt of (_,Add_Given "FunktionsVariable x") => ()
12.146 | _ => error "biegelinie.sml: Bsp 7.27 #4a";
12.147 +
12.148 val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.149 val mits = get_obj g_met pt (fst p);writeln (itms2str_ ctxt mits);
12.150 (*if itms2str_ ctxt mits = ... all 6 guard-items*)
12.151 case nxt of (_, Apply_Method ["IntegrierenUndKonstanteBestimmen"]) => ()
12.152 | _ => error "biegelinie.sml: Bsp 7.27 #4b";
12.153
12.154 -(*=== inhibit exn 110722=============================================================
12.155 +"===== Apply_Method IntegrierenUndKonstanteBestimmen ============================";
12.156 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
12.157 case pt of Nd (PblObj _, [Nd _]) => ((*Apply_Method + Take*))
12.158 | _ => error "biegelinie.sml: Bsp 7.27 #4c";
12.159 @@ -342,10 +323,7 @@
12.160 else error "biegelinie.sml: Bsp 7.27 #24 f";
12.161 case nxt of ("End_Proof'", End_Proof') => ()
12.162 | _ => error "biegelinie.sml: Bsp 7.27 #24";
12.163 -=== inhibit exn 110722=============================================================*)
12.164
12.165 -(* use"../smltest/IsacKnowledge/biegelinie.sml";
12.166 - *)
12.167 show_pt pt;
12.168 (*(([], Frm), Problem (Biegelinie.thy, [MomentBestimmte, Biegelinien])),
12.169 (([1], Frm), q_ x = q_0),
12.170 @@ -416,12 +394,10 @@
12.171
12.172 autoCalculate 1 CompleteCalc;
12.173 val ((pt,p),_) = get_calc 1;
12.174 -(*=== inhibit exn 110722=============================================================
12.175 if p = ([], Res) andalso length (children pt) = 23 andalso
12.176 term2str (get_obj g_res pt (fst p)) =
12.177 "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)"
12.178 then () else error "biegelinie.sml: 1st biegelin.7.27 changed";
12.179 -=== inhibit exn 110722=============================================================*)
12.180
12.181 val (unc, del, gen) = (([],Pbl), ([],Pbl), ([],Res));
12.182 getFormulaeFromTo 1 unc gen 1 (*only level 1*) false;
12.183 @@ -455,7 +431,7 @@
12.184 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.185 if nxt = ("Apply_Method", Apply_Method ["Biegelinien", "ausBelastung"])
12.186 then () else error "biegelinie.sml met2 b";
12.187 -(*=== inhibit exn 110722=============================================================
12.188 +(*=== inhibit exn 110722=============================================================*)
12.189
12.190 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "q_ x = q_0";
12.191 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "- q_ x = - q_0";
12.192 @@ -515,58 +491,14 @@
12.193 if nxt = ("End_Proof'", End_Proof') andalso f2str f =
12.194 "[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 ()
12.195 else error "biegelinie.sml met2 e";
12.196 -=== inhibit exn 110722=============================================================*)
12.197 -
12.198
12.199
12.200 "----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
12.201 "----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
12.202 "----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
12.203 -val str =
12.204 -"Script Function2Equality (fun_::bool) (sub_::bool) =\
12.205 -\(equ___::bool)"
12.206 -;
12.207 -(*=== inhibit exn 110722=============================================================
12.208 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
12.209 -val str =
12.210 -"Script Function2Equality (fun_::bool) (sub_::bool) =\
12.211 -\ (let v_v = argument_in (lhs fun_)\
12.212 -\ in (equ___::bool))"
12.213 -;
12.214 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
12.215 -val str =
12.216 -"Script Function2Equality (fun_::bool) (sub_::bool) =\
12.217 -\ (let v_v = argument_in (lhs fun_);\
12.218 -\ (equ_) = (Substitute [sub_]) fun_\
12.219 -\ in (equ_::bool))"
12.220 -;
12.221 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
12.222 -val str =
12.223 -"Script Function2Equality (fun_::bool) (sub_::bool) =\
12.224 -\ (let v_v = argument_in (lhs fun_);\
12.225 -\ equ_ = (Substitute [sub_]) fun_\
12.226 -\ in (Rewrite_Set_Inst [(bdv, v_v)] make_ratpoly_in False) equ_)"
12.227 -;
12.228 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
12.229 -=== inhibit exn 110722=============================================================*)
12.230 -
12.231 -val str =
12.232 -(*(M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2) (M_b L = 0) -->
12.233 - 0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2*)
12.234 -"Script Function2Equality (fun_::bool) (sub_::bool) =\
12.235 -\ (let bdv_ = argument_in (lhs fun_);\
12.236 -\ val_ = argument_in (lhs sub_);\
12.237 -\ equ_ = (Substitute [bdv_ = val_]) fun_;\
12.238 -\ equ_ = (Substitute [sub_]) fun_\
12.239 -\ in (Rewrite_Set_Inst [(bdv_, v_v)] make_ratpoly_in False) equ_)"
12.240 -;
12.241 -(*=== inhibit exn 110722=============================================================
12.242 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
12.243 -atomty sc;
12.244 -
12.245 val fmz = ["functionEq (M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2)",
12.246 "substitution (M_b L = 0)",
12.247 - "equality equ___"];
12.248 + "equality equ_equ"];
12.249 val (dI',pI',mI') = ("Biegelinie", ["makeFunctionTo","equation"],
12.250 ["Equation","fromFunction"]);
12.251 val p = e_pos'; val c = [];
12.252 @@ -589,80 +521,23 @@
12.253 CHANGE NOT considered, already on leave*)
12.254 f2str f = "0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2"
12.255 then () else error "biegelinie.sml: SubProblem (_,[setzeRandbed";
12.256 -=== inhibit exn 110722=============================================================*)
12.257
12.258
12.259 "----------- method [Biegelinien,setzeRandbedingungenEin] + exec -";
12.260 "----------- method [Biegelinien,setzeRandbedingungenEin] + exec -";
12.261 "----------- method [Biegelinien,setzeRandbedingungenEin] + exec -";
12.262 "----- check the scripts syntax";
12.263 -val str =
12.264 -"Script SetzeRandbedScript (funs_::bool list) (beds_::bool list) =\
12.265 -\ (let b1 = Take (nth_ 1 beds_)\
12.266 -\ in (equs_::bool list))"
12.267 -;
12.268 -(*=== inhibit exn 110722=============================================================
12.269 -
12.270 -(*show_types := true;*)
12.271 -val funs_ = str2term "funs_::bool list";
12.272 -val funs = str2term
12.273 - "[Q x = c + -1 * q_0 * x,\
12.274 - \M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2,\
12.275 - \y' x = c_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3),\
12.276 - \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)]";
12.277 -val rb_ = str2term "rb_::bool list";
12.278 -val rb = str2term "[y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]";
12.279 -
12.280 -"--- script expression 1";
12.281 -val screxp1_ = str2term "Take (nth_ 1 (rb_::bool list))";
12.282 -val screxp1 = subst_atomic [(rb_, rb)] screxp1_; term2str screxp1;
12.283 -val SOME (b1,_) = rewrite_set_ (theory "Isac") false srls2 screxp1; term2str b1;
12.284 -if term2str b1 = "Take (y 0 = 0)" then ()
12.285 -else error "biegelinie.sml: rew. Bieglie2 --1";
12.286 -val b1 = str2term "(y 0 = 0)";
12.287 -
12.288 -"--- script expression 2";
12.289 -val screxp2_ = str2term "filter (sameFunId (lhs b1_)) funs_";
12.290 -val b1_ = str2term "b1_::bool";
12.291 -val screxp2 = subst_atomic [(b1_,b1),(funs_,funs)] screxp2_; term2str screxp2;
12.292 -val SOME (fs,_) = rewrite_set_ (theory "Isac") false srls2 screxp2; term2str fs;
12.293 -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 ()
12.294 -else error "biegelinie.sml: rew. Bieglie2 --2";
12.295 -
12.296 -"--- script expression 3";
12.297 -val screxp3_ = str2term "SubProblem (Biegelinie_,[makeFunctionTo,equation],\
12.298 -\ [Equation,fromFunction]) \
12.299 -\ [BOOL (hd fs_), BOOL b1_]";
12.300 -val fs_ = str2term "fs_::bool list";
12.301 -val screxp3 = subst_atomic [(fs_,fs),(b1_,b1)] screxp3_;
12.302 -writeln (term2str screxp3);
12.303 -val SOME (equ,_) = rewrite_set_ (theory "Isac") false srls2 screxp3;
12.304 -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 ()
12.305 -else error "biegelinie.sml: rew. Bieglie2 --3";
12.306 -writeln (term2str equ);
12.307 -(*SubProblem
12.308 - (Biegelinie_, [makeFunctionTo, equation], [Equation, fromFunction])
12.309 - [BOOL
12.310 - (y x =
12.311 - c_4 + c_3 * x +
12.312 - 1 / (-1 * EI) *
12.313 - (c_2 / 2 * x ^^^ 2 + c / 6 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)),
12.314 - BOOL (y 0 = 0)]*)
12.315 -show_types := false;
12.316 -=== inhibit exn 110722=============================================================*)
12.317 -
12.318 -
12.319 +(*WN120309 deleted*)
12.320 "----- execute script by interpreter: setzeRandbedingungenEin";
12.321 -val fmz = ["Funktionen [Q x = c + -1 * q_0 * x,\
12.322 - \M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2,\
12.323 - \y' x = c_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3),\
12.324 - \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)]",
12.325 +val fmz = ["Funktionen [Q x = c + -1 * q_0 * x," ^
12.326 + "M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2," ^
12.327 + "y' x = c_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)," ^
12.328 + "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)]",
12.329 "Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]",
12.330 - "Gleichungen equs___"];
12.331 + "Gleichungen equ_s"];
12.332 val (dI',pI',mI') = ("Biegelinie", ["setzeRandbedingungen","Biegelinien"],
12.333 ["Biegelinien","setzeRandbedingungenEin"]);
12.334 val p = e_pos'; val c = [];
12.335 -(*=== inhibit exn 110722=============================================================
12.336 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
12.337 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.338 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.339 @@ -676,8 +551,9 @@
12.340 "----- Randbedingung y 0 = 0 in SUBpbl with met [Equation, fromFunction]";
12.341 val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.342 if (#1 o (get_obj g_fmz pt)) (fst p) =
12.343 - ["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))",
12.344 - "substitution (y 0 = 0)", "equality equ___"] then ()
12.345 + ["functionEq\n (y x =\n c_4 + c_3 * x +\n 1 / (-1 * EI) *" ^
12.346 + "\n (c_2 / 2 * x ^^^ 2 + c / 6 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4))",
12.347 + "substitution (y 0 = 0)", "equality equ'''"] then ()
12.348 else error "biegelinie.sml met setzeRandbed*Ein bb";
12.349 (writeln o istate2str) (get_istate pt p);
12.350 "--- after 1.subpbl [Equation, fromFunction]";
12.351 @@ -704,7 +580,7 @@
12.352 val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.353 if (#1 o (get_obj g_fmz pt)) (fst p) =
12.354 ["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))",
12.355 - "substitution (y L = 0)", "equality equ___"] then ()
12.356 + "substitution (y L = 0)", "equality equ'''"] then ()
12.357 else error "biegelinie.sml metsetzeRandbed*Ein bb ";
12.358 val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.359 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.360 @@ -755,63 +631,10 @@
12.361 (* "[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]" *)
12.362 "[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]"
12.363 then () else error "biegelinie.sml met2 oo";
12.364 -=== inhibit exn 110722=============================================================*)
12.365 -
12.366 -(*
12.367 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
12.368 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.369 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.370 -*)
12.371 -
12.372 -"----------- method [Biegelinien,setzeRandbedingungenEin]FAST ----";
12.373 -"----------- method [Biegelinien,setzeRandbedingungenEin]FAST ----";
12.374 -"----------- method [Biegelinien,setzeRandbedingungenEin]FAST ----";
12.375 -val str =
12.376 -"Script SetzeRandbedScript (funs_::bool list) (rb_::bool list) = \
12.377 -\ (let b1_ = nth_ 1 rb_; \
12.378 -\ (fs_::bool list) = filter_sameFunId (lhs b1_) funs_; \
12.379 -\ (e1_::bool) = \
12.380 -\ (SubProblem (Biegelinie_,[makeFunctionTo,equation],\
12.381 -\ [Equation,fromFunction]) \
12.382 -\ [BOOL (hd fs_), BOOL b1_]) \
12.383 -\ in [e1_,e2_,e3_,e4_])"
12.384 -;
12.385 -
12.386 -
12.387
12.388 "----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. --------";
12.389 "----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. --------";
12.390 "----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. --------";
12.391 -"----- script ";
12.392 -val str =
12.393 -"Script Belastung2BiegelScript (q__::real) (v_v::real) = \
12.394 -\ (let q___ = Take (q_ v_v = q__); \
12.395 -\ q___ = ((Rewrite sym_real_minus_eq_cancel True) @@ \
12.396 -\ (Rewrite Belastung_Querkraft True)) q___; \
12.397 -\ (Q__:: bool) = \
12.398 -\ (SubProblem (Biegelinie_,[named,integrate,function], \
12.399 -\ [diff,integration,named]) \
12.400 -\ [REAL (rhs q___), REAL v_v, real_REAL Q]); \
12.401 -\ M__ = Rewrite Querkraft_Moment True Q__; \
12.402 -\ (M__::bool) = \
12.403 -\ (SubProblem (Biegelinie_,[named,integrate,function], \
12.404 -\ [diff,integration,named]) \
12.405 -\ [REAL (rhs M__), REAL v_v, real_REAL M_b]); \
12.406 -\ N__ = ((Rewrite Moment_Neigung False) @@ \
12.407 -\ (Rewrite make_fun_explicit False)) M__; \
12.408 -\ (N__:: bool) = \
12.409 -\ (SubProblem (Biegelinie_,[named,integrate,function], \
12.410 -\ [diff,integration,named]) \
12.411 -\ [REAL (rhs N__), REAL v_v, real_REAL y']); \
12.412 -\ (B__:: bool) = \
12.413 -\ (SubProblem (Biegelinie_,[named,integrate,function], \
12.414 -\ [diff,integration,named]) \
12.415 -\ [REAL (rhs N__), REAL v_v, real_REAL y]) \
12.416 -\ in [Q__, M__, N__, B__])"
12.417 -;
12.418 -(*=== inhibit exn 110722=============================================================
12.419 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
12.420 -
12.421 "----- Bsp 7.70 with me";
12.422 val fmz = ["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
12.423 "Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]",
12.424 @@ -831,21 +654,21 @@
12.425 (*** actual arg(s) missing for '["(#Find, (Funktionen, funs_))"]' i.e. should be 'copy-named' by '*_._'
12.426 ... THIS MEANS:
12.427 #a# "Script Biegelinie2Script ..
12.428 -\ ... (SubProblem (Biegelinie_,[vonBelastungZu,Biegelinien], \
12.429 -\ [Biegelinien,ausBelastung]) \
12.430 -\ [REAL q__, REAL v_]); \
12.431 +" ... (SubProblem (Biegelinie_,[vonBelastungZu,Biegelinien], " ^
12.432 +" [Biegelinien,ausBelastung]) " ^
12.433 +" [REAL q__, REAL v_]); "
12.434
12.435 #b# prep_met ... (["Biegelinien","ausBelastung"],
12.436 ... ("#Given" ,["Streckenlast q__","FunktionsVariable v_v"]),
12.437 - "Script Belastung2BiegelScript (q__::real) (v_v::real) = \
12.438 + "Script Belastung2BiegelScript (q__::real) (v_v::real) = "
12.439
12.440 #a#b# BOTH HAVE 2 ARGUMENTS q__ and v_v ...OK
12.441 ##########################################################################
12.442 BUT THE (#Find, (Funktionen, funs_)) IS NOT COPYNAMED BY funs___ !!!3*_!!!
12.443 ##########################################################################*)
12.444 -=== inhibit exn 110722=============================================================*)
12.445 -"further 'me' see ----- SubProblem (_,[vonBelastungZu,Biegelinien] -------\
12.446 -\ ----- SubProblem (_,[setzeRandbedingungen,Biegelinien] -";
12.447 +"further 'me' see ----- SubProblem (_,[vonBelastungZu,Biegelinien] -------" ^
12.448 +" ----- SubProblem (_,[setzeRandbedingungen,Biegelinien] -";
12.449 +
12.450 DEconstrCalcTree 1;
12.451 "----- Bsp 7.70 with autoCalculate";
12.452 CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
12.453 @@ -856,23 +679,21 @@
12.454 moveActiveRoot 1;
12.455 autoCalculate 1 CompleteCalc;
12.456 val ((pt,p),_) = get_calc 1; show_pt pt;
12.457 -(*=== inhibit exn 110722=============================================================
12.458 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) =
12.459 "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 ()
12.460 else error "biegelinie.sml: diff.behav.7.70 with autoCalculate";
12.461 -===== inhibit exn 110722===========================================================*)
12.462
12.463 val is = get_istate pt ([],Res); writeln (istate2str is);
12.464 -val t = str2term " last \
12.465 -\[Q x = L * q_0 + -1 * q_0 * x, \
12.466 -\ M_b x = -1 * q_0 * L ^^^ 2 / 2 + q_0 * L / 1 * x + -1 * q_0 / 2 * x ^^^ 2,\
12.467 -\ y' x = \
12.468 -\ -3 * q_0 * L ^^^ 2 / (-6 * EI) * x + 3 * L * q_0 / (-6 * EI) * x ^^^ 2 +\
12.469 -\ -1 * q_0 / (-6 * EI) * x ^^^ 3, \
12.470 -\ y x = \
12.471 -\ -6 * q_0 * L ^^^ 2 / (-24 * EI) * x ^^^ 2 + \
12.472 -\ 4 * L * q_0 / (-24 * EI) * x ^^^ 3 + \
12.473 -\ -1 * q_0 / (-24 * EI) * x ^^^ 4]";
12.474 +val t = str2term (" last " ^
12.475 +"[Q x = L * q_0 + -1 * q_0 * x, " ^
12.476 +" M_b x = -1 * q_0 * L ^^^ 2 / 2 + q_0 * L / 1 * x + -1 * q_0 / 2 * x ^^^ 2," ^
12.477 +" y' x = " ^
12.478 +" -3 * q_0 * L ^^^ 2 / (-6 * EI) * x + 3 * L * q_0 / (-6 * EI) * x ^^^ 2 +" ^
12.479 +" -1 * q_0 / (-6 * EI) * x ^^^ 3, " ^
12.480 +" y x = " ^
12.481 +" -6 * q_0 * L ^^^ 2 / (-24 * EI) * x ^^^ 2 + " ^
12.482 +" 4 * L * q_0 / (-24 * EI) * x ^^^ 3 + " ^
12.483 +" -1 * q_0 / (-24 * EI) * x ^^^ 4]");
12.484 val srls = append_rls "erls_IntegrierenUndK.." e_rls
12.485 [Calc("Tools.rhs", eval_rhs"eval_rhs_"),
12.486 Calc ("Atools.ident",eval_ident "#ident_"),
12.487 @@ -887,8 +708,6 @@
12.488 trace_rewrite := false;
12.489 term2str e1__;
12.490
12.491 -trace_script := true;
12.492 -trace_script := false;
12.493
12.494 "----------- investigate normalforms in biegelinien --------------";
12.495 "----------- investigate normalforms in biegelinien --------------";
13.1 --- a/test/Tools/isac/Knowledge/partial_fractions.sml Wed Mar 07 15:58:18 2012 +0100
13.2 +++ b/test/Tools/isac/Knowledge/partial_fractions.sml Sat Mar 10 14:38:18 2012 +0100
13.3 @@ -12,6 +12,8 @@
13.4 "----------- Logic.unvarify_global ----------------------";
13.5 "----------- eval_drop_questionmarks --------------------";
13.6 "----------- = me for met_partial_fraction --------------";
13.7 +"----------- progr.vers.2: check erls for multiply_ansatz";
13.8 +"----------- progr.vers.2: improve program --------------";
13.9 "--------------------------------------------------------";
13.10 "--------------------------------------------------------";
13.11 "--------------------------------------------------------";
13.12 @@ -219,3 +221,81 @@
13.13 if f2str f = "4 / (z - 1 / 2) + -4 / (z - -1 / 4)" then()
13.14 else error "= me .. met_partial_fraction broken";
13.15
13.16 +"----------- progr.vers.2: check erls for multiply_ansatz";
13.17 +"----------- progr.vers.2: check erls for multiply_ansatz";
13.18 +"----------- progr.vers.2: check erls for multiply_ansatz";
13.19 +(*test for outcommented 3 lines in script: is norm_Rational strong enough?*)
13.20 +val t = str2term "(3 / ((-1 + -2 * z + 8 * z ^^^ 2) *3/24)) = (3 / ((z - 1 / 2) * (z - -1 / 4)))";
13.21 +val SOME (t', _) = rewrite_set_ @{theory Isac} true ansatz_rls t;
13.22 +term2str t' = "3 / ((-1 + -2 * z + 8 * z ^^^ 2) * 3 / 24) =\n?A / (z - 1 / 2) + ?B / (z - -1 / 4)";
13.23 +
13.24 +val SOME (t'', _) = rewrite_set_ @{theory Isac} true multiply_ansatz t'; (*true*)
13.25 +term2str t'' = "(z - 1 / 2) * (z - -1 / 4) * 3 / ((-1 + -2 * z + 8 * z ^^^ 2) * 3 / 24) =\n" ^
13.26 + "?A * (z - -1 / 4) + ?B * (z - 1 / 2)"; (*true*)
13.27 +
13.28 +val SOME (t''', _) = rewrite_set_ @{theory Isac} true norm_Rational t'';
13.29 +if term2str t''' = "3 = ?A * (1 + 4 * z) / 4 + ?B * (-1 + 2 * z) / 2" then ()
13.30 +else error "ansatz_rls - multiply_ansatz - norm_Rational broken";
13.31 +
13.32 +(*test for outcommented 3 lines in script: empower erls for x = a*b ==> ...*)
13.33 +val xxx = append_rls "multiply_ansatz_erls" norm_Rational
13.34 + [Calc ("HOL.eq",eval_equal "#equal_")];
13.35 +
13.36 +val multiply_ansatz = prep_rls(
13.37 + Rls {id = "multiply_ansatz", preconds = [], rew_ord = ("dummy_ord",dummy_ord),
13.38 + erls = xxx,
13.39 + srls = Erls, calc = [],
13.40 + rules =
13.41 + [Thm ("multiply_2nd_order",num_str @{thm multiply_2nd_order})
13.42 + ],
13.43 + scr = EmptyScr}:rls);
13.44 +
13.45 +rewrite_set_ thy true xxx @{term "a+b = a+(b::real)"}; (*SOME ok*)
13.46 +rewrite_set_ thy true multiply_ansatz @{term "a+b = a+(b::real)"}; (*why NONE?: GOON*)
13.47 +
13.48 +"----------- progr.vers.2: improve program --------------";
13.49 +"----------- progr.vers.2: improve program --------------";
13.50 +"----------- progr.vers.2: improve program --------------";
13.51 +(*WN120318 stopped due to much effort with the test above*)
13.52 + "Script PartFracScript (f_f::real) (zzz::real) = " ^(*f_f: 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)), zzz: z*)
13.53 + " (let f_f = Take f_f; " ^
13.54 + " (num_orig::real) = get_numerator f_f; " ^(*num_orig: 3*)
13.55 + " f_f = (Rewrite_Set norm_Rational False) f_f; " ^(*f_f: 24 / (-1 + -2 * z + 8 * z ^^^ 2)*)
13.56 + " (numer::real) = get_numerator f_f; " ^(*numer: 24*)
13.57 + " (denom::real) = get_denominator f_f; " ^(*denom: -1 + -2 * z + 8 * z ^^^ 2*)
13.58 + " (equ::bool) = (denom = (0::real)); " ^(*equ: -1 + -2 * z + 8 * z ^^^ 2 = 0*)
13.59 + " (L_L::bool list) = (SubProblem (PolyEq', " ^
13.60 + " [abcFormula, degree_2, polynomial, univariate, equation], " ^
13.61 + " [no_met]) [BOOL equ, REAL zzz]); " ^(*L_L: [z = 1 / 2, z = -1 / 4]*)
13.62 + " (facs::real) = factors_from_solution L_L; " ^(*facs: (z - 1 / 2) * (z - -1 / 4)*)
13.63 + " (eql::real) = Take (num_orig / facs); " ^(*eql: 3 / ((z - 1 / 2) * (z - -1 / 4)) *)
13.64 + " (eqr::real) = (Try (Rewrite_Set ansatz_rls False)) eql; " ^(*eqr: ?A / (z - 1 / 2) + ?B / (z - -1 / 4)*)
13.65 + " (eq::bool) = Take (eql = eqr); " ^(*eq: 3 / ((z - 1 / 2) * (z - -1 / 4)) = ?A / (z - 1 / 2) + ?B / (z - -1 / 4)*)
13.66 +(*this has been tested below by rewrite_set_
13.67 + " (eeeee::bool) = Take ((num_orig / denom * denom / numer) = (num_orig / facs));" ^(**)
13.68 + " (eeeee::bool) = (Rewrite_Set ansatz_rls False) eeeee;" ^(**)
13.69 + " eq = (Try (Rewrite_Set multiply_ansatz False)) eeeee; " ^(*eq: 3 = ?A * (z - -1 / 4) + ?B * (z - 1 / 2)*)
13.70 +NEXT try to outcomment the very next line..*)
13.71 + " eq = (Try (Rewrite_Set equival_trans False)) eeeee; " ^(*eq: 3 = ?A * (z - -1 / 4) + ?B * (z - 1 / 2)*)
13.72 + " eq = drop_questionmarks eq; " ^(*eq: 3 = A * (z - -1 / 4) + B * (z - 1 / 2)*)
13.73 + " (z1::real) = (rhs (NTH 1 L_L)); " ^(*z1: 1 / 2*)
13.74 + " (z2::real) = (rhs (NTH 2 L_L)); " ^(*z2: -1 / 4*)
13.75 + " (eq_a::bool) = Take eq; " ^(*eq_a: 3 = A * (z - -1 / 4) + B * (z - 1 / 2)*)
13.76 + " eq_a = (Substitute [zzz = z1]) eq; " ^(*eq_a: 3 = A * (1 / 2 - -1 / 4) + B * (1 / 2 - 1 / 2)*)
13.77 + " eq_a = (Rewrite_Set norm_Rational False) eq_a; " ^(*eq_a: 3 = 3 * A / 4*)
13.78 + " (sol_a::bool list) = " ^
13.79 + " (SubProblem (Isac', [univariate,equation], [no_met]) " ^
13.80 + " [BOOL eq_a, REAL (A::real)]); " ^(*sol_a: [A = 4]*)
13.81 + " (a::real) = (rhs (NTH 1 sol_a)); " ^(*a: 4*)
13.82 + " (eq_b::bool) = Take eq; " ^(*eq_b: 3 = A * (z - -1 / 4) + B * (z - 1 / 2)*)
13.83 + " eq_b = (Substitute [zzz = z2]) eq_b; " ^(*eq_b: *)
13.84 + " eq_b = (Rewrite_Set norm_Rational False) eq_b; " ^(*eq_b: *)
13.85 + " (sol_b::bool list) = " ^
13.86 + " (SubProblem (Isac', [univariate,equation], [no_met]) " ^
13.87 + " [BOOL eq_b, REAL (B::real)]); " ^(*sol_b: [B = -4]*)
13.88 + " (b::real) = (rhs (NTH 1 sol_b)); " ^(*b: -4*)
13.89 + " eqr = drop_questionmarks eqr; " ^(*eqr: A / (z - 1 / 2) + B / (z - -1 / 4)*)
13.90 + " (pbz::real) = Take eqr; " ^(*pbz: A / (z - 1 / 2) + B / (z - -1 / 4)*)
13.91 + " pbz = ((Substitute [A = a, B = b]) pbz) " ^(*pbz: 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
13.92 + " in pbz)"
13.93 +
14.1 --- a/test/Tools/isac/Knowledge/polyeq.sml Wed Mar 07 15:58:18 2012 +0100
14.2 +++ b/test/Tools/isac/Knowledge/polyeq.sml Sat Mar 10 14:38:18 2012 +0100
14.3 @@ -200,15 +200,15 @@
14.4 l = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*false*);
14.5 (*WAS val NasApp _ =(astep_up (thy',srls,scr,d) ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]) )
14.6 ... Assoc ... is correct*)
14.7 -"~~~~~ and astep_up, args:"; val ((ys as (_,_,Script sc,_)), ((E,l,a,v,S,b),ss)) =
14.8 - ((thy',srls,scr,d), ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]));
14.9 +"~~~~~ and astep_up, args:"; val ((ys as (_,_,_,Script sc,_)), ((E,l,a,v,S,b),ss)) =
14.10 + ((thy',ctxt,srls,scr,d), ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]));
14.11 1 < length l (*true*);
14.12 val up = drop_last l;
14.13 term2str (go up sc);
14.14 (go up sc);
14.15 (*WAS val NasNap _ = ass_up ys ((E,up,a,v,S,b),ss) (go up sc)
14.16 ... ???? ... is correct*)
14.17 -"~~~~~ fun ass_up, args:"; val ((ys as (y,s,Script sc,d)), (is as (E,l,a,v,S,b),ss),
14.18 +"~~~~~ fun ass_up, args:"; val ((ys as (y,ctxt,s,Script sc,d)), (is as (E,l,a,v,S,b),ss),
14.19 (Const ("HOL.Let",_) $ _)) = (ys, ((E,up,a,v,S,b),ss), (go up sc));
14.20 val l = drop_last l; (*comes from e, goes to Abs*)
14.21 val (Const ("HOL.Let",_) $ e $ (Abs (i,T,body))) = go l sc;
15.1 --- a/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml Wed Mar 07 15:58:18 2012 +0100
15.2 +++ b/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml Sat Mar 10 14:38:18 2012 +0100
15.3 @@ -34,6 +34,7 @@
15.4 val ctxt = get_ctxt pt p;
15.5 val SOME t = parseNEW ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
15.6 get_loc pt p |> snd |> is_e_ctxt; (*false*)
15.7 +
15.8 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*);
15.9 get_ctxt pt p |> is_e_ctxt; (*false*)
15.10 val ctxt = get_ctxt pt p;
16.1 --- a/test/Tools/isac/Test_Isac.thy Wed Mar 07 15:58:18 2012 +0100
16.2 +++ b/test/Tools/isac/Test_Isac.thy Sat Mar 10 14:38:18 2012 +0100
16.3 @@ -22,7 +22,7 @@
16.4 "../../Pure/Isar/Test_Parsers"
16.5 (*"../../Pure/Isar/Pure/Isar/Struct_Deriv" update 2009-2-->2011*)
16.6 "../../Pure/Isar/Test_Parse_Term"
16.7 -
16.8 +
16.9 uses
16.10 ( "library.sml")
16.11 ( "calcelems.sml")
16.12 @@ -174,8 +174,8 @@
16.13 use "Knowledge/polyminus.sml" (*part.*)
16.14 use "Knowledge/vect.sml"
16.15 use "Knowledge/diffapp.sml" (*part.*)
16.16 - use "Knowledge/biegelinie.sml" (*part.*)
16.17 - use "Knowledge/algein.sml" (*part.*)
16.18 + use "Knowledge/biegelinie.sml"
16.19 + use "Knowledge/algein.sml"
16.20 use "Knowledge/diophanteq.sml"
16.21 use "Knowledge/isac.sml" (*part.*)
16.22 ML {*"%%%%%%%%%%%%%%%%% end Knowledge.thy %%%%%%%%%%%%%%%%%%%%";*}
17.1 --- a/test/Tools/isac/Test_Some.thy Wed Mar 07 15:58:18 2012 +0100
17.2 +++ b/test/Tools/isac/Test_Some.thy Sat Mar 10 14:38:18 2012 +0100
17.3 @@ -5,6 +5,8 @@
17.4
17.5 ML {*
17.6 *}
17.7 +ML {* (*==================*)
17.8 +*}
17.9 ML {*
17.10 *}
17.11 ML {*
17.12 @@ -18,17 +20,15 @@
17.13 ML {* (*==================*)
17.14 *}
17.15 ML {*
17.16 -*}
17.17 -ML {*
17.18 "~~~~~ fun , args:"; val () = ();
17.19 *}
17.20 end
17.21
17.22 -
17.23 -(*============ inhibit exn WN120201 ==============================================
17.24 -============ inhibit exn WN120201 ==============================================*)
17.25 -
17.26 +(*============ inhibit exn WN120309 ==============================================
17.27 +============ inhibit exn WN120309 ==============================================*)
17.28
17.29 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
17.30 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
17.31
17.32 +(*=========================^^^ correct until here ^^^===========================*)
17.33 +
18.1 --- a/test/Tools/isac/thms-survey-Isa02-Isa09-2.sml Wed Mar 07 15:58:18 2012 +0100
18.2 +++ b/test/Tools/isac/thms-survey-Isa02-Isa09-2.sml Sat Mar 10 14:38:18 2012 +0100
18.3 @@ -1,83 +1,90 @@
18.4 -WN110726 see ~/devel/isac/isac-10/isa2009-2/thms-replace-Isa02-Isa09-2.sml
18.5 - Isabelle2002-isac Isabelle2009-2
18.6 - ok
18.7 - \ to be checked
18.8 - \? still misterious
18.9 - # better would be the *_class.*(n)
18.10 - // no rule outside *_class.*(n)
18.11 -> rlsthmsNOTisac;
18.12 -val it =
18.13 - [("refl", "?t = ?t"), HOL.refl
18.14 - ("o_apply", "(?f o ?g) ?x = ?f (?g ?x)"), Fun.o_apply
18.15 - ("take_Nil", "take ?n [] = []"), List.take_Nil
18.16 - ("take_Cons", List.take_Cons
18.17 - "take ?n (?x # ?xs) =
18.18 - (case ?n of 0 => [] | Suc m => ?x # take m ?xs)"),
18.19 - ("if_True", "(if True then ?x else ?y) = ?x"), HOL.if_True
18.20 ------------------------------------------------------------------------------------------------------------------
18.21 - ("if_False", "(if False then ?x else ?y) = ?y"), HOL.if_False
18.22 - ("sym_real_mult_minus1", "- ?z1 = -1 * ?z1" [.]), \???
18.23 - ("real_add_mult_distrib", Rings.semiring_class.left_distrib
18.24 - "(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"),
18.25 - ("real_add_mult_distrib2", Rings.semiring_class.right_distrib
18.26 - "?w * (?z1.0 + ?z2.0) = ?w * ?z1.0 + ?w * ?z2.0"),
18.27 - ("sym_realpow_twoI", "?r1 * ?r1 = ?r1 ^^^ 2" [.]), !^!Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(29)
18.28 ------------------------------------------------------------------------------------------------------------------
18.29 - ("sym_realpow_addI", !^!Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(26)
18.30 - "?r1 ^^^ ?n1 * ?r1 ^^^ ?m1 = ?r1 ^^^ (?n1 + ?m1)" [.]),
18.31 - ("real_mult_1_right", "?z * 1 = ?z"), Groups.monoid_mult_class.mult_1_right
18.32 - ("sym_real_mult_2", "?z1 + ?z1 = 2 * ?z1" [.]), #!^! Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(4): ?m + ?m = ((1::?'a) + (1::?'a)) * ?m
18.33 - -''- //
18.34 - ("real_mult_1", "1 * ?z = ?z"), Groups.monoid_mult_class.mult_1_left
18.35 - ("real_mult_0", "0 * ?z = 0"), Rings.mult_zero_class.mult_zero_left
18.36 ------------------------------------------------------------------------------------------------------------------
18.37 - ("real_mult_0_right", "?z * 0 = 0"), Rings.mult_zero_class.mult_zero_right
18.38 - ("real_add_zero_left", "0 + ?z = ?z"), Groups.monoid_add_class.add_0_left
18.39 - ("real_add_zero_right", "?z + 0 = ?z"), Groups.monoid_add_class.add_0_right
18.40 - ("real_0_divide", "0 / ?x = 0"), Rings.division_ring_class.divide_zero_left
18.41 - ("sym_real_mult_assoc", # Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(18) + see sym_rmult_assoc
18.42 - -''- //
18.43 - "?z1.1 * (?z2.1 * ?z3.1) = ?z1.1 * ?z2.1 * ?z3.1" [.]),
18.44 ------------------------------------------------------------------------------------------------------------------
18.45 - ("le_refl", "?n <= ?n"), RealDef.real_le_refl
18.46 - ("real_minus_minus", "- (- ?z) = ?z"), Groups.group_add_class.minus_minus
18.47 - ("real_mult_commute", "?z * ?w = ?w * ?z"), RealDef.real_mult_commute
18.48 - ("real_mult_left_commute", # Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(19)
18.49 - "?z1.0 * (?z2.0 * ?z3.0) = ?z2.0 * (?z1.0 * ?z3.0)"),
18.50 - -''- //
18.51 - ("real_mult_assoc", "?z1.0 * ?z2.0 * ?z3.0 = ?z1.0 * (?z2.0 * ?z3.0)"), RealDef.real_mult_assoc
18.52 ------------------------------------------------------------------------------------------------------------------
18.53 - ("real_add_commute", "?z + ?w = ?w + ?z"), Groups.ab_semigroup_add_class.add_commute
18.54 - ("real_add_left_commute", "?x + (?y + ?z) = ?y + (?x + ?z)"), Groups.ab_semigroup_add_class.add_left_commute
18.55 - ("real_add_assoc", "?z1.0 + ?z2.0 + ?z3.0 = ?z1.0 + (?z2.0 + ?z3.0)"), Groups.semigroup_add_class.add_assoc
18.56 - ("sym_real_mult_minus_eq1", "- (?x1 * ?y1) = - ?x1 * ?y1" [.]), Rings.ring_class.minus_mult_left
18.57 - ("real_add_minus", "?z + - ?z = 0"), Groups.group_add_class.right_minus
18.58 ------------------------------------------------------------------------------------------------------------------
18.59 - ("sym_real_add_assoc", # Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(25) + see sym_radd_assoc
18.60 - "?z1.1 + (?z2.1 + ?z3.1) = ?z1.1 + ?z2.1 + ?z3.1" [.]),
18.61 - -''- //
18.62 - ("sym_real_minus_divide_eq", "- (?x1 / ?y1) = - ?x1 / ?y1" [.]), Rings.division_ring_class.minus_divide_left
18.63 - ("real_times_divide1_eq", "?x * (?y / ?z) = ?x * ?y / ?z"), # Fields.field_class.times_divide_eq(1)
18.64 - -''- ! Rings.division_ring_class.times_divide_eq_right
18.65 - ("real_times_divide2_eq", "?y / ?z * ?x = ?y * ?x / ?z"), Fields.field_class.times_divide_eq_left
18.66 - ("real_divide_divide2_eq", "?x / ?y / ?z = ?x / (?y * ?z)"), Fields.field_inverse_zero_class.divide_divide_eq_left
18.67 ------------------------------------------------------------------------------------------------------------------
18.68 - ("real_divide_divide1_eq", "?x / (?y / ?z) = ?x * ?z / ?y"), Fields.field_inverse_zero_class.divide_divide_eq_right
18.69 - ("real_divide_1", "?x / 1 = ?x"), Rings.division_ring_class.divide_1
18.70 - ("real_diff_mult_distrib", Rings.ring_class.left_diff_distrib
18.71 - "(?z1.0 - ?z2.0) * ?w = ?z1.0 * ?w - ?z2.0 * ?w"),
18.72 - ("real_diff_mult_distrib2", Rings.ring_class.right_diff_distrib
18.73 - "?w * (?z1.0 - ?z2.0) = ?w * ?z1.0 - ?w * ?z2.0"),
18.74 - ("real_add_divide_distrib", "(?x + ?y) / ?z = ?x / ?z + ?y / ?z"), Rings.division_ring_class.add_divide_distrib
18.75 ------------------------------------------------------------------------------------------------------------------
18.76 - ("sym_radd_assoc", "?m1 + (?n1 + ?k1) = ?m1 + ?n1 + ?k1" [.]), + see sym_real_add_assoc
18.77 - ("sym_rmult_assoc", "?m1 * (?n1 * ?k1) = ?m1 * ?n1 * ?k1" [.])] + see sym_real_mult_assoc
18.78 -: (thmID * Thm.thm) list
18.79 - "real_divide_minus1", "?x / -1 = - ?x" Int.divide_minus1
18.80 -
18.81 -find_theorems
18.82 -(999) name :
18.83 -(999) simp : "?a * (?b + ?c)"
18.84 -Tobias Nipkow 'searched for' ... "_ + _ + _ = _ + (_ + _)"
18.85 - "_ + (_ + (_::nat)) = _ + _ + _"
18.86 -
18.87 +WN110726 see ~/devel/isac/isac-10/isa2009-2/thms-replace-Isa02-Isa09-2.sml
18.88 + Isabelle2002-isac Isabelle2009-2
18.89 + ok
18.90 + \ to be checked
18.91 + \? still misterious
18.92 + # better would be the *_class.*(n)
18.93 + // no rule outside *_class.*(n)
18.94 +> rlsthmsNOTisac;
18.95 +val it =
18.96 + [("refl", "?t = ?t"), HOL.refl
18.97 + ("o_apply", "(?f o ?g) ?x = ?f (?g ?x)"), Fun.o_apply
18.98 + ("take_Nil", "take ?n [] = []"), List.take_Nil
18.99 + ("take_Cons", List.take_Cons
18.100 + "take ?n (?x # ?xs) =
18.101 + (case ?n of 0 => [] | Suc m => ?x # take m ?xs)"),
18.102 + ("if_True", "(if True then ?x else ?y) = ?x"), HOL.if_True
18.103 +-----------------------------------------------------------------------------------------------------------------
18.104 + ("if_False", "(if False then ?x else ?y) = ?y"), HOL.if_False
18.105 + ("sym_real_mult_minus1", "- ?z1 = -1 * ?z1" [.]), \???
18.106 + ("real_add_mult_distrib", Rings.semiring_class.left_distrib
18.107 + "(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"),
18.108 + ("real_add_mult_distrib2", Rings.semiring_class.right_distrib
18.109 + "?w * (?z1.0 + ?z2.0) = ?w * ?z1.0 + ?w * ?z2.0"),
18.110 + ("sym_realpow_twoI", "?r1 * ?r1 = ?r1 ^^^ 2" [.]), !^!Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(29)
18.111 +-----------------------------------------------------------------------------------------------------------------
18.112 + ("sym_realpow_addI", !^!Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(26)
18.113 + "?r1 ^^^ ?n1 * ?r1 ^^^ ?m1 = ?r1 ^^^ (?n1 + ?m1)" [.]),
18.114 + ("real_mult_1_right", "?z * 1 = ?z"), Groups.monoid_mult_class.mult_1_right
18.115 + ("sym_real_mult_2", "?z1 + ?z1 = 2 * ?z1" [.]), #!^! Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(4): ?m + ?m = ((1::?'a) + (1::?'a)) * ?m
18.116 + -''- //
18.117 + ("real_mult_1", "1 * ?z = ?z"), Groups.monoid_mult_class.mult_1_left
18.118 + ("real_mult_0", "0 * ?z = 0"), Rings.mult_zero_class.mult_zero_left
18.119 +-----------------------------------------------------------------------------------------------------------------
18.120 + ("real_mult_0_right", "?z * 0 = 0"), Rings.mult_zero_class.mult_zero_right
18.121 + ("real_add_zero_left", "0 + ?z = ?z"), Groups.monoid_add_class.add_0_left
18.122 + ("real_add_zero_right", "?z + 0 = ?z"), Groups.monoid_add_class.add_0_right
18.123 + ("real_0_divide", "0 / ?x = 0"), Rings.division_ring_class.divide_zero_left
18.124 + ("sym_real_mult_assoc", # Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(18) + see sym_rmult_assoc
18.125 + -''- //
18.126 + "?z1.1 * (?z2.1 * ?z3.1) = ?z1.1 * ?z2.1 * ?z3.1" [.]),
18.127 +-----------------------------------------------------------------------------------------------------------------
18.128 + ("le_refl", "?n <= ?n"), RealDef.real_le_refl
18.129 + ("real_minus_minus", "- (- ?z) = ?z"), Groups.group_add_class.minus_minus
18.130 + ("real_mult_commute", "?z * ?w = ?w * ?z"), RealDef.real_mult_commute
18.131 + ("real_mult_left_commute", # Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(19)
18.132 + "?z1.0 * (?z2.0 * ?z3.0) = ?z2.0 * (?z1.0 * ?z3.0)"),
18.133 + -''- //
18.134 + ("real_mult_assoc", "?z1.0 * ?z2.0 * ?z3.0 = ?z1.0 * (?z2.0 * ?z3.0)"), RealDef.real_mult_assoc
18.135 +-----------------------------------------------------------------------------------------------------------------
18.136 + ("real_add_commute", "?z + ?w = ?w + ?z"), Groups.ab_semigroup_add_class.add_commute
18.137 + ("real_add_left_commute", "?x + (?y + ?z) = ?y + (?x + ?z)"), Groups.ab_semigroup_add_class.add_left_commute
18.138 + ("real_add_assoc", "?z1.0 + ?z2.0 + ?z3.0 = ?z1.0 + (?z2.0 + ?z3.0)"), Groups.semigroup_add_class.add_assoc
18.139 + ("sym_real_mult_minus_eq1", "- (?x1 * ?y1) = - ?x1 * ?y1" [.]), Rings.ring_class.minus_mult_left
18.140 + ("real_add_minus", "?z + - ?z = 0"), Groups.group_add_class.right_minus
18.141 +-----------------------------------------------------------------------------------------------------------------
18.142 + ("sym_real_add_assoc", # Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(25) + see sym_radd_assoc
18.143 + "?z1.1 + (?z2.1 + ?z3.1) = ?z1.1 + ?z2.1 + ?z3.1" [.]),
18.144 + -''- //
18.145 + ("sym_real_minus_divide_eq", "- (?x1 / ?y1) = - ?x1 / ?y1" [.]), Rings.division_ring_class.minus_divide_left
18.146 + ("real_times_divide1_eq", "?x * (?y / ?z) = ?x * ?y / ?z"), # Fields.field_class.times_divide_eq(1)
18.147 + -''- ! Rings.division_ring_class.times_divide_eq_right
18.148 + ("real_times_divide2_eq", "?y / ?z * ?x = ?y * ?x / ?z"), Fields.field_class.times_divide_eq_left
18.149 + ("real_divide_divide2_eq", "?x / ?y / ?z = ?x / (?y * ?z)"), Fields.field_inverse_zero_class.divide_divide_eq_left
18.150 +-----------------------------------------------------------------------------------------------------------------
18.151 + ("real_divide_divide1_eq", "?x / (?y / ?z) = ?x * ?z / ?y"), Fields.field_inverse_zero_class.divide_divide_eq_right
18.152 + ("real_divide_1", "?x / 1 = ?x"), Rings.division_ring_class.divide_1
18.153 + ("real_diff_mult_distrib", Rings.ring_class.left_diff_distrib
18.154 + "(?z1.0 - ?z2.0) * ?w = ?z1.0 * ?w - ?z2.0 * ?w"),
18.155 + ("real_diff_mult_distrib2", Rings.ring_class.right_diff_distrib
18.156 + "?w * (?z1.0 - ?z2.0) = ?w * ?z1.0 - ?w * ?z2.0"),
18.157 + ("real_add_divide_distrib", "(?x + ?y) / ?z = ?x / ?z + ?y / ?z"), Rings.division_ring_class.add_divide_distrib
18.158 +-----------------------------------------------------------------------------------------------------------------
18.159 + ("sym_radd_assoc", "?m1 + (?n1 + ?k1) = ?m1 + ?n1 + ?k1" [.]), + see sym_real_add_assoc
18.160 + ("sym_rmult_assoc", "?m1 * (?n1 * ?k1) = ?m1 * ?n1 * ?k1" [.])] + see sym_real_mult_assoc
18.161 +: (thmID * Thm.thm) list
18.162 + "real_divide_minus1", "?x / -1 = - ?x" Int.divide_minus1
18.163 + "real_minus_eq_cancel", "(- ?a = - ?b) = (?a = ?b)" Groups.group_add_class.neg_equal_iff_equal:
18.164 +
18.165 +-----------------------------------------------------------------------------------------------------------------
18.166 +find_theorems: in emacs
18.167 +(999) name :
18.168 +(999) simp : "?a * (?b + ?c)"
18.169 +Tobias Nipkow 'searched for' ... "_ + _ + _ = _ + (_ + _)"
18.170 + "_ + (_ + (_::nat)) = _ + _ + _"
18.171 +
18.172 +
18.173 +-----------------------------------------------------------------------------------------------------------------
18.174 +list funs:
18.175 +nth_Cons_ NTH_CONS
18.176 +nth_Nil_ NTH_NIL