Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] locale


view this post on Zulip 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.

view this post on Zulip 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: Mar 29 2024 at 04:18 UTC