Re: [isabelle] Interpretation's fact hidden for unknown reason?
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
On 02/06/2013 10:17 PM, Yannick Duchêne (Hibou57) wrote:
Le Wed, 06 Feb 2013 20:22:01 +0100, Yannick <yannick_duchene at yahoo.fr> a
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).
I just tried this, base on the same sample case:
locale L = fixes A assumes P: "A = A"
interpretation I1: L A by (unfold L_def, rule refl)
interpretation I2: L A by (unfold L_def, rule refl)
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and