author | haftmann |
Sat, 17 Dec 2016 15:22:13 +0100 | |
changeset 64591 | 240a39af9ec4 |
child 64784 | 5cb5e7ecb284 |
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 |
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
27 |
instantiation real :: euclidean_ring |
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> _)" |
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
33 |
definition [simp]: "modulo_real = (mod_field :: real \<Rightarrow> _)" |
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
34 |
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
35 |
instance by standard (simp_all add: dvd_field_iff divide_simps) |
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
36 |
end |
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
37 |
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
38 |
instantiation real :: euclidean_ring_gcd |
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
39 |
begin |
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
40 |
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
41 |
definition gcd_real :: "real \<Rightarrow> real \<Rightarrow> real" where |
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
42 |
"gcd_real = gcd_eucl" |
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
43 |
definition lcm_real :: "real \<Rightarrow> real \<Rightarrow> real" where |
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
44 |
"lcm_real = lcm_eucl" |
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
45 |
definition Gcd_real :: "real set \<Rightarrow> real" where |
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
46 |
"Gcd_real = Gcd_eucl" |
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
47 |
definition Lcm_real :: "real set \<Rightarrow> real" where |
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
48 |
"Lcm_real = Lcm_eucl" |
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
49 |
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
50 |
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
|
51 |
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
52 |
end |
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 |
instantiation rat :: euclidean_ring |
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
55 |
begin |
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
56 |
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
57 |
definition [simp]: "normalize_rat = (normalize_field :: rat \<Rightarrow> _)" |
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
58 |
definition [simp]: "unit_factor_rat = (unit_factor_field :: rat \<Rightarrow> _)" |
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
59 |
definition [simp]: "euclidean_size_rat = (euclidean_size_field :: rat \<Rightarrow> _)" |
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
60 |
definition [simp]: "modulo_rat = (mod_field :: rat \<Rightarrow> _)" |
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
61 |
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
62 |
instance by standard (simp_all add: dvd_field_iff divide_simps) |
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
63 |
end |
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
64 |
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
65 |
instantiation rat :: euclidean_ring_gcd |
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
66 |
begin |
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
67 |
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
68 |
definition gcd_rat :: "rat \<Rightarrow> rat \<Rightarrow> rat" where |
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
69 |
"gcd_rat = gcd_eucl" |
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
70 |
definition lcm_rat :: "rat \<Rightarrow> rat \<Rightarrow> rat" where |
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
71 |
"lcm_rat = lcm_eucl" |
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
72 |
definition Gcd_rat :: "rat set \<Rightarrow> rat" where |
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
73 |
"Gcd_rat = Gcd_eucl" |
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
74 |
definition Lcm_rat :: "rat set \<Rightarrow> rat" where |
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
75 |
"Lcm_rat = Lcm_eucl" |
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
76 |
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
77 |
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
|
78 |
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
79 |
end |
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
80 |
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
81 |
instantiation complex :: euclidean_ring |
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
82 |
begin |
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
83 |
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
84 |
definition [simp]: "normalize_complex = (normalize_field :: complex \<Rightarrow> _)" |
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
85 |
definition [simp]: "unit_factor_complex = (unit_factor_field :: complex \<Rightarrow> _)" |
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
86 |
definition [simp]: "euclidean_size_complex = (euclidean_size_field :: complex \<Rightarrow> _)" |
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
87 |
definition [simp]: "modulo_complex = (mod_field :: complex \<Rightarrow> _)" |
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
88 |
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
89 |
instance by standard (simp_all add: dvd_field_iff divide_simps) |
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
90 |
end |
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 |
instantiation complex :: euclidean_ring_gcd |
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
93 |
begin |
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
94 |
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
95 |
definition gcd_complex :: "complex \<Rightarrow> complex \<Rightarrow> complex" where |
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
96 |
"gcd_complex = gcd_eucl" |
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
97 |
definition lcm_complex :: "complex \<Rightarrow> complex \<Rightarrow> complex" where |
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
98 |
"lcm_complex = lcm_eucl" |
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
99 |
definition Gcd_complex :: "complex set \<Rightarrow> complex" where |
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
100 |
"Gcd_complex = Gcd_eucl" |
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
101 |
definition Lcm_complex :: "complex set \<Rightarrow> complex" where |
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
102 |
"Lcm_complex = Lcm_eucl" |
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 |
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
|
105 |
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
106 |
end |
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
107 |
|
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
diff
changeset
|
108 |
end |