1.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Sun Jun 20 12:45:03 2021 +0200
1.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Sun Jun 20 16:26:18 2021 +0200
1.3 @@ -394,90 +394,89 @@
1.4
1.5 section \<open>Problems\<close>
1.6
1.7 -setup \<open>KEStore_Elems.add_pbts
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 @{theory} "pbl_equsys_lin" [] Problem.id_empty
1.14 - (["LINEAR", "system"],
1.15 - [("#Given" ,["equalities e_s", "solveForVars v_s"]),
1.16 - (*TODO.WN050929 check linearity*)
1.17 - ("#Find" ,["solution ss'''"])],
1.18 - Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)], SOME "solveSystem e_s v_s", [])),
1.19 - (Problem.prep_input @{theory} "pbl_equsys_lin_2x2" [] Problem.id_empty
1.20 - (["2x2", "LINEAR", "system"],
1.21 - (*~~~~~~~~~~~~~~~~~~~~~~~~~*)
1.22 - [("#Given" ,["equalities e_s", "solveForVars v_s"]),
1.23 - ("#Where" ,["Length (e_s:: bool list) = 2", "Length v_s = 2"]),
1.24 - ("#Find" ,["solution ss'''"])],
1.25 - Rule_Set.append_rules "prls_2x2_linear_system" Rule_Set.empty
1.26 - [\<^rule_thm>\<open>LENGTH_CONS\<close>,
1.27 - \<^rule_thm>\<open>LENGTH_NIL\<close>,
1.28 - \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
1.29 - \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_")],
1.30 - SOME "solveSystem e_s v_s", [])),
1.31 - (Problem.prep_input @{theory} "pbl_equsys_lin_2x2_tri" [] Problem.id_empty
1.32 - (["triangular", "2x2", "LINEAR", "system"],
1.33 - [("#Given" ,["equalities e_s", "solveForVars v_s"]),
1.34 - ("#Where",
1.35 - ["(tl v_s) from v_s occur_exactly_in (NTH 1 (e_s::bool list))",
1.36 - " v_s from v_s occur_exactly_in (NTH 2 (e_s::bool list))"]),
1.37 - ("#Find" ,["solution ss'''"])],
1.38 - prls_triangular, SOME "solveSystem e_s v_s", [["EqSystem", "top_down_substitution", "2x2"]])),
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 @{theory} "pbl_equsys_lin_3x3" [] Problem.id_empty
1.47 - (["3x3", "LINEAR", "system"],
1.48 - (*~~~~~~~~~~~~~~~~~~~~~~~~~*)
1.49 - [("#Given" ,["equalities e_s", "solveForVars v_s"]),
1.50 - ("#Where" ,["Length (e_s:: bool list) = 3", "Length v_s = 3"]),
1.51 - ("#Find" ,["solution ss'''"])],
1.52 - Rule_Set.append_rules "prls_3x3_linear_system" Rule_Set.empty
1.53 - [\<^rule_thm>\<open>LENGTH_CONS\<close>,
1.54 - \<^rule_thm>\<open>LENGTH_NIL\<close>,
1.55 - \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
1.56 - \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_")],
1.57 - SOME "solveSystem e_s v_s", [])),
1.58 - (Problem.prep_input @{theory} "pbl_equsys_lin_4x4" [] Problem.id_empty
1.59 - (["4x4", "LINEAR", "system"],
1.60 - (*~~~~~~~~~~~~~~~~~~~~~~~~~*)
1.61 - [("#Given" ,["equalities e_s", "solveForVars v_s"]),
1.62 - ("#Where" ,["Length (e_s:: bool list) = 4", "Length v_s = 4"]),
1.63 - ("#Find" ,["solution ss'''"])],
1.64 - Rule_Set.append_rules "prls_4x4_linear_system" Rule_Set.empty
1.65 - [\<^rule_thm>\<open>LENGTH_CONS\<close>,
1.66 - \<^rule_thm>\<open>LENGTH_NIL\<close>,
1.67 - \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
1.68 - \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_")],
1.69 - SOME "solveSystem e_s v_s", [])),
1.70 - (Problem.prep_input @{theory} "pbl_equsys_lin_4x4_tri" [] Problem.id_empty
1.71 - (["triangular", "4x4", "LINEAR", "system"],
1.72 - [("#Given" ,["equalities e_s", "solveForVars v_s"]),
1.73 - ("#Where" , (*accepts missing variables up to diagional form*)
1.74 - ["(NTH 1 (v_s::real list)) occurs_in (NTH 1 (e_s::bool list))",
1.75 - "(NTH 2 (v_s::real list)) occurs_in (NTH 2 (e_s::bool list))",
1.76 - "(NTH 3 (v_s::real list)) occurs_in (NTH 3 (e_s::bool list))",
1.77 - "(NTH 4 (v_s::real list)) occurs_in (NTH 4 (e_s::bool list))"]),
1.78 - ("#Find" ,["solution ss'''"])],
1.79 - Rule_Set.append_rules "prls_tri_4x4_lin_sys" prls_triangular
1.80 - [\<^rule_eval>\<open>Prog_Expr.occurs_in\<close> (Prog_Expr.eval_occurs_in "")],
1.81 - SOME "solveSystem e_s v_s",
1.82 - [["EqSystem", "top_down_substitution", "4x4"]])),
1.83 - (Problem.prep_input @{theory} "pbl_equsys_lin_4x4_norm" [] Problem.id_empty
1.84 - (["normalise", "4x4", "LINEAR", "system"],
1.85 - [("#Given" ,["equalities e_s", "solveForVars v_s"]),
1.86 - (*Length is checked 1 level above*)
1.87 - ("#Find" ,["solution ss'''"])],
1.88 - Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)],
1.89 - SOME "solveSystem e_s v_s",
1.90 - [["EqSystem", "normalise", "4x4"]]))]\<close>
1.91 +problem pbl_equsys : "system" =
1.92 + \<open>Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)]\<close>
1.93 + CAS: "solveSystem e_s v_s"
1.94 + Given: "equalities e_s" "solveForVars v_s"
1.95 + Find: "solution ss'''" (*''' is copy-named*)
1.96 +
1.97 +problem pbl_equsys_lin : "LINEAR/system" =
1.98 + \<open>Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)]\<close>
1.99 + CAS: "solveSystem e_s v_s"
1.100 + Given: "equalities e_s" "solveForVars v_s"
1.101 + (*TODO.WN050929 check linearity*)
1.102 + Find: "solution ss'''"
1.103 +
1.104 +problem pbl_equsys_lin_2x2: "2x2/LINEAR/system" =
1.105 + \<open>Rule_Set.append_rules "prls_2x2_linear_system" Rule_Set.empty
1.106 + [\<^rule_thm>\<open>LENGTH_CONS\<close>,
1.107 + \<^rule_thm>\<open>LENGTH_NIL\<close>,
1.108 + \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
1.109 + \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_")]\<close>
1.110 + CAS: "solveSystem e_s v_s"
1.111 + Given: "equalities e_s" "solveForVars v_s"
1.112 + Where: "Length (e_s:: bool list) = 2" "Length v_s = 2"
1.113 + Find: "solution ss'''"
1.114 +
1.115 +problem pbl_equsys_lin_2x2_tri : "triangular/2x2/LINEAR/system" =
1.116 + \<open>prls_triangular\<close>
1.117 + Method: "EqSystem/top_down_substitution/2x2"
1.118 + CAS: "solveSystem e_s v_s"
1.119 + Given: "equalities e_s" "solveForVars v_s"
1.120 + Where:
1.121 + "(tl v_s) from v_s occur_exactly_in (NTH 1 (e_s::bool list))"
1.122 + " v_s from v_s occur_exactly_in (NTH 2 (e_s::bool list))"
1.123 + Find: "solution ss'''"
1.124 +
1.125 +problem pbl_equsys_lin_2x2_norm : "normalise/2x2/LINEAR/system" =
1.126 + \<open>Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)]\<close>
1.127 + Method: "EqSystem/normalise/2x2"
1.128 + CAS: "solveSystem e_s v_s"
1.129 + Given: "equalities e_s" "solveForVars v_s"
1.130 + Find: "solution ss'''"
1.131 +
1.132 +problem pbl_equsys_lin_3x3 : "3x3/LINEAR/system" =
1.133 + \<open>Rule_Set.append_rules "prls_3x3_linear_system" Rule_Set.empty
1.134 + [\<^rule_thm>\<open>LENGTH_CONS\<close>,
1.135 + \<^rule_thm>\<open>LENGTH_NIL\<close>,
1.136 + \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
1.137 + \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_")]\<close>
1.138 + CAS: "solveSystem e_s v_s"
1.139 + Given: "equalities e_s" "solveForVars v_s"
1.140 + Where: "Length (e_s:: bool list) = 3" "Length v_s = 3"
1.141 + Find: "solution ss'''"
1.142 +
1.143 +problem pbl_equsys_lin_4x4 : "4x4/LINEAR/system" =
1.144 + \<open>Rule_Set.append_rules "prls_4x4_linear_system" Rule_Set.empty
1.145 + [\<^rule_thm>\<open>LENGTH_CONS\<close>,
1.146 + \<^rule_thm>\<open>LENGTH_NIL\<close>,
1.147 + \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
1.148 + \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_")]\<close>
1.149 + CAS: "solveSystem e_s v_s"
1.150 + Given: "equalities e_s" "solveForVars v_s"
1.151 + Where: "Length (e_s:: bool list) = 4" "Length v_s = 4"
1.152 + Find: "solution ss'''"
1.153 +
1.154 +problem pbl_equsys_lin_4x4_tri : "triangular/4x4/LINEAR/system" =
1.155 + \<open>Rule_Set.append_rules "prls_tri_4x4_lin_sys" prls_triangular
1.156 + [\<^rule_eval>\<open>Prog_Expr.occurs_in\<close> (Prog_Expr.eval_occurs_in "")]\<close>
1.157 + Method: "EqSystem/top_down_substitution/4x4"
1.158 + CAS: "solveSystem e_s v_s"
1.159 + Given: "equalities e_s" "solveForVars v_s"
1.160 + Where: (*accepts missing variables up to diagional form*)
1.161 + "(NTH 1 (v_s::real list)) occurs_in (NTH 1 (e_s::bool list))"
1.162 + "(NTH 2 (v_s::real list)) occurs_in (NTH 2 (e_s::bool list))"
1.163 + "(NTH 3 (v_s::real list)) occurs_in (NTH 3 (e_s::bool list))"
1.164 + "(NTH 4 (v_s::real list)) occurs_in (NTH 4 (e_s::bool list))"
1.165 + Find: "solution ss'''"
1.166 +
1.167 +problem pbl_equsys_lin_4x4_norm : "normalise/4x4/LINEAR/system" =
1.168 + \<open>Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)]\<close>
1.169 + Method: "EqSystem/normalise/4x4"
1.170 + CAS: "solveSystem e_s v_s"
1.171 + Given: "equalities e_s" "solveForVars v_s"
1.172 + (*Length is checked 1 level above*)
1.173 + Find: "solution ss'''"
1.174
1.175 ML \<open>
1.176 (*this is for NTH only*)