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