Proofrecording/diffs/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 dest_eq tm =
  29   match tm with
  30     Comb(Comb(Const("=",_),l),r) -> l,r
  31   | _ -> failwith "dest_eq";;
  32
  33 let is_eq tm =
  34   match tm with
  35     Comb(Comb(Const("=",_),_),_) -> true
  36   | _ -> false;;
  37
  38 let mk_eq =
  39   let eq = mk_const("=",[]) in
  40   fun (l,r) ->
  41     try let ty = type_of l in
  42         let eq_tm = inst [ty,aty] eq in
  43         mk_comb(mk_comb(eq_tm,l),r)
  44     with Failure _ -> failwith "mk_eq";;
  45
  46 (* ------------------------------------------------------------------------- *)
  47 (* Useful to have term union modulo alpha-conversion for assumption lists.   *)
  48 (* ------------------------------------------------------------------------- *)
  49
  50   let rec ordav env x1 x2 =
  51     match env with
  52       [] -> Pervasives.compare x1 x2
  53     | (t1,t2 as tp)::oenv -> if Pervasives.compare x1 t1 = 0
  54                              then if Pervasives.compare x2 t2 = 0
  55                                   then 0 else -1
  56                              else if Pervasives.compare x2 t2 = 0 then 1
  57                              else ordav oenv x1 x2
  58
  59   let rec orda env tm1 tm2 =
  60     if tm1 == tm2 & env = [] then 0 else
  61     match (tm1,tm2) with
  62       Var(x1,ty1),Var(x2,ty2) -> ordav env tm1 tm2
  63     | Const(x1,ty1),Const(x2,ty2) -> Pervasives.compare tm1 tm2
  64     | Comb(s1,t1),Comb(s2,t2) ->
  65           let c = orda env s1 s2 in if c <> 0 then c else orda env t1 t2
  66     | Abs(Var(_,ty1) as x1,t1),Abs(Var(_,ty2) as x2,t2) ->
  67           let c = Pervasives.compare ty1 ty2 in
  68           if c <> 0 then c else orda ((x1,x2)::env) t1 t2
  69     | Const(_,_),_ -> -1
  70     | _,Const(_,_) -> 1
  71     | Var(_,_),_ -> -1
  72     | _,Var(_,_) -> 1
  73     | Comb(_,_),_ -> -1
  74     | _,Comb(_,_) -> 1
  75
  76   let alphaorder = orda []
  77
  78   let rec term_union l1 l2 =
  79     match (l1,l2) with
  80       ([],l2) -> l2
  81     | (l1,[]) -> l1
  82     | (h1::t1,h2::t2) -> let c = alphaorder h1 h2 in
  83                          if c = 0 then h1::(term_union t1 t2)
  84                          else if c < 0 then h1::(term_union t1 l2)
  85                          else h2::(term_union l1 t2)
  86
  87   let rec term_remove t l =
  88     match l with
  89       s::ss -> let c = alphaorder t s in
  90                if c > 0 then
  91                  let ss' = term_remove t ss in
  92                  if ss' == ss then l else s::ss'
  93                else if c = 0 then ss else l
  94     | [] -> l
  95
  96   let rec term_image f l =
  97     match l with
  98       h::t -> let h' = f h and t' = term_image f t in
  99               if h' == h & t' == t then l else term_union [h'] t'
 100     | [] -> l
 101
 102 (* ------------------------------------------------------------------------- *)
 103 (* The abstract type of theorems.                                            *)
 104 (* ------------------------------------------------------------------------- *)
 105
 106 module type Hol_thm_primitives =
 107   sig type thm
 108   val dest_thm : thm -> term list * term
 109   val hyp : thm -> term list
 110   val concl : thm -> term
 111   val REFL : term -> thm
 112   val TRANS : thm -> thm -> thm
 113   val MK_COMB : thm * thm -> thm
 114   val ABS : term -> thm -> thm
 115   val BETA : term -> thm
 116   val ASSUME : term -> thm
 117   val EQ_MP : thm -> thm -> thm
 118   val DEDUCT_ANTISYM_RULE : thm -> thm -> thm
 119   val INST_TYPE : (hol_type * hol_type) list -> thm -> thm
 120   val INST : (term * term) list -> thm -> thm
 121   val axioms : unit -> thm list
 122   val new_axiom : term -> thm
 123   val new_basic_definition : term -> thm
 124   val new_basic_type_definition : string -> string * string -> thm -> thm * thm
 125
 126   val equals_thm : thm -> thm -> bool
 127   val le_thm : thm -> thm -> bool
 128   val less_thm : thm -> thm -> bool
 129
 130   val proof_of : thm -> proof
 131   val substitute_proof : thm -> proof -> thm
 132   val save_thm : string -> thm -> thm
 133 end;;
 134
 135 (* ------------------------------------------------------------------------- *)
 136 (* This is the implementation of those primitives.                           *)
 137 (* ------------------------------------------------------------------------- *)
 138
 139 module Hol : Hol_thm_primitives = struct
 140
 141   type thm = Sequent of (term list * term * proof)
 142
 143 (* ------------------------------------------------------------------------- *)
 144 (* Basic theorem destructors.                                                *)
 145 (* ------------------------------------------------------------------------- *)
 146
 147   let dest_thm (Sequent(asl,c,_)) = (asl,c)
 148
 149   let hyp (Sequent(asl,c,_)) = asl
 150
 151   let concl (Sequent(asl,c,_)) = c
 152
 153 (* ------------------------------------------------------------------------- *)
 154 (* Basic equality properties; TRANS is derivable but included for efficiency *)
 155 (* ------------------------------------------------------------------------- *)
 156
 157   let REFL tm =
 158     Sequent([],mk_eq (tm, tm), proof_REFL tm)
 159
 160   let TRANS (Sequent(asl1,c1,p1)) (Sequent(asl2,c2,p2)) =
 161     match (c1,c2) with
 162       Comb((Comb(Const("=",_),l) as eql),m1),Comb(Comb(Const("=",_),m2),r)
 163         when alphaorder m1 m2 = 0 -> Sequent(term_union asl1 asl2,mk_comb (eql, r),proof_TRANS (p1,p2))
 164     | _ -> failwith "TRANS"
 165
 166 (* ------------------------------------------------------------------------- *)
 167 (* Congruence properties of equality.                                        *)
 168 (* ------------------------------------------------------------------------- *)
 169
 170     let MK_COMB(Sequent(asl1,c1,p1),Sequent(asl2,c2,p2)) =
 171      match (c1,c2) with
 172        Comb(Comb(Const("=",_),l1),r1),Comb(Comb(Const("=",_),l2),r2) ->
 173         (match type_of l1 with
 174            Tyapp("fun",[ty;_]) when Pervasives.compare ty (type_of l2) = 0
 175              -> Sequent(term_union asl1 asl2,
 176                         mk_eq (mk_comb (l1, l2), mk_comb(r1, r2)),
 177                         proof_MK_COMB (p1,p2))
 178          | _ -> failwith "MK_COMB: types do not agree")
 179      | _ -> failwith "MK_COMB: not both equations"
 180
 181   let ABS v (Sequent(asl,c,p)) =
 182     match (v,c) with
 183       Var(_,_),Comb(Comb(Const("=",_),l),r) when not(exists (vfree_in v) asl)
 184          -> Sequent(asl,mk_eq (mk_abs (v, l), mk_abs (v, r)),proof_ABS v p)
 185     | _ -> failwith "ABS";;
 186
 187 (* ------------------------------------------------------------------------- *)
 188 (* Trivial case of lambda calculus beta-conversion.                          *)
 189 (* ------------------------------------------------------------------------- *)
 190
 191   let BETA tm =
 192     match tm with
 193       Comb(Abs(v,bod),arg) when Pervasives.compare arg v = 0
 194         -> Sequent([],mk_eq (tm, bod), proof_BETA tm)
 195     | _ -> failwith "BETA: not a trivial beta-redex"
 196
 197 (* ------------------------------------------------------------------------- *)
 198 (* Rules connected with deduction.                                           *)
 199 (* ------------------------------------------------------------------------- *)
 200
 201   let ASSUME tm =
 202     if Pervasives.compare (type_of tm) bool_ty = 0 then Sequent([tm],tm, proof_ASSUME tm)
 203     else failwith "ASSUME: not a proposition"
 204
 205   let EQ_MP (Sequent(asl1,eq,p1)) (Sequent(asl2,c,p2)) =
 206     match eq with
 207       Comb(Comb(Const("=",_),l),r) when alphaorder l c = 0
 208         -> Sequent(term_union asl1 asl2,r, proof_EQ_MP p1 p2)
 209     | _ -> failwith "EQ_MP"
 210
 211   let DEDUCT_ANTISYM_RULE (Sequent(asl1,c1,p1)) (Sequent(asl2,c2,p2)) =
 212     let asl1' = term_remove c2 asl1 and asl2' = term_remove c1 asl2 in
 213     Sequent(term_union asl1' asl2',mk_eq (c1, c2),
 214             proof_DEDUCT_ANTISYM_RULE (p1,c1) (p2,c2))
 215
 216 (* ------------------------------------------------------------------------- *)
 217 (* Type and term instantiation.                                              *)
 218 (* ------------------------------------------------------------------------- *)
 219
 220   let INST_TYPE theta (Sequent(asl,c,p)) =
 221     let inst_fn = inst theta in
 222     Sequent(term_image inst_fn asl,inst_fn c, proof_INST_TYPE theta p)
 223
 224   let INST theta (Sequent(asl,c,p)) =
 225     let inst_fun = vsubst theta in
 226     Sequent(term_image inst_fun asl,inst_fun c, proof_INST theta p)
 227
 228 (* ------------------------------------------------------------------------- *)
 229 (* Handling of axioms.                                                       *)
 230 (* ------------------------------------------------------------------------- *)
 231
 232   let the_axioms = ref ([]:thm list)
 233
 234   let axioms() = !the_axioms
 235
 236   let new_axiom tm =
 237     if Pervasives.compare (type_of tm) bool_ty = 0 then
 238       let axname = new_axiom_name "" in
 239       let p = proof_new_axiom (axname) tm in
 240       let th = Sequent([],tm,p) in
 241       (the_axioms := th::(!the_axioms);
 242        save_proof axname p (Some tm);
 243        th)
 244     else failwith "new_axiom: Not a proposition"
 245
 246 (* ------------------------------------------------------------------------- *)
 247 (* Handling of (term) definitions.                                           *)
 248 (* ------------------------------------------------------------------------- *)
 249
 250   let the_definitions = ref ([]:thm list)
 251
 252   let definitions() = !the_definitions
 253
 254   let new_basic_definition tm =
 255     match tm with
 256       Comb(Comb(Const("=",_),(Var(cname,ty) as l)),r) ->
 257         if not(freesin [] r) then failwith "new_definition: term not closed"
 258         else if not (subset (type_vars_in_term r) (tyvars ty))
 259         then failwith "new_definition: Type variables not reflected in constant"
 260         else let c = new_constant(cname,ty); mk_const (cname, []) in
 261         let p = proof_new_definition cname ty r in
 262         let concl = mk_eq (c, r) in
 263         save_proof ("DEF_"^cname) p (Some concl);
 264              let dth = Sequent([],concl,p) in
 265              the_definitions := dth::(!the_definitions); dth
 266     | _ -> failwith "new_basic_definition"
 267
 268 (* ------------------------------------------------------------------------- *)
 269 (* Handling of type definitions.                                             *)
 270 (*                                                                           *)
 271 (* This function now involves no logical constants beyond equality.          *)
 272 (*                                                                           *)
 273 (*             |- P t                                                        *)
 274 (*    ---------------------------                                            *)
 275 (*        |- abs(rep a) = a                                                  *)
 276 (*     |- P r = (rep(abs r) = r)                                             *)
 277 (*                                                                           *)
 278 (* Where "abs" and "rep" are new constants with the nominated names.         *)
 279 (* ------------------------------------------------------------------------- *)
 280
 281   let new_basic_type_definition tyname (absname,repname) (Sequent(asl,c,p)) =
 282     if exists (can get_const_type) [absname; repname] then
 283       failwith "new_basic_type_definition: Constant(s) already in use" else
 284     if not (asl = []) then
 285       failwith "new_basic_type_definition: Assumptions in theorem" else
 286     let P,x = try dest_comb c
 287               with Failure _ ->
 288                 failwith "new_basic_type_definition: Not a combination" in
 289     if not(freesin [] P) then
 290       failwith "new_basic_type_definition: Predicate is not closed" else
 291     let tyvars = sort (<=) (type_vars_in_term P) in
 292     let _ = try new_type(tyname,length tyvars)
 293             with Failure _ ->
 294                 failwith "new_basic_type_definition: Type already defined" in
 295     let aty = mk_type(tyname,tyvars)
 296     and rty = type_of x in
 297     let absty = mk_type("fun",[rty;aty]) and repty = mk_type("fun",[aty;rty]) in
 298     let abs = (new_constant(absname,absty); mk_const(absname,[]))
 299     and rep = (new_constant(repname,repty); mk_const(repname,[])) in
 300     let a = mk_var("a",aty) and r = mk_var("r",rty) in
 301     let ax1 = mk_eq (mk_comb(abs,mk_comb(rep,a)), a) in
 302     let ax2 = mk_eq (mk_comb(P,r),
 303                           mk_eq (mk_comb(rep,mk_comb(abs,r)), r)) in
 304     let tp = proof_new_basic_type_definition tyname (absname, repname) (P,x) p in
 305     let tname = "TYDEF_"^tyname in
 306     save_proof tname tp None;
 307     Sequent([],ax1,proof_CONJUNCT1 tp),
 308     Sequent([],ax2,proof_CONJUNCT2 tp)
 309
 310 (* ------------------------------------------------------------------------- *)
 311 (* Dealing with proof objects.                                               *)
 312 (* ------------------------------------------------------------------------- *)
 313
 314   let substitute_proof =
 315     if use_extended_proofobjects then
 316       fun (Sequent (asl, c, p)) pnew -> Sequent (asl, c, pnew)
 317     else
 318       fun th p -> th;;
 319
 320   let equals_thm (Sequent (p1,c1,_)) (Sequent (p2,c2,_)) =
 321     (p1 = p2) & (c1 = c2)
 322
 323   let le_thm (Sequent (p1,c1,_)) (Sequent (p2,c2,_)) = (p1, c1) <= (p2, c2)
 324
 325   let less_thm (Sequent (p1, c1,_)) (Sequent (p2, c2,_)) = (p1, c1) < (p2, c2)
 326
 327   let proof_of (Sequent(_,_,p)) = p
 328
 329   let save_thm name th =
 330     (save_proof name (proof_of th) (Some (concl th)); th)
 331
 332 end;;
 333
 334 include Hol;;
 335
 336 (* ------------------------------------------------------------------------- *)
 337 (* Tests for alpha-convertibility (equality ignoring names in abstractions). *)
 338 (* ------------------------------------------------------------------------- *)
 339
 340 let aconv s t = alphaorder s t = 0;;
 341
 342 (* ------------------------------------------------------------------------- *)
 343 (* Comparison function on theorems. Currently the same as equality, but      *)
 344 (* it's useful to separate because in the proof-recording version it isn't.  *)
 345 (* ------------------------------------------------------------------------- *)
 346
 347 let equals_thm th th' = dest_thm th = dest_thm th';;