1.1 --- a/src/Tools/isac/Knowledge/Rational.thy Mon Aug 09 14:20:20 2021 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Tue Aug 10 09:43:07 2021 +0200
1.3 @@ -11,7 +11,7 @@
1.4 imports Poly GCD_Poly_ML
1.5 begin
1.6
1.7 -section \<open>Constants for evaluation by "Rule.Eval"\<close>
1.8 +section \<open>Constants for evaluation by \ <^rule_eval>\<close>
1.9 consts
1.10
1.11 is_expanded :: "real => bool" ("_ is'_expanded") (*RL->Poly.thy*)
1.12 @@ -411,12 +411,12 @@
1.13 prep_rls'
1.14 (Rule_Def.Repeat {id = "calc_rat_erls", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1.15 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.16 - rules =
1.17 - [Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches "#matches_"),
1.18 - Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_"),
1.19 - Rule.Eval ("Prog_Expr.is_const", Prog_Expr.eval_const "#is_const_"),
1.20 - Rule.Thm ("not_true", @{thm not_true}),
1.21 - Rule.Thm ("not_false", @{thm not_false})],
1.22 + rules = [
1.23 + \<^rule_eval>\<open>matches\<close> (Prog_Expr.eval_matches "#matches_"),
1.24 + \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"),
1.25 + \<^rule_eval>\<open>is_const\<close> (Prog_Expr.eval_const "#is_const_"),
1.26 + \<^rule_thm>\<open>not_true\<close>,
1.27 + \<^rule_thm>\<open>not_false\<close>],
1.28 scr = Rule.Empty_Prog});
1.29
1.30 (* simplifies expressions with numerals;
1.31 @@ -427,43 +427,28 @@
1.32 (Rule_Def.Repeat {id = "divide", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1.33 erls = calc_rat_erls, srls = Rule_Set.Empty,
1.34 calc = [], errpatts = [],
1.35 - rules =
1.36 - [\<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
1.37 + rules = [
1.38 + \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
1.39
1.40 - Rule.Thm ("minus_divide_left", (@{thm minus_divide_left} RS @{thm sym})),
1.41 - (*SYM - ?x / ?y = - (?x / ?y) may come from subst*)
1.42 + \<^rule_thm_sym>\<open>minus_divide_left\<close>, (*SYM - ?x / ?y = - (?x / ?y) may come from subst*)
1.43 \<^rule_thm>\<open>rat_add\<close>,
1.44 - (*"[| a is_const; b is_const; c is_const; d is_const |] ==> \
1.45 - \a / c + b / d = (a * d) / (c * d) + (b * c ) / (d * c)"*)
1.46 - \<^rule_thm>\<open>rat_add1\<close>,
1.47 - (*"[| a is_const; b is_const; c is_const |] ==> a / c + b / c = (a + b) / c"*)
1.48 - \<^rule_thm>\<open>rat_add2\<close>,
1.49 - (*"[| ?a is_const; ?b is_const; ?c is_const |] ==> ?a / ?c + ?b = (?a + ?b * ?c) / ?c"*)
1.50 - \<^rule_thm>\<open>rat_add3\<close>,
1.51 - (*"[| a is_const; b is_const; c is_const |] ==> a + b / c = (a * c) / c + b / c"\
1.52 - .... is_const to be omitted here FIXME*)
1.53 + (*"[| a is_const; b is_const; c is_const; d is_const |] ==> a / c + b / d = (a * d) / (c * d) + (b * c ) / (d * c)"*)
1.54 + \<^rule_thm>\<open>rat_add1\<close>, (*"[| a is_const; b is_const; c is_const |] ==> a / c + b / c = (a + b) / c"*)
1.55 + \<^rule_thm>\<open>rat_add2\<close>, (*"[| ?a is_const; ?b is_const; ?c is_const |] ==> ?a / ?c + ?b = (?a + ?b * ?c) / ?c"*)
1.56 + \<^rule_thm>\<open>rat_add3\<close>, (*"[| a is_const; b is_const; c is_const |] ==> a + b / c = (a * c) / c + b / c" *)
1.57
1.58 - \<^rule_thm>\<open>rat_mult\<close>,
1.59 - (*a / b * (c / d) = a * c / (b * d)*)
1.60 - \<^rule_thm>\<open>times_divide_eq_right\<close>,
1.61 - (*?x * (?y / ?z) = ?x * ?y / ?z*)
1.62 - \<^rule_thm>\<open>times_divide_eq_left\<close>,
1.63 - (*?y / ?z * ?x = ?y * ?x / ?z*)
1.64 + \<^rule_thm>\<open>rat_mult\<close>, (*a / b * (c / d) = a * c / (b * d)*)
1.65 + \<^rule_thm>\<open>times_divide_eq_right\<close>, (*?x * (?y / ?z) = ?x * ?y / ?z*)
1.66 + \<^rule_thm>\<open>times_divide_eq_left\<close>, (*?y / ?z * ?x = ?y * ?x / ?z*)
1.67
1.68 - \<^rule_thm>\<open>real_divide_divide1\<close>,
1.69 - (*"?y ~= 0 ==> ?u / ?v / (?y / ?z) = ?u / ?v * (?z / ?y)"*)
1.70 - \<^rule_thm>\<open>divide_divide_eq_left\<close>,
1.71 - (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
1.72 + \<^rule_thm>\<open>real_divide_divide1\<close>, (*"?y ~= 0 ==> ?u / ?v / (?y / ?z) = ?u / ?v * (?z / ?y)"*)
1.73 + \<^rule_thm>\<open>divide_divide_eq_left\<close>, (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
1.74
1.75 - \<^rule_thm>\<open>rat_power\<close>,
1.76 - (*"(?a / ?b) \<up> ?n = ?a \<up> ?n / ?b \<up> ?n"*)
1.77 + \<^rule_thm>\<open>rat_power\<close>, (*"(?a / ?b) \<up> ?n = ?a \<up> ?n / ?b \<up> ?n"*)
1.78
1.79 - \<^rule_thm>\<open>mult_cross\<close>,
1.80 - (*"[| b ~= 0; d ~= 0 |] ==> (a / b = c / d) = (a * d = b * c)*)
1.81 - \<^rule_thm>\<open>mult_cross1\<close>,
1.82 - (*" b ~= 0 ==> (a / b = c ) = (a = b * c)*)
1.83 - \<^rule_thm>\<open>mult_cross2\<close>
1.84 - (*" d ~= 0 ==> (a = c / d) = (a * d = c)*)],
1.85 + \<^rule_thm>\<open>mult_cross\<close>, (*"[| b ~= 0; d ~= 0 |] ==> (a / b = c / d) = (a * d = b * c)*)
1.86 + \<^rule_thm>\<open>mult_cross1\<close>, (*" b ~= 0 ==> (a / b = c ) = (a = b * c)*)
1.87 + \<^rule_thm>\<open>mult_cross2\<close> (*" d ~= 0 ==> (a = c / d) = (a * d = c)*)],
1.88 scr = Rule.Empty_Prog})
1.89 calculate_Poly);
1.90
1.91 @@ -481,8 +466,8 @@
1.92 ML \<open>
1.93 val rational_erls =
1.94 Rule_Set.merge "rational_erls" calculate_Rational
1.95 - (Rule_Set.append_rules "is_expanded" Atools_erls
1.96 - [\<^rule_eval>\<open>is_expanded\<close> (eval_is_expanded "")]);
1.97 + (Rule_Set.append_rules "is_expanded" Atools_erls [
1.98 + \<^rule_eval>\<open>is_expanded\<close> (eval_is_expanded "")]);
1.99 \<close>
1.100
1.101 subsection \<open>Embed cancellation into rewriting\<close>
1.102 @@ -554,7 +539,7 @@
1.103
1.104 fun init_state thy eval_rls ro t =
1.105 let
1.106 - val SOME (t',_) = common_nominator_p_ thy t;
1.107 + val SOME (t', _) = common_nominator_p_ thy t;
1.108 val SOME (t'', asm) = add_fraction_p_ thy t;
1.109 val der = Derive.steps_reverse thy eval_rls rules ro NONE t';
1.110 val der = der @
1.111 @@ -623,145 +608,114 @@
1.112 val powers = prep_rls'(
1.113 Rule_Def.Repeat {id = "powers", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
1.114 erls = powers_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.115 - rules = [\<^rule_thm>\<open>realpow_multI\<close>,
1.116 - (*"(r * s) \<up> n = r \<up> n * s \<up> n"*)
1.117 - \<^rule_thm>\<open>realpow_pow\<close>,
1.118 - (*"(a \<up> b) \<up> c = a \<up> (b * c)"*)
1.119 - \<^rule_thm>\<open>realpow_oneI\<close>,
1.120 - (*"r \<up> 1 = r"*)
1.121 - \<^rule_thm>\<open>realpow_minus_even\<close>,
1.122 - (*"n is_even ==> (- r) \<up> n = r \<up> n" ?-->discard_minus?*)
1.123 - \<^rule_thm>\<open>realpow_minus_odd\<close>,
1.124 - (*"Not (n is_even) ==> (- r) \<up> n = -1 * r \<up> n"*)
1.125 -
1.126 - (*----- collect atoms over * -----*)
1.127 - \<^rule_thm>\<open>realpow_two_atom\<close>,
1.128 - (*"r is_atom ==> r * r = r \<up> 2"*)
1.129 - \<^rule_thm>\<open>realpow_plus_1\<close>,
1.130 - (*"r is_atom ==> r * r \<up> n = r \<up> (n + 1)"*)
1.131 - \<^rule_thm>\<open>realpow_addI_atom\<close>,
1.132 - (*"r is_atom ==> r \<up> n * r \<up> m = r \<up> (n + m)"*)
1.133 + rules = [
1.134 + \<^rule_thm>\<open>realpow_multI\<close>, (*"(r * s) \<up> n = r \<up> n * s \<up> n"*)
1.135 + \<^rule_thm>\<open>realpow_pow\<close>, (*"(a \<up> b) \<up> c = a \<up> (b * c)"*)
1.136 + \<^rule_thm>\<open>realpow_oneI\<close>, (*"r \<up> 1 = r"*)
1.137 + \<^rule_thm>\<open>realpow_minus_even\<close>, (*"n is_even ==> (- r) \<up> n = r \<up> n" ?-->discard_minus?*)
1.138 + \<^rule_thm>\<open>realpow_minus_odd\<close>, (*"Not (n is_even) ==> (- r) \<up> n = -1 * r \<up> n"*)
1.139
1.140 - (*----- distribute none-atoms -----*)
1.141 - \<^rule_thm>\<open>realpow_def_atom\<close>,
1.142 - (*"[| 1 < n; ~ (r is_atom) |]==>r \<up> n = r * r \<up> (n + -1)"*)
1.143 - \<^rule_thm>\<open>realpow_eq_oneI\<close>,
1.144 - (*"1 \<up> n = 1"*)
1.145 - \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")
1.146 - ],
1.147 - scr = Rule.Empty_Prog
1.148 - });
1.149 + (*----- collect atoms over * -----*)
1.150 + \<^rule_thm>\<open>realpow_two_atom\<close>, (*"r is_atom ==> r * r = r \<up> 2"*)
1.151 + \<^rule_thm>\<open>realpow_plus_1\<close>, (*"r is_atom ==> r * r \<up> n = r \<up> (n + 1)"*)
1.152 + \<^rule_thm>\<open>realpow_addI_atom\<close>, (*"r is_atom ==> r \<up> n * r \<up> m = r \<up> (n + m)"*)
1.153 +
1.154 + (*----- distribute none-atoms -----*)
1.155 + \<^rule_thm>\<open>realpow_def_atom\<close>, (*"[| 1 < n; ~ (r is_atom) |]==>r \<up> n = r * r \<up> (n + -1)"*)
1.156 + \<^rule_thm>\<open>realpow_eq_oneI\<close>, (*"1 \<up> n = 1"*)
1.157 + \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")],
1.158 + scr = Rule.Empty_Prog});
1.159 +
1.160 (*.contains absolute minimum of thms for context in norm_Rational.*)
1.161 val rat_mult_divide = prep_rls'(
1.162 Rule_Def.Repeat {id = "rat_mult_divide", preconds = [],
1.163 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1.164 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.165 - rules = [\<^rule_thm>\<open>rat_mult\<close>,
1.166 - (*(1)"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)
1.167 - \<^rule_thm>\<open>times_divide_eq_right\<close>,
1.168 - (*(2)"?a * (?c / ?d) = ?a * ?c / ?d" must be [2],
1.169 - otherwise inv.to a / b / c = ...*)
1.170 - \<^rule_thm>\<open>times_divide_eq_left\<close>,
1.171 - (*"?a / ?b * ?c = ?a * ?c / ?b" order weights x \<up> n too much
1.172 - and does not commute a / b * c \<up> 2 !*)
1.173 + rules = [
1.174 + \<^rule_thm>\<open>rat_mult\<close>, (*(1)"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)
1.175 + \<^rule_thm>\<open>times_divide_eq_right\<close>, (*(2)"?a * (?c / ?d) = ?a * ?c / ?d" must be [2],
1.176 + otherwise inv.to a / b / c = ...*)
1.177 + \<^rule_thm>\<open>times_divide_eq_left\<close>, (*"?a / ?b * ?c = ?a * ?c / ?b" order weights x \<up> n too much
1.178 + and does not commute a / b * c \<up> 2 !*)
1.179
1.180 - \<^rule_thm>\<open>divide_divide_eq_right\<close>,
1.181 - (*"?x / (?y / ?z) = ?x * ?z / ?y"*)
1.182 - \<^rule_thm>\<open>divide_divide_eq_left\<close>,
1.183 - (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
1.184 - \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e")
1.185 - ],
1.186 - scr = Rule.Empty_Prog
1.187 - });
1.188 + \<^rule_thm>\<open>divide_divide_eq_right\<close>, (*"?x / (?y / ?z) = ?x * ?z / ?y"*)
1.189 + \<^rule_thm>\<open>divide_divide_eq_left\<close>, (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
1.190 + \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e")],
1.191 + scr = Rule.Empty_Prog});
1.192
1.193 (*.contains absolute minimum of thms for context in norm_Rational.*)
1.194 val reduce_0_1_2 = prep_rls'(
1.195 Rule_Def.Repeat{id = "reduce_0_1_2", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1.196 - erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.197 - rules = [(*\<^rule_thm>\<open>divide_1\<close>,
1.198 - "?x / 1 = ?x" unnecess.for normalform*)
1.199 - \<^rule_thm>\<open>mult_1_left\<close>,
1.200 - (*"1 * z = z"*)
1.201 - (*\<^rule_thm>\<open>real_mult_minus1\<close>,
1.202 - "-1 * z = - z"*)
1.203 - (*\<^rule_thm>\<open>real_minus_mult_cancel\<close>,
1.204 - "- ?x * - ?y = ?x * ?y"*)
1.205 -
1.206 - \<^rule_thm>\<open>mult_zero_left\<close>,
1.207 - (*"0 * z = 0"*)
1.208 - \<^rule_thm>\<open>add_0_left\<close>,
1.209 - (*"0 + z = z"*)
1.210 - (*\<^rule_thm>\<open>right_minus\<close>,
1.211 - "?z + - ?z = 0"*)
1.212 -
1.213 - \<^rule_thm_sym>\<open>real_mult_2\<close>,
1.214 - (*"z1 + z1 = 2 * z1"*)
1.215 - \<^rule_thm>\<open>real_mult_2_assoc\<close>,
1.216 - (*"z1 + (z1 + k) = 2 * z1 + k"*)
1.217 -
1.218 - \<^rule_thm>\<open>division_ring_divide_zero\<close>
1.219 - (*"0 / ?x = 0"*)
1.220 - ], scr = Rule.Empty_Prog});
1.221 + erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.222 + rules = [
1.223 + (*\<^rule_thm>\<open>divide_1\<close>, "?x / 1 = ?x" unnecessary.for normalform*)
1.224 + \<^rule_thm>\<open>mult_1_left\<close>, (*"1 * z = z"*)
1.225 + (*\<^rule_thm>\<open>real_mult_minus1\<close>, "-1 * z = - z"*)
1.226 + (*\<^rule_thm>\<open>real_minus_mult_cancel\<close>, "- ?x * - ?y = ?x * ?y"*)
1.227 +
1.228 +
1.229 + \<^rule_thm>\<open>mult_zero_left\<close>, (*"0 * z = 0"*)
1.230 + \<^rule_thm>\<open>add_0_left\<close>, (*"0 + z = z"*)
1.231 + (*\<^rule_thm>\<open>right_minus\<close>, "?z + - ?z = 0"*)
1.232 +
1.233 + \<^rule_thm_sym>\<open>real_mult_2\<close>, (*"z1 + z1 = 2 * z1"*)
1.234 + \<^rule_thm>\<open>real_mult_2_assoc\<close>, (*"z1 + (z1 + k) = 2 * z1 + k"*)
1.235 +
1.236 + \<^rule_thm>\<open>division_ring_divide_zero\<close> (*"0 / ?x = 0"*)],
1.237 + scr = Rule.Empty_Prog});
1.238
1.239 (*erls for calculate_Rational;
1.240 make local with FIXX@ME result:term *term list WN0609???SKMG*)
1.241 val norm_rat_erls = prep_rls'(
1.242 Rule_Def.Repeat {id = "norm_rat_erls", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
1.243 - erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.244 - rules = [\<^rule_eval>\<open>Prog_Expr.is_const\<close> (Prog_Expr.eval_const "#is_const_")
1.245 - ], scr = Rule.Empty_Prog});
1.246 + erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.247 + rules = [
1.248 + \<^rule_eval>\<open>Prog_Expr.is_const\<close> (Prog_Expr.eval_const "#is_const_")],
1.249 + scr = Rule.Empty_Prog});
1.250
1.251 (* consists of rls containing the absolute minimum of thms *)
1.252 -(*040209: this version has been used by RL for his equations,
1.253 -which is now replaced by MGs version "norm_Rational" below *)
1.254 +(*
1.255 + which is now replaced by MGs version "norm_Rational" below
1.256 +*)
1.257 val norm_Rational_min = prep_rls'(
1.258 Rule_Def.Repeat {id = "norm_Rational_min", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
1.259 - erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.260 - rules = [(*sequence given by operator precedence*)
1.261 - Rule.Rls_ discard_minus,
1.262 - Rule.Rls_ powers,
1.263 - Rule.Rls_ rat_mult_divide,
1.264 - Rule.Rls_ expand,
1.265 - Rule.Rls_ reduce_0_1_2,
1.266 - Rule.Rls_ order_add_mult,
1.267 - Rule.Rls_ collect_numerals,
1.268 - Rule.Rls_ add_fractions_p,
1.269 - Rule.Rls_ cancel_p
1.270 - ],
1.271 - scr = Rule.Empty_Prog});
1.272 + erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.273 + rules = [(*sequence given by operator precedence*)
1.274 + Rule.Rls_ discard_minus,
1.275 + Rule.Rls_ powers,
1.276 + Rule.Rls_ rat_mult_divide,
1.277 + Rule.Rls_ expand,
1.278 + Rule.Rls_ reduce_0_1_2,
1.279 + Rule.Rls_ order_add_mult,
1.280 + Rule.Rls_ collect_numerals,
1.281 + Rule.Rls_ add_fractions_p,
1.282 + Rule.Rls_ cancel_p
1.283 + ],
1.284 + scr = Rule.Empty_Prog});
1.285
1.286 val norm_Rational_parenthesized = prep_rls'(
1.287 Rule_Set.Sequence {id = "norm_Rational_parenthesized", preconds = []:term list,
1.288 - rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1.289 - erls = Atools_erls, srls = Rule_Set.Empty,
1.290 - calc = [], errpatts = [],
1.291 - rules = [Rule.Rls_ norm_Rational_min,
1.292 - Rule.Rls_ discard_parentheses
1.293 - ],
1.294 - scr = Rule.Empty_Prog});
1.295 + rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1.296 + erls = Atools_erls, srls = Rule_Set.Empty,
1.297 + calc = [], errpatts = [],
1.298 + rules = [
1.299 + Rule.Rls_ norm_Rational_min,
1.300 + Rule.Rls_ discard_parentheses],
1.301 + scr = Rule.Empty_Prog});
1.302
1.303 (*WN030318???SK: simplifies all but cancel and common_nominator*)
1.304 val simplify_rational =
1.305 - Rule_Set.merge "simplify_rational" expand_binoms
1.306 - (Rule_Set.append_rules "divide" calculate_Rational
1.307 - [\<^rule_thm>\<open>div_by_1\<close>,
1.308 - (*"?x / 1 = ?x"*)
1.309 - \<^rule_thm>\<open>rat_mult\<close>,
1.310 - (*(1)"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)
1.311 - \<^rule_thm>\<open>times_divide_eq_right\<close>,
1.312 - (*(2)"?a * (?c / ?d) = ?a * ?c / ?d" must be [2],
1.313 - otherwise inv.to a / b / c = ...*)
1.314 - \<^rule_thm>\<open>times_divide_eq_left\<close>,
1.315 - (*"?a / ?b * ?c = ?a * ?c / ?b"*)
1.316 - \<^rule_thm>\<open>add_minus\<close>,
1.317 - (*"?a + ?b - ?b = ?a"*)
1.318 - \<^rule_thm>\<open>add_minus1\<close>,
1.319 - (*"?a - ?b + ?b = ?a"*)
1.320 - \<^rule_thm>\<open>divide_minus1\<close>
1.321 - (*"?x / -1 = - ?x"*)
1.322 - ]);
1.323 -\<close>
1.324 -ML \<open>
1.325 + Rule_Set.merge "simplify_rational" expand_binoms
1.326 + (Rule_Set.append_rules "divide" calculate_Rational [
1.327 + \<^rule_thm>\<open>div_by_1\<close>, (*"?x / 1 = ?x"*)
1.328 + \<^rule_thm>\<open>rat_mult\<close>, (*(1)"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)
1.329 + \<^rule_thm>\<open>times_divide_eq_right\<close>, (*(2)"?a * (?c / ?d) = ?a * ?c / ?d" must be [2],
1.330 + otherwise inv.to a / b / c = ...*)
1.331 + \<^rule_thm>\<open>times_divide_eq_left\<close>, (*"?a / ?b * ?c = ?a * ?c / ?b"*)
1.332 + \<^rule_thm>\<open>add_minus\<close>, (*"?a + ?b - ?b = ?a"*)
1.333 + \<^rule_thm>\<open>add_minus1\<close>, (*"?a - ?b + ?b = ?a"*)
1.334 + \<^rule_thm>\<open>divide_minus1\<close> (*"?x / -1 = - ?x"*)]);
1.335 +
1.336 val add_fractions_p_rls = prep_rls'(
1.337 Rule_Def.Repeat {id = "add_fractions_p_rls", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1.338 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.339 @@ -780,14 +734,12 @@
1.340 used in initial part norm_Rational_mg, see example DA-M02-main.p.60.*)
1.341 val rat_mult_poly = prep_rls'(
1.342 Rule_Def.Repeat {id = "rat_mult_poly", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1.343 - erls = Rule_Set.append_rules "Rule_Set.empty-is_polyexp" Rule_Set.empty
1.344 - [\<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp "")],
1.345 + erls = Rule_Set.append_rules "Rule_Set.empty-is_polyexp" Rule_Set.empty [
1.346 + \<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp "")],
1.347 srls = Rule_Set.Empty, calc = [], errpatts = [],
1.348 - rules =
1.349 - [\<^rule_thm>\<open>rat_mult_poly_l\<close>,
1.350 - (*"?c is_polyexp ==> ?c * (?a / ?b) = ?c * ?a / ?b"*)
1.351 - \<^rule_thm>\<open>rat_mult_poly_r\<close>
1.352 - (*"?c is_polyexp ==> ?a / ?b * ?c = ?a * ?c / ?b"*) ],
1.353 + rules = [
1.354 + \<^rule_thm>\<open>rat_mult_poly_l\<close>, (*"?c is_polyexp ==> ?c * (?a / ?b) = ?c * ?a / ?b"*)
1.355 + \<^rule_thm>\<open>rat_mult_poly_r\<close> (*"?c is_polyexp ==> ?a / ?b * ?c = ?a * ?c / ?b"*)],
1.356 scr = Rule.Empty_Prog});
1.357
1.358 (*. makes 'normal' fractions; 'is_polyexp' inhibits double fractions;
1.359 @@ -798,60 +750,50 @@
1.360 val rat_mult_div_pow = prep_rls'(
1.361 Rule_Def.Repeat {id = "rat_mult_div_pow", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
1.362 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.363 - rules = [\<^rule_thm>\<open>rat_mult\<close>,
1.364 - (*"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)
1.365 - \<^rule_thm>\<open>rat_mult_poly_l\<close>,
1.366 - (*"?c is_polyexp ==> ?c * (?a / ?b) = ?c * ?a / ?b"*)
1.367 - \<^rule_thm>\<open>rat_mult_poly_r\<close>,
1.368 - (*"?c is_polyexp ==> ?a / ?b * ?c = ?a * ?c / ?b"*)
1.369 + rules = [
1.370 + \<^rule_thm>\<open>rat_mult\<close>, (*"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)
1.371 + \<^rule_thm>\<open>rat_mult_poly_l\<close>, (*"?c is_polyexp ==> ?c * (?a / ?b) = ?c * ?a / ?b"*)
1.372 + \<^rule_thm>\<open>rat_mult_poly_r\<close>, (*"?c is_polyexp ==> ?a / ?b * ?c = ?a * ?c / ?b"*)
1.373
1.374 - \<^rule_thm>\<open>real_divide_divide1_mg\<close>,
1.375 - (*"y ~= 0 ==> (u / v) / (y / z) = (u * z) / (y * v)"*)
1.376 - \<^rule_thm>\<open>divide_divide_eq_right\<close>,
1.377 - (*"?x / (?y / ?z) = ?x * ?z / ?y"*)
1.378 - \<^rule_thm>\<open>divide_divide_eq_left\<close>,
1.379 - (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
1.380 + \<^rule_thm>\<open>real_divide_divide1_mg\<close>, (*"y ~= 0 ==> (u / v) / (y / z) = (u * z) / (y * v)"*)
1.381 + \<^rule_thm>\<open>divide_divide_eq_right\<close>, (*"?x / (?y / ?z) = ?x * ?z / ?y"*)
1.382 + \<^rule_thm>\<open>divide_divide_eq_left\<close>, (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
1.383 \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
1.384
1.385 - \<^rule_thm>\<open>rat_power\<close>
1.386 - (*"(?a / ?b) \<up> ?n = ?a \<up> ?n / ?b \<up> ?n"*)
1.387 - ],
1.388 + \<^rule_thm>\<open>rat_power\<close> (*"(?a / ?b) \<up> ?n = ?a \<up> ?n / ?b \<up> ?n"*)],
1.389 scr = Rule.Empty_Prog});
1.390
1.391 val rat_reduce_1 = prep_rls'(
1.392 Rule_Def.Repeat {id = "rat_reduce_1", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1.393 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.394 - rules =
1.395 - [\<^rule_thm>\<open>div_by_1\<close>,
1.396 - (*"?x / 1 = ?x"*)
1.397 - \<^rule_thm>\<open>mult_1_left\<close>
1.398 - (*"1 * z = z"*)
1.399 - ],
1.400 + rules = [
1.401 + \<^rule_thm>\<open>div_by_1\<close>, (*"?x / 1 = ?x"*)
1.402 + \<^rule_thm>\<open>mult_1_left\<close> (*"1 * z = z"*)],
1.403 scr = Rule.Empty_Prog});
1.404
1.405 (* looping part of norm_Rational *)
1.406 val norm_Rational_rls = prep_rls' (
1.407 Rule_Def.Repeat {id = "norm_Rational_rls", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
1.408 erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.409 - rules = [Rule.Rls_ add_fractions_p_rls,
1.410 + rules = [
1.411 + Rule.Rls_ add_fractions_p_rls,
1.412 Rule.Rls_ rat_mult_div_pow,
1.413 Rule.Rls_ make_rat_poly_with_parentheses,
1.414 Rule.Rls_ cancel_p_rls,
1.415 - Rule.Rls_ rat_reduce_1
1.416 - ],
1.417 + Rule.Rls_ rat_reduce_1],
1.418 scr = Rule.Empty_Prog});
1.419
1.420 val norm_Rational = prep_rls' (
1.421 Rule_Set.Sequence
1.422 {id = "norm_Rational", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1.423 erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.424 - rules = [Rule.Rls_ discard_minus,
1.425 + rules = [
1.426 + Rule.Rls_ discard_minus,
1.427 Rule.Rls_ rat_mult_poly, (* removes double fractions like a/b/c *)
1.428 Rule.Rls_ make_rat_poly_with_parentheses,
1.429 Rule.Rls_ cancel_p_rls,
1.430 Rule.Rls_ norm_Rational_rls, (* the main rls, looping (#) *)
1.431 - Rule.Rls_ discard_parentheses1 (* mult only *)
1.432 - ],
1.433 + Rule.Rls_ discard_parentheses1], (* mult only *)
1.434 scr = Rule.Empty_Prog});
1.435 \<close>
1.436