[isabelle-dev] Order of sublocale declarations

[Andreas Lochbihler]

Hi Amine,

the error message in the second case is only delayed: You get it, once 
you open the AB context again (context AB begin). In the first case, it 
shows up immediately, because the sublocale command already constructs 
the context AB enriched with B.

Best,
Andreas

On 01/31/2013 12:48 PM, Amine Chaieb wrote:
> 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
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev