src/HOL/Tools/SMT2/z3_new_isar.ML
author blanchet
Thu, 10 Jul 2014 18:08:21 +0200
changeset 57541 147e3f1e0459
parent 57289 5483868da0d8
child 57704 c0da3fc313e3
permissions -rw-r--r--
lambda-lifting for Z3 Isar proofs
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
     1
(*  Title:      HOL/Tools/SMT2/z3_new_isar.ML
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
     2
    Author:     Jasmin Blanchette, TU Muenchen
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
     3
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
     4
Z3 proofs as generic ATP proofs for Isar proof reconstruction.
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
     5
*)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
     6
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
     7
signature Z3_NEW_ISAR =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
     8
sig
57541
147e3f1e0459 lambda-lifting for Z3 Isar proofs
blanchet
parents: 57289
diff changeset
     9
  val atp_proof_of_z3_proof: Proof.context -> term list -> thm list -> term list -> term ->
56985
82c83978fbd9 correctly add extra facts to lemmas (cf. conjecture and hypotheses) in Z3 Isar proofs
blanchet
parents: 56981
diff changeset
    10
    (string * term) list -> int list -> int -> (int * string) list -> Z3_New_Proof.z3_step list ->
57159
24cbdebba35a refactored Z3 to Isar proof construction code
blanchet
parents: 57056
diff changeset
    11
    (term, string) ATP_Proof.atp_step list
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    12
end;
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    13
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    14
structure Z3_New_Isar: Z3_NEW_ISAR =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    15
struct
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    16
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    17
open ATP_Util
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    18
open ATP_Problem
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    19
open ATP_Proof
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    20
open ATP_Proof_Reconstruct
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    21
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    22
val z3_apply_def_rule = Z3_New_Proof.string_of_rule Z3_New_Proof.Apply_Def
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    23
val z3_hypothesis_rule = Z3_New_Proof.string_of_rule Z3_New_Proof.Hypothesis
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    24
val z3_intro_def_rule = Z3_New_Proof.string_of_rule Z3_New_Proof.Intro_Def
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    25
val z3_lemma_rule = Z3_New_Proof.string_of_rule Z3_New_Proof.Lemma
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    26
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    27
fun inline_z3_defs _ [] = []
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    28
  | inline_z3_defs defs ((name, role, t, rule, deps) :: lines) =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    29
    if rule = z3_intro_def_rule then
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    30
      let val def = t |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> swap in
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    31
        inline_z3_defs (insert (op =) def defs)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    32
          (map (replace_dependencies_in_line (name, [])) lines)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    33
      end
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    34
    else if rule = z3_apply_def_rule then
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    35
      inline_z3_defs defs (map (replace_dependencies_in_line (name, [])) lines)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    36
    else
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    37
      (name, role, Term.subst_atomic defs t, rule, deps) :: inline_z3_defs defs lines
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    38
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    39
fun add_z3_hypotheses [] = I
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    40
  | add_z3_hypotheses hyps =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    41
    HOLogic.dest_Trueprop
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    42
    #> curry s_imp (Library.foldr1 s_conj (map HOLogic.dest_Trueprop hyps))
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    43
    #> HOLogic.mk_Trueprop
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    44
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    45
fun inline_z3_hypotheses _ _ [] = []
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    46
  | inline_z3_hypotheses hyp_names hyps ((name, role, t, rule, deps) :: lines) =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    47
    if rule = z3_hypothesis_rule then
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    48
      inline_z3_hypotheses (name :: hyp_names) (AList.map_default (op =) (t, []) (cons name) hyps)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    49
        lines
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    50
    else
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    51
      let val deps' = subtract (op =) hyp_names deps in
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    52
        if rule = z3_lemma_rule then
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    53
          (name, role, t, rule, deps') :: inline_z3_hypotheses hyp_names hyps lines
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    54
        else
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    55
          let
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    56
            val add_hyps = filter_out (null o inter (op =) deps o snd) hyps
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    57
            val t' = add_z3_hypotheses (map fst add_hyps) t
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    58
            val deps' = subtract (op =) hyp_names deps
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    59
            val hyps' = fold (AList.update (op =) o apsnd (insert (op =) name)) add_hyps hyps
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    60
          in
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    61
            (name, role, t', rule, deps') :: inline_z3_hypotheses hyp_names hyps' lines
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    62
          end
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    63
      end
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    64
56855
e7a55d295b8e simplify unused universally quantified variables in Z3 proofs
blanchet
parents: 56129
diff changeset
    65
fun simplify_bool ((all as Const (@{const_name All}, _)) $ Abs (s, T, t)) =
e7a55d295b8e simplify unused universally quantified variables in Z3 proofs
blanchet
parents: 56129
diff changeset
    66
    let val t' = simplify_bool t in
e7a55d295b8e simplify unused universally quantified variables in Z3 proofs
blanchet
parents: 56129
diff changeset
    67
      if loose_bvar1 (t', 0) then all $ Abs (s, T, t') else t'
e7a55d295b8e simplify unused universally quantified variables in Z3 proofs
blanchet
parents: 56129
diff changeset
    68
    end
e7a55d295b8e simplify unused universally quantified variables in Z3 proofs
blanchet
parents: 56129
diff changeset
    69
  | simplify_bool (@{const Not} $ t) = s_not (simplify_bool t)
56129
9ee083f9da5b remove '__' skolem suffixes before showing terms to users
blanchet
parents: 56128
diff changeset
    70
  | simplify_bool (@{const conj} $ t $ u) = s_conj (simplify_bool t, simplify_bool u)
9ee083f9da5b remove '__' skolem suffixes before showing terms to users
blanchet
parents: 56128
diff changeset
    71
  | simplify_bool (@{const disj} $ t $ u) = s_disj (simplify_bool t, simplify_bool u)
9ee083f9da5b remove '__' skolem suffixes before showing terms to users
blanchet
parents: 56128
diff changeset
    72
  | simplify_bool (@{const implies} $ t $ u) = s_imp (simplify_bool t, simplify_bool u)
9ee083f9da5b remove '__' skolem suffixes before showing terms to users
blanchet
parents: 56128
diff changeset
    73
  | simplify_bool (@{const HOL.eq (bool)} $ t $ u) = s_iff (simplify_bool t, simplify_bool u)
9ee083f9da5b remove '__' skolem suffixes before showing terms to users
blanchet
parents: 56128
diff changeset
    74
  | simplify_bool (t as Const (@{const_name HOL.eq}, _) $ u $ v) =
56126
fc937e7ef4c6 more simplification of trivial steps
blanchet
parents: 56104
diff changeset
    75
    if u aconv v then @{const True} else t
56129
9ee083f9da5b remove '__' skolem suffixes before showing terms to users
blanchet
parents: 56128
diff changeset
    76
  | simplify_bool (t $ u) = simplify_bool t $ simplify_bool u
9ee083f9da5b remove '__' skolem suffixes before showing terms to users
blanchet
parents: 56128
diff changeset
    77
  | simplify_bool (Abs (s, T, t)) = Abs (s, T, simplify_bool t)
9ee083f9da5b remove '__' skolem suffixes before showing terms to users
blanchet
parents: 56128
diff changeset
    78
  | simplify_bool t = t
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    79
56129
9ee083f9da5b remove '__' skolem suffixes before showing terms to users
blanchet
parents: 56128
diff changeset
    80
(* It is not entirely clear why this should be necessary, especially for abstractions variables. *)
9ee083f9da5b remove '__' skolem suffixes before showing terms to users
blanchet
parents: 56128
diff changeset
    81
val unskolemize_names =
9ee083f9da5b remove '__' skolem suffixes before showing terms to users
blanchet
parents: 56128
diff changeset
    82
  Term.map_abs_vars (perhaps (try Name.dest_skolem))
9ee083f9da5b remove '__' skolem suffixes before showing terms to users
blanchet
parents: 56128
diff changeset
    83
  #> Term.map_aterms (perhaps (try (fn Free (s, T) => Free (Name.dest_skolem s, T))))
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
    84
57289
5483868da0d8 help reconstruction of Z3 skolemization by weakening formulas a bit
blanchet
parents: 57218
diff changeset
    85
fun strip_alls (Const (@{const_name All}, _) $ Abs (s, T, body)) = strip_alls body |>> cons (s, T)
5483868da0d8 help reconstruction of Z3 skolemization by weakening formulas a bit
blanchet
parents: 57218
diff changeset
    86
  | strip_alls t = ([], t)
5483868da0d8 help reconstruction of Z3 skolemization by weakening formulas a bit
blanchet
parents: 57218
diff changeset
    87
5483868da0d8 help reconstruction of Z3 skolemization by weakening formulas a bit
blanchet
parents: 57218
diff changeset
    88
fun push_skolem_all_under_iff t =
5483868da0d8 help reconstruction of Z3 skolemization by weakening formulas a bit
blanchet
parents: 57218
diff changeset
    89
  (case strip_alls t of
5483868da0d8 help reconstruction of Z3 skolemization by weakening formulas a bit
blanchet
parents: 57218
diff changeset
    90
    (qs as _ :: _,
5483868da0d8 help reconstruction of Z3 skolemization by weakening formulas a bit
blanchet
parents: 57218
diff changeset
    91
     (t0 as Const (@{const_name HOL.eq}, _)) $ (t1 as Const (@{const_name Ex}, _) $ _) $ t2) =>
5483868da0d8 help reconstruction of Z3 skolemization by weakening formulas a bit
blanchet
parents: 57218
diff changeset
    92
    t0 $ HOLogic.list_all (qs, t1) $ HOLogic.list_all (qs, t2)
5483868da0d8 help reconstruction of Z3 skolemization by weakening formulas a bit
blanchet
parents: 57218
diff changeset
    93
  | _ => t)
5483868da0d8 help reconstruction of Z3 skolemization by weakening formulas a bit
blanchet
parents: 57218
diff changeset
    94
57541
147e3f1e0459 lambda-lifting for Z3 Isar proofs
blanchet
parents: 57289
diff changeset
    95
fun unlift_term ll_defs =
147e3f1e0459 lambda-lifting for Z3 Isar proofs
blanchet
parents: 57289
diff changeset
    96
  let
147e3f1e0459 lambda-lifting for Z3 Isar proofs
blanchet
parents: 57289
diff changeset
    97
    val lifted = map (ATP_Util.extract_lambda_def dest_Free o ATP_Util.hol_open_form I) ll_defs
147e3f1e0459 lambda-lifting for Z3 Isar proofs
blanchet
parents: 57289
diff changeset
    98
147e3f1e0459 lambda-lifting for Z3 Isar proofs
blanchet
parents: 57289
diff changeset
    99
    fun un_free (t as Free (s, _)) =
147e3f1e0459 lambda-lifting for Z3 Isar proofs
blanchet
parents: 57289
diff changeset
   100
       (case AList.lookup (op =) lifted s of
147e3f1e0459 lambda-lifting for Z3 Isar proofs
blanchet
parents: 57289
diff changeset
   101
         SOME t => un_term t
147e3f1e0459 lambda-lifting for Z3 Isar proofs
blanchet
parents: 57289
diff changeset
   102
       | NONE => t)
147e3f1e0459 lambda-lifting for Z3 Isar proofs
blanchet
parents: 57289
diff changeset
   103
     | un_free t = t
147e3f1e0459 lambda-lifting for Z3 Isar proofs
blanchet
parents: 57289
diff changeset
   104
    and un_term t = map_aterms un_free t
147e3f1e0459 lambda-lifting for Z3 Isar proofs
blanchet
parents: 57289
diff changeset
   105
  in un_term end
147e3f1e0459 lambda-lifting for Z3 Isar proofs
blanchet
parents: 57289
diff changeset
   106
147e3f1e0459 lambda-lifting for Z3 Isar proofs
blanchet
parents: 57289
diff changeset
   107
fun atp_proof_of_z3_proof ctxt ll_defs rewrite_rules hyp_ts concl_t fact_helper_ts prem_ids
147e3f1e0459 lambda-lifting for Z3 Isar proofs
blanchet
parents: 57289
diff changeset
   108
    conjecture_id fact_helper_ids proof =
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   109
  let
56981
3ef45ce002b5 honor original format of conjecture or hypotheses in Z3-to-Isar proofs
blanchet
parents: 56855
diff changeset
   110
    val thy = Proof_Context.theory_of ctxt
3ef45ce002b5 honor original format of conjecture or hypotheses in Z3-to-Isar proofs
blanchet
parents: 56855
diff changeset
   111
57541
147e3f1e0459 lambda-lifting for Z3 Isar proofs
blanchet
parents: 57289
diff changeset
   112
    val unlift_term = unlift_term ll_defs
147e3f1e0459 lambda-lifting for Z3 Isar proofs
blanchet
parents: 57289
diff changeset
   113
56981
3ef45ce002b5 honor original format of conjecture or hypotheses in Z3-to-Isar proofs
blanchet
parents: 56855
diff changeset
   114
    fun steps_of (Z3_New_Proof.Z3_Step {id, rule, prems, concl, ...}) =
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   115
      let
56985
82c83978fbd9 correctly add extra facts to lemmas (cf. conjecture and hypotheses) in Z3 Isar proofs
blanchet
parents: 56981
diff changeset
   116
        val sid = string_of_int id
56128
c106ac2ff76d undo rewrite rules (e.g. for 'fun_app') in Isar
blanchet
parents: 56126
diff changeset
   117
56981
3ef45ce002b5 honor original format of conjecture or hypotheses in Z3-to-Isar proofs
blanchet
parents: 56855
diff changeset
   118
        val concl' =
3ef45ce002b5 honor original format of conjecture or hypotheses in Z3-to-Isar proofs
blanchet
parents: 56855
diff changeset
   119
          concl
56128
c106ac2ff76d undo rewrite rules (e.g. for 'fun_app') in Isar
blanchet
parents: 56126
diff changeset
   120
          |> Raw_Simplifier.rewrite_term thy rewrite_rules []
c106ac2ff76d undo rewrite rules (e.g. for 'fun_app') in Isar
blanchet
parents: 56126
diff changeset
   121
          |> Object_Logic.atomize_term thy
56129
9ee083f9da5b remove '__' skolem suffixes before showing terms to users
blanchet
parents: 56128
diff changeset
   122
          |> simplify_bool
57541
147e3f1e0459 lambda-lifting for Z3 Isar proofs
blanchet
parents: 57289
diff changeset
   123
          |> not (null ll_defs) ? unlift_term
56129
9ee083f9da5b remove '__' skolem suffixes before showing terms to users
blanchet
parents: 56128
diff changeset
   124
          |> unskolemize_names
57289
5483868da0d8 help reconstruction of Z3 skolemization by weakening formulas a bit
blanchet
parents: 57218
diff changeset
   125
          |> push_skolem_all_under_iff
56128
c106ac2ff76d undo rewrite rules (e.g. for 'fun_app') in Isar
blanchet
parents: 56126
diff changeset
   126
          |> HOLogic.mk_Trueprop
56981
3ef45ce002b5 honor original format of conjecture or hypotheses in Z3-to-Isar proofs
blanchet
parents: 56855
diff changeset
   127
3ef45ce002b5 honor original format of conjecture or hypotheses in Z3-to-Isar proofs
blanchet
parents: 56855
diff changeset
   128
        fun standard_step role =
56985
82c83978fbd9 correctly add extra facts to lemmas (cf. conjecture and hypotheses) in Z3 Isar proofs
blanchet
parents: 56981
diff changeset
   129
          ((sid, []), role, concl', Z3_New_Proof.string_of_rule rule,
82c83978fbd9 correctly add extra facts to lemmas (cf. conjecture and hypotheses) in Z3 Isar proofs
blanchet
parents: 56981
diff changeset
   130
           map (fn id => (string_of_int id, [])) prems)
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   131
      in
56981
3ef45ce002b5 honor original format of conjecture or hypotheses in Z3-to-Isar proofs
blanchet
parents: 56855
diff changeset
   132
        (case rule of
3ef45ce002b5 honor original format of conjecture or hypotheses in Z3-to-Isar proofs
blanchet
parents: 56855
diff changeset
   133
          Z3_New_Proof.Asserted =>
3ef45ce002b5 honor original format of conjecture or hypotheses in Z3-to-Isar proofs
blanchet
parents: 56855
diff changeset
   134
          let
57056
8b2283566f6e properly reconstruct helpers in Z3 proofs
blanchet
parents: 56985
diff changeset
   135
            val ss = the_list (AList.lookup (op =) fact_helper_ids id)
56981
3ef45ce002b5 honor original format of conjecture or hypotheses in Z3-to-Isar proofs
blanchet
parents: 56855
diff changeset
   136
            val name0 = (sid ^ "a", ss)
56985
82c83978fbd9 correctly add extra facts to lemmas (cf. conjecture and hypotheses) in Z3 Isar proofs
blanchet
parents: 56981
diff changeset
   137
56981
3ef45ce002b5 honor original format of conjecture or hypotheses in Z3-to-Isar proofs
blanchet
parents: 56855
diff changeset
   138
            val (role0, concl0) =
56985
82c83978fbd9 correctly add extra facts to lemmas (cf. conjecture and hypotheses) in Z3 Isar proofs
blanchet
parents: 56981
diff changeset
   139
              (case ss of
57056
8b2283566f6e properly reconstruct helpers in Z3 proofs
blanchet
parents: 56985
diff changeset
   140
                [s] => (Axiom, the (AList.lookup (op =) fact_helper_ts s))
56985
82c83978fbd9 correctly add extra facts to lemmas (cf. conjecture and hypotheses) in Z3 Isar proofs
blanchet
parents: 56981
diff changeset
   141
              | _ =>
82c83978fbd9 correctly add extra facts to lemmas (cf. conjecture and hypotheses) in Z3 Isar proofs
blanchet
parents: 56981
diff changeset
   142
                if id = conjecture_id then
82c83978fbd9 correctly add extra facts to lemmas (cf. conjecture and hypotheses) in Z3 Isar proofs
blanchet
parents: 56981
diff changeset
   143
                  (Conjecture, concl_t)
82c83978fbd9 correctly add extra facts to lemmas (cf. conjecture and hypotheses) in Z3 Isar proofs
blanchet
parents: 56981
diff changeset
   144
                else
82c83978fbd9 correctly add extra facts to lemmas (cf. conjecture and hypotheses) in Z3 Isar proofs
blanchet
parents: 56981
diff changeset
   145
                  (Hypothesis,
82c83978fbd9 correctly add extra facts to lemmas (cf. conjecture and hypotheses) in Z3 Isar proofs
blanchet
parents: 56981
diff changeset
   146
                   (case find_index (curry (op =) id) prem_ids of
82c83978fbd9 correctly add extra facts to lemmas (cf. conjecture and hypotheses) in Z3 Isar proofs
blanchet
parents: 56981
diff changeset
   147
                     ~1 => concl
82c83978fbd9 correctly add extra facts to lemmas (cf. conjecture and hypotheses) in Z3 Isar proofs
blanchet
parents: 56981
diff changeset
   148
                   | i => nth hyp_ts i)))
56981
3ef45ce002b5 honor original format of conjecture or hypotheses in Z3-to-Isar proofs
blanchet
parents: 56855
diff changeset
   149
3ef45ce002b5 honor original format of conjecture or hypotheses in Z3-to-Isar proofs
blanchet
parents: 56855
diff changeset
   150
            val normalize_prems =
3ef45ce002b5 honor original format of conjecture or hypotheses in Z3-to-Isar proofs
blanchet
parents: 56855
diff changeset
   151
              SMT2_Normalize.case_bool_entry :: SMT2_Normalize.special_quant_table @
3ef45ce002b5 honor original format of conjecture or hypotheses in Z3-to-Isar proofs
blanchet
parents: 56855
diff changeset
   152
              SMT2_Normalize.abs_min_max_table
3ef45ce002b5 honor original format of conjecture or hypotheses in Z3-to-Isar proofs
blanchet
parents: 56855
diff changeset
   153
              |> map_filter (fn (c, th) =>
3ef45ce002b5 honor original format of conjecture or hypotheses in Z3-to-Isar proofs
blanchet
parents: 56855
diff changeset
   154
                if exists_Const (curry (op =) c o fst) concl0 then
3ef45ce002b5 honor original format of conjecture or hypotheses in Z3-to-Isar proofs
blanchet
parents: 56855
diff changeset
   155
                  let val s = short_thm_name ctxt th in SOME (s, [s]) end
3ef45ce002b5 honor original format of conjecture or hypotheses in Z3-to-Isar proofs
blanchet
parents: 56855
diff changeset
   156
                else
3ef45ce002b5 honor original format of conjecture or hypotheses in Z3-to-Isar proofs
blanchet
parents: 56855
diff changeset
   157
                  NONE)
3ef45ce002b5 honor original format of conjecture or hypotheses in Z3-to-Isar proofs
blanchet
parents: 56855
diff changeset
   158
          in
57218
7e90e30822a9 simplify slightly ATP proof generated for Z3
blanchet
parents: 57159
diff changeset
   159
            (if role0 = Axiom then []
7e90e30822a9 simplify slightly ATP proof generated for Z3
blanchet
parents: 57159
diff changeset
   160
             else [(name0, role0, concl0, Z3_New_Proof.string_of_rule rule, [])]) @
7e90e30822a9 simplify slightly ATP proof generated for Z3
blanchet
parents: 57159
diff changeset
   161
            [((sid, []), Plain, concl', Z3_New_Proof.string_of_rule Z3_New_Proof.Rewrite,
56985
82c83978fbd9 correctly add extra facts to lemmas (cf. conjecture and hypotheses) in Z3 Isar proofs
blanchet
parents: 56981
diff changeset
   162
              name0 :: normalize_prems)]
56981
3ef45ce002b5 honor original format of conjecture or hypotheses in Z3-to-Isar proofs
blanchet
parents: 56855
diff changeset
   163
          end
3ef45ce002b5 honor original format of conjecture or hypotheses in Z3-to-Isar proofs
blanchet
parents: 56855
diff changeset
   164
        | Z3_New_Proof.Rewrite => [standard_step Lemma]
3ef45ce002b5 honor original format of conjecture or hypotheses in Z3-to-Isar proofs
blanchet
parents: 56855
diff changeset
   165
        | Z3_New_Proof.Rewrite_Star => [standard_step Lemma]
3ef45ce002b5 honor original format of conjecture or hypotheses in Z3-to-Isar proofs
blanchet
parents: 56855
diff changeset
   166
        | Z3_New_Proof.Skolemize => [standard_step Lemma]
3ef45ce002b5 honor original format of conjecture or hypotheses in Z3-to-Isar proofs
blanchet
parents: 56855
diff changeset
   167
        | Z3_New_Proof.Th_Lemma _ => [standard_step Lemma]
3ef45ce002b5 honor original format of conjecture or hypotheses in Z3-to-Isar proofs
blanchet
parents: 56855
diff changeset
   168
        | _ => [standard_step Plain])
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   169
      end
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   170
  in
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   171
    proof
56981
3ef45ce002b5 honor original format of conjecture or hypotheses in Z3-to-Isar proofs
blanchet
parents: 56855
diff changeset
   172
    |> maps steps_of
56078
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   173
    |> inline_z3_defs []
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   174
    |> inline_z3_hypotheses [] []
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   175
  end
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   176
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff changeset
   177
end;