1(*  Title:      HOL/Tools/SMT/smtlib_isar.ML
2    Author:     Jasmin Blanchette, TU Muenchen
3    Author:     Mathias Fleury, ENS Rennes
4
5General tools for Isar proof reconstruction.
6*)
7
8signature SMTLIB_ISAR =
9sig
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
16end;
17
18structure SMTLIB_Isar: SMTLIB_ISAR =
19struct
20
21open ATP_Util
22open ATP_Problem
23open ATP_Proof_Reconstruct
24
25fun 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. *)
39fun 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
44fun 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
54fun 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
63fun 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
75end;
76