Theory Resumption

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

section ‹The resumption-error monad›

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]

adhoc_overloading Monad_Syntax.bind bind_resumption

lemma is_Done_bind_resumption [simp]:
  "is_Done (x  f)  is_Done x  (result x  None  is_Done (f (the (result x))))"
by(simp add: bind_resumption_def)

lemma result_bind_resumption [simp]:
  "is_Done (x  f)  result (x  f) = result x  result  f"
by(simp add: bind_resumption_def)

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)"
by(simp add: bind_resumption_def)

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))"
by(auto simp add: bind_resumption_def)

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"
by(auto simp add: DONE_def ABORT_def)

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

declare resumption.sel(3)[simp del]

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

lemma results_ABORT [simp]: "results ABORT = {}"
by(simp add: ABORT_def)

lemma outputs_ABORT [simp]: "outputs ABORT = {}"
by(simp add: ABORT_def)

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

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"
by(simp add: DONE_def Done_bind)

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(auto simp add: split_beta bind_eq_Some_conv)
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"
by(simp add: ABORT_def Done_bind)

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) = (aresults 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  (xresults 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)"
by(clarsimp simp add: is_Done_def)

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"
by(cases r')(auto simp add: fun_ord_def)

lemma resumption_ord_resultD:
  " resumption_ord r r'; is_Done r'   flat_ord None (result r) (result r')"
by(cases r')(auto simp add: flat_ord_def)

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"
by(cases r)(simp_all add: flat_ord_def resumption_ord.Done_Pause)

lemma resumption_ord_ABORT2 [simp]: "resumption_ord r ABORT  r = ABORT"
by(simp add: ABORT_def flat_ord_def)

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''
    by(cases)(auto simp add: rel_fun_def)
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)"
by(simp add: resumption_lub_def)

lemma result_resumption_lub [simp]:
  "r  R. is_Done r  result (resumption_lub R) = flat_lub None (result ` R)"
by(simp add: resumption_lub_def)

lemma output_resumption_lub [simp]:
  "rR. ¬ is_Done r  output (resumption_lub R) = (THE out. out  output ` (R  {r. ¬ is_Done r}))"
by(simp add: resumption_lub_def)

lemma resume_resumption_lub [simp]:
  "rR. ¬ is_Done r
   resume (resumption_lub R) inp = 
     resumption_lub ((λc. c inp) ` resume ` (R  {r. ¬ is_Done r}))"
by(simp add: resumption_lub_def)

lemma resumption_lub_empty: "resumption_lub {} = ABORT"
by(subst resumption_lub.code)(simp add: flat_lub_def)

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 𝗋''"
    by(auto simp add: R'_def)
  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]
      by(auto simp add: rel_fun_def bexI)
    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'"
      by(auto simp add: flat_ord_def)
    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
    by(simp add: h_def split: resumption.split)
  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 lfp.fixp_preserves_mcont1[OF results_mono results_conv_fixp])
apply(rule mcont_case_resumption)
apply(simp_all add: mcont_applyI)
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]
by(auto simp add: pred_resumption_def)

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)" 
by(simp add: resumption.rel_compp)

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