src/HOL/Tools/SMT2/z3_new_isar.ML
changeset 56981 3ef45ce002b5
parent 56855 e7a55d295b8e
child 56985 82c83978fbd9
     1.1 --- a/src/HOL/Tools/SMT2/z3_new_isar.ML	Fri May 16 17:11:56 2014 +0200
     1.2 +++ b/src/HOL/Tools/SMT2/z3_new_isar.ML	Fri May 16 19:13:50 2014 +0200
     1.3 @@ -8,8 +8,8 @@
     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: theory -> thm list -> int -> (int * string) list ->
     1.8 -    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 -> int list -> int ->
    1.10 +    (int * string) list -> Z3_New_Proof.z3_step list -> (term, string) atp_step list
    1.11  end;
    1.12  
    1.13  structure Z3_New_Isar: Z3_NEW_ISAR =
    1.14 @@ -83,38 +83,67 @@
    1.15    Term.map_abs_vars (perhaps (try Name.dest_skolem))
    1.16    #> Term.map_aterms (perhaps (try (fn Free (s, T) => Free (Name.dest_skolem s, T))))
    1.17  
    1.18 -fun atp_proof_of_z3_proof thy rewrite_rules conjecture_id fact_ids proof =
    1.19 +fun atp_proof_of_z3_proof ctxt rewrite_rules hyp_ts concl_t prem_ids conjecture_id fact_ids proof =
    1.20    let
    1.21 -    fun step_of (Z3_New_Proof.Z3_Step {id, rule, prems, concl, ...}) =
    1.22 +    val thy = Proof_Context.theory_of ctxt
    1.23 +
    1.24 +    fun steps_of (Z3_New_Proof.Z3_Step {id, rule, prems, concl, ...}) =
    1.25        let
    1.26          fun step_name_of id = (string_of_int id, the_list (AList.lookup (op =) fact_ids id))
    1.27  
    1.28 -        val name as (_, ss) = step_name_of id
    1.29 +        val name as (sid, ss) = step_name_of id
    1.30  
    1.31 -        val role =
    1.32 -          (case rule of
    1.33 -            Z3_New_Proof.Asserted =>
    1.34 -              if not (null ss) then Axiom
    1.35 -              else if id = conjecture_id then Negated_Conjecture
    1.36 -              else Hypothesis
    1.37 -          | Z3_New_Proof.Rewrite => Lemma
    1.38 -          | Z3_New_Proof.Rewrite_Star => Lemma
    1.39 -          | Z3_New_Proof.Skolemize => Lemma
    1.40 -          | Z3_New_Proof.Th_Lemma _ => Lemma
    1.41 -          | _ => Plain)
    1.42 -
    1.43 -        val concl' = concl
    1.44 +        val concl' =
    1.45 +          concl
    1.46            |> Raw_Simplifier.rewrite_term thy rewrite_rules []
    1.47            |> Object_Logic.atomize_term thy
    1.48            |> simplify_bool
    1.49            |> unskolemize_names
    1.50            |> HOLogic.mk_Trueprop
    1.51 +
    1.52 +        fun standard_step role =
    1.53 +          (name, role, concl', Z3_New_Proof.string_of_rule rule, map step_name_of prems)
    1.54        in
    1.55 -        (name, role, concl', Z3_New_Proof.string_of_rule rule, map step_name_of prems)
    1.56 +        (case rule of
    1.57 +          Z3_New_Proof.Asserted =>
    1.58 +          let
    1.59 +            val name0 = (sid ^ "a", ss)
    1.60 +            val (role0, concl0) =
    1.61 +              if not (null ss) then
    1.62 +                (Axiom, concl(*FIXME*))
    1.63 +              else if id = conjecture_id then
    1.64 +                (Conjecture, concl_t)
    1.65 +              else
    1.66 +                (Hypothesis,
    1.67 +                 (case find_index (curry (op =) id) prem_ids of
    1.68 +                   ~1 => concl
    1.69 +                 | i => nth hyp_ts i))
    1.70 +
    1.71 +            val normalize_prems =
    1.72 +              SMT2_Normalize.case_bool_entry :: SMT2_Normalize.special_quant_table @
    1.73 +              SMT2_Normalize.abs_min_max_table
    1.74 +              |> map_filter (fn (c, th) =>
    1.75 +                if exists_Const (curry (op =) c o fst) concl0 then
    1.76 +                  let val s = short_thm_name ctxt th in SOME (s, [s]) end
    1.77 +                else
    1.78 +                  NONE)
    1.79 +          in
    1.80 +            if null normalize_prems then
    1.81 +              [(name, role0, concl0, Z3_New_Proof.string_of_rule rule, [])]
    1.82 +            else
    1.83 +              [(name0, role0, concl0, Z3_New_Proof.string_of_rule rule, []),
    1.84 +               (name, Plain, concl', Z3_New_Proof.string_of_rule Z3_New_Proof.Rewrite,
    1.85 +                name0 :: normalize_prems)]
    1.86 +          end
    1.87 +        | Z3_New_Proof.Rewrite => [standard_step Lemma]
    1.88 +        | Z3_New_Proof.Rewrite_Star => [standard_step Lemma]
    1.89 +        | Z3_New_Proof.Skolemize => [standard_step Lemma]
    1.90 +        | Z3_New_Proof.Th_Lemma _ => [standard_step Lemma]
    1.91 +        | _ => [standard_step Plain])
    1.92        end
    1.93    in
    1.94      proof
    1.95 -    |> map step_of
    1.96 +    |> maps steps_of
    1.97      |> inline_z3_defs []
    1.98      |> inline_z3_hypotheses [] []
    1.99    end