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

thm I1.P
thm I2.P

Andreas


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
écrit:

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:

     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.







This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.