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