Jan van Brügge (Dec 30 2021 at 16:15): 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
Jan van Brügge (Dec 30 2021 at 16:16):<image> above means ` but that confuses the markdown parser of 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
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: Dec 21 2024 at 12:33 UTC