Theory Exceptions

(*<*)
theory Exceptions
imports
  "ConcurrentHOL.ConcurrentHOL"
begin

(*>*)
section‹ Exceptions\label{sec:exceptions} ›

text‹

A sketch of how we might handle exceptions in this framework.

›

setup ‹Sign.mandatory_path "raw"›

type_synonym ('s, 'x, 'v) exn = "('s, 'x + 'v) prog"

definition action :: "('v × 's × 's) set ⇒ ('s, 'x, 'v) raw.exn" where
  "action = prog.action ∘ image (map_prod Inr id)"

definition return :: "'v ⇒ ('s, 'x, 'v) raw.exn" where
  "return = prog.return ∘ Inr"

definition throw :: "'x ⇒ ('s, 'x, 'v) raw.exn" where
  "throw = prog.return ∘ Inl"

definition catch :: "('s, 'x, 'v) raw.exn ⇒ ('x ⇒ ('s, 'x, 'v) raw.exn) ⇒ ('s, 'x, 'v) raw.exn" where
  "catch f handler = f ⤜ case_sum handler raw.return"

definition bind :: "('s, 'x, 'v) raw.exn ⇒ ('v ⇒ ('s, 'x, 'v) raw.exn) ⇒ ('s, 'x, 'v) raw.exn" where
  "bind f g = f ⤜ case_sum raw.throw g"

definition parallel :: "('s, 'x, unit) raw.exn ⇒ ('s, 'x, unit) raw.exn ⇒ ('s, 'x, unit) raw.exn" where
  "parallel P Q = (P ⤜ case_sum ⊥ prog.return ∥ Q ⤜ case_sum ⊥ prog.return) ⤜ raw.return"

setup ‹Sign.mandatory_path "bind"›

lemma bind:
  shows "raw.bind (raw.bind f g) h = raw.bind f (λx. raw.bind (g x) h)"
by (simp add: raw.bind_def prog.bind.bind sum.case_distrib[where h="λf. f ⤜ case_sum raw.throw h"])
   (simp add: raw.throw_def comp_def prog.bind.return cong: sum.case_cong)

lemma return:
  shows returnL: "raw.bind (raw.return v) = (λg. g v)"
    and returnR: "raw.bind f raw.return = f"
by (simp_all add: fun_eq_iff raw.bind_def raw.return_def raw.throw_def prog.bind.return case_sum_Inl_Inr_L)

lemma throwL:
  shows "raw.bind (raw.throw x) = (λg. raw.throw x)"
by (simp add: fun_eq_iff raw.bind_def raw.throw_def prog.bind.return)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "catch"›

lemma catch:
  shows "raw.catch (raw.catch f handler⇩1) handler⇩2 = raw.catch f (λx. raw.catch (handler⇩1 x) handler⇩2)"
by (simp add: raw.catch_def prog.bind.bind sum.case_distrib[where h="λf. f ⤜ case_sum handler⇩2 raw.return"])
   (simp add: raw.return_def comp_def prog.bind.return cong: sum.case_cong)

lemma returnL:
  shows "raw.catch (raw.return v) = (λhandler. raw.return v)"
by (simp add: fun_eq_iff raw.catch_def raw.return_def prog.bind.return)

lemma throw:
  shows throwL: "raw.catch (raw.throw x) = (λg. g x)"
    and throwR: "raw.catch f raw.throw = f"
by (simp_all add: fun_eq_iff raw.catch_def raw.return_def raw.throw_def prog.bind.return case_sum_Inl_Inr_L)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "parallel"›

lemma commute:
  shows "raw.parallel P Q = raw.parallel Q P"
by (simp add: raw.parallel_def prog.parallel.commute)

lemma assoc:
  shows "raw.parallel P (raw.parallel Q R) = raw.parallel (raw.parallel P Q) R"
by (simp add: raw.parallel_def raw.return_def prog.bind.bind prog.bind.return prog.parallel.assoc)

lemma return:
  shows "raw.parallel (raw.return ()) P = raw.catch P (λx. ⊥)" (is ?thesis1)
    and "raw.parallel P (raw.return ()) = raw.catch P (λx. ⊥)" (is ?thesis2)
proof -
  show ?thesis1
    by (simp add: raw.parallel_def raw.return_def
                  prog.bind.bind prog.bind.return prog.parallel.return prog.bind.botL
                  sum.case_distrib[where h="λf. f ⤜ prog.return ∘ Inr"]
            flip: raw.catch_def[unfolded raw.return_def o_def]
            cong: sum.case_cong)
  then show ?thesis2
    by (simp add: raw.parallel.commute)
qed

lemma throw:
  shows "raw.parallel (raw.throw x) P = raw.bind (raw.catch P (λx. ⊥)) (λx. ⊥)" (is ?thesis1)
    and "raw.parallel P (raw.throw x) = raw.bind (raw.catch P (λx. ⊥)) (λx. ⊥)" (is ?thesis2)
proof -
  show ?thesis1
    by (simp add: raw.parallel_def raw.throw_def raw.bind_def raw.return_def raw.catch_def
                  prog.bind.bind prog.bind.return prog.bind.botL prog.parallel.bot
                  sum.case_distrib[where h="λf. prog.bind f (λx. ⊥)"]
                  sum.case_distrib[where h="λf. f ⤜ case_sum (prog.return ∘ Inl) (λx. ⊥)"]
            cong: sum.case_cong)
  then show ?thesis2
    by (simp add: raw.parallel.commute)
qed

setup ‹Sign.parent_path›

setup ‹Sign.parent_path›

typedef ('s, 'x, 'v) exn = "UNIV :: ('s, 'x, 'v) raw.exn set"
by blast

setup_lifting type_definition_exn

instantiation exn :: (type, type, type) complete_distrib_lattice
begin

lift_definition bot_exn :: "('s, 'x, 'v) exn" is "⊥" .
lift_definition top_exn :: "('s, 'x, 'v) exn" is "⊤" .
lift_definition sup_exn :: "('s, 'x, 'v) exn ⇒ ('s, 'x, 'v) exn ⇒ ('s, 'x, 'v) exn" is sup .
lift_definition inf_exn :: "('s, 'x, 'v) exn ⇒ ('s, 'x, 'v) exn ⇒ ('s, 'x, 'v) exn" is inf .
lift_definition less_eq_exn :: "('s, 'x, 'v) exn ⇒ ('s, 'x, 'v) exn ⇒ bool" is less_eq .
lift_definition less_exn :: "('s, 'x, 'v) exn ⇒ ('s, 'x, 'v) exn ⇒ bool" is less .
lift_definition Inf_exn :: "('s, 'x, 'v) exn set ⇒ ('s, 'x, 'v) exn" is Inf .
lift_definition Sup_exn :: "('s, 'x, 'v) exn set ⇒ ('s, 'x, 'v) exn" is Sup .

instance by standard (transfer; auto intro: Inf_lower InfI le_supI1 SupI SupE Inf_Sup)+

end

setup ‹Sign.mandatory_path "exn"›

lift_definition action :: "('v × 's × 's) set ⇒ ('s, 'x, 'v) exn" is raw.action .
lift_definition return :: "'v ⇒ ('s, 'x, 'v) exn" is raw.return .
lift_definition throw :: "'x ⇒ ('s, 'x, 'v) exn" is raw.throw .
lift_definition catch :: "('s, 'x, 'v) exn ⇒ ('x ⇒ ('s, 'x, 'v) exn) ⇒ ('s, 'x, 'v) exn" is raw.catch .
lift_definition bind :: "('s, 'x, 'v) exn ⇒ ('v ⇒ ('s, 'x, 'v) exn) ⇒ ('s, 'x, 'v) exn" is raw.bind .
lift_definition parallel :: "('s, 'x, unit) exn ⇒ ('s, 'x, unit) exn ⇒ ('s, 'x, unit) exn" is raw.parallel .

adhoc_overloading
  Monad_Syntax.bind exn.bind
adhoc_overloading
  parallel exn.parallel

setup ‹Sign.mandatory_path "bind"›

lemma bind:
  shows "f ⤜ g ⤜ h = exn.bind f (λx. g x ⤜ h)"
by transfer (rule raw.bind.bind)

lemma return:
  shows returnL: "(⤜) (exn.return v) = (λg. g v)" (is ?thesis1)
    and returnR: "f ⤜ exn.return = f" (is ?thesis2)
by (transfer; rule raw.bind.return)+

lemma throwL:
  shows "(⤜) (exn.throw x) = (λg. exn.throw x)"
by transfer (rule raw.bind.throwL)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "catch"›

lemma catch:
  shows "exn.catch (exn.catch f handler⇩1) handler⇩2 = exn.catch f (λx. exn.catch (handler⇩1 x) handler⇩2)"
by transfer (rule raw.catch.catch)

lemma returnL:
  shows "exn.catch (exn.return v) = (λhandler. exn.return v)"
by transfer (rule raw.catch.returnL)

lemma throw:
  shows throwL: "exn.catch (exn.throw x) = (λg. g x)"
    and throwR: "exn.catch f exn.throw = f"
by (transfer; rule raw.catch.throw)+

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "parallel"›

lemma commute:     
  shows "exn.parallel P Q = exn.parallel Q P"
by transfer (rule raw.parallel.commute)

lemma assoc:
  shows "exn.parallel P (exn.parallel Q R) = exn.parallel (exn.parallel P Q) R"
by transfer (rule raw.parallel.assoc)

lemma return:
  shows returnL: "exn.return () ∥ P = exn.catch P ⊥"
    and returnR: "P ∥ exn.return () = exn.catch P ⊥"
unfolding bot_fun_def by (transfer; rule raw.parallel.return)+

lemma throw:
  shows throwL: "exn.throw x ∥ P = exn.catch P ⊥ ⤜ ⊥"
    and throwR: "P ∥ exn.throw x = exn.catch P ⊥ ⤜ ⊥"
unfolding bot_fun_def by (transfer; rule raw.parallel.throw)+

setup ‹Sign.parent_path›

setup ‹Sign.parent_path›
(*<*)

end
(*>*)