1.1 --- a/src/Tools/isac/BaseDefinitions/rewrite-order.sml Wed Nov 16 10:30:59 2022 +0100
1.2 +++ b/src/Tools/isac/BaseDefinitions/rewrite-order.sml Wed Nov 16 17:42:41 2022 +0100
1.3 @@ -26,7 +26,7 @@
1.4 val id_empty = "Rewrite_Ord.id_empty";
1.5
1.6 type function = Rule_Def.rew_ord_function;
1.7 -fun function_empty (_: LibraryC.subst) (_: term, _: term) = true;
1.8 +fun function_empty (_: Proof.context) (_: LibraryC.subst) (_: term, _: term) = true;
1.9
1.10 type T = Rule_Def.rew_ord_T
1.11 val empty = (id_empty, function_empty)
2.1 --- a/src/Tools/isac/BaseDefinitions/rule-def.sml Wed Nov 16 10:30:59 2022 +0100
2.2 +++ b/src/Tools/isac/BaseDefinitions/rule-def.sml Wed Nov 16 17:42:41 2022 +0100
2.3 @@ -14,7 +14,7 @@
2.4 eqtype errpatID
2.5
2.6 type rew_ord_id = string
2.7 - type rew_ord_function = LibraryC.subst -> term * term -> bool
2.8 + type rew_ord_function = Proof.context -> LibraryC.subst -> term * term -> bool
2.9 type rew_ord_T = rew_ord_id * rew_ord_function
2.10
2.11
2.12 @@ -48,7 +48,7 @@
2.13 type eval_fn = string -> term -> Proof.context -> (string * term) option;
2.14
2.15 type rew_ord_id = string;
2.16 -type rew_ord_function = LibraryC.subst -> term * term -> bool;
2.17 +type rew_ord_function = Proof.context -> LibraryC.subst -> term * term -> bool;
2.18 type rew_ord_T = rew_ord_id * rew_ord_function;
2.19
2.20 type eval_const_id = string;
3.1 --- a/src/Tools/isac/BaseDefinitions/rule-set.sml Wed Nov 16 10:30:59 2022 +0100
3.2 +++ b/src/Tools/isac/BaseDefinitions/rule-set.sml Wed Nov 16 17:42:41 2022 +0100
3.3 @@ -46,7 +46,7 @@
3.4 type id = string;
3.5
3.6 (*/------- this will disappear eventually ----------------------------------------------------\*)
3.7 -fun dummy_ord (_: LibraryC.subst) (_: term, _: term) = true;
3.8 +val dummy_ord = Rewrite_Ord.function_empty;
3.9 val empty =
3.10 Rule_Def.Repeat {id = "empty", preconds = [], rew_ord = ("dummy_ord", dummy_ord), asm_rls = Rule_Def.Empty,
3.11 prog_rls = Rule_Def.Empty, calc = [], rules = [], errpatts = [], program = Rule_Def.Empty_Prog}
4.1 --- a/src/Tools/isac/BaseDefinitions/thy-write.sml Wed Nov 16 10:30:59 2022 +0100
4.2 +++ b/src/Tools/isac/BaseDefinitions/thy-write.sml Wed Nov 16 17:42:41 2022 +0100
4.3 @@ -56,7 +56,7 @@
4.4 | Hrls of {guh: Check_Unique.id, coursedesign: authors, mathauthors: authors, thy_rls: (ThyC.id * Rule_Set.T)}
4.5 | Hcal of {guh: Check_Unique.id, coursedesign: authors, mathauthors: authors, calc: Rule_Def.eval_ml_from_prog}
4.6 | Hord of {guh: Check_Unique.id, coursedesign: authors, mathauthors: authors,
4.7 - ord: (subst -> (term * term) -> bool)};
4.8 + ord: (Proof.context -> subst -> (term * term) -> bool)};
4.9 fun the2str (Html {guh, ...}) = guh
4.10 | the2str (Hthm {guh, ...}) = guh
4.11 | the2str (Hrls {guh, ...}) = guh
5.1 --- a/src/Tools/isac/Knowledge/Base_Tools.thy Wed Nov 16 10:30:59 2022 +0100
5.2 +++ b/src/Tools/isac/Knowledge/Base_Tools.thy Wed Nov 16 17:42:41 2022 +0100
5.3 @@ -46,8 +46,8 @@
5.4 local
5.5 open Term;
5.6 in
5.7 - fun termlessI (_: subst) uv = LibraryC.termless uv;
5.8 - fun term_ordI (_: subst) uv = Term_Ord.term_ord uv;
5.9 + fun termlessI (_: Proof.context) (_: subst) uv = LibraryC.termless uv;
5.10 + fun term_ordI (_: Proof.context) (_: subst) uv = Term_Ord.term_ord uv;
5.11 end;
5.12 \<close> ML \<open>
5.13 (*TODO.WN0509 reduce ids: tless_true = e_rew_ord' = Rewrite_Ord.function_empty = Rewrite_Ord.function_empty*)
6.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Wed Nov 16 10:30:59 2022 +0100
6.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Wed Nov 16 17:42:41 2022 +0100
6.3 @@ -119,22 +119,22 @@
6.4 | size_of_term' (f$t) = size_of_term' f + size_of_term' t
6.5 | size_of_term' _ = 1;
6.6
6.7 -fun term_ord' pr thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
6.8 - (case term_ord' pr thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord)
6.9 - | term_ord' pr thy (t, u) =
6.10 +fun term_ord' pr ctxt (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
6.11 + (case term_ord' pr ctxt (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord)
6.12 + | term_ord' pr ctxt (t, u) =
6.13 (if pr
6.14 then
6.15 let
6.16 val (f, ts) = strip_comb t and (g, us) = strip_comb u;
6.17 - val _ = tracing ("t= f @ ts= \"" ^ UnparseC.term_in_thy thy f ^ "\" @ \"[" ^
6.18 - commas (map (UnparseC.term_in_thy thy) ts) ^ "]\"");
6.19 - val _ = tracing ("u= g @ us= \"" ^ UnparseC.term_in_thy thy g ^ "\" @ \"[" ^
6.20 - commas (map (UnparseC.term_in_thy thy) us) ^ "]\"");
6.21 + val _ = tracing ("t= f @ ts= \"" ^ UnparseC.term_in_ctxt ctxt f ^ "\" @ \"[" ^
6.22 + commas (map (UnparseC.term_in_ctxt ctxt) ts) ^ "]\"");
6.23 + val _ = tracing ("u= g @ us= \"" ^ UnparseC.term_in_ctxt ctxt g ^ "\" @ \"[" ^
6.24 + commas (map (UnparseC.term_in_ctxt ctxt) us) ^ "]\"");
6.25 val _ = tracing ("size_of_term (t, u) = (" ^ string_of_int (size_of_term' t) ^ ", " ^
6.26 string_of_int (size_of_term' u) ^ ")");
6.27 val _ = tracing ("hd_ord (f, g) = " ^ ((pr_ord o hd_ord) (f, g)) );
6.28 (** )val _ = @{print tracing}{a = "hd_ord (f, g) = ", z = hd_ord (f, g)}( **)
6.29 - val _ = tracing ("terms_ord (ts, us) = " ^(pr_ord o terms_ord str false) (ts,us));
6.30 + val _ = tracing ("terms_ord (ts, us) = " ^ (pr_ord o terms_ord str false ctxt) (ts,us) );
6.31 val _= tracing ("-------");
6.32 in () end
6.33 else ();
6.34 @@ -142,13 +142,13 @@
6.35 EQUAL =>
6.36 let val (f, ts) = strip_comb t and (g, us) = strip_comb u
6.37 in (case hd_ord (f, g) of
6.38 - EQUAL => (terms_ord str pr) (ts, us)
6.39 + EQUAL => (terms_ord str pr ctxt) (ts, us)
6.40 | ord => ord)
6.41 end
6.42 - | ord => ord)
6.43 + | ord => ord)
6.44 and hd_ord (f, g) = (* ~ term.ML *)
6.45 prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord (dest_hd' f, dest_hd' g)
6.46 -and terms_ord _ pr (ts, us) = list_ord (term_ord' pr (ThyC.get_theory "Isac_Knowledge"))(ts, us);
6.47 +and terms_ord _ pr ctxt (ts, us) = list_ord (term_ord' pr ctxt) (ts, us);
6.48 (**)
6.49 in
6.50 (**)
6.51 @@ -164,7 +164,7 @@
6.52 \<close> ML \<open>
6.53 \<close>
6.54 setup \<open>Know_Store.add_rew_ords [
6.55 - ("ord_simplify_System", ord_simplify_System false \<^theory>)]\<close>
6.56 + ("ord_simplify_System", ord_simplify_System false)]\<close>
6.57
6.58 ML \<open>
6.59 (** rulesets **)
6.60 @@ -173,7 +173,7 @@
6.61 val order_add_mult_System =
6.62 Rule_Def.Repeat{
6.63 id = "order_add_mult_System", preconds = [],
6.64 - rew_ord = ("ord_simplify_System", ord_simplify_System false @{theory "Integrate"}),
6.65 + rew_ord = ("ord_simplify_System", ord_simplify_System false),
6.66 asm_rls = Rule_Set.empty,prog_rls = Rule_Set.Empty, calc = [], errpatts = [],
6.67 rules = [
6.68 \<^rule_thm>\<open>mult.commute\<close>, (* z * w = w * z *)
6.69 @@ -310,7 +310,7 @@
6.70 appears as [..c_4 = .., ..., ..., ..c_1 + ..c_2 + ..c_3 ..c_4 = ..].*)
6.71 val order_system =
6.72 Rule_Def.Repeat {id="order_system", preconds = [],
6.73 - rew_ord = ("ord_simplify_System", ord_simplify_System false \<^theory>),
6.74 + rew_ord = ("ord_simplify_System", ord_simplify_System false),
6.75 asm_rls = Rule_Set.Empty, prog_rls = Rule_Set.Empty, calc = [], errpatts = [],
6.76 rules = [
6.77 \<^rule_thm>\<open>order_system_NxN\<close>],
7.1 --- a/src/Tools/isac/Knowledge/Poly.thy Wed Nov 16 10:30:59 2022 +0100
7.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Wed Nov 16 17:42:41 2022 +0100
7.3 @@ -514,45 +514,49 @@
7.4 | size_of_term' (f$t) = size_of_term' f + size_of_term' t
7.5 | size_of_term' _ = 1;
7.6
7.7 -fun term_ord' pr thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
7.8 - (case term_ord' pr thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord)
7.9 - | term_ord' pr thy (t, u) =
7.10 +fun term_ord' pr ctxt (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
7.11 + (case term_ord' pr ctxt (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord)
7.12 + | term_ord' pr ctxt (t, u) =
7.13 (if pr then
7.14 let
7.15 val (f, ts) = strip_comb t and (g, us) = strip_comb u;
7.16 - val _ = tracing ("t= f@ts= \"" ^ UnparseC.term_in_thy thy f ^ "\" @ \"[" ^
7.17 - commas (map (UnparseC.term_in_thy thy) ts) ^ "]\"");
7.18 - val _ = tracing("u= g@us= \"" ^ UnparseC.term_in_thy thy g ^ "\" @ \"[" ^
7.19 - commas (map (UnparseC.term_in_thy thy) us) ^ "]\"");
7.20 + val _ = tracing ("t= f@ts= \"" ^ UnparseC.term_in_ctxt ctxt f ^ "\" @ \"[" ^
7.21 + commas (map (UnparseC.term_in_ctxt ctxt) ts) ^ "]\"");
7.22 + val _ = tracing("u= g@us= \"" ^ UnparseC.term_in_ctxt ctxt g ^ "\" @ \"[" ^
7.23 + commas (map (UnparseC.term_in_ctxt ctxt) us) ^ "]\"");
7.24 val _ = tracing ("size_of_term(t,u)= (" ^ string_of_int (size_of_term' t) ^ ", " ^
7.25 string_of_int (size_of_term' u) ^ ")");
7.26 val _ = tracing ("hd_ord(f,g) = " ^ (pr_ord o hd_ord) (f,g));
7.27 - val _ = tracing ("terms_ord(ts,us) = " ^ (pr_ord o terms_ord str false) (ts, us));
7.28 + val _ = tracing ("terms_ord(ts,us) = " ^ (pr_ord o terms_ord str false ctxt) (ts, us));
7.29 val _ = tracing ("-------");
7.30 in () end
7.31 else ();
7.32 case int_ord (size_of_term' t, size_of_term' u) of
7.33 EQUAL =>
7.34 let val (f, ts) = strip_comb t and (g, us) = strip_comb u in
7.35 - (case hd_ord (f, g) of EQUAL => (terms_ord str pr) (ts, us)
7.36 + (case hd_ord (f, g) of EQUAL => (terms_ord str pr ctxt) (ts, us)
7.37 | ord => ord)
7.38 end
7.39 | ord => ord)
7.40 and hd_ord (f, g) = (* ~ term.ML *)
7.41 prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord (dest_hd' f, dest_hd' g)
7.42 -and terms_ord _ pr (ts, us) =
7.43 - list_ord (term_ord' pr (ThyC.get_theory "Isac_Knowledge"))(ts, us);
7.44 +and terms_ord _ pr ctxt (ts, us) =
7.45 + list_ord (term_ord' pr ctxt) (ts, us);
7.46
7.47 in
7.48
7.49 -fun ord_make_polynomial (pr:bool) thy (_: subst) (ts, us) =
7.50 - (term_ord' pr thy(***) (TermC.numerals_to_Free ts, TermC.numerals_to_Free us) = LESS );
7.51 +fun ord_make_polynomial (pr:bool) ctxt (_: subst) (ts, us) =
7.52 + (term_ord' pr ctxt (TermC.numerals_to_Free ts, TermC.numerals_to_Free us) = LESS );
7.53
7.54 end;(*local*)
7.55 +\<close> ML \<open>
7.56 +ord_make_polynomial
7.57 +\<close> ML \<open>
7.58 +\<close> ML \<open>
7.59 \<close>
7.60 setup \<open>Know_Store.add_rew_ords [
7.61 ("termlessI", termlessI),
7.62 - ("ord_make_polynomial", ord_make_polynomial false \<^theory>)]\<close>
7.63 + ("ord_make_polynomial", ord_make_polynomial false)]\<close>
7.64
7.65 subsection \<open>predicates\<close>
7.66 subsubsection \<open>in specifications\<close>
7.67 @@ -989,7 +993,7 @@
7.68 (total-degree-)ordering of monoms NOT possible with size_of_term GIVEN*)
7.69 val order_add_mult =
7.70 Rule_Def.Repeat{id = "order_add_mult", preconds = [],
7.71 - rew_ord = ("ord_make_polynomial", ord_make_polynomial false \<^theory>),
7.72 + rew_ord = ("ord_make_polynomial", ord_make_polynomial false),
7.73 asm_rls = Rule_Set.empty,prog_rls = Rule_Set.Empty,
7.74 calc = [], errpatts = [],
7.75 rules = [
7.76 @@ -1004,7 +1008,7 @@
7.77 (total-degree-)ordering of monoms NOT possible with size_of_term GIVEN*)
7.78 val order_mult =
7.79 Rule_Def.Repeat{id = "order_mult", preconds = [],
7.80 - rew_ord = ("ord_make_polynomial",ord_make_polynomial false \<^theory>),
7.81 + rew_ord = ("ord_make_polynomial",ord_make_polynomial false),
7.82 asm_rls = Rule_Set.empty,prog_rls = Rule_Set.Empty,
7.83 calc = [], errpatts = [],
7.84 rules = [
8.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Wed Nov 16 10:30:59 2022 +0100
8.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Wed Nov 16 17:42:41 2022 +0100
8.3 @@ -1060,59 +1060,64 @@
8.4 | _ => raise ERROR ("size_of_term' called with subst = " ^ UnparseC.term x))
8.5 | _ => (if pr then tracing (idt "#" i ^ "bot --> " ^ "1") else (); 1));
8.6
8.7 -fun term_ord' i pr x thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
8.8 +fun term_ord' i pr x ctxt (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
8.9 let
8.10 val _ = if pr then tracing (idt "#" i ^ "term_ord' Abs") else ();
8.11 val ord =
8.12 - case term_ord' (i + 1) pr x thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord
8.13 + case term_ord' (i + 1) pr x ctxt (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord
8.14 val _ = if pr then tracing (idt "#" i ^ "term_ord' Abs --> " ^ pr_ord ord) else ()
8.15 in ord end
8.16 - | term_ord' i pr x _ (t, u) =
8.17 + | term_ord' i pr x ctxt (t, u) =
8.18 let
8.19 - val _ = if pr then tracing (idt "#" i ^ "term_ord' bot (" ^ UnparseC.term t ^ ", " ^ UnparseC.term u ^ ")") else ();
8.20 + val _ = if pr then tracing (idt "#" i ^ "term_ord' bot (" ^ UnparseC.term_in_ctxt ctxt t ^
8.21 + ", " ^ UnparseC.term_in_ctxt ctxt u ^ ")") else ();
8.22 val ord =
8.23 case int_ord (size_of_term' (i + 1) pr x t, size_of_term' (i + 1) pr x u) of
8.24 EQUAL =>
8.25 let val (f, ts) = strip_comb t and (g, us) = strip_comb u
8.26 in
8.27 - (case hd_ord (i + 1) pr x (f, g) of
8.28 - EQUAL => (terms_ord x (i + 1) pr) (ts, us)
8.29 + (case hd_ord (i + 1) pr x ctxt (f, g) of
8.30 + EQUAL => (terms_ord x (i + 1) pr ctxt) (ts, us)
8.31 | ord => ord)
8.32 end
8.33 | ord => ord
8.34 val _ = if pr then tracing (idt "#" i ^ "term_ord' bot --> " ^ pr_ord ord) else ()
8.35 in ord end
8.36 -and hd_ord i pr x (f, g) = (* ~ term.ML *)
8.37 +and hd_ord i pr x ctxt (f, g) = (* ~ term.ML *)
8.38 let
8.39 - val _ = if pr then tracing (idt "#" i ^ "hd_ord (" ^ UnparseC.term f ^ ", " ^ UnparseC.term g ^ ")") else ();
8.40 + val _ = if pr then tracing (idt "#" i ^ "hd_ord (" ^ UnparseC.term_in_ctxt ctxt f ^
8.41 + ", " ^ UnparseC.term g ^ ")") else ();
8.42 val ord = prod_ord
8.43 (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord
8.44 (dest_hd' x f, dest_hd' x g)
8.45 val _ = if pr then tracing (idt "#" i ^ "hd_ord --> " ^ pr_ord ord) else ();
8.46 in ord end
8.47 -and terms_ord x i pr (ts, us) =
8.48 +and terms_ord x i pr ctxt (ts, us) =
8.49 let
8.50 - val _ = if pr then tracing (idt "#" i ^ "terms_ord (" ^ UnparseC.terms ts ^ ", " ^ UnparseC.terms us ^ ")") else ();
8.51 - val ord = list_ord (term_ord' (i + 1) pr x (ThyC.get_theory "Isac_Knowledge"))(ts, us);
8.52 + val _ = if pr then tracing (idt "#" i ^ "terms_ord (" ^ UnparseC.terms_in_ctxt ctxt ts ^
8.53 + ", " ^ UnparseC.terms_in_ctxt ctxt us ^ ")") else ();
8.54 + val ord = list_ord (term_ord' (i + 1) pr x ctxt) (ts, us);
8.55 val _ = if pr then tracing (idt "#" i ^ "terms_ord --> " ^ pr_ord ord) else ();
8.56 in ord end
8.57
8.58 (**)in(*local*)
8.59
8.60 -fun ord_make_polynomial_in (pr:bool) thy subst (ts, us) =
8.61 +fun ord_make_polynomial_in (pr:bool) ctxt subst (ts, us) =
8.62 ((** )tracing ("*** subs variable is: " ^ Env.subst2str subst); ( **)
8.63 case subst of
8.64 (_, x) :: _ =>
8.65 - term_ord' 1 pr x thy (TermC.numerals_to_Free ts, TermC.numerals_to_Free us) = LESS
8.66 + term_ord' 1 pr x ctxt (TermC.numerals_to_Free ts, TermC.numerals_to_Free us) = LESS
8.67 | _ => raise ERROR ("ord_make_polynomial_in called with subst = " ^ Env.subst2str subst))
8.68
8.69 end;(*local*)
8.70 -
8.71 +\<close> ML \<open>
8.72 +ord_make_polynomial_in
8.73 +\<close> ML \<open>
8.74 \<close>
8.75 ML\<open>
8.76 val order_add_mult_in = prep_rls'(
8.77 Rule_Def.Repeat{id = "order_add_mult_in", preconds = [],
8.78 - rew_ord = ("ord_make_polynomial_in", ord_make_polynomial_in false @{theory "Poly"}),
8.79 + rew_ord = ("ord_make_polynomial_in", ord_make_polynomial_in false),
8.80 asm_rls = Rule_Set.empty,prog_rls = Rule_Set.Empty,
8.81 calc = [], errpatts = [],
8.82 rules = [
9.1 --- a/src/Tools/isac/Knowledge/Rational.thy Wed Nov 16 10:30:59 2022 +0100
9.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Wed Nov 16 17:42:41 2022 +0100
9.3 @@ -513,7 +513,7 @@
9.4
9.5 val cancel_p =
9.6 Rule_Set.Rrls {id = "cancel_p", prepat = [],
9.7 - rew_ord = ("ord_make_polynomial", ord_make_polynomial false \<^theory>),
9.8 + rew_ord = ("ord_make_polynomial", ord_make_polynomial false),
9.9 asm_rls = rational_erls,
9.10 calc =
9.11 [("PLUS", (\<^const_name>\<open>plus\<close>, (**)Calc_Binop.numeric "#add_")),
9.12 @@ -581,7 +581,7 @@
9.13
9.14 val add_fractions_p =
9.15 Rule_Set.Rrls {id = "add_fractions_p", prepat=prepat,
9.16 - rew_ord = ("ord_make_polynomial", ord_make_polynomial false \<^theory>),
9.17 + rew_ord = ("ord_make_polynomial", ord_make_polynomial false),
9.18 asm_rls = rational_erls,
9.19 calc = [("PLUS", (\<^const_name>\<open>plus\<close>, (**)Calc_Binop.numeric "#add_")),
9.20 ("TIMES", (\<^const_name>\<open>times\<close>, (**)Calc_Binop.numeric "#mult_")),
10.1 --- a/src/Tools/isac/Knowledge/Root.thy Wed Nov 16 10:30:59 2022 +0100
10.2 +++ b/src/Tools/isac/Knowledge/Root.thy Wed Nov 16 17:42:41 2022 +0100
10.3 @@ -101,38 +101,37 @@
10.4 | size_of_term' (Abs (_,_,body)) = 1 + size_of_term' body
10.5 | size_of_term' (f $ t) = size_of_term' f + size_of_term' t
10.6 | size_of_term' _ = 1;
10.7 -fun term_ord' pr thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
10.8 - (case term_ord' pr thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U)
10.9 +fun term_ord' pr ctxt (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
10.10 + (case term_ord' pr ctxt (t, u) of EQUAL => Term_Ord.typ_ord (T, U)
10.11 | ord => ord)
10.12 - | term_ord' pr thy (t, u) =
10.13 - (if pr then
10.14 - let
10.15 - val (f, ts) = strip_comb t and (g, us) = strip_comb u;
10.16 - val _ = tracing ("t= f@ts= \"" ^ UnparseC.term_in_ctxt (Proof_Context.init_global thy) f ^"\" @ \"[" ^
10.17 - commas (map (UnparseC.term_in_ctxt (Proof_Context.init_global thy)) ts) ^ "]\"");
10.18 - val _ = tracing ("u= g@us= \"" ^ UnparseC.term g ^"\" @ \"[" ^
10.19 - commas (map (UnparseC.term_in_ctxt (Proof_Context.init_global thy)) us) ^ "]\"");
10.20 - val _ = tracing ("size_of_term(t,u)= (" ^
10.21 - string_of_int(size_of_term' t) ^", " ^
10.22 - string_of_int(size_of_term' u) ^")");
10.23 - val _ = tracing ("hd_ord(f,g) = " ^ (pr_ord o hd_ord) (f,g));
10.24 - val _ = tracing ("terms_ord(ts,us) = " ^
10.25 - (pr_ord o terms_ord str false) (ts,us));
10.26 - val _=tracing("-------");
10.27 - in () end
10.28 + | term_ord' pr ctxt (t, u) =
10.29 + (if pr
10.30 + then
10.31 + let
10.32 + val (f, ts) = strip_comb t and (g, us) = strip_comb u;
10.33 + val _ = tracing ("t= f@ts= \"" ^ UnparseC.term_in_ctxt ctxt f ^"\" @ \"[" ^
10.34 + commas (map (UnparseC.term_in_ctxt ctxt) ts) ^ "]\"");
10.35 + val _ = tracing ("u= g@us= \"" ^ UnparseC.term g ^"\" @ \"[" ^
10.36 + commas (map (UnparseC.term_in_ctxt ctxt) us) ^ "]\"");
10.37 + val _ = tracing ("size_of_term(t,u)= (" ^
10.38 + string_of_int(size_of_term' t) ^", " ^
10.39 + string_of_int(size_of_term' u) ^")");
10.40 + val _ = tracing ("hd_ord(f,g) = " ^ (pr_ord o hd_ord) (f,g));
10.41 + val _ = tracing ("terms_ord(ts,us) = " ^ (pr_ord o terms_ord str false ctxt) (ts,us));
10.42 + val _=tracing("-------");
10.43 + in () end
10.44 else ();
10.45 - case int_ord (size_of_term' t, size_of_term' u) of
10.46 - EQUAL =>
10.47 - let val (f, ts) = strip_comb t and (g, us) = strip_comb u in
10.48 - (case hd_ord (f, g) of EQUAL => (terms_ord str pr) (ts, us)
10.49 - | ord => ord)
10.50 - end
10.51 - | ord => ord)
10.52 + case int_ord (size_of_term' t, size_of_term' u) of
10.53 + EQUAL =>
10.54 + let val (f, ts) = strip_comb t and (g, us) = strip_comb u
10.55 + in (case hd_ord (f, g) of
10.56 + EQUAL => (terms_ord str pr ctxt) (ts, us)
10.57 + | ord => ord)
10.58 + end
10.59 + | ord => ord)
10.60 and hd_ord (f, g) = (* ~ term.ML *)
10.61 - prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord
10.62 - (dest_hd' f, dest_hd' g)
10.63 -and terms_ord _(*str*) pr (ts, us) =
10.64 - list_ord (term_ord' pr (ThyC.get_theory "Isac_Knowledge"))(ts, us);
10.65 + prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord (dest_hd' f, dest_hd' g)
10.66 +and terms_ord _(*str*) pr ctxt (ts, us) = list_ord (term_ord' pr ctxt) (ts, us);
10.67
10.68 in
10.69 (* associates a+(b+c) => (a+b)+c = a+b+c ... avoiding parentheses
10.70 @@ -143,17 +142,19 @@
10.71
10.72 (*args
10.73 pr: print trace, WN0509 'sqrt_right true' not used anymore
10.74 - thy:
10.75 + ctxt:
10.76 subst: no bound variables, only Root.sqrt
10.77 tu: the terms to compare (t1, t2) ... *)
10.78 -fun sqrt_right (pr:bool) thy (_: subst) (ts, us) =
10.79 - (term_ord' pr thy(***) (TermC.numerals_to_Free ts, TermC.numerals_to_Free us) = LESS );
10.80 +fun sqrt_right (pr:bool) ctxt (_: subst) (ts, us) =
10.81 + (term_ord' pr ctxt (TermC.numerals_to_Free ts, TermC.numerals_to_Free us) = LESS );
10.82 end;
10.83 \<close> ML \<open>
10.84 +\<close> ML \<open>
10.85 +sqrt_right: bool -> Proof.context -> Subst.T -> term * term -> bool
10.86 \<close>
10.87 setup \<open>Know_Store.add_rew_ords [
10.88 ("termlessI", termlessI),
10.89 - ("sqrt_right", sqrt_right false @{theory "Pure"})]\<close>
10.90 + ("sqrt_right", sqrt_right false)]\<close>
10.91
10.92 ML \<open>
10.93 (*------------------------- rules -------------------------*)
10.94 @@ -189,7 +190,7 @@
10.95
10.96 val make_rooteq = prep_rls'(
10.97 Rule_Def.Repeat{id = "make_rooteq", preconds = []:term list,
10.98 - rew_ord = ("sqrt_right", sqrt_right false \<^theory>),
10.99 + rew_ord = ("sqrt_right", sqrt_right false),
10.100 asm_rls = Atools_erls, prog_rls = Rule_Set.Empty,
10.101 calc = [], errpatts = [],
10.102 rules = [
11.1 --- a/src/Tools/isac/Knowledge/Test.thy Wed Nov 16 10:30:59 2022 +0100
11.2 +++ b/src/Tools/isac/Knowledge/Test.thy Wed Nov 16 17:42:41 2022 +0100
11.3 @@ -313,36 +313,35 @@
11.4 | size_of_term' (Abs (_,_,body)) = 1 + size_of_term' body
11.5 | size_of_term' (f$t) = size_of_term' f + size_of_term' t
11.6 | size_of_term' _ = 1;
11.7 -fun term_ord' pr thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
11.8 - (case term_ord' pr thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U)
11.9 +fun term_ord' pr ctxt (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
11.10 + (case term_ord' pr ctxt (t, u) of EQUAL => Term_Ord.typ_ord (T, U)
11.11 | ord => ord)
11.12 - | term_ord' pr _ (t, u) =
11.13 + | term_ord' pr ctxt (t, u) =
11.14 (if pr then
11.15 let val (f, ts) = strip_comb t and (g, us) = strip_comb u;
11.16 - val _ = tracing ("t= f@ts= \"" ^ UnparseC.term f ^ "\" @ \"[" ^
11.17 - commas(map UnparseC.term ts) ^ "]\"")
11.18 - val _ = tracing ("u= g@us= \"" ^ UnparseC.term g ^"\" @ \"[" ^
11.19 - commas(map UnparseC.term us) ^"]\"")
11.20 + val _ = tracing ("t= f@ts= \"" ^ UnparseC.term_in_ctxt ctxt f ^ "\" @ \"[" ^
11.21 + commas (map (UnparseC.term_in_ctxt ctxt) ts) ^ "]\"")
11.22 + val _ = tracing ("u= g@us= \"" ^ UnparseC.term_in_ctxt ctxt g ^"\" @ \"[" ^
11.23 + commas (map (UnparseC.term_in_ctxt ctxt) us) ^"]\"")
11.24 val _ = tracing ("size_of_term(t,u)= (" ^
11.25 string_of_int (size_of_term' t) ^ ", " ^
11.26 string_of_int (size_of_term' u) ^ ")")
11.27 val _ = tracing ("hd_ord(f,g) = " ^ (pr_ord o hd_ord) (f,g))
11.28 val _ = tracing ("terms_ord(ts,us) = " ^
11.29 - (pr_ord o terms_ord str false) (ts,us));
11.30 + (pr_ord o terms_ord str false ctxt) (ts,us));
11.31 val _ = tracing "-------"
11.32 in () end
11.33 else ();
11.34 case int_ord (size_of_term' t, size_of_term' u) of
11.35 EQUAL =>
11.36 let val (f, ts) = strip_comb t and (g, us) = strip_comb u in
11.37 - (case hd_ord (f, g) of EQUAL => (terms_ord str pr) (ts, us)
11.38 + (case hd_ord (f, g) of EQUAL => (terms_ord str pr ctxt) (ts, us)
11.39 | ord => ord)
11.40 end
11.41 | ord => ord)
11.42 and hd_ord (f, g) = (* ~ term.ML *)
11.43 prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord (dest_hd' f, dest_hd' g)
11.44 -and terms_ord _ pr (ts, us) =
11.45 - list_ord (term_ord' pr (ThyC.get_theory "Isac_Knowledge"))(ts, us);
11.46 +and terms_ord _ pr ctxt (ts, us) = list_ord (term_ord' pr ctxt) (ts, us);
11.47 in
11.48
11.49 fun ord_make_polytest (pr:bool) thy (_: subst) (ts, us) =
11.50 @@ -353,7 +352,7 @@
11.51
11.52 section \<open>term order\<close>
11.53 ML \<open>
11.54 -fun term_order (_: subst) tu = (term_ordI [] tu = LESS);
11.55 +val term_order = Rewrite_Ord.function_empty;
11.56 \<close>
11.57
11.58 section \<open>rulesets\<close>
11.59 @@ -393,7 +392,7 @@
11.60 (*FIXXXXXXME 10.8.02: handle like _simplify*)
11.61 val tval_rls =
11.62 Rule_Def.Repeat{id = "tval_rls", preconds = [],
11.63 - rew_ord = ("sqrt_right",sqrt_right false @{theory "Pure"}),
11.64 + rew_ord = ("sqrt_right",sqrt_right false),
11.65 asm_rls=testerls,prog_rls = Rule_Set.empty,
11.66 calc=[], errpatts = [],
11.67 rules = [
11.68 @@ -439,16 +438,17 @@
11.69 val rearrange_assoc =
11.70 Rule_Def.Repeat{
11.71 id = "rearrange_assoc", preconds = [],
11.72 - rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty),
11.73 + rew_ord = ("Rewrite_Ord.id_empty", Rewrite_Ord.function_empty),
11.74 asm_rls = Rule_Set.empty, prog_rls = Rule_Set.empty, calc = [], errpatts = [],
11.75 rules = [
11.76 \<^rule_thm_sym>\<open>add.assoc\<close>,
11.77 \<^rule_thm_sym>\<open>rmult_assoc\<close>],
11.78 program = Rule.Empty_Prog};
11.79
11.80 +\<close> ML \<open>
11.81 val ac_plus_times =
11.82 Rule_Def.Repeat{
11.83 - id = "ac_plus_times", preconds = [], rew_ord = ("term_order",term_order),
11.84 + id = "ac_plus_times", preconds = [], rew_ord = ("term_order", term_order),
11.85 asm_rls = Rule_Set.empty, prog_rls = Rule_Set.empty, calc = [], errpatts = [],
11.86 rules = [
11.87 \<^rule_thm>\<open>radd_commute\<close>,
11.88 @@ -458,6 +458,7 @@
11.89 \<^rule_thm>\<open>rmult_left_commute\<close>,
11.90 \<^rule_thm>\<open>rmult_assoc\<close>],
11.91 program = Rule.Empty_Prog};
11.92 +\<close> ML \<open>
11.93
11.94 (*todo: replace by Rewrite("rnorm_equation_add", @{thm rnorm_equation_add)*)
11.95 val norm_equation =
11.96 @@ -466,13 +467,12 @@
11.97 rules = [
11.98 \<^rule_thm>\<open>rnorm_equation_add\<close>],
11.99 program = Rule.Empty_Prog};
11.100 -\<close>
11.101 -ML \<open>
11.102 +\<close> ML \<open>
11.103 (* expects * distributed over + *)
11.104 val Test_simplify =
11.105 Rule_Def.Repeat{
11.106 id = "Test_simplify", preconds = [],
11.107 - rew_ord = ("sqrt_right", sqrt_right false @{theory "Pure"}),
11.108 + rew_ord = ("sqrt_right", sqrt_right false),
11.109 asm_rls = tval_rls, prog_rls = Rule_Set.empty,
11.110 calc=[(*since 040209 filled by prep_rls'*)], errpatts = [],
11.111 rules = [
11.112 @@ -591,12 +591,12 @@
11.113
11.114 setup \<open>Know_Store.add_rew_ords [
11.115 ("termlessI", termlessI),
11.116 - ("ord_make_polytest", ord_make_polytest false \<^theory>)]\<close>
11.117 + ("ord_make_polytest", ord_make_polytest false)]\<close>
11.118
11.119 ML \<open>
11.120 val make_polytest =
11.121 Rule_Def.Repeat{id = "make_polytest", preconds = []:term list,
11.122 - rew_ord = ("ord_make_polytest", ord_make_polytest false @{theory "Poly"}),
11.123 + rew_ord = ("ord_make_polytest", ord_make_polytest false),
11.124 asm_rls = testerls, prog_rls = Rule_Set.Empty,
11.125 calc = [
11.126 ("PLUS" , (\<^const_name>\<open>plus\<close>, (**)Calc_Binop.numeric "#add_")),
12.1 --- a/src/Tools/isac/Knowledge/Test_Build_Thydata.thy Wed Nov 16 10:30:59 2022 +0100
12.2 +++ b/src/Tools/isac/Knowledge/Test_Build_Thydata.thy Wed Nov 16 17:42:41 2022 +0100
12.3 @@ -6,7 +6,7 @@
12.4
12.5 ML \<open>
12.6 open Rule
12.7 -fun termlessI (_: subst) uv = LibraryC.termless uv;
12.8 +fun termlessI (_: Proof.context) (_: subst) uv = LibraryC.termless uv;
12.9 \<close>
12.10 axiomatization where
12.11 thm111: "thm111 = thm111 + (111::int)" and
13.1 --- a/src/Tools/isac/MathEngBasic/MathEngBasic.thy Wed Nov 16 10:30:59 2022 +0100
13.2 +++ b/src/Tools/isac/MathEngBasic/MathEngBasic.thy Wed Nov 16 17:42:41 2022 +0100
13.3 @@ -47,6 +47,7 @@
13.4
13.5 ML \<open>
13.6 \<close> ML \<open>
13.7 +Rewrite_Ord.function_empty
13.8 \<close> ML \<open>
13.9 \<close>
13.10 end
14.1 --- a/src/Tools/isac/MathEngBasic/rewrite.sml Wed Nov 16 10:30:59 2022 +0100
14.2 +++ b/src/Tools/isac/MathEngBasic/rewrite.sml Wed Nov 16 17:42:41 2022 +0100
14.3 @@ -114,7 +114,7 @@
14.4 else (trace_in5 ctxt i "asms false" p'; raise NO_REWRITE) (* don't go into subtm.of cond*)
14.5 end
14.6 in
14.7 - if TermC.perm lhs rhs andalso not (tless bdv (t', t)) (*ordered rewriting*)
14.8 + if TermC.perm lhs rhs andalso not (tless ctxt bdv (t', t)) (*ordered rewriting*)
14.9 then (trace_eq2 ctxt i "not >" t t'; raise NO_REWRITE)
14.10 else (t'', p'', [], true)
14.11 end
15.1 --- a/test/Tools/isac/BaseDefinitions/rewrite-order.sml Wed Nov 16 10:30:59 2022 +0100
15.2 +++ b/test/Tools/isac/BaseDefinitions/rewrite-order.sml Wed Nov 16 17:42:41 2022 +0100
15.3 @@ -61,9 +61,9 @@
15.4 then (trace_in4 ctxt i "asms accepted" p' simpl_p'; (t',simpl_p'))(* uncond.rew.from above*)
15.5 else (trace_in5 ctxt i "asms false" p'; raise NO_REWRITE) (* don't go into subtm.of cond*)
15.6 end;
15.7 - (*if*) TermC.perm lhs rhs andalso not (tless bdv (t', t)); (*ordered rewriting*)
15.8 - not (tless bdv (t', t)); (*isa = true , isa2 = false*)
15.9 - (tless bdv (t', t)); (*isa = false, isa2 = true*)
15.10 + (*if*) TermC.perm lhs rhs andalso not (tless @{context} bdv (t', t)); (*ordered rewriting*)
15.11 + not (tless @{context} bdv (t', t)); (*isa = true , isa2 = false*)
15.12 + (tless @{context} bdv (t', t)); (*isa = false, isa2 = true*)
15.13 (*WHAT IS ..:
15.14 tless <-- Repeat {rew_ord = ("sqrt_right", rew_ord_), asm_rls, ...} = Test_simplify; ..in Test_Some.thy
15.15 rew_ord_ <-- sqrt_right false @{theory "Pure"} ..in Test.thy
15.16 @@ -71,7 +71,7 @@
15.17 CHECK THIS ...(same error as with ^^^^^^^^^tless
15.18 CHECK THIS ...(same error as with code copied into Test_Some.thy
15.19 *)
15.20 -if (sqrt_right false @{theory "Pure"} bdv (t', t)) (*isa = false, isa2 = true*)
15.21 +if (sqrt_right false @{context} bdv (t', t)) (*isa = false, isa2 = true*)
15.22 (** )then error "sqrt_right: special case NOT ok" else (); ( *isa*)
15.23 (**)then () else error "sqrt_right: special case OK"; (*isa2*)
15.24 "~~~~~ fun sqrt_right , args:"; val ((pr:bool), thy, (_: subst), tu) =
15.25 @@ -112,7 +112,7 @@
15.26 "-------- check simple terms -------------------------------------------------------------------";
15.27 "-------- check simple terms -------------------------------------------------------------------";
15.28 "-------- check simple terms -------------------------------------------------------------------";
15.29 -val rew_ord_ = sqrt_right false @{theory "Pure"};
15.30 +val rew_ord_ = sqrt_right false @{context} ;
15.31
15.32 if rew_ord_ [] (@{term "1::real"}, @{term "2::real"}) = true then () else error "";
15.33 if rew_ord_ [] (@{term "3::real"}, @{term "2::real"}) = false then () else error "";
15.34 @@ -136,43 +136,43 @@
15.35 (*# rls: Test_simplify on: x + 1 + - 1 * 2 = 0 ..selected "not >:" from trace:*)
15.36
15.37 (*## not >: "x + 1 + - 1 * 2" > "x + 1 + - 1 * 2" *)
15.38 -if rew_ord_ [] (@{term "x + 1 + - 1 * 2::real"}, @{term "x + 1 + - 1 * 2::real"}) = false
15.39 +if rew_ord_ @{context} [] (@{term "x + 1 + - 1 * 2::real"}, @{term "x + 1 + - 1 * 2::real"}) = false
15.40 then () else error "term_ord' 1";
15.41
15.42 (*## not >: "1 + x + - 1 * 2" > "- 1 * 2 + (1 + x)" *)
15.43 -if rew_ord_ [] (@{term "1 + x + - 1 * 2::real"}, @{term "- 1 * 2 + (1 + x)::real"}) = true
15.44 +if rew_ord_ @{context} [] (@{term "1 + x + - 1 * 2::real"}, @{term "- 1 * 2 + (1 + x)::real"}) = true
15.45 then () else error "term_ord' 2";
15.46
15.47 (*## not >: "1 + x" > "x + 1" *)
15.48 -if rew_ord_ [] (@{term "1 + x::real"}, @{term "x + 1::real"}) = true
15.49 +if rew_ord_ @{context} [] (@{term "1 + x::real"}, @{term "x + 1::real"}) = true
15.50 then () else error "term_ord' 3";
15.51
15.52 (*## not >: "- 1 * 2" > "2 * - 1" *)
15.53 -if rew_ord_ [] (@{term "- 1 * 2::real"}, @{term "2 * - 1::real"}) = true
15.54 +if rew_ord_ @{context} [] (@{term "- 1 * 2::real"}, @{term "2 * - 1::real"}) = true
15.55 then () else error "term_ord' 4";
15.56
15.57 (*## not >: "1 + (x + - 2)" > "x + - 2 + 1" *)
15.58 -if rew_ord_ [] (@{term "1 + (x + - 2)::real"}, @{term "x + - 2 + 1::real"}) = true
15.59 +if rew_ord_ @{context} [] (@{term "1 + (x + - 2)::real"}, @{term "x + - 2 + 1::real"}) = true
15.60 then () else error "term_ord' 5";
15.61
15.62 (*## not >: "x + - 2" > "- 2 + x"*)
15.63 -if rew_ord_ [] (@{term "x + - 2::real"}, @{term "- 2 + x ::real"}) = false
15.64 +if rew_ord_ @{context} [] (@{term "x + - 2::real"}, @{term "- 2 + x ::real"}) = false
15.65 then () else error "term_ord' 5a"; (*<<<<<<<<<<<<<<----------------- false in trace isa2*)
15.66
15.67 (*--------------------------------- ordered rew. (NOT) inhibited*)
15.68
15.69 (*## not >: "1 + (-2 + x)" > "-2 + x + 1" *)
15.70 -if rew_ord_ [] (@{term "1 + (-2 + x)::real"}, @{term "-2 + x + 1::real"}) = true
15.71 +if rew_ord_ @{context} [] (@{term "1 + (-2 + x)::real"}, @{term "-2 + x + 1::real"}) = true
15.72 then () else error "term_ord' 6";
15.73
15.74 (*## not >: "- 2 + x" > "x + - 2" *)
15.75 -if rew_ord_ [] (@{term "- 2 + x::real"}, @{term "x + - 2::real"}) = true
15.76 +if rew_ord_ @{context} [] (@{term "- 2 + x::real"}, @{term "x + - 2::real"}) = true
15.77 then () else error "term_ord' 7";
15.78
15.79 (*## not >: "- 2 + (1 + x)" > "1 + (- 2 + x)" *)
15.80 -if rew_ord_ [] (@{term "- 2 + (1 + x)::real"}, @{term "1 + (- 2 + x)::real"}) = true
15.81 +if rew_ord_ @{context} [] (@{term "- 2 + (1 + x)::real"}, @{term "1 + (- 2 + x)::real"}) = true
15.82 then () else error "term_ord' 8";
15.83
15.84 (*## not > "- 1 + x" > "x + - 1" *)
15.85 -if rew_ord_ [] (@{term "- 1 + x::real"}, @{term "x + - 1::real"}) = true
15.86 +if rew_ord_ @{context} [] (@{term "- 1 + x::real"}, @{term "x + - 1::real"}) = true
15.87 then () else error "term_ord' 9";
16.1 --- a/test/Tools/isac/Interpret/error-pattern.sml Wed Nov 16 10:30:59 2022 +0100
16.2 +++ b/test/Tools/isac/Interpret/error-pattern.sml Wed Nov 16 17:42:41 2022 +0100
16.3 @@ -118,13 +118,13 @@
16.4
16.5 val fod = Derive.do_one (Proof_Context.init_global @{theory "Isac_Knowledge"}) Atools_erls
16.6 ((#rules o Rule_Set.rep) Test_simplify)
16.7 - (sqrt_right false (@{theory "Pure"})) NONE
16.8 + (sqrt_right false) NONE
16.9 (TermC.parse_test @{context} "x + 1 + - 1 * 2 = 0");
16.10 (writeln o Derive.trtas2str) fod;
16.11
16.12 val ifod = Derive.do_one (Proof_Context.init_global @{theory "Isac_Knowledge"}) Atools_erls
16.13 ((#rules o Rule_Set.rep) Test_simplify)
16.14 - (sqrt_right false (@{theory "Pure"})) NONE
16.15 + (sqrt_right false) NONE
16.16 (TermC.parse_test @{context} "- 2 * 1 + (1 + x) = 0");
16.17 (writeln o Derive.trtas2str) ifod;
16.18 fun equal (_,_,(t1, _)) (_,_,(t2, _)) = t1 = t2;
17.1 --- a/test/Tools/isac/Knowledge/eqsystem-1.sml Wed Nov 16 10:30:59 2022 +0100
17.2 +++ b/test/Tools/isac/Knowledge/eqsystem-1.sml Wed Nov 16 17:42:41 2022 +0100
17.3 @@ -124,28 +124,28 @@
17.4 "----------- rewrite-order ord_simplify_System -------------------";
17.5 "M_b x = c * x + - 1 * q_0 * (x \<up> 2 / 2) + c_2";
17.6 "--- add.commute ---"; (* ... add.commute cf. b42e334c97ee *)
17.7 -if ord_simplify_System false thy [] (TermC.parse_test @{context}"- 1 * q_0 * (x \<up> 2 / 2)",
17.8 +if ord_simplify_System false ctxt [] (TermC.parse_test @{context}"- 1 * q_0 * (x \<up> 2 / 2)",
17.9 TermC.parse_test @{context}"c * x") then ()
17.10 else error "integrate.sml, (- 1 * q_0 * (x \<up> 2 / 2)) < (c * x) not#1";
17.11
17.12 -if ord_simplify_System false thy [] (TermC.parse_test @{context}"- 1 * q_0 * (x \<up> 2 / 2)",
17.13 +if ord_simplify_System false ctxt [] (TermC.parse_test @{context}"- 1 * q_0 * (x \<up> 2 / 2)",
17.14 TermC.parse_test @{context}"c_2") then ()
17.15 else error "integrate.sml, (- 1 * q_0 * (x \<up> 2 / 2)) < (c_2) not#2";
17.16
17.17 -if ord_simplify_System false thy [] (TermC.parse_test @{context}"c * x",
17.18 +if ord_simplify_System false ctxt [] (TermC.parse_test @{context}"c * x",
17.19 TermC.parse_test @{context}"c_2") then ()
17.20 else error "integrate.sml, (c * x) < (c_2) not#3";
17.21
17.22 "--- mult.commute ---";
17.23 -if ord_simplify_System false thy [] (TermC.parse_test @{context}"x * c",
17.24 +if ord_simplify_System false ctxt [] (TermC.parse_test @{context}"x * c",
17.25 TermC.parse_test @{context}"c * x") then ()
17.26 else error "integrate.sml, (x * c) < (c * x) not#4";
17.27
17.28 -if ord_simplify_System false thy [] (TermC.parse_test @{context}"- 1 * q_0 * (x \<up> 2 / 2) * c",
17.29 +if ord_simplify_System false ctxt [] (TermC.parse_test @{context}"- 1 * q_0 * (x \<up> 2 / 2) * c",
17.30 TermC.parse_test @{context}"- 1 * q_0 * c * (x \<up> 2 / 2)")
17.31 then () else error "integrate.sml, (. * .) < (. * .) not#5";
17.32
17.33 -if ord_simplify_System false thy [] (TermC.parse_test @{context}"- 1 * q_0 * (x \<up> 2 / 2) * c",
17.34 +if ord_simplify_System false ctxt [] (TermC.parse_test @{context}"- 1 * q_0 * (x \<up> 2 / 2) * c",
17.35 TermC.parse_test @{context}"c * - 1 * q_0 * (x \<up> 2 / 2)")
17.36 then () else error "integrate.sml, (. * .) < (. * .) not#6";
17.37
17.38 @@ -240,7 +240,7 @@
17.39 else error "eqsystem.sml top_down_substitution,2x2] order_system";
17.40
17.41 if not (ord_simplify_System
17.42 - false thy []
17.43 + false ctxt []
17.44 (TermC.parse_test @{context}"[c_2 = 77, c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L]",
17.45 TermC.parse_test @{context}"[c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L, c_2 = 77]"))
17.46 then () else error "eqsystem.sml, order_result rew_ord";
18.1 --- a/test/Tools/isac/Knowledge/poly-2.sml Wed Nov 16 10:30:59 2022 +0100
18.2 +++ b/test/Tools/isac/Knowledge/poly-2.sml Wed Nov 16 17:42:41 2022 +0100
18.3 @@ -693,7 +693,7 @@
18.4 val t1 = TermC.parse_test @{context} "2 * b + (3 * a + 3 * b)";
18.5 val t2 = TermC.parse_test @{context} "(3 * a + 3 * b) + 2 * b";
18.6
18.7 -if ord_make_polynomial true @{theory} [] (t1, t2) then ()
18.8 +if ord_make_polynomial true @{context} [] (t1, t2) then ()
18.9 else error "poly.sml: diff.behav. in ord_make_polynomial";
18.10 (*SO: WHY IS THERE NO REWRITING ...*)
18.11
19.1 --- a/test/Tools/isac/Knowledge/polyminus.sml Wed Nov 16 10:30:59 2022 +0100
19.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml Wed Nov 16 17:42:41 2022 +0100
19.3 @@ -170,13 +170,13 @@
19.4 "----------- watch order_add_mult -------------------------------";
19.5 "----- with these simple variables it works...";
19.6 val ctxt = @{context};
19.7 -val t = TermC.parse_test @{context} "((a + d) + c) + b";
19.8 +val t = TermC.parse_test ctxt "((a + d) + c) + b";
19.9 val SOME (t,_) = rewrite_set_ ctxt false order_add_mult t; UnparseC.term t;
19.10 if UnparseC.term t = "a + (b + (c + d))" then ()
19.11 else error "polyminus.sml 1 watch order_add_mult";
19.12
19.13 "----- the same stepwise...";
19.14 -val od = ord_make_polynomial true (@{theory "Poly"});
19.15 +val od = ord_make_polynomial true
19.16 val t = TermC.parse_test @{context} "((a + d) + c) + b";
19.17 "((a + d) + c) + b";
19.18 val SOME (t,_) = rewrite_ ctxt od Rule_Set.empty true @{thm add.commute} t; UnparseC.term t;
19.19 @@ -208,7 +208,7 @@
19.20 else error "polyminus.sml: order_add_mult changed";
19.21
19.22 "----- here we see rew_sub going into subterm with ord.rew....";
19.23 -val od = ord_make_polynomial false (@{theory "Poly"});
19.24 +val od = ord_make_polynomial false;
19.25 val t = TermC.parse_test @{context} "b + a + c + d";
19.26 val SOME (t,_) = rewrite_ ctxt od Rule_Set.empty false @{thm add.commute} t; UnparseC.term t;
19.27 val SOME (t,_) = rewrite_ ctxt od Rule_Set.empty false @{thm add.commute} t; UnparseC.term t;
20.1 --- a/test/Tools/isac/MathEngBasic/rewrite.sml Wed Nov 16 10:30:59 2022 +0100
20.2 +++ b/test/Tools/isac/MathEngBasic/rewrite.sml Wed Nov 16 17:42:41 2022 +0100
20.3 @@ -100,8 +100,8 @@
20.4 val SOME (r, _) = (rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.empty false thm tm);
20.5
20.6 "----- ordered rewriting";
20.7 -fun tord (_:subst) pp = LibraryC.termless pp;
20.8 -if tord [] (@{term "x + y*z::real"}, @{term "y*z + x::real"}) then ()
20.9 +fun tord (_:Proof.context) (_:subst) pp = LibraryC.termless pp;
20.10 +if tord @{context} [] (@{term "x + y*z::real"}, @{term "y*z + x::real"}) then ()
20.11 else error "rewrite.sml diff.behav. in ord.rewr.";
20.12
20.13 val NONE = (rewrite_ ctxt tord Rule_Set.empty false thm tm);
21.1 --- a/test/Tools/isac/Test_Isac.thy Wed Nov 16 10:30:59 2022 +0100
21.2 +++ b/test/Tools/isac/Test_Isac.thy Wed Nov 16 17:42:41 2022 +0100
21.3 @@ -306,7 +306,7 @@
21.4 ML_file "Knowledge/descript.sml"
21.5 ML_file "Knowledge/simplify.sml"
21.6 ML_file "Knowledge/poly-1.sml"
21.7 - ML_file "Knowledge/poly-2.sml" (*Test_Isac_Short*)
21.8 + ML_file "Knowledge/poly-2.sml" (*Test_Isac_Short*)
21.9 ML_file "Knowledge/gcd_poly_ml.sml"
21.10 ML_file "Knowledge/rational-1.sml"
21.11 ML_file "Knowledge/rational-2.sml" (*Test_Isac_Short*)