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