Re: [isabelle] Interpretation's fact hidden for unknown reason?



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.

On Wed, 06 Feb 2013 12:39:17 +0100, Alfio Martini <alfio.martini at acm.org> wrote:

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!

On Wed, Feb 6, 2013 at 1:37 AM, Yannick Duchêne (Hibou57) <yannick_duchene at yahoo.fr> wrote:
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.


--
Yannick Duchêne




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