On Thu, 19 Jul 2012, Freek Wiedijk wrote: > 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?
Yes, this concept is called "proof promise". See page 5 of my PLMMS 2009 paper http://www4.in.tum.de/~wenzelm/papers/parallel-isabelle.pdf Note that at the bottom right of page 5, the two main kernel rules (promise) and (fulfill) have been simplified later: \Pi_2 is required to be empty (all pending promises already fulfilled) and the \Pi_2 << a check becomes obsolete --- it would be hard to implement anyway. Moreover note that the idea to fork proofs in one context and join later in another context hinges on the \Theta_2 <= \Theta_1 test of (fulfill). This works in Isabelle thanks to theory certificates that were introduced by Larry in the 1990-ies, and refined by myself over the years. HOL4 and HOL-Light lack that concept. (John Harrison keeps asking me every 10 years what is its purpose :-) Proof promises are used for parallel proof checking, but the basic concept is independent of all that: a promise acts like a polymorphic proof constant that can be replaced later on, by substituting with its "definition". This is like an implicit let-redex within the conceptual proof term language -- LCF systems usually omit that structure in memory. Contrast promises with oracles, which are polymorphic contants that are postulated but never replaced ("implemented"). Cf. 'sorry' in Isabelle. Contrast promises also with ASSUME, which is like a non-polymorphic lambda over the proof; it also tends to get in the way of other tools, not just the pretty printer. Cf. "Shallow lazy proofs" at TPHOLs 2005. My general plan is to make more aggressive use for proof promises in the Isabelle/PIDE interaction model, not just to improve parallelism, but do get top-down development by default without the user having to say 'sorry' all the time. Makarius ------------------------------------------------------------------------------ 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
