1 (* ========================================================================= *)
2 (* Tools for defining quotient types and lifting first order theorems. *)
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 (* Given a type name "ty" and a curried binary relation R, this defines *)
14 (* a new type "ty" of R-equivalence classes. The abstraction and *)
15 (* representation functions for the new type are called "mk_ty" and *)
16 (* "dest_ty". The type bijections (after beta-conversion) are returned: *)
18 (* |- mk_ty (dest_ty a) = a *)
20 (* |- (?x. r = R x) <=> (dest_ty (mk_ty r) = r) *)
21 (* ------------------------------------------------------------------------- *)
23 let define_quotient_type =
24 fun tyname (absname,repname) eqv ->
25 let ty = hd(snd(dest_type(type_of eqv))) in
26 let pty = mk_fun_ty ty bool_ty in
27 let s = mk_var("s",pty) and x = mk_var("x",ty) in
28 let eqvx = mk_comb(eqv,x) in
29 let pred = mk_abs(s,mk_exists(x,mk_eq(s,eqvx))) in
30 let th0 = BETA_CONV(mk_comb(pred,eqvx)) in
31 let th1 = EXISTS(rand(concl th0),x) (REFL eqvx) in
32 let th2 = EQ_MP (SYM th0) th1 in
33 let abs,rep = new_basic_type_definition tyname (absname,repname) th2 in
34 abs,CONV_RULE(LAND_CONV BETA_CONV) rep;;
36 (* ------------------------------------------------------------------------- *)
37 (* Given a welldefinedness theorem for a curried function f, of the form: *)
39 (* |- !x1 x1' .. xn xn'. (x1 == x1') /\ ... /\ (xn == xn') *)
40 (* ==> (f x1 .. xn == f x1' .. f nx') *)
42 (* where each "==" is either equality or some fixed binary relation R, a *)
43 (* new operator called "opname" is introduced which lifts "f" up to the *)
44 (* R-equivalence classes. Two theorems are returned: the actual definition *)
45 (* and a useful consequence for lifting theorems. *)
47 (* The function also needs the second (more complicated) type bijection, and *)
48 (* the reflexivity and transitivity (not symmetry!) of the equivalence *)
49 (* relation. The use also gives a name for the new function. *)
50 (* ------------------------------------------------------------------------- *)
53 let SELECT_LEMMA = prove
54 (`!x:A. (@y. x = y) = x`,
55 GEN_TAC THEN GEN_REWRITE_TAC (LAND_CONV o BINDER_CONV) [EQ_SYM_EQ] THEN
56 MATCH_ACCEPT_TAC SELECT_REFL) in
58 let tybl,tybr = dest_comb(concl tybij2) in
59 let eqvx = rand(body(rand(rand tybl))) in
60 let eqv,xtm = dest_comb eqvx in
61 let dmr,rtm = dest_eq tybr in
62 let dest,mrt = dest_comb dmr in
64 let ety = type_of mrt in
65 fun (refl_th,trans_th) fname wth ->
66 let wtm = repeat (snd o dest_forall) (concl wth) in
67 let wfvs = frees wtm in
68 let hyps,con = try (conjuncts F_F I) (dest_imp wtm)
69 with Failure _ -> [],wtm in
70 let eqs,rels = partition is_eq hyps in
71 let rvs = map lhand rels in
72 let qvs = map lhs eqs in
74 variants wfvs (map (fun v -> mk_var(fst(dest_var v),ety)) rvs) in
75 let mems = map2 (fun rv ev -> mk_comb(mk_comb(dest,ev),rv)) rvs evs in
76 let lcon,rcon = dest_comb con in
77 let u = variant (evs @ wfvs) (mk_var("u",type_of rcon)) in
78 let ucon = mk_comb(lcon,u) in
79 let dbod = list_mk_conj(ucon::mems) in
80 let detm = list_mk_exists(rvs,dbod) in
81 let datm = mk_abs(u,detm) in
83 if is_eq con then list_mk_icomb "@" [datm] else mk_comb(mk,datm) in
85 (fun e -> try lhs e with Failure _ -> assoc (lhand e) (zip rvs evs)) hyps in
86 let rdef = list_mk_abs(newargs,def) in
87 let ldef = mk_var(fname,type_of rdef) in
88 let dth = new_definition(mk_eq(ldef,rdef)) in
90 (fun v th -> CONV_RULE(RAND_CONV BETA_CONV) (AP_THM th v))
92 let targs = map (fun v -> mk_comb(mk,mk_comb(eqv,v))) rvs in
94 let th = INST [eqvx,rtm] tybij2 in
95 EQ_MP th (EXISTS(lhs(concl th),xtm) (REFL eqvx)) in
96 let ith = INST (zip targs evs) eth in
97 let jth = SUBS (map (fun v -> INST[v,xtm] dme_th) rvs) ith in
98 let apop,uxtm = dest_comb(rand(concl jth)) in
99 let extm = body uxtm in
100 let evs,bod = strip_exists extm in
101 let th1 = ASSUME bod in
103 if evs = [] then th1 else
104 let th2a,th2b = CONJ_PAIR th1 in
105 let ethlist = CONJUNCTS th2b @ map REFL qvs in
106 let th2c = end_itlist CONJ (map
107 (fun v -> find ((=) (lhand v) o lhand o concl) ethlist) hyps) in
108 let th2d = MATCH_MP wth th2c in
109 let th2e = try TRANS th2d th2a
110 with Failure _ -> MATCH_MP trans_th (CONJ th2d th2a) in
111 itlist SIMPLE_CHOOSE evs th2e in
112 let th3 = ASSUME(concl th2) in
113 let th4 = end_itlist CONJ (th3::(map (C SPEC refl_th) rvs)) in
114 let th5 = itlist SIMPLE_EXISTS evs (ASSUME bod) in
115 let th6 = MATCH_MP (DISCH_ALL th5) th4 in
116 let th7 = IMP_ANTISYM_RULE (DISCH_ALL th2) (DISCH_ALL th6) in
117 let th8 = TRANS jth (AP_TERM apop (ABS u th7)) in
118 let fconv = if is_eq con then REWR_CONV SELECT_LEMMA
119 else RAND_CONV ETA_CONV in
120 let th9 = CONV_RULE (RAND_CONV fconv) th8 in
123 (* ------------------------------------------------------------------------- *)
124 (* Lifts a theorem. This can be done by higher order rewriting alone. *)
126 (* NB! All and only the first order variables must be bound by quantifiers. *)
127 (* ------------------------------------------------------------------------- *)
131 (`(!x:Repty. R x x) /\
132 (!x y. R x y <=> R y x) /\
133 (!x y z. R x y /\ R y z ==> R x z) /\
134 (!a. mk(dest a) = a) /\
135 (!r. (?x. r = R x) <=> (dest(mk r) = r))
136 ==> (!x y. R x y <=> (mk(R x) = mk(R y))) /\
137 (!P. (!x. P(mk(R x))) <=> (!x. P x)) /\
138 (!P. (?x. P(mk(R x))) <=> (?x. P x)) /\
139 (!x:Absty. mk(R((@)(dest x))) = x)`,
142 `!x y. (mk((R:Repty->Repty->bool) x):Absty = mk(R y)) <=> (R x = R y)`
143 ASSUME_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
144 MATCH_MP_TAC(TAUT `(a /\ b /\ c) /\ (b ==> a ==> d)
145 ==> a /\ b /\ c /\ d`) THEN
147 [ASM_REWRITE_TAC[] THEN REWRITE_TAC[FUN_EQ_THM] THEN ASM_MESON_TAC[];
149 REPEAT(DISCH_THEN(fun th -> REWRITE_TAC[GSYM th])) THEN
150 X_GEN_TAC `x:Repty` THEN
151 SUBGOAL_THEN `dest(mk((R:Repty->Repty->bool) x):Absty) = R x`
152 SUBST1_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
153 GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [GSYM ETA_AX] THEN
154 FIRST_ASSUM(fun th -> GEN_REWRITE_TAC I [th]) THEN
155 CONV_TAC SELECT_CONV THEN ASM_MESON_TAC[]) in
156 fun tybij (refl_th,sym_th,trans_th) ->
157 let tybij1 = GEN_ALL (fst tybij)
158 and tybij2 = GEN_ALL (snd tybij) in
159 let cth = end_itlist CONJ [refl_th; sym_th; trans_th; tybij1; tybij2] in
160 let ith = MATCH_MP pth cth in
162 REWRITE_RULE (ith::trths);;