src/HOL/Enum.thy
 changeset 66817 0b12755ccbb2 parent 66806 a4e82b58d833 child 66838 17989f6bc7b2
```     1.1 --- a/src/HOL/Enum.thy	Sun Oct 08 22:28:22 2017 +0200
1.2 +++ b/src/HOL/Enum.thy	Sun Oct 08 22:28:22 2017 +0200
1.3 @@ -712,7 +712,7 @@
1.4    "x dvd y \<longleftrightarrow> x = a\<^sub>2 \<or> y = a\<^sub>1"
1.5    by (auto simp add: dvd_def times_finite_2_def split: finite_2.splits)
1.6
1.7 -instantiation finite_2 :: unique_euclidean_semiring begin
1.8 +instantiation finite_2 :: "{normalization_semidom, unique_euclidean_semiring}" begin
1.9  definition [simp]: "normalize = (id :: finite_2 \<Rightarrow> _)"
1.10  definition [simp]: "unit_factor = (id :: finite_2 \<Rightarrow> _)"
1.11  definition [simp]: "euclidean_size x = (case x of a\<^sub>1 \<Rightarrow> 0 | a\<^sub>2 \<Rightarrow> 1)"
1.12 @@ -864,7 +864,7 @@
1.13    "x dvd y \<longleftrightarrow> x = a\<^sub>2 \<or> x = a\<^sub>3 \<or> y = a\<^sub>1"
1.14    by (cases x) (auto simp add: dvd_def times_finite_3_def split: finite_3.splits)
1.15
1.16 -instantiation finite_3 :: unique_euclidean_semiring begin
1.17 +instantiation finite_3 :: "{normalization_semidom, unique_euclidean_semiring}" begin
1.18  definition [simp]: "normalize x = (case x of a\<^sub>3 \<Rightarrow> a\<^sub>2 | _ \<Rightarrow> x)"
1.19  definition [simp]: "unit_factor = (id :: finite_3 \<Rightarrow> _)"
1.20  definition [simp]: "euclidean_size x = (case x of a\<^sub>1 \<Rightarrow> 0 | _ \<Rightarrow> 1)"
```