src/HOL/Tools/SMT/z3_isar.ML
author wenzelm
Sun Nov 26 21:08:32 2017 +0100 (17 months ago)
changeset 67091 1393c2340eec
parent 60924 610794dff23c
child 69593 3dda49e08b9d
permissions -rw-r--r--
more symbols;
     1 (*  Title:      HOL/Tools/SMT/z3_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_ISAR =
     8 sig
     9   val atp_proof_of_z3_proof: Proof.context -> term list -> thm list -> term list -> term ->
    10     (string * term) list -> int list -> int -> (int * string) list -> Z3_Proof.z3_step list ->
    11     (term, string) ATP_Proof.atp_step list
    12 end;
    13 
    14 structure Z3_Isar: Z3_ISAR =
    15 struct
    16 
    17 open ATP_Util
    18 open ATP_Problem
    19 open ATP_Proof
    20 open ATP_Proof_Reconstruct
    21 open SMTLIB_Isar
    22 
    23 val z3_apply_def_rule = Z3_Proof.string_of_rule Z3_Proof.Apply_Def
    24 val z3_hypothesis_rule = Z3_Proof.string_of_rule Z3_Proof.Hypothesis
    25 val z3_intro_def_rule = Z3_Proof.string_of_rule Z3_Proof.Intro_Def
    26 val z3_lemma_rule = Z3_Proof.string_of_rule Z3_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 hyps' = fold (AList.update (op =) o apsnd (insert (op =) name)) add_hyps hyps
    60           in
    61             (name, role, t', rule, deps') :: inline_z3_hypotheses hyp_names hyps' lines
    62           end
    63       end
    64 
    65 fun dest_alls (Const (@{const_name Pure.all}, _) $ Abs (abs as (_, T, _))) =
    66     let val (s', t') = Term.dest_abs abs in
    67       dest_alls t' |>> cons (s', T)
    68     end
    69   | dest_alls t = ([], t)
    70 
    71 val reorder_foralls =
    72   dest_alls
    73   #>> sort_by fst
    74   #-> fold_rev (Logic.all o Free);
    75 
    76 fun atp_proof_of_z3_proof ctxt ll_defs rewrite_rules hyp_ts concl_t fact_helper_ts prem_ids
    77     conjecture_id fact_helper_ids proof =
    78   let
    79     fun steps_of (Z3_Proof.Z3_Step {id, rule, prems, concl, ...}) =
    80       let
    81         val sid = string_of_int id
    82 
    83         val concl' = concl
    84           |> reorder_foralls (* crucial for skolemization steps *)
    85           |> postprocess_step_conclusion ctxt rewrite_rules ll_defs
    86         fun standard_step role =
    87           ((sid, []), role, concl', Z3_Proof.string_of_rule rule,
    88            map (fn id => (string_of_int id, [])) prems)
    89       in
    90         (case rule of
    91           Z3_Proof.Asserted =>
    92           let val ss = the_list (AList.lookup (op =) fact_helper_ids id) in
    93             (case distinguish_conjecture_and_hypothesis ss id conjecture_id prem_ids fact_helper_ts
    94                 hyp_ts concl_t of
    95               NONE => []
    96             | SOME (role0, concl00) =>
    97               let
    98                 val name0 = (sid ^ "a", ss)
    99                 val concl0 = unskolemize_names ctxt concl00
   100               in
   101                 (if role0 = Axiom then []
   102                  else [(name0, role0, concl0, Z3_Proof.string_of_rule rule, [])]) @
   103                 [((sid, []), Plain, concl', Z3_Proof.string_of_rule Z3_Proof.Rewrite,
   104                   name0 :: normalizing_prems ctxt concl0)]
   105               end)
   106           end
   107         | Z3_Proof.Rewrite => [standard_step Lemma]
   108         | Z3_Proof.Rewrite_Star => [standard_step Lemma]
   109         | Z3_Proof.Skolemize => [standard_step Lemma]
   110         | Z3_Proof.Th_Lemma _ => [standard_step Lemma]
   111         | _ => [standard_step Plain])
   112       end
   113   in
   114     proof
   115     |> maps steps_of
   116     |> inline_z3_defs []
   117     |> inline_z3_hypotheses [] []
   118   end
   119 
   120 end;