# HG changeset patch # User blanchet # Date 1285940049 -7200 # Node ID 75d792edf634092a8e2c40a463ef9381cec928b3 # Parent 549c00e0e89b8a2a5330b8c919a6b86566adfb49 make "cnf_axiom" work (after a fashion) in the absence of the axiom of choice diff -r 549c00e0e89b -r 75d792edf634 src/HOL/Tools/Sledgehammer/meson_clausify.ML --- a/src/HOL/Tools/Sledgehammer/meson_clausify.ML Fri Oct 01 14:01:29 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/meson_clausify.ML Fri Oct 01 15:34:09 2010 +0200 @@ -14,7 +14,7 @@ val to_definitional_cnf_with_quantifiers : theory -> thm -> thm val cluster_of_zapped_var_name : string -> (int * int) * bool val cnf_axiom : - theory -> bool -> int -> thm -> (thm * term) option * thm list + Proof.context -> bool -> int -> thm -> (thm * term) option * thm list val meson_general_tac : Proof.context -> thm list -> int -> tactic val setup: theory -> theory end; @@ -281,13 +281,15 @@ #> 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]} +fun ss_only ths = MetaSimplifier.clear_ss HOL_basic_ss addsimps ths + +val no_choice = + @{prop "ALL x. EX y. Q x y ==> EX f. ALL x. Q x (f x)"} + |> Logic.varify_global + |> Skip_Proof.make_thm @{theory} (* Converts an Isabelle theorem into NNF. *) -fun nnf_axiom new_skolemizer ax_no th ctxt = +fun nnf_axiom choice_ths new_skolemizer ax_no th ctxt = let val thy = ProofContext.theory_of ctxt val th = @@ -301,10 +303,18 @@ 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 |> zap_quantifiers ax_no |> term_of + fun skolemize choice_ths = + Meson.skolemize ctxt choice_ths + #> simplify (ss_only @{thms all_simps[symmetric]}) + val pull_out = + simplify (ss_only @{thms all_simps[symmetric] ex_simps[symmetric]}) + val (discharger_th, fully_skolemized_th) = + if null choice_ths then + (th |> pull_out, th |> skolemize [no_choice]) + else + th |> skolemize choice_ths |> `I + val t = + fully_skolemized_th |> cprop_of |> zap_quantifiers ax_no |> term_of in if exists_subterm (fn Var ((s, _), _) => String.isPrefix new_skolem_var_prefix s @@ -313,7 +323,7 @@ val (ct, ctxt) = Variable.import_terms true [t] ctxt |>> the_single |>> cterm_of thy - in (SOME (th', ct), Thm.assume ct, ctxt) end + in (SOME (discharger_th, ct), Thm.assume ct, ctxt) end else (NONE, th, ctxt) end @@ -322,10 +332,11 @@ end (* Convert a theorem to CNF, with additional premises due to skolemization. *) -fun cnf_axiom thy new_skolemizer ax_no th = +fun cnf_axiom ctxt0 new_skolemizer ax_no th = let - val ctxt0 = Variable.global_thm_context th - val (opt, nnf_th, ctxt) = nnf_axiom new_skolemizer ax_no th ctxt0 + val thy = ProofContext.theory_of ctxt0 + val choice_ths = Meson_Choices.get ctxt0 + val (opt, nnf_th, ctxt) = nnf_axiom choice_ths new_skolemizer ax_no th ctxt0 fun clausify th = Meson.make_cnf (if new_skolemizer then [] @@ -356,10 +367,9 @@ 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 (snd o cnf_axiom thy false 0) ths) end + let val ctxt = Classical.put_claset HOL_cs ctxt in + Meson.meson_tac ctxt (maps (snd o cnf_axiom ctxt false 0) ths) + end val setup = Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn ctxt => diff -r 549c00e0e89b -r 75d792edf634 src/HOL/Tools/Sledgehammer/metis_tactics.ML --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Fri Oct 01 14:01:29 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Fri Oct 01 15:34:09 2010 +0200 @@ -182,10 +182,9 @@ handle Int_Pair_Graph.CYCLES _ => error "Cannot replay Metis proof in Isabelle without axiom of \ \choice." -(* +(* FIXME *) val _ = tracing ("SUBSTS: " ^ PolyML.makestring substs) val _ = tracing ("ORDERED: " ^ PolyML.makestring ordered_clusters) -*) in Goal.prove ctxt [] [] @{prop False} (K (cut_rules_tac (map fst axioms) 1 @@ -204,11 +203,12 @@ fun FOL_SOLVE mode ctxt cls ths0 = let val thy = ProofContext.theory_of ctxt val type_lits = Config.get ctxt type_lits - val new_skolemizer = Config.get ctxt new_skolemizer + val new_skolemizer = + Config.get ctxt new_skolemizer orelse null (Meson_Choices.get ctxt) val th_cls_pairs = map2 (fn j => fn th => (Thm.get_name_hint th, - Meson_Clausify.cnf_axiom thy new_skolemizer j th)) + Meson_Clausify.cnf_axiom ctxt new_skolemizer j th)) (0 upto length ths0 - 1) ths0 val thss = map (snd o snd) th_cls_pairs val dischargers = map_filter (fst o snd) th_cls_pairs diff -r 549c00e0e89b -r 75d792edf634 src/HOL/Tools/meson.ML --- a/src/HOL/Tools/meson.ML Fri Oct 01 14:01:29 2010 +0200 +++ b/src/HOL/Tools/meson.ML Fri Oct 01 15:34:09 2010 +0200 @@ -15,7 +15,7 @@ val finish_cnf: thm list -> thm list val presimplify: thm -> thm val make_nnf: Proof.context -> thm -> thm - val skolemize: Proof.context -> thm -> thm + val skolemize : Proof.context -> thm list -> thm -> thm val is_fol_term: theory -> term -> bool val make_clauses_unsorted: thm list -> thm list val make_clauses: thm list -> thm list @@ -39,7 +39,7 @@ val setup: theory -> theory end -structure Meson: MESON = +structure Meson : MESON = struct val trace = Unsynchronized.ref false; @@ -530,13 +530,13 @@ (* Pull existential quantifiers to front. This accomplishes Skolemization for clauses that arise from a subgoal. *) -fun skolemize ctxt = +fun skolemize ctxt choice_ths = let fun aux th = if not (has_conns [@{const_name Ex}] (prop_of th)) then th else - tryres (th, Meson_Choices.get ctxt @ + tryres (th, choice_ths @ [conj_exD1, conj_exD2, disj_exD, disj_exD1, disj_exD2]) |> aux handle THM ("tryres", _, _) => @@ -550,7 +550,7 @@ (* "RS" can fail if "unify_search_bound" is too small. *) fun try_skolemize ctxt th = - try (skolemize ctxt) th + try (skolemize ctxt (Meson_Choices.get ctxt)) th |> tap (fn NONE => trace_msg (fn () => "Failed to skolemize " ^ Display.string_of_thm ctxt th) | _ => ())