diff -r 861a255cf1e7 -r a6d480e6c5f0 src/HOL/Tools/res_axioms.ML --- a/src/HOL/Tools/res_axioms.ML Thu May 19 02:33:40 2005 +0200 +++ b/src/HOL/Tools/res_axioms.ML Thu May 19 11:08:15 2005 +0200 @@ -5,8 +5,6 @@ Transformation of axiom rules (elim/intro/etc) into CNF forms. *) - - signature RES_AXIOMS = sig exception ELIMR2FOL of string @@ -27,6 +25,7 @@ val claset_rules_of_thy : theory -> (string * thm) list val simpset_rules_of_thy : theory -> (string * thm) list val clausify_rules : thm list -> thm list -> ResClause.clause list list * thm list + val setup : (theory -> theory) list end; structure ResAxioms : RES_AXIOMS = @@ -36,14 +35,14 @@ (**** Transformation of Elimination Rules into First-Order Formulas****) (* a tactic used to prove an elim-rule. *) -fun elimRule_tac thm = - ((rtac impI 1) ORELSE (rtac notI 1)) THEN (etac thm 1) THEN +fun elimRule_tac th = + ((rtac impI 1) ORELSE (rtac notI 1)) THEN (etac th 1) THEN REPEAT(Fast_tac 1); (* This following version fails sometimes, need to investigate, do not use it now. *) -fun elimRule_tac' thm = - ((rtac impI 1) ORELSE (rtac notI 1)) THEN (etac thm 1) THEN +fun elimRule_tac' th = + ((rtac impI 1) ORELSE (rtac notI 1)) THEN (etac th 1) THEN REPEAT(SOLVE((etac exI 1) ORELSE (rtac conjI 1) ORELSE (rtac disjI1 1) ORELSE (rtac disjI2 1))); @@ -126,21 +125,21 @@ (* check if a rule is an elim rule *) -fun is_elimR thm = - case (concl_of thm) of (Const ("Trueprop", _) $ Var (idx,_)) => true +fun is_elimR th = + case (concl_of th) of (Const ("Trueprop", _) $ Var (idx,_)) => true | Var(indx,Type("prop",[])) => true | _ => false; (* convert an elim-rule into an equivalent theorem that does not have the predicate variable. Leave other theorems unchanged.*) -fun transform_elim thm = - if is_elimR thm then - let val tm = elimR2Fol thm - val ctm = cterm_of (sign_of_thm thm) tm +fun transform_elim th = + if is_elimR th then + let val tm = elimR2Fol th + val ctm = cterm_of (sign_of_thm th) tm in - prove_goalw_cterm [] ctm (fn prems => [elimRule_tac thm]) + prove_goalw_cterm [] ctm (fn prems => [elimRule_tac th]) end - else thm; + else th; (**** Transformation of Clasets and Simpsets into First-Order Axioms ****) @@ -155,25 +154,26 @@ end; -(* convert a theorem into NNF and also skolemize it. *) -fun skolem_axiom thm = - if Term.is_first_order (prop_of thm) then - let val thm' = (skolemize o make_nnf o ObjectLogic.atomize_thm o Drule.freeze_all) thm +(*Convert a theorem into NNF and also skolemize it. Original version, using + Hilbert's epsilon in the resulting clauses.*) +fun skolem_axiom th = + if Term.is_first_order (prop_of th) then + let val th' = (skolemize o make_nnf o ObjectLogic.atomize_thm o Drule.freeze_all) th in - repeat_RS thm' someI_ex + repeat_RS th' someI_ex end - else raise THM ("skolem_axiom: not first-order", 0, [thm]); + else raise THM ("skolem_axiom: not first-order", 0, [th]); -fun cnf_rule thm = make_clauses [skolem_axiom (transform_elim thm)]; +fun cnf_rule th = make_clauses [skolem_axiom (transform_elim th)]; (*Transfer a theorem in to theory Reconstruction.thy if it is not already inside that theory -- because it's needed for Skolemization *) val recon_thy = ThyInfo.get_theory"Reconstruction"; -fun transfer_to_Reconstruction thm = - transfer recon_thy thm handle THM _ => thm; +fun transfer_to_Reconstruction th = + transfer recon_thy th handle THM _ => th; fun is_taut th = case (prop_of th) of @@ -184,14 +184,102 @@ val rm_redundant_cls = List.filter (not o is_taut); (* transform an Isabelle thm into CNF *) -fun cnf_axiom_aux thm = +fun cnf_axiom_aux th = map (zero_var_indexes o Thm.varifyT) - (rm_redundant_cls (cnf_rule (transfer_to_Reconstruction thm))); + (rm_redundant_cls (cnf_rule (transfer_to_Reconstruction th))); -(*Cache for clauses: could be a hash table if we provided them.*) +(**** SKOLEMIZATION BY INFERENCE (lcp) ****) + +(*Traverse a term, accumulating Skolem function definitions.*) +fun declare_skofuns s t thy = + let fun dec_sko (Const ("Ex",_) $ (xtp as Abs(_,T,p))) (n, thy) = + (*Existential: declare a Skolem function, then insert into body and continue*) + let val cname = s ^ "_" ^ Int.toString n + val args = term_frees xtp + val Ts = map type_of args + val cT = Ts ---> T + val c = Const(NameSpace.append (PureThy.get_name thy) cname, cT) + val rhs = list_abs_free (map dest_Free args, HOLogic.choice_const T $ xtp) + val def = equals cT $ c $ rhs + val thy' = Theory.add_consts_i [(cname, cT, NoSyn)] thy + val thy'' = Theory.add_defs_i false [(cname ^ "_def", def)] thy' + in dec_sko (subst_bound (list_comb(c,args), p)) (n+1, thy'') end + | dec_sko (Const ("All",_) $ (xtp as Abs(a,T,p))) (n, thy) = + (*Universal: insert a free variable into body and continue*) + let val fname = variant (add_term_names (p,[])) a + in dec_sko (subst_bound (Free(fname,T), p)) (n+1, thy) 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 (n,thy) = (n,thy) (*Do nothing otherwise*) + in #2 (dec_sko t (1,thy)) end; + +(*cterms are used throughout for efficiency*) +val cTrueprop = Thm.cterm_of (Theory.sign_of HOL.thy) HOLogic.Trueprop; + +(*cterm version of mk_cTrueprop*) +fun c_mkTrueprop A = Thm.capply cTrueprop A; + +(*Given an abstraction over n variables, replace the bound variables by free + ones. Return the body, along with the list of free variables.*) +fun c_variant_abs_multi (ct0, vars) = + let val (cv,ct) = Thm.dest_abs NONE ct0 + in c_variant_abs_multi (ct, cv::vars) end + handle CTERM _ => (ct0, rev vars); + +(*Given the definition of a Skolem function, return a theorem to replace + an existential formula by a use of that function.*) +fun skolem_of_def def = + let val (c,rhs) = Drule.dest_equals (cprop_of (Drule.freeze_all def)) + val (ch, frees) = c_variant_abs_multi (rhs, []) + val (chil,cabs) = Thm.dest_comb ch + val {sign, t, ...} = rep_cterm chil + val (Const ("Hilbert_Choice.Eps", Type("fun",[_,T]))) = t + val cex = Thm.cterm_of sign (HOLogic.exists_const T) + val ex_tm = c_mkTrueprop (Thm.capply cex cabs) + and conc = c_mkTrueprop (Drule.beta_conv cabs (Drule.list_comb(c,frees))); + in prove_goalw_cterm [def] (Drule.mk_implies (ex_tm, conc)) + (fn [prem] => [ rtac (prem RS someI_ex) 1 ]) + end; + + +(*Converts an Isabelle theorem (intro, elim or simp format) into nnf.*) +fun to_nnf thy th = + if Term.is_first_order (prop_of th) then + th |> Thm.transfer thy |> transform_elim |> Drule.freeze_all + |> ObjectLogic.atomize_thm |> make_nnf + else raise THM ("to_nnf: not first-order", 0, [th]); + +(*The cache prevents repeated clausification of a theorem, + and also repeated declaration of Skolem functions*) val clause_cache = ref (Symtab.empty : (thm * thm list) Symtab.table) +(*Declare Skolem functions for a theorem, supplied in nnf and with its name*) +fun skolem thy (name,th) = + let val cname = (case name of + "" => gensym "sko" | s => Sign.base_name s) + val thy' = declare_skofuns cname (#prop (rep_thm th)) thy + in (map (skolem_of_def o #2) (axioms_of thy'), thy') end; + +(*Populate the clause cache using the supplied theorems*) +fun skolemlist [] thy = thy + | skolemlist ((name,th)::nths) thy = + (case Symtab.lookup (!clause_cache,name) of + NONE => + let val nnfth = to_nnf thy th + val (skoths,thy') = skolem thy (name, nnfth) + val cls = Meson.make_cnf skoths nnfth + in clause_cache := Symtab.update ((name, (th,cls)), !clause_cache); + skolemlist nths thy' + end + | SOME _ => skolemlist nths thy) (*FIXME: check for duplicate names?*) + handle THM _ => skolemlist nths thy; + +(*Exported function to convert Isabelle theorems into axiom clauses*) fun cnf_axiom (name,th) = case name of "" => cnf_axiom_aux th (*no name, so can't cache*) @@ -246,32 +334,29 @@ | SOME sk => (sk,epss); -fun rm_Eps_cls_aux epss (t as (Const ("Hilbert_Choice.Eps",_) $ Abs(_,_,_))) = get_skolem epss t +fun rm_Eps_cls_aux epss (t as (Const ("Hilbert_Choice.Eps",_) $ Abs(_,_,_))) = + get_skolem epss t | rm_Eps_cls_aux epss (P $ Q) = - let val (P',epss') = rm_Eps_cls_aux epss P - val (Q',epss'') = rm_Eps_cls_aux epss' Q - in - (P' $ Q',epss'') - end + let val (P',epss') = rm_Eps_cls_aux epss P + val (Q',epss'') = rm_Eps_cls_aux epss' Q + in (P' $ Q',epss'') end | rm_Eps_cls_aux epss t = (t,epss); -fun rm_Eps_cls epss thm = rm_Eps_cls_aux epss (prop_of thm); +fun rm_Eps_cls epss th = rm_Eps_cls_aux epss (prop_of th); (* remove the epsilon terms in a formula, by skolem terms. *) fun rm_Eps _ [] = [] - | rm_Eps epss (thm::thms) = - let val (thm',epss') = rm_Eps_cls epss thm - in - thm' :: (rm_Eps epss' thms) - end; + | rm_Eps epss (th::thms) = + let val (th',epss') = rm_Eps_cls epss th + in th' :: (rm_Eps epss' thms) end; (* convert a theorem into CNF and then into Clause.clause format. *) -fun clausify_axiom thm = - let val name = Thm.name_of_thm thm - val isa_clauses = cnf_axiom (name, thm) +fun clausify_axiom th = + let val name = Thm.name_of_thm th + val isa_clauses = cnf_axiom (name, th) (*"isa_clauses" are already in "standard" form. *) val isa_clauses' = rm_Eps [] isa_clauses val clauses_n = length isa_clauses @@ -306,9 +391,9 @@ (* classical rules *) fun cnf_rules [] err_list = ([],err_list) - | cnf_rules ((name,thm) :: thms) err_list = + | cnf_rules ((name,th) :: thms) err_list = let val (ts,es) = cnf_rules thms err_list - in (cnf_axiom (name,thm) :: ts,es) handle _ => (ts, (thm::es)) end; + in (cnf_axiom (name,th) :: ts,es) handle _ => (ts, (th::es)) end; (* CNF all rules from a given theory's classical reasoner *) fun cnf_classical_rules_thy thy = @@ -323,13 +408,12 @@ (* classical rules *) fun clausify_rules [] err_list = ([],err_list) - | clausify_rules (thm::thms) err_list = + | clausify_rules (th::thms) err_list = let val (ts,es) = clausify_rules thms err_list in - ((clausify_axiom thm)::ts,es) handle _ => (ts,(thm::es)) + ((clausify_axiom th)::ts,es) handle _ => (ts,(th::es)) end; - (* convert all classical rules from a given theory into Clause.clause format. *) fun clausify_classical_rules_thy thy = clausify_rules (map #2 (claset_rules_of_thy thy)) []; @@ -338,5 +422,13 @@ fun clausify_simpset_rules_thy thy = clausify_rules (map #2 (simpset_rules_of_thy thy)) []; +(*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 + in skolemlist clas (skolemlist simps thy) end; + +val setup = [clause_cache_setup]; end;