*To*: Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] Proving relationships between locale predicates.*From*: Lars Noschinski <noschinl at in.tum.de>*Date*: Wed, 30 Nov 2011 17:58:38 +0100*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <alpine.LNX.2.00.1111291803220.4315@macbroy22.informatik.tu-muenchen.de>*References*: <4ED4E3B4.1050200@in.tum.de> <alpine.LNX.2.00.1111291803220.4315@macbroy22.informatik.tu-muenchen.de>*User-agent*: Mozilla/5.0 (X11; U; Linux x86_64; en-US; rv:1.9.2.24) Gecko/20111114 Icedove/3.1.16

On 29.11.2011 18:05, Makarius wrote:

On Tue, 29 Nov 2011, Lars Noschinski wrote:I only need one lemma from B, so I would really like to avoid instantiating A, as this takes very long (around 2.5s per instantiation).I have recently started to make some more systematic performance measurements on the locale infrastructure. So if you can point me to the sources of a concrete example like yours above, the situation might eventually improve.

--------------------------------------------------------------------- theory Scratch imports "~~/src/HOL/Probability/Probability" begin locale edge_space = fixes p :: real fixes n :: nat assumes p_prob: "0 ≤ p" "p ≤ 1" assumes n_Suc: "0 < n" context edge_space begin definition "S_verts ≡ {1..n}" definition "S_edges = S_verts × S_verts" lemma finite[simp]: "finite S_verts" "finite S_edges" and not_empty[simp]: "S_verts ≠ {}" using n_Suc by (auto simp: S_verts_def S_edges_def) end sublocale edge_space ⊆ product_finite_prob_space "(λ_. bernoulli_space p)" S_edges by default (auto simp: S_edges_def) ML_prf {* Toplevel.timing := true *} notepad begin fix n :: nat and p :: real assume A: "0 ≤ p" "p ≤ 1" "0 < n" interpret I: product_finite_prob_space "λ_. bernoulli_space p" "{1..n}" apply default apply auto done from A interpret E: edge_space p n apply unfold_locales apply auto done end --------------------------------------------------------------------- The first interpret command gives (in jedit, e903a390370c) 1.633s elapsed time, 1.596s cpu time, 0.540s GC time the second (with the minimally extended locale): 2.269s elapsed time, 2.208s cpu time, 0.708s GC time

-- Lars

**References**:**[isabelle] Proving relationships between locale predicates.***From:*Lars Noschinski

**Re: [isabelle] Proving relationships between locale predicates.***From:*Makarius

- Previous by Date: Re: [isabelle] locale import
- Previous by Thread: Re: [isabelle] Proving relationships between locale predicates.
- Next by Thread: [isabelle] locale import
- Cl-isabelle-users November 2011 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list