# HG changeset patch # User blanchet # Date 1394792146 -3600 # Node ID c106ac2ff76dd09e48e0d5d27ef9a2f313bfd5ca # Parent ae164dc4b2a1883c03f08100f404eb7183e9a4d9 undo rewrite rules (e.g. for 'fun_app') in Isar diff -r ae164dc4b2a1 -r c106ac2ff76d src/HOL/Sledgehammer.thy --- a/src/HOL/Sledgehammer.thy Fri Mar 14 11:05:45 2014 +0100 +++ b/src/HOL/Sledgehammer.thy Fri Mar 14 11:15:46 2014 +0100 @@ -34,13 +34,4 @@ ML_file "Tools/Sledgehammer/sledgehammer.ML" ML_file "Tools/Sledgehammer/sledgehammer_commands.ML" -definition plus1 where "plus1 x = x + (1::int)" - -ML {* print_depth 1000 *} - -lemma "map plus1 [0] = [1]" -sledgehammer [z3_new, isar_proofs = true, mepo, debug, dont_preplay, dont_minimize, dont_try0_isar] -(add: plus1_def) -oops - end diff -r ae164dc4b2a1 -r c106ac2ff76d src/HOL/Tools/SMT2/smt2_solver.ML --- a/src/HOL/Tools/SMT2/smt2_solver.ML Fri Mar 14 11:05:45 2014 +0100 +++ b/src/HOL/Tools/SMT2/smt2_solver.ML Fri Mar 14 11:15:46 2014 +0100 @@ -26,14 +26,13 @@ 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 option * thm) list -> - ((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 -> ('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} + {outcome: SMT2_Failure.failure option, rewrite_rules: thm list, 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 @@ -239,7 +238,7 @@ val wthms = map (apsnd (check_topsort ctxt)) wthms0 val (name, {command, finish, ...}) = name_and_info_of ctxt val (output, replay_data) = invoke name command (SMT2_Normalize.normalize ctxt wthms) ctxt - in finish ctxt replay_data output end + in (finish ctxt replay_data output, replay_data) end val default_max_relevant = #default_max_relevant oo get_info val can_filter = #can_filter o snd o name_and_info_of @@ -275,12 +274,11 @@ in wthms |> apply_solver ctxt - |> fst - |> (fn (iidths0, z3_proof) => - let - val iidths = if can_filter ctxt then iidths0 else map (apsnd (apfst (K no_id))) iwthms + |> (fn (((iidths0, z3_proof), _), {rewrite_rules, ...}) => + let val iidths = if can_filter ctxt then iidths0 else map (apsnd (apfst (K no_id))) iwthms in - {outcome = NONE, + {outcome = NONE, + rewrite_rules = rewrite_rules, conjecture_id = the_default no_id (Option.map fst (AList.lookup (op =) iidths conjecture_i)), helper_ids = map_filter (try (fn (~1, idth) => idth)) iidths, @@ -289,8 +287,8 @@ z3_proof = z3_proof} end) end - handle SMT2_Failure.SMT fail => {outcome = SOME fail, conjecture_id = no_id, helper_ids = [], - fact_ids = [], z3_proof = []} + handle SMT2_Failure.SMT fail => {outcome = SOME fail, rewrite_rules = [], conjecture_id = no_id, + helper_ids = [], fact_ids = [], z3_proof = []} (* SMT tactic *) @@ -307,6 +305,7 @@ fun solve ctxt wfacts = wfacts |> apply_solver ctxt + |> fst |>> apfst (trace_assumptions ctxt wfacts) |> snd diff -r ae164dc4b2a1 -r c106ac2ff76d src/HOL/Tools/SMT2/z3_new_isar.ML --- a/src/HOL/Tools/SMT2/z3_new_isar.ML Fri Mar 14 11:05:45 2014 +0100 +++ b/src/HOL/Tools/SMT2/z3_new_isar.ML Fri Mar 14 11:15:46 2014 +0100 @@ -8,8 +8,8 @@ sig type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step - val atp_proof_of_z3_proof: theory -> int -> (int * string) list -> Z3_New_Proof.z3_step list -> - (term, string) atp_step list + val atp_proof_of_z3_proof: theory -> thm list -> int -> (int * string) list -> + Z3_New_Proof.z3_step list -> (term, string) atp_step list end; structure Z3_New_Isar: Z3_NEW_ISAR = @@ -76,13 +76,14 @@ fun simplify_line (name, role, t, rule, deps) = (name, role, simplify_prop t, rule, deps) -fun atp_proof_of_z3_proof thy conjecture_id fact_ids proof = +fun atp_proof_of_z3_proof thy rewrite_rules conjecture_id fact_ids proof = let fun step_of (Z3_New_Proof.Z3_Step {id, rule, prems, concl, ...}) = let fun step_name_of id = (string_of_int id, the_list (AList.lookup (op =) fact_ids id)) val name as (_, ss) = step_name_of id + val role = (case rule of Z3_New_Proof.Asserted => @@ -94,9 +95,13 @@ | Z3_New_Proof.Skolemize => Lemma | Z3_New_Proof.Th_Lemma _ => Lemma | _ => Plain) + + val concl' = concl + |> Raw_Simplifier.rewrite_term thy rewrite_rules [] + |> Object_Logic.atomize_term thy + |> HOLogic.mk_Trueprop in - (name, role, HOLogic.mk_Trueprop (Object_Logic.atomize_term thy concl), - Z3_New_Proof.string_of_rule rule, map step_name_of prems) + (name, role, concl', Z3_New_Proof.string_of_rule rule, map step_name_of prems) end in proof diff -r ae164dc4b2a1 -r c106ac2ff76d src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Mar 14 11:05:45 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Mar 14 11:15:46 2014 +0100 @@ -89,9 +89,6 @@ fun add_lines_pass2 res [] = rev res | add_lines_pass2 res ((line as (name, role, t, rule, deps)) :: lines) = let -val line as (name, role, t, rule, deps) = (name, role, Term.map_aterms - (perhaps (try (fn Free (s, T) => Free (unsuffix "__" s, T)))) t - |> Term.map_abs_vars (perhaps (try (unsuffix "__"))), rule, deps) (*###*) val is_last_line = null lines fun looks_interesting () = diff -r ae164dc4b2a1 -r c106ac2ff76d src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML Fri Mar 14 11:05:45 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML Fri Mar 14 11:15:46 2014 +0100 @@ -161,7 +161,8 @@ reraise exn else {outcome = SOME (SMT2_Failure.Other_Failure (ML_Compiler.exn_message exn)), - conjecture_id = ~1, helper_ids = [], fact_ids = [], z3_proof = []} + rewrite_rules = [], 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 @@ -226,8 +227,9 @@ end val weighted_factss = map (apsnd weight_facts) factss - 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 {outcome, filter_result = {conjecture_id, rewrite_rules, 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 @@ -243,7 +245,8 @@ 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 atp_proof = Z3_New_Isar.atp_proof_of_z3_proof thy rewrite_rules 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)