src/HOL/Enum.thy
changeset 64592 7759f1766189
parent 64290 fb5c74a58796
child 65956 639eb3617a86
     1.1 --- a/src/HOL/Enum.thy	Sat Dec 17 15:22:13 2016 +0100
     1.2 +++ b/src/HOL/Enum.thy	Sat Dec 17 15:22:14 2016 +0100
     1.3 @@ -683,7 +683,7 @@
     1.4  
     1.5  instance finite_2 :: complete_linorder ..
     1.6  
     1.7 -instantiation finite_2 :: "{field, ring_div, idom_abs_sgn}" begin
     1.8 +instantiation finite_2 :: "{field, idom_abs_sgn}" begin
     1.9  definition [simp]: "0 = a\<^sub>1"
    1.10  definition [simp]: "1 = a\<^sub>2"
    1.11  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.12 @@ -693,19 +693,33 @@
    1.13  definition "inverse = (\<lambda>x :: finite_2. x)"
    1.14  definition "divide = (op * :: finite_2 \<Rightarrow> _)"
    1.15  definition "abs = (\<lambda>x :: finite_2. x)"
    1.16 -definition "x mod y = (case (x, y) of (a\<^sub>2, a\<^sub>1) \<Rightarrow> a\<^sub>2 | _ \<Rightarrow> a\<^sub>1)"
    1.17  definition "sgn = (\<lambda>x :: finite_2. x)"
    1.18  instance
    1.19 -by intro_classes
    1.20 -  (simp_all add: plus_finite_2_def uminus_finite_2_def minus_finite_2_def times_finite_2_def
    1.21 -       inverse_finite_2_def divide_finite_2_def abs_finite_2_def modulo_finite_2_def sgn_finite_2_def
    1.22 -     split: finite_2.splits)
    1.23 +  by standard
    1.24 +    (simp_all add: plus_finite_2_def uminus_finite_2_def minus_finite_2_def times_finite_2_def
    1.25 +      inverse_finite_2_def divide_finite_2_def abs_finite_2_def sgn_finite_2_def
    1.26 +      split: finite_2.splits)
    1.27  end
    1.28  
    1.29  lemma two_finite_2 [simp]:
    1.30    "2 = a\<^sub>1"
    1.31    by (simp add: numeral.simps plus_finite_2_def)
    1.32 -  
    1.33 +
    1.34 +lemma dvd_finite_2_unfold:
    1.35 +  "x dvd y \<longleftrightarrow> x = a\<^sub>2 \<or> y = a\<^sub>1"
    1.36 +  by (auto simp add: dvd_def times_finite_2_def split: finite_2.splits)
    1.37 +
    1.38 +instantiation finite_2 :: "{ring_div, normalization_semidom}" begin
    1.39 +definition [simp]: "normalize = (id :: finite_2 \<Rightarrow> _)"
    1.40 +definition [simp]: "unit_factor = (id :: finite_2 \<Rightarrow> _)"
    1.41 +definition "x mod y = (case (x, y) of (a\<^sub>2, a\<^sub>1) \<Rightarrow> a\<^sub>2 | _ \<Rightarrow> a\<^sub>1)"
    1.42 +instance
    1.43 +  by standard
    1.44 +    (simp_all add: dvd_finite_2_unfold times_finite_2_def
    1.45 +      divide_finite_2_def modulo_finite_2_def split: finite_2.splits)
    1.46 +end
    1.47 +
    1.48 + 
    1.49  hide_const (open) a\<^sub>1 a\<^sub>2
    1.50  
    1.51  datatype (plugins only: code "quickcheck" extraction) finite_3 =
    1.52 @@ -736,6 +750,12 @@
    1.53  
    1.54  end
    1.55  
    1.56 +lemma finite_3_not_eq_unfold:
    1.57 +  "x \<noteq> a\<^sub>1 \<longleftrightarrow> x \<in> {a\<^sub>2, a\<^sub>3}"
    1.58 +  "x \<noteq> a\<^sub>2 \<longleftrightarrow> x \<in> {a\<^sub>1, a\<^sub>3}"
    1.59 +  "x \<noteq> a\<^sub>3 \<longleftrightarrow> x \<in> {a\<^sub>1, a\<^sub>2}"
    1.60 +  by (cases x; simp)+
    1.61 +
    1.62  instantiation finite_3 :: linorder
    1.63  begin
    1.64  
    1.65 @@ -806,7 +826,7 @@
    1.66  
    1.67  instance finite_3 :: complete_linorder ..
    1.68  
    1.69 -instantiation finite_3 :: "{field, ring_div, idom_abs_sgn}" begin
    1.70 +instantiation finite_3 :: "{field, idom_abs_sgn}" begin
    1.71  definition [simp]: "0 = a\<^sub>1"
    1.72  definition [simp]: "1 = a\<^sub>2"
    1.73  definition
    1.74 @@ -820,14 +840,33 @@
    1.75  definition "inverse = (\<lambda>x :: finite_3. x)" 
    1.76  definition "x div y = x * inverse (y :: finite_3)"
    1.77  definition "abs = (\<lambda>x. case x of a\<^sub>3 \<Rightarrow> a\<^sub>2 | _ \<Rightarrow> x)"
    1.78 -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.79  definition "sgn = (\<lambda>x :: finite_3. x)"
    1.80  instance
    1.81 -by intro_classes
    1.82 -  (simp_all add: plus_finite_3_def uminus_finite_3_def minus_finite_3_def times_finite_3_def
    1.83 -       inverse_finite_3_def divide_finite_3_def abs_finite_3_def modulo_finite_3_def sgn_finite_3_def
    1.84 -       less_finite_3_def
    1.85 -     split: finite_3.splits)
    1.86 +  by standard
    1.87 +    (simp_all add: plus_finite_3_def uminus_finite_3_def minus_finite_3_def times_finite_3_def
    1.88 +      inverse_finite_3_def divide_finite_3_def abs_finite_3_def sgn_finite_3_def
    1.89 +      less_finite_3_def
    1.90 +      split: finite_3.splits)
    1.91 +end
    1.92 +
    1.93 +lemma two_finite_3 [simp]:
    1.94 +  "2 = a\<^sub>3"
    1.95 +  by (simp add: numeral.simps plus_finite_3_def)
    1.96 +
    1.97 +lemma dvd_finite_3_unfold:
    1.98 +  "x dvd y \<longleftrightarrow> x = a\<^sub>2 \<or> x = a\<^sub>3 \<or> y = a\<^sub>1"
    1.99 +  by (cases x) (auto simp add: dvd_def times_finite_3_def split: finite_3.splits)
   1.100 +
   1.101 +instantiation finite_3 :: "{ring_div, normalization_semidom}" begin
   1.102 +definition "normalize x = (case x of a\<^sub>3 \<Rightarrow> a\<^sub>2 | _ \<Rightarrow> x)"
   1.103 +definition [simp]: "unit_factor = (id :: finite_3 \<Rightarrow> _)"
   1.104 +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.105 +instance
   1.106 +  by standard
   1.107 +    (auto simp add: finite_3_not_eq_unfold plus_finite_3_def
   1.108 +      dvd_finite_3_unfold times_finite_3_def inverse_finite_3_def
   1.109 +      normalize_finite_3_def divide_finite_3_def modulo_finite_3_def
   1.110 +      split: finite_3.splits)
   1.111  end
   1.112  
   1.113