# Theory Resumption

```(* Title: Resumption.thy
Author: Andreas Lochbihler, ETH Zurich *)

theory Resumption
imports
Misc_CryptHOL
Partial_Function_Set
begin

codatatype (results: 'a, outputs: 'out, 'in) resumption
= Done (result: "'a option")
| Pause ("output": 'out) (resume: "'in ⇒ ('a, 'out, 'in) resumption")
where
"resume (Done a) = (λinp. Done None)"

code_datatype Done Pause

primcorec bind_resumption ::
"('a, 'out, 'in) resumption
⇒ ('a ⇒ ('b, 'out, 'in) resumption) ⇒ ('b, 'out, 'in) resumption"
where
"⟦ is_Done x; result x ≠ None ⟶ is_Done (f (the (result x))) ⟧ ⟹ is_Done (bind_resumption x f)"
| "result (bind_resumption x f) = result x ⤜ result ∘ f"
| "output (bind_resumption x f) = (if is_Done x then output (f (the (result x))) else output x)"
| "resume (bind_resumption x f) = (λinp. if is_Done x then resume (f (the (result x))) inp else bind_resumption (resume x inp) f)"

declare bind_resumption.sel [simp del]

lemma is_Done_bind_resumption [simp]:
"is_Done (x ⤜ f) ⟷ is_Done x ∧ (result x ≠ None ⟶ is_Done (f (the (result x))))"

lemma result_bind_resumption [simp]:
"is_Done (x ⤜ f) ⟹ result (x ⤜ f) = result x ⤜ result ∘ f"

lemma output_bind_resumption [simp]:
"¬ is_Done (x ⤜ f) ⟹ output (x ⤜ f) = (if is_Done x then output (f (the (result x))) else output x)"

lemma resume_bind_resumption [simp]:
"¬ is_Done (x ⤜ f) ⟹
resume (x ⤜ f) =
(if is_Done x then resume (f (the (result x)))
else (λinp. resume x inp ⤜ f))"

definition DONE :: "'a ⇒ ('a, 'out, 'in) resumption"
where "DONE = Done ∘ Some"

definition ABORT :: "('a, 'out, 'in) resumption"
where "ABORT = Done None"

lemma [simp]:
shows is_Done_DONE: "is_Done (DONE a)"
and is_Done_ABORT: "is_Done ABORT"
and result_DONE: "result (DONE a) = Some a"
and result_ABORT: "result ABORT = None"
and DONE_inject: "DONE a = DONE b ⟷ a = b"
and DONE_neq_ABORT: "DONE a ≠ ABORT"
and ABORT_neq_DONE: "ABORT ≠ DONE a"
and ABORT_eq_Done: "⋀a. ABORT = Done a ⟷ a = None"
and Done_eq_ABORT: "⋀a. Done a = ABORT ⟷ a = None"
and DONE_eq_Done: "⋀b. DONE a = Done b ⟷ b = Some a"
and Done_eq_DONE: "⋀b. Done b = DONE a ⟷ b = Some a"
and DONE_neq_Pause: "DONE a ≠ Pause out c"
and Pause_neq_DONE: "Pause out c ≠ DONE a"
and ABORT_neq_Pause: "ABORT ≠ Pause out c"
and Pause_neq_ABORT: "Pause out c ≠ ABORT"

lemma resume_ABORT [simp]:
"resume (Done r) = (λinp. ABORT)"

declare resumption.sel(3)[simp del]

lemma results_DONE [simp]: "results (DONE x) = {x}"

lemma results_ABORT [simp]: "results ABORT = {}"

lemma outputs_ABORT [simp]: "outputs ABORT = {}"

lemma outputs_DONE [simp]: "outputs (DONE x) = {}"

lemma is_Done_cases [cases pred]:
assumes "is_Done r"
obtains (DONE) x where "r = DONE x" | (ABORT) "r = ABORT"
using assms by(cases r) auto

lemma not_is_Done_conv_Pause: "¬ is_Done r ⟷ (∃out c. r = Pause out c)"
by(cases r) auto

lemma Done_bind [code]:
"Done a ⤜ f = (case a of None ⇒ Done None | Some a ⇒ f a)"
by(rule resumption.expand)(auto split: option.split)

lemma DONE_bind [simp]:
"DONE a ⤜ f = f a"

lemma bind_resumption_Pause [simp, code]: fixes cont shows
"Pause out cont ⤜ f
= Pause out (λinp. cont inp ⤜ f)"
by(rule resumption.expand)(simp_all)

lemma bind_DONE [simp]:
"x ⤜ DONE = x"
by(coinduction arbitrary: x)(auto simp add: split_beta o_def)

lemma bind_bind_resumption:
fixes r :: "('a, 'in, 'out) resumption"
shows "(r ⤜ f) ⤜ g = do { x ← r; f x ⤜ g }"
apply(coinduction arbitrary: r rule: resumption.coinduct_strong)
apply(case_tac [!] "result r")
apply simp_all
done

lemmas resumption_monad = DONE_bind bind_DONE bind_bind_resumption

lemma ABORT_bind [simp]: "ABORT ⤜ f = ABORT"

lemma bind_resumption_is_Done: "is_Done f ⟹ f ⤜ g = (if result f = None then ABORT else g (the (result f)))"
by(rule resumption.expand) auto

lemma bind_resumption_eq_Done_iff [simp]:
"f ⤜ g = Done x ⟷ (∃y. f = DONE y ∧ g y = Done x) ∨ f = ABORT ∧ x = None"
by(cases f)(auto simp add: Done_bind split: option.split)

lemma bind_resumption_cong:
assumes "x = y"
and "⋀z. z ∈ results y ⟹ f z = g z"
shows "x ⤜ f = y ⤜ g"
using assms(2) unfolding ‹x = y›
proof(coinduction arbitrary: y rule: resumption.coinduct_strong)
case Eq_resumption thus ?case
by(auto intro: resumption.set_sel simp add: is_Done_def rel_fun_def)
(fastforce del: exI intro!: exI intro: resumption.set_sel(2) simp add: is_Done_def)
qed

lemma results_bind_resumption: (* Move to Resumption *)
"results (bind_resumption x f) = (⋃a∈results x. results (f a))"
(is "?lhs = ?rhs")
proof(intro set_eqI iffI)
show "z ∈ ?rhs" if "z ∈ ?lhs" for z using that
proof(induction r≡"x ⤜ f" arbitrary: x)
case (Done z z' x)
from Done(1) Done(2)[symmetric] show ?case by(auto)
next
case (Pause out c r z x)
then show ?case
proof(cases x)
case (Done x')
show ?thesis
proof(cases x')
case None
with Done Pause(4) show ?thesis by(auto simp add: ABORT_def[symmetric])
next
case (Some x'')
thus ?thesis using Pause(1,2,4) Done
by(auto 4 3 simp add: DONE_def[unfolded o_def, symmetric, unfolded fun_eq_iff] dest: sym)
qed
qed(fastforce)
qed
next
fix z
assume "z ∈ ?rhs"
then obtain z' where z': "z' ∈ results x"
and z: "z ∈ results (f z')" by blast
from z' show "z ∈ ?lhs"
proof(induction z'≡z' x)
case (Done r)
then show ?case using z
by(auto simp add: DONE_def[unfolded o_def, symmetric, unfolded fun_eq_iff])
qed auto
qed

lemma outputs_bind_resumption [simp]:
"outputs (bind_resumption r f) = outputs r ∪ (⋃x∈results r. outputs (f x))"
(is "?lhs = ?rhs")
proof(rule set_eqI iffI)+
show "x ∈ ?rhs" if "x ∈ ?lhs" for x using that
proof(induction r'≡"bind_resumption r f" arbitrary: r)
case (Pause1 out c)
thus ?case by(cases r)(auto simp add: Done_bind split: option.split_asm dest: sym)
next
case (Pause2 out c r' x)
thus ?case by(cases r)(auto 4 3 simp add: Done_bind split: option.split_asm dest: sym)
qed
next
fix x
assume "x ∈ ?rhs"
then consider (left) "x ∈ outputs r" | (right) a where "a ∈ results r" "x ∈ outputs (f a)" by auto
then show "x ∈ ?lhs"
proof cases
{ case left  thus ?thesis by induction auto }
{ case right thus ?thesis by induction(auto simp add: Done_bind) }
qed
qed

primrec ensure :: "bool ⇒ (unit, 'out, 'in) resumption"
where
"ensure True = DONE ()"
| "ensure False = ABORT"

lemma is_Done_map_resumption [simp]:
"is_Done (map_resumption f1 f2 r) ⟷ is_Done r"
by(cases r) simp_all

lemma result_map_resumption [simp]:
"is_Done r ⟹ result (map_resumption f1 f2 r) = map_option f1 (result r)"

lemma output_map_resumption [simp]:
"¬ is_Done r ⟹ output (map_resumption f1 f2 r) = f2 (output r)"
by(cases r) simp_all

lemma resume_map_resumption [simp]:
"¬ is_Done r
⟹ resume (map_resumption f1 f2 r) = map_resumption f1 f2 ∘ resume r"
by(cases r) simp_all

lemma rel_resumption_is_DoneD: "rel_resumption A B r1 r2 ⟹ is_Done r1 ⟷ is_Done r2"
by(cases r1 r2 rule: resumption.exhaust[case_product resumption.exhaust]) simp_all

lemma rel_resumption_resultD1:
"⟦ rel_resumption A B r1 r2; is_Done r1 ⟧ ⟹ rel_option A (result r1) (result r2)"
by(cases r1 r2 rule: resumption.exhaust[case_product resumption.exhaust]) simp_all

lemma rel_resumption_resultD2:
"⟦ rel_resumption A B r1 r2; is_Done r2 ⟧ ⟹ rel_option A (result r1) (result r2)"
by(cases r1 r2 rule: resumption.exhaust[case_product resumption.exhaust]) simp_all

lemma rel_resumption_outputD1:
"⟦ rel_resumption A B r1 r2; ¬ is_Done r1 ⟧ ⟹ B (output r1) (output r2)"
by(cases r1 r2 rule: resumption.exhaust[case_product resumption.exhaust]) simp_all

lemma rel_resumption_outputD2:
"⟦ rel_resumption A B r1 r2; ¬ is_Done r2 ⟧ ⟹ B (output r1) (output r2)"
by(cases r1 r2 rule: resumption.exhaust[case_product resumption.exhaust]) simp_all

lemma rel_resumption_resumeD1:
"⟦ rel_resumption A B r1 r2; ¬ is_Done r1 ⟧
⟹ rel_resumption A B (resume r1 inp) (resume r2 inp)"
by(cases r1 r2 rule: resumption.exhaust[case_product resumption.exhaust])(auto dest: rel_funD)

lemma rel_resumption_resumeD2:
"⟦ rel_resumption A B r1 r2; ¬ is_Done r2 ⟧
⟹ rel_resumption A B (resume r1 inp) (resume r2 inp)"
by(cases r1 r2 rule: resumption.exhaust[case_product resumption.exhaust])(auto dest: rel_funD)

lemma rel_resumption_coinduct
[consumes 1, case_names Done Pause,
case_conclusion Done is_Done result,
case_conclusion Pause "output" resume,
coinduct pred: rel_resumption]:
assumes X: "X r1 r2"
and Done: "⋀r1 r2. X r1 r2 ⟹ (is_Done r1 ⟷ is_Done r2) ∧ (is_Done r1 ⟶ is_Done r2 ⟶ rel_option A (result r1) (result r2))"
and Pause: "⋀r1 r2. ⟦ X r1 r2; ¬ is_Done r1; ¬ is_Done r2 ⟧ ⟹ B (output r1) (output r2) ∧ (∀inp. X (resume r1 inp) (resume r2 inp))"
shows "rel_resumption A B r1 r2"
using X
apply(rule resumption.rel_coinduct)
apply(unfold rel_fun_def)
apply(rule conjI)
apply(erule Done[THEN conjunct1])
apply(rule conjI)
apply(erule Done[THEN conjunct2])
apply(rule impI)+
apply(drule (2) Pause)
apply blast
done

subsection ‹Setup for ‹partial_function››

context includes lifting_syntax begin

coinductive resumption_ord :: "('a, 'out, 'in) resumption ⇒ ('a, 'out, 'in) resumption ⇒ bool"
where
Done_Done: "flat_ord None a a' ⟹ resumption_ord (Done a) (Done a')"
| Done_Pause: "resumption_ord ABORT (Pause out c)"
| Pause_Pause: "((=) ===> resumption_ord) c c' ⟹ resumption_ord (Pause out c) (Pause out c')"

inductive_simps resumption_ord_simps [simp]:
"resumption_ord (Pause out c) r"
"resumption_ord r (Done a)"

lemma resumption_ord_is_DoneD:
"⟦ resumption_ord r r'; is_Done r' ⟧ ⟹ is_Done r"

lemma resumption_ord_resultD:
"⟦ resumption_ord r r'; is_Done r' ⟧ ⟹ flat_ord None (result r) (result r')"

lemma resumption_ord_outputD:
"⟦ resumption_ord r r'; ¬ is_Done r ⟧ ⟹ output r = output r'"
by(cases r) auto

lemma resumption_ord_resumeD:
"⟦ resumption_ord r r'; ¬ is_Done r ⟧ ⟹ ((=) ===> resumption_ord) (resume r) (resume r')"
by(cases r) auto

lemma resumption_ord_abort:
"⟦ resumption_ord r r'; is_Done r; ¬ is_Done r' ⟧ ⟹ result r = None"
by(auto elim: resumption_ord.cases)

lemma resumption_ord_coinduct [consumes 1, case_names Done Abort Pause, case_conclusion Pause "output" resume, coinduct pred: resumption_ord]:
assumes "X r r'"
and Done: "⋀r r'. ⟦ X r r'; is_Done r' ⟧ ⟹ is_Done r ∧ flat_ord None (result r) (result r')"
and Abort: "⋀r r'. ⟦ X r r'; ¬ is_Done r'; is_Done r ⟧ ⟹ result r = None"
and Pause: "⋀r r'. ⟦ X r r'; ¬ is_Done r; ¬ is_Done r' ⟧
⟹ output r = output r' ∧ ((=) ===> (λr r'. X r r' ∨ resumption_ord r r')) (resume r) (resume r')"
shows "resumption_ord r r'"
using ‹X r r'›
proof coinduct
case (resumption_ord r r')
thus ?case
by(cases r r' rule: resumption.exhaust[case_product resumption.exhaust])(auto dest: Done Pause Abort)
qed

end

lemma resumption_ord_ABORT [intro!, simp]: "resumption_ord ABORT r"

lemma resumption_ord_ABORT2 [simp]: "resumption_ord r ABORT ⟷ r = ABORT"

lemma resumption_ord_DONE1 [simp]: "resumption_ord (DONE x) r ⟷ r = DONE x"
by(cases r)(auto simp add: option_ord_Some1_iff DONE_def dest: resumption_ord_abort)

lemma resumption_ord_refl: "resumption_ord r r"
by(coinduction arbitrary: r)(auto simp add: flat_ord_def)

lemma resumption_ord_antisym:
"⟦ resumption_ord r r'; resumption_ord r' r ⟧
⟹ r = r'"
proof(coinduction arbitrary: r r' rule: resumption.coinduct_strong)
case (Eq_resumption r r')
thus ?case
by cases(auto simp add: flat_ord_def rel_fun_def)
qed

lemma resumption_ord_trans:
"⟦ resumption_ord r r'; resumption_ord r' r'' ⟧
⟹ resumption_ord r r''"
proof(coinduction arbitrary: r r' r'')
case (Done r r' r'')
thus ?case by(auto 4 4 elim: resumption_ord.cases simp add: flat_ord_def)
next
case (Abort r r' r'')
thus ?case by(auto 4 4 elim: resumption_ord.cases simp add: flat_ord_def)
next
case (Pause r r' r'')
hence "resumption_ord r r'" "resumption_ord r' r''" by simp_all
thus ?case using ‹¬ is_Done r› ‹¬ is_Done r''›
qed

primcorec resumption_lub :: "('a, 'out, 'in) resumption set ⇒ ('a, 'out, 'in) resumption"
where
"∀r ∈ R. is_Done r ⟹ is_Done (resumption_lub R)"
| "result (resumption_lub R) = flat_lub None (result ` R)"
| "output (resumption_lub R) = (THE out. out ∈ output ` (R ∩ {r. ¬ is_Done r}))"
| "resume (resumption_lub R) = (λinp. resumption_lub ((λc. c inp) ` resume ` (R ∩ {r. ¬ is_Done r})))"

lemma is_Done_resumption_lub [simp]:
"is_Done (resumption_lub R) ⟷ (∀r ∈ R. is_Done r)"

lemma result_resumption_lub [simp]:
"∀r ∈ R. is_Done r ⟹ result (resumption_lub R) = flat_lub None (result ` R)"

lemma output_resumption_lub [simp]:
"∃r∈R. ¬ is_Done r ⟹ output (resumption_lub R) = (THE out. out ∈ output ` (R ∩ {r. ¬ is_Done r}))"

lemma resume_resumption_lub [simp]:
"∃r∈R. ¬ is_Done r
⟹ resume (resumption_lub R) inp =
resumption_lub ((λc. c inp) ` resume ` (R ∩ {r. ¬ is_Done r}))"

lemma resumption_lub_empty: "resumption_lub {} = ABORT"

context
fixes R state inp R'
defines R'_def: "R' ≡ (λc. c inp) ` resume ` (R ∩ {r. ¬ is_Done r})"
assumes chain: "Complete_Partial_Order.chain resumption_ord R"
begin

lemma resumption_ord_chain_resume: "Complete_Partial_Order.chain resumption_ord R'"
proof(rule chainI)
fix r' r''
assume "r' ∈ R'"
and "r'' ∈ R'"
then obtain 𝗋' 𝗋''
where r': "r' = resume 𝗋' inp" "𝗋' ∈ R" "¬ is_Done 𝗋'"
and r'': "r'' = resume 𝗋'' inp" "𝗋'' ∈ R" "¬ is_Done 𝗋''"
from chain ‹𝗋' ∈ R› ‹𝗋'' ∈ R›
have "resumption_ord 𝗋' 𝗋'' ∨ resumption_ord 𝗋'' 𝗋'"
by(auto elim: chainE)
with r' r''
have "resumption_ord (resume 𝗋' inp) (resume 𝗋'' inp) ∨
resumption_ord (resume 𝗋'' inp) (resume 𝗋' inp)"
by(auto elim: resumption_ord.cases simp add: rel_fun_def)
with r' r''
show "resumption_ord r' r'' ∨ resumption_ord r'' r'" by auto
qed

end

lemma resumption_partial_function_definition:
"partial_function_definitions resumption_ord resumption_lub"
proof
show "resumption_ord r r" for r :: "('a, 'b, 'c) resumption" by(rule resumption_ord_refl)
show "resumption_ord r r''" if "resumption_ord r r'" "resumption_ord r' r''"
for r r' r'' :: "('a, 'b, 'c) resumption" using that by(rule resumption_ord_trans)
show "r = r'" if "resumption_ord r r'" "resumption_ord r' r" for r r' :: "('a, 'b, 'c) resumption"
using that by(rule resumption_ord_antisym)
next
fix R and r :: "('a, 'b, 'c) resumption"
assume "Complete_Partial_Order.chain resumption_ord R" "r ∈ R"
thus "resumption_ord r (resumption_lub R)"
proof(coinduction arbitrary: r R)
case (Done r R)
note chain = ‹Complete_Partial_Order.chain resumption_ord R›
and r = ‹r ∈ R›
from ‹is_Done (resumption_lub R)› have A: "∀r ∈ R. is_Done r" by simp
with r obtain a' where "r = Done a'" by(cases r) auto
{ fix r'
assume "a' ≠ None"
hence "(THE x. x ∈ result ` R ∧ x ≠ None) = a'"
using r A ‹r = Done a'›
by(auto 4 3 del: the_equality intro!: the_equality intro: rev_image_eqI elim: chainE[OF chain] simp add: flat_ord_def is_Done_def)
}
with A r ‹r = Done a'› show ?case
by(cases a')(auto simp add: flat_ord_def flat_lub_def)
next
case (Abort r R)
hence chain: "Complete_Partial_Order.chain resumption_ord R" and "r ∈ R" by simp_all
from ‹r ∈ R› ‹¬ is_Done (resumption_lub R)› ‹is_Done r›
show ?case by(auto elim: chainE[OF chain] dest: resumption_ord_abort resumption_ord_is_DoneD)
next
case (Pause r R)
hence chain: "Complete_Partial_Order.chain resumption_ord R"
and r: "r ∈ R" by simp_all
have ?resume
using r ‹¬ is_Done r› resumption_ord_chain_resume[OF chain]
moreover
from r ‹¬ is_Done r› have "output (resumption_lub R) = output r"
by(auto 4 4 simp add: bexI del: the_equality intro!: the_equality elim: chainE[OF chain] dest: resumption_ord_outputD)
ultimately show ?case by simp
qed
next
fix R and r :: "('a, 'b, 'c) resumption"
assume "Complete_Partial_Order.chain resumption_ord R" "⋀r'. r' ∈ R ⟹ resumption_ord r' r"
thus "resumption_ord (resumption_lub R) r"
proof(coinduction arbitrary: R r)
case (Done R r)
hence chain: "Complete_Partial_Order.chain resumption_ord R"
and ub: "∀r'∈R. resumption_ord r' r" by simp_all
from ‹is_Done r› ub have is_Done: "∀r' ∈ R. is_Done r'"
and ub': "⋀r'. r' ∈ result ` R ⟹ flat_ord None r' (result r)"
by(auto dest: resumption_ord_is_DoneD resumption_ord_resultD)
from is_Done have chain': "Complete_Partial_Order.chain (flat_ord None) (result ` R)"
by(auto 5 2 intro!: chainI elim: chainE[OF chain] dest: resumption_ord_resultD)
hence "flat_ord None (flat_lub None (result ` R)) (result r)"
by(rule partial_function_definitions.lub_least[OF flat_interpretation])(rule ub')
thus ?case using is_Done by simp
next
case (Abort R r)
hence chain: "Complete_Partial_Order.chain resumption_ord R"
and ub: "∀r'∈R. resumption_ord r' r" by simp_all
from ‹¬ is_Done r› ‹is_Done (resumption_lub R)› ub
show ?case by(auto simp add: flat_lub_def dest: resumption_ord_abort)
next
case (Pause R r)
hence chain: "Complete_Partial_Order.chain resumption_ord R"
and ub: "⋀r'. r'∈R ⟹ resumption_ord r' r" by simp_all
from ‹¬ is_Done (resumption_lub R)› have exR: "∃r ∈ R. ¬ is_Done r" by simp
then obtain r' where r': "r' ∈ R" "¬ is_Done r'" by auto
with ub[of r'] have "output r = output r'" by(auto dest: resumption_ord_outputD)
also have [symmetric]: "output (resumption_lub R) = output r'" using exR r'
by(auto 4 4 elim: chainE[OF chain] dest: resumption_ord_outputD)
finally have ?output ..
moreover
{ fix inp r''
assume "r'' ∈ R" "¬ is_Done r''"
with ub[of r'']
have "resumption_ord (resume r'' inp) (resume r inp)"
by(auto dest!: resumption_ord_resumeD simp add: rel_fun_def) }
with exR resumption_ord_chain_resume[OF chain] r'
have ?resume by(auto simp add: rel_fun_def)
ultimately show ?case ..
qed
qed

interpretation resumption:
partial_function_definitions resumption_ord resumption_lub
rewrites "resumption_lub {} = (ABORT :: ('a, 'b, 'c) resumption)"
by (rule resumption_partial_function_definition resumption_lub_empty)+

declaration ‹Partial_Function.init "resumption" @{term resumption.fixp_fun}
@{term resumption.mono_body} @{thm resumption.fixp_rule_uc} @{thm resumption.fixp_induct_uc} NONE›

abbreviation "mono_resumption ≡ monotone (fun_ord resumption_ord) resumption_ord"

lemma mono_resumption_resume:
assumes "mono_resumption B"
shows "mono_resumption (λf. resume (B f) inp)"
proof
fix f g :: "'a ⇒ ('b, 'c, 'd) resumption"
assume fg: "fun_ord resumption_ord f g"
hence "resumption_ord (B f) (B g)" by(rule monotoneD[OF assms])
with resumption_ord_resumeD[OF this]
show "resumption_ord (resume (B f) inp) (resume (B g) inp)"
by(cases "is_Done (B f)")(auto simp add: rel_fun_def is_Done_def)
qed

lemma bind_resumption_mono [partial_function_mono]:
assumes mf: "mono_resumption B"
and mg: "⋀y. mono_resumption (C y)"
shows "mono_resumption (λf. do { y ← B f; C y f })"
proof(rule monotoneI)
fix f g :: "'a ⇒ ('b, 'c, 'd) resumption"
assume *: "fun_ord resumption_ord f g"
define f' where "f' ≡ B f" define g' where "g' ≡ B g"
define h where "h ≡ λx. C x f" define k where "k ≡ λx. C x g"
from mf[THEN monotoneD, OF *] mg[THEN monotoneD, OF *] f'_def g'_def h_def k_def
have "resumption_ord f' g'" "⋀x. resumption_ord (h x) (k x)" by auto
thus "resumption_ord (f' ⤜ h) (g' ⤜ k)"
proof(coinduction arbitrary: f' g' h k)
case (Done f' g' h k)
hence le: "resumption_ord f' g'"
and mg: "⋀y. resumption_ord (h y) (k y)" by simp_all
from ‹is_Done (g' ⤜ k)›
have done_Bg: "is_Done g'"
and "result g' ≠ None ⟹ is_Done (k (the (result g')))" by simp_all
moreover
have "is_Done f'" using le done_Bg by(rule resumption_ord_is_DoneD)
moreover
from le done_Bg have "flat_ord None (result f') (result g')"
by(rule resumption_ord_resultD)
hence "result f' ≠ None ⟹ result g' = result f'"
moreover
have "resumption_ord (h (the (result f'))) (k (the (result f')))" by(rule mg)
ultimately show ?case
by(subst (1 2) result_bind_resumption)(auto dest: resumption_ord_is_DoneD resumption_ord_resultD simp add: flat_ord_def bind_eq_None_conv)
next
case (Abort f' g' h k)
hence "resumption_ord (h (the (result f'))) (k (the (result f')))" by simp
thus ?case using Abort
by(cases "is_Done g'")(auto 4 4 simp add: bind_eq_None_conv flat_ord_def dest: resumption_ord_abort resumption_ord_resultD resumption_ord_is_DoneD)
next
case (Pause f' g' h k)
hence ?output
by(auto 4 4 dest: resumption_ord_outputD resumption_ord_is_DoneD resumption_ord_resultD resumption_ord_abort simp add: flat_ord_def)
moreover have ?resume
proof(cases "is_Done f'")
case False
with Pause show ?thesis
by(auto simp add: rel_fun_def dest: resumption_ord_is_DoneD intro: resumption_ord_resumeD[THEN rel_funD] del: exI intro!: exI)
next
case True
hence "is_Done g'" using Pause by(auto dest: resumption_ord_abort)
thus ?thesis using True Pause resumption_ord_resultD[OF ‹resumption_ord f' g'›]
by(auto del: rel_funI intro!: rel_funI simp add: bind_resumption_is_Done flat_ord_def intro: resumption_ord_resumeD[THEN rel_funD] exI[where x=f'] exI[where x=g'])
qed
ultimately show ?case ..
qed
qed

lemma fixes f F
defines "F ≡ λresults r. case r of resumption.Done x ⇒ set_option x | resumption.Pause out c ⇒ ⋃input. results (c input)"
shows results_conv_fixp: "results ≡ ccpo.fixp (fun_lub Union) (fun_ord (⊆)) F" (is "_ ≡ ?fixp")
and results_mono: "⋀x. monotone (fun_ord (⊆)) (⊆) (λf. F f x)" (is "PROP ?mono")
proof(rule eq_reflection ext antisym subsetI)+
show mono: "PROP ?mono" unfolding F_def by(tactic ‹Partial_Function.mono_tac @{context} 1›)
fix x r
show "?fixp r ⊆ results r"
by(induction arbitrary: r rule: lfp.fixp_induct_uc[of "λx. x" F "λx. x", OF mono reflexive refl])
(fastforce simp add: F_def split: resumption.split_asm)+

assume "x ∈ results r"
thus "x ∈ ?fixp r" by induct(subst lfp.mono_body_fixp[OF mono]; auto simp add: F_def)+
qed

lemma mcont_case_resumption:
fixes f g
defines "h ≡ λr. if is_Done r then f (result r) else g (output r) (resume r) r"
assumes mcont1: "mcont (flat_lub None) option_ord lub ord f"
and mcont2: "⋀out. mcont (fun_lub resumption_lub) (fun_ord resumption_ord) lub ord (λc. g out c (Pause out c))"
and ccpo: "class.ccpo lub ord (mk_less ord)"
and bot: "⋀x. ord (f None) x"
shows "mcont resumption_lub resumption_ord lub ord (λr. case r of Done x ⇒ f x | Pause out c ⇒ g out c r)"
(is "mcont ?lub ?ord _ _ ?f")
proof(rule resumption.mcont_if_bot[OF ccpo bot, where bound=ABORT and f=h])
show "?f x = (if ?ord x ABORT then f None else h x)" for x
show "ord (h x) (h y)" if "?ord x y" "¬ ?ord x ABORT" for x y using that
by(cases x)(simp_all add: h_def mcont_monoD[OF mcont1] fun_ord_conv_rel_fun mcont_monoD[OF mcont2])

fix Y :: "('a, 'b, 'c) resumption set"
assume chain: "Complete_Partial_Order.chain ?ord Y"
and Y: "Y ≠ {}"
and nbot: "⋀x. x ∈ Y ⟹ ¬ ?ord x ABORT"
show "h (?lub Y) = lub (h ` Y)"
proof(cases "∃x. DONE x ∈ Y")
case True
then obtain x where x: "DONE x ∈ Y" ..
have is_Done: "is_Done r" if "r ∈ Y" for r using chainD[OF chain that x]
by(auto dest: resumption_ord_is_DoneD)
from is_Done have chain': "Complete_Partial_Order.chain (flat_ord None) (result ` Y)"
by(auto 5 2 intro!: chainI elim: chainE[OF chain] dest: resumption_ord_resultD)
from is_Done have "is_Done (?lub Y)" "Y ∩ {r. is_Done r} = Y" "Y ∩ {r. ¬ is_Done r} = {}" by auto
then show ?thesis using Y by(simp add: h_def mcont_contD[OF mcont1 chain'] image_image)
next
case False
have is_Done: "¬ is_Done r" if "r ∈ Y" for r using that False nbot
by(auto elim!: is_Done_cases)
from Y obtain out c where Pause: "Pause out c ∈ Y"
by(auto 5 2 dest: is_Done iff: not_is_Done_conv_Pause)

have out: "(THE out. out ∈ output ` (Y ∩ {r. ¬ is_Done r})) = out" using Pause
by(auto 4 3 intro: rev_image_eqI iff: not_is_Done_conv_Pause dest: chainD[OF chain])
have "(λr. g (output r) (resume r) r) ` (Y ∩ {r. ¬ is_Done r}) = (λr. g out (resume r) r) ` (Y ∩ {r. ¬ is_Done r})"
by(auto 4 3 simp add: not_is_Done_conv_Pause dest: chainD[OF chain Pause] intro: rev_image_eqI)
moreover have "¬ is_Done (?lub Y)" using Y is_Done by(auto)
moreover from is_Done have "Y ∩ {r. is_Done r} = {}" "Y ∩ {r. ¬ is_Done r} = Y" by auto
moreover have "(λinp. resumption_lub ((λx. resume x inp) ` Y)) = fun_lub resumption_lub (resume ` Y)"
by(auto simp add: fun_lub_def fun_eq_iff intro!: arg_cong[where f="resumption_lub"])
moreover have "resumption_lub Y = Pause out (fun_lub resumption_lub (resume ` Y))"
using Y is_Done out
by(intro resumption.expand)(auto simp add: fun_lub_def fun_eq_iff image_image intro!: arg_cong[where f=resumption_lub])
moreover have chain': "Complete_Partial_Order.chain resumption.le_fun (resume ` Y)" using chain
by(rule chain_imageI)(auto dest!: is_Done simp add: not_is_Done_conv_Pause fun_ord_conv_rel_fun)
moreover have "(λr. g out (resume r) (Pause out (resume r))) ` Y = (λr. g out (resume r) r) ` Y"
by(intro image_cong[OF refl])(frule nbot; auto dest!: chainD[OF chain Pause] elim: resumption_ord.cases)
ultimately show ?thesis using False out Y
by(simp add: h_def image_image mcont_contD[OF mcont2])
qed
qed

lemma mcont2mcont_results[THEN mcont2mcont, cont_intro, simp]:
shows mcont_results: "mcont resumption_lub resumption_ord Union (⊆) results"
apply(rule mcont_case_resumption)
done

lemma mono2mono_results[THEN lfp.mono2mono, cont_intro, simp]:
shows monotone_results: "monotone resumption_ord (⊆) results"
using mcont_results by(rule mcont_mono)

lemma fixes f F
defines "F ≡ λoutputs xs. case xs of resumption.Done x ⇒ {} | resumption.Pause out c ⇒ insert out (⋃input. outputs (c input))"
shows outputs_conv_fixp: "outputs ≡ ccpo.fixp (fun_lub Union) (fun_ord (⊆)) F" (is "_ ≡ ?fixp")
and outputs_mono: "⋀x. monotone (fun_ord (⊆)) (⊆) (λf. F f x)" (is "PROP ?mono")
proof(rule eq_reflection ext antisym subsetI)+
show mono: "PROP ?mono" unfolding F_def by(tactic ‹Partial_Function.mono_tac @{context} 1›)
show "?fixp r ⊆ outputs r" for r
by(induct arbitrary: r rule: lfp.fixp_induct_uc[of "λx. x" F "λx. x", OF mono reflexive refl])(auto simp add: F_def split: resumption.split)
show "x ∈ ?fixp r" if "x ∈ outputs r" for x r using that
by induct(subst lfp.mono_body_fixp[OF mono]; auto simp add: F_def; fail)+
qed

lemma mcont2mcont_outputs[THEN lfp.mcont2mcont, cont_intro, simp]:
shows mcont_outputs: "mcont resumption_lub resumption_ord Union (⊆) outputs"
apply(rule lfp.fixp_preserves_mcont1[OF outputs_mono outputs_conv_fixp])
apply(auto intro: lfp.mcont2mcont intro!: mcont2mcont_insert mcont_SUP mcont_case_resumption)
done

lemma mono2mono_outputs[THEN lfp.mono2mono, cont_intro, simp]:
shows monotone_outputs: "monotone resumption_ord (⊆) outputs"
using mcont_outputs by(rule mcont_mono)

lemma pred_resumption_antimono:
assumes r: "pred_resumption A C r'"
and le: "resumption_ord r r'"
shows "pred_resumption A C r"
using r monotoneD[OF monotone_results le] monotoneD[OF monotone_outputs le]

subsection ‹Setup for lifting and transfer›

declare resumption.rel_eq [id_simps, relator_eq]
declare resumption.rel_mono [relator_mono]

lemma rel_resumption_OO [relator_distr]:
"rel_resumption A B OO rel_resumption C D = rel_resumption (A OO C) (B OO D)"

lemma left_total_rel_resumption [transfer_rule]:
"⟦ left_total R1; left_total R2 ⟧ ⟹ left_total (rel_resumption R1 R2)"
by(simp only: left_total_alt_def resumption.rel_eq[symmetric] resumption.rel_conversep[symmetric] rel_resumption_OO resumption.rel_mono)

lemma left_unique_rel_resumption [transfer_rule]:
"⟦ left_unique R1; left_unique R2 ⟧ ⟹ left_unique (rel_resumption R1 R2)"
by(simp only: left_unique_alt_def resumption.rel_eq[symmetric] resumption.rel_conversep[symmetric] rel_resumption_OO resumption.rel_mono)

lemma right_total_rel_resumption [transfer_rule]:
"⟦ right_total R1; right_total R2 ⟧ ⟹ right_total (rel_resumption R1 R2)"
by(simp only: right_total_alt_def resumption.rel_eq[symmetric] resumption.rel_conversep[symmetric] rel_resumption_OO resumption.rel_mono)

lemma right_unique_rel_resumption [transfer_rule]:
"⟦ right_unique R1; right_unique R2 ⟧ ⟹ right_unique (rel_resumption R1 R2)"
by(simp only: right_unique_alt_def resumption.rel_eq[symmetric] resumption.rel_conversep[symmetric] rel_resumption_OO resumption.rel_mono)

lemma bi_total_rel_resumption [transfer_rule]:
"⟦ bi_total A; bi_total B ⟧ ⟹ bi_total (rel_resumption A B)"
unfolding bi_total_alt_def
by(blast intro: left_total_rel_resumption right_total_rel_resumption)

lemma bi_unique_rel_resumption [transfer_rule]:
"⟦ bi_unique A; bi_unique B ⟧ ⟹ bi_unique (rel_resumption A B)"
unfolding bi_unique_alt_def
by(blast intro: left_unique_rel_resumption right_unique_rel_resumption)

lemma Quotient_resumption [quot_map]:
"⟦ Quotient R1 Abs1 Rep1 T1; Quotient R2 Abs2 Rep2 T2 ⟧
⟹ Quotient (rel_resumption R1 R2) (map_resumption Abs1 Abs2) (map_resumption Rep1 Rep2) (rel_resumption T1 T2)"
by(simp add: Quotient_alt_def5 resumption.rel_Grp[of UNIV _ UNIV _, symmetric, simplified] resumption.rel_compp resumption.rel_conversep[symmetric] resumption.rel_mono)

end
```