Re: [isabelle-dev] Isabelle release
I looked for the documentation of HOL-Probability, but it looks like it is missing. It should be under HOL-Multivatiate-Analysis, but there are now further Session. Was there a change in the build-system? - Johannes On Mon, 10 Oct 2011, Makarius wrote: Dear all, the release is alreay in place, but before announcing it officially the Sydney mirror needs another round of updating, which will probably happen around midnight GMT. This gives another chance to sport drop-outs on the website. The main Isabelle repository is already in post-release mode: I have merged the release branch in Isabelle/d78ec6c10fa1. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Bayesian statistics
Hi David, as far as I know there is no such development, however Kevin Van Horn asked half a year ago a similar question: https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2011-March/msg00033.html There is already Probability theory in Isabelle/HOL: http://isabelle.in.tum.de/dist/library/HOL/HOL-Multivariate_Analysis/HOL-Probability/index.html in the next Isabelle version contains a improved version of this, mostly about infinite products and independent functions. Greetings, Johannes On Sun, 25 Sep 2011, David Blubaugh wrote: Has anyone ever developed theories with Isabelle HOL regarding Bayesian statistics ?? Thanks, David ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS - Redundant lemmas
On Wed, 21 Sep 2011, Brian Huffman wrote:
On Tue, Sep 20, 2011 at 10:03 AM, Christian Urban urb...@in.tum.de wrote:
I was able to put together replacement theorems for a few of these lemmas:
Inf_singleton ~ Inf_insert [where A={}, unfolded Inf_empty inf_top_right]
Sup_singleton ~ Sup_insert [where A={}, unfolded Sup_empty sup_bot_right]
INTER_eq_Inter_image ~ INF_def
UNION_eq_Union_image ~ SUP_def
INF_subset ~ INF_superset_mono [OF _ order_refl]
[..]
I added this information to the NEWS entry.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS - Redundant lemmas
In Java, there is a deprecated flag for such issues. Isabelle could then issue a warning whenever using a deprecated lemma --- like the legacy-warnings it already issues when using some deprecated features (recdef, etc.) You are assuming that you could flag theorems, and all tools know what these flags should actually mean, and if they use them. That's technically quite difficult to achieve. In principle we have similar flags for name space entries already, e.g. concealed. Having an official legacy status (also in the Proper IDE) is probably easy to implement, but the main work is maintaining the actual annotations in the libraries. My impression is that the traditional approach is to clear out old material quickly, so that the issue only arises in a weak sense. (In contrast, the Java standard library is famous for being strictly monotonic, where deprecated stuff is never disposed.) I think theory developers are happy with maintaining the annotations. Some theories in the distribution already contain a Legacy section (just grep for Legacy in the *.thy files), adding a deprecation flag would simplify the maintainance of this and allow us to remove them in a couple of releases. - Johannes ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: Isabelle/jEdit (19e1c6e922b6)
On Tue, 20 Sep 2011, Makarius wrote: In the meantime I have investigated this a little bit. It seems that HOL-Probability requires quite some memory even in minimalistic batch mode -- approx. 2GB on my 4GB machine. With Isabelle/jEdit one needs further 600 MB for the editor process and the same (and more) for the fully persistent document state within ML. So it adds up to something 4 GB such that it becomes infeasible to edit the full session live on a small laptop with only 4 GB. I tried to reduce the runtime requirement of HOL-Probability by removing some of the sublocale instantiations. As a lot of time is spend in locale interpretation inside proofs. For example currently I had: locale A = ... locale B = A + ... (0) locale C = A + th sublocale C B I assume replacing (0) by: locale C = B + th lemma [Pure.intros!]: C - A /\ th should fasten up locale interpretation? But how is it in the following case: locale prodA = A M1 + A M2 (1) locale prodB = B M1 + B M2 sublocale prodB prodA locale prodC = C M1 + C M2 sublocale prodC prodB locale prodD = D M1 + D M2 sublocale prodD prodA Or should this be: (2) locale prodB = prodA + B M1 + B M2 locale prodC = prodB + C M1 + C M2 locale prodD = prodC + D M1 + D M2 as a user the difference should not be visible, and I thought (1) would be slower than (2) but after updating Probability it seams like (2) is slower than (1). - Johannes ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
