# HG changeset patch # User wenzelm # Date 1248797855 -7200 # Node ID bad5a99c16d8a915b578fddcc1ca8e012a0ebcf5 # Parent 8721c74c53826df089b4241d33361de419e874ae neg_conjecture_clauses, neg_clausify_tac: proper context, eliminated METAHYPS; external_prover: neg_conjecture_clauses should handle TVars within goals; misc tuning; diff -r 8721c74c5382 -r bad5a99c16d8 src/HOL/Tools/atp_wrapper.ML --- a/src/HOL/Tools/atp_wrapper.ML Tue Jul 28 18:17:35 2009 +0200 +++ b/src/HOL/Tools/atp_wrapper.ML Tue Jul 28 18:17:35 2009 +0200 @@ -59,9 +59,7 @@ val (ctxt, (chain_ths, th)) = goal val thy = ProofContext.theory_of ctxt val chain_ths = map (Thm.put_name_hint ResReconstruct.chained_hint) chain_ths - val goal_cls = #1 (ResAxioms.neg_conjecture_clauses th subgoalno) - handle THM ("assume: variables", _, _) => - error "Sledgehammer: Goal contains type variables (TVars)" + val goal_cls = #1 (ResAxioms.neg_conjecture_clauses ctxt th subgoalno) val _ = app (fn th => Output.debug (fn _ => Display.string_of_thm ctxt th)) goal_cls val the_filtered_clauses = case filtered_clauses of @@ -71,7 +69,8 @@ case axiom_clauses of NONE => the_filtered_clauses | SOME axcls => axcls - val (thm_names, clauses) = preparer goal_cls chain_ths the_axiom_clauses the_filtered_clauses thy + val (thm_names, clauses) = + preparer goal_cls chain_ths the_axiom_clauses the_filtered_clauses thy (* write out problem file and call prover *) val probfile = prob_pathname subgoalno @@ -85,7 +84,7 @@ val _ = if destdir' = "" then File.rm probfile else File.write (Path.explode (Path.implode probfile ^ "_proof")) proof - + (* check for success and print out some information on failure *) val failure = find_failure proof val success = rc = 0 andalso is_none failure @@ -133,7 +132,7 @@ fun vampire_opts max_new theory_const timeout = tptp_prover_opts max_new theory_const (Path.explode "$VAMPIRE_HOME/vampire", - ("--output_syntax tptp --mode casc -t " ^ string_of_int timeout)) + ("--output_syntax tptp --mode casc -t " ^ string_of_int timeout)) timeout; val vampire = vampire_opts 60 false; @@ -141,7 +140,7 @@ fun vampire_opts_full max_new theory_const timeout = full_prover_opts max_new theory_const (Path.explode "$VAMPIRE_HOME/vampire", - ("--output_syntax tptp --mode casc -t " ^ string_of_int timeout)) + ("--output_syntax tptp --mode casc -t " ^ string_of_int timeout)) timeout; val vampire_full = vampire_opts_full 60 false; @@ -173,7 +172,8 @@ (ResAtp.prepare_clauses true) (ResHolClause.dfg_write_file (AtpManager.get_full_types())) (Path.explode "$SPASS_HOME/SPASS", - "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof -TimeLimit=" ^ string_of_int timeout) + "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof -TimeLimit=" ^ + string_of_int timeout) ResReconstruct.find_failure (ResReconstruct.lemma_list true) timeout ax_clauses fcls name n goal; @@ -196,22 +196,23 @@ end; fun refresh_systems () = Synchronized.change systems (fn _ => - get_systems()); + get_systems ()); fun get_system prefix = Synchronized.change_result systems (fn systems => let val systems = if null systems then get_systems() else systems in (find_first (String.isPrefix prefix) systems, systems) end); fun remote_prover_opts max_new theory_const args prover_prefix timeout = - let val sys = case get_system prover_prefix of + let val sys = + case get_system prover_prefix of NONE => error ("No system like " ^ quote prover_prefix ^ " at SystemOnTPTP") | SOME sys => sys in tptp_prover_opts max_new theory_const (Path.explode "$ISABELLE_HOME/lib/scripts/SystemOnTPTP", - args ^ " -t " ^ string_of_int timeout ^ " -s " ^ sys) timeout end; + args ^ " -t " ^ string_of_int timeout ^ " -s " ^ sys) timeout + end; val remote_prover = remote_prover_opts 60 false; end; - diff -r 8721c74c5382 -r bad5a99c16d8 src/HOL/Tools/res_axioms.ML --- a/src/HOL/Tools/res_axioms.ML Tue Jul 28 18:17:35 2009 +0200 +++ b/src/HOL/Tools/res_axioms.ML Tue Jul 28 18:17:35 2009 +0200 @@ -14,7 +14,7 @@ val neg_clausify: thm list -> thm list val expand_defs_tac: thm -> tactic val combinators: thm -> thm - val neg_conjecture_clauses: thm -> int -> thm list * (string * typ) list + val neg_conjecture_clauses: Proof.context -> thm -> int -> thm list * (string * typ) list val atpset_rules_of: Proof.context -> (string * thm) list val suppress_endtheory: bool ref (*for emergency use where endtheory causes problems*) val setup: theory -> theory @@ -498,32 +498,30 @@ val neg_skolemize_tac = EVERY' [rtac ccontr, ObjectLogic.atomize_prems_tac, Meson.skolemize_tac]; -fun neg_clausify sts = - sts |> Meson.make_clauses |> map combinators |> Meson.finish_cnf; +val neg_clausify = Meson.make_clauses #> map combinators #> Meson.finish_cnf; -fun neg_conjecture_clauses st0 n = - let val st = Seq.hd (neg_skolemize_tac n st0) - val (params,_,_) = OldGoals.strip_context (Logic.nth_prem (n, Thm.prop_of st)) - in (neg_clausify (the (OldGoals.metahyps_thms n st)), params) end - handle Option => error "unable to Skolemize subgoal"; +fun neg_conjecture_clauses ctxt st0 n = + let + val st = Seq.hd (neg_skolemize_tac n st0) + val ({params, prems, ...}, _) = Subgoal.focus (Variable.set_body false ctxt) n st + in (neg_clausify prems, map (Term.dest_Free o Thm.term_of o #2) params) end; (*Conversion of a subgoal to conjecture clauses. Each clause has leading !!-bound universal variables, to express generality. *) -val neg_clausify_tac = +fun neg_clausify_tac ctxt = neg_skolemize_tac THEN' - SUBGOAL - (fn (prop,_) => - let val ts = Logic.strip_assums_hyp prop - in EVERY1 - [OldGoals.METAHYPS - (fn hyps => - (Method.insert_tac - (map forall_intr_vars (neg_clausify hyps)) 1)), - REPEAT_DETERM_N (length ts) o (etac thin_rl)] + SUBGOAL (fn (prop, i) => + let val ts = Logic.strip_assums_hyp prop in + EVERY' + [FOCUS + (fn {prems, ...} => + (Method.insert_tac + (map forall_intr_vars (neg_clausify prems)) i)) ctxt, + REPEAT_DETERM_N (length ts) o etac thin_rl] i end); val neg_clausify_setup = - Method.setup @{binding neg_clausify} (Scan.succeed (K (SIMPLE_METHOD' neg_clausify_tac))) + Method.setup @{binding neg_clausify} (Scan.succeed (SIMPLE_METHOD' o neg_clausify_tac)) "conversion of goal to conjecture clauses";