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".

See also:

  -- Lars

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