1.1 --- a/src/Tools/isac/Knowledge/AlgEin.thy Wed May 13 12:14:49 2020 +0200
1.2 +++ b/src/Tools/isac/Knowledge/AlgEin.thy Wed May 13 16:10:22 2020 +0200
1.3 @@ -24,8 +24,8 @@
1.4 \<close>
1.5 (** problems **)
1.6 setup \<open>KEStore_Elems.add_pbts
1.7 - [(Specify.prep_pbt thy "pbl_algein" [] Problem.id_empty (["Berechnung"], [], Rule_Set.empty, NONE, [])),
1.8 - (Specify.prep_pbt thy "pbl_algein_numsym" [] Problem.id_empty
1.9 + [(Problem.prep_input thy "pbl_algein" [] Problem.id_empty (["Berechnung"], [], Rule_Set.empty, NONE, [])),
1.10 + (Problem.prep_input thy "pbl_algein_numsym" [] Problem.id_empty
1.11 (["numerischSymbolische", "Berechnung"],
1.12 [("#Given",
1.13 ["KantenLaenge k_k","Querschnitt q__q"(*q_ in Biegelinie.thy*), "KantenUnten u_u",
1.14 @@ -34,12 +34,12 @@
1.15 Rule_Set.empty, NONE, [["Berechnung", "erstNumerisch"], ["Berechnung", "erstSymbolisch"]]))]\<close>
1.16
1.17 setup \<open>KEStore_Elems.add_mets
1.18 - [Specify.prep_met thy "met_algein" [] Method.id_empty
1.19 + [Method.prep_input thy "met_algein" [] Method.id_empty
1.20 (["Berechnung"], [],
1.21 {rew_ord'="tless_true", rls'= Rule_Set.Empty, calc = [], srls = Rule_Set.Empty, prls = Rule_Set.Empty, crls =Rule_Set.Empty,
1.22 errpats = [], nrls = Rule_Set.Empty},
1.23 @{thm refl}),
1.24 - Specify.prep_met thy "met_algein_numsym" [] Method.id_empty
1.25 + Method.prep_input thy "met_algein_numsym" [] Method.id_empty
1.26 (["Berechnung","erstNumerisch"], [],
1.27 {rew_ord'="tless_true", rls'= Rule_Set.Empty, calc = [], srls = Rule_Set.Empty, prls = Rule_Set.Empty, crls =Rule_Set.Empty,
1.28 errpats = [], nrls = Rule_Set.Empty},
1.29 @@ -69,7 +69,7 @@
1.30 in
1.31 Try (Rewrite_Set ''norm_Poly'') t_t)"
1.32 setup \<open>KEStore_Elems.add_mets
1.33 - [Specify.prep_met thy "met_algein_numsym_1num" [] Method.id_empty
1.34 + [Method.prep_input thy "met_algein_numsym_1num" [] Method.id_empty
1.35 (["Berechnung","erstNumerisch"],
1.36 [("#Given" ,["KantenLaenge k_k","Querschnitt q__q", "KantenUnten u_u",
1.37 "KantenSenkrecht s_s", "KantenOben o_o"]),
1.38 @@ -102,7 +102,7 @@
1.39 in
1.40 (Try (Rewrite_Set ''norm_Poly'')) t_t)"
1.41 setup \<open>KEStore_Elems.add_mets
1.42 - [Specify.prep_met thy "met_algein_symnum" [] Method.id_empty
1.43 + [Method.prep_input thy "met_algein_symnum" [] Method.id_empty
1.44 (["Berechnung","erstSymbolisch"],
1.45 [("#Given" ,["KantenLaenge k_k","Querschnitt q__q", "KantenUnten u_u",
1.46 "KantenSenkrecht s_s", "KantenOben o_o"]),
2.1 --- a/src/Tools/isac/Knowledge/Biegelinie.thy Wed May 13 12:14:49 2020 +0200
2.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy Wed May 13 16:10:22 2020 +0200
2.3 @@ -72,14 +72,14 @@
2.4
2.5 (** problems **)
2.6 setup \<open>KEStore_Elems.add_pbts
2.7 - [(Specify.prep_pbt @{theory} "pbl_bieg" [] Problem.id_empty
2.8 + [(Problem.prep_input @{theory} "pbl_bieg" [] Problem.id_empty
2.9 (["Biegelinien"],
2.10 [("#Given" ,["Traegerlaenge l_l", "Streckenlast q_q"]),
2.11 (*("#Where",["0 < l_l"]), ...wait for < and handling Arbfix*)
2.12 ("#Find" ,["Biegelinie b_b"]),
2.13 ("#Relate",["Randbedingungen r_b"])],
2.14 Rule_Set.append_rules "empty" Rule_Set.empty [], NONE, [["IntegrierenUndKonstanteBestimmen2"]])),
2.15 - (Specify.prep_pbt @{theory} "pbl_bieg_mom" [] Problem.id_empty
2.16 + (Problem.prep_input @{theory} "pbl_bieg_mom" [] Problem.id_empty
2.17 (["MomentBestimmte","Biegelinien"],
2.18 [("#Given" ,["Traegerlaenge l_l", "Streckenlast q_q"]),
2.19 (*("#Where",["0 < l_l"]), ...wait for < and handling Arbfix*)
2.20 @@ -87,26 +87,26 @@
2.21 ("#Relate",["RandbedingungenBiegung r_b","RandbedingungenMoment r_m"])
2.22 ],
2.23 Rule_Set.append_rules "empty" Rule_Set.empty [], NONE, [["IntegrierenUndKonstanteBestimmen"]])),
2.24 - (Specify.prep_pbt @{theory} "pbl_bieg_momg" [] Problem.id_empty
2.25 + (Problem.prep_input @{theory} "pbl_bieg_momg" [] Problem.id_empty
2.26 (["MomentGegebene","Biegelinien"], [], Rule_Set.append_rules "empty" Rule_Set.empty [], NONE,
2.27 [["IntegrierenUndKonstanteBestimmen","2xIntegrieren"]])),
2.28 - (Specify.prep_pbt @{theory} "pbl_bieg_einf" [] Problem.id_empty
2.29 + (Problem.prep_input @{theory} "pbl_bieg_einf" [] Problem.id_empty
2.30 (["einfache","Biegelinien"], [], Rule_Set.append_rules "empty" Rule_Set.empty [], NONE,
2.31 [["IntegrierenUndKonstanteBestimmen","4x4System"]])),
2.32 - (Specify.prep_pbt @{theory} "pbl_bieg_momquer" [] Problem.id_empty
2.33 + (Problem.prep_input @{theory} "pbl_bieg_momquer" [] Problem.id_empty
2.34 (["QuerkraftUndMomentBestimmte","Biegelinien"], [], Rule_Set.append_rules "empty" Rule_Set.empty [], NONE,
2.35 [["IntegrierenUndKonstanteBestimmen","1xIntegrieren"]])),
2.36 - (Specify.prep_pbt @{theory} "pbl_bieg_vonq" [] Problem.id_empty
2.37 + (Problem.prep_input @{theory} "pbl_bieg_vonq" [] Problem.id_empty
2.38 (["vonBelastungZu","Biegelinien"],
2.39 [("#Given" ,["Streckenlast q_q","FunktionsVariable v_v"]),
2.40 ("#Find" ,["Funktionen funs'''"])],
2.41 Rule_Set.append_rules "empty" Rule_Set.empty [], NONE, [["Biegelinien","ausBelastung"]])),
2.42 - (Specify.prep_pbt @{theory} "pbl_bieg_randbed" [] Problem.id_empty
2.43 + (Problem.prep_input @{theory} "pbl_bieg_randbed" [] Problem.id_empty
2.44 (["setzeRandbedingungen","Biegelinien"],
2.45 [("#Given" ,["Funktionen fun_s","Randbedingungen r_b"]),
2.46 ("#Find" ,["Gleichungen equs'''"])],
2.47 Rule_Set.append_rules "empty" Rule_Set.empty [], NONE, [["Biegelinien","setzeRandbedingungenEin"]])),
2.48 - (Specify.prep_pbt @{theory} "pbl_equ_fromfun" [] Problem.id_empty
2.49 + (Problem.prep_input @{theory} "pbl_equ_fromfun" [] Problem.id_empty
2.50 (["makeFunctionTo","equation"],
2.51 [("#Given" ,["functionEq fu_n","substitution su_b"]),
2.52 ("#Find" ,["equality equ'''"])],
2.53 @@ -163,7 +163,7 @@
2.54 section \<open>Methods\<close>
2.55 (* setup parent directory *)
2.56 setup \<open>KEStore_Elems.add_mets
2.57 - [Specify.prep_met @{theory} "met_biege" [] Method.id_empty
2.58 + [Method.prep_input @{theory} "met_biege" [] Method.id_empty
2.59 (["IntegrierenUndKonstanteBestimmen"], [],
2.60 {rew_ord'="tless_true", rls'= Rule_Set.Empty, calc = [], srls = Rule_Set.Empty, prls = Rule_Set.Empty, crls =Rule_Set.Empty,
2.61 errpats = [], nrls = Rule_Set.Empty},
2.62 @@ -186,7 +186,7 @@
2.63 B = ((Substitute cons) #> (Rewrite_Set_Inst [(''bdv'', v)] ''make_ratpoly_in'')) B
2.64 in B)"
2.65 setup \<open>KEStore_Elems.add_mets
2.66 - [Specify.prep_met @{theory} "met_biege_2" [] Method.id_empty
2.67 + [Method.prep_input @{theory} "met_biege_2" [] Method.id_empty
2.68 (["IntegrierenUndKonstanteBestimmen2"],
2.69 [("#Given" ,["Traegerlaenge l", "Streckenlast q",
2.70 "FunktionsVariable v", "GleichungsVariablen vs", "AbleitungBiegelinie id_abl"]),
2.71 @@ -209,22 +209,22 @@
2.72 @{thm biegelinie.simps})]
2.73 \<close>
2.74 setup \<open>KEStore_Elems.add_mets
2.75 - [Specify.prep_met @{theory} "met_biege_intconst_2" [] Method.id_empty
2.76 + [Method.prep_input @{theory} "met_biege_intconst_2" [] Method.id_empty
2.77 (["IntegrierenUndKonstanteBestimmen","2xIntegrieren"], [],
2.78 {rew_ord'="tless_true", rls'=Rule_Set.Empty, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty, crls = Atools_erls,
2.79 errpats = [], nrls = Rule_Set.empty},
2.80 @{thm refl}),
2.81 - Specify.prep_met @{theory} "met_biege_intconst_4" [] Method.id_empty
2.82 + Method.prep_input @{theory} "met_biege_intconst_4" [] Method.id_empty
2.83 (["IntegrierenUndKonstanteBestimmen","4x4System"], [],
2.84 {rew_ord'="tless_true", rls'=Rule_Set.Empty, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty, crls = Atools_erls,
2.85 errpats = [], nrls = Rule_Set.empty},
2.86 @{thm refl}),
2.87 - Specify.prep_met @{theory} "met_biege_intconst_1" [] Method.id_empty
2.88 + Method.prep_input @{theory} "met_biege_intconst_1" [] Method.id_empty
2.89 (["IntegrierenUndKonstanteBestimmen","1xIntegrieren"], [],
2.90 {rew_ord'="tless_true", rls'=Rule_Set.Empty, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty, crls = Atools_erls,
2.91 errpats = [], nrls = Rule_Set.empty},
2.92 @{thm refl}),
2.93 - Specify.prep_met @{theory} "met_biege2" [] Method.id_empty
2.94 + Method.prep_input @{theory} "met_biege2" [] Method.id_empty
2.95 (["Biegelinien"], [],
2.96 {rew_ord'="tless_true", rls'=Rule_Set.Empty, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty, crls = Atools_erls,
2.97 errpats = [], nrls = Rule_Set.empty},
2.98 @@ -254,7 +254,7 @@
2.99 in
2.100 [Q__Q, M__M, N__N, B__B])"
2.101 setup \<open>KEStore_Elems.add_mets
2.102 - [Specify.prep_met @{theory} "met_biege_ausbelast" [] Method.id_empty
2.103 + [Method.prep_input @{theory} "met_biege_ausbelast" [] Method.id_empty
2.104 (["Biegelinien", "ausBelastung"],
2.105 [("#Given" ,["Streckenlast q__q", "FunktionsVariable v_v",
2.106 "Biegelinie id_fun", "AbleitungBiegelinie id_abl"]),
2.107 @@ -295,7 +295,7 @@
2.108 in
2.109 [e_1, e_2, e_3, e_4])"
2.110 setup \<open>KEStore_Elems.add_mets
2.111 - [Specify.prep_met @{theory} "met_biege_setzrand" [] Method.id_empty
2.112 + [Method.prep_input @{theory} "met_biege_setzrand" [] Method.id_empty
2.113 (["Biegelinien", "setzeRandbedingungenEin"],
2.114 [("#Given" , ["Funktionen fun_s", "Randbedingungen r_b"]),
2.115 ("#Find" , ["Gleichungen equs'''"])],
2.116 @@ -319,7 +319,7 @@
2.117 in
2.118 (Rewrite_Set ''norm_Rational'') eq_u)"
2.119 setup \<open>KEStore_Elems.add_mets
2.120 - [Specify.prep_met @{theory} "met_equ_fromfun" [] Method.id_empty
2.121 + [Method.prep_input @{theory} "met_equ_fromfun" [] Method.id_empty
2.122 (["Equation","fromFunction"],
2.123 [("#Given" ,["functionEq fu_n","substitution su_b"]),
2.124 ("#Find" ,["equality equ'''"])],
3.1 --- a/src/Tools/isac/Knowledge/Diff.thy Wed May 13 12:14:49 2020 +0200
3.2 +++ b/src/Tools/isac/Knowledge/Diff.thy Wed May 13 16:10:22 2020 +0200
3.3 @@ -239,8 +239,8 @@
3.4
3.5 (** problem types **)
3.6 setup \<open>KEStore_Elems.add_pbts
3.7 - [(Specify.prep_pbt thy "pbl_fun" [] Problem.id_empty (["function"], [], Rule_Set.empty, NONE, [])),
3.8 - (Specify.prep_pbt thy "pbl_fun_deriv" [] Problem.id_empty
3.9 + [(Problem.prep_input thy "pbl_fun" [] Problem.id_empty (["function"], [], Rule_Set.empty, NONE, [])),
3.10 + (Problem.prep_input thy "pbl_fun_deriv" [] Problem.id_empty
3.11 (["derivative_of","function"],
3.12 [("#Given" ,["functionTerm f_f","differentiateFor v_v"]),
3.13 ("#Find" ,["derivative f_f'"])],
3.14 @@ -248,7 +248,7 @@
3.15 SOME "Diff (f_f, v_v)", [["diff","differentiate_on_R"],
3.16 ["diff","after_simplification"]])),
3.17 (*here "named" is used differently from Integration"*)
3.18 - (Specify.prep_pbt thy "pbl_fun_deriv_nam" [] Problem.id_empty
3.19 + (Problem.prep_input thy "pbl_fun_deriv_nam" [] Problem.id_empty
3.20 (["named","derivative_of","function"],
3.21 [("#Given" ,["functionEq f_f","differentiateFor v_v"]),
3.22 ("#Find" ,["derivativeEq f_f'"])],
3.23 @@ -272,7 +272,7 @@
3.24 | argl2dtss _ = raise ERROR "Diff.ML: wrong argument for argl2dtss";
3.25 \<close>
3.26 setup \<open>KEStore_Elems.add_mets
3.27 - [Specify.prep_met thy "met_diff" [] Method.id_empty
3.28 + [Method.prep_input thy "met_diff" [] Method.id_empty
3.29 (["diff"], [],
3.30 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
3.31 crls = Atools_erls, errpats = [], nrls = norm_diff},
3.32 @@ -307,7 +307,7 @@
3.33 Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''diff_sym_conv''))
3.34 ) f_f')"
3.35 setup \<open>KEStore_Elems.add_mets
3.36 - [Specify.prep_met thy "met_diff_onR" [] Method.id_empty
3.37 + [Method.prep_input thy "met_diff_onR" [] Method.id_empty
3.38 (["diff","differentiate_on_R"],
3.39 [("#Given" ,["functionTerm f_f","differentiateFor v_v"]),
3.40 ("#Find" ,["derivative f_f'"])],
3.41 @@ -342,7 +342,7 @@
3.42 (Repeat (Rewrite_Set ''make_polynomial'')))
3.43 ) f_f')"
3.44 setup \<open>KEStore_Elems.add_mets
3.45 - [Specify.prep_met thy "met_diff_simpl" [] Method.id_empty
3.46 + [Method.prep_input thy "met_diff_simpl" [] Method.id_empty
3.47 (["diff","diff_simpl"],
3.48 [("#Given", ["functionTerm f_f","differentiateFor v_v"]),
3.49 ("#Find" , ["derivative f_f'"])],
3.50 @@ -380,7 +380,7 @@
3.51 Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''diff_sym_conv'' ))
3.52 ) f_f')"
3.53 setup \<open>KEStore_Elems.add_mets
3.54 - [Specify.prep_met thy "met_diff_equ" [] Method.id_empty
3.55 + [Method.prep_input thy "met_diff_equ" [] Method.id_empty
3.56 (["diff","differentiate_equality"],
3.57 [("#Given" ,["functionEq f_f","differentiateFor v_v"]),
3.58 ("#Find" ,["derivativeEq f_f'"])],
3.59 @@ -403,7 +403,7 @@
3.60 ) term')"
3.61
3.62 setup \<open>KEStore_Elems.add_mets
3.63 - [Specify.prep_met thy "met_diff_after_simp" [] Method.id_empty
3.64 + [Method.prep_input thy "met_diff_after_simp" [] Method.id_empty
3.65 (["diff","after_simplification"],
3.66 [("#Given" ,["functionTerm term","differentiateFor bound_variable"]),
3.67 ("#Find" ,["derivative term'"])],
4.1 --- a/src/Tools/isac/Knowledge/DiffApp.thy Wed May 13 12:14:49 2020 +0200
4.2 +++ b/src/Tools/isac/Knowledge/DiffApp.thy Wed May 13 16:10:22 2020 +0200
4.3 @@ -63,37 +63,37 @@
4.4
4.5 (** problem types **)
4.6 setup \<open>KEStore_Elems.add_pbts
4.7 - [(Specify.prep_pbt thy "pbl_fun_max" [] Problem.id_empty
4.8 + [(Problem.prep_input thy "pbl_fun_max" [] Problem.id_empty
4.9 (["maximum_of","function"],
4.10 [("#Given" ,["fixedValues f_ix"]),
4.11 ("#Find" ,["maximum m_m","valuesFor v_s"]),
4.12 ("#Relate",["relations r_s"])],
4.13 Rule_Set.empty, NONE, [])),
4.14 - (Specify.prep_pbt thy "pbl_fun_make" [] Problem.id_empty
4.15 + (Problem.prep_input thy "pbl_fun_make" [] Problem.id_empty
4.16 (["make","function"],
4.17 [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]),
4.18 ("#Find" ,["functionEq f_1"])],
4.19 Rule_Set.empty, NONE, [])),
4.20 - (Specify.prep_pbt thy "pbl_fun_max_expl" [] Problem.id_empty
4.21 + (Problem.prep_input thy "pbl_fun_max_expl" [] Problem.id_empty
4.22 (["by_explicit","make","function"],
4.23 [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]),
4.24 ("#Find" ,["functionEq f_1"])],
4.25 Rule_Set.empty, NONE, [["DiffApp","make_fun_by_explicit"]])),
4.26 - (Specify.prep_pbt thy "pbl_fun_max_newvar" [] Problem.id_empty
4.27 + (Problem.prep_input thy "pbl_fun_max_newvar" [] Problem.id_empty
4.28 (["by_new_variable","make","function"],
4.29 [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]),
4.30 (*WN.12.5.03: precond for distinction still missing*)
4.31 ("#Find" ,["functionEq f_1"])],
4.32 Rule_Set.empty, NONE, [["DiffApp","make_fun_by_new_variable"]])),
4.33 - (Specify.prep_pbt thy "pbl_fun_max_interv" [] Problem.id_empty
4.34 + (Problem.prep_input thy "pbl_fun_max_interv" [] Problem.id_empty
4.35 (["on_interval","maximum_of","function"],
4.36 [("#Given" ,["functionEq t_t","boundVariable v_v","interval i_tv"]),
4.37 (*WN.12.5.03: precond for distinction still missing*)
4.38 ("#Find" ,["maxArgument v_0"])],
4.39 Rule_Set.empty, NONE, [])),
4.40 - (Specify.prep_pbt thy "pbl_tool" [] Problem.id_empty
4.41 + (Problem.prep_input thy "pbl_tool" [] Problem.id_empty
4.42 (["tool"], [], Rule_Set.empty, NONE, [])),
4.43 - (Specify.prep_pbt thy "pbl_tool_findvals" [] Problem.id_empty
4.44 + (Problem.prep_input thy "pbl_tool_findvals" [] Problem.id_empty
4.45 (["find_values","tool"],
4.46 [("#Given" ,["maxArgument m_ax","functionEq f_f","boundVariable v_v"]),
4.47 ("#Find" ,["valuesFor v_ls"]),
4.48 @@ -103,7 +103,7 @@
4.49
4.50 (** methods, scripts not yet implemented **)
4.51 setup \<open>KEStore_Elems.add_mets
4.52 - [Specify.prep_met thy "met_diffapp" [] Method.id_empty
4.53 + [Method.prep_input thy "met_diffapp" [] Method.id_empty
4.54 (["DiffApp"], [],
4.55 {rew_ord'="tless_true", rls'=Atools_erls,calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty,
4.56 crls = Atools_erls, errpats = [], nrls = norm_Rational (*, asm_rls=[],asm_thm=[]*)},
4.57 @@ -125,7 +125,7 @@
4.58 in SubProblem (''DiffApp'',[''find_values'', ''tool''], [''Isac_Knowledge'', ''find_values''])
4.59 [REAL m_x, REAL (rhs t_t), REAL v_v, REAL m_m, BOOL_LIST (dropWhile (ident e_e) r_s)])"
4.60 setup \<open>KEStore_Elems.add_mets
4.61 - [Specify.prep_met thy "met_diffapp_max" [] Method.id_empty
4.62 + [Method.prep_input thy "met_diffapp_max" [] Method.id_empty
4.63 (["DiffApp","max_by_calculus"],
4.64 [("#Given" ,["fixedValues f_ix","maximum m_m","relations r_s", "boundVariable v_v",
4.65 "interval i_tv","errorBound e_rr"]),
4.66 @@ -152,7 +152,7 @@
4.67 [BOOL e_2, REAL v_2]
4.68 in Substitute [(v_1 = (rhs o hd) s_1), (v_2 = (rhs o hd) s_2)] h_h)"
4.69 setup \<open>KEStore_Elems.add_mets
4.70 - [Specify.prep_met thy "met_diffapp_funnew" [] Method.id_empty
4.71 + [Method.prep_input thy "met_diffapp_funnew" [] Method.id_empty
4.72 (["DiffApp","make_fun_by_new_variable"],
4.73 [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]),
4.74 ("#Find" ,["functionEq f_1"])],
4.75 @@ -172,7 +172,7 @@
4.76 [BOOL e_1, REAL v_1]
4.77 in Substitute [(v_1 = (rhs o hd) s_1)] h_h) "
4.78 setup \<open>KEStore_Elems.add_mets
4.79 - [Specify.prep_met thy "met_diffapp_funexp" [] Method.id_empty
4.80 + [Method.prep_input thy "met_diffapp_funexp" [] Method.id_empty
4.81 (["DiffApp","make_fun_by_explicit"],
4.82 [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]),
4.83 ("#Find" ,["functionEq f_1"])],
4.84 @@ -181,14 +181,14 @@
4.85 @{thm make_fun_by_explicit.simps})]
4.86 \<close>
4.87 setup \<open>KEStore_Elems.add_mets
4.88 - [Specify.prep_met thy "met_diffapp_max_oninterval" [] Method.id_empty
4.89 + [Method.prep_input thy "met_diffapp_max_oninterval" [] Method.id_empty
4.90 (["DiffApp","max_on_interval_by_calculus"],
4.91 [("#Given" ,["functionEq t_t","boundVariable v_v","interval i_tv"(*, "errorBound e_rr"*)]),
4.92 ("#Find" ,["maxArgument v_0"])],
4.93 {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls = Rule_Set.empty,prls=Rule_Set.empty, crls = eval_rls,
4.94 errpats = [], nrls = norm_Rational (*, asm_rls=[],asm_thm=[]*)},
4.95 @{thm refl}),
4.96 - Specify.prep_met thy "met_diffapp_findvals" [] Method.id_empty
4.97 + Method.prep_input thy "met_diffapp_findvals" [] Method.id_empty
4.98 (["DiffApp","find_values"], [],
4.99 {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls = Rule_Set.empty,prls=Rule_Set.empty, crls = eval_rls,
4.100 errpats = [], nrls = norm_Rational(*, asm_rls = [], asm_thm = []*)},
5.1 --- a/src/Tools/isac/Knowledge/DiophantEq.thy Wed May 13 12:14:49 2020 +0200
5.2 +++ b/src/Tools/isac/Knowledge/DiophantEq.thy Wed May 13 16:10:22 2020 +0200
5.3 @@ -15,7 +15,7 @@
5.4
5.5 text \<open>problemclass for the usecase\<close>
5.6 setup \<open>KEStore_Elems.add_pbts
5.7 - [(Specify.prep_pbt thy "pbl_equ_dio" [] Problem.id_empty
5.8 + [(Problem.prep_input thy "pbl_equ_dio" [] Problem.id_empty
5.9 (["diophantine","equation"],
5.10 [("#Given" ,["boolTestGiven e_e","intTestGiven (v_v::int)"]),
5.11 (* TODO: drop ^^^^^*)
5.12 @@ -33,7 +33,7 @@
5.13 (Try (Calculate ''PLUS'')) #>
5.14 (Try (Calculate ''TIMES''))) e_e)"
5.15 setup \<open>KEStore_Elems.add_mets
5.16 - [Specify.prep_met thy "met_test_diophant" [] Method.id_empty
5.17 + [Method.prep_input thy "met_test_diophant" [] Method.id_empty
5.18 (["Test","solve_diophant"],
5.19 [("#Given" ,["boolTestGiven e_e","intTestGiven (v_v::int)"]),
5.20 (* TODO: drop ^^^^^*)
6.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Wed May 13 12:14:49 2020 +0200
6.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Wed May 13 16:10:22 2020 +0200
6.3 @@ -406,18 +406,18 @@
6.4
6.5 (** problems **)
6.6 setup \<open>KEStore_Elems.add_pbts
6.7 - [(Specify.prep_pbt thy "pbl_equsys" [] Problem.id_empty
6.8 + [(Problem.prep_input thy "pbl_equsys" [] Problem.id_empty
6.9 (["system"],
6.10 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
6.11 ("#Find" ,["solution ss'''"](*''' is copy-named*))],
6.12 Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)], SOME "solveSystem e_s v_s", [])),
6.13 - (Specify.prep_pbt thy "pbl_equsys_lin" [] Problem.id_empty
6.14 + (Problem.prep_input thy "pbl_equsys_lin" [] Problem.id_empty
6.15 (["LINEAR", "system"],
6.16 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
6.17 (*TODO.WN050929 check linearity*)
6.18 ("#Find" ,["solution ss'''"])],
6.19 Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)], SOME "solveSystem e_s v_s", [])),
6.20 - (Specify.prep_pbt thy "pbl_equsys_lin_2x2" [] Problem.id_empty
6.21 + (Problem.prep_input thy "pbl_equsys_lin_2x2" [] Problem.id_empty
6.22 (["2x2", "LINEAR", "system"],
6.23 (*~~~~~~~~~~~~~~~~~~~~~~~~~*)
6.24 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
6.25 @@ -429,7 +429,7 @@
6.26 Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
6.27 Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_")],
6.28 SOME "solveSystem e_s v_s", [])),
6.29 - (Specify.prep_pbt thy "pbl_equsys_lin_2x2_tri" [] Problem.id_empty
6.30 + (Problem.prep_input thy "pbl_equsys_lin_2x2_tri" [] Problem.id_empty
6.31 (["triangular", "2x2", "LINEAR", "system"],
6.32 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
6.33 ("#Where",
6.34 @@ -437,14 +437,14 @@
6.35 " v_s from v_s occur_exactly_in (NTH 2 (e_s::bool list))"]),
6.36 ("#Find" ,["solution ss'''"])],
6.37 prls_triangular, SOME "solveSystem e_s v_s", [["EqSystem","top_down_substitution","2x2"]])),
6.38 - (Specify.prep_pbt thy "pbl_equsys_lin_2x2_norm" [] Problem.id_empty
6.39 + (Problem.prep_input thy "pbl_equsys_lin_2x2_norm" [] Problem.id_empty
6.40 (["normalise", "2x2", "LINEAR", "system"],
6.41 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
6.42 ("#Find" ,["solution ss'''"])],
6.43 Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)],
6.44 SOME "solveSystem e_s v_s",
6.45 [["EqSystem","normalise","2x2"]])),
6.46 - (Specify.prep_pbt thy "pbl_equsys_lin_3x3" [] Problem.id_empty
6.47 + (Problem.prep_input thy "pbl_equsys_lin_3x3" [] Problem.id_empty
6.48 (["3x3", "LINEAR", "system"],
6.49 (*~~~~~~~~~~~~~~~~~~~~~~~~~*)
6.50 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
6.51 @@ -456,7 +456,7 @@
6.52 Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
6.53 Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_")],
6.54 SOME "solveSystem e_s v_s", [])),
6.55 - (Specify.prep_pbt thy "pbl_equsys_lin_4x4" [] Problem.id_empty
6.56 + (Problem.prep_input thy "pbl_equsys_lin_4x4" [] Problem.id_empty
6.57 (["4x4", "LINEAR", "system"],
6.58 (*~~~~~~~~~~~~~~~~~~~~~~~~~*)
6.59 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
6.60 @@ -468,7 +468,7 @@
6.61 Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
6.62 Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_")],
6.63 SOME "solveSystem e_s v_s", [])),
6.64 - (Specify.prep_pbt thy "pbl_equsys_lin_4x4_tri" [] Problem.id_empty
6.65 + (Problem.prep_input thy "pbl_equsys_lin_4x4_tri" [] Problem.id_empty
6.66 (["triangular", "4x4", "LINEAR", "system"],
6.67 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
6.68 ("#Where" , (*accepts missing variables up to diagional form*)
6.69 @@ -481,7 +481,7 @@
6.70 [Rule.Eval ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in "")],
6.71 SOME "solveSystem e_s v_s",
6.72 [["EqSystem","top_down_substitution","4x4"]])),
6.73 - (Specify.prep_pbt thy "pbl_equsys_lin_4x4_norm" [] Problem.id_empty
6.74 + (Problem.prep_input thy "pbl_equsys_lin_4x4_norm" [] Problem.id_empty
6.75 (["normalise", "4x4", "LINEAR", "system"],
6.76 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
6.77 (*LENGTH is checked 1 level above*)
6.78 @@ -510,12 +510,12 @@
6.79
6.80 (**methods**)
6.81 setup \<open>KEStore_Elems.add_mets
6.82 - [Specify.prep_met thy "met_eqsys" [] Method.id_empty
6.83 + [Method.prep_input thy "met_eqsys" [] Method.id_empty
6.84 (["EqSystem"], [],
6.85 {rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [], srls = Rule_Set.Empty, prls = Rule_Set.Empty, crls = Rule_Set.Empty,
6.86 errpats = [], nrls = Rule_Set.Empty},
6.87 @{thm refl}),
6.88 - Specify.prep_met thy "met_eqsys_topdown" [] Method.id_empty
6.89 + Method.prep_input thy "met_eqsys_topdown" [] Method.id_empty
6.90 (["EqSystem","top_down_substitution"], [],
6.91 {rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [], srls = Rule_Set.Empty, prls = Rule_Set.Empty, crls = Rule_Set.Empty,
6.92 errpats = [], nrls = Rule_Set.Empty},
6.93 @@ -542,7 +542,7 @@
6.94 in
6.95 Try (Rewrite_Set ''order_system'' ) e__s) "
6.96 setup \<open>KEStore_Elems.add_mets
6.97 - [Specify.prep_met thy "met_eqsys_topdown_2x2" [] Method.id_empty
6.98 + [Method.prep_input thy "met_eqsys_topdown_2x2" [] Method.id_empty
6.99 (["EqSystem", "top_down_substitution", "2x2"],
6.100 [("#Given", ["equalities e_s", "solveForVars v_s"]),
6.101 ("#Where",
6.102 @@ -558,7 +558,7 @@
6.103 @{thm solve_system.simps})]
6.104 \<close>
6.105 setup \<open>KEStore_Elems.add_mets
6.106 - [Specify.prep_met thy "met_eqsys_norm" [] Method.id_empty
6.107 + [Method.prep_input thy "met_eqsys_norm" [] Method.id_empty
6.108 (["EqSystem", "normalise"], [],
6.109 {rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [], srls = Rule_Set.Empty, prls = Rule_Set.Empty, crls = Rule_Set.Empty,
6.110 errpats = [], nrls = Rule_Set.Empty},
6.111 @@ -580,7 +580,7 @@
6.112 SubProblem (''EqSystem'', [''LINEAR'', ''system''], [''no_met''])
6.113 [BOOL_LIST e__s, REAL_LIST v_s])"
6.114 setup \<open>KEStore_Elems.add_mets
6.115 - [Specify.prep_met thy "met_eqsys_norm_2x2" [] Method.id_empty
6.116 + [Method.prep_input thy "met_eqsys_norm_2x2" [] Method.id_empty
6.117 (["EqSystem","normalise","2x2"],
6.118 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
6.119 ("#Find" ,["solution ss'''"])],
6.120 @@ -612,7 +612,7 @@
6.121 SubProblem (''EqSystem'', [''LINEAR'', ''system''], [''no_met''])
6.122 [BOOL_LIST e__s, REAL_LIST v_s])"
6.123 setup \<open>KEStore_Elems.add_mets
6.124 - [Specify.prep_met thy "met_eqsys_norm_4x4" [] Method.id_empty
6.125 + [Method.prep_input thy "met_eqsys_norm_4x4" [] Method.id_empty
6.126 (["EqSystem","normalise","4x4"],
6.127 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
6.128 ("#Find" ,["solution ss'''"])],
6.129 @@ -644,7 +644,7 @@
6.130 in
6.131 [e_1, e_2, NTH 3 e_s, NTH 4 e_s])"
6.132 setup \<open>KEStore_Elems.add_mets
6.133 - [Specify.prep_met thy "met_eqsys_topdown_4x4" [] Method.id_empty
6.134 + [Method.prep_input thy "met_eqsys_topdown_4x4" [] Method.id_empty
6.135 (["EqSystem","top_down_substitution","4x4"],
6.136 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
6.137 ("#Where" , (*accepts missing variables up to diagonal form*)
7.1 --- a/src/Tools/isac/Knowledge/Equation.thy Wed May 13 12:14:49 2020 +0200
7.2 +++ b/src/Tools/isac/Knowledge/Equation.thy Wed May 13 16:10:22 2020 +0200
7.3 @@ -43,14 +43,14 @@
7.4 setup \<open>KEStore_Elems.add_rlss [("univariate_equation_prls",
7.5 (Context.theory_name @{theory}, Auto_Prog.prep_rls @{theory} univariate_equation_prls))]\<close>
7.6 setup \<open>KEStore_Elems.add_pbts
7.7 - [(Specify.prep_pbt thy "pbl_equ" [] Problem.id_empty
7.8 + [(Problem.prep_input thy "pbl_equ" [] Problem.id_empty
7.9 (["equation"],
7.10 [("#Given" ,["equality e_e","solveFor v_v"]),
7.11 ("#Where" ,["matches (?a = ?b) e_e"]),
7.12 ("#Find" ,["solutions v_v'i'"])],
7.13 Rule_Set.append_rules "equation_prls" Rule_Set.empty [Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches "")],
7.14 SOME "solve (e_e::bool, v_v)", [])),
7.15 - (Specify.prep_pbt thy "pbl_equ_univ" [] Problem.id_empty
7.16 + (Problem.prep_input thy "pbl_equ_univ" [] Problem.id_empty
7.17 (["univariate","equation"],
7.18 [("#Given" ,["equality e_e","solveFor v_v"]),
7.19 ("#Where" ,["matches (?a = ?b) e_e"]),
7.20 @@ -81,7 +81,7 @@
7.21
7.22
7.23 setup \<open>KEStore_Elems.add_mets
7.24 - [Specify.prep_met thy "met_equ" [] Method.id_empty
7.25 + [Method.prep_input thy "met_equ" [] Method.id_empty
7.26 (["Equation"], [],
7.27 {rew_ord'="tless_true", rls'=Rule_Set.Empty, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty, crls = Atools_erls,
7.28 errpats = [], nrls = Rule_Set.empty},
8.1 --- a/src/Tools/isac/Knowledge/InsSort.thy Wed May 13 12:14:49 2020 +0200
8.2 +++ b/src/Tools/isac/Knowledge/InsSort.thy Wed May 13 16:10:22 2020 +0200
8.3 @@ -72,11 +72,11 @@
8.4
8.5 section \<open>problems\<close>
8.6 setup \<open>KEStore_Elems.add_pbts
8.7 - [(Specify.prep_pbt @{theory} "pbl_Programming" [] Problem.id_empty
8.8 + [(Problem.prep_input @{theory} "pbl_Programming" [] Problem.id_empty
8.9 (["Programming"], [], Rule_Set.empty, NONE, [])),
8.10 - (Specify.prep_pbt @{theory} "pbl_Prog_sort" [] Problem.id_empty
8.11 + (Problem.prep_input @{theory} "pbl_Prog_sort" [] Problem.id_empty
8.12 (["SORT","Programming"], [], Rule_Set.empty, NONE, [])),
8.13 - (Specify.prep_pbt @{theory} "pbl_Prog_sort_ins" [] Problem.id_empty
8.14 + (Problem.prep_input @{theory} "pbl_Prog_sort_ins" [] Problem.id_empty
8.15 (["insertion","SORT","Programming"],
8.16 [("#Given", ["unsorted u_u"]), ("#Find", ["sorted s_s"])],
8.17 Rule_Set.empty,
8.18 @@ -85,11 +85,11 @@
8.19 section \<open>methods\<close>
8.20 (* TODO: implementation needs extra object-level lists ?!?*)
8.21 setup \<open>KEStore_Elems.add_mets
8.22 - [ Specify.prep_met @{theory} "met_Programming" [] Method.id_empty
8.23 + [ Method.prep_input @{theory} "met_Programming" [] Method.id_empty
8.24 (["Programming"], [],
8.25 {rew_ord'="tless_true",rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty,
8.26 crls = Rule_Set.empty, errpats = [], nrls = Rule_Set.empty}, @{thm refl}),
8.27 - Specify.prep_met @{theory} "met_Prog_sort" [] Method.id_empty
8.28 + Method.prep_input @{theory} "met_Prog_sort" [] Method.id_empty
8.29 (["Programming","SORT"], [],
8.30 {rew_ord'="tless_true",rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty,
8.31 crls = Rule_Set.empty, errpats = [], nrls = Rule_Set.empty},
8.32 @@ -104,7 +104,7 @@
8.33 in
8.34 (Rewrite_Set ''ins_sort'') uns)"
8.35 setup \<open>KEStore_Elems.add_mets
8.36 - [Specify.prep_met @{theory} "met_Prog_sort_ins" [] Method.id_empty
8.37 + [Method.prep_input @{theory} "met_Prog_sort_ins" [] Method.id_empty
8.38 (["Programming","SORT","insertion"],
8.39 [("#Given", ["unsorted u_u"]), ("#Find", ["sorted s_s"])],
8.40 {rew_ord'="tless_true",rls' = Atools_erls, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty,
8.41 @@ -134,7 +134,7 @@
8.42 (Repeat (Rewrite ''if_False'')))
8.43 ) uns)"
8.44 setup \<open>KEStore_Elems.add_mets
8.45 - [Specify.prep_met @{theory} "met_Prog_sort_ins_steps" [] Method.id_empty
8.46 + [Method.prep_input @{theory} "met_Prog_sort_ins_steps" [] Method.id_empty
8.47 (["Programming","SORT","insertion_steps"],
8.48 [("#Given", ["unsorted u_u"]), ("#Find", ["sorted s_s"])],
8.49 {rew_ord'="tless_true",rls' = Atools_erls, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty,
9.1 --- a/src/Tools/isac/Knowledge/Integrate.thy Wed May 13 12:14:49 2020 +0200
9.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy Wed May 13 16:10:22 2020 +0200
9.3 @@ -331,7 +331,7 @@
9.4
9.5 (** problems **)
9.6 setup \<open>KEStore_Elems.add_pbts
9.7 - [(Specify.prep_pbt thy "pbl_fun_integ" [] Problem.id_empty
9.8 + [(Problem.prep_input thy "pbl_fun_integ" [] Problem.id_empty
9.9 (["integrate","function"],
9.10 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
9.11 ("#Find" ,["antiDerivative F_F"])],
9.12 @@ -339,7 +339,7 @@
9.13 SOME "Integrate (f_f, v_v)",
9.14 [["diff","integration"]])),
9.15 (*here "named" is used differently from Differentiation"*)
9.16 - (Specify.prep_pbt thy "pbl_fun_integ_nam" [] Problem.id_empty
9.17 + (Problem.prep_input thy "pbl_fun_integ_nam" [] Problem.id_empty
9.18 (["named","integrate","function"],
9.19 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
9.20 ("#Find" ,["antiDerivativeName F_F"])],
9.21 @@ -357,7 +357,7 @@
9.22 in
9.23 (Rewrite_Set_Inst [(''bdv'', v_v)] ''integration'') t_t)"
9.24 setup \<open>KEStore_Elems.add_mets
9.25 - [Specify.prep_met thy "met_diffint" [] Method.id_empty
9.26 + [Method.prep_input thy "met_diffint" [] Method.id_empty
9.27 (["diff","integration"],
9.28 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]), ("#Find" ,["antiDerivative F_F"])],
9.29 {rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
9.30 @@ -375,7 +375,7 @@
9.31 (Rewrite_Set_Inst [(''bdv'', v_v)] ''integration'')
9.32 ) t_t)"
9.33 setup \<open>KEStore_Elems.add_mets
9.34 - [Specify.prep_met thy "met_diffint_named" [] Method.id_empty
9.35 + [Method.prep_input thy "met_diffint_named" [] Method.id_empty
9.36 (["diff","integration","named"],
9.37 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
9.38 ("#Find" ,["antiDerivativeName F_F"])],
10.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Wed May 13 12:14:49 2020 +0200
10.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Wed May 13 16:10:22 2020 +0200
10.3 @@ -46,10 +46,10 @@
10.4 val thy = @{theory};
10.5 \<close>
10.6 setup \<open>KEStore_Elems.add_pbts
10.7 - [(Specify.prep_pbt thy "pbl_SP" [] Problem.id_empty (["SignalProcessing"], [], Rule_Set.empty, NONE, [])),
10.8 - (Specify.prep_pbt thy "pbl_SP_Ztrans" [] Problem.id_empty
10.9 + [(Problem.prep_input thy "pbl_SP" [] Problem.id_empty (["SignalProcessing"], [], Rule_Set.empty, NONE, [])),
10.10 + (Problem.prep_input thy "pbl_SP_Ztrans" [] Problem.id_empty
10.11 (["Z_Transform","SignalProcessing"], [], Rule_Set.empty, NONE, [])),
10.12 - (Specify.prep_pbt thy "pbl_SP_Ztrans_inv" [] Problem.id_empty
10.13 + (Problem.prep_input thy "pbl_SP_Ztrans_inv" [] Problem.id_empty
10.14 (["Inverse", "Z_Transform", "SignalProcessing"],
10.15 [("#Given" , ["filterExpression X_eq"]),
10.16 ("#Find" ,["stepResponse n_eq"])], \<comment> \<open>TODO: unused, "u [n]" is introduced by rule1..6\<close>
10.17 @@ -59,11 +59,11 @@
10.18 subsection \<open>Setup Parent Nodes in Hierarchy of Method\<close>
10.19 ML \<open>val thy = @{theory}; (*latest version of thy required*)\<close>
10.20 setup \<open>KEStore_Elems.add_mets
10.21 - [Specify.prep_met thy "met_SP" [] Method.id_empty
10.22 + [Method.prep_input thy "met_SP" [] Method.id_empty
10.23 (["SignalProcessing"], [],
10.24 {rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty, crls = Rule_Set.empty,
10.25 errpats = [], nrls = Rule_Set.empty}, @{thm refl}),
10.26 - Specify.prep_met thy "met_SP_Ztrans" [] Method.id_empty
10.27 + Method.prep_input thy "met_SP_Ztrans" [] Method.id_empty
10.28 (["SignalProcessing", "Z_Transform"], [],
10.29 {rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty, crls = Rule_Set.empty,
10.30 errpats = [], nrls = Rule_Set.empty}, @{thm refl})]
10.31 @@ -87,7 +87,7 @@
10.32 [BOOL equ, REAL X_z]
10.33 in X) "
10.34 setup \<open>KEStore_Elems.add_mets
10.35 - [Specify.prep_met thy "met_SP_Ztrans_inv" [] Method.id_empty
10.36 + [Method.prep_input thy "met_SP_Ztrans_inv" [] Method.id_empty
10.37 (["SignalProcessing", "Z_Transform", "Inverse"],
10.38 [("#Given" ,["filterExpression X_eq", "functionName X_z"]),
10.39 ("#Find" ,["stepResponse n_eq"])], \<comment> \<open>TODO: unused, "u [n]" is introduced by rule1..6\<close>
10.40 @@ -115,7 +115,7 @@
10.41 n_eq = (Rewrite_Set ''inverse_z'' ) X_zeq
10.42 in n_eq)"
10.43 setup \<open>KEStore_Elems.add_mets
10.44 - [Specify.prep_met thy "met_SP_Ztrans_inv_sub" [] Method.id_empty
10.45 + [Method.prep_input thy "met_SP_Ztrans_inv_sub" [] Method.id_empty
10.46 (["SignalProcessing", "Z_Transform", "Inverse_sub"],
10.47 [("#Given" ,["filterExpression X_eq", "functionName X_z"]),
10.48 ("#Find" ,["stepResponse n_eq"])], \<comment> \<open>TODO: unused, "u [n]" is introduced by rule1..6\<close>
11.1 --- a/src/Tools/isac/Knowledge/LinEq.thy Wed May 13 12:14:49 2020 +0200
11.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy Wed May 13 16:10:22 2020 +0200
11.3 @@ -114,7 +114,7 @@
11.4 (*----------------------------- problem types --------------------------------*)
11.5 (* ---------linear----------- *)
11.6 setup \<open>KEStore_Elems.add_pbts
11.7 - [(Specify.prep_pbt thy "pbl_equ_univ_lin" [] Problem.id_empty
11.8 + [(Problem.prep_input thy "pbl_equ_univ_lin" [] Problem.id_empty
11.9 (["LINEAR", "univariate", "equation"],
11.10 [("#Given" ,["equality e_e", "solveFor v_v"]),
11.11 ("#Where" ,["HOL.False", (*WN0509 just detected: this pbl can never be used?!?*)
11.12 @@ -127,7 +127,7 @@
11.13
11.14 (*-------------- methods------------------------------------------------------*)
11.15 setup \<open>KEStore_Elems.add_mets
11.16 - [Specify.prep_met thy "met_eqlin" [] Method.id_empty
11.17 + [Method.prep_input thy "met_eqlin" [] Method.id_empty
11.18 (["LinEq"], [],
11.19 {rew_ord' = "tless_true",rls' = Atools_erls,calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty,
11.20 crls = LinEq_crls, errpats = [], nrls = norm_Poly},
11.21 @@ -151,7 +151,7 @@
11.22 in
11.23 Or_to_List e_e)"
11.24 setup \<open>KEStore_Elems.add_mets
11.25 - [Specify.prep_met thy "met_eq_lin" [] Method.id_empty
11.26 + [Method.prep_input thy "met_eq_lin" [] Method.id_empty
11.27 (["LinEq","solve_lineq_equation"],
11.28 [("#Given", ["equality e_e", "solveFor v_v"]),
11.29 ("#Where", ["Not ((lhs e_e) is_polyrat_in v_v)", "((lhs e_e) has_degree_in v_v) = 1"]),
12.1 --- a/src/Tools/isac/Knowledge/LogExp.thy Wed May 13 12:14:49 2020 +0200
12.2 +++ b/src/Tools/isac/Knowledge/LogExp.thy Wed May 13 16:10:22 2020 +0200
12.3 @@ -22,7 +22,7 @@
12.4 \<close>
12.5 (** problems **)
12.6 setup \<open>KEStore_Elems.add_pbts
12.7 - [(Specify.prep_pbt thy "pbl_test_equ_univ_log" [] Problem.id_empty
12.8 + [(Problem.prep_input thy "pbl_test_equ_univ_log" [] Problem.id_empty
12.9 (["logarithmic","univariate","equation"],
12.10 [("#Given",["equality e_e","solveFor v_v"]),
12.11 ("#Where",["matches ((?a log ?v_v) = ?b) e_e"]),
12.12 @@ -44,7 +44,7 @@
12.13 in
12.14 [e_e])"
12.15 setup \<open>KEStore_Elems.add_mets
12.16 - [Specify.prep_met thy "met_equ_log" [] Method.id_empty
12.17 + [Method.prep_input thy "met_equ_log" [] Method.id_empty
12.18 (["Equation","solve_log"],
12.19 [("#Given" ,["equality e_e","solveFor v_v"]),
12.20 ("#Where" ,["matches ((?a log ?v_v) = ?b) e_e"]),
13.1 --- a/src/Tools/isac/Knowledge/Partial_Fractions.thy Wed May 13 12:14:49 2020 +0200
13.2 +++ b/src/Tools/isac/Knowledge/Partial_Fractions.thy Wed May 13 16:10:22 2020 +0200
13.3 @@ -148,7 +148,7 @@
13.4 Check_Unique.on := false; (*WN120307 REMOVE after editing*)
13.5 \<close>
13.6 setup \<open>KEStore_Elems.add_pbts
13.7 - [(Specify.prep_pbt @{theory} "pbl_simp_rat_partfrac" [] Problem.id_empty
13.8 + [(Problem.prep_input @{theory} "pbl_simp_rat_partfrac" [] Problem.id_empty
13.9 (["partial_fraction", "rational", "simplification"],
13.10 [("#Given" ,["functionTerm t_t", "solveFor v_v"]),
13.11 (* TODO: call this sub-problem with appropriate functionTerm:
13.12 @@ -228,7 +228,7 @@
13.13 pbz = Substitute [AA = a, BB = b] pbz \<comment> \<open>([], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)\<close>
13.14 in pbz) "
13.15 setup \<open>KEStore_Elems.add_mets
13.16 - [Specify.prep_met @{theory} "met_partial_fraction" [] Method.id_empty
13.17 + [Method.prep_input @{theory} "met_partial_fraction" [] Method.id_empty
13.18 (["simplification","of_rationals","to_partial_fraction"],
13.19 [("#Given" ,["functionTerm t_t", "solveFor v_v"]),
13.20 (*("#Where" ,["((get_numerator t_t) has_degree_in v_v) <
14.1 --- a/src/Tools/isac/Knowledge/Poly.thy Wed May 13 12:14:49 2020 +0200
14.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Wed May 13 16:10:22 2020 +0200
14.3 @@ -1434,7 +1434,7 @@
14.4
14.5 subsection \<open>problems\<close>
14.6 setup \<open>KEStore_Elems.add_pbts
14.7 - [(Specify.prep_pbt thy "pbl_simp_poly" [] Problem.id_empty
14.8 + [(Problem.prep_input thy "pbl_simp_poly" [] Problem.id_empty
14.9 (["polynomial","simplification"],
14.10 [("#Given" ,["Term t_t"]),
14.11 ("#Where" ,["t_t is_polyexp"]),
14.12 @@ -1450,7 +1450,7 @@
14.13 where
14.14 "simplify term = ((Rewrite_Set ''norm_Poly'') term)"
14.15 setup \<open>KEStore_Elems.add_mets
14.16 - [Specify.prep_met thy "met_simp_poly" [] Method.id_empty
14.17 + [Method.prep_input thy "met_simp_poly" [] Method.id_empty
14.18 (["simplification","for_polynomials"],
14.19 [("#Given" ,["Term t_t"]),
14.20 ("#Where" ,["t_t is_polyexp"]),
15.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Wed May 13 12:14:49 2020 +0200
15.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Wed May 13 16:10:22 2020 +0200
15.3 @@ -778,7 +778,7 @@
15.4 *)
15.5 \<close>
15.6 setup \<open>KEStore_Elems.add_pbts
15.7 - [(Specify.prep_pbt thy "pbl_equ_univ_poly" [] Problem.id_empty
15.8 + [(Problem.prep_input thy "pbl_equ_univ_poly" [] Problem.id_empty
15.9 (["polynomial","univariate","equation"],
15.10 [("#Given" ,["equality e_e","solveFor v_v"]),
15.11 ("#Where" ,["~((e_e::bool) is_ratequation_in (v_v::real))",
15.12 @@ -787,7 +787,7 @@
15.13 ("#Find" ,["solutions v_v'i'"])],
15.14 PolyEq_prls, SOME "solve (e_e::bool, v_v)", [])),
15.15 (*--- d0 ---*)
15.16 - (Specify.prep_pbt thy "pbl_equ_univ_poly_deg0" [] Problem.id_empty
15.17 + (Problem.prep_input thy "pbl_equ_univ_poly_deg0" [] Problem.id_empty
15.18 (["degree_0","polynomial","univariate","equation"],
15.19 [("#Given" ,["equality e_e","solveFor v_v"]),
15.20 ("#Where" ,["matches (?a = 0) e_e",
15.21 @@ -796,7 +796,7 @@
15.22 ("#Find" ,["solutions v_v'i'"])],
15.23 PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq","solve_d0_polyeq_equation"]])),
15.24 (*--- d1 ---*)
15.25 - (Specify.prep_pbt thy "pbl_equ_univ_poly_deg1" [] Problem.id_empty
15.26 + (Problem.prep_input thy "pbl_equ_univ_poly_deg1" [] Problem.id_empty
15.27 (["degree_1","polynomial","univariate","equation"],
15.28 [("#Given" ,["equality e_e","solveFor v_v"]),
15.29 ("#Where" ,["matches (?a = 0) e_e",
15.30 @@ -805,7 +805,7 @@
15.31 ("#Find" ,["solutions v_v'i'"])],
15.32 PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq","solve_d1_polyeq_equation"]])),
15.33 (*--- d2 ---*)
15.34 - (Specify.prep_pbt thy "pbl_equ_univ_poly_deg2" [] Problem.id_empty
15.35 + (Problem.prep_input thy "pbl_equ_univ_poly_deg2" [] Problem.id_empty
15.36 (["degree_2","polynomial","univariate","equation"],
15.37 [("#Given" ,["equality e_e","solveFor v_v"]),
15.38 ("#Where" ,["matches (?a = 0) e_e",
15.39 @@ -813,7 +813,7 @@
15.40 "((lhs e_e) has_degree_in v_v ) = 2"]),
15.41 ("#Find" ,["solutions v_v'i'"])],
15.42 PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq","solve_d2_polyeq_equation"]])),
15.43 - (Specify.prep_pbt thy "pbl_equ_univ_poly_deg2_sqonly" [] Problem.id_empty
15.44 + (Problem.prep_input thy "pbl_equ_univ_poly_deg2_sqonly" [] Problem.id_empty
15.45 (["sq_only","degree_2","polynomial","univariate","equation"],
15.46 [("#Given" ,["equality e_e","solveFor v_v"]),
15.47 ("#Where" ,["matches ( ?a + ?v_^^^2 = 0) e_e | " ^
15.48 @@ -831,7 +831,7 @@
15.49 ("#Find" ,["solutions v_v'i'"])],
15.50 PolyEq_prls, SOME "solve (e_e::bool, v_v)",
15.51 [["PolyEq","solve_d2_polyeq_sqonly_equation"]])),
15.52 - (Specify.prep_pbt thy "pbl_equ_univ_poly_deg2_bdvonly" [] Problem.id_empty
15.53 + (Problem.prep_input thy "pbl_equ_univ_poly_deg2_bdvonly" [] Problem.id_empty
15.54 (["bdv_only","degree_2","polynomial","univariate","equation"],
15.55 [("#Given", ["equality e_e","solveFor v_v"]),
15.56 ("#Where", ["matches (?a*?v_ + ?v_^^^2 = 0) e_e | " ^
15.57 @@ -843,14 +843,14 @@
15.58 ("#Find", ["solutions v_v'i'"])],
15.59 PolyEq_prls, SOME "solve (e_e::bool, v_v)",
15.60 [["PolyEq","solve_d2_polyeq_bdvonly_equation"]])),
15.61 - (Specify.prep_pbt thy "pbl_equ_univ_poly_deg2_pq" [] Problem.id_empty
15.62 + (Problem.prep_input thy "pbl_equ_univ_poly_deg2_pq" [] Problem.id_empty
15.63 (["pqFormula","degree_2","polynomial","univariate","equation"],
15.64 [("#Given", ["equality e_e","solveFor v_v"]),
15.65 ("#Where", ["matches (?a + 1*?v_^^^2 = 0) e_e | " ^
15.66 "matches (?a + ?v_^^^2 = 0) e_e"]),
15.67 ("#Find", ["solutions v_v'i'"])],
15.68 PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq","solve_d2_polyeq_pq_equation"]])),
15.69 - (Specify.prep_pbt thy "pbl_equ_univ_poly_deg2_abc" [] Problem.id_empty
15.70 + (Problem.prep_input thy "pbl_equ_univ_poly_deg2_abc" [] Problem.id_empty
15.71 (["abcFormula","degree_2","polynomial","univariate","equation"],
15.72 [("#Given", ["equality e_e","solveFor v_v"]),
15.73 ("#Where", ["matches (?a + ?v_^^^2 = 0) e_e | " ^
15.74 @@ -858,7 +858,7 @@
15.75 ("#Find", ["solutions v_v'i'"])],
15.76 PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq","solve_d2_polyeq_abc_equation"]])),
15.77 (*--- d3 ---*)
15.78 - (Specify.prep_pbt thy "pbl_equ_univ_poly_deg3" [] Problem.id_empty
15.79 + (Problem.prep_input thy "pbl_equ_univ_poly_deg3" [] Problem.id_empty
15.80 (["degree_3","polynomial","univariate","equation"],
15.81 [("#Given", ["equality e_e","solveFor v_v"]),
15.82 ("#Where", ["matches (?a = 0) e_e",
15.83 @@ -867,7 +867,7 @@
15.84 ("#Find", ["solutions v_v'i'"])],
15.85 PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq","solve_d3_polyeq_equation"]])),
15.86 (*--- d4 ---*)
15.87 - (Specify.prep_pbt thy "pbl_equ_univ_poly_deg4" [] Problem.id_empty
15.88 + (Problem.prep_input thy "pbl_equ_univ_poly_deg4" [] Problem.id_empty
15.89 (["degree_4","polynomial","univariate","equation"],
15.90 [("#Given", ["equality e_e","solveFor v_v"]),
15.91 ("#Where", ["matches (?a = 0) e_e",
15.92 @@ -876,7 +876,7 @@
15.93 ("#Find", ["solutions v_v'i'"])],
15.94 PolyEq_prls, SOME "solve (e_e::bool, v_v)", [(*["PolyEq","solve_d4_polyeq_equation"]*)])),
15.95 (*--- normalise ---*)
15.96 - (Specify.prep_pbt thy "pbl_equ_univ_poly_norm" [] Problem.id_empty
15.97 + (Problem.prep_input thy "pbl_equ_univ_poly_norm" [] Problem.id_empty
15.98 (["normalise","polynomial","univariate","equation"],
15.99 [("#Given", ["equality e_e","solveFor v_v"]),
15.100 ("#Where", ["(Not((matches (?a = 0 ) e_e ))) |" ^
15.101 @@ -884,7 +884,7 @@
15.102 ("#Find", ["solutions v_v'i'"])],
15.103 PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq", "normalise_poly"]])),
15.104 (*-------------------------expanded-----------------------*)
15.105 - (Specify.prep_pbt thy "pbl_equ_univ_expand" [] Problem.id_empty
15.106 + (Problem.prep_input thy "pbl_equ_univ_expand" [] Problem.id_empty
15.107 (["expanded","univariate","equation"],
15.108 [("#Given", ["equality e_e","solveFor v_v"]),
15.109 ("#Where", ["matches (?a = 0) e_e",
15.110 @@ -892,7 +892,7 @@
15.111 ("#Find", ["solutions v_v'i'"])],
15.112 PolyEq_prls, SOME "solve (e_e::bool, v_v)", [])),
15.113 (*--- d2 ---*)
15.114 - (Specify.prep_pbt thy "pbl_equ_univ_expand_deg2" [] Problem.id_empty
15.115 + (Problem.prep_input thy "pbl_equ_univ_expand_deg2" [] Problem.id_empty
15.116 (["degree_2","expanded","univariate","equation"],
15.117 [("#Given", ["equality e_e","solveFor v_v"]),
15.118 ("#Where", ["((lhs e_e) has_degree_in v_v) = 2"]),
15.119 @@ -901,7 +901,7 @@
15.120
15.121 text \<open>"-------------------------methods-----------------------"\<close>
15.122 setup \<open>KEStore_Elems.add_mets
15.123 - [Specify.prep_met thy "met_polyeq" [] Method.id_empty
15.124 + [Method.prep_input thy "met_polyeq" [] Method.id_empty
15.125 (["PolyEq"], [],
15.126 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
15.127 crls=PolyEq_crls, errpats = [], nrls = norm_Rational},
15.128 @@ -922,7 +922,7 @@
15.129 SubProblem (''PolyEq'', [''polynomial'', ''univariate'', ''equation''], [''no_met''])
15.130 [BOOL e_e, REAL v_v])"
15.131 setup \<open>KEStore_Elems.add_mets
15.132 - [Specify.prep_met thy "met_polyeq_norm" [] Method.id_empty
15.133 + [Method.prep_input thy "met_polyeq_norm" [] Method.id_empty
15.134 (["PolyEq", "normalise_poly"],
15.135 [("#Given" ,["equality e_e","solveFor v_v"]),
15.136 ("#Where" ,["(Not((matches (?a = 0 ) e_e ))) | (Not(((lhs e_e) is_poly_in v_v)))"]),
15.137 @@ -940,7 +940,7 @@
15.138 in
15.139 Or_to_List e_e)"
15.140 setup \<open>KEStore_Elems.add_mets
15.141 - [Specify.prep_met thy "met_polyeq_d0" [] Method.id_empty
15.142 + [Method.prep_input thy "met_polyeq_d0" [] Method.id_empty
15.143 (["PolyEq","solve_d0_polyeq_equation"],
15.144 [("#Given" ,["equality e_e","solveFor v_v"]),
15.145 ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 0"]),
15.146 @@ -963,7 +963,7 @@
15.147 in
15.148 Check_elementwise L_L {(v_v::real). Assumptions})"
15.149 setup \<open>KEStore_Elems.add_mets
15.150 - [Specify.prep_met thy "met_polyeq_d1" [] Method.id_empty
15.151 + [Method.prep_input thy "met_polyeq_d1" [] Method.id_empty
15.152 (["PolyEq","solve_d1_polyeq_equation"],
15.153 [("#Given" ,["equality e_e","solveFor v_v"]),
15.154 ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 1"]),
15.155 @@ -988,7 +988,7 @@
15.156 in
15.157 Check_elementwise L_L {(v_v::real). Assumptions})"
15.158 setup \<open>KEStore_Elems.add_mets
15.159 - [Specify.prep_met thy "met_polyeq_d22" [] Method.id_empty
15.160 + [Method.prep_input thy "met_polyeq_d22" [] Method.id_empty
15.161 (["PolyEq","solve_d2_polyeq_equation"],
15.162 [("#Given" ,["equality e_e","solveFor v_v"]),
15.163 ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 2"]),
15.164 @@ -1013,7 +1013,7 @@
15.165 in
15.166 Check_elementwise L_L {(v_v::real). Assumptions})"
15.167 setup \<open>KEStore_Elems.add_mets
15.168 - [Specify.prep_met thy "met_polyeq_d2_bdvonly" [] Method.id_empty
15.169 + [Method.prep_input thy "met_polyeq_d2_bdvonly" [] Method.id_empty
15.170 (["PolyEq","solve_d2_polyeq_bdvonly_equation"],
15.171 [("#Given" ,["equality e_e","solveFor v_v"]),
15.172 ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 2"]),
15.173 @@ -1036,7 +1036,7 @@
15.174 in
15.175 Check_elementwise L_L {(v_v::real). Assumptions})"
15.176 setup \<open>KEStore_Elems.add_mets
15.177 - [Specify.prep_met thy "met_polyeq_d2_sqonly" [] Method.id_empty
15.178 + [Method.prep_input thy "met_polyeq_d2_sqonly" [] Method.id_empty
15.179 (["PolyEq","solve_d2_polyeq_sqonly_equation"],
15.180 [("#Given" ,["equality e_e","solveFor v_v"]),
15.181 ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 2"]),
15.182 @@ -1059,7 +1059,7 @@
15.183 in
15.184 Check_elementwise L_L {(v_v::real). Assumptions})"
15.185 setup \<open>KEStore_Elems.add_mets
15.186 - [Specify.prep_met thy "met_polyeq_d2_pq" [] Method.id_empty
15.187 + [Method.prep_input thy "met_polyeq_d2_pq" [] Method.id_empty
15.188 (["PolyEq","solve_d2_polyeq_pq_equation"],
15.189 [("#Given" ,["equality e_e","solveFor v_v"]),
15.190 ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 2"]),
15.191 @@ -1081,7 +1081,7 @@
15.192 L_L = Or_to_List e_e
15.193 in Check_elementwise L_L {(v_v::real). Assumptions})"
15.194 setup \<open>KEStore_Elems.add_mets
15.195 - [Specify.prep_met thy "met_polyeq_d2_abc" [] Method.id_empty
15.196 + [Method.prep_input thy "met_polyeq_d2_abc" [] Method.id_empty
15.197 (["PolyEq","solve_d2_polyeq_abc_equation"],
15.198 [("#Given" ,["equality e_e","solveFor v_v"]),
15.199 ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 2"]),
15.200 @@ -1108,7 +1108,7 @@
15.201 in
15.202 Check_elementwise L_L {(v_v::real). Assumptions})"
15.203 setup \<open>KEStore_Elems.add_mets
15.204 - [Specify.prep_met thy "met_polyeq_d3" [] Method.id_empty
15.205 + [Method.prep_input thy "met_polyeq_d3" [] Method.id_empty
15.206 (["PolyEq","solve_d3_polyeq_equation"],
15.207 [("#Given" ,["equality e_e","solveFor v_v"]),
15.208 ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 3"]),
15.209 @@ -1138,7 +1138,7 @@
15.210 in
15.211 Or_to_List e_e)"
15.212 setup \<open>KEStore_Elems.add_mets
15.213 - [Specify.prep_met thy "met_polyeq_complsq" [] Method.id_empty
15.214 + [Method.prep_input thy "met_polyeq_complsq" [] Method.id_empty
15.215 (["PolyEq","complete_square"],
15.216 [("#Given" ,["equality e_e","solveFor v_v"]),
15.217 ("#Where" ,["matches (?a = 0) e_e", "((lhs e_e) has_degree_in v_v) = 2"]),
16.1 --- a/src/Tools/isac/Knowledge/PolyMinus.thy Wed May 13 12:14:49 2020 +0200
16.2 +++ b/src/Tools/isac/Knowledge/PolyMinus.thy Wed May 13 16:10:22 2020 +0200
16.3 @@ -392,9 +392,9 @@
16.4
16.5 (** problems **)
16.6 setup \<open>KEStore_Elems.add_pbts
16.7 - [(Specify.prep_pbt thy "pbl_vereinf_poly" [] Problem.id_empty
16.8 + [(Problem.prep_input thy "pbl_vereinf_poly" [] Problem.id_empty
16.9 (["polynom","vereinfachen"], [], Rule_Set.Empty, NONE, [])),
16.10 - (Specify.prep_pbt thy "pbl_vereinf_poly_minus" [] Problem.id_empty
16.11 + (Problem.prep_input thy "pbl_vereinf_poly_minus" [] Problem.id_empty
16.12 (["plus_minus","polynom","vereinfachen"],
16.13 [("#Given", ["Term t_t"]),
16.14 ("#Where", ["t_t is_polyexp",
16.15 @@ -419,7 +419,7 @@
16.16 Rule.Thm ("not_false",ThmC.numerals_to_Free @{thm not_false})
16.17 (*"(~ False) = True"*)],
16.18 SOME "Vereinfache t_t", [["simplification","for_polynomials","with_minus"]])),
16.19 - (Specify.prep_pbt thy "pbl_vereinf_poly_klammer" [] Problem.id_empty
16.20 + (Problem.prep_input thy "pbl_vereinf_poly_klammer" [] Problem.id_empty
16.21 (["klammer","polynom","vereinfachen"],
16.22 [("#Given" ,["Term t_t"]),
16.23 ("#Where" ,["t_t is_polyexp",
16.24 @@ -441,7 +441,7 @@
16.25 (*"(~ False) = True"*)],
16.26 SOME "Vereinfache t_t",
16.27 [["simplification","for_polynomials","with_parentheses"]])),
16.28 - (Specify.prep_pbt thy "pbl_vereinf_poly_klammer_mal" [] Problem.id_empty
16.29 + (Problem.prep_input thy "pbl_vereinf_poly_klammer_mal" [] Problem.id_empty
16.30 (["binom_klammer","polynom","vereinfachen"],
16.31 [("#Given", ["Term t_t"]),
16.32 ("#Where", ["t_t is_polyexp"]),
16.33 @@ -450,8 +450,8 @@
16.34 Rule.Eval ("Poly.is'_polyexp", eval_is_polyexp "")],
16.35 SOME "Vereinfache t_t",
16.36 [["simplification","for_polynomials","with_parentheses_mult"]])),
16.37 - (Specify.prep_pbt thy "pbl_probe" [] Problem.id_empty (["probe"], [], Rule_Set.Empty, NONE, [])),
16.38 - (Specify.prep_pbt thy "pbl_probe_poly" [] Problem.id_empty
16.39 + (Problem.prep_input thy "pbl_probe" [] Problem.id_empty (["probe"], [], Rule_Set.Empty, NONE, [])),
16.40 + (Problem.prep_input thy "pbl_probe_poly" [] Problem.id_empty
16.41 (["polynom","probe"],
16.42 [("#Given", ["Pruefe e_e", "mitWert w_w"]),
16.43 ("#Where", ["e_e is_polyexp"]),
16.44 @@ -460,7 +460,7 @@
16.45 Rule.Eval ("Poly.is'_polyexp", eval_is_polyexp "")],
16.46 SOME "Probe e_e w_w",
16.47 [["probe","fuer_polynom"]])),
16.48 - (Specify.prep_pbt thy "pbl_probe_bruch" [] Problem.id_empty
16.49 + (Problem.prep_input thy "pbl_probe_bruch" [] Problem.id_empty
16.50 (["bruch","probe"],
16.51 [("#Given" ,["Pruefe e_e", "mitWert w_w"]),
16.52 ("#Where" ,["e_e is_ratpolyexp"]),
16.53 @@ -480,7 +480,7 @@
16.54 (Try (Rewrite_Set ''verschoenere'')))
16.55 ) t_t)"
16.56 setup \<open>KEStore_Elems.add_mets
16.57 - [Specify.prep_met thy "met_simp_poly_minus" [] Method.id_empty
16.58 + [Method.prep_input thy "met_simp_poly_minus" [] Method.id_empty
16.59 (["simplification","for_polynomials","with_minus"],
16.60 [("#Given" ,["Term t_t"]),
16.61 ("#Where" ,["t_t is_polyexp",
16.62 @@ -515,7 +515,7 @@
16.63 (Try (Rewrite_Set ''verschoenere'')))
16.64 ) t_t)"
16.65 setup \<open>KEStore_Elems.add_mets
16.66 - [Specify.prep_met thy "met_simp_poly_parenth" [] Method.id_empty
16.67 + [Method.prep_input thy "met_simp_poly_parenth" [] Method.id_empty
16.68 (["simplification","for_polynomials","with_parentheses"],
16.69 [("#Given" ,["Term t_t"]),
16.70 ("#Where" ,["t_t is_polyexp"]),
16.71 @@ -540,7 +540,7 @@
16.72 (Try (Rewrite_Set ''verschoenere'')))
16.73 ) t_t)"
16.74 setup \<open>KEStore_Elems.add_mets
16.75 - [Specify.prep_met thy "met_simp_poly_parenth_mult" [] Method.id_empty
16.76 + [Method.prep_input thy "met_simp_poly_parenth_mult" [] Method.id_empty
16.77 (["simplification","for_polynomials","with_parentheses_mult"],
16.78 [("#Given" ,["Term t_t"]), ("#Where" ,["t_t is_polyexp"]), ("#Find" ,["normalform n_n"])],
16.79 {rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty,
16.80 @@ -550,7 +550,7 @@
16.81 @{thm simplify3.simps})]
16.82 \<close>
16.83 setup \<open>KEStore_Elems.add_mets
16.84 - [Specify.prep_met thy "met_probe" [] Method.id_empty
16.85 + [Method.prep_input thy "met_probe" [] Method.id_empty
16.86 (["probe"], [],
16.87 {rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.Empty, crls = Rule_Set.empty,
16.88 errpats = [], nrls = Rule_Set.Empty},
16.89 @@ -570,7 +570,7 @@
16.90 (Try (Repeat (Calculate ''MINUS''))))
16.91 ) e_e)"
16.92 setup \<open>KEStore_Elems.add_mets
16.93 - [Specify.prep_met thy "met_probe_poly" [] Method.id_empty
16.94 + [Method.prep_input thy "met_probe_poly" [] Method.id_empty
16.95 (["probe","fuer_polynom"],
16.96 [("#Given" ,["Pruefe e_e", "mitWert w_w"]),
16.97 ("#Where" ,["e_e is_polyexp"]),
16.98 @@ -582,7 +582,7 @@
16.99 @{thm mache_probe.simps})]
16.100 \<close>
16.101 setup \<open>KEStore_Elems.add_mets
16.102 - [Specify.prep_met thy "met_probe_bruch" [] Method.id_empty
16.103 + [Method.prep_input thy "met_probe_bruch" [] Method.id_empty
16.104 (["probe","fuer_bruch"],
16.105 [("#Given" ,["Pruefe e_e", "mitWert w_w"]),
16.106 ("#Where" ,["e_e is_ratpolyexp"]),
17.1 --- a/src/Tools/isac/Knowledge/RatEq.thy Wed May 13 12:14:49 2020 +0200
17.2 +++ b/src/Tools/isac/Knowledge/RatEq.thy Wed May 13 16:10:22 2020 +0200
17.3 @@ -161,7 +161,7 @@
17.4
17.5 subsection \<open>problems\<close>
17.6 setup \<open>KEStore_Elems.add_pbts
17.7 - [(Specify.prep_pbt thy "pbl_equ_univ_rat" [] Problem.id_empty
17.8 + [(Problem.prep_input thy "pbl_equ_univ_rat" [] Problem.id_empty
17.9 (["rational","univariate","equation"],
17.10 [("#Given", ["equality e_e","solveFor v_v"]),
17.11 ("#Where", ["(e_e::bool) is_ratequation_in (v_v::real)"]),
17.12 @@ -170,7 +170,7 @@
17.13
17.14 subsection \<open>methods\<close>
17.15 setup \<open>KEStore_Elems.add_mets
17.16 - [Specify.prep_met thy "met_rateq" [] Method.id_empty
17.17 + [Method.prep_input thy "met_rateq" [] Method.id_empty
17.18 (["RatEq"], [],
17.19 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
17.20 crls=RatEq_crls, errpats = [], nrls = norm_Rational}, @{thm refl})]\<close>
17.21 @@ -188,7 +188,7 @@
17.22 in
17.23 Check_elementwise L_L {(v_v::real). Assumptions})"
17.24 setup \<open>KEStore_Elems.add_mets
17.25 - [Specify.prep_met thy "met_rat_eq" [] Method.id_empty
17.26 + [Method.prep_input thy "met_rat_eq" [] Method.id_empty
17.27 (["RatEq", "solve_rat_equation"],
17.28 [("#Given" ,["equality e_e","solveFor v_v"]),
17.29 ("#Where" ,["(e_e::bool) is_ratequation_in (v_v::real)"]),
18.1 --- a/src/Tools/isac/Knowledge/Rational.thy Wed May 13 12:14:49 2020 +0200
18.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Wed May 13 16:10:22 2020 +0200
18.3 @@ -877,7 +877,7 @@
18.4
18.5 section \<open>A problem for simplification of rationals\<close>
18.6 setup \<open>KEStore_Elems.add_pbts
18.7 - [(Specify.prep_pbt thy "pbl_simp_rat" [] Problem.id_empty
18.8 + [(Problem.prep_input thy "pbl_simp_rat" [] Problem.id_empty
18.9 (["rational","simplification"],
18.10 [("#Given" ,["Term t_t"]),
18.11 ("#Where" ,["t_t is_ratpolyexp"]),
18.12 @@ -905,7 +905,7 @@
18.13 Try (Rewrite_Set ''discard_parentheses1''))
18.14 term)"
18.15 setup \<open>KEStore_Elems.add_mets
18.16 - [Specify.prep_met thy "met_simp_rat" [] Method.id_empty
18.17 + [Method.prep_input thy "met_simp_rat" [] Method.id_empty
18.18 (["simplification","of_rationals"],
18.19 [("#Given" ,["Term t_t"]),
18.20 ("#Where" ,["t_t is_ratpolyexp"]),
19.1 --- a/src/Tools/isac/Knowledge/RootEq.thy Wed May 13 12:14:49 2020 +0200
19.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy Wed May 13 16:10:22 2020 +0200
19.3 @@ -444,7 +444,7 @@
19.4 subsection \<open>problems\<close>
19.5 setup \<open>KEStore_Elems.add_pbts
19.6 (* ---------root----------- *)
19.7 - [(Specify.prep_pbt thy "pbl_equ_univ_root" [] Problem.id_empty
19.8 + [(Problem.prep_input thy "pbl_equ_univ_root" [] Problem.id_empty
19.9 (["rootX","univariate","equation"],
19.10 [("#Given" ,["equality e_e","solveFor v_v"]),
19.11 ("#Where" ,["(lhs e_e) is_rootTerm_in (v_v::real) | " ^
19.12 @@ -452,7 +452,7 @@
19.13 ("#Find" ,["solutions v_v'i'"])],
19.14 RootEq_prls, SOME "solve (e_e::bool, v_v)", [])),
19.15 (* ---------sqrt----------- *)
19.16 - (Specify.prep_pbt thy "pbl_equ_univ_root_sq" [] Problem.id_empty
19.17 + (Problem.prep_input thy "pbl_equ_univ_root_sq" [] Problem.id_empty
19.18 (["sq","rootX","univariate","equation"],
19.19 [("#Given" ,["equality e_e","solveFor v_v"]),
19.20 ("#Where" ,["( ((lhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
19.21 @@ -462,7 +462,7 @@
19.22 ("#Find" ,["solutions v_v'i'"])],
19.23 RootEq_prls, SOME "solve (e_e::bool, v_v)", [["RootEq", "solve_sq_root_equation"]])),
19.24 (* ---------normalise----------- *)
19.25 - (Specify.prep_pbt thy "pbl_equ_univ_root_norm" [] Problem.id_empty
19.26 + (Problem.prep_input thy "pbl_equ_univ_root_norm" [] Problem.id_empty
19.27 (["normalise","rootX","univariate","equation"],
19.28 [("#Given" ,["equality e_e","solveFor v_v"]),
19.29 ("#Where" ,["( ((lhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
19.30 @@ -474,7 +474,7 @@
19.31
19.32 subsection \<open>methods\<close>
19.33 setup \<open>KEStore_Elems.add_mets
19.34 - [Specify.prep_met thy "met_rooteq" [] Method.id_empty
19.35 + [Method.prep_input thy "met_rooteq" [] Method.id_empty
19.36 (["RootEq"], [],
19.37 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
19.38 crls=RootEq_crls, errpats = [], nrls = norm_Poly}, @{thm refl})]
19.39 @@ -495,7 +495,7 @@
19.40 SubProblem (''RootEq'', [''univariate'', ''equation''], [''no_met''])
19.41 [BOOL e_e, REAL v_v])"
19.42 setup \<open>KEStore_Elems.add_mets
19.43 - [Specify.prep_met thy "met_rooteq_norm" [] Method.id_empty
19.44 + [Method.prep_input thy "met_rooteq_norm" [] Method.id_empty
19.45 (["RootEq","norm_sq_root_equation"],
19.46 [("#Given" ,["equality e_e","solveFor v_v"]),
19.47 ("#Where" ,["( ((lhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
19.48 @@ -528,7 +528,7 @@
19.49 [BOOL e_e, REAL v_v])
19.50 in Check_elementwise L_L {(v_v::real). Assumptions})"
19.51 setup \<open>KEStore_Elems.add_mets
19.52 - [Specify.prep_met thy "met_rooteq_sq" [] Method.id_empty
19.53 + [Method.prep_input thy "met_rooteq_sq" [] Method.id_empty
19.54 (["RootEq", "solve_sq_root_equation"],
19.55 [("#Given" ,["equality e_e", "solveFor v_v"]),
19.56 ("#Where" ,["(((lhs e_e) is_sqrtTerm_in (v_v::real)) & " ^
19.57 @@ -560,7 +560,7 @@
19.58 SubProblem (''RootEq'',[''univariate'', ''equation''], [''no_met''])
19.59 [BOOL e_e, REAL v_v])"
19.60 setup \<open>KEStore_Elems.add_mets
19.61 - [Specify.prep_met thy "met_rooteq_sq_right" [] Method.id_empty
19.62 + [Method.prep_input thy "met_rooteq_sq_right" [] Method.id_empty
19.63 (["RootEq","solve_right_sq_root_equation"],
19.64 [("#Given" ,["equality e_e","solveFor v_v"]),
19.65 ("#Where" ,["(rhs e_e) is_sqrtTerm_in v_v"]),
19.66 @@ -589,7 +589,7 @@
19.67 SubProblem (''RootEq'',[''univariate'',''equation''], [''no_met''])
19.68 [BOOL e_e, REAL v_v])"
19.69 setup \<open>KEStore_Elems.add_mets
19.70 - [Specify.prep_met thy "met_rooteq_sq_left" [] Method.id_empty
19.71 + [Method.prep_input thy "met_rooteq_sq_left" [] Method.id_empty
19.72 (["RootEq","solve_left_sq_root_equation"],
19.73 [("#Given" ,["equality e_e","solveFor v_v"]),
19.74 ("#Where" ,["(lhs e_e) is_sqrtTerm_in v_v"]),
20.1 --- a/src/Tools/isac/Knowledge/RootRatEq.thy Wed May 13 12:14:49 2020 +0200
20.2 +++ b/src/Tools/isac/Knowledge/RootRatEq.thy Wed May 13 16:10:22 2020 +0200
20.3 @@ -129,7 +129,7 @@
20.4 *)
20.5 \<close>
20.6 setup \<open>KEStore_Elems.add_pbts
20.7 - [(Specify.prep_pbt thy "pbl_equ_univ_root_sq_rat" [] Problem.id_empty
20.8 + [(Problem.prep_input thy "pbl_equ_univ_root_sq_rat" [] Problem.id_empty
20.9 (["rat","sq","rootX","univariate","equation"],
20.10 [("#Given" ,["equality e_e","solveFor v_v"]),
20.11 ("#Where" ,["( (lhs e_e) is_rootRatAddTerm_in (v_v::real) )| " ^
20.12 @@ -139,7 +139,7 @@
20.13
20.14 subsection \<open>methods\<close>
20.15 setup \<open>KEStore_Elems.add_mets
20.16 - [Specify.prep_met @{theory LinEq} "met_rootrateq" [] Method.id_empty
20.17 + [Method.prep_input @{theory LinEq} "met_rootrateq" [] Method.id_empty
20.18 (["RootRatEq"], [],
20.19 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
20.20 crls=Atools_erls, errpats = [], nrls = norm_Rational}, @{thm refl})]
20.21 @@ -157,7 +157,7 @@
20.22 (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''rootrat_solve'')) ) e_e
20.23 in SubProblem (''RootEq'', [''univariate'', ''equation''], [''no_met'']) [BOOL e_e, REAL v_v])"
20.24 setup \<open>KEStore_Elems.add_mets
20.25 - [Specify.prep_met thy "met_rootrateq_elim" [] Method.id_empty
20.26 + [Method.prep_input thy "met_rootrateq_elim" [] Method.id_empty
20.27 (["RootRatEq","elim_rootrat_equation"],
20.28 [("#Given" ,["equality e_e","solveFor v_v"]),
20.29 ("#Where" ,["( (lhs e_e) is_rootRatAddTerm_in (v_v::real) ) | " ^
21.1 --- a/src/Tools/isac/Knowledge/Simplify.thy Wed May 13 12:14:49 2020 +0200
21.2 +++ b/src/Tools/isac/Knowledge/Simplify.thy Wed May 13 16:10:22 2020 +0200
21.3 @@ -25,12 +25,12 @@
21.4 \<close>
21.5 (** problems **)
21.6 setup \<open>KEStore_Elems.add_pbts
21.7 - [(Specify.prep_pbt thy "pbl_simp" [] Problem.id_empty
21.8 + [(Problem.prep_input thy "pbl_simp" [] Problem.id_empty
21.9 (["simplification"],
21.10 [("#Given" ,["Term t_t"]),
21.11 ("#Find" ,["normalform n_n"])],
21.12 Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)], SOME "Simplify t_t", [])),
21.13 - (Specify.prep_pbt thy "pbl_vereinfache" [] Problem.id_empty
21.14 + (Problem.prep_input thy "pbl_vereinfache" [] Problem.id_empty
21.15 (["vereinfachen"],
21.16 [("#Given", ["Term t_t"]),
21.17 ("#Find", ["normalform n_n"])],
21.18 @@ -38,7 +38,7 @@
21.19
21.20 (** methods **)
21.21 setup \<open>KEStore_Elems.add_mets
21.22 - [Specify.prep_met thy "met_tsimp" [] Method.id_empty
21.23 + [Method.prep_input thy "met_tsimp" [] Method.id_empty
21.24 (["simplification"],
21.25 [("#Given" ,["Term t_t"]),
21.26 ("#Find" ,["normalform n_n"])],
22.1 --- a/src/Tools/isac/Knowledge/Test.thy Wed May 13 12:14:49 2020 +0200
22.2 +++ b/src/Tools/isac/Knowledge/Test.thy Wed May 13 16:10:22 2020 +0200
22.3 @@ -570,20 +570,20 @@
22.4 subsection \<open>problems\<close>
22.5 (** problem types **)
22.6 setup \<open>KEStore_Elems.add_pbts
22.7 - [(Specify.prep_pbt thy "pbl_test" [] Problem.id_empty (["test"], [], Rule_Set.empty, NONE, [])),
22.8 - (Specify.prep_pbt thy "pbl_test_equ" [] Problem.id_empty
22.9 + [(Problem.prep_input thy "pbl_test" [] Problem.id_empty (["test"], [], Rule_Set.empty, NONE, [])),
22.10 + (Problem.prep_input thy "pbl_test_equ" [] Problem.id_empty
22.11 (["equation","test"],
22.12 [("#Given" ,["equality e_e","solveFor v_v"]),
22.13 ("#Where" ,["matches (?a = ?b) e_e"]),
22.14 ("#Find" ,["solutions v_v'i'"])],
22.15 assoc_rls' @{theory} "matches", SOME "solve (e_e::bool, v_v)", [])),
22.16 - (Specify.prep_pbt thy "pbl_test_uni" [] Problem.id_empty
22.17 + (Problem.prep_input thy "pbl_test_uni" [] Problem.id_empty
22.18 (["univariate","equation","test"],
22.19 [("#Given" ,["equality e_e","solveFor v_v"]),
22.20 ("#Where" ,["matches (?a = ?b) e_e"]),
22.21 ("#Find" ,["solutions v_v'i'"])],
22.22 assoc_rls' @{theory} "matches", SOME "solve (e_e::bool, v_v)", [])),
22.23 - (Specify.prep_pbt thy "pbl_test_uni_lin" [] Problem.id_empty
22.24 + (Problem.prep_input thy "pbl_test_uni_lin" [] Problem.id_empty
22.25 (["LINEAR","univariate","equation","test"],
22.26 [("#Given" ,["equality e_e","solveFor v_v"]),
22.27 ("#Where" ,["(matches ( v_v = 0) e_e) | (matches ( ?b*v_v = 0) e_e) |" ^
22.28 @@ -772,7 +772,7 @@
22.29
22.30 section \<open>problems\<close>
22.31 setup \<open>KEStore_Elems.add_pbts
22.32 - [(Specify.prep_pbt thy "pbl_test_uni_plain2" [] Problem.id_empty
22.33 + [(Problem.prep_input thy "pbl_test_uni_plain2" [] Problem.id_empty
22.34 (["plain_square","univariate","equation","test"],
22.35 [("#Given" ,["equality e_e","solveFor v_v"]),
22.36 ("#Where" ,["(matches (?a + ?b*v_v ^^^2 = 0) e_e) |" ^
22.37 @@ -782,28 +782,28 @@
22.38 ("#Find" ,["solutions v_v'i'"])],
22.39 assoc_rls' @{theory} "matches",
22.40 SOME "solve (e_e::bool, v_v)", [["Test","solve_plain_square"]])),
22.41 - (Specify.prep_pbt thy "pbl_test_uni_poly" [] Problem.id_empty
22.42 + (Problem.prep_input thy "pbl_test_uni_poly" [] Problem.id_empty
22.43 (["polynomial","univariate","equation","test"],
22.44 [("#Given" ,["equality (v_v ^^^2 + p_p * v_v + q__q = 0)","solveFor v_v"]),
22.45 ("#Where" ,["HOL.False"]),
22.46 ("#Find" ,["solutions v_v'i'"])],
22.47 Rule_Set.empty, SOME "solve (e_e::bool, v_v)", [])),
22.48 - (Specify.prep_pbt thy "pbl_test_uni_poly_deg2" [] Problem.id_empty
22.49 + (Problem.prep_input thy "pbl_test_uni_poly_deg2" [] Problem.id_empty
22.50 (["degree_two","polynomial","univariate","equation","test"],
22.51 [("#Given" ,["equality (v_v ^^^2 + p_p * v_v + q__q = 0)","solveFor v_v"]),
22.52 ("#Find" ,["solutions v_v'i'"])],
22.53 Rule_Set.empty, SOME "solve (v_v ^^^2 + p_p * v_v + q__q = 0, v_v)", [])),
22.54 - (Specify.prep_pbt thy "pbl_test_uni_poly_deg2_pq" [] Problem.id_empty
22.55 + (Problem.prep_input thy "pbl_test_uni_poly_deg2_pq" [] Problem.id_empty
22.56 (["pq_formula","degree_two","polynomial","univariate","equation","test"],
22.57 [("#Given" ,["equality (v_v ^^^2 + p_p * v_v + q__q = 0)","solveFor v_v"]),
22.58 ("#Find" ,["solutions v_v'i'"])],
22.59 Rule_Set.empty, SOME "solve (v_v ^^^2 + p_p * v_v + q__q = 0, v_v)", [])),
22.60 - (Specify.prep_pbt thy "pbl_test_uni_poly_deg2_abc" [] Problem.id_empty
22.61 + (Problem.prep_input thy "pbl_test_uni_poly_deg2_abc" [] Problem.id_empty
22.62 (["abc_formula","degree_two","polynomial","univariate","equation","test"],
22.63 [("#Given" ,["equality (a_a * x ^^^2 + b_b * x + c_c = 0)","solveFor v_v"]),
22.64 ("#Find" ,["solutions v_v'i'"])],
22.65 Rule_Set.empty, SOME "solve (a_a * x ^^^2 + b_b * x + c_c = 0, v_v)", [])),
22.66 - (Specify.prep_pbt thy "pbl_test_uni_root" [] Problem.id_empty
22.67 + (Problem.prep_input thy "pbl_test_uni_root" [] Problem.id_empty
22.68 (["squareroot","univariate","equation","test"],
22.69 [("#Given" ,["equality e_e","solveFor v_v"]),
22.70 ("#Where" ,["precond_rootpbl v_v"]),
22.71 @@ -811,19 +811,19 @@
22.72 Rule_Set.append_rules "contains_root" Rule_Set.empty [Rule.Eval ("Test.contains'_root",
22.73 eval_contains_root "#contains_root_")],
22.74 SOME "solve (e_e::bool, v_v)", [["Test","square_equation"]])),
22.75 - (Specify.prep_pbt thy "pbl_test_uni_norm" [] Problem.id_empty
22.76 + (Problem.prep_input thy "pbl_test_uni_norm" [] Problem.id_empty
22.77 (["normalise","univariate","equation","test"],
22.78 [("#Given" ,["equality e_e","solveFor v_v"]),
22.79 ("#Where" ,[]),
22.80 ("#Find" ,["solutions v_v'i'"])],
22.81 Rule_Set.empty, SOME "solve (e_e::bool, v_v)", [["Test","norm_univar_equation"]])),
22.82 - (Specify.prep_pbt thy "pbl_test_uni_roottest" [] Problem.id_empty
22.83 + (Problem.prep_input thy "pbl_test_uni_roottest" [] Problem.id_empty
22.84 (["sqroot-test","univariate","equation","test"],
22.85 [("#Given" ,["equality e_e","solveFor v_v"]),
22.86 ("#Where" ,["precond_rootpbl v_v"]),
22.87 ("#Find" ,["solutions v_v'i'"])],
22.88 Rule_Set.empty, SOME "solve (e_e::bool, v_v)", [])),
22.89 - (Specify.prep_pbt thy "pbl_test_intsimp" [] Problem.id_empty
22.90 + (Problem.prep_input thy "pbl_test_intsimp" [] Problem.id_empty
22.91 (["inttype","test"],
22.92 [("#Given" ,["intTestGiven t_t"]),
22.93 ("#Where" ,[]),
22.94 @@ -833,7 +833,7 @@
22.95 section \<open>methods\<close>
22.96 subsection \<open>differentiate\<close>
22.97 setup \<open>KEStore_Elems.add_mets
22.98 - [Specify.prep_met @{theory "Diff"} "met_test" [] Method.id_empty
22.99 + [Method.prep_input @{theory "Diff"} "met_test" [] Method.id_empty
22.100 (["Test"], [],
22.101 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
22.102 crls=Atools_erls, errpats = [], nrls = Rule_Set.empty}, @{thm refl})]
22.103 @@ -849,7 +849,7 @@
22.104 in
22.105 [e_e])"
22.106 setup \<open>KEStore_Elems.add_mets
22.107 - [Specify.prep_met thy "met_test_solvelin" [] Method.id_empty
22.108 + [Method.prep_input thy "met_test_solvelin" [] Method.id_empty
22.109 (["Test","solve_linear"],
22.110 [("#Given" ,["equality e_e","solveFor v_v"]),
22.111 ("#Where" ,["matches (?a = ?b) e_e"]),
22.112 @@ -880,7 +880,7 @@
22.113 in
22.114 [e_e])"
22.115 setup \<open>KEStore_Elems.add_mets
22.116 - [Specify.prep_met thy "met_test_sqrt" [] Method.id_empty
22.117 + [Method.prep_input thy "met_test_sqrt" [] Method.id_empty
22.118 (*root-equation, version for tests before 8.01.01*)
22.119 (["Test","sqrt-equ-test"],
22.120 [("#Given" ,["equality e_e","solveFor v_v"]),
22.121 @@ -908,7 +908,7 @@
22.122 in
22.123 Check_elementwise L_L {(v_v::real). Assumptions})"
22.124 setup \<open>KEStore_Elems.add_mets
22.125 - [Specify.prep_met thy "met_test_squ_sub" [] Method.id_empty
22.126 + [Method.prep_input thy "met_test_squ_sub" [] Method.id_empty
22.127 (*tests subproblem fixed linear*)
22.128 (["Test","squ-equ-test-subpbl1"],
22.129 [("#Given" ,["equality e_e","solveFor v_v"]),
22.130 @@ -940,7 +940,7 @@
22.131 in
22.132 Check_elementwise L_L {(v_v::real). Assumptions}) "
22.133 setup \<open>KEStore_Elems.add_mets
22.134 - [Specify.prep_met thy "met_test_eq1" [] Method.id_empty
22.135 + [Method.prep_input thy "met_test_eq1" [] Method.id_empty
22.136 (*root-equation1:*)
22.137 (["Test","square_equation1"],
22.138 [("#Given" ,["equality e_e","solveFor v_v"]),
22.139 @@ -973,7 +973,7 @@
22.140 in
22.141 Check_elementwise L_L {(v_v::real). Assumptions})"
22.142 setup \<open>KEStore_Elems.add_mets
22.143 - [Specify.prep_met thy "met_test_squ2" [] Method.id_empty
22.144 + [Method.prep_input thy "met_test_squ2" [] Method.id_empty
22.145 (*root-equation2*)
22.146 (["Test","square_equation2"],
22.147 [("#Given" ,["equality e_e","solveFor v_v"]),
22.148 @@ -1006,7 +1006,7 @@
22.149 in
22.150 Check_elementwise L_L {(v_v::real). Assumptions})"
22.151 setup \<open>KEStore_Elems.add_mets
22.152 - [Specify.prep_met thy "met_test_squeq" [] Method.id_empty
22.153 + [Method.prep_input thy "met_test_squeq" [] Method.id_empty
22.154 (*root-equation*)
22.155 (["Test","square_equation"],
22.156 [("#Given" ,["equality e_e","solveFor v_v"]),
22.157 @@ -1032,7 +1032,7 @@
22.158 in
22.159 Or_to_List e_e)"
22.160 setup \<open>KEStore_Elems.add_mets
22.161 - [Specify.prep_met thy "met_test_eq_plain" [] Method.id_empty
22.162 + [Method.prep_input thy "met_test_eq_plain" [] Method.id_empty
22.163 (*solve_plain_square*)
22.164 (["Test","solve_plain_square"],
22.165 [("#Given",["equality e_e","solveFor v_v"]),
22.166 @@ -1059,7 +1059,7 @@
22.167 SubProblem (''Test'', [''univariate'', ''equation'', ''test''],
22.168 [''no_met'']) [BOOL e_e, REAL v_v])"
22.169 setup \<open>KEStore_Elems.add_mets
22.170 - [Specify.prep_met thy "met_test_norm_univ" [] Method.id_empty
22.171 + [Method.prep_input thy "met_test_norm_univ" [] Method.id_empty
22.172 (["Test","norm_univar_equation"],
22.173 [("#Given",["equality e_e","solveFor v_v"]),
22.174 ("#Where" ,[]),
22.175 @@ -1077,7 +1077,7 @@
22.176 (Try (Calculate ''PLUS'')) #>
22.177 (Try (Calculate ''TIMES''))) t_t)"
22.178 setup \<open>KEStore_Elems.add_mets
22.179 - [Specify.prep_met thy "met_test_intsimp" [] Method.id_empty
22.180 + [Method.prep_input thy "met_test_intsimp" [] Method.id_empty
22.181 (["Test","intsimp"],
22.182 [("#Given" ,["intTestGiven t_t"]),
22.183 ("#Where" ,[]),
23.1 --- a/src/Tools/isac/MathEngBasic/method.sml Wed May 13 12:14:49 2020 +0200
23.2 +++ b/src/Tools/isac/MathEngBasic/method.sml Wed May 13 16:10:22 2020 +0200
23.3 @@ -12,6 +12,11 @@
23.4 val id_empty: id
23.5 val id_to_string: id -> string
23.6
23.7 + type input
23.8 + (* TODO: ------------- remove always empty --- vvvvvvvvvvv -- vvv*)
23.9 + val prep_input : theory -> Check_Unique.id -> string list -> id ->
23.10 + id * Problem.model_input * input * thm -> T * id
23.11 +
23.12 val from_store: id -> T
23.13 val from_store': theory -> id -> T
23.14
23.15 @@ -34,6 +39,61 @@
23.16 val id_empty = Meth_Def.id_empty;
23.17 val id_to_string = Meth_Def.id_to_string;
23.18
23.19 +
23.20 +(** prepare Method for Store **)
23.21 +
23.22 +(* a subset of Method.T record's fields *)
23.23 +type input =
23.24 + {calc: Rule_Def.calc list, crls: Rule_Set.T, errpats: Error_Pattern_Def.T list, nrls: Rule_Set.T,
23.25 + prls: Rule_Set.T, rew_ord': Rewrite_Ord.rew_ord', rls': Rule_Set.T, srls: Rule_Set.T}
23.26 +
23.27 +fun prep_input thy guh maa init
23.28 + (metID, ppc,
23.29 + {rew_ord' = ro, rls' = rls, srls = srls, prls = prls, calc = _(*scr_isa_fns*), crls = cr,
23.30 + errpats = ep, nrls = nr}, scr) =
23.31 + let
23.32 + fun eq f (f', _) = f = f';
23.33 + val gi = filter (eq "#Given") ppc;
23.34 + val gi = (case gi of
23.35 + [] => (writeln ("prep_input: in " ^ guh ^ " #Given is empty ?!?"); [])
23.36 + | ((_, gi') :: []) => (map (Problem.split_did o Thm.term_of o the o (TermC.parse thy)) gi'
23.37 + handle _ => raise ERROR ("prep_pbt: syntax raise ERROR in '#Given' of " ^ strs2str metID))
23.38 + | _ => raise ERROR ("prep_pbt: more than one '#Given' in " ^ strs2str metID));
23.39 + val gi = map (pair "#Given") gi;
23.40 +
23.41 + val fi = filter (eq "#Find") ppc;
23.42 + val fi = (case fi of
23.43 + [] => (writeln ("prep_input: in " ^ guh ^ " #Find is empty ?!?"); [])
23.44 + | ((_, fi') :: []) => (map (Problem.split_did o Thm.term_of o the o (TermC.parse thy)) fi'
23.45 + handle _ => raise ERROR ("prep_pbt: syntax raise ERROR in '#Find' of " ^ strs2str metID))
23.46 + | _ => raise ERROR ("prep_pbt: more than one '#Find' in " ^ strs2str metID));
23.47 + val fi = map (pair "#Find") fi;
23.48 +
23.49 + val re = filter (eq "#Relate") ppc;
23.50 + val re = (case re of
23.51 + [] => (writeln ("prep_input: in " ^ guh ^ " #Relate is empty ?!?"); [])
23.52 + | ((_,re') :: []) => (map (Problem.split_did o Thm.term_of o the o (TermC.parse thy)) re'
23.53 + handle _ => raise ERROR ("prep_pbt: syntax raise ERROR in '#Relate' of " ^ strs2str metID))
23.54 + | _ => raise ERROR ("prep_pbt: more than one '#Relate' in " ^ strs2str metID));
23.55 + val re = map (pair "#Relate") re;
23.56 +
23.57 + val wh = filter (eq "#Where") ppc;
23.58 + val wh = (case wh of
23.59 + [] => (writeln ("prep_input: in " ^ guh ^ " #Where is empty ?!?"); [])
23.60 + | ((_, wh') :: []) => (map (TermC.parse_patt thy) wh'
23.61 + handle _ => raise ERROR ("prep_pbt: syntax raise ERROR in '#Where' of " ^ strs2str metID))
23.62 + | _ => raise ERROR ("prep_pbt: more than one '#Where' in " ^ strs2str metID));
23.63 + val sc = Program.prep_program scr
23.64 + val calc = if Thm.eq_thm (scr, @{thm refl}) then [] else Auto_Prog.get_calcs thy sc
23.65 + in
23.66 + ({guh = guh, mathauthors = maa, init = init, ppc = gi @ fi @ re, pre = wh, rew_ord' = ro,
23.67 + erls = rls, srls = srls, prls = prls, calc = calc,
23.68 + crls = cr, errpats = ep, nrls = nr, scr = Rule.Prog sc}, metID)
23.69 + end;
23.70 +
23.71 +
23.72 +(** get Method from Store **)
23.73 +
23.74 (* TODO: throws exn 'get_pbt not found: ' ... confusing !! take 'ketype' as an argument *)
23.75 fun from_store metID = Store.get (get_mets ()) metID metID;
23.76 fun from_store' thy metID = Store.get (KEStore_Elems.get_mets thy) metID metID;
24.1 --- a/src/Tools/isac/MathEngBasic/problem.sml Wed May 13 12:14:49 2020 +0200
24.2 +++ b/src/Tools/isac/MathEngBasic/problem.sml Wed May 13 16:10:22 2020 +0200
24.3 @@ -12,6 +12,12 @@
24.4 val id_empty: id
24.5 val id_to_string: id -> string
24.6
24.7 + type input
24.8 + type model_input
24.9 + val split_did: term -> term * term
24.10 + (* TODO: ---------- remove always empty --- vvvvvvvvvvv -- vvv*)
24.11 + val prep_input : theory -> Check_Unique.id -> string list -> id -> input -> T * id
24.12 +
24.13 val from_store: id -> T
24.14 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
24.15 (*NONE*)
24.16 @@ -39,6 +45,71 @@
24.17 val id_empty = Probl_Def.id_empty;
24.18 val id_to_string = Probl_Def.id_to_string;
24.19
24.20 -fun from_store id = Store.get (get_ptyps ()) id (rev id)
24.21 +
24.22 +(** prepare Problem for Store **)
24.23 +
24.24 +type model_input = (Model_Pattern.m_field * TermC.as_string list) list;
24.25 +type input =
24.26 + id * (* the key into the problem hierarchy *)
24.27 + model_input * (* e.g. ("#Given", ["unsorted u_u"]) list *)
24.28 + Rule_Set.T * (* *)
24.29 + string option * (* CAS_Cmd *)
24.30 + Meth_Def.id list; (* methods that can solve the problem *)
24.31 +
24.32 +(* split a term into description and (id | structured variable) for pbt, met.ppc *)
24.33 +fun split_did t =
24.34 + let
24.35 + val (hd, arg) = case strip_comb t of
24.36 + (hd, [arg]) => (hd, arg)
24.37 + | _ => raise ERROR ("split_did: doesn't match (hd,[arg]) for t = " ^ UnparseC.term t)
24.38 + in (hd, arg) end
24.39 +
24.40 +(* prepare problem-types before storing in pbltypes;
24.41 + dont forget to "check_guh_unique" before ins *)
24.42 +fun prep_input thy guh maa init (pblID, dsc_dats, ev, ca, metIDs) =
24.43 + let
24.44 + fun eq f (f', _) = f = f';
24.45 + val gi = filter (eq "#Given") dsc_dats;
24.46 + val gi = (case gi of
24.47 + [] => []
24.48 + | ((_, gi') :: []) => (map (split_did o Thm.term_of o the o (TermC.parse thy)) gi'
24.49 + handle _ => raise ERROR ("prep_input: syntax raise ERROR in '#Given' of " ^ strs2str pblID))
24.50 + | _ => raise ERROR ("prep_input: more than one '#Given' in " ^ strs2str pblID));
24.51 + val gi = map (pair "#Given") gi;
24.52 +
24.53 + val fi = filter (eq "#Find") dsc_dats;
24.54 + val fi = (case fi of
24.55 + [] => []
24.56 + | ((_, fi') :: []) => (map (split_did o Thm.term_of o the o (TermC.parse thy)) fi'
24.57 + handle _ => raise ERROR ("prep_input: syntax raise ERROR in '#Find' of " ^ strs2str pblID))
24.58 + | _ => raise ERROR ("prep_input: more than one '#Find' in " ^ strs2str pblID));
24.59 + val fi = map (pair "#Find") fi;
24.60 +
24.61 + val re = filter (eq "#Relate") dsc_dats;
24.62 + val re = (case re of
24.63 + [] => []
24.64 + | ((_, re') :: []) => (map (split_did o Thm.term_of o the o (TermC.parse thy)) re'
24.65 + handle _ => raise ERROR ("prep_input: syntax raise ERROR in '#Relate' of " ^ strs2str pblID))
24.66 + | _ => raise ERROR ("prep_input: more than one '#Relate' in " ^ strs2str pblID));
24.67 + val re = map (pair "#Relate") re;
24.68 +
24.69 + val wh = filter (eq "#Where") dsc_dats;
24.70 + val wh = (case wh of
24.71 + [] => []
24.72 + | ((_, wh') :: []) => (map (TermC.parse_patt thy) wh'
24.73 + handle _ => raise ERROR ("prep_input: syntax raise ERROR in '#Where' of " ^ strs2str pblID))
24.74 + | _ => raise ERROR ("prep_input: more than one '#Where' in " ^ strs2str pblID));
24.75 + in
24.76 + ({guh = guh, mathauthors = maa, init = init, thy = thy,
24.77 + cas= case ca of
24.78 + NONE => NONE
24.79 + | SOME s => SOME ((Thm.term_of o the o (TermC.parse thy)) s),
24.80 + prls = ev, where_ = wh, ppc = gi @ fi @ re, met = metIDs}, pblID)
24.81 + end;
24.82 +
24.83 +
24.84 +(** get Method from Store **)
24.85 +
24.86 +fun from_store id = Store.get (get_ptyps ()) id (rev id);
24.87
24.88 (**)end(**)
25.1 --- a/src/Tools/isac/Specify/ptyps.sml Wed May 13 12:14:49 2020 +0200
25.2 +++ b/src/Tools/isac/Specify/ptyps.sml Wed May 13 16:10:22 2020 +0200
25.3 @@ -21,18 +21,10 @@
25.4 val kestoreID2guh : ketype -> kestoreID -> Check_Unique.id (* for datatypes.sml *)
25.5 val guh2kestoreID : Check_Unique.id -> string list (* for interface.sml *)
25.6
25.7 - val prep_pbt : theory -> Check_Unique.id -> string list -> Problem.id ->
25.8 - string list * (string * string list) list * Rule_Set.T * string option * Method.id list ->
25.9 - Problem.T * Problem.id
25.10 - val prep_met : theory -> string -> string list -> Problem.id ->
25.11 - string list * (string * string list) list *
25.12 - {calc: 'a, crls: Rule_Set.T, errpats: Error_Pattern_Def.T list, nrls: Rule_Set.T, prls: Rule_Set.T,
25.13 - rew_ord': Rewrite_Ord.rew_ord', rls': Rule_Set.T, srls: Rule_Set.T} * thm ->
25.14 - Method.T * Method.id
25.15 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
25.16 (*NONE*)
25.17 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
25.18 - val split_did: term -> term * term
25.19 + (*NONE*)
25.20 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
25.21
25.22 end
25.23 @@ -76,14 +68,6 @@
25.24 (*either ThyC.id or Problem.id or Method.id*)
25.25 type kestoreID = string list;
25.26
25.27 -(* split a term into description and (id | structured variable) for pbt, met.ppc *)
25.28 -fun split_did t =
25.29 - let
25.30 - val (hd, arg) = case strip_comb t of
25.31 - (hd, [arg]) => (hd, arg)
25.32 - | _ => raise ERROR ("split_did: doesn't match (hd,[arg]) for t = " ^ UnparseC.term t)
25.33 - in (hd, arg) end
25.34 -
25.35 (*create output-string for itm_*)
25.36 fun itm_out _ (I_Model.Cor ((d, ts), _)) = UnparseC.term (Input_Descript.join (d, ts))
25.37 | itm_out _ (I_Model.Syn c) = c
25.38 @@ -124,94 +108,6 @@
25.39 end
25.40 | _ => raise ERROR ("guh2kestoreID called with \"" ^ guh ^ "\":");
25.41
25.42 -(* prepare problem-types before storing in pbltypes;
25.43 - dont forget to "check_guh_unique" before ins *)
25.44 -fun prep_pbt thy guh maa init (pblID, dsc_dats, ev, ca, metIDs) =
25.45 - let
25.46 - fun eq f (f', _) = f = f';
25.47 - val gi = filter (eq "#Given") dsc_dats;
25.48 - val gi = (case gi of
25.49 - [] => []
25.50 - | ((_, gi') :: []) => (map (split_did o Thm.term_of o the o (TermC.parse thy)) gi'
25.51 - handle _ => raise ERROR ("prep_pbt: syntax raise ERROR in '#Given' of " ^ strs2str pblID))
25.52 - | _ => raise ERROR ("prep_pbt: more than one '#Given' in " ^ strs2str pblID));
25.53 - val gi = map (pair "#Given") gi;
25.54 -
25.55 - val fi = filter (eq "#Find") dsc_dats;
25.56 - val fi = (case fi of
25.57 - [] => []
25.58 - | ((_, fi') :: []) => (map (split_did o Thm.term_of o the o (TermC.parse thy)) fi'
25.59 - handle _ => raise ERROR ("prep_pbt: syntax raise ERROR in '#Find' of " ^ strs2str pblID))
25.60 - | _ => raise ERROR ("prep_pbt: more than one '#Find' in " ^ strs2str pblID));
25.61 - val fi = map (pair "#Find") fi;
25.62 -
25.63 - val re = filter (eq "#Relate") dsc_dats;
25.64 - val re = (case re of
25.65 - [] => []
25.66 - | ((_, re') :: []) => (map (split_did o Thm.term_of o the o (TermC.parse thy)) re'
25.67 - handle _ => raise ERROR ("prep_pbt: syntax raise ERROR in '#Relate' of " ^ strs2str pblID))
25.68 - | _ => raise ERROR ("prep_pbt: more than one '#Relate' in " ^ strs2str pblID));
25.69 - val re = map (pair "#Relate") re;
25.70 -
25.71 - val wh = filter (eq "#Where") dsc_dats;
25.72 - val wh = (case wh of
25.73 - [] => []
25.74 - | ((_, wh') :: []) => (map (TermC.parse_patt thy) wh'
25.75 - handle _ => raise ERROR ("prep_pbt: syntax raise ERROR in '#Where' of " ^ strs2str pblID))
25.76 - | _ => raise ERROR ("prep_pbt: more than one '#Where' in " ^ strs2str pblID));
25.77 - in
25.78 - ({guh = guh, mathauthors = maa, init = init, thy = thy,
25.79 - cas= case ca of
25.80 - NONE => NONE
25.81 - | SOME s => SOME ((Thm.term_of o the o (TermC.parse thy)) s),
25.82 - prls = ev, where_ = wh, ppc = gi @ fi @ re, met = metIDs}, pblID)
25.83 - end;
25.84 -
25.85 -(* prepare met for storage analogous to pbt *)
25.86 -fun prep_met thy guh maa init
25.87 - (metID, ppc,
25.88 - {rew_ord' = ro, rls' = rls, srls = srls, prls = prls, calc = _(*scr_isa_fns*), crls = cr,
25.89 - errpats = ep, nrls = nr}, scr) =
25.90 - let
25.91 - fun eq f (f', _) = f = f';
25.92 - val gi = filter (eq "#Given") ppc;
25.93 - val gi = (case gi of
25.94 - [] => (writeln ("prep_met: in " ^ guh ^ " #Given is empty ?!?"); [])
25.95 - | ((_, gi') :: []) => (map (split_did o Thm.term_of o the o (TermC.parse thy)) gi'
25.96 - handle _ => raise ERROR ("prep_pbt: syntax raise ERROR in '#Given' of " ^ strs2str metID))
25.97 - | _ => raise ERROR ("prep_pbt: more than one '#Given' in " ^ strs2str metID));
25.98 - val gi = map (pair "#Given") gi;
25.99 -
25.100 - val fi = filter (eq "#Find") ppc;
25.101 - val fi = (case fi of
25.102 - [] => (writeln ("prep_met: in " ^ guh ^ " #Find is empty ?!?"); [])
25.103 - | ((_, fi') :: []) => (map (split_did o Thm.term_of o the o (TermC.parse thy)) fi'
25.104 - handle _ => raise ERROR ("prep_pbt: syntax raise ERROR in '#Find' of " ^ strs2str metID))
25.105 - | _ => raise ERROR ("prep_pbt: more than one '#Find' in " ^ strs2str metID));
25.106 - val fi = map (pair "#Find") fi;
25.107 -
25.108 - val re = filter (eq "#Relate") ppc;
25.109 - val re = (case re of
25.110 - [] => (writeln ("prep_met: in " ^ guh ^ " #Relate is empty ?!?"); [])
25.111 - | ((_,re') :: []) => (map (split_did o Thm.term_of o the o (TermC.parse thy)) re'
25.112 - handle _ => raise ERROR ("prep_pbt: syntax raise ERROR in '#Relate' of " ^ strs2str metID))
25.113 - | _ => raise ERROR ("prep_pbt: more than one '#Relate' in " ^ strs2str metID));
25.114 - val re = map (pair "#Relate") re;
25.115 -
25.116 - val wh = filter (eq "#Where") ppc;
25.117 - val wh = (case wh of
25.118 - [] => (writeln ("prep_met: in " ^ guh ^ " #Where is empty ?!?"); [])
25.119 - | ((_, wh') :: []) => (map (TermC.parse_patt thy) wh'
25.120 - handle _ => raise ERROR ("prep_pbt: syntax raise ERROR in '#Where' of " ^ strs2str metID))
25.121 - | _ => raise ERROR ("prep_pbt: more than one '#Where' in " ^ strs2str metID));
25.122 - val sc = Program.prep_program scr
25.123 - val calc = if Thm.eq_thm (scr, @{thm refl}) then [] else Auto_Prog.get_calcs thy sc
25.124 - in
25.125 - ({guh = guh, mathauthors = maa, init = init, ppc = gi @ fi @ re, pre = wh, rew_ord' = ro,
25.126 - erls = rls, srls = srls, prls = prls, calc = calc,
25.127 - crls = cr, errpats = ep, nrls = nr, scr = Rule.Prog sc}, metID)
25.128 - end;
25.129 -
25.130 (* for distinction of contexts WN130621: disambiguate with Isabelle's Context *)
25.131 datatype ketype = Exp_ | Thy_ | Pbl_ | Met_;
25.132 fun ketype2str Exp_ = "Exp_"
26.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Wed May 13 12:14:49 2020 +0200
26.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Wed May 13 16:10:22 2020 +0200
26.3 @@ -883,8 +883,8 @@
26.4 \em Z\_Transform\normalfont.\<close>
26.5
26.6 setup \<open>KEStore_Elems.add_pbts
26.7 - [prep_pbt thy "pbl_SP" [] Problem.id_empty (["SignalProcessing"], [], Rule_Set.empty, NONE, []),
26.8 - prep_pbt thy "pbl_SP_Ztrans" [] Problem.id_empty
26.9 + [Problem.prep_input thy "pbl_SP" [] Problem.id_empty (["SignalProcessing"], [], Rule_Set.empty, NONE, []),
26.10 + Problem.prep_input thy "pbl_SP_Ztrans" [] Problem.id_empty
26.11 (["Z_Transform","SignalProcessing"], [], Rule_Set.empty, NONE, [])]\<close>
26.12
26.13 text\<open>\noindent For the suddenly created node we have to define the input
26.14 @@ -892,7 +892,7 @@
26.15 Section~\ref{sec:deffdes}.\<close>
26.16
26.17 setup \<open>KEStore_Elems.add_pbts
26.18 - [prep_pbt thy "pbl_SP_Ztrans_inv" [] Problem.id_empty
26.19 + [Problem.prep_input thy "pbl_SP_Ztrans_inv" [] Problem.id_empty
26.20 (["Inverse", "Z_Transform", "SignalProcessing"],
26.21 [("#Given" ,["filterExpression X_eq"]),
26.22 ("#Find", ["stepResponse n_eq"])],
26.23 @@ -921,12 +921,12 @@
26.24 as content.\<close>
26.25
26.26 setup \<open>KEStore_Elems.add_mets
26.27 - [prep_met thy "met_SP" [] e_metID
26.28 + [Method.prep_input thy "met_SP" [] e_metID
26.29 (["SignalProcessing"], [],
26.30 {rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty, crls = Rule_Set.empty,
26.31 errpats = [], nrls = Rule_Set.empty},
26.32 "empty_script"),
26.33 - prep_met thy "met_SP_Ztrans" [] e_metID
26.34 + Method.prep_input thy "met_SP_Ztrans" [] e_metID
26.35 (["SignalProcessing", "Z_Transform"], [],
26.36 {rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty, crls = Rule_Set.empty,
26.37 errpats = [], nrls = Rule_Set.empty},
26.38 @@ -938,7 +938,7 @@
26.39 of the script in e.g. the in- and output.\<close>
26.40
26.41 setup \<open>KEStore_Elems.add_mets
26.42 - [prep_met thy "met_SP_Ztrans_inv" [] e_metID
26.43 + [Method.prep_input thy "met_SP_Ztrans_inv" [] e_metID
26.44 (["SignalProcessing", "Z_Transform", "Inverse"],
26.45 [("#Given" ,["filterExpression X_eq", "boundVariable X_z"]),
26.46 ("#Find", ["stepResponse n_eq"])],
26.47 @@ -952,7 +952,7 @@
26.48 simple operation.\<close>
26.49
26.50 setup \<open>KEStore_Elems.add_mets
26.51 - [prep_met thy "met_SP_Ztrans_inv" [] e_metID
26.52 + [Method.prep_input thy "met_SP_Ztrans_inv" [] e_metID
26.53 (["SignalProcessing", "Z_Transform", "Inverse"],
26.54 [("#Given" , ["filterExpression X_eq", "boundVariable X_z"]),
26.55 ("#Find", ["stepResponse n_eq"])],
26.56 @@ -1122,7 +1122,7 @@
26.57 subversion.\<close>
26.58
26.59 setup \<open>KEStore_Elems.add_mets
26.60 - [prep_met thy "met_SP_Ztrans_inv" [] e_metID
26.61 + [Method.prep_input thy "met_SP_Ztrans_inv" [] e_metID
26.62 (["SignalProcessing", "Z_Transform", "Inverse"],
26.63 [("#Given" , ["filterExpression X_eq"]), (*TODO boundVariable X_z*)
26.64 ("#Find", ["stepResponse n_eq"])],
27.1 --- a/test/Tools/isac/ADDTESTS/course/phst11/T3_MathEngine.thy Wed May 13 12:14:49 2020 +0200
27.2 +++ b/test/Tools/isac/ADDTESTS/course/phst11/T3_MathEngine.thy Wed May 13 16:10:22 2020 +0200
27.3 @@ -42,7 +42,7 @@
27.4 'get_met' gets the one we need:
27.5 \<close>
27.6 ML \<open>
27.7 -Specify.show_mets ();
27.8 +Test_Tool.show_mets ();
27.9 Method.from_store ["simplification","for_polynomials","with_minus"];
27.10 \<close>
27.11 text \<open>For a readable format of the method look up the definition in
28.1 --- a/test/Tools/isac/BaseDefinitions/termC.sml Wed May 13 12:14:49 2020 +0200
28.2 +++ b/test/Tools/isac/BaseDefinitions/termC.sml Wed May 13 16:10:22 2020 +0200
28.3 @@ -14,7 +14,7 @@
28.4 "----------- fun parse, fun parse_patt, fun T_a2real -------------------------------------------";
28.5 "----------- fun vars_of -----------------------------------------------------------------------";
28.6 "----------- uminus_to_string ---------------------------";
28.7 -"----------- *** prep_pbt: syntax error in '#Where' of [v";
28.8 +"----------- *** Problem.prep_input: syntax error in '#Where' of [v";
28.9 "----------- check writeln, tracing for string markup ---";
28.10 "----------- build fun is_bdv_subst ------------------------------------------------------------";
28.11 "----------- fun str_of_int --------------------------------------------------------------------";
28.12 @@ -440,9 +440,9 @@
28.13 then ()
28.14 else error "termC.sml diff.behav. in uminus_to_string";
28.15
28.16 -"----------- *** prep_pbt: syntax error in '#Where' of [v";
28.17 -"----------- *** prep_pbt: syntax error in '#Where' of [v";
28.18 -"----------- *** prep_pbt: syntax error in '#Where' of [v";
28.19 +"----------- *** Problem.prep_input: syntax error in '#Where' of [v";
28.20 +"----------- *** Problem.prep_input: syntax error in '#Where' of [v";
28.21 +"----------- *** Problem.prep_input: syntax error in '#Where' of [v";
28.22 "===== deconstruct datatype typ ===";
28.23 val str = "?a";
28.24 val t = (thy, str) |>> ThyC.to_ctxt
29.1 --- a/test/Tools/isac/Knowledge/eqsystem.sml Wed May 13 12:14:49 2020 +0200
29.2 +++ b/test/Tools/isac/Knowledge/eqsystem.sml Wed May 13 16:10:22 2020 +0200
29.3 @@ -436,7 +436,7 @@
29.4 val it = "length_ (es_::real list) = (2::real)" : string
29.5
29.6 =========================================================================\
29.7 --------fun prep_pbt
29.8 +-------fun Problem.prep_input
29.9 (* val (thy, (pblID, dsc_dats: (string * (string list)) list,
29.10 ev:rls, ca: string option, metIDs:metID list)) =
29.11 (EqSystem.thy, (["system"],
30.1 --- a/test/Tools/isac/Knowledge/integrate.thy Wed May 13 12:14:49 2020 +0200
30.2 +++ b/test/Tools/isac/Knowledge/integrate.thy Wed May 13 16:10:22 2020 +0200
30.3 @@ -15,7 +15,7 @@
30.4 (Rewrite_Set_Inst [(''bdv'',v_v)] ''add_new_c'') #>
30.5 (Rewrite_Set_Inst [(''bdv'',v_v)] ''simplify_Integral'')) (f_f::real))"
30.6 setup \<open>KEStore_Elems.add_mets
30.7 - [Specify.prep_met @{theory "Isac_Knowledge"} "met_testint" [] Method.id_empty
30.8 + [Method.prep_input @{theory "Isac_Knowledge"} "met_testint" [] Method.id_empty
30.9 (["diff","integration","test"],
30.10 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]), ("#Find", ["antiDerivative F_F"])],
30.11 {rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty,
31.1 --- a/test/Tools/isac/Knowledge/polyminus.sml Wed May 13 12:14:49 2020 +0200
31.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml Wed May 13 16:10:22 2020 +0200
31.3 @@ -22,7 +22,7 @@
31.4 "----------- pbl binom polynom vereinfachen p.39 --------";
31.5 "----------- pbl binom polynom vereinfachen: cube -------";
31.6 "----------- Refine.refine Vereinfache -------------------------";
31.7 -"----------- *** prep_pbt: syntax error in '#Where' of [v";
31.8 +"----------- *** Problem.prep_input: syntax error in '#Where' of [v";
31.9 "--------------------------------------------------------";
31.10 "--------------------------------------------------------";
31.11 "--------------------------------------------------------";
31.12 @@ -593,9 +593,9 @@
31.13 if UnparseC.term t' = "False" then ()
31.14 else error "polyminus.sml Not (matchsub (?a * (?b + ?c)) (8 ...";
31.15
31.16 -"----------- *** prep_pbt: syntax error in '#Where' of [v";
31.17 -"----------- *** prep_pbt: syntax error in '#Where' of [v";
31.18 -"----------- *** prep_pbt: syntax error in '#Where' of [v";
31.19 +"----------- *** Problem.prep_input: syntax error in '#Where' of [v";
31.20 +"----------- *** Problem.prep_input: syntax error in '#Where' of [v";
31.21 +"----------- *** Problem.prep_input: syntax error in '#Where' of [v";
31.22 (*see test/../termC.sml for details*)
31.23 val t = parse_patt thy "t_t is_polyexp";
31.24 val t = parse_patt thy ("Not (matchsub (?a + (?b + ?c)) t_t | " ^
32.1 --- a/test/Tools/isac/OLDTESTS/script_if.sml Wed May 13 12:14:49 2020 +0200
32.2 +++ b/test/Tools/isac/OLDTESTS/script_if.sml Wed May 13 16:10:22 2020 +0200
32.3 @@ -56,7 +56,7 @@
32.4 siehe unten. Wir werden w"ahrend der Arbeit auf diesen Fehler drauskommen*)
32.5
32.6 KEStore_Elems.add_pbts
32.7 - [prep_pbt (*Test.thy*) (theory "Isac_Knowledge")
32.8 + [Problem.prep_input (*Test.thy*) (theory "Isac_Knowledge")
32.9 (["rootX","univariate","equation","test"],
32.10 [("#Given" ,["equality e_e","solveFor v_v"]),
32.11 ("#Where" ,["is_rootequation_in (e_e::bool) (v_::real)"]),
32.12 @@ -68,7 +68,7 @@
32.13 Model.match_pbl ["equality (sqrt(x)=1)","solveFor x","solutions L"] (Problem.from_store ["rootX","univariate","equation","test"]);
32.14
32.15 KEStore_Elems.add_pbts
32.16 - [prep_pbt (theory "Isac_Knowledge")
32.17 + [Problem.prep_input (theory "Isac_Knowledge")
32.18 (["approximate","univariate","equation","test"],
32.19 [("#Given", ["equality e_e","solveFor v_v","errorBound err_"]),
32.20 ("#Where", ["matches (?a = ?b) e_e"]),
32.21 @@ -78,7 +78,7 @@
32.22
32.23 methods:= overwritel (!methods,
32.24 [
32.25 - prep_met
32.26 + Method.prep_input
32.27 (("Isac_Knowledge","solve_univar_err"):metID,
32.28 [("#Given" ,["equality e_e","solveFor v_v","errorBound err_"]),
32.29 ("#Find" ,["solutions v_i_"])
33.1 --- a/test/Tools/isac/OLDTESTS/scriptnew.sml Wed May 13 12:14:49 2020 +0200
33.2 +++ b/test/Tools/isac/OLDTESTS/scriptnew.sml Wed May 13 16:10:22 2020 +0200
33.3 @@ -20,9 +20,9 @@
33.4 " --- test 30.4.02 Testterm: Repeat Repeat Or ------------------ ";
33.5 " --- test 30.4.02 Testterm: Repeat Repeat Or ------------------ ";
33.6 KEStore_Elems.add_pbts
33.7 - [prep_pbt Test.thy "pbl_testss" [] Problem.id_empty
33.8 + [Problem.prep_input Test.thy "pbl_testss" [] Problem.id_empty
33.9 (["tests"], []:(string * string list) list, Rule_Set.empty, NONE, []),
33.10 - prep_pbt Test.thy "pbl_testss_term" [] Problem.id_empty
33.11 + Problem.prep_input Test.thy "pbl_testss_term" [] Problem.id_empty
33.12 (["met_testterm","tests"],
33.13 [("#Given" ,["realTestGiven g_"]),
33.14 ("#Find" ,["realTestFind f_"])],
33.15 @@ -30,7 +30,7 @@
33.16 thy;
33.17
33.18 store_met
33.19 - (prep_met Test.thy "met_test_simp" [] e_metID
33.20 + (Method.prep_input Test.thy "met_test_simp" [] e_metID
33.21 (*test for simplification*)
33.22 (["Test","met_testterm"]:metID,
33.23 [("#Given" ,["realTestGiven g_"]),
33.24 @@ -87,7 +87,7 @@
33.25 " --- test 9.5.02 Testeq: While Try Repeat #> ------------------ ";
33.26 " --- test 9.5.02 Testeq: While Try Repeat #> ------------------ ";
33.27 KEStore_Elems.add_pbts
33.28 - [prep_pbt Test.thy "pbl_testss_eq" [] Problem.id_empty
33.29 + [Problem.prep_input Test.thy "pbl_testss_eq" [] Problem.id_empty
33.30 (["met_testeq","tests"],
33.31 [("#Given" ,["boolTestGiven e_e"]),
33.32 ("#Find" ,["boolTestFind v_i_"])],
33.33 @@ -95,7 +95,7 @@
33.34 thy;
33.35
33.36 store_met
33.37 - (prep_met Test.thy "met_test_eq1" [] e_metID
33.38 + (Method.prep_input Test.thy "met_test_eq1" [] e_metID
33.39 (["Test","testeq1"]:metID,
33.40 [("#Given",["boolTestGiven e_e"]),
33.41 ("#Where" ,[]),
33.42 @@ -150,7 +150,7 @@
33.43 " --- test 11.5.02 Testeq: let e_e =... in [e_] --------- ";
33.44 " --- test 11.5.02 Testeq: let e_e =... in [e_] --------- ";
33.45 store_met
33.46 - (prep_met Test.thy "met_test_let" [] e_metID
33.47 + (Method.prep_input Test.thy "met_test_let" [] e_metID
33.48 (["Test","testlet"]:metID,
33.49 [("#Given",["boolTestGiven e_e"]),
33.50 ("#Where" ,[]),
34.1 --- a/test/Tools/isac/ProgLang/calculate.thy Wed May 13 12:14:49 2020 +0200
34.2 +++ b/test/Tools/isac/ProgLang/calculate.thy Wed May 13 16:10:22 2020 +0200
34.3 @@ -18,8 +18,8 @@
34.4 \<close>
34.5
34.6 setup \<open>KEStore_Elems.add_pbts
34.7 - [Specify.prep_pbt @{theory "Test"} "pbl_ttest" [] Problem.id_empty (["test"], [], Rule_Set.empty, NONE, []),
34.8 - Specify.prep_pbt @{theory "Test"} "pbl_ttest_calc" [] Problem.id_empty
34.9 + [Problem.prep_input @{theory "Test"} "pbl_ttest" [] Problem.id_empty (["test"], [], Rule_Set.empty, NONE, []),
34.10 + Problem.prep_input @{theory "Test"} "pbl_ttest_calc" [] Problem.id_empty
34.11 (["calculate", "test"],
34.12 [("#Given", ["realTestGiven t_t"]),
34.13 ("#Find", ["realTestFind s_s"])],
34.14 @@ -34,7 +34,7 @@
34.15 (Try (Repeat (Calculate ''DIVIDE''))) #>
34.16 (Try (Repeat (Calculate ''POWER''))))) t_t"
34.17 setup \<open>KEStore_Elems.add_mets
34.18 - [Specify.prep_met (@{theory "Test"}) "met_testcal" [] Method.id_empty
34.19 + [Method.prep_input (@{theory "Test"}) "met_testcal" [] Method.id_empty
34.20 (["Test","test_calculate"],
34.21 [("#Given" , ["realTestGiven t_t"]), ("#Find", ["realTestFind s_s"])],
34.22 {rew_ord'="sqrt_right",rls'=tval_rls,srls = Rule_Set.empty, prls = Rule_Set.empty,
35.1 --- a/test/Tools/isac/Specify/refine.thy Wed May 13 12:14:49 2020 +0200
35.2 +++ b/test/Tools/isac/Specify/refine.thy Wed May 13 16:10:22 2020 +0200
35.3 @@ -14,30 +14,30 @@
35.4
35.5 section \<open>data for test "-ptyps.thy: store test-pbtyps by 'setup' ---"\<close>
35.6 setup \<open>KEStore_Elems.add_pbts
35.7 -[(Specify.prep_pbt thy "pbl_test_refine" [] Problem.id_empty
35.8 +[(Problem.prep_input thy "pbl_test_refine" [] Problem.id_empty
35.9 (["refine", "test"], [], Rule_Set.empty, NONE, [])),
35.10 -(Specify.prep_pbt @{theory DiffApp} "pbl_pbla" [] Problem.id_empty
35.11 +(Problem.prep_input @{theory DiffApp} "pbl_pbla" [] Problem.id_empty
35.12 (["pbla", "refine", "test"],
35.13 [("#Given", ["fixedValues a_a"])], Rule_Set.empty, NONE, [])),
35.14 -(Specify.prep_pbt @{theory DiffApp} "pbl_pbla1" [] Problem.id_empty
35.15 +(Problem.prep_input @{theory DiffApp} "pbl_pbla1" [] Problem.id_empty
35.16 (["pbla1","pbla", "refine", "test"],
35.17 [("#Given", ["fixedValues a_a","maximum a_1"])], Rule_Set.empty, NONE, [])),
35.18 -(Specify.prep_pbt @{theory DiffApp} "pbl_pbla2" [] Problem.id_empty
35.19 +(Problem.prep_input @{theory DiffApp} "pbl_pbla2" [] Problem.id_empty
35.20 (["pbla2","pbla", "refine", "test"],
35.21 [("#Given", ["fixedValues a_a","valuesFor a_2"])], Rule_Set.empty, NONE, [])),
35.22 -(Specify.prep_pbt @{theory DiffApp} "pbl_pbla2x" [] Problem.id_empty
35.23 +(Problem.prep_input @{theory DiffApp} "pbl_pbla2x" [] Problem.id_empty
35.24 (["pbla2x","pbla2","pbla", "refine", "test"],
35.25 [("#Given", ["fixedValues a_a","valuesFor a_2","functionOf a2_x"])],
35.26 Rule_Set.empty, NONE, [])),
35.27 -(Specify.prep_pbt @{theory DiffApp} "pbl_pbla2y" [] Problem.id_empty
35.28 +(Problem.prep_input @{theory DiffApp} "pbl_pbla2y" [] Problem.id_empty
35.29 (["pbla2y","pbla2","pbla", "refine", "test"],
35.30 [("#Given" ,["fixedValues a_a","valuesFor a_2","boundVariable a2_y"])],
35.31 Rule_Set.empty, NONE, [])),
35.32 -(Specify.prep_pbt @{theory DiffApp} "pbl_pbla2z" [] Problem.id_empty
35.33 +(Problem.prep_input @{theory DiffApp} "pbl_pbla2z" [] Problem.id_empty
35.34 (["pbla2z","pbla2","pbla", "refine", "test"],
35.35 [("#Given" ,["fixedValues a_a","valuesFor a_2","interval a2_z"])],
35.36 Rule_Set.empty, NONE, [])),
35.37 -(Specify.prep_pbt @{theory DiffApp} "pbl_pbla3" [] Problem.id_empty
35.38 +(Problem.prep_input @{theory DiffApp} "pbl_pbla3" [] Problem.id_empty
35.39 (["pbla3","pbla", "refine", "test"],
35.40 [("#Given" ,["fixedValues a_a","relations a_3"])],
35.41 Rule_Set.empty, NONE, []))]