--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Jul 27 12:02:10 2010 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Jul 27 14:02:15 2010 +0200
@@ -324,8 +324,7 @@
NONE => (message, SH_OK (time_isa, time_atp, relevant_thm_names))
| SOME _ => (message, SH_FAIL (time_isa, time_atp))
end
- handle ATP_Manager.TRIVIAL () => ("trivial", SH_OK (0, 0, []))
- | ERROR msg => ("error: " ^ msg, SH_ERROR)
+ handle ERROR msg => ("error: " ^ msg, SH_ERROR)
| TimeLimit.TimeOut => ("timeout", SH_ERROR)
fun thms_of_name ctxt name =
--- a/src/HOL/Tools/ATP_Manager/SPASS_TPTP Tue Jul 27 12:02:10 2010 +0100
+++ b/src/HOL/Tools/ATP_Manager/SPASS_TPTP Tue Jul 27 14:02:15 2010 +0200
@@ -14,5 +14,6 @@
> $name.cnf.dfg
rm -f $name.fof.dfg
cat $name.cnf.dfg
-$SPASS_HOME/SPASS $options $name.cnf.dfg
+$SPASS_HOME/SPASS $options $name.cnf.dfg \
+ | sed 's/\(Formulae used in the proof :\).*/\1 N\/A/'
rm -f $name.cnf.dfg
--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Tue Jul 27 12:02:10 2010 +0100
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Tue Jul 27 14:02:15 2010 +0200
@@ -29,8 +29,8 @@
{subgoal: int,
goal: Proof.context * (thm list * thm),
relevance_override: relevance_override,
- axiom_clauses: ((string * int) * thm) list option,
- filtered_clauses: ((string * int) * thm) list option}
+ axiom_clauses: (string * thm) list option,
+ filtered_clauses: (string * thm) list option}
datatype failure =
Unprovable | IncompleteUnprovable | CantConnect | TimedOut |
OutOfResources | OldSpass | MalformedInput | MalformedOutput | UnknownError
@@ -43,11 +43,10 @@
output: string,
proof: string,
internal_thm_names: string Vector.vector,
- conjecture_shape: int list list,
- filtered_clauses: ((string * int) * thm) list}
+ conjecture_shape: int list,
+ filtered_clauses: (string * thm) list}
type prover =
params -> minimize_command -> Time.time -> problem -> prover_result
- exception TRIVIAL of unit
val kill_atps: unit -> unit
val running_atps: unit -> unit
@@ -97,8 +96,8 @@
{subgoal: int,
goal: Proof.context * (thm list * thm),
relevance_override: relevance_override,
- axiom_clauses: ((string * int) * thm) list option,
- filtered_clauses: ((string * int) * thm) list option}
+ axiom_clauses: (string * thm) list option,
+ filtered_clauses: (string * thm) list option}
datatype failure =
Unprovable | IncompleteUnprovable | CantConnect | TimedOut | OutOfResources |
@@ -113,15 +112,12 @@
output: string,
proof: string,
internal_thm_names: string Vector.vector,
- conjecture_shape: int list list,
- filtered_clauses: ((string * int) * thm) list}
+ conjecture_shape: int list,
+ filtered_clauses: (string * thm) list}
type prover =
params -> minimize_command -> Time.time -> problem -> prover_result
-(* Trivial problem, which resolution cannot handle (empty clause) *)
-exception TRIVIAL of unit
-
(* named provers *)
structure Data = Theory_Data
@@ -168,8 +164,7 @@
filtered_clauses = NONE}
in
prover params (minimize_command name) timeout problem |> #message
- handle TRIVIAL () => metis_line full_types i n []
- | ERROR message => "Error: " ^ message ^ "\n"
+ handle ERROR message => "Error: " ^ message ^ "\n"
end)
end
--- a/src/HOL/Tools/ATP_Manager/atp_systems.ML Tue Jul 27 12:02:10 2010 +0100
+++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML Tue Jul 27 14:02:15 2010 +0200
@@ -51,8 +51,9 @@
arguments: bool -> Time.time -> string,
proof_delims: (string * string) list,
known_failures: (failure * string) list,
- max_axiom_clauses: int,
- prefers_theory_relevant: bool};
+ max_new_relevant_facts_per_iter: int,
+ prefers_theory_relevant: bool,
+ explicit_forall: bool}
(* basic template *)
@@ -99,7 +100,7 @@
| string_for_failure OutOfResources = "The ATP ran out of resources."
| string_for_failure OldSpass =
(* FIXME: Change the error message below to point to the Isabelle download
- page once the package is there (around the Isabelle2010 release). *)
+ page once the package is there. *)
"Warning: Sledgehammer requires a more recent version of SPASS with \
\support for the TPTP syntax. To install it, download and untar the \
\package \"http://isabelle.in.tum.de/~blanchet/spass-3.7.tgz\" and add the \
@@ -114,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 *)
@@ -132,105 +126,192 @@
fun subtract_cls ax_clauses =
filter_out (Termtab.defined (make_clause_table ax_clauses) o prop_of)
-fun is_false_literal (FOLLiteral (pos, CombConst ((c, _), _, _))) =
- c = (if pos then "c_False" else "c_True")
- | is_false_literal _ = false
-fun is_true_literal (FOLLiteral (pol, CombConst ((c, _), _, _))) =
- (pol andalso c = "c_True") orelse
- (not pol andalso c = "c_False")
- | is_true_literal _ = false;
-fun is_tautology (FOLClause {literals,...}) = exists is_true_literal literals
+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 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
+
+(* Converts an elim-rule into an equivalent theorem that does not have the
+ predicate variable. Leaves other theorems unchanged. We simply instantiate
+ the conclusion variable to False. (Cf. "transform_elim_term" in
+ "ATP_Systems".) *)
+(* FIXME: test! *)
+fun transform_elim_term t =
+ case Logic.strip_imp_concl t of
+ @{const Trueprop} $ Var (z, @{typ bool}) =>
+ subst_Vars [(z, @{const True})] t
+ | Var (z, @{typ prop}) => subst_Vars [(z, @{prop True})] t
+ | _ => t
+
+(* Removes the lambdas from an equation of the form "t = (%x. u)".
+ (Cf. "extensionalize_theorem" in "Clausifier".) *)
+fun extensionalize_term t =
+ let
+ fun aux j (Const (@{const_name "op ="}, Type (_, [Type (_, [_, T']), _]))
+ $ t2 $ Abs (s, var_T, t')) =
+ let val var_t = Var (("x", j), var_T) in
+ Const (@{const_name "op ="}, T' --> T' --> HOLogic.boolT)
+ $ betapply (t2, var_t) $ subst_bound (var_t, t')
+ |> aux (j + 1)
+ end
+ | aux _ t = t
+ in aux (maxidx_of_term t + 1) t end
+
+(* FIXME: Guarantee freshness *)
+fun concealed_bound_name j = "Sledgehammer" ^ Int.toString j
+fun conceal_bounds Ts t =
+ subst_bounds (map (Free o apfst concealed_bound_name)
+ (length Ts - 1 downto 0 ~~ rev Ts), t)
+fun reveal_bounds Ts =
+ subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j))
+ (0 upto length Ts - 1 ~~ Ts))
+
+fun introduce_combinators_in_term ctxt kind t =
+ let
+ val thy = ProofContext.theory_of ctxt
+ fun aux Ts t =
+ case t of
+ @{const Not} $ t1 => @{const Not} $ aux Ts t1
+ | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>
+ t0 $ Abs (s, T, aux (T :: Ts) t')
+ | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>
+ t0 $ Abs (s, T, aux (T :: Ts) t')
+ | (t0 as @{const "op &"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
+ | (t0 as @{const "op |"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
+ | (t0 as @{const "op -->"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
+ | (t0 as Const (@{const_name "op ="}, Type (_, [@{typ bool}, _])))
+ $ t1 $ t2 =>
+ t0 $ aux Ts t1 $ aux Ts t2
+ | _ => if not (exists_subterm (fn Abs _ => true | _ => false) t) then
+ t
+ else
+ let
+ val t = t |> conceal_bounds Ts
+ |> Envir.eta_contract
+ val ([t], ctxt') = Variable.import_terms true [t] ctxt
+ in
+ t |> cterm_of thy
+ |> Clausifier.introduce_combinators_in_cterm
+ |> singleton (Variable.export ctxt' ctxt)
+ |> prop_of |> Logic.dest_equals |> snd
+ |> reveal_bounds Ts
+ end
+ in t |> not (Meson.is_fol_term thy t) ? aux [] end
+ handle THM _ =>
+ (* A type variable of sort "{}" will make abstraction fail. *)
+ case kind of
+ Axiom => HOLogic.true_const
+ | Conjecture => HOLogic.false_const
(* making axiom and conjecture clauses *)
-fun make_clause thy (clause_id, axiom_name, kind, th) skolems =
+fun make_clause ctxt (formula_name, kind, t) =
let
- val (skolems, t) = th |> prop_of |> conceal_skolem_terms clause_id skolems
- val (lits, ctypes_sorts) = literals_of_term thy t
+ val thy = ProofContext.theory_of ctxt
+ (* ### FIXME: perform other transformations previously done by
+ "Clausifier.to_nnf", e.g. "HOL.If" *)
+ val t = t |> transform_elim_term
+ |> Object_Logic.atomize_term thy
+ |> extensionalize_term
+ |> introduce_combinators_in_term ctxt kind
+ val (combformula, ctypes_sorts) = combformula_for_prop thy t []
in
- if forall is_false_literal lits then
- raise TRIVIAL ()
- else
- (skolems,
- FOLClause {clause_id = clause_id, axiom_name = axiom_name, th = th,
- kind = kind, literals = lits, ctypes_sorts = ctypes_sorts})
+ FOLFormula {formula_name = formula_name, combformula = combformula,
+ kind = kind, ctypes_sorts = ctypes_sorts}
end
-fun add_axiom_clause thy ((name, k), th) (skolems, clss) =
- let
- val (skolems, cls) = make_clause thy (k, name, Axiom, th) skolems
- in (skolems, clss |> not (is_tautology cls) ? cons (name, cls)) end
-
-fun make_axiom_clauses thy clauses =
- ([], []) |> fold_rev (add_axiom_clause thy) clauses |> snd
-
-fun make_conjecture_clauses thy =
- let
- fun aux _ _ [] = []
- | aux n skolems (th :: ths) =
- let
- val (skolems, cls) =
- make_clause thy (n, "conjecture", Conjecture, th) skolems
- in cls :: aux (n + 1) skolems ths end
- in aux 0 [] end
+fun make_axiom_clause ctxt (name, th) =
+ (name, make_clause ctxt (name, Axiom, prop_of th))
+fun make_conjecture_clauses ctxt ts =
+ map2 (fn j => fn t => make_clause ctxt (Int.toString j, Conjecture, t))
+ (0 upto length ts - 1) ts
(** Helper clauses **)
-fun count_combterm (CombConst ((c, _), _, _)) =
- Symtab.map_entry c (Integer.add 1)
+fun count_combterm (CombConst ((s, _), _, _)) =
+ Symtab.map_entry s (Integer.add 1)
| count_combterm (CombVar _) = I
- | count_combterm (CombApp (t1, t2)) = count_combterm t1 #> count_combterm t2
-fun count_literal (FOLLiteral (_, t)) = count_combterm t
-fun count_clause (FOLClause {literals, ...}) = fold count_literal literals
-
-fun cnf_helper_thms thy raw =
- map (`Thm.get_name_hint)
- #> (if raw then map (apfst (rpair 0)) else Clausifier.cnf_rules_pairs thy true)
+ | count_combterm (CombApp (t1, t2)) = fold count_combterm [t1, t2]
+fun count_combformula (AQuant (_, _, phi)) = count_combformula phi
+ | count_combformula (AConn (_, phis)) = fold count_combformula phis
+ | count_combformula (APred tm) = count_combterm tm
+fun count_fol_formula (FOLFormula {combformula, ...}) =
+ count_combformula combformula
val optional_helpers =
- [(["c_COMBI", "c_COMBK"], (false, @{thms COMBI_def COMBK_def})),
- (["c_COMBB", "c_COMBC"], (false, @{thms COMBB_def COMBC_def})),
- (["c_COMBS"], (false, @{thms COMBS_def}))]
+ [(["c_COMBI", "c_COMBK"], @{thms COMBI_def COMBK_def}),
+ (["c_COMBB", "c_COMBC"], @{thms COMBB_def COMBC_def}),
+ (["c_COMBS"], @{thms COMBS_def})]
val optional_typed_helpers =
- [(["c_True", "c_False"], (true, @{thms True_or_False})),
- (["c_If"], (true, @{thms if_True if_False True_or_False}))]
+ [(["c_True", "c_False"], @{thms True_or_False}),
+ (["c_If"], @{thms if_True if_False True_or_False})]
val mandatory_helpers = @{thms fequal_imp_equal equal_imp_fequal}
val init_counters =
Symtab.make (maps (maps (map (rpair 0) o fst))
[optional_helpers, optional_typed_helpers])
-fun get_helper_clauses thy is_FO full_types conjectures axcls =
+fun get_helper_clauses ctxt is_FO full_types conjectures axclauses =
let
- val axclauses = map snd (make_axiom_clauses thy axcls)
- val ct = fold (fold count_clause) [conjectures, axclauses] init_counters
+ val ct = fold (fold count_fol_formula) [conjectures, axclauses]
+ init_counters
fun is_needed c = the (Symtab.lookup ct c) > 0
val cnfs =
(optional_helpers
|> full_types ? append optional_typed_helpers
- |> maps (fn (ss, (raw, ths)) =>
- if exists is_needed ss then cnf_helper_thms thy raw ths
- else []))
- @ (if is_FO then [] else cnf_helper_thms thy false mandatory_helpers)
- in map snd (make_axiom_clauses thy cnfs) end
+ |> maps (fn (ss, ths) =>
+ if exists is_needed ss then map (`Thm.get_name_hint) ths
+ else [])) @
+ (if is_FO then [] else map (`Thm.get_name_hint) mandatory_helpers)
+ in map (snd o make_axiom_clause ctxt) cnfs end
+
+fun s_not (@{const Not} $ t) = t
+ | s_not 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 ctxt full_types hyp_ts concl_t axcls extra_cls =
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)
- (*TFrees in conjecture clauses; TVars in axiom clauses*)
- val conjectures = make_conjecture_clauses thy ccls
- val (_, extra_clauses) = ListPair.unzip (make_axiom_clauses thy extra_cls)
- val (clnames, axiom_clauses) = ListPair.unzip (make_axiom_clauses thy axcls)
+ val thy = ProofContext.theory_of ctxt
+ 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 ctxt 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 =
+ map (s_not o HOLogic.dest_Trueprop) hyp_ts @
+ [HOLogic.dest_Trueprop concl_t]
+ |> make_conjecture_clauses ctxt
+ val extra_clauses = map (snd o make_axiom_clause ctxt) extra_cls
+ val (clnames, axiom_clauses) =
+ ListPair.unzip (map (make_axiom_clause ctxt) axcls)
+ (* FIXME: Should it read "extra_clauses" or "axiom_clauses" in the
+ "get_helper_clauses" call? *)
val helper_clauses =
- get_helper_clauses thy is_FO full_types conjectures extra_cls
+ get_helper_clauses ctxt is_FO full_types conjectures extra_clauses
val (supers', arity_clauses) = make_arity_clauses thy tycons supers
val class_rel_clauses = make_class_rel_clauses thy subs supers'
in
@@ -261,27 +342,38 @@
#> snd #> Substring.string #> strip_spaces #> explode
#> parse_clause_formula_relation #> fst
-fun repair_theorem_names output thm_names =
+fun repair_conjecture_shape_and_theorem_names output conjecture_shape
+ thm_names =
if String.isSubstring set_ClauseFormulaRelationN output then
+ (* This is a hack required for keeping track of axioms after they have been
+ clausified by SPASS's Flotter tool. The "SPASS_TPTP" script is also part
+ of this hack. *)
let
+ val j0 = hd conjecture_shape
val seq = extract_clause_sequence output
val name_map = extract_clause_formula_relation output
+ fun renumber_conjecture j =
+ AList.find (op =) name_map (conjecture_prefix ^ Int.toString (j - j0))
+ |> the_single
+ |> (fn s => find_index (curry (op =) s) seq + 1)
in
- seq |> map (the o AList.lookup (op =) name_map)
- |> map (fn s => case try (unprefix axiom_prefix) s of
- SOME s' => undo_ascii_of s'
- | NONE => "")
- |> Vector.fromList
+ (conjecture_shape |> map renumber_conjecture,
+ seq |> map (the o AList.lookup (op =) name_map)
+ |> map (fn s => case try (unprefix axiom_prefix) s of
+ SOME s' => undo_ascii_of s'
+ | NONE => "")
+ |> Vector.fromList)
end
else
- thm_names
+ (conjecture_shape, thm_names)
(* generic TPTP-based provers *)
fun generic_tptp_prover
(name, {home_var, executable, arguments, proof_delims, known_failures,
- max_axiom_clauses, prefers_theory_relevant})
+ max_new_relevant_facts_per_iter, prefers_theory_relevant,
+ explicit_forall})
({debug, overlord, full_types, explicit_apply, relevance_threshold,
relevance_convergence, theory_relevant, defs_relevant, isar_proof,
isar_shrink_factor, ...} : params)
@@ -291,21 +383,21 @@
let
(* 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
+ val thy = ProofContext.theory_of ctxt
+ (* ### 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
+ relevance_convergence defs_relevant
+ max_new_relevant_facts_per_iter
(the_default prefers_theory_relevant theory_relevant)
- relevance_override goal goal_cls
- |> Clausifier.cnf_rules_pairs thy true
+ relevance_override goal hyp_ts concl_t
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 ctxt full_types hyp_ts concl_t the_axiom_clauses
+ the_filtered_clauses
(* path to unique problem file *)
val the_dest_dir = if overlord then getenv "ISABELLE_HOME_USER"
@@ -370,9 +462,10 @@
in (output, msecs, proof, outcome) end
val readable_names = debug andalso overlord
val (pool, conjecture_offset) =
- write_tptp_file thy readable_names full_types explicit_apply
- probfile clauses
- val conjecture_shape = shape_of_clauses (conjecture_offset + 1) goal_clss
+ write_tptp_file thy readable_names explicit_forall full_types
+ explicit_apply probfile clauses
+ val conjecture_shape =
+ conjecture_offset + 1 upto conjecture_offset + length hyp_ts + 1
val result =
do_run false
|> (fn (_, msecs0, _, SOME _) =>
@@ -396,7 +489,9 @@
val ((pool, conjecture_shape), (output, msecs, proof, outcome)) =
with_path cleanup export run_on (prob_pathname subgoal)
- val internal_thm_names = repair_theorem_names output internal_thm_names
+ val (conjecture_shape, internal_thm_names) =
+ repair_conjecture_shape_and_theorem_names output conjecture_shape
+ internal_thm_names
val (message, relevant_thm_names) =
case outcome of
@@ -431,16 +526,17 @@
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,
"# Cannot determine problem status within resource limit"),
(OutOfResources, "SZS status: ResourceOut"),
(OutOfResources, "SZS status ResourceOut")],
- max_axiom_clauses = 100,
- prefers_theory_relevant = false}
+ max_new_relevant_facts_per_iter = 80 (* FIXME *),
+ prefers_theory_relevant = false,
+ explicit_forall = false}
val e = tptp_prover "e" e_config
@@ -463,8 +559,9 @@
(MalformedInput, "Undefined symbol"),
(MalformedInput, "Free Variable"),
(OldSpass, "tptp2dfg")],
- max_axiom_clauses = 40,
- prefers_theory_relevant = true}
+ max_new_relevant_facts_per_iter = 26 (* FIXME *),
+ prefers_theory_relevant = true,
+ explicit_forall = true}
val spass = tptp_prover "spass" spass_config
(* Vampire *)
@@ -484,8 +581,9 @@
(IncompleteUnprovable, "CANNOT PROVE"),
(Unprovable, "Satisfiability detected"),
(OutOfResources, "Refutation not found")],
- max_axiom_clauses = 60,
- prefers_theory_relevant = false}
+ max_new_relevant_facts_per_iter = 40 (* FIXME *),
+ prefers_theory_relevant = false,
+ explicit_forall = false}
val vampire = tptp_prover "vampire" vampire_config
(* Remote prover invocation via SystemOnTPTP *)
@@ -517,8 +615,9 @@
(MalformedOutput, "Remote script could not extract proof")]
fun remote_config atp_prefix args
- ({proof_delims, known_failures, max_axiom_clauses,
- prefers_theory_relevant, ...} : prover_config) : prover_config =
+ ({proof_delims, known_failures, max_new_relevant_facts_per_iter,
+ prefers_theory_relevant, explicit_forall, ...} : prover_config)
+ : prover_config =
{home_var = "ISABELLE_ATP_MANAGER",
executable = "SystemOnTPTP",
arguments = fn _ => fn timeout =>
@@ -526,8 +625,9 @@
the_system atp_prefix,
proof_delims = insert (op =) tstp_proof_delims proof_delims,
known_failures = remote_known_failures @ known_failures,
- max_axiom_clauses = max_axiom_clauses,
- prefers_theory_relevant = prefers_theory_relevant}
+ max_new_relevant_facts_per_iter = max_new_relevant_facts_per_iter,
+ prefers_theory_relevant = prefers_theory_relevant,
+ explicit_forall = explicit_forall}
fun remote_tptp_prover prover atp_prefix args config =
tptp_prover (remotify (fst prover)) (remote_config atp_prefix args config)
--- a/src/HOL/Tools/Sledgehammer/clausifier.ML Tue Jul 27 12:02:10 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/clausifier.ML Tue Jul 27 14:02:15 2010 +0200
@@ -7,12 +7,11 @@
signature CLAUSIFIER =
sig
+ val introduce_combinators_in_cterm : cterm -> thm
val cnf_axiom: theory -> bool -> thm -> thm list
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 =
@@ -23,16 +22,17 @@
val cfalse = cterm_of @{theory HOL} HOLogic.false_const;
val ctp_false = cterm_of @{theory HOL} (HOLogic.mk_Trueprop HOLogic.false_const);
-(*Converts an elim-rule into an equivalent theorem that does not have the
- predicate variable. Leaves other theorems unchanged. We simply instantiate the
- conclusion variable to False.*)
-fun transform_elim th =
+(* Converts an elim-rule into an equivalent theorem that does not have the
+ predicate variable. Leaves other theorems unchanged. We simply instantiate
+ the conclusion variable to False. (Cf. "transform_elim_term" in
+ "ATP_Systems".) *)
+fun transform_elim_theorem th =
case concl_of th of (*conclusion variable*)
@{const Trueprop} $ (v as Var (_, @{typ bool})) =>
Thm.instantiate ([], [(cterm_of @{theory HOL} v, cfalse)]) th
| v as Var(_, @{typ prop}) =>
Thm.instantiate ([], [(cterm_of @{theory HOL} v, ctp_false)]) th
- | _ => th;
+ | _ => th
(*To enforce single-threading*)
exception Clausify_failure of theory;
@@ -84,11 +84,13 @@
val fun_cong_all = @{thm expand_fun_eq [THEN iffD1]}
-(* Removes the lambdas from an equation of the form t = (%x. u). *)
-fun extensionalize th =
+(* ### FIXME: removes only one lambda? *)
+(* Removes the lambdas from an equation of the form "t = (%x. u)".
+ (Cf. "extensionalize_term" in "ATP_Systems".) *)
+fun extensionalize_theorem th =
case prop_of th of
_ $ (Const (@{const_name "op ="}, Type (_, [Type (@{type_name fun}, _), _]))
- $ _ $ Abs (s, _, _)) => extensionalize (th RS fun_cong_all)
+ $ _ $ Abs (s, _, _)) => extensionalize_theorem (th RS fun_cong_all)
| _ => th
fun is_quasi_lambda_free (Const (@{const_name skolem_id}, _) $ _) = true
@@ -107,8 +109,11 @@
val thy = theory_of_cterm ct
val Abs(x,_,body) = term_of ct
val Type(@{type_name fun}, [xT,bodyT]) = typ_of (ctyp_of_term ct)
- val cxT = ctyp_of thy xT and cbodyT = ctyp_of thy bodyT
- fun makeK() = instantiate' [SOME cxT, SOME cbodyT] [SOME (cterm_of thy body)] @{thm abs_K}
+ val cxT = ctyp_of thy xT
+ val cbodyT = ctyp_of thy bodyT
+ fun makeK () =
+ instantiate' [SOME cxT, SOME cbodyT] [SOME (cterm_of thy body)]
+ @{thm abs_K}
in
case body of
Const _ => makeK()
@@ -145,7 +150,7 @@
end;
(* Traverse a theorem, remplacing lambda-abstractions with combinators. *)
-fun do_introduce_combinators ct =
+fun introduce_combinators_in_cterm ct =
if is_quasi_lambda_free (term_of ct) then
Thm.reflexive ct
else case term_of ct of
@@ -153,23 +158,23 @@
let
val (cv, cta) = Thm.dest_abs NONE ct
val (v, _) = dest_Free (term_of cv)
- val u_th = do_introduce_combinators cta
+ val u_th = introduce_combinators_in_cterm cta
val cu = Thm.rhs_of u_th
val comb_eq = abstract (Thm.cabs cv cu)
in Thm.transitive (Thm.abstract_rule v cv u_th) comb_eq end
| _ $ _ =>
let val (ct1, ct2) = Thm.dest_comb ct in
- Thm.combination (do_introduce_combinators ct1)
- (do_introduce_combinators ct2)
+ Thm.combination (introduce_combinators_in_cterm ct1)
+ (introduce_combinators_in_cterm ct2)
end
-fun introduce_combinators th =
+fun introduce_combinators_in_theorem th =
if is_quasi_lambda_free (prop_of th) then
th
else
let
val th = Drule.eta_contraction_rule th
- val eqth = do_introduce_combinators (cprop_of th)
+ val eqth = introduce_combinators_in_cterm (cprop_of th)
in Thm.equal_elim eqth th end
handle THM (msg, _, _) =>
(warning ("Error in the combinator translation of " ^
@@ -222,16 +227,17 @@
|> 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
+ let val th1 = th |> transform_elim_theorem |> zero_var_indexes
val ((_, [th2]), ctxt) = Variable.import true [th1] ctxt0
val th3 = th2 |> Conv.fconv_rule Object_Logic.atomize
- |> extensionalize
+ |> extensionalize_theorem
|> 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
@@ -240,7 +246,7 @@
(assume_skolem_funs nnfth)
val (cnfs, ctxt) = Meson.make_cnf sko_ths nnfth ctxt
in
- cnfs |> map introduce_combinators
+ cnfs |> map introduce_combinators_in_theorem
|> Variable.export ctxt ctxt0
|> Meson.finish_cnf
|> map Thm.close_derivation
@@ -255,6 +261,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 _ [] = []
@@ -277,16 +284,7 @@
val neg_clausify =
single
#> Meson.make_clauses_unsorted
- #> map introduce_combinators
+ #> map introduce_combinators_in_theorem
#> 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;
--- a/src/HOL/Tools/Sledgehammer/metis_clauses.ML Tue Jul 27 12:02:10 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/metis_clauses.ML Tue Jul 27 14:02:15 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
@@ -45,7 +46,8 @@
val invert_const: string -> string
val ascii_of: string -> string
val undo_ascii_of: string -> string
- val strip_prefix: string -> string -> string option
+ 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
@@ -61,8 +63,10 @@
val type_literals_for_types : typ list -> type_literal list
val make_class_rel_clauses: theory -> class list -> class list -> class_rel_clause list
val make_arity_clauses: theory -> string list -> class list -> class list * arity_clause list
- val type_of_combterm : combterm -> combtyp
+ 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_";
@@ -163,7 +168,7 @@
(* If string s has the prefix s1, return the result of deleting it,
un-ASCII'd. *)
-fun strip_prefix s1 s =
+fun strip_prefix_and_undo_ascii s1 s =
if String.isPrefix s1 s then
SOME (undo_ascii_of (String.extract (s, size s1, NONE)))
else
@@ -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));
@@ -373,9 +379,9 @@
fun result_type (CombType (_, [_, tp2])) = tp2
| result_type _ = raise Fail "non-function type"
-fun type_of_combterm (CombConst (_, tp, _)) = tp
- | type_of_combterm (CombVar (_, tp)) = tp
- | type_of_combterm (CombApp (t1, _)) = result_type (type_of_combterm t1)
+fun combtyp_of (CombConst (_, tp, _)) = tp
+ | combtyp_of (CombVar (_, tp)) = tp
+ | combtyp_of (CombApp (t1, _)) = result_type (combtyp_of t1)
(*gets the head of a combinator application, along with the list of arguments*)
fun strip_combterm_comb u =
@@ -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
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Tue Jul 27 12:02:10 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Tue Jul 27 14:02:15 2010 +0200
@@ -100,7 +100,7 @@
wrap_type (Metis.Term.Fn(fn_isa_to_met a, []), ty)
| hol_term_to_fol_FT (tm as CombApp(tm1,tm2)) =
wrap_type (Metis.Term.Fn(".", map hol_term_to_fol_FT [tm1,tm2]),
- type_of_combterm tm);
+ combtyp_of tm)
fun hol_literal_to_fol FO (FOLLiteral (pos, tm)) =
let val (CombConst((p, _), _, tys), tms) = strip_combterm_comb tm
@@ -223,15 +223,15 @@
fun make_tvar s = TVar (("'" ^ s, 0), HOLogic.typeS)
fun hol_type_from_metis_term _ (Metis.Term.Var v) =
- (case strip_prefix tvar_prefix v of
+ (case strip_prefix_and_undo_ascii tvar_prefix v of
SOME w => make_tvar w
| NONE => make_tvar v)
| hol_type_from_metis_term ctxt (Metis.Term.Fn(x, tys)) =
- (case strip_prefix type_const_prefix x of
+ (case strip_prefix_and_undo_ascii type_const_prefix x of
SOME tc => Term.Type (invert_const tc,
map (hol_type_from_metis_term ctxt) tys)
| NONE =>
- case strip_prefix tfree_prefix x of
+ case strip_prefix_and_undo_ascii tfree_prefix x of
SOME tf => mk_tfree ctxt tf
| NONE => raise Fail ("hol_type_from_metis_term: " ^ x));
@@ -241,10 +241,10 @@
val _ = trace_msg (fn () => "hol_term_from_metis_PT: " ^
Metis.Term.toString fol_tm)
fun tm_to_tt (Metis.Term.Var v) =
- (case strip_prefix tvar_prefix v of
+ (case strip_prefix_and_undo_ascii tvar_prefix v of
SOME w => Type (make_tvar w)
| NONE =>
- case strip_prefix schematic_var_prefix v of
+ case strip_prefix_and_undo_ascii schematic_var_prefix v of
SOME w => Term (mk_var (w, HOLogic.typeT))
| NONE => Term (mk_var (v, HOLogic.typeT)) )
(*Var from Metis with a name like _nnn; possibly a type variable*)
@@ -261,7 +261,7 @@
and applic_to_tt ("=",ts) =
Term (list_comb(Const (@{const_name "op ="}, HOLogic.typeT), terms_of (map tm_to_tt ts)))
| applic_to_tt (a,ts) =
- case strip_prefix const_prefix a of
+ case strip_prefix_and_undo_ascii const_prefix a of
SOME b =>
let val c = invert_const b
val ntypes = num_type_args thy c
@@ -279,14 +279,14 @@
cat_lines (map (Syntax.string_of_term ctxt) (terms_of tts)))
end
| NONE => (*Not a constant. Is it a type constructor?*)
- case strip_prefix type_const_prefix a of
+ case strip_prefix_and_undo_ascii type_const_prefix a of
SOME b =>
Type (Term.Type (invert_const b, types_of (map tm_to_tt ts)))
| NONE => (*Maybe a TFree. Should then check that ts=[].*)
- case strip_prefix tfree_prefix a of
+ case strip_prefix_and_undo_ascii tfree_prefix a of
SOME b => Type (mk_tfree ctxt b)
| NONE => (*a fixed variable? They are Skolem functions.*)
- case strip_prefix fixed_var_prefix a of
+ case strip_prefix_and_undo_ascii fixed_var_prefix a of
SOME b =>
let val opr = Term.Free(b, HOLogic.typeT)
in apply_list opr (length ts) (map tm_to_tt ts) end
@@ -302,16 +302,16 @@
let val _ = trace_msg (fn () => "hol_term_from_metis_FT: " ^
Metis.Term.toString fol_tm)
fun cvt (Metis.Term.Fn ("ti", [Metis.Term.Var v, _])) =
- (case strip_prefix schematic_var_prefix v of
+ (case strip_prefix_and_undo_ascii schematic_var_prefix v of
SOME w => mk_var(w, dummyT)
| NONE => mk_var(v, dummyT))
| cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn ("=",[]), _])) =
Const ("op =", HOLogic.typeT)
| cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (x,[]), ty])) =
- (case strip_prefix const_prefix x of
+ (case strip_prefix_and_undo_ascii const_prefix x of
SOME c => Const (invert_const c, dummyT)
| NONE => (*Not a constant. Is it a fixed variable??*)
- case strip_prefix fixed_var_prefix x of
+ case strip_prefix_and_undo_ascii fixed_var_prefix x of
SOME v => Free (v, hol_type_from_metis_term ctxt ty)
| NONE => raise Fail ("hol_term_from_metis_FT bad constant: " ^ x))
| cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (".",[tm1,tm2]), _])) =
@@ -322,10 +322,10 @@
| cvt (Metis.Term.Fn ("=", [tm1,tm2])) =
list_comb(Const (@{const_name "op ="}, HOLogic.typeT), map cvt [tm1,tm2])
| cvt (t as Metis.Term.Fn (x, [])) =
- (case strip_prefix const_prefix x of
+ (case strip_prefix_and_undo_ascii const_prefix x of
SOME c => Const (invert_const c, dummyT)
| NONE => (*Not a constant. Is it a fixed variable??*)
- case strip_prefix fixed_var_prefix x of
+ case strip_prefix_and_undo_ascii fixed_var_prefix x of
SOME v => Free (v, dummyT)
| NONE => (trace_msg (fn () => "hol_term_from_metis_FT bad const: " ^ x);
hol_term_from_metis_PT ctxt t))
@@ -405,9 +405,9 @@
" in " ^ Display.string_of_thm ctxt i_th);
NONE)
fun remove_typeinst (a, t) =
- case strip_prefix schematic_var_prefix a of
+ case strip_prefix_and_undo_ascii schematic_var_prefix a of
SOME b => SOME (b, t)
- | NONE => case strip_prefix tvar_prefix a of
+ | NONE => case strip_prefix_and_undo_ascii tvar_prefix a of
SOME _ => NONE (*type instantiations are forbidden!*)
| NONE => SOME (a,t) (*internal Metis var?*)
val _ = trace_msg (fn () => " isa th: " ^ Display.string_of_thm ctxt i_th)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Tue Jul 27 12:02:10 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Tue Jul 27 14:02:15 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
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Tue Jul 27 12:02:10 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Tue Jul 27 14:02:15 2010 +0200
@@ -55,13 +55,12 @@
val _ = priority ("Testing " ^ string_of_int num_theorems ^
" theorem" ^ plural_s num_theorems ^ "...")
val name_thm_pairs = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs
- val axclauses = Clausifier.cnf_rules_pairs thy true name_thm_pairs
val {context = ctxt, facts, goal} = Proof.goal state
val problem =
{subgoal = subgoal, goal = (ctxt, (facts, goal)),
relevance_override = {add = [], del = [], only = false},
- axiom_clauses = SOME axclauses,
- filtered_clauses = SOME (the_default axclauses filtered_clauses)}
+ axiom_clauses = SOME name_thm_pairs,
+ filtered_clauses = SOME (the_default name_thm_pairs filtered_clauses)}
in
prover params (K "") timeout problem
|> tap (fn result : prover_result =>
@@ -126,8 +125,7 @@
\option (e.g., \"timeout = " ^
string_of_int (10 + msecs div 1000) ^ " s\").")
| {message, ...} => (NONE, "ATP error: " ^ message))
- handle TRIVIAL () => (SOME [], metis_line full_types i n [])
- | ERROR msg => (NONE, "Error: " ^ msg)
+ handle ERROR msg => (NONE, "Error: " ^ msg)
end
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Tue Jul 27 12:02:10 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Tue Jul 27 14:02:15 2010 +0200
@@ -14,11 +14,11 @@
bool * minimize_command * string * string vector * thm * int
-> string * string list
val isar_proof_text:
- string Symtab.table * bool * int * Proof.context * int list list
+ string Symtab.table * bool * int * Proof.context * int list
-> bool * minimize_command * string * string vector * thm * int
-> string * string list
val proof_text:
- bool -> string Symtab.table * bool * int * Proof.context * int list list
+ bool -> string Symtab.table * bool * int * Proof.context * int list
-> bool * minimize_command * string * string vector * thm * int
-> string * string list
end;
@@ -33,22 +33,28 @@
type minimize_command = string list -> string
-val index_in_shape : int -> int list list -> int =
- find_index o exists o curry (op =)
+fun mk_anot phi = AConn (ANot, [phi])
+fun mk_aconn c (phi1, phi2) = AConn (c, [phi1, phi2])
+
+val index_in_shape : int -> int list -> int = find_index o curry (op =)
fun is_axiom_clause_number thm_names num =
num > 0 andalso num <= Vector.length thm_names andalso
Vector.sub (thm_names, num - 1) <> ""
fun is_conjecture_clause_number conjecture_shape num =
index_in_shape num conjecture_shape >= 0
-fun smart_lambda v t =
- Abs (case v of
- Const (s, _) =>
- List.last (space_explode skolem_infix (Long_Name.base_name s))
- | Var ((s, _), _) => s
- | Free (s, _) => s
- | _ => "", fastype_of v, abstract_over (v, t))
-fun forall_of v t = HOLogic.all_const (fastype_of v) $ smart_lambda v t
+fun negate_term (Const (@{const_name All}, T) $ Abs (s, T', t')) =
+ Const (@{const_name Ex}, T) $ Abs (s, T', negate_term t')
+ | negate_term (Const (@{const_name Ex}, T) $ Abs (s, T', t')) =
+ Const (@{const_name All}, T) $ Abs (s, T', negate_term t')
+ | negate_term (@{const "op -->"} $ t1 $ t2) =
+ @{const "op &"} $ t1 $ negate_term t2
+ | negate_term (@{const "op &"} $ t1 $ t2) =
+ @{const "op |"} $ negate_term t1 $ negate_term t2
+ | negate_term (@{const "op |"} $ t1 $ t2) =
+ @{const "op &"} $ negate_term t1 $ negate_term t2
+ | negate_term (@{const Not} $ t) = t
+ | negate_term t = @{const Not} $ t
datatype ('a, 'b, 'c, 'd, 'e) raw_step =
Definition of 'a * 'b * 'c |
@@ -56,86 +62,92 @@
(**** PARSING OF TSTP FORMAT ****)
-(* Syntax trees, either term list or formulae *)
-datatype node = IntLeaf of int | StrNode of string * node list
-
-fun str_leaf s = StrNode (s, [])
-
-fun scons (x, y) = StrNode ("cons", [x, y])
-val slist_of = List.foldl scons (str_leaf "nil")
+datatype int_or_string = Str of string | Int of int
(*Strings enclosed in single quotes, e.g. filenames*)
-val parse_quoted = $$ "'" |-- Scan.repeat (~$$ "'") --| $$ "'" >> implode;
+val scan_quoted = $$ "'" |-- Scan.repeat (~$$ "'") --| $$ "'" >> implode;
-val parse_dollar_name =
+val scan_dollar_name =
Scan.repeat ($$ "$") -- Symbol.scan_id >> (fn (ss, s) => implode ss ^ s)
(* needed for SPASS's output format *)
fun repair_name _ "$true" = "c_True"
| repair_name _ "$false" = "c_False"
- | repair_name _ "$$e" = "c_equal" (* seen in Vampire 11 proofs *)
+ | repair_name _ "$$e" = "c_equal" (* seen in Vampire proofs *)
| repair_name _ "equal" = "c_equal" (* probably not needed *)
| repair_name pool s = Symtab.lookup pool s |> the_default s
(* Generalized first-order terms, which include file names, numbers, etc. *)
(* The "x" argument is not strictly necessary, but without it Poly/ML loops
forever at compile time. *)
+fun parse_generalized_term x =
+ (scan_quoted >> (fn s => ATerm (Str s, []))
+ || scan_dollar_name
+ -- Scan.optional ($$ "(" |-- parse_generalized_terms --| $$ ")") []
+ >> (fn (s, gs) => ATerm (Str s, gs))
+ || scan_integer >> (fn k => ATerm (Int k, []))
+ || $$ "(" |-- parse_generalized_term --| $$ ")"
+ || $$ "[" |-- Scan.optional parse_generalized_terms [] --| $$ "]"
+ >> curry ATerm (Str "list")) x
+and parse_generalized_terms x =
+ (parse_generalized_term ::: Scan.repeat ($$ "," |-- parse_generalized_term)) x
fun parse_term pool x =
- (parse_quoted >> str_leaf
- || scan_integer >> IntLeaf
- || (parse_dollar_name >> repair_name pool)
- -- Scan.optional ($$ "(" |-- parse_terms pool --| $$ ")") [] >> StrNode
- || $$ "(" |-- parse_term pool --| $$ ")"
- || $$ "[" |-- Scan.optional (parse_terms pool) [] --| $$ "]" >> slist_of) x
+ ((scan_dollar_name >> repair_name pool)
+ -- Scan.optional ($$ "(" |-- parse_terms pool --| $$ ")") [] >> ATerm) x
and parse_terms pool x =
(parse_term pool ::: Scan.repeat ($$ "," |-- parse_term pool)) x
-fun negate_node u = StrNode ("c_Not", [u])
-fun equate_nodes u1 u2 = StrNode ("c_equal", [u1, u2])
-
-(* Apply equal or not-equal to a term. *)
-fun repair_predicate_term (u, NONE) = u
- | repair_predicate_term (u1, SOME (NONE, u2)) = equate_nodes u1 u2
- | repair_predicate_term (u1, SOME (SOME _, u2)) =
- negate_node (equate_nodes u1 u2)
fun parse_predicate_term pool =
parse_term pool -- Scan.option (Scan.option ($$ "!") --| $$ "="
-- parse_term pool)
- >> repair_predicate_term
-fun parse_literal pool x =
- ($$ "~" |-- parse_literal pool >> negate_node || parse_predicate_term pool) x
-fun parse_literals pool =
- parse_literal pool ::: Scan.repeat ($$ "|" |-- parse_literal pool)
-fun parse_parenthesized_literals pool =
- $$ "(" |-- parse_literals pool --| $$ ")" || parse_literals pool
-fun parse_clause pool =
- parse_parenthesized_literals pool
- ::: Scan.repeat ($$ "|" |-- parse_parenthesized_literals pool)
- >> List.concat
+ >> (fn (u, NONE) => APred u
+ | (u1, SOME (NONE, u2)) => APred (ATerm ("c_equal", [u1, u2]))
+ | (u1, SOME (SOME _, u2)) =>
+ mk_anot (APred (ATerm ("c_equal", [u1, u2]))))
+
+fun fo_term_head (ATerm (s, _)) = s
-fun ints_of_node (IntLeaf n) = cons n
- | ints_of_node (StrNode (_, us)) = fold ints_of_node us
+(* TPTP formulas are fully parenthesized, so we don't need to worry about
+ operator precedence. *)
+fun parse_formula pool x =
+ (($$ "(" |-- parse_formula pool --| $$ ")"
+ || ($$ "!" >> K AForall || $$ "?" >> K AExists)
+ --| $$ "[" -- parse_terms pool --| $$ "]" --| $$ ":"
+ -- parse_formula pool
+ >> (fn ((q, ts), phi) => AQuant (q, map fo_term_head ts, phi))
+ || $$ "~" |-- parse_formula pool >> mk_anot
+ || parse_predicate_term pool)
+ -- Scan.option ((Scan.this_string "=>" >> K AImplies
+ || Scan.this_string "<=>" >> K AIff
+ || Scan.this_string "<~>" >> K ANotIff
+ || Scan.this_string "<=" >> K AIf
+ || $$ "|" >> K AOr || $$ "&" >> K AAnd)
+ -- parse_formula pool)
+ >> (fn (phi1, NONE) => phi1
+ | (phi1, SOME (c, phi2)) => mk_aconn c (phi1, phi2))) x
+
+fun ints_of_generalized_term (ATerm (label, gs)) =
+ fold ints_of_generalized_term gs #> (case label of Int k => cons k | _ => I)
val parse_tstp_annotations =
- Scan.optional ($$ "," |-- parse_term Symtab.empty
- --| Scan.option ($$ "," |-- parse_terms Symtab.empty)
- >> (fn source => ints_of_node source [])) []
+ Scan.optional ($$ "," |-- parse_generalized_term
+ --| Scan.option ($$ "," |-- parse_generalized_terms)
+ >> (fn g => ints_of_generalized_term g [])) []
-fun parse_definition pool =
- $$ "(" |-- parse_literal pool --| Scan.this_string "<=>"
- -- parse_clause pool --| $$ ")"
-
-(* Syntax: cnf(<num>, <formula_role>, <cnf_formula> <annotations>).
+(* Syntax: (fof|cnf)\(<num>, <formula_role>, <cnf_formula> <annotations>\).
The <num> could be an identifier, but we assume integers. *)
-fun finish_tstp_definition_line (num, (u, us)) = Definition (num, u, us)
-fun finish_tstp_inference_line ((num, us), deps) = Inference (num, us, deps)
-fun parse_tstp_line pool =
- ((Scan.this_string "fof" -- $$ "(") |-- scan_integer --| $$ ","
- --| Scan.this_string "definition" --| $$ "," -- parse_definition pool
- --| parse_tstp_annotations --| $$ ")" --| $$ "."
- >> finish_tstp_definition_line)
- || ((Scan.this_string "cnf" -- $$ "(") |-- scan_integer --| $$ ","
- --| Symbol.scan_id --| $$ "," -- parse_clause pool
- -- parse_tstp_annotations --| $$ ")" --| $$ "."
- >> finish_tstp_inference_line)
+ fun parse_tstp_line pool =
+ ((Scan.this_string "fof" || Scan.this_string "cnf") -- $$ "(")
+ |-- scan_integer --| $$ "," -- Symbol.scan_id --| $$ ","
+ -- parse_formula pool -- parse_tstp_annotations --| $$ ")" --| $$ "."
+ >> (fn (((num, role), phi), deps) =>
+ case role of
+ "definition" =>
+ (case phi of
+ AConn (AIff, [phi1 as APred _, phi2]) =>
+ Definition (num, phi1, phi2)
+ | APred (ATerm ("$$e", _)) =>
+ Inference (num, phi, deps) (* Vampire's equality proxy axiom *)
+ | _ => raise Fail "malformed definition")
+ | _ => Inference (num, phi, deps))
(**** PARSING OF SPASS OUTPUT ****)
@@ -152,21 +164,25 @@
fun parse_decorated_predicate_term pool =
parse_predicate_term pool --| Scan.repeat ($$ "*" || $$ "+" || $$ " ")
+fun mk_horn ([], []) = APred (ATerm ("c_False", []))
+ | mk_horn ([], pos_lits) = foldr1 (mk_aconn AOr) pos_lits
+ | mk_horn (neg_lits, []) = mk_anot (foldr1 (mk_aconn AAnd) neg_lits)
+ | mk_horn (neg_lits, pos_lits) =
+ mk_aconn AImplies (foldr1 (mk_aconn AAnd) neg_lits,
+ foldr1 (mk_aconn AOr) pos_lits)
+
fun parse_horn_clause pool =
Scan.repeat (parse_decorated_predicate_term pool) --| $$ "|" --| $$ "|"
-- Scan.repeat (parse_decorated_predicate_term pool) --| $$ "-" --| $$ ">"
-- Scan.repeat (parse_decorated_predicate_term pool)
- >> (fn (([], []), []) => [str_leaf "c_False"]
- | ((clauses1, clauses2), clauses3) =>
- map negate_node (clauses1 @ clauses2) @ clauses3)
+ >> (mk_horn o apfst (op @))
(* Syntax: <num>[0:<inference><annotations>]
<cnf_formulas> || <cnf_formulas> -> <cnf_formulas>. *)
-fun finish_spass_line ((num, deps), us) = Inference (num, us, deps)
fun parse_spass_line pool =
scan_integer --| $$ "[" --| $$ "0" --| $$ ":" --| Symbol.scan_id
-- parse_spass_annotations --| $$ "]" -- parse_horn_clause pool --| $$ "."
- >> finish_spass_line
+ >> (fn ((num, deps), u) => Inference (num, u, deps))
fun parse_line pool = parse_tstp_line pool || parse_spass_line pool
fun parse_lines pool = Scan.repeat1 (parse_line pool)
@@ -178,30 +194,31 @@
(**** INTERPRETATION OF TSTP SYNTAX TREES ****)
-exception NODE of node list
+exception FO_TERM of string fo_term list
+exception FORMULA of (string, string fo_term) formula list
+exception SAME of unit
(* Type variables are given the basic sort "HOL.type". Some will later be
- constrained by information from type literals, or by type inference. *)
-fun type_from_node _ (u as IntLeaf _) = raise NODE [u]
- | type_from_node tfrees (u as StrNode (a, us)) =
- let val Ts = map (type_from_node tfrees) us in
- case strip_prefix type_const_prefix a of
- SOME b => Type (invert_const b, Ts)
+ constrained by information from type literals, or by type inference. *)
+fun type_from_fo_term tfrees (u as ATerm (a, us)) =
+ let val Ts = map (type_from_fo_term tfrees) us in
+ case strip_prefix_and_undo_ascii type_const_prefix a of
+ SOME b => Type (invert_const b, Ts)
+ | NONE =>
+ if not (null us) then
+ raise FO_TERM [u] (* only "tconst"s have type arguments *)
+ else case strip_prefix_and_undo_ascii tfree_prefix a of
+ SOME b =>
+ let val s = "'" ^ b in
+ TFree (s, AList.lookup (op =) tfrees s |> the_default HOLogic.typeS)
+ end
| NONE =>
- if not (null us) then
- raise NODE [u] (* only "tconst"s have type arguments *)
- else case strip_prefix tfree_prefix a of
- SOME b =>
- let val s = "'" ^ b in
- TFree (s, AList.lookup (op =) tfrees s |> the_default HOLogic.typeS)
- end
+ case strip_prefix_and_undo_ascii tvar_prefix a of
+ SOME b => TVar (("'" ^ b, 0), HOLogic.typeS)
| NONE =>
- case strip_prefix tvar_prefix a of
- SOME b => TVar (("'" ^ b, 0), HOLogic.typeS)
- | NONE =>
- (* Variable from the ATP, say "X1" *)
- Type_Infer.param 0 (a, HOLogic.typeS)
- end
+ (* Variable from the ATP, say "X1" *)
+ Type_Infer.param 0 (a, HOLogic.typeS)
+ end
fun fix_atp_variable_name s =
let
@@ -222,21 +239,19 @@
(* First-order translation. No types are known for variables. "HOLogic.typeT"
should allow them to be inferred.*)
-fun term_from_node thy full_types tfrees =
+fun term_from_fo_term thy full_types tfrees opt_T =
let
fun aux opt_T extra_us u =
case u of
- IntLeaf _ => raise NODE [u]
- | StrNode ("hBOOL", [u1]) => aux (SOME @{typ bool}) [] u1
- | StrNode ("hAPP", [u1, u2]) => aux opt_T (u2 :: extra_us) u1
- | StrNode ("c_Not", [u1]) => @{const Not} $ aux (SOME @{typ bool}) [] u1
- | StrNode (a, us) =>
+ ATerm ("hBOOL", [u1]) => aux (SOME @{typ bool}) [] u1
+ | ATerm ("hAPP", [u1, u2]) => aux opt_T (u2 :: extra_us) u1
+ | ATerm (a, us) =>
if a = type_wrapper_name then
case us of
[typ_u, term_u] =>
- aux (SOME (type_from_node tfrees typ_u)) extra_us term_u
- | _ => raise NODE us
- else case strip_prefix const_prefix a of
+ aux (SOME (type_from_fo_term tfrees typ_u)) extra_us term_u
+ | _ => raise FO_TERM us
+ else case strip_prefix_and_undo_ascii const_prefix a of
SOME "equal" =>
list_comb (Const (@{const_name "op ="}, HOLogic.typeT),
map (aux NONE []) us)
@@ -260,39 +275,35 @@
else
raise Fail ("no type information for " ^ quote c)
else
- if String.isPrefix skolem_theory_name c then
- map fastype_of term_ts ---> HOLogic.typeT
- else
- Sign.const_instance thy (c,
- map (type_from_node tfrees) type_us))
+ Sign.const_instance thy (c,
+ map (type_from_fo_term tfrees) type_us))
in list_comb (t, term_ts @ extra_ts) end
| NONE => (* a free or schematic variable *)
let
val ts = map (aux NONE []) (us @ extra_us)
val T = map fastype_of ts ---> HOLogic.typeT
val t =
- case strip_prefix fixed_var_prefix a of
+ case strip_prefix_and_undo_ascii fixed_var_prefix a of
SOME b => Free (b, T)
| NONE =>
- case strip_prefix schematic_var_prefix a of
+ case strip_prefix_and_undo_ascii schematic_var_prefix a of
SOME b => Var ((b, 0), T)
| NONE =>
(* Variable from the ATP, say "X1" *)
Var ((fix_atp_variable_name a, 0), T)
in list_comb (t, ts) end
- in aux end
+ in aux opt_T [] end
(* Type class literal applied to a type. Returns triple of polarity, class,
type. *)
-fun type_constraint_from_node pos tfrees (StrNode ("c_Not", [u])) =
- type_constraint_from_node (not pos) tfrees u
- | type_constraint_from_node pos tfrees u = case u of
- IntLeaf _ => raise NODE [u]
- | StrNode (a, us) =>
- (case (strip_prefix class_prefix a,
- map (type_from_node tfrees) us) of
- (SOME b, [T]) => (pos, b, T)
- | _ => raise NODE [u])
+fun type_constraint_from_formula pos tfrees (AConn (ANot, [u])) =
+ type_constraint_from_formula (not pos) tfrees u
+ | type_constraint_from_formula pos tfrees (phi as APred (ATerm (a, us))) =
+ (case (strip_prefix_and_undo_ascii class_prefix a,
+ map (type_from_fo_term tfrees) us) of
+ (SOME b, [T]) => (pos, b, T)
+ | _ => raise FORMULA [phi])
+ | type_constraint_from_formula _ _ phi = raise FORMULA [phi]
(** Accumulate type constraints in a clause: negative type literals **)
@@ -305,68 +316,6 @@
fun is_positive_literal (@{const Not} $ _) = false
| is_positive_literal _ = true
-fun negate_term thy (Const (@{const_name All}, T) $ Abs (s, T', t')) =
- Const (@{const_name Ex}, T) $ Abs (s, T', negate_term thy t')
- | negate_term thy (Const (@{const_name Ex}, T) $ Abs (s, T', t')) =
- Const (@{const_name All}, T) $ Abs (s, T', negate_term thy t')
- | negate_term thy (@{const "op -->"} $ t1 $ t2) =
- @{const "op &"} $ t1 $ negate_term thy t2
- | negate_term thy (@{const "op &"} $ t1 $ t2) =
- @{const "op |"} $ negate_term thy t1 $ negate_term thy t2
- | negate_term thy (@{const "op |"} $ t1 $ t2) =
- @{const "op &"} $ negate_term thy t1 $ negate_term thy t2
- | negate_term _ (@{const Not} $ t) = t
- | negate_term _ t = @{const Not} $ t
-
-fun clause_for_literals _ [] = HOLogic.false_const
- | clause_for_literals _ [lit] = lit
- | clause_for_literals thy lits =
- case List.partition is_positive_literal lits of
- (pos_lits as _ :: _, neg_lits as _ :: _) =>
- @{const "op -->"}
- $ foldr1 HOLogic.mk_conj (map (negate_term thy) neg_lits)
- $ foldr1 HOLogic.mk_disj pos_lits
- | _ => foldr1 HOLogic.mk_disj lits
-
-(* Final treatment of the list of "real" literals from a clause.
- No "real" literals means only type information. *)
-fun finish_clause _ [] = HOLogic.true_const
- | finish_clause thy lits =
- lits |> filter_out (curry (op =) HOLogic.false_const) |> rev
- |> clause_for_literals thy
-
-(*Accumulate sort constraints in vt, with "real" literals in lits.*)
-fun lits_of_nodes thy full_types tfrees =
- let
- fun aux (vt, lits) [] = (vt, finish_clause thy lits)
- | aux (vt, lits) (u :: us) =
- aux (add_type_constraint
- (type_constraint_from_node true tfrees u) vt, lits) us
- handle NODE _ =>
- aux (vt, term_from_node thy full_types tfrees (SOME @{typ bool})
- [] u :: lits) us
- in aux end
-
-(* Update TVars with detected sort constraints. It's not totally clear when
- this code is necessary. *)
-fun repair_tvar_sorts vt =
- let
- fun do_type (Type (a, Ts)) = Type (a, map do_type Ts)
- | do_type (TVar (xi, s)) = TVar (xi, the_default s (Vartab.lookup vt xi))
- | do_type (TFree z) = TFree z
- fun do_term (Const (a, T)) = Const (a, do_type T)
- | do_term (Free (a, T)) = Free (a, do_type T)
- | do_term (Var (xi, T)) = Var (xi, do_type T)
- | do_term (t as Bound _) = t
- | do_term (Abs (a, T, t)) = Abs (a, do_type T, do_term t)
- | do_term (t1 $ t2) = do_term t1 $ do_term t2
- in not (Vartab.is_empty vt) ? do_term end
-
-fun unskolemize_term t =
- Term.add_consts t []
- |> filter (is_skolem_const_name o fst) |> map Const
- |> rpair t |-> fold forall_of
-
val combinator_table =
[(@{const_name COMBI}, @{thm COMBI_def_raw}),
(@{const_name COMBK}, @{thm COMBK_def_raw}),
@@ -382,14 +331,75 @@
| NONE => t)
| uncombine_term t = t
-(* Interpret a list of syntax trees as a clause, given by "real" literals and
- sort constraints. "vt" holds the initial sort constraints, from the
- conjecture clauses. *)
-fun clause_of_nodes ctxt full_types tfrees us =
+fun disjuncts (AConn (AOr, phis)) = maps disjuncts phis
+ | disjuncts phi = [phi]
+
+(* Update schematic type variables with detected sort constraints. It's not
+ totally clear when this code is necessary. *)
+fun repair_tvar_sorts (tvar_tab, t) =
let
- val thy = ProofContext.theory_of ctxt
- val (vt, t) = lits_of_nodes thy full_types tfrees (Vartab.empty, []) us
- in repair_tvar_sorts vt t end
+ fun do_type (Type (a, Ts)) = Type (a, map do_type Ts)
+ | do_type (TVar (xi, s)) =
+ TVar (xi, the_default s (Vartab.lookup tvar_tab xi))
+ | do_type (TFree z) = TFree z
+ fun do_term (Const (a, T)) = Const (a, do_type T)
+ | do_term (Free (a, T)) = Free (a, do_type T)
+ | do_term (Var (xi, T)) = Var (xi, do_type T)
+ | do_term (t as Bound _) = t
+ | do_term (Abs (a, T, t)) = Abs (a, do_type T, do_term t)
+ | do_term (t1 $ t2) = do_term t1 $ do_term t2
+ in t |> not (Vartab.is_empty tvar_tab) ? do_term end
+
+fun s_disj (t1, @{const False}) = t1
+ | s_disj p = HOLogic.mk_disj p
+
+fun quantify_over_free quant_s free_s body_t =
+ case Term.add_frees body_t [] |> filter (curry (op =) free_s o fst) of
+ [] => body_t
+ | frees as (_, free_T) :: _ =>
+ Abs (free_s, free_T, fold (curry abstract_over) (map Free frees) body_t)
+
+ (* Interpret a list of syntax trees as a clause, given by "real" literals and
+ sort constraints. Accumulates sort constraints in "tvar_tab", with "real"
+ literals in "lits". *)
+fun prop_from_formula thy full_types tfrees =
+ let
+ val do_sort_constraint =
+ add_type_constraint o type_constraint_from_formula true tfrees
+ fun do_real_literal phi =
+ case phi of
+ AQuant (_, [], phi) => do_real_literal phi
+ | AQuant (q, x :: xs, phi') =>
+ let
+ val body = do_real_literal (AQuant (q, xs, phi'))
+ val quant_s = case q of
+ AForall => @{const_name All}
+ | AExists => @{const_name Ex}
+ in quantify_over_free quant_s x body end
+ | AConn (ANot, [phi']) => HOLogic.mk_not (do_real_literal phi')
+ | AConn (c, [phi1, phi2]) =>
+ (phi1, phi2)
+ |> pairself do_real_literal
+ |> (case c of
+ AAnd => HOLogic.mk_conj
+ | AOr => HOLogic.mk_disj
+ | AImplies => HOLogic.mk_imp
+ | AIff => (fn (t1, t2) => HOLogic.eq_const HOLogic.boolT $ t1 $ t2))
+ | APred tm =>
+ term_from_fo_term thy full_types tfrees (SOME @{typ bool}) tm
+ | _ => raise FORMULA [phi]
+ fun do_literals (tvar_tab, t) [] = (tvar_tab, t)
+ | do_literals (tvar_tab, t) (u :: us) =
+ (do_literals (tvar_tab |> do_sort_constraint u, t) us
+ handle FO_TERM _ => raise SAME ()
+ | FORMULA _ => raise SAME ())
+ handle SAME () =>
+ do_literals (tvar_tab, s_disj (do_real_literal u, t)) us
+ in
+ repair_tvar_sorts o do_literals (Vartab.empty, HOLogic.false_const)
+ o disjuncts
+ end
+
fun check_formula ctxt =
Type_Infer.constrain @{typ bool}
#> Syntax.check_term (ProofContext.set_mode ProofContext.mode_schematic ctxt)
@@ -400,13 +410,14 @@
fun unvarify_term (Var ((s, 0), T)) = Free (s, T)
| unvarify_term t = raise TERM ("unvarify_term: non-Var", [t])
-fun decode_line full_types tfrees (Definition (num, u, us)) ctxt =
+fun decode_line full_types tfrees (Definition (num, phi1, phi2)) ctxt =
let
- val t1 = clause_of_nodes ctxt full_types tfrees [u]
+ val thy = ProofContext.theory_of ctxt
+ val t1 = prop_from_formula thy full_types tfrees phi1
val vars = snd (strip_comb t1)
val frees = map unvarify_term vars
val unvarify_args = subst_atomic (vars ~~ frees)
- val t2 = clause_of_nodes ctxt full_types tfrees us
+ val t2 = prop_from_formula thy full_types tfrees phi2
val (t1, t2) =
HOLogic.eq_const HOLogic.typeT $ t1 $ t2
|> unvarify_args |> uncombine_term |> check_formula ctxt
@@ -415,10 +426,11 @@
(Definition (num, t1, t2),
fold Variable.declare_term (maps OldTerm.term_frees [t1, t2]) ctxt)
end
- | decode_line full_types tfrees (Inference (num, us, deps)) ctxt =
+ | decode_line full_types tfrees (Inference (num, u, deps)) ctxt =
let
- val t = us |> clause_of_nodes ctxt full_types tfrees
- |> unskolemize_term |> uncombine_term |> check_formula ctxt
+ val thy = ProofContext.theory_of ctxt
+ val t = u |> prop_from_formula thy full_types tfrees
+ |> uncombine_term |> check_formula ctxt
in
(Inference (num, t, deps),
fold Variable.declare_term (OldTerm.term_frees t) ctxt)
@@ -507,11 +519,10 @@
(** EXTRACTING LEMMAS **)
-(* A list consisting of the first number in each line is returned.
- TSTP: Interesting lines have the form "fof(108, axiom, ...)", where the
- number (108) is extracted.
- SPASS: Lines have the form "108[0:Inp] ...", where the first number (108) is
- extracted. *)
+(* A list consisting of the first number in each line is returned. For TSTP,
+ interesting lines have the form "fof(108, axiom, ...)", where the number
+ (108) is extracted. For SPASS, lines have the form "108[0:Inp] ...", where
+ the first number (108) is extracted. *)
fun extract_formula_numbers_in_atp_proof atp_proof =
let
val tokens_of = String.tokens (not o Char.isAlphaNum)
@@ -600,6 +611,7 @@
else
apfst (insert (op =) (raw_prefix, num))
+fun forall_of v t = HOLogic.all_const (fastype_of v) $ lambda v t
fun forall_vars t = fold_rev forall_of (map Var (Term.add_vars t [])) t
fun step_for_line _ _ (Definition (_, t1, t2)) = Let (t1, t2)
@@ -613,7 +625,7 @@
atp_proof conjecture_shape thm_names params frees =
let
val lines =
- atp_proof ^ "$" (* the $ sign acts as a sentinel *)
+ atp_proof ^ "$" (* the $ sign acts as a sentinel (FIXME: pick it up) *)
|> parse_proof pool
|> decode_lines ctxt full_types tfrees
|> rpair [] |-> fold_rev (add_line conjecture_shape thm_names)
@@ -674,32 +686,26 @@
| 1 => [Then]
| _ => [Ultimately]
-fun redirect_proof thy conjecture_shape hyp_ts concl_t proof =
+fun redirect_proof conjecture_shape hyp_ts concl_t proof =
let
(* The first pass outputs those steps that are independent of the negated
conjecture. The second pass flips the proof by contradiction to obtain a
direct proof, introducing case splits when an inference depends on
several facts that depend on the negated conjecture. *)
fun find_hyp num = nth hyp_ts (index_in_shape num conjecture_shape)
- val concl_ls = map (pair raw_prefix) (List.last conjecture_shape)
- val canonicalize_labels =
- map (fn l => if member (op =) concl_ls l then hd concl_ls else l)
- #> distinct (op =)
+ val concl_l = (raw_prefix, List.last conjecture_shape)
fun first_pass ([], contra) = ([], contra)
| first_pass ((step as Fix _) :: proof, contra) =
first_pass (proof, contra) |>> cons step
| first_pass ((step as Let _) :: proof, contra) =
first_pass (proof, contra) |>> cons step
| first_pass ((step as Assume (l as (_, num), _)) :: proof, contra) =
- if member (op =) concl_ls l then
- first_pass (proof, contra ||> l = hd concl_ls ? cons step)
+ if l = concl_l then
+ first_pass (proof, contra ||> l = concl_l ? cons step)
else
first_pass (proof, contra) |>> cons (Assume (l, find_hyp num))
| first_pass (Have (qs, l, t, ByMetis (ls, ss)) :: proof, contra) =
- let
- val ls = canonicalize_labels ls
- val step = Have (qs, l, t, ByMetis (ls, ss))
- in
+ let val step = Have (qs, l, t, ByMetis (ls, ss)) in
if exists (member (op =) (fst contra)) ls then
first_pass (proof, contra |>> cons l ||> cons step)
else
@@ -707,7 +713,7 @@
end
| first_pass _ = raise Fail "malformed proof"
val (proof_top, (contra_ls, contra_proof)) =
- first_pass (proof, (concl_ls, []))
+ first_pass (proof, ([concl_l], []))
val backpatch_label = the_default ([], []) oo AList.lookup (op =) o fst
fun backpatch_labels patches ls =
fold merge_fact_sets (map (backpatch_label patches) ls) ([], [])
@@ -733,16 +739,16 @@
(proof, assums,
patches |>> cons (contra_l, (l :: co_ls, ss)))
|>> cons (if member (op =) (fst (snd patches)) l then
- Assume (l, negate_term thy t)
+ Assume (l, negate_term t)
else
- Have (qs, l, negate_term thy t,
+ Have (qs, l, negate_term t,
ByMetis (backpatch_label patches l)))
| (contra_ls as _ :: _, co_ls) =>
let
val proofs =
map_filter
(fn l =>
- if member (op =) concl_ls l then
+ if l = concl_l then
NONE
else
let
@@ -756,7 +762,7 @@
end) contra_ls
val (assumes, facts) =
if member (op =) (fst (snd patches)) l then
- ([Assume (l, negate_term thy t)], (l :: co_ls, ss))
+ ([Assume (l, negate_term t)], (l :: co_ls, ss))
else
([], (co_ls, ss))
in
@@ -927,18 +933,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
- val thy = ProofContext.theory_of ctxt
+ (* ### 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) []
@@ -948,7 +948,7 @@
case proof_from_atp_proof pool ctxt full_types tfrees isar_shrink_factor
atp_proof conjecture_shape thm_names params
frees
- |> redirect_proof thy conjecture_shape hyp_ts concl_t
+ |> redirect_proof conjecture_shape hyp_ts concl_t
|> kill_duplicate_assumptions_in_proof
|> then_chain_proof
|> kill_useless_labels_in_proof
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML Tue Jul 27 12:02:10 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML Tue Jul 27 14:02:15 2010 +0200
@@ -7,14 +7,31 @@
signature SLEDGEHAMMER_TPTP_FORMAT =
sig
+ type name = Metis_Clauses.name
+ type kind = Metis_Clauses.kind
+ type combterm = Metis_Clauses.combterm
type class_rel_clause = Metis_Clauses.class_rel_clause
type arity_clause = Metis_Clauses.arity_clause
- type fol_clause = Metis_Clauses.fol_clause
+
+ datatype 'a fo_term = ATerm of 'a * 'a fo_term list
+ datatype quantifier = AForall | AExists
+ datatype connective = ANot | AAnd | AOr | AImplies | AIf | AIff | ANotIff
+ datatype ('a, 'b) formula =
+ AQuant of quantifier * 'a list * ('a, 'b) formula |
+ AConn of connective * ('a, 'b) formula list |
+ APred of 'b
+
+ datatype fol_formula =
+ FOLFormula of {formula_name: string,
+ kind: kind,
+ combformula: (name, combterm) formula,
+ ctypes_sorts: typ list}
val axiom_prefix : string
+ val conjecture_prefix : string
val write_tptp_file :
- theory -> bool -> bool -> bool -> Path.T
- -> fol_clause list * fol_clause list * fol_clause list * fol_clause list
+ theory -> bool -> bool -> bool -> bool -> Path.T
+ -> fol_formula list * fol_formula list * fol_formula list * fol_formula list
* class_rel_clause list * arity_clause list
-> string Symtab.table * int
end;
@@ -30,15 +47,19 @@
datatype 'a fo_term = ATerm of 'a * 'a fo_term list
datatype quantifier = AForall | AExists
-datatype connective = ANot | AAnd | AOr | AImplies | AIff
-datatype 'a formula =
- AQuant of quantifier * 'a list * 'a formula |
- AConn of connective * 'a formula list |
- APred of 'a fo_term
+datatype connective = ANot | AAnd | AOr | AImplies | AIf | AIff | ANotIff
+datatype ('a, 'b) formula =
+ AQuant of quantifier * 'a list * ('a, 'b) formula |
+ AConn of connective * ('a, 'b) formula list |
+ APred of 'b
fun mk_anot phi = AConn (ANot, [phi])
+fun mk_aconn c phi1 phi2 = AConn (c, [phi1, phi2])
+fun mk_ahorn [] phi = phi
+ | mk_ahorn (phi :: phis) psi =
+ AConn (AImplies, [fold (mk_aconn AAnd) phis phi, psi])
-datatype 'a problem_line = Fof of string * kind * 'a formula
+datatype 'a problem_line = Fof of string * kind * ('a, 'a fo_term) formula
type 'a problem = (string * 'a problem_line list) list
fun string_for_term (ATerm (s, [])) = s
@@ -51,10 +72,14 @@
| string_for_connective AAnd = "&"
| string_for_connective AOr = "|"
| string_for_connective AImplies = "=>"
+ | string_for_connective AIf = "<="
| 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 (ANot, [APred (ATerm ("equal", ts))])) =
+ space_implode " != " (map string_for_term ts)
| string_for_formula (AConn (c, [phi])) =
string_for_connective c ^ " " ^ string_for_formula phi
| string_for_formula (AConn (c, phis)) =
@@ -137,11 +162,16 @@
(** Sledgehammer stuff **)
+datatype fol_formula =
+ FOLFormula of {formula_name: string,
+ kind: kind,
+ combformula: (name, combterm) formula,
+ ctypes_sorts: typ list}
+
val axiom_prefix = "ax_"
val conjecture_prefix = "conj_"
val arity_clause_prefix = "clsarity_"
-
-fun hol_ident prefix axiom_name = prefix ^ ascii_of axiom_name
+val tfrees_name = "tfrees"
fun wrap_type ty t = ATerm ((type_wrapper_name, type_wrapper_name), [ty, t])
@@ -150,49 +180,51 @@
| fo_term_for_combtyp (CombType (name, tys)) =
ATerm (name, map fo_term_for_combtyp tys)
-fun fo_term_for_combterm full_types top_level u =
- let
- val (head, args) = strip_combterm_comb u
- val (x, ty_args) =
- case head of
- CombConst (name, _, ty_args) =>
- if fst name = "equal" then
- (if top_level andalso length args = 2 then name
- else ("c_fequal", @{const_name fequal}), [])
- else
- (name, if full_types then [] else ty_args)
- | CombVar (name, _) => (name, [])
- | CombApp _ => raise Fail "impossible \"CombApp\""
- val t = ATerm (x, map fo_term_for_combtyp ty_args @
- map (fo_term_for_combterm full_types false) args)
- in
- if full_types then wrap_type (fo_term_for_combtyp (type_of_combterm u)) t
- else t
- end
-
-fun fo_literal_for_literal full_types (FOLLiteral (pos, t)) =
- (pos, fo_term_for_combterm full_types true t)
-
-fun fo_literal_for_type_literal pos (TyLitVar (class, name)) =
- (pos, ATerm (class, [ATerm (name, [])]))
- | fo_literal_for_type_literal pos (TyLitFree (class, name)) =
- (pos, ATerm (class, [ATerm (name, [])]))
+fun fo_literal_for_type_literal (TyLitVar (class, name)) =
+ (true, ATerm (class, [ATerm (name, [])]))
+ | fo_literal_for_type_literal (TyLitFree (class, name)) =
+ (true, ATerm (class, [ATerm (name, [])]))
fun formula_for_fo_literal (pos, t) = APred t |> not pos ? mk_anot
-fun formula_for_fo_literals [] = APred (ATerm (("$false", "$false"), []))
- | formula_for_fo_literals (lit :: lits) =
- AConn (AOr, [formula_for_fo_literal lit, formula_for_fo_literals lits])
-fun formula_for_axiom full_types (FOLClause {literals, ctypes_sorts, ...}) =
- map (fo_literal_for_literal full_types) literals @
- map (fo_literal_for_type_literal false)
- (type_literals_for_types ctypes_sorts)
- |> formula_for_fo_literals
+fun fo_term_for_combterm full_types =
+ let
+ fun aux top_level u =
+ let
+ val (head, args) = strip_combterm_comb u
+ val (x, ty_args) =
+ case head of
+ CombConst (name, _, ty_args) =>
+ if fst name = "equal" then
+ (if top_level andalso length args = 2 then name
+ else ("c_fequal", @{const_name fequal}), [])
+ else
+ (name, if full_types then [] else ty_args)
+ | CombVar (name, _) => (name, [])
+ | CombApp _ => raise Fail "impossible \"CombApp\""
+ val t = ATerm (x, map fo_term_for_combtyp ty_args @
+ map (aux false) args)
+ in
+ if full_types then wrap_type (fo_term_for_combtyp (combtyp_of u)) t else t
+ end
+ in aux true end
+
+fun formula_for_combformula full_types =
+ let
+ fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi)
+ | aux (AConn (c, phis)) = AConn (c, map aux phis)
+ | aux (APred tm) = APred (fo_term_for_combterm full_types tm)
+ in aux end
+
+fun formula_for_axiom full_types (FOLFormula {combformula, ctypes_sorts, ...}) =
+ mk_ahorn (map (formula_for_fo_literal o fo_literal_for_type_literal)
+ (type_literals_for_types ctypes_sorts))
+ (formula_for_combformula full_types combformula)
fun problem_line_for_axiom full_types
- (clause as FOLClause {axiom_name, kind, ...}) =
- Fof (hol_ident axiom_prefix axiom_name, kind,
- formula_for_axiom full_types clause)
+ (formula as FOLFormula {formula_name, kind, ...}) =
+ Fof (axiom_prefix ^ ascii_of formula_name, kind,
+ formula_for_axiom full_types formula)
fun problem_line_for_class_rel_clause
(ClassRelClause {axiom_name, subclass, superclass, ...}) =
@@ -210,23 +242,24 @@
fun problem_line_for_arity_clause
(ArityClause {axiom_name, conclLit, premLits, ...}) =
Fof (arity_clause_prefix ^ ascii_of axiom_name, Axiom,
- map fo_literal_for_arity_literal (conclLit :: premLits)
- |> formula_for_fo_literals)
+ mk_ahorn (map (formula_for_fo_literal o apfst not
+ o fo_literal_for_arity_literal) premLits)
+ (formula_for_fo_literal
+ (fo_literal_for_arity_literal conclLit)))
fun problem_line_for_conjecture full_types
- (clause as FOLClause {axiom_name, kind, literals, ...}) =
- Fof (hol_ident conjecture_prefix axiom_name, kind,
- map (fo_literal_for_literal full_types) literals
- |> formula_for_fo_literals |> mk_anot)
+ (FOLFormula {formula_name, kind, combformula, ...}) =
+ Fof (conjecture_prefix ^ formula_name, kind,
+ formula_for_combformula full_types combformula)
-fun atp_free_type_literals_for_conjecture (FOLClause {ctypes_sorts, ...}) =
- map (fo_literal_for_type_literal true) (type_literals_for_types ctypes_sorts)
+fun free_type_literals_for_conjecture (FOLFormula {ctypes_sorts, ...}) =
+ map fo_literal_for_type_literal (type_literals_for_types ctypes_sorts)
fun problem_line_for_free_type lit =
- Fof ("tfree_tcs", Conjecture, formula_for_fo_literal lit)
+ Fof (tfrees_name, Conjecture, mk_anot (formula_for_fo_literal lit))
fun problem_lines_for_free_types conjectures =
let
- val litss = map atp_free_type_literals_for_conjecture conjectures
+ val litss = map free_type_literals_for_conjecture conjectures
val lits = fold (union (op =)) litss []
in map problem_line_for_free_type lits end
@@ -269,7 +302,7 @@
16383 (* large number *)
else if full_types then
0
- else case strip_prefix const_prefix s of
+ else case strip_prefix_and_undo_ascii const_prefix s of
SOME s' => num_type_args thy (invert_const s')
| NONE => 0)
| min_arity_of _ _ (SOME the_const_tab) s =
@@ -360,11 +393,10 @@
repair_problem_with_const_table thy explicit_forall full_types
(const_table_for_problem explicit_apply problem) problem
-fun write_tptp_file thy readable_names full_types explicit_apply file
- (conjectures, axiom_clauses, extra_clauses, helper_clauses,
- class_rel_clauses, arity_clauses) =
+fun write_tptp_file thy readable_names explicit_forall full_types explicit_apply
+ file (conjectures, axiom_clauses, extra_clauses,
+ helper_clauses, class_rel_clauses, arity_clauses) =
let
- val explicit_forall = true (* FIXME *)
val axiom_lines = map (problem_line_for_axiom full_types) axiom_clauses
val class_rel_lines =
map problem_line_for_class_rel_clause class_rel_clauses
@@ -373,6 +405,8 @@
val conjecture_lines =
map (problem_line_for_conjecture full_types) conjectures
val tfree_lines = problem_lines_for_free_types conjectures
+ (* Reordering these might or might not confuse the proof reconstruction
+ code or the SPASS Flotter hack. *)
val problem =
[("Relevant facts", axiom_lines),
("Class relationships", class_rel_lines),
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Tue Jul 27 12:02:10 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Tue Jul 27 14:02:15 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;