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