Examples/mizar.ml

   1 (* ========================================================================= *)
   2 (* Mizar-style proofs integrated with the HOL goalstack.                     *)
   3 (*                                                                           *)
   4 (*       John Harrison, University of Cambridge Computer Laboratory          *)
   5 (*                                                                           *)
   6 (*            (c) Copyright, University of Cambridge 1998                    *)
   7 (* ========================================================================= *)
   8
   9 let old_parse_term = parse_term;;
  10
  11 (* ------------------------------------------------------------------------- *)
  12 (* This version of CHOOSE is more convenient to "itlist".                    *)
  13 (* ------------------------------------------------------------------------- *)
  14
  15 let IMP_CHOOSE_RULE =
  16   let P = `P:A->bool`
  17   and Q = `Q:bool`
  18   and pth = prove
  19    (`(!x:A. P x ==> Q) ==> ((?) P ==> Q)`,
  20     GEN_REWRITE_TAC (RAND_CONV o LAND_CONV o RAND_CONV) [GSYM ETA_AX] THEN
  21     REWRITE_TAC[LEFT_IMP_EXISTS_THM]) in
  22   fun v th ->
  23     let ant,con = dest_imp (concl th) in
  24     let pred = mk_abs(v,ant) in
  25     let tm = concl th in
  26     let q = rand tm in
  27     let th1 = BETA_CONV(mk_comb(pred,v)) in
  28     let th2 = PINST [type_of v,aty] [pred,P; q,Q] pth in
  29     let th3 = AP_THM (AP_TERM (rator(rator tm)) th1) q in
  30     let th4 = GEN v (EQ_MP (SYM th3) th) in
  31     MP th2 th4;;
  32
  33 (* ------------------------------------------------------------------------- *)
  34 (* Some preterm operations we need.                                          *)
  35 (* ------------------------------------------------------------------------- *)
  36
  37 let rec split_ppair ptm =
  38   match ptm with
  39     Combp(Combp(Varp(",",dpty),ptm1),ptm2) -> ptm1::(split_ppair ptm2)
  40   | _ -> [ptm];;
  41
  42 let pmk_conj(ptm1,ptm2) =
  43   Combp(Combp(Varp("/\\",dpty),ptm1),ptm2);;
  44
  45 let pmk_exists(v,ptm) =
  46   Combp(Varp("?",dpty),Absp(v,ptm));;
  47
  48 (* ------------------------------------------------------------------------- *)
  49 (* Typecheck a preterm into a term in an environment of (typed) variables.   *)
  50 (* ------------------------------------------------------------------------- *)
  51
  52 let typecheck_in_env env ptm =
  53   let penv = itlist
  54     (fun v acc -> let n,ty = dest_var v in (n,pretype_of_type ty)::acc)
  55     env [] in
  56   (term_of_preterm o retypecheck penv) ptm;;
  57
  58 (* ------------------------------------------------------------------------- *)
  59 (* Converts a labelled preterm (using "and"s) into a single conjunction.     *)
  60 (* ------------------------------------------------------------------------- *)
  61
  62 let delabel lfs = end_itlist (curry pmk_conj) (map snd lfs);;
  63
  64 (* ------------------------------------------------------------------------- *)
  65 (* These special constants are replaced by useful bits when encountered:     *)
  66 (*                                                                           *)
  67 (*  thesis       -- Current thesis (i.e. conclusion of goal).                *)
  68 (*                                                                           *)
  69 (*  antecedent   -- antecedent of goal, if applicable                        *)
  70 (*                                                                           *)
  71 (* contradiction -- falsity                                                  *)
  72 (*                                                                           *)
  73 (*  ...          -- Right hand side of previous conclusion.                  *)
  74 (* ------------------------------------------------------------------------- *)
  75
  76 let thesis = new_definition
  77   `thesis = F`;;
  78
  79 let antecedent = new_definition
  80   `antecedent = F`;;
  81
  82 let contradiction = new_definition
  83   `contradiction = F`;;
  84
  85 let iter_rhs = new_definition
  86   `... = @x:A. F`;;
  87
  88 (* ------------------------------------------------------------------------- *)
  89 (* This function performs the replacement, and typechecks in current env.    *)
  90 (*                                                                           *)
  91 (* The replacement of "..." is done specially, since it also adds a "then".  *)
  92 (* ------------------------------------------------------------------------- *)
  93
  94 let mizarate_term =
  95   let atm = `antecedent`
  96   and ttm = `thesis`
  97   and ctm = `contradiction` in
  98   let f_tm = `F` in
  99   let filter_env fvs =
 100     let env1 = map dest_var fvs in
 101     let sizes = map
 102       (fun (v,_) -> v,length (filter ((=) v o fst) env1)) env1 in
 103     let env2 = filter (fun (v,_) -> assoc v sizes = 1) env1 in
 104     map mk_var env2 in
 105   let goal_lconsts (asl,w) =
 106     itlist (union o frees o concl o snd) asl (frees w) in
 107   fun (asl,w as gl) ptm ->
 108     let lconsts = goal_lconsts gl in
 109     let tm = typecheck_in_env (filter_env lconsts) ptm in
 110     let ant = try fst(dest_imp w) with Failure _ -> atm in
 111     subst [w,ttm; ant,atm; f_tm,ctm] tm;;
 112
 113 (* ------------------------------------------------------------------------- *)
 114 (* The following is occasionally useful as a hack.                           *)
 115 (* ------------------------------------------------------------------------- *)
 116
 117 let LIMITED_REWRITE_CONV =
 118   let LIMITED_ONCE_REWRITE_CONV ths =
 119     GEN_REWRITE_CONV ONCE_DEPTH_CONV ths THENC
 120     GENERAL_REWRITE_CONV true TOP_DEPTH_CONV (basic_net()) [] in
 121   fun n ths tm ->
 122         funpow n (CONV_RULE(RAND_CONV(LIMITED_ONCE_REWRITE_CONV ths)))
 123                  (REFL tm);;
 124
 125 (* ------------------------------------------------------------------------- *)
 126 (* The default prover.                                                       *)
 127 (* ------------------------------------------------------------------------- *)
 128
 129 let DEFAULT_PROVER =
 130   let FREEZE_THENL fn ths x =
 131     let ths' = map (ASSUME o concl) ths in
 132     let th = fn ths' x in
 133     itlist PROVE_HYP ths th in
 134   let REWRITE_PROVER ths tm =
 135     if length ths < 2 then
 136           EQT_ELIM(LIMITED_REWRITE_CONV 3 ths tm)
 137         else
 138            let ths' = tl ths in
 139            let th' = CONV_RULE (LIMITED_REWRITE_CONV 4 ths') (hd ths) in
 140            EQT_ELIM(LIMITED_REWRITE_CONV 4 (th'::ths') tm) in
 141   fun ths tm ->
 142     let sths = itlist (union o CONJUNCTS) ths [] in
 143     try prove(tm,MAP_FIRST MATCH_ACCEPT_TAC sths)
 144     with Failure _ -> try
 145         FREEZE_THENL REWRITE_PROVER ths tm
 146     with Failure _ ->
 147         prove(tm,GEN_MESON_TAC 0 30 1 ths);;
 148
 149 let default_prover = ref DEFAULT_PROVER;;
 150
 151 let prover_list = ref
 152   ["rewriting",(fun ths tm -> EQT_ELIM(REWRITE_CONV ths tm))];;
 153
 154 (* ------------------------------------------------------------------------- *)
 155 (*    "arithmetic",(fun ths tm ->                                            *)
 156 (*                    let tm' = itlist (curry mk_imp o concl) ths tm in      *)
 157 (*                    let th = REAL_ARITH tm' in                             *)
 158 (*                    rev_itlist (C MP) ths th);;                            *)
 159 (* ------------------------------------------------------------------------- *)
 160
 161 (* ------------------------------------------------------------------------- *)
 162 (* Produce a "default" label for various constructs where applicable.        *)
 163 (* ------------------------------------------------------------------------- *)
 164
 165 let default_assumptions = ref false;;
 166
 167 let mklabel s =
 168   if s = "" & !default_assumptions then "*"
 169   else s;;
 170
 171 (* ------------------------------------------------------------------------- *)
 172 (* Augment assumptions, throwing away an *unnamed* previous step.            *)
 173 (* ------------------------------------------------------------------------- *)
 174
 175 let augments =
 176   let augment nw asl =
 177     if asl = [] then [nw]
 178     else if fst(hd asl) = "" then nw::(tl asl)
 179     else nw::asl in
 180   fun labs th asl ->
 181     let ths,thl = nsplit CONJ_PAIR (tl labs) th in
 182     itlist augment (zip (map mklabel labs) (ths@[thl])) asl;;
 183
 184 (* ------------------------------------------------------------------------- *)
 185 (* Wrapper for labels in justification list (use K for preproved theorems).  *)
 186 (* ------------------------------------------------------------------------- *)
 187
 188 let L s asl =
 189   if s = "" then snd(hd asl) else ((assoc s asl):thm);;
 190
 191 (* ------------------------------------------------------------------------- *)
 192 (* Perform justification, given asl and target.                              *)
 193 (* ------------------------------------------------------------------------- *)
 194
 195 let JUSTIFY (prover,tlist) asl tm =
 196   let xthms = map (C I asl) tlist in
 197   let proof_fn =
 198     if prover = "" then !default_prover
 199     else assoc prover (!prover_list) in
 200   let ithms = map snd (filter ((=) "*" o fst) asl) in
 201   proof_fn (xthms @ ithms) tm;;
 202
 203 (* ------------------------------------------------------------------------- *)
 204 (* Either do justification or split off subproof then call ttac with result. *)
 205 (* ------------------------------------------------------------------------- *)
 206
 207 let JUSTIFY_THEN wtm ((pr,tls) as jdata) ttac (asl,w as gl) =
 208   if pr = "proof" then
 209     SUBGOAL_THEN wtm ttac gl
 210   else
 211     let wth = JUSTIFY jdata asl wtm in
 212     ttac wth gl;;
 213
 214 (* ------------------------------------------------------------------------- *)
 215 (* Utilise a conclusion.                                                     *)
 216 (* ------------------------------------------------------------------------- *)
 217
 218 let (MIZAR_CONCLUSION_TAC:thm_tactic) =
 219   let t_tm = `T` in
 220   let CONJ_ASSOC_RULE =
 221     EQT_ELIM o
 222     GEN_REWRITE_RULE RAND_CONV [EQT_INTRO(SPEC_ALL EQ_REFL)] o
 223     PURE_REWRITE_CONV[GSYM CONJ_ASSOC] in
 224   fun th (asl,w as gl) ->
 225     let cjs = conjuncts(concl th) in
 226     let cjs1,cjs2 = chop_list(length cjs) (conjuncts w) in
 227     if cjs2 = [] then
 228       let th' = EQ_MP (CONJ_ASSOC_RULE(mk_eq(concl th,w))) th in
 229       null_meta,[asl,t_tm],fun i _ -> INSTANTIATE i th'
 230     else
 231       let w1 = list_mk_conj cjs1
 232       and w2 = list_mk_conj cjs2 in
 233       let w12 = mk_conj(w1,w2) in
 234       let th' = EQ_MP (CONJ_ASSOC_RULE(mk_eq(concl th,w1))) th in
 235       let wth = CONJ_ASSOC_RULE(mk_eq(w,w12)) in
 236       (SUBST1_TAC wth THEN CONJ_TAC THENL [ACCEPT_TAC th'; ALL_TAC]) gl;;
 237
 238 (* ------------------------------------------------------------------------- *)
 239 (* Transitivity chain stuff; store a list of useful transitivity theorems.   *)
 240 (* ------------------------------------------------------------------------- *)
 241
 242 let mizar_transitivity_net = ref empty_net;;
 243
 244 let add_mizar_transitivity_theorem th =
 245   let pat = fst(dest_imp(snd(strip_forall(concl th)))) in
 246   mizar_transitivity_net :=
 247     enter [] (pat,MATCH_MP th) (!mizar_transitivity_net);;
 248
 249 let TRANSITIVITY_CHAIN th1 th2 ttac =
 250   let tm1 = concl th1
 251   and tm2 = concl th2 in
 252   let th =
 253     if is_eq tm1 then
 254       EQ_MP (SYM (AP_THM (AP_TERM (rator(rator tm2)) th1) (rand tm2))) th2
 255     else if is_eq tm2 then
 256       EQ_MP (AP_TERM (rator tm1) th2) th1
 257     else
 258       let th12 = CONJ th1 th2 in
 259       tryfind (fun rule -> rule th12)
 260         (lookup (concl th12) (!mizar_transitivity_net)) in
 261   ttac th;;
 262
 263 (* ------------------------------------------------------------------------- *)
 264 (* Perform terminal or initial step.                                         *)
 265 (* ------------------------------------------------------------------------- *)
 266
 267 let MIZAR_SUBSTEP_TAC =
 268   fun labs thm (asl,w) ->
 269     let asl' = augments labs thm asl in
 270     null_meta,[asl',w],
 271     K(function [th] -> PROVE_HYP thm th | _ -> fail());;
 272
 273 let MIZAR_BISTEP_TAC =
 274   fun termflag labs jth ->
 275     if termflag then
 276       MIZAR_SUBSTEP_TAC labs jth THEN
 277       MIZAR_CONCLUSION_TAC jth
 278     else
 279       MIZAR_SUBSTEP_TAC labs jth;;
 280
 281 let MIZAR_STEP_TAC =
 282   fun termflag lfs (pr,tls as jdata) (asl,w as gl) ->
 283     let tm = mizarate_term gl (delabel lfs) in
 284     if try fst(dest_const(lhand tm)) = "..." with Failure _ -> false then
 285       let thp = snd(hd asl) in
 286       let lhd = rand(concl thp) in
 287       let tm' = mk_comb(mk_comb(rator(rator tm),lhd),rand tm) in
 288       JUSTIFY_THEN tm' (pr,tls)
 289         (fun th -> TRANSITIVITY_CHAIN thp th
 290                       (MIZAR_BISTEP_TAC termflag (map fst lfs))) gl
 291     else
 292       JUSTIFY_THEN tm (pr,tls)
 293         (MIZAR_BISTEP_TAC termflag (map fst lfs)) gl;;
 294
 295 (* ------------------------------------------------------------------------- *)
 296 (* Perform an "end": finish the trivial goal.                                *)
 297 (* ------------------------------------------------------------------------- *)
 298
 299 let MIZAR_END_TAC = ACCEPT_TAC TRUTH;;
 300
 301 (* ------------------------------------------------------------------------- *)
 302 (* Perform "assume <lform>"                                                  *)
 303 (* ------------------------------------------------------------------------- *)
 304
 305 let (MIZAR_ASSUME_TAC: (string * preterm) list -> tactic) =
 306   let f_tm = `F`
 307   and CONTRA_HACK = CONV_RULE(REWR_CONV(TAUT `(~p ==> F) <=> p`)) in
 308   fun lfs (asl,w as gl) ->
 309     let tm = mizarate_term gl (delabel lfs) in
 310     if try aconv (dest_neg tm) w with Failure _ -> false then
 311       (null_meta,[augments (map fst lfs) (ASSUME tm) asl,f_tm],
 312       (fun i -> function [th] -> CONTRA_HACK(DISCH (instantiate i tm) th)
 313                        | _ -> fail()))
 314     else if try aconv tm (fst(dest_imp w)) with Failure _ -> false then
 315       (null_meta,[augments (map fst lfs) (ASSUME tm) asl,rand w],
 316       (fun i -> function [th] -> DISCH (instantiate i tm) th
 317                        | _ -> fail()))
 318     else failwith "MIZAR_ASSUME_REF: Bad thesis";;
 319
 320 (* ------------------------------------------------------------------------- *)
 321 (* Perform "let <v1>,...,<vn> [be <type>]"                                   *)
 322 (* ------------------------------------------------------------------------- *)
 323
 324 let (MIZAR_LET_TAC: preterm list * hol_type list -> tactic) =
 325   fun (vlist,tys) (asl,w as gl) ->
 326     let ty = if tys = [] then type_of(fst(dest_forall w)) else hd tys in
 327     let pty = pretype_of_type ty in
 328     let mk_varb v =
 329        (term_of_preterm o retypecheck []) (Typing(v,pty)) in
 330     let vs = map mk_varb vlist in
 331     MAP_EVERY X_GEN_TAC vs gl;;
 332
 333 (* ------------------------------------------------------------------------- *)
 334 (* Perform "take <tm>"                                                       *)
 335 (* ------------------------------------------------------------------------- *)
 336
 337 let (MIZAR_TAKE_TAC: preterm -> tactic) =
 338   fun ptm (asl,w as gl) ->
 339     let ptm' = Typing(ptm,pretype_of_type(type_of(fst(dest_exists w)))) in
 340     let tm = mizarate_term (asl,w) ptm' in
 341     EXISTS_TAC tm gl;;
 342
 343 (* ------------------------------------------------------------------------- *)
 344 (* Perform "suffices to prove <form> by <just>".                             *)
 345 (* ------------------------------------------------------------------------- *)
 346
 347 let MIZAR_SUFFICES_TAC =
 348   fun new0 ((pr,tlist) as jdata) (asl,w as gl) ->
 349     let nw = mizarate_term gl (end_itlist (curry pmk_conj) new0) in
 350     JUSTIFY_THEN (mk_imp(nw,w)) jdata
 351       (fun jth (asl,w) ->
 352          null_meta,[asl,nw],
 353          (fun i -> function [th] -> MP (INSTANTIATE_ALL i jth) th
 354                           | _ -> fail())) gl;;
 355
 356 (* ------------------------------------------------------------------------- *)
 357 (* Perform "set <lform>"                                                     *)
 358 (* ------------------------------------------------------------------------- *)
 359
 360 let MIZAR_SET_TAC =
 361   fun (lab,ptm) (asl,w as gl) ->
 362     let tm = mizarate_term gl ptm in
 363     let v,t = dest_eq tm in
 364     CHOOSE_THEN (fun th -> SUBST_ALL_TAC th THEN
 365                            LABEL_TAC (mklabel lab) (SYM th))
 366                 (EXISTS(mk_exists(v,mk_eq(t,v)),t) (REFL t)) gl;;
 367
 368 (* ------------------------------------------------------------------------- *)
 369 (* Perform "consider <vars> such that <lform> by <just>".                    *)
 370 (* ------------------------------------------------------------------------- *)
 371
 372 let MIZAR_CONSIDER_TAC =
 373   fun vars0 lfs ((pr,tls) as jdata) (asl,w as gl) ->
 374     let ptm = itlist (curry pmk_exists) vars0 (delabel lfs) in
 375     let etm = mizarate_term gl ptm in
 376     let vars,tm = nsplit dest_exists vars0 etm in
 377     JUSTIFY_THEN etm jdata
 378       (fun jth (asl,w) ->
 379          null_meta,[augments (map fst lfs) (ASSUME tm) asl,w],
 380          (fun i -> function [th] -> MP (itlist IMP_CHOOSE_RULE vars
 381                                    (DISCH (instantiate i tm) th)) jth
 382                           | _ -> fail())) gl;;
 383
 384 (* ------------------------------------------------------------------------- *)
 385 (* Perform "given <terms> such that <lform>".                                *)
 386 (* ------------------------------------------------------------------------- *)
 387
 388 let MIZAR_GIVEN_TAC =
 389   fun vars0 lfs (asl,w as gl) ->
 390     let ant = fst(dest_imp w) in
 391     let gvars,gbod = nsplit dest_exists vars0 ant in
 392     let tvars = map2
 393       (fun p v -> Typing(p,pretype_of_type(snd(dest_var v)))) vars0 gvars in
 394     let ptm = itlist (curry pmk_exists) tvars (delabel lfs) in
 395     let etm = mizarate_term gl ptm in
 396     let vars,tm = nsplit dest_exists vars0 etm in
 397     if try aconv ant etm with Failure _ -> false then
 398       null_meta,[augments (map fst lfs) (ASSUME tm) asl,rand w],
 399       (fun i -> function [th] -> DISCH ant
 400                      (MP (itlist IMP_CHOOSE_RULE vars
 401                                  (DISCH (instantiate i tm) th))
 402                          (ASSUME ant))
 403                   | _ -> fail())
 404     else failwith "MIZAR_GIVEN_TAC: Bad thesis";;
 405
 406 (* ------------------------------------------------------------------------- *)
 407 (* Initialize a case split.                                                  *)
 408 (* ------------------------------------------------------------------------- *)
 409
 410 let MIZAR_PER_CASES_TAC =
 411   fun jdata (asl,w as gl) ->
 412     null_meta,[gl],
 413     K(function [th] ->
 414         let ghyps = itlist (union o hyp o snd) asl [] in
 415         let rogues = subtract (hyp th) ghyps in
 416         if rogues = [] then th
 417         else if tl rogues = [] then
 418           let thm = JUSTIFY jdata asl (hd rogues) in
 419           PROVE_HYP thm th
 420         else failwith "MIZAR_PER_CASES_ATAC: Too many suppositions"
 421      | _ -> fail());;
 422
 423 (* ------------------------------------------------------------------------- *)
 424 (* Perform a case split. NB! This tactic is not "valid" in the LCF sense.    *)
 425 (* We could make it so, but that would force classical logic!                *)
 426 (* ------------------------------------------------------------------------- *)
 427
 428 let MIZAR_SUPPOSE_TAC =
 429   fun lfs (asl,w as gl) ->
 430     let asm = mizarate_term gl (delabel lfs) in
 431     let ghyps = itlist (union o hyp o snd) asl [] in
 432     null_meta,
 433     [augments (map fst lfs) (ASSUME asm) asl,w; gl],
 434     K(function [th1; th2] ->
 435        let hyp1 = hyp th1
 436        and hyp2 = hyp th2 in
 437        let asm1 = subtract hyp1 ghyps
 438        and asm2 = subtract hyp2 ghyps in
 439        if asm1 = [] then th1 else if asm2 = [] then th2
 440        else if tl asm1 = [] & tl asm2 = [] then
 441          DISJ_CASES (ASSUME(mk_disj(hd asm1,hd asm2))) th1 th2
 442        else failwith "MIZAR_SUPPOSE_TAC: Too many suppositions"
 443      | _ -> fail());;
 444
 445 let MIZAR_SUPPOSE_REF lfs =
 446   by (MIZAR_SUPPOSE_TAC lfs) o by (TRY MIZAR_END_TAC);;
 447
 448 (* ------------------------------------------------------------------------- *)
 449 (* Terminate a case split.                                                   *)
 450 (* ------------------------------------------------------------------------- *)
 451
 452 let MIZAR_RAW_ENDCASE_TAC =
 453   let pth = ITAUT `F ==> p`
 454   and p = `p:bool` in
 455   fun (asl,w) ->
 456     let th = UNDISCH (INST [w,p] pth) in
 457     null_meta,[],fun _ _ -> th;;
 458
 459 let MIZAR_ENDCASE_REF =
 460   by MIZAR_RAW_ENDCASE_TAC o by (TRY MIZAR_END_TAC);;
 461
 462 (* ------------------------------------------------------------------------- *)
 463 (* Parser-processor for textual version of Mizar proofs.                     *)
 464 (* ------------------------------------------------------------------------- *)
 465
 466 let add_mizar_words,subtract_mizar_words =
 467   let l =  ["assume"; "take"; "set"; "given"; "such"; "that";
 468             "proof"; "end"; "consider"; "suffices"; "to"; "show";
 469             "per"; "cases"; "endcase"; "suppose"; "be";
 470             "then"; "thus"; "hence"; "by"; "so"] in
 471   (fun () -> reserve_words l),
 472   (fun () -> unreserve_words l);;
 473
 474 let parse_preform l =
 475   let ptm,rst = parse_preterm l in
 476   let ptm' = Typing(ptm,Ptycon("bool",[])) in
 477   ptm',rst;;
 478
 479 let parse_fulltype l =
 480   let pty,rst = parse_pretype l in
 481   type_of_pretype pty,rst;;
 482
 483 let parse_ident l =
 484   match (hd l) with
 485     Ident n -> n,tl l
 486   | _ -> raise Noparse;;
 487
 488 let parse_string l =
 489   match (hd l) with
 490     Ident n -> n,tl l
 491   | Resword n -> n,tl l;;
 492
 493 let rec parse_lform oldlab l =
 494   match l with
 495     (Ident n)::(Resword ":")::rst ->
 496         if oldlab = "" then parse_lform n rst
 497         else failwith "Too many labels"
 498   | _ -> let fm,rst = parse_preform l in (oldlab,fm),rst;;
 499
 500 let parse_lforms oldlab =
 501   listof (parse_lform oldlab) (a (Resword "and")) "labelled formula";;
 502
 503 let parse_just tlink l =
 504   if l = [] then
 505     if tlink then ("",[L""]),l
 506     else ("",[]),l else
 507   match (hd l) with
 508     Resword "by" ->
 509         let pot,rem = parse_string (tl l) in
 510         if rem = [] or hd rem <> Ident "," & hd rem <> Ident "with" then
 511           if can (assoc pot) (!prover_list) then
 512             (pot,if tlink then [L""] else []),rem
 513           else
 514             ("",if tlink then [L""; L pot] else [L pot]),rem
 515         else if hd rem = Ident "," then
 516           let oths,rst = listof parse_string (a (Ident ",")) "theorem name"
 517            (tl rem) in
 518           let ths = if tlink then ""::pot::oths else pot::oths in
 519           ("",map L ths),rst
 520         else
 521           let oths,rst = listof parse_string (a (Ident ",")) "theorem name"
 522             (tl rem) in
 523           let ths = if tlink then ""::oths else oths in
 524           (pot,map L ths),rst
 525   | Resword "proof" ->
 526         ("proof",[]),tl l
 527   | _ ->
 528         if tlink then ("",[L""]),l
 529         else ("",[]),l;;
 530
 531 let rec parse_step tlink l =
 532    (a (Resword "assume") ++ parse_lforms ""
 533       >> (by o MIZAR_ASSUME_TAC o snd)
 534  || a (Resword "let") ++ (parse_preterm >> split_ppair) ++
 535     possibly (a (Resword "be") ++ parse_fulltype >> snd)
 536     >> (fun ((_,vnames),ty) -> by (MIZAR_LET_TAC (vnames,ty)))
 537  || a (Resword "take") ++ parse_preterm
 538     >> (by o MIZAR_TAKE_TAC o snd)
 539  || a (Resword "set") ++ parse_lforms ""
 540     >> (itlist (by o MIZAR_SET_TAC) o snd)
 541  || a (Resword "consider") ++
 542     (parse_preterm >> split_ppair) ++
 543     a (Resword "such") ++
 544     a (Resword "that") ++
 545     parse_lforms "" ++
 546     parse_just tlink
 547     >> (fun (((((_,vars),_),_),lf),jst) -> by (MIZAR_CONSIDER_TAC vars lf jst))
 548  || a (Resword "given") ++
 549     (parse_preterm >> split_ppair) ++
 550     a (Resword "such") ++
 551     a (Resword "that") ++
 552     parse_lforms ""
 553     >> (fun ((((_,vars),_),_),lf) -> by (MIZAR_GIVEN_TAC vars lf))
 554  || a (Resword "suffices") ++
 555     a (Resword "to") ++
 556     a (Resword "show") ++
 557     parse_lforms "" ++
 558     parse_just tlink
 559     >> (fun ((((_,_),_),lf),jst) -> by (MIZAR_SUFFICES_TAC (map snd lf) jst))
 560  || a (Resword "per") ++
 561     a (Resword "cases") ++
 562     parse_just tlink
 563     >> (fun ((_,_),jst) -> by (MIZAR_PER_CASES_TAC jst))
 564  || a (Resword "suppose") ++
 565     parse_lforms ""
 566     >> (fun (_,lf) -> MIZAR_SUPPOSE_REF lf)
 567  || a (Resword "endcase")
 568     >> K MIZAR_ENDCASE_REF
 569  || a (Resword "end")
 570     >> K (by MIZAR_END_TAC)
 571  || a (Resword "then") ++ parse_step true
 572     >> snd
 573  || a (Resword "so") ++ parse_step true
 574     >> snd
 575  || a (Resword "hence") ++
 576     parse_lforms "" ++
 577     parse_just true
 578     >> (fun ((_,lf),jst) -> by (MIZAR_STEP_TAC true lf jst))
 579  || a (Resword "thus") ++
 580     parse_lforms "" ++
 581     parse_just tlink
 582     >> (fun ((_,lf),jst) -> by (MIZAR_STEP_TAC true lf jst))
 583  || parse_lforms "" ++ parse_just tlink
 584     >> (fun (lf,jst) -> by (MIZAR_STEP_TAC false lf jst))) l;;
 585
 586 (* ------------------------------------------------------------------------- *)
 587 (* From now on, quotations evaluate to preterms.                             *)
 588 (* ------------------------------------------------------------------------- *)
 589
 590 let run_steps lexemes =
 591   let rec compose_steps lexemes gs =
 592     if lexemes = [] then gs else
 593     let rf,rest = parse_step false lexemes in
 594     let gs' = rf gs in
 595     if rest <> [] & hd rest = Resword ";" then compose_steps (tl rest) gs'
 596     else compose_steps rest gs' in
 597   refine (compose_steps lexemes);;
 598
 599 (* ------------------------------------------------------------------------- *)
 600 (* Include some theorems.                                                    *)
 601 (* ------------------------------------------------------------------------- *)
 602
 603 do_list add_mizar_transitivity_theorem
 604   [LE_TRANS; LT_TRANS; LET_TRANS; LTE_TRANS];;
 605
 606 do_list add_mizar_transitivity_theorem
 607   [INT_LE_TRANS; INT_LT_TRANS; INT_LET_TRANS; INT_LTE_TRANS];;
 608
 609 do_list add_mizar_transitivity_theorem
 610   [REAL_LE_TRANS; REAL_LT_TRANS; REAL_LET_TRANS; REAL_LTE_TRANS];;
 611
 612 do_list add_mizar_transitivity_theorem
 613   [SUBSET_TRANS; PSUBSET_TRANS; PSUBSET_SUBSET_TRANS; SUBSET_PSUBSET_TRANS];;
 614
 615 (* ------------------------------------------------------------------------- *)
 616 (* Simple example: Knaster-Tarski fixpoint theorem.                          *)
 617 (* ------------------------------------------------------------------------- *)
 618
 619 add_mizar_words();;
 620
 621 hide_constant "<=";;
 622
 623 (*** Set up goal ***)
 624
 625 g `!f. (!x y. x <= y /\ y <= x ==> (x = y)) /\
 626      (!x y z. x <= y /\ y <= z ==> x <= z) /\
 627      (!x y. x <= y ==> f x <= f y) /\
 628      (!X. ?s:A. (!x. x IN X ==> s <= x) /\
 629                 (!s'. (!x. x IN X ==> s' <= x) ==> s' <= s))
 630      ==> ?x. f x = x`;;
 631
 632 (*** Start parsing quotations as Mizar directives ***)
 633
 634 let parse_term = run_steps o lex o explode;;
 635
 636 (*** Label the external facts needed ***)
 637
 638 e(LABEL_TAC "IN_ELIM_THM" IN_ELIM_THM);;
 639 e(LABEL_TAC "BETA_THM" BETA_THM);;
 640
 641 (*** The proof itself ***)
 642
 643  `let f be A->A;
 644   assume L:antecedent;
 645   antisymmetry: (!x y. x <= y /\ y <= x ==> (x = y)) by L;
 646   transitivity: (!x y z. x <= y /\ y <= z ==> x <= z) by L;
 647   monotonicity: (!x y. x <= y ==> f x <= f y) by L;
 648   least_upper_bound:
 649       (!X. ?s:A. (!x. x IN X ==> s <= x) /\
 650                  (!s'. (!x. x IN X ==> s' <= x) ==> s' <= s)) by L;
 651   set Y_def: Y = {b | f b <= b};
 652   Y_thm: !b. b IN Y <=> f b <= b by Y_def,IN_ELIM_THM,BETA_THM;
 653   consider a such that
 654       lub: (!x. x IN Y ==> a <= x) /\
 655            (!a'. (!x. x IN Y ==> a' <= x) ==> a' <= a)
 656       by least_upper_bound;
 657   take a;
 658   !b. b IN Y ==> f a <= b
 659   proof
 660     let b be A;
 661     assume b_in_Y: b IN Y;
 662     then L0: f b <= b by Y_thm;
 663     a <= b by b_in_Y, lub;
 664     so f a <= f b by monotonicity;
 665     hence f a <= b by L0, transitivity;
 666     end;
 667   so Part1: f(a) <= a by lub;
 668   so f(f(a)) <= f(a) by monotonicity;
 669   so f(a) IN Y by Y_thm;
 670   so a <= f(a) by lub;
 671   hence thesis by Part1, antisymmetry;
 672 end`;;
 673
 674 (*** Get the theorem ***)
 675
 676 top_thm();;
 677
 678 (* ------------------------------------------------------------------------- *)
 679 (* Back to normal.                                                           *)
 680 (* ------------------------------------------------------------------------- *)
 681
 682 let parse_term = old_parse_term;;