[isabelle] Simplifying a nested if
I need to use the following kind of rule repeatedly:
"(if (x∈S) then (f x (if x∈S then g x else h x)) else (i x)) =
(if (x∈S) then (f x (g x)) else (i x))"
by (metis (mono_tags))
However, this is not working automatically (I suspect because the pattern
matching isn't powerful enough to work on functions?).
For example, the following goal should be solved (and can be solved with *apply
(auto simp add: if_if_simp[where S="S" and f="λx y. f x ⊕⇘K⇙ y"])*)
⋀f∷'e ⇒ 'a.
f ∈ S →⇩E carrier K ⟹
module K V ⟹
field K ⟹
if x ∈ S
then f x ⊕⇘K⇙ (if x ∈ S then ⊖⇘K⇙ f x else undefined)
else undefined) =
(λx∷'e. if x ∈ S then 𝟬⇘K⇙ else undefined)
Is there a way to simplify using if_if_simp in a more automatic fashion?
While metis works on the lemma it doesn't work here (probably because of
the presence of too many other terms).
This archive was generated by a fusion of
Pipermail (Mailman edition) and