Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Quotient_type and locale

Email Gateway (Dec 29 2022 at 19:47):

From: Jelena Markovic <jelena.markovic.10.11@gmail.com>
Is there some way to use quotient_type inside locale? Currently we use
quotient_type with axiomatization, but it's not what we wanted to do. Can
we connect these two somehow?

Email Gateway (Dec 31 2022 at 09:19):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Jelena,

Am 29.12.22 um 11:38 schrieb Jelena Markovic:

Is there some way to use quotient_type inside locale? Currently we use
quotient_type with axiomatization, but it's not what we wanted to do.
Can we connect these two somehow?

your question is very implicit.

Can you show an example which illustrates your issue?

In principle, quotient_type can be used within locales

locale foo =
fixes bar :: ‹'a itself ⇒ nat›
assumes ‹even (bar TYPE('a))›
begin

quotient_type int = ‹nat × nat› / intrel
morphisms Rep_Integ Abs_Integ
proof (rule equivpI)
show ‹reflp intrel›
by (auto simp: reflp_def)
show ‹symp intrel›
by (auto simp: symp_def)
show ‹transp intrel›
by (auto simp: transp_def)
qed

end

as long as it does not depend on context parameters.

Cheers,
Florian
OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature

Last updated: Apr 25 2024 at 01:08 UTC