# HG changeset patch # User paulson # Date 1167929712 -3600 # Node ID 0cf192e489e2565cdc63e8e87d1b8e7cc770f6dd # Parent aa2764dda077f47c63eac69f7c229404b286ab9e improvements to proof reconstruction. Some files loaded in a different order diff -r aa2764dda077 -r 0cf192e489e2 src/HOL/ATP_Linkup.thy --- 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 diff -r aa2764dda077 -r 0cf192e489e2 src/HOL/Hilbert_Choice.thy --- 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 *} diff -r aa2764dda077 -r 0cf192e489e2 src/HOL/Tools/meson.ML --- 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; diff -r aa2764dda077 -r 0cf192e489e2 src/HOL/Tools/res_atp.ML --- 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) diff -r aa2764dda077 -r 0cf192e489e2 src/HOL/Tools/res_axioms.ML --- 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; diff -r aa2764dda077 -r 0cf192e489e2 src/HOL/Tools/res_reconstruct.ML --- 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; diff -r aa2764dda077 -r 0cf192e489e2 src/HOL/ex/Classical.thy --- 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 "\x. \y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))" -proof (rule ccontr, skolemize, make_clauses) +proof (neg_clausify) fix x assume P: "\U. P U" and Q: "\U. ~ Q U" @@ -844,7 +844,7 @@ text{*Full single-step proof*} lemma "\S::'a set set. \x \ S. \y \ S. x \ y \ \z. S \ {z}" -proof (rule ccontr, skolemize, make_clauses) +proof (neg_clausify) fix S :: "'a set set" assume CL1: "\Z. ~ (S \ {Z})" and CL2: "\X Y. X \ S | Y \ S | X \ Y" @@ -872,7 +872,7 @@ text{*Partially condensed proof*} lemma singleton_example_1: "\S::'a set set. \x \ S. \y \ S. x \ y \ \z. S \ {z}" -proof (rule ccontr, skolemize, make_clauses) +proof (neg_clausify) fix S :: "'a set set" assume CL1: "\Z. ~ (S \ {Z})" and CL2: "\X Y. X \ S | Y \ S | X \ Y" @@ -890,7 +890,7 @@ (**Not working: needs Metis text{*More condensed proof*} lemma "\S::'a set set. \x \ S. \y \ S. x \ y \ \z. S \ {z}" -proof (rule ccontr, skolemize, make_clauses) +proof (neg_clausify) fix S :: "'a set set" assume CL1: "\Z. ~ (S \ {Z})" and CL2: "\X Y. X \ S | Y \ S | X \ Y"