| author | wenzelm |
| Wed, 08 Mar 2017 10:50:59 +0100 | |
| changeset 65151 | a7394aa4d21c |
| parent 64786 | 340db65fd2c1 |
| permissions | -rw-r--r-- |
|
64591
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
1 |
(* Title: HOL/Library/Field_as_Ring.thy |
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
2 |
Author: Manuel Eberl |
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
3 |
*) |
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
4 |
|
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
5 |
theory Field_as_Ring |
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
6 |
imports |
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
7 |
Complex_Main |
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
8 |
"~~/src/HOL/Number_Theory/Euclidean_Algorithm" |
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
9 |
begin |
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
10 |
|
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
11 |
context field |
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
12 |
begin |
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
13 |
|
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
14 |
subclass idom_divide .. |
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
15 |
|
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
16 |
definition normalize_field :: "'a \<Rightarrow> 'a" |
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
17 |
where [simp]: "normalize_field x = (if x = 0 then 0 else 1)" |
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
18 |
definition unit_factor_field :: "'a \<Rightarrow> 'a" |
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
19 |
where [simp]: "unit_factor_field x = x" |
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
20 |
definition euclidean_size_field :: "'a \<Rightarrow> nat" |
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
21 |
where [simp]: "euclidean_size_field x = (if x = 0 then 0 else 1)" |
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
22 |
definition mod_field :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" |
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
23 |
where [simp]: "mod_field x y = (if y = 0 then x else 0)" |
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
24 |
|
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
25 |
end |
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
26 |
|
|
64784
5cb5e7ecb284
reshaped euclidean semiring into hierarchy of euclidean semirings culminating in uniquely determined euclidean divion
haftmann
parents:
64591
diff
changeset
|
27 |
instantiation real :: unique_euclidean_ring |
|
64591
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
28 |
begin |
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
29 |
|
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
30 |
definition [simp]: "normalize_real = (normalize_field :: real \<Rightarrow> _)" |
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
31 |
definition [simp]: "unit_factor_real = (unit_factor_field :: real \<Rightarrow> _)" |
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
32 |
definition [simp]: "euclidean_size_real = (euclidean_size_field :: real \<Rightarrow> _)" |
|
64784
5cb5e7ecb284
reshaped euclidean semiring into hierarchy of euclidean semirings culminating in uniquely determined euclidean divion
haftmann
parents:
64591
diff
changeset
|
33 |
definition [simp]: "uniqueness_constraint_real = (top :: real \<Rightarrow> real \<Rightarrow> bool)" |
|
64591
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
34 |
definition [simp]: "modulo_real = (mod_field :: real \<Rightarrow> _)" |
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
35 |
|
|
64784
5cb5e7ecb284
reshaped euclidean semiring into hierarchy of euclidean semirings culminating in uniquely determined euclidean divion
haftmann
parents:
64591
diff
changeset
|
36 |
instance |
|
5cb5e7ecb284
reshaped euclidean semiring into hierarchy of euclidean semirings culminating in uniquely determined euclidean divion
haftmann
parents:
64591
diff
changeset
|
37 |
by standard |
|
5cb5e7ecb284
reshaped euclidean semiring into hierarchy of euclidean semirings culminating in uniquely determined euclidean divion
haftmann
parents:
64591
diff
changeset
|
38 |
(simp_all add: dvd_field_iff divide_simps split: if_splits) |
|
5cb5e7ecb284
reshaped euclidean semiring into hierarchy of euclidean semirings culminating in uniquely determined euclidean divion
haftmann
parents:
64591
diff
changeset
|
39 |
|
|
64591
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
40 |
end |
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
41 |
|
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
42 |
instantiation real :: euclidean_ring_gcd |
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
43 |
begin |
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
44 |
|
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
45 |
definition gcd_real :: "real \<Rightarrow> real \<Rightarrow> real" where |
|
64786
340db65fd2c1
reworked to provide auxiliary operations Euclidean_Algorithm.* to instantiate gcd etc. for euclidean rings
haftmann
parents:
64784
diff
changeset
|
46 |
"gcd_real = Euclidean_Algorithm.gcd" |
|
64591
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
47 |
definition lcm_real :: "real \<Rightarrow> real \<Rightarrow> real" where |
|
64786
340db65fd2c1
reworked to provide auxiliary operations Euclidean_Algorithm.* to instantiate gcd etc. for euclidean rings
haftmann
parents:
64784
diff
changeset
|
48 |
"lcm_real = Euclidean_Algorithm.lcm" |
|
64591
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
49 |
definition Gcd_real :: "real set \<Rightarrow> real" where |
|
64786
340db65fd2c1
reworked to provide auxiliary operations Euclidean_Algorithm.* to instantiate gcd etc. for euclidean rings
haftmann
parents:
64784
diff
changeset
|
50 |
"Gcd_real = Euclidean_Algorithm.Gcd" |
|
64591
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
51 |
definition Lcm_real :: "real set \<Rightarrow> real" where |
|
64786
340db65fd2c1
reworked to provide auxiliary operations Euclidean_Algorithm.* to instantiate gcd etc. for euclidean rings
haftmann
parents:
64784
diff
changeset
|
52 |
"Lcm_real = Euclidean_Algorithm.Lcm" |
|
64591
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
53 |
|
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
54 |
instance by standard (simp_all add: gcd_real_def lcm_real_def Gcd_real_def Lcm_real_def) |
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
55 |
|
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
56 |
end |
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
57 |
|
|
64784
5cb5e7ecb284
reshaped euclidean semiring into hierarchy of euclidean semirings culminating in uniquely determined euclidean divion
haftmann
parents:
64591
diff
changeset
|
58 |
instantiation rat :: unique_euclidean_ring |
|
64591
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
59 |
begin |
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
60 |
|
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
61 |
definition [simp]: "normalize_rat = (normalize_field :: rat \<Rightarrow> _)" |
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
62 |
definition [simp]: "unit_factor_rat = (unit_factor_field :: rat \<Rightarrow> _)" |
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
63 |
definition [simp]: "euclidean_size_rat = (euclidean_size_field :: rat \<Rightarrow> _)" |
|
64784
5cb5e7ecb284
reshaped euclidean semiring into hierarchy of euclidean semirings culminating in uniquely determined euclidean divion
haftmann
parents:
64591
diff
changeset
|
64 |
definition [simp]: "uniqueness_constraint_rat = (top :: rat \<Rightarrow> rat \<Rightarrow> bool)" |
|
64591
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
65 |
definition [simp]: "modulo_rat = (mod_field :: rat \<Rightarrow> _)" |
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
66 |
|
|
64784
5cb5e7ecb284
reshaped euclidean semiring into hierarchy of euclidean semirings culminating in uniquely determined euclidean divion
haftmann
parents:
64591
diff
changeset
|
67 |
instance |
|
5cb5e7ecb284
reshaped euclidean semiring into hierarchy of euclidean semirings culminating in uniquely determined euclidean divion
haftmann
parents:
64591
diff
changeset
|
68 |
by standard |
|
5cb5e7ecb284
reshaped euclidean semiring into hierarchy of euclidean semirings culminating in uniquely determined euclidean divion
haftmann
parents:
64591
diff
changeset
|
69 |
(simp_all add: dvd_field_iff divide_simps split: if_splits) |
|
5cb5e7ecb284
reshaped euclidean semiring into hierarchy of euclidean semirings culminating in uniquely determined euclidean divion
haftmann
parents:
64591
diff
changeset
|
70 |
|
|
64591
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
71 |
end |
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
72 |
|
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
73 |
instantiation rat :: euclidean_ring_gcd |
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
74 |
begin |
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
75 |
|
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
76 |
definition gcd_rat :: "rat \<Rightarrow> rat \<Rightarrow> rat" where |
|
64786
340db65fd2c1
reworked to provide auxiliary operations Euclidean_Algorithm.* to instantiate gcd etc. for euclidean rings
haftmann
parents:
64784
diff
changeset
|
77 |
"gcd_rat = Euclidean_Algorithm.gcd" |
|
64591
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
78 |
definition lcm_rat :: "rat \<Rightarrow> rat \<Rightarrow> rat" where |
|
64786
340db65fd2c1
reworked to provide auxiliary operations Euclidean_Algorithm.* to instantiate gcd etc. for euclidean rings
haftmann
parents:
64784
diff
changeset
|
79 |
"lcm_rat = Euclidean_Algorithm.lcm" |
|
64591
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
80 |
definition Gcd_rat :: "rat set \<Rightarrow> rat" where |
|
64786
340db65fd2c1
reworked to provide auxiliary operations Euclidean_Algorithm.* to instantiate gcd etc. for euclidean rings
haftmann
parents:
64784
diff
changeset
|
81 |
"Gcd_rat = Euclidean_Algorithm.Gcd" |
|
64591
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
82 |
definition Lcm_rat :: "rat set \<Rightarrow> rat" where |
|
64786
340db65fd2c1
reworked to provide auxiliary operations Euclidean_Algorithm.* to instantiate gcd etc. for euclidean rings
haftmann
parents:
64784
diff
changeset
|
83 |
"Lcm_rat = Euclidean_Algorithm.Lcm" |
|
64591
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
84 |
|
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
85 |
instance by standard (simp_all add: gcd_rat_def lcm_rat_def Gcd_rat_def Lcm_rat_def) |
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
86 |
|
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
87 |
end |
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
88 |
|
|
64784
5cb5e7ecb284
reshaped euclidean semiring into hierarchy of euclidean semirings culminating in uniquely determined euclidean divion
haftmann
parents:
64591
diff
changeset
|
89 |
instantiation complex :: unique_euclidean_ring |
|
64591
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
90 |
begin |
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
91 |
|
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
92 |
definition [simp]: "normalize_complex = (normalize_field :: complex \<Rightarrow> _)" |
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
93 |
definition [simp]: "unit_factor_complex = (unit_factor_field :: complex \<Rightarrow> _)" |
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
94 |
definition [simp]: "euclidean_size_complex = (euclidean_size_field :: complex \<Rightarrow> _)" |
|
64784
5cb5e7ecb284
reshaped euclidean semiring into hierarchy of euclidean semirings culminating in uniquely determined euclidean divion
haftmann
parents:
64591
diff
changeset
|
95 |
definition [simp]: "uniqueness_constraint_complex = (top :: complex \<Rightarrow> complex \<Rightarrow> bool)" |
|
64591
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
96 |
definition [simp]: "modulo_complex = (mod_field :: complex \<Rightarrow> _)" |
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
97 |
|
|
64784
5cb5e7ecb284
reshaped euclidean semiring into hierarchy of euclidean semirings culminating in uniquely determined euclidean divion
haftmann
parents:
64591
diff
changeset
|
98 |
instance |
|
5cb5e7ecb284
reshaped euclidean semiring into hierarchy of euclidean semirings culminating in uniquely determined euclidean divion
haftmann
parents:
64591
diff
changeset
|
99 |
by standard |
|
5cb5e7ecb284
reshaped euclidean semiring into hierarchy of euclidean semirings culminating in uniquely determined euclidean divion
haftmann
parents:
64591
diff
changeset
|
100 |
(simp_all add: dvd_field_iff divide_simps split: if_splits) |
|
5cb5e7ecb284
reshaped euclidean semiring into hierarchy of euclidean semirings culminating in uniquely determined euclidean divion
haftmann
parents:
64591
diff
changeset
|
101 |
|
|
64591
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
102 |
end |
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
103 |
|
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
104 |
instantiation complex :: euclidean_ring_gcd |
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
105 |
begin |
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
106 |
|
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
107 |
definition gcd_complex :: "complex \<Rightarrow> complex \<Rightarrow> complex" where |
|
64786
340db65fd2c1
reworked to provide auxiliary operations Euclidean_Algorithm.* to instantiate gcd etc. for euclidean rings
haftmann
parents:
64784
diff
changeset
|
108 |
"gcd_complex = Euclidean_Algorithm.gcd" |
|
64591
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
109 |
definition lcm_complex :: "complex \<Rightarrow> complex \<Rightarrow> complex" where |
|
64786
340db65fd2c1
reworked to provide auxiliary operations Euclidean_Algorithm.* to instantiate gcd etc. for euclidean rings
haftmann
parents:
64784
diff
changeset
|
110 |
"lcm_complex = Euclidean_Algorithm.lcm" |
|
64591
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
111 |
definition Gcd_complex :: "complex set \<Rightarrow> complex" where |
|
64786
340db65fd2c1
reworked to provide auxiliary operations Euclidean_Algorithm.* to instantiate gcd etc. for euclidean rings
haftmann
parents:
64784
diff
changeset
|
112 |
"Gcd_complex = Euclidean_Algorithm.Gcd" |
|
64591
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
113 |
definition Lcm_complex :: "complex set \<Rightarrow> complex" where |
|
64786
340db65fd2c1
reworked to provide auxiliary operations Euclidean_Algorithm.* to instantiate gcd etc. for euclidean rings
haftmann
parents:
64784
diff
changeset
|
114 |
"Lcm_complex = Euclidean_Algorithm.Lcm" |
|
64591
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
115 |
|
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
116 |
instance by standard (simp_all add: gcd_complex_def lcm_complex_def Gcd_complex_def Lcm_complex_def) |
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
117 |
|
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
118 |
end |
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
119 |
|
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
120 |
end |