[isabelle] structure of a theorem



Hello,

in Isar, given a theorem, is there a way to access to the terms of its assumptions and
conclusion?

I have in mind a use like that:

-- suppose we have:

theorem t1:
  assumes po_1: "P x1"
  assumes po_n: "Q xn"
shows
  C x1 xn
end

-- can we write something like that:

theorem need_t1:
  ...
proof -
  ...
  have po_1:inv.po_1[of "a"] sorry
  moreover have po_n:inv.po_n[of "z"] sorry
  ultimately have inv.C[of "a" "z"] using t1[OF "po_1" "po_n"]
  ...
qed

thanks

Mamoun Filali
begin:vcard
fn:Mamoun FILALI-AMINE
n:FILALI-AMINE;Mamoun
adr;quoted-printable:118 Route de Narbonne;;IRIT Universit=C3=A9 Paul Sabatier;Toulouse;;31062 cedex 9;France
email;internet:filali at irit.fr
tel;work:00 33 5 61 55 69 26
tel;fax:00 33 5 61 55 68 47
version:2.1
end:vcard



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