1.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml Tue Jul 27 12:32:43 2021 +0200
1.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml Sun Aug 01 14:39:03 2021 +0200
1.3 @@ -13,6 +13,7 @@
1.4 "----------- tests on predicates in problems ---------------------";
1.5 "----------- test matching problems ------------------------------";
1.6 "----------- prep. for introduction of Matthias Goldgruber 2003 trials on rewrite orders -----";
1.7 +"----------- open local of fun ord_make_polynomial_in ------------------------------------------";
1.8 "----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
1.9 "----------- lin.eq degree_0 -------------------------------------";
1.10 "----------- test thm's d2_pq_formulsxx[_neg]---------------------";
1.11 @@ -49,11 +50,11 @@
1.12 "----------- tests on predicates in problems ---------------------";
1.13 "----------- tests on predicates in problems ---------------------";
1.14 "----------- tests on predicates in problems ---------------------";
1.15 -Rewrite.trace_on:=true; (*true false*)
1.16 +Rewrite.trace_on:=false; (*true false*)
1.17
1.18 val t1 = (Thm.term_of o the o (TermC.parse thy)) "lhs (-8 - 2*x + x \<up> 2 = 0)";
1.19 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t1;
1.20 - if ((UnparseC.term t) = "-8 - 2 * x + x \<up> 2") then ()
1.21 + if ((UnparseC.term t) = "- 8 - 2 * x + x \<up> 2") then ()
1.22 else error "polyeq.sml: diff.behav. in lhs";
1.23
1.24 val t2 = (Thm.term_of o the o (TermC.parse thy)) "(-8 - 2*x + x \<up> 2) is_expanded_in x";
1.25 @@ -98,7 +99,7 @@
1.26 if (UnparseC.term t) = "False" then ()
1.27 else error "polyeq.sml: diff.behav. 7 in has_degree_in_in";
1.28
1.29 - val t5 = (Thm.term_of o the o (TermC.parse thy))
1.30 +val t5 = (Thm.term_of o the o (TermC.parse thy))
1.31 "((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";
1.32 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t5;
1.33 if (UnparseC.term t) = "True" then ()
1.34 @@ -221,6 +222,122 @@
1.35 ##################################################################################*)
1.36
1.37
1.38 +"----------- open local of fun ord_make_polynomial_in ------------------------------------------";
1.39 +"----------- open local of fun ord_make_polynomial_in ------------------------------------------";
1.40 +"----------- open local of fun ord_make_polynomial_in ------------------------------------------";
1.41 +(* termorder hacked by MG, adapted later by WN *)
1.42 +(** )local ( *. for make_polynomial_in .*)
1.43 +
1.44 +open Term; (* for type order = EQUAL | LESS | GREATER *)
1.45 +
1.46 +fun pr_ord EQUAL = "EQUAL"
1.47 + | pr_ord LESS = "LESS"
1.48 + | pr_ord GREATER = "GREATER";
1.49 +
1.50 +fun dest_hd' _ (Const (a, T)) = (((a, 0), T), 0)
1.51 + | dest_hd' x (t as Free (a, T)) =
1.52 + if x = t then ((("|||||||||||||", 0), T), 0) (*WN*)
1.53 + else (((a, 0), T), 1)
1.54 + | dest_hd' _ (Var v) = (v, 2)
1.55 + | dest_hd' _ (Bound i) = ((("", i), dummyT), 3)
1.56 + | dest_hd' _ (Abs (_, T, _)) = ((("", 0), T), 4)
1.57 + | dest_hd' _ _ = raise ERROR "dest_hd': uncovered case in fun.def.";
1.58 +
1.59 +fun size_of_term' i pr x (t as Const (\<^const_name>\<open>powr\<close>, _) $
1.60 + Free (var, _) $ Free (pot, _)) =
1.61 + (if pr then tracing (idt "#" i ^ "size_of_term' powr: " ^ UnparseC.term t) else ();
1.62 + case x of (*WN*)
1.63 + (Free (xstr, _)) =>
1.64 + if xstr = var
1.65 + then (if pr then tracing (idt "#" i ^ "xstr = var --> " ^ string_of_int (1000 * (the (TermC.int_opt_of_string pot)))) else ();
1.66 + 1000 * (the (TermC.int_opt_of_string pot)))
1.67 + else (if pr then tracing (idt "#" i ^ "x <> Free --> " ^ "3") else (); 3)
1.68 + | _ => raise ERROR ("size_of_term' called with subst = " ^ UnparseC.term x))
1.69 + | size_of_term' i pr x (t as Abs (_, _, body)) =
1.70 + (if pr then tracing (idt "#" i ^ "size_of_term' Abs: " ^ UnparseC.term t) else ();
1.71 + 1 + size_of_term' (i + 1) pr x body)
1.72 + | size_of_term' i pr x (f $ t) =
1.73 + let
1.74 + val _ = if pr then tracing (idt "#" i ^ "size_of_term' $$$: " ^ UnparseC.term f ^ " $$$ " ^ UnparseC.term t) else ();
1.75 + val s1 = size_of_term' (i + 1) pr x f
1.76 + val s2 = size_of_term' (i + 1) pr x t
1.77 + val _ = if pr then tracing (idt "#" i ^ "size_of_term' $$$-->: " ^ string_of_int s1 ^ " + " ^ string_of_int s2 ^ " = " ^ string_of_int(s1 + s2)) else ();
1.78 + in (s1 + s2) end
1.79 + | size_of_term' i pr x t =
1.80 + (if pr then tracing (idt "#" i ^ "size_of_term' bot: " ^ UnparseC.term t) else ();
1.81 + case t of
1.82 + Free (subst, _) =>
1.83 + (case x of
1.84 + Free (xstr, _) =>
1.85 + if xstr = subst
1.86 + then (if pr then tracing (idt "#" i ^ "xstr = var --> " ^ "1000") else (); 1000)
1.87 + else (if pr then tracing (idt "#" i ^ "x <> Free --> " ^ "1") else (); 1)
1.88 + | _ => raise ERROR ("size_of_term' called with subst = " ^ UnparseC.term x))
1.89 + | _ => (if pr then tracing (idt "#" i ^ "bot --> " ^ "1") else (); 1));
1.90 +
1.91 +fun term_ord' i pr x thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
1.92 + let
1.93 + val _ = if pr then tracing (idt "#" i ^ "term_ord' Abs") else ();
1.94 + val ord =
1.95 + case term_ord' (i + 1) pr x thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord
1.96 + val _ = if pr then tracing (idt "#" i ^ "term_ord' Abs --> " ^ pr_ord ord) else ()
1.97 + in ord end
1.98 + | term_ord' i pr x _ (t, u) =
1.99 + let
1.100 + val _ = if pr then tracing (idt "#" i ^ "term_ord' bot (" ^ UnparseC.term t ^ ", " ^ UnparseC.term u ^ ")") else ();
1.101 + val ord =
1.102 + case int_ord (size_of_term' (i + 1) pr x t, size_of_term' (i + 1) pr x u) of
1.103 + EQUAL =>
1.104 + let val (f, ts) = strip_comb t and (g, us) = strip_comb u
1.105 + in
1.106 + (case hd_ord (i + 1) pr x (f, g) of
1.107 + EQUAL => (terms_ord x (i + 1) pr) (ts, us)
1.108 + | ord => ord)
1.109 + end
1.110 + | ord => ord
1.111 + val _ = if pr then tracing (idt "#" i ^ "term_ord' bot --> " ^ pr_ord ord) else ()
1.112 + in ord end
1.113 +and hd_ord i pr x (f, g) = (* ~ term.ML *)
1.114 + let
1.115 + val _ = if pr then tracing (idt "#" i ^ "hd_ord (" ^ UnparseC.term f ^ ", " ^ UnparseC.term g ^ ")") else ();
1.116 + val ord = prod_ord
1.117 + (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord
1.118 + (dest_hd' x f, dest_hd' x g)
1.119 + val _ = if pr then tracing (idt "#" i ^ "hd_ord --> " ^ pr_ord ord) else ();
1.120 + in ord end
1.121 +and terms_ord x i pr (ts, us) =
1.122 + let
1.123 + val _ = if pr then tracing (idt "#" i ^ "terms_ord (" ^ UnparseC.terms ts ^ ", " ^ UnparseC.terms us ^ ")") else ();
1.124 + val ord = list_ord (term_ord' (i + 1) pr x (ThyC.get_theory "Isac_Knowledge"))(ts, us);
1.125 + val _ = if pr then tracing (idt "#" i ^ "terms_ord --> " ^ pr_ord ord) else ();
1.126 + in ord end
1.127 +
1.128 +(** )in( *local*)
1.129 +
1.130 +fun ord_make_polynomial_in (pr:bool) thy subst (ts, us) =
1.131 + ((** )tracing ("*** subs variable is: " ^ Env.subst2str subst); ( **)
1.132 + case subst of
1.133 + (_, x) :: _ =>
1.134 + term_ord' 1 pr x thy (TermC.numerals_to_Free ts, TermC.numerals_to_Free us) = LESS
1.135 + | _ => raise ERROR ("ord_make_polynomial_in called with subst = " ^ Env.subst2str subst))
1.136 +
1.137 +(** )end;( *local*)
1.138 +
1.139 +\<close> ML \<open>
1.140 +val subs = [(TermC.str2term "bdv::real", TermC.str2term "x::real")];
1.141 +if ord_make_polynomial_in true @{theory} subs (t1, t2) then () else error "still GREATER?";
1.142 +
1.143 +val x = TermC.str2term "x ::real";
1.144 +
1.145 +val t1 = TermC.numerals_to_Free (TermC.str2term "L * q_0 * x \<up> 2 / 4 ::real");
1.146 +if 2006 = size_of_term' 1 true x t1
1.147 +then () else error "size_of_term' (L * q_0 * x \<up> 2) CHANGED)";
1.148 +
1.149 +val t2 = TermC.numerals_to_Free (TermC.str2term "- 1 * (q_0 * x \<up> 3) :: real");
1.150 +if 3004 = size_of_term' 1 true x t2
1.151 +then () else error "size_of_term' (- 1 * (q_0 * x \<up> 3)) CHANGED";
1.152 +
1.153 +
1.154 "----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
1.155 "----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
1.156 "----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
1.157 @@ -271,14 +388,14 @@
1.158 val ppp' = "-6 + -5*x + x \<up> 3 + - 1*x \<up> 2 + - 1*x \<up> 3 + - 14*x \<up> 2";
1.159 val ppp = (Thm.term_of o the o (TermC.parse thy)) ppp';
1.160 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ppp;
1.161 -if UnparseC.term t' = "-6 + -5 * x + - 15 * x \<up> 2 + 0" then ()
1.162 +if UnparseC.term t' = "- 6 + -5 * x + - 15 * x \<up> 2 + 0" then ()
1.163 else error "termorder.sml diff.behav ord_make_polynomial_in #14";
1.164
1.165 val SOME (t', _) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ppp;
1.166 -if UnparseC.term t' = "-6 + -5 * x + - 15 * x \<up> 2 + 0" then ()
1.167 +if UnparseC.term t' = "- 6 + - 5 * x + - 15 * x \<up> 2 + 0" then ()
1.168 else error "termorder.sml diff.behav ord_make_polynomial_in #15";
1.169
1.170 - val ttt' = "(3*x + 5)/18";
1.171 + val ttt' = "(3*x + 5)/18 ::real";
1.172 val ttt = (Thm.term_of o the o (TermC.parse thy)) ttt';
1.173 val SOME (uuu,_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ttt;
1.174 if UnparseC.term uuu = "(5 + 3 * x) / 18" then ()
1.175 @@ -288,7 +405,6 @@
1.176 val SOME (uuu,_) = rewrite_set_ thy false make_polynomial ttt;
1.177 if UnparseC.term uuu = "(5 + 3 * x) / 18" then ()
1.178 else error "termorder.sml diff.behav ord_make_polynomial_in #16b";
1.179 -============ inhibit exn WN120316 ==============================================*)
1.180
1.181
1.182 "----------- lin.eq degree_0 -------------------------------------";