minor refactoring
authorblanchet
Tue Jul 27 19:41:19 2010 +0200 (2010-07-27)
changeset 3802822dcaec5fa77
parent 38027 505657ddb047
child 38029 479dfaae0b52
minor refactoring
src/HOL/Sledgehammer.thy
src/HOL/Tools/Sledgehammer/clausifier.ML
src/HOL/Tools/Sledgehammer/metis_clauses.ML
src/HOL/Tools/Sledgehammer/metis_tactics.ML
src/HOL/Tools/Sledgehammer/sledgehammer.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
     1.1 --- a/src/HOL/Sledgehammer.thy	Tue Jul 27 19:17:15 2010 +0200
     1.2 +++ b/src/HOL/Sledgehammer.thy	Tue Jul 27 19:41:19 2010 +0200
     1.3 @@ -1,6 +1,6 @@
     1.4  (*  Title:      HOL/Sledgehammer.thy
     1.5      Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
     1.6 -    Author:     Jia Meng, NICTA
     1.7 +    Author:     Jia Meng, Cambridge University Computer Laboratory and NICTA
     1.8      Author:     Fabian Immler, TU Muenchen
     1.9      Author:     Jasmin Blanchette, TU Muenchen
    1.10  *)
     2.1 --- a/src/HOL/Tools/Sledgehammer/clausifier.ML	Tue Jul 27 19:17:15 2010 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/clausifier.ML	Tue Jul 27 19:41:19 2010 +0200
     2.3 @@ -8,8 +8,8 @@
     2.4  signature CLAUSIFIER =
     2.5  sig
     2.6    val introduce_combinators_in_cterm : cterm -> thm
     2.7 +  val introduce_combinators_in_theorem : thm -> thm
     2.8    val cnf_axiom: theory -> thm -> thm list
     2.9 -  val neg_clausify: thm -> thm list
    2.10  end;
    2.11  
    2.12  structure Clausifier : CLAUSIFIER =
    2.13 @@ -251,16 +251,4 @@
    2.14  (* FIXME: is transfer necessary? *)
    2.15  fun cnf_axiom thy = skolemize_theorem thy o Thm.transfer thy
    2.16  
    2.17 -
    2.18 -(*** Converting a subgoal into negated conjecture clauses. ***)
    2.19 -
    2.20 -fun neg_skolemize_tac ctxt =
    2.21 -  EVERY' [rtac ccontr, Object_Logic.atomize_prems_tac, Meson.skolemize_tac ctxt]
    2.22 -
    2.23 -val neg_clausify =
    2.24 -  single
    2.25 -  #> Meson.make_clauses_unsorted
    2.26 -  #> map introduce_combinators_in_theorem
    2.27 -  #> Meson.finish_cnf
    2.28 -
    2.29  end;
     3.1 --- a/src/HOL/Tools/Sledgehammer/metis_clauses.ML	Tue Jul 27 19:17:15 2010 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/metis_clauses.ML	Tue Jul 27 19:41:19 2010 +0200
     3.3 @@ -15,10 +15,10 @@
     3.4    datatype arLit =
     3.5      TConsLit of name * name * name list |
     3.6      TVarLit of name * name
     3.7 -  datatype arity_clause = ArityClause of
     3.8 -   {axiom_name: string, conclLit: arLit, premLits: arLit list}
     3.9 -  datatype class_rel_clause = ClassRelClause of
    3.10 -   {axiom_name: string, subclass: name, superclass: name}
    3.11 +  datatype arity_clause =
    3.12 +    ArityClause of {axiom_name: string, conclLit: arLit, premLits: arLit list}
    3.13 +  datatype class_rel_clause =
    3.14 +    ClassRelClause of {axiom_name: string, subclass: name, superclass: name}
    3.15    datatype combtyp =
    3.16      CombTVar of name |
    3.17      CombTFree of name |
     4.1 --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Tue Jul 27 19:17:15 2010 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Tue Jul 27 19:41:19 2010 +0200
     4.3 @@ -775,6 +775,12 @@
     4.4  val type_has_top_sort =
     4.5    exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)
     4.6  
     4.7 +val neg_clausify =
     4.8 +  single
     4.9 +  #> Meson.make_clauses_unsorted
    4.10 +  #> map Clausifier.introduce_combinators_in_theorem
    4.11 +  #> Meson.finish_cnf
    4.12 +
    4.13  fun generic_metis_tac mode ctxt ths i st0 =
    4.14    let
    4.15      val _ = trace_msg (fn () =>
    4.16 @@ -783,7 +789,7 @@
    4.17      if exists_type type_has_top_sort (prop_of st0) then
    4.18        (warning ("Metis: Proof state contains the universal sort {}"); Seq.empty)
    4.19      else
    4.20 -      Meson.MESON (maps Clausifier.neg_clausify)
    4.21 +      Meson.MESON (maps neg_clausify)
    4.22                    (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1)
    4.23                    ctxt i st0
    4.24       handle ERROR msg => raise METIS ("generic_metis_tac", msg)
     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Jul 27 19:17:15 2010 +0200
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Jul 27 19:41:19 2010 +0200
     5.3 @@ -62,11 +62,11 @@
     5.4  structure Sledgehammer : SLEDGEHAMMER =
     5.5  struct
     5.6  
     5.7 +open ATP_Problem
     5.8 +open ATP_Systems
     5.9  open Metis_Clauses
    5.10  open Sledgehammer_Util
    5.11  open Sledgehammer_Fact_Filter
    5.12 -open ATP_Problem
    5.13 -open ATP_Systems
    5.14  open Sledgehammer_Proof_Reconstruct
    5.15  
    5.16  
     6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Jul 27 19:17:15 2010 +0200
     6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Jul 27 19:41:19 2010 +0200
     6.3 @@ -17,10 +17,10 @@
     6.4  structure Sledgehammer_Isar : SLEDGEHAMMER_ISAR =
     6.5  struct
     6.6  
     6.7 +open ATP_Systems
     6.8  open Sledgehammer_Util
     6.9  open Sledgehammer_Fact_Filter
    6.10  open Sledgehammer
    6.11 -open ATP_Systems
    6.12  open Sledgehammer_Fact_Minimizer
    6.13  
    6.14  (** Sledgehammer commands **)
     7.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Tue Jul 27 19:17:15 2010 +0200
     7.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Tue Jul 27 19:41:19 2010 +0200
     7.3 @@ -27,10 +27,10 @@
     7.4  structure Sledgehammer_Proof_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT =
     7.5  struct
     7.6  
     7.7 +open ATP_Problem
     7.8  open Metis_Clauses
     7.9  open Sledgehammer_Util
    7.10  open Sledgehammer_Fact_Filter
    7.11 -open ATP_Problem
    7.12  
    7.13  type minimize_command = string list -> string
    7.14