1.1 --- a/src/HOL/Tools/res_axioms.ML Thu Jun 12 22:29:50 2008 +0200
1.2 +++ b/src/HOL/Tools/res_axioms.ML Thu Jun 12 22:29:51 2008 +0200
1.3 @@ -9,7 +9,7 @@
1.4 sig
1.5 val cnf_axiom: theory -> thm -> thm list
1.6 val pairname: thm -> string * thm
1.7 - val multi_base_blacklist: string list
1.8 + val multi_base_blacklist: string list
1.9 val bad_for_atp: thm -> bool
1.10 val type_has_empty_sort: typ -> bool
1.11 val cnf_rules_pairs: theory -> (string * thm) list -> (thm * (string * int)) list
1.12 @@ -20,8 +20,6 @@
1.13 val claset_rules_of: Proof.context -> (string * thm) list (*FIXME DELETE*)
1.14 val simpset_rules_of: Proof.context -> (string * thm) list (*FIXME DELETE*)
1.15 val atpset_rules_of: Proof.context -> (string * thm) list
1.16 - val meson_method_setup: theory -> theory
1.17 - val clause_cache_endtheory: theory -> theory option
1.18 val suppress_endtheory: bool ref (*for emergency use where endtheory causes problems*)
1.19 val setup: theory -> theory
1.20 end;
1.21 @@ -36,7 +34,7 @@
1.22 | type_has_empty_sort (TVar (_, [])) = true
1.23 | type_has_empty_sort (Type (_, Ts)) = exists type_has_empty_sort Ts
1.24 | type_has_empty_sort _ = false;
1.25 -
1.26 +
1.27 (**** Transformation of Elimination Rules into First-Order Formulas****)
1.28
1.29 val cfalse = cterm_of HOL.thy HOLogic.false_const;
1.30 @@ -161,15 +159,9 @@
1.31
1.32 val monomorphic = not o Term.exists_type (Term.exists_subtype Term.is_TVar);
1.33
1.34 -val abs_S = @{thm"abs_S"};
1.35 -val abs_K = @{thm"abs_K"};
1.36 -val abs_I = @{thm"abs_I"};
1.37 -val abs_B = @{thm"abs_B"};
1.38 -val abs_C = @{thm"abs_C"};
1.39 -
1.40 -val [f_B,g_B] = map (cterm_of @{theory}) (term_vars (prop_of abs_B));
1.41 -val [g_C,f_C] = map (cterm_of @{theory}) (term_vars (prop_of abs_C));
1.42 -val [f_S,g_S] = map (cterm_of @{theory}) (term_vars (prop_of abs_S));
1.43 +val [f_B,g_B] = map (cterm_of @{theory}) (term_vars (prop_of @{thm abs_B}));
1.44 +val [g_C,f_C] = map (cterm_of @{theory}) (term_vars (prop_of @{thm abs_C}));
1.45 +val [f_S,g_S] = map (cterm_of @{theory}) (term_vars (prop_of @{thm abs_S}));
1.46
1.47 (*FIXME: requires more use of cterm constructors*)
1.48 fun abstract ct =
1.49 @@ -178,37 +170,37 @@
1.50 val thy = theory_of_cterm ct
1.51 val Type("fun",[xT,bodyT]) = typ_of (ctyp_of_term ct)
1.52 val cxT = ctyp_of thy xT and cbodyT = ctyp_of thy bodyT
1.53 - fun makeK() = instantiate' [SOME cxT, SOME cbodyT] [SOME (cterm_of thy body)] abs_K
1.54 + fun makeK() = instantiate' [SOME cxT, SOME cbodyT] [SOME (cterm_of thy body)] @{thm abs_K}
1.55 in
1.56 case body of
1.57 Const _ => makeK()
1.58 | Free _ => makeK()
1.59 | Var _ => makeK() (*though Var isn't expected*)
1.60 - | Bound 0 => instantiate' [SOME cxT] [] abs_I (*identity: I*)
1.61 + | Bound 0 => instantiate' [SOME cxT] [] @{thm abs_I} (*identity: I*)
1.62 | rator$rand =>
1.63 - if loose_bvar1 (rator,0) then (*C or S*)
1.64 + if loose_bvar1 (rator,0) then (*C or S*)
1.65 if loose_bvar1 (rand,0) then (*S*)
1.66 let val crator = cterm_of thy (Abs(x,xT,rator))
1.67 val crand = cterm_of thy (Abs(x,xT,rand))
1.68 - val abs_S' = cterm_instantiate [(f_S,crator),(g_S,crand)] abs_S
1.69 - val (_,rhs) = Thm.dest_equals (cprop_of abs_S')
1.70 + val abs_S' = cterm_instantiate [(f_S,crator),(g_S,crand)] @{thm abs_S}
1.71 + val (_,rhs) = Thm.dest_equals (cprop_of abs_S')
1.72 in
1.73 Thm.transitive abs_S' (Conv.binop_conv abstract rhs)
1.74 end
1.75 else (*C*)
1.76 let val crator = cterm_of thy (Abs(x,xT,rator))
1.77 - val abs_C' = cterm_instantiate [(f_C,crator),(g_C,cterm_of thy rand)] abs_C
1.78 - val (_,rhs) = Thm.dest_equals (cprop_of abs_C')
1.79 + val abs_C' = cterm_instantiate [(f_C,crator),(g_C,cterm_of thy rand)] @{thm abs_C}
1.80 + val (_,rhs) = Thm.dest_equals (cprop_of abs_C')
1.81 in
1.82 Thm.transitive abs_C' (Conv.fun_conv (Conv.arg_conv abstract) rhs)
1.83 end
1.84 - else if loose_bvar1 (rand,0) then (*B or eta*)
1.85 + else if loose_bvar1 (rand,0) then (*B or eta*)
1.86 if rand = Bound 0 then eta_conversion ct
1.87 else (*B*)
1.88 let val crand = cterm_of thy (Abs(x,xT,rand))
1.89 val crator = cterm_of thy rator
1.90 - val abs_B' = cterm_instantiate [(f_B,crator),(g_B,crand)] abs_B
1.91 - val (_,rhs) = Thm.dest_equals (cprop_of abs_B')
1.92 + val abs_B' = cterm_instantiate [(f_B,crator),(g_B,crand)] @{thm abs_B}
1.93 + val (_,rhs) = Thm.dest_equals (cprop_of abs_B')
1.94 in
1.95 Thm.transitive abs_B' (Conv.arg_conv abstract rhs)
1.96 end
1.97 @@ -235,16 +227,16 @@
1.98 | t1 $ t2 =>
1.99 let val (ct1,ct2) = Thm.dest_comb ct
1.100 in combination (combinators_aux ct1) (combinators_aux ct2) end;
1.101 -
1.102 +
1.103 fun combinators th =
1.104 - if lambda_free (prop_of th) then th
1.105 + if lambda_free (prop_of th) then th
1.106 else
1.107 let val _ = Output.debug (fn()=>"Conversion to combinators: " ^ Display.string_of_thm th);
1.108 val th = Drule.eta_contraction_rule th
1.109 val eqth = combinators_aux (cprop_of th)
1.110 val _ = Output.debug (fn()=>"Conversion result: " ^ Display.string_of_thm eqth);
1.111 in equal_elim eqth th end
1.112 - handle THM (msg,_,_) =>
1.113 + handle THM (msg,_,_) =>
1.114 (warning ("Error in the combinator translation of " ^ Display.string_of_thm th);
1.115 warning (" Exception message: " ^ msg);
1.116 TrueI); (*A type variable of sort {} will cause make abstraction fail.*)
1.117 @@ -287,7 +279,7 @@
1.118 (*Converts an Isabelle theorem (intro, elim or simp format, even higher-order) into NNF.*)
1.119 fun to_nnf th ctxt0 =
1.120 let val th1 = th |> transform_elim |> zero_var_indexes
1.121 - val ((_,[th2]),ctxt) = Variable.import_thms false [th1] ctxt0
1.122 + val ((_,[th2]),ctxt) = Variable.import_thms true [th1] ctxt0
1.123 val th3 = th2 |> Conv.fconv_rule ObjectLogic.atomize |> Meson.make_nnf |> strip_lambdas ~1
1.124 in (th3, ctxt) end;
1.125
1.126 @@ -301,10 +293,10 @@
1.127 | ths' => error (msg ^ "\n" ^ cat_lines (map Display.string_of_thm ths'));
1.128
1.129
1.130 -(*** Blacklisting (duplicated in ResAtp? ***)
1.131 +(*** Blacklisting (duplicated in ResAtp?) ***)
1.132
1.133 val max_lambda_nesting = 3;
1.134 -
1.135 +
1.136 fun excessive_lambdas (f$t, k) = excessive_lambdas (f,k) orelse excessive_lambdas (t,k)
1.137 | excessive_lambdas (Abs(_,_,t), k) = k=0 orelse excessive_lambdas (t,k-1)
1.138 | excessive_lambdas _ = false;
1.139 @@ -320,25 +312,25 @@
1.140
1.141 (*The max apply_depth of any metis call in MetisExamples (on 31-10-2007) was 11.*)
1.142 val max_apply_depth = 15;
1.143 -
1.144 +
1.145 fun apply_depth (f$t) = Int.max (apply_depth f, apply_depth t + 1)
1.146 | apply_depth (Abs(_,_,t)) = apply_depth t
1.147 | apply_depth _ = 0;
1.148
1.149 -fun too_complex t =
1.150 - apply_depth t > max_apply_depth orelse
1.151 +fun too_complex t =
1.152 + apply_depth t > max_apply_depth orelse
1.153 Meson.too_many_clauses NONE t orelse
1.154 excessive_lambdas_fm [] t;
1.155 -
1.156 +
1.157 fun is_strange_thm th =
1.158 case head_of (concl_of th) of
1.159 Const (a,_) => (a <> "Trueprop" andalso a <> "==")
1.160 | _ => false;
1.161
1.162 -fun bad_for_atp th =
1.163 - PureThy.is_internal th
1.164 - orelse too_complex (prop_of th)
1.165 - orelse exists_type type_has_empty_sort (prop_of th)
1.166 +fun bad_for_atp th =
1.167 + PureThy.is_internal th
1.168 + orelse too_complex (prop_of th)
1.169 + orelse exists_type type_has_empty_sort (prop_of th)
1.170 orelse is_strange_thm th;
1.171
1.172 val multi_base_blacklist =
1.173 @@ -356,78 +348,66 @@
1.174 if PureThy.has_name_hint th then PureThy.get_name_hint th
1.175 else Display.string_of_thm th;
1.176
1.177 +(*Skolemize a named theorem, with Skolem functions as additional premises.*)
1.178 +fun skolem_thm (s, th) =
1.179 + if member (op =) multi_base_blacklist (Sign.base_name s) orelse bad_for_atp th then []
1.180 + else
1.181 + let
1.182 + val ctxt0 = Variable.thm_context th
1.183 + val (nnfth, ctxt1) = to_nnf th ctxt0
1.184 + val (cnfs, ctxt2) = Meson.make_cnf (assume_skolem_of_def s nnfth) nnfth ctxt1
1.185 + in cnfs |> map combinators |> Variable.export ctxt2 ctxt0 |> Meson.finish_cnf end
1.186 + handle THM _ => [];
1.187 +
1.188 (*Declare Skolem functions for a theorem, supplied in nnf and with its name.
1.189 It returns a modified theory, unless skolemization fails.*)
1.190 -fun skolem th0 thy =
1.191 +fun skolem (name, th0) thy =
1.192 let
1.193 val th = Thm.transfer thy th0
1.194 val ctxt0 = Variable.thm_context th
1.195 - val _ = Output.debug (fn () => "skolemizing " ^ name_or_string th)
1.196 in
1.197 - Option.map
1.198 - (fn (nnfth,ctxt1) =>
1.199 - let
1.200 - val _ = Output.debug (fn () => " initial nnf: " ^ Display.string_of_thm nnfth)
1.201 - val s = fake_name th
1.202 - val (defs,thy') = declare_skofuns s nnfth thy
1.203 - val (cnfs,ctxt2) = Meson.make_cnf (map skolem_of_def defs) nnfth ctxt1
1.204 - val _ = Output.debug (fn () => Int.toString (length cnfs) ^ " clauses yielded")
1.205 - val cnfs' = cnfs |> map combinators |> Variable.export ctxt2 ctxt0
1.206 - |> Meson.finish_cnf |> map Thm.close_derivation
1.207 - in (cnfs', thy') end
1.208 - handle Clausify_failure thy_e => ([],thy_e)
1.209 - )
1.210 - (try (to_nnf th) ctxt0)
1.211 + try (to_nnf th) ctxt0 |> Option.map (fn (nnfth, ctxt1) =>
1.212 + let
1.213 + val s = flatten_name name
1.214 + val (defs, thy') = declare_skofuns s nnfth thy
1.215 + val (cnfs, ctxt2) = Meson.make_cnf (map skolem_of_def defs) nnfth ctxt1
1.216 + val cnfs' = cnfs |> map combinators |> Variable.export ctxt2 ctxt0
1.217 + |> Meson.finish_cnf |> map Thm.close_derivation
1.218 + in (cnfs', thy') end
1.219 + handle Clausify_failure thy_e => ([], thy_e)) (* FIXME !? *)
1.220 end;
1.221
1.222 (*The cache prevents repeated clausification of a theorem, and also repeated declaration of
1.223 Skolem functions.*)
1.224 structure ThmCache = TheoryDataFun
1.225 (
1.226 - type T = thm list Thmtab.table;
1.227 - val empty = Thmtab.empty;
1.228 + type T = thm list Thmtab.table * unit Symtab.table
1.229 + val empty = (Thmtab.empty, Symtab.empty)
1.230 val copy = I;
1.231 val extend = I;
1.232 - fun merge _ tabs : T = Thmtab.merge (K true) tabs;
1.233 + fun merge _ ((cache1, seen1), (cache2, seen2)) : T =
1.234 + (Thmtab.merge (K true) (cache1, cache2), Symtab.merge (K true) (seen1, seen2));
1.235 );
1.236
1.237 -(*Populate the clause cache using the supplied theorem. Return the clausal form
1.238 - and modified theory.*)
1.239 -fun skolem_cache_thm th thy =
1.240 - case Thmtab.lookup (ThmCache.get thy) th of
1.241 - NONE =>
1.242 - (case skolem th thy of
1.243 - NONE => ([th],thy)
1.244 - | SOME (cls,thy') =>
1.245 - (Output.debug (fn () => "skolem_cache_thm: " ^ Int.toString (length cls) ^
1.246 - " clauses inserted into cache: " ^ name_or_string th);
1.247 - (cls, ThmCache.map (Thmtab.update (th,cls)) thy')))
1.248 - | SOME cls => (cls,thy);
1.249 +val lookup_cache = Thmtab.lookup o #1 o ThmCache.get;
1.250 +val already_seen = Symtab.defined o #2 o ThmCache.get;
1.251
1.252 -(*Skolemize a named theorem, with Skolem functions as additional premises.*)
1.253 -fun skolem_thm (s,th) =
1.254 - if (Sign.base_name s) mem_string multi_base_blacklist orelse bad_for_atp th then []
1.255 - else
1.256 - let val ctxt0 = Variable.thm_context th
1.257 - val (nnfth,ctxt1) = to_nnf th ctxt0
1.258 - val (cnfs,ctxt2) = Meson.make_cnf (assume_skolem_of_def s nnfth) nnfth ctxt1
1.259 - in cnfs |> map combinators |> Variable.export ctxt2 ctxt0 |> Meson.finish_cnf end
1.260 - handle THM _ => [];
1.261 +val update_cache = ThmCache.map o apfst o Thmtab.update;
1.262 +fun mark_seen name = ThmCache.map (apsnd (Symtab.update (name, ())));
1.263
1.264 (*Exported function to convert Isabelle theorems into axiom clauses*)
1.265 fun cnf_axiom thy th0 =
1.266 - let val th = Thm.transfer thy th0
1.267 - in
1.268 - case Thmtab.lookup (ThmCache.get thy) th of
1.269 - NONE => (Output.debug (fn () => "cnf_axiom: " ^ name_or_string th);
1.270 - map Thm.close_derivation (skolem_thm (fake_name th, th)))
1.271 - | SOME cls => cls
1.272 + let val th = Thm.transfer thy th0 in
1.273 + case lookup_cache thy th of
1.274 + NONE => map Thm.close_derivation (skolem_thm (fake_name th, th))
1.275 + | SOME cls => cls
1.276 end;
1.277
1.278 -fun pairname th = (PureThy.get_name_hint th, th);
1.279
1.280 (**** Extract and Clausify theorems from a theory's claset and simpset ****)
1.281
1.282 +fun pairname th = (PureThy.get_name_hint th, th);
1.283 +
1.284 fun rules_of_claset cs =
1.285 let val {safeIs,safeEs,hazIs,hazEs,...} = rep_cs cs
1.286 val intros = safeIs @ hazIs
1.287 @@ -467,35 +447,41 @@
1.288 fun cnf_rules_pairs thy l = cnf_rules_pairs_aux thy [] (rev l);
1.289
1.290
1.291 -(**** Convert all theorems of a claset/simpset into clauses (ResClause.clause, or ResHolClause.clause) ****)
1.292 +(**** Convert all facts of the theory into clauses (ResClause.clause, or ResHolClause.clause) ****)
1.293
1.294 -(*Setup function: takes a theory and installs ALL known theorems into the clause cache*)
1.295 +(*Populate the clause cache using the supplied theorem. Return the clausal form
1.296 + and modified theory.*)
1.297 +fun skolem_cache_thm (name, th) thy =
1.298 + if bad_for_atp th then thy
1.299 + else
1.300 + (case lookup_cache thy th of
1.301 + SOME _ => thy
1.302 + | NONE =>
1.303 + (case skolem (name, th) thy of
1.304 + NONE => thy
1.305 + | SOME (cls, thy') => update_cache (th, cls) thy'));
1.306
1.307 -val mark_skolemized = Sign.add_consts_i [("ResAxioms_endtheory", HOLogic.boolT, NoSyn)];
1.308 +fun skolem_cache_fact (name, ths) (changed, thy) =
1.309 + if (Sign.base_name name) mem_string multi_base_blacklist orelse already_seen thy name
1.310 + then (changed, thy)
1.311 + else (true, thy |> mark_seen name |> fold skolem_cache_thm (PureThy.name_multi name ths));
1.312
1.313 -fun skolem_cache th thy =
1.314 - if bad_for_atp th then thy else #2 (skolem_cache_thm th thy);
1.315 +fun saturate_skolem_cache thy =
1.316 + (case Facts.fold_static skolem_cache_fact (PureThy.facts_of thy) (false, thy) of
1.317 + (false, _) => NONE
1.318 + | (true, thy') => SOME thy');
1.319
1.320 -fun skolem_cache_list (a,ths) thy =
1.321 - if (Sign.base_name a) mem_string multi_base_blacklist then thy
1.322 - else fold skolem_cache ths thy;
1.323
1.324 -val skolem_cache_theorems_of = Symtab.fold skolem_cache_list o #2 o PureThy.theorems_of;
1.325 -fun skolem_cache_node thy = skolem_cache_theorems_of thy thy;
1.326 -fun skolem_cache_all thy = fold skolem_cache_theorems_of (thy :: Theory.ancestors_of thy) thy;
1.327 +val suppress_endtheory = ref false;
1.328 +
1.329 +fun clause_cache_endtheory thy =
1.330 + if ! suppress_endtheory then NONE
1.331 + else saturate_skolem_cache thy;
1.332 +
1.333
1.334 (*The cache can be kept smaller by inspecting the prop of each thm. Can ignore all that are
1.335 lambda_free, but then the individual theory caches become much bigger.*)
1.336
1.337 -val suppress_endtheory = ref false;
1.338 -
1.339 -(*The new constant is a hack to prevent multiple execution*)
1.340 -fun clause_cache_endtheory thy =
1.341 - if !suppress_endtheory then NONE
1.342 - else
1.343 - (Output.debug (fn () => "RexAxioms end theory action: " ^ Context.str_of_thy thy);
1.344 - Option.map skolem_cache_node (try mark_skolemized thy) );
1.345 -
1.346
1.347 (*** meson proof methods ***)
1.348
1.349 @@ -538,13 +524,6 @@
1.350 "MESON resolution proof procedure")];
1.351
1.352
1.353 -(** Attribute for converting a theorem into clauses **)
1.354 -
1.355 -val clausify = Attrib.syntax (Scan.lift Args.nat
1.356 - >> (fn i => Thm.rule_attribute (fn context => fn th =>
1.357 - Meson.make_meta_clause (nth (cnf_axiom (Context.theory_of context) th) i))));
1.358 -
1.359 -
1.360 (*** Converting a subgoal into negated conjecture clauses. ***)
1.361
1.362 val neg_skolemize_tac = EVERY' [rtac ccontr, ObjectLogic.atomize_prems_tac, Meson.skolemize_tac];
1.363 @@ -573,28 +552,30 @@
1.364 REPEAT_DETERM_N (length ts) o (etac thin_rl)]
1.365 end);
1.366
1.367 -
1.368 -(** The Skolemization attribute **)
1.369 -
1.370 -fun conj2_rule (th1,th2) = conjI OF [th1,th2];
1.371 -
1.372 -(*Conjoin a list of theorems to form a single theorem*)
1.373 -fun conj_rule [] = TrueI
1.374 - | conj_rule ths = foldr1 conj2_rule ths;
1.375 -
1.376 -fun skolem_attr (Context.Theory thy, th) =
1.377 - let val (cls, thy') = skolem_cache_thm th thy
1.378 - in (Context.Theory thy', conj_rule cls) end
1.379 - | skolem_attr (context, th) = (context, th)
1.380 -
1.381 -val setup_attrs = Attrib.add_attributes
1.382 - [("skolem", Attrib.no_args skolem_attr, "skolemization of a theorem"),
1.383 - ("clausify", clausify, "conversion of theorem to clauses")];
1.384 -
1.385 val setup_methods = Method.add_methods
1.386 [("neg_clausify", Method.no_args (Method.SIMPLE_METHOD' neg_clausify_tac),
1.387 "conversion of goal to conjecture clauses")];
1.388
1.389 -val setup = mark_skolemized #> skolem_cache_all #> ThmCache.init #> setup_attrs #> setup_methods;
1.390 +
1.391 +(** Attribute for converting a theorem into clauses **)
1.392 +
1.393 +val clausify = Attrib.syntax (Scan.lift Args.nat
1.394 + >> (fn i => Thm.rule_attribute (fn context => fn th =>
1.395 + Meson.make_meta_clause (nth (cnf_axiom (Context.theory_of context) th) i))));
1.396 +
1.397 +val setup_attrs = Attrib.add_attributes
1.398 + [("clausify", clausify, "conversion of theorem to clauses")];
1.399 +
1.400 +
1.401 +
1.402 +(** setup **)
1.403 +
1.404 +val setup =
1.405 + meson_method_setup #>
1.406 + setup_methods #>
1.407 + setup_attrs #>
1.408 + perhaps saturate_skolem_cache #>
1.409 + Theory.at_end clause_cache_endtheory;
1.410
1.411 end;
1.412 +