1(*  Title:      HOL/Tools/SMT/z3_isar.ML
2    Author:     Jasmin Blanchette, TU Muenchen
3
4Z3 proofs as generic ATP proofs for Isar proof reconstruction.
5*)
6
7signature Z3_ISAR =
8sig
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
12end;
13
14structure Z3_Isar: Z3_ISAR =
15struct
16
17open ATP_Util
18open ATP_Problem
19open ATP_Proof
20open ATP_Proof_Reconstruct
21open SMTLIB_Isar
22
23val z3_apply_def_rule = Z3_Proof.string_of_rule Z3_Proof.Apply_Def
24val z3_hypothesis_rule = Z3_Proof.string_of_rule Z3_Proof.Hypothesis
25val z3_intro_def_rule = Z3_Proof.string_of_rule Z3_Proof.Intro_Def
26val z3_lemma_rule = Z3_Proof.string_of_rule Z3_Proof.Lemma
27
28fun 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
40fun 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
46fun 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
65fun dest_alls (Const (\<^const_name>\<open>Pure.all\<close>, _) $ 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
71val reorder_foralls =
72  dest_alls
73  #>> sort_by fst
74  #-> fold_rev (Logic.all o Free);
75
76fun 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
120end;
121