killed legacy "neg_clausify" and "clausify"
authorblanchet
Wed Jun 23 09:40:06 2010 +0200 (2010-06-23)
changeset 3751126afa11a1fb2
parent 37510 6d9923e8d208
child 37512 ff72d3ddc898
killed legacy "neg_clausify" and "clausify"
src/HOL/Sledgehammer.thy
src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
     1.1 --- a/src/HOL/Sledgehammer.thy	Tue Jun 22 23:54:16 2010 +0200
     1.2 +++ b/src/HOL/Sledgehammer.thy	Wed Jun 23 09:40:06 2010 +0200
     1.3 @@ -110,7 +110,6 @@
     1.4  setup ATP_Systems.setup
     1.5  use "Tools/Sledgehammer/sledgehammer_fact_minimizer.ML"
     1.6  use "Tools/Sledgehammer/sledgehammer_isar.ML"
     1.7 -setup Sledgehammer_Isar.setup
     1.8  
     1.9  
    1.10  subsection {* The MESON prover *}
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Tue Jun 22 23:54:16 2010 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Wed Jun 23 09:40:06 2010 +0200
     2.3 @@ -22,11 +22,9 @@
     2.4    val cnf_rules_pairs : theory -> (string * thm) list -> cnf_thm list
     2.5    val saturate_skolem_cache: theory -> theory option
     2.6    val auto_saturate_skolem_cache: bool Unsynchronized.ref
     2.7 -    (* for emergency use where the Skolem cache causes problems *)
     2.8    val neg_clausify: thm -> thm list
     2.9    val neg_conjecture_clauses:
    2.10      Proof.context -> thm -> int -> thm list list * (string * typ) list
    2.11 -  val neg_clausify_tac: Proof.context -> int -> tactic
    2.12    val setup: theory -> theory
    2.13  end;
    2.14  
    2.15 @@ -522,6 +520,7 @@
    2.16  
    2.17  end;
    2.18  
    2.19 +(* For emergency use where the Skolem cache causes problems. *)
    2.20  val auto_saturate_skolem_cache = Unsynchronized.ref true
    2.21  
    2.22  fun conditionally_saturate_skolem_cache thy =
    2.23 @@ -547,20 +546,6 @@
    2.24        Subgoal.focus (Variable.set_body false ctxt) n st
    2.25    in (map neg_clausify prems, map (dest_Free o term_of o #2) params) end
    2.26  
    2.27 -(*Conversion of a subgoal to conjecture clauses. Each clause has
    2.28 -  leading !!-bound universal variables, to express generality. *)
    2.29 -fun neg_clausify_tac ctxt =
    2.30 -  neg_skolemize_tac ctxt THEN'
    2.31 -  SUBGOAL (fn (prop, i) =>
    2.32 -    let val ts = Logic.strip_assums_hyp prop in
    2.33 -      EVERY'
    2.34 -       [Subgoal.FOCUS
    2.35 -         (fn {prems, ...} =>
    2.36 -           (Method.insert_tac
    2.37 -             (map forall_intr_vars (maps neg_clausify prems)) i)) ctxt,
    2.38 -        REPEAT_DETERM_N (length ts) o etac thin_rl] i
    2.39 -     end);
    2.40 -
    2.41  
    2.42  (** setup **)
    2.43  
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Jun 22 23:54:16 2010 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Jun 23 09:40:06 2010 +0200
     3.3 @@ -12,7 +12,6 @@
     3.4    val timeout: int Unsynchronized.ref
     3.5    val full_types: bool Unsynchronized.ref
     3.6    val default_params : theory -> (string * string) list -> params
     3.7 -  val setup: theory -> theory
     3.8  end;
     3.9  
    3.10  structure Sledgehammer_Isar : SLEDGEHAMMER_ISAR =
    3.11 @@ -25,31 +24,6 @@
    3.12  open ATP_Systems
    3.13  open Sledgehammer_Fact_Minimizer
    3.14  
    3.15 -(** Proof method used in Isar proofs **)
    3.16 -
    3.17 -val neg_clausify_setup =
    3.18 -  Method.setup @{binding neg_clausify}
    3.19 -               (Scan.succeed (SIMPLE_METHOD' o neg_clausify_tac)
    3.20 -                o tap (fn _ => legacy_feature "Old 'neg_clausify' method -- \
    3.21 -                                   \rerun Sledgehammer to obtain a direct \
    3.22 -                                   \proof"))
    3.23 -               "conversion of goal to negated conjecture clauses (legacy)"
    3.24 -
    3.25 -(** Attribute for converting a theorem into clauses **)
    3.26 -
    3.27 -val parse_clausify_attribute : attribute context_parser =
    3.28 -  Scan.lift Parse.nat
    3.29 -  >> (fn i => Thm.rule_attribute (fn context => fn th =>
    3.30 -                  let val thy = Context.theory_of context in
    3.31 -                    Meson.make_meta_clause (nth (cnf_axiom thy th) i)
    3.32 -                  end))
    3.33 -
    3.34 -val clausify_setup =
    3.35 -  Attrib.setup @{binding clausify}
    3.36 -               (parse_clausify_attribute
    3.37 -                o tap (fn _ => legacy_feature "Old 'clausify' attribute"))
    3.38 -               "conversion of theorem to clauses"
    3.39 -
    3.40  (** Sledgehammer commands **)
    3.41  
    3.42  fun add_to_relevance_override ns : relevance_override =
    3.43 @@ -357,8 +331,4 @@
    3.44        "set and display the default parameters for Sledgehammer" Keyword.thy_decl
    3.45        parse_sledgehammer_params_command
    3.46  
    3.47 -val setup =
    3.48 -  neg_clausify_setup
    3.49 -  #> clausify_setup
    3.50 -
    3.51  end;