src/HOL/Tools/SMT/z3_isar.ML
author blanchet
Thu Aug 28 00:40:38 2014 +0200 (2014-08-28)
changeset 58061 3d060f43accb
parent 57768 src/HOL/Tools/SMT2/z3_new_isar.ML@a63f14f1214c
child 58064 e9ab6f4c650b
permissions -rw-r--r--
renamed new SMT module from 'SMT2' to 'SMT'
blanchet@58061
     1
(*  Title:      HOL/Tools/SMT/z3_isar.ML
blanchet@56078
     2
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@56078
     3
blanchet@56078
     4
Z3 proofs as generic ATP proofs for Isar proof reconstruction.
blanchet@56078
     5
*)
blanchet@56078
     6
blanchet@58061
     7
signature Z3_ISAR =
blanchet@56078
     8
sig
blanchet@57541
     9
  val atp_proof_of_z3_proof: Proof.context -> term list -> thm list -> term list -> term ->
blanchet@58061
    10
    (string * term) list -> int list -> int -> (int * string) list -> Z3_Proof.z3_step list ->
blanchet@57159
    11
    (term, string) ATP_Proof.atp_step list
blanchet@56078
    12
end;
blanchet@56078
    13
blanchet@58061
    14
structure Z3_Isar: Z3_ISAR =
blanchet@56078
    15
struct
blanchet@56078
    16
blanchet@56078
    17
open ATP_Util
blanchet@56078
    18
open ATP_Problem
blanchet@56078
    19
open ATP_Proof
blanchet@56078
    20
open ATP_Proof_Reconstruct
blanchet@58061
    21
open SMTLIB_Isar
blanchet@56078
    22
blanchet@58061
    23
val z3_apply_def_rule = Z3_Proof.string_of_rule Z3_Proof.Apply_Def
blanchet@58061
    24
val z3_hypothesis_rule = Z3_Proof.string_of_rule Z3_Proof.Hypothesis
blanchet@58061
    25
val z3_intro_def_rule = Z3_Proof.string_of_rule Z3_Proof.Intro_Def
blanchet@58061
    26
val z3_lemma_rule = Z3_Proof.string_of_rule Z3_Proof.Lemma
blanchet@56078
    27
blanchet@56078
    28
fun inline_z3_defs _ [] = []
blanchet@56078
    29
  | inline_z3_defs defs ((name, role, t, rule, deps) :: lines) =
blanchet@56078
    30
    if rule = z3_intro_def_rule then
blanchet@56078
    31
      let val def = t |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> swap in
blanchet@56078
    32
        inline_z3_defs (insert (op =) def defs)
blanchet@56078
    33
          (map (replace_dependencies_in_line (name, [])) lines)
blanchet@56078
    34
      end
blanchet@56078
    35
    else if rule = z3_apply_def_rule then
blanchet@56078
    36
      inline_z3_defs defs (map (replace_dependencies_in_line (name, [])) lines)
blanchet@56078
    37
    else
blanchet@56078
    38
      (name, role, Term.subst_atomic defs t, rule, deps) :: inline_z3_defs defs lines
blanchet@56078
    39
blanchet@56078
    40
fun add_z3_hypotheses [] = I
blanchet@56078
    41
  | add_z3_hypotheses hyps =
blanchet@56078
    42
    HOLogic.dest_Trueprop
blanchet@56078
    43
    #> curry s_imp (Library.foldr1 s_conj (map HOLogic.dest_Trueprop hyps))
blanchet@56078
    44
    #> HOLogic.mk_Trueprop
blanchet@56078
    45
blanchet@56078
    46
fun inline_z3_hypotheses _ _ [] = []
blanchet@56078
    47
  | inline_z3_hypotheses hyp_names hyps ((name, role, t, rule, deps) :: lines) =
blanchet@56078
    48
    if rule = z3_hypothesis_rule then
blanchet@56078
    49
      inline_z3_hypotheses (name :: hyp_names) (AList.map_default (op =) (t, []) (cons name) hyps)
blanchet@56078
    50
        lines
blanchet@56078
    51
    else
blanchet@56078
    52
      let val deps' = subtract (op =) hyp_names deps in
blanchet@56078
    53
        if rule = z3_lemma_rule then
blanchet@56078
    54
          (name, role, t, rule, deps') :: inline_z3_hypotheses hyp_names hyps lines
blanchet@56078
    55
        else
blanchet@56078
    56
          let
blanchet@56078
    57
            val add_hyps = filter_out (null o inter (op =) deps o snd) hyps
blanchet@56078
    58
            val t' = add_z3_hypotheses (map fst add_hyps) t
blanchet@56078
    59
            val deps' = subtract (op =) hyp_names deps
blanchet@56078
    60
            val hyps' = fold (AList.update (op =) o apsnd (insert (op =) name)) add_hyps hyps
blanchet@56078
    61
          in
blanchet@56078
    62
            (name, role, t', rule, deps') :: inline_z3_hypotheses hyp_names hyps' lines
blanchet@56078
    63
          end
blanchet@56078
    64
      end
blanchet@56078
    65
blanchet@57749
    66
fun dest_alls (Const (@{const_name Pure.all}, _) $ Abs (abs as (_, T, _))) =
blanchet@57749
    67
    let val (s', t') = Term.dest_abs abs in
blanchet@57749
    68
      dest_alls t' |>> cons (s', T)
blanchet@57749
    69
    end
blanchet@57749
    70
  | dest_alls t = ([], t)
blanchet@57749
    71
blanchet@57749
    72
val reorder_foralls =
blanchet@57749
    73
  dest_alls
blanchet@57749
    74
  #>> sort_wrt fst
blanchet@57749
    75
  #-> fold_rev (Logic.all o Free);
blanchet@57749
    76
blanchet@57541
    77
fun atp_proof_of_z3_proof ctxt ll_defs rewrite_rules hyp_ts concl_t fact_helper_ts prem_ids
blanchet@57541
    78
    conjecture_id fact_helper_ids proof =
blanchet@56078
    79
  let
blanchet@56981
    80
    val thy = Proof_Context.theory_of ctxt
blanchet@56981
    81
blanchet@58061
    82
    fun steps_of (Z3_Proof.Z3_Step {id, rule, prems, concl, ...}) =
blanchet@56078
    83
      let
blanchet@56985
    84
        val sid = string_of_int id
blanchet@56128
    85
blanchet@57749
    86
        val concl' = concl
blanchet@57749
    87
          |> reorder_foralls (* crucial for skolemization steps *)
blanchet@57749
    88
          |> postprocess_step_conclusion thy rewrite_rules ll_defs
blanchet@56981
    89
        fun standard_step role =
blanchet@58061
    90
          ((sid, []), role, concl', Z3_Proof.string_of_rule rule,
blanchet@56985
    91
           map (fn id => (string_of_int id, [])) prems)
blanchet@56078
    92
      in
blanchet@56981
    93
        (case rule of
blanchet@58061
    94
          Z3_Proof.Asserted =>
blanchet@57730
    95
          let val ss = the_list (AList.lookup (op =) fact_helper_ids id) in
blanchet@57730
    96
            (case distinguish_conjecture_and_hypothesis ss id conjecture_id prem_ids fact_helper_ts
blanchet@57768
    97
                hyp_ts concl_t of
blanchet@57730
    98
              NONE => []
blanchet@57745
    99
            | SOME (role0, concl00) =>
blanchet@57745
   100
              let
blanchet@57745
   101
                val name0 = (sid ^ "a", ss)
blanchet@57745
   102
                val concl0 = unskolemize_names concl00
blanchet@57745
   103
              in
blanchet@57730
   104
                (if role0 = Axiom then []
blanchet@58061
   105
                 else [(name0, role0, concl0, Z3_Proof.string_of_rule rule, [])]) @
blanchet@58061
   106
                [((sid, []), Plain, concl', Z3_Proof.string_of_rule Z3_Proof.Rewrite,
blanchet@57730
   107
                  name0 :: normalizing_prems ctxt concl0)]
blanchet@57730
   108
              end)
blanchet@56981
   109
          end
blanchet@58061
   110
        | Z3_Proof.Rewrite => [standard_step Lemma]
blanchet@58061
   111
        | Z3_Proof.Rewrite_Star => [standard_step Lemma]
blanchet@58061
   112
        | Z3_Proof.Skolemize => [standard_step Lemma]
blanchet@58061
   113
        | Z3_Proof.Th_Lemma _ => [standard_step Lemma]
blanchet@56981
   114
        | _ => [standard_step Plain])
blanchet@56078
   115
      end
blanchet@56078
   116
  in
blanchet@56078
   117
    proof
blanchet@56981
   118
    |> maps steps_of
blanchet@56078
   119
    |> inline_z3_defs []
blanchet@56078
   120
    |> inline_z3_hypotheses [] []
blanchet@56078
   121
  end
blanchet@56078
   122
blanchet@56078
   123
end;