Re: [isabelle] Bug in Eisbach



Hi Yakoub,

Eisbach's match does not like schematic variables in goal states much. match works similar to the subgoal command, which turns all schematic variables into goal parameters, i.e., they cannot be instantiated afterwards any more. This is by design because it removes the interdependency between different goals and therefore allows for parallel proof processing. If you want to work with goals with schematics in them, don't use match or subgoal.

Best,
Andreas

On 07/06/18 23:26, Nemouchi Yakoub wrote:
Hi again,

I just figure out it has nothing to do with schematic variables.

However, the bug is even worst. Namely:

1) apply ((match conclusion
           in "⦃_⦄_⦃_⦄"  ⇒ ‹succeed›), rule H)

2)apply ((match conclusion
           in "⦃_⦄_⦃_⦄"  ⇒ ‹ rule H ›) )

(1) Here (1) works fine and (2) does NOT work!

For me (1) and (2) should always behave the same!

Best wishes,

Yakoub.



2018-06-07 16:04 GMT-04:00 Nemouchi Yakoub <y.nemouchi at gmail.com>:

Dear all,

***Description:

**Which Eisbach functionality ?
    Eisbach matching, namely:

    (match conclusion  in _"  ⇒ _)

The bug is related to matching conclusions in proof goals that comes with
schematic variables.

**Example:

If the conclusion of the proof goal is of the form ⦃?ps5⦄_⦃_⦄ then:
   apply (match conclusion  in ⦃?ps5⦄_⦃_⦄ "  ⇒ succeed) -->This WORKS FINE

However,  If the conclusion of the proof goal is of the form ⦃ ?ps2.5 ⦄_
⦃_⦄ or   ⦃ ?p⇩5 ⦄_⦃_⦄  then:

  apply (match conclusion  in ⦃ ?ps2.5 ⦄_⦃_⦄ "  ⇒ succeed)   -->
      This WILL NOT WORK because of   ?ps2.5

  apply (match conclusion  in ⦃ ?p⇩5  ⦄_⦃_⦄ "  ⇒ succeed)
  This WILL NOT WORK because of    ?p⇩5

In Other words If you have a schematic variable coming from a "fact" that
uses a free variable with
an underscore like " p⇩5 " or the "fact" uses a free variable followed by
a numeral like " p5 ", Eisbach will not manage to
match it. This is because of the generated schematic variable by Isabelle
after using the "fact" will have the form " ?p⇩5 " and  "?p2.5"
respectively.

Best wishes,

Yakoub.






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