1.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Thu Jun 10 11:54:20 2021 +0200
1.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Thu Jun 10 12:23:57 2021 +0200
1.3 @@ -407,18 +407,18 @@
1.4 section \<open>Problems\<close>
1.5
1.6 setup \<open>KEStore_Elems.add_pbts
1.7 - [(Problem.prep_input thy "pbl_equsys" [] Problem.id_empty
1.8 + [(Problem.prep_input @{theory} "pbl_equsys" [] Problem.id_empty
1.9 (["system"],
1.10 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
1.11 ("#Find" ,["solution ss'''"](*''' is copy-named*))],
1.12 Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)], SOME "solveSystem e_s v_s", [])),
1.13 - (Problem.prep_input thy "pbl_equsys_lin" [] Problem.id_empty
1.14 + (Problem.prep_input @{theory} "pbl_equsys_lin" [] Problem.id_empty
1.15 (["LINEAR", "system"],
1.16 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
1.17 (*TODO.WN050929 check linearity*)
1.18 ("#Find" ,["solution ss'''"])],
1.19 Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)], SOME "solveSystem e_s v_s", [])),
1.20 - (Problem.prep_input thy "pbl_equsys_lin_2x2" [] Problem.id_empty
1.21 + (Problem.prep_input @{theory} "pbl_equsys_lin_2x2" [] Problem.id_empty
1.22 (["2x2", "LINEAR", "system"],
1.23 (*~~~~~~~~~~~~~~~~~~~~~~~~~*)
1.24 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
1.25 @@ -430,7 +430,7 @@
1.26 Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
1.27 Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_")],
1.28 SOME "solveSystem e_s v_s", [])),
1.29 - (Problem.prep_input thy "pbl_equsys_lin_2x2_tri" [] Problem.id_empty
1.30 + (Problem.prep_input @{theory} "pbl_equsys_lin_2x2_tri" [] Problem.id_empty
1.31 (["triangular", "2x2", "LINEAR", "system"],
1.32 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
1.33 ("#Where",
1.34 @@ -438,14 +438,14 @@
1.35 " v_s from v_s occur_exactly_in (NTH 2 (e_s::bool list))"]),
1.36 ("#Find" ,["solution ss'''"])],
1.37 prls_triangular, SOME "solveSystem e_s v_s", [["EqSystem", "top_down_substitution", "2x2"]])),
1.38 - (Problem.prep_input thy "pbl_equsys_lin_2x2_norm" [] Problem.id_empty
1.39 + (Problem.prep_input @{theory} "pbl_equsys_lin_2x2_norm" [] Problem.id_empty
1.40 (["normalise", "2x2", "LINEAR", "system"],
1.41 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
1.42 ("#Find" ,["solution ss'''"])],
1.43 Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)],
1.44 SOME "solveSystem e_s v_s",
1.45 [["EqSystem", "normalise", "2x2"]])),
1.46 - (Problem.prep_input thy "pbl_equsys_lin_3x3" [] Problem.id_empty
1.47 + (Problem.prep_input @{theory} "pbl_equsys_lin_3x3" [] Problem.id_empty
1.48 (["3x3", "LINEAR", "system"],
1.49 (*~~~~~~~~~~~~~~~~~~~~~~~~~*)
1.50 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
1.51 @@ -457,7 +457,7 @@
1.52 Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
1.53 Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_")],
1.54 SOME "solveSystem e_s v_s", [])),
1.55 - (Problem.prep_input thy "pbl_equsys_lin_4x4" [] Problem.id_empty
1.56 + (Problem.prep_input @{theory} "pbl_equsys_lin_4x4" [] Problem.id_empty
1.57 (["4x4", "LINEAR", "system"],
1.58 (*~~~~~~~~~~~~~~~~~~~~~~~~~*)
1.59 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
1.60 @@ -469,7 +469,7 @@
1.61 Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
1.62 Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_")],
1.63 SOME "solveSystem e_s v_s", [])),
1.64 - (Problem.prep_input thy "pbl_equsys_lin_4x4_tri" [] Problem.id_empty
1.65 + (Problem.prep_input @{theory} "pbl_equsys_lin_4x4_tri" [] Problem.id_empty
1.66 (["triangular", "4x4", "LINEAR", "system"],
1.67 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
1.68 ("#Where" , (*accepts missing variables up to diagional form*)
1.69 @@ -482,7 +482,7 @@
1.70 [Rule.Eval ("Prog_Expr.occurs_in", Prog_Expr.eval_occurs_in "")],
1.71 SOME "solveSystem e_s v_s",
1.72 [["EqSystem", "top_down_substitution", "4x4"]])),
1.73 - (Problem.prep_input thy "pbl_equsys_lin_4x4_norm" [] Problem.id_empty
1.74 + (Problem.prep_input @{theory} "pbl_equsys_lin_4x4_norm" [] Problem.id_empty
1.75 (["normalise", "4x4", "LINEAR", "system"],
1.76 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
1.77 (*Length is checked 1 level above*)
1.78 @@ -512,12 +512,12 @@
1.79 section \<open>Methods\<close>
1.80
1.81 setup \<open>KEStore_Elems.add_mets
1.82 - [MethodC.prep_input thy "met_eqsys" [] MethodC.id_empty
1.83 + [MethodC.prep_input @{theory} "met_eqsys" [] MethodC.id_empty
1.84 (["EqSystem"], [],
1.85 {rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [], srls = Rule_Set.Empty, prls = Rule_Set.Empty, crls = Rule_Set.Empty,
1.86 errpats = [], nrls = Rule_Set.Empty},
1.87 @{thm refl}),
1.88 - MethodC.prep_input thy "met_eqsys_topdown" [] MethodC.id_empty
1.89 + MethodC.prep_input @{theory} "met_eqsys_topdown" [] MethodC.id_empty
1.90 (["EqSystem", "top_down_substitution"], [],
1.91 {rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [], srls = Rule_Set.Empty, prls = Rule_Set.Empty, crls = Rule_Set.Empty,
1.92 errpats = [], nrls = Rule_Set.Empty},
1.93 @@ -544,7 +544,7 @@
1.94 in
1.95 Try (Rewrite_Set ''order_system'' ) e__s) "
1.96 setup \<open>KEStore_Elems.add_mets
1.97 - [MethodC.prep_input thy "met_eqsys_topdown_2x2" [] MethodC.id_empty
1.98 + [MethodC.prep_input @{theory} "met_eqsys_topdown_2x2" [] MethodC.id_empty
1.99 (["EqSystem", "top_down_substitution", "2x2"],
1.100 [("#Given", ["equalities e_s", "solveForVars v_s"]),
1.101 ("#Where",
1.102 @@ -560,7 +560,7 @@
1.103 @{thm solve_system.simps})]
1.104 \<close>
1.105 setup \<open>KEStore_Elems.add_mets
1.106 - [MethodC.prep_input thy "met_eqsys_norm" [] MethodC.id_empty
1.107 + [MethodC.prep_input @{theory} "met_eqsys_norm" [] MethodC.id_empty
1.108 (["EqSystem", "normalise"], [],
1.109 {rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [], srls = Rule_Set.Empty, prls = Rule_Set.Empty, crls = Rule_Set.Empty,
1.110 errpats = [], nrls = Rule_Set.Empty},
1.111 @@ -582,7 +582,7 @@
1.112 SubProblem (''EqSystem'', [''LINEAR'', ''system''], [''no_met''])
1.113 [BOOL_LIST e__s, REAL_LIST v_s])"
1.114 setup \<open>KEStore_Elems.add_mets
1.115 - [MethodC.prep_input thy "met_eqsys_norm_2x2" [] MethodC.id_empty
1.116 + [MethodC.prep_input @{theory} "met_eqsys_norm_2x2" [] MethodC.id_empty
1.117 (["EqSystem", "normalise", "2x2"],
1.118 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
1.119 ("#Find" ,["solution ss'''"])],
1.120 @@ -614,7 +614,7 @@
1.121 SubProblem (''EqSystem'', [''LINEAR'', ''system''], [''no_met''])
1.122 [BOOL_LIST e__s, REAL_LIST v_s])"
1.123 setup \<open>KEStore_Elems.add_mets
1.124 - [MethodC.prep_input thy "met_eqsys_norm_4x4" [] MethodC.id_empty
1.125 + [MethodC.prep_input @{theory} "met_eqsys_norm_4x4" [] MethodC.id_empty
1.126 (["EqSystem", "normalise", "4x4"],
1.127 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
1.128 ("#Find" ,["solution ss'''"])],
1.129 @@ -646,7 +646,7 @@
1.130 in
1.131 [e_1, e_2, NTH 3 e_s, NTH 4 e_s])"
1.132 setup \<open>KEStore_Elems.add_mets
1.133 - [MethodC.prep_input thy "met_eqsys_topdown_4x4" [] MethodC.id_empty
1.134 + [MethodC.prep_input @{theory} "met_eqsys_topdown_4x4" [] MethodC.id_empty
1.135 (["EqSystem", "top_down_substitution", "4x4"],
1.136 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
1.137 ("#Where" , (*accepts missing variables up to diagonal form*)