improvements to proof reconstruction. Some files loaded in a different order
authorpaulson
Thu Jan 04 17:55:12 2007 +0100 (2007-01-04)
changeset 219990cf192e489e2
parent 21998 aa2764dda077
child 22000 358525557580
improvements to proof reconstruction. Some files loaded in a different order
src/HOL/ATP_Linkup.thy
src/HOL/Hilbert_Choice.thy
src/HOL/Tools/meson.ML
src/HOL/Tools/res_atp.ML
src/HOL/Tools/res_axioms.ML
src/HOL/Tools/res_reconstruct.ML
src/HOL/ex/Classical.thy
     1.1 --- a/src/HOL/ATP_Linkup.thy	Thu Jan 04 17:52:28 2007 +0100
     1.2 +++ b/src/HOL/ATP_Linkup.thy	Thu Jan 04 17:55:12 2007 +0100
     1.3 @@ -11,11 +11,11 @@
     1.4  uses
     1.5    "Tools/polyhash.ML"
     1.6    "Tools/res_clause.ML"
     1.7 -  "Tools/res_reconstruct.ML"
     1.8 -  "Tools/ATP/watcher.ML"
     1.9    "Tools/ATP/reduce_axiomsN.ML"
    1.10    ("Tools/res_hol_clause.ML")
    1.11    ("Tools/res_axioms.ML")
    1.12 +  ("Tools/res_reconstruct.ML")
    1.13 +  ("Tools/ATP/watcher.ML")
    1.14    ("Tools/res_atp.ML")
    1.15    ("Tools/res_atp_provers.ML")
    1.16    ("Tools/res_atp_methods.ML")
    1.17 @@ -83,8 +83,10 @@
    1.18  lemma iff_negative: "~P | ~Q | P=Q"
    1.19  by blast
    1.20  
    1.21 -use "Tools/res_axioms.ML"
    1.22 -use "Tools/res_hol_clause.ML"
    1.23 +use "Tools/res_axioms.ML"      --{*requires the combinators declared above*}
    1.24 +use "Tools/res_hol_clause.ML"  --{*requires the combinators*}
    1.25 +use "Tools/res_reconstruct.ML"
    1.26 +use "Tools/ATP/watcher.ML"
    1.27  use "Tools/res_atp.ML"
    1.28  
    1.29  setup ResAxioms.meson_method_setup
     2.1 --- a/src/HOL/Hilbert_Choice.thy	Thu Jan 04 17:52:28 2007 +0100
     2.2 +++ b/src/HOL/Hilbert_Choice.thy	Thu Jan 04 17:55:12 2007 +0100
     2.3 @@ -620,10 +620,9 @@
     2.4  *}
     2.5  
     2.6  
     2.7 -subsection {* Meson method setup *}
     2.8 +subsection {* Meson package *}
     2.9  
    2.10  use "Tools/meson.ML"
    2.11 -setup Meson.skolemize_setup
    2.12  
    2.13  
    2.14  subsection {* Specification package -- Hilbertized version *}
     3.1 --- a/src/HOL/Tools/meson.ML	Thu Jan 04 17:52:28 2007 +0100
     3.2 +++ b/src/HOL/Tools/meson.ML	Thu Jan 04 17:55:12 2007 +0100
     3.3 @@ -36,7 +36,6 @@
     3.4    val negate_head	: thm -> thm
     3.5    val select_literal	: int -> thm -> thm
     3.6    val skolemize_tac	: int -> tactic
     3.7 -  val make_clauses_tac	: int -> tactic
     3.8  end
     3.9  
    3.10  
    3.11 @@ -646,34 +645,6 @@
    3.12    end
    3.13    handle Subscript => Seq.empty;
    3.14  
    3.15 -(*Top-level conversion to meta-level clauses. Each clause has  
    3.16 -  leading !!-bound universal variables, to express generality. To get 
    3.17 -  meta-clauses instead of disjunctions, uncomment "make_meta_clauses" below.*)
    3.18 -val make_clauses_tac = 
    3.19 -  SUBGOAL
    3.20 -    (fn (prop,_) =>
    3.21 -     let val ts = Logic.strip_assums_hyp prop
    3.22 -     in EVERY1 
    3.23 -	 [METAHYPS
    3.24 -	    (fn hyps => 
    3.25 -              (Method.insert_tac
    3.26 -                (map forall_intr_vars 
    3.27 -                  ( (**make_meta_clauses**) (make_clauses hyps))) 1)),
    3.28 -	  REPEAT_DETERM_N (length ts) o (etac thin_rl)]
    3.29 -     end);
    3.30 -     
    3.31 -     
    3.32 -(*** setup the special skoklemization methods ***)
    3.33 -
    3.34 -(*No CHANGED_PROP here, since these always appear in the preamble*)
    3.35 -
    3.36 -val skolemize_setup =
    3.37 -  Method.add_methods
    3.38 -    [("skolemize", Method.no_args (Method.SIMPLE_METHOD' skolemize_tac),
    3.39 -      "Skolemization into existential quantifiers"),
    3.40 -     ("make_clauses", Method.no_args (Method.SIMPLE_METHOD' make_clauses_tac), 
    3.41 -      "Conversion to !!-quantified meta-level clauses")];
    3.42 -
    3.43  end;
    3.44  
    3.45  structure BasicMeson: BASIC_MESON = Meson;
     4.1 --- a/src/HOL/Tools/res_atp.ML	Thu Jan 04 17:52:28 2007 +0100
     4.2 +++ b/src/HOL/Tools/res_atp.ML	Thu Jan 04 17:55:12 2007 +0100
     4.3 @@ -823,13 +823,6 @@
     4.4    let val path = File.explode_platform_path fname
     4.5    in  Vector.app (File.append path o (fn s => s ^ "\n"))  end;
     4.6  
     4.7 -(*Converting a subgoal into negated conjecture clauses*)
     4.8 -fun neg_clauses th n =
     4.9 -  let val tacs = [rtac ccontr, ObjectLogic.atomize_tac, skolemize_tac]
    4.10 -      val st = Seq.hd (EVERY' tacs n th)
    4.11 -      val negs = Option.valOf (metahyps_thms n st)
    4.12 -  in make_clauses negs |> ResAxioms.assume_abstract_list |> Meson.finish_cnf end;
    4.13 -
    4.14  (*We write out problem files for each subgoal. Argument probfile generates filenames,
    4.15    and allows the suppression of the suffix "_1" in problem-generation mode.
    4.16    FIXME: does not cope with &&, and it isn't easy because one could have multiple
    4.17 @@ -839,7 +832,8 @@
    4.18        val _ = Output.debug ("number of subgoals = " ^ Int.toString (length goals))
    4.19        val thy = ProofContext.theory_of ctxt
    4.20        fun get_neg_subgoals [] _ = []
    4.21 -        | get_neg_subgoals (gl::gls) n = neg_clauses th n :: get_neg_subgoals gls (n+1)
    4.22 +        | get_neg_subgoals (gl::gls) n = #1 (ResAxioms.neg_conjecture_clauses th n) :: 
    4.23 +                                         get_neg_subgoals gls (n+1)
    4.24        val goal_cls = get_neg_subgoals goals 1
    4.25        val logic = case !linkup_logic_mode of
    4.26                  Auto => problem_logic_goals (map ((map prop_of)) goal_cls)
     5.1 --- a/src/HOL/Tools/res_axioms.ML	Thu Jan 04 17:52:28 2007 +0100
     5.2 +++ b/src/HOL/Tools/res_axioms.ML	Thu Jan 04 17:55:12 2007 +0100
     5.3 @@ -18,8 +18,9 @@
     5.4    val meson_method_setup : theory -> theory
     5.5    val setup : theory -> theory
     5.6    val assume_abstract_list: thm list -> thm list
     5.7 -  val claset_rules_of: Proof.context -> (string * thm) list
     5.8 -  val simpset_rules_of: Proof.context -> (string * thm) list
     5.9 +  val neg_conjecture_clauses: thm -> int -> thm list * (string * typ) list
    5.10 +  val claset_rules_of: Proof.context -> (string * thm) list   (*FIXME DELETE*)
    5.11 +  val simpset_rules_of: Proof.context -> (string * thm) list  (*FIXME DELETE*)
    5.12    val atpset_rules_of: Proof.context -> (string * thm) list
    5.13  end;
    5.14  
    5.15 @@ -619,6 +620,32 @@
    5.16  val clausify = Attrib.syntax (Scan.lift Args.nat
    5.17    >> (fn i => Thm.rule_attribute (fn _ => fn th => clausify_rule (th, i))));
    5.18  
    5.19 +
    5.20 +(*** Converting a subgoal into negated conjecture clauses. ***)
    5.21 +
    5.22 +val neg_skolemize_tac = EVERY' [rtac ccontr, ObjectLogic.atomize_tac, skolemize_tac];
    5.23 +val neg_clausify = Meson.finish_cnf o assume_abstract_list o make_clauses;
    5.24 +
    5.25 +fun neg_conjecture_clauses st0 n =
    5.26 +  let val st = Seq.hd (neg_skolemize_tac n st0)
    5.27 +      val (params,_,_) = strip_context (Logic.nth_prem (n, Thm.prop_of st))
    5.28 +  in (neg_clausify (Option.valOf (metahyps_thms n st)), params) end;
    5.29 +
    5.30 +(*Conversion of a subgoal to conjecture clauses. Each clause has  
    5.31 +  leading !!-bound universal variables, to express generality. *)
    5.32 +val neg_clausify_tac = 
    5.33 +  neg_skolemize_tac THEN' 
    5.34 +  SUBGOAL
    5.35 +    (fn (prop,_) =>
    5.36 +     let val ts = Logic.strip_assums_hyp prop
    5.37 +     in EVERY1 
    5.38 +	 [METAHYPS
    5.39 +	    (fn hyps => 
    5.40 +              (Method.insert_tac
    5.41 +                (map forall_intr_vars (neg_clausify hyps)) 1)),
    5.42 +	  REPEAT_DETERM_N (length ts) o (etac thin_rl)]
    5.43 +     end);
    5.44 +
    5.45  (** The Skolemization attribute **)
    5.46  
    5.47  fun conj2_rule (th1,th2) = conjI OF [th1,th2];
    5.48 @@ -635,8 +662,12 @@
    5.49  
    5.50  val setup_attrs = Attrib.add_attributes
    5.51    [("skolem", Attrib.no_args skolem_attr, "skolemization of a theorem"),
    5.52 -   ("clausify", clausify, "conversion to clauses")];
    5.53 +   ("clausify", clausify, "conversion of theorem to clauses")];
    5.54 +
    5.55 +val setup_methods = Method.add_methods
    5.56 +  [("neg_clausify", Method.no_args (Method.SIMPLE_METHOD' neg_clausify_tac), 
    5.57 +    "conversion of goal to conjecture clauses")];
    5.58       
    5.59 -val setup = clause_cache_setup #> setup_attrs;
    5.60 +val setup = clause_cache_setup #> setup_attrs #> setup_methods;
    5.61  
    5.62  end;
     6.1 --- a/src/HOL/Tools/res_reconstruct.ML	Thu Jan 04 17:52:28 2007 +0100
     6.2 +++ b/src/HOL/Tools/res_reconstruct.ML	Thu Jan 04 17:55:12 2007 +0100
     6.3 @@ -3,8 +3,6 @@
     6.4      Copyright   2004  University of Cambridge
     6.5  *)
     6.6  
     6.7 -(*FIXME: can we delete the "thm * int" and "th sgno" below?*)
     6.8 -
     6.9  (***************************************************************************)
    6.10  (*  Code to deal with the transfer of proofs from a prover process         *)
    6.11  (***************************************************************************)
    6.12 @@ -322,10 +320,30 @@
    6.13    let val vt0 = tfree_constraints_of_clauses Vartab.empty (map #3 tuples)
    6.14    in  map (decode_tstp thy vt0) tuples  end;
    6.15  
    6.16 -fun isar_lines ctxt =
    6.17 +(*FIXME: simmilar function in res_atp. Move to HOLogic?*)
    6.18 +fun dest_disj_aux (Const ("op |", _) $ t $ t') disjs = dest_disj_aux t (dest_disj_aux t' disjs)
    6.19 +  | dest_disj_aux t disjs = t::disjs;
    6.20 +
    6.21 +fun dest_disj t = dest_disj_aux t [];
    6.22 +
    6.23 +val sort_lits = sort Term.fast_term_ord o dest_disj o HOLogic.dest_Trueprop o strip_all_body;
    6.24 +
    6.25 +fun permuted_clause t =
    6.26 +  let val lits = sort_lits t
    6.27 +      fun perm [] = NONE
    6.28 +        | perm (ctm::ctms) = 
    6.29 +            if forall (op aconv) (ListPair.zip (lits, sort_lits ctm)) then SOME ctm
    6.30 +            else perm ctms
    6.31 +  in perm end;
    6.32 +
    6.33 +(*ctms is a list of conjecture clauses as yielded by Isabelle. Those returned by the
    6.34 +  ATP may have their literals reordered.*)
    6.35 +fun isar_lines ctxt ctms =
    6.36    let val string_of = ProofContext.string_of_term ctxt
    6.37        fun doline hs (lname, t, []) =  (*No deps: it's a conjecture clause, with no proof.*)
    6.38 -            "assume " ^ lname ^ ": \"" ^ string_of t ^ "\"\n"
    6.39 +           (case permuted_clause t ctms of
    6.40 +                SOME u => "assume " ^ lname ^ ": \"" ^ string_of u ^ "\"\n"
    6.41 +              | NONE => "assume? " ^ lname ^ ": \"" ^ string_of t ^ "\"\n")  (*no match!!*)
    6.42          | doline hs (lname, t, deps) =
    6.43              hs ^ lname ^ ": \"" ^ string_of t ^ 
    6.44              "\"\n  by (meson " ^ space_implode " " deps ^ ")\n"
    6.45 @@ -364,7 +382,7 @@
    6.46                   (lno, t', deps) ::  (*replace later line by earlier one*)
    6.47                   (pre @ map (replace_deps (lno', [lno])) post));
    6.48  
    6.49 -(*Replace numeric proof lines by strings.*)
    6.50 +(*Replace numeric proof lines by strings, either from thm_names or sequential line numbers*)
    6.51  fun stringify_deps thm_names deps_map [] = []
    6.52    | stringify_deps thm_names deps_map ((lno, t, deps) :: lines) =
    6.53        if lno <= Vector.length thm_names  (*axiom*)
    6.54 @@ -377,22 +395,24 @@
    6.55                 stringify_deps thm_names ((lno,lname)::deps_map) lines
    6.56             end;
    6.57  
    6.58 -val proofstart = "\nproof (rule ccontr, skolemize, make_clauses)\n";
    6.59 -
    6.60 -fun string_of_Free (Free (x,_)) = x
    6.61 -  | string_of_Free _ = "??string_of_Free??";
    6.62 +val proofstart = "\nproof (neg_clausify)\n";
    6.63  
    6.64  fun isar_header [] = proofstart
    6.65 -  | isar_header ts = proofstart ^ "fix " ^ space_implode " " (map string_of_Free ts) ^ "\n";
    6.66 +  | isar_header ts = proofstart ^ "fix " ^ space_implode " " ts ^ "\n";
    6.67  
    6.68 -fun decode_tstp_file ctxt (cnfs,thm_names) =
    6.69 +fun decode_tstp_file cnfs th sgno thm_names =
    6.70    let val tuples = map (dest_tstp o tstp_line o explode) cnfs
    6.71 +      and ctxt = ProofContext.init (Thm.theory_of_thm th)
    6.72 +       (*The full context could be sent from ResAtp.isar_atp_body to Watcher.createWatcher,
    6.73 +         then to setupWatcher and checkChildren...but is it really needed?*)
    6.74        val decoded_tuples = decode_tstp_list (ProofContext.theory_of ctxt) tuples
    6.75 +      val (ccls,fixes) = ResAxioms.neg_conjecture_clauses th sgno
    6.76 +      val ccls = map forall_intr_vars ccls
    6.77        val lines = foldr add_prfline [] decoded_tuples
    6.78 -      and fixes = foldr add_term_frees [] (map #3 decoded_tuples)
    6.79 +      and clines = map (fn th => string_of_thm th ^ "\n") ccls
    6.80    in  
    6.81 -      isar_header fixes ^ 
    6.82 -      String.concat (isar_lines ctxt (stringify_deps thm_names [] lines))
    6.83 +      isar_header (map #1 fixes) ^ 
    6.84 +      String.concat (clines @ isar_lines ctxt (map prop_of ccls) (stringify_deps thm_names [] lines))
    6.85    end;
    6.86  
    6.87  (*Could use split_lines, but it can return blank lines...*)
    6.88 @@ -413,12 +433,9 @@
    6.89  
    6.90  fun tstp_extract proofextract probfile toParent ppid th sgno thm_names = 
    6.91    let val cnfs = filter (String.isPrefix "cnf(") (map nospaces (lines proofextract))
    6.92 -      and ctxt = ProofContext.init (Thm.theory_of_thm th)
    6.93 -       (*The full context could be sent from ResAtp.isar_atp_body to Watcher.createWatcher,
    6.94 -         then to setupWatcher and checkChildren...but is it needed?*)
    6.95    in  
    6.96      signal_success probfile toParent ppid 
    6.97 -      (decode_tstp_file ctxt (cnfs,thm_names))
    6.98 +      (decode_tstp_file cnfs th sgno thm_names)
    6.99    end;
   6.100  
   6.101  
     7.1 --- a/src/HOL/ex/Classical.thy	Thu Jan 04 17:52:28 2007 +0100
     7.2 +++ b/src/HOL/ex/Classical.thy	Thu Jan 04 17:55:12 2007 +0100
     7.3 @@ -825,7 +825,7 @@
     7.4  
     7.5  text{*A manual resolution proof of problem 19.*}
     7.6  lemma "\<exists>x. \<forall>y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))"
     7.7 -proof (rule ccontr, skolemize, make_clauses)
     7.8 +proof (neg_clausify)
     7.9    fix x
    7.10    assume P: "\<And>U. P U" 
    7.11       and Q: "\<And>U. ~ Q U"
    7.12 @@ -844,7 +844,7 @@
    7.13  
    7.14  text{*Full single-step proof*}
    7.15  lemma "\<And>S::'a set set. \<forall>x \<in> S. \<forall>y \<in> S. x \<subseteq> y \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
    7.16 -proof (rule ccontr, skolemize, make_clauses)
    7.17 +proof (neg_clausify)
    7.18    fix S :: "'a set set"
    7.19    assume CL1: "\<And>Z. ~ (S \<subseteq> {Z})"
    7.20       and CL2: "\<And>X Y. X \<notin> S | Y \<notin> S | X \<subseteq> Y"
    7.21 @@ -872,7 +872,7 @@
    7.22  text{*Partially condensed proof*}
    7.23  lemma singleton_example_1:
    7.24       "\<And>S::'a set set. \<forall>x \<in> S. \<forall>y \<in> S. x \<subseteq> y \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
    7.25 -proof (rule ccontr, skolemize, make_clauses)
    7.26 +proof (neg_clausify)
    7.27    fix S :: "'a set set"
    7.28    assume CL1: "\<And>Z. ~ (S \<subseteq> {Z})"
    7.29       and CL2: "\<And>X Y. X \<notin> S | Y \<notin> S | X \<subseteq> Y"
    7.30 @@ -890,7 +890,7 @@
    7.31  (**Not working: needs Metis
    7.32  text{*More condensed proof*}
    7.33  lemma "\<And>S::'a set set. \<forall>x \<in> S. \<forall>y \<in> S. x \<subseteq> y \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
    7.34 -proof (rule ccontr, skolemize, make_clauses)
    7.35 +proof (neg_clausify)
    7.36    fix S :: "'a set set"
    7.37    assume CL1: "\<And>Z. ~ (S \<subseteq> {Z})"
    7.38       and CL2: "\<And>X Y. X \<notin> S | Y \<notin> S | X \<subseteq> Y"