# 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
```