1.1 --- a/src/Tools/isac/CalcElements/KEStore.thy Wed Apr 08 15:50:03 2020 +0200
1.2 +++ b/src/Tools/isac/CalcElements/KEStore.thy Wed Apr 08 16:56:47 2020 +0200
1.3 @@ -8,6 +8,7 @@
1.4 ML_file libraryC.sml
1.5 ML_file "rule-def.sml"
1.6 ML_file "exec-def.sml"
1.7 +ML_file "rewrite-order.sml"
1.8 ML_file theoryC.sml
1.9 ML_file rule.sml
1.10 ML_file "rule-set.sml"
2.1 --- a/src/Tools/isac/CalcElements/calcelems.sml Wed Apr 08 15:50:03 2020 +0200
2.2 +++ b/src/Tools/isac/CalcElements/calcelems.sml Wed Apr 08 16:56:47 2020 +0200
2.3 @@ -562,7 +562,7 @@
2.4 see ME/calchead.sml 'fun is_copy_named'. *)
2.5 pre : term list (* preconditions in where *)
2.6 };
2.7 -val e_met = {guh = "met_empty", mathauthors = [], init = e_metID, rew_ord' = "e_rew_ord'",
2.8 +val e_met = {guh = "met_empty", mathauthors = [], init = e_metID, rew_ord' = Rewrite_Ord.e_rew_ord',
2.9 erls = Rule_Set.empty, srls = Rule_Set.empty, prls = Rule_Set.empty, calc = [], crls = Rule_Set.empty,
2.10 errpats = [], nrls = Rule_Set.empty, ppc = [], pre = [], scr = Rule.EmptyScr};
2.11 val e_Mets = Ptyp ("e_metID", [e_met],[]);
3.1 --- a/src/Tools/isac/CalcElements/exec-def.sml Wed Apr 08 15:50:03 2020 +0200
3.2 +++ b/src/Tools/isac/CalcElements/exec-def.sml Wed Apr 08 16:56:47 2020 +0200
3.3 @@ -33,6 +33,12 @@
3.4 then if ci1 = ci2 then true else error ("calc_eq: " ^ ci1 ^ " <> " ^ ci2)
3.5 else false
3.6
3.7 +(* eval function calling sml code during rewriting.
3.8 +Unifying "type cal" and "type calc" would make Lucas-Interpretation more efficient,
3.9 + see "fun rule2stac": instead of
3.10 + Num_Calc: calID * eval_fn -> rule
3.11 + would be better
3.12 + Num_Calc: prog_calcID * (calID * eval_fn)) -> rule*)
3.13 type eval_fn = Rule_Def.eval_fn
3.14 fun e_evalfn (_ : 'a) (_ : term) (_ : theory) = NONE : (string * term) option;
3.15 end
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/src/Tools/isac/CalcElements/rewrite-order.sml Wed Apr 08 16:56:47 2020 +0200
4.3 @@ -0,0 +1,53 @@
4.4 +(* Title: CalcElements/rewrite-order.sml
4.5 + Author: Walther Neuper
4.6 + (c) due to copyright terms
4.7 +
4.8 +TODO: use "Rewrite_Ord" for renaming identifiers.
4.9 +*)
4.10 +signature REWRITE_ORDER =
4.11 +sig
4.12 + type subst
4.13 + val e_rew_ord': Rule_Def.rew_ord';
4.14 + val dummy_ord: Rule_Def.rew_ord_
4.15 + val e_rew_ord: Rule_Def.rew_ord_
4.16 +
4.17 + type rew_ord = Rule_Def.rew_ord
4.18 + val e_rew_ordX: rew_ord
4.19 +
4.20 + type rew_ord' = Rule_Def.rew_ord'
4.21 + val rew_ord': (rew_ord' * (subst -> term * term -> bool)) list Unsynchronized.ref
4.22 + val assoc_rew_ord: string -> subst -> term * term -> bool
4.23 +end
4.24 +
4.25 +(**)
4.26 +structure Rewrite_Ord(**): REWRITE_ORDER(**) =
4.27 +struct
4.28 +(**)
4.29 +
4.30 +val e_rew_ord' = "e_rew_ord" : Rule_Def.rew_ord';
4.31 +type rew_ord_ = Rule_Def.rew_ord_;
4.32 +type subst = (term * term) list;
4.33 +fun dummy_ord (_: subst) (_: term, _: term) = true;
4.34 +val e_rew_ord_ = dummy_ord;
4.35 +
4.36 +type rew_ord = (*rew_ord' * rew_ord_;*) Rule_Def.rew_ord
4.37 +val e_rew_ord = dummy_ord; (* TODO.WN071231 clarify identifiers..e_rew_ordX*)
4.38 +val e_rew_ordX = (e_rew_ord', e_rew_ord_)
4.39 +
4.40 +type rew_ord' = Rule_Def.rew_ord'
4.41 +(* rewrite orders, also stored in 'type met' and type 'and rls'
4.42 + The association list is required for 'rewrite.."rew_ord"..' *)
4.43 +val rew_ord' = Unsynchronized.ref
4.44 + ([("e_rew_ord", e_rew_ord), ("dummy_ord", dummy_ord)]
4.45 + : (rew_ord' * (* the key for the association list *)
4.46 + (subst (* the bound variables - they get high order*)
4.47 + -> (term * term) (* (t1, t2) to be compared *)
4.48 + -> bool)) (* if t1 <= t2 then true else false *)
4.49 + list); (* association list *)
4.50 +fun assoc' ([], key) = raise ERROR ("ME_Isa: \"" ^ key ^ "\" not known")
4.51 + | assoc' ((keyi, xi) :: pairs, key) =
4.52 + if key = keyi then SOME xi else assoc' (pairs, key);
4.53 +fun assoc_rew_ord ro = ((the o assoc') (! rew_ord',ro))
4.54 + handle _ => raise ERROR ("ME_Isa: rew_ord '" ^ ro ^ "' not in system");
4.55 +
4.56 +end
4.57 \ No newline at end of file
5.1 --- a/src/Tools/isac/CalcElements/rule-def.sml Wed Apr 08 15:50:03 2020 +0200
5.2 +++ b/src/Tools/isac/CalcElements/rule-def.sml Wed Apr 08 16:56:47 2020 +0200
5.3 @@ -46,13 +46,6 @@
5.4 struct
5.5 (**)
5.6
5.7 -
5.8 -(* eval function calling sml code during rewriting.
5.9 -Unifying "type cal" and "type calc" would make Lucas-Interpretation more efficient,
5.10 - see "fun rule2stac": instead of
5.11 - Num_Calc: calID * eval_fn -> rule
5.12 - would be better
5.13 - Num_Calc: prog_calcID * (calID * eval_fn)) -> rule*)
5.14 type eval_fn = (string -> term -> theory -> (string * term) option);
5.15
5.16 type rew_ord' = string;
6.1 --- a/src/Tools/isac/CalcElements/rule-set.sml Wed Apr 08 15:50:03 2020 +0200
6.2 +++ b/src/Tools/isac/CalcElements/rule-set.sml Wed Apr 08 16:56:47 2020 +0200
6.3 @@ -10,7 +10,7 @@
6.4 eqtype identifier
6.5
6.6 val rep: T -> {calc: Rule_Def.calc list, erls: T, errpats: Rule_Def.errpatID list, id: string,
6.7 - preconds: term list, rew_ord: Rule_Def.rew_ord, rules: Rule_Def.rule list, scr: Rule_Def.program, srls: T}
6.8 + preconds: term list, rew_ord: Rewrite_Ord.rew_ord, rules: Rule_Def.rule list, scr: Rule_Def.program, srls: T}
6.9
6.10 val append_rules: string -> T -> Rule_Def.rule list -> T
6.11 val keep_unique_rules: string -> T -> Rule_Def.rule list -> T
7.1 --- a/src/Tools/isac/CalcElements/rule.sml Wed Apr 08 15:50:03 2020 +0200
7.2 +++ b/src/Tools/isac/CalcElements/rule.sml Wed Apr 08 16:56:47 2020 +0200
7.3 @@ -2,11 +2,6 @@
7.4 Author: Walther Neuper 2018
7.5 (c) copyright due to lincense terms
7.6
7.7 -TODO: this theory should vanish; vaious stuff awaits separation.
7.8 -* rew_ord: this also needs to
7.9 -* ThmC
7.10 -* TheoryC
7.11 -* ...
7.12 Some stuff waits for later rounds of restructuring, e.g. Rule.e_term
7.13 *)
7.14
7.15 @@ -18,16 +13,7 @@
7.16 eqtype cterm'
7.17 type subst = (term * term) list
7.18
7.19 -(*/------- to rewrite-ord.sml ---------------------\*)
7.20 - val dummy_ord: Rule_Def.rew_ord_
7.21 - val e_rew_ord_: Rule_Def.rew_ord_
7.22 - val e_rew_ord: Rule_Def.rew_ord_
7.23 - val e_rew_ordX: Rule_Def.rew_ord
7.24 - val rew_ord': (Rule_Def.rew_ord' * (subst -> term * term -> bool)) list Unsynchronized.ref
7.25 - val assoc_rew_ord: string -> subst -> term * term -> bool
7.26 -(*\------- to rewrite-ord.sml ---------------------/*)
7.27 -
7.28 - eqtype errpatID (*..from Rule_Def*)
7.29 + eqtype errpatID
7.30 type errpat = errpatID * term list * thm list
7.31
7.32 val scr2str: program -> string
7.33 @@ -40,12 +26,12 @@
7.34 val termopt2str: term option -> string (* shift up to Unparse *)
7.35 val terms2str: term list -> string (* shift up to Unparse *)
7.36 val terms2strs: term list -> string list
7.37 - val term_to_string'': ThyC.thyID -> term -> string (* shift up to Unparse *)
7.38 + val term_to_string'': ThyC.thyID -> term -> string (* shift up to Unparse *)
7.39 val term_to_string''': theory -> term -> string (* shift up to Unparse *)
7.40 val t2str: theory -> term -> string
7.41 val ts2str: theory -> term list -> string (* shift up to Unparse *)
7.42 val string_of_typ: typ -> string (* shift up to Unparse *)
7.43 - val string_of_typ_thy: ThyC.thyID -> typ -> string (* shift up to Unparse *)
7.44 + val string_of_typ_thy: ThyC.thyID -> typ -> string (* shift up to Unparse *)
7.45
7.46 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
7.47 val terms2str': term list -> string (* shift up to Unparse *)
7.48 @@ -80,29 +66,6 @@
7.49 type cterm' = string;
7.50 type subst = (term * term) list;
7.51
7.52 -val e_rew_ord' = "e_rew_ord" : Rule_Def.rew_ord';
7.53 -type rew_ord_ = Rule_Def.rew_ord_;
7.54 -fun dummy_ord (_: subst) (_: term, _: term) = true;
7.55 -val e_rew_ord_ = dummy_ord;
7.56 -type rew_ord = (*rew_ord' * rew_ord_;*) Rule_Def.rew_ord (*..from Rule_Def*)
7.57 -val e_rew_ord = dummy_ord; (* TODO.WN071231 clarify identifiers..e_rew_ordX*)
7.58 -val e_rew_ordX = (e_rew_ord', e_rew_ord_);
7.59 -
7.60 -(* rewrite orders, also stored in 'type met' and type 'and rls'
7.61 - The association list is required for 'rewrite.."rew_ord"..' *)
7.62 -val rew_ord' = Unsynchronized.ref
7.63 - ([("e_rew_ord", e_rew_ord), ("dummy_ord", dummy_ord)]
7.64 - : (Rule_Def.rew_ord' * (* the key for the association list *)
7.65 - (subst (* the bound variables - they get high order*)
7.66 - -> (term * term) (* (t1, t2) to be compared *)
7.67 - -> bool)) (* if t1 <= t2 then true else false *)
7.68 - list); (* association list *)
7.69 -fun assoc' ([], key) = raise ERROR ("ME_Isa: \"" ^ key ^ "\" not known")
7.70 - | assoc' ((keyi, xi) :: pairs, key) =
7.71 - if key = keyi then SOME xi else assoc' (pairs, key);
7.72 -fun assoc_rew_ord ro = ((the o assoc') (! rew_ord',ro))
7.73 - handle _ => raise ERROR ("ME_Isa: rew_ord '" ^ ro ^ "' not in system");
7.74 -
7.75 fun term_to_string' ctxt t =
7.76 let
7.77 val ctxt' = Config.put show_markup false ctxt
8.1 --- a/src/Tools/isac/Interpret/error-pattern.sml Wed Apr 08 15:50:03 2020 +0200
8.2 +++ b/src/Tools/isac/Interpret/error-pattern.sml Wed Apr 08 16:56:47 2020 +0200
8.3 @@ -10,7 +10,7 @@
8.4 val is_exactly_equal : Calc.T -> string -> string * Tactic.input
8.5 val concat_deriv : 'a * ((term * term) list -> term * term -> bool) ->
8.6 Rule_Set.T -> Rule.rule list -> term -> term -> bool * (term * Rule.rule * (term * term list)) list
8.7 - val mk_tacis: Rule_Def.rew_ord' * 'a -> Rule_Set.T -> term * Rule.rule * (term * term list) -> Tactic.input * Tactic.T * (Pos.pos' * (Istate.T * Proof.context))
8.8 + val mk_tacis: Rewrite_Ord.rew_ord' * 'a -> Rule_Set.T -> term * Rule.rule * (term * term list) -> Tactic.input * Tactic.T * (Pos.pos' * (Istate.T * Proof.context))
8.9 val fetchErrorpatterns : Tactic.input -> Rule.errpatID list
8.10 val check_for :
8.11 term * term ->
8.12 @@ -97,7 +97,7 @@
8.13 fun check_err_patt (res, inf) subst (errpatID, pat) rls =
8.14 let
8.15 val (res', _, _, rewritten) =
8.16 - Rewrite.rew_sub (ThyC.Isac()) 1 subst Rule.e_rew_ord Rule_Set.empty false [] (HOLogic.Trueprop $ pat) res;
8.17 + Rewrite.rew_sub (ThyC.Isac()) 1 subst Rewrite_Ord.e_rew_ord Rule_Set.empty false [] (HOLogic.Trueprop $ pat) res;
8.18 in
8.19 if rewritten then
8.20 let
8.21 @@ -134,7 +134,7 @@
8.22 fun get_fillform (subs_opt, subst) (thm, form) errpatID (fillpatID, pat, erpaID) =
8.23 let
8.24 val (form', _, _, rewritten) =
8.25 - Rewrite.rew_sub (ThyC.Isac()) 1 subst Rule.e_rew_ord Rule_Set.empty false [] (HOLogic.Trueprop $ pat) form;
8.26 + Rewrite.rew_sub (ThyC.Isac()) 1 subst Rewrite_Ord.e_rew_ord Rule_Set.empty false [] (HOLogic.Trueprop $ pat) form;
8.27 in (*the fillpat of the thm must be dedicated to errpatID*)
8.28 if errpatID = erpaID andalso rewritten then
8.29 SOME (fillpatID, HOLogic.mk_eq (form, form'), thm, subs_opt)
9.1 --- a/src/Tools/isac/Interpret/rewtools.sml Wed Apr 08 15:50:03 2020 +0200
9.2 +++ b/src/Tools/isac/Interpret/rewtools.sml Wed Apr 08 16:56:47 2020 +0200
9.3 @@ -18,10 +18,10 @@
9.4 | ContRls of {applto: term, asms: term list, result: term, rls: Celem.guh, thyID: ThyC.thyID}
9.5 | ContRlsInst of {applto: term, asms: term list, bdvs: Rule.subst, result: term, rls: Celem.guh, thyID: ThyC.thyID}
9.6 | ContThm of {applat: term, applto: term, asmrls: Rule_Set.identifier, asms: (term * term) list,
9.7 - lhs: term * term, resasms: term list, result: term, reword: Rule_Def.rew_ord', rhs: term * term,
9.8 + lhs: term * term, resasms: term list, result: term, reword: Rewrite_Ord.rew_ord', rhs: term * term,
9.9 thm: Celem.guh, thyID: ThyC.thyID}
9.10 | ContThmInst of {applat: term, applto: term, asmrls: Rule_Set.identifier, asms: (term * term) list,
9.11 - bdvs: Rule.subst, lhs: term * term, resasms: term list, result: term, reword: Rule_Def.rew_ord',
9.12 + bdvs: Rule.subst, lhs: term * term, resasms: term list, result: term, reword: Rewrite_Ord.rew_ord',
9.13 rhs: term * term, thm: Celem.guh, thminst: term, thyID: ThyC.thyID}
9.14 | EContThy
9.15 val guh2filename : Celem.guh -> Celem.filename
9.16 @@ -276,7 +276,7 @@
9.17 thm : Celem.guh, (* theorem in the context .*)
9.18 applto : term, (* applied to formula ... .*)
9.19 applat : term, (* ... with lhs inserted .*)
9.20 - reword : Rule_Def.rew_ord', (* order used for rewrite .*)
9.21 + reword : Rewrite_Ord.rew_ord', (* order used for rewrite .*)
9.22 asms : (term (* asumption instantiated .*)
9.23 * term) list, (* asumption evaluated .*)
9.24 lhs : term (* lhs of the theorem ... #*)
9.25 @@ -294,7 +294,7 @@
9.26 thminst : term, (*... theorem instantiated .*)
9.27 applto : term, (*applied to formula ... .*)
9.28 applat : term, (*... with lhs inserted .*)
9.29 - reword : Rule_Def.rew_ord', (*order used for rewrite .*)
9.30 + reword : Rewrite_Ord.rew_ord', (*order used for rewrite .*)
9.31 asms : (term (*asumption instantiated .*)
9.32 * term) list, (*asumption evaluated .*)
9.33 lhs : term (*lhs of the theorem ... #*)
9.34 @@ -451,7 +451,7 @@
9.35
9.36 (* try if a rewrite-rule is applicable to a given formula;
9.37 in case of rule-sets (recursivley) collect all _atomic_ rewrites *)
9.38 -fun try_rew thy ((_, ro) : Rule_Def.rew_ord) erls (subst : Rule.subst) f (thm' as Rule.Thm (_, thm)) =
9.39 +fun try_rew thy ((_, ro) : Rewrite_Ord.rew_ord) erls (subst : Rule.subst) f (thm' as Rule.Thm (_, thm)) =
9.40 if Auto_Prog.contains_bdv thm
9.41 then case Rewrite.rewrite_inst_ thy ro erls false subst thm f of
9.42 SOME _ => [Tactic.rule2tac thy subst thm']
9.43 @@ -479,11 +479,11 @@
9.44 (* decide if a tactic is applicable to a given formula;
9.45 in case of Rewrite_Set* go down to _atomic_ rewrite-tactics *)
9.46 fun atomic_appl_tacs thy _ _ f (Tactic.Calculate scrID) =
9.47 - try_rew thy Rule.e_rew_ordX Rule_Set.empty [] f (Rule.Num_Calc (assoc_calc' thy scrID |> snd))
9.48 + try_rew thy Rewrite_Ord.e_rew_ordX Rule_Set.empty [] f (Rule.Num_Calc (assoc_calc' thy scrID |> snd))
9.49 | atomic_appl_tacs thy ro erls f (Tactic.Rewrite thm'') =
9.50 - try_rew thy (ro, Rule.assoc_rew_ord ro) erls [] f (Rule.Thm thm'')
9.51 + try_rew thy (ro, Rewrite_Ord.assoc_rew_ord ro) erls [] f (Rule.Thm thm'')
9.52 | atomic_appl_tacs thy ro erls f (Tactic.Rewrite_Inst (subs, thm'')) =
9.53 - try_rew thy (ro, Rule.assoc_rew_ord ro) erls (Selem.subs2subst thy subs) f (Rule.Thm thm'')
9.54 + try_rew thy (ro, Rewrite_Ord.assoc_rew_ord ro) erls (Selem.subs2subst thy subs) f (Rule.Thm thm'')
9.55
9.56 | atomic_appl_tacs thy _ _ f (Tactic.Rewrite_Set rls') =
9.57 filter_appl_rews thy [] f (assoc_rls rls')
10.1 --- a/src/Tools/isac/Knowledge/Base_Tools.thy Wed Apr 08 15:50:03 2020 +0200
10.2 +++ b/src/Tools/isac/Knowledge/Base_Tools.thy Wed Apr 08 16:56:47 2020 +0200
10.3 @@ -46,12 +46,12 @@
10.4 fun term_ordI (_: Rule.subst) uv = Term_Ord.term_ord uv;
10.5 end;
10.6 \<close> ML \<open>
10.7 -(*TODO.WN0509 reduce ids: tless_true = e_rew_ord' = Rule.e_rew_ord = Rule.dummy_ord*)
10.8 -val tless_true = Rule.dummy_ord;
10.9 -Rule.rew_ord' := overwritel (! Rule.rew_ord', (*<<<---- use KEStore.xxx here, too*)
10.10 +(*TODO.WN0509 reduce ids: tless_true = e_rew_ord' = Rewrite_Ord.e_rew_ord = Rewrite_Ord.dummy_ord*)
10.11 +val tless_true = Rewrite_Ord.dummy_ord;
10.12 +Rewrite_Ord.rew_ord' := overwritel (! Rewrite_Ord.rew_ord', (*<<<---- use KEStore.xxx here, too*)
10.13 [("tless_true", tless_true),
10.14 ("e_rew_ord'", tless_true),
10.15 - ("dummy_ord", Rule.dummy_ord)]);
10.16 + ("dummy_ord", Rewrite_Ord.dummy_ord)]);
10.17 \<close>
10.18
10.19 subsection \<open>rule-sets\<close>
11.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Wed Apr 08 15:50:03 2020 +0200
11.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Wed Apr 08 16:56:47 2020 +0200
11.3 @@ -161,7 +161,7 @@
11.4 (**)
11.5 end;
11.6 (**)
11.7 -Rule.rew_ord' := overwritel (! Rule.rew_ord',
11.8 +Rewrite_Ord.rew_ord' := overwritel (! Rewrite_Ord.rew_ord',
11.9 [("ord_simplify_System", ord_simplify_System false thy)
11.10 ]);
11.11 \<close>
11.12 @@ -195,7 +195,7 @@
11.13 #2 NOT using common_nominator_p .*)
11.14 val norm_System_noadd_fractions =
11.15 Rule_Def.Repeat {id = "norm_System_noadd_fractions", preconds = [],
11.16 - rew_ord = ("dummy_ord",Rule.dummy_ord),
11.17 + rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
11.18 erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
11.19 rules = [(*sequence given by operator precedence*)
11.20 Rule.Rls_ discard_minus,
11.21 @@ -216,7 +216,7 @@
11.22 *1* using 'ord_simplify_System' in 'order_add_mult_System'.*)
11.23 val norm_System =
11.24 Rule_Def.Repeat {id = "norm_System", preconds = [],
11.25 - rew_ord = ("dummy_ord",Rule.dummy_ord),
11.26 + rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
11.27 erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
11.28 rules = [(*sequence given by operator precedence*)
11.29 Rule.Rls_ discard_minus,
11.30 @@ -244,7 +244,7 @@
11.31 analoguous to simplify_Integral .*)
11.32 val simplify_System_parenthesized =
11.33 Rule_Set.Seqence {id = "simplify_System_parenthesized", preconds = []:term list,
11.34 - rew_ord = ("dummy_ord", Rule.dummy_ord),
11.35 + rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
11.36 erls = Atools_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
11.37 rules = [Rule.Thm ("distrib_right",TermC.num_str @{thm distrib_right}),
11.38 (*"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"*)
11.39 @@ -269,7 +269,7 @@
11.40 (*TODO.WN051031 ^^^^^^^^^^ should be in EACH rls contained *)
11.41 val simplify_System =
11.42 Rule_Set.Seqence {id = "simplify_System", preconds = []:term list,
11.43 - rew_ord = ("dummy_ord", Rule.dummy_ord),
11.44 + rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
11.45 erls = Atools_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
11.46 rules = [Rule.Rls_ norm_Rational,
11.47 Rule.Rls_ (*order_add_mult_in*) norm_System (**1**),
11.48 @@ -289,7 +289,7 @@
11.49 ML \<open>
11.50 val isolate_bdvs =
11.51 Rule_Def.Repeat {id="isolate_bdvs", preconds = [],
11.52 - rew_ord = ("e_rew_ord", Rule.e_rew_ord),
11.53 + rew_ord = ("e_rew_ord", Rewrite_Ord.e_rew_ord),
11.54 erls = Rule_Set.append_rules "erls_isolate_bdvs" Rule_Set.empty
11.55 [(Rule.Num_Calc ("EqSystem.occur'_exactly'_in",
11.56 eval_occur_exactly_in
11.57 @@ -305,7 +305,7 @@
11.58 ML \<open>
11.59 val isolate_bdvs_4x4 =
11.60 Rule_Def.Repeat {id="isolate_bdvs_4x4", preconds = [],
11.61 - rew_ord = ("e_rew_ord", Rule.e_rew_ord),
11.62 + rew_ord = ("e_rew_ord", Rewrite_Ord.e_rew_ord),
11.63 erls = Rule_Set.append_rules
11.64 "erls_isolate_bdvs_4x4" Rule_Set.empty
11.65 [Rule.Num_Calc ("EqSystem.occur'_exactly'_in",
11.66 @@ -339,9 +339,9 @@
11.67
11.68 val prls_triangular =
11.69 Rule_Def.Repeat {id="prls_triangular", preconds = [],
11.70 - rew_ord = ("e_rew_ord", Rule.e_rew_ord),
11.71 + rew_ord = ("e_rew_ord", Rewrite_Ord.e_rew_ord),
11.72 erls = Rule_Def.Repeat {id="erls_prls_triangular", preconds = [],
11.73 - rew_ord = ("e_rew_ord", Rule.e_rew_ord),
11.74 + rew_ord = ("e_rew_ord", Rewrite_Ord.e_rew_ord),
11.75 erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
11.76 rules = [(*for precond NTH_CONS ...*)
11.77 Rule.Num_Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
11.78 @@ -368,9 +368,9 @@
11.79 more similarity to prls_triangular desirable*)
11.80 val prls_triangular4 =
11.81 Rule_Def.Repeat {id="prls_triangular4", preconds = [],
11.82 - rew_ord = ("e_rew_ord", Rule.e_rew_ord),
11.83 + rew_ord = ("e_rew_ord", Rewrite_Ord.e_rew_ord),
11.84 erls = Rule_Def.Repeat {id="erls_prls_triangular4", preconds = [],
11.85 - rew_ord = ("e_rew_ord", Rule.e_rew_ord),
11.86 + rew_ord = ("e_rew_ord", Rewrite_Ord.e_rew_ord),
11.87 erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
11.88 rules = [(*for precond NTH_CONS ...*)
11.89 Rule.Num_Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
12.1 --- a/src/Tools/isac/Knowledge/Integrate.thy Wed Apr 08 15:50:03 2020 +0200
12.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy Wed Apr 08 16:56:47 2020 +0200
12.3 @@ -163,12 +163,12 @@
12.4 (*.for simplify_Integral adapted from 'norm_Rational_rls'.*)
12.5 val norm_Rational_rls_noadd_fractions =
12.6 Rule_Def.Repeat {id = "norm_Rational_rls_noadd_fractions", preconds = [],
12.7 - rew_ord = ("dummy_ord",Rule.dummy_ord),
12.8 + rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
12.9 erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
12.10 rules = [(*Rule.Rls_ add_fractions_p_rls,!!!*)
12.11 Rule.Rls_ (*rat_mult_div_pow original corrected WN051028*)
12.12 (Rule_Def.Repeat {id = "rat_mult_div_pow", preconds = [],
12.13 - rew_ord = ("dummy_ord",Rule.dummy_ord),
12.14 + rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
12.15 erls = (*FIXME.WN051028 Rule_Set.empty,*)
12.16 Rule_Set.append_rules "Rule_Set.empty-is_polyexp" Rule_Set.empty
12.17 [Rule.Num_Calc ("Poly.is'_polyexp",
12.18 @@ -207,7 +207,7 @@
12.19 (*.for simplify_Integral adapted from 'norm_Rational'.*)
12.20 val norm_Rational_noadd_fractions =
12.21 Rule_Set.Seqence {id = "norm_Rational_noadd_fractions", preconds = [],
12.22 - rew_ord = ("dummy_ord",Rule.dummy_ord),
12.23 + rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
12.24 erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
12.25 rules = [Rule.Rls_ discard_minus,
12.26 Rule.Rls_ rat_mult_poly,(* removes double fractions like a/b/c *)
12.27 @@ -241,7 +241,7 @@
12.28 ];
12.29 val simplify_Integral =
12.30 Rule_Set.Seqence {id = "simplify_Integral", preconds = []:term list,
12.31 - rew_ord = ("dummy_ord", Rule.dummy_ord),
12.32 + rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
12.33 erls = Atools_erls, srls = Rule_Set.Empty,
12.34 calc = [], errpatts = [],
12.35 rules = [Rule.Thm ("distrib_right", TermC.num_str @{thm distrib_right}),
12.36 @@ -267,7 +267,7 @@
12.37 THIS IS KEPT FOR COMPARISON ............................................
12.38 * val simplify_Integral = prep_rls'(
12.39 * Rule_Set.Seqence {id = "", preconds = []:term list,
12.40 -* rew_ord = ("dummy_ord", Rule.dummy_ord),
12.41 +* rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
12.42 * erls = Atools_erls, srls = Rule_Set.Empty,
12.43 * calc = [], (*asm_thm = [],*)
12.44 * rules = [Rule.Rls_ expand_poly,
13.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Wed Apr 08 15:50:03 2020 +0200
13.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Wed Apr 08 16:56:47 2020 +0200
13.3 @@ -27,7 +27,7 @@
13.4
13.5 ML \<open>
13.6 val inverse_z = prep_rls'(
13.7 - Rule_Def.Repeat {id = "inverse_z", preconds = [], rew_ord = ("dummy_ord",Rule.dummy_ord),
13.8 + Rule_Def.Repeat {id = "inverse_z", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
13.9 erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
13.10 rules =
13.11 [
14.1 --- a/src/Tools/isac/Knowledge/LinEq.thy Wed Apr 08 15:50:03 2020 +0200
14.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy Wed Apr 08 16:56:47 2020 +0200
14.3 @@ -94,7 +94,7 @@
14.4 (*isolate the bound variable in an linear equation; 'bdv' is a meta-constant*)
14.5 val LinEq_simplify = prep_rls'(
14.6 Rule_Def.Repeat {id = "LinEq_simplify", preconds = [],
14.7 - rew_ord = ("e_rew_ord", Rule.e_rew_ord),
14.8 + rew_ord = ("e_rew_ord", Rewrite_Ord.e_rew_ord),
14.9 erls = LinEq_erls,
14.10 srls = Rule_Set.Empty,
14.11 calc = [], errpatts = [],
15.1 --- a/src/Tools/isac/Knowledge/Partial_Fractions.thy Wed Apr 08 15:50:03 2020 +0200
15.2 +++ b/src/Tools/isac/Knowledge/Partial_Fractions.thy Wed Apr 08 16:56:47 2020 +0200
15.3 @@ -106,7 +106,7 @@
15.4
15.5 ML \<open>
15.6 val ansatz_rls = prep_rls'(
15.7 - Rule_Def.Repeat {id = "ansatz_rls", preconds = [], rew_ord = ("dummy_ord",Rule.dummy_ord),
15.8 + Rule_Def.Repeat {id = "ansatz_rls", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
15.9 erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
15.10 rules =
15.11 [Rule.Thm ("ansatz_2nd_order",TermC.num_str @{thm ansatz_2nd_order}),
15.12 @@ -115,7 +115,7 @@
15.13 scr = Rule.EmptyScr});
15.14
15.15 val equival_trans = prep_rls'(
15.16 - Rule_Def.Repeat {id = "equival_trans", preconds = [], rew_ord = ("dummy_ord",Rule.dummy_ord),
15.17 + Rule_Def.Repeat {id = "equival_trans", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
15.18 erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
15.19 rules =
15.20 [Rule.Thm ("equival_trans_2nd_order",TermC.num_str @{thm equival_trans_2nd_order}),
15.21 @@ -124,7 +124,7 @@
15.22 scr = Rule.EmptyScr});
15.23
15.24 val multiply_ansatz = prep_rls'(
15.25 - Rule_Def.Repeat {id = "multiply_ansatz", preconds = [], rew_ord = ("dummy_ord",Rule.dummy_ord),
15.26 + Rule_Def.Repeat {id = "multiply_ansatz", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
15.27 erls = Rule_Set.Empty,
15.28 srls = Rule_Set.Empty, calc = [], errpatts = [],
15.29 rules =
16.1 --- a/src/Tools/isac/Knowledge/Poly.thy Wed Apr 08 15:50:03 2020 +0200
16.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Wed Apr 08 16:56:47 2020 +0200
16.3 @@ -510,7 +510,7 @@
16.4
16.5 end;(*local*)
16.6
16.7 -Rule.rew_ord' := overwritel (! Rule.rew_ord', (* TODO: make analogous to KEStore_Elems.add_mets *)
16.8 +Rewrite_Ord.rew_ord' := overwritel (! Rewrite_Ord.rew_ord', (* TODO: make analogous to KEStore_Elems.add_mets *)
16.9 [("termlessI", termlessI), ("ord_make_polynomial", ord_make_polynomial false thy)]);
16.10 \<close>
16.11
16.12 @@ -669,7 +669,7 @@
16.13 \<close>
16.14 ML \<open>
16.15 val expand =
16.16 - Rule_Def.Repeat {id = "expand", preconds = [], rew_ord = ("dummy_ord", Rule.dummy_ord),
16.17 + Rule_Def.Repeat {id = "expand", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
16.18 erls = Rule_Set.empty,srls = Rule_Set.Empty, calc = [], errpatts = [],
16.19 rules = [Rule.Thm ("distrib_right" , TermC.num_str @{thm distrib_right}),
16.20 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
16.21 @@ -678,7 +678,7 @@
16.22 ], scr = Rule.EmptyScr};
16.23
16.24 val discard_minus =
16.25 - Rule_Def.Repeat {id = "discard_minus", preconds = [], rew_ord = ("dummy_ord", Rule.dummy_ord),
16.26 + Rule_Def.Repeat {id = "discard_minus", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
16.27 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
16.28 rules =
16.29 [Rule.Thm ("real_diff_minus", TermC.num_str @{thm real_diff_minus}),
16.30 @@ -689,7 +689,7 @@
16.31
16.32 val expand_poly_ =
16.33 Rule_Def.Repeat{id = "expand_poly_", preconds = [],
16.34 - rew_ord = ("dummy_ord", Rule.dummy_ord),
16.35 + rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
16.36 erls = Rule_Set.empty,srls = Rule_Set.Empty,
16.37 calc = [], errpatts = [],
16.38 rules =
16.39 @@ -723,7 +723,7 @@
16.40
16.41 val expand_poly_rat_ =
16.42 Rule_Def.Repeat{id = "expand_poly_rat_", preconds = [],
16.43 - rew_ord = ("dummy_ord", Rule.dummy_ord),
16.44 + rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
16.45 erls = Rule_Set.append_rules "Rule_Set.empty-is_polyexp" Rule_Set.empty
16.46 [Rule.Num_Calc ("Poly.is'_polyexp", eval_is_polyexp "")
16.47 ],
16.48 @@ -761,7 +761,7 @@
16.49
16.50 val simplify_power_ =
16.51 Rule_Def.Repeat{id = "simplify_power_", preconds = [],
16.52 - rew_ord = ("dummy_ord", Rule.dummy_ord),
16.53 + rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
16.54 erls = Rule_Set.empty, srls = Rule_Set.Empty,
16.55 calc = [], errpatts = [],
16.56 rules = [(*MG: Reihenfolge der folgenden 2 Rule.Thm muss so bleiben, wegen
16.57 @@ -796,7 +796,7 @@
16.58
16.59 val calc_add_mult_pow_ =
16.60 Rule_Def.Repeat{id = "calc_add_mult_pow_", preconds = [],
16.61 - rew_ord = ("dummy_ord", Rule.dummy_ord),
16.62 + rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
16.63 erls = Atools_erls(*erls3.4.03*),srls = Rule_Set.Empty,
16.64 calc = [("PLUS" , ("Groups.plus_class.plus", (**)eval_binop "#add_")),
16.65 ("TIMES" , ("Groups.times_class.times", (**)eval_binop "#mult_")),
16.66 @@ -810,7 +810,7 @@
16.67
16.68 val reduce_012_mult_ =
16.69 Rule_Def.Repeat{id = "reduce_012_mult_", preconds = [],
16.70 - rew_ord = ("dummy_ord", Rule.dummy_ord),
16.71 + rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
16.72 erls = Rule_Set.empty,srls = Rule_Set.Empty,
16.73 calc = [], errpatts = [],
16.74 rules = [(* MG: folgende Rule.Thm müssen hier stehen bleiben: *)
16.75 @@ -826,7 +826,7 @@
16.76
16.77 val collect_numerals_ =
16.78 Rule_Def.Repeat{id = "collect_numerals_", preconds = [],
16.79 - rew_ord = ("dummy_ord", Rule.dummy_ord),
16.80 + rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
16.81 erls = Atools_erls, srls = Rule_Set.Empty,
16.82 calc = [("PLUS" , ("Groups.plus_class.plus", (**)eval_binop "#add_"))
16.83 ], errpatts = [],
16.84 @@ -853,7 +853,7 @@
16.85
16.86 val reduce_012_ =
16.87 Rule_Def.Repeat{id = "reduce_012_", preconds = [],
16.88 - rew_ord = ("dummy_ord", Rule.dummy_ord),
16.89 + rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
16.90 erls = Rule_Set.empty,srls = Rule_Set.Empty, calc = [], errpatts = [],
16.91 rules = [Rule.Thm ("mult_1_left",TermC.num_str @{thm mult_1_left}),
16.92 (*"1 * z = z"*)
16.93 @@ -884,7 +884,7 @@
16.94
16.95 val expand_poly =
16.96 Rule_Def.Repeat{id = "expand_poly", preconds = [],
16.97 - rew_ord = ("dummy_ord", Rule.dummy_ord),
16.98 + rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
16.99 erls = Rule_Set.empty,srls = Rule_Set.Empty,
16.100 calc = [], errpatts = [],
16.101 (*asm_thm = [],*)
16.102 @@ -923,7 +923,7 @@
16.103
16.104 val simplify_power =
16.105 Rule_Def.Repeat{id = "simplify_power", preconds = [],
16.106 - rew_ord = ("dummy_ord", Rule.dummy_ord),
16.107 + rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
16.108 erls = Rule_Set.empty, srls = Rule_Set.Empty,
16.109 calc = [], errpatts = [],
16.110 rules = [Rule.Thm ("realpow_multI", TermC.num_str @{thm realpow_multI}),
16.111 @@ -947,7 +947,7 @@
16.112
16.113 val collect_numerals =
16.114 Rule_Def.Repeat{id = "collect_numerals", preconds = [],
16.115 - rew_ord = ("dummy_ord", Rule.dummy_ord),
16.116 + rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
16.117 erls = Atools_erls(*erls3.4.03*),srls = Rule_Set.Empty,
16.118 calc = [("PLUS" , ("Groups.plus_class.plus", (**)eval_binop "#add_")),
16.119 ("TIMES" , ("Groups.times_class.times", (**)eval_binop "#mult_")),
16.120 @@ -968,7 +968,7 @@
16.121 ], scr = Rule.EmptyScr};
16.122 val reduce_012 =
16.123 Rule_Def.Repeat{id = "reduce_012", preconds = [],
16.124 - rew_ord = ("dummy_ord", Rule.dummy_ord),
16.125 + rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
16.126 erls = Rule_Set.empty,srls = Rule_Set.Empty,
16.127 calc = [], errpatts = [],
16.128 rules = [Rule.Thm ("mult_1_left",TermC.num_str @{thm mult_1_left}),
16.129 @@ -1055,7 +1055,7 @@
16.130 which evaluates (the instantiated) "?p is_multUnordered" to true *)
16.131 [([TermC.parse_patt thy "?p is_multUnordered"],
16.132 TermC.parse_patt thy "?p :: real")],
16.133 - rew_ord = ("dummy_ord", Rule.dummy_ord),
16.134 + rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
16.135 erls = Rule_Set.append_rules "Rule_Set.empty-is_multUnordered" Rule_Set.empty
16.136 [Rule.Num_Calc ("Poly.is'_multUnordered",
16.137 eval_is_multUnordered "")],
16.138 @@ -1071,7 +1071,7 @@
16.139 attach_form = attach_form}};
16.140 val order_mult_rls_ =
16.141 Rule_Def.Repeat {id = "order_mult_rls_", preconds = [],
16.142 - rew_ord = ("dummy_ord", Rule.dummy_ord),
16.143 + rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
16.144 erls = Rule_Set.empty,srls = Rule_Set.Empty,
16.145 calc = [], errpatts = [],
16.146 rules = [Rule.Rls_ order_mult_
16.147 @@ -1095,7 +1095,7 @@
16.148 TermC.parse_patt @{theory} "?p :: real"
16.149 (*WN.18.6.03 also KEIN pattern, dieses erzeugt nur das Environment
16.150 fuer die Evaluation der Precondition "p is_addUnordered"*))],
16.151 - rew_ord = ("dummy_ord", Rule.dummy_ord),
16.152 + rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
16.153 erls = Rule_Set.append_rules "Rule_Set.empty-is_addUnordered" Rule_Set.empty(*MG: poly_erls*)
16.154 [Rule.Num_Calc ("Poly.is'_addUnordered", eval_is_addUnordered "")],
16.155 calc = [("PLUS" ,("Groups.plus_class.plus", (**)eval_binop "#add_")),
16.156 @@ -1111,7 +1111,7 @@
16.157
16.158 val order_add_rls_ =
16.159 Rule_Def.Repeat {id = "order_add_rls_", preconds = [],
16.160 - rew_ord = ("dummy_ord", Rule.dummy_ord),
16.161 + rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
16.162 erls = Rule_Set.empty,srls = Rule_Set.Empty,
16.163 calc = [], errpatts = [],
16.164 rules = [Rule.Rls_ order_add_
16.165 @@ -1131,7 +1131,7 @@
16.166 val make_polynomial(*MG.03, overwrites version from above,
16.167 previously 'make_polynomial_'*) =
16.168 Rule_Set.Seqence {id = "make_polynomial", preconds = []:term list,
16.169 - rew_ord = ("dummy_ord", Rule.dummy_ord),
16.170 + rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
16.171 erls = Atools_erls, srls = Rule_Set.Empty,calc = [], errpatts = [],
16.172 rules = [Rule.Rls_ discard_minus,
16.173 Rule.Rls_ expand_poly_,
16.174 @@ -1151,7 +1151,7 @@
16.175 ML \<open>
16.176 val norm_Poly(*=make_polynomial*) =
16.177 Rule_Set.Seqence {id = "norm_Poly", preconds = []:term list,
16.178 - rew_ord = ("dummy_ord", Rule.dummy_ord),
16.179 + rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
16.180 erls = Atools_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
16.181 rules = [Rule.Rls_ discard_minus,
16.182 Rule.Rls_ expand_poly_,
16.183 @@ -1174,7 +1174,7 @@
16.184 (* MG necessary for termination of norm_Rational(*_mg*) in Rational.ML*)
16.185 val make_rat_poly_with_parentheses =
16.186 Rule_Set.Seqence{id = "make_rat_poly_with_parentheses", preconds = []:term list,
16.187 - rew_ord = ("dummy_ord", Rule.dummy_ord),
16.188 + rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
16.189 erls = Atools_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
16.190 rules = [Rule.Rls_ discard_minus,
16.191 Rule.Rls_ expand_poly_rat_,(*ignors rationals*)
17.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Wed Apr 08 15:50:03 2020 +0200
17.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Wed Apr 08 16:56:47 2020 +0200
17.3 @@ -369,7 +369,7 @@
17.4
17.5 val cancel_leading_coeff = prep_rls'(
17.6 Rule_Def.Repeat {id = "cancel_leading_coeff", preconds = [],
17.7 - rew_ord = ("e_rew_ord",Rule.e_rew_ord),
17.8 + rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord),
17.9 erls = PolyEq_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
17.10 rules =
17.11 [Rule.Thm ("cancel_leading_coeff1",TermC.num_str @{thm cancel_leading_coeff1}),
17.12 @@ -392,7 +392,7 @@
17.13 ML\<open>
17.14 val complete_square = prep_rls'(
17.15 Rule_Def.Repeat {id = "complete_square", preconds = [],
17.16 - rew_ord = ("e_rew_ord",Rule.e_rew_ord),
17.17 + rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord),
17.18 erls = PolyEq_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
17.19 rules = [Rule.Thm ("complete_square1",TermC.num_str @{thm complete_square1}),
17.20 Rule.Thm ("complete_square2",TermC.num_str @{thm complete_square2}),
17.21 @@ -437,7 +437,7 @@
17.22 (*isolate the bound variable in an d0 equation; 'bdv' is a meta-constant*)
17.23 val d0_polyeq_simplify = prep_rls'(
17.24 Rule_Def.Repeat {id = "d0_polyeq_simplify", preconds = [],
17.25 - rew_ord = ("e_rew_ord",Rule.e_rew_ord),
17.26 + rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord),
17.27 erls = PolyEq_erls,
17.28 srls = Rule_Set.Empty,
17.29 calc = [], errpatts = [],
17.30 @@ -451,7 +451,7 @@
17.31 (*isolate the bound variable in an d1 equation; 'bdv' is a meta-constant*)
17.32 val d1_polyeq_simplify = prep_rls'(
17.33 Rule_Def.Repeat {id = "d1_polyeq_simplify", preconds = [],
17.34 - rew_ord = ("e_rew_ord",Rule.e_rew_ord),
17.35 + rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord),
17.36 erls = PolyEq_erls,
17.37 srls = Rule_Set.Empty,
17.38 calc = [], errpatts = [],
17.39 @@ -472,7 +472,7 @@
17.40 (* isolate the bound variable in an d2 equation with bdv only;
17.41 "bdv" is a meta-constant substituted for the "x" below by isac's rewriter. *)
17.42 val d2_polyeq_bdv_only_simplify = prep_rls'(
17.43 - Rule_Def.Repeat {id = "d2_polyeq_bdv_only_simplify", preconds = [], rew_ord = ("e_rew_ord",Rule.e_rew_ord),
17.44 + Rule_Def.Repeat {id = "d2_polyeq_bdv_only_simplify", preconds = [], rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord),
17.45 erls = PolyEq_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
17.46 rules =
17.47 [Rule.Thm ("d2_prescind1", TermC.num_str @{thm d2_prescind1}), (* ax+bx^2=0 -> x(a+bx)=0 *)
17.48 @@ -494,7 +494,7 @@
17.49 'bdv' is a meta-constant*)
17.50 val d2_polyeq_sq_only_simplify = prep_rls'(
17.51 Rule_Def.Repeat {id = "d2_polyeq_sq_only_simplify", preconds = [],
17.52 - rew_ord = ("e_rew_ord",Rule.e_rew_ord),
17.53 + rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord),
17.54 erls = PolyEq_erls,
17.55 srls = Rule_Set.Empty,
17.56 calc = [], errpatts = [],
17.57 @@ -521,7 +521,7 @@
17.58 'bdv' is a meta-constant*)
17.59 val d2_polyeq_pqFormula_simplify = prep_rls'(
17.60 Rule_Def.Repeat {id = "d2_polyeq_pqFormula_simplify", preconds = [],
17.61 - rew_ord = ("e_rew_ord",Rule.e_rew_ord), erls = PolyEq_erls,
17.62 + rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord), erls = PolyEq_erls,
17.63 srls = Rule_Set.Empty, calc = [], errpatts = [],
17.64 rules = [Rule.Thm("d2_pqformula1",TermC.num_str @{thm d2_pqformula1}),
17.65 (* q+px+ x^2=0 *)
17.66 @@ -567,7 +567,7 @@
17.67 'bdv' is a meta-constant*)
17.68 val d2_polyeq_abcFormula_simplify = prep_rls'(
17.69 Rule_Def.Repeat {id = "d2_polyeq_abcFormula_simplify", preconds = [],
17.70 - rew_ord = ("e_rew_ord",Rule.e_rew_ord), erls = PolyEq_erls,
17.71 + rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord), erls = PolyEq_erls,
17.72 srls = Rule_Set.Empty, calc = [], errpatts = [],
17.73 rules = [Rule.Thm("d2_abcformula1",TermC.num_str @{thm d2_abcformula1}),
17.74 (*c+bx+cx^2=0 *)
17.75 @@ -615,7 +615,7 @@
17.76 'bdv' is a meta-constant*)
17.77 val d2_polyeq_simplify = prep_rls'(
17.78 Rule_Def.Repeat {id = "d2_polyeq_simplify", preconds = [],
17.79 - rew_ord = ("e_rew_ord",Rule.e_rew_ord), erls = PolyEq_erls,
17.80 + rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord), erls = PolyEq_erls,
17.81 srls = Rule_Set.Empty, calc = [], errpatts = [],
17.82 rules = [Rule.Thm("d2_pqformula1",TermC.num_str @{thm d2_pqformula1}),
17.83 (* p+qx+ x^2=0 *)
17.84 @@ -675,7 +675,7 @@
17.85 (* isolate the bound variable in an d3 equation; 'bdv' is a meta-constant *)
17.86 val d3_polyeq_simplify = prep_rls'(
17.87 Rule_Def.Repeat {id = "d3_polyeq_simplify", preconds = [],
17.88 - rew_ord = ("e_rew_ord",Rule.e_rew_ord), erls = PolyEq_erls,
17.89 + rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord), erls = PolyEq_erls,
17.90 srls = Rule_Set.Empty, calc = [], errpatts = [],
17.91 rules =
17.92 [Rule.Thm("d3_reduce_equation1",TermC.num_str @{thm d3_reduce_equation1}),
17.93 @@ -748,7 +748,7 @@
17.94 (*isolate the bound variable in an d4 equation; 'bdv' is a meta-constant*)
17.95 val d4_polyeq_simplify = prep_rls'(
17.96 Rule_Def.Repeat {id = "d4_polyeq_simplify", preconds = [],
17.97 - rew_ord = ("e_rew_ord",Rule.e_rew_ord), erls = PolyEq_erls,
17.98 + rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord), erls = PolyEq_erls,
17.99 srls = Rule_Set.Empty, calc = [], errpatts = [],
17.100 rules =
17.101 [Rule.Thm("d4_sub_u1",TermC.num_str @{thm d4_sub_u1})
17.102 @@ -1255,7 +1255,7 @@
17.103 ML\<open>
17.104 val collect_bdv = prep_rls'(
17.105 Rule_Def.Repeat{id = "collect_bdv", preconds = [],
17.106 - rew_ord = ("dummy_ord", Rule.dummy_ord),
17.107 + rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
17.108 erls = Rule_Set.empty,srls = Rule_Set.Empty,
17.109 calc = [], errpatts = [],
17.110 rules = [Rule.Thm ("bdv_collect_1",TermC.num_str @{thm bdv_collect_1}),
17.111 @@ -1290,7 +1290,7 @@
17.112 according to knowledge/Poly.sml.*)
17.113 val make_polynomial_in = prep_rls'(
17.114 Rule_Set.Seqence {id = "make_polynomial_in", preconds = []:term list,
17.115 - rew_ord = ("dummy_ord", Rule.dummy_ord),
17.116 + rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
17.117 erls = Atools_erls, srls = Rule_Set.Empty,
17.118 calc = [], errpatts = [],
17.119 rules = [Rule.Rls_ expand_poly,
17.120 @@ -1326,7 +1326,7 @@
17.121 ML\<open>
17.122 val make_ratpoly_in = prep_rls'(
17.123 Rule_Set.Seqence {id = "make_ratpoly_in", preconds = []:term list,
17.124 - rew_ord = ("dummy_ord", Rule.dummy_ord),
17.125 + rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
17.126 erls = Atools_erls, srls = Rule_Set.Empty,
17.127 calc = [], errpatts = [],
17.128 rules = [Rule.Rls_ norm_Rational,
18.1 --- a/src/Tools/isac/Knowledge/PolyMinus.thy Wed Apr 08 15:50:03 2020 +0200
18.2 +++ b/src/Tools/isac/Knowledge/PolyMinus.thy Wed Apr 08 16:56:47 2020 +0200
18.3 @@ -192,7 +192,7 @@
18.4
18.5 val ordne_alphabetisch =
18.6 Rule_Def.Repeat{id = "ordne_alphabetisch", preconds = [],
18.7 - rew_ord = ("dummy_ord", Rule.dummy_ord), srls = Rule_Set.Empty, calc = [], errpatts = [],
18.8 + rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), srls = Rule_Set.Empty, calc = [], errpatts = [],
18.9 erls = erls_ordne_alphabetisch,
18.10 rules = [Rule.Thm ("tausche_plus",TermC.num_str @{thm tausche_plus}),
18.11 (*"b kleiner a ==> (b + a) = (a + b)"*)
18.12 @@ -214,7 +214,7 @@
18.13
18.14 val fasse_zusammen =
18.15 Rule_Def.Repeat{id = "fasse_zusammen", preconds = [],
18.16 - rew_ord = ("dummy_ord", Rule.dummy_ord),
18.17 + rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
18.18 erls = Rule_Set.append_rules "erls_fasse_zusammen" Rule_Set.empty
18.19 [Rule.Num_Calc ("Prog_Expr.is'_const", Prog_Expr.eval_const "#is_const_")],
18.20 srls = Rule_Set.Empty, calc = [], errpatts = [],
18.21 @@ -280,7 +280,7 @@
18.22
18.23 val verschoenere =
18.24 Rule_Def.Repeat{id = "verschoenere", preconds = [],
18.25 - rew_ord = ("dummy_ord", Rule.dummy_ord), srls = Rule_Set.Empty, calc = [], errpatts = [],
18.26 + rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), srls = Rule_Set.Empty, calc = [], errpatts = [],
18.27 erls = Rule_Set.append_rules "erls_verschoenere" Rule_Set.empty
18.28 [Rule.Num_Calc ("PolyMinus.kleiner", eval_kleiner "")],
18.29 rules = [Rule.Thm ("vorzeichen_minus_weg1",TermC.num_str @{thm vorzeichen_minus_weg1}),
18.30 @@ -311,7 +311,7 @@
18.31
18.32 val klammern_aufloesen =
18.33 Rule_Def.Repeat{id = "klammern_aufloesen", preconds = [],
18.34 - rew_ord = ("dummy_ord", Rule.dummy_ord), srls = Rule_Set.Empty, calc = [], errpatts = [], erls = Rule_Set.Empty,
18.35 + rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), srls = Rule_Set.Empty, calc = [], errpatts = [], erls = Rule_Set.Empty,
18.36 rules = [Rule.Thm ("sym_add_assoc",
18.37 TermC.num_str (@{thm add.assoc} RS @{thm sym})),
18.38 (*"a + (b + c) = (a + b) + c"*)
18.39 @@ -325,7 +325,7 @@
18.40
18.41 val klammern_ausmultiplizieren =
18.42 Rule_Def.Repeat{id = "klammern_ausmultiplizieren", preconds = [],
18.43 - rew_ord = ("dummy_ord", Rule.dummy_ord), srls = Rule_Set.Empty, calc = [], errpatts = [], erls = Rule_Set.Empty,
18.44 + rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), srls = Rule_Set.Empty, calc = [], errpatts = [], erls = Rule_Set.Empty,
18.45 rules = [Rule.Thm ("distrib_right" ,TermC.num_str @{thm distrib_right}),
18.46 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
18.47 Rule.Thm ("distrib_left",TermC.num_str @{thm distrib_left}),
18.48 @@ -342,7 +342,7 @@
18.49
18.50 val ordne_monome =
18.51 Rule_Def.Repeat{id = "ordne_monome", preconds = [],
18.52 - rew_ord = ("dummy_ord", Rule.dummy_ord), srls = Rule_Set.Empty, calc = [], errpatts = [],
18.53 + rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), srls = Rule_Set.Empty, calc = [], errpatts = [],
18.54 erls = Rule_Set.append_rules "erls_ordne_monome" Rule_Set.empty
18.55 [Rule.Num_Calc ("PolyMinus.kleiner", eval_kleiner ""),
18.56 Rule.Num_Calc ("Prog_Expr.is'_atom", Prog_Expr.eval_is_atom "")
19.1 --- a/src/Tools/isac/Knowledge/Rational.thy Wed Apr 08 15:50:03 2020 +0200
19.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Wed Apr 08 16:56:47 2020 +0200
19.3 @@ -391,7 +391,7 @@
19.4 (* evaluates conditions in calculate_Rational *)
19.5 val calc_rat_erls =
19.6 prep_rls'
19.7 - (Rule_Def.Repeat {id = "calc_rat_erls", preconds = [], rew_ord = ("dummy_ord", Rule.dummy_ord),
19.8 + (Rule_Def.Repeat {id = "calc_rat_erls", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
19.9 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
19.10 rules =
19.11 [Rule.Num_Calc ("HOL.eq", Prog_Expr.eval_equal "#equal_"),
19.12 @@ -405,7 +405,7 @@
19.13 need to have constants to be commuted together respectively *)
19.14 val calculate_Rational =
19.15 prep_rls' (Rule_Set.merge "calculate_Rational"
19.16 - (Rule_Def.Repeat {id = "divide", preconds = [], rew_ord = ("dummy_ord", Rule.dummy_ord),
19.17 + (Rule_Def.Repeat {id = "divide", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
19.18 erls = calc_rat_erls, srls = Rule_Set.Empty,
19.19 calc = [], errpatts = [],
19.20 rules =
19.21 @@ -603,7 +603,7 @@
19.22 ML \<open>
19.23 (*erls for calculate_Rational; make local with FIXX@ME result:term *term list*)
19.24 val powers_erls = prep_rls'(
19.25 - Rule_Def.Repeat {id = "powers_erls", preconds = [], rew_ord = ("dummy_ord",Rule.dummy_ord),
19.26 + Rule_Def.Repeat {id = "powers_erls", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
19.27 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
19.28 rules = [Rule.Num_Calc ("Prog_Expr.is'_atom", Prog_Expr.eval_is_atom "#is_atom_"),
19.29 Rule.Num_Calc ("Prog_Expr.is'_even", Prog_Expr.eval_is_even "#is_even_"),
19.30 @@ -617,7 +617,7 @@
19.31 (*.all powers over + distributed; atoms over * collected, other distributed
19.32 contains absolute minimum of thms for context in norm_Rational .*)
19.33 val powers = prep_rls'(
19.34 - Rule_Def.Repeat {id = "powers", preconds = [], rew_ord = ("dummy_ord",Rule.dummy_ord),
19.35 + Rule_Def.Repeat {id = "powers", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
19.36 erls = powers_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
19.37 rules = [Rule.Thm ("realpow_multI", TermC.num_str @{thm realpow_multI}),
19.38 (*"(r * s) ^^^ n = r ^^^ n * s ^^^ n"*)
19.39 @@ -650,7 +650,7 @@
19.40 (*.contains absolute minimum of thms for context in norm_Rational.*)
19.41 val rat_mult_divide = prep_rls'(
19.42 Rule_Def.Repeat {id = "rat_mult_divide", preconds = [],
19.43 - rew_ord = ("dummy_ord", Rule.dummy_ord),
19.44 + rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
19.45 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
19.46 rules = [Rule.Thm ("rat_mult",TermC.num_str @{thm rat_mult}),
19.47 (*(1)"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)
19.48 @@ -674,7 +674,7 @@
19.49
19.50 (*.contains absolute minimum of thms for context in norm_Rational.*)
19.51 val reduce_0_1_2 = prep_rls'(
19.52 - Rule_Def.Repeat{id = "reduce_0_1_2", preconds = [], rew_ord = ("dummy_ord", Rule.dummy_ord),
19.53 + Rule_Def.Repeat{id = "reduce_0_1_2", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
19.54 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
19.55 rules = [(*Rule.Thm ("divide_1",TermC.num_str @{thm divide_1}),
19.56 "?x / 1 = ?x" unnecess.for normalform*)
19.57 @@ -705,7 +705,7 @@
19.58 (*erls for calculate_Rational;
19.59 make local with FIXX@ME result:term *term list WN0609???SKMG*)
19.60 val norm_rat_erls = prep_rls'(
19.61 - Rule_Def.Repeat {id = "norm_rat_erls", preconds = [], rew_ord = ("dummy_ord",Rule.dummy_ord),
19.62 + Rule_Def.Repeat {id = "norm_rat_erls", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
19.63 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
19.64 rules = [Rule.Num_Calc ("Prog_Expr.is'_const", Prog_Expr.eval_const "#is_const_")
19.65 ], scr = Rule.EmptyScr});
19.66 @@ -714,7 +714,7 @@
19.67 (*040209: this version has been used by RL for his equations,
19.68 which is now replaced by MGs version "norm_Rational" below *)
19.69 val norm_Rational_min = prep_rls'(
19.70 - Rule_Def.Repeat {id = "norm_Rational_min", preconds = [], rew_ord = ("dummy_ord",Rule.dummy_ord),
19.71 + Rule_Def.Repeat {id = "norm_Rational_min", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
19.72 erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
19.73 rules = [(*sequence given by operator precedence*)
19.74 Rule.Rls_ discard_minus,
19.75 @@ -731,7 +731,7 @@
19.76
19.77 val norm_Rational_parenthesized = prep_rls'(
19.78 Rule_Set.Seqence {id = "norm_Rational_parenthesized", preconds = []:term list,
19.79 - rew_ord = ("dummy_ord", Rule.dummy_ord),
19.80 + rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
19.81 erls = Atools_erls, srls = Rule_Set.Empty,
19.82 calc = [], errpatts = [],
19.83 rules = [Rule.Rls_ norm_Rational_min,
19.84 @@ -762,7 +762,7 @@
19.85 \<close>
19.86 ML \<open>
19.87 val add_fractions_p_rls = prep_rls'(
19.88 - Rule_Def.Repeat {id = "add_fractions_p_rls", preconds = [], rew_ord = ("dummy_ord", Rule.dummy_ord),
19.89 + Rule_Def.Repeat {id = "add_fractions_p_rls", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
19.90 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
19.91 rules = [Rule.Rls_ add_fractions_p],
19.92 scr = Rule.EmptyScr});
19.93 @@ -770,7 +770,7 @@
19.94 (* "Rule_Def.Repeat" causes repeated application of cancel_p to one and the same term *)
19.95 val cancel_p_rls = prep_rls'(
19.96 Rule_Def.Repeat
19.97 - {id = "cancel_p_rls", preconds = [], rew_ord = ("dummy_ord", Rule.dummy_ord),
19.98 + {id = "cancel_p_rls", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
19.99 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
19.100 rules = [Rule.Rls_ cancel_p],
19.101 scr = Rule.EmptyScr});
19.102 @@ -778,7 +778,7 @@
19.103 (*. makes 'normal' fractions; 'is_polyexp' inhibits double fractions;
19.104 used in initial part norm_Rational_mg, see example DA-M02-main.p.60.*)
19.105 val rat_mult_poly = prep_rls'(
19.106 - Rule_Def.Repeat {id = "rat_mult_poly", preconds = [], rew_ord = ("dummy_ord", Rule.dummy_ord),
19.107 + Rule_Def.Repeat {id = "rat_mult_poly", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
19.108 erls = Rule_Set.append_rules "Rule_Set.empty-is_polyexp" Rule_Set.empty [Rule.Num_Calc ("Poly.is'_polyexp", eval_is_polyexp "")],
19.109 srls = Rule_Set.Empty, calc = [], errpatts = [],
19.110 rules =
19.111 @@ -794,7 +794,7 @@
19.112 I.E. THE RESPECTIVE ASSUMPTION IS STORED AND Rule.Thm APPLIED; WN051028
19.113 ... WN0609???MG.*)
19.114 val rat_mult_div_pow = prep_rls'(
19.115 - Rule_Def.Repeat {id = "rat_mult_div_pow", preconds = [], rew_ord = ("dummy_ord",Rule.dummy_ord),
19.116 + Rule_Def.Repeat {id = "rat_mult_div_pow", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
19.117 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
19.118 rules = [Rule.Thm ("rat_mult", TermC.num_str @{thm rat_mult}),
19.119 (*"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)
19.120 @@ -817,7 +817,7 @@
19.121 scr = Rule.EmptyScr});
19.122
19.123 val rat_reduce_1 = prep_rls'(
19.124 - Rule_Def.Repeat {id = "rat_reduce_1", preconds = [], rew_ord = ("dummy_ord", Rule.dummy_ord),
19.125 + Rule_Def.Repeat {id = "rat_reduce_1", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
19.126 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
19.127 rules =
19.128 [Rule.Thm ("div_by_1", TermC.num_str @{thm div_by_1}),
19.129 @@ -829,7 +829,7 @@
19.130
19.131 (* looping part of norm_Rational *)
19.132 val norm_Rational_rls = prep_rls' (
19.133 - Rule_Def.Repeat {id = "norm_Rational_rls", preconds = [], rew_ord = ("dummy_ord",Rule.dummy_ord),
19.134 + Rule_Def.Repeat {id = "norm_Rational_rls", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
19.135 erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
19.136 rules = [Rule.Rls_ add_fractions_p_rls,
19.137 Rule.Rls_ rat_mult_div_pow,
19.138 @@ -841,7 +841,7 @@
19.139
19.140 val norm_Rational = prep_rls' (
19.141 Rule_Set.Seqence
19.142 - {id = "norm_Rational", preconds = [], rew_ord = ("dummy_ord", Rule.dummy_ord),
19.143 + {id = "norm_Rational", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
19.144 erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
19.145 rules = [Rule.Rls_ discard_minus,
19.146 Rule.Rls_ rat_mult_poly, (* removes double fractions like a/b/c *)
20.1 --- a/src/Tools/isac/Knowledge/Root.thy Wed Apr 08 15:50:03 2020 +0200
20.2 +++ b/src/Tools/isac/Knowledge/Root.thy Wed Apr 08 16:56:47 2020 +0200
20.3 @@ -155,7 +155,7 @@
20.4 (term_ord' pr thy(***) tu = LESS );
20.5 end;
20.6
20.7 -Rule.rew_ord' := overwritel (! Rule.rew_ord',
20.8 +Rewrite_Ord.rew_ord' := overwritel (! Rewrite_Ord.rew_ord',
20.9 [("termlessI", termlessI),
20.10 ("sqrt_right", sqrt_right false @{theory "Pure"})
20.11 ]);
21.1 --- a/src/Tools/isac/Knowledge/Test.thy Wed Apr 08 15:50:03 2020 +0200
21.2 +++ b/src/Tools/isac/Knowledge/Test.thy Wed Apr 08 16:56:47 2020 +0200
21.3 @@ -439,7 +439,7 @@
21.4 (*make () dissappear*)
21.5 val rearrange_assoc =
21.6 Rule_Def.Repeat{id = "rearrange_assoc", preconds = [],
21.7 - rew_ord = ("e_rew_ord",Rule.e_rew_ord),
21.8 + rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord),
21.9 erls = Rule_Set.empty, srls = Rule_Set.empty, calc = [], errpatts = [],
21.10 rules =
21.11 [Rule.Thm ("sym_add_assoc",TermC.num_str (@{thm add.assoc} RS @{thm sym})),
21.12 @@ -462,7 +462,7 @@
21.13
21.14 (*todo: replace by Rewrite("rnorm_equation_add",TermC.num_str @{thm rnorm_equation_add)*)
21.15 val norm_equation =
21.16 - Rule_Def.Repeat{id = "norm_equation", preconds = [], rew_ord = ("e_rew_ord",Rule.e_rew_ord),
21.17 + Rule_Def.Repeat{id = "norm_equation", preconds = [], rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord),
21.18 erls = tval_rls, srls = Rule_Set.empty, calc = [], errpatts = [],
21.19 rules = [Rule.Thm ("rnorm_equation_add",TermC.num_str @{thm rnorm_equation_add})
21.20 ],
21.21 @@ -529,7 +529,7 @@
21.22 ML \<open>
21.23 (*isolate the root in a root-equation*)
21.24 val isolate_root =
21.25 - Rule_Def.Repeat{id = "isolate_root", preconds = [], rew_ord = ("e_rew_ord",Rule.e_rew_ord),
21.26 + Rule_Def.Repeat{id = "isolate_root", preconds = [], rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord),
21.27 erls=tval_rls,srls = Rule_Set.empty, calc=[], errpatts = [],
21.28 rules = [Rule.Thm ("rroot_to_lhs",TermC.num_str @{thm rroot_to_lhs}),
21.29 Rule.Thm ("rroot_to_lhs_mult",TermC.num_str @{thm rroot_to_lhs_mult}),
21.30 @@ -543,7 +543,7 @@
21.31
21.32 (*isolate the bound variable in an equation; 'bdv' is a meta-constant*)
21.33 val isolate_bdv =
21.34 - Rule_Def.Repeat{id = "isolate_bdv", preconds = [], rew_ord = ("e_rew_ord",Rule.e_rew_ord),
21.35 + Rule_Def.Repeat{id = "isolate_bdv", preconds = [], rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord),
21.36 erls=tval_rls,srls = Rule_Set.empty, calc= [], errpatts = [],
21.37 rules =
21.38 [Rule.Thm ("risolate_bdv_add",TermC.num_str @{thm risolate_bdv_add}),
21.39 @@ -593,7 +593,7 @@
21.40 SOME "solve (e_e::bool, v_v)", [["Test","solve_linear"]]))]
21.41 \<close>
21.42 ML \<open>
21.43 -Rule.rew_ord' := overwritel (! Rule.rew_ord',
21.44 +Rewrite_Ord.rew_ord' := overwritel (! Rewrite_Ord.rew_ord',
21.45 [("termlessI", termlessI),
21.46 ("ord_make_polytest", ord_make_polytest false thy)
21.47 ]);
22.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml Wed Apr 08 15:50:03 2020 +0200
22.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml Wed Apr 08 16:56:47 2020 +0200
22.3 @@ -40,8 +40,8 @@
22.4 | Refine_Problem' of Celem.pblID * (Model.itm list * (bool * term) list)
22.5 | Refine_Tacitly' of Celem.pblID * Celem.pblID * ThyC.domID * Celem.metID * Model.itm list
22.6
22.7 - | Rewrite' of ThyC.theory' * Rule_Def.rew_ord' * Rule_Set.T * bool * Celem.thm'' * term * Selem.result
22.8 - | Rewrite_Inst' of ThyC.theory' * Rule_Def.rew_ord' * Rule_Set.T * bool * Rule.subst * Celem.thm'' * term * Selem.result
22.9 + | Rewrite' of ThyC.theory' * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * Celem.thm'' * term * Selem.result
22.10 + | Rewrite_Inst' of ThyC.theory' * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * Rule.subst * Celem.thm'' * term * Selem.result
22.11 | Rewrite_Set' of ThyC.theory' * bool * Rule_Set.T * term * Selem.result
22.12 | Rewrite_Set_Inst' of ThyC.theory' * bool * Rule.subst * Rule_Set.T * term * Selem.result
22.13
22.14 @@ -381,8 +381,8 @@
22.15 ThyC.domID * (* from new pbt?! filled in specify *)
22.16 Celem.metID * (* from new pbt?! filled in specify *)
22.17 Model.itm list (* drop ! 9.03: remains [] for Model_Problem recognizing its activation *)
22.18 - | Rewrite' of ThyC.theory' * Rule_Def.rew_ord' * Rule_Set.T * bool * Celem.thm'' * term * Selem.result
22.19 - | Rewrite_Inst' of ThyC.theory' * Rule_Def.rew_ord' * Rule_Set.T * bool * Rule.subst * Celem.thm'' * term * Selem.result
22.20 + | Rewrite' of ThyC.theory' * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * Celem.thm'' * term * Selem.result
22.21 + | Rewrite_Inst' of ThyC.theory' * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * Rule.subst * Celem.thm'' * term * Selem.result
22.22 | Rewrite_Set' of ThyC.theory' * bool * Rule_Set.T * term * Selem.result
22.23 | Rewrite_Set_Inst' of ThyC.theory' * bool * Rule.subst * Rule_Set.T * term * Selem.result
22.24
23.1 --- a/src/Tools/isac/ProgLang/ListC.thy Wed Apr 08 15:50:03 2020 +0200
23.2 +++ b/src/Tools/isac/ProgLang/ListC.thy Wed Apr 08 16:56:47 2020 +0200
23.3 @@ -131,7 +131,7 @@
23.4 ML \<open>
23.5 \<close> ML \<open>
23.6 val prog_expr =
23.7 - Rule_Def.Repeat {id = "prog_expr", preconds = [], rew_ord = ("dummy_ord", Rule.dummy_ord),
23.8 + Rule_Def.Repeat {id = "prog_expr", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
23.9 erls = Rule_Def.Empty, srls = Rule_Def.Empty, calc = [], errpatts = [],
23.10 rules = [Rule_Def.Thm ("refl", TermC.num_str @{thm refl}), (*'a<>b -> FALSE' by fun eval_equal*)
23.11 Rule_Def.Thm ("o_apply", TermC.num_str @{thm o_apply}),
24.1 --- a/src/Tools/isac/ProgLang/Prog_Expr.thy Wed Apr 08 15:50:03 2020 +0200
24.2 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy Wed Apr 08 16:56:47 2020 +0200
24.3 @@ -360,13 +360,13 @@
24.4 > reflI;
24.5 val it = "(?t = ?t) = True"
24.6 > val t = str2term "x = 0";
24.7 -> val NONE = rewrite_ thy Rule.dummy_ord Rule_Set.empty false reflI t;
24.8 +> val NONE = rewrite_ thy Rewrite_Ord.dummy_ord Rule_Set.empty false reflI t;
24.9
24.10 > val t = str2term "1 = 0";
24.11 -> val NONE = rewrite_ thy Rule.dummy_ord Rule_Set.empty false reflI t;
24.12 +> val NONE = rewrite_ thy Rewrite_Ord.dummy_ord Rule_Set.empty false reflI t;
24.13 ----------- thus needs Rule.Num_Calc !
24.14 > val t = str2term "0 = 0";
24.15 -> val SOME (t',_) = rewrite_ thy Rule.dummy_ord Rule_Set.empty false reflI t;
24.16 +> val SOME (t',_) = rewrite_ thy Rewrite_Ord.dummy_ord Rule_Set.empty false reflI t;
24.17 > Rule.term2str t';
24.18 val it = "HOL.True"
24.19
25.1 --- a/src/Tools/isac/ProgLang/rewrite.sml Wed Apr 08 15:50:03 2020 +0200
25.2 +++ b/src/Tools/isac/ProgLang/rewrite.sml Wed Apr 08 16:56:47 2020 +0200
25.3 @@ -269,7 +269,7 @@
25.4 in case Num_Calc.adhoc_thm thy isa_fn ct of
25.5 NONE => NONE
25.6 | SOME (thmID, thm) =>
25.7 - (let val rew = case rewrite_ thy Rule.dummy_ord Rule_Set.empty false thm ct of
25.8 + (let val rew = case rewrite_ thy Rewrite_Ord.dummy_ord Rule_Set.empty false thm ct of
25.9 SOME (rew, _) => rew
25.10 | NONE => raise ERROR ""
25.11 in SOME (rew, (thmID, thm)) end)
26.1 --- a/src/Tools/isac/Specify/appl.sml Wed Apr 08 15:50:03 2020 +0200
26.2 +++ b/src/Tools/isac/Specify/appl.sml Wed Apr 08 16:56:47 2020 +0200
26.3 @@ -263,7 +263,7 @@
26.4 let
26.5 val subst = Selem.subs2subst thy subs;
26.6 in
26.7 - case Rewrite.rewrite_inst_ thy (Rule.assoc_rew_ord ro') erls false subst (snd thm'') f of
26.8 + case Rewrite.rewrite_inst_ thy (Rewrite_Ord.assoc_rew_ord ro') erls false subst (snd thm'') f of
26.9 SOME (f',asm) =>
26.10 Appl (Tactic.Rewrite_Inst' (thy', ro', erls, false, subst, thm'', f, (f', asm)))
26.11 | NONE => Notappl ((fst thm'')^" not applicable")
26.12 @@ -284,7 +284,7 @@
26.13 in
26.14 if msg = "OK"
26.15 then
26.16 - case Rewrite.rewrite_ thy (Rule.assoc_rew_ord ro) rls' false (snd thm'') f of
26.17 + case Rewrite.rewrite_ thy (Rewrite_Ord.assoc_rew_ord ro) rls' false (snd thm'') f of
26.18 SOME (f',asm) => Appl (Tactic.Rewrite' (thy', ro, rls', false, thm'', f, (f', asm)))
26.19 | NONE => Notappl ("'" ^ fst thm'' ^"' not applicable")
26.20 else Notappl msg
26.21 @@ -398,7 +398,7 @@
26.22 val {rew_ord',erls,...} = Specify.get_met (get_obj g_metID pt pp)
26.23 val subte = Selem.sube2subte sube
26.24 val subst = Selem.sube2subst thy sube
26.25 - val ro = Rule.assoc_rew_ord rew_ord'
26.26 + val ro = Rewrite_Ord.assoc_rew_ord rew_ord'
26.27 in
26.28 if foldl and_ (true, map TermC.contains_Var subte)
26.29 then (*1*)
27.1 --- a/src/Tools/isac/Specify/ptyps.sml Wed Apr 08 15:50:03 2020 +0200
27.2 +++ b/src/Tools/isac/Specify/ptyps.sml Wed Apr 08 16:56:47 2020 +0200
27.3 @@ -47,7 +47,7 @@
27.4 val prep_met : theory -> string -> string list -> Celem.pblID ->
27.5 string list * (string * string list) list *
27.6 {calc: 'a, crls: Rule_Set.T, errpats: Rule.errpat list, nrls: Rule_Set.T, prls: Rule_Set.T,
27.7 - rew_ord': Rule_Def.rew_ord', rls': Rule_Set.T, srls: Rule_Set.T} * thm ->
27.8 + rew_ord': Rewrite_Ord.rew_ord', rls': Rule_Set.T, srls: Rule_Set.T} * thm ->
27.9 Celem.met * Celem.metID
27.10 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
27.11 val show_ptyps : unit -> unit
28.1 --- a/src/Tools/isac/TODO.thy Wed Apr 08 15:50:03 2020 +0200
28.2 +++ b/src/Tools/isac/TODO.thy Wed Apr 08 16:56:47 2020 +0200
28.3 @@ -204,7 +204,7 @@
28.4 \item Diff.thy: differentiateX --> differentiate after removal of script-constant
28.5 \item Test.thy: met_test_sqrt2: deleted?!
28.6 \item xxx
28.7 - \item Rule_Def.rew_ord' := overwritel (! Rule_Def.rew_ord', (*<<<---- use KEStore.xxx, too*)
28.8 + \item Rewrite_Ord.rew_ord' := overwritel (! Rewrite_Ord.rew_ord', (*<<<---- use KEStore.xxx, too*)
28.9 \item xxx
28.10 \item automatically extrac rls from program-code
28.11 ? take ["SignalProcessing", "Z_Transform", "Inverse_sub"] as an example ?
29.1 --- a/test/Tools/isac/Test_Isac_Short.thy Wed Apr 08 15:50:03 2020 +0200
29.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Wed Apr 08 16:56:47 2020 +0200
29.3 @@ -130,6 +130,7 @@
29.4 open Rule_Set
29.5 open Exec_Def
29.6 open ThyC
29.7 + open Rewrite_Ord
29.8 (*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
29.9 \<close>
29.10