honor original format of conjecture or hypotheses in Z3-to-Isar proofs
authorblanchet
Fri May 16 19:13:50 2014 +0200 (2014-05-16)
changeset 569813ef45ce002b5
parent 56980 9c5220e05e04
child 56982 51d4189d95cf
honor original format of conjecture or hypotheses in Z3-to-Isar proofs
src/HOL/Tools/SMT2/smt2_normalize.ML
src/HOL/Tools/SMT2/smt2_solver.ML
src/HOL/Tools/SMT2/z3_new_isar.ML
src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML
     1.1 --- a/src/HOL/Tools/SMT2/smt2_normalize.ML	Fri May 16 17:11:56 2014 +0200
     1.2 +++ b/src/HOL/Tools/SMT2/smt2_normalize.ML	Fri May 16 19:13:50 2014 +0200
     1.3 @@ -8,6 +8,11 @@
     1.4  sig
     1.5    val drop_fact_warning: Proof.context -> thm -> unit
     1.6    val atomize_conv: Proof.context -> conv
     1.7 +
     1.8 +  val special_quant_table: (string * thm) list
     1.9 +  val case_bool_entry: string * thm
    1.10 +  val abs_min_max_table: (string * thm) list
    1.11 +
    1.12    type extra_norm = Proof.context -> thm list * thm list -> thm list * thm list
    1.13    val add_extra_norm: SMT2_Util.class * extra_norm -> Context.generic -> Context.generic
    1.14    val normalize: Proof.context -> (int option * thm) list -> (int * thm) list
    1.15 @@ -71,13 +76,13 @@
    1.16  
    1.17  (** unfold special quantifiers **)
    1.18  
    1.19 +val special_quant_table = [
    1.20 +  (@{const_name Ex1}, @{thm Ex1_def_raw}),
    1.21 +  (@{const_name Ball}, @{thm Ball_def_raw}),
    1.22 +  (@{const_name Bex}, @{thm Bex_def_raw})]
    1.23 +
    1.24  local
    1.25 -  val special_quants = [
    1.26 -    (@{const_name Ex1}, @{thm Ex1_def_raw}),
    1.27 -    (@{const_name Ball}, @{thm Ball_def_raw}),
    1.28 -    (@{const_name Bex}, @{thm Bex_def_raw})]
    1.29 -  
    1.30 -  fun special_quant (Const (n, _)) = AList.lookup (op =) special_quants n
    1.31 +  fun special_quant (Const (n, _)) = AList.lookup (op =) special_quant_table n
    1.32      | special_quant _ = NONE
    1.33  
    1.34    fun special_quant_conv _ ct =
    1.35 @@ -89,7 +94,7 @@
    1.36  fun unfold_special_quants_conv ctxt =
    1.37    SMT2_Util.if_exists_conv (is_some o special_quant) (Conv.top_conv special_quant_conv ctxt)
    1.38  
    1.39 -val setup_unfolded_quants = fold (SMT2_Builtin.add_builtin_fun_ext'' o fst) special_quants
    1.40 +val setup_unfolded_quants = fold (SMT2_Builtin.add_builtin_fun_ext'' o fst) special_quant_table
    1.41  
    1.42  end
    1.43  
    1.44 @@ -326,6 +331,8 @@
    1.45  
    1.46  (** rewrite bool case expressions as if expressions **)
    1.47  
    1.48 +val case_bool_entry = (@{const_name "bool.case_bool"}, @{thm case_bool_if})
    1.49 +
    1.50  local
    1.51    fun is_case_bool (Const (@{const_name "bool.case_bool"}, _)) = true
    1.52      | is_case_bool _ = false
    1.53 @@ -345,14 +352,14 @@
    1.54  
    1.55  (** unfold abs, min and max **)
    1.56  
    1.57 +val abs_min_max_table = [
    1.58 +  (@{const_name min}, @{thm min_def_raw}),
    1.59 +  (@{const_name max}, @{thm max_def_raw}),
    1.60 +  (@{const_name abs}, @{thm abs_if_raw})]
    1.61 +
    1.62  local
    1.63 -  val defs = [
    1.64 -    (@{const_name min}, @{thm min_def_raw}),
    1.65 -    (@{const_name max}, @{thm max_def_raw}),
    1.66 -    (@{const_name abs}, @{thm abs_if_raw})]
    1.67 -
    1.68    fun abs_min_max ctxt (Const (n, Type (@{type_name fun}, [T, _]))) =
    1.69 -        (case AList.lookup (op =) defs n of
    1.70 +        (case AList.lookup (op =) abs_min_max_table n of
    1.71            NONE => NONE
    1.72          | SOME thm => if SMT2_Builtin.is_builtin_typ_ext ctxt T then SOME thm else NONE)
    1.73      | abs_min_max _ _ = NONE
    1.74 @@ -366,7 +373,7 @@
    1.75  fun unfold_abs_min_max_conv ctxt =
    1.76    SMT2_Util.if_exists_conv (is_some o abs_min_max ctxt) (Conv.top_conv unfold_amm_conv ctxt)
    1.77    
    1.78 -val setup_abs_min_max = fold (SMT2_Builtin.add_builtin_fun_ext'' o fst) defs
    1.79 +val setup_abs_min_max = fold (SMT2_Builtin.add_builtin_fun_ext'' o fst) abs_min_max_table
    1.80  
    1.81  end
    1.82  
     2.1 --- a/src/HOL/Tools/SMT2/smt2_solver.ML	Fri May 16 17:11:56 2014 +0200
     2.2 +++ b/src/HOL/Tools/SMT2/smt2_solver.ML	Fri May 16 19:13:50 2014 +0200
     2.3 @@ -29,7 +29,7 @@
     2.4    (*filter*)
     2.5    val smt2_filter: Proof.context -> thm -> ('a * (int option * thm)) list -> int -> Time.time ->
     2.6      {outcome: SMT2_Failure.failure option, rewrite_rules: thm list, conjecture_id: int,
     2.7 -     helper_ids: (int * thm) list, fact_ids: (int * ('a * thm)) list,
     2.8 +     prem_ids: int list, helper_ids: (int * thm) list, fact_ids: (int * ('a * thm)) list,
     2.9       z3_proof: Z3_New_Proof.z3_step list}
    2.10  
    2.11    (*tactic*)
    2.12 @@ -260,17 +260,20 @@
    2.13      val iwthms = map_index I wthms
    2.14  
    2.15      val conjecture_i = 0
    2.16 -    val facts_i = 1 + length wprems
    2.17 +    val prems_i = 1
    2.18 +    val facts_i = prems_i + length wprems
    2.19    in
    2.20      wthms
    2.21      |> apply_solver ctxt
    2.22      |> (fn (((iidths0, z3_proof), _), {rewrite_rules, ...}) =>
    2.23 -      let val iidths = if can_filter ctxt then iidths0 else map (apsnd (apfst (K no_id))) iwthms
    2.24 +      let
    2.25 +        val iidths = if can_filter ctxt then iidths0 else map (apsnd (apfst (K no_id))) iwthms
    2.26 +        fun id_of_index i = the_default no_id (Option.map fst (AList.lookup (op =) iidths i))
    2.27        in
    2.28          {outcome = NONE,
    2.29           rewrite_rules = rewrite_rules,
    2.30 -         conjecture_id =
    2.31 -           the_default no_id (Option.map fst (AList.lookup (op =) iidths conjecture_i)),
    2.32 +         conjecture_id = id_of_index conjecture_i,
    2.33 +         prem_ids = map id_of_index (prems_i upto facts_i - 1),
    2.34           helper_ids = map_filter (try (fn (~1, idth) => idth)) iidths,
    2.35           fact_ids = map_filter (fn (i, (id, _)) =>
    2.36             try (apsnd (apsnd snd o nth xwfacts)) (id, i - facts_i)) iidths,
    2.37 @@ -278,7 +281,7 @@
    2.38        end)
    2.39    end
    2.40    handle SMT2_Failure.SMT fail => {outcome = SOME fail, rewrite_rules = [], conjecture_id = no_id,
    2.41 -    helper_ids = [], fact_ids = [], z3_proof = []}
    2.42 +    prem_ids = [], helper_ids = [], fact_ids = [], z3_proof = []}
    2.43  
    2.44  
    2.45  (* SMT tactic *)
     3.1 --- a/src/HOL/Tools/SMT2/z3_new_isar.ML	Fri May 16 17:11:56 2014 +0200
     3.2 +++ b/src/HOL/Tools/SMT2/z3_new_isar.ML	Fri May 16 19:13:50 2014 +0200
     3.3 @@ -8,8 +8,8 @@
     3.4  sig
     3.5    type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step
     3.6  
     3.7 -  val atp_proof_of_z3_proof: theory -> thm list -> int -> (int * string) list ->
     3.8 -    Z3_New_Proof.z3_step list -> (term, string) atp_step list
     3.9 +  val atp_proof_of_z3_proof: Proof.context -> thm list -> term list -> term -> int list -> int ->
    3.10 +    (int * string) list -> Z3_New_Proof.z3_step list -> (term, string) atp_step list
    3.11  end;
    3.12  
    3.13  structure Z3_New_Isar: Z3_NEW_ISAR =
    3.14 @@ -83,38 +83,67 @@
    3.15    Term.map_abs_vars (perhaps (try Name.dest_skolem))
    3.16    #> Term.map_aterms (perhaps (try (fn Free (s, T) => Free (Name.dest_skolem s, T))))
    3.17  
    3.18 -fun atp_proof_of_z3_proof thy rewrite_rules conjecture_id fact_ids proof =
    3.19 +fun atp_proof_of_z3_proof ctxt rewrite_rules hyp_ts concl_t prem_ids conjecture_id fact_ids proof =
    3.20    let
    3.21 -    fun step_of (Z3_New_Proof.Z3_Step {id, rule, prems, concl, ...}) =
    3.22 +    val thy = Proof_Context.theory_of ctxt
    3.23 +
    3.24 +    fun steps_of (Z3_New_Proof.Z3_Step {id, rule, prems, concl, ...}) =
    3.25        let
    3.26          fun step_name_of id = (string_of_int id, the_list (AList.lookup (op =) fact_ids id))
    3.27  
    3.28 -        val name as (_, ss) = step_name_of id
    3.29 +        val name as (sid, ss) = step_name_of id
    3.30  
    3.31 -        val role =
    3.32 -          (case rule of
    3.33 -            Z3_New_Proof.Asserted =>
    3.34 -              if not (null ss) then Axiom
    3.35 -              else if id = conjecture_id then Negated_Conjecture
    3.36 -              else Hypothesis
    3.37 -          | Z3_New_Proof.Rewrite => Lemma
    3.38 -          | Z3_New_Proof.Rewrite_Star => Lemma
    3.39 -          | Z3_New_Proof.Skolemize => Lemma
    3.40 -          | Z3_New_Proof.Th_Lemma _ => Lemma
    3.41 -          | _ => Plain)
    3.42 -
    3.43 -        val concl' = concl
    3.44 +        val concl' =
    3.45 +          concl
    3.46            |> Raw_Simplifier.rewrite_term thy rewrite_rules []
    3.47            |> Object_Logic.atomize_term thy
    3.48            |> simplify_bool
    3.49            |> unskolemize_names
    3.50            |> HOLogic.mk_Trueprop
    3.51 +
    3.52 +        fun standard_step role =
    3.53 +          (name, role, concl', Z3_New_Proof.string_of_rule rule, map step_name_of prems)
    3.54        in
    3.55 -        (name, role, concl', Z3_New_Proof.string_of_rule rule, map step_name_of prems)
    3.56 +        (case rule of
    3.57 +          Z3_New_Proof.Asserted =>
    3.58 +          let
    3.59 +            val name0 = (sid ^ "a", ss)
    3.60 +            val (role0, concl0) =
    3.61 +              if not (null ss) then
    3.62 +                (Axiom, concl(*FIXME*))
    3.63 +              else if id = conjecture_id then
    3.64 +                (Conjecture, concl_t)
    3.65 +              else
    3.66 +                (Hypothesis,
    3.67 +                 (case find_index (curry (op =) id) prem_ids of
    3.68 +                   ~1 => concl
    3.69 +                 | i => nth hyp_ts i))
    3.70 +
    3.71 +            val normalize_prems =
    3.72 +              SMT2_Normalize.case_bool_entry :: SMT2_Normalize.special_quant_table @
    3.73 +              SMT2_Normalize.abs_min_max_table
    3.74 +              |> map_filter (fn (c, th) =>
    3.75 +                if exists_Const (curry (op =) c o fst) concl0 then
    3.76 +                  let val s = short_thm_name ctxt th in SOME (s, [s]) end
    3.77 +                else
    3.78 +                  NONE)
    3.79 +          in
    3.80 +            if null normalize_prems then
    3.81 +              [(name, role0, concl0, Z3_New_Proof.string_of_rule rule, [])]
    3.82 +            else
    3.83 +              [(name0, role0, concl0, Z3_New_Proof.string_of_rule rule, []),
    3.84 +               (name, Plain, concl', Z3_New_Proof.string_of_rule Z3_New_Proof.Rewrite,
    3.85 +                name0 :: normalize_prems)]
    3.86 +          end
    3.87 +        | Z3_New_Proof.Rewrite => [standard_step Lemma]
    3.88 +        | Z3_New_Proof.Rewrite_Star => [standard_step Lemma]
    3.89 +        | Z3_New_Proof.Skolemize => [standard_step Lemma]
    3.90 +        | Z3_New_Proof.Th_Lemma _ => [standard_step Lemma]
    3.91 +        | _ => [standard_step Plain])
    3.92        end
    3.93    in
    3.94      proof
    3.95 -    |> map step_of
    3.96 +    |> maps steps_of
    3.97      |> inline_z3_defs []
    3.98      |> inline_z3_hypotheses [] []
    3.99    end
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML	Fri May 16 17:11:56 2014 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML	Fri May 16 19:13:50 2014 +0200
     4.3 @@ -161,8 +161,8 @@
     4.4                reraise exn
     4.5              else
     4.6                {outcome = SOME (SMT2_Failure.Other_Failure (Runtime.exn_message exn)),
     4.7 -               rewrite_rules = [], conjecture_id = ~1, helper_ids = [], fact_ids = [],
     4.8 -               z3_proof = []}
     4.9 +               rewrite_rules = [], conjecture_id = ~1, prem_ids = [], helper_ids = [],
    4.10 +               fact_ids = [], z3_proof = []}
    4.11  
    4.12          val death = Timer.checkRealTimer timer
    4.13          val outcome0 = if is_none outcome0 then SOME outcome else outcome0
    4.14 @@ -227,8 +227,8 @@
    4.15        end
    4.16  
    4.17      val weighted_factss = map (apsnd weight_facts) factss
    4.18 -    val {outcome, filter_result = {conjecture_id, rewrite_rules, helper_ids, fact_ids, z3_proof,
    4.19 -           ...}, used_from, run_time} =
    4.20 +    val {outcome, filter_result = {rewrite_rules, conjecture_id, prem_ids, helper_ids, fact_ids,
    4.21 +           z3_proof, ...}, used_from, run_time} =
    4.22        smt2_filter_loop name params state goal subgoal weighted_factss
    4.23      val used_named_facts = map snd fact_ids
    4.24      val used_facts = map fst used_named_facts
    4.25 @@ -245,7 +245,7 @@
    4.26                val fact_ids =
    4.27                  map (fn (id, th) => (id, short_thm_name ctxt th)) helper_ids @
    4.28                  map (fn (id, ((name, _), _)) => (id, name)) fact_ids
    4.29 -              val atp_proof = Z3_New_Isar.atp_proof_of_z3_proof thy rewrite_rules conjecture_id
    4.30 +              val atp_proof = Z3_New_Isar.atp_proof_of_z3_proof thy rewrite_rules prem_ids conjecture_id
    4.31                  fact_ids z3_proof
    4.32                val isar_params =
    4.33                  K (verbose, (NONE, NONE), preplay_timeout, compress_isar, try0_isar,