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