[isabelle] case-expression and simplification



Hi,

is there any deeper reason why abbreviations do not work with "case _
of" - expressions?
On the other side, they work well with case-splitting in the
function-package.

datatype test = A "nat list" | B
abbreviation "As n == A [n]"
fun f where "f (As n) = True" | "f _ = False" (* Works well! *)
lemma "(case x of As n => n | _ => 0) = 0" (* Does not work! *)



Regards,
  Peter





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