<div dir="auto">Hm also ich wollte nur helfen. Aber anscheinend ist dies unerwünscht...</div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">---------- Forwarded message ---------<br>Von: <span dir="auto"><<a href="mailto:cl-isabelle-users-owner@lists.cam.ac.uk">cl-isabelle-users-owner@lists.cam.ac.uk</a>></span><br>Date: Mi., 18. Nov. 2020, 08:44<br>Subject: Bug in Isabelle 2019/2020<br>To:  <<a href="mailto:peter.reitinger@gmail.com">peter.reitinger@gmail.com</a>><br></div><br><br>Only subscribers may post messages to this list. If you believe that<br>
you are a subscriber, please check that you are using the subscribed<br>
e-mail address.<br>
<br>
<br><br><br>---------- Forwarded message ----------<br>From: Peter Reitinger <<a href="mailto:peter.reitinger@gmail.com" target="_blank" rel="noreferrer">peter.reitinger@gmail.com</a>><br>To: <a href="mailto:isabelle-users@cl.cam.ac.uk" target="_blank" rel="noreferrer">isabelle-users@cl.cam.ac.uk</a><br>Cc: <br>Bcc: <br>Date: Wed, 18 Nov 2020 08:44:27 +0100<br>Subject: Bug in Isabelle 2019/2020<br><div dir="ltr"><div>Hello,</div><div><br></div><div>I would like to report a bug in Isabelle.</div><div><br></div><div>The attached theory file produces unexpected behavior during the simplification of an obviously true equation.</div><div>These are the imports:</div><div>imports Main "HOL-Word.Word"</div><div><br></div><div>Essentially it is as it cannot proof for a function f  that f x = f y follows from x = y which is absolutely irritating. ;-)</div><div><br></div><div>I hope you can find out what is wrong here?</div><div><br></div><div>Best regards</div><div>Peter Reitinger</div><div><br></div><div>In case the bug should not repeat at your installation setup, these are the proof states of variant a and b respectively.</div><div><br></div><div>a:</div><div>proof (prove)<br>goal (1 subgoal):<br> 1. to_bl (word_cat y x) = to_bl (of_bl (to_bl y @ to_bl x)) <br>Metis: Falling back on "metis (full_types)"... <br>Metis: Falling back on "metis (mono_tags)"... <br>Failed to apply proof method⌂:<br>goal (1 subgoal):<br> 1. to_bl (word_cat y x) = to_bl (of_bl (to_bl y @ to_bl x))</div><div><br></div><div>b:</div><div>proof (prove)<br>goal (1 subgoal):<br> 1. to_bl (of_bl (to_bl y @ to_bl x)) = to_bl (of_bl (to_bl y @ to_bl x))</div><div><br></div><div>Especially proof state in b after apply (simp add:...) is extremely confusing.<br></div></div>
</div>