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
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
|
(* ========================================================================= *)
(* Proof-objects for HOL-light *)
(* *)
(* Steven Obua, TU Mnchen, December 2004 *)
(* *)
(* based on Sebastian Skalberg's HOL4 proof-objects *)
(* *)
(* dummy proof objects, is used when proof objects are switched off, *)
(* the real thing can be found in proofobjects_trt.ml *)
(* ========================================================================= *)
module type Proofobject_primitives =
sig
type proof
val proof_REFL : term -> proof
val proof_TRANS : proof * proof -> proof
val proof_MK_COMB : proof * proof -> proof
val proof_ASSUME : term -> proof
val proof_EQ_MP : proof -> proof -> proof
val proof_IMPAS : proof -> proof -> proof
val proof_DISCH : proof -> term -> proof
val proof_DEDUCT_ANTISYM_RULE : proof * term -> proof * term -> proof
val proof_BETA : term -> proof
val proof_ABS : term -> proof -> proof
val proof_INST_TYPE : (hol_type * hol_type) list -> proof -> proof
val proof_INST : (term * term) list -> proof -> proof
val proof_new_definition : string -> hol_type -> term -> proof
val proof_CONJ : proof -> proof -> proof
val proof_CONJUNCT1 : proof -> proof
val proof_CONJUNCT2 : proof -> proof
val proof_new_basic_type_definition :
string -> string * string -> term * term -> proof -> proof
val proof_SPEC : term -> proof -> proof
val proof_SYM : proof -> proof
val proof_GEN : proof -> term -> proof
val proof_DISJ1 : proof -> term -> proof
val proof_DISJ2 : proof -> term -> proof
val proof_NOTI : proof -> proof
val proof_NOTE : proof -> proof
val proof_CONTR : proof -> term -> proof
val proof_DISJCASES : proof -> proof -> proof -> proof
val proof_CHOOSE : term -> proof -> proof -> proof
val proof_EXISTS : term -> term -> proof -> proof
val new_axiom_name : string -> string
val proof_new_axiom : string -> term -> proof
val save_proof : string -> proof -> (term option) -> unit
val proof_database : unit -> ((string * proof * (term option)) list)
val export_proofs : string option -> (string * proof * (term option)) list -> unit
val export_saved_proofs : string option -> unit
end;;
module Proofobjects : Proofobject_primitives = struct
type proof = unit -> unit
let dummy () x = x;;
let proof_REFL _ = dummy ()
let proof_TRANS _ = dummy ()
let proof_MK_COMB _ = dummy ()
let proof_ASSUME _ = dummy ()
let proof_EQ_MP _ _ = dummy ()
let proof_IMPAS _ _ = dummy ()
let proof_DISCH _ _ = dummy ()
let proof_DEDUCT_ANTISYM_RULE _ _ = dummy ()
let proof_BETA _ = dummy ()
let proof_ABS _ _ = dummy ()
let proof_INST_TYPE _ _ = dummy ()
let proof_INST _ _ = dummy ()
let proof_new_definition _ _ _ = dummy ()
let proof_CONJ _ _ = dummy ()
let proof_CONJUNCT1 _ = dummy ()
let proof_CONJUNCT2 _ = dummy ()
let proof_new_basic_type_definition _ _ _ _ = dummy ()
let proof_SPEC _ _ = dummy ()
let proof_SYM _ = dummy ()
let proof_GEN _ _ = dummy ()
let proof_DISJ1 _ _ = dummy ()
let proof_DISJ2 _ _ = dummy ()
let proof_NOTI _ = dummy ()
let proof_NOTE _ = dummy ()
let proof_CONTR _ _ = dummy ()
let proof_DISJCASES _ _ _ = dummy ()
let proof_CHOOSE _ _ _ = dummy ()
let proof_EXISTS _ _ _ = dummy ()
let new_axiom_name _ = ""
let proof_new_axiom _ _ = dummy ()
let save_proof _ _ _ = ()
let proof_database _ = []
let export_proofs _ _ = ()
let export_saved_proofs _ = ()
end;;
include Proofobjects;;
|
