|
65435
|
1 |
(* Title: HOL/Computational_Algebra/Field_as_Ring.thy
|
|
65417
|
2 |
Author: Manuel Eberl
|
|
|
3 |
*)
|
|
|
4 |
|
|
|
5 |
theory Field_as_Ring
|
|
|
6 |
imports
|
|
|
7 |
Complex_Main
|
|
|
8 |
Euclidean_Algorithm
|
|
|
9 |
begin
|
|
|
10 |
|
|
|
11 |
context field
|
|
|
12 |
begin
|
|
|
13 |
|
|
|
14 |
subclass idom_divide ..
|
|
|
15 |
|
|
|
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)"
|
|
|
24 |
|
|
|
25 |
end
|
|
|
26 |
|
|
66817
|
27 |
instantiation real :: "{unique_euclidean_ring, normalization_euclidean_semiring}"
|
|
65417
|
28 |
begin
|
|
|
29 |
|
|
|
30 |
definition [simp]: "normalize_real = (normalize_field :: real \<Rightarrow> _)"
|
|
|
31 |
definition [simp]: "unit_factor_real = (unit_factor_field :: real \<Rightarrow> _)"
|
|
|
32 |
definition [simp]: "euclidean_size_real = (euclidean_size_field :: real \<Rightarrow> _)"
|
|
|
33 |
definition [simp]: "uniqueness_constraint_real = (top :: real \<Rightarrow> real \<Rightarrow> bool)"
|
|
|
34 |
definition [simp]: "modulo_real = (mod_field :: real \<Rightarrow> _)"
|
|
|
35 |
|
|
|
36 |
instance
|
|
|
37 |
by standard
|
|
|
38 |
(simp_all add: dvd_field_iff divide_simps split: if_splits)
|
|
|
39 |
|
|
|
40 |
end
|
|
|
41 |
|
|
|
42 |
instantiation real :: euclidean_ring_gcd
|
|
|
43 |
begin
|
|
|
44 |
|
|
|
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"
|
|
|
53 |
|
|
|
54 |
instance by standard (simp_all add: gcd_real_def lcm_real_def Gcd_real_def Lcm_real_def)
|
|
|
55 |
|
|
|
56 |
end
|
|
|
57 |
|
|
66817
|
58 |
instantiation rat :: "{unique_euclidean_ring, normalization_euclidean_semiring}"
|
|
65417
|
59 |
begin
|
|
|
60 |
|
|
|
61 |
definition [simp]: "normalize_rat = (normalize_field :: rat \<Rightarrow> _)"
|
|
|
62 |
definition [simp]: "unit_factor_rat = (unit_factor_field :: rat \<Rightarrow> _)"
|
|
|
63 |
definition [simp]: "euclidean_size_rat = (euclidean_size_field :: rat \<Rightarrow> _)"
|
|
|
64 |
definition [simp]: "uniqueness_constraint_rat = (top :: rat \<Rightarrow> rat \<Rightarrow> bool)"
|
|
|
65 |
definition [simp]: "modulo_rat = (mod_field :: rat \<Rightarrow> _)"
|
|
|
66 |
|
|
|
67 |
instance
|
|
|
68 |
by standard
|
|
|
69 |
(simp_all add: dvd_field_iff divide_simps split: if_splits)
|
|
|
70 |
|
|
|
71 |
end
|
|
|
72 |
|
|
|
73 |
instantiation rat :: euclidean_ring_gcd
|
|
|
74 |
begin
|
|
|
75 |
|
|
|
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"
|
|
|
84 |
|
|
|
85 |
instance by standard (simp_all add: gcd_rat_def lcm_rat_def Gcd_rat_def Lcm_rat_def)
|
|
|
86 |
|
|
|
87 |
end
|
|
|
88 |
|
|
66817
|
89 |
instantiation complex :: "{unique_euclidean_ring, normalization_euclidean_semiring}"
|
|
65417
|
90 |
begin
|
|
|
91 |
|
|
|
92 |
definition [simp]: "normalize_complex = (normalize_field :: complex \<Rightarrow> _)"
|
|
|
93 |
definition [simp]: "unit_factor_complex = (unit_factor_field :: complex \<Rightarrow> _)"
|
|
|
94 |
definition [simp]: "euclidean_size_complex = (euclidean_size_field :: complex \<Rightarrow> _)"
|
|
|
95 |
definition [simp]: "uniqueness_constraint_complex = (top :: complex \<Rightarrow> complex \<Rightarrow> bool)"
|
|
|
96 |
definition [simp]: "modulo_complex = (mod_field :: complex \<Rightarrow> _)"
|
|
|
97 |
|
|
|
98 |
instance
|
|
|
99 |
by standard
|
|
|
100 |
(simp_all add: dvd_field_iff divide_simps split: if_splits)
|
|
|
101 |
|
|
|
102 |
end
|
|
|
103 |
|
|
|
104 |
instantiation complex :: euclidean_ring_gcd
|
|
|
105 |
begin
|
|
|
106 |
|
|
|
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"
|
|
|
115 |
|
|
|
116 |
instance by standard (simp_all add: gcd_complex_def lcm_complex_def Gcd_complex_def Lcm_complex_def)
|
|
|
117 |
|
|
|
118 |
end
|
|
|
119 |
|
|
|
120 |
end
|