--- a/src/HOL/Hilbert_Choice.thy Fri Oct 01 14:15:49 2010 +0200
+++ b/src/HOL/Hilbert_Choice.thy Fri Oct 01 16:13:28 2010 +0200
@@ -81,8 +81,17 @@
subsection{*Axiom of Choice, Proved Using the Description Operator*}
-text{*Used in @{text "Tools/meson.ML"}*}
-lemma choice: "\<forall>x. \<exists>y. Q x y ==> \<exists>f. \<forall>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]: "\<forall>x. \<exists>y. Q x y ==> \<exists>f. \<forall>x. Q x (f x)"
by (fast elim: someI)
lemma bchoice: "\<forall>x\<in>S. \<exists>y. Q x y ==> \<exists>f. \<forall>x\<in>S. Q x (f x)"
--- a/src/HOL/IsaMakefile Fri Oct 01 14:15:49 2010 +0200
+++ b/src/HOL/IsaMakefile Fri Oct 01 16:13:28 2010 +0200
@@ -315,7 +315,7 @@
Tools/recdef.ML \
Tools/record.ML \
Tools/semiring_normalizer.ML \
- Tools/Sledgehammer/meson_clausifier.ML \
+ Tools/Sledgehammer/meson_clausify.ML \
Tools/Sledgehammer/metis_reconstruct.ML \
Tools/Sledgehammer/metis_translate.ML \
Tools/Sledgehammer/metis_tactics.ML \
--- a/src/HOL/Sledgehammer.thy Fri Oct 01 14:15:49 2010 +0200
+++ b/src/HOL/Sledgehammer.thy Fri Oct 01 16:13:28 2010 +0200
@@ -14,7 +14,7 @@
("Tools/ATP/atp_proof.ML")
("Tools/ATP/atp_systems.ML")
("~~/src/Tools/Metis/metis.ML")
- ("Tools/Sledgehammer/meson_clausifier.ML")
+ ("Tools/Sledgehammer/meson_clausify.ML")
("Tools/Sledgehammer/metis_translate.ML")
("Tools/Sledgehammer/metis_reconstruct.ML")
("Tools/Sledgehammer/metis_tactics.ML")
@@ -60,6 +60,12 @@
lemma equal_imp_equal [no_atp]: "X = Y ==> X = Y"
by auto
+lemma skolem_COMBK_iff: "P \<longleftrightarrow> skolem (COMBK P (i\<Colon>nat))"
+unfolding skolem_def COMBK_def by (rule refl)
+
+lemmas skolem_COMBK_I = iffD1 [OF skolem_COMBK_iff]
+lemmas skolem_COMBK_D = iffD2 [OF skolem_COMBK_iff]
+
text{*Theorems for translation to combinators*}
lemma abs_S [no_atp]: "\<lambda>x. (f x) (g x) \<equiv> COMBS f g"
@@ -98,8 +104,8 @@
setup ATP_Systems.setup
use "~~/src/Tools/Metis/metis.ML"
-use "Tools/Sledgehammer/meson_clausifier.ML"
-setup Meson_Clausifier.setup
+use "Tools/Sledgehammer/meson_clausify.ML"
+setup Meson_Clausify.setup
use "Tools/Sledgehammer/metis_translate.ML"
use "Tools/Sledgehammer/metis_reconstruct.ML"
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Fri Oct 01 14:15:49 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Fri Oct 01 16:13:28 2010 +0200
@@ -49,8 +49,6 @@
structure KK = Kodkod
-structure NfaGraph = Typ_Graph
-
fun pull x xs = x :: filter_out (curry (op =) x) xs
fun is_datatype_acyclic ({co = false, standard = true, deep = true, ...}
@@ -720,19 +718,16 @@
kk_union (loop_path_rel_expr kk nfa Ts start_T)
(knot_path_rel_expr kk nfa Ts start_T T start_T)
-fun graph_for_nfa nfa =
- let
- fun new_node T = perhaps (try (NfaGraph.new_node (T, ())))
- fun add_nfa [] = I
- | add_nfa ((_, []) :: nfa) = add_nfa nfa
- | add_nfa ((T, ((_, T') :: transitions)) :: nfa) =
- add_nfa ((T, transitions) :: nfa) o NfaGraph.add_edge (T, T') o
- new_node T' o new_node T
- in add_nfa nfa NfaGraph.empty end
+fun add_nfa_to_graph [] = I
+ | add_nfa_to_graph ((_, []) :: nfa) = add_nfa_to_graph nfa
+ | add_nfa_to_graph ((T, ((_, T') :: transitions)) :: nfa) =
+ add_nfa_to_graph ((T, transitions) :: nfa) o Typ_Graph.add_edge (T, T') o
+ Typ_Graph.default_node (T', ()) o Typ_Graph.default_node (T, ())
fun strongly_connected_sub_nfas nfa =
- nfa |> graph_for_nfa |> NfaGraph.strong_conn
- |> map (fn keys => filter (member (op =) keys o fst) nfa)
+ add_nfa_to_graph nfa Typ_Graph.empty
+ |> Typ_Graph.strong_conn
+ |> map (fn keys => filter (member (op =) keys o fst) nfa)
fun acyclicity_axiom_for_datatype (kk as {kk_no, kk_intersect, ...}) nfa
start_T =
--- a/src/HOL/Tools/Sledgehammer/meson_clausifier.ML Fri Oct 01 14:15:49 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,267 +0,0 @@
-(* Title: HOL/Tools/Sledgehammer/clausifier.ML
- Author: Jia Meng, Cambridge University Computer Laboratory and NICTA
- Author: Jasmin Blanchette, TU Muenchen
-
-Transformation of axiom rules (elim/intro/etc) into CNF forms.
-*)
-
-signature MESON_CLAUSIFIER =
-sig
- 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 meson_cnf_axiom : theory -> thm -> thm list
- val meson_general_tac : Proof.context -> thm list -> int -> tactic
- val setup: theory -> theory
-end;
-
-structure Meson_Clausifier : MESON_CLAUSIFIER =
-struct
-
-(**** Transformation of Elimination Rules into First-Order Formulas****)
-
-val cfalse = cterm_of @{theory HOL} HOLogic.false_const;
-val ctp_false = cterm_of @{theory HOL} (HOLogic.mk_Trueprop HOLogic.false_const);
-
-(* Converts an elim-rule into an equivalent theorem that does not have the
- predicate variable. Leaves other theorems unchanged. We simply instantiate
- the conclusion variable to False. (Cf. "transform_elim_term" in
- "Sledgehammer_Util".) *)
-fun transform_elim_theorem th =
- case concl_of th of (*conclusion variable*)
- @{const Trueprop} $ (v as Var (_, @{typ bool})) =>
- Thm.instantiate ([], [(cterm_of @{theory HOL} v, cfalse)]) th
- | v as Var(_, @{typ prop}) =>
- Thm.instantiate ([], [(cterm_of @{theory HOL} v, ctp_false)]) th
- | _ => th
-
-
-(**** SKOLEMIZATION BY INFERENCE (lcp) ****)
-
-fun mk_skolem t =
- let val T = fastype_of t in
- Const (@{const_name skolem}, T --> T) $ t
- end
-
-fun beta_eta_under_lambdas (Abs (s, T, t')) =
- Abs (s, T, beta_eta_under_lambdas t')
- | beta_eta_under_lambdas t = Envir.beta_eta_contract t
-
-(*Traverse a theorem, accumulating Skolem function definitions.*)
-fun assume_skolem_funs th =
- let
- fun dec_sko (Const (@{const_name Ex}, _) $ (body as Abs (_, T, p))) rhss =
- (*Existential: declare a Skolem function, then insert into body and continue*)
- let
- val args = OldTerm.term_frees body
- (* Forms a lambda-abstraction over the formal parameters *)
- val rhs =
- list_abs_free (map dest_Free args,
- HOLogic.choice_const T $ beta_eta_under_lambdas body)
- |> mk_skolem
- val comb = list_comb (rhs, args)
- in dec_sko (subst_bound (comb, p)) (rhs :: rhss) end
- | dec_sko (Const (@{const_name All},_) $ Abs (a, T, p)) rhss =
- (*Universal quant: insert a free variable into body and continue*)
- let val fname = Name.variant (OldTerm.add_term_names (p,[])) a
- in dec_sko (subst_bound (Free(fname,T), p)) rhss end
- | dec_sko (@{const HOL.conj} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
- | dec_sko (@{const HOL.disj} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
- | dec_sko (@{const Trueprop} $ p) rhss = dec_sko p rhss
- | dec_sko _ rhss = rhss
- in dec_sko (prop_of th) [] end;
-
-
-(**** REPLACING ABSTRACTIONS BY COMBINATORS ****)
-
-val fun_cong_all = @{thm fun_eq_iff [THEN iffD1]}
-
-(* Removes the lambdas from an equation of the form "t = (%x. u)".
- (Cf. "extensionalize_term" in "Sledgehammer_Translate".) *)
-fun extensionalize_theorem th =
- case prop_of th of
- _ $ (Const (@{const_name HOL.eq}, Type (_, [Type (@{type_name fun}, _), _]))
- $ _ $ Abs _) => extensionalize_theorem (th RS fun_cong_all)
- | _ => th
-
-fun is_quasi_lambda_free (Const (@{const_name skolem}, _) $ _) = true
- | is_quasi_lambda_free (t1 $ t2) =
- is_quasi_lambda_free t1 andalso is_quasi_lambda_free t2
- | is_quasi_lambda_free (Abs _) = false
- | is_quasi_lambda_free _ = true
-
-val [f_B,g_B] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_B}));
-val [g_C,f_C] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_C}));
-val [f_S,g_S] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_S}));
-
-(* FIXME: Requires more use of cterm constructors. *)
-fun abstract ct =
- let
- val thy = theory_of_cterm ct
- val Abs(x,_,body) = term_of ct
- val Type(@{type_name fun}, [xT,bodyT]) = typ_of (ctyp_of_term ct)
- val cxT = ctyp_of thy xT
- val cbodyT = ctyp_of thy bodyT
- fun makeK () =
- instantiate' [SOME cxT, SOME cbodyT] [SOME (cterm_of thy body)]
- @{thm abs_K}
- in
- case body of
- Const _ => makeK()
- | Free _ => makeK()
- | Var _ => makeK() (*though Var isn't expected*)
- | Bound 0 => instantiate' [SOME cxT] [] @{thm abs_I} (*identity: I*)
- | rator$rand =>
- if loose_bvar1 (rator,0) then (*C or S*)
- if loose_bvar1 (rand,0) then (*S*)
- let val crator = cterm_of thy (Abs(x,xT,rator))
- val crand = cterm_of thy (Abs(x,xT,rand))
- val abs_S' = cterm_instantiate [(f_S,crator),(g_S,crand)] @{thm abs_S}
- val (_,rhs) = Thm.dest_equals (cprop_of abs_S')
- in
- Thm.transitive abs_S' (Conv.binop_conv abstract rhs)
- end
- else (*C*)
- let val crator = cterm_of thy (Abs(x,xT,rator))
- val abs_C' = cterm_instantiate [(f_C,crator),(g_C,cterm_of thy rand)] @{thm abs_C}
- val (_,rhs) = Thm.dest_equals (cprop_of abs_C')
- in
- Thm.transitive abs_C' (Conv.fun_conv (Conv.arg_conv abstract) rhs)
- end
- else if loose_bvar1 (rand,0) then (*B or eta*)
- if rand = Bound 0 then Thm.eta_conversion ct
- else (*B*)
- let val crand = cterm_of thy (Abs(x,xT,rand))
- val crator = cterm_of thy rator
- val abs_B' = cterm_instantiate [(f_B,crator),(g_B,crand)] @{thm abs_B}
- val (_,rhs) = Thm.dest_equals (cprop_of abs_B')
- in Thm.transitive abs_B' (Conv.arg_conv abstract rhs) end
- else makeK()
- | _ => raise Fail "abstract: Bad term"
- end;
-
-(* Traverse a theorem, remplacing lambda-abstractions with combinators. *)
-fun introduce_combinators_in_cterm ct =
- if is_quasi_lambda_free (term_of ct) then
- Thm.reflexive ct
- else case term_of ct of
- Abs _ =>
- let
- val (cv, cta) = Thm.dest_abs NONE ct
- val (v, _) = dest_Free (term_of cv)
- val u_th = introduce_combinators_in_cterm cta
- val cu = Thm.rhs_of u_th
- val comb_eq = abstract (Thm.cabs cv cu)
- in Thm.transitive (Thm.abstract_rule v cv u_th) comb_eq end
- | _ $ _ =>
- let val (ct1, ct2) = Thm.dest_comb ct in
- Thm.combination (introduce_combinators_in_cterm ct1)
- (introduce_combinators_in_cterm ct2)
- end
-
-fun introduce_combinators_in_theorem th =
- if is_quasi_lambda_free (prop_of th) then
- th
- else
- let
- val th = Drule.eta_contraction_rule th
- val eqth = introduce_combinators_in_cterm (cprop_of th)
- in Thm.equal_elim eqth th end
- handle THM (msg, _, _) =>
- (warning ("Error in the combinator translation of " ^
- Display.string_of_thm_without_context th ^
- "\nException message: " ^ msg ^ ".");
- (* A type variable of sort "{}" will make abstraction fail. *)
- TrueI)
-
-(*cterms are used throughout for efficiency*)
-val cTrueprop = cterm_of @{theory HOL} HOLogic.Trueprop;
-
-(*Given an abstraction over n variables, replace the bound variables by free
- ones. Return the body, along with the list of free variables.*)
-fun c_variant_abs_multi (ct0, vars) =
- let val (cv,ct) = Thm.dest_abs NONE ct0
- in c_variant_abs_multi (ct, cv::vars) end
- handle CTERM _ => (ct0, rev vars);
-
-val skolem_def_raw = @{thms skolem_def_raw}
-
-(* Given the definition of a Skolem function, return a theorem to replace
- an existential formula by a use of that function.
- Example: "EX x. x : A & x ~: B ==> sko A B : A & sko A B ~: B" [.] *)
-fun skolem_theorem_of_def thy rhs0 =
- let
- val rhs = rhs0 |> Type.legacy_freeze_thaw |> #1 |> cterm_of thy
- val rhs' = rhs |> Thm.dest_comb |> snd
- val (ch, frees) = c_variant_abs_multi (rhs', [])
- val (hilbert, cabs) = ch |> Thm.dest_comb |>> term_of
- val T =
- case hilbert of
- Const (@{const_name Eps}, Type (@{type_name fun}, [_, T])) => T
- | _ => raise TERM ("skolem_theorem_of_def: expected \"Eps\"", [hilbert])
- val cex = cterm_of thy (HOLogic.exists_const T)
- val ex_tm = Thm.capply cTrueprop (Thm.capply cex cabs)
- val conc =
- Drule.list_comb (rhs, frees)
- |> Drule.beta_conv cabs |> Thm.capply cTrueprop
- fun tacf [prem] =
- rewrite_goals_tac skolem_def_raw
- THEN rtac ((prem |> rewrite_rule skolem_def_raw) RS @{thm someI_ex}) 1
- in
- Goal.prove_internal [ex_tm] conc tacf
- |> forall_intr_list frees
- |> Thm.forall_elim_vars 0 (*Introduce Vars, but don't discharge defs.*)
- |> Thm.varifyT_global
- end
-
-(* Converts an Isabelle theorem (intro, elim or simp format, even higher-order)
- into NNF. *)
-fun to_nnf 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))
- val eqth = eqth RS @{thm eq_reflection}
- val eqth = eqth RS @{thm TruepropI}
- in Thm.equal_elim eqth th end
-
-(* Convert a theorem to CNF, with Skolem functions as additional premises. *)
-fun meson_cnf_axiom thy th =
- let
- val ctxt0 = Variable.global_thm_context th
- val (nnf_th, ctxt) = to_nnf th ctxt0
- fun aux th =
- Meson.make_cnf (map (skolem_theorem_of_def thy) (assume_skolem_funs th))
- th ctxt
- val (cnf_ths, ctxt) =
- aux nnf_th
- |> (fn ([], _) => aux (to_definitional_cnf_with_quantifiers thy nnf_th)
- | p => p)
- in
- cnf_ths |> map introduce_combinators_in_theorem
- |> Variable.export ctxt ctxt0
- |> Meson.finish_cnf
- |> map Thm.close_derivation
- end
- handle THM _ => []
-
-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 (meson_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";
-
-end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Sledgehammer/meson_clausify.ML Fri Oct 01 16:13:28 2010 +0200
@@ -0,0 +1,379 @@
+(* Title: HOL/Tools/Sledgehammer/meson_clausify.ML
+ Author: Jia Meng, Cambridge University Computer Laboratory and NICTA
+ Author: Jasmin Blanchette, TU Muenchen
+
+Transformation of axiom rules (elim/intro/etc) into CNF forms.
+*)
+
+signature MESON_CLAUSIFY =
+sig
+ 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 cluster_of_zapped_var_name : string -> (int * int) * bool
+ val cnf_axiom :
+ 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;
+
+structure Meson_Clausify : MESON_CLAUSIFY =
+struct
+
+(* the extra "?" helps prevent clashes *)
+val new_skolem_var_prefix = "?SK"
+val new_nonskolem_var_prefix = "?V"
+
+(**** Transformation of Elimination Rules into First-Order Formulas****)
+
+val cfalse = cterm_of @{theory HOL} HOLogic.false_const;
+val ctp_false = cterm_of @{theory HOL} (HOLogic.mk_Trueprop HOLogic.false_const);
+
+(* Converts an elim-rule into an equivalent theorem that does not have the
+ predicate variable. Leaves other theorems unchanged. We simply instantiate
+ the conclusion variable to False. (Cf. "transform_elim_term" in
+ "Sledgehammer_Util".) *)
+fun transform_elim_theorem th =
+ case concl_of th of (*conclusion variable*)
+ @{const Trueprop} $ (v as Var (_, @{typ bool})) =>
+ Thm.instantiate ([], [(cterm_of @{theory HOL} v, cfalse)]) th
+ | v as Var(_, @{typ prop}) =>
+ Thm.instantiate ([], [(cterm_of @{theory HOL} v, ctp_false)]) th
+ | _ => th
+
+
+(**** SKOLEMIZATION BY INFERENCE (lcp) ****)
+
+fun mk_old_skolem_term_wrapper t =
+ let val T = fastype_of t in
+ Const (@{const_name skolem}, T --> T) $ t
+ end
+
+fun beta_eta_under_lambdas (Abs (s, T, t')) =
+ Abs (s, T, beta_eta_under_lambdas t')
+ | beta_eta_under_lambdas t = Envir.beta_eta_contract t
+
+(*Traverse a theorem, accumulating Skolem function definitions.*)
+fun old_skolem_defs th =
+ let
+ fun dec_sko (Const (@{const_name Ex}, _) $ (body as Abs (_, T, p))) rhss =
+ (*Existential: declare a Skolem function, then insert into body and continue*)
+ let
+ val args = OldTerm.term_frees body
+ (* Forms a lambda-abstraction over the formal parameters *)
+ val rhs =
+ list_abs_free (map dest_Free args,
+ HOLogic.choice_const T $ beta_eta_under_lambdas body)
+ |> mk_old_skolem_term_wrapper
+ val comb = list_comb (rhs, args)
+ in dec_sko (subst_bound (comb, p)) (rhs :: rhss) end
+ | dec_sko (Const (@{const_name All},_) $ Abs (a, T, p)) rhss =
+ (*Universal quant: insert a free variable into body and continue*)
+ let val fname = Name.variant (OldTerm.add_term_names (p,[])) a
+ in dec_sko (subst_bound (Free(fname,T), p)) rhss end
+ | dec_sko (@{const HOL.conj} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
+ | dec_sko (@{const HOL.disj} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
+ | dec_sko (@{const Trueprop} $ p) rhss = dec_sko p rhss
+ | dec_sko _ rhss = rhss
+ in dec_sko (prop_of th) [] end;
+
+
+(**** REPLACING ABSTRACTIONS BY COMBINATORS ****)
+
+val fun_cong_all = @{thm fun_eq_iff [THEN iffD1]}
+
+(* Removes the lambdas from an equation of the form "t = (%x. u)".
+ (Cf. "extensionalize_term" in "Sledgehammer_Translate".) *)
+fun extensionalize_theorem th =
+ case prop_of th of
+ _ $ (Const (@{const_name HOL.eq}, Type (_, [Type (@{type_name fun}, _), _]))
+ $ _ $ Abs _) => extensionalize_theorem (th RS fun_cong_all)
+ | _ => th
+
+fun is_quasi_lambda_free (Const (@{const_name skolem}, _) $ _) = true
+ | is_quasi_lambda_free (t1 $ t2) =
+ is_quasi_lambda_free t1 andalso is_quasi_lambda_free t2
+ | is_quasi_lambda_free (Abs _) = false
+ | is_quasi_lambda_free _ = true
+
+val [f_B,g_B] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_B}));
+val [g_C,f_C] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_C}));
+val [f_S,g_S] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_S}));
+
+(* FIXME: Requires more use of cterm constructors. *)
+fun abstract ct =
+ let
+ val thy = theory_of_cterm ct
+ val Abs(x,_,body) = term_of ct
+ val Type(@{type_name fun}, [xT,bodyT]) = typ_of (ctyp_of_term ct)
+ val cxT = ctyp_of thy xT
+ val cbodyT = ctyp_of thy bodyT
+ fun makeK () =
+ instantiate' [SOME cxT, SOME cbodyT] [SOME (cterm_of thy body)]
+ @{thm abs_K}
+ in
+ case body of
+ Const _ => makeK()
+ | Free _ => makeK()
+ | Var _ => makeK() (*though Var isn't expected*)
+ | Bound 0 => instantiate' [SOME cxT] [] @{thm abs_I} (*identity: I*)
+ | rator$rand =>
+ if loose_bvar1 (rator,0) then (*C or S*)
+ if loose_bvar1 (rand,0) then (*S*)
+ let val crator = cterm_of thy (Abs(x,xT,rator))
+ val crand = cterm_of thy (Abs(x,xT,rand))
+ val abs_S' = cterm_instantiate [(f_S,crator),(g_S,crand)] @{thm abs_S}
+ val (_,rhs) = Thm.dest_equals (cprop_of abs_S')
+ in
+ Thm.transitive abs_S' (Conv.binop_conv abstract rhs)
+ end
+ else (*C*)
+ let val crator = cterm_of thy (Abs(x,xT,rator))
+ val abs_C' = cterm_instantiate [(f_C,crator),(g_C,cterm_of thy rand)] @{thm abs_C}
+ val (_,rhs) = Thm.dest_equals (cprop_of abs_C')
+ in
+ Thm.transitive abs_C' (Conv.fun_conv (Conv.arg_conv abstract) rhs)
+ end
+ else if loose_bvar1 (rand,0) then (*B or eta*)
+ if rand = Bound 0 then Thm.eta_conversion ct
+ else (*B*)
+ let val crand = cterm_of thy (Abs(x,xT,rand))
+ val crator = cterm_of thy rator
+ val abs_B' = cterm_instantiate [(f_B,crator),(g_B,crand)] @{thm abs_B}
+ val (_,rhs) = Thm.dest_equals (cprop_of abs_B')
+ in Thm.transitive abs_B' (Conv.arg_conv abstract rhs) end
+ else makeK()
+ | _ => raise Fail "abstract: Bad term"
+ end;
+
+(* Traverse a theorem, remplacing lambda-abstractions with combinators. *)
+fun introduce_combinators_in_cterm ct =
+ if is_quasi_lambda_free (term_of ct) then
+ Thm.reflexive ct
+ else case term_of ct of
+ Abs _ =>
+ let
+ val (cv, cta) = Thm.dest_abs NONE ct
+ val (v, _) = dest_Free (term_of cv)
+ val u_th = introduce_combinators_in_cterm cta
+ val cu = Thm.rhs_of u_th
+ val comb_eq = abstract (Thm.cabs cv cu)
+ in Thm.transitive (Thm.abstract_rule v cv u_th) comb_eq end
+ | _ $ _ =>
+ let val (ct1, ct2) = Thm.dest_comb ct in
+ Thm.combination (introduce_combinators_in_cterm ct1)
+ (introduce_combinators_in_cterm ct2)
+ end
+
+fun introduce_combinators_in_theorem th =
+ if is_quasi_lambda_free (prop_of th) then
+ th
+ else
+ let
+ val th = Drule.eta_contraction_rule th
+ val eqth = introduce_combinators_in_cterm (cprop_of th)
+ in Thm.equal_elim eqth th end
+ handle THM (msg, _, _) =>
+ (warning ("Error in the combinator translation of " ^
+ Display.string_of_thm_without_context th ^
+ "\nException message: " ^ msg ^ ".");
+ (* A type variable of sort "{}" will make abstraction fail. *)
+ TrueI)
+
+(*cterms are used throughout for efficiency*)
+val cTrueprop = cterm_of @{theory HOL} HOLogic.Trueprop;
+
+(*Given an abstraction over n variables, replace the bound variables by free
+ ones. Return the body, along with the list of free variables.*)
+fun c_variant_abs_multi (ct0, vars) =
+ let val (cv,ct) = Thm.dest_abs NONE ct0
+ in c_variant_abs_multi (ct, cv::vars) end
+ handle CTERM _ => (ct0, rev vars);
+
+val skolem_def_raw = @{thms skolem_def_raw}
+
+(* Given the definition of a Skolem function, return a theorem to replace
+ an existential formula by a use of that function.
+ Example: "EX x. x : A & x ~: B ==> sko A B : A & sko A B ~: B" [.] *)
+fun old_skolem_theorem_from_def thy rhs0 =
+ let
+ val rhs = rhs0 |> Type.legacy_freeze_thaw |> #1 |> cterm_of thy
+ val rhs' = rhs |> Thm.dest_comb |> snd
+ val (ch, frees) = c_variant_abs_multi (rhs', [])
+ val (hilbert, cabs) = ch |> Thm.dest_comb |>> term_of
+ val T =
+ case hilbert of
+ Const (@{const_name Eps}, Type (@{type_name fun}, [_, T])) => T
+ | _ => raise TERM ("old_skolem_theorem_from_def: expected \"Eps\"",
+ [hilbert])
+ val cex = cterm_of thy (HOLogic.exists_const T)
+ val ex_tm = Thm.capply cTrueprop (Thm.capply cex cabs)
+ val conc =
+ Drule.list_comb (rhs, frees)
+ |> Drule.beta_conv cabs |> Thm.capply cTrueprop
+ fun tacf [prem] =
+ rewrite_goals_tac skolem_def_raw
+ THEN rtac ((prem |> rewrite_rule skolem_def_raw) RS @{thm someI_ex}) 1
+ in
+ Goal.prove_internal [ex_tm] conc tacf
+ |> forall_intr_list frees
+ |> Thm.forall_elim_vars 0 (*Introduce Vars, but don't discharge defs.*)
+ |> Thm.varifyT_global
+ end
+
+fun to_definitional_cnf_with_quantifiers thy th =
+ let
+ val eqth = cnf.make_cnfx_thm thy (HOLogic.dest_Trueprop (prop_of th))
+ val eqth = eqth RS @{thm eq_reflection}
+ val eqth = eqth RS @{thm TruepropI}
+ in Thm.equal_elim eqth th end
+
+fun zapped_var_name ax_no (cluster_no, skolem) s =
+ (if skolem then new_skolem_var_prefix else new_nonskolem_var_prefix) ^
+ "_" ^ string_of_int ax_no ^ "_" ^ string_of_int cluster_no ^ "_" ^ s
+
+fun cluster_of_zapped_var_name s =
+ ((1, 2) |> pairself (the o Int.fromString o nth (space_explode "_" s)),
+ String.isPrefix new_skolem_var_prefix s)
+
+fun zap_quantifiers ax_no =
+ let
+ fun conv (cluster as (cluster_no, cluster_skolem)) 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
+ let
+ val skolem = (pos = (s = @{const_name Ex}))
+ val cluster =
+ if skolem = cluster_skolem then cluster
+ else (cluster_no |> cluster_skolem ? Integer.add 1, skolem)
+ in
+ Thm.dest_comb #> snd
+ #> Thm.dest_abs (SOME (zapped_var_name ax_no cluster s'))
+ #> snd #> conv cluster pos
+ end
+ else
+ Conv.all_conv
+ | Const (s, _) $ _ $ _ =>
+ if s = @{const_name "==>"} orelse
+ s = @{const_name HOL.implies} then
+ Conv.combination_conv (Conv.arg_conv (conv cluster (not pos)))
+ (conv cluster pos)
+ else if s = @{const_name HOL.conj} orelse
+ s = @{const_name HOL.disj} then
+ Conv.combination_conv (Conv.arg_conv (conv cluster pos))
+ (conv cluster pos)
+ else
+ Conv.all_conv
+ | Const (s, _) $ _ =>
+ if s = @{const_name Trueprop} then
+ Conv.arg_conv (conv cluster pos)
+ else if s = @{const_name Not} then
+ Conv.arg_conv (conv cluster (not pos))
+ else
+ Conv.all_conv
+ | _ => Conv.all_conv)
+ in
+ conv (0, true) true #> Drule.export_without_context
+ #> cprop_of #> Thm.dest_equals #> snd
+ end
+
+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 choice_ths new_skolemizer ax_no 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
+ 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
+ | _ => false) t then
+ let
+ val (ct, ctxt) =
+ Variable.import_terms true [t] ctxt
+ |>> the_single |>> cterm_of thy
+ in (SOME (discharger_th, ct), Thm.assume ct, 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 ctxt0 new_skolemizer ax_no th =
+ let
+ 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
+ []
+ else
+ map (old_skolem_theorem_from_def thy)
+ (old_skolem_defs th)) th ctxt
+ val (cnf_ths, ctxt) =
+ clausify nnf_th
+ |> (fn ([], _) =>
+ clausify (to_definitional_cnf_with_quantifiers thy nnf_th)
+ | p => p)
+ fun intr_imp ct th =
+ Thm.instantiate ([], map (pairself (cterm_of @{theory}))
+ [(Var (("i", 1), @{typ nat}),
+ HOLogic.mk_nat ax_no)])
+ @{thm skolem_COMBK_D}
+ RS Thm.implies_intr ct th
+ in
+ (opt |> Option.map (I #>> singleton (Variable.export ctxt ctxt0)
+ ##> (term_of #> HOLogic.dest_Trueprop
+ #> singleton (Variable.export_terms ctxt ctxt0))),
+ cnf_ths |> map (introduce_combinators_in_theorem
+ #> (case opt of SOME (_, ct) => intr_imp ct | NONE => I))
+ |> Variable.export ctxt ctxt0
+ |> Meson.finish_cnf
+ |> map Thm.close_derivation)
+ end
+ handle THM _ => (NONE, [])
+
+fun meson_general_tac ctxt ths =
+ 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 =>
+ SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ctxt ths)))
+ "MESON resolution proof procedure"
+
+end;
--- a/src/HOL/Tools/Sledgehammer/metis_reconstruct.ML Fri Oct 01 14:15:49 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_reconstruct.ML Fri Oct 01 16:13:28 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
@@ -114,13 +115,18 @@
| applic_to_tt (a,ts) =
case strip_prefix_and_unascii const_prefix a of
SOME b =>
- let val c = smart_invert_const b
- val ntypes = num_type_args thy c
- val nterms = length ts - ntypes
- val tts = map tm_to_tt ts
- val tys = types_of (List.take(tts,ntypes))
+ let
+ val c = smart_invert_const b
+ val ntypes = num_type_args thy c
+ val nterms = length ts - ntypes
+ val tts = map tm_to_tt ts
+ val tys = types_of (List.take(tts,ntypes))
+ val t = if String.isPrefix new_skolem_const_prefix c then
+ Var (new_skolem_var_from_const c, tl tys ---> hd tys)
+ else
+ Const (c, dummyT)
in if length tys = ntypes then
- apply_list (Const (c, dummyT)) nterms (List.drop(tts,ntypes))
+ apply_list t nterms (List.drop(tts,ntypes))
else
raise Fail ("Constant " ^ c ^ " expects " ^ Int.toString ntypes ^
" but gets " ^ Int.toString (length tys) ^
@@ -187,11 +193,12 @@
fun hol_term_from_metis FT = hol_term_from_metis_FT
| hol_term_from_metis _ = hol_term_from_metis_PT
-fun hol_terms_from_fol ctxt mode skolems fol_tms =
+fun hol_terms_from_fol ctxt mode old_skolems fol_tms =
let val ts = map (hol_term_from_metis mode ctxt) fol_tms
val _ = trace_msg (fn () => " calling type inference:")
val _ = app (fn t => trace_msg (fn () => Syntax.string_of_term ctxt t)) ts
- val ts' = ts |> map (reveal_skolem_terms skolems) |> infer_types ctxt
+ val ts' = ts |> map (reveal_old_skolem_terms old_skolems)
+ |> infer_types ctxt
val _ = app (fn t => trace_msg
(fn () => " final term: " ^ Syntax.string_of_term ctxt t ^
" of type " ^ Syntax.string_of_typ ctxt (type_of t)))
@@ -232,24 +239,24 @@
val substs = [(cterm_of thy (Var vx), cterm_of thy i_atm)]
in cterm_instantiate substs th end;
-fun assume_inf ctxt mode skolems atm =
+fun assume_inf ctxt mode old_skolems atm =
inst_excluded_middle
(ProofContext.theory_of ctxt)
- (singleton (hol_terms_from_fol ctxt mode skolems) (Metis_Term.Fn atm))
+ (singleton (hol_terms_from_fol ctxt mode old_skolems) (Metis_Term.Fn atm))
(* INFERENCE RULE: INSTANTIATE (SUBST). Type instantiations are ignored. Trying
to reconstruct them admits new possibilities of errors, e.g. concerning
sorts. Instead we try to arrange that new TVars are distinct and that types
can be inferred from terms. *)
-fun inst_inf ctxt mode skolems thpairs fsubst th =
+fun inst_inf ctxt mode old_skolems thpairs fsubst th =
let val thy = ProofContext.theory_of ctxt
val i_th = lookth thpairs th
val i_th_vars = Term.add_vars (prop_of i_th) []
fun find_var x = the (List.find (fn ((a,_),_) => a=x) i_th_vars)
fun subst_translation (x,y) =
let val v = find_var x
- (* We call "reveal_skolem_terms" and "infer_types" below. *)
+ (* We call "reveal_old_skolem_terms" and "infer_types" below. *)
val t = hol_term_from_metis mode ctxt y
in SOME (cterm_of thy (Var v), t) end
handle Option.Option =>
@@ -269,7 +276,8 @@
val _ = trace_msg (fn () => " isa th: " ^ Display.string_of_thm ctxt i_th)
val substs = map_filter remove_typeinst (Metis_Subst.toList fsubst)
val (vars,rawtms) = ListPair.unzip (map_filter subst_translation substs)
- val tms = rawtms |> map (reveal_skolem_terms skolems) |> infer_types ctxt
+ val tms = rawtms |> map (reveal_old_skolem_terms old_skolems)
+ |> infer_types ctxt
val ctm_of = cterm_incr_types thy (1 + Thm.maxidx_of i_th)
val substs' = ListPair.zip (vars, map ctm_of tms)
val _ = trace_msg (fn () =>
@@ -344,7 +352,22 @@
get (n+1) xs
in get 1 end
-fun resolve_inf ctxt mode skolems thpairs atm th1 th2 =
+(* Permute a rule's premises to move the i-th premise to the last position. *)
+fun make_last i th =
+ let val n = nprems_of th
+ in if 1 <= i andalso i <= n
+ then Thm.permute_prems (i-1) 1 th
+ else raise THM("select_literal", i, [th])
+ end;
+
+(* Maps a rule that ends "... ==> P ==> False" to "... ==> ~P" while suppressing
+ double-negations. *)
+val negate_head = rewrite_rule [@{thm atomize_not}, not_not RS eq_reflection]
+
+(* Maps the clause [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P *)
+val select_literal = negate_head oo make_last
+
+fun resolve_inf ctxt mode old_skolems thpairs atm th1 th2 =
let
val thy = ProofContext.theory_of ctxt
val i_th1 = lookth thpairs th1 and i_th2 = lookth thpairs th2
@@ -358,7 +381,7 @@
i_th1
else
let
- val i_atm = singleton (hol_terms_from_fol ctxt mode skolems)
+ val i_atm = singleton (hol_terms_from_fol ctxt mode old_skolems)
(Metis_Term.Fn atm)
val _ = trace_msg (fn () => " atom: " ^ Syntax.string_of_term ctxt i_atm)
val prems_th1 = prems_of i_th1
@@ -370,8 +393,7 @@
handle Empty => raise Fail "Failed to find literal in th2"
val _ = trace_msg (fn () => " index_th2: " ^ Int.toString index_th2)
in
- resolve_inc_tyvars thy (Meson.select_literal index_th1 i_th1) index_th2
- i_th2
+ resolve_inc_tyvars thy (select_literal index_th1 i_th1) index_th2 i_th2
end
end;
@@ -382,9 +404,9 @@
val refl_x = cterm_of @{theory} (Var (hd (Term.add_vars (prop_of REFL_THM) [])));
val refl_idx = 1 + Thm.maxidx_of REFL_THM;
-fun refl_inf ctxt mode skolems t =
+fun refl_inf ctxt mode old_skolems t =
let val thy = ProofContext.theory_of ctxt
- val i_t = singleton (hol_terms_from_fol ctxt mode skolems) t
+ val i_t = singleton (hol_terms_from_fol ctxt mode old_skolems) t
val _ = trace_msg (fn () => " term: " ^ Syntax.string_of_term ctxt i_t)
val c_t = cterm_incr_types thy refl_idx i_t
in cterm_instantiate [(refl_x, c_t)] REFL_THM end;
@@ -400,10 +422,10 @@
| get_ty_arg_size thy (Const (c, _)) = (num_type_args thy c handle TYPE _ => 0)
| get_ty_arg_size _ _ = 0;
-fun equality_inf ctxt mode skolems (pos, atm) fp fr =
+fun equality_inf ctxt mode old_skolems (pos, atm) fp fr =
let val thy = ProofContext.theory_of ctxt
val m_tm = Metis_Term.Fn atm
- val [i_atm,i_tm] = hol_terms_from_fol ctxt mode skolems [m_tm, fr]
+ val [i_atm,i_tm] = hol_terms_from_fol ctxt mode old_skolems [m_tm, fr]
val _ = trace_msg (fn () => "sign of the literal: " ^ Bool.toString pos)
fun replace_item_list lx 0 (_::ls) = lx::ls
| replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls
@@ -482,32 +504,51 @@
val factor = Seq.hd o distinct_subgoals_tac;
-fun step ctxt mode skolems thpairs p =
+fun step ctxt mode old_skolems thpairs p =
case p of
(fol_th, Metis_Proof.Axiom _) => factor (axiom_inf thpairs fol_th)
- | (_, Metis_Proof.Assume f_atm) => assume_inf ctxt mode skolems f_atm
+ | (_, Metis_Proof.Assume f_atm) => assume_inf ctxt mode old_skolems f_atm
| (_, Metis_Proof.Metis_Subst (f_subst, f_th1)) =>
- factor (inst_inf ctxt mode skolems thpairs f_subst f_th1)
+ factor (inst_inf ctxt mode old_skolems thpairs f_subst f_th1)
| (_, Metis_Proof.Resolve(f_atm, f_th1, f_th2)) =>
- factor (resolve_inf ctxt mode skolems thpairs f_atm f_th1 f_th2)
- | (_, Metis_Proof.Refl f_tm) => refl_inf ctxt mode skolems f_tm
+ factor (resolve_inf ctxt mode old_skolems thpairs f_atm f_th1 f_th2)
+ | (_, Metis_Proof.Refl f_tm) => refl_inf ctxt mode old_skolems f_tm
| (_, Metis_Proof.Equality (f_lit, f_p, f_r)) =>
- equality_inf ctxt mode skolems f_lit f_p f_r
+ equality_inf ctxt mode old_skolems f_lit f_p f_r
-fun is_real_literal (_, (c, _)) = not (String.isPrefix class_prefix c)
+fun flexflex_first_order th =
+ case Thm.tpairs_of th of
+ [] => th
+ | pairs =>
+ let val thy = theory_of_thm th
+ val (_, tenv) =
+ fold (Pattern.first_order_match thy) pairs (Vartab.empty, Vartab.empty)
+ val t_pairs = map Meson.term_pair_of (Vartab.dest tenv)
+ val th' = Thm.instantiate ([], map (pairself (cterm_of thy)) t_pairs) th
+ in th' end
+ handle THM _ => th;
-fun replay_one_inference ctxt mode skolems (fol_th, inf) thpairs =
+fun is_metis_literal_genuine (_, (s, _)) = not (String.isPrefix class_prefix s)
+fun is_isabelle_literal_genuine t =
+ case t of _ $ (Const (@{const_name skolem}, _) $ _) => false | _ => true
+
+fun count p xs = fold (fn x => if p x then Integer.add 1 else I) xs 0
+
+fun replay_one_inference ctxt mode old_skolems (fol_th, inf) thpairs =
let
val _ = trace_msg (fn () => "=============================================")
val _ = trace_msg (fn () => "METIS THM: " ^ Metis_Thm.toString fol_th)
val _ = trace_msg (fn () => "INFERENCE: " ^ Metis_Proof.inferenceToString inf)
- val th = Meson.flexflex_first_order (step ctxt mode skolems
- thpairs (fol_th, inf))
+ val th = step ctxt mode old_skolems thpairs (fol_th, inf)
+ |> flexflex_first_order
val _ = trace_msg (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th)
val _ = trace_msg (fn () => "=============================================")
- val n_metis_lits =
- length (filter is_real_literal (Metis_LiteralSet.toList (Metis_Thm.clause fol_th)))
- val _ = if nprems_of th = n_metis_lits then ()
+ val num_metis_lits =
+ fol_th |> Metis_Thm.clause |> Metis_LiteralSet.toList
+ |> count is_metis_literal_genuine
+ val num_isabelle_lits =
+ th |> prems_of |> count is_isabelle_literal_genuine
+ val _ = if num_metis_lits = num_isabelle_lits then ()
else error "Cannot replay Metis proof in Isabelle: Out of sync."
in (fol_th, th) :: thpairs end
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Fri Oct 01 14:15:49 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Fri Oct 01 16:13:28 2010 +0200
@@ -11,6 +11,7 @@
sig
val trace : bool Unsynchronized.ref
val type_lits : bool Config.T
+ val new_skolemizer : bool Config.T
val metis_tac : Proof.context -> thm list -> int -> tactic
val metisF_tac : Proof.context -> thm list -> int -> tactic
val metisFT_tac : Proof.context -> thm list -> int -> tactic
@@ -23,9 +24,14 @@
open Metis_Translate
open Metis_Reconstruct
+structure Int_Pair_Graph =
+ Graph(type key = int * int val ord = prod_ord int_ord int_ord)
+
fun trace_msg msg = if !trace then tracing (msg ()) else ()
-val (type_lits, type_lits_setup) = Attrib.config_bool "metis_type_lits" (K true);
+val (type_lits, type_lits_setup) = Attrib.config_bool "metis_type_lits" (K true)
+val (new_skolemizer, new_skolemizer_setup) =
+ Attrib.config_bool "metis_new_skolemizer" (K false)
fun is_false t = t aconv (HOLogic.mk_Trueprop HOLogic.false_const);
@@ -51,24 +57,171 @@
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_prem_with_concl thy i th =
+ let
+ val goal = Logic.get_goal (prop_of th) i |> Envir.beta_eta_contract
+ val prem = goal |> Logic.strip_assums_hyp |> the_single
+ val concl = goal |> Logic.strip_assums_concl
+ 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 (*FIXME: 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])
+
+ val inst = [] |> unify_terms (prem, concl)
+ val _ = trace_msg (fn () => cat_lines (map (fn (t, u) =>
+ Syntax.string_of_term @{context} t ^ " |-> " ^
+ Syntax.string_of_term @{context} u) inst))
+ val instT = fold (fn Tp => unify_types (pairself fastype_of Tp)
+ handle TERM _ => I) 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
+ handle Empty => th (* ### FIXME *)
+
+val cluster_ord = prod_ord (prod_ord int_ord int_ord) bool_ord
+
+(* 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 prems_imp_false =
+ case prop_of prems_imp_false of
+ @{prop False} => prems_imp_false
+ | prems_imp_false_prop =>
+ let
+ val thy = ProofContext.theory_of ctxt
+ fun match_term p =
+ let
+ val (tyenv, tenv) =
+ Pattern.first_order_match thy p (Vartab.empty, Vartab.empty)
+ val tsubst =
+ tenv |> Vartab.dest
+ |> sort (cluster_ord
+ o pairself (Meson_Clausify.cluster_of_zapped_var_name
+ o fst o fst))
+ |> map (Meson.term_pair_of
+ #> pairself (Envir.subst_term_types tyenv))
+ in (tyenv, tsubst) end
+ fun subst_info_for_prem assm_no prem =
+ case prem of
+ _ $ (Const (@{const_name skolem}, _) $ (_ $ t $ num)) =>
+ let val ax_no = HOLogic.dest_nat num in
+ (ax_no, (assm_no, match_term (nth axioms ax_no |> snd, t)))
+ end
+ | _ => raise TERM ("discharge_skolem_premises: Malformed premise",
+ [prem])
+ fun cluster_of_var_name skolem s =
+ let val (jj, skolem') = Meson_Clausify.cluster_of_zapped_var_name s in
+ if skolem' = skolem then SOME jj else NONE
+ end
+ fun clusters_in_term skolem t =
+ Term.add_var_names t [] |> map_filter (cluster_of_var_name skolem o fst)
+ fun deps_for_term_subst (var, t) =
+ case clusters_in_term false var of
+ [] => NONE
+ | [(ax_no, cluster_no)] =>
+ SOME ((ax_no, cluster_no),
+ clusters_in_term true t
+ |> cluster_no > 0 ? cons (ax_no, cluster_no - 1))
+ | _ => raise TERM ("discharge_skolem_premises: Expected Var", [var])
+ val prems = Logic.strip_imp_prems prems_imp_false_prop
+ val substs = map2 subst_info_for_prem (0 upto length prems - 1) prems
+ val depss = maps (map_filter deps_for_term_subst o snd o snd o snd) substs
+ val clusters = maps (op ::) depss
+ val ordered_clusters =
+ Int_Pair_Graph.empty
+ |> fold Int_Pair_Graph.default_node (map (rpair ()) clusters)
+ |> fold Int_Pair_Graph.add_deps_acyclic depss
+ |> Int_Pair_Graph.topological_order
+ 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
+ THEN TRY (REPEAT_ALL_NEW (etac @{thm exE}) 1)
+ (* two copies are better than one (FIXME) *)
+ THEN etac @{lemma "P ==> (P ==> P ==> Q) ==> Q" by fast} 1
+ THEN TRY (REPEAT_ALL_NEW (etac @{thm allE}) 1)
+ THEN match_tac [prems_imp_false] 1
+ THEN DETERM_UNTIL_SOLVED
+ (rtac @{thm skolem_COMBK_I} 1
+ THEN PRIMITIVE (unify_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
val type_lits = Config.get ctxt type_lits
+ val new_skolemizer =
+ Config.get ctxt new_skolemizer orelse null (Meson_Choices.get ctxt)
val th_cls_pairs =
- map (fn th => (Thm.get_name_hint th,
- Meson_Clausifier.meson_cnf_axiom thy th)) ths0
- val ths = maps #2 th_cls_pairs
+ map2 (fn j => fn th =>
+ (Thm.get_name_hint 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
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")
- val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) ths
- val (mode, {axioms, tfrees, skolems}) =
- build_logic_map mode ctxt type_lits cls ths
+ val _ = app (app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th))) thss
+ val (mode, {axioms, tfrees, old_skolems}) =
+ build_logic_map mode ctxt type_lits cls thss
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
@@ -86,11 +239,12 @@
val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt
(*add constraints arising from converting goal to clause form*)
val proof = Metis_Proof.proof mth
- val result = fold (replay_one_inference ctxt' mode skolems) proof axioms
+ val result =
+ fold (replay_one_inference ctxt' mode old_skolems) proof axioms
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
@@ -105,7 +259,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 _ =>
@@ -117,7 +271,7 @@
does, but also keep an unextensionalized version of "th" for backward
compatibility. *)
fun also_extensionalize_theorem th =
- let val th' = Meson_Clausifier.extensionalize_theorem th in
+ let val th' = Meson_Clausify.extensionalize_theorem th in
if Thm.eq_thm (th, th') then [th]
else th :: Meson.make_clauses_unsorted [th']
end
@@ -126,7 +280,7 @@
single
#> Meson.make_clauses_unsorted
#> maps also_extensionalize_theorem
- #> map Meson_Clausifier.introduce_combinators_in_theorem
+ #> map Meson_Clausify.introduce_combinators_in_theorem
#> Meson.finish_cnf
fun preskolem_tac ctxt st0 =
@@ -139,9 +293,6 @@
val type_has_top_sort =
exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)
-val preproc_ss =
- HOL_basic_ss addsimps @{thms all_simps[symmetric] ex_simps[symmetric]}
-
fun generic_metis_tac mode ctxt ths i st0 =
let
val _ = trace_msg (fn () =>
@@ -180,6 +331,7 @@
val setup =
type_lits_setup
+ #> new_skolemizer_setup
#> method @{binding metis} HO "Metis for FOL/HOL problems"
#> method @{binding metisF} FO "Metis for FOL problems"
#> method @{binding metisFT} FT
--- a/src/HOL/Tools/Sledgehammer/metis_translate.ML Fri Oct 01 14:15:49 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_translate.ML Fri Oct 01 16:13:28 2010 +0200
@@ -34,7 +34,7 @@
type logic_map =
{axioms: (Metis_Thm.thm * thm) list,
tfrees: type_literal list,
- skolems: (string * term) list}
+ old_skolems: (string * term) list}
val type_wrapper_name : string
val bound_var_prefix : string
@@ -45,6 +45,7 @@
val const_prefix: string
val type_const_prefix: string
val class_prefix: string
+ val new_skolem_const_prefix : string
val invert_const: string -> string
val ascii_of: string -> string
val unascii_of: string -> string
@@ -58,6 +59,7 @@
val make_fixed_type_const : string -> string
val make_type_class : string -> string
val num_type_args: theory -> string -> int
+ val new_skolem_var_from_const: string -> indexname
val type_literals_for_types : typ list -> type_literal list
val make_class_rel_clauses :
theory -> class list -> class list -> class_rel_clause list
@@ -66,14 +68,15 @@
val combtyp_of : combterm -> combtyp
val strip_combterm_comb : combterm -> combterm * combterm list
val combterm_from_term :
- theory -> (string * typ) list -> term -> combterm * typ list
- val reveal_skolem_terms : (string * term) list -> term -> term
+ theory -> int -> (string * typ) list -> term -> combterm * typ list
+ val reveal_old_skolem_terms : (string * term) list -> term -> term
val tfree_classes_of_terms : term list -> string list
val tvar_classes_of_terms : term list -> string list
val type_consts_of_terms : theory -> term list -> string list
val string_of_mode : mode -> string
val build_logic_map :
- mode -> Proof.context -> bool -> thm list -> thm list -> mode * logic_map
+ mode -> Proof.context -> bool -> thm list -> thm list list
+ -> mode * logic_map
end
structure Metis_Translate : METIS_TRANSLATE =
@@ -92,6 +95,10 @@
val type_const_prefix = "tc_";
val class_prefix = "class_";
+val skolem_const_prefix = "Sledgehammer" ^ Long_Name.separator ^ "Sko"
+val old_skolem_const_prefix = skolem_const_prefix ^ "o"
+val new_skolem_const_prefix = skolem_const_prefix ^ "n"
+
fun union_all xss = fold (union (op =)) xss []
(* Readable names for the more common symbolic functions. Do not mess with the
@@ -198,17 +205,22 @@
fun make_type_class clas = class_prefix ^ ascii_of clas;
-val skolem_prefix = "Sledgehammer" ^ Long_Name.separator ^ "Sko"
-
(* The number of type arguments of a constant, zero if it's monomorphic. For
(instances of) Skolem pseudoconstants, this information is encoded in the
constant name. *)
fun num_type_args thy s =
- if String.isPrefix skolem_prefix s then
+ if String.isPrefix skolem_const_prefix s then
s |> space_explode Long_Name.separator |> List.last |> Int.fromString |> the
else
(s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length
+fun new_skolem_var_from_const s =
+ let
+ val ss = s |> space_explode Long_Name.separator
+ val n = length ss
+ in (nth ss (n - 2), nth ss (n - 3) |> Int.fromString |> the) end
+
+
(**** Definitions and functions for FOL clauses for TPTP format output ****)
type name = string * string
@@ -384,92 +396,107 @@
| simple_combtype_of (TVar (x, _)) =
CombTVar (make_schematic_type_var x, string_of_indexname x)
+fun new_skolem_const_name th_no s num_T_args =
+ [new_skolem_const_prefix, string_of_int th_no, s, string_of_int num_T_args]
+ |> space_implode Long_Name.separator
+
(* Converts a term (with combinators) into a combterm. Also accummulates sort
infomation. *)
-fun combterm_from_term thy bs (P $ Q) =
- let val (P', tsP) = combterm_from_term thy bs P
- val (Q', tsQ) = combterm_from_term thy bs Q
+fun combterm_from_term thy th_no bs (P $ Q) =
+ let val (P', tsP) = combterm_from_term thy th_no bs P
+ val (Q', tsQ) = combterm_from_term thy th_no bs Q
in (CombApp (P', Q'), union (op =) tsP tsQ) end
- | combterm_from_term thy _ (Const (c, T)) =
+ | combterm_from_term thy _ _ (Const (c, T)) =
let
val (tp, ts) = combtype_of T
val tvar_list =
- (if String.isPrefix skolem_prefix c then
+ (if String.isPrefix old_skolem_const_prefix c then
[] |> Term.add_tvarsT T |> map TVar
else
(c, T) |> Sign.const_typargs thy)
|> map simple_combtype_of
val c' = CombConst (`make_fixed_const c, tp, tvar_list)
in (c',ts) end
- | combterm_from_term _ _ (Free (v, T)) =
+ | combterm_from_term _ _ _ (Free (v, T)) =
let val (tp, ts) = combtype_of T
val v' = CombConst (`make_fixed_var v, tp, [])
in (v',ts) end
- | combterm_from_term _ _ (Var (v, T)) =
- let val (tp,ts) = combtype_of T
- val v' = CombVar ((make_schematic_var v, string_of_indexname v), tp)
- in (v',ts) end
- | combterm_from_term _ bs (Bound j) =
+ | combterm_from_term _ th_no _ (Var (v as (s, _), T)) =
+ let
+ val (tp, ts) = combtype_of T
+ val v' =
+ if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then
+ let
+ val tys = T |> strip_type |> swap |> op ::
+ val s' = new_skolem_const_name th_no s (length tys)
+ in
+ CombConst (`make_fixed_const s', tp, map simple_combtype_of tys)
+ end
+ else
+ CombVar ((make_schematic_var v, string_of_indexname v), tp)
+ in (v', ts) end
+ | combterm_from_term _ _ bs (Bound j) =
let
val (s, T) = nth bs j
val (tp, ts) = combtype_of T
val v' = CombConst (`make_bound_var s, tp, [])
in (v', ts) end
- | combterm_from_term _ _ (Abs _) = raise Fail "HOL clause: Abs"
+ | combterm_from_term _ _ _ (Abs _) = raise Fail "HOL clause: Abs"
-fun predicate_of thy ((@{const Not} $ P), pos) = predicate_of thy (P, not pos)
- | predicate_of thy (t, pos) =
- (combterm_from_term thy [] (Envir.eta_contract t), pos)
+fun predicate_of thy th_no ((@{const Not} $ P), pos) =
+ predicate_of thy th_no (P, not pos)
+ | predicate_of thy th_no (t, pos) =
+ (combterm_from_term thy th_no [] (Envir.eta_contract t), pos)
-fun literals_of_term1 args thy (@{const Trueprop} $ P) =
- literals_of_term1 args thy P
- | literals_of_term1 args thy (@{const HOL.disj} $ P $ Q) =
- literals_of_term1 (literals_of_term1 args thy P) thy Q
- | literals_of_term1 (lits, ts) thy P =
- let val ((pred, ts'), pol) = predicate_of thy (P, true) in
+fun literals_of_term1 args thy th_no (@{const Trueprop} $ P) =
+ literals_of_term1 args thy th_no P
+ | literals_of_term1 args thy th_no (@{const HOL.disj} $ P $ Q) =
+ literals_of_term1 (literals_of_term1 args thy th_no P) thy th_no Q
+ | literals_of_term1 (lits, ts) thy th_no P =
+ let val ((pred, ts'), pol) = predicate_of thy th_no (P, true) in
(FOLLiteral (pol, pred) :: lits, union (op =) ts ts')
end
val literals_of_term = literals_of_term1 ([], [])
-fun skolem_name i j num_T_args =
- skolem_prefix ^ Long_Name.separator ^
+fun old_skolem_const_name i j num_T_args =
+ old_skolem_const_prefix ^ Long_Name.separator ^
(space_implode Long_Name.separator (map Int.toString [i, j, num_T_args]))
-fun conceal_skolem_terms i skolems t =
+fun conceal_old_skolem_terms i old_skolems t =
if exists_Const (curry (op =) @{const_name skolem} o fst) t then
let
- fun aux skolems
+ fun aux old_skolems
(t as (Const (@{const_name skolem}, Type (_, [_, T])) $ _)) =
let
- val (skolems, s) =
+ val (old_skolems, s) =
if i = ~1 then
- (skolems, @{const_name undefined})
- else case AList.find (op aconv) skolems t of
- s :: _ => (skolems, s)
+ (old_skolems, @{const_name undefined})
+ else case AList.find (op aconv) old_skolems t of
+ s :: _ => (old_skolems, s)
| [] =>
let
- val s = skolem_name i (length skolems)
- (length (Term.add_tvarsT T []))
- in ((s, t) :: skolems, s) end
- in (skolems, Const (s, T)) end
- | aux skolems (t1 $ t2) =
+ val s = old_skolem_const_name i (length old_skolems)
+ (length (Term.add_tvarsT T []))
+ in ((s, t) :: old_skolems, s) end
+ in (old_skolems, Const (s, T)) end
+ | aux old_skolems (t1 $ t2) =
let
- val (skolems, t1) = aux skolems t1
- val (skolems, t2) = aux skolems t2
- in (skolems, t1 $ t2) end
- | aux skolems (Abs (s, T, t')) =
- let val (skolems, t') = aux skolems t' in
- (skolems, Abs (s, T, t'))
+ val (old_skolems, t1) = aux old_skolems t1
+ val (old_skolems, t2) = aux old_skolems t2
+ in (old_skolems, t1 $ t2) end
+ | aux old_skolems (Abs (s, T, t')) =
+ let val (old_skolems, t') = aux old_skolems t' in
+ (old_skolems, Abs (s, T, t'))
end
- | aux skolems t = (skolems, t)
- in aux skolems t end
+ | aux old_skolems t = (old_skolems, t)
+ in aux old_skolems t end
else
- (skolems, t)
+ (old_skolems, t)
-fun reveal_skolem_terms skolems =
+fun reveal_old_skolem_terms old_skolems =
map_aterms (fn t as Const (s, _) =>
- if String.isPrefix skolem_prefix s then
- AList.lookup (op =) skolems s |> the
+ if String.isPrefix old_skolem_const_prefix s then
+ AList.lookup (op =) old_skolems s |> the
|> map_types Type_Infer.paramify_vars
else
t
@@ -580,8 +607,8 @@
metis_lit pos "=" (map hol_term_to_fol_FT tms)
| _ => metis_lit pos "{}" [hol_term_to_fol_FT tm]) (*hBOOL*);
-fun literals_of_hol_term thy mode t =
- let val (lits, types_sorts) = literals_of_term thy t
+fun literals_of_hol_term thy th_no mode t =
+ let val (lits, types_sorts) = literals_of_term thy th_no t
in (map (hol_literal_to_fol mode) lits, types_sorts) end;
(*Sign should be "true" for conjecture type constraints, "false" for type lits in clauses.*)
@@ -596,16 +623,17 @@
fun metis_of_tfree tf =
Metis_Thm.axiom (Metis_LiteralSet.singleton (metis_of_type_literals true tf));
-fun hol_thm_to_fol is_conjecture ctxt type_lits mode j skolems th =
+fun hol_thm_to_fol is_conjecture th_no ctxt type_lits mode j old_skolems th =
let
val thy = ProofContext.theory_of ctxt
- val (skolems, (mlits, types_sorts)) =
- th |> prop_of |> conceal_skolem_terms j skolems
- ||> (HOLogic.dest_Trueprop #> literals_of_hol_term thy mode)
+ val (old_skolems, (mlits, types_sorts)) =
+ th |> prop_of |> Logic.strip_imp_concl
+ |> conceal_old_skolem_terms j old_skolems
+ ||> (HOLogic.dest_Trueprop #> literals_of_hol_term thy th_no mode)
in
if is_conjecture then
(Metis_Thm.axiom (Metis_LiteralSet.fromList mlits),
- type_literals_for_types types_sorts, skolems)
+ type_literals_for_types types_sorts, old_skolems)
else
let
val tylits = filter_out (default_sort ctxt) types_sorts
@@ -614,7 +642,7 @@
if type_lits then map (metis_of_type_literals false) tylits else []
in
(Metis_Thm.axiom (Metis_LiteralSet.fromList(mtylits @ mlits)), [],
- skolems)
+ old_skolems)
end
end;
@@ -637,10 +665,10 @@
type logic_map =
{axioms: (Metis_Thm.thm * thm) list,
tfrees: type_literal list,
- skolems: (string * term) list}
+ old_skolems: (string * term) list}
fun is_quasi_fol_clause thy =
- Meson.is_fol_term thy o snd o conceal_skolem_terms ~1 [] o prop_of
+ Meson.is_fol_term thy o snd o conceal_old_skolem_terms ~1 [] o prop_of
(*Extract TFree constraints from context to include as conjecture clauses*)
fun init_tfrees ctxt =
@@ -650,16 +678,16 @@
end;
(*Insert non-logical axioms corresponding to all accumulated TFrees*)
-fun add_tfrees {axioms, tfrees, skolems} : logic_map =
+fun add_tfrees {axioms, tfrees, old_skolems} : logic_map =
{axioms = map (rpair TrueI o metis_of_tfree) (distinct (op =) tfrees) @
axioms,
- tfrees = tfrees, skolems = skolems}
+ tfrees = tfrees, old_skolems = old_skolems}
(*transform isabelle type / arity clause to metis clause *)
fun add_type_thm [] lmap = lmap
- | add_type_thm ((ith, mth) :: cls) {axioms, tfrees, skolems} =
+ | add_type_thm ((ith, mth) :: cls) {axioms, tfrees, old_skolems} =
add_type_thm cls {axioms = (mth, ith) :: axioms, tfrees = tfrees,
- skolems = skolems}
+ old_skolems = old_skolems}
fun const_in_metis c (pred, tm_list) =
let
@@ -694,29 +722,31 @@
end;
(* Function to generate metis clauses, including comb and type clauses *)
-fun build_logic_map mode0 ctxt type_lits cls ths =
+fun build_logic_map mode0 ctxt type_lits cls thss =
let val thy = ProofContext.theory_of ctxt
(*The modes FO and FT are sticky. HO can be downgraded to FO.*)
fun set_mode FO = FO
| set_mode HO =
- if forall (is_quasi_fol_clause thy) (cls @ ths) then FO else HO
+ if forall (forall (is_quasi_fol_clause thy)) (cls :: thss) then FO
+ else HO
| set_mode FT = FT
val mode = set_mode mode0
(*transform isabelle clause to metis clause *)
- fun add_thm is_conjecture (metis_ith, isa_ith) {axioms, tfrees, skolems}
- : logic_map =
+ fun add_thm th_no is_conjecture (metis_ith, isa_ith)
+ {axioms, tfrees, old_skolems} : logic_map =
let
- val (mth, tfree_lits, skolems) =
- hol_thm_to_fol is_conjecture ctxt type_lits mode (length axioms)
- skolems metis_ith
+ val (mth, tfree_lits, old_skolems) =
+ hol_thm_to_fol is_conjecture th_no ctxt type_lits mode (length axioms)
+ old_skolems metis_ith
in
{axioms = (mth, Meson.make_meta_clause isa_ith) :: axioms,
- tfrees = union (op =) tfree_lits tfrees, skolems = skolems}
+ tfrees = union (op =) tfree_lits tfrees, old_skolems = old_skolems}
end;
- val lmap = {axioms = [], tfrees = init_tfrees ctxt, skolems = []}
- |> fold (add_thm true o `I) cls
+ val lmap = {axioms = [], tfrees = init_tfrees ctxt, old_skolems = []}
+ |> fold (add_thm 0 true o `I) cls
|> add_tfrees
- |> fold (add_thm false o `I) ths
+ |> fold (fn (th_no, ths) => fold (add_thm th_no false o `I) ths)
+ (1 upto length thss ~~ thss)
val clause_lists = map (Metis_Thm.clause o #1) (#axioms lmap)
fun is_used c =
exists (Metis_LiteralSet.exists (const_in_metis c o #2)) clause_lists
@@ -733,7 +763,9 @@
[]
else
thms)
- in lmap |> fold (add_thm false) helper_ths end
- in (mode, add_type_thm (type_ext thy (map prop_of (cls @ ths))) lmap) end
+ in lmap |> fold (add_thm ~1 false) helper_ths end
+ in
+ (mode, add_type_thm (type_ext thy (maps (map prop_of) (cls :: thss))) lmap)
+ end
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Fri Oct 01 14:15:49 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Fri Oct 01 16:13:28 2010 +0200
@@ -77,8 +77,8 @@
only: bool}
val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator
-val abs_name = "Sledgehammer.abs"
-val skolem_prefix = "Sledgehammer.sko"
+val abs_name = sledgehammer_prefix ^ "abs"
+val skolem_prefix = sledgehammer_prefix ^ "sko"
val theory_const_suffix = Long_Name.separator ^ " 1"
fun repair_name reserved multi j name =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Fri Oct 01 14:15:49 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Fri Oct 01 16:13:28 2010 +0200
@@ -57,7 +57,7 @@
fun combformula_for_prop thy =
let
- val do_term = combterm_from_term thy
+ val do_term = combterm_from_term thy ~1
fun do_quant bs q s T t' =
let val s = Name.variant (map fst bs) s in
do_formula ((s, T) :: bs) t'
@@ -94,7 +94,7 @@
(0 upto length Ts - 1 ~~ Ts))
(* Removes the lambdas from an equation of the form "t = (%x. u)".
- (Cf. "extensionalize_theorem" in "Meson_Clausifier".) *)
+ (Cf. "extensionalize_theorem" in "Meson_Clausify".) *)
fun extensionalize_term t =
let
fun aux j (@{const Trueprop} $ t') = @{const Trueprop} $ aux j t'
@@ -141,7 +141,7 @@
t |> conceal_bounds Ts
|> Envir.eta_contract
|> cterm_of thy
- |> Meson_Clausifier.introduce_combinators_in_cterm
+ |> Meson_Clausify.introduce_combinators_in_cterm
|> prop_of |> Logic.dest_equals |> snd
|> reveal_bounds Ts
val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Oct 01 14:15:49 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Oct 01 16:13:28 2010 +0200
@@ -98,7 +98,7 @@
(* Converts an elim-rule into an equivalent theorem that does not have the
predicate variable. Leaves other theorems unchanged. We simply instantiate
the conclusion variable to False. (Cf. "transform_elim_theorem" in
- "Meson_Clausifier".) *)
+ "Meson_Clausify".) *)
fun transform_elim_term t =
case Logic.strip_imp_concl t of
@{const Trueprop} $ Var (z, @{typ bool}) =>
--- a/src/HOL/Tools/meson.ML Fri Oct 01 14:15:49 2010 +0200
+++ b/src/HOL/Tools/meson.ML Fri Oct 01 16:13:28 2010 +0200
@@ -9,14 +9,13 @@
sig
val trace: bool Unsynchronized.ref
val term_pair_of: indexname * (typ * 'a) -> term * 'a
- val flexflex_first_order: thm -> thm
val size_of_subgoals: thm -> int
val has_too_many_clauses: Proof.context -> term -> bool
val make_cnf: thm list -> thm -> Proof.context -> thm list * Proof.context
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
@@ -24,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
@@ -37,13 +36,10 @@
val make_meta_clause: thm -> thm
val make_meta_clauses: thm list -> thm list
val meson_tac: Proof.context -> thm list -> int -> tactic
- val negate_head: thm -> thm
- val select_literal: int -> thm -> thm
- val skolemize_tac: Proof.context -> int -> tactic
val setup: theory -> theory
end
-structure Meson: MESON =
+structure Meson : MESON =
struct
val trace = Unsynchronized.ref false;
@@ -66,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};
@@ -110,18 +105,6 @@
SOME th => th
| NONE => raise THM ("first_order_resolve", 0, [thA, thB]))
-fun flexflex_first_order th =
- case Thm.tpairs_of th of
- [] => th
- | pairs =>
- let val thy = theory_of_thm th
- val (_, tenv) =
- fold (Pattern.first_order_match thy) pairs (Vartab.empty, Vartab.empty)
- val t_pairs = map term_pair_of (Vartab.dest tenv)
- val th' = Thm.instantiate ([], map (pairself (cterm_of thy)) t_pairs) th
- in th' end
- handle THM _ => th;
-
(*Forward proof while preserving bound variables names*)
fun rename_bvs_RS th rl =
let val th' = th RS rl
@@ -330,7 +313,7 @@
(* Conjunctive normal form, adding clauses from th in front of ths (for foldr).
Strips universal quantifiers and breaks up conjunctions.
Eliminates existential quantifiers using Skolemization theorems. *)
-fun cnf skolem_ths ctxt (th, ths) =
+fun cnf old_skolem_ths ctxt (th, ths) =
let val ctxtr = Unsynchronized.ref ctxt (* FIXME ??? *)
fun cnf_aux (th,ths) =
if not (can HOLogic.dest_Trueprop (prop_of th)) then ths (*meta-level: ignore*)
@@ -344,7 +327,7 @@
in ctxtr := ctxt'; cnf_aux (th', ths) end
| Const (@{const_name Ex}, _) =>
(*existential quantifier: Insert Skolem functions*)
- cnf_aux (apply_skolem_theorem (th, skolem_ths), ths)
+ cnf_aux (apply_skolem_theorem (th, old_skolem_ths), ths)
| Const (@{const_name HOL.disj}, _) =>
(*Disjunction of P, Q: Create new goal of proving ?P | ?Q and solve it using
all combinations of converting P, Q to CNF.*)
@@ -360,7 +343,7 @@
else cnf_aux (th,ths)
in (cls, !ctxtr) end;
-fun make_cnf skolem_ths th ctxt = cnf skolem_ths ctxt (th, []);
+fun make_cnf old_skolem_ths th ctxt = cnf old_skolem_ths ctxt (th, [])
(*Generalization, removal of redundant equalities, removal of tautologies.*)
fun finish_cnf ths = filter (not o is_taut) (map refl_clause ths);
@@ -539,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 choice_ths =
+ let
+ fun aux th =
+ if not (has_conns [@{const_name Ex}] (prop_of th)) then
+ th
+ else
+ tryres (th, choice_ths @
+ [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 (Meson_Choices.get 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
@@ -595,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.*)
@@ -694,37 +682,4 @@
name_thms "MClause#"
(distinct Thm.eq_thm_prop (map make_meta_clause ths));
-(*Permute a rule's premises to move the i-th premise to the last position.*)
-fun make_last i th =
- let val n = nprems_of th
- in if 1 <= i andalso i <= n
- then Thm.permute_prems (i-1) 1 th
- else raise THM("select_literal", i, [th])
- end;
-
-(*Maps a rule that ends "... ==> P ==> False" to "... ==> ~P" while suppressing
- double-negations.*)
-val negate_head = rewrite_rule [@{thm atomize_not}, not_not RS eq_reflection];
-
-(*Maps the clause [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P*)
-fun select_literal i cl = negate_head (make_last i cl);
-
-
-(*Top-level Skolemization. Allows part of the conversion to clauses to be
- expressed as a tactic (or Isar method). Each assumption of the selected
- goal is converted to NNF and then its existential quantifiers are pulled
- to the front. Finally, all existential quantifiers are eliminated,
- leaving !!-quantified variables. Perhaps Safe_tac should follow, but it
- might generate many subgoals.*)
-
-fun skolemize_tac ctxt = SUBGOAL (fn (goal, i) =>
- let val ts = Logic.strip_assums_hyp goal
- in
- EVERY'
- [Misc_Legacy.METAHYPS (fn hyps =>
- (cut_facts_tac (skolemize_nnf_list ctxt hyps) 1
- THEN REPEAT (etac exE 1))),
- REPEAT_DETERM_N (length ts) o (etac thin_rl)] i
- end);
-
end;