|
(* Title: HOL/Tools/SMT/smtlib_isar.ML
Author: Jasmin Blanchette, TU Muenchen
Author: Mathias Fleury, ENS Rennes
General tools for Isar proof reconstruction.
*)
signature SMTLIB_ISAR =
sig
val unlift_term: term list -> term -> term
val postprocess_step_conclusion: Proof.context -> thm list -> term list -> term -> term
val normalizing_prems : Proof.context -> term -> (string * string list) list
val distinguish_conjecture_and_hypothesis : ''a list -> ''b -> ''b -> ''b list ->
(''a * term) list -> term list -> term -> (ATP_Problem.atp_formula_role * term) option
val unskolemize_names: Proof.context -> term -> term
end;
structure SMTLIB_Isar: SMTLIB_ISAR =
struct
open ATP_Util
open ATP_Problem
open ATP_Proof_Reconstruct
fun unlift_term ll_defs =
let
val lifted = map (ATP_Util.extract_lambda_def dest_Free o ATP_Util.hol_open_form I) ll_defs
fun un_free (t as Free (s, _)) =
(case AList.lookup (op =) lifted s of
SOME t => un_term t
| NONE => t)
| un_free t = t
and un_term t = map_aterms un_free t
in un_term end
(* Remove the "__" suffix for newly introduced variables (Skolems). It is not clear why "__" is
generated also for abstraction variables, but this is repaired here. *)
fun unskolemize_names ctxt =
Term.map_abs_vars (perhaps (try Name.dest_skolem))
#> Term.map_aterms (perhaps (try (fn Free (s, T) =>
Free (s |> not (Variable.is_fixed ctxt s) ? Name.dest_skolem, T))))
fun postprocess_step_conclusion ctxt rewrite_rules ll_defs =
let val thy = Proof_Context.theory_of ctxt in
Raw_Simplifier.rewrite_term thy rewrite_rules []
#> Object_Logic.atomize_term ctxt
#> not (null ll_defs) ? unlift_term ll_defs
#> simplify_bool
#> unskolemize_names ctxt
#> HOLogic.mk_Trueprop
end
fun normalizing_prems ctxt concl0 =
SMT_Normalize.case_bool_entry :: SMT_Normalize.special_quant_table @
SMT_Normalize.abs_min_max_table
|> map_filter (fn (c, th) =>
if exists_Const (curry (op =) c o fst) concl0 then
let val s = short_thm_name ctxt th in SOME (s, [s]) end
else
NONE)
fun distinguish_conjecture_and_hypothesis ss id conjecture_id prem_ids fact_helper_ts hyp_ts
concl_t =
(case ss of
[s] => SOME (Axiom, the (AList.lookup (op =) fact_helper_ts s))
| _ =>
if id = conjecture_id then
SOME (Conjecture, concl_t)
else
(case find_index (curry (op =) id) prem_ids of
~1 => NONE (* lambda-lifting definition *)
| i => SOME (Hypothesis, close_form (nth hyp_ts i))))
end;
¤ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
