(* Title: HOL/Library/Option_ord.thy Author: Florian Haftmann, TU Muenchen *) section ‹Canonical order on option type› theory Option_ord imports Main begin unbundle lattice_syntax 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 ∘ 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 ∘ 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 ∘ 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))" by (simp add: Some_Inf image_comp) lemma Some_SUP: "A ≠ {} ⟹ Some (⨆x∈A. f x) = (⨆x∈A. Some (f x))" by (simp add: Some_Sup image_comp) lemma option_Inf_Sup: "⨅(Sup ` A) ≤ ⨆(Inf ` {f ` A |f. ∀Y∈A. f Y ∈ Y})" for A :: "('a::complete_distrib_lattice option) set set" proof (cases "{} ∈ A") case True then show ?thesis by (rule INF_lower2, simp_all) next case False from this have X: "{} ∉ A" by simp then show ?thesis proof (cases "{None} ∈ A") case True then show ?thesis by (rule INF_lower2, simp_all) next case False {fix y assume A: "y ∈ A" have "Sup (y - {None}) = Sup y" by (metis (no_types, lifting) Sup_option_def insert_Diff_single these_insert_None these_not_empty_eq) from A and this have "(∃z. y - {None} = z - {None} ∧ z ∈ A) ∧ ⨆y = ⨆(y - {None})" by auto } from this have A: "Sup ` A = (Sup ` {y - {None} | y. y∈A})" by (auto simp add: image_def) have [simp]: "⋀y. y ∈ A ⟹ ∃ya. {ya. ∃x. x ∈ y ∧ (∃y. x = Some y) ∧ ya = the x} = {y. ∃x∈ya - {None}. y = the x} ∧ ya ∈ A" by (rule exI, auto) have [simp]: "⋀y. y ∈ A ⟹ (∃ya. y - {None} = ya - {None} ∧ ya ∈ A) ∧ ⨆{ya. ∃x∈y - {None}. ya = the x} = ⨆{ya. ∃x. x ∈ y ∧ (∃y. x = Some y) ∧ ya = the x}" apply (safe, blast) by (rule arg_cong [of _ _ Sup], auto) {fix y assume [simp]: "y ∈ A" have "∃x. (∃y. x = {ya. ∃x∈y - {None}. ya = the x} ∧ y ∈ A) ∧ ⨆{ya. ∃x. x ∈ y ∧ (∃y. x = Some y) ∧ ya = the x} = ⨆x" and "∃x. (∃y. x = y - {None} ∧ y ∈ A) ∧ ⨆{ya. ∃x∈y - {None}. ya = the x} = ⨆{y. ∃xa. xa ∈ x ∧ (∃y. xa = Some y) ∧ y = the xa}" apply (rule exI [of _ "{ya. ∃x. x ∈ y ∧ (∃y. x = Some y) ∧ ya = the x}"], simp) by (rule exI [of _ "y - {None}"], simp) } from this have C: "(λx. (⨆Option.these x)) ` {y - {None} |y. y ∈ A} = (Sup ` {the ` (y - {None}) |y. y ∈ A})" by (simp add: image_def Option.these_def, safe, simp_all) have D: "∀ f . ∃Y∈A. f Y ∉ Y ⟹ False" by (drule spec [of _ "λ Y . SOME x . x ∈ Y"], simp add: X some_in_eq) define F where "F = (λ Y . SOME x::'a option . x ∈ (Y - {None}))" have G: "⋀ Y . Y ∈ A ⟹ ∃ x . x ∈ Y - {None}" by (metis False X all_not_in_conv insert_Diff_single these_insert_None these_not_empty_eq) have F: "⋀ Y . Y ∈ A ⟹ F Y ∈ (Y - {None})" by (metis F_def G empty_iff some_in_eq) have "Some ⊥ ≤ Inf (F ` A)" by (metis (no_types, lifting) Diff_iff F Inf_option_def bot.extremum image_iff less_eq_option_Some singletonI) from this have "Inf (F ` A) ≠ None" by (cases "⨅x∈A. F x", simp_all) from this have "Inf (F ` A) ≠ None ∧ Inf (F ` A) ∈ Inf ` {f ` A |f. ∀Y∈A. f Y ∈ Y}" using F by auto from this have "∃ x . x ≠ None ∧ x ∈ Inf ` {f ` A |f. ∀Y∈A. f Y ∈ Y}" by blast from this have E:" Inf ` {f ` A |f. ∀Y∈A. f Y ∈ Y} = {None} ⟹ False" by blast have [simp]: "((⨆x∈{f ` A |f. ∀Y∈A. f Y ∈ Y}. ⨅x) = None) = False" by (metis (no_types, lifting) E Sup_option_def ‹∃x. x ≠ None ∧ x ∈ Inf ` {f ` A |f. ∀Y∈A. f Y ∈ Y}› ex_in_conv option.simps(3)) have B: "Option.these ((λx. Some (⨆Option.these x)) ` {y - {None} |y. y ∈ A}) = ((λx. (⨆ Option.these x)) ` {y - {None} |y. y ∈ A})" by (metis image_image these_image_Some_eq) { fix f assume A: "⋀ Y . (∃y. Y = the ` (y - {None}) ∧ y ∈ A) ⟹ f Y ∈ Y" have "⋀xa. xa ∈ A ⟹ f {y. ∃a∈xa - {None}. y = the a} = f (the ` (xa - {None}))" by (simp add: image_def) from this have [simp]: "⋀xa. xa ∈ A ⟹ ∃x∈A. f {y. ∃a∈xa - {None}. y = the a} = f (the ` (x - {None}))" by blast have "⋀xa. xa ∈ A ⟹ f (the ` (xa - {None})) = f {y. ∃a ∈ xa - {None}. y = the a} ∧ xa ∈ A" by (simp add: image_def) from this have [simp]: "⋀xa. xa ∈ A ⟹ ∃x. f (the ` (xa - {None})) = f {y. ∃a∈x - {None}. y = the a} ∧ x ∈ A" by blast { fix Y have "Y ∈ A ⟹ Some (f (the ` (Y - {None}))) ∈ Y" using A [of "the ` (Y - {None})"] apply (simp add: image_def) using option.collapse by fastforce } from this have [simp]: "⋀ Y . Y ∈ A ⟹ Some (f (the ` (Y - {None}))) ∈ Y" by blast have [simp]: "(⨅x∈A. Some (f {y. ∃x∈x - {None}. y = the x})) = ⨅{Some (f {y. ∃a∈x - {None}. y = the a}) |x. x ∈ A}" by (simp add: Setcompr_eq_image) have [simp]: "∃x. (∃f. x = {y. ∃x∈A. y = f x} ∧ (∀Y∈A. f Y ∈ Y)) ∧ ⨅{Some (f {y. ∃a∈x - {None}. y = the a}) |x. x ∈ A} = ⨅x" apply (rule exI [of _ "{Some (f {y. ∃a∈x - {None}. y = the a}) | x . x∈ A}"], safe) by (rule exI [of _ "(λ Y . Some (f (the ` (Y - {None})))) "], safe, simp_all) { fix xb have "xb ∈ A ⟹ (⨅x∈{{ya. ∃x∈y - {None}. ya = the x} |y. y ∈ A}. f x) ≤ f {y. ∃x∈xb - {None}. y = the x}" apply (rule INF_lower2 [of "{y. ∃x∈xb - {None}. y = the x}"]) by blast+ } from this have [simp]: "(⨅x∈{the ` (y - {None}) |y. y ∈ A}. f x) ≤ the (⨅Y∈A. Some (f (the ` (Y - {None}))))" apply (simp add: Inf_option_def image_def Option.these_def) by (rule Inf_greatest, clarsimp) have [simp]: "the (⨅Y∈A. Some (f (the ` (Y - {None})))) ∈ Option.these (Inf ` {f ` A |f. ∀Y∈A. f Y ∈ Y})" apply (auto simp add: Option.these_def) apply (rule imageI) apply auto using ‹⋀Y. Y ∈ A ⟹ Some (f (the ` (Y - {None}))) ∈ Y› apply blast apply (auto simp add: Some_INF [symmetric]) done have "(⨅x∈{the ` (y - {None}) |y. y ∈ A}. f x) ≤ ⨆Option.these (Inf ` {f ` A |f. ∀Y∈A. f Y ∈ Y})" by (rule Sup_upper2 [of "the (Inf ((λ Y . Some (f (the ` (Y - {None})) )) ` A))"], simp_all) } from this have X: "⋀ f . ∀Y. (∃y. Y = the ` (y - {None}) ∧ y ∈ A) ⟶ f Y ∈ Y ⟹ (⨅x∈{the ` (y - {None}) |y. y ∈ A}. f x) ≤ ⨆Option.these (Inf ` {f ` A |f. ∀Y∈A. f Y ∈ Y})" by blast have [simp]: "⋀ x . x∈{y - {None} |y. y ∈ A} ⟹ x ≠ {} ∧ x ≠ {None}" using F by fastforce have "(Inf (Sup `A)) = (Inf (Sup ` {y - {None} | y. y∈A}))" by (subst A, simp) also have "... = (⨅x∈{y - {None} |y. y ∈ A}. if x = {} ∨ x = {None} then None else Some (⨆Option.these x))" by (simp add: Sup_option_def) also have "... = (⨅x∈{y - {None} |y. y ∈ A}. Some (⨆Option.these x))" using G by fastforce also have "... = Some (⨅Option.these ((λx. Some (⨆Option.these x)) ` {y - {None} |y. y ∈ A}))" by (simp add: Inf_option_def, safe) also have "... = Some (⨅ ((λx. (⨆Option.these x)) ` {y - {None} |y. y ∈ A}))" by (simp add: B) also have "... = Some (Inf (Sup ` {the ` (y - {None}) |y. y ∈ A}))" by (unfold C, simp) thm Inf_Sup also have "... = Some (⨆x∈{f ` {the ` (y - {None}) |y. y ∈ A} |f. ∀Y. (∃y. Y = the ` (y - {None}) ∧ y ∈ A) ⟶ f Y ∈ Y}. ⨅x) " by (simp add: Inf_Sup) also have "... ≤ ⨆ (Inf ` {f ` A |f. ∀Y∈A. f Y ∈ Y})" proof (cases "⨆ (Inf ` {f ` A |f. ∀Y∈A. f Y ∈ Y})") case None then show ?thesis by (simp add: less_eq_option_def) next case (Some a) then show ?thesis apply simp apply (rule Sup_least, safe) apply (simp add: Sup_option_def) apply (cases "(∀f. ∃Y∈A. f Y ∉ Y) ∨ Inf ` {f ` A |f. ∀Y∈A. f Y ∈ Y} = {None}", simp_all) by (drule X, simp) qed finally show ?thesis by simp qed qed instance option :: (complete_distrib_lattice) complete_distrib_lattice by (standard, simp add: option_Inf_Sup) instance option :: (complete_linorder) complete_linorder .. unbundle no_lattice_syntax end