1.1 --- a/src/Tools/isac/BridgeLibisabelle/datatypes.sml Sat Apr 04 12:11:32 2020 +0200
1.2 +++ b/src/Tools/isac/BridgeLibisabelle/datatypes.sml Mon Apr 06 11:44:36 2020 +0200
1.3 @@ -37,7 +37,7 @@
1.4 val posterms2xml : int -> (Pos.pos' * term) list -> Celem.xml
1.5 val precond2xml : int -> bool * Term.term -> Celem.xml
1.6 val preconds2xml : int -> (bool * Term.term) list -> Celem.xml
1.7 - val rls2xml : int -> Rule.thyID * Rule_Set.rls -> Celem.xml
1.8 + val rls2xml : int -> Rule.thyID * Rule_Set.T -> Celem.xml
1.9 val rule2xml : int -> Celem.guh -> Rule.rule -> Celem.xml
1.10 val rules2xml : int -> Celem.guh -> Rule.rule list -> Celem.xml
1.11 val scr2xml : int -> Program.T -> Celem.xml
1.12 @@ -257,9 +257,9 @@
1.13 calcrefs2xml (j+i) (thyID, calc) ^
1.14 scr2xml (j+i) scr ^
1.15 indt j ^"</RULESET>\n";
1.16 -fun rls2xml j (thyID, Rule_Set.Erls) = rls2xml j (thyID, Rule_Set.e_rls)
1.17 - | rls2xml j (thyID, Rule_Set.Rls data) = rls2xm j (thyID, "Rls", data)
1.18 - | rls2xml j (thyID, Rule_Set.Seq data) = rls2xm j (thyID, "Seq", data)
1.19 +fun rls2xml j (thyID, Rule_Set.Empty) = rls2xml j (thyID, Rule_Set.e_rls)
1.20 + | rls2xml j (thyID, Rule_Def.Repeat data) = rls2xm j (thyID, "Rls", data)
1.21 + | rls2xml j (thyID, Rule_Set.Seqence data) = rls2xm j (thyID, "Seq", data)
1.22 | rls2xml j (thyID, Rule_Set.Rrls {id, prepat, rew_ord=(ord,_), erls, calc, errpatts, scr}) =
1.23 indt j ^"<RULESET>\n"^
1.24 indt (j+i) ^"<ID> "^ id ^" </ID>\n"^
2.1 --- a/src/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Sat Apr 04 12:11:32 2020 +0200
2.2 +++ b/src/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Mon Apr 06 11:44:36 2020 +0200
2.3 @@ -25,7 +25,7 @@
2.4 in (theID, Celem.Hthm {guh = Celem.theID2guh theID, coursedesign = [],
2.5 mathauthors = ["isac-team"], fillpats = [], thm = thm})
2.6 end;
2.7 -fun makeHrls (part : string) (rls' : Rule_Set.rls', thy_rls as (thyID, rls): Rule.thyID * Rule_Set.rls) =
2.8 +fun makeHrls (part : string) (rls' : Rule_Set.rls', thy_rls as (thyID, rls): Rule.thyID * Rule_Set.T) =
2.9 let val theID = [part, thyID,"Rulesets"] @ [rls'] : Celem.theID
2.10 in (theID, Celem.Hrls {guh = Celem.theID2guh theID, coursedesign = [],
2.11 mathauthors = ["isac-team"], thy_rls = thy_rls})
2.12 @@ -52,7 +52,7 @@
2.13 else Rule.Thm (Thm.get_name_hint thm, thm)
2.14
2.15 (* get all theorems from the list of rule-sets (defined in Knowledge) *)
2.16 -fun thms_of_rlss thy rlss = (rlss : (Rule_Set.rls' * (Rule.theory' * Rule_Set.rls)) list)
2.17 +fun thms_of_rlss thy rlss = (rlss : (Rule_Set.rls' * (Rule.theory' * Rule_Set.T)) list)
2.18 |> map (Rtools.thms_of_rls o #2 o #2)
2.19 |> flat
2.20 |> map (revert_sym thy)
2.21 @@ -64,7 +64,7 @@
2.22
2.23 fun collect_thms part thy =
2.24 map (makeHthm (part, Context.theory_name thy)) (rev (thms_of thy))
2.25 -fun collect_rlss part rlss thys = (rlss : (Rule_Set.rls' * (Rule.thyID * Rule_Set.rls)) list)
2.26 +fun collect_rlss part rlss thys = (rlss : (Rule_Set.rls' * (Rule.thyID * Rule_Set.T)) list)
2.27 |> filter (fn (_, (thyID, _)) => member (op=) (map Context.theory_name thys) thyID)
2.28 |> map (makeHrls part)
2.29 fun collect_cals (part, thy') =
3.1 --- a/src/Tools/isac/CalcElements/KEStore.thy Sat Apr 04 12:11:32 2020 +0200
3.2 +++ b/src/Tools/isac/CalcElements/KEStore.thy Mon Apr 06 11:44:36 2020 +0200
3.3 @@ -31,8 +31,8 @@
3.4 *)
3.5 signature KESTORE_ELEMS =
3.6 sig
3.7 - val get_rlss: theory -> (Rule_Set.rls' * (Rule.theory' * Rule_Set.rls)) list
3.8 - val add_rlss: (Rule_Set.rls' * (Rule.theory' * Rule_Set.rls)) list -> theory -> theory
3.9 + val get_rlss: theory -> (Rule_Set.rls' * (Rule.theory' * Rule_Set.T)) list
3.10 + val add_rlss: (Rule_Set.rls' * (Rule.theory' * Rule_Set.T)) list -> theory -> theory
3.11 val get_calcs: theory -> (Rule_Set.prog_calcID * (Rule.calID * Rule.eval_fn)) list
3.12 val add_calcs: (Rule_Set.prog_calcID * (Rule.calID * Rule.eval_fn)) list -> theory -> theory
3.13 val get_cas: theory -> Celem.cas_elem list
3.14 @@ -53,7 +53,7 @@
3.15 fun union_overwrite eq l1 l2 = fold (insert eq) l2 (*..swapped..*) l1;
3.16
3.17 structure Data = Theory_Data (
3.18 - type T = (Rule_Set.rls' * (Rule.theory' * Rule_Set.rls)) list;
3.19 + type T = (Rule_Set.rls' * (Rule.theory' * Rule_Set.T)) list;
3.20 val empty = [];
3.21 val extend = I;
3.22 val merge = Rule_Set.merge_rlss;
3.23 @@ -190,11 +190,11 @@
3.24
3.25 section \<open>Functions for checking KEStore_Elems\<close>
3.26 ML \<open>
3.27 -fun short_string_of_rls Rule_Set.Erls = "Erls"
3.28 - | short_string_of_rls (Rule_Set.Rls {calc, rules, ...}) =
3.29 +fun short_string_of_rls Rule_Set.Empty = "Erls"
3.30 + | short_string_of_rls (Rule_Def.Repeat {calc, rules, ...}) =
3.31 "Rls {#calc = " ^ string_of_int (length calc) ^
3.32 ", #rules = " ^ string_of_int (length rules) ^ ", ..."
3.33 - | short_string_of_rls (Rule_Set.Seq {calc, rules, ...}) =
3.34 + | short_string_of_rls (Rule_Set.Seqence {calc, rules, ...}) =
3.35 "Seq {#calc = " ^ string_of_int (length calc) ^
3.36 ", #rules = " ^ string_of_int (length rules) ^ ", ..."
3.37 | short_string_of_rls (Rule_Set.Rrls _) = "Rrls {...}";
4.1 --- a/src/Tools/isac/CalcElements/calcelems.sml Sat Apr 04 12:11:32 2020 +0200
4.2 +++ b/src/Tools/isac/CalcElements/calcelems.sml Mon Apr 06 11:44:36 2020 +0200
4.3 @@ -26,7 +26,7 @@
4.4 datatype thydata
4.5 = Hcal of {calc: Rule_Set.calc, coursedesign: authors, guh: guh, mathauthors: authors}
4.6 | Hord of {coursedesign: authors, guh: guh, mathauthors: authors, ord: Rule.subst -> term * term -> bool}
4.7 - | Hrls of {coursedesign: authors, guh: guh, mathauthors: authors, thy_rls: Rule.thyID * Rule_Set.rls}
4.8 + | Hrls of {coursedesign: authors, guh: guh, mathauthors: authors, thy_rls: Rule.thyID * Rule_Set.T}
4.9 | Hthm of {coursedesign: authors, fillpats: fillpat list, guh: guh, mathauthors: authors, thm: thm}
4.10 | Html of {coursedesign: authors, guh: guh, html: string, mathauthors: authors}
4.11 type theID
4.12 @@ -109,8 +109,8 @@
4.13 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
4.14
4.15 (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
4.16 -val overwritelthy: theory -> (Rule_Set.rls' * (string * Rule_Set.rls)) list * (Rule_Set.rls' * Rule_Set.rls) list ->
4.17 - (Rule_Set.rls' * (string * Rule_Set.rls)) list end
4.18 +val overwritelthy: theory -> (Rule_Set.rls' * (string * Rule_Set.T)) list * (Rule_Set.rls' * Rule_Set.T) list ->
4.19 + (Rule_Set.rls' * (string * Rule_Set.T)) list end
4.20
4.21 (**)
4.22 structure Celem(**): CALC_ELEMENT(**) =
4.23 @@ -285,7 +285,7 @@
4.24 Html of {guh: guh, coursedesign: authors, mathauthors: authors, html: string}
4.25 | Hthm of {guh: guh, coursedesign: authors, mathauthors: authors, fillpats: fillpat list,
4.26 thm: thm} (* here no sym_thm, thus no thmID required *)
4.27 -| Hrls of {guh: guh, coursedesign: authors, mathauthors: authors, thy_rls: (Rule.thyID * Rule_Set.rls)}
4.28 +| Hrls of {guh: guh, coursedesign: authors, mathauthors: authors, thy_rls: (Rule.thyID * Rule_Set.T)}
4.29 | Hcal of {guh: guh, coursedesign: authors, mathauthors: authors, calc: Rule_Set.calc}
4.30 | Hord of {guh: guh, coursedesign: authors, mathauthors: authors,
4.31 ord: (Rule.subst -> (term * term) -> bool)};
4.32 @@ -411,7 +411,7 @@
4.33 in scripts...
4.34 actually a hack to get alltogether run again with minimal effort *)
4.35 fun insthy thy' (rls', rls) = (rls', (thy', rls));
4.36 -fun overwritelthy thy (al, bl: (Rule_Set.rls' * Rule_Set.rls) list) =
4.37 +fun overwritelthy thy (al, bl: (Rule_Set.rls' * Rule_Set.T) list) =
4.38 let val bl' = map (insthy ((get_thy o Rule.theory2theory') thy)) bl
4.39 in overwritel (al, bl') end;
4.40
4.41 @@ -460,7 +460,7 @@
4.42 cas : term option, (* 'CAS-command' *)
4.43 met : metID list, (* methods solving the pbt *)
4.44 (*TODO: abstract to ?pre_model?...*)
4.45 - prls : Rule_Set.rls, (* for preds in where_ *)
4.46 + prls : Rule_Set.T, (* for preds in where_ *)
4.47 where_ : term list, (* where - predicates *)
4.48 ppc : pat list (* this is the model-pattern;
4.49 it contains "#Given","#Where","#Find","#Relate"-patterns
4.50 @@ -468,7 +468,7 @@
4.51 }
4.52
4.53 val e_pbt = {guh = "pbl_empty", mathauthors = [], init = e_pblID, thy = Thy_Info.get_theory "Pure",
4.54 - cas = NONE, prls = Rule_Set.Erls, where_ = [], ppc = [], met = []} : pbt
4.55 + cas = NONE, prls = Rule_Set.Empty, where_ = [], ppc = [], met = []} : pbt
4.56 fun pbt2str ({cas = cas', guh = guh', init = init', mathauthors = ma', met = met', ppc = ppc',
4.57 prls = prls', thy = thy', where_ = w'} : pbt)
4.58 = "{cas = " ^ (Rule.termopt2str cas') ^ ", guh = \"" ^ guh' ^ "\", init = "
4.59 @@ -544,17 +544,17 @@
4.60 init : pblID, (* WN060721 introduced mistakenly--TODO.REMOVE! *)
4.61 rew_ord' : Rule_Def.rew_ord', (* for rules in Detail
4.62 TODO.WN0509 store fun itself, see 'type pbt' *)
4.63 - erls : Rule_Set.rls, (* the eval_rls for cond. in rules FIXME "rls'
4.64 + erls : Rule_Set.T, (* the eval_rls for cond. in rules FIXME "rls'
4.65 instead erls in "fun prep_met" *)
4.66 - srls : Rule_Set.rls, (* for evaluating list expressions in scr *)
4.67 - crls : Rule_Set.rls, (* for check_elementwise, ie. formulae in calc. *)
4.68 - nrls : Rule_Set.rls, (* canonical simplifier specific for this met *)
4.69 + srls : Rule_Set.T, (* for evaluating list expressions in scr *)
4.70 + crls : Rule_Set.T, (* for check_elementwise, ie. formulae in calc. *)
4.71 + nrls : Rule_Set.T, (* canonical simplifier specific for this met *)
4.72 errpats : Rule.errpat list,(* error patterns expected in this method *)
4.73 calc : Rule_Set.calc list, (* Theory_Data in fun prep_met *)
4.74 (*branch : TransitiveB set in append_problem at generation ob pblobj *)
4.75 scr : Rule.program, (* progam, empty as @{thm refl} or Rfuns *)
4.76 (*TODO: abstract to ?pre_model?...*)
4.77 - prls : Rule_Set.rls, (* for evaluating predicates in modelpattern *)
4.78 + prls : Rule_Set.T, (* for evaluating predicates in modelpattern *)
4.79 ppc : pat list, (* items in given, find, relate;
4.80 items (in "#Find") which need not occur in the arg-list of a SubProblem
4.81 are 'copy-named' with an identifier "*'.'".
4.82 @@ -614,11 +614,11 @@
4.83 let
4.84 val rls' =
4.85 case rls of
4.86 - Rule_Set.Rls {id, preconds, rew_ord, erls, srls, calc, rules, scr, ...}
4.87 - => Rule_Set.Rls {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, srls = srls,
4.88 + Rule_Def.Repeat {id, preconds, rew_ord, erls, srls, calc, rules, scr, ...}
4.89 + => Rule_Def.Repeat {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, srls = srls,
4.90 calc = calc, rules = rules, scr = scr, errpatts = errpatIDs}
4.91 - | Rule_Set.Seq {id, preconds, rew_ord, erls, srls, calc, rules, scr, ...}
4.92 - => Rule_Set.Seq {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, srls = srls,
4.93 + | Rule_Set.Seqence {id, preconds, rew_ord, erls, srls, calc, rules, scr, ...}
4.94 + => Rule_Set.Seqence {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, srls = srls,
4.95 calc = calc, rules = rules, scr = scr, errpatts = errpatIDs}
4.96 | Rule_Set.Rrls {id, prepat, rew_ord, erls, calc, scr, ...}
4.97 => Rule_Set.Rrls {id = id, prepat = prepat, rew_ord = rew_ord, erls = erls, calc = calc,
5.1 --- a/src/Tools/isac/CalcElements/rule-def.sml Sat Apr 04 12:11:32 2020 +0200
5.2 +++ b/src/Tools/isac/CalcElements/rule-def.sml Mon Apr 06 11:44:36 2020 +0200
5.3 @@ -15,16 +15,16 @@
5.4 type rew_ord_
5.5 type eval_fn
5.6
5.7 - datatype rls =
5.8 - Erls
5.9 - | Rls of {calc: calc list, erls: rls, errpatts: errpatID list, id: string,
5.10 - preconds: term list, rew_ord: rew_ord, rules: rule list, scr: program, srls: rls}
5.11 - | Seq of {calc: calc list, erls: rls, errpatts: errpatID list, id: string,
5.12 - preconds: term list, rew_ord: rew_ord, rules: rule list, scr: program, srls: rls}
5.13 - | Rrls of {calc: calc list, erls: rls, errpatts: errpatID list, id: string,
5.14 + datatype rule_set =
5.15 + Empty
5.16 + | Repeat of {calc: calc list, erls: rule_set, errpatts: errpatID list, id: string,
5.17 + preconds: term list, rew_ord: rew_ord, rules: rule list, scr: program, srls: rule_set}
5.18 + | Seqence of {calc: calc list, erls: rule_set, errpatts: errpatID list, id: string,
5.19 + preconds: term list, rew_ord: rew_ord, rules: rule list, scr: program, srls: rule_set}
5.20 + | Rrls of {calc: calc list, erls: rule_set, errpatts: errpatID list, id: string,
5.21 prepat: (term list * term) list, rew_ord: rew_ord, scr: program}
5.22 and rule = Cal1 of string * eval_fn | Num_Calc of string * eval_fn | Erule
5.23 - | Rls_ of rls | Thm of string * thm
5.24 + | Rls_ of rule_set | Thm of string * thm
5.25 and program =
5.26 EmptyScr
5.27 | Prog of term
5.28 @@ -76,7 +76,7 @@
5.29 | Cal1 of string * (*.sml-code applied only to whole term
5.30 or left/right-hand-side of eqality .*)
5.31 eval_fn
5.32 - | Rls_ of rls (*.ie. rule sets may be nested.*)
5.33 + | Rls_ of rule_set (*.ie. rule sets may be nested.*)
5.34 and program =
5.35 EmptyScr
5.36 | Prog of term (* a leaf is either a tactic or an 'exp' in 'let v = expr'
5.37 @@ -126,39 +126,38 @@
5.38 list} (* there may be several such rules; the list is empty, if the
5.39 users term does not belong to e.g. a cancellation of the term
5.40 last agreed upon. *)
5.41 -and rls =
5.42 - Erls (*for init e_rls*)
5.43 -
5.44 - | Rls of (*a confluent and terminating ruleset, in general *)
5.45 +and rule_set =
5.46 + Empty
5.47 + | Repeat of (*a confluent and terminating ruleset, in general *)
5.48 {id : string, (*for trace_rewrite:=true *)
5.49 preconds : term list, (*unused WN020820 *)
5.50 (*WN060616 for efficiency...
5.51 bdvs : false, (*set in prep_rls' for get_bdvs *)*)
5.52 rew_ord : rew_ord, (*for rules*)
5.53 - erls : rls, (*for the conditions in rules *)
5.54 - srls : rls, (*for evaluation of list_fns in script *)
5.55 + erls : rule_set, (*for the conditions in rules *)
5.56 + srls : rule_set, (*for evaluation of list_fns in script *)
5.57 calc : calc list, (*for Calculate in scr, set by prep_rls' *)
5.58 rules : rule list,
5.59 errpatts : errpatID list,(*dialog-authoring in Build_Thydata.thy *)
5.60 scr : program} (*Prog term: generating intermed.steps *)
5.61 - | Seq of (*a sequence of rules to be tried only once *)
5.62 + | Seqence of (*a sequence of rules to be tried only once *)
5.63 {id : string, (*for trace_rewrite:=true *)
5.64 preconds : term list, (*unused 20.8.02 *)
5.65 (*WN060616 for efficiency...
5.66 bdvs : false, (*set in prep_rls' for get_bdvs *)*)
5.67 rew_ord : rew_ord, (*for rules *)
5.68 - erls : rls, (*for the conditions in rules *)
5.69 - srls : rls, (*for evaluation of list_fns in script *)
5.70 + erls : rule_set, (*for the conditions in rules *)
5.71 + srls : rule_set, (*for evaluation of list_fns in script *)
5.72 calc : calc list, (*for Calculate in scr, set by prep_rls' *)
5.73 rules : rule list,
5.74 errpatts : errpatID list,(*dialog-authoring in Build_Thydata.thy*)
5.75 scr : program} (*Prog term (how to restrict type ???)*)
5.76
5.77 - (*Rrls call SML-code and simulate an rls
5.78 + (*Rrls call SML-code and simulate an rule_set
5.79 difference: there is always _ONE_ redex rewritten in 1 call,
5.80 thus wrap Rrls by: Rls (Rls_ ...)*)
5.81 | Rrls of (* SML-functions within rewriting; step-wise execution provided;
5.82 - Rrls simulate an rls
5.83 + Rrls simulate an rule_set
5.84 difference: there is always _ONE_ redex rewritten in 1 call,
5.85 thus wrap Rrls by: Rls (Rls_ ...) *)
5.86 {id : string, (* for trace_rewrite := true *)
5.87 @@ -167,7 +166,7 @@
5.88 term ) (* pattern matched with current (sub)term *)
5.89 list, (* meta-conjunction is or *)
5.90 rew_ord : rew_ord, (* for rules *)
5.91 - erls : rls, (* for the conditions in rules and preconds *)
5.92 + erls : rule_set, (* for the conditions in rules and preconds *)
5.93 calc : calc list, (* for Calculate in scr, set automatic.in prep_rls' *)
5.94 errpatts : errpatID list,(*dialog-authoring in Build_Thydata.thy*)
5.95 scr : program}; (* Rfuns {...} (how to restrict type ???) *)
6.1 --- a/src/Tools/isac/CalcElements/rule-set.sml Sat Apr 04 12:11:32 2020 +0200
6.2 +++ b/src/Tools/isac/CalcElements/rule-set.sml Mon Apr 06 11:44:36 2020 +0200
6.3 @@ -6,29 +6,29 @@
6.4 *)
6.5 signature RULE_SET =
6.6 sig
6.7 - datatype rls = datatype Rule_Def.rls
6.8 + datatype T = datatype Rule_Def.rule_set
6.9 eqtype rls'
6.10
6.11 type calc = Rule_Def.calc (*..from Rule_Def*)
6.12 - val e_rls: rls
6.13 + val e_rls: T
6.14
6.15 type rrlsstate = term * term * Rule_Def.rule list list * (Rule_Def.rule * (term * term list)) list
6.16 val e_rrlsstate: rrlsstate
6.17 - val e_rrls: rls
6.18 + val e_rrls: T
6.19 type rlss_elem
6.20
6.21 - val append_rls: string -> rls -> Rule_Def.rule list -> rls
6.22 - val rep_rls: rls -> {calc: calc list, erls: rls, errpats: Rule_Def.errpatID list, id: string,
6.23 - preconds: term list, rew_ord: Rule_Def.rew_ord, rules: Rule_Def.rule list, scr: Rule_Def.program, srls: rls}
6.24 + val append_rls: string -> T -> Rule_Def.rule list -> T
6.25 + val rep_rls: T -> {calc: calc list, erls: T, errpats: Rule_Def.errpatID list, id: string,
6.26 + preconds: term list, rew_ord: Rule_Def.rew_ord, rules: Rule_Def.rule list, scr: Rule_Def.program, srls: T}
6.27
6.28 - val rls2str: Rule_Def.rls -> string
6.29 - val id_rls: Rule_Def.rls -> string
6.30 + val rls2str: T -> string
6.31 + val id_rls: T -> string
6.32 val id_rule: Rule_Def.rule -> string
6.33 val eq_rule: Rule_Def.rule * Rule_Def.rule -> bool
6.34
6.35 - val merge_rls: string -> rls -> rls -> rls
6.36 + val merge_rls: string -> T -> T -> T
6.37 val merge_rlss: rlss_elem list * rlss_elem list -> rlss_elem list
6.38 - val remove_rls: string -> rls -> Rule_Def.rule list -> rls
6.39 + val remove_rls: string -> T -> Rule_Def.rule list -> T
6.40
6.41 val rule2str: Rule_Def.rule -> string
6.42 val rule2str': Rule_Def.rule -> string
6.43 @@ -39,7 +39,7 @@
6.44 val calc_eq: calc_elem * calc_elem -> bool
6.45 val e_evalfn: Rule_Def.eval_fn
6.46
6.47 - val get_rules: rls -> Rule_Def.rule list
6.48 + val get_rules: T -> Rule_Def.rule list
6.49 val rls_eq: (''a * ('b * 'c)) * (''a * ('d * 'e)) -> bool
6.50
6.51 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
6.52 @@ -52,7 +52,7 @@
6.53 structure Rule_Set(**): RULE_SET(**) =
6.54 struct
6.55 (**)
6.56 -datatype rls = datatype Rule_Def.rls
6.57 +datatype T = datatype Rule_Def.rule_set
6.58 type rls' = string
6.59
6.60 type calc = Rule_Def.calc
6.61 @@ -60,8 +60,8 @@
6.62 fun dummy_ord (_: subst) (_: term, _: term) = true;
6.63
6.64 val e_rls =
6.65 - Rls {id = "e_rls", preconds = [], rew_ord = ("dummy_ord", dummy_ord), erls = Erls,
6.66 - srls = Erls, calc = [], rules = [], errpatts = [], scr = Rule_Def.EmptyScr}: rls;
6.67 + Rule_Def.Repeat {id = "e_rls", preconds = [], rew_ord = ("dummy_ord", dummy_ord), erls = Rule_Def.Empty,
6.68 + srls = Rule_Def.Empty, calc = [], rules = [], errpatts = [], scr = Rule_Def.EmptyScr}
6.69
6.70 (*/--------------------------------------\*)
6.71 type rrlsstate = (* state for reverse rewriting, comments see type rule and scr | Rfuns *)
6.72 @@ -79,32 +79,32 @@
6.73 next_rule = ne, attach_form = fo};
6.74 end;
6.75 val e_rrls =
6.76 - Rrls {id = "e_rrls", prepat = [], rew_ord = ("dummy_ord", dummy_ord), erls = Erls,
6.77 - calc = [], errpatts = [], scr = e_rfuns}:rls;
6.78 + Rrls {id = "e_rrls", prepat = [], rew_ord = ("dummy_ord", dummy_ord), erls = Rule_Def.Empty,
6.79 + calc = [], errpatts = [], scr = e_rfuns}
6.80
6.81 -fun rep_rls Erls = rep_rls e_rls
6.82 - | rep_rls (Rls {id, preconds, rew_ord, erls, srls, calc, errpatts, rules, scr}) =
6.83 +fun rep_rls Rule_Def.Empty = rep_rls e_rls
6.84 + | rep_rls (Rule_Def.Repeat {id, preconds, rew_ord, erls, srls, calc, errpatts, rules, scr}) =
6.85 {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, srls = srls, errpats = errpatts,
6.86 calc = calc, rules = rules, scr = scr}
6.87 - | rep_rls (Seq {id, preconds, rew_ord, erls, srls, calc, errpatts, rules, scr}) =
6.88 + | rep_rls (Rule_Def.Seqence {id, preconds, rew_ord, erls, srls, calc, errpatts, rules, scr}) =
6.89 {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, srls = srls, errpats = errpatts,
6.90 calc = calc, rules = rules, scr = scr}
6.91 | rep_rls (Rrls _) = rep_rls e_rls
6.92
6.93 -fun append_rls id Erls _ = raise ERROR ("append_rls: with \"" ^ id ^ "\" not for Erls")
6.94 - | append_rls id (Rls {id = _, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
6.95 +fun append_rls id Rule_Def.Empty _ = raise ERROR ("append_rls: with \"" ^ id ^ "\" not for Rule_Def.Empty")
6.96 + | append_rls id (Rule_Def.Repeat {id = _, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
6.97 rules = rs, errpatts = errpatts, scr = sc}) r =
6.98 - Rls {id = id, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
6.99 + Rule_Def.Repeat {id = id, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
6.100 rules = rs @ r, errpatts = errpatts, scr = sc}
6.101 - | append_rls id (Seq {id = _, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
6.102 + | append_rls id (Rule_Def.Seqence {id = _, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
6.103 rules = rs, errpatts = errpatts, scr = sc}) r =
6.104 - Seq {id = id, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
6.105 + Rule_Def.Seqence {id = id, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
6.106 rules = rs @ r, errpatts = errpatts, scr = sc}
6.107 | append_rls id (Rrls _) _ = raise ERROR ("append_rls: not for reverse-rewrite-rule-set " ^ id);
6.108
6.109 -fun id_rls Erls = "e_rls" (*WN060714 quick and dirty: recursive defs! TODO "Erls"*)
6.110 - | id_rls (Rule_Def.Rls {id, ...}) = id
6.111 - | id_rls (Rule_Def.Seq {id, ...}) = id
6.112 +fun id_rls Rule_Def.Empty = "e_rls" (*WN060714 quick and dirty: recursive defs! TODO "Rule_Def.Empty"*)
6.113 + | id_rls (Rule_Def.Repeat {id, ...}) = id
6.114 + | id_rls (Rule_Def.Seqence {id, ...}) = id
6.115 | id_rls (Rule_Def.Rrls {id, ...}) = id;
6.116 val rls2str = id_rls;
6.117
6.118 @@ -151,17 +151,17 @@
6.119 else false
6.120 fun e_evalfn (_ : 'a) (_ : term) (_ : theory) = NONE : (string * term) option;
6.121
6.122 -fun merge_rls _ Erls rls = rls
6.123 - | merge_rls _ rls Erls = rls
6.124 +fun merge_rls _ Rule_Def.Empty rls = rls
6.125 + | merge_rls _ rls Rule_Def.Empty = rls
6.126 | merge_rls _ (Rrls x) _ = Rrls x (* required for merging Theory_Data *)
6.127 | merge_rls _ _ (Rrls x) = Rrls x
6.128 | merge_rls id
6.129 - (Rls {preconds = pc1, rew_ord = ro1, erls = er1, srls = sr1, calc = ca1,
6.130 + (Rule_Def.Repeat {preconds = pc1, rew_ord = ro1, erls = er1, srls = sr1, calc = ca1,
6.131 rules = rs1, errpatts = eps1, scr = sc1, ...})
6.132 - (Rls {preconds = pc2, erls = er2, srls = sr2, calc = ca2,
6.133 + (Rule_Def.Repeat {preconds = pc2, erls = er2, srls = sr2, calc = ca2,
6.134 rules = rs2, errpatts = eps2, ...})
6.135 =
6.136 - Rls {id = id, rew_ord = ro1, scr = sc1,
6.137 + Rule_Def.Repeat {id = id, rew_ord = ro1, scr = sc1,
6.138 preconds = union (op =) pc1 pc2,
6.139 erls = merge_rls (merge_ids er1 er2) er1 er2,
6.140 srls = merge_rls (merge_ids sr1 sr2) sr1 sr2,
6.141 @@ -169,12 +169,12 @@
6.142 rules = union eq_rule rs1 rs2,
6.143 errpatts = union (op =) eps1 eps2}
6.144 | merge_rls id
6.145 - (Seq {preconds = pc1, rew_ord = ro1, erls = er1, srls = sr1, calc = ca1,
6.146 + (Rule_Def.Seqence {preconds = pc1, rew_ord = ro1, erls = er1, srls = sr1, calc = ca1,
6.147 rules = rs1, errpatts = eps1, scr = sc1, ...})
6.148 - (Seq {preconds = pc2, erls = er2, srls = sr2, calc = ca2,
6.149 + (Rule_Def.Seqence {preconds = pc2, erls = er2, srls = sr2, calc = ca2,
6.150 rules = rs2, errpatts = eps2, ...})
6.151 =
6.152 - Seq {id = id, rew_ord = ro1, scr = sc1,
6.153 + Rule_Def.Seqence {id = id, rew_ord = ro1, scr = sc1,
6.154 preconds = union (op =) pc1 pc2,
6.155 erls = merge_rls (merge_ids er1 er2) er1 er2,
6.156 srls = merge_rls (merge_ids sr1 sr2) sr1 sr2,
6.157 @@ -182,13 +182,13 @@
6.158 rules = union eq_rule rs1 rs2,
6.159 errpatts = union (op =) eps1 eps2}
6.160 | merge_rls id _ _ = error ("merge_rls: \"" ^ id ^
6.161 - "\"; not for reverse-rewrite-rule-sets and not for mixed Rls -- Seq");
6.162 + "\"; not for reverse-rewrite-rule-sets and not for mixed Rls -- Rule_Def.Seqence");
6.163
6.164 (* datastructure for KEStore_Elems, intermediate for thehier *)
6.165 type rlss_elem =
6.166 (rls' * (* identifier unique within Isac *)
6.167 (Rule.theory' * (* just for assignment in thehier, not appropriate for parsing etc *)
6.168 - Rule_Def.rls)) (* ((#id o rep_rls) rls) = rls' by coding discipline *)
6.169 + T)) (* ((#id o rep_rls) T) = rls' by coding discipline *)
6.170 fun rls_eq ((id1, (_, _)), (id2, (_, _))) = id1 = id2
6.171
6.172 fun insert_merge_rls (re as (id, (thyID, r1)) : rlss_elem) ys =
6.173 @@ -201,25 +201,25 @@
6.174 fun merge_rlss (s1, s2) = fold insert_merge_rls s1 s2;
6.175
6.176 (* used only for one hack TODO remove *)
6.177 -fun remove_rls id (Rls {id = _, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
6.178 +fun remove_rls id (Rule_Def.Repeat {id = _, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
6.179 rules = rs, errpatts = eps, scr = sc}) r =
6.180 - Rls {id = id, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
6.181 + Rule_Def.Repeat {id = id, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
6.182 rules = gen_rems eq_rule (rs, r),
6.183 errpatts = eps,
6.184 scr = sc}
6.185 - | remove_rls id (Seq {id = _, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
6.186 + | remove_rls id (Rule_Def.Seqence {id = _, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
6.187 rules = rs, errpatts = eps, scr = sc}) r =
6.188 - Seq {id = id, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
6.189 + Rule_Def.Seqence {id = id, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
6.190 rules = gen_rems eq_rule (rs, r),
6.191 errpatts = eps,
6.192 scr = sc}
6.193 - | remove_rls id (Rrls _) _ = raise ERROR ("remove_rls: not for reverse-rewrite-rule-set "^id)
6.194 + | remove_rls id (Rule_Def.Rrls _) _ = raise ERROR ("remove_rls: not for reverse-rewrite-rule-set "^id)
6.195 | remove_rls _ rls _ = raise ERROR ("remove_rls called with " ^ rls2str rls);
6.196
6.197 -fun get_rules Erls = []
6.198 - | get_rules (Rls {rules, ...}) = rules
6.199 - | get_rules (Seq {rules, ...}) = rules
6.200 - | get_rules (Rrls _) = [];
6.201 +fun get_rules Rule_Def.Empty = []
6.202 + | get_rules (Rule_Def.Repeat {rules, ...}) = rules
6.203 + | get_rules (Rule_Def.Seqence {rules, ...}) = rules
6.204 + | get_rules (Rule_Def.Rrls _) = [];
6.205
6.206
6.207 (**)end(**)
7.1 --- a/src/Tools/isac/Interpret/error-pattern.sml Sat Apr 04 12:11:32 2020 +0200
7.2 +++ b/src/Tools/isac/Interpret/error-pattern.sml Mon Apr 06 11:44:36 2020 +0200
7.3 @@ -9,12 +9,12 @@
7.4 val find_fillpatterns : Calc.T -> Rule.errpatID -> (Celem.fillpatID * term * thm * Selem.subs option) list
7.5 val is_exactly_equal : Calc.T -> string -> string * Tactic.input
7.6 val concat_deriv : 'a * ((term * term) list -> term * term -> bool) ->
7.7 - Rule_Set.rls -> Rule.rule list -> term -> term -> bool * (term * Rule.rule * (term * term list)) list
7.8 - val mk_tacis: Rule_Def.rew_ord' * 'a -> Rule_Set.rls -> term * Rule.rule * (term * term list) -> Tactic.input * Tactic.T * (Pos.pos' * (Istate.T * Proof.context))
7.9 + Rule_Set.T -> Rule.rule list -> term -> term -> bool * (term * Rule.rule * (term * term list)) list
7.10 + 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))
7.11 val fetchErrorpatterns : Tactic.input -> Rule.errpatID list
7.12 val check_for :
7.13 term * term ->
7.14 - term * (term * term) list -> (Rule.errpatID * term list * 'a list) list * Rule_Set.rls -> Rule.errpatID option
7.15 + term * (term * term) list -> (Rule.errpatID * term list * 'a list) list * Rule_Set.T -> Rule.errpatID option
7.16 val rule2thm'' : Rule.rule -> Celem.thm''
7.17 val rule2rls' : Rule.rule -> string
7.18 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
7.19 @@ -22,7 +22,7 @@
7.20 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
7.21 val dropwhile' : ('a -> 'b -> bool) -> 'a list -> 'b list -> 'a list * 'b list
7.22 val rev_deriv' : 'a * Rule.rule * ('b * 'c) -> 'b * Rule.rule * ('a * 'c)
7.23 - val check_err_patt : term * term -> Rule.subst -> Rule.errpatID * term -> Rule_Set.rls -> Rule.errpatID option
7.24 + val check_err_patt : term * term -> Rule.subst -> Rule.errpatID * term -> Rule_Set.T -> Rule.errpatID option
7.25 val get_fillform :
7.26 'a * (term * term) list -> 'b * term -> Rule.errpatID -> Celem.fillpat -> (Celem.fillpatID * term * 'b * 'a) option
7.27 val get_fillpats :
7.28 @@ -205,10 +205,10 @@
7.29 Celem.Hrls {thy_rls = (_, rls), ...} => rls
7.30 | _ => error "fetchErrorpatterns: uncovered case of get_the"
7.31 in case rls of
7.32 - Rule_Set.Rls {errpatts, ...} => errpatts
7.33 - | Rule_Set.Seq {errpatts, ...} => errpatts
7.34 + Rule_Def.Repeat {errpatts, ...} => errpatts
7.35 + | Rule_Set.Seqence {errpatts, ...} => errpatts
7.36 | Rule_Set.Rrls {errpatts, ...} => errpatts
7.37 - | Rule_Set.Erls => []
7.38 + | Rule_Set.Empty => []
7.39 end
7.40
7.41 (**)
8.1 --- a/src/Tools/isac/Interpret/istate.sml Sat Apr 04 12:11:32 2020 +0200
8.2 +++ b/src/Tools/isac/Interpret/istate.sml Mon Apr 06 11:44:36 2020 +0200
8.3 @@ -34,7 +34,7 @@
8.4
8.5 val set_form: term -> pstate -> pstate
8.6 val set_path: TermC.path -> pstate -> pstate
8.7 - val set_eval: Rule_Set.rls -> pstate -> pstate
8.8 + val set_eval: Rule_Set.T -> pstate -> pstate
8.9 val set_act: term -> pstate -> pstate
8.10 val set_or: asap -> pstate -> pstate
8.11 val set_found: pstate -> pstate
9.1 --- a/src/Tools/isac/Interpret/li-tool.sml Sat Apr 04 12:11:32 2020 +0200
9.2 +++ b/src/Tools/isac/Interpret/li-tool.sml Mon Apr 06 11:44:36 2020 +0200
9.3 @@ -14,15 +14,15 @@
9.4 val associate: Ctree.ctree -> Proof.context -> (Tactic.T * term (*..Prog_Tac*)) -> ass
9.5
9.6 val implicit_take : Program.T -> (term * term) list -> term option
9.7 - val init_pstate : Rule_Set.rls -> Proof.context -> Model.itm list -> Celem.metID ->
9.8 + val init_pstate : Rule_Set.T -> Proof.context -> Model.itm list -> Celem.metID ->
9.9 Istate.T * Proof.context * Program.T
9.10
9.11 - val get_simplifier : Calc.T -> Rule_Set.rls
9.12 + val get_simplifier : Calc.T -> Rule_Set.T
9.13 val resume_prog : Rule.theory' (*..for lookup in KEStore*) -> Pos.pos' -> Ctree.ctree ->
9.14 (Istate.T * Proof.context) * Program.T
9.15
9.16 val tac_from_prog : Ctree.ctree -> theory (*..for lookup in KEStore*) -> term -> Tactic.input
9.17 - val check_leaf : string -> Proof.context -> Rule_Set.rls -> (Env.T * (term option * term)) -> term ->
9.18 + val check_leaf : string -> Proof.context -> Rule_Set.T -> (Env.T * (term option * term)) -> term ->
9.19 Program.leaf * term option
9.20 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
9.21 (*NONE*)
10.1 --- a/src/Tools/isac/Interpret/rewtools.sml Sat Apr 04 12:11:32 2020 +0200
10.2 +++ b/src/Tools/isac/Interpret/rewtools.sml Mon Apr 06 11:44:36 2020 +0200
10.3 @@ -8,8 +8,8 @@
10.4 signature REWRITE_TOOLS =
10.5 sig
10.6 type deriv
10.7 - val contains_rule : Rule.rule -> Rule_Set.rls -> bool
10.8 - val atomic_appl_tacs : theory -> string -> Rule_Set.rls -> term -> Tactic.input -> Tactic.input list
10.9 + val contains_rule : Rule.rule -> Rule_Set.T -> bool
10.10 + val atomic_appl_tacs : theory -> string -> Rule_Set.T -> term -> Tactic.input -> Tactic.input list
10.11 val thy_containing_rls : Rule.theory' -> Rule_Set.rls' -> string * Rule.theory'
10.12 val thy_containing_cal : Rule.theory' -> Rule_Set.prog_calcID -> string * string
10.13 datatype contthy
10.14 @@ -27,9 +27,9 @@
10.15 val guh2filename : Celem.guh -> Celem.filename
10.16 val is_sym : Celem.thmID -> bool
10.17 val sym_drop : Celem.thmID -> Celem.thmID
10.18 - val sym_rls : Rule_Set.rls -> Rule_Set.rls
10.19 + val sym_rls : Rule_Set.T -> Rule_Set.T
10.20 val sym_rule : Rule.rule -> Rule.rule
10.21 - val thms_of_rls : Rule_Set.rls -> Rule.rule list
10.22 + val thms_of_rls : Rule_Set.T -> Rule.rule list
10.23 val theID2filename : Celem.theID -> Celem.filename
10.24 val no_thycontext : Celem.guh -> bool
10.25 val subs_from : Istate.T -> 'a -> Celem.guh -> Selem.subs
10.26 @@ -38,9 +38,9 @@
10.27 val context_thy : Calc.T -> Tactic.input -> contthy
10.28 val distinct_Thm : Rule.rule list -> Rule.rule list
10.29 val eq_Thms : string list -> Rule.rule -> bool
10.30 - val make_deriv : theory -> Rule_Set.rls -> Rule.rule list -> ((term * term) list -> term * term -> bool) ->
10.31 + val make_deriv : theory -> Rule_Set.T -> Rule.rule list -> ((term * term) list -> term * term -> bool) ->
10.32 term option -> term -> deriv
10.33 - val reverse_deriv : theory -> Rule_Set.rls -> Rule.rule list -> ((term * term) list -> term * term -> bool) ->
10.34 + val reverse_deriv : theory -> Rule_Set.T -> Rule.rule list -> ((term * term) list -> term * term -> bool) ->
10.35 term option -> term -> (Rule.rule * (term * term list)) list
10.36 val get_bdv_subst : term -> (term * term) list -> Selem.subs option * Rule.subst
10.37 val thy_containing_thm : string -> string * string
10.38 @@ -201,12 +201,12 @@
10.39
10.40 (*FIXXXXME.040219: detail has to handle Rls id="sym_..."
10.41 by applying make_deriv, rev_deriv'; see concat_deriv*)
10.42 -fun sym_rls Rule_Set.Erls = Rule_Set.Erls
10.43 - | sym_rls (Rule_Set.Rls {id, scr, calc, errpatts, erls, srls, rules, rew_ord, preconds}) =
10.44 - Rule_Set.Rls {id = "sym_" ^ id, scr = scr, calc = calc, errpatts = errpatts, erls = erls, srls = srls,
10.45 +fun sym_rls Rule_Set.Empty = Rule_Set.Empty
10.46 + | sym_rls (Rule_Def.Repeat {id, scr, calc, errpatts, erls, srls, rules, rew_ord, preconds}) =
10.47 + Rule_Def.Repeat {id = "sym_" ^ id, scr = scr, calc = calc, errpatts = errpatts, erls = erls, srls = srls,
10.48 rules = rules, rew_ord = rew_ord, preconds = preconds}
10.49 - | sym_rls (Rule_Set.Seq {id, scr, calc, errpatts, erls, srls, rules, rew_ord, preconds}) =
10.50 - Rule_Set.Seq {id = "sym_" ^ id, scr = scr, calc = calc, errpatts = errpatts, erls = erls, srls = srls,
10.51 + | sym_rls (Rule_Set.Seqence {id, scr, calc, errpatts, erls, srls, rules, rew_ord, preconds}) =
10.52 + Rule_Set.Seqence {id = "sym_" ^ id, scr = scr, calc = calc, errpatts = errpatts, erls = erls, srls = srls,
10.53 rules = rules, rew_ord = rew_ord, preconds = preconds}
10.54 | sym_rls (Rule_Set.Rrls {id, scr, calc, errpatts, erls, prepat, rew_ord}) =
10.55 Rule_Set.Rrls {id = "sym_" ^ id, scr = scr, calc = calc, errpatts = errpatts, erls = erls,
10.56 @@ -432,9 +432,9 @@
10.57 | thm_of_rule (Rule.Num_Calc _) = []
10.58 | thm_of_rule (Rule.Cal1 _) = []
10.59 | thm_of_rule (Rule.Rls_ rls) = thms_of_rls rls
10.60 -and thms_of_rls Rule_Set.Erls = []
10.61 - | thms_of_rls (Rule_Set.Rls {rules,...}) = (flat o (map thm_of_rule)) rules
10.62 - | thms_of_rls (Rule_Set.Seq {rules,...}) = (flat o (map thm_of_rule)) rules
10.63 +and thms_of_rls Rule_Set.Empty = []
10.64 + | thms_of_rls (Rule_Def.Repeat {rules,...}) = (flat o (map thm_of_rule)) rules
10.65 + | thms_of_rls (Rule_Set.Seqence {rules,...}) = (flat o (map thm_of_rule)) rules
10.66 | thms_of_rls (Rule_Set.Rrls _) = []
10.67
10.68 (* check if a rule is contained in a rule-set (recursivley down in Rls_);
10.69 @@ -469,9 +469,9 @@
10.70 | NONE => [])
10.71 | try_rew thy _ _ subst f (Rule.Rls_ rls) = filter_appl_rews thy subst f rls
10.72 | try_rew _ _ _ _ _ _ = error "try_rew: uncovered case"
10.73 -and filter_appl_rews thy subst f (Rule_Set.Rls {rew_ord = ro, erls, rules, ...}) =
10.74 +and filter_appl_rews thy subst f (Rule_Def.Repeat {rew_ord = ro, erls, rules, ...}) =
10.75 gen_distinct Tactic.eq_tac (flat (map (try_rew thy ro erls subst f) rules))
10.76 - | filter_appl_rews thy subst f (Rule_Set.Seq {rew_ord = ro, erls, rules,...}) =
10.77 + | filter_appl_rews thy subst f (Rule_Set.Seqence {rew_ord = ro, erls, rules,...}) =
10.78 gen_distinct Tactic.eq_tac (flat (map (try_rew thy ro erls subst f) rules))
10.79 | filter_appl_rews _ _ _ (Rule_Set.Rrls _) = []
10.80 | filter_appl_rews _ _ _ _ = error "filter_appl_rews: uncovered case"
11.1 --- a/src/Tools/isac/Knowledge/AlgEin.thy Sat Apr 04 12:11:32 2020 +0200
11.2 +++ b/src/Tools/isac/Knowledge/AlgEin.thy Mon Apr 06 11:44:36 2020 +0200
11.3 @@ -36,13 +36,13 @@
11.4 setup \<open>KEStore_Elems.add_mets
11.5 [Specify.prep_met thy "met_algein" [] Celem.e_metID
11.6 (["Berechnung"], [],
11.7 - {rew_ord'="tless_true", rls'= Rule_Set.Erls, calc = [], srls = Rule_Set.Erls, prls = Rule_Set.Erls, crls =Rule_Set.Erls,
11.8 - errpats = [], nrls = Rule_Set.Erls},
11.9 + {rew_ord'="tless_true", rls'= Rule_Set.Empty, calc = [], srls = Rule_Set.Empty, prls = Rule_Set.Empty, crls =Rule_Set.Empty,
11.10 + errpats = [], nrls = Rule_Set.Empty},
11.11 @{thm refl}),
11.12 Specify.prep_met thy "met_algein_numsym" [] Celem.e_metID
11.13 (["Berechnung","erstNumerisch"], [],
11.14 - {rew_ord'="tless_true", rls'= Rule_Set.Erls, calc = [], srls = Rule_Set.Erls, prls = Rule_Set.Erls, crls =Rule_Set.Erls,
11.15 - errpats = [], nrls = Rule_Set.Erls},
11.16 + {rew_ord'="tless_true", rls'= Rule_Set.Empty, calc = [], srls = Rule_Set.Empty, prls = Rule_Set.Empty, crls =Rule_Set.Empty,
11.17 + errpats = [], nrls = Rule_Set.Empty},
11.18 @{thm refl})]
11.19 \<close>
11.20
12.1 --- a/src/Tools/isac/Knowledge/Base_Tools.thy Sat Apr 04 12:11:32 2020 +0200
12.2 +++ b/src/Tools/isac/Knowledge/Base_Tools.thy Mon Apr 06 11:44:36 2020 +0200
12.3 @@ -131,14 +131,14 @@
12.4 Rule.Thm ("if_False",TermC.num_str @{thm if_False})];
12.5
12.6 val prog_expr = Auto_Prog.prep_rls @{theory} (Rule_Set.merge_rls "list_erls"
12.7 - (Rule_Set.Rls {id = "replaced", preconds = [], rew_ord = ("termlessI", termlessI),
12.8 - erls = Rule_Set.Rls {id = "list_elrs", preconds = [], rew_ord = ("termlessI", termlessI),
12.9 - erls = Rule_Set.e_rls, srls = Rule_Set.Erls, calc = [], errpatts = [],
12.10 + (Rule_Def.Repeat {id = "replaced", preconds = [], rew_ord = ("termlessI", termlessI),
12.11 + erls = Rule_Def.Repeat {id = "list_elrs", preconds = [], rew_ord = ("termlessI", termlessI),
12.12 + erls = Rule_Set.e_rls, srls = Rule_Set.Empty, calc = [], errpatts = [],
12.13 rules = [Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"),
12.14 Rule.Num_Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_")
12.15 (* ~~~~~~ for nth_Cons_*)],
12.16 scr = Rule.EmptyScr},
12.17 - srls = Rule_Set.Erls, calc = [], errpatts = [],
12.18 + srls = Rule_Set.Empty, calc = [], errpatts = [],
12.19 rules = [], scr = Rule.EmptyScr})
12.20 prog_expr);
12.21 \<close>
13.1 --- a/src/Tools/isac/Knowledge/Biegelinie.thy Sat Apr 04 12:11:32 2020 +0200
13.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy Mon Apr 06 11:44:36 2020 +0200
13.3 @@ -114,7 +114,7 @@
13.4 ML \<open>
13.5 (** methods **)
13.6
13.7 -val srls = Rule_Set.Rls {id="srls_IntegrierenUnd..",
13.8 +val srls = Rule_Def.Repeat {id="srls_IntegrierenUnd..",
13.9 preconds = [],
13.10 rew_ord = ("termlessI",termlessI),
13.11 erls = Rule_Set.append_rls "erls_in_srls_IntegrierenUnd.." Rule_Set.e_rls
13.12 @@ -123,7 +123,7 @@
13.13 (*2nd NTH_CONS pushes n+-1 into asms*)
13.14 Rule.Num_Calc("Groups.plus_class.plus", (**)eval_binop "#add_")
13.15 ],
13.16 - srls = Rule_Set.Erls, calc = [], errpatts = [],
13.17 + srls = Rule_Set.Empty, calc = [], errpatts = [],
13.18 rules = [Rule.Thm ("NTH_CONS",TermC.num_str @{thm NTH_CONS}),
13.19 Rule.Num_Calc("Groups.plus_class.plus", (**)eval_binop "#add_"),
13.20 Rule.Thm ("NTH_NIL",TermC.num_str @{thm NTH_NIL}),
13.21 @@ -134,7 +134,7 @@
13.22 scr = Rule.EmptyScr};
13.23
13.24 val srls2 =
13.25 - Rule_Set.Rls {id="srls_IntegrierenUnd..",
13.26 + Rule_Def.Repeat {id="srls_IntegrierenUnd..",
13.27 preconds = [],
13.28 rew_ord = ("termlessI",termlessI),
13.29 erls = Rule_Set.append_rls "erls_in_srls_IntegrierenUnd.." Rule_Set.e_rls
13.30 @@ -143,7 +143,7 @@
13.31 (*2nd NTH_CONS pushes n+-1 into asms*)
13.32 Rule.Num_Calc("Groups.plus_class.plus", (**)eval_binop "#add_")
13.33 ],
13.34 - srls = Rule_Set.Erls, calc = [], errpatts = [],
13.35 + srls = Rule_Set.Empty, calc = [], errpatts = [],
13.36 rules = [Rule.Thm ("NTH_CONS",TermC.num_str @{thm NTH_CONS}),
13.37 Rule.Num_Calc("Groups.plus_class.plus", (**)eval_binop "#add_"),
13.38 Rule.Thm ("NTH_NIL", TermC.num_str @{thm NTH_NIL}),
13.39 @@ -165,8 +165,8 @@
13.40 setup \<open>KEStore_Elems.add_mets
13.41 [Specify.prep_met @{theory} "met_biege" [] Celem.e_metID
13.42 (["IntegrierenUndKonstanteBestimmen"], [],
13.43 - {rew_ord'="tless_true", rls'= Rule_Set.Erls, calc = [], srls = Rule_Set.Erls, prls = Rule_Set.Erls, crls =Rule_Set.Erls,
13.44 - errpats = [], nrls = Rule_Set.Erls},
13.45 + {rew_ord'="tless_true", rls'= Rule_Set.Empty, calc = [], srls = Rule_Set.Empty, prls = Rule_Set.Empty, crls =Rule_Set.Empty,
13.46 + errpats = [], nrls = Rule_Set.Empty},
13.47 @{thm refl})]
13.48 \<close>
13.49 subsection \<open>Sub-problem "integrate and determine constants", nicely modularised\<close>
13.50 @@ -205,28 +205,28 @@
13.51 Rule.Thm ("last_thmI",TermC.num_str @{thm last_thmI}),
13.52 Rule.Thm ("if_True",TermC.num_str @{thm if_True}),
13.53 Rule.Thm ("if_False",TermC.num_str @{thm if_False})],
13.54 - prls = Rule_Set.Erls, crls = Atools_erls, errpats = [], nrls = Rule_Set.Erls},
13.55 + prls = Rule_Set.Empty, crls = Atools_erls, errpats = [], nrls = Rule_Set.Empty},
13.56 @{thm biegelinie.simps})]
13.57 \<close>
13.58 setup \<open>KEStore_Elems.add_mets
13.59 [Specify.prep_met @{theory} "met_biege_intconst_2" [] Celem.e_metID
13.60 (["IntegrierenUndKonstanteBestimmen","2xIntegrieren"], [],
13.61 - {rew_ord'="tless_true", rls'=Rule_Set.Erls, calc = [], srls = Rule_Set.e_rls, prls=Rule_Set.e_rls, crls = Atools_erls,
13.62 + {rew_ord'="tless_true", rls'=Rule_Set.Empty, calc = [], srls = Rule_Set.e_rls, prls=Rule_Set.e_rls, crls = Atools_erls,
13.63 errpats = [], nrls = Rule_Set.e_rls},
13.64 @{thm refl}),
13.65 Specify.prep_met @{theory} "met_biege_intconst_4" [] Celem.e_metID
13.66 (["IntegrierenUndKonstanteBestimmen","4x4System"], [],
13.67 - {rew_ord'="tless_true", rls'=Rule_Set.Erls, calc = [], srls = Rule_Set.e_rls, prls=Rule_Set.e_rls, crls = Atools_erls,
13.68 + {rew_ord'="tless_true", rls'=Rule_Set.Empty, calc = [], srls = Rule_Set.e_rls, prls=Rule_Set.e_rls, crls = Atools_erls,
13.69 errpats = [], nrls = Rule_Set.e_rls},
13.70 @{thm refl}),
13.71 Specify.prep_met @{theory} "met_biege_intconst_1" [] Celem.e_metID
13.72 (["IntegrierenUndKonstanteBestimmen","1xIntegrieren"], [],
13.73 - {rew_ord'="tless_true", rls'=Rule_Set.Erls, calc = [], srls = Rule_Set.e_rls, prls=Rule_Set.e_rls, crls = Atools_erls,
13.74 + {rew_ord'="tless_true", rls'=Rule_Set.Empty, calc = [], srls = Rule_Set.e_rls, prls=Rule_Set.e_rls, crls = Atools_erls,
13.75 errpats = [], nrls = Rule_Set.e_rls},
13.76 @{thm refl}),
13.77 Specify.prep_met @{theory} "met_biege2" [] Celem.e_metID
13.78 (["Biegelinien"], [],
13.79 - {rew_ord'="tless_true", rls'=Rule_Set.Erls, calc = [], srls = Rule_Set.e_rls, prls=Rule_Set.e_rls, crls = Atools_erls,
13.80 + {rew_ord'="tless_true", rls'=Rule_Set.Empty, calc = [], srls = Rule_Set.e_rls, prls=Rule_Set.e_rls, crls = Atools_erls,
13.81 errpats = [], nrls = Rule_Set.e_rls},
13.82 @{thm refl})]
13.83 \<close>
13.84 @@ -299,7 +299,7 @@
13.85 (["Biegelinien", "setzeRandbedingungenEin"],
13.86 [("#Given" , ["Funktionen fun_s", "Randbedingungen r_b"]),
13.87 ("#Find" , ["Gleichungen equs'''"])],
13.88 - {rew_ord'="tless_true", rls'=Rule_Set.Erls, calc = [], srls = srls2, prls=Rule_Set.e_rls, crls = Atools_erls,
13.89 + {rew_ord'="tless_true", rls'=Rule_Set.Empty, calc = [], srls = srls2, prls=Rule_Set.e_rls, crls = Atools_erls,
13.90 errpats = [], nrls = Rule_Set.e_rls},
13.91 @{thm setzte_randbedingungen.simps})]
13.92 \<close>
13.93 @@ -323,7 +323,7 @@
13.94 (["Equation","fromFunction"],
13.95 [("#Given" ,["functionEq fu_n","substitution su_b"]),
13.96 ("#Find" ,["equality equ'''"])],
13.97 - {rew_ord'="tless_true", rls'=Rule_Set.Erls, calc = [],
13.98 + {rew_ord'="tless_true", rls'=Rule_Set.Empty, calc = [],
13.99 srls = Rule_Set.append_rls "srls_in_EquationfromFunc" Rule_Set.e_rls
13.100 [Rule.Num_Calc("Prog_Expr.lhs", Prog_Expr.eval_lhs "eval_lhs_"),
13.101 Rule.Num_Calc("Prog_Expr.argument'_in", Prog_Expr.eval_argument_in "Prog_Expr.argument'_in")],
14.1 --- a/src/Tools/isac/Knowledge/Diff.thy Sat Apr 04 12:11:32 2020 +0200
14.2 +++ b/src/Tools/isac/Knowledge/Diff.thy Mon Apr 06 11:44:36 2020 +0200
14.3 @@ -106,7 +106,7 @@
14.4
14.5 (*.converts a term such that differentiation works optimally.*)
14.6 val diff_conv =
14.7 - Rule_Set.Rls {id="diff_conv",
14.8 + Rule_Def.Repeat {id="diff_conv",
14.9 preconds = [],
14.10 rew_ord = ("termlessI",termlessI),
14.11 erls = Rule_Set.append_rls "erls_diff_conv" Rule_Set.e_rls
14.12 @@ -117,7 +117,7 @@
14.13 Rule.Thm ("and_true",TermC.num_str @{thm and_true}),
14.14 Rule.Thm ("and_false",TermC.num_str @{thm and_false})
14.15 ],
14.16 - srls = Rule_Set.Erls, calc = [], errpatts = [],
14.17 + srls = Rule_Set.Empty, calc = [], errpatts = [],
14.18 rules =
14.19 [Rule.Thm ("frac_conv", TermC.num_str @{thm frac_conv}),
14.20 (*"?bdv occurs_in ?b \<Longrightarrow> 0 < ?n \<Longrightarrow> ?a / ?b ^^^ ?n = ?a * ?b ^^^ - ?n"*)
14.21 @@ -144,13 +144,13 @@
14.22 ML \<open>
14.23 (*.beautifies a term after differentiation.*)
14.24 val diff_sym_conv =
14.25 - Rule_Set.Rls {id="diff_sym_conv",
14.26 + Rule_Def.Repeat {id="diff_sym_conv",
14.27 preconds = [],
14.28 rew_ord = ("termlessI",termlessI),
14.29 erls = Rule_Set.append_rls "erls_diff_sym_conv" Rule_Set.e_rls
14.30 [Rule.Num_Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_")
14.31 ],
14.32 - srls = Rule_Set.Erls, calc = [], errpatts = [],
14.33 + srls = Rule_Set.Empty, calc = [], errpatts = [],
14.34 rules = [Rule.Thm ("frac_sym_conv", TermC.num_str @{thm frac_sym_conv}),
14.35 Rule.Thm ("sqrt_sym_conv", TermC.num_str @{thm sqrt_sym_conv}),
14.36 Rule.Thm ("root_sym_conv", TermC.num_str @{thm root_sym_conv}),
14.37 @@ -169,11 +169,11 @@
14.38
14.39 (*..*)
14.40 val srls_diff =
14.41 - Rule_Set.Rls {id="srls_differentiate..",
14.42 + Rule_Def.Repeat {id="srls_differentiate..",
14.43 preconds = [],
14.44 rew_ord = ("termlessI",termlessI),
14.45 erls = Rule_Set.e_rls,
14.46 - srls = Rule_Set.Erls, calc = [], errpatts = [],
14.47 + srls = Rule_Set.Empty, calc = [], errpatts = [],
14.48 rules = [Rule.Num_Calc("Prog_Expr.lhs", Prog_Expr.eval_lhs "eval_lhs_"),
14.49 Rule.Num_Calc("Prog_Expr.rhs", Prog_Expr.eval_rhs "eval_rhs_"),
14.50 Rule.Num_Calc("Diff.primed", eval_primed "Diff.primed")
14.51 @@ -195,8 +195,8 @@
14.52
14.53 (*.rules for differentiation, _no_ simplification.*)
14.54 val diff_rules =
14.55 - Rule_Set.Rls {id="diff_rules", preconds = [], rew_ord = ("termlessI",termlessI),
14.56 - erls = erls_diff, srls = Rule_Set.Erls, calc = [], errpatts = [],
14.57 + Rule_Def.Repeat {id="diff_rules", preconds = [], rew_ord = ("termlessI",termlessI),
14.58 + erls = erls_diff, srls = Rule_Set.Empty, calc = [], errpatts = [],
14.59 rules = [Rule.Thm ("diff_sum",TermC.num_str @{thm diff_sum}),
14.60 Rule.Thm ("diff_dif",TermC.num_str @{thm diff_dif}),
14.61 Rule.Thm ("diff_prod_const",TermC.num_str @{thm diff_prod_const}),
14.62 @@ -224,9 +224,9 @@
14.63 ML \<open>
14.64 (*.normalisation for checking user-input.*)
14.65 val norm_diff =
14.66 - Rule_Set.Rls
14.67 + Rule_Def.Repeat
14.68 {id="norm_diff", preconds = [], rew_ord = ("termlessI",termlessI),
14.69 - erls = Rule_Set.Erls, srls = Rule_Set.Erls, calc = [], errpatts = [],
14.70 + erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
14.71 rules = [Rule.Rls_ diff_rules, Rule.Rls_ norm_Poly ],
14.72 scr = Rule.EmptyScr};
14.73 \<close>
15.1 --- a/src/Tools/isac/Knowledge/DiffApp.thy Sat Apr 04 12:11:32 2020 +0200
15.2 +++ b/src/Tools/isac/Knowledge/DiffApp.thy Mon Apr 06 11:44:36 2020 +0200
15.3 @@ -35,8 +35,8 @@
15.4 val thy = @{theory};
15.5
15.6 val eval_rls = prep_rls' (
15.7 - Rule_Set.Rls {id = "eval_rls", preconds = [], rew_ord = ("termlessI", termlessI),
15.8 - erls = Rule_Set.e_rls, srls = Rule_Set.Erls, calc = [], errpatts = [],
15.9 + Rule_Def.Repeat {id = "eval_rls", preconds = [], rew_ord = ("termlessI", termlessI),
15.10 + erls = Rule_Set.e_rls, srls = Rule_Set.Empty, calc = [], errpatts = [],
15.11 rules = [Rule.Thm ("refl", TermC.num_str @{thm refl}),
15.12 Rule.Thm ("order_refl", TermC.num_str @{thm order_refl}),
15.13 Rule.Thm ("radd_left_cancel_le", TermC.num_str @{thm radd_left_cancel_le}),
16.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Sat Apr 04 12:11:32 2020 +0200
16.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Mon Apr 06 11:44:36 2020 +0200
16.3 @@ -170,10 +170,10 @@
16.4
16.5 (*.adapted from 'order_add_mult_in' by just replacing the rew_ord.*)
16.6 val order_add_mult_System =
16.7 - Rule_Set.Rls{id = "order_add_mult_System", preconds = [],
16.8 + Rule_Def.Repeat{id = "order_add_mult_System", preconds = [],
16.9 rew_ord = ("ord_simplify_System",
16.10 ord_simplify_System false @{theory "Integrate"}),
16.11 - erls = Rule_Set.e_rls,srls = Rule_Set.Erls, calc = [], errpatts = [],
16.12 + erls = Rule_Set.e_rls,srls = Rule_Set.Empty, calc = [], errpatts = [],
16.13 rules = [Rule.Thm ("mult_commute",TermC.num_str @{thm mult.commute}),
16.14 (* z * w = w * z *)
16.15 Rule.Thm ("real_mult_left_commute",TermC.num_str @{thm real_mult_left_commute}),
16.16 @@ -194,9 +194,9 @@
16.17 #1 using 'ord_simplify_System' in 'order_add_mult_System'
16.18 #2 NOT using common_nominator_p .*)
16.19 val norm_System_noadd_fractions =
16.20 - Rule_Set.Rls {id = "norm_System_noadd_fractions", preconds = [],
16.21 + Rule_Def.Repeat {id = "norm_System_noadd_fractions", preconds = [],
16.22 rew_ord = ("dummy_ord",Rule.dummy_ord),
16.23 - erls = norm_rat_erls, srls = Rule_Set.Erls, calc = [], errpatts = [],
16.24 + erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
16.25 rules = [(*sequence given by operator precedence*)
16.26 Rule.Rls_ discard_minus,
16.27 Rule.Rls_ powers,
16.28 @@ -215,9 +215,9 @@
16.29 (*.adapted from 'norm_Rational' by
16.30 *1* using 'ord_simplify_System' in 'order_add_mult_System'.*)
16.31 val norm_System =
16.32 - Rule_Set.Rls {id = "norm_System", preconds = [],
16.33 + Rule_Def.Repeat {id = "norm_System", preconds = [],
16.34 rew_ord = ("dummy_ord",Rule.dummy_ord),
16.35 - erls = norm_rat_erls, srls = Rule_Set.Erls, calc = [], errpatts = [],
16.36 + erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
16.37 rules = [(*sequence given by operator precedence*)
16.38 Rule.Rls_ discard_minus,
16.39 Rule.Rls_ powers,
16.40 @@ -243,9 +243,9 @@
16.41 *3* discard_parentheses only for (.*(.*.))
16.42 analoguous to simplify_Integral .*)
16.43 val simplify_System_parenthesized =
16.44 - Rule_Set.Seq {id = "simplify_System_parenthesized", preconds = []:term list,
16.45 + Rule_Set.Seqence {id = "simplify_System_parenthesized", preconds = []:term list,
16.46 rew_ord = ("dummy_ord", Rule.dummy_ord),
16.47 - erls = Atools_erls, srls = Rule_Set.Erls, calc = [], errpatts = [],
16.48 + erls = Atools_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
16.49 rules = [Rule.Thm ("distrib_right",TermC.num_str @{thm distrib_right}),
16.50 (*"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"*)
16.51 Rule.Thm ("add_divide_distrib",TermC.num_str @{thm add_divide_distrib}),
16.52 @@ -268,9 +268,9 @@
16.53 *1* ord_simplify_System instead of termlessI .*)
16.54 (*TODO.WN051031 ^^^^^^^^^^ should be in EACH rls contained *)
16.55 val simplify_System =
16.56 - Rule_Set.Seq {id = "simplify_System", preconds = []:term list,
16.57 + Rule_Set.Seqence {id = "simplify_System", preconds = []:term list,
16.58 rew_ord = ("dummy_ord", Rule.dummy_ord),
16.59 - erls = Atools_erls, srls = Rule_Set.Erls, calc = [], errpatts = [],
16.60 + erls = Atools_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
16.61 rules = [Rule.Rls_ norm_Rational,
16.62 Rule.Rls_ (*order_add_mult_in*) norm_System (**1**),
16.63 Rule.Rls_ discard_parentheses,
16.64 @@ -288,14 +288,14 @@
16.65 \<close>
16.66 ML \<open>
16.67 val isolate_bdvs =
16.68 - Rule_Set.Rls {id="isolate_bdvs", preconds = [],
16.69 + Rule_Def.Repeat {id="isolate_bdvs", preconds = [],
16.70 rew_ord = ("e_rew_ord", Rule.e_rew_ord),
16.71 erls = Rule_Set.append_rls "erls_isolate_bdvs" Rule_Set.e_rls
16.72 [(Rule.Num_Calc ("EqSystem.occur'_exactly'_in",
16.73 eval_occur_exactly_in
16.74 "#eval_occur_exactly_in_"))
16.75 ],
16.76 - srls = Rule_Set.Erls, calc = [], errpatts = [],
16.77 + srls = Rule_Set.Empty, calc = [], errpatts = [],
16.78 rules =
16.79 [Rule.Thm ("commute_0_equality", TermC.num_str @{thm commute_0_equality}),
16.80 Rule.Thm ("separate_bdvs_add", TermC.num_str @{thm separate_bdvs_add}),
16.81 @@ -304,7 +304,7 @@
16.82 \<close>
16.83 ML \<open>
16.84 val isolate_bdvs_4x4 =
16.85 - Rule_Set.Rls {id="isolate_bdvs_4x4", preconds = [],
16.86 + Rule_Def.Repeat {id="isolate_bdvs_4x4", preconds = [],
16.87 rew_ord = ("e_rew_ord", Rule.e_rew_ord),
16.88 erls = Rule_Set.append_rls
16.89 "erls_isolate_bdvs_4x4" Rule_Set.e_rls
16.90 @@ -315,7 +315,7 @@
16.91 Rule.Thm ("not_true",TermC.num_str @{thm not_true}),
16.92 Rule.Thm ("not_false",TermC.num_str @{thm not_false})
16.93 ],
16.94 - srls = Rule_Set.Erls, calc = [], errpatts = [],
16.95 + srls = Rule_Set.Empty, calc = [], errpatts = [],
16.96 rules = [Rule.Thm ("commute_0_equality", TermC.num_str @{thm commute_0_equality}),
16.97 Rule.Thm ("separate_bdvs0", TermC.num_str @{thm separate_bdvs0}),
16.98 Rule.Thm ("separate_bdvs_add1", TermC.num_str @{thm separate_bdvs_add1}),
16.99 @@ -329,20 +329,20 @@
16.100 (*.order the equations in a system such, that a triangular system (if any)
16.101 appears as [..c_4 = .., ..., ..., ..c_1 + ..c_2 + ..c_3 ..c_4 = ..].*)
16.102 val order_system =
16.103 - Rule_Set.Rls {id="order_system", preconds = [],
16.104 + Rule_Def.Repeat {id="order_system", preconds = [],
16.105 rew_ord = ("ord_simplify_System",
16.106 ord_simplify_System false thy),
16.107 - erls = Rule_Set.Erls, srls = Rule_Set.Erls, calc = [], errpatts = [],
16.108 + erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
16.109 rules = [Rule.Thm ("order_system_NxN", TermC.num_str @{thm order_system_NxN})
16.110 ],
16.111 scr = Rule.EmptyScr};
16.112
16.113 val prls_triangular =
16.114 - Rule_Set.Rls {id="prls_triangular", preconds = [],
16.115 + Rule_Def.Repeat {id="prls_triangular", preconds = [],
16.116 rew_ord = ("e_rew_ord", Rule.e_rew_ord),
16.117 - erls = Rule_Set.Rls {id="erls_prls_triangular", preconds = [],
16.118 + erls = Rule_Def.Repeat {id="erls_prls_triangular", preconds = [],
16.119 rew_ord = ("e_rew_ord", Rule.e_rew_ord),
16.120 - erls = Rule_Set.Erls, srls = Rule_Set.Erls, calc = [], errpatts = [],
16.121 + erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
16.122 rules = [(*for precond NTH_CONS ...*)
16.123 Rule.Num_Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
16.124 Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_")
16.125 @@ -350,7 +350,7 @@
16.126 '+' into precondition !*)
16.127 ],
16.128 scr = Rule.EmptyScr},
16.129 - srls = Rule_Set.Erls, calc = [], errpatts = [],
16.130 + srls = Rule_Set.Empty, calc = [], errpatts = [],
16.131 rules = [Rule.Thm ("NTH_CONS",TermC.num_str @{thm NTH_CONS}),
16.132 Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"),
16.133 Rule.Thm ("NTH_NIL",TermC.num_str @{thm NTH_NIL}),
16.134 @@ -367,11 +367,11 @@
16.135 (*WN060914 quickly created for 4x4;
16.136 more similarity to prls_triangular desirable*)
16.137 val prls_triangular4 =
16.138 - Rule_Set.Rls {id="prls_triangular4", preconds = [],
16.139 + Rule_Def.Repeat {id="prls_triangular4", preconds = [],
16.140 rew_ord = ("e_rew_ord", Rule.e_rew_ord),
16.141 - erls = Rule_Set.Rls {id="erls_prls_triangular4", preconds = [],
16.142 + erls = Rule_Def.Repeat {id="erls_prls_triangular4", preconds = [],
16.143 rew_ord = ("e_rew_ord", Rule.e_rew_ord),
16.144 - erls = Rule_Set.Erls, srls = Rule_Set.Erls, calc = [], errpatts = [],
16.145 + erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
16.146 rules = [(*for precond NTH_CONS ...*)
16.147 Rule.Num_Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
16.148 Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_")
16.149 @@ -379,7 +379,7 @@
16.150 '+' into precondition !*)
16.151 ],
16.152 scr = Rule.EmptyScr},
16.153 - srls = Rule_Set.Erls, calc = [], errpatts = [],
16.154 + srls = Rule_Set.Empty, calc = [], errpatts = [],
16.155 rules = [Rule.Thm ("NTH_CONS",TermC.num_str @{thm NTH_CONS}),
16.156 Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"),
16.157 Rule.Thm ("NTH_NIL",TermC.num_str @{thm NTH_NIL}),
16.158 @@ -492,7 +492,7 @@
16.159
16.160 ML \<open>
16.161 (*this is for NTH only*)
16.162 -val srls = Rule_Set.Rls {id="srls_normalise_4x4",
16.163 +val srls = Rule_Def.Repeat {id="srls_normalise_4x4",
16.164 preconds = [],
16.165 rew_ord = ("termlessI",termlessI),
16.166 erls = Rule_Set.append_rls "erls_in_srls_IntegrierenUnd.." Rule_Set.e_rls
16.167 @@ -501,7 +501,7 @@
16.168 (*2nd NTH_CONS pushes n+-1 into asms*)
16.169 Rule.Num_Calc("Groups.plus_class.plus", (**)eval_binop "#add_")
16.170 ],
16.171 - srls = Rule_Set.Erls, calc = [], errpatts = [],
16.172 + srls = Rule_Set.Empty, calc = [], errpatts = [],
16.173 rules = [Rule.Thm ("NTH_CONS",TermC.num_str @{thm NTH_CONS}),
16.174 Rule.Num_Calc("Groups.plus_class.plus", (**)eval_binop "#add_"),
16.175 Rule.Thm ("NTH_NIL",TermC.num_str @{thm NTH_NIL})],
16.176 @@ -512,13 +512,13 @@
16.177 setup \<open>KEStore_Elems.add_mets
16.178 [Specify.prep_met thy "met_eqsys" [] Celem.e_metID
16.179 (["EqSystem"], [],
16.180 - {rew_ord'="tless_true", rls' = Rule_Set.Erls, calc = [], srls = Rule_Set.Erls, prls = Rule_Set.Erls, crls = Rule_Set.Erls,
16.181 - errpats = [], nrls = Rule_Set.Erls},
16.182 + {rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [], srls = Rule_Set.Empty, prls = Rule_Set.Empty, crls = Rule_Set.Empty,
16.183 + errpats = [], nrls = Rule_Set.Empty},
16.184 @{thm refl}),
16.185 Specify.prep_met thy "met_eqsys_topdown" [] Celem.e_metID
16.186 (["EqSystem","top_down_substitution"], [],
16.187 - {rew_ord'="tless_true", rls' = Rule_Set.Erls, calc = [], srls = Rule_Set.Erls, prls = Rule_Set.Erls, crls = Rule_Set.Erls,
16.188 - errpats = [], nrls = Rule_Set.Erls},
16.189 + {rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [], srls = Rule_Set.Empty, prls = Rule_Set.Empty, crls = Rule_Set.Empty,
16.190 + errpats = [], nrls = Rule_Set.Empty},
16.191 @{thm refl})]
16.192 \<close>
16.193
16.194 @@ -549,19 +549,19 @@
16.195 ["(tl v_s) from v_s occur_exactly_in (NTH 1 (e_s::bool list))",
16.196 " v_s from v_s occur_exactly_in (NTH 2 (e_s::bool list))"]),
16.197 ("#Find" ,["solution ss'''"])],
16.198 - {rew_ord'="ord_simplify_System", rls' = Rule_Set.Erls, calc = [],
16.199 + {rew_ord'="ord_simplify_System", rls' = Rule_Set.Empty, calc = [],
16.200 srls = Rule_Set.append_rls "srls_top_down_2x2" Rule_Set.e_rls
16.201 [Rule.Thm ("hd_thm",TermC.num_str @{thm hd_thm}),
16.202 Rule.Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}),
16.203 Rule.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil})],
16.204 - prls = prls_triangular, crls = Rule_Set.Erls, errpats = [], nrls = Rule_Set.Erls},
16.205 + prls = prls_triangular, crls = Rule_Set.Empty, errpats = [], nrls = Rule_Set.Empty},
16.206 @{thm solve_system.simps})]
16.207 \<close>
16.208 setup \<open>KEStore_Elems.add_mets
16.209 [Specify.prep_met thy "met_eqsys_norm" [] Celem.e_metID
16.210 (["EqSystem", "normalise"], [],
16.211 - {rew_ord'="tless_true", rls' = Rule_Set.Erls, calc = [], srls = Rule_Set.Erls, prls = Rule_Set.Erls, crls = Rule_Set.Erls,
16.212 - errpats = [], nrls = Rule_Set.Erls},
16.213 + {rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [], srls = Rule_Set.Empty, prls = Rule_Set.Empty, crls = Rule_Set.Empty,
16.214 + errpats = [], nrls = Rule_Set.Empty},
16.215 @{thm refl})]
16.216 \<close>
16.217
16.218 @@ -584,12 +584,12 @@
16.219 (["EqSystem","normalise","2x2"],
16.220 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
16.221 ("#Find" ,["solution ss'''"])],
16.222 - {rew_ord'="tless_true", rls' = Rule_Set.Erls, calc = [],
16.223 + {rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [],
16.224 srls = Rule_Set.append_rls "srls_normalise_2x2" Rule_Set.e_rls
16.225 [Rule.Thm ("hd_thm",TermC.num_str @{thm hd_thm}),
16.226 Rule.Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}),
16.227 Rule.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil})],
16.228 - prls = Rule_Set.Erls, crls = Rule_Set.Erls, errpats = [], nrls = Rule_Set.Erls},
16.229 + prls = Rule_Set.Empty, crls = Rule_Set.Empty, errpats = [], nrls = Rule_Set.Empty},
16.230 @{thm solve_system2.simps})]
16.231 \<close>
16.232
16.233 @@ -616,12 +616,12 @@
16.234 (["EqSystem","normalise","4x4"],
16.235 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
16.236 ("#Find" ,["solution ss'''"])],
16.237 - {rew_ord'="tless_true", rls' = Rule_Set.Erls, calc = [],
16.238 + {rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [],
16.239 srls = Rule_Set.append_rls "srls_normalise_4x4" srls
16.240 [Rule.Thm ("hd_thm",TermC.num_str @{thm hd_thm}),
16.241 Rule.Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}),
16.242 Rule.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil})],
16.243 - prls = Rule_Set.Erls, crls = Rule_Set.Erls, errpats = [], nrls = Rule_Set.Erls},
16.244 + prls = Rule_Set.Empty, crls = Rule_Set.Empty, errpats = [], nrls = Rule_Set.Empty},
16.245 (*STOPPED.WN06? met ["EqSystem","normalise","4x4"] #>#>#>#>#>#>#>#>#>#>#>#>#>@*)
16.246 @{thm solve_system3.simps})]
16.247 \<close>
16.248 @@ -653,11 +653,11 @@
16.249 "(NTH 3 (v_s::real list)) occurs_in (NTH 3 (e_s::bool list))",
16.250 "(NTH 4 (v_s::real list)) occurs_in (NTH 4 (e_s::bool list))"]),
16.251 ("#Find", ["solution ss'''"])],
16.252 - {rew_ord'="ord_simplify_System", rls' = Rule_Set.Erls, calc = [],
16.253 + {rew_ord'="ord_simplify_System", rls' = Rule_Set.Empty, calc = [],
16.254 srls = Rule_Set.append_rls "srls_top_down_4x4" srls [],
16.255 prls = Rule_Set.append_rls "prls_tri_4x4_lin_sys" prls_triangular
16.256 [Rule.Num_Calc ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in "")],
16.257 - crls = Rule_Set.Erls, errpats = [], nrls = Rule_Set.Erls},
16.258 + crls = Rule_Set.Empty, errpats = [], nrls = Rule_Set.Empty},
16.259 (*FIXXXXME.WN060916: this script works ONLY for exp 7.79 #>#>#>#>#>#>#>#>#>#>*)
16.260 @{thm solve_system4.simps})]
16.261 \<close>
17.1 --- a/src/Tools/isac/Knowledge/Equation.thy Sat Apr 04 12:11:32 2020 +0200
17.2 +++ b/src/Tools/isac/Knowledge/Equation.thy Mon Apr 06 11:44:36 2020 +0200
17.3 @@ -83,7 +83,7 @@
17.4 setup \<open>KEStore_Elems.add_mets
17.5 [Specify.prep_met thy "met_equ" [] Celem.e_metID
17.6 (["Equation"], [],
17.7 - {rew_ord'="tless_true", rls'=Rule_Set.Erls, calc = [], srls = Rule_Set.e_rls, prls=Rule_Set.e_rls, crls = Atools_erls,
17.8 + {rew_ord'="tless_true", rls'=Rule_Set.Empty, calc = [], srls = Rule_Set.e_rls, prls=Rule_Set.e_rls, crls = Atools_erls,
17.9 errpats = [], nrls = Rule_Set.e_rls},
17.10 @{thm refl})]
17.11 \<close>
18.1 --- a/src/Tools/isac/Knowledge/InsSort.thy Sat Apr 04 12:11:32 2020 +0200
18.2 +++ b/src/Tools/isac/Knowledge/InsSort.thy Mon Apr 06 11:44:36 2020 +0200
18.3 @@ -47,7 +47,7 @@
18.4 section \<open>rulesets\<close>
18.5 ML \<open>
18.6 val ins_sort =
18.7 - Rule_Set.Rls {
18.8 + Rule_Def.Repeat {
18.9 id = "ins_sort", preconds = [], rew_ord = ("tless_true", tless_true), erls = Rule_Set.e_rls,
18.10 srls = Rule_Set.e_rls, calc = [], rules = [
18.11 Rule.Thm ("xfoldr_Nil",(*num_str*) @{thm xfoldr_Nil} (* foldr ?f [] = id *)),
19.1 --- a/src/Tools/isac/Knowledge/Integrate.thy Sat Apr 04 12:11:32 2020 +0200
19.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy Mon Apr 06 11:44:36 2020 +0200
19.3 @@ -110,20 +110,20 @@
19.4
19.5 (*.rulesets for integration.*)
19.6 val integration_rules =
19.7 - Rule_Set.Rls {id="integration_rules", preconds = [],
19.8 + Rule_Def.Repeat {id="integration_rules", preconds = [],
19.9 rew_ord = ("termlessI",termlessI),
19.10 - erls = Rule_Set.Rls {id="conditions_in_integration_rules",
19.11 + erls = Rule_Def.Repeat {id="conditions_in_integration_rules",
19.12 preconds = [],
19.13 rew_ord = ("termlessI",termlessI),
19.14 - erls = Rule_Set.Erls,
19.15 - srls = Rule_Set.Erls, calc = [], errpatts = [],
19.16 + erls = Rule_Set.Empty,
19.17 + srls = Rule_Set.Empty, calc = [], errpatts = [],
19.18 rules = [(*for rewriting conditions in Thm's*)
19.19 Rule.Num_Calc ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in "#occurs_in_"),
19.20 Rule.Thm ("not_true", TermC.num_str @{thm not_true}),
19.21 Rule.Thm ("not_false",@{thm not_false})
19.22 ],
19.23 scr = Rule.EmptyScr},
19.24 - srls = Rule_Set.Erls, calc = [], errpatts = [],
19.25 + srls = Rule_Set.Empty, calc = [], errpatts = [],
19.26 rules = [
19.27 Rule.Thm ("integral_const", TermC.num_str @{thm integral_const}),
19.28 Rule.Thm ("integral_var", TermC.num_str @{thm integral_var}),
19.29 @@ -136,13 +136,13 @@
19.30 \<close>
19.31 ML \<open>
19.32 val add_new_c =
19.33 - Rule_Set.Seq {id="add_new_c", preconds = [],
19.34 + Rule_Set.Seqence {id="add_new_c", preconds = [],
19.35 rew_ord = ("termlessI",termlessI),
19.36 - erls = Rule_Set.Rls {id="conditions_in_add_new_c",
19.37 + erls = Rule_Def.Repeat {id="conditions_in_add_new_c",
19.38 preconds = [],
19.39 rew_ord = ("termlessI",termlessI),
19.40 - erls = Rule_Set.Erls,
19.41 - srls = Rule_Set.Erls, calc = [], errpatts = [],
19.42 + erls = Rule_Set.Empty,
19.43 + srls = Rule_Set.Empty, calc = [], errpatts = [],
19.44 rules = [Rule.Num_Calc ("Prog_Expr.matches", Prog_Expr.eval_matches""),
19.45 Rule.Num_Calc ("Integrate.is'_f'_x",
19.46 eval_is_f_x "is_f_x_"),
19.47 @@ -150,7 +150,7 @@
19.48 Rule.Thm ("not_false", TermC.num_str @{thm not_false})
19.49 ],
19.50 scr = Rule.EmptyScr},
19.51 - srls = Rule_Set.Erls, calc = [], errpatts = [],
19.52 + srls = Rule_Set.Empty, calc = [], errpatts = [],
19.53 rules = [ (*Rule.Thm ("call_for_new_c", TermC.num_str @{thm call_for_new_c}),*)
19.54 Rule.Cal1 ("Integrate.add'_new'_c", eval_add_new_c "new_c_")
19.55 ],
19.56 @@ -162,18 +162,18 @@
19.57
19.58 (*.for simplify_Integral adapted from 'norm_Rational_rls'.*)
19.59 val norm_Rational_rls_noadd_fractions =
19.60 -Rule_Set.Rls {id = "norm_Rational_rls_noadd_fractions", preconds = [],
19.61 +Rule_Def.Repeat {id = "norm_Rational_rls_noadd_fractions", preconds = [],
19.62 rew_ord = ("dummy_ord",Rule.dummy_ord),
19.63 - erls = norm_rat_erls, srls = Rule_Set.Erls, calc = [], errpatts = [],
19.64 + erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
19.65 rules = [(*Rule.Rls_ add_fractions_p_rls,!!!*)
19.66 Rule.Rls_ (*rat_mult_div_pow original corrected WN051028*)
19.67 - (Rule_Set.Rls {id = "rat_mult_div_pow", preconds = [],
19.68 + (Rule_Def.Repeat {id = "rat_mult_div_pow", preconds = [],
19.69 rew_ord = ("dummy_ord",Rule.dummy_ord),
19.70 erls = (*FIXME.WN051028 Rule_Set.e_rls,*)
19.71 Rule_Set.append_rls "Rule_Set.e_rls-is_polyexp" Rule_Set.e_rls
19.72 [Rule.Num_Calc ("Poly.is'_polyexp",
19.73 eval_is_polyexp "")],
19.74 - srls = Rule_Set.Erls, calc = [], errpatts = [],
19.75 + srls = Rule_Set.Empty, calc = [], errpatts = [],
19.76 rules = [Rule.Thm ("rat_mult", TermC.num_str @{thm rat_mult}),
19.77 (*"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)
19.78 Rule.Thm ("rat_mult_poly_l", TermC.num_str @{thm rat_mult_poly_l}),
19.79 @@ -206,9 +206,9 @@
19.80
19.81 (*.for simplify_Integral adapted from 'norm_Rational'.*)
19.82 val norm_Rational_noadd_fractions =
19.83 - Rule_Set.Seq {id = "norm_Rational_noadd_fractions", preconds = [],
19.84 + Rule_Set.Seqence {id = "norm_Rational_noadd_fractions", preconds = [],
19.85 rew_ord = ("dummy_ord",Rule.dummy_ord),
19.86 - erls = norm_rat_erls, srls = Rule_Set.Erls, calc = [], errpatts = [],
19.87 + erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
19.88 rules = [Rule.Rls_ discard_minus,
19.89 Rule.Rls_ rat_mult_poly,(* removes double fractions like a/b/c *)
19.90 Rule.Rls_ make_rat_poly_with_parentheses, (*WN0510 also in(#)below*)
19.91 @@ -240,9 +240,9 @@
19.92 (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)----------*)
19.93 ];
19.94 val simplify_Integral =
19.95 - Rule_Set.Seq {id = "simplify_Integral", preconds = []:term list,
19.96 + Rule_Set.Seqence {id = "simplify_Integral", preconds = []:term list,
19.97 rew_ord = ("dummy_ord", Rule.dummy_ord),
19.98 - erls = Atools_erls, srls = Rule_Set.Erls,
19.99 + erls = Atools_erls, srls = Rule_Set.Empty,
19.100 calc = [], errpatts = [],
19.101 rules = [Rule.Thm ("distrib_right", TermC.num_str @{thm distrib_right}),
19.102 (*"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"*)
19.103 @@ -266,9 +266,9 @@
19.104 'make_ratpoly_in'
19.105 THIS IS KEPT FOR COMPARISON ............................................
19.106 * val simplify_Integral = prep_rls'(
19.107 -* Rule_Set.Seq {id = "", preconds = []:term list,
19.108 +* Rule_Set.Seqence {id = "", preconds = []:term list,
19.109 * rew_ord = ("dummy_ord", Rule.dummy_ord),
19.110 -* erls = Atools_erls, srls = Rule_Set.Erls,
19.111 +* erls = Atools_erls, srls = Rule_Set.Empty,
19.112 * calc = [], (*asm_thm = [],*)
19.113 * rules = [Rule.Rls_ expand_poly,
19.114 * Rule.Rls_ order_add_mult_in,
19.115 @@ -299,16 +299,16 @@
19.116 .......................................................................*)
19.117
19.118 val integration =
19.119 - Rule_Set.Seq {id="integration", preconds = [],
19.120 + Rule_Set.Seqence {id="integration", preconds = [],
19.121 rew_ord = ("termlessI",termlessI),
19.122 - erls = Rule_Set.Rls {id="conditions_in_integration",
19.123 + erls = Rule_Def.Repeat {id="conditions_in_integration",
19.124 preconds = [],
19.125 rew_ord = ("termlessI",termlessI),
19.126 - erls = Rule_Set.Erls,
19.127 - srls = Rule_Set.Erls, calc = [], errpatts = [],
19.128 + erls = Rule_Set.Empty,
19.129 + srls = Rule_Set.Empty, calc = [], errpatts = [],
19.130 rules = [],
19.131 scr = Rule.EmptyScr},
19.132 - srls = Rule_Set.Erls, calc = [], errpatts = [],
19.133 + srls = Rule_Set.Empty, calc = [], errpatts = [],
19.134 rules = [ Rule.Rls_ integration_rules,
19.135 Rule.Rls_ add_new_c,
19.136 Rule.Rls_ simplify_Integral
20.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Sat Apr 04 12:11:32 2020 +0200
20.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Mon Apr 06 11:44:36 2020 +0200
20.3 @@ -27,8 +27,8 @@
20.4
20.5 ML \<open>
20.6 val inverse_z = prep_rls'(
20.7 - Rule_Set.Rls {id = "inverse_z", preconds = [], rew_ord = ("dummy_ord",Rule.dummy_ord),
20.8 - erls = Rule_Set.Erls, srls = Rule_Set.Erls, calc = [], errpatts = [],
20.9 + Rule_Def.Repeat {id = "inverse_z", preconds = [], rew_ord = ("dummy_ord",Rule.dummy_ord),
20.10 + erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
20.11 rules =
20.12 [
20.13 Rule.Thm ("rule4", @{thm rule4})
20.14 @@ -120,14 +120,14 @@
20.15 [("#Given" ,["filterExpression X_eq", "functionName X_z"]),
20.16 ("#Find" ,["stepResponse n_eq"])], \<comment> \<open>TODO: unused, "u [n]" is introduced by rule1..6\<close>
20.17 {rew_ord'="tless_true", rls'= Rule_Set.e_rls, calc = [],
20.18 - srls = Rule_Set.Rls {id="srls_partial_fraction",
20.19 + srls = Rule_Def.Repeat {id="srls_partial_fraction",
20.20 preconds = [], rew_ord = ("termlessI",termlessI),
20.21 erls = Rule_Set.append_rls "erls_in_srls_partial_fraction" Rule_Set.e_rls
20.22 [(*for asm in NTH_CONS ...*)
20.23 Rule.Num_Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
20.24 (*2nd NTH_CONS pushes n+-1 into asms*)
20.25 Rule.Num_Calc("Groups.plus_class.plus", (**)eval_binop "#add_")],
20.26 - srls = Rule_Set.Erls, calc = [], errpatts = [],
20.27 + srls = Rule_Set.Empty, calc = [], errpatts = [],
20.28 rules = [Rule.Thm ("NTH_CONS", @{thm NTH_CONS}),
20.29 Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"),
20.30 Rule.Thm ("NTH_NIL", @{thm NTH_NIL}),
21.1 --- a/src/Tools/isac/Knowledge/LinEq.thy Sat Apr 04 12:11:32 2020 +0200
21.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy Mon Apr 06 11:44:36 2020 +0200
21.3 @@ -69,10 +69,10 @@
21.4 ML \<open>
21.5
21.6 val LinPoly_simplify = prep_rls'(
21.7 - Rule_Set.Rls {id = "LinPoly_simplify", preconds = [],
21.8 + Rule_Def.Repeat {id = "LinPoly_simplify", preconds = [],
21.9 rew_ord = ("termlessI",termlessI),
21.10 erls = LinEq_erls,
21.11 - srls = Rule_Set.Erls,
21.12 + srls = Rule_Set.Empty,
21.13 calc = [], errpatts = [],
21.14 rules = [
21.15 Rule.Thm ("real_assoc_1",TermC.num_str @{thm real_assoc_1}),
21.16 @@ -93,10 +93,10 @@
21.17
21.18 (*isolate the bound variable in an linear equation; 'bdv' is a meta-constant*)
21.19 val LinEq_simplify = prep_rls'(
21.20 -Rule_Set.Rls {id = "LinEq_simplify", preconds = [],
21.21 +Rule_Def.Repeat {id = "LinEq_simplify", preconds = [],
21.22 rew_ord = ("e_rew_ord", Rule.e_rew_ord),
21.23 erls = LinEq_erls,
21.24 - srls = Rule_Set.Erls,
21.25 + srls = Rule_Set.Empty,
21.26 calc = [], errpatts = [],
21.27 rules = [
21.28 Rule.Thm("lin_isolate_add1",TermC.num_str @{thm lin_isolate_add1}),
22.1 --- a/src/Tools/isac/Knowledge/Partial_Fractions.thy Sat Apr 04 12:11:32 2020 +0200
22.2 +++ b/src/Tools/isac/Knowledge/Partial_Fractions.thy Mon Apr 06 11:44:36 2020 +0200
22.3 @@ -106,8 +106,8 @@
22.4
22.5 ML \<open>
22.6 val ansatz_rls = prep_rls'(
22.7 - Rule_Set.Rls {id = "ansatz_rls", preconds = [], rew_ord = ("dummy_ord",Rule.dummy_ord),
22.8 - erls = Rule_Set.Erls, srls = Rule_Set.Erls, calc = [], errpatts = [],
22.9 + Rule_Def.Repeat {id = "ansatz_rls", preconds = [], rew_ord = ("dummy_ord",Rule.dummy_ord),
22.10 + erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
22.11 rules =
22.12 [Rule.Thm ("ansatz_2nd_order",TermC.num_str @{thm ansatz_2nd_order}),
22.13 Rule.Thm ("ansatz_3rd_order",TermC.num_str @{thm ansatz_3rd_order})
22.14 @@ -115,8 +115,8 @@
22.15 scr = Rule.EmptyScr});
22.16
22.17 val equival_trans = prep_rls'(
22.18 - Rule_Set.Rls {id = "equival_trans", preconds = [], rew_ord = ("dummy_ord",Rule.dummy_ord),
22.19 - erls = Rule_Set.Erls, srls = Rule_Set.Erls, calc = [], errpatts = [],
22.20 + Rule_Def.Repeat {id = "equival_trans", preconds = [], rew_ord = ("dummy_ord",Rule.dummy_ord),
22.21 + erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
22.22 rules =
22.23 [Rule.Thm ("equival_trans_2nd_order",TermC.num_str @{thm equival_trans_2nd_order}),
22.24 Rule.Thm ("equival_trans_3rd_order",TermC.num_str @{thm equival_trans_3rd_order})
22.25 @@ -124,9 +124,9 @@
22.26 scr = Rule.EmptyScr});
22.27
22.28 val multiply_ansatz = prep_rls'(
22.29 - Rule_Set.Rls {id = "multiply_ansatz", preconds = [], rew_ord = ("dummy_ord",Rule.dummy_ord),
22.30 - erls = Rule_Set.Erls,
22.31 - srls = Rule_Set.Erls, calc = [], errpatts = [],
22.32 + Rule_Def.Repeat {id = "multiply_ansatz", preconds = [], rew_ord = ("dummy_ord",Rule.dummy_ord),
22.33 + erls = Rule_Set.Empty,
22.34 + srls = Rule_Set.Empty, calc = [], errpatts = [],
22.35 rules =
22.36 [Rule.Thm ("multiply_2nd_order",TermC.num_str @{thm multiply_2nd_order})
22.37 ],
22.38 @@ -163,7 +163,7 @@
22.39 subsection \<open>Method\<close>
22.40 text \<open>rule set for functions called in the Program\<close>
22.41 ML \<open>
22.42 - val srls_partial_fraction = Rule_Set.Rls {id="srls_partial_fraction",
22.43 + val srls_partial_fraction = Rule_Def.Repeat {id="srls_partial_fraction",
22.44 preconds = [],
22.45 rew_ord = ("termlessI",termlessI),
22.46 erls = Rule_Set.append_rls "erls_in_srls_partial_fraction" Rule_Set.e_rls
22.47 @@ -171,7 +171,7 @@
22.48 Rule.Num_Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
22.49 (*2nd NTH_CONS pushes n+-1 into asms*)
22.50 Rule.Num_Calc("Groups.plus_class.plus", (**)eval_binop "#add_")],
22.51 - srls = Rule_Set.Erls, calc = [], errpatts = [],
22.52 + srls = Rule_Set.Empty, calc = [], errpatts = [],
22.53 rules = [
22.54 Rule.Thm ("NTH_CONS",TermC.num_str @{thm NTH_CONS}),
22.55 Rule.Num_Calc("Groups.plus_class.plus", (**)eval_binop "#add_"),
23.1 --- a/src/Tools/isac/Knowledge/Poly.thy Sat Apr 04 12:11:32 2020 +0200
23.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Mon Apr 06 11:44:36 2020 +0200
23.3 @@ -669,8 +669,8 @@
23.4 \<close>
23.5 ML \<open>
23.6 val expand =
23.7 - Rule_Set.Rls {id = "expand", preconds = [], rew_ord = ("dummy_ord", Rule.dummy_ord),
23.8 - erls = Rule_Set.e_rls,srls = Rule_Set.Erls, calc = [], errpatts = [],
23.9 + Rule_Def.Repeat {id = "expand", preconds = [], rew_ord = ("dummy_ord", Rule.dummy_ord),
23.10 + erls = Rule_Set.e_rls,srls = Rule_Set.Empty, calc = [], errpatts = [],
23.11 rules = [Rule.Thm ("distrib_right" , TermC.num_str @{thm distrib_right}),
23.12 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
23.13 Rule.Thm ("distrib_left", TermC.num_str @{thm distrib_left})
23.14 @@ -678,8 +678,8 @@
23.15 ], scr = Rule.EmptyScr};
23.16
23.17 val discard_minus =
23.18 - Rule_Set.Rls {id = "discard_minus", preconds = [], rew_ord = ("dummy_ord", Rule.dummy_ord),
23.19 - erls = Rule_Set.e_rls, srls = Rule_Set.Erls, calc = [], errpatts = [],
23.20 + Rule_Def.Repeat {id = "discard_minus", preconds = [], rew_ord = ("dummy_ord", Rule.dummy_ord),
23.21 + erls = Rule_Set.e_rls, srls = Rule_Set.Empty, calc = [], errpatts = [],
23.22 rules =
23.23 [Rule.Thm ("real_diff_minus", TermC.num_str @{thm real_diff_minus}),
23.24 (*"a - b = a + -1 * b"*)
23.25 @@ -688,9 +688,9 @@
23.26 scr = Rule.EmptyScr};
23.27
23.28 val expand_poly_ =
23.29 - Rule_Set.Rls{id = "expand_poly_", preconds = [],
23.30 + Rule_Def.Repeat{id = "expand_poly_", preconds = [],
23.31 rew_ord = ("dummy_ord", Rule.dummy_ord),
23.32 - erls = Rule_Set.e_rls,srls = Rule_Set.Erls,
23.33 + erls = Rule_Set.e_rls,srls = Rule_Set.Empty,
23.34 calc = [], errpatts = [],
23.35 rules =
23.36 [Rule.Thm ("real_plus_binom_pow4", TermC.num_str @{thm real_plus_binom_pow4}),
23.37 @@ -722,12 +722,12 @@
23.38 ], scr = Rule.EmptyScr};
23.39
23.40 val expand_poly_rat_ =
23.41 - Rule_Set.Rls{id = "expand_poly_rat_", preconds = [],
23.42 + Rule_Def.Repeat{id = "expand_poly_rat_", preconds = [],
23.43 rew_ord = ("dummy_ord", Rule.dummy_ord),
23.44 erls = Rule_Set.append_rls "Rule_Set.e_rls-is_polyexp" Rule_Set.e_rls
23.45 [Rule.Num_Calc ("Poly.is'_polyexp", eval_is_polyexp "")
23.46 ],
23.47 - srls = Rule_Set.Erls,
23.48 + srls = Rule_Set.Empty,
23.49 calc = [], errpatts = [],
23.50 rules =
23.51 [Rule.Thm ("real_plus_binom_pow4_poly", TermC.num_str @{thm real_plus_binom_pow4_poly}),
23.52 @@ -760,9 +760,9 @@
23.53 ], scr = Rule.EmptyScr};
23.54
23.55 val simplify_power_ =
23.56 - Rule_Set.Rls{id = "simplify_power_", preconds = [],
23.57 + Rule_Def.Repeat{id = "simplify_power_", preconds = [],
23.58 rew_ord = ("dummy_ord", Rule.dummy_ord),
23.59 - erls = Rule_Set.e_rls, srls = Rule_Set.Erls,
23.60 + erls = Rule_Set.e_rls, srls = Rule_Set.Empty,
23.61 calc = [], errpatts = [],
23.62 rules = [(*MG: Reihenfolge der folgenden 2 Rule.Thm muss so bleiben, wegen
23.63 a*(a*a) --> a*a^^^2 und nicht a*(a*a) --> a^^^2*a *)
23.64 @@ -795,9 +795,9 @@
23.65 ], scr = Rule.EmptyScr};
23.66
23.67 val calc_add_mult_pow_ =
23.68 - Rule_Set.Rls{id = "calc_add_mult_pow_", preconds = [],
23.69 + Rule_Def.Repeat{id = "calc_add_mult_pow_", preconds = [],
23.70 rew_ord = ("dummy_ord", Rule.dummy_ord),
23.71 - erls = Atools_erls(*erls3.4.03*),srls = Rule_Set.Erls,
23.72 + erls = Atools_erls(*erls3.4.03*),srls = Rule_Set.Empty,
23.73 calc = [("PLUS" , ("Groups.plus_class.plus", (**)eval_binop "#add_")),
23.74 ("TIMES" , ("Groups.times_class.times", (**)eval_binop "#mult_")),
23.75 ("POWER", ("Prog_Expr.pow", (**)eval_binop "#power_"))
23.76 @@ -809,9 +809,9 @@
23.77 ], scr = Rule.EmptyScr};
23.78
23.79 val reduce_012_mult_ =
23.80 - Rule_Set.Rls{id = "reduce_012_mult_", preconds = [],
23.81 + Rule_Def.Repeat{id = "reduce_012_mult_", preconds = [],
23.82 rew_ord = ("dummy_ord", Rule.dummy_ord),
23.83 - erls = Rule_Set.e_rls,srls = Rule_Set.Erls,
23.84 + erls = Rule_Set.e_rls,srls = Rule_Set.Empty,
23.85 calc = [], errpatts = [],
23.86 rules = [(* MG: folgende Rule.Thm müssen hier stehen bleiben: *)
23.87 Rule.Thm ("mult_1_right",TermC.num_str @{thm mult_1_right}),
23.88 @@ -825,9 +825,9 @@
23.89 ], scr = Rule.EmptyScr};
23.90
23.91 val collect_numerals_ =
23.92 - Rule_Set.Rls{id = "collect_numerals_", preconds = [],
23.93 + Rule_Def.Repeat{id = "collect_numerals_", preconds = [],
23.94 rew_ord = ("dummy_ord", Rule.dummy_ord),
23.95 - erls = Atools_erls, srls = Rule_Set.Erls,
23.96 + erls = Atools_erls, srls = Rule_Set.Empty,
23.97 calc = [("PLUS" , ("Groups.plus_class.plus", (**)eval_binop "#add_"))
23.98 ], errpatts = [],
23.99 rules =
23.100 @@ -852,9 +852,9 @@
23.101 ], scr = Rule.EmptyScr};
23.102
23.103 val reduce_012_ =
23.104 - Rule_Set.Rls{id = "reduce_012_", preconds = [],
23.105 + Rule_Def.Repeat{id = "reduce_012_", preconds = [],
23.106 rew_ord = ("dummy_ord", Rule.dummy_ord),
23.107 - erls = Rule_Set.e_rls,srls = Rule_Set.Erls, calc = [], errpatts = [],
23.108 + erls = Rule_Set.e_rls,srls = Rule_Set.Empty, calc = [], errpatts = [],
23.109 rules = [Rule.Thm ("mult_1_left",TermC.num_str @{thm mult_1_left}),
23.110 (*"1 * z = z"*)
23.111 Rule.Thm ("mult_zero_left",TermC.num_str @{thm mult_zero_left}),
23.112 @@ -883,9 +883,9 @@
23.113 ];
23.114
23.115 val expand_poly =
23.116 - Rule_Set.Rls{id = "expand_poly", preconds = [],
23.117 + Rule_Def.Repeat{id = "expand_poly", preconds = [],
23.118 rew_ord = ("dummy_ord", Rule.dummy_ord),
23.119 - erls = Rule_Set.e_rls,srls = Rule_Set.Erls,
23.120 + erls = Rule_Set.e_rls,srls = Rule_Set.Empty,
23.121 calc = [], errpatts = [],
23.122 (*asm_thm = [],*)
23.123 rules = [Rule.Thm ("distrib_right" ,TermC.num_str @{thm distrib_right}),
23.124 @@ -922,9 +922,9 @@
23.125 ], scr = Rule.EmptyScr};
23.126
23.127 val simplify_power =
23.128 - Rule_Set.Rls{id = "simplify_power", preconds = [],
23.129 + Rule_Def.Repeat{id = "simplify_power", preconds = [],
23.130 rew_ord = ("dummy_ord", Rule.dummy_ord),
23.131 - erls = Rule_Set.e_rls, srls = Rule_Set.Erls,
23.132 + erls = Rule_Set.e_rls, srls = Rule_Set.Empty,
23.133 calc = [], errpatts = [],
23.134 rules = [Rule.Thm ("realpow_multI", TermC.num_str @{thm realpow_multI}),
23.135 (*"(r * s) ^^^ n = r ^^^ n * s ^^^ n"*)
23.136 @@ -946,9 +946,9 @@
23.137 ], scr = Rule.EmptyScr};
23.138
23.139 val collect_numerals =
23.140 - Rule_Set.Rls{id = "collect_numerals", preconds = [],
23.141 + Rule_Def.Repeat{id = "collect_numerals", preconds = [],
23.142 rew_ord = ("dummy_ord", Rule.dummy_ord),
23.143 - erls = Atools_erls(*erls3.4.03*),srls = Rule_Set.Erls,
23.144 + erls = Atools_erls(*erls3.4.03*),srls = Rule_Set.Empty,
23.145 calc = [("PLUS" , ("Groups.plus_class.plus", (**)eval_binop "#add_")),
23.146 ("TIMES" , ("Groups.times_class.times", (**)eval_binop "#mult_")),
23.147 ("POWER", ("Prog_Expr.pow", (**)eval_binop "#power_"))
23.148 @@ -967,9 +967,9 @@
23.149 Rule.Num_Calc ("Prog_Expr.pow", (**)eval_binop "#power_")
23.150 ], scr = Rule.EmptyScr};
23.151 val reduce_012 =
23.152 - Rule_Set.Rls{id = "reduce_012", preconds = [],
23.153 + Rule_Def.Repeat{id = "reduce_012", preconds = [],
23.154 rew_ord = ("dummy_ord", Rule.dummy_ord),
23.155 - erls = Rule_Set.e_rls,srls = Rule_Set.Erls,
23.156 + erls = Rule_Set.e_rls,srls = Rule_Set.Empty,
23.157 calc = [], errpatts = [],
23.158 rules = [Rule.Thm ("mult_1_left",TermC.num_str @{thm mult_1_left}),
23.159 (*"1 * z = z"*)
23.160 @@ -1007,9 +1007,9 @@
23.161 (*MG.0401: termorders for multivariate polys dropped due to principal problems:
23.162 (total-degree-)ordering of monoms NOT possible with size_of_term GIVEN*)
23.163 val order_add_mult =
23.164 - Rule_Set.Rls{id = "order_add_mult", preconds = [],
23.165 + Rule_Def.Repeat{id = "order_add_mult", preconds = [],
23.166 rew_ord = ("ord_make_polynomial",ord_make_polynomial false thy),
23.167 - erls = Rule_Set.e_rls,srls = Rule_Set.Erls,
23.168 + erls = Rule_Set.e_rls,srls = Rule_Set.Empty,
23.169 calc = [], errpatts = [],
23.170 rules = [Rule.Thm ("mult_commute",TermC.num_str @{thm mult.commute}),
23.171 (* z * w = w * z *)
23.172 @@ -1027,9 +1027,9 @@
23.173 (*MG.0401: termorders for multivariate polys dropped due to principal problems:
23.174 (total-degree-)ordering of monoms NOT possible with size_of_term GIVEN*)
23.175 val order_mult =
23.176 - Rule_Set.Rls{id = "order_mult", preconds = [],
23.177 + Rule_Def.Repeat{id = "order_mult", preconds = [],
23.178 rew_ord = ("ord_make_polynomial",ord_make_polynomial false thy),
23.179 - erls = Rule_Set.e_rls,srls = Rule_Set.Erls,
23.180 + erls = Rule_Set.e_rls,srls = Rule_Set.Empty,
23.181 calc = [], errpatts = [],
23.182 rules = [Rule.Thm ("mult_commute",TermC.num_str @{thm mult.commute}),
23.183 (* z * w = w * z *)
23.184 @@ -1070,9 +1070,9 @@
23.185 next_rule = next_rule,
23.186 attach_form = attach_form}};
23.187 val order_mult_rls_ =
23.188 - Rule_Set.Rls {id = "order_mult_rls_", preconds = [],
23.189 + Rule_Def.Repeat {id = "order_mult_rls_", preconds = [],
23.190 rew_ord = ("dummy_ord", Rule.dummy_ord),
23.191 - erls = Rule_Set.e_rls,srls = Rule_Set.Erls,
23.192 + erls = Rule_Set.e_rls,srls = Rule_Set.Empty,
23.193 calc = [], errpatts = [],
23.194 rules = [Rule.Rls_ order_mult_
23.195 ], scr = Rule.EmptyScr};
23.196 @@ -1110,9 +1110,9 @@
23.197 attach_form = attach_form}};
23.198
23.199 val order_add_rls_ =
23.200 - Rule_Set.Rls {id = "order_add_rls_", preconds = [],
23.201 + Rule_Def.Repeat {id = "order_add_rls_", preconds = [],
23.202 rew_ord = ("dummy_ord", Rule.dummy_ord),
23.203 - erls = Rule_Set.e_rls,srls = Rule_Set.Erls,
23.204 + erls = Rule_Set.e_rls,srls = Rule_Set.Empty,
23.205 calc = [], errpatts = [],
23.206 rules = [Rule.Rls_ order_add_
23.207 ], scr = Rule.EmptyScr};
23.208 @@ -1130,9 +1130,9 @@
23.209 (*. see MG-DA.p.52ff .*)
23.210 val make_polynomial(*MG.03, overwrites version from above,
23.211 previously 'make_polynomial_'*) =
23.212 - Rule_Set.Seq {id = "make_polynomial", preconds = []:term list,
23.213 + Rule_Set.Seqence {id = "make_polynomial", preconds = []:term list,
23.214 rew_ord = ("dummy_ord", Rule.dummy_ord),
23.215 - erls = Atools_erls, srls = Rule_Set.Erls,calc = [], errpatts = [],
23.216 + erls = Atools_erls, srls = Rule_Set.Empty,calc = [], errpatts = [],
23.217 rules = [Rule.Rls_ discard_minus,
23.218 Rule.Rls_ expand_poly_,
23.219 Rule.Num_Calc ("Groups.times_class.times", (**)eval_binop "#mult_"),
23.220 @@ -1150,9 +1150,9 @@
23.221 \<close>
23.222 ML \<open>
23.223 val norm_Poly(*=make_polynomial*) =
23.224 - Rule_Set.Seq {id = "norm_Poly", preconds = []:term list,
23.225 + Rule_Set.Seqence {id = "norm_Poly", preconds = []:term list,
23.226 rew_ord = ("dummy_ord", Rule.dummy_ord),
23.227 - erls = Atools_erls, srls = Rule_Set.Erls, calc = [], errpatts = [],
23.228 + erls = Atools_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
23.229 rules = [Rule.Rls_ discard_minus,
23.230 Rule.Rls_ expand_poly_,
23.231 Rule.Num_Calc ("Groups.times_class.times", (**)eval_binop "#mult_"),
23.232 @@ -1173,9 +1173,9 @@
23.233 and expand_poly_rat_ instead of expand_poly_, see MG-DA.p.56ff*)
23.234 (* MG necessary for termination of norm_Rational(*_mg*) in Rational.ML*)
23.235 val make_rat_poly_with_parentheses =
23.236 - Rule_Set.Seq{id = "make_rat_poly_with_parentheses", preconds = []:term list,
23.237 + Rule_Set.Seqence{id = "make_rat_poly_with_parentheses", preconds = []:term list,
23.238 rew_ord = ("dummy_ord", Rule.dummy_ord),
23.239 - erls = Atools_erls, srls = Rule_Set.Erls, calc = [], errpatts = [],
23.240 + erls = Atools_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
23.241 rules = [Rule.Rls_ discard_minus,
23.242 Rule.Rls_ expand_poly_rat_,(*ignors rationals*)
23.243 Rule.Num_Calc ("Groups.times_class.times", (**)eval_binop "#mult_"),
23.244 @@ -1195,8 +1195,8 @@
23.245 (*.a minimal ruleset for reverse rewriting of factions [2];
23.246 compare expand_binoms.*)
23.247 val rev_rew_p =
23.248 -Rule_Set.Seq{id = "rev_rew_p", preconds = [], rew_ord = ("termlessI",termlessI),
23.249 - erls = Atools_erls, srls = Rule_Set.Erls,
23.250 +Rule_Set.Seqence{id = "rev_rew_p", preconds = [], rew_ord = ("termlessI",termlessI),
23.251 + erls = Atools_erls, srls = Rule_Set.Empty,
23.252 calc = [(*("PLUS" , ("Groups.plus_class.plus", (**)eval_binop "#add_")),
23.253 ("TIMES" , ("Groups.times_class.times", (**)eval_binop "#mult_")),
23.254 ("POWER", ("Prog_Expr.pow", (**)eval_binop "#power_"))*)
23.255 @@ -1297,8 +1297,8 @@
23.256 term)"
23.257 ML \<open>
23.258 val expand_binoms =
23.259 - Rule_Set.Rls{id = "expand_binoms", preconds = [], rew_ord = ("termlessI",termlessI),
23.260 - erls = Atools_erls, srls = Rule_Set.Erls,
23.261 + Rule_Def.Repeat{id = "expand_binoms", preconds = [], rew_ord = ("termlessI",termlessI),
23.262 + erls = Atools_erls, srls = Rule_Set.Empty,
23.263 calc = [("PLUS" , ("Groups.plus_class.plus", (**)eval_binop "#add_")),
23.264 ("TIMES" , ("Groups.times_class.times", (**)eval_binop "#mult_")),
23.265 ("POWER", ("Prog_Expr.pow", (**)eval_binop "#power_"))
24.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Sat Apr 04 12:11:32 2020 +0200
24.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Mon Apr 06 11:44:36 2020 +0200
24.3 @@ -368,9 +368,9 @@
24.4 ]);
24.5
24.6 val cancel_leading_coeff = prep_rls'(
24.7 - Rule_Set.Rls {id = "cancel_leading_coeff", preconds = [],
24.8 + Rule_Def.Repeat {id = "cancel_leading_coeff", preconds = [],
24.9 rew_ord = ("e_rew_ord",Rule.e_rew_ord),
24.10 - erls = PolyEq_erls, srls = Rule_Set.Erls, calc = [], errpatts = [],
24.11 + erls = PolyEq_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
24.12 rules =
24.13 [Rule.Thm ("cancel_leading_coeff1",TermC.num_str @{thm cancel_leading_coeff1}),
24.14 Rule.Thm ("cancel_leading_coeff2",TermC.num_str @{thm cancel_leading_coeff2}),
24.15 @@ -391,9 +391,9 @@
24.16 \<close>
24.17 ML\<open>
24.18 val complete_square = prep_rls'(
24.19 - Rule_Set.Rls {id = "complete_square", preconds = [],
24.20 + Rule_Def.Repeat {id = "complete_square", preconds = [],
24.21 rew_ord = ("e_rew_ord",Rule.e_rew_ord),
24.22 - erls = PolyEq_erls, srls = Rule_Set.Erls, calc = [], errpatts = [],
24.23 + erls = PolyEq_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
24.24 rules = [Rule.Thm ("complete_square1",TermC.num_str @{thm complete_square1}),
24.25 Rule.Thm ("complete_square2",TermC.num_str @{thm complete_square2}),
24.26 Rule.Thm ("complete_square3",TermC.num_str @{thm complete_square3}),
24.27 @@ -404,10 +404,10 @@
24.28 });
24.29
24.30 val polyeq_simplify = prep_rls'(
24.31 - Rule_Set.Rls {id = "polyeq_simplify", preconds = [],
24.32 + Rule_Def.Repeat {id = "polyeq_simplify", preconds = [],
24.33 rew_ord = ("termlessI",termlessI),
24.34 erls = PolyEq_erls,
24.35 - srls = Rule_Set.Erls,
24.36 + srls = Rule_Set.Empty,
24.37 calc = [], errpatts = [],
24.38 rules = [Rule.Thm ("real_assoc_1",TermC.num_str @{thm real_assoc_1}),
24.39 Rule.Thm ("real_assoc_2",TermC.num_str @{thm real_assoc_2}),
24.40 @@ -436,10 +436,10 @@
24.41 (* -- d0 -- *)
24.42 (*isolate the bound variable in an d0 equation; 'bdv' is a meta-constant*)
24.43 val d0_polyeq_simplify = prep_rls'(
24.44 - Rule_Set.Rls {id = "d0_polyeq_simplify", preconds = [],
24.45 + Rule_Def.Repeat {id = "d0_polyeq_simplify", preconds = [],
24.46 rew_ord = ("e_rew_ord",Rule.e_rew_ord),
24.47 erls = PolyEq_erls,
24.48 - srls = Rule_Set.Erls,
24.49 + srls = Rule_Set.Empty,
24.50 calc = [], errpatts = [],
24.51 rules = [Rule.Thm("d0_true",TermC.num_str @{thm d0_true}),
24.52 Rule.Thm("d0_false",TermC.num_str @{thm d0_false})
24.53 @@ -450,10 +450,10 @@
24.54 (* -- d1 -- *)
24.55 (*isolate the bound variable in an d1 equation; 'bdv' is a meta-constant*)
24.56 val d1_polyeq_simplify = prep_rls'(
24.57 - Rule_Set.Rls {id = "d1_polyeq_simplify", preconds = [],
24.58 + Rule_Def.Repeat {id = "d1_polyeq_simplify", preconds = [],
24.59 rew_ord = ("e_rew_ord",Rule.e_rew_ord),
24.60 erls = PolyEq_erls,
24.61 - srls = Rule_Set.Erls,
24.62 + srls = Rule_Set.Empty,
24.63 calc = [], errpatts = [],
24.64 rules = [
24.65 Rule.Thm("d1_isolate_add1",TermC.num_str @{thm d1_isolate_add1}),
24.66 @@ -472,8 +472,8 @@
24.67 (* isolate the bound variable in an d2 equation with bdv only;
24.68 "bdv" is a meta-constant substituted for the "x" below by isac's rewriter. *)
24.69 val d2_polyeq_bdv_only_simplify = prep_rls'(
24.70 - Rule_Set.Rls {id = "d2_polyeq_bdv_only_simplify", preconds = [], rew_ord = ("e_rew_ord",Rule.e_rew_ord),
24.71 - erls = PolyEq_erls, srls = Rule_Set.Erls, calc = [], errpatts = [],
24.72 + Rule_Def.Repeat {id = "d2_polyeq_bdv_only_simplify", preconds = [], rew_ord = ("e_rew_ord",Rule.e_rew_ord),
24.73 + erls = PolyEq_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
24.74 rules =
24.75 [Rule.Thm ("d2_prescind1", TermC.num_str @{thm d2_prescind1}), (* ax+bx^2=0 -> x(a+bx)=0 *)
24.76 Rule.Thm ("d2_prescind2", TermC.num_str @{thm d2_prescind2}), (* ax+ x^2=0 -> x(a+ x)=0 *)
24.77 @@ -493,10 +493,10 @@
24.78 (* isolate the bound variable in an d2 equation with sqrt only;
24.79 'bdv' is a meta-constant*)
24.80 val d2_polyeq_sq_only_simplify = prep_rls'(
24.81 - Rule_Set.Rls {id = "d2_polyeq_sq_only_simplify", preconds = [],
24.82 + Rule_Def.Repeat {id = "d2_polyeq_sq_only_simplify", preconds = [],
24.83 rew_ord = ("e_rew_ord",Rule.e_rew_ord),
24.84 erls = PolyEq_erls,
24.85 - srls = Rule_Set.Erls,
24.86 + srls = Rule_Set.Empty,
24.87 calc = [], errpatts = [],
24.88 (*asm_thm = [("d2_sqrt_equation1",""),("d2_sqrt_equation1_neg",""),
24.89 ("d2_isolate_div","")],*)
24.90 @@ -520,9 +520,9 @@
24.91 (* isolate the bound variable in an d2 equation with pqFormula;
24.92 'bdv' is a meta-constant*)
24.93 val d2_polyeq_pqFormula_simplify = prep_rls'(
24.94 - Rule_Set.Rls {id = "d2_polyeq_pqFormula_simplify", preconds = [],
24.95 + Rule_Def.Repeat {id = "d2_polyeq_pqFormula_simplify", preconds = [],
24.96 rew_ord = ("e_rew_ord",Rule.e_rew_ord), erls = PolyEq_erls,
24.97 - srls = Rule_Set.Erls, calc = [], errpatts = [],
24.98 + srls = Rule_Set.Empty, calc = [], errpatts = [],
24.99 rules = [Rule.Thm("d2_pqformula1",TermC.num_str @{thm d2_pqformula1}),
24.100 (* q+px+ x^2=0 *)
24.101 Rule.Thm("d2_pqformula1_neg",TermC.num_str @{thm d2_pqformula1_neg}),
24.102 @@ -566,9 +566,9 @@
24.103 (* isolate the bound variable in an d2 equation with abcFormula;
24.104 'bdv' is a meta-constant*)
24.105 val d2_polyeq_abcFormula_simplify = prep_rls'(
24.106 - Rule_Set.Rls {id = "d2_polyeq_abcFormula_simplify", preconds = [],
24.107 + Rule_Def.Repeat {id = "d2_polyeq_abcFormula_simplify", preconds = [],
24.108 rew_ord = ("e_rew_ord",Rule.e_rew_ord), erls = PolyEq_erls,
24.109 - srls = Rule_Set.Erls, calc = [], errpatts = [],
24.110 + srls = Rule_Set.Empty, calc = [], errpatts = [],
24.111 rules = [Rule.Thm("d2_abcformula1",TermC.num_str @{thm d2_abcformula1}),
24.112 (*c+bx+cx^2=0 *)
24.113 Rule.Thm("d2_abcformula1_neg",TermC.num_str @{thm d2_abcformula1_neg}),
24.114 @@ -614,9 +614,9 @@
24.115 (* isolate the bound variable in an d2 equation;
24.116 'bdv' is a meta-constant*)
24.117 val d2_polyeq_simplify = prep_rls'(
24.118 - Rule_Set.Rls {id = "d2_polyeq_simplify", preconds = [],
24.119 + Rule_Def.Repeat {id = "d2_polyeq_simplify", preconds = [],
24.120 rew_ord = ("e_rew_ord",Rule.e_rew_ord), erls = PolyEq_erls,
24.121 - srls = Rule_Set.Erls, calc = [], errpatts = [],
24.122 + srls = Rule_Set.Empty, calc = [], errpatts = [],
24.123 rules = [Rule.Thm("d2_pqformula1",TermC.num_str @{thm d2_pqformula1}),
24.124 (* p+qx+ x^2=0 *)
24.125 Rule.Thm("d2_pqformula1_neg",TermC.num_str @{thm d2_pqformula1_neg}),
24.126 @@ -674,9 +674,9 @@
24.127 (* -- d3 -- *)
24.128 (* isolate the bound variable in an d3 equation; 'bdv' is a meta-constant *)
24.129 val d3_polyeq_simplify = prep_rls'(
24.130 - Rule_Set.Rls {id = "d3_polyeq_simplify", preconds = [],
24.131 + Rule_Def.Repeat {id = "d3_polyeq_simplify", preconds = [],
24.132 rew_ord = ("e_rew_ord",Rule.e_rew_ord), erls = PolyEq_erls,
24.133 - srls = Rule_Set.Erls, calc = [], errpatts = [],
24.134 + srls = Rule_Set.Empty, calc = [], errpatts = [],
24.135 rules =
24.136 [Rule.Thm("d3_reduce_equation1",TermC.num_str @{thm d3_reduce_equation1}),
24.137 (*a*bdv + b*bdv^^^2 + c*bdv^^^3=0) =
24.138 @@ -747,9 +747,9 @@
24.139 (* -- d4 -- *)
24.140 (*isolate the bound variable in an d4 equation; 'bdv' is a meta-constant*)
24.141 val d4_polyeq_simplify = prep_rls'(
24.142 - Rule_Set.Rls {id = "d4_polyeq_simplify", preconds = [],
24.143 + Rule_Def.Repeat {id = "d4_polyeq_simplify", preconds = [],
24.144 rew_ord = ("e_rew_ord",Rule.e_rew_ord), erls = PolyEq_erls,
24.145 - srls = Rule_Set.Erls, calc = [], errpatts = [],
24.146 + srls = Rule_Set.Empty, calc = [], errpatts = [],
24.147 rules =
24.148 [Rule.Thm("d4_sub_u1",TermC.num_str @{thm d4_sub_u1})
24.149 (* ax^4+bx^2+c=0 -> x=+-sqrt(ax^2+bx^+c) *)
24.150 @@ -1232,10 +1232,10 @@
24.151 \<close>
24.152 ML\<open>
24.153 val order_add_mult_in = prep_rls'(
24.154 - Rule_Set.Rls{id = "order_add_mult_in", preconds = [],
24.155 + Rule_Def.Repeat{id = "order_add_mult_in", preconds = [],
24.156 rew_ord = ("ord_make_polynomial_in",
24.157 ord_make_polynomial_in false @{theory "Poly"}),
24.158 - erls = Rule_Set.e_rls,srls = Rule_Set.Erls,
24.159 + erls = Rule_Set.e_rls,srls = Rule_Set.Empty,
24.160 calc = [], errpatts = [],
24.161 rules = [Rule.Thm ("mult_commute",TermC.num_str @{thm mult.commute}),
24.162 (* z * w = w * z *)
24.163 @@ -1254,9 +1254,9 @@
24.164 \<close>
24.165 ML\<open>
24.166 val collect_bdv = prep_rls'(
24.167 - Rule_Set.Rls{id = "collect_bdv", preconds = [],
24.168 + Rule_Def.Repeat{id = "collect_bdv", preconds = [],
24.169 rew_ord = ("dummy_ord", Rule.dummy_ord),
24.170 - erls = Rule_Set.e_rls,srls = Rule_Set.Erls,
24.171 + erls = Rule_Set.e_rls,srls = Rule_Set.Empty,
24.172 calc = [], errpatts = [],
24.173 rules = [Rule.Thm ("bdv_collect_1",TermC.num_str @{thm bdv_collect_1}),
24.174 Rule.Thm ("bdv_collect_2",TermC.num_str @{thm bdv_collect_2}),
24.175 @@ -1289,9 +1289,9 @@
24.176 (*.transforms an arbitrary term without roots to a polynomial [4]
24.177 according to knowledge/Poly.sml.*)
24.178 val make_polynomial_in = prep_rls'(
24.179 - Rule_Set.Seq {id = "make_polynomial_in", preconds = []:term list,
24.180 + Rule_Set.Seqence {id = "make_polynomial_in", preconds = []:term list,
24.181 rew_ord = ("dummy_ord", Rule.dummy_ord),
24.182 - erls = Atools_erls, srls = Rule_Set.Erls,
24.183 + erls = Atools_erls, srls = Rule_Set.Empty,
24.184 calc = [], errpatts = [],
24.185 rules = [Rule.Rls_ expand_poly,
24.186 Rule.Rls_ order_add_mult_in,
24.187 @@ -1325,9 +1325,9 @@
24.188 \<close>
24.189 ML\<open>
24.190 val make_ratpoly_in = prep_rls'(
24.191 - Rule_Set.Seq {id = "make_ratpoly_in", preconds = []:term list,
24.192 + Rule_Set.Seqence {id = "make_ratpoly_in", preconds = []:term list,
24.193 rew_ord = ("dummy_ord", Rule.dummy_ord),
24.194 - erls = Atools_erls, srls = Rule_Set.Erls,
24.195 + erls = Atools_erls, srls = Rule_Set.Empty,
24.196 calc = [], errpatts = [],
24.197 rules = [Rule.Rls_ norm_Rational,
24.198 Rule.Rls_ order_add_mult_in,
25.1 --- a/src/Tools/isac/Knowledge/PolyMinus.thy Sat Apr 04 12:11:32 2020 +0200
25.2 +++ b/src/Tools/isac/Knowledge/PolyMinus.thy Mon Apr 06 11:44:36 2020 +0200
25.3 @@ -191,8 +191,8 @@
25.4 ];
25.5
25.6 val ordne_alphabetisch =
25.7 - Rule_Set.Rls{id = "ordne_alphabetisch", preconds = [],
25.8 - rew_ord = ("dummy_ord", Rule.dummy_ord), srls = Rule_Set.Erls, calc = [], errpatts = [],
25.9 + Rule_Def.Repeat{id = "ordne_alphabetisch", preconds = [],
25.10 + rew_ord = ("dummy_ord", Rule.dummy_ord), srls = Rule_Set.Empty, calc = [], errpatts = [],
25.11 erls = erls_ordne_alphabetisch,
25.12 rules = [Rule.Thm ("tausche_plus",TermC.num_str @{thm tausche_plus}),
25.13 (*"b kleiner a ==> (b + a) = (a + b)"*)
25.14 @@ -213,11 +213,11 @@
25.15 ], scr = Rule.EmptyScr};
25.16
25.17 val fasse_zusammen =
25.18 - Rule_Set.Rls{id = "fasse_zusammen", preconds = [],
25.19 + Rule_Def.Repeat{id = "fasse_zusammen", preconds = [],
25.20 rew_ord = ("dummy_ord", Rule.dummy_ord),
25.21 erls = Rule_Set.append_rls "erls_fasse_zusammen" Rule_Set.e_rls
25.22 [Rule.Num_Calc ("Prog_Expr.is'_const", Prog_Expr.eval_const "#is_const_")],
25.23 - srls = Rule_Set.Erls, calc = [], errpatts = [],
25.24 + srls = Rule_Set.Empty, calc = [], errpatts = [],
25.25 rules =
25.26 [Rule.Thm ("real_num_collect",TermC.num_str @{thm real_num_collect}),
25.27 (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
25.28 @@ -279,8 +279,8 @@
25.29 ], scr = Rule.EmptyScr};
25.30
25.31 val verschoenere =
25.32 - Rule_Set.Rls{id = "verschoenere", preconds = [],
25.33 - rew_ord = ("dummy_ord", Rule.dummy_ord), srls = Rule_Set.Erls, calc = [], errpatts = [],
25.34 + Rule_Def.Repeat{id = "verschoenere", preconds = [],
25.35 + rew_ord = ("dummy_ord", Rule.dummy_ord), srls = Rule_Set.Empty, calc = [], errpatts = [],
25.36 erls = Rule_Set.append_rls "erls_verschoenere" Rule_Set.e_rls
25.37 [Rule.Num_Calc ("PolyMinus.kleiner", eval_kleiner "")],
25.38 rules = [Rule.Thm ("vorzeichen_minus_weg1",TermC.num_str @{thm vorzeichen_minus_weg1}),
25.39 @@ -310,8 +310,8 @@
25.40 ], scr = Rule.EmptyScr} (*end verschoenere*);
25.41
25.42 val klammern_aufloesen =
25.43 - Rule_Set.Rls{id = "klammern_aufloesen", preconds = [],
25.44 - rew_ord = ("dummy_ord", Rule.dummy_ord), srls = Rule_Set.Erls, calc = [], errpatts = [], erls = Rule_Set.Erls,
25.45 + Rule_Def.Repeat{id = "klammern_aufloesen", preconds = [],
25.46 + rew_ord = ("dummy_ord", Rule.dummy_ord), srls = Rule_Set.Empty, calc = [], errpatts = [], erls = Rule_Set.Empty,
25.47 rules = [Rule.Thm ("sym_add_assoc",
25.48 TermC.num_str (@{thm add.assoc} RS @{thm sym})),
25.49 (*"a + (b + c) = (a + b) + c"*)
25.50 @@ -324,8 +324,8 @@
25.51 ], scr = Rule.EmptyScr};
25.52
25.53 val klammern_ausmultiplizieren =
25.54 - Rule_Set.Rls{id = "klammern_ausmultiplizieren", preconds = [],
25.55 - rew_ord = ("dummy_ord", Rule.dummy_ord), srls = Rule_Set.Erls, calc = [], errpatts = [], erls = Rule_Set.Erls,
25.56 + Rule_Def.Repeat{id = "klammern_ausmultiplizieren", preconds = [],
25.57 + rew_ord = ("dummy_ord", Rule.dummy_ord), srls = Rule_Set.Empty, calc = [], errpatts = [], erls = Rule_Set.Empty,
25.58 rules = [Rule.Thm ("distrib_right" ,TermC.num_str @{thm distrib_right}),
25.59 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
25.60 Rule.Thm ("distrib_left",TermC.num_str @{thm distrib_left}),
25.61 @@ -341,8 +341,8 @@
25.62 ], scr = Rule.EmptyScr};
25.63
25.64 val ordne_monome =
25.65 - Rule_Set.Rls{id = "ordne_monome", preconds = [],
25.66 - rew_ord = ("dummy_ord", Rule.dummy_ord), srls = Rule_Set.Erls, calc = [], errpatts = [],
25.67 + Rule_Def.Repeat{id = "ordne_monome", preconds = [],
25.68 + rew_ord = ("dummy_ord", Rule.dummy_ord), srls = Rule_Set.Empty, calc = [], errpatts = [],
25.69 erls = Rule_Set.append_rls "erls_ordne_monome" Rule_Set.e_rls
25.70 [Rule.Num_Calc ("PolyMinus.kleiner", eval_kleiner ""),
25.71 Rule.Num_Calc ("Prog_Expr.is'_atom", Prog_Expr.eval_is_atom "")
25.72 @@ -393,7 +393,7 @@
25.73 (** problems **)
25.74 setup \<open>KEStore_Elems.add_pbts
25.75 [(Specify.prep_pbt thy "pbl_vereinf_poly" [] Celem.e_pblID
25.76 - (["polynom","vereinfachen"], [], Rule_Set.Erls, NONE, [])),
25.77 + (["polynom","vereinfachen"], [], Rule_Set.Empty, NONE, [])),
25.78 (Specify.prep_pbt thy "pbl_vereinf_poly_minus" [] Celem.e_pblID
25.79 (["plus_minus","polynom","vereinfachen"],
25.80 [("#Given", ["Term t_t"]),
25.81 @@ -450,7 +450,7 @@
25.82 Rule.Num_Calc ("Poly.is'_polyexp", eval_is_polyexp "")],
25.83 SOME "Vereinfache t_t",
25.84 [["simplification","for_polynomials","with_parentheses_mult"]])),
25.85 - (Specify.prep_pbt thy "pbl_probe" [] Celem.e_pblID (["probe"], [], Rule_Set.Erls, NONE, [])),
25.86 + (Specify.prep_pbt thy "pbl_probe" [] Celem.e_pblID (["probe"], [], Rule_Set.Empty, NONE, [])),
25.87 (Specify.prep_pbt thy "pbl_probe_poly" [] Celem.e_pblID
25.88 (["polynom","probe"],
25.89 [("#Given", ["Pruefe e_e", "mitWert w_w"]),
25.90 @@ -552,8 +552,8 @@
25.91 setup \<open>KEStore_Elems.add_mets
25.92 [Specify.prep_met thy "met_probe" [] Celem.e_metID
25.93 (["probe"], [],
25.94 - {rew_ord'="tless_true", rls' = Rule_Set.e_rls, calc = [], srls = Rule_Set.e_rls, prls = Rule_Set.Erls, crls = Rule_Set.e_rls,
25.95 - errpats = [], nrls = Rule_Set.Erls},
25.96 + {rew_ord'="tless_true", rls' = Rule_Set.e_rls, calc = [], srls = Rule_Set.e_rls, prls = Rule_Set.Empty, crls = Rule_Set.e_rls,
25.97 + errpats = [], nrls = Rule_Set.Empty},
25.98 @{thm refl})]
25.99 \<close>
25.100
25.101 @@ -590,7 +590,7 @@
25.102 {rew_ord'="tless_true", rls' = Rule_Set.e_rls, calc = [], srls = Rule_Set.e_rls,
25.103 prls = Rule_Set.append_rls "prls_met_probe_bruch" Rule_Set.e_rls
25.104 [(*for preds in where_*) Rule.Num_Calc ("Rational.is'_ratpolyexp", eval_is_ratpolyexp "")],
25.105 - crls = Rule_Set.e_rls, errpats = [], nrls = Rule_Set.Erls},
25.106 + crls = Rule_Set.e_rls, errpats = [], nrls = Rule_Set.Empty},
25.107 @{thm refl})]
25.108 \<close>
25.109
26.1 --- a/src/Tools/isac/Knowledge/RatEq.thy Sat Apr 04 12:11:32 2020 +0200
26.2 +++ b/src/Tools/isac/Knowledge/RatEq.thy Mon Apr 06 11:44:36 2020 +0200
26.3 @@ -118,9 +118,9 @@
26.4 Rule.Thm ("or_commute",TermC.num_str @{thm or_commute})]; (*WN: ein Hack*)
26.5
26.6 val RatEq_eliminate = prep_rls'(
26.7 - Rule_Set.Rls
26.8 + Rule_Def.Repeat
26.9 {id = "RatEq_eliminate", preconds = [], rew_ord = ("termlessI", termlessI), erls = rateq_erls,
26.10 - srls = Rule_Set.Erls, calc = [], errpatts = [],
26.11 + srls = Rule_Set.Empty, calc = [], errpatts = [],
26.12 rules = [
26.13 Rule.Thm("rat_mult_denominator_both",TermC.num_str @{thm rat_mult_denominator_both}),
26.14 (* a/b=c/d -> ad=cb *)
26.15 @@ -133,9 +133,9 @@
26.16
26.17 \<close> ML \<open>
26.18 val RatEq_simplify = prep_rls'(
26.19 - Rule_Set.Rls
26.20 + Rule_Def.Repeat
26.21 {id = "RatEq_simplify", preconds = [], rew_ord = ("termlessI", termlessI), erls = rateq_erls,
26.22 - srls = Rule_Set.Erls, calc = [], errpatts = [],
26.23 + srls = Rule_Set.Empty, calc = [], errpatts = [],
26.24 rules = [
26.25 Rule.Thm("real_rat_mult_1",TermC.num_str @{thm real_rat_mult_1}),
26.26 (*a*(b/c) = (a*b)/c*)
27.1 --- a/src/Tools/isac/Knowledge/Rational-WN.sml Sat Apr 04 12:11:32 2020 +0200
27.2 +++ b/src/Tools/isac/Knowledge/Rational-WN.sml Mon Apr 06 11:44:36 2020 +0200
27.3 @@ -186,7 +186,7 @@
27.4 fun rewrite_set_' thy rls put_asm ruless ct =
27.5 case ruless of
27.6 Rule_Set.Rrls _ => error "rewrite_set_' not for Rule_Set.Rrls"
27.7 - | Rule_Set.Rls _ =>
27.8 + | Rule_Def.Repeat _ =>
27.9 let
27.10 datatype switch = Appl | Noap;
27.11 fun rew_once ruls asm ct Noap [] = (ct,asm)
27.12 @@ -222,7 +222,7 @@
27.13 fun rewrite_set_' thy rls put_asm ruless ct =
27.14 case ruless of
27.15 Rule_Set.Rrls _ => error "rewrite_set_' not for Rule_Set.Rrls"
27.16 - | Rule_Set.Rls _ =>
27.17 + | Rule_Def.Repeat _ =>
27.18 let
27.19 datatype switch = Appl | Noap;
27.20 fun rew_once ruls asm ct Noap [] = (ct,asm)
28.1 --- a/src/Tools/isac/Knowledge/Rational.thy Sat Apr 04 12:11:32 2020 +0200
28.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Mon Apr 06 11:44:36 2020 +0200
28.3 @@ -391,8 +391,8 @@
28.4 (* evaluates conditions in calculate_Rational *)
28.5 val calc_rat_erls =
28.6 prep_rls'
28.7 - (Rule_Set.Rls {id = "calc_rat_erls", preconds = [], rew_ord = ("dummy_ord", Rule.dummy_ord),
28.8 - erls = Rule_Set.e_rls, srls = Rule_Set.Erls, calc = [], errpatts = [],
28.9 + (Rule_Def.Repeat {id = "calc_rat_erls", preconds = [], rew_ord = ("dummy_ord", Rule.dummy_ord),
28.10 + erls = Rule_Set.e_rls, srls = Rule_Set.Empty, calc = [], errpatts = [],
28.11 rules =
28.12 [Rule.Num_Calc ("HOL.eq", Prog_Expr.eval_equal "#equal_"),
28.13 Rule.Num_Calc ("Prog_Expr.is'_const", Prog_Expr.eval_const "#is_const_"),
28.14 @@ -405,8 +405,8 @@
28.15 need to have constants to be commuted together respectively *)
28.16 val calculate_Rational =
28.17 prep_rls' (Rule_Set.merge_rls "calculate_Rational"
28.18 - (Rule_Set.Rls {id = "divide", preconds = [], rew_ord = ("dummy_ord", Rule.dummy_ord),
28.19 - erls = calc_rat_erls, srls = Rule_Set.Erls,
28.20 + (Rule_Def.Repeat {id = "divide", preconds = [], rew_ord = ("dummy_ord", Rule.dummy_ord),
28.21 + erls = calc_rat_erls, srls = Rule_Set.Empty,
28.22 calc = [], errpatts = [],
28.23 rules =
28.24 [Rule.Num_Calc ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"),
28.25 @@ -603,8 +603,8 @@
28.26 ML \<open>
28.27 (*erls for calculate_Rational; make local with FIXX@ME result:term *term list*)
28.28 val powers_erls = prep_rls'(
28.29 - Rule_Set.Rls {id = "powers_erls", preconds = [], rew_ord = ("dummy_ord",Rule.dummy_ord),
28.30 - erls = Rule_Set.e_rls, srls = Rule_Set.Erls, calc = [], errpatts = [],
28.31 + Rule_Def.Repeat {id = "powers_erls", preconds = [], rew_ord = ("dummy_ord",Rule.dummy_ord),
28.32 + erls = Rule_Set.e_rls, srls = Rule_Set.Empty, calc = [], errpatts = [],
28.33 rules = [Rule.Num_Calc ("Prog_Expr.is'_atom", Prog_Expr.eval_is_atom "#is_atom_"),
28.34 Rule.Num_Calc ("Prog_Expr.is'_even", Prog_Expr.eval_is_even "#is_even_"),
28.35 Rule.Num_Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
28.36 @@ -617,8 +617,8 @@
28.37 (*.all powers over + distributed; atoms over * collected, other distributed
28.38 contains absolute minimum of thms for context in norm_Rational .*)
28.39 val powers = prep_rls'(
28.40 - Rule_Set.Rls {id = "powers", preconds = [], rew_ord = ("dummy_ord",Rule.dummy_ord),
28.41 - erls = powers_erls, srls = Rule_Set.Erls, calc = [], errpatts = [],
28.42 + Rule_Def.Repeat {id = "powers", preconds = [], rew_ord = ("dummy_ord",Rule.dummy_ord),
28.43 + erls = powers_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
28.44 rules = [Rule.Thm ("realpow_multI", TermC.num_str @{thm realpow_multI}),
28.45 (*"(r * s) ^^^ n = r ^^^ n * s ^^^ n"*)
28.46 Rule.Thm ("realpow_pow",TermC.num_str @{thm realpow_pow}),
28.47 @@ -649,9 +649,9 @@
28.48 });
28.49 (*.contains absolute minimum of thms for context in norm_Rational.*)
28.50 val rat_mult_divide = prep_rls'(
28.51 - Rule_Set.Rls {id = "rat_mult_divide", preconds = [],
28.52 + Rule_Def.Repeat {id = "rat_mult_divide", preconds = [],
28.53 rew_ord = ("dummy_ord", Rule.dummy_ord),
28.54 - erls = Rule_Set.e_rls, srls = Rule_Set.Erls, calc = [], errpatts = [],
28.55 + erls = Rule_Set.e_rls, srls = Rule_Set.Empty, calc = [], errpatts = [],
28.56 rules = [Rule.Thm ("rat_mult",TermC.num_str @{thm rat_mult}),
28.57 (*(1)"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)
28.58 Rule.Thm ("times_divide_eq_right",TermC.num_str @{thm times_divide_eq_right}),
28.59 @@ -674,8 +674,8 @@
28.60
28.61 (*.contains absolute minimum of thms for context in norm_Rational.*)
28.62 val reduce_0_1_2 = prep_rls'(
28.63 - Rule_Set.Rls{id = "reduce_0_1_2", preconds = [], rew_ord = ("dummy_ord", Rule.dummy_ord),
28.64 - erls = Rule_Set.e_rls, srls = Rule_Set.Erls, calc = [], errpatts = [],
28.65 + Rule_Def.Repeat{id = "reduce_0_1_2", preconds = [], rew_ord = ("dummy_ord", Rule.dummy_ord),
28.66 + erls = Rule_Set.e_rls, srls = Rule_Set.Empty, calc = [], errpatts = [],
28.67 rules = [(*Rule.Thm ("divide_1",TermC.num_str @{thm divide_1}),
28.68 "?x / 1 = ?x" unnecess.for normalform*)
28.69 Rule.Thm ("mult_1_left",TermC.num_str @{thm mult_1_left}),
28.70 @@ -705,8 +705,8 @@
28.71 (*erls for calculate_Rational;
28.72 make local with FIXX@ME result:term *term list WN0609???SKMG*)
28.73 val norm_rat_erls = prep_rls'(
28.74 - Rule_Set.Rls {id = "norm_rat_erls", preconds = [], rew_ord = ("dummy_ord",Rule.dummy_ord),
28.75 - erls = Rule_Set.e_rls, srls = Rule_Set.Erls, calc = [], errpatts = [],
28.76 + Rule_Def.Repeat {id = "norm_rat_erls", preconds = [], rew_ord = ("dummy_ord",Rule.dummy_ord),
28.77 + erls = Rule_Set.e_rls, srls = Rule_Set.Empty, calc = [], errpatts = [],
28.78 rules = [Rule.Num_Calc ("Prog_Expr.is'_const", Prog_Expr.eval_const "#is_const_")
28.79 ], scr = Rule.EmptyScr});
28.80
28.81 @@ -714,8 +714,8 @@
28.82 (*040209: this version has been used by RL for his equations,
28.83 which is now replaced by MGs version "norm_Rational" below *)
28.84 val norm_Rational_min = prep_rls'(
28.85 - Rule_Set.Rls {id = "norm_Rational_min", preconds = [], rew_ord = ("dummy_ord",Rule.dummy_ord),
28.86 - erls = norm_rat_erls, srls = Rule_Set.Erls, calc = [], errpatts = [],
28.87 + Rule_Def.Repeat {id = "norm_Rational_min", preconds = [], rew_ord = ("dummy_ord",Rule.dummy_ord),
28.88 + erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
28.89 rules = [(*sequence given by operator precedence*)
28.90 Rule.Rls_ discard_minus,
28.91 Rule.Rls_ powers,
28.92 @@ -730,9 +730,9 @@
28.93 scr = Rule.EmptyScr});
28.94
28.95 val norm_Rational_parenthesized = prep_rls'(
28.96 - Rule_Set.Seq {id = "norm_Rational_parenthesized", preconds = []:term list,
28.97 + Rule_Set.Seqence {id = "norm_Rational_parenthesized", preconds = []:term list,
28.98 rew_ord = ("dummy_ord", Rule.dummy_ord),
28.99 - erls = Atools_erls, srls = Rule_Set.Erls,
28.100 + erls = Atools_erls, srls = Rule_Set.Empty,
28.101 calc = [], errpatts = [],
28.102 rules = [Rule.Rls_ norm_Rational_min,
28.103 Rule.Rls_ discard_parentheses
28.104 @@ -762,25 +762,25 @@
28.105 \<close>
28.106 ML \<open>
28.107 val add_fractions_p_rls = prep_rls'(
28.108 - Rule_Set.Rls {id = "add_fractions_p_rls", preconds = [], rew_ord = ("dummy_ord", Rule.dummy_ord),
28.109 - erls = Rule_Set.e_rls, srls = Rule_Set.Erls, calc = [], errpatts = [],
28.110 + Rule_Def.Repeat {id = "add_fractions_p_rls", preconds = [], rew_ord = ("dummy_ord", Rule.dummy_ord),
28.111 + erls = Rule_Set.e_rls, srls = Rule_Set.Empty, calc = [], errpatts = [],
28.112 rules = [Rule.Rls_ add_fractions_p],
28.113 scr = Rule.EmptyScr});
28.114
28.115 -(* "Rule_Set.Rls" causes repeated application of cancel_p to one and the same term *)
28.116 +(* "Rule_Def.Repeat" causes repeated application of cancel_p to one and the same term *)
28.117 val cancel_p_rls = prep_rls'(
28.118 - Rule_Set.Rls
28.119 + Rule_Def.Repeat
28.120 {id = "cancel_p_rls", preconds = [], rew_ord = ("dummy_ord", Rule.dummy_ord),
28.121 - erls = Rule_Set.e_rls, srls = Rule_Set.Erls, calc = [], errpatts = [],
28.122 + erls = Rule_Set.e_rls, srls = Rule_Set.Empty, calc = [], errpatts = [],
28.123 rules = [Rule.Rls_ cancel_p],
28.124 scr = Rule.EmptyScr});
28.125
28.126 (*. makes 'normal' fractions; 'is_polyexp' inhibits double fractions;
28.127 used in initial part norm_Rational_mg, see example DA-M02-main.p.60.*)
28.128 val rat_mult_poly = prep_rls'(
28.129 - Rule_Set.Rls {id = "rat_mult_poly", preconds = [], rew_ord = ("dummy_ord", Rule.dummy_ord),
28.130 + Rule_Def.Repeat {id = "rat_mult_poly", preconds = [], rew_ord = ("dummy_ord", Rule.dummy_ord),
28.131 erls = Rule_Set.append_rls "Rule_Set.e_rls-is_polyexp" Rule_Set.e_rls [Rule.Num_Calc ("Poly.is'_polyexp", eval_is_polyexp "")],
28.132 - srls = Rule_Set.Erls, calc = [], errpatts = [],
28.133 + srls = Rule_Set.Empty, calc = [], errpatts = [],
28.134 rules =
28.135 [Rule.Thm ("rat_mult_poly_l",TermC.num_str @{thm rat_mult_poly_l}),
28.136 (*"?c is_polyexp ==> ?c * (?a / ?b) = ?c * ?a / ?b"*)
28.137 @@ -794,8 +794,8 @@
28.138 I.E. THE RESPECTIVE ASSUMPTION IS STORED AND Rule.Thm APPLIED; WN051028
28.139 ... WN0609???MG.*)
28.140 val rat_mult_div_pow = prep_rls'(
28.141 - Rule_Set.Rls {id = "rat_mult_div_pow", preconds = [], rew_ord = ("dummy_ord",Rule.dummy_ord),
28.142 - erls = Rule_Set.e_rls, srls = Rule_Set.Erls, calc = [], errpatts = [],
28.143 + Rule_Def.Repeat {id = "rat_mult_div_pow", preconds = [], rew_ord = ("dummy_ord",Rule.dummy_ord),
28.144 + erls = Rule_Set.e_rls, srls = Rule_Set.Empty, calc = [], errpatts = [],
28.145 rules = [Rule.Thm ("rat_mult", TermC.num_str @{thm rat_mult}),
28.146 (*"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)
28.147 Rule.Thm ("rat_mult_poly_l", TermC.num_str @{thm rat_mult_poly_l}),
28.148 @@ -817,8 +817,8 @@
28.149 scr = Rule.EmptyScr});
28.150
28.151 val rat_reduce_1 = prep_rls'(
28.152 - Rule_Set.Rls {id = "rat_reduce_1", preconds = [], rew_ord = ("dummy_ord", Rule.dummy_ord),
28.153 - erls = Rule_Set.e_rls, srls = Rule_Set.Erls, calc = [], errpatts = [],
28.154 + Rule_Def.Repeat {id = "rat_reduce_1", preconds = [], rew_ord = ("dummy_ord", Rule.dummy_ord),
28.155 + erls = Rule_Set.e_rls, srls = Rule_Set.Empty, calc = [], errpatts = [],
28.156 rules =
28.157 [Rule.Thm ("div_by_1", TermC.num_str @{thm div_by_1}),
28.158 (*"?x / 1 = ?x"*)
28.159 @@ -829,8 +829,8 @@
28.160
28.161 (* looping part of norm_Rational *)
28.162 val norm_Rational_rls = prep_rls' (
28.163 - Rule_Set.Rls {id = "norm_Rational_rls", preconds = [], rew_ord = ("dummy_ord",Rule.dummy_ord),
28.164 - erls = norm_rat_erls, srls = Rule_Set.Erls, calc = [], errpatts = [],
28.165 + Rule_Def.Repeat {id = "norm_Rational_rls", preconds = [], rew_ord = ("dummy_ord",Rule.dummy_ord),
28.166 + erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
28.167 rules = [Rule.Rls_ add_fractions_p_rls,
28.168 Rule.Rls_ rat_mult_div_pow,
28.169 Rule.Rls_ make_rat_poly_with_parentheses,
28.170 @@ -840,9 +840,9 @@
28.171 scr = Rule.EmptyScr});
28.172
28.173 val norm_Rational = prep_rls' (
28.174 - Rule_Set.Seq
28.175 + Rule_Set.Seqence
28.176 {id = "norm_Rational", preconds = [], rew_ord = ("dummy_ord", Rule.dummy_ord),
28.177 - erls = norm_rat_erls, srls = Rule_Set.Erls, calc = [], errpatts = [],
28.178 + erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
28.179 rules = [Rule.Rls_ discard_minus,
28.180 Rule.Rls_ rat_mult_poly, (* removes double fractions like a/b/c *)
28.181 Rule.Rls_ make_rat_poly_with_parentheses,
29.1 --- a/src/Tools/isac/Knowledge/Root.thy Sat Apr 04 12:11:32 2020 +0200
29.2 +++ b/src/Tools/isac/Knowledge/Root.thy Mon Apr 06 11:44:36 2020 +0200
29.3 @@ -189,9 +189,9 @@
29.4 ML \<open>
29.5
29.6 val make_rooteq = prep_rls'(
29.7 - Rule_Set.Rls{id = "make_rooteq", preconds = []:term list,
29.8 + Rule_Def.Repeat{id = "make_rooteq", preconds = []:term list,
29.9 rew_ord = ("sqrt_right", sqrt_right false thy),
29.10 - erls = Atools_erls, srls = Rule_Set.Erls,
29.11 + erls = Atools_erls, srls = Rule_Set.Empty,
29.12 calc = [], errpatts = [],
29.13 rules = [Rule.Thm ("real_diff_minus",TermC.num_str @{thm real_diff_minus}),
29.14 (*"a - b = a + (-1) * b"*)
29.15 @@ -259,9 +259,9 @@
29.16 val prep_rls' = Auto_Prog.prep_rls @{theory};
29.17
29.18 val expand_rootbinoms = prep_rls'(
29.19 - Rule_Set.Rls{id = "expand_rootbinoms", preconds = [],
29.20 + Rule_Def.Repeat{id = "expand_rootbinoms", preconds = [],
29.21 rew_ord = ("termlessI",termlessI),
29.22 - erls = Atools_erls, srls = Rule_Set.Erls,
29.23 + erls = Atools_erls, srls = Rule_Set.Empty,
29.24 calc = [], errpatts = [],
29.25 rules = [Rule.Thm ("real_plus_binom_pow2" ,TermC.num_str @{thm real_plus_binom_pow2}),
29.26 (*"(a + b) ^^^ 2 = a ^^^ 2 + 2 * a * b + b ^^^ 2"*)
30.1 --- a/src/Tools/isac/Knowledge/RootEq.thy Sat Apr 04 12:11:32 2020 +0200
30.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy Mon Apr 06 11:44:36 2020 +0200
30.3 @@ -214,8 +214,8 @@
30.4
30.5 (*isolate the bound variable in an sqrt equation; 'bdv' is a meta-constant*)
30.6 val sqrt_isolate = prep_rls'(
30.7 - Rule_Set.Rls {id = "sqrt_isolate", preconds = [], rew_ord = ("termlessI",termlessI),
30.8 - erls = RootEq_erls, srls = Rule_Set.Erls, calc = [], errpatts = [],
30.9 + Rule_Def.Repeat {id = "sqrt_isolate", preconds = [], rew_ord = ("termlessI",termlessI),
30.10 + erls = RootEq_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
30.11 rules = [
30.12 Rule.Thm("sqrt_square_1",TermC.num_str @{thm sqrt_square_1}),
30.13 (* (sqrt a)^^^2 -> a *)
30.14 @@ -313,9 +313,9 @@
30.15 \<close> ML \<open>
30.16 (*isolate the bound variable in an sqrt left equation; 'bdv' is a meta-constant*)
30.17 val l_sqrt_isolate = prep_rls'(
30.18 - Rule_Set.Rls {id = "l_sqrt_isolate", preconds = [],
30.19 + Rule_Def.Repeat {id = "l_sqrt_isolate", preconds = [],
30.20 rew_ord = ("termlessI",termlessI),
30.21 - erls = RootEq_erls, srls = Rule_Set.Erls, calc = [], errpatts = [],
30.22 + erls = RootEq_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
30.23 rules = [
30.24 Rule.Thm("sqrt_square_1",TermC.num_str @{thm sqrt_square_1}),
30.25 (* (sqrt a)^^^2 -> a *)
30.26 @@ -359,9 +359,9 @@
30.27 (* -- right 28.8.02--*)
30.28 (*isolate the bound variable in an sqrt right equation; 'bdv' is a meta-constant*)
30.29 val r_sqrt_isolate = prep_rls'(
30.30 - Rule_Set.Rls {id = "r_sqrt_isolate", preconds = [],
30.31 + Rule_Def.Repeat {id = "r_sqrt_isolate", preconds = [],
30.32 rew_ord = ("termlessI",termlessI),
30.33 - erls = RootEq_erls, srls = Rule_Set.Erls, calc = [], errpatts = [],
30.34 + erls = RootEq_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
30.35 rules = [
30.36 Rule.Thm("sqrt_square_1",TermC.num_str @{thm sqrt_square_1}),
30.37 (* (sqrt a)^^^2 -> a *)
30.38 @@ -403,9 +403,9 @@
30.39
30.40 \<close> ML \<open>
30.41 val rooteq_simplify = prep_rls'(
30.42 - Rule_Set.Rls {id = "rooteq_simplify",
30.43 + Rule_Def.Repeat {id = "rooteq_simplify",
30.44 preconds = [], rew_ord = ("termlessI",termlessI),
30.45 - erls = RootEq_erls, srls = Rule_Set.Erls, calc = [], errpatts = [],
30.46 + erls = RootEq_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
30.47 (*asm_thm = [("sqrt_square_1","")],*)
30.48 rules = [Rule.Thm ("real_assoc_1",TermC.num_str @{thm real_assoc_1}),
30.49 (* a+(b+c) = a+b+c *)
31.1 --- a/src/Tools/isac/Knowledge/RootRatEq.thy Sat Apr 04 12:11:32 2020 +0200
31.2 +++ b/src/Tools/isac/Knowledge/RootRatEq.thy Mon Apr 06 11:44:36 2020 +0200
31.3 @@ -101,9 +101,9 @@
31.4 \<close> ML \<open>
31.5 (* Solves a rootrat Equation *)
31.6 val rootrat_solve = prep_rls'(
31.7 - Rule_Set.Rls {id = "rootrat_solve", preconds = [],
31.8 + Rule_Def.Repeat {id = "rootrat_solve", preconds = [],
31.9 rew_ord = ("termlessI",termlessI),
31.10 - erls = Rule_Set.e_rls, srls = Rule_Set.Erls, calc = [], errpatts = [],
31.11 + erls = Rule_Set.e_rls, srls = Rule_Set.Empty, calc = [], errpatts = [],
31.12 rules =
31.13 [Rule.Thm("rootrat_equation_left_1", TermC.num_str @{thm rootrat_equation_left_1}),
31.14 (* [|c is_rootTerm_in bdv|] ==>
32.1 --- a/src/Tools/isac/Knowledge/Test.thy Sat Apr 04 12:11:32 2020 +0200
32.2 +++ b/src/Tools/isac/Knowledge/Test.thy Mon Apr 06 11:44:36 2020 +0200
32.3 @@ -359,8 +359,8 @@
32.4 section \<open>rulesets\<close>
32.5 ML \<open>
32.6 val testerls =
32.7 - Rule_Set.Rls {id = "testerls", preconds = [], rew_ord = ("termlessI",termlessI),
32.8 - erls = Rule_Set.e_rls, srls = Rule_Set.Erls,
32.9 + Rule_Def.Repeat {id = "testerls", preconds = [], rew_ord = ("termlessI",termlessI),
32.10 + erls = Rule_Set.e_rls, srls = Rule_Set.Empty,
32.11 calc = [], errpatts = [],
32.12 rules = [Rule.Thm ("refl",TermC.num_str @{thm refl}),
32.13 Rule.Thm ("order_refl",TermC.num_str @{thm order_refl}),
32.14 @@ -392,7 +392,7 @@
32.15 (*.for evaluation of conditions in rewrite rules.*)
32.16 (*FIXXXXXXME 10.8.02: handle like _simplify*)
32.17 val tval_rls =
32.18 - Rule_Set.Rls{id = "tval_rls", preconds = [],
32.19 + Rule_Def.Repeat{id = "tval_rls", preconds = [],
32.20 rew_ord = ("sqrt_right",sqrt_right false @{theory "Pure"}),
32.21 erls=testerls,srls = Rule_Set.e_rls,
32.22 calc=[], errpatts = [],
32.23 @@ -438,7 +438,7 @@
32.24 ML \<open>
32.25 (*make () dissappear*)
32.26 val rearrange_assoc =
32.27 - Rule_Set.Rls{id = "rearrange_assoc", preconds = [],
32.28 + Rule_Def.Repeat{id = "rearrange_assoc", preconds = [],
32.29 rew_ord = ("e_rew_ord",Rule.e_rew_ord),
32.30 erls = Rule_Set.e_rls, srls = Rule_Set.e_rls, calc = [], errpatts = [],
32.31 rules =
32.32 @@ -448,7 +448,7 @@
32.33 };
32.34
32.35 val ac_plus_times =
32.36 - Rule_Set.Rls{id = "ac_plus_times", preconds = [], rew_ord = ("term_order",term_order),
32.37 + Rule_Def.Repeat{id = "ac_plus_times", preconds = [], rew_ord = ("term_order",term_order),
32.38 erls = Rule_Set.e_rls, srls = Rule_Set.e_rls, calc = [], errpatts = [],
32.39 rules =
32.40 [Rule.Thm ("radd_commute",TermC.num_str @{thm radd_commute}),
32.41 @@ -462,7 +462,7 @@
32.42
32.43 (*todo: replace by Rewrite("rnorm_equation_add",TermC.num_str @{thm rnorm_equation_add)*)
32.44 val norm_equation =
32.45 - Rule_Set.Rls{id = "norm_equation", preconds = [], rew_ord = ("e_rew_ord",Rule.e_rew_ord),
32.46 + Rule_Def.Repeat{id = "norm_equation", preconds = [], rew_ord = ("e_rew_ord",Rule.e_rew_ord),
32.47 erls = tval_rls, srls = Rule_Set.e_rls, calc = [], errpatts = [],
32.48 rules = [Rule.Thm ("rnorm_equation_add",TermC.num_str @{thm rnorm_equation_add})
32.49 ],
32.50 @@ -472,7 +472,7 @@
32.51 ML \<open>
32.52 (* expects * distributed over + *)
32.53 val Test_simplify =
32.54 - Rule_Set.Rls{id = "Test_simplify", preconds = [],
32.55 + Rule_Def.Repeat{id = "Test_simplify", preconds = [],
32.56 rew_ord = ("sqrt_right",sqrt_right false @{theory "Pure"}),
32.57 erls = tval_rls, srls = Rule_Set.e_rls,
32.58 calc=[(*since 040209 filled by prep_rls'*)], errpatts = [],
32.59 @@ -529,7 +529,7 @@
32.60 ML \<open>
32.61 (*isolate the root in a root-equation*)
32.62 val isolate_root =
32.63 - Rule_Set.Rls{id = "isolate_root", preconds = [], rew_ord = ("e_rew_ord",Rule.e_rew_ord),
32.64 + Rule_Def.Repeat{id = "isolate_root", preconds = [], rew_ord = ("e_rew_ord",Rule.e_rew_ord),
32.65 erls=tval_rls,srls = Rule_Set.e_rls, calc=[], errpatts = [],
32.66 rules = [Rule.Thm ("rroot_to_lhs",TermC.num_str @{thm rroot_to_lhs}),
32.67 Rule.Thm ("rroot_to_lhs_mult",TermC.num_str @{thm rroot_to_lhs_mult}),
32.68 @@ -543,7 +543,7 @@
32.69
32.70 (*isolate the bound variable in an equation; 'bdv' is a meta-constant*)
32.71 val isolate_bdv =
32.72 - Rule_Set.Rls{id = "isolate_bdv", preconds = [], rew_ord = ("e_rew_ord",Rule.e_rew_ord),
32.73 + Rule_Def.Repeat{id = "isolate_bdv", preconds = [], rew_ord = ("e_rew_ord",Rule.e_rew_ord),
32.74 erls=tval_rls,srls = Rule_Set.e_rls, calc= [], errpatts = [],
32.75 rules =
32.76 [Rule.Thm ("risolate_bdv_add",TermC.num_str @{thm risolate_bdv_add}),
32.77 @@ -599,9 +599,9 @@
32.78 ]);
32.79
32.80 val make_polytest =
32.81 - Rule_Set.Rls{id = "make_polytest", preconds = []:term list,
32.82 + Rule_Def.Repeat{id = "make_polytest", preconds = []:term list,
32.83 rew_ord = ("ord_make_polytest", ord_make_polytest false @{theory "Poly"}),
32.84 - erls = testerls, srls = Rule_Set.Erls,
32.85 + erls = testerls, srls = Rule_Set.Empty,
32.86 calc = [("PLUS" , ("Groups.plus_class.plus", (**)eval_binop "#add_")),
32.87 ("TIMES" , ("Groups.times_class.times", (**)eval_binop "#mult_")),
32.88 ("POWER", ("Prog_Expr.pow", (**)eval_binop "#power_"))
32.89 @@ -667,9 +667,9 @@
32.90 };
32.91
32.92 val expand_binomtest =
32.93 - Rule_Set.Rls{id = "expand_binomtest", preconds = [],
32.94 + Rule_Def.Repeat{id = "expand_binomtest", preconds = [],
32.95 rew_ord = ("termlessI",termlessI),
32.96 - erls = testerls, srls = Rule_Set.Erls,
32.97 + erls = testerls, srls = Rule_Set.Empty,
32.98 calc = [("PLUS" , ("Groups.plus_class.plus", (**)eval_binop "#add_")),
32.99 ("TIMES" , ("Groups.times_class.times", (**)eval_binop "#mult_")),
32.100 ("POWER", ("Prog_Expr.pow", (**)eval_binop "#power_"))
33.1 --- a/src/Tools/isac/Knowledge/Test_Build_Thydata.thy Sat Apr 04 12:11:32 2020 +0200
33.2 +++ b/src/Tools/isac/Knowledge/Test_Build_Thydata.thy Mon Apr 06 11:44:36 2020 +0200
33.3 @@ -13,15 +13,15 @@
33.4 thm222: "thm222 = thm222 + (222::int)"
33.5
33.6 ML \<open>
33.7 -val rls111 = Rule_Set.Rls {id = "rls111",
33.8 +val rls111 = Rule_Def.Repeat {id = "rls111",
33.9 preconds = [], rew_ord = ("termlessI", termlessI), erls = Rule_Set.e_rls,
33.10 - srls = Rule_Set.Erls, calc = [], errpatts = [],
33.11 + srls = Rule_Set.Empty, calc = [], errpatts = [],
33.12 rules = [Rule.Thm ("thm111", @{thm thm111}), Rule.Thm ("refl", @{thm refl})],
33.13 scr = Rule.EmptyScr};
33.14
33.15 -val rls222 = Rule_Set.Rls {id = "rls222",
33.16 +val rls222 = Rule_Def.Repeat {id = "rls222",
33.17 preconds = [], rew_ord = ("termlessI", termlessI), erls = Rule_Set.e_rls,
33.18 - srls = Rule_Set.Erls, calc = [], errpatts = [],
33.19 + srls = Rule_Set.Empty, calc = [], errpatts = [],
33.20 rules = [Rule.Thm ("sym_thm111", @{thm thm111} RS @{thm sym}), Rule.Thm ("o_def", @{thm o_def})],
33.21 scr = Rule.EmptyScr};
33.22
33.23 @@ -45,21 +45,21 @@
33.24 case ddd of
33.25 ("rls111",
33.26 ("Test_Build_Thydata",
33.27 - Rule_Set.Rls {calc = [], erls =
33.28 - Rule_Set.Rls {calc = [], erls = Erls, errpatts = [], id = "e_rls", preconds = [], rew_ord =
33.29 - ("dummy_ord", _), rules = [], scr = EmptyScr, srls = Rule_Set.Erls},
33.30 + Rule_Def.Repeat {calc = [], erls =
33.31 + Rule_Def.Repeat {calc = [], erls = Erls, errpatts = [], id = "e_rls", preconds = [], rew_ord =
33.32 + ("dummy_ord", _), rules = [], scr = EmptyScr, srls = Rule_Set.Empty},
33.33 errpatts = [], id = "rls111", preconds = [], rew_ord = ("termlessI", _), rules =
33.34 - [Thm ("thm111", _), Thm ("refl", _)], scr = EmptyScr, srls = Rule_Set.Erls})) => ()
33.35 + [Thm ("thm111", _), Thm ("refl", _)], scr = EmptyScr, srls = Rule_Set.Empty})) => ()
33.36 | _ => error "test/../thy-hierarchy CHANGED 4";
33.37 \<close> ML \<open>
33.38 case eee of
33.39 ("rls222",
33.40 ("Test_Build_Thydata",
33.41 - Rule_Set.Rls {calc = [], erls =
33.42 - Rule_Set.Rls {calc = [], erls = Erls, errpatts = [], id = "e_rls", preconds = [], rew_ord =
33.43 - ("dummy_ord", _), rules = [], scr = EmptyScr, srls = Rule_Set.Erls},
33.44 + Rule_Def.Repeat {calc = [], erls =
33.45 + Rule_Def.Repeat {calc = [], erls = Erls, errpatts = [], id = "e_rls", preconds = [], rew_ord =
33.46 + ("dummy_ord", _), rules = [], scr = EmptyScr, srls = Rule_Set.Empty},
33.47 errpatts = [], id = "rls222", preconds = [], rew_ord = ("termlessI", _), rules =
33.48 - [Thm ("sym_thm111", _), Thm ("o_def", _)], scr = EmptyScr, srls = Rule_Set.Erls})) => ()
33.49 + [Thm ("sym_thm111", _), Thm ("o_def", _)], scr = EmptyScr, srls = Rule_Set.Empty})) => ()
33.50 | _ => error "test/../thy-hierarchy CHANGED 5";
33.51 \<close>
33.52
34.1 --- a/src/Tools/isac/MathEngBasic/ctree-basic.sml Sat Apr 04 12:11:32 2020 +0200
34.2 +++ b/src/Tools/isac/MathEngBasic/ctree-basic.sml Mon Apr 06 11:44:36 2020 +0200
34.3 @@ -82,7 +82,7 @@
34.4 val get_somespec' : Celem.spec -> Celem.spec -> Celem.spec
34.5 exception PTREE of string;
34.6
34.7 - val parent_node : ctree -> Pos.pos -> bool * Pos.pos * Rule_Set.rls (* for appl.sml *)
34.8 + val parent_node : ctree -> Pos.pos -> bool * Pos.pos * Rule_Set.T (* for appl.sml *)
34.9 val rootthy : ctree -> theory (* for script.sml *)
34.10 (* ---- made visible ONLY for structure CTaccess : CALC_TREE_ACCESS --------------------------- *)
34.11 val appl_obj : (ppobj -> ppobj) -> ctree -> Pos.pos -> ctree
34.12 @@ -185,7 +185,7 @@
34.13
34.14 type envp =(*9.5.03: unused, delete with field in ctree.PblObj FIXXXME*)
34.15 (int * term list) list * (* assoc-list: args of met*)
34.16 - (int * Rule_Set.rls) list * (* assoc-list: tacs already done ///15.9.00*)
34.17 + (int * Rule_Set.T) list * (* assoc-list: tacs already done ///15.9.00*)
34.18 (int * ets) list * (* assoc-list: tacs etc. already done*)
34.19 (string * pos) list; (* asms * from where*)
34.20
34.21 @@ -386,13 +386,13 @@
34.22 (*\--------------- duplicates in ctree-navi.sml: required also here below ---------------/*)
34.23
34.24 (* find the next parent, which is either a PblObj or a PrfObj *)
34.25 -fun parent_node _ [] = (true, [], Rule_Set.Erls)
34.26 +fun parent_node _ [] = (true, [], Rule_Set.Empty)
34.27 | parent_node pt p =
34.28 let
34.29 - fun par _ [] = (true, [], Rule_Set.Erls)
34.30 + fun par _ [] = (true, [], Rule_Set.Empty)
34.31 | par pt p =
34.32 if is_pblobj (get_obj I pt p)
34.33 - then (true, p, Rule_Set.Erls)
34.34 + then (true, p, Rule_Set.Empty)
34.35 else case get_obj g_tac pt p of
34.36 Tactic.Rewrite_Set rls' => (false, p, assoc_rls rls')
34.37 | Tactic.Rewrite_Set_Inst (_, rls') => (false, p, assoc_rls rls')
35.1 --- a/src/Tools/isac/MathEngBasic/istate-def.sml Sat Apr 04 12:11:32 2020 +0200
35.2 +++ b/src/Tools/isac/MathEngBasic/istate-def.sml Mon Apr 06 11:44:36 2020 +0200
35.3 @@ -20,7 +20,7 @@
35.4 val string_of': T -> string
35.5 val istates2str: T option * T option -> string
35.6
35.7 - val set_eval: Rule_Set.rls -> pstate -> pstate
35.8 + val set_eval: Rule_Set.T -> pstate -> pstate
35.9 val set_act: term -> pstate -> pstate
35.10 val set_env_true: Env.T -> pstate -> pstate
35.11
35.12 @@ -47,7 +47,7 @@
35.13 type pstate =
35.14 {env: Env.T, (* environment for variables in a program *)
35.15 path: TermC.path, (* to the current location in a program *)
35.16 - eval: Rule_Set.rls, (* rule-set for evaluating a Prog_Expr *)
35.17 + eval: Rule_Set.T, (* rule-set for evaluating a Prog_Expr *)
35.18 form_arg: term option,(* argument of a curried function *)
35.19 act_arg: term, (* value for the curried argument *)
35.20 or: asap, (* flag for scanning tactical "Or" !shall be dropped *)
36.1 --- a/src/Tools/isac/MathEngBasic/mstools.sml Sat Apr 04 12:11:32 2020 +0200
36.2 +++ b/src/Tools/isac/MathEngBasic/mstools.sml Mon Apr 06 11:44:36 2020 +0200
36.3 @@ -9,8 +9,8 @@
36.4
36.5 signature SPECIFY_TOOL =
36.6 sig
36.7 - val check_preconds : 'a -> Rule_Set.rls -> term list -> Model.itm list -> (bool * term) list
36.8 - val check_preconds' : Rule_Set.rls -> term list -> Model.itm list -> 'a -> (bool * term) list
36.9 + val check_preconds : 'a -> Rule_Set.T -> term list -> Model.itm list -> (bool * term) list
36.10 + val check_preconds' : Rule_Set.T -> term list -> Model.itm list -> 'a -> (bool * term) list
36.11
36.12 datatype match_ = Match_ of Celem.pblID * (Model.itm list * (bool * term) list) | NoMatch_
36.13 val refined_ : match_ list -> match_ option
37.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml Sat Apr 04 12:11:32 2020 +0200
37.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml Mon Apr 06 11:44:36 2020 +0200
37.3 @@ -26,9 +26,9 @@
37.4 | Check_elementwise' of term * Rule.cterm' * Selem.result
37.5 | Del_Find' of Rule.cterm' | Del_Given' of Rule.cterm' | Del_Relation' of Rule.cterm'
37.6
37.7 - | Derive' of Rule_Set.rls
37.8 - | Detail_Set' of Rule.theory' * bool * Rule_Set.rls * term * Selem.result
37.9 - | Detail_Set_Inst' of Rule.theory' * bool * Rule.subst * Rule_Set.rls * term * Selem.result
37.10 + | Derive' of Rule_Set.T
37.11 + | Detail_Set' of Rule.theory' * bool * Rule_Set.T * term * Selem.result
37.12 + | Detail_Set_Inst' of Rule.theory' * bool * Rule.subst * Rule_Set.T * term * Selem.result
37.13 | End_Detail' of Selem.result
37.14
37.15 | Empty_Tac_
37.16 @@ -40,10 +40,10 @@
37.17 | Refine_Problem' of Celem.pblID * (Model.itm list * (bool * term) list)
37.18 | Refine_Tacitly' of Celem.pblID * Celem.pblID * Rule.domID * Celem.metID * Model.itm list
37.19
37.20 - | Rewrite' of Rule.theory' * Rule_Def.rew_ord' * Rule_Set.rls * bool * Celem.thm'' * term * Selem.result
37.21 - | Rewrite_Inst' of Rule.theory' * Rule_Def.rew_ord' * Rule_Set.rls * bool * Rule.subst * Celem.thm'' * term * Selem.result
37.22 - | Rewrite_Set' of Rule.theory' * bool * Rule_Set.rls * term * Selem.result
37.23 - | Rewrite_Set_Inst' of Rule.theory' * bool * Rule.subst * Rule_Set.rls * term * Selem.result
37.24 + | Rewrite' of Rule.theory' * Rule_Def.rew_ord' * Rule_Set.T * bool * Celem.thm'' * term * Selem.result
37.25 + | Rewrite_Inst' of Rule.theory' * Rule_Def.rew_ord' * Rule_Set.T * bool * Rule.subst * Celem.thm'' * term * Selem.result
37.26 + | Rewrite_Set' of Rule.theory' * bool * Rule_Set.T * term * Selem.result
37.27 + | Rewrite_Set_Inst' of Rule.theory' * bool * Rule.subst * Rule_Set.T * term * Selem.result
37.28
37.29 | Specify_Method' of Celem.metID * Model.ori list * Model.itm list
37.30 | Specify_Problem' of Celem.pblID * (bool * (Model.itm list * (bool * term) list))
37.31 @@ -55,7 +55,7 @@
37.32 (*Istate.T * ? *)
37.33 Proof.context * (* derived from prog. in ??? *)
37.34 term (* ?UNUSED, e.g."Subproblem\n (''Test'',\n ??.\<^const>String.char.Char ''LINEAR'' ''univariate'' ''equation''\n ''test'')" *)
37.35 - | Substitute' of Rule_Def.rew_ord_ * Rule_Set.rls * Selem.subte * term * term
37.36 + | Substitute' of Rule_Def.rew_ord_ * Rule_Set.T * Selem.subte * term * term
37.37 | Tac_ of theory * string * string * string
37.38 | Take' of term
37.39 val string_of: T -> string
37.40 @@ -360,9 +360,9 @@
37.41 Selem.result (* (3) composed from (1) and (2): {x. pred} *)
37.42 | Del_Find' of Rule.cterm' | Del_Given' of Rule.cterm' | Del_Relation' of Rule.cterm'
37.43
37.44 - | Derive' of Rule_Set.rls
37.45 - | Detail_Set' of Rule.theory' * bool * Rule_Set.rls * term * Selem.result
37.46 - | Detail_Set_Inst' of Rule.theory' * bool * Rule.subst * Rule_Set.rls * term * Selem.result
37.47 + | Derive' of Rule_Set.T
37.48 + | Detail_Set' of Rule.theory' * bool * Rule_Set.T * term * Selem.result
37.49 + | Detail_Set_Inst' of Rule.theory' * bool * Rule.subst * Rule_Set.T * term * Selem.result
37.50 | End_Detail' of Selem.result
37.51
37.52 | Empty_Tac_
37.53 @@ -381,10 +381,10 @@
37.54 Rule.domID * (* from new pbt?! filled in specify *)
37.55 Celem.metID * (* from new pbt?! filled in specify *)
37.56 Model.itm list (* drop ! 9.03: remains [] for Model_Problem recognizing its activation *)
37.57 - | Rewrite' of Rule.theory' * Rule_Def.rew_ord' * Rule_Set.rls * bool * Celem.thm'' * term * Selem.result
37.58 - | Rewrite_Inst' of Rule.theory' * Rule_Def.rew_ord' * Rule_Set.rls * bool * Rule.subst * Celem.thm'' * term * Selem.result
37.59 - | Rewrite_Set' of Rule.theory' * bool * Rule_Set.rls * term * Selem.result
37.60 - | Rewrite_Set_Inst' of Rule.theory' * bool * Rule.subst * Rule_Set.rls * term * Selem.result
37.61 + | Rewrite' of Rule.theory' * Rule_Def.rew_ord' * Rule_Set.T * bool * Celem.thm'' * term * Selem.result
37.62 + | Rewrite_Inst' of Rule.theory' * Rule_Def.rew_ord' * Rule_Set.T * bool * Rule.subst * Celem.thm'' * term * Selem.result
37.63 + | Rewrite_Set' of Rule.theory' * bool * Rule_Set.T * term * Selem.result
37.64 + | Rewrite_Set_Inst' of Rule.theory' * bool * Rule.subst * Rule_Set.T * term * Selem.result
37.65
37.66 | Specify_Method' of Celem.metID * Model.ori list * Model.itm list
37.67 | Specify_Problem' of Celem.pblID *
37.68 @@ -401,7 +401,7 @@
37.69 term (* Subproblem (thyID, pbl) OR cascmd *)
37.70 | Substitute' of
37.71 Rule_Def.rew_ord_ * (* for re-calculation *)
37.72 - Rule_Set.rls * (* for re-calculation *)
37.73 + Rule_Set.T * (* for re-calculation *)
37.74 Selem.subte * (* the 'substitution': terms of type bool *)
37.75 term * (* to be substituted into *)
37.76 term (* resulting from the substitution *)
38.1 --- a/src/Tools/isac/ProgLang/Auto_Prog.thy Sat Apr 04 12:11:32 2020 +0200
38.2 +++ b/src/Tools/isac/ProgLang/Auto_Prog.thy Mon Apr 06 11:44:36 2020 +0200
38.3 @@ -33,8 +33,8 @@
38.4 val stacpbls: term -> term list
38.5 val op_of_calc: term -> string
38.6 val get_calcs: theory -> term -> (Rule_Set.prog_calcID * (Rule.calID * Rule.eval_fn)) list
38.7 - val prep_rls: theory -> Rule_Set.rls -> Rule_Set.rls (*ren insert*)
38.8 - val gen: theory -> term -> Rule_Set.rls -> term
38.9 + val prep_rls: theory -> Rule_Set.T -> Rule_Set.T (*ren insert*)
38.10 + val gen: theory -> term -> Rule_Set.T -> term
38.11 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
38.12 (* NONE *)
38.13 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
38.14 @@ -208,20 +208,20 @@
38.15 # filter the operators for Num_Calc out of the script ?WN111014?
38.16 use this function while storing (TODO integrate..) into KEStore_Elems.add_rlss
38.17 *)
38.18 -fun prep_rls _ Rule_Set.Erls = error "prep_rls: not required for Erls"
38.19 - | prep_rls thy (Rule_Set.Rls {id, preconds, rew_ord, erls, srls, rules, errpatts, ...}) =
38.20 +fun prep_rls _ Rule_Set.Empty = error "prep_rls: not required for Erls"
38.21 + | prep_rls thy (Rule_Def.Repeat {id, preconds, rew_ord, erls, srls, rules, errpatts, ...}) =
38.22 let
38.23 val sc = (rules2scr_Rls thy rules)
38.24 in
38.25 - Rule_Set.Rls {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, srls = srls,
38.26 + Rule_Def.Repeat {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, srls = srls,
38.27 calc = get_calcs thy sc,
38.28 rules = rules, errpatts = errpatts,
38.29 scr = Rule.EmptyScr (*Rule.Prog sc AD-HOC REPLACED BY Auto_Prog.gen*)} end
38.30 - | prep_rls thy (Rule_Set.Seq {id, preconds, rew_ord, erls, srls, rules, errpatts, ...}) =
38.31 + | prep_rls thy (Rule_Set.Seqence {id, preconds, rew_ord, erls, srls, rules, errpatts, ...}) =
38.32 let
38.33 val sc = (rules2scr_Seq thy rules)
38.34 in
38.35 - Rule_Set.Seq {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, srls = srls,
38.36 + Rule_Set.Seqence {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, srls = srls,
38.37 calc = get_calcs thy sc,
38.38 rules = rules, errpatts = errpatts,
38.39 scr = Rule.EmptyScr (*Rule.Prog sc AD-HOC REPLACED BY Auto_Prog.gen*)} end
38.40 @@ -235,8 +235,8 @@
38.41 fun gen thy t rls =
38.42 let
38.43 val prog = case rls of
38.44 - Rule_Set.Rls {rules, ...} => rules2scr_Rls thy rules
38.45 - | Rule_Set.Seq {rules, ...} => rules2scr_Seq thy rules
38.46 + Rule_Def.Repeat {rules, ...} => rules2scr_Rls thy rules
38.47 + | Rule_Set.Seqence {rules, ...} => rules2scr_Seq thy rules
38.48 | _ => raise ERROR ("Auto_Prog.gen: not for rule-set \"" ^ Rule_Set.id_rls rls ^ "\"")
38.49 in
38.50 subst_typs prog (type_of t) (TermC.guess_bdv_typ t)
39.1 --- a/src/Tools/isac/ProgLang/ListC.thy Sat Apr 04 12:11:32 2020 +0200
39.2 +++ b/src/Tools/isac/ProgLang/ListC.thy Mon Apr 06 11:44:36 2020 +0200
39.3 @@ -131,8 +131,8 @@
39.4 ML \<open>
39.5 \<close> ML \<open>
39.6 val prog_expr =
39.7 - Rule_Def.Rls {id = "prog_expr", preconds = [], rew_ord = ("dummy_ord", Rule.dummy_ord),
39.8 - erls = Rule_Def.Erls, srls = Rule_Def.Erls, calc = [], errpatts = [],
39.9 + Rule_Def.Repeat {id = "prog_expr", preconds = [], rew_ord = ("dummy_ord", Rule.dummy_ord),
39.10 + erls = Rule_Def.Empty, srls = Rule_Def.Empty, calc = [], errpatts = [],
39.11 rules = [Rule_Def.Thm ("refl", TermC.num_str @{thm refl}), (*'a<>b -> FALSE' by fun eval_equal*)
39.12 Rule_Def.Thm ("o_apply", TermC.num_str @{thm o_apply}),
39.13
39.14 @@ -176,7 +176,7 @@
39.15 Rule_Def.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil}),
39.16 Rule_Def.Thm ("zip_Cons",TermC.num_str @{thm zip_Cons}),
39.17 Rule_Def.Thm ("zip_Nil",TermC.num_str @{thm zip_Nil})],
39.18 - scr = Rule_Def.EmptyScr}: Rule_Set.rls;
39.19 + scr = Rule_Def.EmptyScr}: Rule_Set.T;
39.20 \<close>
39.21 setup \<open>KEStore_Elems.add_rlss [("prog_expr", (Context.theory_name @{theory}, prog_expr))]\<close>
39.22
40.1 --- a/src/Tools/isac/ProgLang/rewrite.sml Sat Apr 04 12:11:32 2020 +0200
40.2 +++ b/src/Tools/isac/ProgLang/rewrite.sml Mon Apr 06 11:44:36 2020 +0200
40.3 @@ -7,28 +7,28 @@
40.4 val assoc_thm': theory -> Celem.thm' -> thm
40.5 val assoc_thm'': theory -> Celem.thmID -> thm
40.6 val calculate_: theory -> string * Rule.eval_fn -> term -> (term * (string * thm)) option
40.7 - val eval__true: theory -> int -> term list -> (term * term) list -> Rule_Set.rls -> term list * bool
40.8 - val eval_prog_expr: theory -> Rule_Set.rls -> term -> term
40.9 - val eval_true_: theory -> Rule_Set.rls -> term -> bool
40.10 - val eval_true: theory -> term list -> Rule_Set.rls -> bool
40.11 + val eval__true: theory -> int -> term list -> (term * term) list -> Rule_Set.T -> term list * bool
40.12 + val eval_prog_expr: theory -> Rule_Set.T -> term -> term
40.13 + val eval_true_: theory -> Rule_Set.T -> term -> bool
40.14 + val eval_true: theory -> term list -> Rule_Set.T -> bool
40.15 val rew_sub: theory -> int -> (term * term) list -> ((term * term) list -> term * term -> bool)
40.16 - -> Rule_Set.rls -> bool -> TermC.path -> term -> term -> term * term list * TermC.path * bool
40.17 - val rewrite_: theory -> ((term * term) list -> term * term -> bool) -> Rule_Set.rls -> bool -> thm ->
40.18 + -> Rule_Set.T -> bool -> TermC.path -> term -> term -> term * term list * TermC.path * bool
40.19 + val rewrite_: theory -> ((term * term) list -> term * term -> bool) -> Rule_Set.T -> bool -> thm ->
40.20 term -> (term * term list) option
40.21 - val rewrite_inst_: theory -> ((term * term) list -> term * term -> bool) -> Rule_Set.rls -> bool
40.22 + val rewrite_inst_: theory -> ((term * term) list -> term * term -> bool) -> Rule_Set.T -> bool
40.23 -> (term * term) list -> thm -> term -> (term * term list) option
40.24 - val rewrite_set_: theory -> bool -> Rule_Set.rls -> term -> (term * term list) option
40.25 - val rewrite_set_inst_: theory -> bool -> (term * term) list -> Rule_Set.rls -> term -> (term * term list) option
40.26 - val rewrite_terms_: theory -> ((term * term) list -> term * term -> bool) -> Rule_Set.rls -> term list
40.27 + val rewrite_set_: theory -> bool -> Rule_Set.T -> term -> (term * term list) option
40.28 + val rewrite_set_inst_: theory -> bool -> (term * term) list -> Rule_Set.T -> term -> (term * term list) option
40.29 + val rewrite_terms_: theory -> ((term * term) list -> term * term -> bool) -> Rule_Set.T -> term list
40.30 -> term -> (term * term list) option
40.31 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
40.32 (* NONE *)
40.33 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
40.34 val rewrite__: theory -> int -> (term * term) list -> ((term * term) list -> term * term -> bool) ->
40.35 - Rule_Set.rls -> bool -> thm -> term -> (term * term list) option
40.36 - val rewrite__set_: theory -> int -> bool -> (term * term) list -> Rule_Set.rls -> term -> (term * term list) option
40.37 - val app_rev: theory -> int -> Rule_Set.rls -> term -> term * term list * bool
40.38 - val app_sub: theory -> int -> Rule_Set.rls -> term -> term * term list * bool
40.39 + Rule_Set.T -> bool -> thm -> term -> (term * term list) option
40.40 + val rewrite__set_: theory -> int -> bool -> (term * term) list -> Rule_Set.T -> term -> (term * term list) option
40.41 + val app_rev: theory -> int -> Rule_Set.T -> term -> term * term list * bool
40.42 + val app_sub: theory -> int -> Rule_Set.T -> term -> term * term list * bool
40.43 val mk_thm: theory -> string -> thm
40.44 val trace1: int -> string -> unit
40.45 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
40.46 @@ -121,7 +121,7 @@
40.47 (*asm false .. thm not applied ^^^; continue until False vvv*)
40.48 else chk (indets @ [t] @ a') asms);
40.49 in chk [] asms end
40.50 -and rewrite__set_ thy _ __ Rule_Set.Erls t = (* rewrite with a rule set *)
40.51 +and rewrite__set_ thy _ __ Rule_Set.Empty t = (* rewrite with a rule set *)
40.52 error ("rewrite__set_ called with 'Erls' for '" ^ Rule.t2str thy t ^ "'")
40.53 | rewrite__set_ thy i _ _ (rrls as Rule_Set.Rrls _) t = (* rewrite with a 'reverse rule set' *)
40.54 let
40.55 @@ -134,8 +134,8 @@
40.56 datatype switch = Appl | Noap;
40.57 fun rew_once _ asm ct Noap [] = (ct, asm) (* ?TODO unify with Prog_Expr.rew_once? *)
40.58 | rew_once ruls asm ct Appl [] =
40.59 - (case rls of Rule_Set.Rls _ => rew_once ruls asm ct Noap ruls
40.60 - | Rule_Set.Seq _ => (ct, asm)
40.61 + (case rls of Rule_Def.Repeat _ => rew_once ruls asm ct Noap ruls
40.62 + | Rule_Set.Seqence _ => (ct, asm)
40.63 | rls => raise ERROR ("rew_once not appl. to \"" ^ Rule_Set.rls2str rls ^ "\""))
40.64 | rew_once ruls asm ct apno (rul :: thms) =
40.65 case rul of
41.1 --- a/src/Tools/isac/Specify/appl.sml Sat Apr 04 12:11:32 2020 +0200
41.2 +++ b/src/Tools/isac/Specify/appl.sml Mon Apr 06 11:44:36 2020 +0200
41.3 @@ -23,9 +23,9 @@
41.4 open Ctree
41.5 open Pos
41.6
41.7 -fun rew_info (Rule_Set.Rls {erls, rew_ord = (rew_ord', _), calc = ca, ...}) =
41.8 +fun rew_info (Rule_Def.Repeat {erls, rew_ord = (rew_ord', _), calc = ca, ...}) =
41.9 (rew_ord', erls, ca)
41.10 - | rew_info (Rule_Set.Seq {erls, rew_ord = (rew_ord', _), calc = ca, ...}) =
41.11 + | rew_info (Rule_Set.Seqence {erls, rew_ord = (rew_ord', _), calc = ca, ...}) =
41.12 (rew_ord', erls, ca)
41.13 | rew_info (Rule_Set.Rrls {erls, rew_ord = (rew_ord', _), calc = ca, ...}) =
41.14 (rew_ord', erls, ca)
42.1 --- a/src/Tools/isac/Specify/ptyps.sml Sat Apr 04 12:11:32 2020 +0200
42.2 +++ b/src/Tools/isac/Specify/ptyps.sml Mon Apr 06 11:44:36 2020 +0200
42.3 @@ -14,7 +14,7 @@
42.4 val prep_ori : Selem.fmz_ -> theory -> field list -> Model.ori list * Proof.context
42.5 val add_id : 'a list -> (int * 'a) list
42.6 val add_field' : theory -> field list -> Model.ori list -> Model.ori list
42.7 - val match_itms_oris : theory -> Model.itm list -> field list * term list * Rule_Set.rls ->
42.8 + val match_itms_oris : theory -> Model.itm list -> field list * term list * Rule_Set.T ->
42.9 Model.ori list -> bool * (Model.itm list * (bool * term) list)
42.10 val refine_ori : Model.ori list -> Celem.pblID -> Celem.pblID option
42.11 val refine_ori' : Model.ori list -> Celem.pblID -> Celem.pblID
42.12 @@ -42,12 +42,12 @@
42.13 val guh2kestoreID : Celem.guh -> string list (* for interface.sml *)
42.14 (* for Knowledge/, if below at left margin *)
42.15 val prep_pbt : theory -> Celem.guh -> string list -> Celem.pblID ->
42.16 - string list * (string * string list) list * Rule_Set.rls * string option * Celem.metID list ->
42.17 + string list * (string * string list) list * Rule_Set.T * string option * Celem.metID list ->
42.18 Celem.pbt * Celem.pblID
42.19 val prep_met : theory -> string -> string list -> Celem.pblID ->
42.20 string list * (string * string list) list *
42.21 - {calc: 'a, crls: Rule_Set.rls, errpats: Rule.errpat list, nrls: Rule_Set.rls, prls: Rule_Set.rls,
42.22 - rew_ord': Rule_Def.rew_ord', rls': Rule_Set.rls, srls: Rule_Set.rls} * thm ->
42.23 + {calc: 'a, crls: Rule_Set.T, errpats: Rule.errpat list, nrls: Rule_Set.T, prls: Rule_Set.T,
42.24 + rew_ord': Rule_Def.rew_ord', rls': Rule_Set.T, srls: Rule_Set.T} * thm ->
42.25 Celem.met * Celem.metID
42.26 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
42.27 val show_ptyps : unit -> unit
43.1 --- a/src/Tools/isac/TODO.thy Sat Apr 04 12:11:32 2020 +0200
43.2 +++ b/src/Tools/isac/TODO.thy Mon Apr 06 11:44:36 2020 +0200
43.3 @@ -36,6 +36,22 @@
43.4 \<close>
43.5 subsection \<open>Postponed from current changeset\<close>
43.6 text \<open>
43.7 + \item see "TODO CLEANUP Thm" in code
43.8 + (* TODO CLEANUP Thm:
43.9 + Thm (string, thm): (a) needs string to identify sym_thmID for handling in front-end;
43.10 + (b) investigate if ""RS sym" attaches a [.]" still occurs: string_of_thmI
43.11 + thmID : type for data from user input + program
43.12 + thmDeriv : type for thy_hierarchy ONLY
43.13 + obsolete types : thm' (SEE "ad thm'"), thm''.
43.14 + revise funs : id_of_thm, thm_of_thm, rep_thm_G', eq_thmI, eq_thmI', thm''_of_thm thm.
43.15 + activate : thmID_of_derivation_name'
43.16 + *)
43.17 + \item xxx
43.18 + \item xxx
43.19 + \item xxx
43.20 + \item xxx
43.21 + \item xxx
43.22 + \item xxx
43.23 \begin{itemize}
43.24 \item LI.do_next (*TODO RM..*) ???
43.25 \item generate.sml: RM datatype edit TOGETHER WITH datatype inout
43.26 @@ -159,7 +175,7 @@
43.27 \item xxx
43.28 \end{itemize}
43.29 \<close>
43.30 -subsection \<open>Postponed -?-> separated task ?\<close>
43.31 +subsection \<open>Postponed --> Major reforms\<close>
43.32 text \<open>
43.33 \begin{itemize}
43.34 \item xxx
43.35 @@ -195,6 +211,19 @@
43.36 \item xxx
43.37 \item finish output of trace_LI with Check_Postcond (useful for SubProblem)
43.38 \item xxx
43.39 + \item replace Rule_Set.empty by Rule_Set.Empty
43.40 + latter is more clear, but replacing ***breaks rewriting over all examples***,
43.41 + e.g. see ERROR: rewrite__set_ called with 'Erls' for 'precond_rootpbl x'
43.42 + in Minisubplb/200-start-method-NEXT_STEP.sml:
43.43 + (*+* )------- in f3cac3053e7b (Rule_Set.empty just renamed, NOT deleted) we had
43.44 + (*+*) prls =
43.45 + (*+*) Rls {calc = [], erls = Erls, errpatts = [], id = "e_rls", preconds = [], rew_ord =
43.46 + (*+*) ("dummy_ord", fn), rules = [], scr = EmptyScr, srls = Erls}:
43.47 + (*+*).. THIS IS Rule_Set.empty, BUT IT DID not CAUSE ANY ERROR !
43.48 + (*+*)------- WITH Rule_Set.empty REMOVED (based on f3cac3053e7b) we had
43.49 + (*+*)val Empty = prls (* <---ERROR: rewrite__set_ called with 'Erls' for 'precond_rootpbl x' *)
43.50 + ( *+*)val ["sqroot-test", "univariate", "equation", "test"] = cpI
43.51 + THAT INDICATES, that much rewriting/evaluating JUST WORKED BY CHANCE?!?
43.52 \item xxx
43.53 \item xxx
43.54 \item xxx
43.55 @@ -205,13 +234,6 @@
43.56 \end{itemize}
43.57 \<close>
43.58
43.59 -section \<open>Separated tasks\<close>
43.60 -text \<open>
43.61 - This section shall be removed, because
43.62 - the distinction \<open>Simple\<close> | \<open>Simple but laborous\<close> | \<open>Questionable\<close>
43.63 - is too distracting when working on \<open>TODOs from current changesets\<close>.
43.64 -\<close>
43.65 -
43.66 section \<open>Major reforms\<close>
43.67 text \<open>
43.68 \<close>
43.69 @@ -386,8 +408,8 @@
43.70 \item xxx
43.71 \item in locate_input_tactic .. ?scan_dn1?; Program.is_eval_expr .use Term.exists_Const
43.72 \item push srls into pstate
43.73 - \item lucas-intrpreter.locate_input_tactic: scan_to_tactic1 srls tac cstate (progr, Rule_Set.e_rls)
43.74 - ^^^^^^^^^^
43.75 + \item lucas-intrpreter.locate_input_tactic: scan_to_tactic1 srls tac cstate (progr, Rule_Set.Empty)
43.76 + ^^^^^^^^^^^^^^^
43.77 \item xxx
43.78 \end{itemize}
43.79 \<close>
44.1 --- a/test/Tools/isac/ADDTESTS/accumulate-val/Thy_1.thy Sat Apr 04 12:11:32 2020 +0200
44.2 +++ b/test/Tools/isac/ADDTESTS/accumulate-val/Thy_1.thy Mon Apr 06 11:44:36 2020 +0200
44.3 @@ -6,9 +6,9 @@
44.4 length (Test_KEStore_Elems.get_rlss @{theory}) = 0;
44.5 (*length (! test_ruleset') = 1 (* if you have clicked somewhere below *)*)
44.6 \<close>
44.7 -setup \<open>Test_KEStore_Elems.add_rlss [("test_list_rls", (Context.theory_name @{theory}, Rule_Set.Erls))]\<close>
44.8 +setup \<open>Test_KEStore_Elems.add_rlss [("test_list_rls", (Context.theory_name @{theory}, Rule_Set.Empty))]\<close>
44.9 ML \<open>
44.10 -(*test_ruleset' := overwritelthy @{theory} (! test_ruleset', [("test_list_rls", Erls)])
44.11 +(*test_ruleset' := overwritelthy @{theory} (! test_ruleset', [("test_list_rls", Rule_Set.Empty)])
44.12 ;
44.13 if length (Test_KEStore_Elems.get_rlss @{theory}) = length (! test_ruleset') then ()
44.14 else error "removal of Unsynchonized.ref: ruleset' <> Test_KEStore_Elems.get_rlss in Thy_1"*)
45.1 --- a/test/Tools/isac/ADDTESTS/accumulate-val/Thy_3.thy Sat Apr 04 12:11:32 2020 +0200
45.2 +++ b/test/Tools/isac/ADDTESTS/accumulate-val/Thy_3.thy Mon Apr 06 11:44:36 2020 +0200
45.3 @@ -16,7 +16,7 @@
45.4 (*if length (Test_KEStore_Elems.get_rlss @{theory}) = length (! test_ruleset')
45.5 then () else error "Test_KEStore_Elems.get_rlss = test_ruleset': changed"*)
45.6 ;
45.7 - val SOME (_, Rule_Set.Rls {rules, ...}) =
45.8 + val SOME (_, Rule_Set.Repeat {rules, ...}) =
45.9 AList.lookup op= (Test_KEStore_Elems.get_rlss @{theory}) "test_list_rls"
45.10 ;
45.11 case rules of
46.1 --- a/test/Tools/isac/ADDTESTS/accumulate-val/Thy_4.thy Sat Apr 04 12:11:32 2020 +0200
46.2 +++ b/test/Tools/isac/ADDTESTS/accumulate-val/Thy_4.thy Mon Apr 06 11:44:36 2020 +0200
46.3 @@ -1,6 +1,6 @@
46.4 theory Thy_4 imports Lucas_Interpreter (*!!!!!*) begin
46.5
46.6 setup \<open>Test_KEStore_Elems.add_rlss
46.7 - [("rls1", ("Thy_4", Rule_Set.Erls)), ("rls2", ("Thy_4", Rule_Set.Erls))]\<close>
46.8 + [("rls1", ("Thy_4", Rule_Set.Empty)), ("rls2", ("Thy_4", Rule_Set.Empty))]\<close>
46.9
46.10 end
47.1 --- a/test/Tools/isac/ADDTESTS/accumulate-val/Thy_5.thy Sat Apr 04 12:11:32 2020 +0200
47.2 +++ b/test/Tools/isac/ADDTESTS/accumulate-val/Thy_5.thy Mon Apr 06 11:44:36 2020 +0200
47.3 @@ -1,5 +1,5 @@
47.4 theory Thy_5 imports Thy_4 begin
47.5
47.6 -setup \<open>Test_KEStore_Elems.add_rlss [("rls", ("Thy_5", Rule_Set.Erls))]\<close>
47.7 +setup \<open>Test_KEStore_Elems.add_rlss [("rls", ("Thy_5", Rule_Set.Empty))]\<close>
47.8
47.9 end
48.1 --- a/test/Tools/isac/ADDTESTS/accumulate-val/Thy_All.thy Sat Apr 04 12:11:32 2020 +0200
48.2 +++ b/test/Tools/isac/ADDTESTS/accumulate-val/Thy_All.thy Mon Apr 06 11:44:36 2020 +0200
48.3 @@ -6,14 +6,14 @@
48.4 |> enumerate_strings
48.5 |> map writeln*)
48.6 (*
48.7 -(rls2, (Thy_4, Erls))--1
48.8 -(rls1, (Thy_4, Erls))--2
48.9 -(rls, (Thy_5, Erls))--3
48.10 -(test_list_rls, (Thy_3, Rls {#calc = 0, #rules = 1, ...))--4
48.11 +(rls2, (Thy_4, Rule_Set.Empty))--1
48.12 +(rls1, (Thy_4, Rule_Set.Empty))--2
48.13 +(rls, (Thy_5, Rule_Set.Empty))--3
48.14 +(test_list_rls, (Thy_3, Rule_Set.Repeat {#calc = 0, #rules = 1, ...))--4
48.15 *)
48.16 ;
48.17 case Test_KEStore_Elems.get_rlss @{theory} of
48.18 - ("rls2", ("Thy_4", Erls)) :: ("rls1", ("Thy_4", Rule_Set.Erls)) :: _ => ()
48.19 + ("rls2", ("Thy_4", Rule_Set.Empty)) :: ("rls1", ("Thy_4", Rule_Set.Empty)) :: _ => ()
48.20 | _ => raise error "Test_KEStore_Elems.get_rlss changed"
48.21 ;
48.22 case Test_KEStore_Elems.get_calcs @{theory} of
49.1 --- a/test/Tools/isac/ADDTESTS/accumulate-val/lucas_interpreter.sml Sat Apr 04 12:11:32 2020 +0200
49.2 +++ b/test/Tools/isac/ADDTESTS/accumulate-val/lucas_interpreter.sml Mon Apr 06 11:44:36 2020 +0200
49.3 @@ -7,8 +7,8 @@
49.4 *)
49.5 signature KESTORE_ELEMS =
49.6 sig
49.7 - val get_rlss: theory -> (Rule_Set.rls' * (Rule.theory' * Rule_Set.rls)) list
49.8 - val add_rlss: (Rule_Set.rls' * (Rule.theory' * Rule_Set.rls)) list -> theory -> theory
49.9 + val get_rlss: theory -> (Rule_Set.rls' * (Rule.theory' * Rule_Set.T)) list
49.10 + val add_rlss: (Rule_Set.rls' * (Rule.theory' * Rule_Set.T)) list -> theory -> theory
49.11 val get_calcs: theory -> (Rule_Set.prog_calcID * (Rule.calID * Rule.eval_fn)) list
49.12 val add_calcs: (Rule_Set.prog_calcID * (Rule.calID * Rule.eval_fn)) list -> theory -> theory
49.13 (*etc*)
49.14 @@ -20,7 +20,7 @@
49.15
49.16 fun rls_eq ((id1, (thyID1, _)), (id2, (thyID2, _))) = id1 = id2 (*andalso thyID1 = thyID2*)
49.17 structure Data = Theory_Data (
49.18 - type T = (Rule_Set.rls' * (Rule.theory' * Rule_Set.rls)) list;
49.19 + type T = (Rule_Set.rls' * (Rule.theory' * Rule_Set.T)) list;
49.20 val empty = [];
49.21 val extend = I;
49.22 val merge = merge rls_eq;
50.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Sat Apr 04 12:11:32 2020 +0200
50.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Mon Apr 06 11:44:36 2020 +0200
50.3 @@ -535,7 +535,7 @@
50.4 \emph{srls}:
50.5 \begin{verbatim}
50.6 val srls =
50.7 - Rls{id = "srls_InverseZTransform",
50.8 + Rule_Set.Repeat{id = "srls_InverseZTransform",
50.9 rules = [Num_Calc("Rational.get_numerator",
50.10 eval_get_numerator "Rational.get_numerator"),
50.11 Num_Calc("Partial_Fractions.factors_from_solution",
50.12 @@ -698,8 +698,8 @@
50.13
50.14 ML \<open>
50.15 val ansatz_rls = prep_rls @{theory} (
50.16 - Rls {id = "ansatz_rls", preconds = [], rew_ord = ("dummy_ord",dummy_ord),
50.17 - erls = e_rls, srls = Erls, calc = [], errpatts = [],
50.18 + Rule_Set.Repeat {id = "ansatz_rls", preconds = [], rew_ord = ("dummy_ord",dummy_ord),
50.19 + erls = e_rls, srls = Rule_Set.Empty, calc = [], errpatts = [],
50.20 rules = [
50.21 Thm ("ansatz_2nd_order",num_str @{thm ansatz_2nd_order}),
50.22 Thm ("equival_trans_2nd_order",num_str @{thm equival_trans_2nd_order})
50.23 @@ -1085,7 +1085,7 @@
50.24
50.25 ML \<open>
50.26 val srls =
50.27 - Rls {id="srls_InverseZTransform",
50.28 + Rule_Set.Repeat {id="srls_InverseZTransform",
50.29 preconds = [],
50.30 rew_ord = ("termlessI",termlessI),
50.31 erls = append_rls "erls_in_srls_InverseZTransform" e_rls
50.32 @@ -1094,7 +1094,7 @@
50.33 (*2nd NTH_CONS pushes n+-1 into asms*)
50.34 Num_Calc("Groups.plus_class.plus", eval_binop "#add_")
50.35 ],
50.36 - srls = Erls, calc = [], errpatts = [],
50.37 + srls = Rule_Set.Empty, calc = [], errpatts = [],
50.38 rules = [
50.39 Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
50.40 Num_Calc("Groups.plus_class.plus", eval_binop "#add_"),
51.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/document/Build_Inverse_Z_Transform.tex Sat Apr 04 12:11:32 2020 +0200
51.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/document/Build_Inverse_Z_Transform.tex Mon Apr 06 11:44:36 2020 +0200
51.3 @@ -1024,7 +1024,7 @@
51.4 \emph{srls}:
51.5 \begin{verbatim}
51.6 val srls =
51.7 - Rls{id = "srls_InverseZTransform",
51.8 + Rule_Set.Repeat{id = "srls_InverseZTransform",
51.9 rules = [Num_Calc("Rational.get_numerator",
51.10 eval_get_numerator "Rational.get_numerator"),
51.11 Num_Calc("Partial_Fractions.factors_from_solution",
51.12 @@ -1354,8 +1354,8 @@
51.13 \isacommand{ML}\isamarkupfalse%
51.14 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
51.15 \ \ val\ ansatz{\isaliteral{5F}{\isacharunderscore}}rls\ {\isaliteral{3D}{\isacharequal}}\ prep{\isaliteral{5F}{\isacharunderscore}}rls{\isaliteral{28}{\isacharparenleft}}\isanewline
51.16 -\ \ \ \ Rls\ {\isaliteral{7B}{\isacharbraceleft}}id\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}ansatz{\isaliteral{5F}{\isacharunderscore}}rls{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ preconds\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ rew{\isaliteral{5F}{\isacharunderscore}}ord\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}dummy{\isaliteral{5F}{\isacharunderscore}}ord{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}dummy{\isaliteral{5F}{\isacharunderscore}}ord{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
51.17 -\ \ \ \ \ \ erls\ {\isaliteral{3D}{\isacharequal}}\ e{\isaliteral{5F}{\isacharunderscore}}rls{\isaliteral{2C}{\isacharcomma}}\ srls\ {\isaliteral{3D}{\isacharequal}}\ Erls{\isaliteral{2C}{\isacharcomma}}\ calc\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
51.18 +\ \ \ \ Rule_Set.Repeat\ {\isaliteral{7B}{\isacharbraceleft}}id\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}ansatz{\isaliteral{5F}{\isacharunderscore}}rls{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ preconds\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ rew{\isaliteral{5F}{\isacharunderscore}}ord\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}dummy{\isaliteral{5F}{\isacharunderscore}}ord{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}dummy{\isaliteral{5F}{\isacharunderscore}}ord{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
51.19 +\ \ \ \ \ \ erls\ {\isaliteral{3D}{\isacharequal}}\ e{\isaliteral{5F}{\isacharunderscore}}rls{\isaliteral{2C}{\isacharcomma}}\ srls\ {\isaliteral{3D}{\isacharequal}}\ Rule_Set.Empty{\isaliteral{2C}{\isacharcomma}}\ calc\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
51.20 \ \ \ \ \ \ rules\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}\isanewline
51.21 \ \ \ \ \ \ \ \ Thm\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}ansatz{\isaliteral{5F}{\isacharunderscore}}{\isadigit{2}}nd{\isaliteral{5F}{\isacharunderscore}}order{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}num{\isaliteral{5F}{\isacharunderscore}}str\ %
51.22 \isaantiq
51.23 @@ -2080,7 +2080,7 @@
51.24 \isacommand{ML}\isamarkupfalse%
51.25 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
51.26 \ \ val\ srls\ {\isaliteral{3D}{\isacharequal}}\ \isanewline
51.27 -\ \ \ \ Rls\ {\isaliteral{7B}{\isacharbraceleft}}id{\isaliteral{3D}{\isacharequal}}{\isaliteral{22}{\isachardoublequote}}srls{\isaliteral{5F}{\isacharunderscore}}InverseZTransform{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ \isanewline
51.28 +\ \ \ \ Rule_Set.Repeat\ {\isaliteral{7B}{\isacharbraceleft}}id{\isaliteral{3D}{\isacharequal}}{\isaliteral{22}{\isachardoublequote}}srls{\isaliteral{5F}{\isacharunderscore}}InverseZTransform{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ \isanewline
51.29 \ \ \ \ \ \ \ \ \ preconds\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
51.30 \ \ \ \ \ \ \ \ \ rew{\isaliteral{5F}{\isacharunderscore}}ord\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}termlessI{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}termlessI{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
51.31 \ \ \ \ \ \ \ \ \ erls\ {\isaliteral{3D}{\isacharequal}}\ append{\isaliteral{5F}{\isacharunderscore}}rls\ {\isaliteral{22}{\isachardoublequote}}erls{\isaliteral{5F}{\isacharunderscore}}in{\isaliteral{5F}{\isacharunderscore}}srls{\isaliteral{5F}{\isacharunderscore}}InverseZTransform{\isaliteral{22}{\isachardoublequote}}\ e{\isaliteral{5F}{\isacharunderscore}}rls\isanewline
51.32 @@ -2089,7 +2089,7 @@
51.33 \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}{\isadigit{2}}nd\ NTH{\isaliteral{5F}{\isacharunderscore}}CONS\ pushes\ n{\isaliteral{2B}{\isacharplus}}{\isaliteral{2D}{\isacharminus}}{\isadigit{1}}\ into\ asms{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
51.34 \ \ \ \ \ \ \ \ \ \ \ \ Num_Calc{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}Groups{\isaliteral{2E}{\isachardot}}plus{\isaliteral{5F}{\isacharunderscore}}class{\isaliteral{2E}{\isachardot}}plus{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ eval{\isaliteral{5F}{\isacharunderscore}}binop\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{23}{\isacharhash}}add{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}\isanewline
51.35 \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ \isanewline
51.36 -\ \ \ \ \ \ \ \ \ srls\ {\isaliteral{3D}{\isacharequal}}\ Erls{\isaliteral{2C}{\isacharcomma}}\ calc\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
51.37 +\ \ \ \ \ \ \ \ \ srls\ {\isaliteral{3D}{\isacharequal}}\ Rule_Set.Empty{\isaliteral{2C}{\isacharcomma}}\ calc\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
51.38 \ \ \ \ \ \ \ \ \ rules\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}\isanewline
51.39 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Thm\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}NTH{\isaliteral{5F}{\isacharunderscore}}CONS{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}num{\isaliteral{5F}{\isacharunderscore}}str\ %
51.40 \isaantiq
52.1 --- a/test/Tools/isac/BridgeLibisabelle/datatypes.sml Sat Apr 04 12:11:32 2020 +0200
52.2 +++ b/test/Tools/isac/BridgeLibisabelle/datatypes.sml Mon Apr 06 11:44:36 2020 +0200
52.3 @@ -46,7 +46,7 @@
52.4 (*AK110725 To be continued...s*)
52.5 *)
52.6
52.7 -val Hrls {thy_rls = (_,Rls {rules = rules as rule::_,...}),...} = thydata;
52.8 +val Hrls {thy_rls = (_,Rule_Set.Repeat {rules = rules as rule::_,...}),...} = thydata;
52.9
52.10 (*for rule2xml...*)
52.11 val (j, thyID, Thm (thmID, thm)) = (2, thyID, rule);
53.1 --- a/test/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Sat Apr 04 12:11:32 2020 +0200
53.2 +++ b/test/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Mon Apr 06 11:44:36 2020 +0200
53.3 @@ -77,11 +77,11 @@
53.4 val (theID:theID, Hrls {guh, coursedesign, mathauthors, thy_rls}) = (theID, thydata);
53.5 rls2xml i thy_rls (*reported Exception- Match in question*);
53.6 ;
53.7 -val (j, (thyID, Seq data)) = (i, thy_rls);
53.8 -rls2xml j (thyID, Seq data) (*reported Exception- Match in question*);
53.9 +val (j, (thyID, Rule_Set.Seqence data)) = (i, thy_rls);
53.10 +rls2xml j (thyID, Rule_Set.Seqence data) (*reported Exception- Match in question*);
53.11 ;
53.12 -val (j, (thyID, Seq {id, preconds, rew_ord=(ord,_), erls, errpatts, srls, calc, rules, scr})) =
53.13 - (j, (thyID, Seq data));
53.14 +val (j, (thyID, Rule_Set.Seqence {id, preconds, rew_ord=(ord,_), erls, errpatts, srls, calc, rules, scr})) =
53.15 + (j, (thyID, Rule_Set.Seqence data));
53.16 ;
53.17 rules2xml (j+2*i) thyID rules (*reports Exception- Match in question*);
53.18 (*TODO: Num_Calc + Cal1 in datatypes.sml *)
53.19 @@ -126,9 +126,9 @@
53.20 (pa, po', (ids@[id]), n);
53.21 "~~~~~ fun thydata2xml, args:"; val (theID, Hrls {guh, coursedesign, mathauthors, thy_rls}) =
53.22 (theID:theID, thydata);
53.23 -"~~~~~ fun rls2xml, args:"; val (j, (thyID, Seq data)) = (i, thy_rls);
53.24 +"~~~~~ fun rls2xml, args:"; val (j, (thyID, Rule_Set.Seqence data)) = (i, thy_rls);
53.25 "~~~~~ fun rls2xm, args:"; val (j, (thyID, seqrls, {id, preconds, rew_ord=(ord,_), erls,
53.26 - srls, calc, errpatts, rules, scr})) = (j, (thyID, "Seq", data));
53.27 + srls, calc, errpatts, rules, scr})) = (j, (thyID, "Rule_Set.Seqence", data));
53.28 "~~~~~ fun rules2xml, args:"; val (j, thyID, (r::rs)) = ((j+2*i), thyID, rules);
53.29 "~~~~~ fun rule2xml, args:"; val (j, thyID, (Rls_ rls)) = (j, thyID, r);
53.30 val rls' = (#id o rep_rls) rls;
53.31 @@ -198,7 +198,7 @@
53.32 *)
53.33 ;
53.34 "~~~~~ fun thms_of_rlss, args:"; val (thy, rlss) = (@{theory Isac_Knowledge}, rlss);
53.35 -val rlss' = (rlss : (rls' * (theory' * rls)) list)
53.36 +val rlss' = (rlss : (rls' * (theory' * Rule_Set.T)) list)
53.37 |> map (thms_of_rls o #2 o #2)
53.38 (* = [[], [Thm ("real_diff_minus", "?a - ?b = ?a + -1 * ?b"),
53.39 Thm ("sym_real_mult_minus1", "- ?z1 = -1 * ?z1")]]*)
53.40 @@ -305,10 +305,10 @@
53.41 mathauthors = ["isac-team"], thm = _}),
53.42 (["IsacKnowledge", "Test_Build_Thydata", "Rulesets", "rls111"],
53.43 Hrls {coursedesign = [], guh = "thy_isac_Test_Build_Thydata-rls-rls111",
53.44 - mathauthors = ["isac-team"], thy_rls = ("Test_Build_Thydata", Rls _)}),
53.45 + mathauthors = ["isac-team"], thy_rls = ("Test_Build_Thydata", Rule_Set.Repeat _)}),
53.46 (["IsacKnowledge", "Test_Build_Thydata", "Rulesets", "rls222"],
53.47 Hrls {coursedesign = [], guh = "thy_isac_Test_Build_Thydata-rls-rls222",
53.48 - mathauthors = ["isac-team"], thy_rls = ("Test_Build_Thydata", Rls _)}),
53.49 + mathauthors = ["isac-team"], thy_rls = ("Test_Build_Thydata", Rule_Set.Repeat _)}),
53.50 (["Isabelle", "HOL", "Theorems", "refl"],
53.51 Hthm {coursedesign = [], fillpats = [], guh = "thy_isab_HOL-thm-refl",
53.52 mathauthors = ["Isabelle team, TU Munich"], thm = _}),
54.1 --- a/test/Tools/isac/BridgeLibisabelle/use-cases.sml Sat Apr 04 12:11:32 2020 +0200
54.2 +++ b/test/Tools/isac/BridgeLibisabelle/use-cases.sml Mon Apr 06 11:44:36 2020 +0200
54.3 @@ -201,7 +201,7 @@
54.4 val Safe_Step (istate, _, tac) =
54.5 (*case*) LI.locate_input_tactic sc (pt, po) (fst is) (snd is) m (*of*);
54.6
54.7 -(*+*)Safe_Step: Istate.T * Proof.context * T -> input_tactic_result;
54.8 +(*+*)Safe_Step: Istate.T * Proof.context * Tactic.T -> input_tactic_result;
54.9 (********************* locate_input_tactic returns cstate * istate * Proof.context *************)
54.10 (*+*)if Istate.string_of istate
54.11 (*+isa*) = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"], [R,L,R,L,R,L,R], e_rls, SOME e_e, \nx = 0 + -1 * (1 + -1 * 2), ORundef, true, true)"
55.1 --- a/test/Tools/isac/CalcElements/calcelems.sml Sat Apr 04 12:11:32 2020 +0200
55.2 +++ b/test/Tools/isac/CalcElements/calcelems.sml Mon Apr 06 11:44:36 2020 +0200
55.3 @@ -110,7 +110,7 @@
55.4 val rlss2b = [("test_list_rls", (Context.theory_name @{theory},
55.5 append_rls "test_list_rls" e_rls [Thm ("False_def", @{thm False_def})]))]
55.6
55.7 -val [(_, (_, Rls {rules, ...}))] = merge_rlss (rlss2, rlss2b)
55.8 +val [(_, (_, Rule_Set.Repeat {rules, ...}))] = merge_rlss (rlss2, rlss2b)
55.9 ;
55.10 case rules of
55.11 [Thm ("subst", _), Thm ("refl", _), Thm ("False_def", _)] => ()
56.1 --- a/test/Tools/isac/CalcElements/kestore.sml Sat Apr 04 12:11:32 2020 +0200
56.2 +++ b/test/Tools/isac/CalcElements/kestore.sml Mon Apr 06 11:44:36 2020 +0200
56.3 @@ -32,7 +32,7 @@
56.4 fun union_overwrite eq l1 l2 = fold (insert eq) l2 (*..swapped..*) l1;
56.5 fun rls_eq ((id1, (thyID1, _)), (id2, (thyID2, _))) = id1 = id2 (*andalso thyID1 = thyID2*)
56.6
56.7 -val data1 = [("test", ("theory-1", Erls)),
56.8 +val data1 = [("test", ("theory-1", Rule_Set.Empty)),
56.9 ("test_rls", ("theory-1",
56.10 append_rls "test_rls" e_rls [Thm ("refl", @{thm refl}), Thm ("subst", @{thm subst})]))]
56.11 val data2 =
56.12 @@ -41,12 +41,12 @@
56.13 val data_3a = union rls_eq data1 data2
56.14 val data_3b = union_overwrite rls_eq data1 data2
56.15
56.16 -val SOME (_, Rls {rules, ...}) = AList.lookup op = data_3a "test_rls";
56.17 +val SOME (_, Rule_Set.Repeat {rules, ...}) = AList.lookup op = data_3a "test_rls";
56.18 case rules of
56.19 [Thm ("not_def", _)] => ()
56.20 | _ => error "union rls_eq changed: 1st argument is NOT overwritten anymore"
56.21 ;
56.22 -val SOME (_, Rls {rules, ...}) = AList.lookup op = data_3b "test_rls";
56.23 +val SOME (_, Rule_Set.Repeat {rules, ...}) = AList.lookup op = data_3b "test_rls";
56.24 case rules of
56.25 [Thm ("refl", _), Thm ("subst", _)] => ()
56.26 | _ => error "union_overwrite rls_eq changed: 2nd argument is NOT overwritten anymore"
57.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml Sat Apr 04 12:11:32 2020 +0200
57.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml Mon Apr 06 11:44:36 2020 +0200
57.3 @@ -371,25 +371,25 @@
57.4 val thy' = get_obj g_domID pt (par_pblobj pt p);
57.5 val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt;
57.6
57.7 -val Next_Step (_, _, Rewrite_Set' ("Poly", _, Seq {id = "norm_Poly", ...}, _, _)) =
57.8 +val Next_Step (_, _, Rewrite_Set' ("Poly", _, Rule_Set.Seqence {id = "norm_Poly", ...}, _, _)) =
57.9 LI.find_next_step sc (pt, pos) ist ctxt (*of*);
57.10 "~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as(pt, (p, _))), (Pstate ist), ctxt)
57.11 = (sc, (pt, pos), ist, ctxt);
57.12
57.13 -val Accept_Tac (Rewrite_Set' ("Poly", _, Seq {id = "norm_Poly", ...}, _, _), _, _) =
57.14 +val Accept_Tac (Rewrite_Set' ("Poly", _, Rule_Set.Seqence {id = "norm_Poly", ...}, _, _), _, _) =
57.15 (*case*) scan_to_tactic (prog, (ptp, ctxt)) (Pstate ist) (*of*);
57.16 "~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Pstate (ist as {path, ...})))
57.17 = ((prog, (ptp, ctxt)), (Pstate ist));
57.18 (*if*) path = [] (*then*);
57.19
57.20 -val Accept_Tac (Rewrite_Set' ("Poly", _, Seq {id = "norm_Poly", ...}, _, _), _, _) =
57.21 +val Accept_Tac (Rewrite_Set' ("Poly", _, Rule_Set.Seqence {id = "norm_Poly", ...}, _, _), _, _) =
57.22 scan_dn cc (trans_scan_dn ist) (Program.body_of prog);
57.23 "~~~~~ fun scan_dn , args:"; val ((cc as (_, ctxt)), (ist as {eval, ...}), t)
57.24 = (cc, (trans_scan_dn ist), (Program.body_of prog));
57.25 (*if*) Tactical.contained_in t (*else*);
57.26 val (Program.Tac prog_tac, form_arg) = (*case*) LItool.check_leaf "next " ctxt eval (get_subst ist) t (*of*);
57.27
57.28 -val Accept_Tac (Rewrite_Set' ("Poly", _, Seq {id = "norm_Poly", ...}, _, _), _, _) =
57.29 +val Accept_Tac (Rewrite_Set' ("Poly", _, Rule_Set.Seqence {id = "norm_Poly", ...}, _, _), _, _) =
57.30 check_tac cc ist (prog_tac, form_arg) (*return from xxx*);
57.31 "~~~~~ from fun scan_dn\<longrightarrow>fun scan_to_tactic\<longrightarrow>fun find_next_step, return:"; val (Accept_Tac (tac, ist, ctxt))
57.32 = (check_tac cc ist (prog_tac, form_arg));
58.1 --- a/test/Tools/isac/Knowledge/algein.sml Sat Apr 04 12:11:32 2020 +0200
58.2 +++ b/test/Tools/isac/Knowledge/algein.sml Mon Apr 06 11:44:36 2020 +0200
58.3 @@ -102,7 +102,7 @@
58.4 "----------- Widerspruch 3 = 777 ---------------------------------";
58.5 val thy = @{theory "Isac_Knowledge"};
58.6 val rew_ord = dummy_ord;
58.7 -val erls = Erls;
58.8 +val erls = Rule_Set.Empty;
58.9 val thm = assoc_thm' thy ("sym_mult_zero_right","");
58.10 val t = str2term "0 = (0::real)";
58.11 val SOME (t',_) = rewrite_ thy rew_ord erls false thm t;
59.1 --- a/test/Tools/isac/Knowledge/biegelinie-1.sml Sat Apr 04 12:11:32 2020 +0200
59.2 +++ b/test/Tools/isac/Knowledge/biegelinie-1.sml Mon Apr 06 11:44:36 2020 +0200
59.3 @@ -51,7 +51,7 @@
59.4 "----------- simplify_leaf for this script -----------------------";
59.5 "----------- simplify_leaf for this script -----------------------";
59.6 "----------- simplify_leaf for this script -----------------------";
59.7 -val srls = Rls {id="srls_IntegrierenUnd..",
59.8 +val srls = Rule_Set.Repeat {id="srls_IntegrierenUnd..",
59.9 preconds = [],
59.10 rew_ord = ("termlessI",termlessI),
59.11 erls = append_rls "erls_in_srls_IntegrierenUnd.." e_rls
59.12 @@ -60,7 +60,7 @@
59.13 (*2nd NTH_CONS pushes n+-1 into asms*)
59.14 Num_Calc("Groups.plus_class.plus", eval_binop "#add_")
59.15 ],
59.16 - srls = Erls, calc = [], errpatts = [],
59.17 + srls = Rule_Set.Empty, calc = [], errpatts = [],
59.18 rules = [Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
59.19 Num_Calc("Groups.plus_class.plus", eval_binop "#add_"),
59.20 Thm ("NTH_NIL",num_str @{thm NTH_NIL}),
60.1 --- a/test/Tools/isac/Knowledge/eqsystem.sml Sat Apr 04 12:11:32 2020 +0200
60.2 +++ b/test/Tools/isac/Knowledge/eqsystem.sml Mon Apr 06 11:44:36 2020 +0200
60.3 @@ -210,7 +210,7 @@
60.4 val e2__ = str2term "L * c + c_2 = q_0 * L ^^^ 2 / 2";
60.5 val bdvs = [(str2term"bdv_1",str2term"c"),
60.6 (str2term"bdv_2",str2term"c_2")];
60.7 -val SOME (e2__,_) = rewrite_terms_ thy dummy_ord Erls [e1__] e2__;
60.8 +val SOME (e2__,_) = rewrite_terms_ thy dummy_ord Rule_Set.Empty [e1__] e2__;
60.9 if term2str e2__ = "L * c + 77 = q_0 * L ^^^ 2 / 2" then ()
60.10 else error "eqsystem.sml top_down_substitution,2x2] subst";
60.11
61.1 --- a/test/Tools/isac/Knowledge/integrate.sml Sat Apr 04 12:11:32 2020 +0200
61.2 +++ b/test/Tools/isac/Knowledge/integrate.sml Mon Apr 06 11:44:36 2020 +0200
61.3 @@ -30,11 +30,11 @@
61.4 fun term2s t = term_to_string' ctxt t;
61.5
61.6 val conditions_in_integration_rules =
61.7 - Rls {id="conditions_in_integration_rules",
61.8 + Rule_Set.Repeat {id="conditions_in_integration_rules",
61.9 preconds = [],
61.10 rew_ord = ("termlessI",termlessI),
61.11 - erls = Erls,
61.12 - srls = Erls, calc = [], errpatts = [],
61.13 + erls = Rule_Set.Empty,
61.14 + srls = Rule_Set.Empty, calc = [], errpatts = [],
61.15 rules = [(*for rewriting conditions in Thm's*)
61.16 Num_Calc ("Prog_Expr.occurs'_in",
61.17 eval_occurs_in "#occurs_in_"),
61.18 @@ -141,11 +141,11 @@
61.19 else error "integrate.sml: eval_is_f_x --> false";
61.20
61.21 val conditions_in_integration =
61.22 -Rls {id="conditions_in_integration",
61.23 +Rule_Set.Repeat {id="conditions_in_integration",
61.24 preconds = [],
61.25 rew_ord = ("termlessI",termlessI),
61.26 - erls = Erls,
61.27 - srls = Erls, calc = [], errpatts = [],
61.28 + erls = Rule_Set.Empty,
61.29 + srls = Rule_Set.Empty, calc = [], errpatts = [],
61.30 rules = [Num_Calc ("Prog_Expr.matches",eval_matches ""),
61.31 Num_Calc ("Integrate.is'_f'_x",
61.32 eval_is_f_x "is_f_x_"),
62.1 --- a/test/Tools/isac/Knowledge/partial_fractions.sml Sat Apr 04 12:11:32 2020 +0200
62.2 +++ b/test/Tools/isac/Knowledge/partial_fractions.sml Mon Apr 06 11:44:36 2020 +0200
62.3 @@ -289,9 +289,9 @@
62.4 [Num_Calc ("HOL.eq",eval_equal "#equal_")];
62.5
62.6 val multiply_ansatz = prep_rls @{theory} (
62.7 - Rls {id = "multiply_ansatz", preconds = [], rew_ord = ("dummy_ord",dummy_ord),
62.8 + Rule_Set.Repeat {id = "multiply_ansatz", preconds = [], rew_ord = ("dummy_ord",dummy_ord),
62.9 erls = xxx,
62.10 - srls = Erls, calc = [], errpatts = [],
62.11 + srls = Rule_Set.Empty, calc = [], errpatts = [],
62.12 rules =
62.13 [Thm ("multiply_2nd_order",num_str @{thm multiply_2nd_order})
62.14 ],
63.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml Sat Apr 04 12:11:32 2020 +0200
63.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml Mon Apr 06 11:44:36 2020 +0200
63.3 @@ -965,7 +965,7 @@
63.4 term2str t = "-8 + (2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2";
63.5
63.6 val thm = num_str @{thm square_explicit1};
63.7 -val SOME (t,asm) = rewrite_ thy dummy_ord Erls true thm t;
63.8 +val SOME (t,asm) = rewrite_ thy dummy_ord Rule_Set.Empty true thm t;
63.9 term2str t = "(2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2 - -8";
63.10
63.11 val thm = num_str @{thm root_plus_minus};
63.12 @@ -975,17 +975,17 @@
63.13
63.14 (*the thm bdv_explicit2* here required to be constrained to ::real*)
63.15 val thm = num_str @{thm bdv_explicit2};
63.16 -val SOME (t,asm) = rewrite_inst_ thy dummy_ord Erls true inst thm t;
63.17 +val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t;
63.18 term2str t = "2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |"^
63.19 "\n-1 * x = - (2 / 2) + -1 * sqrt ((2 / 2) ^^^ 2 - -8)";
63.20
63.21 val thm = num_str @{thm bdv_explicit3};
63.22 -val SOME (t,asm) = rewrite_inst_ thy dummy_ord Erls true inst thm t;
63.23 +val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t;
63.24 term2str t = "2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |"^
63.25 "\nx = -1 * (- (2 / 2) + -1 * sqrt ((2 / 2) ^^^ 2 - -8))";
63.26
63.27 val thm = num_str @{thm bdv_explicit2};
63.28 -val SOME (t,asm) = rewrite_inst_ thy dummy_ord Erls true inst thm t;
63.29 +val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t;
63.30 term2str t = "-1 * x = - (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8) |"^
63.31 "\nx = -1 * (- (2 / 2) + -1 * sqrt ((2 / 2) ^^^ 2 - -8))";
63.32
64.1 --- a/test/Tools/isac/Knowledge/rlang.sml Sat Apr 04 12:11:32 2020 +0200
64.2 +++ b/test/Tools/isac/Knowledge/rlang.sml Mon Apr 06 11:44:36 2020 +0200
64.3 @@ -895,8 +895,8 @@
64.4 \0 <= 1 / 9,\
64.5 \0 <= (25 * (1 / 9) + -1 * (16 + 49 * (1 / 9))) * -56,\
64.6 \0 <= 1 / 9]"
64.7 -(*WN050916 before correction 'rewrite__set_ called with 'Erls' for ..'
64.8 - thus: maybe the rls for the asms is Erls ??:
64.9 +(*WN050916 before correction 'rewrite__set_ called with 'Rule_Set.Empty' for ..'
64.10 + thus: maybe the rls for the asms is Rule_Set.Empty ??:
64.11 [(str2term"0 <= (25 * (1 / 9) + -1 * (16 + 49 * (1 / 9))) * -56", []),
64.12 (str2term"9 ~= 0", []),
64.13 (str2term"0 <= (-5 + 7 * sqrt (1 / 9) + 1) * 5", []),
65.1 --- a/test/Tools/isac/Knowledge/rooteq.sml Sat Apr 04 12:11:32 2020 +0200
65.2 +++ b/test/Tools/isac/Knowledge/rooteq.sml Mon Apr 06 11:44:36 2020 +0200
65.3 @@ -135,7 +135,7 @@
65.4 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1 / 25]")) => ()
65.5 | _ => error "rooteq.sml: diff.behav. [x = 1 / 25]";
65.6 if terms2str (*WN1104changed*) (Ctree.get_assumptions pt p) = "[0 <= 1 / 25]"
65.7 -(*WN050916 before correction 'rewrite__set_ called with 'Erls' for ..:
65.8 +(*WN050916 before correction 'rewrite__set_ called with 'Rule_Set.Empty' for ..:
65.9 [(str2term"25 ~= 0",[])] *)
65.10 then writeln "should be True\n\
65.11 \should be True\n\
66.1 --- a/test/Tools/isac/MathEngBasic/tactic.sml Sat Apr 04 12:11:32 2020 +0200
66.2 +++ b/test/Tools/isac/MathEngBasic/tactic.sml Mon Apr 06 11:44:36 2020 +0200
66.3 @@ -18,7 +18,7 @@
66.4 val thm'' = ("real_mult_div_cancel2", @{thm real_mult_div_cancel2});
66.5 val (f, res) = (@{term "a * x / (b * x) :: real"}, (@{term "a / b :: real"}, [@{term "k \<noteq> (0 :: real)"}]: term list))
66.6 ;
66.7 -Rewrite': theory' * Rule_Def.rew_ord' * rls * bool * thm'' * term * result -> T;
66.8 +Rewrite': theory' * Rule_Def.rew_ord' * Rule_Set.T * bool * thm'' * term * result -> Tactic.T;
66.9 val tac = Rewrite' ("Diff", "dummy_ord", e_rls, true, thm'', f, res)
66.10 ;
66.11 if (Tactic.result tac |> term2str) = "a / b" then () else error "creates_assms CHANGED";
67.1 --- a/test/Tools/isac/MathEngine/mathengine-stateless.sml Sat Apr 04 12:11:32 2020 +0200
67.2 +++ b/test/Tools/isac/MathEngine/mathengine-stateless.sml Mon Apr 06 11:44:36 2020 +0200
67.3 @@ -200,7 +200,7 @@
67.4 val tac = get_obj g_tac pt p
67.5 val rls = (assoc_rls o rls_of) tac
67.6 val ctxt = get_ctxt pt pos
67.7 -(*rls = Rls {calc = [], erls = ...*)
67.8 +(*rls = Rule_Set.Repeat {calc = [], erls = ...*)
67.9 val is = init_istate tac t
67.10 (*TODO.WN060602 Pstate (["(t_, Problem (Isac,[equation,univar]))"]
67.11 is wrong for simpl, but working ?!? *)
68.1 --- a/test/Tools/isac/MathEngine/solve.sml Sat Apr 04 12:11:32 2020 +0200
68.2 +++ b/test/Tools/isac/MathEngine/solve.sml Mon Apr 06 11:44:36 2020 +0200
68.3 @@ -6,7 +6,7 @@
68.4 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
68.5 uses from Rational.ML: Rrls cancel_p, Rrls cancel
68.6 which in turn
68.7 -uses from Poly.ML: Rls make_polynomial, Rls expand_binom
68.8 +uses from Poly.ML: Rule_Set.Repeat make_polynomial, Rule_Set.Repeat expand_binom
68.9 *)
68.10
68.11 "-----------------------------------------------------------------";
69.1 --- a/test/Tools/isac/Minisubpbl/200-start-method-NEXT_STEP.sml Sat Apr 04 12:11:32 2020 +0200
69.2 +++ b/test/Tools/isac/Minisubpbl/200-start-method-NEXT_STEP.sml Mon Apr 06 11:44:36 2020 +0200
69.3 @@ -12,8 +12,51 @@
69.4 ["Test","squ-equ-test-subpbl1"]);
69.5 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
69.6 (*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Model_Problem*)
69.7 -(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Specify_Theory*)
69.8 -(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Specify_Problem ["sqroot-test", "univariate", "equation", "test"*)
69.9 +
69.10 +(*rewrite__set_ called with 'Rule_Set.Empty' for 'precond_rootpbl x'*)
69.11 +(*[], Pbl*)val (_, ([(tac''''', _, _)], _, (pt''''', p'''''))) = Step.do_next p ((pt, e_pos'), []);(*Specify_Theory*)
69.12 +
69.13 +(*/--------- step into Specify_Theory --------------------------------------------------------\*)
69.14 +"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) = (p, ((pt, e_pos'), []));
69.15 + val pIopt = Ctree.get_pblID (pt, ip);
69.16 + (*if*) ip = ([], Pos.Res) (*else*);
69.17 + val _ = (*case*) tacis (*of*);
69.18 + val SOME _ = (*case*) pIopt (*of*);
69.19 +
69.20 +(*rewrite__set_ called with 'Rule_Set.Empty' for 'precond_rootpbl x'*)
69.21 + switch_specify_solve p_ (pt, ip);
69.22 +"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
69.23 + (*if*) member op = [Pos.Pbl, Pos.Met] state_pos (*then*);
69.24 +
69.25 +(*rewrite__set_ called with 'Rule_Set.Empty' for 'precond_rootpbl x'*)
69.26 + specify_do_next (pt, input_pos);
69.27 +"~~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);
69.28 +
69.29 +(*rewrite__set_ called with 'Rule_Set.Empty' for 'precond_rootpbl x'*)
69.30 + val (_, (_, _)) =
69.31 +SpecifyNEW.find_next_step ptp;
69.32 +"~~~~~ fun find_next_step , args:"; val (pt, (p, p_)) = ptp;
69.33 + val (pblobj, met, origin, oris, dI', pI', mI', pbl, dI, pI, mI) =
69.34 + case Ctree.get_obj I pt p of
69.35 + pblobj as (Ctree.PblObj {meth, origin = origin as (oris, (dI', pI', mI'), _),
69.36 + probl, spec = (dI, pI, mI), ...}) => (pblobj, meth, origin, oris, dI', pI', mI', probl, dI, pI, mI)
69.37 + | Ctree.PrfObj _ => error "nxt_specify_: not on PrfObj";
69.38 + (*if*) Ctree.just_created_ pblobj (*by Subproblem*) andalso origin <> Ctree.e_origin (*else*);
69.39 + val cpI = if pI = Celem.e_pblID then pI' else pI;
69.40 + val cmI = if mI = Celem.e_metID then mI' else mI;
69.41 + val {ppc = pbt, prls, where_, ...} = Specify.get_pbt cpI;
69.42 +
69.43 +(*+* )------- in f3cac3053e7b (Rule_Set.empty just renamed, NOT deleted) we had
69.44 +(*+*) prls =
69.45 +(*+*) Rule_Set.Repeat {calc = [], erls = Rule_Set.Empty, errpatts = [], id = "e_rls", preconds = [], rew_ord =
69.46 +(*+*) ("dummy_ord", fn), rules = [], scr = EmptyScr, srls = Rule_Set.Empty}:
69.47 +(*+*).. THIS IS Rule_Set.empty, BUT IT DID not CAUSE ANY ERROR !
69.48 +(*+*)------- WITH Rule_Set.empty REMOVED (based on f3cac3053e7b) we had
69.49 +(*+*)val Empty = prls (* <---ERROR: rewrite__set_ called with 'Rule_Set.Empty' for 'precond_rootpbl x' *)
69.50 +( *+*)val ["sqroot-test", "univariate", "equation", "test"] = cpI
69.51 +(*\--------- step into Specify_Theory --------------------------------------------------------/*)
69.52 +
69.53 +(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p''''' ((pt''''', e_pos'), []);(*Specify_Problem ["sqroot-test", "univariate", "equation", "test"*)
69.54 (*[], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Specify_Method ["Test", "squ-equ-test-subpbl1"]*)
69.55 (*[1], Frm*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Apply_Method ["Test", "squ-equ-test-subpbl1"]*)
69.56 (*[1], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Rewrite_Set "norm_equation"*)
69.57 @@ -25,3 +68,10 @@
69.58 (*[3], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Specify_Method ["Test", "solve_linear"]*)
69.59 (*[3, 1], Frm*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Apply_Method ["Test", "solve_linear"]*)
69.60 (*[3, 1], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv")*)
69.61 +
69.62 +val Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv") = tac;
69.63 +
69.64 +if p = ([3, 1], Res) andalso (get_obj g_res pt (fst p) |> term2str) = "x = 0 + -1 * -1"
69.65 +then case tac of Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv") => ()
69.66 + | _ => error "Minisubplb/200-start-method-NEXT_STEP.sml CHANGED 1"
69.67 +else error "Minisubplb/200-start-method-NEXT_STEP.sml CHANGED 2"
70.1 --- a/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Sat Apr 04 12:11:32 2020 +0200
70.2 +++ b/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Mon Apr 06 11:44:36 2020 +0200
70.3 @@ -45,7 +45,7 @@
70.4 val thy' = get_obj g_domID pt (par_pblobj pt p);
70.5 val (is, sc) = LItool.resume_prog thy' (p,p_) pt;
70.6
70.7 - val Safe_Step (_, _, Rewrite_Set' (_, _, Rls {id = "norm_equation", ...}, _, _)) = (*case*)
70.8 + val Safe_Step (_, _, Rewrite_Set' (_, _, Rule_Set.Repeat {id = "norm_equation", ...}, _, _)) = (*case*)
70.9 locate_input_tactic sc (pt, po) (fst is) (snd is) m (*of*);
70.10 "~~~~~ fun locate_input_tactic , args:"; val (Rule.Prog progr, cstate, istate, ctxt, tac)
70.11 = (sc, (pt, po), (fst is), (snd is), m);
70.12 @@ -60,7 +60,7 @@
70.13 "~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const ("HOL.Let", _) $ e $ (Abs (id, T, b))))
70.14 = (cctt, (ist |> set_path [R] |> set_or ORundef), (Program.body_of prog));
70.15
70.16 -val Accept_Tac1 (_, _, Rewrite_Set' (_, _, Rls {id = "norm_equation", ...}, _, _)) = (*case*)
70.17 +val Accept_Tac1 (_, _, Rewrite_Set' (_, _, Rule_Set.Repeat {id = "norm_equation", ...}, _, _)) = (*case*)
70.18 scan_dn1 xxx (ist |> path_down [L, R]) e (*of*);
70.19 "~~~~~ fun scan_dn1, args:"; val ((xxx as (cstate, _, _)), ist, (Const ("Tactical.Chain"(*1*),_) $e1 $ e2 $ a)) =
70.20 (xxx, (ist |> path_down [L, R]), e);
71.1 --- a/test/Tools/isac/Minisubpbl/700-interSteps.sml Sat Apr 04 12:11:32 2020 +0200
71.2 +++ b/test/Tools/isac/Minisubpbl/700-interSteps.sml Mon Apr 06 11:44:36 2020 +0200
71.3 @@ -89,7 +89,7 @@
71.4 val _ = (*case*) rls (*of*);
71.5 val is = Generate.init_istate tac t
71.6
71.7 -(*+*)val Rls {scr = EmptyProg, ...} = rls; (*this prog is replaced by Auto_Prog.gen on the fly*)
71.8 +(*+*)val Rule_Set.Repeat {scr = EmptyProg, ...} = rls; (*this prog is replaced by Auto_Prog.gen on the fly*)
71.9
71.10 val tac_ = Tactic.Apply_Method' (Celem.e_metID(*WN0402: see generate1 !?!*), SOME t, is, ctxt)
71.11 val pos' = ((lev_on o lev_dn) p, Frm)
71.12 @@ -117,7 +117,7 @@
71.13 (*+*)val (keep_c', keep_ptp') = (c', ptp');
71.14 "~~~~~ and Step_Solve.do_next , args:"; val () = ();
71.15 (*+*)(*STOPPED HERE:
71.16 - NOTE: prog.xxx found by LItool.resume_prog from Rls {scr = Prog xxx, ...}*)
71.17 + NOTE: prog.xxx found by LItool.resume_prog from Rule_Set.Repeat {scr = Prog xxx, ...}*)
71.18
71.19 (*+*)val (c', ptp') = (keep_c', keep_ptp');
71.20
72.1 --- a/test/Tools/isac/ProgLang/auto_prog.sml Sat Apr 04 12:11:32 2020 +0200
72.2 +++ b/test/Tools/isac/ProgLang/auto_prog.sml Mon Apr 06 11:44:36 2020 +0200
72.3 @@ -32,8 +32,8 @@
72.4 Auto_Prog.gen thy' t rls;
72.5 "~~~~~ fun generate , args:"; val (thy, t, rls) = (thy', t, rls);
72.6 val prog = case rls of
72.7 - Rule_Set.Rls {rules, ...} => rules2scr_Rls thy rules
72.8 - | Rule_Set.Seq {rules, ...} => rules2scr_Seq thy rules
72.9 + Rule_Set.Repeat {rules, ...} => rules2scr_Rls thy rules
72.10 + | Rule_Set.Seqence {rules, ...} => rules2scr_Seq thy rules
72.11 val auto_script = subst_typs prog (type_of t) (TermC.guess_bdv_typ t) (*return from generate*);
72.12
72.13 if term2str auto_script =
73.1 --- a/test/Tools/isac/ProgLang/rewrite.sml Sat Apr 04 12:11:32 2020 +0200
73.2 +++ b/test/Tools/isac/ProgLang/rewrite.sml Mon Apr 06 11:44:36 2020 +0200
73.3 @@ -198,7 +198,7 @@
73.4 "----------- step through 'fun rewrite_terms_' ---------";
73.5 "----- step 0: args for rewrite_terms_, local fun";
73.6 val (thy, ord, erls, equs, t) =
73.7 - (@{theory "Biegelinie"}, dummy_ord, Erls, [str2term "x = 0"],
73.8 + (@{theory "Biegelinie"}, dummy_ord, Rule_Set.Empty, [str2term "x = 0"],
73.9 str2term "M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2");
73.10 "----- step 1: args for rew_";
73.11 val ((t', asm'), (rules as r::rs), t) = ((e_term, []), equs, t);
73.12 @@ -207,21 +207,21 @@
73.13 "----- step 3: step through rew_sub -- inefficient: goes into subterms";
73.14
73.15
73.16 -val SOME (t', _) = rewrite_terms_ thy dummy_ord Erls equs t;
73.17 +val SOME (t', _) = rewrite_terms_ thy dummy_ord Rule_Set.Empty equs t;
73.18 writeln "----------- rewrite_terms_ 1---------------------------";
73.19 if term2str t' = "M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
73.20 else error "rewrite.sml rewrite_terms_ [x = 0]";
73.21
73.22 val equs = [str2term "M_b 0 = 0"];
73.23 val t = str2term "M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2";
73.24 -val SOME (t', _) = rewrite_terms_ thy dummy_ord Erls equs t;
73.25 +val SOME (t', _) = rewrite_terms_ thy dummy_ord Rule_Set.Empty equs t;
73.26 writeln "----------- rewrite_terms_ 2---------------------------";
73.27 if term2str t' = "0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
73.28 else error "rewrite.sml rewrite_terms_ [M_b 0 = 0]";
73.29
73.30 val equs = [str2term "x = 0", str2term"M_b 0 = 0"];
73.31 val t = str2term "M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2";
73.32 -val SOME (t', _) = rewrite_terms_ thy dummy_ord Erls equs t;
73.33 +val SOME (t', _) = rewrite_terms_ thy dummy_ord Rule_Set.Empty equs t;
73.34 writeln "----------- rewrite_terms_ 3---------------------------";
73.35 if term2str t' = "0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
73.36 else error "rewrite.sml rewrite_terms_ [x = 0, M_b 0 = 0]";
73.37 @@ -530,8 +530,8 @@
73.38 datatype switch = Appl | Noap;
73.39 fun rew_once _ asm ct Noap [] = (ct, asm) (* ?TODO unify with Prog_Expr.rew_once? *)
73.40 | rew_once ruls asm ct Appl [] =
73.41 - (case rls of Rule_Set.Rls _ => rew_once ruls asm ct Noap ruls
73.42 - | Rule_Set.Seq _ => (ct, asm)
73.43 + (case rls of Rule_Set.Repeat _ => rew_once ruls asm ct Noap ruls
73.44 + | Rule_Set.Seqence _ => (ct, asm)
73.45 | rls => raise ERROR ("rew_once not appl. to \"" ^ Rule.rls2str rls ^ "\""))
73.46 | rew_once ruls asm ct apno (rul :: thms) =
73.47 case rul of
73.48 @@ -641,7 +641,7 @@
73.49 chk [] asms; (*return from eval__true*);
73.50 "~~~~~ fun chk , args:"; val (indets, (a :: asms)) = ([], asms);
73.51
73.52 -(*+*)val Rls {id = "rateq_erls", rules, ...} = rls;
73.53 +(*+*)val Rule_Set.Repeat {id = "rateq_erls", rules, ...} = rls;
73.54 (*+*)(*val rules =
73.55 (*+*) [Num_Calc ("Rings.divide_class.divide", fn),
73.56 (*+*) Thm ("minus_divide_left", "- ?a1 / ?b1 = - (?a1 / ?b1)"),
74.1 --- a/test/Tools/isac/Test_Isac_Short.thy Sat Apr 04 12:11:32 2020 +0200
74.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Mon Apr 06 11:44:36 2020 +0200
74.3 @@ -143,6 +143,14 @@
74.4 ML \<open>
74.5 \<close> ML \<open>
74.6 \<close> ML \<open>
74.7 +\<close> ML \<open>
74.8 +\<close> ML \<open>
74.9 +\<close> ML \<open>
74.10 +\<close> ML \<open>
74.11 +\<close> ML \<open>
74.12 +\<close> ML \<open>
74.13 +\<close> ML \<open>
74.14 +\<close> ML \<open>
74.15 \<close>
74.16
74.17 ML \<open>