Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Field_as_Ring.thy Sprache: Isabelle

Original von: 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

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.