[isabelle-dev] Fwd: Bug in Isabelle 2019/2020

[Peter Reitinger]

Hm also ich wollte nur helfen. Aber anscheinend ist dies unerwünscht...

---------- Forwarded message ---------
Von: <cl-isabelle-users-owner at lists.cam.ac.uk>
Date: Mi., 18. Nov. 2020, 08:44
Subject: Bug in Isabelle 2019/2020
To: <peter.reitinger at gmail.com>


Only subscribers may post messages to this list. If you believe that
you are a subscriber, please check that you are using the subscribed
e-mail address.




---------- Forwarded message ----------
From: Peter Reitinger <peter.reitinger at gmail.com>
To: isabelle-users at cl.cam.ac.uk
Cc:
Bcc:
Date: Wed, 18 Nov 2020 08:44:27 +0100
Subject: Bug in Isabelle 2019/2020
Hello,

I would like to report a bug in Isabelle.

The attached theory file produces unexpected behavior during the
simplification of an obviously true equation.
These are the imports:
imports Main "HOL-Word.Word"

Essentially it is as it cannot proof for a function f  that f x = f y
follows from x = y which is absolutely irritating. ;-)

I hope you can find out what is wrong here?

Best regards
Peter Reitinger

In case the bug should not repeat at your installation setup, these are the
proof states of variant a and b respectively.

a:
proof (prove)
goal (1 subgoal):
 1. to_bl (word_cat y x) = to_bl (of_bl (to_bl y @ to_bl x))
Metis: Falling back on "metis (full_types)"...
Metis: Falling back on "metis (mono_tags)"...
Failed to apply proof method⌂:
goal (1 subgoal):
 1. to_bl (word_cat y x) = to_bl (of_bl (to_bl y @ to_bl x))

b:
proof (prove)
goal (1 subgoal):
 1. to_bl (of_bl (to_bl y @ to_bl x)) = to_bl (of_bl (to_bl y @ to_bl x))

Especially proof state in b after apply (simp add:...) is extremely
confusing.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20201120/3939a84a/attachment.htm>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Show_bug.thy
Type: application/octet-stream
Size: 3205 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20201120/3939a84a/attachment.obj>