src/HOL/Enum.thy
changeset 66806 a4e82b58d833
parent 65956 639eb3617a86
child 66817 0b12755ccbb2
     1.1 --- a/src/HOL/Enum.thy	Sun Oct 08 22:28:21 2017 +0200
     1.2 +++ b/src/HOL/Enum.thy	Sun Oct 08 22:28:21 2017 +0200
     1.3 @@ -683,7 +683,7 @@
     1.4  
     1.5  instance finite_2 :: complete_linorder ..
     1.6  
     1.7 -instantiation finite_2 :: "{field, idom_abs_sgn}" begin
     1.8 +instantiation finite_2 :: "{field, idom_abs_sgn, idom_modulo}" 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 @@ -692,12 +692,15 @@
    1.13  definition "x * y = (case (x, y) of (a\<^sub>2, a\<^sub>2) \<Rightarrow> a\<^sub>2 | _ \<Rightarrow> a\<^sub>1)"
    1.14  definition "inverse = (\<lambda>x :: finite_2. x)"
    1.15  definition "divide = (op * :: finite_2 \<Rightarrow> _)"
    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 "abs = (\<lambda>x :: finite_2. x)"
    1.18  definition "sgn = (\<lambda>x :: finite_2. x)"
    1.19  instance
    1.20    by standard
    1.21 -    (simp_all add: plus_finite_2_def uminus_finite_2_def minus_finite_2_def times_finite_2_def
    1.22 -      inverse_finite_2_def divide_finite_2_def abs_finite_2_def sgn_finite_2_def
    1.23 +    (simp_all add: plus_finite_2_def uminus_finite_2_def minus_finite_2_def
    1.24 +      times_finite_2_def
    1.25 +      inverse_finite_2_def divide_finite_2_def modulo_finite_2_def
    1.26 +      abs_finite_2_def sgn_finite_2_def
    1.27        split: finite_2.splits)
    1.28  end
    1.29  
    1.30 @@ -709,14 +712,15 @@
    1.31    "x dvd y \<longleftrightarrow> x = a\<^sub>2 \<or> y = a\<^sub>1"
    1.32    by (auto simp add: dvd_def times_finite_2_def split: finite_2.splits)
    1.33  
    1.34 -instantiation finite_2 :: "{ring_div, normalization_semidom}" begin
    1.35 +instantiation finite_2 :: unique_euclidean_semiring begin
    1.36  definition [simp]: "normalize = (id :: finite_2 \<Rightarrow> _)"
    1.37  definition [simp]: "unit_factor = (id :: finite_2 \<Rightarrow> _)"
    1.38 -definition "x mod y = (case (x, y) of (a\<^sub>2, a\<^sub>1) \<Rightarrow> a\<^sub>2 | _ \<Rightarrow> a\<^sub>1)"
    1.39 +definition [simp]: "euclidean_size x = (case x of a\<^sub>1 \<Rightarrow> 0 | a\<^sub>2 \<Rightarrow> 1)"
    1.40 +definition [simp]: "uniqueness_constraint = (\<top> :: finite_2 \<Rightarrow> _)"
    1.41  instance
    1.42    by standard
    1.43 -    (simp_all add: dvd_finite_2_unfold times_finite_2_def
    1.44 -      divide_finite_2_def modulo_finite_2_def split: finite_2.splits)
    1.45 +    (auto simp add: divide_finite_2_def times_finite_2_def dvd_finite_2_unfold
    1.46 +    split: finite_2.splits)
    1.47  end
    1.48  
    1.49   
    1.50 @@ -826,7 +830,7 @@
    1.51  
    1.52  instance finite_3 :: complete_linorder ..
    1.53  
    1.54 -instantiation finite_3 :: "{field, idom_abs_sgn}" begin
    1.55 +instantiation finite_3 :: "{field, idom_abs_sgn, idom_modulo}" begin
    1.56  definition [simp]: "0 = a\<^sub>1"
    1.57  definition [simp]: "1 = a\<^sub>2"
    1.58  definition
    1.59 @@ -839,12 +843,15 @@
    1.60  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.61  definition "inverse = (\<lambda>x :: finite_3. x)" 
    1.62  definition "x div y = x * inverse (y :: finite_3)"
    1.63 +definition "x mod y = (case y of a\<^sub>1 \<Rightarrow> x | _ \<Rightarrow> a\<^sub>1)"
    1.64  definition "abs = (\<lambda>x. case x of a\<^sub>3 \<Rightarrow> a\<^sub>2 | _ \<Rightarrow> x)"
    1.65  definition "sgn = (\<lambda>x :: finite_3. x)"
    1.66  instance
    1.67    by standard
    1.68 -    (simp_all add: plus_finite_3_def uminus_finite_3_def minus_finite_3_def times_finite_3_def
    1.69 -      inverse_finite_3_def divide_finite_3_def abs_finite_3_def sgn_finite_3_def
    1.70 +    (simp_all add: plus_finite_3_def uminus_finite_3_def minus_finite_3_def
    1.71 +      times_finite_3_def
    1.72 +      inverse_finite_3_def divide_finite_3_def modulo_finite_3_def
    1.73 +      abs_finite_3_def sgn_finite_3_def
    1.74        less_finite_3_def
    1.75        split: finite_3.splits)
    1.76  end
    1.77 @@ -857,20 +864,21 @@
    1.78    "x dvd y \<longleftrightarrow> x = a\<^sub>2 \<or> x = a\<^sub>3 \<or> y = a\<^sub>1"
    1.79    by (cases x) (auto simp add: dvd_def times_finite_3_def split: finite_3.splits)
    1.80  
    1.81 -instantiation finite_3 :: "{ring_div, normalization_semidom}" begin
    1.82 -definition "normalize x = (case x of a\<^sub>3 \<Rightarrow> a\<^sub>2 | _ \<Rightarrow> x)"
    1.83 +instantiation finite_3 :: unique_euclidean_semiring begin
    1.84 +definition [simp]: "normalize x = (case x of a\<^sub>3 \<Rightarrow> a\<^sub>2 | _ \<Rightarrow> x)"
    1.85  definition [simp]: "unit_factor = (id :: finite_3 \<Rightarrow> _)"
    1.86 -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.87 -instance
    1.88 -  by standard
    1.89 -    (auto simp add: finite_3_not_eq_unfold plus_finite_3_def
    1.90 -      dvd_finite_3_unfold times_finite_3_def inverse_finite_3_def
    1.91 -      normalize_finite_3_def divide_finite_3_def modulo_finite_3_def
    1.92 -      split: finite_3.splits)
    1.93 +definition [simp]: "euclidean_size x = (case x of a\<^sub>1 \<Rightarrow> 0 | _ \<Rightarrow> 1)"
    1.94 +definition [simp]: "uniqueness_constraint = (\<top> :: finite_3 \<Rightarrow> _)"
    1.95 +instance proof
    1.96 +  fix x :: finite_3
    1.97 +  assume "x \<noteq> 0"
    1.98 +  then show "is_unit (unit_factor x)"
    1.99 +    by (cases x) (simp_all add: dvd_finite_3_unfold)
   1.100 +qed (auto simp add: divide_finite_3_def times_finite_3_def
   1.101 +  dvd_finite_3_unfold inverse_finite_3_def plus_finite_3_def
   1.102 +  split: finite_3.splits)
   1.103  end
   1.104  
   1.105 -
   1.106 -
   1.107  hide_const (open) a\<^sub>1 a\<^sub>2 a\<^sub>3
   1.108  
   1.109  datatype (plugins only: code "quickcheck" extraction) finite_4 =