# HG changeset patch # User wneuper # Date 1668616961 -3600 # Node ID 439f7f3867ecc35aa75ecae20b87023bfefd1b28 # Parent 48c31909de24c2468c2e5194f60346c837c9ed37 make Minisubplb/200-start-method independent #3: Rewrite_Ord.T with ctxt diff -r 48c31909de24 -r 439f7f3867ec src/Tools/isac/BaseDefinitions/rewrite-order.sml --- a/src/Tools/isac/BaseDefinitions/rewrite-order.sml Wed Nov 16 10:30:59 2022 +0100 +++ b/src/Tools/isac/BaseDefinitions/rewrite-order.sml Wed Nov 16 17:42:41 2022 +0100 @@ -26,7 +26,7 @@ val id_empty = "Rewrite_Ord.id_empty"; type function = Rule_Def.rew_ord_function; -fun function_empty (_: LibraryC.subst) (_: term, _: term) = true; +fun function_empty (_: Proof.context) (_: LibraryC.subst) (_: term, _: term) = true; type T = Rule_Def.rew_ord_T val empty = (id_empty, function_empty) diff -r 48c31909de24 -r 439f7f3867ec src/Tools/isac/BaseDefinitions/rule-def.sml --- a/src/Tools/isac/BaseDefinitions/rule-def.sml Wed Nov 16 10:30:59 2022 +0100 +++ b/src/Tools/isac/BaseDefinitions/rule-def.sml Wed Nov 16 17:42:41 2022 +0100 @@ -14,7 +14,7 @@ eqtype errpatID type rew_ord_id = string - type rew_ord_function = LibraryC.subst -> term * term -> bool + type rew_ord_function = Proof.context -> LibraryC.subst -> term * term -> bool type rew_ord_T = rew_ord_id * rew_ord_function @@ -48,7 +48,7 @@ type eval_fn = string -> term -> Proof.context -> (string * term) option; type rew_ord_id = string; -type rew_ord_function = LibraryC.subst -> term * term -> bool; +type rew_ord_function = Proof.context -> LibraryC.subst -> term * term -> bool; type rew_ord_T = rew_ord_id * rew_ord_function; type eval_const_id = string; diff -r 48c31909de24 -r 439f7f3867ec src/Tools/isac/BaseDefinitions/rule-set.sml --- a/src/Tools/isac/BaseDefinitions/rule-set.sml Wed Nov 16 10:30:59 2022 +0100 +++ b/src/Tools/isac/BaseDefinitions/rule-set.sml Wed Nov 16 17:42:41 2022 +0100 @@ -46,7 +46,7 @@ type id = string; (*/------- this will disappear eventually ----------------------------------------------------\*) -fun dummy_ord (_: LibraryC.subst) (_: term, _: term) = true; +val dummy_ord = Rewrite_Ord.function_empty; val empty = Rule_Def.Repeat {id = "empty", preconds = [], rew_ord = ("dummy_ord", dummy_ord), asm_rls = Rule_Def.Empty, prog_rls = Rule_Def.Empty, calc = [], rules = [], errpatts = [], program = Rule_Def.Empty_Prog} diff -r 48c31909de24 -r 439f7f3867ec src/Tools/isac/BaseDefinitions/thy-write.sml --- a/src/Tools/isac/BaseDefinitions/thy-write.sml Wed Nov 16 10:30:59 2022 +0100 +++ b/src/Tools/isac/BaseDefinitions/thy-write.sml Wed Nov 16 17:42:41 2022 +0100 @@ -56,7 +56,7 @@ | Hrls of {guh: Check_Unique.id, coursedesign: authors, mathauthors: authors, thy_rls: (ThyC.id * Rule_Set.T)} | Hcal of {guh: Check_Unique.id, coursedesign: authors, mathauthors: authors, calc: Rule_Def.eval_ml_from_prog} | Hord of {guh: Check_Unique.id, coursedesign: authors, mathauthors: authors, - ord: (subst -> (term * term) -> bool)}; + ord: (Proof.context -> subst -> (term * term) -> bool)}; fun the2str (Html {guh, ...}) = guh | the2str (Hthm {guh, ...}) = guh | the2str (Hrls {guh, ...}) = guh diff -r 48c31909de24 -r 439f7f3867ec src/Tools/isac/Knowledge/Base_Tools.thy --- a/src/Tools/isac/Knowledge/Base_Tools.thy Wed Nov 16 10:30:59 2022 +0100 +++ b/src/Tools/isac/Knowledge/Base_Tools.thy Wed Nov 16 17:42:41 2022 +0100 @@ -46,8 +46,8 @@ local open Term; in - fun termlessI (_: subst) uv = LibraryC.termless uv; - fun term_ordI (_: subst) uv = Term_Ord.term_ord uv; + fun termlessI (_: Proof.context) (_: subst) uv = LibraryC.termless uv; + fun term_ordI (_: Proof.context) (_: subst) uv = Term_Ord.term_ord uv; end; \ ML \ (*TODO.WN0509 reduce ids: tless_true = e_rew_ord' = Rewrite_Ord.function_empty = Rewrite_Ord.function_empty*) diff -r 48c31909de24 -r 439f7f3867ec src/Tools/isac/Knowledge/EqSystem.thy --- a/src/Tools/isac/Knowledge/EqSystem.thy Wed Nov 16 10:30:59 2022 +0100 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Wed Nov 16 17:42:41 2022 +0100 @@ -119,22 +119,22 @@ | size_of_term' (f$t) = size_of_term' f + size_of_term' t | size_of_term' _ = 1; -fun term_ord' pr thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *) - (case term_ord' pr thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord) - | term_ord' pr thy (t, u) = +fun term_ord' pr ctxt (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *) + (case term_ord' pr ctxt (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord) + | term_ord' pr ctxt (t, u) = (if pr then let val (f, ts) = strip_comb t and (g, us) = strip_comb u; - val _ = tracing ("t= f @ ts= \"" ^ UnparseC.term_in_thy thy f ^ "\" @ \"[" ^ - commas (map (UnparseC.term_in_thy thy) ts) ^ "]\""); - val _ = tracing ("u= g @ us= \"" ^ UnparseC.term_in_thy thy g ^ "\" @ \"[" ^ - commas (map (UnparseC.term_in_thy thy) us) ^ "]\""); + val _ = tracing ("t= f @ ts= \"" ^ UnparseC.term_in_ctxt ctxt f ^ "\" @ \"[" ^ + commas (map (UnparseC.term_in_ctxt ctxt) ts) ^ "]\""); + val _ = tracing ("u= g @ us= \"" ^ UnparseC.term_in_ctxt ctxt g ^ "\" @ \"[" ^ + commas (map (UnparseC.term_in_ctxt ctxt) us) ^ "]\""); val _ = tracing ("size_of_term (t, u) = (" ^ string_of_int (size_of_term' t) ^ ", " ^ string_of_int (size_of_term' u) ^ ")"); val _ = tracing ("hd_ord (f, g) = " ^ ((pr_ord o hd_ord) (f, g)) ); (** )val _ = @{print tracing}{a = "hd_ord (f, g) = ", z = hd_ord (f, g)}( **) - val _ = tracing ("terms_ord (ts, us) = " ^(pr_ord o terms_ord str false) (ts,us)); + val _ = tracing ("terms_ord (ts, us) = " ^ (pr_ord o terms_ord str false ctxt) (ts,us) ); val _= tracing ("-------"); in () end else (); @@ -142,13 +142,13 @@ EQUAL => let val (f, ts) = strip_comb t and (g, us) = strip_comb u in (case hd_ord (f, g) of - EQUAL => (terms_ord str pr) (ts, us) + EQUAL => (terms_ord str pr ctxt) (ts, us) | ord => ord) end - | ord => ord) + | ord => ord) and hd_ord (f, g) = (* ~ term.ML *) prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord (dest_hd' f, dest_hd' g) -and terms_ord _ pr (ts, us) = list_ord (term_ord' pr (ThyC.get_theory "Isac_Knowledge"))(ts, us); +and terms_ord _ pr ctxt (ts, us) = list_ord (term_ord' pr ctxt) (ts, us); (**) in (**) @@ -164,7 +164,7 @@ \ ML \ \ setup \Know_Store.add_rew_ords [ - ("ord_simplify_System", ord_simplify_System false \<^theory>)]\ + ("ord_simplify_System", ord_simplify_System false)]\ ML \ (** rulesets **) @@ -173,7 +173,7 @@ val order_add_mult_System = Rule_Def.Repeat{ id = "order_add_mult_System", preconds = [], - rew_ord = ("ord_simplify_System", ord_simplify_System false @{theory "Integrate"}), + rew_ord = ("ord_simplify_System", ord_simplify_System false), asm_rls = Rule_Set.empty,prog_rls = Rule_Set.Empty, calc = [], errpatts = [], rules = [ \<^rule_thm>\mult.commute\, (* z * w = w * z *) @@ -310,7 +310,7 @@ appears as [..c_4 = .., ..., ..., ..c_1 + ..c_2 + ..c_3 ..c_4 = ..].*) val order_system = Rule_Def.Repeat {id="order_system", preconds = [], - rew_ord = ("ord_simplify_System", ord_simplify_System false \<^theory>), + rew_ord = ("ord_simplify_System", ord_simplify_System false), asm_rls = Rule_Set.Empty, prog_rls = Rule_Set.Empty, calc = [], errpatts = [], rules = [ \<^rule_thm>\order_system_NxN\], diff -r 48c31909de24 -r 439f7f3867ec src/Tools/isac/Knowledge/Poly.thy --- a/src/Tools/isac/Knowledge/Poly.thy Wed Nov 16 10:30:59 2022 +0100 +++ b/src/Tools/isac/Knowledge/Poly.thy Wed Nov 16 17:42:41 2022 +0100 @@ -514,45 +514,49 @@ | size_of_term' (f$t) = size_of_term' f + size_of_term' t | size_of_term' _ = 1; -fun term_ord' pr thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *) - (case term_ord' pr thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord) - | term_ord' pr thy (t, u) = +fun term_ord' pr ctxt (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *) + (case term_ord' pr ctxt (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord) + | term_ord' pr ctxt (t, u) = (if pr then let val (f, ts) = strip_comb t and (g, us) = strip_comb u; - val _ = tracing ("t= f@ts= \"" ^ UnparseC.term_in_thy thy f ^ "\" @ \"[" ^ - commas (map (UnparseC.term_in_thy thy) ts) ^ "]\""); - val _ = tracing("u= g@us= \"" ^ UnparseC.term_in_thy thy g ^ "\" @ \"[" ^ - commas (map (UnparseC.term_in_thy thy) us) ^ "]\""); + val _ = tracing ("t= f@ts= \"" ^ UnparseC.term_in_ctxt ctxt f ^ "\" @ \"[" ^ + commas (map (UnparseC.term_in_ctxt ctxt) ts) ^ "]\""); + val _ = tracing("u= g@us= \"" ^ UnparseC.term_in_ctxt ctxt g ^ "\" @ \"[" ^ + commas (map (UnparseC.term_in_ctxt ctxt) us) ^ "]\""); val _ = tracing ("size_of_term(t,u)= (" ^ string_of_int (size_of_term' t) ^ ", " ^ string_of_int (size_of_term' u) ^ ")"); val _ = tracing ("hd_ord(f,g) = " ^ (pr_ord o hd_ord) (f,g)); - val _ = tracing ("terms_ord(ts,us) = " ^ (pr_ord o terms_ord str false) (ts, us)); + val _ = tracing ("terms_ord(ts,us) = " ^ (pr_ord o terms_ord str false ctxt) (ts, us)); val _ = tracing ("-------"); in () end else (); case int_ord (size_of_term' t, size_of_term' u) of EQUAL => let val (f, ts) = strip_comb t and (g, us) = strip_comb u in - (case hd_ord (f, g) of EQUAL => (terms_ord str pr) (ts, us) + (case hd_ord (f, g) of EQUAL => (terms_ord str pr ctxt) (ts, us) | ord => ord) end | ord => ord) and hd_ord (f, g) = (* ~ term.ML *) prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord (dest_hd' f, dest_hd' g) -and terms_ord _ pr (ts, us) = - list_ord (term_ord' pr (ThyC.get_theory "Isac_Knowledge"))(ts, us); +and terms_ord _ pr ctxt (ts, us) = + list_ord (term_ord' pr ctxt) (ts, us); in -fun ord_make_polynomial (pr:bool) thy (_: subst) (ts, us) = - (term_ord' pr thy(***) (TermC.numerals_to_Free ts, TermC.numerals_to_Free us) = LESS ); +fun ord_make_polynomial (pr:bool) ctxt (_: subst) (ts, us) = + (term_ord' pr ctxt (TermC.numerals_to_Free ts, TermC.numerals_to_Free us) = LESS ); end;(*local*) +\ ML \ +ord_make_polynomial +\ ML \ +\ ML \ \ setup \Know_Store.add_rew_ords [ ("termlessI", termlessI), - ("ord_make_polynomial", ord_make_polynomial false \<^theory>)]\ + ("ord_make_polynomial", ord_make_polynomial false)]\ subsection \predicates\ subsubsection \in specifications\ @@ -989,7 +993,7 @@ (total-degree-)ordering of monoms NOT possible with size_of_term GIVEN*) val order_add_mult = Rule_Def.Repeat{id = "order_add_mult", preconds = [], - rew_ord = ("ord_make_polynomial", ord_make_polynomial false \<^theory>), + rew_ord = ("ord_make_polynomial", ord_make_polynomial false), asm_rls = Rule_Set.empty,prog_rls = Rule_Set.Empty, calc = [], errpatts = [], rules = [ @@ -1004,7 +1008,7 @@ (total-degree-)ordering of monoms NOT possible with size_of_term GIVEN*) val order_mult = Rule_Def.Repeat{id = "order_mult", preconds = [], - rew_ord = ("ord_make_polynomial",ord_make_polynomial false \<^theory>), + rew_ord = ("ord_make_polynomial",ord_make_polynomial false), asm_rls = Rule_Set.empty,prog_rls = Rule_Set.Empty, calc = [], errpatts = [], rules = [ diff -r 48c31909de24 -r 439f7f3867ec src/Tools/isac/Knowledge/PolyEq.thy --- a/src/Tools/isac/Knowledge/PolyEq.thy Wed Nov 16 10:30:59 2022 +0100 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Wed Nov 16 17:42:41 2022 +0100 @@ -1060,59 +1060,64 @@ | _ => raise ERROR ("size_of_term' called with subst = " ^ UnparseC.term x)) | _ => (if pr then tracing (idt "#" i ^ "bot --> " ^ "1") else (); 1)); -fun term_ord' i pr x thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *) +fun term_ord' i pr x ctxt (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *) let val _ = if pr then tracing (idt "#" i ^ "term_ord' Abs") else (); val ord = - case term_ord' (i + 1) pr x thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord + case term_ord' (i + 1) pr x ctxt (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord val _ = if pr then tracing (idt "#" i ^ "term_ord' Abs --> " ^ pr_ord ord) else () in ord end - | term_ord' i pr x _ (t, u) = + | term_ord' i pr x ctxt (t, u) = let - val _ = if pr then tracing (idt "#" i ^ "term_ord' bot (" ^ UnparseC.term t ^ ", " ^ UnparseC.term u ^ ")") else (); + val _ = if pr then tracing (idt "#" i ^ "term_ord' bot (" ^ UnparseC.term_in_ctxt ctxt t ^ + ", " ^ UnparseC.term_in_ctxt ctxt u ^ ")") else (); val ord = case int_ord (size_of_term' (i + 1) pr x t, size_of_term' (i + 1) pr x u) of EQUAL => let val (f, ts) = strip_comb t and (g, us) = strip_comb u in - (case hd_ord (i + 1) pr x (f, g) of - EQUAL => (terms_ord x (i + 1) pr) (ts, us) + (case hd_ord (i + 1) pr x ctxt (f, g) of + EQUAL => (terms_ord x (i + 1) pr ctxt) (ts, us) | ord => ord) end | ord => ord val _ = if pr then tracing (idt "#" i ^ "term_ord' bot --> " ^ pr_ord ord) else () in ord end -and hd_ord i pr x (f, g) = (* ~ term.ML *) +and hd_ord i pr x ctxt (f, g) = (* ~ term.ML *) let - val _ = if pr then tracing (idt "#" i ^ "hd_ord (" ^ UnparseC.term f ^ ", " ^ UnparseC.term g ^ ")") else (); + val _ = if pr then tracing (idt "#" i ^ "hd_ord (" ^ UnparseC.term_in_ctxt ctxt f ^ + ", " ^ UnparseC.term g ^ ")") else (); val ord = prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord (dest_hd' x f, dest_hd' x g) val _ = if pr then tracing (idt "#" i ^ "hd_ord --> " ^ pr_ord ord) else (); in ord end -and terms_ord x i pr (ts, us) = +and terms_ord x i pr ctxt (ts, us) = let - val _ = if pr then tracing (idt "#" i ^ "terms_ord (" ^ UnparseC.terms ts ^ ", " ^ UnparseC.terms us ^ ")") else (); - val ord = list_ord (term_ord' (i + 1) pr x (ThyC.get_theory "Isac_Knowledge"))(ts, us); + val _ = if pr then tracing (idt "#" i ^ "terms_ord (" ^ UnparseC.terms_in_ctxt ctxt ts ^ + ", " ^ UnparseC.terms_in_ctxt ctxt us ^ ")") else (); + val ord = list_ord (term_ord' (i + 1) pr x ctxt) (ts, us); val _ = if pr then tracing (idt "#" i ^ "terms_ord --> " ^ pr_ord ord) else (); in ord end (**)in(*local*) -fun ord_make_polynomial_in (pr:bool) thy subst (ts, us) = +fun ord_make_polynomial_in (pr:bool) ctxt subst (ts, us) = ((** )tracing ("*** subs variable is: " ^ Env.subst2str subst); ( **) case subst of (_, x) :: _ => - term_ord' 1 pr x thy (TermC.numerals_to_Free ts, TermC.numerals_to_Free us) = LESS + term_ord' 1 pr x ctxt (TermC.numerals_to_Free ts, TermC.numerals_to_Free us) = LESS | _ => raise ERROR ("ord_make_polynomial_in called with subst = " ^ Env.subst2str subst)) end;(*local*) - +\ ML \ +ord_make_polynomial_in +\ ML \ \ ML\ val order_add_mult_in = prep_rls'( Rule_Def.Repeat{id = "order_add_mult_in", preconds = [], - rew_ord = ("ord_make_polynomial_in", ord_make_polynomial_in false @{theory "Poly"}), + rew_ord = ("ord_make_polynomial_in", ord_make_polynomial_in false), asm_rls = Rule_Set.empty,prog_rls = Rule_Set.Empty, calc = [], errpatts = [], rules = [ diff -r 48c31909de24 -r 439f7f3867ec src/Tools/isac/Knowledge/Rational.thy --- a/src/Tools/isac/Knowledge/Rational.thy Wed Nov 16 10:30:59 2022 +0100 +++ b/src/Tools/isac/Knowledge/Rational.thy Wed Nov 16 17:42:41 2022 +0100 @@ -513,7 +513,7 @@ val cancel_p = Rule_Set.Rrls {id = "cancel_p", prepat = [], - rew_ord = ("ord_make_polynomial", ord_make_polynomial false \<^theory>), + rew_ord = ("ord_make_polynomial", ord_make_polynomial false), asm_rls = rational_erls, calc = [("PLUS", (\<^const_name>\plus\, (**)Calc_Binop.numeric "#add_")), @@ -581,7 +581,7 @@ val add_fractions_p = Rule_Set.Rrls {id = "add_fractions_p", prepat=prepat, - rew_ord = ("ord_make_polynomial", ord_make_polynomial false \<^theory>), + rew_ord = ("ord_make_polynomial", ord_make_polynomial false), asm_rls = rational_erls, calc = [("PLUS", (\<^const_name>\plus\, (**)Calc_Binop.numeric "#add_")), ("TIMES", (\<^const_name>\times\, (**)Calc_Binop.numeric "#mult_")), diff -r 48c31909de24 -r 439f7f3867ec src/Tools/isac/Knowledge/Root.thy --- a/src/Tools/isac/Knowledge/Root.thy Wed Nov 16 10:30:59 2022 +0100 +++ b/src/Tools/isac/Knowledge/Root.thy Wed Nov 16 17:42:41 2022 +0100 @@ -101,38 +101,37 @@ | size_of_term' (Abs (_,_,body)) = 1 + size_of_term' body | size_of_term' (f $ t) = size_of_term' f + size_of_term' t | size_of_term' _ = 1; -fun term_ord' pr thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *) - (case term_ord' pr thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U) +fun term_ord' pr ctxt (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *) + (case term_ord' pr ctxt (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord) - | term_ord' pr thy (t, u) = - (if pr then - let - val (f, ts) = strip_comb t and (g, us) = strip_comb u; - val _ = tracing ("t= f@ts= \"" ^ UnparseC.term_in_ctxt (Proof_Context.init_global thy) f ^"\" @ \"[" ^ - commas (map (UnparseC.term_in_ctxt (Proof_Context.init_global thy)) ts) ^ "]\""); - val _ = tracing ("u= g@us= \"" ^ UnparseC.term g ^"\" @ \"[" ^ - commas (map (UnparseC.term_in_ctxt (Proof_Context.init_global thy)) us) ^ "]\""); - val _ = tracing ("size_of_term(t,u)= (" ^ - string_of_int(size_of_term' t) ^", " ^ - string_of_int(size_of_term' u) ^")"); - val _ = tracing ("hd_ord(f,g) = " ^ (pr_ord o hd_ord) (f,g)); - val _ = tracing ("terms_ord(ts,us) = " ^ - (pr_ord o terms_ord str false) (ts,us)); - val _=tracing("-------"); - in () end + | term_ord' pr ctxt (t, u) = + (if pr + then + let + val (f, ts) = strip_comb t and (g, us) = strip_comb u; + val _ = tracing ("t= f@ts= \"" ^ UnparseC.term_in_ctxt ctxt f ^"\" @ \"[" ^ + commas (map (UnparseC.term_in_ctxt ctxt) ts) ^ "]\""); + val _ = tracing ("u= g@us= \"" ^ UnparseC.term g ^"\" @ \"[" ^ + commas (map (UnparseC.term_in_ctxt ctxt) us) ^ "]\""); + val _ = tracing ("size_of_term(t,u)= (" ^ + string_of_int(size_of_term' t) ^", " ^ + string_of_int(size_of_term' u) ^")"); + val _ = tracing ("hd_ord(f,g) = " ^ (pr_ord o hd_ord) (f,g)); + val _ = tracing ("terms_ord(ts,us) = " ^ (pr_ord o terms_ord str false ctxt) (ts,us)); + val _=tracing("-------"); + in () end else (); - case int_ord (size_of_term' t, size_of_term' u) of - EQUAL => - let val (f, ts) = strip_comb t and (g, us) = strip_comb u in - (case hd_ord (f, g) of EQUAL => (terms_ord str pr) (ts, us) - | ord => ord) - end - | ord => ord) + case int_ord (size_of_term' t, size_of_term' u) of + EQUAL => + let val (f, ts) = strip_comb t and (g, us) = strip_comb u + in (case hd_ord (f, g) of + EQUAL => (terms_ord str pr ctxt) (ts, us) + | ord => ord) + end + | ord => ord) and hd_ord (f, g) = (* ~ term.ML *) - prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord - (dest_hd' f, dest_hd' g) -and terms_ord _(*str*) pr (ts, us) = - list_ord (term_ord' pr (ThyC.get_theory "Isac_Knowledge"))(ts, us); + prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord (dest_hd' f, dest_hd' g) +and terms_ord _(*str*) pr ctxt (ts, us) = list_ord (term_ord' pr ctxt) (ts, us); in (* associates a+(b+c) => (a+b)+c = a+b+c ... avoiding parentheses @@ -143,17 +142,19 @@ (*args pr: print trace, WN0509 'sqrt_right true' not used anymore - thy: + ctxt: subst: no bound variables, only Root.sqrt tu: the terms to compare (t1, t2) ... *) -fun sqrt_right (pr:bool) thy (_: subst) (ts, us) = - (term_ord' pr thy(***) (TermC.numerals_to_Free ts, TermC.numerals_to_Free us) = LESS ); +fun sqrt_right (pr:bool) ctxt (_: subst) (ts, us) = + (term_ord' pr ctxt (TermC.numerals_to_Free ts, TermC.numerals_to_Free us) = LESS ); end; \ ML \ +\ ML \ +sqrt_right: bool -> Proof.context -> Subst.T -> term * term -> bool \ setup \Know_Store.add_rew_ords [ ("termlessI", termlessI), - ("sqrt_right", sqrt_right false @{theory "Pure"})]\ + ("sqrt_right", sqrt_right false)]\ ML \ (*------------------------- rules -------------------------*) @@ -189,7 +190,7 @@ val make_rooteq = prep_rls'( Rule_Def.Repeat{id = "make_rooteq", preconds = []:term list, - rew_ord = ("sqrt_right", sqrt_right false \<^theory>), + rew_ord = ("sqrt_right", sqrt_right false), asm_rls = Atools_erls, prog_rls = Rule_Set.Empty, calc = [], errpatts = [], rules = [ diff -r 48c31909de24 -r 439f7f3867ec src/Tools/isac/Knowledge/Test.thy --- a/src/Tools/isac/Knowledge/Test.thy Wed Nov 16 10:30:59 2022 +0100 +++ b/src/Tools/isac/Knowledge/Test.thy Wed Nov 16 17:42:41 2022 +0100 @@ -313,36 +313,35 @@ | size_of_term' (Abs (_,_,body)) = 1 + size_of_term' body | size_of_term' (f$t) = size_of_term' f + size_of_term' t | size_of_term' _ = 1; -fun term_ord' pr thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *) - (case term_ord' pr thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U) +fun term_ord' pr ctxt (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *) + (case term_ord' pr ctxt (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord) - | term_ord' pr _ (t, u) = + | term_ord' pr ctxt (t, u) = (if pr then let val (f, ts) = strip_comb t and (g, us) = strip_comb u; - val _ = tracing ("t= f@ts= \"" ^ UnparseC.term f ^ "\" @ \"[" ^ - commas(map UnparseC.term ts) ^ "]\"") - val _ = tracing ("u= g@us= \"" ^ UnparseC.term g ^"\" @ \"[" ^ - commas(map UnparseC.term us) ^"]\"") + val _ = tracing ("t= f@ts= \"" ^ UnparseC.term_in_ctxt ctxt f ^ "\" @ \"[" ^ + commas (map (UnparseC.term_in_ctxt ctxt) ts) ^ "]\"") + val _ = tracing ("u= g@us= \"" ^ UnparseC.term_in_ctxt ctxt g ^"\" @ \"[" ^ + commas (map (UnparseC.term_in_ctxt ctxt) us) ^"]\"") val _ = tracing ("size_of_term(t,u)= (" ^ string_of_int (size_of_term' t) ^ ", " ^ string_of_int (size_of_term' u) ^ ")") val _ = tracing ("hd_ord(f,g) = " ^ (pr_ord o hd_ord) (f,g)) val _ = tracing ("terms_ord(ts,us) = " ^ - (pr_ord o terms_ord str false) (ts,us)); + (pr_ord o terms_ord str false ctxt) (ts,us)); val _ = tracing "-------" in () end else (); case int_ord (size_of_term' t, size_of_term' u) of EQUAL => let val (f, ts) = strip_comb t and (g, us) = strip_comb u in - (case hd_ord (f, g) of EQUAL => (terms_ord str pr) (ts, us) + (case hd_ord (f, g) of EQUAL => (terms_ord str pr ctxt) (ts, us) | ord => ord) end | ord => ord) and hd_ord (f, g) = (* ~ term.ML *) prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord (dest_hd' f, dest_hd' g) -and terms_ord _ pr (ts, us) = - list_ord (term_ord' pr (ThyC.get_theory "Isac_Knowledge"))(ts, us); +and terms_ord _ pr ctxt (ts, us) = list_ord (term_ord' pr ctxt) (ts, us); in fun ord_make_polytest (pr:bool) thy (_: subst) (ts, us) = @@ -353,7 +352,7 @@ section \term order\ ML \ -fun term_order (_: subst) tu = (term_ordI [] tu = LESS); +val term_order = Rewrite_Ord.function_empty; \ section \rulesets\ @@ -393,7 +392,7 @@ (*FIXXXXXXME 10.8.02: handle like _simplify*) val tval_rls = Rule_Def.Repeat{id = "tval_rls", preconds = [], - rew_ord = ("sqrt_right",sqrt_right false @{theory "Pure"}), + rew_ord = ("sqrt_right",sqrt_right false), asm_rls=testerls,prog_rls = Rule_Set.empty, calc=[], errpatts = [], rules = [ @@ -439,16 +438,17 @@ val rearrange_assoc = Rule_Def.Repeat{ id = "rearrange_assoc", preconds = [], - rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty), + rew_ord = ("Rewrite_Ord.id_empty", Rewrite_Ord.function_empty), asm_rls = Rule_Set.empty, prog_rls = Rule_Set.empty, calc = [], errpatts = [], rules = [ \<^rule_thm_sym>\add.assoc\, \<^rule_thm_sym>\rmult_assoc\], program = Rule.Empty_Prog}; +\ ML \ val ac_plus_times = Rule_Def.Repeat{ - id = "ac_plus_times", preconds = [], rew_ord = ("term_order",term_order), + id = "ac_plus_times", preconds = [], rew_ord = ("term_order", term_order), asm_rls = Rule_Set.empty, prog_rls = Rule_Set.empty, calc = [], errpatts = [], rules = [ \<^rule_thm>\radd_commute\, @@ -458,6 +458,7 @@ \<^rule_thm>\rmult_left_commute\, \<^rule_thm>\rmult_assoc\], program = Rule.Empty_Prog}; +\ ML \ (*todo: replace by Rewrite("rnorm_equation_add", @{thm rnorm_equation_add)*) val norm_equation = @@ -466,13 +467,12 @@ rules = [ \<^rule_thm>\rnorm_equation_add\], program = Rule.Empty_Prog}; -\ -ML \ +\ ML \ (* expects * distributed over + *) val Test_simplify = Rule_Def.Repeat{ id = "Test_simplify", preconds = [], - rew_ord = ("sqrt_right", sqrt_right false @{theory "Pure"}), + rew_ord = ("sqrt_right", sqrt_right false), asm_rls = tval_rls, prog_rls = Rule_Set.empty, calc=[(*since 040209 filled by prep_rls'*)], errpatts = [], rules = [ @@ -591,12 +591,12 @@ setup \Know_Store.add_rew_ords [ ("termlessI", termlessI), - ("ord_make_polytest", ord_make_polytest false \<^theory>)]\ + ("ord_make_polytest", ord_make_polytest false)]\ ML \ val make_polytest = Rule_Def.Repeat{id = "make_polytest", preconds = []:term list, - rew_ord = ("ord_make_polytest", ord_make_polytest false @{theory "Poly"}), + rew_ord = ("ord_make_polytest", ord_make_polytest false), asm_rls = testerls, prog_rls = Rule_Set.Empty, calc = [ ("PLUS" , (\<^const_name>\plus\, (**)Calc_Binop.numeric "#add_")), diff -r 48c31909de24 -r 439f7f3867ec src/Tools/isac/Knowledge/Test_Build_Thydata.thy --- a/src/Tools/isac/Knowledge/Test_Build_Thydata.thy Wed Nov 16 10:30:59 2022 +0100 +++ b/src/Tools/isac/Knowledge/Test_Build_Thydata.thy Wed Nov 16 17:42:41 2022 +0100 @@ -6,7 +6,7 @@ ML \ open Rule -fun termlessI (_: subst) uv = LibraryC.termless uv; +fun termlessI (_: Proof.context) (_: subst) uv = LibraryC.termless uv; \ axiomatization where thm111: "thm111 = thm111 + (111::int)" and diff -r 48c31909de24 -r 439f7f3867ec src/Tools/isac/MathEngBasic/MathEngBasic.thy --- a/src/Tools/isac/MathEngBasic/MathEngBasic.thy Wed Nov 16 10:30:59 2022 +0100 +++ b/src/Tools/isac/MathEngBasic/MathEngBasic.thy Wed Nov 16 17:42:41 2022 +0100 @@ -47,6 +47,7 @@ ML \ \ ML \ +Rewrite_Ord.function_empty \ ML \ \ end diff -r 48c31909de24 -r 439f7f3867ec src/Tools/isac/MathEngBasic/rewrite.sml --- a/src/Tools/isac/MathEngBasic/rewrite.sml Wed Nov 16 10:30:59 2022 +0100 +++ b/src/Tools/isac/MathEngBasic/rewrite.sml Wed Nov 16 17:42:41 2022 +0100 @@ -114,7 +114,7 @@ else (trace_in5 ctxt i "asms false" p'; raise NO_REWRITE) (* don't go into subtm.of cond*) end in - if TermC.perm lhs rhs andalso not (tless bdv (t', t)) (*ordered rewriting*) + if TermC.perm lhs rhs andalso not (tless ctxt bdv (t', t)) (*ordered rewriting*) then (trace_eq2 ctxt i "not >" t t'; raise NO_REWRITE) else (t'', p'', [], true) end diff -r 48c31909de24 -r 439f7f3867ec test/Tools/isac/BaseDefinitions/rewrite-order.sml --- a/test/Tools/isac/BaseDefinitions/rewrite-order.sml Wed Nov 16 10:30:59 2022 +0100 +++ b/test/Tools/isac/BaseDefinitions/rewrite-order.sml Wed Nov 16 17:42:41 2022 +0100 @@ -61,9 +61,9 @@ then (trace_in4 ctxt i "asms accepted" p' simpl_p'; (t',simpl_p'))(* uncond.rew.from above*) else (trace_in5 ctxt i "asms false" p'; raise NO_REWRITE) (* don't go into subtm.of cond*) end; - (*if*) TermC.perm lhs rhs andalso not (tless bdv (t', t)); (*ordered rewriting*) - not (tless bdv (t', t)); (*isa = true , isa2 = false*) - (tless bdv (t', t)); (*isa = false, isa2 = true*) + (*if*) TermC.perm lhs rhs andalso not (tless @{context} bdv (t', t)); (*ordered rewriting*) + not (tless @{context} bdv (t', t)); (*isa = true , isa2 = false*) + (tless @{context} bdv (t', t)); (*isa = false, isa2 = true*) (*WHAT IS ..: tless <-- Repeat {rew_ord = ("sqrt_right", rew_ord_), asm_rls, ...} = Test_simplify; ..in Test_Some.thy rew_ord_ <-- sqrt_right false @{theory "Pure"} ..in Test.thy @@ -71,7 +71,7 @@ CHECK THIS ...(same error as with ^^^^^^^^^tless CHECK THIS ...(same error as with code copied into Test_Some.thy *) -if (sqrt_right false @{theory "Pure"} bdv (t', t)) (*isa = false, isa2 = true*) +if (sqrt_right false @{context} bdv (t', t)) (*isa = false, isa2 = true*) (** )then error "sqrt_right: special case NOT ok" else (); ( *isa*) (**)then () else error "sqrt_right: special case OK"; (*isa2*) "~~~~~ fun sqrt_right , args:"; val ((pr:bool), thy, (_: subst), tu) = @@ -112,7 +112,7 @@ "-------- check simple terms -------------------------------------------------------------------"; "-------- check simple terms -------------------------------------------------------------------"; "-------- check simple terms -------------------------------------------------------------------"; -val rew_ord_ = sqrt_right false @{theory "Pure"}; +val rew_ord_ = sqrt_right false @{context} ; if rew_ord_ [] (@{term "1::real"}, @{term "2::real"}) = true then () else error ""; if rew_ord_ [] (@{term "3::real"}, @{term "2::real"}) = false then () else error ""; @@ -136,43 +136,43 @@ (*# rls: Test_simplify on: x + 1 + - 1 * 2 = 0 ..selected "not >:" from trace:*) (*## not >: "x + 1 + - 1 * 2" > "x + 1 + - 1 * 2" *) -if rew_ord_ [] (@{term "x + 1 + - 1 * 2::real"}, @{term "x + 1 + - 1 * 2::real"}) = false +if rew_ord_ @{context} [] (@{term "x + 1 + - 1 * 2::real"}, @{term "x + 1 + - 1 * 2::real"}) = false then () else error "term_ord' 1"; (*## not >: "1 + x + - 1 * 2" > "- 1 * 2 + (1 + x)" *) -if rew_ord_ [] (@{term "1 + x + - 1 * 2::real"}, @{term "- 1 * 2 + (1 + x)::real"}) = true +if rew_ord_ @{context} [] (@{term "1 + x + - 1 * 2::real"}, @{term "- 1 * 2 + (1 + x)::real"}) = true then () else error "term_ord' 2"; (*## not >: "1 + x" > "x + 1" *) -if rew_ord_ [] (@{term "1 + x::real"}, @{term "x + 1::real"}) = true +if rew_ord_ @{context} [] (@{term "1 + x::real"}, @{term "x + 1::real"}) = true then () else error "term_ord' 3"; (*## not >: "- 1 * 2" > "2 * - 1" *) -if rew_ord_ [] (@{term "- 1 * 2::real"}, @{term "2 * - 1::real"}) = true +if rew_ord_ @{context} [] (@{term "- 1 * 2::real"}, @{term "2 * - 1::real"}) = true then () else error "term_ord' 4"; (*## not >: "1 + (x + - 2)" > "x + - 2 + 1" *) -if rew_ord_ [] (@{term "1 + (x + - 2)::real"}, @{term "x + - 2 + 1::real"}) = true +if rew_ord_ @{context} [] (@{term "1 + (x + - 2)::real"}, @{term "x + - 2 + 1::real"}) = true then () else error "term_ord' 5"; (*## not >: "x + - 2" > "- 2 + x"*) -if rew_ord_ [] (@{term "x + - 2::real"}, @{term "- 2 + x ::real"}) = false +if rew_ord_ @{context} [] (@{term "x + - 2::real"}, @{term "- 2 + x ::real"}) = false then () else error "term_ord' 5a"; (*<<<<<<<<<<<<<<----------------- false in trace isa2*) (*--------------------------------- ordered rew. (NOT) inhibited*) (*## not >: "1 + (-2 + x)" > "-2 + x + 1" *) -if rew_ord_ [] (@{term "1 + (-2 + x)::real"}, @{term "-2 + x + 1::real"}) = true +if rew_ord_ @{context} [] (@{term "1 + (-2 + x)::real"}, @{term "-2 + x + 1::real"}) = true then () else error "term_ord' 6"; (*## not >: "- 2 + x" > "x + - 2" *) -if rew_ord_ [] (@{term "- 2 + x::real"}, @{term "x + - 2::real"}) = true +if rew_ord_ @{context} [] (@{term "- 2 + x::real"}, @{term "x + - 2::real"}) = true then () else error "term_ord' 7"; (*## not >: "- 2 + (1 + x)" > "1 + (- 2 + x)" *) -if rew_ord_ [] (@{term "- 2 + (1 + x)::real"}, @{term "1 + (- 2 + x)::real"}) = true +if rew_ord_ @{context} [] (@{term "- 2 + (1 + x)::real"}, @{term "1 + (- 2 + x)::real"}) = true then () else error "term_ord' 8"; (*## not > "- 1 + x" > "x + - 1" *) -if rew_ord_ [] (@{term "- 1 + x::real"}, @{term "x + - 1::real"}) = true +if rew_ord_ @{context} [] (@{term "- 1 + x::real"}, @{term "x + - 1::real"}) = true then () else error "term_ord' 9"; diff -r 48c31909de24 -r 439f7f3867ec test/Tools/isac/Interpret/error-pattern.sml --- a/test/Tools/isac/Interpret/error-pattern.sml Wed Nov 16 10:30:59 2022 +0100 +++ b/test/Tools/isac/Interpret/error-pattern.sml Wed Nov 16 17:42:41 2022 +0100 @@ -118,13 +118,13 @@ val fod = Derive.do_one (Proof_Context.init_global @{theory "Isac_Knowledge"}) Atools_erls ((#rules o Rule_Set.rep) Test_simplify) - (sqrt_right false (@{theory "Pure"})) NONE + (sqrt_right false) NONE (TermC.parse_test @{context} "x + 1 + - 1 * 2 = 0"); (writeln o Derive.trtas2str) fod; val ifod = Derive.do_one (Proof_Context.init_global @{theory "Isac_Knowledge"}) Atools_erls ((#rules o Rule_Set.rep) Test_simplify) - (sqrt_right false (@{theory "Pure"})) NONE + (sqrt_right false) NONE (TermC.parse_test @{context} "- 2 * 1 + (1 + x) = 0"); (writeln o Derive.trtas2str) ifod; fun equal (_,_,(t1, _)) (_,_,(t2, _)) = t1 = t2; diff -r 48c31909de24 -r 439f7f3867ec test/Tools/isac/Knowledge/eqsystem-1.sml --- a/test/Tools/isac/Knowledge/eqsystem-1.sml Wed Nov 16 10:30:59 2022 +0100 +++ b/test/Tools/isac/Knowledge/eqsystem-1.sml Wed Nov 16 17:42:41 2022 +0100 @@ -124,28 +124,28 @@ "----------- rewrite-order ord_simplify_System -------------------"; "M_b x = c * x + - 1 * q_0 * (x \ 2 / 2) + c_2"; "--- add.commute ---"; (* ... add.commute cf. b42e334c97ee *) -if ord_simplify_System false thy [] (TermC.parse_test @{context}"- 1 * q_0 * (x \ 2 / 2)", +if ord_simplify_System false ctxt [] (TermC.parse_test @{context}"- 1 * q_0 * (x \ 2 / 2)", TermC.parse_test @{context}"c * x") then () else error "integrate.sml, (- 1 * q_0 * (x \ 2 / 2)) < (c * x) not#1"; -if ord_simplify_System false thy [] (TermC.parse_test @{context}"- 1 * q_0 * (x \ 2 / 2)", +if ord_simplify_System false ctxt [] (TermC.parse_test @{context}"- 1 * q_0 * (x \ 2 / 2)", TermC.parse_test @{context}"c_2") then () else error "integrate.sml, (- 1 * q_0 * (x \ 2 / 2)) < (c_2) not#2"; -if ord_simplify_System false thy [] (TermC.parse_test @{context}"c * x", +if ord_simplify_System false ctxt [] (TermC.parse_test @{context}"c * x", TermC.parse_test @{context}"c_2") then () else error "integrate.sml, (c * x) < (c_2) not#3"; "--- mult.commute ---"; -if ord_simplify_System false thy [] (TermC.parse_test @{context}"x * c", +if ord_simplify_System false ctxt [] (TermC.parse_test @{context}"x * c", TermC.parse_test @{context}"c * x") then () else error "integrate.sml, (x * c) < (c * x) not#4"; -if ord_simplify_System false thy [] (TermC.parse_test @{context}"- 1 * q_0 * (x \ 2 / 2) * c", +if ord_simplify_System false ctxt [] (TermC.parse_test @{context}"- 1 * q_0 * (x \ 2 / 2) * c", TermC.parse_test @{context}"- 1 * q_0 * c * (x \ 2 / 2)") then () else error "integrate.sml, (. * .) < (. * .) not#5"; -if ord_simplify_System false thy [] (TermC.parse_test @{context}"- 1 * q_0 * (x \ 2 / 2) * c", +if ord_simplify_System false ctxt [] (TermC.parse_test @{context}"- 1 * q_0 * (x \ 2 / 2) * c", TermC.parse_test @{context}"c * - 1 * q_0 * (x \ 2 / 2)") then () else error "integrate.sml, (. * .) < (. * .) not#6"; @@ -240,7 +240,7 @@ else error "eqsystem.sml top_down_substitution,2x2] order_system"; if not (ord_simplify_System - false thy [] + false ctxt [] (TermC.parse_test @{context}"[c_2 = 77, c = (q_0 * L \ 2 / 2 + - 1 * 77) / L]", TermC.parse_test @{context}"[c = (q_0 * L \ 2 / 2 + - 1 * 77) / L, c_2 = 77]")) then () else error "eqsystem.sml, order_result rew_ord"; diff -r 48c31909de24 -r 439f7f3867ec test/Tools/isac/Knowledge/poly-2.sml --- a/test/Tools/isac/Knowledge/poly-2.sml Wed Nov 16 10:30:59 2022 +0100 +++ b/test/Tools/isac/Knowledge/poly-2.sml Wed Nov 16 17:42:41 2022 +0100 @@ -693,7 +693,7 @@ val t1 = TermC.parse_test @{context} "2 * b + (3 * a + 3 * b)"; val t2 = TermC.parse_test @{context} "(3 * a + 3 * b) + 2 * b"; -if ord_make_polynomial true @{theory} [] (t1, t2) then () +if ord_make_polynomial true @{context} [] (t1, t2) then () else error "poly.sml: diff.behav. in ord_make_polynomial"; (*SO: WHY IS THERE NO REWRITING ...*) diff -r 48c31909de24 -r 439f7f3867ec test/Tools/isac/Knowledge/polyminus.sml --- a/test/Tools/isac/Knowledge/polyminus.sml Wed Nov 16 10:30:59 2022 +0100 +++ b/test/Tools/isac/Knowledge/polyminus.sml Wed Nov 16 17:42:41 2022 +0100 @@ -170,13 +170,13 @@ "----------- watch order_add_mult -------------------------------"; "----- with these simple variables it works..."; val ctxt = @{context}; -val t = TermC.parse_test @{context} "((a + d) + c) + b"; +val t = TermC.parse_test ctxt "((a + d) + c) + b"; val SOME (t,_) = rewrite_set_ ctxt false order_add_mult t; UnparseC.term t; if UnparseC.term t = "a + (b + (c + d))" then () else error "polyminus.sml 1 watch order_add_mult"; "----- the same stepwise..."; -val od = ord_make_polynomial true (@{theory "Poly"}); +val od = ord_make_polynomial true val t = TermC.parse_test @{context} "((a + d) + c) + b"; "((a + d) + c) + b"; val SOME (t,_) = rewrite_ ctxt od Rule_Set.empty true @{thm add.commute} t; UnparseC.term t; @@ -208,7 +208,7 @@ else error "polyminus.sml: order_add_mult changed"; "----- here we see rew_sub going into subterm with ord.rew...."; -val od = ord_make_polynomial false (@{theory "Poly"}); +val od = ord_make_polynomial false; val t = TermC.parse_test @{context} "b + a + c + d"; val SOME (t,_) = rewrite_ ctxt od Rule_Set.empty false @{thm add.commute} t; UnparseC.term t; val SOME (t,_) = rewrite_ ctxt od Rule_Set.empty false @{thm add.commute} t; UnparseC.term t; diff -r 48c31909de24 -r 439f7f3867ec test/Tools/isac/MathEngBasic/rewrite.sml --- a/test/Tools/isac/MathEngBasic/rewrite.sml Wed Nov 16 10:30:59 2022 +0100 +++ b/test/Tools/isac/MathEngBasic/rewrite.sml Wed Nov 16 17:42:41 2022 +0100 @@ -100,8 +100,8 @@ val SOME (r, _) = (rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.empty false thm tm); "----- ordered rewriting"; -fun tord (_:subst) pp = LibraryC.termless pp; -if tord [] (@{term "x + y*z::real"}, @{term "y*z + x::real"}) then () +fun tord (_:Proof.context) (_:subst) pp = LibraryC.termless pp; +if tord @{context} [] (@{term "x + y*z::real"}, @{term "y*z + x::real"}) then () else error "rewrite.sml diff.behav. in ord.rewr."; val NONE = (rewrite_ ctxt tord Rule_Set.empty false thm tm); diff -r 48c31909de24 -r 439f7f3867ec test/Tools/isac/Test_Isac.thy --- a/test/Tools/isac/Test_Isac.thy Wed Nov 16 10:30:59 2022 +0100 +++ b/test/Tools/isac/Test_Isac.thy Wed Nov 16 17:42:41 2022 +0100 @@ -306,7 +306,7 @@ ML_file "Knowledge/descript.sml" ML_file "Knowledge/simplify.sml" ML_file "Knowledge/poly-1.sml" - ML_file "Knowledge/poly-2.sml" (*Test_Isac_Short*) + ML_file "Knowledge/poly-2.sml" (*Test_Isac_Short*) ML_file "Knowledge/gcd_poly_ml.sml" ML_file "Knowledge/rational-1.sml" ML_file "Knowledge/rational-2.sml" (*Test_Isac_Short*)