[isabelle] Simplifying a nested if



 I need to use the following kind of rule repeatedly:

lemma if_if_simp[simp]:
  "(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 ⟹
       (λx∷'e.
           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).

Thanks,
Holden



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.