Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/Sources/formale Sprachen/Isabelle/HOL/Computational_Algebra/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 4 kB

Impressum Field_as_Ring.thy Sprache: Isabelle

(*  Title:      HOL/Computational_Algebra/Field_as_Ring.thy
    Author:     Manuel Eberl
*)

theory Field_as_Ring
imports
  Complex_Main
  Euclidean_Algorithm
begin

context field
begin

subclass idom_divide ..

definition normalize_field :: "'a \ 'a"
  where [simp]: "normalize_field x = (if x = 0 then 0 else 1)"
definition unit_factor_field :: "'a \ 'a"
  where [simp]: "unit_factor_field x = x"
definition euclidean_size_field :: "'a \ nat"
  where [simp]: "euclidean_size_field x = (if x = 0 then 0 else 1)"
definition mod_field :: "'a \ 'a \ 'a"
  where [simp]: "mod_field x y = (if y = 0 then x else 0)"

end

instantiation real ::
  "{unique_euclidean_ring, normalization_euclidean_semiring, normalization_semidom_multiplicative}"
begin

definition [simp]: "normalize_real = (normalize_field :: real \ _)"
definition [simp]: "unit_factor_real = (unit_factor_field :: real \ _)"
definition [simp]: "modulo_real = (mod_field :: real \ _)"
definition [simp]: "euclidean_size_real = (euclidean_size_field :: real \ _)"
definition [simp]: "division_segment (x :: real) = 1"

instance
  by standard
    (simp_all add: dvd_field_iff field_split_simps split: if_splits)

end

instantiation real :: euclidean_ring_gcd
begin

definition gcd_real :: "real \ real \ real" where
  "gcd_real = Euclidean_Algorithm.gcd"
definition lcm_real :: "real \ real \ real" where
  "lcm_real = Euclidean_Algorithm.lcm"
definition Gcd_real :: "real set \ real" where
"Gcd_real = Euclidean_Algorithm.Gcd"
definition Lcm_real :: "real set \ real" where
"Lcm_real = Euclidean_Algorithm.Lcm"

instance by standard (simp_all add: gcd_real_def lcm_real_def Gcd_real_def Lcm_real_def)

end

instance real :: field_gcd ..

instantiation rat ::
  "{unique_euclidean_ring, normalization_euclidean_semiring, normalization_semidom_multiplicative}"
begin

definition [simp]: "normalize_rat = (normalize_field :: rat \ _)"
definition [simp]: "unit_factor_rat = (unit_factor_field :: rat \ _)"
definition [simp]: "modulo_rat = (mod_field :: rat \ _)"
definition [simp]: "euclidean_size_rat = (euclidean_size_field :: rat \ _)"
definition [simp]: "division_segment (x :: rat) = 1"

instance
  by standard
    (simp_all add: dvd_field_iff field_split_simps split: if_splits)

end

instantiation rat :: euclidean_ring_gcd
begin

definition gcd_rat :: "rat \ rat \ rat" where
  "gcd_rat = Euclidean_Algorithm.gcd"
definition lcm_rat :: "rat \ rat \ rat" where
  "lcm_rat = Euclidean_Algorithm.lcm"
definition Gcd_rat :: "rat set \ rat" where
"Gcd_rat = Euclidean_Algorithm.Gcd"
definition Lcm_rat :: "rat set \ rat" where
"Lcm_rat = Euclidean_Algorithm.Lcm"

instance by standard (simp_all add: gcd_rat_def lcm_rat_def Gcd_rat_def Lcm_rat_def)

end

instance rat :: field_gcd ..

instantiation complex ::
  "{unique_euclidean_ring, normalization_euclidean_semiring, normalization_semidom_multiplicative}"
begin

definition [simp]: "normalize_complex = (normalize_field :: complex \ _)"
definition [simp]: "unit_factor_complex = (unit_factor_field :: complex \ _)"
definition [simp]: "modulo_complex = (mod_field :: complex \ _)"
definition [simp]: "euclidean_size_complex = (euclidean_size_field :: complex \ _)"
definition [simp]: "division_segment (x :: complex) = 1"

instance
  by standard
    (simp_all add: dvd_field_iff field_split_simps split: if_splits)

end

instantiation complex :: euclidean_ring_gcd
begin

definition gcd_complex :: "complex \ complex \ complex" where
  "gcd_complex = Euclidean_Algorithm.gcd"
definition lcm_complex :: "complex \ complex \ complex" where
  "lcm_complex = Euclidean_Algorithm.lcm"
definition Gcd_complex :: "complex set \ complex" where
"Gcd_complex = Euclidean_Algorithm.Gcd"
definition Lcm_complex :: "complex set \ complex" where
"Lcm_complex = Euclidean_Algorithm.Lcm"

instance by standard (simp_all add: gcd_complex_def lcm_complex_def Gcd_complex_def Lcm_complex_def)

end

instance complex :: field_gcd ..

end

quality100%

¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.11Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.