ad 967c8a1eb6b1 (7): remove all code concerned with 'mets = Unsynchronized.ref'
1.1 --- a/src/Tools/isac/Interpret/ptyps.sml Sun Feb 02 02:45:11 2014 +0100
1.2 +++ b/src/Tools/isac/Interpret/ptyps.sml Sun Feb 02 03:09:40 2014 +0100
1.3 @@ -382,13 +382,6 @@
1.4 val it = ["linear", "univariate", "equation"] : string list*)
1.5
1.6
1.7 -
1.8 -(*.the metID has the root-element as first.*)
1.9 -fun store_met (met as {guh,...}, metID) =
1.10 - (if (!check_guhs_unique) then check_metguh_unique guh (!mets) else ();
1.11 - mets:= insrt metID met metID (!mets));
1.12 -
1.13 -
1.14 (*. prepare problem-types before storing in pbltypes;
1.15 dont forget to 'check_guh_unique' before ins.*)
1.16 fun prep_pbt thy guh maa init
2.1 --- a/src/Tools/isac/Knowledge/AlgEin.thy Sun Feb 02 02:45:11 2014 +0100
2.2 +++ b/src/Tools/isac/Knowledge/AlgEin.thy Sun Feb 02 03:09:40 2014 +0100
2.3 @@ -35,100 +35,6 @@
2.4 ("#Find", ["GesamtLaenge l_l"])],
2.5 e_rls, NONE, [["Berechnung","erstNumerisch"], ["Berechnung","erstSymbolisch"]]))]; *}
2.6
2.7 -ML {*
2.8 -(** methods **)
2.9 -
2.10 -store_met
2.11 - (prep_met thy "met_algein" [] e_metID
2.12 - (["Berechnung"],
2.13 - [],
2.14 - {rew_ord'="tless_true", rls'= Erls, calc = [],
2.15 - srls = Erls, prls = Erls,
2.16 - crls =Erls , errpats = [], nrls = Erls},
2.17 -"empty_script"
2.18 -));
2.19 -
2.20 -store_met
2.21 - (prep_met thy "met_algein_numsym" [] e_metID
2.22 - (["Berechnung","erstNumerisch"],
2.23 - [],
2.24 - {rew_ord'="tless_true", rls'= Erls, calc = [],
2.25 - srls = Erls, prls = Erls,
2.26 - crls =Erls , errpats = [], nrls = Erls},
2.27 -"empty_script"
2.28 -));
2.29 -
2.30 -*}
2.31 -ML {*
2.32 -store_met
2.33 - (prep_met thy "met_algein_numsym" [] e_metID
2.34 - (["Berechnung","erstNumerisch"],
2.35 - [("#Given" ,["KantenLaenge k_k","Querschnitt q__q",
2.36 - "KantenUnten u_u", "KantenSenkrecht s_s",
2.37 - "KantenOben o_o"]),
2.38 - ("#Find" ,["GesamtLaenge l_l"])
2.39 - ],
2.40 - {rew_ord'="tless_true", rls'= e_rls, calc = [],
2.41 - srls = append_rls "srls_..Berechnung-erstSymbolisch" e_rls
2.42 - [Calc ("Atools.boollist2sum",
2.43 - eval_boollist2sum "")],
2.44 - prls = e_rls, crls =e_rls , errpats = [], nrls = norm_Rational},
2.45 -"Script RechnenSymbolScript (k_k::bool) (q__q::bool) " ^
2.46 -"(u_u::bool list) (s_s::bool list) (o_o::bool list) (l_l::real) =" ^
2.47 -" (let t_t = Take (l_l = oben + senkrecht + unten); " ^
2.48 -" su_m = boollist2sum o_o; " ^
2.49 -" t_t = Substitute [oben = su_m] t_t; " ^
2.50 -" t_t = Substitute o_o t_t; " ^
2.51 -" t_t = Substitute [k_k, q__q] t_t; " ^
2.52 -" t_t = (Repeat (Try (Rewrite_Set norm_Poly False))) t_t; " ^
2.53 -" su_m = boollist2sum s_s; " ^
2.54 -" t_t = Substitute [senkrecht = su_m] t_t; " ^
2.55 -" t_t = Substitute s_s t_t; " ^
2.56 -" t_t = Substitute [k_k, q__q] t_t; " ^
2.57 -" t_t = (Repeat (Try (Rewrite_Set norm_Poly False))) t_t; " ^
2.58 -" su_m = boollist2sum u_u; " ^
2.59 -" t_t = Substitute [unten = su_m] t_t; " ^
2.60 -" t_t = Substitute u_u t_t; " ^
2.61 -" t_t = Substitute [k_k, q__q] t_t; " ^
2.62 -" t_t = (Repeat (Try (Rewrite_Set norm_Poly False))) t_t " ^
2.63 -" in (Try (Rewrite_Set norm_Poly False)) t_t) "
2.64 -));
2.65 -
2.66 -*}
2.67 -ML {*
2.68 -store_met
2.69 - (prep_met thy "met_algein_symnum" [] e_metID
2.70 - (["Berechnung","erstSymbolisch"],
2.71 - [("#Given" ,["KantenLaenge k_k","Querschnitt q__q",
2.72 - "KantenUnten u_u", "KantenSenkrecht s_s",
2.73 - "KantenOben o_o"]),
2.74 - ("#Find" ,["GesamtLaenge l_l"])
2.75 - ],
2.76 - {rew_ord'="tless_true", rls'= e_rls, calc = [],
2.77 - srls = append_rls "srls_..Berechnung-erstSymbolisch" e_rls
2.78 - [Calc ("Atools.boollist2sum",
2.79 - eval_boollist2sum "")],
2.80 - prls = e_rls,
2.81 - crls =e_rls , errpats = [], nrls = norm_Rational},
2.82 -"Script RechnenSymbolScript (k_k::bool) (q__q::bool) " ^
2.83 -"(u_u::bool list) (s_s::bool list) (o_o::bool list) (l_l::real) =" ^
2.84 -" (let t_t = Take (l_l = oben + senkrecht + unten); " ^
2.85 -" su_m = boollist2sum o_o; " ^
2.86 -" t_t = Substitute [oben = su_m] t_t; " ^
2.87 -" t_t = Substitute o_o t_t; " ^
2.88 -" t_t = (Repeat (Try (Rewrite_Set norm_Poly False))) t_t; " ^
2.89 -" su_m = boollist2sum s_s; " ^
2.90 -" t_t = Substitute [senkrecht = su_m] t_t; " ^
2.91 -" t_t = Substitute s_s t_t; " ^
2.92 -" t_t = (Repeat (Try (Rewrite_Set norm_Poly False))) t_t; " ^
2.93 -" su_m = boollist2sum u_u; " ^
2.94 -" t_t = Substitute [unten = su_m] t_t; " ^
2.95 -" t_t = Substitute u_u t_t; " ^
2.96 -" t_t = (Repeat (Try (Rewrite_Set norm_Poly False))) t_t; " ^
2.97 -" t_t = Substitute [k_k, q__q] t_t " ^
2.98 -" in (Try (Rewrite_Set norm_Poly False)) t_t) "
2.99 -));
2.100 -*}
2.101 setup {* KEStore_Elems.add_mets
2.102 [prep_met thy "met_algein" [] e_metID
2.103 (["Berechnung"], [],
3.1 --- a/src/Tools/isac/Knowledge/Biegelinie.thy Sun Feb 02 02:45:11 2014 +0100
3.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy Sun Feb 02 03:09:40 2014 +0100
3.3 @@ -188,307 +188,6 @@
3.4 scr = EmptyScr};
3.5 *}
3.6
3.7 -ML {*
3.8 -store_met
3.9 - (prep_met thy "met_biege" [] e_metID
3.10 - (["IntegrierenUndKonstanteBestimmen"],
3.11 - [("#Given" ,["Traegerlaenge l_l", "Streckenlast q__q", "FunktionsVariable v_v"]),
3.12 - (*("#Where",["0 < l_l"]), ...wait for < and handling Arbfix*)
3.13 - ("#Find" ,["Biegelinie b_b"]),
3.14 - ("#Relate",["RandbedingungenBiegung r_b", "RandbedingungenMoment r_m"])],
3.15 - {rew_ord'="tless_true",
3.16 - rls' = append_rls "erls_IntegrierenUndK.." e_rls
3.17 - [Calc ("Atools.ident",eval_ident "#ident_"),
3.18 - Thm ("not_true",num_str @{thm not_true}),
3.19 - Thm ("not_false",num_str @{thm not_false})],
3.20 - calc = [], srls = srls, prls = Erls, crls = Atools_erls, errpats = [], nrls = Erls},
3.21 -"Script BiegelinieScript " ^
3.22 -"(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) " ^
3.23 -"(r_b::bool list) (r_m::bool list) = " ^
3.24 -" (let q___q = Take (qq v_v = q__q); " ^
3.25 -" q___q = ((Rewrite sym_neg_equal_iff_equal True) @@ " ^
3.26 -" (Rewrite Belastung_Querkraft True)) q___q; " ^
3.27 -" (Q__Q:: bool) = " ^
3.28 -" (SubProblem (Biegelinie',[named,integrate,function], " ^
3.29 -" [diff,integration,named]) " ^
3.30 -" [REAL (rhs q___q), REAL v_v, REAL_REAL Q]); " ^
3.31 -" Q__Q = Rewrite Querkraft_Moment True Q__Q; " ^
3.32 -" (M__M::bool) = " ^
3.33 -" (SubProblem (Biegelinie',[named,integrate,function], " ^
3.34 -" [diff,integration,named]) " ^
3.35 -" [REAL (rhs Q__Q), REAL v_v, REAL_REAL M_b]); " ^
3.36 - (*([5], Res), M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2*)
3.37 -" e__1 = NTH 1 r_m; " ^
3.38 -" (x__1::real) = argument_in (lhs e__1); " ^
3.39 -" (M__1::bool) = (Substitute [v_v = x__1]) M__M; " ^
3.40 - (*([6], Res), M_b 0 = c_2 + c * 0 + -1 * q_0 / 2 * 0 ^^^ 2*)
3.41 -" M__1 = (Substitute [e__1]) M__1; " ^
3.42 - (*([7], Res), 0 = c_2 + c * 0 + -1 * q_0 / 2 * 0 ^^^ 2*)
3.43 -" M__2 = Take M__M; " ^
3.44 - (*([8], Frm), M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2*)
3.45 -(*without above Take 'Substitute [v_v = x__2]' takes _last formula from ctree_*)
3.46 -" e__2 = NTH 2 r_m; " ^
3.47 -" (x__2::real) = argument_in (lhs e__2); " ^
3.48 -" (M__2::bool) = (Substitute [v_v = x__2]) M__M; " ^
3.49 - (*([8], Res), M_b L = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2*)
3.50 -" M__2 = (Substitute [e__2]) M__2; " ^
3.51 - (**)
3.52 -" (c_1_2::bool list) = " ^
3.53 -" (SubProblem (Biegelinie',[LINEAR,system],[no_met]) " ^
3.54 -" [BOOL_LIST [M__1, M__2], REAL_LIST [c,c_2]]); " ^
3.55 -" M__M = Take M__M; " ^
3.56 -" M__M = ((Substitute c_1_2) @@ " ^
3.57 -" (Try (Rewrite_Set_Inst [(bdv_1, c),(bdv_2, c_2)] " ^
3.58 -" simplify_System False)) @@ " ^
3.59 -" (Rewrite Moment_Neigung False) @@ " ^
3.60 -" (Rewrite make_fun_explicit False)) M__M; " ^
3.61 -(*----------------------- and the same once more ------------------------*)
3.62 -" (N__N:: bool) = " ^
3.63 -" (SubProblem (Biegelinie',[named,integrate,function], " ^
3.64 -" [diff,integration,named]) " ^
3.65 -" [REAL (rhs M__M), REAL v_v, REAL_REAL y']); " ^
3.66 -" (B__B:: bool) = " ^
3.67 -" (SubProblem (Biegelinie',[named,integrate,function], " ^
3.68 -" [diff,integration,named]) " ^
3.69 -" [REAL (rhs N__N), REAL v_v, REAL_REAL y]); " ^
3.70 -" e__1 = NTH 1 r_b; " ^
3.71 -" (x__1::real) = argument_in (lhs e__1); " ^
3.72 -" (B__1::bool) = (Substitute [v_v = x__1]) B__B; " ^
3.73 -" B__1 = (Substitute [e__1]) B__1 ; " ^
3.74 -" B__2 = Take B__B; " ^
3.75 -" e__2 = NTH 2 r_b; " ^
3.76 -" (x__2::real) = argument_in (lhs e__2); " ^
3.77 -" (B__2::bool) = (Substitute [v_v = x__2]) B__B; " ^
3.78 -" B__2 = (Substitute [e__2]) B__2 ; " ^
3.79 -" (c_1_2::bool list) = " ^
3.80 -" (SubProblem (Biegelinie',[LINEAR,system],[no_met]) " ^
3.81 -" [BOOL_LIST [B__1, B__2], REAL_LIST [c,c_2]]); " ^
3.82 -" B__B = Take B__B; " ^
3.83 -" B__B = ((Substitute c_1_2) @@ " ^
3.84 -" (Rewrite_Set_Inst [(bdv, x)] make_ratpoly_in False)) B__B " ^
3.85 -" in B__B)"
3.86 -));
3.87 -*}
3.88 -ML {*
3.89 -store_met
3.90 - (prep_met thy "met_biege_2" [] e_metID
3.91 - (["IntegrierenUndKonstanteBestimmen2"],
3.92 - [("#Given" ,["Traegerlaenge l_l", "Streckenlast q__q", "FunktionsVariable v_v"]),
3.93 - (*("#Where",["0 < l_l"]), ...wait for < and handling Arbfix*)
3.94 - ("#Find" ,["Biegelinie b_b"]),
3.95 - ("#Relate",["Randbedingungen r_b"])],
3.96 - {rew_ord'="tless_true",
3.97 - rls' = append_rls "erls_IntegrierenUndK.." e_rls
3.98 - [Calc ("Atools.ident",eval_ident "#ident_"),
3.99 - Thm ("not_true",num_str @{thm not_true}),
3.100 - Thm ("not_false",num_str @{thm not_false})],
3.101 - calc = [],
3.102 - srls = append_rls "erls_IntegrierenUndK.." e_rls
3.103 - [Calc("Tools.rhs", eval_rhs"eval_rhs_"),
3.104 - Calc ("Atools.ident",eval_ident "#ident_"),
3.105 - Thm ("last_thmI",num_str @{thm last_thmI}),
3.106 - Thm ("if_True",num_str @{thm if_True}),
3.107 - Thm ("if_False",num_str @{thm if_False})],
3.108 - prls = Erls, crls = Atools_erls, errpats = [], nrls = Erls},
3.109 -"Script Biegelinie2Script " ^
3.110 -"(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) (r_b::bool list) = " ^
3.111 -" (let " ^
3.112 -" (fun_s:: bool list) = " ^
3.113 -" (SubProblem (Biegelinie',[vonBelastungZu,Biegelinien], " ^
3.114 -" [Biegelinien,ausBelastung]) " ^
3.115 -" [REAL q__q, REAL v_v]); " ^
3.116 -" (equ_s::bool list) = " ^
3.117 -" (SubProblem (Biegelinie',[setzeRandbedingungen,Biegelinien], " ^
3.118 -" [Biegelinien,setzeRandbedingungenEin]) " ^
3.119 -" [BOOL_LIST fun_s, BOOL_LIST r_b]); " ^
3.120 -" (con_s::bool list) = " ^
3.121 -" (SubProblem (Biegelinie',[LINEAR,system],[no_met]) " ^
3.122 -" [BOOL_LIST equ_s, REAL_LIST [c,c_2,c_3,c_4]]); " ^
3.123 -" B_B = Take (lastI fun_s); " ^
3.124 -" B_B = ((Substitute con_s) @@ " ^
3.125 -" (Rewrite_Set_Inst [(bdv, v_v)] make_ratpoly_in False)) B_B " ^
3.126 -" in B_B)"
3.127 -));
3.128 -
3.129 -*}
3.130 -ML {*
3.131 -store_met
3.132 - (prep_met thy "met_biege_intconst_2" [] e_metID
3.133 - (["IntegrierenUndKonstanteBestimmen","2xIntegrieren"],
3.134 - [],
3.135 - {rew_ord'="tless_true", rls'=Erls, calc = [],
3.136 - srls = e_rls,
3.137 - prls=e_rls,
3.138 - crls = Atools_erls, errpats = [], nrls = e_rls},
3.139 -"empty_script"
3.140 -));
3.141 -
3.142 -store_met
3.143 - (prep_met thy "met_biege_intconst_4" [] e_metID
3.144 - (["IntegrierenUndKonstanteBestimmen","4x4System"],
3.145 - [],
3.146 - {rew_ord'="tless_true", rls'=Erls, calc = [],
3.147 - srls = e_rls,
3.148 - prls=e_rls,
3.149 - crls = Atools_erls, errpats = [], nrls = e_rls},
3.150 -"empty_script"
3.151 -));
3.152 -
3.153 -store_met
3.154 - (prep_met thy "met_biege_intconst_1" [] e_metID
3.155 - (["IntegrierenUndKonstanteBestimmen","1xIntegrieren"],
3.156 - [],
3.157 - {rew_ord'="tless_true", rls'=Erls, calc = [],
3.158 - srls = e_rls,
3.159 - prls=e_rls,
3.160 - crls = Atools_erls, errpats = [], nrls = e_rls},
3.161 -"empty_script"
3.162 -));
3.163 -
3.164 -store_met
3.165 - (prep_met thy "met_biege2" [] e_metID
3.166 - (["Biegelinien"],
3.167 - [],
3.168 - {rew_ord'="tless_true", rls'=Erls, calc = [],
3.169 - srls = e_rls,
3.170 - prls=e_rls,
3.171 - crls = Atools_erls, errpats = [], nrls = e_rls},
3.172 -"empty_script"
3.173 -));
3.174 -
3.175 -*}
3.176 -ML {*
3.177 -store_met
3.178 - (prep_met thy "met_biege_ausbelast" [] e_metID
3.179 - (["Biegelinien", "ausBelastung"],
3.180 - [("#Given" ,["Streckenlast q__q", "FunktionsVariable v_v"]),
3.181 - ("#Find" ,["Funktionen fun_s"])],
3.182 - {rew_ord'="tless_true",
3.183 - rls' = append_rls "erls_ausBelastung" e_rls
3.184 - [Calc ("Atools.ident", eval_ident "#ident_"),
3.185 - Thm ("not_true", num_str @{thm not_true}),
3.186 - Thm ("not_false", num_str @{thm not_false})],
3.187 - calc = [],
3.188 - srls = append_rls "srls_ausBelastung" e_rls
3.189 - [Calc ("Tools.rhs", eval_rhs "eval_rhs_")],
3.190 - prls = e_rls, crls = Atools_erls, errpats = [], nrls = e_rls},
3.191 -"Script Belastung2BiegelScript (q__q::real) (v_v::real) = " ^
3.192 -" (let q___q = Take (qq v_v = q__q); " ^
3.193 -" q___q = ((Rewrite sym_neg_equal_iff_equal True) @@ " ^
3.194 -" (Rewrite Belastung_Querkraft True)) q___q; " ^
3.195 -" (Q__Q:: bool) = " ^
3.196 -" (SubProblem (Biegelinie',[named,integrate,function], " ^
3.197 -" [diff,integration,named]) " ^
3.198 -" [REAL (rhs q___q), REAL v_v, REAL_REAL Q]); " ^
3.199 -" M__M = Rewrite Querkraft_Moment True Q__Q; " ^
3.200 -" (M__M::bool) = " ^
3.201 -" (SubProblem (Biegelinie',[named,integrate,function], " ^
3.202 -" [diff,integration,named]) " ^
3.203 -" [REAL (rhs M__M), REAL v_v, REAL_REAL M_b]); " ^
3.204 -" N__N = ((Rewrite Moment_Neigung False) @@ " ^
3.205 -" (Rewrite make_fun_explicit False)) M__M; " ^
3.206 -" (N__N:: bool) = " ^
3.207 -" (SubProblem (Biegelinie',[named,integrate,function], " ^
3.208 -" [diff,integration,named]) " ^
3.209 -" [REAL (rhs N__N), REAL v_v, REAL_REAL y']); " ^
3.210 -" (B__B:: bool) = " ^
3.211 -" (SubProblem (Biegelinie',[named,integrate,function], " ^
3.212 -" [diff,integration,named]) " ^
3.213 -" [REAL (rhs N__N), REAL v_v, REAL_REAL y]) " ^
3.214 -" in [Q__Q, M__M, N__N, B__B])"
3.215 -));
3.216 -
3.217 -*}
3.218 -ML {*
3.219 -store_met
3.220 - (prep_met thy "met_biege_setzrand" [] e_metID
3.221 - (["Biegelinien", "setzeRandbedingungenEin"],
3.222 - [("#Given" , ["Funktionen fun_s", "Randbedingungen r_b"]),
3.223 - ("#Find" , ["Gleichungen equs'''"])],
3.224 - {rew_ord'="tless_true", rls'=Erls, calc = [],
3.225 - srls = srls2,
3.226 - prls=e_rls,
3.227 - crls = Atools_erls, errpats = [], nrls = e_rls},
3.228 -"Script SetzeRandbedScript (fun_s::bool list) (r_b::bool list) = " ^
3.229 -" (let b_1 = NTH 1 r_b; " ^
3.230 -" f_s = filter_sameFunId (lhs b_1) fun_s; " ^
3.231 -" (e_1::bool) = " ^
3.232 -" (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
3.233 -" [Equation,fromFunction]) " ^
3.234 -" [BOOL (hd f_s), BOOL b_1]); " ^
3.235 -" b_2 = NTH 2 r_b; " ^
3.236 -" f_s = filter_sameFunId (lhs b_2) fun_s; " ^
3.237 -" (e_2::bool) = " ^
3.238 -" (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
3.239 -" [Equation,fromFunction]) " ^
3.240 -" [BOOL (hd f_s), BOOL b_2]); " ^
3.241 -" b_3 = NTH 3 r_b; " ^
3.242 -" f_s = filter_sameFunId (lhs b_3) fun_s; " ^
3.243 -" (e_3::bool) = " ^
3.244 -" (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
3.245 -" [Equation,fromFunction]) " ^
3.246 -" [BOOL (hd f_s), BOOL b_3]); " ^
3.247 -" b_4 = NTH 4 r_b; " ^
3.248 -" f_s = filter_sameFunId (lhs b_4) fun_s; " ^
3.249 -" (e_4::bool) = " ^
3.250 -" (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
3.251 -" [Equation,fromFunction]) " ^
3.252 -" [BOOL (hd f_s), BOOL b_4]) " ^
3.253 -" in [e_1, e_2, e_3, e_4])"
3.254 -(* filter requires more than 1 sec !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
3.255 -"Script SetzeRandbedScript (fun_s::bool list) (r_b::bool list) = " ^
3.256 -" (let b_1 = NTH 1 r_b; " ^
3.257 -" f_s = filter (sameFunId (lhs b_1)) fun_s; " ^
3.258 -" (e_1::bool) = " ^
3.259 -" (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
3.260 -" [Equation,fromFunction]) " ^
3.261 -" [BOOL (hd f_s), BOOL b_1]); " ^
3.262 -" b_2 = NTH 2 r_b; " ^
3.263 -" f_s = filter (sameFunId (lhs b_2)) fun_s; " ^
3.264 -" (e_2::bool) = " ^
3.265 -" (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
3.266 -" [Equation,fromFunction]) " ^
3.267 -" [BOOL (hd f_s), BOOL b_2]); " ^
3.268 -" b_3 = NTH 3 r_b; " ^
3.269 -" f_s = filter (sameFunId (lhs b_3)) fun_s; " ^
3.270 -" (e_3::bool) = " ^
3.271 -" (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
3.272 -" [Equation,fromFunction]) " ^
3.273 -" [BOOL (hd f_s), BOOL b_3]); " ^
3.274 -" b_4 = NTH 4 r_b; " ^
3.275 -" f_s = filter (sameFunId (lhs b_4)) fun_s; " ^
3.276 -" (e_4::bool) = " ^
3.277 -" (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
3.278 -" [Equation,fromFunction]) " ^
3.279 -" [BOOL (hd f_s), BOOL b_4]) " ^
3.280 -" in [e_1,e_2,e_3,e_4])"*)
3.281 -));
3.282 -
3.283 -*}
3.284 -ML {*
3.285 -store_met
3.286 - (prep_met thy "met_equ_fromfun" [] e_metID
3.287 - (["Equation","fromFunction"],
3.288 - [("#Given" ,["functionEq fu_n","substitution su_b"]),
3.289 - ("#Find" ,["equality equ'''"])],
3.290 - {rew_ord'="tless_true", rls'=Erls, calc = [],
3.291 - srls = append_rls "srls_in_EquationfromFunc" e_rls
3.292 - [Calc("Tools.lhs", eval_lhs"eval_lhs_"),
3.293 - Calc("Atools.argument'_in", eval_argument_in "Atools.argument'_in")],
3.294 - prls=e_rls, crls = Atools_erls, errpats = [], nrls = e_rls},
3.295 -(*(M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2) (M_b L = 0) -->
3.296 - 0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2*)
3.297 -"Script Function2Equality (fu_n::bool) (su_b::bool) =" ^
3.298 -" (let fu_n = Take fu_n; " ^
3.299 -" bd_v = argument_in (lhs fu_n); " ^
3.300 -" va_l = argument_in (lhs su_b); " ^
3.301 -" eq_u = (Substitute [bd_v = va_l]) fu_n; " ^
3.302 - (*([1], Res), M_b L = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2*)
3.303 -" eq_u = (Substitute [su_b]) eq_u " ^
3.304 -" in (Rewrite_Set norm_Rational False) eq_u) "
3.305 -));
3.306 -*}
3.307 -
3.308 setup {* KEStore_Elems.add_mets
3.309 [prep_met thy "met_biege" [] e_metID
3.310 (["IntegrierenUndKonstanteBestimmen"],
4.1 --- a/src/Tools/isac/Knowledge/Build_Thydata.thy Sun Feb 02 02:45:11 2014 +0100
4.2 +++ b/src/Tools/isac/Knowledge/Build_Thydata.thy Sun Feb 02 03:09:40 2014 +0100
4.3 @@ -9,7 +9,7 @@
4.4 text {* This theory collects data of theorems and axioms defined and used in ISAC *}
4.5
4.6 ML {*
4.7 - writeln ("======= length (KEStore_Elems = " ^
4.8 + (*writeln ("======= length (KEStore_Elems = " ^
4.9 (KEStore_Elems.get_mets @{theory} |> count_kestore_ptyps |> string_of_int));
4.10 writeln ("======= length (! mets) = " ^
4.11 (count_kestore_ptyps (! mets) |> string_of_int));
4.12 @@ -30,7 +30,7 @@
4.13 writeln "\n\n======= ! mets ordered =======";
4.14 ! mets |> sort_kestore_met |> sort ptyp_ord
4.15 |> map check_kestore_met |> enumerate_strings |> sort string_ord |> map writeln;
4.16 - writeln "======= end ! mets =======";
4.17 + writeln "======= end ! mets =======";*)
4.18 *}
4.19
4.20 ML {*
4.21 @@ -170,17 +170,6 @@
4.22 ["Isabelle2011-->12"];
4.23 (*\========= inhibit exn WN130620 (1.4.1) below: fill thehier ==============/*)
4.24 *}
4.25 -ML {*
4.26 -insert_errpats ["diff","differentiate_on_R"]
4.27 - ([("chain-rule-diff-both",
4.28 - [parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)",
4.29 - parse_patt @{theory Diff} "d_d ?bdv (cos ?u) = - sin (d_d ?bdv ?u)",
4.30 - parse_patt @{theory Diff} "d_d ?bdv (?u ^^^ ?n) = ?n * ?u ^^^ (?n - 1)",
4.31 - parse_patt @{theory Diff} "d_d ?bdv (LogExp.ln ?u) = 1 / ?u",
4.32 - parse_patt @{theory Diff} "d_d ?bdv (LogExp.ln ?u) = 1 / d_d ?bdv ?u"],
4.33 - [@{thm diff_sin_chain}, @{thm diff_cos_chain}, @{thm diff_pow_chain},
4.34 - @{thm diff_ln_chain}, @{thm diff_exp_chain}])]: errpat list);
4.35 -*}
4.36 setup {* KEStore_Elems.add_mets
4.37 [update_metpair ["diff","differentiate_on_R"]
4.38 [("chain-rule-diff-both",
4.39 @@ -205,17 +194,6 @@
4.40 parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = cos ?u * _", "chain-rule-diff-both"),
4.41 ("fill-all",
4.42 parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = _", "chain-rule-diff-both")]: fillpat list);
4.43 -
4.44 -insert_errpats ["simplification","of_rationals"]
4.45 - ([("addition-of-fractions",
4.46 - [parse_patt @{theory Rational} "(?a / ?b + ?c / ?d) = (?a + ?c)/(?b + ?d)",
4.47 - parse_patt @{theory Rational} "(?a / ?b + ?c / ?d) = (?a + ?c)/(?b * ?d)",
4.48 - parse_patt @{theory Rational} "(?a / ?b + ?c / ?d) = (?c * ?a)/(?d * ?b)",
4.49 - parse_patt @{theory Rational} "?a + (?b /?c)= (?a + ?b)/ ?c",
4.50 - parse_patt @{theory Rational} "?a + (?b /?c)= (?a * ?b)/ ?c"],
4.51 - [@{thm rat_add}, @{thm rat_add_assoc}, @{thm rat_add1},
4.52 - @{thm rat_add1_assoc}, @{thm rat_add2}, @{thm rat_add2_assoc},
4.53 - @{thm rat_add3}, @{thm rat_add3_assoc}])]: errpat list);
4.54 *}
4.55 setup {* KEStore_Elems.add_mets
4.56 [update_metpair ["simplification", "of_rationals"]
5.1 --- a/src/Tools/isac/Knowledge/Diff.thy Sun Feb 02 02:45:11 2014 +0100
5.2 +++ b/src/Tools/isac/Knowledge/Diff.thy Sun Feb 02 03:09:40 2014 +0100
5.3 @@ -264,132 +264,8 @@
5.4 append_rls "e_rls" e_rls [],
5.5 SOME "Differentiate (f_f, v_v)",
5.6 [["diff","differentiate_equality"]]))] *}
5.7 +
5.8 ML {*
5.9 -
5.10 -(** methods **)
5.11 -
5.12 -store_met
5.13 - (prep_met thy "met_diff" [] e_metID
5.14 - (["diff"], [],
5.15 - {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
5.16 - crls = Atools_erls, errpats = [], nrls = norm_diff}, "empty_script"));
5.17 -
5.18 -store_met
5.19 - (prep_met thy "met_diff_onR" [] e_metID
5.20 - (["diff","differentiate_on_R"],
5.21 - [("#Given" ,["functionTerm f_f","differentiateFor v_v"]),
5.22 - ("#Find" ,["derivative f_f'"])
5.23 - ],
5.24 - {rew_ord'="tless_true", rls' = erls_diff, calc = [], srls = e_rls,
5.25 - prls=e_rls, crls = Atools_erls, errpats = [], nrls = norm_diff},
5.26 -"Script DiffScr (f_f::real) (v_v::real) = " ^
5.27 -" (let f_f' = Take (d_d v_v f_f) " ^
5.28 -" in (((Try (Rewrite_Set_Inst [(bdv,v_v)] diff_conv False)) @@ " ^
5.29 -" (Repeat " ^
5.30 -" ((Repeat (Rewrite_Inst [(bdv,v_v)] diff_sum False)) Or " ^
5.31 -" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod_const False)) Or " ^
5.32 -" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod False)) Or " ^
5.33 -" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_quot True )) Or " ^
5.34 -" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin False)) Or " ^
5.35 -" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin_chain False)) Or " ^
5.36 -" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos False)) Or " ^
5.37 -" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos_chain False)) Or " ^
5.38 -" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow False)) Or " ^
5.39 -" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow_chain False)) Or " ^
5.40 -" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln False)) Or " ^
5.41 -" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln_chain False)) Or " ^
5.42 -" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp False)) Or " ^
5.43 -" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp_chain False)) Or " ^
5.44 -" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_const False)) Or " ^
5.45 -" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_var False)) Or " ^
5.46 -" (Repeat (Rewrite_Set make_polynomial False)))) @@ " ^
5.47 -" (Try (Rewrite_Set_Inst [(bdv,v_v)] diff_sym_conv False)))) f_f')"
5.48 -));
5.49 -*}
5.50 -ML {*
5.51 -store_met
5.52 - (prep_met thy "met_diff_simpl" [] e_metID
5.53 - (["diff","diff_simpl"],
5.54 - [("#Given" ,["functionTerm f_f","differentiateFor v_v"]),
5.55 - ("#Find" ,["derivative f_f'"])
5.56 - ],
5.57 - {rew_ord'="tless_true", rls' = erls_diff, calc = [], srls = e_rls,
5.58 - prls=e_rls, crls = Atools_erls, errpats = [], nrls = norm_diff},
5.59 -"Script DiffScr (f_f::real) (v_v::real) = " ^
5.60 -" (let f_f' = Take (d_d v_v f_f) " ^
5.61 -" in (( " ^
5.62 -" (Repeat " ^
5.63 -" ((Repeat (Rewrite_Inst [(bdv,v_v)] diff_sum False)) Or " ^
5.64 -" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod_const False)) Or " ^
5.65 -" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod False)) Or " ^
5.66 -" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_quot True )) Or " ^
5.67 -" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin False)) Or " ^
5.68 -" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin_chain False)) Or " ^
5.69 -" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos False)) Or " ^
5.70 -" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos_chain False)) Or " ^
5.71 -" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow False)) Or " ^
5.72 -" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow_chain False)) Or " ^
5.73 -" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln False)) Or " ^
5.74 -" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln_chain False)) Or " ^
5.75 -" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp False)) Or " ^
5.76 -" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp_chain False)) Or " ^
5.77 -" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_const False)) Or " ^
5.78 -" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_var False)) Or " ^
5.79 -" (Repeat (Rewrite_Set make_polynomial False)))) " ^
5.80 -" )) f_f')"
5.81 - ));
5.82 -
5.83 -store_met
5.84 - (prep_met thy "met_diff_equ" [] e_metID
5.85 - (["diff","differentiate_equality"],
5.86 - [("#Given" ,["functionEq f_f","differentiateFor v_v"]),
5.87 - ("#Find" ,["derivativeEq f_f'"])
5.88 - ],
5.89 - {rew_ord'="tless_true", rls' = erls_diff, calc = [],
5.90 - srls = srls_diff, prls=e_rls, crls=Atools_erls, errpats = [], nrls = norm_diff},
5.91 -"Script DiffEqScr (f_f::bool) (v_v::real) = " ^
5.92 -" (let f_f' = Take ((primed (lhs f_f)) = d_d v_v (rhs f_f)) " ^
5.93 -" in (((Try (Rewrite_Set_Inst [(bdv,v_v)] diff_conv False)) @@ " ^
5.94 -" (Repeat " ^
5.95 -" ((Repeat (Rewrite_Inst [(bdv,v_v)] diff_sum False)) Or " ^
5.96 -" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_dif False)) Or " ^
5.97 -" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod_const False)) Or " ^
5.98 -" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod False)) Or " ^
5.99 -" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_quot True )) Or " ^
5.100 -" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin False)) Or " ^
5.101 -" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin_chain False)) Or " ^
5.102 -" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos False)) Or " ^
5.103 -" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos_chain False)) Or " ^
5.104 -" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow False)) Or " ^
5.105 -" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow_chain False)) Or " ^
5.106 -" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln False)) Or " ^
5.107 -" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln_chain False)) Or " ^
5.108 -" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp False)) Or " ^
5.109 -" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp_chain False)) Or " ^
5.110 -" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_const False)) Or " ^
5.111 -" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_var False)) Or " ^
5.112 -" (Repeat (Rewrite_Set make_polynomial False)))) @@ " ^
5.113 -" (Try (Rewrite_Set_Inst [(bdv,v_v)] diff_sym_conv False)))) f_f')"
5.114 -));
5.115 -
5.116 -store_met
5.117 - (prep_met thy "met_diff_after_simp" [] e_metID
5.118 - (["diff","after_simplification"],
5.119 - [("#Given" ,["functionTerm f_f","differentiateFor v_v"]),
5.120 - ("#Find" ,["derivative f_f'"])
5.121 - ],
5.122 - {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls, prls=e_rls,
5.123 - crls=Atools_erls, errpats = [], nrls = norm_Rational},
5.124 -"Script DiffScr (f_f::real) (v_v::real) = " ^
5.125 -" (let f_f' = Take (d_d v_v f_f) " ^
5.126 -" in ((Try (Rewrite_Set norm_Rational False)) @@ " ^
5.127 -" (Try (Rewrite_Set_Inst [(bdv,v_v)] diff_conv False)) @@ " ^
5.128 -" (Try (Rewrite_Set_Inst [(bdv,v_v)] norm_diff False)) @@ " ^
5.129 -" (Try (Rewrite_Set_Inst [(bdv,v_v)] diff_sym_conv False)) @@ " ^
5.130 -" (Try (Rewrite_Set norm_Rational False))) f_f')"
5.131 -));
5.132 -
5.133 -
5.134 (** CAS-commands **)
5.135
5.136 (*.handle cas-input like "Diff (a * x^3 + b, x)".*)
6.1 --- a/src/Tools/isac/Knowledge/DiffApp.thy Sun Feb 02 02:45:11 2014 +0100
6.2 +++ b/src/Tools/isac/Knowledge/DiffApp.thy Sun Feb 02 03:09:40 2014 +0100
6.3 @@ -115,119 +115,9 @@
6.4 ("#Find" ,["valuesFor v_ls"]),
6.5 ("#Relate",["additionalRels r_s"])],
6.6 e_rls, NONE, []))] *}
6.7 -ML{*
6.8 +
6.9
6.10 (** methods, scripts not yet implemented **)
6.11 -
6.12 -store_met
6.13 - (prep_met thy "met_diffapp" [] e_metID
6.14 - (["DiffApp"],
6.15 - [],
6.16 - {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
6.17 - crls = Atools_erls, errpats = [], nrls = norm_Rational
6.18 - (*, asm_rls=[],asm_thm=[]*)}, "empty_script"));
6.19 -*}
6.20 -ML{*
6.21 -store_met
6.22 - (prep_met thy "met_diffapp_max" [] e_metID
6.23 - (["DiffApp","max_by_calculus"]:metID,
6.24 - [("#Given" ,["fixedValues f_ix","maximum m_m","relations r_s",
6.25 - "boundVariable v_v","interval i_tv","errorBound e_rr"]),
6.26 - ("#Find" ,["valuesFor v_s"]),
6.27 - ("#Relate",[])
6.28 - ],
6.29 - {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls=list_rls,prls=e_rls,
6.30 - crls = eval_rls, errpats = [], nrls = norm_Rational
6.31 - (*, asm_rls=[],asm_thm=[]*)},
6.32 - "Script Maximum_value(f_ix::bool list)(m_m::real) (r_s::bool list) " ^
6.33 - " (v_v::real) (itv_v::real set) (e_rr::bool) = " ^
6.34 - " (let e_e = (hd o (filterVar m_m)) r_s; " ^
6.35 - " t_t = (if 1 < LENGTH r_s " ^
6.36 - " then (SubProblem (DiffApp',[make,function],[no_met]) " ^
6.37 - " [REAL m_m, REAL v_v, BOOL_LIST r_s]) " ^
6.38 - " else (hd r_s)); " ^
6.39 - " (m_x::real) = " ^
6.40 - "SubProblem(DiffApp',[on_interval,maximum_of,function], " ^
6.41 - " [DiffApp,max_on_interval_by_calculus]) " ^
6.42 - " [BOOL t_t, REAL v_v, REAL_SET i_tv] " ^
6.43 - " in ((SubProblem (DiffApp',[find_values,tool],[Isac,find_values]) " ^
6.44 - " [REAL m_x, REAL (Rhs t_t), REAL v_v, REAL m_m, " ^
6.45 - " BOOL_LIST (dropWhile (ident e_e) r_s)])::bool list)) "
6.46 - ));
6.47 -*}
6.48 -ML{*
6.49 -store_met
6.50 - (prep_met thy "met_diffapp_funnew" [] e_metID
6.51 - (["DiffApp","make_fun_by_new_variable"]:metID,
6.52 - [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]),
6.53 - ("#Find" ,["functionEq f_1"])
6.54 - ],
6.55 - {rew_ord'="tless_true",rls'=eval_rls,srls=list_rls,prls=e_rls,
6.56 - calc=[], crls = eval_rls, errpats = [], nrls = norm_Rational(*,asm_rls=[],asm_thm=[]*)},
6.57 - "Script Make_fun_by_new_variable (f_f::real) (v_v::real) " ^
6.58 - " (eqs::bool list) = " ^
6.59 - "(let h_h = (hd o (filterVar f_f)) eqs; " ^
6.60 - " e_s = dropWhile (ident h_h) eqs; " ^
6.61 - " v_s = dropWhile (ident f_f) (Vars h_h); " ^
6.62 - " v_1 = NTH 1 v_s; " ^
6.63 - " v_2 = NTH 2 v_s; " ^
6.64 - " e_1 = (hd o (filterVar v_1)) e_s; " ^
6.65 - " e_2 = (hd o (filterVar v_2)) e_s; " ^
6.66 - " (s_1::bool list) = " ^
6.67 - " (SubProblem (DiffApp',[univariate,equation],[no_met])" ^
6.68 - " [BOOL e_1, REAL v_1]); " ^
6.69 - " (s_2::bool list) = " ^
6.70 - " (SubProblem (DiffApp',[univariate,equation],[no_met])" ^
6.71 - " [BOOL e_2, REAL v_2])" ^
6.72 - "in Substitute [(v_1 = (rhs o hd) s_1),(v_2 = (rhs o hd) s_2)] h_h)"
6.73 -));
6.74 -*}
6.75 -ML{*
6.76 -store_met
6.77 -(prep_met thy "met_diffapp_funexp" [] e_metID
6.78 -(["DiffApp","make_fun_by_explicit"]:metID,
6.79 - [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]),
6.80 - ("#Find" ,["functionEq f_1"])
6.81 - ],
6.82 - {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls=list_rls,prls=e_rls,
6.83 - crls = eval_rls, errpats = [], nrls = norm_Rational
6.84 - (*, asm_rls=[],asm_thm=[]*)},
6.85 - "Script Make_fun_by_explicit (f_f::real) (v_v::real) " ^
6.86 - " (eqs::bool list) = " ^
6.87 - " (let h_h = (hd o (filterVar f_f)) eqs; " ^
6.88 - " e_1 = hd (dropWhile (ident h_h) eqs); " ^
6.89 - " v_s = dropWhile (ident f_f) (Vars h_h); " ^
6.90 - " v_1 = hd (dropWhile (ident v_v) v_s); " ^
6.91 - " (s_1::bool list)= " ^
6.92 - " (SubProblem(DiffApp',[univariate,equation],[no_met])" ^
6.93 - " [BOOL e_1, REAL v_1]) " ^
6.94 - " in Substitute [(v_1 = (rhs o hd) s_1)] h_h) "
6.95 - ));
6.96 -*}
6.97 -ML{*
6.98 -store_met
6.99 - (prep_met thy "met_diffapp_max_oninterval" [] e_metID
6.100 - (["DiffApp","max_on_interval_by_calculus"]:metID,
6.101 - [("#Given" ,["functionEq t_t","boundVariable v_v","interval i_tv"(*,
6.102 - "errorBound e_rr"*)]),
6.103 - ("#Find" ,["maxArgument v_0"])
6.104 - ],
6.105 - {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls = e_rls,prls=e_rls,
6.106 - crls = eval_rls, errpats = [], nrls = norm_Rational
6.107 - (*, asm_rls=[],asm_thm=[]*)},
6.108 - "empty_script"
6.109 - ));
6.110 -*}
6.111 -ML{*
6.112 -store_met
6.113 - (prep_met thy "met_diffapp_findvals" [] e_metID
6.114 - (["DiffApp","find_values"]:metID,
6.115 - [],
6.116 - {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls = e_rls,prls=e_rls,
6.117 - crls = eval_rls, errpats = [], nrls = norm_Rational(*,
6.118 - asm_rls=[],asm_thm=[]*)},
6.119 - "empty_script"));
6.120 -*}
6.121 setup {* KEStore_Elems.add_mets
6.122 [prep_met thy "met_diffapp" [] e_metID
6.123 (["DiffApp"], [],
7.1 --- a/src/Tools/isac/Knowledge/DiophantEq.thy Sun Feb 02 02:45:11 2014 +0100
7.2 +++ b/src/Tools/isac/Knowledge/DiophantEq.thy Sun Feb 02 03:09:40 2014 +0100
7.3 @@ -29,24 +29,6 @@
7.4 e_rls, SOME "solve (e_e::bool, v_v::int)", [["LinEq","solve_lineq_equation"]]))] *}
7.5
7.6 text {*method solving the usecase*}
7.7 -ML {*
7.8 -store_met
7.9 -(prep_met thy "met_test_diophant" [] e_metID
7.10 - (["Test","solve_diophant"]:metID,
7.11 - [("#Given" ,["boolTestGiven e_e","intTestGiven (v_v::int)"]),
7.12 - (* TODO: drop ^^^^^*)
7.13 - ("#Where" ,[]),
7.14 - ("#Find" ,["boolTestFind s_s"])
7.15 - ],
7.16 - {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = e_rls,
7.17 - prls = e_rls, calc = [], crls = tval_rls, errpats = [], nrls = Test_simplify},
7.18 - "Script Diophant_equation (e_e::bool) (v_v::int)= " ^
7.19 - "(Repeat " ^
7.20 - " ((Try (Rewrite_Inst [(bdv,v_v::int)] int_isolate_add False)) @@" ^
7.21 - " (Try (Calculate PLUS)) @@ " ^
7.22 - " (Try (Calculate TIMES))) e_e::bool)"
7.23 - ))
7.24 -*}
7.25 setup {* KEStore_Elems.add_mets
7.26 [prep_met thy "met_test_diophant" [] e_metID
7.27 (["Test","solve_diophant"]:metID,
8.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Sun Feb 02 02:45:11 2014 +0100
8.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Sun Feb 02 03:09:40 2014 +0100
8.3 @@ -495,115 +495,7 @@
8.4 append_rls "e_rls" e_rls [(*for preds in where_*)],
8.5 SOME "solveSystem e_s v_s",
8.6 [["EqSystem","normalize","4x4"]]))] *}
8.7 -ML {*
8.8 -(** methods **)
8.9
8.10 -store_met
8.11 - (prep_met thy "met_eqsys" [] e_metID
8.12 - (["EqSystem"],
8.13 - [],
8.14 - {rew_ord'="tless_true", rls' = Erls, calc = [],
8.15 - srls = Erls, prls = Erls, crls = Erls, errpats = [], nrls = Erls},
8.16 - "empty_script"
8.17 - ));
8.18 -store_met
8.19 - (prep_met thy "met_eqsys_topdown" [] e_metID
8.20 - (["EqSystem","top_down_substitution"],
8.21 - [],
8.22 - {rew_ord'="tless_true", rls' = Erls, calc = [],
8.23 - srls = Erls, prls = Erls, crls = Erls, errpats = [], nrls = Erls},
8.24 - "empty_script"
8.25 - ));
8.26 -*}
8.27 -ML {*
8.28 -store_met
8.29 - (prep_met thy "met_eqsys_topdown_2x2" [] e_metID
8.30 - (["EqSystem","top_down_substitution","2x2"],
8.31 - [("#Given" ,["equalities e_s", "solveForVars v_s"]),
8.32 - ("#Where" ,
8.33 - ["(tl v_s) from v_s occur_exactly_in (NTH 1 (e_s::bool list))",
8.34 - " v_s from v_s occur_exactly_in (NTH 2 (e_s::bool list))"]),
8.35 - ("#Find" ,["solution ss'''"])
8.36 - ],
8.37 - {rew_ord'="ord_simplify_System", rls' = Erls, calc = [],
8.38 - srls = append_rls "srls_top_down_2x2" e_rls
8.39 - [Thm ("hd_thm",num_str @{thm hd_thm}),
8.40 - Thm ("tl_Cons",num_str @{thm tl_Cons}),
8.41 - Thm ("tl_Nil",num_str @{thm tl_Nil})
8.42 - ],
8.43 - prls = prls_triangular, crls = Erls, errpats = [], nrls = Erls},
8.44 -"Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^
8.45 -" (let e_1 = Take (hd e_s); " ^
8.46 -" e_1 = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
8.47 -" isolate_bdvs False)) @@ " ^
8.48 -" (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
8.49 -" simplify_System False))) e_1; " ^
8.50 -" e_2 = Take (hd (tl e_s)); " ^
8.51 -" e_2 = ((Substitute [e_1]) @@ " ^
8.52 -" (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
8.53 -" simplify_System_parenthesized False)) @@ " ^
8.54 -" (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
8.55 -" isolate_bdvs False)) @@ " ^
8.56 -" (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
8.57 -" simplify_System False))) e_2; " ^
8.58 -" e__s = Take [e_1, e_2] " ^
8.59 -" in (Try (Rewrite_Set order_system False)) e__s)"
8.60 -(*---------------------------------------------------------------------------
8.61 - this script does NOT separate the equations as above,
8.62 - but it does not yet work due to preliminary script-interpreter,
8.63 - see eqsystem.sml 'script [EqSystem,top_down_substitution,2x2] Vers.2'
8.64 -
8.65 -"Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^
8.66 -" (let e__s = Take e_s; " ^
8.67 -" e_1 = hd e__s; " ^
8.68 -" e_2 = hd (tl e__s); " ^
8.69 -" e__s = [e_1, Substitute [e_1] e_2] " ^
8.70 -" in ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
8.71 -" simplify_System_parenthesized False)) @@ " ^
8.72 -" (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))] " ^
8.73 -" isolate_bdvs False)) @@ " ^
8.74 -" (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
8.75 -" simplify_System False))) e__s)"
8.76 ----------------------------------------------------------------------------*)
8.77 - ));
8.78 -*}
8.79 -ML {*
8.80 -store_met
8.81 - (prep_met thy "met_eqsys_norm" [] e_metID
8.82 - (["EqSystem","normalize"],
8.83 - [],
8.84 - {rew_ord'="tless_true", rls' = Erls, calc = [],
8.85 - srls = Erls, prls = Erls, crls = Erls, errpats = [], nrls = Erls},
8.86 - "empty_script"
8.87 - ));
8.88 -*}
8.89 -ML {*
8.90 -store_met
8.91 - (prep_met thy "met_eqsys_norm_2x2" [] e_metID
8.92 - (["EqSystem","normalize","2x2"],
8.93 - [("#Given" ,["equalities e_s", "solveForVars v_s"]),
8.94 - ("#Find" ,["solution ss'''"])],
8.95 - {rew_ord'="tless_true", rls' = Erls, calc = [],
8.96 - srls = append_rls "srls_normalize_2x2" e_rls
8.97 - [Thm ("hd_thm",num_str @{thm hd_thm}),
8.98 - Thm ("tl_Cons",num_str @{thm tl_Cons}),
8.99 - Thm ("tl_Nil",num_str @{thm tl_Nil})
8.100 - ],
8.101 - prls = Erls, crls = Erls, errpats = [], nrls = Erls},
8.102 -"Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^
8.103 -" (let e__s = ((Try (Rewrite_Set norm_Rational False)) @@ " ^
8.104 -" (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
8.105 -" simplify_System_parenthesized False)) @@ " ^
8.106 -" (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
8.107 -" isolate_bdvs False)) @@ " ^
8.108 -" (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
8.109 -" simplify_System_parenthesized False)) @@ " ^
8.110 -" (Try (Rewrite_Set order_system False))) e_s " ^
8.111 -" in (SubProblem (EqSystem',[LINEAR,system],[no_met]) " ^
8.112 -" [BOOL_LIST e__s, REAL_LIST v_s]))"
8.113 - ));
8.114 -
8.115 -*}
8.116 ML {*
8.117 (*this is for NTH only*)
8.118 val srls = Rls {id="srls_normalize_4x4",
8.119 @@ -620,73 +512,9 @@
8.120 Calc("Groups.plus_class.plus", eval_binop "#add_"),
8.121 Thm ("NTH_NIL",num_str @{thm NTH_NIL})],
8.122 scr = EmptyScr};
8.123 -
8.124 -store_met
8.125 - (prep_met thy "met_eqsys_norm_4x4" [] e_metID
8.126 - (["EqSystem","normalize","4x4"],
8.127 - [("#Given" ,["equalities e_s", "solveForVars v_s"]),
8.128 - ("#Find" ,["solution ss'''"])],
8.129 - {rew_ord'="tless_true", rls' = Erls, calc = [],
8.130 - srls = append_rls "srls_normalize_4x4" srls
8.131 - [Thm ("hd_thm",num_str @{thm hd_thm}),
8.132 - Thm ("tl_Cons",num_str @{thm tl_Cons}),
8.133 - Thm ("tl_Nil",num_str @{thm tl_Nil})
8.134 - ],
8.135 - prls = Erls, crls = Erls, errpats = [], nrls = Erls},
8.136 -(*STOPPED.WN06? met ["EqSystem","normalize","4x4"] @@@@@@@@@@@@@@@@@@@@@@@@@@@*)
8.137 -"Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^
8.138 -" (let e__s = " ^
8.139 -" ((Try (Rewrite_Set norm_Rational False)) @@ " ^
8.140 -" (Repeat (Rewrite commute_0_equality False)) @@ " ^
8.141 -" (Try (Rewrite_Set_Inst [(bdv_1, NTH 1 v_s),(bdv_2, NTH 2 v_s ), " ^
8.142 -" (bdv_3, NTH 3 v_s),(bdv_3, NTH 4 v_s )] " ^
8.143 -" simplify_System_parenthesized False)) @@ " ^
8.144 -" (Try (Rewrite_Set_Inst [(bdv_1, NTH 1 v_s),(bdv_2, NTH 2 v_s ), " ^
8.145 -" (bdv_3, NTH 3 v_s),(bdv_3, NTH 4 v_s )] " ^
8.146 -" isolate_bdvs_4x4 False)) @@ " ^
8.147 -" (Try (Rewrite_Set_Inst [(bdv_1, NTH 1 v_s),(bdv_2, NTH 2 v_s ), " ^
8.148 -" (bdv_3, NTH 3 v_s),(bdv_3, NTH 4 v_s )] " ^
8.149 -" simplify_System_parenthesized False)) @@ " ^
8.150 -" (Try (Rewrite_Set order_system False))) e_s " ^
8.151 -" in (SubProblem (EqSystem',[LINEAR,system],[no_met]) " ^
8.152 -" [BOOL_LIST e__s, REAL_LIST v_s]))"
8.153 -));
8.154 -
8.155 -store_met
8.156 -(prep_met thy "met_eqsys_topdown_4x4" [] e_metID
8.157 - (["EqSystem","top_down_substitution","4x4"],
8.158 - [("#Given" ,["equalities e_s", "solveForVars v_s"]),
8.159 - ("#Where" , (*accepts missing variables up to diagonal form*)
8.160 - ["(NTH 1 (v_s::real list)) occurs_in (NTH 1 (e_s::bool list))",
8.161 - "(NTH 2 (v_s::real list)) occurs_in (NTH 2 (e_s::bool list))",
8.162 - "(NTH 3 (v_s::real list)) occurs_in (NTH 3 (e_s::bool list))",
8.163 - "(NTH 4 (v_s::real list)) occurs_in (NTH 4 (e_s::bool list))"
8.164 - ]),
8.165 - ("#Find" ,["solution ss'''"])
8.166 - ],
8.167 - {rew_ord'="ord_simplify_System", rls' = Erls, calc = [],
8.168 - srls = append_rls "srls_top_down_4x4" srls [],
8.169 - prls = append_rls "prls_tri_4x4_lin_sys" prls_triangular
8.170 - [Calc ("Atools.occurs'_in",eval_occurs_in "")],
8.171 - crls = Erls, errpats = [], nrls = Erls},
8.172 -(*FIXXXXME.WN060916: this script works ONLY for exp 7.79 @@@@@@@@@@@@@@@@@@@@*)
8.173 -"Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^
8.174 -" (let e_1 = NTH 1 e_s; " ^
8.175 -" e_2 = Take (NTH 2 e_s); " ^
8.176 -" e_2 = ((Substitute [e_1]) @@ " ^
8.177 -" (Try (Rewrite_Set_Inst [(bdv_1,NTH 1 v_s),(bdv_2,NTH 2 v_s)," ^
8.178 -" (bdv_3,NTH 3 v_s),(bdv_4,NTH 4 v_s)]" ^
8.179 -" simplify_System_parenthesized False)) @@ " ^
8.180 -" (Try (Rewrite_Set_Inst [(bdv_1,NTH 1 v_s),(bdv_2,NTH 2 v_s)," ^
8.181 -" (bdv_3,NTH 3 v_s),(bdv_4,NTH 4 v_s)]" ^
8.182 -" isolate_bdvs False)) @@ " ^
8.183 -" (Try (Rewrite_Set_Inst [(bdv_1,NTH 1 v_s),(bdv_2,NTH 2 v_s)," ^
8.184 -" (bdv_3,NTH 3 v_s),(bdv_4,NTH 4 v_s)]" ^
8.185 -" norm_Rational False))) e_2 " ^
8.186 -" in [e_1, e_2, NTH 3 e_s, NTH 4 e_s])"
8.187 -));
8.188 *}
8.189
8.190 +(**methods**)
8.191 setup {* KEStore_Elems.add_mets
8.192 [prep_met thy "met_eqsys" [] e_metID
8.193 (["EqSystem"], [],
9.1 --- a/src/Tools/isac/Knowledge/Equation.thy Sun Feb 02 02:45:11 2014 +0100
9.2 +++ b/src/Tools/isac/Knowledge/Equation.thy Sun Feb 02 03:09:40 2014 +0100
9.3 @@ -85,18 +85,6 @@
9.4 (("Isac", ["univariate","equation"], ["no_met"]), argl2dtss))]*}
9.5
9.6
9.7 -ML {*
9.8 -store_met
9.9 - (prep_met thy "met_equ" [] e_metID
9.10 - (["Equation"],
9.11 - [],
9.12 - {rew_ord'="tless_true", rls'=Erls, calc = [],
9.13 - srls = e_rls,
9.14 - prls=e_rls,
9.15 - crls = Atools_erls, errpats = [], nrls = e_rls},
9.16 -"empty_script"
9.17 -));
9.18 -*}
9.19 setup {* KEStore_Elems.add_mets
9.20 [prep_met thy "met_equ" [] e_metID
9.21 (["Equation"], [],
10.1 --- a/src/Tools/isac/Knowledge/InsSort.thy Sun Feb 02 02:45:11 2014 +0100
10.2 +++ b/src/Tools/isac/Knowledge/InsSort.thy Sun Feb 02 03:09:40 2014 +0100
10.3 @@ -67,28 +67,8 @@
10.4 (["inssort","functional"]:pblID,
10.5 [("#Given" ,["unsorted u_"]), ("#Find" ,["sorted s_"])], []))] *}
10.6
10.7 -ML {*
10.8 (** method,
10.9 todo: implementation needs extra object-level lists **)
10.10 -
10.11 -store_met
10.12 - (prep_met @{theory "Diff"}
10.13 - (["InsSort"],
10.14 - [],
10.15 - {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
10.16 - crls = Atools_rls, errpats = [], nrls = norm_Rational
10.17 - (*, asm_rls=[],asm_thm=[]*)}, "empty_script"));
10.18 -store_met
10.19 - (prep_met @{theory "InsSort"} (*test-version for [#1,#3,#2] only: see *.sml*)
10.20 - (["InsSort","sort"]:metID,
10.21 - [("#Given" ,["unsorted u_"]),
10.22 - ("#Find" ,["sorted s_"])
10.23 - ],
10.24 - {rew_ord'="tless_true",rls'=eval_rls,calc = [], srls = e_rls, prls=e_rls,
10.25 - crls = eval_rls, errpats = [], nrls = norm_Rational},
10.26 - "Script Sort (u_::'a list) = (Rewrite_Set ins_sort False) u_"
10.27 - ));
10.28 -*}
10.29 setup {* KEStore_Elems.add_mets
10.30 [prep_met @{theory "Diff"}
10.31 (["InsSort"], [],
11.1 --- a/src/Tools/isac/Knowledge/Integrate.thy Sun Feb 02 02:45:11 2014 +0100
11.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy Sun Feb 02 03:09:40 2014 +0100
11.3 @@ -351,42 +351,8 @@
11.4 append_rls "e_rls" e_rls [(*for preds in where_*)],
11.5 SOME "Integrate (f_f, v_v)",
11.6 [["diff","integration","named"]]))] *}
11.7 -ML {*
11.8 +
11.9 (** methods **)
11.10 -
11.11 -store_met
11.12 - (prep_met thy "met_diffint" [] e_metID
11.13 - (["diff","integration"],
11.14 - [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
11.15 - ("#Find" ,["antiDerivative F_F"])
11.16 - ],
11.17 - {rew_ord'="tless_true", rls'=Atools_erls, calc = [],
11.18 - srls = e_rls,
11.19 - prls=e_rls,
11.20 - crls = Atools_erls, errpats = [], nrls = e_rls},
11.21 -"Script IntegrationScript (f_f::real) (v_v::real) = " ^
11.22 -" (let t_t = Take (Integral f_f D v_v) " ^
11.23 -" in (Rewrite_Set_Inst [(bdv,v_v)] integration False) (t_t::real))"
11.24 -));
11.25 - *}
11.26 -ML {*
11.27 -
11.28 -store_met
11.29 - (prep_met thy "met_diffint_named" [] e_metID
11.30 - (["diff","integration","named"],
11.31 - [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
11.32 - ("#Find" ,["antiDerivativeName F_F"])
11.33 - ],
11.34 - {rew_ord'="tless_true", rls'=Atools_erls, calc = [],
11.35 - srls = e_rls,
11.36 - prls=e_rls,
11.37 - crls = Atools_erls, errpats = [], nrls = e_rls},
11.38 -"Script NamedIntegrationScript (f_f::real) (v_v::real) (F_F::real=>real) = " ^
11.39 -" (let t_t = Take (F_F v_v = Integral f_f D v_v) " ^
11.40 -" in ((Try (Rewrite_Set_Inst [(bdv,v_v)] simplify_Integral False)) @@ " ^
11.41 -" (Rewrite_Set_Inst [(bdv,v_v)] integration False)) t_t) "
11.42 - ));
11.43 -*}
11.44 setup {* KEStore_Elems.add_mets
11.45 [prep_met thy "met_diffint" [] e_metID
11.46 (["diff","integration"],
12.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Sun Feb 02 02:45:11 2014 +0100
12.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Sun Feb 02 03:09:40 2014 +0100
12.3 @@ -71,181 +71,7 @@
12.4 ("((Script InverseZTransform (_ =))// (_))" 9)
12.5
12.6 subsection {*Setup Parent Nodes in Hierarchy of Method*}
12.7 -ML {*
12.8 -store_met
12.9 - (prep_met thy "met_SP" [] e_metID
12.10 - (["SignalProcessing"], [],
12.11 - {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls,
12.12 - crls = e_rls, errpats = [], nrls = e_rls}, "empty_script"));
12.13 -store_met
12.14 - (prep_met thy "met_SP_Ztrans" [] e_metID
12.15 - (["SignalProcessing", "Z_Transform"], [],
12.16 - {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls,
12.17 - crls = e_rls, errpats = [], nrls = e_rls}, "empty_script"));
12.18 -val thy = @{theory}; (*latest version of thy required*)
12.19 -store_met
12.20 - (prep_met thy "met_SP_Ztrans_inv" [] e_metID
12.21 - (["SignalProcessing", "Z_Transform", "Inverse"],
12.22 - [("#Given" ,["filterExpression (X_eq::bool)"]),
12.23 - ("#Find" ,["stepResponse (n_eq::bool)"])
12.24 - ],
12.25 - {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls,
12.26 - crls = e_rls, errpats = [], nrls = e_rls},
12.27 -"Script InverseZTransform (X_eq::bool) =" ^ (*(1/z) instead of z ^^^ -1*)
12.28 -" (let X = Take X_eq;" ^
12.29 -" X' = Rewrite ruleZY False X;" ^ (*z * denominator*)
12.30 -" X' = (Rewrite_Set norm_Rational False) X';" ^ (*simplify*)
12.31 -" funterm = Take (rhs X');" ^ (*drop X' z = for equation solving*)
12.32 -" denom = (Rewrite_Set partial_fraction False) funterm;" ^ (*get_denominator*)
12.33 -" equ = (denom = (0::real));" ^
12.34 -" fun_arg = Take (lhs X');" ^
12.35 -" arg = (Rewrite_Set partial_fraction False) X';" ^ (*get_argument TODO*)
12.36 -" (L_L::bool list) = " ^
12.37 -" (SubProblem (Test', " ^
12.38 -" [LINEAR,univariate,equation,test]," ^
12.39 -" [Test,solve_linear]) " ^
12.40 -" [BOOL equ, REAL z]) " ^
12.41 -" in X)"
12.42 - ));
12.43 -*}
12.44 -ML {*
12.45 - store_met(
12.46 - prep_met thy "met_SP_Ztrans_inv" [] e_metID
12.47 - (["SignalProcessing",
12.48 - "Z_Transform",
12.49 - "Inverse"],
12.50 - [
12.51 - ("#Given" ,["filterExpression X_eq"]),
12.52 - ("#Find" ,["stepResponse n_eq"])
12.53 - ],
12.54 - {
12.55 - rew_ord'="tless_true",
12.56 - rls'= e_rls, calc = [],
12.57 - srls = srls_partial_fraction,
12.58 - prls = e_rls,
12.59 - crls = e_rls, errpats = [], nrls = e_rls
12.60 - },
12.61 - "Script InverseZTransform (X_eq::bool) = "^
12.62 - (*(1/z) instead of z ^^^ -1*)
12.63 - "(let X = Take X_eq; "^
12.64 - " X' = Rewrite ruleZY False X; "^
12.65 - (*z * denominator*)
12.66 - " (num_orig::real) = get_numerator (rhs X'); "^
12.67 - " X' = (Rewrite_Set norm_Rational False) X'; "^
12.68 - (*simplify*)
12.69 - " (X'_z::real) = lhs X'; "^
12.70 - " (zzz::real) = argument_in X'_z; "^
12.71 - " (funterm::real) = rhs X'; "^
12.72 - (*drop X' z = for equation solving*)
12.73 - " (denom::real) = get_denominator funterm; "^
12.74 - (*get_denominator*)
12.75 - " (num::real) = get_numerator funterm; "^
12.76 - (*get_numerator*)
12.77 - " (equ::bool) = (denom = (0::real)); "^
12.78 - " (L_L::bool list) = (SubProblem (PolyEq', "^
12.79 - " [abcFormula,degree_2,polynomial,univariate,equation], "^
12.80 - " [no_met]) "^
12.81 - " [BOOL equ, REAL zzz]); "^
12.82 - " (facs::real) = factors_from_solution L_L; "^
12.83 - " (eql::real) = Take (num_orig / facs); "^
12.84 -
12.85 - " (eqr::real) = (Try (Rewrite_Set ansatz_rls False)) eql; "^
12.86 -
12.87 - " (eq::bool) = Take (eql = eqr); "^
12.88 - (*Maybe possible to use HOLogic.mk_eq ??*)
12.89 - " eq = (Try (Rewrite_Set equival_trans False)) eq; "^
12.90 -
12.91 - " eq = drop_questionmarks eq; "^
12.92 - " (z1::real) = (rhs (NTH 1 L_L)); "^
12.93 - (*
12.94 - * prepare equation for a - eq_a
12.95 - * therefor substitute z with solution 1 - z1
12.96 - *)
12.97 - " (z2::real) = (rhs (NTH 2 L_L)); "^
12.98 -
12.99 - " (eq_a::bool) = Take eq; "^
12.100 - " eq_a = (Substitute [zzz=z1]) eq; "^
12.101 - " eq_a = (Rewrite_Set norm_Rational False) eq_a; "^
12.102 - " (sol_a::bool list) = "^
12.103 - " (SubProblem (Isac', "^
12.104 - " [univariate,equation],[no_met]) "^
12.105 - " [BOOL eq_a, REAL (A::real)]); "^
12.106 - " (a::real) = (rhs(NTH 1 sol_a)); "^
12.107 -
12.108 - " (eq_b::bool) = Take eq; "^
12.109 - " eq_b = (Substitute [zzz=z2]) eq_b; "^
12.110 - " eq_b = (Rewrite_Set norm_Rational False) eq_b; "^
12.111 - " (sol_b::bool list) = "^
12.112 - " (SubProblem (Isac', "^
12.113 - " [univariate,equation],[no_met]) "^
12.114 - " [BOOL eq_b, REAL (B::real)]); "^
12.115 - " (b::real) = (rhs(NTH 1 sol_b)); "^
12.116 -
12.117 - " eqr = drop_questionmarks eqr; "^
12.118 - " (pbz::real) = Take eqr; "^
12.119 - " pbz = ((Substitute [A=a, B=b]) pbz); "^
12.120 -
12.121 - " pbz = Rewrite ruleYZ False pbz; "^
12.122 - " pbz = drop_questionmarks pbz; "^
12.123 -
12.124 - " (X_z::bool) = Take (X_z = pbz); "^
12.125 - " (n_eq::bool) = (Rewrite_Set inverse_z False) X_z; "^
12.126 - " n_eq = drop_questionmarks n_eq "^
12.127 - "in n_eq)"
12.128 - )
12.129 - );
12.130 -
12.131 -store_met (prep_met thy "met_SP_Ztrans_inv_sub" [] e_metID
12.132 - (["SignalProcessing", "Z_Transform", "Inverse_sub"],
12.133 - [("#Given" ,["filterExpression X_eq"]),
12.134 - ("#Find" ,["stepResponse n_eq"])],
12.135 - {rew_ord'="tless_true",
12.136 - rls'= e_rls, calc = [],
12.137 - srls = Rls {id="srls_partial_fraction",
12.138 - preconds = [],
12.139 - rew_ord = ("termlessI",termlessI),
12.140 - erls = append_rls "erls_in_srls_partial_fraction" e_rls
12.141 - [(*for asm in NTH_CONS ...*)
12.142 - Calc ("Orderings.ord_class.less",eval_equ "#less_"),
12.143 - (*2nd NTH_CONS pushes n+-1 into asms*)
12.144 - Calc("Groups.plus_class.plus", eval_binop "#add_")],
12.145 - srls = Erls, calc = [], errpatts = [],
12.146 - rules = [
12.147 - Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
12.148 - Calc("Groups.plus_class.plus", eval_binop "#add_"),
12.149 - Thm ("NTH_NIL",num_str @{thm NTH_NIL}),
12.150 - Calc("Tools.lhs", eval_lhs "eval_lhs_"),
12.151 - Calc("Tools.rhs", eval_rhs"eval_rhs_"),
12.152 - Calc("Atools.argument'_in", eval_argument_in "Atools.argument'_in"),
12.153 - Calc("Rational.get_denominator", eval_get_denominator "#get_denominator"),
12.154 - Calc("Rational.get_numerator", eval_get_numerator "#get_numerator"),
12.155 - Calc("Partial_Fractions.factors_from_solution",
12.156 - eval_factors_from_solution "#factors_from_solution"),
12.157 - Calc("Partial_Fractions.drop_questionmarks", eval_drop_questionmarks "#drop_?")],
12.158 - scr = EmptyScr},
12.159 - prls = e_rls, crls = e_rls, errpats = [], nrls = norm_Rational},
12.160 - "Script InverseZTransform (X_eq::bool) = "^(*([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])*)
12.161 - "(let X = Take X_eq; "^(*([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))*)
12.162 - " X' = Rewrite ruleZY False X; "^(*([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
12.163 - " (X'_z::real) = lhs X'; "^(* ?X' z*)
12.164 - " (zzz::real) = argument_in X'_z; "^(* z *)
12.165 - " (funterm::real) = rhs X'; "^(* 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
12.166 -
12.167 - " (pbz::real) = (SubProblem (Isac', "^(**)
12.168 - " [partial_fraction,rational,simplification], "^
12.169 - " [simplification,of_rationals,to_partial_fraction]) "^
12.170 - " [REAL funterm, REAL zzz]); "^(*([2], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
12.171 -
12.172 - " (pbz_eq::bool) = Take (X'_z = pbz); "^(*([3], Frm), ?X' z = 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
12.173 - " pbz_eq = Rewrite ruleYZ False pbz_eq; "^(*([3], Res), ?X' z = 4 * (?z / (z - 1 / 2)) + -4 * (?z / (z - -1 / 4))*)
12.174 - " pbz_eq = drop_questionmarks pbz_eq; "^(* 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
12.175 - " (X_zeq::bool) = Take (X_z = rhs pbz_eq); "^(*([4], Frm), X_z = 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
12.176 - " n_eq = (Rewrite_Set inverse_z False) X_zeq; "^(*([4], Res), X_z = 4 * (1 / 2) ^^^ ?n * ?u [?n] + -4 * (-1 / 4) ^^^ ?n * ?u [?n]*)
12.177 - " n_eq = drop_questionmarks n_eq "^(* X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
12.178 - "in n_eq)" (*([], Res), X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
12.179 - ));
12.180 -
12.181 -*}
12.182 +ML {* val thy = @{theory}; (*latest version of thy required*) *}
12.183 setup {* KEStore_Elems.add_mets
12.184 [prep_met thy "met_SP" [] e_metID
12.185 (["SignalProcessing"], [],
13.1 --- a/src/Tools/isac/Knowledge/LinEq.thy Sun Feb 02 02:45:11 2014 +0100
13.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy Sun Feb 02 03:09:40 2014 +0100
13.3 @@ -132,39 +132,6 @@
13.4 ("#Find" ,["solutions v_v'i'"])],
13.5 LinEq_prls, SOME "solve (e_e::bool, v_v)", [["LinEq", "solve_lineq_equation"]]))] *}
13.6
13.7 -ML {*
13.8 -(*-------------- methods------------------------------------------------------*)
13.9 -store_met
13.10 - (prep_met thy "met_eqlin" [] e_metID
13.11 - (["LinEq"],
13.12 - [],
13.13 - {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
13.14 - crls=LinEq_crls, errpats = [], nrls = norm_Poly}, "empty_script"));
13.15 -
13.16 -(* ansprechen mit ["LinEq","solve_univar_equation"] *)
13.17 -store_met
13.18 -(prep_met thy "met_eq_lin" [] e_metID
13.19 - (["LinEq","solve_lineq_equation"],
13.20 - [("#Given", ["equality e_e", "solveFor v_v"]),
13.21 - ("#Where", ["Not ((lhs e_e) is_polyrat_in v_v)",
13.22 - "((lhs e_e) has_degree_in v_v) = 1"]),
13.23 - ("#Find", ["solutions v_v'i'"])
13.24 - ],
13.25 - {rew_ord'="termlessI", rls'=LinEq_erls, srls=e_rls, prls=LinEq_prls,
13.26 - calc=[], crls=LinEq_crls, errpats = [], nrls = norm_Poly},
13.27 - "Script Solve_lineq_equation (e_e::bool) (v_v::real) = " ^
13.28 - "(let e_e =((Try (Rewrite all_left False)) @@ " ^
13.29 - " (Try (Repeat (Rewrite makex1_x False))) @@ " ^
13.30 - " (Try (Rewrite_Set expand_binoms False)) @@ " ^
13.31 - " (Try (Repeat (Rewrite_Set_Inst [(bdv, v_v::real)] " ^
13.32 - " make_ratpoly_in False))) @@ " ^
13.33 - " (Try (Repeat (Rewrite_Set LinPoly_simplify False))))e_e;" ^
13.34 - " e_e = ((Try (Rewrite_Set_Inst [(bdv, v_v::real)] " ^
13.35 - " LinEq_simplify True)) @@ " ^
13.36 - " (Repeat(Try (Rewrite_Set LinPoly_simplify False)))) e_e " ^
13.37 - " in ((Or_to_List e_e)::bool list))"
13.38 - ));
13.39 -*}
13.40 (*-------------- methods------------------------------------------------------*)
13.41 setup {* KEStore_Elems.add_mets
13.42 [prep_met thy "met_eqlin" [] e_metID
14.1 --- a/src/Tools/isac/Knowledge/LogExp.thy Sun Feb 02 02:45:11 2014 +0100
14.2 +++ b/src/Tools/isac/Knowledge/LogExp.thy Sun Feb 02 03:09:40 2014 +0100
14.3 @@ -37,24 +37,7 @@
14.4 ("#With" ,["||(lhs (Subst (v'i', v_v) e_e) - " ^
14.5 " (rhs (Subst (v'i', v_v) e_e) || < eps)"])],
14.6 PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["Equation","solve_log"]]))] *}
14.7 -ML {*
14.8 -(** methods **)
14.9 -store_met
14.10 - (prep_met thy "met_equ_log" [] e_metID
14.11 - (["Equation","solve_log"],
14.12 - [("#Given" ,["equality e_e","solveFor v_v"]),
14.13 - ("#Where" ,["matches ((?a log ?v_v) = ?b) e_e"]),
14.14 - ("#Find" ,["solutions v_v'i'"])
14.15 - ],
14.16 - {rew_ord'="termlessI",rls'=PolyEq_erls,srls=e_rls,prls=PolyEq_prls,
14.17 - calc=[],crls=PolyEq_crls, errpats = [], nrls = norm_Rational},
14.18 - "Script Solve_log (e_e::bool) (v_v::real) = " ^
14.19 - "(let e_e = ((Rewrite equality_power False) @@ " ^
14.20 - " (Rewrite exp_invers_log False) @@ " ^
14.21 - " (Rewrite_Set norm_Poly False)) e_e " ^
14.22 - " in [e_e])"
14.23 - ));
14.24 -*}
14.25 +
14.26 (** methods **)
14.27 setup {* KEStore_Elems.add_mets
14.28 [prep_met thy "met_equ_log" [] e_metID
15.1 --- a/src/Tools/isac/Knowledge/Partial_Fractions.thy Sun Feb 02 02:45:11 2014 +0100
15.2 +++ b/src/Tools/isac/Knowledge/Partial_Fractions.thy Sun Feb 02 03:09:40 2014 +0100
15.3 @@ -223,57 +223,8 @@
15.4 parseNEW ctxt "decomposedFunction p_p'''";
15.5 parseNEW ctxt "decomposedFunction";
15.6 *}
15.7 -ML {*
15.8 -*}
15.9 -ML {* (* current version, error outcommented *)
15.10 -store_met
15.11 - (prep_met @{theory} "met_partial_fraction" [] e_metID
15.12 - (["simplification","of_rationals","to_partial_fraction"],
15.13 - [("#Given" ,["functionTerm t_t", "solveFor v_v"]),
15.14 - (*("#Where" ,["((get_numerator t_t) has_degree_in v_v) <
15.15 - ((get_denominator t_t) has_degree_in v_v)"]), TODO*)
15.16 - ("#Find" ,["decomposedFunction p_p'''"])],
15.17 - {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = srls_partial_fraction, prls = e_rls,
15.18 - crls = e_rls, errpats = [], nrls = e_rls}, (*f_f = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)), zzz: z*)
15.19 - "Script PartFracScript (f_f::real) (zzz::real) = " ^(*([], Frm), Problem (Partial_Fractions, [partial_fraction, rational, simplification])*)
15.20 - "(let f_f = Take f_f; " ^(*([1], Frm), 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
15.21 - " (num_orig::real) = get_numerator f_f; " ^(* num_orig = 3*)
15.22 - " f_f = (Rewrite_Set norm_Rational False) f_f; " ^(*([1], Res), 24 / (-1 + -2 * z + 8 * z ^^^ 2)*)
15.23 - " (denom::real) = get_denominator f_f; " ^(* denom = -1 + -2 * z + 8 * z ^^^ 2*)
15.24 - " (equ::bool) = (denom = (0::real)); " ^(* equ = -1 + -2 * z + 8 * z ^^^ 2 = 0*)
15.25
15.26 - " (L_L::bool list) = (SubProblem (PolyEq', " ^(*([2], Pbl), solve (-1 + -2 * z + 8 * z ^^^ 2 = 0, z)*)
15.27 - " [abcFormula, degree_2, polynomial, univariate, equation], " ^
15.28 - " [no_met]) [BOOL equ, REAL zzz]); " ^(*([2], Res), [z = 1 / 2, z = -1 / 4]*)
15.29 - " (facs::real) = factors_from_solution L_L; " ^(* facs: (z - 1 / 2) * (z - -1 / 4)*)
15.30 - " (eql::real) = Take (num_orig / facs); " ^(*([3], Frm), 33 / ((z - 1 / 2) * (z - -1 / 4)) *)
15.31 - " (eqr::real) = (Try (Rewrite_Set ansatz_rls False)) eql; " ^(*([3], Res), ?A / (z - 1 / 2) + ?B / (z - -1 / 4)*)
15.32 - " (eq::bool) = Take (eql = eqr); " ^(*([4], Frm), 3 / ((z - 1 / 2) * (z - -1 / 4)) = ?A / (z - 1 / 2) + ?B / (z - -1 / 4)*)
15.33 - " eq = (Try (Rewrite_Set equival_trans False)) eq;" ^(*([4], Res), 3 = ?A * (z - -1 / 4) + ?B * (z - 1 / 2)*)
15.34 - " eq = drop_questionmarks eq; " ^(* eq = 3 = A * (z - -1 / 4) + B * (z - 1 / 2)*)
15.35 - " (z1::real) = (rhs (NTH 1 L_L)); " ^(* z1 = 1 / 2*)
15.36 - " (z2::real) = (rhs (NTH 2 L_L)); " ^(* z2 = -1 / 4*)
15.37 - " (eq_a::bool) = Take eq; " ^(*([5], Frm), 3 = A * (z - -1 / 4) + B * (z - 1 / 2)*)
15.38 - " eq_a = (Substitute [zzz = z1]) eq; " ^(*([5], Res), 3 = A * (1 / 2 - -1 / 4) + B * (1 / 2 - 1 / 2)*)
15.39 - " eq_a = (Rewrite_Set norm_Rational False) eq_a; " ^(*([6], Res), 3 = 3 * A / 4*)
15.40 -
15.41 - " (sol_a::bool list) = " ^(*([7], Pbl), solve (3 = 3 * A / 4, A)*)
15.42 - " (SubProblem (Isac', [univariate,equation], [no_met]) " ^
15.43 - " [BOOL eq_a, REAL (A::real)]); " ^(*([7], Res), [A = 4]*)
15.44 - " (a::real) = (rhs (NTH 1 sol_a)); " ^(* a = 4*)
15.45 - " (eq_b::bool) = Take eq; " ^(*([8], Frm), 3 = A * (z - -1 / 4) + B * (z - 1 / 2)*)
15.46 - " eq_b = (Substitute [zzz = z2]) eq_b; " ^(*([8], Res), 3 = A * (-1 / 4 - -1 / 4) + B * (-1 / 4 - 1 / 2)*)
15.47 - " eq_b = (Rewrite_Set norm_Rational False) eq_b; " ^(*([9], Res), 3 = -3 * B / 4*)
15.48 - " (sol_b::bool list) = " ^(*([10], Pbl), solve (3 = -3 * B / 4, B)*)
15.49 - " (SubProblem (Isac', [univariate,equation], [no_met]) " ^
15.50 - " [BOOL eq_b, REAL (B::real)]); " ^(*([10], Res), [B = -4]*)
15.51 - " (b::real) = (rhs (NTH 1 sol_b)); " ^(* b = -4*)
15.52 - " eqr = drop_questionmarks eqr; " ^(* eqr = A / (z - 1 / 2) + B / (z - -1 / 4)*)
15.53 - " (pbz::real) = Take eqr; " ^(*([11], Frm), A / (z - 1 / 2) + B / (z - -1 / 4)*)
15.54 - " pbz = ((Substitute [A = a, B = b]) pbz) " ^(*([11], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
15.55 - "in pbz)" (*([], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
15.56 -));
15.57 -*}
15.58 +(* current version, error outcommented *)
15.59 setup {* KEStore_Elems.add_mets
15.60 [prep_met @{theory} "met_partial_fraction" [] e_metID
15.61 (["simplification","of_rationals","to_partial_fraction"],
16.1 --- a/src/Tools/isac/Knowledge/Poly.thy Sun Feb 02 02:45:11 2014 +0100
16.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Sun Feb 02 03:09:40 2014 +0100
16.3 @@ -1603,29 +1603,7 @@
16.4 Calc ("Poly.is'_polyexp", eval_is_polyexp "")],
16.5 SOME "Simplify t_t",
16.6 [["simplification","for_polynomials"]]))] *}
16.7 -ML {*
16.8 -
16.9 (** methods **)
16.10 -
16.11 -store_met
16.12 - (prep_met thy "met_simp_poly" [] e_metID
16.13 - (["simplification","for_polynomials"],
16.14 - [("#Given" ,["Term t_t"]),
16.15 - ("#Where" ,["t_t is_polyexp"]),
16.16 - ("#Find" ,["normalform n_n"])
16.17 - ],
16.18 - {rew_ord'="tless_true",
16.19 - rls' = e_rls,
16.20 - calc = [],
16.21 - srls = e_rls,
16.22 - prls = append_rls "simplification_for_polynomials_prls" e_rls
16.23 - [(*for preds in where_*)
16.24 - Calc ("Poly.is'_polyexp",eval_is_polyexp"")],
16.25 - crls = e_rls, errpats = [], nrls = norm_Poly},
16.26 - "Script SimplifyScript (t_t::real) = " ^
16.27 - " ((Rewrite_Set norm_Poly False) t_t)"
16.28 - ));
16.29 -*}
16.30 setup {* KEStore_Elems.add_mets
16.31 [prep_met thy "met_simp_poly" [] e_metID
16.32 (["simplification","for_polynomials"],
17.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Sun Feb 02 02:45:11 2014 +0100
17.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Sun Feb 02 03:09:40 2014 +0100
17.3 @@ -975,270 +975,7 @@
17.4 " [BOOL e_e, REAL v_v]))";
17.5 parse thy scr;
17.6 *}
17.7 -ML{*
17.8 -"-------------------------methods-----------------------";
17.9 -store_met
17.10 - (prep_met thy "met_polyeq" [] e_metID
17.11 - (["PolyEq"],
17.12 - [],
17.13 - {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
17.14 - crls=PolyEq_crls, errpats = [], nrls = norm_Rational}, "empty_script"));
17.15
17.16 -store_met
17.17 - (prep_met thy "met_polyeq_norm" [] e_metID
17.18 - (["PolyEq","normalize_poly"],
17.19 - [("#Given" ,["equality e_e","solveFor v_v"]),
17.20 - ("#Where" ,["(Not((matches (?a = 0 ) e_e ))) |" ^
17.21 - "(Not(((lhs e_e) is_poly_in v_v)))"]),
17.22 - ("#Find" ,["solutions v_v'i'"])
17.23 - ],
17.24 - {rew_ord'="termlessI",
17.25 - rls'=PolyEq_erls,
17.26 - srls=e_rls,
17.27 - prls=PolyEq_prls,
17.28 - calc=[],
17.29 - crls=PolyEq_crls, errpats = [], nrls = norm_Rational},
17.30 - "Script Normalize_poly (e_e::bool) (v_v::real) = " ^
17.31 - "(let e_e =((Try (Rewrite all_left False)) @@ " ^
17.32 - " (Try (Repeat (Rewrite makex1_x False))) @@ " ^
17.33 - " (Try (Repeat (Rewrite_Set expand_binoms False))) @@ " ^
17.34 - " (Try (Repeat (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
17.35 - " make_ratpoly_in False))) @@ " ^
17.36 - " (Try (Repeat (Rewrite_Set polyeq_simplify False)))) e_e " ^
17.37 - " in (SubProblem (PolyEq',[polynomial,univariate,equation], [no_met]) " ^
17.38 - " [BOOL e_e, REAL v_v]))"
17.39 - ));
17.40 -
17.41 -*}
17.42 -ML{*
17.43 -store_met
17.44 - (prep_met thy "met_polyeq_d0" [] e_metID
17.45 - (["PolyEq","solve_d0_polyeq_equation"],
17.46 - [("#Given" ,["equality e_e","solveFor v_v"]),
17.47 - ("#Where" ,["(lhs e_e) is_poly_in v_v ",
17.48 - "((lhs e_e) has_degree_in v_v) = 0"]),
17.49 - ("#Find" ,["solutions v_v'i'"])
17.50 - ],
17.51 - {rew_ord'="termlessI",
17.52 - rls'=PolyEq_erls,
17.53 - srls=e_rls,
17.54 - prls=PolyEq_prls,
17.55 - calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))],
17.56 - crls=PolyEq_crls, errpats = [], nrls = norm_Rational},
17.57 - "Script Solve_d0_polyeq_equation (e_e::bool) (v_v::real) = " ^
17.58 - "(let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
17.59 - " d0_polyeq_simplify False))) e_e " ^
17.60 - " in ((Or_to_List e_e)::bool list))"
17.61 - ));
17.62 -*}
17.63 -ML{*
17.64 -store_met
17.65 - (prep_met thy "met_polyeq_d1" [] e_metID
17.66 - (["PolyEq","solve_d1_polyeq_equation"],
17.67 - [("#Given" ,["equality e_e","solveFor v_v"]),
17.68 - ("#Where" ,["(lhs e_e) is_poly_in v_v ",
17.69 - "((lhs e_e) has_degree_in v_v) = 1"]),
17.70 - ("#Find" ,["solutions v_v'i'"])
17.71 - ],
17.72 - {rew_ord'="termlessI", rls'=PolyEq_erls, srls=e_rls, prls=PolyEq_prls,
17.73 - calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))],
17.74 - crls=PolyEq_crls, errpats = [], nrls = norm_Rational},
17.75 - "Script Solve_d1_polyeq_equation (e_e::bool) (v_v::real) = " ^
17.76 - "(let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
17.77 - " d1_polyeq_simplify True)) @@ " ^
17.78 - " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
17.79 - " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^
17.80 - " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
17.81 - " in Check_elementwise L_L {(v_v::real). Assumptions} )"
17.82 - ));
17.83 -*}
17.84 -ML{*
17.85 -store_met
17.86 - (prep_met thy "met_polyeq_d22" [] e_metID
17.87 - (["PolyEq","solve_d2_polyeq_equation"],
17.88 - [("#Given" ,["equality e_e","solveFor v_v"]),
17.89 - ("#Where" ,["(lhs e_e) is_poly_in v_v ",
17.90 - "((lhs e_e) has_degree_in v_v) = 2"]),
17.91 - ("#Find" ,["solutions v_v'i'"])
17.92 - ],
17.93 - {rew_ord'="termlessI",
17.94 - rls'=PolyEq_erls,
17.95 - srls=e_rls,
17.96 - prls=PolyEq_prls,
17.97 - calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))],
17.98 - crls=PolyEq_crls, errpats = [], nrls = norm_Rational},
17.99 - "Script Solve_d2_polyeq_equation (e_e::bool) (v_v::real) = " ^
17.100 - " (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
17.101 - " d2_polyeq_simplify True)) @@ " ^
17.102 - " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
17.103 - " (Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
17.104 - " d1_polyeq_simplify True)) @@ " ^
17.105 - " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
17.106 - " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^
17.107 - " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
17.108 - " in Check_elementwise L_L {(v_v::real). Assumptions} )"
17.109 - ));
17.110 -*}
17.111 -ML{*
17.112 -store_met
17.113 - (prep_met thy "met_polyeq_d2_bdvonly" [] e_metID
17.114 - (["PolyEq","solve_d2_polyeq_bdvonly_equation"],
17.115 - [("#Given" ,["equality e_e","solveFor v_v"]),
17.116 - ("#Where" ,["(lhs e_e) is_poly_in v_v ",
17.117 - "((lhs e_e) has_degree_in v_v) = 2"]),
17.118 - ("#Find" ,["solutions v_v'i'"])
17.119 - ],
17.120 - {rew_ord'="termlessI",
17.121 - rls'=PolyEq_erls,
17.122 - srls=e_rls,
17.123 - prls=PolyEq_prls,
17.124 - calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))],
17.125 - crls=PolyEq_crls, errpats = [], nrls = norm_Rational},
17.126 - "Script Solve_d2_polyeq_bdvonly_equation (e_e::bool) (v_v::real) =" ^
17.127 - " (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
17.128 - " d2_polyeq_bdv_only_simplify True)) @@ " ^
17.129 - " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
17.130 - " (Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
17.131 - " d1_polyeq_simplify True)) @@ " ^
17.132 - " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
17.133 - " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^
17.134 - " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
17.135 - " in Check_elementwise L_L {(v_v::real). Assumptions} )"
17.136 - ));
17.137 -*}
17.138 -ML{*
17.139 -store_met
17.140 - (prep_met thy "met_polyeq_d2_sqonly" [] e_metID
17.141 - (["PolyEq","solve_d2_polyeq_sqonly_equation"],
17.142 - [("#Given" ,["equality e_e","solveFor v_v"]),
17.143 - ("#Where" ,["(lhs e_e) is_poly_in v_v ",
17.144 - "((lhs e_e) has_degree_in v_v) = 2"]),
17.145 - ("#Find" ,["solutions v_v'i'"])
17.146 - ],
17.147 - {rew_ord'="termlessI",
17.148 - rls'=PolyEq_erls,
17.149 - srls=e_rls,
17.150 - prls=PolyEq_prls,
17.151 - calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))],
17.152 - crls=PolyEq_crls, errpats = [], nrls = norm_Rational},
17.153 - "Script Solve_d2_polyeq_sqonly_equation (e_e::bool) (v_v::real) =" ^
17.154 - " (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
17.155 - " d2_polyeq_sq_only_simplify True)) @@ " ^
17.156 - " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
17.157 - " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e; " ^
17.158 - " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
17.159 - " in Check_elementwise L_L {(v_v::real). Assumptions} )"
17.160 - ));
17.161 -*}
17.162 -ML{*
17.163 -store_met
17.164 - (prep_met thy "met_polyeq_d2_pq" [] e_metID
17.165 - (["PolyEq","solve_d2_polyeq_pq_equation"],
17.166 - [("#Given" ,["equality e_e","solveFor v_v"]),
17.167 - ("#Where" ,["(lhs e_e) is_poly_in v_v ",
17.168 - "((lhs e_e) has_degree_in v_v) = 2"]),
17.169 - ("#Find" ,["solutions v_v'i'"])
17.170 - ],
17.171 - {rew_ord'="termlessI",
17.172 - rls'=PolyEq_erls,
17.173 - srls=e_rls,
17.174 - prls=PolyEq_prls,
17.175 - calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))],
17.176 - crls=PolyEq_crls, errpats = [], nrls = norm_Rational},
17.177 - "Script Solve_d2_polyeq_pq_equation (e_e::bool) (v_v::real) = " ^
17.178 - " (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
17.179 - " d2_polyeq_pqFormula_simplify True)) @@ " ^
17.180 - " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
17.181 - " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^
17.182 - " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
17.183 - " in Check_elementwise L_L {(v_v::real). Assumptions} )"
17.184 - ));
17.185 -*}
17.186 -ML{*
17.187 -store_met
17.188 - (prep_met thy "met_polyeq_d2_abc" [] e_metID
17.189 - (["PolyEq","solve_d2_polyeq_abc_equation"],
17.190 - [("#Given" ,["equality e_e","solveFor v_v"]),
17.191 - ("#Where" ,["(lhs e_e) is_poly_in v_v ",
17.192 - "((lhs e_e) has_degree_in v_v) = 2"]),
17.193 - ("#Find" ,["solutions v_v'i'"])
17.194 - ],
17.195 - {rew_ord'="termlessI",
17.196 - rls'=PolyEq_erls,
17.197 - srls=e_rls,
17.198 - prls=PolyEq_prls,
17.199 - calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))],
17.200 - crls=PolyEq_crls, errpats = [], nrls = norm_Rational},
17.201 - "Script Solve_d2_polyeq_abc_equation (e_e::bool) (v_v::real) = " ^
17.202 - " (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
17.203 - " d2_polyeq_abcFormula_simplify True)) @@ " ^
17.204 - " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
17.205 - " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^
17.206 - " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
17.207 - " in Check_elementwise L_L {(v_v::real). Assumptions} )"
17.208 - ));
17.209 -*}
17.210 -ML{*
17.211 -store_met
17.212 - (prep_met thy "met_polyeq_d3" [] e_metID
17.213 - (["PolyEq","solve_d3_polyeq_equation"],
17.214 - [("#Given" ,["equality e_e","solveFor v_v"]),
17.215 - ("#Where" ,["(lhs e_e) is_poly_in v_v ",
17.216 - "((lhs e_e) has_degree_in v_v) = 3"]),
17.217 - ("#Find" ,["solutions v_v'i'"])
17.218 - ],
17.219 - {rew_ord'="termlessI",
17.220 - rls'=PolyEq_erls,
17.221 - srls=e_rls,
17.222 - prls=PolyEq_prls,
17.223 - calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))],
17.224 - crls=PolyEq_crls, errpats = [], nrls = norm_Rational},
17.225 - "Script Solve_d3_polyeq_equation (e_e::bool) (v_v::real) = " ^
17.226 - " (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
17.227 - " d3_polyeq_simplify True)) @@ " ^
17.228 - " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
17.229 - " (Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
17.230 - " d2_polyeq_simplify True)) @@ " ^
17.231 - " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
17.232 - " (Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
17.233 - " d1_polyeq_simplify True)) @@ " ^
17.234 - " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
17.235 - " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^
17.236 - " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
17.237 - " in Check_elementwise L_L {(v_v::real). Assumptions} )"
17.238 - ));
17.239 -*}
17.240 -ML{*
17.241 - (*.solves all expanded (ie. normalized) terms of degree 2.*)
17.242 - (*Oct.02 restriction: 'eval_true 0 =< discriminant' ony for integer values
17.243 - by 'PolyEq_erls'; restricted until Float.thy is implemented*)
17.244 -store_met
17.245 - (prep_met thy "met_polyeq_complsq" [] e_metID
17.246 - (["PolyEq","complete_square"],
17.247 - [("#Given" ,["equality e_e","solveFor v_v"]),
17.248 - ("#Where" ,["matches (?a = 0) e_e",
17.249 - "((lhs e_e) has_degree_in v_v) = 2"]),
17.250 - ("#Find" ,["solutions v_v'i'"])
17.251 - ],
17.252 - {rew_ord'="termlessI",rls'=PolyEq_erls,srls=e_rls,prls=PolyEq_prls,
17.253 - calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))],
17.254 - crls=PolyEq_crls, errpats = [], nrls = norm_Rational},
17.255 - "Script Complete_square (e_e::bool) (v_v::real) = " ^
17.256 - "(let e_e = " ^
17.257 - " ((Try (Rewrite_Set_Inst [(bdv,v_v)] cancel_leading_coeff True)) " ^
17.258 - " @@ (Try (Rewrite_Set_Inst [(bdv,v_v)] complete_square True)) " ^
17.259 - " @@ (Try (Rewrite square_explicit1 False)) " ^
17.260 - " @@ (Try (Rewrite square_explicit2 False)) " ^
17.261 - " @@ (Rewrite root_plus_minus True) " ^
17.262 - " @@ (Try (Repeat (Rewrite_Inst [(bdv,v_v)] bdv_explicit1 False))) " ^
17.263 - " @@ (Try (Repeat (Rewrite_Inst [(bdv,v_v)] bdv_explicit2 False))) " ^
17.264 - " @@ (Try (Repeat " ^
17.265 - " (Rewrite_Inst [(bdv,v_v)] bdv_explicit3 False))) " ^
17.266 - " @@ (Try (Rewrite_Set calculate_RootRat False)) " ^
17.267 - " @@ (Try (Repeat (Calculate SQRT)))) e_e " ^
17.268 - " in ((Or_to_List e_e)::bool list))"
17.269 - ));
17.270 -*}
17.271 text {* "-------------------------methods-----------------------" *}
17.272 setup {* KEStore_Elems.add_mets
17.273 [prep_met thy "met_polyeq" [] e_metID
18.1 --- a/src/Tools/isac/Knowledge/PolyMinus.thy Sun Feb 02 02:45:11 2014 +0100
18.2 +++ b/src/Tools/isac/Knowledge/PolyMinus.thy Sun Feb 02 03:09:40 2014 +0100
18.3 @@ -474,125 +474,7 @@
18.4 Calc ("Rational.is'_ratpolyexp", eval_is_ratpolyexp "")],
18.5 SOME "Probe e_e w_w", [["probe","fuer_bruch"]]))] *}
18.6
18.7 -
18.8 -ML {*
18.9 (** methods **)
18.10 -
18.11 -store_met
18.12 - (prep_met thy "met_simp_poly_minus" [] e_metID
18.13 - (["simplification","for_polynomials","with_minus"],
18.14 - [("#Given" ,["Term t_t"]),
18.15 - ("#Where" ,["t_t is_polyexp",
18.16 - "Not (matchsub (?a + (?b + ?c)) t_t | " ^
18.17 - " matchsub (?a + (?b - ?c)) t_t | " ^
18.18 - " matchsub (?a - (?b + ?c)) t_t | " ^
18.19 - " matchsub (?a + (?b - ?c)) t_t )"]),
18.20 - ("#Find" ,["normalform n_n"])
18.21 - ],
18.22 - {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls,
18.23 - prls = append_rls "prls_met_simp_poly_minus" e_rls
18.24 - [Calc ("Poly.is'_polyexp", eval_is_polyexp ""),
18.25 - Calc ("Tools.matchsub", eval_matchsub ""),
18.26 - Thm ("and_true",num_str @{thm and_true}),
18.27 - (*"(?a & True) = ?a"*)
18.28 - Thm ("and_false",num_str @{thm and_false}),
18.29 - (*"(?a & False) = False"*)
18.30 - Thm ("not_true",num_str @{thm not_true}),
18.31 - (*"(~ True) = False"*)
18.32 - Thm ("not_false",num_str @{thm not_false})
18.33 - (*"(~ False) = True"*)],
18.34 - crls = e_rls, errpats = [], nrls = rls_p_33},
18.35 -"Script SimplifyScript (t_t::real) = " ^
18.36 -" ((Repeat((Try (Rewrite_Set ordne_alphabetisch False)) @@ " ^
18.37 -" (Try (Rewrite_Set fasse_zusammen False)) @@ " ^
18.38 -" (Try (Rewrite_Set verschoenere False)))) t_t)"
18.39 - ));
18.40 -
18.41 -store_met
18.42 - (prep_met thy "met_simp_poly_parenth" [] e_metID
18.43 - (["simplification","for_polynomials","with_parentheses"],
18.44 - [("#Given" ,["Term t_t"]),
18.45 - ("#Where" ,["t_t is_polyexp"]),
18.46 - ("#Find" ,["normalform n_n"])
18.47 - ],
18.48 - {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls,
18.49 - prls = append_rls "simplification_for_polynomials_prls" e_rls
18.50 - [(*for preds in where_*)
18.51 - Calc("Poly.is'_polyexp",eval_is_polyexp"")],
18.52 - crls = e_rls, errpats = [], nrls = rls_p_34},
18.53 -"Script SimplifyScript (t_t::real) = " ^
18.54 -" ((Repeat((Try (Rewrite_Set klammern_aufloesen False)) @@ " ^
18.55 -" (Try (Rewrite_Set ordne_alphabetisch False)) @@ " ^
18.56 -" (Try (Rewrite_Set fasse_zusammen False)) @@ " ^
18.57 -" (Try (Rewrite_Set verschoenere False)))) t_t)"
18.58 - ));
18.59 -
18.60 -store_met
18.61 - (prep_met thy "met_simp_poly_parenth_mult" [] e_metID
18.62 - (["simplification","for_polynomials","with_parentheses_mult"],
18.63 - [("#Given" ,["Term t_t"]),
18.64 - ("#Where" ,["t_t is_polyexp"]),
18.65 - ("#Find" ,["normalform n_n"])
18.66 - ],
18.67 - {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls,
18.68 - prls = append_rls "simplification_for_polynomials_prls" e_rls
18.69 - [(*for preds in where_*)
18.70 - Calc("Poly.is'_polyexp",eval_is_polyexp"")],
18.71 - crls = e_rls, errpats = [], nrls = rls_p_34},
18.72 -"Script SimplifyScript (t_t::real) = " ^
18.73 -" ((Repeat((Try (Rewrite_Set klammern_ausmultiplizieren False)) @@ " ^
18.74 -" (Try (Rewrite_Set discard_parentheses False)) @@ " ^
18.75 -" (Try (Rewrite_Set ordne_monome False)) @@ " ^
18.76 -" (Try (Rewrite_Set klammern_aufloesen False)) @@ " ^
18.77 -" (Try (Rewrite_Set ordne_alphabetisch False)) @@ " ^
18.78 -" (Try (Rewrite_Set fasse_zusammen False)) @@ " ^
18.79 -" (Try (Rewrite_Set verschoenere False)))) t_t)"
18.80 - ));
18.81 -
18.82 -store_met
18.83 - (prep_met thy "met_probe" [] e_metID
18.84 - (["probe"],
18.85 - [],
18.86 - {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls,
18.87 - prls = Erls, crls = e_rls, errpats = [], nrls = Erls},
18.88 - "empty_script"));
18.89 -
18.90 -store_met
18.91 - (prep_met thy "met_probe_poly" [] e_metID
18.92 - (["probe","fuer_polynom"],
18.93 - [("#Given" ,["Pruefe e_e", "mitWert w_w"]),
18.94 - ("#Where" ,["e_e is_polyexp"]),
18.95 - ("#Find" ,["Geprueft p_p"])
18.96 - ],
18.97 - {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls,
18.98 - prls = append_rls "prls_met_probe_bruch"
18.99 - e_rls [(*for preds in where_*)
18.100 - Calc ("Rational.is'_ratpolyexp",
18.101 - eval_is_ratpolyexp "")],
18.102 - crls = e_rls, errpats = [], nrls = rechnen},
18.103 -"Script ProbeScript (e_e::bool) (w_w::bool list) = " ^
18.104 -" (let e_e = Take e_e; " ^
18.105 -" e_e = Substitute w_w e_e " ^
18.106 -" in (Repeat((Try (Repeat (Calculate TIMES))) @@ " ^
18.107 -" (Try (Repeat (Calculate PLUS ))) @@ " ^
18.108 -" (Try (Repeat (Calculate MINUS))))) e_e)"
18.109 -));
18.110 -
18.111 -store_met
18.112 - (prep_met thy "met_probe_bruch" [] e_metID
18.113 - (["probe","fuer_bruch"],
18.114 - [("#Given" ,["Pruefe e_e", "mitWert w_w"]),
18.115 - ("#Where" ,["e_e is_ratpolyexp"]),
18.116 - ("#Find" ,["Geprueft p_p"])
18.117 - ],
18.118 - {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls,
18.119 - prls = append_rls "prls_met_probe_bruch"
18.120 - e_rls [(*for preds in where_*)
18.121 - Calc ("Rational.is'_ratpolyexp",
18.122 - eval_is_ratpolyexp "")],
18.123 - crls = e_rls, errpats = [], nrls = Erls},
18.124 - "empty_script"));
18.125 -*}
18.126 setup {* KEStore_Elems.add_mets
18.127 [prep_met thy "met_simp_poly_minus" [] e_metID
18.128 (["simplification","for_polynomials","with_minus"],
19.1 --- a/src/Tools/isac/Knowledge/RatEq.thy Sun Feb 02 02:45:11 2014 +0100
19.2 +++ b/src/Tools/isac/Knowledge/RatEq.thy Sun Feb 02 03:09:40 2014 +0100
19.3 @@ -191,40 +191,6 @@
19.4 ("#Find", ["solutions v_v'i'"])],
19.5 RatEq_prls, SOME "solve (e_e::bool, v_v)", [["RatEq","solve_rat_equation"]]))] *}
19.6
19.7 -ML {*
19.8 -(*-------------------------methods-----------------------*)
19.9 -store_met
19.10 - (prep_met thy "met_rateq" [] e_metID
19.11 - (["RatEq"],
19.12 - [],
19.13 - {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
19.14 - crls=RatEq_crls, errpats = [], nrls = norm_Rational}, "empty_script"));
19.15 -*}
19.16 -
19.17 -ML {*
19.18 -store_met
19.19 - (prep_met thy "met_rat_eq" [] e_metID
19.20 - (["RatEq", "solve_rat_equation"],
19.21 - [("#Given" ,["equality e_e","solveFor v_v"]),
19.22 - ("#Where" ,["(e_e::bool) is_ratequation_in (v_v::real)"]),
19.23 - ("#Find" ,["solutions v_v'i'"])
19.24 - ],
19.25 - {rew_ord'="termlessI",
19.26 - rls'=rateq_erls,
19.27 - srls=e_rls,
19.28 - prls=RatEq_prls,
19.29 - calc=[],
19.30 - crls=RatEq_crls, errpats = [], nrls = norm_Rational},
19.31 - "Script Solve_rat_equation (e_e::bool) (v_v::real) = " ^
19.32 - "(let e_e = ((Repeat(Try (Rewrite_Set RatEq_simplify True))) @@ " ^
19.33 - " (Repeat(Try (Rewrite_Set norm_Rational False))) @@ " ^
19.34 - " (Repeat(Try (Rewrite_Set add_fractions_p False))) @@ " ^
19.35 - " (Repeat(Try (Rewrite_Set RatEq_eliminate True)))) e_e;" ^
19.36 - " (L_L::bool list) = (SubProblem (RatEq',[univariate,equation], [no_met])" ^
19.37 - " [BOOL e_e, REAL v_v]) " ^
19.38 - " in Check_elementwise L_L {(v_v::real). Assumptions})"
19.39 - ));
19.40 -*}
19.41 (*-------------------------methods-----------------------*)
19.42 setup {* KEStore_Elems.add_mets
19.43 [prep_met thy "met_rateq" [] e_metID
20.1 --- a/src/Tools/isac/Knowledge/Rational.thy Sun Feb 02 02:45:11 2014 +0100
20.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Sun Feb 02 03:09:40 2014 +0100
20.3 @@ -894,32 +894,6 @@
20.4 SOME "Simplify t_t", [["simplification","of_rationals"]]))] *}
20.5
20.6 section {* A methods for simplification of rationals *}
20.7 -ML {*
20.8 -(*WN061025 this methods script is copied from (auto-generated) script
20.9 - of norm_Rational in order to ease repair on inform*)
20.10 -store_met (prep_met thy "met_simp_rat" [] e_metID (["simplification","of_rationals"],
20.11 - [("#Given" ,["Term t_t"]),
20.12 - ("#Where" ,["t_t is_ratpolyexp"]),
20.13 - ("#Find" ,["normalform n_n"])],
20.14 - {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls,
20.15 - prls = append_rls "simplification_of_rationals_prls" e_rls
20.16 - [(*for preds in where_*) Calc ("Rational.is'_ratpolyexp", eval_is_ratpolyexp "")],
20.17 - crls = e_rls, errpats = [],
20.18 - nrls = norm_Rational_rls},
20.19 - "Script SimplifyScript (t_t::real) = " ^
20.20 - " ((Try (Rewrite_Set discard_minus False) @@ " ^
20.21 - " Try (Rewrite_Set rat_mult_poly False) @@ " ^
20.22 - " Try (Rewrite_Set make_rat_poly_with_parentheses False) @@ " ^
20.23 - " Try (Rewrite_Set cancel_p_rls False) @@ " ^
20.24 - " (Repeat " ^
20.25 - " ((Try (Rewrite_Set add_fractions_p_rls False) @@ " ^
20.26 - " Try (Rewrite_Set rat_mult_div_pow False) @@ " ^
20.27 - " Try (Rewrite_Set make_rat_poly_with_parentheses False) @@" ^
20.28 - " Try (Rewrite_Set cancel_p_rls False) @@ " ^
20.29 - " Try (Rewrite_Set rat_reduce_1 False)))) @@ " ^
20.30 - " Try (Rewrite_Set discard_parentheses1 False)) " ^
20.31 - " t_t)"));
20.32 -*}
20.33 (*WN061025 this methods script is copied from (auto-generated) script
20.34 of norm_Rational in order to ease repair on inform*)
20.35 setup {* KEStore_Elems.add_mets
21.1 --- a/src/Tools/isac/Knowledge/RootEq.thy Sun Feb 02 02:45:11 2014 +0100
21.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy Sun Feb 02 03:09:40 2014 +0100
21.3 @@ -516,127 +516,7 @@
21.4 ("#Find" ,["solutions v_v'i'"])],
21.5 RootEq_prls, SOME "solve (e_e::bool, v_v)", [["RootEq","norm_sq_root_equation"]]))] *}
21.6
21.7 -ML {*
21.8 -(*-------------------------methods-----------------------*)
21.9 -(* ---- root 20.8.02 ---*)
21.10 -store_met
21.11 - (prep_met thy "met_rooteq" [] e_metID
21.12 - (["RootEq"],
21.13 - [],
21.14 - {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
21.15 - crls=RootEq_crls, errpats = [], nrls = norm_Poly}, "empty_script"));
21.16
21.17 -(*-- normalize 20.10.02 --*)
21.18 -store_met
21.19 - (prep_met thy "met_rooteq_norm" [] e_metID
21.20 - (["RootEq","norm_sq_root_equation"],
21.21 - [("#Given" ,["equality e_e","solveFor v_v"]),
21.22 - ("#Where" ,["( ((lhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
21.23 - " Not((lhs e_e) is_normSqrtTerm_in (v_v::real))) | " ^
21.24 - "( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
21.25 - " Not((rhs e_e) is_normSqrtTerm_in (v_v::real)))"]),
21.26 - ("#Find" ,["solutions v_v'i'"])
21.27 - ],
21.28 - {rew_ord'="termlessI", rls'=RootEq_erls, srls=e_rls, prls=RootEq_prls,
21.29 - calc=[], crls=RootEq_crls, errpats = [], nrls = norm_Poly},
21.30 - "Script Norm_sq_root_equation (e_e::bool) (v_v::real) = " ^
21.31 - "(let e_e = ((Repeat(Try (Rewrite makex1_x False))) @@ " ^
21.32 - " (Try (Repeat (Rewrite_Set expand_rootbinoms False))) @@ " ^
21.33 - " (Try (Rewrite_Set rooteq_simplify True)) @@ " ^
21.34 - " (Try (Repeat (Rewrite_Set make_rooteq False))) @@ " ^
21.35 - " (Try (Rewrite_Set rooteq_simplify True))) e_e " ^
21.36 - " in ((SubProblem (RootEq',[univariate,equation], " ^
21.37 - " [no_met]) [BOOL e_e, REAL v_v])))"
21.38 - ));
21.39 -
21.40 -*}
21.41 -
21.42 -ML {*
21.43 -val -------------------------------------------------- = "00000";
21.44 -store_met
21.45 - (prep_met thy "met_rooteq_sq" [] e_metID
21.46 - (["RootEq","solve_sq_root_equation"],
21.47 - [("#Given" ,["equality e_e", "solveFor v_v"]),
21.48 - ("#Where" ,["(((lhs e_e) is_sqrtTerm_in (v_v::real)) & " ^
21.49 - " ((lhs e_e) is_normSqrtTerm_in (v_v::real))) |" ^
21.50 - "(((rhs e_e) is_sqrtTerm_in (v_v::real)) & " ^
21.51 - " ((rhs e_e) is_normSqrtTerm_in (v_v::real)))"]),
21.52 - ("#Find" ,["solutions v_v'i'"])
21.53 - ],
21.54 - {rew_ord'="termlessI", rls'=RootEq_erls, srls = rooteq_srls,
21.55 - prls = RootEq_prls, calc = [], crls=RootEq_crls, errpats = [], nrls = norm_Poly},
21.56 -"Script Solve_sq_root_equation (e_e::bool) (v_v::real) = " ^
21.57 -"(let e_e = " ^
21.58 -" ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] sqrt_isolate True)) @@ " ^
21.59 -" (Try (Rewrite_Set rooteq_simplify True)) @@ " ^
21.60 -" (Try (Repeat (Rewrite_Set expand_rootbinoms False))) @@ " ^
21.61 -" (Try (Repeat (Rewrite_Set make_rooteq False))) @@ " ^
21.62 -" (Try (Rewrite_Set rooteq_simplify True)) ) e_e; " ^
21.63 -" (L_L::bool list) = " ^
21.64 -" (if (((lhs e_e) is_sqrtTerm_in v_v) | ((rhs e_e) is_sqrtTerm_in v_v))" ^
21.65 -" then (SubProblem (RootEq',[normalize,root',univariate,equation], " ^
21.66 -" [no_met]) [BOOL e_e, REAL v_v]) " ^
21.67 -" else (SubProblem (RootEq',[univariate,equation], [no_met]) " ^
21.68 -" [BOOL e_e, REAL v_v])) " ^
21.69 -"in Check_elementwise L_L {(v_v::real). Assumptions})"
21.70 - ));
21.71 -*}
21.72 -
21.73 -ML {*
21.74 -(*-- right 28.08.02 --*)
21.75 -store_met
21.76 - (prep_met thy "met_rooteq_sq_right" [] e_metID
21.77 - (["RootEq","solve_right_sq_root_equation"],
21.78 - [("#Given" ,["equality e_e","solveFor v_v"]),
21.79 - ("#Where" ,["(rhs e_e) is_sqrtTerm_in v_v"]),
21.80 - ("#Find" ,["solutions v_v'i'"])
21.81 - ],
21.82 - {rew_ord' = "termlessI", rls' = RootEq_erls, srls = e_rls,
21.83 - prls = RootEq_prls, calc = [], crls = RootEq_crls, errpats = [], nrls = norm_Poly},
21.84 - "Script Solve_right_sq_root_equation (e_e::bool) (v_v::real) = " ^
21.85 - "(let e_e = " ^
21.86 - " ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] r_sqrt_isolate False)) @@ " ^
21.87 - " (Try (Rewrite_Set rooteq_simplify False)) @@ " ^
21.88 - " (Try (Repeat (Rewrite_Set expand_rootbinoms False))) @@ " ^
21.89 - " (Try (Repeat (Rewrite_Set make_rooteq False))) @@ " ^
21.90 - " (Try (Rewrite_Set rooteq_simplify False))) e_e " ^
21.91 - " in if ((rhs e_e) is_sqrtTerm_in v_v) " ^
21.92 - " then (SubProblem (RootEq',[normalize,root',univariate,equation], " ^
21.93 - " [no_met]) [BOOL e_e, REAL v_v]) " ^
21.94 - " else ((SubProblem (RootEq',[univariate,equation], " ^
21.95 - " [no_met]) [BOOL e_e, REAL v_v])))"
21.96 - ));
21.97 -val --------------------------------------------------+++ = "33333";
21.98 -
21.99 -(*-- left 28.08.02 --*)
21.100 -store_met
21.101 - (prep_met thy "met_rooteq_sq_left" [] e_metID
21.102 - (["RootEq","solve_left_sq_root_equation"],
21.103 - [("#Given" ,["equality e_e","solveFor v_v"]),
21.104 - ("#Where" ,["(lhs e_e) is_sqrtTerm_in v_v"]),
21.105 - ("#Find" ,["solutions v_v'i'"])
21.106 - ],
21.107 - {rew_ord'="termlessI",
21.108 - rls'=RootEq_erls,
21.109 - srls=e_rls,
21.110 - prls=RootEq_prls,
21.111 - calc=[],
21.112 - crls=RootEq_crls, errpats = [], nrls = norm_Poly},
21.113 - "Script Solve_left_sq_root_equation (e_e::bool) (v_v::real) = " ^
21.114 - "(let e_e = " ^
21.115 - " ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] l_sqrt_isolate False)) @@ " ^
21.116 - " (Try (Rewrite_Set rooteq_simplify False)) @@ " ^
21.117 - " (Try (Repeat (Rewrite_Set expand_rootbinoms False))) @@ " ^
21.118 - " (Try (Repeat (Rewrite_Set make_rooteq False))) @@ " ^
21.119 - " (Try (Rewrite_Set rooteq_simplify False))) e_e " ^
21.120 - " in if ((lhs e_e) is_sqrtTerm_in v_v) " ^
21.121 - " then (SubProblem (RootEq',[normalize,root',univariate,equation], " ^
21.122 - " [no_met]) [BOOL e_e, REAL v_v]) " ^
21.123 - " else ((SubProblem (RootEq',[univariate,equation], " ^
21.124 - " [no_met]) [BOOL e_e, REAL v_v])))"
21.125 - ));
21.126 -val --------------------------------------------------++++ = "44444";
21.127 -*}
21.128 (*-------------------------methods-----------------------*)
21.129 setup {* KEStore_Elems.add_mets
21.130 [(* ---- root 20.8.02 ---*)
22.1 --- a/src/Tools/isac/Knowledge/RootRatEq.thy Sun Feb 02 02:45:11 2014 +0100
22.2 +++ b/src/Tools/isac/Knowledge/RootRatEq.thy Sun Feb 02 03:09:40 2014 +0100
22.3 @@ -147,40 +147,7 @@
22.4 "( (rhs e_e) is_rootRatAddTerm_in (v_v::real) )"]),
22.5 ("#Find" ,["solutions v_v'i'"])],
22.6 RootRatEq_prls, SOME "solve (e_e::bool, v_v)", [["RootRatEq","elim_rootrat_equation"]]))] *}
22.7 -ML {*
22.8 -(*-------------------------Methode-----------------------*)
22.9 -store_met
22.10 - (prep_met @{theory LinEq} "met_rootrateq" [] e_metID
22.11 - (["RootRatEq"],
22.12 - [],
22.13 - {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
22.14 - crls=Atools_erls, errpats = [], nrls = norm_Rational}, "empty_script"));
22.15 -(*-- left 20.10.02 --*)
22.16 -store_met
22.17 - (prep_met thy "met_rootrateq_elim" [] e_metID
22.18 - (["RootRatEq","elim_rootrat_equation"],
22.19 - [("#Given" ,["equality e_e","solveFor v_v"]),
22.20 - ("#Where" ,["( (lhs e_e) is_rootRatAddTerm_in (v_v::real) ) | " ^
22.21 - "( (rhs e_e) is_rootRatAddTerm_in (v_v::real) )"]),
22.22 - ("#Find" ,["solutions v_v'i'"])
22.23 - ],
22.24 - {rew_ord'="termlessI",
22.25 - rls'=RooRatEq_erls,
22.26 - srls=e_rls,
22.27 - prls=RootRatEq_prls,
22.28 - calc=[],
22.29 - crls=RootRatEq_crls, errpats = [], nrls = norm_Rational},
22.30 - "Script Elim_rootrat_equation (e_e::bool) (v_v::real) = " ^
22.31 - "(let e_e = ((Try (Rewrite_Set expand_rootbinoms False)) @@ " ^
22.32 - " (Try (Rewrite_Set rooteq_simplify False)) @@ " ^
22.33 - " (Try (Rewrite_Set make_rooteq False)) @@ " ^
22.34 - " (Try (Rewrite_Set rooteq_simplify False)) @@ " ^
22.35 - " (Try (Rewrite_Set_Inst [(bdv,v_v)] " ^
22.36 - " rootrat_solve False))) e_e " ^
22.37 - " in (SubProblem (RootEq',[univariate,equation], " ^
22.38 - " [no_met]) [BOOL e_e, REAL v_v]))"
22.39 - ));
22.40 -*}
22.41 +
22.42 (*-------------------------Methode-----------------------*)
22.43 setup {* KEStore_Elems.add_mets
22.44 [prep_met @{theory LinEq} "met_rootrateq" [] e_metID
23.1 --- a/src/Tools/isac/Knowledge/Simplify.thy Sun Feb 02 02:45:11 2014 +0100
23.2 +++ b/src/Tools/isac/Knowledge/Simplify.thy Sun Feb 02 03:09:40 2014 +0100
23.3 @@ -42,20 +42,8 @@
23.4 ML {*
23.5 @{thm mult_commute}
23.6 *}
23.7 -ML {*
23.8
23.9 (** methods **)
23.10 -
23.11 -store_met
23.12 - (prep_met thy "met_tsimp" [] e_metID
23.13 - (["simplification"],
23.14 - [("#Given" ,["Term t_t"]),
23.15 - ("#Find" ,["normalform n_n"])],
23.16 - {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls=e_rls,
23.17 - crls = e_rls, errpats = [], nrls = e_rls},
23.18 - "empty_script"));
23.19 -*}
23.20 -(** methods **)
23.21 setup {* KEStore_Elems.add_mets
23.22 [prep_met thy "met_tsimp" [] e_metID
23.23 (["simplification"],
24.1 --- a/src/Tools/isac/Knowledge/Test.thy Sun Feb 02 02:45:11 2014 +0100
24.2 +++ b/src/Tools/isac/Knowledge/Test.thy Sun Feb 02 03:09:40 2014 +0100
24.3 @@ -546,50 +546,6 @@
24.4
24.5 ------ 25.8.01*)
24.6
24.7 -ML {*
24.8 -(** methods **)
24.9 -store_met
24.10 - (prep_met @{theory "Diff"} "met_test" [] e_metID
24.11 - (["Test"],
24.12 - [],
24.13 - {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
24.14 - crls=Atools_erls, errpats = [], nrls = e_rls}, "empty_script"));
24.15 -*}
24.16 -ML {*
24.17 -store_met
24.18 - (prep_met thy "met_test_solvelin" [] e_metID
24.19 - (["Test","solve_linear"]:metID,
24.20 - [("#Given" ,["equality e_e","solveFor v_v"]),
24.21 - ("#Where" ,["matches (?a = ?b) e_e"]),
24.22 - ("#Find" ,["solutions v_v'i'"])
24.23 - ],
24.24 - {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = e_rls,
24.25 - prls = assoc_rls' @{theory} "matches", calc = [], crls = tval_rls,
24.26 - errpats = [], nrls = Test_simplify},
24.27 - "Script Solve_linear (e_e::bool) (v_v::real)= " ^
24.28 - "(let e_e = " ^
24.29 - " Repeat " ^
24.30 - " (((Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@ " ^
24.31 - " (Rewrite_Set Test_simplify False))) e_e" ^
24.32 - " in [e_e::bool])"
24.33 - )
24.34 -(*, prep_met thy (*test for equations*)
24.35 - (["Test","testeq"]:metID,
24.36 - [("#Given" ,["boolTestGiven g_g"]),
24.37 - ("#Find" ,["boolTestFind f_f"])
24.38 - ],
24.39 - {rew_ord'="e_rew_ord",rls'="tval_rls",asm_rls=[],
24.40 - asm_thm=[("square_equation_left","")]},
24.41 - "Script Testeq (e_q::bool) = " ^
24.42 - "Repeat " ^
24.43 - " (let e_e = Try (Repeat (Rewrite rroot_square_inv False e_q)); " ^
24.44 - " e_e = Try (Repeat (Rewrite square_equation_left True e_e)); " ^
24.45 - " e_e = Try (Repeat (Rewrite rmult_0 False e_e)) " ^
24.46 - " in e_e) Until (is_root_free e_e)" (*deleted*)
24.47 - )
24.48 -, ---------27.4.02*)
24.49 -);
24.50 -*}
24.51 (** methods **)
24.52 setup {* KEStore_Elems.add_mets
24.53 [prep_met @{theory "Diff"} "met_test" [] e_metID
24.54 @@ -854,314 +810,6 @@
24.55 get_pbt ["inttype","test"];
24.56 *)
24.57
24.58 -ML {*
24.59 -store_met
24.60 - (prep_met thy "met_test_sqrt" [] e_metID
24.61 -(*root-equation, version for tests before 8.01.01*)
24.62 - (["Test","sqrt-equ-test"]:metID,
24.63 - [("#Given" ,["equality e_e","solveFor v_v"]),
24.64 - ("#Where" ,["contains_root (e_e::bool)"]),
24.65 - ("#Find" ,["solutions v_v'i'"])
24.66 - ],
24.67 - {rew_ord'="e_rew_ord",rls'=tval_rls,
24.68 - srls =append_rls "srls_contains_root" e_rls
24.69 - [Calc ("Test.contains'_root",eval_contains_root "")],
24.70 - prls =append_rls "prls_contains_root" e_rls
24.71 - [Calc ("Test.contains'_root",eval_contains_root "")],
24.72 - calc=[],
24.73 - crls=tval_rls, errpats = [], nrls = e_rls(*,asm_rls=[],
24.74 - asm_thm=[("square_equation_left",""),
24.75 - ("square_equation_right","")]*)},
24.76 - "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
24.77 - "(let e_e = " ^
24.78 - " ((While (contains_root e_e) Do" ^
24.79 - " ((Rewrite square_equation_left True) @@" ^
24.80 - " (Try (Rewrite_Set Test_simplify False)) @@" ^
24.81 - " (Try (Rewrite_Set rearrange_assoc False)) @@" ^
24.82 - " (Try (Rewrite_Set isolate_root False)) @@" ^
24.83 - " (Try (Rewrite_Set Test_simplify False)))) @@" ^
24.84 - " (Try (Rewrite_Set norm_equation False)) @@" ^
24.85 - " (Try (Rewrite_Set Test_simplify False)) @@" ^
24.86 - " (Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@" ^
24.87 - " (Try (Rewrite_Set Test_simplify False)))" ^
24.88 - " e_e" ^
24.89 - " in [e_e::bool])"
24.90 - ));
24.91 -
24.92 -*}
24.93 -ML {*
24.94 -store_met
24.95 - (prep_met thy "met_test_sqrt2" [] e_metID
24.96 -(*root-equation ... for test-*.sml until 8.01*)
24.97 - (["Test","squ-equ-test2"]:metID,
24.98 - [("#Given" ,["equality e_e","solveFor v_v"]),
24.99 - ("#Find" ,["solutions v_v'i'"])
24.100 - ],
24.101 - {rew_ord'="e_rew_ord",rls'=tval_rls,
24.102 - srls = append_rls "srls_contains_root" e_rls
24.103 - [Calc ("Test.contains'_root",eval_contains_root"")],
24.104 - prls=e_rls,calc=[],
24.105 - crls=tval_rls, errpats = [], nrls = e_rls(*,asm_rls=[],
24.106 - asm_thm=[("square_equation_left",""),
24.107 - ("square_equation_right","")]*)},
24.108 - "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
24.109 - "(let e_e = " ^
24.110 - " ((While (contains_root e_e) Do" ^
24.111 - " ((Rewrite square_equation_left True) @@" ^
24.112 - " (Try (Rewrite_Set Test_simplify False)) @@" ^
24.113 - " (Try (Rewrite_Set rearrange_assoc False)) @@" ^
24.114 - " (Try (Rewrite_Set isolate_root False)) @@" ^
24.115 - " (Try (Rewrite_Set Test_simplify False)))) @@" ^
24.116 - " (Try (Rewrite_Set norm_equation False)) @@" ^
24.117 - " (Try (Rewrite_Set Test_simplify False)) @@" ^
24.118 - " (Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@" ^
24.119 - " (Try (Rewrite_Set Test_simplify False)))" ^
24.120 - " e_e;" ^
24.121 - " (L_L::bool list) = Tac subproblem_equation_dummy; " ^
24.122 - " L_L = Tac solve_equation_dummy " ^
24.123 - " in Check_elementwise L_L {(v_v::real). Assumptions})"
24.124 - ));
24.125 -
24.126 -*}
24.127 -ML {*
24.128 -store_met
24.129 - (prep_met thy "met_test_squ_sub" [] e_metID
24.130 -(*tests subproblem fixed linear*)
24.131 - (["Test","squ-equ-test-subpbl1"]:metID,
24.132 - [("#Given" ,["equality e_e","solveFor v_v"]),
24.133 - ("#Where" ,["precond_rootmet v_v"]),
24.134 - ("#Find" ,["solutions v_v'i'"])
24.135 - ],
24.136 - {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = e_rls,
24.137 - prls = append_rls "prls_met_test_squ_sub" e_rls
24.138 - [Calc ("Test.precond'_rootmet", eval_precond_rootmet "")],
24.139 - calc=[], crls=tval_rls, errpats = [], nrls = Test_simplify},
24.140 - "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
24.141 - " (let e_e = ((Try (Rewrite_Set norm_equation False)) @@ " ^
24.142 - " (Try (Rewrite_Set Test_simplify False))) e_e; " ^
24.143 - " (L_L::bool list) = " ^
24.144 - " (SubProblem (Test', " ^
24.145 - " [LINEAR,univariate,equation,test]," ^
24.146 - " [Test,solve_linear]) " ^
24.147 - " [BOOL e_e, REAL v_v]) " ^
24.148 - " in Check_elementwise L_L {(v_v::real). Assumptions}) "
24.149 - ));
24.150 -
24.151 -*}
24.152 -ML {*
24.153 -store_met
24.154 - (prep_met thy "met_test_squ_sub2" [] e_metID
24.155 - (*tests subproblem fixed degree 2*)
24.156 - (["Test","squ-equ-test-subpbl2"]:metID,
24.157 - [("#Given" ,["equality e_e","solveFor v_v"]),
24.158 - ("#Find" ,["solutions v_v'i'"])
24.159 - ],
24.160 - {rew_ord'="e_rew_ord",rls'=tval_rls,srls=e_rls,prls=e_rls,calc=[],
24.161 - crls=tval_rls, errpats = [], nrls = e_rls(*,
24.162 - asm_rls=[],asm_thm=[("square_equation_left",""),
24.163 - ("square_equation_right","")]*)},
24.164 - "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
24.165 - " (let e_e = Try (Rewrite_Set norm_equation False) e_e; " ^
24.166 - "(L_L::bool list) = (SubProblem (Test',[LINEAR,univariate,equation,test]," ^
24.167 - " [Test,solve_by_pq_formula]) [BOOL e_e, REAL v_v])" ^
24.168 - "in Check_elementwise L_L {(v_v::real). Assumptions})"
24.169 - ));
24.170 -
24.171 -*}
24.172 -ML {*
24.173 -store_met
24.174 - (prep_met thy "met_test_squ_nonterm" [] e_metID
24.175 - (*root-equation: see foils..., but notTerminating*)
24.176 - (["Test","square_equation...notTerminating"]:metID,
24.177 - [("#Given" ,["equality e_e","solveFor v_v"]),
24.178 - ("#Find" ,["solutions v_v'i'"])
24.179 - ],
24.180 - {rew_ord'="e_rew_ord",rls'=tval_rls,
24.181 - srls = append_rls "srls_contains_root" e_rls
24.182 - [Calc ("Test.contains'_root",eval_contains_root"")],
24.183 - prls=e_rls,calc=[],
24.184 - crls=tval_rls, errpats = [], nrls = e_rls(*,asm_rls=[],
24.185 - asm_thm=[("square_equation_left",""),
24.186 - ("square_equation_right","")]*)},
24.187 - "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
24.188 - "(let e_e = " ^
24.189 - " ((While (contains_root e_e) Do" ^
24.190 - " ((Rewrite square_equation_left True) @@" ^
24.191 - " (Try (Rewrite_Set Test_simplify False)) @@" ^
24.192 - " (Try (Rewrite_Set rearrange_assoc False)) @@" ^
24.193 - " (Try (Rewrite_Set isolate_root False)) @@" ^
24.194 - " (Try (Rewrite_Set Test_simplify False)))) @@" ^
24.195 - " (Try (Rewrite_Set norm_equation False)) @@" ^
24.196 - " (Try (Rewrite_Set Test_simplify False)))" ^
24.197 - " e_e;" ^
24.198 - " (L_L::bool list) = " ^
24.199 - " (SubProblem (Test',[LINEAR,univariate,equation,test]," ^
24.200 - " [Test,solve_linear]) [BOOL e_e, REAL v_v])" ^
24.201 - "in Check_elementwise L_L {(v_v::real). Assumptions})"
24.202 - ));
24.203 -
24.204 -*}
24.205 -ML {*
24.206 -store_met
24.207 - (prep_met thy "met_test_eq1" [] e_metID
24.208 -(*root-equation1:*)
24.209 - (["Test","square_equation1"]:metID,
24.210 - [("#Given" ,["equality e_e","solveFor v_v"]),
24.211 - ("#Find" ,["solutions v_v'i'"])
24.212 - ],
24.213 - {rew_ord'="e_rew_ord",rls'=tval_rls,
24.214 - srls = append_rls "srls_contains_root" e_rls
24.215 - [Calc ("Test.contains'_root",eval_contains_root"")],
24.216 - prls=e_rls,calc=[],
24.217 - crls=tval_rls, errpats = [], nrls = e_rls(*,asm_rls=[],
24.218 - asm_thm=[("square_equation_left",""),
24.219 - ("square_equation_right","")]*)},
24.220 - "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
24.221 - "(let e_e = " ^
24.222 - " ((While (contains_root e_e) Do" ^
24.223 - " ((Rewrite square_equation_left True) @@" ^
24.224 - " (Try (Rewrite_Set Test_simplify False)) @@" ^
24.225 - " (Try (Rewrite_Set rearrange_assoc False)) @@" ^
24.226 - " (Try (Rewrite_Set isolate_root False)) @@" ^
24.227 - " (Try (Rewrite_Set Test_simplify False)))) @@" ^
24.228 - " (Try (Rewrite_Set norm_equation False)) @@" ^
24.229 - " (Try (Rewrite_Set Test_simplify False)))" ^
24.230 - " e_e;" ^
24.231 - " (L_L::bool list) = (SubProblem (Test',[LINEAR,univariate,equation,test]," ^
24.232 - " [Test,solve_linear]) [BOOL e_e, REAL v_v])" ^
24.233 - " in Check_elementwise L_L {(v_v::real). Assumptions})"
24.234 - ));
24.235 -
24.236 -*}
24.237 -ML {*
24.238 -store_met
24.239 - (prep_met thy "met_test_squ2" [] e_metID
24.240 - (*root-equation2*)
24.241 - (["Test","square_equation2"]:metID,
24.242 - [("#Given" ,["equality e_e","solveFor v_v"]),
24.243 - ("#Find" ,["solutions v_v'i'"])
24.244 - ],
24.245 - {rew_ord'="e_rew_ord",rls'=tval_rls,
24.246 - srls = append_rls "srls_contains_root" e_rls
24.247 - [Calc ("Test.contains'_root",eval_contains_root"")],
24.248 - prls=e_rls,calc=[],
24.249 - crls=tval_rls, errpats = [], nrls = e_rls(*,asm_rls=[],
24.250 - asm_thm=[("square_equation_left",""),
24.251 - ("square_equation_right","")]*)},
24.252 - "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
24.253 - "(let e_e = " ^
24.254 - " ((While (contains_root e_e) Do" ^
24.255 - " (((Rewrite square_equation_left True) Or " ^
24.256 - " (Rewrite square_equation_right True)) @@" ^
24.257 - " (Try (Rewrite_Set Test_simplify False)) @@" ^
24.258 - " (Try (Rewrite_Set rearrange_assoc False)) @@" ^
24.259 - " (Try (Rewrite_Set isolate_root False)) @@" ^
24.260 - " (Try (Rewrite_Set Test_simplify False)))) @@" ^
24.261 - " (Try (Rewrite_Set norm_equation False)) @@" ^
24.262 - " (Try (Rewrite_Set Test_simplify False)))" ^
24.263 - " e_e;" ^
24.264 - " (L_L::bool list) = (SubProblem (Test',[plain_square,univariate,equation,test]," ^
24.265 - " [Test,solve_plain_square]) [BOOL e_e, REAL v_v])" ^
24.266 - " in Check_elementwise L_L {(v_v::real). Assumptions})"
24.267 - ));
24.268 -
24.269 -*}
24.270 -ML {*
24.271 -store_met
24.272 - (prep_met thy "met_test_squeq" [] e_metID
24.273 - (*root-equation*)
24.274 - (["Test","square_equation"]:metID,
24.275 - [("#Given" ,["equality e_e","solveFor v_v"]),
24.276 - ("#Find" ,["solutions v_v'i'"])
24.277 - ],
24.278 - {rew_ord'="e_rew_ord",rls'=tval_rls,
24.279 - srls = append_rls "srls_contains_root" e_rls
24.280 - [Calc ("Test.contains'_root",eval_contains_root"")],
24.281 - prls=e_rls,calc=[],
24.282 - crls=tval_rls, errpats = [], nrls = e_rls(*,asm_rls=[],
24.283 - asm_thm=[("square_equation_left",""),
24.284 - ("square_equation_right","")]*)},
24.285 - "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
24.286 - "(let e_e = " ^
24.287 - " ((While (contains_root e_e) Do" ^
24.288 - " (((Rewrite square_equation_left True) Or" ^
24.289 - " (Rewrite square_equation_right True)) @@" ^
24.290 - " (Try (Rewrite_Set Test_simplify False)) @@" ^
24.291 - " (Try (Rewrite_Set rearrange_assoc False)) @@" ^
24.292 - " (Try (Rewrite_Set isolate_root False)) @@" ^
24.293 - " (Try (Rewrite_Set Test_simplify False)))) @@" ^
24.294 - " (Try (Rewrite_Set norm_equation False)) @@" ^
24.295 - " (Try (Rewrite_Set Test_simplify False)))" ^
24.296 - " e_e;" ^
24.297 - " (L_L::bool list) = (SubProblem (Test',[univariate,equation,test]," ^
24.298 - " [no_met]) [BOOL e_e, REAL v_v])" ^
24.299 - " in Check_elementwise L_L {(v_v::real). Assumptions})"
24.300 - ) ); (*#######*)
24.301 -
24.302 -*}
24.303 -ML {*
24.304 -store_met
24.305 - (prep_met thy "met_test_eq_plain" [] e_metID
24.306 - (*solve_plain_square*)
24.307 - (["Test","solve_plain_square"]:metID,
24.308 - [("#Given",["equality e_e","solveFor v_v"]),
24.309 - ("#Where" ,["(matches (?a + ?b*v_v ^^^2 = 0) e_e) |" ^
24.310 - "(matches ( ?b*v_v ^^^2 = 0) e_e) |" ^
24.311 - "(matches (?a + v_v ^^^2 = 0) e_e) |" ^
24.312 - "(matches ( v_v ^^^2 = 0) e_e)"]),
24.313 - ("#Find" ,["solutions v_v'i'"])
24.314 - ],
24.315 - {rew_ord'="e_rew_ord",rls'=tval_rls,calc=[],srls=e_rls,
24.316 - prls = assoc_rls' @{theory} "matches",
24.317 - crls=tval_rls, errpats = [], nrls = e_rls(*,
24.318 - asm_rls=[],asm_thm=[]*)},
24.319 - "Script Solve_plain_square (e_e::bool) (v_v::real) = " ^
24.320 - " (let e_e = ((Try (Rewrite_Set isolate_bdv False)) @@ " ^
24.321 - " (Try (Rewrite_Set Test_simplify False)) @@ " ^
24.322 - " ((Rewrite square_equality_0 False) Or " ^
24.323 - " (Rewrite square_equality True)) @@ " ^
24.324 - " (Try (Rewrite_Set tval_rls False))) e_e " ^
24.325 - " in ((Or_to_List e_e)::bool list))"
24.326 - ));
24.327 -
24.328 -*}
24.329 -
24.330 -ML {*
24.331 -store_met
24.332 - (prep_met thy "met_test_norm_univ" [] e_metID
24.333 - (["Test","norm_univar_equation"]:metID,
24.334 - [("#Given",["equality e_e","solveFor v_v"]),
24.335 - ("#Where" ,[]),
24.336 - ("#Find" ,["solutions v_v'i'"])
24.337 - ],
24.338 - {rew_ord'="e_rew_ord",rls'=tval_rls,srls = e_rls,prls=e_rls,
24.339 - calc=[],
24.340 - crls=tval_rls, errpats = [], nrls = e_rls},
24.341 - "Script Norm_univar_equation (e_e::bool) (v_v::real) = " ^
24.342 - " (let e_e = ((Try (Rewrite rnorm_equation_add False)) @@ " ^
24.343 - " (Try (Rewrite_Set Test_simplify False))) e_e " ^
24.344 - " in (SubProblem (Test',[univariate,equation,test], " ^
24.345 - " [no_met]) [BOOL e_e, REAL v_v]))"
24.346 - ));
24.347 -
24.348 -(*17.9.02 aus SqRoot.ML------------------------------^^^---*)
24.349 -
24.350 -store_met
24.351 -(prep_met thy "met_test_intsimp" [] e_metID
24.352 - (["Test","intsimp"]:metID,
24.353 - [("#Given" ,["intTestGiven t_t"]),
24.354 - ("#Where" ,[]),
24.355 - ("#Find" ,["intTestFind s_s"])
24.356 - ],
24.357 - {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = e_rls,
24.358 - prls = e_rls, calc = [], crls = tval_rls, errpats = [], nrls = Test_simplify},
24.359 - "Script STest_simplify (t_t::int) = " ^
24.360 - "(Repeat " ^
24.361 - " ((Try (Calculate PLUS)) @@ " ^
24.362 - " (Try (Calculate TIMES))) t_t::int)"
24.363 - ));
24.364 -
24.365 -*}
24.366 setup {* KEStore_Elems.add_mets
24.367 [prep_met thy "met_test_sqrt" [] e_metID
24.368 (*root-equation, version for tests before 8.01.01*)
25.1 --- a/src/Tools/isac/calcelems.sml Sun Feb 02 02:45:11 2014 +0100
25.2 +++ b/src/Tools/isac/calcelems.sml Sun Feb 02 03:09:40 2014 +0100
25.3 @@ -892,7 +892,6 @@
25.4
25.5
25.6 type mets = (met ptyp) list;
25.7 -val mets = Unsynchronized.ref ([e_Mets]:mets);
25.8
25.9 fun coll_metguhs mets =
25.10 let fun node coll (Ptyp (_,[n],ns)) =
26.1 --- a/src/Tools/isac/xmlsrc/pbl-met-hierarchy.sml Sun Feb 02 02:45:11 2014 +0100
26.2 +++ b/src/Tools/isac/xmlsrc/pbl-met-hierarchy.sml Sun Feb 02 03:09:40 2014 +0100
26.3 @@ -329,14 +329,6 @@
26.4 srls = srls, prls = prls, crls = crls, nrls = nrls, calc = calc,
26.5 ppc = ppc, pre = pre, scr = scr, errpats = errpats'}: met
26.6
26.7 -(* interface for dialog-authoring: call in Buld_Thydata.thy only ! *)
26.8 -fun insert_errpats theID errpats =
26.9 - let
26.10 - val met = get_met theID
26.11 - val met' = update_metdata met errpats
26.12 - handle ERROR _ => error ("insert_errpats: " ^ strs2str theID ^ "must address a method")
26.13 - in mets := insrt theID met' theID (! mets) end;
26.14 -
26.15 fun update_metpair metID errpats = let
26.16 val ret = (update_metdata (get_met metID) errpats, metID)
26.17 handle ERROR _ => error ("update_metpair: " ^ (strs2str metID) ^ "must address a method");
27.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Sun Feb 02 02:45:11 2014 +0100
27.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Sun Feb 02 03:09:40 2014 +0100
27.3 @@ -922,20 +922,6 @@
27.4 \normalfont node. We have to define both nodes first with an empty script
27.5 as content.*}
27.6
27.7 -ML {*
27.8 - store_met
27.9 - (prep_met thy "met_SP" [] e_metID
27.10 - (["SignalProcessing"], [],
27.11 - {rew_ord'="tless_true", rls'= e_rls, calc = [],
27.12 - srls = e_rls, prls = e_rls,
27.13 - crls = e_rls, errpats = [], nrls = e_rls}, "empty_script"));
27.14 - store_met
27.15 - (prep_met thy "met_SP_Ztrans" [] e_metID
27.16 - (["SignalProcessing", "Z_Transform"], [],
27.17 - {rew_ord'="tless_true", rls'= e_rls, calc = [],
27.18 - srls = e_rls, prls = e_rls,
27.19 - crls = e_rls, errpats = [], nrls = e_rls}, "empty_script"));
27.20 -*}
27.21 setup {* KEStore_Elems.add_mets
27.22 [prep_met thy "met_SP" [] e_metID
27.23 (["SignalProcessing"], [],
27.24 @@ -953,17 +939,6 @@
27.25 script we want to implement later. First we define the specifications
27.26 of the script in e.g. the in- and output.*}
27.27
27.28 -ML {*
27.29 - store_met
27.30 - (prep_met thy "met_SP_Ztrans_inv" [] e_metID
27.31 - (["SignalProcessing", "Z_Transform", "Inverse"],
27.32 - [("#Given" ,["filterExpression X_eq"]),
27.33 - ("#Find" ,["stepResponse n_eq"])
27.34 - ],
27.35 - {rew_ord'="tless_true", rls'= e_rls, calc = [],
27.36 - srls = e_rls, prls = e_rls,
27.37 - crls = e_rls, errpats = [], nrls = e_rls}, "empty_script"));
27.38 -*}
27.39 setup {* KEStore_Elems.add_mets
27.40 [prep_met thy "met_SP_Ztrans_inv" [] e_metID
27.41 (["SignalProcessing", "Z_Transform", "Inverse"],
27.42 @@ -977,21 +952,6 @@
27.43 script itself. As a first try we define only three rows containing one
27.44 simple operation.*}
27.45
27.46 -ML {*
27.47 - store_met
27.48 - (prep_met thy "met_SP_Ztrans_inv" [] e_metID
27.49 - (["SignalProcessing", "Z_Transform", "Inverse"],
27.50 - [("#Given" ,["filterExpression X_eq"]),
27.51 - ("#Find" ,["stepResponse n_eq"])
27.52 - ],
27.53 - {rew_ord'="tless_true", rls'= e_rls, calc = [],
27.54 - srls = e_rls, prls = e_rls,
27.55 - crls = e_rls, errpats = [], nrls = e_rls},
27.56 - "Script InverseZTransform (Xeq::bool) =" ^
27.57 - " (let X = Take Xeq;" ^
27.58 - " X = Rewrite ruleZY False X" ^
27.59 - " in X)"));
27.60 -*}
27.61 setup {* KEStore_Elems.add_mets
27.62 [prep_met thy "met_SP_Ztrans_inv" [] e_metID
27.63 (["SignalProcessing", "Z_Transform", "Inverse"],
27.64 @@ -1166,93 +1126,6 @@
27.65 Note that we also did this stepwise, but we didn't kept every
27.66 subversion.*}
27.67
27.68 -ML {*
27.69 - store_met(
27.70 - prep_met thy "met_SP_Ztrans_inv" [] e_metID
27.71 - (["SignalProcessing",
27.72 - "Z_Transform",
27.73 - "Inverse"],
27.74 - [
27.75 - ("#Given" ,["filterExpression X_eq"]),
27.76 - ("#Find" ,["stepResponse n_eq"])
27.77 - ],
27.78 - {
27.79 - rew_ord'="tless_true",
27.80 - rls'= e_rls, calc = [],
27.81 - srls = srls,
27.82 - prls = e_rls,
27.83 - crls = e_rls, errpats = [], nrls = e_rls
27.84 - },
27.85 - "Script InverseZTransform (X_eq::bool) = "^
27.86 - (*(1/z) instead of z ^^^ -1*)
27.87 - "(let X = Take X_eq; "^
27.88 - " X' = Rewrite ruleZY False X; "^
27.89 - (*z * denominator*)
27.90 - " (num_orig::real) = get_numerator (rhs X'); "^
27.91 - " X' = (Rewrite_Set norm_Rational False) X'; "^
27.92 - (*simplify*)
27.93 - " (X'_z::real) = lhs X'; "^
27.94 - " (zzz::real) = argument_in X'_z; "^
27.95 - " (funterm::real) = rhs X'; "^
27.96 - (*drop X' z = for equation solving*)
27.97 - " (denom::real) = get_denominator funterm; "^
27.98 - (*get_denominator*)
27.99 - " (num::real) = get_numerator funterm; "^
27.100 - (*get_numerator*)
27.101 - " (equ::bool) = (denom = (0::real)); "^
27.102 - " (L_L::bool list) = (SubProblem (PolyEq', "^
27.103 - " [abcFormula,degree_2,polynomial,univariate,equation], "^
27.104 - " [no_met]) "^
27.105 - " [BOOL equ, REAL zzz]); "^
27.106 - " (facs::real) = factors_from_solution L_L; "^
27.107 - " (eql::real) = Take (num_orig / facs); "^
27.108 -
27.109 - " (eqr::real) = (Try (Rewrite_Set ansatz_rls False)) eql; "^
27.110 -
27.111 - " (eq::bool) = Take (eql = eqr); "^
27.112 - (*Maybe possible to use HOLogic.mk_eq ??*)
27.113 - " eq = (Try (Rewrite_Set equival_trans False)) eq; "^
27.114 -
27.115 - " eq = drop_questionmarks eq; "^
27.116 - " (z1::real) = (rhs (NTH 1 L_L)); "^
27.117 - (*
27.118 - * prepare equation for a - eq_a
27.119 - * therefor substitute z with solution 1 - z1
27.120 - *)
27.121 - " (z2::real) = (rhs (NTH 2 L_L)); "^
27.122 -
27.123 - " (eq_a::bool) = Take eq; "^
27.124 - " eq_a = (Substitute [zzz=z1]) eq; "^
27.125 - " eq_a = (Rewrite_Set norm_Rational False) eq_a; "^
27.126 - " (sol_a::bool list) = "^
27.127 - " (SubProblem (Isac', "^
27.128 - " [univariate,equation],[no_met]) "^
27.129 - " [BOOL eq_a, REAL (A::real)]); "^
27.130 - " (a::real) = (rhs(NTH 1 sol_a)); "^
27.131 -
27.132 - " (eq_b::bool) = Take eq; "^
27.133 - " eq_b = (Substitute [zzz=z2]) eq_b; "^
27.134 - " eq_b = (Rewrite_Set norm_Rational False) eq_b; "^
27.135 - " (sol_b::bool list) = "^
27.136 - " (SubProblem (Isac', "^
27.137 - " [univariate,equation],[no_met]) "^
27.138 - " [BOOL eq_b, REAL (B::real)]); "^
27.139 - " (b::real) = (rhs(NTH 1 sol_b)); "^
27.140 -
27.141 - " eqr = drop_questionmarks eqr; "^
27.142 - " (pbz::real) = Take eqr; "^
27.143 - " pbz = ((Substitute [A=a, B=b]) pbz); "^
27.144 -
27.145 - " pbz = Rewrite ruleYZ False pbz; "^
27.146 - " pbz = drop_questionmarks pbz; "^
27.147 -
27.148 - " (X_z::bool) = Take (X_z = pbz); "^
27.149 - " (n_eq::bool) = (Rewrite_Set inverse_z False) X_z; "^
27.150 - " n_eq = drop_questionmarks n_eq "^
27.151 - "in n_eq)"
27.152 - )
27.153 - );
27.154 -*}
27.155 setup {* KEStore_Elems.add_mets
27.156 [prep_met thy "met_SP_Ztrans_inv" [] e_metID
27.157 (["SignalProcessing", "Z_Transform", "Inverse"],
28.1 --- a/test/Tools/isac/Knowledge/integrate.sml Sun Feb 02 02:45:11 2014 +0100
28.2 +++ b/test/Tools/isac/Knowledge/integrate.sml Sun Feb 02 03:09:40 2014 +0100
28.3 @@ -502,25 +502,6 @@
28.4 else error "integrate.sml: interSteps on Rewrite_Set_Inst";
28.5
28.6
28.7 -"----------- method analog to rls 'integration' ---------";
28.8 -"----------- method analog to rls 'integration' ---------";
28.9 -"----------- method analog to rls 'integration' ---------";
28.10 -store_met
28.11 - (prep_met thy "met_testint" [] e_metID
28.12 - (["diff","integration","test"],
28.13 - [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
28.14 - ("#Find" ,["antiDerivative F_F"])
28.15 - ],
28.16 - {rew_ord'="tless_true", rls'=Atools_erls, calc = [],
28.17 - srls = e_rls,
28.18 - prls=e_rls,
28.19 - crls = Atools_erls, errpats = [], nrls = e_rls},
28.20 -"Script IntegrationScript (f_f::real) (v_v::real) = \
28.21 -\ (((Rewrite_Set_Inst [(bdv,v_v)] integration_rules False) @@ \
28.22 -\ (Rewrite_Set_Inst [(bdv,v_v)] add_new_c False) @@ \
28.23 -\ (Rewrite_Set_Inst [(bdv,v_v)] simplify_Integral False)) (f_f::real))"
28.24 -));
28.25 -
28.26 states:=[];
28.27 CalcTree
28.28 [(["functionTerm (Integral x^2 + 1 D x)", "integrateBy x", "antiDerivative FF"],
29.1 --- a/test/Tools/isac/ProgLang/calculate.sml Sun Feb 02 02:45:11 2014 +0100
29.2 +++ b/test/Tools/isac/ProgLang/calculate.sml Sun Feb 02 03:09:40 2014 +0100
29.3 @@ -71,29 +71,6 @@
29.4 if term2str t <> "16" then error "calculate.sml: new behaviour in calculate_"
29.5 else ();
29.6
29.7 -"----------- calculate from script ----------------------";
29.8 -"----------- calculate from script ----------------------";
29.9 -"----------- calculate from script ----------------------";
29.10 -store_met
29.11 - (prep_met (@{theory "Test"}) "met_testcal" [] e_metID
29.12 - (["Test","test_calculate"]:metID,
29.13 - [("#Given" ,["realTestGiven t_t"]),
29.14 - ("#Find" ,["realTestFind s_s"])
29.15 - ],
29.16 - {rew_ord'="sqrt_right",rls'=tval_rls,srls=e_rls,prls=e_rls,
29.17 - calc=[("PLUS" ,("op +" ,eval_binop "#add_")),
29.18 - ("TIMES" ,("Groups.times_class.times" ,eval_binop "#mult_")),
29.19 - ("DIVIDE" ,("HOL.divide" ,eval_cancel "#divide_")),
29.20 - ("POWER" ,("Atools.pow" ,eval_binop "#power_"))],
29.21 - crls=tval_rls, errpats = [], nrls=e_rls(*,
29.22 - asm_rls=[],asm_thm=[]*)},
29.23 - "Script STest_simplify (t_t::real) = \
29.24 - \(Repeat \
29.25 - \ ((Try (Repeat (Calculate PLUS))) @@ \
29.26 - \ (Try (Repeat (Calculate TIMES))) @@ \
29.27 - \ (Try (Repeat (Calculate DIVIDE))) @@ \
29.28 - \ (Try (Repeat (Calculate POWER))))) t_t"
29.29 - ));
29.30
29.31 val fmz = ["realTestGiven (((1+2)*4/3)^^^2)","realTestFind s"];
29.32 val (dI',pI',mI') =
30.1 --- a/test/Tools/isac/ProgLang/scrtools.sml Sun Feb 02 02:45:11 2014 +0100
30.2 +++ b/test/Tools/isac/ProgLang/scrtools.sml Sun Feb 02 03:09:40 2014 +0100
30.3 @@ -22,31 +22,6 @@
30.4 writeln(term2str auto_script);
30.5 atomty auto_script;
30.6
30.7 -store_met
30.8 - (prep_met @{theory "Test"} "met_testinter" [] e_metID
30.9 - (["Test","test_interSteps_1"]:metID,
30.10 - [("#Given" ,["Term t_t"]),
30.11 - ("#Find" ,["normalform n_n"])
30.12 - ],
30.13 - {rew_ord' = "dummy_ord", rls' = tval_rls, calc = [], srls = e_rls, prls = e_rls,
30.14 - crls=tval_rls, errpats = [], nrls=e_rls},
30.15 -"Script Stepwise t_t = \
30.16 - \(Try (Rewrite_Set discard_minus False) @@ \
30.17 - \ Try (Rewrite_Set expand_poly False) @@ \
30.18 - \ Try (Repeat (Calculate TIMES)) @@ \
30.19 - \ Try (Rewrite_Set order_mult_rls False) @@ \
30.20 - \ Try (Rewrite_Set simplify_power False) @@ \
30.21 - \ Try (Rewrite_Set calc_add_mult_pow False) @@ \
30.22 - \ Try (Rewrite_Set reduce_012_mult False) @@ \
30.23 - \ Try (Rewrite_Set order_add_rls False) @@ \
30.24 - \ Try (Rewrite_Set collect_numerals False) @@ \
30.25 - \ Try (Rewrite_Set reduce_012 False) @@ \
30.26 - \ Try (Rewrite_Set discard_parentheses False)) \
30.27 - \ t_t"
30.28 -(*presently this script cannot become equal in types to auto_script, because:
30.29 - this t_t must be either 'real' or 'bool' #1#,
30.30 - while the auto_script must be 'z and type-instantiated before usage*)
30.31 - ));
30.32 show_mets();
30.33 val {scr = Prog parsed_script,...} = get_met ["Test","test_interSteps_1"];
30.34 writeln(term2str parsed_script);