1.1 --- a/src/Tools/isac/Knowledge/Rational.thy Wed Apr 15 11:11:54 2020 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Wed Apr 15 11:37:43 2020 +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.Num_Calc"\<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 @@ -393,11 +393,11 @@
1.13 (Rule_Def.Repeat {id = "calc_rat_erls", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1.14 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.15 rules =
1.16 - [Rule.Num_Calc ("HOL.eq", Prog_Expr.eval_equal "#equal_"),
1.17 - Rule.Num_Calc ("Prog_Expr.is'_const", Prog_Expr.eval_const "#is_const_"),
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", ThmC.numerals_to_Free @{thm not_true}),
1.21 Rule.Thm ("not_false", ThmC.numerals_to_Free @{thm not_false})],
1.22 - scr = Rule.EmptyScr});
1.23 + scr = Rule.Empty_Prog});
1.24
1.25 (* simplifies expressions with numerals;
1.26 does NOT rearrange the term by AC-rewriting; thus terms with variables
1.27 @@ -408,7 +408,7 @@
1.28 erls = calc_rat_erls, srls = Rule_Set.Empty,
1.29 calc = [], errpatts = [],
1.30 rules =
1.31 - [Rule.Num_Calc ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"),
1.32 + [Rule.Eval ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"),
1.33
1.34 Rule.Thm ("minus_divide_left", ThmC.numerals_to_Free (@{thm minus_divide_left} RS @{thm sym})),
1.35 (*SYM - ?x / ?y = - (?x / ?y) may come from subst*)
1.36 @@ -444,7 +444,7 @@
1.37 (*" b ~= 0 ==> (a / b = c ) = (a = b * c)*)
1.38 Rule.Thm ("mult_cross2", ThmC.numerals_to_Free @{thm mult_cross2})
1.39 (*" d ~= 0 ==> (a = c / d) = (a * d = c)*)],
1.40 - scr = Rule.EmptyScr})
1.41 + scr = Rule.Empty_Prog})
1.42 calculate_Poly);
1.43
1.44 (*("is_expanded", ("Rational.is'_expanded", eval_is_expanded ""))*)
1.45 @@ -463,7 +463,7 @@
1.46 val rational_erls =
1.47 Rule_Set.merge "rational_erls" calculate_Rational
1.48 (Rule_Set.append_rules "is_expanded" Atools_erls
1.49 - [Rule.Num_Calc ("Rational.is'_expanded", eval_is_expanded "")]);
1.50 + [Rule.Eval ("Rational.is'_expanded", eval_is_expanded "")]);
1.51 \<close>
1.52
1.53 subsection \<open>Embed cancellation into rewriting\<close>
1.54 @@ -603,14 +603,14 @@
1.55 val powers_erls = prep_rls'(
1.56 Rule_Def.Repeat {id = "powers_erls", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
1.57 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.58 - rules = [Rule.Num_Calc ("Prog_Expr.is'_atom", Prog_Expr.eval_is_atom "#is_atom_"),
1.59 - Rule.Num_Calc ("Prog_Expr.is'_even", Prog_Expr.eval_is_even "#is_even_"),
1.60 - Rule.Num_Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
1.61 + rules = [Rule.Eval ("Prog_Expr.is'_atom", Prog_Expr.eval_is_atom "#is_atom_"),
1.62 + Rule.Eval ("Prog_Expr.is'_even", Prog_Expr.eval_is_even "#is_even_"),
1.63 + Rule.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
1.64 Rule.Thm ("not_false", ThmC.numerals_to_Free @{thm not_false}),
1.65 Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true}),
1.66 - Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_")
1.67 + Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_")
1.68 ],
1.69 - scr = Rule.EmptyScr
1.70 + scr = Rule.Empty_Prog
1.71 });
1.72 (*.all powers over + distributed; atoms over * collected, other distributed
1.73 contains absolute minimum of thms for context in norm_Rational .*)
1.74 @@ -641,9 +641,9 @@
1.75 (*"[| 1 < n; not(r is_atom) |]==>r ^^^ n = r * r ^^^ (n + -1)"*)
1.76 Rule.Thm ("realpow_eq_oneI",ThmC.numerals_to_Free @{thm realpow_eq_oneI}),
1.77 (*"1 ^^^ n = 1"*)
1.78 - Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_")
1.79 + Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_")
1.80 ],
1.81 - scr = Rule.EmptyScr
1.82 + scr = Rule.Empty_Prog
1.83 });
1.84 (*.contains absolute minimum of thms for context in norm_Rational.*)
1.85 val rat_mult_divide = prep_rls'(
1.86 @@ -665,9 +665,9 @@
1.87 Rule.Thm ("divide_divide_eq_left",
1.88 ThmC.numerals_to_Free @{thm divide_divide_eq_left}),
1.89 (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
1.90 - Rule.Num_Calc ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e")
1.91 + Rule.Eval ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e")
1.92 ],
1.93 - scr = Rule.EmptyScr
1.94 + scr = Rule.Empty_Prog
1.95 });
1.96
1.97 (*.contains absolute minimum of thms for context in norm_Rational.*)
1.98 @@ -698,15 +698,15 @@
1.99
1.100 Rule.Thm ("division_ring_divide_zero",ThmC.numerals_to_Free @{thm division_ring_divide_zero})
1.101 (*"0 / ?x = 0"*)
1.102 - ], scr = Rule.EmptyScr});
1.103 + ], scr = Rule.Empty_Prog});
1.104
1.105 (*erls for calculate_Rational;
1.106 make local with FIXX@ME result:term *term list WN0609???SKMG*)
1.107 val norm_rat_erls = prep_rls'(
1.108 Rule_Def.Repeat {id = "norm_rat_erls", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
1.109 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.110 - rules = [Rule.Num_Calc ("Prog_Expr.is'_const", Prog_Expr.eval_const "#is_const_")
1.111 - ], scr = Rule.EmptyScr});
1.112 + rules = [Rule.Eval ("Prog_Expr.is'_const", Prog_Expr.eval_const "#is_const_")
1.113 + ], scr = Rule.Empty_Prog});
1.114
1.115 (* consists of rls containing the absolute minimum of thms *)
1.116 (*040209: this version has been used by RL for his equations,
1.117 @@ -725,17 +725,17 @@
1.118 Rule.Rls_ add_fractions_p,
1.119 Rule.Rls_ cancel_p
1.120 ],
1.121 - scr = Rule.EmptyScr});
1.122 + scr = Rule.Empty_Prog});
1.123
1.124 val norm_Rational_parenthesized = prep_rls'(
1.125 - Rule_Set.Seqence {id = "norm_Rational_parenthesized", preconds = []:term list,
1.126 + Rule_Set.Sequence {id = "norm_Rational_parenthesized", preconds = []:term list,
1.127 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1.128 erls = Atools_erls, srls = Rule_Set.Empty,
1.129 calc = [], errpatts = [],
1.130 rules = [Rule.Rls_ norm_Rational_min,
1.131 Rule.Rls_ discard_parentheses
1.132 ],
1.133 - scr = Rule.EmptyScr});
1.134 + scr = Rule.Empty_Prog});
1.135
1.136 (*WN030318???SK: simplifies all but cancel and common_nominator*)
1.137 val simplify_rational =
1.138 @@ -763,7 +763,7 @@
1.139 Rule_Def.Repeat {id = "add_fractions_p_rls", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1.140 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.141 rules = [Rule.Rls_ add_fractions_p],
1.142 - scr = Rule.EmptyScr});
1.143 + scr = Rule.Empty_Prog});
1.144
1.145 (* "Rule_Def.Repeat" causes repeated application of cancel_p to one and the same term *)
1.146 val cancel_p_rls = prep_rls'(
1.147 @@ -771,20 +771,20 @@
1.148 {id = "cancel_p_rls", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1.149 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.150 rules = [Rule.Rls_ cancel_p],
1.151 - scr = Rule.EmptyScr});
1.152 + scr = Rule.Empty_Prog});
1.153
1.154 (*. makes 'normal' fractions; 'is_polyexp' inhibits double fractions;
1.155 used in initial part norm_Rational_mg, see example DA-M02-main.p.60.*)
1.156 val rat_mult_poly = prep_rls'(
1.157 Rule_Def.Repeat {id = "rat_mult_poly", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1.158 - erls = Rule_Set.append_rules "Rule_Set.empty-is_polyexp" Rule_Set.empty [Rule.Num_Calc ("Poly.is'_polyexp", eval_is_polyexp "")],
1.159 + erls = Rule_Set.append_rules "Rule_Set.empty-is_polyexp" Rule_Set.empty [Rule.Eval ("Poly.is'_polyexp", eval_is_polyexp "")],
1.160 srls = Rule_Set.Empty, calc = [], errpatts = [],
1.161 rules =
1.162 [Rule.Thm ("rat_mult_poly_l",ThmC.numerals_to_Free @{thm rat_mult_poly_l}),
1.163 (*"?c is_polyexp ==> ?c * (?a / ?b) = ?c * ?a / ?b"*)
1.164 Rule.Thm ("rat_mult_poly_r",ThmC.numerals_to_Free @{thm rat_mult_poly_r})
1.165 (*"?c is_polyexp ==> ?a / ?b * ?c = ?a * ?c / ?b"*) ],
1.166 - scr = Rule.EmptyScr});
1.167 + scr = Rule.Empty_Prog});
1.168
1.169 (*. makes 'normal' fractions; 'is_polyexp' inhibits double fractions;
1.170 used in looping part norm_Rational_rls, see example DA-M02-main.p.60
1.171 @@ -807,12 +807,12 @@
1.172 (*"?x / (?y / ?z) = ?x * ?z / ?y"*)
1.173 Rule.Thm ("divide_divide_eq_left", ThmC.numerals_to_Free @{thm divide_divide_eq_left}),
1.174 (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
1.175 - Rule.Num_Calc ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"),
1.176 + Rule.Eval ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"),
1.177
1.178 Rule.Thm ("rat_power", ThmC.numerals_to_Free @{thm rat_power})
1.179 (*"(?a / ?b) ^^^ ?n = ?a ^^^ ?n / ?b ^^^ ?n"*)
1.180 ],
1.181 - scr = Rule.EmptyScr});
1.182 + scr = Rule.Empty_Prog});
1.183
1.184 val rat_reduce_1 = prep_rls'(
1.185 Rule_Def.Repeat {id = "rat_reduce_1", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1.186 @@ -823,7 +823,7 @@
1.187 Rule.Thm ("mult_1_left", ThmC.numerals_to_Free @{thm mult_1_left})
1.188 (*"1 * z = z"*)
1.189 ],
1.190 - scr = Rule.EmptyScr});
1.191 + scr = Rule.Empty_Prog});
1.192
1.193 (* looping part of norm_Rational *)
1.194 val norm_Rational_rls = prep_rls' (
1.195 @@ -835,10 +835,10 @@
1.196 Rule.Rls_ cancel_p_rls,
1.197 Rule.Rls_ rat_reduce_1
1.198 ],
1.199 - scr = Rule.EmptyScr});
1.200 + scr = Rule.Empty_Prog});
1.201
1.202 val norm_Rational = prep_rls' (
1.203 - Rule_Set.Seqence
1.204 + Rule_Set.Sequence
1.205 {id = "norm_Rational", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1.206 erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.207 rules = [Rule.Rls_ discard_minus,
1.208 @@ -848,7 +848,7 @@
1.209 Rule.Rls_ norm_Rational_rls, (* the main rls, looping (#) *)
1.210 Rule.Rls_ discard_parentheses1 (* mult only *)
1.211 ],
1.212 - scr = Rule.EmptyScr});
1.213 + scr = Rule.Empty_Prog});
1.214 \<close>
1.215
1.216 setup \<open>KEStore_Elems.add_rlss
1.217 @@ -912,7 +912,7 @@
1.218 ("#Find" ,["normalform n_n"])],
1.219 {rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty,
1.220 prls = Rule_Set.append_rules "simplification_of_rationals_prls" Rule_Set.empty
1.221 - [(*for preds in where_*) Rule.Num_Calc ("Rational.is'_ratpolyexp", eval_is_ratpolyexp "")],
1.222 + [(*for preds in where_*) Rule.Eval ("Rational.is'_ratpolyexp", eval_is_ratpolyexp "")],
1.223 crls = Rule_Set.empty, errpats = [], nrls = norm_Rational_rls},
1.224 @{thm simplify.simps})]
1.225 \<close>