Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Surprising markup for pretty-printed case expr...


view this post on Zulip Email Gateway (Aug 22 2022 at 10:55):

From: Lars Hupel <hupel@in.tum.de>
Dear list,

I have this very simple function:

fun rightUnitAppend'0 :: "'T'00 list ⇒ bool" where
"rightUnitAppend'0 (l1'00::'T'00 List.list) = (case l1'00 of [] => True
| (x'6::'T'00) # (x::'T'00 list) => rightUnitAppend'0 x)"

Now, if I look at the generated theorem:

thm rightUnitAppend'0.simps

... and hover over the "x", I get the markup

:: ?'a list
bound variable

However, the markup for "x'6" is:

:: ?'T'00.0
bound variable

Clearly, one of them is incorrect, because it should be either "?'a" or
"?'T'00.0" in both cases. This looks like a problem in the unchecking of
case expressions, because when I look at the term representation:

declare [[ML_print_depth=100]]

ML‹Thm.prop_of @{thm rightUnitAppend'0.simps}›

... all I get is "?'T'00.0", as expected. "?'a" is nowhere to be found.

Cheers
Lars

view this post on Zulip Email Gateway (Aug 22 2022 at 10:55):

From: Dmitriy Traytel <traytel@in.tum.de>
Hi Lars,

thanks for the report. Something indeed went wrong during uncheck. It
has to do with eta contracted arguments to the case combinator and shows
already at this minimized example:

term "case_list undefined (λx. f) (xs :: 't list)"

(I resist to comment on your choice of names in your example; I hope
they are automatically generated ;-) )

The uncheck phase has to eta expand before printing and picks the wrong
types from elsewhere. I have a local changeset to improve on that, which
I will test and push soon.

BTW this was a nice opportunity for me to test the newly available
ML_debugger (in the repository)---which is awesome! I could locate the
problem and (hopefully) improve the situation without inserting a single
print statement :-)

Dmitriy


Last updated: Mar 28 2024 at 12:29 UTC