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
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
