Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Option case and pairs with the function package

Email Gateway (Aug 18 2022 at 11:52):

From: Alexander Krauss <krauss@in.tum.de>
Andreas,

I stumbled across a syntax problem for the option_case expressions:

[...]
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.

This is because the function package eta-normalizes the right hand
sides, which breaks the case syntax. Currently there is no easy fix for
this, unfortunately.

Alex

Email Gateway (Aug 18 2022 at 11:57):

From: Andreas Lochbihler <lochbihl@ipd.info.uni-karlsruhe.de>
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

Last updated: Nov 21 2024 at 12:39 UTC