# HG changeset patch # User blanchet # Date 1394718500 -3600 # Node ID fd6e132ee4fbd7b175160298f918f32c0717e59f # Parent 6689512f3710ab61d4324f545081d9fe778c0b38 correctly reconstruct helper facts (e.g. 'nat_int') in Isar proofs diff -r 6689512f3710 -r fd6e132ee4fb src/HOL/Tools/ATP/atp_proof_reconstruct.ML --- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Thu Mar 13 14:48:20 2014 +0100 +++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Thu Mar 13 14:48:20 2014 +0100 @@ -377,22 +377,12 @@ union (op =) (filter (fn (_, (_, status)) => status = Non_Rec_Def) facts) facts') accum fact_names -val isa_ext = Thm.get_name_hint @{thm ext} -val isa_short_ext = Long_Name.base_name isa_ext - -fun ext_name ctxt = - if Thm.eq_thm_prop (@{thm ext}, - singleton (Attrib.eval_thms ctxt) (Facts.named isa_short_ext, [])) then - isa_short_ext - else - isa_ext - val leo2_extcnf_equal_neg_rule = "extcnf_equal_neg" val leo2_unfold_def_rule = "unfold_def" fun add_fact ctxt fact_names ((_, ss), _, _, rule, deps) = (if rule = leo2_extcnf_equal_neg_rule then - insert (op =) (ext_name ctxt, (Global, General)) + insert (op =) (short_thm_name ctxt ext, (Global, General)) else if rule = leo2_unfold_def_rule then (* LEO 1.3.3 does not record definitions properly, leading to missing dependencies in the TSTP proof. Remove the next line once this is fixed. *) @@ -401,7 +391,7 @@ (fn [] => (* agsyHOL and Satallax don't include definitions in their unsatisfiable cores, so we assume the worst and include them all here. *) - [(ext_name ctxt, (Global, General))] |> add_non_rec_defs fact_names + [(short_thm_name ctxt ext, (Global, General))] |> add_non_rec_defs fact_names | facts => facts) else I) diff -r 6689512f3710 -r fd6e132ee4fb src/HOL/Tools/ATP/atp_util.ML --- a/src/HOL/Tools/ATP/atp_util.ML Thu Mar 13 14:48:20 2014 +0100 +++ b/src/HOL/Tools/ATP/atp_util.ML Thu Mar 13 14:48:20 2014 +0100 @@ -48,8 +48,8 @@ val is_legitimate_tptp_def : term -> bool 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 strip_subgoal : thm -> int -> Proof.context -> (string * typ) list * term list * term + val short_thm_name : Proof.context -> thm -> string end; structure ATP_Util : ATP_UTIL = @@ -425,4 +425,13 @@ val concl_t = t |> Logic.strip_assums_concl |> curry subst_bounds frees in (rev params, hyp_ts, concl_t) end +fun short_thm_name ctxt th = + let + val long = Thm.get_name_hint th + val short = Long_Name.base_name long + in + if Thm.eq_thm_prop (th, singleton (Attrib.eval_thms ctxt) (Facts.named short, [])) then short + else long + end + end; diff -r 6689512f3710 -r fd6e132ee4fb src/HOL/Tools/SMT2/smt2_normalize.ML --- a/src/HOL/Tools/SMT2/smt2_normalize.ML Thu Mar 13 14:48:20 2014 +0100 +++ b/src/HOL/Tools/SMT2/smt2_normalize.ML Thu Mar 13 14:48:20 2014 +0100 @@ -497,7 +497,7 @@ let val (is, thms) = split_list ithms val (thms', extra_thms) = f thms - in (is ~~ thms') @ map (pair ~1) extra_thms end + in (is ~~ thms') @ tag_list (length is) extra_thms end fun unfold2 ctxt ithms = ithms diff -r 6689512f3710 -r fd6e132ee4fb src/HOL/Tools/SMT2/smt2_solver.ML --- a/src/HOL/Tools/SMT2/smt2_solver.ML Thu Mar 13 14:48:20 2014 +0100 +++ b/src/HOL/Tools/SMT2/smt2_solver.ML Thu Mar 13 14:48:20 2014 +0100 @@ -20,20 +20,20 @@ cex_parser: (Proof.context -> SMT2_Translate.replay_data -> string list -> term list * term list) option, replay: (Proof.context -> SMT2_Translate.replay_data -> string list -> - ((int * int) list * Z3_New_Proof.z3_step list) * thm) option } + ((int * (int * thm)) list * Z3_New_Proof.z3_step list) * thm) option } (*registry*) val add_solver: solver_config -> theory -> theory val solver_name_of: Proof.context -> string val available_solvers_of: Proof.context -> string list val apply_solver: Proof.context -> (int * (int option * thm)) list -> - ((int * int) list * Z3_New_Proof.z3_step list) * thm + ((int * (int * thm)) list * Z3_New_Proof.z3_step list) * thm val default_max_relevant: Proof.context -> string -> int (*filter*) - val smt2_filter: Proof.context -> thm list -> thm -> ('a * (int option * thm)) list -> int -> - Time.time -> {outcome: SMT2_Failure.failure option, used_fact_infos: (int * ('a * thm)) list, - z3_proof: Z3_New_Proof.z3_step list} + val smt2_filter: Proof.context -> thm -> ('a * (int option * thm)) list -> int -> Time.time -> + {outcome: SMT2_Failure.failure option, conjecture_id: int, helper_ids: (int * thm) list, + fact_ids: (int * ('a * thm)) list, z3_proof: Z3_New_Proof.z3_step list} (*tactic*) val smt2_tac: Proof.context -> thm list -> int -> tactic @@ -152,7 +152,7 @@ cex_parser: (Proof.context -> SMT2_Translate.replay_data -> string list -> term list * term list) option, replay: (Proof.context -> SMT2_Translate.replay_data -> string list -> - ((int * int) list * Z3_New_Proof.z3_step list) * thm) option } + ((int * (int * thm)) list * Z3_New_Proof.z3_step list) * thm) option } (* registry *) @@ -162,7 +162,7 @@ default_max_relevant: int, supports_filter: bool, replay: Proof.context -> string list * SMT2_Translate.replay_data -> - ((int * int) list * Z3_New_Proof.z3_step list) * thm } + ((int * (int * thm)) list * Z3_New_Proof.z3_step list) * thm } structure Solvers = Generic_Data ( @@ -258,7 +258,7 @@ val cnot = Thm.cterm_of @{theory} @{const Not} -fun smt2_filter ctxt facts goal xwthms i time_limit = +fun smt2_filter ctxt goal xwfacts i time_limit = let val ctxt = ctxt @@ -273,53 +273,61 @@ SOME ct => ct | NONE => raise SMT2_Failure.SMT (SMT2_Failure.Other_Failure "goal is not a HOL term")) - val xthms = map (apsnd snd) xwthms + val iwconjecture = (~1, (NONE, Thm.assume cprop)) + val iwprems = map (pair ~2 o pair NONE) prems + val iwfacts = map_index I (map snd xwfacts) - val used_fact_infos_of = - if supports_filter ctxt then map_filter (try (apsnd (nth xthms))) - else K (map (pair ~1) xthms) + val n = length iwfacts + val xfacts = map (apsnd snd) xwfacts in - map snd xwthms - |> map_index I - |> append (map (pair ~1 o pair NONE) (Thm.assume cprop :: prems @ facts)) + iwconjecture :: iwprems @ iwfacts |> check_topsorts ctxt |> apply_solver ctxt |> fst - |> (fn (idis, z3_proof) => - {outcome = NONE, used_fact_infos = used_fact_infos_of idis, z3_proof = z3_proof}) + |> (fn (iidths0, z3_proof) => + let val iidths = if supports_filter ctxt then iidths0 else map (apsnd (apfst (K ~1))) iwfacts + in + {outcome = NONE, + conjecture_id = + the_default ~1 (Option.map fst (AList.lookup (op =) iidths (fst iwconjecture))), + helper_ids = map_filter (fn (i, (id, th)) => if i >= n then SOME (id, th) else NONE) iidths, + fact_ids = map_filter (fn (i, (id, _)) => try (apsnd (nth xfacts)) (id, i)) iidths, + z3_proof = z3_proof} + end) end - handle SMT2_Failure.SMT fail => {outcome = SOME fail, used_fact_infos = [], z3_proof = []} + handle SMT2_Failure.SMT fail => {outcome = SOME fail, conjecture_id = ~1, helper_ids = [], + fact_ids = [], z3_proof = []} (* SMT tactic *) local - fun trace_assumptions ctxt iwthms idis = + fun trace_assumptions ctxt iwfacts iidths = let - val wthms = - idis - |> map snd + val wfacts = + iidths + |> map fst |> filter (fn i => i >= 0) - |> map_filter (AList.lookup (op =) iwthms) + |> map_filter (AList.lookup (op =) iwfacts) in - if Config.get ctxt SMT2_Config.trace_used_facts andalso length wthms > 0 then + if Config.get ctxt SMT2_Config.trace_used_facts andalso length wfacts > 0 then tracing (Pretty.string_of (Pretty.big_list "SMT used facts:" - (map (Display.pretty_thm ctxt o snd) wthms))) + (map (Display.pretty_thm ctxt o snd) wfacts))) else () end - fun solve ctxt iwthms = - iwthms + fun solve ctxt iwfacts = + iwfacts |> check_topsorts ctxt |> apply_solver ctxt - |>> apfst (trace_assumptions ctxt iwthms) + |>> apfst (trace_assumptions ctxt iwfacts) |> snd fun str_of ctxt fail = SMT2_Failure.string_of_failure ctxt fail |> prefix ("Solver " ^ SMT2_Config.solver_of ctxt ^ ": ") - fun safe_solve ctxt iwthms = SOME (solve ctxt iwthms) + fun safe_solve ctxt iwfacts = SOME (solve ctxt iwfacts) handle SMT2_Failure.SMT (fail as SMT2_Failure.Counterexample _) => (SMT2_Config.verbose_msg ctxt (str_of ctxt) fail; NONE) diff -r 6689512f3710 -r fd6e132ee4fb src/HOL/Tools/SMT2/smt2_translate.ML --- a/src/HOL/Tools/SMT2/smt2_translate.ML Thu Mar 13 14:48:20 2014 +0100 +++ b/src/HOL/Tools/SMT2/smt2_translate.ML Thu Mar 13 14:48:20 2014 +0100 @@ -321,8 +321,7 @@ exception BAD_PATTERN of unit fun wrap_in_if pat t = - if pat then raise BAD_PATTERN () - else @{const If (bool)} $ t $ @{const True} $ @{const False} + if pat then raise BAD_PATTERN () else @{const If (bool)} $ t $ @{const True} $ @{const False} fun is_builtin_conn_or_pred ctxt c ts = is_some (SMT2_Builtin.dest_builtin_conn ctxt c ts) orelse @@ -338,8 +337,7 @@ (@{const True}, []) => t | (@{const False}, []) => t | (u as Const (@{const_name If}, _), [t1, t2, t3]) => - if pat then raise BAD_PATTERN () - else u $ in_form t1 $ in_term pat t2 $ in_term pat t3 + if pat then raise BAD_PATTERN () else u $ in_form t1 $ in_term pat t2 $ in_term pat t3 | (Const (c as (n, _)), ts) => if is_builtin_conn_or_pred ctxt c ts then wrap_in_if pat (in_form t) else if is_quant n then wrap_in_if pat (in_form t) @@ -357,11 +355,9 @@ | in_pat t = raise TERM ("bad pattern", [t]) and in_pats ps = - in_list @{typ "SMT2.pattern list"} - (SOME o in_list @{typ SMT2.pattern} (try in_pat)) ps + in_list @{typ "SMT2.pattern list"} (SOME o in_list @{typ SMT2.pattern} (try in_pat)) ps - and in_trigger ((c as @{const SMT2.trigger}) $ p $ t) = - c $ in_pats p $ in_weight t + and in_trigger ((c as @{const SMT2.trigger}) $ p $ t) = c $ in_pats p $ in_weight t | in_trigger t = in_weight t and in_form t = @@ -462,7 +458,7 @@ let val (Us, U) = SMT2_Util.dest_funT (length ts) T in fold_map transT Us ##>> transT U #-> (fn Up => - add_fun t (SOME Up) ##>> fold_map trans ts #>> SApp) + add_fun t (SOME Up) ##>> fold_map trans ts #>> SApp) end val (us, trx') = fold_map trans ts trx @@ -528,13 +524,12 @@ |> pair ctxt') val ((rewrite_rules, builtin), ts4) = folify ctxt2 ts3 - - val rewrite_rules' = fun_app_eq :: rewrite_rules + |>> apfst (cons fun_app_eq) in (ts4, tr_context) |-> intermediate header dtyps (builtin SMT2_Builtin.dest_builtin) ctxt2 |>> uncurry (serialize comments) - ||> replay_data_of ctxt2 rewrite_rules' ithms + ||> replay_data_of ctxt2 rewrite_rules ithms end end diff -r 6689512f3710 -r fd6e132ee4fb src/HOL/Tools/SMT2/z3_new_isar.ML --- a/src/HOL/Tools/SMT2/z3_new_isar.ML Thu Mar 13 14:48:20 2014 +0100 +++ b/src/HOL/Tools/SMT2/z3_new_isar.ML Thu Mar 13 14:48:20 2014 +0100 @@ -8,7 +8,7 @@ sig type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step - val atp_proof_of_z3_proof: theory -> Z3_New_Proof.z3_step list -> (int * string) list -> + val atp_proof_of_z3_proof: theory -> int -> (int * string) list -> Z3_New_Proof.z3_step list -> (term, string) atp_step list end; @@ -74,7 +74,7 @@ fun simplify_line (name, role, t, rule, deps) = (name, role, simplify_prop t, rule, deps) -fun atp_proof_of_z3_proof thy proof fact_ids = +fun atp_proof_of_z3_proof thy conjecture_id fact_ids proof = let fun step_of (Z3_New_Proof.Z3_Step {id, rule, prems, concl, ...}) = let @@ -84,7 +84,9 @@ val role = (case rule of Z3_New_Proof.Asserted => - if null ss then Negated_Conjecture (* FIXME: or hypothesis! *) else Axiom + if not (null ss) then Axiom + else if id = conjecture_id then Negated_Conjecture + else Hypothesis | Z3_New_Proof.Rewrite => Lemma | Z3_New_Proof.Rewrite_Star => Lemma | Z3_New_Proof.Skolemize => Lemma diff -r 6689512f3710 -r fd6e132ee4fb src/HOL/Tools/SMT2/z3_new_replay.ML --- a/src/HOL/Tools/SMT2/z3_new_replay.ML Thu Mar 13 14:48:20 2014 +0100 +++ b/src/HOL/Tools/SMT2/z3_new_replay.ML Thu Mar 13 14:48:20 2014 +0100 @@ -8,7 +8,7 @@ signature Z3_NEW_REPLAY = sig val replay: Proof.context -> SMT2_Translate.replay_data -> string list -> - ((int * int) list * Z3_New_Proof.z3_step list) * thm + ((int * (int * thm)) list * Z3_New_Proof.z3_step list) * thm end structure Z3_New_Replay: Z3_NEW_REPLAY = @@ -106,14 +106,14 @@ val (thm', ctxt') = yield_singleton Assumption.add_assumes ct ctxt in (thm' RS thm, ctxt') end - fun add1 id fixes thm1 ((i, th), exact) ((idis, thms), (ctxt, ptab)) = + fun add1 id fixes thm1 ((i, th), exact) ((iidths, thms), (ctxt, ptab)) = let val (thm, ctxt') = if exact then (Thm.implies_elim thm1 th, ctxt) else assume thm1 ctxt val thms' = if exact then thms else th :: thms - in (((id, i) :: idis, thms'), (ctxt', Inttab.update (id, (fixes, thm)) ptab)) end + in (((i, (id, th)) :: iidths, thms'), (ctxt', Inttab.update (id, (fixes, thm)) ptab)) end fun add (Z3_New_Proof.Z3_Step {id, rule, concl, fixes, ...}) - (cx as ((idis, thms), (ctxt, ptab))) = + (cx as ((iidths, thms), (ctxt, ptab))) = if Z3_New_Replay_Methods.is_assumption rule andalso rule <> Z3_New_Proof.Hypothesis then let val ct = SMT2_Util.certify ctxt concl @@ -123,7 +123,7 @@ (case lookup_assm assms_net (Thm.cprem_of thm2 1) of [] => let val (thm, ctxt') = assume thm1 ctxt - in ((idis, thms), (ctxt', Inttab.update (id, (fixes, thm)) ptab)) end + in ((iidths, thms), (ctxt', Inttab.update (id, (fixes, thm)) ptab)) end | ithms => fold (add1 id fixes thm1) ithms cx) end else @@ -176,10 +176,10 @@ ({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 ((idis, rules), (ctxt3, assumed)) = add_asserted outer_ctxt rewrite_rules assms steps ctxt2 + val ((iidths, rules), (ctxt3, assumed)) = add_asserted outer_ctxt rewrite_rules assms steps ctxt2 in if Config.get ctxt3 SMT2_Config.filter_only_facts then - ((idis, steps), TrueI) + ((iidths, steps), TrueI) else let val ctxt4 = put_simpset (Z3_New_Replay_Util.make_simpset ctxt3 []) ctxt3 diff -r 6689512f3710 -r fd6e132ee4fb src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML Thu Mar 13 14:48:20 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML Thu Mar 13 14:48:20 2014 +0100 @@ -154,14 +154,14 @@ val birth = Timer.checkRealTimer timer val _ = if debug then Output.urgent_message "Invoking SMT solver..." else () - val {outcome, used_fact_infos, z3_proof} = - SMT2_Solver.smt2_filter ctxt [] goal weighted_facts i slice_timeout + val filter_result as {outcome, ...} = + SMT2_Solver.smt2_filter ctxt goal weighted_facts i slice_timeout handle exn => if Exn.is_interrupt exn orelse debug then reraise exn else {outcome = SOME (SMT2_Failure.Other_Failure (ML_Compiler.exn_message exn)), - used_fact_infos = [], z3_proof = []} + conjecture_id = ~1, helper_ids = [], fact_ids = [], z3_proof = []} val death = Timer.checkRealTimer timer val outcome0 = if is_none outcome0 then SOME outcome else outcome0 @@ -206,9 +206,8 @@ do_slice timeout (slice + 1) outcome0 time_so_far weighted_factss end else - {outcome = if is_none outcome then NONE else the outcome0, - used_fact_infos = used_fact_infos, used_from = map (apsnd snd) weighted_facts, - z3_proof = z3_proof, run_time = time_so_far} + {outcome = if is_none outcome then NONE else the outcome0, filter_result = filter_result, + used_from = map (apsnd snd) weighted_facts, run_time = time_so_far} end in do_slice timeout 1 NONE Time.zeroTime @@ -227,9 +226,9 @@ end val weighted_factss = map (apsnd weight_facts) factss - val {outcome, used_fact_infos, used_from, z3_proof, run_time} = - smt2_filter_loop name params state goal subgoal weighted_factss - val used_named_facts = map snd used_fact_infos + val {outcome, filter_result = {conjecture_id, helper_ids, fact_ids, z3_proof, ...}, + used_from, run_time} = smt2_filter_loop name params state goal subgoal weighted_factss + val used_named_facts = map snd fact_ids val used_facts = map fst used_named_facts val outcome = Option.map failure_of_smt2_failure outcome @@ -241,8 +240,10 @@ SMT2_Method (bunch_of_proof_methods (smt_proofs <> SOME false) false liftingN)), fn preplay => let - val fact_ids = map (fn (id, ((name, _), _)) => (id, name)) used_fact_infos - val atp_proof = Z3_New_Isar.atp_proof_of_z3_proof thy z3_proof fact_ids + val fact_ids = + map (fn (id, th) => (id, short_thm_name ctxt th)) helper_ids @ + map (fn (id, ((name, _), _)) => (id, name)) fact_ids + val atp_proof = Z3_New_Isar.atp_proof_of_z3_proof thy conjecture_id fact_ids z3_proof val isar_params = K (verbose, (NONE, NONE), preplay_timeout, compress_isar, try0_isar, minimize <> SOME false, atp_proof, goal)