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:

http://stackoverflow.com/questions/15627676/why-wont-isabelle-simplify-the-body-of-my-if-then-else-construct/

  -- Lars




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