Email Gateway (Aug 19 2022 at 10:24): Email Gateway (Aug 19 2022 at 10:24):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
Hi all,
I don't understand why in the following (simple and stupid) sample case,
the P fact from the second interpretation, is not visible:
locale L = fixes A assumes P: "A = A"
thm L.P
interpretation I1: L A by (unfold L_def, rule refl)
thm I1.P
interpretation I2: L A by (unfold L_def, rule refl)
thm I2.P
At “thm I2.P” the ouput pan says “Unknown fact I2.P”. If I move I2 before
I1, then I2.P becomes visible and I1.P is hidden.
Note: it occurs with Isabelle RC2.
Is this normal behaviour? If yes, then I must be miss‑understanding
something.
Email Gateway (Aug 19 2022 at 10:25):From: Alfio Martini <alfio.martini@acm.org>
Hi Yannick,
I have also the same doubt with respect to the same situation. In a
more complex setting, I usually
like to try several different proofs for the same locale interpretation and
because of the situation mentioned below I find that I can not do it.
best!
Email Gateway (Aug 19 2022 at 10:27):From: Yannick <yannick_duchene@yahoo.fr>
One may also not only enjoy different proofs, but need different proofs.
May be a workaround is to move each interpretation in its own theory file,
but that may lead to other issues (I did not try).
We will have to wait to know if it's on purpose or not.
Email Gateway (Aug 19 2022 at 10:27):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
I just tried this, base on the same sample case:
theory TL
imports HOL
begin
locale L = fixes A assumes P: "A = A"
thm L.P
end
theory TI1
imports TL
begin
interpretation I1: L A by (unfold L_def, rule refl)
thm I1.P
end
theory TI2
imports TL
begin
interpretation I2: L A by (unfold L_def, rule refl)
thm I2.P
end
As‑is, I1.P and I2.P are both visible, but still cannot see both at the
same time. If in theory “TI2”, I change “imports TL” into “imports TI1”,
then the same issue occurs, “I2.P” is not visible.
Using separate theories allows to have both, but still not simultaneously.
Email Gateway (Aug 19 2022 at 10:28):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
The interpretation command only generates declarations for instances
that have not been subsumed by previous interpretations. In the running
example, both interpretations yield syntactically identical theorems
I1.P and I2.P. So, only one of them is actually needed, and
interpretation does not generate the second at all. This behaviour
allows to detect and handle certain cycles in the sublocale hierarchy.
If you insist on getting both interpretations simultaneously, you have
to move the interpretations to different theories and merge later. In
the example below, add
theory TI imports TI1 TI2 begin
thm I1.P
thm I2.P
Andreas
Last updated: Apr 30 2024 at 12:28 UTC