section ‹Canonical order on option type›
theory Option_ord
imports Option Main
begin
notation
bot ("⊥") and
top ("⊤") and
inf (infixl "⊓" 70) and
sup (infixl "⊔" 65) and
Inf ("⨅_" [900] 900) and
Sup ("⨆_" [900] 900)
syntax
"_INF1" :: "pttrns ⇒ 'b ⇒ 'b" ("(3⨅_./ _)" [0, 10] 10)
"_INF" :: "pttrn ⇒ 'a set ⇒ 'b ⇒ 'b" ("(3⨅_∈_./ _)" [0, 0, 10] 10)
"_SUP1" :: "pttrns ⇒ 'b ⇒ 'b" ("(3⨆_./ _)" [0, 10] 10)
"_SUP" :: "pttrn ⇒ 'a set ⇒ 'b ⇒ 'b" ("(3⨆_∈_./ _)" [0, 0, 10] 10)
instantiation option :: (preorder) preorder
begin
definition less_eq_option where
"x ≤ y ⟷ (case x of None ⇒ True | Some x ⇒ (case y of None ⇒ False | Some y ⇒ x ≤ y))"
definition less_option where
"x < y ⟷ (case y of None ⇒ False | Some y ⇒ (case x of None ⇒ True | Some x ⇒ x < y))"
lemma less_eq_option_None [simp]: "None ≤ x"
by (simp add: less_eq_option_def)
lemma less_eq_option_None_code [code]: "None ≤ x ⟷ True"
by simp
lemma less_eq_option_None_is_None: "x ≤ None ⟹ x = None"
by (cases x) (simp_all add: less_eq_option_def)
lemma less_eq_option_Some_None [simp, code]: "Some x ≤ None ⟷ False"
by (simp add: less_eq_option_def)
lemma less_eq_option_Some [simp, code]: "Some x ≤ Some y ⟷ x ≤ y"
by (simp add: less_eq_option_def)
lemma less_option_None [simp, code]: "x < None ⟷ False"
by (simp add: less_option_def)
lemma less_option_None_is_Some: "None < x ⟹ ∃z. x = Some z"
by (cases x) (simp_all add: less_option_def)
lemma less_option_None_Some [simp]: "None < Some x"
by (simp add: less_option_def)
lemma less_option_None_Some_code [code]: "None < Some x ⟷ True"
by simp
lemma less_option_Some [simp, code]: "Some x < Some y ⟷ x < y"
by (simp add: less_option_def)
instance
by standard
(auto simp add: less_eq_option_def less_option_def less_le_not_le
elim: order_trans split: option.splits)
end
instance option :: (order) order
by standard (auto simp add: less_eq_option_def less_option_def split: option.splits)
instance option :: (linorder) linorder
by standard (auto simp add: less_eq_option_def less_option_def split: option.splits)
instantiation option :: (order) order_bot
begin
definition bot_option where "⊥ = None"
instance
by standard (simp add: bot_option_def)
end
instantiation option :: (order_top) order_top
begin
definition top_option where "⊤ = Some ⊤"
instance
by standard (simp add: top_option_def less_eq_option_def split: option.split)
end
instance option :: (wellorder) wellorder
proof
fix P :: "'a option ⇒ bool"
fix z :: "'a option"
assume H: "⋀x. (⋀y. y < x ⟹ P y) ⟹ P x"
have "P None" by (rule H) simp
then have P_Some [case_names Some]: "P z" if "⋀x. z = Some x ⟹ (P o Some) x" for z
using ‹P None› that by (cases z) simp_all
show "P z"
proof (cases z rule: P_Some)
case (Some w)
show "(P o Some) w"
proof (induct rule: less_induct)
case (less x)
have "P (Some x)"
proof (rule H)
fix y :: "'a option"
assume "y < Some x"
show "P y"
proof (cases y rule: P_Some)
case (Some v)
with ‹y < Some x› have "v < x" by simp
with less show "(P o Some) v" .
qed
qed
then show ?case by simp
qed
qed
qed
instantiation option :: (inf) inf
begin
definition inf_option where
"x ⊓ y = (case x of None ⇒ None | Some x ⇒ (case y of None ⇒ None | Some y ⇒ Some (x ⊓ y)))"
lemma inf_None_1 [simp, code]: "None ⊓ y = None"
by (simp add: inf_option_def)
lemma inf_None_2 [simp, code]: "x ⊓ None = None"
by (cases x) (simp_all add: inf_option_def)
lemma inf_Some [simp, code]: "Some x ⊓ Some y = Some (x ⊓ y)"
by (simp add: inf_option_def)
instance ..
end
instantiation option :: (sup) sup
begin
definition sup_option where
"x ⊔ y = (case x of None ⇒ y | Some x' ⇒ (case y of None ⇒ x | Some y ⇒ Some (x' ⊔ y)))"
lemma sup_None_1 [simp, code]: "None ⊔ y = y"
by (simp add: sup_option_def)
lemma sup_None_2 [simp, code]: "x ⊔ None = x"
by (cases x) (simp_all add: sup_option_def)
lemma sup_Some [simp, code]: "Some x ⊔ Some y = Some (x ⊔ y)"
by (simp add: sup_option_def)
instance ..
end
instance option :: (semilattice_inf) semilattice_inf
proof
fix x y z :: "'a option"
show "x ⊓ y ≤ x"
by (cases x, simp_all, cases y, simp_all)
show "x ⊓ y ≤ y"
by (cases x, simp_all, cases y, simp_all)
show "x ≤ y ⟹ x ≤ z ⟹ x ≤ y ⊓ z"
by (cases x, simp_all, cases y, simp_all, cases z, simp_all)
qed
instance option :: (semilattice_sup) semilattice_sup
proof
fix x y z :: "'a option"
show "x ≤ x ⊔ y"
by (cases x, simp_all, cases y, simp_all)
show "y ≤ x ⊔ y"
by (cases x, simp_all, cases y, simp_all)
fix x y z :: "'a option"
show "y ≤ x ⟹ z ≤ x ⟹ y ⊔ z ≤ x"
by (cases y, simp_all, cases z, simp_all, cases x, simp_all)
qed
instance option :: (lattice) lattice ..
instance option :: (lattice) bounded_lattice_bot ..
instance option :: (bounded_lattice_top) bounded_lattice_top ..
instance option :: (bounded_lattice_top) bounded_lattice ..
instance option :: (distrib_lattice) distrib_lattice
proof
fix x y z :: "'a option"
show "x ⊔ y ⊓ z = (x ⊔ y) ⊓ (x ⊔ z)"
by (cases x, simp_all, cases y, simp_all, cases z, simp_all add: sup_inf_distrib1 inf_commute)
qed
instantiation option :: (complete_lattice) complete_lattice
begin
definition Inf_option :: "'a option set ⇒ 'a option" where
"⨅A = (if None ∈ A then None else Some (⨅Option.these A))"
lemma None_in_Inf [simp]: "None ∈ A ⟹ ⨅A = None"
by (simp add: Inf_option_def)
definition Sup_option :: "'a option set ⇒ 'a option" where
"⨆A = (if A = {} ∨ A = {None} then None else Some (⨆Option.these A))"
lemma empty_Sup [simp]: "⨆{} = None"
by (simp add: Sup_option_def)
lemma singleton_None_Sup [simp]: "⨆{None} = None"
by (simp add: Sup_option_def)
instance
proof
fix x :: "'a option" and A
assume "x ∈ A"
then show "⨅A ≤ x"
by (cases x) (auto simp add: Inf_option_def in_these_eq intro: Inf_lower)
next
fix z :: "'a option" and A
assume *: "⋀x. x ∈ A ⟹ z ≤ x"
show "z ≤ ⨅A"
proof (cases z)
case None then show ?thesis by simp
next
case (Some y)
show ?thesis
by (auto simp add: Inf_option_def in_these_eq Some intro!: Inf_greatest dest!: *)
qed
next
fix x :: "'a option" and A
assume "x ∈ A"
then show "x ≤ ⨆A"
by (cases x) (auto simp add: Sup_option_def in_these_eq intro: Sup_upper)
next
fix z :: "'a option" and A
assume *: "⋀x. x ∈ A ⟹ x ≤ z"
show "⨆A ≤ z "
proof (cases z)
case None
with * have "⋀x. x ∈ A ⟹ x = None" by (auto dest: less_eq_option_None_is_None)
then have "A = {} ∨ A = {None}" by blast
then show ?thesis by (simp add: Sup_option_def)
next
case (Some y)
from * have "⋀w. Some w ∈ A ⟹ Some w ≤ z" .
with Some have "⋀w. w ∈ Option.these A ⟹ w ≤ y"
by (simp add: in_these_eq)
then have "⨆Option.these A ≤ y" by (rule Sup_least)
with Some show ?thesis by (simp add: Sup_option_def)
qed
next
show "⨆{} = (⊥::'a option)"
by (auto simp: bot_option_def)
show "⨅{} = (⊤::'a option)"
by (auto simp: top_option_def Inf_option_def)
qed
end
lemma Some_Inf:
"Some (⨅A) = ⨅(Some ` A)"
by (auto simp add: Inf_option_def)
lemma Some_Sup:
"A ≠ {} ⟹ Some (⨆A) = ⨆(Some ` A)"
by (auto simp add: Sup_option_def)
lemma Some_INF:
"Some (⨅x∈A. f x) = (⨅x∈A. Some (f x))"
using Some_Inf [of "f ` A"] by (simp add: comp_def)
lemma Some_SUP:
"A ≠ {} ⟹ Some (⨆x∈A. f x) = (⨆x∈A. Some (f x))"
using Some_Sup [of "f ` A"] by (simp add: comp_def)
instance option :: (complete_distrib_lattice) complete_distrib_lattice
proof
fix a :: "'a option" and B
show "a ⊔ ⨅B = (⨅b∈B. a ⊔ b)"
proof (cases a)
case None
then show ?thesis by simp
next
case (Some c)
show ?thesis
proof (cases "None ∈ B")
case True
then have "Some c = (⨅b∈B. Some c ⊔ b)"
by (auto intro!: antisym INF_lower2 INF_greatest)
with True Some show ?thesis by simp
next
case False then have B: "{x ∈ B. ∃y. x = Some y} = B" by auto (metis not_Some_eq)
from sup_Inf have "Some c ⊔ Some (⨅Option.these B) = Some (⨅b∈Option.these B. c ⊔ b)" by simp
then have "Some c ⊔ ⨅(Some ` Option.these B) = (⨅x∈Some ` Option.these B. Some c ⊔ x)"
by (simp add: Some_INF Some_Inf comp_def)
with Some B show ?thesis by (simp add: Some_image_these_eq cong del: strong_INF_cong)
qed
qed
show "a ⊓ ⨆B = (⨆b∈B. a ⊓ b)"
proof (cases a)
case None
then show ?thesis by (simp add: image_constant_conv bot_option_def cong del: strong_SUP_cong)
next
case (Some c)
show ?thesis
proof (cases "B = {} ∨ B = {None}")
case True
then show ?thesis by auto
next
have B: "B = {x ∈ B. ∃y. x = Some y} ∪ {x ∈ B. x = None}"
by auto
then have Sup_B: "⨆B = ⨆({x ∈ B. ∃y. x = Some y} ∪ {x ∈ B. x = None})"
and SUP_B: "⋀f. (⨆x ∈ B. f x) = (⨆x ∈ {x ∈ B. ∃y. x = Some y} ∪ {x ∈ B. x = None}. f x)"
by simp_all
have Sup_None: "⨆{x. x = None ∧ x ∈ B} = None"
by (simp add: bot_option_def [symmetric])
have SUP_None: "(⨆x∈{x. x = None ∧ x ∈ B}. Some c ⊓ x) = None"
by (simp add: bot_option_def [symmetric])
case False then have "Option.these B ≠ {}" by (simp add: these_not_empty_eq)
moreover from inf_Sup have "Some c ⊓ Some (⨆Option.these B) = Some (⨆b∈Option.these B. c ⊓ b)"
by simp
ultimately have "Some c ⊓ ⨆(Some ` Option.these B) = (⨆x∈Some ` Option.these B. Some c ⊓ x)"
by (simp add: Some_SUP Some_Sup comp_def)
with Some show ?thesis
by (simp add: Some_image_these_eq Sup_B SUP_B Sup_None SUP_None SUP_union Sup_union_distrib cong del: strong_SUP_cong)
qed
qed
qed
instance option :: (complete_linorder) complete_linorder ..
no_notation
bot ("⊥") and
top ("⊤") and
inf (infixl "⊓" 70) and
sup (infixl "⊔" 65) and
Inf ("⨅_" [900] 900) and
Sup ("⨆_" [900] 900)
no_syntax
"_INF1" :: "pttrns ⇒ 'b ⇒ 'b" ("(3⨅_./ _)" [0, 10] 10)
"_INF" :: "pttrn ⇒ 'a set ⇒ 'b ⇒ 'b" ("(3⨅_∈_./ _)" [0, 0, 10] 10)
"_SUP1" :: "pttrns ⇒ 'b ⇒ 'b" ("(3⨆_./ _)" [0, 10] 10)
"_SUP" :: "pttrn ⇒ 'a set ⇒ 'b ⇒ 'b" ("(3⨆_∈_./ _)" [0, 0, 10] 10)
end