Mizarlight/make.ml

   1 (* ========================================================================= *)
   2 (*            "Mizar Light" by Freek Wiedijk.                                *)
   3 (*                                                                           *)
   4 (*        http://www.cs.ru.nl/~freek/mizar/miz.pdf                           *)
   5 (* ========================================================================= *)
   6
   7 exception Innergoal of goal;;
   8
   9 let (GOAL_TAC:tactic) = fun gl -> raise(Innergoal gl);;
  10
  11 let e tac =
  12   try refine(by(VALID tac))
  13   with Innergoal gl ->
  14        let oldgoalstack = !current_goalstack in
  15        current_goalstack := (mk_goalstate gl)::oldgoalstack;
  16        !current_goalstack;;
  17
  18 (* ------------------------------------------------------------------------- *)
  19 (* Set up more infix operators.                                              *)
  20 (* ------------------------------------------------------------------------- *)
  21
  22 Topdirs.dir_directory (!hol_dir);;
  23
  24 Topdirs.load_file Format.std_formatter
  25  (Filename.concat (!hol_dir) "Mizarlight/pa_f.cmo");;
  26
  27 List.iter (fun s -> Hashtbl.add (Pa_j.ht) s true)
  28  ["st'";"st";"at";"from";"by";"using";"proof"; "THEN'"];;
  29
  30 (* ------------------------------------------------------------------------- *)
  31 (* Mizar Light.                                                              *)
  32 (* ------------------------------------------------------------------------- *)
  33
  34 loadt "Mizarlight/miz2a.ml";;
  35
  36 (* ------------------------------------------------------------------------- *)
  37 (* Projective duality proof in Mizar Light.                                  *)
  38 (* ------------------------------------------------------------------------- *)
  39
  40 loadt "Mizarlight/duality.ml";;
  41
  42 (* ------------------------------------------------------------------------- *)
  43 (* A prover more closely approximating Mizar's own.                          *)
  44 (* ------------------------------------------------------------------------- *)
  45
  46 loadt "Examples/holby.ml";;
  47
  48 (* ------------------------------------------------------------------------- *)
  49 (* A version of the duality proof based on that.                             *)
  50 (* ------------------------------------------------------------------------- *)
  51
  52 loadt "Mizarlight/duality_holby.ml";;