1.1 --- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Fri Nov 18 11:47:12 2011 +0100
     1.2 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Fri Nov 18 11:47:12 2011 +0100
     1.3 @@ -57,7 +57,7 @@
     1.4      lits |> map (atp_literal_from_metis type_enc) |> mk_aconns AOr
     1.5  
     1.6  fun polish_hol_terms ctxt (lifted, old_skolems) =
     1.7 -  map (reveal_lambda_lifted lifted #> reveal_old_skolem_terms old_skolems)
     1.8 +  map (reveal_lam_lifted lifted #> reveal_old_skolem_terms old_skolems)
     1.9    #> Syntax.check_terms (Proof_Context.set_mode Proof_Context.mode_pattern ctxt)
    1.10  
    1.11  fun hol_clause_from_metis ctxt type_enc sym_tab concealed =

     2.1 --- a/src/HOL/Tools/Metis/metis_tactic.ML	Fri Nov 18 11:47:12 2011 +0100
     2.2 +++ b/src/HOL/Tools/Metis/metis_tactic.ML	Fri Nov 18 11:47:12 2011 +0100
     2.3 @@ -59,7 +59,7 @@
     2.4    end
     2.5    |> Meson.make_meta_clause
     2.6  
     2.7 -fun lambda_lifted_from_metis ctxt type_enc sym_tab concealed mth =
     2.8 +fun lam_lifted_from_metis ctxt type_enc sym_tab concealed mth =
     2.9    let
    2.10      val thy = Proof_Context.theory_of ctxt
    2.11      val tac = rewrite_goals_tac @{thms lambda_def_raw} THEN rtac refl 1
    2.12 @@ -67,7 +67,7 @@
    2.13      val ct = cterm_of thy (HOLogic.mk_Trueprop t)
    2.14    in Goal.prove_internal [] ct (K tac) |> Meson.make_meta_clause end
    2.15  
    2.16 -fun introduce_lambda_wrappers_in_theorem ctxt th =
    2.17 +fun introduce_lam_wrappers ctxt th =
    2.18    if Meson_Clausify.is_quasi_lambda_free (prop_of th) then
    2.19      th
    2.20    else
    2.21 @@ -104,8 +104,11 @@
    2.22    let val thy = Proof_Context.theory_of ctxt
    2.23        val new_skolemizer =
    2.24          Config.get ctxt new_skolemizer orelse null (Meson.choice_theorems thy)
    2.25 -      val cls = cls |> map Drule.eta_contraction_rule
    2.26 -      val ths0 = ths0 |> map Drule.eta_contraction_rule
    2.27 +      val preproc =
    2.28 +        Drule.eta_contraction_rule
    2.29 +        #> lam_trans = lam_liftingN ? introduce_lam_wrappers ctxt
    2.30 +      val cls = cls |> map preproc
    2.31 +      val ths0 = ths0 |> map preproc
    2.32        val th_cls_pairs =
    2.33          map2 (fn j => fn th =>
    2.34                  (Thm.get_name_hint th,
    2.35 @@ -118,16 +121,14 @@
    2.36        val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) cls
    2.37        val _ = trace_msg ctxt (fn () => "type_enc = " ^ type_enc)
    2.38        val type_enc = type_enc_from_string Sound type_enc
    2.39 -      val (sym_tab, axioms0, concealed) =
    2.40 +      val (sym_tab, axioms, concealed) =
    2.41          prepare_metis_problem ctxt type_enc lam_trans cls ths
    2.42        fun get_isa_thm mth Isa_Reflexive_or_Trivial =
    2.43            reflexive_or_trivial_from_metis ctxt type_enc sym_tab concealed mth
    2.44          | get_isa_thm mth Isa_Lambda_Lifted =
    2.45 -          lambda_lifted_from_metis ctxt type_enc sym_tab concealed mth
    2.46 -        | get_isa_thm _ (Isa_Raw ith) =
    2.47 -          ith |> lam_trans = lam_liftingN
    2.48 -                 ? introduce_lambda_wrappers_in_theorem ctxt
    2.49 -      val axioms = axioms0 |> map (fn (mth, ith) => (mth, get_isa_thm mth ith))
    2.50 +          lam_lifted_from_metis ctxt type_enc sym_tab concealed mth
    2.51 +        | get_isa_thm _ (Isa_Raw ith) = ith
    2.52 +      val axioms = axioms |> map (fn (mth, ith) => (mth, get_isa_thm mth ith))
    2.53        val _ = trace_msg ctxt (fn () => "ISABELLE CLAUSES")
    2.54        val _ = app (fn (_, ith) => trace_msg ctxt (fn () => Display.string_of_thm ctxt ith)) axioms
    2.55        val _ = trace_msg ctxt (fn () => "METIS CLAUSES")
    2.56 @@ -149,9 +150,7 @@
    2.57                  val result =
    2.58                    axioms
    2.59                    |> fold (replay_one_inference ctxt' type_enc concealed sym_tab) proof
    2.60 -                val used =
    2.61 -                  proof |> map_filter (used_axioms axioms0)
    2.62 -                        |> map_filter (fn Isa_Raw ith => SOME ith | _ => NONE)
    2.63 +                val used = proof |> map_filter (used_axioms axioms)
    2.64                  val _ = trace_msg ctxt (fn () => "METIS COMPLETED...clauses actually used:")
    2.65                  val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) used
    2.66                  val names = th_cls_pairs |> map fst

     3.1 --- a/src/HOL/Tools/Metis/metis_translate.ML	Fri Nov 18 11:47:12 2011 +0100
     3.2 +++ b/src/HOL/Tools/Metis/metis_translate.ML	Fri Nov 18 11:47:12 2011 +0100
     3.3 @@ -28,7 +28,7 @@
     3.4    val verbose_warning : Proof.context -> string -> unit
     3.5    val metis_name_table : ((string * int) * ((type_enc -> string) * bool)) list
     3.6    val reveal_old_skolem_terms : (string * term) list -> term -> term
     3.7 -  val reveal_lambda_lifted : (string * term) list -> term -> term
     3.8 +  val reveal_lam_lifted : (string * term) list -> term -> term
     3.9    val prepare_metis_problem :
    3.10      Proof.context -> type_enc -> string -> thm list -> thm list
    3.11      -> int Symtab.table * (Metis_Thm.thm * isa_thm) list
    3.12 @@ -110,14 +110,14 @@
    3.13                     t
    3.14                 | t => t)
    3.15  
    3.16 -fun reveal_lambda_lifted lambdas =
    3.17 +fun reveal_lam_lifted lambdas =
    3.18    map_aterms (fn t as Const (s, _) =>
    3.19                   if String.isPrefix lam_lifted_prefix s then
    3.20                     case AList.lookup (op =) lambdas s of
    3.21                       SOME t =>
    3.22                       Const (@{const_name Metis.lambda}, dummyT)
    3.23                       $ map_types (map_type_tvar (K dummyT))
    3.24 -                                 (reveal_lambda_lifted lambdas t)
    3.25 +                                 (reveal_lam_lifted lambdas t)
    3.26                     | NONE => t
    3.27                   else
    3.28                     t
    3.29 @@ -199,6 +199,14 @@
    3.30      end
    3.31    | metis_axiom_from_atp _ _ _ = raise Fail "not CNF -- expected formula"
    3.32  
    3.33 +fun eliminate_lam_wrappers (Const (@{const_name Metis.lambda}, _) $ t) =
    3.34 +    eliminate_lam_wrappers t
    3.35 +  | eliminate_lam_wrappers (t $ u) =
    3.36 +    eliminate_lam_wrappers t $ eliminate_lam_wrappers u
    3.37 +  | eliminate_lam_wrappers (Abs (s, T, t)) =
    3.38 +    Abs (s, T, eliminate_lam_wrappers t)
    3.39 +  | eliminate_lam_wrappers t = t
    3.40 +
    3.41  (* Function to generate metis clauses, including comb and type clauses *)
    3.42  fun prepare_metis_problem ctxt type_enc lam_trans conj_clauses fact_clauses =
    3.43    let
    3.44 @@ -223,6 +231,7 @@
    3.45        fold_rev (fn (name, th) => fn (old_skolems, props) =>
    3.46                     th |> prop_of |> Logic.strip_imp_concl
    3.47                        |> conceal_old_skolem_terms (length clauses) old_skolems
    3.48 +                      ||> lam_trans = lam_liftingN ? eliminate_lam_wrappers
    3.49                        ||> (fn prop => (name, prop) :: props))
    3.50                 clauses ([], [])
    3.51      (*