1signature EXP_LOG_EXPRESSION = sig 2 3exception DUP 4 5datatype expr = 6 ConstExpr of term 7 | X 8 | Uminus of expr 9 | Add of expr * expr 10 | Minus of expr * expr 11 | Inverse of expr 12 | Mult of expr * expr 13 | Div of expr * expr 14 | Ln of expr 15 | Exp of expr 16 | Power of expr * term 17 | LnPowr of expr * expr 18 | ExpLn of expr 19 | Powr of expr * expr 20 | Powr_Nat of expr * expr 21 | Powr' of expr * term 22 | Root of expr * term 23 | Absolute of expr 24 | Sgn of expr 25 | Min of expr * expr 26 | Max of expr * expr 27 | Floor of expr 28 | Ceiling of expr 29 | Frac of expr 30 | NatMod of expr * expr 31 | Sin of expr 32 | Cos of expr 33 | ArcTan of expr 34 | Custom of string * term * expr list 35 36val preproc_term_conv : Proof.context -> conv 37val expr_to_term : expr -> term 38val reify : Proof.context -> term -> expr * thm 39val reify_simple : Proof.context -> term -> expr * thm 40 41type custom_handler = 42 Lazy_Eval.eval_ctxt -> term -> thm list * Asymptotic_Basis.basis -> thm * Asymptotic_Basis.basis 43 44val register_custom : 45 binding -> term -> custom_handler -> local_theory -> local_theory 46val register_custom_from_thm : 47 binding -> thm -> custom_handler -> local_theory -> local_theory 48val expand_custom : Proof.context -> string -> custom_handler option 49 50val to_mathematica : expr -> string 51val to_maple : expr -> string 52val to_maxima : expr -> string 53val to_sympy : expr -> string 54val to_sage : expr -> string 55 56val reify_mathematica : Proof.context -> term -> string 57val reify_maple : Proof.context -> term -> string 58val reify_maxima : Proof.context -> term -> string 59val reify_sympy : Proof.context -> term -> string 60val reify_sage : Proof.context -> term -> string 61 62val limit_mathematica : string -> string 63val limit_maple : string -> string 64val limit_maxima : string -> string 65val limit_sympy : string -> string 66val limit_sage : string -> string 67 68end 69 70structure Exp_Log_Expression : EXP_LOG_EXPRESSION = struct 71 72 73datatype expr = 74 ConstExpr of term 75 | X 76 | Uminus of expr 77 | Add of expr * expr 78 | Minus of expr * expr 79 | Inverse of expr 80 | Mult of expr * expr 81 | Div of expr * expr 82 | Ln of expr 83 | Exp of expr 84 | Power of expr * term 85 | LnPowr of expr * expr 86 | ExpLn of expr 87 | Powr of expr * expr 88 | Powr_Nat of expr * expr 89 | Powr' of expr * term 90 | Root of expr * term 91 | Absolute of expr 92 | Sgn of expr 93 | Min of expr * expr 94 | Max of expr * expr 95 | Floor of expr 96 | Ceiling of expr 97 | Frac of expr 98 | NatMod of expr * expr 99 | Sin of expr 100 | Cos of expr 101 | ArcTan of expr 102 | Custom of string * term * expr list 103 104type custom_handler = 105 Lazy_Eval.eval_ctxt -> term -> thm list * Asymptotic_Basis.basis -> thm * Asymptotic_Basis.basis 106 107type entry = { 108 name : string, 109 pat : term, 110 net_pat : term, 111 expand : custom_handler 112} 113 114type entry' = { 115 pat : term, 116 net_pat : term, 117 expand : custom_handler 118} 119 120exception DUP 121 122structure Custom_Funs = Generic_Data 123( 124 type T = { 125 name_table : entry' Name_Space.table, 126 net : entry Item_Net.T 127 } 128 fun eq_entry ({name = name1, ...}, {name = name2, ...}) = (name1 = name2) 129 val empty = 130 { 131 name_table = Name_Space.empty_table "Exp-Log Custom Function", 132 net = Item_Net.init eq_entry (fn {net_pat, ...} => [net_pat]) 133 } 134 135 fun merge ({name_table = tbl1, net = net1}, {name_table = tbl2, net = net2}) = 136 {name_table = Name_Space.join_tables (fn _ => raise DUP) (tbl1, tbl2), 137 net = Item_Net.merge (net1, net2)} 138 val extend = I 139) 140 141fun rewrite' ctxt old_prems bounds thms ct = 142 let 143 val thy = Proof_Context.theory_of ctxt 144 fun apply_rule t thm = 145 let 146 val lhs = thm |> Thm.concl_of |> Logic.dest_equals |> fst 147 val _ = Pattern.first_order_match thy (lhs, t) (Vartab.empty, Vartab.empty) 148 val insts = (lhs, t) |> apply2 (Thm.cterm_of ctxt) |> Thm.first_order_match 149 val thm = Thm.instantiate insts thm 150 val prems = Thm.prems_of thm 151 val frees = fold Term.add_frees prems [] 152 in 153 if exists (member op = bounds o fst) frees then 154 NONE 155 else 156 let 157 val thm' = thm OF (map (Thm.assume o Thm.cterm_of ctxt) prems) 158 val prems' = fold (insert op aconv) prems old_prems 159 val crhs = thm |> Thm.concl_of |> Logic.dest_equals |> snd |> Thm.cterm_of ctxt 160 in 161 SOME (thm', crhs, prems') 162 end 163 end 164 handle Pattern.MATCH => NONE 165 fun rewrite_subterm prems ct (Abs (x, _, _)) = 166 let 167 val (u, ctxt') = yield_singleton Variable.variant_fixes x ctxt; 168 val (v, ct') = Thm.dest_abs (SOME u) ct; 169 val (thm, prems) = rewrite' ctxt' prems (x :: bounds) thms ct' 170 in 171 if Thm.is_reflexive thm then 172 (Thm.reflexive ct, prems) 173 else 174 (Thm.abstract_rule x v thm, prems) 175 end 176 | rewrite_subterm prems ct (_ $ _) = 177 let 178 val (cs, ct) = Thm.dest_comb ct 179 val (thm, prems') = rewrite' ctxt prems bounds thms cs 180 val (thm', prems'') = rewrite' ctxt prems' bounds thms ct 181 in 182 (Thm.combination thm thm', prems'') 183 end 184 | rewrite_subterm prems ct _ = (Thm.reflexive ct, prems) 185 val t = Thm.term_of ct 186 in 187 case get_first (apply_rule t) thms of 188 NONE => rewrite_subterm old_prems ct t 189 | SOME (thm, rhs, prems) => 190 case rewrite' ctxt prems bounds thms rhs of 191 (thm', prems) => (Thm.transitive thm thm', prems) 192 end 193 194fun rewrite ctxt thms ct = 195 let 196 val thm1 = Thm.eta_long_conversion ct 197 val rhs = thm1 |> Thm.cprop_of |> Thm.dest_comb |> snd 198 val (thm2, prems) = rewrite' ctxt [] [] thms rhs 199 val rhs = thm2 |> Thm.cprop_of |> Thm.dest_comb |> snd 200 val thm3 = Thm.eta_conversion rhs 201 val thm = Thm.transitive thm1 (Thm.transitive thm2 thm3) 202 in 203 fold (fn prem => fn thm => Thm.implies_intr (Thm.cterm_of ctxt prem) thm) prems thm 204 end 205 206fun preproc_term_conv ctxt = 207 let 208 val thms = Named_Theorems.get ctxt \<^named_theorems>\<open>real_asymp_reify_simps\<close> 209 val thms = map (fn thm => thm RS @{thm HOL.eq_reflection}) thms 210 in 211 rewrite ctxt thms 212 end 213 214fun register_custom' binding pat expand context = 215 let 216 val n = pat |> fastype_of |> strip_type |> fst |> length 217 val maxidx = Term.maxidx_of_term pat 218 val vars = map (fn i => Var ((Name.uu_, maxidx + i), \<^typ>\<open>real\<close>)) (1 upto n) 219 val net_pat = Library.foldl betapply (pat, vars) 220 val {name_table = tbl, net = net} = Custom_Funs.get context 221 val entry' = {pat = pat, net_pat = net_pat, expand = expand} 222 val (name, tbl) = Name_Space.define context true (binding, entry') tbl 223 val entry = {name = name, pat = pat, net_pat = net_pat, expand = expand} 224 val net = Item_Net.update entry net 225 in 226 Custom_Funs.put {name_table = tbl, net = net} context 227 end 228 229fun register_custom binding pat expand = 230 let 231 fun decl phi = 232 register_custom' binding (Morphism.term phi pat) expand 233 in 234 Local_Theory.declaration {syntax = false, pervasive = false} decl 235 end 236 237fun register_custom_from_thm binding thm expand = 238 let 239 val pat = thm |> Thm.concl_of |> HOLogic.dest_Trueprop |> dest_comb |> snd 240 in 241 register_custom binding pat expand 242 end 243 244fun expand_custom ctxt name = 245 let 246 val {name_table, ...} = Custom_Funs.get (Context.Proof ctxt) 247 in 248 case Name_Space.lookup name_table name of 249 NONE => NONE 250 | SOME {expand, ...} => SOME expand 251 end 252 253fun expr_to_term e = 254 let 255 fun expr_to_term' (ConstExpr c) = c 256 | expr_to_term' X = Bound 0 257 | expr_to_term' (Add (a, b)) = 258 \<^term>\<open>(+) :: real => _\<close> $ expr_to_term' a $ expr_to_term' b 259 | expr_to_term' (Mult (a, b)) = 260 \<^term>\<open>(*) :: real => _\<close> $ expr_to_term' a $ expr_to_term' b 261 | expr_to_term' (Minus (a, b)) = 262 \<^term>\<open>(-) :: real => _\<close> $ expr_to_term' a $ expr_to_term' b 263 | expr_to_term' (Div (a, b)) = 264 \<^term>\<open>(/) :: real => _\<close> $ expr_to_term' a $ expr_to_term' b 265 | expr_to_term' (Uminus a) = 266 \<^term>\<open>uminus :: real => _\<close> $ expr_to_term' a 267 | expr_to_term' (Inverse a) = 268 \<^term>\<open>inverse :: real => _\<close> $ expr_to_term' a 269 | expr_to_term' (Ln a) = 270 \<^term>\<open>ln :: real => _\<close> $ expr_to_term' a 271 | expr_to_term' (Exp a) = 272 \<^term>\<open>exp :: real => _\<close> $ expr_to_term' a 273 | expr_to_term' (Powr (a,b)) = 274 \<^term>\<open>(powr) :: real => _\<close> $ expr_to_term' a $ expr_to_term' b 275 | expr_to_term' (Powr_Nat (a,b)) = 276 \<^term>\<open>powr_nat :: real => _\<close> $ expr_to_term' a $ expr_to_term' b 277 | expr_to_term' (LnPowr (a,b)) = 278 \<^term>\<open>ln :: real => _\<close> $ 279 (\<^term>\<open>(powr) :: real => _\<close> $ expr_to_term' a $ expr_to_term' b) 280 | expr_to_term' (ExpLn a) = 281 \<^term>\<open>exp :: real => _\<close> $ (\<^term>\<open>ln :: real => _\<close> $ expr_to_term' a) 282 | expr_to_term' (Powr' (a,b)) = 283 \<^term>\<open>(powr) :: real => _\<close> $ expr_to_term' a $ b 284 | expr_to_term' (Power (a,b)) = 285 \<^term>\<open>(^) :: real => _\<close> $ expr_to_term' a $ b 286 | expr_to_term' (Floor a) = 287 \<^term>\<open>Multiseries_Expansion.rfloor\<close> $ expr_to_term' a 288 | expr_to_term' (Ceiling a) = 289 \<^term>\<open>Multiseries_Expansion.rceil\<close> $ expr_to_term' a 290 | expr_to_term' (Frac a) = 291 \<^term>\<open>Archimedean_Field.frac :: real \<Rightarrow> real\<close> $ expr_to_term' a 292 | expr_to_term' (NatMod (a,b)) = 293 \<^term>\<open>Multiseries_Expansion.rnatmod\<close> $ expr_to_term' a $ expr_to_term' b 294 | expr_to_term' (Root (a,b)) = 295 \<^term>\<open>root :: nat \<Rightarrow> real \<Rightarrow> _\<close> $ b $ expr_to_term' a 296 | expr_to_term' (Sin a) = 297 \<^term>\<open>sin :: real => _\<close> $ expr_to_term' a 298 | expr_to_term' (ArcTan a) = 299 \<^term>\<open>arctan :: real => _\<close> $ expr_to_term' a 300 | expr_to_term' (Cos a) = 301 \<^term>\<open>cos :: real => _\<close> $ expr_to_term' a 302 | expr_to_term' (Absolute a) = 303 \<^term>\<open>abs :: real => _\<close> $ expr_to_term' a 304 | expr_to_term' (Sgn a) = 305 \<^term>\<open>sgn :: real => _\<close> $ expr_to_term' a 306 | expr_to_term' (Min (a,b)) = 307 \<^term>\<open>min :: real => _\<close> $ expr_to_term' a $ expr_to_term' b 308 | expr_to_term' (Max (a,b)) = 309 \<^term>\<open>max :: real => _\<close> $ expr_to_term' a $ expr_to_term' b 310 | expr_to_term' (Custom (_, t, args)) = Envir.beta_eta_contract ( 311 fold (fn e => fn t => betapply (t, expr_to_term' e )) args t) 312 in 313 Abs ("x", \<^typ>\<open>real\<close>, expr_to_term' e) 314 end 315 316fun reify_custom ctxt t = 317 let 318 val thy = Proof_Context.theory_of ctxt 319 val t = Envir.beta_eta_contract t 320 val t' = Envir.beta_eta_contract (Term.abs ("x", \<^typ>\<open>real\<close>) t) 321 val {net, ...} = Custom_Funs.get (Context.Proof ctxt) 322 val entries = Item_Net.retrieve_matching net (Term.subst_bound (Free ("x", \<^typ>\<open>real\<close>), t)) 323 fun go {pat, name, ...} = 324 let 325 val n = pat |> fastype_of |> strip_type |> fst |> length 326 val maxidx = Term.maxidx_of_term t' 327 val vs = map (fn i => (Name.uu_, maxidx + i)) (1 upto n) 328 val args = map (fn v => Var (v, \<^typ>\<open>real => real\<close>) $ Bound 0) vs 329 val pat' = 330 Envir.beta_eta_contract (Term.abs ("x", \<^typ>\<open>real\<close>) 331 (Library.foldl betapply (pat, args))) 332 val (T_insts, insts) = Pattern.match thy (pat', t') (Vartab.empty, Vartab.empty) 333 fun map_option _ [] acc = SOME (rev acc) 334 | map_option f (x :: xs) acc = 335 case f x of 336 NONE => NONE 337 | SOME y => map_option f xs (y :: acc) 338 val t = Envir.subst_term (T_insts, insts) pat 339 in 340 Option.map (pair (name, t)) (map_option (Option.map snd o Vartab.lookup insts) vs []) 341 end 342 handle Pattern.MATCH => NONE 343 in 344 get_first go entries 345 end 346 347fun reify_aux ctxt t' t = 348 let 349 fun is_const t = 350 fastype_of (Abs ("x", \<^typ>\<open>real\<close>, t)) = \<^typ>\<open>real \<Rightarrow> real\<close> 351 andalso not (exists_subterm (fn t => t = Bound 0) t) 352 fun is_const' t = not (exists_subterm (fn t => t = Bound 0) t) 353 fun reify'' (\<^term>\<open>(+) :: real => _\<close> $ s $ t) = 354 Add (reify' s, reify' t) 355 | reify'' (\<^term>\<open>(-) :: real => _\<close> $ s $ t) = 356 Minus (reify' s, reify' t) 357 | reify'' (\<^term>\<open>(*) :: real => _\<close> $ s $ t) = 358 Mult (reify' s, reify' t) 359 | reify'' (\<^term>\<open>(/) :: real => _\<close> $ s $ t) = 360 Div (reify' s, reify' t) 361 | reify'' (\<^term>\<open>uminus :: real => _\<close> $ s) = 362 Uminus (reify' s) 363 | reify'' (\<^term>\<open>inverse :: real => _\<close> $ s) = 364 Inverse (reify' s) 365 | reify'' (\<^term>\<open>ln :: real => _\<close> $ (\<^term>\<open>(powr) :: real => _\<close> $ s $ t)) = 366 LnPowr (reify' s, reify' t) 367 | reify'' (\<^term>\<open>exp :: real => _\<close> $ (\<^term>\<open>ln :: real => _\<close> $ s)) = 368 ExpLn (reify' s) 369 | reify'' (\<^term>\<open>ln :: real => _\<close> $ s) = 370 Ln (reify' s) 371 | reify'' (\<^term>\<open>exp :: real => _\<close> $ s) = 372 Exp (reify' s) 373 | reify'' (\<^term>\<open>(powr) :: real => _\<close> $ s $ t) = 374 (if is_const t then Powr' (reify' s, t) else Powr (reify' s, reify' t)) 375 | reify'' (\<^term>\<open>powr_nat :: real => _\<close> $ s $ t) = 376 Powr_Nat (reify' s, reify' t) 377 | reify'' (\<^term>\<open>(^) :: real => _\<close> $ s $ t) = 378 (if is_const' t then Power (reify' s, t) else raise TERM ("reify", [t'])) 379 | reify'' (\<^term>\<open>root\<close> $ s $ t) = 380 (if is_const' s then Root (reify' t, s) else raise TERM ("reify", [t'])) 381 | reify'' (\<^term>\<open>abs :: real => _\<close> $ s) = 382 Absolute (reify' s) 383 | reify'' (\<^term>\<open>sgn :: real => _\<close> $ s) = 384 Sgn (reify' s) 385 | reify'' (\<^term>\<open>min :: real => _\<close> $ s $ t) = 386 Min (reify' s, reify' t) 387 | reify'' (\<^term>\<open>max :: real => _\<close> $ s $ t) = 388 Max (reify' s, reify' t) 389 | reify'' (\<^term>\<open>Multiseries_Expansion.rfloor\<close> $ s) = 390 Floor (reify' s) 391 | reify'' (\<^term>\<open>Multiseries_Expansion.rceil\<close> $ s) = 392 Ceiling (reify' s) 393 | reify'' (\<^term>\<open>Archimedean_Field.frac :: real \<Rightarrow> real\<close> $ s) = 394 Frac (reify' s) 395 | reify'' (\<^term>\<open>Multiseries_Expansion.rnatmod\<close> $ s $ t) = 396 NatMod (reify' s, reify' t) 397 | reify'' (\<^term>\<open>sin :: real => _\<close> $ s) = 398 Sin (reify' s) 399 | reify'' (\<^term>\<open>arctan :: real => _\<close> $ s) = 400 ArcTan (reify' s) 401 | reify'' (\<^term>\<open>cos :: real => _\<close> $ s) = 402 Cos (reify' s) 403 | reify'' (Bound 0) = X 404 | reify'' t = 405 case reify_custom ctxt t of 406 SOME ((name, t), ts) => 407 let 408 val args = map (reify_aux ctxt t') ts 409 in 410 Custom (name, t, args) 411 end 412 | NONE => raise TERM ("reify", [t']) 413 and reify' t = if is_const t then ConstExpr t else reify'' t 414 in 415 case Envir.eta_long [] t of 416 Abs (_, \<^typ>\<open>real\<close>, t'') => reify' t'' 417 | _ => raise TERM ("reify", [t]) 418 end 419 420fun reify ctxt t = 421 let 422 val thm = preproc_term_conv ctxt (Thm.cterm_of ctxt t) 423 val rhs = thm |> Thm.concl_of |> Logic.dest_equals |> snd 424 in 425 (reify_aux ctxt t rhs, thm) 426 end 427 428fun reify_simple_aux ctxt t' t = 429 let 430 fun is_const t = 431 fastype_of (Abs ("x", \<^typ>\<open>real\<close>, t)) = \<^typ>\<open>real \<Rightarrow> real\<close> 432 andalso not (exists_subterm (fn t => t = Bound 0) t) 433 fun is_const' t = not (exists_subterm (fn t => t = Bound 0) t) 434 fun reify'' (\<^term>\<open>(+) :: real => _\<close> $ s $ t) = 435 Add (reify'' s, reify'' t) 436 | reify'' (\<^term>\<open>(-) :: real => _\<close> $ s $ t) = 437 Minus (reify'' s, reify'' t) 438 | reify'' (\<^term>\<open>(*) :: real => _\<close> $ s $ t) = 439 Mult (reify'' s, reify'' t) 440 | reify'' (\<^term>\<open>(/) :: real => _\<close> $ s $ t) = 441 Div (reify'' s, reify'' t) 442 | reify'' (\<^term>\<open>uminus :: real => _\<close> $ s) = 443 Uminus (reify'' s) 444 | reify'' (\<^term>\<open>inverse :: real => _\<close> $ s) = 445 Inverse (reify'' s) 446 | reify'' (\<^term>\<open>ln :: real => _\<close> $ s) = 447 Ln (reify'' s) 448 | reify'' (\<^term>\<open>exp :: real => _\<close> $ s) = 449 Exp (reify'' s) 450 | reify'' (\<^term>\<open>(powr) :: real => _\<close> $ s $ t) = 451 Powr (reify'' s, reify'' t) 452 | reify'' (\<^term>\<open>powr_nat :: real => _\<close> $ s $ t) = 453 Powr_Nat (reify'' s, reify'' t) 454 | reify'' (\<^term>\<open>(^) :: real => _\<close> $ s $ t) = 455 (if is_const' t then Power (reify'' s, t) else raise TERM ("reify", [t'])) 456 | reify'' (\<^term>\<open>root\<close> $ s $ t) = 457 (if is_const' s then Root (reify'' t, s) else raise TERM ("reify", [t'])) 458 | reify'' (\<^term>\<open>abs :: real => _\<close> $ s) = 459 Absolute (reify'' s) 460 | reify'' (\<^term>\<open>sgn :: real => _\<close> $ s) = 461 Sgn (reify'' s) 462 | reify'' (\<^term>\<open>min :: real => _\<close> $ s $ t) = 463 Min (reify'' s, reify'' t) 464 | reify'' (\<^term>\<open>max :: real => _\<close> $ s $ t) = 465 Max (reify'' s, reify'' t) 466 | reify'' (\<^term>\<open>Multiseries_Expansion.rfloor\<close> $ s) = 467 Floor (reify'' s) 468 | reify'' (\<^term>\<open>Multiseries_Expansion.rceil\<close> $ s) = 469 Ceiling (reify'' s) 470 | reify'' (\<^term>\<open>Archimedean_Field.frac :: real \<Rightarrow> real\<close> $ s) = 471 Frac (reify'' s) 472 | reify'' (\<^term>\<open>Multiseries_Expansion.rnatmod\<close> $ s $ t) = 473 NatMod (reify'' s, reify'' t) 474 | reify'' (\<^term>\<open>sin :: real => _\<close> $ s) = 475 Sin (reify'' s) 476 | reify'' (\<^term>\<open>cos :: real => _\<close> $ s) = 477 Cos (reify'' s) 478 | reify'' (Bound 0) = X 479 | reify'' t = 480 if is_const t then 481 ConstExpr t 482 else 483 case reify_custom ctxt t of 484 SOME ((name, t), ts) => 485 let 486 val args = map (reify_aux ctxt t') ts 487 in 488 Custom (name, t, args) 489 end 490 | NONE => raise TERM ("reify", [t']) 491 in 492 case Envir.eta_long [] t of 493 Abs (_, \<^typ>\<open>real\<close>, t'') => reify'' t'' 494 | _ => raise TERM ("reify", [t]) 495 end 496 497fun reify_simple ctxt t = 498 let 499 val thm = preproc_term_conv ctxt (Thm.cterm_of ctxt t) 500 val rhs = thm |> Thm.concl_of |> Logic.dest_equals |> snd 501 in 502 (reify_simple_aux ctxt t rhs, thm) 503 end 504 505fun simple_print_const (Free (x, _)) = x 506 | simple_print_const (\<^term>\<open>uminus :: real => real\<close> $ a) = 507 "(-" ^ simple_print_const a ^ ")" 508 | simple_print_const (\<^term>\<open>(+) :: real => _\<close> $ a $ b) = 509 "(" ^ simple_print_const a ^ "+" ^ simple_print_const b ^ ")" 510 | simple_print_const (\<^term>\<open>(-) :: real => _\<close> $ a $ b) = 511 "(" ^ simple_print_const a ^ "-" ^ simple_print_const b ^ ")" 512 | simple_print_const (\<^term>\<open>(*) :: real => _\<close> $ a $ b) = 513 "(" ^ simple_print_const a ^ "*" ^ simple_print_const b ^ ")" 514 | simple_print_const (\<^term>\<open>inverse :: real => _\<close> $ a) = 515 "(1 / " ^ simple_print_const a ^ ")" 516 | simple_print_const (\<^term>\<open>(/) :: real => _\<close> $ a $ b) = 517 "(" ^ simple_print_const a ^ "/" ^ simple_print_const b ^ ")" 518 | simple_print_const t = Int.toString (snd (HOLogic.dest_number t)) 519 520fun to_mathematica (Add (a, b)) = "(" ^ to_mathematica a ^ " + " ^ to_mathematica b ^ ")" 521 | to_mathematica (Minus (a, b)) = "(" ^ to_mathematica a ^ " - " ^ to_mathematica b ^ ")" 522 | to_mathematica (Mult (a, b)) = "(" ^ to_mathematica a ^ " * " ^ to_mathematica b ^ ")" 523 | to_mathematica (Div (a, b)) = "(" ^ to_mathematica a ^ " / " ^ to_mathematica b ^ ")" 524 | to_mathematica (Powr (a, b)) = "(" ^ to_mathematica a ^ " ^ " ^ to_mathematica b ^ ")" 525 | to_mathematica (Powr_Nat (a, b)) = "(" ^ to_mathematica a ^ " ^ " ^ to_mathematica b ^ ")" 526 | to_mathematica (Powr' (a, b)) = "(" ^ to_mathematica a ^ " ^ " ^ 527 to_mathematica (ConstExpr b) ^ ")" 528 | to_mathematica (LnPowr (a, b)) = "Log[" ^ to_mathematica a ^ " ^ " ^ to_mathematica b ^ "]" 529 | to_mathematica (ExpLn a) = "Exp[Ln[" ^ to_mathematica a ^ "]]" 530 | to_mathematica (Power (a, b)) = "(" ^ to_mathematica a ^ " ^ " ^ 531 to_mathematica (ConstExpr b) ^ ")" 532 | to_mathematica (Root (a, \<^term>\<open>2::real\<close>)) = "Sqrt[" ^ to_mathematica a ^ "]" 533 | to_mathematica (Root (a, b)) = "Surd[" ^ to_mathematica a ^ ", " ^ 534 to_mathematica (ConstExpr b) ^ "]" 535 | to_mathematica (Uminus a) = "(-" ^ to_mathematica a ^ ")" 536 | to_mathematica (Inverse a) = "(1/(" ^ to_mathematica a ^ "))" 537 | to_mathematica (Exp a) = "Exp[" ^ to_mathematica a ^ "]" 538 | to_mathematica (Ln a) = "Log[" ^ to_mathematica a ^ "]" 539 | to_mathematica (Sin a) = "Sin[" ^ to_mathematica a ^ "]" 540 | to_mathematica (Cos a) = "Cos[" ^ to_mathematica a ^ "]" 541 | to_mathematica (ArcTan a) = "ArcTan[" ^ to_mathematica a ^ "]" 542 | to_mathematica (Absolute a) = "Abs[" ^ to_mathematica a ^ "]" 543 | to_mathematica (Sgn a) = "Sign[" ^ to_mathematica a ^ "]" 544 | to_mathematica (Min (a, b)) = "Min[" ^ to_mathematica a ^ ", " ^ to_mathematica b ^ "]" 545 | to_mathematica (Max (a, b)) = "Max[" ^ to_mathematica a ^ ", " ^ to_mathematica b ^ "]" 546 | to_mathematica (Floor a) = "Floor[" ^ to_mathematica a ^ "]" 547 | to_mathematica (Ceiling a) = "Ceiling[" ^ to_mathematica a ^ "]" 548 | to_mathematica (Frac a) = "Mod[" ^ to_mathematica a ^ ", 1]" 549 | to_mathematica (ConstExpr t) = simple_print_const t 550 | to_mathematica X = "X" 551 552(* TODO: correct translation of frac() for Maple and Sage *) 553fun to_maple (Add (a, b)) = "(" ^ to_maple a ^ " + " ^ to_maple b ^ ")" 554 | to_maple (Minus (a, b)) = "(" ^ to_maple a ^ " - " ^ to_maple b ^ ")" 555 | to_maple (Mult (a, b)) = "(" ^ to_maple a ^ " * " ^ to_maple b ^ ")" 556 | to_maple (Div (a, b)) = "(" ^ to_maple a ^ " / " ^ to_maple b ^ ")" 557 | to_maple (Powr (a, b)) = "(" ^ to_maple a ^ " ^ " ^ to_maple b ^ ")" 558 | to_maple (Powr_Nat (a, b)) = "(" ^ to_maple a ^ " ^ " ^ to_maple b ^ ")" 559 | to_maple (Powr' (a, b)) = "(" ^ to_maple a ^ " ^ " ^ 560 to_maple (ConstExpr b) ^ ")" 561 | to_maple (LnPowr (a, b)) = "ln(" ^ to_maple a ^ " ^ " ^ to_maple b ^ ")" 562 | to_maple (ExpLn a) = "ln(exp(" ^ to_maple a ^ "))" 563 | to_maple (Power (a, b)) = "(" ^ to_maple a ^ " ^ " ^ 564 to_maple (ConstExpr b) ^ ")" 565 | to_maple (Root (a, \<^term>\<open>2::real\<close>)) = "sqrt(" ^ to_maple a ^ ")" 566 | to_maple (Root (a, b)) = "root(" ^ to_maple a ^ ", " ^ 567 to_maple (ConstExpr b) ^ ")" 568 | to_maple (Uminus a) = "(-" ^ to_maple a ^ ")" 569 | to_maple (Inverse a) = "(1/(" ^ to_maple a ^ "))" 570 | to_maple (Exp a) = "exp(" ^ to_maple a ^ ")" 571 | to_maple (Ln a) = "ln(" ^ to_maple a ^ ")" 572 | to_maple (Sin a) = "sin(" ^ to_maple a ^ ")" 573 | to_maple (Cos a) = "cos(" ^ to_maple a ^ ")" 574 | to_maple (ArcTan a) = "arctan(" ^ to_maple a ^ ")" 575 | to_maple (Absolute a) = "abs(" ^ to_maple a ^ ")" 576 | to_maple (Sgn a) = "signum(" ^ to_maple a ^ ")" 577 | to_maple (Min (a, b)) = "min(" ^ to_maple a ^ ", " ^ to_maple b ^ ")" 578 | to_maple (Max (a, b)) = "max(" ^ to_maple a ^ ", " ^ to_maple b ^ ")" 579 | to_maple (Floor a) = "floor(" ^ to_maple a ^ ")" 580 | to_maple (Ceiling a) = "ceil(" ^ to_maple a ^ ")" 581 | to_maple (Frac a) = "frac(" ^ to_maple a ^ ")" 582 | to_maple (ConstExpr t) = simple_print_const t 583 | to_maple X = "x" 584 585fun to_maxima (Add (a, b)) = "(" ^ to_maxima a ^ " + " ^ to_maxima b ^ ")" 586 | to_maxima (Minus (a, b)) = "(" ^ to_maxima a ^ " - " ^ to_maxima b ^ ")" 587 | to_maxima (Mult (a, b)) = "(" ^ to_maxima a ^ " * " ^ to_maxima b ^ ")" 588 | to_maxima (Div (a, b)) = "(" ^ to_maxima a ^ " / " ^ to_maxima b ^ ")" 589 | to_maxima (Powr (a, b)) = "(" ^ to_maxima a ^ " ^ " ^ to_maxima b ^ ")" 590 | to_maxima (Powr_Nat (a, b)) = "(" ^ to_maxima a ^ " ^ " ^ to_maxima b ^ ")" 591 | to_maxima (Powr' (a, b)) = "(" ^ to_maxima a ^ " ^ " ^ 592 to_maxima (ConstExpr b) ^ ")" 593 | to_maxima (ExpLn a) = "exp (log (" ^ to_maxima a ^ "))" 594 | to_maxima (LnPowr (a, b)) = "log(" ^ to_maxima a ^ " ^ " ^ to_maxima b ^ ")" 595 | to_maxima (Power (a, b)) = "(" ^ to_maxima a ^ " ^ " ^ 596 to_maxima (ConstExpr b) ^ ")" 597 | to_maxima (Root (a, \<^term>\<open>2::real\<close>)) = "sqrt(" ^ to_maxima a ^ ")" 598 | to_maxima (Root (a, b)) = to_maxima a ^ "^(1/" ^ 599 to_maxima (ConstExpr b) ^ ")" 600 | to_maxima (Uminus a) = "(-" ^ to_maxima a ^ ")" 601 | to_maxima (Inverse a) = "(1/(" ^ to_maxima a ^ "))" 602 | to_maxima (Exp a) = "exp(" ^ to_maxima a ^ ")" 603 | to_maxima (Ln a) = "log(" ^ to_maxima a ^ ")" 604 | to_maxima (Sin a) = "sin(" ^ to_maxima a ^ ")" 605 | to_maxima (Cos a) = "cos(" ^ to_maxima a ^ ")" 606 | to_maxima (ArcTan a) = "atan(" ^ to_maxima a ^ ")" 607 | to_maxima (Absolute a) = "abs(" ^ to_maxima a ^ ")" 608 | to_maxima (Sgn a) = "signum(" ^ to_maxima a ^ ")" 609 | to_maxima (Min (a, b)) = "min(" ^ to_maxima a ^ ", " ^ to_maxima b ^ ")" 610 | to_maxima (Max (a, b)) = "max(" ^ to_maxima a ^ ", " ^ to_maxima b ^ ")" 611 | to_maxima (Floor a) = "floor(" ^ to_maxima a ^ ")" 612 | to_maxima (Ceiling a) = "ceil(" ^ to_maxima a ^ ")" 613 | to_maxima (Frac a) = let val x = to_maxima a in "(" ^ x ^ " - floor(" ^ x ^ "))" end 614 | to_maxima (ConstExpr t) = simple_print_const t 615 | to_maxima X = "x" 616 617fun to_sympy (Add (a, b)) = "(" ^ to_sympy a ^ " + " ^ to_sympy b ^ ")" 618 | to_sympy (Minus (a, b)) = "(" ^ to_sympy a ^ " - " ^ to_sympy b ^ ")" 619 | to_sympy (Mult (a, b)) = "(" ^ to_sympy a ^ " * " ^ to_sympy b ^ ")" 620 | to_sympy (Div (a, b)) = "(" ^ to_sympy a ^ " / " ^ to_sympy b ^ ")" 621 | to_sympy (Powr (a, b)) = "(" ^ to_sympy a ^ " ** " ^ to_sympy b ^ ")" 622 | to_sympy (Powr_Nat (a, b)) = "(" ^ to_sympy a ^ " ** " ^ to_sympy b ^ ")" 623 | to_sympy (Powr' (a, b)) = "(" ^ to_sympy a ^ " ** " ^ 624 to_sympy (ConstExpr b) ^ ")" 625 | to_sympy (ExpLn a) = "exp (log (" ^ to_sympy a ^ "))" 626 | to_sympy (LnPowr (a, b)) = "log(" ^ to_sympy a ^ " ** " ^ to_sympy b ^ ")" 627 | to_sympy (Power (a, b)) = "(" ^ to_sympy a ^ " ** " ^ 628 to_sympy (ConstExpr b) ^ ")" 629 | to_sympy (Root (a, \<^term>\<open>2::real\<close>)) = "sqrt(" ^ to_sympy a ^ ")" 630 | to_sympy (Root (a, b)) = "root(" ^ to_sympy a ^ ", " ^ to_sympy (ConstExpr b) ^ ")" 631 | to_sympy (Uminus a) = "(-" ^ to_sympy a ^ ")" 632 | to_sympy (Inverse a) = "(1/(" ^ to_sympy a ^ "))" 633 | to_sympy (Exp a) = "exp(" ^ to_sympy a ^ ")" 634 | to_sympy (Ln a) = "log(" ^ to_sympy a ^ ")" 635 | to_sympy (Sin a) = "sin(" ^ to_sympy a ^ ")" 636 | to_sympy (Cos a) = "cos(" ^ to_sympy a ^ ")" 637 | to_sympy (ArcTan a) = "atan(" ^ to_sympy a ^ ")" 638 | to_sympy (Absolute a) = "abs(" ^ to_sympy a ^ ")" 639 | to_sympy (Sgn a) = "sign(" ^ to_sympy a ^ ")" 640 | to_sympy (Min (a, b)) = "min(" ^ to_sympy a ^ ", " ^ to_sympy b ^ ")" 641 | to_sympy (Max (a, b)) = "max(" ^ to_sympy a ^ ", " ^ to_sympy b ^ ")" 642 | to_sympy (Floor a) = "floor(" ^ to_sympy a ^ ")" 643 | to_sympy (Ceiling a) = "ceiling(" ^ to_sympy a ^ ")" 644 | to_sympy (Frac a) = "frac(" ^ to_sympy a ^ ")" 645 | to_sympy (ConstExpr t) = simple_print_const t 646 | to_sympy X = "x" 647 648fun to_sage (Add (a, b)) = "(" ^ to_sage a ^ " + " ^ to_sage b ^ ")" 649 | to_sage (Minus (a, b)) = "(" ^ to_sage a ^ " - " ^ to_sage b ^ ")" 650 | to_sage (Mult (a, b)) = "(" ^ to_sage a ^ " * " ^ to_sage b ^ ")" 651 | to_sage (Div (a, b)) = "(" ^ to_sage a ^ " / " ^ to_sage b ^ ")" 652 | to_sage (Powr (a, b)) = "(" ^ to_sage a ^ " ^ " ^ to_sage b ^ ")" 653 | to_sage (Powr_Nat (a, b)) = "(" ^ to_sage a ^ " ^ " ^ to_sage b ^ ")" 654 | to_sage (Powr' (a, b)) = "(" ^ to_sage a ^ " ^ " ^ 655 to_sage (ConstExpr b) ^ ")" 656 | to_sage (ExpLn a) = "exp (log (" ^ to_sage a ^ "))" 657 | to_sage (LnPowr (a, b)) = "log(" ^ to_sage a ^ " ^ " ^ to_sage b ^ ")" 658 | to_sage (Power (a, b)) = "(" ^ to_sage a ^ " ^ " ^ 659 to_sage (ConstExpr b) ^ ")" 660 | to_sage (Root (a, \<^term>\<open>2::real\<close>)) = "sqrt(" ^ to_sage a ^ ")" 661 | to_sage (Root (a, b)) = to_sage a ^ "^(1/" ^ to_sage (ConstExpr b) ^ ")" 662 | to_sage (Uminus a) = "(-" ^ to_sage a ^ ")" 663 | to_sage (Inverse a) = "(1/(" ^ to_sage a ^ "))" 664 | to_sage (Exp a) = "exp(" ^ to_sage a ^ ")" 665 | to_sage (Ln a) = "log(" ^ to_sage a ^ ")" 666 | to_sage (Sin a) = "sin(" ^ to_sage a ^ ")" 667 | to_sage (Cos a) = "cos(" ^ to_sage a ^ ")" 668 | to_sage (ArcTan a) = "atan(" ^ to_sage a ^ ")" 669 | to_sage (Absolute a) = "abs(" ^ to_sage a ^ ")" 670 | to_sage (Sgn a) = "sign(" ^ to_sage a ^ ")" 671 | to_sage (Min (a, b)) = "min(" ^ to_sage a ^ ", " ^ to_sage b ^ ")" 672 | to_sage (Max (a, b)) = "max(" ^ to_sage a ^ ", " ^ to_sage b ^ ")" 673 | to_sage (Floor a) = "floor(" ^ to_sage a ^ ")" 674 | to_sage (Ceiling a) = "ceil(" ^ to_sage a ^ ")" 675 | to_sage (Frac a) = "frac(" ^ to_sage a ^ ")" 676 | to_sage (ConstExpr t) = simple_print_const t 677 | to_sage X = "x" 678 679fun reify_mathematica ctxt = to_mathematica o fst o reify_simple ctxt 680fun reify_maple ctxt = to_maple o fst o reify_simple ctxt 681fun reify_maxima ctxt = to_maxima o fst o reify_simple ctxt 682fun reify_sympy ctxt = to_sympy o fst o reify_simple ctxt 683fun reify_sage ctxt = to_sage o fst o reify_simple ctxt 684 685fun limit_mathematica s = "Limit[" ^ s ^ ", X -> Infinity]" 686fun limit_maple s = "limit(" ^ s ^ ", x = infinity);" 687fun limit_maxima s = "limit(" ^ s ^ ", x, inf);" 688fun limit_sympy s = "limit(" ^ s ^ ", x, oo)" 689fun limit_sage s = "limit(" ^ s ^ ", x = Infinity)" 690 691end 692