Email Gateway (Aug 22 2022 at 18:34): Email Gateway (Aug 22 2022 at 18:34):From: Cezary Kaliszyk <cezarykaliszyk@gmail.com>
Dear Isabelle list,
Consider the following complete correct theory that Isabelle 2018 accepts:
theory bla imports Complex_Main "~~/src/HOL/Eisbach/Eisbach" begin
lemma "a ⟹ a ⟶ b ∧ c ⟹ b ∧ c" proof -
assume "a" "a ⟶ b ∧ c"
thus "b ∧ c" by simp
qed
If I only reorder the imports:
theory bla imports "~~/src/HOL/Eisbach/Eisbach" Complex_Main begin
The simp call fails with the error: "Failed to apply initial proof method⌂:..."
The obvious workaround it to randomly reshuffle my (longer) list of
imports until the simplifier works as expected, but would I rather
understand the issue.
Regards,
Cezary
Email Gateway (Aug 22 2022 at 18:34):From: Lars Hupel <hupel@in.tum.de>
Dear Cezary,
theory bla imports Complex_Main "~~/src/HOL/Eisbach/Eisbach" begin
despite what the location of Eisbach in HOL suggests, Eisbach actually
imports Pure, not Main. The problem can be reduced to that. I had a
similar issue last year:
<https://github.com/larsrh/libisabelle/issues/61>
The problem, as far as I can recall it, is that you'll get "Pure.simp"
instead of "HOL.simp".
Cheers
Lars
Email Gateway (Aug 22 2022 at 18:34):From: Cezary Kaliszyk <cezarykaliszyk@gmail.com>
Thanks for the answer - this makes it mostly clear.
But maybe one more clarification: If HOL relies on Pure, why is it at
all possible to get the Pure-simp and not HOL-simp?
cheers,
Cezary
Email Gateway (Aug 22 2022 at 18:34):From: Makarius <makarius@sketis.net>
The Prover IDE shows you which "simp" method you get: it is HOL.simp in
both cases.
The problem encountered here is a bad merge of the initial simplifier
configuration (see HOL_basic_ss). It contains machinery that can only be
defined once and not merged: the merge will pick the left branch and
ignore the right branch.
That conforms to the general merge policy to prefer the left sub-graph.
Makarius
Email Gateway (Aug 22 2022 at 18:34):From: Makarius <makarius@sketis.net>
On 06/10/18 05:58, Cezary Kaliszyk wrote:
Consider the following complete correct theory that Isabelle 2018 accepts:
theory bla imports Complex_Main "~~/src/HOL/Eisbach/Eisbach" begin
Some side-remarks.
The theory import should be "HOL-Eisbach.Eisbach", see the following
important NEWS entries.
"""
New in Isabelle2018 (August 2018)
* General *
New in Isabelle2017 (October 2017)
* General *
In order to import theories from other sessions, the ROOT file format
provides a new 'sessions' keyword. In contrast, a theory that is
imported in the old-fashioned manner via an explicit file-system path
belongs to the current session, and might cause theory name conflicts
later on. Theories that are imported from other sessions are excluded
from the current session document. The command-line tool "isabelle
imports" helps to update theory imports.
"""
lemma "a ⟹ a ⟶ b ∧ c ⟹ b ∧ c" proof -
assume "a" "a ⟶ b ∧ c"
thus "b ∧ c" by simp
qed
Isar commands 'hence' and 'thus' are merely historic: they came from
Mizar into John Harrison's Mizar mode. In very early Isar versions
(approx. 1998) I merely copied them from there. Later I refined the Isar
language quite a lot (2001/2002, 2015/2016) without reconsidering this
legacy: proofs become shorter and more maintainable by not using
'hence' and 'thus' anymore. (That is the standard Isar style since 2006.)
Moreover some Mizar users have pointed out that the overlap of these old
Isar keywords with the ones of the same name, but different meaning in
Mizar cause unnecessary confusion. I agree with them: it is better to
phase them out completely.
Makarius
Last updated: Apr 25 2024 at 20:15 UTC