improvements to proof reconstruction. Some files loaded in a different order
--- a/src/HOL/ATP_Linkup.thy Thu Jan 04 17:52:28 2007 +0100
+++ b/src/HOL/ATP_Linkup.thy Thu Jan 04 17:55:12 2007 +0100
@@ -11,11 +11,11 @@
uses
"Tools/polyhash.ML"
"Tools/res_clause.ML"
- "Tools/res_reconstruct.ML"
- "Tools/ATP/watcher.ML"
"Tools/ATP/reduce_axiomsN.ML"
("Tools/res_hol_clause.ML")
("Tools/res_axioms.ML")
+ ("Tools/res_reconstruct.ML")
+ ("Tools/ATP/watcher.ML")
("Tools/res_atp.ML")
("Tools/res_atp_provers.ML")
("Tools/res_atp_methods.ML")
@@ -83,8 +83,10 @@
lemma iff_negative: "~P | ~Q | P=Q"
by blast
-use "Tools/res_axioms.ML"
-use "Tools/res_hol_clause.ML"
+use "Tools/res_axioms.ML" --{*requires the combinators declared above*}
+use "Tools/res_hol_clause.ML" --{*requires the combinators*}
+use "Tools/res_reconstruct.ML"
+use "Tools/ATP/watcher.ML"
use "Tools/res_atp.ML"
setup ResAxioms.meson_method_setup
--- a/src/HOL/Hilbert_Choice.thy Thu Jan 04 17:52:28 2007 +0100
+++ b/src/HOL/Hilbert_Choice.thy Thu Jan 04 17:55:12 2007 +0100
@@ -620,10 +620,9 @@
*}
-subsection {* Meson method setup *}
+subsection {* Meson package *}
use "Tools/meson.ML"
-setup Meson.skolemize_setup
subsection {* Specification package -- Hilbertized version *}
--- a/src/HOL/Tools/meson.ML Thu Jan 04 17:52:28 2007 +0100
+++ b/src/HOL/Tools/meson.ML Thu Jan 04 17:55:12 2007 +0100
@@ -36,7 +36,6 @@
val negate_head : thm -> thm
val select_literal : int -> thm -> thm
val skolemize_tac : int -> tactic
- val make_clauses_tac : int -> tactic
end
@@ -646,34 +645,6 @@
end
handle Subscript => Seq.empty;
-(*Top-level conversion to meta-level clauses. Each clause has
- leading !!-bound universal variables, to express generality. To get
- meta-clauses instead of disjunctions, uncomment "make_meta_clauses" below.*)
-val make_clauses_tac =
- SUBGOAL
- (fn (prop,_) =>
- let val ts = Logic.strip_assums_hyp prop
- in EVERY1
- [METAHYPS
- (fn hyps =>
- (Method.insert_tac
- (map forall_intr_vars
- ( (**make_meta_clauses**) (make_clauses hyps))) 1)),
- REPEAT_DETERM_N (length ts) o (etac thin_rl)]
- end);
-
-
-(*** setup the special skoklemization methods ***)
-
-(*No CHANGED_PROP here, since these always appear in the preamble*)
-
-val skolemize_setup =
- Method.add_methods
- [("skolemize", Method.no_args (Method.SIMPLE_METHOD' skolemize_tac),
- "Skolemization into existential quantifiers"),
- ("make_clauses", Method.no_args (Method.SIMPLE_METHOD' make_clauses_tac),
- "Conversion to !!-quantified meta-level clauses")];
-
end;
structure BasicMeson: BASIC_MESON = Meson;
--- a/src/HOL/Tools/res_atp.ML Thu Jan 04 17:52:28 2007 +0100
+++ b/src/HOL/Tools/res_atp.ML Thu Jan 04 17:55:12 2007 +0100
@@ -823,13 +823,6 @@
let val path = File.explode_platform_path fname
in Vector.app (File.append path o (fn s => s ^ "\n")) end;
-(*Converting a subgoal into negated conjecture clauses*)
-fun neg_clauses th n =
- let val tacs = [rtac ccontr, ObjectLogic.atomize_tac, skolemize_tac]
- val st = Seq.hd (EVERY' tacs n th)
- val negs = Option.valOf (metahyps_thms n st)
- in make_clauses negs |> ResAxioms.assume_abstract_list |> Meson.finish_cnf end;
-
(*We write out problem files for each subgoal. Argument probfile generates filenames,
and allows the suppression of the suffix "_1" in problem-generation mode.
FIXME: does not cope with &&, and it isn't easy because one could have multiple
@@ -839,7 +832,8 @@
val _ = Output.debug ("number of subgoals = " ^ Int.toString (length goals))
val thy = ProofContext.theory_of ctxt
fun get_neg_subgoals [] _ = []
- | get_neg_subgoals (gl::gls) n = neg_clauses th n :: get_neg_subgoals gls (n+1)
+ | get_neg_subgoals (gl::gls) n = #1 (ResAxioms.neg_conjecture_clauses th n) ::
+ get_neg_subgoals gls (n+1)
val goal_cls = get_neg_subgoals goals 1
val logic = case !linkup_logic_mode of
Auto => problem_logic_goals (map ((map prop_of)) goal_cls)
--- a/src/HOL/Tools/res_axioms.ML Thu Jan 04 17:52:28 2007 +0100
+++ b/src/HOL/Tools/res_axioms.ML Thu Jan 04 17:55:12 2007 +0100
@@ -18,8 +18,9 @@
val meson_method_setup : theory -> theory
val setup : theory -> theory
val assume_abstract_list: thm list -> thm list
- val claset_rules_of: Proof.context -> (string * thm) list
- val simpset_rules_of: Proof.context -> (string * thm) list
+ val neg_conjecture_clauses: thm -> int -> thm list * (string * typ) list
+ val claset_rules_of: Proof.context -> (string * thm) list (*FIXME DELETE*)
+ val simpset_rules_of: Proof.context -> (string * thm) list (*FIXME DELETE*)
val atpset_rules_of: Proof.context -> (string * thm) list
end;
@@ -619,6 +620,32 @@
val clausify = Attrib.syntax (Scan.lift Args.nat
>> (fn i => Thm.rule_attribute (fn _ => fn th => clausify_rule (th, i))));
+
+(*** Converting a subgoal into negated conjecture clauses. ***)
+
+val neg_skolemize_tac = EVERY' [rtac ccontr, ObjectLogic.atomize_tac, skolemize_tac];
+val neg_clausify = Meson.finish_cnf o assume_abstract_list o make_clauses;
+
+fun neg_conjecture_clauses st0 n =
+ let val st = Seq.hd (neg_skolemize_tac n st0)
+ val (params,_,_) = strip_context (Logic.nth_prem (n, Thm.prop_of st))
+ in (neg_clausify (Option.valOf (metahyps_thms n st)), params) end;
+
+(*Conversion of a subgoal to conjecture clauses. Each clause has
+ leading !!-bound universal variables, to express generality. *)
+val neg_clausify_tac =
+ neg_skolemize_tac THEN'
+ SUBGOAL
+ (fn (prop,_) =>
+ let val ts = Logic.strip_assums_hyp prop
+ in EVERY1
+ [METAHYPS
+ (fn hyps =>
+ (Method.insert_tac
+ (map forall_intr_vars (neg_clausify hyps)) 1)),
+ REPEAT_DETERM_N (length ts) o (etac thin_rl)]
+ end);
+
(** The Skolemization attribute **)
fun conj2_rule (th1,th2) = conjI OF [th1,th2];
@@ -635,8 +662,12 @@
val setup_attrs = Attrib.add_attributes
[("skolem", Attrib.no_args skolem_attr, "skolemization of a theorem"),
- ("clausify", clausify, "conversion to clauses")];
+ ("clausify", clausify, "conversion of theorem to clauses")];
+
+val setup_methods = Method.add_methods
+ [("neg_clausify", Method.no_args (Method.SIMPLE_METHOD' neg_clausify_tac),
+ "conversion of goal to conjecture clauses")];
-val setup = clause_cache_setup #> setup_attrs;
+val setup = clause_cache_setup #> setup_attrs #> setup_methods;
end;
--- a/src/HOL/Tools/res_reconstruct.ML Thu Jan 04 17:52:28 2007 +0100
+++ b/src/HOL/Tools/res_reconstruct.ML Thu Jan 04 17:55:12 2007 +0100
@@ -3,8 +3,6 @@
Copyright 2004 University of Cambridge
*)
-(*FIXME: can we delete the "thm * int" and "th sgno" below?*)
-
(***************************************************************************)
(* Code to deal with the transfer of proofs from a prover process *)
(***************************************************************************)
@@ -322,10 +320,30 @@
let val vt0 = tfree_constraints_of_clauses Vartab.empty (map #3 tuples)
in map (decode_tstp thy vt0) tuples end;
-fun isar_lines ctxt =
+(*FIXME: simmilar function in res_atp. Move to HOLogic?*)
+fun dest_disj_aux (Const ("op |", _) $ t $ t') disjs = dest_disj_aux t (dest_disj_aux t' disjs)
+ | dest_disj_aux t disjs = t::disjs;
+
+fun dest_disj t = dest_disj_aux t [];
+
+val sort_lits = sort Term.fast_term_ord o dest_disj o HOLogic.dest_Trueprop o strip_all_body;
+
+fun permuted_clause t =
+ let val lits = sort_lits t
+ fun perm [] = NONE
+ | perm (ctm::ctms) =
+ if forall (op aconv) (ListPair.zip (lits, sort_lits ctm)) then SOME ctm
+ else perm ctms
+ in perm end;
+
+(*ctms is a list of conjecture clauses as yielded by Isabelle. Those returned by the
+ ATP may have their literals reordered.*)
+fun isar_lines ctxt ctms =
let val string_of = ProofContext.string_of_term ctxt
fun doline hs (lname, t, []) = (*No deps: it's a conjecture clause, with no proof.*)
- "assume " ^ lname ^ ": \"" ^ string_of t ^ "\"\n"
+ (case permuted_clause t ctms of
+ SOME u => "assume " ^ lname ^ ": \"" ^ string_of u ^ "\"\n"
+ | NONE => "assume? " ^ lname ^ ": \"" ^ string_of t ^ "\"\n") (*no match!!*)
| doline hs (lname, t, deps) =
hs ^ lname ^ ": \"" ^ string_of t ^
"\"\n by (meson " ^ space_implode " " deps ^ ")\n"
@@ -364,7 +382,7 @@
(lno, t', deps) :: (*replace later line by earlier one*)
(pre @ map (replace_deps (lno', [lno])) post));
-(*Replace numeric proof lines by strings.*)
+(*Replace numeric proof lines by strings, either from thm_names or sequential line numbers*)
fun stringify_deps thm_names deps_map [] = []
| stringify_deps thm_names deps_map ((lno, t, deps) :: lines) =
if lno <= Vector.length thm_names (*axiom*)
@@ -377,22 +395,24 @@
stringify_deps thm_names ((lno,lname)::deps_map) lines
end;
-val proofstart = "\nproof (rule ccontr, skolemize, make_clauses)\n";
-
-fun string_of_Free (Free (x,_)) = x
- | string_of_Free _ = "??string_of_Free??";
+val proofstart = "\nproof (neg_clausify)\n";
fun isar_header [] = proofstart
- | isar_header ts = proofstart ^ "fix " ^ space_implode " " (map string_of_Free ts) ^ "\n";
+ | isar_header ts = proofstart ^ "fix " ^ space_implode " " ts ^ "\n";
-fun decode_tstp_file ctxt (cnfs,thm_names) =
+fun decode_tstp_file cnfs th sgno thm_names =
let val tuples = map (dest_tstp o tstp_line o explode) cnfs
+ and ctxt = ProofContext.init (Thm.theory_of_thm th)
+ (*The full context could be sent from ResAtp.isar_atp_body to Watcher.createWatcher,
+ then to setupWatcher and checkChildren...but is it really needed?*)
val decoded_tuples = decode_tstp_list (ProofContext.theory_of ctxt) tuples
+ val (ccls,fixes) = ResAxioms.neg_conjecture_clauses th sgno
+ val ccls = map forall_intr_vars ccls
val lines = foldr add_prfline [] decoded_tuples
- and fixes = foldr add_term_frees [] (map #3 decoded_tuples)
+ and clines = map (fn th => string_of_thm th ^ "\n") ccls
in
- isar_header fixes ^
- String.concat (isar_lines ctxt (stringify_deps thm_names [] lines))
+ isar_header (map #1 fixes) ^
+ String.concat (clines @ isar_lines ctxt (map prop_of ccls) (stringify_deps thm_names [] lines))
end;
(*Could use split_lines, but it can return blank lines...*)
@@ -413,12 +433,9 @@
fun tstp_extract proofextract probfile toParent ppid th sgno thm_names =
let val cnfs = filter (String.isPrefix "cnf(") (map nospaces (lines proofextract))
- and ctxt = ProofContext.init (Thm.theory_of_thm th)
- (*The full context could be sent from ResAtp.isar_atp_body to Watcher.createWatcher,
- then to setupWatcher and checkChildren...but is it needed?*)
in
signal_success probfile toParent ppid
- (decode_tstp_file ctxt (cnfs,thm_names))
+ (decode_tstp_file cnfs th sgno thm_names)
end;
--- a/src/HOL/ex/Classical.thy Thu Jan 04 17:52:28 2007 +0100
+++ b/src/HOL/ex/Classical.thy Thu Jan 04 17:55:12 2007 +0100
@@ -825,7 +825,7 @@
text{*A manual resolution proof of problem 19.*}
lemma "\<exists>x. \<forall>y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))"
-proof (rule ccontr, skolemize, make_clauses)
+proof (neg_clausify)
fix x
assume P: "\<And>U. P U"
and Q: "\<And>U. ~ Q U"
@@ -844,7 +844,7 @@
text{*Full single-step proof*}
lemma "\<And>S::'a set set. \<forall>x \<in> S. \<forall>y \<in> S. x \<subseteq> y \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
-proof (rule ccontr, skolemize, make_clauses)
+proof (neg_clausify)
fix S :: "'a set set"
assume CL1: "\<And>Z. ~ (S \<subseteq> {Z})"
and CL2: "\<And>X Y. X \<notin> S | Y \<notin> S | X \<subseteq> Y"
@@ -872,7 +872,7 @@
text{*Partially condensed proof*}
lemma singleton_example_1:
"\<And>S::'a set set. \<forall>x \<in> S. \<forall>y \<in> S. x \<subseteq> y \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
-proof (rule ccontr, skolemize, make_clauses)
+proof (neg_clausify)
fix S :: "'a set set"
assume CL1: "\<And>Z. ~ (S \<subseteq> {Z})"
and CL2: "\<And>X Y. X \<notin> S | Y \<notin> S | X \<subseteq> Y"
@@ -890,7 +890,7 @@
(**Not working: needs Metis
text{*More condensed proof*}
lemma "\<And>S::'a set set. \<forall>x \<in> S. \<forall>y \<in> S. x \<subseteq> y \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
-proof (rule ccontr, skolemize, make_clauses)
+proof (neg_clausify)
fix S :: "'a set set"
assume CL1: "\<And>Z. ~ (S \<subseteq> {Z})"
and CL2: "\<And>X Y. X \<notin> S | Y \<notin> S | X \<subseteq> Y"