1.1 --- a/src/Tools/isac/Interpret/generate.sml Fri Jun 13 09:55:49 2014 +0200
1.2 +++ b/src/Tools/isac/Interpret/generate.sml Fri Jun 13 10:29:06 2014 +0200
1.3 @@ -12,12 +12,12 @@
1.4 *)
1.5 | Rls {scr=EmptyScr,...} =>
1.6 error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
1.7 - ^"use prep_rls for storing rule-sets !")
1.8 + ^"use prep_rls' for storing rule-sets !")
1.9 | Rls {scr = Prog s,...} =>
1.10 (ScrState ([(one_scr_arg s, t)], [], NONE, e_term, Sundef, true))
1.11 | Seq {scr=EmptyScr,...} =>
1.12 error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
1.13 - ^"use prep_rls for storing rule-sets !")
1.14 + ^"use prep_rls' for storing rule-sets !")
1.15 | Seq {srls=srls,scr = Prog s,...} =>
1.16 (ScrState ([(one_scr_arg s, t)], [], NONE, e_term, Sundef, true)))
1.17 (* val ((Rewrite_Set_Inst (subs, rls)), t) = ((get_obj g_tac pt p), t);
1.18 @@ -28,14 +28,14 @@
1.19 in case assoc_rls rls of
1.20 Rls {scr=EmptyScr,...} =>
1.21 error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
1.22 - ^"use prep_rls for storing rule-sets !")
1.23 + ^"use prep_rls' for storing rule-sets !")
1.24 | Rls {scr = Prog s,...} =>
1.25 let val (form, bdv) = two_scr_arg s
1.26 in (ScrState ([(form, t), (bdv, v)],[], NONE, e_term, Sundef,true))
1.27 end
1.28 | Seq {scr=EmptyScr,...} =>
1.29 error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
1.30 - ^"use prep_rls for storing rule-sets !")
1.31 + ^"use prep_rls' for storing rule-sets !")
1.32 | Seq {scr = Prog s,...} =>
1.33 let val (form, bdv) = two_scr_arg s
1.34 in (ScrState ([(form, t), (bdv, v)],[], NONE, e_term, Sundef,true))
2.1 --- a/src/Tools/isac/Knowledge/Atools.thy Fri Jun 13 09:55:49 2014 +0200
2.2 +++ b/src/Tools/isac/Knowledge/Atools.thy Fri Jun 13 10:29:06 2014 +0200
2.3 @@ -109,7 +109,7 @@
2.4 The above rulesets are all visible to the user, and also may be input;
2.5 thus they must be contained in {\tt Theory_Data} (KEStore_Elems.add_rlss,
2.6 KEStore_Elems.get_rlss). All these rulesets must undergo a preparation
2.7 -using the function {\tt prep_rls}, which generates a script for stepwise rewriting etc.
2.8 +using the function {\tt prep_rls'}, which generates a script for stepwise rewriting etc.
2.9 The following rulesets are used for internal purposes and usually invisible to the (naive) user:
2.10 \begin{description}
2.11
2.12 @@ -643,7 +643,7 @@
2.13 Calc ("Tools.matches",eval_matches "#matches")
2.14 ] (*i.A. zu viele rules*)
2.15 );*)
2.16 -(* val atools_erls = prep_rls( (*outcommented*)
2.17 +(* val atools_erls = prep_rls'( (*outcommented*)
2.18 Rls {id="atools_erls",preconds = [], rew_ord = ("termlessI",termlessI),
2.19 erls = e_rls, srls = Erls, calc = [], errpatts = [],
2.20 rules = [Thm ("refl",num_str @{thm refl}),
2.21 @@ -689,7 +689,7 @@
2.22 ("POWER" ,("Atools.pow", eval_binop "#power_")),
2.23 ("boollist2sum",("Atools.boollist2sum", eval_boollist2sum ""))] *}
2.24 ML {*
2.25 -val list_rls = prep_rls' @{theory} (merge_rls "list_erls"
2.26 +val list_rls = prep_rls @{theory} (merge_rls "list_erls"
2.27 (Rls {id = "replaced", preconds = [], rew_ord = ("termlessI", termlessI),
2.28 erls = Rls {id = "list_elrs", preconds = [], rew_ord = ("termlessI", termlessI),
2.29 erls = e_rls, srls = Erls, calc = [], errpatts = [],
2.30 @@ -702,6 +702,6 @@
2.31 list_rls);
2.32 *}
2.33 setup {* KEStore_Elems.add_rlss
2.34 - [("list_rls", (Context.theory_name @{theory}, prep_rls' @{theory} list_rls))] *}
2.35 + [("list_rls", (Context.theory_name @{theory}, prep_rls @{theory} list_rls))] *}
2.36
2.37 end
3.1 --- a/src/Tools/isac/Knowledge/Diff.thy Fri Jun 13 09:55:49 2014 +0200
3.2 +++ b/src/Tools/isac/Knowledge/Diff.thy Fri Jun 13 10:29:06 2014 +0200
3.3 @@ -240,11 +240,11 @@
3.4 scr = EmptyScr};
3.5 *}
3.6 setup {* KEStore_Elems.add_rlss
3.7 - [("erls_diff", (Context.theory_name @{theory}, prep_rls erls_diff)),
3.8 - ("diff_rules", (Context.theory_name @{theory}, prep_rls diff_rules)),
3.9 - ("norm_diff", (Context.theory_name @{theory}, prep_rls norm_diff)),
3.10 - ("diff_conv", (Context.theory_name @{theory}, prep_rls diff_conv)),
3.11 - ("diff_sym_conv", (Context.theory_name @{theory}, prep_rls diff_sym_conv))] *}
3.12 + [("erls_diff", (Context.theory_name @{theory}, prep_rls' erls_diff)),
3.13 + ("diff_rules", (Context.theory_name @{theory}, prep_rls' diff_rules)),
3.14 + ("norm_diff", (Context.theory_name @{theory}, prep_rls' norm_diff)),
3.15 + ("diff_conv", (Context.theory_name @{theory}, prep_rls' diff_conv)),
3.16 + ("diff_sym_conv", (Context.theory_name @{theory}, prep_rls' diff_sym_conv))] *}
3.17
3.18 (** problem types **)
3.19 setup {* KEStore_Elems.add_pbts
4.1 --- a/src/Tools/isac/Knowledge/DiffApp.thy Fri Jun 13 09:55:49 2014 +0200
4.2 +++ b/src/Tools/isac/Knowledge/DiffApp.thy Fri Jun 13 10:29:06 2014 +0200
4.3 @@ -50,7 +50,7 @@
4.4 ML {*
4.5 val thy = @{theory};
4.6
4.7 -val eval_rls = prep_rls (
4.8 +val eval_rls = prep_rls' (
4.9 Rls {id = "eval_rls", preconds = [], rew_ord = ("termlessI", termlessI),
4.10 erls = e_rls, srls = Erls, calc = [], errpatts = [],
4.11 rules = [Thm ("refl", num_str @{thm refl}),
5.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Fri Jun 13 09:55:49 2014 +0200
5.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Fri Jun 13 10:29:06 2014 +0200
5.3 @@ -400,15 +400,15 @@
5.4
5.5 setup {* KEStore_Elems.add_rlss
5.6 [("simplify_System_parenthesized",
5.7 - (Context.theory_name @{theory}, prep_rls simplify_System_parenthesized)),
5.8 - ("simplify_System", (Context.theory_name @{theory}, prep_rls simplify_System)),
5.9 - ("isolate_bdvs", (Context.theory_name @{theory}, prep_rls isolate_bdvs)),
5.10 - ("isolate_bdvs_4x4", (Context.theory_name @{theory}, prep_rls isolate_bdvs_4x4)),
5.11 - ("order_system", (Context.theory_name @{theory}, prep_rls order_system)),
5.12 - ("order_add_mult_System", (Context.theory_name @{theory}, prep_rls order_add_mult_System)),
5.13 + (Context.theory_name @{theory}, prep_rls' simplify_System_parenthesized)),
5.14 + ("simplify_System", (Context.theory_name @{theory}, prep_rls' simplify_System)),
5.15 + ("isolate_bdvs", (Context.theory_name @{theory}, prep_rls' isolate_bdvs)),
5.16 + ("isolate_bdvs_4x4", (Context.theory_name @{theory}, prep_rls' isolate_bdvs_4x4)),
5.17 + ("order_system", (Context.theory_name @{theory}, prep_rls' order_system)),
5.18 + ("order_add_mult_System", (Context.theory_name @{theory}, prep_rls' order_add_mult_System)),
5.19 ("norm_System_noadd_fractions",
5.20 - (Context.theory_name @{theory}, prep_rls norm_System_noadd_fractions)),
5.21 - ("norm_System", (Context.theory_name @{theory}, prep_rls norm_System))] *}
5.22 + (Context.theory_name @{theory}, prep_rls' norm_System_noadd_fractions)),
5.23 + ("norm_System", (Context.theory_name @{theory}, prep_rls' norm_System))] *}
5.24
5.25 (** problems **)
5.26 setup {* KEStore_Elems.add_pbts
6.1 --- a/src/Tools/isac/Knowledge/Equation.thy Fri Jun 13 09:55:49 2014 +0200
6.2 +++ b/src/Tools/isac/Knowledge/Equation.thy Fri Jun 13 10:29:06 2014 +0200
6.3 @@ -46,7 +46,7 @@
6.4 [Calc ("Tools.matches",eval_matches "")];
6.5 *}
6.6 setup {* KEStore_Elems.add_rlss [("univariate_equation_prls",
6.7 - (Context.theory_name @{theory}, prep_rls univariate_equation_prls))] *}
6.8 + (Context.theory_name @{theory}, prep_rls @{theory} univariate_equation_prls))] *}
6.9 setup {* KEStore_Elems.add_pbts
6.10 [(prep_pbt thy "pbl_equ" [] e_pblID
6.11 (["equation"],
7.1 --- a/src/Tools/isac/Knowledge/Integrate.thy Fri Jun 13 09:55:49 2014 +0200
7.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy Fri Jun 13 10:29:06 2014 +0200
7.3 @@ -272,7 +272,7 @@
7.4 This is a copy from 'make_polynomial_in' with insertions from
7.5 'make_ratpoly_in'
7.6 THIS IS KEPT FOR COMPARISON ............................................
7.7 -* val simplify_Integral = prep_rls(
7.8 +* val simplify_Integral = prep_rls'(
7.9 * Seq {id = "", preconds = []:term list,
7.10 * rew_ord = ("dummy_ord", dummy_ord),
7.11 * erls = Atools_erls, srls = Erls,
7.12 @@ -321,18 +321,20 @@
7.13 Rls_ simplify_Integral
7.14 ],
7.15 scr = EmptyScr};
7.16 +
7.17 +val prep_rls' = prep_rls @{theory};
7.18 *}
7.19 setup {* KEStore_Elems.add_rlss
7.20 - [("integration_rules", (Context.theory_name @{theory}, prep_rls integration_rules)),
7.21 - ("add_new_c", (Context.theory_name @{theory}, prep_rls add_new_c)),
7.22 - ("simplify_Integral", (Context.theory_name @{theory}, prep_rls simplify_Integral)),
7.23 - ("integration", (Context.theory_name @{theory}, prep_rls integration)),
7.24 - ("separate_bdv2", (Context.theory_name @{theory}, prep_rls separate_bdv2)),
7.25 + [("integration_rules", (Context.theory_name @{theory}, prep_rls' integration_rules)),
7.26 + ("add_new_c", (Context.theory_name @{theory}, prep_rls' add_new_c)),
7.27 + ("simplify_Integral", (Context.theory_name @{theory}, prep_rls' simplify_Integral)),
7.28 + ("integration", (Context.theory_name @{theory}, prep_rls' integration)),
7.29 + ("separate_bdv2", (Context.theory_name @{theory}, prep_rls' separate_bdv2)),
7.30
7.31 ("norm_Rational_noadd_fractions", (Context.theory_name @{theory},
7.32 - prep_rls norm_Rational_noadd_fractions)),
7.33 + prep_rls' norm_Rational_noadd_fractions)),
7.34 ("norm_Rational_rls_noadd_fractions", (Context.theory_name @{theory},
7.35 - prep_rls norm_Rational_rls_noadd_fractions))] *}
7.36 + prep_rls' norm_Rational_rls_noadd_fractions))] *}
7.37
7.38 (** problems **)
7.39 setup {* KEStore_Elems.add_pbts
8.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Fri Jun 13 09:55:49 2014 +0200
8.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Fri Jun 13 10:29:06 2014 +0200
8.3 @@ -27,7 +27,7 @@
8.4
8.5
8.6 ML {*
8.7 -val inverse_z = prep_rls(
8.8 +val inverse_z = prep_rls'(
8.9 Rls {id = "inverse_z", preconds = [], rew_ord = ("dummy_ord",dummy_ord),
8.10 erls = Erls, srls = Erls, calc = [], errpatts = [],
8.11 rules =
9.1 --- a/src/Tools/isac/Knowledge/LinEq.thy Fri Jun 13 09:55:49 2014 +0200
9.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy Fri Jun 13 10:29:06 2014 +0200
9.3 @@ -75,7 +75,7 @@
9.4 [("LinEq_erls", (Context.theory_name @{theory}, LinEq_erls))] *}
9.5 ML {*
9.6
9.7 -val LinPoly_simplify = prep_rls(
9.8 +val LinPoly_simplify = prep_rls'(
9.9 Rls {id = "LinPoly_simplify", preconds = [],
9.10 rew_ord = ("termlessI",termlessI),
9.11 erls = LinEq_erls,
9.12 @@ -99,7 +99,7 @@
9.13 ML {*
9.14
9.15 (*isolate the bound variable in an linear equation; 'bdv' is a meta-constant*)
9.16 -val LinEq_simplify = prep_rls(
9.17 +val LinEq_simplify = prep_rls'(
9.18 Rls {id = "LinEq_simplify", preconds = [],
9.19 rew_ord = ("e_rew_ord",e_rew_ord),
9.20 erls = LinEq_erls,
10.1 --- a/src/Tools/isac/Knowledge/Partial_Fractions.thy Fri Jun 13 09:55:49 2014 +0200
10.2 +++ b/src/Tools/isac/Knowledge/Partial_Fractions.thy Fri Jun 13 10:29:06 2014 +0200
10.3 @@ -127,7 +127,7 @@
10.4 *}
10.5
10.6 ML {*
10.7 -val ansatz_rls = prep_rls(
10.8 +val ansatz_rls = prep_rls'(
10.9 Rls {id = "ansatz_rls", preconds = [], rew_ord = ("dummy_ord",dummy_ord),
10.10 erls = Erls, srls = Erls, calc = [], errpatts = [],
10.11 rules =
10.12 @@ -136,7 +136,7 @@
10.13 ],
10.14 scr = EmptyScr}:rls);
10.15
10.16 -val equival_trans = prep_rls(
10.17 +val equival_trans = prep_rls'(
10.18 Rls {id = "equival_trans", preconds = [], rew_ord = ("dummy_ord",dummy_ord),
10.19 erls = Erls, srls = Erls, calc = [], errpatts = [],
10.20 rules =
10.21 @@ -145,7 +145,7 @@
10.22 ],
10.23 scr = EmptyScr}:rls);
10.24
10.25 -val multiply_ansatz = prep_rls(
10.26 +val multiply_ansatz = prep_rls'(
10.27 Rls {id = "multiply_ansatz", preconds = [], rew_ord = ("dummy_ord",dummy_ord),
10.28 erls = Erls,
10.29 srls = Erls, calc = [], errpatts = [],
11.1 --- a/src/Tools/isac/Knowledge/Poly.thy Fri Jun 13 09:55:49 2014 +0200
11.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Fri Jun 13 10:29:06 2014 +0200
11.3 @@ -953,7 +953,7 @@
11.4 " t_t)";
11.5
11.6 (*version used by MG.02/03, overwritten by version AG in 04 below
11.7 -val make_polynomial = prep_rls(
11.8 +val make_polynomial = prep_rls'(
11.9 Seq{id = "make_polynomial", preconds = []:term list,
11.10 rew_ord = ("dummy_ord", dummy_ord),
11.11 erls = Atools_erls, srls = Erls,
11.12 @@ -1552,36 +1552,38 @@
11.13 scr = EmptyScr}:rls;
11.14 *}
11.15
11.16 +ML {* val prep_rls' = prep_rls @{theory} *}
11.17 +
11.18 setup {* KEStore_Elems.add_rlss
11.19 - [("norm_Poly", (Context.theory_name @{theory}, prep_rls norm_Poly)),
11.20 - ("Poly_erls", (Context.theory_name @{theory}, prep_rls Poly_erls)),(*FIXXXME:del with rls.rls'*)
11.21 - ("expand", (Context.theory_name @{theory}, prep_rls expand)),
11.22 - ("expand_poly", (Context.theory_name @{theory}, prep_rls expand_poly)),
11.23 - ("simplify_power", (Context.theory_name @{theory}, prep_rls simplify_power)),
11.24 + [("norm_Poly", (Context.theory_name @{theory}, prep_rls' norm_Poly)),
11.25 + ("Poly_erls", (Context.theory_name @{theory}, prep_rls' Poly_erls)),(*FIXXXME:del with rls.rls'*)
11.26 + ("expand", (Context.theory_name @{theory}, prep_rls' expand)),
11.27 + ("expand_poly", (Context.theory_name @{theory}, prep_rls' expand_poly)),
11.28 + ("simplify_power", (Context.theory_name @{theory}, prep_rls' simplify_power)),
11.29
11.30 - ("order_add_mult", (Context.theory_name @{theory}, prep_rls order_add_mult)),
11.31 - ("collect_numerals", (Context.theory_name @{theory}, prep_rls collect_numerals)),
11.32 - ("collect_numerals_", (Context.theory_name @{theory}, prep_rls collect_numerals_)),
11.33 - ("reduce_012", (Context.theory_name @{theory}, prep_rls reduce_012)),
11.34 - ("discard_parentheses", (Context.theory_name @{theory}, prep_rls discard_parentheses)),
11.35 + ("order_add_mult", (Context.theory_name @{theory}, prep_rls' order_add_mult)),
11.36 + ("collect_numerals", (Context.theory_name @{theory}, prep_rls' collect_numerals)),
11.37 + ("collect_numerals_", (Context.theory_name @{theory}, prep_rls' collect_numerals_)),
11.38 + ("reduce_012", (Context.theory_name @{theory}, prep_rls' reduce_012)),
11.39 + ("discard_parentheses", (Context.theory_name @{theory}, prep_rls' discard_parentheses)),
11.40
11.41 - ("make_polynomial", (Context.theory_name @{theory}, prep_rls make_polynomial)),
11.42 - ("expand_binoms", (Context.theory_name @{theory}, prep_rls expand_binoms)),
11.43 - ("rev_rew_p", (Context.theory_name @{theory}, prep_rls rev_rew_p)),
11.44 - ("discard_minus", (Context.theory_name @{theory}, prep_rls discard_minus)),
11.45 - ("expand_poly_", (Context.theory_name @{theory}, prep_rls expand_poly_)),
11.46 + ("make_polynomial", (Context.theory_name @{theory}, prep_rls' make_polynomial)),
11.47 + ("expand_binoms", (Context.theory_name @{theory}, prep_rls' expand_binoms)),
11.48 + ("rev_rew_p", (Context.theory_name @{theory}, prep_rls' rev_rew_p)),
11.49 + ("discard_minus", (Context.theory_name @{theory}, prep_rls' discard_minus)),
11.50 + ("expand_poly_", (Context.theory_name @{theory}, prep_rls' expand_poly_)),
11.51
11.52 - ("expand_poly_rat_", (Context.theory_name @{theory}, prep_rls expand_poly_rat_)),
11.53 - ("simplify_power_", (Context.theory_name @{theory}, prep_rls simplify_power_)),
11.54 - ("calc_add_mult_pow_", (Context.theory_name @{theory}, prep_rls calc_add_mult_pow_)),
11.55 - ("reduce_012_mult_", (Context.theory_name @{theory}, prep_rls reduce_012_mult_)),
11.56 - ("reduce_012_", (Context.theory_name @{theory}, prep_rls reduce_012_)),
11.57 + ("expand_poly_rat_", (Context.theory_name @{theory}, prep_rls' expand_poly_rat_)),
11.58 + ("simplify_power_", (Context.theory_name @{theory}, prep_rls' simplify_power_)),
11.59 + ("calc_add_mult_pow_", (Context.theory_name @{theory}, prep_rls' calc_add_mult_pow_)),
11.60 + ("reduce_012_mult_", (Context.theory_name @{theory}, prep_rls' reduce_012_mult_)),
11.61 + ("reduce_012_", (Context.theory_name @{theory}, prep_rls' reduce_012_)),
11.62
11.63 - ("discard_parentheses1", (Context.theory_name @{theory}, prep_rls discard_parentheses1)),
11.64 - ("order_mult_rls_", (Context.theory_name @{theory}, prep_rls order_mult_rls_)),
11.65 - ("order_add_rls_", (Context.theory_name @{theory}, prep_rls order_add_rls_)),
11.66 + ("discard_parentheses1", (Context.theory_name @{theory}, prep_rls' discard_parentheses1)),
11.67 + ("order_mult_rls_", (Context.theory_name @{theory}, prep_rls' order_mult_rls_)),
11.68 + ("order_add_rls_", (Context.theory_name @{theory}, prep_rls' order_add_rls_)),
11.69 ("make_rat_poly_with_parentheses",
11.70 - (Context.theory_name @{theory}, prep_rls make_rat_poly_with_parentheses))] *}
11.71 + (Context.theory_name @{theory}, prep_rls' make_rat_poly_with_parentheses))] *}
11.72 setup {* KEStore_Elems.add_calcs
11.73 [("is_polyrat_in", ("Poly.is'_polyrat'_in",
11.74 eval_is_polyrat_in "#eval_is_polyrat_in")),
12.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Fri Jun 13 09:55:49 2014 +0200
12.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Fri Jun 13 10:29:06 2014 +0200
12.3 @@ -432,7 +432,7 @@
12.4 Thm ("rat_leq3", num_str @{thm rat_leq3})
12.5 ]);
12.6
12.7 -val cancel_leading_coeff = prep_rls(
12.8 +val cancel_leading_coeff = prep_rls'(
12.9 Rls {id = "cancel_leading_coeff", preconds = [],
12.10 rew_ord = ("e_rew_ord",e_rew_ord),
12.11 erls = PolyEq_erls, srls = Erls, calc = [], errpatts = [],
12.12 @@ -451,9 +451,11 @@
12.13 Thm ("cancel_leading_coeff12",num_str @{thm cancel_leading_coeff12}),
12.14 Thm ("cancel_leading_coeff13",num_str @{thm cancel_leading_coeff13})
12.15 ],scr = Prog ((term_of o the o (parse thy)) "empty_script")}:rls);
12.16 +
12.17 +val prep_rls' = prep_rls @{theory};
12.18 *}
12.19 ML{*
12.20 -val complete_square = prep_rls(
12.21 +val complete_square = prep_rls'(
12.22 Rls {id = "complete_square", preconds = [],
12.23 rew_ord = ("e_rew_ord",e_rew_ord),
12.24 erls = PolyEq_erls, srls = Erls, calc = [], errpatts = [],
12.25 @@ -466,7 +468,7 @@
12.26 scr = Prog ((term_of o the o (parse thy)) "empty_script")
12.27 }:rls);
12.28
12.29 -val polyeq_simplify = prep_rls(
12.30 +val polyeq_simplify = prep_rls'(
12.31 Rls {id = "polyeq_simplify", preconds = [],
12.32 rew_ord = ("termlessI",termlessI),
12.33 erls = PolyEq_erls,
12.34 @@ -498,7 +500,7 @@
12.35 (* ------------- polySolve ------------------ *)
12.36 (* -- d0 -- *)
12.37 (*isolate the bound variable in an d0 equation; 'bdv' is a meta-constant*)
12.38 -val d0_polyeq_simplify = prep_rls(
12.39 +val d0_polyeq_simplify = prep_rls'(
12.40 Rls {id = "d0_polyeq_simplify", preconds = [],
12.41 rew_ord = ("e_rew_ord",e_rew_ord),
12.42 erls = PolyEq_erls,
12.43 @@ -512,7 +514,7 @@
12.44
12.45 (* -- d1 -- *)
12.46 (*isolate the bound variable in an d1 equation; 'bdv' is a meta-constant*)
12.47 -val d1_polyeq_simplify = prep_rls(
12.48 +val d1_polyeq_simplify = prep_rls'(
12.49 Rls {id = "d1_polyeq_simplify", preconds = [],
12.50 rew_ord = ("e_rew_ord",e_rew_ord),
12.51 erls = PolyEq_erls,
12.52 @@ -534,7 +536,7 @@
12.53 ML{*
12.54 (* isolate the bound variable in an d2 equation with bdv only;
12.55 "bdv" is a meta-constant substituted for the "x" below by isac's rewriter. *)
12.56 -val d2_polyeq_bdv_only_simplify = prep_rls(
12.57 +val d2_polyeq_bdv_only_simplify = prep_rls'(
12.58 Rls {id = "d2_polyeq_bdv_only_simplify", preconds = [], rew_ord = ("e_rew_ord",e_rew_ord),
12.59 erls = PolyEq_erls, srls = Erls, calc = [], errpatts = [],
12.60 rules =
12.61 @@ -555,7 +557,7 @@
12.62 ML{*
12.63 (* isolate the bound variable in an d2 equation with sqrt only;
12.64 'bdv' is a meta-constant*)
12.65 -val d2_polyeq_sq_only_simplify = prep_rls(
12.66 +val d2_polyeq_sq_only_simplify = prep_rls'(
12.67 Rls {id = "d2_polyeq_sq_only_simplify", preconds = [],
12.68 rew_ord = ("e_rew_ord",e_rew_ord),
12.69 erls = PolyEq_erls,
12.70 @@ -582,7 +584,7 @@
12.71 ML{*
12.72 (* isolate the bound variable in an d2 equation with pqFormula;
12.73 'bdv' is a meta-constant*)
12.74 -val d2_polyeq_pqFormula_simplify = prep_rls(
12.75 +val d2_polyeq_pqFormula_simplify = prep_rls'(
12.76 Rls {id = "d2_polyeq_pqFormula_simplify", preconds = [],
12.77 rew_ord = ("e_rew_ord",e_rew_ord), erls = PolyEq_erls,
12.78 srls = Erls, calc = [], errpatts = [],
12.79 @@ -628,7 +630,7 @@
12.80 ML{*
12.81 (* isolate the bound variable in an d2 equation with abcFormula;
12.82 'bdv' is a meta-constant*)
12.83 -val d2_polyeq_abcFormula_simplify = prep_rls(
12.84 +val d2_polyeq_abcFormula_simplify = prep_rls'(
12.85 Rls {id = "d2_polyeq_abcFormula_simplify", preconds = [],
12.86 rew_ord = ("e_rew_ord",e_rew_ord), erls = PolyEq_erls,
12.87 srls = Erls, calc = [], errpatts = [],
12.88 @@ -676,7 +678,7 @@
12.89
12.90 (* isolate the bound variable in an d2 equation;
12.91 'bdv' is a meta-constant*)
12.92 -val d2_polyeq_simplify = prep_rls(
12.93 +val d2_polyeq_simplify = prep_rls'(
12.94 Rls {id = "d2_polyeq_simplify", preconds = [],
12.95 rew_ord = ("e_rew_ord",e_rew_ord), erls = PolyEq_erls,
12.96 srls = Erls, calc = [], errpatts = [],
12.97 @@ -736,7 +738,7 @@
12.98
12.99 (* -- d3 -- *)
12.100 (* isolate the bound variable in an d3 equation; 'bdv' is a meta-constant *)
12.101 -val d3_polyeq_simplify = prep_rls(
12.102 +val d3_polyeq_simplify = prep_rls'(
12.103 Rls {id = "d3_polyeq_simplify", preconds = [],
12.104 rew_ord = ("e_rew_ord",e_rew_ord), erls = PolyEq_erls,
12.105 srls = Erls, calc = [], errpatts = [],
12.106 @@ -809,7 +811,7 @@
12.107
12.108 (* -- d4 -- *)
12.109 (*isolate the bound variable in an d4 equation; 'bdv' is a meta-constant*)
12.110 -val d4_polyeq_simplify = prep_rls(
12.111 +val d4_polyeq_simplify = prep_rls'(
12.112 Rls {id = "d4_polyeq_simplify", preconds = [],
12.113 rew_ord = ("e_rew_ord",e_rew_ord), erls = PolyEq_erls,
12.114 srls = Erls, calc = [], errpatts = [],
12.115 @@ -1237,7 +1239,7 @@
12.116
12.117 *}
12.118 ML{*
12.119 -val order_add_mult_in = prep_rls(
12.120 +val order_add_mult_in = prep_rls'(
12.121 Rls{id = "order_add_mult_in", preconds = [],
12.122 rew_ord = ("ord_make_polynomial_in",
12.123 ord_make_polynomial_in false @{theory "Poly"}),
12.124 @@ -1259,7 +1261,7 @@
12.125
12.126 *}
12.127 ML{*
12.128 -val collect_bdv = prep_rls(
12.129 +val collect_bdv = prep_rls'(
12.130 Rls{id = "collect_bdv", preconds = [],
12.131 rew_ord = ("dummy_ord", dummy_ord),
12.132 erls = e_rls,srls = Erls,
12.133 @@ -1294,7 +1296,7 @@
12.134 ML{*
12.135 (*.transforms an arbitrary term without roots to a polynomial [4]
12.136 according to knowledge/Poly.sml.*)
12.137 -val make_polynomial_in = prep_rls(
12.138 +val make_polynomial_in = prep_rls'(
12.139 Seq {id = "make_polynomial_in", preconds = []:term list,
12.140 rew_ord = ("dummy_ord", dummy_ord),
12.141 erls = Atools_erls, srls = Erls,
12.142 @@ -1330,7 +1332,7 @@
12.143 ];
12.144 *}
12.145 ML{*
12.146 -val make_ratpoly_in = prep_rls(
12.147 +val make_ratpoly_in = prep_rls'(
12.148 Seq {id = "make_ratpoly_in", preconds = []:term list,
12.149 rew_ord = ("dummy_ord", dummy_ord),
12.150 erls = Atools_erls, srls = Erls,
13.1 --- a/src/Tools/isac/Knowledge/PolyMinus.thy Fri Jun 13 09:55:49 2014 +0200
13.2 +++ b/src/Tools/isac/Knowledge/PolyMinus.thy Fri Jun 13 10:29:06 2014 +0200
13.3 @@ -387,13 +387,13 @@
13.4 ];
13.5 *}
13.6 setup {* KEStore_Elems.add_rlss
13.7 - [("ordne_alphabetisch", (Context.theory_name @{theory}, prep_rls ordne_alphabetisch)),
13.8 - ("fasse_zusammen", (Context.theory_name @{theory}, prep_rls fasse_zusammen)),
13.9 - ("verschoenere", (Context.theory_name @{theory}, prep_rls verschoenere)),
13.10 - ("ordne_monome", (Context.theory_name @{theory}, prep_rls ordne_monome)),
13.11 - ("klammern_aufloesen", (Context.theory_name @{theory}, prep_rls klammern_aufloesen)),
13.12 + [("ordne_alphabetisch", (Context.theory_name @{theory}, prep_rls' ordne_alphabetisch)),
13.13 + ("fasse_zusammen", (Context.theory_name @{theory}, prep_rls' fasse_zusammen)),
13.14 + ("verschoenere", (Context.theory_name @{theory}, prep_rls' verschoenere)),
13.15 + ("ordne_monome", (Context.theory_name @{theory}, prep_rls' ordne_monome)),
13.16 + ("klammern_aufloesen", (Context.theory_name @{theory}, prep_rls' klammern_aufloesen)),
13.17 ("klammern_ausmultiplizieren",
13.18 - (Context.theory_name @{theory}, prep_rls klammern_ausmultiplizieren))] *}
13.19 + (Context.theory_name @{theory}, prep_rls' klammern_ausmultiplizieren))] *}
13.20
13.21 (** problems **)
13.22 setup {* KEStore_Elems.add_pbts
14.1 --- a/src/Tools/isac/Knowledge/RatEq.thy Fri Jun 13 09:55:49 2014 +0200
14.2 +++ b/src/Tools/isac/Knowledge/RatEq.thy Fri Jun 13 10:29:06 2014 +0200
14.3 @@ -131,7 +131,7 @@
14.4 Thm ("or_commute",num_str @{thm or_commute}) (*WN: ein Hack*)
14.5 ];
14.6
14.7 -val RatEq_eliminate = prep_rls(
14.8 +val RatEq_eliminate = prep_rls'(
14.9 Rls {id = "RatEq_eliminate", preconds = [],
14.10 rew_ord = ("termlessI", termlessI), erls = rateq_erls, srls = Erls,
14.11 calc = [], errpatts = [],
14.12 @@ -150,7 +150,7 @@
14.13 (Context.theory_name @{theory}, RatEq_eliminate))] *}
14.14 ML {*
14.15
14.16 -val RatEq_simplify = prep_rls(
14.17 +val RatEq_simplify = prep_rls'(
14.18 Rls {id = "RatEq_simplify", preconds = [], rew_ord = ("termlessI", termlessI),
14.19 erls = rateq_erls, srls = Erls, calc = [], errpatts = [],
14.20 rules = [
15.1 --- a/src/Tools/isac/Knowledge/Rational.thy Fri Jun 13 09:55:49 2014 +0200
15.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Fri Jun 13 10:29:06 2014 +0200
15.3 @@ -393,7 +393,7 @@
15.4 ML {*
15.5 (* evaluates conditions in calculate_Rational *)
15.6 val calc_rat_erls =
15.7 - prep_rls
15.8 + prep_rls'
15.9 (Rls {id = "calc_rat_erls", preconds = [], rew_ord = ("dummy_ord", dummy_ord),
15.10 erls = e_rls, srls = Erls, calc = [], errpatts = [],
15.11 rules =
15.12 @@ -407,7 +407,7 @@
15.13 does NOT rearrange the term by AC-rewriting; thus terms with variables
15.14 need to have constants to be commuted together respectively *)
15.15 val calculate_Rational =
15.16 - prep_rls (merge_rls "calculate_Rational"
15.17 + prep_rls' (merge_rls "calculate_Rational"
15.18 (Rls {id = "divide", preconds = [], rew_ord = ("dummy_ord", dummy_ord),
15.19 erls = calc_rat_erls, srls = Erls,
15.20 calc = [], errpatts = [],
15.21 @@ -609,7 +609,7 @@
15.22 -------------------18.3.03 --> struct <-----------vvv--*)
15.23
15.24 (*erls for calculate_Rational; make local with FIXX@ME result:term *term list*)
15.25 -val powers_erls = prep_rls(
15.26 +val powers_erls = prep_rls'(
15.27 Rls {id = "powers_erls", preconds = [], rew_ord = ("dummy_ord",dummy_ord),
15.28 erls = e_rls, srls = Erls, calc = [], errpatts = [],
15.29 rules = [Calc ("Atools.is'_atom",eval_is_atom "#is_atom_"),
15.30 @@ -623,7 +623,7 @@
15.31 }:rls);
15.32 (*.all powers over + distributed; atoms over * collected, other distributed
15.33 contains absolute minimum of thms for context in norm_Rational .*)
15.34 -val powers = prep_rls(
15.35 +val powers = prep_rls'(
15.36 Rls {id = "powers", preconds = [], rew_ord = ("dummy_ord",dummy_ord),
15.37 erls = powers_erls, srls = Erls, calc = [], errpatts = [],
15.38 rules = [Thm ("realpow_multI", num_str @{thm realpow_multI}),
15.39 @@ -655,7 +655,7 @@
15.40 scr = EmptyScr
15.41 }:rls);
15.42 (*.contains absolute minimum of thms for context in norm_Rational.*)
15.43 -val rat_mult_divide = prep_rls(
15.44 +val rat_mult_divide = prep_rls'(
15.45 Rls {id = "rat_mult_divide", preconds = [],
15.46 rew_ord = ("dummy_ord", dummy_ord),
15.47 erls = e_rls, srls = Erls, calc = [], errpatts = [],
15.48 @@ -680,7 +680,7 @@
15.49 }:rls);
15.50
15.51 (*.contains absolute minimum of thms for context in norm_Rational.*)
15.52 -val reduce_0_1_2 = prep_rls(
15.53 +val reduce_0_1_2 = prep_rls'(
15.54 Rls{id = "reduce_0_1_2", preconds = [], rew_ord = ("dummy_ord", dummy_ord),
15.55 erls = e_rls, srls = Erls, calc = [], errpatts = [],
15.56 rules = [(*Thm ("divide_1",num_str @{thm divide_1}),
15.57 @@ -711,7 +711,7 @@
15.58
15.59 (*erls for calculate_Rational;
15.60 make local with FIXX@ME result:term *term list WN0609???SKMG*)
15.61 -val norm_rat_erls = prep_rls(
15.62 +val norm_rat_erls = prep_rls'(
15.63 Rls {id = "norm_rat_erls", preconds = [], rew_ord = ("dummy_ord",dummy_ord),
15.64 erls = e_rls, srls = Erls, calc = [], errpatts = [],
15.65 rules = [Calc ("Atools.is'_const",eval_const "#is_const_")
15.66 @@ -720,7 +720,7 @@
15.67 (* consists of rls containing the absolute minimum of thms *)
15.68 (*040209: this version has been used by RL for his equations,
15.69 which is now replaced by MGs version "norm_Rational" below *)
15.70 -val norm_Rational_min = prep_rls(
15.71 +val norm_Rational_min = prep_rls'(
15.72 Rls {id = "norm_Rational_min", preconds = [], rew_ord = ("dummy_ord",dummy_ord),
15.73 erls = norm_rat_erls, srls = Erls, calc = [], errpatts = [],
15.74 rules = [(*sequence given by operator precedence*)
15.75 @@ -736,7 +736,7 @@
15.76 ],
15.77 scr = EmptyScr}:rls);
15.78
15.79 -val norm_Rational_parenthesized = prep_rls(
15.80 +val norm_Rational_parenthesized = prep_rls'(
15.81 Seq {id = "norm_Rational_parenthesized", preconds = []:term list,
15.82 rew_ord = ("dummy_ord", dummy_ord),
15.83 erls = Atools_erls, srls = Erls,
15.84 @@ -768,14 +768,14 @@
15.85 ]);
15.86 *}
15.87 ML {*
15.88 -val add_fractions_p_rls = prep_rls(
15.89 +val add_fractions_p_rls = prep_rls'(
15.90 Rls {id = "add_fractions_p_rls", preconds = [], rew_ord = ("dummy_ord", dummy_ord),
15.91 erls = e_rls, srls = Erls, calc = [], errpatts = [],
15.92 rules = [Rls_ add_fractions_p],
15.93 scr = EmptyScr});
15.94
15.95 (* "Rls" causes repeated application of cancel_p to one and the same term *)
15.96 -val cancel_p_rls = prep_rls(
15.97 +val cancel_p_rls = prep_rls'(
15.98 Rls
15.99 {id = "cancel_p_rls", preconds = [], rew_ord = ("dummy_ord", dummy_ord),
15.100 erls = e_rls, srls = Erls, calc = [], errpatts = [],
15.101 @@ -784,7 +784,7 @@
15.102
15.103 (*. makes 'normal' fractions; 'is_polyexp' inhibits double fractions;
15.104 used in initial part norm_Rational_mg, see example DA-M02-main.p.60.*)
15.105 -val rat_mult_poly = prep_rls(
15.106 +val rat_mult_poly = prep_rls'(
15.107 Rls {id = "rat_mult_poly", preconds = [], rew_ord = ("dummy_ord", dummy_ord),
15.108 erls = append_rls "e_rls-is_polyexp" e_rls [Calc ("Poly.is'_polyexp", eval_is_polyexp "")],
15.109 srls = Erls, calc = [], errpatts = [],
15.110 @@ -800,7 +800,7 @@
15.111 .. WHERE THE LATTER DOES ALWAYS WORK, BECAUSE erls = e_rls,
15.112 I.E. THE RESPECTIVE ASSUMPTION IS STORED AND Thm APPLIED; WN051028
15.113 ... WN0609???MG.*)
15.114 -val rat_mult_div_pow = prep_rls(
15.115 +val rat_mult_div_pow = prep_rls'(
15.116 Rls {id = "rat_mult_div_pow", preconds = [], rew_ord = ("dummy_ord",dummy_ord),
15.117 erls = e_rls, srls = Erls, calc = [], errpatts = [],
15.118 rules = [Thm ("rat_mult", num_str @{thm rat_mult}),
15.119 @@ -823,7 +823,7 @@
15.120 ],
15.121 scr = EmptyScr}:rls);
15.122
15.123 -val rat_reduce_1 = prep_rls(
15.124 +val rat_reduce_1 = prep_rls'(
15.125 Rls {id = "rat_reduce_1", preconds = [], rew_ord = ("dummy_ord", dummy_ord),
15.126 erls = e_rls, srls = Erls, calc = [], errpatts = [],
15.127 rules =
15.128 @@ -835,7 +835,7 @@
15.129 scr = EmptyScr}:rls);
15.130
15.131 (* looping part of norm_Rational *)
15.132 -val norm_Rational_rls = prep_rls (
15.133 +val norm_Rational_rls = prep_rls' (
15.134 Rls {id = "norm_Rational_rls", preconds = [], rew_ord = ("dummy_ord",dummy_ord),
15.135 erls = norm_rat_erls, srls = Erls, calc = [], errpatts = [],
15.136 rules = [Rls_ add_fractions_p_rls,
15.137 @@ -846,7 +846,7 @@
15.138 ],
15.139 scr = EmptyScr}:rls);
15.140
15.141 -val norm_Rational = prep_rls (
15.142 +val norm_Rational = prep_rls' (
15.143 Seq
15.144 {id = "norm_Rational", preconds = [], rew_ord = ("dummy_ord", dummy_ord),
15.145 erls = norm_rat_erls, srls = Erls, calc = [], errpatts = [],
16.1 --- a/src/Tools/isac/Knowledge/Root.thy Fri Jun 13 09:55:49 2014 +0200
16.2 +++ b/src/Tools/isac/Knowledge/Root.thy Fri Jun 13 10:29:06 2014 +0200
16.3 @@ -188,7 +188,7 @@
16.4 setup {* KEStore_Elems.add_rlss [("Root_erls", (Context.theory_name @{theory}, Root_erls))] *}
16.5 ML {*
16.6
16.7 -val make_rooteq = prep_rls(
16.8 +val make_rooteq = prep_rls'(
16.9 Rls{id = "make_rooteq", preconds = []:term list,
16.10 rew_ord = ("sqrt_right", sqrt_right false thy),
16.11 erls = Atools_erls, srls = Erls,
16.12 @@ -256,7 +256,9 @@
16.13 setup {* KEStore_Elems.add_rlss [("make_rooteq", (Context.theory_name @{theory}, make_rooteq))] *}
16.14 ML {*
16.15
16.16 -val expand_rootbinoms = prep_rls(
16.17 +val prep_rls' = prep_rls @{theory};
16.18 +
16.19 +val expand_rootbinoms = prep_rls'(
16.20 Rls{id = "expand_rootbinoms", preconds = [],
16.21 rew_ord = ("termlessI",termlessI),
16.22 erls = Atools_erls, srls = Erls,
17.1 --- a/src/Tools/isac/Knowledge/RootEq.thy Fri Jun 13 09:55:49 2014 +0200
17.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy Fri Jun 13 10:29:06 2014 +0200
17.3 @@ -247,7 +247,7 @@
17.4 ML {*
17.5
17.6 (*isolate the bound variable in an sqrt equation; 'bdv' is a meta-constant*)
17.7 - val sqrt_isolate = prep_rls(
17.8 + val sqrt_isolate = prep_rls'(
17.9 Rls {id = "sqrt_isolate", preconds = [], rew_ord = ("termlessI",termlessI),
17.10 erls = RootEq_erls, srls = Erls, calc = [], errpatts = [],
17.11 rules = [
17.12 @@ -349,7 +349,7 @@
17.13 ML {*
17.14
17.15 (*isolate the bound variable in an sqrt left equation; 'bdv' is a meta-constant*)
17.16 - val l_sqrt_isolate = prep_rls(
17.17 + val l_sqrt_isolate = prep_rls'(
17.18 Rls {id = "l_sqrt_isolate", preconds = [],
17.19 rew_ord = ("termlessI",termlessI),
17.20 erls = RootEq_erls, srls = Erls, calc = [], errpatts = [],
17.21 @@ -398,7 +398,7 @@
17.22
17.23 (* -- right 28.8.02--*)
17.24 (*isolate the bound variable in an sqrt right equation; 'bdv' is a meta-constant*)
17.25 - val r_sqrt_isolate = prep_rls(
17.26 + val r_sqrt_isolate = prep_rls'(
17.27 Rls {id = "r_sqrt_isolate", preconds = [],
17.28 rew_ord = ("termlessI",termlessI),
17.29 erls = RootEq_erls, srls = Erls, calc = [], errpatts = [],
17.30 @@ -445,7 +445,7 @@
17.31 [("r_sqrt_isolate", (Context.theory_name @{theory}, r_sqrt_isolate))] *}
17.32 ML {*
17.33
17.34 -val rooteq_simplify = prep_rls(
17.35 +val rooteq_simplify = prep_rls'(
17.36 Rls {id = "rooteq_simplify",
17.37 preconds = [], rew_ord = ("termlessI",termlessI),
17.38 erls = RootEq_erls, srls = Erls, calc = [], errpatts = [],
18.1 --- a/src/Tools/isac/Knowledge/RootRat.thy Fri Jun 13 09:55:49 2014 +0200
18.2 +++ b/src/Tools/isac/Knowledge/RootRat.thy Fri Jun 13 10:29:06 2014 +0200
18.3 @@ -24,9 +24,11 @@
18.4 (* "- z1 = -1 * z1" *)
18.5 Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_")
18.6 ];
18.7 +
18.8 +val prep_rls' = prep_rls @{theory};
18.9 *}
18.10 setup {* KEStore_Elems.add_rlss
18.11 - [("rootrat_erls", (Context.theory_name @{theory}, prep_rls rootrat_erls)),
18.12 - ("calculate_RootRat", (Context.theory_name @{theory}, prep_rls calculate_RootRat))] *}
18.13 + [("rootrat_erls", (Context.theory_name @{theory}, prep_rls' rootrat_erls)),
18.14 + ("calculate_RootRat", (Context.theory_name @{theory}, prep_rls' calculate_RootRat))] *}
18.15
18.16 end
19.1 --- a/src/Tools/isac/Knowledge/RootRatEq.thy Fri Jun 13 09:55:49 2014 +0200
19.2 +++ b/src/Tools/isac/Knowledge/RootRatEq.thy Fri Jun 13 10:29:06 2014 +0200
19.3 @@ -113,7 +113,7 @@
19.4 [("RooRatEq_erls", (Context.theory_name @{theory}, RooRatEq_erls))] *}
19.5 ML {*
19.6 (* Solves a rootrat Equation *)
19.7 - val rootrat_solve = prep_rls(
19.8 + val rootrat_solve = prep_rls'(
19.9 Rls {id = "rootrat_solve", preconds = [],
19.10 rew_ord = ("termlessI",termlessI),
19.11 erls = e_rls, srls = Erls, calc = [], errpatts = [],
20.1 --- a/src/Tools/isac/Knowledge/Test.thy Fri Jun 13 09:55:49 2014 +0200
20.2 +++ b/src/Tools/isac/Knowledge/Test.thy Fri Jun 13 10:29:06 2014 +0200
20.3 @@ -295,7 +295,7 @@
20.4 scr = Prog ((term_of o the o (parse thy)) "empty_script")
20.5 }:rls;
20.6 *}
20.7 -setup {* KEStore_Elems.add_rlss [("testerls", (Context.theory_name @{theory}, prep_rls testerls))] *}
20.8 +setup {* KEStore_Elems.add_rlss [("testerls", (Context.theory_name @{theory}, prep_rls' testerls))] *}
20.9
20.10 ML {*
20.11 (*make () dissappear*)
20.12 @@ -388,7 +388,7 @@
20.13 Rls{id = "Test_simplify", preconds = [],
20.14 rew_ord = ("sqrt_right",sqrt_right false @{theory "Pure"}),
20.15 erls = tval_rls, srls = e_rls,
20.16 - calc=[(*since 040209 filled by prep_rls*)], errpatts = [],
20.17 + calc=[(*since 040209 filled by prep_rls'*)], errpatts = [],
20.18 rules = [
20.19 Thm ("real_diff_minus",num_str @{thm real_diff_minus}),
20.20 Thm ("radd_mult_distrib2",num_str @{thm radd_mult_distrib2}),
20.21 @@ -436,7 +436,7 @@
20.22 Thm ("radd_0_right",num_str @{thm radd_0_right})
20.23 ],
20.24 scr = Prog ((term_of o the o (parse thy)) "empty_script")
20.25 - (*since 040209 filled by prep_rls: STest_simplify*)
20.26 + (*since 040209 filled by prep_rls': STest_simplify*)
20.27 }:rls;
20.28 *}
20.29 ML {*
20.30 @@ -501,12 +501,13 @@
20.31 eval_contains_root"#contains_root_"))
20.32 ];
20.33 *}
20.34 +ML {* val prep_rls' = prep_rls @{theory}; *}
20.35 setup {* KEStore_Elems.add_rlss
20.36 - [("Test_simplify", (Context.theory_name @{theory}, prep_rls Test_simplify)),
20.37 - ("tval_rls", (Context.theory_name @{theory}, prep_rls tval_rls)),
20.38 - ("isolate_root", (Context.theory_name @{theory}, prep_rls isolate_root)),
20.39 - ("isolate_bdv", (Context.theory_name @{theory}, prep_rls isolate_bdv)),
20.40 - ("matches", (Context.theory_name @{theory}, prep_rls
20.41 + [("Test_simplify", (Context.theory_name @{theory}, prep_rls' Test_simplify)),
20.42 + ("tval_rls", (Context.theory_name @{theory}, prep_rls' tval_rls)),
20.43 + ("isolate_root", (Context.theory_name @{theory}, prep_rls' isolate_root)),
20.44 + ("isolate_bdv", (Context.theory_name @{theory}, prep_rls' isolate_bdv)),
20.45 + ("matches", (Context.theory_name @{theory}, prep_rls'
20.46 (append_rls "matches" testerls [Calc ("Tools.matches",eval_matches "#matches_")])))] *}
20.47
20.48 (** problem types **)
20.49 @@ -580,9 +581,9 @@
20.50 *}
20.51
20.52 setup {* KEStore_Elems.add_rlss
20.53 - [("norm_equation", (Context.theory_name @{theory}, prep_rls norm_equation)),
20.54 - ("ac_plus_times", (Context.theory_name @{theory}, prep_rls ac_plus_times)),
20.55 - ("rearrange_assoc", (Context.theory_name @{theory}, prep_rls rearrange_assoc))] *}
20.56 + [("norm_equation", (Context.theory_name @{theory}, prep_rls' norm_equation)),
20.57 + ("ac_plus_times", (Context.theory_name @{theory}, prep_rls' ac_plus_times)),
20.58 + ("rearrange_assoc", (Context.theory_name @{theory}, prep_rls' rearrange_assoc))] *}
20.59 ML {*
20.60
20.61
20.62 @@ -1117,7 +1118,7 @@
20.63 ("ord_make_polytest", ord_make_polytest false thy)
20.64 ]);
20.65
20.66 -(*WN060510 this was a preparation for prep_rls ...
20.67 +(*WN060510 this was a preparation for prep_rls' ...
20.68 val scr_make_polytest =
20.69 "Script Expand_binomtest t_t =" ^
20.70 "(Repeat " ^
20.71 @@ -1225,7 +1226,7 @@
20.72 }:rls;
20.73 *}
20.74 ML {*
20.75 -(*WN060510 this was done before 'fun prep_rls' ...------------------------
20.76 +(*WN060510 this was done before 'fun prep_rls ...------------------------
20.77 val scr_expand_binomtest =
20.78 "Script Expand_binomtest t_t =" ^
20.79 "(Repeat " ^
20.80 @@ -1358,7 +1359,7 @@
20.81 }:rls;
20.82 *}
20.83 setup {* KEStore_Elems.add_rlss
20.84 - [("make_polytest", (Context.theory_name @{theory}, prep_rls make_polytest)),
20.85 - ("expand_binomtest", (Context.theory_name @{theory}, prep_rls expand_binomtest))] *}
20.86 + [("make_polytest", (Context.theory_name @{theory}, prep_rls' make_polytest)),
20.87 + ("expand_binomtest", (Context.theory_name @{theory}, prep_rls' expand_binomtest))] *}
20.88
20.89 end
21.1 --- a/src/Tools/isac/Knowledge/Test_Build_Thydata.thy Fri Jun 13 09:55:49 2014 +0200
21.2 +++ b/src/Tools/isac/Knowledge/Test_Build_Thydata.thy Fri Jun 13 10:29:06 2014 +0200
21.3 @@ -24,11 +24,13 @@
21.4 rules = [Thm ("thm111", @{thm thm111}),
21.5 Thm ("refl", @{thm refl}), Thm ("o_def", @{thm o_def})],
21.6 scr = EmptyScr};
21.7 +
21.8 +val prep_rls' = prep_rls @{theory};
21.9 *}
21.10
21.11 setup {* KEStore_Elems.add_rlss
21.12 - [("rls111", (Context.theory_name @{theory}, prep_rls rls111)),
21.13 - ("rls222", (Context.theory_name @{theory}, prep_rls rls222))] *}
21.14 + [("rls111", (Context.theory_name @{theory}, prep_rls' rls111)),
21.15 + ("rls222", (Context.theory_name @{theory}, prep_rls' rls222))] *}
21.16
21.17 ML {*
21.18 @{thm refl};
22.1 --- a/src/Tools/isac/ProgLang/scrtools.sml Fri Jun 13 09:55:49 2014 +0200
22.2 +++ b/src/Tools/isac/ProgLang/scrtools.sml Fri Jun 13 10:29:06 2014 +0200
22.3 @@ -464,8 +464,8 @@
22.4 # generate a script for stepwise execution of the rls
22.5 # filter the operators for Calc out of the script ?WN111014?
22.6 !!!use this function while storing by or integrate into KEStore_Elems.add_rlss.*)
22.7 -fun prep_rls' _ Erls = error "prep_rls not impl. for Erls"
22.8 - | prep_rls' thy (Rls {id,preconds,rew_ord,erls,srls,calc,rules,errpatts,...}) =
22.9 +fun prep_rls _ Erls = error "prep_rls' not impl. for Erls"
22.10 + | prep_rls thy (Rls {id,preconds,rew_ord,erls,srls,calc,rules,errpatts,...}) =
22.11 let val sc = (rules2scr_Rls thy rules)
22.12 in Rls {id=id,preconds=preconds,rew_ord=rew_ord,erls=erls,
22.13 srls = srls,
22.14 @@ -475,7 +475,7 @@
22.15 rules = rules,
22.16 errpatts=errpatts,
22.17 scr = Prog sc} end
22.18 - | prep_rls' thy (Seq {id,preconds,rew_ord,erls,srls,calc,rules,errpatts,...}) =
22.19 + | prep_rls thy (Seq {id,preconds,rew_ord,erls,srls,calc,rules,errpatts,...}) =
22.20 let val sc = (rules2scr_Seq thy rules)
22.21 in Seq {id=id,preconds=preconds,rew_ord=rew_ord,erls=erls,
22.22 srls=srls,
22.23 @@ -484,8 +484,5 @@
22.24 rules=rules,
22.25 errpatts=errpatts,
22.26 scr = Prog sc} end
22.27 - | prep_rls' _ (Rrls {id,...}) =
22.28 - error ("prep_rls not required for Rrls \"" ^ id ^ "\"");
22.29 -
22.30 -fun prep_rls rls = prep_rls' (ML_Context.the_generic_context () |> Context.theory_of) rls;
22.31 -
22.32 + | prep_rls _ (Rrls {id,...}) =
22.33 + error ("prep_rls' not required for Rrls \"" ^ id ^ "\"");
23.1 --- a/src/Tools/isac/calcelems.sml Fri Jun 13 09:55:49 2014 +0200
23.2 +++ b/src/Tools/isac/calcelems.sml Fri Jun 13 10:29:06 2014 +0200
23.3 @@ -164,11 +164,11 @@
23.4 {id : string, (*for trace_rewrite:=true *)
23.5 preconds : term list, (*unused WN020820 *)
23.6 (*WN060616 for efficiency...
23.7 - bdvs : false, (*set in prep_rls for get_bdvs *)*)
23.8 + bdvs : false, (*set in prep_rls' for get_bdvs *)*)
23.9 rew_ord : rew_ord, (*for rules*)
23.10 erls : rls, (*for the conditions in rules *)
23.11 srls : rls, (*for evaluation of list_fns in script *)
23.12 - calc : calc list, (*for Calculate in scr, set by prep_rls *)
23.13 + calc : calc list, (*for Calculate in scr, set by prep_rls' *)
23.14 rules : rule list,
23.15 errpatts : errpatID list,(*dialog-authoring in Build_Thydata.thy*)
23.16 scr : scr} (*Prog term: generating intermed.steps *)
23.17 @@ -176,11 +176,11 @@
23.18 {id : string, (*for trace_rewrite:=true *)
23.19 preconds : term list, (*unused 20.8.02 *)
23.20 (*WN060616 for efficiency...
23.21 - bdvs : false, (*set in prep_rls for get_bdvs *)*)
23.22 + bdvs : false, (*set in prep_rls' for get_bdvs *)*)
23.23 rew_ord : rew_ord, (*for rules *)
23.24 erls : rls, (*for the conditions in rules *)
23.25 srls : rls, (*for evaluation of list_fns in script *)
23.26 - calc : calc list, (*for Calculate in scr, set by prep_rls *)
23.27 + calc : calc list, (*for Calculate in scr, set by prep_rls' *)
23.28 rules : rule list,
23.29 errpatts : errpatID list,(*dialog-authoring in Build_Thydata.thy*)
23.30 scr : scr} (*Prog term (how to restrict type ???)*)
23.31 @@ -199,7 +199,7 @@
23.32 list, (* meta-conjunction is or *)
23.33 rew_ord : rew_ord, (* for rules *)
23.34 erls : rls, (* for the conditions in rules and preconds *)
23.35 - calc : calc list, (* for Calculate in scr, set automatic.in prep_rls *)
23.36 + calc : calc list, (* for Calculate in scr, set automatic.in prep_rls' *)
23.37 errpatts : errpatID list,(*dialog-authoring in Build_Thydata.thy*)
23.38 scr : scr}; (* Rfuns {...} (how to restrict type ???) *)
23.39
24.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Fri Jun 13 09:55:49 2014 +0200
24.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Fri Jun 13 10:29:06 2014 +0200
24.3 @@ -699,7 +699,7 @@
24.4 drop\_questionmarks\normalfont.*}
24.5
24.6 ML {*
24.7 - val ansatz_rls = prep_rls(
24.8 + val ansatz_rls = prep_rls @{theory} (
24.9 Rls {id = "ansatz_rls", preconds = [], rew_ord = ("dummy_ord",dummy_ord),
24.10 erls = e_rls, srls = Erls, calc = [], errpatts = [],
24.11 rules = [
25.1 --- a/test/Tools/isac/Knowledge/partial_fractions.sml Fri Jun 13 09:55:49 2014 +0200
25.2 +++ b/test/Tools/isac/Knowledge/partial_fractions.sml Fri Jun 13 10:29:06 2014 +0200
25.3 @@ -330,7 +330,7 @@
25.4 val xxx = append_rls "multiply_ansatz_erls" norm_Rational
25.5 [Calc ("HOL.eq",eval_equal "#equal_")];
25.6
25.7 -val multiply_ansatz = prep_rls(
25.8 +val multiply_ansatz = prep_rls @{theory} (
25.9 Rls {id = "multiply_ansatz", preconds = [], rew_ord = ("dummy_ord",dummy_ord),
25.10 erls = xxx,
25.11 srls = Erls, calc = [], errpatts = [],