src/HOL/Enum.thy
changeset 57818 51aa30c9ee4e
parent 57247 8191ccf6a1bd
child 57922 dc78785427d0
     1.1 --- a/src/HOL/Enum.thy	Fri Aug 08 08:26:32 2014 +0200
     1.2 +++ b/src/HOL/Enum.thy	Fri Aug 08 17:36:08 2014 +0200
     1.3 @@ -537,6 +537,24 @@
     1.4  
     1.5  end
     1.6  
     1.7 +instantiation finite_1 :: complete_lattice
     1.8 +begin
     1.9 +
    1.10 +definition [simp]: "Inf = (\<lambda>_. a\<^sub>1)"
    1.11 +definition [simp]: "Sup = (\<lambda>_. a\<^sub>1)"
    1.12 +definition [simp]: "bot = a\<^sub>1"
    1.13 +definition [simp]: "top = a\<^sub>1"
    1.14 +definition [simp]: "inf = (\<lambda>_ _. a\<^sub>1)"
    1.15 +definition [simp]: "sup = (\<lambda>_ _. a\<^sub>1)"
    1.16 +
    1.17 +instance by intro_classes(simp_all add: less_eq_finite_1_def)
    1.18 +end
    1.19 +
    1.20 +instance finite_1 :: complete_distrib_lattice
    1.21 +by intro_classes(simp_all add: INF_def SUP_def)
    1.22 +
    1.23 +instance finite_1 :: complete_linorder ..
    1.24 +
    1.25  hide_const (open) a\<^sub>1
    1.26  
    1.27  datatype finite_2 = a\<^sub>1 | a\<^sub>2
    1.28 @@ -584,6 +602,42 @@
    1.29  
    1.30  end
    1.31  
    1.32 +instantiation finite_2 :: complete_lattice
    1.33 +begin
    1.34 +
    1.35 +definition "\<Sqinter>A = (if a\<^sub>1 \<in> A then a\<^sub>1 else a\<^sub>2)"
    1.36 +definition "\<Squnion>A = (if a\<^sub>2 \<in> A then a\<^sub>2 else a\<^sub>1)"
    1.37 +definition [simp]: "bot = a\<^sub>1"
    1.38 +definition [simp]: "top = a\<^sub>2"
    1.39 +definition "x \<sqinter> y = (if x = a\<^sub>1 \<or> y = a\<^sub>1 then a\<^sub>1 else a\<^sub>2)"
    1.40 +definition "x \<squnion> y = (if x = a\<^sub>2 \<or> y = a\<^sub>2 then a\<^sub>2 else a\<^sub>1)"
    1.41 +
    1.42 +lemma neq_finite_2_a\<^sub>1_iff [simp]: "x \<noteq> a\<^sub>1 \<longleftrightarrow> x = a\<^sub>2"
    1.43 +by(cases x) simp_all
    1.44 +
    1.45 +lemma neq_finite_2_a\<^sub>1_iff' [simp]: "a\<^sub>1 \<noteq> x \<longleftrightarrow> x = a\<^sub>2"
    1.46 +by(cases x) simp_all
    1.47 +
    1.48 +lemma neq_finite_2_a\<^sub>2_iff [simp]: "x \<noteq> a\<^sub>2 \<longleftrightarrow> x = a\<^sub>1"
    1.49 +by(cases x) simp_all
    1.50 +
    1.51 +lemma neq_finite_2_a\<^sub>2_iff' [simp]: "a\<^sub>2 \<noteq> x \<longleftrightarrow> x = a\<^sub>1"
    1.52 +by(cases x) simp_all
    1.53 +
    1.54 +instance
    1.55 +proof
    1.56 +  fix x :: finite_2 and A
    1.57 +  assume "x \<in> A"
    1.58 +  then show "\<Sqinter>A \<le> x" "x \<le> \<Squnion>A"
    1.59 +    by(case_tac [!] x)(auto simp add: less_eq_finite_2_def less_finite_2_def Inf_finite_2_def Sup_finite_2_def)
    1.60 +qed(auto simp add: less_eq_finite_2_def less_finite_2_def inf_finite_2_def sup_finite_2_def Inf_finite_2_def Sup_finite_2_def)
    1.61 +end
    1.62 +
    1.63 +instance finite_2 :: complete_distrib_lattice
    1.64 +by(intro_classes)(auto simp add: INF_def SUP_def sup_finite_2_def inf_finite_2_def Inf_finite_2_def Sup_finite_2_def)
    1.65 +
    1.66 +instance finite_2 :: complete_linorder ..
    1.67 +
    1.68  hide_const (open) a\<^sub>1 a\<^sub>2
    1.69  
    1.70  datatype finite_3 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3
    1.71 @@ -629,6 +683,53 @@
    1.72  
    1.73  end
    1.74  
    1.75 +instantiation finite_3 :: complete_lattice
    1.76 +begin
    1.77 +
    1.78 +definition "\<Sqinter>A = (if a\<^sub>1 \<in> A then a\<^sub>1 else if a\<^sub>2 \<in> A then a\<^sub>2 else a\<^sub>3)"
    1.79 +definition "\<Squnion>A = (if a\<^sub>3 \<in> A then a\<^sub>3 else if a\<^sub>2 \<in> A then a\<^sub>2 else a\<^sub>1)"
    1.80 +definition [simp]: "bot = a\<^sub>1"
    1.81 +definition [simp]: "top = a\<^sub>3"
    1.82 +definition [simp]: "inf = (min :: finite_3 \<Rightarrow> _)"
    1.83 +definition [simp]: "sup = (max :: finite_3 \<Rightarrow> _)"
    1.84 +
    1.85 +instance
    1.86 +proof
    1.87 +  fix x :: finite_3 and A
    1.88 +  assume "x \<in> A"
    1.89 +  then show "\<Sqinter>A \<le> x" "x \<le> \<Squnion>A"
    1.90 +    by(case_tac [!] x)(auto simp add: Inf_finite_3_def Sup_finite_3_def less_eq_finite_3_def less_finite_3_def)
    1.91 +next
    1.92 +  fix A and z :: finite_3
    1.93 +  assume "\<And>x. x \<in> A \<Longrightarrow> z \<le> x"
    1.94 +  then show "z \<le> \<Sqinter>A"
    1.95 +    by(cases z)(auto simp add: Inf_finite_3_def less_eq_finite_3_def less_finite_3_def)
    1.96 +next
    1.97 +  fix A and z :: finite_3
    1.98 +  assume *: "\<And>x. x \<in> A \<Longrightarrow> x \<le> z"
    1.99 +  show "\<Squnion>A \<le> z"
   1.100 +    by(auto simp add: Sup_finite_3_def less_eq_finite_3_def less_finite_3_def dest: *)
   1.101 +qed(auto simp add: Inf_finite_3_def Sup_finite_3_def)
   1.102 +end
   1.103 +
   1.104 +instance finite_3 :: complete_distrib_lattice
   1.105 +proof
   1.106 +  fix a :: finite_3 and B
   1.107 +  show "a \<squnion> \<Sqinter>B = (\<Sqinter>b\<in>B. a \<squnion> b)"
   1.108 +  proof(cases a "\<Sqinter>B" rule: finite_3.exhaust[case_product finite_3.exhaust])
   1.109 +    case a\<^sub>2_a\<^sub>3
   1.110 +    then have "\<And>x. x \<in> B \<Longrightarrow> x = a\<^sub>3"
   1.111 +      by(case_tac x)(auto simp add: Inf_finite_3_def split: split_if_asm)
   1.112 +    then show ?thesis using a\<^sub>2_a\<^sub>3
   1.113 +      by(auto simp add: INF_def Inf_finite_3_def max_def less_eq_finite_3_def less_finite_3_def split: split_if_asm)
   1.114 +  qed(auto simp add: INF_def Inf_finite_3_def max_def less_finite_3_def less_eq_finite_3_def split: split_if_asm)
   1.115 +  show "a \<sqinter> \<Squnion>B = (\<Squnion>b\<in>B. a \<sqinter> b)"
   1.116 +    by(cases a "\<Squnion>B" rule: finite_3.exhaust[case_product finite_3.exhaust])
   1.117 +      (auto simp add: SUP_def Sup_finite_3_def min_def less_finite_3_def less_eq_finite_3_def split: split_if_asm)
   1.118 +qed
   1.119 +
   1.120 +instance finite_3 :: complete_linorder ..
   1.121 +
   1.122  hide_const (open) a\<^sub>1 a\<^sub>2 a\<^sub>3
   1.123  
   1.124  datatype finite_4 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4
   1.125 @@ -659,6 +760,69 @@
   1.126  
   1.127  end
   1.128  
   1.129 +instantiation finite_4 :: complete_lattice begin
   1.130 +
   1.131 +text {* @{term a\<^sub>1} $<$ @{term a\<^sub>2},@{term a\<^sub>3} $<$ @{term a\<^sub>4},
   1.132 +  but @{term a\<^sub>2} and @{term a\<^sub>3} are incomparable. *}
   1.133 +
   1.134 +definition
   1.135 +  "x < y \<longleftrightarrow> (case (x, y) of
   1.136 +     (a\<^sub>1, a\<^sub>1) \<Rightarrow> False | (a\<^sub>1, _) \<Rightarrow> True
   1.137 +   |  (a\<^sub>2, a\<^sub>4) \<Rightarrow> True
   1.138 +   |  (a\<^sub>3, a\<^sub>4) \<Rightarrow> True  | _ \<Rightarrow> False)"
   1.139 +
   1.140 +definition 
   1.141 +  "x \<le> y \<longleftrightarrow> (case (x, y) of
   1.142 +     (a\<^sub>1, _) \<Rightarrow> True
   1.143 +   | (a\<^sub>2, a\<^sub>2) \<Rightarrow> True | (a\<^sub>2, a\<^sub>4) \<Rightarrow> True
   1.144 +   | (a\<^sub>3, a\<^sub>3) \<Rightarrow> True | (a\<^sub>3, a\<^sub>4) \<Rightarrow> True
   1.145 +   | (a\<^sub>4, a\<^sub>4) \<Rightarrow> True | _ \<Rightarrow> False)"
   1.146 +
   1.147 +definition
   1.148 +  "\<Sqinter>A = (if a\<^sub>1 \<in> A \<or> a\<^sub>2 \<in> A \<and> a\<^sub>3 \<in> A then a\<^sub>1 else if a\<^sub>2 \<in> A then a\<^sub>2 else if a\<^sub>3 \<in> A then a\<^sub>3 else a\<^sub>4)"
   1.149 +definition
   1.150 +  "\<Squnion>A = (if a\<^sub>4 \<in> A \<or> a\<^sub>2 \<in> A \<and> a\<^sub>3 \<in> A then a\<^sub>4 else if a\<^sub>2 \<in> A then a\<^sub>2 else if a\<^sub>3 \<in> A then a\<^sub>3 else a\<^sub>1)"
   1.151 +definition [simp]: "bot = a\<^sub>1"
   1.152 +definition [simp]: "top = a\<^sub>4"
   1.153 +definition
   1.154 +  "x \<sqinter> y = (case (x, y) of
   1.155 +     (a\<^sub>1, _) \<Rightarrow> 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.156 +   | (a\<^sub>2, _) \<Rightarrow> a\<^sub>2 | (_, a\<^sub>2) \<Rightarrow> a\<^sub>2
   1.157 +   | (a\<^sub>3, _) \<Rightarrow> a\<^sub>3 | (_, a\<^sub>3) \<Rightarrow> a\<^sub>3
   1.158 +   | _ \<Rightarrow> a\<^sub>4)"
   1.159 +definition
   1.160 +  "x \<squnion> y = (case (x, y) of
   1.161 +     (a\<^sub>4, _) \<Rightarrow> a\<^sub>4 | (_, a\<^sub>4) \<Rightarrow> a\<^sub>4 | (a\<^sub>2, a\<^sub>3) \<Rightarrow> a\<^sub>4 | (a\<^sub>3, a\<^sub>2) \<Rightarrow> a\<^sub>4
   1.162 +  | (a\<^sub>2, _) \<Rightarrow> a\<^sub>2 | (_, a\<^sub>2) \<Rightarrow> a\<^sub>2
   1.163 +  | (a\<^sub>3, _) \<Rightarrow> a\<^sub>3 | (_, a\<^sub>3) \<Rightarrow> a\<^sub>3
   1.164 +  | _ \<Rightarrow> a\<^sub>1)"
   1.165 +
   1.166 +instance
   1.167 +proof
   1.168 +  fix A and z :: finite_4
   1.169 +  assume *: "\<And>x. x \<in> A \<Longrightarrow> x \<le> z"
   1.170 +  show "\<Squnion>A \<le> z"
   1.171 +    by(auto simp add: Sup_finite_4_def less_eq_finite_4_def dest!: * split: finite_4.splits)
   1.172 +next
   1.173 +  fix A and z :: finite_4
   1.174 +  assume *: "\<And>x. x \<in> A \<Longrightarrow> z \<le> x"
   1.175 +  show "z \<le> \<Sqinter>A"
   1.176 +    by(auto simp add: Inf_finite_4_def less_eq_finite_4_def dest!: * split: finite_4.splits)
   1.177 +qed(auto simp add: less_finite_4_def less_eq_finite_4_def Inf_finite_4_def Sup_finite_4_def inf_finite_4_def sup_finite_4_def split: finite_4.splits)
   1.178 +
   1.179 +end
   1.180 +
   1.181 +instance finite_4 :: complete_distrib_lattice
   1.182 +proof
   1.183 +  fix a :: finite_4 and B
   1.184 +  show "a \<squnion> \<Sqinter>B = (\<Sqinter>b\<in>B. a \<squnion> b)"
   1.185 +    by(cases a "\<Sqinter>B" rule: finite_4.exhaust[case_product finite_4.exhaust])
   1.186 +      (auto simp add: sup_finite_4_def Inf_finite_4_def INF_def split: finite_4.splits split_if_asm)
   1.187 +  show "a \<sqinter> \<Squnion>B = (\<Squnion>b\<in>B. a \<sqinter> b)"
   1.188 +    by(cases a "\<Squnion>B" rule: finite_4.exhaust[case_product finite_4.exhaust])
   1.189 +      (auto simp add: inf_finite_4_def Sup_finite_4_def SUP_def split: finite_4.splits split_if_asm)
   1.190 +qed
   1.191 +
   1.192  hide_const (open) a\<^sub>1 a\<^sub>2 a\<^sub>3 a\<^sub>4
   1.193  
   1.194  
   1.195 @@ -691,6 +855,72 @@
   1.196  
   1.197  end
   1.198  
   1.199 +instantiation finite_5 :: complete_lattice
   1.200 +begin
   1.201 +
   1.202 +text {* The non-distributive pentagon lattice $N_5$ *}
   1.203 +
   1.204 +definition
   1.205 +  "x < y \<longleftrightarrow> (case (x, y) of
   1.206 +     (a\<^sub>1, a\<^sub>1) \<Rightarrow> False | (a\<^sub>1, _) \<Rightarrow> True
   1.207 +   | (a\<^sub>2, a\<^sub>3) \<Rightarrow> True  | (a\<^sub>2, a\<^sub>5) \<Rightarrow> True
   1.208 +   | (a\<^sub>3, a\<^sub>5) \<Rightarrow> True
   1.209 +   | (a\<^sub>4, a\<^sub>5) \<Rightarrow> True  | _ \<Rightarrow> False)"
   1.210 +
   1.211 +definition
   1.212 +  "x \<le> y \<longleftrightarrow> (case (x, y) of
   1.213 +     (a\<^sub>1, _) \<Rightarrow> True
   1.214 +   | (a\<^sub>2, a\<^sub>2) \<Rightarrow> True | (a\<^sub>2, a\<^sub>3) \<Rightarrow> True | (a\<^sub>2, a\<^sub>5) \<Rightarrow> True
   1.215 +   | (a\<^sub>3, a\<^sub>3) \<Rightarrow> True | (a\<^sub>3, a\<^sub>5) \<Rightarrow> True
   1.216 +   | (a\<^sub>4, a\<^sub>4) \<Rightarrow> True | (a\<^sub>4, a\<^sub>5) \<Rightarrow> True
   1.217 +   | (a\<^sub>5, a\<^sub>5) \<Rightarrow> True | _ \<Rightarrow> False)"
   1.218 +
   1.219 +definition
   1.220 +  "\<Sqinter>A = 
   1.221 +  (if a\<^sub>1 \<in> A \<or> a\<^sub>4 \<in> A \<and> (a\<^sub>2 \<in> A \<or> a\<^sub>3 \<in> A) then a\<^sub>1
   1.222 +   else if a\<^sub>2 \<in> A then a\<^sub>2
   1.223 +   else if a\<^sub>3 \<in> A then a\<^sub>3
   1.224 +   else if a\<^sub>4 \<in> A then a\<^sub>4
   1.225 +   else a\<^sub>5)"
   1.226 +definition
   1.227 +  "\<Squnion>A = 
   1.228 +  (if a\<^sub>5 \<in> A \<or> a\<^sub>4 \<in> A \<and> (a\<^sub>2 \<in> A \<or> a\<^sub>3 \<in> A) then a\<^sub>5
   1.229 +   else if a\<^sub>3 \<in> A then a\<^sub>3
   1.230 +   else if a\<^sub>2 \<in> A then a\<^sub>2
   1.231 +   else if a\<^sub>4 \<in> A then a\<^sub>4
   1.232 +   else a\<^sub>1)"
   1.233 +definition [simp]: "bot = a\<^sub>1"
   1.234 +definition [simp]: "top = a\<^sub>5"
   1.235 +definition
   1.236 +  "x \<sqinter> y = (case (x, y) of
   1.237 +     (a\<^sub>1, _) \<Rightarrow> a\<^sub>1 | (_, a\<^sub>1) \<Rightarrow> a\<^sub>1 | (a\<^sub>2, a\<^sub>4) \<Rightarrow> a\<^sub>1 | (a\<^sub>4, a\<^sub>2) \<Rightarrow> a\<^sub>1 | (a\<^sub>3, a\<^sub>4) \<Rightarrow> a\<^sub>1 | (a\<^sub>4, a\<^sub>3) \<Rightarrow> a\<^sub>1
   1.238 +   | (a\<^sub>2, _) \<Rightarrow> a\<^sub>2 | (_, a\<^sub>2) \<Rightarrow> a\<^sub>2
   1.239 +   | (a\<^sub>3, _) \<Rightarrow> a\<^sub>3 | (_, a\<^sub>3) \<Rightarrow> a\<^sub>3
   1.240 +   | (a\<^sub>4, _) \<Rightarrow> a\<^sub>4 | (_, a\<^sub>4) \<Rightarrow> a\<^sub>4
   1.241 +   | _ \<Rightarrow> a\<^sub>5)"
   1.242 +definition
   1.243 +  "x \<squnion> y = (case (x, y) of
   1.244 +     (a\<^sub>5, _) \<Rightarrow> a\<^sub>5 | (_, a\<^sub>5) \<Rightarrow> a\<^sub>5 | (a\<^sub>2, a\<^sub>4) \<Rightarrow> a\<^sub>5 | (a\<^sub>4, a\<^sub>2) \<Rightarrow> a\<^sub>5 | (a\<^sub>3, a\<^sub>4) \<Rightarrow> a\<^sub>5 | (a\<^sub>4, a\<^sub>3) \<Rightarrow> a\<^sub>5
   1.245 +   | (a\<^sub>3, _) \<Rightarrow> a\<^sub>3 | (_, a\<^sub>3) \<Rightarrow> a\<^sub>3
   1.246 +   | (a\<^sub>2, _) \<Rightarrow> a\<^sub>2 | (_, a\<^sub>2) \<Rightarrow> a\<^sub>2
   1.247 +   | (a\<^sub>4, _) \<Rightarrow> a\<^sub>4 | (_, a\<^sub>4) \<Rightarrow> a\<^sub>4
   1.248 +   | _ \<Rightarrow> a\<^sub>1)"
   1.249 +
   1.250 +instance 
   1.251 +proof intro_classes
   1.252 +  fix A and z :: finite_5
   1.253 +  assume *: "\<And>x. x \<in> A \<Longrightarrow> z \<le> x"
   1.254 +  show "z \<le> \<Sqinter>A"
   1.255 +    by(auto simp add: less_eq_finite_5_def Inf_finite_5_def split: finite_5.splits split_if_asm dest!: *)
   1.256 +next
   1.257 +  fix A and z :: finite_5
   1.258 +  assume *: "\<And>x. x \<in> A \<Longrightarrow> x \<le> z"
   1.259 +  show "\<Squnion>A \<le> z"
   1.260 +    by(auto simp add: less_eq_finite_5_def Sup_finite_5_def split: finite_5.splits split_if_asm dest!: *)
   1.261 +qed(auto simp add: less_eq_finite_5_def less_finite_5_def inf_finite_5_def sup_finite_5_def Inf_finite_5_def Sup_finite_5_def split: finite_5.splits split_if_asm)
   1.262 +
   1.263 +end
   1.264 +
   1.265  hide_const (open) a\<^sub>1 a\<^sub>2 a\<^sub>3 a\<^sub>4 a\<^sub>5
   1.266  
   1.267