Removal of the unused atpset concept, the atp attribute and some related code.
authorpaulson
Tue Oct 20 15:02:48 2009 +0100 (2009-10-20)
changeset 33022c95102496490
parent 33021 c065b9300d44
child 33023 207c21697a48
child 33044 fd0a9c794ec1
Removal of the unused atpset concept, the atp attribute and some related code.
src/HOL/HOL.thy
src/HOL/Set.thy
src/HOL/Tools/res_atp.ML
src/HOL/Tools/res_axioms.ML
     1.1 --- a/src/HOL/HOL.thy	Tue Oct 20 15:03:17 2009 +0200
     1.2 +++ b/src/HOL/HOL.thy	Tue Oct 20 15:02:48 2009 +0100
     1.3 @@ -839,9 +839,6 @@
     1.4  ML_Antiquote.value "claset"
     1.5    (Scan.succeed "Classical.claset_of (ML_Context.the_local_context ())");
     1.6  
     1.7 -structure ResAtpset = Named_Thms
     1.8 -  (val name = "atp" val description = "ATP rules");
     1.9 -
    1.10  structure ResBlacklist = Named_Thms
    1.11    (val name = "noatp" val description = "theorems blacklisted for ATP");
    1.12  *}
    1.13 @@ -860,7 +857,6 @@
    1.14    Hypsubst.hypsubst_setup
    1.15    #> ContextRules.addSWrapper (fn tac => hyp_subst_tac' ORELSE' tac)
    1.16    #> Classical.setup
    1.17 -  #> ResAtpset.setup
    1.18    #> ResBlacklist.setup
    1.19  end
    1.20  *}
     2.1 --- a/src/HOL/Set.thy	Tue Oct 20 15:03:17 2009 +0200
     2.2 +++ b/src/HOL/Set.thy	Tue Oct 20 15:02:48 2009 +0100
     2.3 @@ -445,7 +445,7 @@
     2.4  
     2.5  subsubsection {* Subsets *}
     2.6  
     2.7 -lemma subsetI [atp, intro!]: "(\<And>x. x \<in> A \<Longrightarrow> x \<in> B) \<Longrightarrow> A \<subseteq> B"
     2.8 +lemma subsetI [intro!]: "(\<And>x. x \<in> A \<Longrightarrow> x \<in> B) \<Longrightarrow> A \<subseteq> B"
     2.9    unfolding mem_def by (rule le_funI, rule le_boolI)
    2.10  
    2.11  text {*
    2.12 @@ -476,7 +476,7 @@
    2.13  lemma contra_subsetD: "A \<subseteq> B ==> c \<notin> B ==> c \<notin> A"
    2.14    by blast
    2.15  
    2.16 -lemma subset_refl [simp,atp]: "A \<subseteq> A"
    2.17 +lemma subset_refl [simp]: "A \<subseteq> A"
    2.18    by (fact order_refl)
    2.19  
    2.20  lemma subset_trans: "A \<subseteq> B ==> B \<subseteq> C ==> A \<subseteq> C"
     3.1 --- a/src/HOL/Tools/res_atp.ML	Tue Oct 20 15:03:17 2009 +0200
     3.2 +++ b/src/HOL/Tools/res_atp.ML	Tue Oct 20 15:02:48 2009 +0100
     3.3 @@ -38,8 +38,6 @@
     3.4  val pass_mark = 0.5;
     3.5  val convergence = 3.2;    (*Higher numbers allow longer inference chains*)
     3.6  val follow_defs = false;  (*Follow definitions. Makes problems bigger.*)
     3.7 -val include_all = true;
     3.8 -val include_atpset = true;
     3.9    
    3.10  (***************************************************************)
    3.11  (* Relevance Filtering                                         *)
    3.12 @@ -293,15 +291,14 @@
    3.13  
    3.14  (*** white list and black list of lemmas ***)
    3.15  
    3.16 -(*The rule subsetI is frequently omitted by the relevance filter. This could be theory data
    3.17 -  or identified with ATPset (which however is too big currently)*)
    3.18 +(*The rule subsetI is frequently omitted by the relevance filter.*)
    3.19  val whitelist_fo = [subsetI];
    3.20  (* ext has been a 'helper clause', always given to the atps.
    3.21    As such it was not passed to metis, but metis does not include ext (in contrast
    3.22    to the other helper_clauses *)
    3.23  val whitelist_ho = [ResHolClause.ext];
    3.24  
    3.25 -(*** retrieve lemmas from clasimpset and atpset, may filter them ***)
    3.26 +(*** retrieve lemmas and filter them ***)
    3.27  
    3.28  (*Hashing to detect duplicate and variant clauses, e.g. from the [iff] attribute*)
    3.29  
    3.30 @@ -405,18 +402,11 @@
    3.31        (warning ("No name for theorem " ^ Display.string_of_thm_without_context th); false)
    3.32    | check_named _ = true;
    3.33  
    3.34 -(* get lemmas from claset, simpset, atpset and extra supplied rules *)
    3.35 -fun get_clasimp_atp_lemmas ctxt =
    3.36 +fun get_all_lemmas ctxt =
    3.37    let val included_thms =
    3.38 -    if include_all
    3.39 -    then (tap (fn ths => ResAxioms.trace_msg
    3.40 -                 (fn () => ("Including all " ^ Int.toString (length ths) ^ " theorems")))
    3.41 -              (name_thm_pairs ctxt))
    3.42 -    else
    3.43 -    let val atpset_thms =
    3.44 -            if include_atpset then ResAxioms.atpset_rules_of ctxt
    3.45 -            else []
    3.46 -    in  atpset_thms  end
    3.47 +        tap (fn ths => ResAxioms.trace_msg
    3.48 +                     (fn () => ("Including all " ^ Int.toString (length ths) ^ " theorems")))
    3.49 +            (name_thm_pairs ctxt)
    3.50    in
    3.51      filter check_named included_thms
    3.52    end;
    3.53 @@ -524,7 +514,7 @@
    3.54    let
    3.55      val thy = ProofContext.theory_of ctxt
    3.56      val isFO = isFO thy goal_cls
    3.57 -    val included_thms = get_clasimp_atp_lemmas ctxt
    3.58 +    val included_thms = get_all_lemmas ctxt
    3.59      val included_cls = included_thms |> ResAxioms.cnf_rules_pairs thy |> make_unique
    3.60                                       |> restrict_to_logic thy isFO
    3.61                                       |> remove_unwanted_clauses
     4.1 --- a/src/HOL/Tools/res_axioms.ML	Tue Oct 20 15:03:17 2009 +0200
     4.2 +++ b/src/HOL/Tools/res_axioms.ML	Tue Oct 20 15:02:48 2009 +0100
     4.3 @@ -17,7 +17,6 @@
     4.4    val expand_defs_tac: thm -> tactic
     4.5    val combinators: thm -> thm
     4.6    val neg_conjecture_clauses: Proof.context -> thm -> int -> thm list * (string * typ) list
     4.7 -  val atpset_rules_of: Proof.context -> (string * thm) list
     4.8    val suppress_endtheory: bool Unsynchronized.ref
     4.9      (*for emergency use where endtheory causes problems*)
    4.10    val setup: theory -> theory
    4.11 @@ -378,8 +377,6 @@
    4.12  
    4.13  fun pairname th = (Thm.get_name_hint th, th);
    4.14  
    4.15 -fun atpset_rules_of ctxt = map pairname (ResAtpset.get ctxt);
    4.16 -
    4.17  
    4.18  (**** Translate a set of theorems into CNF ****)
    4.19