57704
|
1 |
(* Title: HOL/Tools/SMT2/smtlib2_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 SMTLIB2_ISAR =
|
|
9 |
sig
|
|
10 |
val simplify_bool: term -> term
|
|
11 |
val unlift_term: term list -> term -> term
|
|
12 |
val postprocess_step_conclusion: term -> theory -> thm list -> term list -> term
|
57705
|
13 |
val normalizing_prems : Proof.context -> term -> (string * string list) list
|
57704
|
14 |
val distinguish_conjecture_and_hypothesis : ''a list -> ''b -> ''b -> ''b list ->
|
|
15 |
(''a * 'c) list -> 'c list -> 'c -> 'c -> ATP_Problem.atp_formula_role * 'c
|
|
16 |
end;
|
|
17 |
|
|
18 |
structure SMTLIB2_Isar: SMTLIB2_ISAR =
|
|
19 |
struct
|
|
20 |
|
|
21 |
open ATP_Problem
|
|
22 |
open ATP_Util
|
|
23 |
|
|
24 |
fun simplify_bool ((all as Const (@{const_name All}, _)) $ Abs (s, T, t)) =
|
|
25 |
let val t' = simplify_bool t in
|
|
26 |
if loose_bvar1 (t', 0) then all $ Abs (s, T, t') else t'
|
|
27 |
end
|
|
28 |
| simplify_bool (@{const Not} $ t) = s_not (simplify_bool t)
|
|
29 |
| simplify_bool (@{const conj} $ t $ u) = s_conj (simplify_bool t, simplify_bool u)
|
|
30 |
| simplify_bool (@{const disj} $ t $ u) = s_disj (simplify_bool t, simplify_bool u)
|
|
31 |
| simplify_bool (@{const implies} $ t $ u) = s_imp (simplify_bool t, simplify_bool u)
|
|
32 |
| simplify_bool (@{const HOL.eq (bool)} $ t $ u) = s_iff (simplify_bool t, simplify_bool u)
|
|
33 |
| simplify_bool (t as Const (@{const_name HOL.eq}, _) $ u $ v) =
|
|
34 |
if u aconv v then @{const True} else t
|
|
35 |
| simplify_bool (t $ u) = simplify_bool t $ simplify_bool u
|
|
36 |
| simplify_bool (Abs (s, T, t)) = Abs (s, T, simplify_bool t)
|
|
37 |
| simplify_bool t = t
|
|
38 |
|
|
39 |
fun strip_alls (Const (@{const_name All}, _) $ Abs (s, T, body)) = strip_alls body |>> cons (s, T)
|
|
40 |
| strip_alls t = ([], t)
|
|
41 |
|
|
42 |
fun push_skolem_all_under_iff t =
|
|
43 |
(case strip_alls t of
|
|
44 |
(qs as _ :: _,
|
|
45 |
(t0 as Const (@{const_name HOL.eq}, _)) $ (t1 as Const (@{const_name Ex}, _) $ _) $ t2) =>
|
|
46 |
t0 $ HOLogic.list_all (qs, t1) $ HOLogic.list_all (qs, t2)
|
|
47 |
| _ => t)
|
|
48 |
|
|
49 |
(* It is not entirely clear why this should be necessary, especially for abstractions variables. *)
|
|
50 |
val unskolemize_names =
|
|
51 |
Term.map_abs_vars (perhaps (try Name.dest_skolem))
|
|
52 |
#> Term.map_aterms (perhaps (try (fn Free (s, T) => Free (Name.dest_skolem s, T))))
|
|
53 |
|
|
54 |
fun unlift_term ll_defs =
|
|
55 |
let
|
|
56 |
val lifted = map (ATP_Util.extract_lambda_def dest_Free o ATP_Util.hol_open_form I) ll_defs
|
|
57 |
|
|
58 |
fun un_free (t as Free (s, _)) =
|
|
59 |
(case AList.lookup (op =) lifted s of
|
|
60 |
SOME t => un_term t
|
|
61 |
| NONE => t)
|
|
62 |
| un_free t = t
|
|
63 |
and un_term t = map_aterms un_free t
|
|
64 |
in un_term end
|
|
65 |
|
|
66 |
fun postprocess_step_conclusion concl thy rewrite_rules ll_defs =
|
|
67 |
concl
|
|
68 |
|> Raw_Simplifier.rewrite_term thy rewrite_rules []
|
|
69 |
|> Object_Logic.atomize_term thy
|
|
70 |
|> simplify_bool
|
|
71 |
|> not (null ll_defs) ? unlift_term ll_defs
|
|
72 |
|> unskolemize_names
|
|
73 |
|> push_skolem_all_under_iff
|
|
74 |
|> HOLogic.mk_Trueprop
|
|
75 |
|
57705
|
76 |
fun normalizing_prems ctxt concl0 =
|
57704
|
77 |
SMT2_Normalize.case_bool_entry :: SMT2_Normalize.special_quant_table @
|
|
78 |
SMT2_Normalize.abs_min_max_table
|
|
79 |
|> map_filter (fn (c, th) =>
|
|
80 |
if exists_Const (curry (op =) c o fst) concl0 then
|
|
81 |
let val s = short_thm_name ctxt th in SOME (s, [s]) end
|
|
82 |
else
|
|
83 |
NONE)
|
|
84 |
|
|
85 |
fun distinguish_conjecture_and_hypothesis ss id conjecture_id prem_ids fact_helper_ts hyp_ts concl_t
|
|
86 |
t =
|
|
87 |
(case ss of
|
|
88 |
[s] => (Axiom, the (AList.lookup (op =) fact_helper_ts s))
|
|
89 |
| _ =>
|
|
90 |
if id = conjecture_id then
|
|
91 |
(Conjecture, concl_t)
|
|
92 |
else
|
|
93 |
(Hypothesis,
|
|
94 |
(case find_index (curry (op =) id) prem_ids of
|
|
95 |
~1 => t
|
|
96 |
| i => nth hyp_ts i)))
|
|
97 |
|
|
98 |
end;
|