# HG changeset patch # User blanchet # Date 1285934489 -7200 # Node ID 549c00e0e89b8a2a5330b8c919a6b86566adfb49 # Parent 608b108ec9792c6e1fe3270002f6bc05bb7e659c added "meson_choice" attribute as a step towards making (less powerful versions of) Meson/Metis/Sledgehammer work without the axiom of choice diff -r 608b108ec979 -r 549c00e0e89b src/HOL/Hilbert_Choice.thy --- a/src/HOL/Hilbert_Choice.thy Fri Oct 01 12:01:07 2010 +0200 +++ b/src/HOL/Hilbert_Choice.thy Fri Oct 01 14:01:29 2010 +0200 @@ -81,8 +81,17 @@ subsection{*Axiom of Choice, Proved Using the Description Operator*} -text{*Used in @{text "Tools/meson.ML"}*} -lemma choice: "\x. \y. Q x y ==> \f. \x. Q x (f x)" +ML {* +structure Meson_Choices = Named_Thms +( + val name = "meson_choice" + val description = "choice axioms for MESON's (and Metis's) skolemizer" +) +*} + +setup Meson_Choices.setup + +lemma choice [meson_choice]: "\x. \y. Q x y ==> \f. \x. Q x (f x)" by (fast elim: someI) lemma bchoice: "\x\S. \y. Q x y ==> \f. \x\S. Q x (f x)" diff -r 608b108ec979 -r 549c00e0e89b src/HOL/Tools/Sledgehammer/meson_clausify.ML --- a/src/HOL/Tools/Sledgehammer/meson_clausify.ML Fri Oct 01 12:01:07 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/meson_clausify.ML Fri Oct 01 14:01:29 2010 +0200 @@ -281,6 +281,7 @@ #> cprop_of #> Thm.dest_equals #> snd end +(* FIXME: needed? and should we add ex_simps[symmetric]? *) val pull_out_quant_ss = MetaSimplifier.clear_ss HOL_basic_ss addsimps @{thms all_simps[symmetric]} diff -r 608b108ec979 -r 549c00e0e89b src/HOL/Tools/meson.ML --- a/src/HOL/Tools/meson.ML Fri Oct 01 12:01:07 2010 +0200 +++ b/src/HOL/Tools/meson.ML Fri Oct 01 14:01:29 2010 +0200 @@ -23,7 +23,7 @@ val best_prolog_tac: (thm -> int) -> thm list -> tactic val depth_prolog_tac: thm list -> tactic val gocls: thm list -> thm list - val skolemize_prems_tac: Proof.context -> thm list -> int -> tactic + val skolemize_prems_tac : Proof.context -> thm list -> int -> tactic val MESON: tactic -> (thm list -> thm list) -> (thm list -> tactic) -> Proof.context -> int -> tactic @@ -62,7 +62,6 @@ val conj_forward = @{thm conj_forward}; val all_forward = @{thm all_forward}; val ex_forward = @{thm ex_forward}; -val choice = @{thm choice}; val not_conjD = @{thm meson_not_conjD}; val not_disjD = @{thm meson_not_disjD}; @@ -523,33 +522,38 @@ addsimprocs [defALL_regroup,defEX_regroup, @{simproc neq}, @{simproc let_simp}]; val presimplify = - rewrite_rule (map safe_mk_meta_eq nnf_simps) - #> simplify nnf_ss + rewrite_rule (map safe_mk_meta_eq nnf_simps) #> simplify nnf_ss fun make_nnf ctxt th = case prems_of th of [] => th |> presimplify |> make_nnf1 ctxt | _ => raise THM ("make_nnf: premises in argument", 0, [th]); -(*Pull existential quantifiers to front. This accomplishes Skolemization for - clauses that arise from a subgoal.*) -fun skolemize1 ctxt th = - if not (has_conns [@{const_name Ex}] (prop_of th)) then th - else (skolemize1 ctxt (tryres(th, [choice, conj_exD1, conj_exD2, - disj_exD, disj_exD1, disj_exD2]))) - handle THM ("tryres", _, _) => - skolemize1 ctxt (forward_res ctxt (skolemize1 ctxt) - (tryres (th, [conj_forward, disj_forward, all_forward]))) - handle THM ("tryres", _, _) => - forward_res ctxt (skolemize1 ctxt) (rename_bvs_RS th ex_forward); +(* Pull existential quantifiers to front. This accomplishes Skolemization for + clauses that arise from a subgoal. *) +fun skolemize ctxt = + let + fun aux th = + if not (has_conns [@{const_name Ex}] (prop_of th)) then + th + else + tryres (th, Meson_Choices.get ctxt @ + [conj_exD1, conj_exD2, disj_exD, disj_exD1, disj_exD2]) + |> aux + handle THM ("tryres", _, _) => + tryres (th, [conj_forward, disj_forward, all_forward]) + |> forward_res ctxt aux + |> aux + handle THM ("tryres", _, _) => + rename_bvs_RS th ex_forward + |> forward_res ctxt aux + in aux o make_nnf ctxt end -fun skolemize ctxt th = skolemize1 ctxt (make_nnf ctxt th); - -fun skolemize_nnf_list _ [] = [] - | skolemize_nnf_list ctxt (th::ths) = - skolemize ctxt th :: skolemize_nnf_list ctxt ths - handle THM _ => (*RS can fail if Unify.search_bound is too small*) - (trace_msg (fn () => "Failed to Skolemize " ^ Display.string_of_thm ctxt th); - skolemize_nnf_list ctxt ths); +(* "RS" can fail if "unify_search_bound" is too small. *) +fun try_skolemize ctxt th = + try (skolemize ctxt) th + |> tap (fn NONE => trace_msg (fn () => "Failed to skolemize " ^ + Display.string_of_thm ctxt th) + | _ => ()) fun add_clauses th cls = let val ctxt0 = Variable.global_thm_context th @@ -579,7 +583,7 @@ fun gocls cls = name_thms "Goal#" (map make_goal (neg_clauses cls)); fun skolemize_prems_tac ctxt prems = - cut_facts_tac (skolemize_nnf_list ctxt prems) THEN' REPEAT o etac exE + cut_facts_tac (map_filter (try_skolemize ctxt) prems) THEN' REPEAT o etac exE (*Basis of all meson-tactics. Supplies cltac with clauses: HOL disjunctions. Function mkcl converts theorems to clauses.*)