135 (if pr then |
135 (if pr then |
136 let |
136 let |
137 val (f, ts) = strip_comb t and (g, us) = strip_comb u; |
137 val (f, ts) = strip_comb t and (g, us) = strip_comb u; |
138 val _=writeln("t= f@ts= \""^ |
138 val _=writeln("t= f@ts= \""^ |
139 ((Syntax.string_of_term (thy2ctxt thy)) f)^"\" @ \"["^ |
139 ((Syntax.string_of_term (thy2ctxt thy)) f)^"\" @ \"["^ |
140 (commas(map(string_of_cterm o cterm_of(sign_of thy)) ts))^"]\""); |
140 (commas(map(Syntax.string_of_term (thy2ctxt thy)) ts))^"]\""); |
141 val _=writeln("u= g@us= \""^ |
141 val _=writeln("u= g@us= \""^ |
142 ((Syntax.string_of_term (thy2ctxt thy)) g)^"\" @ \"["^ |
142 ((Syntax.string_of_term (thy2ctxt thy)) g)^"\" @ \"["^ |
143 (commas(map(string_of_cterm o cterm_of(sign_of thy)) us))^"]\""); |
143 (commas(map(Syntax.string_of_term (thy2ctxt thy)) us))^"]\""); |
144 val _=writeln("size_of_term(t,u)= ("^ |
144 val _=writeln("size_of_term(t,u)= ("^ |
145 (string_of_int(size_of_term' t))^", "^ |
145 (string_of_int(size_of_term' t))^", "^ |
146 (string_of_int(size_of_term' u))^")"); |
146 (string_of_int(size_of_term' u))^")"); |
147 val _=writeln("hd_ord(f,g) = "^((pr_ord o hd_ord)(f,g))); |
147 val _=writeln("hd_ord(f,g) = "^((pr_ord o hd_ord)(f,g))); |
148 val _=writeln("terms_ord(ts,us) = "^ |
148 val _=writeln("terms_ord(ts,us) = "^ |
156 (case hd_ord (f, g) of EQUAL => (terms_ord str pr) (ts, us) |
156 (case hd_ord (f, g) of EQUAL => (terms_ord str pr) (ts, us) |
157 | ord => ord) |
157 | ord => ord) |
158 end |
158 end |
159 | ord => ord) |
159 | ord => ord) |
160 and hd_ord (f, g) = (* ~ term.ML *) |
160 and hd_ord (f, g) = (* ~ term.ML *) |
161 prod_ord (prod_ord indexname_ord Term_Ord.typ_ord) int_ord (dest_hd' f, |
161 prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord (dest_hd' f, |
162 dest_hd' g) |
162 dest_hd' g) |
163 and terms_ord str pr (ts, us) = |
163 and terms_ord str pr (ts, us) = |
164 list_ord (term_ord' pr (assoc_thy "Isac.thy"))(ts, us); |
164 list_ord (term_ord' pr (assoc_thy "Isac"))(ts, us); |
165 (**) |
165 (**) |
166 in |
166 in |
167 (**) |
167 (**) |
168 (*WN0510 for preliminary use in eval_order_system, see case-study mat-eng.tex |
168 (*WN0510 for preliminary use in eval_order_system, see case-study mat-eng.tex |
169 fun ord_simplify_System_rev (pr:bool) thy subst tu = |
169 fun ord_simplify_System_rev (pr:bool) thy subst tu = |
258 Seq {id = "simplify_System_parenthesized", preconds = []:term list, |
258 Seq {id = "simplify_System_parenthesized", preconds = []:term list, |
259 rew_ord = ("dummy_ord", dummy_ord), |
259 rew_ord = ("dummy_ord", dummy_ord), |
260 erls = Atools_erls, srls = Erls, calc = [], |
260 erls = Atools_erls, srls = Erls, calc = [], |
261 rules = [Thm ("left_distrib",num_str @{thm left_distrib}), |
261 rules = [Thm ("left_distrib",num_str @{thm left_distrib}), |
262 (*"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"*) |
262 (*"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"*) |
263 Thm ("nadd_divide_distrib",num_str @{thm nadd_divide_distrib}), |
263 Thm ("add_divide_distrib",num_str @{thm add_divide_distrib}), |
264 (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*) |
264 (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*) |
265 (*^^^^^ *0* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*) |
265 (*^^^^^ *0* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*) |
266 Rls_ norm_Rational_noadd_fractions(**2**), |
266 Rls_ norm_Rational_noadd_fractions(**2**), |
267 Rls_ (*order_add_mult_in*) norm_System_noadd_fractions (**1**), |
267 Rls_ (*order_add_mult_in*) norm_System_noadd_fractions (**1**), |
268 Thm ("sym_real_mult_assoc", |
268 Thm ("sym_real_mult_assoc", |