--- a/src/HOL/Tools/res_axioms.ML Thu Sep 20 20:58:40 2007 +0200
+++ b/src/HOL/Tools/res_axioms.ML Fri Sep 21 22:51:08 2007 +0200
@@ -7,23 +7,25 @@
signature RES_AXIOMS =
sig
- val cnf_axiom : string * thm -> thm list
- val cnf_name : string -> thm list
- val meta_cnf_axiom : thm -> thm list
- val pairname : thm -> string * thm
- val skolem_thm : thm -> thm list
- val cnf_rules_pairs : (string * thm) list -> (thm * (string * int)) list
- val meson_method_setup : theory -> theory
- val setup : theory -> theory
- val clause_cache_setup : theory -> theory
+ val cnf_axiom: thm -> thm list
+ val meta_cnf_axiom: thm -> thm list
+ val pairname: thm -> string * thm
+ val skolem_thm: thm -> thm list
+ val cnf_rules_pairs: (string * thm) list -> (thm * (string * int)) list
+ val cnf_rules_of_ths: thm list -> thm list
+ val neg_clausify: thm list -> thm list
+ val expand_defs_tac: thm -> tactic
val assume_abstract_list: string -> thm list -> thm list
val neg_conjecture_clauses: thm -> int -> thm list * (string * typ) list
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_setup: theory -> theory
+ val setup: theory -> theory
end;
-structure ResAxioms =
+structure ResAxioms: RES_AXIOMS =
struct
(*For running the comparison between combinators and abstractions.
@@ -49,11 +51,11 @@
let val (_,ct) = Thm.dest_abs NONE (Thm.rhs_of th)
val t = Logic.legacy_varify (term_of ct)
in Net.insert_term Thm.eq_thm (t, th) net end;
-
-val abstraction_cache = ref
- (seed (thm"ATP_Linkup.I_simp")
- (seed (thm"ATP_Linkup.B_simp")
- (seed (thm"ATP_Linkup.K_simp") Net.empty)));
+
+val abstraction_cache = ref
+ (seed (thm"ATP_Linkup.I_simp")
+ (seed (thm"ATP_Linkup.B_simp")
+ (seed (thm"ATP_Linkup.K_simp") Net.empty)));
(**** Transformation of Elimination Rules into First-Order Formulas****)
@@ -66,9 +68,9 @@
conclusion variable to False.*)
fun transform_elim th =
case concl_of th of (*conclusion variable*)
- Const("Trueprop",_) $ (v as Var(_,Type("bool",[]))) =>
+ Const("Trueprop",_) $ (v as Var(_,Type("bool",[]))) =>
Thm.instantiate ([], [(cterm_of HOL.thy v, cfalse)]) th
- | v as Var(_, Type("prop",[])) =>
+ | v as Var(_, Type("prop",[])) =>
Thm.instantiate ([], [(cterm_of HOL.thy v, ctp_false)]) th
| _ => th;
@@ -167,11 +169,11 @@
(*Removes the lambdas from an equation of the form t = (%x. u). A non-negative n,
serves as an upper bound on how many to remove.*)
fun strip_lambdas 0 th = th
- | strip_lambdas n th =
+ | strip_lambdas n th =
case prop_of th of
- _ $ (Const ("op =", _) $ _ $ Abs (x,_,_)) =>
- strip_lambdas (n-1) (freeze_thm (th RS xfun_cong x))
- | _ => th;
+ _ $ (Const ("op =", _) $ _ $ Abs (x,_,_)) =>
+ strip_lambdas (n-1) (freeze_thm (th RS xfun_cong x))
+ | _ => th;
(*Convert meta- to object-equality. Fails for theorems like split_comp_eq,
where some types have the empty sort.*)
@@ -202,12 +204,9 @@
Context.joinable (theory_of_thm th1, theory_of_thm th2) andalso
rhs_of th1 aconv rhs_of th2;
-fun lambda_free (Abs _) = false
- | lambda_free (t $ u) = lambda_free t andalso lambda_free u
- | lambda_free _ = true;
+val lambda_free = not o Term.has_abs;
-fun monomorphic t =
- Term.fold_types (Term.fold_atyps (fn TVar _ => K false | _ => I)) t true;
+val monomorphic = not o Term.exists_type (Term.exists_subtype Term.is_TVar);
fun dest_abs_list ct =
let val (cv,ct') = Thm.dest_abs NONE ct
@@ -215,9 +214,6 @@
in (cv::cvs, cu) end
handle CTERM _ => ([],ct);
-fun lambda_list [] u = u
- | lambda_list (v::vs) u = lambda v (lambda_list vs u);
-
fun abstract_rule_list [] [] th = th
| abstract_rule_list (v::vs) (ct::cts) th = abstract_rule v ct (abstract_rule_list vs cts th)
| abstract_rule_list _ _ th = raise THM ("abstract_rule_list", 0, [th]);
@@ -228,12 +224,12 @@
(*Does an existing abstraction definition have an RHS that matches the one we need now?
thy is the current theory, which must extend that of theorem th.*)
fun match_rhs thy t th =
- let val _ = Output.debug (fn()=> "match_rhs: " ^ string_of_cterm (cterm_of thy t) ^
+ let val _ = Output.debug (fn()=> "match_rhs: " ^ string_of_cterm (cterm_of thy t) ^
" against\n" ^ string_of_thm th);
val (tyenv,tenv) = Pattern.first_order_match thy (rhs_of th, t) (tyenv0,tenv0)
val term_insts = map Meson.term_pair_of (Vartab.dest tenv)
- val ct_pairs = if subthy (theory_of_thm th, thy) andalso
- forall lambda_free (map #2 term_insts)
+ val ct_pairs = if subthy (theory_of_thm th, thy) andalso
+ forall lambda_free (map #2 term_insts)
then map (pairself (cterm_of thy)) term_insts
else raise Pattern.MATCH (*Cannot allow lambdas in the instantiation*)
fun ctyp2 (ixn, (S, T)) = (ctyp_of thy (TVar (ixn, S)), ctyp_of thy T)
@@ -259,7 +255,7 @@
val _ = Output.debug (fn()=>"Returned " ^ string_of_thm u'_th);
val cu' = Thm.rhs_of u'_th
val u' = term_of cu'
- val abs_v_u = lambda_list (map term_of cvs) u'
+ val abs_v_u = fold_rev (lambda o term_of) cvs u'
(*get the formal parameters: ALL variables free in the term*)
val args = term_frees abs_v_u
val _ = Output.debug (fn()=>Int.toString (length args) ^ " arguments");
@@ -268,9 +264,9 @@
val _ = Output.debug (fn()=>"Looking up " ^ string_of_cterm cu');
val thy = theory_of_thm u'_th
val (ax,ax',thy) =
- case List.mapPartial (match_rhs thy abs_v_u)
+ case List.mapPartial (match_rhs thy abs_v_u)
(Net.match_term (!abstraction_cache) u') of
- (ax,ax')::_ =>
+ (ax,ax')::_ =>
(Output.debug (fn()=>"Re-using axiom " ^ string_of_thm ax);
(ax,ax',thy))
| [] =>
@@ -291,7 +287,7 @@
val (_,ax') = Option.valOf (match_rhs thy abs_v_u ax)
val _ = Output.debug (fn()=> "Declaring: " ^ string_of_thm ax ^ "\n" ^
"Instance: " ^ string_of_thm ax');
- val _ = abstraction_cache := Net.insert_term eq_absdef
+ val _ = abstraction_cache := Net.insert_term eq_absdef
((Logic.varify u'), ax) (!abstraction_cache)
handle Net.INSERT =>
raise THM ("declare_absfuns: INSERT", 0, [th,u'_th,ax])
@@ -332,7 +328,7 @@
val cu' = Thm.rhs_of u'_th
val u' = term_of cu'
(*Could use Thm.cabs instead of lambda to work at level of cterms*)
- val abs_v_u = lambda_list (map term_of cvs) (term_of cu')
+ val abs_v_u = fold_rev (lambda o term_of) cvs (term_of cu')
(*get the formal parameters: free variables not present in the defs
(to avoid taking abstraction function names as parameters) *)
val args = filter (valid_name defs) (term_frees abs_v_u)
@@ -340,9 +336,9 @@
(*Forms a lambda-abstraction over the formal parameters*)
val rhs = term_of crhs
val (ax,ax') =
- case List.mapPartial (match_rhs thy abs_v_u)
+ case List.mapPartial (match_rhs thy abs_v_u)
(Net.match_term (!abstraction_cache) u') of
- (ax,ax')::_ =>
+ (ax,ax')::_ =>
(Output.debug (fn()=>"Re-using axiom " ^ string_of_thm ax);
(ax,ax'))
| [] =>
@@ -416,7 +412,7 @@
fun skolem_of_nnf s th =
map (skolem_of_def o assume o (cterm_of (theory_of_thm th))) (assume_skofuns s th);
-fun assert_lambda_free ths msg =
+fun assert_lambda_free ths msg =
case filter (not o lambda_free o prop_of) ths of
[] => ()
| ths' => error (msg ^ "\n" ^ cat_lines (map string_of_thm ths'));
@@ -451,7 +447,7 @@
fun flatten_name s = space_implode "_X" (NameSpace.explode s);
fun fake_name th =
- if PureThy.has_name_hint th then flatten_name (PureThy.get_name_hint th)
+ if PureThy.has_name_hint th then flatten_name (PureThy.get_name_hint th)
else gensym "unknown_thm_";
(*Skolemize a named theorem, with Skolem functions as additional premises.*)
@@ -483,7 +479,7 @@
fun merge _ (ref tab1, ref tab2) : T = ref (Thmtab.merge (K true) (tab1, tab2));
);
-(*The cache prevents repeated clausification of a theorem, and also repeated declaration of
+(*The cache prevents repeated clausification of a theorem, and also repeated declaration of
Skolem functions. The global one holds theorems proved prior to this point. Theory data
holds the remaining ones.*)
val global_clause_cache = ref (Thmtab.empty : (thm list) Thmtab.table);
@@ -495,11 +491,11 @@
NONE =>
(case skolem thy (Thm.transfer thy th) of
NONE => ([th],thy)
- | SOME (cls,thy') =>
- (if null cls
+ | SOME (cls,thy') =>
+ (if null cls
then warning ("skolem_cache: empty clause set for " ^ string_of_thm th)
else ();
- change clause_cache (Thmtab.update (th, cls));
+ change clause_cache (Thmtab.update (th, cls));
(cls,thy')))
| SOME cls => (cls,thy);
@@ -510,16 +506,16 @@
val in_cache = if cache = global_clause_cache then NONE else Thmtab.lookup (!cache) th
in
case in_cache of
- NONE =>
- (case Thmtab.lookup (!global_clause_cache) th of
- NONE =>
- let val cls = map Goal.close_result (skolem_thm th)
- in Output.debug (fn () => Int.toString (length cls) ^ " clauses inserted into cache: " ^
- (if PureThy.has_name_hint th then PureThy.get_name_hint th
- else string_of_thm th));
- change cache (Thmtab.update (th, cls)); cls
- end
- | SOME cls => cls)
+ NONE =>
+ (case Thmtab.lookup (!global_clause_cache) th of
+ NONE =>
+ let val cls = map Goal.close_result (skolem_thm th)
+ in Output.debug (fn () => Int.toString (length cls) ^ " clauses inserted into cache: " ^
+ (if PureThy.has_name_hint th then PureThy.get_name_hint th
+ else string_of_thm th));
+ change cache (Thmtab.update (th, cls)); cls
+ end
+ | SOME cls => cls)
| SOME cls => cls
end;
@@ -581,7 +577,7 @@
(*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.*)
-fun clause_cache_setup thy =
+fun clause_cache_setup thy =
fold (skolem_cache global_clause_cache) (map #2 (PureThy.all_thms_of thy)) thy;
@@ -605,7 +601,7 @@
val hyps = #hyps (crep_thm st)
val newhyps = filter_out (member (op aconv) hyps0 o Thm.term_of) hyps
val defs = filter (is_absko o Thm.term_of) newhyps
- val remaining_hyps = filter_out (member (op aconv) (map Thm.term_of defs))
+ val remaining_hyps = filter_out (member (op aconv) (map Thm.term_of defs))
(map Thm.term_of hyps)
val fixed = term_frees (concl_of st) @
foldl (gen_union (op aconv)) [] (map term_frees remaining_hyps)
@@ -652,19 +648,19 @@
in (neg_clausify (Option.valOf (metahyps_thms n st)), params) end
handle Option => raise ERROR "unable to Skolemize subgoal";
-(*Conversion of a subgoal to conjecture clauses. Each clause has
+(*Conversion of a subgoal to conjecture clauses. Each clause has
leading !!-bound universal variables, to express generality. *)
-val neg_clausify_tac =
- neg_skolemize_tac THEN'
+val neg_clausify_tac =
+ neg_skolemize_tac THEN'
SUBGOAL
(fn (prop,_) =>
let val ts = Logic.strip_assums_hyp prop
- in EVERY1
- [METAHYPS
- (fn hyps =>
+ in EVERY1
+ [METAHYPS
+ (fn hyps =>
(Method.insert_tac
(map forall_intr_vars (neg_clausify hyps)) 1)),
- REPEAT_DETERM_N (length ts) o (etac thin_rl)]
+ REPEAT_DETERM_N (length ts) o (etac thin_rl)]
end);
(** The Skolemization attribute **)
@@ -685,9 +681,9 @@
("clausify", clausify, "conversion of theorem to clauses")];
val setup_methods = Method.add_methods
- [("neg_clausify", Method.no_args (Method.SIMPLE_METHOD' neg_clausify_tac),
+ [("neg_clausify", Method.no_args (Method.SIMPLE_METHOD' neg_clausify_tac),
"conversion of goal to conjecture clauses")];
-
+
val setup = clause_cache_setup #> ThmCache.init #> setup_attrs #> setup_methods;
end;