[isabelle] obtains and is-bindings


when I declare an shorthand via (is "?A") in an obtain statement, the shorthand only becomes bound after the proof has been completed. Why is this? For ordinary have and show, I can use such shortcuts inside the proof. Is this different behaviour intended?

Here's an example:

notepad begin
  fix f :: "'a => 'b"
  obtain x y where "f x = y" (is "?A x y")
    (* term "?A"  fails *)
  proof -
    (* term "?A" fails *)
    show thesis sorry
  term ?A (* works *)

  have "f x = y" (is "?A x y")
  proof	-
    term "?A" (* works *)
    show ?thesis sorry


Karlsruher Institut für Technologie
IPD Snelting

Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Adenauerring 20a, Geb. 50.41, Raum 031
76131 Karlsruhe

Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at kit.edu
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum in der Helmholtz-Gemeinschaft

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