Theory KAT_and_DRA.KAT

(* Title:      Kleene algebra with tests
   Author:     Alasdair Armstrong, Victor B. F. Gomes, Georg Struth
   Maintainer: Georg Struth <g.struth at sheffield.ac.uk>
*)

section ‹Kleene Algebra with Tests›

theory KAT
  imports Kleene_Algebra.Kleene_Algebra Conway_Tests
begin

text ‹
  First, we study left Kleene algebras with tests which also have only a left zero.
  These structures can be expanded to demonic refinement algebras.
›

class left_kat_zerol =  left_kleene_algebra_zerol + test_semiring_zerol
begin

lemma star_n_export1: "(n x ⋅ y)⇧⋆ ⋅ n x ≤ n x ⋅ y⇧⋆"
  by (simp add: local.n_restrictr local.star_sim1)

lemma star_test_export1: "test p ⟹ (p ⋅ x)⇧⋆ ⋅ p ≤ p ⋅ x⇧⋆"
  using star_n_export1 by auto

lemma star_n_export2: "(n x ⋅ y)⇧⋆ ⋅ n x ≤ y⇧⋆ ⋅ n x"
  by (simp add: local.mult_isor local.n_restrictl local.star_iso)

lemma star_test_export2: "test p ⟹ (p ⋅ x)⇧⋆ ⋅ p ≤ x⇧⋆ ⋅ p"
  using star_n_export2 by auto

lemma star_n_export_left: "x ⋅ n y ≤ n y ⋅ x ⟹ x⇧⋆ ⋅ n y = n y ⋅ (x ⋅ n y)⇧⋆"
proof (rule order.antisym)
  assume a1: "x ⋅ n y ≤ n y ⋅ x"
  hence "x ⋅ n y = n y ⋅ x ⋅ n y"
    by (simp add: local.n_kat_2_opp)
  thus "x⇧⋆ ⋅ n y ≤ n y ⋅ (x ⋅ n y)⇧⋆"
    by (simp add: local.star_sim1 mult_assoc)
next
  assume a1: "x ⋅ n y ≤ n y ⋅ x"
  thus "n y ⋅ (x ⋅ n y)⇧⋆ ≤ x⇧⋆ ⋅ n y"
using local.star_slide star_n_export2 by force
qed

lemma star_test_export_left: "test p ⟹ x ⋅ p ≤ p ⋅ x ⟶ x⇧⋆ ⋅ p = p ⋅ (x ⋅ p)⇧⋆"
  using star_n_export_left by auto

lemma star_n_export_right: "x ⋅ n y ≤ n y ⋅ x ⟹ x⇧⋆ ⋅ n y = (n y ⋅ x)⇧⋆ ⋅ n y"
  by (simp add: local.star_slide star_n_export_left)

lemma star_test_export_right: "test p ⟹ x ⋅ p ≤ p ⋅ x ⟶ x⇧⋆ ⋅ p = (p ⋅ x)⇧⋆ ⋅ p"
  using star_n_export_right by auto

lemma star_n_folk: "n z ⋅ x = x ⋅ n z ⟹ n z ⋅ y = y ⋅ n z ⟹ (n z ⋅ x + t z ⋅ y)⇧⋆ ⋅ n z = n z ⋅ (n z ⋅ x)⇧⋆"
proof -
assume a: "n z ⋅ x = x ⋅ n z" and b: "n z ⋅ y = y ⋅ n z"
  hence "n z ⋅ (n z ⋅ x + t z ⋅ y) = (n z ⋅ x + t z ⋅ y) ⋅ n z"
    using local.comm_add_var local.t_n_closed local.test_def by blast
  hence "(n z ⋅ x + t z ⋅ y)⇧⋆ ⋅ n z = n z ⋅ ((n z ⋅ x + t z ⋅ y) ⋅ n z)⇧⋆"
    using local.order_refl star_n_export_left by presburger
  also have "... = n z ⋅ (n z ⋅ x ⋅ n z + t z ⋅ y ⋅ n z)⇧⋆"
    by simp
  also have "... = n z ⋅ (n z ⋅ n z ⋅ x + t z ⋅ n z ⋅ y)⇧⋆"
    by (simp add: a b mult_assoc)
 also have "... = n z ⋅ (n z ⋅ x + 0 ⋅ y)⇧⋆"
  by (simp add: local.n_mult_comm)
  finally show "(n z ⋅ x + t z ⋅ y)⇧⋆ ⋅ n z = n z ⋅ (n z ⋅ x)⇧⋆"
    by simp
qed

lemma star_test_folk: "test p ⟹ p ⋅ x = x ⋅ p ⟶ p ⋅ y = y ⋅ p ⟶ (p ⋅ x + !p ⋅ y)⇧⋆ ⋅ p = p ⋅ (p ⋅ x)⇧⋆"
  using star_n_folk by auto

end

class kat_zerol = kleene_algebra_zerol + test_semiring_zerol
begin

sublocale conway: near_conway_zerol_tests star ..

lemma n_star_sim_right: "n y ⋅ x = x ⋅ n y ⟹ n y ⋅ x⇧⋆ = (n y ⋅ x)⇧⋆ ⋅ n y"
  by (metis local.n_mult_idem local.star_sim3 mult_assoc)

lemma star_sim_right: "test p ⟹ p ⋅ x = x ⋅ p ⟶ p ⋅ x⇧⋆ = (p ⋅ x)⇧⋆ ⋅ p"
  using n_star_sim_right by auto

lemma n_star_sim_left: "n y ⋅ x = x ⋅ n y ⟹ n y ⋅ x⇧⋆ = n y ⋅ (x ⋅ n y)⇧⋆"
  by (metis local.star_slide n_star_sim_right)

lemma star_sim_left: "test p ⟹ p ⋅ x = x ⋅ p ⟶ p ⋅ x⇧⋆ = p ⋅ (x ⋅ p)⇧⋆"
  using n_star_sim_left by auto

lemma n_comm_star: "n z ⋅ x = x ⋅ n z ⟹  n z ⋅ y = y ⋅ n z ⟹ n z ⋅ x ⋅ (n z ⋅ y)⇧⋆ = n z ⋅ x ⋅ y⇧⋆"
  using mult_assoc n_star_sim_left by presburger

lemma comm_star: "test p ⟹ p ⋅ x = x ⋅ p ⟶  p ⋅ y = y ⋅ p ⟶ p ⋅ x ⋅ (p ⋅ y)⇧⋆ = p ⋅ x ⋅ y⇧⋆"
  using n_comm_star by auto

lemma n_star_sim_right_var: "n y ⋅ x = x ⋅ n y ⟹ x⇧⋆ ⋅ n y = n y ⋅ (x ⋅ n y)⇧⋆"
  using local.star_sim3 n_star_sim_left by force

lemma star_sim_right_var: "test p ⟹ p ⋅ x = x ⋅ p ⟶ x⇧⋆ ⋅ p = p ⋅ (x ⋅ p)⇧⋆"
  using n_star_sim_right_var by auto

end

text ‹Finally, we define Kleene algebra with tests.›

class kat = kleene_algebra + test_semiring

begin

sublocale conway: test_pre_conway star ..

end

end