Stream: Beginner Questions

Topic: apply case_tac to ∀x.


view this post on Zulip Isaac Freund (Oct 01 2022 at 09:16):

Hello, I have a subgoal containing a ∀x::Foo. ... expression and know that Foo only has one possible value. In the past I've used apply(case_tac x) to handle a similar situation, but it seems that does not work with ∀x::Foo. ..., only with ⋀x::Foo. ....

view this post on Zulip Isaac Freund (Oct 01 2022 at 09:17):

Is there a way to convert ∀x::Foo. ... to ⋀x::Foo. ... or otherwise cleanly solve this?

view this post on Zulip Jan van Brügge (Oct 01 2022 at 09:52):

you can use rule allI to get rid of the HOL forall

view this post on Zulip Wolfgang Jeltsch (Oct 01 2022 at 13:31):

Also, if possible, use cases instead of case_tac, as the former is more high-level than the latter.


Last updated: Mar 29 2024 at 04:18 UTC