author | haftmann |
Mon, 09 Oct 2017 19:10:49 +0200 | |
changeset 66838 | 17989f6bc7b2 |
parent 66817 | 0b12755ccbb2 |
child 70817 | dd675800469d |
permissions | -rw-r--r-- |
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> _)" |
|
66838
17989f6bc7b2
clarified uniqueness criterion for euclidean rings
haftmann
parents:
66817
diff
changeset
|
32 |
definition [simp]: "modulo_real = (mod_field :: real \<Rightarrow> _)" |
65417 | 33 |
definition [simp]: "euclidean_size_real = (euclidean_size_field :: real \<Rightarrow> _)" |
66838
17989f6bc7b2
clarified uniqueness criterion for euclidean rings
haftmann
parents:
66817
diff
changeset
|
34 |
definition [simp]: "division_segment (x :: real) = 1" |
65417 | 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> _)" |
|
66838
17989f6bc7b2
clarified uniqueness criterion for euclidean rings
haftmann
parents:
66817
diff
changeset
|
63 |
definition [simp]: "modulo_rat = (mod_field :: rat \<Rightarrow> _)" |
65417 | 64 |
definition [simp]: "euclidean_size_rat = (euclidean_size_field :: rat \<Rightarrow> _)" |
66838
17989f6bc7b2
clarified uniqueness criterion for euclidean rings
haftmann
parents:
66817
diff
changeset
|
65 |
definition [simp]: "division_segment (x :: rat) = 1" |
65417 | 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> _)" |
|
66838
17989f6bc7b2
clarified uniqueness criterion for euclidean rings
haftmann
parents:
66817
diff
changeset
|
94 |
definition [simp]: "modulo_complex = (mod_field :: complex \<Rightarrow> _)" |
65417 | 95 |
definition [simp]: "euclidean_size_complex = (euclidean_size_field :: complex \<Rightarrow> _)" |
66838
17989f6bc7b2
clarified uniqueness criterion for euclidean rings
haftmann
parents:
66817
diff
changeset
|
96 |
definition [simp]: "division_segment (x :: complex) = 1" |
65417 | 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 |