1.1 --- a/src/HOL/Tools/ATP/atp_problem.ML	Wed Jun 01 10:29:43 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_problem.ML	Wed Jun 01 10:29:43 2011 +0200
     1.3 @@ -330,29 +330,44 @@
     1.4  
     1.5  exception CLAUSIFY of unit
     1.6  
     1.7 -fun clausify_formula pos (phi as AAtom _) = phi |> not pos ? mk_anot
     1.8 -  | clausify_formula pos (AConn (ANot, [phi])) = clausify_formula (not pos) phi
     1.9 -  | clausify_formula false (AConn (AAnd, phis)) =
    1.10 -    AConn (AOr, map (clausify_formula false) phis)
    1.11 -  | clausify_formula true (AConn (AOr, phis)) =
    1.12 -    AConn (AOr, map (clausify_formula true) phis)
    1.13 -  | clausify_formula true (AConn (AImplies, [phi1, phi2])) =
    1.14 -    AConn (AOr, [clausify_formula false phi1, clausify_formula true phi2])
    1.15 -  | clausify_formula true (AConn (AIf, phis)) =
    1.16 -    clausify_formula true (AConn (AImplies, rev phis))
    1.17 -  | clausify_formula _ _ = raise CLAUSIFY ()
    1.18 +(* This "clausification" only expands syntactic sugar, such as "phi => psi" to
    1.19 +   "~ phi | psi" and "phi <=> psi" to "~ phi | psi" and "~ psi | phi". We don't
    1.20 +   attempt to distribute conjunctions over disjunctions. *)
    1.21 +fun clausify_formula1 pos (phi as AAtom _) = phi |> not pos ? mk_anot
    1.22 +  | clausify_formula1 pos (AConn (ANot, [phi])) = clausify_formula1 (not pos) phi
    1.23 +  | clausify_formula1 false (AConn (AAnd, phis)) =
    1.24 +    AConn (AOr, map (clausify_formula1 false) phis)
    1.25 +  | clausify_formula1 true (AConn (AOr, phis)) =
    1.26 +    AConn (AOr, map (clausify_formula1 true) phis)
    1.27 +  | clausify_formula1 true (AConn (AImplies, [phi1, phi2])) =
    1.28 +    AConn (AOr, [clausify_formula1 false phi1, clausify_formula1 true phi2])
    1.29 +  | clausify_formula1 true (AConn (AIf, phis)) =
    1.30 +    clausify_formula1 true (AConn (AImplies, rev phis))
    1.31 +  | clausify_formula1 _ _ = raise CLAUSIFY ()
    1.32 +fun clausify_formula true (AConn (AIff, phis)) =
    1.33 +    [clausify_formula1 true (AConn (AIf, phis)),
    1.34 +     clausify_formula1 true (AConn (AImplies, phis))]
    1.35 +  | clausify_formula false (AConn (ANotIff, phis)) =
    1.36 +    clausify_formula true (AConn (AIff, phis))
    1.37 +  | clausify_formula pos phi = [clausify_formula1 pos phi]
    1.38  
    1.39  fun clausify_formula_line (Formula (ident, kind, phi, source, info)) =
    1.40 -    (case try (clausify_formula true) phi of
    1.41 -       SOME phi => SOME (Formula (ident, kind, phi, source, info))
    1.42 -     | NONE => NONE)
    1.43 -  | clausify_formula_line _ = NONE
    1.44 +    let
    1.45 +      val (n, phis) = phi |> try (clausify_formula true) |> these |> `length
    1.46 +    in
    1.47 +      map2 (fn phi => fn j =>
    1.48 +               Formula (ident ^
    1.49 +                        (if n > 1 then "_cls" ^ string_of_int j else ""),
    1.50 +                        kind, phi, source, info))
    1.51 +           phis (1 upto n)
    1.52 +    end
    1.53 +  | clausify_formula_line _ = []
    1.54  
    1.55  fun ensure_cnf_problem_line line =
    1.56    line |> open_formula_line |> negate_conjecture_line |> clausify_formula_line
    1.57  
    1.58  fun ensure_cnf_problem problem =
    1.59 -  problem |> map (apsnd (map_filter ensure_cnf_problem_line))
    1.60 +  problem |> map (apsnd (maps ensure_cnf_problem_line))
    1.61  
    1.62  fun filter_cnf_ueq_problem problem =
    1.63    problem