1 (* Title: nominal_permeq.ML |
|
2 Author: Christian Urban |
|
3 Author: Brian Huffman |
|
4 *) |
|
5 |
|
6 signature NOMINAL_PERMEQ = |
|
7 sig |
|
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 |
|
10 |
|
11 val perm_simp_meth: thm list * string list -> Proof.context -> Method.method |
|
12 val perm_strict_simp_meth: thm list * string list -> Proof.context -> Method.method |
|
13 val args_parser: (thm list * string list) context_parser |
|
14 |
|
15 val trace_eqvt: bool Config.T |
|
16 val setup: theory -> theory |
|
17 end; |
|
18 |
|
19 (* |
|
20 |
|
21 - eqvt_tac and eqvt_strict_tac take a list of theorems |
|
22 which are first tried to simplify permutations |
|
23 |
|
24 the string list contains constants that should not be |
|
25 analysed (for example there is no raw eqvt-lemma for |
|
26 the constant The); therefore it should not be analysed |
|
27 |
|
28 - setting [[trace_eqvt = true]] switches on tracing |
|
29 information |
|
30 |
|
31 *) |
|
32 |
|
33 structure Nominal_Permeq: NOMINAL_PERMEQ = |
|
34 struct |
|
35 |
|
36 open Nominal_ThmDecls; |
|
37 |
|
38 (* tracing infrastructure *) |
|
39 val (trace_eqvt, trace_eqvt_setup) = Attrib.config_bool "trace_eqvt" (K false); |
|
40 |
|
41 fun trace_enabled ctxt = Config.get ctxt trace_eqvt |
|
42 |
|
43 fun trace_msg ctxt result = |
|
44 let |
|
45 val lhs_str = Syntax.string_of_term ctxt (term_of (Thm.lhs_of result)) |
|
46 val rhs_str = Syntax.string_of_term ctxt (term_of (Thm.rhs_of result)) |
|
47 in |
|
48 warning (Pretty.string_of (Pretty.strs ["Rewriting", lhs_str, "to", rhs_str])) |
|
49 end |
|
50 |
|
51 fun trace_conv ctxt conv ctrm = |
|
52 let |
|
53 val result = conv ctrm |
|
54 in |
|
55 if Thm.is_reflexive result |
|
56 then result |
|
57 else (trace_msg ctxt result; result) |
|
58 end |
|
59 |
|
60 (* this conversion always fails, but prints |
|
61 out the analysed term *) |
|
62 fun trace_info_conv ctxt ctrm = |
|
63 let |
|
64 val trm = term_of ctrm |
|
65 val _ = case (head_of trm) of |
|
66 @{const "Trueprop"} => () |
|
67 | _ => warning ("Analysing term " ^ Syntax.string_of_term ctxt trm) |
|
68 in |
|
69 Conv.no_conv ctrm |
|
70 end |
|
71 |
|
72 (* conversion for applications *) |
|
73 fun eqvt_apply_conv ctrm = |
|
74 case (term_of ctrm) of |
|
75 Const (@{const_name "permute"}, _) $ _ $ (_ $ _) => |
|
76 let |
|
77 val (perm, t) = Thm.dest_comb ctrm |
|
78 val (_, p) = Thm.dest_comb perm |
|
79 val (f, x) = Thm.dest_comb t |
|
80 val a = ctyp_of_term x; |
|
81 val b = ctyp_of_term t; |
|
82 val ty_insts = map SOME [b, a] |
|
83 val term_insts = map SOME [p, f, x] |
|
84 in |
|
85 Drule.instantiate' ty_insts term_insts @{thm eqvt_apply} |
|
86 end |
|
87 | _ => Conv.no_conv ctrm |
|
88 |
|
89 (* conversion for lambdas *) |
|
90 fun eqvt_lambda_conv ctrm = |
|
91 case (term_of ctrm) of |
|
92 Const (@{const_name "permute"}, _) $ _ $ (Abs _) => |
|
93 Conv.rewr_conv @{thm eqvt_lambda} ctrm |
|
94 | _ => Conv.no_conv ctrm |
|
95 |
|
96 |
|
97 (* conversion that raises an error or prints a warning message, |
|
98 if a permutation on a constant or application cannot be analysed *) |
|
99 |
|
100 fun is_excluded excluded (Const (a, _)) = member (op=) excluded a |
|
101 | is_excluded _ _ = false |
|
102 |
|
103 fun progress_info_conv ctxt strict_flag excluded ctrm = |
|
104 let |
|
105 fun msg trm = |
|
106 if is_excluded excluded trm then () else |
|
107 (if strict_flag then error else warning) |
|
108 ("Cannot solve equivariance for " ^ (Syntax.string_of_term ctxt trm)) |
|
109 |
|
110 val _ = case (term_of ctrm) of |
|
111 Const (@{const_name "permute"}, _) $ _ $ (trm as Const _) => msg trm |
|
112 | Const (@{const_name "permute"}, _) $ _ $ (trm as _ $ _) => msg trm |
|
113 | _ => () |
|
114 in |
|
115 Conv.all_conv ctrm |
|
116 end |
|
117 |
|
118 (* main conversion *) |
|
119 fun eqvt_conv ctxt strict_flag user_thms excluded ctrm = |
|
120 let |
|
121 val first_conv_wrapper = |
|
122 if trace_enabled ctxt |
|
123 then Conv.first_conv o (cons (trace_info_conv ctxt)) o (map (trace_conv ctxt)) |
|
124 else Conv.first_conv |
|
125 |
|
126 val pre_thms = map safe_mk_equiv user_thms @ @{thms eqvt_bound} @ get_eqvts_raw_thms ctxt |
|
127 val post_thms = map safe_mk_equiv @{thms permute_pure} |
|
128 in |
|
129 first_conv_wrapper |
|
130 [ Conv.rewrs_conv pre_thms, |
|
131 eqvt_apply_conv, |
|
132 eqvt_lambda_conv, |
|
133 Conv.rewrs_conv post_thms, |
|
134 progress_info_conv ctxt strict_flag excluded |
|
135 ] ctrm |
|
136 end |
|
137 |
|
138 (* the eqvt-tactics first eta-normalise goals in |
|
139 order to avoid problems with inductions in the |
|
140 equivaraince command. *) |
|
141 |
|
142 (* raises an error if some permutations cannot be eliminated *) |
|
143 fun eqvt_strict_tac ctxt user_thms excluded = |
|
144 CONVERSION (Conv.top_conv |
|
145 (fn ctxt => Thm.eta_conversion then_conv (eqvt_conv ctxt true user_thms excluded)) ctxt) |
|
146 |
|
147 (* prints a warning message if some permutations cannot be eliminated *) |
|
148 fun eqvt_tac ctxt user_thms excluded = |
|
149 CONVERSION (Conv.top_conv |
|
150 (fn ctxt => Thm.eta_conversion then_conv (eqvt_conv ctxt false user_thms excluded)) ctxt) |
|
151 |
|
152 (* setup of the configuration value *) |
|
153 val setup = |
|
154 trace_eqvt_setup |
|
155 |
|
156 |
|
157 (** methods **) |
|
158 fun unless_more_args scan = Scan.unless (Scan.lift ((Args.$$$ "exclude") -- Args.colon)) scan |
|
159 |
|
160 val add_thms_parser = Scan.optional (Scan.lift (Args.add -- Args.colon) |-- |
|
161 Scan.repeat (unless_more_args Attrib.multi_thm) >> flat) []; |
|
162 |
|
163 val exclude_consts_parser = Scan.optional (Scan.lift ((Args.$$$ "exclude") -- Args.colon) |-- |
|
164 (Scan.repeat (Args.const true))) [] |
|
165 |
|
166 val args_parser = add_thms_parser -- exclude_consts_parser |
|
167 |
|
168 fun perm_simp_meth (thms, consts) ctxt = |
|
169 SIMPLE_METHOD (HEADGOAL (eqvt_tac ctxt thms consts)) |
|
170 |
|
171 fun perm_strict_simp_meth (thms, consts) ctxt = |
|
172 SIMPLE_METHOD (HEADGOAL (eqvt_strict_tac ctxt thms consts)) |
|
173 |
|
174 end; (* structure *) |
|