(* Title: HOL/Library/Lattice_Constructions.thy
Author: Lukas Bulwahn
Copyright 2010 TU Muenchen
*)
theory Lattice_Constructions
imports Main
begin
subsection \<open>Values extended by a bottom element\<close>
datatype 'a bot = Value 'a | Bot
instantiation bot :: (preorder) preorder
begin
definition less_eq_bot where
"x \<le> y \<longleftrightarrow> (case x of Bot \<Rightarrow> True | Value x \<Rightarrow> (case y of Bot \<Rightarrow> False | Value y \<Rightarrow> x \<le> y))"
definition less_bot where
"x < y \<longleftrightarrow> (case y of Bot \<Rightarrow> False | Value y \<Rightarrow> (case x of Bot \<Rightarrow> True | Value x \<Rightarrow> x < y))"
lemma less_eq_bot_Bot [simp]: "Bot \<le> x"
by (simp add: less_eq_bot_def)
lemma less_eq_bot_Bot_code [code]: "Bot \<le> x \<longleftrightarrow> True"
by simp
lemma less_eq_bot_Bot_is_Bot: "x \<le> Bot \<Longrightarrow> x = Bot"
by (cases x) (simp_all add: less_eq_bot_def)
lemma less_eq_bot_Value_Bot [simp, code]: "Value x \<le> Bot \<longleftrightarrow> False"
by (simp add: less_eq_bot_def)
lemma less_eq_bot_Value [simp, code]: "Value x \<le> Value y \<longleftrightarrow> x \<le> y"
by (simp add: less_eq_bot_def)
lemma less_bot_Bot [simp, code]: "x < Bot \<longleftrightarrow> False"
by (simp add: less_bot_def)
lemma less_bot_Bot_is_Value: "Bot < x \<Longrightarrow> \<exists>z. x = Value z"
by (cases x) (simp_all add: less_bot_def)
lemma less_bot_Bot_Value [simp]: "Bot < Value x"
by (simp add: less_bot_def)
lemma less_bot_Bot_Value_code [code]: "Bot < Value x \<longleftrightarrow> True"
by simp
lemma less_bot_Value [simp, code]: "Value x < Value y \<longleftrightarrow> x < y"
by (simp add: less_bot_def)
instance
by default
(auto simp add: less_eq_bot_def less_bot_def less_le_not_le elim: order_trans split: bot.splits)
end
instance bot :: (order) order
by default (auto simp add: less_eq_bot_def less_bot_def split: bot.splits)
instance bot :: (linorder) linorder
by default (auto simp add: less_eq_bot_def less_bot_def split: bot.splits)
instantiation bot :: (order) bot
begin
definition "bot = Bot"
instance ..
end
instantiation bot :: (top) top
begin
definition "top = Value top"
instance ..
end
instantiation bot :: (semilattice_inf) semilattice_inf
begin
definition inf_bot
where
"inf x y =
(case x of
Bot \<Rightarrow> Bot
| Value v \<Rightarrow>
(case y of
Bot \<Rightarrow> Bot
| Value v' \<Rightarrow> Value (inf v v')))"
instance
by default (auto simp add: inf_bot_def less_eq_bot_def split: bot.splits)
end
instantiation bot :: (semilattice_sup) semilattice_sup
begin
definition sup_bot
where
"sup x y =
(case x of
Bot \<Rightarrow> y
| Value v \<Rightarrow>
(case y of
Bot \<Rightarrow> x
| Value v' \<Rightarrow> Value (sup v v')))"
instance
by default (auto simp add: sup_bot_def less_eq_bot_def split: bot.splits)
end
instance bot :: (lattice) bounded_lattice_bot
by intro_classes (simp add: bot_bot_def)
subsection \<open>Values extended by a top element\<close>
datatype 'a top = Value 'a | Top
instantiation top :: (preorder) preorder
begin
definition less_eq_top where
"x \<le> y \<longleftrightarrow> (case y of Top \<Rightarrow> True | Value y \<Rightarrow> (case x of Top \<Rightarrow> False | Value x \<Rightarrow> x \<le> y))"
definition less_top where
"x < y \<longleftrightarrow> (case x of Top \<Rightarrow> False | Value x \<Rightarrow> (case y of Top \<Rightarrow> True | Value y \<Rightarrow> x < y))"
lemma less_eq_top_Top [simp]: "x \<le> Top"
by (simp add: less_eq_top_def)
lemma less_eq_top_Top_code [code]: "x \<le> Top \<longleftrightarrow> True"
by simp
lemma less_eq_top_is_Top: "Top \<le> x \<Longrightarrow> x = Top"
by (cases x) (simp_all add: less_eq_top_def)
lemma less_eq_top_Top_Value [simp, code]: "Top \<le> Value x \<longleftrightarrow> False"
by (simp add: less_eq_top_def)
lemma less_eq_top_Value_Value [simp, code]: "Value x \<le> Value y \<longleftrightarrow> x \<le> y"
by (simp add: less_eq_top_def)
lemma less_top_Top [simp, code]: "Top < x \<longleftrightarrow> False"
by (simp add: less_top_def)
lemma less_top_Top_is_Value: "x < Top \<Longrightarrow> \<exists>z. x = Value z"
by (cases x) (simp_all add: less_top_def)
lemma less_top_Value_Top [simp]: "Value x < Top"
by (simp add: less_top_def)
lemma less_top_Value_Top_code [code]: "Value x < Top \<longleftrightarrow> True"
by simp
lemma less_top_Value [simp, code]: "Value x < Value y \<longleftrightarrow> x < y"
by (simp add: less_top_def)
instance
by default
(auto simp add: less_eq_top_def less_top_def less_le_not_le elim: order_trans split: top.splits)
end
instance top :: (order) order
by default (auto simp add: less_eq_top_def less_top_def split: top.splits)
instance top :: (linorder) linorder
by default (auto simp add: less_eq_top_def less_top_def split: top.splits)
instantiation top :: (order) top
begin
definition "top = Top"
instance ..
end
instantiation top :: (bot) bot
begin
definition "bot = Value bot"
instance ..
end
instantiation top :: (semilattice_inf) semilattice_inf
begin
definition inf_top
where
"inf x y =
(case x of
Top \<Rightarrow> y
| Value v \<Rightarrow>
(case y of
Top \<Rightarrow> x
| Value v' \<Rightarrow> Value (inf v v')))"
instance
by default (auto simp add: inf_top_def less_eq_top_def split: top.splits)
end
instantiation top :: (semilattice_sup) semilattice_sup
begin
definition sup_top
where
"sup x y =
(case x of
Top \<Rightarrow> Top
| Value v \<Rightarrow>
(case y of
Top \<Rightarrow> Top
| Value v' \<Rightarrow> Value (sup v v')))"
instance
by default (auto simp add: sup_top_def less_eq_top_def split: top.splits)
end
instance top :: (lattice) bounded_lattice_top
by default (simp add: top_top_def)
subsection \<open>Values extended by a top and a bottom element\<close>
datatype 'a flat_complete_lattice = Value 'a | Bot | Top
instantiation flat_complete_lattice :: (type) order
begin
definition less_eq_flat_complete_lattice
where
"x \<le> y \<equiv>
(case x of
Bot \<Rightarrow> True
| Value v1 \<Rightarrow>
(case y of
Bot \<Rightarrow> False
| Value v2 \<Rightarrow> v1 = v2
| Top \<Rightarrow> True)
| Top \<Rightarrow> y = Top)"
definition less_flat_complete_lattice
where
"x < y =
(case x of
Bot \<Rightarrow> y \<noteq> Bot
| Value v1 \<Rightarrow> y = Top
| Top \<Rightarrow> False)"
lemma [simp]: "Bot \<le> y"
unfolding less_eq_flat_complete_lattice_def by auto
lemma [simp]: "y \<le> Top"
unfolding less_eq_flat_complete_lattice_def by (auto split: flat_complete_lattice.splits)
lemma greater_than_two_values:
assumes "a \<noteq> b" "Value a \<le> z" "Value b \<le> z"
shows "z = Top"
using assms
by (cases z) (auto simp add: less_eq_flat_complete_lattice_def)
lemma lesser_than_two_values:
assumes "a \<noteq> b" "z \<le> Value a" "z \<le> Value b"
shows "z = Bot"
using assms
by (cases z) (auto simp add: less_eq_flat_complete_lattice_def)
instance
by default
(auto simp add: less_eq_flat_complete_lattice_def less_flat_complete_lattice_def
split: flat_complete_lattice.splits)
end
instantiation flat_complete_lattice :: (type) bot
begin
definition "bot = Bot"
instance ..
end
instantiation flat_complete_lattice :: (type) top
begin
definition "top = Top"
instance ..
end
instantiation flat_complete_lattice :: (type) lattice
begin
definition inf_flat_complete_lattice
where
"inf x y =
(case x of
Bot \<Rightarrow> Bot
| Value v1 \<Rightarrow>
(case y of
Bot \<Rightarrow> Bot
| Value v2 \<Rightarrow> if v1 = v2 then x else Bot
| Top \<Rightarrow> x)
| Top \<Rightarrow> y)"
definition sup_flat_complete_lattice
where
"sup x y =
(case x of
Bot \<Rightarrow> y
| Value v1 \<Rightarrow>
(case y of
Bot \<Rightarrow> x
| Value v2 \<Rightarrow> if v1 = v2 then x else Top
| Top \<Rightarrow> Top)
| Top \<Rightarrow> Top)"
instance
by default
(auto simp add: inf_flat_complete_lattice_def sup_flat_complete_lattice_def
less_eq_flat_complete_lattice_def split: flat_complete_lattice.splits)
end
instantiation flat_complete_lattice :: (type) complete_lattice
begin
definition Sup_flat_complete_lattice
where
"Sup A =
(if A = {} \<or> A = {Bot} then Bot
else if \<exists>v. A - {Bot} = {Value v} then Value (THE v. A - {Bot} = {Value v})
else Top)"
definition Inf_flat_complete_lattice
where
"Inf A =
(if A = {} \<or> A = {Top} then Top
else if \<exists>v. A - {Top} = {Value v} then Value (THE v. A - {Top} = {Value v})
else Bot)"
instance
proof
fix x :: "'a flat_complete_lattice"
fix A
assume "x \<in> A"
{
fix v
assume "A - {Top} = {Value v}"
then have "(THE v. A - {Top} = {Value v}) = v"
by (auto intro!: the1_equality)
moreover
from \<open>x \<in> A\<close> \<open>A - {Top} = {Value v}\<close> have "x = Top \<or> x = Value v"
by auto
ultimately have "Value (THE v. A - {Top} = {Value v}) \<le> x"
by auto
}
with \<open>x \<in> A\<close> show "Inf A \<le> x"
unfolding Inf_flat_complete_lattice_def
by fastforce
next
fix z :: "'a flat_complete_lattice"
fix A
show "z \<le> Inf A" if z: "\<And>x. x \<in> A \<Longrightarrow> z \<le> x"
proof -
consider "A = {} \<or> A = {Top}"
| "A \<noteq> {}" "A \<noteq> {Top}" "\<exists>v. A - {Top} = {Value v}"
| "A \<noteq> {}" "A \<noteq> {Top}" "\<not> (\<exists>v. A - {Top} = {Value v})"
by blast
then show ?thesis
proof cases
case 1
then have "Inf A = Top"
unfolding Inf_flat_complete_lattice_def by auto
then show ?thesis by simp
next
case 2
then obtain v where v1: "A - {Top} = {Value v}"
by auto
then have v2: "(THE v. A - {Top} = {Value v}) = v"
by (auto intro!: the1_equality)
from 2 v2 have Inf: "Inf A = Value v"
unfolding Inf_flat_complete_lattice_def by simp
from v1 have "Value v \<in> A" by blast
then have "z \<le> Value v" by (rule z)
with Inf show ?thesis by simp
next
case 3
then have Inf: "Inf A = Bot"
unfolding Inf_flat_complete_lattice_def by auto
have "z \<le> Bot"
proof (cases "A - {Top} = {Bot}")
case True
then have "Bot \<in> A" by blast
then show ?thesis by (rule z)
next
case False
from 3 obtain a1 where a1: "a1 \<in> A - {Top}"
by auto
from 3 False a1 obtain a2 where "a2 \<in> A - {Top} \<and> a1 \<noteq> a2"
by (cases a1) auto
with a1 z[of "a1"] z[of "a2"] show ?thesis
apply (cases a1)
apply auto
apply (cases a2)
apply auto
apply (auto dest!: lesser_than_two_values)
done
qed
with Inf show ?thesis by simp
qed
qed
next
fix x :: "'a flat_complete_lattice"
fix A
assume "x \<in> A"
{
fix v
assume "A - {Bot} = {Value v}"
then have "(THE v. A - {Bot} = {Value v}) = v"
by (auto intro!: the1_equality)
moreover
from \<open>x \<in> A\<close> \<open>A - {Bot} = {Value v}\<close> have "x = Bot \<or> x = Value v"
by auto
ultimately have "x \<le> Value (THE v. A - {Bot} = {Value v})"
by auto
}
with \<open>x \<in> A\<close> show "x \<le> Sup A"
unfolding Sup_flat_complete_lattice_def
by fastforce
next
fix z :: "'a flat_complete_lattice"
fix A
show "Sup A \<le> z" if z: "\<And>x. x \<in> A \<Longrightarrow> x \<le> z"
proof -
consider "A = {} \<or> A = {Bot}"
| "A \<noteq> {}" "A \<noteq> {Bot}" "\<exists>v. A - {Bot} = {Value v}"
| "A \<noteq> {}" "A \<noteq> {Bot}" "\<not> (\<exists>v. A - {Bot} = {Value v})"
by blast
then show ?thesis
proof cases
case 1
then have "Sup A = Bot"
unfolding Sup_flat_complete_lattice_def by auto
then show ?thesis by simp
next
case 2
then obtain v where v1: "A - {Bot} = {Value v}"
by auto
then have v2: "(THE v. A - {Bot} = {Value v}) = v"
by (auto intro!: the1_equality)
from 2 v2 have Sup: "Sup A = Value v"
unfolding Sup_flat_complete_lattice_def by simp
from v1 have "Value v \<in> A" by blast
then have "Value v \<le> z" by (rule z)
with Sup show ?thesis by simp
next
case 3
then have Sup: "Sup A = Top"
unfolding Sup_flat_complete_lattice_def by auto
have "Top \<le> z"
proof (cases "A - {Bot} = {Top}")
case True
then have "Top \<in> A" by blast
then show ?thesis by (rule z)
next
case False
from 3 obtain a1 where a1: "a1 \<in> A - {Bot}"
by auto
from 3 False a1 obtain a2 where "a2 \<in> A - {Bot} \<and> a1 \<noteq> a2"
by (cases a1) auto
with a1 z[of "a1"] z[of "a2"] show ?thesis
apply (cases a1)
apply auto
apply (cases a2)
apply (auto dest!: greater_than_two_values)
done
qed
with Sup show ?thesis by simp
qed
qed
next
show "Inf {} = (top :: 'a flat_complete_lattice)"
by (simp add: Inf_flat_complete_lattice_def top_flat_complete_lattice_def)
show "Sup {} = (bot :: 'a flat_complete_lattice)"
by (simp add: Sup_flat_complete_lattice_def bot_flat_complete_lattice_def)
qed
end
end