Re: [isabelle] Simplifying a nested if
On 23.07.2014 13:26, Holden Lee wrote:
> 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))
Instead of this rule, use the strong congruence rule for if by calling
the simplifier with "cong: if_cong".
This archive was generated by a fusion of
Pipermail (Mailman edition) and