the "skolem" attribute and better initialization of the clause database
authorpaulson
Fri Dec 23 17:37:54 2005 +0100 (2005-12-23)
changeset 185100a6c24f549c3
parent 18509 d2d96f12a1fc
child 18511 beed2bc052a3
the "skolem" attribute and better initialization of the clause database
src/HOL/Main.thy
src/HOL/Tools/res_axioms.ML
     1.1 --- a/src/HOL/Main.thy	Fri Dec 23 17:36:00 2005 +0100
     1.2 +++ b/src/HOL/Main.thy	Fri Dec 23 17:37:54 2005 +0100
     1.3 @@ -18,11 +18,6 @@
     1.4    claset rules into the clause cache; cf.\ theory @{text
     1.5    Reconstruction}. *}
     1.6  
     1.7 -declare subset_refl [intro] 
     1.8 -  text {*Ensures that this important theorem is not superseded by the
     1.9 -         simplifier's "== True" version.*}
    1.10 -setup ResAxioms.clause_setup
    1.11 -declare subset_refl [rule del]
    1.12 -  text {*Removed again because it harms blast's performance.*}
    1.13 +setup ResAxioms.setup
    1.14  
    1.15  end
     2.1 --- a/src/HOL/Tools/res_axioms.ML	Fri Dec 23 17:36:00 2005 +0100
     2.2 +++ b/src/HOL/Tools/res_axioms.ML	Fri Dec 23 17:37:54 2005 +0100
     2.3 @@ -22,12 +22,13 @@
     2.4    val simpset_rules_of_ctxt : Proof.context -> (string * thm) list
     2.5    val clausify_rules_pairs : (string*thm) list -> (ResClause.clause*thm) list list
     2.6    val clausify_rules_pairsH : (string*thm) list -> (ResHolClause.clause*thm) list list
     2.7 -  val clause_setup : (theory -> theory) list
     2.8 -  val meson_method_setup : (theory -> theory) list
     2.9    val pairname : thm -> (string * thm)
    2.10 -  val cnf_axiom_aux : thm -> thm list
    2.11 +  val skolem_thm : thm -> thm list
    2.12    val cnf_rules1 : (string * thm) list -> string list -> (string * thm list) list * string list
    2.13    val cnf_rules2 : (string * thm) list -> string list -> (string * term list) list * string list
    2.14 +
    2.15 +  val meson_method_setup : (theory -> theory) list  (*Reconstruction.thy*)
    2.16 +  val setup : (theory -> theory) list               (*Main.thy*)
    2.17    end;
    2.18  
    2.19  structure ResAxioms : RES_AXIOMS =
    2.20 @@ -256,7 +257,8 @@
    2.21         |> ObjectLogic.atomize_thm |> make_nnf;
    2.22  
    2.23  (*The cache prevents repeated clausification of a theorem, 
    2.24 -  and also repeated declaration of Skolem functions*)  (* FIXME better use Termtab!? *)
    2.25 +  and also repeated declaration of Skolem functions*)  
    2.26 +  (* FIXME better use Termtab!? No, we MUST use theory data!!*)
    2.27  val clause_cache = ref (Symtab.empty : (thm * thm list) Symtab.table)
    2.28  
    2.29  
    2.30 @@ -264,15 +266,16 @@
    2.31  fun skolem_of_nnf th =
    2.32    map (skolem_of_def o assume o (cterm_of (theory_of_thm th))) (assume_skofuns th);
    2.33  
    2.34 -(*Skolemize a named theorem, returning a modified theory.*)
    2.35 +(*Skolemize a named theorem, with Skolem functions as additional premises.*)
    2.36  (*also works for HOL*) 
    2.37  fun skolem_thm th = 
    2.38 -  Option.map (fn nnfth => Meson.make_cnf (skolem_of_nnf nnfth) nnfth)
    2.39 -	 (SOME (to_nnf th)  handle THM _ => NONE);
    2.40 +  let val nnfth = to_nnf th
    2.41 +  in  Meson.make_cnf (skolem_of_nnf nnfth) nnfth
    2.42 +  end
    2.43 +  handle THM _ => [];
    2.44  
    2.45 -
    2.46 -(*Declare Skolem functions for a theorem, supplied in nnf and with its name*)
    2.47 -(*in case skolemization fails, the input theory is not changed*)
    2.48 +(*Declare Skolem functions for a theorem, supplied in nnf and with its name.
    2.49 +  It returns a modified theory, unless skolemization fails.*)
    2.50  fun skolem thy (name,th) =
    2.51    let val cname = (case name of "" => gensym "sko" | s => Sign.base_name s)
    2.52    in Option.map 
    2.53 @@ -283,20 +286,23 @@
    2.54        (SOME (to_nnf th)  handle THM _ => NONE) 
    2.55    end;
    2.56  
    2.57 -(*Populate the clause cache using the supplied theorems*)
    2.58 -fun skolem_cache ((name,th), thy) = 
    2.59 +(*Populate the clause cache using the supplied theorem. Return the clausal form
    2.60 +  and modified theory.*)
    2.61 +fun skolem_cache_thm ((name,th), thy) = 
    2.62    case Symtab.lookup (!clause_cache) name of
    2.63        NONE => 
    2.64  	(case skolem thy (name, Thm.transfer thy th) of
    2.65 -	     NONE => thy
    2.66 +	     NONE => ([th],thy)
    2.67  	   | SOME (thy',cls) => 
    2.68 -	       (change clause_cache (Symtab.update (name, (th, cls))); thy'))
    2.69 +	       (change clause_cache (Symtab.update (name, (th, cls))); (cls,thy')))
    2.70      | SOME (th',cls) =>
    2.71 -        if eq_thm(th,th') then thy
    2.72 +        if eq_thm(th,th') then (cls,thy)
    2.73  	else (warning ("skolem_cache: Ignoring variant of theorem " ^ name); 
    2.74  	      warning (string_of_thm th);
    2.75  	      warning (string_of_thm th');
    2.76 -	      thy);
    2.77 +	      ([th],thy));
    2.78 +	      
    2.79 +fun skolem_cache ((name,th), thy) = #2 (skolem_cache_thm ((name,th), thy));
    2.80  
    2.81  
    2.82  (*Exported function to convert Isabelle theorems into axiom clauses*) 
    2.83 @@ -317,12 +323,7 @@
    2.84  fun pairname th = (Thm.name_of_thm th, th);
    2.85  
    2.86  
    2.87 -(*no first-order check, so works for HOL too.*)
    2.88 -fun cnf_axiom_aux th = Option.getOpt (skolem_thm th, []);
    2.89 -
    2.90 -
    2.91 -
    2.92 -val cnf_axiom = cnf_axiom_g cnf_axiom_aux;
    2.93 +val cnf_axiom = cnf_axiom_g skolem_thm;
    2.94  
    2.95  
    2.96  fun meta_cnf_axiom th = 
    2.97 @@ -444,16 +445,22 @@
    2.98  
    2.99  val clausify_rules_pairsH = clausify_rules_pairs_auxH [];
   2.100  
   2.101 +(*These should include any plausibly-useful theorems, especially if they need
   2.102 +  Skolem functions. FIXME: this list is VERY INCOMPLETE*)
   2.103 +val default_initial_thms = map pairname
   2.104 +  [refl_def, antisym_def, sym_def, trans_def, single_valued_def,
   2.105 +   subset_refl, Union_least, Inter_greatest];
   2.106 +
   2.107  (*Setup function: takes a theory and installs ALL simprules and claset rules 
   2.108    into the clause cache*)
   2.109  fun clause_cache_setup thy =
   2.110    let val simps = simpset_rules_of_thy thy
   2.111        and clas  = claset_rules_of_thy thy
   2.112 -  in List.foldl skolem_cache (List.foldl skolem_cache thy clas) simps end;
   2.113 +      and thy0  = List.foldl skolem_cache thy default_initial_thms
   2.114 +      val thy1  = List.foldl skolem_cache thy0 clas
   2.115 +  in List.foldl skolem_cache thy1 simps end;
   2.116  (*Could be duplicate theorem names, due to multiple attributes*)
   2.117    
   2.118 -val clause_setup = [clause_cache_setup];  
   2.119 -
   2.120  
   2.121  (*** meson proof methods ***)
   2.122  
   2.123 @@ -468,4 +475,28 @@
   2.124    [("meson", Method.thms_ctxt_args meson_meth, 
   2.125      "The MESON resolution proof procedure")]];
   2.126  
   2.127 +
   2.128 +
   2.129 +(*** The Skolemization attribute ***)
   2.130 +
   2.131 +fun conj2_rule (th1,th2) = conjI OF [th1,th2];
   2.132 +
   2.133 +(*Conjoin a list of clauses to recreate a single theorem*)
   2.134 +val conj_rule = foldr1 conj2_rule;
   2.135 +
   2.136 +fun skolem_global_fun (thy, th) = 
   2.137 +  let val name = Thm.name_of_thm th
   2.138 +      val (cls,thy') = skolem_cache_thm ((name,th), thy)
   2.139 +  in  (thy', conj_rule cls)  end;
   2.140 +
   2.141 +val skolem_global = Attrib.no_args skolem_global_fun;
   2.142 +
   2.143 +fun skolem_local x = Attrib.no_args (Drule.rule_attribute (K (conj_rule o skolem_thm))) x;
   2.144 +
   2.145 +val setup_attrs = Attrib.add_attributes
   2.146 + [("skolem", (skolem_global, skolem_local),
   2.147 +    "skolemization of a theorem")];
   2.148 +
   2.149 +val setup = [clause_cache_setup, setup_attrs];
   2.150 +
   2.151  end;