header {* \isaheader{More about Options} *}
theory Opt imports Err begin
definition le :: "'a ord => 'a option ord"
where
"le r o⇣1 o⇣2 =
(case o⇣2 of None => o⇣1=None | Some y => (case o⇣1 of None => True | Some x => x \<sqsubseteq>⇩r y))"
definition opt :: "'a set => 'a option set"
where
"opt A = insert None {Some y |y. y ∈ A}"
definition sup :: "'a ebinop => 'a option ebinop"
where
"sup f o⇣1 o⇣2 =
(case o⇣1 of None => OK o⇣2
| Some x => (case o⇣2 of None => OK o⇣1
| Some y => (case f x y of Err => Err | OK z => OK (Some z))))"
definition esl :: "'a esl => 'a option esl"
where
"esl = (λ(A,r,f). (opt A, le r, sup f))"
lemma unfold_le_opt:
"o⇣1 \<sqsubseteq>⇘le r⇙ o⇣2 =
(case o⇣2 of None => o⇣1=None |
Some y => (case o⇣1 of None => True | Some x => x \<sqsubseteq>⇩r y))"
apply (unfold lesub_def le_def)
apply (rule refl)
done
lemma le_opt_refl: "order r ==> x \<sqsubseteq>⇘le r⇙ x"
by (simp add: unfold_le_opt split: option.split)
lemma le_opt_trans [rule_format]:
"order r ==> x \<sqsubseteq>⇘le r⇙ y --> y \<sqsubseteq>⇘le r⇙ z --> x \<sqsubseteq>⇘le r⇙ z"
apply (simp add: unfold_le_opt split: option.split)
apply (blast intro: order_trans)
done
lemma le_opt_antisym [rule_format]:
"order r ==> x \<sqsubseteq>⇘le r⇙ y --> y \<sqsubseteq>⇘le r⇙ x --> x=y"
apply (simp add: unfold_le_opt split: option.split)
apply (blast intro: order_antisym)
done
lemma order_le_opt [intro!,simp]: "order r ==> order(le r)"
apply (subst order_def)
apply (blast intro: le_opt_refl le_opt_trans le_opt_antisym)
done
lemma None_bot [iff]: "None \<sqsubseteq>⇘le r⇙ ox"
apply (unfold lesub_def le_def)
apply (simp split: option.split)
done
lemma Some_le [iff]: "(Some x \<sqsubseteq>⇘le r⇙ z) = (∃y. z = Some y ∧ x \<sqsubseteq>⇩r y)"
apply (unfold lesub_def le_def)
apply (simp split: option.split)
done
lemma le_None [iff]: "(x \<sqsubseteq>⇘le r⇙ None) = (x = None)"
apply (unfold lesub_def le_def)
apply (simp split: option.split)
done
lemma OK_None_bot [iff]: "OK None \<sqsubseteq>⇘Err.le (le r)⇙ x"
by (simp add: lesub_def Err.le_def le_def split: option.split err.split)
lemma sup_None1 [iff]: "x \<squnion>⇘sup f⇙ None = OK x"
by (simp add: plussub_def sup_def split: option.split)
lemma sup_None2 [iff]: "None \<squnion>⇘sup f⇙ x = OK x"
by (simp add: plussub_def sup_def split: option.split)
lemma None_in_opt [iff]: "None ∈ opt A"
by (simp add: opt_def)
lemma Some_in_opt [iff]: "(Some x ∈ opt A) = (x ∈ A)"
by (unfold opt_def) auto
lemma semilat_opt [intro, simp]:
"err_semilat L ==> err_semilat (Opt.esl L)"
proof -
assume s: "err_semilat L"
obtain A r f where [simp]: "L = (A,r,f)" by (cases L)
let ?A0 = "err A" and ?r0 = "Err.le r" and ?f0 = "lift2 f"
from s obtain
ord: "order ?r0" and
clo: "closed ?A0 ?f0" and
ub1: "∀x∈?A0. ∀y∈?A0. x \<sqsubseteq>⇘?r0⇙ x \<squnion>⇘?f0⇙ y" and
ub2: "∀x∈?A0. ∀y∈?A0. y \<sqsubseteq>⇘?r0⇙ x \<squnion>⇘?f0⇙ y" and
lub: "∀x∈?A0. ∀y∈?A0. ∀z∈?A0. x \<sqsubseteq>⇘?r0⇙ z ∧ y \<sqsubseteq>⇘?r0⇙ z --> x \<squnion>⇘?f0⇙ y \<sqsubseteq>⇘?r0⇙ z"
by (unfold semilat_def sl_def) simp
let ?A = "err (opt A)" and ?r = "Err.le (Opt.le r)" and ?f = "lift2 (Opt.sup f)"
from ord have "order ?r" by simp
moreover
have "closed ?A ?f"
proof (unfold closed_def, intro strip)
fix x y assume x: "x ∈ ?A" and y: "y ∈ ?A"
{ fix a b assume ab: "x = OK a" "y = OK b"
with x have a: "!!c. a = Some c ==> c ∈ A" by (clarsimp simp add: opt_def)
from ab y have b: "!!d. b = Some d ==> d ∈ A" by (clarsimp simp add: opt_def)
{ fix c d assume "a = Some c" "b = Some d"
with ab x y have "c ∈ A & d ∈ A" by (simp add: err_def opt_def Bex_def)
with clo have "f c d ∈ err A"
by (simp add: closed_def plussub_def err_def' lift2_def)
moreover fix z assume "f c d = OK z"
ultimately have "z ∈ A" by simp
} note f_closed = this
have "sup f a b ∈ ?A"
proof (cases a)
case None thus ?thesis
by (simp add: sup_def opt_def) (cases b, simp, simp add: b Bex_def)
next
case Some thus ?thesis
by (auto simp add: sup_def opt_def Bex_def a b f_closed split: err.split option.split)
qed
}
thus "x \<squnion>⇘?f⇙ y ∈ ?A" by (simp add: plussub_def lift2_def split: err.split)
qed
moreover
{ fix a b c assume "a ∈ opt A" and "b ∈ opt A" and "a \<squnion>⇘sup f⇙ b = OK c"
moreover from ord have "order r" by simp
moreover
{ fix x y z assume "x ∈ A" and "y ∈ A"
hence "OK x ∈ err A ∧ OK y ∈ err A" by simp
with ub1 ub2
have "(OK x) \<sqsubseteq>⇘Err.le r⇙ (OK x) \<squnion>⇘lift2 f⇙ (OK y) ∧
(OK y) \<sqsubseteq>⇘Err.le r⇙ (OK x) \<squnion>⇘lift2 f⇙ (OK y)"
by blast
moreover assume "x \<squnion>⇩f y = OK z"
ultimately have "x \<sqsubseteq>⇩r z ∧ y \<sqsubseteq>⇩r z"
by (auto simp add: plussub_def lift2_def Err.le_def lesub_def)
}
ultimately have "a \<sqsubseteq>⇘le r⇙ c ∧ b \<sqsubseteq>⇘le r⇙ c"
by (auto simp add: sup_def le_def lesub_def plussub_def
dest: order_refl split: option.splits err.splits)
}
hence "(∀x∈?A. ∀y∈?A. x \<sqsubseteq>⇘?r⇙ x \<squnion>⇘?f⇙ y) ∧ (∀x∈?A. ∀y∈?A. y \<sqsubseteq>⇘?r⇙ x \<squnion>⇘?f⇙ y)"
by (auto simp add: lesub_def plussub_def Err.le_def lift2_def split: err.split)
moreover
have "∀x∈?A. ∀y∈?A. ∀z∈?A. x \<sqsubseteq>⇘?r⇙ z ∧ y \<sqsubseteq>⇘?r⇙ z --> x \<squnion>⇘?f⇙ y \<sqsubseteq>⇘?r⇙ z"
proof (intro strip, elim conjE)
fix x y z
assume xyz: "x ∈ ?A" "y ∈ ?A" "z ∈ ?A"
assume xz: "x \<sqsubseteq>⇘?r⇙ z" and yz: "y \<sqsubseteq>⇘?r⇙ z"
{ fix a b c assume ok: "x = OK a" "y = OK b" "z = OK c"
{ fix d e g assume some: "a = Some d" "b = Some e" "c = Some g"
with ok xyz obtain "OK d:err A" "OK e:err A" "OK g:err A" by simp
with lub
have "[| OK d \<sqsubseteq>⇘Err.le r⇙ OK g; OK e \<sqsubseteq>⇘Err.le r⇙ OK g |] ==> OK d \<squnion>⇘lift2 f⇙ OK e \<sqsubseteq>⇘Err.le r⇙ OK g"
by blast
hence "[| d \<sqsubseteq>⇩r g; e \<sqsubseteq>⇩r g |] ==> ∃y. d \<squnion>⇩f e = OK y ∧ y \<sqsubseteq>⇩r g" by simp
with ok some xyz xz yz have "x \<squnion>⇘?f⇙ y \<sqsubseteq>⇘?r⇙ z"
by (auto simp add: sup_def le_def lesub_def lift2_def plussub_def Err.le_def)
} note this [intro!]
from ok xyz xz yz have "x \<squnion>⇘?f⇙ y \<sqsubseteq>⇘?r⇙ z"
by - (cases a, simp, cases b, simp, cases c, simp, blast)
}
with xyz xz yz show "x \<squnion>⇘?f⇙ y \<sqsubseteq>⇘?r⇙ z"
by - (cases x, simp, cases y, simp, cases z, simp+)
qed
ultimately show "err_semilat (Opt.esl L)"
by (unfold semilat_def esl_def sl_def) simp
qed
lemma top_le_opt_Some [iff]: "top (le r) (Some T) = top r T"
apply (unfold top_def)
apply (rule iffI)
apply blast
apply (rule allI)
apply (case_tac "x")
apply simp+
done
lemma Top_le_conv: "[| order r; top r T |] ==> (T \<sqsubseteq>⇩r x) = (x = T)"
apply (unfold top_def)
apply (blast intro: order_antisym)
done
lemma acc_le_optI [intro!]: "acc r ==> acc(le r)"
apply (unfold acc_def lesub_def le_def lesssub_def)
apply (simp add: wf_eq_minimal split: option.split)
apply clarify
apply (case_tac "∃a. Some a ∈ Q")
apply (erule_tac x = "{a . Some a ∈ Q}" in allE)
apply blast
apply (case_tac "x")
apply blast
apply blast
done
lemma option_map_in_optionI:
"[| ox ∈ opt S; ∀x∈S. ox = Some x --> f x ∈ S |]
==> Option.map f ox ∈ opt S"
apply (unfold Option.map_def)
apply (simp split: option.split)
apply blast
done
end