drule.ml

   1 (* ========================================================================= *)
   2 (* More sophisticated derived rules including definitions and rewriting.     *)
   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 "bool.ml";;
  11
  12 (* ------------------------------------------------------------------------- *)
  13 (* Type of instantiations, with terms, types and higher-order data.          *)
  14 (* ------------------------------------------------------------------------- *)
  15
  16 type instantiation =
  17   (int * term) list * (term * term) list * (hol_type * hol_type) list;;
  18
  19 (* ------------------------------------------------------------------------- *)
  20 (* The last recourse when all else fails!                                    *)
  21 (* ------------------------------------------------------------------------- *)
  22
  23 let mk_thm(asl,c) =
  24   let ax = new_axiom(itlist (curry mk_imp) (rev asl) c) in
  25   rev_itlist (fun t th -> MP th (ASSUME t)) (rev asl) ax;;
  26
  27 (* ------------------------------------------------------------------------- *)
  28 (* Derived congruence rules; very useful things!                             *)
  29 (* ------------------------------------------------------------------------- *)
  30
  31 let MK_CONJ =
  32   let andtm = `(/\)` in
  33   fun eq1 eq2 -> MK_COMB(AP_TERM andtm eq1,eq2);;
  34
  35 let MK_DISJ =
  36   let ortm = `(\/)` in
  37   fun eq1 eq2 -> MK_COMB(AP_TERM ortm eq1,eq2);;
  38
  39 let MK_FORALL =
  40   let atm = mk_const("!",[]) in
  41   fun v th -> AP_TERM (inst [type_of v,aty] atm) (ABS v th);;
  42
  43 let MK_EXISTS =
  44   let atm = mk_const("?",[]) in
  45   fun v th -> AP_TERM (inst [type_of v,aty] atm) (ABS v th);;
  46
  47 (* ------------------------------------------------------------------------- *)
  48 (* Eliminate the antecedent of a theorem using a conversion/proof rule.      *)
  49 (* ------------------------------------------------------------------------- *)
  50
  51 let MP_CONV (cnv:conv) th =
  52   let l,r = dest_imp(concl th) in
  53   let ath = cnv l in
  54   try MP th (EQT_ELIM ath) with Failure _ -> MP th ath;;
  55
  56 (* ------------------------------------------------------------------------- *)
  57 (* Multiple beta-reduction (we use a slight variant below).                  *)
  58 (* ------------------------------------------------------------------------- *)
  59
  60 let rec BETAS_CONV tm =
  61   match tm with
  62     Comb(Abs(_,_),_) -> BETA_CONV tm
  63   | Comb(Comb(_,_),_) -> (RATOR_CONV BETAS_CONV THENC BETA_CONV) tm
  64   | _ -> failwith "BETAS_CONV";;
  65
  66 (* ------------------------------------------------------------------------- *)
  67 (* Instantiators.                                                            *)
  68 (* ------------------------------------------------------------------------- *)
  69
  70 let (instantiate :instantiation->term->term) =
  71   let betas n tm =
  72     let args,lam = funpow n (fun (l,t) -> (rand t)::l,rator t) ([],tm) in
  73     rev_itlist (fun a l -> let v,b = dest_abs l in vsubst[a,v] b) args lam in
  74   let rec ho_betas bcs pat tm =
  75     if is_var pat or is_const pat then fail() else
  76     try let bv,bod = dest_abs tm in
  77         mk_abs(bv,ho_betas bcs (body pat) bod)
  78     with Failure _ ->
  79         let hop,args = strip_comb pat in
  80         try let n = rev_assoc hop bcs in
  81             if length args = n then betas n tm else fail()
  82         with Failure _ ->
  83             let lpat,rpat = dest_comb pat in
  84             let ltm,rtm = dest_comb tm in
  85             try let lth = ho_betas bcs lpat ltm in
  86                 try let rth = ho_betas bcs rpat rtm in
  87                     mk_comb(lth,rth)
  88                 with Failure _ ->
  89                     mk_comb(lth,rtm)
  90             with Failure _ ->
  91                 let rth = ho_betas bcs rpat rtm in
  92                 mk_comb(ltm,rth) in
  93   fun (bcs,tmin,tyin) tm ->
  94     let itm = if tyin = [] then tm else inst tyin tm in
  95     if tmin = [] then itm else
  96     let ttm = vsubst tmin itm in
  97     if bcs = [] then ttm else
  98     try ho_betas bcs itm ttm with Failure _ -> ttm;;
  99
 100 let (INSTANTIATE : instantiation->thm->thm) =
 101   let rec BETAS_CONV n tm =
 102     if n = 1 then TRY_CONV BETA_CONV tm else
 103     (RATOR_CONV (BETAS_CONV (n-1)) THENC
 104      TRY_CONV BETA_CONV) tm in
 105   let rec HO_BETAS bcs pat tm =
 106     if is_var pat or is_const pat then fail() else
 107     try let bv,bod = dest_abs tm in
 108         ABS bv (HO_BETAS bcs (body pat) bod)
 109     with Failure _ ->
 110         let hop,args = strip_comb pat in
 111         try let n = rev_assoc hop bcs in
 112             if length args = n then BETAS_CONV n tm else fail()
 113         with Failure _ ->
 114             let lpat,rpat = dest_comb pat in
 115             let ltm,rtm = dest_comb tm in
 116             try let lth = HO_BETAS bcs lpat ltm in
 117                 try let rth = HO_BETAS bcs rpat rtm in
 118                     MK_COMB(lth,rth)
 119                 with Failure _ ->
 120                     AP_THM lth rtm
 121             with Failure _ ->
 122                 let rth = HO_BETAS bcs rpat rtm in
 123                 AP_TERM ltm rth in
 124   fun (bcs,tmin,tyin) th ->
 125     let ith = if tyin = [] then th else INST_TYPE tyin th in
 126     if tmin = [] then ith else
 127     let tth = INST tmin ith in
 128     if hyp tth = hyp th then
 129       if bcs = [] then tth else
 130       try let eth = HO_BETAS bcs (concl ith) (concl tth) in
 131           EQ_MP eth tth
 132       with Failure _ -> tth
 133     else failwith "INSTANTIATE: term or type var free in assumptions";;
 134
 135 let (INSTANTIATE_ALL : instantiation->thm->thm) =
 136   fun ((_,tmin,tyin) as i) th ->
 137     if tmin = [] & tyin = [] then th else
 138     let hyps = hyp th in
 139     if hyps = [] then INSTANTIATE i th else
 140     let tyrel,tyiirel =
 141       if tyin = [] then [],hyps else
 142       let tvs = itlist (union o tyvars o snd) tyin [] in
 143       partition (fun tm -> let tvs' = type_vars_in_term tm in
 144                            not(intersect tvs tvs' = [])) hyps in
 145     let tmrel,tmirrel =
 146       if tmin = [] then [],tyiirel else
 147       let vs = itlist (union o frees o snd) tmin [] in
 148       partition (fun tm -> let vs' = frees tm in
 149                            not (intersect vs vs' = [])) tyiirel in
 150     let rhyps = union tyrel tmrel in
 151     let th1 = rev_itlist DISCH rhyps th in
 152     let th2 = INSTANTIATE i th1 in
 153     funpow (length rhyps) UNDISCH th2;;
 154
 155 (* ------------------------------------------------------------------------- *)
 156 (* Higher order matching of terms.                                           *)
 157 (*                                                                           *)
 158 (* Note: in the event of spillover patterns, this may return false results;  *)
 159 (* but there's usually an implicit check outside that the match worked       *)
 160 (* anyway. A test could be put in (see if any "env" variables are left in    *)
 161 (* the term after abstracting out the pattern instances) but it'd be slower. *)
 162 (* ------------------------------------------------------------------------- *)
 163
 164 let (term_match:term list -> term -> term -> instantiation) =
 165   let safe_inserta ((y,x) as n) l =
 166     try let z = rev_assoc x l in
 167         if aconv y z then l else failwith "safe_inserta"
 168     with Failure "find" -> n::l in
 169
 170   let safe_insert ((y,x) as n) l =
 171     try let z = rev_assoc x l in
 172         if Pervasives.compare y z = 0 then l else failwith "safe_insert"
 173     with Failure "find" -> n::l in
 174
 175   let mk_dummy =
 176     let name = fst(dest_var(genvar aty)) in
 177     fun ty -> mk_var(name,ty) in
 178
 179   let rec term_pmatch lconsts env vtm ctm ((insts,homs) as sofar) =
 180     match (vtm,ctm) with
 181       Var(_,_),_ ->
 182        (try let ctm' = rev_assoc vtm env in
 183             if Pervasives.compare ctm' ctm = 0 then sofar
 184             else failwith "term_pmatch"
 185         with Failure "find" ->
 186             if mem vtm lconsts then
 187               if Pervasives.compare ctm vtm = 0 then sofar
 188               else failwith "term_pmatch: can't instantiate local constant"
 189             else safe_inserta (ctm,vtm) insts,homs)
 190     | Const(vname,vty),Const(cname,cty) ->
 191         if Pervasives.compare vname cname = 0 then
 192           if Pervasives.compare vty cty = 0 then sofar
 193           else safe_insert (mk_dummy cty,mk_dummy vty) insts,homs
 194         else failwith "term_pmatch"
 195     | Abs(vv,vbod),Abs(cv,cbod) ->
 196         let sofar' = safe_insert
 197           (mk_dummy(snd(dest_var cv)),mk_dummy(snd(dest_var vv))) insts,homs in
 198         term_pmatch lconsts ((cv,vv)::env) vbod cbod sofar'
 199     | _ ->
 200       let vhop = repeat rator vtm in
 201       if is_var vhop & not (mem vhop lconsts) &
 202                        not (can (rev_assoc vhop) env) then
 203         let vty = type_of vtm and cty = type_of ctm in
 204         let insts' =
 205           if Pervasives.compare vty cty = 0 then insts
 206           else safe_insert (mk_dummy cty,mk_dummy vty) insts in
 207         (insts',(env,ctm,vtm)::homs)
 208       else
 209         let lv,rv = dest_comb vtm
 210         and lc,rc = dest_comb ctm in
 211         let sofar' = term_pmatch lconsts env lv lc sofar in
 212         term_pmatch lconsts env rv rc sofar' in
 213
 214   let get_type_insts insts =
 215     itlist (fun (t,x) -> type_match (snd(dest_var x)) (type_of t)) insts in
 216
 217   let separate_insts insts =
 218       let realinsts,patterns = partition (is_var o snd) insts in
 219       let betacounts =
 220         if patterns = [] then [] else
 221         itlist
 222           (fun (_,p) sof ->
 223             let hop,args = strip_comb p in
 224             try safe_insert (length args,hop) sof with Failure _ ->
 225             (warn true "Inconsistent patterning in higher order match"; sof))
 226           patterns [] in
 227       let tyins = get_type_insts realinsts [] in
 228       betacounts,
 229       mapfilter (fun (t,x) ->
 230         let x' = let xn,xty = dest_var x in
 231                  mk_var(xn,type_subst tyins xty) in
 232         if Pervasives.compare t x' = 0 then fail() else (t,x')) realinsts,
 233       tyins in
 234
 235   let rec term_homatch lconsts tyins (insts,homs) =
 236     if homs = [] then insts else
 237     let (env,ctm,vtm) = hd homs in
 238     if is_var vtm then
 239       if Pervasives.compare ctm vtm = 0
 240        then term_homatch lconsts tyins (insts,tl homs) else
 241       let newtyins = safe_insert (type_of ctm,snd(dest_var vtm)) tyins
 242       and newinsts = (ctm,vtm)::insts in
 243       term_homatch lconsts newtyins (newinsts,tl homs) else
 244     let vhop,vargs = strip_comb vtm in
 245     let afvs = freesl vargs in
 246     let inst_fn = inst tyins in
 247     try let tmins = map
 248           (fun a -> (try rev_assoc a env with Failure _ -> try
 249                          rev_assoc a insts with Failure _ ->
 250                          if mem a lconsts then a else fail()),
 251                     inst_fn a) afvs in
 252         let pats0 = map inst_fn vargs in
 253         let pats = map (vsubst tmins) pats0 in
 254         let vhop' = inst_fn vhop in
 255         let ni =
 256           let chop,cargs = strip_comb ctm in
 257           if Pervasives.compare cargs pats = 0 then
 258             if Pervasives.compare chop vhop = 0
 259             then insts else safe_inserta (chop,vhop) insts else
 260           let ginsts = map
 261             (fun p -> (if is_var p then p else genvar(type_of p)),p) pats in
 262           let ctm' = subst ginsts ctm
 263           and gvs = map fst ginsts in
 264           let abstm = list_mk_abs(gvs,ctm') in
 265           let vinsts = safe_inserta (abstm,vhop) insts in
 266           let icpair = ctm',list_mk_comb(vhop',gvs) in
 267           icpair::vinsts in
 268         term_homatch lconsts tyins (ni,tl homs)
 269     with Failure _ ->
 270         let lc,rc = dest_comb ctm
 271         and lv,rv = dest_comb vtm in
 272         let pinsts_homs' =
 273           term_pmatch lconsts env rv rc (insts,(env,lc,lv)::(tl homs)) in
 274         let tyins' = get_type_insts (fst pinsts_homs') [] in
 275         term_homatch lconsts tyins' pinsts_homs' in
 276
 277   fun lconsts vtm ctm ->
 278     let pinsts_homs = term_pmatch lconsts [] vtm ctm ([],[]) in
 279     let tyins = get_type_insts (fst pinsts_homs) [] in
 280     let insts = term_homatch lconsts tyins pinsts_homs in
 281     separate_insts insts;;
 282
 283 (* ------------------------------------------------------------------------- *)
 284 (* First order unification (no type instantiation -- yet).                   *)
 285 (* ------------------------------------------------------------------------- *)
 286
 287 let (term_unify:term list -> term -> term -> instantiation) =
 288   let augment1 sofar (s,x) =
 289     let s' = subst sofar s in
 290     if vfree_in x s & not (s = x) then failwith "augment_insts"
 291     else (s',x) in
 292   let raw_augment_insts p insts =
 293     p::(map (augment1 [p]) insts) in
 294   let augment_insts(t,v) insts =
 295     let t' = vsubst insts t in
 296     if t' = v then insts
 297     else if vfree_in v t' then failwith "augment_insts"
 298     else raw_augment_insts (t',v) insts in
 299   let rec unify vars tm1 tm2 sofar =
 300     if tm1 = tm2 then sofar
 301     else if is_var tm1 & mem tm1 vars then
 302       try let tm1' = rev_assoc tm1 sofar in
 303           unify vars tm1' tm2 sofar
 304       with Failure "find" ->
 305           augment_insts (tm2,tm1) sofar
 306     else if is_var tm2 & mem tm2 vars then
 307        try let tm2' = rev_assoc tm2 sofar in
 308           unify vars tm1 tm2' sofar
 309       with Failure "find" ->
 310           augment_insts (tm1,tm2) sofar
 311     else if is_abs tm1 then
 312       let tm1' = body tm1
 313       and tm2' = subst [bndvar tm1,bndvar tm2] (body tm2) in
 314       unify vars tm1' tm2' sofar
 315     else
 316       let l1,r1 = dest_comb tm1
 317       and l2,r2 = dest_comb tm2 in
 318       unify vars l1 l2 (unify vars r1 r2 sofar) in
 319   fun vars tm1 tm2 -> [],unify vars tm1 tm2 [],[];;
 320
 321 (* ------------------------------------------------------------------------- *)
 322 (* Modify bound variable names at depth. (Not very efficient...)             *)
 323 (* ------------------------------------------------------------------------- *)
 324
 325 let deep_alpha =
 326   let tryalpha v tm =
 327     try alpha v tm
 328     with Failure _ -> try
 329         let v' = variant (frees tm) v in
 330         alpha v' tm
 331     with Failure _ -> tm in
 332   let rec deep_alpha env tm =
 333     if env = [] then tm else
 334     try let v,bod = dest_abs tm in
 335         let vn,vty = dest_var v in
 336         try let (vn',_),newenv = remove (fun (_,x) -> x = vn) env in
 337             let v' = mk_var(vn',vty) in
 338             let tm' = tryalpha v' tm in
 339             let iv,ib = dest_abs tm' in
 340             mk_abs(iv,deep_alpha newenv ib)
 341         with Failure _ -> mk_abs(v,deep_alpha env bod)
 342     with Failure _ -> try
 343         let l,r = dest_comb tm in
 344         mk_comb(deep_alpha env l,deep_alpha env r)
 345     with Failure _ -> tm in
 346   deep_alpha;;
 347
 348 (* ------------------------------------------------------------------------- *)
 349 (* Instantiate theorem by matching part of it to a term.                     *)
 350 (* The GEN_PART_MATCH version renames free vars to avoid clashes.            *)
 351 (* ------------------------------------------------------------------------- *)
 352
 353 let PART_MATCH,GEN_PART_MATCH =
 354   let rec match_bvs t1 t2 acc =
 355     try let v1,b1 = dest_abs t1
 356         and v2,b2 = dest_abs t2 in
 357         let n1 = fst(dest_var v1) and n2 = fst(dest_var v2) in
 358         let newacc = if n1 = n2 then acc else insert (n1,n2) acc in
 359         match_bvs b1 b2 newacc
 360     with Failure _ -> try
 361         let l1,r1 = dest_comb t1
 362         and l2,r2 = dest_comb t2 in
 363         match_bvs l1 l2 (match_bvs r1 r2 acc)
 364     with Failure _ -> acc in
 365   let PART_MATCH partfn th =
 366     let sth = SPEC_ALL th in
 367     let bod = concl sth in
 368     let pbod = partfn bod in
 369     let lconsts = intersect (frees (concl th)) (freesl(hyp th)) in
 370     fun tm ->
 371       let bvms = match_bvs tm pbod [] in
 372       let abod = deep_alpha bvms bod in
 373       let ath = EQ_MP (ALPHA bod abod) sth in
 374       let insts = term_match lconsts (partfn abod) tm in
 375       let fth = INSTANTIATE insts ath in
 376       if hyp fth <> hyp ath then failwith "PART_MATCH: instantiated hyps" else
 377       let tm' = partfn (concl fth) in
 378       if Pervasives.compare tm' tm = 0 then fth else
 379       try SUBS[ALPHA tm' tm] fth
 380       with Failure _ -> failwith "PART_MATCH: Sanity check failure"
 381   and GEN_PART_MATCH partfn th =
 382     let sth = SPEC_ALL th in
 383     let bod = concl sth in
 384     let pbod = partfn bod in
 385     let lconsts = intersect (frees (concl th)) (freesl(hyp th)) in
 386     let fvs = subtract (subtract (frees bod) (frees pbod)) lconsts in
 387     fun tm ->
 388       let bvms = match_bvs tm pbod [] in
 389       let abod = deep_alpha bvms bod in
 390       let ath = EQ_MP (ALPHA bod abod) sth in
 391       let insts = term_match lconsts (partfn abod) tm in
 392       let eth = INSTANTIATE insts (GENL fvs ath) in
 393       let fth = itlist (fun v th -> snd(SPEC_VAR th)) fvs eth in
 394       if hyp fth <> hyp ath then failwith "PART_MATCH: instantiated hyps" else
 395       let tm' = partfn (concl fth) in
 396       if Pervasives.compare tm' tm = 0 then fth else
 397       try SUBS[ALPHA tm' tm] fth
 398       with Failure _ -> failwith "PART_MATCH: Sanity check failure" in
 399   PART_MATCH,GEN_PART_MATCH;;
 400
 401 (* ------------------------------------------------------------------------- *)
 402 (* Matching modus ponens.                                                    *)
 403 (* ------------------------------------------------------------------------- *)
 404
 405 let MATCH_MP ith =
 406   let sth =
 407     try let tm = concl ith in
 408         let avs,bod = strip_forall tm in
 409         let ant,con = dest_imp bod in
 410         let svs,pvs = partition (C vfree_in ant) avs in
 411         if pvs = [] then ith else
 412         let th1 = SPECL avs (ASSUME tm) in
 413         let th2 = GENL svs (DISCH ant (GENL pvs (UNDISCH th1))) in
 414         MP (DISCH tm th2) ith
 415     with Failure _ -> failwith "MATCH_MP: Not an implication" in
 416   let match_fun = PART_MATCH (fst o dest_imp) sth in
 417   fun th -> try MP (match_fun (concl th)) th
 418             with Failure _ -> failwith "MATCH_MP: No match";;
 419
 420 (* ------------------------------------------------------------------------- *)
 421 (* Useful instance of more general higher order matching.                    *)
 422 (* ------------------------------------------------------------------------- *)
 423
 424 let HIGHER_REWRITE_CONV =
 425   let BETA_VAR =
 426     let rec BETA_CONVS n =
 427       if n = 1 then TRY_CONV BETA_CONV else
 428       RATOR_CONV (BETA_CONVS (n - 1)) THENC TRY_CONV BETA_CONV in
 429     let rec free_beta v tm =
 430       if is_abs tm then
 431         let bv,bod = dest_abs tm in
 432         if v = bv then failwith "unchanged" else
 433         ABS_CONV(free_beta v bod) else
 434       let op,args = strip_comb tm in
 435       if args = [] then failwith "unchanged" else
 436       if op = v then BETA_CONVS (length args) else
 437       let l,r = dest_comb tm in
 438       try let lconv = free_beta v l in
 439           (try let rconv = free_beta v r in
 440                COMB2_CONV lconv rconv
 441            with Failure _ -> RATOR_CONV lconv)
 442       with Failure _ -> RAND_CONV (free_beta v r) in
 443     free_beta in
 444   let GINST th =
 445     let fvs = subtract (frees(concl th)) (freesl (hyp th)) in
 446     let gvs = map (genvar o type_of) fvs in
 447     INST (zip gvs fvs) th in
 448   fun ths ->
 449     let thl = map (GINST o SPEC_ALL) ths in
 450     let concs = map concl thl in
 451     let lefts = map lhs concs in
 452     let preds,pats = unzip(map dest_comb lefts) in
 453     let beta_fns = map2 BETA_VAR preds concs in
 454     let ass_list = zip pats (zip preds (zip thl beta_fns)) in
 455     let mnet = itlist (fun p n -> enter [] (p,p) n) pats empty_net in
 456     let look_fn t =
 457       mapfilter (fun p -> if can (term_match [] p) t then p else fail())
 458                 (lookup t mnet) in
 459     fun top tm ->
 460       let pred t = not (look_fn t = []) & free_in t tm in
 461       let stm = if top then find_term pred tm
 462                 else hd(sort free_in (find_terms pred tm)) in
 463       let pat = hd(look_fn stm) in
 464       let _,tmin,tyin = term_match [] pat stm in
 465       let pred,(th,beta_fn) = assoc pat ass_list in
 466       let gv = genvar(type_of stm) in
 467       let abs = mk_abs(gv,subst[gv,stm] tm) in
 468       let _,tmin0,tyin0 = term_match [] pred abs in
 469       CONV_RULE beta_fn (INST tmin (INST tmin0 (INST_TYPE tyin0 th)));;
 470
 471 (* ------------------------------------------------------------------------- *)
 472 (* Derived principle of definition justifying |- c x1 .. xn = t[x1,..,xn]    *)
 473 (* ------------------------------------------------------------------------- *)
 474
 475 let new_definition tm =
 476   let avs,bod = strip_forall tm in
 477   let l,r = try dest_eq bod
 478     with Failure _ -> failwith "new_definition: Not an equation" in
 479   let lv,largs = strip_comb l in
 480   let rtm = try list_mk_abs(largs,r)
 481     with Failure _ -> failwith "new_definition: Non-variable in LHS pattern" in
 482   let def = mk_eq(lv,rtm) in
 483   let th1 = new_basic_definition def in
 484   let th2 = rev_itlist
 485     (fun tm th -> let ith = AP_THM th tm in
 486                   TRANS ith (BETA_CONV(rand(concl ith)))) largs th1 in
 487   let rvs = filter (not o C mem avs) largs in
 488   itlist GEN rvs (itlist GEN avs th2);;