Theory HS_VC_KA_rel

(*  Title:       Verification components with relational MKA 
    Author:      Jonathan Julián Huerta y Munive, 2020
    Maintainer:  Jonathan Julián Huerta y Munive <jonjulian23@gmail.com>
*)

subsection ‹ Relational model › (* by Victor Gomes, Georg Struth *)

text ‹ In this subsection, we follow Gomes and Struth~\<^cite>‹"afp:vericomp"› and show that relations 
form Kleene algebras.  ›

theory HS_VC_KA_rel
  imports Kleene_Algebra.Kleene_Algebra

begin

context dioid_one_zero
begin

lemma power_inductl: "z + x ⋅ y ≤ y ⟹ (x ^ n) ⋅ z ≤ y"
  by(induct n, auto, metis mult.assoc mult_isol order_trans)

lemma power_inductr: "z + y ⋅ x ≤ y ⟹ z ⋅ (x ^ n) ≤ y"
proof (induct n)
  case 0 show ?case
    using "0.prems" by auto
  case Suc
  {fix n
    assume "z + y ⋅ x ≤ y ⟹ z ⋅ x ^ n ≤ y"
      and "z + y ⋅ x ≤ y"
    hence "z ⋅ x ^ n ≤ y"
      by auto
    also have "z ⋅ x ^ Suc n = z ⋅ x ⋅ x ^ n"
      by (metis mult.assoc power_Suc)
    moreover have "... = (z ⋅ x ^ n) ⋅ x"
      by (metis mult.assoc power_commutes)
    moreover have "... ≤ y ⋅ x"
      by (metis calculation(1) mult_isor)
    moreover have "... ≤ y"
      using ‹z + y ⋅ x ≤ y› by auto
    ultimately have "z ⋅ x ^ Suc n ≤ y" by auto}
  thus ?case
    by (metis Suc)
qed

end

interpretation rel_dioid: dioid_one_zero "(∪)" "(O)" Id "{}" "(⊆)" "(⊂)"
  by (unfold_locales, auto)

lemma power_is_relpow: "rel_dioid.power X n = X ^^ n"
proof (induct n)
  case 0 show ?case
    by (metis rel_dioid.power_0 relpow.simps(1))
  case Suc thus ?case
    by (metis rel_dioid.power_Suc2 relpow.simps(2))
qed

lemma rel_star_def: "X^* = (⋃n. rel_dioid.power X n)"
  by (simp add: power_is_relpow rtrancl_is_UN_relpow)

lemma rel_star_contl: "X O Y^* = (⋃n. X O rel_dioid.power Y n)"
  by (metis rel_star_def relcomp_UNION_distrib)

lemma rel_star_contr: "X^* O Y = (⋃n. (rel_dioid.power X n) O Y)"
  by (metis rel_star_def relcomp_UNION_distrib2)

interpretation rel_ka: kleene_algebra "(∪)" "(O)" Id "{}" "(⊆)" "(⊂)" rtrancl
proof
  fix x y z :: "'a rel"
  show "Id ∪ x O x⇧* ⊆ x⇧*"
    by (metis order_refl r_comp_rtrancl_eq rtrancl_unfold)
next
  fix x y z :: "'a rel"
  assume "z ∪ x O y ⊆ y"
  thus "x⇧* O z ⊆ y"
    by (simp only: rel_star_contr, metis (lifting) SUP_le_iff rel_dioid.power_inductl)
next
  fix x y z :: "'a rel"
  assume "z ∪ y O x ⊆ y"
  thus "z O x⇧* ⊆ y"
    by (simp only: rel_star_contl, metis (lifting) SUP_le_iff rel_dioid.power_inductr)
qed

end