On Thu, Jul 19, 2012 at 9:54 AM, Freek Wiedijk <[email protected]> wrote: > I forgot who wrote this > >>>>> One way to ameliorate this problem is to compose proofs lazily.
That was me. > > 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 confirm that I have also heard this. Don't know the details, though. > > 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? In HOL4 that is called PROVE_HYP. > > 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. In HOL4 you can control how much assumptions are printed with a trace called "assumptions", but even the lowest setting still prints them as dots, I think. But that would be easy to change. > > 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
