1 (* ========================================================================= *)
2 (* Proof-objects for HOL-light *)
4 (* Steven Obua, TU München, December 2004 *)
6 (* based on Sebastian Skalberg's HOL4 proof-objects *)
8 (* dummy proof objects, is used when proof objects are switched off, *)
9 (* the real thing can be found in proofobjects_trt.ml *)
10 (* ========================================================================= *)
12 module type Proofobject_primitives =
17 val proof_REFL : term -> proof
18 val proof_TRANS : proof * proof -> proof
19 val proof_MK_COMB : proof * proof -> proof
20 val proof_ASSUME : term -> proof
21 val proof_EQ_MP : proof -> proof -> proof
22 val proof_IMPAS : proof -> proof -> proof
23 val proof_DISCH : proof -> term -> proof
24 val proof_DEDUCT_ANTISYM_RULE : proof * term -> proof * term -> proof
25 val proof_BETA : term -> proof
26 val proof_ABS : term -> proof -> proof
27 val proof_INST_TYPE : (hol_type * hol_type) list -> proof -> proof
28 val proof_INST : (term * term) list -> proof -> proof
29 val proof_new_definition : string -> hol_type -> term -> proof
30 val proof_CONJ : proof -> proof -> proof
31 val proof_CONJUNCT1 : proof -> proof
32 val proof_CONJUNCT2 : proof -> proof
33 val proof_new_basic_type_definition :
34 string -> string * string -> term * term -> proof -> proof
35 val proof_SPEC : term -> proof -> proof
36 val proof_SYM : proof -> proof
37 val proof_GEN : proof -> term -> proof
38 val proof_DISJ1 : proof -> term -> proof
39 val proof_DISJ2 : proof -> term -> proof
40 val proof_NOTI : proof -> proof
41 val proof_NOTE : proof -> proof
42 val proof_CONTR : proof -> term -> proof
43 val proof_DISJCASES : proof -> proof -> proof -> proof
44 val proof_CHOOSE : term -> proof -> proof -> proof
45 val proof_EXISTS : term -> term -> proof -> proof
47 val new_axiom_name : string -> string
48 val proof_new_axiom : string -> term -> proof
50 val save_proof : string -> proof -> (term option) -> unit
51 val proof_database : unit -> ((string * proof * (term option)) list)
53 val export_proofs : string option -> (string * proof * (term option)) list -> unit
54 val export_saved_proofs : string option -> unit
58 module Proofobjects : Proofobject_primitives = struct
60 type proof = unit -> unit
64 let proof_REFL _ = dummy ()
65 let proof_TRANS _ = dummy ()
66 let proof_MK_COMB _ = dummy ()
67 let proof_ASSUME _ = dummy ()
68 let proof_EQ_MP _ _ = dummy ()
69 let proof_IMPAS _ _ = dummy ()
70 let proof_DISCH _ _ = dummy ()
71 let proof_DEDUCT_ANTISYM_RULE _ _ = dummy ()
72 let proof_BETA _ = dummy ()
73 let proof_ABS _ _ = dummy ()
74 let proof_INST_TYPE _ _ = dummy ()
75 let proof_INST _ _ = dummy ()
76 let proof_new_definition _ _ _ = dummy ()
77 let proof_CONJ _ _ = dummy ()
78 let proof_CONJUNCT1 _ = dummy ()
79 let proof_CONJUNCT2 _ = dummy ()
80 let proof_new_basic_type_definition _ _ _ _ = dummy ()
81 let proof_SPEC _ _ = dummy ()
82 let proof_SYM _ = dummy ()
83 let proof_GEN _ _ = dummy ()
84 let proof_DISJ1 _ _ = dummy ()
85 let proof_DISJ2 _ _ = dummy ()
86 let proof_NOTI _ = dummy ()
87 let proof_NOTE _ = dummy ()
88 let proof_CONTR _ _ = dummy ()
89 let proof_DISJCASES _ _ _ = dummy ()
90 let proof_CHOOSE _ _ _ = dummy ()
91 let proof_EXISTS _ _ _ = dummy ()
92 let new_axiom_name _ = ""
93 let proof_new_axiom _ _ = dummy ()
94 let save_proof _ _ _ = ()
95 let proof_database _ = []
96 let export_proofs _ _ = ()
97 let export_saved_proofs _ = ()
101 include Proofobjects;;