|
1 (* Title: HOL/Library/Field_as_Ring.thy |
|
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 |
|
27 instantiation real :: unique_euclidean_ring |
|
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 |
|
58 instantiation rat :: unique_euclidean_ring |
|
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 |
|
89 instantiation complex :: unique_euclidean_ring |
|
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 |