Theory KAT_and_DRA.Conway_Tests

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

section ‹Pre-Conway Algebra with Tests›

theory Conway_Tests
  imports Kleene_Algebra.Conway Test_Dioid

begin

class near_conway_zerol_tests = near_conway_zerol + test_near_semiring_zerol_distrib

begin

lemma n_preserve1_var: "n x  y  n x  y  n x  n x  (n x  y + t x  z)  (n x  y)  n x"
proof -
  assume a: "n x  y  n x  y  n x"
  have "n x  (n x  y + t x  z) = n x  y"
    by (metis (no_types) local.add_zeror local.annil local.n_left_distrib local.n_mult_idem local.test_mult_comp mult_assoc)
  hence "n x  (n x  y + t x  z)  n x  y  n x"
    by (simp add: a)
  thus " n x  (n x  y + t x  z)  (n x  y)  n x"
    by (simp add: local.dagger_simr)
qed

lemma test_preserve1_var: "test p  p  x  p  x  p  p  (p  x + !p  y)  (p  x)  p"
  by (metis local.test_double_comp_var n_preserve1_var)

end

class test_pre_conway = pre_conway + test_pre_dioid_zerol

begin

subclass near_conway_zerol_tests
  by (unfold_locales)

lemma test_preserve: "test p   p  x  p  x  p   p  x = (p  x)  p"
  using local.preservation1_eq local.test_restrictr by auto

lemma test_preserve1: "test p  p  x  p  x  p  p  (p  x + !p  y) = (p  x)  p"
proof (rule order.antisym)
  assume a: "test p" 
  and b: "p  x  p  x  p"
  hence "p  (p  x + !p  y)  (p  x)  p"
    by (metis local.add_0_right local.annil local.n_left_distrib_var local.test_comp_mult2 local.test_mult_idem_var mult_assoc)
  thus "p  (p  x + !p  y)  (p  x)  p"
    using local.dagger_simr by blast
next
  assume a: "test p" 
  and b: "p  x  p  x  p"
  hence "(p  x)  p = p  (p  x  p)"
    by (metis dagger_slide local.test_mult_idem_var mult_assoc)
  also have "... = p  (p  x)"
    by (metis a b local.order.antisym local.test_restrictr)
  finally show "(p  x)  p  p  (p  x + !p  y)"
    by (simp add: a local.dagger_iso local.test_mult_isol)
qed

lemma test_preserve2: "test p  p  x  p = p  x  p  (p  x + !p  y)  x"
  by (metis (no_types) local.eq_refl local.test_restrictl test_preserve test_preserve1)

end

end