# [isabelle] structure of a theorem

*To*: cl-isabelle-users at lists.cam.ac.uk
*Subject*: [isabelle] structure of a theorem
*From*: Mamoun FILALI-AMINE <filali at irit.fr>
*Date*: Thu, 26 Aug 2010 10:01:01 +0200
*Organization*: IRIT CNRS Université de Toulouse
*User-agent*: Mozilla/5.0 (Macintosh; U; Intel Mac OS X 10.6; fr; rv:1.9.1.5) Gecko/20091204 Lightning/1.0b2pre Thunderbird/3.0

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.*