add functions accessing Theory_Data in parallel to those accessing "ruleset' = Unsynchronized.ref"
updates have been done incrementally following Build_Isac.thy:
# ./bin/isabelle jedit -l HOL src/Tools/isac/ProgLang/ProgLang.thy &
# ./bin/isabelle jedit -l HOL src/Tools/isac/Interpret/Interpret.thy &
# ./bin/isabelle jedit -l HOL src/Tools/isac/xmlsrc/xmlsrc.thy &
# ./bin/isabelle jedit -l HOL src/Tools/isac/Frontend/Frontend.thy &
Note, that the original access function "fun assoc_rls" is still outcommented;
so the old and new functionality is established in parallel.
1.1 --- a/src/Tools/isac/Interpret/rewtools.sml Sun Sep 22 17:28:55 2013 +0200
1.2 +++ b/src/Tools/isac/Interpret/rewtools.sml Sun Sep 22 18:09:05 2013 +0200
1.3 @@ -477,7 +477,7 @@
1.4 (*drop those rulesets which are generated in a theory found in #1#*)
1.5 val ancestors_rls =
1.6 filter_out ((curry ((op mem) o swap) dropthys') o ((#1 o #2): rls'*(theory' * rls)->theory'))
1.7 - (rev (!ruleset'))
1.8 + (rev (!ruleset' (*SWITCH KEStore_Elems.get_rlss (Thy_Info.get_theory thy')*)))
1.9 in case assoc (ancestors_rls, rls') of
1.10 SOME (thy', _) => ("IsacKnowledge", thyID2theory' thy')
1.11 | _ => error ("thy_containing_rls : rls '" ^ rls' ^
2.1 --- a/src/Tools/isac/KEStore.thy Sun Sep 22 17:28:55 2013 +0200
2.2 +++ b/src/Tools/isac/KEStore.thy Sun Sep 22 18:09:05 2013 +0200
2.3 @@ -56,7 +56,7 @@
2.4 *}
2.5 ML {*
2.6 (* in this phase of removing Unsynchornized.ref we do NOT overwrite the existing function!
2.7 -fun assoc_rls (rls' : rls') =
2.8 +fun assoc_rls (rls' : rls') = (*SWITCH outcommented*)
2.9 case AList.lookup (op =) (KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac")) rls' of
2.10 SOME (_, rls) => rls
2.11 | NONE => raise ERROR ("rls \""^ rls' ^ "\" missing in KEStore.\n" ^
2.12 @@ -72,5 +72,8 @@
2.13 [("e_rls", ("Tools", e_rls)),
2.14 ("e_rrls", ("Tools", e_rrls))]);
2.15 *}
2.16 +setup {* KEStore_Elems.add_rlss
2.17 + [("e_rls", (Context.theory_name @{theory}, e_rls)),
2.18 + ("e_rrls", (Context.theory_name @{theory}, e_rrls))] *}
2.19
2.20 end
3.1 --- a/src/Tools/isac/Knowledge/Atools.thy Sun Sep 22 17:28:55 2013 +0200
3.2 +++ b/src/Tools/isac/Knowledge/Atools.thy Sun Sep 22 18:09:05 2013 +0200
3.3 @@ -546,6 +546,9 @@
3.4 ruleset' := overwritelthy thy (!ruleset',
3.5 [("list_rls",list_rls)
3.6 ]);
3.7 +*}
3.8 +setup {* KEStore_Elems.add_rlss [("list_rls", (Context.theory_name @{theory}, list_rls))] *}
3.9 +ML {*
3.10
3.11 (*TODO.WN0509 reduce ids: tless_true = e_rew_ord' = e_rew_ord = dummy_ord*)
3.12 val tless_true = dummy_ord;
3.13 @@ -642,7 +645,7 @@
3.14 Calc ("Tools.matches",eval_matches "#matches")
3.15 ] (*i.A. zu viele rules*)
3.16 );*)
3.17 -(* val atools_erls = prep_rls(
3.18 +(* val atools_erls = prep_rls( (*outcommented*)
3.19 Rls {id="atools_erls",preconds = [], rew_ord = ("termlessI",termlessI),
3.20 erls = e_rls, srls = Erls, calc = [], errpatts = [],
3.21 rules = [Thm ("refl",num_str @{thm refl}),
3.22 @@ -667,7 +670,7 @@
3.23 ],
3.24 scr = Prog ((term_of o the o (parse @{theory})) "empty_script")
3.25 }:rls);
3.26 -ruleset' := overwritelth @{theory}
3.27 +ruleset' := overwritelth @{theory} (*outcommented*)
3.28 (!ruleset',
3.29 [("atools_erls",atools_erls)(*FIXXXME:del with rls.rls'*)
3.30 ]);
3.31 @@ -711,5 +714,6 @@
3.32 list_rls);
3.33 ruleset' := overwritelthy @{theory} (!ruleset', [("list_rls", list_rls)]);
3.34 *}
3.35 +setup {* KEStore_Elems.add_rlss [("list_rls", (Context.theory_name @{theory}, list_rls))] *}
3.36
3.37 end
4.1 --- a/src/Tools/isac/Knowledge/Build_Thydata.thy Sun Sep 22 17:28:55 2013 +0200
4.2 +++ b/src/Tools/isac/Knowledge/Build_Thydata.thy Sun Sep 22 18:09:05 2013 +0200
4.3 @@ -24,7 +24,7 @@
4.4 val progthys' = (*WN120321.TODO rearrange theories -------vvv*)
4.5 drop ((find_index (curry Theory.eq_thy first_Knowledge_thy) isacthys') + 1 +3, isacthys');
4.6
4.7 - val isacrlsthms = ! ruleset'
4.8 + val isacrlsthms = ! ruleset' (*SWITCH (KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac"))*)
4.9 |> map (thms_of_rls o #2 o #2)
4.10 |> flat
4.11 |> map thm_of_thm
5.1 --- a/src/Tools/isac/Knowledge/Diff.thy Sun Sep 22 17:28:55 2013 +0200
5.2 +++ b/src/Tools/isac/Knowledge/Diff.thy Sun Sep 22 18:09:05 2013 +0200
5.3 @@ -248,8 +248,12 @@
5.4 ("diff_conv", prep_rls diff_conv),
5.5 ("diff_sym_conv", prep_rls diff_sym_conv)
5.6 ]);
5.7 -
5.8 *}
5.9 +setup {* KEStore_Elems.add_rlss
5.10 + [("diff_rules", (Context.theory_name @{theory}, prep_rls diff_rules)),
5.11 + ("norm_diff", (Context.theory_name @{theory}, prep_rls norm_diff)),
5.12 + ("diff_conv", (Context.theory_name @{theory}, prep_rls diff_conv)),
5.13 + ("diff_sym_conv", (Context.theory_name @{theory}, prep_rls diff_sym_conv))] *}
5.14 ML {*
5.15 (** problem types **)
5.16
6.1 --- a/src/Tools/isac/Knowledge/DiffApp.thy Sun Sep 22 17:28:55 2013 +0200
6.2 +++ b/src/Tools/isac/Knowledge/DiffApp.thy Sun Sep 22 18:09:05 2013 +0200
6.3 @@ -80,6 +80,7 @@
6.4 [("eval_rls",Atools_erls)(*FIXXXME:del with rls.rls'*)
6.5 ]);
6.6 *}
6.7 +setup {* KEStore_Elems.add_rlss [("eval_rls", (Context.theory_name @{theory}, eval_rls))] *}
6.8 ML{*
6.9
6.10 (** problem types **)
6.11 @@ -262,5 +263,6 @@
6.12 [("list_rls",list_rls)
6.13 ]);
6.14 *}
6.15 +setup {* KEStore_Elems.add_rlss [("list_rls", (Context.theory_name @{theory}, list_rls))] *}
6.16
6.17 end
6.18 \ No newline at end of file
7.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Sun Sep 22 17:28:55 2013 +0200
7.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Sun Sep 22 18:09:05 2013 +0200
7.3 @@ -415,6 +415,17 @@
7.4 ("norm_System", prep_rls norm_System)
7.5 ]);
7.6 *}
7.7 +setup {* KEStore_Elems.add_rlss
7.8 + [("simplify_System_parenthesized",
7.9 + (Context.theory_name @{theory}, prep_rls simplify_System_parenthesized)),
7.10 + ("simplify_System", (Context.theory_name @{theory}, prep_rls simplify_System)),
7.11 + ("isolate_bdvs", (Context.theory_name @{theory}, prep_rls isolate_bdvs)),
7.12 + ("isolate_bdvs_4x4", (Context.theory_name @{theory}, prep_rls isolate_bdvs_4x4)),
7.13 + ("order_system", (Context.theory_name @{theory}, prep_rls order_system)),
7.14 + ("order_add_mult_System", (Context.theory_name @{theory}, prep_rls order_add_mult_System)),
7.15 + ("norm_System_noadd_fractions",
7.16 + (Context.theory_name @{theory}, prep_rls norm_System_noadd_fractions)),
7.17 + ("norm_System", (Context.theory_name @{theory}, prep_rls norm_System))] *}
7.18
7.19 ML {*
7.20 (** problems **)
8.1 --- a/src/Tools/isac/Knowledge/Equation.thy Sun Sep 22 17:28:55 2013 +0200
8.2 +++ b/src/Tools/isac/Knowledge/Equation.thy Sun Sep 22 18:09:05 2013 +0200
8.3 @@ -48,6 +48,10 @@
8.4 overwritelthy @{theory} (!ruleset',
8.5 [("univariate_equation_prls",
8.6 prep_rls univariate_equation_prls)]);
8.7 +*}
8.8 +setup {* KEStore_Elems.add_rlss [("univariate_equation_prls",
8.9 + (Context.theory_name @{theory}, prep_rls univariate_equation_prls))] *}
8.10 +ML {*
8.11
8.12
8.13 store_pbt
9.1 --- a/src/Tools/isac/Knowledge/InsSort.thy Sun Sep 22 17:28:55 2013 +0200
9.2 +++ b/src/Tools/isac/Knowledge/InsSort.thy Sun Sep 22 18:09:05 2013 +0200
9.3 @@ -102,5 +102,6 @@
9.4 [(*("ins_sort",ins_sort) overwrites a Isa fun!!*)
9.5 ]:(string * rls) list);
9.6 *}
9.7 +setup {* KEStore_Elems.add_rlss [("ins_sort", (Context.theory_name @{theory}, ins_sort))] *}
9.8
9.9 end
10.1 --- a/src/Tools/isac/Knowledge/Integrate.thy Sun Sep 22 17:28:55 2013 +0200
10.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy Sun Sep 22 18:09:05 2013 +0200
10.3 @@ -331,11 +331,23 @@
10.4 ("simplify_Integral", prep_rls simplify_Integral),
10.5 ("integration", prep_rls integration),
10.6 ("separate_bdv2", separate_bdv2),
10.7 +
10.8 ("norm_Rational_noadd_fractions", norm_Rational_noadd_fractions),
10.9 ("norm_Rational_rls_noadd_fractions",
10.10 norm_Rational_rls_noadd_fractions)
10.11 ]);
10.12 *}
10.13 +setup {* KEStore_Elems.add_rlss
10.14 + [("integration_rules", (Context.theory_name @{theory}, prep_rls integration_rules)),
10.15 + ("add_new_c", (Context.theory_name @{theory}, prep_rls add_new_c)),
10.16 + ("simplify_Integral", (Context.theory_name @{theory}, prep_rls simplify_Integral)),
10.17 + ("integration", (Context.theory_name @{theory}, prep_rls integration)),
10.18 + ("separate_bdv2", (Context.theory_name @{theory}, prep_rls separate_bdv2)),
10.19 +
10.20 + ("norm_Rational_noadd_fractions", (Context.theory_name @{theory},
10.21 + prep_rls norm_Rational_noadd_fractions)),
10.22 + ("norm_Rational_rls_noadd_fractions", (Context.theory_name @{theory},
10.23 + prep_rls norm_Rational_rls_noadd_fractions))] *}
10.24 ML {*
10.25
10.26 (** problems **)
11.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Sun Sep 22 17:28:55 2013 +0200
11.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Sun Sep 22 18:09:05 2013 +0200
11.3 @@ -45,6 +45,7 @@
11.4 [("inverse_z", inverse_z)
11.5 ]);
11.6 *}
11.7 +setup {* KEStore_Elems.add_rlss [("inverse_z", (Context.theory_name @{theory}, inverse_z))] *}
11.8
11.9 subsection{*Define the Specification*}
11.10 ML {*
12.1 --- a/src/Tools/isac/Knowledge/LinEq.thy Sun Sep 22 17:28:55 2013 +0200
12.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy Sun Sep 22 18:09:05 2013 +0200
12.3 @@ -74,6 +74,10 @@
12.4 ruleset' := overwritelthy @{theory} (!ruleset',
12.5 [("LinEq_erls",LinEq_erls)(*FIXXXME:del with rls.rls'*)
12.6 ]);
12.7 +*}
12.8 +setup {* KEStore_Elems.add_rlss
12.9 + [("LinEq_erls", (Context.theory_name @{theory}, LinEq_erls))] *}
12.10 +ML {*
12.11
12.12 val LinPoly_simplify = prep_rls(
12.13 Rls {id = "LinPoly_simplify", preconds = [],
12.14 @@ -96,6 +100,10 @@
12.15
12.16 ruleset' := overwritelthy @{theory} (!ruleset',
12.17 [("LinPoly_simplify",LinPoly_simplify)]);
12.18 +*}
12.19 +setup {* KEStore_Elems.add_rlss
12.20 + [("LinPoly_simplify", (Context.theory_name @{theory}, LinPoly_simplify))] *}
12.21 +ML {*
12.22
12.23 (*isolate the bound variable in an linear equation; 'bdv' is a meta-constant*)
12.24 val LinEq_simplify = prep_rls(
12.25 @@ -115,6 +123,10 @@
12.26 scr = EmptyScr}:rls);
12.27 ruleset' := overwritelthy @{theory} (!ruleset',
12.28 [("LinEq_simplify",LinEq_simplify)]);
12.29 +*}
12.30 +setup {* KEStore_Elems.add_rlss
12.31 + [("LinEq_simplify", (Context.theory_name @{theory}, LinEq_simplify))] *}
12.32 +ML {*
12.33
12.34 (*----------------------------- problem types --------------------------------*)
12.35 (*
13.1 --- a/src/Tools/isac/Knowledge/Partial_Fractions.thy Sun Sep 22 17:28:55 2013 +0200
13.2 +++ b/src/Tools/isac/Knowledge/Partial_Fractions.thy Sun Sep 22 18:09:05 2013 +0200
13.3 @@ -166,6 +166,10 @@
13.4 ("equival_trans", equival_trans)
13.5 ]);
13.6 *}
13.7 +setup {* KEStore_Elems.add_rlss
13.8 + [("ansatz_rls", (Context.theory_name @{theory}, ansatz_rls)),
13.9 + ("multiply_ansatz", (Context.theory_name @{theory}, multiply_ansatz)),
13.10 + ("equival_trans", (Context.theory_name @{theory}, equival_trans))] *}
13.11
13.12 subsection {* Specification *}
13.13
14.1 --- a/src/Tools/isac/Knowledge/Poly.thy Sun Sep 22 17:28:55 2013 +0200
14.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Sun Sep 22 18:09:05 2013 +0200
14.3 @@ -1563,27 +1563,61 @@
14.4 ("expand", prep_rls expand),
14.5 ("expand_poly", prep_rls expand_poly),
14.6 ("simplify_power", prep_rls simplify_power),
14.7 +
14.8 ("order_add_mult", prep_rls order_add_mult),
14.9 ("collect_numerals", prep_rls collect_numerals),
14.10 ("collect_numerals_", prep_rls collect_numerals_),
14.11 ("reduce_012", prep_rls reduce_012),
14.12 ("discard_parentheses", prep_rls discard_parentheses),
14.13 +
14.14 ("make_polynomial", prep_rls make_polynomial),
14.15 ("expand_binoms", prep_rls expand_binoms),
14.16 ("rev_rew_p", prep_rls rev_rew_p),
14.17 ("discard_minus", prep_rls discard_minus),
14.18 ("expand_poly_", prep_rls expand_poly_),
14.19 +
14.20 ("expand_poly_rat_", prep_rls expand_poly_rat_),
14.21 ("simplify_power_", prep_rls simplify_power_),
14.22 ("calc_add_mult_pow_", prep_rls calc_add_mult_pow_),
14.23 ("reduce_012_mult_", prep_rls reduce_012_mult_),
14.24 ("reduce_012_", prep_rls reduce_012_),
14.25 +
14.26 ("discard_parentheses1",prep_rls discard_parentheses1),
14.27 ("order_mult_rls_", prep_rls order_mult_rls_),
14.28 ("order_add_rls_", prep_rls order_add_rls_),
14.29 ("make_rat_poly_with_parentheses", prep_rls make_rat_poly_with_parentheses)
14.30 ]);
14.31 *}
14.32 +setup {* KEStore_Elems.add_rlss
14.33 + [("norm_Poly", (Context.theory_name @{theory}, prep_rls norm_Poly)),
14.34 + ("Poly_erls", (Context.theory_name @{theory}, prep_rls Poly_erls)),
14.35 + ("expand", (Context.theory_name @{theory}, prep_rls expand)),
14.36 + ("expand_poly", (Context.theory_name @{theory}, prep_rls expand_poly)),
14.37 + ("simplify_power", (Context.theory_name @{theory}, prep_rls simplify_power)),
14.38 +
14.39 + ("order_add_mult", (Context.theory_name @{theory}, prep_rls order_add_mult)),
14.40 + ("collect_numerals", (Context.theory_name @{theory}, prep_rls collect_numerals)),
14.41 + ("collect_numerals_", (Context.theory_name @{theory}, prep_rls collect_numerals_)),
14.42 + ("reduce_012", (Context.theory_name @{theory}, prep_rls reduce_012)),
14.43 + ("discard_parentheses", (Context.theory_name @{theory}, prep_rls discard_parentheses)),
14.44 +
14.45 + ("make_polynomial", (Context.theory_name @{theory}, prep_rls make_polynomial)),
14.46 + ("expand_binoms", (Context.theory_name @{theory}, prep_rls expand_binoms)),
14.47 + ("rev_rew_p", (Context.theory_name @{theory}, prep_rls rev_rew_p)),
14.48 + ("discard_minus", (Context.theory_name @{theory}, prep_rls discard_minus)),
14.49 + ("expand_poly_", (Context.theory_name @{theory}, prep_rls expand_poly_)),
14.50 +
14.51 + ("expand_poly_rat_", (Context.theory_name @{theory}, prep_rls expand_poly_rat_)),
14.52 + ("simplify_power_", (Context.theory_name @{theory}, prep_rls simplify_power_)),
14.53 + ("calc_add_mult_pow_", (Context.theory_name @{theory}, prep_rls calc_add_mult_pow_)),
14.54 + ("reduce_012_mult_", (Context.theory_name @{theory}, prep_rls reduce_012_mult_)),
14.55 + ("reduce_012_", (Context.theory_name @{theory}, prep_rls reduce_012_)),
14.56 +
14.57 + ("discard_parentheses1", (Context.theory_name @{theory}, prep_rls discard_parentheses1)),
14.58 + ("order_mult_rls_", (Context.theory_name @{theory}, prep_rls order_mult_rls_)),
14.59 + ("order_add_rls_", (Context.theory_name @{theory}, prep_rls order_add_rls_)),
14.60 + ("make_rat_poly_with_parentheses",
14.61 + (Context.theory_name @{theory}, prep_rls make_rat_poly_with_parentheses))] *}
14.62 ML {*
14.63 calclist':= overwritel (!calclist',
14.64 [("is_polyrat_in", ("Poly.is'_polyrat'_in",
15.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Sun Sep 22 17:28:55 2013 +0200
15.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Sun Sep 22 18:09:05 2013 +0200
15.3 @@ -492,8 +492,12 @@
15.4 ("complete_square",complete_square),
15.5 ("PolyEq_erls",PolyEq_erls),(*FIXXXME:del with rls.rls'*)
15.6 ("polyeq_simplify",polyeq_simplify)]);
15.7 -
15.8 *}
15.9 +setup {* KEStore_Elems.add_rlss
15.10 + [("cancel_leading_coeff", (Context.theory_name @{theory}, cancel_leading_coeff)),
15.11 + ("complete_square", (Context.theory_name @{theory}, complete_square)),
15.12 + ("PolyEq_erls", (Context.theory_name @{theory}, PolyEq_erls)),
15.13 + ("polyeq_simplify", (Context.theory_name @{theory}, polyeq_simplify))] *}
15.14 ML{*
15.15
15.16 (* ------------- polySolve ------------------ *)
15.17 @@ -829,13 +833,26 @@
15.18 ("d2_polyeq_simplify", d2_polyeq_simplify),
15.19 ("d2_polyeq_bdv_only_simplify", d2_polyeq_bdv_only_simplify),
15.20 ("d2_polyeq_sq_only_simplify", d2_polyeq_sq_only_simplify),
15.21 +
15.22 ("d2_polyeq_pqFormula_simplify", d2_polyeq_pqFormula_simplify),
15.23 - ("d2_polyeq_abcFormula_simplify",
15.24 - d2_polyeq_abcFormula_simplify),
15.25 + ("d2_polyeq_abcFormula_simplify", d2_polyeq_abcFormula_simplify),
15.26 ("d3_polyeq_simplify", d3_polyeq_simplify),
15.27 ("d4_polyeq_simplify", d4_polyeq_simplify)
15.28 ]);
15.29 *}
15.30 +setup {* KEStore_Elems.add_rlss
15.31 + [("d0_polyeq_simplify", (Context.theory_name @{theory}, d0_polyeq_simplify)),
15.32 + ("d1_polyeq_simplify", (Context.theory_name @{theory}, d1_polyeq_simplify)),
15.33 + ("d2_polyeq_simplify", (Context.theory_name @{theory}, d2_polyeq_simplify)),
15.34 + ("d2_polyeq_bdv_only_simplify", (Context.theory_name @{theory}, d2_polyeq_bdv_only_simplify)),
15.35 + ("d2_polyeq_sq_only_simplify", (Context.theory_name @{theory}, d2_polyeq_sq_only_simplify)),
15.36 +
15.37 + ("d2_polyeq_pqFormula_simplify",
15.38 + (Context.theory_name @{theory}, d2_polyeq_pqFormula_simplify)),
15.39 + ("d2_polyeq_abcFormula_simplify",
15.40 + (Context.theory_name @{theory}, d2_polyeq_abcFormula_simplify)),
15.41 + ("d3_polyeq_simplify", (Context.theory_name @{theory}, d3_polyeq_simplify)),
15.42 + ("d4_polyeq_simplify", (Context.theory_name @{theory}, d4_polyeq_simplify))] *}
15.43 ML{*
15.44
15.45 (*------------------------problems------------------------*)
16.1 --- a/src/Tools/isac/Knowledge/PolyMinus.thy Sun Sep 22 17:28:55 2013 +0200
16.2 +++ b/src/Tools/isac/Knowledge/PolyMinus.thy Sun Sep 22 18:09:05 2013 +0200
16.3 @@ -396,6 +396,16 @@
16.4 ("klammern_ausmultiplizieren",
16.5 prep_rls klammern_ausmultiplizieren)
16.6 ]);
16.7 +*}
16.8 +setup {* KEStore_Elems.add_rlss
16.9 + [("ordne_alphabetisch", (Context.theory_name @{theory}, prep_rls ordne_alphabetisch)),
16.10 + ("fasse_zusammen", (Context.theory_name @{theory}, prep_rls fasse_zusammen)),
16.11 + ("verschoenere", (Context.theory_name @{theory}, prep_rls verschoenere)),
16.12 + ("ordne_monome", (Context.theory_name @{theory}, prep_rls ordne_monome)),
16.13 + ("klammern_aufloesen", (Context.theory_name @{theory}, prep_rls klammern_aufloesen)),
16.14 + ("klammern_ausmultiplizieren",
16.15 + (Context.theory_name @{theory}, prep_rls klammern_ausmultiplizieren))] *}
16.16 +ML {*
16.17
16.18 (** problems **)
16.19
17.1 --- a/src/Tools/isac/Knowledge/RatEq.thy Sun Sep 22 17:28:55 2013 +0200
17.2 +++ b/src/Tools/isac/Knowledge/RatEq.thy Sun Sep 22 18:09:05 2013 +0200
17.3 @@ -117,7 +117,9 @@
17.4 ruleset' := overwritelthy @{theory} (!ruleset',
17.5 [("rateq_erls",rateq_erls)(*FIXXXME:del with rls.rls'*)
17.6 ]);
17.7 -
17.8 +*}
17.9 +setup {* KEStore_Elems.add_rlss [("rateq_erls", (Context.theory_name @{theory}, rateq_erls))] *}
17.10 +ML {*
17.11
17.12 val RatEq_crls =
17.13 remove_rls "RatEq_crls" (*WN: ein Hack*)
17.14 @@ -149,6 +151,10 @@
17.15 ruleset' := overwritelthy @{theory} (!ruleset',
17.16 [("RatEq_eliminate",RatEq_eliminate)
17.17 ]);
17.18 +*}
17.19 +setup {* KEStore_Elems.add_rlss [("RatEq_eliminate",
17.20 + (Context.theory_name @{theory}, RatEq_eliminate))] *}
17.21 +ML {*
17.22
17.23 val RatEq_simplify = prep_rls(
17.24 Rls {id = "RatEq_simplify", preconds = [], rew_ord = ("termlessI", termlessI),
17.25 @@ -176,6 +182,10 @@
17.26 ruleset' := overwritelthy @{theory} (!ruleset',
17.27 [("RatEq_simplify",RatEq_simplify)
17.28 ]);
17.29 +*}
17.30 +setup {* KEStore_Elems.add_rlss [("RatEq_simplify",
17.31 + (Context.theory_name @{theory}, RatEq_simplify))] *}
17.32 +ML {*
17.33
17.34 (*-------------------------Problem-----------------------*)
17.35 (*
18.1 --- a/src/Tools/isac/Knowledge/Rational.thy Sun Sep 22 17:28:55 2013 +0200
18.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Sun Sep 22 18:09:05 2013 +0200
18.3 @@ -866,23 +866,47 @@
18.4 ("rational_erls", rational_erls),
18.5 ("cancel_p", cancel_p),
18.6 ("add_fractions_p", add_fractions_p),
18.7 +
18.8 ("add_fractions_p_rls", add_fractions_p_rls),
18.9 (*WN120410 ("discard_minus", discard_minus), is defined in Poly.thy*)
18.10 ("powers_erls", powers_erls),
18.11 ("powers", powers),
18.12 ("rat_mult_divide", rat_mult_divide),
18.13 ("reduce_0_1_2", reduce_0_1_2),
18.14 +
18.15 ("rat_reduce_1", rat_reduce_1),
18.16 ("norm_rat_erls", norm_rat_erls),
18.17 ("norm_Rational", norm_Rational),
18.18 ("norm_Rational_rls", norm_Rational_rls),
18.19 ("norm_Rational_parenthesized", norm_Rational_parenthesized),
18.20 +
18.21 ("rat_mult_poly", rat_mult_poly),
18.22 ("rat_mult_div_pow", rat_mult_div_pow),
18.23 ("cancel_p_rls", cancel_p_rls)
18.24 ]);
18.25 -
18.26 *}
18.27 +setup {* KEStore_Elems.add_rlss
18.28 + [("calculate_Rational", (Context.theory_name @{theory}, calculate_Rational)),
18.29 + ("calc_rat_erls", (Context.theory_name @{theory}, calc_rat_erls)),
18.30 + ("rational_erls", (Context.theory_name @{theory}, rational_erls)),
18.31 + ("cancel_p", (Context.theory_name @{theory}, cancel_p)),
18.32 + ("add_fractions_p", (Context.theory_name @{theory}, add_fractions_p)),
18.33 +
18.34 + ("add_fractions_p_rls", (Context.theory_name @{theory}, add_fractions_p_rls)),
18.35 + ("powers_erls", (Context.theory_name @{theory}, powers_erls)),
18.36 + ("powers", (Context.theory_name @{theory}, powers)),
18.37 + ("rat_mult_divide", (Context.theory_name @{theory}, rat_mult_divide)),
18.38 + ("reduce_0_1_2", (Context.theory_name @{theory}, reduce_0_1_2)),
18.39 +
18.40 + ("rat_reduce_1", (Context.theory_name @{theory}, rat_reduce_1)),
18.41 + ("norm_rat_erls", (Context.theory_name @{theory}, norm_rat_erls)),
18.42 + ("norm_Rational", (Context.theory_name @{theory}, norm_Rational)),
18.43 + ("norm_Rational_rls", (Context.theory_name @{theory}, norm_Rational_rls)),
18.44 + ("norm_Rational_parenthesized", (Context.theory_name @{theory}, norm_Rational_parenthesized)),
18.45 +
18.46 + ("rat_mult_poly", (Context.theory_name @{theory}, rat_mult_poly)),
18.47 + ("rat_mult_div_pow", (Context.theory_name @{theory}, rat_mult_div_pow)),
18.48 + ("cancel_p_rls", (Context.theory_name @{theory}, cancel_p_rls))] *}
18.49
18.50 section {* A problem for simplification of rationals *}
18.51 ML {*
19.1 --- a/src/Tools/isac/Knowledge/Root.thy Sun Sep 22 17:28:55 2013 +0200
19.2 +++ b/src/Tools/isac/Knowledge/Root.thy Sun Sep 22 18:09:05 2013 +0200
19.3 @@ -190,6 +190,9 @@
19.4 ruleset' := overwritelthy @{theory} (!ruleset',
19.5 [("Root_erls",Root_erls) (*FIXXXME:del with rls.rls'*)
19.6 ]);
19.7 +*}
19.8 +setup {* KEStore_Elems.add_rlss [("Root_erls", (Context.theory_name @{theory}, Root_erls))] *}
19.9 +ML {*
19.10
19.11 val make_rooteq = prep_rls(
19.12 Rls{id = "make_rooteq", preconds = []:term list,
19.13 @@ -258,6 +261,9 @@
19.14 ruleset' := overwritelthy @{theory} (!ruleset',
19.15 [("make_rooteq", make_rooteq)
19.16 ]);
19.17 +*}
19.18 +setup {* KEStore_Elems.add_rlss [("make_rooteq", (Context.theory_name @{theory}, make_rooteq))] *}
19.19 +ML {*
19.20
19.21 val expand_rootbinoms = prep_rls(
19.22 Rls{id = "expand_rootbinoms", preconds = [],
19.23 @@ -333,5 +339,8 @@
19.24 [("expand_rootbinoms", expand_rootbinoms)
19.25 ]);
19.26 *}
19.27 +setup {* KEStore_Elems.add_rlss
19.28 + [("expand_rootbinoms", (Context.theory_name @{theory}, expand_rootbinoms))] *}
19.29 +
19.30
19.31 end
20.1 --- a/src/Tools/isac/Knowledge/RootEq.thy Sun Sep 22 17:28:55 2013 +0200
20.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy Sun Sep 22 18:09:05 2013 +0200
20.3 @@ -246,6 +246,11 @@
20.4 (*FIXXXME:del with rls.rls'*)
20.5 ("rooteq_srls",rooteq_srls)
20.6 ]);
20.7 +*}
20.8 +setup {* KEStore_Elems.add_rlss
20.9 + [("RootEq_erls", (Context.theory_name @{theory}, RootEq_erls)),
20.10 + ("rooteq_srls", (Context.theory_name @{theory}, rooteq_srls))] *}
20.11 +ML {*
20.12
20.13 (*isolate the bound variable in an sqrt equation; 'bdv' is a meta-constant*)
20.14 val sqrt_isolate = prep_rls(
20.15 @@ -348,7 +353,11 @@
20.16 ruleset' := overwritelthy @{theory} (!ruleset',
20.17 [("sqrt_isolate",sqrt_isolate)
20.18 ]);
20.19 -(* -- left 28.08.02--*)
20.20 +*}
20.21 +setup {* KEStore_Elems.add_rlss
20.22 + [("sqrt_isolate", (Context.theory_name @{theory}, sqrt_isolate))] *}
20.23 +ML {*
20.24 +
20.25 (*isolate the bound variable in an sqrt left equation; 'bdv' is a meta-constant*)
20.26 val l_sqrt_isolate = prep_rls(
20.27 Rls {id = "l_sqrt_isolate", preconds = [],
20.28 @@ -396,6 +405,10 @@
20.29 ruleset' := overwritelthy @{theory} (!ruleset',
20.30 [("l_sqrt_isolate",l_sqrt_isolate)
20.31 ]);
20.32 +*}
20.33 +setup {* KEStore_Elems.add_rlss
20.34 + [("l_sqrt_isolate", (Context.theory_name @{theory}, l_sqrt_isolate))] *}
20.35 +ML {*
20.36
20.37 (* -- right 28.8.02--*)
20.38 (*isolate the bound variable in an sqrt right equation; 'bdv' is a meta-constant*)
20.39 @@ -445,6 +458,10 @@
20.40 ruleset' := overwritelthy @{theory} (!ruleset',
20.41 [("r_sqrt_isolate",r_sqrt_isolate)
20.42 ]);
20.43 +*}
20.44 +setup {* KEStore_Elems.add_rlss
20.45 + [("r_sqrt_isolate", (Context.theory_name @{theory}, r_sqrt_isolate))] *}
20.46 +ML {*
20.47
20.48 val rooteq_simplify = prep_rls(
20.49 Rls {id = "rooteq_simplify",
20.50 @@ -479,6 +496,10 @@
20.51 ruleset' := overwritelthy @{theory} (!ruleset',
20.52 [("rooteq_simplify",rooteq_simplify)
20.53 ]);
20.54 +*}
20.55 +setup {* KEStore_Elems.add_rlss
20.56 + [("rooteq_simplify", (Context.theory_name @{theory}, rooteq_simplify))] *}
20.57 +ML {*
20.58
20.59 (*-------------------------Problem-----------------------*)
20.60 (*
21.1 --- a/src/Tools/isac/Knowledge/RootRat.thy Sun Sep 22 17:28:55 2013 +0200
21.2 +++ b/src/Tools/isac/Knowledge/RootRat.thy Sun Sep 22 18:09:05 2013 +0200
21.3 @@ -30,5 +30,8 @@
21.4 ("calculate_RootRat", prep_rls calculate_RootRat)
21.5 ]);
21.6 *}
21.7 +setup {* KEStore_Elems.add_rlss
21.8 + [("rootrat_erls", (Context.theory_name @{theory}, prep_rls rootrat_erls)),
21.9 + ("calculate_RootRat", (Context.theory_name @{theory}, prep_rls calculate_RootRat))] *}
21.10
21.11 end
22.1 --- a/src/Tools/isac/Knowledge/RootRatEq.thy Sun Sep 22 17:28:55 2013 +0200
22.2 +++ b/src/Tools/isac/Knowledge/RootRatEq.thy Sun Sep 22 18:09:05 2013 +0200
22.3 @@ -111,8 +111,9 @@
22.4
22.5 ruleset' := overwritelthy @{theory} (!ruleset',
22.6 [("RooRatEq_erls",RooRatEq_erls) (*FIXXXME:del with rls.rls'*)]);
22.7 -
22.8 *}
22.9 +setup {* KEStore_Elems.add_rlss
22.10 + [("RooRatEq_erls", (Context.theory_name @{theory}, RooRatEq_erls))] *}
22.11 ML {*
22.12 (* Solves a rootrat Equation *)
22.13 val rootrat_solve = prep_rls(
22.14 @@ -136,6 +137,8 @@
22.15 [("rootrat_solve",rootrat_solve)
22.16 ]);
22.17 *}
22.18 +setup {* KEStore_Elems.add_rlss
22.19 + [("rootrat_solve", (Context.theory_name @{theory}, rootrat_solve))] *}
22.20 ML {*
22.21
22.22 (*-----------------------probleme------------------------*)
23.1 --- a/src/Tools/isac/Knowledge/Test.thy Sun Sep 22 17:28:55 2013 +0200
23.2 +++ b/src/Tools/isac/Knowledge/Test.thy Sun Sep 22 18:09:05 2013 +0200
23.3 @@ -305,6 +305,9 @@
23.4 ruleset' := overwritelthy @{theory} (!ruleset',
23.5 [("testerls", prep_rls testerls)
23.6 ]);
23.7 +*}
23.8 +setup {* KEStore_Elems.add_rlss [("testerls", (Context.theory_name @{theory}, prep_rls testerls))] *}
23.9 +ML {*
23.10
23.11
23.12 (*make () dissappear*)
23.13 @@ -519,8 +522,15 @@
23.14 prep_rls (append_rls "matches" testerls
23.15 [Calc ("Tools.matches",eval_matches "#matches_")]))
23.16 ]);
23.17 +*}
23.18 +setup {* KEStore_Elems.add_rlss
23.19 + [("Test_simplify", (Context.theory_name @{theory}, prep_rls Test_simplify)),
23.20 + ("tval_rls", (Context.theory_name @{theory}, prep_rls tval_rls)),
23.21 + ("isolate_root", (Context.theory_name @{theory}, prep_rls isolate_root)),
23.22 + ("isolate_bdv", (Context.theory_name @{theory}, prep_rls isolate_bdv)),
23.23 + ("matches", (Context.theory_name @{theory}, prep_rls
23.24 + (append_rls "matches" testerls [Calc ("Tools.matches",eval_matches "#matches_")])))] *}
23.25
23.26 -*}
23.27 ML {*
23.28 (** problem types **)
23.29 store_pbt
23.30 @@ -633,6 +643,12 @@
23.31 ("ac_plus_times", prep_rls ac_plus_times),
23.32 ("rearrange_assoc", prep_rls rearrange_assoc)
23.33 ]);
23.34 +*}
23.35 +setup {* KEStore_Elems.add_rlss
23.36 + [("norm_equation", (Context.theory_name @{theory}, prep_rls norm_equation)),
23.37 + ("ac_plus_times", (Context.theory_name @{theory}, prep_rls ac_plus_times)),
23.38 + ("rearrange_assoc", (Context.theory_name @{theory}, prep_rls rearrange_assoc))] *}
23.39 +ML {*
23.40
23.41
23.42 fun bin_o (Const (op_,(Type ("fun",
23.43 @@ -1524,5 +1540,8 @@
23.44 ("expand_binomtest", prep_rls expand_binomtest)
23.45 ]);
23.46 *}
23.47 +setup {* KEStore_Elems.add_rlss
23.48 + [("make_polytest", (Context.theory_name @{theory}, prep_rls make_polytest)),
23.49 + ("expand_binomtest", (Context.theory_name @{theory}, prep_rls expand_binomtest))] *}
23.50
23.51 end
24.1 --- a/src/Tools/isac/ProgLang/Tools.thy Sun Sep 22 17:28:55 2013 +0200
24.2 +++ b/src/Tools/isac/ProgLang/Tools.thy Sun Sep 22 18:09:05 2013 +0200
24.3 @@ -223,6 +223,9 @@
24.4 ruleset' := overwritelthy @{theory} (!ruleset',
24.5 [("list_rls",list_rls)
24.6 ]);
24.7 +*}
24.8 +setup {* KEStore_Elems.add_rlss [("list_rls", (Context.theory_name @{theory}, list_rls))] *}
24.9 +ML {*
24.10 calclist':= overwritel (!calclist',
24.11 [("matches",("Tools.matches",eval_matches "#matches_")),
24.12 ("matchsub",("Tools.matchsub",eval_matchsub "#matchsub_")),
25.1 --- a/src/Tools/isac/xmlsrc/thy-hierarchy.sml Sun Sep 22 17:28:55 2013 +0200
25.2 +++ b/src/Tools/isac/xmlsrc/thy-hierarchy.sml Sun Sep 22 18:09:05 2013 +0200
25.3 @@ -51,7 +51,7 @@
25.4 fun collect_rlss (part, thy') =
25.5 let val rlss = filter ((curry op= thy') o
25.6 ((#1 o #2):(rls' * (theory' * rls)) -> theory'))
25.7 - (!ruleset')
25.8 + (!ruleset') (*SWITCH KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac")*)
25.9 in map (makeHrls part) rlss end;
25.10
25.11 (*.collect all calcs defined in in a theory.*)