1.1 --- a/src/HOL/Tools/meson.ML Thu Jun 15 17:50:30 2006 +0200
1.2 +++ b/src/HOL/Tools/meson.ML Thu Jun 15 17:50:47 2006 +0200
1.3 @@ -123,7 +123,8 @@
1.4 in exists taut_poslit poslits
1.5 orelse
1.6 exists (fn t => mem_term (t, neglits)) (HOLogic.false_const :: poslits)
1.7 - end;
1.8 + end
1.9 + handle TERM _ => false; (*probably dest_Trueprop on a weird theorem*)
1.10
1.11
1.12 (*** To remove trivial negated equality literals from clauses ***)
1.13 @@ -154,11 +155,20 @@
1.14 (*Simplify a clause by applying reflexivity to its negated equality literals*)
1.15 fun refl_clause th =
1.16 let val neqs = notequal_lits_count (HOLogic.dest_Trueprop (concl_of th))
1.17 - in zero_var_indexes (refl_clause_aux neqs th) end;
1.18 + in zero_var_indexes (refl_clause_aux neqs th) end
1.19 + handle TERM _ => th; (*probably dest_Trueprop on a weird theorem*)
1.20
1.21
1.22 (*** The basic CNF transformation ***)
1.23
1.24 +(*Estimate the number of clauses in order to detect infeasible theorems*)
1.25 +fun nclauses (Const("Trueprop",_) $ t) = nclauses t
1.26 + | nclauses (Const("op &",_) $ t $ u) = nclauses t + nclauses u
1.27 + | nclauses (Const("Ex", _) $ Abs (_,_,t)) = nclauses t
1.28 + | nclauses (Const("All",_) $ Abs (_,_,t)) = nclauses t
1.29 + | nclauses (Const("op |",_) $ t $ u) = nclauses t * nclauses u
1.30 + | nclauses _ = 1; (* literal *)
1.31 +
1.32 (*Replaces universally quantified variables by FREE variables -- because
1.33 assumptions may not contain scheme variables. Later, call "generalize". *)
1.34 fun freeze_spec th =
1.35 @@ -179,7 +189,7 @@
1.36 Eliminates existential quantifiers using skoths: Skolemization theorems.*)
1.37 fun cnf skoths (th,ths) =
1.38 let fun cnf_aux (th,ths) =
1.39 - if has_meta_conn (prop_of th) then ths (*meta-level: ignore*)
1.40 + if has_meta_conn (prop_of th) then ths (*meta-level: ignore*)
1.41 else if not (has_consts ["All","Ex","op &"] (prop_of th))
1.42 then th::ths (*no work to do, terminate*)
1.43 else case head_of (HOLogic.dest_Trueprop (concl_of th)) of
1.44 @@ -199,7 +209,9 @@
1.45 | _ => (*no work to do*) th::ths
1.46 and cnf_nil th = cnf_aux (th,[])
1.47 in
1.48 - cnf_aux (th,ths)
1.49 + if nclauses (concl_of th) > 20
1.50 + then (Output.debug ("cnf is ignoring: " ^ string_of_thm th); ths)
1.51 + else cnf_aux (th,ths)
1.52 end;
1.53
1.54 (*Convert all suitable free variables to schematic variables,
1.55 @@ -379,15 +391,18 @@
1.56 which are needed to avoid the various one-point theorems from generating junk clauses.*)
1.57 val tag_True = thm "tag_True";
1.58 val tag_False = thm "tag_False";
1.59 -val nnf_simps = [Ex1_def,Ball_def,Bex_def,tag_True,tag_False]
1.60 +val nnf_simps =
1.61 + [simp_implies_def, Ex1_def, Ball_def, Bex_def, tag_True, tag_False, if_True,
1.62 + if_False, if_cancel, if_eq_cancel, cases_simp];
1.63 +val nnf_extra_simps =
1.64 + thms"split_ifs" @ ex_simps @ all_simps @ simp_thms;
1.65
1.66 val nnf_ss =
1.67 - HOL_basic_ss addsimps
1.68 - (nnf_simps @ [if_True, if_False, if_cancel, if_eq_cancel, cases_simp] @
1.69 - thms"split_ifs" @ ex_simps @ all_simps @ simp_thms)
1.70 - addsimprocs [defALL_regroup,defEX_regroup,neq_simproc,let_simproc];
1.71 + HOL_basic_ss addsimps nnf_extra_simps
1.72 + addsimprocs [defALL_regroup,defEX_regroup,neq_simproc,let_simproc];
1.73
1.74 -fun make_nnf th = th |> simplify nnf_ss
1.75 +fun make_nnf th = th |> rewrite_rule (map safe_mk_meta_eq nnf_simps)
1.76 + |> simplify nnf_ss (*But this doesn't simplify premises...*)
1.77 |> make_nnf1
1.78
1.79 (*Pull existential quantifiers to front. This accomplishes Skolemization for
2.1 --- a/src/HOL/Tools/res_atp.ML Thu Jun 15 17:50:30 2006 +0200
2.2 +++ b/src/HOL/Tools/res_atp.ML Thu Jun 15 17:50:47 2006 +0200
2.3 @@ -39,10 +39,12 @@
2.4 val run_relevance_filter: bool ref
2.5 val run_blacklist_filter: bool ref
2.6 val invoke_atp_ml : ProofContext.context * thm -> unit
2.7 + val add_all : unit -> unit
2.8 val add_claset : unit -> unit
2.9 val add_simpset : unit -> unit
2.10 val add_clasimp : unit -> unit
2.11 val add_atpset : unit -> unit
2.12 + val rm_all : unit -> unit
2.13 val rm_claset : unit -> unit
2.14 val rm_simpset : unit -> unit
2.15 val rm_atpset : unit -> unit
2.16 @@ -133,13 +135,16 @@
2.17 else error ("No such directory: " ^ !destdir)
2.18 end;
2.19
2.20 +val include_all = ref false;
2.21 val include_simpset = ref false;
2.22 val include_claset = ref false;
2.23 val include_atpset = ref true;
2.24 +val add_all = (fn () => include_all:=true);
2.25 val add_simpset = (fn () => include_simpset:=true);
2.26 val add_claset = (fn () => include_claset:=true);
2.27 val add_clasimp = (fn () => (include_simpset:=true;include_claset:=true));
2.28 val add_atpset = (fn () => include_atpset:=true);
2.29 +val rm_all = (fn () => include_all:=false);
2.30 val rm_simpset = (fn () => include_simpset:=false);
2.31 val rm_claset = (fn () => include_claset:=false);
2.32 val rm_clasimp = (fn () => (include_simpset:=false;include_claset:=false));
2.33 @@ -512,47 +517,55 @@
2.34 in Output.debug nthm; display_thms nthms end;
2.35
2.36
2.37 +fun all_facts_of ctxt =
2.38 + FactIndex.find (ProofContext.fact_index_of ctxt) ([], [])
2.39 + |> maps #2 |> map (`Thm.name_of_thm);
2.40 +
2.41 (* get lemmas from claset, simpset, atpset and extra supplied rules *)
2.42 fun get_clasimp_atp_lemmas ctxt user_thms =
2.43 - let val claset_thms =
2.44 - if !include_claset then
2.45 - map put_name_pair (ResAxioms.claset_rules_of_ctxt ctxt)
2.46 - else []
2.47 - val simpset_thms =
2.48 - if !include_simpset then
2.49 - map put_name_pair (ResAxioms.simpset_rules_of_ctxt ctxt)
2.50 - else []
2.51 - val atpset_thms =
2.52 - if !include_atpset then
2.53 - map put_name_pair (ResAxioms.atpset_rules_of_ctxt ctxt)
2.54 - else []
2.55 - val _ = if !Output.show_debug_msgs then (Output.debug "ATP theorems: "; display_thms atpset_thms) else ()
2.56 - val user_rules =
2.57 - case user_thms of (*use whitelist if there are no user-supplied rules*)
2.58 - [] => map (put_name_pair o ResAxioms.pairname) (!whitelist)
2.59 - | _ => map put_name_pair user_thms
2.60 - in
2.61 - (claset_thms, simpset_thms, atpset_thms, user_rules)
2.62 - end;
2.63 + let val included_thms =
2.64 + if !include_all
2.65 + then (tap (fn ths => Output.debug ("Including all " ^ Int.toString (length ths) ^
2.66 + " theorems"))
2.67 + (all_facts_of ctxt @ PureThy.all_thms_of (ProofContext.theory_of ctxt)))
2.68 + else
2.69 + let val claset_thms =
2.70 + if !include_claset then ResAxioms.claset_rules_of_ctxt ctxt
2.71 + else []
2.72 + val simpset_thms =
2.73 + if !include_simpset then ResAxioms.simpset_rules_of_ctxt ctxt
2.74 + else []
2.75 + val atpset_thms =
2.76 + if !include_atpset then ResAxioms.atpset_rules_of_ctxt ctxt
2.77 + else []
2.78 + val _ = if !Output.show_debug_msgs
2.79 + then (Output.debug "ATP theorems: "; display_thms atpset_thms)
2.80 + else ()
2.81 + in claset_thms @ simpset_thms @ atpset_thms end
2.82 + val user_rules = map (put_name_pair o ResAxioms.pairname)
2.83 + (if null user_thms then !whitelist else user_thms)
2.84 + in
2.85 + (map put_name_pair included_thms, user_rules)
2.86 + end;
2.87
2.88 (* remove lemmas that are banned from the backlist *)
2.89 fun blacklist_filter thms =
2.90 - if !run_blacklist_filter then
2.91 - let val banned = make_banned_test (map #1 thms)
2.92 - fun ok (a,_) = not (banned a)
2.93 - in
2.94 - filter ok thms
2.95 - end
2.96 - else
2.97 - thms;
2.98 + if !run_blacklist_filter then
2.99 + let val banned = make_banned_test (map #1 thms)
2.100 + fun ok (a,_) = not (banned a)
2.101 + in filter ok thms end
2.102 + else thms;
2.103
2.104 (* filter axiom clauses, but keep supplied clauses and clauses in whitelist *)
2.105 fun get_relevant_clauses ctxt cls_thms white_cls goals =
2.106 - let val cls_thms_list = make_unique (mk_clause_table 2200) (List.concat (white_cls@cls_thms))
2.107 - 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
2.108 - in
2.109 - insert_thms (List.concat white_cls) relevant_cls_thms_list
2.110 - end;
2.111 + let val cls_thms_list = make_unique (mk_clause_table 2200) (List.concat (white_cls@cls_thms))
2.112 + val relevant_cls_thms_list =
2.113 + if !run_relevance_filter
2.114 + then ReduceAxiomsN.relevance_filter (ProofContext.theory_of ctxt) cls_thms_list goals
2.115 + else cls_thms_list
2.116 + in
2.117 + insert_thms (List.concat white_cls) relevant_cls_thms_list
2.118 + end;
2.119
2.120 (***************************************************************)
2.121 (* ATP invocation methods setup *)
2.122 @@ -587,8 +600,8 @@
2.123 let val conj_cls = make_clauses conjectures
2.124 val hyp_cls = cnf_hyps_thms ctxt
2.125 val goal_cls = conj_cls@hyp_cls
2.126 - val (cla_thms,simp_thms,atp_thms,user_rules) = get_clasimp_atp_lemmas ctxt (map ResAxioms.pairname user_thms)
2.127 - val rm_black_cls = blacklist_filter (cla_thms@simp_thms@atp_thms)
2.128 + val (included_thms,user_rules) = get_clasimp_atp_lemmas ctxt user_thms
2.129 + val rm_black_cls = blacklist_filter included_thms
2.130 val cla_simp_atp_clauses = ResAxioms.cnf_rules_pairs rm_black_cls
2.131 val user_cls = ResAxioms.cnf_rules_pairs user_rules
2.132 val axclauses_as_thms = get_relevant_clauses ctxt cla_simp_atp_clauses user_cls (map prop_of goal_cls)
2.133 @@ -685,8 +698,8 @@
2.134 fun write_problem_files pf (ctxt,th) =
2.135 let val goals = Thm.prems_of th
2.136 val _ = Output.debug ("number of subgoals = " ^ Int.toString (length goals))
2.137 - val (cla_thms,simp_thms,atp_thms,white_thms) = get_clasimp_atp_lemmas ctxt []
2.138 - val rm_blacklist_cls = blacklist_filter (cla_thms@simp_thms@atp_thms)
2.139 + val (included_thms,white_thms) = get_clasimp_atp_lemmas ctxt []
2.140 + val rm_blacklist_cls = blacklist_filter included_thms
2.141 val cla_simp_atp_clauses = ResAxioms.cnf_rules_pairs rm_blacklist_cls
2.142 val axclauses = get_relevant_clauses ctxt cla_simp_atp_clauses (ResAxioms.cnf_rules_pairs white_thms) goals
2.143 val _ = Output.debug ("claset, simprules and atprules total clauses = " ^
3.1 --- a/src/HOL/Tools/res_axioms.ML Thu Jun 15 17:50:30 2006 +0200
3.2 +++ b/src/HOL/Tools/res_axioms.ML Thu Jun 15 17:50:47 2006 +0200
3.3 @@ -44,88 +44,65 @@
3.4
3.5 exception ELIMR2FOL of string;
3.6
3.7 -(* functions used to construct a formula *)
3.8 -
3.9 -fun make_disjs [x] = x
3.10 - | make_disjs (x :: xs) = HOLogic.mk_disj(x, make_disjs xs)
3.11 -
3.12 -fun make_conjs [x] = x
3.13 - | make_conjs (x :: xs) = HOLogic.mk_conj(x, make_conjs xs)
3.14 -
3.15 fun add_EX tm [] = tm
3.16 | add_EX tm ((x,xtp)::xs) = add_EX (HOLogic.exists_const xtp $ Abs(x,xtp,tm)) xs;
3.17
3.18 -fun is_neg (Const("Trueprop",_) $ (Const("Not",_) $ Free(p,_))) (Const("Trueprop",_) $ Free(q,_)) = (p = q)
3.19 +(*Checks for the premise ~P when the conclusion is P.*)
3.20 +fun is_neg (Const("Trueprop",_) $ (Const("Not",_) $ Free(p,_)))
3.21 + (Const("Trueprop",_) $ Free(q,_)) = (p = q)
3.22 | is_neg _ _ = false;
3.23
3.24 -
3.25 -exception STRIP_CONCL;
3.26 -
3.27 -
3.28 +(*FIXME: What if dest_Trueprop fails?*)
3.29 fun strip_concl' prems bvs (Const ("==>",_) $ P $ Q) =
3.30 - let val P' = HOLogic.dest_Trueprop P
3.31 - val prems' = P'::prems
3.32 - in
3.33 - strip_concl' prems' bvs Q
3.34 - end
3.35 + strip_concl' (HOLogic.dest_Trueprop P :: prems) bvs Q
3.36 | strip_concl' prems bvs P =
3.37 let val P' = HOLogic.Not $ (HOLogic.dest_Trueprop P)
3.38 - in
3.39 - add_EX (make_conjs (P'::prems)) bvs
3.40 - end;
3.41 -
3.42 + in add_EX (foldr1 HOLogic.mk_conj (P'::prems)) bvs end;
3.43
3.44 fun strip_concl prems bvs concl (Const ("all", _) $ Abs (x,xtp,body)) =
3.45 strip_concl prems ((x,xtp)::bvs) concl body
3.46 | strip_concl prems bvs concl (Const ("==>",_) $ P $ Q) =
3.47 if (is_neg P concl) then (strip_concl' prems bvs Q)
3.48 else strip_concl (HOLogic.dest_Trueprop P::prems) bvs concl Q
3.49 - | strip_concl prems bvs concl _ = add_EX (make_conjs prems) bvs;
3.50 + | strip_concl prems bvs concl _ = add_EX (foldr1 HOLogic.mk_conj prems) bvs;
3.51
3.52 -
3.53 -fun trans_elim (main,others,concl) =
3.54 - let val others' = map (strip_concl [] [] concl) others
3.55 - val disjs = make_disjs others'
3.56 +fun trans_elim (major,minors,concl) =
3.57 + let val disjs = foldr1 HOLogic.mk_disj (map (strip_concl [] [] concl) minors)
3.58 in
3.59 - HOLogic.mk_imp (HOLogic.dest_Trueprop main, disjs)
3.60 + HOLogic.mk_imp (HOLogic.dest_Trueprop major, disjs)
3.61 end;
3.62
3.63 -
3.64 -(* aux function of elim2Fol, take away predicate variable. *)
3.65 -fun elimR2Fol_aux prems concl =
3.66 - let val nprems = length prems
3.67 - val main = hd prems
3.68 - in
3.69 - if (nprems = 1) then HOLogic.Not $ (HOLogic.dest_Trueprop main)
3.70 - else trans_elim (main, tl prems, concl)
3.71 - end;
3.72 -
3.73 -
3.74 (* convert an elim rule into an equivalent formula, of type term. *)
3.75 fun elimR2Fol elimR =
3.76 - let val elimR' = Drule.freeze_all elimR
3.77 - val (prems,concl) = (prems_of elimR', concl_of elimR')
3.78 - in
3.79 - case concl of Const("Trueprop",_) $ Free(_,Type("bool",[]))
3.80 - => HOLogic.mk_Trueprop (elimR2Fol_aux prems concl)
3.81 - | Free(x,Type("prop",[])) => HOLogic.mk_Trueprop(elimR2Fol_aux prems concl)
3.82 - | _ => raise ELIMR2FOL("Not an elimination rule!")
3.83 - end;
3.84 -
3.85 + let val elimR' = Drule.freeze_all elimR
3.86 + val (prems,concl) = (prems_of elimR', concl_of elimR')
3.87 + val _ = case concl of
3.88 + Const("Trueprop",_) $ Free(_,Type("bool",[])) => ()
3.89 + | Free(_, Type("prop",[])) => ()
3.90 + | _ => raise ELIMR2FOL "elimR2Fol: Not an elimination rule!"
3.91 + val th = case prems of
3.92 + [] => raise ELIMR2FOL "elimR2Fol: No premises!"
3.93 + | [major] => HOLogic.Not $ (HOLogic.dest_Trueprop major)
3.94 + | major::minors => trans_elim (major, minors, concl)
3.95 + in HOLogic.mk_Trueprop th end
3.96 + handle exn =>
3.97 + (warning ("elimR2Fol raised exception " ^ Toplevel.exn_message exn);
3.98 + concl_of elimR);
3.99
3.100 (* check if a rule is an elim rule *)
3.101 fun is_elimR th =
3.102 - case (concl_of th) of (Const ("Trueprop", _) $ Var (idx,_)) => true
3.103 - | Var(indx,Type("prop",[])) => true
3.104 - | _ => false;
3.105 + case concl_of th of Const ("Trueprop", _) $ Var _ => true
3.106 + | Var(_,Type("prop",[])) => true
3.107 + | _ => false;
3.108
3.109 (* convert an elim-rule into an equivalent theorem that does not have the
3.110 predicate variable. Leave other theorems unchanged.*)
3.111 fun transform_elim th =
3.112 if is_elimR th then
3.113 - let val tm = elimR2Fol th
3.114 - val ctm = cterm_of (sign_of_thm th) tm
3.115 + let val ctm = cterm_of (sign_of_thm th) (elimR2Fol th)
3.116 in Goal.prove_raw [] ctm (fn _ => elimRule_tac th) end
3.117 + handle exn => (warning ("transform_elim failed: " ^ Toplevel.exn_message exn ^
3.118 + " for theorem " ^ string_of_thm th); th)
3.119 else th;
3.120
3.121
3.122 @@ -303,12 +280,12 @@
3.123
3.124
3.125 (*Exported function to convert Isabelle theorems into axiom clauses*)
3.126 -fun cnf_axiom_g cnf (name,th) =
3.127 +fun cnf_axiom (name,th) =
3.128 case name of
3.129 - "" => cnf th (*no name, so can't cache*)
3.130 + "" => skolem_thm th (*no name, so can't cache*)
3.131 | s => case Symtab.lookup (!clause_cache) s of
3.132 NONE =>
3.133 - let val cls = cnf th
3.134 + let val cls = skolem_thm th
3.135 in change clause_cache (Symtab.update (s, (th, cls))); cls end
3.136 | SOME(th',cls) =>
3.137 if eq_thm(th,th') then cls
3.138 @@ -319,15 +296,10 @@
3.139
3.140 fun pairname th = (Thm.name_of_thm th, th);
3.141
3.142 -
3.143 -val cnf_axiom = cnf_axiom_g skolem_thm;
3.144 -
3.145 -
3.146 fun meta_cnf_axiom th =
3.147 map Meson.make_meta_clause (cnf_axiom (pairname th));
3.148
3.149
3.150 -
3.151 (**** Extract and Clausify theorems from a theory's claset and simpset ****)
3.152
3.153 (*Preserve the name of "th" after the transformation "f"*)
3.154 @@ -374,34 +346,27 @@
3.155
3.156 (**** Translate a set of classical/simplifier rules into CNF (still as type "thm") ****)
3.157
3.158 -(* classical rules *)
3.159 -fun cnf_rules_g cnf_axiom [] err_list = ([],err_list)
3.160 - | cnf_rules_g cnf_axiom ((name,th) :: ths) err_list =
3.161 - let val (ts,es) = cnf_rules_g cnf_axiom ths err_list
3.162 +(* classical rules: works for both FOL and HOL *)
3.163 +fun cnf_rules [] err_list = ([],err_list)
3.164 + | cnf_rules ((name,th) :: ths) err_list =
3.165 + let val (ts,es) = cnf_rules ths err_list
3.166 in (cnf_axiom (name,th) :: ts,es) handle _ => (ts, (th::es)) end;
3.167
3.168 -
3.169 -(*works for both FOL and HOL*)
3.170 -val cnf_rules = cnf_rules_g cnf_axiom;
3.171 -
3.172 -fun cnf_rules_pairs_aux [] = []
3.173 - | cnf_rules_pairs_aux ((name,th)::ths) =
3.174 - let val ts = cnf_rules_pairs_aux ths
3.175 - fun pair_name_cls k (n, []) = []
3.176 - | pair_name_cls k (n, cls::clss) =
3.177 - (cls, (n,k))::(pair_name_cls (k+1) (n, clss))
3.178 - in
3.179 - (pair_name_cls 0 (name, cnf_axiom(name,th)))::ts
3.180 - handle THM _ => ts | ResClause.CLAUSE _ => ts | ResHolClause.LAM2COMB _ => ts
3.181 - end;
3.182 +fun pair_name_cls k (n, []) = []
3.183 + | pair_name_cls k (n, cls::clss) = (cls, (n,k)) :: pair_name_cls (k+1) (n, clss)
3.184 +
3.185 +fun cnf_rules_pairs_aux pairs [] = pairs
3.186 + | cnf_rules_pairs_aux pairs ((name,th)::ths) =
3.187 + let val pairs' = (pair_name_cls 0 (name, cnf_axiom(name,th))) :: pairs
3.188 + handle THM _ => pairs | ResClause.CLAUSE _ => pairs
3.189 + | ResHolClause.LAM2COMB _ => pairs
3.190 + in cnf_rules_pairs_aux pairs' ths end;
3.191
3.192 -
3.193 -fun cnf_rules_pairs thms = rev (cnf_rules_pairs_aux thms);
3.194 +val cnf_rules_pairs = cnf_rules_pairs_aux [];
3.195
3.196
3.197 (**** Convert all theorems of a claset/simpset into clauses (ResClause.clause, or ResHolClause.clause) ****)
3.198
3.199 -
3.200 (*These should include any plausibly-useful theorems, especially if they need
3.201 Skolem functions. FIXME: this list is VERY INCOMPLETE*)
3.202 val default_initial_thms = map pairname