1.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Sat Jun 12 18:33:15 2021 +0200
1.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Tue Jun 15 22:24:20 2021 +0200
1.3 @@ -499,18 +499,13 @@
1.4
1.5 section \<open>Methods\<close>
1.6
1.7 -setup \<open>KEStore_Elems.add_mets
1.8 - [MethodC.prep_input @{theory} "met_eqsys" [] MethodC.id_empty
1.9 - (["EqSystem"], [],
1.10 - {rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [], srls = Rule_Set.Empty, prls = Rule_Set.Empty, crls = Rule_Set.Empty,
1.11 - errpats = [], nrls = Rule_Set.Empty},
1.12 - @{thm refl}),
1.13 - MethodC.prep_input @{theory} "met_eqsys_topdown" [] MethodC.id_empty
1.14 - (["EqSystem", "top_down_substitution"], [],
1.15 - {rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [], srls = Rule_Set.Empty, prls = Rule_Set.Empty, crls = Rule_Set.Empty,
1.16 - errpats = [], nrls = Rule_Set.Empty},
1.17 - @{thm refl})]
1.18 -\<close>
1.19 +method met_eqsys : "EqSystem" =
1.20 + \<open>{rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [], srls = Rule_Set.Empty, prls = Rule_Set.Empty, crls = Rule_Set.Empty,
1.21 + errpats = [], nrls = Rule_Set.Empty}\<close>
1.22 +
1.23 +method met_eqsys_topdown : "EqSystem/top_down_substitution" =
1.24 + \<open>{rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [], srls = Rule_Set.Empty, prls = Rule_Set.Empty, crls = Rule_Set.Empty,
1.25 + errpats = [], nrls = Rule_Set.Empty}\<close>
1.26
1.27 partial_function (tailrec) solve_system :: "bool list => real list => bool list"
1.28 where
1.29 @@ -531,29 +526,24 @@
1.30 e__s = Take [e_1, e_2]
1.31 in
1.32 Try (Rewrite_Set ''order_system'' ) e__s) "
1.33 -setup \<open>KEStore_Elems.add_mets
1.34 - [MethodC.prep_input @{theory} "met_eqsys_topdown_2x2" [] MethodC.id_empty
1.35 - (["EqSystem", "top_down_substitution", "2x2"],
1.36 - [("#Given", ["equalities e_s", "solveForVars v_s"]),
1.37 - ("#Where",
1.38 - ["(tl v_s) from v_s occur_exactly_in (NTH 1 (e_s::bool list))",
1.39 - " v_s from v_s occur_exactly_in (NTH 2 (e_s::bool list))"]),
1.40 - ("#Find" ,["solution ss'''"])],
1.41 - {rew_ord'="ord_simplify_System", rls' = Rule_Set.Empty, calc = [],
1.42 - srls = Rule_Set.append_rules "srls_top_down_2x2" Rule_Set.empty
1.43 - [\<^rule_thm>\<open>hd_thm\<close>,
1.44 - \<^rule_thm>\<open>tl_Cons\<close>,
1.45 - \<^rule_thm>\<open>tl_Nil\<close>],
1.46 - prls = prls_triangular, crls = Rule_Set.Empty, errpats = [], nrls = Rule_Set.Empty},
1.47 - @{thm solve_system.simps})]
1.48 -\<close>
1.49 -setup \<open>KEStore_Elems.add_mets
1.50 - [MethodC.prep_input @{theory} "met_eqsys_norm" [] MethodC.id_empty
1.51 - (["EqSystem", "normalise"], [],
1.52 - {rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [], srls = Rule_Set.Empty, prls = Rule_Set.Empty, crls = Rule_Set.Empty,
1.53 - errpats = [], nrls = Rule_Set.Empty},
1.54 - @{thm refl})]
1.55 -\<close>
1.56 +
1.57 +method met_eqsys_topdown_2x2 : "EqSystem/top_down_substitution/2x2" =
1.58 + \<open>{rew_ord'="ord_simplify_System", rls' = Rule_Set.Empty, calc = [],
1.59 + srls = Rule_Set.append_rules "srls_top_down_2x2" Rule_Set.empty
1.60 + [\<^rule_thm>\<open>hd_thm\<close>,
1.61 + \<^rule_thm>\<open>tl_Cons\<close>,
1.62 + \<^rule_thm>\<open>tl_Nil\<close>],
1.63 + prls = prls_triangular, crls = Rule_Set.Empty, errpats = [], nrls = Rule_Set.Empty}\<close>
1.64 + Program: solve_system.simps
1.65 + Given: "equalities e_s" "solveForVars v_s"
1.66 + Where:
1.67 + "(tl v_s) from v_s occur_exactly_in (NTH 1 (e_s::bool list))"
1.68 + " v_s from v_s occur_exactly_in (NTH 2 (e_s::bool list))"
1.69 + Find: "solution ss'''"
1.70 +
1.71 +method met_eqsys_norm : "EqSystem/normalise" =
1.72 + \<open>{rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [], srls = Rule_Set.Empty, prls = Rule_Set.Empty, crls = Rule_Set.Empty,
1.73 + errpats = [], nrls = Rule_Set.Empty}\<close>
1.74
1.75 partial_function (tailrec) solve_system2 :: "bool list => real list => bool list"
1.76 where
1.77 @@ -569,19 +559,17 @@
1.78 in
1.79 SubProblem (''EqSystem'', [''LINEAR'', ''system''], [''no_met''])
1.80 [BOOL_LIST e__s, REAL_LIST v_s])"
1.81 -setup \<open>KEStore_Elems.add_mets
1.82 - [MethodC.prep_input @{theory} "met_eqsys_norm_2x2" [] MethodC.id_empty
1.83 - (["EqSystem", "normalise", "2x2"],
1.84 - [("#Given" ,["equalities e_s", "solveForVars v_s"]),
1.85 - ("#Find" ,["solution ss'''"])],
1.86 - {rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [],
1.87 - srls = Rule_Set.append_rules "srls_normalise_2x2" Rule_Set.empty
1.88 - [\<^rule_thm>\<open>hd_thm\<close>,
1.89 - \<^rule_thm>\<open>tl_Cons\<close>,
1.90 - \<^rule_thm>\<open>tl_Nil\<close>],
1.91 - prls = Rule_Set.Empty, crls = Rule_Set.Empty, errpats = [], nrls = Rule_Set.Empty},
1.92 - @{thm solve_system2.simps})]
1.93 -\<close>
1.94 +
1.95 +method met_eqsys_norm_2x2 : "EqSystem/normalise/2x2" =
1.96 + \<open>{rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [],
1.97 + srls = Rule_Set.append_rules "srls_normalise_2x2" Rule_Set.empty
1.98 + [\<^rule_thm>\<open>hd_thm\<close>,
1.99 + \<^rule_thm>\<open>tl_Cons\<close>,
1.100 + \<^rule_thm>\<open>tl_Nil\<close>],
1.101 + prls = Rule_Set.Empty, crls = Rule_Set.Empty, errpats = [], nrls = Rule_Set.Empty}\<close>
1.102 + Program: solve_system2.simps
1.103 + Given: "equalities e_s" "solveForVars v_s"
1.104 + Find: "solution ss'''"
1.105
1.106 partial_function (tailrec) solve_system3 :: "bool list => real list => bool list"
1.107 where
1.108 @@ -601,20 +589,17 @@
1.109 in
1.110 SubProblem (''EqSystem'', [''LINEAR'', ''system''], [''no_met''])
1.111 [BOOL_LIST e__s, REAL_LIST v_s])"
1.112 -setup \<open>KEStore_Elems.add_mets
1.113 - [MethodC.prep_input @{theory} "met_eqsys_norm_4x4" [] MethodC.id_empty
1.114 - (["EqSystem", "normalise", "4x4"],
1.115 - [("#Given" ,["equalities e_s", "solveForVars v_s"]),
1.116 - ("#Find" ,["solution ss'''"])],
1.117 - {rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [],
1.118 - srls = Rule_Set.append_rules "srls_normalise_4x4" srls
1.119 - [\<^rule_thm>\<open>hd_thm\<close>,
1.120 - \<^rule_thm>\<open>tl_Cons\<close>,
1.121 - \<^rule_thm>\<open>tl_Nil\<close>],
1.122 - prls = Rule_Set.Empty, crls = Rule_Set.Empty, errpats = [], nrls = Rule_Set.Empty},
1.123 - (*STOPPED.WN06? met ["EqSystem", "normalise", "4x4"] #>#>#>#>#>#>#>#>#>#>#>#>#>@*)
1.124 - @{thm solve_system3.simps})]
1.125 -\<close>
1.126 +
1.127 +method met_eqsys_norm_4x4 : "EqSystem/normalise/4x4" =
1.128 + \<open>{rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [],
1.129 + srls =
1.130 + Rule_Set.append_rules "srls_normalise_4x4" srls
1.131 + [\<^rule_thm>\<open>hd_thm\<close>, \<^rule_thm>\<open>tl_Cons\<close>, \<^rule_thm>\<open>tl_Nil\<close>],
1.132 + prls = Rule_Set.Empty, crls = Rule_Set.Empty, errpats = [], nrls = Rule_Set.Empty}\<close>
1.133 + Program: solve_system3.simps
1.134 + Given: "equalities e_s" "solveForVars v_s"
1.135 + Find: "solution ss'''"
1.136 + (*STOPPED.WN06? met ["EqSystem", "normalise", "4x4"] #>#>#>#>#>#>#>#>#>#>#>#>#>@*)
1.137
1.138 partial_function (tailrec) solve_system4 :: "bool list => real list => bool list"
1.139 where
1.140 @@ -633,24 +618,24 @@
1.141 ) e_2
1.142 in
1.143 [e_1, e_2, NTH 3 e_s, NTH 4 e_s])"
1.144 -setup \<open>KEStore_Elems.add_mets
1.145 - [MethodC.prep_input @{theory} "met_eqsys_topdown_4x4" [] MethodC.id_empty
1.146 - (["EqSystem", "top_down_substitution", "4x4"],
1.147 - [("#Given" ,["equalities e_s", "solveForVars v_s"]),
1.148 - ("#Where" , (*accepts missing variables up to diagonal form*)
1.149 - ["(NTH 1 (v_s::real list)) occurs_in (NTH 1 (e_s::bool list))",
1.150 - "(NTH 2 (v_s::real list)) occurs_in (NTH 2 (e_s::bool list))",
1.151 - "(NTH 3 (v_s::real list)) occurs_in (NTH 3 (e_s::bool list))",
1.152 - "(NTH 4 (v_s::real list)) occurs_in (NTH 4 (e_s::bool list))"]),
1.153 - ("#Find", ["solution ss'''"])],
1.154 - {rew_ord'="ord_simplify_System", rls' = Rule_Set.Empty, calc = [],
1.155 - srls = Rule_Set.append_rules "srls_top_down_4x4" srls [],
1.156 - prls = Rule_Set.append_rules "prls_tri_4x4_lin_sys" prls_triangular
1.157 - [\<^rule_eval>\<open>Prog_Expr.occurs_in\<close> (Prog_Expr.eval_occurs_in "")],
1.158 - crls = Rule_Set.Empty, errpats = [], nrls = Rule_Set.Empty},
1.159 - (*FIXXXXME.WN060916: this script works ONLY for exp 7.79 #>#>#>#>#>#>#>#>#>#>*)
1.160 - @{thm solve_system4.simps})]
1.161 -\<close> ML \<open>
1.162 +
1.163 +method met_eqsys_topdown_4x4 : "EqSystem/top_down_substitution/4x4" =
1.164 + \<open>{rew_ord'="ord_simplify_System", rls' = Rule_Set.Empty, calc = [],
1.165 + srls = Rule_Set.append_rules "srls_top_down_4x4" srls [],
1.166 + prls = Rule_Set.append_rules "prls_tri_4x4_lin_sys" prls_triangular
1.167 + [\<^rule_eval>\<open>Prog_Expr.occurs_in\<close> (Prog_Expr.eval_occurs_in "")],
1.168 + crls = Rule_Set.Empty, errpats = [], nrls = Rule_Set.Empty}\<close>
1.169 + (*FIXXXXME.WN060916: this script works ONLY for exp 7.79 #>#>#>#>#>#>#>#>#>#>*)
1.170 + Program: solve_system4.simps
1.171 + Given: "equalities e_s" "solveForVars v_s"
1.172 + Where: (*accepts missing variables up to diagonal form*)
1.173 + "(NTH 1 (v_s::real list)) occurs_in (NTH 1 (e_s::bool list))"
1.174 + "(NTH 2 (v_s::real list)) occurs_in (NTH 2 (e_s::bool list))"
1.175 + "(NTH 3 (v_s::real list)) occurs_in (NTH 3 (e_s::bool list))"
1.176 + "(NTH 4 (v_s::real list)) occurs_in (NTH 4 (e_s::bool list))"
1.177 + Find: "solution ss'''"
1.178 +
1.179 +ML \<open>
1.180 \<close> ML \<open>
1.181 \<close> ML \<open>
1.182 \<close>