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: "xaA. 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. fA. 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. fA. y = f x})) h = Inr (r, h2)"
    assume a2: "xaA. 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. fA. y = f aa} = a  a = Inl e  a  {y. fA. 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]: "xaA. 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. fA. y = f a}"
    by (rule chain_fun[OF 1])
  have "h  ?lub  {y. fA. 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. fA. 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