# HG changeset patch
# User blanchet
# Date 1337003666 -7200
# Node ID fc26d5538868d6a098ebc3839422d9388cffc30c
# Parent  a5c2386518e2cf3d81dc4e3e1924514ea1b5a040
ensure the "show" equation is not reoriented by Waldmeister

diff -r a5c2386518e2 -r fc26d5538868 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Mon May 14 15:54:26 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Mon May 14 15:54:26 2012 +0200
@@ -341,26 +341,29 @@
         | _ => NONE
   in SOME subst |> do_term_pair (tm1, tm2) |> is_some end
 
-fun is_same_formula subst (AQuant (q1, xs1, phi1)) (AQuant (q2, xs2, phi2)) =
+fun is_same_formula comm subst (AQuant (q1, xs1, phi1)) (AQuant (q2, xs2, phi2)) =
     q1 = q2 andalso length xs1 = length xs2 andalso
-    is_same_formula ((map fst xs1 ~~ map fst xs2) @ subst) phi1 phi2
-  | is_same_formula subst (AConn (c1, phis1)) (AConn (c2, phis2)) =
+    is_same_formula comm ((map fst xs1 ~~ map fst xs2) @ subst) phi1 phi2
+  | is_same_formula comm subst (AConn (c1, phis1)) (AConn (c2, phis2)) =
     c1 = c2 andalso length phis1 = length phis2 andalso
-    forall (uncurry (is_same_formula subst)) (phis1 ~~ phis2)
-  | is_same_formula subst (AAtom (ATerm ("equal", [tm11, tm12]))) (AAtom tm2) =
+    forall (uncurry (is_same_formula comm subst)) (phis1 ~~ phis2)
+  | is_same_formula comm subst (AAtom (ATerm ("equal", [tm11, tm12]))) (AAtom tm2) =
     is_same_term subst (ATerm ("equal", [tm11, tm12])) tm2 orelse
-    is_same_term subst (ATerm ("equal", [tm12, tm11])) tm2
-  | is_same_formula subst (AAtom tm1) (AAtom tm2) = is_same_term subst tm1 tm2
-  | is_same_formula _ _ _ = false
+    (comm andalso is_same_term subst (ATerm ("equal", [tm12, tm11])) tm2)
+  | is_same_formula _ subst (AAtom tm1) (AAtom tm2) = is_same_term subst tm1 tm2
+  | is_same_formula _ _ _ _ = false
 
 fun matching_formula_line_identifier phi (Formula (ident, _, phi', _, _)) =
-    if is_same_formula [] phi phi' then SOME ident else NONE
+    if is_same_formula true [] phi phi' then SOME (ident, phi') else NONE
   | matching_formula_line_identifier _ _ = NONE
 
 fun find_formula_in_problem problem phi =
   problem |> maps snd |> map_filter (matching_formula_line_identifier phi)
           |> try (single o hd) |> the_default []
 
+fun commute_eq (AAtom (ATerm (s, tms))) = AAtom (ATerm (s, rev tms))
+  | commute_eq t = raise Fail "expected equation"
+
 (* Syntax: (cnf|fof|tff|thf)\(<num>, <formula_role>,
             <formula> <extra_arguments>\).
    The <num> could be an identifier, but we assume integers. *)
@@ -372,19 +375,27 @@
     --| $$ ")" --| $$ "."
    >> (fn (((num, role), phi), deps) =>
           let
-            val (name, rule, deps) =
+            val ((name, phi), rule, deps) =
               (* Waldmeister isn't exactly helping. *)
               case deps of
                 File_Source (_, SOME s) =>
-                ((num,
-                  if s = waldmeister_conjecture then
-                    find_formula_in_problem problem (mk_anot phi)
-                  else
-                    [s |> perhaps (try (unprefix tofof_fact_prefix))]), "",
-                 [])
+                (if s = waldmeister_conjecture then
+                   case find_formula_in_problem problem (mk_anot phi) of
+                     (* Waldmeister hack: Get the original orientation of the
+                        equation to avoid confusing Isar. *)
+                     [(s, phi')] =>
+                     ((num, [s]),
+                      phi |> not (is_same_formula false [] phi phi')
+                             ? commute_eq)
+                   | _ => ((num, []), phi)
+                 else
+                   ((num, [s |> perhaps (try (unprefix tofof_fact_prefix))]),
+                    phi),
+                 "", [])
               | File_Source _ =>
-                ((num, find_formula_in_problem problem phi), "", [])
-              | Inference_Source (rule, deps) => ((num, []), rule, deps)
+                (((num, phi |> find_formula_in_problem problem |> map fst),
+                  phi), "", [])
+              | Inference_Source (rule, deps) => (((num, []), phi), rule, deps)
             fun mk_step () =
               Inference_Step (name, phi, rule, map (rpair []) deps)
           in
diff -r a5c2386518e2 -r fc26d5538868 src/HOL/Tools/ATP/atp_proof_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Mon May 14 15:54:26 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Mon May 14 15:54:26 2012 +0200
@@ -897,7 +897,7 @@
           |> fold (fn Definition_Step _ => I (* FIXME *)
                     | Inference_Step ((s, _), t, _, _) =>
                       Symtab.update_new (s,
-                          t |> fold_rev forall_of (map Var (Term.add_vars t []))
+                          t |> fold forall_of (map Var (Term.add_vars t []))
                             |> member (op = o apsnd fst) tainted s ? s_not))
                   atp_proof
         fun prop_of_clause c =