Theory Action_Algebra_Models

(* Title:      Models of Action Algebra
   Author:     Alasdair Armstrong, Georg Struth, Tjark Weber
   Maintainer: Georg Struth <g.struth at sheffield.ac.uk>
               Tjark Weber <tjark.weber at it.uu.se>
*)

section ‹Models of Action Algebras›

theory Action_Algebra_Models
imports Action_Algebra Kleene_Algebra.Kleene_Algebra_Models
begin

subsection ‹The Powerset Action Algebra over a Monoid›

text ‹Here we show that various models of Kleene algebras are also
residuated; hence they form action algebras. In each case the main
work is to establish the residuated lattice structure.›

text ‹The interpretation proofs for some of the following models are
quite similar. One could, perhaps, abstract out common reasoning.›


subsection ‹The Powerset Action Algebra over a Monoid›

instantiation set :: (monoid_mult) residuated_sup_lgroupoid
begin

  definition residual_r_set where
    "X → Z = ⋃ {Y. X ⋅ Y ⊆ Z}"

  definition residual_l_set where
    "Z ← Y = ⋃ {X. X ⋅ Y ⊆ Z}"

  instance
  proof
    fix X Y Z :: "'a set"
    show "X ⊆ (Z ← Y) ⟷ X ⋅ Y ⊆ Z"
    proof
      assume "X ⊆ Z ← Y"
      hence "X ⋅ Y ⊆ (Z ← Y) ⋅ Y"
        by (metis near_dioid_class.mult_isor)
      also have "… ⊆ ⋃ {X. X ⋅ Y ⊆ Z} ⋅ Y"
        by (simp add: residual_l_set_def)
      also have "… = ⋃ {X ⋅ Y | X. X ⋅ Y ⊆ Z}"
        by (auto simp only: c_prod_def)
      finally show "X ⋅ Y ⊆ Z"
        by auto
    next
      assume "X ⋅ Y ⊆ Z"
      hence "X ⊆ ⋃ {X. X ⋅ Y ⊆ Z}"
        by (metis Sup_upper mem_Collect_eq)
      thus "X ⊆ Z ← Y"
        by (simp add: residual_l_set_def)
    qed
    show "X ⋅ Y ⊆ Z ⟷ Y ⊆ (X → Z)"
    proof
      assume "Y ⊆ X → Z"
      hence "X ⋅ Y ⊆ X ⋅ (X → Z)"
        by (metis pre_dioid_class.mult_isol)
      also have "… ⊆ X ⋅ ⋃ {Y. X ⋅ Y ⊆ Z}"
        by (simp add: residual_r_set_def)
      also have "… = ⋃ {X ⋅ Y | Y. X ⋅ Y ⊆ Z}"
        by (auto simp only: c_prod_def)
      finally show "X ⋅ Y ⊆ Z"
        by auto
    next
      assume "X ⋅ Y ⊆ Z"
      hence "Y ⊆ ⋃ {Y. X ⋅ Y ⊆ Z}"
        by (metis Sup_upper mem_Collect_eq)
      thus "Y ⊆ X → Z"
        by (simp add: residual_r_set_def)
    qed
qed

end (* instantiation *)

instantiation set :: (monoid_mult) action_algebra
begin

  instance
  proof
    fix x y :: "'a set"
    show "1 + x⇧⋆ ⋅ x⇧⋆ + x ⊆ x⇧⋆"
      by simp
    show  "1 + y ⋅ y + x ⊆ y ⟹ x⇧⋆ ⊆ y"
      by (simp add: left_pre_kleene_algebra_class.star_rtc_least)
  qed

end (* instantiation *)


subsection ‹Language Action Algebras›

definition limp_lan :: "'a lan ⇒ 'a lan ⇒ 'a lan" where
  "limp_lan Z Y = {x. ∀y ∈ Y. x @ y ∈ Z}"

definition rimp_lan :: "'a lan ⇒ 'a lan ⇒ 'a lan" where
  "rimp_lan X Z = {y. ∀x ∈ X. x @ y ∈ Z}"

interpretation lan_residuated_join_semilattice: residuated_sup_lgroupoid "(+)" "(⊆)" "(⊂)" "(⋅)" limp_lan rimp_lan
proof
  fix x y z :: "'a lan"
  show "x ⊆ limp_lan z y ⟷ x ⋅ y ⊆ z"
    by (auto simp add: c_prod_def limp_lan_def times_list_def)
  show "x ⋅ y ⊆ z ⟷ y ⊆ rimp_lan x z"
    by (auto simp add: c_prod_def rimp_lan_def times_list_def)
qed

interpretation lan_action_algebra: action_algebra "(+)" "(⋅)" 1 0 "(⊆)" "(⊂)" "(+)" limp_lan rimp_lan star
proof
  fix x y :: "'a lan"
  show "1 + x⇧⋆ ⋅ x⇧⋆ + x ⊆ x⇧⋆"
    by simp
  show "1 + y ⋅ y + x ⊆ y ⟹ x⇧⋆ ⊆ y"
    by (simp add: action_algebra_class.star_rtc_2)
qed


subsection ‹Relation Action Algebras›

definition limp_rel :: "'a rel ⇒ 'a rel ⇒ 'a rel" where
  "limp_rel T S = {(y,x) | y x. ∀z. (x,z) ∈ S ⟶ (y,z) ∈ T}"

definition rimp_rel :: "'a rel ⇒ 'a rel ⇒ 'a rel" where
  "rimp_rel R T = {(y,z) | y z. ∀x. (x,y) ∈ R ⟶ (x,z) ∈ T}"

interpretation rel_residuated_join_semilattice: residuated_sup_lgroupoid "(∪)" "(⊆)" "(⊂)" "(O)" limp_rel rimp_rel
proof
  fix x y z :: "'a rel"
  show "x ⊆ limp_rel z y ⟷ x O y ⊆ z"
    by (auto simp add: limp_rel_def)
  show "x O y ⊆ z ⟷ y ⊆ rimp_rel x z"
    by (auto simp add: rimp_rel_def)
qed

interpretation rel_action_algebra: action_algebra "(∪)" "(O)" Id "{}" "(⊆)" "(⊂)" "(∪)" limp_rel rimp_rel rtrancl
proof
  fix x y :: "'a rel"
  show "Id ∪ x⇧* O x⇧* ∪ x ⊆ x⇧*"
    by auto
  show "Id ∪ y O y ∪ x ⊆ y ⟹ x⇧* ⊆ y"
    by (simp add: rel_kleene_algebra.star_rtc_least)
qed


subsection ‹Trace Action Algebras›

definition limp_trace :: "('p, 'a) trace set ⇒ ('p, 'a) trace set ⇒ ('p, 'a) trace set" where
  "limp_trace Z Y = ⋃ {X. t_prod X Y ⊆ Z}"

definition rimp_trace :: "('p, 'a) trace set ⇒ ('p, 'a) trace set ⇒ ('p, 'a) trace set" where
  "rimp_trace X Z = ⋃ {Y. t_prod X Y ⊆ Z}"

interpretation trace_residuated_join_semilattice: residuated_sup_lgroupoid "(∪)" "(⊆)" "(⊂)" t_prod limp_trace rimp_trace
proof
  fix X Y Z :: "('a,'b) trace set"
  show "X ⊆ limp_trace Z Y ⟷ t_prod X Y ⊆ Z"
    proof
      assume "X ⊆ limp_trace Z Y"
      hence "t_prod X Y ⊆ t_prod (limp_trace Z Y) Y"
        by (metis trace_dioid.mult_isor)
      also have "… ⊆ t_prod (⋃ {X. t_prod X Y ⊆ Z}) Y"
        by (simp add: limp_trace_def)
      also have "… = ⋃ {t_prod X Y | X. t_prod X Y ⊆ Z}"
        by (auto simp only: t_prod_def)
      finally show "t_prod X Y ⊆ Z"
        by auto
    next
      assume "t_prod X Y ⊆ Z"
      hence "X ⊆ ⋃ {X. t_prod X Y ⊆ Z}"
        by (metis Sup_upper mem_Collect_eq)
      thus "X ⊆ limp_trace Z Y"
        by (simp add: limp_trace_def)
    qed
  show "t_prod X Y ⊆ Z ⟷ Y ⊆ rimp_trace X Z"
    proof
      assume "t_prod X Y ⊆ Z"
      hence "Y ⊆ ⋃ {Y. t_prod X Y ⊆ Z}"
        by (metis Sup_upper mem_Collect_eq)
      thus "Y ⊆ rimp_trace X Z"
        by (simp add: rimp_trace_def)
    next
      assume "Y ⊆ rimp_trace X Z"
      hence "t_prod X Y ⊆ t_prod X (rimp_trace X Z)"
        by (metis trace_dioid.mult_isol)
      also have "… ⊆ t_prod X (⋃ {Y. t_prod X Y ⊆ Z})"
        by (simp add: rimp_trace_def)
      also have "… = ⋃ {t_prod X Y | Y. t_prod X Y ⊆ Z}"
        by (auto simp only: t_prod_def)
      finally show "t_prod X Y ⊆ Z"
        by auto
    qed
qed

interpretation trace_action_algebra: action_algebra "(∪)" t_prod t_one t_zero "(⊆)" "(⊂)" "(∪)" limp_trace rimp_trace t_star
proof
  fix X Y :: "('a,'b) trace set"
  show "t_one ∪ t_prod (t_star X) (t_star X) ∪ X ⊆ t_star X"
    by auto
  show "t_one ∪ t_prod Y Y ∪ X ⊆ Y ⟹ t_star X ⊆ Y"
    by (simp add: trace_kleene_algebra.star_rtc_least)
qed


subsection ‹Path Action Algebras›

text ‹We start with paths that include the empty path.›

definition limp_path :: "'a path set ⇒ 'a path set ⇒ 'a path set" where
  "limp_path Z Y = ⋃ {X. p_prod X Y ⊆ Z}"

definition rimp_path :: "'a path set ⇒ 'a path set ⇒ 'a path set" where
  "rimp_path X Z = ⋃ {Y. p_prod X Y ⊆ Z}"

interpretation path_residuated_join_semilattice: residuated_sup_lgroupoid "(∪)" "(⊆)" "(⊂)" p_prod limp_path rimp_path
proof
  fix X Y Z :: "'a path set"
  show "X ⊆ limp_path Z Y ⟷ p_prod X Y ⊆ Z"
    proof
      assume "X ⊆ limp_path Z Y"
      hence "p_prod X Y ⊆ p_prod (limp_path Z Y) Y"
        by (metis path_dioid.mult_isor)
      also have "… ⊆ p_prod (⋃ {X. p_prod X Y ⊆ Z}) Y"
        by (simp add: limp_path_def)
      also have "… = ⋃ {p_prod X Y | X. p_prod X Y ⊆ Z}"
        by (auto simp only: p_prod_def)
      finally show "p_prod X Y ⊆ Z"
        by auto
    next
      assume "p_prod X Y ⊆ Z"
      hence "X ⊆ ⋃ {X. p_prod X Y ⊆ Z}"
        by (metis Sup_upper mem_Collect_eq)
      thus "X ⊆ limp_path Z Y"
        by (simp add: limp_path_def)
    qed
  show "p_prod X Y ⊆ Z ⟷ Y ⊆ rimp_path X Z"
    proof
      assume "p_prod X Y ⊆ Z"
      hence "Y ⊆ ⋃ {Y. p_prod X Y ⊆ Z}"
        by (metis Sup_upper mem_Collect_eq)
      thus "Y ⊆ rimp_path X Z"
        by (simp add: rimp_path_def)
    next
      assume "Y ⊆ rimp_path X Z"
      hence "p_prod X Y ⊆ p_prod X (rimp_path X Z)"
        by (metis path_dioid.mult_isol)
      also have "… ⊆ p_prod X (⋃ {Y. p_prod X Y ⊆ Z})"
        by (simp add: rimp_path_def)
      also have "… = ⋃ {p_prod X Y | Y. p_prod X Y ⊆ Z}"
        by (auto simp only: p_prod_def)
      finally show "p_prod X Y ⊆ Z"
        by auto
    qed
qed

interpretation path_action_algebra: action_algebra "(∪)" p_prod p_one "{}" "(⊆)" "(⊂)" "(∪)" limp_path rimp_path  p_star
proof
  fix X Y :: "'a path set"
  show "p_one ∪ p_prod (p_star X) (p_star X) ∪ X ⊆ p_star X"
    by auto
  show "p_one ∪ p_prod Y Y ∪ X ⊆ Y ⟹ p_star X ⊆ Y"
    by (simp add: path_kleene_algebra.star_rtc_least)    
qed

text ‹We now consider a notion of paths that does not include the
empty path.›

definition limp_ppath :: "'a ppath set ⇒ 'a ppath set ⇒ 'a ppath set" where
  "limp_ppath Z Y = ⋃ {X. pp_prod X Y ⊆ Z}"

definition rimp_ppath :: "'a ppath set ⇒ 'a ppath set ⇒ 'a ppath set" where
  "rimp_ppath X Z = ⋃ {Y. pp_prod X Y ⊆ Z}"

interpretation ppath_residuated_join_semilattice: residuated_sup_lgroupoid "(∪)" "(⊆)" "(⊂)" pp_prod limp_ppath rimp_ppath
proof
  fix X Y Z :: "'a ppath set"
  show "X ⊆ limp_ppath Z Y ⟷ pp_prod X Y ⊆ Z"
    proof
      assume "X ⊆ limp_ppath Z Y"
      hence "pp_prod X Y ⊆ pp_prod (limp_ppath Z Y) Y"
        by (metis ppath_dioid.mult_isor)
      also have "… ⊆ pp_prod (⋃ {X. pp_prod X Y ⊆ Z}) Y"
        by (simp add: limp_ppath_def)
      also have "… = ⋃ {pp_prod X Y | X. pp_prod X Y ⊆ Z}"
        by (auto simp only: pp_prod_def)
      finally show "pp_prod X Y ⊆ Z"
        by auto
    next
      assume "pp_prod X Y ⊆ Z"
      hence "X ⊆ ⋃ {X. pp_prod X Y ⊆ Z}"
        by (metis Sup_upper mem_Collect_eq)
      thus "X ⊆ limp_ppath Z Y"
        by (simp add: limp_ppath_def)
    qed
  show "pp_prod X Y ⊆ Z ⟷ Y ⊆ rimp_ppath X Z"
    proof
      assume "pp_prod X Y ⊆ Z"
      hence "Y ⊆ ⋃ {Y. pp_prod X Y ⊆ Z}"
        by (metis Sup_upper mem_Collect_eq)
      thus "Y ⊆ rimp_ppath X Z"
        by (simp add: rimp_ppath_def)
    next
      assume "Y ⊆ rimp_ppath X Z"
      hence "pp_prod X Y ⊆ pp_prod X (rimp_ppath X Z)"
        by (metis ppath_dioid.mult_isol)
      also have "… ⊆ pp_prod X (⋃ {Y. pp_prod X Y ⊆ Z})"
        by (simp add: rimp_ppath_def)
      also have "… = ⋃ {pp_prod X Y | Y. pp_prod X Y ⊆ Z}"
        by (auto simp only: pp_prod_def)
      finally show "pp_prod X Y ⊆ Z"
        by auto
    qed
qed

interpretation ppath_action_algebra: action_algebra "(∪)" pp_prod pp_one "{}" "(⊆)" "(⊂)" "(∪)" limp_ppath rimp_ppath pp_star
proof
  fix X Y :: "'a ppath set"
  show "pp_one ∪ pp_prod (pp_star X) (pp_star X) ∪ X ⊆ pp_star X"
    by auto
  show "pp_one ∪ pp_prod Y Y ∪ X ⊆ Y ⟹ pp_star X ⊆ Y"
    by (simp add: ppath_kleene_algebra.star_rtc_least)   
qed


subsection ‹The Min-Plus Action Algebra›

instantiation pnat :: minus
begin

  fun minus_pnat where
    "(pnat x) - (pnat y) = pnat (x - y)"
  | "x - PInfty = 1"
  | "PInfty - (pnat x) = 0"

  instance ..

end

instantiation pnat :: semilattice_sup
begin
  definition sup_pnat: "sup_pnat x y ≡ pnat_min x y" 
  instance
  proof
    fix x y z :: pnat
    show "x ≤ x ⊔ y"
      by (metis (no_types) sup_pnat join_semilattice_class.order_prop plus_pnat_def)
    show "y ≤ x ⊔ y"
      by (metis add.left_commute less_eq_pnat_def linear plus_pnat_def sup_pnat)
    show "y ≤ x ⟹ z ≤ x ⟹ y ⊔ z ≤ x"
      by (metis add.commute add.left_commute less_eq_pnat_def plus_pnat_def sup_pnat)  
qed

end


instantiation pnat :: residuated_sup_lgroupoid
begin

  definition residual_r_pnat where
    "(x::pnat) → y ≡ y - x"

  definition residual_l_pnat where
    "(y::pnat) ← x ≡ y - x"

  instance
  proof
    fix x y z :: pnat
    show "x ≤ (z ← y) ⟷ x ⋅ y ≤ z"
      by (cases x, cases y, cases z) (auto simp add: plus_pnat_def times_pnat_def residual_l_pnat_def less_eq_pnat_def zero_pnat_def one_pnat_def)
    show "x ⋅ y ≤ z ⟷ y ≤ (x → z)"
      by (cases y, cases x, cases z) (auto simp add: plus_pnat_def times_pnat_def residual_r_pnat_def less_eq_pnat_def zero_pnat_def one_pnat_def)
  qed

end (* instantiation *)

instantiation pnat :: action_algebra
begin

text ‹The Kleene star for type~@{typ pnat} has already been defined in theory
@{theory Kleene_Algebra.Kleene_Algebra_Models}.›

  instance
  proof
    fix x y :: pnat
    show "1 + x⇧⋆ ⋅ x⇧⋆ + x ≤ x⇧⋆"
      by auto
    show "1 + y ⋅ y + x ≤ y ⟹ x⇧⋆ ≤ y"
      by (simp add: star_pnat_def)
  qed

end (* instantiation *)

end