1.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu Jul 10 17:01:23 2014 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu Jul 10 18:08:21 2014 +0200
     1.3 @@ -1804,15 +1804,6 @@
     1.4  fun type_ctrs_of_terms thy ts =
     1.5    Symtab.keys (fold (add_type_ctrs_in_term thy) ts Symtab.empty)
     1.6  
     1.7 -fun extract_lambda_def (Const (@{const_name HOL.eq}, _) $ t $ u) =
     1.8 -    let val (head, args) = strip_comb t in
     1.9 -      (head |> dest_Const |> fst,
    1.10 -       fold_rev (fn t as Var ((s, _), T) =>
    1.11 -                    (fn u => Abs (s, T, abstract_over (t, u)))
    1.12 -                  | _ => raise Fail "expected \"Var\"") args u)
    1.13 -    end
    1.14 -  | extract_lambda_def _ = raise Fail "malformed lifted lambda"
    1.15 -
    1.16  fun trans_lams_of_string ctxt type_enc lam_trans =
    1.17    if lam_trans = no_lamsN then
    1.18      rpair []
    1.19 @@ -1865,8 +1856,7 @@
    1.20    | s_not_prop (@{const Pure.imp} $ t $ @{prop False}) = t
    1.21    | s_not_prop t = @{const Pure.imp} $ t $ @{prop False}
    1.22  
    1.23 -fun translate_formulas ctxt prem_role format type_enc lam_trans presimp hyp_ts
    1.24 -                       concl_t facts =
    1.25 +fun translate_formulas ctxt prem_role format type_enc lam_trans presimp hyp_ts concl_t facts =
    1.26    let
    1.27      val thy = Proof_Context.theory_of ctxt
    1.28      val trans_lams = trans_lams_of_string ctxt type_enc lam_trans
    1.29 @@ -1894,7 +1884,7 @@
    1.30      val facts =
    1.31        facts |> map_filter (fn (name, (_, t)) => make_fact ctxt format type_enc true (name, t))
    1.32              |> pull_and_reorder_definitions
    1.33 -    val lifted = lam_facts |> map (extract_lambda_def o snd o snd)
    1.34 +    val lifted = lam_facts |> map (extract_lambda_def dest_Const o snd o snd)
    1.35      val lam_facts = lam_facts |> map_filter (make_fact ctxt format type_enc true o apsnd snd)
    1.36      val all_ts = concl_t :: hyp_ts @ fact_ts
    1.37      val subs = tfree_classes_of_terms all_ts

     2.1 --- a/src/HOL/Tools/ATP/atp_util.ML	Thu Jul 10 17:01:23 2014 +0200
     2.2 +++ b/src/HOL/Tools/ATP/atp_util.ML	Thu Jul 10 18:08:21 2014 +0200
     2.3 @@ -49,6 +49,7 @@
     2.4    val transform_elim_prop : term -> term
     2.5    val specialize_type : theory -> (string * typ) -> term -> term
     2.6    val strip_subgoal : thm -> int -> Proof.context -> (string * typ) list * term list * term
     2.7 +  val extract_lambda_def : (term -> string * typ) -> term -> string * term
     2.8    val short_thm_name : Proof.context -> thm -> string
     2.9  end;
    2.10  
    2.11 @@ -425,6 +426,15 @@
    2.12      val concl_t = t |> Logic.strip_assums_concl |> curry subst_bounds frees
    2.13    in (rev params, hyp_ts, concl_t) end
    2.14  
    2.15 +fun extract_lambda_def dest_head (Const (@{const_name HOL.eq}, _) $ t $ u) =
    2.16 +    let val (head, args) = strip_comb t in
    2.17 +      (head |> dest_head |> fst,
    2.18 +       fold_rev (fn t as Var ((s, _), T) =>
    2.19 +                    (fn u => Abs (s, T, abstract_over (t, u)))
    2.20 +                  | _ => raise Fail "expected \"Var\"") args u)
    2.21 +    end
    2.22 +  | extract_lambda_def _ _ = raise Fail "malformed lifted lambda"
    2.23 +
    2.24  fun short_thm_name ctxt th =
    2.25    let
    2.26      val long = Thm.get_name_hint th

     3.1 --- a/src/HOL/Tools/SMT2/smt2_translate.ML	Thu Jul 10 17:01:23 2014 +0200
     3.2 +++ b/src/HOL/Tools/SMT2/smt2_translate.ML	Thu Jul 10 18:08:21 2014 +0200
     3.3 @@ -29,6 +29,7 @@
     3.4      context: Proof.context,
     3.5      typs: typ Symtab.table,
     3.6      terms: term Symtab.table,
     3.7 +    ll_defs: term list,
     3.8      rewrite_rules: thm list,
     3.9      assms: (int * thm) list }
    3.10  
    3.11 @@ -72,6 +73,7 @@
    3.12    context: Proof.context,
    3.13    typs: typ Symtab.table,
    3.14    terms: term Symtab.table,
    3.15 +  ll_defs: term list,
    3.16    rewrite_rules: thm list,
    3.17    assms: (int * thm) list }
    3.18  
    3.19 @@ -118,7 +120,7 @@
    3.20    dtyps = dtyps,
    3.21    funcs = Termtab.fold (fn (_, (n, SOME ss)) => cons (n,ss) | _ => I) terms []}
    3.22  
    3.23 -fun replay_data_of ctxt rules assms (_, typs, terms) =
    3.24 +fun replay_data_of ctxt ll_defs rules assms (_, typs, terms) =
    3.25    let
    3.26      fun add_typ (T, (n, _)) = Symtab.update (n, T)
    3.27      val typs' = Typtab.fold add_typ typs Symtab.empty
    3.28 @@ -126,7 +128,8 @@
    3.29      fun add_fun (t, (n, _)) = Symtab.update (n, t)
    3.30      val terms' = Termtab.fold add_fun terms Symtab.empty
    3.31    in
    3.32 -    {context=ctxt, typs=typs', terms=terms', rewrite_rules=rules, assms=assms}
    3.33 +    {context = ctxt, typs = typs', terms = terms', ll_defs = ll_defs, rewrite_rules = rules,
    3.34 +     assms = assms}
    3.35    end
    3.36  
    3.37  
    3.38 @@ -499,15 +502,13 @@
    3.39            |> (fn t => @{const trigger} $ t $ eq)
    3.40        | mk_trigger t = t
    3.41  
    3.42 -    val (ctxt2, ts3) =
    3.43 +    val (ctxt2, (ts3, ll_defs)) =
    3.44        ts2
    3.45        |> eta_expand ctxt1 funcs
    3.46        |> rpair ctxt1
    3.47        |-> Lambda_Lifting.lift_lambdas NONE is_binder
    3.48 -      |-> (fn (ts', defs) => fn ctxt' =>
    3.49 -          ts' @ map mk_trigger defs
    3.50 -          |> intro_explicit_application ctxt' funcs
    3.51 -          |> pair ctxt')
    3.52 +      |-> (fn (ts', ll_defs) => fn ctxt' =>
    3.53 +          (ctxt', (intro_explicit_application ctxt' funcs (map mk_trigger ll_defs @ ts'), ll_defs)))
    3.54  
    3.55      val ((rewrite_rules, builtin), ts4) = folify ctxt2 ts3
    3.56        |>> apfst (cons fun_app_eq)
    3.57 @@ -515,7 +516,7 @@
    3.58      (ts4, tr_context)
    3.59      |-> intermediate logic dtyps (builtin SMT2_Builtin.dest_builtin) ctxt2
    3.60      |>> uncurry (serialize smt_options comments)
    3.61 -    ||> replay_data_of ctxt2 rewrite_rules ithms
    3.62 +    ||> replay_data_of ctxt2 ll_defs rewrite_rules ithms
    3.63    end
    3.64  
    3.65  end;

     4.1 --- a/src/HOL/Tools/SMT2/z3_new_isar.ML	Thu Jul 10 17:01:23 2014 +0200
     4.2 +++ b/src/HOL/Tools/SMT2/z3_new_isar.ML	Thu Jul 10 18:08:21 2014 +0200
     4.3 @@ -6,7 +6,7 @@
     4.4  
     4.5  signature Z3_NEW_ISAR =
     4.6  sig
     4.7 -  val atp_proof_of_z3_proof: Proof.context -> thm list -> term list -> term ->
     4.8 +  val atp_proof_of_z3_proof: Proof.context -> term list -> thm list -> term list -> term ->
     4.9      (string * term) list -> int list -> int -> (int * string) list -> Z3_New_Proof.z3_step list ->
    4.10      (term, string) ATP_Proof.atp_step list
    4.11  end;
    4.12 @@ -92,11 +92,25 @@
    4.13      t0 $ HOLogic.list_all (qs, t1) $ HOLogic.list_all (qs, t2)
    4.14    | _ => t)
    4.15  
    4.16 -fun atp_proof_of_z3_proof ctxt rewrite_rules hyp_ts concl_t fact_helper_ts prem_ids conjecture_id
    4.17 -    fact_helper_ids proof =
    4.18 +fun unlift_term ll_defs =
    4.19 +  let
    4.20 +    val lifted = map (ATP_Util.extract_lambda_def dest_Free o ATP_Util.hol_open_form I) ll_defs
    4.21 +
    4.22 +    fun un_free (t as Free (s, _)) =
    4.23 +       (case AList.lookup (op =) lifted s of
    4.24 +         SOME t => un_term t
    4.25 +       | NONE => t)
    4.26 +     | un_free t = t
    4.27 +    and un_term t = map_aterms un_free t
    4.28 +  in un_term end
    4.29 +
    4.30 +fun atp_proof_of_z3_proof ctxt ll_defs rewrite_rules hyp_ts concl_t fact_helper_ts prem_ids
    4.31 +    conjecture_id fact_helper_ids proof =
    4.32    let
    4.33      val thy = Proof_Context.theory_of ctxt
    4.34  
    4.35 +    val unlift_term = unlift_term ll_defs
    4.36 +
    4.37      fun steps_of (Z3_New_Proof.Z3_Step {id, rule, prems, concl, ...}) =
    4.38        let
    4.39          val sid = string_of_int id
    4.40 @@ -106,6 +120,7 @@
    4.41            |> Raw_Simplifier.rewrite_term thy rewrite_rules []
    4.42            |> Object_Logic.atomize_term thy
    4.43            |> simplify_bool
    4.44 +          |> not (null ll_defs) ? unlift_term
    4.45            |> unskolemize_names
    4.46            |> push_skolem_all_under_iff
    4.47            |> HOLogic.mk_Trueprop

     5.1 --- a/src/HOL/Tools/SMT2/z3_new_replay.ML	Thu Jul 10 17:01:23 2014 +0200
     5.2 +++ b/src/HOL/Tools/SMT2/z3_new_replay.ML	Thu Jul 10 18:08:21 2014 +0200
     5.3 @@ -174,8 +174,8 @@
     5.4    #> discharge_assms outer_ctxt (make_discharge_rules rules)
     5.5  
     5.6  fun parse_proof outer_ctxt
     5.7 -    ({context = ctxt, typs, terms, rewrite_rules, assms} : SMT2_Translate.replay_data) xfacts prems
     5.8 -    concl output =
     5.9 +    ({context = ctxt, typs, terms, ll_defs, rewrite_rules, assms} : SMT2_Translate.replay_data)
    5.10 +    xfacts prems concl output =
    5.11    let
    5.12      val (steps, ctxt2) = Z3_New_Proof.parse typs terms output ctxt
    5.13      val ((iidths, _), _) = add_asserted outer_ctxt rewrite_rules assms steps ctxt2
    5.14 @@ -197,12 +197,12 @@
    5.15        map (apsnd (ATP_Util.short_thm_name ctxt)) helper_ids @ map (apsnd (fst o fst)) fact_ids
    5.16    in
    5.17      {outcome = NONE, fact_ids = fact_ids,
    5.18 -     atp_proof = fn () => Z3_New_Isar.atp_proof_of_z3_proof ctxt rewrite_rules prems concl
    5.19 +     atp_proof = fn () => Z3_New_Isar.atp_proof_of_z3_proof ctxt ll_defs rewrite_rules prems concl
    5.20         fact_helper_ts prem_ids conjecture_id fact_helper_ids steps}
    5.21    end
    5.22  
    5.23  fun replay outer_ctxt
    5.24 -    ({context=ctxt, typs, terms, rewrite_rules, assms} : SMT2_Translate.replay_data) output =
    5.25 +    ({context = ctxt, typs, terms, rewrite_rules, assms, ...} : SMT2_Translate.replay_data) output =
    5.26    let
    5.27      val (steps, ctxt2) = Z3_New_Proof.parse typs terms output ctxt
    5.28      val ((_, rules), (ctxt3, assumed)) = add_asserted outer_ctxt rewrite_rules assms steps ctxt2