meson.ml

   1 (* ========================================================================= *)
   2 (* Version of the MESON procedure a la PTTP. Various search options.         *)
   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 "canon.ml";;
  11
  12 (* ------------------------------------------------------------------------- *)
  13 (* Some parameters controlling MESON behaviour.                              *)
  14 (* ------------------------------------------------------------------------- *)
  15
  16 let meson_depth = ref false;;   (* Use depth not inference bound.            *)
  17
  18 let meson_prefine = ref true;;  (* Use Plaisted's positive refinement.       *)
  19
  20 let meson_dcutin = ref 1;;      (* Min size for d-and-c optimization cut-in. *)
  21
  22 let meson_skew = ref 3;;        (* Skew proof bias (one side is <= n / skew) *)
  23
  24 let meson_brand = ref false;;   (* Use Brand transformation                  *)
  25
  26 let meson_split_limit = ref 8;; (* Limit of case splits before MESON proper  *)
  27
  28 let meson_chatty = ref false;;  (* Old-style verbose MESON output            *)
  29
  30 (* ------------------------------------------------------------------------- *)
  31 (* Prolog exception.                                                         *)
  32 (* ------------------------------------------------------------------------- *)
  33
  34 exception Cut;;
  35
  36 (* ------------------------------------------------------------------------- *)
  37 (* Shadow syntax for FOL terms in NNF. Functions and predicates have         *)
  38 (* numeric codes, and negation is done by negating the predicate code.       *)
  39 (* ------------------------------------------------------------------------- *)
  40
  41 type fol_term = Fvar of int
  42               | Fnapp of int * fol_term list;;
  43
  44 type fol_atom = int * fol_term list;;
  45
  46 type fol_form = Atom of fol_atom
  47                | Conj of fol_form * fol_form
  48                | Disj of fol_form * fol_form
  49                | Forallq of int * fol_form;;
  50
  51 (* ------------------------------------------------------------------------- *)
  52 (* Type for recording a MESON proof tree.                                    *)
  53 (* ------------------------------------------------------------------------- *)
  54
  55 type fol_goal =
  56   Subgoal of fol_atom * fol_goal list * (int * thm) *
  57              int * (fol_term * int)list;;
  58
  59 (* ------------------------------------------------------------------------- *)
  60 (* General MESON procedure, using assumptions and with settable limits.      *)
  61 (* ------------------------------------------------------------------------- *)
  62
  63 let GEN_MESON_TAC =
  64
  65   let offinc = 10000
  66   and inferences = ref 0 in
  67
  68   (* ----------------------------------------------------------------------- *)
  69   (* Like partition, but with short-circuiting for special situation.        *)
  70   (* ----------------------------------------------------------------------- *)
  71
  72   let qpartition p m =
  73     let rec qpartition l =
  74       if l == m then raise Unchanged else
  75       match l with
  76         [] -> raise Unchanged
  77       | (h::t) -> if p h then
  78                     try let yes,no = qpartition t in h::yes,no
  79                     with Unchanged -> [h],t
  80                   else
  81                     let yes,no = qpartition t in yes,h::no in
  82     function l -> try qpartition l
  83                   with Unchanged -> [],l in
  84
  85   (* ----------------------------------------------------------------------- *)
  86   (* Translate a term (in NNF) into the shadow syntax.                       *)
  87   (* ----------------------------------------------------------------------- *)
  88
  89   let reset_vars,fol_of_var,hol_of_var =
  90     let vstore = ref []
  91     and gstore = ref []
  92     and vcounter = ref 0 in
  93     let inc_vcounter() =
  94       let n = !vcounter in
  95       let m = n + 1 in
  96       if m >= offinc then failwith "inc_vcounter: too many variables" else
  97       (vcounter := m; n) in
  98     let reset_vars() = vstore := []; gstore := []; vcounter := 0 in
  99     let fol_of_var v =
 100       let currentvars = !vstore in
 101       try assoc v currentvars with Failure _ ->
 102       let n = inc_vcounter() in
 103       vstore := (v,n)::currentvars; n in
 104     let hol_of_var v =
 105       try rev_assoc v (!vstore)
 106       with Failure _ -> rev_assoc v (!gstore) in
 107     let hol_of_bumped_var v =
 108       try hol_of_var v with Failure _ ->
 109       let v' = v mod offinc in
 110       let hv' = hol_of_var v' in
 111       let gv = genvar(type_of hv') in
 112       gstore := (gv,v)::(!gstore); gv in
 113     reset_vars,fol_of_var,hol_of_bumped_var in
 114
 115   let reset_consts,fol_of_const,hol_of_const =
 116     let false_tm = `F` in
 117     let cstore = ref ([]:(term * int)list)
 118     and ccounter = ref 2 in
 119     let reset_consts() = cstore := [false_tm,1]; ccounter := 2 in
 120     let fol_of_const c =
 121       let currentconsts = !cstore in
 122       try assoc c currentconsts with Failure _ ->
 123       let n = !ccounter in
 124       ccounter := n + 1; cstore := (c,n)::currentconsts; n in
 125     let hol_of_const c = rev_assoc c (!cstore) in
 126     reset_consts,fol_of_const,hol_of_const in
 127
 128   let rec fol_of_term env consts tm =
 129     if is_var tm & not (mem tm consts) then
 130       Fvar(fol_of_var tm)
 131     else
 132       let f,args = strip_comb tm in
 133       if mem f env then failwith "fol_of_term: higher order" else
 134       let ff = fol_of_const f in
 135       Fnapp(ff,map (fol_of_term env consts) args) in
 136
 137   let fol_of_atom env consts tm =
 138     let f,args = strip_comb tm in
 139     if mem f env then failwith "fol_of_atom: higher order" else
 140     let ff = fol_of_const f in
 141     ff,map (fol_of_term env consts) args in
 142
 143   let fol_of_literal env consts tm =
 144     try let tm' = dest_neg tm in
 145         let p,a = fol_of_atom env consts tm' in
 146         -p,a
 147     with Failure _ -> fol_of_atom env consts tm in
 148
 149   let rec fol_of_form env consts tm =
 150     try let v,bod = dest_forall tm in
 151         let fv = fol_of_var v in
 152         let fbod = fol_of_form (v::env) (subtract consts [v]) bod in
 153         Forallq(fv,fbod)
 154     with Failure _ -> try
 155         let l,r = dest_conj tm in
 156         let fl = fol_of_form env consts l
 157         and fr = fol_of_form env consts r in
 158         Conj(fl,fr)
 159     with Failure _ -> try
 160         let l,r = dest_disj tm in
 161         let fl = fol_of_form env consts l
 162         and fr = fol_of_form env consts r in
 163         Disj(fl,fr)
 164     with Failure _ ->
 165         Atom(fol_of_literal env consts tm) in
 166
 167   (* ----------------------------------------------------------------------- *)
 168   (* Further translation functions for HOL formulas.                         *)
 169   (* ----------------------------------------------------------------------- *)
 170
 171   let rec hol_of_term tm =
 172     match tm with
 173       Fvar v -> hol_of_var v
 174     | Fnapp(f,args) -> list_mk_comb(hol_of_const f,map hol_of_term args) in
 175
 176   let hol_of_atom (p,args) =
 177     list_mk_comb(hol_of_const p,map hol_of_term args) in
 178
 179   let hol_of_literal (p,args) =
 180     if p < 0 then mk_neg(hol_of_atom(-p,args))
 181     else hol_of_atom (p,args) in
 182
 183   (* ----------------------------------------------------------------------- *)
 184   (* Versions of shadow syntax operations with variable bumping.             *)
 185   (* ----------------------------------------------------------------------- *)
 186
 187   let rec fol_free_in v tm =
 188     match tm with
 189       Fvar x -> x = v
 190     | Fnapp(_,lis) -> exists (fol_free_in v) lis in
 191
 192   let rec fol_subst theta tm =
 193     match tm with
 194       Fvar v -> rev_assocd v theta tm
 195     | Fnapp(f,args) ->
 196           let args' = qmap (fol_subst theta) args in
 197           if args' == args then tm else Fnapp(f,args') in
 198
 199   let fol_inst theta ((p,args) as at:fol_atom) =
 200     let args' = qmap (fol_subst theta) args in
 201     if args' == args then at else p,args' in
 202
 203   let rec fol_subst_bump offset theta tm =
 204     match tm with
 205       Fvar v -> if v < offinc then
 206                  let v' = v + offset in
 207                  rev_assocd v' theta (Fvar(v'))
 208                else
 209                  rev_assocd v theta tm
 210     | Fnapp(f,args) ->
 211           let args' = qmap (fol_subst_bump offset theta) args in
 212           if args' == args then tm else Fnapp(f,args') in
 213
 214   let fol_inst_bump offset theta ((p,args) as at:fol_atom) =
 215     let args' = qmap (fol_subst_bump offset theta) args in
 216     if args' == args then at else p,args' in
 217
 218   (* ----------------------------------------------------------------------- *)
 219   (* Main unification function, maintaining a "graph" instantiation.         *)
 220   (* We implicitly apply an offset to variables in the second term, so this  *)
 221   (* is not symmetric between the arguments.                                 *)
 222   (* ----------------------------------------------------------------------- *)
 223
 224   let rec istriv env x t =
 225     match t with
 226       Fvar y -> y = x or
 227                 (try let t' = rev_assoc y env in istriv env x t'
 228                  with Failure "find" -> false)
 229     | Fnapp(f,args) -> exists (istriv env x) args & failwith "cyclic" in
 230
 231   let rec fol_unify offset tm1 tm2 sofar =
 232     match tm1,tm2 with
 233       Fnapp(f,fargs),Fnapp(g,gargs) ->
 234           if f <> g then failwith "" else
 235           itlist2 (fol_unify offset) fargs gargs sofar
 236     | _,Fvar(x) ->
 237          (let x' = x + offset in
 238           try let tm2' = rev_assoc x' sofar in
 239               fol_unify 0 tm1 tm2' sofar
 240           with Failure "find" ->
 241               if istriv sofar x' tm1 then sofar
 242               else (tm1,x')::sofar)
 243     | Fvar(x),_ ->
 244          (try let tm1' = rev_assoc x sofar in
 245               fol_unify offset tm1' tm2 sofar
 246           with Failure "find" ->
 247               let tm2' = fol_subst_bump offset [] tm2 in
 248               if istriv sofar x tm2' then sofar
 249               else (tm2',x)::sofar) in
 250
 251   (* ----------------------------------------------------------------------- *)
 252   (* Test for equality under the pending instantiations.                     *)
 253   (* ----------------------------------------------------------------------- *)
 254
 255   let rec fol_eq insts tm1 tm2 =
 256     tm1 == tm2 or
 257     match tm1,tm2 with
 258       Fnapp(f,fargs),Fnapp(g,gargs) ->
 259           f = g & forall2 (fol_eq insts) fargs gargs
 260     | _,Fvar(x) ->
 261          (try let tm2' = rev_assoc x insts in
 262               fol_eq insts tm1 tm2'
 263           with Failure "find" ->
 264           try istriv insts x tm1 with Failure _ -> false)
 265     | Fvar(x),_ ->
 266          (try let tm1' = rev_assoc x insts in
 267               fol_eq insts tm1' tm2
 268           with Failure "find" ->
 269           try istriv insts x tm2 with Failure _ -> false) in
 270
 271   let fol_atom_eq insts (p1,args1) (p2,args2) =
 272     p1 = p2 & forall2 (fol_eq insts) args1 args2 in
 273
 274   (* ----------------------------------------------------------------------- *)
 275   (* Cacheing continuations. Very crude, but it works remarkably well.       *)
 276   (* ----------------------------------------------------------------------- *)
 277
 278   let cacheconts f =
 279     let memory = ref [] in
 280     fun (gg,(insts,offset,size) as input) ->
 281       if exists (fun (_,(insts',_,size')) ->
 282                      insts = insts' & (size <= size' or !meson_depth))
 283           (!memory)
 284       then failwith "cachecont"
 285       else memory := input::(!memory); f input in
 286
 287   (* ----------------------------------------------------------------------- *)
 288   (* Check ancestor list for repetition.                                     *)
 289   (* ----------------------------------------------------------------------- *)
 290
 291   let checkan insts (p,a) ancestors =
 292     let p' = -p in
 293     let t' = (p',a) in
 294     try let ours = assoc p' ancestors in
 295         if exists (fun u -> fol_atom_eq insts t' (snd(fst u))) ours
 296         then failwith "checkan"
 297         else ancestors
 298     with Failure "find" -> ancestors in
 299
 300   (* ----------------------------------------------------------------------- *)
 301   (* Insert new goal's negation in ancestor clause, given refinement.        *)
 302   (* ----------------------------------------------------------------------- *)
 303
 304   let insertan insts (p,a) ancestors =
 305     let p' = -p in
 306     let t' = (p',a) in
 307     let ourancp,otheranc =
 308       try remove (fun (pr,_) -> pr = p') ancestors
 309       with Failure _ -> (p',[]),ancestors in
 310     let ouranc = snd ourancp in
 311     if exists (fun u -> fol_atom_eq insts t' (snd(fst u))) ouranc
 312     then failwith "insertan: loop"
 313     else (p',(([],t'),(0,TRUTH))::ouranc)::otheranc in
 314
 315   (* ----------------------------------------------------------------------- *)
 316   (* Apply a multi-level "graph" instantiation.                              *)
 317   (* ----------------------------------------------------------------------- *)
 318
 319   let rec fol_subst_partial insts tm =
 320     match tm with
 321       Fvar(v) -> (try let t = rev_assoc v insts in
 322                       fol_subst_partial insts t
 323                   with Failure "find" -> tm)
 324     | Fnapp(f,args) -> Fnapp(f,map (fol_subst_partial insts) args) in
 325
 326   (* ----------------------------------------------------------------------- *)
 327   (* Tease apart local and global instantiations.                            *)
 328   (* At the moment we also force a full evaluation; should eliminate this.   *)
 329   (* ----------------------------------------------------------------------- *)
 330
 331   let separate_insts offset oldinsts newinsts =
 332     let locins,globins =
 333       qpartition (fun (_,v) -> offset <= v) oldinsts newinsts in
 334     if globins = oldinsts then
 335       map (fun (t,x) -> fol_subst_partial newinsts t,x) locins,oldinsts
 336     else
 337       map (fun (t,x) -> fol_subst_partial newinsts t,x) locins,
 338       map (fun (t,x) -> fol_subst_partial newinsts t,x) globins in
 339
 340   (* ----------------------------------------------------------------------- *)
 341   (* Perform basic MESON expansion.                                          *)
 342   (* ----------------------------------------------------------------------- *)
 343
 344   let meson_single_expand loffset rule ((g,ancestors),(insts,offset,size)) =
 345     let (hyps,conc),tag = rule in
 346     let allins = rev_itlist2 (fol_unify loffset) (snd g) (snd conc) insts in
 347     let locin,globin = separate_insts offset insts allins in
 348     let mk_ihyp h =
 349       let h' = fol_inst_bump offset locin h in
 350       h',checkan insts h' ancestors in
 351     let newhyps =  map mk_ihyp hyps in
 352     inferences := !inferences + 1;
 353     newhyps,(globin,offset+offinc,size-length hyps) in
 354
 355   (* ----------------------------------------------------------------------- *)
 356   (* Perform first basic expansion which allows continuation call.           *)
 357   (* ----------------------------------------------------------------------- *)
 358
 359   let meson_expand_cont loffset rules state cont =
 360     tryfind
 361      (fun r -> cont (snd r) (meson_single_expand loffset r state)) rules in
 362
 363   (* ----------------------------------------------------------------------- *)
 364   (* Try expansion and continuation call with ancestor or initial rule.      *)
 365   (* ----------------------------------------------------------------------- *)
 366
 367   let meson_expand rules ((g,ancestors),((insts,offset,size) as tup)) cont =
 368     let pr = fst g in
 369     let newancestors = insertan insts g ancestors in
 370     let newstate = (g,newancestors),tup in
 371     try if !meson_prefine & pr > 0 then failwith "meson_expand" else
 372         let arules = assoc pr ancestors in
 373         meson_expand_cont 0 arules newstate cont
 374     with Cut -> failwith "meson_expand" | Failure _ ->
 375         try let crules =
 376               filter (fun ((h,_),_) -> length h <= size) (assoc pr rules) in
 377             meson_expand_cont offset crules newstate cont
 378         with Cut -> failwith "meson_expand"
 379            | Failure _ -> failwith "meson_expand" in
 380
 381   (* ----------------------------------------------------------------------- *)
 382   (* Simple Prolog engine organizing search and backtracking.                *)
 383   (* ----------------------------------------------------------------------- *)
 384
 385   let expand_goal rules =
 386     let rec expand_goal depth ((g,_),(insts,offset,size) as state) cont =
 387       if depth < 0 then failwith "expand_goal: too deep" else
 388       meson_expand rules state
 389         (fun apprule (_,(pinsts,_,_) as newstate) ->
 390             expand_goals (depth-1) newstate
 391               (cacheconts(fun (gs,(newinsts,newoffset,newsize)) ->
 392                  let locin,globin = separate_insts offset pinsts newinsts in
 393                  let g' = Subgoal(g,gs,apprule,offset,locin) in
 394                  if globin = insts & gs = [] then
 395                    try cont(g',(globin,newoffset,size))
 396                    with Failure _ -> raise Cut
 397                  else
 398                    try cont(g',(globin,newoffset,newsize))
 399                    with Cut -> failwith "expand_goal"
 400                       | Failure _ -> failwith "expand_goal")))
 401
 402     and expand_goals depth (gl,(insts,offset,size as tup)) cont =
 403       match gl with
 404         [] -> cont ([],tup)
 405
 406       | [g] -> expand_goal depth (g,tup) (fun (g',stup) -> cont([g'],stup))
 407
 408       | gl -> if size >= !meson_dcutin then
 409                 let lsize = size / (!meson_skew) in
 410                 let rsize = size - lsize in
 411                 let lgoals,rgoals = chop_list (length gl / 2) gl in
 412                 try expand_goals depth (lgoals,(insts,offset,lsize))
 413                      (cacheconts(fun (lg',(i,off,n)) ->
 414                          expand_goals depth (rgoals,(i,off,n + rsize))
 415                            (cacheconts(fun (rg',ztup) -> cont (lg'@rg',ztup)))))
 416                 with Failure _ ->
 417                     expand_goals depth (rgoals,(insts,offset,lsize))
 418                       (cacheconts(fun (rg',(i,off,n)) ->
 419                          expand_goals depth (lgoals,(i,off,n + rsize))
 420                            (cacheconts (fun (lg',((_,_,fsize) as ztup)) ->
 421                               if n + rsize <= lsize + fsize
 422                               then failwith "repetition of demigoal pair"
 423                               else cont (lg'@rg',ztup)))))
 424               else
 425                 let g::gs = gl in
 426                 expand_goal depth (g,tup)
 427                   (cacheconts(fun (g',stup) ->
 428                       expand_goals depth (gs,stup)
 429                         (cacheconts(fun (gs',ftup) -> cont(g'::gs',ftup))))) in
 430
 431     fun g maxdep maxinf cont ->
 432       expand_goal maxdep (g,([],2 * offinc,maxinf)) cont in
 433
 434   (* ----------------------------------------------------------------------- *)
 435   (* With iterative deepening of inferences or depth.                        *)
 436   (* ----------------------------------------------------------------------- *)
 437
 438   let solve_goal rules incdepth min max incsize =
 439     let rec solve n g =
 440       if n > max then failwith "solve_goal: Too deep" else
 441       (if !meson_chatty & !verbose then
 442         (Format.print_string
 443           ((string_of_int (!inferences))^" inferences so far. "^
 444               "Searching with maximum size "^(string_of_int n)^".");
 445          Format.print_newline())
 446        else if !verbose then
 447         (Format.print_string(string_of_int (!inferences)^"..");
 448          Format.print_flush())
 449        else ());
 450       try let gi =
 451             if incdepth then expand_goal rules g n 100000 (fun x -> x)
 452             else expand_goal rules g 100000 n (fun x -> x) in
 453           (if !meson_chatty & !verbose then
 454             (Format.print_string
 455               ("Goal solved with "^(string_of_int (!inferences))^
 456                " inferences.");
 457              Format.print_newline())
 458            else if !verbose then
 459             (Format.print_string("solved at "^string_of_int (!inferences));
 460              Format.print_newline())
 461            else ());
 462           gi
 463       with Failure _ -> solve (n + incsize) g in
 464     fun g -> solve min (g,[]) in
 465
 466   (* ----------------------------------------------------------------------- *)
 467   (* Creation of tagged contrapositives from a HOL clause.                   *)
 468   (* This includes any possible support clauses (1 = falsity).               *)
 469   (* The rules are partitioned into association lists.                       *)
 470   (* ----------------------------------------------------------------------- *)
 471
 472   let fol_of_hol_clauses =
 473     let eqt (a1,(b1,c1)) (a2, (b2,c2)) =
 474      ((a1 = a2) & (b1 = b2) & (equals_thm c1 c2)) in
 475     let mk_negated (p,a) = -p,a in
 476     let rec mk_contraposes n th used unused sofar =
 477       match unused with
 478         [] -> sofar
 479       | h::t -> let nw = (map mk_negated (used @ t),h),(n,th) in
 480                 mk_contraposes (n + 1) th (used@[h]) t (nw::sofar) in
 481     let fol_of_hol_clause th =
 482       let lconsts = freesl (hyp th) in
 483       let tm = concl th in
 484       let hlits = disjuncts tm in
 485       let flits = map (fol_of_literal [] lconsts) hlits in
 486       let basics = mk_contraposes 0 th [] flits [] in
 487       if forall (fun (p,_) -> p < 0) flits then
 488         ((map mk_negated flits,(1,[])),(-1,th))::basics
 489       else basics in
 490     fun thms ->
 491       let rawrules = itlist (union' eqt o fol_of_hol_clause) thms [] in
 492       let prs = setify (map (fst o snd o fst) rawrules) in
 493       let prules =
 494         map (fun t -> t,filter ((=) t o fst o snd o fst) rawrules) prs in
 495       let srules = sort (fun (p,_) (q,_) -> abs(p) <= abs(q)) prules in
 496       srules in
 497
 498   (* ----------------------------------------------------------------------- *)
 499   (* Optimize set of clauses; changing literal order complicates HOL stuff.  *)
 500   (* ----------------------------------------------------------------------- *)
 501
 502   let optimize_rules =
 503     let optimize_clause_order cls =
 504       sort (fun ((l1,_),_) ((l2,_),_) -> length l1 <= length l2) cls in
 505     map (fun (a,b) -> a,optimize_clause_order b) in
 506
 507   (* ----------------------------------------------------------------------- *)
 508   (* Create a HOL contrapositive on demand, with a cache.                    *)
 509   (* ----------------------------------------------------------------------- *)
 510
 511   let clear_contrapos_cache,make_hol_contrapos =
 512     let DISJ_AC = AC DISJ_ACI
 513     and imp_CONV = REWR_CONV(TAUT `a \/ b <=> ~b ==> a`)
 514     and push_CONV =
 515       GEN_REWRITE_CONV TOP_SWEEP_CONV
 516        [TAUT `~(a \/ b) <=> ~a /\ ~b`; TAUT `~(~a) <=> a`]
 517     and pull_CONV = GEN_REWRITE_CONV DEPTH_CONV
 518        [TAUT `~a \/ ~b <=> ~(a /\ b)`]
 519     and imf_CONV = REWR_CONV(TAUT `~p <=> p ==> F`) in
 520     let memory = ref [] in
 521     let clear_contrapos_cache() = memory := [] in
 522     let make_hol_contrapos (n,th) =
 523       let tm = concl th in
 524       let key = (n,tm) in
 525       try assoc key (!memory) with Failure _ ->
 526       if n < 0 then
 527         CONV_RULE (pull_CONV THENC imf_CONV) th
 528       else
 529         let djs = disjuncts tm in
 530         let acth =
 531           if n = 0 then th else
 532           let ldjs,rdjs = chop_list n djs in
 533           let ndjs = (hd rdjs)::(ldjs@(tl rdjs)) in
 534           EQ_MP (DISJ_AC(mk_eq(tm,list_mk_disj ndjs))) th in
 535         let fth =
 536           if length djs = 1 then acth
 537           else CONV_RULE (imp_CONV THENC push_CONV) acth in
 538         (memory := (key,fth)::(!memory); fth) in
 539     clear_contrapos_cache,make_hol_contrapos in
 540
 541   (* ----------------------------------------------------------------------- *)
 542   (* Translate back the saved proof into HOL.                                *)
 543   (* ----------------------------------------------------------------------- *)
 544
 545   let meson_to_hol =
 546     let hol_negate tm =
 547       try dest_neg tm with Failure _ -> mk_neg tm in
 548     let merge_inst (t,x) current =
 549       (fol_subst current t,x)::current in
 550     let finish_RULE =
 551       GEN_REWRITE_RULE I
 552        [TAUT `(~p ==> p) <=> p`; TAUT `(p ==> ~p) <=> ~p`] in
 553     let rec meson_to_hol insts (Subgoal(g,gs,(n,th),offset,locin)) =
 554       let newins = itlist merge_inst locin insts in
 555       let g' = fol_inst newins g in
 556       let hol_g = hol_of_literal g' in
 557       let ths = map (meson_to_hol newins) gs in
 558       let hth =
 559         if equals_thm th TRUTH then ASSUME hol_g else
 560         let cth = make_hol_contrapos(n,th) in
 561         if ths = [] then cth else MATCH_MP cth (end_itlist CONJ ths) in
 562       let ith = PART_MATCH I hth hol_g in
 563       finish_RULE (DISCH (hol_negate(concl ith)) ith) in
 564     meson_to_hol in
 565
 566   (* ----------------------------------------------------------------------- *)
 567   (* Create equality axioms for all the function and predicate symbols in    *)
 568   (* a HOL term. Not very efficient (but then neither is throwing them into  *)
 569   (* automated proof search!)                                                *)
 570   (* ----------------------------------------------------------------------- *)
 571
 572   let create_equality_axioms =
 573     let eq_thms = (CONJUNCTS o prove)
 574      (`(x:A = x) /\
 575        (~(x:A = y) \/ ~(x = z) \/ (y = z))`,
 576       REWRITE_TAC[] THEN ASM_CASES_TAC `x:A = y` THEN
 577       ASM_REWRITE_TAC[] THEN CONV_TAC TAUT) in
 578     let imp_elim_CONV = REWR_CONV
 579       (TAUT `(a ==> b) <=> ~a \/ b`) in
 580     let eq_elim_RULE =
 581       MATCH_MP(TAUT `(a <=> b) ==> b \/ ~a`) in
 582     let veq_tm = rator(rator(concl(hd eq_thms))) in
 583     let create_equivalence_axioms (eq,_) =
 584       let tyins = type_match (type_of veq_tm) (type_of eq) [] in
 585       map (INST_TYPE tyins) eq_thms in
 586     let rec tm_consts tm acc =
 587       let fn,args = strip_comb tm in
 588       if args = [] then acc
 589       else itlist tm_consts args (insert (fn,length args) acc) in
 590     let rec fm_consts tm ((preds,funs) as acc) =
 591       try fm_consts(snd(dest_forall tm)) acc with Failure _ ->
 592       try fm_consts(snd(dest_exists tm)) acc with Failure _ ->
 593       try let l,r = dest_conj tm in fm_consts l (fm_consts r acc)
 594       with Failure _ -> try
 595           let l,r = dest_disj tm in fm_consts l (fm_consts r acc)
 596       with Failure _ -> try
 597           let l,r = dest_imp tm in fm_consts l (fm_consts r acc)
 598       with Failure _ -> try
 599            fm_consts (dest_neg tm) acc with Failure _ ->
 600       try let l,r = dest_eq tm in
 601           if type_of l = bool_ty
 602           then fm_consts r (fm_consts l acc)
 603           else failwith "atomic equality"
 604       with Failure _ ->
 605       let pred,args = strip_comb tm in
 606       if args = [] then acc else
 607       insert (pred,length args) preds,itlist tm_consts args funs in
 608     let create_congruence_axiom pflag (tm,len) =
 609       let atys,rty = splitlist (fun ty -> let op,l = dest_type ty in
 610                                           if op = "fun" then hd l,hd(tl l)
 611                                           else fail())
 612                                (type_of tm) in
 613       let ctys = fst(chop_list len atys) in
 614       let largs = map genvar ctys
 615       and rargs = map genvar ctys in
 616       let th1 = rev_itlist (C (curry MK_COMB)) (map (ASSUME o mk_eq)
 617           (zip largs rargs)) (REFL tm) in
 618       let th2 = if pflag then eq_elim_RULE th1 else th1 in
 619       itlist (fun e th -> CONV_RULE imp_elim_CONV (DISCH e th)) (hyp th2) th2 in
 620     fun tms -> let preds,funs = itlist fm_consts tms ([],[]) in
 621                let eqs0,noneqs = partition
 622                   (fun (t,_) -> is_const t & fst(dest_const t) = "=") preds in
 623                if eqs0 = [] then [] else
 624                let pcongs = map (create_congruence_axiom true) noneqs
 625                and fcongs = map (create_congruence_axiom false) funs in
 626                let preds1,_ =
 627                  itlist fm_consts (map concl (pcongs @ fcongs)) ([],[]) in
 628                let eqs1 = filter
 629                  (fun (t,_) -> is_const t & fst(dest_const t) = "=") preds1 in
 630                let eqs = union eqs0 eqs1 in
 631                let equivs =
 632                  itlist (union' equals_thm o create_equivalence_axioms)
 633                         eqs [] in
 634                equivs@pcongs@fcongs in
 635
 636   (* ----------------------------------------------------------------------- *)
 637   (* Brand's transformation.                                                 *)
 638   (* ----------------------------------------------------------------------- *)
 639
 640   let perform_brand_modification =
 641     let rec subterms_irrefl lconsts tm acc =
 642       if is_var tm or is_const tm then acc else
 643       let fn,args = strip_comb tm in
 644       itlist (subterms_refl lconsts) args acc
 645     and subterms_refl lconsts tm acc =
 646       if is_var tm then if mem tm lconsts then insert tm acc else acc
 647       else if is_const tm then insert tm acc else
 648       let fn,args = strip_comb tm in
 649       itlist (subterms_refl lconsts) args (insert tm acc) in
 650     let CLAUSIFY = CONV_RULE(REWR_CONV(TAUT `a ==> b <=> ~a \/ b`)) in
 651     let rec BRAND tms th =
 652       if tms = [] then th else
 653       let tm = hd tms in
 654       let gv = genvar (type_of tm) in
 655       let eq = mk_eq(gv,tm) in
 656       let th' = CLAUSIFY (DISCH eq (SUBS [SYM (ASSUME eq)] th))
 657       and tms' = map (subst [gv,tm]) (tl tms) in
 658       BRAND  tms' th' in
 659     let BRAND_CONGS th =
 660       let lconsts = freesl (hyp th) in
 661       let lits = disjuncts (concl th) in
 662       let atoms = map (fun t -> try dest_neg t with Failure _ -> t) lits in
 663       let eqs,noneqs = partition
 664         (fun t -> try fst(dest_const(fst(strip_comb t))) = "="
 665                   with Failure _ -> false) atoms in
 666       let acc = itlist (subterms_irrefl lconsts) noneqs [] in
 667       let uts = itlist
 668         (itlist (subterms_irrefl lconsts) o snd o strip_comb) eqs acc in
 669       let sts = sort (fun s t -> not(free_in s t)) uts in
 670       BRAND sts th in
 671     let BRANDE th =
 672       let tm = concl th in
 673       let l,r = dest_eq tm in
 674       let gv = genvar(type_of l) in
 675       let eq = mk_eq(r,gv) in
 676       CLAUSIFY(DISCH eq (EQ_MP (AP_TERM (rator tm) (ASSUME eq)) th)) in
 677     let LDISJ_CASES th lth rth =
 678       DISJ_CASES th (DISJ1 lth (concl rth)) (DISJ2 (concl lth) rth) in
 679     let ASSOCIATE = CONV_RULE(REWR_CONV(GSYM DISJ_ASSOC)) in
 680     let rec BRAND_TRANS th =
 681       let tm = concl th in
 682       try let l,r = dest_disj tm in
 683           if is_eq l then
 684             let lth = ASSUME l in
 685             let lth1 = BRANDE lth
 686             and lth2 = BRANDE (SYM lth)
 687             and rth = BRAND_TRANS (ASSUME r) in
 688             map (ASSOCIATE o LDISJ_CASES th lth1) rth @
 689             map (ASSOCIATE o LDISJ_CASES th lth2) rth
 690           else
 691             let rth = BRAND_TRANS (ASSUME r) in
 692             map (LDISJ_CASES th (ASSUME l)) rth
 693       with Failure _ ->
 694           if is_eq tm then [BRANDE th; BRANDE (SYM th)]
 695           else [th] in
 696     let find_eqs =
 697       find_terms (fun t -> try fst(dest_const t) = "="
 698                            with Failure _ -> false) in
 699     let REFLEXATE ths =
 700       let eqs = itlist (union o find_eqs o concl) ths [] in
 701       let tys = map (hd o snd o dest_type o snd o dest_const) eqs in
 702       let gvs = map genvar tys in
 703       itlist (fun v acc -> (REFL v)::acc) gvs ths in
 704     fun ths ->
 705       if exists (can (find_term is_eq o concl)) ths then
 706         let ths' = map BRAND_CONGS ths in
 707         let ths'' = itlist (union' equals_thm o BRAND_TRANS) ths' [] in
 708         REFLEXATE ths''
 709       else ths in
 710
 711   (* ----------------------------------------------------------------------- *)
 712   (* Push duplicated copies of poly theorems to match existing assumptions.  *)
 713   (* ----------------------------------------------------------------------- *)
 714
 715   let POLY_ASSUME_TAC =
 716     let rec uniq' eq =
 717       fun l ->
 718         match l with
 719           x::(y::_ as t) -> let t' = uniq' eq t in
 720                               if eq x y then t' else
 721                               if t'==t then l else x::t'
 722         | _ -> l in
 723     let setify' le eq s = uniq' eq (sort le s) in
 724     let rec grab_constants tm acc =
 725       if is_forall tm or is_exists tm then grab_constants (body(rand tm)) acc
 726       else if is_iff tm or is_imp tm or is_conj tm or is_disj tm then
 727         grab_constants (rand tm) (grab_constants (lhand tm) acc)
 728       else if is_neg tm then grab_constants (rand tm) acc
 729       else union (find_terms is_const tm) acc in
 730     let match_consts (tm1,tm2) =
 731       let s1,ty1 = dest_const tm1
 732       and s2,ty2 = dest_const tm2 in
 733       if s1 = s2 then type_match ty1 ty2 []
 734       else failwith "match_consts" in
 735     let polymorph mconsts th =
 736       let tvs = subtract (type_vars_in_term (concl th))
 737                          (unions (map type_vars_in_term (hyp th))) in
 738       if tvs = [] then [th] else
 739       let pconsts = grab_constants (concl th) [] in
 740       let tyins = mapfilter match_consts
 741         (allpairs (fun x y -> x,y) pconsts mconsts) in
 742       let ths' =
 743         setify' (fun th th' -> dest_thm th <= dest_thm th')
 744                 equals_thm (mapfilter (C INST_TYPE th) tyins) in
 745       if ths' = [] then
 746         (warn true "No useful-looking instantiations of lemma"; [th])
 747       else ths' in
 748     let rec polymorph_all mconsts ths acc =
 749       if ths = [] then acc else
 750       let ths' = polymorph mconsts (hd ths) in
 751       let mconsts' = itlist grab_constants (map concl ths') mconsts in
 752       polymorph_all mconsts' (tl ths) (union' equals_thm ths' acc) in
 753     fun ths (asl,w as gl) ->
 754       let mconsts = itlist (grab_constants o concl o snd) asl [] in
 755       let ths' = polymorph_all mconsts ths [] in
 756       MAP_EVERY ASSUME_TAC ths' gl in
 757
 758   (* ----------------------------------------------------------------------- *)
 759   (* Basic HOL MESON procedure.                                              *)
 760   (* ----------------------------------------------------------------------- *)
 761
 762   let SIMPLE_MESON_REFUTE min max inc ths =
 763     clear_contrapos_cache();
 764     inferences := 0;
 765     let old_dcutin = !meson_dcutin in
 766     if !meson_depth then meson_dcutin := 100001 else ();
 767     let ths' = if !meson_brand then perform_brand_modification ths
 768                else ths @ create_equality_axioms (map concl ths) in
 769     let rules = optimize_rules(fol_of_hol_clauses ths') in
 770     let proof,(insts,_,_) =
 771       solve_goal rules (!meson_depth) min max inc (1,[]) in
 772     meson_dcutin := old_dcutin;
 773     meson_to_hol insts proof in
 774
 775   let CONJUNCTS_THEN' ttac cth =
 776     ttac(CONJUNCT1 cth) THEN ttac(CONJUNCT2 cth) in
 777
 778   let PURE_MESON_TAC min max inc gl =
 779     reset_vars(); reset_consts();
 780     (FIRST_ASSUM CONTR_TAC ORELSE
 781      W(ACCEPT_TAC o SIMPLE_MESON_REFUTE min max inc o map snd o fst)) gl in
 782
 783   let QUANT_BOOL_CONV =
 784     PURE_REWRITE_CONV[FORALL_BOOL_THM; EXISTS_BOOL_THM; COND_CLAUSES;
 785                       NOT_CLAUSES; IMP_CLAUSES; AND_CLAUSES; OR_CLAUSES;
 786                       EQ_CLAUSES; FORALL_SIMP; EXISTS_SIMP] in
 787
 788   let rec SPLIT_TAC n g =
 789     ((FIRST_X_ASSUM(CONJUNCTS_THEN' ASSUME_TAC) THEN SPLIT_TAC n) ORELSE
 790      (if n > 0 then FIRST_X_ASSUM DISJ_CASES_TAC THEN SPLIT_TAC (n - 1)
 791       else NO_TAC) ORELSE
 792      ALL_TAC) g in
 793
 794   fun min max step ths ->
 795     REFUTE_THEN ASSUME_TAC THEN
 796     POLY_ASSUME_TAC (map GEN_ALL ths) THEN
 797     W(MAP_EVERY(UNDISCH_TAC o concl o snd) o fst) THEN
 798     SELECT_ELIM_TAC THEN
 799     W(fun (asl,w) -> MAP_EVERY (fun v -> SPEC_TAC(v,v)) (frees w)) THEN
 800     CONV_TAC(PRESIMP_CONV THENC
 801              TOP_DEPTH_CONV BETA_CONV THENC
 802              LAMBDA_ELIM_CONV THENC
 803              CONDS_CELIM_CONV THENC
 804              QUANT_BOOL_CONV) THEN
 805     REPEAT(GEN_TAC ORELSE DISCH_TAC) THEN
 806     REFUTE_THEN ASSUME_TAC THEN
 807     RULE_ASSUM_TAC(CONV_RULE(NNF_CONV THENC SKOLEM_CONV)) THEN
 808     REPEAT (FIRST_X_ASSUM CHOOSE_TAC) THEN
 809     ASM_FOL_TAC THEN
 810     SPLIT_TAC (!meson_split_limit) THEN
 811     RULE_ASSUM_TAC(CONV_RULE(PRENEX_CONV THENC WEAK_CNF_CONV)) THEN
 812     RULE_ASSUM_TAC(repeat
 813      (fun th -> SPEC(genvar(type_of(fst(dest_forall(concl th))))) th)) THEN
 814     REPEAT (FIRST_X_ASSUM (CONJUNCTS_THEN' ASSUME_TAC)) THEN
 815     RULE_ASSUM_TAC(CONV_RULE(ASSOC_CONV DISJ_ASSOC)) THEN
 816     REPEAT (FIRST_X_ASSUM SUBST_VAR_TAC) THEN
 817     PURE_MESON_TAC min max step;;
 818
 819 (* ------------------------------------------------------------------------- *)
 820 (* Common cases.                                                             *)
 821 (* ------------------------------------------------------------------------- *)
 822
 823 let ASM_MESON_TAC = GEN_MESON_TAC 0 50 1;;
 824
 825 let MESON_TAC ths = POP_ASSUM_LIST(K ALL_TAC) THEN ASM_MESON_TAC ths;;
 826
 827 (* ------------------------------------------------------------------------- *)
 828 (* Also introduce a rule.                                                  *)
 829 (* ------------------------------------------------------------------------- *)
 830
 831 let MESON ths tm = prove(tm,MESON_TAC ths);;