src/HOL/Computational_Algebra/Field_as_Ring.thy
 author haftmann Mon Oct 09 19:10:49 2017 +0200 (20 months ago) changeset 66838 17989f6bc7b2 parent 66817 0b12755ccbb2 permissions -rw-r--r--
clarified uniqueness criterion for euclidean rings
 wenzelm@65435 ` 1` ```(* Title: HOL/Computational_Algebra/Field_as_Ring.thy ``` haftmann@65417 ` 2` ``` Author: Manuel Eberl ``` haftmann@65417 ` 3` ```*) ``` haftmann@65417 ` 4` haftmann@65417 ` 5` ```theory Field_as_Ring ``` haftmann@65417 ` 6` ```imports ``` haftmann@65417 ` 7` ``` Complex_Main ``` haftmann@65417 ` 8` ``` Euclidean_Algorithm ``` haftmann@65417 ` 9` ```begin ``` haftmann@65417 ` 10` haftmann@65417 ` 11` ```context field ``` haftmann@65417 ` 12` ```begin ``` haftmann@65417 ` 13` haftmann@65417 ` 14` ```subclass idom_divide .. ``` haftmann@65417 ` 15` haftmann@65417 ` 16` ```definition normalize_field :: "'a \ 'a" ``` haftmann@65417 ` 17` ``` where [simp]: "normalize_field x = (if x = 0 then 0 else 1)" ``` haftmann@65417 ` 18` ```definition unit_factor_field :: "'a \ 'a" ``` haftmann@65417 ` 19` ``` where [simp]: "unit_factor_field x = x" ``` haftmann@65417 ` 20` ```definition euclidean_size_field :: "'a \ nat" ``` haftmann@65417 ` 21` ``` where [simp]: "euclidean_size_field x = (if x = 0 then 0 else 1)" ``` haftmann@65417 ` 22` ```definition mod_field :: "'a \ 'a \ 'a" ``` haftmann@65417 ` 23` ``` where [simp]: "mod_field x y = (if y = 0 then x else 0)" ``` haftmann@65417 ` 24` haftmann@65417 ` 25` ```end ``` haftmann@65417 ` 26` haftmann@66817 ` 27` ```instantiation real :: "{unique_euclidean_ring, normalization_euclidean_semiring}" ``` haftmann@65417 ` 28` ```begin ``` haftmann@65417 ` 29` haftmann@65417 ` 30` ```definition [simp]: "normalize_real = (normalize_field :: real \ _)" ``` haftmann@65417 ` 31` ```definition [simp]: "unit_factor_real = (unit_factor_field :: real \ _)" ``` haftmann@66838 ` 32` ```definition [simp]: "modulo_real = (mod_field :: real \ _)" ``` haftmann@65417 ` 33` ```definition [simp]: "euclidean_size_real = (euclidean_size_field :: real \ _)" ``` haftmann@66838 ` 34` ```definition [simp]: "division_segment (x :: real) = 1" ``` haftmann@65417 ` 35` haftmann@65417 ` 36` ```instance ``` haftmann@65417 ` 37` ``` by standard ``` haftmann@65417 ` 38` ``` (simp_all add: dvd_field_iff divide_simps split: if_splits) ``` haftmann@65417 ` 39` haftmann@65417 ` 40` ```end ``` haftmann@65417 ` 41` haftmann@65417 ` 42` ```instantiation real :: euclidean_ring_gcd ``` haftmann@65417 ` 43` ```begin ``` haftmann@65417 ` 44` haftmann@65417 ` 45` ```definition gcd_real :: "real \ real \ real" where ``` haftmann@65417 ` 46` ``` "gcd_real = Euclidean_Algorithm.gcd" ``` haftmann@65417 ` 47` ```definition lcm_real :: "real \ real \ real" where ``` haftmann@65417 ` 48` ``` "lcm_real = Euclidean_Algorithm.lcm" ``` haftmann@65417 ` 49` ```definition Gcd_real :: "real set \ real" where ``` haftmann@65417 ` 50` ``` "Gcd_real = Euclidean_Algorithm.Gcd" ``` haftmann@65417 ` 51` ```definition Lcm_real :: "real set \ real" where ``` haftmann@65417 ` 52` ``` "Lcm_real = Euclidean_Algorithm.Lcm" ``` haftmann@65417 ` 53` haftmann@65417 ` 54` ```instance by standard (simp_all add: gcd_real_def lcm_real_def Gcd_real_def Lcm_real_def) ``` haftmann@65417 ` 55` haftmann@65417 ` 56` ```end ``` haftmann@65417 ` 57` haftmann@66817 ` 58` ```instantiation rat :: "{unique_euclidean_ring, normalization_euclidean_semiring}" ``` haftmann@65417 ` 59` ```begin ``` haftmann@65417 ` 60` haftmann@65417 ` 61` ```definition [simp]: "normalize_rat = (normalize_field :: rat \ _)" ``` haftmann@65417 ` 62` ```definition [simp]: "unit_factor_rat = (unit_factor_field :: rat \ _)" ``` haftmann@66838 ` 63` ```definition [simp]: "modulo_rat = (mod_field :: rat \ _)" ``` haftmann@65417 ` 64` ```definition [simp]: "euclidean_size_rat = (euclidean_size_field :: rat \ _)" ``` haftmann@66838 ` 65` ```definition [simp]: "division_segment (x :: rat) = 1" ``` haftmann@65417 ` 66` haftmann@65417 ` 67` ```instance ``` haftmann@65417 ` 68` ``` by standard ``` haftmann@65417 ` 69` ``` (simp_all add: dvd_field_iff divide_simps split: if_splits) ``` haftmann@65417 ` 70` haftmann@65417 ` 71` ```end ``` haftmann@65417 ` 72` haftmann@65417 ` 73` ```instantiation rat :: euclidean_ring_gcd ``` haftmann@65417 ` 74` ```begin ``` haftmann@65417 ` 75` haftmann@65417 ` 76` ```definition gcd_rat :: "rat \ rat \ rat" where ``` haftmann@65417 ` 77` ``` "gcd_rat = Euclidean_Algorithm.gcd" ``` haftmann@65417 ` 78` ```definition lcm_rat :: "rat \ rat \ rat" where ``` haftmann@65417 ` 79` ``` "lcm_rat = Euclidean_Algorithm.lcm" ``` haftmann@65417 ` 80` ```definition Gcd_rat :: "rat set \ rat" where ``` haftmann@65417 ` 81` ``` "Gcd_rat = Euclidean_Algorithm.Gcd" ``` haftmann@65417 ` 82` ```definition Lcm_rat :: "rat set \ rat" where ``` haftmann@65417 ` 83` ``` "Lcm_rat = Euclidean_Algorithm.Lcm" ``` haftmann@65417 ` 84` haftmann@65417 ` 85` ```instance by standard (simp_all add: gcd_rat_def lcm_rat_def Gcd_rat_def Lcm_rat_def) ``` haftmann@65417 ` 86` haftmann@65417 ` 87` ```end ``` haftmann@65417 ` 88` haftmann@66817 ` 89` ```instantiation complex :: "{unique_euclidean_ring, normalization_euclidean_semiring}" ``` haftmann@65417 ` 90` ```begin ``` haftmann@65417 ` 91` haftmann@65417 ` 92` ```definition [simp]: "normalize_complex = (normalize_field :: complex \ _)" ``` haftmann@65417 ` 93` ```definition [simp]: "unit_factor_complex = (unit_factor_field :: complex \ _)" ``` haftmann@66838 ` 94` ```definition [simp]: "modulo_complex = (mod_field :: complex \ _)" ``` haftmann@65417 ` 95` ```definition [simp]: "euclidean_size_complex = (euclidean_size_field :: complex \ _)" ``` haftmann@66838 ` 96` ```definition [simp]: "division_segment (x :: complex) = 1" ``` haftmann@65417 ` 97` haftmann@65417 ` 98` ```instance ``` haftmann@65417 ` 99` ``` by standard ``` haftmann@65417 ` 100` ``` (simp_all add: dvd_field_iff divide_simps split: if_splits) ``` haftmann@65417 ` 101` haftmann@65417 ` 102` ```end ``` haftmann@65417 ` 103` haftmann@65417 ` 104` ```instantiation complex :: euclidean_ring_gcd ``` haftmann@65417 ` 105` ```begin ``` haftmann@65417 ` 106` haftmann@65417 ` 107` ```definition gcd_complex :: "complex \ complex \ complex" where ``` haftmann@65417 ` 108` ``` "gcd_complex = Euclidean_Algorithm.gcd" ``` haftmann@65417 ` 109` ```definition lcm_complex :: "complex \ complex \ complex" where ``` haftmann@65417 ` 110` ``` "lcm_complex = Euclidean_Algorithm.lcm" ``` haftmann@65417 ` 111` ```definition Gcd_complex :: "complex set \ complex" where ``` haftmann@65417 ` 112` ``` "Gcd_complex = Euclidean_Algorithm.Gcd" ``` haftmann@65417 ` 113` ```definition Lcm_complex :: "complex set \ complex" where ``` haftmann@65417 ` 114` ``` "Lcm_complex = Euclidean_Algorithm.Lcm" ``` haftmann@65417 ` 115` haftmann@65417 ` 116` ```instance by standard (simp_all add: gcd_complex_def lcm_complex_def Gcd_complex_def Lcm_complex_def) ``` haftmann@65417 ` 117` haftmann@65417 ` 118` ```end ``` haftmann@65417 ` 119` haftmann@65417 ` 120` ```end ```