Code generation from Locales and Sublocales in Isabelle

Question

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"
begin

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)
end

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

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) 

end

---

Experiments

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.

---

Question

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?