1(* ===================================================================== *) 2(* FILE : Thm.sml *) 3(* DESCRIPTION : The abstract data type of theorems. *) 4(* *) 5(* AUTHORS : (c) Mike Gordon, University of Cambridge *) 6(* Konrad Slind, University of Calgary *) 7(* University of Cambridge *) 8(* Bruno Barras, University of Cambridge and INRIA *) 9(* DATE : September 10, 1991, Konrad Slind *) 10(* Modified : September 23, 1997, Ken Larsen *) 11(* : 1999, Bruno Barras *) 12(* : July 2000, Konrad Slind *) 13(* ===================================================================== *) 14 15structure Thm :> Thm = 16struct 17 18open Feedback Lib Term Tag Dep 19 20type 'a set = 'a HOLset.set; 21type depdisk = (string * int) * ((string * int list) list); 22datatype thm = THM of Tag.tag * term HOLset.set * term 23 24val --> = Type.-->; 25infixr 3 -->; 26infix 5 |-> ; 27 28val kernelid = Term.kernelid 29 30(*--------------------------------------------------------------------------- 31 Exception handling 32 ---------------------------------------------------------------------------*) 33 34val thm_err = mk_HOL_ERR "Thm" 35fun ERR f m = raise thm_err f m 36fun Assert b s1 s2 = if b then () else ERR s1 s2 37 38 39(*---------------------------------------------------------------------------* 40 * Miscellaneous syntax routines. * 41 *---------------------------------------------------------------------------*) 42 43val bool = Type.bool 44val alpha = Type.alpha 45fun dom ty = fst (Type.dom_rng ty) 46fun rng ty = snd (Type.dom_rng ty); 47val EQ = Term.fast_term_eq 48val empty_tag = Tag.empty_tag 49 50 51(*--------------------------------------------------------------------------- 52 The following are here because I didn't want to Thm to be dependent 53 on some derived syntax (now in boolSyntax). 54 ---------------------------------------------------------------------------*) 55structure Susp = Portable.HOLSusp 56 57val F = Susp.delay (fn () => mk_thy_const{Name="F", Thy="bool", Ty=bool}); 58 59val mk_neg = Susp.delay (fn () => 60 let val notc = mk_thy_const{Name="~",Thy="bool",Ty=bool --> bool} 61 in fn M => mk_comb(notc,M) 62 end); 63 64val mk_forall = Susp.delay (fn () => 65 let val forallc = prim_mk_const{Name="!", Thy="bool"} 66 in fn v => fn tm => 67 mk_comb(inst[alpha |-> type_of v] forallc, mk_abs(v,tm)) 68 end); 69 70val mk_conj = Susp.delay (fn () => 71 let val conjc = prim_mk_const{Name="/\\", Thy="bool"} 72 in fn (M,N) => list_mk_comb(conjc,[M,N]) 73 end); 74 75val mk_disj = Susp.delay (fn () => 76 let val disjc = prim_mk_const{Name="\\/", Thy="bool"} 77 in fn (M,N) => list_mk_comb(disjc,[M,N]) 78 end); 79 80 81local val DEST_IMP_ERR = thm_err "dest_imp" "" 82in 83fun dest_imp M = 84 let val (Rator,conseq) = with_exn dest_comb M DEST_IMP_ERR 85 in if is_comb Rator 86 then let val (Rator,ant) = dest_comb Rator 87 in if Rator=Term.imp then (ant,conseq) else raise DEST_IMP_ERR 88 end 89 else case with_exn dest_thy_const Rator DEST_IMP_ERR 90 of {Name="~", Thy="bool",...} => (conseq,Susp.force F) 91 | otherwise => raise DEST_IMP_ERR 92 end 93end; 94 95local val err = thm_err "dest_exists" "" 96in 97fun dest_exists tm = 98 let val (Rator,Rand) = with_exn dest_comb tm err 99 in case with_exn dest_thy_const Rator err 100 of {Name="?", Thy="bool",...} => with_exn dest_abs Rand err 101 | otherwise => raise err 102 end 103end; 104 105 106(*---------------------------------------------------------------------------* 107 * The type of theorems and some basic operations on it. * 108 *---------------------------------------------------------------------------*) 109 110(* datatype thm = datatype KernelTypes.thm *) 111 112fun single_hyp tm = HOLset.singleton Term.compare tm 113val empty_hyp = Term.empty_tmset 114fun list_hyp tml = HOLset.addList(empty_hyp,tml) 115 116fun tag (THM(tg,_,_)) = tg 117fun concl(THM(_,_,c)) = c 118fun hypset (THM(_,asl,_)) = asl 119fun hyplist (THM(_,asl,_)) = HOLset.listItems asl 120val hyp = hyplist (* backwards compatibility *) 121 122fun dest_thm(t as THM(_,asl,w)) = (hyplist t,w) (* Compatible with old code. *) 123fun sdest_thm(THM(_,asl,w)) = (asl,w) 124fun make_thm R seq = (Count.inc_count R; THM seq); (* internal only *) 125 126fun thm_frees (t as THM(_,asl,c)) = free_varsl (c::hyplist t); 127 128fun add_hyp h asl = HOLset.add(asl,h) 129fun union_hyp asl1 asl2 = HOLset.union(asl1, asl2) 130 131fun tag_hyp_union thm_list = 132 (itlist (Tag.merge o tag) (tl thm_list) (tag (hd thm_list)), 133 itlist (union_hyp o hypset) thm_list empty_hyp); 134 135fun var_occursl v l = isSome (HOLset.find (var_occurs v) l); 136 137fun hypset_all P s = not (isSome (HOLset.find (not o P) s)) 138fun hypset_exists P s = isSome (HOLset.find P s) 139fun hypset_map f s = HOLset.foldl(fn(i,s0) => HOLset.add(s0,f i)) empty_hyp s 140 141fun hyp_tyvars th = 142 HOLset.foldl (fn (h,tys) => 143 List.foldl (fn (tyv,tys) => HOLset.add(tys,tyv)) 144 tys 145 (Term.type_vars_in_term h)) 146 (HOLset.empty Type.compare) 147 (hypset th) 148 149fun hyp_frees th = 150 HOLset.foldl (fn (h,tms) => Term.FVL[h] tms) empty_tmset (hypset th); 151 152fun is_bool tm = (type_of tm = bool); 153 154 155(*--------------------------------------------------------------------------- 156 * THE PRIMITIVE RULES OF INFERENCE 157 *---------------------------------------------------------------------------*) 158 159 160(*---------------------------------------------------------------------------* 161 * * 162 * --------- ASSUME M [M is boolean] * 163 * M |- M * 164 *---------------------------------------------------------------------------*) 165 166fun ASSUME tm = 167 (Assert (is_bool tm) "ASSUME" "not a proposition"; 168 make_thm Count.Assume (empty_tag,single_hyp tm,tm)); 169 170 171(*---------------------------------------------------------------------------* 172 * * 173 * --------- REFL M * 174 * |- M = M * 175 *---------------------------------------------------------------------------*) 176 177val mk_eq_nocheck = Term.prim_mk_eq; 178 179fun refl_nocheck ty tm = 180 make_thm Count.Refl (empty_tag, empty_hyp, mk_eq_nocheck ty tm tm); 181 182fun REFL tm = refl_nocheck (type_of tm) tm; 183 184 185(*---------------------------------------------------------------------------* 186 * * 187 * ------------------------ BETA_CONV "(\v.M) N" * 188 * |- (\v.M) N = M [v|->N] * 189 *---------------------------------------------------------------------------*) 190 191fun BETA_CONV tm = 192 make_thm Count.Beta 193 (empty_tag, empty_hyp, mk_eq_nocheck (type_of tm) tm (beta_conv tm)) 194 handle HOL_ERR _ => ERR "BETA_CONV" "not a beta-redex" 195 196 197(*--------------------------------------------------------------------------- 198 * ltheta is a substitution mapping from the template to the concl of 199 * the given theorem. It checks that the template is an OK abstraction of 200 * the given theorem. rtheta maps the template to another theorem, in which 201 * the lhs in the first theorem have been replaced by the rhs in the second 202 * theorem. The replacements provide the lhs and rhs. 203 *---------------------------------------------------------------------------*) 204 205fun SUBST replacements template (th as THM(O,asl,c)) = 206 let val fvs = Term.FVL [template] Term.empty_varset 207 val (ltheta, rtheta, hyps, oracles) = 208 itlist (fn {redex, residue = THM(ocls,h,c)} => 209 fn (tuple as (ltheta,rtheta,hyps,Ocls)) => 210 if HOLset.member(fvs,redex) 211 then let val (lhs,rhs,_) = Term.dest_eq_ty c 212 in ((redex |-> lhs)::ltheta, 213 (redex |-> rhs)::rtheta, 214 union_hyp h hyps, 215 Tag.merge ocls Ocls) 216 end 217 else tuple) 218 replacements ([],[],asl,O) 219 in 220 if aconv (subst ltheta template) c 221 then make_thm Count.Subst (oracles,hyps,subst rtheta template) 222 else th 223 end; 224 225(*---------------------------------------------------------------------------* 226 * A |- t1 = t2 * 227 * ------------------------ ABS x [Where x is not free in A] * 228 * A |- (\x.t1) = (\x.t2) * 229 *---------------------------------------------------------------------------*) 230 231fun ABS v (THM(ocl,asl,c)) = 232 let val (lhs,rhs,ty) = Term.dest_eq_ty c handle HOL_ERR _ 233 => ERR "ABS" "not an equality" 234 val vty = snd(dest_var v) handle HOL_ERR _ 235 => ERR "ABS" "first argument is not a variable" 236 in if var_occursl v asl 237 then ERR "ABS" "The variable is free in the assumptions" 238 else make_thm Count.Abs 239 (ocl, asl, mk_eq_nocheck (vty --> ty) 240 (mk_abs(v,lhs)) 241 (mk_abs(v,rhs))) 242 end; 243 244(*---------------------------------------------------------------------------* 245 * A |- t1 = t2 * 246 * ------------------------------------ GEN_ABS f [v1,...,vn] * 247 * A |- (Q v1...vn.t1) = (Q v1...vn.t2) (where no vi is free in A) * 248 *---------------------------------------------------------------------------*) 249 250fun GEN_ABS opt vlist (th as THM(ocl,asl,c)) = 251 let open HOLset 252 val vset = addList(Term.empty_varset,vlist) 253 val hset = hyp_frees th 254 in if isEmpty (intersection(vset,hset)) 255 then let val (lhs,rhs,ty) = with_exn Term.dest_eq_ty c 256 (thm_err "GEN_ABS" "not an equality") 257 val lhs' = list_mk_binder opt (vlist,lhs) 258 val rhs' = list_mk_binder opt (vlist,rhs) 259 in make_thm Count.GenAbs 260 (ocl,asl,mk_eq_nocheck (Term.type_of lhs') lhs' rhs') 261 end 262 else ERR "GEN_ABS" "variable(s) free in the assumptions" 263 end 264 265(*--------------------------------------------------------------------------- 266 * A |- M 267 * -------------------- INST_TYPE theta 268 * theta(A) |- theta(M) 269 * 270 *---------------------------------------------------------------------------*) 271 272fun INST_TYPE [] th = th 273 | INST_TYPE theta (THM(ocl,asl,c)) = 274 make_thm Count.InstType(ocl, hypset_map (inst theta) asl, inst theta c) 275 276(*--------------------------------------------------------------------------- 277 * A |- M 278 * ---------------------- DISCH tm 279 * A - tm |- tm ==> M 280 * 281 * The term tm need not occur in A. All terms in A that are 282 * alpha-convertible to tm are removed. 283 *---------------------------------------------------------------------------*) 284 285fun DISCH w (THM(ocl,asl,c)) = 286 (Assert (is_bool w) "DISCH" "not a proposition"; 287 make_thm Count.Disch 288 (ocl, 289 HOLset.delete(asl, w) handle HOLset.NotFound => asl, 290 Term.prim_mk_imp w c)); 291 292 293(*--------------------------------------------------------------------------- 294 * A |- M ==> N , B |- M' 295 * ---------------------------------- MP 296 * A u B |- N 297 * 298 * M and M' must be alpha-convertible 299 *---------------------------------------------------------------------------*) 300 301fun MP (THM(o1,asl1,c1)) (THM(o2,asl2,c2)) = 302 let val (ant,conseq) = dest_imp c1 303 in Assert (aconv ant c2) "MP" 304 "antecedent of first thm not alpha-convertible to concl. of second"; 305 make_thm Count.Mp (Tag.merge o1 o2, union_hyp asl1 asl2, conseq) 306 end; 307 308 309(*---------------------------------------------------------------------------* 310 * Derived Rules -- these are here for efficiency purposes, and so that all * 311 * invocations of mk_thm are in Thm. The following derived rules do not use * 312 * any axioms of boolTheory: * 313 * * 314 * ALPHA, SYM, TRANS, MK_COMB, AP_TERM, AP_THM, EQ_MP, EQ_IMP_RULE, * 315 * Beta, Mk_comb, Mk_abs * 316 * * 317 *---------------------------------------------------------------------------*) 318 319(*--------------------------------------------------------------------------- 320 * Equivalence of alpha-convertible terms 321 * 322 * t1, t2 alpha-convertable 323 * ------------------------- 324 * |- t1 = t2 325 * 326 * fun ALPHA t1 t2 = TRANS (REFL t1) (REFL t2) 327 *---------------------------------------------------------------------------*) 328 329fun ALPHA t1 t2 = 330 if aconv t1 t2 then 331 make_thm Count.Alpha (empty_tag, empty_hyp, 332 mk_eq_nocheck (type_of t1) t1 t2) 333 else ERR "ALPHA" "Terms not alpha-convertible"; 334 335(*---------------------------------------------------------------------------* 336 * Symmetry of = 337 * 338 * A |- t1 = t2 339 * ---------------- 340 * A |- t2 = t1 341 * 342 * fun SYM th = 343 * let val (t1,t2) = dest_eq(concl th) 344 * val v = genvar(type_of t1) 345 * in 346 * SUBST [(th,v)] (mk_eq(v,t1)) (REFL t1) 347 * end 348 * handle _ => ERR "SYM" ""; 349 *---------------------------------------------------------------------------*) 350 351fun SYM th = 352 let val (lhs,rhs,ty) = Term.dest_eq_ty (concl th) 353 in make_thm Count.Sym 354 (tag th, hypset th, mk_eq_nocheck ty rhs lhs) 355 end 356 handle HOL_ERR _ => ERR "SYM" ""; 357 358(*--------------------------------------------------------------------------- 359 * Transitivity of = 360 * 361 * A1 |- t1 = t2 , A2 |- t2 = t3 362 * --------------------------------- 363 * A1 u A2 |- t1=t3 364 * 365 * fun TRANS th1 th2 = 366 * let val (t1,t2) = dest_eq(concl th1) 367 * and (t2',t3) = dest_eq(concl th2) 368 * val v = genvar(type_of t1) 369 * in 370 * SUBST [(th2,v)] (mk_eq(t1,v)) th1 371 * end 372 * handle _ => ERR{function = "TRANS",message = ""}; 373 * 374 *---------------------------------------------------------------------------*) 375 376fun TRANS th1 th2 = 377 let val (lhs1,rhs1,ty) = Term.dest_eq_ty (concl th1) 378 and (lhs2,rhs2,_) = Term.dest_eq_ty (concl th2) 379 val _ = Assert (aconv rhs1 lhs2) "" "" 380 val hyps = union_hyp (hypset th1) (hypset th2) 381 val ocls = Tag.merge (tag th1) (tag th2) 382 in 383 make_thm Count.Trans (ocls, hyps, mk_eq_nocheck ty lhs1 rhs2) 384 end 385 handle HOL_ERR _ => ERR "TRANS" ""; 386 387 388(*--------------------------------------------------------------------------- 389 * A1 |- f = g A2 |- x = y 390 * --------------------------- 391 * A1 u A2 |- f x = g y 392 * 393 * fun MK_COMB (funth,argth) = 394 * let val f = lhs (concl funth) 395 * and x = lhs (concl argth) 396 * in 397 * SUBS_OCCS [([2], funth), ([2], argth)] (REFL (Comb(f,x)))) 398 * ? failwith `MK_COMB`; 399 *---------------------------------------------------------------------------*) 400 401fun MK_COMB (funth,argth) = 402 let val (f,g,ty) = Term.dest_eq_ty (concl funth) 403 val (x,y,_) = Term.dest_eq_ty (concl argth) 404 in 405 make_thm Count.MkComb 406 (Tag.merge (tag funth) (tag argth), 407 union_hyp (hypset funth) (hypset argth), 408 mk_eq_nocheck (rng ty) (mk_comb(f,x)) (mk_comb(g,y))) 409 end 410 handle HOL_ERR _ => ERR "MK_COMB" ""; 411 412(*--------------------------------------------------------------------------- 413 * Application of a term to a theorem 414 * 415 * A |- t1 = t2 416 * ------------------ 417 * A |- t t1 = t t2 418 * 419 * fun AP_TERM tm th = 420 * let val (t1,_) = dest_eq(concl th) 421 * val th1 = REFL (--`^tm ^t1`--) 422 * (* th1 = |- t t1 = t t1 *) 423 * and v = genvar(type_of t1) 424 * in 425 * SUBST [(th,v)] (--`^tm ^t1 = ^tm ^v`--) th1 426 * end 427 * handle _ => ERR{function = "AP_TERM",message = ""}; 428 *---------------------------------------------------------------------------*) 429 430fun AP_TERM f th = 431 let val (lhs,rhs,_) = Term.dest_eq_ty (concl th) 432 in make_thm Count.ApTerm 433 (tag th, hypset th, 434 mk_eq_nocheck (rng (type_of f)) (mk_comb(f,lhs)) (mk_comb(f,rhs))) 435 end 436 handle HOL_ERR _ => ERR "AP_TERM" ""; 437 438 439(*--------------------------------------------------------------------------- 440 * Application of a theorem to a term 441 * 442 * A |- t1 = t2 443 * ---------------- 444 * A |- t1 t = t2 t 445 * 446 * fun AP_THM th tm = 447 * let val (t1,_) = dest_eq(concl th) 448 * val th1 = REFL (--`^t1 ^tm`--) 449 * (* th1 = |- t1 t = t1 t *) 450 * and v = genvar(type_of t1) 451 * in 452 * SUBST [(th,v)] (--`^t1 ^tm = ^v ^tm`--) th1 453 * end 454 * handle _ => ERR{function = "AP_THM",message = ""}; 455 *---------------------------------------------------------------------------*) 456 457fun AP_THM th tm = 458 let val (lhs,rhs,ty) = Term.dest_eq_ty (concl th) 459 in make_thm Count.ApThm 460 (tag th, hypset th, 461 mk_eq_nocheck (rng ty) (mk_comb(lhs,tm)) (mk_comb(rhs,tm))) 462 end 463 handle HOL_ERR _ => ERR "AP_THM" ""; 464 465(*--------------------------------------------------------------------------- 466 * Modus Ponens for = 467 * 468 * 469 * A1 |- t1 = t2 , A2 |- t1 470 * ---------------------------- 471 * A1 u A2 |- t2 472 * 473 * fun EQ_MP th1 th2 = 474 * let val (t1,t2) = dest_eq(concl th1) 475 * val v = genvar(type_of t1) 476 * in SUBST [(th1,v)] v th2 477 * end handle _ => ERR{function = "EQ_MP",message = ""}; 478 *---------------------------------------------------------------------------*) 479 480fun EQ_MP th1 th2 = 481 let val (lhs,rhs,_) = Term.dest_eq_ty (concl th1) 482 val _ = Assert (aconv lhs (concl th2)) "" "" 483 in 484 make_thm Count.EqMp (Tag.merge (tag th1) (tag th2), 485 union_hyp (hypset th1) (hypset th2), rhs) 486 end handle HOL_ERR _ => ERR "EQ_MP" ""; 487 488(*--------------------------------------------------------------------------- 489 * A |- t1 = t2 490 * ------------------------------------ 491 * A |- t1 ==> t2 A |- t2 ==> t1 492 * 493 * fun EQ_IMP_RULE th = 494 * let val (t1,t2) = dest_eq(concl th) 495 * in 496 * (DISCH t1 (EQ_MP th (ASSUME t1)), 497 * DISCH t2 (EQ_MP (SYM th)(ASSUME t2))) 498 * end 499 * handle _ => ERR{function = "EQ_IMP_RULE",message = ""}; 500 *---------------------------------------------------------------------------*) 501 502fun EQ_IMP_RULE th = 503 let val (lhs,rhs,ty) = Term.dest_eq_ty (concl th) 504 and A = hypset th 505 and O = tag th 506 in if ty = Type.bool 507 then (make_thm Count.EqImpRule(O,A, Term.prim_mk_imp lhs rhs), 508 make_thm Count.EqImpRule(O,A, Term.prim_mk_imp rhs lhs)) 509 else ERR "" "" 510 end 511 handle HOL_ERR _ => ERR "EQ_IMP_RULE" ""; 512 513(*--------------------------------------------------------------------------- 514 * Specialization 515 * 516 * A |- !(\x.u) 517 * -------------------- (where t is free for x in u) 518 * A |- u[t/x] 519 * 520 * fun SPEC t th = 521 * let val {Rator=F,Rand=body} = dest_comb(concl th) 522 * in 523 * if (not(#Name(dest_const F)="!")) 524 * then ERR{function = "SPEC",message = ""} 525 * else let val {Bvar=x,Body=u} = dest_abs body 526 * and v1 = genvar(type_of F) 527 * and v2 = genvar(type_of body) 528 * val th1 = SUBST[{var = v1, 529 * thm = INST_TYPE[{redex = (==`:'a`==), 530 * residue = type_of x}] FORALL_DEF}] 531 * (--`^v1 ^body`--) th 532 * (* th1 = |- (\P. P = (\x. T))(\x. t1 x) *) 533 * val th2 = BETA_CONV(concl th1) 534 * (* th2 = |- (\P. P = (\x. T))(\x. t1 x) = ((\x. t1 x) = (\x. T)) *) 535 * val th3 = EQ_MP th2 th1 536 * (* th3 = |- (\x. t1 x) = (\x. T) *) 537 * val th4 = SUBST [{var= v2, thm=th3}] (--`^body ^t = ^v2 ^t`--) 538 * (REFL (--`^body ^t`--)) 539 * (* th4 = |- (\x. t1 x)t = (\x. T)t *) 540 * val {lhs=ls,rhs=rs} = dest_eq(concl th4) 541 * val th5 = TRANS(TRANS(SYM(BETA_CONV ls))th4)(BETA_CONV rs) 542 * (* th5 = |- t1 t = T *) 543 * in 544 * EQT_ELIM th5 545 * end 546 * end 547 * handle _ => ERR{function = "SPEC",message = ""}; 548 * 549 * 550 * pre-dB manner: 551 * fun SPEC t th = 552 * let val {Bvar,Body} = dest_forall(concl th) 553 * in 554 * make_thm Count.(hypset th, subst[{redex = Bvar, residue = t}] Body) 555 * end 556 * handle _ => ERR{function = "SPEC",message = ""}; 557 *---------------------------------------------------------------------------*) 558 559fun SPEC t th = 560 let val (Rator,Rand) = dest_comb(concl th) 561 val {Thy,Name,...} = dest_thy_const Rator 562 in 563 Assert (Name="!" andalso Thy="bool") 564 "SPEC" "Theorem not universally quantified"; 565 make_thm Count.Spec 566 (tag th, hypset th, beta_conv(mk_comb(Rand, t))) 567 handle HOL_ERR _ => 568 raise thm_err "SPEC" 569 "Term argument's type not equal to bound variable's" 570 end; 571 572 573(*--------------------------------------------------------------------------- 574 * Generalization 575 * 576 * A |- t 577 * ------------------- (where x not free in A) 578 * A |- !(\x.t) 579 * 580 * fun GEN x th = 581 * let val th1 = ABS x (EQT_INTRO th) 582 * (* th1 = |- (\x. t1 x) = (\x. T) --ABS does not behave this way --KLS*) 583 * val abs = `\^x. ^(concl th)` 584 * and v1 = genvar `:(^(type_of x) -> bool) -> bool` 585 * and v2 = genvar `:bool` 586 * val th2 = SUBST [(INST_TYPE[(type_of x, `:'a`)]FORALL_DEF,v1)] 587 * `($! ^abs) = (^v1 ^abs)` 588 * (REFL `$! ^abs`) 589 * (* th2 = |- (!x. t1 x) = (\P. P = (\x. T))(\x. t1 x) *) 590 * val th3 = TRANS th2 (BETA_CONV(snd(dest_eq(concl th2)))) 591 * (* th3 = |- (!x. t1 x) = ((\x. t1 x) = (\x. T)) *) 592 * in 593 * SUBST [(SYM th3, v2)] v2 th1 594 * end 595 * handle _ => ERR{function = "GEN",message = ""}; 596 *---------------------------------------------------------------------------*) 597 598 599fun GEN x th = 600 let val (asl,c) = sdest_thm th 601 in if var_occursl x asl 602 then ERR "GEN" "variable occurs free in hypotheses" 603 else make_thm Count.Gen(tag th, asl, Susp.force mk_forall x c) 604 handle HOL_ERR _ => ERR "GEN" "" 605 end; 606 607fun GENL vs th = let 608 val (asl,c) = sdest_thm th 609in 610 if exists (fn v => var_occursl v asl) vs then 611 ERR "GENL" "variable occurs free in hypotheses" 612 else 613 make_thm 614 Count.Gen(tag th, asl, 615 list_mk_binder (SOME (prim_mk_const {Thy="bool", Name="!"})) 616 (vs,c)) 617 handle HOL_ERR _ => ERR "GENL" "" 618end 619 620 621 622(*--------------------------------------------------------------------------- 623 * Existential introduction 624 * 625 * A |- t[t'] 626 * -------------- EXISTS ("?x.t[x]", "t'") ( |- t[t'] ) 627 * A |- ?x.t[x] 628 * 629 * 630 * 631 * fun EXISTS (fm,tm) th = 632 * let val (x,t) = dest_exists fm 633 * val th1 = BETA_CONV `(\(^x). ^t) ^tm` 634 * (* th1 = |- (\x. t x)t' = t t' *) 635 * val th2 = EQ_MP (SYM th1) th 636 * (* th2 = |- (\x. t x)t' *) 637 * val th3 = SELECT_INTRO th2 638 * (* th3 = |- (\x. t x)(@x. t x) *) 639 * val th4 = AP_THM(INST_TYPE[(type_of x, `:'a`)]EXISTS_DEF) `\(^x).^t` 640 * (* th4 = |- (?x. t x) = (\P. P($@ P))(\x. t x) *) 641 * val th5 = TRANS th4 (BETA_CONV(snd(dest_eq(concl th4)))) 642 * (* th5 = |- (?x. t x) = (\x. t x)(@x. t x) *) 643 * in 644 * EQ_MP (SYM th5) th3 645 * end 646 * handle _ => ERR{function = "EXISTS",message = ""}; 647 * 648 *---------------------------------------------------------------------------*) 649 650local 651 val mesg1 = "First argument not of form `?x. P`" 652 val mesg2 = "(2nd argument)/(bound var) in body of 1st argument is not theorem's conclusion" 653 val err = thm_err "EXISTS" mesg1 654in 655fun EXISTS (w,t) th = 656 let val (ex,Rand) = with_exn dest_comb w err 657 val {Name,Thy,...} = with_exn dest_thy_const ex err 658 val _ = Assert ("?"=Name andalso Thy="bool") "EXISTS" mesg1 659 val _ = Assert (aconv (beta_conv(mk_comb(Rand,t))) (concl th)) 660 "EXISTS" mesg2 661 in make_thm Count.Exists (tag th, hypset th, w) 662 end 663end; 664 665(*--------------------------------------------------------------------------- 666 * Existential elimination 667 * 668 * A1 |- ?x.t[x] , A2, "t[v]" |- t' 669 * ------------------------------------ (variable v occurs nowhere) 670 * A1 u A2 |- t' 671 * 672 * fun CHOOSE (v,th1) th2 = 673 * let val (x,body) = dest_exists(concl th1) 674 * and t' = concl th2 675 * and v1 = genvar `:bool` 676 * val th3 = AP_THM(INST_TYPE[(type_of v, `:'a`)]EXISTS_DEF)`\(^x).^body` 677 * (* th3 = |- (?x. t x) = (\P. P($@ P))(\x. t x) *) 678 * val th4 = EQ_MP th3 th1 679 * (* th4 = |- (\P. P($@ P))(\x. t x) *) 680 * val th5 = EQ_MP (BETA_CONV(concl th4)) th4 681 * (* th5 = |- (\x. t x)(@x. t x) *) 682 * val th6 = BETA_CONV `(\(^x).^body)^v` 683 * (* th6 = |- (\x. t x)v = t v *) 684 * val Pa = snd(dest_eq(concl th6)) 685 * val th7 = UNDISCH(SUBST [(SYM th6,v1)] `^v1 ==> ^t'` (DISCH Pa th2)) 686 * (* th7 = |- t' *) 687 * in 688 * SELECT_ELIM th5 (v,th7) 689 * end 690 * handle _ => ERR{function = "CHOOSE",message = ""}; 691 *---------------------------------------------------------------------------*) 692 693fun disch(w,wl) = HOLset.delete(wl,w) handle HOLset.NotFound => wl 694 695fun CHOOSE (v,xth) bth = 696 let val (x_asl, x_c) = sdest_thm xth 697 val (b_asl, b_c) = sdest_thm bth 698 val (Bvar,Body) = dest_exists x_c 699 val A2_hyps = disch (subst [Bvar |-> v] Body, b_asl) 700 val newhyps = union_hyp x_asl A2_hyps 701 val occursv = var_occurs v 702 val _ = Assert (not(occursv x_c) andalso 703 not(occursv b_c) andalso 704 not(hypset_exists occursv A2_hyps)) "" "" 705 (* Need not check for occurrence of v in A1: one can imagine 706 implementing a derived rule on top of a more restrictive one that 707 instantiated the occurrence of v in A1 to something else, applied 708 the restrictive rule, and then instantiated it back again. 709 710 Credit for pointing out this optimisation to Jim Grundy and 711 Tom Melham. *) 712 in make_thm Count.Choose 713 (Tag.merge (tag xth) (tag bth), newhyps, b_c) 714 end 715 handle HOL_ERR _ => ERR "CHOOSE" ""; 716 717 718(*--------------------------------------------------------------------------- 719 * Conjunction introduction rule 720 * 721 * A1 |- t1 , A2 |- t2 722 * ----------------------- 723 * A1 u A2 |- t1 /\ t2 724 * 725 * fun CONJ th1 th2 = MP (MP (SPEC (concl th2) 726 * (SPEC (concl th1) AND_INTRO_THM)) 727 * th1) 728 * th2; 729 *---------------------------------------------------------------------------*) 730 731fun CONJ th1 th2 = 732 make_thm Count.Conj 733 (Tag.merge (tag th1) (tag th2), 734 union_hyp (hypset th1) (hypset th2), 735 Susp.force mk_conj(concl th1, concl th2)) 736 handle HOL_ERR _ => ERR "CONJ" ""; 737 738 739(*--------------------------------------------------------------------------- 740 * Left conjunct extraction 741 * 742 * A |- t1 /\ t2 743 * ------------- 744 * A |- t1 745 * 746 * fun CONJUNCT1 th = 747 * let val (t1,t2) = dest_conj(concl th) 748 * in 749 * MP (SPEC t2 (SPEC t1 AND1_THM)) th 750 * end 751 * handle _ => ERR{function = "CONJUNCT1",message = ""}; 752 * 753 *---------------------------------------------------------------------------*) 754 755fun conj1 tm = 756 let val (c,M) = dest_comb (rator tm) 757 val {Name,Thy,...} = dest_thy_const c 758 in 759 if Name="/\\" andalso Thy="bool" then M else ERR "" "" 760 end 761 762 763fun CONJUNCT1 th = 764 make_thm Count.Conjunct1 (tag th, hypset th, conj1 (concl th)) 765 handle HOL_ERR _ => ERR "CONJUNCT1" ""; 766 767 768(*--------------------------------------------------------------------------- 769 * Right conjunct extraction 770 * 771 * A |- t1 /\ t2 772 * ------------- 773 * A |- t2 774 * 775 * fun CONJUNCT2 th = 776 * let val (t1,t2) = dest_conj(concl th) 777 * in 778 * MP (SPEC t2 (SPEC t1 AND2_THM)) th 779 * end 780 * handle _ => ERR{function = "CONJUNCT2",message = ""}; 781 *---------------------------------------------------------------------------*) 782 783fun conj2 tm = 784 let val (Rator,M) = dest_comb tm 785 val {Name,Thy,...} = dest_thy_const (rator Rator) 786 in 787 if Name="/\\" andalso Thy="bool" then M else ERR "" "" 788 end 789 790fun CONJUNCT2 th = 791 make_thm Count.Conjunct2 (tag th, hypset th, conj2 (concl th)) 792 handle HOL_ERR _ => ERR "CONJUNCT2" ""; 793 794 795(*--------------------------------------------------------------------------- 796 * Left disjunction introduction 797 * 798 * A |- t1 799 * --------------- 800 * A |- t1 \/ t2 801 * 802 * fun DISJ1 th t2 = MP (SPEC t2 (SPEC (concl th) OR_INTRO_THM1)) th 803 * handle _ => ERR{function = "DISJ1",message = ""}; 804 *---------------------------------------------------------------------------*) 805 806fun DISJ1 th w = make_thm Count.Disj1 807 (tag th, hypset th, Susp.force mk_disj (concl th, w)) 808 handle HOL_ERR _ => ERR "DISJ1" ""; 809 810 811(*--------------------------------------------------------------------------- 812 * Right disjunction introduction 813 * 814 * A |- t2 815 * --------------- 816 * A |- t1 \/ t2 817 * 818 * fun DISJ2 t1 th = MP (SPEC (concl th) (SPEC t1 OR_INTRO_THM2)) th 819 * handle _ => ERR{function = "DISJ2",message = ""}; 820 *---------------------------------------------------------------------------*) 821 822fun DISJ2 w th = make_thm Count.Disj2 823 (tag th, hypset th, Susp.force mk_disj(w,concl th)) 824 handle HOL_ERR _ => ERR "DISJ2" ""; 825 826 827(*--------------------------------------------------------------------------- 828 * Disjunction elimination 829 * 830 * A |- t1 \/ t2 , A1,t1 |- t , A2,t2 |- t 831 * ----------------------------------------------- 832 * A u A1 u A2 |- t 833 * 834 * fun DISJ_CASES th1 th2 th3 = 835 * let val (t1,t2) = dest_disj(concl th1) 836 * and t = concl th2 837 * val th4 = SPEC t2 (SPEC t1 (SPEC t OR_ELIM_THM)) 838 * in 839 * MP (MP (MP th4 th1) (DISCH t1 th2)) (DISCH t2 th3) 840 * end 841 * handle _ => ERR{function = "DISJ_CASES",message = ""}; 842 *---------------------------------------------------------------------------*) 843 844fun dest_disj tm = 845 let val (Rator,N) = dest_comb tm 846 val (c,M) = dest_comb Rator 847 val {Name,Thy,...} = dest_thy_const c 848 in 849 if Name="\\/" andalso Thy="bool" then (M,N) else ERR "" "" 850 end 851 852 853fun DISJ_CASES dth ath bth = 854 let val _ = Assert (aconv (concl ath) (concl bth)) "" "" 855 val (disj1,disj2) = dest_disj (concl dth) 856 in 857 make_thm Count.DisjCases 858 (itlist Tag.merge [tag dth, tag ath, tag bth] empty_tag, 859 union_hyp (hypset dth) (union_hyp (disch(disj1, hypset ath)) 860 (disch(disj2, hypset bth))), 861 concl ath) 862 end 863 handle HOL_ERR _ => ERR "DISJ_CASES" ""; 864 865 866(*--------------------------------------------------------------------------- 867 * NOT introduction 868 * 869 * A |- t ==> F 870 * ------------ 871 * A |- ~t 872 * 873 * fun NOT_INTRO th = 874 * let val (t,_) = dest_imp(concl th) 875 * in MP (SPEC t IMP_F) th 876 * end 877 * handle _ => ERR{function = "NOT_INTRO",message = ""}; 878 *---------------------------------------------------------------------------*) 879 880fun NOT_INTRO th = 881 let val (ant,c) = dest_imp(concl th) 882 in Assert (c = Susp.force F) "" ""; 883 make_thm Count.NotIntro (tag th, hypset th, Susp.force mk_neg ant) 884 end 885 handle HOL_ERR _ => ERR "NOT_INTRO" ""; 886 887 888(*--------------------------------------------------------------------------- 889 * Negation elimination 890 * 891 * A |- ~ t 892 * -------------- 893 * A |- t ==> F 894 * 895 * fun NOT_ELIM th = 896 * let val (_,t) = dest_comb(concl th) 897 * in MP (SPEC t F_IMP) th 898 * end 899 * handle _ => ERR{function = "NOT_ELIM",message = ""}; 900 *---------------------------------------------------------------------------*) 901 902local fun dest M = 903 let val (Rator,Rand) = dest_comb M 904 in (dest_thy_const Rator, Rand) 905 end 906in 907fun NOT_ELIM th = 908 case with_exn dest (concl th) (thm_err "NOT_ELIM" "") 909 of ({Name="~", Thy="bool",...},Rand) 910 => make_thm Count.NotElim 911 (tag th, hypset th, Term.prim_mk_imp Rand (Susp.force F)) 912 | otherwise => ERR "NOT_ELIM" "" 913end; 914 915 916(*---------------------------------------------------------------------------* 917 * Classical contradiction rule * 918 * * 919 * A,"~t" |- F * 920 * -------------- * 921 * A |- t * 922 * * 923 * fun CCONTR t th = * 924 * let val th1 = RIGHT_BETA(AP_THM NOT_DEF t) * 925 * and v = genvar (--`:bool`--) * 926 * val th2 = EQT_ELIM (ASSUME (--`^t = T`--)) * 927 * val th3 = SUBST [(th1,v)] (--`^v ==> F`--) (DISCH (--`~ ^t`--) th) * 928 * val th4 = SUBST[(ASSUME(--`^t = F`--),v)] (--`(^v ==>F)==>F`--)th3 * 929 * val th5 = MP th4 (EQT_ELIM (CONJUNCT2 IMP_CLAUSE4)) * 930 * val th6 = EQ_MP (SYM(ASSUME (--`^t = F`--))) th5 * 931 * in * 932 * DISJ_CASES (SPEC t BOOL_CASES_AX) th2 th6 * 933 * end handle _ => ERR{function = "CCONTR",message = ""} * 934 *---------------------------------------------------------------------------*) 935 936fun CCONTR w fth = 937 (Assert (concl fth = Susp.force F) "CCONTR" ""; 938 make_thm Count.Ccontr 939 (tag fth, disch(Susp.force mk_neg w, hypset fth), w) 940 handle HOL_ERR _ => ERR "CCONTR" ""); 941 942 943(*---------------------------------------------------------------------------* 944 * Instantiate free variables in a theorem * 945 *---------------------------------------------------------------------------*) 946 947fun INST [] th = th 948 | INST theta th = 949 if List.all (is_var o #redex) theta then 950 let 951 val substf = subst theta 952 in 953 make_thm Count.Inst 954 (tag th, hypset_map substf (hypset th), substf (concl th)) 955 handle HOL_ERR _ => ERR "INST" "" 956 end 957 else 958 raise ERR "INST" "can only instantiate variables" 959 960(*---------------------------------------------------------------------------* 961 * Now some derived rules optimized for computations, avoiding most * 962 * of useless type-checking, using pointer equality and delayed * 963 * substitutions. See computeLib for further details. * 964 *---------------------------------------------------------------------------*) 965 966(*---------------------------------------------------------------------------* 967 * A |- t = (\x.m) n * 968 * --------------------- Beta * 969 * A |- t = m{x\n} * 970 * * 971 * Other implementation (less efficient not using explicit subst.): * 972 * val Beta = Drule.RIGHT_BETA * 973 *---------------------------------------------------------------------------*) 974 975fun Beta th = 976 let val (lhs, rhs, ty) = Term.dest_eq_ty (concl th) 977 in make_thm Count.Beta 978 (tag th, hypset th, mk_eq_nocheck ty lhs (Term.lazy_beta_conv rhs)) 979 end 980 handle HOL_ERR _ => ERR "Beta" ""; 981 982 983(*---------------------------------------------------------------------------* 984 * This rule behaves like a tactic: given a goal (reducing the rhs of thm), * 985 * it returns two subgoals (reducing the rhs of th1 and th2), together * 986 * with a validation (mkthm), that builds the normal form of t from the * 987 * normal forms of u and v. * 988 * NB: we do not have to typecheck the rator u, and we replaced the alpha * 989 * conversion test with pointer equality. * 990 * * 991 * |- u = u (th1) |- v = v (th2) * 992 * (thm) ... ... * 993 * A |- t = u v A' |- u = u' (th1') A'' |- v = v' (th2') * 994 * ---------------------------------------------------------------- * 995 * A u A' u A'' |- t = u' v' * 996 * * 997 * Could be implemented outside Thm as: * 998 * fun Mk_comb th = * 999 * let val {Rator,Rand} = dest_comb(rhs (concl th)) * 1000 * fun mka th1 th2 = TRANS th (MK_COMB(th1,th2)) in * 1001 * (REFL Rator, REFL Rand, mka) * 1002 * end * 1003 *---------------------------------------------------------------------------*) 1004 1005fun Mk_comb thm = 1006 let val (lhs, rhs, ty) = Term.dest_eq_ty (concl thm) 1007 val (Rator,Rand) = dest_comb rhs 1008 fun mkthm th1' th2' = 1009 let val (lhs1, rhs1, _) = Term.dest_eq_ty (concl th1') 1010 val _ = Assert (lhs1 = Rator) "" "" 1011 val (lhs2, rhs2, _) = Term.dest_eq_ty (concl th2') 1012 val _ = Assert (lhs2 = Rand) "" "" 1013 val (ocls,hyps) = tag_hyp_union [thm, th1', th2'] 1014 in make_thm Count.MkComb 1015 (ocls, hyps,mk_eq_nocheck ty lhs (mk_comb(rhs1,rhs2))) 1016 end 1017 handle HOL_ERR _ => ERR "Mk_comb" ""; 1018 val aty = type_of Rand (* typing! *) 1019 val th1 = refl_nocheck (aty --> ty) Rator 1020 val th2 = refl_nocheck aty Rand 1021 in (th1,th2,mkthm) 1022 end 1023 handle HOL_ERR _ => ERR "Mk_comb" ""; 1024 1025(*---------------------------------------------------------------------------* 1026 * |- u = u (th1) * 1027 * (thm) ... * 1028 * A |- t = \x.u A' |- u = u' (th1') * 1029 * ---------------------------------------- x not in FV(A') * 1030 * A u A' |- t = \x.u' * 1031 * * 1032 * Could be implemented outside Thm as: * 1033 * fun Mk_abs th = * 1034 * let val {Bvar,Body} = dest_abs(rhs (concl th)) in * 1035 * (Bvar, REFL Body, (fn th1 => TRANS th (ABS Bvar th1))) * 1036 * end * 1037 *---------------------------------------------------------------------------*) 1038 1039fun Mk_abs thm = 1040 let val (lhs, rhs, ty) = Term.dest_eq_ty (concl thm) 1041 val (Bvar,Body) = dest_abs rhs 1042 fun mkthm th1' = 1043 let val (lhs1, rhs1, _) = Term.dest_eq_ty (concl th1') 1044 val _ = Assert (EQ lhs1 Body) "" "" 1045 val _ = Assert (not (var_occursl Bvar (hypset th1'))) "" "" 1046 val (ocls,hyps) = tag_hyp_union [thm, th1'] 1047 in make_thm Count.Abs 1048 (ocls, hyps, mk_eq_nocheck ty lhs (mk_abs(Bvar, rhs1))) 1049 end 1050 handle HOL_ERR _ => ERR "Mk_abs" "" 1051 val th1 = refl_nocheck (rng ty) Body 1052 in (Bvar,th1,mkthm) 1053 end 1054 handle HOL_ERR _ => ERR "Mk_abs" ""; 1055 1056(*---------------------------------------------------------------------------* 1057 * Same as SPEC, but without propagating the substitution. Spec = SPEC. * 1058 *---------------------------------------------------------------------------*) 1059 1060fun Specialize t th = 1061 let val (Rator,Rand) = dest_comb(concl th) 1062 val {Name,Thy,...} = dest_thy_const Rator 1063 in 1064 Assert (Thy="bool" andalso Name="!") "" ""; 1065 make_thm Count.Spec 1066 (tag th, hypset th, Term.lazy_beta_conv(mk_comb(Rand,t))) 1067 end 1068 handle HOL_ERR _ => ERR "Specialize" ""; 1069 1070(*---------------------------------------------------------------------------* 1071 * Construct a theorem directly and attach the given tag to it. * 1072 *---------------------------------------------------------------------------*) 1073 1074fun mk_oracle_thm tg (asl,c) = 1075 (Assert (Lib.all is_bool (c::asl)) "mk_oracle_thm" "not a proposition" 1076 ; Assert (tg <> "DISK_THM") "mk_oracle_thm" "invalid user tag" 1077 ; make_thm Count.Oracle (Tag.read tg,list_hyp asl,c)); 1078 1079 1080val mk_thm = mk_oracle_thm "MK_THM" 1081 1082fun add_tag (tag1, THM(tag2, h,c)) = THM(Tag.merge tag1 tag2, h, c) 1083 1084(*---------------------------------------------------------------------------* 1085 * The following two are only used internally 1086 *---------------------------------------------------------------------------*) 1087 1088fun mk_axiom_thm (r,c) = 1089 (Assert (type_of c = bool) "mk_axiom_thm" "Not a proposition!"; 1090 make_thm Count.Axiom (Tag.ax_tag r, empty_hyp, c)) 1091 1092fun mk_defn_thm (witness_tag, c) = 1093 (Assert (type_of c = bool) "mk_defn_thm" "Not a proposition!"; 1094 make_thm Count.Definition (witness_tag,empty_hyp,c)) 1095 1096(* ---------------------------------------------------------------------- 1097 Primitive Definition Principles 1098 ---------------------------------------------------------------------- *) 1099 1100fun ERR f msg = HOL_ERR {origin_structure = "Thm", 1101 origin_function = f, message = msg} 1102val TYDEF_ERR = ERR "prim_type_definition" 1103val DEF_ERR = ERR "new_definition" 1104val SPEC_ERR = ERR "new_specification" 1105 1106val TYDEF_FORM_ERR = TYDEF_ERR "expected a theorem of the form \"?x. P x\"" 1107val DEF_FORM_ERR = DEF_ERR "expected a term of the form \"v = M\"" 1108 1109(* some simple term manipulation functions *) 1110fun mk_exists (absrec as (Bvar,_)) = 1111 mk_comb(mk_thy_const{Name="?",Thy="bool", Ty= (type_of Bvar-->bool)-->bool}, 1112 mk_abs absrec) 1113 1114fun dest_eq M = 1115 let val (Rator,r) = dest_comb M 1116 val (eq,l) = dest_comb Rator 1117 in case dest_thy_const eq 1118 of {Name="=",Thy="min",...} => (l,r) 1119 | _ => raise ERR "dest_eq" "not an equality" 1120 end; 1121 1122fun mk_eq (lhs,rhs) = 1123 let val ty = type_of lhs 1124 val eq = mk_thy_const{Name="=",Thy="min",Ty=ty-->ty-->bool} 1125 in list_mk_comb(eq,[lhs,rhs]) 1126 end; 1127 1128fun nstrip_exists 0 t = ([],t) 1129 | nstrip_exists n t = 1130 let val (Bvar, Body) = dest_exists t 1131 val (l,t'') = nstrip_exists (n-1) Body 1132 in (Bvar::l, t'') 1133 end; 1134 1135(* standard checks *) 1136fun check_null_hyp th f = 1137 if null(hyp th) then () 1138 else raise f "theorem must have no assumptions"; 1139 1140fun check_free_vars tm f = 1141 case free_vars tm 1142 of [] => () 1143 | V => raise f (String.concat 1144 ("Free variables in rhs of definition: " 1145 :: commafy (map (Lib.quote o fst o dest_var) V))); 1146 1147fun check_vars tm vars f = 1148 case Lib.set_diff (free_vars tm) vars 1149 of [] => () 1150 | extras => 1151 raise f (String.concat 1152 ("Unbound variable(s) in definition: " 1153 :: commafy (map (Lib.quote o fst o dest_var) extras))); 1154 1155fun check_tyvars body_tyvars ty f = 1156 case Lib.set_diff body_tyvars (Type.type_vars ty) 1157 of [] => () 1158 | extras => 1159 raise f (String.concat 1160 ("Unbound type variable(s) in definition: " 1161 :: commafy (map (Lib.quote o Type.dest_vartype) extras))); 1162 1163fun prim_type_definition (name as {Thy, Tyop}, thm) = let 1164 val (bv,Body) = with_exn dest_exists (concl thm) TYDEF_FORM_ERR 1165 val (P,v) = with_exn dest_comb Body TYDEF_FORM_ERR 1166 val _ = assert_exn (equal bv) v TYDEF_FORM_ERR 1167 val Pty = type_of P 1168 val (dom,rng) = with_exn Type.dom_rng Pty TYDEF_FORM_ERR 1169 val tyvars = Listsort.sort Type.compare (type_vars_in_term P) 1170 val checked = check_null_hyp thm TYDEF_ERR 1171 val checked = 1172 assert_exn null (free_vars P) 1173 (TYDEF_ERR "subset predicate must be a closed term") 1174 val checked = assert_exn (op=) (rng,bool) 1175 (TYDEF_ERR "subset predicate has the wrong type") 1176 val _ = Type.prim_new_type name (List.length tyvars) 1177 val newty = Type.mk_thy_type{Tyop=Tyop,Thy=Thy,Args=tyvars} 1178 val repty = newty --> dom 1179 val rep = mk_primed_var("rep", repty) 1180 val TYDEF = mk_thy_const{Name="TYPE_DEFINITION", Thy="bool", 1181 Ty = Pty --> (repty-->bool)} 1182in 1183 mk_defn_thm(tag thm, mk_exists(rep, list_mk_comb(TYDEF,[P,rep]))) 1184end 1185 1186(* subsumed by gen_prim_specification 1187fun prim_constant_definition Thy M = let 1188 val (lhs, rhs) = with_exn dest_eq M DEF_FORM_ERR 1189 val {Name, Thy, Ty} = 1190 if is_const lhs then let 1191 val r as {Name, Ty, ...} = dest_thy_const lhs 1192 (* note how we ignore the constant's theory; this is because the 1193 user may be defining another version of an earlier constant *) 1194 in 1195 {Name = Name, Thy = Thy, Ty = Ty} 1196 end 1197 else if is_var lhs then let 1198 val (n, ty) = dest_var lhs 1199 in 1200 {Name = n, Ty = ty, Thy = Thy} 1201 end 1202 else raise DEF_FORM_ERR 1203 val checked = check_free_vars rhs DEF_ERR 1204 val checked = check_tyvars (type_vars_in_term rhs) Ty DEF_ERR 1205 val new_lhs = Term.prim_new_const {Name = Name, Thy = Thy} Ty 1206in 1207 mk_defn_thm(empty_tag, mk_eq(new_lhs, rhs)) 1208end 1209*) 1210 1211fun bind thy s ty = 1212 Term.prim_new_const {Name = s, Thy = thy} ty 1213 1214fun prim_specification thyname cnames th = let 1215 val con = concl th 1216 val checked = check_null_hyp th SPEC_ERR 1217 val checked = check_free_vars con SPEC_ERR 1218 val checked = 1219 assert_exn (op=) (length(mk_set cnames),length cnames) 1220 (SPEC_ERR "duplicate constant names in specification") 1221 val (V,body) = 1222 with_exn (nstrip_exists (length cnames)) con 1223 (SPEC_ERR "too few existentially quantified variables") 1224 fun vOK V v = check_tyvars V (type_of v) SPEC_ERR 1225 val checked = List.app (vOK (type_vars_in_term body)) V 1226 fun addc v s = v |-> bind thyname s (snd(dest_var v)) 1227in 1228 mk_defn_thm (tag th, subst (map2 addc V cnames) body) 1229end 1230 1231fun gen_prim_specification thyname th = let 1232 val hyps = hypset th 1233 val stys = 1234 let 1235 fun foldthis (tm,stys) = 1236 let 1237 val (l,r) = 1238 with_exn dest_eq tm (SPEC_ERR "non-equational hypothesis") 1239 val (s,ty) = 1240 with_exn dest_var l (SPEC_ERR "lhs of hyp not a variable") 1241 val checked = check_free_vars r SPEC_ERR 1242 val checked = check_tyvars (type_vars_in_term r) ty SPEC_ERR 1243 in 1244 (s,ty)::stys 1245 end 1246 in 1247 HOLset.foldl foldthis [] hyps 1248 end 1249 val cnames = List.map fst stys 1250 val checked = 1251 assert_exn (op=) (length(mk_set cnames),length cnames) 1252 (SPEC_ERR "duplicate constant names in specification") 1253 val body = concl th 1254 val checked = check_vars body (List.map mk_var stys) SPEC_ERR 1255 fun addc (s,ty) = (mk_var (s,ty)) |-> bind thyname s ty 1256in 1257 (cnames, mk_defn_thm (tag th, subst (List.map addc stys) body)) 1258end 1259 1260 1261 1262 1263 1264 1265 1266(* ---------------------------------------------------------------------- 1267 Creating a theorem from disk 1268 ---------------------------------------------------------------------- *) 1269 1270local 1271 val mk_disk_thm = make_thm Count.Disk 1272in 1273fun disk_thm ((d,ocl), termlist) = let 1274 val c = hd termlist 1275 val asl = tl termlist 1276in 1277 mk_disk_thm (Tag.read_disk_tag (d,ocl),list_hyp asl,c) 1278end 1279end; (* local *) 1280 1281(* ---------------------------------------------------------------------- 1282 Saving dependencies of a theorem 1283 ---------------------------------------------------------------------- *) 1284 1285(* This reference is automatically reset to 0 each time you create 1286 a theory. *) 1287val thm_order = ref 0 1288 1289fun save_dep thy (th as (THM(t,h,c))) = 1290 let 1291 val did = (thy,!thm_order) 1292 val dl = (transfer_thydepl o dep_of o tag) th 1293 val dep = DEP_SAVED(did,dl) 1294 in 1295 thm_order := (!thm_order) + 1; 1296 THM(Tag.set_dep dep t,h,c) 1297 end 1298 1299 1300end (* Thm *) 1301