added extensionalization to Sledgehammer, mimicking what the Clausifier used to do
--- a/src/HOL/Tools/ATP_Manager/atp_systems.ML Mon Jul 26 17:26:02 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML Mon Jul 26 17:56:10 2010 +0200
@@ -153,12 +153,29 @@
|>> APred ||> union (op =) ts)
in do_formula [] end
+(* Removes the lambdas from an equation of the form "t = (%x. u)" (cf.
+ "extensionalize_theorem" in "Clausifier"). *)
+fun extensionalize_term t =
+ let
+ fun aux j (Const (@{const_name "op ="}, _) $ t2 $ Abs (s, var_T, t')) =
+ let
+ val T' = fastype_of t'
+ val var_t = Var (("x", j), var_T)
+ in
+ Const (@{const_name "op ="}, T' --> T' --> HOLogic.boolT)
+ $ betapply (t2, var_t) $ subst_bound (var_t, t')
+ |> aux (j + 1)
+ end
+ | aux _ t = t
+ in aux (maxidx_of_term t + 1) t end
+
(* making axiom and conjecture clauses *)
fun make_clause thy (formula_id, formula_name, kind, t) =
let
(* ### FIXME: introduce combinators and perform other transformations
previously done by Clausifier.to_nnf *)
val t = t |> Object_Logic.atomize_term thy
+ |> extensionalize_term
val (combformula, ctypes_sorts) = combformula_for_prop thy t []
in
FOLFormula {formula_name = formula_name, formula_id = formula_id,
--- a/src/HOL/Tools/Sledgehammer/clausifier.ML Mon Jul 26 17:26:02 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/clausifier.ML Mon Jul 26 17:56:10 2010 +0200
@@ -82,11 +82,13 @@
val fun_cong_all = @{thm expand_fun_eq [THEN iffD1]}
-(* Removes the lambdas from an equation of the form t = (%x. u). *)
-fun extensionalize th =
+(* ### FIXME: removes only one lambda? *)
+(* Removes the lambdas from an equation of the form "t = (%x. u)" (cf.
+ "extensionalize_term" in "ATP_Systems"). *)
+fun extensionalize_theorem th =
case prop_of th of
_ $ (Const (@{const_name "op ="}, Type (_, [Type (@{type_name fun}, _), _]))
- $ _ $ Abs (s, _, _)) => extensionalize (th RS fun_cong_all)
+ $ _ $ Abs (s, _, _)) => extensionalize_theorem (th RS fun_cong_all)
| _ => th
fun is_quasi_lambda_free (Const (@{const_name skolem_id}, _) $ _) = true
@@ -226,7 +228,7 @@
let val th1 = th |> transform_elim |> zero_var_indexes
val ((_, [th2]), ctxt) = Variable.import true [th1] ctxt0
val th3 = th2 |> Conv.fconv_rule Object_Logic.atomize
- |> extensionalize
+ |> extensionalize_theorem
|> Meson.make_nnf ctxt
in (th3, ctxt) end;