use the same code for extensionalization in Metis and Sledgehammer and generalize that code so that it gracefully handles negations (e.g. negated conjecture), formulas of the form (%x. t) = u, etc.
--- a/src/HOL/Metis_Examples/Clausify.thy Thu May 12 15:29:19 2011 +0200
+++ b/src/HOL/Metis_Examples/Clausify.thy Thu May 12 15:29:19 2011 +0200
@@ -12,6 +12,37 @@
declare [[unify_search_bound = 100]]
declare [[unify_trace_bound = 100]]
+sledgehammer_params [prover = e, blocking, timeout = 10]
+
+
+text {* Extensionality *}
+
+lemma plus_1_not_0: "n + (1\<Colon>nat) \<noteq> 0"
+by simp
+
+definition inc :: "nat \<Rightarrow> nat" where
+"inc x = x + 1"
+
+lemma "inc \<noteq> (\<lambda>y. 0)"
+sledgehammer [expect = some] (inc_def plus_1_not_0)
+by (metis inc_def plus_1_not_0)
+
+lemma "inc = (\<lambda>y. y + 1)"
+sledgehammer [expect = some] (inc_def)
+by (metis inc_def)
+
+lemma "(\<lambda>y. y + 1) = inc"
+sledgehammer [expect = some] (inc_def)
+by (metis inc_def)
+
+definition add_swap :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
+"add_swap = (\<lambda>x y. y + x)"
+
+lemma "add_swap m n = n + m"
+sledgehammer [expect = some] (add_swap_def)
+by (metis add_swap_def)
+
+
text {* Definitional CNF for facts *}
declare [[meson_max_clauses = 10]]
@@ -83,6 +114,7 @@
(r 3 0 \<and> r 3 1 \<and> r 3 2 \<and> r 3 3)"
by (metisFT rax)
+
text {* Definitional CNF for goal *}
axiomatization p :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
@@ -108,6 +140,7 @@
(p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
by (metisFT pax)
+
text {* New Skolemizer *}
declare [[metis_new_skolemizer]]
--- a/src/HOL/Tools/Meson/meson.ML Thu May 12 15:29:19 2011 +0200
+++ b/src/HOL/Tools/Meson/meson.ML Thu May 12 15:29:19 2011 +0200
@@ -22,6 +22,8 @@
val choice_theorems : theory -> thm list
val skolemize_with_choice_theorems : Proof.context -> thm list -> thm -> thm
val skolemize : Proof.context -> thm -> thm
+ val extensionalize_conv : Proof.context -> conv
+ val extensionalize_theorem : Proof.context -> thm -> thm
val is_fol_term: theory -> term -> bool
val make_clauses_unsorted: thm list -> thm list
val make_clauses: thm list -> thm list
@@ -610,12 +612,37 @@
skolemize_with_choice_theorems ctxt (choice_theorems thy)
end
+fun is_Abs (Abs _) = true
+ | is_Abs _ = false
+
+(* Removes the lambdas from an equation of the form "t = (%x. u)". *)
+fun extensionalize_conv ctxt ct =
+ case term_of ct of
+ Const (@{const_name HOL.eq}, _) $ t1 $ t2 =>
+ ct |> (if is_Abs t1 orelse is_Abs t2 then
+ Conv.rewr_conv @{thm fun_eq_iff [THEN eq_reflection]}
+ then_conv extensionalize_conv ctxt
+ else
+ Conv.comb_conv (extensionalize_conv ctxt))
+ | _ $ _ => Conv.comb_conv (extensionalize_conv ctxt) ct
+ | Abs _ => Conv.abs_conv (extensionalize_conv o snd) ctxt ct
+ | _ => Conv.all_conv ct
+
+val extensionalize_theorem = Conv.fconv_rule o extensionalize_conv
+
(* "RS" can fail if "unify_search_bound" is too small. *)
-fun try_skolemize ctxt th =
- try (skolemize ctxt) th
- |> tap (fn NONE => trace_msg ctxt (fn () => "Failed to skolemize " ^
- Display.string_of_thm ctxt th)
- | _ => ())
+fun try_skolemize_etc ctxt =
+ Raw_Simplifier.rewrite_rule (unfold_set_const_simps ctxt)
+ (* Extensionalize "th", because that makes sense and that's what Sledgehammer
+ does, but also keep an unextensionalized version of "th" for backward
+ compatibility. *)
+ #> (fn th => insert Thm.eq_thm_prop (extensionalize_theorem ctxt th) [th])
+ #> map_filter (fn th => try (skolemize ctxt) th
+ |> tap (fn NONE =>
+ trace_msg ctxt (fn () =>
+ "Failed to skolemize " ^
+ Display.string_of_thm ctxt th)
+ | _ => ()))
fun add_clauses th cls =
let val ctxt0 = Variable.global_thm_context th
@@ -645,7 +672,7 @@
fun gocls cls = name_thms "Goal#" (map make_goal (neg_clauses cls));
fun skolemize_prems_tac ctxt prems =
- cut_facts_tac (map_filter (try_skolemize ctxt) prems) THEN' REPEAT o etac exE
+ cut_facts_tac (maps (try_skolemize_etc ctxt) prems) THEN' REPEAT o etac exE
(*Basis of all meson-tactics. Supplies cltac with clauses: HOL disjunctions.
Function mkcl converts theorems to clauses.*)
--- a/src/HOL/Tools/Meson/meson_clausify.ML Thu May 12 15:29:19 2011 +0200
+++ b/src/HOL/Tools/Meson/meson_clausify.ML Thu May 12 15:29:19 2011 +0200
@@ -10,7 +10,6 @@
val new_skolem_var_prefix : string
val new_nonskolem_var_prefix : string
val is_zapped_var_name : string -> bool
- val extensionalize_theorem : thm -> thm
val introduce_combinators_in_cterm : cterm -> thm
val introduce_combinators_in_theorem : thm -> thm
val cluster_of_zapped_var_name : string -> (int * (int * int)) * bool
@@ -87,16 +86,6 @@
(**** 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 Meson.skolem}, _) $ _) = true
| is_quasi_lambda_free (t1 $ t2) =
is_quasi_lambda_free t1 andalso is_quasi_lambda_free t2
@@ -321,7 +310,7 @@
val (th, ctxt) = Variable.import true [th] ctxt |>> snd |>> the_single
val th = th |> Conv.fconv_rule Object_Logic.atomize
|> Raw_Simplifier.rewrite_rule (unfold_set_const_simps ctxt)
- |> extensionalize_theorem
+ |> extensionalize_theorem ctxt
|> make_nnf ctxt
in
if new_skolemizer then
--- a/src/HOL/Tools/Metis/metis_tactics.ML Thu May 12 15:29:19 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_tactics.ML Thu May 12 15:29:19 2011 +0200
@@ -132,20 +132,9 @@
(if Config.get ctxt verbose then "\n" ^ loc ^ ": " ^ msg
else ""))
-(* Extensionalize "th", because that makes sense and that's what Sledgehammer
- does, but also keep an unextensionalized version of "th" for backward
- compatibility. *)
-fun also_extensionalize_theorem th =
- 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
-
fun neg_clausify ctxt =
single
#> Meson.make_clauses_unsorted
- #> maps (Raw_Simplifier.rewrite_rule (Meson.unfold_set_const_simps ctxt)
- #> also_extensionalize_theorem)
#> map Meson_Clausify.introduce_combinators_in_theorem
#> Meson.finish_cnf
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Thu May 12 15:29:19 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Thu May 12 15:29:19 2011 +0200
@@ -355,24 +355,11 @@
subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j))
(0 upto length Ts - 1 ~~ Ts))
-(* Removes the lambdas from an equation of the form "t = (%x. u)".
- (Cf. "extensionalize_theorem" in "Meson_Clausify".) *)
-fun extensionalize_term t =
- let
- fun aux j (@{const Trueprop} $ t') = @{const Trueprop} $ aux j t'
- | aux j (t as Const (s, Type (_, [Type (_, [_, T']),
- Type (_, [_, res_T])]))
- $ t2 $ Abs (var_s, var_T, t')) =
- if s = @{const_name HOL.eq} orelse s = @{const_name "=="} then
- let val var_t = Var ((var_s, j), var_T) in
- Const (s, T' --> T' --> res_T)
- $ betapply (t2, var_t) $ subst_bound (var_t, t')
- |> aux (j + 1)
- end
- else
- t
- | aux _ t = t
- in aux (maxidx_of_term t + 1) t end
+fun extensionalize_term ctxt t =
+ let val thy = Proof_Context.theory_of ctxt in
+ t |> cterm_of thy |> Meson.extensionalize_conv ctxt
+ |> prop_of |> Logic.dest_equals |> snd
+ end
fun introduce_combinators_in_term ctxt kind t =
let val thy = Proof_Context.theory_of ctxt in
@@ -436,7 +423,7 @@
val t = t |> need_trueprop ? HOLogic.mk_Trueprop
|> Raw_Simplifier.rewrite_term thy
(Meson.unfold_set_const_simps ctxt) []
- |> extensionalize_term
+ |> extensionalize_term ctxt
|> presimp ? presimplify_term thy
|> perhaps (try (HOLogic.dest_Trueprop))
|> introduce_combinators_in_term ctxt kind