src/HOL/Enum.thy
 changeset 64290 fb5c74a58796 parent 63950 cdc1e59aa513 child 64592 7759f1766189
```     1.1 --- a/src/HOL/Enum.thy	Tue Oct 18 17:29:28 2016 +0200
1.2 +++ b/src/HOL/Enum.thy	Tue Oct 18 18:48:53 2016 +0200
1.3 @@ -580,7 +580,7 @@
1.4  instantiation finite_1 ::
1.5    "{linordered_ring_strict, linordered_comm_semiring_strict, ordered_comm_ring,
1.6      ordered_cancel_comm_monoid_diff, comm_monoid_mult, ordered_ring_abs,
1.7 -    one, modulo, sgn_if, inverse}"
1.8 +    one, modulo, sgn, inverse}"
1.9  begin
1.10  definition [simp]: "Groups.zero = a\<^sub>1"
1.11  definition [simp]: "Groups.one = a\<^sub>1"
1.12 @@ -683,7 +683,7 @@
1.13
1.14  instance finite_2 :: complete_linorder ..
1.15
1.16 -instantiation finite_2 :: "{field, abs_if, ring_div, sgn_if, semiring_div}" begin
1.17 +instantiation finite_2 :: "{field, ring_div, idom_abs_sgn}" begin
1.18  definition [simp]: "0 = a\<^sub>1"
1.19  definition [simp]: "1 = a\<^sub>2"
1.20  definition "x + y = (case (x, y) of (a\<^sub>1, a\<^sub>1) \<Rightarrow> a\<^sub>1 | (a\<^sub>2, a\<^sub>2) \<Rightarrow> a\<^sub>1 | _ \<Rightarrow> a\<^sub>2)"
1.21 @@ -806,7 +806,7 @@
1.22
1.23  instance finite_3 :: complete_linorder ..
1.24
1.25 -instantiation finite_3 :: "{field, abs_if, ring_div, semiring_div, sgn_if}" begin
1.26 +instantiation finite_3 :: "{field, ring_div, idom_abs_sgn}" begin
1.27  definition [simp]: "0 = a\<^sub>1"
1.28  definition [simp]: "1 = a\<^sub>2"
1.29  definition
1.30 @@ -819,9 +819,9 @@
1.31  definition "x * y = (case (x, y) of (a\<^sub>2, a\<^sub>2) \<Rightarrow> a\<^sub>2 | (a\<^sub>3, a\<^sub>3) \<Rightarrow> a\<^sub>2 | (a\<^sub>2, a\<^sub>3) \<Rightarrow> a\<^sub>3 | (a\<^sub>3, a\<^sub>2) \<Rightarrow> a\<^sub>3 | _ \<Rightarrow> a\<^sub>1)"
1.32  definition "inverse = (\<lambda>x :: finite_3. x)"
1.33  definition "x div y = x * inverse (y :: finite_3)"
1.34 -definition "abs = (\<lambda>x :: finite_3. x)"
1.35 +definition "abs = (\<lambda>x. case x of a\<^sub>3 \<Rightarrow> a\<^sub>2 | _ \<Rightarrow> x)"
1.36  definition "x mod y = (case (x, y) of (a\<^sub>2, a\<^sub>1) \<Rightarrow> a\<^sub>2 | (a\<^sub>3, a\<^sub>1) \<Rightarrow> a\<^sub>3 | _ \<Rightarrow> a\<^sub>1)"
1.37 -definition "sgn = (\<lambda>x. case x of a\<^sub>1 \<Rightarrow> a\<^sub>1 | _ \<Rightarrow> a\<^sub>2)"
1.38 +definition "sgn = (\<lambda>x :: finite_3. x)"
1.39  instance
1.40  by intro_classes
1.41    (simp_all add: plus_finite_3_def uminus_finite_3_def minus_finite_3_def times_finite_3_def
```