# HG changeset patch # User blanchet # Date 1285794362 -7200 # Node ID 74939e2afb959317c530eba0ac67f67d2a82de77 # Parent 8a9f0c97d5500099fcb70beff4447d43f42717d5 second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions diff -r 8a9f0c97d550 -r 74939e2afb95 src/HOL/Tools/Sledgehammer/meson_clausifier.ML --- a/src/HOL/Tools/Sledgehammer/meson_clausifier.ML Wed Sep 29 22:23:27 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/meson_clausifier.ML Wed Sep 29 23:06:02 2010 +0200 @@ -8,11 +8,12 @@ signature MESON_CLAUSIFIER = sig val new_skolemizer : bool Config.T + val new_skolem_var_prefix : string val extensionalize_theorem : thm -> thm val introduce_combinators_in_cterm : cterm -> thm val introduce_combinators_in_theorem : thm -> thm val to_definitional_cnf_with_quantifiers : theory -> thm -> thm - val cnf_axiom : theory -> thm -> thm list + val cnf_axiom : theory -> thm -> thm option * thm list val meson_general_tac : Proof.context -> thm list -> int -> tactic val setup: theory -> theory end; @@ -23,6 +24,8 @@ val (new_skolemizer, new_skolemizer_setup) = Attrib.config_bool "meson_new_skolemizer" (K false) +val new_skolem_var_prefix = "SK?" (* purposedly won't parse *) + (**** Transformation of Elimination Rules into First-Order Formulas****) val cfalse = cterm_of @{theory HOL} HOLogic.false_const; @@ -220,17 +223,6 @@ |> Thm.varifyT_global end -(* Converts an Isabelle theorem (intro, elim or simp format, even higher-order) - into NNF. *) -fun nnf_axiom th ctxt0 = - let - val th1 = th |> transform_elim_theorem |> zero_var_indexes - val ((_, [th2]), ctxt) = Variable.import true [th1] ctxt0 - val th3 = th2 |> Conv.fconv_rule Object_Logic.atomize - |> extensionalize_theorem - |> Meson.make_nnf ctxt - in (th3, ctxt) end - fun to_definitional_cnf_with_quantifiers thy th = let val eqth = cnf.make_cnfx_thm thy (HOLogic.dest_Trueprop (prop_of th)) @@ -238,35 +230,120 @@ val eqth = eqth RS @{thm TruepropI} in Thm.equal_elim eqth th end -(* Convert a theorem to CNF, with Skolem functions as additional premises. *) +val kill_quantifiers = + let + fun conv pos ct = + ct |> (case term_of ct of + Const (s, _) $ Abs (s', _, _) => + if s = @{const_name all} orelse s = @{const_name All} orelse + s = @{const_name Ex} then + Thm.dest_comb #> snd + #> Thm.dest_abs (SOME (s' |> pos = (s = @{const_name Ex}) + ? prefix new_skolem_var_prefix)) + #> snd #> conv pos + else + Conv.all_conv + | Const (s, _) $ _ $ _ => + if s = @{const_name "==>"} orelse + s = @{const_name HOL.implies} then + Conv.combination_conv (Conv.arg_conv (conv (not pos))) + (conv pos) + else if s = @{const_name HOL.conj} orelse + s = @{const_name HOL.disj} then + Conv.combination_conv (Conv.arg_conv (conv pos)) (conv pos) + else + Conv.all_conv + | Const (s, _) $ _ => + if s = @{const_name Trueprop} then + Conv.arg_conv (conv pos) + else if s = @{const_name Not} then + Conv.arg_conv (conv (not pos)) + else + Conv.all_conv + | _ => Conv.all_conv) + in + conv true #> Drule.export_without_context + #> cprop_of #> Thm.dest_equals #> snd + end + +val pull_out_quant_ss = + MetaSimplifier.clear_ss HOL_basic_ss + addsimps @{thms all_simps[symmetric]} + +(* Converts an Isabelle theorem into NNF. *) +fun nnf_axiom new_skolemizer th ctxt = + let + val thy = ProofContext.theory_of ctxt + val th = + th |> transform_elim_theorem + |> zero_var_indexes + |> new_skolemizer ? forall_intr_vars + val (th, ctxt) = Variable.import true [th] ctxt |>> snd |>> the_single + val th = th |> Conv.fconv_rule Object_Logic.atomize + |> extensionalize_theorem + |> Meson.make_nnf ctxt + in + if new_skolemizer then + let + val th' = th |> Meson.skolemize ctxt + |> simplify pull_out_quant_ss + |> Drule.eta_contraction_rule + val t = th' |> cprop_of |> kill_quantifiers |> term_of + in + if exists_subterm (fn Var ((s, _), _) => + String.isPrefix new_skolem_var_prefix s + | _ => false) t then + let + val (ct, ctxt) = + Variable.import_terms true [t] ctxt + |>> the_single |>> cterm_of thy + in (SOME (th', ct), ct |> Thm.assume, ctxt) end + else + (NONE, th, ctxt) + end + else + (NONE, th, ctxt) + end + +(* Convert a theorem to CNF, with additional premises due to skolemization. *) fun cnf_axiom thy th = let val ctxt0 = Variable.global_thm_context th - val (nnf_th, ctxt) = nnf_axiom th ctxt0 + val new_skolemizer = Config.get ctxt0 new_skolemizer + val (opt, nnf_th, ctxt) = nnf_axiom new_skolemizer th ctxt0 fun aux th = - Meson.make_cnf (map (old_skolem_theorem_from_def thy) - (old_skolem_defs th)) th ctxt + Meson.make_cnf (if new_skolemizer then + [] + else + map (old_skolem_theorem_from_def thy) + (old_skolem_defs th)) th ctxt val (cnf_ths, ctxt) = aux nnf_th |> (fn ([], _) => aux (to_definitional_cnf_with_quantifiers thy nnf_th) | p => p) + val export = Variable.export ctxt ctxt0 in - cnf_ths |> map introduce_combinators_in_theorem - |> Variable.export ctxt ctxt0 - |> Meson.finish_cnf - |> map Thm.close_derivation + (opt |> Option.map (singleton export o fst), + cnf_ths |> map (introduce_combinators_in_theorem + #> (case opt of + SOME (_, ct) => Thm.implies_intr ct + | NONE => I)) + |> export + |> Meson.finish_cnf + |> map Thm.close_derivation) end - handle THM _ => [] + handle THM _ => (NONE, []) fun meson_general_tac ctxt ths = let val thy = ProofContext.theory_of ctxt val ctxt0 = Classical.put_claset HOL_cs ctxt - in Meson.meson_tac ctxt0 (maps (cnf_axiom thy) ths) end + in Meson.meson_tac ctxt0 (maps (snd o cnf_axiom thy) ths) end val setup = - Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn ctxt => - SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ctxt ths))) - "MESON resolution proof procedure"; + new_skolemizer_setup + #> Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn ctxt => + SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ctxt ths))) + "MESON resolution proof procedure" end; diff -r 8a9f0c97d550 -r 74939e2afb95 src/HOL/Tools/Sledgehammer/metis_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/metis_reconstruct.ML Wed Sep 29 22:23:27 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/metis_reconstruct.ML Wed Sep 29 23:06:02 2010 +0200 @@ -13,6 +13,7 @@ val trace : bool Unsynchronized.ref val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a + val untyped_aconv : term -> term -> bool val replay_one_inference : Proof.context -> mode -> (string * term) list -> Metis_Thm.thm * Metis_Proof.inference -> (Metis_Thm.thm * thm) list diff -r 8a9f0c97d550 -r 74939e2afb95 src/HOL/Tools/Sledgehammer/metis_tactics.ML --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Wed Sep 29 22:23:27 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Wed Sep 29 23:06:02 2010 +0200 @@ -51,6 +51,98 @@ models = []} val resolution_params = {active = active_params, waiting = waiting_params} +(* In principle, it should be sufficient to apply "assume_tac" to unify the + conclusion with one of the premises. However, in practice, this fails + horribly because of the mildly higher-order nature of the unification + problems. Typical constraints are of the form "?x a b =?= b", where "a" and + "b" are goal parameters. *) +fun unify_one_prem_with_concl thy i th = + let + val goal = Logic.get_goal (prop_of th) i |> Envir.beta_eta_contract + val prems = Logic.strip_assums_hyp goal + val concl = Logic.strip_assums_concl goal + fun add_types Tp instT = + if exists (curry (op =) Tp) instT then instT + else Tp :: map (apsnd (typ_subst_atomic [Tp])) instT + fun unify_types (T, U) = + if T = U then + I + else case (T, U) of + (TVar _, _) => add_types (T, U) + | (_, TVar _) => add_types (U, T) + | (Type (s, Ts), Type (t, Us)) => + if s = t andalso length Ts = length Us then fold unify_types (Ts ~~ Us) + else raise TYPE ("unify_types", [T, U], []) + | _ => raise TYPE ("unify_types", [T, U], []) + fun pair_untyped_aconv (t1, t2) (u1, u2) = + untyped_aconv t1 u1 andalso untyped_aconv t2 u2 + fun add_terms tp inst = + if exists (pair_untyped_aconv tp) inst then inst + else tp :: map (apsnd (subst_atomic [tp])) inst + fun is_flex t = + case strip_comb t of + (Var _, args) => forall (is_Bound orf is_Var orf is_Free) args + | _ => false + fun unify_flex flex rigid = + case strip_comb flex of + (Var (z as (_, T)), args) => + add_terms (Var z, + (* FIXME: reindex bound variables *) + fold_rev (curry absdummy) (take (length args) (binder_types T)) rigid) + | _ => raise TERM ("unify_flex: expected flex", [flex]) + fun unify_potential_flex comb atom = + if is_flex comb then unify_flex comb atom + else if is_Var atom then add_terms (atom, comb) + else raise TERM ("unify_terms", [comb, atom]) + fun unify_terms (t, u) = + case (t, u) of + (t1 $ t2, u1 $ u2) => + if is_flex t then unify_flex t u + else if is_flex u then unify_flex u t + else fold unify_terms [(t1, u1), (t2, u2)] + | (_ $ _, _) => unify_potential_flex t u + | (_, _ $ _) => unify_potential_flex u t + | (Var _, _) => add_terms (t, u) + | (_, Var _) => add_terms (u, t) + | _ => if untyped_aconv t u then I else raise TERM ("unify_terms", [t, u]) + fun unify_prem prem = + let + val inst = [] |> unify_terms (prem, concl) + val instT = fold (unify_types o pairself fastype_of) inst [] + val inst = inst |> map (pairself (subst_atomic_types instT)) + val cinstT = instT |> map (pairself (ctyp_of thy)) + val cinst = inst |> map (pairself (cterm_of thy)) + in th |> Thm.instantiate (cinstT, []) |> Thm.instantiate ([], cinst) end + in + case prems of + [prem] => unify_prem prem + | _ => + case fold (fn prem => fn th as SOME _ => th + | NONE => try unify_prem prem) prems NONE of + SOME th => th + | NONE => raise Fail "unify_one_prem_with_concl" + end + +(* Attempts to derive the theorem "False" from a theorem of the form + "P1 ==> ... ==> Pn ==> False", where the "Pi"s are to be discharged using the + specified axioms. The axioms have leading "All" and "Ex" quantifiers, which + must be eliminated first. *) +fun discharge_skolem_premises ctxt axioms premises_imp_false = + if prop_of premises_imp_false aconv @{prop False} then + premises_imp_false + else + let val thy = ProofContext.theory_of ctxt in + Goal.prove ctxt [] [] @{prop False} + (K (cut_rules_tac axioms 1 + THEN TRY (REPEAT_ALL_NEW (etac @{thm exE}) 1) +(* FIXME: THEN etac @{lemma "P ==> (P ==> P ==> Q) ==> Q" by fast} 1 *) + THEN TRY (REPEAT_ALL_NEW (etac @{thm allE}) 1) + THEN match_tac [premises_imp_false] 1 + THEN DETERM_UNTIL_SOLVED + (PRIMITIVE (unify_one_prem_with_concl thy 1) + THEN assume_tac 1))) + end + (* Main function to start Metis proof and reconstruction *) fun FOL_SOLVE mode ctxt cls ths0 = let val thy = ProofContext.theory_of ctxt @@ -58,7 +150,8 @@ val th_cls_pairs = map (fn th => (Thm.get_name_hint th, Meson_Clausifier.cnf_axiom thy th)) ths0 - val thss = map #2 th_cls_pairs + val thss = map (snd o snd) th_cls_pairs + val dischargers = map_filter (fst o snd) th_cls_pairs val _ = trace_msg (fn () => "FOL_SOLVE: CONJECTURE CLAUSES") val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) cls val _ = trace_msg (fn () => "THEOREM CLAUSES") @@ -68,7 +161,7 @@ val _ = if null tfrees then () else (trace_msg (fn () => "TFREE CLAUSES"); app (fn TyLitFree ((s, _), (s', _)) => - trace_msg (fn _ => s ^ "(" ^ s' ^ ")")) tfrees) + trace_msg (fn () => s ^ "(" ^ s' ^ ")")) tfrees) val _ = trace_msg (fn () => "CLAUSES GIVEN TO METIS") val thms = map #1 axioms val _ = app (fn th => trace_msg (fn () => Metis_Thm.toString th)) thms @@ -91,7 +184,7 @@ and used = map_filter (used_axioms axioms) proof val _ = trace_msg (fn () => "METIS COMPLETED...clauses actually used:") val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) used - val unused = th_cls_pairs |> map_filter (fn (name, cls) => + val unused = th_cls_pairs |> map_filter (fn (name, (_, cls)) => if have_common_thm used cls then NONE else SOME name) in if not (null cls) andalso not (have_common_thm used cls) then @@ -106,7 +199,7 @@ case result of (_,ith)::_ => (trace_msg (fn () => "Success: " ^ Display.string_of_thm ctxt ith); - [ith]) + [discharge_skolem_premises ctxt dischargers ith]) | _ => (trace_msg (fn () => "Metis: No result"); []) end | Metis_Resolution.Satisfiable _ => diff -r 8a9f0c97d550 -r 74939e2afb95 src/HOL/Tools/Sledgehammer/metis_translate.ML --- a/src/HOL/Tools/Sledgehammer/metis_translate.ML Wed Sep 29 22:23:27 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/metis_translate.ML Wed Sep 29 23:06:02 2010 +0200 @@ -95,8 +95,6 @@ val type_const_prefix = "tc_"; val class_prefix = "class_"; -val new_skolem_var_prefix = "SK?" (* purposedly won't parse *) - val skolem_prefix = "Sledgehammer" ^ Long_Name.separator ^ "Sko" val old_skolem_prefix = skolem_prefix ^ "o" val new_skolem_prefix = skolem_prefix ^ "n" @@ -427,7 +425,7 @@ let val (tp, ts) = combtype_of T val v' = - if String.isPrefix new_skolem_var_prefix s then + if String.isPrefix Meson_Clausifier.new_skolem_var_prefix s then let val tys = T |> strip_type |> swap |> op :: val s' = new_skolem_name th_no s (length tys)