# Re: [isabelle] Proving relationships between locale predicates.

```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.
```
```
```
I get this when interpreting stuff from probability theory, which has a elaborate locale hierarchy. Some small example:
```
---------------------------------------------------------------------
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 *}

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

```
I do not really use it, but using interpretation on the toplevel seems to be a lot slower then interpret in a proof (3.5 to 3.8s).
```
-- Lars

```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.