1.1 --- a/src/Tools/isac/Knowledge/Test.thy Wed Nov 16 10:30:59 2022 +0100
1.2 +++ b/src/Tools/isac/Knowledge/Test.thy Wed Nov 16 17:42:41 2022 +0100
1.3 @@ -313,36 +313,35 @@
1.4 | size_of_term' (Abs (_,_,body)) = 1 + size_of_term' body
1.5 | size_of_term' (f$t) = size_of_term' f + size_of_term' t
1.6 | size_of_term' _ = 1;
1.7 -fun term_ord' pr thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
1.8 - (case term_ord' pr thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U)
1.9 +fun term_ord' pr ctxt (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
1.10 + (case term_ord' pr ctxt (t, u) of EQUAL => Term_Ord.typ_ord (T, U)
1.11 | ord => ord)
1.12 - | term_ord' pr _ (t, u) =
1.13 + | term_ord' pr ctxt (t, u) =
1.14 (if pr then
1.15 let val (f, ts) = strip_comb t and (g, us) = strip_comb u;
1.16 - val _ = tracing ("t= f@ts= \"" ^ UnparseC.term f ^ "\" @ \"[" ^
1.17 - commas(map UnparseC.term ts) ^ "]\"")
1.18 - val _ = tracing ("u= g@us= \"" ^ UnparseC.term g ^"\" @ \"[" ^
1.19 - commas(map UnparseC.term us) ^"]\"")
1.20 + val _ = tracing ("t= f@ts= \"" ^ UnparseC.term_in_ctxt ctxt f ^ "\" @ \"[" ^
1.21 + commas (map (UnparseC.term_in_ctxt ctxt) ts) ^ "]\"")
1.22 + val _ = tracing ("u= g@us= \"" ^ UnparseC.term_in_ctxt ctxt g ^"\" @ \"[" ^
1.23 + commas (map (UnparseC.term_in_ctxt ctxt) us) ^"]\"")
1.24 val _ = tracing ("size_of_term(t,u)= (" ^
1.25 string_of_int (size_of_term' t) ^ ", " ^
1.26 string_of_int (size_of_term' u) ^ ")")
1.27 val _ = tracing ("hd_ord(f,g) = " ^ (pr_ord o hd_ord) (f,g))
1.28 val _ = tracing ("terms_ord(ts,us) = " ^
1.29 - (pr_ord o terms_ord str false) (ts,us));
1.30 + (pr_ord o terms_ord str false ctxt) (ts,us));
1.31 val _ = tracing "-------"
1.32 in () end
1.33 else ();
1.34 case int_ord (size_of_term' t, size_of_term' u) of
1.35 EQUAL =>
1.36 let val (f, ts) = strip_comb t and (g, us) = strip_comb u in
1.37 - (case hd_ord (f, g) of EQUAL => (terms_ord str pr) (ts, us)
1.38 + (case hd_ord (f, g) of EQUAL => (terms_ord str pr ctxt) (ts, us)
1.39 | ord => ord)
1.40 end
1.41 | ord => ord)
1.42 and hd_ord (f, g) = (* ~ term.ML *)
1.43 prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord (dest_hd' f, dest_hd' g)
1.44 -and terms_ord _ pr (ts, us) =
1.45 - list_ord (term_ord' pr (ThyC.get_theory "Isac_Knowledge"))(ts, us);
1.46 +and terms_ord _ pr ctxt (ts, us) = list_ord (term_ord' pr ctxt) (ts, us);
1.47 in
1.48
1.49 fun ord_make_polytest (pr:bool) thy (_: subst) (ts, us) =
1.50 @@ -353,7 +352,7 @@
1.51
1.52 section \<open>term order\<close>
1.53 ML \<open>
1.54 -fun term_order (_: subst) tu = (term_ordI [] tu = LESS);
1.55 +val term_order = Rewrite_Ord.function_empty;
1.56 \<close>
1.57
1.58 section \<open>rulesets\<close>
1.59 @@ -393,7 +392,7 @@
1.60 (*FIXXXXXXME 10.8.02: handle like _simplify*)
1.61 val tval_rls =
1.62 Rule_Def.Repeat{id = "tval_rls", preconds = [],
1.63 - rew_ord = ("sqrt_right",sqrt_right false @{theory "Pure"}),
1.64 + rew_ord = ("sqrt_right",sqrt_right false),
1.65 asm_rls=testerls,prog_rls = Rule_Set.empty,
1.66 calc=[], errpatts = [],
1.67 rules = [
1.68 @@ -439,16 +438,17 @@
1.69 val rearrange_assoc =
1.70 Rule_Def.Repeat{
1.71 id = "rearrange_assoc", preconds = [],
1.72 - rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty),
1.73 + rew_ord = ("Rewrite_Ord.id_empty", Rewrite_Ord.function_empty),
1.74 asm_rls = Rule_Set.empty, prog_rls = Rule_Set.empty, calc = [], errpatts = [],
1.75 rules = [
1.76 \<^rule_thm_sym>\<open>add.assoc\<close>,
1.77 \<^rule_thm_sym>\<open>rmult_assoc\<close>],
1.78 program = Rule.Empty_Prog};
1.79
1.80 +\<close> ML \<open>
1.81 val ac_plus_times =
1.82 Rule_Def.Repeat{
1.83 - id = "ac_plus_times", preconds = [], rew_ord = ("term_order",term_order),
1.84 + id = "ac_plus_times", preconds = [], rew_ord = ("term_order", term_order),
1.85 asm_rls = Rule_Set.empty, prog_rls = Rule_Set.empty, calc = [], errpatts = [],
1.86 rules = [
1.87 \<^rule_thm>\<open>radd_commute\<close>,
1.88 @@ -458,6 +458,7 @@
1.89 \<^rule_thm>\<open>rmult_left_commute\<close>,
1.90 \<^rule_thm>\<open>rmult_assoc\<close>],
1.91 program = Rule.Empty_Prog};
1.92 +\<close> ML \<open>
1.93
1.94 (*todo: replace by Rewrite("rnorm_equation_add", @{thm rnorm_equation_add)*)
1.95 val norm_equation =
1.96 @@ -466,13 +467,12 @@
1.97 rules = [
1.98 \<^rule_thm>\<open>rnorm_equation_add\<close>],
1.99 program = Rule.Empty_Prog};
1.100 -\<close>
1.101 -ML \<open>
1.102 +\<close> ML \<open>
1.103 (* expects * distributed over + *)
1.104 val Test_simplify =
1.105 Rule_Def.Repeat{
1.106 id = "Test_simplify", preconds = [],
1.107 - rew_ord = ("sqrt_right", sqrt_right false @{theory "Pure"}),
1.108 + rew_ord = ("sqrt_right", sqrt_right false),
1.109 asm_rls = tval_rls, prog_rls = Rule_Set.empty,
1.110 calc=[(*since 040209 filled by prep_rls'*)], errpatts = [],
1.111 rules = [
1.112 @@ -591,12 +591,12 @@
1.113
1.114 setup \<open>Know_Store.add_rew_ords [
1.115 ("termlessI", termlessI),
1.116 - ("ord_make_polytest", ord_make_polytest false \<^theory>)]\<close>
1.117 + ("ord_make_polytest", ord_make_polytest false)]\<close>
1.118
1.119 ML \<open>
1.120 val make_polytest =
1.121 Rule_Def.Repeat{id = "make_polytest", preconds = []:term list,
1.122 - rew_ord = ("ord_make_polytest", ord_make_polytest false @{theory "Poly"}),
1.123 + rew_ord = ("ord_make_polytest", ord_make_polytest false),
1.124 asm_rls = testerls, prog_rls = Rule_Set.Empty,
1.125 calc = [
1.126 ("PLUS" , (\<^const_name>\<open>plus\<close>, (**)Calc_Binop.numeric "#add_")),