# HG changeset patch # User blanchet # Date 1405008501 -7200 # Node ID 147e3f1e04598a05dc6cd9e62d9e51b1915f4c96 # Parent 10e7aabe17620ed365ab084fe93d52a412bd8532 lambda-lifting for Z3 Isar proofs diff -r 10e7aabe1762 -r 147e3f1e0459 src/HOL/Tools/ATP/atp_problem_generate.ML --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Thu Jul 10 17:01:23 2014 +0200 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Thu Jul 10 18:08:21 2014 +0200 @@ -1804,15 +1804,6 @@ fun type_ctrs_of_terms thy ts = Symtab.keys (fold (add_type_ctrs_in_term thy) ts Symtab.empty) -fun extract_lambda_def (Const (@{const_name HOL.eq}, _) $ t $ u) = - let val (head, args) = strip_comb t in - (head |> dest_Const |> fst, - fold_rev (fn t as Var ((s, _), T) => - (fn u => Abs (s, T, abstract_over (t, u))) - | _ => raise Fail "expected \"Var\"") args u) - end - | extract_lambda_def _ = raise Fail "malformed lifted lambda" - fun trans_lams_of_string ctxt type_enc lam_trans = if lam_trans = no_lamsN then rpair [] @@ -1865,8 +1856,7 @@ | s_not_prop (@{const Pure.imp} $ t $ @{prop False}) = t | s_not_prop t = @{const Pure.imp} $ t $ @{prop False} -fun translate_formulas ctxt prem_role format type_enc lam_trans presimp hyp_ts - concl_t facts = +fun translate_formulas ctxt prem_role format type_enc lam_trans presimp hyp_ts concl_t facts = let val thy = Proof_Context.theory_of ctxt val trans_lams = trans_lams_of_string ctxt type_enc lam_trans @@ -1894,7 +1884,7 @@ val facts = facts |> map_filter (fn (name, (_, t)) => make_fact ctxt format type_enc true (name, t)) |> pull_and_reorder_definitions - val lifted = lam_facts |> map (extract_lambda_def o snd o snd) + val lifted = lam_facts |> map (extract_lambda_def dest_Const o snd o snd) val lam_facts = lam_facts |> map_filter (make_fact ctxt format type_enc true o apsnd snd) val all_ts = concl_t :: hyp_ts @ fact_ts val subs = tfree_classes_of_terms all_ts diff -r 10e7aabe1762 -r 147e3f1e0459 src/HOL/Tools/ATP/atp_util.ML --- a/src/HOL/Tools/ATP/atp_util.ML Thu Jul 10 17:01:23 2014 +0200 +++ b/src/HOL/Tools/ATP/atp_util.ML Thu Jul 10 18:08:21 2014 +0200 @@ -49,6 +49,7 @@ val transform_elim_prop : term -> term val specialize_type : theory -> (string * typ) -> term -> term val strip_subgoal : thm -> int -> Proof.context -> (string * typ) list * term list * term + val extract_lambda_def : (term -> string * typ) -> term -> string * term val short_thm_name : Proof.context -> thm -> string end; @@ -425,6 +426,15 @@ val concl_t = t |> Logic.strip_assums_concl |> curry subst_bounds frees in (rev params, hyp_ts, concl_t) end +fun extract_lambda_def dest_head (Const (@{const_name HOL.eq}, _) $ t $ u) = + let val (head, args) = strip_comb t in + (head |> dest_head |> fst, + fold_rev (fn t as Var ((s, _), T) => + (fn u => Abs (s, T, abstract_over (t, u))) + | _ => raise Fail "expected \"Var\"") args u) + end + | extract_lambda_def _ _ = raise Fail "malformed lifted lambda" + fun short_thm_name ctxt th = let val long = Thm.get_name_hint th diff -r 10e7aabe1762 -r 147e3f1e0459 src/HOL/Tools/SMT2/smt2_translate.ML --- a/src/HOL/Tools/SMT2/smt2_translate.ML Thu Jul 10 17:01:23 2014 +0200 +++ b/src/HOL/Tools/SMT2/smt2_translate.ML Thu Jul 10 18:08:21 2014 +0200 @@ -29,6 +29,7 @@ context: Proof.context, typs: typ Symtab.table, terms: term Symtab.table, + ll_defs: term list, rewrite_rules: thm list, assms: (int * thm) list } @@ -72,6 +73,7 @@ context: Proof.context, typs: typ Symtab.table, terms: term Symtab.table, + ll_defs: term list, rewrite_rules: thm list, assms: (int * thm) list } @@ -118,7 +120,7 @@ dtyps = dtyps, funcs = Termtab.fold (fn (_, (n, SOME ss)) => cons (n,ss) | _ => I) terms []} -fun replay_data_of ctxt rules assms (_, typs, terms) = +fun replay_data_of ctxt ll_defs rules assms (_, typs, terms) = let fun add_typ (T, (n, _)) = Symtab.update (n, T) val typs' = Typtab.fold add_typ typs Symtab.empty @@ -126,7 +128,8 @@ fun add_fun (t, (n, _)) = Symtab.update (n, t) val terms' = Termtab.fold add_fun terms Symtab.empty in - {context=ctxt, typs=typs', terms=terms', rewrite_rules=rules, assms=assms} + {context = ctxt, typs = typs', terms = terms', ll_defs = ll_defs, rewrite_rules = rules, + assms = assms} end @@ -499,15 +502,13 @@ |> (fn t => @{const trigger} $ t $ eq) | mk_trigger t = t - val (ctxt2, ts3) = + val (ctxt2, (ts3, ll_defs)) = ts2 |> eta_expand ctxt1 funcs |> rpair ctxt1 |-> Lambda_Lifting.lift_lambdas NONE is_binder - |-> (fn (ts', defs) => fn ctxt' => - ts' @ map mk_trigger defs - |> intro_explicit_application ctxt' funcs - |> pair ctxt') + |-> (fn (ts', ll_defs) => fn ctxt' => + (ctxt', (intro_explicit_application ctxt' funcs (map mk_trigger ll_defs @ ts'), ll_defs))) val ((rewrite_rules, builtin), ts4) = folify ctxt2 ts3 |>> apfst (cons fun_app_eq) @@ -515,7 +516,7 @@ (ts4, tr_context) |-> intermediate logic dtyps (builtin SMT2_Builtin.dest_builtin) ctxt2 |>> uncurry (serialize smt_options comments) - ||> replay_data_of ctxt2 rewrite_rules ithms + ||> replay_data_of ctxt2 ll_defs rewrite_rules ithms end end; diff -r 10e7aabe1762 -r 147e3f1e0459 src/HOL/Tools/SMT2/z3_new_isar.ML --- a/src/HOL/Tools/SMT2/z3_new_isar.ML Thu Jul 10 17:01:23 2014 +0200 +++ b/src/HOL/Tools/SMT2/z3_new_isar.ML Thu Jul 10 18:08:21 2014 +0200 @@ -6,7 +6,7 @@ signature Z3_NEW_ISAR = sig - val atp_proof_of_z3_proof: Proof.context -> thm list -> term list -> term -> + val atp_proof_of_z3_proof: Proof.context -> term list -> thm list -> term list -> term -> (string * term) list -> int list -> int -> (int * string) list -> Z3_New_Proof.z3_step list -> (term, string) ATP_Proof.atp_step list end; @@ -92,11 +92,25 @@ t0 $ HOLogic.list_all (qs, t1) $ HOLogic.list_all (qs, t2) | _ => t) -fun atp_proof_of_z3_proof ctxt rewrite_rules hyp_ts concl_t fact_helper_ts prem_ids conjecture_id - fact_helper_ids proof = +fun unlift_term ll_defs = + let + val lifted = map (ATP_Util.extract_lambda_def dest_Free o ATP_Util.hol_open_form I) ll_defs + + fun un_free (t as Free (s, _)) = + (case AList.lookup (op =) lifted s of + SOME t => un_term t + | NONE => t) + | un_free t = t + and un_term t = map_aterms un_free t + in un_term end + +fun atp_proof_of_z3_proof ctxt ll_defs rewrite_rules hyp_ts concl_t fact_helper_ts prem_ids + conjecture_id fact_helper_ids proof = let val thy = Proof_Context.theory_of ctxt + val unlift_term = unlift_term ll_defs + fun steps_of (Z3_New_Proof.Z3_Step {id, rule, prems, concl, ...}) = let val sid = string_of_int id @@ -106,6 +120,7 @@ |> Raw_Simplifier.rewrite_term thy rewrite_rules [] |> Object_Logic.atomize_term thy |> simplify_bool + |> not (null ll_defs) ? unlift_term |> unskolemize_names |> push_skolem_all_under_iff |> HOLogic.mk_Trueprop diff -r 10e7aabe1762 -r 147e3f1e0459 src/HOL/Tools/SMT2/z3_new_replay.ML --- a/src/HOL/Tools/SMT2/z3_new_replay.ML Thu Jul 10 17:01:23 2014 +0200 +++ b/src/HOL/Tools/SMT2/z3_new_replay.ML Thu Jul 10 18:08:21 2014 +0200 @@ -174,8 +174,8 @@ #> discharge_assms outer_ctxt (make_discharge_rules rules) fun parse_proof outer_ctxt - ({context = ctxt, typs, terms, rewrite_rules, assms} : SMT2_Translate.replay_data) xfacts prems - concl output = + ({context = ctxt, typs, terms, ll_defs, rewrite_rules, assms} : SMT2_Translate.replay_data) + xfacts prems concl output = let val (steps, ctxt2) = Z3_New_Proof.parse typs terms output ctxt val ((iidths, _), _) = add_asserted outer_ctxt rewrite_rules assms steps ctxt2 @@ -197,12 +197,12 @@ map (apsnd (ATP_Util.short_thm_name ctxt)) helper_ids @ map (apsnd (fst o fst)) fact_ids in {outcome = NONE, fact_ids = fact_ids, - atp_proof = fn () => Z3_New_Isar.atp_proof_of_z3_proof ctxt rewrite_rules prems concl + atp_proof = fn () => Z3_New_Isar.atp_proof_of_z3_proof ctxt ll_defs rewrite_rules prems concl fact_helper_ts prem_ids conjecture_id fact_helper_ids steps} end fun replay outer_ctxt - ({context=ctxt, typs, terms, rewrite_rules, assms} : SMT2_Translate.replay_data) output = + ({context = ctxt, typs, terms, rewrite_rules, assms, ...} : SMT2_Translate.replay_data) output = let val (steps, ctxt2) = Z3_New_Proof.parse typs terms output ctxt val ((_, rules), (ctxt3, assumed)) = add_asserted outer_ctxt rewrite_rules assms steps ctxt2