equal
deleted
inserted
replaced
1 (* Title: HOL/SMT/Tools/smt_additional_facts.ML |
|
2 Author: Sascha Boehme, TU Muenchen |
|
3 |
|
4 Include additional facts. |
|
5 *) |
|
6 |
|
7 signature SMT_ADDITIONAL_FACTS = |
|
8 sig |
|
9 val add_facts: thm list -> thm list |
|
10 end |
|
11 |
|
12 structure SMT_Additional_Facts: SMT_ADDITIONAL_FACTS = |
|
13 struct |
|
14 |
|
15 infix 2 ?? |
|
16 fun (ex ?? f) thms = if exists (ex o Thm.prop_of) thms then f thms else thms |
|
17 |
|
18 |
|
19 |
|
20 (* pairs *) |
|
21 |
|
22 val pair_rules = [@{thm fst_conv}, @{thm snd_conv}, @{thm pair_collapse}] |
|
23 |
|
24 val pair_type = (fn Type (@{type_name "*"}, _) => true | _ => false) |
|
25 val exists_pair_type = Term.exists_type (Term.exists_subtype pair_type) |
|
26 |
|
27 val add_pair_rules = exists_pair_type ?? append pair_rules |
|
28 |
|
29 |
|
30 |
|
31 (* function update *) |
|
32 |
|
33 val fun_upd_rules = [@{thm fun_upd_same}, @{thm fun_upd_apply}] |
|
34 |
|
35 val is_fun_upd = (fn Const (@{const_name fun_upd}, _) => true | _ => false) |
|
36 val exists_fun_upd = Term.exists_subterm is_fun_upd |
|
37 |
|
38 val add_fun_upd_rules = exists_fun_upd ?? append fun_upd_rules |
|
39 |
|
40 |
|
41 (* include additional facts *) |
|
42 |
|
43 val add_facts = add_pair_rules #> add_fun_upd_rules |
|
44 |
|
45 end |
|