--- 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 =>
--- 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
--- 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)
| _ => ())