equal
deleted
inserted
replaced
1 (* Title: Tools/more_conv.ML |
|
2 Author: Sascha Boehme, TU Muenchen |
|
3 |
|
4 Further conversions and conversionals. |
|
5 *) |
|
6 |
|
7 signature MORE_CONV = |
|
8 sig |
|
9 val rewrs_conv: thm list -> conv |
|
10 |
|
11 val sub_conv: (Proof.context -> conv) -> Proof.context -> conv |
|
12 val bottom_conv: (Proof.context -> conv) -> Proof.context -> conv |
|
13 val top_conv: (Proof.context -> conv) -> Proof.context -> conv |
|
14 val top_sweep_conv: (Proof.context -> conv) -> Proof.context -> conv |
|
15 |
|
16 val binder_conv: (Proof.context -> conv) -> Proof.context -> conv |
|
17 end |
|
18 |
|
19 structure More_Conv : MORE_CONV = |
|
20 struct |
|
21 |
|
22 fun rewrs_conv eqs = Conv.first_conv (map Conv.rewr_conv eqs) |
|
23 |
|
24 |
|
25 fun sub_conv conv ctxt = |
|
26 Conv.comb_conv (conv ctxt) else_conv |
|
27 Conv.abs_conv (fn (_, cx) => conv cx) ctxt else_conv |
|
28 Conv.all_conv |
|
29 |
|
30 fun bottom_conv conv ctxt ct = |
|
31 (sub_conv (bottom_conv conv) ctxt then_conv conv ctxt) ct |
|
32 |
|
33 fun top_conv conv ctxt ct = |
|
34 (conv ctxt then_conv sub_conv (top_conv conv) ctxt) ct |
|
35 |
|
36 fun top_sweep_conv conv ctxt ct = |
|
37 (conv ctxt else_conv sub_conv (top_sweep_conv conv) ctxt) ct |
|
38 |
|
39 |
|
40 fun binder_conv cv ctxt = |
|
41 Conv.arg_conv (Conv.abs_conv (fn (_, cx) => cv cx) ctxt) |
|
42 |
|
43 end |
|