correctly add extra facts to lemmas (cf. conjecture and hypotheses) in Z3 Isar proofs
authorblanchet
Fri May 16 19:14:00 2014 +0200 (2014-05-16)
changeset 5698582c83978fbd9
parent 56984 d20f19f54789
child 56986 43be5818a45c
correctly add extra facts to lemmas (cf. conjecture and hypotheses) in Z3 Isar proofs
src/HOL/Tools/SMT2/z3_new_isar.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML
src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML
src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML
src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML
src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML
     1.1 --- a/src/HOL/Tools/SMT2/z3_new_isar.ML	Fri May 16 19:13:50 2014 +0200
     1.2 +++ b/src/HOL/Tools/SMT2/z3_new_isar.ML	Fri May 16 19:14:00 2014 +0200
     1.3 @@ -8,8 +8,9 @@
     1.4  sig
     1.5    type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step
     1.6  
     1.7 -  val atp_proof_of_z3_proof: Proof.context -> thm list -> term list -> term -> int list -> int ->
     1.8 -    (int * string) list -> Z3_New_Proof.z3_step list -> (term, string) atp_step list
     1.9 +  val atp_proof_of_z3_proof: Proof.context -> thm list -> term list -> term ->
    1.10 +    (string * term) list -> int list -> int -> (int * string) list -> Z3_New_Proof.z3_step list ->
    1.11 +    (term, string) atp_step list
    1.12  end;
    1.13  
    1.14  structure Z3_New_Isar: Z3_NEW_ISAR =
    1.15 @@ -83,15 +84,14 @@
    1.16    Term.map_abs_vars (perhaps (try Name.dest_skolem))
    1.17    #> Term.map_aterms (perhaps (try (fn Free (s, T) => Free (Name.dest_skolem s, T))))
    1.18  
    1.19 -fun atp_proof_of_z3_proof ctxt rewrite_rules hyp_ts concl_t prem_ids conjecture_id fact_ids proof =
    1.20 +fun atp_proof_of_z3_proof ctxt rewrite_rules hyp_ts concl_t fact_ts prem_ids conjecture_id fact_ids
    1.21 +    proof =
    1.22    let
    1.23      val thy = Proof_Context.theory_of ctxt
    1.24  
    1.25      fun steps_of (Z3_New_Proof.Z3_Step {id, rule, prems, concl, ...}) =
    1.26        let
    1.27 -        fun step_name_of id = (string_of_int id, the_list (AList.lookup (op =) fact_ids id))
    1.28 -
    1.29 -        val name as (sid, ss) = step_name_of id
    1.30 +        val sid = string_of_int id
    1.31  
    1.32          val concl' =
    1.33            concl
    1.34 @@ -102,22 +102,26 @@
    1.35            |> HOLogic.mk_Trueprop
    1.36  
    1.37          fun standard_step role =
    1.38 -          (name, role, concl', Z3_New_Proof.string_of_rule rule, map step_name_of prems)
    1.39 +          ((sid, []), role, concl', Z3_New_Proof.string_of_rule rule,
    1.40 +           map (fn id => (string_of_int id, [])) prems)
    1.41        in
    1.42          (case rule of
    1.43            Z3_New_Proof.Asserted =>
    1.44            let
    1.45 +            val ss = the_list (AList.lookup (op =) fact_ids id)
    1.46              val name0 = (sid ^ "a", ss)
    1.47 +
    1.48              val (role0, concl0) =
    1.49 -              if not (null ss) then
    1.50 -                (Axiom, concl(*FIXME*))
    1.51 -              else if id = conjecture_id then
    1.52 -                (Conjecture, concl_t)
    1.53 -              else
    1.54 -                (Hypothesis,
    1.55 -                 (case find_index (curry (op =) id) prem_ids of
    1.56 -                   ~1 => concl
    1.57 -                 | i => nth hyp_ts i))
    1.58 +              (case ss of
    1.59 +                [s] => (Axiom, the (AList.lookup (op =) fact_ts s))
    1.60 +              | _ =>
    1.61 +                if id = conjecture_id then
    1.62 +                  (Conjecture, concl_t)
    1.63 +                else
    1.64 +                  (Hypothesis,
    1.65 +                   (case find_index (curry (op =) id) prem_ids of
    1.66 +                     ~1 => concl
    1.67 +                   | i => nth hyp_ts i)))
    1.68  
    1.69              val normalize_prems =
    1.70                SMT2_Normalize.case_bool_entry :: SMT2_Normalize.special_quant_table @
    1.71 @@ -128,12 +132,9 @@
    1.72                  else
    1.73                    NONE)
    1.74            in
    1.75 -            if null normalize_prems then
    1.76 -              [(name, role0, concl0, Z3_New_Proof.string_of_rule rule, [])]
    1.77 -            else
    1.78 -              [(name0, role0, concl0, Z3_New_Proof.string_of_rule rule, []),
    1.79 -               (name, Plain, concl', Z3_New_Proof.string_of_rule Z3_New_Proof.Rewrite,
    1.80 -                name0 :: normalize_prems)]
    1.81 +            [(name0, role0, concl0, Z3_New_Proof.string_of_rule rule, []),
    1.82 +             ((sid, []), Plain, concl', Z3_New_Proof.string_of_rule Z3_New_Proof.Rewrite,
    1.83 +              name0 :: normalize_prems)]
    1.84            end
    1.85          | Z3_New_Proof.Rewrite => [standard_step Lemma]
    1.86          | Z3_New_Proof.Rewrite_Star => [standard_step Lemma]
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri May 16 19:13:50 2014 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri May 16 19:14:00 2014 +0200
     2.3 @@ -295,7 +295,7 @@
     2.4          fun str_of_preplay_outcome outcome =
     2.5            if Lazy.is_finished outcome then string_of_play_outcome (Lazy.force outcome) else "?"
     2.6          fun str_of_meth l meth =
     2.7 -          string_of_proof_method [] meth ^ " " ^
     2.8 +          string_of_proof_method ctxt [] meth ^ " " ^
     2.9            str_of_preplay_outcome (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth)
    2.10          fun comment_of l = map (str_of_meth l) #> commas
    2.11  
    2.12 @@ -355,7 +355,7 @@
    2.13            end)
    2.14        end
    2.15  
    2.16 -    val one_line_proof = one_line_proof_text 0 one_line_params
    2.17 +    val one_line_proof = one_line_proof_text ctxt 0 one_line_params
    2.18      val isar_proof =
    2.19        if debug then
    2.20          isar_proof_of ()
    2.21 @@ -378,6 +378,6 @@
    2.22        (isar_proofs = NONE andalso isar_proof_would_be_a_good_idea smt_proofs preplay) then
    2.23       isar_proof_text ctxt debug isar_proofs smt_proofs isar_params
    2.24     else
    2.25 -     one_line_proof_text num_chained) one_line_params
    2.26 +     one_line_proof_text ctxt num_chained) one_line_params
    2.27  
    2.28  end;
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Fri May 16 19:13:50 2014 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Fri May 16 19:14:00 2014 +0200
     3.3 @@ -208,15 +208,15 @@
     3.4  
     3.5  val indent_size = 2
     3.6  
     3.7 -fun string_of_isar_proof ctxt i n proof =
     3.8 +fun string_of_isar_proof ctxt0 i n proof =
     3.9    let
    3.10      (* Make sure only type constraints inserted by the type annotation code are printed. *)
    3.11 -    val ctxt =
    3.12 -      ctxt |> Config.put show_markup false
    3.13 -           |> Config.put Printer.show_type_emphasis false
    3.14 -           |> Config.put show_types false
    3.15 -           |> Config.put show_sorts false
    3.16 -           |> Config.put show_consts false
    3.17 +    val ctxt = ctxt0
    3.18 +      |> Config.put show_markup false
    3.19 +      |> Config.put Printer.show_type_emphasis false
    3.20 +      |> Config.put show_types false
    3.21 +      |> Config.put show_sorts false
    3.22 +      |> Config.put show_consts false
    3.23  
    3.24      val register_fixes = map Free #> fold Variable.auto_fixes
    3.25  
    3.26 @@ -264,7 +264,7 @@
    3.27      fun of_method ls ss meth =
    3.28        let val direct = is_direct_method meth in
    3.29          using_facts ls (if direct then [] else ss) ^
    3.30 -        "by " ^ string_of_proof_method (if direct then ss else []) meth
    3.31 +        "by " ^ string_of_proof_method ctxt (if direct then ss else []) meth
    3.32        end
    3.33  
    3.34      fun of_free (s, T) =
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Fri May 16 19:13:50 2014 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Fri May 16 19:14:00 2014 +0200
     4.3 @@ -33,12 +33,12 @@
     4.4    type one_line_params =
     4.5      (proof_method * play_outcome) * string * (string * stature) list * minimize_command * int * int
     4.6  
     4.7 -  val string_of_proof_method : string list -> proof_method -> string
     4.8 +  val string_of_proof_method : Proof.context -> string list -> proof_method -> string
     4.9    val tac_of_proof_method : Proof.context -> bool -> thm list * thm list -> proof_method -> int ->
    4.10      tactic
    4.11    val string_of_play_outcome : play_outcome -> string
    4.12    val play_outcome_ord : play_outcome * play_outcome -> order
    4.13 -  val one_line_proof_text : int -> one_line_params -> string
    4.14 +  val one_line_proof_text : Proof.context -> int -> one_line_params -> string
    4.15  end;
    4.16  
    4.17  structure Sledgehammer_Proof_Methods : SLEDGEHAMMER_PROOF_METHODS =
    4.18 @@ -74,7 +74,7 @@
    4.19  
    4.20  fun maybe_paren s = s |> not (Symbol_Pos.is_identifier s) ? enclose "(" ")"
    4.21  
    4.22 -fun string_of_proof_method ss meth =
    4.23 +fun string_of_proof_method ctxt ss meth =
    4.24    let
    4.25      val meth_s =
    4.26        (case meth of
    4.27 @@ -86,7 +86,7 @@
    4.28        | SATx_Method => "satx"
    4.29        | Blast_Method => "blast"
    4.30        | Simp_Method => if null ss then "simp" else "simp add:"
    4.31 -      | Simp_Size_Method => "simp add: size_ne_size_imp_ne"
    4.32 +      | Simp_Size_Method => "simp add: " ^ short_thm_name ctxt @{thm size_ne_size_imp_ne}
    4.33        | Auto_Method => "auto"
    4.34        | Fastforce_Method => "fastforce"
    4.35        | Force_Method => "force"
    4.36 @@ -141,8 +141,8 @@
    4.37      "prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal 1 n
    4.38  
    4.39  (* FIXME *)
    4.40 -fun proof_method_command meth i n _(*used_chaineds*) _(*num_chained*) ss =
    4.41 -  apply_on_subgoal i n ^ string_of_proof_method ss meth
    4.42 +fun proof_method_command ctxt meth i n _(*used_chaineds*) _(*num_chained*) ss =
    4.43 +  apply_on_subgoal i n ^ string_of_proof_method ctxt ss meth
    4.44  
    4.45  fun try_command_line banner play command =
    4.46    let val s = string_of_play_outcome play in
    4.47 @@ -161,14 +161,14 @@
    4.48    |> List.partition (fn (_, (sc, _)) => sc = Chained)
    4.49    |> pairself (sort_distinct (string_ord o pairself fst))
    4.50  
    4.51 -fun one_line_proof_text num_chained
    4.52 +fun one_line_proof_text ctxt num_chained
    4.53      ((meth, play), banner, used_facts, minimize_command, subgoal, subgoal_count) =
    4.54    let
    4.55      val (chained, extra) = split_used_facts used_facts
    4.56  
    4.57      val try_line =
    4.58        map fst extra
    4.59 -      |> proof_method_command meth subgoal subgoal_count (map fst chained) num_chained
    4.60 +      |> proof_method_command ctxt meth subgoal subgoal_count (map fst chained) num_chained
    4.61        |> (if play = Play_Failed then enclose "One-line proof reconstruction failed: " "."
    4.62            else try_command_line banner play)
    4.63    in
     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Fri May 16 19:13:50 2014 +0200
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Fri May 16 19:14:00 2014 +0200
     5.3 @@ -216,6 +216,8 @@
     5.4  
     5.5  fun play_one_line_proof mode debug verbose timeout pairs state i preferred (meths as meth :: _) =
     5.6    let
     5.7 +    val ctxt = Proof.context_of state
     5.8 +
     5.9      fun get_preferred meths = if member (op =) meths preferred then preferred else meth
    5.10    in
    5.11      if timeout = Time.zeroTime then
    5.12 @@ -230,7 +232,7 @@
    5.13              let
    5.14                val _ =
    5.15                  if verbose then
    5.16 -                  Output.urgent_message ("Trying \"" ^ string_of_proof_method [] meth ^
    5.17 +                  Output.urgent_message ("Trying \"" ^ string_of_proof_method ctxt [] meth ^
    5.18                      "\" for " ^ string_of_time timeout ^ "...")
    5.19                  else
    5.20                    ()
     6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Fri May 16 19:13:50 2014 +0200
     6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Fri May 16 19:14:00 2014 +0200
     6.3 @@ -61,21 +61,22 @@
     6.4        else raise Fail ("unknown proof_method: " ^ quote name)
     6.5      val used_facts = facts |> map fst
     6.6    in
     6.7 -    (case play_one_line_proof (if mode = Minimize then Normal else mode) debug verbose timeout facts
     6.8 -        state subgoal meth [meth] of
     6.9 +    (case play_one_line_proof (if mode = Minimize then Normal else mode) debug verbose timeout
    6.10 +        facts state subgoal meth [meth] of
    6.11        play as (_, Played time) =>
    6.12        {outcome = NONE, used_facts = used_facts, used_from = facts, run_time = time,
    6.13         preplay = Lazy.value play,
    6.14         message =
    6.15           fn play =>
    6.16              let
    6.17 +              val ctxt = Proof.context_of state
    6.18                val (_, override_params) = extract_proof_method params meth
    6.19                val one_line_params =
    6.20                  (play, proof_banner mode name, used_facts, minimize_command override_params name,
    6.21                   subgoal, subgoal_count)
    6.22                val num_chained = length (#facts (Proof.goal state))
    6.23              in
    6.24 -              one_line_proof_text num_chained one_line_params
    6.25 +              one_line_proof_text ctxt num_chained one_line_params
    6.26              end,
    6.27         message_tail = ""}
    6.28      | play =>
     7.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Fri May 16 19:13:50 2014 +0200
     7.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Fri May 16 19:14:00 2014 +0200
     7.3 @@ -243,7 +243,7 @@
     7.4                   subgoal_count)
     7.5                val num_chained = length (#facts (Proof.goal state))
     7.6              in
     7.7 -              one_line_proof_text num_chained one_line_params
     7.8 +              one_line_proof_text ctxt num_chained one_line_params
     7.9              end,
    7.10           if verbose then "\nSMT solver real CPU time: " ^ string_of_time run_time ^ "." else "")
    7.11        | SOME failure =>
     8.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML	Fri May 16 19:13:50 2014 +0200
     8.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML	Fri May 16 19:14:00 2014 +0200
     8.3 @@ -246,7 +246,8 @@
     8.4                  map (fn (id, th) => (id, short_thm_name ctxt th)) helper_ids @
     8.5                  map (fn (id, ((name, _), _)) => (id, name)) fact_ids
     8.6                val atp_proof = Z3_New_Isar.atp_proof_of_z3_proof ctxt rewrite_rules hyp_ts concl_t
     8.7 -                prem_ids conjecture_id fact_ids z3_proof
     8.8 +                (map (fn ((s, _), th) => (s, prop_of th)) used_named_facts) prem_ids conjecture_id
     8.9 +                fact_ids z3_proof
    8.10                val isar_params =
    8.11                  K (verbose, (NONE, NONE), preplay_timeout, compress_isar, try0_isar,
    8.12                     minimize <> SOME false, atp_proof, goal)