|
1 (* Title: nominal_thmdecls.ML |
|
2 Author: Brian Huffman, Christian Urban |
|
3 *) |
|
4 |
|
5 signature NOMINAL_PERMEQ = |
|
6 sig |
|
7 val eqvt_tac: Proof.context -> int -> tactic |
|
8 |
|
9 end; |
|
10 |
|
11 (* TODO: |
|
12 |
|
13 - provide a method interface with the usual add and del options |
|
14 |
|
15 - print a warning if for a constant no eqvt lemma is stored |
|
16 |
|
17 - there seems to be too much simplified in case of multiple |
|
18 permutations, like |
|
19 |
|
20 p o q o r o x |
|
21 |
|
22 we usually only want the outermost permutation to "float" in |
|
23 *) |
|
24 |
|
25 |
|
26 structure Nominal_Permeq: NOMINAL_PERMEQ = |
|
27 struct |
|
28 |
|
29 local |
|
30 |
|
31 fun eqvt_apply_conv ctxt ct = |
|
32 case (term_of ct) of |
|
33 (Const (@{const_name "permute"}, _) $ _ $ (_ $ _)) => |
|
34 let |
|
35 val (perm, t) = Thm.dest_comb ct |
|
36 val (_, p) = Thm.dest_comb perm |
|
37 val (f, x) = Thm.dest_comb t |
|
38 val a = ctyp_of_term x; |
|
39 val b = ctyp_of_term t; |
|
40 val ty_insts = map SOME [b, a] |
|
41 val term_insts = map SOME [p, f, x] |
|
42 in |
|
43 Drule.instantiate' ty_insts term_insts @{thm eqvt_apply} |
|
44 end |
|
45 | _ => Conv.no_conv ct |
|
46 |
|
47 fun eqvt_lambda_conv ctxt ct = |
|
48 case (term_of ct) of |
|
49 (Const (@{const_name "permute"}, _) $ _ $ Abs _) => |
|
50 Conv.rewr_conv @{thm eqvt_lambda} ct |
|
51 | _ => Conv.no_conv ct |
|
52 |
|
53 in |
|
54 |
|
55 fun eqvt_conv ctxt ct = |
|
56 Conv.first_conv |
|
57 [ Conv.rewr_conv @{thm eqvt_bound}, |
|
58 eqvt_apply_conv ctxt |
|
59 then_conv Conv.comb_conv (eqvt_conv ctxt), |
|
60 eqvt_lambda_conv ctxt |
|
61 then_conv Conv.abs_conv (fn (v, ctxt) => eqvt_conv ctxt) ctxt, |
|
62 More_Conv.rewrs_conv (Nominal_ThmDecls.get_eqvts_raw_thms ctxt), |
|
63 Conv.all_conv |
|
64 ] ct |
|
65 |
|
66 fun eqvt_tac ctxt = |
|
67 CONVERSION (More_Conv.bottom_conv (fn ctxt => eqvt_conv ctxt) ctxt) |
|
68 |
|
69 end |
|
70 |
|
71 end; (* structure *) |