1.1 --- a/src/Tools/isac/Knowledge/Rational.thy Sat Jun 12 14:29:10 2021 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Sat Jun 12 18:06:27 2021 +0200
1.3 @@ -396,8 +396,8 @@
1.4 rules =
1.5 [\<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"),
1.6 \<^rule_eval>\<open>Prog_Expr.is_const\<close> (Prog_Expr.eval_const "#is_const_"),
1.7 - Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true}),
1.8 - Rule.Thm ("not_false", ThmC.numerals_to_Free @{thm not_false})],
1.9 + \<^rule_thm>\<open>not_true\<close>,
1.10 + \<^rule_thm>\<open>not_false\<close>],
1.11 scr = Rule.Empty_Prog});
1.12
1.13 (* simplifies expressions with numerals;
1.14 @@ -413,37 +413,37 @@
1.15
1.16 Rule.Thm ("minus_divide_left", ThmC.numerals_to_Free (@{thm minus_divide_left} RS @{thm sym})),
1.17 (*SYM - ?x / ?y = - (?x / ?y) may come from subst*)
1.18 - Rule.Thm ("rat_add", ThmC.numerals_to_Free @{thm rat_add}),
1.19 + \<^rule_thm>\<open>rat_add\<close>,
1.20 (*"[| a is_const; b is_const; c is_const; d is_const |] ==> \
1.21 \a / c + b / d = (a * d) / (c * d) + (b * c ) / (d * c)"*)
1.22 - Rule.Thm ("rat_add1", ThmC.numerals_to_Free @{thm rat_add1}),
1.23 + \<^rule_thm>\<open>rat_add1\<close>,
1.24 (*"[| a is_const; b is_const; c is_const |] ==> a / c + b / c = (a + b) / c"*)
1.25 - Rule.Thm ("rat_add2", ThmC.numerals_to_Free @{thm rat_add2}),
1.26 + \<^rule_thm>\<open>rat_add2\<close>,
1.27 (*"[| ?a is_const; ?b is_const; ?c is_const |] ==> ?a / ?c + ?b = (?a + ?b * ?c) / ?c"*)
1.28 - Rule.Thm ("rat_add3", ThmC.numerals_to_Free @{thm rat_add3}),
1.29 + \<^rule_thm>\<open>rat_add3\<close>,
1.30 (*"[| a is_const; b is_const; c is_const |] ==> a + b / c = (a * c) / c + b / c"\
1.31 .... is_const to be omitted here FIXME*)
1.32
1.33 - Rule.Thm ("rat_mult", ThmC.numerals_to_Free @{thm rat_mult}),
1.34 + \<^rule_thm>\<open>rat_mult\<close>,
1.35 (*a / b * (c / d) = a * c / (b * d)*)
1.36 - Rule.Thm ("times_divide_eq_right", ThmC.numerals_to_Free @{thm times_divide_eq_right}),
1.37 + \<^rule_thm>\<open>times_divide_eq_right\<close>,
1.38 (*?x * (?y / ?z) = ?x * ?y / ?z*)
1.39 - Rule.Thm ("times_divide_eq_left", ThmC.numerals_to_Free @{thm times_divide_eq_left}),
1.40 + \<^rule_thm>\<open>times_divide_eq_left\<close>,
1.41 (*?y / ?z * ?x = ?y * ?x / ?z*)
1.42
1.43 - Rule.Thm ("real_divide_divide1", ThmC.numerals_to_Free @{thm real_divide_divide1}),
1.44 + \<^rule_thm>\<open>real_divide_divide1\<close>,
1.45 (*"?y ~= 0 ==> ?u / ?v / (?y / ?z) = ?u / ?v * (?z / ?y)"*)
1.46 - Rule.Thm ("divide_divide_eq_left", ThmC.numerals_to_Free @{thm divide_divide_eq_left}),
1.47 + \<^rule_thm>\<open>divide_divide_eq_left\<close>,
1.48 (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
1.49
1.50 - Rule.Thm ("rat_power", ThmC.numerals_to_Free @{thm rat_power}),
1.51 + \<^rule_thm>\<open>rat_power\<close>,
1.52 (*"(?a / ?b) \<up> ?n = ?a \<up> ?n / ?b \<up> ?n"*)
1.53
1.54 - Rule.Thm ("mult_cross", ThmC.numerals_to_Free @{thm mult_cross}),
1.55 + \<^rule_thm>\<open>mult_cross\<close>,
1.56 (*"[| b ~= 0; d ~= 0 |] ==> (a / b = c / d) = (a * d = b * c)*)
1.57 - Rule.Thm ("mult_cross1", ThmC.numerals_to_Free @{thm mult_cross1}),
1.58 + \<^rule_thm>\<open>mult_cross1\<close>,
1.59 (*" b ~= 0 ==> (a / b = c ) = (a = b * c)*)
1.60 - Rule.Thm ("mult_cross2", ThmC.numerals_to_Free @{thm mult_cross2})
1.61 + \<^rule_thm>\<open>mult_cross2\<close>
1.62 (*" d ~= 0 ==> (a = c / d) = (a * d = c)*)],
1.63 scr = Rule.Empty_Prog})
1.64 calculate_Poly);
1.65 @@ -479,7 +479,7 @@
1.66 val SOME (t'', asm) = cancel_p_ thy t;
1.67 val der = Derive.steps_reverse thy eval_rls rules ro NONE t';
1.68 val der = der @
1.69 - [(Rule.Thm ("real_mult_div_cancel2", ThmC.numerals_to_Free @{thm real_mult_div_cancel2}), (t'', asm))]
1.70 + [(\<^rule_thm>\<open>real_mult_div_cancel2\<close>, (t'', asm))]
1.71 val rs = (Rule.distinct' o (map #1)) der
1.72 val rs = filter_out (ThmC.member'
1.73 ["sym_real_add_zero_left", "sym_real_mult_0", "sym_real_mult_1"]) rs
1.74 @@ -540,7 +540,7 @@
1.75 val SOME (t'', asm) = add_fraction_p_ thy t;
1.76 val der = Derive.steps_reverse thy eval_rls rules ro NONE t';
1.77 val der = der @
1.78 - [(Rule.Thm ("real_mult_div_cancel2", ThmC.numerals_to_Free @{thm real_mult_div_cancel2}), (t'',asm))]
1.79 + [(\<^rule_thm>\<open>real_mult_div_cancel2\<close>, (t'',asm))]
1.80 val rs = (Rule.distinct' o (map #1)) der;
1.81 val rs = filter_out (ThmC.member'
1.82 ["sym_real_add_zero_left", "sym_real_mult_0", "sym_real_mult_1"]) rs;
1.83 @@ -607,8 +607,8 @@
1.84 rules = [\<^rule_eval>\<open>Prog_Expr.is_atom\<close> (Prog_Expr.eval_is_atom "#is_atom_"),
1.85 \<^rule_eval>\<open>Prog_Expr.is_even\<close> (Prog_Expr.eval_is_even "#is_even_"),
1.86 \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
1.87 - Rule.Thm ("not_false", ThmC.numerals_to_Free @{thm not_false}),
1.88 - Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true}),
1.89 + \<^rule_thm>\<open>not_false\<close>,
1.90 + \<^rule_thm>\<open>not_true\<close>,
1.91 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")
1.92 ],
1.93 scr = Rule.Empty_Prog
1.94 @@ -618,29 +618,29 @@
1.95 val powers = prep_rls'(
1.96 Rule_Def.Repeat {id = "powers", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
1.97 erls = powers_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.98 - rules = [Rule.Thm ("realpow_multI", ThmC.numerals_to_Free @{thm realpow_multI}),
1.99 + rules = [\<^rule_thm>\<open>realpow_multI\<close>,
1.100 (*"(r * s) \<up> n = r \<up> n * s \<up> n"*)
1.101 - Rule.Thm ("realpow_pow",ThmC.numerals_to_Free @{thm realpow_pow}),
1.102 + \<^rule_thm>\<open>realpow_pow\<close>,
1.103 (*"(a \<up> b) \<up> c = a \<up> (b * c)"*)
1.104 - Rule.Thm ("realpow_oneI",ThmC.numerals_to_Free @{thm realpow_oneI}),
1.105 + \<^rule_thm>\<open>realpow_oneI\<close>,
1.106 (*"r \<up> 1 = r"*)
1.107 - Rule.Thm ("realpow_minus_even",ThmC.numerals_to_Free @{thm realpow_minus_even}),
1.108 + \<^rule_thm>\<open>realpow_minus_even\<close>,
1.109 (*"n is_even ==> (- r) \<up> n = r \<up> n" ?-->discard_minus?*)
1.110 - Rule.Thm ("realpow_minus_odd",ThmC.numerals_to_Free @{thm realpow_minus_odd}),
1.111 + \<^rule_thm>\<open>realpow_minus_odd\<close>,
1.112 (*"Not (n is_even) ==> (- r) \<up> n = -1 * r \<up> n"*)
1.113
1.114 (*----- collect atoms over * -----*)
1.115 - Rule.Thm ("realpow_two_atom",ThmC.numerals_to_Free @{thm realpow_two_atom}),
1.116 + \<^rule_thm>\<open>realpow_two_atom\<close>,
1.117 (*"r is_atom ==> r * r = r \<up> 2"*)
1.118 - Rule.Thm ("realpow_plus_1",ThmC.numerals_to_Free @{thm realpow_plus_1}),
1.119 + \<^rule_thm>\<open>realpow_plus_1\<close>,
1.120 (*"r is_atom ==> r * r \<up> n = r \<up> (n + 1)"*)
1.121 - Rule.Thm ("realpow_addI_atom",ThmC.numerals_to_Free @{thm realpow_addI_atom}),
1.122 + \<^rule_thm>\<open>realpow_addI_atom\<close>,
1.123 (*"r is_atom ==> r \<up> n * r \<up> m = r \<up> (n + m)"*)
1.124
1.125 (*----- distribute none-atoms -----*)
1.126 - Rule.Thm ("realpow_def_atom",ThmC.numerals_to_Free @{thm realpow_def_atom}),
1.127 + \<^rule_thm>\<open>realpow_def_atom\<close>,
1.128 (*"[| 1 < n; ~ (r is_atom) |]==>r \<up> n = r * r \<up> (n + -1)"*)
1.129 - Rule.Thm ("realpow_eq_oneI",ThmC.numerals_to_Free @{thm realpow_eq_oneI}),
1.130 + \<^rule_thm>\<open>realpow_eq_oneI\<close>,
1.131 (*"1 \<up> n = 1"*)
1.132 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")
1.133 ],
1.134 @@ -651,12 +651,12 @@
1.135 Rule_Def.Repeat {id = "rat_mult_divide", preconds = [],
1.136 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1.137 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.138 - rules = [Rule.Thm ("rat_mult",ThmC.numerals_to_Free @{thm rat_mult}),
1.139 + rules = [\<^rule_thm>\<open>rat_mult\<close>,
1.140 (*(1)"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)
1.141 - Rule.Thm ("times_divide_eq_right",ThmC.numerals_to_Free @{thm times_divide_eq_right}),
1.142 + \<^rule_thm>\<open>times_divide_eq_right\<close>,
1.143 (*(2)"?a * (?c / ?d) = ?a * ?c / ?d" must be [2],
1.144 otherwise inv.to a / b / c = ...*)
1.145 - Rule.Thm ("times_divide_eq_left",ThmC.numerals_to_Free @{thm times_divide_eq_left}),
1.146 + \<^rule_thm>\<open>times_divide_eq_left\<close>,
1.147 (*"?a / ?b * ?c = ?a * ?c / ?b" order weights x \<up> n too much
1.148 and does not commute a / b * c \<up> 2 !*)
1.149
1.150 @@ -675,28 +675,28 @@
1.151 val reduce_0_1_2 = prep_rls'(
1.152 Rule_Def.Repeat{id = "reduce_0_1_2", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1.153 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.154 - rules = [(*Rule.Thm ("divide_1",ThmC.numerals_to_Free @{thm divide_1}),
1.155 + rules = [(*\<^rule_thm>\<open>divide_1\<close>,
1.156 "?x / 1 = ?x" unnecess.for normalform*)
1.157 - Rule.Thm ("mult_1_left",ThmC.numerals_to_Free @{thm mult_1_left}),
1.158 + \<^rule_thm>\<open>mult_1_left\<close>,
1.159 (*"1 * z = z"*)
1.160 - (*Rule.Thm ("real_mult_minus1",ThmC.numerals_to_Free @{thm real_mult_minus1}),
1.161 + (*\<^rule_thm>\<open>real_mult_minus1\<close>,
1.162 "-1 * z = - z"*)
1.163 - (*Rule.Thm ("real_minus_mult_cancel",ThmC.numerals_to_Free @{thm real_minus_mult_cancel}),
1.164 + (*\<^rule_thm>\<open>real_minus_mult_cancel\<close>,
1.165 "- ?x * - ?y = ?x * ?y"*)
1.166
1.167 - Rule.Thm ("mult_zero_left",ThmC.numerals_to_Free @{thm mult_zero_left}),
1.168 + \<^rule_thm>\<open>mult_zero_left\<close>,
1.169 (*"0 * z = 0"*)
1.170 - Rule.Thm ("add_0_left",ThmC.numerals_to_Free @{thm add_0_left}),
1.171 + \<^rule_thm>\<open>add_0_left\<close>,
1.172 (*"0 + z = z"*)
1.173 - (*Rule.Thm ("right_minus",ThmC.numerals_to_Free @{thm right_minus}),
1.174 + (*\<^rule_thm>\<open>right_minus\<close>,
1.175 "?z + - ?z = 0"*)
1.176
1.177 \<^rule_thm_sym>\<open>real_mult_2\<close>,
1.178 (*"z1 + z1 = 2 * z1"*)
1.179 - Rule.Thm ("real_mult_2_assoc",ThmC.numerals_to_Free @{thm real_mult_2_assoc}),
1.180 + \<^rule_thm>\<open>real_mult_2_assoc\<close>,
1.181 (*"z1 + (z1 + k) = 2 * z1 + k"*)
1.182
1.183 - Rule.Thm ("division_ring_divide_zero",ThmC.numerals_to_Free @{thm division_ring_divide_zero})
1.184 + \<^rule_thm>\<open>division_ring_divide_zero\<close>
1.185 (*"0 / ?x = 0"*)
1.186 ], scr = Rule.Empty_Prog});
1.187
1.188 @@ -741,20 +741,20 @@
1.189 val simplify_rational =
1.190 Rule_Set.merge "simplify_rational" expand_binoms
1.191 (Rule_Set.append_rules "divide" calculate_Rational
1.192 - [Rule.Thm ("div_by_1",ThmC.numerals_to_Free @{thm div_by_1}),
1.193 + [\<^rule_thm>\<open>div_by_1\<close>,
1.194 (*"?x / 1 = ?x"*)
1.195 - Rule.Thm ("rat_mult",ThmC.numerals_to_Free @{thm rat_mult}),
1.196 + \<^rule_thm>\<open>rat_mult\<close>,
1.197 (*(1)"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)
1.198 - Rule.Thm ("times_divide_eq_right",ThmC.numerals_to_Free @{thm times_divide_eq_right}),
1.199 + \<^rule_thm>\<open>times_divide_eq_right\<close>,
1.200 (*(2)"?a * (?c / ?d) = ?a * ?c / ?d" must be [2],
1.201 otherwise inv.to a / b / c = ...*)
1.202 - Rule.Thm ("times_divide_eq_left",ThmC.numerals_to_Free @{thm times_divide_eq_left}),
1.203 + \<^rule_thm>\<open>times_divide_eq_left\<close>,
1.204 (*"?a / ?b * ?c = ?a * ?c / ?b"*)
1.205 - Rule.Thm ("add_minus",ThmC.numerals_to_Free @{thm add_minus}),
1.206 + \<^rule_thm>\<open>add_minus\<close>,
1.207 (*"?a + ?b - ?b = ?a"*)
1.208 - Rule.Thm ("add_minus1",ThmC.numerals_to_Free @{thm add_minus1}),
1.209 + \<^rule_thm>\<open>add_minus1\<close>,
1.210 (*"?a - ?b + ?b = ?a"*)
1.211 - Rule.Thm ("divide_minus1",ThmC.numerals_to_Free @{thm divide_minus1})
1.212 + \<^rule_thm>\<open>divide_minus1\<close>
1.213 (*"?x / -1 = - ?x"*)
1.214 ]);
1.215 \<close>
1.216 @@ -781,9 +781,9 @@
1.217 [\<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp "")],
1.218 srls = Rule_Set.Empty, calc = [], errpatts = [],
1.219 rules =
1.220 - [Rule.Thm ("rat_mult_poly_l",ThmC.numerals_to_Free @{thm rat_mult_poly_l}),
1.221 + [\<^rule_thm>\<open>rat_mult_poly_l\<close>,
1.222 (*"?c is_polyexp ==> ?c * (?a / ?b) = ?c * ?a / ?b"*)
1.223 - Rule.Thm ("rat_mult_poly_r",ThmC.numerals_to_Free @{thm rat_mult_poly_r})
1.224 + \<^rule_thm>\<open>rat_mult_poly_r\<close>
1.225 (*"?c is_polyexp ==> ?a / ?b * ?c = ?a * ?c / ?b"*) ],
1.226 scr = Rule.Empty_Prog});
1.227
1.228 @@ -795,22 +795,22 @@
1.229 val rat_mult_div_pow = prep_rls'(
1.230 Rule_Def.Repeat {id = "rat_mult_div_pow", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
1.231 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.232 - rules = [Rule.Thm ("rat_mult", ThmC.numerals_to_Free @{thm rat_mult}),
1.233 + rules = [\<^rule_thm>\<open>rat_mult\<close>,
1.234 (*"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)
1.235 - Rule.Thm ("rat_mult_poly_l", ThmC.numerals_to_Free @{thm rat_mult_poly_l}),
1.236 + \<^rule_thm>\<open>rat_mult_poly_l\<close>,
1.237 (*"?c is_polyexp ==> ?c * (?a / ?b) = ?c * ?a / ?b"*)
1.238 - Rule.Thm ("rat_mult_poly_r", ThmC.numerals_to_Free @{thm rat_mult_poly_r}),
1.239 + \<^rule_thm>\<open>rat_mult_poly_r\<close>,
1.240 (*"?c is_polyexp ==> ?a / ?b * ?c = ?a * ?c / ?b"*)
1.241
1.242 - Rule.Thm ("real_divide_divide1_mg", ThmC.numerals_to_Free @{thm real_divide_divide1_mg}),
1.243 + \<^rule_thm>\<open>real_divide_divide1_mg\<close>,
1.244 (*"y ~= 0 ==> (u / v) / (y / z) = (u * z) / (y * v)"*)
1.245 - Rule.Thm ("divide_divide_eq_right", ThmC.numerals_to_Free @{thm divide_divide_eq_right}),
1.246 + \<^rule_thm>\<open>divide_divide_eq_right\<close>,
1.247 (*"?x / (?y / ?z) = ?x * ?z / ?y"*)
1.248 - Rule.Thm ("divide_divide_eq_left", ThmC.numerals_to_Free @{thm divide_divide_eq_left}),
1.249 + \<^rule_thm>\<open>divide_divide_eq_left\<close>,
1.250 (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
1.251 \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
1.252
1.253 - Rule.Thm ("rat_power", ThmC.numerals_to_Free @{thm rat_power})
1.254 + \<^rule_thm>\<open>rat_power\<close>
1.255 (*"(?a / ?b) \<up> ?n = ?a \<up> ?n / ?b \<up> ?n"*)
1.256 ],
1.257 scr = Rule.Empty_Prog});
1.258 @@ -819,9 +819,9 @@
1.259 Rule_Def.Repeat {id = "rat_reduce_1", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1.260 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.261 rules =
1.262 - [Rule.Thm ("div_by_1", ThmC.numerals_to_Free @{thm div_by_1}),
1.263 + [\<^rule_thm>\<open>div_by_1\<close>,
1.264 (*"?x / 1 = ?x"*)
1.265 - Rule.Thm ("mult_1_left", ThmC.numerals_to_Free @{thm mult_1_left})
1.266 + \<^rule_thm>\<open>mult_1_left\<close>
1.267 (*"1 * z = z"*)
1.268 ],
1.269 scr = Rule.Empty_Prog});