# Theory Opt

(*  Title:      HOL/MicroJava/BV/Opt.thy
Author:     Tobias Nipkow
Copyright   2000 TUM

More about options.
*)

section ‹More about Options›

theory Opt imports Err begin

definition le :: "'a ord  'a option ord"
where
"le r o1 o2 =
(case o2 of None  o1=None | Some y  (case o1 of None  True | Some x  x ⊑⇩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 o1 o2 =
(case o1 of None  OK o2
| Some x  (case o2 of None  OK o1
| 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:
"o1 ⊑⇘le ro2 =
(case o2 of None  o1=None |
Some y  (case o1 of None  True | Some x  x ⊑⇩r y))"
(*<*)
apply (unfold lesub_def le_def)
apply (rule refl)
done
(*>*)

lemma le_opt_refl: "order r A   x  opt A  x ⊑⇘le rx"
(*<*) by (auto simp add: unfold_le_opt opt_def split: option.split) (*<*)

lemma le_opt_trans [rule_format]:
"order r A  x  opt A  y  opt A  z  opt A  x ⊑⇘le ry  y ⊑⇘le rz  x ⊑⇘le rz"
(*<*)
apply (simp add: unfold_le_opt opt_def split: option.split)
apply (blast intro: order_trans)
done
(*>*)

lemma le_opt_antisym [rule_format]:
"order r A  x  opt A  y  opt A  z  opt A  x ⊑⇘le ry  y ⊑⇘le rx  x=y"
(*<*)
apply (simp add: unfold_le_opt opt_def split: option.split)
apply (blast intro: order_antisym)
done
(*>*)

lemma order_le_opt [intro!,simp]: "order r A  order(le r) (opt A)"
(*<*)
apply (subst order_def)
apply (blast intro: le_opt_refl le_opt_trans le_opt_antisym)
done
(*>*)

lemma None_bot [iff]:  "None ⊑⇘le rox"
(*<*)
apply (unfold lesub_def le_def)
apply (simp split: option.split)
done
(*>*)

lemma Some_le [iff]: "(Some x ⊑⇘le rz) = (y. z = Some y  x ⊑⇩r y)"
(*<*)
apply (unfold lesub_def le_def)
apply (simp split: option.split)
done
(*>*)

lemma le_None [iff]: "(x ⊑⇘le rNone) = (x = None)"
(*<*)
apply (unfold lesub_def le_def)
apply (simp split: option.split)
done
(*>*)

lemma OK_None_bot [iff]: "OK None ⊑⇘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 ⊔⇘sup fNone = OK x"
(*<*) by (simp add: plussub_def sup_def split: option.split) (*>*)

lemma sup_None2 [iff]: "None ⊔⇘sup fx = 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]:

(*<*)
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 ?A" and
clo: "closed ?A0 ?f0" and
ub1: "x?A0. y?A0. x ⊑⇘?r0x ⊔⇘?f0y" and
ub2: "x?A0. y?A0. y ⊑⇘?r0x ⊔⇘?f0y" and
lub: "x?A0. y?A0. z?A0. x ⊑⇘?r0z  y ⊑⇘?r0z  x ⊔⇘?f0y ⊑⇘?r0z"
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 ?A" 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 ⊔⇘?fy  ?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 ⊔⇘sup fb = OK c"
moreover from ord have "order r A" 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) ⊑⇘Err.le r(OK x) ⊔⇘lift2 f(OK y)
(OK y) ⊑⇘Err.le r(OK x) ⊔⇘lift2 f(OK y)"
by blast
moreover assume "x ⊔⇩f y = OK z"
ultimately have "x ⊑⇩r z  y ⊑⇩r z"
by (auto simp add: plussub_def lift2_def Err.le_def lesub_def)
}
ultimately have "a ⊑⇘le rc  b ⊑⇘le rc"
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 ⊑⇘?rx ⊔⇘?fy)  (x?A. y?A. y ⊑⇘?rx ⊔⇘?fy)"
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 ⊑⇘?rz  y ⊑⇘?rz  x ⊔⇘?fy ⊑⇘?rz"
proof (intro strip, elim conjE)
fix x y z
assume xyz: "x  ?A"   "y  ?A"   "z  ?A"
assume xz: "x ⊑⇘?rz" and yz: "y ⊑⇘?rz"
{ 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 ⊑⇘Err.le rOK g; OK e ⊑⇘Err.le rOK g   OK d ⊔⇘lift2 fOK e ⊑⇘Err.le rOK g"
by blast
hence " d ⊑⇩r g; e ⊑⇩r g   y. d ⊔⇩f e = OK y  y ⊑⇩r g" by simp
with ok some xyz xz yz have "x ⊔⇘?fy ⊑⇘?rz"
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 ⊔⇘?fy ⊑⇘?rz"
by - (cases a, simp, cases b, simp, cases c, simp, blast)
}
with xyz xz yz show "x ⊔⇘?fy ⊑⇘?rz"
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 A; top r T; x  A; T  A   (T ⊑⇩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 map_option_in_optionI:
" ox  opt S; xS. ox = Some x  f x  S
map_option f ox  opt S"
(*<*)
apply (unfold map_option_case)
apply (simp split: option.split)
apply blast
done
(*>*)

end