pair.ml

   1 (* ========================================================================= *)
   2 (* Syntax sugaring; theory of pairing, with a bit of support.                *)
   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 "quot.ml";;
  11
  12 (* ------------------------------------------------------------------------- *)
  13 (* Constants implementing (or at least tagging) syntactic sugar.             *)
  14 (* ------------------------------------------------------------------------- *)
  15
  16 let LET_DEF = new_definition
  17  `LET (f:A->B) x = f x`;;
  18
  19 let LET_END_DEF = new_definition
  20  `LET_END (t:A) = t`;;
  21
  22 let GABS_DEF = new_definition
  23  `GABS (P:A->bool) = (@) P`;;
  24
  25 let GEQ_DEF = new_definition
  26  `GEQ a b = (a:A = b)`;;
  27
  28 let _SEQPATTERN = new_definition
  29  `_SEQPATTERN = \r s x. if ?y. r x y then r x else s x`;;
  30
  31 let _UNGUARDED_PATTERN = new_definition
  32  `_UNGUARDED_PATTERN = \p r. p /\ r`;;
  33
  34 let _GUARDED_PATTERN = new_definition
  35  `_GUARDED_PATTERN = \p g r. p /\ g /\ r`;;
  36
  37 let _MATCH = new_definition
  38  `_MATCH =  \e r. if (?!) (r e) then (@) (r e) else @z. F`;;
  39
  40 let _FUNCTION = new_definition
  41  `_FUNCTION = \r x. if (?!) (r x) then (@) (r x) else @z. F`;;
  42
  43 (* ------------------------------------------------------------------------- *)
  44 (* Pair type.                                                                *)
  45 (* ------------------------------------------------------------------------- *)
  46
  47 let mk_pair_def = new_definition
  48   `mk_pair (x:A) (y:B) = \a b. (a = x) /\ (b = y)`;;
  49
  50 let PAIR_EXISTS_THM = prove
  51  (`?x. ?(a:A) (b:B). x = mk_pair a b`,
  52   MESON_TAC[]);;
  53
  54 let prod_tybij = new_type_definition
  55   "prod" ("ABS_prod","REP_prod") PAIR_EXISTS_THM;;
  56
  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]);;
  60
  61 parse_as_infix (",",(14,"right"));;
  62
  63 let COMMA_DEF = new_definition
  64  `(x:A),(y:B) = ABS_prod(mk_pair x y)`;;
  65
  66 let FST_DEF = new_definition
  67  `FST (p:A#B) = @x. ?y. p = x,y`;;
  68
  69 let SND_DEF = new_definition
  70  `SND (p:A#B) = @y. ?x. p = x,y`;;
  71
  72 let PAIR_EQ = prove
  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];
  78     ALL_TAC] THEN
  79   MESON_TAC[]);;
  80
  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);;
  90
  91 let FST = prove
  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[]);;
  98
  99 let SND = prove
 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[]);;
 106
 107 let PAIR = prove
 108  (`!x:A#B. FST x,SND x = x`,
 109   GEN_TAC THEN
 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]);;
 113
 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);;
 119
 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]);;
 124
 125 (* ------------------------------------------------------------------------- *)
 126 (* Syntax operations.                                                        *)
 127 (* ------------------------------------------------------------------------- *)
 128
 129 let is_pair = is_binary ",";;
 130
 131 let dest_pair = dest_binary ",";;
 132
 133 let mk_pair =
 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);;
 136
 137 (* ------------------------------------------------------------------------- *)
 138 (* Extend basic rewrites; extend new_definition to allow paired varstructs.  *)
 139 (* ------------------------------------------------------------------------- *)
 140
 141 extend_basic_rewrites [FST; SND; PAIR];;
 142
 143 (* ------------------------------------------------------------------------- *)
 144 (* Extend definitions to paired varstructs with benignity checking.          *)
 145 (* ------------------------------------------------------------------------- *)
 146
 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;
 151   AND_DEF; T_DEF];;
 152
 153 let new_definition =
 154   let depair =
 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
 161                gv,depair gv arg in
 162   fun tm ->
 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')
 168     with Failure _ ->
 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;;
 181
 182 (* ------------------------------------------------------------------------- *)
 183 (* A few more useful definitions.                                            *)
 184 (* ------------------------------------------------------------------------- *)
 185
 186 let CURRY_DEF = new_definition
 187  `CURRY(f:A#B->C) x y = f(x,y)`;;
 188
 189 let UNCURRY_DEF = new_definition
 190  `!f x y. UNCURRY(f:A->B->C)(x,y) = f x y`;;
 191
 192 let PASSOC_DEF = new_definition
 193  `!f x y z. PASSOC (f:(A#B)#C->D) (x,y,z) = f ((x,y),z)`;;
 194
 195 (* ------------------------------------------------------------------------- *)
 196 (* Analog of ABS_CONV for generalized abstraction.                           *)
 197 (* ------------------------------------------------------------------------- *)
 198
 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)));;
 205
 206 (* ------------------------------------------------------------------------- *)
 207 (* General beta-conversion over linear pattern of nested constructors.       *)
 208 (* ------------------------------------------------------------------------- *)
 209
 210 let GEN_BETA_CONV =
 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
 228     let bth =
 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
 236     let mk_projector a =
 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
 244   let GABS_RULE =
 245     let pth = prove
 246      (`(?) P ==> P (GABS P)`,
 247       SIMP_TAC[GABS_DEF; SELECT_AX; ETA_AX]) in
 248     MATCH_MP pth 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
 279   GEN_BETA_CONV;;
 280
 281 (* ------------------------------------------------------------------------- *)
 282 (* Add this to the basic "rewrites" and pairs to the inductive type store.   *)
 283 (* ------------------------------------------------------------------------- *)
 284
 285 extend_basic_convs("GEN_BETA_CONV",(`GABS (\a. b) c`,GEN_BETA_CONV));;
 286
 287 inductive_type_store :=
 288  ("prod",(1,pair_INDUCT,pair_RECURSION))::(!inductive_type_store);;
 289
 290 (* ------------------------------------------------------------------------- *)
 291 (* Convenient rules to eliminate binders over pairs.                         *)
 292 (* ------------------------------------------------------------------------- *)
 293
 294 let FORALL_PAIR_THM = prove
 295  (`!P. (!p. P p) <=> (!p1 p2. P(p1,p2))`,
 296   MESON_TAC[PAIR]);;
 297
 298 let EXISTS_PAIR_THM = prove
 299  (`!P. (?p. P p) <=> ?p1 p2. P(p1,p2)`,
 300   MESON_TAC[PAIR]);;
 301
 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]);;
 305
 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]);;
 311
 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]);;
 317
 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]);;
 322
 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]);;
 326
 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]);;
 330
 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[]);;
 334
 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[]);;
 338
 339 (* ------------------------------------------------------------------------- *)
 340 (* Related theorems for explicitly paired quantifiers.                       *)
 341 (* ------------------------------------------------------------------------- *)
 342
 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]);;
 347
 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]);;
 352
 353 (* ------------------------------------------------------------------------- *)
 354 (* Likewise for tripled quantifiers (could continue with the same proof).    *)
 355 (* ------------------------------------------------------------------------- *)
 356
 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]);;
 361
 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]);;
 366
 367 (* ------------------------------------------------------------------------- *)
 368 (* Expansion of a let-term.                                                  *)
 369 (* ------------------------------------------------------------------------- *)
 370
 371 let let_CONV =
 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
 379     TRANS th1 th2 in
 380   fun tm ->
 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
 385     let es = tl pargs in
 386     let n = length es in
 387     if length vs <> n then failwith "let_CONV" else
 388     (EXPAND_BETAS_CONV THENC lete_CONV) tm;;
 389
 390 let (LET_TAC:tactic) =
 391   let is_trivlet tm =
 392     try let assigs,bod = dest_let tm in
 393         forall (uncurry (=)) assigs
 394     with Failure _ -> false
 395   and PROVE_DEPAIRING_EXISTS =
 396     let pth = prove
 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
 402     fun tm ->
 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
 411   fun (asl,w as gl) ->
 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
 416     let abbrevs =
 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))
 422                        abbrevs in
 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
 427      W(fun (asl',w') ->
 428         let tm' = follow_path path w' in
 429         CONV_TAC(PATH_CONV path (K(let_CONV tm'))))) gl;;