[isabelle] Bug in Eisbach



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.