Why is the simplifier not able to discharge the following goal:
⟦(λxa. if xa ∈ V⇘K⇙ then ⇘x⇙⇩V (⇘r⇙⇩V xa) else undefined) = (λx. if x ∈ V⇘K⇙ then ⇘y⇙⇩V (⇘d⇙⇩V x) else undefined); v ∈ V⇘K⇙⟧ ⟹ ⇘x⇙⇩V (⇘r⇙⇩V v) = ⇘y⇙⇩V (⇘d⇙⇩V v)
It follows directly from the fact that
v ∈ V⇘K⇙.
Thank you for a hint
Because of the lambdas. Maybe
(simp add: fun_eq_iff) works. But in general forall is better than lambdas.
meson solve the goal.
To solve it using simp, add both
if_split to the simpset.
Don't add if_split to the simpset, use
simp add: fun_eq_iff split: if_splits
Yes, that's much better :)
Robert Soeldner has marked this topic as resolved.
Last updated: Sep 25 2022 at 22:23 UTC