1.1 --- a/src/HOL/Tools/ATP/atp_problem.ML	Tue May 31 16:38:36 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_problem.ML	Tue May 31 16:38:36 2011 +0200
     1.3 @@ -143,6 +143,17 @@
     1.4  fun is_tptp_variable s = Char.isUpper (String.sub (s, 0))
     1.5  val is_tptp_user_symbol = not o (is_tptp_variable orf is_built_in_tptp_symbol)
     1.6  
     1.7 +fun raw_polarities_of_conn ANot = (SOME false, NONE)
     1.8 +  | raw_polarities_of_conn AAnd = (SOME true, SOME true)
     1.9 +  | raw_polarities_of_conn AOr = (SOME true, SOME true)
    1.10 +  | raw_polarities_of_conn AImplies = (SOME false, SOME true)
    1.11 +  | raw_polarities_of_conn AIf = (SOME true, SOME false)
    1.12 +  | raw_polarities_of_conn AIff = (NONE, NONE)
    1.13 +  | raw_polarities_of_conn ANotIff = (NONE, NONE)
    1.14 +fun polarities_of_conn NONE = K (NONE, NONE)
    1.15 +  | polarities_of_conn (SOME pos) =
    1.16 +    raw_polarities_of_conn #> not pos ? pairself (Option.map not)
    1.17 +
    1.18  fun mk_anot (AConn (ANot, [phi])) = phi
    1.19    | mk_anot phi = AConn (ANot, [phi])
    1.20  fun mk_aconn c phi1 phi2 = AConn (c, [phi1, phi2])
    1.21 @@ -286,7 +297,7 @@
    1.22         problem
    1.23  
    1.24  
    1.25 -(** CNF UEQ (Waldmeister) **)
    1.26 +(** CNF (Metis) and CNF UEQ (Waldmeister) **)
    1.27  
    1.28  fun is_problem_line_negated (Formula (_, _, AConn (ANot, _), _, _)) = true
    1.29    | is_problem_line_negated _ = false
    1.30 @@ -298,9 +309,17 @@
    1.31  fun open_conjecture_term (ATerm ((s, s'), tms)) =
    1.32    ATerm (if is_tptp_variable s then (s |> Name.desymbolize false, s')
    1.33           else (s, s'), tms |> map open_conjecture_term)
    1.34 -fun open_formula conj (AQuant (AForall, _, phi)) = open_formula conj phi
    1.35 -  | open_formula true (AAtom t) = AAtom (open_conjecture_term t)
    1.36 -  | open_formula _ phi = phi
    1.37 +fun open_formula conj =
    1.38 +  let
    1.39 +    fun opn (pos as SOME true) (AQuant (AForall, xs, phi)) = opn pos phi
    1.40 +      | opn (pos as SOME false) (AQuant (AExists, xs, phi)) = opn pos phi
    1.41 +      | opn pos (AConn (ANot, [phi])) = mk_anot (opn (Option.map not pos) phi)
    1.42 +      | opn pos (AConn (c, [phi1, phi2])) =
    1.43 +        let val (pos1, pos2) = polarities_of_conn pos c in
    1.44 +          AConn (c, [opn pos1 phi1, opn pos2 phi2])
    1.45 +        end
    1.46 +      | opn _ (AAtom t) = AAtom (t |> conj ? open_conjecture_term)
    1.47 +  in opn (SOME (not conj)) end
    1.48  fun open_formula_line (Formula (ident, kind, phi, source, info)) =
    1.49      Formula (ident, kind, open_formula (kind = Conjecture) phi, source, info)
    1.50    | open_formula_line line = line
    1.51 @@ -309,7 +328,31 @@
    1.52      Formula (ident, Hypothesis, mk_anot phi, source, info)
    1.53    | negate_conjecture_line line = line
    1.54  
    1.55 -fun ensure_cnf_problem problem = problem |> map (apsnd (map open_formula_line))
    1.56 +exception CLAUSIFY of unit
    1.57 +
    1.58 +fun clausify_formula pos (phi as AAtom _) = phi |> not pos ? mk_anot
    1.59 +  | clausify_formula pos (AConn (ANot, [phi])) = clausify_formula (not pos) phi
    1.60 +  | clausify_formula false (AConn (AAnd, phis)) =
    1.61 +    AConn (AOr, map (clausify_formula false) phis)
    1.62 +  | clausify_formula true (AConn (AOr, phis)) =
    1.63 +    AConn (AOr, map (clausify_formula true) phis)
    1.64 +  | clausify_formula true (AConn (AImplies, [phi1, phi2])) =
    1.65 +    AConn (AOr, [clausify_formula false phi1, clausify_formula true phi2])
    1.66 +  | clausify_formula true (AConn (AIf, phis)) =
    1.67 +    clausify_formula true (AConn (AImplies, rev phis))
    1.68 +  | clausify_formula _ _ = raise CLAUSIFY ()
    1.69 +
    1.70 +fun clausify_formula_line (Formula (ident, kind, phi, source, info)) =
    1.71 +    (case try (clausify_formula true) phi of
    1.72 +       SOME phi => SOME (Formula (ident, kind, phi, source, info))
    1.73 +     | NONE => NONE)
    1.74 +  | clausify_formula_line _ = NONE
    1.75 +
    1.76 +fun ensure_cnf_problem_line line =
    1.77 +  line |> open_formula_line |> negate_conjecture_line |> clausify_formula_line
    1.78 +
    1.79 +fun ensure_cnf_problem problem =
    1.80 +  problem |> map (apsnd (map_filter ensure_cnf_problem_line))
    1.81  
    1.82  fun filter_cnf_ueq_problem problem =
    1.83    problem

     2.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Tue May 31 16:38:36 2011 +0200
     2.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Tue May 31 16:38:36 2011 +0200
     2.3 @@ -618,9 +618,9 @@
     2.4      general_type_arg_policy type_sys
     2.5  
     2.6  (*Make literals for sorted type variables*)
     2.7 -fun sorts_on_typs_aux (_, []) = []
     2.8 -  | sorts_on_typs_aux ((x, i), s :: ss) =
     2.9 -    sorts_on_typs_aux ((x, i), ss)
    2.10 +fun generic_sorts_on_type (_, []) = []
    2.11 +  | generic_sorts_on_type ((x, i), s :: ss) =
    2.12 +    generic_sorts_on_type ((x, i), ss)
    2.13      |> (if s = the_single @{sort HOL.type} then
    2.14            I
    2.15          else if i = ~1 then
    2.16 @@ -628,21 +628,18 @@
    2.17          else
    2.18            cons (TyLitVar (`make_type_class s,
    2.19                            (make_schematic_type_var (x, i), x))))
    2.20 +fun sorts_on_tfree (TFree (s, S)) = generic_sorts_on_type ((s, ~1), S)
    2.21 +  | sorts_on_tfree _ = []
    2.22 +fun sorts_on_tvar (TVar z) = generic_sorts_on_type z
    2.23 +  | sorts_on_tvar _ = []
    2.24  
    2.25 -fun sorts_on_typs (TFree (a, s)) = sorts_on_typs_aux ((a, ~1), s)
    2.26 -  | sorts_on_typs (TVar (v, s)) = sorts_on_typs_aux (v, s)
    2.27 -  | sorts_on_typs _ = raise Fail "expected \"TVar\" or \"TFree\""
    2.28 +(* Given a list of sorted type variables, return a list of type literals. *)
    2.29 +fun raw_type_literals_for_types Ts =
    2.30 +  union_all (map sorts_on_tfree Ts @ map sorts_on_tvar Ts)
    2.31  
    2.32 -(*Given a list of sorted type variables, return a list of type literals.*)
    2.33 -val raw_type_literals_for_types = union_all o map sorts_on_typs
    2.34 -
    2.35 -fun type_literals_for_types format type_sys kind Ts =
    2.36 -  if level_of_type_sys type_sys = No_Types orelse format = CNF_UEQ then
    2.37 -    []
    2.38 -  else
    2.39 -    Ts |> raw_type_literals_for_types
    2.40 -       |> filter (fn TyLitVar _ => kind <> Conjecture
    2.41 -                   | TyLitFree _ => kind = Conjecture)
    2.42 +fun type_literals_for_types type_sys sorts_on_typ Ts =
    2.43 +  if level_of_type_sys type_sys = No_Types then []
    2.44 +  else union_all (map sorts_on_typ Ts)
    2.45  
    2.46  fun mk_aconns c phis =
    2.47    let val (phis', phi') = split_last phis in
    2.48 @@ -893,7 +890,6 @@
    2.49        |> extensionalize_term ctxt
    2.50        |> presimp ? presimplify_term ctxt
    2.51        |> introduce_combinators_in_term ctxt kind
    2.52 -      |> kind <> Axiom ? freeze_term
    2.53    end
    2.54  
    2.55  (* making fact and conjecture formulas *)
    2.56 @@ -933,7 +929,7 @@
    2.57                      if prem_kind = Conjecture then update_combformula mk_anot
    2.58                      else I)
    2.59                in
    2.60 -                t |> preproc ? preprocess_prop ctxt true kind
    2.61 +                t |> preproc ? (preprocess_prop ctxt true kind #> freeze_term)
    2.62                    |> make_formula thy format type_sys true (string_of_int j)
    2.63                                    General kind
    2.64                    |> maybe_negate
    2.65 @@ -1458,9 +1454,9 @@
    2.66        | do_formula _ (AAtom tm) = AAtom (do_term tm)
    2.67    in do_formula o SOME end
    2.68  
    2.69 -fun bound_atomic_types format type_sys Ts =
    2.70 +fun bound_tvars type_sys Ts =
    2.71    mk_ahorn (map (formula_from_fo_literal o fo_literal_from_type_literal)
    2.72 -                (type_literals_for_types format type_sys Axiom Ts))
    2.73 +                (type_literals_for_types type_sys sorts_on_tvar Ts))
    2.74  
    2.75  fun formula_for_fact ctxt format nonmono_Ts type_sys
    2.76                       ({combformula, atomic_types, ...} : translated_formula) =
    2.77 @@ -1468,7 +1464,7 @@
    2.78    |> close_combformula_universally
    2.79    |> formula_from_combformula ctxt format nonmono_Ts type_sys
    2.80                                is_var_nonmonotonic_in_formula true
    2.81 -  |> bound_atomic_types format type_sys atomic_types
    2.82 +  |> bound_tvars type_sys atomic_types
    2.83    |> close_formula_universally
    2.84  
    2.85  (* Each fact is given a unique fact number to avoid name clashes (e.g., because
    2.86 @@ -1510,24 +1506,24 @@
    2.87             |> close_formula_universally, intro_info, NONE)
    2.88  
    2.89  fun formula_line_for_conjecture ctxt format nonmono_Ts type_sys
    2.90 -        ({name, kind, combformula, ...} : translated_formula) =
    2.91 +        ({name, kind, combformula, atomic_types, ...} : translated_formula) =
    2.92    Formula (conjecture_prefix ^ name, kind,
    2.93             formula_from_combformula ctxt format nonmono_Ts type_sys
    2.94                 is_var_nonmonotonic_in_formula false
    2.95                 (close_combformula_universally combformula)
    2.96 +           |> bound_tvars type_sys atomic_types
    2.97             |> close_formula_universally, NONE, NONE)
    2.98  
    2.99 -fun free_type_literals format type_sys
   2.100 -                       ({atomic_types, ...} : translated_formula) =
   2.101 -  atomic_types |> type_literals_for_types format type_sys Conjecture
   2.102 +fun free_type_literals type_sys ({atomic_types, ...} : translated_formula) =
   2.103 +  atomic_types |> type_literals_for_types type_sys sorts_on_tfree
   2.104                 |> map fo_literal_from_type_literal
   2.105  
   2.106  fun formula_line_for_free_type j lit =
   2.107    Formula (tfree_clause_prefix ^ string_of_int j, Hypothesis,
   2.108             formula_from_fo_literal lit, NONE, NONE)
   2.109 -fun formula_lines_for_free_types format type_sys facts =
   2.110 +fun formula_lines_for_free_types type_sys facts =
   2.111    let
   2.112 -    val litss = map (free_type_literals format type_sys) facts
   2.113 +    val litss = map (free_type_literals type_sys) facts
   2.114      val lits = fold (union (op =)) litss []
   2.115    in map2 formula_line_for_free_type (0 upto length lits - 1) lits end
   2.116  
   2.117 @@ -1636,7 +1632,7 @@
   2.118               |> AAtom |> mk_aquant AForall (bound_names ~~ bound_Ts)
   2.119               |> formula_from_combformula ctxt format nonmono_Ts type_sys
   2.120                                           (K (K (K (K true)))) true
   2.121 -             |> n > 1 ? bound_atomic_types format type_sys (atyps_of T)
   2.122 +             |> n > 1 ? bound_tvars type_sys (atyps_of T)
   2.123               |> close_formula_universally
   2.124               |> maybe_negate,
   2.125               intro_info, NONE)
   2.126 @@ -1659,7 +1655,7 @@
   2.127      fun eq tms =
   2.128        (if pred_sym then AConn (AIff, map AAtom tms)
   2.129         else AAtom (ATerm (`I tptp_equal, tms)))
   2.130 -      |> bound_atomic_types format type_sys atomic_Ts
   2.131 +      |> bound_tvars type_sys atomic_Ts
   2.132        |> close_formula_universally
   2.133        |> maybe_negate
   2.134      val should_encode = should_encode_type ctxt nonmono_Ts All_Types
   2.135 @@ -1802,8 +1798,7 @@
   2.136         (conjsN,
   2.137          map (formula_line_for_conjecture ctxt format nonmono_Ts type_sys)
   2.138              conjs),
   2.139 -       (free_typesN,
   2.140 -        formula_lines_for_free_types format type_sys (facts @ conjs))]
   2.141 +       (free_typesN, formula_lines_for_free_types type_sys (facts @ conjs))]
   2.142      val problem =
   2.143        problem
   2.144        |> (case format of

     3.1 --- a/src/HOL/Tools/Metis/metis_translate.ML	Tue May 31 16:38:36 2011 +0200
     3.2 +++ b/src/HOL/Tools/Metis/metis_translate.ML	Tue May 31 16:38:36 2011 +0200
     3.3 @@ -299,11 +299,11 @@
     3.4      uncurry (union (op =)) (pairself metis_literals_from_atp (phi1, phi2))
     3.5    | metis_literals_from_atp phi = [metis_literal_from_atp phi]
     3.6  fun metis_axiom_from_atp clauses (Formula (ident, _, phi, _, _)) =
     3.7 -    let val j = ident |> unprefix conjecture_prefix |> Int.fromString |> the in
     3.8 -      (phi |> metis_literals_from_atp |> Metis_LiteralSet.fromList
     3.9 -           |> Metis_Thm.axiom,
    3.10 -       Meson.make_meta_clause (nth clauses j))
    3.11 -    end
    3.12 +    (phi |> metis_literals_from_atp |> Metis_LiteralSet.fromList
    3.13 +         |> Metis_Thm.axiom,
    3.14 +     case try (unprefix conjecture_prefix) ident of
    3.15 +       SOME s => Meson.make_meta_clause (nth clauses (the (Int.fromString s)))
    3.16 +     | NONE => TrueI)
    3.17    | metis_axiom_from_atp _ _ = raise Fail "not CNF -- expected formula"
    3.18  
    3.19  (* Function to generate metis clauses, including comb and type clauses *)
    3.20 @@ -313,9 +313,8 @@
    3.21        val explicit_apply = NONE
    3.22        val clauses = conj_clauses @ fact_clauses
    3.23        val (atp_problem, _, _, _, _, _, sym_tab) =
    3.24 -        prepare_atp_problem ctxt CNF Hypothesis Axiom type_sys
    3.25 -                            explicit_apply false false (map prop_of clauses)
    3.26 -                            @{prop False} []
    3.27 +        prepare_atp_problem ctxt CNF Hypothesis Axiom type_sys explicit_apply
    3.28 +                            false false (map prop_of clauses) @{prop False} []
    3.29        val axioms =
    3.30          atp_problem
    3.31          |> maps (map_filter (try (metis_axiom_from_atp clauses)) o snd)