78 \<^rule_thm>\<open>rule4\<close>, |
78 \<^rule_thm>\<open>rule4\<close>, |
79 \<^rule_thm>\<open>rule1\<close> |
79 \<^rule_thm>\<open>rule1\<close> |
80 ]; |
80 ]; |
81 |
81 |
82 \<close> ML \<open> |
82 \<close> ML \<open> |
83 val t = TermC.str2term "z / (z - 1) + z / (z - \<alpha>) + 1::real"; |
83 val t = TermC.parse_test @{context} "z / (z - 1) + z / (z - \<alpha>) + 1::real"; |
84 \<close> ML \<open> |
84 \<close> ML \<open> |
85 val SOME (t', asm) = Rewrite.rewrite_set_ thy true inverse_Z t; |
85 val SOME (t', asm) = Rewrite.rewrite_set_ thy true inverse_Z t; |
86 (*rewrite__set_ called with 'Erls' for '|| z || < 1'*) |
86 (*rewrite__set_ called with 'Erls' for '|| z || < 1'*) |
87 \<close> ML \<open> |
87 \<close> ML \<open> |
88 UnparseC.term t' = "z / (z - ?\<delta> [?n]) + z / (z - \<alpha>) + ?\<delta> [?n]"; |
88 UnparseC.term t' = "z / (z - ?\<delta> [?n]) + z / (z - \<alpha>) + ?\<delta> [?n]"; |
406 \<close> |
406 \<close> |
407 (* ML {* |
407 (* ML {* |
408 probably keep these test in test/Tools/isac/... |
408 probably keep these test in test/Tools/isac/... |
409 (*mk_prod TermC.empty [];*) |
409 (*mk_prod TermC.empty [];*) |
410 |
410 |
411 val prod = mk_prod TermC.empty [str2term "x + 123"]; |
411 val prod = mk_prod TermC.empty [parse_test @{context} "x + 123"]; |
412 UnparseC.term prod = "x + 123"; |
412 UnparseC.term prod = "x + 123"; |
413 |
413 |
414 val sol = str2term "[z = 1 / 2, z = -1 / 4]"; |
414 val sol = parse_test @{context} "[z = 1 / 2, z = -1 / 4]"; |
415 val sols = HOLogic.dest_list sol; |
415 val sols = HOLogic.dest_list sol; |
416 val facs = map fac_from_sol sols; |
416 val facs = map fac_from_sol sols; |
417 val prod = mk_prod TermC.empty facs; |
417 val prod = mk_prod TermC.empty facs; |
418 UnparseC.term prod = "(z + -1 * (1 / 2)) * (z + -1 * (-1 / 4))"; |
418 UnparseC.term prod = "(z + -1 * (1 / 2)) * (z + -1 * (-1 / 4))"; |
419 |
419 |
420 val prod = |
420 val prod = |
421 mk_prod TermC.empty [str2term "x + 1", str2term "x + 2", str2term "x + 3"]; |
421 mk_prod TermC.empty [parse_test @{context} "x + 1", parse_test @{context} "x + 2", parse_test @{context} "x + 3"]; |
422 UnparseC.term prod = "(x + 1) * (x + 2) * (x + 3)"; |
422 UnparseC.term prod = "(x + 1) * (x + 2) * (x + 3)"; |
423 *} *) |
423 *} *) |
424 ML \<open> |
424 ML \<open> |
425 fun factors_from_solution sol = |
425 fun factors_from_solution sol = |
426 let val ts = HOLogic.dest_list sol |
426 let val ts = HOLogic.dest_list sol |
427 in mk_prod TermC.empty (map fac_from_sol ts) end; |
427 in mk_prod TermC.empty (map fac_from_sol ts) end; |
428 \<close> |
428 \<close> |
429 (* ML {* |
429 (* ML {* |
430 val sol = str2term "[z = 1 / 2, z = -1 / 4]"; |
430 val sol = parse_test @{context} "[z = 1 / 2, z = -1 / 4]"; |
431 val fs = factors_from_solution sol; |
431 val fs = factors_from_solution sol; |
432 UnparseC.term fs = "(z + -1 * (1 / 2)) * (z + -1 * (-1 / 4))" |
432 UnparseC.term fs = "(z + -1 * (1 / 2)) * (z + -1 * (-1 / 4))" |
433 *} *) |
433 *} *) |
434 text \<open>\noindent This function needs to be packed such that it can be evaluated |
434 text \<open>\noindent This function needs to be packed such that it can be evaluated |
435 by the Lucas-Interpreter. Therefor we moved the function to the |
435 by the Lucas-Interpreter. Therefor we moved the function to the |