add algebraic type class instances for Enum.finite* types
authorAndreas Lochbihler
Wed Aug 13 17:17:51 2014 +0200 (2014-08-13)
changeset 57922dc78785427d0
parent 57921 9225b2761126
child 57930 3b4deb99a932
add algebraic type class instances for Enum.finite* types
src/HOL/Enum.thy
     1.1 --- a/src/HOL/Enum.thy	Wed Aug 13 14:57:16 2014 +0200
     1.2 +++ b/src/HOL/Enum.thy	Wed Aug 13 17:17:51 2014 +0200
     1.3 @@ -537,6 +537,9 @@
     1.4  
     1.5  end
     1.6  
     1.7 +instance finite_1 :: "{dense_linorder, wellorder}"
     1.8 +by intro_classes (simp_all add: less_finite_1_def)
     1.9 +
    1.10  instantiation finite_1 :: complete_lattice
    1.11  begin
    1.12  
    1.13 @@ -555,6 +558,41 @@
    1.14  
    1.15  instance finite_1 :: complete_linorder ..
    1.16  
    1.17 +lemma finite_1_eq: "x = a\<^sub>1"
    1.18 +by(cases x) simp
    1.19 +
    1.20 +simproc_setup finite_1_eq ("x::finite_1") = {*
    1.21 +  fn _ => fn _ => fn ct => case term_of ct of
    1.22 +    Const (@{const_name a\<^sub>1}, _) => NONE
    1.23 +  | _ => SOME (mk_meta_eq @{thm finite_1_eq})
    1.24 +*}
    1.25 +
    1.26 +instantiation finite_1 :: complete_boolean_algebra begin
    1.27 +definition [simp]: "op - = (\<lambda>_ _. a\<^sub>1)"
    1.28 +definition [simp]: "uminus = (\<lambda>_. a\<^sub>1)"
    1.29 +instance by intro_classes simp_all
    1.30 +end
    1.31 +
    1.32 +instantiation finite_1 :: 
    1.33 +  "{linordered_ring_strict, linordered_comm_semiring_strict, ordered_comm_ring,
    1.34 +    ordered_cancel_comm_monoid_diff, comm_monoid_mult, ordered_ring_abs,
    1.35 +    one, Divides.div, sgn_if, inverse}"
    1.36 +begin
    1.37 +definition [simp]: "Groups.zero = a\<^sub>1"
    1.38 +definition [simp]: "Groups.one = a\<^sub>1"
    1.39 +definition [simp]: "op + = (\<lambda>_ _. a\<^sub>1)"
    1.40 +definition [simp]: "op * = (\<lambda>_ _. a\<^sub>1)"
    1.41 +definition [simp]: "op div = (\<lambda>_ _. a\<^sub>1)" 
    1.42 +definition [simp]: "op mod = (\<lambda>_ _. a\<^sub>1)" 
    1.43 +definition [simp]: "abs = (\<lambda>_. a\<^sub>1)"
    1.44 +definition [simp]: "sgn = (\<lambda>_. a\<^sub>1)"
    1.45 +definition [simp]: "inverse = (\<lambda>_. a\<^sub>1)"
    1.46 +definition [simp]: "op / = (\<lambda>_ _. a\<^sub>1)"
    1.47 +
    1.48 +instance by intro_classes(simp_all add: less_finite_1_def)
    1.49 +end
    1.50 +
    1.51 +declare [[simproc del: finite_1_eq]]
    1.52  hide_const (open) a\<^sub>1
    1.53  
    1.54  datatype finite_2 = a\<^sub>1 | a\<^sub>2
    1.55 @@ -602,6 +640,9 @@
    1.56  
    1.57  end
    1.58  
    1.59 +instance finite_2 :: wellorder
    1.60 +by(rule wf_wellorderI)(simp add: less_finite_2_def, intro_classes)
    1.61 +
    1.62  instantiation finite_2 :: complete_lattice
    1.63  begin
    1.64  
    1.65 @@ -638,6 +679,26 @@
    1.66  
    1.67  instance finite_2 :: complete_linorder ..
    1.68  
    1.69 +instantiation finite_2 :: "{field_inverse_zero, abs_if, ring_div, semiring_div_parity, sgn_if}" begin
    1.70 +definition [simp]: "0 = a\<^sub>1"
    1.71 +definition [simp]: "1 = a\<^sub>2"
    1.72 +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.73 +definition "uminus = (\<lambda>x :: finite_2. x)"
    1.74 +definition "op - = (op + :: finite_2 \<Rightarrow> _)"
    1.75 +definition "x * y = (case (x, y) of (a\<^sub>2, a\<^sub>2) \<Rightarrow> a\<^sub>2 | _ \<Rightarrow> a\<^sub>1)"
    1.76 +definition "inverse = (\<lambda>x :: finite_2. x)"
    1.77 +definition "op / = (op * :: finite_2 \<Rightarrow> _)"
    1.78 +definition "abs = (\<lambda>x :: finite_2. x)"
    1.79 +definition "op div = (op / :: finite_2 \<Rightarrow> _)"
    1.80 +definition "x mod y = (case (x, y) of (a\<^sub>2, a\<^sub>1) \<Rightarrow> a\<^sub>2 | _ \<Rightarrow> a\<^sub>1)"
    1.81 +definition "sgn = (\<lambda>x :: finite_2. x)"
    1.82 +instance
    1.83 +by intro_classes
    1.84 +  (simp_all add: plus_finite_2_def uminus_finite_2_def minus_finite_2_def times_finite_2_def
    1.85 +       inverse_finite_2_def divide_finite_2_def abs_finite_2_def div_finite_2_def mod_finite_2_def sgn_finite_2_def
    1.86 +     split: finite_2.splits)
    1.87 +end
    1.88 +
    1.89  hide_const (open) a\<^sub>1 a\<^sub>2
    1.90  
    1.91  datatype finite_3 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3
    1.92 @@ -683,6 +744,13 @@
    1.93  
    1.94  end
    1.95  
    1.96 +instance finite_3 :: wellorder
    1.97 +proof(rule wf_wellorderI)
    1.98 +  have "inv_image less_than (case_finite_3 0 1 2) = {(x, y). x < y}"
    1.99 +    by(auto simp add: less_finite_3_def split: finite_3.splits)
   1.100 +  from this[symmetric] show "wf \<dots>" by simp
   1.101 +qed intro_classes
   1.102 +
   1.103  instantiation finite_3 :: complete_lattice
   1.104  begin
   1.105  
   1.106 @@ -730,6 +798,31 @@
   1.107  
   1.108  instance finite_3 :: complete_linorder ..
   1.109  
   1.110 +instantiation finite_3 :: "{field_inverse_zero, abs_if, ring_div, semiring_div, sgn_if}" begin
   1.111 +definition [simp]: "0 = a\<^sub>1"
   1.112 +definition [simp]: "1 = a\<^sub>2"
   1.113 +definition
   1.114 +  "x + y = (case (x, y) of
   1.115 +     (a\<^sub>1, a\<^sub>1) \<Rightarrow> a\<^sub>1 | (a\<^sub>2, a\<^sub>3) \<Rightarrow> a\<^sub>1 | (a\<^sub>3, a\<^sub>2) \<Rightarrow> a\<^sub>1
   1.116 +   | (a\<^sub>1, a\<^sub>2) \<Rightarrow> a\<^sub>2 | (a\<^sub>2, a\<^sub>1) \<Rightarrow> a\<^sub>2 | (a\<^sub>3, a\<^sub>3) \<Rightarrow> a\<^sub>2
   1.117 +   | _ \<Rightarrow> a\<^sub>3)"
   1.118 +definition "- x = (case x of a\<^sub>1 \<Rightarrow> a\<^sub>1 | a\<^sub>2 \<Rightarrow> a\<^sub>3 | a\<^sub>3 \<Rightarrow> a\<^sub>2)"
   1.119 +definition "x - y = x + (- y :: finite_3)"
   1.120 +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.121 +definition "inverse = (\<lambda>x :: finite_3. x)" 
   1.122 +definition "x / y = x * inverse (y :: finite_3)"
   1.123 +definition "abs = (\<lambda>x :: finite_3. x)"
   1.124 +definition "op div = (op / :: finite_3 \<Rightarrow> _)"
   1.125 +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.126 +definition "sgn = (\<lambda>x. case x of a\<^sub>1 \<Rightarrow> a\<^sub>1 | _ \<Rightarrow> a\<^sub>2)"
   1.127 +instance
   1.128 +by intro_classes
   1.129 +  (simp_all add: plus_finite_3_def uminus_finite_3_def minus_finite_3_def times_finite_3_def
   1.130 +       inverse_finite_3_def divide_finite_3_def abs_finite_3_def div_finite_3_def mod_finite_3_def sgn_finite_3_def
   1.131 +       less_finite_3_def
   1.132 +     split: finite_3.splits)
   1.133 +end
   1.134 +
   1.135  hide_const (open) a\<^sub>1 a\<^sub>2 a\<^sub>3
   1.136  
   1.137  datatype finite_4 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4
   1.138 @@ -823,6 +916,14 @@
   1.139        (auto simp add: inf_finite_4_def Sup_finite_4_def SUP_def split: finite_4.splits split_if_asm)
   1.140  qed
   1.141  
   1.142 +instantiation finite_4 :: complete_boolean_algebra begin
   1.143 +definition "- x = (case x of a\<^sub>1 \<Rightarrow> a\<^sub>4 | a\<^sub>2 \<Rightarrow> a\<^sub>3 | a\<^sub>3 \<Rightarrow> a\<^sub>2 | a\<^sub>4 \<Rightarrow> a\<^sub>1)"
   1.144 +definition "x - y = x \<sqinter> - (y :: finite_4)"
   1.145 +instance
   1.146 +by intro_classes
   1.147 +  (simp_all add: inf_finite_4_def sup_finite_4_def uminus_finite_4_def minus_finite_4_def split: finite_4.splits)
   1.148 +end
   1.149 +
   1.150  hide_const (open) a\<^sub>1 a\<^sub>2 a\<^sub>3 a\<^sub>4
   1.151  
   1.152