Stream: General

Topic: Thm.assume: undeclared hyps

Lukas Stevens (Jul 20 2020 at 14:54):

I want to construct a thm using a natural deduction proof. The theorem involves conjE which means that I use Thm.assume to construct thms with open assumptions that are closed when using conjE. Unfortunately, this apparently violates Isabelle conventions (see https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2016-August/015534.html), because I get an undeclared hyps when writing done after resolving with the theorem. From the mailing list thread alone, I don't really see what I should do instead. Does anybody know what the canonical way is to construct such a proof?

Josh Chen (Jul 20 2020 at 14:58):

Can you elaborate? It's unclear to me what setting you're in. ML? HOL?

Josh Chen (Jul 20 2020 at 15:00):

Or post a link to the theory?

Lukas Stevens (Jul 20 2020 at 15:06):

I am constructing the theorem with ML. I will try to come up with a minimal example

Lukas Stevens (Jul 20 2020 at 16:09):

Hm, it is not that easy to condense what I have. In the meantime, I tried to use Thm.assume_hyps instead of Thm.assume but no luck.

Lukas Stevens (Jul 20 2020 at 16:32):

It appears to be that I was using Thm.assume incorrectly (I did not close some assumptions).

Manuel Eberl (Jul 22 2020 at 17:16):

Thm.assume is a pretty low-level tool. You have to be careful to actually add these to the assumptions eventually using Thm.implies_intr. I think the more modern approach (that I don't know much about) is using contexts that have these as local assumptions. (In Isar you would write context assumes … begin)

Manuel Eberl (Jul 22 2020 at 17:17):

When you do Thm.assume ct, you get ct as a theorem, but with the pending hypothesis ct. All other theorems you create based on this one will also have ct as a hypothesis. It is only discharged when you do Thm.implies_intr eventually.

Lukas Stevens (Jul 23 2020 at 09:15):

Yeah, I know that. But I really need a natural deduction proof in my case since I am replaying proof terms that some ML code generates.

Lukas Stevens (Jul 23 2020 at 09:23):

Or at least I believe that I need that :P

Last updated: Dec 21 2024 at 12:33 UTC