Email Gateway (Aug 22 2022 at 17:47): Email Gateway (Aug 22 2022 at 17:47):From: Anthony Bordg <bordg.anthony@gmail.com>
Hi,
is there a way to directly denote the ring structure of complex from the
theory Complex.thy where it is proven that complex is a field ? In other
words I want a term of type ring_scheme that denotes the ring structure of
complex, the type of complex numbers.
Thank you
Anthony
Email Gateway (Aug 22 2022 at 17:48):From: Fabian Hellauer <hellauer@in.tum.de>
Hi Anthony,
in Isabelle2018-RC1, I use this:
theory Scratch imports
Complex_Main "HOL-Algebra.Ring"
begin
definition univ_ring
where "univ_ring = (|carrier = UNIV, mult = ( *), one = 1, zero = 0,
add = (+)|)"
lemma field_field_ring: "Ring.field (univ_ring::_::Fields.field ring)"
apply unfold_locales
apply (auto intro: right_inverse simp: univ_ring_def
Units_def field_simps)
by (metis ab_group_add_class.ab_left_minus add.commute)
definition rat_field :: "rat ring" where "rat_field = univ_ring"
definition real_field :: "real ring" where "real_field = univ_ring"
definition complex_field :: "complex ring" where "complex_field = univ_ring"
lemma field_example_fields: "field rat_field" "field real_field" "field
complex_field"
unfolding rat_field_def real_field_def complex_field_def by (fact
field_field_ring)+
end
Cheers,
Fabian
Email Gateway (Aug 22 2022 at 17:48):From: Anthony Bordg <bordg.anthony@gmail.com>
Hi Fabian,
Thank you for your answer.
My question was : "is there a way to directly denote the ring structure of
complex from the theory Complex.thy where it is proven that complex is a
field ?". A yes or no will help here. I think the answer is no, but since
it's strange and disturbing for me I would like to be sure just in case I'm
missing something. It's strange since there (in Complex.thy) one proves
that complex is a field, but despite that fact the theory Complex.thy does
not seem to offer a way to directly speak about the ring structure of
complex.
I'm not sure I understand your code. I would naively write something like
that:
definition cpx_set :: "complex set" where
"cpx_set ≡ {z| z::complex. True}"
definition mult_cpx ::"[complex, complex] ⇒ complex" where
"mult_cpx z z' ≡ z * z' "
definition add_cpx ::"[complex, complex] ⇒ complex" where
"add_cpx z z' ≡ z + z' "
definition cpx_rng ::"complex ring" where
"cpx_rng ≡ ⦇carrier = cpx_set, mult = mult_cpx, one = 1, zero = 0, add =
add_cpx⦈"
However, I'm not sure this is the most direct/clever/convenient way to do
it. In particular, I am unable to use times_complex denoted * (resp.
plus_complex denoted +) for the field mult (resp. add) and this is why I
define mult_cpx and add_cpx, indeed times_complex and plus_complex would
not be recognized and they would be seen as variables displayed in blue if
used in the fields mult and add.
Cheers
Anthony
Email Gateway (Aug 22 2022 at 17:49):From: "Thiemann, René" <Rene.Thiemann@uibk.ac.at>
Hi Anthony,
why not simply:
definition cpx_rng ::"complex ring" where
"cpx_rng ≡ ⦇carrier = UNIV, mult = op *, one = 1, zero = 0, add = op +⦈”
Cheers,
René
Email Gateway (Aug 22 2022 at 17:50):From: Anthony Bordg <bordg.anthony@gmail.com>
Dear Rene,
Thank you! I was unfamiliar with "UNIV" and the syntax "op", now I can see
they are exactly the things I was looking for.
Best regards
Anthony
Email Gateway (Aug 22 2022 at 17:50):From: Anthony Bordg <bordg.anthony@gmail.com>
Thank you Fabian for your help, your code is clear for me now.
cheers
Anthony
Last updated: Apr 19 2024 at 08:19 UTC