thm.ml

   1 (* ========================================================================= *)
   2 (* Abstract type of theorems and primitive inference rules.                  *)
   3 (*                                                                           *)
   4 (*       John Harrison, University of Cambridge Computer Laboratory          *)
   5 (*                                                                           *)
   6 (*            (c) Copyright, University of Cambridge 1998                    *)
   7 (*              (c) Copyright, John Harrison 1998-2007                       *)
   8 (* ========================================================================= *)
   9
  10 (* ------------------------------------------------------------------------- *)
  11 (* A few bits of general derived syntax.                                     *)
  12 (* ------------------------------------------------------------------------- *)
  13
  14 let rator tm =
  15   match tm with
  16     Comb(l,r) -> l
  17   | _ -> failwith "rator: Not a combination";;
  18
  19 let rand tm =
  20   match tm with
  21     Comb(l,r) -> r
  22   | _ -> failwith "rand: Not a combination";;
  23
  24 (* ------------------------------------------------------------------------- *)
  25 (* Syntax operations for equations.                                          *)
  26 (* ------------------------------------------------------------------------- *)
  27
  28 let mk_eq =
  29   let eq = mk_const("=",[]) in
  30   fun (l,r) ->
  31     try let ty = type_of l in
  32         let eq_tm = inst [ty,aty] eq in
  33         mk_comb(mk_comb(eq_tm,l),r)
  34     with Failure _ -> failwith "mk_eq";;
  35
  36 let dest_eq tm =
  37   match tm with
  38     Comb(Comb(Const("=",_),l),r) -> l,r
  39   | _ -> failwith "dest_eq";;
  40
  41 let is_eq tm =
  42   match tm with
  43     Comb(Comb(Const("=",_),_),_) -> true
  44   | _ -> false;;
  45
  46 (* ------------------------------------------------------------------------- *)
  47 (* Useful to have term union modulo alpha-conversion for assumption lists.   *)
  48 (* ------------------------------------------------------------------------- *)
  49
  50 let term_remove t l = filter (fun t' -> not(aconv t t')) l;;
  51
  52 let rec term_union l1 l2 =
  53   match l1 with
  54     [] -> l2
  55   | (h::t) -> let subun = term_union t l2 in
  56               if exists (aconv h) subun then subun else h::subun;;
  57
  58 (* ------------------------------------------------------------------------- *)
  59 (* The abstract type of theorems.                                            *)
  60 (* ------------------------------------------------------------------------- *)
  61
  62 module type Hol_thm_primitives =
  63   sig type thm
  64   val dest_thm : thm -> term list * term
  65   val hyp : thm -> term list
  66   val concl : thm -> term
  67   val REFL : term -> thm
  68   val TRANS : thm -> thm -> thm
  69   val MK_COMB : thm * thm -> thm
  70   val ABS : term -> thm -> thm
  71   val BETA : term -> thm
  72   val ASSUME : term -> thm
  73   val EQ_MP : thm -> thm -> thm
  74   val DEDUCT_ANTISYM_RULE : thm -> thm -> thm
  75   val INST_TYPE : (hol_type * hol_type) list -> thm -> thm
  76   val INST : (term * term) list -> thm -> thm
  77   val axioms : unit -> thm list
  78   val new_axiom : term -> thm
  79   val new_basic_definition : term -> thm
  80   val new_basic_type_definition : string -> string * string -> thm -> thm * thm
  81 end;;
  82
  83 (* ------------------------------------------------------------------------- *)
  84 (* This is the implementation of those primitives.                           *)
  85 (* ------------------------------------------------------------------------- *)
  86
  87 module Hol : Hol_thm_primitives = struct
  88
  89   type thm = Sequent of (term list * term)
  90
  91 (* ------------------------------------------------------------------------- *)
  92 (* Basic theorem destructors.                                                *)
  93 (* ------------------------------------------------------------------------- *)
  94
  95   let dest_thm (Sequent(asl,c)) = (asl,c)
  96
  97   let hyp (Sequent(asl,c)) = asl
  98
  99   let concl (Sequent(asl,c)) = c
 100
 101 (* ------------------------------------------------------------------------- *)
 102 (* Basic equality properties; TRANS is derivable but included for efficiency *)
 103 (* ------------------------------------------------------------------------- *)
 104
 105   let REFL tm =
 106     Sequent([],mk_eq(tm,tm))
 107
 108   let TRANS (Sequent(asl1,c1)) (Sequent(asl2,c2)) =
 109     match (c1,c2) with
 110       Comb(Comb(Const("=",_),l),m1),Comb(Comb(Const("=",_),m2),r)
 111         when aconv m1 m2 -> Sequent(term_union asl1 asl2,mk_eq(l,r))
 112     | _ -> failwith "TRANS"
 113
 114 (* ------------------------------------------------------------------------- *)
 115 (* Congruence properties of equality.                                        *)
 116 (* ------------------------------------------------------------------------- *)
 117
 118   let MK_COMB(Sequent(asl1,c1),Sequent(asl2,c2)) =
 119      match (c1,c2) with
 120        Comb(Comb(Const("=",_),l1),r1),Comb(Comb(Const("=",_),l2),r2)
 121         -> Sequent(term_union asl1 asl2,mk_eq(mk_comb(l1,l2),mk_comb(r1,r2)))
 122      | _ -> failwith "MK_COMB"
 123
 124   let ABS v (Sequent(asl,c)) =
 125     match c with
 126       Comb(Comb(Const("=",_),l),r) ->
 127         if exists (vfree_in v) asl
 128         then failwith "ABS: variable is free in assumptions"
 129         else Sequent(asl,mk_eq(mk_abs(v,l),mk_abs(v,r)))
 130     | _ -> failwith "ABS: not an equation"
 131
 132 (* ------------------------------------------------------------------------- *)
 133 (* Trivial case of lambda calculus beta-conversion.                          *)
 134 (* ------------------------------------------------------------------------- *)
 135
 136   let BETA tm =
 137     match tm with
 138       Comb(Abs(v,bod),arg) when arg = v -> Sequent([],mk_eq(tm,bod))
 139     | _ -> failwith "BETA: not a trivial beta-redex"
 140
 141 (* ------------------------------------------------------------------------- *)
 142 (* Rules connected with deduction.                                           *)
 143 (* ------------------------------------------------------------------------- *)
 144
 145   let ASSUME tm =
 146     if type_of tm = bool_ty then Sequent([tm],tm)
 147     else failwith "ASSUME: not a proposition"
 148
 149   let EQ_MP (Sequent(asl1,eq)) (Sequent(asl2,c)) =
 150     match eq with
 151       Comb(Comb(Const("=",_),l),r) when aconv l c
 152         -> Sequent(term_union asl1 asl2,r)
 153     | _ -> failwith "EQ_MP"
 154
 155   let DEDUCT_ANTISYM_RULE (Sequent(asl1,c1)) (Sequent(asl2,c2)) =
 156     let asl1' = term_remove c2 asl1 and asl2' = term_remove c1 asl2 in
 157     Sequent(term_union asl1' asl2',mk_eq(c1,c2))
 158
 159 (* ------------------------------------------------------------------------- *)
 160 (* Type and term instantiation.                                              *)
 161 (* ------------------------------------------------------------------------- *)
 162
 163   let INST_TYPE theta (Sequent(asl,c)) =
 164     let inst_fn = inst theta in
 165     Sequent(map inst_fn asl,inst_fn c)
 166
 167   let INST theta (Sequent(asl,c)) =
 168     let inst_fun = vsubst theta in
 169     Sequent(map inst_fun asl,inst_fun c)
 170
 171 (* ------------------------------------------------------------------------- *)
 172 (* Handling of axioms.                                                       *)
 173 (* ------------------------------------------------------------------------- *)
 174
 175   let the_axioms = ref ([]:thm list)
 176
 177   let axioms() = !the_axioms
 178
 179   let new_axiom tm =
 180     if fst(dest_type(type_of tm)) = "bool" then
 181       let th = Sequent([],tm) in
 182        (the_axioms := th::(!the_axioms); th)
 183     else failwith "new_axiom: Not a proposition"
 184
 185 (* ------------------------------------------------------------------------- *)
 186 (* Handling of (term) definitions.                                           *)
 187 (* ------------------------------------------------------------------------- *)
 188
 189   let new_basic_definition tm =
 190     let l,r = dest_eq tm in
 191     let cname,ty = dest_var l in
 192     if not(freesin [] r) then failwith "new_definition: term not closed" else
 193     if not (subset (type_vars_in_term r) (tyvars ty))
 194     then failwith "new_definition: Type variables not reflected in constant"
 195     else
 196       let c = new_constant(cname,ty); mk_const(cname,[]) in
 197       Sequent([],mk_eq(c,r))
 198
 199 (* ------------------------------------------------------------------------- *)
 200 (* Handling of type definitions.                                             *)
 201 (*                                                                           *)
 202 (* This function now involves no logical constants beyond equality.          *)
 203 (*                                                                           *)
 204 (*             |- P t                                                        *)
 205 (*    ---------------------------                                            *)
 206 (*        |- abs(rep a) = a                                                  *)
 207 (*     |- P r = (rep(abs r) = r)                                             *)
 208 (*                                                                           *)
 209 (* Where "abs" and "rep" are new constants with the nominated names.         *)
 210 (* ------------------------------------------------------------------------- *)
 211
 212   let new_basic_type_definition tyname (absname,repname) (Sequent(asl,c)) =
 213     if exists (can get_const_type) [absname; repname] then
 214       failwith "new_basic_type_definition: Constant(s) already in use" else
 215     if not (asl = []) then
 216       failwith "new_basic_type_definition: Assumptions in theorem" else
 217     let P,x = try dest_comb c
 218               with Failure _ ->
 219                 failwith "new_basic_type_definition: Not a combination" in
 220     if not(freesin [] P) then
 221       failwith "new_basic_type_definition: Predicate is not closed" else
 222     let tyvars = sort (<=) (type_vars_in_term P) in
 223     let _ = try new_type(tyname,length tyvars)
 224             with Failure _ ->
 225                 failwith "new_basic_type_definition: Type already defined" in
 226     let aty = mk_type(tyname,tyvars)
 227     and rty = type_of x in
 228     let abs = new_constant(absname,mk_fun_ty rty aty); mk_const(absname,[])
 229     and rep = new_constant(repname,mk_fun_ty aty rty); mk_const(repname,[]) in
 230     let a = mk_var("a",aty) and r = mk_var("r",rty) in
 231     Sequent([],mk_eq(mk_comb(abs,mk_comb(rep,a)),a)),
 232     Sequent([],mk_eq(mk_comb(P,r),mk_eq(mk_comb(rep,mk_comb(abs,r)),r)))
 233
 234 end;;
 235
 236 include Hol;;
 237
 238 (* ------------------------------------------------------------------------- *)
 239 (* Comparison function on theorems. Currently the same as equality, but      *)
 240 (* it's useful to separate because in the proof-recording version it isn't.  *)
 241 (* ------------------------------------------------------------------------- *)
 242
 243 let equals_thm th th' = dest_thm th = dest_thm th';;