[isabelle] obtains and is-bindings



Hi,

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
  qed
  term ?A (* works *)

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

Andreas

--
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
http://pp.info.uni-karlsruhe.de
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.