Email Gateway (Aug 22 2022 at 15:12): Email Gateway (Aug 22 2022 at 15:12):From: Michel via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
I am doing the proofs of a theory De_Morgan.thy (sent by Makarius) which
is a sequence of lemmas whose I have to prove. Some lemmas are
intuitionistic, others require the axiom classical. This axiom is
defined as in the isar-ref p44, §2.3.4 by
locale classical =
assumes classical :"(¬C ⟹ C) ⟹ C" begin ...lemmas using classical end
But when, in the same theory, I want to write again "locale classical",
I have a message "Duplicate definition of De_Morgan.classical". So I am
obliged, for this other sequence of exercises, to change the name
classical in, for example classical1. Why locale is not local to the
bloc following the locale command.
Email Gateway (Aug 22 2022 at 15:12):From: Makarius <makarius@sketis.net>
Such a locale is defined once and re-entered multiple times, e.g. via
context classical
begin
lemma ...
end
Or shorter:
lemma (in classical) ...
In some of my examples and exercises, I have used "notepad" with "have"
statements instead of topmost lemma. In a notepad, you cannot operate on
locales as above.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC