author blanchet Thu, 12 May 2011 15:29:19 +0200 changeset 42747 f132d13fcf75 parent 42746 7e227e9de779 child 42748 a37095d03074
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"
+
+
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)
+                                   | _ => ()))

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```