src/HOL/Tools/SMT2/z3_new_isar.ML
author blanchet
Fri May 16 19:13:50 2014 +0200 (2014-05-16)
changeset 56981 3ef45ce002b5
parent 56855 e7a55d295b8e
child 56985 82c83978fbd9
permissions -rw-r--r--
honor original format of conjecture or hypotheses in Z3-to-Isar proofs
     1 (*  Title:      HOL/Tools/SMT2/z3_new_isar.ML
     2     Author:     Jasmin Blanchette, TU Muenchen
     3 
     4 Z3 proofs as generic ATP proofs for Isar proof reconstruction.
     5 *)
     6 
     7 signature Z3_NEW_ISAR =
     8 sig
     9   type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step
    10 
    11   val atp_proof_of_z3_proof: Proof.context -> thm list -> term list -> term -> int list -> int ->
    12     (int * string) list -> Z3_New_Proof.z3_step list -> (term, string) atp_step list
    13 end;
    14 
    15 structure Z3_New_Isar: Z3_NEW_ISAR =
    16 struct
    17 
    18 open ATP_Util
    19 open ATP_Problem
    20 open ATP_Proof
    21 open ATP_Proof_Reconstruct
    22 
    23 val z3_apply_def_rule = Z3_New_Proof.string_of_rule Z3_New_Proof.Apply_Def
    24 val z3_hypothesis_rule = Z3_New_Proof.string_of_rule Z3_New_Proof.Hypothesis
    25 val z3_intro_def_rule = Z3_New_Proof.string_of_rule Z3_New_Proof.Intro_Def
    26 val z3_lemma_rule = Z3_New_Proof.string_of_rule Z3_New_Proof.Lemma
    27 
    28 fun inline_z3_defs _ [] = []
    29   | inline_z3_defs defs ((name, role, t, rule, deps) :: lines) =
    30     if rule = z3_intro_def_rule then
    31       let val def = t |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> swap in
    32         inline_z3_defs (insert (op =) def defs)
    33           (map (replace_dependencies_in_line (name, [])) lines)
    34       end
    35     else if rule = z3_apply_def_rule then
    36       inline_z3_defs defs (map (replace_dependencies_in_line (name, [])) lines)
    37     else
    38       (name, role, Term.subst_atomic defs t, rule, deps) :: inline_z3_defs defs lines
    39 
    40 fun add_z3_hypotheses [] = I
    41   | add_z3_hypotheses hyps =
    42     HOLogic.dest_Trueprop
    43     #> curry s_imp (Library.foldr1 s_conj (map HOLogic.dest_Trueprop hyps))
    44     #> HOLogic.mk_Trueprop
    45 
    46 fun inline_z3_hypotheses _ _ [] = []
    47   | inline_z3_hypotheses hyp_names hyps ((name, role, t, rule, deps) :: lines) =
    48     if rule = z3_hypothesis_rule then
    49       inline_z3_hypotheses (name :: hyp_names) (AList.map_default (op =) (t, []) (cons name) hyps)
    50         lines
    51     else
    52       let val deps' = subtract (op =) hyp_names deps in
    53         if rule = z3_lemma_rule then
    54           (name, role, t, rule, deps') :: inline_z3_hypotheses hyp_names hyps lines
    55         else
    56           let
    57             val add_hyps = filter_out (null o inter (op =) deps o snd) hyps
    58             val t' = add_z3_hypotheses (map fst add_hyps) t
    59             val deps' = subtract (op =) hyp_names deps
    60             val hyps' = fold (AList.update (op =) o apsnd (insert (op =) name)) add_hyps hyps
    61           in
    62             (name, role, t', rule, deps') :: inline_z3_hypotheses hyp_names hyps' lines
    63           end
    64       end
    65 
    66 fun simplify_bool ((all as Const (@{const_name All}, _)) $ Abs (s, T, t)) =
    67     let val t' = simplify_bool t in
    68       if loose_bvar1 (t', 0) then all $ Abs (s, T, t') else t'
    69     end
    70   | simplify_bool (@{const Not} $ t) = s_not (simplify_bool t)
    71   | simplify_bool (@{const conj} $ t $ u) = s_conj (simplify_bool t, simplify_bool u)
    72   | simplify_bool (@{const disj} $ t $ u) = s_disj (simplify_bool t, simplify_bool u)
    73   | simplify_bool (@{const implies} $ t $ u) = s_imp (simplify_bool t, simplify_bool u)
    74   | simplify_bool (@{const HOL.eq (bool)} $ t $ u) = s_iff (simplify_bool t, simplify_bool u)
    75   | simplify_bool (t as Const (@{const_name HOL.eq}, _) $ u $ v) =
    76     if u aconv v then @{const True} else t
    77   | simplify_bool (t $ u) = simplify_bool t $ simplify_bool u
    78   | simplify_bool (Abs (s, T, t)) = Abs (s, T, simplify_bool t)
    79   | simplify_bool t = t
    80 
    81 (* It is not entirely clear why this should be necessary, especially for abstractions variables. *)
    82 val unskolemize_names =
    83   Term.map_abs_vars (perhaps (try Name.dest_skolem))
    84   #> Term.map_aterms (perhaps (try (fn Free (s, T) => Free (Name.dest_skolem s, T))))
    85 
    86 fun atp_proof_of_z3_proof ctxt rewrite_rules hyp_ts concl_t prem_ids conjecture_id fact_ids proof =
    87   let
    88     val thy = Proof_Context.theory_of ctxt
    89 
    90     fun steps_of (Z3_New_Proof.Z3_Step {id, rule, prems, concl, ...}) =
    91       let
    92         fun step_name_of id = (string_of_int id, the_list (AList.lookup (op =) fact_ids id))
    93 
    94         val name as (sid, ss) = step_name_of id
    95 
    96         val concl' =
    97           concl
    98           |> Raw_Simplifier.rewrite_term thy rewrite_rules []
    99           |> Object_Logic.atomize_term thy
   100           |> simplify_bool
   101           |> unskolemize_names
   102           |> HOLogic.mk_Trueprop
   103 
   104         fun standard_step role =
   105           (name, role, concl', Z3_New_Proof.string_of_rule rule, map step_name_of prems)
   106       in
   107         (case rule of
   108           Z3_New_Proof.Asserted =>
   109           let
   110             val name0 = (sid ^ "a", ss)
   111             val (role0, concl0) =
   112               if not (null ss) then
   113                 (Axiom, concl(*FIXME*))
   114               else if id = conjecture_id then
   115                 (Conjecture, concl_t)
   116               else
   117                 (Hypothesis,
   118                  (case find_index (curry (op =) id) prem_ids of
   119                    ~1 => concl
   120                  | i => nth hyp_ts i))
   121 
   122             val normalize_prems =
   123               SMT2_Normalize.case_bool_entry :: SMT2_Normalize.special_quant_table @
   124               SMT2_Normalize.abs_min_max_table
   125               |> map_filter (fn (c, th) =>
   126                 if exists_Const (curry (op =) c o fst) concl0 then
   127                   let val s = short_thm_name ctxt th in SOME (s, [s]) end
   128                 else
   129                   NONE)
   130           in
   131             if null normalize_prems then
   132               [(name, role0, concl0, Z3_New_Proof.string_of_rule rule, [])]
   133             else
   134               [(name0, role0, concl0, Z3_New_Proof.string_of_rule rule, []),
   135                (name, Plain, concl', Z3_New_Proof.string_of_rule Z3_New_Proof.Rewrite,
   136                 name0 :: normalize_prems)]
   137           end
   138         | Z3_New_Proof.Rewrite => [standard_step Lemma]
   139         | Z3_New_Proof.Rewrite_Star => [standard_step Lemma]
   140         | Z3_New_Proof.Skolemize => [standard_step Lemma]
   141         | Z3_New_Proof.Th_Lemma _ => [standard_step Lemma]
   142         | _ => [standard_step Plain])
   143       end
   144   in
   145     proof
   146     |> maps steps_of
   147     |> inline_z3_defs []
   148     |> inline_z3_hypotheses [] []
   149   end
   150 
   151 end;