--- 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
--- 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
--- 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;
--- 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
--- 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