1structure Logging :> Logging = 2struct 3 4open OpenTheoryCommon 5structure Map = OpenTheoryMap.Map 6 7val ERR = Feedback.mk_HOL_ERR "Logging" 8 9fun uptodate_const Thy Name = 10 Theory.uptodate_term (Term.prim_mk_const {Thy=Thy,Name=Name}) 11 handle Feedback.HOL_ERR {origin_function="prim_mk_const",...} => false 12 13val verbosity = ref 0 14val _ = Feedback.register_trace("opentheory logging",verbosity,5) 15 16val proof_type = let open Thm fun 17 f Axiom_prf = "Axiom" 18|f (ABS_prf _) = "ABS" 19|f (ALPHA_prf _) = "ALPHA" 20|f (AP_TERM_prf _) = "AP_TERM" 21|f (AP_THM_prf _) = "AP_THM" 22|f (ASSUME_prf _) = "ASSUME" 23|f (BETA_CONV_prf _) = "BETA_CONV" 24|f (CCONTR_prf _) = "CCONTR" 25|f (CHOOSE_prf _) = "CHOOSE" 26|f (CONJ_prf _) = "CONJ" 27|f (CONJUNCT1_prf _) = "CONJUNCT1" 28|f (CONJUNCT2_prf _) = "CONJUNCT2" 29|f (DISCH_prf _) = "DISCH" 30|f (DISJ_CASES_prf _) = "DISJ_CASES" 31|f (DISJ1_prf _) = "DISJ1" 32|f (DISJ2_prf _) = "DISJ2" 33|f (EQ_IMP_RULE1_prf _) = "EQ_IMP_RULE1" 34|f (EQ_IMP_RULE2_prf _) = "EQ_IMP_RULE2" 35|f (EQ_MP_prf _) = "EQ_MP" 36|f (EXISTS_prf _) = "EXISTS" 37|f (GEN_prf _) = "GEN" 38|f (GEN_ABS_prf _) = "GEN_ABS" 39|f (INST_TYPE_prf _) = "INST_TYPE" 40|f (INST_prf _) = "INST" 41|f (MK_COMB_prf _) = "MK_COMB" 42|f (MP_prf _) = "MP" 43|f (NOT_INTRO_prf _) = "NOT_INTRO" 44|f (NOT_ELIM_prf _) = "NOT_ELIM" 45|f (REFL_prf _) = "REFL" 46|f (SPEC_prf _) = "SPEC" 47|f (SUBST_prf _) = "SUBST" 48|f (SYM_prf _) = "SYM" 49|f (TRANS_prf _) = "TRANS" 50|f (Beta_prf _) = "Beta" 51|f (Def_tyop_prf _) = "Def_tyop" 52|f (Def_const_prf _) = "Def_const" 53|f (Def_const_list_prf _) = "Def_const_list" 54|f (Def_spec_prf _) = "Def_spec" 55|f (Mk_abs_prf _) = "Mk_abs" 56|f (Mk_comb_prf _) = "Mk_comb" 57|f (Specialize_prf _) = "Specialize" 58|f (deductAntisym_prf _) = "deductAntisym" 59in f end 60 61datatype log_state = 62 Not_logging 63| Active_logging of TextIO.outstream 64 65val log_state = ref Not_logging 66 67fun log_raw s = 68 case !log_state of 69 Active_logging h => TextIO.output (h,s^"\n") 70 | Not_logging => () 71 72fun log_num n = log_raw (Int.toString n) 73 74fun log_name s = log_raw ("\""^(OpenTheoryMap.otname_to_string s)^"\"") 75 76fun log_comment s = log_raw ("#"^(String.translate (fn #"\n" => "\n#" | c => String.str c) s)) 77 78fun log_command s = log_raw s 79 80fun log_nil () = log_command "nil" 81 82fun log_list log = let 83 fun logl [] = log_nil () 84 | logl (h::t) = (log h; logl t; log_command "cons") 85in logl end 86 87fun log_pair (loga,logb) (a,b) = let 88 val _ = loga a 89 val _ = logb b 90 val _ = log_nil () 91 val _ = log_command "cons" 92 val _ = log_command "cons" 93in () end 94 95fun log_redres loga logb {redex,residue} = 96 log_pair (loga,logb) (redex,residue) 97 98type thy_tyop = OpenTheoryMap.thy_tyop 99type thy_const = OpenTheoryMap.thy_const 100type otname = OpenTheoryMap.otname 101 102val (log_term, log_thm, log_clear, 103 set_const_name_handler, reset_const_name_handler, 104 set_tyop_name_handler, reset_tyop_name_handler) = let 105 val (reset_key,next_key) = let 106 val key = ref 0 107 fun reset() = key := 0 108 fun next() = let val k = !key in (key := k+1; k) end 109 in (reset,next) end 110 111 val (reset_dict,peek_dict,save_dict) = let 112 fun new_dict() = Map.mkDict object_compare 113 val dict = ref (new_dict()) 114 fun reset() = dict := new_dict() 115 fun peek x = Map.peek(!dict,x) 116 fun save x = case peek x of 117 SOME k => k 118 | NONE => let 119 val k = next_key() 120 val _ = dict := Map.insert(!dict,x,k) 121 val _ = log_num k 122 val _ = log_command "def" 123 in k end 124 in (reset,peek,save) end 125 fun saved ob = case peek_dict ob of 126 SOME k => let 127 val _ = log_num k 128 val _ = log_command "ref" 129 in true end 130 | NONE => false 131 132 fun log_type_var ty = log_name (tyvar_to_ot (Type.dest_vartype ty)) 133 134 local 135 open OpenTheoryMap 136 fun default_tnh t = raise ERR "log_tyop_name" 137 ("No OpenTheory name for type "^(#Thy t)^"$"^(#Tyop t)) 138 fun default_cnh c = raise ERR "log_const_name" 139 ("No OpenTheory name for constant "^(#Thy c)^"$"^(#Name c)) 140 val tnh = ref default_tnh 141 val cnh = ref default_cnh 142 in 143 fun log_tyop_name tyop = let 144 val n = Map.find(tyop_to_ot_map(),tyop) 145 handle Map.NotFound => (!tnh) tyop 146 val _ = log_name n 147 in n end 148 fun log_const_name {Thy="Logging",Name} = 149 log_raw ("\""^Name^"\"") 150 | log_const_name const = let 151 val n = Map.find(const_to_ot_map(),const) 152 handle Map.NotFound => (!cnh) const 153 in log_name n end 154 fun set_const_name_handler h = 155 cnh := (fn c => h c handle _ => default_cnh c) 156 fun reset_const_name_handler() = cnh := default_cnh 157 fun set_tyop_name_handler h = 158 tnh := (fn t => h t handle _ => default_tnh t) 159 fun reset_tyop_name_handler() = tnh := default_tnh 160 end 161 162 fun log_tyop tyop = let 163 val ob = OTypeOp tyop 164 in if saved ob then () else let 165 val _ = log_tyop_name tyop 166 val _ = log_command "typeOp" 167 val _ = save_dict ob 168 in () end 169 end 170 171 fun log_const const = let 172 val ob = OConst const 173 in if saved ob then () else let 174 val _ = log_const_name const 175 val _ = log_command "const" 176 val _ = save_dict ob 177 in () end 178 end 179 180 fun log_type ty = let 181 val ob = OType ty 182 in if saved ob then () else let 183 open Feedback 184 val _ = let 185 val {Thy,Args,Tyop} = Type.dest_thy_type ty 186 val _ = log_tyop {Thy=Thy,Tyop=Tyop} 187 val _ = log_list log_type Args 188 val _ = log_command "opType" 189 in () end handle HOL_ERR {origin_function="dest_thy_type",...} => let 190 val _ = log_type_var ty 191 val _ = log_command "varType" 192 in () end 193 val _ = save_dict ob 194 in () end 195 end 196 197 fun log_var v = let 198 val ob = OVar v 199 in if saved ob then () else let 200 val (n,ty) = Term.dest_var v 201 val _ = log_name ([],n) 202 val _ = log_type ty 203 val _ = log_command "var" 204 val _ = save_dict ob 205 in () end 206 end 207 208 fun strip_old s = let 209 open Substring 210 val s = triml 3 (trimr 5 (full s)) 211 val (_,s) = splitl Char.isDigit s 212 val s = triml 2 s 213 in string s end 214 215 fun log_term tm = let 216 val ob = OTerm tm 217 in if saved ob then () else let 218 open Term Feedback 219 val _ = let 220 val {Thy,Name,Ty} = dest_thy_const tm 221 val Name = if uptodate_const Thy Name then Name else strip_old Name 222 val _ = log_const {Thy=Thy,Name=Name} 223 val _ = log_type Ty 224 val _ = log_command "constTerm" 225 in () end handle HOL_ERR {origin_function="dest_thy_const",...} => let 226 val (t1,t2) = dest_comb tm 227 val _ = log_term t1 228 val _ = log_term t2 229 val _ = log_command "appTerm" 230 in () end handle HOL_ERR {origin_function="dest_comb",...} => let 231 val (v,b) = dest_abs tm 232 val _ = log_var v 233 val _ = log_term b 234 val _ = log_command "absTerm" 235 in () end handle HOL_ERR {origin_function="dest_abs",...} => let 236 val _ = log_var tm 237 val _ = log_command "varTerm" 238 in () end 239 val _ = save_dict ob 240 in () end 241 end 242 243 val log_subst = 244 log_pair 245 (log_list (log_redres log_type_var log_type), 246 log_list (log_redres log_var log_term)) 247 fun log_type_subst s = log_subst (s,[]) 248 fun log_term_subst s = log_subst ([],s) 249 250 (* Attribution: ideas (and code) for reconstructing DISCH, SPEC, GEN, etc. 251 taken from HOL Light *) 252 local open Thm Conv boolTheory boolSyntax Term Type Lib Drule in 253 fun proveHyp th1 th2 = 254 case HOLset.find (aconv (concl th1)) (hypset th2) of 255 SOME _ => EQ_MP (deductAntisym th1 th2) th1 256 | NONE => th2 257 val p = ``p:bool`` 258 val q = ``q:bool`` 259 val eqtIntro = let 260 val pth = let 261 val th1 = deductAntisym (ASSUME p) TRUTH 262 val th2 = EQT_ELIM(ASSUME(concl th1)) 263 in deductAntisym th2 th1 end 264 in fn th => EQ_MP (INST[p|->concl th] pth) th end 265 (* These are in the OpenTheory standard library, so we can give them axiom proofs *) 266 val IMP_DEF = mk_thm([],``$==> = \p q. p /\ q <=> p``) 267 val EXISTS_DEF = mk_thm([],``$? = \P:'a->bool. !q. (!x. P x ==> q) ==> q``) 268 val AND_DEF = mk_thm([],``$/\ = \p q. (\f:bool->bool->bool. f p q) = (\f. f T T)``) 269 val EXISTS_THM = boolTheory.EXISTS_DEF 270 val DISCH_pth = SYM(BETA_RULE (AP_THM (AP_THM IMP_DEF p) q)) 271 val MP_pth = let 272 val th1 = BETA_RULE (AP_THM (AP_THM IMP_DEF p) q) 273 val th2 = EQ_MP th1 (ASSUME ``p ==> q``) 274 in CONJUNCT2 (EQ_MP (SYM th2) (ASSUME p)) end 275 val P = mk_var("P",alpha-->bool) 276 val x = mk_var("x",alpha) 277 val SPEC_pth = let 278 val th1 = EQ_MP (AP_THM FORALL_DEF P) (ASSUME (mk_comb(universal,P))) 279 val th2 = AP_THM (CONV_RULE BETA_CONV th1) x 280 val th3 = CONV_RULE (RAND_CONV BETA_CONV) th2 281 in DISCH_ALL (EQT_ELIM th3) end 282 val GEN_pth = let 283 val th1 = ASSUME (mk_eq(P,mk_abs(x,T))) 284 val th2 = AP_THM FORALL_DEF P 285 in EQ_MP (SYM(CONV_RULE(RAND_CONV BETA_CONV) th2)) th1 end 286 val Q = mk_var("Q",bool) 287 val EXISTS_pth = let 288 val th1 = CONV_RULE (RAND_CONV BETA_CONV) (AP_THM EXISTS_DEF P) 289 val tm = (mk_forall(x,mk_imp(mk_comb(P,x),Q))) 290 val th2 = SPEC x (ASSUME tm) 291 val th3 = DISCH tm (MP th2 (ASSUME (mk_comb(P,x)))) 292 in EQ_MP (SYM th1) (GEN Q th3) end 293 val CHOOSE_pth = let 294 val th1 = CONV_RULE (RAND_CONV BETA_CONV) (AP_THM EXISTS_DEF P) 295 val th2 = SPEC Q (UNDISCH(fst(EQ_IMP_RULE th1))) 296 in DISCH_ALL (DISCH (mk_comb(existential,P)) (UNDISCH th2)) end 297 val f = mk_var("f",bool-->bool-->bool) 298 val CONJ_pth = let 299 val pth = ASSUME p 300 val qth = ASSUME q 301 val th1 = MK_COMB(AP_TERM f (eqtIntro pth),eqtIntro qth) 302 val th2 = ABS f th1 303 val th3 = BETA_RULE (AP_THM (AP_THM AND_DEF p) q) 304 in EQ_MP (SYM th3) th2 end 305 val P = mk_var("P",bool) 306 val REBETA_RULE = CONV_RULE(REDEPTH_CONV BETA_CONV) 307 fun CONJUNCT_pth t = let 308 val th1 = CONV_RULE (RAND_CONV BETA_CONV) (AP_THM AND_DEF P) 309 val th2 = CONV_RULE (RAND_CONV BETA_CONV) (AP_THM th1 Q) 310 val th3 = EQ_MP th2 (ASSUME (mk_conj(P,Q))) 311 in EQT_ELIM(REBETA_RULE (AP_THM th3 (mk_abs(p,mk_abs(q,t))))) end 312 val CONJUNCT1_pth = CONJUNCT_pth p 313 val CONJUNCT2_pth = CONJUNCT_pth q 314 val th1 = CONV_RULE (RAND_CONV BETA_CONV) (AP_THM OR_DEF P) 315 val th2 = CONV_RULE (RAND_CONV BETA_CONV) (AP_THM th1 Q) 316 fun DISJ_pth t = let 317 val th3 = MP (ASSUME (mk_imp(t,p))) (ASSUME t) 318 val th4 = GEN p (DISCH (mk_imp(P,p)) (DISCH (mk_imp(Q,p)) th3)) 319 in EQ_MP (SYM th2) th4 end 320 val DISJ1_pth = DISJ_pth P 321 val DISJ2_pth = DISJ_pth Q 322 val R = mk_var("R",bool) 323 val DISJ_CASES_pth = let 324 val th3 = SPEC R (EQ_MP th2 (ASSUME (mk_disj(P,Q)))) 325 in UNDISCH (UNDISCH th3) end 326 val NOT_ELIM_pth = CONV_RULE (RAND_CONV BETA_CONV) (AP_THM NOT_DEF P) 327 val NOT_INTRO_pth = SYM NOT_ELIM_pth 328 val SEL_CONV = RATOR_CONV (REWR_CONV EXISTS_THM) THENC BETA_CONV 329 val SEL_RULE = CONV_RULE SEL_CONV 330 fun specify c (th,defs) = let 331 val th1 = SEL_RULE th 332 val (l,r) = dest_comb(concl th1) 333 val {Thy,Name,...} = dest_thy_const c 334 val Name = if uptodate_const Thy Name then Name else strip_old Name 335 val th2 = mk_proof_thm (Def_const_prf({Thy=Thy,Name=Name},r)) ([],mk_eq(c,r)) 336 val defs = th2 :: defs 337 val th = CONV_RULE BETA_CONV (EQ_MP (AP_TERM l (SYM th2)) th1) 338 in (th,defs) end 339 val EXISTENCE_RULE = CONV_RULE (SEL_CONV THENC (RATOR_CONV ETA_CONV)) 340 fun mk_ra (b,r,rep,abs) = mk_eq(mk_abs(r,mk_eq(mk_comb(rep,mk_comb(abs,r)),r)), 341 mk_abs(r,mk_comb(b,r))) 342 fun mk_ar (abs,rep,a) = mk_eq(mk_abs(a,mk_comb(abs,mk_comb(rep,a))), 343 mk_abs(a,a)) 344 fun absspec x th = CONV_RULE(BINOP_CONV BETA_CONV)(AP_THM th x) 345 val Def_tyop_pth = let 346 val phi = mk_var("phi",alpha-->bool) 347 val abs = mk_var("abs",alpha-->beta) 348 val rep = mk_var("rep",beta-->alpha) 349 val a = mk_var("a",beta) 350 val r = mk_var("r",alpha) 351 val ar = ASSUME (mk_ar(abs,rep,a)) 352 val ra = ASSUME (mk_ra(phi,r,rep,abs)) 353 val c = concl TYPE_DEFINITION 354 val tyd = lhs c 355 val (c1,c2) = dest_conj(snd(dest_abs(snd(dest_abs(rhs c))))) 356 val ([x',x''],_) = strip_forall c1 357 val (x,_) = dest_forall c2 358 val w = mk_comb(mk_comb(tyd,phi),rep) 359 val th1 = BETA_RULE (AP_THM (AP_THM TYPE_DEFINITION phi) rep) 360 val rx' = mk_comb(rep,x') 361 val rr = mk_eq(rx',mk_comb(rep,x'')) 362 val xar = absspec x' ar 363 val th2 = TRANS (TRANS (SYM xar) (AP_TERM abs (ASSUME rr))) (absspec x'' ar) 364 val th3 = GEN x' (GEN x'' (DISCH rr th2)) 365 val phx = mk_comb(phi,x) 366 val xre = mk_eq(x,rx') 367 val exr = mk_exists(x',xre) 368 val xra = absspec x ra 369 val th4 = DISCH phx (EXISTS (exr,mk_comb(abs,x)) (SYM (EQ_MP (SYM xra) (ASSUME phx)))) 370 val xrt = ASSUME xre 371 val th5 = TRANS (REFL rx') (SYM xrt) 372 val th6 = TRANS (AP_TERM rep (TRANS (AP_TERM abs xrt) xar)) th5 373 val th7 = DISCH exr (CHOOSE (x',ASSUME exr) (EQ_MP xra th6)) 374 val th8 = GEN x (deductAntisym (UNDISCH th7) (UNDISCH th4)) 375 in EXISTS (mk_exists(rep,w),rep) (EQ_MP (SYM th1) (CONJ th3 th8)) end 376 end 377 378 fun log_thm th = let 379 open Thm Term Type Lib Drule Conv boolSyntax Feedback 380 val ob = OThm th 381 in if saved ob then () else let 382 val ths = Susp.delay (fn () => (Lib.ppstring Parse.pp_thm th)) 383 val pt = proof_type (proof th) 384 val _ = if !verbosity >= 4 then HOL_MESG("Start a "^pt^" proof for "^(Susp.force ths)) 385 else if !verbosity >= 3 then HOL_MESG(proof_type (proof th)) 386 else () 387 (* 388 val _ = log_comment ("("^pt) 389 *) 390 val _ = case proof th of 391 392 Axiom_prf => let 393 val _ = log_list log_term (hyp th) 394 val _ = log_term (concl th) 395 val _ = log_command "axiom" 396 in () end 397 | ASSUME_prf tm => let 398 val _ = log_term tm 399 val _ = log_command "assume" 400 in () end 401 | BETA_CONV_prf tm => let 402 val _ = log_term tm 403 val _ = log_command "betaConv" 404 in () end 405 | REFL_prf tm => let 406 val _ = log_term tm 407 val _ = log_command "refl" 408 in () end 409 | Def_const_prf (c,t) => let 410 val _ = log_const_name c 411 val _ = log_term t 412 val _ = log_command "defineConst" 413 val k = save_dict ob 414 val _ = log_command "pop" 415 val _ = save_dict (OConst c) 416 val _ = log_command "pop" 417 val _ = log_num k 418 val _ = log_command "ref" 419 in () end 420 | ABS_prf (v,th) => let 421 val _ = log_var v 422 val _ = log_thm th 423 val _ = log_command "absThm" 424 in () end 425 | deductAntisym_prf (th1,th2) => let 426 val _ = log_thm th1 427 val _ = log_thm th2 428 val _ = log_command "deductAntisym" 429 in () end 430 | EQ_MP_prf (th1,th2) => let 431 val _ = log_thm th1 432 val _ = log_thm th2 433 val _ = log_command "eqMp" 434 in () end 435 | INST_prf (s,th) => let 436 val _ = log_term_subst s 437 val _ = log_thm th 438 val _ = log_command "subst" 439 in () end 440 | INST_TYPE_prf (s,th) => let 441 val _ = log_type_subst s 442 val _ = log_thm th 443 val _ = log_command "subst" 444 in () end 445 | MK_COMB_prf (th1,th2) => let 446 val _ = log_thm th1 447 val _ = log_thm th2 448 val _ = log_command "appThm" 449 in () end 450 | ALPHA_prf (t1,t2) => let 451 val t = mk_comb(inst[alpha|->type_of t1]equality, t1) 452 val _ = log_thm (EQ_MP (MK_COMB (REFL t, REFL t2)) (REFL t1)) 453 in () end 454 | TRANS_prf (th1,th2) => let 455 val _ = log_thm th1 456 val _ = log_thm th2 457 val _ = log_command "trans" 458 in () end 459 | SYM_prf th => let 460 val _ = log_thm th 461 val _ = log_command "sym" 462 in () end 463 | AP_TERM_prf (tm,th) => log_thm (MK_COMB(REFL tm, th)) 464 | AP_THM_prf (th,tm) => log_thm (MK_COMB(th, REFL tm)) 465 | Mk_comb_prf (th,th1,th2) => log_thm (TRANS th (MK_COMB(th1,th2))) 466 | Mk_abs_prf (th,bv,th1) => log_thm (TRANS th (ABS bv th1)) 467 | CONJ_prf (th1,th2) => let 468 val th = INST [p|->concl th1,q|->concl th2] CONJ_pth 469 val _ = log_thm (proveHyp th2 (proveHyp th1 th)) 470 in () end 471 | CONJUNCT1_prf th => let 472 val (l,r) = dest_conj(concl th) 473 val _ = log_thm (proveHyp th (INST [P|->l,Q|->r] CONJUNCT1_pth)) 474 in () end 475 | CONJUNCT2_prf th => let 476 val (l,r) = dest_conj(concl th) 477 val _ = log_thm (proveHyp th (INST [P|->l,Q|->r] CONJUNCT2_pth)) 478 in () end 479 | DISCH_prf (tm,th) => let 480 val th1 = CONJ (ASSUME tm) th 481 val th2 = CONJUNCT1 (ASSUME (concl th1)) 482 val pth = INST [p|->tm, q|->concl th] DISCH_pth 483 val _ = log_thm (EQ_MP pth (deductAntisym th1 th2)) 484 in () end 485 | MP_prf (th1,th2) => let 486 val tm = concl th1 487 val (ant,con) = dest_imp tm 488 val th1 = if is_neg tm 489 then let open boolTheory in 490 (CONV_RULE BETA_CONV) 491 (SUBS_OCCS [([1],NOT_DEF)] th1) 492 end 493 else th1 494 val pth = INST [p|->ant, q|->con] MP_pth 495 val _ = log_thm (EQ_MP (deductAntisym th1 496 (EQ_MP (deductAntisym th2 pth) 497 th2)) 498 th1) 499 in () end 500 | SUBST_prf (map,tm,sth) => let 501 val (h,source) = dest_thm sth 502 val fvs = FVL (source::h) empty_varset 503 fun f (m as {redex,residue},(fvs,allfvs,map,tm)) = let 504 val (h,c) = dest_thm residue 505 val allfvs = FVL (c::h) allfvs 506 in 507 if HOLset.member(fvs,redex) then let 508 val vv = prim_variant (HOLset.listItems fvs) redex 509 val fvs = HOLset.add(fvs,vv) 510 val m = {redex=vv,residue=residue} 511 val tm = subst [redex|->vv] tm 512 in (fvs,allfvs,m::map,tm) end 513 else (fvs,allfvs,m::map,tm) 514 end 515 val (_,fvs,map,tm) = foldl f (fvs,fvs,[],tm) map 516 fun rconv fvs source template = (* |- source = template[rhs/vars] *) 517 ALPHA source template 518 handle HOL_ERR _ => 519 if is_var template 520 then valOf(subst_assoc (equal template) map) 521 else let 522 val (sf,sa) = dest_comb source 523 val (tf,ta) = dest_comb template 524 val f = rconv fvs sf tf 525 val a = rconv fvs sa ta 526 in MK_COMB (f,a) end handle HOL_ERR _ => let 527 val (sv,sb) = dest_abs source 528 val (tv,tb) = dest_abs template 529 val vv = prim_variant (HOLset.listItems fvs) tv 530 val sb = subst [sv|->vv] sb 531 val tb = subst [tv|->vv] tb 532 val b = rconv (HOLset.add(fvs,vv)) sb tb 533 in ABS vv b end 534 val _ = log_thm (EQ_MP (rconv fvs source tm) sth) 535 in () end 536 | GEN_prf (v,th) => let 537 val vty = type_of v 538 val P = mk_var("P",vty-->bool) 539 val pth = INST_TY_TERM ([P|->mk_abs(v,concl th)],[alpha|->vty]) GEN_pth 540 val _ = log_thm (proveHyp (ABS v (eqtIntro th)) pth) 541 in () end 542 | DISJ1_prf (th,tm) => let 543 val _ = log_thm (proveHyp th (INST [P|->concl th,Q|->tm] DISJ1_pth)) 544 in () end 545 | DISJ2_prf (tm,th) => let 546 val _ = log_thm (proveHyp th (INST [Q|->concl th,P|->tm] DISJ2_pth)) 547 in () end 548 | SPEC_prf (tm,th) => let 549 val abs = rand(concl th) 550 val (v,_) = dest_abs abs 551 val vty = type_of v 552 val pth = INST_TY_TERM ([mk_var("P",vty-->bool)|->abs,mk_var("x",vty)|->tm],[alpha|->vty]) SPEC_pth 553 val _ = log_thm (CONV_RULE BETA_CONV (MP pth th)) 554 in () end 555 | Specialize_prf (t,th) => log_thm (SPEC t th) 556 | GEN_ABS_prf (c,vlist,th) => let 557 val dom = fst o dom_rng 558 fun foo th = let val (_,_,ty) = dest_eq_ty(concl th) in dom ty end 559 val f = case c of 560 SOME c => let val ty = dom(dom(type_of c)) 561 in fn th => AP_TERM (inst[ty|->foo th] c) th end 562 | NONE => I 563 val _ = log_thm (List.foldr (f o uncurry ABS) th vlist) 564 in () end 565 | EQ_IMP_RULE1_prf th => let 566 val (t1,t2) = dest_eq(concl th) 567 val _ = log_thm (DISCH t1 (EQ_MP th (ASSUME t1))) 568 in () end 569 | EQ_IMP_RULE2_prf th => let 570 val (t1,t2) = dest_eq(concl th) 571 val _ = log_thm (DISCH t2 (EQ_MP (SYM th) (ASSUME t2))) 572 in () end 573 | EXISTS_prf (fm,tm,th) => let 574 val ty = type_of tm 575 val (_,abs) = dest_comb fm 576 val bth = BETA_CONV(mk_comb(abs,tm)) 577 val cth = INST_TY_TERM ([mk_var("P",ty-->bool)|->abs,mk_var("x",ty)|->tm],[alpha|->ty]) EXISTS_pth 578 val _ = log_thm (proveHyp (EQ_MP (SYM bth) th) cth) 579 in () end 580 | CHOOSE_prf (v,th1,th2) => let 581 val vty = type_of v 582 val abs = rand(concl th1) 583 val (bv,bod) = dest_abs abs 584 val cmb = mk_comb(abs,v) 585 val pat = subst [bv|->v] bod 586 val th3 = CONV_RULE BETA_CONV (ASSUME cmb) 587 val th4 = GEN v (DISCH cmb (MP (DISCH pat th2) th3)) 588 val th5 = INST_TY_TERM ([mk_var("P",vty-->bool)|->abs,Q|->concl th2],[alpha|->vty]) CHOOSE_pth 589 val _ = log_thm (MP (MP th5 th4) th1) 590 in () end 591 | DISJ_CASES_prf (th0,th1,th2) => let 592 val c1 = concl th1 593 val c2 = concl th2 594 val (l,r) = dest_disj (concl th0) 595 val th = INST [P|->l,Q|->r,R|->c1] DISJ_CASES_pth 596 val _ = log_thm (proveHyp (DISCH r th2) (proveHyp (DISCH l th1) (proveHyp th0 th))) 597 in () end 598 | NOT_INTRO_prf th => let 599 val _ = log_thm (EQ_MP (INST [P|->rand(rator(concl th))] NOT_INTRO_pth) th) 600 in () end 601 | NOT_ELIM_prf th => let 602 val _ = log_thm (EQ_MP (INST [P|->rand(concl th)] NOT_ELIM_pth) th) 603 in () end 604 | CCONTR_prf (tm,th) => let 605 open boolTheory 606 val th1 = RIGHT_BETA(AP_THM NOT_DEF tm) 607 val tmF = ASSUME(mk_eq(tm,F)) 608 val th2 = EQT_ELIM (ASSUME(mk_eq(tm,T))) 609 val th3 = SUBST [P|->th1] (mk_imp(P,F)) (DISCH (mk_neg tm) th) 610 val th4 = SUBST [P|->(tmF)] (mk_imp(mk_imp(P,F),F)) th3 611 val th5 = MP th4 (SPEC F FALSITY) 612 val th6 = EQ_MP (SYM(tmF)) th5 613 val _ = log_thm (DISJ_CASES (SPEC tm BOOL_CASES_AX) th2 th6) 614 in () end 615 | Beta_prf th => log_thm (RIGHT_BETA th) 616 | Def_spec_prf (cs,th) => let 617 val (th,defs) = rev_itlist specify cs (th,[]) 618 val _ = app log_thm (rev defs) 619 val _ = log_thm th 620 in () end 621 | Def_const_list_prf (thyname,stys,th) => let 622 val nvars = map (fn (s,ty) => ({Thy=thyname,Name=s},mk_var(s,ty))) stys 623 val _ = log_list (log_pair (log_const_name, log_var)) nvars 624 val _ = log_thm th 625 val _ = log_command "defineConstList" 626 val k = save_dict ob 627 val _ = log_command "pop" 628 val _ = app (fn _ => log_command "hdTl") nvars 629 val _ = log_command "pop" 630 val _ = app (ignore o save_dict o OConst o #1) (rev nvars) 631 val _ = log_num k 632 val _ = log_command "ref" 633 in () end 634 | Def_tyop_prf (name,tyvars,th,aty) => let 635 val n = log_tyop_name name 636 val (ns,n) = n 637 val ns' = ns@[n] 638 val abs_name = (ns',"abs") 639 val rep_name = (ns',"rep") 640 val _ = log_name abs_name 641 val _ = log_name rep_name 642 val _ = log_list log_type_var tyvars 643 val _ = log_thm (EXISTENCE_RULE th) 644 val _ = log_command "defineTypeOp" 645 val (phi,_) = dest_comb (snd(dest_exists(concl th))) 646 val (rty,_) = dom_rng(type_of phi) 647 val a = mk_var("a",aty) 648 val r = mk_var("r",rty) 649 val absty = rty --> aty 650 val repty = aty --> rty 651 val ots = OpenTheoryMap.otname_to_string 652 val abstc = {Thy="Logging",Name=ots abs_name} 653 val reptc = {Thy="Logging",Name=ots rep_name} 654 val abs = prim_new_const abstc absty 655 val rep = prim_new_const reptc repty 656 val ra = mk_thm([],mk_ra(phi,r,rep,abs)) 657 val _ = save_dict (OThm ra) 658 val _ = log_command "pop" 659 val ar = mk_thm([],mk_ar(abs,rep,a)) 660 val _ = save_dict (OThm ar) 661 val _ = log_command "pop" 662 val _ = save_dict (OConst reptc) 663 val _ = log_command "pop" 664 val _ = save_dict (OConst abstc) 665 val _ = log_command "pop" 666 val _ = save_dict (OTypeOp name) 667 val _ = log_command "pop" 668 val pth = INST_TY_TERM ([mk_var("phi",rty-->bool)|->phi, 669 mk_var("abs",rty-->aty)|->abs, 670 mk_var("rep",aty-->rty)|->rep], 671 [alpha|->rty,beta|->aty]) Def_tyop_pth 672 val _ = log_thm (proveHyp ra (proveHyp ar pth)) 673 in () end 674 val _ = if !verbosity >= 4 then HOL_MESG("Finish proof for "^(Susp.force ths)) else () 675 (* 676 val _ = log_comment(pt^")") 677 *) 678 val _ = save_dict ob 679 (* 680 val _ = log_pair (log_list log_term, log_term) (dest_thm th) 681 val _ = log_command "pop" 682 *) 683 in () end 684 end 685in (log_term, log_thm, reset_dict, 686 set_const_name_handler, reset_const_name_handler, 687 set_tyop_name_handler, reset_tyop_name_handler) 688end 689 690val definitions = ref [] 691 692fun log_definitions () = 693 (List.app log_thm (List.rev (!definitions)); 694 definitions := []) 695 696fun export_thm th = let 697 open Thm Feedback Parse 698 val _ = case !log_state of 699 Not_logging => () 700 | Active_logging _ => let 701 val _ = log_definitions () 702 val v = !verbosity >= 1 703 val s = Susp.delay (fn () => Lib.ppstring pp_thm th) 704 val _ = if v then HOL_MESG("Start logging\n"^(Susp.force s)^"\n") else () 705 val _ = log_thm th 706 val _ = log_list log_term (hyp th) 707 val _ = log_term (concl th) 708 val _ = log_command "thm" 709 val _ = if v then HOL_MESG("Finish logging\n"^(Susp.force s)^"\n") else () 710 in () end 711 val _ = delete_proof th 712in th end 713 714fun mk_path name = OS.Path.concat(OS.FileSys.getDir(),OS.Path.joinBaseExt{base=name,ext=SOME"art"}) 715 716fun mkpair f x = (f,x) 717 718datatype OTDirective = DeleteConstant | DeleteType | SkipThm | DeleteProof 719 720fun log_some_thms axdefs th = 721 (if (case Thm.proof th of 722 Thm.Def_const_prf (thyrec, _) => 723 Lib.mem (DeleteConstant, #Name thyrec) axdefs 724 | Thm.Def_const_list_prf (_,stys,_) => 725 List.exists (Lib.C Lib.mem axdefs o mkpair DeleteConstant o #1) 726 stys 727 | Thm.Def_spec_prf (cs,_) => 728 List.exists (Lib.C Lib.mem axdefs o mkpair DeleteConstant o #1 o 729 Term.dest_const) cs 730 | Thm.Def_tyop_prf (thyrec,_,_,_) => 731 Lib.mem (DeleteType, #Tyop thyrec) axdefs 732 | _ => false) 733 then Thm.delete_proof th 734 else (); 735 definitions := th::(!definitions)) 736 737fun raw_start_logging axdefs out = 738 case !log_state of 739 Not_logging => let 740 val _ = Thm.set_definition_callback (log_some_thms axdefs) 741 val _ = log_state := Active_logging out 742 val _ = log_num 6 743 val _ = log_command "version" 744 in () end 745 | Active_logging _ => () 746 747fun read_otdfile fname = 748 let 749 val instrm = TextIO.openIn fname 750 val _ = Feedback.HOL_MESG("Reading "^fname) 751 fun recurse acc = 752 case Option.map (Substring.splitl (not o Char.isSpace) o Substring.full) (TextIO.inputLine instrm) of 753 NONE => List.rev acc 754 | SOME (d,nm) => 755 let 756 val d = Substring.string d 757 val dir = case d of 758 "deltype" => SOME DeleteType 759 | "delconst" => SOME DeleteConstant 760 | "delproof" => SOME DeleteProof 761 | "skipthm" => SOME SkipThm 762 | _ => (Feedback.HOL_WARNING "Logging" "read_otdfile" 763 ("Bad directive "^d); 764 NONE) 765 val fixnm = Substring.string o Substring.dropl Char.isSpace o Substring.trimr 1 766 in 767 recurse (case dir of NONE => acc | SOME dir => (dir,fixnm nm) :: acc) 768 end 769 in 770 recurse [] before TextIO.closeIn instrm 771 end 772 773fun start_logging nm = 774 let 775 val mungefilename = nm ^ ".otd" 776 val axiomatic_defs = read_otdfile mungefilename handle IO.Io _ => [] 777 in 778 case !log_state of 779 Not_logging => 780 let 781 val name = Theory.current_theory() 782 val path = mk_path name 783 val file = TextIO.openOut path 784 in raw_start_logging axiomatic_defs file end 785 | Active_logging _ => () 786 end 787 788fun stop_logging() = 789 case !log_state of 790 Active_logging h => let 791 val _ = log_clear () 792 val _ = TextIO.closeOut h 793 val _ = Thm.clear_definition_callback() 794 in log_state := Not_logging end 795 | Not_logging => () 796 797end 798