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

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)


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

  from A interpret E: edge_space p n
    apply unfold_locales
    apply auto



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.