1.1 --- a/TODO.md Wed Aug 03 18:17:27 2022 +0200
1.2 +++ b/TODO.md Thu Aug 04 12:48:37 2022 +0200
1.3 @@ -50,7 +50,7 @@
1.4 and all Isac_Knowledge is in session Isac.
1.5 So Context.theory_name suffices
1.6
1.7 -* Eliminate mutable Rewrite_Ord.rew_ord' (!?);
1.8 +* Eliminate mutable Rewrite_Ord.id (!?);
1.9 shall be done in connection with cf. e587c45cae0f note in Build_Thydata.thy
1.10
1.11 * What is the idea behind KEStore_Elems.add_thes? How to do it properly in current Isabelle?
2.1 --- a/doc-isac/mat-eng-de.tex Wed Aug 03 18:17:27 2022 +0200
2.2 +++ b/doc-isac/mat-eng-de.tex Thu Aug 04 12:48:37 2022 +0200
2.3 @@ -463,7 +463,7 @@
2.4 Thm
2.5 ("sym_rmult_assoc",
2.6 "?m1 * (?n1 * ?k1) = ?m1 * ?n1 * ?k1" [.])],
2.7 - rew_ord = ("e_rew_ord", fn),
2.8 + rew_ord = ("Rewrite_Ord.id_empty", fn),
2.9 preconds = []} : rls
2.10 \end{verbatim}}
2.11
3.1 --- a/src/Tools/isac/BaseDefinitions/Know_Store.thy Wed Aug 03 18:17:27 2022 +0200
3.2 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy Thu Aug 04 12:48:37 2022 +0200
3.3 @@ -68,8 +68,8 @@
3.4 *)
3.5 signature KESTORE_ELEMS =
3.6 sig
3.7 - val get_rew_ord: theory -> Rewrite_Ord.rew_ord list
3.8 - val add_rew_ord: Rewrite_Ord.rew_ord list -> theory -> theory
3.9 + val get_rew_ord: theory -> Rewrite_Ord.T list
3.10 + val add_rew_ord: Rewrite_Ord.T list -> theory -> theory
3.11 val get_rlss: theory -> (Rule_Set.id * (ThyC.id * Rule_Set.T)) list
3.12 val add_rlss: (Rule_Set.id * (ThyC.id * Rule_Set.T)) list -> theory -> theory
3.13 val get_calcs: theory -> (Eval_Def.prog_calcID * (Eval_Def.calID * Eval_Def.eval_fn)) list
4.1 --- a/src/Tools/isac/BaseDefinitions/method-def.sml Wed Aug 03 18:17:27 2022 +0200
4.2 +++ b/src/Tools/isac/BaseDefinitions/method-def.sml Thu Aug 04 12:48:37 2022 +0200
4.3 @@ -37,7 +37,7 @@
4.4 {guh : Check_Unique.id, (* unique within Isac_Knowledge, for html-presentation *)
4.5 mathauthors: string list, (* copyright *)
4.6 init : References_Def.id, (* DEL: WN060721 pblID introduced mistakenly *)
4.7 - rew_ord' : Rule_Def.rew_ord', (* for ordered rewriting by Tactic.Rewrite *)
4.8 + rew_ord' : Rewrite_Ord.id, (* for ordered rewriting by Tactic.Rewrite *)
4.9 erls : Rule_Set.T, (* for conditions in rewriting by Tactic.Rewrite *)
4.10 srls : Rule_Set.T, (* for evaluating Prog_Expr *)
4.11 crls : Rule_Set.T, (* DEL: for check_elementwise *)
4.12 @@ -50,7 +50,7 @@
4.13 for constraints on identifiers see "O_Model.copy_name" *)
4.14 pre : term list (* ? DEL, as soon as they are input interactively ? *)
4.15 };
4.16 -val empty = {guh = "met_empty", mathauthors = [], init = id_empty, rew_ord' = Rewrite_Ord.e_rew_ord',
4.17 +val empty = {guh = "met_empty", mathauthors = [], init = id_empty, rew_ord' = Rewrite_Ord.id_empty,
4.18 erls = Rule_Set.empty, srls = Rule_Set.empty, prls = Rule_Set.empty, calc = [], crls = Rule_Set.empty,
4.19 errpats = [], nrls = Rule_Set.empty, ppc = [], pre = [], scr = Rule.Empty_Prog};
4.20 val empty_store = Store.Node ("empty_meth_id", [empty],[]);
5.1 --- a/src/Tools/isac/BaseDefinitions/rewrite-order.sml Wed Aug 03 18:17:27 2022 +0200
5.2 +++ b/src/Tools/isac/BaseDefinitions/rewrite-order.sml Thu Aug 04 12:48:37 2022 +0200
5.3 @@ -4,16 +4,17 @@
5.4 *)
5.5 signature REWRITE_ORDER =
5.6 sig
5.7 - val e_rew_ord': Rule_Def.rew_ord';
5.8 - val dummy_ord: Rule_Def.rew_ord_
5.9 - val e_rew_ord: Rule_Def.rew_ord_
5.10 + type id = Rule_Def.rew_ord_id
5.11 + val id_empty: id
5.12
5.13 - type rew_ord = Rule_Def.rew_ord
5.14 - val e_rew_ordX: rew_ord
5.15 - val to_string: rew_ord -> string
5.16 + type function = Rule_Def.rew_ord_function
5.17 + val function_empty: function
5.18
5.19 - type rew_ord' = Rule_Def.rew_ord'
5.20 - val equal: rew_ord * rew_ord -> bool
5.21 + type T = Rule_Def.rew_ord_T
5.22 + val empty: T
5.23 +
5.24 + val to_string: T -> string
5.25 + val equal: T * T -> bool
5.26 end
5.27
5.28 (**)
5.29 @@ -21,17 +22,16 @@
5.30 struct
5.31 (**)
5.32
5.33 -val e_rew_ord' = "e_rew_ord" : Rule_Def.rew_ord';
5.34 -type rew_ord_ = Rule_Def.rew_ord_;
5.35 -fun dummy_ord (_: subst) (_: term, _: term) = true;
5.36 -val e_rew_ord_ = dummy_ord;
5.37 +type id = Rule_Def.rew_ord_id
5.38 +val id_empty = "Rewrite_Ord.id_empty";
5.39
5.40 -type rew_ord = (*rew_ord' * rew_ord_;*) Rule_Def.rew_ord
5.41 -val e_rew_ord = dummy_ord; (* TODO.WN071231 clarify identifiers..e_rew_ordX*)
5.42 -val e_rew_ordX = (e_rew_ord', e_rew_ord_)
5.43 +type function = Rule_Def.rew_ord_function;
5.44 +fun function_empty (_: LibraryC.subst) (_: term, _: term) = true;
5.45 +
5.46 +type T = Rule_Def.rew_ord_T
5.47 +val empty = (id_empty, function_empty)
5.48 +
5.49 fun to_string (rew_ord', _) = "(" ^ rew_ord' ^ ", _: fn)"
5.50 -
5.51 -type rew_ord' = Rule_Def.rew_ord'
5.52 fun equal ((id1, _), (id2, _)) = id1 = id2
5.53
5.54 end
6.1 --- a/src/Tools/isac/BaseDefinitions/rule-def.sml Wed Aug 03 18:17:27 2022 +0200
6.2 +++ b/src/Tools/isac/BaseDefinitions/rule-def.sml Thu Aug 04 12:48:37 2022 +0200
6.3 @@ -10,19 +10,21 @@
6.4 type calc
6.5 eqtype calID
6.6 eqtype errpatID
6.7 - type rew_ord' = string
6.8 - type rew_ord_ = LibraryC.subst -> term * term -> bool
6.9 - type rew_ord = rew_ord' * rew_ord_
6.10 +
6.11 + type rew_ord_id = string
6.12 + type rew_ord_function = LibraryC.subst -> term * term -> bool
6.13 + type rew_ord_T = rew_ord_id * rew_ord_function
6.14 +
6.15 type eval_fn = string -> term -> Proof.context -> (string * term) option
6.16
6.17 datatype rule_set =
6.18 Empty
6.19 | Repeat of {calc: calc list, erls: rule_set, errpatts: errpatID list, id: string,
6.20 - preconds: term list, rew_ord: rew_ord, rules: rule list, scr: program, srls: rule_set}
6.21 + preconds: term list, rew_ord: rew_ord_T, rules: rule list, scr: program, srls: rule_set}
6.22 | Sequence of {calc: calc list, erls: rule_set, errpatts: errpatID list, id: string,
6.23 - preconds: term list, rew_ord: rew_ord, rules: rule list, scr: program, srls: rule_set}
6.24 + preconds: term list, rew_ord: rew_ord_T, rules: rule list, scr: program, srls: rule_set}
6.25 | Rrls of {calc: calc list, erls: rule_set, errpatts: errpatID list, id: string,
6.26 - prepat: (term list * term) list, rew_ord: rew_ord, scr: program}
6.27 + prepat: (term list * term) list, rew_ord: rew_ord_T, scr: program}
6.28 and rule = Cal1 of string * eval_fn | Eval of string * eval_fn | Erule
6.29 | Rls_ of rule_set | Thm of string * thm
6.30 and program =
6.31 @@ -44,9 +46,9 @@
6.32
6.33 type eval_fn = string -> term -> Proof.context -> (string * term) option;
6.34
6.35 -type rew_ord' = string;
6.36 -type rew_ord_ = LibraryC.subst -> term * term -> bool;
6.37 -type rew_ord = rew_ord' * rew_ord_;
6.38 +type rew_ord_id = string;
6.39 +type rew_ord_function = LibraryC.subst -> term * term -> bool;
6.40 +type rew_ord_T = rew_ord_id * rew_ord_function;
6.41
6.42 type calID = string;
6.43 type cal = calID * eval_fn;
6.44 @@ -109,7 +111,7 @@
6.45 | Repeat of (*a confluent and terminating ruleset, in principle *)
6.46 {id: string, (* for trace_rewrite *)
6.47 preconds: term list, (* STILL UNUSED *)
6.48 - rew_ord: rew_ord,(* for rules *)
6.49 + rew_ord: rew_ord_T,(* for rules *)
6.50 erls: rule_set, (* for the conditions in rules *)
6.51 srls: rule_set, (* for evaluation of Prog_Expr *)
6.52 calc: calc list, (* for Calculate in program, set by prep_rls' *)
6.53 @@ -117,7 +119,7 @@
6.54 errpatts: errpatID list,(* by dialog-authoring in Build_Thydata.thy *)
6.55 scr: program} (* DEPRECATED: intersteps are created on the fly now *)
6.56 | Sequence of (* a sequence of rules to be tried only once *)
6.57 - {id: string, preconds: term list, rew_ord: rew_ord, erls: rule_set, srls: rule_set,
6.58 + {id: string, preconds: term list, rew_ord: rew_ord_T, erls: rule_set, srls: rule_set,
6.59 calc: calc list, rules: rule list, errpatts: errpatID list, scr: program}
6.60 | Rrls of (* ML-functions within rewriting, _ONE_ redex rewritten per call*)
6.61 {id: string, (* for trace_rewrite *)
6.62 @@ -125,7 +127,7 @@
6.63 (term list * (* preconds, eval with subst from pattern below *)
6.64 term) (* pattern matched with current (sub)term *)
6.65 list, (* meta-conjunction in guarding is or *)
6.66 - rew_ord: rew_ord, erls: rule_set, calc: calc list, errpatts: errpatID list, scr: program}
6.67 + rew_ord: rew_ord_T, erls: rule_set, calc: calc list, errpatts: errpatID list, scr: program}
6.68
6.69 fun program_to_string Empty_Prog = "Empty_Prog"
6.70 | program_to_string (Prog s) = "Prog " ^ UnparseC.term s
7.1 --- a/src/Tools/isac/BaseDefinitions/rule-set.sml Wed Aug 03 18:17:27 2022 +0200
7.2 +++ b/src/Tools/isac/BaseDefinitions/rule-set.sml Thu Aug 04 12:48:37 2022 +0200
7.3 @@ -11,7 +11,7 @@
7.4
7.5 val id: T -> string
7.6 val rep: T -> {calc: Rule_Def.calc list, erls: T, errpats: Rule_Def.errpatID list, id: string,
7.7 - preconds: term list, rew_ord: Rewrite_Ord.rew_ord, rules: Rule_Def.rule list, scr: Rule_Def.program, srls: T}
7.8 + preconds: term list, rew_ord: Rewrite_Ord.T, rules: Rule_Def.rule list, scr: Rule_Def.program, srls: T}
7.9 val to_string: T -> string
7.10
7.11 val append_rules: string -> T -> Rule_Def.rule list -> T
8.1 --- a/src/Tools/isac/BaseDefinitions/thy-write.sml Wed Aug 03 18:17:27 2022 +0200
8.2 +++ b/src/Tools/isac/BaseDefinitions/thy-write.sml Thu Aug 04 12:48:37 2022 +0200
8.3 @@ -12,7 +12,7 @@
8.4 type authors
8.5 datatype thydata
8.6 = Hcal of {calc: Rule_Def.calc, coursedesign: authors, guh: Check_Unique.id, mathauthors: authors}
8.7 - | Hord of {coursedesign: authors, guh: Check_Unique.id, mathauthors: authors, ord: Rule_Def.rew_ord_}
8.8 + | Hord of {coursedesign: authors, guh: Check_Unique.id, mathauthors: authors, ord: Rewrite_Ord.function}
8.9 | Hrls of {coursedesign: authors, guh: Check_Unique.id, mathauthors: authors, thy_rls: ThyC.id * Rule_Set.T}
8.10 | Hthm of {coursedesign: authors, fillpats: Error_Pattern_Def.fill_in list, guh: Check_Unique.id, mathauthors: authors, thm: thm}
8.11 | Html of {coursedesign: authors, guh: Check_Unique.id, html: string, mathauthors: authors}
9.1 --- a/src/Tools/isac/Interpret/derive.sml Wed Aug 03 18:17:27 2022 +0200
9.2 +++ b/src/Tools/isac/Interpret/derive.sml Thu Aug 04 12:48:37 2022 +0200
9.3 @@ -14,11 +14,11 @@
9.4 type step
9.5 type derivation
9.6
9.7 - val do_one : Proof.context -> Rule_Set.T -> Rule.rule list -> Rule_Def.rew_ord_ ->
9.8 + val do_one : Proof.context -> Rule_Set.T -> Rule.rule list -> Rewrite_Ord.function ->
9.9 term option -> term -> derivation
9.10 - val steps_reverse : Proof.context -> Rule_Set.T -> Rule.rule list -> Rule_Def.rew_ord_ ->
9.11 + val steps_reverse : Proof.context -> Rule_Set.T -> Rule.rule list -> Rewrite_Ord.function ->
9.12 term option -> term -> rule_result list
9.13 - val steps : Rule_Def.rew_ord -> Rule_Set.T -> Rule.rule list -> term -> term ->
9.14 + val steps : Rewrite_Ord.T -> Rule_Set.T -> Rule.rule list -> term -> term ->
9.15 bool * derivation
9.16 val embed: State_Steps.T -> Calc.T -> Pos.pos' list * Calc.T
9.17 \<^isac_test>\<open>
10.1 --- a/src/Tools/isac/Interpret/error-pattern.sml Wed Aug 03 18:17:27 2022 +0200
10.2 +++ b/src/Tools/isac/Interpret/error-pattern.sml Thu Aug 04 12:48:37 2022 +0200
10.3 @@ -58,7 +58,7 @@
10.4 let
10.5 val ctxt = Proof_Context.init_global ((ThyC.Isac()))
10.6 val (res', _, _, rewritten) =
10.7 - Rewrite.rew_sub ctxt 1 subst Rewrite_Ord.e_rew_ord
10.8 + Rewrite.rew_sub ctxt 1 subst Rewrite_Ord.function_empty
10.9 Rule_Set.empty false [] (HOLogic.Trueprop $ pat) res;
10.10 in
10.11 if rewritten then
10.12 @@ -100,7 +100,7 @@
10.13 let
10.14 val ctxt = Proof_Context.init_global ((ThyC.Isac()))
10.15 val (form', _, _, rewritten) =
10.16 - Rewrite.rew_sub ctxt 1 subst Rewrite_Ord.e_rew_ord Rule_Set.empty false [] (HOLogic.Trueprop $ pat) form;
10.17 + Rewrite.rew_sub ctxt 1 subst Rewrite_Ord.function_empty Rule_Set.empty false [] (HOLogic.Trueprop $ pat) form;
10.18 in (*the fillpat of the thm must be dedicated to id*)
10.19 if id = erpaID andalso rewritten then
10.20 SOME (fillpatID, HOLogic.mk_eq (form, form'), thm, subs_opt)
11.1 --- a/src/Tools/isac/Interpret/solve-step.sml Wed Aug 03 18:17:27 2022 +0200
11.2 +++ b/src/Tools/isac/Interpret/solve-step.sml Thu Aug 04 12:48:37 2022 +0200
11.3 @@ -17,7 +17,7 @@
11.4 theory -> Tactic.T -> Pos.pos' -> Ctree.ctree -> Test_Out.T
11.5
11.6 val get_ruleset: 'a -> Pos.pos -> Ctree.ctree ->
11.7 - string * ThyC.id * Rule_Def.rew_ord' * Rule_Def.rule_set * bool
11.8 + string * ThyC.id * Rewrite_Ord.id * Rule_Def.rule_set * bool
11.9 val get_eval: string -> Pos.pos ->Ctree.ctree ->
11.10 string * ThyC.id * (string * Rule_Def.eval_fn)
11.11 \<^isac_test>\<open>
12.1 --- a/src/Tools/isac/Knowledge/Base_Tools.thy Wed Aug 03 18:17:27 2022 +0200
12.2 +++ b/src/Tools/isac/Knowledge/Base_Tools.thy Thu Aug 04 12:48:37 2022 +0200
12.3 @@ -50,15 +50,15 @@
12.4 fun term_ordI (_: subst) uv = Term_Ord.term_ord uv;
12.5 end;
12.6 \<close> ML \<open>
12.7 -(*TODO.WN0509 reduce ids: tless_true = e_rew_ord' = Rewrite_Ord.e_rew_ord = Rewrite_Ord.dummy_ord*)
12.8 -val tless_true = Rewrite_Ord.dummy_ord;
12.9 +(*TODO.WN0509 reduce ids: tless_true = e_rew_ord' = Rewrite_Ord.function_empty = Rewrite_Ord.function_empty*)
12.10 +val tless_true = Rewrite_Ord.function_empty;
12.11 \<close> ML \<open>
12.12 \<close>
12.13 setup \<open>KEStore_Elems.add_rew_ord [
12.14 ("tless_true", tless_true),
12.15 - ("e_rew_ord", tless_true),
12.16 + ("Rewrite_Ord.id_empty", tless_true),
12.17 ("e_rew_ord'", tless_true),
12.18 - ("dummy_ord", Rewrite_Ord.dummy_ord)]\<close>
12.19 + ("dummy_ord", Rewrite_Ord.function_empty)]\<close>
12.20
12.21 subsection \<open>rule-sets\<close>
12.22 ML \<open>
13.1 --- a/src/Tools/isac/Knowledge/DiophantEq.thy Wed Aug 03 18:17:27 2022 +0200
13.2 +++ b/src/Tools/isac/Knowledge/DiophantEq.thy Thu Aug 04 12:48:37 2022 +0200
13.3 @@ -33,7 +33,7 @@
13.4 (Try (Calculate ''TIMES''))) e_e)"
13.5
13.6 method met_test_diophant : "Test/solve_diophant" =
13.7 - \<open>{rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule_Set.empty, prls = Rule_Set.empty, calc = [],
13.8 + \<open>{rew_ord' = "Rewrite_Ord.id_empty", rls' = tval_rls, srls = Rule_Set.empty, prls = Rule_Set.empty, calc = [],
13.9 crls = tval_rls, errpats = [], nrls = Test_simplify}\<close>
13.10 Program: diophant_equation.simps
13.11 Given: "boolTestGiven e_e" "intTestGiven (v_v::int)"
14.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Wed Aug 03 18:17:27 2022 +0200
14.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Thu Aug 04 12:48:37 2022 +0200
14.3 @@ -190,7 +190,7 @@
14.4 #2 NOT using common_nominator_p .*)
14.5 val norm_System_noadd_fractions =
14.6 Rule_Def.Repeat {id = "norm_System_noadd_fractions", preconds = [],
14.7 - rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
14.8 + rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
14.9 erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
14.10 rules = [(*sequence given by operator precedence*)
14.11 Rule.Rls_ discard_minus,
14.12 @@ -209,7 +209,7 @@
14.13 *1* using 'ord_simplify_System' in 'order_add_mult_System'.*)
14.14 val norm_System =
14.15 Rule_Def.Repeat {id = "norm_System", preconds = [],
14.16 - rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
14.17 + rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
14.18 erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
14.19 rules = [(*sequence given by operator precedence*)
14.20 Rule.Rls_ discard_minus,
14.21 @@ -235,7 +235,7 @@
14.22 analoguous to simplify_Integral .*)
14.23 val simplify_System_parenthesized =
14.24 Rule_Set.Sequence {id = "simplify_System_parenthesized", preconds = []:term list,
14.25 - rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
14.26 + rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
14.27 erls = Atools_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
14.28 rules = [
14.29 \<^rule_thm>\<open>distrib_right\<close>, (*"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"*)
14.30 @@ -255,7 +255,7 @@
14.31 (*TODO.WN051031 ^^^^^^^^^^ should be in EACH rls contained *)
14.32 val simplify_System =
14.33 Rule_Set.Sequence {id = "simplify_System", preconds = []:term list,
14.34 - rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
14.35 + rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
14.36 erls = Atools_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
14.37 rules = [
14.38 Rule.Rls_ norm_Rational,
14.39 @@ -274,7 +274,7 @@
14.40 ML \<open>
14.41 val isolate_bdvs =
14.42 Rule_Def.Repeat {
14.43 - id="isolate_bdvs", preconds = [], rew_ord = ("e_rew_ord", Rewrite_Ord.e_rew_ord),
14.44 + id="isolate_bdvs", preconds = [], rew_ord = ("Rewrite_Ord.id_empty", Rewrite_Ord.function_empty),
14.45 erls = Rule_Set.append_rules "erls_isolate_bdvs" Rule_Set.empty [
14.46 (\<^rule_eval>\<open>occur_exactly_in\<close> (eval_occur_exactly_in "#eval_occur_exactly_in_"))],
14.47 srls = Rule_Set.Empty, calc = [], errpatts = [],
14.48 @@ -287,7 +287,7 @@
14.49 ML \<open>
14.50 val isolate_bdvs_4x4 =
14.51 Rule_Def.Repeat {id="isolate_bdvs_4x4", preconds = [],
14.52 - rew_ord = ("e_rew_ord", Rewrite_Ord.e_rew_ord),
14.53 + rew_ord = ("Rewrite_Ord.id_empty", Rewrite_Ord.function_empty),
14.54 erls = Rule_Set.append_rules "erls_isolate_bdvs_4x4" Rule_Set.empty [
14.55 \<^rule_eval>\<open>occur_exactly_in\<close> (eval_occur_exactly_in "#eval_occur_exactly_in_"),
14.56 \<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),
14.57 @@ -318,9 +318,9 @@
14.58
14.59 val prls_triangular =
14.60 Rule_Def.Repeat {
14.61 - id="prls_triangular", preconds = [], rew_ord = ("e_rew_ord", Rewrite_Ord.e_rew_ord),
14.62 + id="prls_triangular", preconds = [], rew_ord = ("Rewrite_Ord.id_empty", Rewrite_Ord.function_empty),
14.63 erls = Rule_Def.Repeat {
14.64 - id="erls_prls_triangular", preconds = [], rew_ord = ("e_rew_ord", Rewrite_Ord.e_rew_ord),
14.65 + id="erls_prls_triangular", preconds = [], rew_ord = ("Rewrite_Ord.id_empty", Rewrite_Ord.function_empty),
14.66 erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
14.67 rules = [(*for precond NTH_CONS ...*)
14.68 \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
14.69 @@ -344,9 +344,9 @@
14.70 more similarity to prls_triangular desirable*)
14.71 val prls_triangular4 =
14.72 Rule_Def.Repeat {
14.73 - id="prls_triangular4", preconds = [], rew_ord = ("e_rew_ord", Rewrite_Ord.e_rew_ord),
14.74 + id="prls_triangular4", preconds = [], rew_ord = ("Rewrite_Ord.id_empty", Rewrite_Ord.function_empty),
14.75 erls = Rule_Def.Repeat {
14.76 - id="erls_prls_triangular4", preconds = [], rew_ord = ("e_rew_ord", Rewrite_Ord.e_rew_ord),
14.77 + id="erls_prls_triangular4", preconds = [], rew_ord = ("Rewrite_Ord.id_empty", Rewrite_Ord.function_empty),
14.78 erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
14.79 rules = [(*for precond NTH_CONS ...*)
14.80 \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
15.1 --- a/src/Tools/isac/Knowledge/Integrate.thy Wed Aug 03 18:17:27 2022 +0200
15.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy Thu Aug 04 12:48:37 2022 +0200
15.3 @@ -158,12 +158,12 @@
15.4 (*.for simplify_Integral adapted from 'norm_Rational_rls'.*)
15.5 val norm_Rational_rls_noadd_fractions =
15.6 Rule_Def.Repeat {id = "norm_Rational_rls_noadd_fractions", preconds = [],
15.7 - rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
15.8 + rew_ord = ("dummy_ord",Rewrite_Ord.function_empty),
15.9 erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
15.10 rules = [(*Rule.Rls_ add_fractions_p_rls,!!!*)
15.11 Rule.Rls_ (*rat_mult_div_pow original corrected WN051028*)
15.12 (Rule_Def.Repeat {id = "rat_mult_div_pow", preconds = [],
15.13 - rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
15.14 + rew_ord = ("dummy_ord",Rewrite_Ord.function_empty),
15.15 erls = Rule_Set.append_rules "Rule_Set.empty-is_polyexp" Rule_Set.empty
15.16 [\<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp "")],
15.17 srls = Rule_Set.Empty, calc = [], errpatts = [],
15.18 @@ -187,7 +187,7 @@
15.19 (*.for simplify_Integral adapted from 'norm_Rational'.*)
15.20 val norm_Rational_noadd_fractions =
15.21 Rule_Set.Sequence {id = "norm_Rational_noadd_fractions", preconds = [],
15.22 - rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
15.23 + rew_ord = ("dummy_ord",Rewrite_Ord.function_empty),
15.24 erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
15.25 rules = [Rule.Rls_ discard_minus,
15.26 Rule.Rls_ rat_mult_poly,(* removes double fractions like a/b/c *)
15.27 @@ -214,7 +214,7 @@
15.28 ];
15.29 val simplify_Integral =
15.30 Rule_Set.Sequence {id = "simplify_Integral", preconds = []:term list,
15.31 - rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
15.32 + rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
15.33 erls = Atools_erls, srls = Rule_Set.Empty,
15.34 calc = [], errpatts = [],
15.35 rules = [
16.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Wed Aug 03 18:17:27 2022 +0200
16.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Thu Aug 04 12:48:37 2022 +0200
16.3 @@ -27,7 +27,7 @@
16.4
16.5 ML \<open>
16.6 val inverse_z = prep_rls'(
16.7 - Rule_Def.Repeat {id = "inverse_z", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
16.8 + Rule_Def.Repeat {id = "inverse_z", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.function_empty),
16.9 erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
16.10 rules =
16.11 [
17.1 --- a/src/Tools/isac/Knowledge/LinEq.thy Wed Aug 03 18:17:27 2022 +0200
17.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy Thu Aug 04 12:48:37 2022 +0200
17.3 @@ -88,7 +88,7 @@
17.4 (*isolate the bound variable in an linear equation; 'bdv' is a meta-constant*)
17.5 val LinEq_simplify = prep_rls'(
17.6 Rule_Def.Repeat {id = "LinEq_simplify", preconds = [],
17.7 - rew_ord = ("e_rew_ord", Rewrite_Ord.e_rew_ord),
17.8 + rew_ord = ("Rewrite_Ord.id_empty", Rewrite_Ord.function_empty),
17.9 erls = LinEq_erls,
17.10 srls = Rule_Set.Empty,
17.11 calc = [], errpatts = [],
18.1 --- a/src/Tools/isac/Knowledge/Partial_Fractions.thy Wed Aug 03 18:17:27 2022 +0200
18.2 +++ b/src/Tools/isac/Knowledge/Partial_Fractions.thy Thu Aug 04 12:48:37 2022 +0200
18.3 @@ -106,7 +106,7 @@
18.4
18.5 ML \<open>
18.6 val ansatz_rls = prep_rls'(
18.7 - Rule_Def.Repeat {id = "ansatz_rls", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
18.8 + Rule_Def.Repeat {id = "ansatz_rls", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.function_empty),
18.9 erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
18.10 rules = [
18.11 \<^rule_thm>\<open>ansatz_2nd_order\<close>,
18.12 @@ -114,7 +114,7 @@
18.13 scr = Rule.Empty_Prog});
18.14
18.15 val equival_trans = prep_rls'(
18.16 - Rule_Def.Repeat {id = "equival_trans", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
18.17 + Rule_Def.Repeat {id = "equival_trans", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.function_empty),
18.18 erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
18.19 rules = [
18.20 \<^rule_thm>\<open>equival_trans_2nd_order\<close>,
18.21 @@ -122,7 +122,7 @@
18.22 scr = Rule.Empty_Prog});
18.23
18.24 val multiply_ansatz = prep_rls'(
18.25 - Rule_Def.Repeat {id = "multiply_ansatz", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
18.26 + Rule_Def.Repeat {id = "multiply_ansatz", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.function_empty),
18.27 erls = Rule_Set.Empty,
18.28 srls = Rule_Set.Empty, calc = [], errpatts = [],
18.29 rules = [
19.1 --- a/src/Tools/isac/Knowledge/Poly.thy Wed Aug 03 18:17:27 2022 +0200
19.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Thu Aug 04 12:48:37 2022 +0200
19.3 @@ -723,7 +723,7 @@
19.4 \<close>
19.5 ML \<open>
19.6 val expand =
19.7 - Rule_Def.Repeat {id = "expand", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
19.8 + Rule_Def.Repeat {id = "expand", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
19.9 erls = Rule_Set.empty,srls = Rule_Set.Empty, calc = [], errpatts = [],
19.10 rules = [
19.11 \<^rule_thm>\<open>distrib_right\<close>, (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
19.12 @@ -735,7 +735,7 @@
19.13 ML \<open>
19.14 (* erls for calculate_Rational + etc *)
19.15 val powers_erls =
19.16 - Rule_Def.Repeat {id = "powers_erls", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
19.17 + Rule_Def.Repeat {id = "powers_erls", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.function_empty),
19.18 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
19.19 rules = [
19.20 \<^rule_eval>\<open>matches\<close> (Prog_Expr.eval_matches "#matches_"),
19.21 @@ -750,7 +750,7 @@
19.22
19.23 \<close> ML \<open>
19.24 val discard_minus =
19.25 - Rule_Def.Repeat {id = "discard_minus", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
19.26 + Rule_Def.Repeat {id = "discard_minus", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
19.27 erls = powers_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
19.28 rules = [
19.29 \<^rule_thm>\<open>real_diff_minus\<close> (*"a - b = a + -1 * b"*),
19.30 @@ -759,7 +759,7 @@
19.31
19.32 val expand_poly_ =
19.33 Rule_Def.Repeat{id = "expand_poly_", preconds = [],
19.34 - rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
19.35 + rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
19.36 erls = powers_erls, srls = Rule_Set.Empty,
19.37 calc = [], errpatts = [],
19.38 rules = [
19.39 @@ -785,7 +785,7 @@
19.40
19.41 val expand_poly_rat_ =
19.42 Rule_Def.Repeat{id = "expand_poly_rat_", preconds = [],
19.43 - rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
19.44 + rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
19.45 erls = Rule_Set.append_rules "Rule_Set.empty-expand_poly_rat_" Rule_Set.empty [
19.46 \<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp ""),
19.47 \<^rule_eval>\<open>is_even\<close> (Prog_Expr.eval_is_even "#is_even_"),
19.48 @@ -813,7 +813,7 @@
19.49
19.50 val simplify_power_ =
19.51 Rule_Def.Repeat{id = "simplify_power_", preconds = [],
19.52 - rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
19.53 + rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
19.54 erls = Rule_Set.empty, srls = Rule_Set.Empty,
19.55 calc = [], errpatts = [],
19.56 rules = [
19.57 @@ -836,7 +836,7 @@
19.58
19.59 val calc_add_mult_pow_ =
19.60 Rule_Def.Repeat{id = "calc_add_mult_pow_", preconds = [],
19.61 - rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
19.62 + rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
19.63 erls = Atools_erls(*erls3.4.03*),srls = Rule_Set.Empty,
19.64 calc = [("PLUS" , (\<^const_name>\<open>plus\<close>, eval_binop "#add_")),
19.65 ("TIMES" , (\<^const_name>\<open>times\<close>, eval_binop "#mult_")),
19.66 @@ -851,7 +851,7 @@
19.67
19.68 val reduce_012_mult_ =
19.69 Rule_Def.Repeat{id = "reduce_012_mult_", preconds = [],
19.70 - rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
19.71 + rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
19.72 erls = Rule_Set.empty,srls = Rule_Set.Empty,
19.73 calc = [], errpatts = [],
19.74 rules = [(* MG: folgende Rule.Thm müssen hier stehen bleiben: *)
19.75 @@ -863,7 +863,7 @@
19.76
19.77 val collect_numerals_ =
19.78 Rule_Def.Repeat{id = "collect_numerals_", preconds = [],
19.79 - rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
19.80 + rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
19.81 erls = Atools_erls, srls = Rule_Set.Empty,
19.82 calc = [("PLUS" , (\<^const_name>\<open>plus\<close>, eval_binop "#add_"))
19.83 ], errpatts = [],
19.84 @@ -884,7 +884,7 @@
19.85
19.86 val reduce_012_ =
19.87 Rule_Def.Repeat{id = "reduce_012_", preconds = [],
19.88 - rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
19.89 + rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
19.90 erls = Rule_Set.empty,srls = Rule_Set.Empty, calc = [], errpatts = [],
19.91 rules = [
19.92 \<^rule_thm>\<open>mult_1_left\<close>, (*"1 * z = z"*)
19.93 @@ -904,7 +904,7 @@
19.94
19.95 val expand_poly =
19.96 Rule_Def.Repeat{id = "expand_poly", preconds = [],
19.97 - rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
19.98 + rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
19.99 erls = powers_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
19.100 rules = [
19.101 \<^rule_thm>\<open>distrib_right\<close>, (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
19.102 @@ -925,7 +925,7 @@
19.103
19.104 val simplify_power =
19.105 Rule_Def.Repeat{id = "simplify_power", preconds = [],
19.106 - rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
19.107 + rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
19.108 erls = Rule_Set.empty, srls = Rule_Set.Empty,
19.109 calc = [], errpatts = [],
19.110 rules = [
19.111 @@ -941,7 +941,7 @@
19.112
19.113 val collect_numerals =
19.114 Rule_Def.Repeat{id = "collect_numerals", preconds = [],
19.115 - rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
19.116 + rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
19.117 erls = Atools_erls(*erls3.4.03*),srls = Rule_Set.Empty,
19.118 calc = [("PLUS" , (\<^const_name>\<open>plus\<close>, eval_binop "#add_")),
19.119 ("TIMES" , (\<^const_name>\<open>times\<close>, eval_binop "#mult_")),
19.120 @@ -959,7 +959,7 @@
19.121 scr = Rule.Empty_Prog};
19.122 val reduce_012 =
19.123 Rule_Def.Repeat{id = "reduce_012", preconds = [],
19.124 - rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
19.125 + rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
19.126 erls = Rule_Set.append_rules "erls_in_reduce_012" Rule_Set.empty [
19.127 \<^rule_eval>\<open>is_num\<close> (Prog_Expr.eval_is_num "#is_num_"),
19.128 \<^rule_thm>\<open>not_false\<close>,
19.129 @@ -989,7 +989,7 @@
19.130 (total-degree-)ordering of monoms NOT possible with size_of_term GIVEN*)
19.131 val order_add_mult =
19.132 Rule_Def.Repeat{id = "order_add_mult", preconds = [],
19.133 - rew_ord = ("ord_make_polynomial",ord_make_polynomial false \<^theory>),
19.134 + rew_ord = ("ord_make_polynomial", ord_make_polynomial false \<^theory>),
19.135 erls = Rule_Set.empty,srls = Rule_Set.Empty,
19.136 calc = [], errpatts = [],
19.137 rules = [
19.138 @@ -1029,7 +1029,7 @@
19.139 which evaluates (the instantiated) "?p is_multUnordered" to true *)
19.140 [([TermC.parse_patt \<^theory> "?p is_multUnordered"],
19.141 TermC.parse_patt \<^theory> "?p :: real")],
19.142 - rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
19.143 + rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
19.144 erls = Rule_Set.append_rules "Rule_Set.empty-is_multUnordered" Rule_Set.empty
19.145 [\<^rule_eval>\<open>is_multUnordered\<close> (eval_is_multUnordered "")],
19.146 calc = [("PLUS" , (\<^const_name>\<open>plus\<close>, eval_binop "#add_")),
19.147 @@ -1044,7 +1044,7 @@
19.148 attach_form = attach_form}};
19.149 val order_mult_rls_ =
19.150 Rule_Def.Repeat {id = "order_mult_rls_", preconds = [],
19.151 - rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
19.152 + rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
19.153 erls = Rule_Set.empty,srls = Rule_Set.Empty,
19.154 calc = [], errpatts = [],
19.155 rules = [
19.156 @@ -1069,7 +1069,7 @@
19.157 TermC.parse_patt @{theory} "?p :: real"
19.158 (*WN.18.6.03 also KEIN pattern, dieses erzeugt nur das Environment
19.159 fuer die Evaluation der Precondition "p is_addUnordered"*))],
19.160 - rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
19.161 + rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
19.162 erls = Rule_Set.append_rules "Rule_Set.empty-is_addUnordered" Rule_Set.empty(*MG: poly_erls*)
19.163 [\<^rule_eval>\<open>is_addUnordered\<close> (eval_is_addUnordered "")],
19.164 calc = [
19.165 @@ -1087,7 +1087,7 @@
19.166
19.167 val order_add_rls_ =
19.168 Rule_Def.Repeat {id = "order_add_rls_", preconds = [],
19.169 - rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
19.170 + rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
19.171 erls = Rule_Set.empty, srls = Rule_Set.Empty,
19.172 calc = [], errpatts = [],
19.173 rules = [
19.174 @@ -1108,7 +1108,7 @@
19.175 val make_polynomial(*MG.03, overwrites version from above,
19.176 previously 'make_polynomial_'*) =
19.177 Rule_Set.Sequence {id = "make_polynomial", preconds = []:term list,
19.178 - rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
19.179 + rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
19.180 erls = Atools_erls, srls = Rule_Set.Empty,calc = [], errpatts = [],
19.181 rules = [
19.182 Rule.Rls_ discard_minus,
19.183 @@ -1127,7 +1127,7 @@
19.184 ML \<open>
19.185 val norm_Poly(*=make_polynomial*) =
19.186 Rule_Set.Sequence {id = "norm_Poly", preconds = []:term list,
19.187 - rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
19.188 + rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
19.189 erls = Atools_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
19.190 rules = [
19.191 Rule.Rls_ discard_minus,
19.192 @@ -1149,7 +1149,7 @@
19.193 (* MG necessary for termination of norm_Rational(*_mg*) in Rational.ML*)
19.194 val make_rat_poly_with_parentheses =
19.195 Rule_Set.Sequence{id = "make_rat_poly_with_parentheses", preconds = []:term list,
19.196 - rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
19.197 + rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
19.198 erls = Atools_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
19.199 rules = [
19.200 Rule.Rls_ discard_minus,
19.201 @@ -1375,5 +1375,5 @@
19.202 Find: "normalform n_n"
19.203 ML \<open>
19.204 \<close> ML \<open>
19.205 -\<close>
19.206 +\<close>
19.207 end
20.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Wed Aug 03 18:17:27 2022 +0200
20.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Thu Aug 04 12:48:37 2022 +0200
20.3 @@ -361,7 +361,7 @@
20.4
20.5 val cancel_leading_coeff = prep_rls'(
20.6 Rule_Def.Repeat {id = "cancel_leading_coeff", preconds = [],
20.7 - rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord),
20.8 + rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty),
20.9 erls = PolyEq_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
20.10 rules = [
20.11 \<^rule_thm>\<open>cancel_leading_coeff1\<close>,
20.12 @@ -384,7 +384,7 @@
20.13 ML\<open>
20.14 val complete_square = prep_rls'(
20.15 Rule_Def.Repeat {id = "complete_square", preconds = [],
20.16 - rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord),
20.17 + rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty),
20.18 erls = PolyEq_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
20.19 rules = [
20.20 \<^rule_thm>\<open>complete_square1\<close>,
20.21 @@ -427,7 +427,7 @@
20.22 (*isolate the bound variable in an d0 equation; 'bdv' is a meta-constant*)
20.23 val d0_polyeq_simplify = prep_rls'(
20.24 Rule_Def.Repeat {id = "d0_polyeq_simplify", preconds = [],
20.25 - rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord),
20.26 + rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty),
20.27 erls = PolyEq_erls,
20.28 srls = Rule_Set.Empty,
20.29 calc = [], errpatts = [],
20.30 @@ -440,7 +440,7 @@
20.31 (*isolate the bound variable in an d1 equation; 'bdv' is a meta-constant*)
20.32 val d1_polyeq_simplify = prep_rls'(
20.33 Rule_Def.Repeat {id = "d1_polyeq_simplify", preconds = [],
20.34 - rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord),
20.35 + rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty),
20.36 erls = PolyEq_erls,
20.37 srls = Rule_Set.Empty,
20.38 calc = [], errpatts = [],
20.39 @@ -456,7 +456,7 @@
20.40 (* isolate the bound variable in an d2 equation with bdv only;
20.41 "bdv" is a meta-constant substituted for the "x" below by isac's rewriter. *)
20.42 val d2_polyeq_bdv_only_simplify = prep_rls'(
20.43 - Rule_Def.Repeat {id = "d2_polyeq_bdv_only_simplify", preconds = [], rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord),
20.44 + Rule_Def.Repeat {id = "d2_polyeq_bdv_only_simplify", preconds = [], rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty),
20.45 erls = PolyEq_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
20.46 rules = [
20.47 \<^rule_thm>\<open>d2_prescind1\<close>, (* ax+bx^2=0 -> x(a+bx)=0 *)
20.48 @@ -475,7 +475,7 @@
20.49 'bdv' is a meta-constant*)
20.50 val d2_polyeq_sq_only_simplify = prep_rls'(
20.51 Rule_Def.Repeat {id = "d2_polyeq_sq_only_simplify", preconds = [],
20.52 - rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord),
20.53 + rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty),
20.54 erls = PolyEq_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
20.55 rules = [
20.56 \<^rule_thm>\<open>d2_isolate_add1\<close>,(* a+ bx^2=0 -> bx^2=(-1)a*)
20.57 @@ -491,7 +491,7 @@
20.58 'bdv' is a meta-constant*)
20.59 val d2_polyeq_pqFormula_simplify = prep_rls'(
20.60 Rule_Def.Repeat {id = "d2_polyeq_pqFormula_simplify", preconds = [],
20.61 - rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord), erls = PolyEq_erls,
20.62 + rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty), erls = PolyEq_erls,
20.63 srls = Rule_Set.Empty, calc = [], errpatts = [],
20.64 rules = [
20.65 \<^rule_thm>\<open>d2_pqformula1\<close>, (* q+px+ x^2=0 *)
20.66 @@ -518,7 +518,7 @@
20.67 'bdv' is a meta-constant*)
20.68 val d2_polyeq_abcFormula_simplify = prep_rls'(
20.69 Rule_Def.Repeat {id = "d2_polyeq_abcFormula_simplify", preconds = [],
20.70 - rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord), erls = PolyEq_erls,
20.71 + rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty), erls = PolyEq_erls,
20.72 srls = Rule_Set.Empty, calc = [], errpatts = [],
20.73 rules = [
20.74 \<^rule_thm>\<open>d2_abcformula1\<close>, (*c+bx+cx^2=0 *)
20.75 @@ -545,7 +545,7 @@
20.76 'bdv' is a meta-constant*)
20.77 val d2_polyeq_simplify = prep_rls'(
20.78 Rule_Def.Repeat {id = "d2_polyeq_simplify", preconds = [],
20.79 - rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord), erls = PolyEq_erls,
20.80 + rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty), erls = PolyEq_erls,
20.81 srls = Rule_Set.Empty, calc = [], errpatts = [],
20.82 rules = [
20.83 \<^rule_thm>\<open>d2_pqformula1\<close>, (* p+qx+ x^2=0 *)
20.84 @@ -578,7 +578,7 @@
20.85 (* isolate the bound variable in an d3 equation; 'bdv' is a meta-constant *)
20.86 val d3_polyeq_simplify = prep_rls'(
20.87 Rule_Def.Repeat {id = "d3_polyeq_simplify", preconds = [],
20.88 - rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord), erls = PolyEq_erls,
20.89 + rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty), erls = PolyEq_erls,
20.90 srls = Rule_Set.Empty, calc = [], errpatts = [],
20.91 rules = [
20.92 \<^rule_thm>\<open>d3_reduce_equation1\<close>, (*a*bdv + b*bdv \<up> 2 + c*bdv \<up> 3=0) = (bdv=0 | (a + b*bdv + c*bdv \<up> 2=0)*)
20.93 @@ -608,7 +608,7 @@
20.94 (*isolate the bound variable in an d4 equation; 'bdv' is a meta-constant*)
20.95 val d4_polyeq_simplify = prep_rls'(
20.96 Rule_Def.Repeat {id = "d4_polyeq_simplify", preconds = [],
20.97 - rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord), erls = PolyEq_erls,
20.98 + rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty), erls = PolyEq_erls,
20.99 srls = Rule_Set.Empty, calc = [], errpatts = [],
20.100 rules = [
20.101 \<^rule_thm>\<open>d4_sub_u1\<close> (* ax^4+bx^2+c=0 -> x=+-sqrt(ax^2+bx^+c) *)],
20.102 @@ -1128,7 +1128,7 @@
20.103 ML\<open>
20.104 val collect_bdv = prep_rls'(
20.105 Rule_Def.Repeat{id = "collect_bdv", preconds = [],
20.106 - rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
20.107 + rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
20.108 erls = Rule_Set.empty,srls = Rule_Set.Empty,
20.109 calc = [], errpatts = [],
20.110 rules = [\<^rule_thm>\<open>bdv_collect_1\<close>,
20.111 @@ -1163,7 +1163,7 @@
20.112 according to knowledge/Poly.sml.*)
20.113 val make_polynomial_in = prep_rls'(
20.114 Rule_Set.Sequence {
20.115 - id = "make_polynomial_in", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
20.116 + id = "make_polynomial_in", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
20.117 erls = Atools_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
20.118 rules = [
20.119 Rule.Rls_ expand_poly,
20.120 @@ -1189,7 +1189,7 @@
20.121 ML\<open>
20.122 val make_ratpoly_in = prep_rls'(
20.123 Rule_Set.Sequence {
20.124 - id = "make_ratpoly_in", preconds = []:term list, rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
20.125 + id = "make_ratpoly_in", preconds = []:term list, rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
20.126 erls = Atools_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
20.127 rules = [
20.128 Rule.Rls_ norm_Rational,
21.1 --- a/src/Tools/isac/Knowledge/PolyMinus.thy Wed Aug 03 18:17:27 2022 +0200
21.2 +++ b/src/Tools/isac/Knowledge/PolyMinus.thy Thu Aug 04 12:48:37 2022 +0200
21.3 @@ -191,7 +191,7 @@
21.4
21.5 val ordne_alphabetisch =
21.6 Rule_Def.Repeat{id = "ordne_alphabetisch", preconds = [],
21.7 - rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), srls = Rule_Set.Empty, calc = [], errpatts = [],
21.8 + rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), srls = Rule_Set.Empty, calc = [], errpatts = [],
21.9 erls = erls_ordne_alphabetisch,
21.10 rules = [
21.11 \<^rule_thm>\<open>tausche_plus\<close>, (*"b kleiner a ==> (b + a) = (a + b)"*)
21.12 @@ -206,7 +206,7 @@
21.13
21.14 val fasse_zusammen =
21.15 Rule_Def.Repeat{id = "fasse_zusammen", preconds = [],
21.16 - rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
21.17 + rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
21.18 erls = Rule_Set.append_rules "erls_fasse_zusammen" Rule_Set.empty
21.19 [\<^rule_eval>\<open>Prog_Expr.is_num\<close> (Prog_Expr.eval_is_num "#is_num_")],
21.20 srls = Rule_Set.Empty, calc = [], errpatts = [],
21.21 @@ -248,7 +248,7 @@
21.22
21.23 val verschoenere =
21.24 Rule_Def.Repeat{id = "verschoenere", preconds = [],
21.25 - rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), srls = Rule_Set.Empty, calc = [], errpatts = [],
21.26 + rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), srls = Rule_Set.Empty, calc = [], errpatts = [],
21.27 erls = Rule_Set.append_rules "erls_verschoenere" Rule_Set.empty
21.28 [\<^rule_eval>\<open>PolyMinus.kleiner\<close> (eval_kleiner "")],
21.29 rules = [
21.30 @@ -268,7 +268,7 @@
21.31
21.32 val klammern_aufloesen =
21.33 Rule_Def.Repeat{id = "klammern_aufloesen", preconds = [],
21.34 - rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), srls = Rule_Set.Empty,
21.35 + rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), srls = Rule_Set.Empty,
21.36 calc = [], errpatts = [], erls = Rule_Set.Empty,
21.37 rules = [
21.38 \<^rule_thm_sym>\<open>add.assoc\<close>, (*"a + (b + c) = (a + b) + c"*)
21.39 @@ -279,7 +279,7 @@
21.40
21.41 val klammern_ausmultiplizieren =
21.42 Rule_Def.Repeat{id = "klammern_ausmultiplizieren", preconds = [],
21.43 - rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), srls = Rule_Set.Empty,
21.44 + rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), srls = Rule_Set.Empty,
21.45 calc = [], errpatts = [], erls = Rule_Set.Empty,
21.46 rules = [
21.47 \<^rule_thm>\<open>distrib_right\<close>, (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
21.48 @@ -291,7 +291,7 @@
21.49
21.50 val ordne_monome =
21.51 Rule_Def.Repeat {
21.52 - id = "ordne_monome", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
21.53 + id = "ordne_monome", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
21.54 srls = Rule_Set.Empty, calc = [], errpatts = [],
21.55 erls = Rule_Set.append_rules "erls_ordne_monome" Rule_Set.empty [
21.56 \<^rule_eval>\<open>PolyMinus.kleiner\<close> (eval_kleiner ""),
22.1 --- a/src/Tools/isac/Knowledge/Rational.thy Wed Aug 03 18:17:27 2022 +0200
22.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Thu Aug 04 12:48:37 2022 +0200
22.3 @@ -409,7 +409,7 @@
22.4 (* evaluates conditions in calculate_Rational *)
22.5 val calc_rat_erls =
22.6 prep_rls'
22.7 - (Rule_Def.Repeat {id = "calc_rat_erls", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
22.8 + (Rule_Def.Repeat {id = "calc_rat_erls", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
22.9 erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
22.10 rules = [
22.11 \<^rule_eval>\<open>matches\<close> (Prog_Expr.eval_matches "#matches_"),
22.12 @@ -424,7 +424,7 @@
22.13 need to have constants to be commuted together respectively *)
22.14 val calculate_Rational =
22.15 prep_rls' (Rule_Set.merge "calculate_Rational"
22.16 - (Rule_Def.Repeat {id = "divide", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
22.17 + (Rule_Def.Repeat {id = "divide", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
22.18 erls = calc_rat_erls, srls = Rule_Set.Empty,
22.19 calc = [], errpatts = [],
22.20 rules = [
22.21 @@ -606,7 +606,7 @@
22.22 (*.all powers over + distributed; atoms over * collected, other distributed
22.23 contains absolute minimum of thms for context in norm_Rational .*)
22.24 val powers = prep_rls'(
22.25 - Rule_Def.Repeat {id = "powers", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
22.26 + Rule_Def.Repeat {id = "powers", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.function_empty),
22.27 erls = powers_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
22.28 rules = [
22.29 \<^rule_thm>\<open>realpow_multI\<close>, (*"(r * s) \<up> n = r \<up> n * s \<up> n"*)
22.30 @@ -630,7 +630,7 @@
22.31 (*.contains absolute minimum of thms for context in norm_Rational.*)
22.32 val rat_mult_divide = prep_rls'(
22.33 Rule_Def.Repeat {id = "rat_mult_divide", preconds = [],
22.34 - rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
22.35 + rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
22.36 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
22.37 rules = [
22.38 \<^rule_thm>\<open>rat_mult\<close>, (*(1)"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)
22.39 @@ -647,7 +647,7 @@
22.40 \<close> ML \<open>
22.41 (*.contains absolute minimum of thms for context in norm_Rational.*)
22.42 val reduce_0_1_2 = prep_rls'(
22.43 - Rule_Def.Repeat{id = "reduce_0_1_2", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
22.44 + Rule_Def.Repeat{id = "reduce_0_1_2", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
22.45 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
22.46 rules = [
22.47 \<^rule_thm>\<open>div_by_1\<close>, (*"?x / 1 = ?x"*)
22.48 @@ -670,7 +670,7 @@
22.49 (*erls for calculate_Rational;
22.50 make local with FIXX@ME result:term *term list WN0609???SKMG*)
22.51 val norm_rat_erls = prep_rls'(
22.52 - Rule_Def.Repeat {id = "norm_rat_erls", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
22.53 + Rule_Def.Repeat {id = "norm_rat_erls", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.function_empty),
22.54 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
22.55 rules = [
22.56 \<^rule_eval>\<open>Prog_Expr.is_num\<close> (Prog_Expr.eval_is_num "#is_num_")
22.57 @@ -683,7 +683,7 @@
22.58 which is now replaced by MGs version "norm_Rational" below
22.59 *)
22.60 val norm_Rational_min = prep_rls'(
22.61 - Rule_Def.Repeat {id = "norm_Rational_min", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
22.62 + Rule_Def.Repeat {id = "norm_Rational_min", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.function_empty),
22.63 erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
22.64 rules = [(*sequence given by operator precedence*)
22.65 Rule.Rls_ discard_minus,
22.66 @@ -701,7 +701,7 @@
22.67 \<close> ML \<open>
22.68 val norm_Rational_parenthesized = prep_rls'(
22.69 Rule_Set.Sequence {id = "norm_Rational_parenthesized", preconds = []:term list,
22.70 - rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
22.71 + rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
22.72 erls = Atools_erls, srls = Rule_Set.Empty,
22.73 calc = [], errpatts = [],
22.74 rules = [
22.75 @@ -723,7 +723,7 @@
22.76 \<^rule_thm>\<open>divide_minus1\<close> (*"?x / -1 = - ?x"*)]);
22.77
22.78 val add_fractions_p_rls = prep_rls'(
22.79 - Rule_Def.Repeat {id = "add_fractions_p_rls", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
22.80 + Rule_Def.Repeat {id = "add_fractions_p_rls", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
22.81 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
22.82 rules = [Rule.Rls_ add_fractions_p],
22.83 scr = Rule.Empty_Prog});
22.84 @@ -731,7 +731,7 @@
22.85 (* "Rule_Def.Repeat" causes repeated application of cancel_p to one and the same term *)
22.86 val cancel_p_rls = prep_rls'(
22.87 Rule_Def.Repeat
22.88 - {id = "cancel_p_rls", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
22.89 + {id = "cancel_p_rls", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
22.90 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
22.91 rules = [Rule.Rls_ cancel_p],
22.92 scr = Rule.Empty_Prog});
22.93 @@ -739,7 +739,7 @@
22.94 (*. makes 'normal' fractions; 'is_polyexp' inhibits double fractions;
22.95 used in initial part norm_Rational_mg, see example DA-M02-main.p.60.*)
22.96 val rat_mult_poly = prep_rls'(
22.97 - Rule_Def.Repeat {id = "rat_mult_poly", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
22.98 + Rule_Def.Repeat {id = "rat_mult_poly", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
22.99 erls = Rule_Set.append_rules "Rule_Set.empty-is_polyexp" Rule_Set.empty [
22.100 \<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp "")],
22.101 srls = Rule_Set.Empty, calc = [], errpatts = [],
22.102 @@ -754,7 +754,7 @@
22.103 I.E. THE RESPECTIVE ASSUMPTION IS STORED AND Rule.Thm APPLIED; WN051028
22.104 ... WN0609???MG.*)
22.105 val rat_mult_div_pow = prep_rls'(
22.106 - Rule_Def.Repeat {id = "rat_mult_div_pow", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
22.107 + Rule_Def.Repeat {id = "rat_mult_div_pow", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.function_empty),
22.108 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
22.109 rules = [
22.110 \<^rule_thm>\<open>rat_mult\<close>, (*"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)
22.111 @@ -770,7 +770,7 @@
22.112 scr = Rule.Empty_Prog});
22.113
22.114 val rat_reduce_1 = prep_rls'(
22.115 - Rule_Def.Repeat {id = "rat_reduce_1", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
22.116 + Rule_Def.Repeat {id = "rat_reduce_1", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
22.117 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
22.118 rules = [
22.119 \<^rule_thm>\<open>div_by_1\<close>, (*"?x / 1 = ?x"*)
22.120 @@ -779,7 +779,7 @@
22.121
22.122 (* looping part of norm_Rational *)
22.123 val norm_Rational_rls = prep_rls' (
22.124 - Rule_Def.Repeat {id = "norm_Rational_rls", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
22.125 + Rule_Def.Repeat {id = "norm_Rational_rls", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.function_empty),
22.126 erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
22.127 rules = [
22.128 Rule.Rls_ add_fractions_p_rls,
22.129 @@ -791,7 +791,7 @@
22.130
22.131 val norm_Rational = prep_rls' (
22.132 Rule_Set.Sequence
22.133 - {id = "norm_Rational", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
22.134 + {id = "norm_Rational", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
22.135 erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
22.136 rules = [
22.137 Rule.Rls_ discard_minus,
23.1 --- a/src/Tools/isac/Knowledge/Test.thy Wed Aug 03 18:17:27 2022 +0200
23.2 +++ b/src/Tools/isac/Knowledge/Test.thy Thu Aug 04 12:48:37 2022 +0200
23.3 @@ -439,7 +439,7 @@
23.4 val rearrange_assoc =
23.5 Rule_Def.Repeat{
23.6 id = "rearrange_assoc", preconds = [],
23.7 - rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord),
23.8 + rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty),
23.9 erls = Rule_Set.empty, srls = Rule_Set.empty, calc = [], errpatts = [],
23.10 rules = [
23.11 \<^rule_thm_sym>\<open>add.assoc\<close>,
23.12 @@ -461,7 +461,7 @@
23.13
23.14 (*todo: replace by Rewrite("rnorm_equation_add", @{thm rnorm_equation_add)*)
23.15 val norm_equation =
23.16 - Rule_Def.Repeat{id = "norm_equation", preconds = [], rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord),
23.17 + Rule_Def.Repeat{id = "norm_equation", preconds = [], rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty),
23.18 erls = tval_rls, srls = Rule_Set.empty, calc = [], errpatts = [],
23.19 rules = [
23.20 \<^rule_thm>\<open>rnorm_equation_add\<close>],
23.21 @@ -525,7 +525,7 @@
23.22 ML \<open>
23.23 (*isolate the root in a root-equation*)
23.24 val isolate_root =
23.25 - Rule_Def.Repeat{id = "isolate_root", preconds = [], rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord),
23.26 + Rule_Def.Repeat{id = "isolate_root", preconds = [], rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty),
23.27 erls=tval_rls,srls = Rule_Set.empty, calc=[], errpatts = [],
23.28 rules = [
23.29 \<^rule_thm>\<open>rroot_to_lhs\<close>,
23.30 @@ -539,7 +539,7 @@
23.31 (*isolate the bound variable in an equation; 'bdv' is a meta-constant*)
23.32 val isolate_bdv =
23.33 Rule_Def.Repeat{
23.34 - id = "isolate_bdv", preconds = [], rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord),
23.35 + id = "isolate_bdv", preconds = [], rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty),
23.36 erls=tval_rls,srls = Rule_Set.empty, calc= [], errpatts = [],
23.37 rules = [
23.38 \<^rule_thm>\<open>risolate_bdv_add\<close>,
23.39 @@ -777,7 +777,7 @@
23.40 in
23.41 [e_e])"
23.42 method met_test_solvelin : "Test/solve_linear" =
23.43 - \<open>{rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule_Set.empty,
23.44 + \<open>{rew_ord' = "Rewrite_Ord.id_empty", rls' = tval_rls, srls = Rule_Set.empty,
23.45 prls = assoc_rls' @{theory} "matches", calc = [], crls = tval_rls, errpats = [],
23.46 nrls = Test_simplify}\<close>
23.47 Program: solve_linear.simps
23.48 @@ -808,7 +808,7 @@
23.49
23.50 method met_test_sqrt : "Test/sqrt-equ-test" =
23.51 (*root-equation, version for tests before 8.01.01*)
23.52 - \<open>{rew_ord'="e_rew_ord",rls'=tval_rls,
23.53 + \<open>{rew_ord'="Rewrite_Ord.id_empty",rls'=tval_rls,
23.54 srls = Rule_Set.append_rules "srls_contains_root" Rule_Set.empty
23.55 [\<^rule_eval>\<open>contains_root\<close> (eval_contains_root "")],
23.56 prls = Rule_Set.append_rules "prls_contains_root" Rule_Set.empty
23.57 @@ -834,7 +834,7 @@
23.58
23.59 method met_test_squ_sub : "Test/squ-equ-test-subpbl1" =
23.60 (*tests subproblem fixed linear*)
23.61 - \<open>{rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule_Set.empty,
23.62 + \<open>{rew_ord' = "Rewrite_Ord.id_empty", rls' = tval_rls, srls = Rule_Set.empty,
23.63 prls = Rule_Set.append_rules "prls_met_test_squ_sub" Rule_Set.empty
23.64 [\<^rule_eval>\<open>precond_rootmet\<close> (eval_precond_rootmet "")],
23.65 calc=[], crls=tval_rls, errpats = [], nrls = Test_simplify}\<close>
23.66 @@ -864,7 +864,7 @@
23.67
23.68 method met_test_eq1 : "Test/square_equation1" =
23.69 (*root-equation1:*)
23.70 - \<open>{rew_ord'="e_rew_ord",rls'=tval_rls,
23.71 + \<open>{rew_ord'="Rewrite_Ord.id_empty",rls'=tval_rls,
23.72 srls = Rule_Set.append_rules "srls_contains_root" Rule_Set.empty
23.73 [\<^rule_eval>\<open>contains_root\<close> (eval_contains_root"")],
23.74 prls=Rule_Set.empty, calc=[], crls=tval_rls, errpats = [], nrls = Rule_Set.empty}\<close>
23.75 @@ -894,7 +894,7 @@
23.76
23.77 method met_test_squ2 : "Test/square_equation2" =
23.78 (*root-equation2*)
23.79 - \<open>{rew_ord'="e_rew_ord",rls'=tval_rls,
23.80 + \<open>{rew_ord'="Rewrite_Ord.id_empty",rls'=tval_rls,
23.81 srls = Rule_Set.append_rules "srls_contains_root" Rule_Set.empty
23.82 [\<^rule_eval>\<open>contains_root\<close> (eval_contains_root"")],
23.83 prls=Rule_Set.empty,calc=[], crls=tval_rls, errpats = [], nrls = Rule_Set.empty}\<close>
23.84 @@ -924,7 +924,7 @@
23.85
23.86 method met_test_squeq : "Test/square_equation" =
23.87 (*root-equation*)
23.88 - \<open>{rew_ord'="e_rew_ord",rls'=tval_rls,
23.89 + \<open>{rew_ord'="Rewrite_Ord.id_empty",rls'=tval_rls,
23.90 srls = Rule_Set.append_rules "srls_contains_root" Rule_Set.empty
23.91 [\<^rule_eval>\<open>contains_root\<close> (eval_contains_root"")],
23.92 prls=Rule_Set.empty,calc=[], crls=tval_rls, errpats = [], nrls = Rule_Set.empty}\<close>
23.93 @@ -947,7 +947,7 @@
23.94
23.95 method met_test_eq_plain : "Test/solve_plain_square" =
23.96 (*solve_plain_square*)
23.97 - \<open>{rew_ord'="e_rew_ord",rls'=tval_rls,calc=[],srls=Rule_Set.empty,
23.98 + \<open>{rew_ord'="Rewrite_Ord.id_empty",rls'=tval_rls,calc=[],srls=Rule_Set.empty,
23.99 prls = assoc_rls' @{theory} "matches", crls=tval_rls, errpats = [], nrls = Rule_Set.empty(*,
23.100 asm_rls=[],asm_thm=[]*)}\<close>
23.101 Program: solve_plain_square.simps
23.102 @@ -974,7 +974,7 @@
23.103 [''no_met'']) [BOOL e_e, REAL v_v])"
23.104
23.105 method met_test_norm_univ : "Test/norm_univar_equation" =
23.106 - \<open>{rew_ord'="e_rew_ord",rls'=tval_rls,srls = Rule_Set.empty,prls=Rule_Set.empty, calc=[], crls=tval_rls,
23.107 + \<open>{rew_ord'="Rewrite_Ord.id_empty",rls'=tval_rls,srls = Rule_Set.empty,prls=Rule_Set.empty, calc=[], crls=tval_rls,
23.108 errpats = [], nrls = Rule_Set.empty}\<close>
23.109 Program: norm_univariate_equ.simps
23.110 Given: "equality e_e" "solveFor v_v"
23.111 @@ -992,7 +992,7 @@
23.112 (Try (Calculate ''TIMES''))) t_t)"
23.113
23.114 method met_test_intsimp : "Test/intsimp" =
23.115 - \<open>{rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule_Set.empty, prls = Rule_Set.empty, calc = [],
23.116 + \<open>{rew_ord' = "Rewrite_Ord.id_empty", rls' = tval_rls, srls = Rule_Set.empty, prls = Rule_Set.empty, calc = [],
23.117 crls = tval_rls, errpats = [], nrls = Test_simplify}\<close>
23.118 Program: test_simplify.simps
23.119 Given: "intTestGiven t_t"
24.1 --- a/src/Tools/isac/MathEngBasic/method.sml Wed Aug 03 18:17:27 2022 +0200
24.2 +++ b/src/Tools/isac/MathEngBasic/method.sml Thu Aug 04 12:48:37 2022 +0200
24.3 @@ -42,7 +42,7 @@
24.4 (* a subset of MethodC.T record's fields *)
24.5 type input =
24.6 {calc: Rule_Def.calc list, crls: Rule_Set.T, errpats: Error_Pattern_Def.T list, nrls: Rule_Set.T,
24.7 - prls: Rule_Set.T, rew_ord': Rewrite_Ord.rew_ord', rls': Rule_Set.T, srls: Rule_Set.T}
24.8 + prls: Rule_Set.T, rew_ord': Rewrite_Ord.id, rls': Rule_Set.T, srls: Rule_Set.T}
24.9
24.10 fun prep_input thy guh (mathauthors: string list) (init: References_Def.id)
24.11 (metID, ppc,
25.1 --- a/src/Tools/isac/MathEngBasic/rewrite.sml Wed Aug 03 18:17:27 2022 +0200
25.2 +++ b/src/Tools/isac/MathEngBasic/rewrite.sml Thu Aug 04 12:48:37 2022 +0200
25.3 @@ -10,19 +10,19 @@
25.4 val eval_prog_expr: Proof.context -> Rule_Set.T -> term -> term
25.5 val eval_true_: Proof.context -> Rule_Set.T -> term -> bool
25.6 val eval_true: Proof.context -> term list -> Rule_Set.T -> bool
25.7 - val rew_sub: Proof.context -> int -> Subst.T -> Rule_Def.rew_ord_
25.8 + val rew_sub: Proof.context -> int -> Subst.T -> Rewrite_Ord.function
25.9 -> Rule_Set.T -> bool -> TermC.path -> term -> term -> term * term list * TermC.path * bool
25.10 - val rewrite_: Proof.context -> Rule_Def.rew_ord_ -> Rule_Set.T -> bool -> thm ->
25.11 + val rewrite_: Proof.context -> Rewrite_Ord.function -> Rule_Set.T -> bool -> thm ->
25.12 term -> (term * term list) option
25.13 - val rewrite_inst_: Proof.context -> Rule_Def.rew_ord_ -> Rule_Set.T -> bool
25.14 + val rewrite_inst_: Proof.context -> Rewrite_Ord.function -> Rule_Set.T -> bool
25.15 -> Subst.T -> thm -> term -> (term * term list) option
25.16 val rewrite_set_: Proof.context -> bool -> Rule_Set.T -> term -> (term * term list) option
25.17 val rewrite_set_inst_: Proof.context -> bool -> Subst.T -> Rule_Set.T -> term -> (term * term list) option
25.18 - val rewrite_terms_: Proof.context -> Rule_Def.rew_ord_ -> Rule_Set.T -> term list
25.19 + val rewrite_terms_: Proof.context -> Rewrite_Ord.function -> Rule_Set.T -> term list
25.20 -> term -> (term * term list) option
25.21
25.22 \<^isac_test>\<open>
25.23 - val rewrite__: Proof.context -> int -> Subst.T -> Rule_Def.rew_ord_ ->
25.24 + val rewrite__: Proof.context -> int -> Subst.T -> Rewrite_Ord.function ->
25.25 Rule_Set.T -> bool -> thm -> term -> (term * term list) option
25.26 val rewrite__set_: Proof.context -> int -> bool -> Subst.T -> Rule_Set.T -> term -> (term * term list) option
25.27 val app_rev: Proof.context -> int -> Rule_Set.T -> term -> term * term list * bool
25.28 @@ -287,7 +287,7 @@
25.29 case Eval.adhoc_thm (Proof_Context.theory_of ctxt) isa_fn t of
25.30 NONE => NONE
25.31 | SOME (thmID, thm) =>
25.32 - (let val rew = case rewrite_ ctxt Rewrite_Ord.dummy_ord Rule_Set.empty false thm t of
25.33 + (let val rew = case rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.empty false thm t of
25.34 SOME (rew, _) => rew
25.35 | NONE => raise ERROR (msg "calculate_" ctxt id thm t)
25.36 in SOME (rew, (thmID, thm)) end)
26.1 --- a/src/Tools/isac/MathEngBasic/state-steps.sml Wed Aug 03 18:17:27 2022 +0200
26.2 +++ b/src/Tools/isac/MathEngBasic/state-steps.sml Thu Aug 04 12:48:37 2022 +0200
26.3 @@ -12,7 +12,7 @@
26.4 type T
26.5 val to_string : T -> string
26.6 val result : single -> (term * term list)
26.7 - val make_single: Rewrite_Ord.rew_ord' * 'a -> Rule_Set.T -> term * Rule.rule * (term * term list) ->
26.8 + val make_single: Rewrite_Ord.id * 'a -> Rule_Set.T -> term * Rule.rule * (term * term list) ->
26.9 single
26.10 val insert_pos : Pos.pos -> T -> T
26.11 end
27.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml Wed Aug 03 18:17:27 2022 +0200
27.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml Thu Aug 04 12:48:37 2022 +0200
27.3 @@ -28,12 +28,12 @@
27.4 | Empty_Tac_
27.5 | Free_Solve'
27.6 | Or_to_List' of term * term
27.7 - | Rewrite' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * ThmC.T * term * Celem.result
27.8 - | Rewrite_Inst' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * subst * ThmC.T * term * Celem.result
27.9 + | Rewrite' of ThyC.id * Rewrite_Ord.id * Rule_Set.T * bool * ThmC.T * term * Celem.result
27.10 + | Rewrite_Inst' of ThyC.id * Rewrite_Ord.id * Rule_Set.T * bool * subst * ThmC.T * term * Celem.result
27.11 | Rewrite_Set' of ThyC.id * bool * Rule_Set.T * term * Celem.result
27.12 | Rewrite_Set_Inst' of ThyC.id * bool * subst * Rule_Set.T * term * Celem.result
27.13 | Subproblem' of References_Def.T * Model_Def.o_model * term * Model_Def.form_model * Proof.context * term
27.14 - | Substitute' of Rule_Def.rew_ord_ * Rule_Set.T * Subst.as_eqs * term * term
27.15 + | Substitute' of Rewrite_Ord.function * Rule_Set.T * Subst.as_eqs * term * term
27.16 (*RM*)| Tac_ of theory * string * string * string
27.17 | Take' of term
27.18 | End_Detail' of Celem.result
27.19 @@ -240,7 +240,7 @@
27.20
27.21 (* try if a rewrite-rule is applicable to a given formula;
27.22 in case of rule-sets (recursivley) collect all _atomic_ rewrites *)
27.23 -fun try_rew ctxt ((_, ro) : Rewrite_Ord.rew_ord) erls (subst : subst) f (thm' as Rule.Thm (_, thm)) =
27.24 +fun try_rew ctxt ((_, ro) : Rewrite_Ord.T) erls (subst : subst) f (thm' as Rule.Thm (_, thm)) =
27.25 if Auto_Prog.contains_bdv thm
27.26 then case Rewrite.rewrite_inst_ ctxt ro erls false subst thm f of
27.27 SOME _ => [rule2tac ctxt subst thm']
27.28 @@ -268,7 +268,7 @@
27.29 (* decide if a tactic is applicable to a given formula;
27.30 in case of Rewrite_Set* go down to _atomic_ rewrite-tactics *)
27.31 fun applicable ctxt _ _ f (Calculate scrID) =
27.32 - try_rew ctxt Rewrite_Ord.e_rew_ordX Rule_Set.empty [] f
27.33 + try_rew ctxt Rewrite_Ord.empty Rule_Set.empty [] f
27.34 (Rule.Eval (assoc_calc' (Proof_Context.theory_of ctxt) scrID |> snd))
27.35 | applicable ctxt ro erls f (Rewrite thm'') =
27.36 try_rew ctxt (ro, assoc_rew_ord (Proof_Context.theory_of ctxt) ro) erls [] f (Rule.Thm thm'')
27.37 @@ -325,8 +325,8 @@
27.38 | Empty_Tac_
27.39 | Free_Solve'
27.40 | Or_to_List' of term * term
27.41 - | Rewrite' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * ThmC.T * term * Celem.result
27.42 - | Rewrite_Inst' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * subst * ThmC.T * term * Celem.result
27.43 + | Rewrite' of ThyC.id * Rewrite_Ord.id * Rule_Set.T * bool * ThmC.T * term * Celem.result
27.44 + | Rewrite_Inst' of ThyC.id * Rewrite_Ord.id * Rule_Set.T * bool * subst * ThmC.T * term * Celem.result
27.45 | Rewrite_Set' of ThyC.id * bool * Rule_Set.T * term * Celem.result
27.46 | Rewrite_Set_Inst' of ThyC.id * bool * subst * Rule_Set.T * term * Celem.result
27.47 | Subproblem' of (* switch from solve-phase to specify-phase *)
27.48 @@ -337,7 +337,7 @@
27.49 Proof.context * (* for the specify-phase *)
27.50 term (* Subproblem (thyID, pbl) OR CAS_Cmd *)
27.51 | Substitute' of (* substitute variables (TODO: from the context) *)
27.52 - Rule_Def.rew_ord_ *(* for re-calculation *)
27.53 + Rewrite_Ord.function *(* for re-calculation *)
27.54 Rule_Set.T * (* for re-calculation *)
27.55 Subst.as_eqs * (* the substitution: terms of type bool *)
27.56 term * (* to be substituted into *)
28.1 --- a/src/Tools/isac/ProgLang/ListC.thy Wed Aug 03 18:17:27 2022 +0200
28.2 +++ b/src/Tools/isac/ProgLang/ListC.thy Thu Aug 04 12:48:37 2022 +0200
28.3 @@ -131,7 +131,7 @@
28.4 ML \<open>
28.5 \<close> ML \<open>
28.6 val prog_expr =
28.7 - Rule_Def.Repeat {id = "prog_expr", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
28.8 + Rule_Def.Repeat {id = "prog_expr", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
28.9 erls = Rule_Def.Empty, srls = Rule_Def.Empty, calc = [], errpatts = [],
28.10 rules = [Rule_Def.Thm ("refl", @{thm refl}), (*'a<>b -> FALSE' by fun eval_equal*)
28.11 Rule_Def.Thm ("o_apply", @{thm o_apply}),
29.1 --- a/src/Tools/isac/ProgLang/Prog_Expr.thy Wed Aug 03 18:17:27 2022 +0200
29.2 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy Thu Aug 04 12:48:37 2022 +0200
29.3 @@ -263,13 +263,13 @@
29.4 > reflI;
29.5 val it = "(?t = ?t) = True"
29.6 > val t = str2term "x = 0";
29.7 -> val NONE = rewrite_ thy Rewrite_Ord.dummy_ord Rule_Set.empty false reflI t;
29.8 +> val NONE = rewrite_ thy Rewrite_Ord.function_empty Rule_Set.empty false reflI t;
29.9
29.10 > val t = str2term "1 = 0";
29.11 -> val NONE = rewrite_ thy Rewrite_Ord.dummy_ord Rule_Set.empty false reflI t;
29.12 +> val NONE = rewrite_ thy Rewrite_Ord.function_empty Rule_Set.empty false reflI t;
29.13 ----------- thus needs Rule.Eval !
29.14 > val t = str2term "0 = 0";
29.15 -> val SOME (t',_) = rewrite_ thy Rewrite_Ord.dummy_ord Rule_Set.empty false reflI t;
29.16 +> val SOME (t',_) = rewrite_ thy Rewrite_Ord.function_empty Rule_Set.empty false reflI t;
29.17 > UnparseC.term t';
29.18 val it = \<^const_name>\<open>True\<close>
29.19
30.1 --- a/src/Tools/isac/TODO.thy Wed Aug 03 18:17:27 2022 +0200
30.2 +++ b/src/Tools/isac/TODO.thy Thu Aug 04 12:48:37 2022 +0200
30.3 @@ -274,7 +274,7 @@
30.4 \item Diff.thy: differentiateX --> differentiate after removal of script-constant
30.5 \item Test.thy: met_test_sqrt2: deleted?!
30.6 \item xxx
30.7 - \item Rewrite_Ord.rew_ord' := overwritel (! Rewrite_Ord.rew_ord', (*<<<---- use Know_Store.xxx, too*)
30.8 + \item Rewrite_Ord.id := overwritel (! Rewrite_Ord.id, (*<<<---- use Know_Store.xxx, too*)
30.9 \item xxx
30.10 \item automatically extrac rls from program-code
30.11 ? take ["SignalProcessing", "Z_Transform", "Inverse_sub"] as an example ?
31.1 --- a/test/Tools/isac/Interpret/error-pattern.sml Wed Aug 03 18:17:27 2022 +0200
31.2 +++ b/test/Tools/isac/Interpret/error-pattern.sml Thu Aug 04 12:48:37 2022 +0200
31.3 @@ -909,7 +909,7 @@
31.4 val (res, inf) = (TermC.str2term "(2 + 3)/(3 + 4)", TermC.str2term "1 / 2");
31.5
31.6 val (res', _, _, rewritten) = (*rewritten: the lhs of the pattern TermC.matches in res*)
31.7 - rew_sub ctxt 1 [] e_rew_ord Rule_Set.empty false [] (HOLogic.Trueprop $ pat) res;
31.8 + rew_sub ctxt 1 [] Rewrite_Ord.function_empty Rule_Set.empty false [] (HOLogic.Trueprop $ pat) res;
31.9 if rewritten then NONE else SOME "e_errpatID";
31.10
31.11 val norm_res = case rewrite_set_ ctxt false rls res' of
31.12 @@ -957,7 +957,7 @@
31.13 val (res, inf) = (TermC.str2term "2 * x + d_d x (sin (x \<up> 4))", TermC.str2term "2 * x + cos (4 * x \<up> 3)");
31.14
31.15 val (res', _, _, rewritten) = (*rewritten: the lhs of the pattern TermC.matches in res*)
31.16 - rew_sub ctxt 1 subst e_rew_ord Rule_Set.empty false [] (HOLogic.Trueprop $ pat) res;
31.17 + rew_sub ctxt 1 subst Rewrite_Ord.function_empty Rule_Set.empty false [] (HOLogic.Trueprop $ pat) res;
31.18 if UnparseC.term res' = "2 * x + cos (d_d x (x \<up> 4))" andalso rewritten then ()
31.19 else error "build fun check_for' ?bdv changed 2";
31.20
31.21 @@ -1119,7 +1119,7 @@
31.22 val ((subs_opt, subst), (thm, form), errpatID, (fillpatID, pat, erpaID)) =
31.23 (subst, (thm, form), errpatID, hd (*simulate beginning of "map"*) fillpats);
31.24 val (form', _, _, rewritten) =
31.25 - rew_sub ctxt 1 subst e_rew_ord Rule_Set.empty false [] (HOLogic.Trueprop $ pat) form;
31.26 + rew_sub ctxt 1 subst Rewrite_Ord.function_empty Rule_Set.empty false [] (HOLogic.Trueprop $ pat) form;
31.27
31.28 if UnparseC.term form' = "d_d x (x \<up> 2) + cos (x \<up> 4) * d_d x ?_dummy_1" then ()
31.29 else error "find_fill_patterns changed 3";
32.1 --- a/test/Tools/isac/Knowledge/algein.sml Wed Aug 03 18:17:27 2022 +0200
32.2 +++ b/test/Tools/isac/Knowledge/algein.sml Thu Aug 04 12:48:37 2022 +0200
32.3 @@ -99,7 +99,7 @@
32.4 "----------- Widerspruch 3 = 777 ---------------------------------";
32.5 val thy = @{theory "Isac_Knowledge"};
32.6 val ctxt = Proof_Context.init_global thy;
32.7 -val rew_ord = dummy_ord;
32.8 +val rew_ord = Rewrite_Ord.function_empty;
32.9 val erls = Rule_Set.Empty;
32.10 val thm = ThmC.thm_from_thy thy "sym_mult_zero_right";
32.11 val t = TermC.str2term "0 = (0::real)";
33.1 --- a/test/Tools/isac/Knowledge/diophanteq.sml Wed Aug 03 18:17:27 2022 +0200
33.2 +++ b/test/Tools/isac/Knowledge/diophanteq.sml Thu Aug 04 12:48:37 2022 +0200
33.3 @@ -33,7 +33,7 @@
33.4 SOME t' => t'
33.5 | NONE => error "diophanteq.sml: syntax error in rewriting for usecase1";
33.6
33.7 -val SOME (t,_) = rewrite_inst_ ctxt e_rew_ord Rule_Set.empty true subst
33.8 +val SOME (t,_) = rewrite_inst_ ctxt Rewrite_Ord.function_empty Rule_Set.empty true subst
33.9 @{thm "int_isolate_add"} t; UnparseC.term t;
33.10
33.11 val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"TIMES"))) t;
34.1 --- a/test/Tools/isac/Knowledge/eqsystem-1.sml Wed Aug 03 18:17:27 2022 +0200
34.2 +++ b/test/Tools/isac/Knowledge/eqsystem-1.sml Thu Aug 04 12:48:37 2022 +0200
34.3 @@ -221,7 +221,7 @@
34.4 val e2__ = TermC.str2term "L * c + c_2 = q_0 * L \<up> 2 / 2";
34.5 val bdvs = [(TermC.str2term"bdv_1",TermC.str2term"c"),
34.6 (TermC.str2term"bdv_2",TermC.str2term"c_2")];
34.7 -val SOME (e2__,_) = rewrite_terms_ ctxt dummy_ord Rule_Set.Empty [e1__] e2__;
34.8 +val SOME (e2__,_) = rewrite_terms_ ctxt Rewrite_Ord.function_empty Rule_Set.Empty [e1__] e2__;
34.9 if UnparseC.term e2__ = "L * c + 77 = q_0 * L \<up> 2 / 2" then ()
34.10 else error "eqsystem.sml top_down_substitution,2x2] subst";
34.11
35.1 --- a/test/Tools/isac/Knowledge/eqsystem-2.sml Wed Aug 03 18:17:27 2022 +0200
35.2 +++ b/test/Tools/isac/Knowledge/eqsystem-2.sml Thu Aug 04 12:48:37 2022 +0200
35.3 @@ -207,9 +207,9 @@
35.4 "0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2, " ^
35.5 "0 = c_4, " ^
35.6 "0 = c_3]");
35.7 -val SOME (t,_) = rewrite_ ctxt e_rew_ord Rule_Set.empty false @{thm commute_0_equality} t;
35.8 -val SOME (t,_) = rewrite_ ctxt e_rew_ord Rule_Set.empty false @{thm commute_0_equality} t;
35.9 -val SOME (t,_) = rewrite_ ctxt e_rew_ord Rule_Set.empty false @{thm commute_0_equality} t;
35.10 +val SOME (t,_) = rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.empty false @{thm commute_0_equality} t;
35.11 +val SOME (t,_) = rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.empty false @{thm commute_0_equality} t;
35.12 +val SOME (t,_) = rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.empty false @{thm commute_0_equality} t;
35.13 if UnparseC.term t =
35.14 "[L * q_0 = c, (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2 = 0,\n c_4 = 0, c_3 = 0]"
35.15 then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 1";
36.1 --- a/test/Tools/isac/Knowledge/poly-1.sml Wed Aug 03 18:17:27 2022 +0200
36.2 +++ b/test/Tools/isac/Knowledge/poly-1.sml Thu Aug 04 12:48:37 2022 +0200
36.3 @@ -470,7 +470,7 @@
36.4
36.5 "----- eval_is_multUnordered ---";
36.6 val tm = TermC.str2term "(5 * x \<up> 2 * (2 * x \<up> 7) + 5 * x \<up> 2 * 3 + (6 * x \<up> 7 + 9) + (- 1 * (3 * x \<up> 5 * (6 * x \<up> 4)) + - 1 * (3 * x \<up> 5 * - 1) + (-48 * x \<up> 4 + 8))) is_multUnordered";
36.7 -case eval_is_multUnordered "testid" "" tm thy of
36.8 +case eval_is_multUnordered "testid" "" tm @{context} of
36.9 SOME (_, Const (\<^const_name>\<open>Trueprop\<close>, _) $
36.10 (Const (\<^const_name>\<open>HOL.eq\<close>, _) $
36.11 (Const (\<^const_name>\<open>is_multUnordered\<close>, _) $ _) $
36.12 @@ -492,7 +492,7 @@
36.13 (*+*) andalso not (is_multUnordered arg)
36.14 (*+*)then () else error "sort_variables 3 * a + - 2 * a CHANGED";
36.15
36.16 -case eval_is_multUnordered "xxx " "yyy " t thy of
36.17 +case eval_is_multUnordered "xxx " "yyy " t @{context} of
36.18 SOME
36.19 ("xxx 3 * a + - 2 * a_",
36.20 Const (\<^const_name>\<open>Trueprop\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $
36.21 @@ -507,7 +507,7 @@
36.22 (*+*) andalso not (is_multUnordered arg)
36.23 (*+*)then () else error "sort_variables - 2 * a CHANGED";
36.24
36.25 -case eval_is_multUnordered "xxx " "yyy " t thy of
36.26 +case eval_is_multUnordered "xxx " "yyy " t @{context} of
36.27 SOME
36.28 ("xxx - 2 * a_",
36.29 Const (\<^const_name>\<open>Trueprop\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $
36.30 @@ -521,7 +521,7 @@
36.31 (*+*) andalso not (is_multUnordered arg)
36.32 (*+*)then () else error "sort_variables a CHANGED";
36.33
36.34 -case eval_is_multUnordered "xxx " "yyy " t thy of
36.35 +case eval_is_multUnordered "xxx " "yyy " t @{context} of
36.36 SOME
36.37 ("xxx a_",
36.38 Const (\<^const_name>\<open>Trueprop\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $
36.39 @@ -535,7 +535,7 @@
36.40 (*+*) andalso not (is_multUnordered arg)
36.41 (*+*)then () else error "sort_variables - 2 CHANGED";
36.42
36.43 -case eval_is_multUnordered "xxx " "yyy " t thy of
36.44 +case eval_is_multUnordered "xxx " "yyy " t @{context} of
36.45 SOME
36.46 ("xxx - 2_",
36.47 Const (\<^const_name>\<open>Trueprop\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $
36.48 @@ -676,7 +676,7 @@
36.49 val t = TermC.str2term "(6 * a) is_multUnordered";
36.50 val SOME
36.51 (_, t') =
36.52 - eval_is_multUnordered "xxx" () t @{theory};
36.53 + eval_is_multUnordered "xxx" () t @{context};
36.54 (*+*)if UnparseC.term t' = "6 * a is_multUnordered = False" then ()
36.55 (*+*)else error "6 * a is_multUnordered = False CHANGED";
36.56
37.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml Wed Aug 03 18:17:27 2022 +0200
37.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml Thu Aug 04 12:48:37 2022 +0200
37.3 @@ -1018,31 +1018,31 @@
37.4 then () else error "rls complete_square CHANGED";
37.5
37.6 val thm = @{thm square_explicit1};
37.7 -val SOME (t,asm) = rewrite_ ctxt dummy_ord Rule_Set.Empty true thm t;
37.8 +val SOME (t,asm) = rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.Empty true thm t;
37.9 if UnparseC.term t = "(2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2 - - 8"
37.10 then () else error "thm square_explicit1 CHANGED";
37.11
37.12 val thm = @{thm root_plus_minus};
37.13 -val SOME (t,asm) = rewrite_ ctxt dummy_ord PolyEq_erls true thm t;
37.14 +val SOME (t,asm) = rewrite_ ctxt Rewrite_Ord.function_empty PolyEq_erls true thm t;
37.15 if UnparseC.term t =
37.16 "2 / 2 - x = sqrt ((2 / 2) \<up> 2 - - 8) \<or>\n2 / 2 - x = - 1 * sqrt ((2 / 2) \<up> 2 - - 8)"
37.17 then () else error "thm root_plus_minus CHANGED";
37.18
37.19 (*the thm bdv_explicit2* here required to be constrained to ::real*)
37.20 val thm = @{thm bdv_explicit2};
37.21 -val SOME (t,asm) = rewrite_inst_ ctxt dummy_ord Rule_Set.Empty true inst thm t;
37.22 +val SOME (t,asm) = rewrite_inst_ ctxt Rewrite_Ord.function_empty Rule_Set.Empty true inst thm t;
37.23 if UnparseC.term t =
37.24 "2 / 2 - x = sqrt ((2 / 2) \<up> 2 - - 8) \<or>\n- 1 * x = - (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - - 8)"
37.25 then () else error "thm bdv_explicit2 CHANGED";
37.26
37.27 val thm = @{thm bdv_explicit3};
37.28 -val SOME (t,asm) = rewrite_inst_ ctxt dummy_ord Rule_Set.Empty true inst thm t;
37.29 +val SOME (t,asm) = rewrite_inst_ ctxt Rewrite_Ord.function_empty Rule_Set.Empty true inst thm t;
37.30 if UnparseC.term t =
37.31 "2 / 2 - x = sqrt ((2 / 2) \<up> 2 - - 8) \<or>\nx = - 1 * (- (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - - 8))"
37.32 then () else error "thm bdv_explicit3 CHANGED";
37.33
37.34 val thm = @{thm bdv_explicit2};
37.35 -val SOME (t,asm) = rewrite_inst_ ctxt dummy_ord Rule_Set.Empty true inst thm t;
37.36 +val SOME (t,asm) = rewrite_inst_ ctxt Rewrite_Ord.function_empty Rule_Set.Empty true inst thm t;
37.37 if UnparseC.term t =
37.38 "- 1 * x = - (2 / 2) + sqrt ((2 / 2) \<up> 2 - - 8) \<or>\nx = - 1 * (- (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - - 8))"
37.39 then () else error "thm bdv_explicit2 CHANGED";
38.1 --- a/test/Tools/isac/Knowledge/polyeq-2.sml Wed Aug 03 18:17:27 2022 +0200
38.2 +++ b/test/Tools/isac/Knowledge/polyeq-2.sml Thu Aug 04 12:48:37 2022 +0200
38.3 @@ -287,14 +287,14 @@
38.4 t |> UnparseC.term; t |> TermC.atomty;
38.5 val thm = @{thm d2_prescind1};
38.6 thm |> Thm.prop_of |> UnparseC.term; thm |> Thm.prop_of |> TermC.atomty;
38.7 -val SOME (t', _) = rewrite_inst_ ctxt e_rew_ord Rule_Set.empty true subst thm t; UnparseC.term t';
38.8 +val SOME (t', _) = rewrite_inst_ ctxt Rewrite_Ord.function_empty Rule_Set.empty true subst thm t; UnparseC.term t';
38.9
38.10 (*x * (-6 + 5 * x) = 0 : Rewrite_Inst (["(''bdv'',x)"],("d2_reduce_equation1", ""))
38.11 --> x = 0 | -6 + 5 * x = 0*)
38.12 t' |> UnparseC.term; t' |> TermC.atomty;
38.13 val thm = @{thm d2_reduce_equation1};
38.14 thm |> Thm.prop_of |> UnparseC.term; thm |> Thm.prop_of |> TermC.atomty;
38.15 -val SOME (t'', _) = rewrite_inst_ ctxt e_rew_ord Rule_Set.empty true subst thm t'; UnparseC.term t'';
38.16 +val SOME (t'', _) = rewrite_inst_ ctxt Rewrite_Ord.function_empty Rule_Set.empty true subst thm t'; UnparseC.term t'';
38.17 (* NONE with d2_reduce_equation1: "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=0))"
38.18 instead d2_reduce_equation1: "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=(0::real)))"
38.19 *)
39.1 --- a/test/Tools/isac/Knowledge/polyminus.sml Wed Aug 03 18:17:27 2022 +0200
39.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml Thu Aug 04 12:48:37 2022 +0200
39.3 @@ -257,7 +257,7 @@
39.4 | _ => error "polyminus.sml: 3 * a * b kleiner b = True";
39.5
39.6 "======= compare tausche_plus with real_num_collect";
39.7 -val od = dummy_ord;
39.8 +val od = Rewrite_Ord.function_empty;
39.9
39.10 val erls = erls_ordne_alphabetisch;
39.11 val t = TermC.str2term "b + a";
39.12 @@ -526,12 +526,12 @@
39.13 val erls = erls_ordne_alphabetisch;
39.14 val t = TermC.str2term "- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f - 8 * g + 10 * g";
39.15 val SOME (t',_) =
39.16 - rewrite_ ctxt e_rew_ord erls false @{thm tausche_minus} t;
39.17 + rewrite_ ctxt Rewrite_Ord.function_empty erls false @{thm tausche_minus} t;
39.18 UnparseC.term t'; "- 9 + 12 + 5 * e - 7 * e + (- 4 + 6) * f - 8 * g + 10 * g";
39.19
39.20 val t = TermC.str2term "- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f - 8 * g + 10 * g";
39.21 val NONE =
39.22 - rewrite_ ctxt e_rew_ord erls false @{thm tausche_minus_plus} t;
39.23 + rewrite_ ctxt Rewrite_Ord.function_empty erls false @{thm tausche_minus_plus} t;
39.24
39.25 val t = TermC.str2term "- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f - 8 * g + 10 * g";
39.26 val SOME (t',_) =
40.1 --- a/test/Tools/isac/Knowledge/rational-2.sml Wed Aug 03 18:17:27 2022 +0200
40.2 +++ b/test/Tools/isac/Knowledge/rational-2.sml Thu Aug 04 12:48:37 2022 +0200
40.3 @@ -854,7 +854,7 @@
40.4 "HOL.True";
40.5
40.6 val t = TermC.str2term "(6*x) \<up> 2";
40.7 -val SOME (t',_) = rewrite_ ctxt dummy_ord powers_erls false @{thm realpow_def_atom} t;
40.8 +val SOME (t',_) = rewrite_ ctxt Rewrite_Ord.function_empty powers_erls false @{thm realpow_def_atom} t;
40.9 if UnparseC.term t' = "6 * x * (6 * x) \<up> (2 + - 1)" then ()
40.10 else error "rational.sml powers_erls (6*x) \<up> 2";
40.11
41.1 --- a/test/Tools/isac/MathEngBasic/rewrite.sml Wed Aug 03 18:17:27 2022 +0200
41.2 +++ b/test/Tools/isac/MathEngBasic/rewrite.sml Thu Aug 04 12:48:37 2022 +0200
41.3 @@ -88,7 +88,7 @@
41.4 val thm = @{thm add.commute};
41.5 val tm = @{term "x + y*z::real"};
41.6
41.7 -val SOME (r,_) = (rewrite_ ctxt dummy_ord Rule_Set.empty false thm tm);
41.8 +val SOME (r,_) = (rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.empty false thm tm);
41.9 (*is displayed on _TOP_ of <response> buffer...*)
41.10 Pretty.writeln (Proof_Context.pretty_term_abbrev @{context} r);
41.11 if r = @{term "y*z + x::real"}
41.12 @@ -97,7 +97,7 @@
41.13 "----- rewriting a subterm";
41.14 val tm = @{term "w*(x + y*z)::real"};
41.15
41.16 -val SOME (r, _) = (rewrite_ ctxt dummy_ord Rule_Set.empty false thm tm);
41.17 +val SOME (r, _) = (rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.empty false thm tm);
41.18
41.19 "----- ordered rewriting";
41.20 fun tord (_:subst) pp = LibraryC.termless pp;
41.21 @@ -150,7 +150,7 @@
41.22 val thm = @{thm nonzero_divide_mult_cancel_right};
41.23 val tm = @{term "x / (2 * x)::real"};
41.24
41.25 -val SOME (rew, asm) = (rewrite_ ctxt dummy_ord Rule_Set.empty false thm tm);
41.26 +val SOME (rew, asm) = rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.empty false thm tm;
41.27
41.28 if rew = @{term "1 / 2::real"} then () (* the rewrite is _NO_ Trueprop *)
41.29 else error "rewrite.sml diff.result in cond.rew.";
41.30 @@ -168,12 +168,12 @@
41.31 val tm = @{term "x / (2 * x)::real"};
41.32 val erls = eval_rls;
41.33
41.34 -(**)val SOME (rew, asm) = rewrite_ ctxt dummy_ord Rule_Set.empty false thm tm;
41.35 +(**)val SOME (rew, asm) = rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.empty false thm tm;
41.36 (** )exception TERM raised (line 196 of "~~/src/HOL/Tools/hologic.ML"):
41.37 dest_Trueprop
41.38 ?b \<noteq> 0 \<Longrightarrow> ?b / (?a * ?b) = 1 / ?a( **)
41.39 "~~~~~ fun rewrite_ , args:"; val (thy, rew_ord, erls, bool, thm, term) =
41.40 - (thy, dummy_ord, erls, false, thm, tm);
41.41 + (thy, Rewrite_Ord.function_empty, erls, false, thm, tm);
41.42 "~~~~~ fun rewrite__ , args:"; val (thy, i, bdv, tless, rls, put_asm, thm, ct) =
41.43 (thy, 1, []: Subst.T, rew_ord, erls, bool, thm, term);
41.44
41.45 @@ -210,11 +210,11 @@
41.46 "----------- step through 'and rew_sub': ----------------";
41.47 (*and make asms without Trueprop, beginning with the result:*)
41.48 val tm = @{term "x / (2 * x)::real"};
41.49 -val (t', asm, _, _) = rew_sub ctxt 0 [] dummy_ord Rule_Set.empty true [] (Thm.prop_of thm) tm;
41.50 +val (t', asm, _, _) = rew_sub ctxt 0 [] Rewrite_Ord.function_empty Rule_Set.empty true [] (Thm.prop_of thm) tm;
41.51 (*show_types := false;*)
41.52 "----- evaluate arguments";
41.53 val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) =
41.54 - (thy, 0, [], dummy_ord, Rule_Set.empty, true, [], (Thm.prop_of thm), tm);
41.55 + (thy, 0, [], Rewrite_Ord.function_empty, Rule_Set.empty, true, [], (Thm.prop_of thm), tm);
41.56 "----- step 1: LHS, RHS of rule";
41.57 val (LHS, RHS) = (HOLogic.dest_eq o HOLogic.dest_Trueprop
41.58 o Logic.strip_imp_concl) r;
41.59 @@ -245,7 +245,7 @@
41.60 "----------- step through 'fun rewrite_terms_' ------------------------------------------------";
41.61 "----- step 0: args for rewrite_terms_, local fun";
41.62 val (thy, ord, erls, equs, t) =
41.63 - (@{theory "Biegelinie"}, dummy_ord, Rule_Set.Empty, [TermC.str2term "x = 0"],
41.64 + (@{theory "Biegelinie"}, Rewrite_Ord.function_empty, Rule_Set.Empty, [TermC.str2term "x = 0"],
41.65 TermC.str2term "M_b x = -1 * q_0 * x \<up> 2 / 2 + x * c + c_2");
41.66 "----- step 1: args for rew_";
41.67 val ((t', asm'), (rules as r::rs), t) = ((TermC.empty, []), equs, t);
41.68 @@ -254,21 +254,21 @@
41.69 "----- step 3: step through rew_sub -- inefficient: goes into subterms";
41.70
41.71
41.72 -val SOME (t', _) = rewrite_terms_ ctxt dummy_ord Rule_Set.Empty equs t;
41.73 +val SOME (t', _) = rewrite_terms_ ctxt Rewrite_Ord.function_empty Rule_Set.Empty equs t;
41.74 writeln "---------- rewrite_terms_ 1---------------------------";
41.75 if UnparseC.term t' = "M_b 0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2" then ()
41.76 else error "rewrite.sml rewrite_terms_ [x = 0]";
41.77
41.78 val equs = [TermC.str2term "M_b 0 = 0"];
41.79 val t = TermC.str2term "M_b 0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2";
41.80 -val SOME (t', _) = rewrite_terms_ ctxt dummy_ord Rule_Set.Empty equs t;
41.81 +val SOME (t', _) = rewrite_terms_ ctxt Rewrite_Ord.function_empty Rule_Set.Empty equs t;
41.82 writeln "---------- rewrite_terms_ 2---------------------------";
41.83 if UnparseC.term t' = "0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2" then ()
41.84 else error "rewrite.sml rewrite_terms_ [M_b 0 = 0]";
41.85
41.86 val equs = [TermC.str2term "x = 0", TermC.str2term"M_b 0 = 0"];
41.87 val t = TermC.str2term "M_b x = - 1 * q_0 * x \<up> 2 / 2 + x * c + c_2";
41.88 -val SOME (t', _) = rewrite_terms_ ctxt dummy_ord Rule_Set.Empty equs t;
41.89 +val SOME (t', _) = rewrite_terms_ ctxt Rewrite_Ord.function_empty Rule_Set.Empty equs t;
41.90 writeln "---------- rewrite_terms_ 3---------------------------";
41.91 if UnparseC.term t' = "0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2" then ()
41.92 else error "rewrite.sml rewrite_terms_ [x = 0, M_b 0 = 0]";
41.93 @@ -658,7 +658,7 @@
41.94 "----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
41.95 "----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
41.96 "~~~~~ fun rewrite_ , args:"; val (thy, rew_ord, erls, bool, thm, term) =
41.97 - (@{theory}, dummy_ord, Rule_Set.empty, false, @{thm distrib_left}, @{term "x * (y + z) :: int"});
41.98 + (@{theory}, Rewrite_Ord.function_empty, Rule_Set.empty, false, @{thm distrib_left}, @{term "x * (y + z) :: int"});
41.99 "~~~~~ fun rewrite__ , args:"; val (thy, i, bdv, tless, rls, put_asm, thm, ct) =
41.100 (thy, 1, [], rew_ord, erls, bool, thm, term);
41.101 "~~~~~ and rew_sub , args:"; val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) =
42.1 --- a/test/Tools/isac/MathEngBasic/tactic.sml Wed Aug 03 18:17:27 2022 +0200
42.2 +++ b/test/Tools/isac/MathEngBasic/tactic.sml Thu Aug 04 12:48:37 2022 +0200
42.3 @@ -18,7 +18,7 @@
42.4 val thm'' = ("real_mult_div_cancel2", @{thm real_mult_div_cancel2});
42.5 val (f, res) = (@{term "a * x / (b * x) :: real"}, (@{term "a / b :: real"}, [@{term "k \<noteq> (0 :: real)"}]: term list))
42.6 ;
42.7 -Rewrite': ThyC.id * Rule_Def.rew_ord' * Rule_Set.T * bool * ThmC.T * term * Calc.result -> Tactic.T;
42.8 +Rewrite': ThyC.id * Rewrite_Ord.id * Rule_Set.T * bool * ThmC.T * term * Calc.result -> Tactic.T;
42.9 val tac = Rewrite' ("Diff", "dummy_ord", Rule_Set.empty, true, thm'', f, res)
42.10 ;
42.11 if (Tactic.result tac |> UnparseC.term) = "a / b" then () else error "creates_assms CHANGED";
43.1 --- a/test/Tools/isac/ProgLang/calculate.sml Wed Aug 03 18:17:27 2022 +0200
43.2 +++ b/test/Tools/isac/ProgLang/calculate.sml Thu Aug 04 12:48:37 2022 +0200
43.3 @@ -15,7 +15,8 @@
43.4 "----------- RE-BUILD fun eval_binop -----------------------------------------------------------";
43.5 "----------- RE-BUILD fun eval_binop -----------------------------------------------------------";
43.6
43.7 -fun test thy t = writeln (Syntax.string_of_term_global thy (Logic.mk_equals (t, calcul thy t)));
43.8 +fun test thy t =
43.9 + writeln (Syntax.string_of_term_global thy (Logic.mk_equals (t, calcul @{context} t)));
43.10
43.11 test \<^theory> \<^term>\<open>10 + 20 :: real\<close>;
43.12 test \<^theory> \<^term>\<open>10 - 20 :: real\<close>;
44.1 --- a/test/Tools/isac/ProgLang/evaluate.sml Wed Aug 03 18:17:27 2022 +0200
44.2 +++ b/test/Tools/isac/ProgLang/evaluate.sml Thu Aug 04 12:48:37 2022 +0200
44.3 @@ -56,22 +56,22 @@
44.4
44.5 "~~~~~ fun calculate_ , args:"; val (thy, isa_fn, t) = (thy, plus, t);
44.6 val SOME ("#: 1 + 2 = 3", adh_thm) = adhoc_thm @{theory} isa_fn t;
44.7 -val SOME (t', []) = rewrite__ ctxt 0 [] e_rew_ord Rule_Set.empty true adh_thm t;
44.8 +val SOME (t', []) = rewrite__ ctxt 0 [] Rewrite_Ord.function_empty Rule_Set.empty true adh_thm t;
44.9 if UnparseC.term t' = "(3 * 4 / 3) \<up> 2" then () else error "calculate_ 1 + 2 = 3 changed";
44.10
44.11 "~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, times, t');
44.12 val SOME ("#: 3 * 4 = 12", adh_thm) = adhoc_thm @{theory} isa_fn t';
44.13 -val SOME (t'', []) = rewrite__ ctxt 0 [] e_rew_ord Rule_Set.empty true adh_thm t;
44.14 +val SOME (t'', []) = rewrite__ ctxt 0 [] Rewrite_Ord.function_empty Rule_Set.empty true adh_thm t;
44.15 if UnparseC.term t'' = "(12 / 3) \<up> 2" then () else error "calculate_ 3 * 4 = 12 changed";
44.16
44.17 "~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, divide, t'');
44.18 val SOME ("#divide_e12_3", adh_thm) = adhoc_thm @{theory} isa_fn t;
44.19 -val SOME (t''', []) = rewrite__ ctxt 0 [] e_rew_ord Rule_Set.empty true adh_thm t;
44.20 +val SOME (t''', []) = rewrite__ ctxt 0 [] Rewrite_Ord.function_empty Rule_Set.empty true adh_thm t;
44.21 if UnparseC.term t''' = "4 \<up> 2" then () else error "calculate_ 12 / 3 = 4 changed";
44.22
44.23 "~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, pow, t''');
44.24 val SOME ("#: 4 \<up> 2 = 16", adh_thm) = adhoc_thm @{theory} isa_fn t;
44.25 -val SOME (t'''', []) = rewrite__ ctxt 0 [] e_rew_ord Rule_Set.empty true adh_thm t;
44.26 +val SOME (t'''', []) = rewrite__ ctxt 0 [] Rewrite_Ord.function_empty Rule_Set.empty true adh_thm t;
44.27 if UnparseC.term t'''' = "16" then () else error "calculate_ 12 / 3 = 4 changed";
44.28
44.29 "----------- calculate from Prog --------------------------------- -----------------------------";
45.1 --- a/test/Tools/isac/ProgLang/listC.sml Wed Aug 03 18:17:27 2022 +0200
45.2 +++ b/test/Tools/isac/ProgLang/listC.sml Thu Aug 04 12:48:37 2022 +0200
45.3 @@ -51,7 +51,7 @@
45.4 TermC.atomty t;
45.5 val thm = Thm.prop_of @{thm NTH_NIL};
45.6 TermC.atomty thm;
45.7 -val SOME (t', _) = rewrite_ ctxt dummy_ord prog_expr false @{thm NTH_NIL} t;
45.8 +val SOME (t', _) = rewrite_ ctxt Rewrite_Ord.function_empty prog_expr false @{thm NTH_NIL} t;
45.9 if UnparseC.term t' = "a" then ()
45.10 else error "NTH 1 [a,b,c,d,e] = a ..changed";
45.11
45.12 @@ -66,7 +66,7 @@
45.13 | _ => error "ListC.NTH changed";
45.14 val thm = Thm.prop_of @{thm NTH_CONS};
45.15 TermC.atomty thm;
45.16 -val SOME (t', _) = rewrite_ ctxt dummy_ord prog_expr false @{thm NTH_CONS} t;
45.17 +val SOME (t', _) = rewrite_ ctxt Rewrite_Ord.function_empty prog_expr false @{thm NTH_CONS} t;
45.18 if UnparseC.term t' = "NTH (3 + - 1) [b, c, d, e]" then ()
45.19 else error "NTH 3 [a,b,c,d,e] = NTH (3 + - 1) [b, c, d, e] ..changed";
45.20
46.1 --- a/test/Tools/isac/Test_Isac_Short.thy Wed Aug 03 18:17:27 2022 +0200
46.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Thu Aug 04 12:48:37 2022 +0200
46.3 @@ -145,19 +145,12 @@
46.4 \<close> ML \<open> (*//---------------- adhoc inserted ------------------------------------------------\\*)
46.5 \<close> ML \<open>
46.6 \<close> ML \<open> (*\\---------------- adhoc inserted ------------------------------------------------//*)
46.7 -Rewrite.trace_on := false;
46.8 \<close>
46.9 ML \<open>
46.10 \<close> ML \<open>
46.11 \<close> ML \<open>
46.12 \<close> ML \<open>
46.13 \<close> ML \<open>
46.14 -\<close> ML \<open>
46.15 -\<close> ML \<open>
46.16 -\<close> ML \<open>
46.17 -\<close> ML \<open>
46.18 -\<close> ML \<open>
46.19 -\<close> ML \<open>
46.20 \<close>
46.21
46.22 ML \<open>
46.23 @@ -333,12 +326,6 @@
46.24 \<close> ML \<open>
46.25 \<close> ML \<open>
46.26 \<close> ML \<open>
46.27 -\<close> ML \<open>
46.28 -\<close> ML \<open>
46.29 -\<close> ML \<open>
46.30 -\<close> ML \<open>
46.31 -\<close> ML \<open>
46.32 -\<close> ML \<open>
46.33 \<close>
46.34
46.35 section \<open>history of tests\<close>