# [isabelle-dev] Order of sublocale declarations

Amine Chaieb amine at chaieb.org
Thu Jan 31 12:48:20 CET 2013

```Hi,

I came across a situation where the order of sublocale declarations
makes a difference in the theory development, which in this case is not
clear to me. Can anyone please clarify the following behaviour within
the simplified case below? Is the behaviour due to purely technical
reasons or is there a deeper sense?

The theory basically defines two locales A and B, which are equivalent
when the parameter is transformed. Within locale A I have an
abbreviation depending on a local fixed parameter. Suppose I have proved
several interesting lemmas for locale A and would like to transfer them
to locale B and vice vesa. The order in which the sublocale declarations
between A and B appear indeed matters (in the form of the presence of an
error related to duplicating the abbreviation declaration)

theory Test
imports Main
begin

fun iter:: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> ('a
\<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
"iter 0 f0 f = f0"
| "iter (Suc n) f0 f = (\<lambda>x. f (iter n f0 f x) x)"

locale A = fixes f:: "int \<Rightarrow> int \<Rightarrow> int"
assumes "\<And> a. f a 1 = a "
begin

abbreviation fpower:: "int \<Rightarrow> nat \<Rightarrow> int" (infixr
"^f" 80) where
"fpower x n == iter n (\<lambda>x. f 0 1) f x"
end

locale B  = fixes g :: "int \<Rightarrow> int \<Rightarrow> int"
assumes "\<And> a. g a 0 = a"

definition d:: "(int \<Rightarrow> int \<Rightarrow> int) \<Rightarrow>
(int \<Rightarrow> int \<Rightarrow> int)"
where "d f = (\<lambda> a b. 1 - f (1 - a) (1 - b))"

lemma dd[simp]: "d (d f) = f"

lemma AB_iff[simp]: "B (d f) = A f"
apply (auto simp add: A_def B_def d_def)
apply (erule_tac x="1 -a" in allE)
apply simp
done

lemma BA_iff[simp]: "A (d g) = B g"
using AB_iff[where f = "d g"]
by simp

---

Since A and B are equivalent I introduce a "transitional" locale for A,
to avoid infinite sublocale relationship

locale AB = A

Now to sublocale: In this order:

sublocale B < A "d g"
unfolding BA_iff ..

sublocale AB < B "d f"
unfolding AB_iff ..

I get an error at the second sublocale declaration:

*** Duplicate constant declaration "local.fpower" vs. "local.fpower"
(line 13 of "/home/ac/tmp/Test.thy")
*** At command "sublocale" (line 43 of "/home/ac/tmp/Test.thy")

In this order however, everything works fine:

sublocale AB < B "d f"
unfolding AB_iff ..

sublocale B < A "d g"
unfolding BA_iff ..

Is there a reason I am missing?