1.1 --- a/src/Tools/isac/Knowledge/Poly.thy Wed Aug 03 18:17:27 2022 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Thu Aug 04 12:48:37 2022 +0200
1.3 @@ -723,7 +723,7 @@
1.4 \<close>
1.5 ML \<open>
1.6 val expand =
1.7 - Rule_Def.Repeat {id = "expand", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1.8 + Rule_Def.Repeat {id = "expand", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
1.9 erls = Rule_Set.empty,srls = Rule_Set.Empty, calc = [], errpatts = [],
1.10 rules = [
1.11 \<^rule_thm>\<open>distrib_right\<close>, (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
1.12 @@ -735,7 +735,7 @@
1.13 ML \<open>
1.14 (* erls for calculate_Rational + etc *)
1.15 val powers_erls =
1.16 - Rule_Def.Repeat {id = "powers_erls", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
1.17 + Rule_Def.Repeat {id = "powers_erls", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.function_empty),
1.18 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.19 rules = [
1.20 \<^rule_eval>\<open>matches\<close> (Prog_Expr.eval_matches "#matches_"),
1.21 @@ -750,7 +750,7 @@
1.22
1.23 \<close> ML \<open>
1.24 val discard_minus =
1.25 - Rule_Def.Repeat {id = "discard_minus", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1.26 + Rule_Def.Repeat {id = "discard_minus", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
1.27 erls = powers_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.28 rules = [
1.29 \<^rule_thm>\<open>real_diff_minus\<close> (*"a - b = a + -1 * b"*),
1.30 @@ -759,7 +759,7 @@
1.31
1.32 val expand_poly_ =
1.33 Rule_Def.Repeat{id = "expand_poly_", preconds = [],
1.34 - rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1.35 + rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
1.36 erls = powers_erls, srls = Rule_Set.Empty,
1.37 calc = [], errpatts = [],
1.38 rules = [
1.39 @@ -785,7 +785,7 @@
1.40
1.41 val expand_poly_rat_ =
1.42 Rule_Def.Repeat{id = "expand_poly_rat_", preconds = [],
1.43 - rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1.44 + rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
1.45 erls = Rule_Set.append_rules "Rule_Set.empty-expand_poly_rat_" Rule_Set.empty [
1.46 \<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp ""),
1.47 \<^rule_eval>\<open>is_even\<close> (Prog_Expr.eval_is_even "#is_even_"),
1.48 @@ -813,7 +813,7 @@
1.49
1.50 val simplify_power_ =
1.51 Rule_Def.Repeat{id = "simplify_power_", preconds = [],
1.52 - rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1.53 + rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
1.54 erls = Rule_Set.empty, srls = Rule_Set.Empty,
1.55 calc = [], errpatts = [],
1.56 rules = [
1.57 @@ -836,7 +836,7 @@
1.58
1.59 val calc_add_mult_pow_ =
1.60 Rule_Def.Repeat{id = "calc_add_mult_pow_", preconds = [],
1.61 - rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1.62 + rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
1.63 erls = Atools_erls(*erls3.4.03*),srls = Rule_Set.Empty,
1.64 calc = [("PLUS" , (\<^const_name>\<open>plus\<close>, eval_binop "#add_")),
1.65 ("TIMES" , (\<^const_name>\<open>times\<close>, eval_binop "#mult_")),
1.66 @@ -851,7 +851,7 @@
1.67
1.68 val reduce_012_mult_ =
1.69 Rule_Def.Repeat{id = "reduce_012_mult_", preconds = [],
1.70 - rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1.71 + rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
1.72 erls = Rule_Set.empty,srls = Rule_Set.Empty,
1.73 calc = [], errpatts = [],
1.74 rules = [(* MG: folgende Rule.Thm müssen hier stehen bleiben: *)
1.75 @@ -863,7 +863,7 @@
1.76
1.77 val collect_numerals_ =
1.78 Rule_Def.Repeat{id = "collect_numerals_", preconds = [],
1.79 - rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1.80 + rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
1.81 erls = Atools_erls, srls = Rule_Set.Empty,
1.82 calc = [("PLUS" , (\<^const_name>\<open>plus\<close>, eval_binop "#add_"))
1.83 ], errpatts = [],
1.84 @@ -884,7 +884,7 @@
1.85
1.86 val reduce_012_ =
1.87 Rule_Def.Repeat{id = "reduce_012_", preconds = [],
1.88 - rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1.89 + rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
1.90 erls = Rule_Set.empty,srls = Rule_Set.Empty, calc = [], errpatts = [],
1.91 rules = [
1.92 \<^rule_thm>\<open>mult_1_left\<close>, (*"1 * z = z"*)
1.93 @@ -904,7 +904,7 @@
1.94
1.95 val expand_poly =
1.96 Rule_Def.Repeat{id = "expand_poly", preconds = [],
1.97 - rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1.98 + rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
1.99 erls = powers_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.100 rules = [
1.101 \<^rule_thm>\<open>distrib_right\<close>, (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
1.102 @@ -925,7 +925,7 @@
1.103
1.104 val simplify_power =
1.105 Rule_Def.Repeat{id = "simplify_power", preconds = [],
1.106 - rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1.107 + rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
1.108 erls = Rule_Set.empty, srls = Rule_Set.Empty,
1.109 calc = [], errpatts = [],
1.110 rules = [
1.111 @@ -941,7 +941,7 @@
1.112
1.113 val collect_numerals =
1.114 Rule_Def.Repeat{id = "collect_numerals", preconds = [],
1.115 - rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1.116 + rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
1.117 erls = Atools_erls(*erls3.4.03*),srls = Rule_Set.Empty,
1.118 calc = [("PLUS" , (\<^const_name>\<open>plus\<close>, eval_binop "#add_")),
1.119 ("TIMES" , (\<^const_name>\<open>times\<close>, eval_binop "#mult_")),
1.120 @@ -959,7 +959,7 @@
1.121 scr = Rule.Empty_Prog};
1.122 val reduce_012 =
1.123 Rule_Def.Repeat{id = "reduce_012", preconds = [],
1.124 - rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1.125 + rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
1.126 erls = Rule_Set.append_rules "erls_in_reduce_012" Rule_Set.empty [
1.127 \<^rule_eval>\<open>is_num\<close> (Prog_Expr.eval_is_num "#is_num_"),
1.128 \<^rule_thm>\<open>not_false\<close>,
1.129 @@ -989,7 +989,7 @@
1.130 (total-degree-)ordering of monoms NOT possible with size_of_term GIVEN*)
1.131 val order_add_mult =
1.132 Rule_Def.Repeat{id = "order_add_mult", preconds = [],
1.133 - rew_ord = ("ord_make_polynomial",ord_make_polynomial false \<^theory>),
1.134 + rew_ord = ("ord_make_polynomial", ord_make_polynomial false \<^theory>),
1.135 erls = Rule_Set.empty,srls = Rule_Set.Empty,
1.136 calc = [], errpatts = [],
1.137 rules = [
1.138 @@ -1029,7 +1029,7 @@
1.139 which evaluates (the instantiated) "?p is_multUnordered" to true *)
1.140 [([TermC.parse_patt \<^theory> "?p is_multUnordered"],
1.141 TermC.parse_patt \<^theory> "?p :: real")],
1.142 - rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1.143 + rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
1.144 erls = Rule_Set.append_rules "Rule_Set.empty-is_multUnordered" Rule_Set.empty
1.145 [\<^rule_eval>\<open>is_multUnordered\<close> (eval_is_multUnordered "")],
1.146 calc = [("PLUS" , (\<^const_name>\<open>plus\<close>, eval_binop "#add_")),
1.147 @@ -1044,7 +1044,7 @@
1.148 attach_form = attach_form}};
1.149 val order_mult_rls_ =
1.150 Rule_Def.Repeat {id = "order_mult_rls_", preconds = [],
1.151 - rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1.152 + rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
1.153 erls = Rule_Set.empty,srls = Rule_Set.Empty,
1.154 calc = [], errpatts = [],
1.155 rules = [
1.156 @@ -1069,7 +1069,7 @@
1.157 TermC.parse_patt @{theory} "?p :: real"
1.158 (*WN.18.6.03 also KEIN pattern, dieses erzeugt nur das Environment
1.159 fuer die Evaluation der Precondition "p is_addUnordered"*))],
1.160 - rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1.161 + rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
1.162 erls = Rule_Set.append_rules "Rule_Set.empty-is_addUnordered" Rule_Set.empty(*MG: poly_erls*)
1.163 [\<^rule_eval>\<open>is_addUnordered\<close> (eval_is_addUnordered "")],
1.164 calc = [
1.165 @@ -1087,7 +1087,7 @@
1.166
1.167 val order_add_rls_ =
1.168 Rule_Def.Repeat {id = "order_add_rls_", preconds = [],
1.169 - rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1.170 + rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
1.171 erls = Rule_Set.empty, srls = Rule_Set.Empty,
1.172 calc = [], errpatts = [],
1.173 rules = [
1.174 @@ -1108,7 +1108,7 @@
1.175 val make_polynomial(*MG.03, overwrites version from above,
1.176 previously 'make_polynomial_'*) =
1.177 Rule_Set.Sequence {id = "make_polynomial", preconds = []:term list,
1.178 - rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1.179 + rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
1.180 erls = Atools_erls, srls = Rule_Set.Empty,calc = [], errpatts = [],
1.181 rules = [
1.182 Rule.Rls_ discard_minus,
1.183 @@ -1127,7 +1127,7 @@
1.184 ML \<open>
1.185 val norm_Poly(*=make_polynomial*) =
1.186 Rule_Set.Sequence {id = "norm_Poly", preconds = []:term list,
1.187 - rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1.188 + rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
1.189 erls = Atools_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.190 rules = [
1.191 Rule.Rls_ discard_minus,
1.192 @@ -1149,7 +1149,7 @@
1.193 (* MG necessary for termination of norm_Rational(*_mg*) in Rational.ML*)
1.194 val make_rat_poly_with_parentheses =
1.195 Rule_Set.Sequence{id = "make_rat_poly_with_parentheses", preconds = []:term list,
1.196 - rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1.197 + rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
1.198 erls = Atools_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.199 rules = [
1.200 Rule.Rls_ discard_minus,
1.201 @@ -1375,5 +1375,5 @@
1.202 Find: "normalform n_n"
1.203 ML \<open>
1.204 \<close> ML \<open>
1.205 -\<close>
1.206 +\<close>
1.207 end