--- a/src/HOL/Tools/res_axioms.ML Thu Jun 12 22:29:50 2008 +0200
+++ b/src/HOL/Tools/res_axioms.ML Thu Jun 12 22:29:51 2008 +0200
@@ -9,7 +9,7 @@
sig
val cnf_axiom: theory -> thm -> thm list
val pairname: thm -> string * thm
- val multi_base_blacklist: string list
+ val multi_base_blacklist: string list
val bad_for_atp: thm -> bool
val type_has_empty_sort: typ -> bool
val cnf_rules_pairs: theory -> (string * thm) list -> (thm * (string * int)) list
@@ -20,8 +20,6 @@
val claset_rules_of: Proof.context -> (string * thm) list (*FIXME DELETE*)
val simpset_rules_of: Proof.context -> (string * thm) list (*FIXME DELETE*)
val atpset_rules_of: Proof.context -> (string * thm) list
- val meson_method_setup: theory -> theory
- val clause_cache_endtheory: theory -> theory option
val suppress_endtheory: bool ref (*for emergency use where endtheory causes problems*)
val setup: theory -> theory
end;
@@ -36,7 +34,7 @@
| type_has_empty_sort (TVar (_, [])) = true
| type_has_empty_sort (Type (_, Ts)) = exists type_has_empty_sort Ts
| type_has_empty_sort _ = false;
-
+
(**** Transformation of Elimination Rules into First-Order Formulas****)
val cfalse = cterm_of HOL.thy HOLogic.false_const;
@@ -161,15 +159,9 @@
val monomorphic = not o Term.exists_type (Term.exists_subtype Term.is_TVar);
-val abs_S = @{thm"abs_S"};
-val abs_K = @{thm"abs_K"};
-val abs_I = @{thm"abs_I"};
-val abs_B = @{thm"abs_B"};
-val abs_C = @{thm"abs_C"};
-
-val [f_B,g_B] = map (cterm_of @{theory}) (term_vars (prop_of abs_B));
-val [g_C,f_C] = map (cterm_of @{theory}) (term_vars (prop_of abs_C));
-val [f_S,g_S] = map (cterm_of @{theory}) (term_vars (prop_of abs_S));
+val [f_B,g_B] = map (cterm_of @{theory}) (term_vars (prop_of @{thm abs_B}));
+val [g_C,f_C] = map (cterm_of @{theory}) (term_vars (prop_of @{thm abs_C}));
+val [f_S,g_S] = map (cterm_of @{theory}) (term_vars (prop_of @{thm abs_S}));
(*FIXME: requires more use of cterm constructors*)
fun abstract ct =
@@ -178,37 +170,37 @@
val thy = theory_of_cterm ct
val Type("fun",[xT,bodyT]) = typ_of (ctyp_of_term ct)
val cxT = ctyp_of thy xT and cbodyT = ctyp_of thy bodyT
- fun makeK() = instantiate' [SOME cxT, SOME cbodyT] [SOME (cterm_of thy body)] abs_K
+ fun makeK() = instantiate' [SOME cxT, SOME cbodyT] [SOME (cterm_of thy body)] @{thm abs_K}
in
case body of
Const _ => makeK()
| Free _ => makeK()
| Var _ => makeK() (*though Var isn't expected*)
- | Bound 0 => instantiate' [SOME cxT] [] abs_I (*identity: I*)
+ | Bound 0 => instantiate' [SOME cxT] [] @{thm abs_I} (*identity: I*)
| rator$rand =>
- if loose_bvar1 (rator,0) then (*C or S*)
+ if loose_bvar1 (rator,0) then (*C or S*)
if loose_bvar1 (rand,0) then (*S*)
let val crator = cterm_of thy (Abs(x,xT,rator))
val crand = cterm_of thy (Abs(x,xT,rand))
- val abs_S' = cterm_instantiate [(f_S,crator),(g_S,crand)] abs_S
- val (_,rhs) = Thm.dest_equals (cprop_of abs_S')
+ val abs_S' = cterm_instantiate [(f_S,crator),(g_S,crand)] @{thm abs_S}
+ val (_,rhs) = Thm.dest_equals (cprop_of abs_S')
in
Thm.transitive abs_S' (Conv.binop_conv abstract rhs)
end
else (*C*)
let val crator = cterm_of thy (Abs(x,xT,rator))
- val abs_C' = cterm_instantiate [(f_C,crator),(g_C,cterm_of thy rand)] abs_C
- val (_,rhs) = Thm.dest_equals (cprop_of abs_C')
+ val abs_C' = cterm_instantiate [(f_C,crator),(g_C,cterm_of thy rand)] @{thm abs_C}
+ val (_,rhs) = Thm.dest_equals (cprop_of abs_C')
in
Thm.transitive abs_C' (Conv.fun_conv (Conv.arg_conv abstract) rhs)
end
- else if loose_bvar1 (rand,0) then (*B or eta*)
+ else if loose_bvar1 (rand,0) then (*B or eta*)
if rand = Bound 0 then eta_conversion ct
else (*B*)
let val crand = cterm_of thy (Abs(x,xT,rand))
val crator = cterm_of thy rator
- val abs_B' = cterm_instantiate [(f_B,crator),(g_B,crand)] abs_B
- val (_,rhs) = Thm.dest_equals (cprop_of abs_B')
+ val abs_B' = cterm_instantiate [(f_B,crator),(g_B,crand)] @{thm abs_B}
+ val (_,rhs) = Thm.dest_equals (cprop_of abs_B')
in
Thm.transitive abs_B' (Conv.arg_conv abstract rhs)
end
@@ -235,16 +227,16 @@
| t1 $ t2 =>
let val (ct1,ct2) = Thm.dest_comb ct
in combination (combinators_aux ct1) (combinators_aux ct2) end;
-
+
fun combinators th =
- if lambda_free (prop_of th) then th
+ if lambda_free (prop_of th) then th
else
let val _ = Output.debug (fn()=>"Conversion to combinators: " ^ Display.string_of_thm th);
val th = Drule.eta_contraction_rule th
val eqth = combinators_aux (cprop_of th)
val _ = Output.debug (fn()=>"Conversion result: " ^ Display.string_of_thm eqth);
in equal_elim eqth th end
- handle THM (msg,_,_) =>
+ handle THM (msg,_,_) =>
(warning ("Error in the combinator translation of " ^ Display.string_of_thm th);
warning (" Exception message: " ^ msg);
TrueI); (*A type variable of sort {} will cause make abstraction fail.*)
@@ -287,7 +279,7 @@
(*Converts an Isabelle theorem (intro, elim or simp format, even higher-order) into NNF.*)
fun to_nnf th ctxt0 =
let val th1 = th |> transform_elim |> zero_var_indexes
- val ((_,[th2]),ctxt) = Variable.import_thms false [th1] ctxt0
+ val ((_,[th2]),ctxt) = Variable.import_thms true [th1] ctxt0
val th3 = th2 |> Conv.fconv_rule ObjectLogic.atomize |> Meson.make_nnf |> strip_lambdas ~1
in (th3, ctxt) end;
@@ -301,10 +293,10 @@
| ths' => error (msg ^ "\n" ^ cat_lines (map Display.string_of_thm ths'));
-(*** Blacklisting (duplicated in ResAtp? ***)
+(*** Blacklisting (duplicated in ResAtp?) ***)
val max_lambda_nesting = 3;
-
+
fun excessive_lambdas (f$t, k) = excessive_lambdas (f,k) orelse excessive_lambdas (t,k)
| excessive_lambdas (Abs(_,_,t), k) = k=0 orelse excessive_lambdas (t,k-1)
| excessive_lambdas _ = false;
@@ -320,25 +312,25 @@
(*The max apply_depth of any metis call in MetisExamples (on 31-10-2007) was 11.*)
val max_apply_depth = 15;
-
+
fun apply_depth (f$t) = Int.max (apply_depth f, apply_depth t + 1)
| apply_depth (Abs(_,_,t)) = apply_depth t
| apply_depth _ = 0;
-fun too_complex t =
- apply_depth t > max_apply_depth orelse
+fun too_complex t =
+ apply_depth t > max_apply_depth orelse
Meson.too_many_clauses NONE t orelse
excessive_lambdas_fm [] t;
-
+
fun is_strange_thm th =
case head_of (concl_of th) of
Const (a,_) => (a <> "Trueprop" andalso a <> "==")
| _ => false;
-fun bad_for_atp th =
- PureThy.is_internal th
- orelse too_complex (prop_of th)
- orelse exists_type type_has_empty_sort (prop_of th)
+fun bad_for_atp th =
+ PureThy.is_internal th
+ orelse too_complex (prop_of th)
+ orelse exists_type type_has_empty_sort (prop_of th)
orelse is_strange_thm th;
val multi_base_blacklist =
@@ -356,78 +348,66 @@
if PureThy.has_name_hint th then PureThy.get_name_hint th
else Display.string_of_thm th;
+(*Skolemize a named theorem, with Skolem functions as additional premises.*)
+fun skolem_thm (s, th) =
+ if member (op =) multi_base_blacklist (Sign.base_name s) orelse bad_for_atp th then []
+ else
+ let
+ val ctxt0 = Variable.thm_context th
+ val (nnfth, ctxt1) = to_nnf th ctxt0
+ val (cnfs, ctxt2) = Meson.make_cnf (assume_skolem_of_def s nnfth) nnfth ctxt1
+ in cnfs |> map combinators |> Variable.export ctxt2 ctxt0 |> Meson.finish_cnf end
+ handle THM _ => [];
+
(*Declare Skolem functions for a theorem, supplied in nnf and with its name.
It returns a modified theory, unless skolemization fails.*)
-fun skolem th0 thy =
+fun skolem (name, th0) thy =
let
val th = Thm.transfer thy th0
val ctxt0 = Variable.thm_context th
- val _ = Output.debug (fn () => "skolemizing " ^ name_or_string th)
in
- Option.map
- (fn (nnfth,ctxt1) =>
- let
- val _ = Output.debug (fn () => " initial nnf: " ^ Display.string_of_thm nnfth)
- val s = fake_name th
- val (defs,thy') = declare_skofuns s nnfth thy
- val (cnfs,ctxt2) = Meson.make_cnf (map skolem_of_def defs) nnfth ctxt1
- val _ = Output.debug (fn () => Int.toString (length cnfs) ^ " clauses yielded")
- val cnfs' = cnfs |> map combinators |> Variable.export ctxt2 ctxt0
- |> Meson.finish_cnf |> map Thm.close_derivation
- in (cnfs', thy') end
- handle Clausify_failure thy_e => ([],thy_e)
- )
- (try (to_nnf th) ctxt0)
+ try (to_nnf th) ctxt0 |> Option.map (fn (nnfth, ctxt1) =>
+ let
+ val s = flatten_name name
+ val (defs, thy') = declare_skofuns s nnfth thy
+ val (cnfs, ctxt2) = Meson.make_cnf (map skolem_of_def defs) nnfth ctxt1
+ val cnfs' = cnfs |> map combinators |> Variable.export ctxt2 ctxt0
+ |> Meson.finish_cnf |> map Thm.close_derivation
+ in (cnfs', thy') end
+ handle Clausify_failure thy_e => ([], thy_e)) (* FIXME !? *)
end;
(*The cache prevents repeated clausification of a theorem, and also repeated declaration of
Skolem functions.*)
structure ThmCache = TheoryDataFun
(
- type T = thm list Thmtab.table;
- val empty = Thmtab.empty;
+ type T = thm list Thmtab.table * unit Symtab.table
+ val empty = (Thmtab.empty, Symtab.empty)
val copy = I;
val extend = I;
- fun merge _ tabs : T = Thmtab.merge (K true) tabs;
+ fun merge _ ((cache1, seen1), (cache2, seen2)) : T =
+ (Thmtab.merge (K true) (cache1, cache2), Symtab.merge (K true) (seen1, seen2));
);
-(*Populate the clause cache using the supplied theorem. Return the clausal form
- and modified theory.*)
-fun skolem_cache_thm th thy =
- case Thmtab.lookup (ThmCache.get thy) th of
- NONE =>
- (case skolem th thy of
- NONE => ([th],thy)
- | SOME (cls,thy') =>
- (Output.debug (fn () => "skolem_cache_thm: " ^ Int.toString (length cls) ^
- " clauses inserted into cache: " ^ name_or_string th);
- (cls, ThmCache.map (Thmtab.update (th,cls)) thy')))
- | SOME cls => (cls,thy);
+val lookup_cache = Thmtab.lookup o #1 o ThmCache.get;
+val already_seen = Symtab.defined o #2 o ThmCache.get;
-(*Skolemize a named theorem, with Skolem functions as additional premises.*)
-fun skolem_thm (s,th) =
- if (Sign.base_name s) mem_string multi_base_blacklist orelse bad_for_atp th then []
- else
- let val ctxt0 = Variable.thm_context th
- val (nnfth,ctxt1) = to_nnf th ctxt0
- val (cnfs,ctxt2) = Meson.make_cnf (assume_skolem_of_def s nnfth) nnfth ctxt1
- in cnfs |> map combinators |> Variable.export ctxt2 ctxt0 |> Meson.finish_cnf end
- handle THM _ => [];
+val update_cache = ThmCache.map o apfst o Thmtab.update;
+fun mark_seen name = ThmCache.map (apsnd (Symtab.update (name, ())));
(*Exported function to convert Isabelle theorems into axiom clauses*)
fun cnf_axiom thy th0 =
- let val th = Thm.transfer thy th0
- in
- case Thmtab.lookup (ThmCache.get thy) th of
- NONE => (Output.debug (fn () => "cnf_axiom: " ^ name_or_string th);
- map Thm.close_derivation (skolem_thm (fake_name th, th)))
- | SOME cls => cls
+ let val th = Thm.transfer thy th0 in
+ case lookup_cache thy th of
+ NONE => map Thm.close_derivation (skolem_thm (fake_name th, th))
+ | SOME cls => cls
end;
-fun pairname th = (PureThy.get_name_hint th, th);
(**** Extract and Clausify theorems from a theory's claset and simpset ****)
+fun pairname th = (PureThy.get_name_hint th, th);
+
fun rules_of_claset cs =
let val {safeIs,safeEs,hazIs,hazEs,...} = rep_cs cs
val intros = safeIs @ hazIs
@@ -467,35 +447,41 @@
fun cnf_rules_pairs thy l = cnf_rules_pairs_aux thy [] (rev l);
-(**** Convert all theorems of a claset/simpset into clauses (ResClause.clause, or ResHolClause.clause) ****)
+(**** Convert all facts of the theory into clauses (ResClause.clause, or ResHolClause.clause) ****)
-(*Setup function: takes a theory and installs ALL known theorems into the clause cache*)
-
-val mark_skolemized = Sign.add_consts_i [("ResAxioms_endtheory", HOLogic.boolT, NoSyn)];
+(*Populate the clause cache using the supplied theorem. Return the clausal form
+ and modified theory.*)
+fun skolem_cache_thm (name, th) thy =
+ if bad_for_atp th then thy
+ else
+ (case lookup_cache thy th of
+ SOME _ => thy
+ | NONE =>
+ (case skolem (name, th) thy of
+ NONE => thy
+ | SOME (cls, thy') => update_cache (th, cls) thy'));
-fun skolem_cache th thy =
- if bad_for_atp th then thy else #2 (skolem_cache_thm th thy);
+fun skolem_cache_fact (name, ths) (changed, thy) =
+ if (Sign.base_name name) mem_string multi_base_blacklist orelse already_seen thy name
+ then (changed, thy)
+ else (true, thy |> mark_seen name |> fold skolem_cache_thm (PureThy.name_multi name ths));
-fun skolem_cache_list (a,ths) thy =
- if (Sign.base_name a) mem_string multi_base_blacklist then thy
- else fold skolem_cache ths thy;
+fun saturate_skolem_cache thy =
+ (case Facts.fold_static skolem_cache_fact (PureThy.facts_of thy) (false, thy) of
+ (false, _) => NONE
+ | (true, thy') => SOME thy');
+
-val skolem_cache_theorems_of = Symtab.fold skolem_cache_list o #2 o PureThy.theorems_of;
-fun skolem_cache_node thy = skolem_cache_theorems_of thy thy;
-fun skolem_cache_all thy = fold skolem_cache_theorems_of (thy :: Theory.ancestors_of thy) thy;
+val suppress_endtheory = ref false;
+
+fun clause_cache_endtheory thy =
+ if ! suppress_endtheory then NONE
+ else saturate_skolem_cache thy;
+
(*The cache can be kept smaller by inspecting the prop of each thm. Can ignore all that are
lambda_free, but then the individual theory caches become much bigger.*)
-val suppress_endtheory = ref false;
-
-(*The new constant is a hack to prevent multiple execution*)
-fun clause_cache_endtheory thy =
- if !suppress_endtheory then NONE
- else
- (Output.debug (fn () => "RexAxioms end theory action: " ^ Context.str_of_thy thy);
- Option.map skolem_cache_node (try mark_skolemized thy) );
-
(*** meson proof methods ***)
@@ -538,13 +524,6 @@
"MESON resolution proof procedure")];
-(** Attribute for converting a theorem into clauses **)
-
-val clausify = Attrib.syntax (Scan.lift Args.nat
- >> (fn i => Thm.rule_attribute (fn context => fn th =>
- Meson.make_meta_clause (nth (cnf_axiom (Context.theory_of context) th) i))));
-
-
(*** Converting a subgoal into negated conjecture clauses. ***)
val neg_skolemize_tac = EVERY' [rtac ccontr, ObjectLogic.atomize_prems_tac, Meson.skolemize_tac];
@@ -573,28 +552,30 @@
REPEAT_DETERM_N (length ts) o (etac thin_rl)]
end);
-
-(** The Skolemization attribute **)
-
-fun conj2_rule (th1,th2) = conjI OF [th1,th2];
-
-(*Conjoin a list of theorems to form a single theorem*)
-fun conj_rule [] = TrueI
- | conj_rule ths = foldr1 conj2_rule ths;
-
-fun skolem_attr (Context.Theory thy, th) =
- let val (cls, thy') = skolem_cache_thm th thy
- in (Context.Theory thy', conj_rule cls) end
- | skolem_attr (context, th) = (context, th)
-
-val setup_attrs = Attrib.add_attributes
- [("skolem", Attrib.no_args skolem_attr, "skolemization of a theorem"),
- ("clausify", clausify, "conversion of theorem to clauses")];
-
val setup_methods = Method.add_methods
[("neg_clausify", Method.no_args (Method.SIMPLE_METHOD' neg_clausify_tac),
"conversion of goal to conjecture clauses")];
-val setup = mark_skolemized #> skolem_cache_all #> ThmCache.init #> setup_attrs #> setup_methods;
+
+(** Attribute for converting a theorem into clauses **)
+
+val clausify = Attrib.syntax (Scan.lift Args.nat
+ >> (fn i => Thm.rule_attribute (fn context => fn th =>
+ Meson.make_meta_clause (nth (cnf_axiom (Context.theory_of context) th) i))));
+
+val setup_attrs = Attrib.add_attributes
+ [("clausify", clausify, "conversion of theorem to clauses")];
+
+
+
+(** setup **)
+
+val setup =
+ meson_method_setup #>
+ setup_methods #>
+ setup_attrs #>
+ perhaps saturate_skolem_cache #>
+ Theory.at_end clause_cache_endtheory;
end;
+