src/HOL/Tools/SMT2/z3_new_isar.ML
author blanchet
Thu Mar 13 13:18:13 2014 +0100 (2014-03-13)
changeset 56078 624faeda77b5
child 56083 b5d1d9c60341
permissions -rw-r--r--
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet@56078
     1
(*  Title:      HOL/Tools/SMT2/z3_new_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@56078
     7
signature Z3_NEW_ISAR =
blanchet@56078
     8
sig
blanchet@56078
     9
  type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step
blanchet@56078
    10
blanchet@56078
    11
  val atp_proof_of_z3_proof: theory -> Z3_New_Proof.z3_step list -> (term, string) atp_step list
blanchet@56078
    12
end;
blanchet@56078
    13
blanchet@56078
    14
structure Z3_New_Isar: Z3_NEW_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@56078
    21
blanchet@56078
    22
val z3_apply_def_rule = Z3_New_Proof.string_of_rule Z3_New_Proof.Apply_Def
blanchet@56078
    23
val z3_hypothesis_rule = Z3_New_Proof.string_of_rule Z3_New_Proof.Hypothesis
blanchet@56078
    24
val z3_intro_def_rule = Z3_New_Proof.string_of_rule Z3_New_Proof.Intro_Def
blanchet@56078
    25
val z3_lemma_rule = Z3_New_Proof.string_of_rule Z3_New_Proof.Lemma
blanchet@56078
    26
blanchet@56078
    27
fun inline_z3_defs _ [] = []
blanchet@56078
    28
  | inline_z3_defs defs ((name, role, t, rule, deps) :: lines) =
blanchet@56078
    29
    if rule = z3_intro_def_rule then
blanchet@56078
    30
      let val def = t |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> swap in
blanchet@56078
    31
        inline_z3_defs (insert (op =) def defs)
blanchet@56078
    32
          (map (replace_dependencies_in_line (name, [])) lines)
blanchet@56078
    33
      end
blanchet@56078
    34
    else if rule = z3_apply_def_rule then
blanchet@56078
    35
      inline_z3_defs defs (map (replace_dependencies_in_line (name, [])) lines)
blanchet@56078
    36
    else
blanchet@56078
    37
      (name, role, Term.subst_atomic defs t, rule, deps) :: inline_z3_defs defs lines
blanchet@56078
    38
blanchet@56078
    39
fun add_z3_hypotheses [] = I
blanchet@56078
    40
  | add_z3_hypotheses hyps =
blanchet@56078
    41
    HOLogic.dest_Trueprop
blanchet@56078
    42
    #> curry s_imp (Library.foldr1 s_conj (map HOLogic.dest_Trueprop hyps))
blanchet@56078
    43
    #> HOLogic.mk_Trueprop
blanchet@56078
    44
blanchet@56078
    45
fun inline_z3_hypotheses _ _ [] = []
blanchet@56078
    46
  | inline_z3_hypotheses hyp_names hyps ((name, role, t, rule, deps) :: lines) =
blanchet@56078
    47
    if rule = z3_hypothesis_rule then
blanchet@56078
    48
      inline_z3_hypotheses (name :: hyp_names) (AList.map_default (op =) (t, []) (cons name) hyps)
blanchet@56078
    49
        lines
blanchet@56078
    50
    else
blanchet@56078
    51
      let val deps' = subtract (op =) hyp_names deps in
blanchet@56078
    52
        if rule = z3_lemma_rule then
blanchet@56078
    53
          (name, role, t, rule, deps') :: inline_z3_hypotheses hyp_names hyps lines
blanchet@56078
    54
        else
blanchet@56078
    55
          let
blanchet@56078
    56
            val add_hyps = filter_out (null o inter (op =) deps o snd) hyps
blanchet@56078
    57
            val t' = add_z3_hypotheses (map fst add_hyps) t
blanchet@56078
    58
            val deps' = subtract (op =) hyp_names deps
blanchet@56078
    59
            val hyps' = fold (AList.update (op =) o apsnd (insert (op =) name)) add_hyps hyps
blanchet@56078
    60
          in
blanchet@56078
    61
            (name, role, t', rule, deps') :: inline_z3_hypotheses hyp_names hyps' lines
blanchet@56078
    62
          end
blanchet@56078
    63
      end
blanchet@56078
    64
blanchet@56078
    65
fun simplify_prop (@{const Not} $ t) = s_not (simplify_prop t)
blanchet@56078
    66
  | simplify_prop (@{const conj} $ t $ u) = s_conj (simplify_prop t, simplify_prop u)
blanchet@56078
    67
  | simplify_prop (@{const disj} $ t $ u) = s_disj (simplify_prop t, simplify_prop u)
blanchet@56078
    68
  | simplify_prop (@{const implies} $ t $ u) = s_imp (simplify_prop t, simplify_prop u)
blanchet@56078
    69
  | simplify_prop (@{const HOL.eq (bool)} $ t $ u) = s_iff (simplify_prop t, simplify_prop u)
blanchet@56078
    70
  | simplify_prop (t $ u) = simplify_prop t $ simplify_prop u
blanchet@56078
    71
  | simplify_prop (Abs (s, T, t)) = Abs (s, T, simplify_prop t)
blanchet@56078
    72
  | simplify_prop t = t
blanchet@56078
    73
blanchet@56078
    74
fun simplify_line (name, role, t, rule, deps) = (name, role, simplify_prop t, rule, deps)
blanchet@56078
    75
blanchet@56078
    76
fun atp_proof_of_z3_proof thy proof =
blanchet@56078
    77
  let
blanchet@56078
    78
    fun step_name_of id = (string_of_int id, [])
blanchet@56078
    79
blanchet@56078
    80
    (* FIXME: find actual conjecture *)
blanchet@56078
    81
    val id_of_last_asserted =
blanchet@56078
    82
      proof
blanchet@56078
    83
      |> rev |> find_first (fn Z3_New_Proof.Z3_Step {rule, ...} => rule = Z3_New_Proof.Asserted)
blanchet@56078
    84
      |> Option.map (fn Z3_New_Proof.Z3_Step {id, ...} => id)
blanchet@56078
    85
blanchet@56078
    86
    fun step_of (Z3_New_Proof.Z3_Step {id, rule, prems, concl, ...}) =
blanchet@56078
    87
      let
blanchet@56078
    88
        val role =
blanchet@56078
    89
          (case rule of
blanchet@56078
    90
            Z3_New_Proof.Asserted =>
blanchet@56078
    91
              if id_of_last_asserted = SOME id then Negated_Conjecture else Hypothesis
blanchet@56078
    92
          | Z3_New_Proof.Rewrite => Lemma
blanchet@56078
    93
          | Z3_New_Proof.Rewrite_Star => Lemma
blanchet@56078
    94
          | Z3_New_Proof.Skolemize => Lemma
blanchet@56078
    95
          | Z3_New_Proof.Th_Lemma _ => Lemma
blanchet@56078
    96
          | _ => Plain)
blanchet@56078
    97
      in
blanchet@56078
    98
        (step_name_of id, role, HOLogic.mk_Trueprop (Object_Logic.atomize_term thy concl),
blanchet@56078
    99
         Z3_New_Proof.string_of_rule rule, map step_name_of prems)
blanchet@56078
   100
      end
blanchet@56078
   101
  in
blanchet@56078
   102
    proof
blanchet@56078
   103
    |> map step_of
blanchet@56078
   104
    |> inline_z3_defs []
blanchet@56078
   105
    |> inline_z3_hypotheses [] []
blanchet@56078
   106
    |> map simplify_line
blanchet@56078
   107
  end
blanchet@56078
   108
blanchet@56078
   109
end;