1.1 --- a/src/HOL/Tools/res_axioms.ML Mon Mar 19 15:57:20 2007 +0100
1.2 +++ b/src/HOL/Tools/res_axioms.ML Mon Mar 19 15:58:02 2007 +0100
1.3 @@ -415,8 +415,8 @@
1.4
1.5 (*The cache prevents repeated clausification of a theorem,
1.6 and also repeated declaration of Skolem functions*)
1.7 - (* FIXME better use Termtab!? No, we MUST use theory data!!*)
1.8 -val clause_cache = ref (Symtab.empty : (thm * thm list) Symtab.table)
1.9 + (* FIXME use theory data!!*)
1.10 +val clause_cache = ref (Thmtab.empty : thm list Thmtab.table)
1.11
1.12
1.13 (*Generate Skolem functions for a theorem supplied in nnf*)
1.14 @@ -466,9 +466,9 @@
1.15
1.16 (*Declare Skolem functions for a theorem, supplied in nnf and with its name.
1.17 It returns a modified theory, unless skolemization fails.*)
1.18 -fun skolem thy (name,th) =
1.19 - let val cname = (case name of "" => gensym "" | s => flatten_name s)
1.20 - val _ = Output.debug (fn () => "skolemizing " ^ name ^ ": ")
1.21 +fun skolem thy th =
1.22 + let val cname = (case PureThy.get_name_hint th of "" => gensym "" | s => flatten_name s)
1.23 + val _ = Output.debug (fn () => "skolemizing " ^ cname ^ ": ")
1.24 in Option.map
1.25 (fn nnfth =>
1.26 let val (thy',defs) = declare_skofuns cname nnfth thy
1.27 @@ -481,50 +481,31 @@
1.28
1.29 (*Populate the clause cache using the supplied theorem. Return the clausal form
1.30 and modified theory.*)
1.31 -fun skolem_cache_thm (name,th) thy =
1.32 - case Symtab.lookup (!clause_cache) name of
1.33 +fun skolem_cache_thm th thy =
1.34 + case Thmtab.lookup (!clause_cache) th of
1.35 NONE =>
1.36 - (case skolem thy (name, Thm.transfer thy th) of
1.37 + (case skolem thy (Thm.transfer thy th) of
1.38 NONE => ([th],thy)
1.39 | SOME (cls,thy') =>
1.40 - (if null cls then warning ("skolem_cache: empty clause set for " ^ name)
1.41 + (if null cls
1.42 + then warning ("skolem_cache: empty clause set for " ^ string_of_thm th)
1.43 else ();
1.44 - change clause_cache (Symtab.update (name, (th, cls)));
1.45 + change clause_cache (Thmtab.update (th, cls));
1.46 (cls,thy')))
1.47 - | SOME (th',cls) =>
1.48 - if Thm.eq_thm(th,th') then (cls,thy)
1.49 - else (Output.debug (fn () => "skolem_cache: Ignoring variant of theorem " ^ name);
1.50 - Output.debug (fn () => string_of_thm th);
1.51 - Output.debug (fn () => string_of_thm th');
1.52 - getOpt (skolem thy (name, Thm.transfer thy th), ([th],thy)));
1.53 + | SOME cls => (cls,thy);
1.54
1.55 (*Exported function to convert Isabelle theorems into axiom clauses*)
1.56 -fun cnf_axiom (name,th) =
1.57 - (Output.debug (fn () => "cnf_axiom called, theorem name = " ^ name);
1.58 - case name of
1.59 - "" => skolem_thm th (*no name, so can't cache*)
1.60 - | s => case Symtab.lookup (!clause_cache) s of
1.61 - NONE =>
1.62 - let val cls = map Goal.close_result (skolem_thm th)
1.63 - in Output.debug (fn () => "inserted into cache");
1.64 - change clause_cache (Symtab.update (s, (th, cls))); cls
1.65 - end
1.66 - | SOME(th',cls) =>
1.67 - if Thm.eq_thm(th,th') then cls
1.68 - else
1.69 - (Output.debug (fn () => "cnf_axiom: duplicate or variant of theorem " ^ name);
1.70 - Output.debug (fn () => string_of_thm th);
1.71 - Output.debug (fn () => string_of_thm th');
1.72 - skolem_thm th)
1.73 - );
1.74 +fun cnf_axiom th =
1.75 + case Thmtab.lookup (!clause_cache) th of
1.76 + NONE =>
1.77 + let val cls = map Goal.close_result (skolem_thm th)
1.78 + in Output.debug (fn () => "inserted into cache");
1.79 + change clause_cache (Thmtab.update (th, cls)); cls
1.80 + end
1.81 + | SOME cls => cls;
1.82
1.83 fun pairname th = (PureThy.get_name_hint th, th);
1.84
1.85 -(*Principally for debugging*)
1.86 -fun cnf_name s =
1.87 - let val th = thm s
1.88 - in cnf_axiom (PureThy.get_name_hint th, th) end;
1.89 -
1.90 (**** Extract and Clausify theorems from a theory's claset and simpset ****)
1.91
1.92 fun rules_of_claset cs =
1.93 @@ -551,20 +532,20 @@
1.94 fun atpset_rules_of ctxt = map pairname (ResAtpset.get_atpset ctxt);
1.95
1.96
1.97 -(**** Translate a set of classical/simplifier rules into CNF (still as type "thm") ****)
1.98 +(**** Translate a set of theorems into CNF ****)
1.99
1.100 (* classical rules: works for both FOL and HOL *)
1.101 fun cnf_rules [] err_list = ([],err_list)
1.102 | cnf_rules ((name,th) :: ths) err_list =
1.103 let val (ts,es) = cnf_rules ths err_list
1.104 - in (cnf_axiom (name,th) :: ts,es) handle _ => (ts, (th::es)) end;
1.105 + in (cnf_axiom th :: ts,es) handle _ => (ts, (th::es)) end;
1.106
1.107 fun pair_name_cls k (n, []) = []
1.108 | pair_name_cls k (n, cls::clss) = (cls, (n,k)) :: pair_name_cls (k+1) (n, clss)
1.109
1.110 fun cnf_rules_pairs_aux pairs [] = pairs
1.111 | cnf_rules_pairs_aux pairs ((name,th)::ths) =
1.112 - let val pairs' = (pair_name_cls 0 (name, cnf_axiom(name,th))) @ pairs
1.113 + let val pairs' = (pair_name_cls 0 (name, cnf_axiom th)) @ pairs
1.114 handle THM _ => pairs | ResClause.CLAUSE _ => pairs
1.115 in cnf_rules_pairs_aux pairs' ths end;
1.116
1.117 @@ -576,7 +557,7 @@
1.118
1.119 (*Setup function: takes a theory and installs ALL known theorems into the clause cache*)
1.120
1.121 -fun skolem_cache (name,th) thy =
1.122 +fun skolem_cache th thy =
1.123 let val prop = Thm.prop_of th
1.124 in
1.125 if lambda_free prop
1.126 @@ -584,7 +565,7 @@
1.127 but there are problems with re-use of abstraction functions if we don't
1.128 do them now, even for monomorphic theorems.*)
1.129 then thy
1.130 - else #2 (skolem_cache_thm (name,th) thy)
1.131 + else #2 (skolem_cache_thm th thy)
1.132 end;
1.133
1.134 (*The cache can be kept smaller by augmenting the condition above with
1.135 @@ -592,16 +573,15 @@
1.136 However, while this step does not reduce the time needed to build HOL,
1.137 it doubles the time taken by the first call to the ATP link-up.*)
1.138
1.139 -fun clause_cache_setup thy = fold skolem_cache (PureThy.all_thms_of thy) thy;
1.140 +fun clause_cache_setup thy = fold skolem_cache (map #2 (PureThy.all_thms_of thy)) thy;
1.141
1.142
1.143 (*** meson proof methods ***)
1.144
1.145 fun skolem_use_cache_thm th =
1.146 - case Symtab.lookup (!clause_cache) (PureThy.get_name_hint th) of
1.147 + case Thmtab.lookup (!clause_cache) th of
1.148 NONE => skolem_thm th
1.149 - | SOME (th',cls) =>
1.150 - if Thm.eq_thm(th,th') then cls else skolem_thm th;
1.151 + | SOME cls => cls;
1.152
1.153 fun cnf_rules_of_ths ths = List.concat (map skolem_use_cache_thm ths);
1.154
1.155 @@ -612,7 +592,7 @@
1.156
1.157 (** Attribute for converting a theorem into clauses **)
1.158
1.159 -fun meta_cnf_axiom th = map Meson.make_meta_clause (cnf_axiom (pairname th));
1.160 +fun meta_cnf_axiom th = map Meson.make_meta_clause (cnf_axiom th);
1.161
1.162 fun clausify_rule (th,i) = List.nth (meta_cnf_axiom th, i)
1.163
1.164 @@ -623,7 +603,10 @@
1.165 (*** Converting a subgoal into negated conjecture clauses. ***)
1.166
1.167 val neg_skolemize_tac = EVERY' [rtac ccontr, ObjectLogic.atomize_tac, skolemize_tac];
1.168 -val neg_clausify = Meson.finish_cnf o assume_abstract_list o make_clauses;
1.169 +
1.170 +(*finish_cnf removes tautologies and functional reflexivity axioms, but by calling Thm.varifyT
1.171 + it can introduce TVars, which we don't want in conjecture clauses.*)
1.172 +val neg_clausify = map Thm.freezeT o Meson.finish_cnf o assume_abstract_list o make_clauses;
1.173
1.174 fun neg_conjecture_clauses st0 n =
1.175 let val st = Seq.hd (neg_skolemize_tac n st0)
1.176 @@ -654,8 +637,7 @@
1.177 | conj_rule ths = foldr1 conj2_rule ths;
1.178
1.179 fun skolem_attr (Context.Theory thy, th) =
1.180 - let val name = PureThy.get_name_hint th
1.181 - val (cls, thy') = skolem_cache_thm (name, th) thy
1.182 + let val (cls, thy') = skolem_cache_thm th thy
1.183 in (Context.Theory thy', conj_rule cls) end
1.184 | skolem_attr (context, th) = (context, conj_rule (skolem_use_cache_thm th));
1.185