[isabelle] Simplifying a nested if · Archive Mirror: Isabelle Users Mailing List

Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Simplifying a nested if

Email Gateway (Aug 19 2022 at 15:02):

From: Holden Lee <hl422@cam.ac.uk>
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

Email Gateway (Aug 19 2022 at 15:02):

From: Lars Noschinski <noschinl@in.tum.de>
Instead of this rule, use the strong congruence rule for if by calling
the simplifier with "cong: if_cong".