Email Gateway (Aug 18 2022 at 15:54): Email Gateway (Aug 18 2022 at 15:54):From: Mamoun FILALI-AMINE <filali@irit.fr>
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
filali.vcf
Email Gateway (Aug 18 2022 at 15:54):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Mamoun,
short answer: no there isn't such.
Maybe, I guess, you have some proofs and want to find ways to organize
them in a nice fashion -- there are a couple of such organization
principles possible in Isar, but from your toy example it is impossible
to glimpse what could be helpful for you. So, if you like, just post
more context on here and maybe we can find a device for the problem you
actually want to solve.
Cheers,
Florian
signature.asc
Last updated: Apr 26 2024 at 20:16 UTC