1.1 --- a/src/Tools/isac/Knowledge/Integrate.thy Wed Apr 15 11:11:54 2020 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy Wed Apr 15 11:37:43 2020 +0200
1.3 @@ -44,7 +44,7 @@
1.4 (** eval functions **)
1.5
1.6 val c = Free ("c", HOLogic.realT);
1.7 -(*.create a new unique variable 'c..' in a term; for use by Rule.Num_Calc in a rls;
1.8 +(*.create a new unique variable 'c..' in a term; for use by Rule.Eval in a rls;
1.9 an alternative to do this would be '(Try (Calculate new_c_) (new_c es__))'
1.10 in the script; this will be possible if currying doesnt take the value
1.11 from a variable, but the value '(new_c es__)' itself.*)
1.12 @@ -118,11 +118,11 @@
1.13 erls = Rule_Set.Empty,
1.14 srls = Rule_Set.Empty, calc = [], errpatts = [],
1.15 rules = [(*for rewriting conditions in Thm's*)
1.16 - Rule.Num_Calc ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in "#occurs_in_"),
1.17 + Rule.Eval ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in "#occurs_in_"),
1.18 Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true}),
1.19 Rule.Thm ("not_false",@{thm not_false})
1.20 ],
1.21 - scr = Rule.EmptyScr},
1.22 + scr = Rule.Empty_Prog},
1.23 srls = Rule_Set.Empty, calc = [], errpatts = [],
1.24 rules = [
1.25 Rule.Thm ("integral_const", ThmC.numerals_to_Free @{thm integral_const}),
1.26 @@ -130,31 +130,31 @@
1.27 Rule.Thm ("integral_add", ThmC.numerals_to_Free @{thm integral_add}),
1.28 Rule.Thm ("integral_mult", ThmC.numerals_to_Free @{thm integral_mult}),
1.29 Rule.Thm ("integral_pow", ThmC.numerals_to_Free @{thm integral_pow}),
1.30 - Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_")(*for n+1*)
1.31 + Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_")(*for n+1*)
1.32 ],
1.33 - scr = Rule.EmptyScr};
1.34 + scr = Rule.Empty_Prog};
1.35 \<close>
1.36 ML \<open>
1.37 val add_new_c =
1.38 - Rule_Set.Seqence {id="add_new_c", preconds = [],
1.39 + Rule_Set.Sequence {id="add_new_c", preconds = [],
1.40 rew_ord = ("termlessI",termlessI),
1.41 erls = Rule_Def.Repeat {id="conditions_in_add_new_c",
1.42 preconds = [],
1.43 rew_ord = ("termlessI",termlessI),
1.44 erls = Rule_Set.Empty,
1.45 srls = Rule_Set.Empty, calc = [], errpatts = [],
1.46 - rules = [Rule.Num_Calc ("Prog_Expr.matches", Prog_Expr.eval_matches""),
1.47 - Rule.Num_Calc ("Integrate.is'_f'_x",
1.48 + rules = [Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches""),
1.49 + Rule.Eval ("Integrate.is'_f'_x",
1.50 eval_is_f_x "is_f_x_"),
1.51 Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true}),
1.52 Rule.Thm ("not_false", ThmC.numerals_to_Free @{thm not_false})
1.53 ],
1.54 - scr = Rule.EmptyScr},
1.55 + scr = Rule.Empty_Prog},
1.56 srls = Rule_Set.Empty, calc = [], errpatts = [],
1.57 rules = [ (*Rule.Thm ("call_for_new_c", ThmC.numerals_to_Free @{thm call_for_new_c}),*)
1.58 Rule.Cal1 ("Integrate.add'_new'_c", eval_add_new_c "new_c_")
1.59 ],
1.60 - scr = Rule.EmptyScr};
1.61 + scr = Rule.Empty_Prog};
1.62 \<close>
1.63 ML \<open>
1.64
1.65 @@ -171,7 +171,7 @@
1.66 rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
1.67 erls = (*FIXME.WN051028 Rule_Set.empty,*)
1.68 Rule_Set.append_rules "Rule_Set.empty-is_polyexp" Rule_Set.empty
1.69 - [Rule.Num_Calc ("Poly.is'_polyexp",
1.70 + [Rule.Eval ("Poly.is'_polyexp",
1.71 eval_is_polyexp "")],
1.72 srls = Rule_Set.Empty, calc = [], errpatts = [],
1.73 rules = [Rule.Thm ("rat_mult", ThmC.numerals_to_Free @{thm rat_mult}),
1.74 @@ -190,23 +190,23 @@
1.75 Rule.Thm ("divide_divide_eq_left",
1.76 ThmC.numerals_to_Free @{thm divide_divide_eq_left}),
1.77 (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
1.78 - Rule.Num_Calc ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"),
1.79 + Rule.Eval ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"),
1.80
1.81 Rule.Thm ("rat_power", ThmC.numerals_to_Free @{thm rat_power})
1.82 (*"(?a / ?b) ^^^ ?n = ?a ^^^ ?n / ?b ^^^ ?n"*)
1.83 ],
1.84 - scr = Rule.EmptyScr
1.85 + scr = Rule.Empty_Prog
1.86 }),
1.87 Rule.Rls_ make_rat_poly_with_parentheses,
1.88 Rule.Rls_ cancel_p_rls,(*FIXME:cancel_p does NOT order sometimes*)
1.89 Rule.Rls_ rat_reduce_1
1.90 ],
1.91 - scr = Rule.EmptyScr
1.92 + scr = Rule.Empty_Prog
1.93 };
1.94
1.95 (*.for simplify_Integral adapted from 'norm_Rational'.*)
1.96 val norm_Rational_noadd_fractions =
1.97 - Rule_Set.Seqence {id = "norm_Rational_noadd_fractions", preconds = [],
1.98 + Rule_Set.Sequence {id = "norm_Rational_noadd_fractions", preconds = [],
1.99 rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
1.100 erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.101 rules = [Rule.Rls_ discard_minus,
1.102 @@ -216,7 +216,7 @@
1.103 Rule.Rls_ norm_Rational_rls_noadd_fractions,(* the main rls (#) *)
1.104 Rule.Rls_ discard_parentheses1 (* mult only *)
1.105 ],
1.106 - scr = Rule.EmptyScr
1.107 + scr = Rule.Empty_Prog
1.108 };
1.109
1.110 (*.simplify terms before and after Integration such that
1.111 @@ -240,7 +240,7 @@
1.112 (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)----------*)
1.113 ];
1.114 val simplify_Integral =
1.115 - Rule_Set.Seqence {id = "simplify_Integral", preconds = []:term list,
1.116 + Rule_Set.Sequence {id = "simplify_Integral", preconds = []:term list,
1.117 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1.118 erls = Atools_erls, srls = Rule_Set.Empty,
1.119 calc = [], errpatts = [],
1.120 @@ -254,9 +254,9 @@
1.121 Rule.Rls_ discard_parentheses,
1.122 (*Rule.Rls_ collect_bdv, from make_polynomial_in*)
1.123 Rule.Rls_ separate_bdv2,
1.124 - Rule.Num_Calc ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e")
1.125 + Rule.Eval ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e")
1.126 ],
1.127 - scr = Rule.EmptyScr};
1.128 + scr = Rule.Empty_Prog};
1.129
1.130
1.131 (*simplify terms before and after Integration such that
1.132 @@ -266,7 +266,7 @@
1.133 'make_ratpoly_in'
1.134 THIS IS KEPT FOR COMPARISON ............................................
1.135 * val simplify_Integral = prep_rls'(
1.136 -* Rule_Set.Seqence {id = "", preconds = []:term list,
1.137 +* Rule_Set.Sequence {id = "", preconds = []:term list,
1.138 * rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1.139 * erls = Atools_erls, srls = Rule_Set.Empty,
1.140 * calc = [], (*asm_thm = [],*)
1.141 @@ -292,14 +292,14 @@
1.142 * ThmC.numerals_to_Free @{thm add_divide_distrib})
1.143 * (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)*)
1.144 * ]),
1.145 -* Rule.Num_Calc ("Rings.divide_class.divide" , eval_cancel "#divide_e")
1.146 +* Rule.Eval ("Rings.divide_class.divide" , eval_cancel "#divide_e")
1.147 * ],
1.148 -* scr = Rule.EmptyScr
1.149 +* scr = Rule.Empty_Prog
1.150 * });
1.151 .......................................................................*)
1.152
1.153 val integration =
1.154 - Rule_Set.Seqence {id="integration", preconds = [],
1.155 + Rule_Set.Sequence {id="integration", preconds = [],
1.156 rew_ord = ("termlessI",termlessI),
1.157 erls = Rule_Def.Repeat {id="conditions_in_integration",
1.158 preconds = [],
1.159 @@ -307,13 +307,13 @@
1.160 erls = Rule_Set.Empty,
1.161 srls = Rule_Set.Empty, calc = [], errpatts = [],
1.162 rules = [],
1.163 - scr = Rule.EmptyScr},
1.164 + scr = Rule.Empty_Prog},
1.165 srls = Rule_Set.Empty, calc = [], errpatts = [],
1.166 rules = [ Rule.Rls_ integration_rules,
1.167 Rule.Rls_ add_new_c,
1.168 Rule.Rls_ simplify_Integral
1.169 ],
1.170 - scr = Rule.EmptyScr};
1.171 + scr = Rule.Empty_Prog};
1.172
1.173 val prep_rls' = Auto_Prog.prep_rls @{theory};
1.174 \<close>