Isar command 'problem' as combination of KEStore_Elems.add_pbts + Problem.prep_import, without change of semantics;
1.1 --- a/src/Tools/isac/Knowledge/AlgEin.thy Sun Jun 20 12:45:03 2021 +0200
1.2 +++ b/src/Tools/isac/Knowledge/AlgEin.thy Sun Jun 20 16:26:18 2021 +0200
1.3 @@ -20,15 +20,14 @@
1.4 unten :: real
1.5
1.6 (** problems **)
1.7 -setup \<open>KEStore_Elems.add_pbts
1.8 - [(Problem.prep_input @{theory} "pbl_algein" [] Problem.id_empty (["Berechnung"], [], Rule_Set.empty, NONE, [])),
1.9 - (Problem.prep_input @{theory} "pbl_algein_numsym" [] Problem.id_empty
1.10 - (["numerischSymbolische", "Berechnung"],
1.11 - [("#Given",
1.12 - ["KantenLaenge k_k", "Querschnitt q__q"(*q_ in Biegelinie.thy*), "KantenUnten u_u",
1.13 - "KantenSenkrecht s_s", "KantenOben o_o"]),
1.14 - ("#Find", ["GesamtLaenge l_l"])],
1.15 - Rule_Set.empty, NONE, [["Berechnung", "erstNumerisch"], ["Berechnung", "erstSymbolisch"]]))]\<close>
1.16 +
1.17 +problem pbl_algein : "Berechnung" = \<open>Rule_Set.empty\<close>
1.18 +
1.19 +problem pbl_algein_numsym : "numerischSymbolische/Berechnung" = \<open>Rule_Set.empty\<close>
1.20 + Method: "Berechnung/erstNumerisch" "Berechnung/erstSymbolisch"
1.21 + Given: "KantenLaenge k_k" "Querschnitt q__q" (*q_ in Biegelinie.thy*) "KantenUnten u_u"
1.22 + "KantenSenkrecht s_s" "KantenOben o_o"
1.23 + Find: "GesamtLaenge l_l"
1.24
1.25 method met_algein : "Berechnung" =
1.26 \<open>{rew_ord'="tless_true", rls'= Rule_Set.Empty, calc = [], srls = Rule_Set.Empty, prls = Rule_Set.Empty, crls =Rule_Set.Empty,
2.1 --- a/src/Tools/isac/Knowledge/Biegelinie.thy Sun Jun 20 12:45:03 2021 +0200
2.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy Sun Jun 20 16:26:18 2021 +0200
2.3 @@ -102,46 +102,52 @@
2.4
2.5 section \<open>Problems\<close>
2.6
2.7 -setup \<open>KEStore_Elems.add_pbts
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 - (Problem.prep_input @{theory} "pbl_bieg_mom" [] Problem.id_empty
2.16 - (["MomentBestimmte", "Biegelinien"],
2.17 - [("#Given" ,["Traegerlaenge l_l", "Streckenlast q_q"]),
2.18 - (*("#Where",["0 < l_l"]), ...wait for < and handling Arbfix*)
2.19 - ("#Find" ,["Biegelinie b_b"]),
2.20 - ("#Relate",["RandbedingungenBiegung r_b", "RandbedingungenMoment r_m"])
2.21 - ],
2.22 - Rule_Set.append_rules "empty" Rule_Set.empty [], NONE, [["IntegrierenUndKonstanteBestimmen"]])),
2.23 - (Problem.prep_input @{theory} "pbl_bieg_momg" [] Problem.id_empty
2.24 - (["MomentGegebene", "Biegelinien"], [], Rule_Set.append_rules "empty" Rule_Set.empty [], NONE,
2.25 - [["IntegrierenUndKonstanteBestimmen", "2xIntegrieren"]])),
2.26 - (Problem.prep_input @{theory} "pbl_bieg_einf" [] Problem.id_empty
2.27 - (["einfache", "Biegelinien"], [], Rule_Set.append_rules "empty" Rule_Set.empty [], NONE,
2.28 - [["IntegrierenUndKonstanteBestimmen", "4x4System"]])),
2.29 - (Problem.prep_input @{theory} "pbl_bieg_momquer" [] Problem.id_empty
2.30 - (["QuerkraftUndMomentBestimmte", "Biegelinien"], [], Rule_Set.append_rules "empty" Rule_Set.empty [], NONE,
2.31 - [["IntegrierenUndKonstanteBestimmen", "1xIntegrieren"]])),
2.32 - (Problem.prep_input @{theory} "pbl_bieg_vonq" [] Problem.id_empty
2.33 - (["vonBelastungZu", "Biegelinien"],
2.34 - [("#Given" ,["Streckenlast q_q", "FunktionsVariable v_v"]),
2.35 - ("#Find" ,["Funktionen funs'''"])],
2.36 - Rule_Set.append_rules "empty" Rule_Set.empty [], NONE, [["Biegelinien", "ausBelastung"]])),
2.37 - (Problem.prep_input @{theory} "pbl_bieg_randbed" [] Problem.id_empty
2.38 - (["setzeRandbedingungen", "Biegelinien"],
2.39 - [("#Given" ,["Funktionen fun_s", "Randbedingungen r_b"]),
2.40 - ("#Find" ,["Gleichungen equs'''"])],
2.41 - Rule_Set.append_rules "empty" Rule_Set.empty [], NONE, [["Biegelinien", "setzeRandbedingungenEin"]])),
2.42 - (Problem.prep_input @{theory} "pbl_equ_fromfun" [] Problem.id_empty
2.43 - (["makeFunctionTo", "equation"],
2.44 - [("#Given" ,["functionEq fu_n", "substitution su_b"]),
2.45 - ("#Find" ,["equality equ'''"])],
2.46 - Rule_Set.append_rules "empty" Rule_Set.empty [], NONE, [["Equation", "fromFunction"]]))]\<close>
2.47 +problem pbl_bieg : "Biegelinien" =
2.48 + \<open>Rule_Set.append_rules "empty" Rule_Set.empty []\<close>
2.49 + Method: "IntegrierenUndKonstanteBestimmen2"
2.50 + Given: "Traegerlaenge l_l" "Streckenlast q_q"
2.51 + (* Where: "0 < l_l" ...wait for < and handling Arbfix*)
2.52 + Find: "Biegelinie b_b"
2.53 + Relate: "Randbedingungen r_b"
2.54 +
2.55 +problem pbl_bieg_mom : "MomentBestimmte/Biegelinien" =
2.56 + \<open>Rule_Set.append_rules "empty" Rule_Set.empty []\<close>
2.57 + Method: "IntegrierenUndKonstanteBestimmen"
2.58 + Given: "Traegerlaenge l_l" "Streckenlast q_q"
2.59 + (* Where: "0 < l_l" ...wait for < and handling Arbfix*)
2.60 + Find: "Biegelinie b_b"
2.61 + Relate: "RandbedingungenBiegung r_b" "RandbedingungenMoment r_m"
2.62 +
2.63 +problem pbl_bieg_momg : "MomentGegebene/Biegelinien" =
2.64 + \<open>Rule_Set.append_rules "empty" Rule_Set.empty []\<close>
2.65 + Method: "IntegrierenUndKonstanteBestimmen/2xIntegrieren"
2.66 +
2.67 +problem pbl_bieg_einf : "einfache/Biegelinien" =
2.68 + \<open>Rule_Set.append_rules "empty" Rule_Set.empty []\<close>
2.69 + Method: "IntegrierenUndKonstanteBestimmen/4x4System"
2.70 +
2.71 +problem pbl_bieg_momquer : "QuerkraftUndMomentBestimmte/Biegelinien" =
2.72 + \<open>Rule_Set.append_rules "empty" Rule_Set.empty []\<close>
2.73 + Method: "IntegrierenUndKonstanteBestimmen/1xIntegrieren"
2.74 +
2.75 +problem pbl_bieg_vonq : "vonBelastungZu/Biegelinien" =
2.76 + \<open>Rule_Set.append_rules "empty" Rule_Set.empty []\<close>
2.77 + Method: "Biegelinien/ausBelastung"
2.78 + Given: "Streckenlast q_q" "FunktionsVariable v_v"
2.79 + Find: "Funktionen funs'''"
2.80 +
2.81 +problem pbl_bieg_randbed : "setzeRandbedingungen/Biegelinien" =
2.82 + \<open>Rule_Set.append_rules "empty" Rule_Set.empty []\<close>
2.83 + Method: "Biegelinien/setzeRandbedingungenEin"
2.84 + Given: "Funktionen fun_s" "Randbedingungen r_b"
2.85 + Find: "Gleichungen equs'''"
2.86 +
2.87 +problem pbl_equ_fromfun : "makeFunctionTo/equation" =
2.88 + \<open>Rule_Set.append_rules "empty" Rule_Set.empty []\<close>
2.89 + Method: "Equation/fromFunction"
2.90 + Given: "functionEq fu_n" "substitution su_b"
2.91 + Find: "equality equ'''"
2.92 +
2.93 ML \<open>
2.94 (** methods **)
2.95
3.1 --- a/src/Tools/isac/Knowledge/Diff.thy Sun Jun 20 12:45:03 2021 +0200
3.2 +++ b/src/Tools/isac/Knowledge/Diff.thy Sun Jun 20 16:26:18 2021 +0200
3.3 @@ -235,24 +235,25 @@
3.4 diff_conv = \<open>prep_rls' diff_conv\<close> and
3.5 diff_sym_conv = \<open>prep_rls' diff_sym_conv\<close>
3.6
3.7 -(** problem types **)
3.8 -setup \<open>KEStore_Elems.add_pbts
3.9 - [(Problem.prep_input @{theory} "pbl_fun" [] Problem.id_empty (["function"], [], Rule_Set.empty, NONE, [])),
3.10 - (Problem.prep_input @{theory} "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 - Rule_Set.append_rules "empty" Rule_Set.empty [],
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 - (Problem.prep_input @{theory} "pbl_fun_deriv_nam" [] Problem.id_empty
3.19 - (["named", "derivative_of", "function"],
3.20 - [("#Given" ,["functionEq f_f", "differentiateFor v_v"]),
3.21 - ("#Find" ,["derivativeEq f_f'"])],
3.22 - Rule_Set.append_rules "empty" Rule_Set.empty [],
3.23 - SOME "Differentiate (f_f, v_v)",
3.24 - [["diff", "differentiate_equality"]]))]\<close>
3.25 +
3.26 +(** problems **)
3.27 +
3.28 +problem pbl_fun : "function" = \<open>Rule_Set.empty\<close>
3.29 +
3.30 +problem pbl_fun_deriv : "derivative_of/function" =
3.31 + \<open>Rule_Set.append_rules "empty" Rule_Set.empty []\<close>
3.32 + Method: "diff/differentiate_on_R" "diff/after_simplification"
3.33 + CAS: "Diff (f_f, v_v)"
3.34 + Given: "functionTerm f_f" "differentiateFor v_v"
3.35 + Find: "derivative f_f'"
3.36 +
3.37 +problem pbl_fun_deriv_nam :
3.38 + "named/derivative_of/function" (*here "named" is used differently from Integration"*) =
3.39 + \<open>Rule_Set.append_rules "empty" Rule_Set.empty []\<close>
3.40 + Method: "diff/differentiate_equality"
3.41 + CAS: "Differentiate (f_f, v_v)"
3.42 + Given: "functionEq f_f" "differentiateFor v_v"
3.43 + Find: "derivativeEq f_f'"
3.44
3.45 ML \<open>
3.46 (** CAS-commands **)
4.1 --- a/src/Tools/isac/Knowledge/DiffApp.thy Sun Jun 20 12:45:03 2021 +0200
4.2 +++ b/src/Tools/isac/Knowledge/DiffApp.thy Sun Jun 20 16:26:18 2021 +0200
4.3 @@ -59,44 +59,46 @@
4.4 \<close>
4.5 rule_set_knowledge eval_rls = \<open>eval_rls\<close>
4.6
4.7 -(** problem types **)
4.8 -setup \<open>KEStore_Elems.add_pbts
4.9 - [(Problem.prep_input @{theory} "pbl_fun_max" [] Problem.id_empty
4.10 - (["maximum_of", "function"],
4.11 - [("#Given" ,["fixedValues f_ix"]),
4.12 - ("#Find" ,["maximum m_m", "valuesFor v_s"]),
4.13 - ("#Relate",["relations r_s"])],
4.14 - Rule_Set.empty, NONE, [])),
4.15 - (Problem.prep_input @{theory} "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 - (Problem.prep_input @{theory} "pbl_fun_max_expl" [] Problem.id_empty
4.21 - (["by_explicit", "make", "function"],
4.22 - [("#Given" ,["functionOf f_f", "boundVariable v_v", "equalities eqs"]),
4.23 - ("#Find" ,["functionEq f_1"])],
4.24 - Rule_Set.empty, NONE, [["DiffApp", "make_fun_by_explicit"]])),
4.25 - (Problem.prep_input @{theory} "pbl_fun_max_newvar" [] Problem.id_empty
4.26 - (["by_new_variable", "make", "function"],
4.27 - [("#Given" ,["functionOf f_f", "boundVariable v_v", "equalities eqs"]),
4.28 - (*WN.12.5.03: precond for distinction still missing*)
4.29 - ("#Find" ,["functionEq f_1"])],
4.30 - Rule_Set.empty, NONE, [["DiffApp", "make_fun_by_new_variable"]])),
4.31 - (Problem.prep_input @{theory} "pbl_fun_max_interv" [] Problem.id_empty
4.32 - (["on_interval", "maximum_of", "function"],
4.33 - [("#Given" ,["functionEq t_t", "boundVariable v_v", "interval i_tv"]),
4.34 - (*WN.12.5.03: precond for distinction still missing*)
4.35 - ("#Find" ,["maxArgument v_0"])],
4.36 - Rule_Set.empty, NONE, [])),
4.37 - (Problem.prep_input @{theory} "pbl_tool" [] Problem.id_empty
4.38 - (["tool"], [], Rule_Set.empty, NONE, [])),
4.39 - (Problem.prep_input @{theory} "pbl_tool_findvals" [] Problem.id_empty
4.40 - (["find_values", "tool"],
4.41 - [("#Given" ,["maxArgument m_ax", "functionEq f_f", "boundVariable v_v"]),
4.42 - ("#Find" ,["valuesFor v_ls"]),
4.43 - ("#Relate",["additionalRels r_s"])],
4.44 - Rule_Set.empty, NONE, []))]\<close>
4.45 +(** problems **)
4.46 +
4.47 +problem pbl_fun_max : "maximum_of/function" =
4.48 + \<open>Rule_Set.empty\<close>
4.49 + Given: "fixedValues f_ix"
4.50 + Find: "maximum m_m" "valuesFor v_s"
4.51 + Relate: "relations r_s"
4.52 +
4.53 +problem pbl_fun_make : "make/function" =
4.54 + \<open>Rule_Set.empty\<close>
4.55 + Given: "functionOf f_f" "boundVariable v_v" "equalities eqs"
4.56 + Find: "functionEq f_1"
4.57 +
4.58 +problem pbl_fun_max_expl : "by_explicit/make/function" =
4.59 + \<open>Rule_Set.empty\<close>
4.60 + Method: "DiffApp/make_fun_by_explicit"
4.61 + Given: "functionOf f_f" "boundVariable v_v" "equalities eqs"
4.62 + Find: "functionEq f_1"
4.63 +
4.64 +problem pbl_fun_max_newvar : "by_new_variable/make/function" =
4.65 + \<open>Rule_Set.empty\<close>
4.66 + Method: "DiffApp/make_fun_by_new_variable"
4.67 + Given: "functionOf f_f" "boundVariable v_v" "equalities eqs"
4.68 + (*WN.12.5.03: precond for distinction still missing*)
4.69 + Find: "functionEq f_1"
4.70 +
4.71 +problem pbl_fun_max_interv : "on_interval/maximum_of/function" =
4.72 + \<open>Rule_Set.empty\<close>
4.73 + Given: "functionEq t_t" "boundVariable v_v" "interval i_tv"
4.74 + (*WN.12.5.03: precond for distinction still missing*)
4.75 + Find: "maxArgument v_0"
4.76 +
4.77 +problem pbl_tool : "tool" =
4.78 + \<open>Rule_Set.empty\<close>
4.79 +
4.80 +problem pbl_tool_findvals : "find_values/tool" =
4.81 + \<open>Rule_Set.empty\<close>
4.82 + Given: "maxArgument m_ax" "functionEq f_f" "boundVariable v_v"
4.83 + Find: "valuesFor v_ls"
4.84 + Relate: "additionalRels r_s"
4.85
4.86
4.87 (** methods, scripts not yet implemented **)
5.1 --- a/src/Tools/isac/Knowledge/DiophantEq.thy Sun Jun 20 12:45:03 2021 +0200
5.2 +++ b/src/Tools/isac/Knowledge/DiophantEq.thy Sun Jun 20 16:26:18 2021 +0200
5.3 @@ -12,14 +12,15 @@
5.4 int_isolate_add: "(bdv + a = b) = (bdv = b + (-1)*(a::int))"
5.5
5.6 text \<open>problemclass for the usecase\<close>
5.7 -setup \<open>KEStore_Elems.add_pbts
5.8 - [(Problem.prep_input @{theory} "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 - ("#Where" ,[]),
5.13 - ("#Find" ,["boolTestFind s_s"])],
5.14 - Rule_Set.empty, SOME "solve (e_e::bool, v_v::int)", [["LinEq", "solve_lineq_equation"]]))]\<close>
5.15 +
5.16 +problem pbl_equ_dio : "diophantine/equation" =
5.17 + \<open>Rule_Set.empty\<close>
5.18 + Method: "LinEq/solve_lineq_equation"
5.19 + CAS: "solve (e_e::bool, v_v::int)"
5.20 + Given: "boolTestGiven e_e" "intTestGiven (v_v::int)"
5.21 + (* TODO: drop ^^^^^*)
5.22 + Where:
5.23 + Find: "boolTestFind s_s"
5.24
5.25 text \<open>method solving the usecase\<close>
5.26
6.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Sun Jun 20 12:45:03 2021 +0200
6.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Sun Jun 20 16:26:18 2021 +0200
6.3 @@ -394,90 +394,89 @@
6.4
6.5 section \<open>Problems\<close>
6.6
6.7 -setup \<open>KEStore_Elems.add_pbts
6.8 - [(Problem.prep_input @{theory} "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 - (Problem.prep_input @{theory} "pbl_equsys_lin" [] Problem.id_empty
6.14 - (["LINEAR", "system"],
6.15 - [("#Given" ,["equalities e_s", "solveForVars v_s"]),
6.16 - (*TODO.WN050929 check linearity*)
6.17 - ("#Find" ,["solution ss'''"])],
6.18 - Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)], SOME "solveSystem e_s v_s", [])),
6.19 - (Problem.prep_input @{theory} "pbl_equsys_lin_2x2" [] Problem.id_empty
6.20 - (["2x2", "LINEAR", "system"],
6.21 - (*~~~~~~~~~~~~~~~~~~~~~~~~~*)
6.22 - [("#Given" ,["equalities e_s", "solveForVars v_s"]),
6.23 - ("#Where" ,["Length (e_s:: bool list) = 2", "Length v_s = 2"]),
6.24 - ("#Find" ,["solution ss'''"])],
6.25 - Rule_Set.append_rules "prls_2x2_linear_system" Rule_Set.empty
6.26 - [\<^rule_thm>\<open>LENGTH_CONS\<close>,
6.27 - \<^rule_thm>\<open>LENGTH_NIL\<close>,
6.28 - \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
6.29 - \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_")],
6.30 - SOME "solveSystem e_s v_s", [])),
6.31 - (Problem.prep_input @{theory} "pbl_equsys_lin_2x2_tri" [] Problem.id_empty
6.32 - (["triangular", "2x2", "LINEAR", "system"],
6.33 - [("#Given" ,["equalities e_s", "solveForVars v_s"]),
6.34 - ("#Where",
6.35 - ["(tl v_s) from v_s occur_exactly_in (NTH 1 (e_s::bool list))",
6.36 - " v_s from v_s occur_exactly_in (NTH 2 (e_s::bool list))"]),
6.37 - ("#Find" ,["solution ss'''"])],
6.38 - prls_triangular, SOME "solveSystem e_s v_s", [["EqSystem", "top_down_substitution", "2x2"]])),
6.39 - (Problem.prep_input @{theory} "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 - (Problem.prep_input @{theory} "pbl_equsys_lin_3x3" [] Problem.id_empty
6.47 - (["3x3", "LINEAR", "system"],
6.48 - (*~~~~~~~~~~~~~~~~~~~~~~~~~*)
6.49 - [("#Given" ,["equalities e_s", "solveForVars v_s"]),
6.50 - ("#Where" ,["Length (e_s:: bool list) = 3", "Length v_s = 3"]),
6.51 - ("#Find" ,["solution ss'''"])],
6.52 - Rule_Set.append_rules "prls_3x3_linear_system" Rule_Set.empty
6.53 - [\<^rule_thm>\<open>LENGTH_CONS\<close>,
6.54 - \<^rule_thm>\<open>LENGTH_NIL\<close>,
6.55 - \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
6.56 - \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_")],
6.57 - SOME "solveSystem e_s v_s", [])),
6.58 - (Problem.prep_input @{theory} "pbl_equsys_lin_4x4" [] Problem.id_empty
6.59 - (["4x4", "LINEAR", "system"],
6.60 - (*~~~~~~~~~~~~~~~~~~~~~~~~~*)
6.61 - [("#Given" ,["equalities e_s", "solveForVars v_s"]),
6.62 - ("#Where" ,["Length (e_s:: bool list) = 4", "Length v_s = 4"]),
6.63 - ("#Find" ,["solution ss'''"])],
6.64 - Rule_Set.append_rules "prls_4x4_linear_system" Rule_Set.empty
6.65 - [\<^rule_thm>\<open>LENGTH_CONS\<close>,
6.66 - \<^rule_thm>\<open>LENGTH_NIL\<close>,
6.67 - \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
6.68 - \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_")],
6.69 - SOME "solveSystem e_s v_s", [])),
6.70 - (Problem.prep_input @{theory} "pbl_equsys_lin_4x4_tri" [] Problem.id_empty
6.71 - (["triangular", "4x4", "LINEAR", "system"],
6.72 - [("#Given" ,["equalities e_s", "solveForVars v_s"]),
6.73 - ("#Where" , (*accepts missing variables up to diagional form*)
6.74 - ["(NTH 1 (v_s::real list)) occurs_in (NTH 1 (e_s::bool list))",
6.75 - "(NTH 2 (v_s::real list)) occurs_in (NTH 2 (e_s::bool list))",
6.76 - "(NTH 3 (v_s::real list)) occurs_in (NTH 3 (e_s::bool list))",
6.77 - "(NTH 4 (v_s::real list)) occurs_in (NTH 4 (e_s::bool list))"]),
6.78 - ("#Find" ,["solution ss'''"])],
6.79 - Rule_Set.append_rules "prls_tri_4x4_lin_sys" prls_triangular
6.80 - [\<^rule_eval>\<open>Prog_Expr.occurs_in\<close> (Prog_Expr.eval_occurs_in "")],
6.81 - SOME "solveSystem e_s v_s",
6.82 - [["EqSystem", "top_down_substitution", "4x4"]])),
6.83 - (Problem.prep_input @{theory} "pbl_equsys_lin_4x4_norm" [] Problem.id_empty
6.84 - (["normalise", "4x4", "LINEAR", "system"],
6.85 - [("#Given" ,["equalities e_s", "solveForVars v_s"]),
6.86 - (*Length is checked 1 level above*)
6.87 - ("#Find" ,["solution ss'''"])],
6.88 - Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)],
6.89 - SOME "solveSystem e_s v_s",
6.90 - [["EqSystem", "normalise", "4x4"]]))]\<close>
6.91 +problem pbl_equsys : "system" =
6.92 + \<open>Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)]\<close>
6.93 + CAS: "solveSystem e_s v_s"
6.94 + Given: "equalities e_s" "solveForVars v_s"
6.95 + Find: "solution ss'''" (*''' is copy-named*)
6.96 +
6.97 +problem pbl_equsys_lin : "LINEAR/system" =
6.98 + \<open>Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)]\<close>
6.99 + CAS: "solveSystem e_s v_s"
6.100 + Given: "equalities e_s" "solveForVars v_s"
6.101 + (*TODO.WN050929 check linearity*)
6.102 + Find: "solution ss'''"
6.103 +
6.104 +problem pbl_equsys_lin_2x2: "2x2/LINEAR/system" =
6.105 + \<open>Rule_Set.append_rules "prls_2x2_linear_system" Rule_Set.empty
6.106 + [\<^rule_thm>\<open>LENGTH_CONS\<close>,
6.107 + \<^rule_thm>\<open>LENGTH_NIL\<close>,
6.108 + \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
6.109 + \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_")]\<close>
6.110 + CAS: "solveSystem e_s v_s"
6.111 + Given: "equalities e_s" "solveForVars v_s"
6.112 + Where: "Length (e_s:: bool list) = 2" "Length v_s = 2"
6.113 + Find: "solution ss'''"
6.114 +
6.115 +problem pbl_equsys_lin_2x2_tri : "triangular/2x2/LINEAR/system" =
6.116 + \<open>prls_triangular\<close>
6.117 + Method: "EqSystem/top_down_substitution/2x2"
6.118 + CAS: "solveSystem e_s v_s"
6.119 + Given: "equalities e_s" "solveForVars v_s"
6.120 + Where:
6.121 + "(tl v_s) from v_s occur_exactly_in (NTH 1 (e_s::bool list))"
6.122 + " v_s from v_s occur_exactly_in (NTH 2 (e_s::bool list))"
6.123 + Find: "solution ss'''"
6.124 +
6.125 +problem pbl_equsys_lin_2x2_norm : "normalise/2x2/LINEAR/system" =
6.126 + \<open>Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)]\<close>
6.127 + Method: "EqSystem/normalise/2x2"
6.128 + CAS: "solveSystem e_s v_s"
6.129 + Given: "equalities e_s" "solveForVars v_s"
6.130 + Find: "solution ss'''"
6.131 +
6.132 +problem pbl_equsys_lin_3x3 : "3x3/LINEAR/system" =
6.133 + \<open>Rule_Set.append_rules "prls_3x3_linear_system" Rule_Set.empty
6.134 + [\<^rule_thm>\<open>LENGTH_CONS\<close>,
6.135 + \<^rule_thm>\<open>LENGTH_NIL\<close>,
6.136 + \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
6.137 + \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_")]\<close>
6.138 + CAS: "solveSystem e_s v_s"
6.139 + Given: "equalities e_s" "solveForVars v_s"
6.140 + Where: "Length (e_s:: bool list) = 3" "Length v_s = 3"
6.141 + Find: "solution ss'''"
6.142 +
6.143 +problem pbl_equsys_lin_4x4 : "4x4/LINEAR/system" =
6.144 + \<open>Rule_Set.append_rules "prls_4x4_linear_system" Rule_Set.empty
6.145 + [\<^rule_thm>\<open>LENGTH_CONS\<close>,
6.146 + \<^rule_thm>\<open>LENGTH_NIL\<close>,
6.147 + \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
6.148 + \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_")]\<close>
6.149 + CAS: "solveSystem e_s v_s"
6.150 + Given: "equalities e_s" "solveForVars v_s"
6.151 + Where: "Length (e_s:: bool list) = 4" "Length v_s = 4"
6.152 + Find: "solution ss'''"
6.153 +
6.154 +problem pbl_equsys_lin_4x4_tri : "triangular/4x4/LINEAR/system" =
6.155 + \<open>Rule_Set.append_rules "prls_tri_4x4_lin_sys" prls_triangular
6.156 + [\<^rule_eval>\<open>Prog_Expr.occurs_in\<close> (Prog_Expr.eval_occurs_in "")]\<close>
6.157 + Method: "EqSystem/top_down_substitution/4x4"
6.158 + CAS: "solveSystem e_s v_s"
6.159 + Given: "equalities e_s" "solveForVars v_s"
6.160 + Where: (*accepts missing variables up to diagional form*)
6.161 + "(NTH 1 (v_s::real list)) occurs_in (NTH 1 (e_s::bool list))"
6.162 + "(NTH 2 (v_s::real list)) occurs_in (NTH 2 (e_s::bool list))"
6.163 + "(NTH 3 (v_s::real list)) occurs_in (NTH 3 (e_s::bool list))"
6.164 + "(NTH 4 (v_s::real list)) occurs_in (NTH 4 (e_s::bool list))"
6.165 + Find: "solution ss'''"
6.166 +
6.167 +problem pbl_equsys_lin_4x4_norm : "normalise/4x4/LINEAR/system" =
6.168 + \<open>Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)]\<close>
6.169 + Method: "EqSystem/normalise/4x4"
6.170 + CAS: "solveSystem e_s v_s"
6.171 + Given: "equalities e_s" "solveForVars v_s"
6.172 + (*Length is checked 1 level above*)
6.173 + Find: "solution ss'''"
6.174
6.175 ML \<open>
6.176 (*this is for NTH only*)
7.1 --- a/src/Tools/isac/Knowledge/Equation.thy Sun Jun 20 12:45:03 2021 +0200
7.2 +++ b/src/Tools/isac/Knowledge/Equation.thy Sun Jun 20 16:26:18 2021 +0200
7.3 @@ -38,22 +38,21 @@
7.4 [\<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches "")];
7.5 \<close>
7.6 rule_set_knowledge univariate_equation_prls = \<open>Auto_Prog.prep_rls @{theory} univariate_equation_prls\<close>
7.7 -setup \<open>KEStore_Elems.add_pbts
7.8 - [(Problem.prep_input @{theory} "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
7.14 - [\<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches "")],
7.15 - SOME "solve (e_e::bool, v_v)", [])),
7.16 - (Problem.prep_input @{theory} "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 - ("#Find" ,["solutions v_v'i'"])],
7.21 - univariate_equation_prls, SOME "solve (e_e::bool, v_v)", []))]\<close>
7.22
7.23 +problem pbl_equ : "equation" =
7.24 + \<open>Rule_Set.append_rules "equation_prls" Rule_Set.empty
7.25 + [\<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches "")]\<close>
7.26 + CAS: "solve (e_e::bool, v_v)"
7.27 + Given: "equality e_e" "solveFor v_v"
7.28 + Where: "matches (?a = ?b) e_e"
7.29 + Find: "solutions v_v'i'"
7.30 +
7.31 +problem pbl_equ_univ : "univariate/equation" =
7.32 + \<open>univariate_equation_prls\<close>
7.33 + CAS: "solve (e_e::bool, v_v)"
7.34 + Given: "equality e_e" "solveFor v_v"
7.35 + Where: "matches (?a = ?b) e_e"
7.36 + Find: "solutions v_v'i'"
7.37
7.38 ML\<open>
7.39 (*.function for handling the cas-input "solve (x+1=2, x)":
8.1 --- a/src/Tools/isac/Knowledge/InsSort.thy Sun Jun 20 12:45:03 2021 +0200
8.2 +++ b/src/Tools/isac/Knowledge/InsSort.thy Sun Jun 20 16:26:18 2021 +0200
8.3 @@ -71,16 +71,17 @@
8.4 rule_set_knowledge ins_sort = ins_sort
8.5
8.6 section \<open>problems\<close>
8.7 -setup \<open>KEStore_Elems.add_pbts
8.8 - [ Problem.prep_input @{theory} "pbl_Programming" [] Problem.id_empty
8.9 - (["Programming"], [], Rule_Set.empty, NONE, []),
8.10 - Problem.prep_input @{theory} "pbl_Prog_sort" [] Problem.id_empty
8.11 - (["SORT", "Programming"], [], Rule_Set.empty, NONE, []),
8.12 - Problem.prep_input @{theory} "pbl_Prog_sort_ins" [] Problem.id_empty
8.13 - (["insertion", "SORT", "Programming"],
8.14 - [("#Given", ["unsorted u_u"]), ("#Find", ["sorted s_s"])],
8.15 - Rule_Set.empty,
8.16 - SOME "Sort u_u", [["Programming", "SORT", "insertion_steps"]])]\<close>
8.17 +
8.18 +problem pbl_Programming : Programming = \<open>Rule_Set.empty\<close>
8.19 +
8.20 +problem pbl_Prog_sort : "SORT/Programming" = \<open>Rule_Set.empty\<close>
8.21 +
8.22 +problem pbl_Prog_sort_ins : "insertion/SORT/Programming" =
8.23 + \<open>Rule_Set.empty\<close>
8.24 + Method: "Programming/SORT/insertion_steps"
8.25 + CAS: "Sort u_u"
8.26 + Given: "unsorted u_u"
8.27 + Find: "sorted s_s"
8.28
8.29 section \<open>methods\<close>
8.30 (* TODO: implementation needs extra object-level lists ?!?*)
9.1 --- a/src/Tools/isac/Knowledge/Integrate.thy Sun Jun 20 12:45:03 2021 +0200
9.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy Sun Jun 20 16:26:18 2021 +0200
9.3 @@ -320,22 +320,21 @@
9.4 norm_Rational_rls_noadd_fractions = \<open>prep_rls' norm_Rational_rls_noadd_fractions\<close>
9.5
9.6 (** problems **)
9.7 -setup \<open>KEStore_Elems.add_pbts
9.8 - [(Problem.prep_input @{theory} "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 - Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)],
9.13 - SOME "Integrate (f_f, v_v)",
9.14 - [["diff", "integration"]])),
9.15 - (*here "named" is used differently from Differentiation"*)
9.16 - (Problem.prep_input @{theory} "pbl_fun_integ_nam" [] Problem.id_empty
9.17 - (["named", "integrate", "function"],
9.18 - [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
9.19 - ("#Find" ,["antiDerivativeName F_F"])],
9.20 - Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)],
9.21 - SOME "Integrate (f_f, v_v)",
9.22 - [["diff", "integration", "named"]]))]\<close>
9.23 +
9.24 +problem pbl_fun_integ : "integrate/function" =
9.25 + \<open>Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)]\<close>
9.26 + Method: "diff/integration"
9.27 + CAS: "Integrate (f_f, v_v)"
9.28 + Given: "functionTerm f_f" "integrateBy v_v"
9.29 + Find: "antiDerivative F_F"
9.30 +
9.31 +problem pbl_fun_integ_nam : "named/integrate/function" =
9.32 + (*here "named" is used differently from Differentiation"*)
9.33 + \<open>Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)]\<close>
9.34 + Method: "diff/integration/named"
9.35 + CAS: "Integrate (f_f, v_v)"
9.36 + Given: "functionTerm f_f" "integrateBy v_v"
9.37 + Find: "antiDerivativeName F_F"
9.38
9.39 (** methods **)
9.40
10.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Sun Jun 20 12:45:03 2021 +0200
10.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Sun Jun 20 16:26:18 2021 +0200
10.3 @@ -43,16 +43,16 @@
10.4
10.5 subsection\<open>Define the Specification\<close>
10.6
10.7 -setup \<open>KEStore_Elems.add_pbts
10.8 - [(Problem.prep_input @{theory} "pbl_SP" [] Problem.id_empty (["SignalProcessing"], [], Rule_Set.empty, NONE, [])),
10.9 - (Problem.prep_input @{theory} "pbl_SP_Ztrans" [] Problem.id_empty
10.10 - (["Z_Transform", "SignalProcessing"], [], Rule_Set.empty, NONE, [])),
10.11 - (Problem.prep_input @{theory} "pbl_SP_Ztrans_inv" [] Problem.id_empty
10.12 - (["Inverse", "Z_Transform", "SignalProcessing"],
10.13 - [("#Given" , ["filterExpression X_eq"]),
10.14 - ("#Find" ,["stepResponse n_eq"])], \<comment> \<open>TODO: unused, "u [n]" is introduced by rule1..6\<close>
10.15 - Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)], NONE,
10.16 - [["SignalProcessing", "Z_Transform", "Inverse"]]))]\<close>
10.17 +problem pbl_SP : "SignalProcessing" = \<open>Rule_Set.empty\<close>
10.18 +
10.19 +problem pbl_SP_Ztrans : "Z_Transform/SignalProcessing" = \<open>Rule_Set.empty\<close>
10.20 +
10.21 +problem pbl_SP_Ztrans_inv : "Inverse/Z_Transform/SignalProcessing" =
10.22 + \<open>Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)]\<close>
10.23 + Method: "SignalProcessing/Z_Transform/Inverse"
10.24 + Given: "filterExpression X_eq"
10.25 + Find: "stepResponse n_eq" \<comment> \<open>TODO: unused, "u [n]" is introduced by rule1..6\<close>
10.26 +
10.27
10.28 subsection \<open>Setup Parent Nodes in Hierarchy of MethodC\<close>
10.29
11.1 --- a/src/Tools/isac/Knowledge/LinEq.thy Sun Jun 20 12:45:03 2021 +0200
11.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy Sun Jun 20 16:26:18 2021 +0200
11.3 @@ -106,19 +106,20 @@
11.4 \<close>
11.5 rule_set_knowledge LinEq_simplify = LinEq_simplify
11.6
11.7 -(*----------------------------- problem types --------------------------------*)
11.8 +(*----------------------------- problems --------------------------------*)
11.9 (* ---------linear----------- *)
11.10 -setup \<open>KEStore_Elems.add_pbts
11.11 - [(Problem.prep_input @{theory} "pbl_equ_univ_lin" [] Problem.id_empty
11.12 - (["LINEAR", "univariate", "equation"],
11.13 - [("#Given" ,["equality e_e", "solveFor v_v"]),
11.14 - ("#Where" ,["HOL.False", (*WN0509 just detected: this pbl can never be used?!?*)
11.15 - "Not( (lhs e_e) is_polyrat_in v_v)",
11.16 - "Not( (rhs e_e) is_polyrat_in v_v)",
11.17 - "((lhs e_e) has_degree_in v_v)=1",
11.18 - "((rhs e_e) has_degree_in v_v)=1"]),
11.19 - ("#Find" ,["solutions v_v'i'"])],
11.20 - LinEq_prls, SOME "solve (e_e::bool, v_v)", [["LinEq", "solve_lineq_equation"]]))]\<close>
11.21 +
11.22 +problem pbl_equ_univ_lin : "LINEAR/univariate/equation" =
11.23 + \<open>LinEq_prls\<close>
11.24 + Method: "LinEq/solve_lineq_equation"
11.25 + CAS: "solve (e_e::bool, v_v)"
11.26 + Given: "equality e_e" "solveFor v_v"
11.27 + Where: "HOL.False" (*WN0509 just detected: this pbl can never be used?!?*)
11.28 + "Not( (lhs e_e) is_polyrat_in v_v)"
11.29 + "Not( (rhs e_e) is_polyrat_in v_v)"
11.30 + "((lhs e_e) has_degree_in v_v)=1"
11.31 + "((rhs e_e) has_degree_in v_v)=1"
11.32 + Find: "solutions v_v'i'"
11.33
11.34 (*-------------- methods------------------------------------------------------*)
11.35 method met_eqlin : "LinEq" =
12.1 --- a/src/Tools/isac/Knowledge/LogExp.thy Sun Jun 20 12:45:03 2021 +0200
12.2 +++ b/src/Tools/isac/Knowledge/LogExp.thy Sun Jun 20 16:26:18 2021 +0200
12.3 @@ -17,15 +17,15 @@
12.4 exp_invers_log: "a \<up> (a log b) = b"
12.5
12.6 (** problems **)
12.7 -setup \<open>KEStore_Elems.add_pbts
12.8 - [(Problem.prep_input @{theory} "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 - ("#Find" ,["solutions v_v'i'"]),
12.13 - ("#With" ,["||(lhs (Subst (v'i', v_v) e_e) - " ^
12.14 - " (rhs (Subst (v'i', v_v) e_e) || < eps)"])],
12.15 - PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["Equation", "solve_log"]]))]\<close>
12.16 +
12.17 +problem pbl_test_equ_univ_log : "logarithmic/univariate/equation" =
12.18 + \<open>PolyEq_prls\<close>
12.19 + Method: "Equation/solve_log"
12.20 + CAS: "solve (e_e::bool, v_v)"
12.21 + Given: "equality e_e" "solveFor v_v"
12.22 + Where: "matches ((?a log ?v_v) = ?b) e_e"
12.23 + Find: "solutions v_v'i'"
12.24 + (*With: FIXME !? "||(lhs (Subst (v'i', v_v) e_e) - (rhs (Subst (v'i', v_v) e_e) || < eps)" *)
12.25
12.26 (** methods **)
12.27
13.1 --- a/src/Tools/isac/Knowledge/Partial_Fractions.thy Sun Jun 20 12:45:03 2021 +0200
13.2 +++ b/src/Tools/isac/Knowledge/Partial_Fractions.thy Sun Jun 20 16:26:18 2021 +0200
13.3 @@ -147,18 +147,15 @@
13.4 ML \<open>
13.5 Check_Unique.on := false; (*WN120307 REMOVE after editing*)
13.6 \<close>
13.7 -setup \<open>KEStore_Elems.add_pbts
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 - leading coefficient of the denominator is 1: to be checked here! and..
13.13 - ("#Where" ,["((get_numerator t_t) has_degree_in v_v) <
13.14 - ((get_denominator t_t) has_degree_in v_v)"]), TODO*)
13.15 - ("#Find" ,["decomposedFunction p_p'''"])],
13.16 - Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_ TODO*)],
13.17 - NONE,
13.18 - [["simplification", "of_rationals", "to_partial_fraction"]]))]\<close>
13.19 +problem pbl_simp_rat_partfrac : "partial_fraction/rational/simplification" =
13.20 + \<open>Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_ TODO*)]\<close>
13.21 + Method: "simplification/of_rationals/to_partial_fraction"
13.22 + Given: "functionTerm t_t" "solveFor v_v"
13.23 + (* TODO: call this sub-problem with appropriate functionTerm:
13.24 + leading coefficient of the denominator is 1: to be checked here! and..
13.25 + Where: "((get_numerator t_t) has_degree_in v_v) <
13.26 + ((get_denominator t_t) has_degree_in v_v)" TODO*)
13.27 + Find: "decomposedFunction p_p'''"
13.28
13.29 subsection \<open>MethodC\<close>
13.30 text \<open>rule set for functions called in the Program\<close>
14.1 --- a/src/Tools/isac/Knowledge/Poly.thy Sun Jun 20 12:45:03 2021 +0200
14.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Sun Jun 20 16:26:18 2021 +0200
14.3 @@ -1397,16 +1397,15 @@
14.4 make_rat_poly_with_parentheses = \<open>prep_rls' make_rat_poly_with_parentheses\<close>
14.5
14.6 subsection \<open>problems\<close>
14.7 -setup \<open>KEStore_Elems.add_pbts
14.8 - [(Problem.prep_input @{theory} "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 - ("#Find" ,["normalform n_n"])],
14.13 - Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)
14.14 - \<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp "")],
14.15 - SOME "Simplify t_t",
14.16 - [["simplification", "for_polynomials"]]))]\<close>
14.17 +
14.18 +problem pbl_simp_poly : "polynomial/simplification" =
14.19 + \<open>Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)
14.20 + \<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp "")]\<close>
14.21 + Method: "simplification/for_polynomials"
14.22 + CAS: "Simplify t_t"
14.23 + Given: "Term t_t"
14.24 + Where: "t_t is_polyexp"
14.25 + Find: "normalform n_n"
14.26
14.27 subsection \<open>methods\<close>
14.28
15.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Sun Jun 20 12:45:03 2021 +0200
15.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Sun Jun 20 16:26:18 2021 +0200
15.3 @@ -765,127 +765,159 @@
15.4 d3_polyeq_simplify = d3_polyeq_simplify and
15.5 d4_polyeq_simplify = d4_polyeq_simplify
15.6
15.7 -setup \<open>KEStore_Elems.add_pbts
15.8 - [(Problem.prep_input @{theory} "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 - "~((lhs e_e) is_rootTerm_in (v_v::real))",
15.13 - "~((rhs e_e) is_rootTerm_in (v_v::real))"]),
15.14 - ("#Find" ,["solutions v_v'i'"])],
15.15 - PolyEq_prls, SOME "solve (e_e::bool, v_v)", [])),
15.16 - (*--- d0 ---*)
15.17 - (Problem.prep_input @{theory} "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 - "(lhs e_e) is_poly_in v_v",
15.22 - "((lhs e_e) has_degree_in v_v ) = 0"]),
15.23 - ("#Find" ,["solutions v_v'i'"])],
15.24 - PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq", "solve_d0_polyeq_equation"]])),
15.25 - (*--- d1 ---*)
15.26 - (Problem.prep_input @{theory} "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 - "(lhs e_e) is_poly_in v_v",
15.31 - "((lhs e_e) has_degree_in v_v ) = 1"]),
15.32 - ("#Find" ,["solutions v_v'i'"])],
15.33 - PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq", "solve_d1_polyeq_equation"]])),
15.34 - (*--- d2 ---*)
15.35 - (Problem.prep_input @{theory} "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 - "(lhs e_e) is_poly_in v_v ",
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 - (Problem.prep_input @{theory} "pbl_equ_univ_poly_deg2_sqonly" [] Problem.id_empty
15.44 - (["sq_only", "degree_2", "polynomial", "univariate", "equation"],
15.45 - [("#Given" ,["equality e_e", "solveFor v_v"]),
15.46 - ("#Where" ,["matches ( ?a + ?v_ \<up> 2 = 0) e_e | " ^
15.47 - "matches ( ?a + ?b*?v_ \<up> 2 = 0) e_e | " ^
15.48 - "matches ( ?v_ \<up> 2 = 0) e_e | " ^
15.49 - "matches ( ?b*?v_ \<up> 2 = 0) e_e" ,
15.50 - "Not (matches (?a + ?v_ + ?v_ \<up> 2 = 0) e_e) &" ^
15.51 - "Not (matches (?a + ?b*?v_ + ?v_ \<up> 2 = 0) e_e) &" ^
15.52 - "Not (matches (?a + ?v_ + ?c*?v_ \<up> 2 = 0) e_e) &" ^
15.53 - "Not (matches (?a + ?b*?v_ + ?c*?v_ \<up> 2 = 0) e_e) &" ^
15.54 - "Not (matches ( ?v_ + ?v_ \<up> 2 = 0) e_e) &" ^
15.55 - "Not (matches ( ?b*?v_ + ?v_ \<up> 2 = 0) e_e) &" ^
15.56 - "Not (matches ( ?v_ + ?c*?v_ \<up> 2 = 0) e_e) &" ^
15.57 - "Not (matches ( ?b*?v_ + ?c*?v_ \<up> 2 = 0) e_e)"]),
15.58 - ("#Find" ,["solutions v_v'i'"])],
15.59 - PolyEq_prls, SOME "solve (e_e::bool, v_v)",
15.60 - [["PolyEq", "solve_d2_polyeq_sqonly_equation"]])),
15.61 - (Problem.prep_input @{theory} "pbl_equ_univ_poly_deg2_bdvonly" [] Problem.id_empty
15.62 - (["bdv_only", "degree_2", "polynomial", "univariate", "equation"],
15.63 - [("#Given", ["equality e_e", "solveFor v_v"]),
15.64 - ("#Where", ["matches (?a*?v_ + ?v_ \<up> 2 = 0) e_e | " ^
15.65 - "matches ( ?v_ + ?v_ \<up> 2 = 0) e_e | " ^
15.66 - "matches ( ?v_ + ?b*?v_ \<up> 2 = 0) e_e | " ^
15.67 - "matches (?a*?v_ + ?b*?v_ \<up> 2 = 0) e_e | " ^
15.68 - "matches ( ?v_ \<up> 2 = 0) e_e | " ^
15.69 - "matches ( ?b*?v_ \<up> 2 = 0) e_e "]),
15.70 - ("#Find", ["solutions v_v'i'"])],
15.71 - PolyEq_prls, SOME "solve (e_e::bool, v_v)",
15.72 - [["PolyEq", "solve_d2_polyeq_bdvonly_equation"]])),
15.73 - (Problem.prep_input @{theory} "pbl_equ_univ_poly_deg2_pq" [] Problem.id_empty
15.74 - (["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
15.75 - [("#Given", ["equality e_e", "solveFor v_v"]),
15.76 - ("#Where", ["matches (?a + 1*?v_ \<up> 2 = 0) e_e | " ^
15.77 - "matches (?a + ?v_ \<up> 2 = 0) e_e"]),
15.78 - ("#Find", ["solutions v_v'i'"])],
15.79 - PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq", "solve_d2_polyeq_pq_equation"]])),
15.80 - (Problem.prep_input @{theory} "pbl_equ_univ_poly_deg2_abc" [] Problem.id_empty
15.81 - (["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
15.82 - [("#Given", ["equality e_e", "solveFor v_v"]),
15.83 - ("#Where", ["matches (?a + ?v_ \<up> 2 = 0) e_e | " ^
15.84 - "matches (?a + ?b*?v_ \<up> 2 = 0) e_e"]),
15.85 - ("#Find", ["solutions v_v'i'"])],
15.86 - PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq", "solve_d2_polyeq_abc_equation"]])),
15.87 - (*--- d3 ---*)
15.88 - (Problem.prep_input @{theory} "pbl_equ_univ_poly_deg3" [] Problem.id_empty
15.89 - (["degree_3", "polynomial", "univariate", "equation"],
15.90 - [("#Given", ["equality e_e", "solveFor v_v"]),
15.91 - ("#Where", ["matches (?a = 0) e_e",
15.92 - "(lhs e_e) is_poly_in v_v ",
15.93 - "((lhs e_e) has_degree_in v_v) = 3"]),
15.94 - ("#Find", ["solutions v_v'i'"])],
15.95 - PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq", "solve_d3_polyeq_equation"]])),
15.96 - (*--- d4 ---*)
15.97 - (Problem.prep_input @{theory} "pbl_equ_univ_poly_deg4" [] Problem.id_empty
15.98 - (["degree_4", "polynomial", "univariate", "equation"],
15.99 - [("#Given", ["equality e_e", "solveFor v_v"]),
15.100 - ("#Where", ["matches (?a = 0) e_e",
15.101 - "(lhs e_e) is_poly_in v_v ",
15.102 - "((lhs e_e) has_degree_in v_v) = 4"]),
15.103 - ("#Find", ["solutions v_v'i'"])],
15.104 - PolyEq_prls, SOME "solve (e_e::bool, v_v)", [(*["PolyEq", "solve_d4_polyeq_equation"]*)])),
15.105 - (*--- normalise ---*)
15.106 - (Problem.prep_input @{theory} "pbl_equ_univ_poly_norm" [] Problem.id_empty
15.107 - (["normalise", "polynomial", "univariate", "equation"],
15.108 - [("#Given", ["equality e_e", "solveFor v_v"]),
15.109 - ("#Where", ["(Not((matches (?a = 0 ) e_e ))) |" ^
15.110 - "(Not(((lhs e_e) is_poly_in v_v)))"]),
15.111 - ("#Find", ["solutions v_v'i'"])],
15.112 - PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq", "normalise_poly"]])),
15.113 - (*-------------------------expanded-----------------------*)
15.114 - (Problem.prep_input @{theory} "pbl_equ_univ_expand" [] Problem.id_empty
15.115 - (["expanded", "univariate", "equation"],
15.116 - [("#Given", ["equality e_e", "solveFor v_v"]),
15.117 - ("#Where", ["matches (?a = 0) e_e",
15.118 - "(lhs e_e) is_expanded_in v_v "]),
15.119 - ("#Find", ["solutions v_v'i'"])],
15.120 - PolyEq_prls, SOME "solve (e_e::bool, v_v)", [])),
15.121 - (*--- d2 ---*)
15.122 - (Problem.prep_input @{theory} "pbl_equ_univ_expand_deg2" [] Problem.id_empty
15.123 - (["degree_2", "expanded", "univariate", "equation"],
15.124 - [("#Given", ["equality e_e", "solveFor v_v"]),
15.125 - ("#Where", ["((lhs e_e) has_degree_in v_v) = 2"]),
15.126 - ("#Find", ["solutions v_v'i'"])],
15.127 - PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq", "complete_square"]]))]\<close>
15.128 +problem pbl_equ_univ_poly : "polynomial/univariate/equation" =
15.129 + \<open>PolyEq_prls\<close>
15.130 + CAS: "solve (e_e::bool, v_v)"
15.131 + Given: "equality e_e" "solveFor v_v"
15.132 + Where:
15.133 + "~((e_e::bool) is_ratequation_in (v_v::real))"
15.134 + "~((lhs e_e) is_rootTerm_in (v_v::real))"
15.135 + "~((rhs e_e) is_rootTerm_in (v_v::real))"
15.136 + Find: "solutions v_v'i'"
15.137 +
15.138 +(*--- d0 ---*)
15.139 +problem pbl_equ_univ_poly_deg0 : "degree_0/polynomial/univariate/equation" =
15.140 + \<open>PolyEq_prls\<close>
15.141 + Method: "PolyEq/solve_d0_polyeq_equation"
15.142 + CAS: "solve (e_e::bool, v_v)"
15.143 + Given: "equality e_e" "solveFor v_v"
15.144 + Where:
15.145 + "matches (?a = 0) e_e"
15.146 + "(lhs e_e) is_poly_in v_v"
15.147 + "((lhs e_e) has_degree_in v_v ) = 0"
15.148 + Find: "solutions v_v'i'"
15.149 +
15.150 +(*--- d1 ---*)
15.151 +problem pbl_equ_univ_poly_deg1 : "degree_1/polynomial/univariate/equation" =
15.152 + \<open>PolyEq_prls\<close>
15.153 + Method: "PolyEq/solve_d1_polyeq_equation"
15.154 + CAS: "solve (e_e::bool, v_v)"
15.155 + Given: "equality e_e" "solveFor v_v"
15.156 + Where:
15.157 + "matches (?a = 0) e_e"
15.158 + "(lhs e_e) is_poly_in v_v"
15.159 + "((lhs e_e) has_degree_in v_v ) = 1"
15.160 + Find: "solutions v_v'i'"
15.161 +
15.162 +(*--- d2 ---*)
15.163 +problem pbl_equ_univ_poly_deg2 : "degree_2/polynomial/univariate/equation" =
15.164 + \<open>PolyEq_prls\<close>
15.165 + Method: "PolyEq/solve_d2_polyeq_equation"
15.166 + CAS: "solve (e_e::bool, v_v)"
15.167 + Given: "equality e_e" "solveFor v_v"
15.168 + Where:
15.169 + "matches (?a = 0) e_e"
15.170 + "(lhs e_e) is_poly_in v_v "
15.171 + "((lhs e_e) has_degree_in v_v ) = 2"
15.172 + Find: "solutions v_v'i'"
15.173 +
15.174 +problem pbl_equ_univ_poly_deg2_sqonly : "sq_only/degree_2/polynomial/univariate/equation" =
15.175 + \<open>PolyEq_prls\<close>
15.176 + Method: "PolyEq/solve_d2_polyeq_sqonly_equation"
15.177 + CAS: "solve (e_e::bool, v_v)"
15.178 + Given: "equality e_e" "solveFor v_v"
15.179 + Where:
15.180 + "matches ( ?a + ?v_ \<up> 2 = 0) e_e |
15.181 + matches ( ?a + ?b*?v_ \<up> 2 = 0) e_e |
15.182 + matches ( ?v_ \<up> 2 = 0) e_e |
15.183 + matches ( ?b*?v_ \<up> 2 = 0) e_e"
15.184 + "Not (matches (?a + ?v_ + ?v_ \<up> 2 = 0) e_e) &
15.185 + Not (matches (?a + ?b*?v_ + ?v_ \<up> 2 = 0) e_e) &
15.186 + Not (matches (?a + ?v_ + ?c*?v_ \<up> 2 = 0) e_e) &
15.187 + Not (matches (?a + ?b*?v_ + ?c*?v_ \<up> 2 = 0) e_e) &
15.188 + Not (matches ( ?v_ + ?v_ \<up> 2 = 0) e_e) &
15.189 + Not (matches ( ?b*?v_ + ?v_ \<up> 2 = 0) e_e) &
15.190 + Not (matches ( ?v_ + ?c*?v_ \<up> 2 = 0) e_e) &
15.191 + Not (matches ( ?b*?v_ + ?c*?v_ \<up> 2 = 0) e_e)"
15.192 + Find: "solutions v_v'i'"
15.193 +
15.194 +problem pbl_equ_univ_poly_deg2_bdvonly : "bdv_only/degree_2/polynomial/univariate/equation" =
15.195 + \<open>PolyEq_prls\<close>
15.196 + Method: "PolyEq/solve_d2_polyeq_bdvonly_equation"
15.197 + CAS: "solve (e_e::bool, v_v)"
15.198 + Given: "equality e_e" "solveFor v_v"
15.199 + Where:
15.200 + "matches (?a*?v_ + ?v_ \<up> 2 = 0) e_e |
15.201 + matches ( ?v_ + ?v_ \<up> 2 = 0) e_e |
15.202 + matches ( ?v_ + ?b*?v_ \<up> 2 = 0) e_e |
15.203 + matches (?a*?v_ + ?b*?v_ \<up> 2 = 0) e_e |
15.204 + matches ( ?v_ \<up> 2 = 0) e_e |
15.205 + matches ( ?b*?v_ \<up> 2 = 0) e_e "
15.206 + Find: "solutions v_v'i'"
15.207 +
15.208 +problem pbl_equ_univ_poly_deg2_pq : "pqFormula/degree_2/polynomial/univariate/equation" =
15.209 + \<open>PolyEq_prls\<close>
15.210 + Method: "PolyEq/solve_d2_polyeq_pq_equation"
15.211 + CAS: "solve (e_e::bool, v_v)"
15.212 + Given: "equality e_e" "solveFor v_v"
15.213 + Where:
15.214 + "matches (?a + 1*?v_ \<up> 2 = 0) e_e |
15.215 + matches (?a + ?v_ \<up> 2 = 0) e_e"
15.216 + Find: "solutions v_v'i'"
15.217 +
15.218 +problem pbl_equ_univ_poly_deg2_abc : "abcFormula/degree_2/polynomial/univariate/equation" =
15.219 + \<open>PolyEq_prls\<close>
15.220 + Method: "PolyEq/solve_d2_polyeq_abc_equation"
15.221 + CAS: "solve (e_e::bool, v_v)"
15.222 + Given: "equality e_e" "solveFor v_v"
15.223 + Where:
15.224 + "matches (?a + ?v_ \<up> 2 = 0) e_e |
15.225 + matches (?a + ?b*?v_ \<up> 2 = 0) e_e"
15.226 + Find: "solutions v_v'i'"
15.227 +
15.228 +(*--- d3 ---*)
15.229 +problem pbl_equ_univ_poly_deg3 : "degree_3/polynomial/univariate/equation" =
15.230 + \<open>PolyEq_prls\<close>
15.231 + Method: "PolyEq/solve_d3_polyeq_equation"
15.232 + CAS: "solve (e_e::bool, v_v)"
15.233 + Given: "equality e_e" "solveFor v_v"
15.234 + Where:
15.235 + "matches (?a = 0) e_e"
15.236 + "(lhs e_e) is_poly_in v_v"
15.237 + "((lhs e_e) has_degree_in v_v) = 3"
15.238 + Find: "solutions v_v'i'"
15.239 +
15.240 +(*--- d4 ---*)
15.241 +problem pbl_equ_univ_poly_deg4 : "degree_4/polynomial/univariate/equation" =
15.242 + \<open>PolyEq_prls\<close>
15.243 + (*Method: "PolyEq/solve_d4_polyeq_equation"*)
15.244 + CAS: "solve (e_e::bool, v_v)"
15.245 + Given: "equality e_e" "solveFor v_v"
15.246 + Where:
15.247 + "matches (?a = 0) e_e"
15.248 + "(lhs e_e) is_poly_in v_v"
15.249 + "((lhs e_e) has_degree_in v_v) = 4"
15.250 + Find: "solutions v_v'i'"
15.251 +
15.252 +(*--- normalise ---*)
15.253 +problem pbl_equ_univ_poly_norm : "normalise/polynomial/univariate/equation" =
15.254 + \<open>PolyEq_prls\<close>
15.255 + Method: "PolyEq/normalise_poly"
15.256 + CAS: "solve (e_e::bool, v_v)"
15.257 + Given: "equality e_e" "solveFor v_v"
15.258 + Where:
15.259 + "(Not((matches (?a = 0 ) e_e ))) |
15.260 + (Not(((lhs e_e) is_poly_in v_v)))"
15.261 + Find: "solutions v_v'i'"
15.262 +
15.263 +(*-------------------------expanded-----------------------*)
15.264 +problem "pbl_equ_univ_expand" : "expanded/univariate/equation" =
15.265 + \<open>PolyEq_prls\<close>
15.266 + CAS: "solve (e_e::bool, v_v)"
15.267 + Given: "equality e_e" "solveFor v_v"
15.268 + Where:
15.269 + "matches (?a = 0) e_e"
15.270 + "(lhs e_e) is_expanded_in v_v "
15.271 + Find: "solutions v_v'i'"
15.272 +
15.273 +(*--- d2 ---*)
15.274 +problem pbl_equ_univ_expand_deg2 : "degree_2/expanded/univariate/equation" =
15.275 + \<open>PolyEq_prls\<close>
15.276 + Method: "PolyEq/complete_square"
15.277 + CAS: "solve (e_e::bool, v_v)"
15.278 + Given: "equality e_e" "solveFor v_v"
15.279 + Where: "((lhs e_e) has_degree_in v_v) = 2"
15.280 + Find: "solutions v_v'i'"
15.281
15.282 text \<open>"-------------------------methods-----------------------"\<close>
15.283
16.1 --- a/src/Tools/isac/Knowledge/PolyMinus.thy Sun Jun 20 12:45:03 2021 +0200
16.2 +++ b/src/Tools/isac/Knowledge/PolyMinus.thy Sun Jun 20 16:26:18 2021 +0200
16.3 @@ -386,83 +386,87 @@
16.4 klammern_ausmultiplizieren = \<open>prep_rls' klammern_ausmultiplizieren\<close>
16.5
16.6 (** problems **)
16.7 -setup \<open>KEStore_Elems.add_pbts
16.8 - [(Problem.prep_input @{theory} "pbl_vereinf_poly" [] Problem.id_empty
16.9 - (["polynom", "vereinfachen"], [], Rule_Set.Empty, NONE, [])),
16.10 - (Problem.prep_input @{theory} "pbl_vereinf_poly_minus" [] Problem.id_empty
16.11 - (["plus_minus", "polynom", "vereinfachen"],
16.12 - [("#Given", ["Term t_t"]),
16.13 - ("#Where", ["t_t is_polyexp",
16.14 - "Not (matchsub (?a + (?b + ?c)) t_t | " ^
16.15 - " matchsub (?a + (?b - ?c)) t_t | " ^
16.16 - " matchsub (?a - (?b + ?c)) t_t | " ^
16.17 - " matchsub (?a + (?b - ?c)) t_t )",
16.18 - "Not (matchsub (?a * (?b + ?c)) t_t | " ^
16.19 - " matchsub (?a * (?b - ?c)) t_t | " ^
16.20 - " matchsub ((?b + ?c) * ?a) t_t | " ^
16.21 - " matchsub ((?b - ?c) * ?a) t_t )"]),
16.22 - ("#Find", ["normalform n_n"])],
16.23 - Rule_Set.append_rules "prls_pbl_vereinf_poly" Rule_Set.empty
16.24 - [\<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp ""),
16.25 - \<^rule_eval>\<open>Prog_Expr.matchsub\<close> (Prog_Expr.eval_matchsub ""),
16.26 - \<^rule_thm>\<open>or_true\<close>,
16.27 - (*"(?a | True) = True"*)
16.28 - \<^rule_thm>\<open>or_false\<close>,
16.29 - (*"(?a | False) = ?a"*)
16.30 - \<^rule_thm>\<open>not_true\<close>,
16.31 - (*"(~ True) = False"*)
16.32 - \<^rule_thm>\<open>not_false\<close>
16.33 - (*"(~ False) = True"*)],
16.34 - SOME "Vereinfache t_t", [["simplification", "for_polynomials", "with_minus"]])),
16.35 - (Problem.prep_input @{theory} "pbl_vereinf_poly_klammer" [] Problem.id_empty
16.36 - (["klammer", "polynom", "vereinfachen"],
16.37 - [("#Given" ,["Term t_t"]),
16.38 - ("#Where" ,["t_t is_polyexp",
16.39 - "Not (matchsub (?a * (?b + ?c)) t_t | " ^
16.40 - " matchsub (?a * (?b - ?c)) t_t | " ^
16.41 - " matchsub ((?b + ?c) * ?a) t_t | " ^
16.42 - " matchsub ((?b - ?c) * ?a) t_t )"]),
16.43 - ("#Find" ,["normalform n_n"])],
16.44 - Rule_Set.append_rules "prls_pbl_vereinf_poly_klammer" Rule_Set.empty
16.45 - [\<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp ""),
16.46 - \<^rule_eval>\<open>Prog_Expr.matchsub\<close> (Prog_Expr.eval_matchsub ""),
16.47 - \<^rule_thm>\<open>or_true\<close>,
16.48 - (*"(?a | True) = True"*)
16.49 - \<^rule_thm>\<open>or_false\<close>,
16.50 - (*"(?a | False) = ?a"*)
16.51 - \<^rule_thm>\<open>not_true\<close>,
16.52 - (*"(~ True) = False"*)
16.53 - \<^rule_thm>\<open>not_false\<close>
16.54 - (*"(~ False) = True"*)],
16.55 - SOME "Vereinfache t_t",
16.56 - [["simplification", "for_polynomials", "with_parentheses"]])),
16.57 - (Problem.prep_input @{theory} "pbl_vereinf_poly_klammer_mal" [] Problem.id_empty
16.58 - (["binom_klammer", "polynom", "vereinfachen"],
16.59 - [("#Given", ["Term t_t"]),
16.60 - ("#Where", ["t_t is_polyexp"]),
16.61 - ("#Find", ["normalform n_n"])],
16.62 - Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)
16.63 - \<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp "")],
16.64 - SOME "Vereinfache t_t",
16.65 - [["simplification", "for_polynomials", "with_parentheses_mult"]])),
16.66 - (Problem.prep_input @{theory} "pbl_probe" [] Problem.id_empty (["probe"], [], Rule_Set.Empty, NONE, [])),
16.67 - (Problem.prep_input @{theory} "pbl_probe_poly" [] Problem.id_empty
16.68 - (["polynom", "probe"],
16.69 - [("#Given", ["Pruefe e_e", "mitWert w_w"]),
16.70 - ("#Where", ["e_e is_polyexp"]),
16.71 - ("#Find", ["Geprueft p_p"])],
16.72 - Rule_Set.append_rules "prls_pbl_probe_poly" Rule_Set.empty [(*for preds in where_*)
16.73 - \<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp "")],
16.74 - SOME "Probe e_e w_w",
16.75 - [["probe", "fuer_polynom"]])),
16.76 - (Problem.prep_input @{theory} "pbl_probe_bruch" [] Problem.id_empty
16.77 - (["bruch", "probe"],
16.78 - [("#Given" ,["Pruefe e_e", "mitWert w_w"]),
16.79 - ("#Where" ,["e_e is_ratpolyexp"]),
16.80 - ("#Find" ,["Geprueft p_p"])],
16.81 - Rule_Set.append_rules "prls_pbl_probe_bruch" Rule_Set.empty [(*for preds in where_*)
16.82 - \<^rule_eval>\<open>is_ratpolyexp\<close> (eval_is_ratpolyexp "")],
16.83 - SOME "Probe e_e w_w", [["probe", "fuer_bruch"]]))]\<close>
16.84 +
16.85 +problem pbl_vereinf_poly : "polynom/vereinfachen" = \<open>Rule_Set.Empty\<close>
16.86 +
16.87 +problem pbl_vereinf_poly_minus : "plus_minus/polynom/vereinfachen" =
16.88 + \<open>Rule_Set.append_rules "prls_pbl_vereinf_poly" Rule_Set.empty
16.89 + [\<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp ""),
16.90 + \<^rule_eval>\<open>Prog_Expr.matchsub\<close> (Prog_Expr.eval_matchsub ""),
16.91 + \<^rule_thm>\<open>or_true\<close>,
16.92 + (*"(?a | True) = True"*)
16.93 + \<^rule_thm>\<open>or_false\<close>,
16.94 + (*"(?a | False) = ?a"*)
16.95 + \<^rule_thm>\<open>not_true\<close>,
16.96 + (*"(~ True) = False"*)
16.97 + \<^rule_thm>\<open>not_false\<close>
16.98 + (*"(~ False) = True"*)]\<close>
16.99 + Method: "simplification/for_polynomials/with_minus"
16.100 + CAS: "Vereinfache t_t"
16.101 + Given: "Term t_t"
16.102 + Where:
16.103 + "t_t is_polyexp"
16.104 + "Not (matchsub (?a + (?b + ?c)) t_t |
16.105 + matchsub (?a + (?b - ?c)) t_t |
16.106 + matchsub (?a - (?b + ?c)) t_t |
16.107 + matchsub (?a + (?b - ?c)) t_t )"
16.108 + "Not (matchsub (?a * (?b + ?c)) t_t |
16.109 + matchsub (?a * (?b - ?c)) t_t |
16.110 + matchsub ((?b + ?c) * ?a) t_t |
16.111 + matchsub ((?b - ?c) * ?a) t_t )"
16.112 + Find: "normalform n_n"
16.113 +
16.114 +problem pbl_vereinf_poly_klammer : "klammer/polynom/vereinfachen" =
16.115 + \<open>Rule_Set.append_rules "prls_pbl_vereinf_poly_klammer" Rule_Set.empty
16.116 + [\<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp ""),
16.117 + \<^rule_eval>\<open>Prog_Expr.matchsub\<close> (Prog_Expr.eval_matchsub ""),
16.118 + \<^rule_thm>\<open>or_true\<close>,
16.119 + (*"(?a | True) = True"*)
16.120 + \<^rule_thm>\<open>or_false\<close>,
16.121 + (*"(?a | False) = ?a"*)
16.122 + \<^rule_thm>\<open>not_true\<close>,
16.123 + (*"(~ True) = False"*)
16.124 + \<^rule_thm>\<open>not_false\<close>
16.125 + (*"(~ False) = True"*)]\<close>
16.126 + Method: "simplification/for_polynomials/with_parentheses"
16.127 + CAS: "Vereinfache t_t"
16.128 + Given: "Term t_t"
16.129 + Where:
16.130 + "t_t is_polyexp"
16.131 + "Not (matchsub (?a * (?b + ?c)) t_t |
16.132 + matchsub (?a * (?b - ?c)) t_t |
16.133 + matchsub ((?b + ?c) * ?a) t_t |
16.134 + matchsub ((?b - ?c) * ?a) t_t )"
16.135 + Find: "normalform n_n"
16.136 +
16.137 +problem pbl_vereinf_poly_klammer_mal : "binom_klammer/polynom/vereinfachen" =
16.138 + \<open>Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)
16.139 + \<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp "")]\<close>
16.140 + Method: "simplification/for_polynomials/with_parentheses_mult"
16.141 + CAS: "Vereinfache t_t"
16.142 + Given: "Term t_t"
16.143 + Where: "t_t is_polyexp"
16.144 + Find: "normalform n_n"
16.145 +
16.146 +problem pbl_probe : "probe" = \<open>Rule_Set.Empty\<close>
16.147 +
16.148 +problem pbl_probe_poly : "polynom/probe" =
16.149 + \<open>Rule_Set.append_rules "prls_pbl_probe_poly" Rule_Set.empty [(*for preds in where_*)
16.150 + \<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp "")]\<close>
16.151 + Method: "probe/fuer_polynom"
16.152 + CAS: "Probe e_e w_w"
16.153 + Given: "Pruefe e_e" "mitWert w_w"
16.154 + Where: "e_e is_polyexp"
16.155 + Find: "Geprueft p_p"
16.156 +
16.157 +problem pbl_probe_bruch : "bruch/probe" =
16.158 + \<open>Rule_Set.append_rules "prls_pbl_probe_bruch" Rule_Set.empty [(*for preds in where_*)
16.159 + \<^rule_eval>\<open>is_ratpolyexp\<close> (eval_is_ratpolyexp "")]\<close>
16.160 + Method: "probe/fuer_bruch"
16.161 + CAS: "Probe e_e w_w"
16.162 + Given: "Pruefe e_e" "mitWert w_w"
16.163 + Where: "e_e is_ratpolyexp"
16.164 + Find: "Geprueft p_p"
16.165
16.166 (** methods **)
16.167
17.1 --- a/src/Tools/isac/Knowledge/RatEq.thy Sun Jun 20 12:45:03 2021 +0200
17.2 +++ b/src/Tools/isac/Knowledge/RatEq.thy Sun Jun 20 16:26:18 2021 +0200
17.3 @@ -158,13 +158,14 @@
17.4 rule_set_knowledge RatEq_simplify = RatEq_simplify
17.5
17.6 subsection \<open>problems\<close>
17.7 -setup \<open>KEStore_Elems.add_pbts
17.8 - [(Problem.prep_input @{theory} "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 - ("#Find", ["solutions v_v'i'"])],
17.13 - RatEq_prls, SOME "solve (e_e::bool, v_v)", [["RatEq", "solve_rat_equation"]]))]\<close>
17.14 +
17.15 +problem pbl_equ_univ_rat : "rational/univariate/equation" =
17.16 + \<open>RatEq_prls\<close>
17.17 + Method: "RatEq/solve_rat_equation"
17.18 + CAS: "solve (e_e::bool, v_v)"
17.19 + Given: "equality e_e" "solveFor v_v"
17.20 + Where: "(e_e::bool) is_ratequation_in (v_v::real)"
17.21 + Find: "solutions v_v'i'"
17.22
17.23 subsection \<open>methods\<close>
17.24
18.1 --- a/src/Tools/isac/Knowledge/Rational.thy Sun Jun 20 12:45:03 2021 +0200
18.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Sun Jun 20 16:26:18 2021 +0200
18.3 @@ -875,14 +875,14 @@
18.4 cancel_p_rls = cancel_p_rls
18.5
18.6 section \<open>A problem for simplification of rationals\<close>
18.7 -setup \<open>KEStore_Elems.add_pbts
18.8 - [(Problem.prep_input @{theory} "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 - ("#Find" ,["normalform n_n"])],
18.13 - Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)],
18.14 - SOME "Simplify t_t", [["simplification", "of_rationals"]]))]\<close>
18.15 +
18.16 +problem pbl_simp_rat : "rational/simplification" =
18.17 + \<open>Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)]\<close>
18.18 + Method: "simplification/of_rationals"
18.19 + CAS: "Simplify t_t"
18.20 + Given: "Term t_t"
18.21 + Where: "t_t is_ratpolyexp"
18.22 + Find: "normalform n_n"
18.23
18.24 section \<open>A methods for simplification of rationals\<close>
18.25 (*WN061025 this methods script is copied from (auto-generated) script
19.1 --- a/src/Tools/isac/Knowledge/RootEq.thy Sun Jun 20 12:45:03 2021 +0200
19.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy Sun Jun 20 16:26:18 2021 +0200
19.3 @@ -422,37 +422,41 @@
19.4 rooteq_simplify = rooteq_simplify
19.5
19.6 subsection \<open>problems\<close>
19.7 -(*Ambiguous input produces 5 parse trees -----------------------------------------------------\\*)
19.8 -setup \<open>KEStore_Elems.add_pbts
19.9 - (* ---------root----------- *)
19.10 - [(Problem.prep_input @{theory} "pbl_equ_univ_root" [] Problem.id_empty
19.11 - (["rootX", "univariate", "equation"],
19.12 - [("#Given" ,["equality e_e", "solveFor v_v"]),
19.13 - ("#Where" ,["(lhs e_e) is_rootTerm_in (v_v::real) | " ^
19.14 - "(rhs e_e) is_rootTerm_in (v_v::real)"]),
19.15 - ("#Find" ,["solutions v_v'i'"])],
19.16 - RootEq_prls, SOME "solve (e_e::bool, v_v)", [])),
19.17 - (* ---------sqrt----------- *)
19.18 - (Problem.prep_input @{theory} "pbl_equ_univ_root_sq" [] Problem.id_empty
19.19 - (["sq", "rootX", "univariate", "equation"],
19.20 - [("#Given" ,["equality e_e", "solveFor v_v"]),
19.21 - ("#Where" ,["( ((lhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
19.22 - " ((lhs e_e) is_normSqrtTerm_in (v_v::real)) ) |" ^
19.23 - "( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
19.24 - " ((rhs e_e) is_normSqrtTerm_in (v_v::real)) )"]),
19.25 - ("#Find" ,["solutions v_v'i'"])],
19.26 - RootEq_prls, SOME "solve (e_e::bool, v_v)", [["RootEq", "solve_sq_root_equation"]])),
19.27 - (* ---------normalise----------- *)
19.28 - (Problem.prep_input @{theory} "pbl_equ_univ_root_norm" [] Problem.id_empty
19.29 - (["normalise", "rootX", "univariate", "equation"],
19.30 - [("#Given" ,["equality e_e", "solveFor v_v"]),
19.31 - ("#Where" ,["( ((lhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
19.32 - " Not((lhs e_e) is_normSqrtTerm_in (v_v::real))) | " ^
19.33 - "( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
19.34 - " Not((rhs e_e) is_normSqrtTerm_in (v_v::real)))"]),
19.35 - ("#Find" ,["solutions v_v'i'"])],
19.36 - RootEq_prls, SOME "solve (e_e::bool, v_v)", [["RootEq", "norm_sq_root_equation"]]))]\<close>
19.37 -(*Ambiguous input produces 5 parse trees -----------------------------------------------------//*)
19.38 +
19.39 +problem pbl_equ_univ_root : "rootX/univariate/equation" =
19.40 + \<open>RootEq_prls\<close>
19.41 + CAS: "solve (e_e::bool, v_v)"
19.42 + Given: "equality e_e" "solveFor v_v"
19.43 + Where:
19.44 + (*Ambiguous input produces 5 parse trees -----------------------------------------------------\\*)
19.45 + "(lhs e_e) is_rootTerm_in (v_v::real) |
19.46 + (rhs e_e) is_rootTerm_in (v_v::real)"
19.47 + Find: "solutions v_v'i'"
19.48 +
19.49 +problem pbl_equ_univ_root_sq : "sq/rootX/univariate/equation" =
19.50 + \<open>RootEq_prls\<close>
19.51 + Method: "RootEq/solve_sq_root_equation"
19.52 + CAS: "solve (e_e::bool, v_v)"
19.53 + Given: "equality e_e" "solveFor v_v"
19.54 + Where:
19.55 + "( ((lhs e_e) is_sqrtTerm_in (v_v::real)) &
19.56 + ((lhs e_e) is_normSqrtTerm_in (v_v::real)) ) |
19.57 + ( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &
19.58 + ((rhs e_e) is_normSqrtTerm_in (v_v::real)) )"
19.59 + Find: "solutions v_v'i'"
19.60 +
19.61 +(* ---------normalise----------- *)
19.62 +problem pbl_equ_univ_root_norm : "normalise/rootX/univariate/equation" =
19.63 + \<open>RootEq_prls\<close>
19.64 + Method: "RootEq/norm_sq_root_equation"
19.65 + CAS: "solve (e_e::bool, v_v)"
19.66 + Given: "equality e_e" "solveFor v_v"
19.67 + Where:
19.68 + "( ((lhs e_e) is_sqrtTerm_in (v_v::real)) &
19.69 + Not((lhs e_e) is_normSqrtTerm_in (v_v::real))) |
19.70 + ( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &
19.71 + Not((rhs e_e) is_normSqrtTerm_in (v_v::real)))"
19.72 + Find: "solutions v_v'i'"
19.73
19.74 subsection \<open>methods\<close>
19.75
20.1 --- a/src/Tools/isac/Knowledge/RootRatEq.thy Sun Jun 20 12:45:03 2021 +0200
20.2 +++ b/src/Tools/isac/Knowledge/RootRatEq.thy Sun Jun 20 16:26:18 2021 +0200
20.3 @@ -120,14 +120,14 @@
20.4
20.5 subsection \<open>problems\<close>
20.6
20.7 -setup \<open>KEStore_Elems.add_pbts
20.8 - [(Problem.prep_input @{theory} "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 - "( (rhs e_e) is_rootRatAddTerm_in (v_v::real) )"]),
20.13 - ("#Find" ,["solutions v_v'i'"])],
20.14 - RootRatEq_prls, SOME "solve (e_e::bool, v_v)", [["RootRatEq", "elim_rootrat_equation"]]))]\<close>
20.15 +problem pbl_equ_univ_root_sq_rat : "rat/sq/rootX/univariate/equation" =
20.16 + \<open>RootRatEq_prls\<close>
20.17 + Method: "RootRatEq/elim_rootrat_equation"
20.18 + CAS: "solve (e_e::bool, v_v)"
20.19 + Given: "equality e_e" "solveFor v_v"
20.20 + Where: "( (lhs e_e) is_rootRatAddTerm_in (v_v::real) ) |
20.21 + ( (rhs e_e) is_rootRatAddTerm_in (v_v::real) )"
20.22 + Find: "solutions v_v'i'"
20.23
20.24 subsection \<open>methods\<close>
20.25
21.1 --- a/src/Tools/isac/Knowledge/Simplify.thy Sun Jun 20 12:45:03 2021 +0200
21.2 +++ b/src/Tools/isac/Knowledge/Simplify.thy Sun Jun 20 16:26:18 2021 +0200
21.3 @@ -21,17 +21,18 @@
21.4 Vereinfache :: "real => real" (*"Vereinfache (1+2a+3+4a)*)
21.5
21.6 (** problems **)
21.7 -setup \<open>KEStore_Elems.add_pbts
21.8 - [(Problem.prep_input @{theory} "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 - (Problem.prep_input @{theory} "pbl_vereinfache" [] Problem.id_empty
21.14 - (["vereinfachen"],
21.15 - [("#Given", ["Term t_t"]),
21.16 - ("#Find", ["normalform n_n"])],
21.17 - Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)], SOME "Vereinfache t_t", []))]\<close>
21.18 +
21.19 +problem pbl_simp : "simplification" =
21.20 + \<open>Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)]\<close>
21.21 + CAS: "Simplify t_t"
21.22 + Given: "Term t_t"
21.23 + Find: "normalform n_n"
21.24 +
21.25 +problem pbl_vereinfache : "vereinfachen" =
21.26 + \<open>Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)]\<close>
21.27 + CAS: "Vereinfache t_t"
21.28 + Given: "Term t_t"
21.29 + Find: "normalform n_n"
21.30
21.31 (** methods **)
21.32
22.1 --- a/src/Tools/isac/Knowledge/Test.thy Sun Jun 20 12:45:03 2021 +0200
22.2 +++ b/src/Tools/isac/Knowledge/Test.thy Sun Jun 20 16:26:18 2021 +0200
22.3 @@ -567,30 +567,33 @@
22.4
22.5
22.6 subsection \<open>problems\<close>
22.7 -(** problem types **)
22.8 -setup \<open>KEStore_Elems.add_pbts
22.9 - [(Problem.prep_input @{theory} "pbl_test" [] Problem.id_empty (["test"], [], Rule_Set.empty, NONE, [])),
22.10 - (Problem.prep_input @{theory} "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 - (Problem.prep_input @{theory} "pbl_test_uni" [] Problem.id_empty
22.17 - (["univariate", "equation", "test"],
22.18 - [("#Given" ,["equality e_e", "solveFor v_v"]),
22.19 - ("#Where" ,["matches (?a = ?b) e_e"]),
22.20 - ("#Find" ,["solutions v_v'i'"])],
22.21 - assoc_rls' @{theory} "matches", SOME "solve (e_e::bool, v_v)", [])),
22.22 - (Problem.prep_input @{theory} "pbl_test_uni_lin" [] Problem.id_empty
22.23 - (["LINEAR", "univariate", "equation", "test"],
22.24 - [("#Given" ,["equality e_e", "solveFor v_v"]),
22.25 - ("#Where" ,["(matches ( v_v = 0) e_e) | (matches ( ?b*v_v = 0) e_e) |" ^
22.26 - "(matches (?a+v_v = 0) e_e) | (matches (?a+?b*v_v = 0) e_e) "]),
22.27 - ("#Find" ,["solutions v_v'i'"])],
22.28 - assoc_rls' @{theory} "matches",
22.29 - SOME "solve (e_e::bool, v_v)", [["Test", "solve_linear"]]))]
22.30 -\<close>
22.31 +
22.32 +problem pbl_test : "test" = \<open>Rule_Set.empty\<close>
22.33 +
22.34 +problem pbl_test_equ : "equation/test" =
22.35 + \<open>assoc_rls' @{theory} "matches"\<close>
22.36 + CAS: "solve (e_e::bool, v_v)"
22.37 + Given: "equality e_e" "solveFor v_v"
22.38 + Where: "matches (?a = ?b) e_e"
22.39 + Find: "solutions v_v'i'"
22.40 +
22.41 +problem pbl_test_uni : "univariate/equation/test" =
22.42 + \<open>assoc_rls' @{theory} "matches"\<close>
22.43 + CAS: "solve (e_e::bool, v_v)"
22.44 + Given: "equality e_e" "solveFor v_v"
22.45 + Where: "matches (?a = ?b) e_e"
22.46 + Find: "solutions v_v'i'"
22.47 +
22.48 +problem pbl_test_uni_lin : "LINEAR/univariate/equation/test" =
22.49 + \<open>assoc_rls' @{theory} "matches"\<close>
22.50 + Method: "Test/solve_linear"
22.51 + CAS: "solve (e_e::bool, v_v)"
22.52 + Given: "equality e_e" "solveFor v_v"
22.53 + Where:
22.54 + "(matches ( v_v = 0) e_e) | (matches ( ?b*v_v = 0) e_e) |
22.55 + (matches (?a+v_v = 0) e_e) | (matches (?a+?b*v_v = 0) e_e)"
22.56 + Find: "solutions v_v'i'"
22.57 +
22.58 ML \<open>
22.59 Rewrite_Ord.rew_ord' := overwritel (! Rewrite_Ord.rew_ord',
22.60 [("termlessI", termlessI),
22.61 @@ -766,64 +769,74 @@
22.62 rearrange_assoc = \<open>prep_rls' rearrange_assoc\<close>
22.63
22.64 section \<open>problems\<close>
22.65 -setup \<open>KEStore_Elems.add_pbts
22.66 - [(Problem.prep_input @{theory} "pbl_test_uni_plain2" [] Problem.id_empty
22.67 - (["plain_square", "univariate", "equation", "test"],
22.68 - [("#Given" ,["equality e_e", "solveFor v_v"]),
22.69 - ("#Where" ,["(matches (?a + ?b*v_v \<up> 2 = 0) e_e) |" ^
22.70 - "(matches ( ?b*v_v \<up> 2 = 0) e_e) |" ^
22.71 - "(matches (?a + v_v \<up> 2 = 0) e_e) |" ^
22.72 - "(matches ( v_v \<up> 2 = 0) e_e)"]),
22.73 - ("#Find" ,["solutions v_v'i'"])],
22.74 - assoc_rls' @{theory} "matches",
22.75 - SOME "solve (e_e::bool, v_v)", [["Test", "solve_plain_square"]])),
22.76 - (Problem.prep_input @{theory} "pbl_test_uni_poly" [] Problem.id_empty
22.77 - (["polynomial", "univariate", "equation", "test"],
22.78 - [("#Given" ,["equality (v_v \<up> 2 + p_p * v_v + q__q = 0)", "solveFor v_v"]),
22.79 - ("#Where" ,["HOL.False"]),
22.80 - ("#Find" ,["solutions v_v'i'"])],
22.81 - Rule_Set.empty, SOME "solve (e_e::bool, v_v)", [])),
22.82 - (Problem.prep_input @{theory} "pbl_test_uni_poly_deg2" [] Problem.id_empty
22.83 - (["degree_two", "polynomial", "univariate", "equation", "test"],
22.84 - [("#Given" ,["equality (v_v \<up> 2 + p_p * v_v + q__q = 0)", "solveFor v_v"]),
22.85 - ("#Find" ,["solutions v_v'i'"])],
22.86 - Rule_Set.empty, SOME "solve (v_v \<up> 2 + p_p * v_v + q__q = 0, v_v)", [])),
22.87 - (Problem.prep_input @{theory} "pbl_test_uni_poly_deg2_pq" [] Problem.id_empty
22.88 - (["pq_formula", "degree_two", "polynomial", "univariate", "equation", "test"],
22.89 - [("#Given" ,["equality (v_v \<up> 2 + p_p * v_v + q__q = 0)", "solveFor v_v"]),
22.90 - ("#Find" ,["solutions v_v'i'"])],
22.91 - Rule_Set.empty, SOME "solve (v_v \<up> 2 + p_p * v_v + q__q = 0, v_v)", [])),
22.92 - (Problem.prep_input @{theory} "pbl_test_uni_poly_deg2_abc" [] Problem.id_empty
22.93 - (["abc_formula", "degree_two", "polynomial", "univariate", "equation", "test"],
22.94 - [("#Given" ,["equality (a_a * x \<up> 2 + b_b * x + c_c = 0)", "solveFor v_v"]),
22.95 - ("#Find" ,["solutions v_v'i'"])],
22.96 - Rule_Set.empty, SOME "solve (a_a * x \<up> 2 + b_b * x + c_c = 0, v_v)", [])),
22.97 - (Problem.prep_input @{theory} "pbl_test_uni_root" [] Problem.id_empty
22.98 - (["squareroot", "univariate", "equation", "test"],
22.99 - [("#Given" ,["equality e_e", "solveFor v_v"]),
22.100 - ("#Where" ,["precond_rootpbl v_v"]),
22.101 - ("#Find" ,["solutions v_v'i'"])],
22.102 - Rule_Set.append_rules "contains_root" Rule_Set.empty [\<^rule_eval>\<open>contains_root\<close>
22.103 - (eval_contains_root "#contains_root_")],
22.104 - SOME "solve (e_e::bool, v_v)", [["Test", "square_equation"]])),
22.105 - (Problem.prep_input @{theory} "pbl_test_uni_norm" [] Problem.id_empty
22.106 - (["normalise", "univariate", "equation", "test"],
22.107 - [("#Given" ,["equality e_e", "solveFor v_v"]),
22.108 - ("#Where" ,[]),
22.109 - ("#Find" ,["solutions v_v'i'"])],
22.110 - Rule_Set.empty, SOME "solve (e_e::bool, v_v)", [["Test", "norm_univar_equation"]])),
22.111 - (Problem.prep_input @{theory} "pbl_test_uni_roottest" [] Problem.id_empty
22.112 - (["sqroot-test", "univariate", "equation", "test"],
22.113 - [("#Given" ,["equality e_e", "solveFor v_v"]),
22.114 - ("#Where" ,["precond_rootpbl v_v"]),
22.115 - ("#Find" ,["solutions v_v'i'"])],
22.116 - Rule_Set.empty, SOME "solve (e_e::bool, v_v)", [])),
22.117 - (Problem.prep_input @{theory} "pbl_test_intsimp" [] Problem.id_empty
22.118 - (["inttype", "test"],
22.119 - [("#Given" ,["intTestGiven t_t"]),
22.120 - ("#Where" ,[]),
22.121 - ("#Find" ,["intTestFind s_s"])],
22.122 - Rule_Set.empty, NONE, [["Test", "intsimp"]]))]\<close>
22.123 +
22.124 +problem pbl_test_uni_plain2 : "plain_square/univariate/equation/test" =
22.125 + \<open>assoc_rls' @{theory} "matches"\<close>
22.126 + Method: "Test/solve_plain_square"
22.127 + CAS: "solve (e_e::bool, v_v)"
22.128 + Given: "equality e_e" "solveFor v_v"
22.129 + Where:
22.130 + "(matches (?a + ?b*v_v \<up> 2 = 0) e_e) |
22.131 + (matches ( ?b*v_v \<up> 2 = 0) e_e) |
22.132 + (matches (?a + v_v \<up> 2 = 0) e_e) |
22.133 + (matches ( v_v \<up> 2 = 0) e_e)"
22.134 + Find: "solutions v_v'i'"
22.135 +
22.136 +problem pbl_test_uni_poly : "polynomial/univariate/equation/test" =
22.137 + \<open>Rule_Set.empty\<close>
22.138 + CAS: "solve (e_e::bool, v_v)"
22.139 + Given: "equality (v_v \<up> 2 + p_p * v_v + q__q = 0)" "solveFor v_v"
22.140 + Where: "HOL.False"
22.141 + Find: "solutions v_v'i'"
22.142 +
22.143 +problem pbl_test_uni_poly_deg2 : "degree_two/polynomial/univariate/equation/test" =
22.144 + \<open>Rule_Set.empty\<close>
22.145 + CAS: "solve (v_v \<up> 2 + p_p * v_v + q__q = 0, v_v)"
22.146 + Given: "equality (v_v \<up> 2 + p_p * v_v + q__q = 0)" "solveFor v_v"
22.147 + Find: "solutions v_v'i'"
22.148 +
22.149 +problem pbl_test_uni_poly_deg2_pq : "pq_formula/degree_two/polynomial/univariate/equation/test" =
22.150 + \<open>Rule_Set.empty\<close>
22.151 + CAS: "solve (v_v \<up> 2 + p_p * v_v + q__q = 0, v_v)"
22.152 + Given: "equality (v_v \<up> 2 + p_p * v_v + q__q = 0)" "solveFor v_v"
22.153 + Find: "solutions v_v'i'"
22.154 +
22.155 +problem pbl_test_uni_poly_deg2_abc : "abc_formula/degree_two/polynomial/univariate/equation/test" =
22.156 + \<open>Rule_Set.empty\<close>
22.157 + CAS: "solve (a_a * x \<up> 2 + b_b * x + c_c = 0, v_v)"
22.158 + Given: "equality (a_a * x \<up> 2 + b_b * x + c_c = 0)" "solveFor v_v"
22.159 + Find: "solutions v_v'i'"
22.160 +
22.161 +problem pbl_test_uni_root : "squareroot/univariate/equation/test" =
22.162 + \<open>Rule_Set.append_rules "contains_root" Rule_Set.empty [\<^rule_eval>\<open>contains_root\<close>
22.163 + (eval_contains_root "#contains_root_")]\<close>
22.164 + Method: "Test/square_equation"
22.165 + CAS: "solve (e_e::bool, v_v)"
22.166 + Given: "equality e_e" "solveFor v_v"
22.167 + Where: "precond_rootpbl v_v"
22.168 + Find: "solutions v_v'i'"
22.169 +
22.170 +problem pbl_test_uni_norm : "normalise/univariate/equation/test" =
22.171 + \<open>Rule_Set.empty\<close>
22.172 + Method: "Test/norm_univar_equation"
22.173 + CAS: "solve (e_e::bool, v_v)"
22.174 + Given: "equality e_e" "solveFor v_v"
22.175 + Where:
22.176 + Find: "solutions v_v'i'"
22.177 +
22.178 +problem pbl_test_uni_roottest : "sqroot-test/univariate/equation/test" =
22.179 + \<open>Rule_Set.empty\<close>
22.180 + CAS: "solve (e_e::bool, v_v)"
22.181 + Given: "equality e_e" "solveFor v_v"
22.182 + Where: "precond_rootpbl v_v"
22.183 + Find: "solutions v_v'i'"
22.184 +
22.185 +problem pbl_test_intsimp : "inttype/test" =
22.186 + \<open>Rule_Set.empty\<close>
22.187 + Method: "Test/intsimp"
22.188 + Given: "intTestGiven t_t"
22.189 + Where:
22.190 + Find: "intTestFind s_s"
22.191
22.192 section \<open>methods\<close>
22.193 subsection \<open>differentiate\<close>
23.1 --- a/src/Tools/isac/MathEngBasic/MathEngBasic.thy Sun Jun 20 12:45:03 2021 +0200
23.2 +++ b/src/Tools/isac/MathEngBasic/MathEngBasic.thy Sun Jun 20 16:26:18 2021 +0200
23.3 @@ -6,8 +6,8 @@
23.4 *)
23.5 theory MathEngBasic
23.6 imports "$ISABELLE_ISAC/ProgLang/ProgLang" "$ISABELLE_ISAC/Specify/Input_Descript"
23.7 - keywords "method" :: thy_decl
23.8 - and "Author" "Program" "Given" "Where" "Find" "Relate"
23.9 + keywords "problem" "method" :: thy_decl
23.10 + and "Author" "Method" "CAS" "Program" "Given" "Where" "Find" "Relate"
23.11 begin
23.12 ML_file thmC.sml
23.13 ML_file problem.sml
24.1 --- a/src/Tools/isac/MathEngBasic/problem.sml Sun Jun 20 12:45:03 2021 +0200
24.2 +++ b/src/Tools/isac/MathEngBasic/problem.sml Sun Jun 20 16:26:18 2021 +0200
24.3 @@ -18,6 +18,13 @@
24.4 (* TODO: ---------- remove always empty --- vvvvvvvvvvv -- vvv*)
24.5 val prep_input : theory -> Check_Unique.id -> string list -> id -> input -> T * id
24.6
24.7 + val set_data: Rule_Def.rule_set -> theory -> theory
24.8 + val the_data: theory -> Rule_Def.rule_set
24.9 +
24.10 + val parse_item: string parser -> 'a parser -> 'a parser
24.11 + val parse_model_input: model_input parser
24.12 + val parse_authors: string list parser
24.13 +
24.14 val from_store: id -> T
24.15 end
24.16
24.17 @@ -64,7 +71,7 @@
24.18
24.19 (* prepare problem-types before storing in pbltypes;
24.20 dont forget to "check_guh_unique" before ins *)
24.21 -fun prep_input thy guh maa init (pblID, dsc_dats, ev, ca, metIDs) =
24.22 +fun prep_input thy guh maa init ((pblID, dsc_dats, ev, ca, metIDs): input) : T * id =
24.23 let
24.24 fun eq f (f', _) = f = f';
24.25 val gi = filter (eq "#Given") dsc_dats;
24.26 @@ -112,6 +119,74 @@
24.27 end;
24.28
24.29
24.30 +(** Isar command **)
24.31 +
24.32 +(* theory data *)
24.33 +
24.34 +structure Data = Theory_Data
24.35 +(
24.36 + type T = Rule_Def.rule_set option;
24.37 + val empty = NONE;
24.38 + val extend = I;
24.39 + fun merge _ = NONE;
24.40 +);
24.41 +
24.42 +val set_data = Data.put o SOME;
24.43 +val the_data = the o Data.get;
24.44 +
24.45 +
24.46 +(* auxiliary parsers *)
24.47 +
24.48 +fun parse_item (keyword: string parser) (parse: 'a parser) =
24.49 + (keyword -- Args.colon) |-- Parse.!!! parse;
24.50 +
24.51 +fun parse_tagged_terms keyword (tag: string) =
24.52 + Scan.optional (parse_item keyword (Scan.repeat Parse.term) >> (fn ts => [(tag, ts)])) [];
24.53 +
24.54 +val parse_model_input : model_input parser =
24.55 + parse_tagged_terms \<^keyword>\<open>Given\<close> "#Given" @@@
24.56 + parse_tagged_terms \<^keyword>\<open>Where\<close> "#Where" @@@
24.57 + parse_tagged_terms \<^keyword>\<open>Find\<close> "#Find" @@@
24.58 + parse_tagged_terms \<^keyword>\<open>Relate\<close> "#Relate";
24.59 +
24.60 +val parse_authors =
24.61 + Scan.optional (parse_item \<^keyword>\<open>Author\<close> (Scan.repeat1 Parse.name)) [];
24.62 +
24.63 +
24.64 +(* command definition *)
24.65 +
24.66 +local
24.67 +
24.68 +val parse_methods =
24.69 + Scan.optional (parse_item \<^keyword>\<open>Method\<close> (Scan.repeat1 Parse.name)) [];
24.70 +
24.71 +val parse_cas = Scan.option (parse_item \<^keyword>\<open>CAS\<close> Parse.term);
24.72 +
24.73 +val ml = ML_Lex.read;
24.74 +
24.75 +val _ =
24.76 + Outer_Syntax.command \<^command_keyword>\<open>problem\<close>
24.77 + "prepare ISAC problem type and register it to Knowledge Store"
24.78 + (Parse.name -- Parse.!!! (\<^keyword>\<open>:\<close> |-- Parse.name --
24.79 + Parse.!!! (\<^keyword>\<open>=\<close> |-- Parse.ML_source -- parse_authors --
24.80 + parse_methods -- parse_cas -- parse_model_input)) >>
24.81 + (fn (name, (id, ((((source, maa), mets), cas), model_input))) =>
24.82 + Toplevel.theory (fn thy =>
24.83 + let
24.84 + val pblID = References_Def.explode_id id;
24.85 + val metIDs = map References_Def.explode_id mets;
24.86 + val eval_data =
24.87 + ML_Context.expression (Input.pos_of source)
24.88 + (ml "Theory.setup (Problem.set_data (" @ ML_Lex.read_source source @ ml "))")
24.89 + |> Context.theory_map;
24.90 + val input = the_data (eval_data thy);
24.91 + val arg = prep_input thy name maa id_empty (pblID, model_input, input, cas, metIDs);
24.92 + in KEStore_Elems.add_pbts [arg] thy end)))
24.93 +
24.94 +in end;
24.95 +
24.96 +
24.97 +
24.98 (** get MethodC from Store **)
24.99
24.100 fun from_store id = Store.get (get_ptyps ()) id (rev id);