1 (* Title: nominal_thmdecls.ML |
1 (* Title: nominal_permeq.ML |
2 Author: Brian Huffman, Christian Urban |
2 Author: Christian Urban |
|
3 Author: Brian Huffman |
3 *) |
4 *) |
4 |
5 |
5 signature NOMINAL_PERMEQ = |
6 signature NOMINAL_PERMEQ = |
6 sig |
7 sig |
7 val eqvt_tac: Proof.context -> thm list -> int -> tactic |
8 val eqvt_tac: Proof.context -> thm list -> string list -> int -> tactic |
|
9 val eqvt_strict_tac: Proof.context -> thm list -> string list -> int -> tactic |
8 val trace_eqvt: bool Config.T |
10 val trace_eqvt: bool Config.T |
9 val setup: theory -> theory |
11 val setup: theory -> theory |
10 end; |
12 end; |
11 |
13 |
12 (* TODO: |
14 (* |
13 |
15 |
14 - provide a method interface with the usual add and del options |
16 - eqvt_tac and eqvt_strict_tac take a list of theorems |
|
17 which are first tried to simplify permutations |
15 |
18 |
16 - print a warning if for a constant no eqvt lemma is stored |
19 the string list contains constants that should not be |
|
20 analysed (for example there is no raw eqvt-lemma for |
|
21 the constant The; therefore it should not be analysed |
|
22 |
|
23 - setting [[trace_eqvt = true]] switches on tracing |
|
24 information |
|
25 |
|
26 |
|
27 TODO: |
|
28 |
|
29 - provide a proper parser for the method (see Nominal2_Eqvt) |
|
30 |
|
31 - proably the list of bad constant should be a dataslot |
17 |
32 |
18 *) |
33 *) |
19 |
|
20 |
34 |
21 structure Nominal_Permeq: NOMINAL_PERMEQ = |
35 structure Nominal_Permeq: NOMINAL_PERMEQ = |
22 struct |
36 struct |
23 |
37 |
24 fun is_head_Trueprop trm = |
38 open Nominal_ThmDecls; |
25 case (head_of trm) of |
|
26 @{const "Trueprop"} => true |
|
27 | _ => false |
|
28 |
39 |
29 (* debugging infrastructure *) |
40 (* tracing infrastructure *) |
30 val (trace_eqvt, trace_eqvt_setup) = Attrib.config_bool "trace_eqvt" (K false); |
41 val (trace_eqvt, trace_eqvt_setup) = Attrib.config_bool "trace_eqvt" (K false); |
31 |
42 |
32 fun trace_enabled ctxt = Config.get ctxt trace_eqvt |
43 fun trace_enabled ctxt = Config.get ctxt trace_eqvt |
33 |
44 |
34 fun trace_conv ctxt conv ct = |
45 fun trace_msg ctxt result = |
35 let |
46 let |
36 val result = conv ct |
47 val lhs_str = Syntax.string_of_term ctxt (term_of (Thm.lhs_of result)) |
37 val _ = |
48 val rhs_str = Syntax.string_of_term ctxt (term_of (Thm.rhs_of result)) |
38 if trace_enabled ctxt andalso not (Thm.is_reflexive result) |
49 in |
39 then |
50 tracing (Pretty.string_of (Pretty.strs ["Rewriting", lhs_str, "to", rhs_str])) |
|
51 end |
|
52 |
|
53 fun trace_conv ctxt conv ctrm = |
|
54 let |
|
55 val result = conv ctrm |
|
56 in |
|
57 if Thm.is_reflexive result |
|
58 then result |
|
59 else (trace_msg ctxt result; result) |
|
60 end |
|
61 |
|
62 (* this conversion always fails, but prints |
|
63 out the analysed term *) |
|
64 fun trace_info_conv ctxt ctrm = |
|
65 let |
|
66 val trm = term_of ctrm |
|
67 val _ = case (head_of trm) of |
|
68 @{const "Trueprop"} => () |
|
69 | _ => tracing ("Analysing term " ^ Syntax.string_of_term ctxt trm) |
|
70 in |
|
71 Conv.no_conv ctrm |
|
72 end |
|
73 |
|
74 |
|
75 (* conversion for applications: |
|
76 only applies the conversion, if the head of the |
|
77 application is not a "bad head" *) |
|
78 fun has_bad_head bad_hds trm = |
|
79 case (head_of trm) of |
|
80 Const (s, _) => member (op=) bad_hds s |
|
81 | _ => false |
|
82 |
|
83 fun eqvt_apply_conv bad_hds ctrm = |
|
84 case (term_of ctrm) of |
|
85 Const (@{const_name "permute"}, _) $ _ $ (trm $ _) => |
40 let |
86 let |
41 val lhs_str = Syntax.string_of_term ctxt (term_of (Thm.lhs_of result)) |
87 val (perm, t) = Thm.dest_comb ctrm |
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 *) |
|
52 fun eqvt_apply_conv ctxt ct = |
|
53 case (term_of ct) of |
|
54 (Const (@{const_name "permute"}, _) $ _ $ (_ $ _)) => |
|
55 let |
|
56 val (perm, t) = Thm.dest_comb ct |
|
57 val (_, p) = Thm.dest_comb perm |
88 val (_, p) = Thm.dest_comb perm |
58 val (f, x) = Thm.dest_comb t |
89 val (f, x) = Thm.dest_comb t |
59 val a = ctyp_of_term x; |
90 val a = ctyp_of_term x; |
60 val b = ctyp_of_term t; |
91 val b = ctyp_of_term t; |
61 val ty_insts = map SOME [b, a] |
92 val ty_insts = map SOME [b, a] |
62 val term_insts = map SOME [p, f, x] |
93 val term_insts = map SOME [p, f, x] |
63 in |
94 in |
64 Drule.instantiate' ty_insts term_insts @{thm eqvt_apply} |
95 if has_bad_head bad_hds trm |
|
96 then Conv.no_conv ctrm |
|
97 else Drule.instantiate' ty_insts term_insts @{thm eqvt_apply} |
65 end |
98 end |
66 | _ => Conv.no_conv ct |
99 | _ => Conv.no_conv ctrm |
67 |
100 |
68 (* conversion for lambdas *) |
101 (* conversion for lambdas *) |
69 fun eqvt_lambda_conv ctxt ct = |
102 fun eqvt_lambda_conv ctrm = |
70 case (term_of ct) of |
103 case (term_of ctrm) of |
71 (Const (@{const_name "permute"}, _) $ _ $ Abs _) => |
104 Const (@{const_name "permute"}, _) $ _ $ (Abs _) => |
72 Conv.rewr_conv @{thm eqvt_lambda} ct |
105 Conv.rewr_conv @{thm eqvt_lambda} ctrm |
73 | _ => Conv.no_conv ct |
106 | _ => Conv.no_conv ctrm |
|
107 |
|
108 (* conversion that raises an error or prints a warning message, |
|
109 if a permutation on a constant or application cannot be analysed *) |
|
110 fun progress_info_conv ctxt strict_flag ctrm = |
|
111 let |
|
112 fun msg trm = |
|
113 (if strict_flag then error else warning) |
|
114 ("Cannot solve equivariance for " ^ (Syntax.string_of_term ctxt trm)) |
|
115 |
|
116 val _ = case (term_of ctrm) of |
|
117 Const (@{const_name "permute"}, _) $ _ $ (trm as Const _) => msg trm |
|
118 | Const (@{const_name "permute"}, _) $ _ $ (trm as _ $ _) => msg trm |
|
119 | _ => () |
|
120 in |
|
121 Conv.all_conv ctrm |
|
122 end |
74 |
123 |
75 |
124 |
76 (* main conversion *) |
125 (* main conversion *) |
77 fun eqvt_conv ctxt thms ctrm = |
126 fun eqvt_conv ctxt strict_flag thms bad_hds ctrm = |
78 let |
127 let |
79 val trm = term_of ctrm |
128 val first_conv_wrapper = |
80 val _ = if trace_enabled ctxt andalso not (is_head_Trueprop trm) |
129 if trace_enabled ctxt |
81 then warning ("analysing " ^ Syntax.string_of_term ctxt trm) |
130 then Conv.first_conv o (cons (trace_info_conv ctxt)) o (map (trace_conv ctxt)) |
82 else () |
131 else Conv.first_conv |
83 val wrapper = if trace_enabled ctxt then trace_conv ctxt else I |
132 |
|
133 val pre_thms = thms @ @{thms eqvt_bound} @ (get_eqvts_raw_thms ctxt) |
|
134 val post_thms = @{thms permute_pure[THEN eq_reflection]} |
84 in |
135 in |
85 Conv.first_conv (map wrapper |
136 first_conv_wrapper |
86 [ More_Conv.rewrs_conv thms, |
137 [ More_Conv.rewrs_conv pre_thms, |
87 Conv.rewr_conv @{thm eqvt_bound}, |
138 eqvt_apply_conv bad_hds, |
88 More_Conv.rewrs_conv (Nominal_ThmDecls.get_eqvts_raw_thms ctxt), |
139 eqvt_lambda_conv, |
89 eqvt_apply_conv ctxt, |
140 More_Conv.rewrs_conv post_thms, |
90 eqvt_lambda_conv ctxt, |
141 progress_info_conv ctxt strict_flag |
91 More_Conv.rewrs_conv @{thms permute_pure[THEN eq_reflection]}, |
142 ] ctrm |
92 Conv.all_conv |
|
93 ]) ctrm |
|
94 end |
143 end |
95 |
144 |
|
145 (* raises an error if some permutations cannot be eliminated *) |
|
146 fun eqvt_strict_tac ctxt thms bad_hds = |
|
147 CONVERSION (More_Conv.top_conv (fn ctxt => eqvt_conv ctxt true thms bad_hds) ctxt) |
96 |
148 |
97 fun eqvt_tac ctxt thms = |
149 (* prints a warning message if some permutations cannot be eliminated *) |
98 CONVERSION (More_Conv.top_conv (fn ctxt => eqvt_conv ctxt thms) ctxt) |
150 fun eqvt_tac ctxt thms bad_hds = |
|
151 CONVERSION (More_Conv.top_conv (fn ctxt => eqvt_conv ctxt false thms bad_hds) ctxt) |
99 |
152 |
|
153 (* setup of the configuration value *) |
100 val setup = |
154 val setup = |
101 trace_eqvt_setup |
155 trace_eqvt_setup |
102 |
156 |
103 end; (* structure *) |
157 end; (* structure *) |