author | blanchet |
Fri, 01 Aug 2014 14:43:57 +0200 | |
changeset 57743 | 0af2d5dfb0ac |
parent 57730 | d39815cdb7ba |
child 57745 | c65c116553b5 |
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 -> |
57730
d39815cdb7ba
remove lambda-lifting related assumptions from generated Isar proofs
blanchet
parents:
57714
diff
changeset
|
15 |
(''a * 'c) list -> 'c list -> 'c -> 'c -> (ATP_Problem.atp_formula_role * 'c) option |
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 unlift_term ll_defs = |
|
44 |
let |
|
45 |
val lifted = map (ATP_Util.extract_lambda_def dest_Free o ATP_Util.hol_open_form I) ll_defs |
|
46 |
||
47 |
fun un_free (t as Free (s, _)) = |
|
48 |
(case AList.lookup (op =) lifted s of |
|
49 |
SOME t => un_term t |
|
50 |
| NONE => t) |
|
51 |
| un_free t = t |
|
52 |
and un_term t = map_aterms un_free t |
|
53 |
in un_term end |
|
54 |
||
57714
4856a7b8b9c3
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents:
57710
diff
changeset
|
55 |
(* It is not entirely clear why this should be necessary, especially for abstractions variables. *) |
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
56 |
val unskolemize_names = |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
57 |
Term.map_abs_vars (perhaps (try Name.dest_skolem)) |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
58 |
#> 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
|
59 |
|
57704 | 60 |
fun postprocess_step_conclusion concl thy rewrite_rules ll_defs = |
61 |
concl |
|
62 |
|> Raw_Simplifier.rewrite_term thy rewrite_rules [] |
|
63 |
|> Object_Logic.atomize_term thy |
|
64 |
|> simplify_bool |
|
65 |
|> not (null ll_defs) ? unlift_term ll_defs |
|
66 |
|> unskolemize_names |
|
67 |
|> HOLogic.mk_Trueprop |
|
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
68 |
|> unskolemize_names |
57704 | 69 |
|
57705 | 70 |
fun normalizing_prems ctxt concl0 = |
57704 | 71 |
SMT2_Normalize.case_bool_entry :: SMT2_Normalize.special_quant_table @ |
72 |
SMT2_Normalize.abs_min_max_table |
|
73 |
|> map_filter (fn (c, th) => |
|
74 |
if exists_Const (curry (op =) c o fst) concl0 then |
|
75 |
let val s = short_thm_name ctxt th in SOME (s, [s]) end |
|
76 |
else |
|
77 |
NONE) |
|
78 |
||
79 |
fun distinguish_conjecture_and_hypothesis ss id conjecture_id prem_ids fact_helper_ts hyp_ts concl_t |
|
80 |
t = |
|
81 |
(case ss of |
|
57730
d39815cdb7ba
remove lambda-lifting related assumptions from generated Isar proofs
blanchet
parents:
57714
diff
changeset
|
82 |
[s] => SOME (Axiom, the (AList.lookup (op =) fact_helper_ts s)) |
57704 | 83 |
| _ => |
84 |
if id = conjecture_id then |
|
57730
d39815cdb7ba
remove lambda-lifting related assumptions from generated Isar proofs
blanchet
parents:
57714
diff
changeset
|
85 |
SOME (Conjecture, concl_t) |
57704 | 86 |
else |
57730
d39815cdb7ba
remove lambda-lifting related assumptions from generated Isar proofs
blanchet
parents:
57714
diff
changeset
|
87 |
(case find_index (curry (op =) id) prem_ids of |
d39815cdb7ba
remove lambda-lifting related assumptions from generated Isar proofs
blanchet
parents:
57714
diff
changeset
|
88 |
~1 => NONE (* lambda-lifting definition *) |
d39815cdb7ba
remove lambda-lifting related assumptions from generated Isar proofs
blanchet
parents:
57714
diff
changeset
|
89 |
| i => SOME (Hypothesis, nth hyp_ts i))) |
57704 | 90 |
|
91 |
end; |