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