--- a/src/HOL/Tools/meson.ML Thu Jun 15 17:50:30 2006 +0200
+++ b/src/HOL/Tools/meson.ML Thu Jun 15 17:50:47 2006 +0200
@@ -123,7 +123,8 @@
in exists taut_poslit poslits
orelse
exists (fn t => mem_term (t, neglits)) (HOLogic.false_const :: poslits)
- end;
+ end
+ handle TERM _ => false; (*probably dest_Trueprop on a weird theorem*)
(*** To remove trivial negated equality literals from clauses ***)
@@ -154,11 +155,20 @@
(*Simplify a clause by applying reflexivity to its negated equality literals*)
fun refl_clause th =
let val neqs = notequal_lits_count (HOLogic.dest_Trueprop (concl_of th))
- in zero_var_indexes (refl_clause_aux neqs th) end;
+ in zero_var_indexes (refl_clause_aux neqs th) end
+ handle TERM _ => th; (*probably dest_Trueprop on a weird theorem*)
(*** The basic CNF transformation ***)
+(*Estimate the number of clauses in order to detect infeasible theorems*)
+fun nclauses (Const("Trueprop",_) $ t) = nclauses t
+ | nclauses (Const("op &",_) $ t $ u) = nclauses t + nclauses u
+ | nclauses (Const("Ex", _) $ Abs (_,_,t)) = nclauses t
+ | nclauses (Const("All",_) $ Abs (_,_,t)) = nclauses t
+ | nclauses (Const("op |",_) $ t $ u) = nclauses t * nclauses u
+ | nclauses _ = 1; (* literal *)
+
(*Replaces universally quantified variables by FREE variables -- because
assumptions may not contain scheme variables. Later, call "generalize". *)
fun freeze_spec th =
@@ -179,7 +189,7 @@
Eliminates existential quantifiers using skoths: Skolemization theorems.*)
fun cnf skoths (th,ths) =
let fun cnf_aux (th,ths) =
- if has_meta_conn (prop_of th) then ths (*meta-level: ignore*)
+ if has_meta_conn (prop_of th) then ths (*meta-level: ignore*)
else if not (has_consts ["All","Ex","op &"] (prop_of th))
then th::ths (*no work to do, terminate*)
else case head_of (HOLogic.dest_Trueprop (concl_of th)) of
@@ -199,7 +209,9 @@
| _ => (*no work to do*) th::ths
and cnf_nil th = cnf_aux (th,[])
in
- cnf_aux (th,ths)
+ if nclauses (concl_of th) > 20
+ then (Output.debug ("cnf is ignoring: " ^ string_of_thm th); ths)
+ else cnf_aux (th,ths)
end;
(*Convert all suitable free variables to schematic variables,
@@ -379,15 +391,18 @@
which are needed to avoid the various one-point theorems from generating junk clauses.*)
val tag_True = thm "tag_True";
val tag_False = thm "tag_False";
-val nnf_simps = [Ex1_def,Ball_def,Bex_def,tag_True,tag_False]
+val nnf_simps =
+ [simp_implies_def, Ex1_def, Ball_def, Bex_def, tag_True, tag_False, if_True,
+ if_False, if_cancel, if_eq_cancel, cases_simp];
+val nnf_extra_simps =
+ thms"split_ifs" @ ex_simps @ all_simps @ simp_thms;
val nnf_ss =
- HOL_basic_ss addsimps
- (nnf_simps @ [if_True, if_False, if_cancel, if_eq_cancel, cases_simp] @
- thms"split_ifs" @ ex_simps @ all_simps @ simp_thms)
- addsimprocs [defALL_regroup,defEX_regroup,neq_simproc,let_simproc];
+ HOL_basic_ss addsimps nnf_extra_simps
+ addsimprocs [defALL_regroup,defEX_regroup,neq_simproc,let_simproc];
-fun make_nnf th = th |> simplify nnf_ss
+fun make_nnf th = th |> rewrite_rule (map safe_mk_meta_eq nnf_simps)
+ |> simplify nnf_ss (*But this doesn't simplify premises...*)
|> make_nnf1
(*Pull existential quantifiers to front. This accomplishes Skolemization for
--- a/src/HOL/Tools/res_atp.ML Thu Jun 15 17:50:30 2006 +0200
+++ b/src/HOL/Tools/res_atp.ML Thu Jun 15 17:50:47 2006 +0200
@@ -39,10 +39,12 @@
val run_relevance_filter: bool ref
val run_blacklist_filter: bool ref
val invoke_atp_ml : ProofContext.context * thm -> unit
+ val add_all : unit -> unit
val add_claset : unit -> unit
val add_simpset : unit -> unit
val add_clasimp : unit -> unit
val add_atpset : unit -> unit
+ val rm_all : unit -> unit
val rm_claset : unit -> unit
val rm_simpset : unit -> unit
val rm_atpset : unit -> unit
@@ -133,13 +135,16 @@
else error ("No such directory: " ^ !destdir)
end;
+val include_all = ref false;
val include_simpset = ref false;
val include_claset = ref false;
val include_atpset = ref true;
+val add_all = (fn () => include_all:=true);
val add_simpset = (fn () => include_simpset:=true);
val add_claset = (fn () => include_claset:=true);
val add_clasimp = (fn () => (include_simpset:=true;include_claset:=true));
val add_atpset = (fn () => include_atpset:=true);
+val rm_all = (fn () => include_all:=false);
val rm_simpset = (fn () => include_simpset:=false);
val rm_claset = (fn () => include_claset:=false);
val rm_clasimp = (fn () => (include_simpset:=false;include_claset:=false));
@@ -512,47 +517,55 @@
in Output.debug nthm; display_thms nthms end;
+fun all_facts_of ctxt =
+ FactIndex.find (ProofContext.fact_index_of ctxt) ([], [])
+ |> maps #2 |> map (`Thm.name_of_thm);
+
(* get lemmas from claset, simpset, atpset and extra supplied rules *)
fun get_clasimp_atp_lemmas ctxt user_thms =
- let val claset_thms =
- if !include_claset then
- map put_name_pair (ResAxioms.claset_rules_of_ctxt ctxt)
- else []
- val simpset_thms =
- if !include_simpset then
- map put_name_pair (ResAxioms.simpset_rules_of_ctxt ctxt)
- else []
- val atpset_thms =
- if !include_atpset then
- map put_name_pair (ResAxioms.atpset_rules_of_ctxt ctxt)
- else []
- val _ = if !Output.show_debug_msgs then (Output.debug "ATP theorems: "; display_thms atpset_thms) else ()
- val user_rules =
- case user_thms of (*use whitelist if there are no user-supplied rules*)
- [] => map (put_name_pair o ResAxioms.pairname) (!whitelist)
- | _ => map put_name_pair user_thms
- in
- (claset_thms, simpset_thms, atpset_thms, user_rules)
- end;
+ let val included_thms =
+ if !include_all
+ then (tap (fn ths => Output.debug ("Including all " ^ Int.toString (length ths) ^
+ " theorems"))
+ (all_facts_of ctxt @ PureThy.all_thms_of (ProofContext.theory_of ctxt)))
+ else
+ let val claset_thms =
+ if !include_claset then ResAxioms.claset_rules_of_ctxt ctxt
+ else []
+ val simpset_thms =
+ if !include_simpset then ResAxioms.simpset_rules_of_ctxt ctxt
+ else []
+ val atpset_thms =
+ if !include_atpset then ResAxioms.atpset_rules_of_ctxt ctxt
+ else []
+ val _ = if !Output.show_debug_msgs
+ then (Output.debug "ATP theorems: "; display_thms atpset_thms)
+ else ()
+ in claset_thms @ simpset_thms @ atpset_thms end
+ val user_rules = map (put_name_pair o ResAxioms.pairname)
+ (if null user_thms then !whitelist else user_thms)
+ in
+ (map put_name_pair included_thms, user_rules)
+ end;
(* remove lemmas that are banned from the backlist *)
fun blacklist_filter thms =
- if !run_blacklist_filter then
- let val banned = make_banned_test (map #1 thms)
- fun ok (a,_) = not (banned a)
- in
- filter ok thms
- end
- else
- thms;
+ if !run_blacklist_filter then
+ let val banned = make_banned_test (map #1 thms)
+ fun ok (a,_) = not (banned a)
+ in filter ok thms end
+ else thms;
(* filter axiom clauses, but keep supplied clauses and clauses in whitelist *)
fun get_relevant_clauses ctxt cls_thms white_cls goals =
- let val cls_thms_list = make_unique (mk_clause_table 2200) (List.concat (white_cls@cls_thms))
- val relevant_cls_thms_list = if !run_relevance_filter then ReduceAxiomsN.relevance_filter (ProofContext.theory_of ctxt) cls_thms_list goals else cls_thms_list
- in
- insert_thms (List.concat white_cls) relevant_cls_thms_list
- end;
+ let val cls_thms_list = make_unique (mk_clause_table 2200) (List.concat (white_cls@cls_thms))
+ val relevant_cls_thms_list =
+ if !run_relevance_filter
+ then ReduceAxiomsN.relevance_filter (ProofContext.theory_of ctxt) cls_thms_list goals
+ else cls_thms_list
+ in
+ insert_thms (List.concat white_cls) relevant_cls_thms_list
+ end;
(***************************************************************)
(* ATP invocation methods setup *)
@@ -587,8 +600,8 @@
let val conj_cls = make_clauses conjectures
val hyp_cls = cnf_hyps_thms ctxt
val goal_cls = conj_cls@hyp_cls
- val (cla_thms,simp_thms,atp_thms,user_rules) = get_clasimp_atp_lemmas ctxt (map ResAxioms.pairname user_thms)
- val rm_black_cls = blacklist_filter (cla_thms@simp_thms@atp_thms)
+ val (included_thms,user_rules) = get_clasimp_atp_lemmas ctxt user_thms
+ val rm_black_cls = blacklist_filter included_thms
val cla_simp_atp_clauses = ResAxioms.cnf_rules_pairs rm_black_cls
val user_cls = ResAxioms.cnf_rules_pairs user_rules
val axclauses_as_thms = get_relevant_clauses ctxt cla_simp_atp_clauses user_cls (map prop_of goal_cls)
@@ -685,8 +698,8 @@
fun write_problem_files pf (ctxt,th) =
let val goals = Thm.prems_of th
val _ = Output.debug ("number of subgoals = " ^ Int.toString (length goals))
- val (cla_thms,simp_thms,atp_thms,white_thms) = get_clasimp_atp_lemmas ctxt []
- val rm_blacklist_cls = blacklist_filter (cla_thms@simp_thms@atp_thms)
+ val (included_thms,white_thms) = get_clasimp_atp_lemmas ctxt []
+ val rm_blacklist_cls = blacklist_filter included_thms
val cla_simp_atp_clauses = ResAxioms.cnf_rules_pairs rm_blacklist_cls
val axclauses = get_relevant_clauses ctxt cla_simp_atp_clauses (ResAxioms.cnf_rules_pairs white_thms) goals
val _ = Output.debug ("claset, simprules and atprules total clauses = " ^
--- a/src/HOL/Tools/res_axioms.ML Thu Jun 15 17:50:30 2006 +0200
+++ b/src/HOL/Tools/res_axioms.ML Thu Jun 15 17:50:47 2006 +0200
@@ -44,88 +44,65 @@
exception ELIMR2FOL of string;
-(* functions used to construct a formula *)
-
-fun make_disjs [x] = x
- | make_disjs (x :: xs) = HOLogic.mk_disj(x, make_disjs xs)
-
-fun make_conjs [x] = x
- | make_conjs (x :: xs) = HOLogic.mk_conj(x, make_conjs xs)
-
fun add_EX tm [] = tm
| add_EX tm ((x,xtp)::xs) = add_EX (HOLogic.exists_const xtp $ Abs(x,xtp,tm)) xs;
-fun is_neg (Const("Trueprop",_) $ (Const("Not",_) $ Free(p,_))) (Const("Trueprop",_) $ Free(q,_)) = (p = q)
+(*Checks for the premise ~P when the conclusion is P.*)
+fun is_neg (Const("Trueprop",_) $ (Const("Not",_) $ Free(p,_)))
+ (Const("Trueprop",_) $ Free(q,_)) = (p = q)
| is_neg _ _ = false;
-
-exception STRIP_CONCL;
-
-
+(*FIXME: What if dest_Trueprop fails?*)
fun strip_concl' prems bvs (Const ("==>",_) $ P $ Q) =
- let val P' = HOLogic.dest_Trueprop P
- val prems' = P'::prems
- in
- strip_concl' prems' bvs Q
- end
+ strip_concl' (HOLogic.dest_Trueprop P :: prems) bvs Q
| strip_concl' prems bvs P =
let val P' = HOLogic.Not $ (HOLogic.dest_Trueprop P)
- in
- add_EX (make_conjs (P'::prems)) bvs
- end;
-
+ in add_EX (foldr1 HOLogic.mk_conj (P'::prems)) bvs end;
fun strip_concl prems bvs concl (Const ("all", _) $ Abs (x,xtp,body)) =
strip_concl prems ((x,xtp)::bvs) concl body
| strip_concl prems bvs concl (Const ("==>",_) $ P $ Q) =
if (is_neg P concl) then (strip_concl' prems bvs Q)
else strip_concl (HOLogic.dest_Trueprop P::prems) bvs concl Q
- | strip_concl prems bvs concl _ = add_EX (make_conjs prems) bvs;
+ | strip_concl prems bvs concl _ = add_EX (foldr1 HOLogic.mk_conj prems) bvs;
-
-fun trans_elim (main,others,concl) =
- let val others' = map (strip_concl [] [] concl) others
- val disjs = make_disjs others'
+fun trans_elim (major,minors,concl) =
+ let val disjs = foldr1 HOLogic.mk_disj (map (strip_concl [] [] concl) minors)
in
- HOLogic.mk_imp (HOLogic.dest_Trueprop main, disjs)
+ HOLogic.mk_imp (HOLogic.dest_Trueprop major, disjs)
end;
-
-(* aux function of elim2Fol, take away predicate variable. *)
-fun elimR2Fol_aux prems concl =
- let val nprems = length prems
- val main = hd prems
- in
- if (nprems = 1) then HOLogic.Not $ (HOLogic.dest_Trueprop main)
- else trans_elim (main, tl prems, concl)
- end;
-
-
(* convert an elim rule into an equivalent formula, of type term. *)
fun elimR2Fol elimR =
- let val elimR' = Drule.freeze_all elimR
- val (prems,concl) = (prems_of elimR', concl_of elimR')
- in
- case concl of Const("Trueprop",_) $ Free(_,Type("bool",[]))
- => HOLogic.mk_Trueprop (elimR2Fol_aux prems concl)
- | Free(x,Type("prop",[])) => HOLogic.mk_Trueprop(elimR2Fol_aux prems concl)
- | _ => raise ELIMR2FOL("Not an elimination rule!")
- end;
-
+ let val elimR' = Drule.freeze_all elimR
+ val (prems,concl) = (prems_of elimR', concl_of elimR')
+ val _ = case concl of
+ Const("Trueprop",_) $ Free(_,Type("bool",[])) => ()
+ | Free(_, Type("prop",[])) => ()
+ | _ => raise ELIMR2FOL "elimR2Fol: Not an elimination rule!"
+ val th = case prems of
+ [] => raise ELIMR2FOL "elimR2Fol: No premises!"
+ | [major] => HOLogic.Not $ (HOLogic.dest_Trueprop major)
+ | major::minors => trans_elim (major, minors, concl)
+ in HOLogic.mk_Trueprop th end
+ handle exn =>
+ (warning ("elimR2Fol raised exception " ^ Toplevel.exn_message exn);
+ concl_of elimR);
(* check if a rule is an elim rule *)
fun is_elimR th =
- case (concl_of th) of (Const ("Trueprop", _) $ Var (idx,_)) => true
- | Var(indx,Type("prop",[])) => true
- | _ => false;
+ case concl_of th of Const ("Trueprop", _) $ Var _ => true
+ | Var(_,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 th =
if is_elimR th then
- let val tm = elimR2Fol th
- val ctm = cterm_of (sign_of_thm th) tm
+ let val ctm = cterm_of (sign_of_thm th) (elimR2Fol th)
in Goal.prove_raw [] ctm (fn _ => elimRule_tac th) end
+ handle exn => (warning ("transform_elim failed: " ^ Toplevel.exn_message exn ^
+ " for theorem " ^ string_of_thm th); th)
else th;
@@ -303,12 +280,12 @@
(*Exported function to convert Isabelle theorems into axiom clauses*)
-fun cnf_axiom_g cnf (name,th) =
+fun cnf_axiom (name,th) =
case name of
- "" => cnf th (*no name, so can't cache*)
+ "" => skolem_thm th (*no name, so can't cache*)
| s => case Symtab.lookup (!clause_cache) s of
NONE =>
- let val cls = cnf th
+ let val cls = skolem_thm th
in change clause_cache (Symtab.update (s, (th, cls))); cls end
| SOME(th',cls) =>
if eq_thm(th,th') then cls
@@ -319,15 +296,10 @@
fun pairname th = (Thm.name_of_thm th, th);
-
-val cnf_axiom = cnf_axiom_g skolem_thm;
-
-
fun meta_cnf_axiom th =
map Meson.make_meta_clause (cnf_axiom (pairname th));
-
(**** Extract and Clausify theorems from a theory's claset and simpset ****)
(*Preserve the name of "th" after the transformation "f"*)
@@ -374,34 +346,27 @@
(**** Translate a set of classical/simplifier rules into CNF (still as type "thm") ****)
-(* classical rules *)
-fun cnf_rules_g cnf_axiom [] err_list = ([],err_list)
- | cnf_rules_g cnf_axiom ((name,th) :: ths) err_list =
- let val (ts,es) = cnf_rules_g cnf_axiom ths err_list
+(* classical rules: works for both FOL and HOL *)
+fun cnf_rules [] err_list = ([],err_list)
+ | cnf_rules ((name,th) :: ths) err_list =
+ let val (ts,es) = cnf_rules ths err_list
in (cnf_axiom (name,th) :: ts,es) handle _ => (ts, (th::es)) end;
-
-(*works for both FOL and HOL*)
-val cnf_rules = cnf_rules_g cnf_axiom;
-
-fun cnf_rules_pairs_aux [] = []
- | cnf_rules_pairs_aux ((name,th)::ths) =
- let val ts = cnf_rules_pairs_aux ths
- fun pair_name_cls k (n, []) = []
- | pair_name_cls k (n, cls::clss) =
- (cls, (n,k))::(pair_name_cls (k+1) (n, clss))
- in
- (pair_name_cls 0 (name, cnf_axiom(name,th)))::ts
- handle THM _ => ts | ResClause.CLAUSE _ => ts | ResHolClause.LAM2COMB _ => ts
- end;
+fun pair_name_cls k (n, []) = []
+ | pair_name_cls k (n, cls::clss) = (cls, (n,k)) :: pair_name_cls (k+1) (n, clss)
+
+fun cnf_rules_pairs_aux pairs [] = pairs
+ | cnf_rules_pairs_aux pairs ((name,th)::ths) =
+ let val pairs' = (pair_name_cls 0 (name, cnf_axiom(name,th))) :: pairs
+ handle THM _ => pairs | ResClause.CLAUSE _ => pairs
+ | ResHolClause.LAM2COMB _ => pairs
+ in cnf_rules_pairs_aux pairs' ths end;
-
-fun cnf_rules_pairs thms = rev (cnf_rules_pairs_aux thms);
+val cnf_rules_pairs = cnf_rules_pairs_aux [];
(**** Convert all theorems of a claset/simpset into clauses (ResClause.clause, or ResHolClause.clause) ****)
-
(*These should include any plausibly-useful theorems, especially if they need
Skolem functions. FIXME: this list is VERY INCOMPLETE*)
val default_initial_thms = map pairname