I forgot who wrote this >>>> One way to ameliorate this problem is to compose proofs lazily.
but anyway: Doesn't the Isabelle kernel now have a feature that you can "postpone" proving a thm and still already being allowed to use it? I think Makarius put that in the kernel especially to be able to parallelize Isabelle proof checking on multi-core machines? Can someone confirm or deny this, and give some details? My memory of the talk by Makarius in which he described this (I think I heard it twice :-)) is a bit hazy. I can imagine adding something similar in HOL Light. But I can also imagine just using "ASSUME" of the thing you plan to prove later (so any thm that uses it will get it explicitly in the assumption list), and then once you have proved it, explicitly discharging it with something like: fun th1 th2 -> let tm = concl th2 in MP (DISCH tm th1) th2 I guess this function already is in HOL Light, but I don't know its name. Anyone? To comfortably work in a style like this you probably would want to change the thm printer though, or else you would go crazy by all the assumptions. Freek ------------------------------------------------------------------------------ Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
