404 q1 = q2 andalso length xs1 = length xs2 andalso |
404 q1 = q2 andalso length xs1 = length xs2 andalso |
405 is_same_formula comm ((map fst xs1 ~~ map fst xs2) @ subst) phi1 phi2 |
405 is_same_formula comm ((map fst xs1 ~~ map fst xs2) @ subst) phi1 phi2 |
406 | is_same_formula comm subst (AConn (c1, phis1)) (AConn (c2, phis2)) = |
406 | is_same_formula comm subst (AConn (c1, phis1)) (AConn (c2, phis2)) = |
407 c1 = c2 andalso length phis1 = length phis2 andalso |
407 c1 = c2 andalso length phis1 = length phis2 andalso |
408 forall (uncurry (is_same_formula comm subst)) (phis1 ~~ phis2) |
408 forall (uncurry (is_same_formula comm subst)) (phis1 ~~ phis2) |
409 | is_same_formula comm subst |
409 | is_same_formula comm subst (AAtom (tm1 as ATerm (("equal", tys), [tm11, tm12]))) (AAtom tm2) = |
410 (AAtom (tm1 as ATerm (("equal", tys), [tm11, tm12]))) (AAtom tm2) = |
|
411 is_same_term subst tm1 tm2 orelse |
410 is_same_term subst tm1 tm2 orelse |
412 (comm andalso is_same_term subst (ATerm (("equal", tys), [tm12, tm11])) tm2) |
411 (comm andalso is_same_term subst (ATerm (("equal", tys), [tm12, tm11])) tm2) |
413 | is_same_formula _ subst (AAtom tm1) (AAtom tm2) = is_same_term subst tm1 tm2 |
412 | is_same_formula _ subst (AAtom tm1) (AAtom tm2) = is_same_term subst tm1 tm2 |
414 | is_same_formula _ _ _ _ = false |
413 | is_same_formula _ _ _ _ = false |
415 |
414 |
449 (* Waldmeister isn't exactly helping. *) |
448 (* Waldmeister isn't exactly helping. *) |
450 (case deps of |
449 (case deps of |
451 File_Source (_, SOME s) => |
450 File_Source (_, SOME s) => |
452 (if s = waldmeister_conjecture_name then |
451 (if s = waldmeister_conjecture_name then |
453 (case find_formula_in_problem (mk_anot phi) problem of |
452 (case find_formula_in_problem (mk_anot phi) problem of |
454 (* Waldmeister hack: Get the original orientation of the |
453 (* Waldmeister hack: Get the original orientation of the equation to avoid |
455 equation to avoid confusing Isar. *) |
454 confusing Isar. *) |
456 [(s, phi')] => |
455 [(s, phi')] => |
457 ((num, [s]), |
456 ((num, [s]), |
458 phi |> not (is_same_formula false [] (mk_anot phi) phi') ? commute_eq) |
457 phi |> not (is_same_formula false [] (mk_anot phi) phi') ? commute_eq) |
459 | _ => ((num, []), phi)) |
458 | _ => ((num, []), phi)) |
460 else |
459 else |