# HG changeset patch # User blanchet # Date 1400260440 -7200 # Node ID 82c83978fbd9c33fb96af97410c54ee97af281fa # Parent d20f19f54789414be3db14f5aec129a3a97cf84a correctly add extra facts to lemmas (cf. conjecture and hypotheses) in Z3 Isar proofs diff -r d20f19f54789 -r 82c83978fbd9 src/HOL/Tools/SMT2/z3_new_isar.ML --- a/src/HOL/Tools/SMT2/z3_new_isar.ML Fri May 16 19:13:50 2014 +0200 +++ b/src/HOL/Tools/SMT2/z3_new_isar.ML Fri May 16 19:14:00 2014 +0200 @@ -8,8 +8,9 @@ sig type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step - val atp_proof_of_z3_proof: Proof.context -> thm list -> term list -> term -> int list -> int -> - (int * string) list -> Z3_New_Proof.z3_step list -> (term, string) atp_step list + val atp_proof_of_z3_proof: Proof.context -> thm list -> term list -> term -> + (string * term) list -> int list -> int -> (int * string) list -> Z3_New_Proof.z3_step list -> + (term, string) atp_step list end; structure Z3_New_Isar: Z3_NEW_ISAR = @@ -83,15 +84,14 @@ Term.map_abs_vars (perhaps (try Name.dest_skolem)) #> Term.map_aterms (perhaps (try (fn Free (s, T) => Free (Name.dest_skolem s, T)))) -fun atp_proof_of_z3_proof ctxt rewrite_rules hyp_ts concl_t prem_ids conjecture_id fact_ids proof = +fun atp_proof_of_z3_proof ctxt rewrite_rules hyp_ts concl_t fact_ts prem_ids conjecture_id fact_ids + proof = let val thy = Proof_Context.theory_of ctxt fun steps_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 (sid, ss) = step_name_of id + val sid = string_of_int id val concl' = concl @@ -102,22 +102,26 @@ |> HOLogic.mk_Trueprop fun standard_step role = - (name, role, concl', Z3_New_Proof.string_of_rule rule, map step_name_of prems) + ((sid, []), role, concl', Z3_New_Proof.string_of_rule rule, + map (fn id => (string_of_int id, [])) prems) in (case rule of Z3_New_Proof.Asserted => let + val ss = the_list (AList.lookup (op =) fact_ids id) val name0 = (sid ^ "a", ss) + val (role0, concl0) = - if not (null ss) then - (Axiom, concl(*FIXME*)) - else if id = conjecture_id then - (Conjecture, concl_t) - else - (Hypothesis, - (case find_index (curry (op =) id) prem_ids of - ~1 => concl - | i => nth hyp_ts i)) + (case ss of + [s] => (Axiom, the (AList.lookup (op =) fact_ts s)) + | _ => + if id = conjecture_id then + (Conjecture, concl_t) + else + (Hypothesis, + (case find_index (curry (op =) id) prem_ids of + ~1 => concl + | i => nth hyp_ts i))) val normalize_prems = SMT2_Normalize.case_bool_entry :: SMT2_Normalize.special_quant_table @ @@ -128,12 +132,9 @@ else NONE) in - if null normalize_prems then - [(name, role0, concl0, Z3_New_Proof.string_of_rule rule, [])] - else - [(name0, role0, concl0, Z3_New_Proof.string_of_rule rule, []), - (name, Plain, concl', Z3_New_Proof.string_of_rule Z3_New_Proof.Rewrite, - name0 :: normalize_prems)] + [(name0, role0, concl0, Z3_New_Proof.string_of_rule rule, []), + ((sid, []), Plain, concl', Z3_New_Proof.string_of_rule Z3_New_Proof.Rewrite, + name0 :: normalize_prems)] end | Z3_New_Proof.Rewrite => [standard_step Lemma] | Z3_New_Proof.Rewrite_Star => [standard_step Lemma] diff -r d20f19f54789 -r 82c83978fbd9 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri May 16 19:13:50 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri May 16 19:14:00 2014 +0200 @@ -295,7 +295,7 @@ fun str_of_preplay_outcome outcome = if Lazy.is_finished outcome then string_of_play_outcome (Lazy.force outcome) else "?" fun str_of_meth l meth = - string_of_proof_method [] meth ^ " " ^ + string_of_proof_method ctxt [] meth ^ " " ^ str_of_preplay_outcome (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth) fun comment_of l = map (str_of_meth l) #> commas @@ -355,7 +355,7 @@ end) end - val one_line_proof = one_line_proof_text 0 one_line_params + val one_line_proof = one_line_proof_text ctxt 0 one_line_params val isar_proof = if debug then isar_proof_of () @@ -378,6 +378,6 @@ (isar_proofs = NONE andalso isar_proof_would_be_a_good_idea smt_proofs preplay) then isar_proof_text ctxt debug isar_proofs smt_proofs isar_params else - one_line_proof_text num_chained) one_line_params + one_line_proof_text ctxt num_chained) one_line_params end; diff -r d20f19f54789 -r 82c83978fbd9 src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Fri May 16 19:13:50 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Fri May 16 19:14:00 2014 +0200 @@ -208,15 +208,15 @@ val indent_size = 2 -fun string_of_isar_proof ctxt i n proof = +fun string_of_isar_proof ctxt0 i n proof = let (* Make sure only type constraints inserted by the type annotation code are printed. *) - val ctxt = - ctxt |> Config.put show_markup false - |> Config.put Printer.show_type_emphasis false - |> Config.put show_types false - |> Config.put show_sorts false - |> Config.put show_consts false + val ctxt = ctxt0 + |> Config.put show_markup false + |> Config.put Printer.show_type_emphasis false + |> Config.put show_types false + |> Config.put show_sorts false + |> Config.put show_consts false val register_fixes = map Free #> fold Variable.auto_fixes @@ -264,7 +264,7 @@ fun of_method ls ss meth = let val direct = is_direct_method meth in using_facts ls (if direct then [] else ss) ^ - "by " ^ string_of_proof_method (if direct then ss else []) meth + "by " ^ string_of_proof_method ctxt (if direct then ss else []) meth end fun of_free (s, T) = diff -r d20f19f54789 -r 82c83978fbd9 src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Fri May 16 19:13:50 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Fri May 16 19:14:00 2014 +0200 @@ -33,12 +33,12 @@ type one_line_params = (proof_method * play_outcome) * string * (string * stature) list * minimize_command * int * int - val string_of_proof_method : string list -> proof_method -> string + val string_of_proof_method : Proof.context -> string list -> proof_method -> string val tac_of_proof_method : Proof.context -> bool -> thm list * thm list -> proof_method -> int -> tactic val string_of_play_outcome : play_outcome -> string val play_outcome_ord : play_outcome * play_outcome -> order - val one_line_proof_text : int -> one_line_params -> string + val one_line_proof_text : Proof.context -> int -> one_line_params -> string end; structure Sledgehammer_Proof_Methods : SLEDGEHAMMER_PROOF_METHODS = @@ -74,7 +74,7 @@ fun maybe_paren s = s |> not (Symbol_Pos.is_identifier s) ? enclose "(" ")" -fun string_of_proof_method ss meth = +fun string_of_proof_method ctxt ss meth = let val meth_s = (case meth of @@ -86,7 +86,7 @@ | SATx_Method => "satx" | Blast_Method => "blast" | Simp_Method => if null ss then "simp" else "simp add:" - | Simp_Size_Method => "simp add: size_ne_size_imp_ne" + | Simp_Size_Method => "simp add: " ^ short_thm_name ctxt @{thm size_ne_size_imp_ne} | Auto_Method => "auto" | Fastforce_Method => "fastforce" | Force_Method => "force" @@ -141,8 +141,8 @@ "prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal 1 n (* FIXME *) -fun proof_method_command meth i n _(*used_chaineds*) _(*num_chained*) ss = - apply_on_subgoal i n ^ string_of_proof_method ss meth +fun proof_method_command ctxt meth i n _(*used_chaineds*) _(*num_chained*) ss = + apply_on_subgoal i n ^ string_of_proof_method ctxt ss meth fun try_command_line banner play command = let val s = string_of_play_outcome play in @@ -161,14 +161,14 @@ |> List.partition (fn (_, (sc, _)) => sc = Chained) |> pairself (sort_distinct (string_ord o pairself fst)) -fun one_line_proof_text num_chained +fun one_line_proof_text ctxt num_chained ((meth, play), banner, used_facts, minimize_command, subgoal, subgoal_count) = let val (chained, extra) = split_used_facts used_facts val try_line = map fst extra - |> proof_method_command meth subgoal subgoal_count (map fst chained) num_chained + |> proof_method_command ctxt meth subgoal subgoal_count (map fst chained) num_chained |> (if play = Play_Failed then enclose "One-line proof reconstruction failed: " "." else try_command_line banner play) in diff -r d20f19f54789 -r 82c83978fbd9 src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Fri May 16 19:13:50 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Fri May 16 19:14:00 2014 +0200 @@ -216,6 +216,8 @@ fun play_one_line_proof mode debug verbose timeout pairs state i preferred (meths as meth :: _) = let + val ctxt = Proof.context_of state + fun get_preferred meths = if member (op =) meths preferred then preferred else meth in if timeout = Time.zeroTime then @@ -230,7 +232,7 @@ let val _ = if verbose then - Output.urgent_message ("Trying \"" ^ string_of_proof_method [] meth ^ + Output.urgent_message ("Trying \"" ^ string_of_proof_method ctxt [] meth ^ "\" for " ^ string_of_time timeout ^ "...") else () diff -r d20f19f54789 -r 82c83978fbd9 src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Fri May 16 19:13:50 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Fri May 16 19:14:00 2014 +0200 @@ -61,21 +61,22 @@ else raise Fail ("unknown proof_method: " ^ quote name) val used_facts = facts |> map fst in - (case play_one_line_proof (if mode = Minimize then Normal else mode) debug verbose timeout facts - state subgoal meth [meth] of + (case play_one_line_proof (if mode = Minimize then Normal else mode) debug verbose timeout + facts state subgoal meth [meth] of play as (_, Played time) => {outcome = NONE, used_facts = used_facts, used_from = facts, run_time = time, preplay = Lazy.value play, message = fn play => let + val ctxt = Proof.context_of state val (_, override_params) = extract_proof_method params meth val one_line_params = (play, proof_banner mode name, used_facts, minimize_command override_params name, subgoal, subgoal_count) val num_chained = length (#facts (Proof.goal state)) in - one_line_proof_text num_chained one_line_params + one_line_proof_text ctxt num_chained one_line_params end, message_tail = ""} | play => diff -r d20f19f54789 -r 82c83978fbd9 src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Fri May 16 19:13:50 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Fri May 16 19:14:00 2014 +0200 @@ -243,7 +243,7 @@ subgoal_count) val num_chained = length (#facts (Proof.goal state)) in - one_line_proof_text num_chained one_line_params + one_line_proof_text ctxt num_chained one_line_params end, if verbose then "\nSMT solver real CPU time: " ^ string_of_time run_time ^ "." else "") | SOME failure => diff -r d20f19f54789 -r 82c83978fbd9 src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML Fri May 16 19:13:50 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML Fri May 16 19:14:00 2014 +0200 @@ -246,7 +246,8 @@ 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 ctxt rewrite_rules hyp_ts concl_t - prem_ids conjecture_id fact_ids z3_proof + (map (fn ((s, _), th) => (s, prop_of th)) used_named_facts) prem_ids 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)