development/thales/chaff/meson_edit.hl

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