Re: [isabelle-dev] Code generation in Isabelle
Lukas already assured me of that. No worries here. - Steven On 22.07.2011, at 00:07, Alexander Krauss wrote: On 07/21/2011 04:25 PM, Steven Obua wrote: Actually, there is a third code generator hidden somewhere in Isabelle. If you are talking about what I know under the name Compute Oracle, then rest assured that it is hidden well enough that the chance of some user accidentially confusing it with the mainstream code generator is negligible. Interested parties can discover it using grep, of course. Alex ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Isabelle/HOL axiom ext is redundant
Anyway, since eq_reflection actually *is* an axiom, and (=) actually *does* mean the same thing as (==), then I really don't see any reason why we need to have both (or separate bool and prop types, for that matter). I don't know of any other HOL provers that do. Even if we got rid of the bool/prop and (=)/(==) distinctions, we still have the meta-meta-logic as a natural deduction framework: The hyps component of theorems encodes the is derivable from relation, and free variables in theorems encode the this derivation can be done uniformly for all x property. I have never understood why Isabelle needs multiple levels of meta-logics. I agree, these multiple levels are unfortunate ... But I think it is too late to change this now, as frameworks like Isar and many other packages rely on them. In a new theorem prover built from scratch (but of course based on many years of Isabelle experience...) this would be one of the lessons learnt ;-) Steven PS: Now that the Google App Engine is here (with support for Java (that means, also Scala - Makarius)), wouldn't it be great to make this new theorem prover a native of the cloud? - Brian ___ Isabelle-dev mailing list Isabelle-dev at mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev -- next part -- An HTML attachment was scrubbed... URL: https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20091112/66863895/attachment.htm
[isabelle-dev] Isabelle/HOL axiom ext is redundant
In the translation to ZF which Andy and I am developing, such strange proofs actually caused some weird problems at some point. This sounds interesting :-) Is there more information on this translation available? Best, Steven PS: For those of you who a) speak German b) play Skat c) have an iPhone / iPod touch: http://74.207.244.176/pubstatic/onlineskat -- next part -- An HTML attachment was scrubbed... URL: https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/2009/b168d2c1/attachment.htm
[isabelle-dev] Numeral simplification: neg and iszero
NatBin.thy is now nearly neg-free, but there are still some other places with lemmas that use neg. For example, Tools/ ComputeNumeral.thy seems to be a complete re-implementation of the simpset defined in NatBin.thy for arithmetic at type nat. If such other lemmas involving neg can be made redundant, or merged into NatBin.thy, then we will be able to remove neg. The rules in Tools/ComputeNumeral.thy are used within ML code for the HOL computing oracle. It's true, they are basically a cleaned up version of the NatBin.thy rules; simplification with these rules is supposed to work together with the oracle, not necessarily with the simplifier. Changes here might break my part of the proof of the Kepler Conjecture; but chances are it does not run with the current version of Isabelle anyway :-) Steven
[isabelle-dev] Clojure
I just came across this great new language for the Java VM, Clojure. It is like somebody read my mind about how a modern programming language should be, melted the vague ideas there into a detailed specification, put a lot of other goodies like STM in there, and finally implemented it! I recommend the talk (slides + audio, about 2 hours) by Clojure inventor Rich Hickey here: http://lispnyc.org/wiki.clp?page=past-meetings There is also a slightly more recent talk, where the focus is mostly on concurrency: http://clojure.blip.tv/#819147 And there is lots of info on the closure page (although you probably should be a little bit familiar with LISP; a nice tutorial from the ground up is missing): closure.sourceforge.net Enjoy!, Steven
