Proofrecording/diffs/proofobjects_dummy.ml

   1 (* ========================================================================= *)
   2 (*                 Proof-objects for HOL-light                               *)
   3 (*                                                                           *)
   4 (*       Steven Obua, TU München, December 2004                              *)
   5 (*                                                                           *)
   6 (*       based on Sebastian Skalberg's HOL4 proof-objects                    *)
   7 (*                                                                           *)
   8 (*       dummy proof objects, is used when proof objects are switched off,   *)
   9 (*       the real thing can be found in proofobjects_trt.ml                  *)
  10 (* ========================================================================= *)
  11
  12 module type Proofobject_primitives =
  13   sig
  14
  15     type proof
  16
  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
  46
  47     val new_axiom_name : string -> string
  48     val proof_new_axiom : string -> term -> proof
  49
  50     val save_proof : string -> proof -> (term option) -> unit
  51     val proof_database : unit -> ((string * proof * (term option)) list)
  52
  53     val export_proofs : string option -> (string * proof * (term option)) list -> unit
  54     val export_saved_proofs : string option -> unit
  55
  56 end;;
  57
  58 module Proofobjects : Proofobject_primitives = struct
  59
  60   type proof = unit -> unit
  61
  62   let dummy () x = x;;
  63
  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 _ = ()
  98
  99 end;;
 100
 101 include Proofobjects;;