On Sun, 5 Aug 2012, Rob Arthan wrote: >> I've often wanted Isabelle locales. Are you going to code them in >> HOL4? > > Locales are one of the many things that (I believe) make the Isabelle > HOL logic much more bloated than the original and best HOL logic as > supported by HOL4, HOL Light, HOL Zero and ProofPower. It might be > possible to give a similar facility as a bolt-on outside the logic.
Locales are not even part of Isabelle/HOL, but of Isabelle/Pure, where they are added as an infrastructure outside the logic. (Most of Isabelle/Pure is just infrastructure in some sense.) Historically it were the Coq guys who made their "sections" part of the core logic, and regretted it ever after. Today they follow a more HOL-ish approach: Coq type classes are merely some infrastructure around the logic. More historically, Isabelle type classes were done the other way round: as some kind of kernel extension of Isabelle/Pure, but we also regretted that. In recent years we have moved more and more towards rephrasing (and rebasing) type classes in terms of locales, and thus outside the logic. This is still not fully achieved. Anyway, I've asked myself the same question above, when some HOL person will start to implement a version of "sections" or "locales". My estimate is that when starting today, it would take approx. 5 years to make this become real. Our very first version of Isabelle locales can be seen here (14 years ago): http://isabelle.in.tum.de/repos/isabelle/file/5313f781efe0/src/Pure/locale.ML 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 hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
