Quelle  Option_Cpo.thy

(*  Title:      HOL/HOLCF/Library/Option_Cpo.thy
  Author: Brian Huffman
*)

section ‹Cpo class instance for HOL option type›

theory Option_Cpo
imports HOLCF Sum_Cpo
begin

subsection ‹Ordering on option type›

instantiation option :: (below) below
begin

definition below_option_def:
  "x ⊑ y ≡ case x of
         None ==> (case y of None ==> True | Some b ==> False) |
         Some a ==> (case y of None ==> False | Some b ==> a ⊑ b)"

instance ..
end

lemma None_below_None [simp]: "None ⊑ None"
unfolding below_option_def by simp

lemma Some_below_Some [simp]: "Some x ⊑ Some y ⟷ x ⊑ y"
unfolding below_option_def by simp

lemma Some_below_None [simp]: "¬ Some x ⊑ None"
unfolding below_option_def by simp

lemma None_below_Some [simp]: "¬ None ⊑ Some y"
unfolding below_option_def by simp

lemma Some_mono: "x ⊑ y ==> Some x ⊑ Some y"
by simp

lemma None_below_iff [simp]: "None ⊑ x ⟷ x = None"
by (cases x, simp_all)

lemma below_None_iff [simp]: "x ⊑ None ⟷ x = None"
by (cases x, simp_all)

lemma option_below_cases:
  assumes "x ⊑ y"
  obtains "x = None" and "y = None"
  | a b where "x = Some a" and "y = Some b" and "a ⊑ b"
using assms unfolding below_option_def
by (simp split: option.split_asm)

subsection ‹Option type is a complete partial order›

instance option :: (po) po
proof
  fix x :: "'a option"
  show "x ⊑ x"
    unfolding below_option_def
    by (simp split: option.split)
next
  fix x y :: "'a option"
  assume "x ⊑ y" and "y ⊑ x" thus "x = y"
    unfolding below_option_def
    by (auto split: option.split_asm intro: below_antisym)
next
  fix x y z :: "'a option"
  assume "x ⊑ y" and "y ⊑ z" thus "x ⊑ z"
    unfolding below_option_def
    by (auto split: option.split_asm intro: below_trans)
qed

lemma monofun_the: "monofun the"
by (rule monofunI, erule option_below_cases, simp_all)

lemma option_chain_cases:
  assumes Y: "chain Y"
  obtains "Y = (λi. None)" | A where "chain A" and "Y = (λi. Some (A i))"
 apply (cases "Y 0")
  apply (rule that(1))
  apply (rule ext)
  apply (cut_tac j=i in chain_mono [OF Y le0], simp)
 apply (rule that(2))
  apply (rule ch2ch_monofun [OF monofun_the Y])
 apply (rule ext)
 apply (cut_tac j=i in chain_mono [OF Y le0], simp)
 apply (case_tac "Y i", simp_all)
done

lemma is_lub_Some: "range S <<| x ==> range (λi. Some (S i)) <<| Some x"
 apply (rule is_lubI)
  apply (rule ub_rangeI)
  apply (simp add: is_lub_rangeD1)
 apply (frule ub_rangeD [where i=arbitrary])
 apply (case_tac u, simp_all)
 apply (erule is_lubD2)
 apply (rule ub_rangeI)
 apply (drule ub_rangeD, simp)
done

instance option :: (cpo) cpo
 apply intro_classes
 apply (erule option_chain_cases, safe)
  apply (rule exI, rule is_lub_const)
 apply (rule exI)
 apply (rule is_lub_Some)
 apply (erule cpo_lubI)
done

subsection ‹Continuity of Some and case function›

lemma cont_Some: "cont Some"
by (intro contI is_lub_Some cpo_lubI)

lemmas cont2cont_Some [simp, cont2cont] = cont_compose [OF cont_Some]

lemmas ch2ch_Some [simp] = ch2ch_cont [OF cont_Some]

lemmas lub_Some = cont2contlubE [OF cont_Some, symmetric]

lemma cont2cont_case_option:
  assumes f: "cont (λx. f x)"
  assumes g: "cont (λx. g x)"
  assumes h1: "∧a. cont (λx. h x a)"
  assumes h2: "∧x. cont (λa. h x a)"
  shows "cont (λx. case f x of None ==> g x | Some a ==> h x a)"
apply (rule cont_apply [OF f])
apply (rule contI)
apply (erule option_chain_cases)
apply (simp add: is_lub_const)
apply (simp add: lub_Some)
apply (simp add: cont2contlubE [OF h2])
apply (rule cpo_lubI, rule chainI)
apply (erule cont2monofunE [OF h2 chainE])
apply (case_tac y, simp_all add: g h1)
done

lemma cont2cont_case_option' [simp, cont2cont]:
  assumes f: "cont (λx. f x)"
  assumes g: "cont (λx. g x)"
  assumes h: "cont (λp. h (fst p) (snd p))"
  shows "cont (λx. case f x of None ==> g x | Some a ==> h x a)"
using assms by (simp add: cont2cont_case_option prod_cont_iff)

text ‹Simple version for when the element type is not a cpo.›

lemma cont2cont_case_option_simple [simp, cont2cont]:
  assumes "cont (λx. f x)"
  assumes "∧a. cont (λx. g x a)"
  shows "cont (λx. case z of None ==> f x | Some a ==> g x a)"
using assms by (cases z) auto

text ‹Continuity rule for map.›

lemma cont2cont_map_option [simp, cont2cont]:
  assumes f: "cont (λ(x, y). f x y)"
  assumes g: "cont (λx. g x)"
  shows "cont (λx. map_option (λy. f x y) (g x))"
using assms by (simp add: prod_cont_iff map_option_case)

subsection ‹Compactness and chain-finiteness›

lemma compact_None [simp]: "compact None"
apply (rule compactI2)
apply (erule option_chain_cases, safe)
apply simp
apply (simp add: lub_Some)
done

lemma compact_Some: "compact a ==> compact (Some a)"
apply (rule compactI2)
apply (erule option_chain_cases, safe)
apply simp
apply (simp add: lub_Some)
apply (erule (2) compactD2)
done

lemma compact_Some_rev: "compact (Some a) ==> compact a"
unfolding compact_def
by (drule adm_subst [OF cont_Some], simp)

lemma compact_Some_iff [simp]: "compact (Some a) = compact a"
by (safe elim!: compact_Some compact_Some_rev)

instance option :: (chfin) chfin
apply intro_classes
apply (erule compact_imp_max_in_chain)
apply (case_tac "⊔i. Y i", simp_all)
done

instance option :: (discrete_cpo) discrete_cpo
by intro_classes (simp add: below_option_def split: option.split)

subsection ‹Using option types with Fixrec›

definition
  "match_None = (Λ x k. case x of None ==> k | Some a ==> Fixrec.fail)"

definition
  "match_Some = (Λ x k. case x of None ==> Fixrec.fail | Some a ==> k⋅a)"

lemma match_None_simps [simp]:
  "match_None⋅None⋅k = k"
  "match_None⋅(Some a)⋅k = Fixrec.fail"
unfolding match_None_def by simp_all

lemma match_Some_simps [simp]:
  "match_Some⋅None⋅k = Fixrec.fail"
  "match_Some⋅(Some a)⋅k = k⋅a"
unfolding match_Some_def by simp_all

setup ‹
  Fixrec.add_matchers
  [ (🍋‹None›, 🍋‹match_None›),
  (🍋‹Some›, 🍋‹match_Some›) ]
 ›

subsection ‹Option type is a predomain›

definition
  "encode_option = (Λ x. case x of None ==> Inl () | Some a ==> Inr a)"

definition
  "decode_option = (Λ x. case x of Inl (u::unit) ==> None | Inr a ==> Some a)"

lemma decode_encode_option [simp]: "decode_option⋅(encode_option⋅x) = x"
unfolding decode_option_def encode_option_def
by (cases x, simp_all)

lemma encode_decode_option [simp]: "encode_option⋅(decode_option⋅x) = x"
unfolding decode_option_def encode_option_def
by (cases x, simp_all)

instantiation option :: (predomain) predomain
begin

definition
  "liftemb = liftemb oo u_map⋅encode_option"

definition
  "liftprj = u_map⋅decode_option oo liftprj"

definition
  "liftdefl (t::('a option) itself) = LIFTDEFL(unit + 'a)"

instance proof
  show "ep_pair liftemb (liftprj :: udom u → ('a option) u)"
    unfolding liftemb_option_def liftprj_option_def
    apply (intro ep_pair_comp ep_pair_u_map predomain_ep)
    apply (rule ep_pair.intro, simp, simp)
    done
  show "cast⋅LIFTDEFL('a option) = liftemb oo (liftprj :: udom u → ('a option) u)"
    unfolding liftemb_option_def liftprj_option_def liftdefl_option_def
    by (simp add: cast_liftdefl cfcomp1 u_map_map ID_def [symmetric] u_map_ID)
qed

end

subsection ‹Configuring domain package to work with option type›

lemma liftdefl_option [domain_defl_simps]:
  "LIFTDEFL('a::predomain option) = LIFTDEFL(unit + 'a)"
by (rule liftdefl_option_def)

abbreviation option_map
  where "option_map f ≡ Abs_cfun (map_option (Rep_cfun f))"

lemma option_map_ID [domain_map_ID]: "option_map ID = ID"
by (simp add: ID_def cfun_eq_iff option.map_id[unfolded id_def] id_def)

lemma deflation_option_map [domain_deflation]:
  "deflation d ==> deflation (option_map d)"
apply standard
apply (induct_tac x, simp_all add: deflation.idem)
apply (induct_tac x, simp_all add: deflation.below)
done

lemma encode_option_option_map:
  "encode_option⋅(map_option (λx. f⋅x) (decode_option⋅x)) = map_sum' ID f⋅x"
by (induct x, simp_all add: decode_option_def encode_option_def)

lemma isodefl_option [domain_isodefl]:
  assumes "isodefl' d t"
  shows "isodefl' (option_map d) (sum_liftdefl⋅(liftdefl_of⋅DEFL(unit))⋅t)"
using isodefl_sum [OF isodefl_LIFTDEFL [where 'a=unit] assms]
unfolding isodefl'_def liftemb_option_def liftprj_option_def liftdefl_eq
by (simp add: cfcomp1 u_map_map encode_option_option_map)

setup ‹
  Domain_Take_Proofs.add_rec_type (🍋‹option›, [true])
 ›

end