Theory BaseMonad

(***********************************************************************************
 * Copyright (c) 2016-2018 The University of Sheffield, UK
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are met:
 *
 * * Redistributions of source code must retain the above copyright notice, this
 *   list of conditions and the following disclaimer.
 *
 * * Redistributions in binary form must reproduce the above copyright notice,
 *   this list of conditions and the following disclaimer in the documentation
 *   and/or other materials provided with the distribution.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
 * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
 * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
 * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
 * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
 * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
 * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 * 
 * SPDX-License-Identifier: BSD-2-Clause
 ***********************************************************************************)

section‹The Monad Infrastructure›
text‹In this theory, we introduce the basic infrastructure for our monadic class encoding.›
theory BaseMonad
  imports
    "../classes/BaseClass"
    "../preliminaries/Heap_Error_Monad"
begin
subsection‹Datatypes›

datatype exception = NotFoundError | HierarchyRequestError | NotSupportedError | SegmentationFault
  | AssertException | NonTerminationException | InvokeError | TypeError

consts put_M :: 'a
consts get_M :: 'a
consts delete_M :: 'a

lemma sorted_list_of_set_eq [dest]: 
  "sorted_list_of_set (fset x) = sorted_list_of_set (fset y) ⟹ x = y"
  by (metis finite_fset fset_inject sorted_list_of_set(1))


locale l_ptr_kinds_M =
  fixes ptr_kinds :: "'heap ⇒ 'ptr::linorder fset"
begin
definition a_ptr_kinds_M :: "('heap, exception, 'ptr list) prog"
  where
    "a_ptr_kinds_M = do {
      h ← get_heap;
      return (sorted_list_of_set (fset (ptr_kinds h)))
    }"

lemma ptr_kinds_M_ok [simp]: "h ⊢ ok a_ptr_kinds_M"
  by(simp add: a_ptr_kinds_M_def)

lemma ptr_kinds_M_pure [simp]: "pure a_ptr_kinds_M h"
  by (auto simp add: a_ptr_kinds_M_def intro: bind_pure_I)

lemma ptr_kinds_ptr_kinds_M [simp]: "ptr ∈ set |h ⊢ a_ptr_kinds_M|⇩r ⟷ ptr |∈| ptr_kinds h"
  by(simp add: a_ptr_kinds_M_def)

lemma ptr_kinds_M_ptr_kinds [simp]: 
  "h ⊢ a_ptr_kinds_M →⇩r xa ⟷ xa = sorted_list_of_set (fset (ptr_kinds h))"
  by(auto simp add: a_ptr_kinds_M_def)
lemma ptr_kinds_M_ptr_kinds_returns_result [simp]: 
  "h ⊢ a_ptr_kinds_M ⤜ f →⇩r x ⟷ h ⊢ f (sorted_list_of_set (fset (ptr_kinds h))) →⇩r x"
  by(auto simp add: a_ptr_kinds_M_def)
lemma ptr_kinds_M_ptr_kinds_returns_heap [simp]: 
  "h ⊢ a_ptr_kinds_M ⤜ f →⇩h h' ⟷ h ⊢ f (sorted_list_of_set (fset (ptr_kinds h))) →⇩h h'"
  by(auto simp add: a_ptr_kinds_M_def)
end

locale l_get_M = 
  fixes get :: "'ptr ⇒ 'heap ⇒ 'obj option"
  fixes type_wf :: "'heap ⇒ bool"
  fixes ptr_kinds :: "'heap ⇒ 'ptr fset"
  assumes "type_wf h ⟹ ptr |∈| ptr_kinds h ⟹ get ptr h ≠ None"
  assumes "get ptr h ≠ None ⟹ ptr |∈| ptr_kinds h"
begin

definition a_get_M :: "'ptr ⇒ ('obj ⇒ 'result) ⇒  ('heap, exception, 'result) prog"
  where
    "a_get_M ptr getter = (do {
      h ← get_heap;
      (case get ptr h of
        Some res ⇒ return (getter res)
      | None ⇒ error SegmentationFault)
    })"

lemma get_M_pure [simp]: "pure (a_get_M ptr getter) h"
  by(auto simp add: a_get_M_def bind_pure_I split: option.splits)

lemma get_M_ok:
  "type_wf h ⟹ ptr |∈| ptr_kinds h ⟹ h ⊢ ok (a_get_M ptr getter)"
  apply(simp add: a_get_M_def)
  by (metis l_get_M_axioms l_get_M_def option.case_eq_if return_ok)
lemma get_M_ptr_in_heap:
  "h ⊢ ok (a_get_M ptr getter) ⟹ ptr |∈| ptr_kinds h"
  apply(simp add: a_get_M_def)
  by (metis error_returns_result is_OK_returns_result_E l_get_M_axioms l_get_M_def option.simps(4))

end

locale l_put_M = l_get_M get for get :: "'ptr ⇒ 'heap ⇒ 'obj option" +
  fixes put :: "'ptr ⇒ 'obj ⇒ 'heap ⇒ 'heap"
begin
definition a_put_M :: "'ptr ⇒ (('v ⇒ 'v) ⇒ 'obj ⇒ 'obj) ⇒ 'v ⇒ ('heap, exception, unit) prog"
  where
    "a_put_M ptr setter v = (do {
      obj ← a_get_M ptr id;
      h ← get_heap;
      return_heap (put ptr (setter (λ_. v) obj) h)
    })"

lemma put_M_ok:
  "type_wf h ⟹ ptr |∈| ptr_kinds h ⟹ h ⊢ ok (a_put_M ptr setter v)"
  by(auto simp add: a_put_M_def intro!: bind_is_OK_I2 dest: get_M_ok elim!: bind_is_OK_E)

lemma put_M_ptr_in_heap:
  "h ⊢ ok (a_put_M ptr setter v) ⟹ ptr |∈| ptr_kinds h"
  by(auto simp add: a_put_M_def intro!: bind_is_OK_I2 elim: get_M_ptr_in_heap 
      dest: is_OK_returns_result_I elim!: bind_is_OK_E)

end

subsection ‹Setup for Defining Partial Functions›

lemma execute_admissible: 
  "ccpo.admissible (fun_lub (flat_lub (Inl (e::'e)))) (fun_ord (flat_ord (Inl e)))
     ((λa. ∀(h::'heap) h2 (r::'result). h ⊢ a = Inr (r, h2) ⟶ P h h2 r) ∘ Prog)"
proof (unfold comp_def, rule ccpo.admissibleI, clarify)
  fix A :: "('heap ⇒ 'e + 'result × 'heap) set"
  let ?lub = "Prog (fun_lub (flat_lub (Inl e)) A)"
  fix h h2 r
  assume 1: "Complete_Partial_Order.chain (fun_ord (flat_ord (Inl e))) A"
    and 2: "∀xa∈A. ∀h h2 r. h ⊢ Prog xa = Inr (r, h2)  ⟶ P h h2 r"
    and 4: "h ⊢ Prog (fun_lub (flat_lub (Inl e)) A) = Inr (r, h2)"
  have h1:"⋀a. Complete_Partial_Order.chain (flat_ord (Inl e)) {y. ∃f∈A. y = f a}"
    by (rule chain_fun[OF 1])
  show "P h h2 r"
    using CollectD Inl_Inr_False prog.sel chain_fun[OF 1] flat_lub_in_chain[OF chain_fun[OF 1]] 2 4 
    unfolding execute_def fun_lub_def
  proof -
    assume a1: "the_prog (Prog (λx. flat_lub (Inl e) {y. ∃f∈A. y = f x})) h = Inr (r, h2)"
    assume a2: "∀xa∈A. ∀h h2 r. the_prog (Prog xa) h = Inr (r, h2) ⟶ P h h2 r"
    have "Inr (r, h2) ∈ {s. ∃f. f ∈ A ∧ s = f h} ∨ Inr (r, h2) = Inl e"
      using a1 by (metis (lifting) ‹⋀aa a. flat_lub (Inl e) {y. ∃f∈A. y = f aa} = a ⟹ a = Inl e ∨ a ∈ {y. ∃f∈A. y = f aa}› prog.sel)
    then show ?thesis
      using a2 by fastforce
  qed
qed

lemma execute_admissible2:
  "ccpo.admissible (fun_lub (flat_lub (Inl (e::'e)))) (fun_ord (flat_ord (Inl e)))
     ((λa. ∀(h::'heap) h' h2 h2' (r::'result) r'. 
                    h ⊢ a = Inr (r, h2) ⟶ h' ⊢ a = Inr (r', h2') ⟶ P h h' h2 h2' r r') ∘ Prog)"
proof (unfold comp_def, rule ccpo.admissibleI, clarify)
  fix A :: "('heap ⇒ 'e + 'result × 'heap) set"
  let ?lub = "Prog (fun_lub (flat_lub (Inl e)) A)"
  fix h h' h2 h2' r r'
  assume 1: "Complete_Partial_Order.chain (fun_ord (flat_ord (Inl e))) A"
    and 2 [rule_format]: "∀xa∈A. ∀h h' h2 h2' r r'. h ⊢ Prog xa = Inr (r, h2) 
                          ⟶ h' ⊢ Prog xa = Inr (r', h2') ⟶ P h h' h2 h2' r r'"
    and 4: "h ⊢ Prog (fun_lub (flat_lub (Inl e)) A) = Inr (r, h2)"
    and 5: "h' ⊢ Prog (fun_lub (flat_lub (Inl e)) A) = Inr (r', h2')"
  have h1:"⋀a. Complete_Partial_Order.chain (flat_ord (Inl e)) {y. ∃f∈A. y = f a}"
    by (rule chain_fun[OF 1])
  have "h ⊢ ?lub ∈ {y. ∃f∈A. y = f h}"
    using flat_lub_in_chain[OF h1] 4
    unfolding execute_def fun_lub_def
    by (metis (mono_tags, lifting) Collect_cong Inl_Inr_False prog.sel)
  moreover have "h' ⊢ ?lub ∈ {y. ∃f∈A. y = f h'}"
    using flat_lub_in_chain[OF h1] 5
    unfolding execute_def fun_lub_def
    by (metis (no_types, lifting) Collect_cong Inl_Inr_False prog.sel)
  ultimately obtain f where
    "f ∈ A" and
    "h ⊢ Prog f = Inr (r, h2)" and
    "h' ⊢ Prog f = Inr (r', h2')"
    using 1 4 5 
    apply(auto simp add:  chain_def fun_ord_def flat_ord_def execute_def)[1]
    by (metis Inl_Inr_False)
  then show "P h h' h2 h2' r r'"
    by(fact 2)
qed

definition dom_prog_ord :: 
  "('heap, exception, 'result) prog ⇒ ('heap, exception, 'result) prog ⇒ bool" where
  "dom_prog_ord = img_ord (λa b. execute b a) (fun_ord (flat_ord (Inl NonTerminationException)))"

definition dom_prog_lub :: 
  "('heap, exception, 'result) prog set ⇒ ('heap, exception, 'result) prog" where
  "dom_prog_lub = img_lub (λa b. execute b a) Prog (fun_lub (flat_lub (Inl NonTerminationException)))"

lemma dom_prog_lub_empty: "dom_prog_lub {} = error NonTerminationException"
  by(simp add: dom_prog_lub_def img_lub_def fun_lub_def flat_lub_def error_def)

lemma dom_prog_interpretation: "partial_function_definitions dom_prog_ord dom_prog_lub"
proof -
  have "partial_function_definitions (fun_ord (flat_ord (Inl NonTerminationException))) 
                                     (fun_lub (flat_lub (Inl NonTerminationException)))"
    by (rule partial_function_lift) (rule flat_interpretation)
  then show ?thesis
    apply (simp add: dom_prog_lub_def dom_prog_ord_def flat_interpretation execute_def)
    using partial_function_image prog.expand prog.sel by blast
qed

interpretation dom_prog: partial_function_definitions dom_prog_ord dom_prog_lub
  rewrites "dom_prog_lub {} ≡ error NonTerminationException"
  by (fact dom_prog_interpretation)(simp add: dom_prog_lub_empty)

lemma admissible_dom_prog: 
  "dom_prog.admissible (λf. ∀x h h' r. h ⊢ f x →⇩r r ⟶ h ⊢ f x →⇩h h' ⟶ P x h h' r)"
proof (rule admissible_fun[OF dom_prog_interpretation])
  fix x
  show "ccpo.admissible dom_prog_lub dom_prog_ord (λa. ∀h h' r. h ⊢ a →⇩r r ⟶ h ⊢ a →⇩h h' 
         ⟶ P x h h' r)"
    unfolding dom_prog_ord_def dom_prog_lub_def
  proof (intro admissible_image partial_function_lift flat_interpretation)
    show "ccpo.admissible (fun_lub (flat_lub (Inl NonTerminationException))) 
                          (fun_ord (flat_ord (Inl NonTerminationException)))
     ((λa. ∀h h' r. h ⊢ a →⇩r r ⟶ h ⊢ a →⇩h h' ⟶ P x h h' r) ∘ Prog)"
      by(auto simp add: execute_admissible returns_result_def returns_heap_def split: sum.splits)
  next
    show "⋀x y. (λb. b ⊢ x) = (λb. b ⊢ y) ⟹ x = y"
      by(simp add: execute_def prog.expand)
  next
    show "⋀x. (λb. b ⊢ Prog x) = x"
      by(simp add: execute_def)
  qed
qed

lemma admissible_dom_prog2:
  "dom_prog.admissible (λf. ∀x h h2 h' h2' r r2. h ⊢ f x →⇩r r ⟶ h ⊢ f x →⇩h h' 
            ⟶ h2 ⊢ f x →⇩r r2 ⟶ h2 ⊢ f x →⇩h h2' ⟶ P x h h2 h' h2' r r2)"
proof (rule admissible_fun[OF dom_prog_interpretation])
  fix x
  show "ccpo.admissible dom_prog_lub dom_prog_ord (λa. ∀h h2 h' h2' r r2. h ⊢ a →⇩r r 
                   ⟶ h ⊢ a →⇩h h' ⟶ h2 ⊢ a →⇩r r2 ⟶ h2 ⊢ a →⇩h h2' ⟶ P x h h2 h' h2' r r2)"
    unfolding dom_prog_ord_def dom_prog_lub_def
  proof (intro admissible_image partial_function_lift flat_interpretation)
    show "ccpo.admissible (fun_lub (flat_lub (Inl NonTerminationException))) 
                          (fun_ord (flat_ord (Inl NonTerminationException)))
     ((λa. ∀h h2 h' h2' r r2. h ⊢ a →⇩r r ⟶ h ⊢ a →⇩h h' ⟶ h2 ⊢ a →⇩r r2 ⟶ h2 ⊢ a →⇩h h2' 
                 ⟶ P x h h2 h' h2' r r2) ∘ Prog)"
      by(auto simp add: returns_result_def returns_heap_def intro!: ccpo.admissibleI 
          dest!: ccpo.admissibleD[OF execute_admissible2[where P="P x"]] 
          split: sum.splits)
  next
    show "⋀x y. (λb. b ⊢ x) = (λb. b ⊢ y) ⟹ x = y"
      by(simp add: execute_def prog.expand)
  next
    show "⋀x. (λb. b ⊢ Prog x) = x"
      by(simp add: execute_def)
  qed
qed

lemma fixp_induct_dom_prog:
  fixes F :: "'c ⇒ 'c" and
    U :: "'c ⇒ 'b ⇒ ('heap, exception, 'result) prog" and
    C :: "('b ⇒ ('heap, exception, 'result) prog) ⇒ 'c" and
    P :: "'b ⇒ 'heap ⇒ 'heap ⇒ 'result ⇒ bool"
  assumes mono: "⋀x. monotone (fun_ord dom_prog_ord) dom_prog_ord (λf. U (F (C f)) x)"
  assumes eq: "f ≡ C (ccpo.fixp (fun_lub dom_prog_lub) (fun_ord dom_prog_ord) (λf. U (F (C f))))"
  assumes inverse2: "⋀f. U (C f) = f"
  assumes step: "⋀f x h h' r. (⋀x h h' r. h ⊢ (U f x) →⇩r r ⟹ h ⊢ (U f x) →⇩h h' ⟹ P x h h' r) 
    ⟹ h ⊢ (U (F f) x) →⇩r r ⟹ h ⊢ (U (F f) x) →⇩h h' ⟹ P x h h' r"
  assumes defined: "h ⊢ (U f x) →⇩r r" and "h ⊢ (U f x) →⇩h h'"
  shows "P x h h' r"
  using step defined dom_prog.fixp_induct_uc[of U F C, OF mono eq inverse2 admissible_dom_prog, of P]
  by (metis assms(6) error_returns_heap)

declaration ‹Partial_Function.init "dom_prog" @{term dom_prog.fixp_fun}
  @{term dom_prog.mono_body} @{thm dom_prog.fixp_rule_uc} @{thm dom_prog.fixp_induct_uc}
  (SOME @{thm fixp_induct_dom_prog})›


abbreviation "mono_dom_prog ≡ monotone (fun_ord dom_prog_ord) dom_prog_ord"

lemma dom_prog_ordI:
  assumes "⋀h. h ⊢ f →⇩e NonTerminationException ∨ h ⊢ f = h ⊢ g"
  shows "dom_prog_ord f g"
proof(auto simp add: dom_prog_ord_def img_ord_def fun_ord_def flat_ord_def)[1]
  fix x
  assume "x ⊢ f ≠ x ⊢ g"
  then show "x ⊢ f = Inl NonTerminationException"
    using assms[where h=x]
    by(auto simp add: returns_error_def split: sum.splits)
qed

lemma dom_prog_ordE:
  assumes "dom_prog_ord x y"
  obtains "h ⊢ x →⇩e NonTerminationException" | " h ⊢ x = h ⊢ y"
  using assms unfolding dom_prog_ord_def img_ord_def fun_ord_def flat_ord_def
  using returns_error_def by force


lemma bind_mono [partial_function_mono]:
  fixes B :: "('a ⇒ ('heap, exception, 'result) prog) ⇒ ('heap, exception, 'result2) prog"
  assumes mf: "mono_dom_prog B" and mg: "⋀y. mono_dom_prog (λf. C y f)"
  shows "mono_dom_prog (λf. B f ⤜ (λy. C y f))"
proof (rule monotoneI)
  fix f g :: "'a ⇒ ('heap, exception, 'result) prog"
  assume fg: "dom_prog.le_fun f g"
  from mf
  have 1: "dom_prog_ord (B f) (B g)" by (rule monotoneD) (rule fg)
  from mg
  have 2: "⋀y'. dom_prog_ord (C y' f) (C y' g)" by (rule monotoneD) (rule fg)

  have "dom_prog_ord (B f ⤜ (λy. C y f)) (B g ⤜ (λy. C y f))"
    (is "dom_prog_ord ?L ?R")
  proof (rule dom_prog_ordI)
    fix h
    from 1 show "h ⊢ ?L →⇩e NonTerminationException ∨ h ⊢ ?L = h ⊢ ?R"
      apply(rule dom_prog_ordE) 
       apply(auto)[1]
      using bind_cong by fastforce
  qed
  also
  have h1: "dom_prog_ord (B g ⤜ (λy'. C y' f)) (B g ⤜ (λy'. C y' g))"
    (is "dom_prog_ord ?L ?R")
  proof (rule dom_prog_ordI)
    (* { *)
    fix h
    show "h ⊢ ?L →⇩e NonTerminationException ∨ h ⊢ ?L = h ⊢ ?R"
    proof (cases "h ⊢ ok (B g)")
      case True
      then obtain x h' where x: "h ⊢ B g →⇩r x" and h': "h ⊢ B g →⇩h h'"
        by blast
      then have "dom_prog_ord (C x f) (C x g)"
        using 2 by simp
      then show ?thesis
        using x h'
        apply(auto intro!: bind_returns_error_I3 dest: returns_result_eq dest!: dom_prog_ordE)[1]
        apply(auto simp add: execute_bind_simp)[1]
        using "2" dom_prog_ordE by metis
    next
      case False
      then obtain e where e: "h ⊢ B g →⇩e e"
        by(simp add: is_OK_def returns_error_def split: sum.splits)
      have "h ⊢ B g ⤜ (λy'. C y' f) →⇩e e"
        using e by(auto)
      moreover have "h ⊢ B g ⤜ (λy'. C y' g) →⇩e e"
        using e by auto
      ultimately show ?thesis
        using bind_returns_error_eq by metis
    qed
  qed
  finally (dom_prog.leq_trans)
  show "dom_prog_ord (B f ⤜ (λy. C y f)) (B g ⤜ (λy'. C y' g))" .
qed

lemma mono_dom_prog1 [partial_function_mono]:
  fixes g ::  "('a ⇒ ('heap, exception, 'result) prog) ⇒ 'b ⇒ ('heap, exception, 'result) prog"
  assumes "⋀x. (mono_dom_prog (λf. g f x))"
  shows "mono_dom_prog (λf. map_M (g f) xs)"
  using assms
  apply (induct xs) 
  by(auto simp add: call_mono dom_prog.const_mono intro!: bind_mono)

lemma mono_dom_prog2 [partial_function_mono]:
  fixes g ::  "('a ⇒ ('heap, exception, 'result) prog) ⇒ 'b ⇒ ('heap, exception, 'result) prog"
  assumes "⋀x. (mono_dom_prog (λf. g f x))"
  shows "mono_dom_prog (λf. forall_M (g f) xs)"
  using assms
  apply (induct xs) 
  by(auto simp add: call_mono dom_prog.const_mono intro!: bind_mono)

lemma sorted_list_set_cong [simp]: 
  "sorted_list_of_set (fset FS) = sorted_list_of_set (fset FS') ⟷ FS = FS'"
  by auto

end