ad 967c8a1eb6b1 (2): add functions accessing Theory_Data in parallel to those accessing 'mets = Unsynchronized.ref'
1.1 --- a/src/Tools/isac/Interpret/ptyps.sml Fri Jan 31 17:50:50 2014 +0100
1.2 +++ b/src/Tools/isac/Interpret/ptyps.sml Sat Feb 01 16:44:45 2014 +0100
1.3 @@ -347,14 +347,6 @@
1.4 else del k (ptyps @ [Ptyp (k', [p], ps)]) pys;
1.5 in del k [] ptyps end;
1.6
1.7 -
1.8 -fun coll_metguhs mets =
1.9 - let fun node coll (Ptyp (_,[n],ns)) =
1.10 - [(#guh : met -> guh) n]
1.11 - and nodes coll [] = coll
1.12 - | nodes coll (n::ns) = (node coll n) @ (nodes coll ns);
1.13 - in nodes [] mets end;
1.14 -
1.15 (*.lookup a guh in hierarchy or methods depending on fst chars in guh.*)
1.16 fun guh2kestoreID (guh:guh) =
1.17 case (implode o (take_fromto 1 4) o Symbol.explode) guh of
1.18 @@ -389,16 +381,6 @@
1.19 (*> guh2kestoreID "pbl_equ_univ_lin";
1.20 val it = ["linear", "univariate", "equation"] : string list*)
1.21
1.22 -
1.23 -(* val (guh, mets) = ("met_test", !mets);
1.24 - *)
1.25 -fun check_metguh_unique (guh:guh) (mets: (met ptyp) list) =
1.26 - if member op = (coll_metguhs mets) guh
1.27 - then error ("check_guh_unique failed with '"^guh^"';\n"^
1.28 - "use 'sort_metguhs()' for a list of guhs;\n"^
1.29 - "consider setting 'check_guhs_unique := false'")
1.30 - else ();
1.31 -
1.32
1.33
1.34 (*.the metID has the root-element as first.*)
2.1 --- a/src/Tools/isac/KEStore.thy Fri Jan 31 17:50:50 2014 +0100
2.2 +++ b/src/Tools/isac/KEStore.thy Sat Feb 01 16:44:45 2014 +0100
2.3 @@ -27,6 +27,8 @@
2.4 val add_cas: cas_elem list -> theory -> theory
2.5 val get_ptyps: theory -> ptyps
2.6 val add_pbts: (pbt * pblID) list -> theory -> theory
2.7 + val get_mets: theory -> mets
2.8 + val add_mets: (met * metID) list -> theory -> theory
2.9 (*etc*)
2.10 end;
2.11
2.12 @@ -75,6 +77,19 @@
2.13 rev pblID |> insrt pblID pbt);
2.14 in Data.map (fold add_pbt pbts) thy end;
2.15
2.16 + structure Data = Theory_Data (
2.17 + type T = mets;
2.18 + val empty = [e_Mets];
2.19 + val extend = I;
2.20 + val merge = merge_ptyps;
2.21 + );
2.22 + val get_mets = Data.get;
2.23 + fun add_mets mets thy = let
2.24 + fun add_met (met as {guh,...}, metID) =
2.25 + (if (!check_guhs_unique) then check_metguh_unique guh (Data.get thy) else ();
2.26 + insrt metID met metID);
2.27 + in Data.map (fold add_met mets) thy end;
2.28 +
2.29 (*etc*)
2.30 end;
2.31 *}
2.32 @@ -117,7 +132,9 @@
2.33 fun get_ptyps () =
2.34 ML_Context.the_generic_context () |> Context.theory_of |> KEStore_Elems.get_ptyps;
2.35
2.36 -fun get_mets () = ! mets;
2.37 +fun get_mets () = ! mets; (* SWITCH remove *)
2.38 +(*fun get_mets () = SWITCH outcommented
2.39 + ML_Context.the_generic_context () |> Context.theory_of |> KEStore_Elems.get_mets*)
2.40
2.41 *}
2.42 setup {* KEStore_Elems.add_rlss
3.1 --- a/src/Tools/isac/Knowledge/AlgEin.thy Fri Jan 31 17:50:50 2014 +0100
3.2 +++ b/src/Tools/isac/Knowledge/AlgEin.thy Sat Feb 01 16:44:45 2014 +0100
3.3 @@ -129,5 +129,71 @@
3.4 " in (Try (Rewrite_Set norm_Poly False)) t_t) "
3.5 ));
3.6 *}
3.7 +setup {* KEStore_Elems.add_mets
3.8 + [prep_met thy "met_algein" [] e_metID
3.9 + (["Berechnung"], [],
3.10 + {rew_ord'="tless_true", rls'= Erls, calc = [], srls = Erls, prls = Erls, crls =Erls,
3.11 + errpats = [], nrls = Erls},
3.12 + "empty_script"),
3.13 + prep_met thy "met_algein_numsym" [] e_metID
3.14 + (["Berechnung","erstNumerisch"], [],
3.15 + {rew_ord'="tless_true", rls'= Erls, calc = [], srls = Erls, prls = Erls, crls =Erls,
3.16 + errpats = [], nrls = Erls},
3.17 + "empty_script"),
3.18 + prep_met thy "met_algein_numsym" [] e_metID
3.19 + (["Berechnung","erstNumerisch"],
3.20 + [("#Given" ,["KantenLaenge k_k","Querschnitt q__q", "KantenUnten u_u",
3.21 + "KantenSenkrecht s_s", "KantenOben o_o"]),
3.22 + ("#Find" ,["GesamtLaenge l_l"])],
3.23 + {rew_ord'="tless_true", rls'= e_rls, calc = [],
3.24 + srls = append_rls "srls_..Berechnung-erstSymbolisch" e_rls
3.25 + [Calc ("Atools.boollist2sum", eval_boollist2sum "")],
3.26 + prls = e_rls, crls =e_rls , errpats = [], nrls = norm_Rational},
3.27 + "Script RechnenSymbolScript (k_k::bool) (q__q::bool) " ^
3.28 + "(u_u::bool list) (s_s::bool list) (o_o::bool list) (l_l::real) =" ^
3.29 + " (let t_t = Take (l_l = oben + senkrecht + unten); " ^
3.30 + " su_m = boollist2sum o_o; " ^
3.31 + " t_t = Substitute [oben = su_m] t_t; " ^
3.32 + " t_t = Substitute o_o t_t; " ^
3.33 + " t_t = Substitute [k_k, q__q] t_t; " ^
3.34 + " t_t = (Repeat (Try (Rewrite_Set norm_Poly False))) t_t; " ^
3.35 + " su_m = boollist2sum s_s; " ^
3.36 + " t_t = Substitute [senkrecht = su_m] t_t; " ^
3.37 + " t_t = Substitute s_s t_t; " ^
3.38 + " t_t = Substitute [k_k, q__q] t_t; " ^
3.39 + " t_t = (Repeat (Try (Rewrite_Set norm_Poly False))) t_t; " ^
3.40 + " su_m = boollist2sum u_u; " ^
3.41 + " t_t = Substitute [unten = su_m] t_t; " ^
3.42 + " t_t = Substitute u_u t_t; " ^
3.43 + " t_t = Substitute [k_k, q__q] t_t; " ^
3.44 + " t_t = (Repeat (Try (Rewrite_Set norm_Poly False))) t_t " ^
3.45 + " in (Try (Rewrite_Set norm_Poly False)) t_t) "),
3.46 + prep_met thy "met_algein_symnum" [] e_metID
3.47 + (["Berechnung","erstSymbolisch"],
3.48 + [("#Given" ,["KantenLaenge k_k","Querschnitt q__q", "KantenUnten u_u",
3.49 + "KantenSenkrecht s_s", "KantenOben o_o"]),
3.50 + ("#Find" ,["GesamtLaenge l_l"])],
3.51 + {rew_ord'="tless_true", rls'= e_rls, calc = [],
3.52 + srls = append_rls "srls_..Berechnung-erstSymbolisch" e_rls
3.53 + [Calc ("Atools.boollist2sum", eval_boollist2sum "")],
3.54 + prls = e_rls, crls =e_rls , errpats = [], nrls = norm_Rational},
3.55 + "Script RechnenSymbolScript (k_k::bool) (q__q::bool) " ^
3.56 + "(u_u::bool list) (s_s::bool list) (o_o::bool list) (l_l::real) =" ^
3.57 + " (let t_t = Take (l_l = oben + senkrecht + unten); " ^
3.58 + " su_m = boollist2sum o_o; " ^
3.59 + " t_t = Substitute [oben = su_m] t_t; " ^
3.60 + " t_t = Substitute o_o t_t; " ^
3.61 + " t_t = (Repeat (Try (Rewrite_Set norm_Poly False))) t_t; " ^
3.62 + " su_m = boollist2sum s_s; " ^
3.63 + " t_t = Substitute [senkrecht = su_m] t_t; " ^
3.64 + " t_t = Substitute s_s t_t; " ^
3.65 + " t_t = (Repeat (Try (Rewrite_Set norm_Poly False))) t_t; " ^
3.66 + " su_m = boollist2sum u_u; " ^
3.67 + " t_t = Substitute [unten = su_m] t_t; " ^
3.68 + " t_t = Substitute u_u t_t; " ^
3.69 + " t_t = (Repeat (Try (Rewrite_Set norm_Poly False))) t_t; " ^
3.70 + " t_t = Substitute [k_k, q__q] t_t " ^
3.71 + " in (Try (Rewrite_Set norm_Poly False)) t_t) ")]
3.72 +*}
3.73
3.74 end
4.1 --- a/src/Tools/isac/Knowledge/Biegelinie.thy Fri Jan 31 17:50:50 2014 +0100
4.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy Sat Feb 01 16:44:45 2014 +0100
4.3 @@ -489,5 +489,256 @@
4.4 ));
4.5 *}
4.6
4.7 +setup {* KEStore_Elems.add_mets
4.8 + [prep_met thy "met_biege" [] e_metID
4.9 + (["IntegrierenUndKonstanteBestimmen"],
4.10 + [("#Given" ,["Traegerlaenge l_l", "Streckenlast q__q", "FunktionsVariable v_v"]),
4.11 + (*("#Where",["0 < l_l"]), ...wait for < and handling Arbfix*)
4.12 + ("#Find" ,["Biegelinie b_b"]),
4.13 + ("#Relate",["RandbedingungenBiegung r_b", "RandbedingungenMoment r_m"])],
4.14 + {rew_ord'="tless_true",
4.15 + rls' = append_rls "erls_IntegrierenUndK.." e_rls
4.16 + [Calc ("Atools.ident",eval_ident "#ident_"),
4.17 + Thm ("not_true",num_str @{thm not_true}),
4.18 + Thm ("not_false",num_str @{thm not_false})],
4.19 + calc = [], srls = srls, prls = Erls, crls = Atools_erls, errpats = [], nrls = Erls},
4.20 + "Script BiegelinieScript " ^
4.21 + "(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) " ^
4.22 + "(r_b::bool list) (r_m::bool list) = " ^
4.23 + " (let q___q = Take (qq v_v = q__q); " ^
4.24 + " q___q = ((Rewrite sym_neg_equal_iff_equal True) @@ " ^
4.25 + " (Rewrite Belastung_Querkraft True)) q___q; " ^
4.26 + " (Q__Q:: bool) = " ^
4.27 + " (SubProblem (Biegelinie',[named,integrate,function], " ^
4.28 + " [diff,integration,named]) " ^
4.29 + " [REAL (rhs q___q), REAL v_v, REAL_REAL Q]); " ^
4.30 + " Q__Q = Rewrite Querkraft_Moment True Q__Q; " ^
4.31 + " (M__M::bool) = " ^
4.32 + " (SubProblem (Biegelinie',[named,integrate,function], " ^
4.33 + " [diff,integration,named]) " ^
4.34 + " [REAL (rhs Q__Q), REAL v_v, REAL_REAL M_b]); " ^
4.35 + (*([5], Res), M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2*)
4.36 + " e__1 = NTH 1 r_m; " ^
4.37 + " (x__1::real) = argument_in (lhs e__1); " ^
4.38 + " (M__1::bool) = (Substitute [v_v = x__1]) M__M; " ^
4.39 + (*([6], Res), M_b 0 = c_2 + c * 0 + -1 * q_0 / 2 * 0 ^^^ 2*)
4.40 + " M__1 = (Substitute [e__1]) M__1; " ^
4.41 + (*([7], Res), 0 = c_2 + c * 0 + -1 * q_0 / 2 * 0 ^^^ 2*)
4.42 + " M__2 = Take M__M; " ^
4.43 + (*([8], Frm), M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2*)
4.44 + (*without above Take 'Substitute [v_v = x__2]' takes _last formula from ctree_*)
4.45 + " e__2 = NTH 2 r_m; " ^
4.46 + " (x__2::real) = argument_in (lhs e__2); " ^
4.47 + " (M__2::bool) = (Substitute [v_v = x__2]) M__M; " ^
4.48 + (*([8], Res), M_b L = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2*)
4.49 + " M__2 = (Substitute [e__2]) M__2; " ^
4.50 + " (c_1_2::bool list) = " ^
4.51 + " (SubProblem (Biegelinie',[LINEAR,system],[no_met]) " ^
4.52 + " [BOOL_LIST [M__1, M__2], REAL_LIST [c,c_2]]); " ^
4.53 + " M__M = Take M__M; " ^
4.54 + " M__M = ((Substitute c_1_2) @@ " ^
4.55 + " (Try (Rewrite_Set_Inst [(bdv_1, c),(bdv_2, c_2)] " ^
4.56 + " simplify_System False)) @@ " ^
4.57 + " (Rewrite Moment_Neigung False) @@ " ^
4.58 + " (Rewrite make_fun_explicit False)) M__M; " ^
4.59 + (*----------------------- and the same once more ------------------------*)
4.60 + " (N__N:: bool) = " ^
4.61 + " (SubProblem (Biegelinie',[named,integrate,function], " ^
4.62 + " [diff,integration,named]) " ^
4.63 + " [REAL (rhs M__M), REAL v_v, REAL_REAL y']); " ^
4.64 + " (B__B:: bool) = " ^
4.65 + " (SubProblem (Biegelinie',[named,integrate,function], " ^
4.66 + " [diff,integration,named]) " ^
4.67 + " [REAL (rhs N__N), REAL v_v, REAL_REAL y]); " ^
4.68 + " e__1 = NTH 1 r_b; " ^
4.69 + " (x__1::real) = argument_in (lhs e__1); " ^
4.70 + " (B__1::bool) = (Substitute [v_v = x__1]) B__B; " ^
4.71 + " B__1 = (Substitute [e__1]) B__1 ; " ^
4.72 + " B__2 = Take B__B; " ^
4.73 + " e__2 = NTH 2 r_b; " ^
4.74 + " (x__2::real) = argument_in (lhs e__2); " ^
4.75 + " (B__2::bool) = (Substitute [v_v = x__2]) B__B; " ^
4.76 + " B__2 = (Substitute [e__2]) B__2 ; " ^
4.77 + " (c_1_2::bool list) = " ^
4.78 + " (SubProblem (Biegelinie',[LINEAR,system],[no_met]) " ^
4.79 + " [BOOL_LIST [B__1, B__2], REAL_LIST [c,c_2]]); " ^
4.80 + " B__B = Take B__B; " ^
4.81 + " B__B = ((Substitute c_1_2) @@ " ^
4.82 + " (Rewrite_Set_Inst [(bdv, x)] make_ratpoly_in False)) B__B " ^
4.83 + " in B__B)"),
4.84 + prep_met thy "met_biege_2" [] e_metID
4.85 + (["IntegrierenUndKonstanteBestimmen2"],
4.86 + [("#Given" ,["Traegerlaenge l_l", "Streckenlast q__q", "FunktionsVariable v_v"]),
4.87 + (*("#Where",["0 < l_l"]), ...wait for < and handling Arbfix*)
4.88 + ("#Find" ,["Biegelinie b_b"]),
4.89 + ("#Relate",["Randbedingungen r_b"])],
4.90 + {rew_ord'="tless_true",
4.91 + rls' = append_rls "erls_IntegrierenUndK.." e_rls
4.92 + [Calc ("Atools.ident",eval_ident "#ident_"),
4.93 + Thm ("not_true",num_str @{thm not_true}),
4.94 + Thm ("not_false",num_str @{thm not_false})],
4.95 + calc = [],
4.96 + srls = append_rls "erls_IntegrierenUndK.." e_rls
4.97 + [Calc("Tools.rhs", eval_rhs"eval_rhs_"),
4.98 + Calc ("Atools.ident",eval_ident "#ident_"),
4.99 + Thm ("last_thmI",num_str @{thm last_thmI}),
4.100 + Thm ("if_True",num_str @{thm if_True}),
4.101 + Thm ("if_False",num_str @{thm if_False})],
4.102 + prls = Erls, crls = Atools_erls, errpats = [], nrls = Erls},
4.103 + "Script Biegelinie2Script " ^
4.104 + "(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) (r_b::bool list) = " ^
4.105 + " (let " ^
4.106 + " (fun_s:: bool list) = " ^
4.107 + " (SubProblem (Biegelinie',[vonBelastungZu,Biegelinien], " ^
4.108 + " [Biegelinien,ausBelastung]) " ^
4.109 + " [REAL q__q, REAL v_v]); " ^
4.110 + " (equ_s::bool list) = " ^
4.111 + " (SubProblem (Biegelinie',[setzeRandbedingungen,Biegelinien], " ^
4.112 + " [Biegelinien,setzeRandbedingungenEin]) " ^
4.113 + " [BOOL_LIST fun_s, BOOL_LIST r_b]); " ^
4.114 + " (con_s::bool list) = " ^
4.115 + " (SubProblem (Biegelinie',[LINEAR,system],[no_met]) " ^
4.116 + " [BOOL_LIST equ_s, REAL_LIST [c,c_2,c_3,c_4]]); " ^
4.117 + " B_B = Take (lastI fun_s); " ^
4.118 + " B_B = ((Substitute con_s) @@ " ^
4.119 + " (Rewrite_Set_Inst [(bdv, v_v)] make_ratpoly_in False)) B_B " ^
4.120 + " in B_B)"),
4.121 + prep_met thy "met_biege_intconst_2" [] e_metID
4.122 + (["IntegrierenUndKonstanteBestimmen","2xIntegrieren"], [],
4.123 + {rew_ord'="tless_true", rls'=Erls, calc = [], srls = e_rls, prls=e_rls, crls = Atools_erls,
4.124 + errpats = [], nrls = e_rls},
4.125 + "empty_script"),
4.126 + prep_met thy "met_biege_intconst_4" [] e_metID
4.127 + (["IntegrierenUndKonstanteBestimmen","4x4System"], [],
4.128 + {rew_ord'="tless_true", rls'=Erls, calc = [], srls = e_rls, prls=e_rls, crls = Atools_erls,
4.129 + errpats = [], nrls = e_rls},
4.130 + "empty_script"),
4.131 + prep_met thy "met_biege_intconst_1" [] e_metID
4.132 + (["IntegrierenUndKonstanteBestimmen","1xIntegrieren"], [],
4.133 + {rew_ord'="tless_true", rls'=Erls, calc = [], srls = e_rls, prls=e_rls, crls = Atools_erls,
4.134 + errpats = [], nrls = e_rls},
4.135 + "empty_script"),
4.136 + prep_met thy "met_biege2" [] e_metID
4.137 + (["Biegelinien"], [],
4.138 + {rew_ord'="tless_true", rls'=Erls, calc = [], srls = e_rls, prls=e_rls, crls = Atools_erls,
4.139 + errpats = [], nrls = e_rls},
4.140 + "empty_script"),
4.141 + prep_met thy "met_biege_ausbelast" [] e_metID
4.142 + (["Biegelinien", "ausBelastung"],
4.143 + [("#Given" ,["Streckenlast q__q", "FunktionsVariable v_v"]),
4.144 + ("#Find" ,["Funktionen fun_s"])],
4.145 + {rew_ord'="tless_true",
4.146 + rls' = append_rls "erls_ausBelastung" e_rls
4.147 + [Calc ("Atools.ident", eval_ident "#ident_"),
4.148 + Thm ("not_true", num_str @{thm not_true}),
4.149 + Thm ("not_false", num_str @{thm not_false})],
4.150 + calc = [],
4.151 + srls = append_rls "srls_ausBelastung" e_rls
4.152 + [Calc ("Tools.rhs", eval_rhs "eval_rhs_")],
4.153 + prls = e_rls, crls = Atools_erls, errpats = [], nrls = e_rls},
4.154 + "Script Belastung2BiegelScript (q__q::real) (v_v::real) = " ^
4.155 + " (let q___q = Take (qq v_v = q__q); " ^
4.156 + " q___q = ((Rewrite sym_neg_equal_iff_equal True) @@ " ^
4.157 + " (Rewrite Belastung_Querkraft True)) q___q; " ^
4.158 + " (Q__Q:: bool) = " ^
4.159 + " (SubProblem (Biegelinie',[named,integrate,function], " ^
4.160 + " [diff,integration,named]) " ^
4.161 + " [REAL (rhs q___q), REAL v_v, REAL_REAL Q]); " ^
4.162 + " M__M = Rewrite Querkraft_Moment True Q__Q; " ^
4.163 + " (M__M::bool) = " ^
4.164 + " (SubProblem (Biegelinie',[named,integrate,function], " ^
4.165 + " [diff,integration,named]) " ^
4.166 + " [REAL (rhs M__M), REAL v_v, REAL_REAL M_b]); " ^
4.167 + " N__N = ((Rewrite Moment_Neigung False) @@ " ^
4.168 + " (Rewrite make_fun_explicit False)) M__M; " ^
4.169 + " (N__N:: bool) = " ^
4.170 + " (SubProblem (Biegelinie',[named,integrate,function], " ^
4.171 + " [diff,integration,named]) " ^
4.172 + " [REAL (rhs N__N), REAL v_v, REAL_REAL y']); " ^
4.173 + " (B__B:: bool) = " ^
4.174 + " (SubProblem (Biegelinie',[named,integrate,function], " ^
4.175 + " [diff,integration,named]) " ^
4.176 + " [REAL (rhs N__N), REAL v_v, REAL_REAL y]) " ^
4.177 + " in [Q__Q, M__M, N__N, B__B])"),
4.178 + prep_met thy "met_biege_setzrand" [] e_metID
4.179 + (["Biegelinien", "setzeRandbedingungenEin"],
4.180 + [("#Given" , ["Funktionen fun_s", "Randbedingungen r_b"]),
4.181 + ("#Find" , ["Gleichungen equs'''"])],
4.182 + {rew_ord'="tless_true", rls'=Erls, calc = [], srls = srls2, prls=e_rls, crls = Atools_erls,
4.183 + errpats = [], nrls = e_rls},
4.184 + "Script SetzeRandbedScript (fun_s::bool list) (r_b::bool list) = " ^
4.185 + " (let b_1 = NTH 1 r_b; " ^
4.186 + " f_s = filter_sameFunId (lhs b_1) fun_s; " ^
4.187 + " (e_1::bool) = " ^
4.188 + " (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
4.189 + " [Equation,fromFunction]) " ^
4.190 + " [BOOL (hd f_s), BOOL b_1]); " ^
4.191 + " b_2 = NTH 2 r_b; " ^
4.192 + " f_s = filter_sameFunId (lhs b_2) fun_s; " ^
4.193 + " (e_2::bool) = " ^
4.194 + " (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
4.195 + " [Equation,fromFunction]) " ^
4.196 + " [BOOL (hd f_s), BOOL b_2]); " ^
4.197 + " b_3 = NTH 3 r_b; " ^
4.198 + " f_s = filter_sameFunId (lhs b_3) fun_s; " ^
4.199 + " (e_3::bool) = " ^
4.200 + " (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
4.201 + " [Equation,fromFunction]) " ^
4.202 + " [BOOL (hd f_s), BOOL b_3]); " ^
4.203 + " b_4 = NTH 4 r_b; " ^
4.204 + " f_s = filter_sameFunId (lhs b_4) fun_s; " ^
4.205 + " (e_4::bool) = " ^
4.206 + " (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
4.207 + " [Equation,fromFunction]) " ^
4.208 + " [BOOL (hd f_s), BOOL b_4]) " ^
4.209 + " in [e_1, e_2, e_3, e_4])"
4.210 + (* filter requires more than 1 sec !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
4.211 + "Script SetzeRandbedScript (fun_s::bool list) (r_b::bool list) = " ^
4.212 + " (let b_1 = NTH 1 r_b; " ^
4.213 + " f_s = filter (sameFunId (lhs b_1)) fun_s; " ^
4.214 + " (e_1::bool) = " ^
4.215 + " (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
4.216 + " [Equation,fromFunction]) " ^
4.217 + " [BOOL (hd f_s), BOOL b_1]); " ^
4.218 + " b_2 = NTH 2 r_b; " ^
4.219 + " f_s = filter (sameFunId (lhs b_2)) fun_s; " ^
4.220 + " (e_2::bool) = " ^
4.221 + " (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
4.222 + " [Equation,fromFunction]) " ^
4.223 + " [BOOL (hd f_s), BOOL b_2]); " ^
4.224 + " b_3 = NTH 3 r_b; " ^
4.225 + " f_s = filter (sameFunId (lhs b_3)) fun_s; " ^
4.226 + " (e_3::bool) = " ^
4.227 + " (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
4.228 + " [Equation,fromFunction]) " ^
4.229 + " [BOOL (hd f_s), BOOL b_3]); " ^
4.230 + " b_4 = NTH 4 r_b; " ^
4.231 + " f_s = filter (sameFunId (lhs b_4)) fun_s; " ^
4.232 + " (e_4::bool) = " ^
4.233 + " (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
4.234 + " [Equation,fromFunction]) " ^
4.235 + " [BOOL (hd f_s), BOOL b_4]) " ^
4.236 + " in [e_1,e_2,e_3,e_4])"*)),
4.237 + prep_met thy "met_equ_fromfun" [] e_metID
4.238 + (["Equation","fromFunction"],
4.239 + [("#Given" ,["functionEq fu_n","substitution su_b"]),
4.240 + ("#Find" ,["equality equ'''"])],
4.241 + {rew_ord'="tless_true", rls'=Erls, calc = [],
4.242 + srls = append_rls "srls_in_EquationfromFunc" e_rls
4.243 + [Calc("Tools.lhs", eval_lhs"eval_lhs_"),
4.244 + Calc("Atools.argument'_in", eval_argument_in "Atools.argument'_in")],
4.245 + prls=e_rls, crls = Atools_erls, errpats = [], nrls = e_rls},
4.246 + (*(M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2) (M_b L = 0) -->
4.247 + 0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2*)
4.248 + "Script Function2Equality (fu_n::bool) (su_b::bool) =" ^
4.249 + " (let fu_n = Take fu_n; " ^
4.250 + " bd_v = argument_in (lhs fu_n); " ^
4.251 + " va_l = argument_in (lhs su_b); " ^
4.252 + " eq_u = (Substitute [bd_v = va_l]) fu_n; " ^
4.253 + (*([1], Res), M_b L = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2*)
4.254 + " eq_u = (Substitute [su_b]) eq_u " ^
4.255 + " in (Rewrite_Set norm_Rational False) eq_u) ")]
4.256 +*}
4.257 +
4.258 end
4.259
5.1 --- a/src/Tools/isac/Knowledge/Diff.thy Fri Jan 31 17:50:50 2014 +0100
5.2 +++ b/src/Tools/isac/Knowledge/Diff.thy Sat Feb 01 16:44:45 2014 +0100
5.3 @@ -404,6 +404,111 @@
5.4 ]
5.5 | argl2dtss _ = error "Diff.ML: wrong argument for argl2dtss";
5.6 *}
5.7 +setup {* KEStore_Elems.add_mets
5.8 + [prep_met thy "met_diff" [] e_metID
5.9 + (["diff"], [],
5.10 + {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
5.11 + crls = Atools_erls, errpats = [], nrls = norm_diff},
5.12 + "empty_script"),
5.13 + prep_met thy "met_diff_onR" [] e_metID
5.14 + (["diff","differentiate_on_R"],
5.15 + [("#Given" ,["functionTerm f_f","differentiateFor v_v"]),
5.16 + ("#Find" ,["derivative f_f'"])],
5.17 + {rew_ord'="tless_true", rls' = erls_diff, calc = [], srls = e_rls, prls=e_rls,
5.18 + crls = Atools_erls, errpats = [], nrls = norm_diff},
5.19 + "Script DiffScr (f_f::real) (v_v::real) = " ^
5.20 + " (let f_f' = Take (d_d v_v f_f) " ^
5.21 + " in (((Try (Rewrite_Set_Inst [(bdv,v_v)] diff_conv False)) @@ " ^
5.22 + " (Repeat " ^
5.23 + " ((Repeat (Rewrite_Inst [(bdv,v_v)] diff_sum False)) Or " ^
5.24 + " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod_const False)) Or " ^
5.25 + " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod False)) Or " ^
5.26 + " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_quot True )) Or " ^
5.27 + " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin False)) Or " ^
5.28 + " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin_chain False)) Or " ^
5.29 + " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos False)) Or " ^
5.30 + " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos_chain False)) Or " ^
5.31 + " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow False)) Or " ^
5.32 + " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow_chain False)) Or " ^
5.33 + " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln False)) Or " ^
5.34 + " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln_chain False)) Or " ^
5.35 + " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp False)) Or " ^
5.36 + " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp_chain False)) Or " ^
5.37 + " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_const False)) Or " ^
5.38 + " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_var False)) Or " ^
5.39 + " (Repeat (Rewrite_Set make_polynomial False)))) @@ " ^
5.40 + " (Try (Rewrite_Set_Inst [(bdv,v_v)] diff_sym_conv False)))) f_f')"),
5.41 + prep_met thy "met_diff_simpl" [] e_metID
5.42 + (["diff","diff_simpl"],
5.43 + [("#Given" ,["functionTerm f_f","differentiateFor v_v"]),
5.44 + ("#Find" ,["derivative f_f'"])],
5.45 + {rew_ord'="tless_true", rls' = erls_diff, calc = [], srls = e_rls, prls=e_rls,
5.46 + crls = Atools_erls, errpats = [], nrls = norm_diff},
5.47 + "Script DiffScr (f_f::real) (v_v::real) = " ^
5.48 + " (let f_f' = Take (d_d v_v f_f) " ^
5.49 + " in (( " ^
5.50 + " (Repeat " ^
5.51 + " ((Repeat (Rewrite_Inst [(bdv,v_v)] diff_sum False)) Or " ^
5.52 + " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod_const False)) Or " ^
5.53 + " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod False)) Or " ^
5.54 + " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_quot True )) Or " ^
5.55 + " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin False)) Or " ^
5.56 + " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin_chain False)) Or " ^
5.57 + " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos False)) Or " ^
5.58 + " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos_chain False)) Or " ^
5.59 + " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow False)) Or " ^
5.60 + " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow_chain False)) Or " ^
5.61 + " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln False)) Or " ^
5.62 + " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln_chain False)) Or " ^
5.63 + " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp False)) Or " ^
5.64 + " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp_chain False)) Or " ^
5.65 + " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_const False)) Or " ^
5.66 + " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_var False)) Or " ^
5.67 + " (Repeat (Rewrite_Set make_polynomial False)))) " ^
5.68 + " )) f_f')"),
5.69 + prep_met thy "met_diff_equ" [] e_metID
5.70 + (["diff","differentiate_equality"],
5.71 + [("#Given" ,["functionEq f_f","differentiateFor v_v"]),
5.72 + ("#Find" ,["derivativeEq f_f'"])],
5.73 + {rew_ord'="tless_true", rls' = erls_diff, calc = [], srls = srls_diff, prls=e_rls,
5.74 + crls=Atools_erls, errpats = [], nrls = norm_diff},
5.75 + "Script DiffEqScr (f_f::bool) (v_v::real) = " ^
5.76 + " (let f_f' = Take ((primed (lhs f_f)) = d_d v_v (rhs f_f)) " ^
5.77 + " in (((Try (Rewrite_Set_Inst [(bdv,v_v)] diff_conv False)) @@ " ^
5.78 + " (Repeat " ^
5.79 + " ((Repeat (Rewrite_Inst [(bdv,v_v)] diff_sum False)) Or " ^
5.80 + " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_dif False)) Or " ^
5.81 + " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod_const False)) Or " ^
5.82 + " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod False)) Or " ^
5.83 + " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_quot True )) Or " ^
5.84 + " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin False)) Or " ^
5.85 + " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin_chain False)) Or " ^
5.86 + " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos False)) Or " ^
5.87 + " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos_chain False)) Or " ^
5.88 + " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow False)) Or " ^
5.89 + " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow_chain False)) Or " ^
5.90 + " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln False)) Or " ^
5.91 + " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln_chain False)) Or " ^
5.92 + " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp False)) Or " ^
5.93 + " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp_chain False)) Or " ^
5.94 + " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_const False)) Or " ^
5.95 + " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_var False)) Or " ^
5.96 + " (Repeat (Rewrite_Set make_polynomial False)))) @@ " ^
5.97 + " (Try (Rewrite_Set_Inst [(bdv,v_v)] diff_sym_conv False)))) f_f')"),
5.98 + prep_met thy "met_diff_after_simp" [] e_metID
5.99 + (["diff","after_simplification"],
5.100 + [("#Given" ,["functionTerm f_f","differentiateFor v_v"]),
5.101 + ("#Find" ,["derivative f_f'"])],
5.102 + {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls, prls=e_rls,
5.103 + crls=Atools_erls, errpats = [], nrls = norm_Rational},
5.104 + "Script DiffScr (f_f::real) (v_v::real) = " ^
5.105 + " (let f_f' = Take (d_d v_v f_f) " ^
5.106 + " in ((Try (Rewrite_Set norm_Rational False)) @@ " ^
5.107 + " (Try (Rewrite_Set_Inst [(bdv,v_v)] diff_conv False)) @@ " ^
5.108 + " (Try (Rewrite_Set_Inst [(bdv,v_v)] norm_diff False)) @@ " ^
5.109 + " (Try (Rewrite_Set_Inst [(bdv,v_v)] diff_sym_conv False)) @@ " ^
5.110 + " (Try (Rewrite_Set norm_Rational False))) f_f')")]
5.111 +*}
5.112 setup {* KEStore_Elems.add_cas
5.113 [((term_of o the o (parse thy)) "Diff",
5.114 (("Isac", ["derivative_of","function"], ["no_met"]), argl2dtss))] *}
6.1 --- a/src/Tools/isac/Knowledge/DiffApp.thy Fri Jan 31 17:50:50 2014 +0100
6.2 +++ b/src/Tools/isac/Knowledge/DiffApp.thy Sat Feb 01 16:44:45 2014 +0100
6.3 @@ -227,7 +227,87 @@
6.4 crls = eval_rls, errpats = [], nrls = norm_Rational(*,
6.5 asm_rls=[],asm_thm=[]*)},
6.6 "empty_script"));
6.7 -
6.8 +*}
6.9 +setup {* KEStore_Elems.add_mets
6.10 + [prep_met thy "met_diffapp" [] e_metID
6.11 + (["DiffApp"], [],
6.12 + {rew_ord'="tless_true", rls'=Atools_erls,calc = [], srls = e_rls, prls = e_rls,
6.13 + crls = Atools_erls, errpats = [], nrls = norm_Rational (*, asm_rls=[],asm_thm=[]*)},
6.14 + "empty_script"),
6.15 + prep_met thy "met_diffapp_max" [] e_metID
6.16 + (["DiffApp","max_by_calculus"]:metID,
6.17 + [("#Given" ,["fixedValues f_ix","maximum m_m","relations r_s", "boundVariable v_v",
6.18 + "interval i_tv","errorBound e_rr"]),
6.19 + ("#Find" ,["valuesFor v_s"]),
6.20 + ("#Relate",[])],
6.21 + {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls=list_rls,prls=e_rls, crls = eval_rls,
6.22 + errpats = [], nrls = norm_Rational (*, asm_rls=[],asm_thm=[]*)},
6.23 + "Script Maximum_value(f_ix::bool list)(m_m::real) (r_s::bool list) " ^
6.24 + " (v_v::real) (itv_v::real set) (e_rr::bool) = " ^
6.25 + " (let e_e = (hd o (filterVar m_m)) r_s; " ^
6.26 + " t_t = (if 1 < LENGTH r_s " ^
6.27 + " then (SubProblem (DiffApp',[make,function],[no_met]) " ^
6.28 + " [REAL m_m, REAL v_v, BOOL_LIST r_s]) " ^
6.29 + " else (hd r_s)); " ^
6.30 + " (m_x::real) = " ^
6.31 + "SubProblem(DiffApp',[on_interval,maximum_of,function], " ^
6.32 + " [DiffApp,max_on_interval_by_calculus]) " ^
6.33 + " [BOOL t_t, REAL v_v, REAL_SET i_tv] " ^
6.34 + " in ((SubProblem (DiffApp',[find_values,tool],[Isac,find_values]) " ^
6.35 + " [REAL m_x, REAL (Rhs t_t), REAL v_v, REAL m_m, " ^
6.36 + " BOOL_LIST (dropWhile (ident e_e) r_s)])::bool list)) "),
6.37 + prep_met thy "met_diffapp_funnew" [] e_metID
6.38 + (["DiffApp","make_fun_by_new_variable"]:metID,
6.39 + [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]),
6.40 + ("#Find" ,["functionEq f_1"])],
6.41 + {rew_ord'="tless_true",rls'=eval_rls,srls=list_rls,prls=e_rls, calc=[], crls = eval_rls,
6.42 + errpats = [], nrls = norm_Rational(*,asm_rls=[],asm_thm=[]*)},
6.43 + "Script Make_fun_by_new_variable (f_f::real) (v_v::real) " ^
6.44 + " (eqs::bool list) = " ^
6.45 + "(let h_h = (hd o (filterVar f_f)) eqs; " ^
6.46 + " e_s = dropWhile (ident h_h) eqs; " ^
6.47 + " v_s = dropWhile (ident f_f) (Vars h_h); " ^
6.48 + " v_1 = NTH 1 v_s; " ^
6.49 + " v_2 = NTH 2 v_s; " ^
6.50 + " e_1 = (hd o (filterVar v_1)) e_s; " ^
6.51 + " e_2 = (hd o (filterVar v_2)) e_s; " ^
6.52 + " (s_1::bool list) = " ^
6.53 + " (SubProblem (DiffApp',[univariate,equation],[no_met])" ^
6.54 + " [BOOL e_1, REAL v_1]); " ^
6.55 + " (s_2::bool list) = " ^
6.56 + " (SubProblem (DiffApp',[univariate,equation],[no_met])" ^
6.57 + " [BOOL e_2, REAL v_2])" ^
6.58 + "in Substitute [(v_1 = (rhs o hd) s_1),(v_2 = (rhs o hd) s_2)] h_h)"),
6.59 + prep_met thy "met_diffapp_funexp" [] e_metID
6.60 + (["DiffApp","make_fun_by_explicit"]:metID,
6.61 + [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]),
6.62 + ("#Find" ,["functionEq f_1"])],
6.63 + {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls=list_rls,prls=e_rls, crls = eval_rls,
6.64 + errpats = [], nrls = norm_Rational (*, asm_rls=[],asm_thm=[]*)},
6.65 + "Script Make_fun_by_explicit (f_f::real) (v_v::real) " ^
6.66 + " (eqs::bool list) = " ^
6.67 + " (let h_h = (hd o (filterVar f_f)) eqs; " ^
6.68 + " e_1 = hd (dropWhile (ident h_h) eqs); " ^
6.69 + " v_s = dropWhile (ident f_f) (Vars h_h); " ^
6.70 + " v_1 = hd (dropWhile (ident v_v) v_s); " ^
6.71 + " (s_1::bool list)= " ^
6.72 + " (SubProblem(DiffApp',[univariate,equation],[no_met])" ^
6.73 + " [BOOL e_1, REAL v_1]) " ^
6.74 + " in Substitute [(v_1 = (rhs o hd) s_1)] h_h) "),
6.75 + prep_met thy "met_diffapp_max_oninterval" [] e_metID
6.76 + (["DiffApp","max_on_interval_by_calculus"]:metID,
6.77 + [("#Given" ,["functionEq t_t","boundVariable v_v","interval i_tv"(*, "errorBound e_rr"*)]),
6.78 + ("#Find" ,["maxArgument v_0"])],
6.79 + {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls = e_rls,prls=e_rls, crls = eval_rls,
6.80 + errpats = [], nrls = norm_Rational (*, asm_rls=[],asm_thm=[]*)},
6.81 + "empty_script"),
6.82 + prep_met thy "met_diffapp_findvals" [] e_metID
6.83 + (["DiffApp","find_values"]:metID, [],
6.84 + {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls = e_rls,prls=e_rls, crls = eval_rls,
6.85 + errpats = [], nrls = norm_Rational(*, asm_rls = [], asm_thm = []*)},
6.86 + "empty_script")]
6.87 +*}
6.88 +ML {*
6.89 val list_rls = append_rls "list_rls" list_rls
6.90 [Thm ("filterVar_Const", num_str @{thm filterVar_Const}),
6.91 Thm ("filterVar_Nil", num_str @{thm filterVar_Nil})];
7.1 --- a/src/Tools/isac/Knowledge/DiophantEq.thy Fri Jan 31 17:50:50 2014 +0100
7.2 +++ b/src/Tools/isac/Knowledge/DiophantEq.thy Sat Feb 01 16:44:45 2014 +0100
7.3 @@ -47,5 +47,20 @@
7.4 " (Try (Calculate TIMES))) e_e::bool)"
7.5 ))
7.6 *}
7.7 +setup {* KEStore_Elems.add_mets
7.8 + [prep_met thy "met_test_diophant" [] e_metID
7.9 + (["Test","solve_diophant"]:metID,
7.10 + [("#Given" ,["boolTestGiven e_e","intTestGiven (v_v::int)"]),
7.11 + (* TODO: drop ^^^^^*)
7.12 + ("#Where" ,[]),
7.13 + ("#Find" ,["boolTestFind s_s"])],
7.14 + {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = e_rls, prls = e_rls, calc = [],
7.15 + crls = tval_rls, errpats = [], nrls = Test_simplify},
7.16 + "Script Diophant_equation (e_e::bool) (v_v::int)= " ^
7.17 + "(Repeat " ^
7.18 + " ((Try (Rewrite_Inst [(bdv,v_v::int)] int_isolate_add False)) @@" ^
7.19 + " (Try (Calculate PLUS)) @@ " ^
7.20 + " (Try (Calculate TIMES))) e_e::bool)")]
7.21 +*}
7.22
7.23 end
7.24 \ No newline at end of file
8.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Fri Jan 31 17:50:50 2014 +0100
8.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Sat Feb 01 16:44:45 2014 +0100
8.3 @@ -687,4 +687,145 @@
8.4 ));
8.5 *}
8.6
8.7 +setup {* KEStore_Elems.add_mets
8.8 + [prep_met thy "met_eqsys" [] e_metID
8.9 + (["EqSystem"], [],
8.10 + {rew_ord'="tless_true", rls' = Erls, calc = [], srls = Erls, prls = Erls, crls = Erls,
8.11 + errpats = [], nrls = Erls},
8.12 + "empty_script"),
8.13 + prep_met thy "met_eqsys_topdown" [] e_metID
8.14 + (["EqSystem","top_down_substitution"], [],
8.15 + {rew_ord'="tless_true", rls' = Erls, calc = [], srls = Erls, prls = Erls, crls = Erls,
8.16 + errpats = [], nrls = Erls},
8.17 + "empty_script"),
8.18 + prep_met thy "met_eqsys_topdown_2x2" [] e_metID
8.19 + (["EqSystem", "top_down_substitution", "2x2"],
8.20 + [("#Given", ["equalities e_s", "solveForVars v_s"]),
8.21 + ("#Where",
8.22 + ["(tl v_s) from v_s occur_exactly_in (NTH 1 (e_s::bool list))",
8.23 + " v_s from v_s occur_exactly_in (NTH 2 (e_s::bool list))"]),
8.24 + ("#Find" ,["solution ss'''"])],
8.25 + {rew_ord'="ord_simplify_System", rls' = Erls, calc = [],
8.26 + srls = append_rls "srls_top_down_2x2" e_rls
8.27 + [Thm ("hd_thm",num_str @{thm hd_thm}),
8.28 + Thm ("tl_Cons",num_str @{thm tl_Cons}),
8.29 + Thm ("tl_Nil",num_str @{thm tl_Nil})],
8.30 + prls = prls_triangular, crls = Erls, errpats = [], nrls = Erls},
8.31 + "Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^
8.32 + " (let e_1 = Take (hd e_s); " ^
8.33 + " e_1 = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
8.34 + " isolate_bdvs False)) @@ " ^
8.35 + " (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
8.36 + " simplify_System False))) e_1; " ^
8.37 + " e_2 = Take (hd (tl e_s)); " ^
8.38 + " e_2 = ((Substitute [e_1]) @@ " ^
8.39 + " (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
8.40 + " simplify_System_parenthesized False)) @@ " ^
8.41 + " (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
8.42 + " isolate_bdvs False)) @@ " ^
8.43 + " (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
8.44 + " simplify_System False))) e_2; " ^
8.45 + " e__s = Take [e_1, e_2] " ^
8.46 + " in (Try (Rewrite_Set order_system False)) e__s)"
8.47 + (*---------------------------------------------------------------------------
8.48 + this script does NOT separate the equations as above,
8.49 + but it does not yet work due to preliminary script-interpreter,
8.50 + see eqsystem.sml 'script [EqSystem,top_down_substitution,2x2] Vers.2'
8.51 +
8.52 + "Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^
8.53 + " (let e__s = Take e_s; " ^
8.54 + " e_1 = hd e__s; " ^
8.55 + " e_2 = hd (tl e__s); " ^
8.56 + " e__s = [e_1, Substitute [e_1] e_2] " ^
8.57 + " in ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
8.58 + " simplify_System_parenthesized False)) @@ " ^
8.59 + " (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))] " ^
8.60 + " isolate_bdvs False)) @@ " ^
8.61 + " (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
8.62 + " simplify_System False))) e__s)"
8.63 + ---------------------------------------------------------------------------*)),
8.64 + prep_met thy "met_eqsys_norm" [] e_metID
8.65 + (["EqSystem", "normalize"], [],
8.66 + {rew_ord'="tless_true", rls' = Erls, calc = [], srls = Erls, prls = Erls, crls = Erls,
8.67 + errpats = [], nrls = Erls},
8.68 + "empty_script"),
8.69 + prep_met thy "met_eqsys_norm_2x2" [] e_metID
8.70 + (["EqSystem","normalize","2x2"],
8.71 + [("#Given" ,["equalities e_s", "solveForVars v_s"]),
8.72 + ("#Find" ,["solution ss'''"])],
8.73 + {rew_ord'="tless_true", rls' = Erls, calc = [],
8.74 + srls = append_rls "srls_normalize_2x2" e_rls
8.75 + [Thm ("hd_thm",num_str @{thm hd_thm}),
8.76 + Thm ("tl_Cons",num_str @{thm tl_Cons}),
8.77 + Thm ("tl_Nil",num_str @{thm tl_Nil})],
8.78 + prls = Erls, crls = Erls, errpats = [], nrls = Erls},
8.79 + "Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^
8.80 + " (let e__s = ((Try (Rewrite_Set norm_Rational False)) @@ " ^
8.81 + " (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
8.82 + " simplify_System_parenthesized False)) @@ " ^
8.83 + " (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
8.84 + " isolate_bdvs False)) @@ " ^
8.85 + " (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
8.86 + " simplify_System_parenthesized False)) @@ " ^
8.87 + " (Try (Rewrite_Set order_system False))) e_s " ^
8.88 + " in (SubProblem (EqSystem',[LINEAR,system],[no_met]) " ^
8.89 + " [BOOL_LIST e__s, REAL_LIST v_s]))"),
8.90 + prep_met thy "met_eqsys_norm_4x4" [] e_metID
8.91 + (["EqSystem","normalize","4x4"],
8.92 + [("#Given" ,["equalities e_s", "solveForVars v_s"]),
8.93 + ("#Find" ,["solution ss'''"])],
8.94 + {rew_ord'="tless_true", rls' = Erls, calc = [],
8.95 + srls = append_rls "srls_normalize_4x4" srls
8.96 + [Thm ("hd_thm",num_str @{thm hd_thm}),
8.97 + Thm ("tl_Cons",num_str @{thm tl_Cons}),
8.98 + Thm ("tl_Nil",num_str @{thm tl_Nil})],
8.99 + prls = Erls, crls = Erls, errpats = [], nrls = Erls},
8.100 + (*STOPPED.WN06? met ["EqSystem","normalize","4x4"] @@@@@@@@@@@@@@@@@@@@@@@@@@@*)
8.101 + "Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^
8.102 + " (let e__s = " ^
8.103 + " ((Try (Rewrite_Set norm_Rational False)) @@ " ^
8.104 + " (Repeat (Rewrite commute_0_equality False)) @@ " ^
8.105 + " (Try (Rewrite_Set_Inst [(bdv_1, NTH 1 v_s),(bdv_2, NTH 2 v_s ), " ^
8.106 + " (bdv_3, NTH 3 v_s),(bdv_3, NTH 4 v_s )] " ^
8.107 + " simplify_System_parenthesized False)) @@ " ^
8.108 + " (Try (Rewrite_Set_Inst [(bdv_1, NTH 1 v_s),(bdv_2, NTH 2 v_s ), " ^
8.109 + " (bdv_3, NTH 3 v_s),(bdv_3, NTH 4 v_s )] " ^
8.110 + " isolate_bdvs_4x4 False)) @@ " ^
8.111 + " (Try (Rewrite_Set_Inst [(bdv_1, NTH 1 v_s),(bdv_2, NTH 2 v_s ), " ^
8.112 + " (bdv_3, NTH 3 v_s),(bdv_3, NTH 4 v_s )] " ^
8.113 + " simplify_System_parenthesized False)) @@ " ^
8.114 + " (Try (Rewrite_Set order_system False))) e_s " ^
8.115 + " in (SubProblem (EqSystem',[LINEAR,system],[no_met]) " ^
8.116 + " [BOOL_LIST e__s, REAL_LIST v_s]))"),
8.117 + prep_met thy "met_eqsys_topdown_4x4" [] e_metID
8.118 + (["EqSystem","top_down_substitution","4x4"],
8.119 + [("#Given" ,["equalities e_s", "solveForVars v_s"]),
8.120 + ("#Where" , (*accepts missing variables up to diagonal form*)
8.121 + ["(NTH 1 (v_s::real list)) occurs_in (NTH 1 (e_s::bool list))",
8.122 + "(NTH 2 (v_s::real list)) occurs_in (NTH 2 (e_s::bool list))",
8.123 + "(NTH 3 (v_s::real list)) occurs_in (NTH 3 (e_s::bool list))",
8.124 + "(NTH 4 (v_s::real list)) occurs_in (NTH 4 (e_s::bool list))"]),
8.125 + ("#Find", ["solution ss'''"])],
8.126 + {rew_ord'="ord_simplify_System", rls' = Erls, calc = [],
8.127 + srls = append_rls "srls_top_down_4x4" srls [],
8.128 + prls = append_rls "prls_tri_4x4_lin_sys" prls_triangular
8.129 + [Calc ("Atools.occurs'_in",eval_occurs_in "")],
8.130 + crls = Erls, errpats = [], nrls = Erls},
8.131 + (*FIXXXXME.WN060916: this script works ONLY for exp 7.79 @@@@@@@@@@@@@@@@@@@@*)
8.132 + "Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^
8.133 + " (let e_1 = NTH 1 e_s; " ^
8.134 + " e_2 = Take (NTH 2 e_s); " ^
8.135 + " e_2 = ((Substitute [e_1]) @@ " ^
8.136 + " (Try (Rewrite_Set_Inst [(bdv_1,NTH 1 v_s),(bdv_2,NTH 2 v_s)," ^
8.137 + " (bdv_3,NTH 3 v_s),(bdv_4,NTH 4 v_s)]" ^
8.138 + " simplify_System_parenthesized False)) @@ " ^
8.139 + " (Try (Rewrite_Set_Inst [(bdv_1,NTH 1 v_s),(bdv_2,NTH 2 v_s)," ^
8.140 + " (bdv_3,NTH 3 v_s),(bdv_4,NTH 4 v_s)]" ^
8.141 + " isolate_bdvs False)) @@ " ^
8.142 + " (Try (Rewrite_Set_Inst [(bdv_1,NTH 1 v_s),(bdv_2,NTH 2 v_s)," ^
8.143 + " (bdv_3,NTH 3 v_s),(bdv_4,NTH 4 v_s)]" ^
8.144 + " norm_Rational False))) e_2 " ^
8.145 + " in [e_1, e_2, NTH 3 e_s, NTH 4 e_s])")]
8.146 +*}
8.147 +
8.148 end
8.149 \ No newline at end of file
9.1 --- a/src/Tools/isac/Knowledge/Equation.thy Fri Jan 31 17:50:50 2014 +0100
9.2 +++ b/src/Tools/isac/Knowledge/Equation.thy Sat Feb 01 16:44:45 2014 +0100
9.3 @@ -97,5 +97,12 @@
9.4 "empty_script"
9.5 ));
9.6 *}
9.7 +setup {* KEStore_Elems.add_mets
9.8 + [prep_met thy "met_equ" [] e_metID
9.9 + (["Equation"], [],
9.10 + {rew_ord'="tless_true", rls'=Erls, calc = [], srls = e_rls, prls=e_rls, crls = Atools_erls,
9.11 + errpats = [], nrls = e_rls},
9.12 + "empty_script")]
9.13 +*}
9.14
9.15 end
9.16 \ No newline at end of file
10.1 --- a/src/Tools/isac/Knowledge/InsSort.thy Fri Jan 31 17:50:50 2014 +0100
10.2 +++ b/src/Tools/isac/Knowledge/InsSort.thy Sat Feb 01 16:44:45 2014 +0100
10.3 @@ -89,6 +89,19 @@
10.4 "Script Sort (u_::'a list) = (Rewrite_Set ins_sort False) u_"
10.5 ));
10.6 *}
10.7 +setup {* KEStore_Elems.add_mets
10.8 + [prep_met @{theory "Diff"}
10.9 + (["InsSort"], [],
10.10 + {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
10.11 + crls = Atools_rls, errpats = [], nrls = norm_Rational (*, asm_rls=[],asm_thm=[]*)},
10.12 + "empty_script"),
10.13 + prep_met @{theory "InsSort"} (*test-version for [#1,#3,#2] only: see *.sml*)
10.14 + (["InsSort","sort"]:metID,
10.15 + [("#Given" ,["unsorted u_"]), ("#Find" ,["sorted s_"])],
10.16 + {rew_ord'="tless_true",rls'=eval_rls,calc = [], srls = e_rls, prls=e_rls, crls = eval_rls,
10.17 + errpats = [], nrls = norm_Rational},
10.18 + "Script Sort (u_::'a list) = (Rewrite_Set ins_sort False) u_")]
10.19 +*}
10.20 setup {* KEStore_Elems.add_rlss [("ins_sort", (Context.theory_name @{theory}, ins_sort))] *}
10.21
10.22 end
11.1 --- a/src/Tools/isac/Knowledge/Integrate.thy Fri Jan 31 17:50:50 2014 +0100
11.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy Sat Feb 01 16:44:45 2014 +0100
11.3 @@ -387,5 +387,25 @@
11.4 " (Rewrite_Set_Inst [(bdv,v_v)] integration False)) t_t) "
11.5 ));
11.6 *}
11.7 +setup {* KEStore_Elems.add_mets
11.8 + [prep_met thy "met_diffint" [] e_metID
11.9 + (["diff","integration"],
11.10 + [("#Given" ,["functionTerm f_f", "integrateBy v_v"]), ("#Find" ,["antiDerivative F_F"])],
11.11 + {rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = e_rls, prls=e_rls,
11.12 + crls = Atools_erls, errpats = [], nrls = e_rls},
11.13 + "Script IntegrationScript (f_f::real) (v_v::real) = " ^
11.14 + " (let t_t = Take (Integral f_f D v_v) " ^
11.15 + " in (Rewrite_Set_Inst [(bdv,v_v)] integration False) (t_t::real))"),
11.16 + prep_met thy "met_diffint_named" [] e_metID
11.17 + (["diff","integration","named"],
11.18 + [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
11.19 + ("#Find" ,["antiDerivativeName F_F"])],
11.20 + {rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = e_rls, prls=e_rls,
11.21 + crls = Atools_erls, errpats = [], nrls = e_rls},
11.22 + "Script NamedIntegrationScript (f_f::real) (v_v::real) (F_F::real=>real) = " ^
11.23 + " (let t_t = Take (F_F v_v = Integral f_f D v_v) " ^
11.24 + " in ((Try (Rewrite_Set_Inst [(bdv,v_v)] simplify_Integral False)) @@ " ^
11.25 + " (Rewrite_Set_Inst [(bdv,v_v)] integration False)) t_t) ")]
11.26 +*}
11.27
11.28 end
11.29 \ No newline at end of file
12.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Fri Jan 31 17:50:50 2014 +0100
12.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Sat Feb 01 16:44:45 2014 +0100
12.3 @@ -246,6 +246,169 @@
12.4 ));
12.5
12.6 *}
12.7 +setup {* KEStore_Elems.add_mets
12.8 + [prep_met thy "met_SP" [] e_metID
12.9 + (["SignalProcessing"], [],
12.10 + {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls, crls = e_rls,
12.11 + errpats = [], nrls = e_rls}, "empty_script"),
12.12 + prep_met thy "met_SP_Ztrans" [] e_metID
12.13 + (["SignalProcessing", "Z_Transform"], [],
12.14 + {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls, crls = e_rls,
12.15 + errpats = [], nrls = e_rls}, "empty_script"),
12.16 + prep_met thy "met_SP_Ztrans_inv" [] e_metID
12.17 + (["SignalProcessing", "Z_Transform", "Inverse"],
12.18 + [("#Given" ,["filterExpression (X_eq::bool)"]),
12.19 + ("#Find" ,["stepResponse (n_eq::bool)"])],
12.20 + {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls, crls = e_rls,
12.21 + errpats = [], nrls = e_rls},
12.22 + "Script InverseZTransform (X_eq::bool) =" ^ (*(1/z) instead of z ^^^ -1*)
12.23 + " (let X = Take X_eq;" ^
12.24 + " X' = Rewrite ruleZY False X;" ^ (*z * denominator*)
12.25 + " X' = (Rewrite_Set norm_Rational False) X';" ^ (*simplify*)
12.26 + " funterm = Take (rhs X');" ^ (*drop X' z = for equation solving*)
12.27 + " denom = (Rewrite_Set partial_fraction False) funterm;" ^ (*get_denominator*)
12.28 + " equ = (denom = (0::real));" ^
12.29 + " fun_arg = Take (lhs X');" ^
12.30 + " arg = (Rewrite_Set partial_fraction False) X';" ^ (*get_argument TODO*)
12.31 + " (L_L::bool list) = " ^
12.32 + " (SubProblem (Test', " ^
12.33 + " [LINEAR,univariate,equation,test]," ^
12.34 + " [Test,solve_linear]) " ^
12.35 + " [BOOL equ, REAL z]) " ^
12.36 + " in X)"),
12.37 + prep_met thy "met_SP_Ztrans_inv" [] e_metID
12.38 + (["SignalProcessing", "Z_Transform", "Inverse"],
12.39 + [("#Given" ,["filterExpression X_eq"]),
12.40 + ("#Find" ,["stepResponse n_eq"])],
12.41 + {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = srls_partial_fraction, prls = e_rls,
12.42 + crls = e_rls, errpats = [], nrls = e_rls},
12.43 + "Script InverseZTransform (X_eq::bool) = "^
12.44 + (*(1/z) instead of z ^^^ -1*)
12.45 + "(let X = Take X_eq; "^
12.46 + " X' = Rewrite ruleZY False X; "^
12.47 + (*z * denominator*)
12.48 + " (num_orig::real) = get_numerator (rhs X'); "^
12.49 + " X' = (Rewrite_Set norm_Rational False) X'; "^
12.50 + (*simplify*)
12.51 + " (X'_z::real) = lhs X'; "^
12.52 + " (zzz::real) = argument_in X'_z; "^
12.53 + " (funterm::real) = rhs X'; "^
12.54 + (*drop X' z = for equation solving*)
12.55 + " (denom::real) = get_denominator funterm; "^
12.56 + (*get_denominator*)
12.57 + " (num::real) = get_numerator funterm; "^
12.58 + (*get_numerator*)
12.59 + " (equ::bool) = (denom = (0::real)); "^
12.60 + " (L_L::bool list) = (SubProblem (PolyEq', "^
12.61 + " [abcFormula,degree_2,polynomial,univariate,equation], "^
12.62 + " [no_met]) "^
12.63 + " [BOOL equ, REAL zzz]); "^
12.64 + " (facs::real) = factors_from_solution L_L; "^
12.65 + " (eql::real) = Take (num_orig / facs); "^
12.66 +
12.67 + " (eqr::real) = (Try (Rewrite_Set ansatz_rls False)) eql; "^
12.68 +
12.69 + " (eq::bool) = Take (eql = eqr); "^
12.70 + (*Maybe possible to use HOLogic.mk_eq ??*)
12.71 + " eq = (Try (Rewrite_Set equival_trans False)) eq; "^
12.72 +
12.73 + " eq = drop_questionmarks eq; "^
12.74 + " (z1::real) = (rhs (NTH 1 L_L)); "^
12.75 + (*
12.76 + * prepare equation for a - eq_a
12.77 + * therefor substitute z with solution 1 - z1
12.78 + *)
12.79 + " (z2::real) = (rhs (NTH 2 L_L)); "^
12.80 +
12.81 + " (eq_a::bool) = Take eq; "^
12.82 + " eq_a = (Substitute [zzz=z1]) eq; "^
12.83 + " eq_a = (Rewrite_Set norm_Rational False) eq_a; "^
12.84 + " (sol_a::bool list) = "^
12.85 + " (SubProblem (Isac', "^
12.86 + " [univariate,equation],[no_met]) "^
12.87 + " [BOOL eq_a, REAL (A::real)]); "^
12.88 + " (a::real) = (rhs(NTH 1 sol_a)); "^
12.89 +
12.90 + " (eq_b::bool) = Take eq; "^
12.91 + " eq_b = (Substitute [zzz=z2]) eq_b; "^
12.92 + " eq_b = (Rewrite_Set norm_Rational False) eq_b; "^
12.93 + " (sol_b::bool list) = "^
12.94 + " (SubProblem (Isac', "^
12.95 + " [univariate,equation],[no_met]) "^
12.96 + " [BOOL eq_b, REAL (B::real)]); "^
12.97 + " (b::real) = (rhs(NTH 1 sol_b)); "^
12.98 +
12.99 + " eqr = drop_questionmarks eqr; "^
12.100 + " (pbz::real) = Take eqr; "^
12.101 + " pbz = ((Substitute [A=a, B=b]) pbz); "^
12.102 +
12.103 + " pbz = Rewrite ruleYZ False pbz; "^
12.104 + " pbz = drop_questionmarks pbz; "^
12.105 +
12.106 + " (X_z::bool) = Take (X_z = pbz); "^
12.107 + " (n_eq::bool) = (Rewrite_Set inverse_z False) X_z; "^
12.108 + " n_eq = drop_questionmarks n_eq "^
12.109 + "in n_eq)"),
12.110 + prep_met thy "met_SP_Ztrans_inv_sub" [] e_metID
12.111 + (["SignalProcessing", "Z_Transform", "Inverse_sub"],
12.112 + [("#Given" ,["filterExpression X_eq"]),
12.113 + ("#Find" ,["stepResponse n_eq"])],
12.114 + {rew_ord'="tless_true", rls'= e_rls, calc = [],
12.115 + srls = Rls {id="srls_partial_fraction",
12.116 + preconds = [], rew_ord = ("termlessI",termlessI),
12.117 + erls = append_rls "erls_in_srls_partial_fraction" e_rls
12.118 + [(*for asm in NTH_CONS ...*)
12.119 + Calc ("Orderings.ord_class.less",eval_equ "#less_"),
12.120 + (*2nd NTH_CONS pushes n+-1 into asms*)
12.121 + Calc("Groups.plus_class.plus", eval_binop "#add_")],
12.122 + srls = Erls, calc = [], errpatts = [],
12.123 + rules = [Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
12.124 + Calc ("Groups.plus_class.plus", eval_binop "#add_"),
12.125 + Thm ("NTH_NIL",num_str @{thm NTH_NIL}),
12.126 + Calc ("Tools.lhs", eval_lhs "eval_lhs_"),
12.127 + Calc ("Tools.rhs", eval_rhs"eval_rhs_"),
12.128 + Calc ("Atools.argument'_in", eval_argument_in "Atools.argument'_in"),
12.129 + Calc ("Rational.get_denominator", eval_get_denominator "#get_denominator"),
12.130 + Calc ("Rational.get_numerator", eval_get_numerator "#get_numerator"),
12.131 + Calc ("Partial_Fractions.factors_from_solution",
12.132 + eval_factors_from_solution "#factors_from_solution"),
12.133 + Calc("Partial_Fractions.drop_questionmarks", eval_drop_questionmarks "#drop_?")],
12.134 + scr = EmptyScr},
12.135 + prls = e_rls, crls = e_rls, errpats = [], nrls = norm_Rational},
12.136 + (*([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])*)
12.137 + "Script InverseZTransform (X_eq::bool) = "^
12.138 + (*([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))*)
12.139 + "(let X = Take X_eq; "^
12.140 + (*([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
12.141 + " X' = Rewrite ruleZY False X; "^
12.142 + (* ?X' z*)
12.143 + " (X'_z::real) = lhs X'; "^
12.144 + (* z *)
12.145 + " (zzz::real) = argument_in X'_z; "^
12.146 + (* 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
12.147 + " (funterm::real) = rhs X'; "^
12.148 +
12.149 + " (pbz::real) = (SubProblem (Isac', "^
12.150 + " [partial_fraction,rational,simplification], "^
12.151 + " [simplification,of_rationals,to_partial_fraction]) "^
12.152 + (*([2], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
12.153 + " [REAL funterm, REAL zzz]); "^
12.154 +
12.155 + (*([3], Frm), ?X' z = 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
12.156 + " (pbz_eq::bool) = Take (X'_z = pbz); "^
12.157 + (*([3], Res), ?X' z = 4 * (?z / (z - 1 / 2)) + -4 * (?z / (z - -1 / 4))*)
12.158 + " pbz_eq = Rewrite ruleYZ False pbz_eq; "^
12.159 + (* 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
12.160 + " pbz_eq = drop_questionmarks pbz_eq; "^
12.161 + (*([4], Frm), X_z = 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
12.162 + " (X_zeq::bool) = Take (X_z = rhs pbz_eq); "^
12.163 + (*([4], Res), X_z = 4 * (1 / 2) ^^^ ?n * ?u [?n] + -4 * (-1 / 4) ^^^ ?n * ?u [?n]*)
12.164 + " n_eq = (Rewrite_Set inverse_z False) X_zeq; "^
12.165 + (* X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
12.166 + " n_eq = drop_questionmarks n_eq "^
12.167 + (*([], Res), X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
12.168 + "in n_eq)")]
12.169 +*}
12.170
12.171 end
12.172
13.1 --- a/src/Tools/isac/Knowledge/LinEq.thy Fri Jan 31 17:50:50 2014 +0100
13.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy Sat Feb 01 16:44:45 2014 +0100
13.3 @@ -164,9 +164,35 @@
13.4 " (Repeat(Try (Rewrite_Set LinPoly_simplify False)))) e_e " ^
13.5 " in ((Or_to_List e_e)::bool list))"
13.6 ));
13.7 -get_met ["LinEq","solve_lineq_equation"];
13.8 -
13.9 *}
13.10 +(*-------------- methods------------------------------------------------------*)
13.11 +setup {* KEStore_Elems.add_mets
13.12 + [prep_met thy "met_eqlin" [] e_metID
13.13 + (["LinEq"], [],
13.14 + {rew_ord' = "tless_true",rls' = Atools_erls,calc = [], srls = e_rls, prls = e_rls,
13.15 + crls = LinEq_crls, errpats = [], nrls = norm_Poly},
13.16 + "empty_script"),
13.17 + (* ansprechen mit ["LinEq","solve_univar_equation"] *)
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)", "((lhs e_e) has_degree_in v_v) = 1"]),
13.22 + ("#Find", ["solutions v_v'i'"])],
13.23 + {rew_ord' = "termlessI", rls' = LinEq_erls, srls = e_rls, prls = LinEq_prls, calc = [],
13.24 + crls = LinEq_crls, errpats = [], nrls = norm_Poly},
13.25 + "Script Solve_lineq_equation (e_e::bool) (v_v::real) = " ^
13.26 + "(let e_e =((Try (Rewrite all_left False)) @@ " ^
13.27 + " (Try (Repeat (Rewrite makex1_x False))) @@ " ^
13.28 + " (Try (Rewrite_Set expand_binoms False)) @@ " ^
13.29 + " (Try (Repeat (Rewrite_Set_Inst [(bdv, v_v::real)] " ^
13.30 + " make_ratpoly_in False))) @@ " ^
13.31 + " (Try (Repeat (Rewrite_Set LinPoly_simplify False))))e_e;" ^
13.32 + " e_e = ((Try (Rewrite_Set_Inst [(bdv, v_v::real)] " ^
13.33 + " LinEq_simplify True)) @@ " ^
13.34 + " (Repeat(Try (Rewrite_Set LinPoly_simplify False)))) e_e " ^
13.35 + " in ((Or_to_List e_e)::bool list))")]
13.36 +*}
13.37 +ML {* get_met ["LinEq","solve_lineq_equation"]; *}
13.38
13.39 end
13.40
14.1 --- a/src/Tools/isac/Knowledge/LogExp.thy Fri Jan 31 17:50:50 2014 +0100
14.2 +++ b/src/Tools/isac/Knowledge/LogExp.thy Sat Feb 01 16:44:45 2014 +0100
14.3 @@ -55,5 +55,20 @@
14.4 " in [e_e])"
14.5 ));
14.6 *}
14.7 +(** methods **)
14.8 +setup {* KEStore_Elems.add_mets
14.9 + [prep_met thy "met_equ_log" [] e_metID
14.10 + (["Equation","solve_log"],
14.11 + [("#Given" ,["equality e_e","solveFor v_v"]),
14.12 + ("#Where" ,["matches ((?a log ?v_v) = ?b) e_e"]),
14.13 + ("#Find" ,["solutions v_v'i'"])],
14.14 + {rew_ord' = "termlessI", rls' = PolyEq_erls, srls = e_rls, prls = PolyEq_prls, calc = [],
14.15 + crls = PolyEq_crls, errpats = [], nrls = norm_Rational},
14.16 + "Script Solve_log (e_e::bool) (v_v::real) = " ^
14.17 + "(let e_e = ((Rewrite equality_power False) @@ " ^
14.18 + " (Rewrite exp_invers_log False) @@ " ^
14.19 + " (Rewrite_Set norm_Poly False)) e_e " ^
14.20 + " in [e_e])")]
14.21 +*}
14.22
14.23 end
14.24 \ No newline at end of file
15.1 --- a/src/Tools/isac/Knowledge/Partial_Fractions.thy Fri Jan 31 17:50:50 2014 +0100
15.2 +++ b/src/Tools/isac/Knowledge/Partial_Fractions.thy Sat Feb 01 16:44:45 2014 +0100
15.3 @@ -274,6 +274,87 @@
15.4 "in pbz)" (*([], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
15.5 ));
15.6 *}
15.7 +setup {* KEStore_Elems.add_mets
15.8 + [prep_met @{theory} "met_partial_fraction" [] e_metID
15.9 + (["simplification","of_rationals","to_partial_fraction"],
15.10 + [("#Given" ,["functionTerm t_t", "solveFor v_v"]),
15.11 + (*("#Where" ,["((get_numerator t_t) has_degree_in v_v) <
15.12 + ((get_denominator t_t) has_degree_in v_v)"]), TODO*)
15.13 + ("#Find" ,["decomposedFunction p_p'''"])],
15.14 + (*f_f = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)), zzz: z*)
15.15 + {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = srls_partial_fraction, prls = e_rls,
15.16 + crls = e_rls, errpats = [], nrls = e_rls},
15.17 + (*([], Frm), Problem (Partial_Fractions, [partial_fraction, rational, simplification])*)
15.18 + "Script PartFracScript (f_f::real) (zzz::real) = " ^
15.19 + (*([1], Frm), 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
15.20 + "(let f_f = Take f_f; " ^
15.21 + (* num_orig = 3*)
15.22 + " (num_orig::real) = get_numerator f_f; " ^
15.23 + (*([1], Res), 24 / (-1 + -2 * z + 8 * z ^^^ 2)*)
15.24 + " f_f = (Rewrite_Set norm_Rational False) f_f; " ^
15.25 + (* denom = -1 + -2 * z + 8 * z ^^^ 2*)
15.26 + " (denom::real) = get_denominator f_f; " ^
15.27 + (* equ = -1 + -2 * z + 8 * z ^^^ 2 = 0*)
15.28 + " (equ::bool) = (denom = (0::real)); " ^
15.29 +
15.30 + (*([2], Pbl), solve (-1 + -2 * z + 8 * z ^^^ 2 = 0, z)*)
15.31 + " (L_L::bool list) = (SubProblem (PolyEq', " ^
15.32 + " [abcFormula, degree_2, polynomial, univariate, equation], " ^
15.33 + (*([2], Res), [z = 1 / 2, z = -1 / 4]*)
15.34 + " [no_met]) [BOOL equ, REAL zzz]); " ^
15.35 + (* facs: (z - 1 / 2) * (z - -1 / 4)*)
15.36 + " (facs::real) = factors_from_solution L_L; " ^
15.37 + (*([3], Frm), 33 / ((z - 1 / 2) * (z - -1 / 4)) *)
15.38 + " (eql::real) = Take (num_orig / facs); " ^
15.39 + (*([3], Res), ?A / (z - 1 / 2) + ?B / (z - -1 / 4)*)
15.40 + " (eqr::real) = (Try (Rewrite_Set ansatz_rls False)) eql; " ^
15.41 + (*([4], Frm), 3 / ((z - 1 / 2) * (z - -1 / 4)) = ?A / (z - 1 / 2) + ?B / (z - -1 / 4)*)
15.42 + " (eq::bool) = Take (eql = eqr); " ^
15.43 + (*([4], Res), 3 = ?A * (z - -1 / 4) + ?B * (z - 1 / 2)*)
15.44 + " eq = (Try (Rewrite_Set equival_trans False)) eq;" ^
15.45 + (* eq = 3 = A * (z - -1 / 4) + B * (z - 1 / 2)*)
15.46 + " eq = drop_questionmarks eq; " ^
15.47 + (* z1 = 1 / 2*)
15.48 + " (z1::real) = (rhs (NTH 1 L_L)); " ^
15.49 + (* z2 = -1 / 4*)
15.50 + " (z2::real) = (rhs (NTH 2 L_L)); " ^
15.51 + (*([5], Frm), 3 = A * (z - -1 / 4) + B * (z - 1 / 2)*)
15.52 + " (eq_a::bool) = Take eq; " ^
15.53 + (*([5], Res), 3 = A * (1 / 2 - -1 / 4) + B * (1 / 2 - 1 / 2)*)
15.54 + " eq_a = (Substitute [zzz = z1]) eq; " ^
15.55 + (*([6], Res), 3 = 3 * A / 4*)
15.56 + " eq_a = (Rewrite_Set norm_Rational False) eq_a; " ^
15.57 +
15.58 + (*([7], Pbl), solve (3 = 3 * A / 4, A)*)
15.59 + " (sol_a::bool list) = " ^
15.60 + " (SubProblem (Isac', [univariate,equation], [no_met]) " ^
15.61 + (*([7], Res), [A = 4]*)
15.62 + " [BOOL eq_a, REAL (A::real)]); " ^
15.63 + (* a = 4*)
15.64 + " (a::real) = (rhs (NTH 1 sol_a)); " ^
15.65 + (*([8], Frm), 3 = A * (z - -1 / 4) + B * (z - 1 / 2)*)
15.66 + " (eq_b::bool) = Take eq; " ^
15.67 + (*([8], Res), 3 = A * (-1 / 4 - -1 / 4) + B * (-1 / 4 - 1 / 2)*)
15.68 + " eq_b = (Substitute [zzz = z2]) eq_b; " ^
15.69 + (*([9], Res), 3 = -3 * B / 4*)
15.70 + " eq_b = (Rewrite_Set norm_Rational False) eq_b; " ^
15.71 + (*([10], Pbl), solve (3 = -3 * B / 4, B)*)
15.72 + " (sol_b::bool list) = " ^
15.73 + " (SubProblem (Isac', [univariate,equation], [no_met]) " ^
15.74 + (*([10], Res), [B = -4]*)
15.75 + " [BOOL eq_b, REAL (B::real)]); " ^
15.76 + (* b = -4*)
15.77 + " (b::real) = (rhs (NTH 1 sol_b)); " ^
15.78 + (* eqr = A / (z - 1 / 2) + B / (z - -1 / 4)*)
15.79 + " eqr = drop_questionmarks eqr; " ^
15.80 + (*([11], Frm), A / (z - 1 / 2) + B / (z - -1 / 4)*)
15.81 + " (pbz::real) = Take eqr; " ^
15.82 + (*([11], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
15.83 + " pbz = ((Substitute [A = a, B = b]) pbz) " ^
15.84 + (*([], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
15.85 + "in pbz)"
15.86 +)]
15.87 +*}
15.88 ML {*
15.89 (*
15.90 val fmz =
16.1 --- a/src/Tools/isac/Knowledge/Poly.thy Fri Jan 31 17:50:50 2014 +0100
16.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Sat Feb 01 16:44:45 2014 +0100
16.3 @@ -1626,5 +1626,19 @@
16.4 " ((Rewrite_Set norm_Poly False) t_t)"
16.5 ));
16.6 *}
16.7 +setup {* KEStore_Elems.add_mets
16.8 + [prep_met thy "met_simp_poly" [] e_metID
16.9 + (["simplification","for_polynomials"],
16.10 + [("#Given" ,["Term t_t"]),
16.11 + ("#Where" ,["t_t is_polyexp"]),
16.12 + ("#Find" ,["normalform n_n"])],
16.13 + {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls,
16.14 + prls = append_rls "simplification_for_polynomials_prls" e_rls
16.15 + [(*for preds in where_*)
16.16 + Calc ("Poly.is'_polyexp",eval_is_polyexp"")],
16.17 + crls = e_rls, errpats = [], nrls = norm_Poly},
16.18 + "Script SimplifyScript (t_t::real) = " ^
16.19 + " ((Rewrite_Set norm_Poly False) t_t)")]
16.20 +*}
16.21
16.22 end
17.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Fri Jan 31 17:50:50 2014 +0100
17.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Sat Feb 01 16:44:45 2014 +0100
17.3 @@ -1239,6 +1239,185 @@
17.4 " in ((Or_to_List e_e)::bool list))"
17.5 ));
17.6 *}
17.7 +text {* "-------------------------methods-----------------------" *}
17.8 +setup {* KEStore_Elems.add_mets
17.9 + [prep_met thy "met_polyeq" [] e_metID
17.10 + (["PolyEq"], [],
17.11 + {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
17.12 + crls=PolyEq_crls, errpats = [], nrls = norm_Rational},
17.13 + "empty_script"),
17.14 + prep_met thy "met_polyeq_norm" [] e_metID
17.15 + (["PolyEq","normalize_poly"],
17.16 + [("#Given" ,["equality e_e","solveFor v_v"]),
17.17 + ("#Where" ,["(Not((matches (?a = 0 ) e_e ))) |(Not(((lhs e_e) is_poly_in v_v)))"]),
17.18 + ("#Find" ,["solutions v_v'i'"])],
17.19 + {rew_ord'="termlessI", rls'=PolyEq_erls, srls=e_rls, prls=PolyEq_prls, calc=[],
17.20 + crls=PolyEq_crls, errpats = [], nrls = norm_Rational},
17.21 + "Script Normalize_poly (e_e::bool) (v_v::real) = " ^
17.22 + "(let e_e =((Try (Rewrite all_left False)) @@ " ^
17.23 + " (Try (Repeat (Rewrite makex1_x False))) @@ " ^
17.24 + " (Try (Repeat (Rewrite_Set expand_binoms False))) @@ " ^
17.25 + " (Try (Repeat (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
17.26 + " make_ratpoly_in False))) @@ " ^
17.27 + " (Try (Repeat (Rewrite_Set polyeq_simplify False)))) e_e " ^
17.28 + " in (SubProblem (PolyEq',[polynomial,univariate,equation], [no_met]) " ^
17.29 + " [BOOL e_e, REAL v_v]))"),
17.30 + prep_met thy "met_polyeq_d0" [] e_metID
17.31 + (["PolyEq","solve_d0_polyeq_equation"],
17.32 + [("#Given" ,["equality e_e","solveFor v_v"]),
17.33 + ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 0"]),
17.34 + ("#Find" ,["solutions v_v'i'"])],
17.35 + {rew_ord'="termlessI", rls'=PolyEq_erls, srls=e_rls, prls=PolyEq_prls,
17.36 + calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
17.37 + nrls = norm_Rational},
17.38 + "Script Solve_d0_polyeq_equation (e_e::bool) (v_v::real) = " ^
17.39 + "(let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
17.40 + " d0_polyeq_simplify False))) e_e " ^
17.41 + " in ((Or_to_List e_e)::bool list))"),
17.42 + prep_met thy "met_polyeq_d1" [] e_metID
17.43 + (["PolyEq","solve_d1_polyeq_equation"],
17.44 + [("#Given" ,["equality e_e","solveFor v_v"]),
17.45 + ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 1"]),
17.46 + ("#Find" ,["solutions v_v'i'"])],
17.47 + {rew_ord'="termlessI", rls'=PolyEq_erls, srls=e_rls, prls=PolyEq_prls,
17.48 + calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
17.49 + nrls = norm_Rational},
17.50 + "Script Solve_d1_polyeq_equation (e_e::bool) (v_v::real) = " ^
17.51 + "(let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
17.52 + " d1_polyeq_simplify True)) @@ " ^
17.53 + " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
17.54 + " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^
17.55 + " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
17.56 + " in Check_elementwise L_L {(v_v::real). Assumptions} )"),
17.57 + prep_met thy "met_polyeq_d22" [] e_metID
17.58 + (["PolyEq","solve_d2_polyeq_equation"],
17.59 + [("#Given" ,["equality e_e","solveFor v_v"]),
17.60 + ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 2"]),
17.61 + ("#Find" ,["solutions v_v'i'"])],
17.62 + {rew_ord'="termlessI", rls'=PolyEq_erls, srls=e_rls, prls=PolyEq_prls,
17.63 + calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
17.64 + nrls = norm_Rational},
17.65 + "Script Solve_d2_polyeq_equation (e_e::bool) (v_v::real) = " ^
17.66 + " (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
17.67 + " d2_polyeq_simplify True)) @@ " ^
17.68 + " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
17.69 + " (Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
17.70 + " d1_polyeq_simplify True)) @@ " ^
17.71 + " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
17.72 + " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^
17.73 + " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
17.74 + " in Check_elementwise L_L {(v_v::real). Assumptions} )"),
17.75 + prep_met thy "met_polyeq_d2_bdvonly" [] e_metID
17.76 + (["PolyEq","solve_d2_polyeq_bdvonly_equation"],
17.77 + [("#Given" ,["equality e_e","solveFor v_v"]),
17.78 + ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 2"]),
17.79 + ("#Find" ,["solutions v_v'i'"])],
17.80 + {rew_ord'="termlessI", rls'=PolyEq_erls, srls=e_rls, prls=PolyEq_prls,
17.81 + calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
17.82 + nrls = norm_Rational},
17.83 + "Script Solve_d2_polyeq_bdvonly_equation (e_e::bool) (v_v::real) =" ^
17.84 + " (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
17.85 + " d2_polyeq_bdv_only_simplify True)) @@ " ^
17.86 + " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
17.87 + " (Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
17.88 + " d1_polyeq_simplify True)) @@ " ^
17.89 + " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
17.90 + " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^
17.91 + " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
17.92 + " in Check_elementwise L_L {(v_v::real). Assumptions} )"),
17.93 + prep_met thy "met_polyeq_d2_sqonly" [] e_metID
17.94 + (["PolyEq","solve_d2_polyeq_sqonly_equation"],
17.95 + [("#Given" ,["equality e_e","solveFor v_v"]),
17.96 + ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 2"]),
17.97 + ("#Find" ,["solutions v_v'i'"])],
17.98 + {rew_ord'="termlessI", rls'=PolyEq_erls, srls=e_rls, prls=PolyEq_prls,
17.99 + calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
17.100 + nrls = norm_Rational},
17.101 + "Script Solve_d2_polyeq_sqonly_equation (e_e::bool) (v_v::real) =" ^
17.102 + " (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
17.103 + " d2_polyeq_sq_only_simplify True)) @@ " ^
17.104 + " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
17.105 + " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e; " ^
17.106 + " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
17.107 + " in Check_elementwise L_L {(v_v::real). Assumptions} )"),
17.108 + prep_met thy "met_polyeq_d2_pq" [] e_metID
17.109 + (["PolyEq","solve_d2_polyeq_pq_equation"],
17.110 + [("#Given" ,["equality e_e","solveFor v_v"]),
17.111 + ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 2"]),
17.112 + ("#Find" ,["solutions v_v'i'"])],
17.113 + {rew_ord'="termlessI", rls'=PolyEq_erls, srls=e_rls, prls=PolyEq_prls,
17.114 + calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
17.115 + nrls = norm_Rational},
17.116 + "Script Solve_d2_polyeq_pq_equation (e_e::bool) (v_v::real) = " ^
17.117 + " (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
17.118 + " d2_polyeq_pqFormula_simplify True)) @@ " ^
17.119 + " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
17.120 + " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^
17.121 + " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
17.122 + " in Check_elementwise L_L {(v_v::real). Assumptions} )"),
17.123 + prep_met thy "met_polyeq_d2_abc" [] e_metID
17.124 + (["PolyEq","solve_d2_polyeq_abc_equation"],
17.125 + [("#Given" ,["equality e_e","solveFor v_v"]),
17.126 + ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 2"]),
17.127 + ("#Find" ,["solutions v_v'i'"])],
17.128 + {rew_ord'="termlessI", rls'=PolyEq_erls,srls=e_rls, prls=PolyEq_prls,
17.129 + calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
17.130 + nrls = norm_Rational},
17.131 + "Script Solve_d2_polyeq_abc_equation (e_e::bool) (v_v::real) = " ^
17.132 + " (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
17.133 + " d2_polyeq_abcFormula_simplify True)) @@ " ^
17.134 + " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
17.135 + " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^
17.136 + " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
17.137 + " in Check_elementwise L_L {(v_v::real). Assumptions} )"),
17.138 + prep_met thy "met_polyeq_d3" [] e_metID
17.139 + (["PolyEq","solve_d3_polyeq_equation"],
17.140 + [("#Given" ,["equality e_e","solveFor v_v"]),
17.141 + ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 3"]),
17.142 + ("#Find" ,["solutions v_v'i'"])],
17.143 + {rew_ord'="termlessI", rls'=PolyEq_erls, srls=e_rls, prls=PolyEq_prls,
17.144 + calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
17.145 + nrls = norm_Rational},
17.146 + "Script Solve_d3_polyeq_equation (e_e::bool) (v_v::real) = " ^
17.147 + " (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
17.148 + " d3_polyeq_simplify True)) @@ " ^
17.149 + " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
17.150 + " (Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
17.151 + " d2_polyeq_simplify True)) @@ " ^
17.152 + " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
17.153 + " (Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
17.154 + " d1_polyeq_simplify True)) @@ " ^
17.155 + " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
17.156 + " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^
17.157 + " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
17.158 + " in Check_elementwise L_L {(v_v::real). Assumptions} )"),
17.159 + (*.solves all expanded (ie. normalized) terms of degree 2.*)
17.160 + (*Oct.02 restriction: 'eval_true 0 =< discriminant' ony for integer values
17.161 + by 'PolyEq_erls'; restricted until Float.thy is implemented*)
17.162 + prep_met thy "met_polyeq_complsq" [] e_metID
17.163 + (["PolyEq","complete_square"],
17.164 + [("#Given" ,["equality e_e","solveFor v_v"]),
17.165 + ("#Where" ,["matches (?a = 0) e_e", "((lhs e_e) has_degree_in v_v) = 2"]),
17.166 + ("#Find" ,["solutions v_v'i'"])],
17.167 + {rew_ord'="termlessI",rls'=PolyEq_erls,srls=e_rls,prls=PolyEq_prls,
17.168 + calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
17.169 + nrls = norm_Rational},
17.170 + "Script Complete_square (e_e::bool) (v_v::real) = " ^
17.171 + "(let e_e = " ^
17.172 + " ((Try (Rewrite_Set_Inst [(bdv,v_v)] cancel_leading_coeff True)) " ^
17.173 + " @@ (Try (Rewrite_Set_Inst [(bdv,v_v)] complete_square True)) " ^
17.174 + " @@ (Try (Rewrite square_explicit1 False)) " ^
17.175 + " @@ (Try (Rewrite square_explicit2 False)) " ^
17.176 + " @@ (Rewrite root_plus_minus True) " ^
17.177 + " @@ (Try (Repeat (Rewrite_Inst [(bdv,v_v)] bdv_explicit1 False))) " ^
17.178 + " @@ (Try (Repeat (Rewrite_Inst [(bdv,v_v)] bdv_explicit2 False))) " ^
17.179 + " @@ (Try (Repeat " ^
17.180 + " (Rewrite_Inst [(bdv,v_v)] bdv_explicit3 False))) " ^
17.181 + " @@ (Try (Rewrite_Set calculate_RootRat False)) " ^
17.182 + " @@ (Try (Repeat (Calculate SQRT)))) e_e " ^
17.183 + " in ((Or_to_List e_e)::bool list))")]
17.184 +*}
17.185 +
17.186 ML{*
17.187
17.188 (* termorder hacked by MG *)
18.1 --- a/src/Tools/isac/Knowledge/PolyMinus.thy Fri Jan 31 17:50:50 2014 +0100
18.2 +++ b/src/Tools/isac/Knowledge/PolyMinus.thy Sat Feb 01 16:44:45 2014 +0100
18.3 @@ -593,6 +593,93 @@
18.4 crls = e_rls, errpats = [], nrls = Erls},
18.5 "empty_script"));
18.6 *}
18.7 +setup {* KEStore_Elems.add_mets
18.8 + [prep_met thy "met_simp_poly_minus" [] e_metID
18.9 + (["simplification","for_polynomials","with_minus"],
18.10 + [("#Given" ,["Term t_t"]),
18.11 + ("#Where" ,["t_t is_polyexp",
18.12 + "Not (matchsub (?a + (?b + ?c)) t_t | " ^
18.13 + " matchsub (?a + (?b - ?c)) t_t | " ^
18.14 + " matchsub (?a - (?b + ?c)) t_t | " ^
18.15 + " matchsub (?a + (?b - ?c)) t_t )"]),
18.16 + ("#Find" ,["normalform n_n"])],
18.17 + {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls,
18.18 + prls = append_rls "prls_met_simp_poly_minus" e_rls
18.19 + [Calc ("Poly.is'_polyexp", eval_is_polyexp ""),
18.20 + Calc ("Tools.matchsub", eval_matchsub ""),
18.21 + Thm ("and_true",num_str @{thm and_true}),
18.22 + (*"(?a & True) = ?a"*)
18.23 + Thm ("and_false",num_str @{thm and_false}),
18.24 + (*"(?a & False) = False"*)
18.25 + Thm ("not_true",num_str @{thm not_true}),
18.26 + (*"(~ True) = False"*)
18.27 + Thm ("not_false",num_str @{thm not_false})
18.28 + (*"(~ False) = True"*)],
18.29 + crls = e_rls, errpats = [], nrls = rls_p_33},
18.30 + "Script SimplifyScript (t_t::real) = " ^
18.31 + " ((Repeat((Try (Rewrite_Set ordne_alphabetisch False)) @@ " ^
18.32 + " (Try (Rewrite_Set fasse_zusammen False)) @@ " ^
18.33 + " (Try (Rewrite_Set verschoenere False)))) t_t)"),
18.34 + prep_met thy "met_simp_poly_parenth" [] e_metID
18.35 + (["simplification","for_polynomials","with_parentheses"],
18.36 + [("#Given" ,["Term t_t"]),
18.37 + ("#Where" ,["t_t is_polyexp"]),
18.38 + ("#Find" ,["normalform n_n"])],
18.39 + {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls,
18.40 + prls = append_rls "simplification_for_polynomials_prls" e_rls
18.41 + [(*for preds in where_*) Calc("Poly.is'_polyexp",eval_is_polyexp"")],
18.42 + crls = e_rls, errpats = [], nrls = rls_p_34},
18.43 + "Script SimplifyScript (t_t::real) = " ^
18.44 + " ((Repeat((Try (Rewrite_Set klammern_aufloesen False)) @@ " ^
18.45 + " (Try (Rewrite_Set ordne_alphabetisch False)) @@ " ^
18.46 + " (Try (Rewrite_Set fasse_zusammen False)) @@ " ^
18.47 + " (Try (Rewrite_Set verschoenere False)))) t_t)"),
18.48 + prep_met thy "met_simp_poly_parenth_mult" [] e_metID
18.49 + (["simplification","for_polynomials","with_parentheses_mult"],
18.50 + [("#Given" ,["Term t_t"]), ("#Where" ,["t_t is_polyexp"]), ("#Find" ,["normalform n_n"])],
18.51 + {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls,
18.52 + prls = append_rls "simplification_for_polynomials_prls" e_rls
18.53 + [(*for preds in where_*) Calc("Poly.is'_polyexp",eval_is_polyexp"")],
18.54 + crls = e_rls, errpats = [], nrls = rls_p_34},
18.55 + "Script SimplifyScript (t_t::real) = " ^
18.56 + " ((Repeat((Try (Rewrite_Set klammern_ausmultiplizieren False)) @@ " ^
18.57 + " (Try (Rewrite_Set discard_parentheses False)) @@ " ^
18.58 + " (Try (Rewrite_Set ordne_monome False)) @@ " ^
18.59 + " (Try (Rewrite_Set klammern_aufloesen False)) @@ " ^
18.60 + " (Try (Rewrite_Set ordne_alphabetisch False)) @@ " ^
18.61 + " (Try (Rewrite_Set fasse_zusammen False)) @@ " ^
18.62 + " (Try (Rewrite_Set verschoenere False)))) t_t)"),
18.63 + prep_met thy "met_probe" [] e_metID
18.64 + (["probe"], [],
18.65 + {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls, prls = Erls, crls = e_rls,
18.66 + errpats = [], nrls = Erls},
18.67 + "empty_script"),
18.68 + prep_met thy "met_probe_poly" [] e_metID
18.69 + (["probe","fuer_polynom"],
18.70 + [("#Given" ,["Pruefe e_e", "mitWert w_w"]),
18.71 + ("#Where" ,["e_e is_polyexp"]),
18.72 + ("#Find" ,["Geprueft p_p"])],
18.73 + {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls,
18.74 + prls = append_rls "prls_met_probe_bruch" e_rls
18.75 + [(*for preds in where_*) Calc ("Rational.is'_ratpolyexp", eval_is_ratpolyexp "")],
18.76 + crls = e_rls, errpats = [], nrls = rechnen},
18.77 + "Script ProbeScript (e_e::bool) (w_w::bool list) = " ^
18.78 + " (let e_e = Take e_e; " ^
18.79 + " e_e = Substitute w_w e_e " ^
18.80 + " in (Repeat((Try (Repeat (Calculate TIMES))) @@ " ^
18.81 + " (Try (Repeat (Calculate PLUS ))) @@ " ^
18.82 + " (Try (Repeat (Calculate MINUS))))) e_e)"),
18.83 + prep_met thy "met_probe_bruch" [] e_metID
18.84 + (["probe","fuer_bruch"],
18.85 + [("#Given" ,["Pruefe e_e", "mitWert w_w"]),
18.86 + ("#Where" ,["e_e is_ratpolyexp"]),
18.87 + ("#Find" ,["Geprueft p_p"])],
18.88 + {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls,
18.89 + prls = append_rls "prls_met_probe_bruch" e_rls
18.90 + [(*for preds in where_*) Calc ("Rational.is'_ratpolyexp", eval_is_ratpolyexp "")],
18.91 + crls = e_rls, errpats = [], nrls = Erls},
18.92 + "empty_script")]
18.93 +*}
18.94
18.95 end
18.96
19.1 --- a/src/Tools/isac/Knowledge/RatEq.thy Fri Jan 31 17:50:50 2014 +0100
19.2 +++ b/src/Tools/isac/Knowledge/RatEq.thy Sat Feb 01 16:44:45 2014 +0100
19.3 @@ -225,6 +225,28 @@
19.4 " in Check_elementwise L_L {(v_v::real). Assumptions})"
19.5 ));
19.6 *}
19.7 +(*-------------------------methods-----------------------*)
19.8 +setup {* KEStore_Elems.add_mets
19.9 + [prep_met thy "met_rateq" [] e_metID
19.10 + (["RatEq"], [],
19.11 + {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
19.12 + crls=RatEq_crls, errpats = [], nrls = norm_Rational}, "empty_script"),
19.13 + prep_met thy "met_rat_eq" [] e_metID
19.14 + (["RatEq", "solve_rat_equation"],
19.15 + [("#Given" ,["equality e_e","solveFor v_v"]),
19.16 + ("#Where" ,["(e_e::bool) is_ratequation_in (v_v::real)"]),
19.17 + ("#Find" ,["solutions v_v'i'"])],
19.18 + {rew_ord'="termlessI", rls'=rateq_erls, srls=e_rls, prls=RatEq_prls, calc=[],
19.19 + crls=RatEq_crls, errpats = [], nrls = norm_Rational},
19.20 + "Script Solve_rat_equation (e_e::bool) (v_v::real) = " ^
19.21 + "(let e_e = ((Repeat(Try (Rewrite_Set RatEq_simplify True))) @@ " ^
19.22 + " (Repeat(Try (Rewrite_Set norm_Rational False))) @@ " ^
19.23 + " (Repeat(Try (Rewrite_Set add_fractions_p False))) @@ " ^
19.24 + " (Repeat(Try (Rewrite_Set RatEq_eliminate True)))) e_e;" ^
19.25 + " (L_L::bool list) = (SubProblem (RatEq',[univariate,equation], [no_met])" ^
19.26 + " [BOOL e_e, REAL v_v]) " ^
19.27 + " in Check_elementwise L_L {(v_v::real). Assumptions})")]
19.28 +*}
19.29
19.30 setup {* KEStore_Elems.add_calcs
19.31 [("is_ratequation_in", ("RatEq.is_ratequation_in", eval_is_ratequation_in ""))] *}
20.1 --- a/src/Tools/isac/Knowledge/Rational.thy Fri Jan 31 17:50:50 2014 +0100
20.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Sat Feb 01 16:44:45 2014 +0100
20.3 @@ -920,5 +920,31 @@
20.4 " Try (Rewrite_Set discard_parentheses1 False)) " ^
20.5 " t_t)"));
20.6 *}
20.7 +(*WN061025 this methods script is copied from (auto-generated) script
20.8 + of norm_Rational in order to ease repair on inform*)
20.9 +setup {* KEStore_Elems.add_mets
20.10 + [prep_met thy "met_simp_rat" [] e_metID
20.11 + (["simplification","of_rationals"],
20.12 + [("#Given" ,["Term t_t"]),
20.13 + ("#Where" ,["t_t is_ratpolyexp"]),
20.14 + ("#Find" ,["normalform n_n"])],
20.15 + {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls,
20.16 + prls = append_rls "simplification_of_rationals_prls" e_rls
20.17 + [(*for preds in where_*) Calc ("Rational.is'_ratpolyexp", eval_is_ratpolyexp "")],
20.18 + crls = e_rls, errpats = [], 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
20.34 end
21.1 --- a/src/Tools/isac/Knowledge/RootEq.thy Fri Jan 31 17:50:50 2014 +0100
21.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy Sat Feb 01 16:44:45 2014 +0100
21.3 @@ -637,6 +637,97 @@
21.4 ));
21.5 val --------------------------------------------------++++ = "44444";
21.6 *}
21.7 +(*-------------------------methods-----------------------*)
21.8 +setup {* KEStore_Elems.add_mets
21.9 + [(* ---- root 20.8.02 ---*)
21.10 + prep_met thy "met_rooteq" [] e_metID
21.11 + (["RootEq"], [],
21.12 + {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
21.13 + crls=RootEq_crls, errpats = [], nrls = norm_Poly}, "empty_script"),
21.14 + (*-- normalize 20.10.02 --*)
21.15 + prep_met thy "met_rooteq_norm" [] e_metID
21.16 + (["RootEq","norm_sq_root_equation"],
21.17 + [("#Given" ,["equality e_e","solveFor v_v"]),
21.18 + ("#Where" ,["( ((lhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
21.19 + " Not((lhs e_e) is_normSqrtTerm_in (v_v::real))) | " ^
21.20 + "( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
21.21 + " Not((rhs e_e) is_normSqrtTerm_in (v_v::real)))"]),
21.22 + ("#Find" ,["solutions v_v'i'"])],
21.23 + {rew_ord'="termlessI", rls'=RootEq_erls, srls=e_rls, prls=RootEq_prls, calc=[],
21.24 + crls=RootEq_crls, errpats = [], nrls = norm_Poly},
21.25 + "Script Norm_sq_root_equation (e_e::bool) (v_v::real) = " ^
21.26 + "(let e_e = ((Repeat(Try (Rewrite makex1_x False))) @@ " ^
21.27 + " (Try (Repeat (Rewrite_Set expand_rootbinoms False))) @@ " ^
21.28 + " (Try (Rewrite_Set rooteq_simplify True)) @@ " ^
21.29 + " (Try (Repeat (Rewrite_Set make_rooteq False))) @@ " ^
21.30 + " (Try (Rewrite_Set rooteq_simplify True))) e_e " ^
21.31 + " in ((SubProblem (RootEq',[univariate,equation], " ^
21.32 + " [no_met]) [BOOL e_e, REAL v_v])))"),
21.33 + prep_met thy "met_rooteq_sq" [] e_metID
21.34 + (["RootEq","solve_sq_root_equation"],
21.35 + [("#Given" ,["equality e_e", "solveFor v_v"]),
21.36 + ("#Where" ,["(((lhs e_e) is_sqrtTerm_in (v_v::real)) & " ^
21.37 + " ((lhs e_e) is_normSqrtTerm_in (v_v::real))) |" ^
21.38 + "(((rhs e_e) is_sqrtTerm_in (v_v::real)) & " ^
21.39 + " ((rhs e_e) is_normSqrtTerm_in (v_v::real)))"]),
21.40 + ("#Find" ,["solutions v_v'i'"])],
21.41 + {rew_ord'="termlessI", rls'=RootEq_erls, srls = rooteq_srls, prls = RootEq_prls, calc = [],
21.42 + crls=RootEq_crls, errpats = [], nrls = norm_Poly},
21.43 + "Script Solve_sq_root_equation (e_e::bool) (v_v::real) = " ^
21.44 + "(let e_e = " ^
21.45 + " ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] sqrt_isolate True)) @@ " ^
21.46 + " (Try (Rewrite_Set rooteq_simplify True)) @@ " ^
21.47 + " (Try (Repeat (Rewrite_Set expand_rootbinoms False))) @@ " ^
21.48 + " (Try (Repeat (Rewrite_Set make_rooteq False))) @@ " ^
21.49 + " (Try (Rewrite_Set rooteq_simplify True)) ) e_e; " ^
21.50 + " (L_L::bool list) = " ^
21.51 + " (if (((lhs e_e) is_sqrtTerm_in v_v) | ((rhs e_e) is_sqrtTerm_in v_v))" ^
21.52 + " then (SubProblem (RootEq',[normalize,root',univariate,equation], " ^
21.53 + " [no_met]) [BOOL e_e, REAL v_v]) " ^
21.54 + " else (SubProblem (RootEq',[univariate,equation], [no_met]) " ^
21.55 + " [BOOL e_e, REAL v_v])) " ^
21.56 + "in Check_elementwise L_L {(v_v::real). Assumptions})"),
21.57 + (*-- right 28.08.02 --*)
21.58 + prep_met thy "met_rooteq_sq_right" [] e_metID
21.59 + (["RootEq","solve_right_sq_root_equation"],
21.60 + [("#Given" ,["equality e_e","solveFor v_v"]),
21.61 + ("#Where" ,["(rhs e_e) is_sqrtTerm_in v_v"]),
21.62 + ("#Find" ,["solutions v_v'i'"])],
21.63 + {rew_ord' = "termlessI", rls' = RootEq_erls, srls = e_rls, prls = RootEq_prls, calc = [],
21.64 + crls = RootEq_crls, errpats = [], nrls = norm_Poly},
21.65 + "Script Solve_right_sq_root_equation (e_e::bool) (v_v::real) = " ^
21.66 + "(let e_e = " ^
21.67 + " ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] r_sqrt_isolate False)) @@ " ^
21.68 + " (Try (Rewrite_Set rooteq_simplify False)) @@ " ^
21.69 + " (Try (Repeat (Rewrite_Set expand_rootbinoms False))) @@ " ^
21.70 + " (Try (Repeat (Rewrite_Set make_rooteq False))) @@ " ^
21.71 + " (Try (Rewrite_Set rooteq_simplify False))) e_e " ^
21.72 + " in if ((rhs e_e) is_sqrtTerm_in v_v) " ^
21.73 + " then (SubProblem (RootEq',[normalize,root',univariate,equation], " ^
21.74 + " [no_met]) [BOOL e_e, REAL v_v]) " ^
21.75 + " else ((SubProblem (RootEq',[univariate,equation], " ^
21.76 + " [no_met]) [BOOL e_e, REAL v_v])))"),
21.77 + (*-- left 28.08.02 --*)
21.78 + prep_met thy "met_rooteq_sq_left" [] e_metID
21.79 + (["RootEq","solve_left_sq_root_equation"],
21.80 + [("#Given" ,["equality e_e","solveFor v_v"]),
21.81 + ("#Where" ,["(lhs e_e) is_sqrtTerm_in v_v"]),
21.82 + ("#Find" ,["solutions v_v'i'"])],
21.83 + {rew_ord'="termlessI", rls'=RootEq_erls, srls=e_rls, prls=RootEq_prls, calc=[],
21.84 + crls=RootEq_crls, errpats = [], nrls = norm_Poly},
21.85 + "Script Solve_left_sq_root_equation (e_e::bool) (v_v::real) = " ^
21.86 + "(let e_e = " ^
21.87 + " ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] l_sqrt_isolate False)) @@ " ^
21.88 + " (Try (Rewrite_Set rooteq_simplify False)) @@ " ^
21.89 + " (Try (Repeat (Rewrite_Set expand_rootbinoms False))) @@ " ^
21.90 + " (Try (Repeat (Rewrite_Set make_rooteq False))) @@ " ^
21.91 + " (Try (Rewrite_Set rooteq_simplify False))) e_e " ^
21.92 + " in if ((lhs e_e) is_sqrtTerm_in v_v) " ^
21.93 + " then (SubProblem (RootEq',[normalize,root',univariate,equation], " ^
21.94 + " [no_met]) [BOOL e_e, REAL v_v]) " ^
21.95 + " else ((SubProblem (RootEq',[univariate,equation], " ^
21.96 + " [no_met]) [BOOL e_e, REAL v_v])))")] *}
21.97 +
21.98 setup {* KEStore_Elems.add_calcs
21.99 [("is_rootTerm_in", ("RootEq.is'_rootTerm'_in", eval_is_rootTerm_in"")),
21.100 ("is_sqrtTerm_in", ("RootEq.is'_sqrtTerm'_in", eval_is_sqrtTerm_in"")),
22.1 --- a/src/Tools/isac/Knowledge/RootRatEq.thy Fri Jan 31 17:50:50 2014 +0100
22.2 +++ b/src/Tools/isac/Knowledge/RootRatEq.thy Sat Feb 01 16:44:45 2014 +0100
22.3 @@ -181,6 +181,32 @@
22.4 " [no_met]) [BOOL e_e, REAL v_v]))"
22.5 ));
22.6 *}
22.7 +(*-------------------------Methode-----------------------*)
22.8 +setup {* KEStore_Elems.add_mets
22.9 + [prep_met @{theory LinEq} "met_rootrateq" [] e_metID
22.10 + (["RootRatEq"], [],
22.11 + {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
22.12 + crls=Atools_erls, errpats = [], nrls = norm_Rational}, "empty_script"),
22.13 + (*-- left 20.10.02 --*)
22.14 + prep_met thy "met_rootrateq_elim" [] e_metID
22.15 + (["RootRatEq","elim_rootrat_equation"],
22.16 + [("#Given" ,["equality e_e","solveFor v_v"]),
22.17 + ("#Where" ,["( (lhs e_e) is_rootRatAddTerm_in (v_v::real) ) | " ^
22.18 + "( (rhs e_e) is_rootRatAddTerm_in (v_v::real) )"]),
22.19 + ("#Find" ,["solutions v_v'i'"])],
22.20 + {rew_ord'="termlessI", rls'=RooRatEq_erls, srls=e_rls, prls=RootRatEq_prls, calc=[],
22.21 + crls=RootRatEq_crls, errpats = [], nrls = norm_Rational},
22.22 + "Script Elim_rootrat_equation (e_e::bool) (v_v::real) = " ^
22.23 + "(let e_e = ((Try (Rewrite_Set expand_rootbinoms False)) @@ " ^
22.24 + " (Try (Rewrite_Set rooteq_simplify False)) @@ " ^
22.25 + " (Try (Rewrite_Set make_rooteq False)) @@ " ^
22.26 + " (Try (Rewrite_Set rooteq_simplify False)) @@ " ^
22.27 + " (Try (Rewrite_Set_Inst [(bdv,v_v)] " ^
22.28 + " rootrat_solve False))) e_e " ^
22.29 + " in (SubProblem (RootEq',[univariate,equation], " ^
22.30 + " [no_met]) [BOOL e_e, REAL v_v]))")]
22.31 +*}
22.32 +
22.33 setup {* KEStore_Elems.add_calcs
22.34 [("is_rootRatAddTerm_in", ("RootRatEq.is_rootRatAddTerm_in", eval_is_rootRatAddTerm_in""))] *}
22.35
23.1 --- a/src/Tools/isac/Knowledge/Simplify.thy Fri Jan 31 17:50:50 2014 +0100
23.2 +++ b/src/Tools/isac/Knowledge/Simplify.thy Sat Feb 01 16:44:45 2014 +0100
23.3 @@ -55,6 +55,17 @@
23.4 crls = e_rls, errpats = [], nrls = e_rls},
23.5 "empty_script"));
23.6 *}
23.7 +(** methods **)
23.8 +setup {* KEStore_Elems.add_mets
23.9 + [prep_met thy "met_tsimp" [] e_metID
23.10 + (["simplification"],
23.11 + [("#Given" ,["Term t_t"]),
23.12 + ("#Find" ,["normalform n_n"])],
23.13 + {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls=e_rls, crls = e_rls,
23.14 + errpats = [], nrls = e_rls},
23.15 + "empty_script")]
23.16 +*}
23.17 +
23.18 ML {*
23.19
23.20 (** CAS-command **)
24.1 --- a/src/Tools/isac/Knowledge/Test.thy Fri Jan 31 17:50:50 2014 +0100
24.2 +++ b/src/Tools/isac/Knowledge/Test.thy Sat Feb 01 16:44:45 2014 +0100
24.3 @@ -590,6 +590,38 @@
24.4 , ---------27.4.02*)
24.5 );
24.6 *}
24.7 +(** methods **)
24.8 +setup {* KEStore_Elems.add_mets
24.9 + [prep_met @{theory "Diff"} "met_test" [] e_metID
24.10 + (["Test"], [],
24.11 + {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
24.12 + crls=Atools_erls, errpats = [], nrls = e_rls}, "empty_script"),
24.13 + prep_met thy "met_test_solvelin" [] e_metID
24.14 + (["Test","solve_linear"]:metID,
24.15 + [("#Given" ,["equality e_e","solveFor v_v"]),
24.16 + ("#Where" ,["matches (?a = ?b) e_e"]),
24.17 + ("#Find" ,["solutions v_v'i'"])],
24.18 + {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = e_rls,
24.19 + prls = assoc_rls' @{theory} "matches", calc = [], crls = tval_rls, errpats = [],
24.20 + nrls = Test_simplify},
24.21 + "Script Solve_linear (e_e::bool) (v_v::real)= " ^
24.22 + "(let e_e = " ^
24.23 + " Repeat " ^
24.24 + " (((Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@ " ^
24.25 + " (Rewrite_Set Test_simplify False))) e_e" ^
24.26 + " in [e_e::bool])")(*,
24.27 + prep_met thy (*test for equations*)
24.28 + (["Test","testeq"]:metID,
24.29 + [("#Given" ,["boolTestGiven g_g"]),
24.30 + ("#Find" ,["boolTestFind f_f"])],
24.31 + {rew_ord'="e_rew_ord",rls'="tval_rls",asm_rls=[], asm_thm=[("square_equation_left","")]},
24.32 + "Script Testeq (e_q::bool) = " ^
24.33 + "Repeat " ^
24.34 + " (let e_e = Try (Repeat (Rewrite rroot_square_inv False e_q)); " ^
24.35 + " e_e = Try (Repeat (Rewrite square_equation_left True e_e)); " ^
24.36 + " e_e = Try (Repeat (Rewrite rmult_0 False e_e)) " ^
24.37 + " in e_e) Until (is_root_free e_e)" (*deleted*)) ---------27.4.02*)]
24.38 +*}
24.39
24.40 setup {* KEStore_Elems.add_rlss
24.41 [("norm_equation", (Context.theory_name @{theory}, prep_rls norm_equation)),
24.42 @@ -1130,6 +1162,235 @@
24.43 ));
24.44
24.45 *}
24.46 +setup {* KEStore_Elems.add_mets
24.47 + [prep_met thy "met_test_sqrt" [] e_metID
24.48 + (*root-equation, version for tests before 8.01.01*)
24.49 + (["Test","sqrt-equ-test"]:metID,
24.50 + [("#Given" ,["equality e_e","solveFor v_v"]),
24.51 + ("#Where" ,["contains_root (e_e::bool)"]),
24.52 + ("#Find" ,["solutions v_v'i'"])],
24.53 + {rew_ord'="e_rew_ord",rls'=tval_rls,
24.54 + srls = append_rls "srls_contains_root" e_rls
24.55 + [Calc ("Test.contains'_root",eval_contains_root "")],
24.56 + prls = append_rls "prls_contains_root" e_rls
24.57 + [Calc ("Test.contains'_root",eval_contains_root "")],
24.58 + calc=[], crls=tval_rls, errpats = [], nrls = e_rls (*,asm_rls=[],
24.59 + asm_thm=[("square_equation_left",""), ("square_equation_right","")]*)},
24.60 + "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
24.61 + "(let e_e = " ^
24.62 + " ((While (contains_root e_e) Do" ^
24.63 + " ((Rewrite square_equation_left True) @@" ^
24.64 + " (Try (Rewrite_Set Test_simplify False)) @@" ^
24.65 + " (Try (Rewrite_Set rearrange_assoc False)) @@" ^
24.66 + " (Try (Rewrite_Set isolate_root False)) @@" ^
24.67 + " (Try (Rewrite_Set Test_simplify False)))) @@" ^
24.68 + " (Try (Rewrite_Set norm_equation False)) @@" ^
24.69 + " (Try (Rewrite_Set Test_simplify False)) @@" ^
24.70 + " (Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@" ^
24.71 + " (Try (Rewrite_Set Test_simplify False)))" ^
24.72 + " e_e" ^
24.73 + " in [e_e::bool])"),
24.74 + prep_met thy "met_test_sqrt2" [] e_metID
24.75 + (*root-equation ... for test-*.sml until 8.01*)
24.76 + (["Test","squ-equ-test2"]:metID,
24.77 + [("#Given" ,["equality e_e","solveFor v_v"]),
24.78 + ("#Find" ,["solutions v_v'i'"])],
24.79 + {rew_ord'="e_rew_ord",rls'=tval_rls,
24.80 + srls = append_rls "srls_contains_root" e_rls
24.81 + [Calc ("Test.contains'_root",eval_contains_root"")],
24.82 + prls=e_rls,calc=[], crls=tval_rls, errpats = [], nrls = e_rls(*,asm_rls=[],
24.83 + asm_thm=[("square_equation_left",""), ("square_equation_right","")]*)},
24.84 + "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
24.85 + "(let e_e = " ^
24.86 + " ((While (contains_root e_e) Do" ^
24.87 + " ((Rewrite square_equation_left True) @@" ^
24.88 + " (Try (Rewrite_Set Test_simplify False)) @@" ^
24.89 + " (Try (Rewrite_Set rearrange_assoc False)) @@" ^
24.90 + " (Try (Rewrite_Set isolate_root False)) @@" ^
24.91 + " (Try (Rewrite_Set Test_simplify False)))) @@" ^
24.92 + " (Try (Rewrite_Set norm_equation False)) @@" ^
24.93 + " (Try (Rewrite_Set Test_simplify False)) @@" ^
24.94 + " (Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@" ^
24.95 + " (Try (Rewrite_Set Test_simplify False)))" ^
24.96 + " e_e;" ^
24.97 + " (L_L::bool list) = Tac subproblem_equation_dummy; " ^
24.98 + " L_L = Tac solve_equation_dummy " ^
24.99 + " in Check_elementwise L_L {(v_v::real). Assumptions})"),
24.100 + prep_met thy "met_test_squ_sub" [] e_metID
24.101 + (*tests subproblem fixed linear*)
24.102 + (["Test","squ-equ-test-subpbl1"]:metID,
24.103 + [("#Given" ,["equality e_e","solveFor v_v"]),
24.104 + ("#Where" ,["precond_rootmet v_v"]),
24.105 + ("#Find" ,["solutions v_v'i'"])],
24.106 + {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = e_rls,
24.107 + prls = append_rls "prls_met_test_squ_sub" e_rls
24.108 + [Calc ("Test.precond'_rootmet", eval_precond_rootmet "")],
24.109 + calc=[], crls=tval_rls, errpats = [], nrls = Test_simplify},
24.110 + "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
24.111 + " (let e_e = ((Try (Rewrite_Set norm_equation False)) @@ " ^
24.112 + " (Try (Rewrite_Set Test_simplify False))) e_e; " ^
24.113 + " (L_L::bool list) = " ^
24.114 + " (SubProblem (Test', " ^
24.115 + " [LINEAR,univariate,equation,test]," ^
24.116 + " [Test,solve_linear]) " ^
24.117 + " [BOOL e_e, REAL v_v]) " ^
24.118 + " in Check_elementwise L_L {(v_v::real). Assumptions}) "),
24.119 + prep_met thy "met_test_squ_sub2" [] e_metID
24.120 + (*tests subproblem fixed degree 2*)
24.121 + (["Test","squ-equ-test-subpbl2"]:metID,
24.122 + [("#Given" ,["equality e_e","solveFor v_v"]),
24.123 + ("#Find" ,["solutions v_v'i'"])],
24.124 + {rew_ord'="e_rew_ord",rls'=tval_rls,srls=e_rls,prls=e_rls,calc=[], crls=tval_rls,
24.125 + errpats = [], nrls = e_rls (*, asm_rls=[],asm_thm=[("square_equation_left",""),
24.126 + ("square_equation_right","")]*)},
24.127 + "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
24.128 + " (let e_e = Try (Rewrite_Set norm_equation False) e_e; " ^
24.129 + "(L_L::bool list) = (SubProblem (Test',[LINEAR,univariate,equation,test]," ^
24.130 + " [Test,solve_by_pq_formula]) [BOOL e_e, REAL v_v])" ^
24.131 + "in Check_elementwise L_L {(v_v::real). Assumptions})"),
24.132 + prep_met thy "met_test_squ_nonterm" [] e_metID
24.133 + (*root-equation: see foils..., but notTerminating*)
24.134 + (["Test","square_equation...notTerminating"]:metID,
24.135 + [("#Given" ,["equality e_e","solveFor v_v"]),
24.136 + ("#Find" ,["solutions v_v'i'"])],
24.137 + {rew_ord'="e_rew_ord",rls'=tval_rls,
24.138 + srls = append_rls "srls_contains_root" e_rls
24.139 + [Calc ("Test.contains'_root",eval_contains_root"")],
24.140 + prls=e_rls,calc=[], crls=tval_rls, errpats = [], nrls = e_rls(*,asm_rls=[],
24.141 + asm_thm=[("square_equation_left",""), ("square_equation_right","")]*)},
24.142 + "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
24.143 + "(let e_e = " ^
24.144 + " ((While (contains_root e_e) Do" ^
24.145 + " ((Rewrite square_equation_left True) @@" ^
24.146 + " (Try (Rewrite_Set Test_simplify False)) @@" ^
24.147 + " (Try (Rewrite_Set rearrange_assoc False)) @@" ^
24.148 + " (Try (Rewrite_Set isolate_root False)) @@" ^
24.149 + " (Try (Rewrite_Set Test_simplify False)))) @@" ^
24.150 + " (Try (Rewrite_Set norm_equation False)) @@" ^
24.151 + " (Try (Rewrite_Set Test_simplify False)))" ^
24.152 + " e_e;" ^
24.153 + " (L_L::bool list) = " ^
24.154 + " (SubProblem (Test',[LINEAR,univariate,equation,test]," ^
24.155 + " [Test,solve_linear]) [BOOL e_e, REAL v_v])" ^
24.156 + "in Check_elementwise L_L {(v_v::real). Assumptions})"),
24.157 + prep_met thy "met_test_eq1" [] e_metID
24.158 + (*root-equation1:*)
24.159 + (["Test","square_equation1"]:metID,
24.160 + [("#Given" ,["equality e_e","solveFor v_v"]),
24.161 + ("#Find" ,["solutions v_v'i'"])],
24.162 + {rew_ord'="e_rew_ord",rls'=tval_rls,
24.163 + srls = append_rls "srls_contains_root" e_rls
24.164 + [Calc ("Test.contains'_root",eval_contains_root"")], prls=e_rls, calc=[], crls=tval_rls,
24.165 + errpats = [], nrls = e_rls(*,asm_rls=[], asm_thm=[("square_equation_left",""),
24.166 + ("square_equation_right","")]*)},
24.167 + "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
24.168 + "(let e_e = " ^
24.169 + " ((While (contains_root e_e) Do" ^
24.170 + " ((Rewrite square_equation_left True) @@" ^
24.171 + " (Try (Rewrite_Set Test_simplify False)) @@" ^
24.172 + " (Try (Rewrite_Set rearrange_assoc False)) @@" ^
24.173 + " (Try (Rewrite_Set isolate_root False)) @@" ^
24.174 + " (Try (Rewrite_Set Test_simplify False)))) @@" ^
24.175 + " (Try (Rewrite_Set norm_equation False)) @@" ^
24.176 + " (Try (Rewrite_Set Test_simplify False)))" ^
24.177 + " e_e;" ^
24.178 + " (L_L::bool list) = (SubProblem (Test',[LINEAR,univariate,equation,test]," ^
24.179 + " [Test,solve_linear]) [BOOL e_e, REAL v_v])" ^
24.180 + " in Check_elementwise L_L {(v_v::real). Assumptions})"),
24.181 + prep_met thy "met_test_squ2" [] e_metID
24.182 + (*root-equation2*)
24.183 + (["Test","square_equation2"]:metID,
24.184 + [("#Given" ,["equality e_e","solveFor v_v"]),
24.185 + ("#Find" ,["solutions v_v'i'"])],
24.186 + {rew_ord'="e_rew_ord",rls'=tval_rls,
24.187 + srls = append_rls "srls_contains_root" e_rls
24.188 + [Calc ("Test.contains'_root",eval_contains_root"")],
24.189 + prls=e_rls,calc=[], crls=tval_rls, errpats = [], nrls = e_rls(*,asm_rls=[],
24.190 + asm_thm=[("square_equation_left",""), ("square_equation_right","")]*)},
24.191 + "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
24.192 + "(let e_e = " ^
24.193 + " ((While (contains_root e_e) Do" ^
24.194 + " (((Rewrite square_equation_left True) Or " ^
24.195 + " (Rewrite square_equation_right True)) @@" ^
24.196 + " (Try (Rewrite_Set Test_simplify False)) @@" ^
24.197 + " (Try (Rewrite_Set rearrange_assoc False)) @@" ^
24.198 + " (Try (Rewrite_Set isolate_root False)) @@" ^
24.199 + " (Try (Rewrite_Set Test_simplify False)))) @@" ^
24.200 + " (Try (Rewrite_Set norm_equation False)) @@" ^
24.201 + " (Try (Rewrite_Set Test_simplify False)))" ^
24.202 + " e_e;" ^
24.203 + " (L_L::bool list) = (SubProblem (Test',[plain_square,univariate,equation,test]," ^
24.204 + " [Test,solve_plain_square]) [BOOL e_e, REAL v_v])" ^
24.205 + " in Check_elementwise L_L {(v_v::real). Assumptions})"),
24.206 + prep_met thy "met_test_squeq" [] e_metID
24.207 + (*root-equation*)
24.208 + (["Test","square_equation"]:metID,
24.209 + [("#Given" ,["equality e_e","solveFor v_v"]),
24.210 + ("#Find" ,["solutions v_v'i'"])],
24.211 + {rew_ord'="e_rew_ord",rls'=tval_rls,
24.212 + srls = append_rls "srls_contains_root" e_rls
24.213 + [Calc ("Test.contains'_root",eval_contains_root"")],
24.214 + prls=e_rls,calc=[], crls=tval_rls, errpats = [], nrls = e_rls (*,asm_rls=[],
24.215 + asm_thm=[("square_equation_left",""), ("square_equation_right","")]*)},
24.216 + "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
24.217 + "(let e_e = " ^
24.218 + " ((While (contains_root e_e) Do" ^
24.219 + " (((Rewrite square_equation_left True) Or" ^
24.220 + " (Rewrite square_equation_right True)) @@" ^
24.221 + " (Try (Rewrite_Set Test_simplify False)) @@" ^
24.222 + " (Try (Rewrite_Set rearrange_assoc False)) @@" ^
24.223 + " (Try (Rewrite_Set isolate_root False)) @@" ^
24.224 + " (Try (Rewrite_Set Test_simplify False)))) @@" ^
24.225 + " (Try (Rewrite_Set norm_equation False)) @@" ^
24.226 + " (Try (Rewrite_Set Test_simplify False)))" ^
24.227 + " e_e;" ^
24.228 + " (L_L::bool list) = (SubProblem (Test',[univariate,equation,test]," ^
24.229 + " [no_met]) [BOOL e_e, REAL v_v])" ^
24.230 + " in Check_elementwise L_L {(v_v::real). Assumptions})"),
24.231 + prep_met thy "met_test_eq_plain" [] e_metID
24.232 + (*solve_plain_square*)
24.233 + (["Test","solve_plain_square"]:metID,
24.234 + [("#Given",["equality e_e","solveFor v_v"]),
24.235 + ("#Where" ,["(matches (?a + ?b*v_v ^^^2 = 0) e_e) |" ^
24.236 + "(matches ( ?b*v_v ^^^2 = 0) e_e) |" ^
24.237 + "(matches (?a + v_v ^^^2 = 0) e_e) |" ^
24.238 + "(matches ( v_v ^^^2 = 0) e_e)"]),
24.239 + ("#Find" ,["solutions v_v'i'"])],
24.240 + {rew_ord'="e_rew_ord",rls'=tval_rls,calc=[],srls=e_rls,
24.241 + prls = assoc_rls' @{theory} "matches", crls=tval_rls, errpats = [], nrls = e_rls(*,
24.242 + asm_rls=[],asm_thm=[]*)},
24.243 + "Script Solve_plain_square (e_e::bool) (v_v::real) = " ^
24.244 + " (let e_e = ((Try (Rewrite_Set isolate_bdv False)) @@ " ^
24.245 + " (Try (Rewrite_Set Test_simplify False)) @@ " ^
24.246 + " ((Rewrite square_equality_0 False) Or " ^
24.247 + " (Rewrite square_equality True)) @@ " ^
24.248 + " (Try (Rewrite_Set tval_rls False))) e_e " ^
24.249 + " in ((Or_to_List e_e)::bool list))"),
24.250 + prep_met thy "met_test_norm_univ" [] e_metID
24.251 + (["Test","norm_univar_equation"]:metID,
24.252 + [("#Given",["equality e_e","solveFor v_v"]),
24.253 + ("#Where" ,[]),
24.254 + ("#Find" ,["solutions v_v'i'"])],
24.255 + {rew_ord'="e_rew_ord",rls'=tval_rls,srls = e_rls,prls=e_rls, calc=[], crls=tval_rls,
24.256 + errpats = [], nrls = e_rls},
24.257 + "Script Norm_univar_equation (e_e::bool) (v_v::real) = " ^
24.258 + " (let e_e = ((Try (Rewrite rnorm_equation_add False)) @@ " ^
24.259 + " (Try (Rewrite_Set Test_simplify False))) e_e " ^
24.260 + " in (SubProblem (Test',[univariate,equation,test], " ^
24.261 + " [no_met]) [BOOL e_e, REAL v_v]))"),
24.262 + (*17.9.02 aus SqRoot.ML------------------------------^^^---*)
24.263 + prep_met thy "met_test_intsimp" [] e_metID
24.264 + (["Test","intsimp"]:metID,
24.265 + [("#Given" ,["intTestGiven t_t"]),
24.266 + ("#Where" ,[]),
24.267 + ("#Find" ,["intTestFind s_s"])],
24.268 + {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = e_rls, prls = e_rls, calc = [],
24.269 + crls = tval_rls, errpats = [], nrls = Test_simplify},
24.270 + "Script STest_simplify (t_t::int) = " ^
24.271 + "(Repeat " ^
24.272 + " ((Try (Calculate PLUS)) @@ " ^
24.273 + " (Try (Calculate TIMES))) t_t::int)")]
24.274 +*}
24.275
24.276 ML {*
24.277 (*8.4.03 aus Poly.ML--------------------------------vvv---
25.1 --- a/src/Tools/isac/calcelems.sml Fri Jan 31 17:50:50 2014 +0100
25.2 +++ b/src/Tools/isac/calcelems.sml Sat Feb 01 16:44:45 2014 +0100
25.3 @@ -894,6 +894,22 @@
25.4 type mets = (met ptyp) list;
25.5 val mets = Unsynchronized.ref ([e_Mets]:mets);
25.6
25.7 +fun coll_metguhs mets =
25.8 + let fun node coll (Ptyp (_,[n],ns)) =
25.9 + [(#guh : met -> guh) n]
25.10 + and nodes coll [] = coll
25.11 + | nodes coll (n::ns) = (node coll n) @ (nodes coll ns);
25.12 + in nodes [] mets end;
25.13 +
25.14 +(* val (guh, mets) = ("met_test", !mets);
25.15 + *)
25.16 +fun check_metguh_unique (guh:guh) (mets: (met ptyp) list) =
25.17 + if member op = (coll_metguhs mets) guh
25.18 + then error ("check_guh_unique failed with '"^guh^"';\n"^
25.19 + "use 'sort_metguhs()' for a list of guhs;\n"^
25.20 + "consider setting 'check_guhs_unique := false'")
25.21 + else ();
25.22 +
25.23
25.24 (*
25.25 end (*struct*)