Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] case-expression and simplification

Email Gateway (Aug 18 2022 at 13:46):

From: Peter Lammich <peter.lammich@uni-muenster.de>
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

Last updated: May 03 2024 at 12:27 UTC