1 (* ========================================================================= *)
2 (* Basic equality reasoning including conversionals. *)
4 (* John Harrison, University of Cambridge Computer Laboratory *)
6 (* (c) Copyright, University of Cambridge 1998 *)
7 (* (c) Copyright, John Harrison 1998-2007 *)
8 (* ========================================================================= *)
12 (* ------------------------------------------------------------------------- *)
13 (* Type abbreviation for conversions. *)
14 (* ------------------------------------------------------------------------- *)
16 type conv = term->thm;;
18 (* ------------------------------------------------------------------------- *)
19 (* A bit more syntax. *)
20 (* ------------------------------------------------------------------------- *)
22 let lhand = rand o rator;;
24 let lhs = fst o dest_eq;;
26 let rhs = snd o dest_eq;;
28 (* ------------------------------------------------------------------------- *)
29 (* Similar to variant, but even avoids constants, and ignores types. *)
30 (* ------------------------------------------------------------------------- *)
33 let rec svariant avoid s =
34 if mem s avoid or (can get_const_type s & not(is_hidden s)) then
35 svariant avoid (s^"'")
38 let s,ty = dest_var v in
39 let s' = svariant (mapfilter (fst o dest_var) avoid) s in
42 (* ------------------------------------------------------------------------- *)
43 (* General case of beta-conversion. *)
44 (* ------------------------------------------------------------------------- *)
47 try BETA tm with Failure _ ->
48 try let f,arg = dest_comb tm in
50 INST [arg,v] (BETA (mk_comb(f,v)))
51 with Failure _ -> failwith "BETA_CONV: Not a beta-redex";;
53 (* ------------------------------------------------------------------------- *)
54 (* A few very basic derived equality rules. *)
55 (* ------------------------------------------------------------------------- *)
59 fun th -> try MK_COMB(rth,th)
60 with Failure _ -> failwith "AP_TERM";;
63 try MK_COMB(th,REFL tm)
64 with Failure _ -> failwith "AP_THM";;
68 let l,r = dest_eq tm in
70 EQ_MP (MK_COMB(AP_TERM (rator (rator tm)) th,lth)) lth;;
73 try TRANS (REFL tm1) (REFL tm2)
74 with Failure _ -> failwith "ALPHA";;
77 let res = alpha v tm in
80 let GEN_ALPHA_CONV v tm =
81 if is_abs tm then ALPHA_CONV v tm else
82 let b,abs = dest_comb tm in
83 AP_TERM b (ALPHA_CONV v abs);;
86 let afn = AP_TERM op in
87 fun (lth,rth) -> MK_COMB(afn lth,rth);;
89 (* ------------------------------------------------------------------------- *)
90 (* Terminal conversion combinators. *)
91 (* ------------------------------------------------------------------------- *)
93 let (NO_CONV:conv) = fun tm -> failwith "NO_CONV";;
95 let (ALL_CONV:conv) = REFL;;
97 (* ------------------------------------------------------------------------- *)
98 (* Combinators for sequencing, trying, repeating etc. conversions. *)
99 (* ------------------------------------------------------------------------- *)
101 let ((THENC):conv -> conv -> conv) =
104 let th2 = conv2 (rand(concl th1)) in
107 let ((ORELSEC):conv -> conv -> conv) =
109 try conv1 t with Failure _ -> conv2 t;;
111 let (FIRST_CONV:conv list -> conv) = end_itlist (fun c1 c2 -> c1 ORELSEC c2);;
113 let (EVERY_CONV:conv list -> conv) =
114 fun l -> itlist (fun c1 c2 -> c1 THENC c2) l ALL_CONV;;
117 let rec REPEATC conv t =
118 ((conv THENC (REPEATC conv)) ORELSEC ALL_CONV) t in
119 (REPEATC:conv->conv);;
121 let (CHANGED_CONV:conv->conv) =
124 let l,r = dest_eq (concl th) in
125 if aconv l r then failwith "CHANGED_CONV" else th;;
127 let TRY_CONV conv = conv ORELSEC ALL_CONV;;
129 (* ------------------------------------------------------------------------- *)
130 (* Subterm conversions. *)
131 (* ------------------------------------------------------------------------- *)
133 let (RATOR_CONV:conv->conv) =
136 Comb(l,r) -> AP_THM (conv l) r
137 | _ -> failwith "RATOR_CONV: Not a combination";;
139 let (RAND_CONV:conv->conv) =
142 Comb(l,r) -> MK_COMB(REFL l,conv r)
143 | _ -> failwith "RAND_CONV: Not a combination";;
145 let LAND_CONV = RATOR_CONV o RAND_CONV;;
147 let (COMB2_CONV: conv->conv->conv) =
148 fun lconv rconv tm ->
150 Comb(l,r) -> MK_COMB(lconv l,rconv r)
151 | _ -> failwith "COMB2_CONV: Not a combination";;
153 let COMB_CONV = W COMB2_CONV;;
155 let (ABS_CONV:conv->conv) =
157 let v,bod = dest_abs tm in
159 try ABS v th with Failure _ ->
160 let gv = genvar(type_of v) in
161 let gbod = vsubst[gv,v] bod in
162 let gth = ABS gv (conv gbod) in
163 let gtm = concl gth in
164 let l,r = dest_eq gtm in
165 let v' = variant (frees gtm) v in
166 let l' = alpha v' l and r' = alpha v' r in
167 EQ_MP (ALPHA gtm (mk_eq(l',r'))) gth;;
169 let BINDER_CONV conv tm =
170 if is_abs tm then ABS_CONV conv tm
171 else RAND_CONV(ABS_CONV conv) tm;;
173 let SUB_CONV conv tm =
175 Comb(_,_) -> COMB_CONV conv tm
176 | Abs(_,_) -> ABS_CONV conv tm
179 let BINOP_CONV conv tm =
180 let lop,r = dest_comb tm in
181 let op,l = dest_comb lop in
182 MK_COMB(AP_TERM op (conv l),conv r);;
184 (* ------------------------------------------------------------------------- *)
185 (* Depth conversions; internal use of a failure-propagating `Boultonized' *)
186 (* version to avoid a great deal of reuilding of terms. *)
187 (* ------------------------------------------------------------------------- *)
189 let (ONCE_DEPTH_CONV: conv->conv),
190 (DEPTH_CONV: conv->conv),
191 (REDEPTH_CONV: conv->conv),
192 (TOP_DEPTH_CONV: conv->conv),
193 (TOP_SWEEP_CONV: conv->conv) =
194 let THENQC conv1 conv2 tm =
195 try let th1 = conv1 tm in
196 try let th2 = conv2(rand(concl th1)) in TRANS th1 th2
197 with Failure _ -> th1
198 with Failure _ -> conv2 tm
199 and THENCQC conv1 conv2 tm =
200 let th1 = conv1 tm in
201 try let th2 = conv2(rand(concl th1)) in TRANS th1 th2
202 with Failure _ -> th1
203 and COMB_QCONV conv tm =
206 (try let th1 = conv l in
207 try let th2 = conv r in MK_COMB(th1,th2)
208 with Failure _ -> AP_THM th1 r
209 with Failure _ -> AP_TERM l (conv r))
210 | _ -> failwith "COMB_QCONV: Not a combination" in
211 let rec REPEATQC conv tm = THENCQC conv (REPEATQC conv) tm in
212 let SUB_QCONV conv tm =
214 Abs(_,_) -> ABS_CONV conv tm
215 | _ -> COMB_QCONV conv tm in
216 let rec ONCE_DEPTH_QCONV conv tm =
217 (conv ORELSEC (SUB_QCONV (ONCE_DEPTH_QCONV conv))) tm
218 and DEPTH_QCONV conv tm =
219 THENQC (SUB_QCONV (DEPTH_QCONV conv))
221 and REDEPTH_QCONV conv tm =
222 THENQC (SUB_QCONV (REDEPTH_QCONV conv))
223 (THENCQC conv (REDEPTH_QCONV conv)) tm
224 and TOP_DEPTH_QCONV conv tm =
225 THENQC (REPEATQC conv)
226 (THENCQC (SUB_QCONV (TOP_DEPTH_QCONV conv))
227 (THENCQC conv (TOP_DEPTH_QCONV conv))) tm
228 and TOP_SWEEP_QCONV conv tm =
229 THENQC (REPEATQC conv)
230 (SUB_QCONV (TOP_SWEEP_QCONV conv)) tm in
231 (fun c -> TRY_CONV (ONCE_DEPTH_QCONV c)),
232 (fun c -> TRY_CONV (DEPTH_QCONV c)),
233 (fun c -> TRY_CONV (REDEPTH_QCONV c)),
234 (fun c -> TRY_CONV (TOP_DEPTH_QCONV c)),
235 (fun c -> TRY_CONV (TOP_SWEEP_QCONV c));;
237 (* ------------------------------------------------------------------------- *)
238 (* Apply at leaves of op-tree; NB any failures at leaves cause failure. *)
239 (* ------------------------------------------------------------------------- *)
241 let rec DEPTH_BINOP_CONV op conv tm =
243 Comb(Comb(op',l),r) when Pervasives.compare op' op = 0 ->
244 let l,r = dest_binop op tm in
245 let lth = DEPTH_BINOP_CONV op conv l
246 and rth = DEPTH_BINOP_CONV op conv r in
247 MK_COMB(AP_TERM op' lth,rth)
250 (* ------------------------------------------------------------------------- *)
252 (* ------------------------------------------------------------------------- *)
255 let rec path_conv s cnv =
258 | "l"::t -> RATOR_CONV (path_conv t cnv)
259 | "r"::t -> RAND_CONV (path_conv t cnv)
260 | _::t -> ABS_CONV (path_conv t cnv) in
261 fun s cnv -> path_conv (explode s) cnv;;
263 (* ------------------------------------------------------------------------- *)
264 (* Follow a pattern *)
265 (* ------------------------------------------------------------------------- *)
268 let rec PCONV xs pat conv =
269 if mem pat xs then conv
270 else if not(exists (fun x -> free_in x pat) xs) then ALL_CONV
271 else if is_comb pat then
272 COMB2_CONV (PCONV xs (rator pat) conv) (PCONV xs (rand pat) conv)
274 ABS_CONV (PCONV xs (body pat) conv) in
275 fun pat -> let xs,pbod = strip_abs pat in PCONV xs pbod;;
277 (* ------------------------------------------------------------------------- *)
278 (* Symmetry conversion. *)
279 (* ------------------------------------------------------------------------- *)
282 try let th1 = SYM(ASSUME tm) in
283 let tm' = concl th1 in
284 let th2 = SYM(ASSUME tm') in
285 DEDUCT_ANTISYM_RULE th2 th1
286 with Failure _ -> failwith "SYM_CONV";;
288 (* ------------------------------------------------------------------------- *)
289 (* Conversion to a rule. *)
290 (* ------------------------------------------------------------------------- *)
292 let CONV_RULE (conv:conv) th =
293 EQ_MP (conv(concl th)) th;;
295 (* ------------------------------------------------------------------------- *)
296 (* Substitution conversion. *)
297 (* ------------------------------------------------------------------------- *)
299 let SUBS_CONV ths tm =
300 try if ths = [] then REFL tm else
301 let lefts = map (lhand o concl) ths in
302 let gvs = map (genvar o type_of) lefts in
303 let pat = subst (zip gvs lefts) tm in
304 let abs = list_mk_abs(gvs,pat) in
306 (fun y x -> CONV_RULE (RAND_CONV BETA_CONV THENC LAND_CONV BETA_CONV)
307 (MK_COMB(x,y))) ths (REFL abs) in
308 if rand(concl th) = tm then REFL tm else th
309 with Failure _ -> failwith "SUBS_CONV";;
311 (* ------------------------------------------------------------------------- *)
312 (* Get a few rules. *)
313 (* ------------------------------------------------------------------------- *)
315 let BETA_RULE = CONV_RULE(REDEPTH_CONV BETA_CONV);;
317 let GSYM = CONV_RULE(ONCE_DEPTH_CONV SYM_CONV);;
319 let SUBS ths = CONV_RULE (SUBS_CONV ths);;
321 (* ------------------------------------------------------------------------- *)
322 (* A cacher for conversions. *)
323 (* ------------------------------------------------------------------------- *)
327 let tm' = lhand(concl th) in
328 fun tm -> if tm' = tm then th else TRANS (ALPHA tm tm') th in
330 let net = ref empty_net in
331 fun tm -> try tryfind (fun f -> f tm) (lookup tm (!net))
334 (net := enter [] (tm,ALPHA_HACK th) (!net); th);;