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