--- a/src/HOL/Tools/res_axioms.ML Fri Aug 25 18:48:09 2006 +0200
+++ b/src/HOL/Tools/res_axioms.ML Fri Aug 25 18:48:58 2006 +0200
@@ -18,6 +18,7 @@
val simpset_rules_of_ctxt : Proof.context -> (string * thm) list
val pairname : thm -> (string * thm)
val skolem_thm : thm -> thm list
+ val to_nnf : thm -> thm
val cnf_rules_pairs : (string * Thm.thm) list -> (Thm.thm * (string * int)) list list;
val meson_method_setup : theory -> theory
val setup : theory -> theory
@@ -25,17 +26,22 @@
val atpset_rules_of_thy : theory -> (string * thm) list
val atpset_rules_of_ctxt : Proof.context -> (string * thm) list
end;
-
-structure ResAxioms : RES_AXIOMS =
+
+structure ResAxioms =
struct
+(*FIXME DELETE: For running the comparison between combinators and abstractions.
+ CANNOT be a ref, as the setting is used while Isabelle is built.*)
+val abstract_lambdas = true;
+
+val trace_abs = ref false;
(**** Transformation of Elimination Rules into First-Order Formulas****)
(* a tactic used to prove an elim-rule. *)
fun elimRule_tac th =
- (resolve_tac [impI,notI] 1) THEN (etac th 1) THEN REPEAT(blast_tac HOL_cs 1);
+ (resolve_tac [impI,notI] 1) THEN (etac th 1) THEN REPEAT(fast_tac HOL_cs 1);
fun add_EX tm [] = tm
| add_EX tm ((x,xtp)::xs) = add_EX (HOLogic.exists_const xtp $ Abs(x,xtp,tm)) xs;
@@ -97,10 +103,8 @@
" for theorem " ^ string_of_thm th); th)
-
(**** Transformation of Clasets and Simpsets into First-Order Axioms ****)
-
(*Transfer a theorem into theory Reconstruction.thy if it is not already
inside that theory -- because it's needed for Skolemization *)
@@ -126,43 +130,41 @@
(*Traverse a theorem, declaring Skolem function definitions. String s is the suggested
prefix for the Skolem constant. Result is a new theory*)
fun declare_skofuns s th thy =
- let fun dec_sko (Const ("Ex",_) $ (xtp as Abs(_,T,p))) (n, (thy, axs)) =
+ let fun dec_sko (Const ("Ex",_) $ (xtp as Abs(_,T,p))) (thy, axs) =
(*Existential: declare a Skolem function, then insert into body and continue*)
- let val cname = s ^ "_" ^ Int.toString n
+ let val cname = gensym ("sko_" ^ s ^ "_")
val args = term_frees xtp (*get the formal parameter list*)
val Ts = map type_of args
val cT = Ts ---> T
val c = Const (Sign.full_name thy cname, cT)
val rhs = list_abs_free (map dest_Free args, HOLogic.choice_const T $ xtp)
(*Forms a lambda-abstraction over the formal parameters*)
- val def = equals cT $ c $ rhs
val thy' = Theory.add_consts_i [(cname, cT, NoSyn)] thy
(*Theory is augmented with the constant, then its def*)
val cdef = cname ^ "_def"
- val thy'' = Theory.add_defs_i false false [(cdef, def)] thy'
+ val thy'' = Theory.add_defs_i false false [(cdef, equals cT $ c $ rhs)] thy'
in dec_sko (subst_bound (list_comb(c,args), p))
- (n+1, (thy'', get_axiom thy'' cdef :: axs))
+ (thy'', get_axiom thy'' cdef :: axs)
end
- | dec_sko (Const ("All",_) $ (xtp as Abs(a,T,p))) (n, thx) =
+ | dec_sko (Const ("All",_) $ (xtp as Abs(a,T,p))) thx =
(*Universal quant: insert a free variable into body and continue*)
let val fname = Name.variant (add_term_names (p,[])) a
- in dec_sko (subst_bound (Free(fname,T), p)) (n, thx) end
- | dec_sko (Const ("op &", _) $ p $ q) nthy = dec_sko q (dec_sko p nthy)
- | dec_sko (Const ("op |", _) $ p $ q) nthy = dec_sko q (dec_sko p nthy)
- | dec_sko (Const ("Trueprop", _) $ p) nthy = dec_sko p nthy
- | dec_sko t nthx = nthx (*Do nothing otherwise*)
- in #2 (dec_sko (#prop (rep_thm th)) (1, (thy,[]))) end;
+ in dec_sko (subst_bound (Free(fname,T), p)) thx end
+ | dec_sko (Const ("op &", _) $ p $ q) thx = dec_sko q (dec_sko p thx)
+ | dec_sko (Const ("op |", _) $ p $ q) thx = dec_sko q (dec_sko p thx)
+ | dec_sko (Const ("Trueprop", _) $ p) thx = dec_sko p thx
+ | dec_sko t thx = thx (*Do nothing otherwise*)
+ in dec_sko (prop_of th) (thy,[]) end;
(*Traverse a theorem, accumulating Skolem function definitions.*)
fun assume_skofuns th =
let fun dec_sko (Const ("Ex",_) $ (xtp as Abs(_,T,p))) defs =
(*Existential: declare a Skolem function, then insert into body and continue*)
- let val name = Name.variant (add_term_names (p,[])) (gensym "sko_")
- val skos = map (#1 o Logic.dest_equals) defs (*existing sko fns*)
+ let val skos = map (#1 o Logic.dest_equals) defs (*existing sko fns*)
val args = term_frees xtp \\ skos (*the formal parameters*)
val Ts = map type_of args
val cT = Ts ---> T
- val c = Free (name, cT)
+ val c = Free (gensym "sko_", cT)
val rhs = list_abs_free (map dest_Free args,
HOLogic.choice_const T $ xtp)
(*Forms a lambda-abstraction over the formal parameters*)
@@ -178,7 +180,145 @@
| dec_sko (Const ("op |", _) $ p $ q) defs = dec_sko q (dec_sko p defs)
| dec_sko (Const ("Trueprop", _) $ p) defs = dec_sko p defs
| dec_sko t defs = defs (*Do nothing otherwise*)
- in dec_sko (#prop (rep_thm th)) [] end;
+ in dec_sko (prop_of th) [] end;
+
+
+(**** REPLACING ABSTRACTIONS BY FUNCTION DEFINITIONS ****)
+
+(*Returns the vars of a theorem*)
+fun vars_of_thm th =
+ map (Thm.cterm_of (Thm.theory_of_thm th) o Var) (Drule.fold_terms Term.add_vars th []);
+
+(*Make a version of fun_cong with a given variable name*)
+local
+ val fun_cong' = fun_cong RS asm_rl; (*renumber f, g to prevent clashes with (a,0)*)
+ val cx = hd (vars_of_thm fun_cong');
+ val ty = typ_of (ctyp_of_term cx);
+ val thy = Thm.theory_of_thm fun_cong;
+ fun mkvar a = cterm_of thy (Var((a,0),ty));
+in
+fun xfun_cong x = Thm.instantiate ([], [(cx, mkvar x)]) fun_cong'
+end;
+
+(*Removes the lambdas from an equation of the form t = (%x. u)*)
+fun strip_lambdas th =
+ case prop_of th of
+ _ $ (Const ("op =", _) $ _ $ Abs (x,_,_)) =>
+ strip_lambdas (#1 (Drule.freeze_thaw (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.*)
+fun object_eq th = th RS def_imp_eq
+ handle THM _ => error ("Theorem contains empty sort: " ^ string_of_thm th);
+
+fun valid_name vs (Free(x,T)) = x mem_string vs
+ | valid_name vs _ = false;
+
+(*Contract all eta-redexes in the theorem, lest they give rise to needless abstractions*)
+fun eta_conversion_rule th =
+ equal_elim (eta_conversion (cprop_of th)) th;
+
+fun crhs th =
+ case Drule.strip_comb (cprop_of th) of
+ (f, [_, rhs]) =>
+ (case term_of f of
+ Const ("==", _) => rhs
+ | _ => raise THM ("crhs", 0, [th]))
+ | _ => raise THM ("crhs", 1, [th]);
+
+(*Apply a function definition to an argument, beta-reducing the result.*)
+fun beta_comb cf x =
+ let val th1 = combination cf (reflexive x)
+ val th2 = beta_conversion false (crhs th1)
+ in transitive th1 th2 end;
+
+(*Apply a function definition to arguments, beta-reducing along the way.*)
+fun list_combination cf [] = cf
+ | list_combination cf (x::xs) = list_combination (beta_comb cf x) xs;
+
+fun list_cabs ([] , t) = t
+ | list_cabs (v::vars, t) = Thm.cabs v (list_cabs(vars,t));
+
+(*FIXME DELETE*)
+fun check_eta ct =
+ let val t = term_of ct
+ in if (t aconv Envir.eta_contract t) then ()
+ else error ("Eta redex in term: " ^ string_of_cterm ct)
+ end;
+
+(*Traverse a theorem, declaring abstraction function definitions. String s is the suggested
+ prefix for the constants. Resulting theory is returned in the first theorem. *)
+fun declare_absfuns th =
+ let fun abstract thy ct = case term_of ct of
+ Abs (_,T,u) =>
+ let val cname = gensym "abs_"
+ val _ = check_eta ct;
+ val (cv,cta) = Thm.dest_abs NONE ct
+ val v = (#1 o dest_Free o term_of) cv
+ val (u'_th,defs) = abstract thy cta
+ val cu' = crhs u'_th
+ val abs_v_u = lambda (term_of cv) (term_of cu')
+ (*get the formal parameters: ALL variables free in the term*)
+ val args = term_frees abs_v_u
+ val Ts = map type_of args
+ val cT = Ts ---> (T --> typ_of (ctyp_of_term cu'))
+ val thy = theory_of_thm u'_th
+ val c = Const (Sign.full_name thy cname, cT)
+ val thy = Theory.add_consts_i [(cname, cT, NoSyn)] thy
+ (*Theory is augmented with the constant, then its def*)
+ val rhs = list_abs_free (map dest_Free args, abs_v_u)
+ (*Forms a lambda-abstraction over the formal parameters*)
+ val cdef = cname ^ "_def"
+ val thy = Theory.add_defs_i false false [(cdef, equals cT $ c $ rhs)] thy
+ val def = #1 (Drule.freeze_thaw (get_axiom thy cdef))
+ val def_args = list_combination def (map (cterm_of thy) args)
+ in (transitive (abstract_rule v cv u'_th) (symmetric def_args),
+ def :: defs) end
+ | (t1$t2) =>
+ let val (ct1,ct2) = Thm.dest_comb ct
+ val (th1,defs1) = abstract thy ct1
+ val (th2,defs2) = abstract (theory_of_thm th1) ct2
+ in (combination th1 th2, defs1@defs2) end
+ | _ => (transfer thy (reflexive ct), [])
+ val _ = if !trace_abs then warning (string_of_thm th) else ();
+ val (eqth,defs) = abstract (theory_of_thm th) (cprop_of th)
+ val ths = equal_elim eqth th ::
+ map (forall_intr_vars o strip_lambdas o object_eq) defs
+ in (theory_of_thm eqth, ths) end;
+
+fun assume_absfuns th =
+ let val cterm = cterm_of (Thm.theory_of_thm th)
+ fun abstract vs ct = case term_of ct of
+ Abs (_,T,u) =>
+ let val (cv,cta) = Thm.dest_abs NONE ct
+ val _ = check_eta ct;
+ val v = (#1 o dest_Free o term_of) cv
+ val (u'_th,defs) = abstract (v::vs) cta
+ val cu' = crhs u'_th
+ val abs_v_u = Thm.cabs cv cu'
+ (*get the formal parameters: bound variables also present in the term*)
+ val args = filter (valid_name vs) (term_frees (term_of abs_v_u))
+ val Ts = map type_of args
+ val const_ty = Ts ---> (T --> typ_of (ctyp_of_term cu'))
+ val c = Free (gensym "abs_", const_ty)
+ val rhs = list_cabs (map cterm args, abs_v_u)
+ (*Forms a lambda-abstraction over the formal parameters*)
+ val def = assume (Thm.capply (cterm (equals const_ty $ c)) rhs)
+ val def_args = list_combination def (map cterm args)
+ in (transitive (abstract_rule v cv u'_th) (symmetric def_args),
+ def :: defs) end
+ | (t1$t2) =>
+ let val (ct1,ct2) = Thm.dest_comb ct
+ val (t1',defs1) = abstract vs ct1
+ val (t2',defs2) = abstract vs ct2
+ in (combination t1' t2', defs1@defs2) end
+ | _ => (reflexive ct, [])
+ val (eqth,defs) = abstract [] (cprop_of th)
+ in equal_elim eqth th ::
+ map (forall_intr_vars o strip_lambdas o object_eq) defs
+ end;
+
(*cterms are used throughout for efficiency*)
val cTrueprop = Thm.cterm_of HOL.thy HOLogic.Trueprop;
@@ -217,7 +357,7 @@
(*It now works for HOL too. *)
fun to_nnf th =
th |> transfer_to_Reconstruction
- |> transform_elim |> Drule.freeze_thaw |> #1
+ |> transform_elim |> zero_var_indexes |> Drule.freeze_thaw |> #1
|> ObjectLogic.atomize_thm |> make_nnf;
(*The cache prevents repeated clausification of a theorem,
@@ -230,23 +370,46 @@
fun skolem_of_nnf th =
map (skolem_of_def o assume o (cterm_of (theory_of_thm th))) (assume_skofuns th);
+(*Replace lambdas by assumed function definitions in the theorems*)
+fun assume_abstract ths =
+ if abstract_lambdas then List.concat (map (assume_absfuns o eta_conversion_rule) ths)
+ else map eta_conversion_rule ths;
+
+(*Replace lambdas by declared function definitions in the theorems*)
+fun declare_abstract' (thy, []) = (thy, [])
+ | declare_abstract' (thy, th::ths) =
+ let val (thy', th_defs) =
+ th |> zero_var_indexes |> Drule.freeze_thaw |> #1
+ |> eta_conversion_rule |> transfer thy |> declare_absfuns
+ val (thy'', ths') = declare_abstract' (thy', ths)
+ in (thy'', th_defs @ ths') end;
+
+(*FIXME DELETE*)
+fun declare_abstract (thy, ths) =
+ if abstract_lambdas then declare_abstract' (thy, ths)
+ else (thy, map eta_conversion_rule ths);
+
(*Skolemize a named theorem, with Skolem functions as additional premises.*)
(*also works for HOL*)
fun skolem_thm th =
let val nnfth = to_nnf th
- in rm_redundant_cls (Meson.make_cnf (skolem_of_nnf nnfth) nnfth)
+ in Meson.make_cnf (skolem_of_nnf nnfth) nnfth
+ |> assume_abstract |> Meson.finish_cnf |> rm_redundant_cls
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 thy (name,th) =
- let val cname = (case name of "" => gensym "sko_" | s => Sign.base_name s)
+ let val cname = (case name of "" => gensym "" | s => Sign.base_name s)
+ val _ = Output.debug ("skolemizing " ^ name ^ ": ")
in Option.map
(fn nnfth =>
let val (thy',defs) = declare_skofuns cname nnfth thy
- val skoths = map skolem_of_def defs
- in (thy', rm_redundant_cls (Meson.make_cnf skoths nnfth)) end)
+ val cnfs = Meson.make_cnf (map skolem_of_def defs) nnfth
+ val (thy'',cnfs') = declare_abstract (thy',cnfs)
+ in (thy'', rm_redundant_cls (Meson.finish_cnf cnfs'))
+ end)
(SOME (to_nnf th) handle THM _ => NONE)
end;
@@ -347,14 +510,8 @@
(**** Convert all theorems of a claset/simpset into clauses (ResClause.clause, or ResHolClause.clause) ****)
-(*Setup function: takes a theory and installs ALL simprules and claset rules
- into the clause cache*)
-fun clause_cache_setup thy =
- let val simps = simpset_rules_of_thy thy
- and clas = claset_rules_of_thy thy
- val thy1 = List.foldl skolem_cache thy clas
- in List.foldl skolem_cache thy1 simps end;
-(*Could be duplicate theorem names, due to multiple attributes*)
+(*Setup function: takes a theory and installs ALL known theorems into the clause cache*)
+fun clause_cache_setup thy = List.foldl skolem_cache thy (PureThy.all_thms_of thy);
(*** meson proof methods ***)
@@ -379,15 +536,14 @@
(*Conjoin a list of clauses to recreate a single theorem*)
val conj_rule = foldr1 conj2_rule;
-fun skolem (Context.Theory thy, th) =
- let
- val name = Thm.name_of_thm th
- val (cls, thy') = skolem_cache_thm ((name, th), thy)
+fun skolem_attr (Context.Theory thy, th) =
+ let val name = Thm.name_of_thm th
+ val (cls, thy') = skolem_cache_thm ((name, th), thy)
in (Context.Theory thy', conj_rule cls) end
- | skolem (context, th) = (context, conj_rule (skolem_thm th));
+ | skolem_attr (context, th) = (context, conj_rule (skolem_thm th));
val setup_attrs = Attrib.add_attributes
- [("skolem", Attrib.no_args skolem, "skolemization of a theorem")];
+ [("skolem", Attrib.no_args skolem_attr, "skolemization of a theorem")];
val setup = clause_cache_setup #> setup_attrs;