src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
changeset 37502 a8f7b25d5478
parent 37501 b5440c78ed3f
child 37503 c2dfa26b9da6
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Tue Jun 22 16:40:36 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Tue Jun 22 16:50:55 2010 +0200
     1.3 @@ -63,16 +63,6 @@
     1.4  val weight_fn = log_weight2;
     1.5  
     1.6  
     1.7 -(*Including equality in this list might be expected to stop rules like subset_antisym from
     1.8 -  being chosen, but for some reason filtering works better with them listed. The
     1.9 -  logical signs All, Ex, &, and --> are omitted because any remaining occurrrences
    1.10 -  must be within comprehensions.*)
    1.11 -val standard_consts =
    1.12 -  [@{const_name Trueprop}, @{const_name "==>"}, @{const_name all},
    1.13 -   @{const_name "=="}, @{const_name "op |"}, @{const_name Not},
    1.14 -   @{const_name "op ="}];
    1.15 -
    1.16 -
    1.17  (*** constants with types ***)
    1.18  
    1.19  (*An abstraction of Isabelle types*)
    1.20 @@ -105,29 +95,36 @@
    1.21  
    1.22  (*Add a const/type pair to the table, but a [] entry means a standard connective,
    1.23    which we ignore.*)
    1.24 -fun add_const_typ_table ((c,ctyps), tab) =
    1.25 -  Symtab.map_default (c, [ctyps]) (fn [] => [] | ctyps_list => insert (op =) ctyps ctyps_list) 
    1.26 -    tab;
    1.27 +fun add_const_type_to_table (c, ctyps) =
    1.28 +  Symtab.map_default (c, [ctyps])
    1.29 +                     (fn [] => [] | ctypss => insert (op =) ctyps ctypss)
    1.30  
    1.31  (*Free variables are included, as well as constants, to handle locales*)
    1.32 -fun add_term_consts_typs_rm thy (Const(c, typ), tab) =
    1.33 -      add_const_typ_table (const_with_typ thy (c,typ), tab) 
    1.34 -  | add_term_consts_typs_rm thy (Free(c, typ), tab) =
    1.35 -      add_const_typ_table (const_with_typ thy (c,typ), tab) 
    1.36 -  | add_term_consts_typs_rm _ (Const (@{const_name skolem_id}, _) $ _, tab) =
    1.37 -      tab
    1.38 -  | add_term_consts_typs_rm thy (t $ u, tab) =
    1.39 -      add_term_consts_typs_rm thy (t, add_term_consts_typs_rm thy (u, tab))
    1.40 -  | add_term_consts_typs_rm thy (Abs(_,_,t), tab) = add_term_consts_typs_rm thy (t, tab)
    1.41 -  | add_term_consts_typs_rm _ (_, tab) = tab;
    1.42 +fun add_term_consts_typs_rm thy (Const x) =
    1.43 +    add_const_type_to_table (const_with_typ thy x)
    1.44 +  | add_term_consts_typs_rm thy (Free x) =
    1.45 +    add_const_type_to_table (const_with_typ thy x)
    1.46 +  | add_term_consts_typs_rm _ (Const (@{const_name skolem_id}, _) $ _) = I
    1.47 +  | add_term_consts_typs_rm thy (t $ u) =
    1.48 +    add_term_consts_typs_rm thy t #> add_term_consts_typs_rm thy u
    1.49 +  | add_term_consts_typs_rm thy (Abs (_, _, t)) = add_term_consts_typs_rm thy t
    1.50 +  | add_term_consts_typs_rm _ _ = I
    1.51  
    1.52 -(*The empty list here indicates that the constant is being ignored*)
    1.53 -fun add_standard_const (s,tab) = Symtab.update (s,[]) tab;
    1.54 +
    1.55 +(* Including equality in this list might be expected to stop rules like
    1.56 +   subset_antisym from being chosen, but for some reason filtering works better
    1.57 +   with them listed. The logical signs All, Ex, &, and --> are omitted because
    1.58 +   any remaining occurrences must be within comprehensions. *)
    1.59 +val standard_consts =
    1.60 +  [@{const_name Trueprop}, @{const_name "==>"}, @{const_name all},
    1.61 +   @{const_name "=="}, @{const_name "op |"}, @{const_name Not},
    1.62 +   @{const_name "op ="}];
    1.63  
    1.64  val null_const_tab : const_typ list list Symtab.table = 
    1.65 -    List.foldl add_standard_const Symtab.empty standard_consts;
    1.66 +    fold (Symtab.update o rpair []) standard_consts Symtab.empty
    1.67  
    1.68 -fun get_goal_consts_typs thy = List.foldl (add_term_consts_typs_rm thy) null_const_tab;
    1.69 +fun get_goal_consts_typs thy goals =
    1.70 +  fold (add_term_consts_typs_rm thy) goals null_const_tab
    1.71  
    1.72  (*Inserts a dummy "constant" referring to the theory name, so that relevance
    1.73    takes the given theory into account.*)
    1.74 @@ -202,8 +199,9 @@
    1.75  fun add_expand_pairs (x,ys) xys = List.foldl (fn (y,acc) => (x,y)::acc) xys ys;
    1.76  
    1.77  fun consts_typs_of_term thy t = 
    1.78 -  let val tab = add_term_consts_typs_rm thy (t, null_const_tab)
    1.79 -  in  Symtab.fold add_expand_pairs tab []  end;
    1.80 +  let val tab = add_term_consts_typs_rm thy t null_const_tab in
    1.81 +    Symtab.fold add_expand_pairs tab []
    1.82 +  end
    1.83  
    1.84  fun pair_consts_typs_axiom theory_relevant thy (p as (thm, _)) =
    1.85    (p, (consts_typs_of_term thy (const_prop_of theory_relevant thm)));
    1.86 @@ -268,7 +266,7 @@
    1.87              let
    1.88                val (newrels, more_rejects) = take_best max_new newpairs
    1.89                val new_consts = maps #2 newrels
    1.90 -              val rel_consts' = List.foldl add_const_typ_table rel_consts new_consts
    1.91 +              val rel_consts' = fold add_const_type_to_table new_consts rel_consts
    1.92                val threshold =
    1.93                  threshold + (1.0 - threshold) / relevance_convergence
    1.94              in