(* 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