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)"