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