src/HOL/Tools/SMT/smtlib_isar.ML
author nipkow
Wed Jan 10 15:25:09 2018 +0100 (19 months ago)
changeset 67399 eab6ce8368fa
parent 59970 e9f73d87d904
permissions -rw-r--r--
ran isabelle update_op on all sources
     1 (*  Title:      HOL/Tools/SMT/smtlib_isar.ML
     2     Author:     Jasmin Blanchette, TU Muenchen
     3     Author:     Mathias Fleury, ENS Rennes
     4 
     5 General tools for Isar proof reconstruction.
     6 *)
     7 
     8 signature SMTLIB_ISAR =
     9 sig
    10   val unlift_term: term list -> term -> term
    11   val postprocess_step_conclusion: Proof.context -> thm list -> term list -> term -> term
    12   val normalizing_prems : Proof.context -> term -> (string * string list) list
    13   val distinguish_conjecture_and_hypothesis : ''a list -> ''b -> ''b -> ''b list ->
    14     (''a * term) list -> term list -> term -> (ATP_Problem.atp_formula_role * term) option
    15   val unskolemize_names: Proof.context -> term -> term
    16 end;
    17 
    18 structure SMTLIB_Isar: SMTLIB_ISAR =
    19 struct
    20 
    21 open ATP_Util
    22 open ATP_Problem
    23 open ATP_Proof_Reconstruct
    24 
    25 fun unlift_term ll_defs =
    26   let
    27     val lifted = map (ATP_Util.extract_lambda_def dest_Free o ATP_Util.hol_open_form I) ll_defs
    28 
    29     fun un_free (t as Free (s, _)) =
    30        (case AList.lookup (op =) lifted s of
    31          SOME t => un_term t
    32        | NONE => t)
    33      | un_free t = t
    34     and un_term t = map_aterms un_free t
    35   in un_term end
    36 
    37 (* Remove the "__" suffix for newly introduced variables (Skolems). It is not clear why "__" is
    38    generated also for abstraction variables, but this is repaired here. *)
    39 fun unskolemize_names ctxt =
    40   Term.map_abs_vars (perhaps (try Name.dest_skolem))
    41   #> Term.map_aterms (perhaps (try (fn Free (s, T) =>
    42     Free (s |> not (Variable.is_fixed ctxt s) ? Name.dest_skolem, T))))
    43 
    44 fun postprocess_step_conclusion ctxt rewrite_rules ll_defs =
    45   let val thy = Proof_Context.theory_of ctxt in
    46     Raw_Simplifier.rewrite_term thy rewrite_rules []
    47     #> Object_Logic.atomize_term ctxt
    48     #> not (null ll_defs) ? unlift_term ll_defs
    49     #> simplify_bool
    50     #> unskolemize_names ctxt
    51     #> HOLogic.mk_Trueprop
    52   end
    53 
    54 fun normalizing_prems ctxt concl0 =
    55   SMT_Normalize.case_bool_entry :: SMT_Normalize.special_quant_table @
    56   SMT_Normalize.abs_min_max_table
    57   |> map_filter (fn (c, th) =>
    58     if exists_Const (curry (op =) c o fst) concl0 then
    59       let val s = short_thm_name ctxt th in SOME (s, [s]) end
    60     else
    61       NONE)
    62 
    63 fun distinguish_conjecture_and_hypothesis ss id conjecture_id prem_ids fact_helper_ts hyp_ts
    64     concl_t =
    65   (case ss of
    66     [s] => SOME (Axiom, the (AList.lookup (op =) fact_helper_ts s))
    67   | _ =>
    68     if id = conjecture_id then
    69       SOME (Conjecture, concl_t)
    70     else
    71      (case find_index (curry (op =) id) prem_ids of
    72        ~1 => NONE (* lambda-lifting definition *)
    73      | i => SOME (Hypothesis, close_form (nth hyp_ts i))))
    74 
    75 end;