blanchet@39941: (* Title: HOL/Tools/Meson/meson.ML paulson@9840: Author: Lawrence C Paulson, Cambridge University Computer Laboratory blanchet@39941: Author: Jasmin Blanchette, TU Muenchen paulson@9840: wenzelm@9869: The MESON resolution proof procedure for HOL. wenzelm@29267: When making clauses, avoids using the rewriter -- instead uses RS recursively. paulson@9840: *) paulson@9840: wenzelm@24300: signature MESON = paulson@15579: sig wenzelm@32955: val trace: bool Unsynchronized.ref wenzelm@24300: val term_pair_of: indexname * (typ * 'a) -> term * 'a wenzelm@24300: val size_of_subgoals: thm -> int blanchet@39269: val has_too_many_clauses: Proof.context -> term -> bool paulson@24937: val make_cnf: thm list -> thm -> Proof.context -> thm list * Proof.context wenzelm@24300: val finish_cnf: thm list -> thm list blanchet@38089: val presimplify: thm -> thm wenzelm@32262: val make_nnf: Proof.context -> thm -> thm blanchet@39950: val choice_theorems : theory -> thm list blanchet@39950: val skolemize_with_choice_theorems : Proof.context -> thm list -> thm -> thm blanchet@39904: val skolemize : Proof.context -> thm -> thm wenzelm@24300: val is_fol_term: theory -> term -> bool blanchet@35869: val make_clauses_unsorted: thm list -> thm list wenzelm@24300: val make_clauses: thm list -> thm list wenzelm@24300: val make_horns: thm list -> thm list wenzelm@24300: val best_prolog_tac: (thm -> int) -> thm list -> tactic wenzelm@24300: val depth_prolog_tac: thm list -> tactic wenzelm@24300: val gocls: thm list -> thm list blanchet@39900: val skolemize_prems_tac : Proof.context -> thm list -> int -> tactic blanchet@39037: val MESON: blanchet@39269: tactic -> (thm list -> thm list) -> (thm list -> tactic) -> Proof.context blanchet@39269: -> int -> tactic wenzelm@32262: val best_meson_tac: (thm -> int) -> Proof.context -> int -> tactic wenzelm@32262: val safe_best_meson_tac: Proof.context -> int -> tactic wenzelm@32262: val depth_meson_tac: Proof.context -> int -> tactic wenzelm@24300: val prolog_step_tac': thm list -> int -> tactic wenzelm@24300: val iter_deepen_prolog_tac: thm list -> tactic wenzelm@32262: val iter_deepen_meson_tac: Proof.context -> thm list -> int -> tactic wenzelm@24300: val make_meta_clause: thm -> thm wenzelm@24300: val make_meta_clauses: thm list -> thm list wenzelm@32262: val meson_tac: Proof.context -> thm list -> int -> tactic wenzelm@32262: val setup: theory -> theory paulson@15579: end paulson@9840: blanchet@39901: structure Meson : MESON = paulson@15579: struct paulson@9840: wenzelm@32955: val trace = Unsynchronized.ref false; wenzelm@32955: fun trace_msg msg = if ! trace then tracing (msg ()) else (); wenzelm@32955: paulson@26562: val max_clauses_default = 60; wenzelm@38806: val (max_clauses, setup) = Attrib.config_int "meson_max_clauses" (K max_clauses_default); paulson@26562: wenzelm@38802: (*No known example (on 1-5-2007) needs even thirty*) wenzelm@38802: val iter_deepen_limit = 50; wenzelm@38802: haftmann@31454: val disj_forward = @{thm disj_forward}; haftmann@31454: val disj_forward2 = @{thm disj_forward2}; haftmann@31454: val make_pos_rule = @{thm make_pos_rule}; haftmann@31454: val make_pos_rule' = @{thm make_pos_rule'}; haftmann@31454: val make_pos_goal = @{thm make_pos_goal}; haftmann@31454: val make_neg_rule = @{thm make_neg_rule}; haftmann@31454: val make_neg_rule' = @{thm make_neg_rule'}; haftmann@31454: val make_neg_goal = @{thm make_neg_goal}; haftmann@31454: val conj_forward = @{thm conj_forward}; haftmann@31454: val all_forward = @{thm all_forward}; haftmann@31454: val ex_forward = @{thm ex_forward}; haftmann@31454: blanchet@39953: val not_conjD = @{thm not_conjD}; blanchet@39953: val not_disjD = @{thm not_disjD}; blanchet@39953: val not_notD = @{thm not_notD}; blanchet@39953: val not_allD = @{thm not_allD}; blanchet@39953: val not_exD = @{thm not_exD}; blanchet@39953: val imp_to_disjD = @{thm imp_to_disjD}; blanchet@39953: val not_impD = @{thm not_impD}; blanchet@39953: val iff_to_disjD = @{thm iff_to_disjD}; blanchet@39953: val not_iffD = @{thm not_iffD}; blanchet@39953: val conj_exD1 = @{thm conj_exD1}; blanchet@39953: val conj_exD2 = @{thm conj_exD2}; blanchet@39953: val disj_exD = @{thm disj_exD}; blanchet@39953: val disj_exD1 = @{thm disj_exD1}; blanchet@39953: val disj_exD2 = @{thm disj_exD2}; blanchet@39953: val disj_assoc = @{thm disj_assoc}; blanchet@39953: val disj_comm = @{thm disj_comm}; blanchet@39953: val disj_FalseD1 = @{thm disj_FalseD1}; blanchet@39953: val disj_FalseD2 = @{thm disj_FalseD2}; paulson@9840: paulson@9840: paulson@15579: (**** Operators for forward proof ****) paulson@15579: paulson@20417: paulson@20417: (** First-order Resolution **) paulson@20417: paulson@20417: fun term_pair_of (ix, (ty,t)) = (Var (ix,ty), t); paulson@20417: paulson@20417: (*FIXME: currently does not "rename variables apart"*) paulson@20417: fun first_order_resolve thA thB = wenzelm@32262: (case wenzelm@32262: try (fn () => wenzelm@32262: let val thy = theory_of_thm thA wenzelm@32262: val tmA = concl_of thA wenzelm@32262: val Const("==>",_) $ tmB $ _ = prop_of thB blanchet@37398: val tenv = blanchet@37410: Pattern.first_order_match thy (tmB, tmA) blanchet@37410: (Vartab.empty, Vartab.empty) |> snd wenzelm@32262: val ct_pairs = map (pairself (cterm_of thy) o term_pair_of) (Vartab.dest tenv) wenzelm@32262: in thA RS (cterm_instantiate ct_pairs thB) end) () of wenzelm@32262: SOME th => th blanchet@37398: | NONE => raise THM ("first_order_resolve", 0, [thA, thB])) paulson@18175: blanchet@39904: (* Applying "choice" swaps the bound variable names. We tweak blanchet@39904: "Thm.rename_boundvars"'s input to get the desired names. *) blanchet@39930: fun fix_bounds (_ $ (Const (@{const_name Ex}, _) blanchet@39930: $ Abs (_, _, Const (@{const_name All}, _) $ _))) blanchet@39930: (t0 $ (Const (@{const_name All}, T1) blanchet@39930: $ Abs (a1, T1', Const (@{const_name Ex}, T2) blanchet@39930: $ Abs (a2, T2', t')))) = blanchet@39904: t0 $ (Const (@{const_name All}, T1) blanchet@39904: $ Abs (a2, T1', Const (@{const_name Ex}, T2) $ Abs (a1, T2', t'))) blanchet@39930: | fix_bounds _ t = t blanchet@39930: blanchet@39930: (* Hack to make it less likely that we lose our precious bound variable names in blanchet@39930: "rename_bvs_RS" below, because of a clash. *) blanchet@39930: val protect_prefix = "_" blanchet@39930: blanchet@39930: fun protect_bounds (t $ u) = protect_bounds t $ protect_bounds u blanchet@39930: | protect_bounds (Abs (s, T, t')) = blanchet@39930: Abs (protect_prefix ^ s, T, protect_bounds t') blanchet@39930: | protect_bounds t = t blanchet@39904: blanchet@39904: (* Forward proof while preserving bound variables names*) paulson@24937: fun rename_bvs_RS th rl = blanchet@39904: let blanchet@39904: val t = concl_of th blanchet@39930: val r = concl_of rl blanchet@39930: val th' = th RS Thm.rename_boundvars r (protect_bounds r) rl blanchet@39904: val t' = concl_of th' blanchet@39930: in Thm.rename_boundvars t' (fix_bounds t' t) th' end paulson@24937: paulson@24937: (*raises exception if no rules apply*) wenzelm@24300: fun tryres (th, rls) = paulson@18141: let fun tryall [] = raise THM("tryres", 0, th::rls) paulson@24937: | tryall (rl::rls) = (rename_bvs_RS th rl handle THM _ => tryall rls) paulson@18141: in tryall rls end; wenzelm@24300: paulson@21050: (*Permits forward proof from rules that discharge assumptions. The supplied proof state st, paulson@21050: e.g. from conj_forward, should have the form paulson@21050: "[| P' ==> ?P; Q' ==> ?Q |] ==> ?P & ?Q" paulson@21050: and the effect should be to instantiate ?P and ?Q with normalized versions of P' and Q'.*) wenzelm@32262: fun forward_res ctxt nf st = paulson@21050: let fun forward_tacf [prem] = rtac (nf prem) 1 wenzelm@24300: | forward_tacf prems = wenzelm@32091: error (cat_lines wenzelm@32091: ("Bad proof state in forward_res, please inform lcp@cl.cam.ac.uk:" :: wenzelm@32262: Display.string_of_thm ctxt st :: wenzelm@32262: "Premises:" :: map (Display.string_of_thm ctxt) prems)) paulson@21050: in wenzelm@37781: case Seq.pull (ALLGOALS (Misc_Legacy.METAHYPS forward_tacf) st) paulson@21050: of SOME(th,_) => th paulson@21050: | NONE => raise THM("forward_res", 0, [st]) paulson@21050: end; paulson@15579: paulson@20134: (*Are any of the logical connectives in "bs" present in the term?*) paulson@20134: fun has_conns bs = blanchet@39328: let fun has (Const _) = false haftmann@38557: | has (Const(@{const_name Trueprop},_) $ p) = has p haftmann@38557: | has (Const(@{const_name Not},_) $ p) = has p haftmann@38795: | has (Const(@{const_name HOL.disj},_) $ p $ q) = member (op =) bs @{const_name HOL.disj} orelse has p orelse has q haftmann@38795: | has (Const(@{const_name HOL.conj},_) $ p $ q) = member (op =) bs @{const_name HOL.conj} orelse has p orelse has q haftmann@38557: | has (Const(@{const_name All},_) $ Abs(_,_,p)) = member (op =) bs @{const_name All} orelse has p haftmann@38557: | has (Const(@{const_name Ex},_) $ Abs(_,_,p)) = member (op =) bs @{const_name Ex} orelse has p wenzelm@24300: | has _ = false paulson@15579: in has end; wenzelm@24300: paulson@9840: paulson@15579: (**** Clause handling ****) paulson@9840: haftmann@38557: fun literals (Const(@{const_name Trueprop},_) $ P) = literals P haftmann@38795: | literals (Const(@{const_name HOL.disj},_) $ P $ Q) = literals P @ literals Q haftmann@38557: | literals (Const(@{const_name Not},_) $ P) = [(false,P)] paulson@15579: | literals P = [(true,P)]; paulson@9840: paulson@15579: (*number of literals in a term*) paulson@15579: val nliterals = length o literals; paulson@9840: paulson@18389: paulson@18389: (*** Tautology Checking ***) paulson@18389: haftmann@38795: fun signed_lits_aux (Const (@{const_name HOL.disj}, _) $ P $ Q) (poslits, neglits) = paulson@18389: signed_lits_aux Q (signed_lits_aux P (poslits, neglits)) haftmann@38557: | signed_lits_aux (Const(@{const_name Not},_) $ P) (poslits, neglits) = (poslits, P::neglits) paulson@18389: | signed_lits_aux P (poslits, neglits) = (P::poslits, neglits); wenzelm@24300: paulson@18389: fun signed_lits th = signed_lits_aux (HOLogic.dest_Trueprop (concl_of th)) ([],[]); paulson@18389: paulson@18389: (*Literals like X=X are tautologous*) haftmann@38864: fun taut_poslit (Const(@{const_name HOL.eq},_) $ t $ u) = t aconv u haftmann@38557: | taut_poslit (Const(@{const_name True},_)) = true paulson@18389: | taut_poslit _ = false; paulson@18389: paulson@18389: fun is_taut th = paulson@18389: let val (poslits,neglits) = signed_lits th paulson@18389: in exists taut_poslit poslits paulson@18389: orelse wenzelm@20073: exists (member (op aconv) neglits) (HOLogic.false_const :: poslits) paulson@19894: end wenzelm@24300: handle TERM _ => false; (*probably dest_Trueprop on a weird theorem*) paulson@18389: paulson@18389: paulson@18389: (*** To remove trivial negated equality literals from clauses ***) paulson@18389: paulson@18389: (*They are typically functional reflexivity axioms and are the converses of paulson@18389: injectivity equivalences*) wenzelm@24300: blanchet@39953: val not_refl_disj_D = @{thm not_refl_disj_D}; paulson@18389: paulson@20119: (*Is either term a Var that does not properly occur in the other term?*) paulson@20119: fun eliminable (t as Var _, u) = t aconv u orelse not (Logic.occs(t,u)) paulson@20119: | eliminable (u, t as Var _) = t aconv u orelse not (Logic.occs(t,u)) paulson@20119: | eliminable _ = false; paulson@20119: paulson@18389: fun refl_clause_aux 0 th = th paulson@18389: | refl_clause_aux n th = paulson@18389: case HOLogic.dest_Trueprop (concl_of th) of haftmann@38795: (Const (@{const_name HOL.disj}, _) $ (Const (@{const_name HOL.disj}, _) $ _ $ _) $ _) => paulson@18389: refl_clause_aux n (th RS disj_assoc) (*isolate an atom as first disjunct*) haftmann@38864: | (Const (@{const_name HOL.disj}, _) $ (Const(@{const_name Not},_) $ (Const(@{const_name HOL.eq},_) $ t $ u)) $ _) => wenzelm@24300: if eliminable(t,u) wenzelm@24300: then refl_clause_aux (n-1) (th RS not_refl_disj_D) (*Var inequation: delete*) wenzelm@24300: else refl_clause_aux (n-1) (th RS disj_comm) (*not between Vars: ignore*) haftmann@38795: | (Const (@{const_name HOL.disj}, _) $ _ $ _) => refl_clause_aux n (th RS disj_comm) wenzelm@24300: | _ => (*not a disjunction*) th; paulson@18389: haftmann@38795: fun notequal_lits_count (Const (@{const_name HOL.disj}, _) $ P $ Q) = paulson@18389: notequal_lits_count P + notequal_lits_count Q haftmann@38864: | notequal_lits_count (Const(@{const_name Not},_) $ (Const(@{const_name HOL.eq},_) $ _ $ _)) = 1 paulson@18389: | notequal_lits_count _ = 0; paulson@18389: paulson@18389: (*Simplify a clause by applying reflexivity to its negated equality literals*) wenzelm@24300: fun refl_clause th = paulson@18389: let val neqs = notequal_lits_count (HOLogic.dest_Trueprop (concl_of th)) paulson@19894: in zero_var_indexes (refl_clause_aux neqs th) end wenzelm@24300: handle TERM _ => th; (*probably dest_Trueprop on a weird theorem*) paulson@18389: paulson@18389: paulson@24937: (*** Removal of duplicate literals ***) paulson@24937: paulson@24937: (*Forward proof, passing extra assumptions as theorems to the tactic*) blanchet@39328: fun forward_res2 nf hyps st = paulson@24937: case Seq.pull paulson@24937: (REPEAT wenzelm@37781: (Misc_Legacy.METAHYPS (fn major::minors => rtac (nf (minors@hyps) major) 1) 1) paulson@24937: st) paulson@24937: of SOME(th,_) => th paulson@24937: | NONE => raise THM("forward_res2", 0, [st]); paulson@24937: paulson@24937: (*Remove duplicates in P|Q by assuming ~P in Q paulson@24937: rls (initially []) accumulates assumptions of the form P==>False*) wenzelm@32262: fun nodups_aux ctxt rls th = nodups_aux ctxt rls (th RS disj_assoc) paulson@24937: handle THM _ => tryres(th,rls) blanchet@39328: handle THM _ => tryres(forward_res2 (nodups_aux ctxt) rls (th RS disj_forward2), paulson@24937: [disj_FalseD1, disj_FalseD2, asm_rl]) paulson@24937: handle THM _ => th; paulson@24937: paulson@24937: (*Remove duplicate literals, if there are any*) wenzelm@32262: fun nodups ctxt th = paulson@24937: if has_duplicates (op =) (literals (prop_of th)) wenzelm@32262: then nodups_aux ctxt [] th paulson@24937: else th; paulson@24937: paulson@24937: paulson@18389: (*** The basic CNF transformation ***) paulson@18389: blanchet@39328: fun estimated_num_clauses bound t = paulson@26562: let blanchet@39269: fun sum x y = if x < bound andalso y < bound then x+y else bound blanchet@39269: fun prod x y = if x < bound andalso y < bound then x*y else bound paulson@26562: paulson@26562: (*Estimate the number of clauses in order to detect infeasible theorems*) haftmann@38557: fun signed_nclauses b (Const(@{const_name Trueprop},_) $ t) = signed_nclauses b t haftmann@38557: | signed_nclauses b (Const(@{const_name Not},_) $ t) = signed_nclauses (not b) t haftmann@38795: | signed_nclauses b (Const(@{const_name HOL.conj},_) $ t $ u) = wenzelm@32960: if b then sum (signed_nclauses b t) (signed_nclauses b u) wenzelm@32960: else prod (signed_nclauses b t) (signed_nclauses b u) haftmann@38795: | signed_nclauses b (Const(@{const_name HOL.disj},_) $ t $ u) = wenzelm@32960: if b then prod (signed_nclauses b t) (signed_nclauses b u) wenzelm@32960: else sum (signed_nclauses b t) (signed_nclauses b u) haftmann@38786: | signed_nclauses b (Const(@{const_name HOL.implies},_) $ t $ u) = wenzelm@32960: if b then prod (signed_nclauses (not b) t) (signed_nclauses b u) wenzelm@32960: else sum (signed_nclauses (not b) t) (signed_nclauses b u) haftmann@38864: | signed_nclauses b (Const(@{const_name HOL.eq}, Type ("fun", [T, _])) $ t $ u) = wenzelm@32960: if T = HOLogic.boolT then (*Boolean equality is if-and-only-if*) wenzelm@32960: if b then sum (prod (signed_nclauses (not b) t) (signed_nclauses b u)) wenzelm@32960: (prod (signed_nclauses (not b) u) (signed_nclauses b t)) wenzelm@32960: else sum (prod (signed_nclauses b t) (signed_nclauses b u)) wenzelm@32960: (prod (signed_nclauses (not b) t) (signed_nclauses (not b) u)) wenzelm@32960: else 1 haftmann@38557: | signed_nclauses b (Const(@{const_name Ex}, _) $ Abs (_,_,t)) = signed_nclauses b t haftmann@38557: | signed_nclauses b (Const(@{const_name All},_) $ Abs (_,_,t)) = signed_nclauses b t paulson@26562: | signed_nclauses _ _ = 1; (* literal *) blanchet@39269: in signed_nclauses true t end blanchet@39269: blanchet@39269: fun has_too_many_clauses ctxt t = blanchet@39269: let val max_cl = Config.get ctxt max_clauses in blanchet@39328: estimated_num_clauses (max_cl + 1) t > max_cl blanchet@39269: end paulson@19894: paulson@15579: (*Replaces universally quantified variables by FREE variables -- because paulson@24937: assumptions may not contain scheme variables. Later, generalize using Variable.export. *) paulson@24937: local paulson@24937: val spec_var = Thm.dest_arg (Thm.dest_arg (#2 (Thm.dest_implies (Thm.cprop_of spec)))); paulson@24937: val spec_varT = #T (Thm.rep_cterm spec_var); haftmann@38557: fun name_of (Const (@{const_name All}, _) $ Abs(x,_,_)) = x | name_of _ = Name.uu; paulson@24937: in paulson@24937: fun freeze_spec th ctxt = paulson@24937: let paulson@24937: val cert = Thm.cterm_of (ProofContext.theory_of ctxt); paulson@24937: val ([x], ctxt') = Variable.variant_fixes [name_of (HOLogic.dest_Trueprop (concl_of th))] ctxt; paulson@24937: val spec' = Thm.instantiate ([], [(spec_var, cert (Free (x, spec_varT)))]) spec; paulson@24937: in (th RS spec', ctxt') end paulson@24937: end; paulson@9840: paulson@15998: (*Used with METAHYPS below. There is one assumption, which gets bound to prem paulson@15998: and then normalized via function nf. The normal form is given to resolve_tac, paulson@22515: instantiate a Boolean variable created by resolution with disj_forward. Since paulson@22515: (nf prem) returns a LIST of theorems, we can backtrack to get all combinations.*) paulson@15579: fun resop nf [prem] = resolve_tac (nf prem) 1; paulson@9840: blanchet@39037: (* Any need to extend this list with "HOL.type_class", "HOL.eq_class", blanchet@39037: and "Pure.term"? *) haftmann@38557: val has_meta_conn = exists_Const (member (op =) ["==", "==>", "=simp=>", "all", "prop"] o #1); paulson@20417: blanchet@37410: fun apply_skolem_theorem (th, rls) = blanchet@37398: let blanchet@37410: fun tryall [] = raise THM ("apply_skolem_theorem", 0, th::rls) blanchet@37398: | tryall (rl :: rls) = blanchet@37398: first_order_resolve th rl handle THM _ => tryall rls blanchet@37398: in tryall rls end paulson@22515: blanchet@37410: (* Conjunctive normal form, adding clauses from th in front of ths (for foldr). blanchet@37410: Strips universal quantifiers and breaks up conjunctions. blanchet@37410: Eliminates existential quantifiers using Skolemization theorems. *) blanchet@39886: fun cnf old_skolem_ths ctxt (th, ths) = wenzelm@33222: let val ctxtr = Unsynchronized.ref ctxt (* FIXME ??? *) paulson@24937: fun cnf_aux (th,ths) = wenzelm@24300: if not (can HOLogic.dest_Trueprop (prop_of th)) then ths (*meta-level: ignore*) haftmann@38795: else if not (has_conns [@{const_name All}, @{const_name Ex}, @{const_name HOL.conj}] (prop_of th)) wenzelm@32262: then nodups ctxt th :: ths (*no work to do, terminate*) wenzelm@24300: else case head_of (HOLogic.dest_Trueprop (concl_of th)) of haftmann@38795: Const (@{const_name HOL.conj}, _) => (*conjunction*) wenzelm@24300: cnf_aux (th RS conjunct1, cnf_aux (th RS conjunct2, ths)) haftmann@38557: | Const (@{const_name All}, _) => (*universal quantifier*) paulson@24937: let val (th',ctxt') = freeze_spec th (!ctxtr) paulson@24937: in ctxtr := ctxt'; cnf_aux (th', ths) end haftmann@38557: | Const (@{const_name Ex}, _) => wenzelm@24300: (*existential quantifier: Insert Skolem functions*) blanchet@39886: cnf_aux (apply_skolem_theorem (th, old_skolem_ths), ths) haftmann@38795: | Const (@{const_name HOL.disj}, _) => wenzelm@24300: (*Disjunction of P, Q: Create new goal of proving ?P | ?Q and solve it using wenzelm@24300: all combinations of converting P, Q to CNF.*) wenzelm@24300: let val tac = wenzelm@37781: Misc_Legacy.METAHYPS (resop cnf_nil) 1 THEN wenzelm@37781: (fn st' => st' |> Misc_Legacy.METAHYPS (resop cnf_nil) 1) wenzelm@24300: in Seq.list_of (tac (th RS disj_forward)) @ ths end wenzelm@32262: | _ => nodups ctxt th :: ths (*no work to do*) paulson@19154: and cnf_nil th = cnf_aux (th,[]) blanchet@39269: val cls = blanchet@39269: if has_too_many_clauses ctxt (concl_of th) wenzelm@32960: then (trace_msg (fn () => "cnf is ignoring: " ^ Display.string_of_thm ctxt th); ths) wenzelm@32960: else cnf_aux (th,ths) paulson@24937: in (cls, !ctxtr) end; paulson@22515: blanchet@39886: fun make_cnf old_skolem_ths th ctxt = cnf old_skolem_ths ctxt (th, []) paulson@20417: paulson@20417: (*Generalization, removal of redundant equalities, removal of tautologies.*) paulson@24937: fun finish_cnf ths = filter (not o is_taut) (map refl_clause ths); paulson@9840: paulson@9840: paulson@15579: (**** Generation of contrapositives ****) paulson@9840: haftmann@38557: fun is_left (Const (@{const_name Trueprop}, _) $ haftmann@38795: (Const (@{const_name HOL.disj}, _) $ (Const (@{const_name HOL.disj}, _) $ _ $ _) $ _)) = true paulson@21102: | is_left _ = false; wenzelm@24300: paulson@15579: (*Associate disjuctions to right -- make leftmost disjunct a LITERAL*) wenzelm@24300: fun assoc_right th = paulson@21102: if is_left (prop_of th) then assoc_right (th RS disj_assoc) paulson@21102: else th; paulson@9840: paulson@15579: (*Must check for negative literal first!*) paulson@15579: val clause_rules = [disj_assoc, make_neg_rule, make_pos_rule]; paulson@9840: paulson@15579: (*For ordinary resolution. *) paulson@15579: val resolution_clause_rules = [disj_assoc, make_neg_rule', make_pos_rule']; paulson@9840: paulson@15579: (*Create a goal or support clause, conclusing False*) paulson@15579: fun make_goal th = (*Must check for negative literal first!*) paulson@15579: make_goal (tryres(th, clause_rules)) paulson@15579: handle THM _ => tryres(th, [make_neg_goal, make_pos_goal]); paulson@9840: paulson@15579: (*Sort clauses by number of literals*) paulson@15579: fun fewerlits(th1,th2) = nliterals(prop_of th1) < nliterals(prop_of th2); paulson@9840: paulson@18389: fun sort_clauses ths = sort (make_ord fewerlits) ths; paulson@9840: blanchet@38099: fun has_bool @{typ bool} = true blanchet@38099: | has_bool (Type (_, Ts)) = exists has_bool Ts blanchet@38099: | has_bool _ = false blanchet@38099: blanchet@38099: fun has_fun (Type (@{type_name fun}, _)) = true blanchet@38099: | has_fun (Type (_, Ts)) = exists has_fun Ts blanchet@38099: | has_fun _ = false wenzelm@24300: wenzelm@24300: (*Is the string the name of a connective? Really only | and Not can remain, wenzelm@24300: since this code expects to be called on a clause form.*) wenzelm@19875: val is_conn = member (op =) haftmann@38795: [@{const_name Trueprop}, @{const_name HOL.conj}, @{const_name HOL.disj}, haftmann@38786: @{const_name HOL.implies}, @{const_name Not}, haftmann@38557: @{const_name All}, @{const_name Ex}, @{const_name Ball}, @{const_name Bex}]; paulson@15613: wenzelm@24300: (*True if the term contains a function--not a logical connective--where the type paulson@20524: of any argument contains bool.*) wenzelm@24300: val has_bool_arg_const = paulson@15613: exists_Const blanchet@38099: (fn (c,T) => not(is_conn c) andalso exists has_bool (binder_types T)); paulson@22381: wenzelm@24300: (*A higher-order instance of a first-order constant? Example is the definition of haftmann@38622: one, 1, at a function type in theory Function_Algebras.*) wenzelm@24300: fun higher_inst_const thy (c,T) = paulson@22381: case binder_types T of paulson@22381: [] => false (*not a function type, OK*) paulson@22381: | Ts => length (binder_types (Sign.the_const_type thy c)) <> length Ts; paulson@22381: paulson@24742: (*Returns false if any Vars in the theorem mention type bool. paulson@21102: Also rejects functions whose arguments are Booleans or other functions.*) paulson@22381: fun is_fol_term thy t = haftmann@38557: Term.is_first_order ["all", @{const_name All}, @{const_name Ex}] t andalso blanchet@38099: not (exists_subterm (fn Var (_, T) => has_bool T orelse has_fun T blanchet@38099: | _ => false) t orelse blanchet@38099: has_bool_arg_const t orelse wenzelm@24300: exists_Const (higher_inst_const thy) t orelse wenzelm@24300: has_meta_conn t); paulson@19204: paulson@21102: fun rigid t = not (is_Var (head_of t)); paulson@21102: haftmann@38795: fun ok4horn (Const (@{const_name Trueprop},_) $ (Const (@{const_name HOL.disj}, _) $ t $ _)) = rigid t haftmann@38557: | ok4horn (Const (@{const_name Trueprop},_) $ t) = rigid t paulson@21102: | ok4horn _ = false; paulson@21102: paulson@15579: (*Create a meta-level Horn clause*) wenzelm@24300: fun make_horn crules th = wenzelm@24300: if ok4horn (concl_of th) paulson@21102: then make_horn crules (tryres(th,crules)) handle THM _ => th paulson@21102: else th; paulson@9840: paulson@16563: (*Generate Horn clauses for all contrapositives of a clause. The input, th, paulson@16563: is a HOL disjunction.*) wenzelm@33339: fun add_contras crules th hcs = blanchet@39328: let fun rots (0,_) = hcs wenzelm@24300: | rots (k,th) = zero_var_indexes (make_horn crules th) :: wenzelm@24300: rots(k-1, assoc_right (th RS disj_comm)) paulson@15862: in case nliterals(prop_of th) of wenzelm@24300: 1 => th::hcs paulson@15579: | n => rots(n, assoc_right th) paulson@15579: end; paulson@9840: paulson@15579: (*Use "theorem naming" to label the clauses*) paulson@15579: fun name_thms label = wenzelm@33339: let fun name1 th (k, ths) = wenzelm@27865: (k-1, Thm.put_name_hint (label ^ string_of_int k) th :: ths) wenzelm@33339: in fn ths => #2 (fold_rev name1 ths (length ths, [])) end; paulson@9840: paulson@16563: (*Is the given disjunction an all-negative support clause?*) paulson@15579: fun is_negative th = forall (not o #1) (literals (prop_of th)); paulson@9840: wenzelm@33317: val neg_clauses = filter is_negative; paulson@9840: paulson@9840: paulson@15579: (***** MESON PROOF PROCEDURE *****) paulson@9840: haftmann@38557: fun rhyps (Const("==>",_) $ (Const(@{const_name Trueprop},_) $ A) $ phi, wenzelm@24300: As) = rhyps(phi, A::As) paulson@15579: | rhyps (_, As) = As; paulson@9840: paulson@15579: (** Detecting repeated assumptions in a subgoal **) paulson@9840: paulson@15579: (*The stringtree detects repeated assumptions.*) wenzelm@33245: fun ins_term t net = Net.insert_term (op aconv) (t, t) net; paulson@9840: paulson@15579: (*detects repetitions in a list of terms*) paulson@15579: fun has_reps [] = false paulson@15579: | has_reps [_] = false paulson@15579: | has_reps [t,u] = (t aconv u) wenzelm@33245: | has_reps ts = (fold ins_term ts Net.empty; false) handle Net.INSERT => true; paulson@9840: paulson@15579: (*Like TRYALL eq_assume_tac, but avoids expensive THEN calls*) paulson@18508: fun TRYING_eq_assume_tac 0 st = Seq.single st paulson@18508: | TRYING_eq_assume_tac i st = wenzelm@31945: TRYING_eq_assume_tac (i-1) (Thm.eq_assumption i st) paulson@18508: handle THM _ => TRYING_eq_assume_tac (i-1) st; paulson@18508: paulson@18508: fun TRYALL_eq_assume_tac st = TRYING_eq_assume_tac (nprems_of st) st; paulson@9840: paulson@15579: (*Loop checking: FAIL if trying to prove the same thing twice paulson@15579: -- if *ANY* subgoal has repeated literals*) paulson@15579: fun check_tac st = paulson@15579: if exists (fn prem => has_reps (rhyps(prem,[]))) (prems_of st) paulson@15579: then Seq.empty else Seq.single st; paulson@9840: paulson@9840: paulson@15579: (* net_resolve_tac actually made it slower... *) paulson@15579: fun prolog_step_tac horns i = paulson@15579: (assume_tac i APPEND resolve_tac horns i) THEN check_tac THEN paulson@18508: TRYALL_eq_assume_tac; paulson@9840: paulson@9840: (*Sums the sizes of the subgoals, ignoring hypotheses (ancestors)*) wenzelm@33339: fun addconcl prem sz = size_of_term (Logic.strip_assums_concl prem) + sz; paulson@15579: wenzelm@33339: fun size_of_subgoals st = fold_rev addconcl (prems_of st) 0; paulson@15579: paulson@9840: paulson@9840: (*Negation Normal Form*) paulson@9840: val nnf_rls = [imp_to_disjD, iff_to_disjD, not_conjD, not_disjD, wenzelm@9869: not_impD, not_iffD, not_allD, not_exD, not_notD]; paulson@15581: haftmann@38557: fun ok4nnf (Const (@{const_name Trueprop},_) $ (Const (@{const_name Not}, _) $ t)) = rigid t haftmann@38557: | ok4nnf (Const (@{const_name Trueprop},_) $ t) = rigid t paulson@21102: | ok4nnf _ = false; paulson@21102: wenzelm@32262: fun make_nnf1 ctxt th = wenzelm@24300: if ok4nnf (concl_of th) wenzelm@32262: then make_nnf1 ctxt (tryres(th, nnf_rls)) paulson@28174: handle THM ("tryres", _, _) => wenzelm@32262: forward_res ctxt (make_nnf1 ctxt) wenzelm@9869: (tryres(th, [conj_forward,disj_forward,all_forward,ex_forward])) paulson@28174: handle THM ("tryres", _, _) => th blanchet@38608: else th paulson@9840: wenzelm@24300: (*The simplification removes defined quantifiers and occurrences of True and False. paulson@20018: nnf_ss also includes the one-point simprocs, paulson@18405: which are needed to avoid the various one-point theorems from generating junk clauses.*) paulson@19894: val nnf_simps = blanchet@37539: @{thms simp_implies_def Ex1_def Ball_def Bex_def if_True if_False if_cancel blanchet@37539: if_eq_cancel cases_simp} blanchet@37539: val nnf_extra_simps = @{thms split_ifs ex_simps all_simps simp_thms} paulson@18405: paulson@18405: val nnf_ss = wenzelm@24300: HOL_basic_ss addsimps nnf_extra_simps wenzelm@24040: addsimprocs [defALL_regroup,defEX_regroup, @{simproc neq}, @{simproc let_simp}]; paulson@15872: blanchet@38089: val presimplify = blanchet@39900: rewrite_rule (map safe_mk_meta_eq nnf_simps) #> simplify nnf_ss blanchet@38089: wenzelm@32262: fun make_nnf ctxt th = case prems_of th of blanchet@38606: [] => th |> presimplify |> make_nnf1 ctxt paulson@21050: | _ => raise THM ("make_nnf: premises in argument", 0, [th]); paulson@15581: blanchet@39950: fun choice_theorems thy = blanchet@39950: try (Global_Theory.get_thm thy) "Hilbert_Choice.choice" |> the_list blanchet@39950: blanchet@39900: (* Pull existential quantifiers to front. This accomplishes Skolemization for blanchet@39900: clauses that arise from a subgoal. *) blanchet@39950: fun skolemize_with_choice_theorems ctxt choice_ths = blanchet@39900: let blanchet@39900: fun aux th = blanchet@39900: if not (has_conns [@{const_name Ex}] (prop_of th)) then blanchet@39900: th blanchet@39900: else blanchet@39901: tryres (th, choice_ths @ blanchet@39900: [conj_exD1, conj_exD2, disj_exD, disj_exD1, disj_exD2]) blanchet@39900: |> aux blanchet@39900: handle THM ("tryres", _, _) => blanchet@39900: tryres (th, [conj_forward, disj_forward, all_forward]) blanchet@39900: |> forward_res ctxt aux blanchet@39900: |> aux blanchet@39900: handle THM ("tryres", _, _) => blanchet@39900: rename_bvs_RS th ex_forward blanchet@39900: |> forward_res ctxt aux blanchet@39900: in aux o make_nnf ctxt end paulson@29684: blanchet@39950: fun skolemize ctxt = blanchet@39950: let val thy = ProofContext.theory_of ctxt in blanchet@39950: skolemize_with_choice_theorems ctxt (choice_theorems thy) blanchet@39950: end blanchet@39904: blanchet@39900: (* "RS" can fail if "unify_search_bound" is too small. *) blanchet@39900: fun try_skolemize ctxt th = blanchet@39904: try (skolemize ctxt) th blanchet@39900: |> tap (fn NONE => trace_msg (fn () => "Failed to skolemize " ^ blanchet@39900: Display.string_of_thm ctxt th) blanchet@39900: | _ => ()) paulson@25694: wenzelm@33339: fun add_clauses th cls = wenzelm@36603: let val ctxt0 = Variable.global_thm_context th wenzelm@33339: val (cnfs, ctxt) = make_cnf [] th ctxt0 paulson@24937: in Variable.export ctxt ctxt0 cnfs @ cls end; paulson@9840: paulson@9840: (*Make clauses from a list of theorems, previously Skolemized and put into nnf. paulson@9840: The resulting clauses are HOL disjunctions.*) wenzelm@39235: fun make_clauses_unsorted ths = fold_rev add_clauses ths []; blanchet@35869: val make_clauses = sort_clauses o make_clauses_unsorted; quigley@15773: paulson@16563: (*Convert a list of clauses (disjunctions) to Horn clauses (contrapositives)*) wenzelm@9869: fun make_horns ths = paulson@9840: name_thms "Horn#" wenzelm@33339: (distinct Thm.eq_thm_prop (fold_rev (add_contras clause_rules) ths [])); paulson@9840: paulson@9840: (*Could simply use nprems_of, which would count remaining subgoals -- no paulson@9840: discrimination as to their size! With BEST_FIRST, fails for problem 41.*) paulson@9840: wenzelm@9869: fun best_prolog_tac sizef horns = paulson@9840: BEST_FIRST (has_fewer_prems 1, sizef) (prolog_step_tac horns 1); paulson@9840: wenzelm@9869: fun depth_prolog_tac horns = paulson@9840: DEPTH_FIRST (has_fewer_prems 1) (prolog_step_tac horns 1); paulson@9840: paulson@9840: (*Return all negative clauses, as possible goal clauses*) paulson@9840: fun gocls cls = name_thms "Goal#" (map make_goal (neg_clauses cls)); paulson@9840: wenzelm@32262: fun skolemize_prems_tac ctxt prems = blanchet@39900: cut_facts_tac (map_filter (try_skolemize ctxt) prems) THEN' REPEAT o etac exE paulson@9840: paulson@22546: (*Basis of all meson-tactics. Supplies cltac with clauses: HOL disjunctions. paulson@22546: Function mkcl converts theorems to clauses.*) blanchet@39037: fun MESON preskolem_tac mkcl cltac ctxt i st = paulson@16588: SELECT_GOAL wenzelm@35625: (EVERY [Object_Logic.atomize_prems_tac 1, paulson@23552: rtac ccontr 1, blanchet@39269: preskolem_tac, wenzelm@32283: Subgoal.FOCUS (fn {context = ctxt', prems = negs, ...} => blanchet@39269: EVERY1 [skolemize_prems_tac ctxt negs, wenzelm@32283: Subgoal.FOCUS (cltac o mkcl o #prems) ctxt']) ctxt 1]) i st wenzelm@24300: handle THM _ => no_tac st; (*probably from make_meta_clause, not first-order*) paulson@9840: blanchet@39037: paulson@9840: (** Best-first search versions **) paulson@9840: paulson@16563: (*ths is a list of additional clauses (HOL disjunctions) to use.*) wenzelm@9869: fun best_meson_tac sizef = blanchet@39269: MESON all_tac make_clauses paulson@22546: (fn cls => paulson@9840: THEN_BEST_FIRST (resolve_tac (gocls cls) 1) paulson@9840: (has_fewer_prems 1, sizef) paulson@9840: (prolog_step_tac (make_horns cls) 1)); paulson@9840: paulson@9840: (*First, breaks the goal into independent units*) wenzelm@32262: fun safe_best_meson_tac ctxt = wenzelm@32262: SELECT_GOAL (TRY (safe_tac (claset_of ctxt)) THEN wenzelm@32262: TRYALL (best_meson_tac size_of_subgoals ctxt)); paulson@9840: paulson@9840: (** Depth-first search version **) paulson@9840: paulson@9840: val depth_meson_tac = blanchet@39269: MESON all_tac make_clauses paulson@22546: (fn cls => EVERY [resolve_tac (gocls cls) 1, depth_prolog_tac (make_horns cls)]); paulson@9840: paulson@9840: paulson@9840: (** Iterative deepening version **) paulson@9840: paulson@9840: (*This version does only one inference per call; paulson@9840: having only one eq_assume_tac speeds it up!*) wenzelm@9869: fun prolog_step_tac' horns = blanchet@39328: let val (horn0s, _) = (*0 subgoals vs 1 or more*) paulson@9840: take_prefix Thm.no_prems horns paulson@9840: val nrtac = net_resolve_tac horns paulson@9840: in fn i => eq_assume_tac i ORELSE paulson@9840: match_tac horn0s i ORELSE (*no backtracking if unit MATCHES*) paulson@9840: ((assume_tac i APPEND nrtac i) THEN check_tac) paulson@9840: end; paulson@9840: wenzelm@9869: fun iter_deepen_prolog_tac horns = wenzelm@38802: ITER_DEEPEN iter_deepen_limit (has_fewer_prems 1) (prolog_step_tac' horns); paulson@9840: blanchet@39269: fun iter_deepen_meson_tac ctxt ths = ctxt |> MESON all_tac make_clauses wenzelm@32091: (fn cls => wenzelm@32091: (case (gocls (cls @ ths)) of wenzelm@32091: [] => no_tac (*no goal clauses*) wenzelm@32091: | goes => wenzelm@32091: let wenzelm@32091: val horns = make_horns (cls @ ths) wenzelm@32955: val _ = trace_msg (fn () => wenzelm@32091: cat_lines ("meson method called:" :: wenzelm@32262: map (Display.string_of_thm ctxt) (cls @ ths) @ wenzelm@32262: ["clauses:"] @ map (Display.string_of_thm ctxt) horns)) wenzelm@38802: in wenzelm@38802: THEN_ITER_DEEPEN iter_deepen_limit wenzelm@38802: (resolve_tac goes 1) (has_fewer_prems 1) (prolog_step_tac' horns) wenzelm@38802: end)); paulson@9840: wenzelm@32262: fun meson_tac ctxt ths = wenzelm@32262: SELECT_GOAL (TRY (safe_tac (claset_of ctxt)) THEN TRYALL (iter_deepen_meson_tac ctxt ths)); wenzelm@9869: wenzelm@9869: paulson@14813: (**** Code to support ordinary resolution, rather than Model Elimination ****) paulson@14744: wenzelm@24300: (*Convert a list of clauses (disjunctions) to meta-level clauses (==>), paulson@15008: with no contrapositives, for ordinary resolution.*) paulson@14744: paulson@14744: (*Rules to convert the head literal into a negated assumption. If the head paulson@14744: literal is already negated, then using notEfalse instead of notEfalse' paulson@14744: prevents a double negation.*) wenzelm@27239: val notEfalse = read_instantiate @{context} [(("R", 0), "False")] notE; paulson@14744: val notEfalse' = rotate_prems 1 notEfalse; paulson@14744: wenzelm@24300: fun negated_asm_of_head th = paulson@14744: th RS notEfalse handle THM _ => th RS notEfalse'; paulson@14744: paulson@26066: (*Converting one theorem from a disjunction to a meta-level clause*) paulson@26066: fun make_meta_clause th = wenzelm@33832: let val (fth,thaw) = Drule.legacy_freeze_thaw_robust th paulson@26066: in wenzelm@35845: (zero_var_indexes o Thm.varifyT_global o thaw 0 o paulson@26066: negated_asm_of_head o make_horn resolution_clause_rules) fth paulson@26066: end; wenzelm@24300: paulson@14744: fun make_meta_clauses ths = paulson@14744: name_thms "MClause#" wenzelm@22360: (distinct Thm.eq_thm_prop (map make_meta_clause ths)); paulson@14744: paulson@9840: end;