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
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@56981
    11
  val atp_proof_of_z3_proof: Proof.context -> thm list -> term list -> term -> int list -> int ->
blanchet@56981
    12
    (int * string) list -> Z3_New_Proof.z3_step list -> (term, string) atp_step list
blanchet@56078
    13
end;
blanchet@56078
    14
blanchet@56078
    15
structure Z3_New_Isar: Z3_NEW_ISAR =
blanchet@56078
    16
struct
blanchet@56078
    17
blanchet@56078
    18
open ATP_Util
blanchet@56078
    19
open ATP_Problem
blanchet@56078
    20
open ATP_Proof
blanchet@56078
    21
open ATP_Proof_Reconstruct
blanchet@56078
    22
blanchet@56078
    23
val z3_apply_def_rule = Z3_New_Proof.string_of_rule Z3_New_Proof.Apply_Def
blanchet@56078
    24
val z3_hypothesis_rule = Z3_New_Proof.string_of_rule Z3_New_Proof.Hypothesis
blanchet@56078
    25
val z3_intro_def_rule = Z3_New_Proof.string_of_rule Z3_New_Proof.Intro_Def
blanchet@56078
    26
val z3_lemma_rule = Z3_New_Proof.string_of_rule Z3_New_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@56855
    66
fun simplify_bool ((all as Const (@{const_name All}, _)) $ Abs (s, T, t)) =
blanchet@56855
    67
    let val t' = simplify_bool t in
blanchet@56855
    68
      if loose_bvar1 (t', 0) then all $ Abs (s, T, t') else t'
blanchet@56855
    69
    end
blanchet@56855
    70
  | simplify_bool (@{const Not} $ t) = s_not (simplify_bool t)
blanchet@56129
    71
  | simplify_bool (@{const conj} $ t $ u) = s_conj (simplify_bool t, simplify_bool u)
blanchet@56129
    72
  | simplify_bool (@{const disj} $ t $ u) = s_disj (simplify_bool t, simplify_bool u)
blanchet@56129
    73
  | simplify_bool (@{const implies} $ t $ u) = s_imp (simplify_bool t, simplify_bool u)
blanchet@56129
    74
  | simplify_bool (@{const HOL.eq (bool)} $ t $ u) = s_iff (simplify_bool t, simplify_bool u)
blanchet@56129
    75
  | simplify_bool (t as Const (@{const_name HOL.eq}, _) $ u $ v) =
blanchet@56126
    76
    if u aconv v then @{const True} else t
blanchet@56129
    77
  | simplify_bool (t $ u) = simplify_bool t $ simplify_bool u
blanchet@56129
    78
  | simplify_bool (Abs (s, T, t)) = Abs (s, T, simplify_bool t)
blanchet@56129
    79
  | simplify_bool t = t
blanchet@56078
    80
blanchet@56129
    81
(* It is not entirely clear why this should be necessary, especially for abstractions variables. *)
blanchet@56129
    82
val unskolemize_names =
blanchet@56129
    83
  Term.map_abs_vars (perhaps (try Name.dest_skolem))
blanchet@56129
    84
  #> Term.map_aterms (perhaps (try (fn Free (s, T) => Free (Name.dest_skolem s, T))))
blanchet@56078
    85
blanchet@56981
    86
fun atp_proof_of_z3_proof ctxt rewrite_rules hyp_ts concl_t prem_ids conjecture_id fact_ids proof =
blanchet@56078
    87
  let
blanchet@56981
    88
    val thy = Proof_Context.theory_of ctxt
blanchet@56981
    89
blanchet@56981
    90
    fun steps_of (Z3_New_Proof.Z3_Step {id, rule, prems, concl, ...}) =
blanchet@56078
    91
      let
blanchet@56099
    92
        fun step_name_of id = (string_of_int id, the_list (AList.lookup (op =) fact_ids id))
blanchet@56099
    93
blanchet@56981
    94
        val name as (sid, ss) = step_name_of id
blanchet@56128
    95
blanchet@56981
    96
        val concl' =
blanchet@56981
    97
          concl
blanchet@56128
    98
          |> Raw_Simplifier.rewrite_term thy rewrite_rules []
blanchet@56128
    99
          |> Object_Logic.atomize_term thy
blanchet@56129
   100
          |> simplify_bool
blanchet@56129
   101
          |> unskolemize_names
blanchet@56128
   102
          |> HOLogic.mk_Trueprop
blanchet@56981
   103
blanchet@56981
   104
        fun standard_step role =
blanchet@56981
   105
          (name, role, concl', Z3_New_Proof.string_of_rule rule, map step_name_of prems)
blanchet@56078
   106
      in
blanchet@56981
   107
        (case rule of
blanchet@56981
   108
          Z3_New_Proof.Asserted =>
blanchet@56981
   109
          let
blanchet@56981
   110
            val name0 = (sid ^ "a", ss)
blanchet@56981
   111
            val (role0, concl0) =
blanchet@56981
   112
              if not (null ss) then
blanchet@56981
   113
                (Axiom, concl(*FIXME*))
blanchet@56981
   114
              else if id = conjecture_id then
blanchet@56981
   115
                (Conjecture, concl_t)
blanchet@56981
   116
              else
blanchet@56981
   117
                (Hypothesis,
blanchet@56981
   118
                 (case find_index (curry (op =) id) prem_ids of
blanchet@56981
   119
                   ~1 => concl
blanchet@56981
   120
                 | i => nth hyp_ts i))
blanchet@56981
   121
blanchet@56981
   122
            val normalize_prems =
blanchet@56981
   123
              SMT2_Normalize.case_bool_entry :: SMT2_Normalize.special_quant_table @
blanchet@56981
   124
              SMT2_Normalize.abs_min_max_table
blanchet@56981
   125
              |> map_filter (fn (c, th) =>
blanchet@56981
   126
                if exists_Const (curry (op =) c o fst) concl0 then
blanchet@56981
   127
                  let val s = short_thm_name ctxt th in SOME (s, [s]) end
blanchet@56981
   128
                else
blanchet@56981
   129
                  NONE)
blanchet@56981
   130
          in
blanchet@56981
   131
            if null normalize_prems then
blanchet@56981
   132
              [(name, role0, concl0, Z3_New_Proof.string_of_rule rule, [])]
blanchet@56981
   133
            else
blanchet@56981
   134
              [(name0, role0, concl0, Z3_New_Proof.string_of_rule rule, []),
blanchet@56981
   135
               (name, Plain, concl', Z3_New_Proof.string_of_rule Z3_New_Proof.Rewrite,
blanchet@56981
   136
                name0 :: normalize_prems)]
blanchet@56981
   137
          end
blanchet@56981
   138
        | Z3_New_Proof.Rewrite => [standard_step Lemma]
blanchet@56981
   139
        | Z3_New_Proof.Rewrite_Star => [standard_step Lemma]
blanchet@56981
   140
        | Z3_New_Proof.Skolemize => [standard_step Lemma]
blanchet@56981
   141
        | Z3_New_Proof.Th_Lemma _ => [standard_step Lemma]
blanchet@56981
   142
        | _ => [standard_step Plain])
blanchet@56078
   143
      end
blanchet@56078
   144
  in
blanchet@56078
   145
    proof
blanchet@56981
   146
    |> maps steps_of
blanchet@56078
   147
    |> inline_z3_defs []
blanchet@56078
   148
    |> inline_z3_hypotheses [] []
blanchet@56078
   149
  end
blanchet@56078
   150
blanchet@56078
   151
end;