merged
authorwenzelm
Fri Apr 23 19:36:23 2010 +0200 (2010-04-23)
changeset 36314cf1abb4daae6
parent 36313 f2753d6b0859
parent 36297 6b2b9516a3cd
child 36315 e859879079c8
merged
src/HOL/Tools/Sledgehammer/named_thm_set.ML
     1.1 --- a/src/HOL/HOL.thy	Fri Apr 23 19:32:37 2010 +0200
     1.2 +++ b/src/HOL/HOL.thy	Fri Apr 23 19:36:23 2010 +0200
     1.3 @@ -30,7 +30,6 @@
     1.4    ("~~/src/Tools/induct_tacs.ML")
     1.5    ("Tools/recfun_codegen.ML")
     1.6    "~~/src/Tools/more_conv.ML"
     1.7 -  "~~/src/HOL/Tools/Sledgehammer/named_thm_set.ML"
     1.8  begin
     1.9  
    1.10  setup {* Intuitionistic.method_setup @{binding iprover} *}
    1.11 @@ -801,7 +800,7 @@
    1.12  *}
    1.13  
    1.14  ML {*
    1.15 -structure No_ATPs = Named_Thm_Set
    1.16 +structure No_ATPs = Named_Thms
    1.17  (
    1.18    val name = "no_atp"
    1.19    val description = "theorems that should be filtered out by Sledgehammer"
     2.1 --- a/src/HOL/IsaMakefile	Fri Apr 23 19:32:37 2010 +0200
     2.2 +++ b/src/HOL/IsaMakefile	Fri Apr 23 19:36:23 2010 +0200
     2.3 @@ -136,7 +136,6 @@
     2.4    $(SRC)/Tools/random_word.ML \
     2.5    $(SRC)/Tools/value.ML \
     2.6    HOL.thy \
     2.7 -  Tools/Sledgehammer/named_thm_set.ML \
     2.8    Tools/hologic.ML \
     2.9    Tools/recfun_codegen.ML \
    2.10    Tools/simpdata.ML
     3.1 --- a/src/HOL/Tools/Sledgehammer/named_thm_set.ML	Fri Apr 23 19:32:37 2010 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,45 +0,0 @@
     3.4 -(*  Title:      HOL/Tools/Sledgehammer/named_thm_set.ML
     3.5 -    Author:     Makarius
     3.6 -    Author:     Jasmin Blanchette, TU Muenchen
     3.7 -
     3.8 -Named sets of theorems.
     3.9 -*)
    3.10 -
    3.11 -signature NAMED_THM_SET =
    3.12 -sig
    3.13 -  val member: Proof.context -> thm -> bool
    3.14 -  val add_thm: thm -> Context.generic -> Context.generic
    3.15 -  val del_thm: thm -> Context.generic -> Context.generic
    3.16 -  val add: attribute
    3.17 -  val del: attribute
    3.18 -  val setup: theory -> theory
    3.19 -end;
    3.20 -
    3.21 -functor Named_Thm_Set(val name: string val description: string)
    3.22 -        : NAMED_THM_SET =
    3.23 -struct
    3.24 -
    3.25 -structure Data = Generic_Data
    3.26 -(
    3.27 -  type T = thm Termtab.table;
    3.28 -  val empty = Termtab.empty;
    3.29 -  val extend = I;
    3.30 -  fun merge tabs = Termtab.merge (K true) tabs;
    3.31 -);
    3.32 -
    3.33 -fun member ctxt th =
    3.34 -  Termtab.defined (Data.get (Context.Proof ctxt)) (Thm.full_prop_of th);
    3.35 -
    3.36 -fun add_thm th = Data.map (Termtab.update (Thm.full_prop_of th, th));
    3.37 -fun del_thm th = Data.map (Termtab.delete_safe (Thm.full_prop_of th));
    3.38 -
    3.39 -val add = Thm.declaration_attribute add_thm;
    3.40 -val del = Thm.declaration_attribute del_thm;
    3.41 -
    3.42 -val setup =
    3.43 -  Attrib.setup (Binding.name name) (Attrib.add_del add del)
    3.44 -               ("declaration of " ^ description) #>
    3.45 -  PureThy.add_thms_dynamic (Binding.name name,
    3.46 -                            map #2 o Termtab.dest o Data.get);
    3.47 -
    3.48 -end;
     4.1 --- a/src/Pure/Tools/named_thms.ML	Fri Apr 23 19:32:37 2010 +0200
     4.2 +++ b/src/Pure/Tools/named_thms.ML	Fri Apr 23 19:36:23 2010 +0200
     4.3 @@ -6,6 +6,7 @@
     4.4  
     4.5  signature NAMED_THMS =
     4.6  sig
     4.7 +  val member: Proof.context -> thm -> bool
     4.8    val get: Proof.context -> thm list
     4.9    val add_thm: thm -> Context.generic -> Context.generic
    4.10    val del_thm: thm -> Context.generic -> Context.generic
    4.11 @@ -25,6 +26,8 @@
    4.12    val merge = Item_Net.merge;
    4.13  );
    4.14  
    4.15 +val member = Item_Net.member o Data.get o Context.Proof;
    4.16 +
    4.17  val content = Item_Net.content o Data.get;
    4.18  val get = content o Context.Proof;
    4.19  
     5.1 --- a/src/Pure/item_net.ML	Fri Apr 23 19:32:37 2010 +0200
     5.2 +++ b/src/Pure/item_net.ML	Fri Apr 23 19:36:23 2010 +0200
     5.3 @@ -11,6 +11,7 @@
     5.4    val init: ('a * 'a -> bool) -> ('a -> term list) -> 'a T
     5.5    val content: 'a T -> 'a list
     5.6    val retrieve: 'a T -> term -> 'a list
     5.7 +  val member: 'a T -> 'a -> bool
     5.8    val merge: 'a T * 'a T -> 'a T
     5.9    val remove: 'a -> 'a T -> 'a T
    5.10    val update: 'a -> 'a T -> 'a T
    5.11 @@ -49,7 +50,6 @@
    5.12    mk_items eq index (x :: content) (next - 1)
    5.13      (fold (fn t => Net.insert_term (K false) (t, (next, x))) (index x) net);
    5.14  
    5.15 -
    5.16  fun merge (items1, Items {content = content2, ...}) =
    5.17    fold_rev (fn y => if member items1 y then I else cons y) content2 items1;
    5.18