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