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