ad 967c8a1eb6b1 (7): removed all code concerned with 'ptyps = Unsynchronized.ref'
1.1 --- a/src/Tools/isac/Interpret/ptyps.sml Mon Jan 27 21:58:57 2014 +0100
1.2 +++ b/src/Tools/isac/Interpret/ptyps.sml Mon Jan 27 22:26:51 2014 +0100
1.3 @@ -449,7 +449,7 @@
1.4
1.5
1.6
1.7 -(*.the metID has the root-element as first; compare 'fun store_pbt'.*)
1.8 +(*.the metID has the root-element as first.*)
1.9 fun store_met (met as {guh,...}, metID) =
1.10 (if (!check_guhs_unique) then check_metguh_unique guh (!mets) else ();
1.11 mets:= insrt metID met metID (!mets));
2.1 --- a/src/Tools/isac/KEStore.thy Mon Jan 27 21:58:57 2014 +0100
2.2 +++ b/src/Tools/isac/KEStore.thy Mon Jan 27 22:26:51 2014 +0100
2.3 @@ -117,13 +117,6 @@
2.4 fun get_ptyps () =
2.5 ML_Context.the_generic_context () |> Context.theory_of |> KEStore_Elems.get_ptyps;
2.6
2.7 -(*SWITCH: outcomment store_pbt, if all occurrences in src+test have in parallel
2.8 - SETUP ..* KEStore_Elems.add_pbt (.....) *..
2.9 -*)
2.10 -fun store_pbt (pbt as {guh,...}, pblID) =
2.11 - (if (!check_guhs_unique) then check_pblguh_unique guh (! ptyps) else ();
2.12 - ptyps:= insrt pblID pbt (rev pblID) (! ptyps));
2.13 -
2.14 *}
2.15 setup {* KEStore_Elems.add_rlss
2.16 [("e_rls", (Context.theory_name @{theory}, e_rls)),
3.1 --- a/src/Tools/isac/Knowledge/AlgEin.thy Mon Jan 27 21:58:57 2014 +0100
3.2 +++ b/src/Tools/isac/Knowledge/AlgEin.thy Mon Jan 27 22:26:51 2014 +0100
3.3 @@ -23,38 +23,8 @@
3.4
3.5 ML {*
3.6 val thy = @{theory};
3.7 -
3.8 +*}
3.9 (** problems **)
3.10 -
3.11 -store_pbt
3.12 - (prep_pbt thy "pbl_algein" [] e_pblID
3.13 - (["Berechnung"], [], e_rls, NONE,
3.14 - []));
3.15 -(* WN070405
3.16 -store_pbt
3.17 - (prep_pbt thy "pbl_algein_num" [] e_pblID
3.18 - (["numerische", "Berechnung"],
3.19 - [("#Given" ,["KantenUnten u_u", "KantenSenkrecht s_s", "KantenOben o_o"]),
3.20 - ("#Find" ,["GesamtLaenge l_l"])
3.21 - ],
3.22 - append_rls "e_rls" e_rls [],
3.23 - NONE,
3.24 - []));
3.25 -*)
3.26 -store_pbt
3.27 - (prep_pbt thy "pbl_algein_numsym" [] e_pblID
3.28 - (["numerischSymbolische", "Berechnung"],
3.29 - [("#Given" ,["KantenLaenge k_k","Querschnitt q__q"(*q_ in Biegelinie.thy*),
3.30 - "KantenUnten u_u", "KantenSenkrecht s_s", "KantenOben o_o"]),
3.31 - ("#Find" ,["GesamtLaenge l_l"])
3.32 - ],
3.33 - e_rls,
3.34 - NONE,
3.35 - [["Berechnung","erstNumerisch"],["Berechnung","erstSymbolisch"]]));
3.36 -
3.37 -(* show_ptyps();
3.38 - *)
3.39 -*}
3.40 setup {* KEStore_Elems.add_pbts
3.41 [(prep_pbt thy "pbl_algein" [] e_pblID (["Berechnung"], [], e_rls, NONE, [])),
3.42 (prep_pbt thy "pbl_algein_numsym" [] e_pblID
4.1 --- a/src/Tools/isac/Knowledge/Biegelinie.thy Mon Jan 27 21:58:57 2014 +0100
4.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy Mon Jan 27 22:26:51 2014 +0100
4.3 @@ -96,85 +96,7 @@
4.4 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
4.5
4.6 *}
4.7 -ML {*
4.8 (** problems **)
4.9 -
4.10 -store_pbt
4.11 - (prep_pbt thy "pbl_bieg" [] e_pblID
4.12 - (["Biegelinien"],
4.13 - [("#Given" ,["Traegerlaenge l_l", "Streckenlast q_q"]),
4.14 - (*("#Where",["0 < l_l"]), ...wait for < and handling Arbfix*)
4.15 - ("#Find" ,["Biegelinie b_b"]),
4.16 - ("#Relate",["Randbedingungen r_b"])
4.17 - ],
4.18 - append_rls "e_rls" e_rls [],
4.19 - NONE,
4.20 - [["IntegrierenUndKonstanteBestimmen2"]]));
4.21 -
4.22 -store_pbt
4.23 - (prep_pbt thy "pbl_bieg_mom" [] e_pblID
4.24 - (["MomentBestimmte","Biegelinien"],
4.25 - [("#Given" ,["Traegerlaenge l_l", "Streckenlast q_q"]),
4.26 - (*("#Where",["0 < l_l"]), ...wait for < and handling Arbfix*)
4.27 - ("#Find" ,["Biegelinie b_b"]),
4.28 - ("#Relate",["RandbedingungenBiegung r_b","RandbedingungenMoment r_m"])
4.29 - ],
4.30 - append_rls "e_rls" e_rls [],
4.31 - NONE,
4.32 - [["IntegrierenUndKonstanteBestimmen"]]));
4.33 -
4.34 -store_pbt
4.35 - (prep_pbt thy "pbl_bieg_momg" [] e_pblID
4.36 - (["MomentGegebene","Biegelinien"],
4.37 - [],
4.38 - append_rls "e_rls" e_rls [],
4.39 - NONE,
4.40 - [["IntegrierenUndKonstanteBestimmen","2xIntegrieren"]]));
4.41 -
4.42 -store_pbt
4.43 - (prep_pbt thy "pbl_bieg_einf" [] e_pblID
4.44 - (["einfache","Biegelinien"],
4.45 - [],
4.46 - append_rls "e_rls" e_rls [],
4.47 - NONE,
4.48 - [["IntegrierenUndKonstanteBestimmen","4x4System"]]));
4.49 -
4.50 -store_pbt
4.51 - (prep_pbt thy "pbl_bieg_momquer" [] e_pblID
4.52 - (["QuerkraftUndMomentBestimmte","Biegelinien"],
4.53 - [],
4.54 - append_rls "e_rls" e_rls [],
4.55 - NONE,
4.56 - [["IntegrierenUndKonstanteBestimmen","1xIntegrieren"]]));
4.57 -
4.58 -store_pbt
4.59 - (prep_pbt thy "pbl_bieg_vonq" [] e_pblID
4.60 - (["vonBelastungZu","Biegelinien"],
4.61 - [("#Given" ,["Streckenlast q_q","FunktionsVariable v_v"]),
4.62 - ("#Find" ,["Funktionen funs'''"])],
4.63 - append_rls "e_rls" e_rls [],
4.64 - NONE,
4.65 - [["Biegelinien","ausBelastung"]]));
4.66 -
4.67 -store_pbt
4.68 - (prep_pbt thy "pbl_bieg_randbed" [] e_pblID
4.69 - (["setzeRandbedingungen","Biegelinien"],
4.70 - [("#Given" ,["Funktionen fun_s","Randbedingungen r_b"]),
4.71 - ("#Find" ,["Gleichungen equs'''"])],
4.72 - append_rls "e_rls" e_rls [],
4.73 - NONE,
4.74 - [["Biegelinien","setzeRandbedingungenEin"]]));
4.75 -
4.76 -store_pbt
4.77 - (prep_pbt thy "pbl_equ_fromfun" [] e_pblID
4.78 - (["makeFunctionTo","equation"],
4.79 - [("#Given" ,["functionEq fu_n","substitution su_b"]),
4.80 - ("#Find" ,["equality equ'''"])],
4.81 - append_rls "e_rls" e_rls [],
4.82 - NONE,
4.83 - [["Equation","fromFunction"]]));
4.84 -KEStore_Elems.get_ptyps @{theory};
4.85 -*}
4.86 setup {* KEStore_Elems.add_pbts
4.87 [(prep_pbt thy "pbl_bieg" [] e_pblID
4.88 (["Biegelinien"],
5.1 --- a/src/Tools/isac/Knowledge/Diff.thy Mon Jan 27 21:58:57 2014 +0100
5.2 +++ b/src/Tools/isac/Knowledge/Diff.thy Mon Jan 27 22:26:51 2014 +0100
5.3 @@ -245,33 +245,8 @@
5.4 ("norm_diff", (Context.theory_name @{theory}, prep_rls norm_diff)),
5.5 ("diff_conv", (Context.theory_name @{theory}, prep_rls diff_conv)),
5.6 ("diff_sym_conv", (Context.theory_name @{theory}, prep_rls diff_sym_conv))] *}
5.7 -ML {*
5.8 +
5.9 (** problem types **)
5.10 -
5.11 -store_pbt
5.12 - (prep_pbt thy "pbl_fun" [] e_pblID
5.13 - (["function"], [], e_rls, NONE, []));
5.14 -
5.15 -store_pbt
5.16 - (prep_pbt thy "pbl_fun_deriv" [] e_pblID
5.17 - (["derivative_of","function"],
5.18 - [("#Given" ,["functionTerm f_f","differentiateFor v_v"]),
5.19 - ("#Find" ,["derivative f_f'"])
5.20 - ],
5.21 - append_rls "e_rls" e_rls [],
5.22 - SOME "Diff (f_f, v_v)", [["diff","differentiate_on_R"],
5.23 - ["diff","after_simplification"]]));
5.24 -
5.25 -(*here "named" is used differently from Integration"*)
5.26 -store_pbt
5.27 - (prep_pbt thy "pbl_fun_deriv_nam" [] e_pblID
5.28 - (["named","derivative_of","function"],
5.29 - [("#Given" ,["functionEq f_f","differentiateFor v_v"]),
5.30 - ("#Find" ,["derivativeEq f_f'"])
5.31 - ],
5.32 - append_rls "e_rls" e_rls [],
5.33 - SOME "Differentiate (f_f, v_v)", [["diff","differentiate_equality"]]));
5.34 -*}
5.35 setup {* KEStore_Elems.add_pbts
5.36 [(prep_pbt thy "pbl_fun" [] e_pblID (["function"], [], e_rls, NONE, [])),
5.37 (prep_pbt thy "pbl_fun_deriv" [] e_pblID
6.1 --- a/src/Tools/isac/Knowledge/DiffApp.thy Mon Jan 27 21:58:57 2014 +0100
6.2 +++ b/src/Tools/isac/Knowledge/DiffApp.thy Mon Jan 27 22:26:51 2014 +0100
6.3 @@ -76,66 +76,8 @@
6.4 }:rls);
6.5 *}
6.6 setup {* KEStore_Elems.add_rlss [("eval_rls", (Context.theory_name @{theory}, eval_rls))] *}
6.7 -ML{*
6.8
6.9 (** problem types **)
6.10 -
6.11 -store_pbt
6.12 - (prep_pbt thy "pbl_fun_max" [] e_pblID
6.13 - (["maximum_of","function"],
6.14 - [("#Given" ,["fixedValues f_ix"]),
6.15 - ("#Find" ,["maximum m_m","valuesFor v_s"]),
6.16 - ("#Relate",["relations r_s"])
6.17 - ],
6.18 - e_rls, NONE, []));
6.19 -
6.20 -store_pbt
6.21 - (prep_pbt thy "pbl_fun_make" [] e_pblID
6.22 - (["make","function"]:pblID,
6.23 - [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]),
6.24 - ("#Find" ,["functionEq f_1"])
6.25 - ],
6.26 - e_rls, NONE, []));
6.27 -store_pbt
6.28 - (prep_pbt thy "pbl_fun_max_expl" [] e_pblID
6.29 - (["by_explicit","make","function"]:pblID,
6.30 - [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]),
6.31 - ("#Find" ,["functionEq f_1"])
6.32 - ],
6.33 - e_rls, NONE, [["DiffApp","make_fun_by_explicit"]]));
6.34 -store_pbt
6.35 - (prep_pbt thy "pbl_fun_max_newvar" [] e_pblID
6.36 - (["by_new_variable","make","function"]:pblID,
6.37 - [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]),
6.38 - (*WN.12.5.03: precond for distinction still missing*)
6.39 - ("#Find" ,["functionEq f_1"])
6.40 - ],
6.41 - e_rls, NONE, [["DiffApp","make_fun_by_new_variable"]]));
6.42 -
6.43 -store_pbt
6.44 - (prep_pbt thy "pbl_fun_max_interv" [] e_pblID
6.45 - (["on_interval","maximum_of","function"]:pblID,
6.46 - [("#Given" ,["functionEq t_t","boundVariable v_v","interval i_tv"]),
6.47 - (*WN.12.5.03: precond for distinction still missing*)
6.48 - ("#Find" ,["maxArgument v_0"])
6.49 - ],
6.50 - e_rls, NONE, []));
6.51 -
6.52 -store_pbt
6.53 - (prep_pbt thy "pbl_tool" [] e_pblID
6.54 - (["tool"]:pblID,
6.55 - [],
6.56 - e_rls, NONE, []));
6.57 -
6.58 -store_pbt
6.59 - (prep_pbt thy "pbl_tool_findvals" [] e_pblID
6.60 - (["find_values","tool"]:pblID,
6.61 - [("#Given" ,["maxArgument m_ax","functionEq f_f","boundVariable v_v"]),
6.62 - ("#Find" ,["valuesFor v_ls"]),
6.63 - ("#Relate",["additionalRels r_s"])
6.64 - ],
6.65 - e_rls, NONE, []));
6.66 -*}
6.67 setup {* KEStore_Elems.add_pbts
6.68 [(prep_pbt thy "pbl_fun_max" [] e_pblID
6.69 (["maximum_of","function"],
7.1 --- a/src/Tools/isac/Knowledge/DiophantEq.thy Mon Jan 27 21:58:57 2014 +0100
7.2 +++ b/src/Tools/isac/Knowledge/DiophantEq.thy Mon Jan 27 22:26:51 2014 +0100
7.3 @@ -19,18 +19,6 @@
7.4 ML {*val thy = @{theory}*}
7.5
7.6 text {*problemclass for the usecase*}
7.7 -ML {*
7.8 -store_pbt
7.9 - (prep_pbt thy "pbl_equ_dio" [] e_pblID
7.10 - (["diophantine","equation"],
7.11 - [("#Given" ,["boolTestGiven e_e","intTestGiven (v_v::int)"]),
7.12 - (* TODO: drop ^^^^^*)
7.13 - ("#Where" ,[]),
7.14 - ("#Find" ,["boolTestFind s_s"])
7.15 - ],
7.16 - e_rls, SOME "solve (e_e::bool, v_v::int)",
7.17 - [["LinEq","solve_lineq_equation"]])); (*-----TODO*)
7.18 -*}
7.19 setup {* KEStore_Elems.add_pbts
7.20 [(prep_pbt thy "pbl_equ_dio" [] e_pblID
7.21 (["diophantine","equation"],
8.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Mon Jan 27 21:58:57 2014 +0100
8.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Mon Jan 27 22:26:51 2014 +0100
8.3 @@ -410,135 +410,7 @@
8.4 (Context.theory_name @{theory}, prep_rls norm_System_noadd_fractions)),
8.5 ("norm_System", (Context.theory_name @{theory}, prep_rls norm_System))] *}
8.6
8.7 -ML {*
8.8 (** problems **)
8.9 -
8.10 -store_pbt
8.11 - (prep_pbt thy "pbl_equsys" [] e_pblID
8.12 - (["system"],
8.13 - [("#Given" ,["equalities e_s", "solveForVars v_s"]),
8.14 - ("#Find" ,["solution ss'''"](*''' is copy-named*))
8.15 - ],
8.16 - append_rls "e_rls" e_rls [(*for preds in where_*)],
8.17 - SOME "solveSystem e_s v_s",
8.18 - []));
8.19 -store_pbt
8.20 - (prep_pbt thy "pbl_equsys_lin" [] e_pblID
8.21 - (["LINEAR", "system"],
8.22 - [("#Given" ,["equalities e_s", "solveForVars v_s"]),
8.23 - (*TODO.WN050929 check linearity*)
8.24 - ("#Find" ,["solution ss'''"])
8.25 - ],
8.26 - append_rls "e_rls" e_rls [(*for preds in where_*)],
8.27 - SOME "solveSystem e_s v_s",
8.28 - []));
8.29 -store_pbt
8.30 - (prep_pbt thy "pbl_equsys_lin_2x2" [] e_pblID
8.31 - (["2x2", "LINEAR", "system"],
8.32 - (*~~~~~~~~~~~~~~~~~~~~~~~~~*)
8.33 - [("#Given" ,["equalities e_s", "solveForVars v_s"]),
8.34 - ("#Where" ,["LENGTH (e_s:: bool list) = 2", "LENGTH v_s = 2"]),
8.35 - ("#Find" ,["solution ss'''"])
8.36 - ],
8.37 - append_rls "prls_2x2_linear_system" e_rls
8.38 - [Thm ("LENGTH_CONS",num_str @{thm LENGTH_CONS}),
8.39 - Thm ("LENGTH_NIL",num_str @{thm LENGTH_NIL}),
8.40 - Calc ("Groups.plus_class.plus", eval_binop "#add_"),
8.41 - Calc ("HOL.eq",eval_equal "#equal_")
8.42 - ],
8.43 - SOME "solveSystem e_s v_s",
8.44 - []));
8.45 -*}
8.46 -ML {*
8.47 -store_pbt
8.48 - (prep_pbt thy "pbl_equsys_lin_2x2_tri" [] e_pblID
8.49 - (["triangular", "2x2", "LINEAR", "system"],
8.50 - [("#Given" ,["equalities e_s", "solveForVars v_s"]),
8.51 - ("#Where" ,
8.52 - ["(tl v_s) from v_s occur_exactly_in (NTH 1 (e_s::bool list))",
8.53 - " v_s from v_s occur_exactly_in (NTH 2 (e_s::bool list))"]),
8.54 - ("#Find" ,["solution ss'''"])
8.55 - ],
8.56 - prls_triangular,
8.57 - SOME "solveSystem e_s v_s",
8.58 - [["EqSystem","top_down_substitution","2x2"]]));
8.59 -store_pbt
8.60 - (prep_pbt thy "pbl_equsys_lin_2x2_norm" [] e_pblID
8.61 - (["normalize", "2x2", "LINEAR", "system"],
8.62 - [("#Given" ,["equalities e_s", "solveForVars v_s"]),
8.63 - ("#Find" ,["solution ss'''"])
8.64 - ],
8.65 - append_rls "e_rls" e_rls [(*for preds in where_*)],
8.66 - SOME "solveSystem e_s v_s",
8.67 - [["EqSystem","normalize","2x2"]]));
8.68 -store_pbt
8.69 - (prep_pbt thy "pbl_equsys_lin_3x3" [] e_pblID
8.70 - (["3x3", "LINEAR", "system"],
8.71 - (*~~~~~~~~~~~~~~~~~~~~~~~~~*)
8.72 - [("#Given" ,["equalities e_s", "solveForVars v_s"]),
8.73 - ("#Where" ,["LENGTH (e_s:: bool list) = 3", "LENGTH v_s = 3"]),
8.74 - ("#Find" ,["solution ss'''"])
8.75 - ],
8.76 - append_rls "prls_3x3_linear_system" e_rls
8.77 - [Thm ("LENGTH_CONS",num_str @{thm LENGTH_CONS}),
8.78 - Thm ("LENGTH_NIL",num_str @{thm LENGTH_NIL}),
8.79 - Calc ("Groups.plus_class.plus", eval_binop "#add_"),
8.80 - Calc ("HOL.eq",eval_equal "#equal_")
8.81 - ],
8.82 - SOME "solveSystem e_s v_s",
8.83 - []));
8.84 -store_pbt
8.85 - (prep_pbt thy "pbl_equsys_lin_4x4" [] e_pblID
8.86 - (["4x4", "LINEAR", "system"],
8.87 - (*~~~~~~~~~~~~~~~~~~~~~~~~~*)
8.88 - [("#Given" ,["equalities e_s", "solveForVars v_s"]),
8.89 - ("#Where" ,["LENGTH (e_s:: bool list) = 4", "LENGTH v_s = 4"]),
8.90 - ("#Find" ,["solution ss'''"])
8.91 - ],
8.92 - append_rls "prls_4x4_linear_system" e_rls
8.93 - [Thm ("LENGTH_CONS",num_str @{thm LENGTH_CONS}),
8.94 - Thm ("LENGTH_NIL",num_str @{thm LENGTH_NIL}),
8.95 - Calc ("Groups.plus_class.plus", eval_binop "#add_"),
8.96 - Calc ("HOL.eq",eval_equal "#equal_")
8.97 - ],
8.98 - SOME "solveSystem e_s v_s",
8.99 - []));
8.100 -*}
8.101 -ML {*
8.102 -store_pbt
8.103 - (prep_pbt thy "pbl_equsys_lin_4x4_tri" [] e_pblID
8.104 - (["triangular", "4x4", "LINEAR", "system"],
8.105 - [("#Given" ,["equalities e_s", "solveForVars v_s"]),
8.106 - ("#Where" , (*accepts missing variables up to diagional form*)
8.107 - ["(NTH 1 (v_s::real list)) occurs_in (NTH 1 (e_s::bool list))",
8.108 - "(NTH 2 (v_s::real list)) occurs_in (NTH 2 (e_s::bool list))",
8.109 - "(NTH 3 (v_s::real list)) occurs_in (NTH 3 (e_s::bool list))",
8.110 - "(NTH 4 (v_s::real list)) occurs_in (NTH 4 (e_s::bool list))"
8.111 - ]),
8.112 - ("#Find" ,["solution ss'''"])
8.113 - ],
8.114 - append_rls "prls_tri_4x4_lin_sys" prls_triangular
8.115 - [Calc ("Atools.occurs'_in",eval_occurs_in "")],
8.116 - SOME "solveSystem e_s v_s",
8.117 - [["EqSystem","top_down_substitution","4x4"]]));
8.118 -*}
8.119 -ML {*
8.120 -store_pbt
8.121 - (prep_pbt thy "pbl_equsys_lin_4x4_norm" [] e_pblID
8.122 - (["normalize", "4x4", "LINEAR", "system"],
8.123 - [("#Given" ,["equalities e_s", "solveForVars v_s"]),
8.124 - (*LENGTH is checked 1 level above*)
8.125 - ("#Find" ,["solution ss'''"])
8.126 - ],
8.127 - append_rls "e_rls" e_rls [(*for preds in where_*)],
8.128 - SOME "solveSystem e_s v_s",
8.129 - [["EqSystem","normalize","4x4"]]));
8.130 -
8.131 -
8.132 -(* show_ptyps();
8.133 - *)
8.134 -
8.135 -*}
8.136 setup {* KEStore_Elems.add_pbts
8.137 [(prep_pbt thy "pbl_equsys" [] e_pblID
8.138 (["system"],
9.1 --- a/src/Tools/isac/Knowledge/Equation.thy Mon Jan 27 21:58:57 2014 +0100
9.2 +++ b/src/Tools/isac/Knowledge/Equation.thy Mon Jan 27 22:26:51 2014 +0100
9.3 @@ -47,28 +47,6 @@
9.4 *}
9.5 setup {* KEStore_Elems.add_rlss [("univariate_equation_prls",
9.6 (Context.theory_name @{theory}, prep_rls univariate_equation_prls))] *}
9.7 -ML {*
9.8 -store_pbt
9.9 - (prep_pbt thy "pbl_equ" [] e_pblID
9.10 - (["equation"],
9.11 - [("#Given" ,["equality e_e","solveFor v_v"]),
9.12 - ("#Where" ,["matches (?a = ?b) e_e"]),
9.13 - ("#Find" ,["solutions v_v'i'"])
9.14 - ],
9.15 - append_rls "equation_prls" e_rls
9.16 - [Calc ("Tools.matches",eval_matches "")],
9.17 - SOME "solve (e_e::bool, v_v)",
9.18 - []));
9.19 -
9.20 -store_pbt
9.21 - (prep_pbt thy "pbl_equ_univ" [] e_pblID
9.22 - (["univariate","equation"],
9.23 - [("#Given" ,["equality e_e","solveFor v_v"]),
9.24 - ("#Where" ,["matches (?a = ?b) e_e"]),
9.25 - ("#Find" ,["solutions v_v'i'"])
9.26 - ],
9.27 - univariate_equation_prls,SOME "solve (e_e::bool, v_v)",[]));
9.28 -*}
9.29 setup {* KEStore_Elems.add_pbts
9.30 [(prep_pbt thy "pbl_equ" [] e_pblID
9.31 (["equation"],
10.1 --- a/src/Tools/isac/Knowledge/InsSort.thy Mon Jan 27 21:58:57 2014 +0100
10.2 +++ b/src/Tools/isac/Knowledge/InsSort.thy Mon Jan 27 22:26:51 2014 +0100
10.3 @@ -58,25 +58,7 @@
10.4
10.5 sort_def "sort ls = foldr ins ls []"
10.6
10.7 -ML {*
10.8 (** problem type **)
10.9 -
10.10 -store_pbt
10.11 - (prep_pbt @{theory "InsSort"}
10.12 - (["functional"]:pblID,
10.13 - [("#Given" ,["unsorted u_"]),
10.14 - ("#Find" ,["sorted s_"])
10.15 - ],
10.16 - []));
10.17 -
10.18 -store_pbt
10.19 - (prep_pbt @{theory "InsSort"}
10.20 - (["inssort","functional"]:pblID,
10.21 - [("#Given" ,["unsorted u_"]),
10.22 - ("#Find" ,["sorted s_"])
10.23 - ],
10.24 - []));
10.25 -*}
10.26 setup {* KEStore_Elems.add_pbts
10.27 [(prep_pbt @{theory "InsSort"}
10.28 (["functional"]:pblID,
11.1 --- a/src/Tools/isac/Knowledge/Integrate.thy Mon Jan 27 21:58:57 2014 +0100
11.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy Mon Jan 27 22:26:51 2014 +0100
11.3 @@ -333,32 +333,8 @@
11.4 prep_rls norm_Rational_noadd_fractions)),
11.5 ("norm_Rational_rls_noadd_fractions", (Context.theory_name @{theory},
11.6 prep_rls norm_Rational_rls_noadd_fractions))] *}
11.7 -ML {*
11.8
11.9 (** problems **)
11.10 -
11.11 -store_pbt
11.12 - (prep_pbt thy "pbl_fun_integ" [] e_pblID
11.13 - (["integrate","function"],
11.14 - [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
11.15 - ("#Find" ,["antiDerivative F_F"])
11.16 - ],
11.17 - append_rls "e_rls" e_rls [(*for preds in where_*)],
11.18 - SOME "Integrate (f_f, v_v)",
11.19 - [["diff","integration"]]));
11.20 -
11.21 -(*here "named" is used differently from Differentiation"*)
11.22 -store_pbt
11.23 - (prep_pbt thy "pbl_fun_integ_nam" [] e_pblID
11.24 - (["named","integrate","function"],
11.25 - [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
11.26 - ("#Find" ,["antiDerivativeName F_F"])
11.27 - ],
11.28 - append_rls "e_rls" e_rls [(*for preds in where_*)],
11.29 - SOME "Integrate (f_f, v_v)",
11.30 - [["diff","integration","named"]]));
11.31 -
11.32 -*}
11.33 setup {* KEStore_Elems.add_pbts
11.34 [(prep_pbt thy "pbl_fun_integ" [] e_pblID
11.35 (["integrate","function"],
12.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Mon Jan 27 21:58:57 2014 +0100
12.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Mon Jan 27 22:26:51 2014 +0100
12.3 @@ -45,33 +45,6 @@
12.4 subsection{*Define the Specification*}
12.5 ML {*
12.6 val thy = @{theory};
12.7 -
12.8 -store_pbt
12.9 - (prep_pbt thy "pbl_SP" [] e_pblID
12.10 - (["SignalProcessing"], [], e_rls, NONE, []));
12.11 -store_pbt
12.12 - (prep_pbt thy "pbl_SP_Ztrans" [] e_pblID
12.13 - (["Z_Transform","SignalProcessing"], [], e_rls, NONE, []));
12.14 -store_pbt
12.15 - (prep_pbt thy "pbl_SP_Ztrans_inv" [] e_pblID
12.16 - (["Inverse", "Z_Transform", "SignalProcessing"],
12.17 - (*^ capital letter breaks coding standard
12.18 - because "inverse" = Const ("Rings.inverse_class.inverse", ..*)
12.19 - [("#Given" ,["filterExpression (X_eq::bool)"]),
12.20 - ("#Find" ,["stepResponse (n_eq::bool)"])
12.21 - ],
12.22 - append_rls "e_rls" e_rls [(*for preds in where_*)], NONE,
12.23 - [["SignalProcessing","Z_Transform","Inverse"]]));
12.24 -*}
12.25 -ML {*
12.26 - store_pbt
12.27 - (prep_pbt thy "pbl_SP_Ztrans_inv" [] e_pblID
12.28 - (["Inverse", "Z_Transform", "SignalProcessing"],
12.29 - [("#Given" ,["filterExpression X_eq"]),
12.30 - ("#Find" ,["stepResponse n_eq"])
12.31 - ],
12.32 - append_rls "e_rls" e_rls [(*for preds in where_*)], NONE,
12.33 - [["SignalProcessing","Z_Transform","Inverse"]]));
12.34 *}
12.35 setup {* KEStore_Elems.add_pbts
12.36 [(prep_pbt thy "pbl_SP" [] e_pblID (["SignalProcessing"], [], e_rls, NONE, [])),
13.1 --- a/src/Tools/isac/Knowledge/LinEq.thy Mon Jan 27 21:58:57 2014 +0100
13.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy Mon Jan 27 22:26:51 2014 +0100
13.3 @@ -117,29 +117,9 @@
13.4 *}
13.5 setup {* KEStore_Elems.add_rlss
13.6 [("LinEq_simplify", (Context.theory_name @{theory}, LinEq_simplify))] *}
13.7 -ML {*
13.8
13.9 (*----------------------------- problem types --------------------------------*)
13.10 -(*
13.11 -show_ptyps();
13.12 -(get_pbt ["LINEAR","univariate","equation"]);
13.13 -*)
13.14 -
13.15 (* ---------linear----------- *)
13.16 -store_pbt
13.17 - (prep_pbt thy "pbl_equ_univ_lin" [] e_pblID
13.18 - (["LINEAR","univariate","equation"],
13.19 - [("#Given" ,["equality e_e","solveFor v_v"]),
13.20 - ("#Where" ,["HOL.False", (*WN0509 just detected: this pbl can never be used?!?*)
13.21 - "Not( (lhs e_e) is_polyrat_in v_v)",
13.22 - "Not( (rhs e_e) is_polyrat_in v_v)",
13.23 - "((lhs e_e) has_degree_in v_v)=1",
13.24 - "((rhs e_e) has_degree_in v_v)=1"]),
13.25 - ("#Find" ,["solutions v_v'i'"])
13.26 - ],
13.27 - LinEq_prls, SOME "solve (e_e::bool, v_v)",
13.28 - [["LinEq","solve_lineq_equation"]]));
13.29 -*}
13.30 setup {* KEStore_Elems.add_pbts
13.31 [(prep_pbt thy "pbl_equ_univ_lin" [] e_pblID
13.32 (["LINEAR", "univariate", "equation"],
14.1 --- a/src/Tools/isac/Knowledge/LogExp.thy Mon Jan 27 21:58:57 2014 +0100
14.2 +++ b/src/Tools/isac/Knowledge/LogExp.thy Mon Jan 27 22:26:51 2014 +0100
14.3 @@ -26,20 +26,8 @@
14.4
14.5 ML {*
14.6 val thy = @{theory};
14.7 -
14.8 +*}
14.9 (** problems **)
14.10 -store_pbt
14.11 - (prep_pbt thy "pbl_test_equ_univ_log" [] e_pblID
14.12 - (["logarithmic","univariate","equation"],
14.13 - [("#Given",["equality e_e","solveFor v_v"]),
14.14 - ("#Where",["matches ((?a log ?v_v) = ?b) e_e"]),
14.15 - ("#Find" ,["solutions v_v'i'"]),
14.16 - ("#With" ,["||(lhs (Subst (v'i', v_v) e_e) - " ^
14.17 - " (rhs (Subst (v'i', v_v) e_e) || < eps)"])
14.18 - ],
14.19 - PolyEq_prls, SOME "solve (e_e::bool, v_v)",
14.20 - [["Equation","solve_log"]]));
14.21 -*}
14.22 setup {* KEStore_Elems.add_pbts
14.23 [(prep_pbt thy "pbl_test_equ_univ_log" [] e_pblID
14.24 (["logarithmic","univariate","equation"],
15.1 --- a/src/Tools/isac/Knowledge/Partial_Fractions.thy Mon Jan 27 21:58:57 2014 +0100
15.2 +++ b/src/Tools/isac/Knowledge/Partial_Fractions.thy Mon Jan 27 22:26:51 2014 +0100
15.3 @@ -168,19 +168,6 @@
15.4
15.5 ML {*
15.6 check_guhs_unique := false; (*WN120307 REMOVE after editing*)
15.7 -store_pbt
15.8 - (prep_pbt @{theory} "pbl_simp_rat_partfrac" [] e_pblID
15.9 - (["partial_fraction", "rational", "simplification"],
15.10 - [("#Given" ,["functionTerm t_t", "solveFor v_v"]),
15.11 - (* TODO: call this sub-problem with appropriate functionTerm:
15.12 - leading coefficient of the denominator is 1: to be checked here! and..
15.13 - ("#Where" ,["((get_numerator t_t) has_degree_in v_v) <
15.14 - ((get_denominator t_t) has_degree_in v_v)"]), TODO*)
15.15 - ("#Find" ,["decomposedFunction p_p'''"])
15.16 - ],
15.17 - append_rls "e_rls" e_rls [(*for preds in where_ TODO*)],
15.18 - NONE,
15.19 - [["simplification","of_rationals","to_partial_fraction"]]));
15.20 *}
15.21 setup {* KEStore_Elems.add_pbts
15.22 [(prep_pbt @{theory} "pbl_simp_rat_partfrac" [] e_pblID
16.1 --- a/src/Tools/isac/Knowledge/Poly.thy Mon Jan 27 21:58:57 2014 +0100
16.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Mon Jan 27 22:26:51 2014 +0100
16.3 @@ -1592,21 +1592,7 @@
16.4 ("is_multUnordered", ("Poly.is'_multUnordered", eval_is_multUnordered"")),
16.5 ("is_addUnordered", ("Poly.is'_addUnordered", eval_is_addUnordered ""))] *}
16.6
16.7 -ML {*
16.8 (** problems **)
16.9 -
16.10 -store_pbt
16.11 - (prep_pbt thy "pbl_simp_poly" [] e_pblID
16.12 - (["polynomial","simplification"],
16.13 - [("#Given" ,["Term t_t"]),
16.14 - ("#Where" ,["t_t is_polyexp"]),
16.15 - ("#Find" ,["normalform n_n"])
16.16 - ],
16.17 - append_rls "e_rls" e_rls [(*for preds in where_*)
16.18 - Calc ("Poly.is'_polyexp", eval_is_polyexp "")],
16.19 - SOME "Simplify t_t",
16.20 - [["simplification","for_polynomials"]]));
16.21 -*}
16.22 setup {* KEStore_Elems.add_pbts
16.23 [(prep_pbt thy "pbl_simp_poly" [] e_pblID
16.24 (["polynomial","simplification"],
17.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Mon Jan 27 21:58:57 2014 +0100
17.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Mon Jan 27 22:26:51 2014 +0100
17.3 @@ -834,185 +834,11 @@
17.4 ("d3_polyeq_simplify", (Context.theory_name @{theory}, d3_polyeq_simplify)),
17.5 ("d4_polyeq_simplify", (Context.theory_name @{theory}, d4_polyeq_simplify))] *}
17.6 ML{*
17.7 -
17.8 (*------------------------problems------------------------*)
17.9 (*
17.10 (get_pbt ["degree_2","polynomial","univariate","equation"]);
17.11 show_ptyps();
17.12 *)
17.13 -
17.14 -(*-------------------------poly-----------------------*)
17.15 -store_pbt
17.16 - (prep_pbt thy "pbl_equ_univ_poly" [] e_pblID
17.17 - (["polynomial","univariate","equation"],
17.18 - [("#Given" ,["equality e_e","solveFor v_v"]),
17.19 - ("#Where" ,["~((e_e::bool) is_ratequation_in (v_v::real))",
17.20 - "~((lhs e_e) is_rootTerm_in (v_v::real))",
17.21 - "~((rhs e_e) is_rootTerm_in (v_v::real))"]),
17.22 - ("#Find" ,["solutions v_v'i'"])
17.23 - ],
17.24 - PolyEq_prls, SOME "solve (e_e::bool, v_v)",
17.25 - []));
17.26 -(*--- d0 ---*)
17.27 -store_pbt
17.28 - (prep_pbt thy "pbl_equ_univ_poly_deg0" [] e_pblID
17.29 - (["degree_0","polynomial","univariate","equation"],
17.30 - [("#Given" ,["equality e_e","solveFor v_v"]),
17.31 - ("#Where" ,["matches (?a = 0) e_e",
17.32 - "(lhs e_e) is_poly_in v_v",
17.33 - "((lhs e_e) has_degree_in v_v ) = 0"
17.34 - ]),
17.35 - ("#Find" ,["solutions v_v'i'"])
17.36 - ],
17.37 - PolyEq_prls, SOME "solve (e_e::bool, v_v)",
17.38 - [["PolyEq","solve_d0_polyeq_equation"]]));
17.39 -
17.40 -(*--- d1 ---*)
17.41 -store_pbt
17.42 - (prep_pbt thy "pbl_equ_univ_poly_deg1" [] e_pblID
17.43 - (["degree_1","polynomial","univariate","equation"],
17.44 - [("#Given" ,["equality e_e","solveFor v_v"]),
17.45 - ("#Where" ,["matches (?a = 0) e_e",
17.46 - "(lhs e_e) is_poly_in v_v",
17.47 - "((lhs e_e) has_degree_in v_v ) = 1"
17.48 - ]),
17.49 - ("#Find" ,["solutions v_v'i'"])
17.50 - ],
17.51 - PolyEq_prls, SOME "solve (e_e::bool, v_v)",
17.52 - [["PolyEq","solve_d1_polyeq_equation"]]));
17.53 -*}
17.54 -ML{*
17.55 -(*--- d2 ---*)
17.56 -store_pbt
17.57 - (prep_pbt thy "pbl_equ_univ_poly_deg2" [] e_pblID
17.58 - (["degree_2","polynomial","univariate","equation"],
17.59 - [("#Given" ,["equality e_e","solveFor v_v"]),
17.60 - ("#Where" ,["matches (?a = 0) e_e",
17.61 - "(lhs e_e) is_poly_in v_v ",
17.62 - "((lhs e_e) has_degree_in v_v ) = 2"]),
17.63 - ("#Find" ,["solutions v_v'i'"])
17.64 - ],
17.65 - PolyEq_prls, SOME "solve (e_e::bool, v_v)",
17.66 - [["PolyEq","solve_d2_polyeq_equation"]]));
17.67 -
17.68 - store_pbt
17.69 - (prep_pbt thy "pbl_equ_univ_poly_deg2_sqonly" [] e_pblID
17.70 - (["sq_only","degree_2","polynomial","univariate","equation"],
17.71 - [("#Given" ,["equality e_e","solveFor v_v"]),
17.72 - ("#Where" ,["matches ( ?a + ?v_^^^2 = 0) e_e | " ^
17.73 - "matches ( ?a + ?b*?v_^^^2 = 0) e_e | " ^
17.74 - "matches ( ?v_^^^2 = 0) e_e | " ^
17.75 - "matches ( ?b*?v_^^^2 = 0) e_e" ,
17.76 - "Not (matches (?a + ?v_ + ?v_^^^2 = 0) e_e) &" ^
17.77 - "Not (matches (?a + ?b*?v_ + ?v_^^^2 = 0) e_e) &" ^
17.78 - "Not (matches (?a + ?v_ + ?c*?v_^^^2 = 0) e_e) &" ^
17.79 - "Not (matches (?a + ?b*?v_ + ?c*?v_^^^2 = 0) e_e) &" ^
17.80 - "Not (matches ( ?v_ + ?v_^^^2 = 0) e_e) &" ^
17.81 - "Not (matches ( ?b*?v_ + ?v_^^^2 = 0) e_e) &" ^
17.82 - "Not (matches ( ?v_ + ?c*?v_^^^2 = 0) e_e) &" ^
17.83 - "Not (matches ( ?b*?v_ + ?c*?v_^^^2 = 0) e_e)"]),
17.84 - ("#Find" ,["solutions v_v'i'"])
17.85 - ],
17.86 - PolyEq_prls, SOME "solve (e_e::bool, v_v)",
17.87 - [["PolyEq","solve_d2_polyeq_sqonly_equation"]]));
17.88 -
17.89 -store_pbt
17.90 - (prep_pbt thy "pbl_equ_univ_poly_deg2_bdvonly" [] e_pblID
17.91 - (["bdv_only","degree_2","polynomial","univariate","equation"],
17.92 - [("#Given" ,["equality e_e","solveFor v_v"]),
17.93 - ("#Where" ,["matches (?a*?v_ + ?v_^^^2 = 0) e_e | " ^
17.94 - "matches ( ?v_ + ?v_^^^2 = 0) e_e | " ^
17.95 - "matches ( ?v_ + ?b*?v_^^^2 = 0) e_e | " ^
17.96 - "matches (?a*?v_ + ?b*?v_^^^2 = 0) e_e | " ^
17.97 - "matches ( ?v_^^^2 = 0) e_e | " ^
17.98 - "matches ( ?b*?v_^^^2 = 0) e_e "]),
17.99 - ("#Find" ,["solutions v_v'i'"])
17.100 - ],
17.101 - PolyEq_prls, SOME "solve (e_e::bool, v_v)",
17.102 - [["PolyEq","solve_d2_polyeq_bdvonly_equation"]]));
17.103 -
17.104 -store_pbt
17.105 - (prep_pbt thy "pbl_equ_univ_poly_deg2_pq" [] e_pblID
17.106 - (["pqFormula","degree_2","polynomial","univariate","equation"],
17.107 - [("#Given" ,["equality e_e","solveFor v_v"]),
17.108 - ("#Where" ,["matches (?a + 1*?v_^^^2 = 0) e_e | " ^
17.109 - "matches (?a + ?v_^^^2 = 0) e_e"]),
17.110 - ("#Find" ,["solutions v_v'i'"])
17.111 - ],
17.112 - PolyEq_prls, SOME "solve (e_e::bool, v_v)",
17.113 - [["PolyEq","solve_d2_polyeq_pq_equation"]]));
17.114 -
17.115 -store_pbt
17.116 - (prep_pbt thy "pbl_equ_univ_poly_deg2_abc" [] e_pblID
17.117 - (["abcFormula","degree_2","polynomial","univariate","equation"],
17.118 - [("#Given" ,["equality e_e","solveFor v_v"]),
17.119 - ("#Where" ,["matches (?a + ?v_^^^2 = 0) e_e | " ^
17.120 - "matches (?a + ?b*?v_^^^2 = 0) e_e"]),
17.121 - ("#Find" ,["solutions v_v'i'"])
17.122 - ],
17.123 - PolyEq_prls, SOME "solve (e_e::bool, v_v)",
17.124 - [["PolyEq","solve_d2_polyeq_abc_equation"]]));
17.125 -*}
17.126 -ML{*
17.127 -(*--- d3 ---*)
17.128 -store_pbt
17.129 - (prep_pbt thy "pbl_equ_univ_poly_deg3" [] e_pblID
17.130 - (["degree_3","polynomial","univariate","equation"],
17.131 - [("#Given" ,["equality e_e","solveFor v_v"]),
17.132 - ("#Where" ,["matches (?a = 0) e_e",
17.133 - "(lhs e_e) is_poly_in v_v ",
17.134 - "((lhs e_e) has_degree_in v_v) = 3"]),
17.135 - ("#Find" ,["solutions v_v'i'"])
17.136 - ],
17.137 - PolyEq_prls, SOME "solve (e_e::bool, v_v)",
17.138 - [["PolyEq","solve_d3_polyeq_equation"]]));
17.139 -
17.140 -(*--- d4 ---*)
17.141 -store_pbt
17.142 - (prep_pbt thy "pbl_equ_univ_poly_deg4" [] e_pblID
17.143 - (["degree_4","polynomial","univariate","equation"],
17.144 - [("#Given" ,["equality e_e","solveFor v_v"]),
17.145 - ("#Where" ,["matches (?a = 0) e_e",
17.146 - "(lhs e_e) is_poly_in v_v ",
17.147 - "((lhs e_e) has_degree_in v_v) = 4"]),
17.148 - ("#Find" ,["solutions v_v'i'"])
17.149 - ],
17.150 - PolyEq_prls, SOME "solve (e_e::bool, v_v)",
17.151 - [(*["PolyEq","solve_d4_polyeq_equation"]*)]));
17.152 -
17.153 -(*--- normalize ---*)
17.154 -store_pbt
17.155 - (prep_pbt thy "pbl_equ_univ_poly_norm" [] e_pblID
17.156 - (["normalize","polynomial","univariate","equation"],
17.157 - [("#Given" ,["equality e_e","solveFor v_v"]),
17.158 - ("#Where" ,["(Not((matches (?a = 0 ) e_e ))) |" ^
17.159 - "(Not(((lhs e_e) is_poly_in v_v)))"]),
17.160 - ("#Find" ,["solutions v_v'i'"])
17.161 - ],
17.162 - PolyEq_prls, SOME "solve (e_e::bool, v_v)",
17.163 - [["PolyEq","normalize_poly"]]));
17.164 -(*-------------------------expanded-----------------------*)
17.165 -store_pbt
17.166 - (prep_pbt thy "pbl_equ_univ_expand" [] e_pblID
17.167 - (["expanded","univariate","equation"],
17.168 - [("#Given" ,["equality e_e","solveFor v_v"]),
17.169 - ("#Where" ,["matches (?a = 0) e_e",
17.170 - "(lhs e_e) is_expanded_in v_v "]),
17.171 - ("#Find" ,["solutions v_v'i'"])
17.172 - ],
17.173 - PolyEq_prls, SOME "solve (e_e::bool, v_v)",
17.174 - []));
17.175 -
17.176 -(*--- d2 ---*)
17.177 -store_pbt
17.178 - (prep_pbt thy "pbl_equ_univ_expand_deg2" [] e_pblID
17.179 - (["degree_2","expanded","univariate","equation"],
17.180 - [("#Given" ,["equality e_e","solveFor v_v"]),
17.181 - ("#Where" ,["((lhs e_e) has_degree_in v_v) = 2"]),
17.182 - ("#Find" ,["solutions v_v'i'"])
17.183 - ],
17.184 - PolyEq_prls, SOME "solve (e_e::bool, v_v)",
17.185 - [["PolyEq","complete_square"]]));
17.186 *}
17.187 setup {* KEStore_Elems.add_pbts
17.188 [(prep_pbt thy "pbl_equ_univ_poly" [] e_pblID
18.1 --- a/src/Tools/isac/Knowledge/PolyMinus.thy Mon Jan 27 21:58:57 2014 +0100
18.2 +++ b/src/Tools/isac/Knowledge/PolyMinus.thy Mon Jan 27 22:26:51 2014 +0100
18.3 @@ -394,111 +394,8 @@
18.4 ("klammern_aufloesen", (Context.theory_name @{theory}, prep_rls klammern_aufloesen)),
18.5 ("klammern_ausmultiplizieren",
18.6 (Context.theory_name @{theory}, prep_rls klammern_ausmultiplizieren))] *}
18.7 -ML {*
18.8
18.9 (** problems **)
18.10 -
18.11 -store_pbt
18.12 - (prep_pbt thy "pbl_vereinf_poly" [] e_pblID
18.13 - (["polynom","vereinfachen"],
18.14 - [], Erls, NONE, []));
18.15 -
18.16 -store_pbt
18.17 - (prep_pbt thy "pbl_vereinf_poly_minus" [] e_pblID
18.18 - (["plus_minus","polynom","vereinfachen"],
18.19 - [("#Given" ,["Term t_t"]),
18.20 - ("#Where" ,["t_t is_polyexp",
18.21 - "Not (matchsub (?a + (?b + ?c)) t_t | " ^
18.22 - " matchsub (?a + (?b - ?c)) t_t | " ^
18.23 - " matchsub (?a - (?b + ?c)) t_t | " ^
18.24 - " matchsub (?a + (?b - ?c)) t_t )",
18.25 - "Not (matchsub (?a * (?b + ?c)) t_t | " ^
18.26 - " matchsub (?a * (?b - ?c)) t_t | " ^
18.27 - " matchsub ((?b + ?c) * ?a) t_t | " ^
18.28 - " matchsub ((?b - ?c) * ?a) t_t )"]),
18.29 - ("#Find" ,["normalform n_n"])
18.30 - ],
18.31 - append_rls "prls_pbl_vereinf_poly" e_rls
18.32 - [Calc ("Poly.is'_polyexp", eval_is_polyexp ""),
18.33 - Calc ("Tools.matchsub", eval_matchsub ""),
18.34 - Thm ("or_true", num_str @{thm or_true}),
18.35 - (*"(?a | True) = True"*)
18.36 - Thm ("or_false", num_str @{thm or_false}),
18.37 - (*"(?a | False) = ?a"*)
18.38 - Thm ("not_true",num_str @{thm not_true}),
18.39 - (*"(~ True) = False"*)
18.40 - Thm ("not_false",num_str @{thm not_false})
18.41 - (*"(~ False) = True"*)],
18.42 - SOME "Vereinfache t_t",
18.43 - [["simplification","for_polynomials","with_minus"]]));
18.44 -
18.45 -store_pbt
18.46 - (prep_pbt thy "pbl_vereinf_poly_klammer" [] e_pblID
18.47 - (["klammer","polynom","vereinfachen"],
18.48 - [("#Given" ,["Term t_t"]),
18.49 - ("#Where" ,["t_t is_polyexp",
18.50 - "Not (matchsub (?a * (?b + ?c)) t_t | " ^
18.51 - " matchsub (?a * (?b - ?c)) t_t | " ^
18.52 - " matchsub ((?b + ?c) * ?a) t_t | " ^
18.53 - " matchsub ((?b - ?c) * ?a) t_t )"]),
18.54 - ("#Find" ,["normalform n_n"])
18.55 - ],
18.56 - append_rls "prls_pbl_vereinf_poly_klammer" e_rls [Calc ("Poly.is'_polyexp", eval_is_polyexp ""),
18.57 - Calc ("Tools.matchsub", eval_matchsub ""),
18.58 - Thm ("or_true", num_str @{thm or_true}),
18.59 - (*"(?a | True) = True"*)
18.60 - Thm ("or_false", num_str @{thm or_false}),
18.61 - (*"(?a | False) = ?a"*)
18.62 - Thm ("not_true",num_str @{thm not_true}),
18.63 - (*"(~ True) = False"*)
18.64 - Thm ("not_false",num_str @{thm not_false})
18.65 - (*"(~ False) = True"*)],
18.66 - SOME "Vereinfache t_t",
18.67 - [["simplification","for_polynomials","with_parentheses"]]));
18.68 -
18.69 -store_pbt
18.70 - (prep_pbt thy "pbl_vereinf_poly_klammer_mal" [] e_pblID
18.71 - (["binom_klammer","polynom","vereinfachen"],
18.72 - [("#Given" ,["Term t_t"]),
18.73 - ("#Where" ,["t_t is_polyexp"]),
18.74 - ("#Find" ,["normalform n_n"])
18.75 - ],
18.76 - append_rls "e_rls" e_rls [(*for preds in where_*)
18.77 - Calc ("Poly.is'_polyexp", eval_is_polyexp "")],
18.78 - SOME "Vereinfache t_t",
18.79 - [["simplification","for_polynomials","with_parentheses_mult"]]));
18.80 -
18.81 -store_pbt
18.82 - (prep_pbt thy "pbl_probe" [] e_pblID
18.83 - (["probe"],
18.84 - [], Erls, NONE, []));
18.85 -
18.86 -store_pbt
18.87 - (prep_pbt thy "pbl_probe_poly" [] e_pblID
18.88 - (["polynom","probe"],
18.89 - [("#Given" ,["Pruefe e_e", "mitWert w_w"]),
18.90 - ("#Where" ,["e_e is_polyexp"]),
18.91 - ("#Find" ,["Geprueft p_p"])
18.92 - ],
18.93 - append_rls "prls_pbl_probe_poly"
18.94 - e_rls [(*for preds in where_*)
18.95 - Calc ("Poly.is'_polyexp", eval_is_polyexp "")],
18.96 - SOME "Probe e_e w_w",
18.97 - [["probe","fuer_polynom"]]));
18.98 -
18.99 -store_pbt
18.100 - (prep_pbt thy "pbl_probe_bruch" [] e_pblID
18.101 - (["bruch","probe"],
18.102 - [("#Given" ,["Pruefe e_e", "mitWert w_w"]),
18.103 - ("#Where" ,["e_e is_ratpolyexp"]),
18.104 - ("#Find" ,["Geprueft p_p"])
18.105 - ],
18.106 - append_rls "prls_pbl_probe_bruch"
18.107 - e_rls [(*for preds in where_*)
18.108 - Calc ("Rational.is'_ratpolyexp", eval_is_ratpolyexp "")],
18.109 - SOME "Probe e_e w_w",
18.110 - [["probe","fuer_bruch"]]));
18.111 -*}
18.112 setup {* KEStore_Elems.add_pbts
18.113 [(prep_pbt thy "pbl_vereinf_poly" [] e_pblID
18.114 (["polynom","vereinfachen"], [], Erls, NONE, [])),
19.1 --- a/src/Tools/isac/Knowledge/RatEq.thy Mon Jan 27 21:58:57 2014 +0100
19.2 +++ b/src/Tools/isac/Knowledge/RatEq.thy Mon Jan 27 22:26:51 2014 +0100
19.3 @@ -177,22 +177,11 @@
19.4 setup {* KEStore_Elems.add_rlss [("RatEq_simplify",
19.5 (Context.theory_name @{theory}, RatEq_simplify))] *}
19.6 ML {*
19.7 -
19.8 (*-------------------------Problem-----------------------*)
19.9 (*
19.10 (get_pbt ["rational","univariate","equation"]);
19.11 show_ptyps();
19.12 *)
19.13 -store_pbt
19.14 - (prep_pbt thy "pbl_equ_univ_rat" [] e_pblID
19.15 - (["rational","univariate","equation"],
19.16 - [("#Given" ,["equality e_e","solveFor v_v"]),
19.17 - ("#Where" ,["(e_e::bool) is_ratequation_in (v_v::real)"]),
19.18 - ("#Find" ,["solutions v_v'i'"])
19.19 - ],
19.20 -
19.21 - RatEq_prls, SOME "solve (e_e::bool, v_v)",
19.22 - [["RatEq","solve_rat_equation"]]));
19.23 *}
19.24 setup {* KEStore_Elems.add_pbts
19.25 [(prep_pbt thy "pbl_equ_univ_rat" [] e_pblID
20.1 --- a/src/Tools/isac/Knowledge/Rational.thy Mon Jan 27 21:58:57 2014 +0100
20.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Mon Jan 27 22:26:51 2014 +0100
20.3 @@ -884,18 +884,6 @@
20.4 ("cancel_p_rls", (Context.theory_name @{theory}, cancel_p_rls))] *}
20.5
20.6 section {* A problem for simplification of rationals *}
20.7 -ML {*
20.8 -store_pbt
20.9 - (prep_pbt thy "pbl_simp_rat" [] e_pblID
20.10 - (["rational","simplification"],
20.11 - [("#Given" ,["Term t_t"]),
20.12 - ("#Where" ,["t_t is_ratpolyexp"]),
20.13 - ("#Find" ,["normalform n_n"])
20.14 - ],
20.15 - append_rls "e_rls" e_rls [(*for preds in where_*)],
20.16 - SOME "Simplify t_t",
20.17 - [["simplification","of_rationals"]]));
20.18 -*}
20.19 setup {* KEStore_Elems.add_pbts
20.20 [(prep_pbt thy "pbl_simp_rat" [] e_pblID
20.21 (["rational","simplification"],
21.1 --- a/src/Tools/isac/Knowledge/RootEq.thy Mon Jan 27 21:58:57 2014 +0100
21.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy Mon Jan 27 22:26:51 2014 +0100
21.3 @@ -485,45 +485,9 @@
21.4 (get_pbt ["root'","univariate","equation"]);
21.5 show_ptyps();
21.6 *)
21.7 -(* ---------root----------- *)
21.8 -store_pbt
21.9 - (prep_pbt thy "pbl_equ_univ_root" [] e_pblID
21.10 - (["root'","univariate","equation"],
21.11 - [("#Given" ,["equality e_e","solveFor v_v"]),
21.12 - ("#Where" ,["(lhs e_e) is_rootTerm_in (v_v::real) | " ^
21.13 - "(rhs e_e) is_rootTerm_in (v_v::real)"]),
21.14 - ("#Find" ,["solutions v_v'i'"])
21.15 - ],
21.16 - RootEq_prls, SOME "solve (e_e::bool, v_v)",
21.17 - []));
21.18 -(* ---------sqrt----------- *)
21.19 -store_pbt
21.20 - (prep_pbt thy "pbl_equ_univ_root_sq" [] e_pblID
21.21 - (["sq","root'","univariate","equation"],
21.22 - [("#Given" ,["equality e_e","solveFor v_v"]),
21.23 - ("#Where" ,["( ((lhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
21.24 - " ((lhs e_e) is_normSqrtTerm_in (v_v::real)) ) |" ^
21.25 - "( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
21.26 - " ((rhs e_e) is_normSqrtTerm_in (v_v::real)) )"]),
21.27 - ("#Find" ,["solutions v_v'i'"])
21.28 - ],
21.29 - RootEq_prls, SOME "solve (e_e::bool, v_v)",
21.30 - [["RootEq","solve_sq_root_equation"]]));
21.31 -(* ---------normalize----------- *)
21.32 -store_pbt
21.33 - (prep_pbt thy "pbl_equ_univ_root_norm" [] e_pblID
21.34 - (["normalize","root'","univariate","equation"],
21.35 - [("#Given" ,["equality e_e","solveFor v_v"]),
21.36 - ("#Where" ,["( ((lhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
21.37 - " Not((lhs e_e) is_normSqrtTerm_in (v_v::real))) | " ^
21.38 - "( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
21.39 - " Not((rhs e_e) is_normSqrtTerm_in (v_v::real)))"]),
21.40 - ("#Find" ,["solutions v_v'i'"])
21.41 - ],
21.42 - RootEq_prls, SOME "solve (e_e::bool, v_v)",
21.43 - [["RootEq","norm_sq_root_equation"]]));
21.44 *}
21.45 setup {* KEStore_Elems.add_pbts
21.46 + (* ---------root----------- *)
21.47 [(prep_pbt thy "pbl_equ_univ_root" [] e_pblID
21.48 (["root'","univariate","equation"],
21.49 [("#Given" ,["equality e_e","solveFor v_v"]),
22.1 --- a/src/Tools/isac/Knowledge/RootRatEq.thy Mon Jan 27 21:58:57 2014 +0100
22.2 +++ b/src/Tools/isac/Knowledge/RootRatEq.thy Mon Jan 27 22:26:51 2014 +0100
22.3 @@ -138,17 +138,6 @@
22.4 (get_pbt ["rat","root'","univariate","equation"]);
22.5 show_ptyps();
22.6 *)
22.7 -
22.8 -store_pbt
22.9 - (prep_pbt thy "pbl_equ_univ_root_sq_rat" [] e_pblID
22.10 - (["rat","sq","root'","univariate","equation"],
22.11 - [("#Given" ,["equality e_e","solveFor v_v"]),
22.12 - ("#Where" ,["( (lhs e_e) is_rootRatAddTerm_in (v_v::real) )| " ^
22.13 - "( (rhs e_e) is_rootRatAddTerm_in (v_v::real) )"]),
22.14 - ("#Find" ,["solutions v_v'i'"])
22.15 - ],
22.16 - RootRatEq_prls, SOME "solve (e_e::bool, v_v)",
22.17 - [["RootRatEq","elim_rootrat_equation"]]));
22.18 *}
22.19 setup {* KEStore_Elems.add_pbts
22.20 [(prep_pbt thy "pbl_equ_univ_root_sq_rat" [] e_pblID
23.1 --- a/src/Tools/isac/Knowledge/Simplify.thy Mon Jan 27 21:58:57 2014 +0100
23.2 +++ b/src/Tools/isac/Knowledge/Simplify.thy Mon Jan 27 22:26:51 2014 +0100
23.3 @@ -26,28 +26,8 @@
23.4
23.5 ML {*
23.6 val thy = @{theory};
23.7 -
23.8 +*}
23.9 (** problems **)
23.10 -store_pbt
23.11 - (prep_pbt thy "pbl_simp" [] e_pblID
23.12 - (["simplification"],
23.13 - [("#Given" ,["Term t_t"]),
23.14 - ("#Find" ,["normalform n_n"])
23.15 - ],
23.16 - append_rls "e_rls" e_rls [(*for preds in where_*)],
23.17 - SOME "Simplify t_t",
23.18 - []));
23.19 -
23.20 -store_pbt
23.21 - (prep_pbt thy "pbl_vereinfache" [] e_pblID
23.22 - (["vereinfachen"],
23.23 - [("#Given" ,["Term t_t"]),
23.24 - ("#Find" ,["normalform n_n"])
23.25 - ],
23.26 - append_rls "e_rls" e_rls [(*for preds in where_*)],
23.27 - SOME "Vereinfache t_t",
23.28 - []));
23.29 -*}
23.30 setup {* KEStore_Elems.add_pbts
23.31 [(prep_pbt thy "pbl_simp" [] e_pblID
23.32 (["simplification"],
24.1 --- a/src/Tools/isac/Knowledge/Test.thy Mon Jan 27 21:58:57 2014 +0100
24.2 +++ b/src/Tools/isac/Knowledge/Test.thy Mon Jan 27 22:26:51 2014 +0100
24.3 @@ -509,67 +509,7 @@
24.4 ("matches", (Context.theory_name @{theory}, prep_rls
24.5 (append_rls "matches" testerls [Calc ("Tools.matches",eval_matches "#matches_")])))] *}
24.6
24.7 -ML {*
24.8 (** problem types **)
24.9 -store_pbt
24.10 - (prep_pbt thy "pbl_test" [] e_pblID
24.11 - (["test"],
24.12 - [],
24.13 - e_rls, NONE, []));
24.14 -store_pbt
24.15 - (prep_pbt thy "pbl_test_equ" [] e_pblID
24.16 - (["equation","test"],
24.17 - [("#Given" ,["equality e_e","solveFor v_v"]),
24.18 - ("#Where" ,["matches (?a = ?b) e_e"]),
24.19 - ("#Find" ,["solutions v_v'i'"])
24.20 - ],
24.21 - assoc_rls' @{theory} "matches",
24.22 - SOME "solve (e_e::bool, v_v)", []));
24.23 -
24.24 -store_pbt
24.25 - (prep_pbt thy "pbl_test_uni" [] e_pblID
24.26 - (["univariate","equation","test"],
24.27 - [("#Given" ,["equality e_e","solveFor v_v"]),
24.28 - ("#Where" ,["matches (?a = ?b) e_e"]),
24.29 - ("#Find" ,["solutions v_v'i'"])
24.30 - ],
24.31 - assoc_rls' @{theory} "matches",
24.32 - SOME "solve (e_e::bool, v_v)", []));
24.33 -
24.34 -store_pbt
24.35 - (prep_pbt thy "pbl_test_uni_lin" [] e_pblID
24.36 - (["LINEAR","univariate","equation","test"],
24.37 - [("#Given" ,["equality e_e","solveFor v_v"]),
24.38 - ("#Where" ,["(matches ( v_v = 0) e_e) | (matches ( ?b*v_v = 0) e_e) |" ^
24.39 - "(matches (?a+v_v = 0) e_e) | (matches (?a+?b*v_v = 0) e_e) "]),
24.40 - ("#Find" ,["solutions v_v'i'"])
24.41 - ],
24.42 - assoc_rls' @{theory} "matches",
24.43 - SOME "solve (e_e::bool, v_v)", [["Test","solve_linear"]]));
24.44 -
24.45 -(*25.8.01 ------
24.46 -store_pbt
24.47 - (prep_pbt thy
24.48 - (["thy"],
24.49 - [("#Given" ,"boolTestGiven g_g"),
24.50 - ("#Find" ,"boolTestFind f_f")
24.51 - ],
24.52 - []));
24.53 -
24.54 -store_pbt
24.55 - (prep_pbt thy
24.56 - (["testeq","thy"],
24.57 - [("#Given" ,"boolTestGiven g_g"),
24.58 - ("#Find" ,"boolTestFind f_f")
24.59 - ],
24.60 - []));
24.61 -
24.62 -
24.63 -val ttt = (term_of o the o (parse (Thy_Info.get_theory "Isac"))) "(matches ( v_v = 0) e_e)";
24.64 -
24.65 - ------ 25.8.01*)
24.66 -
24.67 -*}
24.68 setup {* KEStore_Elems.add_pbts
24.69 [(prep_pbt thy "pbl_test" [] e_pblID (["test"], [], e_rls, NONE, [])),
24.70 (prep_pbt thy "pbl_test_equ" [] e_pblID
24.71 @@ -602,6 +542,10 @@
24.72 [("#Given" ,"boolTestGiven g_g"),
24.73 ("#Find" ,"boolTestFind f_f")],
24.74 []))*)] *}
24.75 +(*val ttt = (term_of o the o (parse (Thy_Info.get_theory "Isac"))) "(matches ( v_v = 0) e_e)";
24.76 +
24.77 + ------ 25.8.01*)
24.78 +
24.79 ML {*
24.80 (** methods **)
24.81 store_met
24.82 @@ -791,22 +735,18 @@
24.83 is_denom bdVar div_op t andalso bin_ops_only t;
24.84
24.85 *}
24.86 -ML {*
24.87 -
24.88 (** problem types **)
24.89 -
24.90 -store_pbt
24.91 - (prep_pbt thy "pbl_test_uni_plain2" [] e_pblID
24.92 - (["plain_square","univariate","equation","test"],
24.93 - [("#Given" ,["equality e_e","solveFor v_v"]),
24.94 - ("#Where" ,["(matches (?a + ?b*v_v ^^^2 = 0) e_e) |" ^
24.95 - "(matches ( ?b*v_v ^^^2 = 0) e_e) |" ^
24.96 - "(matches (?a + v_v ^^^2 = 0) e_e) |" ^
24.97 - "(matches ( v_v ^^^2 = 0) e_e)"]),
24.98 - ("#Find" ,["solutions v_v'i'"])
24.99 - ],
24.100 - assoc_rls' @{theory} "matches",
24.101 - SOME "solve (e_e::bool, v_v)", [["Test","solve_plain_square"]]));
24.102 +setup {* KEStore_Elems.add_pbts
24.103 + [(prep_pbt thy "pbl_test_uni_plain2" [] e_pblID
24.104 + (["plain_square","univariate","equation","test"],
24.105 + [("#Given" ,["equality e_e","solveFor v_v"]),
24.106 + ("#Where" ,["(matches (?a + ?b*v_v ^^^2 = 0) e_e) |" ^
24.107 + "(matches ( ?b*v_v ^^^2 = 0) e_e) |" ^
24.108 + "(matches (?a + v_v ^^^2 = 0) e_e) |" ^
24.109 + "(matches ( v_v ^^^2 = 0) e_e)"]),
24.110 + ("#Find" ,["solutions v_v'i'"])],
24.111 + assoc_rls' @{theory} "matches",
24.112 + SOME "solve (e_e::bool, v_v)", [["Test","solve_plain_square"]]))] *}
24.113 (*
24.114 val e_e = (term_of o the o (parse thy)) "e_e::bool";
24.115 val ve = (term_of o the o (parse thy)) "4 + 3*x^^^2 = 0";
24.116 @@ -829,98 +769,6 @@
24.117 val ct = "HOL.True" : cterm
24.118
24.119 *)
24.120 -
24.121 -*}
24.122 -setup {* KEStore_Elems.add_pbts
24.123 - [(prep_pbt thy "pbl_test_uni_plain2" [] e_pblID
24.124 - (["plain_square","univariate","equation","test"],
24.125 - [("#Given" ,["equality e_e","solveFor v_v"]),
24.126 - ("#Where" ,["(matches (?a + ?b*v_v ^^^2 = 0) e_e) |" ^
24.127 - "(matches ( ?b*v_v ^^^2 = 0) e_e) |" ^
24.128 - "(matches (?a + v_v ^^^2 = 0) e_e) |" ^
24.129 - "(matches ( v_v ^^^2 = 0) e_e)"]),
24.130 - ("#Find" ,["solutions v_v'i'"])],
24.131 - assoc_rls' @{theory} "matches",
24.132 - SOME "solve (e_e::bool, v_v)", [["Test","solve_plain_square"]]))] *}
24.133 -ML {*
24.134 -store_pbt
24.135 - (prep_pbt thy "pbl_test_uni_poly" [] e_pblID
24.136 - (["polynomial","univariate","equation","test"],
24.137 - [("#Given" ,["equality (v_v ^^^2 + p_p * v_v + q__q = 0)","solveFor v_v"]),
24.138 - ("#Where" ,["HOL.False"]),
24.139 - ("#Find" ,["solutions v_v'i'"])
24.140 - ],
24.141 - e_rls, SOME "solve (e_e::bool, v_v)", []));
24.142 -
24.143 -store_pbt
24.144 - (prep_pbt thy "pbl_test_uni_poly_deg2" [] e_pblID
24.145 - (["degree_two","polynomial","univariate","equation","test"],
24.146 - [("#Given" ,["equality (v_v ^^^2 + p_p * v_v + q__q = 0)","solveFor v_v"]),
24.147 - ("#Find" ,["solutions v_v'i'"])
24.148 - ],
24.149 - e_rls, SOME "solve (v_v ^^^2 + p_p * v_v + q__q = 0, v_v)", []));
24.150 -
24.151 -store_pbt
24.152 - (prep_pbt thy "pbl_test_uni_poly_deg2_pq" [] e_pblID
24.153 - (["pq_formula","degree_two","polynomial","univariate","equation","test"],
24.154 - [("#Given" ,["equality (v_v ^^^2 + p_p * v_v + q__q = 0)","solveFor v_v"]),
24.155 - ("#Find" ,["solutions v_v'i'"])
24.156 - ],
24.157 - e_rls, SOME "solve (v_v ^^^2 + p_p * v_v + q__q = 0, v_v)", []));
24.158 -
24.159 -store_pbt
24.160 - (prep_pbt thy "pbl_test_uni_poly_deg2_abc" [] e_pblID
24.161 - (["abc_formula","degree_two","polynomial","univariate","equation","test"],
24.162 - [("#Given" ,["equality (a_a * x ^^^2 + b_b * x + c_c = 0)","solveFor v_v"]),
24.163 - ("#Find" ,["solutions v_v'i'"])
24.164 - ],
24.165 - e_rls, SOME "solve (a_a * x ^^^2 + b_b * x + c_c = 0, v_v)", []));
24.166 -
24.167 -*}
24.168 -ML {*
24.169 -store_pbt
24.170 - (prep_pbt thy "pbl_test_uni_root" [] e_pblID
24.171 - (["squareroot","univariate","equation","test"],
24.172 - [("#Given" ,["equality e_e","solveFor v_v"]),
24.173 - ("#Where" ,["precond_rootpbl v_v"]),
24.174 - ("#Find" ,["solutions v_v'i'"])
24.175 - ],
24.176 - append_rls "contains_root" e_rls [Calc ("Test.contains'_root",
24.177 - eval_contains_root "#contains_root_")],
24.178 - SOME "solve (e_e::bool, v_v)", [["Test","square_equation"]]));
24.179 -
24.180 -store_pbt
24.181 - (prep_pbt thy "pbl_test_uni_norm" [] e_pblID
24.182 - (["normalize","univariate","equation","test"],
24.183 - [("#Given" ,["equality e_e","solveFor v_v"]),
24.184 - ("#Where" ,[]),
24.185 - ("#Find" ,["solutions v_v'i'"])
24.186 - ],
24.187 - e_rls, SOME "solve (e_e::bool, v_v)", [["Test","norm_univar_equation"]]));
24.188 -
24.189 -store_pbt
24.190 - (prep_pbt thy "pbl_test_uni_roottest" [] e_pblID
24.191 - (["sqroot-test","univariate","equation","test"],
24.192 - [("#Given" ,["equality e_e","solveFor v_v"]),
24.193 - ("#Where" ,["precond_rootpbl v_v"]),
24.194 - ("#Find" ,["solutions v_v'i'"])
24.195 - ],
24.196 - e_rls, SOME "solve (e_e::bool, v_v)", []));
24.197 -
24.198 -store_pbt
24.199 - (prep_pbt thy "pbl_test_intsimp" [] e_pblID
24.200 - (["inttype","test"],
24.201 - [("#Given" ,["intTestGiven t_t"]),
24.202 - ("#Where" ,[]),
24.203 - ("#Find" ,["intTestFind s_s"])
24.204 - ],
24.205 - e_rls, NONE, [["Test","intsimp"]]));
24.206 -(*
24.207 -show_ptyps();
24.208 -get_pbt ["inttype","test"];
24.209 -*)
24.210 -
24.211 -*}
24.212 setup {* KEStore_Elems.add_pbts
24.213 [(prep_pbt thy "pbl_test_uni_poly" [] e_pblID
24.214 (["polynomial","univariate","equation","test"],
24.215 @@ -969,6 +817,10 @@
24.216 ("#Where" ,[]),
24.217 ("#Find" ,["intTestFind s_s"])],
24.218 e_rls, NONE, [["Test","intsimp"]]))] *}
24.219 +(*
24.220 +show_ptyps();
24.221 +get_pbt ["inttype","test"];
24.222 +*)
24.223
24.224 ML {*
24.225 store_met
25.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Mon Jan 27 21:58:57 2014 +0100
25.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Mon Jan 27 22:26:51 2014 +0100
25.3 @@ -884,14 +884,6 @@
25.4 with \em SignalProcessing \normalfont and go on by creating the node
25.5 \em Z\_Transform\normalfont.*}
25.6
25.7 -ML {*
25.8 - store_pbt
25.9 - (prep_pbt thy "pbl_SP" [] e_pblID
25.10 - (["SignalProcessing"], [], e_rls, NONE, []));
25.11 - store_pbt
25.12 - (prep_pbt thy "pbl_SP_Ztrans" [] e_pblID
25.13 - (["Z_Transform","SignalProcessing"], [], e_rls, NONE, []));
25.14 -*}
25.15 setup {* KEStore_Elems.add_pbts
25.16 [prep_pbt thy "pbl_SP" [] e_pblID (["SignalProcessing"], [], e_rls, NONE, []),
25.17 prep_pbt thy "pbl_SP_Ztrans" [] e_pblID
25.18 @@ -901,16 +893,6 @@
25.19 and output parameters. We already prepared their definition in
25.20 Section~\ref{sec:deffdes}.*}
25.21
25.22 -ML {*
25.23 - store_pbt
25.24 - (prep_pbt thy "pbl_SP_Ztrans_inv" [] e_pblID
25.25 - (["Inverse", "Z_Transform", "SignalProcessing"],
25.26 - [("#Given" ,["filterExpression X_eq"]),
25.27 - ("#Find" ,["stepResponse n_eq"])
25.28 - ],
25.29 - append_rls "e_rls" e_rls [(*for preds in where_*)], NONE,
25.30 - [["SignalProcessing","Z_Transform","Inverse"]]));
25.31 -*}
25.32 setup {* KEStore_Elems.add_pbts
25.33 [prep_pbt thy "pbl_SP_Ztrans_inv" [] e_pblID
25.34 (["Inverse", "Z_Transform", "SignalProcessing"],
26.1 --- a/test/Tools/isac/OLDTESTS/script_if.sml Mon Jan 27 21:58:57 2014 +0100
26.2 +++ b/test/Tools/isac/OLDTESTS/script_if.sml Mon Jan 27 22:26:51 2014 +0100
26.3 @@ -54,18 +54,8 @@
26.4
26.5 (*WN: ^^^--- bitte nimm vorerst immer (theory "Isac"), damit wird richtig gematcht,
26.6 siehe unten. Wir werden w"ahrend der Arbeit auf diesen Fehler drauskommen*)
26.7 -store_pbt
26.8 - (prep_pbt (*Test.thy*) (theory "Isac")
26.9 - (["root'","univariate","equation","test"],
26.10 - [("#Given" ,["equality e_e","solveFor v_v"]),
26.11 - ("#Where" ,["is_rootequation_in (e_e::bool) (v_::real)"]),
26.12 - ("#Find" ,["solutions v_i_"])
26.13 - ],
26.14 - append_rls e_rls [Calc ("Test.is'_rootequation'_in",
26.15 - eval_is_rootequation_in "")],
26.16 - [("Test","methode")]));
26.17
26.18 -Test_KEStore_Elems.add_pbts
26.19 +KEStore_Elems.add_pbts
26.20 [prep_pbt (*Test.thy*) (theory "Isac")
26.21 (["root'","univariate","equation","test"],
26.22 [("#Given" ,["equality e_e","solveFor v_v"]),
26.23 @@ -77,20 +67,7 @@
26.24
26.25 match_pbl ["equality (sqrt(x)=1)","solveFor x","solutions L"] (get_pbt ["root'","univariate","equation","test"]);
26.26
26.27 -
26.28 -(*---------------- 29.7.02 ---------------------*)
26.29 -
26.30 -store_pbt
26.31 - (prep_pbt (theory "Isac")
26.32 - (["approximate","univariate","equation","test"],
26.33 - [("#Given" ,["equality e_e","solveFor v_v","errorBound err_"]),
26.34 - ("#Where" ,["matches (?a = ?b) e_e"]),
26.35 - ("#Find" ,["solutions v_i_"])
26.36 - ],
26.37 - append_rls e_rls [Calc ("Tools.matches",eval_matches "#matches_")],
26.38 - []));
26.39 -
26.40 -Test_KEStore_Elems.add_pbts
26.41 +KEStore_Elems.add_pbts
26.42 [prep_pbt (theory "Isac")
26.43 (["approximate","univariate","equation","test"],
26.44 [("#Given", ["equality e_e","solveFor v_v","errorBound err_"]),
27.1 --- a/test/Tools/isac/OLDTESTS/scriptnew.sml Mon Jan 27 21:58:57 2014 +0100
27.2 +++ b/test/Tools/isac/OLDTESTS/scriptnew.sml Mon Jan 27 22:26:51 2014 +0100
27.3 @@ -19,20 +19,7 @@
27.4 " --- test 30.4.02 Testterm: Repeat Repeat Or ------------------ ";
27.5 " --- test 30.4.02 Testterm: Repeat Repeat Or ------------------ ";
27.6 " --- test 30.4.02 Testterm: Repeat Repeat Or ------------------ ";
27.7 -store_pbt
27.8 - (prep_pbt Test.thy "pbl_testss" [] e_pblID
27.9 - (["tests"],
27.10 - []:(string * string list) list,
27.11 - e_rls, NONE, []));
27.12 -store_pbt
27.13 - (prep_pbt Test.thy "pbl_testss_term" [] e_pblID
27.14 - (["met_testterm","tests"],
27.15 - [("#Given" ,["realTestGiven g_"]),
27.16 - ("#Find" ,["realTestFind f_"])
27.17 - ],
27.18 - e_rls, NONE, []));
27.19 -
27.20 -Test_KEStore_Elems.add_pbts
27.21 +KEStore_Elems.add_pbts
27.22 [prep_pbt Test.thy "pbl_testss" [] e_pblID
27.23 (["tests"], []:(string * string list) list, e_rls, NONE, []),
27.24 prep_pbt Test.thy "pbl_testss_term" [] e_pblID
27.25 @@ -102,14 +89,7 @@
27.26 " --- test 9.5.02 Testeq: While Try Repeat @@ ------------------ ";
27.27 " --- test 9.5.02 Testeq: While Try Repeat @@ ------------------ ";
27.28 " --- test 9.5.02 Testeq: While Try Repeat @@ ------------------ ";
27.29 -store_pbt
27.30 - (prep_pbt Test.thy "pbl_testss_eq" [] e_pblID
27.31 - (["met_testeq","tests"],
27.32 - [("#Given" ,["boolTestGiven e_e"]),
27.33 - ("#Find" ,["boolTestFind v_i_"])
27.34 - ],
27.35 - e_rls, NONE, []));
27.36 -Test_KEStore_Elems.add_pbts
27.37 +KEStore_Elems.add_pbts
27.38 [prep_pbt Test.thy "pbl_testss_eq" [] e_pblID
27.39 (["met_testeq","tests"],
27.40 [("#Given" ,["boolTestGiven e_e"]),
28.1 --- a/test/Tools/isac/ProgLang/calculate.sml Mon Jan 27 21:58:57 2014 +0100
28.2 +++ b/test/Tools/isac/ProgLang/calculate.sml Mon Jan 27 22:26:51 2014 +0100
28.3 @@ -73,19 +73,6 @@
28.4 "----------- calculate from script ----------------------";
28.5 "----------- calculate from script ----------------------";
28.6 "----------- calculate from script ----------------------";
28.7 -store_pbt
28.8 - (prep_pbt (@{theory "Test"}) "pbl_ttest" [] e_pblID
28.9 - (["test"],
28.10 - [],
28.11 - e_rls, NONE, []));
28.12 -store_pbt
28.13 - (prep_pbt (@{theory "Test"}) "pbl_ttest_calc" [] e_pblID
28.14 - (["calculate","test"],
28.15 - [("#Given" ,["realTestGiven t_t"]),
28.16 - ("#Find" ,["realTestFind s_s"])
28.17 - ],
28.18 - e_rls, NONE, [["Test","test_calculate"]]));
28.19 -
28.20 store_met
28.21 (prep_met (@{theory "Test"}) "met_testcal" [] e_metID
28.22 (["Test","test_calculate"]:metID,