1.1 --- a/src/Tools/isac/Knowledge/PolyMinus.thy Sat Jun 12 18:33:15 2021 +0200
1.2 +++ b/src/Tools/isac/Knowledge/PolyMinus.thy Tue Jun 15 22:24:20 2021 +0200
1.3 @@ -474,31 +474,31 @@
1.4 (Try (Rewrite_Set ''fasse_zusammen'')) #>
1.5 (Try (Rewrite_Set ''verschoenere'')))
1.6 ) t_t)"
1.7 -setup \<open>KEStore_Elems.add_mets
1.8 - [MethodC.prep_input @{theory} "met_simp_poly_minus" [] MethodC.id_empty
1.9 - (["simplification", "for_polynomials", "with_minus"],
1.10 - [("#Given" ,["Term t_t"]),
1.11 - ("#Where" ,["t_t is_polyexp",
1.12 - "Not (matchsub (?a + (?b + ?c)) t_t | " ^
1.13 - " matchsub (?a + (?b - ?c)) t_t | " ^
1.14 - " matchsub (?a - (?b + ?c)) t_t | " ^
1.15 - " matchsub (?a + (?b - ?c)) t_t )"]),
1.16 - ("#Find" ,["normalform n_n"])],
1.17 - {rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty,
1.18 - prls = Rule_Set.append_rules "prls_met_simp_poly_minus" Rule_Set.empty
1.19 - [\<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp ""),
1.20 - \<^rule_eval>\<open>Prog_Expr.matchsub\<close> (Prog_Expr.eval_matchsub ""),
1.21 - \<^rule_thm>\<open>and_true\<close>,
1.22 - (*"(?a & True) = ?a"*)
1.23 - \<^rule_thm>\<open>and_false\<close>,
1.24 - (*"(?a & False) = False"*)
1.25 - \<^rule_thm>\<open>not_true\<close>,
1.26 - (*"(~ True) = False"*)
1.27 - \<^rule_thm>\<open>not_false\<close>
1.28 - (*"(~ False) = True"*)],
1.29 - crls = Rule_Set.empty, errpats = [], nrls = rls_p_33},
1.30 - @{thm simplify.simps})]
1.31 -\<close>
1.32 +
1.33 +method met_simp_poly_minus : "simplification/for_polynomials/with_minus" =
1.34 + \<open>{rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty,
1.35 + prls =
1.36 + Rule_Set.append_rules "prls_met_simp_poly_minus" Rule_Set.empty
1.37 + [\<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp ""),
1.38 + \<^rule_eval>\<open>Prog_Expr.matchsub\<close> (Prog_Expr.eval_matchsub ""),
1.39 + \<^rule_thm>\<open>and_true\<close>,
1.40 + (*"(?a & True) = ?a"*)
1.41 + \<^rule_thm>\<open>and_false\<close>,
1.42 + (*"(?a & False) = False"*)
1.43 + \<^rule_thm>\<open>not_true\<close>,
1.44 + (*"(~ True) = False"*)
1.45 + \<^rule_thm>\<open>not_false\<close>
1.46 + (*"(~ False) = True"*)],
1.47 + crls = Rule_Set.empty, errpats = [], nrls = rls_p_33}\<close>
1.48 + Program: simplify.simps
1.49 + Given: "Term t_t"
1.50 + Where:
1.51 + "t_t is_polyexp"
1.52 + "Not (matchsub (?a + (?b + ?c)) t_t |
1.53 + matchsub (?a + (?b - ?c)) t_t |
1.54 + matchsub (?a - (?b + ?c)) t_t |
1.55 + matchsub (?a + (?b - ?c)) t_t)"
1.56 + Find: "normalform n_n"
1.57
1.58 partial_function (tailrec) simplify2 :: "real \<Rightarrow> real"
1.59 where
1.60 @@ -509,18 +509,16 @@
1.61 (Try (Rewrite_Set ''fasse_zusammen'')) #>
1.62 (Try (Rewrite_Set ''verschoenere'')))
1.63 ) t_t)"
1.64 -setup \<open>KEStore_Elems.add_mets
1.65 - [MethodC.prep_input @{theory} "met_simp_poly_parenth" [] MethodC.id_empty
1.66 - (["simplification", "for_polynomials", "with_parentheses"],
1.67 - [("#Given" ,["Term t_t"]),
1.68 - ("#Where" ,["t_t is_polyexp"]),
1.69 - ("#Find" ,["normalform n_n"])],
1.70 - {rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty,
1.71 - prls = Rule_Set.append_rules "simplification_for_polynomials_prls" Rule_Set.empty
1.72 - [(*for preds in where_*) \<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp"")],
1.73 - crls = Rule_Set.empty, errpats = [], nrls = rls_p_34},
1.74 - @{thm simplify2.simps})]
1.75 -\<close>
1.76 +
1.77 +method met_simp_poly_parenth : "simplification/for_polynomials/with_parentheses" =
1.78 + \<open>{rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty,
1.79 + prls = Rule_Set.append_rules "simplification_for_polynomials_prls" Rule_Set.empty
1.80 + [(*for preds in where_*) \<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp"")],
1.81 + crls = Rule_Set.empty, errpats = [], nrls = rls_p_34}\<close>
1.82 + Program: simplify2.simps
1.83 + Given: "Term t_t"
1.84 + Where: "t_t is_polyexp"
1.85 + Find: "normalform n_n"
1.86
1.87 partial_function (tailrec) simplify3 :: "real \<Rightarrow> real"
1.88 where
1.89 @@ -534,23 +532,20 @@
1.90 (Try (Rewrite_Set ''fasse_zusammen'')) #>
1.91 (Try (Rewrite_Set ''verschoenere'')))
1.92 ) t_t)"
1.93 -setup \<open>KEStore_Elems.add_mets
1.94 - [MethodC.prep_input @{theory} "met_simp_poly_parenth_mult" [] MethodC.id_empty
1.95 - (["simplification", "for_polynomials", "with_parentheses_mult"],
1.96 - [("#Given" ,["Term t_t"]), ("#Where" ,["t_t is_polyexp"]), ("#Find" ,["normalform n_n"])],
1.97 - {rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty,
1.98 - prls = Rule_Set.append_rules "simplification_for_polynomials_prls" Rule_Set.empty
1.99 - [(*for preds in where_*) \<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp"")],
1.100 - crls = Rule_Set.empty, errpats = [], nrls = rls_p_34},
1.101 - @{thm simplify3.simps})]
1.102 -\<close>
1.103 -setup \<open>KEStore_Elems.add_mets
1.104 - [MethodC.prep_input @{theory} "met_probe" [] MethodC.id_empty
1.105 - (["probe"], [],
1.106 - {rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.Empty, crls = Rule_Set.empty,
1.107 - errpats = [], nrls = Rule_Set.Empty},
1.108 - @{thm refl})]
1.109 -\<close>
1.110 +
1.111 +method met_simp_poly_parenth_mult : "simplification/for_polynomials/with_parentheses_mult" =
1.112 + \<open>{rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty,
1.113 + prls = Rule_Set.append_rules "simplification_for_polynomials_prls" Rule_Set.empty
1.114 + [(*for preds in where_*) \<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp"")],
1.115 + crls = Rule_Set.empty, errpats = [], nrls = rls_p_34}\<close>
1.116 + Program: simplify3.simps
1.117 + Given: "Term t_t"
1.118 + Where: "t_t is_polyexp"
1.119 + Find: "normalform n_n"
1.120 +
1.121 +method met_probe : "probe" =
1.122 + \<open>{rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.Empty, crls = Rule_Set.empty,
1.123 + errpats = [], nrls = Rule_Set.Empty}\<close>
1.124
1.125 partial_function (tailrec) mache_probe :: "bool \<Rightarrow> bool list \<Rightarrow> bool"
1.126 where
1.127 @@ -564,30 +559,27 @@
1.128 (Try (Repeat (Calculate ''PLUS'' ))) #>
1.129 (Try (Repeat (Calculate ''MINUS''))))
1.130 ) e_e)"
1.131 -setup \<open>KEStore_Elems.add_mets
1.132 - [MethodC.prep_input @{theory} "met_probe_poly" [] MethodC.id_empty
1.133 - (["probe", "fuer_polynom"],
1.134 - [("#Given" ,["Pruefe e_e", "mitWert w_w"]),
1.135 - ("#Where" ,["e_e is_polyexp"]),
1.136 - ("#Find" ,["Geprueft p_p"])],
1.137 - {rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty,
1.138 - prls = Rule_Set.append_rules "prls_met_probe_bruch" Rule_Set.empty
1.139 - [(*for preds in where_*) \<^rule_eval>\<open>is_ratpolyexp\<close> (eval_is_ratpolyexp "")],
1.140 - crls = Rule_Set.empty, errpats = [], nrls = rechnen},
1.141 - @{thm mache_probe.simps})]
1.142 -\<close>
1.143 -setup \<open>KEStore_Elems.add_mets
1.144 - [MethodC.prep_input @{theory} "met_probe_bruch" [] MethodC.id_empty
1.145 - (["probe", "fuer_bruch"],
1.146 - [("#Given" ,["Pruefe e_e", "mitWert w_w"]),
1.147 - ("#Where" ,["e_e is_ratpolyexp"]),
1.148 - ("#Find" ,["Geprueft p_p"])],
1.149 - {rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty,
1.150 - prls = Rule_Set.append_rules "prls_met_probe_bruch" Rule_Set.empty
1.151 - [(*for preds in where_*) \<^rule_eval>\<open>is_ratpolyexp\<close> (eval_is_ratpolyexp "")],
1.152 - crls = Rule_Set.empty, errpats = [], nrls = Rule_Set.Empty},
1.153 - @{thm refl})]
1.154 -\<close> ML \<open>
1.155 +
1.156 +method met_probe_poly : "probe/fuer_polynom" =
1.157 + \<open>{rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty,
1.158 + prls = Rule_Set.append_rules "prls_met_probe_bruch" Rule_Set.empty
1.159 + [(*for preds in where_*) \<^rule_eval>\<open>is_ratpolyexp\<close> (eval_is_ratpolyexp "")],
1.160 + crls = Rule_Set.empty, errpats = [], nrls = rechnen}\<close>
1.161 + Program: mache_probe.simps
1.162 + Given: "Pruefe e_e" "mitWert w_w"
1.163 + Where: "e_e is_polyexp"
1.164 + Find: "Geprueft p_p"
1.165 +
1.166 +method met_probe_bruch : "probe/fuer_bruch" =
1.167 + \<open>{rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty,
1.168 + prls = Rule_Set.append_rules "prls_met_probe_bruch" Rule_Set.empty
1.169 + [(*for preds in where_*) \<^rule_eval>\<open>is_ratpolyexp\<close> (eval_is_ratpolyexp "")],
1.170 + crls = Rule_Set.empty, errpats = [], nrls = Rule_Set.Empty}\<close>
1.171 + Given: "Pruefe e_e" "mitWert w_w"
1.172 + Where: "e_e is_ratpolyexp"
1.173 + Find: "Geprueft p_p"
1.174 +
1.175 +ML \<open>
1.176 \<close> ML \<open>
1.177 \<close>
1.178