--- a/src/HOL/Enum.thy Fri Aug 08 08:26:32 2014 +0200
+++ b/src/HOL/Enum.thy Fri Aug 08 17:36:08 2014 +0200
@@ -537,6 +537,24 @@
end
+instantiation finite_1 :: complete_lattice
+begin
+
+definition [simp]: "Inf = (\<lambda>_. a\<^sub>1)"
+definition [simp]: "Sup = (\<lambda>_. a\<^sub>1)"
+definition [simp]: "bot = a\<^sub>1"
+definition [simp]: "top = a\<^sub>1"
+definition [simp]: "inf = (\<lambda>_ _. a\<^sub>1)"
+definition [simp]: "sup = (\<lambda>_ _. a\<^sub>1)"
+
+instance by intro_classes(simp_all add: less_eq_finite_1_def)
+end
+
+instance finite_1 :: complete_distrib_lattice
+by intro_classes(simp_all add: INF_def SUP_def)
+
+instance finite_1 :: complete_linorder ..
+
hide_const (open) a\<^sub>1
datatype finite_2 = a\<^sub>1 | a\<^sub>2
@@ -584,6 +602,42 @@
end
+instantiation finite_2 :: complete_lattice
+begin
+
+definition "\<Sqinter>A = (if a\<^sub>1 \<in> A then a\<^sub>1 else a\<^sub>2)"
+definition "\<Squnion>A = (if a\<^sub>2 \<in> A then a\<^sub>2 else a\<^sub>1)"
+definition [simp]: "bot = a\<^sub>1"
+definition [simp]: "top = a\<^sub>2"
+definition "x \<sqinter> y = (if x = a\<^sub>1 \<or> y = a\<^sub>1 then a\<^sub>1 else a\<^sub>2)"
+definition "x \<squnion> y = (if x = a\<^sub>2 \<or> y = a\<^sub>2 then a\<^sub>2 else a\<^sub>1)"
+
+lemma neq_finite_2_a\<^sub>1_iff [simp]: "x \<noteq> a\<^sub>1 \<longleftrightarrow> x = a\<^sub>2"
+by(cases x) simp_all
+
+lemma neq_finite_2_a\<^sub>1_iff' [simp]: "a\<^sub>1 \<noteq> x \<longleftrightarrow> x = a\<^sub>2"
+by(cases x) simp_all
+
+lemma neq_finite_2_a\<^sub>2_iff [simp]: "x \<noteq> a\<^sub>2 \<longleftrightarrow> x = a\<^sub>1"
+by(cases x) simp_all
+
+lemma neq_finite_2_a\<^sub>2_iff' [simp]: "a\<^sub>2 \<noteq> x \<longleftrightarrow> x = a\<^sub>1"
+by(cases x) simp_all
+
+instance
+proof
+ fix x :: finite_2 and A
+ assume "x \<in> A"
+ then show "\<Sqinter>A \<le> x" "x \<le> \<Squnion>A"
+ by(case_tac [!] x)(auto simp add: less_eq_finite_2_def less_finite_2_def Inf_finite_2_def Sup_finite_2_def)
+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)
+end
+
+instance finite_2 :: complete_distrib_lattice
+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)
+
+instance finite_2 :: complete_linorder ..
+
hide_const (open) a\<^sub>1 a\<^sub>2
datatype finite_3 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3
@@ -629,6 +683,53 @@
end
+instantiation finite_3 :: complete_lattice
+begin
+
+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)"
+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)"
+definition [simp]: "bot = a\<^sub>1"
+definition [simp]: "top = a\<^sub>3"
+definition [simp]: "inf = (min :: finite_3 \<Rightarrow> _)"
+definition [simp]: "sup = (max :: finite_3 \<Rightarrow> _)"
+
+instance
+proof
+ fix x :: finite_3 and A
+ assume "x \<in> A"
+ then show "\<Sqinter>A \<le> x" "x \<le> \<Squnion>A"
+ by(case_tac [!] x)(auto simp add: Inf_finite_3_def Sup_finite_3_def less_eq_finite_3_def less_finite_3_def)
+next
+ fix A and z :: finite_3
+ assume "\<And>x. x \<in> A \<Longrightarrow> z \<le> x"
+ then show "z \<le> \<Sqinter>A"
+ by(cases z)(auto simp add: Inf_finite_3_def less_eq_finite_3_def less_finite_3_def)
+next
+ fix A and z :: finite_3
+ assume *: "\<And>x. x \<in> A \<Longrightarrow> x \<le> z"
+ show "\<Squnion>A \<le> z"
+ by(auto simp add: Sup_finite_3_def less_eq_finite_3_def less_finite_3_def dest: *)
+qed(auto simp add: Inf_finite_3_def Sup_finite_3_def)
+end
+
+instance finite_3 :: complete_distrib_lattice
+proof
+ fix a :: finite_3 and B
+ show "a \<squnion> \<Sqinter>B = (\<Sqinter>b\<in>B. a \<squnion> b)"
+ proof(cases a "\<Sqinter>B" rule: finite_3.exhaust[case_product finite_3.exhaust])
+ case a\<^sub>2_a\<^sub>3
+ then have "\<And>x. x \<in> B \<Longrightarrow> x = a\<^sub>3"
+ by(case_tac x)(auto simp add: Inf_finite_3_def split: split_if_asm)
+ then show ?thesis using a\<^sub>2_a\<^sub>3
+ 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)
+ 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)
+ show "a \<sqinter> \<Squnion>B = (\<Squnion>b\<in>B. a \<sqinter> b)"
+ by(cases a "\<Squnion>B" rule: finite_3.exhaust[case_product finite_3.exhaust])
+ (auto simp add: SUP_def Sup_finite_3_def min_def less_finite_3_def less_eq_finite_3_def split: split_if_asm)
+qed
+
+instance finite_3 :: complete_linorder ..
+
hide_const (open) a\<^sub>1 a\<^sub>2 a\<^sub>3
datatype finite_4 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4
@@ -659,6 +760,69 @@
end
+instantiation finite_4 :: complete_lattice begin
+
+text {* @{term a\<^sub>1} $<$ @{term a\<^sub>2},@{term a\<^sub>3} $<$ @{term a\<^sub>4},
+ but @{term a\<^sub>2} and @{term a\<^sub>3} are incomparable. *}
+
+definition
+ "x < y \<longleftrightarrow> (case (x, y) of
+ (a\<^sub>1, a\<^sub>1) \<Rightarrow> False | (a\<^sub>1, _) \<Rightarrow> True
+ | (a\<^sub>2, a\<^sub>4) \<Rightarrow> True
+ | (a\<^sub>3, a\<^sub>4) \<Rightarrow> True | _ \<Rightarrow> False)"
+
+definition
+ "x \<le> y \<longleftrightarrow> (case (x, y) of
+ (a\<^sub>1, _) \<Rightarrow> True
+ | (a\<^sub>2, a\<^sub>2) \<Rightarrow> True | (a\<^sub>2, a\<^sub>4) \<Rightarrow> True
+ | (a\<^sub>3, a\<^sub>3) \<Rightarrow> True | (a\<^sub>3, a\<^sub>4) \<Rightarrow> True
+ | (a\<^sub>4, a\<^sub>4) \<Rightarrow> True | _ \<Rightarrow> False)"
+
+definition
+ "\<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)"
+definition
+ "\<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)"
+definition [simp]: "bot = a\<^sub>1"
+definition [simp]: "top = a\<^sub>4"
+definition
+ "x \<sqinter> y = (case (x, y) of
+ (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
+ | (a\<^sub>2, _) \<Rightarrow> a\<^sub>2 | (_, a\<^sub>2) \<Rightarrow> a\<^sub>2
+ | (a\<^sub>3, _) \<Rightarrow> a\<^sub>3 | (_, a\<^sub>3) \<Rightarrow> a\<^sub>3
+ | _ \<Rightarrow> a\<^sub>4)"
+definition
+ "x \<squnion> y = (case (x, y) of
+ (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
+ | (a\<^sub>2, _) \<Rightarrow> a\<^sub>2 | (_, a\<^sub>2) \<Rightarrow> a\<^sub>2
+ | (a\<^sub>3, _) \<Rightarrow> a\<^sub>3 | (_, a\<^sub>3) \<Rightarrow> a\<^sub>3
+ | _ \<Rightarrow> a\<^sub>1)"
+
+instance
+proof
+ fix A and z :: finite_4
+ assume *: "\<And>x. x \<in> A \<Longrightarrow> x \<le> z"
+ show "\<Squnion>A \<le> z"
+ by(auto simp add: Sup_finite_4_def less_eq_finite_4_def dest!: * split: finite_4.splits)
+next
+ fix A and z :: finite_4
+ assume *: "\<And>x. x \<in> A \<Longrightarrow> z \<le> x"
+ show "z \<le> \<Sqinter>A"
+ by(auto simp add: Inf_finite_4_def less_eq_finite_4_def dest!: * split: finite_4.splits)
+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)
+
+end
+
+instance finite_4 :: complete_distrib_lattice
+proof
+ fix a :: finite_4 and B
+ show "a \<squnion> \<Sqinter>B = (\<Sqinter>b\<in>B. a \<squnion> b)"
+ by(cases a "\<Sqinter>B" rule: finite_4.exhaust[case_product finite_4.exhaust])
+ (auto simp add: sup_finite_4_def Inf_finite_4_def INF_def split: finite_4.splits split_if_asm)
+ show "a \<sqinter> \<Squnion>B = (\<Squnion>b\<in>B. a \<sqinter> b)"
+ by(cases a "\<Squnion>B" rule: finite_4.exhaust[case_product finite_4.exhaust])
+ (auto simp add: inf_finite_4_def Sup_finite_4_def SUP_def split: finite_4.splits split_if_asm)
+qed
+
hide_const (open) a\<^sub>1 a\<^sub>2 a\<^sub>3 a\<^sub>4
@@ -691,6 +855,72 @@
end
+instantiation finite_5 :: complete_lattice
+begin
+
+text {* The non-distributive pentagon lattice $N_5$ *}
+
+definition
+ "x < y \<longleftrightarrow> (case (x, y) of
+ (a\<^sub>1, a\<^sub>1) \<Rightarrow> False | (a\<^sub>1, _) \<Rightarrow> True
+ | (a\<^sub>2, a\<^sub>3) \<Rightarrow> True | (a\<^sub>2, a\<^sub>5) \<Rightarrow> True
+ | (a\<^sub>3, a\<^sub>5) \<Rightarrow> True
+ | (a\<^sub>4, a\<^sub>5) \<Rightarrow> True | _ \<Rightarrow> False)"
+
+definition
+ "x \<le> y \<longleftrightarrow> (case (x, y) of
+ (a\<^sub>1, _) \<Rightarrow> True
+ | (a\<^sub>2, a\<^sub>2) \<Rightarrow> True | (a\<^sub>2, a\<^sub>3) \<Rightarrow> True | (a\<^sub>2, a\<^sub>5) \<Rightarrow> True
+ | (a\<^sub>3, a\<^sub>3) \<Rightarrow> True | (a\<^sub>3, a\<^sub>5) \<Rightarrow> True
+ | (a\<^sub>4, a\<^sub>4) \<Rightarrow> True | (a\<^sub>4, a\<^sub>5) \<Rightarrow> True
+ | (a\<^sub>5, a\<^sub>5) \<Rightarrow> True | _ \<Rightarrow> False)"
+
+definition
+ "\<Sqinter>A =
+ (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
+ else if a\<^sub>2 \<in> A then a\<^sub>2
+ else if a\<^sub>3 \<in> A then a\<^sub>3
+ else if a\<^sub>4 \<in> A then a\<^sub>4
+ else a\<^sub>5)"
+definition
+ "\<Squnion>A =
+ (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
+ else if a\<^sub>3 \<in> A then a\<^sub>3
+ else if a\<^sub>2 \<in> A then a\<^sub>2
+ else if a\<^sub>4 \<in> A then a\<^sub>4
+ else a\<^sub>1)"
+definition [simp]: "bot = a\<^sub>1"
+definition [simp]: "top = a\<^sub>5"
+definition
+ "x \<sqinter> y = (case (x, y) of
+ (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
+ | (a\<^sub>2, _) \<Rightarrow> a\<^sub>2 | (_, a\<^sub>2) \<Rightarrow> a\<^sub>2
+ | (a\<^sub>3, _) \<Rightarrow> a\<^sub>3 | (_, a\<^sub>3) \<Rightarrow> a\<^sub>3
+ | (a\<^sub>4, _) \<Rightarrow> a\<^sub>4 | (_, a\<^sub>4) \<Rightarrow> a\<^sub>4
+ | _ \<Rightarrow> a\<^sub>5)"
+definition
+ "x \<squnion> y = (case (x, y) of
+ (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
+ | (a\<^sub>3, _) \<Rightarrow> a\<^sub>3 | (_, a\<^sub>3) \<Rightarrow> a\<^sub>3
+ | (a\<^sub>2, _) \<Rightarrow> a\<^sub>2 | (_, a\<^sub>2) \<Rightarrow> a\<^sub>2
+ | (a\<^sub>4, _) \<Rightarrow> a\<^sub>4 | (_, a\<^sub>4) \<Rightarrow> a\<^sub>4
+ | _ \<Rightarrow> a\<^sub>1)"
+
+instance
+proof intro_classes
+ fix A and z :: finite_5
+ assume *: "\<And>x. x \<in> A \<Longrightarrow> z \<le> x"
+ show "z \<le> \<Sqinter>A"
+ by(auto simp add: less_eq_finite_5_def Inf_finite_5_def split: finite_5.splits split_if_asm dest!: *)
+next
+ fix A and z :: finite_5
+ assume *: "\<And>x. x \<in> A \<Longrightarrow> x \<le> z"
+ show "\<Squnion>A \<le> z"
+ by(auto simp add: less_eq_finite_5_def Sup_finite_5_def split: finite_5.splits split_if_asm dest!: *)
+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)
+
+end
+
hide_const (open) a\<^sub>1 a\<^sub>2 a\<^sub>3 a\<^sub>4 a\<^sub>5