Re: [isabelle] Bug in Eisbach
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!
2018-06-07 16:04 GMT-04:00 Nemouchi Yakoub <y.nemouchi at gmail.com>:
> Dear all,
> **Which Eisbach functionality ?
> Eisbach matching, namely:
> (match conclusion in _" ⇒ _)
> The bug is related to matching conclusions in proof goals that comes with
> schematic variables.
> 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"
> Best wishes,
This archive was generated by a fusion of
Pipermail (Mailman edition) and