Theory DRA_Models

(* Title:      Demonic refinement algebra
   Author:     Alasdair Armstrong, Victor B. F. Gomes, Georg Struth
   Maintainer: Georg Struth <g.struth at sheffield.ac.uk>
*)

section ‹Models for Demonic Refinement Algebra with Tests›

theory DRA_Models
  imports DRAT
begin

text ‹
  We formalise the predicate transformer model of demonic refinement algebra.
  Predicate transformers are formalised as strict and additive functions over a field of sets,
  or alternatively as costrict and multiplicative functions. 
  In the future, this should be merged with Preoteasa's more abstract formalisation~cite"Preoteasa11".
›

no_notation 
  plus (infixl "+" 65) and 
  less_eq  ("'(≤')") and
  less_eq  ("(_/  _)"  [51, 51] 50)

notation comp (infixl "" 55)

type_synonym 'a bfun = "'a set  'a set"

text ‹
  Definitions of signature:
›

definition top :: "'a bfun" where "top  λx. UNIV"
definition bot :: "'a bfun" where "bot  λx. {}"
definition adjoint :: "'a bfun  'a bfun" where "adjoint f  (λp. - f (-p))"

definition fun_inter :: "'a bfun  'a bfun  'a bfun" (infix "" 51) where
  "f  g  λp. f p  g p"

definition fun_union :: "'a bfun  'a bfun  'a bfun" (infix "+" 52) where
  "f + g  λp. f p  g p"

definition fun_order :: "'a bfun  'a bfun  bool" (infix "" 50) where
  "f  g  p. f p  g p"

definition fun_strict_order :: "'a bfun  'a bfun  bool" (infix "<." 50) where
  "f <. g  f  g  f  g"

definition N :: "'a bfun  'a bfun" where
  "N f  ((adjoint f o bot)  id)"

lemma top_max: "f  top"
  by (auto simp: top_def fun_order_def)

lemma bot_min: "bot  f"
  by (auto simp: bot_def fun_order_def)

lemma oder_def: "f  g = f  f  g"
  by (metis fun_inter_def fun_order_def le_iff_inf)

lemma order_def_var: "f  g  f  g = f"
  by (auto simp: fun_inter_def fun_order_def)

lemma adjoint_idem [simp]: "adjoint (adjoint f) = f"
  by (auto simp: adjoint_def)

lemma adjoint_prop1[simp]: "(f o top)  (adjoint f o bot) = bot"
  by (auto simp: fun_inter_def adjoint_def bot_def top_def)

lemma adjoint_prop2[simp]: "(f o top) + (adjoint f o bot) = top"
  by (auto simp: fun_union_def adjoint_def bot_def top_def)

lemma adjoint_mult: "adjoint (f o g) = adjoint f o adjoint g"
  by (auto simp: adjoint_def)

lemma adjoint_top[simp]: "adjoint top = bot"
  by (auto simp: adjoint_def bot_def top_def)

lemma N_comp1: "(N (N f)) + N f = id"
  by (auto simp: fun_union_def N_def fun_inter_def adjoint_def bot_def)

lemma N_comp2: "(N (N f)) o N f = bot"
  by (auto simp: N_def fun_inter_def adjoint_def bot_def)

lemma N_comp3: "N f o (N (N f)) = bot"
  by (auto simp: N_def fun_inter_def adjoint_def bot_def)

lemma N_de_morgan: "N (N f) o N (N g) = N (N f)  N (N g)"
  by (auto simp: fun_union_def N_def fun_inter_def adjoint_def bot_def)

lemma conj_pred_aux [simp]: "(λp. x p  y p) = y  p. x p  y p"
  by (metis Un_upper1)

text ‹
  Next, we define a type for conjuctive or multiplicative predicate transformers.
›

typedef 'a bool_op = "{f::'a bfun. (g h. mono f  f  g + f  h = f  (g + h)  bot o f = bot)}"
  apply (rule_tac x="λx. x" in exI)
  apply auto
  apply (metis monoI)
  by (auto simp: fun_order_def fun_union_def)

setup_lifting type_definition_bool_op

text ‹
  Conjuctive predicate transformers form a dioid with tests without right annihilator.
›

instantiation bool_op :: (type) dioid_one_zerol 
begin
  lift_definition less_eq_bool_op :: "'a bool_op  'a bool_op  bool" is fun_order .

  lift_definition less_bool_op :: "'a bool_op  'a bool_op  bool" is "(<.)" .

  lift_definition zero_bool_op :: "'a bool_op" is "bot"
    by (auto simp: bot_def fun_union_def fun_order_def mono_def)

  lift_definition one_bool_op :: "'a bool_op" is "id"
    by (auto simp: fun_union_def fun_order_def mono_def)

  lift_definition times_bool_op :: "'a bool_op  'a bool_op  'a bool_op" is "(o)" 
    by (auto simp: o_def fun_union_def fun_order_def bot_def mono_def) metis

  lift_definition plus_bool_op :: "'a bool_op  'a bool_op  'a bool_op" is "(+)"
    apply (auto simp: o_def fun_union_def fun_order_def bot_def mono_def)
    apply (metis subsetD)
    apply (metis subsetD)
    apply (rule ext)
    by (metis (no_types, lifting) semilattice_sup_class.sup.assoc semilattice_sup_class.sup.left_commute)

  instance
    by standard (transfer, auto simp: fun_order_def fun_strict_order_def fun_union_def bot_def)+

end

instantiation bool_op :: (type) test_semiring_zerol 
begin
  lift_definition n_op_bool_op :: "'a bool_op  'a bool_op" is "N"
    by (auto simp: N_def fun_inter_def adjoint_def bot_def fun_union_def mono_def)

  instance
  apply standard
  apply (transfer, clarsimp simp add: N_def adjoint_def bot_def id_def comp_def fun_inter_def)
  apply (transfer, clarsimp simp add: N_def adjoint_def bot_def id_def comp_def fun_inter_def fun_union_def mono_def, blast)
  apply (transfer, clarsimp simp add: N_def adjoint_def bot_def comp_def mono_def fun_union_def fun_inter_def)
  by (transfer, clarsimp simp add: N_def adjoint_def bot_def comp_def mono_def fun_union_def fun_inter_def, blast)

end

definition fun_star :: "'a bfun  'a bfun" where
  "fun_star f = lfp (λr. f o r + id)"

definition fun_iteration :: "'a bfun  'a bfun" where
  "fun_iteration f = gfp (λg. f o g + id)"
  
text ‹
  Verifying the iteration laws is left for future work. This could be obtained by integrating
  Preoteasa's approach~cite"Preoteasa11".
›

end