(* ========================================================================= *) (* Proof-objects for HOL-light *) (* *) (* Steven Obua, TU München, 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;;