Quelle  Resumption.thy

(* 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) = (∪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)"
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]:
  "∃r∈R. ¬ 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]:
  "∃r∈R. ¬ 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 r' r'' 
    where r': "r' = resume r' inp" "r' ∈ R" "¬ is_Done r'"
    and r'': "r'' = resume r'' inp" "r'' ∈ R" "¬ is_Done r''"
    by(auto simp add: R'_def)
  from chain ‹r' ∈ R› ‹r'' ∈ R›
  have "resumption_ord r' r'' ∨ resumption_ord r'' r'"
    by(auto elim: chainE)
  with r' r''
  have "resumption_ord (resume r' inp) (resume r'' inp) ∨
        resumption_ord (resume r'' inp) (resume r' 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