Stream: General

Topic: Replace higher-order premise


view this post on Zulip Jan van Brügge (Dec 30 2021 at 16:15):

I have a theorem in the form (⋀a b. a ∈ f <image> A ⟹ b ∈ B ⟹ ?g a b = ?h a b) ⟹ P2 ⟹ P3 ⟹ Q. To prove the premise, I need to rewrite it slightly (remove the set image): (⋀x b. x ∈ A ⟹ b ∈ B ⟹ ?g (f x) b = ?h (f x) b) ⟹ P2 ⟹ P3 ⟹ Q. A lemma that takes the original premise and produces the new one is easy to write and can be proven by blast, but I can't apply it because OF tries unify the Q only and not replace the whole higher order premise

view this post on Zulip Jan van Brügge (Dec 30 2021 at 16:16):

<image> above means ` but that confuses the markdown parser of zulip

view this post on Zulip Jan van Brügge (Dec 30 2021 at 16:17):

Is there a way to rewrite the theorem accordingly? I ultimately want to do this from ML, if that helps

view this post on Zulip Wolfgang Jeltsch (Dec 30 2021 at 17:11):

Perhaps you could apply the atomize method or more specifically use [unfolded atomize_imp] with the premise to (temporarily) replace the Pure implication by the HOL implication.


Last updated: Mar 28 2024 at 08:18 UTC