1.1 --- a/src/HOL/Tools/ATP/atp_problem.ML	Mon Jun 06 20:36:35 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_problem.ML	Mon Jun 06 20:36:35 2011 +0200
     1.3 @@ -298,8 +298,8 @@
     1.4  fun is_problem_line_negated (Formula (_, _, AConn (ANot, _), _, _)) = true
     1.5    | is_problem_line_negated _ = false
     1.6  
     1.7 -fun is_problem_line_cnf_ueq
     1.8 -        (Formula (_, _, AAtom (ATerm ((s, _), _)), _, _)) = is_tptp_equal s
     1.9 +fun is_problem_line_cnf_ueq (Formula (_, _, AAtom (ATerm ((s, _), _)), _, _)) =
    1.10 +    is_tptp_equal s
    1.11    | is_problem_line_cnf_ueq _ = false
    1.12  
    1.13  fun open_conjecture_term (ATerm ((s, s'), tms)) =
    1.14 @@ -307,8 +307,10 @@
    1.15           else (s, s'), tms |> map open_conjecture_term)
    1.16  fun open_formula conj =
    1.17    let
    1.18 -    fun opn (pos as SOME true) (AQuant (AForall, xs, phi)) = opn pos phi
    1.19 -      | opn (pos as SOME false) (AQuant (AExists, xs, phi)) = opn pos phi
    1.20 +    (* We are conveniently assuming that all bound variable names are
    1.21 +       distinct, which should be the case for the formulas we generate. *)
    1.22 +    fun opn (pos as SOME true) (AQuant (AForall, _, phi)) = opn pos phi
    1.23 +      | opn (pos as SOME false) (AQuant (AExists, _, phi)) = opn pos phi
    1.24        | opn pos (AConn (ANot, [phi])) = mk_anot (opn (Option.map not pos) phi)
    1.25        | opn pos (AConn (c, [phi1, phi2])) =
    1.26          let val (pos1, pos2) = polarities_of_conn pos c in
    1.27 @@ -329,19 +331,20 @@
    1.28  (* This "clausification" only expands syntactic sugar, such as "phi => psi" to
    1.29     "~ phi | psi" and "phi <=> psi" to "~ phi | psi" and "~ psi | phi". We don't
    1.30     attempt to distribute conjunctions over disjunctions. *)
    1.31 -fun clausify_formula1 pos (phi as AAtom _) = phi |> not pos ? mk_anot
    1.32 -  | clausify_formula1 pos (AConn (ANot, [phi])) = clausify_formula1 (not pos) phi
    1.33 -  | clausify_formula1 false (AConn (AAnd, phis)) =
    1.34 -    AConn (AOr, map (clausify_formula1 false) phis)
    1.35 -  | clausify_formula1 true (AConn (AOr, phis)) =
    1.36 -    AConn (AOr, map (clausify_formula1 true) phis)
    1.37 -  | clausify_formula1 true (AConn (AImplies, [phi1, phi2])) =
    1.38 -    AConn (AOr, [clausify_formula1 false phi1, clausify_formula1 true phi2])
    1.39 -  | clausify_formula1 _ _ = raise CLAUSIFY ()
    1.40 -fun clausify_formula true (AConn (AIff, phis)) =
    1.41 -    [clausify_formula1 true (AConn (AImplies, rev phis)),
    1.42 -     clausify_formula1 true (AConn (AImplies, phis))]
    1.43 -  | clausify_formula pos phi = [clausify_formula1 pos phi]
    1.44 +fun clausify_formula pos (phi as AAtom _) = [phi |> not pos ? mk_anot]
    1.45 +  | clausify_formula pos (AConn (ANot, [phi])) = clausify_formula (not pos) phi
    1.46 +  | clausify_formula true (AConn (AOr, [phi1, phi2])) =
    1.47 +    (phi1, phi2) |> pairself (clausify_formula true)
    1.48 +                 |> uncurry (map_product (mk_aconn AOr))
    1.49 +  | clausify_formula false (AConn (AAnd, [phi1, phi2])) =
    1.50 +    (phi1, phi2) |> pairself (clausify_formula false)
    1.51 +                 |> uncurry (map_product (mk_aconn AOr))
    1.52 +  | clausify_formula true (AConn (AImplies, [phi1, phi2])) =
    1.53 +    clausify_formula true (AConn (AOr, [mk_anot phi1, phi2]))
    1.54 +  | clausify_formula true (AConn (AIff, phis)) =
    1.55 +    clausify_formula true (AConn (AImplies, phis)) @
    1.56 +    clausify_formula true (AConn (AImplies, rev phis))
    1.57 +  | clausify_formula _ _ = raise CLAUSIFY ()
    1.58  
    1.59  fun clausify_formula_line (Formula (ident, kind, phi, source, info)) =
    1.60      let

     2.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Mon Jun 06 20:36:35 2011 +0200
     2.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Mon Jun 06 20:36:35 2011 +0200
     2.3 @@ -981,8 +981,8 @@
     2.4                      else I)
     2.5                in
     2.6                  t |> preproc ? (preprocess_prop ctxt true kind #> freeze_term)
     2.7 -                  |> make_formula thy format type_sys true (string_of_int j)
     2.8 -                                  General kind
     2.9 +                  |> make_formula thy format type_sys (format <> CNF)
    2.10 +                                  (string_of_int j) General kind
    2.11                    |> maybe_negate
    2.12                end)
    2.13           (0 upto last) ts

     3.1 --- a/src/HOL/Tools/Metis/metis_translate.ML	Mon Jun 06 20:36:35 2011 +0200
     3.2 +++ b/src/HOL/Tools/Metis/metis_translate.ML	Mon Jun 06 20:36:35 2011 +0200
     3.3 @@ -367,9 +367,15 @@
     3.4                                                          old_skolems
     3.5                              ||> (fn prop => prop :: props))
     3.6               clauses ([], [])
     3.7 +(*
     3.8 +val _ = tracing ("PROPS:\n" ^ cat_lines (map (Syntax.string_of_term ctxt) props))
     3.9 +*)
    3.10        val (atp_problem, _, _, _, _, _, sym_tab) =
    3.11          prepare_atp_problem ctxt CNF Hypothesis Axiom type_sys explicit_apply
    3.12                              false false props @{prop False} []
    3.13 +(*
    3.14 +val _ = tracing ("ATP PROBLEM: " ^ cat_lines (tptp_strings_for_atp_problem CNF atp_problem))
    3.15 +*)
    3.16        val axioms =
    3.17          atp_problem |> maps (map_filter (metis_axiom_from_atp clauses) o snd)
    3.18      in