Problem Description

I stumbled on this limitation/misunderstanding several times when using locales and sublocales in Isabelle. As a minimal example, let us extend the locale from the example in Section 8.4 Locales and interpretation from Code generation from Isabelle/HOL theories (by Florian Haftman et al.) to highlight the usage of sublocale(s):

lemma concat_replicate_mult:
    "concat (replicate m (concat (replicate n xs))) = concat (replicate (m*n) xs)"
  by (induction m) (simp_all add: concat_append[symmetric] replicate_add[symmetric])

locale power =
  fixes power :: "'a ⇒ 'b ⇒ 'b"
  assumes power_commute: "power x ∘ power y = power y ∘ power x"

primrec powers :: "'a list ⇒ 'b ⇒ 'b" where
  "powers [] = id"
| "powers (x # xs) = power x ∘ powers xs"

lemma powers_append: "powers (xs @ ys) = powers xs ∘ powers ys"
  by (induct xs) simp_all

lemma powers_power: "powers xs ∘ power x = power x ∘ powers xs"
  by (induct xs)
     (simp_all del: o_apply id_apply add: comp_assoc, simp del: o_apply add: o_assoc power_commute)

lemma powers_rev: "powers (rev xs) = powers xs"
  by (induct xs) (simp_all add: powers_append powers_power)

(* silly extension  *)
locale plist =
  fixes to_nat :: "'a ⇒ nat"

definition "pow a b = concat (replicate (to_nat a) b)"

sublocale power: power "pow"
  by standard (auto simp: pow_def concat_replicate_mult mult.commute) 



Following the document, we can get codegeneration like so:

global_interpretation ex: plist id
  defines pows = ex.power.powers.

value "ex.powers.powers [0..<10] [0..<10]" (* Undefined constant: "ex.powers.powers" *)
value "pows [1..<3] [0..<7]"               (* succeeds *)
thm ex.power.powers_power                  (* pows ?xs ∘ (ex.pow ∘ id) ?x = (ex.pow ∘ id) ?x ∘ pows ?xs *)
thm pows_def                               (* pows ≡ power.powers (ex.pow ∘ id) *)

However, now the theorem ex.power.powers_power contains ex.pow and we would want to use ex.power.powers_power[unfolded ex.pow_def] instead. Trying to rewrite it by using a second defines with pow = ex.pow will leave us with no code equations:

global_interpretation ex: plist id
  defines pows = ex.power.powers and pow = ex.pow.

value "ex.powers.powers [0..<10] [0..<10]" (* Undefined constant: "ex.powers.powers" *)
value "pows [1..<3] [0..<7]"               (* No code equations for pows *)

We could also do something like so:

interpretation ex: plist id.

definition "pows = ex.power.powers"

value "pows [1..<3] [0..<7]"  (* No code equations for power.powers, plist.pow *)

lemmas [code] = pows_def[unfolded ex.power.powers_def ex.pow_def]

value "pows [1..<3] [0..<7]"  (* succeeds *)
thm ex.power.powers_power     (* ex.power.powers ?xs ∘ (ex.pow ∘ id) ?x = (ex.pow ∘ id) ?x ∘ ex.power.powers ?xs *)

However, the issue is the same. We duplicated a constant for which codegeneration works but we will need to rewrite the theorems or constant.


For many constants and multiple nested (sub-)locales this process is a bit confusing. How do I organise my code with locales in a way that interfaces nicely with codegeneration?

For example, is there a way to automate the defines steps and rewrites the theorems?



Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.