equal
deleted
inserted
replaced
320 |
320 |
321 val SOME (t'', _) = rewrite_set_ @{theory Isac} true multiply_ansatz t'; (*true*) |
321 val SOME (t'', _) = rewrite_set_ @{theory Isac} true multiply_ansatz t'; (*true*) |
322 term2str t'' = "(z - 1 / 2) * (z - -1 / 4) * 3 / ((-1 + -2 * z + 8 * z ^^^ 2) * 3 / 24) =\n" ^ |
322 term2str t'' = "(z - 1 / 2) * (z - -1 / 4) * 3 / ((-1 + -2 * z + 8 * z ^^^ 2) * 3 / 24) =\n" ^ |
323 "?A * (z - -1 / 4) + ?B * (z - 1 / 2)"; (*true*) |
323 "?A * (z - -1 / 4) + ?B * (z - 1 / 2)"; (*true*) |
324 |
324 |
325 val SOME (t''', _) = rewrite_set_ @{theory Isac} true norm_Rational t''; |
325 val SOME (t''', _) = rewrite_set_ @{theory Isac} true norm_Rational t''; |
326 if term2str t''' = "3 = ?A * (1 + 4 * z) / 4 + ?B * (-1 + 2 * z) / 2" then () |
326 if term2str t''' = "3 = ?A * (1 + 4 * z) / 4 + ?B * (-1 + 2 * z) / 2" then () |
327 else error "ansatz_rls - multiply_ansatz - norm_Rational broken"; |
327 else error "ansatz_rls - multiply_ansatz - norm_Rational broken"; |
328 |
328 |
329 (*test for outcommented 3 lines in script: empower erls for x = a*b ==> ...*) |
329 (*test for outcommented 3 lines in script: empower erls for x = a*b ==> ...*) |
330 val xxx = append_rls "multiply_ansatz_erls" norm_Rational |
330 val xxx = append_rls "multiply_ansatz_erls" norm_Rational |
331 [Calc ("HOL.eq",eval_equal "#equal_")]; |
331 [Calc ("HOL.eq",eval_equal "#equal_")]; |
332 |
332 |