Email Gateway (Aug 18 2022 at 18:38): Email Gateway (Aug 18 2022 at 18:38):From: Lars Noschinski <noschinl@in.tum.de>
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 *}
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
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
Email Gateway (Aug 18 2022 at 18:47):From: Lars Noschinski <noschinl@in.tum.de>
Hi,
I've got two locales A (with predicate "A x") and B and
sublocale A <= B (f x)
holds. Now, if I have "A x", how can I show "B (f x)" without repeating
the proof for the sublocale property?
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).
-- Lars
Email Gateway (Aug 18 2022 at 18:47):From: Johannes Hölzl <hoelzl@in.tum.de>
Hi Lars,
AFAIK sublocale doesn't store the proven theorem. So the best is to
prove:
lemma (in A) B_f: "B (f x)"
...
sublocale A <= B (f x)
by (rule B_f)
and now you can use it also with:
note B_f = A.B_f[OF A x]
note B.lemma[OF B]
which is ugly, but fast.
Email Gateway (Aug 18 2022 at 18:47):From: Makarius <makarius@sketis.net>
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.
Makarius
Last updated: Apr 24 2024 at 04:17 UTC