2 Author: Brian Huffman, Christian Urban |
2 Author: Brian Huffman, Christian Urban |
3 *) |
3 *) |
4 |
4 |
5 signature NOMINAL_PERMEQ = |
5 signature NOMINAL_PERMEQ = |
6 sig |
6 sig |
7 val eqvt_tac: Proof.context -> int -> tactic |
7 val eqvt_tac: Proof.context -> thm list -> int -> tactic |
8 |
8 val trace_eqvt: bool Config.T |
|
9 val setup: theory -> theory |
9 end; |
10 end; |
10 |
11 |
11 (* TODO: |
12 (* TODO: |
12 |
13 |
13 - provide a method interface with the usual add and del options |
14 - provide a method interface with the usual add and del options |
14 |
15 |
15 - print a warning if for a constant no eqvt lemma is stored |
16 - print a warning if for a constant no eqvt lemma is stored |
16 |
17 |
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 *) |
18 *) |
24 |
19 |
25 |
20 |
26 structure Nominal_Permeq: NOMINAL_PERMEQ = |
21 structure Nominal_Permeq: NOMINAL_PERMEQ = |
27 struct |
22 struct |
28 |
23 |
29 local |
24 fun is_head_Trueprop trm = |
|
25 case (head_of trm) of |
|
26 @{const "Trueprop"} => true |
|
27 | _ => false |
30 |
28 |
|
29 (* debugging infrastructure *) |
|
30 val (trace_eqvt, trace_eqvt_setup) = Attrib.config_bool "trace_eqvt" (K false); |
|
31 |
|
32 fun trace_enabled ctxt = Config.get ctxt trace_eqvt |
|
33 |
|
34 fun trace_conv ctxt conv ct = |
|
35 let |
|
36 val result = conv ct |
|
37 val _ = |
|
38 if trace_enabled ctxt andalso not (Thm.is_reflexive result) |
|
39 then |
|
40 let |
|
41 val lhs_str = Syntax.string_of_term ctxt (term_of (Thm.lhs_of result)) |
|
42 val rhs_str = Syntax.string_of_term ctxt (term_of (Thm.rhs_of result)) |
|
43 in |
|
44 warning (Pretty.string_of (Pretty.strs ["Rewriting", lhs_str, "to", rhs_str])) |
|
45 end |
|
46 else () |
|
47 in |
|
48 result |
|
49 end; |
|
50 |
|
51 (* conversion for applications *) |
31 fun eqvt_apply_conv ctxt ct = |
52 fun eqvt_apply_conv ctxt ct = |
32 case (term_of ct) of |
53 case (term_of ct) of |
33 (Const (@{const_name "permute"}, _) $ _ $ (_ $ _)) => |
54 (Const (@{const_name "permute"}, _) $ _ $ (_ $ _)) => |
34 let |
55 let |
35 val (perm, t) = Thm.dest_comb ct |
56 val (perm, t) = Thm.dest_comb ct |
36 val (_, p) = Thm.dest_comb perm |
57 val (_, p) = Thm.dest_comb perm |
37 val (f, x) = Thm.dest_comb t |
58 val (f, x) = Thm.dest_comb t |
38 val a = ctyp_of_term x; |
59 val a = ctyp_of_term x; |
39 val b = ctyp_of_term t; |
60 val b = ctyp_of_term t; |
40 val ty_insts = map SOME [b, a] |
61 val ty_insts = map SOME [b, a] |
41 val term_insts = map SOME [p, f, x] |
62 val term_insts = map SOME [p, f, x] |
42 in |
63 in |
43 Drule.instantiate' ty_insts term_insts @{thm eqvt_apply} |
64 Drule.instantiate' ty_insts term_insts @{thm eqvt_apply} |
44 end |
65 end |
45 | _ => Conv.no_conv ct |
66 | _ => Conv.no_conv ct |
46 |
67 |
|
68 (* conversion for lambdas *) |
47 fun eqvt_lambda_conv ctxt ct = |
69 fun eqvt_lambda_conv ctxt ct = |
48 case (term_of ct) of |
70 case (term_of ct) of |
49 (Const (@{const_name "permute"}, _) $ _ $ Abs _) => |
71 (Const (@{const_name "permute"}, _) $ _ $ Abs _) => |
50 Conv.rewr_conv @{thm eqvt_lambda} ct |
72 Conv.rewr_conv @{thm eqvt_lambda} ct |
51 | _ => Conv.no_conv ct |
73 | _ => Conv.no_conv ct |
52 |
74 |
|
75 |
|
76 (* main conversion *) |
|
77 fun eqvt_conv ctxt thms ctrm = |
|
78 let |
|
79 val trm = term_of ctrm |
|
80 val _ = if trace_enabled ctxt andalso not (is_head_Trueprop trm) |
|
81 then warning ("analysing " ^ Syntax.string_of_term ctxt trm) |
|
82 else () |
|
83 val wrapper = if trace_enabled ctxt then trace_conv ctxt else I |
53 in |
84 in |
54 |
85 Conv.first_conv (map wrapper |
55 fun eqvt_conv ctxt ct = |
86 [ More_Conv.rewrs_conv thms, |
56 Conv.first_conv |
87 Conv.rewr_conv @{thm eqvt_bound}, |
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), |
88 More_Conv.rewrs_conv (Nominal_ThmDecls.get_eqvts_raw_thms ctxt), |
|
89 eqvt_apply_conv ctxt, |
|
90 eqvt_lambda_conv ctxt, |
|
91 More_Conv.rewrs_conv @{thms permute_pure[THEN eq_reflection]}, |
63 Conv.all_conv |
92 Conv.all_conv |
64 ] ct |
93 ]) ctrm |
65 |
|
66 fun eqvt_tac ctxt = |
|
67 CONVERSION (More_Conv.bottom_conv (fn ctxt => eqvt_conv ctxt) ctxt) |
|
68 |
|
69 end |
94 end |
70 |
95 |
|
96 |
|
97 fun eqvt_tac ctxt thms = |
|
98 CONVERSION (More_Conv.top_conv (fn ctxt => eqvt_conv ctxt thms) ctxt) |
|
99 |
|
100 val setup = |
|
101 trace_eqvt_setup |
|
102 |
71 end; (* structure *) |
103 end; (* structure *) |