equal.ml

   1 (* ========================================================================= *)
   2 (* Basic equality reasoning including conversionals.                         *)
   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 "printer.ml";;
  11
  12 (* ------------------------------------------------------------------------- *)
  13 (* Type abbreviation for conversions.                                        *)
  14 (* ------------------------------------------------------------------------- *)
  15
  16 type conv = term->thm;;
  17
  18 (* ------------------------------------------------------------------------- *)
  19 (* A bit more syntax.                                                        *)
  20 (* ------------------------------------------------------------------------- *)
  21
  22 let lhand = rand o rator;;
  23
  24 let lhs = fst o dest_eq;;
  25
  26 let rhs = snd o dest_eq;;
  27
  28 (* ------------------------------------------------------------------------- *)
  29 (* Similar to variant, but even avoids constants, and ignores types.         *)
  30 (* ------------------------------------------------------------------------- *)
  31
  32 let mk_primed_var =
  33   let rec svariant avoid s =
  34     if mem s avoid or (can get_const_type s & not(is_hidden s)) then
  35       svariant avoid (s^"'")
  36     else s in
  37   fun avoid v ->
  38     let s,ty = dest_var v in
  39     let s' = svariant (mapfilter (fst o dest_var) avoid) s in
  40     mk_var(s',ty);;
  41
  42 (* ------------------------------------------------------------------------- *)
  43 (* General case of beta-conversion.                                          *)
  44 (* ------------------------------------------------------------------------- *)
  45
  46 let BETA_CONV tm =
  47   try BETA tm with Failure _ ->
  48   try let f,arg = dest_comb tm in
  49       let v = bndvar f in
  50       INST [arg,v] (BETA (mk_comb(f,v)))
  51   with Failure _ -> failwith "BETA_CONV: Not a beta-redex";;
  52
  53 (* ------------------------------------------------------------------------- *)
  54 (* A few very basic derived equality rules.                                  *)
  55 (* ------------------------------------------------------------------------- *)
  56
  57 let AP_TERM tm =
  58   let rth = REFL tm in
  59   fun th -> try MK_COMB(rth,th)
  60             with Failure _ -> failwith "AP_TERM";;
  61
  62 let AP_THM th tm =
  63   try MK_COMB(th,REFL tm)
  64   with Failure _ -> failwith "AP_THM";;
  65
  66 let SYM th =
  67   let tm = concl th in
  68   let l,r = dest_eq tm in
  69   let lth = REFL l in
  70   EQ_MP (MK_COMB(AP_TERM (rator (rator tm)) th,lth)) lth;;
  71
  72 let ALPHA tm1 tm2 =
  73   try TRANS (REFL tm1) (REFL tm2)
  74   with Failure _ -> failwith "ALPHA";;
  75
  76 let ALPHA_CONV v tm =
  77   let res = alpha v tm in
  78   ALPHA tm res;;
  79
  80 let GEN_ALPHA_CONV v tm =
  81   if is_abs tm then ALPHA_CONV v tm else
  82   let b,abs = dest_comb tm in
  83   AP_TERM b (ALPHA_CONV v abs);;
  84
  85 let MK_BINOP op =
  86   let afn = AP_TERM op in
  87   fun (lth,rth) -> MK_COMB(afn lth,rth);;
  88
  89 (* ------------------------------------------------------------------------- *)
  90 (* Terminal conversion combinators.                                          *)
  91 (* ------------------------------------------------------------------------- *)
  92
  93 let (NO_CONV:conv) = fun tm -> failwith "NO_CONV";;
  94
  95 let (ALL_CONV:conv) = REFL;;
  96
  97 (* ------------------------------------------------------------------------- *)
  98 (* Combinators for sequencing, trying, repeating etc. conversions.           *)
  99 (* ------------------------------------------------------------------------- *)
 100
 101 let ((THENC):conv -> conv -> conv) =
 102   fun conv1 conv2 t ->
 103     let th1 = conv1 t in
 104     let th2 = conv2 (rand(concl th1)) in
 105     TRANS th1 th2;;
 106
 107 let ((ORELSEC):conv -> conv -> conv) =
 108   fun conv1 conv2 t ->
 109     try conv1 t with Failure _ -> conv2 t;;
 110
 111 let (FIRST_CONV:conv list -> conv) = end_itlist (fun c1 c2 -> c1 ORELSEC c2);;
 112
 113 let (EVERY_CONV:conv list -> conv) =
 114   fun l -> itlist (fun c1 c2 -> c1 THENC c2) l ALL_CONV;;
 115
 116 let REPEATC =
 117   let rec REPEATC conv t =
 118     ((conv THENC (REPEATC conv)) ORELSEC ALL_CONV) t in
 119   (REPEATC:conv->conv);;
 120
 121 let (CHANGED_CONV:conv->conv) =
 122   fun conv tm ->
 123     let th = conv tm in
 124     let l,r = dest_eq (concl th) in
 125     if aconv l r then failwith "CHANGED_CONV" else th;;
 126
 127 let TRY_CONV conv = conv ORELSEC ALL_CONV;;
 128
 129 (* ------------------------------------------------------------------------- *)
 130 (* Subterm conversions.                                                      *)
 131 (* ------------------------------------------------------------------------- *)
 132
 133 let (RATOR_CONV:conv->conv) =
 134   fun conv tm ->
 135     match tm with
 136       Comb(l,r) -> AP_THM (conv l) r
 137     | _ -> failwith "RATOR_CONV: Not a combination";;
 138
 139 let (RAND_CONV:conv->conv) =
 140   fun conv tm ->
 141    match tm with
 142      Comb(l,r) -> MK_COMB(REFL l,conv r)
 143    |  _ -> failwith "RAND_CONV: Not a combination";;
 144
 145 let LAND_CONV = RATOR_CONV o RAND_CONV;;
 146
 147 let (COMB2_CONV: conv->conv->conv) =
 148   fun lconv rconv tm ->
 149    match tm with
 150      Comb(l,r) -> MK_COMB(lconv l,rconv r)
 151   | _ -> failwith "COMB2_CONV: Not a combination";;
 152
 153 let COMB_CONV = W COMB2_CONV;;
 154
 155 let (ABS_CONV:conv->conv) =
 156   fun conv tm ->
 157     let v,bod = dest_abs tm in
 158     let th = conv bod in
 159     try ABS v th with Failure _ ->
 160     let gv = genvar(type_of v) in
 161     let gbod = vsubst[gv,v] bod in
 162     let gth = ABS gv (conv gbod) in
 163     let gtm = concl gth in
 164     let l,r = dest_eq gtm in
 165     let v' = variant (frees gtm) v in
 166     let l' = alpha v' l and r' = alpha v' r in
 167     EQ_MP (ALPHA gtm (mk_eq(l',r'))) gth;;
 168
 169 let BINDER_CONV conv tm =
 170   if is_abs tm then ABS_CONV conv tm
 171   else RAND_CONV(ABS_CONV conv) tm;;
 172
 173 let SUB_CONV conv tm =
 174   match tm with
 175     Comb(_,_) -> COMB_CONV conv tm
 176   | Abs(_,_) -> ABS_CONV conv tm
 177   | _ -> REFL tm;;
 178
 179 let BINOP_CONV conv tm =
 180   let lop,r = dest_comb tm in
 181   let op,l = dest_comb lop in
 182   MK_COMB(AP_TERM op (conv l),conv r);;
 183
 184 (* ------------------------------------------------------------------------- *)
 185 (* Depth conversions; internal use of a failure-propagating `Boultonized'    *)
 186 (* version to avoid a great deal of reuilding of terms.                      *)
 187 (* ------------------------------------------------------------------------- *)
 188
 189 let (ONCE_DEPTH_CONV: conv->conv),
 190     (DEPTH_CONV: conv->conv),
 191     (REDEPTH_CONV: conv->conv),
 192     (TOP_DEPTH_CONV: conv->conv),
 193     (TOP_SWEEP_CONV: conv->conv) =
 194   let THENQC conv1 conv2 tm =
 195     try let th1 = conv1 tm in
 196         try let th2 = conv2(rand(concl th1)) in TRANS th1 th2
 197         with Failure _ -> th1
 198     with Failure _ -> conv2 tm
 199   and THENCQC conv1 conv2 tm =
 200     let th1 = conv1 tm in
 201     try let th2 = conv2(rand(concl th1)) in TRANS th1 th2
 202     with Failure _ -> th1
 203   and COMB_QCONV conv tm =
 204     match tm with
 205       Comb(l,r) ->
 206         (try let th1 = conv l in
 207              try let th2 = conv r in MK_COMB(th1,th2)
 208              with Failure _ -> AP_THM th1 r
 209          with Failure _ -> AP_TERM l (conv r))
 210     | _ -> failwith "COMB_QCONV: Not a combination" in
 211   let rec REPEATQC conv tm = THENCQC conv (REPEATQC conv) tm in
 212   let SUB_QCONV conv tm =
 213     match tm with
 214       Abs(_,_) -> ABS_CONV conv tm
 215     | _ -> COMB_QCONV conv tm in
 216   let rec ONCE_DEPTH_QCONV conv tm =
 217       (conv ORELSEC (SUB_QCONV (ONCE_DEPTH_QCONV conv))) tm
 218   and DEPTH_QCONV conv tm =
 219     THENQC (SUB_QCONV (DEPTH_QCONV conv))
 220            (REPEATQC conv) tm
 221   and REDEPTH_QCONV conv tm =
 222     THENQC (SUB_QCONV (REDEPTH_QCONV conv))
 223            (THENCQC conv (REDEPTH_QCONV conv)) tm
 224   and TOP_DEPTH_QCONV conv tm =
 225     THENQC (REPEATQC conv)
 226            (THENCQC (SUB_QCONV (TOP_DEPTH_QCONV conv))
 227                     (THENCQC conv (TOP_DEPTH_QCONV conv))) tm
 228   and TOP_SWEEP_QCONV conv tm =
 229     THENQC (REPEATQC conv)
 230            (SUB_QCONV (TOP_SWEEP_QCONV conv)) tm in
 231   (fun c -> TRY_CONV (ONCE_DEPTH_QCONV c)),
 232   (fun c -> TRY_CONV (DEPTH_QCONV c)),
 233   (fun c -> TRY_CONV (REDEPTH_QCONV c)),
 234   (fun c -> TRY_CONV (TOP_DEPTH_QCONV c)),
 235   (fun c -> TRY_CONV (TOP_SWEEP_QCONV c));;
 236
 237 (* ------------------------------------------------------------------------- *)
 238 (* Apply at leaves of op-tree; NB any failures at leaves cause failure.      *)
 239 (* ------------------------------------------------------------------------- *)
 240
 241 let rec DEPTH_BINOP_CONV op conv tm =
 242   match tm with
 243     Comb(Comb(op',l),r) when Pervasives.compare op' op = 0 ->
 244       let l,r = dest_binop op tm in
 245       let lth = DEPTH_BINOP_CONV op conv l
 246       and rth = DEPTH_BINOP_CONV op conv r in
 247       MK_COMB(AP_TERM op' lth,rth)
 248   | _ -> conv tm;;
 249
 250 (* ------------------------------------------------------------------------- *)
 251 (* Follow a path.                                                            *)
 252 (* ------------------------------------------------------------------------- *)
 253
 254 let PATH_CONV =
 255   let rec path_conv s cnv =
 256     match s with
 257       [] -> cnv
 258     | "l"::t -> RATOR_CONV (path_conv t cnv)
 259     | "r"::t -> RAND_CONV (path_conv t cnv)
 260     | _::t -> ABS_CONV (path_conv t cnv) in
 261   fun s cnv -> path_conv (explode s) cnv;;
 262
 263 (* ------------------------------------------------------------------------- *)
 264 (* Follow a pattern                                                          *)
 265 (* ------------------------------------------------------------------------- *)
 266
 267 let PAT_CONV =
 268   let rec PCONV xs pat conv =
 269     if mem pat xs then conv
 270     else if not(exists (fun x -> free_in x pat) xs) then ALL_CONV
 271     else if is_comb pat then
 272       COMB2_CONV (PCONV xs (rator pat) conv) (PCONV xs (rand pat) conv)
 273     else
 274       ABS_CONV (PCONV xs (body pat) conv) in
 275   fun pat -> let xs,pbod = strip_abs pat in PCONV xs pbod;;
 276
 277 (* ------------------------------------------------------------------------- *)
 278 (* Symmetry conversion.                                                      *)
 279 (* ------------------------------------------------------------------------- *)
 280
 281 let SYM_CONV tm =
 282   try let th1 = SYM(ASSUME tm) in
 283       let tm' = concl th1 in
 284       let th2 = SYM(ASSUME tm') in
 285       DEDUCT_ANTISYM_RULE th2 th1
 286   with Failure _ -> failwith "SYM_CONV";;
 287
 288 (* ------------------------------------------------------------------------- *)
 289 (* Conversion to a rule.                                                     *)
 290 (* ------------------------------------------------------------------------- *)
 291
 292 let CONV_RULE (conv:conv) th =
 293   EQ_MP (conv(concl th)) th;;
 294
 295 (* ------------------------------------------------------------------------- *)
 296 (* Substitution conversion.                                                  *)
 297 (* ------------------------------------------------------------------------- *)
 298
 299 let SUBS_CONV ths tm =
 300   try if ths = [] then REFL tm else
 301       let lefts = map (lhand o concl) ths in
 302       let gvs = map (genvar o type_of) lefts in
 303       let pat = subst (zip gvs lefts) tm in
 304       let abs = list_mk_abs(gvs,pat) in
 305       let th = rev_itlist
 306         (fun y x -> CONV_RULE (RAND_CONV BETA_CONV THENC LAND_CONV BETA_CONV)
 307                               (MK_COMB(x,y))) ths (REFL abs) in
 308       if rand(concl th) = tm then REFL tm else th
 309   with Failure _ -> failwith "SUBS_CONV";;
 310
 311 (* ------------------------------------------------------------------------- *)
 312 (* Get a few rules.                                                          *)
 313 (* ------------------------------------------------------------------------- *)
 314
 315 let BETA_RULE = CONV_RULE(REDEPTH_CONV BETA_CONV);;
 316
 317 let GSYM = CONV_RULE(ONCE_DEPTH_CONV SYM_CONV);;
 318
 319 let SUBS ths = CONV_RULE (SUBS_CONV ths);;
 320
 321 (* ------------------------------------------------------------------------- *)
 322 (* A cacher for conversions.                                                 *)
 323 (* ------------------------------------------------------------------------- *)
 324
 325 let CACHE_CONV =
 326   let ALPHA_HACK th =
 327     let tm' = lhand(concl th) in
 328     fun tm -> if tm' = tm then th else TRANS (ALPHA tm tm') th in
 329   fun conv ->
 330     let net = ref empty_net in
 331     fun tm -> try tryfind (fun f -> f tm) (lookup tm (!net))
 332               with Failure _ ->
 333                   let th = conv tm in
 334                   (net := enter [] (tm,ALPHA_HACK th) (!net); th);;