equal
deleted
inserted
replaced
27 instantiation real :: "{unique_euclidean_ring, normalization_euclidean_semiring}" |
27 instantiation real :: "{unique_euclidean_ring, normalization_euclidean_semiring}" |
28 begin |
28 begin |
29 |
29 |
30 definition [simp]: "normalize_real = (normalize_field :: real \<Rightarrow> _)" |
30 definition [simp]: "normalize_real = (normalize_field :: real \<Rightarrow> _)" |
31 definition [simp]: "unit_factor_real = (unit_factor_field :: real \<Rightarrow> _)" |
31 definition [simp]: "unit_factor_real = (unit_factor_field :: real \<Rightarrow> _)" |
|
32 definition [simp]: "modulo_real = (mod_field :: real \<Rightarrow> _)" |
32 definition [simp]: "euclidean_size_real = (euclidean_size_field :: real \<Rightarrow> _)" |
33 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]: "division_segment (x :: real) = 1" |
34 definition [simp]: "modulo_real = (mod_field :: real \<Rightarrow> _)" |
|
35 |
35 |
36 instance |
36 instance |
37 by standard |
37 by standard |
38 (simp_all add: dvd_field_iff divide_simps split: if_splits) |
38 (simp_all add: dvd_field_iff divide_simps split: if_splits) |
39 |
39 |
58 instantiation rat :: "{unique_euclidean_ring, normalization_euclidean_semiring}" |
58 instantiation rat :: "{unique_euclidean_ring, normalization_euclidean_semiring}" |
59 begin |
59 begin |
60 |
60 |
61 definition [simp]: "normalize_rat = (normalize_field :: rat \<Rightarrow> _)" |
61 definition [simp]: "normalize_rat = (normalize_field :: rat \<Rightarrow> _)" |
62 definition [simp]: "unit_factor_rat = (unit_factor_field :: rat \<Rightarrow> _)" |
62 definition [simp]: "unit_factor_rat = (unit_factor_field :: rat \<Rightarrow> _)" |
|
63 definition [simp]: "modulo_rat = (mod_field :: rat \<Rightarrow> _)" |
63 definition [simp]: "euclidean_size_rat = (euclidean_size_field :: rat \<Rightarrow> _)" |
64 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]: "division_segment (x :: rat) = 1" |
65 definition [simp]: "modulo_rat = (mod_field :: rat \<Rightarrow> _)" |
|
66 |
66 |
67 instance |
67 instance |
68 by standard |
68 by standard |
69 (simp_all add: dvd_field_iff divide_simps split: if_splits) |
69 (simp_all add: dvd_field_iff divide_simps split: if_splits) |
70 |
70 |
89 instantiation complex :: "{unique_euclidean_ring, normalization_euclidean_semiring}" |
89 instantiation complex :: "{unique_euclidean_ring, normalization_euclidean_semiring}" |
90 begin |
90 begin |
91 |
91 |
92 definition [simp]: "normalize_complex = (normalize_field :: complex \<Rightarrow> _)" |
92 definition [simp]: "normalize_complex = (normalize_field :: complex \<Rightarrow> _)" |
93 definition [simp]: "unit_factor_complex = (unit_factor_field :: complex \<Rightarrow> _)" |
93 definition [simp]: "unit_factor_complex = (unit_factor_field :: complex \<Rightarrow> _)" |
|
94 definition [simp]: "modulo_complex = (mod_field :: complex \<Rightarrow> _)" |
94 definition [simp]: "euclidean_size_complex = (euclidean_size_field :: complex \<Rightarrow> _)" |
95 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]: "division_segment (x :: complex) = 1" |
96 definition [simp]: "modulo_complex = (mod_field :: complex \<Rightarrow> _)" |
|
97 |
97 |
98 instance |
98 instance |
99 by standard |
99 by standard |
100 (simp_all add: dvd_field_iff divide_simps split: if_splits) |
100 (simp_all add: dvd_field_iff divide_simps split: if_splits) |
101 |
101 |