quot.ml

   1 (* ========================================================================= *)
   2 (* Tools for defining quotient types and lifting first order theorems.       *)
   3 (*                                                                           *)
   4 (*       John Harrison, University of Cambridge Computer Laboratory          *)
   5 (*                                                                           *)
   6 (*            (c) Copyright, University of Cambridge 1998                    *)
   7 (*              (c) Copyright, John Harrison 1998-2007                       *)
   8 (* ========================================================================= *)
   9
  10 needs "meson.ml";;
  11
  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:      *)
  17 (*                                                                           *)
  18 (*             |- mk_ty (dest_ty a) = a                                      *)
  19 (*                                                                           *)
  20 (*             |- (?x. r = R x) <=> (dest_ty (mk_ty r) = r)                  *)
  21 (* ------------------------------------------------------------------------- *)
  22
  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;;
  35
  36 (* ------------------------------------------------------------------------- *)
  37 (* Given a welldefinedness theorem for a curried function f, of the form:    *)
  38 (*                                                                           *)
  39 (* |- !x1 x1' .. xn xn'. (x1 == x1') /\ ... /\ (xn == xn')                   *)
  40 (*                       ==> (f x1 .. xn == f x1' .. f nx')                  *)
  41 (*                                                                           *)
  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.                            *)
  46 (*                                                                           *)
  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 (* ------------------------------------------------------------------------- *)
  51
  52 let lift_function =
  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
  57   fun tybij2 ->
  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
  63     let mk = rator mrt 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
  73       let evs =
  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
  82       let def =
  83         if is_eq con then list_mk_icomb "@" [datm] else mk_comb(mk,datm) in
  84       let newargs = map
  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
  89       let eth = rev_itlist
  90         (fun v th -> CONV_RULE(RAND_CONV BETA_CONV) (AP_THM th v))
  91         newargs dth in
  92       let targs = map (fun v -> mk_comb(mk,mk_comb(eqv,v))) rvs in
  93       let dme_th =
  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
 102       let th2 =
 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
 121       eth,GSYM th9;;
 122
 123 (* ------------------------------------------------------------------------- *)
 124 (* Lifts a theorem. This can be done by higher order rewriting alone.        *)
 125 (*                                                                           *)
 126 (* NB! All and only the first order variables must be bound by quantifiers.  *)
 127 (* ------------------------------------------------------------------------- *)
 128
 129 let lift_theorem =
 130   let pth = prove
 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)`,
 140     STRIP_TAC THEN
 141     SUBGOAL_THEN
 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
 146     CONJ_TAC THENL
 147      [ASM_REWRITE_TAC[] THEN REWRITE_TAC[FUN_EQ_THM] THEN ASM_MESON_TAC[];
 148       ALL_TAC] THEN
 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
 161     fun trths ->
 162       REWRITE_RULE (ith::trths);;