continued implementation of lambda-lifting in Metis
authorblanchet
Tue Nov 15 22:13:39 2011 +0100 (2011-11-15)
changeset 455119b0f8ca4388e
parent 45510 96696c360b3e
child 45512 a6cce8032fff
continued implementation of lambda-lifting in Metis
src/HOL/Metis.thy
src/HOL/Tools/ATP/atp_reconstruct.ML
src/HOL/Tools/ATP/atp_translate.ML
src/HOL/Tools/ATP/atp_util.ML
src/HOL/Tools/Meson/meson_clausify.ML
src/HOL/Tools/Metis/metis_reconstruct.ML
src/HOL/Tools/Metis/metis_tactic.ML
src/HOL/Tools/Metis/metis_translate.ML
src/HOL/Tools/cnf_funcs.ML
     1.1 --- a/src/HOL/Metis.thy	Tue Nov 15 22:13:39 2011 +0100
     1.2 +++ b/src/HOL/Metis.thy	Tue Nov 15 22:13:39 2011 +0100
     1.3 @@ -15,7 +15,7 @@
     1.4       ("Tools/try_methods.ML")
     1.5  begin
     1.6  
     1.7 -subsection {* Literal selection helpers *}
     1.8 +subsection {* Literal selection and lambda-lifting helpers *}
     1.9  
    1.10  definition select :: "'a \<Rightarrow> 'a" where
    1.11  [no_atp]: "select = (\<lambda>x. x)"
    1.12 @@ -31,6 +31,12 @@
    1.13  
    1.14  lemma select_FalseI: "False \<Longrightarrow> select False" by simp
    1.15  
    1.16 +definition lambda :: "'a \<Rightarrow> 'a" where
    1.17 +[no_atp]: "lambda = (\<lambda>x. x)"
    1.18 +
    1.19 +lemma eq_lambdaI: "x \<equiv> y \<Longrightarrow> x \<equiv> lambda y"
    1.20 +unfolding lambda_def by assumption
    1.21 +
    1.22  
    1.23  subsection {* Metis package *}
    1.24  
    1.25 @@ -40,10 +46,11 @@
    1.26  
    1.27  setup {* Metis_Tactic.setup *}
    1.28  
    1.29 -hide_const (open) fFalse fTrue fNot fconj fdisj fimplies fequal select
    1.30 +hide_const (open) fFalse fTrue fNot fconj fdisj fimplies fequal select lambda
    1.31  hide_fact (open) fFalse_def fTrue_def fNot_def fconj_def fdisj_def fimplies_def
    1.32      fequal_def select_def not_atomize atomize_not_select not_atomize_select
    1.33 -    select_FalseI
    1.34 +    select_FalseI lambda_def eq_lambdaI
    1.35 +
    1.36  
    1.37  subsection {* Try Methods *}
    1.38  
     2.1 --- a/src/HOL/Tools/ATP/atp_reconstruct.ML	Tue Nov 15 22:13:39 2011 +0100
     2.2 +++ b/src/HOL/Tools/ATP/atp_reconstruct.ML	Tue Nov 15 22:13:39 2011 +0100
     2.3 @@ -283,26 +283,26 @@
     2.4     constrained by information from type literals, or by type inference. *)
     2.5  fun typ_from_atp ctxt (u as ATerm (a, us)) =
     2.6    let val Ts = map (typ_from_atp ctxt) us in
     2.7 -    case strip_prefix_and_unascii type_const_prefix a of
     2.8 +    case unprefix_and_unascii type_const_prefix a of
     2.9        SOME b => Type (invert_const b, Ts)
    2.10      | NONE =>
    2.11        if not (null us) then
    2.12          raise HO_TERM [u]  (* only "tconst"s have type arguments *)
    2.13 -      else case strip_prefix_and_unascii tfree_prefix a of
    2.14 +      else case unprefix_and_unascii tfree_prefix a of
    2.15          SOME b => make_tfree ctxt b
    2.16        | NONE =>
    2.17          (* Could be an Isabelle variable or a variable from the ATP, say "X1"
    2.18             or "_5018". Sometimes variables from the ATP are indistinguishable
    2.19             from Isabelle variables, which forces us to use a type parameter in
    2.20             all cases. *)
    2.21 -        (a |> perhaps (strip_prefix_and_unascii tvar_prefix), HOLogic.typeS)
    2.22 +        (a |> perhaps (unprefix_and_unascii tvar_prefix), HOLogic.typeS)
    2.23          |> Type_Infer.param 0
    2.24    end
    2.25  
    2.26  (* Type class literal applied to a type. Returns triple of polarity, class,
    2.27     type. *)
    2.28  fun type_constraint_from_term ctxt (u as ATerm (a, us)) =
    2.29 -  case (strip_prefix_and_unascii class_prefix a, map (typ_from_atp ctxt) us) of
    2.30 +  case (unprefix_and_unascii class_prefix a, map (typ_from_atp ctxt) us) of
    2.31      (SOME b, [T]) => (b, T)
    2.32    | _ => raise HO_TERM [u]
    2.33  
    2.34 @@ -335,6 +335,8 @@
    2.35  fun num_type_args thy s =
    2.36    if String.isPrefix skolem_const_prefix s then
    2.37      s |> space_explode Long_Name.separator |> List.last |> Int.fromString |> the
    2.38 +  else if String.isPrefix lambda_lifted_prefix s then
    2.39 +    if String.isPrefix lambda_lifted_poly_prefix s then 2 else 0
    2.40    else
    2.41      (s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length
    2.42  
    2.43 @@ -364,7 +366,7 @@
    2.44              else
    2.45                list_comb (Const (@{const_name HOL.eq}, HOLogic.typeT), ts)
    2.46            end
    2.47 -        else case strip_prefix_and_unascii const_prefix s of
    2.48 +        else case unprefix_and_unascii const_prefix s of
    2.49            SOME s' =>
    2.50            let
    2.51              val ((s', s''), mangled_us) =
    2.52 @@ -429,12 +431,10 @@
    2.53                  SOME T => map slack_fastype_of term_ts ---> T
    2.54                | NONE => map slack_fastype_of ts ---> HOLogic.typeT
    2.55              val t =
    2.56 -              case strip_prefix_and_unascii fixed_var_prefix s of
    2.57 -                SOME s =>
    2.58 -                (* FIXME: reconstruction of lambda-lifting *)
    2.59 -                Free (s, T)
    2.60 +              case unprefix_and_unascii fixed_var_prefix s of
    2.61 +                SOME s => Free (s, T)
    2.62                | NONE =>
    2.63 -                case strip_prefix_and_unascii schematic_var_prefix s of
    2.64 +                case unprefix_and_unascii schematic_var_prefix s of
    2.65                    SOME s => Var ((s, var_index), T)
    2.66                  | NONE =>
    2.67                    Var ((s |> textual ? repair_variable_name Char.toLower,
     3.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Tue Nov 15 22:13:39 2011 +0100
     3.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Tue Nov 15 22:13:39 2011 +0100
     3.3 @@ -46,6 +46,8 @@
     3.4    val type_const_prefix : string
     3.5    val class_prefix : string
     3.6    val lambda_lifted_prefix : string
     3.7 +  val lambda_lifted_mono_prefix : string
     3.8 +  val lambda_lifted_poly_prefix : string
     3.9    val skolem_const_prefix : string
    3.10    val old_skolem_const_prefix : string
    3.11    val new_skolem_const_prefix : string
    3.12 @@ -59,6 +61,7 @@
    3.13    val class_rel_clause_prefix : string
    3.14    val arity_clause_prefix : string
    3.15    val tfree_clause_prefix : string
    3.16 +  val lambda_fact_prefix : string
    3.17    val typed_helper_suffix : string
    3.18    val untyped_helper_suffix : string
    3.19    val type_tag_idempotence_helper_name : string
    3.20 @@ -72,7 +75,7 @@
    3.21    val prefixed_type_tag_name : string
    3.22    val ascii_of : string -> string
    3.23    val unascii_of : string -> string
    3.24 -  val strip_prefix_and_unascii : string -> string -> string option
    3.25 +  val unprefix_and_unascii : string -> string -> string option
    3.26    val proxy_table : (string * (string * (thm * (string * string)))) list
    3.27    val proxify_const : string -> (string * string) option
    3.28    val invert_const : string -> string
    3.29 @@ -228,7 +231,7 @@
    3.30  
    3.31  (* If string s has the prefix s1, return the result of deleting it,
    3.32     un-ASCII'd. *)
    3.33 -fun strip_prefix_and_unascii s1 s =
    3.34 +fun unprefix_and_unascii s1 s =
    3.35    if String.isPrefix s1 s then
    3.36      SOME (unascii_of (String.extract (s, size s1, NONE)))
    3.37    else
    3.38 @@ -488,7 +491,7 @@
    3.39  fun robust_const_type thy s =
    3.40    if s = app_op_name then
    3.41      Logic.varifyT_global @{typ "('a => 'b) => 'a => 'b"}
    3.42 -  else if String.isPrefix lambda_lifted_poly_prefix s then
    3.43 +  else if String.isPrefix lambda_lifted_prefix s then
    3.44      Logic.varifyT_global @{typ "'a => 'b"}
    3.45    else
    3.46      (* Old Skolems throw a "TYPE" exception here, which will be caught. *)
    3.47 @@ -500,8 +503,11 @@
    3.48      let val (T1, T2) = T |> domain_type |> dest_funT in [T1, T2] end
    3.49    else if String.isPrefix old_skolem_const_prefix s then
    3.50      [] |> Term.add_tvarsT T |> rev |> map TVar
    3.51 -  else if String.isPrefix lambda_lifted_poly_prefix s then
    3.52 -    let val (T1, T2) = T |> dest_funT in [T1, T2] end
    3.53 +  else if String.isPrefix lambda_lifted_prefix s then
    3.54 +    if String.isPrefix lambda_lifted_poly_prefix s then
    3.55 +      let val (T1, T2) = T |> dest_funT in [T1, T2] end
    3.56 +    else
    3.57 +      []
    3.58    else
    3.59      (s, T) |> Sign.const_typargs thy
    3.60  
    3.61 @@ -678,16 +684,21 @@
    3.62      (if String.isPrefix lambda_lifted_prefix s then Const else Free) x
    3.63    | constify_lifted t = t
    3.64  
    3.65 +(* Requires bound variables to have distinct names and not to clash with any
    3.66 +   schematic variables (as should be the case right after lambda-lifting). *)
    3.67 +fun open_form (Const (@{const_name All}, _) $ Abs (s, T, t)) =
    3.68 +    open_form (subst_bound (Var ((s, 0), T), t))
    3.69 +  | open_form t = t
    3.70 +
    3.71  fun lift_lambdas ctxt type_enc =
    3.72 -  map (close_form o Envir.eta_contract) #> rpair ctxt
    3.73 +  map (Envir.eta_contract #> close_form) #> rpair ctxt
    3.74    #-> Lambda_Lifting.lift_lambdas
    3.75            (SOME (if polymorphism_of_type_enc type_enc = Polymorphic then
    3.76                     lambda_lifted_poly_prefix
    3.77                   else
    3.78                     lambda_lifted_mono_prefix))
    3.79            Lambda_Lifting.is_quantifier
    3.80 -  #> fst
    3.81 -  #> pairself (map constify_lifted)
    3.82 +  #> fst #> pairself (map (open_form o constify_lifted))
    3.83  
    3.84  fun intentionalize_def (Const (@{const_name All}, _) $ Abs (_, _, t)) =
    3.85      intentionalize_def t
    3.86 @@ -968,7 +979,7 @@
    3.87        fun mangle (IApp (tm1, tm2)) = IApp (mangle tm1, mangle tm2)
    3.88          | mangle (tm as IConst (_, _, [])) = tm
    3.89          | mangle (tm as IConst (name as (s, _), T, T_args)) =
    3.90 -          (case strip_prefix_and_unascii const_prefix s of
    3.91 +          (case unprefix_and_unascii const_prefix s of
    3.92               NONE => tm
    3.93             | SOME s'' =>
    3.94               case type_arg_policy type_enc (invert_const s'') of
    3.95 @@ -1004,7 +1015,7 @@
    3.96      fun filt ary (IApp (tm1, tm2)) = IApp (filt (ary + 1) tm1, filt 0 tm2)
    3.97        | filt _ (tm as IConst (_, _, [])) = tm
    3.98        | filt ary (IConst (name as (s, _), T, T_args)) =
    3.99 -        (case strip_prefix_and_unascii const_prefix s of
   3.100 +        (case unprefix_and_unascii const_prefix s of
   3.101             NONE =>
   3.102             (name,
   3.103              if level_of_type_enc type_enc = No_Types orelse s = tptp_choice then
   3.104 @@ -1223,7 +1234,7 @@
   3.105  (** Finite and infinite type inference **)
   3.106  
   3.107  fun tvar_footprint thy s ary =
   3.108 -  (case strip_prefix_and_unascii const_prefix s of
   3.109 +  (case unprefix_and_unascii const_prefix s of
   3.110       SOME s =>
   3.111       s |> invert_const |> robust_const_type thy |> chop_fun ary |> fst
   3.112         |> map (fn T => Term.add_tvarsT T [] |> map fst)
   3.113 @@ -1446,7 +1457,7 @@
   3.114    case Symtab.lookup sym_tab s of
   3.115      SOME ({min_ary, ...} : sym_info) => min_ary
   3.116    | NONE =>
   3.117 -    case strip_prefix_and_unascii const_prefix s of
   3.118 +    case unprefix_and_unascii const_prefix s of
   3.119        SOME s =>
   3.120        let val s = s |> unmangled_const_name |> invert_const in
   3.121          if s = predicator_name then 1
   3.122 @@ -1581,7 +1592,7 @@
   3.123    not (null (Term.hidden_polymorphism t))
   3.124  
   3.125  fun helper_facts_for_sym ctxt format type_enc (s, {types, ...} : sym_info) =
   3.126 -  case strip_prefix_and_unascii const_prefix s of
   3.127 +  case unprefix_and_unascii const_prefix s of
   3.128      SOME mangled_s =>
   3.129      let
   3.130        val thy = Proof_Context.theory_of ctxt
   3.131 @@ -1657,21 +1668,37 @@
   3.132  fun type_constrs_of_terms thy ts =
   3.133    Symtab.keys (fold (add_type_constrs_in_term thy) ts Symtab.empty)
   3.134  
   3.135 -val extract_lambda_def =
   3.136 -  let
   3.137 -    fun extr [] (@{const Trueprop} $ t) = extr [] t
   3.138 -      | extr bs (Const (@{const_name All}, _) $ Abs (s, T, t)) =
   3.139 -        extr ((s, T) :: bs) t
   3.140 -      | extr bs (Const (@{const_name HOL.eq}, _) $ t $ u) =
   3.141 -        (t |> head_of |> dest_Const |> fst,
   3.142 -         fold_rev (fn (s, T) => fn u => Abs (s, T, u)) bs u)
   3.143 -      | extr _ _ = raise Fail "malformed lifted lambda"
   3.144 -  in extr [] end
   3.145 +fun extract_lambda_def (Const (@{const_name HOL.eq}, _) $ t $ u) =
   3.146 +    let val (head, args) = strip_comb t in
   3.147 +      (head |> dest_Const |> fst,
   3.148 +       fold_rev (fn t as Var ((s, _), T) =>
   3.149 +                    (fn u => Abs (s, T, abstract_over (t, u)))
   3.150 +                  | _ => raise Fail "expected Var") args u)
   3.151 +    end
   3.152 +  | extract_lambda_def _ = raise Fail "malformed lifted lambda"
   3.153  
   3.154 -fun translate_formulas ctxt format prem_kind type_enc trans_lambdas preproc
   3.155 +fun translate_formulas ctxt format prem_kind type_enc lambda_trans presimp
   3.156                         hyp_ts concl_t facts =
   3.157    let
   3.158      val thy = Proof_Context.theory_of ctxt
   3.159 +    val trans_lambdas =
   3.160 +      if lambda_trans = no_lambdasN then
   3.161 +        rpair []
   3.162 +      else if lambda_trans = concealedN then
   3.163 +        lift_lambdas ctxt type_enc ##> K []
   3.164 +      else if lambda_trans = liftingN then
   3.165 +        lift_lambdas ctxt type_enc
   3.166 +      else if lambda_trans = combinatorsN then
   3.167 +        map (introduce_combinators ctxt) #> rpair []
   3.168 +      else if lambda_trans = hybridN then
   3.169 +        lift_lambdas ctxt type_enc
   3.170 +        ##> maps (fn t => [t, introduce_combinators ctxt
   3.171 +                                  (intentionalize_def t)])
   3.172 +      else if lambda_trans = lambdasN then
   3.173 +        map (Envir.eta_contract) #> rpair []
   3.174 +      else
   3.175 +        error ("Unknown lambda translation method: " ^
   3.176 +               quote lambda_trans ^ ".")
   3.177      val presimp_consts = Meson.presimplified_consts ctxt
   3.178      val fact_ts = facts |> map snd
   3.179      (* Remove existing facts from the conjecture, as this can dramatically
   3.180 @@ -1685,13 +1712,15 @@
   3.181        |> map (apsnd freeze_term)
   3.182        |> map2 (pair o rpair Local o string_of_int) (0 upto length hyp_ts)
   3.183      val ((conjs, facts), lambda_facts) =
   3.184 -      if preproc then
   3.185 -        conjs @ facts
   3.186 -        |> map (apsnd (uncurry (presimp_prop ctxt presimp_consts)))
   3.187 -        |> preprocess_abstractions_in_terms trans_lambdas
   3.188 -        |>> chop (length conjs)
   3.189 -      else
   3.190 -        ((conjs, facts), [])
   3.191 +      (conjs, facts)
   3.192 +      |> presimp
   3.193 +         ? pairself (map (apsnd (uncurry (presimp_prop ctxt presimp_consts))))
   3.194 +      |> (if lambda_trans = no_lambdasN then
   3.195 +            rpair []
   3.196 +          else
   3.197 +            op @
   3.198 +            #> preprocess_abstractions_in_terms trans_lambdas
   3.199 +            #>> chop (length conjs))
   3.200      val conjs = conjs |> make_conjecture ctxt format type_enc
   3.201      val (fact_names, facts) =
   3.202        facts
   3.203 @@ -2115,7 +2144,7 @@
   3.204      val (T, T_args) =
   3.205        if null T_args then
   3.206          (T, [])
   3.207 -      else case strip_prefix_and_unascii const_prefix s of
   3.208 +      else case unprefix_and_unascii const_prefix s of
   3.209          SOME s' =>
   3.210          let
   3.211            val s' = s' |> invert_const
   3.212 @@ -2323,27 +2352,9 @@
   3.213                 \encoding.")
   3.214        else
   3.215          lambda_trans
   3.216 -    val trans_lambdas =
   3.217 -      if lambda_trans = no_lambdasN then
   3.218 -        rpair []
   3.219 -      else if lambda_trans = concealedN then
   3.220 -        lift_lambdas ctxt type_enc ##> K []
   3.221 -      else if lambda_trans = liftingN then
   3.222 -        lift_lambdas ctxt type_enc
   3.223 -      else if lambda_trans = combinatorsN then
   3.224 -        map (introduce_combinators ctxt) #> rpair []
   3.225 -      else if lambda_trans = hybridN then
   3.226 -        lift_lambdas ctxt type_enc
   3.227 -        ##> maps (fn t => [t, introduce_combinators ctxt
   3.228 -                                  (intentionalize_def t)])
   3.229 -      else if lambda_trans = lambdasN then
   3.230 -        map (Envir.eta_contract) #> rpair []
   3.231 -      else
   3.232 -        error ("Unknown lambda translation method: " ^
   3.233 -               quote lambda_trans ^ ".")
   3.234      val (fact_names, classes, conjs, facts, class_rel_clauses, arity_clauses,
   3.235           lifted) =
   3.236 -      translate_formulas ctxt format prem_kind type_enc trans_lambdas preproc
   3.237 +      translate_formulas ctxt format prem_kind type_enc lambda_trans preproc
   3.238                           hyp_ts concl_t facts
   3.239      val sym_tab =
   3.240        sym_table_for_facts ctxt type_enc explicit_apply conjs facts
     4.1 --- a/src/HOL/Tools/ATP/atp_util.ML	Tue Nov 15 22:13:39 2011 +0100
     4.2 +++ b/src/HOL/Tools/ATP/atp_util.ML	Tue Nov 15 22:13:39 2011 +0100
     4.3 @@ -268,7 +268,8 @@
     4.4  
     4.5  fun close_form t =
     4.6    fold (fn ((x, i), T) => fn t' =>
     4.7 -           HOLogic.all_const T $ Abs (x, T, abstract_over (Var ((x, i), T), t')))
     4.8 +           HOLogic.all_const T
     4.9 +           $ Abs (x, T, abstract_over (Var ((x, i), T), t')))
    4.10         (Term.add_vars t []) t
    4.11  
    4.12  fun monomorphic_term subst =
     5.1 --- a/src/HOL/Tools/Meson/meson_clausify.ML	Tue Nov 15 22:13:39 2011 +0100
     5.2 +++ b/src/HOL/Tools/Meson/meson_clausify.ML	Tue Nov 15 22:13:39 2011 +0100
     5.3 @@ -10,6 +10,7 @@
     5.4    val new_skolem_var_prefix : string
     5.5    val new_nonskolem_var_prefix : string
     5.6    val is_zapped_var_name : string -> bool
     5.7 +  val is_quasi_lambda_free : term -> bool
     5.8    val introduce_combinators_in_cterm : cterm -> thm
     5.9    val introduce_combinators_in_theorem : thm -> thm
    5.10    val cluster_of_zapped_var_name : string -> (int * (int * int)) * bool
    5.11 @@ -174,7 +175,7 @@
    5.12             (warning ("Error in the combinator translation of " ^
    5.13                       Display.string_of_thm_without_context th ^
    5.14                       "\nException message: " ^ msg ^ ".");
    5.15 -            (* A type variable of sort "{}" will make abstraction fail. *)
    5.16 +            (* A type variable of sort "{}" will make "abstraction" fail. *)
    5.17              TrueI)
    5.18  
    5.19  (*cterms are used throughout for efficiency*)
     6.1 --- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Tue Nov 15 22:13:39 2011 +0100
     6.2 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Tue Nov 15 22:13:39 2011 +0100
     6.3 @@ -57,8 +57,7 @@
     6.4      lits |> map (atp_literal_from_metis type_enc) |> mk_aconns AOr
     6.5  
     6.6  fun polish_hol_terms ctxt (lifted, old_skolems) =
     6.7 -  map (reveal_lambda_lifted lifted
     6.8 -       #> reveal_old_skolem_terms old_skolems)
     6.9 +  map (reveal_lambda_lifted lifted #> reveal_old_skolem_terms old_skolems)
    6.10    #> Syntax.check_terms (Proof_Context.set_mode Proof_Context.mode_pattern ctxt)
    6.11  
    6.12  fun hol_clause_from_metis ctxt type_enc sym_tab concealed =
    6.13 @@ -146,10 +145,10 @@
    6.14                  NONE)
    6.15        fun remove_typeinst (a, t) =
    6.16          let val a = Metis_Name.toString a in
    6.17 -          case strip_prefix_and_unascii schematic_var_prefix a of
    6.18 +          case unprefix_and_unascii schematic_var_prefix a of
    6.19              SOME b => SOME (b, t)
    6.20            | NONE =>
    6.21 -            case strip_prefix_and_unascii tvar_prefix a of
    6.22 +            case unprefix_and_unascii tvar_prefix a of
    6.23                SOME _ => NONE (* type instantiations are forbidden *)
    6.24              | NONE => SOME (a, t) (* internal Metis var? *)
    6.25          end
    6.26 @@ -337,7 +336,7 @@
    6.27          | path_finder tm (p :: ps) (t as Metis_Term.Fn (s, ts)) =
    6.28            let
    6.29              val s = s |> Metis_Name.toString
    6.30 -                      |> perhaps (try (strip_prefix_and_unascii const_prefix
    6.31 +                      |> perhaps (try (unprefix_and_unascii const_prefix
    6.32                                         #> the #> unmangled_const_name))
    6.33            in
    6.34              if s = metis_predicator orelse s = predicator_name orelse
     7.1 --- a/src/HOL/Tools/Metis/metis_tactic.ML	Tue Nov 15 22:13:39 2011 +0100
     7.2 +++ b/src/HOL/Tools/Metis/metis_tactic.ML	Tue Nov 15 22:13:39 2011 +0100
     7.3 @@ -86,10 +86,34 @@
     7.4      | Const (@{const_name disj}, _) $ t1 $ t2 =>
     7.5        (if can HOLogic.dest_not t1 then t2 else t1)
     7.6        |> HOLogic.mk_Trueprop |> cterm_of thy |> Thm.trivial
     7.7 -    | _ => raise Fail "unexpected tags sym clause"
     7.8 +    | _ => raise Fail "expected reflexive or trivial clause"
     7.9    end
    7.10    |> Meson.make_meta_clause
    7.11  
    7.12 +fun lambda_lifted_from_metis ctxt type_enc sym_tab concealed mth =
    7.13 +  let
    7.14 +    val thy = Proof_Context.theory_of ctxt
    7.15 +    val tac = rewrite_goals_tac @{thms lambda_def_raw} THEN rtac refl 1
    7.16 +    val t = hol_clause_from_metis ctxt type_enc sym_tab concealed mth
    7.17 +    val ct = cterm_of thy (HOLogic.mk_Trueprop t)
    7.18 +  in Goal.prove_internal [] ct (K tac) |> Meson.make_meta_clause end
    7.19 +
    7.20 +fun introduce_lambda_wrappers_in_theorem ctxt th =
    7.21 +  if Meson_Clausify.is_quasi_lambda_free (prop_of th) then
    7.22 +    th
    7.23 +  else
    7.24 +    let
    7.25 +      fun conv wrap ctxt ct =
    7.26 +        if Meson_Clausify.is_quasi_lambda_free (term_of ct) then
    7.27 +          Thm.reflexive ct
    7.28 +        else case term_of ct of
    7.29 +          Abs _ =>
    7.30 +          Conv.abs_conv (conv false o snd) ctxt ct
    7.31 +          |> wrap ? (fn th => th RS @{thm Metis.eq_lambdaI})
    7.32 +        | _ => Conv.comb_conv (conv true ctxt) ct
    7.33 +      val eqth = conv true ctxt (cprop_of th)
    7.34 +    in Thm.equal_elim eqth th end
    7.35 +
    7.36  val clause_params =
    7.37    {ordering = Metis_KnuthBendixOrder.default,
    7.38     orderLiterals = Metis_Clause.UnsignedLiteralOrder,
    7.39 @@ -126,7 +150,11 @@
    7.40          prepare_metis_problem ctxt type_enc lambda_trans cls ths
    7.41        fun get_isa_thm mth Isa_Reflexive_or_Trivial =
    7.42            reflexive_or_trivial_from_metis ctxt type_enc sym_tab concealed mth
    7.43 -        | get_isa_thm _ (Isa_Raw ith) = ith
    7.44 +        | get_isa_thm mth Isa_Lambda_Lifted =
    7.45 +          lambda_lifted_from_metis ctxt type_enc sym_tab concealed mth
    7.46 +        | get_isa_thm _ (Isa_Raw ith) =
    7.47 +          ith |> lambda_trans = liftingN
    7.48 +                 ? introduce_lambda_wrappers_in_theorem ctxt
    7.49        val axioms = axioms |> map (fn (mth, ith) => (mth, get_isa_thm mth ith))
    7.50        val _ = trace_msg ctxt (fn () => "THEOREM CLAUSES")
    7.51        val _ = app (fn (_, th) => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) axioms
     8.1 --- a/src/HOL/Tools/Metis/metis_translate.ML	Tue Nov 15 22:13:39 2011 +0100
     8.2 +++ b/src/HOL/Tools/Metis/metis_translate.ML	Tue Nov 15 22:13:39 2011 +0100
     8.3 @@ -13,6 +13,7 @@
     8.4  
     8.5    datatype isa_thm =
     8.6      Isa_Reflexive_or_Trivial |
     8.7 +    Isa_Lambda_Lifted |
     8.8      Isa_Raw of thm
     8.9  
    8.10    val metis_equal : string
    8.11 @@ -114,10 +115,12 @@
    8.12                 | t => t)
    8.13  
    8.14  fun reveal_lambda_lifted lambdas =
    8.15 -  map_aterms (fn t as Free (s, _) =>
    8.16 +  map_aterms (fn t as Const (s, _) =>
    8.17                   if String.isPrefix lambda_lifted_prefix s then
    8.18                     case AList.lookup (op =) lambdas s of
    8.19 -                     SOME t => t |> map_types (map_type_tvar (K dummyT))
    8.20 +                     SOME t =>
    8.21 +                     Const (@{const_name Metis.lambda}, dummyT)
    8.22 +                     $ map_types (map_type_tvar (K dummyT)) t
    8.23                     | NONE => t
    8.24                   else
    8.25                     t
    8.26 @@ -130,6 +133,7 @@
    8.27  
    8.28  datatype isa_thm =
    8.29    Isa_Reflexive_or_Trivial |
    8.30 +  Isa_Lambda_Lifted |
    8.31    Isa_Raw of thm
    8.32  
    8.33  val proxy_defs = map (fst o snd o snd) proxy_table
    8.34 @@ -183,9 +187,17 @@
    8.35          | _ => raise Fail ("malformed helper identifier " ^ quote ident)
    8.36        else case try (unprefix fact_prefix) ident of
    8.37          SOME s =>
    8.38 -        let
    8.39 -          val j = s |> space_explode "_" |> List.last |> Int.fromString |> the
    8.40 -        in Meson.make_meta_clause (snd (nth clauses j)) |> Isa_Raw |> some end
    8.41 +        let val s = s |> space_explode "_" |> tl |> space_implode "_"
    8.42 +          in
    8.43 +          case Int.fromString s of
    8.44 +            SOME j =>
    8.45 +            Meson.make_meta_clause (snd (nth clauses j)) |> Isa_Raw |> some
    8.46 +          | NONE =>
    8.47 +            if String.isPrefix lambda_fact_prefix (unascii_of s) then
    8.48 +              Isa_Lambda_Lifted |> some
    8.49 +            else
    8.50 +              raise Fail ("malformed fact identifier " ^ quote ident)
    8.51 +        end
    8.52        | NONE => TrueI |> Isa_Raw |> some
    8.53      end
    8.54    | metis_axiom_from_atp _ _ _ = raise Fail "not CNF -- expected formula"
    8.55 @@ -221,12 +233,11 @@
    8.56        tracing ("PROPS:\n" ^
    8.57                 cat_lines (map (Syntax.string_of_term ctxt o snd) props))
    8.58      *)
    8.59 -    val (lambda_trans, preproc) =
    8.60 -      if lambda_trans = combinatorsN then (no_lambdasN, false)
    8.61 -      else (lambda_trans, true)
    8.62 +    val lambda_trans =
    8.63 +      if lambda_trans = combinatorsN then no_lambdasN else lambda_trans
    8.64      val (atp_problem, _, _, _, _, _, lifted, sym_tab) =
    8.65        prepare_atp_problem ctxt CNF Hypothesis Axiom type_enc false lambda_trans
    8.66 -                          false preproc [] @{prop False} props
    8.67 +                          false false [] @{prop False} props
    8.68      (*
    8.69      val _ = tracing ("ATP PROBLEM: " ^
    8.70                       cat_lines (lines_for_atp_problem CNF atp_problem))
     9.1 --- a/src/HOL/Tools/cnf_funcs.ML	Tue Nov 15 22:13:39 2011 +0100
     9.2 +++ b/src/HOL/Tools/cnf_funcs.ML	Tue Nov 15 22:13:39 2011 +0100
     9.3 @@ -261,8 +261,7 @@
     9.4      val thy = Proof_Context.theory_of ctxt
     9.5      fun conv ctxt ct =
     9.6        case term_of ct of
     9.7 -        (t1 as Const _) $ (t2 as Abs _) =>
     9.8 -        Conv.comb_conv (conv ctxt) ct
     9.9 +        Const _ $ Abs _ => Conv.comb_conv (conv ctxt) ct
    9.10        | Abs _ => Conv.abs_conv (conv o snd) ctxt ct
    9.11        | Const _ => Conv.all_conv ct
    9.12        | t => make t RS eq_reflection