1 (* ========================================================================= *)
2 (* Syntax sugaring; theory of pairing, with a bit of support. *)
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 (* Constants implementing (or at least tagging) syntactic sugar. *)
14 (* ------------------------------------------------------------------------- *)
16 let LET_DEF = new_definition
17 `LET (f:A->B) x = f x`;;
19 let LET_END_DEF = new_definition
22 let GABS_DEF = new_definition
23 `GABS (P:A->bool) = (@) P`;;
25 let GEQ_DEF = new_definition
26 `GEQ a b = (a:A = b)`;;
28 let _SEQPATTERN = new_definition
29 `_SEQPATTERN = \r s x. if ?y. r x y then r x else s x`;;
31 let _UNGUARDED_PATTERN = new_definition
32 `_UNGUARDED_PATTERN = \p r. p /\ r`;;
34 let _GUARDED_PATTERN = new_definition
35 `_GUARDED_PATTERN = \p g r. p /\ g /\ r`;;
37 let _MATCH = new_definition
38 `_MATCH = \e r. if (?!) (r e) then (@) (r e) else @z. F`;;
40 let _FUNCTION = new_definition
41 `_FUNCTION = \r x. if (?!) (r x) then (@) (r x) else @z. F`;;
43 (* ------------------------------------------------------------------------- *)
45 (* ------------------------------------------------------------------------- *)
47 let mk_pair_def = new_definition
48 `mk_pair (x:A) (y:B) = \a b. (a = x) /\ (b = y)`;;
50 let PAIR_EXISTS_THM = prove
51 (`?x. ?(a:A) (b:B). x = mk_pair a b`,
54 let prod_tybij = new_type_definition
55 "prod" ("ABS_prod","REP_prod") PAIR_EXISTS_THM;;
57 let REP_ABS_PAIR = prove
58 (`!(x:A) (y:B). REP_prod (ABS_prod (mk_pair x y)) = mk_pair x y`,
59 MESON_TAC[prod_tybij]);;
61 parse_as_infix (",",(14,"right"));;
63 let COMMA_DEF = new_definition
64 `(x:A),(y:B) = ABS_prod(mk_pair x y)`;;
66 let FST_DEF = new_definition
67 `FST (p:A#B) = @x. ?y. p = x,y`;;
69 let SND_DEF = new_definition
70 `SND (p:A#B) = @y. ?x. p = x,y`;;
73 (`!(x:A) (y:B) a b. (x,y = a,b) <=> (x = a) /\ (y = b)`,
74 REPEAT GEN_TAC THEN EQ_TAC THENL
75 [REWRITE_TAC[COMMA_DEF] THEN
76 DISCH_THEN(MP_TAC o AP_TERM `REP_prod:A#B->A->B->bool`) THEN
77 REWRITE_TAC[REP_ABS_PAIR] THEN REWRITE_TAC[mk_pair_def; FUN_EQ_THM];
81 let PAIR_SURJECTIVE = prove
82 (`!p:A#B. ?x y. p = x,y`,
83 GEN_TAC THEN REWRITE_TAC[COMMA_DEF] THEN
84 MP_TAC(SPEC `REP_prod p :A->B->bool` (CONJUNCT2 prod_tybij)) THEN
85 REWRITE_TAC[CONJUNCT1 prod_tybij] THEN
86 DISCH_THEN(X_CHOOSE_THEN `a:A` (X_CHOOSE_THEN `b:B` MP_TAC)) THEN
87 DISCH_THEN(MP_TAC o AP_TERM `ABS_prod:(A->B->bool)->A#B`) THEN
88 REWRITE_TAC[CONJUNCT1 prod_tybij] THEN DISCH_THEN SUBST1_TAC THEN
89 MAP_EVERY EXISTS_TAC [`a:A`; `b:B`] THEN REFL_TAC);;
92 (`!(x:A) (y:B). FST(x,y) = x`,
93 REPEAT GEN_TAC THEN REWRITE_TAC[FST_DEF] THEN
94 MATCH_MP_TAC SELECT_UNIQUE THEN GEN_TAC THEN BETA_TAC THEN
95 REWRITE_TAC[PAIR_EQ] THEN EQ_TAC THEN
96 STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
97 EXISTS_TAC `y:B` THEN ASM_REWRITE_TAC[]);;
100 (`!(x:A) (y:B). SND(x,y) = y`,
101 REPEAT GEN_TAC THEN REWRITE_TAC[SND_DEF] THEN
102 MATCH_MP_TAC SELECT_UNIQUE THEN GEN_TAC THEN BETA_TAC THEN
103 REWRITE_TAC[PAIR_EQ] THEN EQ_TAC THEN
104 STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
105 EXISTS_TAC `x:A` THEN ASM_REWRITE_TAC[]);;
108 (`!x:A#B. FST x,SND x = x`,
110 (X_CHOOSE_THEN `a:A` (X_CHOOSE_THEN `b:B` SUBST1_TAC)
111 (SPEC `x:A#B` PAIR_SURJECTIVE)) THEN
112 REWRITE_TAC[FST; SND]);;
114 let pair_INDUCT = prove
115 (`!P. (!x y. P (x,y)) ==> !p. P p`,
116 REPEAT STRIP_TAC THEN
117 GEN_REWRITE_TAC RAND_CONV [GSYM PAIR] THEN
118 FIRST_ASSUM MATCH_ACCEPT_TAC);;
120 let pair_RECURSION = prove
121 (`!PAIR'. ?fn:A#B->C. !a0 a1. fn (a0,a1) = PAIR' a0 a1`,
122 GEN_TAC THEN EXISTS_TAC `\p. (PAIR':A->B->C) (FST p) (SND p)` THEN
123 REWRITE_TAC[FST; SND]);;
125 (* ------------------------------------------------------------------------- *)
126 (* Syntax operations. *)
127 (* ------------------------------------------------------------------------- *)
129 let is_pair = is_binary ",";;
131 let dest_pair = dest_binary ",";;
134 let ptm = mk_const(",",[]) in
135 fun (l,r) -> mk_comb(mk_comb(inst [type_of l,aty; type_of r,bty] ptm,l),r);;
137 (* ------------------------------------------------------------------------- *)
138 (* Extend basic rewrites; extend new_definition to allow paired varstructs. *)
139 (* ------------------------------------------------------------------------- *)
141 extend_basic_rewrites [FST; SND; PAIR];;
143 (* ------------------------------------------------------------------------- *)
144 (* Extend definitions to paired varstructs with benignity checking. *)
145 (* ------------------------------------------------------------------------- *)
147 let the_definitions = ref
148 [SND_DEF; FST_DEF; COMMA_DEF; mk_pair_def; GEQ_DEF; GABS_DEF;
149 LET_END_DEF; LET_DEF; one_DEF; I_DEF; o_DEF; COND_DEF; _FALSITY_;
150 EXISTS_UNIQUE_DEF; NOT_DEF; F_DEF; OR_DEF; EXISTS_DEF; FORALL_DEF; IMP_DEF;
155 let rec depair gv arg =
156 try let l,r = dest_pair arg in
157 (depair (list_mk_icomb "FST" [gv]) l) @
158 (depair (list_mk_icomb "SND" [gv]) r)
159 with Failure _ -> [gv,arg] in
160 fun arg -> let gv = genvar(type_of arg) in
163 let avs,def = strip_forall tm in
164 try let th,th' = tryfind (fun th -> th,PART_MATCH I th def)
165 (!the_definitions) in
166 ignore(PART_MATCH I th' (snd(strip_forall(concl th))));
167 warn true "Benign redefinition"; GEN_ALL (GENL avs th')
169 let l,r = dest_eq def in
170 let fn,args = strip_comb l in
171 let gargs,reps = (I F_F unions) (unzip(map depair args)) in
172 let l' = list_mk_comb(fn,gargs) and r' = subst reps r in
173 let th1 = new_definition (mk_eq(l',r')) in
174 let slist = zip args gargs in
175 let th2 = INST slist (SPEC_ALL th1) in
176 let xreps = map (subst slist o fst) reps in
177 let threps = map (SYM o PURE_REWRITE_CONV[FST; SND]) xreps in
178 let th3 = TRANS th2 (SYM(SUBS_CONV threps r)) in
179 let th4 = GEN_ALL (GENL avs th3) in
180 the_definitions := th4::(!the_definitions); th4;;
182 (* ------------------------------------------------------------------------- *)
183 (* A few more useful definitions. *)
184 (* ------------------------------------------------------------------------- *)
186 let CURRY_DEF = new_definition
187 `CURRY(f:A#B->C) x y = f(x,y)`;;
189 let UNCURRY_DEF = new_definition
190 `!f x y. UNCURRY(f:A->B->C)(x,y) = f x y`;;
192 let PASSOC_DEF = new_definition
193 `!f x y z. PASSOC (f:(A#B)#C->D) (x,y,z) = f ((x,y),z)`;;
195 (* ------------------------------------------------------------------------- *)
196 (* Analog of ABS_CONV for generalized abstraction. *)
197 (* ------------------------------------------------------------------------- *)
199 let GABS_CONV conv tm =
200 if is_abs tm then ABS_CONV conv tm else
201 let gabs,bod = dest_comb tm in
202 let f,qtm = dest_abs bod in
203 let xs,bod = strip_forall qtm in
204 AP_TERM gabs (ABS f (itlist MK_FORALL xs (RAND_CONV conv bod)));;
206 (* ------------------------------------------------------------------------- *)
207 (* General beta-conversion over linear pattern of nested constructors. *)
208 (* ------------------------------------------------------------------------- *)
211 let projection_cache = ref [] in
212 let create_projections conname =
213 try assoc conname (!projection_cache) with Failure _ ->
214 let genty = get_const_type conname in
215 let conty = fst(dest_type(repeat (snd o dest_fun_ty) genty)) in
216 let _,_,rth = assoc conty (!inductive_type_store) in
217 let sth = SPEC_ALL rth in
218 let evs,bod = strip_exists(concl sth) in
219 let cjs = conjuncts bod in
220 let ourcj = find ((=)conname o fst o dest_const o fst o strip_comb o
221 rand o lhand o snd o strip_forall) cjs in
222 let n = index ourcj cjs in
223 let avs,eqn = strip_forall ourcj in
224 let con',args = strip_comb(rand eqn) in
225 let aargs,zargs = chop_list (length avs) args in
226 let gargs = map (genvar o type_of) zargs in
227 let gcon = genvar(itlist (mk_fun_ty o type_of) avs (type_of(rand eqn))) in
229 INST [list_mk_abs(aargs @ gargs,list_mk_comb(gcon,avs)),con'] sth in
230 let cth = el n (CONJUNCTS(ASSUME(snd(strip_exists(concl bth))))) in
231 let dth = CONV_RULE (funpow (length avs) BINDER_CONV
232 (RAND_CONV(BETAS_CONV))) cth in
233 let eth = SIMPLE_EXISTS (rator(lhand(snd(strip_forall(concl dth))))) dth in
234 let fth = PROVE_HYP bth (itlist SIMPLE_CHOOSE evs eth) in
235 let zty = type_of (rand(snd(strip_forall(concl dth)))) in
237 let ity = type_of a in
238 let th = BETA_RULE(PINST [ity,zty] [list_mk_abs(avs,a),gcon] fth) in
239 SYM(SPEC_ALL(SELECT_RULE th)) in
240 let ths = map mk_projector avs in
241 (projection_cache := (conname,ths)::(!projection_cache); ths) in
242 let GEQ_CONV = REWR_CONV(GSYM GEQ_DEF)
243 and DEGEQ_RULE = CONV_RULE(REWR_CONV GEQ_DEF) in
246 (`(?) P ==> P (GABS P)`,
247 SIMP_TAC[GABS_DEF; SELECT_AX; ETA_AX]) in
249 let rec create_iterated_projections tm =
250 if frees tm = [] then []
251 else if is_var tm then [REFL tm] else
252 let con,args = strip_comb tm in
253 let prjths = create_projections (fst(dest_const con)) in
254 let atm = rand(rand(concl(hd prjths))) in
255 let instn = term_match [] atm tm in
256 let arths = map (INSTANTIATE instn) prjths in
257 let ths = map (fun arth ->
258 let sths = create_iterated_projections (lhand(concl arth)) in
259 map (CONV_RULE(RAND_CONV(SUBS_CONV[arth]))) sths) arths in
260 unions' equals_thm ths in
261 let GEN_BETA_CONV tm =
262 try BETA_CONV tm with Failure _ ->
263 let l,r = dest_comb tm in
264 let vstr,bod = dest_gabs l in
265 let instn = term_match [] vstr r in
266 let prjs = create_iterated_projections vstr in
267 let th1 = SUBS_CONV prjs bod in
268 let bod' = rand(concl th1) in
269 let gv = genvar(type_of vstr) in
270 let pat = mk_abs(gv,subst[gv,vstr] bod') in
271 let th2 = TRANS (BETA_CONV (mk_comb(pat,vstr))) (SYM th1) in
272 let avs = fst(strip_forall(body(rand l))) in
273 let th3 = GENL (fst(strip_forall(body(rand l)))) th2 in
274 let efn = genvar(type_of pat) in
275 let th4 = EXISTS(mk_exists(efn,subst[efn,pat] (concl th3)),pat) th3 in
276 let th5 = CONV_RULE(funpow (length avs + 1) BINDER_CONV GEQ_CONV) th4 in
277 let th6 = CONV_RULE BETA_CONV (GABS_RULE th5) in
278 INSTANTIATE instn (DEGEQ_RULE (SPEC_ALL th6)) in
281 (* ------------------------------------------------------------------------- *)
282 (* Add this to the basic "rewrites" and pairs to the inductive type store. *)
283 (* ------------------------------------------------------------------------- *)
285 extend_basic_convs("GEN_BETA_CONV",(`GABS (\a. b) c`,GEN_BETA_CONV));;
287 inductive_type_store :=
288 ("prod",(1,pair_INDUCT,pair_RECURSION))::(!inductive_type_store);;
290 (* ------------------------------------------------------------------------- *)
291 (* Convenient rules to eliminate binders over pairs. *)
292 (* ------------------------------------------------------------------------- *)
294 let FORALL_PAIR_THM = prove
295 (`!P. (!p. P p) <=> (!p1 p2. P(p1,p2))`,
298 let EXISTS_PAIR_THM = prove
299 (`!P. (?p. P p) <=> ?p1 p2. P(p1,p2)`,
302 let LAMBDA_PAIR_THM = prove
303 (`!t. (\p. t p) = (\(x,y). t(x,y))`,
304 REWRITE_TAC[FORALL_PAIR_THM; FUN_EQ_THM]);;
306 let PAIRED_ETA_THM = prove
307 (`(!f. (\(x,y). f (x,y)) = f) /\
308 (!f. (\(x,y,z). f (x,y,z)) = f) /\
309 (!f. (\(w,x,y,z). f (w,x,y,z)) = f)`,
310 REPEAT STRIP_TAC THEN REWRITE_TAC[FUN_EQ_THM; FORALL_PAIR_THM]);;
312 let FORALL_UNCURRY = prove
313 (`!P. (!f:A->B->C. P f) <=> (!f. P (\a b. f(a,b)))`,
314 GEN_TAC THEN EQ_TAC THEN SIMP_TAC[] THEN DISCH_TAC THEN
315 X_GEN_TAC `f:A->B->C` THEN
316 FIRST_ASSUM(MP_TAC o SPEC `\(a,b). (f:A->B->C) a b`) THEN SIMP_TAC[ETA_AX]);;
318 let EXISTS_UNCURRY = prove
319 (`!P. (?f:A->B->C. P f) <=> (?f. P (\a b. f(a,b)))`,
320 ONCE_REWRITE_TAC[MESON[] `(?x. P x) <=> ~(!x. ~P x)`] THEN
321 REWRITE_TAC[FORALL_UNCURRY]);;
323 let EXISTS_CURRY = prove
324 (`!P. (?f. P f) <=> (?f. P (\(a,b). f a b))`,
325 REWRITE_TAC[EXISTS_UNCURRY; PAIRED_ETA_THM]);;
327 let FORALL_CURRY = prove
328 (`!P. (!f. P f) <=> (!f. P (\(a,b). f a b))`,
329 REWRITE_TAC[FORALL_UNCURRY; PAIRED_ETA_THM]);;
331 let FORALL_UNPAIR_THM = prove
332 (`!P. (!x y. P x y) <=> !z. P (FST z) (SND z)`,
333 REWRITE_TAC[FORALL_PAIR_THM; FST; SND] THEN MESON_TAC[]);;
335 let EXISTS_UNPAIR_THM = prove
336 (`!P. (?x y. P x y) <=> ?z. P (FST z) (SND z)`,
337 REWRITE_TAC[EXISTS_PAIR_THM; FST; SND] THEN MESON_TAC[]);;
339 (* ------------------------------------------------------------------------- *)
340 (* Related theorems for explicitly paired quantifiers. *)
341 (* ------------------------------------------------------------------------- *)
343 let FORALL_PAIRED_THM = prove
344 (`!P. (!(x,y). P x y) <=> (!x y. P x y)`,
345 GEN_TAC THEN GEN_REWRITE_TAC (LAND_CONV o RATOR_CONV) [FORALL_DEF] THEN
346 REWRITE_TAC[FUN_EQ_THM; FORALL_PAIR_THM]);;
348 let EXISTS_PAIRED_THM = prove
349 (`!P. (?(x,y). P x y) <=> (?x y. P x y)`,
350 GEN_TAC THEN MATCH_MP_TAC(TAUT `(~p <=> ~q) ==> (p <=> q)`) THEN
351 REWRITE_TAC[REWRITE_RULE[ETA_AX] NOT_EXISTS_THM; FORALL_PAIR_THM]);;
353 (* ------------------------------------------------------------------------- *)
354 (* Likewise for tripled quantifiers (could continue with the same proof). *)
355 (* ------------------------------------------------------------------------- *)
357 let FORALL_TRIPLED_THM = prove
358 (`!P. (!(x,y,z). P x y z) <=> (!x y z. P x y z)`,
359 GEN_TAC THEN GEN_REWRITE_TAC (LAND_CONV o RATOR_CONV) [FORALL_DEF] THEN
360 REWRITE_TAC[FUN_EQ_THM; FORALL_PAIR_THM]);;
362 let EXISTS_TRIPLED_THM = prove
363 (`!P. (?(x,y,z). P x y z) <=> (?x y z. P x y z)`,
364 GEN_TAC THEN MATCH_MP_TAC(TAUT `(~p <=> ~q) ==> (p <=> q)`) THEN
365 REWRITE_TAC[REWRITE_RULE[ETA_AX] NOT_EXISTS_THM; FORALL_PAIR_THM]);;
367 (* ------------------------------------------------------------------------- *)
368 (* Expansion of a let-term. *)
369 (* ------------------------------------------------------------------------- *)
372 let let1_CONV = REWR_CONV LET_DEF THENC GEN_BETA_CONV
373 and lete_CONV = REWR_CONV LET_END_DEF in
374 let rec EXPAND_BETAS_CONV tm =
375 let tm' = rator tm in
376 try let1_CONV tm with Failure _ ->
377 let th1 = AP_THM (EXPAND_BETAS_CONV tm') (rand tm) in
378 let th2 = GEN_BETA_CONV (rand(concl th1)) in
381 let ltm,pargs = strip_comb tm in
382 if fst(dest_const ltm) <> "LET" or pargs = [] then failwith "let_CONV" else
383 let abstm = hd pargs in
384 let vs,bod = strip_gabs abstm in
387 if length vs <> n then failwith "let_CONV" else
388 (EXPAND_BETAS_CONV THENC lete_CONV) tm;;
390 let (LET_TAC:tactic) =
392 try let assigs,bod = dest_let tm in
393 forall (uncurry (=)) assigs
394 with Failure _ -> false
395 and PROVE_DEPAIRING_EXISTS =
397 (`((x,y) = a) <=> (x = FST a) /\ (y = SND a)`,
398 MESON_TAC[PAIR; PAIR_EQ]) in
399 let rewr1_CONV = GEN_REWRITE_CONV TOP_DEPTH_CONV [pth]
400 and rewr2_RULE = GEN_REWRITE_RULE (LAND_CONV o DEPTH_CONV)
401 [TAUT `(x = x) <=> T`; TAUT `a /\ T <=> a`] in
403 let th1 = rewr1_CONV tm in
404 let tm1 = rand(concl th1) in
405 let cjs = conjuncts tm1 in
406 let vars = map lhand cjs in
407 let th2 = EQ_MP (SYM th1) (ASSUME tm1) in
408 let th3 = DISCH_ALL (itlist SIMPLE_EXISTS vars th2) in
409 let th4 = INST (map (fun t -> rand t,lhand t) cjs) th3 in
410 MP (rewr2_RULE th4) TRUTH in
412 let path = try find_path is_trivlet w
413 with Failure _ -> find_path is_let w in
414 let tm = follow_path path w in
415 let assigs,bod = dest_let tm in
417 mapfilter (fun (x,y) -> if x = y then fail() else mk_eq(x,y)) assigs in
418 let lvars = itlist (union o frees o lhs) abbrevs []
419 and avoids = itlist (union o thm_frees o snd) asl (frees w) in
420 let rename = vsubst (zip (variants avoids lvars) lvars) in
421 let abbrevs' = map (fun eq -> let l,r = dest_eq eq in mk_eq(rename l,r))
423 let deprths = map PROVE_DEPAIRING_EXISTS abbrevs' in
424 (MAP_EVERY (REPEAT_TCL CHOOSE_THEN
425 (fun th -> let th' = SYM th in
426 SUBST_ALL_TAC th' THEN ASSUME_TAC th')) deprths THEN
428 let tm' = follow_path path w' in
429 CONV_TAC(PATH_CONV path (K(let_CONV tm'))))) gl;;