Hm also ich wollte nur helfen. Aber anscheinend ist dies unerwünscht... ---------- Forwarded message --------- Von: <[email protected]> Date: Mi., 18. Nov. 2020, 08:44 Subject: Bug in Isabelle 2019/2020 To: <[email protected]>
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 <[email protected]> To: [email protected] 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.
Show_bug.thy
Description: Binary data
_______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
