[isabelle] Option case and pairs with the function package



Hi all,

I stumbled across a syntax problem for the option_case expressions:

When I define a function with the definition keyword, say

definition syntaxtest :: "('x => bool) Þ ('x * ('l => nat)) option => bool" where "syntaxtest f s = (case s of None Þ True | Some (a, b) => f a & (b = (\<lambda>l. 0)))"


and then display syntaxtest_def, I get as expected:

syntaxtest f s = (case s of None Þ True | Some (a, b) => f a & (b = (\<lambda>l. 0)))


However, when I use the function package, when I want to show syntaxtest'.simps, not (case s of None ...) is displayed, but option_case ... s.

fun syntaxtest' :: "('x => bool) Þ ('x * ('l => nat)) option => bool" where
"syntaxtest' f s = (case s of None Þ True | Some (a, b) => f a Ù (b = (\<lambda>l. 0)))"

syntaxtest' ?f ?s =
option_case True (prod_case (\<lambda>a b. ?f a & b = (\<lambda>l. 0))) ?s

Is there a way to use the function package and have the normal case syntax being displayed?

Andreas





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