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