Re: [isabelle] Bug in Eisbach



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.