1.1 --- a/src/Tools/isac/Interpret/appl.sml Thu Oct 24 14:08:32 2013 +0200
1.2 +++ b/src/Tools/isac/Interpret/appl.sml Thu Oct 24 15:00:44 2013 +0200
1.3 @@ -17,52 +17,47 @@
1.4
1.5 (*FIXME.3.4.03:re-organize from_pblobj_or_detail_thm after rls' --> rls*)
1.6 fun from_pblobj_or_detail_thm thm' p pt =
1.7 - let val (pbl,p',rls') = par_pbl_det pt p
1.8 - in if pbl
1.9 - then let (*val _= tracing("### from_pblobj_or_detail_thm: pbl=true")*)
1.10 - val thy' = get_obj g_domID pt p'
1.11 - val {rew_ord',erls,(*asm_thm,*)...} =
1.12 - get_met (get_obj g_metID pt p')
1.13 - (*val _= tracing("### from_pblobj_or_detail_thm: metID= "^
1.14 - (metID2str(get_obj g_metID pt p')))
1.15 - val _= tracing("### from_pblobj_or_detail_thm: erls= "^erls)*)
1.16 - in ("OK",thy',rew_ord',erls,(*put_asm*)false)
1.17 - end
1.18 - else ((*tracing("### from_pblobj_or_detail_thm: pbl=false");*)
1.19 - (*case assoc(!ruleset', rls') of !!!FIXME.3.4.03:re-organize !!!
1.20 - NONE => ("unknown ruleset '"^rls'^"'","","",Erls,false)
1.21 - | SOME rls =>*)
1.22 - let val thy' = get_obj g_domID pt (par_pblobj pt p)
1.23 - val (rew_ord',erls,(*asm_thm,*)_) = rew_info rls'
1.24 - in ("OK",thy',rew_ord',erls,false) end)
1.25 - end;
1.26 + let
1.27 + val (pbl, p', rls') = par_pbl_det pt p
1.28 + in
1.29 + if pbl
1.30 + then
1.31 + let
1.32 + val thy' = get_obj g_domID pt p'
1.33 + val {rew_ord', erls, ...} = et_met (get_obj g_metID pt p')
1.34 + in ("OK", thy', rew_ord', erls, false) end
1.35 + else
1.36 + let
1.37 + val thy' = get_obj g_domID pt (par_pblobj pt p)
1.38 + val (rew_ord', erls, _) = rew_info rls'
1.39 + in ("OK",thy',rew_ord',erls,false) end
1.40 + end;
1.41 (*FIXME.3.4.03:re-organize from_pblobj_or_detail_calc after rls' --> rls*)
1.42 fun from_pblobj_or_detail_calc scrop p pt =
1.43 -(* val (scrop, p, pt) = (op_, p, pt);
1.44 - *)
1.45 - let val (pbl,p',rls') = par_pbl_det pt p
1.46 - in if pbl
1.47 - then let val thy' = get_obj g_domID pt p'
1.48 - val {calc = scr_isa_fns,...} =
1.49 - get_met (get_obj g_metID pt p')
1.50 - val opt = assoc (scr_isa_fns, scrop)
1.51 - in case opt of
1.52 - SOME isa_fn => ("OK",thy',isa_fn)
1.53 - | NONE => ("applicable_in Calculate: unknown '"^scrop^"'",
1.54 - "",("",e_evalfn)) end
1.55 - else (*case assoc(!ruleset', rls') of
1.56 - NONE => ("unknown ruleset '"^rls'^"'","",("",e_evalfn))
1.57 - | SOME rls => !!!FIXME.3.4.03:re-organize from_pblobj_or_detai*)
1.58 - (* val SOME rls = assoc(!ruleset', rls');
1.59 - *)
1.60 - let val thy' = get_obj g_domID pt (par_pblobj pt p);
1.61 + let
1.62 + val (pbl,p',rls') = par_pbl_det pt p
1.63 + in
1.64 + if pbl
1.65 + then
1.66 + let
1.67 + val thy' = get_obj g_domID pt p'
1.68 + val {calc = scr_isa_fns,...} = get_met (get_obj g_metID pt p')
1.69 + val opt = assoc (scr_isa_fns, scrop)
1.70 + in
1.71 + case opt of
1.72 + SOME isa_fn => ("OK",thy',isa_fn)
1.73 + | NONE => ("applicable_in Calculate: unknown '" ^ scrop ^ "'", "", ("", e_evalfn))
1.74 + end
1.75 + else
1.76 + let
1.77 + val thy' = get_obj g_domID pt (par_pblobj pt p);
1.78 val (_,_,(*_,*)scr_isa_fns) = rew_info rls'(*rls*)
1.79 - in case assoc (scr_isa_fns, scrop) of
1.80 - SOME isa_fn => ("OK",thy',isa_fn)
1.81 - | NONE => ("applicable_in Calculate: unknown '"^scrop^"'",
1.82 - "",("",e_evalfn)) end
1.83 - end;
1.84 -(*------------------------------------------------------------------*)
1.85 + in
1.86 + case assoc (scr_isa_fns, scrop) of
1.87 + SOME isa_fn => ("OK",thy',isa_fn)
1.88 + | NONE => ("applicable_in Calculate: unknown '" ^ scrop ^ "'", "", ("", e_evalfn))
1.89 + end
1.90 + end;
1.91
1.92 val op_and = Const ("op &", [bool, bool] ---> bool);
1.93 (*> (cterm_of thy) (op_and $ Free("a",bool) $ Free("b",bool));
2.1 --- a/src/Tools/isac/Interpret/rewtools.sml Thu Oct 24 14:08:32 2013 +0200
2.2 +++ b/src/Tools/isac/Interpret/rewtools.sml Thu Oct 24 15:00:44 2013 +0200
2.3 @@ -477,7 +477,7 @@
2.4 (*drop those rulesets which are generated in a theory found in #1#*)
2.5 val ancestors_rls =
2.6 filter_out ((curry ((op mem) o swap) dropthys') o ((#1 o #2): rls'*(theory' * rls)->theory'))
2.7 - (rev ((*!ruleset'*) (*SWITCH*) KEStore_Elems.get_rlss (Thy_Info.get_theory thy')(**)))
2.8 + (rev (KEStore_Elems.get_rlss (Thy_Info.get_theory thy')))
2.9 in case assoc (ancestors_rls, rls') of
2.10 SOME (thy', _) => ("IsacKnowledge", thyID2theory' thy')
2.11 | _ => error ("thy_containing_rls : rls '" ^ rls' ^
3.1 --- a/src/Tools/isac/KEStore.thy Thu Oct 24 14:08:32 2013 +0200
3.2 +++ b/src/Tools/isac/KEStore.thy Thu Oct 24 15:00:44 2013 +0200
3.3 @@ -71,14 +71,6 @@
3.4 | NONE => raise ERROR ("rls \""^ rls' ^ "\" missing in KEStore.\n" ^
3.5 "TODO exception hierarchy needs to be established.")
3.6
3.7 -(* associate an rls-identifier with an rls-----------------------
3.8 -fun assoc_rls (rls:rls') = ((#2 o the o assoc')(!ruleset',rls))
3.9 - handle _ => error ("ME_Isa: '"^rls^"' not in system");--------*)
3.10 -;
3.11 -ruleset' := overwritel (!ruleset',
3.12 - [("e_rls", ("Tools", e_rls)),
3.13 - ("e_rrls", ("Tools", e_rrls))]);
3.14 -
3.15 (* fun assoc_calc calID = let
3.16 fun ass ([], key) =
3.17 error ("assoc_calc: '"^ key ^"' not found")
4.1 --- a/src/Tools/isac/Knowledge/Atools.thy Thu Oct 24 14:08:32 2013 +0200
4.2 +++ b/src/Tools/isac/Knowledge/Atools.thy Thu Oct 24 15:00:44 2013 +0200
4.3 @@ -106,7 +106,10 @@
4.4 WN.3.7.03: may be dropped due to more generality: numericals and non-numericals are logically equivalent, where the latter often add to the assumptions (e.g. in Check_elementwise).
4.5 \end{description}
4.6
4.7 -The above rulesets are all visible to the user, and also may be input; thus they must be contained in the global associationlist {\tt ruleset':= }~! All these rulesets must undergo a preparation using the function {\tt prep_rls}, which generates a script for stepwise rewriting etc.
4.8 +The above rulesets are all visible to the user, and also may be input;
4.9 +thus they must be contained in {\tt Theory_Data} (KEStore_Elems.add_rlss,
4.10 +KEStore_Elems.get_rlss). All these rulesets must undergo a preparation
4.11 +using the function {\tt prep_rls}, which generates a script for stepwise rewriting etc.
4.12 The following rulesets are used for internal purposes and usually invisible to the (naive) user:
4.13 \begin{description}
4.14
4.15 @@ -665,10 +668,6 @@
4.16 ],
4.17 scr = Prog ((term_of o the o (parse @{theory})) "empty_script")
4.18 }:rls);
4.19 -ruleset' := overwritelth @{theory} (*outcommented*)
4.20 - (!ruleset',
4.21 - [("atools_erls",atools_erls)(*FIXXXME:del with rls.rls'*)
4.22 - ]);
4.23 *)
4.24 "******* Atools.ML end *******";
4.25
4.26 @@ -720,8 +719,6 @@
4.27 srls = Erls, calc = [], errpatts = [],
4.28 rules = [], scr = EmptyScr})
4.29 list_rls);
4.30 -
4.31 -ruleset' := overwritelthy @{theory} (!ruleset', [("list_rls", list_rls)]);
4.32 *}
4.33 setup {* KEStore_Elems.add_rlss
4.34 [("list_rls", (Context.theory_name @{theory}, prep_rls' @{theory} list_rls))] *}
5.1 --- a/src/Tools/isac/Knowledge/Build_Thydata.thy Thu Oct 24 14:08:32 2013 +0200
5.2 +++ b/src/Tools/isac/Knowledge/Build_Thydata.thy Thu Oct 24 15:00:44 2013 +0200
5.3 @@ -23,7 +23,7 @@
5.4 |> map string_of_calc |> enumerate_strings |> sort string_ord |> map writeln;
5.5 writeln "======= end KEStore_Elems.get_calcs @{theory} =======";
5.6
5.7 - (* use a diff-tool for comparing KEStore_Elems.get_rlss <--> ! ruleset' *)
5.8 + (* use a diff-tool for comparing KEStore_Elems.get_rlss <--> ! xxx *)
5.9 writeln "======= begin ! calclist' =======";
5.10 ! calclist' |> rev (*!!!!!*)
5.11 |> map string_of_calc |> map writeln;
5.12 @@ -49,7 +49,7 @@
5.13 val progthys' = (*WN120321.TODO rearrange theories -------vvv*)
5.14 drop ((find_index (curry Theory.eq_thy first_Knowledge_thy) isacthys') + 1 +3, isacthys');
5.15
5.16 - val isacrlsthms = (*! ruleset'*) (*SWITCH*) (KEStore_Elems.get_rlss @{theory})(**)
5.17 + val isacrlsthms = (KEStore_Elems.get_rlss @{theory})
5.18 |> map (thms_of_rls o #2 o #2)
5.19 |> flat
5.20 |> map thm_of_thm
5.21 @@ -283,7 +283,8 @@
5.22 but this is permanently without errors in Isabelle2012).
5.23
5.24 The major cases of "Unsynchronized.ref" are those in "~~/src/Tools/isac/calcelems.sml",
5.25 - thehier, ptyps, mets, theory', rew_ord', ruleset', calclist',
5.26 + thehier, ptyps, mets, theory', rew_ord', ruleset'-->KEStore_Elems.add_rlss\get_rlss,
5.27 + calclist',
5.28 which shall be handled by "Theory_Data", see
5.29 "~~/test/Tools/isac/ADDTESTS/accumulate-val/lucas_interpreter.sml".
5.30
6.1 --- a/src/Tools/isac/Knowledge/Diff.thy Thu Oct 24 14:08:32 2013 +0200
6.2 +++ b/src/Tools/isac/Knowledge/Diff.thy Thu Oct 24 15:00:44 2013 +0200
6.3 @@ -242,14 +242,6 @@
6.4 erls = Erls, srls = Erls, calc = [], errpatts = [],
6.5 rules = [Rls_ diff_rules, Rls_ norm_Poly ],
6.6 scr = EmptyScr};
6.7 -
6.8 -ruleset' :=
6.9 -overwritelthy @{theory} (!ruleset',
6.10 - [("diff_rules", prep_rls norm_diff),
6.11 - ("norm_diff", prep_rls norm_diff),
6.12 - ("diff_conv", prep_rls diff_conv),
6.13 - ("diff_sym_conv", prep_rls diff_sym_conv)
6.14 - ]);
6.15 *}
6.16 setup {* KEStore_Elems.add_rlss
6.17 [("erls_diff", (Context.theory_name @{theory}, prep_rls erls_diff)),
7.1 --- a/src/Tools/isac/Knowledge/DiffApp.thy Thu Oct 24 14:08:32 2013 +0200
7.2 +++ b/src/Tools/isac/Knowledge/DiffApp.thy Thu Oct 24 15:00:44 2013 +0200
7.3 @@ -74,9 +74,6 @@
7.4 Calc ("Tools.matches", eval_matches "")],
7.5 scr = Prog ((term_of o the o (parse thy)) "empty_script")
7.6 }:rls);
7.7 -
7.8 -ruleset' := overwritelthy @{theory} (!ruleset',
7.9 - [("eval_rls", eval_rls)(*FIXXXME:del with rls.rls'*)]);
7.10 *}
7.11 setup {* KEStore_Elems.add_rlss [("eval_rls", (Context.theory_name @{theory}, eval_rls))] *}
7.12 ML{*
7.13 @@ -256,10 +253,6 @@
7.14 val list_rls = append_rls "list_rls" list_rls
7.15 [Thm ("filterVar_Const", num_str @{thm filterVar_Const}),
7.16 Thm ("filterVar_Nil", num_str @{thm filterVar_Nil})];
7.17 -
7.18 -ruleset' := overwritelthy @{theory} (!ruleset',
7.19 - [("list_rls",list_rls)
7.20 - ]);
7.21 *}
7.22 setup {* KEStore_Elems.add_rlss [("list_rls", (Context.theory_name @{theory}, list_rls))] *}
7.23
8.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Thu Oct 24 14:08:32 2013 +0200
8.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Thu Oct 24 15:00:44 2013 +0200
8.3 @@ -406,20 +406,6 @@
8.4 scr = EmptyScr};
8.5 *}
8.6
8.7 -ML {*
8.8 -ruleset' :=
8.9 -overwritelthy @{theory}
8.10 - (!ruleset',
8.11 -[("simplify_System_parenthesized", prep_rls simplify_System_parenthesized),
8.12 - ("simplify_System", prep_rls simplify_System),
8.13 - ("isolate_bdvs", prep_rls isolate_bdvs),
8.14 - ("isolate_bdvs_4x4", prep_rls isolate_bdvs_4x4),
8.15 - ("order_system", prep_rls order_system),
8.16 - ("order_add_mult_System", prep_rls order_add_mult_System),
8.17 - ("norm_System_noadd_fractions", prep_rls norm_System_noadd_fractions),
8.18 - ("norm_System", prep_rls norm_System)
8.19 - ]);
8.20 -*}
8.21 setup {* KEStore_Elems.add_rlss
8.22 [("simplify_System_parenthesized",
8.23 (Context.theory_name @{theory}, prep_rls simplify_System_parenthesized)),
9.1 --- a/src/Tools/isac/Knowledge/Equation.thy Thu Oct 24 14:08:32 2013 +0200
9.2 +++ b/src/Tools/isac/Knowledge/Equation.thy Thu Oct 24 15:00:44 2013 +0200
9.3 @@ -44,10 +44,6 @@
9.4 val univariate_equation_prls =
9.5 append_rls "univariate_equation_prls" e_rls
9.6 [Calc ("Tools.matches",eval_matches "")];
9.7 -ruleset' :=
9.8 -overwritelthy @{theory} (!ruleset',
9.9 - [("univariate_equation_prls",
9.10 - prep_rls univariate_equation_prls)]);
9.11 *}
9.12 setup {* KEStore_Elems.add_rlss [("univariate_equation_prls",
9.13 (Context.theory_name @{theory}, prep_rls univariate_equation_prls))] *}
10.1 --- a/src/Tools/isac/Knowledge/InsSort.thy Thu Oct 24 14:08:32 2013 +0200
10.2 +++ b/src/Tools/isac/Knowledge/InsSort.thy Thu Oct 24 15:00:44 2013 +0200
10.3 @@ -97,10 +97,6 @@
10.4 crls = eval_rls, errpats = [], nrls = norm_Rational},
10.5 "Script Sort (u_::'a list) = (Rewrite_Set ins_sort False) u_"
10.6 ));
10.7 -
10.8 -ruleset' := overwritelthy @{theory} (!ruleset',
10.9 - [(*("ins_sort",ins_sort) overwrites a Isa fun!!*)
10.10 - ]:(string * rls) list);
10.11 *}
10.12 setup {* KEStore_Elems.add_rlss [("ins_sort", (Context.theory_name @{theory}, ins_sort))] *}
10.13
11.1 --- a/src/Tools/isac/Knowledge/Integrate.thy Thu Oct 24 14:08:32 2013 +0200
11.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy Thu Oct 24 15:00:44 2013 +0200
11.3 @@ -327,18 +327,6 @@
11.4 Rls_ simplify_Integral
11.5 ],
11.6 scr = EmptyScr};
11.7 -ruleset' :=
11.8 -overwritelthy @{theory} (!ruleset',
11.9 - [("integration_rules", prep_rls integration_rules),
11.10 - ("add_new_c", prep_rls add_new_c),
11.11 - ("simplify_Integral", prep_rls simplify_Integral),
11.12 - ("integration", prep_rls integration),
11.13 - ("separate_bdv2", separate_bdv2),
11.14 -
11.15 - ("norm_Rational_noadd_fractions", norm_Rational_noadd_fractions),
11.16 - ("norm_Rational_rls_noadd_fractions",
11.17 - norm_Rational_rls_noadd_fractions)
11.18 - ]);
11.19 *}
11.20 setup {* KEStore_Elems.add_rlss
11.21 [("integration_rules", (Context.theory_name @{theory}, prep_rls integration_rules)),
12.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Thu Oct 24 14:08:32 2013 +0200
12.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Thu Oct 24 15:00:44 2013 +0200
12.3 @@ -40,11 +40,6 @@
12.4
12.5 text {*store the rule set for math engine*}
12.6
12.7 -ML {*
12.8 -ruleset' := overwritelthy @{theory} (!ruleset',
12.9 - [("inverse_z", inverse_z)
12.10 - ]);
12.11 -*}
12.12 setup {* KEStore_Elems.add_rlss [("inverse_z", (Context.theory_name @{theory}, inverse_z))] *}
12.13
12.14 subsection{*Define the Specification*}
13.1 --- a/src/Tools/isac/Knowledge/LinEq.thy Thu Oct 24 14:08:32 2013 +0200
13.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy Thu Oct 24 15:00:44 2013 +0200
13.3 @@ -70,10 +70,6 @@
13.4 Calc ("Atools.pow" ,eval_binop "#power_"),
13.5 *)
13.6 ];
13.7 -
13.8 -ruleset' := overwritelthy @{theory} (!ruleset',
13.9 - [("LinEq_erls",LinEq_erls)(*FIXXXME:del with rls.rls'*)
13.10 - ]);
13.11 *}
13.12 setup {* KEStore_Elems.add_rlss
13.13 [("LinEq_erls", (Context.theory_name @{theory}, LinEq_erls))] *}
13.14 @@ -97,9 +93,6 @@
13.15 Calc ("Atools.pow" ,eval_binop "#power_")
13.16 ],
13.17 scr = EmptyScr}:rls);
13.18 -
13.19 -ruleset' := overwritelthy @{theory} (!ruleset',
13.20 - [("LinPoly_simplify",LinPoly_simplify)]);
13.21 *}
13.22 setup {* KEStore_Elems.add_rlss
13.23 [("LinPoly_simplify", (Context.theory_name @{theory}, LinPoly_simplify))] *}
13.24 @@ -121,8 +114,6 @@
13.25 (* bx=c -> x=c/b *)
13.26 ],
13.27 scr = EmptyScr}:rls);
13.28 -ruleset' := overwritelthy @{theory} (!ruleset',
13.29 - [("LinEq_simplify",LinEq_simplify)]);
13.30 *}
13.31 setup {* KEStore_Elems.add_rlss
13.32 [("LinEq_simplify", (Context.theory_name @{theory}, LinEq_simplify))] *}
14.1 --- a/src/Tools/isac/Knowledge/Partial_Fractions.thy Thu Oct 24 14:08:32 2013 +0200
14.2 +++ b/src/Tools/isac/Knowledge/Partial_Fractions.thy Thu Oct 24 15:00:44 2013 +0200
14.3 @@ -161,13 +161,6 @@
14.4 *}
14.5
14.6 text {*store the rule set for math engine*}
14.7 -ML {*
14.8 -ruleset' := overwritelthy @{theory} (!ruleset',
14.9 - [("ansatz_rls", ansatz_rls),
14.10 - ("multiply_ansatz", multiply_ansatz),
14.11 - ("equival_trans", equival_trans)
14.12 - ]);
14.13 -*}
14.14 setup {* KEStore_Elems.add_rlss
14.15 [("ansatz_rls", (Context.theory_name @{theory}, ansatz_rls)),
14.16 ("multiply_ansatz", (Context.theory_name @{theory}, multiply_ansatz)),
15.1 --- a/src/Tools/isac/Knowledge/Poly.thy Thu Oct 24 14:08:32 2013 +0200
15.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Thu Oct 24 15:00:44 2013 +0200
15.3 @@ -1551,39 +1551,7 @@
15.4
15.5 scr = EmptyScr}:rls;
15.6 *}
15.7 -ML {*
15.8 -ruleset' :=
15.9 -overwritelthy @{theory} (!ruleset',
15.10 - [("norm_Poly", prep_rls norm_Poly),
15.11 - ("Poly_erls", prep_rls Poly_erls)(*FIXXXME:del with rls.rls'*),
15.12 - ("expand", prep_rls expand),
15.13 - ("expand_poly", prep_rls expand_poly),
15.14 - ("simplify_power", prep_rls simplify_power),
15.15
15.16 - ("order_add_mult", prep_rls order_add_mult),
15.17 - ("collect_numerals", prep_rls collect_numerals),
15.18 - ("collect_numerals_", prep_rls collect_numerals_),
15.19 - ("reduce_012", prep_rls reduce_012),
15.20 - ("discard_parentheses", prep_rls discard_parentheses),
15.21 -
15.22 - ("make_polynomial", prep_rls make_polynomial),
15.23 - ("expand_binoms", prep_rls expand_binoms),
15.24 - ("rev_rew_p", prep_rls rev_rew_p),
15.25 - ("discard_minus", prep_rls discard_minus),
15.26 - ("expand_poly_", prep_rls expand_poly_),
15.27 -
15.28 - ("expand_poly_rat_", prep_rls expand_poly_rat_),
15.29 - ("simplify_power_", prep_rls simplify_power_),
15.30 - ("calc_add_mult_pow_", prep_rls calc_add_mult_pow_),
15.31 - ("reduce_012_mult_", prep_rls reduce_012_mult_),
15.32 - ("reduce_012_", prep_rls reduce_012_),
15.33 -
15.34 - ("discard_parentheses1",prep_rls discard_parentheses1),
15.35 - ("order_mult_rls_", prep_rls order_mult_rls_),
15.36 - ("order_add_rls_", prep_rls order_add_rls_),
15.37 - ("make_rat_poly_with_parentheses", prep_rls make_rat_poly_with_parentheses)
15.38 - ]);
15.39 -*}
15.40 setup {* KEStore_Elems.add_rlss
15.41 [("norm_Poly", (Context.theory_name @{theory}, prep_rls norm_Poly)),
15.42 ("Poly_erls", (Context.theory_name @{theory}, prep_rls Poly_erls)),(*FIXXXME:del with rls.rls'*)
16.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Thu Oct 24 14:08:32 2013 +0200
16.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Thu Oct 24 15:00:44 2013 +0200
16.3 @@ -487,12 +487,6 @@
16.4 ],
16.5 scr = Prog ((term_of o the o (parse thy)) "empty_script")
16.6 }:rls);
16.7 -
16.8 -ruleset' := overwritelthy @{theory} (!ruleset',
16.9 - [("cancel_leading_coeff",cancel_leading_coeff),
16.10 - ("complete_square",complete_square),
16.11 - ("PolyEq_erls",PolyEq_erls),(*FIXXXME:del with rls.rls'*)
16.12 - ("polyeq_simplify",polyeq_simplify)]);
16.13 *}
16.14 setup {* KEStore_Elems.add_rlss
16.15 [("cancel_leading_coeff", (Context.theory_name @{theory}, cancel_leading_coeff)),
16.16 @@ -825,21 +819,6 @@
16.17 ],
16.18 scr = Prog ((term_of o the o (parse thy)) "empty_script")
16.19 }:rls);
16.20 -
16.21 -ruleset' :=
16.22 -overwritelthy @{theory}
16.23 - (!ruleset',
16.24 - [("d0_polyeq_simplify", d0_polyeq_simplify),
16.25 - ("d1_polyeq_simplify", d1_polyeq_simplify),
16.26 - ("d2_polyeq_simplify", d2_polyeq_simplify),
16.27 - ("d2_polyeq_bdv_only_simplify", d2_polyeq_bdv_only_simplify),
16.28 - ("d2_polyeq_sq_only_simplify", d2_polyeq_sq_only_simplify),
16.29 -
16.30 - ("d2_polyeq_pqFormula_simplify", d2_polyeq_pqFormula_simplify),
16.31 - ("d2_polyeq_abcFormula_simplify", d2_polyeq_abcFormula_simplify),
16.32 - ("d3_polyeq_simplify", d3_polyeq_simplify),
16.33 - ("d4_polyeq_simplify", d4_polyeq_simplify)
16.34 - ]);
16.35 *}
16.36 setup {* KEStore_Elems.add_rlss
16.37 [("d0_polyeq_simplify", (Context.theory_name @{theory}, d0_polyeq_simplify)),
16.38 @@ -1502,15 +1481,6 @@
16.39 (*Calc ("Fields.inverse_class.divide" ,eval_cancel "#divide_e") too weak!*)
16.40 ],
16.41 scr = EmptyScr}:rls);
16.42 -
16.43 -
16.44 -ruleset' := overwritelthy @{theory} (!ruleset',
16.45 - [("order_add_mult_in", order_add_mult_in),
16.46 - ("collect_bdv", collect_bdv),
16.47 - ("make_polynomial_in", make_polynomial_in),
16.48 - ("make_ratpoly_in", make_ratpoly_in),
16.49 - ("separate_bdvs", separate_bdvs)
16.50 - ]);
16.51 *}
16.52 setup {* KEStore_Elems.add_rlss
16.53 [("order_add_mult_in", (Context.theory_name @{theory}, order_add_mult_in)),
17.1 --- a/src/Tools/isac/Knowledge/PolyMinus.thy Thu Oct 24 14:08:32 2013 +0200
17.2 +++ b/src/Tools/isac/Knowledge/PolyMinus.thy Thu Oct 24 15:00:44 2013 +0200
17.3 @@ -385,17 +385,6 @@
17.4 Calc ("Groups.plus_class.plus", eval_binop "#add_"),
17.5 Calc ("Groups.minus_class.minus", eval_binop "#subtr_")
17.6 ];
17.7 -
17.8 -ruleset' :=
17.9 -overwritelthy @{theory} (!ruleset',
17.10 - [("ordne_alphabetisch", prep_rls ordne_alphabetisch),
17.11 - ("fasse_zusammen", prep_rls fasse_zusammen),
17.12 - ("verschoenere", prep_rls verschoenere),
17.13 - ("ordne_monome", prep_rls ordne_monome),
17.14 - ("klammern_aufloesen", prep_rls klammern_aufloesen),
17.15 - ("klammern_ausmultiplizieren",
17.16 - prep_rls klammern_ausmultiplizieren)
17.17 - ]);
17.18 *}
17.19 setup {* KEStore_Elems.add_rlss
17.20 [("ordne_alphabetisch", (Context.theory_name @{theory}, prep_rls ordne_alphabetisch)),
18.1 --- a/src/Tools/isac/Knowledge/RatEq.thy Thu Oct 24 14:08:32 2013 +0200
18.2 +++ b/src/Tools/isac/Knowledge/RatEq.thy Thu Oct 24 15:00:44 2013 +0200
18.3 @@ -114,9 +114,6 @@
18.4 [Thm ("and_commute",num_str @{thm and_commute}), (*WN: ein Hack*)
18.5 Thm ("or_commute",num_str @{thm or_commute}) (*WN: ein Hack*)
18.6 ];
18.7 -ruleset' := overwritelthy @{theory} (!ruleset',
18.8 - [("rateq_erls",rateq_erls)(*FIXXXME:del with rls.rls'*)
18.9 - ]);
18.10 *}
18.11 setup {* KEStore_Elems.add_rlss [("rateq_erls", (Context.theory_name @{theory}, rateq_erls))] *}
18.12 ML {*
18.13 @@ -148,9 +145,6 @@
18.14 ],
18.15 scr = Prog ((term_of o the o (parse thy)) "empty_script")
18.16 }:rls);
18.17 -ruleset' := overwritelthy @{theory} (!ruleset',
18.18 - [("RatEq_eliminate",RatEq_eliminate)
18.19 - ]);
18.20 *}
18.21 setup {* KEStore_Elems.add_rlss [("RatEq_eliminate",
18.22 (Context.theory_name @{theory}, RatEq_eliminate))] *}
18.23 @@ -179,9 +173,6 @@
18.24 ],
18.25 scr = Prog ((term_of o the o (parse thy)) "empty_script")
18.26 }:rls);
18.27 -ruleset' := overwritelthy @{theory} (!ruleset',
18.28 - [("RatEq_simplify",RatEq_simplify)
18.29 - ]);
18.30 *}
18.31 setup {* KEStore_Elems.add_rlss [("RatEq_simplify",
18.32 (Context.theory_name @{theory}, RatEq_simplify))] *}
19.1 --- a/src/Tools/isac/Knowledge/Rational.thy Thu Oct 24 14:08:32 2013 +0200
19.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Thu Oct 24 15:00:44 2013 +0200
19.3 @@ -862,32 +862,7 @@
19.4 ],
19.5 scr = EmptyScr}:rls);
19.6 *}
19.7 -ML {*
19.8 -ruleset' := overwritelthy @{theory} (!ruleset',
19.9 - [("calculate_Rational", calculate_Rational),
19.10 - ("calc_rat_erls",calc_rat_erls),
19.11 - ("rational_erls", rational_erls),
19.12 - ("cancel_p", cancel_p),
19.13 - ("add_fractions_p", add_fractions_p),
19.14
19.15 - ("add_fractions_p_rls", add_fractions_p_rls),
19.16 - (*WN120410 ("discard_minus", discard_minus), is defined in Poly.thy*)
19.17 - ("powers_erls", powers_erls),
19.18 - ("powers", powers),
19.19 - ("rat_mult_divide", rat_mult_divide),
19.20 - ("reduce_0_1_2", reduce_0_1_2),
19.21 -
19.22 - ("rat_reduce_1", rat_reduce_1),
19.23 - ("norm_rat_erls", norm_rat_erls),
19.24 - ("norm_Rational", norm_Rational),
19.25 - ("norm_Rational_rls", norm_Rational_rls),
19.26 - ("norm_Rational_parenthesized", norm_Rational_parenthesized),
19.27 -
19.28 - ("rat_mult_poly", rat_mult_poly),
19.29 - ("rat_mult_div_pow", rat_mult_div_pow),
19.30 - ("cancel_p_rls", cancel_p_rls)
19.31 - ]);
19.32 -*}
19.33 setup {* KEStore_Elems.add_rlss
19.34 [("calculate_Rational", (Context.theory_name @{theory}, calculate_Rational)),
19.35 ("calc_rat_erls", (Context.theory_name @{theory}, calc_rat_erls)),
20.1 --- a/src/Tools/isac/Knowledge/Root.thy Thu Oct 24 14:08:32 2013 +0200
20.2 +++ b/src/Tools/isac/Knowledge/Root.thy Thu Oct 24 15:00:44 2013 +0200
20.3 @@ -189,10 +189,6 @@
20.4 Calc ("Groups.times_class.times", eval_binop "#mult_"),
20.5 Calc ("HOL.eq",eval_equal "#equal_")
20.6 ];
20.7 -
20.8 -ruleset' := overwritelthy @{theory} (!ruleset',
20.9 - [("Root_erls",Root_erls) (*FIXXXME:del with rls.rls'*)
20.10 - ]);
20.11 *}
20.12 setup {* KEStore_Elems.add_rlss [("Root_erls", (Context.theory_name @{theory}, Root_erls))] *}
20.13 ML {*
20.14 @@ -261,9 +257,6 @@
20.15 ],
20.16 scr = Prog ((term_of o the o (parse thy)) "empty_script")
20.17 }:rls);
20.18 -ruleset' := overwritelthy @{theory} (!ruleset',
20.19 - [("make_rooteq", make_rooteq)
20.20 - ]);
20.21 *}
20.22 setup {* KEStore_Elems.add_rlss [("make_rooteq", (Context.theory_name @{theory}, make_rooteq))] *}
20.23 ML {*
20.24 @@ -336,11 +329,6 @@
20.25 ],
20.26 scr = Prog ((term_of o the o (parse thy)) "empty_script")
20.27 }:rls);
20.28 -
20.29 -
20.30 -ruleset' := overwritelthy @{theory} (!ruleset',
20.31 - [("expand_rootbinoms", expand_rootbinoms)
20.32 - ]);
20.33 *}
20.34 setup {* KEStore_Elems.add_rlss
20.35 [("expand_rootbinoms", (Context.theory_name @{theory}, expand_rootbinoms))] *}
21.1 --- a/src/Tools/isac/Knowledge/RootEq.thy Thu Oct 24 14:08:32 2013 +0200
21.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy Thu Oct 24 15:00:44 2013 +0200
21.3 @@ -240,12 +240,6 @@
21.4 Calc ("RootEq.is'_normSqrtTerm'_in",eval_is_normSqrtTerm_in""),
21.5 Calc ("RootEq.is'_rootTerm'_in",eval_is_rootTerm_in "")
21.6 ];
21.7 -
21.8 -ruleset' := overwritelthy @{theory} (!ruleset',
21.9 - [("RootEq_erls",RootEq_erls),
21.10 - (*FIXXXME:del with rls.rls'*)
21.11 - ("rooteq_srls",rooteq_srls)
21.12 - ]);
21.13 *}
21.14 setup {* KEStore_Elems.add_rlss
21.15 [("RootEq_erls", (Context.theory_name @{theory}, RootEq_erls)),
21.16 @@ -349,10 +343,6 @@
21.17 (* a=c*d/g*sqrt(x) ->a^2=c^2*d^2/g^2*x *)
21.18 ],scr = Prog ((term_of o the o (parse thy)) "empty_script")
21.19 }:rls);
21.20 -
21.21 -ruleset' := overwritelthy @{theory} (!ruleset',
21.22 - [("sqrt_isolate",sqrt_isolate)
21.23 - ]);
21.24 *}
21.25 setup {* KEStore_Elems.add_rlss
21.26 [("sqrt_isolate", (Context.theory_name @{theory}, sqrt_isolate))] *}
21.27 @@ -401,10 +391,6 @@
21.28 ],
21.29 scr = Prog ((term_of o the o (parse thy)) "empty_script")
21.30 }:rls);
21.31 -
21.32 -ruleset' := overwritelthy @{theory} (!ruleset',
21.33 - [("l_sqrt_isolate",l_sqrt_isolate)
21.34 - ]);
21.35 *}
21.36 setup {* KEStore_Elems.add_rlss
21.37 [("l_sqrt_isolate", (Context.theory_name @{theory}, l_sqrt_isolate))] *}
21.38 @@ -454,10 +440,6 @@
21.39 ],
21.40 scr = Prog ((term_of o the o (parse thy)) "empty_script")
21.41 }:rls);
21.42 -
21.43 -ruleset' := overwritelthy @{theory} (!ruleset',
21.44 - [("r_sqrt_isolate",r_sqrt_isolate)
21.45 - ]);
21.46 *}
21.47 setup {* KEStore_Elems.add_rlss
21.48 [("r_sqrt_isolate", (Context.theory_name @{theory}, r_sqrt_isolate))] *}
21.49 @@ -493,9 +475,6 @@
21.50 ],
21.51 scr = Prog ((term_of o the o (parse thy)) "empty_script")
21.52 }:rls);
21.53 - ruleset' := overwritelthy @{theory} (!ruleset',
21.54 - [("rooteq_simplify",rooteq_simplify)
21.55 - ]);
21.56 *}
21.57 setup {* KEStore_Elems.add_rlss
21.58 [("rooteq_simplify", (Context.theory_name @{theory}, rooteq_simplify))] *}
22.1 --- a/src/Tools/isac/Knowledge/RootRat.thy Thu Oct 24 14:08:32 2013 +0200
22.2 +++ b/src/Tools/isac/Knowledge/RootRat.thy Thu Oct 24 15:00:44 2013 +0200
22.3 @@ -24,11 +24,6 @@
22.4 (* "- z1 = -1 * z1" *)
22.5 Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_")
22.6 ];
22.7 -
22.8 -ruleset' := overwritelthy thy (!ruleset',
22.9 - [("rootrat_erls", prep_rls rootrat_erls), (*FIXXXME:del with rls.rls'*)
22.10 - ("calculate_RootRat", prep_rls calculate_RootRat)
22.11 - ]);
22.12 *}
22.13 setup {* KEStore_Elems.add_rlss
22.14 [("rootrat_erls", (Context.theory_name @{theory}, prep_rls rootrat_erls)),
23.1 --- a/src/Tools/isac/Knowledge/RootRatEq.thy Thu Oct 24 14:08:32 2013 +0200
23.2 +++ b/src/Tools/isac/Knowledge/RootRatEq.thy Thu Oct 24 15:00:44 2013 +0200
23.3 @@ -108,9 +108,6 @@
23.4 (merge_rls "" rateq_erls
23.5 (append_rls "" e_rls
23.6 [])));
23.7 -
23.8 -ruleset' := overwritelthy @{theory} (!ruleset',
23.9 - [("RooRatEq_erls",RooRatEq_erls) (*FIXXXME:del with rls.rls'*)]);
23.10 *}
23.11 setup {* KEStore_Elems.add_rlss
23.12 [("RooRatEq_erls", (Context.theory_name @{theory}, RooRatEq_erls))] *}
23.13 @@ -132,10 +129,6 @@
23.14 Thm("rootrat_equation_right_2",num_str @{thm rootrat_equation_right_2})
23.15 (* [|f is_rootTerm_in bdv|] ==> ( (a = e/f) = ( a * f = e ))*)
23.16 ], scr = Prog ((term_of o the o (parse thy)) "empty_script")}:rls);
23.17 -
23.18 -ruleset' := overwritelthy @{theory} (!ruleset',
23.19 - [("rootrat_solve",rootrat_solve)
23.20 - ]);
23.21 *}
23.22 setup {* KEStore_Elems.add_rlss
23.23 [("rootrat_solve", (Context.theory_name @{theory}, rootrat_solve))] *}
24.1 --- a/src/Tools/isac/Knowledge/Test.thy Thu Oct 24 14:08:32 2013 +0200
24.2 +++ b/src/Tools/isac/Knowledge/Test.thy Thu Oct 24 15:00:44 2013 +0200
24.3 @@ -306,16 +306,9 @@
24.4 scr = Prog ((term_of o the o (parse thy)) "empty_script")
24.5 }:rls;
24.6 *}
24.7 +setup {* KEStore_Elems.add_rlss [("testerls", (Context.theory_name @{theory}, prep_rls testerls))] *}
24.8 +
24.9 ML {*
24.10 -
24.11 -ruleset' := overwritelthy @{theory} (!ruleset',
24.12 - [("testerls", prep_rls testerls)
24.13 - ]);
24.14 -*}
24.15 -setup {* KEStore_Elems.add_rlss [("testerls", (Context.theory_name @{theory}, prep_rls testerls))] *}
24.16 -ML {*
24.17 -
24.18 -
24.19 (*make () dissappear*)
24.20 val rearrange_assoc =
24.21 Rls{id = "rearrange_assoc", preconds = [],
24.22 @@ -518,16 +511,6 @@
24.23 ("Test.contains_root",("contains'_root",
24.24 eval_contains_root"#contains_root_"))
24.25 ];
24.26 -
24.27 -ruleset' := overwritelthy @{theory} (!ruleset',
24.28 - [("Test_simplify", prep_rls Test_simplify),
24.29 - ("tval_rls", prep_rls tval_rls),
24.30 - ("isolate_root", prep_rls isolate_root),
24.31 - ("isolate_bdv", prep_rls isolate_bdv),
24.32 - ("matches",
24.33 - prep_rls (append_rls "matches" testerls
24.34 - [Calc ("Tools.matches",eval_matches "#matches_")]))
24.35 - ]);
24.36 *}
24.37 setup {* KEStore_Elems.add_rlss
24.38 [("Test_simplify", (Context.theory_name @{theory}, prep_rls Test_simplify)),
24.39 @@ -641,15 +624,8 @@
24.40 )
24.41 , ---------27.4.02*)
24.42 );
24.43 +*}
24.44
24.45 -*}
24.46 -ML {*
24.47 -ruleset' := overwritelthy @{theory} (!ruleset',
24.48 - [("norm_equation", prep_rls norm_equation),
24.49 - ("ac_plus_times", prep_rls ac_plus_times),
24.50 - ("rearrange_assoc", prep_rls rearrange_assoc)
24.51 - ]);
24.52 -*}
24.53 setup {* KEStore_Elems.add_rlss
24.54 [("norm_equation", (Context.theory_name @{theory}, prep_rls norm_equation)),
24.55 ("ac_plus_times", (Context.theory_name @{theory}, prep_rls ac_plus_times)),
24.56 @@ -1539,12 +1515,6 @@
24.57 scr = EmptyScr
24.58 (*Script ((term_of o the o (parse thy)) scr_expand_binomtest)*)
24.59 }:rls;
24.60 -
24.61 -
24.62 -ruleset' := overwritelthy @{theory} (!ruleset',
24.63 - [("make_polytest", prep_rls make_polytest),
24.64 - ("expand_binomtest", prep_rls expand_binomtest)
24.65 - ]);
24.66 *}
24.67 setup {* KEStore_Elems.add_rlss
24.68 [("make_polytest", (Context.theory_name @{theory}, prep_rls make_polytest)),
25.1 --- a/src/Tools/isac/ProgLang/ListC.thy Thu Oct 24 14:08:32 2013 +0200
25.2 +++ b/src/Tools/isac/ProgLang/ListC.thy Thu Oct 24 15:00:44 2013 +0200
25.3 @@ -140,10 +140,6 @@
25.4 Thm ("zip_Nil",num_str @{thm zip_Nil})],
25.5 scr = EmptyScr}:rls;
25.6 *}
25.7 -
25.8 -ML{*
25.9 -ruleset' := overwritelthy @{theory} (!ruleset', [("list_rls", list_rls)]);
25.10 -*}
25.11 setup {* KEStore_Elems.add_rlss [("list_rls", (Context.theory_name @{theory}, list_rls))] *}
25.12
25.13 end
26.1 --- a/src/Tools/isac/ProgLang/Tools.thy Thu Oct 24 14:08:32 2013 +0200
26.2 +++ b/src/Tools/isac/ProgLang/Tools.thy Thu Oct 24 15:00:44 2013 +0200
26.3 @@ -219,8 +219,6 @@
26.4 (*for evaluating scripts*)
26.5
26.6 val list_rls = append_rls "list_rls" list_rls [Calc ("Tools.rhs", eval_rhs "")];
26.7 -
26.8 -ruleset' := overwritelthy @{theory} (!ruleset', [("list_rls", list_rls)]);
26.9 *}
26.10 setup {* KEStore_Elems.add_rlss [("list_rls", (Context.theory_name @{theory}, list_rls))] *}
26.11 ML {*
27.1 --- a/src/Tools/isac/ProgLang/rewrite.sml Thu Oct 24 14:08:32 2013 +0200
27.2 +++ b/src/Tools/isac/ProgLang/rewrite.sml Thu Oct 24 15:00:44 2013 +0200
27.3 @@ -556,7 +556,6 @@
27.4 val thy = assoc_thy thy';
27.5 val rls = assoc_rls rls
27.6 val subst = subs'2subst thy subs'
27.7 - (*val subrls = instantiate_rls subs ((the o assoc')(!ruleset',rls))*)
27.8 in case rewrite_set_inst_ thy put_asm subst (*sub*)rls
27.9 ((term_of o the o (parse thy)) ct) of
27.10 NONE => NONE
28.1 --- a/src/Tools/isac/ProgLang/scrtools.sml Thu Oct 24 14:08:32 2013 +0200
28.2 +++ b/src/Tools/isac/ProgLang/scrtools.sml Thu Oct 24 15:00:44 2013 +0200
28.3 @@ -463,7 +463,7 @@
28.4 (*.prepare the input for an rls for use:
28.5 # generate a script for stepwise execution of the rls
28.6 # filter the operators for Calc out of the script ?WN111014?
28.7 - !!!use this function in ruleset' := !!! .*)
28.8 + !!!use this function while storing by or integrate into KEStore_Elems.add_rlss.*)
28.9 fun prep_rls' _ Erls = error "prep_rls not impl. for Erls"
28.10 | prep_rls' thy (Rls {id,preconds,rew_ord,erls,srls,calc,rules,errpatts,...}) =
28.11 let val sc = (rules2scr_Rls thy rules)
29.1 --- a/src/Tools/isac/calcelems.sml Thu Oct 24 14:08:32 2013 +0200
29.2 +++ b/src/Tools/isac/calcelems.sml Thu Oct 24 15:00:44 2013 +0200
29.3 @@ -420,11 +420,6 @@
29.4 ("dummy_ord", dummy_ord)]);
29.5
29.6
29.7 -(*WN060120 a hack to get alltogether run again with minimal effort:
29.8 - theory' is inserted for creating thy_hierarchy; calls for assoc_rls
29.9 - need not be called*)
29.10 -val ruleset' = Unsynchronized.ref ([]:(rls' * (theory' * rls)) list);
29.11 -
29.12 (*FIXME.040207 calclist': used by prep_rls, NOT in met*)
29.13 val calclist' = Unsynchronized.ref ([]: calc list);
29.14
29.15 @@ -453,8 +448,6 @@
29.16 | Hrls of {guh: guh,
29.17 coursedesign: authors,
29.18 mathauthors: authors,
29.19 - (*like vvvvvvvvvvvvv val ruleset'
29.20 - WN060711 redesign together !*)
29.21 thy_rls: (thyID * rls)}
29.22 | Hcal of {guh: guh,
29.23 coursedesign: authors,
30.1 --- a/src/Tools/isac/xmlsrc/thy-hierarchy.sml Thu Oct 24 14:08:32 2013 +0200
30.2 +++ b/src/Tools/isac/xmlsrc/thy-hierarchy.sml Thu Oct 24 15:00:44 2013 +0200
30.3 @@ -51,7 +51,7 @@
30.4 fun collect_rlss (part, thy') =
30.5 let val rlss = filter ((curry op= thy') o
30.6 ((#1 o #2):(rls' * (theory' * rls)) -> theory'))
30.7 - ((*!ruleset')*) (*SWITCH*) KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac"))(**)
30.8 + (KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac"))
30.9 in map (makeHrls part) rlss end;
30.10
30.11 (*.collect all calcs defined in in a theory.*)