1.1 --- a/src/Tools/isac/BridgeJEdit/Demo_Example.thy Wed Jun 01 13:39:41 2022 +0200
1.2 +++ b/src/Tools/isac/BridgeJEdit/Demo_Example.thy Wed Jun 01 14:17:23 2022 +0200
1.3 @@ -148,7 +148,7 @@
1.4 \<close>
1.5
1.6 Example "Biegelinien" =
1.7 - Method: "IntegrierenUndKonstanteBestimmen2"
1.8 + Method_Ref: "IntegrierenUndKonstanteBestimmen2"
1.9 CAS: "Diff (f_f, v_v) still a string"
1.10 Given: \<open>Traegerlaenge l_l" "Streckenlast q_q\<close>
1.11 Where: \<open>0 < l_l\<close>
2.1 --- a/src/Tools/isac/Knowledge/AlgEin.thy Wed Jun 01 13:39:41 2022 +0200
2.2 +++ b/src/Tools/isac/Knowledge/AlgEin.thy Wed Jun 01 14:17:23 2022 +0200
2.3 @@ -24,7 +24,7 @@
2.4 problem pbl_algein : "Berechnung" = \<open>Rule_Set.empty\<close>
2.5
2.6 problem pbl_algein_numsym : "numerischSymbolische/Berechnung" = \<open>Rule_Set.empty\<close>
2.7 - Method: "Berechnung/erstNumerisch" "Berechnung/erstSymbolisch"
2.8 + Method_Ref: "Berechnung/erstNumerisch" "Berechnung/erstSymbolisch"
2.9 Given: "KantenLaenge k_k" "Querschnitt q__q" (*q_ in Biegelinie.thy*) "KantenUnten u_u"
2.10 "KantenSenkrecht s_s" "KantenOben o_o"
2.11 Find: "GesamtLaenge l_l"
3.1 --- a/src/Tools/isac/Knowledge/Biegelinie.thy Wed Jun 01 13:39:41 2022 +0200
3.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy Wed Jun 01 14:17:23 2022 +0200
3.3 @@ -104,7 +104,7 @@
3.4
3.5 problem pbl_bieg : "Biegelinien" =
3.6 \<open>Rule_Set.append_rules "empty" Rule_Set.empty []\<close>
3.7 - Method: "IntegrierenUndKonstanteBestimmen2"
3.8 + Method_Ref: "IntegrierenUndKonstanteBestimmen2"
3.9 Given: "Traegerlaenge l_l" "Streckenlast q_q"
3.10 (* Where: "0 < l_l" ...wait for < and handling Arbfix*)
3.11 Find: "Biegelinie b_b"
3.12 @@ -112,7 +112,7 @@
3.13
3.14 problem pbl_bieg_mom : "MomentBestimmte/Biegelinien" =
3.15 \<open>Rule_Set.append_rules "empty" Rule_Set.empty []\<close>
3.16 - Method: "IntegrierenUndKonstanteBestimmen"
3.17 + Method_Ref: "IntegrierenUndKonstanteBestimmen"
3.18 Given: "Traegerlaenge l_l" "Streckenlast q_q"
3.19 (* Where: "0 < l_l" ...wait for < and handling Arbfix*)
3.20 Find: "Biegelinie b_b"
3.21 @@ -120,31 +120,31 @@
3.22
3.23 problem pbl_bieg_momg : "MomentGegebene/Biegelinien" =
3.24 \<open>Rule_Set.append_rules "empty" Rule_Set.empty []\<close>
3.25 - Method: "IntegrierenUndKonstanteBestimmen/2xIntegrieren"
3.26 + Method_Ref: "IntegrierenUndKonstanteBestimmen/2xIntegrieren"
3.27
3.28 problem pbl_bieg_einf : "einfache/Biegelinien" =
3.29 \<open>Rule_Set.append_rules "empty" Rule_Set.empty []\<close>
3.30 - Method: "IntegrierenUndKonstanteBestimmen/4x4System"
3.31 + Method_Ref: "IntegrierenUndKonstanteBestimmen/4x4System"
3.32
3.33 problem pbl_bieg_momquer : "QuerkraftUndMomentBestimmte/Biegelinien" =
3.34 \<open>Rule_Set.append_rules "empty" Rule_Set.empty []\<close>
3.35 - Method: "IntegrierenUndKonstanteBestimmen/1xIntegrieren"
3.36 + Method_Ref: "IntegrierenUndKonstanteBestimmen/1xIntegrieren"
3.37
3.38 problem pbl_bieg_vonq : "vonBelastungZu/Biegelinien" =
3.39 \<open>Rule_Set.append_rules "empty" Rule_Set.empty []\<close>
3.40 - Method: "Biegelinien/ausBelastung"
3.41 + Method_Ref: "Biegelinien/ausBelastung"
3.42 Given: "Streckenlast q_q" "FunktionsVariable v_v"
3.43 Find: "Funktionen funs'''"
3.44
3.45 problem pbl_bieg_randbed : "setzeRandbedingungen/Biegelinien" =
3.46 \<open>Rule_Set.append_rules "empty" Rule_Set.empty []\<close>
3.47 - Method: "Biegelinien/setzeRandbedingungenEin"
3.48 + Method_Ref: "Biegelinien/setzeRandbedingungenEin"
3.49 Given: "Funktionen fun_s" "Randbedingungen r_b"
3.50 Find: "Gleichungen equs'''"
3.51
3.52 problem pbl_equ_fromfun : "makeFunctionTo/equation" =
3.53 \<open>Rule_Set.append_rules "empty" Rule_Set.empty []\<close>
3.54 - Method: "Equation/fromFunction"
3.55 + Method_Ref: "Equation/fromFunction"
3.56 Given: "functionEq fu_n" "substitution su_b"
3.57 Find: "equality equ'''"
3.58
4.1 --- a/src/Tools/isac/Knowledge/Diff.thy Wed Jun 01 13:39:41 2022 +0200
4.2 +++ b/src/Tools/isac/Knowledge/Diff.thy Wed Jun 01 14:17:23 2022 +0200
4.3 @@ -227,7 +227,7 @@
4.4
4.5 problem pbl_fun_deriv : "derivative_of/function" =
4.6 \<open>Rule_Set.append_rules "empty" Rule_Set.empty []\<close>
4.7 - Method: "diff/differentiate_on_R" "diff/after_simplification"
4.8 + Method_Ref: "diff/differentiate_on_R" "diff/after_simplification"
4.9 CAS: "Diff (f_f, v_v)"
4.10 Given: "functionTerm f_f" "differentiateFor v_v"
4.11 Find: "derivative f_f'"
4.12 @@ -235,7 +235,7 @@
4.13 problem pbl_fun_deriv_nam :
4.14 "named/derivative_of/function" (*here "named" is used differently from Integration"*) =
4.15 \<open>Rule_Set.append_rules "empty" Rule_Set.empty []\<close>
4.16 - Method: "diff/differentiate_equality"
4.17 + Method_Ref: "diff/differentiate_equality"
4.18 CAS: "Differentiate (f_f, v_v)"
4.19 Given: "functionEq f_f" "differentiateFor v_v"
4.20 Find: "derivativeEq f_f'"
4.21 @@ -385,7 +385,7 @@
4.22 Find: "derivative term'"
4.23
4.24 cas Diff = \<open>argl2dtss\<close>
4.25 - Problem: "derivative_of/function"
4.26 + Problem_Ref: "derivative_of/function"
4.27
4.28 ML \<open>
4.29
4.30 @@ -402,7 +402,7 @@
4.31 | argl2dtss _ = raise ERROR "Diff.ML: wrong argument for argl2dtss";
4.32 \<close>
4.33 cas Differentiate = \<open>argl2dtss\<close>
4.34 - Problem: "named/derivative_of/function"
4.35 + Problem_Ref: "named/derivative_of/function"
4.36 ML \<open>
4.37 \<close> ML \<open>
4.38 \<close>
5.1 --- a/src/Tools/isac/Knowledge/DiffApp.thy Wed Jun 01 13:39:41 2022 +0200
5.2 +++ b/src/Tools/isac/Knowledge/DiffApp.thy Wed Jun 01 14:17:23 2022 +0200
5.3 @@ -74,13 +74,13 @@
5.4
5.5 problem pbl_fun_max_expl : "by_explicit/make/function" =
5.6 \<open>Rule_Set.empty\<close>
5.7 - Method: "DiffApp/make_fun_by_explicit"
5.8 + Method_Ref: "DiffApp/make_fun_by_explicit"
5.9 Given: "functionOf f_f" "boundVariable v_v" "equalities eqs"
5.10 Find: "functionEq f_1"
5.11
5.12 problem pbl_fun_max_newvar : "by_new_variable/make/function" =
5.13 \<open>Rule_Set.empty\<close>
5.14 - Method: "DiffApp/make_fun_by_new_variable"
5.15 + Method_Ref: "DiffApp/make_fun_by_new_variable"
5.16 Given: "functionOf f_f" "boundVariable v_v" "equalities eqs"
5.17 (*WN.12.5.03: precond for distinction still missing*)
5.18 Find: "functionEq f_1"
6.1 --- a/src/Tools/isac/Knowledge/DiophantEq.thy Wed Jun 01 13:39:41 2022 +0200
6.2 +++ b/src/Tools/isac/Knowledge/DiophantEq.thy Wed Jun 01 14:17:23 2022 +0200
6.3 @@ -15,7 +15,7 @@
6.4
6.5 problem pbl_equ_dio : "diophantine/equation" =
6.6 \<open>Rule_Set.empty\<close>
6.7 - Method: "LinEq/solve_lineq_equation"
6.8 + Method_Ref: "LinEq/solve_lineq_equation"
6.9 CAS: "solve (e_e::bool, v_v::int)"
6.10 Given: "boolTestGiven e_e" "intTestGiven (v_v::int)"
6.11 (* TODO: drop ^^^^^*)
7.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Wed Jun 01 13:39:41 2022 +0200
7.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Wed Jun 01 14:17:23 2022 +0200
7.3 @@ -403,7 +403,7 @@
7.4
7.5 problem pbl_equsys_lin_2x2_tri : "triangular/2x2/LINEAR/system" =
7.6 \<open>prls_triangular\<close>
7.7 - Method: "EqSystem/top_down_substitution/2x2"
7.8 + Method_Ref: "EqSystem/top_down_substitution/2x2"
7.9 CAS: "solveSystem e_s v_s"
7.10 Given: "equalities e_s" "solveForVars v_s"
7.11 Where:
7.12 @@ -413,7 +413,7 @@
7.13
7.14 problem pbl_equsys_lin_2x2_norm : "normalise/2x2/LINEAR/system" =
7.15 \<open>Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)]\<close>
7.16 - Method: "EqSystem/normalise/2x2"
7.17 + Method_Ref: "EqSystem/normalise/2x2"
7.18 CAS: "solveSystem e_s v_s"
7.19 Given: "equalities e_s" "solveForVars v_s"
7.20 Find: "solution ss'''"
7.21 @@ -443,7 +443,7 @@
7.22 problem pbl_equsys_lin_4x4_tri : "triangular/4x4/LINEAR/system" =
7.23 \<open>Rule_Set.append_rules "prls_tri_4x4_lin_sys" prls_triangular
7.24 [\<^rule_eval>\<open>Prog_Expr.occurs_in\<close> (Prog_Expr.eval_occurs_in "")]\<close>
7.25 - Method: "EqSystem/top_down_substitution/4x4"
7.26 + Method_Ref: "EqSystem/top_down_substitution/4x4"
7.27 CAS: "solveSystem e_s v_s"
7.28 Given: "equalities e_s" "solveForVars v_s"
7.29 Where: (*accepts missing variables up to diagional form*)
7.30 @@ -455,7 +455,7 @@
7.31
7.32 problem pbl_equsys_lin_4x4_norm : "normalise/4x4/LINEAR/system" =
7.33 \<open>Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)]\<close>
7.34 - Method: "EqSystem/normalise/4x4"
7.35 + Method_Ref: "EqSystem/normalise/4x4"
7.36 CAS: "solveSystem e_s v_s"
7.37 Given: "equalities e_s" "solveForVars v_s"
7.38 (*Length is checked 1 level above*)
8.1 --- a/src/Tools/isac/Knowledge/Equation.thy Wed Jun 01 13:39:41 2022 +0200
8.2 +++ b/src/Tools/isac/Knowledge/Equation.thy Wed Jun 01 14:17:23 2022 +0200
8.3 @@ -66,10 +66,10 @@
8.4 | argl2dtss _ = raise ERROR "Equation.ML: wrong argument for argl2dtss";
8.5 \<close>
8.6 cas solveTest = \<open>argl2dtss\<close>
8.7 - Theory: Test
8.8 - Problem: "univariate/equation/test"
8.9 + Theory_Ref: Test
8.10 + Problem_Ref: "univariate/equation/test"
8.11 cas solve = \<open>argl2dtss\<close>
8.12 - Problem: "univariate/equation"
8.13 + Problem_Ref: "univariate/equation"
8.14
8.15 method met_equ : "Equation" =
8.16 \<open>{rew_ord' = "tless_true", rls' = Rule_Set.Empty, calc = [], srls = Rule_Set.empty,
9.1 --- a/src/Tools/isac/Knowledge/InsSort.thy Wed Jun 01 13:39:41 2022 +0200
9.2 +++ b/src/Tools/isac/Knowledge/InsSort.thy Wed Jun 01 14:17:23 2022 +0200
9.3 @@ -78,7 +78,7 @@
9.4
9.5 problem pbl_Prog_sort_ins : "insertion/SORT/Programming" =
9.6 \<open>Rule_Set.empty\<close>
9.7 - Method: "Programming/SORT/insertion_steps"
9.8 + Method_Ref: "Programming/SORT/insertion_steps"
9.9 CAS: "Sort u_u"
9.10 Given: "unsorted u_u"
9.11 Find: "sorted s_s"
9.12 @@ -151,8 +151,8 @@
9.13 \<close>
9.14 (* combine input with other data required for formal specification *)
9.15 cas Sort = \<open>argl2dtss\<close>
9.16 - Theory: InsSort
9.17 - Problem: "insertion/SORT/Programming"
9.18 + Theory_Ref: InsSort
9.19 + Problem_Ref: "insertion/SORT/Programming"
9.20 ML \<open>
9.21 \<close> ML \<open>
9.22 \<close>
10.1 --- a/src/Tools/isac/Knowledge/Integrate.thy Wed Jun 01 13:39:41 2022 +0200
10.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy Wed Jun 01 14:17:23 2022 +0200
10.3 @@ -258,7 +258,7 @@
10.4
10.5 problem pbl_fun_integ : "integrate/function" =
10.6 \<open>Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)]\<close>
10.7 - Method: "diff/integration"
10.8 + Method_Ref: "diff/integration"
10.9 CAS: "Integrate (f_f, v_v)"
10.10 Given: "functionTerm f_f" "integrateBy v_v"
10.11 Find: "antiDerivative F_F"
10.12 @@ -266,7 +266,7 @@
10.13 problem pbl_fun_integ_nam : "named/integrate/function" =
10.14 (*here "named" is used differently from Differentiation"*)
10.15 \<open>Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)]\<close>
10.16 - Method: "diff/integration/named"
10.17 + Method_Ref: "diff/integration/named"
10.18 CAS: "Integrate (f_f, v_v)"
10.19 Given: "functionTerm f_f" "integrateBy v_v"
10.20 Find: "antiDerivativeName F_F"
11.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Wed Jun 01 13:39:41 2022 +0200
11.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Wed Jun 01 14:17:23 2022 +0200
11.3 @@ -49,7 +49,7 @@
11.4
11.5 problem pbl_SP_Ztrans_inv : "Inverse/Z_Transform/SignalProcessing" =
11.6 \<open>Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)]\<close>
11.7 - Method: "SignalProcessing/Z_Transform/Inverse"
11.8 + Method_Ref: "SignalProcessing/Z_Transform/Inverse"
11.9 Given: "filterExpression X_eq"
11.10 Find: "stepResponse n_eq" \<comment> \<open>TODO: unused, "u [n]" is introduced by rule1..6\<close>
11.11
12.1 --- a/src/Tools/isac/Knowledge/LinEq.thy Wed Jun 01 13:39:41 2022 +0200
12.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy Wed Jun 01 14:17:23 2022 +0200
12.3 @@ -105,7 +105,7 @@
12.4
12.5 problem pbl_equ_univ_lin : "LINEAR/univariate/equation" =
12.6 \<open>LinEq_prls\<close>
12.7 - Method: "LinEq/solve_lineq_equation"
12.8 + Method_Ref: "LinEq/solve_lineq_equation"
12.9 CAS: "solve (e_e::bool, v_v)"
12.10 Given: "equality e_e" "solveFor v_v"
12.11 Where: "HOL.False" (*WN0509 just detected: this pbl can never be used?!?*)
13.1 --- a/src/Tools/isac/Knowledge/LogExp.thy Wed Jun 01 13:39:41 2022 +0200
13.2 +++ b/src/Tools/isac/Knowledge/LogExp.thy Wed Jun 01 14:17:23 2022 +0200
13.3 @@ -20,7 +20,7 @@
13.4
13.5 problem pbl_test_equ_univ_log : "logarithmic/univariate/equation" =
13.6 \<open>PolyEq_prls\<close>
13.7 - Method: "Equation/solve_log"
13.8 + Method_Ref: "Equation/solve_log"
13.9 CAS: "solve (e_e::bool, v_v)"
13.10 Given: "equality e_e" "solveFor v_v"
13.11 Where: "matches ((?a log ?v_v) = ?b) e_e"
14.1 --- a/src/Tools/isac/Knowledge/Partial_Fractions.thy Wed Jun 01 13:39:41 2022 +0200
14.2 +++ b/src/Tools/isac/Knowledge/Partial_Fractions.thy Wed Jun 01 14:17:23 2022 +0200
14.3 @@ -146,7 +146,7 @@
14.4 \<close>
14.5 problem pbl_simp_rat_partfrac : "partial_fraction/rational/simplification" =
14.6 \<open>Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_ TODO*)]\<close>
14.7 - Method: "simplification/of_rationals/to_partial_fraction"
14.8 + Method_Ref: "simplification/of_rationals/to_partial_fraction"
14.9 Given: "functionTerm t_t" "solveFor v_v"
14.10 (* TODO: call this sub-problem with appropriate functionTerm:
14.11 leading coefficient of the denominator is 1: to be checked here! and..
15.1 --- a/src/Tools/isac/Knowledge/Poly.thy Wed Jun 01 13:39:41 2022 +0200
15.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Wed Jun 01 14:17:23 2022 +0200
15.3 @@ -1352,7 +1352,7 @@
15.4 problem pbl_simp_poly : "polynomial/simplification" =
15.5 \<open>Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)
15.6 \<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp "")]\<close>
15.7 - Method: "simplification/for_polynomials"
15.8 + Method_Ref: "simplification/for_polynomials"
15.9 CAS: "Simplify t_t"
15.10 Given: "Term t_t"
15.11 Where: "t_t is_polyexp"
16.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Wed Jun 01 13:39:41 2022 +0200
16.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Wed Jun 01 14:17:23 2022 +0200
16.3 @@ -639,7 +639,7 @@
16.4 (*--- d0 ---*)
16.5 problem pbl_equ_univ_poly_deg0 : "degree_0/polynomial/univariate/equation" =
16.6 \<open>PolyEq_prls\<close>
16.7 - Method: "PolyEq/solve_d0_polyeq_equation"
16.8 + Method_Ref: "PolyEq/solve_d0_polyeq_equation"
16.9 CAS: "solve (e_e::bool, v_v)"
16.10 Given: "equality e_e" "solveFor v_v"
16.11 Where:
16.12 @@ -651,7 +651,7 @@
16.13 (*--- d1 ---*)
16.14 problem pbl_equ_univ_poly_deg1 : "degree_1/polynomial/univariate/equation" =
16.15 \<open>PolyEq_prls\<close>
16.16 - Method: "PolyEq/solve_d1_polyeq_equation"
16.17 + Method_Ref: "PolyEq/solve_d1_polyeq_equation"
16.18 CAS: "solve (e_e::bool, v_v)"
16.19 Given: "equality e_e" "solveFor v_v"
16.20 Where:
16.21 @@ -663,7 +663,7 @@
16.22 (*--- d2 ---*)
16.23 problem pbl_equ_univ_poly_deg2 : "degree_2/polynomial/univariate/equation" =
16.24 \<open>PolyEq_prls\<close>
16.25 - Method: "PolyEq/solve_d2_polyeq_equation"
16.26 + Method_Ref: "PolyEq/solve_d2_polyeq_equation"
16.27 CAS: "solve (e_e::bool, v_v)"
16.28 Given: "equality e_e" "solveFor v_v"
16.29 Where:
16.30 @@ -674,7 +674,7 @@
16.31
16.32 problem pbl_equ_univ_poly_deg2_sqonly : "sq_only/degree_2/polynomial/univariate/equation" =
16.33 \<open>PolyEq_prls\<close>
16.34 - Method: "PolyEq/solve_d2_polyeq_sqonly_equation"
16.35 + Method_Ref: "PolyEq/solve_d2_polyeq_sqonly_equation"
16.36 CAS: "solve (e_e::bool, v_v)"
16.37 Given: "equality e_e" "solveFor v_v"
16.38 Where:
16.39 @@ -694,7 +694,7 @@
16.40
16.41 problem pbl_equ_univ_poly_deg2_bdvonly : "bdv_only/degree_2/polynomial/univariate/equation" =
16.42 \<open>PolyEq_prls\<close>
16.43 - Method: "PolyEq/solve_d2_polyeq_bdvonly_equation"
16.44 + Method_Ref: "PolyEq/solve_d2_polyeq_bdvonly_equation"
16.45 CAS: "solve (e_e::bool, v_v)"
16.46 Given: "equality e_e" "solveFor v_v"
16.47 Where:
16.48 @@ -708,7 +708,7 @@
16.49
16.50 problem pbl_equ_univ_poly_deg2_pq : "pqFormula/degree_2/polynomial/univariate/equation" =
16.51 \<open>PolyEq_prls\<close>
16.52 - Method: "PolyEq/solve_d2_polyeq_pq_equation"
16.53 + Method_Ref: "PolyEq/solve_d2_polyeq_pq_equation"
16.54 CAS: "solve (e_e::bool, v_v)"
16.55 Given: "equality e_e" "solveFor v_v"
16.56 Where:
16.57 @@ -718,7 +718,7 @@
16.58
16.59 problem pbl_equ_univ_poly_deg2_abc : "abcFormula/degree_2/polynomial/univariate/equation" =
16.60 \<open>PolyEq_prls\<close>
16.61 - Method: "PolyEq/solve_d2_polyeq_abc_equation"
16.62 + Method_Ref: "PolyEq/solve_d2_polyeq_abc_equation"
16.63 CAS: "solve (e_e::bool, v_v)"
16.64 Given: "equality e_e" "solveFor v_v"
16.65 Where:
16.66 @@ -729,7 +729,7 @@
16.67 (*--- d3 ---*)
16.68 problem pbl_equ_univ_poly_deg3 : "degree_3/polynomial/univariate/equation" =
16.69 \<open>PolyEq_prls\<close>
16.70 - Method: "PolyEq/solve_d3_polyeq_equation"
16.71 + Method_Ref: "PolyEq/solve_d3_polyeq_equation"
16.72 CAS: "solve (e_e::bool, v_v)"
16.73 Given: "equality e_e" "solveFor v_v"
16.74 Where:
16.75 @@ -753,7 +753,7 @@
16.76 (*--- normalise ---*)
16.77 problem pbl_equ_univ_poly_norm : "normalise/polynomial/univariate/equation" =
16.78 \<open>PolyEq_prls\<close>
16.79 - Method: "PolyEq/normalise_poly"
16.80 + Method_Ref: "PolyEq/normalise_poly"
16.81 CAS: "solve (e_e::bool, v_v)"
16.82 Given: "equality e_e" "solveFor v_v"
16.83 Where:
16.84 @@ -774,7 +774,7 @@
16.85 (*--- d2 ---*)
16.86 problem pbl_equ_univ_expand_deg2 : "degree_2/expanded/univariate/equation" =
16.87 \<open>PolyEq_prls\<close>
16.88 - Method: "PolyEq/complete_square"
16.89 + Method_Ref: "PolyEq/complete_square"
16.90 CAS: "solve (e_e::bool, v_v)"
16.91 Given: "equality e_e" "solveFor v_v"
16.92 Where: "((lhs e_e) has_degree_in v_v) = 2"
17.1 --- a/src/Tools/isac/Knowledge/PolyMinus.thy Wed Jun 01 13:39:41 2022 +0200
17.2 +++ b/src/Tools/isac/Knowledge/PolyMinus.thy Wed Jun 01 14:17:23 2022 +0200
17.3 @@ -340,7 +340,7 @@
17.4 \<^rule_thm>\<open>or_false\<close>, (*"(?a | False) = ?a"*)
17.5 \<^rule_thm>\<open>not_true\<close>, (*"(~ True) = False"*)
17.6 \<^rule_thm>\<open>not_false\<close> (*"(~ False) = True"*)]\<close>
17.7 - Method: "simplification/for_polynomials/with_minus"
17.8 + Method_Ref: "simplification/for_polynomials/with_minus"
17.9 CAS: "Vereinfache t_t"
17.10 Given: "Term t_t"
17.11 Where:
17.12 @@ -363,7 +363,7 @@
17.13 \<^rule_thm>\<open>or_false\<close>, (*"(?a | False) = ?a"*)
17.14 \<^rule_thm>\<open>not_true\<close>, (*"(~ True) = False"*)
17.15 \<^rule_thm>\<open>not_false\<close> (*"(~ False) = True"*)]\<close>
17.16 - Method: "simplification/for_polynomials/with_parentheses"
17.17 + Method_Ref: "simplification/for_polynomials/with_parentheses"
17.18 CAS: "Vereinfache t_t"
17.19 Given: "Term t_t"
17.20 Where:
17.21 @@ -377,7 +377,7 @@
17.22 problem pbl_vereinf_poly_klammer_mal : "binom_klammer/polynom/vereinfachen" =
17.23 \<open>Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)
17.24 \<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp "")]\<close>
17.25 - Method: "simplification/for_polynomials/with_parentheses_mult"
17.26 + Method_Ref: "simplification/for_polynomials/with_parentheses_mult"
17.27 CAS: "Vereinfache t_t"
17.28 Given: "Term t_t"
17.29 Where: "t_t is_polyexp"
17.30 @@ -388,7 +388,7 @@
17.31 problem pbl_probe_poly : "polynom/probe" =
17.32 \<open>Rule_Set.append_rules "prls_pbl_probe_poly" Rule_Set.empty [(*for preds in where_*)
17.33 \<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp "")]\<close>
17.34 - Method: "probe/fuer_polynom"
17.35 + Method_Ref: "probe/fuer_polynom"
17.36 CAS: "Probe e_e w_w"
17.37 Given: "Pruefe e_e" "mitWert w_w"
17.38 Where: "e_e is_polyexp"
17.39 @@ -397,7 +397,7 @@
17.40 problem pbl_probe_bruch : "bruch/probe" =
17.41 \<open>Rule_Set.append_rules "prls_pbl_probe_bruch" Rule_Set.empty [(*for preds in where_*)
17.42 \<^rule_eval>\<open>is_ratpolyexp\<close> (eval_is_ratpolyexp "")]\<close>
17.43 - Method: "probe/fuer_bruch"
17.44 + Method_Ref: "probe/fuer_bruch"
17.45 CAS: "Probe e_e w_w"
17.46 Given: "Pruefe e_e" "mitWert w_w"
17.47 Where: "e_e is_ratpolyexp"
18.1 --- a/src/Tools/isac/Knowledge/RatEq.thy Wed Jun 01 13:39:41 2022 +0200
18.2 +++ b/src/Tools/isac/Knowledge/RatEq.thy Wed Jun 01 14:17:23 2022 +0200
18.3 @@ -147,7 +147,7 @@
18.4
18.5 problem pbl_equ_univ_rat : "rational/univariate/equation" =
18.6 \<open>RatEq_prls\<close>
18.7 - Method: "RatEq/solve_rat_equation"
18.8 + Method_Ref: "RatEq/solve_rat_equation"
18.9 CAS: "solve (e_e::bool, v_v)"
18.10 Given: "equality e_e" "solveFor v_v"
18.11 Where: "(e_e::bool) is_ratequation_in (v_v::real)"
19.1 --- a/src/Tools/isac/Knowledge/Rational.thy Wed Jun 01 13:39:41 2022 +0200
19.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Wed Jun 01 14:17:23 2022 +0200
19.3 @@ -831,7 +831,7 @@
19.4
19.5 problem pbl_simp_rat : "rational/simplification" =
19.6 \<open>Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)]\<close>
19.7 - Method: "simplification/of_rationals"
19.8 + Method_Ref: "simplification/of_rationals"
19.9 CAS: "Simplify t_t"
19.10 Given: "Term t_t"
19.11 Where: "t_t is_ratpolyexp"
20.1 --- a/src/Tools/isac/Knowledge/RootEq.thy Wed Jun 01 13:39:41 2022 +0200
20.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy Wed Jun 01 14:17:23 2022 +0200
20.3 @@ -355,7 +355,7 @@
20.4
20.5 problem pbl_equ_univ_root_sq : "sq/rootX/univariate/equation" =
20.6 \<open>RootEq_prls\<close>
20.7 - Method: "RootEq/solve_sq_root_equation"
20.8 + Method_Ref: "RootEq/solve_sq_root_equation"
20.9 CAS: "solve (e_e::bool, v_v)"
20.10 Given: "equality e_e" "solveFor v_v"
20.11 Where:
20.12 @@ -368,7 +368,7 @@
20.13 (* ---------normalise----------- *)
20.14 problem pbl_equ_univ_root_norm : "normalise/rootX/univariate/equation" =
20.15 \<open>RootEq_prls\<close>
20.16 - Method: "RootEq/norm_sq_root_equation"
20.17 + Method_Ref: "RootEq/norm_sq_root_equation"
20.18 CAS: "solve (e_e::bool, v_v)"
20.19 Given: "equality e_e" "solveFor v_v"
20.20 Where:
21.1 --- a/src/Tools/isac/Knowledge/RootRatEq.thy Wed Jun 01 13:39:41 2022 +0200
21.2 +++ b/src/Tools/isac/Knowledge/RootRatEq.thy Wed Jun 01 14:17:23 2022 +0200
21.3 @@ -115,7 +115,7 @@
21.4
21.5 problem pbl_equ_univ_root_sq_rat : "rat/sq/rootX/univariate/equation" =
21.6 \<open>RootRatEq_prls\<close>
21.7 - Method: "RootRatEq/elim_rootrat_equation"
21.8 + Method_Ref: "RootRatEq/elim_rootrat_equation"
21.9 CAS: "solve (e_e::bool, v_v)"
21.10 Given: "equality e_e" "solveFor v_v"
21.11 Where: "( (lhs e_e) is_rootRatAddTerm_in (v_v::real) ) |
22.1 --- a/src/Tools/isac/Knowledge/Simplify.thy Wed Jun 01 13:39:41 2022 +0200
22.2 +++ b/src/Tools/isac/Knowledge/Simplify.thy Wed Jun 01 14:17:23 2022 +0200
22.3 @@ -55,9 +55,9 @@
22.4 (*| argl2dtss _ = raise ERROR "Simplify.ML: wrong argument for argl2dtss"*);
22.5 \<close>
22.6 cas Simplify = \<open>argl2dtss\<close>
22.7 - Problem: "simplification"
22.8 + Problem_Ref: "simplification"
22.9 cas Vereinfache = \<open>argl2dtss\<close>
22.10 - Problem: "vereinfachen"
22.11 + Problem_Ref: "vereinfachen"
22.12
22.13 ML \<open>
22.14 \<close> ML \<open>
23.1 --- a/src/Tools/isac/Knowledge/Test.thy Wed Jun 01 13:39:41 2022 +0200
23.2 +++ b/src/Tools/isac/Knowledge/Test.thy Wed Jun 01 14:17:23 2022 +0200
23.3 @@ -581,7 +581,7 @@
23.4
23.5 problem pbl_test_uni_lin : "LINEAR/univariate/equation/test" =
23.6 \<open>assoc_rls' @{theory} "matches"\<close>
23.7 - Method: "Test/solve_linear"
23.8 + Method_Ref: "Test/solve_linear"
23.9 CAS: "solve (e_e::bool, v_v)"
23.10 Given: "equality e_e" "solveFor v_v"
23.11 Where:
23.12 @@ -696,7 +696,7 @@
23.13
23.14 problem pbl_test_uni_plain2 : "plain_square/univariate/equation/test" =
23.15 \<open>assoc_rls' @{theory} "matches"\<close>
23.16 - Method: "Test/solve_plain_square"
23.17 + Method_Ref: "Test/solve_plain_square"
23.18 CAS: "solve (e_e::bool, v_v)"
23.19 Given: "equality e_e" "solveFor v_v"
23.20 Where:
23.21 @@ -734,7 +734,7 @@
23.22 problem pbl_test_uni_root : "squareroot/univariate/equation/test" =
23.23 \<open>Rule_Set.append_rules "contains_root" Rule_Set.empty [\<^rule_eval>\<open>contains_root\<close>
23.24 (eval_contains_root "#contains_root_")]\<close>
23.25 - Method: "Test/square_equation"
23.26 + Method_Ref: "Test/square_equation"
23.27 CAS: "solve (e_e::bool, v_v)"
23.28 Given: "equality e_e" "solveFor v_v"
23.29 Where: "precond_rootpbl v_v"
23.30 @@ -742,7 +742,7 @@
23.31
23.32 problem pbl_test_uni_norm : "normalise/univariate/equation/test" =
23.33 \<open>Rule_Set.empty\<close>
23.34 - Method: "Test/norm_univar_equation"
23.35 + Method_Ref: "Test/norm_univar_equation"
23.36 CAS: "solve (e_e::bool, v_v)"
23.37 Given: "equality e_e" "solveFor v_v"
23.38 Where:
23.39 @@ -757,7 +757,7 @@
23.40
23.41 problem pbl_test_intsimp : "inttype/test" =
23.42 \<open>Rule_Set.empty\<close>
23.43 - Method: "Test/intsimp"
23.44 + Method_Ref: "Test/intsimp"
23.45 Given: "intTestGiven t_t"
23.46 Where:
23.47 Find: "intTestFind s_s"
24.1 --- a/src/Tools/isac/MathEngBasic/MathEngBasic.thy Wed Jun 01 13:39:41 2022 +0200
24.2 +++ b/src/Tools/isac/MathEngBasic/MathEngBasic.thy Wed Jun 01 14:17:23 2022 +0200
24.3 @@ -16,7 +16,8 @@
24.4 theory MathEngBasic
24.5 imports "$ISABELLE_ISAC/ProgLang/ProgLang" "$ISABELLE_ISAC/Specify/Input_Descript"
24.6 keywords "problem" "method" :: thy_decl
24.7 - and "Author" "Theory" "Problem" "Method" "CAS" "Program" "Given" "Where" "Find" "Relate"
24.8 + and "Author" "Theory_Ref" "Problem_Ref" "Method_Ref"
24.9 + "CAS" "Program" "Given" "Where" "Find" "Relate"
24.10 begin
24.11 ML_file thmC.sml
24.12 ML_file problem.sml
24.13 @@ -29,7 +30,7 @@
24.14 ML_file "calc-tree-elem.sml"
24.15 ML_file "pre-conds-def.sml"
24.16
24.17 - ML_file tactic.sml
24.18 + ML_file tactic.sml
24.19 ML_file applicable.sml
24.20
24.21 ML_file position.sml
25.1 --- a/src/Tools/isac/MathEngBasic/problem.sml Wed Jun 01 13:39:41 2022 +0200
25.2 +++ b/src/Tools/isac/MathEngBasic/problem.sml Wed Jun 01 14:17:23 2022 +0200
25.3 @@ -164,7 +164,7 @@
25.4
25.5 val parse_authors = parse_item_names \<^keyword>\<open>Author\<close>;
25.6 val parse_cas = Scan.option (parse_item \<^keyword>\<open>CAS\<close> Parse.term);
25.7 -val parse_methods = parse_item_names \<^keyword>\<open>Method\<close>;
25.8 +val parse_methods = parse_item_names \<^keyword>\<open>Method_Ref\<close>;
25.9 val ml = ML_Lex.read;
25.10
25.11
26.1 --- a/src/Tools/isac/Specify/cas-command.sml Wed Jun 01 13:39:41 2022 +0200
26.2 +++ b/src/Tools/isac/Specify/cas-command.sml Wed Jun 01 14:17:23 2022 +0200
26.3 @@ -88,9 +88,9 @@
26.4
26.5 local
26.6
26.7 -val parse_theory = Problem.parse_item_name \<^keyword>\<open>Theory\<close> "Isac_Knowledge";
26.8 -val parse_problem = Problem.parse_item \<^keyword>\<open>Problem\<close> Parse.name;
26.9 -val parse_method = Problem.parse_item_name \<^keyword>\<open>Method\<close> "no_met";
26.10 +val parse_theory = Problem.parse_item_name \<^keyword>\<open>Theory_Ref\<close> "Isac_Knowledge";
26.11 +val parse_problem = Problem.parse_item \<^keyword>\<open>Problem_Ref\<close> Parse.name;
26.12 +val parse_method = Problem.parse_item_name \<^keyword>\<open>Method_Ref\<close> "no_met";
26.13
26.14 val ml = ML_Lex.read;
26.15