[isabelle-dev] Order of sublocale declarations

[Amine Chaieb]

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"
   by (simp add: d_def)


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?

Thank you in advance,
Amine