1.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Wed Apr 22 11:23:30 2020 +0200
1.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Wed Apr 22 14:36:27 2020 +0200
1.3 @@ -406,18 +406,18 @@
1.4
1.5 (** problems **)
1.6 setup \<open>KEStore_Elems.add_pbts
1.7 - [(Specify.prep_pbt thy "pbl_equsys" [] Spec.e_pblID
1.8 + [(Specify.prep_pbt thy "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 - (Specify.prep_pbt thy "pbl_equsys_lin" [] Spec.e_pblID
1.14 + (Specify.prep_pbt thy "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 - (Specify.prep_pbt thy "pbl_equsys_lin_2x2" [] Spec.e_pblID
1.21 + (Specify.prep_pbt thy "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 @@ -429,7 +429,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 - (Specify.prep_pbt thy "pbl_equsys_lin_2x2_tri" [] Spec.e_pblID
1.30 + (Specify.prep_pbt thy "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 @@ -437,14 +437,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 - (Specify.prep_pbt thy "pbl_equsys_lin_2x2_norm" [] Spec.e_pblID
1.39 + (Specify.prep_pbt thy "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 - (Specify.prep_pbt thy "pbl_equsys_lin_3x3" [] Spec.e_pblID
1.47 + (Specify.prep_pbt thy "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 @@ -456,7 +456,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 - (Specify.prep_pbt thy "pbl_equsys_lin_4x4" [] Spec.e_pblID
1.56 + (Specify.prep_pbt thy "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 @@ -468,7 +468,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 - (Specify.prep_pbt thy "pbl_equsys_lin_4x4_tri" [] Spec.e_pblID
1.65 + (Specify.prep_pbt thy "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 @@ -481,7 +481,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 - (Specify.prep_pbt thy "pbl_equsys_lin_4x4_norm" [] Spec.e_pblID
1.74 + (Specify.prep_pbt thy "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 @@ -510,12 +510,12 @@
1.79
1.80 (**methods**)
1.81 setup \<open>KEStore_Elems.add_mets
1.82 - [Specify.prep_met thy "met_eqsys" [] Spec.e_metID
1.83 + [Specify.prep_met thy "met_eqsys" [] Method.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 - Specify.prep_met thy "met_eqsys_topdown" [] Spec.e_metID
1.89 + Specify.prep_met thy "met_eqsys_topdown" [] Method.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 @@ -542,7 +542,7 @@
1.94 in
1.95 Try (Rewrite_Set ''order_system'' ) e__s) "
1.96 setup \<open>KEStore_Elems.add_mets
1.97 - [Specify.prep_met thy "met_eqsys_topdown_2x2" [] Spec.e_metID
1.98 + [Specify.prep_met thy "met_eqsys_topdown_2x2" [] Method.id_empty
1.99 (["EqSystem", "top_down_substitution", "2x2"],
1.100 [("#Given", ["equalities e_s", "solveForVars v_s"]),
1.101 ("#Where",
1.102 @@ -558,7 +558,7 @@
1.103 @{thm solve_system.simps})]
1.104 \<close>
1.105 setup \<open>KEStore_Elems.add_mets
1.106 - [Specify.prep_met thy "met_eqsys_norm" [] Spec.e_metID
1.107 + [Specify.prep_met thy "met_eqsys_norm" [] Method.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 @@ -580,7 +580,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 - [Specify.prep_met thy "met_eqsys_norm_2x2" [] Spec.e_metID
1.116 + [Specify.prep_met thy "met_eqsys_norm_2x2" [] Method.id_empty
1.117 (["EqSystem","normalise","2x2"],
1.118 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
1.119 ("#Find" ,["solution ss'''"])],
1.120 @@ -612,7 +612,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 - [Specify.prep_met thy "met_eqsys_norm_4x4" [] Spec.e_metID
1.125 + [Specify.prep_met thy "met_eqsys_norm_4x4" [] Method.id_empty
1.126 (["EqSystem","normalise","4x4"],
1.127 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
1.128 ("#Find" ,["solution ss'''"])],
1.129 @@ -644,7 +644,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 - [Specify.prep_met thy "met_eqsys_topdown_4x4" [] Spec.e_metID
1.134 + [Specify.prep_met thy "met_eqsys_topdown_4x4" [] Method.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*)