1.1 --- a/src/HOL/Tools/Metis/metis_tactic.ML	Fri Nov 18 11:47:12 2011 +0100
     1.2 +++ b/src/HOL/Tools/Metis/metis_tactic.ML	Fri Nov 18 11:47:12 2011 +0100
     1.3 @@ -67,22 +67,43 @@
     1.4      val ct = cterm_of thy (HOLogic.mk_Trueprop t)
     1.5    in Goal.prove_internal [] ct (K tac) |> Meson.make_meta_clause end
     1.6  
     1.7 +fun add_vars_and_frees (t $ u) = fold (add_vars_and_frees) [t, u]
     1.8 +  | add_vars_and_frees (Abs (_, _, t)) = add_vars_and_frees t
     1.9 +  | add_vars_and_frees (t as Var _) = insert (op =) t
    1.10 +  | add_vars_and_frees (t as Free _) = insert (op =) t
    1.11 +  | add_vars_and_frees _ = I
    1.12 +
    1.13  fun introduce_lam_wrappers ctxt th =
    1.14    if Meson_Clausify.is_quasi_lambda_free (prop_of th) then
    1.15      th
    1.16    else
    1.17      let
    1.18 -      fun conv wrap ctxt ct =
    1.19 +      val thy = Proof_Context.theory_of ctxt
    1.20 +      fun conv first ctxt ct =
    1.21          if Meson_Clausify.is_quasi_lambda_free (term_of ct) then
    1.22            Thm.reflexive ct
    1.23          else case term_of ct of
    1.24 -          Abs _ =>
    1.25 -          Conv.abs_conv (conv false o snd) ctxt ct
    1.26 -          |> wrap
    1.27 -             ? (fn th => Meson.first_order_resolve th @{thm Metis.eq_lambdaI})
    1.28 +          t as Abs (_, _, u) =>
    1.29 +          if first then
    1.30 +            case add_vars_and_frees u [] of
    1.31 +              [] =>
    1.32 +              Conv.abs_conv (conv false o snd) ctxt ct
    1.33 +              |> (fn th => Meson.first_order_resolve th @{thm Metis.eq_lambdaI})
    1.34 +            | v :: _ =>
    1.35 +              Abs (Name.uu, fastype_of v, abstract_over (v, term_of ct)) $ v
    1.36 +              |> cterm_of thy
    1.37 +              |> Conv.comb_conv (conv true ctxt)
    1.38 +          else
    1.39 +            Conv.abs_conv (conv false o snd) ctxt ct
    1.40 +        | Const (@{const_name Meson.skolem}, _) $ _ => Thm.reflexive ct
    1.41          | _ => Conv.comb_conv (conv true ctxt) ct
    1.42 -      val eqth = conv true ctxt (cprop_of th)
    1.43 -    in Thm.equal_elim eqth th end
    1.44 +      val eq_th = conv true ctxt (cprop_of th)
    1.45 +      (* We replace the equation's left-hand side with a beta-equivalent term
    1.46 +         so that "Thm.equal_elim" works below. *)
    1.47 +      val t0 $ _ $ t2 = prop_of eq_th
    1.48 +      val eq_ct = t0 $ prop_of th $ t2 |> cterm_of thy
    1.49 +      val eq_th' = Goal.prove_internal [] eq_ct (K (Tactic.rtac eq_th 1))
    1.50 +    in Thm.equal_elim eq_th' th end
    1.51  
    1.52  val clause_params =
    1.53    {ordering = Metis_KnuthBendixOrder.default,
    1.54 @@ -104,19 +125,18 @@
    1.55    let val thy = Proof_Context.theory_of ctxt
    1.56        val new_skolemizer =
    1.57          Config.get ctxt new_skolemizer orelse null (Meson.choice_theorems thy)
    1.58 -      val preproc =
    1.59 -        Drule.eta_contraction_rule
    1.60 -        #> lam_trans = lam_liftingN ? introduce_lam_wrappers ctxt
    1.61 -      val cls = cls |> map preproc
    1.62 -      val ths0 = ths0 |> map preproc
    1.63 +      val do_lams = lam_trans = lam_liftingN ? introduce_lam_wrappers ctxt
    1.64        val th_cls_pairs =
    1.65          map2 (fn j => fn th =>
    1.66                  (Thm.get_name_hint th,
    1.67 -                 Meson_Clausify.cnf_axiom ctxt new_skolemizer
    1.68 -                                          (lam_trans = combinatorsN) j th))
    1.69 +                 th |> Drule.eta_contraction_rule
    1.70 +                    |> Meson_Clausify.cnf_axiom ctxt new_skolemizer
    1.71 +                                                (lam_trans = combinatorsN) j
    1.72 +                    ||> map do_lams))
    1.73               (0 upto length ths0 - 1) ths0
    1.74        val ths = maps (snd o snd) th_cls_pairs
    1.75        val dischargers = map (fst o snd) th_cls_pairs
    1.76 +      val cls = cls |> map (Drule.eta_contraction_rule #> do_lams)
    1.77        val _ = trace_msg ctxt (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
    1.78        val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) cls
    1.79        val _ = trace_msg ctxt (fn () => "type_enc = " ^ type_enc)