# HG changeset patch # User blanchet # Date 1280156601 -7200 # Node ID 06f02b15ef8a04de8f14448ee5acd961b20ed72a # Parent b04307085a093a0b4cd54325fc781ce1acd0bdfe generate full first-order formulas (FOF) in Sledgehammer diff -r b04307085a09 -r 06f02b15ef8a src/HOL/Tools/ATP_Manager/atp_systems.ML --- a/src/HOL/Tools/ATP_Manager/atp_systems.ML Mon Jul 26 14:14:24 2010 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML Mon Jul 26 17:03:21 2010 +0200 @@ -115,13 +115,6 @@ | string_for_failure MalformedOutput = "Error: The ATP output is malformed." | string_for_failure UnknownError = "Error: An unknown ATP error occurred." -fun shape_of_clauses _ [] = [] - | shape_of_clauses j ([] :: clauses) = [] :: shape_of_clauses j clauses - | shape_of_clauses j ((_ :: lits) :: clauses) = - let val shape = shape_of_clauses (j + 1) (lits :: clauses) in - (j :: hd shape) :: tl shape - end - (* Clause preparation *) @@ -133,24 +126,42 @@ fun subtract_cls ax_clauses = filter_out (Termtab.defined (make_clause_table ax_clauses) o prop_of) -(* FIXME: kill *) -fun mk_anot phi = AConn (ANot, [phi]) -fun mk_aconn c phi1 phi2 = AConn (c, [phi1, phi2]) +fun combformula_for_prop thy = + let + val do_term = combterm_from_term thy + fun do_quant bs q s T t' = + do_formula ((s, T) :: bs) t' + #>> (fn phi => AQuant (q, [`make_bound_var s], phi)) + and do_conn bs c t1 t2 = + do_formula bs t1 ##>> do_formula bs t2 + #>> (fn (phi1, phi2) => AConn (c, [phi1, phi2])) + and do_formula bs t = + case t of + @{const Trueprop} $ t1 => do_formula bs t1 + | @{const Not} $ t1 => + do_formula bs t1 #>> (fn phi => AConn (ANot, [phi])) + | Const (@{const_name All}, _) $ Abs (s, T, t') => + do_quant bs AForall s T t' + | Const (@{const_name Ex}, _) $ Abs (s, T, t') => + do_quant bs AExists s T t' + | @{const "op &"} $ t1 $ t2 => do_conn bs AAnd t1 t2 + | @{const "op |"} $ t1 $ t2 => do_conn bs AOr t1 t2 + | @{const "op -->"} $ t1 $ t2 => do_conn bs AImplies t1 t2 + | Const (@{const_name "op ="}, Type (_, [@{typ bool}, _])) $ t1 $ t2 => + do_conn bs AIff t1 t2 + | _ => (fn ts => do_term bs (Envir.eta_contract t) + |>> APred ||> union (op =) ts) + in do_formula [] end (* making axiom and conjecture clauses *) -fun make_clause thy (formula_id, formula_name, kind, th) skolems = +fun make_clause thy (formula_id, formula_name, kind, t) skolems = let - val (skolems, t) = th |> prop_of |> conceal_skolem_terms formula_id skolems - val (lits, ctypes_sorts) = literals_of_term thy t - (* FIXME: avoid "literals_of_term *) - val combformula = - case lits of - [] => APred (CombConst (("c_False", "False"), CombType (("bool", "bool"), []), [])) - | _ => - let val phis = lits |> map (fn FOLLiteral (pos, tm) => APred tm |> not pos ? mk_anot) in - fold (mk_aconn AOr) (tl phis) (hd phis) - |> kind = Conjecture ? mk_anot - end + (* ### FIXME: introduce combinators and perform other transformations + previously done by Clausifier.to_nnf *) + val (skolems, t) = + t |> Object_Logic.atomize_term thy + |> conceal_skolem_terms formula_id skolems + val (combformula, ctypes_sorts) = combformula_for_prop thy t [] in (skolems, FOLFormula {formula_name = formula_name, formula_id = formula_id, @@ -160,7 +171,7 @@ fun add_axiom_clause thy ((name, k), th) (skolems, clss) = let - val (skolems, cls) = make_clause thy (k, name, Axiom, th) skolems + val (skolems, cls) = make_clause thy (k, name, Axiom, prop_of th) skolems in (skolems, (name, cls) :: clss) end fun make_axiom_clauses thy clauses = @@ -169,11 +180,11 @@ fun make_conjecture_clauses thy = let fun aux _ _ [] = [] - | aux n skolems (th :: ths) = + | aux n skolems (t :: ts) = let val (skolems, cls) = - make_clause thy (n, "conjecture", Conjecture, th) skolems - in cls :: aux (n + 1) skolems ths end + make_clause thy (n, "conjecture", Conjecture, t) skolems + in cls :: aux (n + 1) skolems ts end in aux 0 [] end (** Helper clauses **) @@ -220,20 +231,24 @@ @ (if is_FO then [] else cnf_helper_thms thy false mandatory_helpers) in map snd (make_axiom_clauses thy cnfs) end +fun negate_prop (@{const Trueprop} $ t) = negate_prop t + | negate_prop (@{const Not} $ t) = t + | negate_prop t = @{const Not} $ t + (* prepare for passing to writer, create additional clauses based on the information from extra_cls *) -fun prepare_clauses full_types goal_cls axcls extra_cls thy = +fun prepare_clauses full_types hyp_ts concl_t axcls extra_cls thy = let - val is_FO = forall (Meson.is_fol_term thy o prop_of) goal_cls - val ccls = subtract_cls extra_cls goal_cls - val _ = app (fn th => trace_msg (fn _ => Display.string_of_thm_global thy th)) ccls - val ccltms = map prop_of ccls - and axtms = map (prop_of o snd) extra_cls - val subs = tfree_classes_of_terms ccltms - and supers = tvar_classes_of_terms axtms - and tycons = type_consts_of_terms thy (ccltms @ axtms) + val goal_t = Logic.list_implies (hyp_ts, concl_t) + val is_FO = Meson.is_fol_term thy goal_t + val _ = trace_msg (fn _ => Syntax.string_of_term_global thy goal_t) + val axtms = map (prop_of o snd) extra_cls + val subs = tfree_classes_of_terms [goal_t] + val supers = tvar_classes_of_terms axtms + val tycons = type_consts_of_terms thy (goal_t :: axtms) (*TFrees in conjecture clauses; TVars in axiom clauses*) - val conjectures = make_conjecture_clauses thy ccls + val conjectures = + make_conjecture_clauses thy (map negate_prop hyp_ts @ [concl_t]) val (_, extra_clauses) = ListPair.unzip (make_axiom_clauses thy extra_cls) val (clnames, axiom_clauses) = ListPair.unzip (make_axiom_clauses thy axcls) val helper_clauses = @@ -307,20 +322,20 @@ (* get clauses and prepare them for writing *) val (ctxt, (_, th)) = goal; val thy = ProofContext.theory_of ctxt; - val goal_clss = #1 (Clausifier.neg_conjecture_clauses ctxt th subgoal) - val goal_cls = List.concat goal_clss + (* ### FIXME: (1) preprocessing for "if" etc. *) + val (params, hyp_ts, concl_t) = strip_subgoal th subgoal val the_filtered_clauses = case filtered_clauses of SOME fcls => fcls | NONE => relevant_facts full_types relevance_threshold relevance_convergence defs_relevant max_axiom_clauses (the_default prefers_theory_relevant theory_relevant) - relevance_override goal goal_cls + relevance_override goal hyp_ts concl_t |> Clausifier.cnf_rules_pairs thy true val the_axiom_clauses = axiom_clauses |> the_default the_filtered_clauses val (internal_thm_names, clauses) = - prepare_clauses full_types goal_cls the_axiom_clauses the_filtered_clauses - thy + prepare_clauses full_types hyp_ts concl_t the_axiom_clauses + the_filtered_clauses thy (* path to unique problem file *) val the_dest_dir = if overlord then getenv "ISABELLE_HOME_USER" @@ -387,7 +402,9 @@ val (pool, conjecture_offset) = write_tptp_file thy readable_names explicit_forall full_types explicit_apply probfile clauses - val conjecture_shape = shape_of_clauses (conjecture_offset + 1) goal_clss + val conjecture_shape = + conjecture_offset + 1 upto conjecture_offset + length hyp_ts + 1 + |> map single (* ### FIXME: get rid of "map single" *) val result = do_run false |> (fn (_, msecs0, _, SOME _) => @@ -448,8 +465,8 @@ string_of_int (to_generous_secs timeout), proof_delims = [tstp_proof_delims], known_failures = - [(Unprovable, "SZS status: Satisfiable"), - (Unprovable, "SZS status Satisfiable"), + [(Unprovable, "SZS status: CounterSatisfiable"), + (Unprovable, "SZS status CounterSatisfiable"), (TimedOut, "Failure: Resource limit exceeded (time)"), (TimedOut, "time limit exceeded"), (OutOfResources, diff -r b04307085a09 -r 06f02b15ef8a src/HOL/Tools/Sledgehammer/clausifier.ML --- a/src/HOL/Tools/Sledgehammer/clausifier.ML Mon Jul 26 14:14:24 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/clausifier.ML Mon Jul 26 17:03:21 2010 +0200 @@ -11,8 +11,6 @@ val cnf_rules_pairs : theory -> bool -> (string * thm) list -> ((string * int) * thm) list val neg_clausify: thm -> thm list - val neg_conjecture_clauses: - Proof.context -> thm -> int -> thm list list * (string * typ) list end; structure Clausifier : CLAUSIFIER = @@ -222,7 +220,8 @@ |> Thm.varifyT_global end -(*Converts an Isabelle theorem (intro, elim or simp format, even higher-order) into NNF.*) +(* Converts an Isabelle theorem (intro, elim or simp format, even higher-order) + into NNF. *) fun to_nnf th ctxt0 = let val th1 = th |> transform_elim |> zero_var_indexes val ((_, [th2]), ctxt) = Variable.import true [th1] ctxt0 @@ -231,7 +230,7 @@ |> Meson.make_nnf ctxt in (th3, ctxt) end; -(*Skolemize a named theorem, with Skolem functions as additional premises.*) +(* Skolemize a named theorem, with Skolem functions as additional premises. *) fun skolemize_theorem thy cheat th = let val ctxt0 = Variable.global_thm_context th @@ -255,6 +254,7 @@ (**** Translate a set of theorems into CNF ****) (*The combination of rev and tail recursion preserves the original order*) +(* ### FIXME: kill "cheat" *) fun cnf_rules_pairs thy cheat = let fun do_one _ [] = [] @@ -280,13 +280,4 @@ #> map introduce_combinators #> Meson.finish_cnf -fun neg_conjecture_clauses ctxt st0 n = - let - (* "Option" is thrown if the assumptions contain schematic variables. *) - val st = Seq.hd (neg_skolemize_tac ctxt n st0) handle Option.Option => st0 - val ({params, prems, ...}, _) = - Subgoal.focus (Variable.set_body false ctxt) n st - in (map neg_clausify prems, map (dest_Free o term_of o #2) params) end - - end; diff -r b04307085a09 -r 06f02b15ef8a src/HOL/Tools/Sledgehammer/metis_clauses.ML --- a/src/HOL/Tools/Sledgehammer/metis_clauses.ML Mon Jul 26 14:14:24 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/metis_clauses.ML Mon Jul 26 17:03:21 2010 +0200 @@ -34,6 +34,7 @@ literals: fol_literal list, ctypes_sorts: typ list} val type_wrapper_name : string + val bound_var_prefix : string val schematic_var_prefix: string val fixed_var_prefix: string val tvar_prefix: string @@ -46,6 +47,7 @@ val ascii_of: string -> string val undo_ascii_of: string -> string val strip_prefix_and_undo_ascii: string -> string -> string option + val make_bound_var : string -> string val make_schematic_var : string * int -> string val make_fixed_var : string -> string val make_schematic_type_var : string * int -> string @@ -63,6 +65,8 @@ val make_arity_clauses: theory -> string list -> class list -> class list * arity_clause list val combtyp_of : combterm -> combtyp val strip_combterm_comb : combterm -> combterm * combterm list + val combterm_from_term : + theory -> (string * typ) list -> term -> combterm * typ list val literals_of_term : theory -> term -> fol_literal list * typ list val conceal_skolem_terms : int -> (string * term) list -> term -> (string * term) list * term @@ -77,8 +81,9 @@ val type_wrapper_name = "ti" -val schematic_var_prefix = "V_"; -val fixed_var_prefix = "v_"; +val bound_var_prefix = "B_" +val schematic_var_prefix = "V_" +val fixed_var_prefix = "v_" val tvar_prefix = "T_"; val tfree_prefix = "t_"; @@ -177,8 +182,9 @@ fun ascii_of_indexname (v,0) = ascii_of v | ascii_of_indexname (v,i) = ascii_of v ^ "_" ^ Int.toString i; -fun make_schematic_var v = schematic_var_prefix ^ (ascii_of_indexname v); -fun make_fixed_var x = fixed_var_prefix ^ (ascii_of x); +fun make_bound_var x = bound_var_prefix ^ ascii_of x +fun make_schematic_var v = schematic_var_prefix ^ ascii_of_indexname v +fun make_fixed_var x = fixed_var_prefix ^ ascii_of x fun make_schematic_type_var (x,i) = tvar_prefix ^ (ascii_of_indexname (trim_type_var x,i)); @@ -402,8 +408,13 @@ | simp_type_of (TVar (x, _)) = CombTVar (make_schematic_type_var x, string_of_indexname x) -(* convert a Term.term (with combinators) into a combterm, also accummulate sort info *) -fun combterm_of thy (Const (c, T)) = +(* Converts a term (with combinators) into a combterm. Also accummulates sort + infomation. *) +fun combterm_from_term thy bs (P $ Q) = + let val (P', tsP) = combterm_from_term thy bs P + val (Q', tsQ) = combterm_from_term thy bs Q + in (CombApp (P', Q'), union (op =) tsP tsQ) end + | combterm_from_term thy _ (Const (c, T)) = let val (tp, ts) = type_of T val tvar_list = @@ -414,22 +425,25 @@ |> map simp_type_of val c' = CombConst (`make_fixed_const c, tp, tvar_list) in (c',ts) end - | combterm_of _ (Free(v, T)) = + | combterm_from_term _ _ (Free (v, T)) = let val (tp,ts) = type_of T val v' = CombConst (`make_fixed_var v, tp, []) in (v',ts) end - | combterm_of _ (Var(v, T)) = + | combterm_from_term _ _ (Var (v, T)) = let val (tp,ts) = type_of T val v' = CombVar ((make_schematic_var v, string_of_indexname v), tp) in (v',ts) end - | combterm_of thy (P $ Q) = - let val (P', tsP) = combterm_of thy P - val (Q', tsQ) = combterm_of thy Q - in (CombApp (P', Q'), union (op =) tsP tsQ) end - | combterm_of _ (Abs _) = raise Fail "HOL clause: Abs" + | combterm_from_term _ bs (Bound j) = + let + val (s, T) = nth bs j + val (tp, ts) = type_of T + val v' = CombConst (`make_bound_var s, tp, []) + in (v', ts) end + | combterm_from_term _ _ (Abs _) = raise Fail "HOL clause: Abs" fun predicate_of thy ((@{const Not} $ P), pos) = predicate_of thy (P, not pos) - | predicate_of thy (t, pos) = (combterm_of thy (Envir.eta_contract t), pos) + | predicate_of thy (t, pos) = + (combterm_from_term thy [] (Envir.eta_contract t), pos) fun literals_of_term1 args thy (@{const Trueprop} $ P) = literals_of_term1 args thy P diff -r b04307085a09 -r 06f02b15ef8a src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Mon Jul 26 14:14:24 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Mon Jul 26 17:03:21 2010 +0200 @@ -16,7 +16,8 @@ Proof.context -> thm list -> Facts.ref -> string * thm list val relevant_facts : bool -> real -> real -> bool -> int -> bool -> relevance_override - -> Proof.context * (thm list * 'a) -> thm list -> (string * thm) list + -> Proof.context * (thm list * 'a) -> term list -> term + -> (string * thm) list end; structure Sledgehammer_Fact_Filter : SLEDGEHAMMER_FACT_FILTER = @@ -148,9 +149,8 @@ do_term t0 #> do_formula pos t1 (* theory constant *) | _ => do_term t in - Symtab.empty - |> fold (Symtab.update o rpair []) boring_natural_consts - |> fold (do_formula pos) ts + Symtab.empty |> fold (Symtab.update o rpair []) boring_natural_consts + |> fold (do_formula pos) ts end (*Inserts a dummy "constant" referring to the theory name, so that relevance @@ -343,7 +343,7 @@ fun relevance_filter ctxt relevance_threshold relevance_convergence defs_relevant max_new theory_relevant relevance_override - thy axioms goals = + thy axioms goal_ts = if relevance_threshold > 1.0 then [] else if relevance_threshold < 0.0 then @@ -352,7 +352,7 @@ let val const_tab = fold (count_axiom_consts theory_relevant thy) axioms Symtab.empty - val goal_const_tab = get_consts_typs thy (SOME true) goals + val goal_const_tab = get_consts_typs thy (SOME true) goal_ts val relevance_threshold = 0.9 * relevance_threshold (* FIXME *) val _ = trace_msg (fn () => "Initial constants: " ^ @@ -563,12 +563,14 @@ fun relevant_facts full_types relevance_threshold relevance_convergence defs_relevant max_new theory_relevant (relevance_override as {add, del, only}) - (ctxt, (chained_ths, _)) goal_cls = + (ctxt, (chained_ths, _)) hyp_ts concl_t = let val thy = ProofContext.theory_of ctxt val add_thms = maps (ProofContext.get_fact ctxt) add val has_override = not (null add) orelse not (null del) - val is_FO = forall (Meson.is_fol_term thy o prop_of) goal_cls +(*### + val is_FO = forall Meson.is_fol_term thy (concl_t :: hyp_ts) +*) val axioms = checked_name_thm_pairs (respect_no_atp andalso not only) ctxt (map (name_thms_pair_from_ref ctxt chained_ths) add @ @@ -581,7 +583,7 @@ in relevance_filter ctxt relevance_threshold relevance_convergence defs_relevant max_new theory_relevant relevance_override - thy axioms (map prop_of goal_cls) + thy axioms (concl_t :: hyp_ts) |> has_override ? make_unique |> sort_wrt fst end diff -r b04307085a09 -r 06f02b15ef8a src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Mon Jul 26 14:14:24 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Mon Jul 26 17:03:21 2010 +0200 @@ -954,17 +954,12 @@ do_indent 0 ^ (if n <> 1 then "next" else "qed") ^ "\n" in do_proof end -fun strip_subgoal goal i = - let - val (t, frees) = Logic.goal_params (prop_of goal) i - val hyp_ts = t |> Logic.strip_assums_hyp |> map (curry subst_bounds frees) - val concl_t = t |> Logic.strip_assums_concl |> curry subst_bounds frees - in (rev (map dest_Free frees), hyp_ts, concl_t) end - fun isar_proof_text (pool, debug, isar_shrink_factor, ctxt, conjecture_shape) (other_params as (full_types, _, atp_proof, thm_names, goal, i)) = let + (* ### FIXME: avoid duplication with ATP_Systems -- and move strip_subgoal + to ATP_Systems *) val (params, hyp_ts, concl_t) = strip_subgoal goal i val frees = fold Term.add_frees (concl_t :: hyp_ts) [] val tfrees = fold Term.add_tfrees (concl_t :: hyp_ts) [] diff -r b04307085a09 -r 06f02b15ef8a src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML Mon Jul 26 14:14:24 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML Mon Jul 26 17:03:21 2010 +0200 @@ -76,7 +76,7 @@ | string_for_connective AIff = "<=>" | string_for_connective ANotIff = "<~>" fun string_for_formula (AQuant (q, xs, phi)) = - string_for_quantifier q ^ " [" ^ commas xs ^ "] : " ^ + string_for_quantifier q ^ "[" ^ commas xs ^ "]: " ^ string_for_formula phi | string_for_formula (AConn (c, [phi])) = string_for_connective c ^ " " ^ string_for_formula phi diff -r b04307085a09 -r 06f02b15ef8a src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Mon Jul 26 14:14:24 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Mon Jul 26 17:03:21 2010 +0200 @@ -18,6 +18,7 @@ val maybe_quote : string -> string val monomorphic_term : Type.tyenv -> term -> term val specialize_type : theory -> (string * typ) -> term -> term + val strip_subgoal : thm -> int -> (string * typ) list * term list * term end; structure Sledgehammer_Util : SLEDGEHAMMER_UTIL = @@ -126,5 +127,11 @@ | NONE => raise Type.TYPE_MATCH end +fun strip_subgoal goal i = + let + val (t, frees) = Logic.goal_params (prop_of goal) i + val hyp_ts = t |> Logic.strip_assums_hyp |> map (curry subst_bounds frees) + val concl_t = t |> Logic.strip_assums_concl |> curry subst_bounds frees + in (rev (map dest_Free frees), hyp_ts, concl_t) end end;