Theory KAT_and_DRA.Test_Dioid

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

section ‹Test Dioids›

theory Test_Dioid
  imports Kleene_Algebra.Dioid
begin

text ‹
  Tests are embedded in a weak dioid, a dioid without the right annihilation and left distributivity axioms, using an 
  operator $t$ defined by a complementation operator. This allows us to use tests in weak settings, such as Probabilistic Kleene Algebra and Demonic Refinement Algebra.
›

subsection ‹Test Monoids›

class n_op =
  fixes n_op :: "'a  'a" ("n _" [90] 91)

class test_monoid = monoid_mult + n_op +
  assumes tm1 [simp]: "n n 1 = 1" 
  and tm2 [simp]: "n x  n n x = n 1" 
  and tm3: "n x  n (n n z  n n y) = n (n (n x  n y)  n (n x  n z))"

begin 

(*no_notation zero_class.zero ("0")*)

definition a_zero :: "'a" ("o") where 
  "o  n 1"

abbreviation "t x  n n x"

definition n_add_op :: "'a  'a  'a" (infixl "" 65) where 
  "x  y  n (n x  n y)"

lemma "n 1  x = n 1"
(*nitpick*) oops

lemma "x  n 1 = n 1"
(*nitpick*) oops

lemma "n 1  x = n 1  n x  y  t z = n 1  n x  y = n x  y  n z  "
(*nitpick*) oops

lemma n_t_closed [simp]: "t (n x) = n x"
proof -
  have "x y. n x  n (t (n x)  t y) = t (n x  n y)"
    by (simp add: local.tm3)
  thus ?thesis
   by (metis (no_types) local.mult_1_right local.tm1 local.tm2 local.tm3 mult_assoc)
qed

lemma mult_t_closed [simp]: "t (n x  n y) = n x  n y"
  by (metis local.mult_1_right local.tm1 local.tm2 local.tm3 n_t_closed)

lemma n_comm_var: "n (n x  n y) = n (n y  n x)"
  by (metis local.mult_1_left local.tm1 local.tm3 n_t_closed)

lemma n_comm: "n x  n y = n y  n x"
  using mult_t_closed n_comm_var by fastforce

lemma huntington1 [simp]: "n (n (n n x  n y)  n (n n x  n n y)) = n n x"
  by (metis local.mult_1_right local.tm1 local.tm2 local.tm3)

lemma huntington2 [simp]: "n (n x  n n y)  n (n x  n y) = n n x"
  by (simp add: n_add_op_def)

lemma add_assoc: "n x  (n y  n z) = (n x  n y)  n z"
  by (simp add: mult_assoc n_add_op_def)

lemma t_mult_closure: "t x = x  t y = y  t (x  y) = x  y"
  by (metis mult_t_closed)

lemma n_t_compl [simp]: "n x  t x = 1"
  using n_add_op_def local.tm1 local.tm2 by presburger

lemma zero_least1 [simp]: "o  n x = n x"
  by (simp add: a_zero_def n_add_op_def)

lemma zero_least2 [simp]: "o  n x = o"
  by (metis a_zero_def local.tm2 local.tm3 mult_assoc mult_t_closed zero_least1)

lemma zero_least3 [simp]: "n x  o  = o"
  using a_zero_def n_comm zero_least2 by fastforce

lemma one_greatest1 [simp]: "1  n x = 1"
  by (metis (no_types) a_zero_def local.tm1 n_add_op_def n_comm_var zero_least3)

lemma one_greatest2 [simp]: "n x  1 = 1"
  by (metis n_add_op_def n_comm_var one_greatest1)

lemma n_add_idem [simp]: "n x  n x = n x"
  by (metis huntington1 local.mult_1_right n_t_closed n_t_compl n_add_op_def)

lemma n_mult_idem [simp]: "n x  n x = n x"
  by (metis mult_t_closed n_add_idem n_add_op_def)

lemma n_preserve [simp]: "n x  n y  n x = n y  n x"
  by (metis mult_assoc n_comm n_mult_idem)

lemma n_preserve2 [simp]: "n x  n y  t x = o"
  by (metis a_zero_def local.tm2 mult_assoc n_comm zero_least3)

lemma de_morgan1 [simp]: "n (n x  n y) = t x  t y"
  by (simp add: n_add_op_def)

lemma de_morgan4 [simp]: "n (t x  t y) = n x  n y"
  using n_add_op_def mult_t_closed n_t_closed by presburger

lemma n_absorb1 [simp]: "n x  n x  n y = n x"
  by (metis local.mult_1_right local.tm1 local.tm3 one_greatest2 n_add_op_def)

lemma n_absorb2 [simp]: "n x  (n x  n y) = n x"
  by (metis mult_t_closed n_absorb1 n_add_op_def)

lemma n_distrib1: "n x  (n y  n z) = (n x  n y)  (n x  n z)"
  using local.tm3 n_comm_var  n_add_op_def by presburger

lemma n_distrib1_opp: "(n x  n y)  n z  = (n x  n z)  (n y  n z)"
  using n_add_op_def n_comm n_distrib1 by presburger

lemma n_distrib2: "n x  n y  n z = (n x  n y)  (n x  n z)"
  by (metis mult_t_closed n_distrib1 n_mult_idem  n_add_op_def)

lemma n_distrib2_opp: "n x  n y  n z = (n x  n z)  (n y  n z)"
  by (metis de_morgan1 mult_t_closed n_distrib1_opp n_add_op_def)

definition ts_ord :: "'a  'a  bool" (infix "" 50) where
  "x  y = (n x  n y = n y)"

lemma ts_ord_alt: "n x  n y  n x  n y = n y"
  by (metis mult_t_closed n_t_closed ts_ord_def n_add_op_def)

lemma ts_ord_refl: "n x  n x"
  by (simp add: ts_ord_def)

lemma ts_ord_trans: "n x  n y  n y  n z  n x  n z"
  by (metis mult_assoc ts_ord_def)

lemma ts_ord_antisym: "n x  n y  n y  n x  n x = n y"
  by (metis n_add_idem n_comm ts_ord_def n_add_op_def)

lemma ts_ord_mult_isol: "n x  n y  n z  n x  n z  n y"
proof -
  assume "n x  n y"
  hence "n (n (n z  n x)  n (n z  n y)) = n z  n y"
    by (metis mult_t_closed n_add_idem n_distrib1 ts_ord_def n_add_op_def)
  thus ?thesis
    by (metis mult_t_closed ts_ord_def)
qed

lemma ts_ord_mult_isor: "n x  n y  n x  n z  n y  n z"
  using n_comm ts_ord_mult_isol by auto

lemma ts_ord_add_isol: "n x  n y  n z  n x  n z  n y"
  by (metis mult_assoc mult_t_closed n_mult_idem ts_ord_def n_add_op_def)

lemma ts_ord_add_isor: "n x  n y  n x  n z  n y  n z"
  using n_add_op_def n_comm ts_ord_add_isol by presburger

lemma ts_ord_anti: "n x  n y  t y  t x"
  by (metis n_absorb2 n_add_idem n_comm ts_ord_def n_add_op_def)

lemma ts_ord_anti_iff: "n x  n y  t y  t x"
  using ts_ord_anti by force

lemma zero_ts_ord: "o  n x"
  by (simp add: a_zero_def ts_ord_def)

lemma n_subid: "n x  1"
  by (simp add: a_zero_def[symmetric] ts_ord_def)

lemma n_mult_lb1: "n x  n y  n x"
  by (metis (no_types) local.mult_1_right local.tm1 n_comm n_subid ts_ord_mult_isor)

lemma n_mult_lb2: "n x  n y  n y"
  by (metis n_comm n_mult_lb1)

lemma n_mult_glbI: "n z  n x   n z  n y  n z  n x  n y"
  by (metis n_t_closed ts_ord_anti_iff ts_ord_def ts_ord_mult_isol)

lemma n_mult_glb: "n z  n x  n z  n y  n z  n x  n y"
  by (metis mult_t_closed n_mult_glbI n_mult_lb1 n_mult_lb2 ts_ord_trans)

lemma n_add_ub1: "n x  n x  n y"
  by (metis (no_types) n_absorb2 n_mult_lb2 n_add_op_def)

lemma n_add_ub2: "n y  n x  n y"
  by (metis n_add_ub1 n_comm_var n_add_op_def)

lemma n_add_lubI: "n x  n z  n y  n z  n x  n y  n z"
  by (metis ts_ord_add_isol ts_ord_alt) 

lemma n_add_lub: "n x  n z  n y  n z  n x  n y  n z"
  by (metis n_add_lubI n_add_op_def n_add_ub1 n_add_ub2 ts_ord_trans)

lemma n_galois1: "n x  n y  n z  n x  t y  n z"
proof 
  assume "n x  n y  n z"
  hence "n x  t y  (n y  n z )  t y"
    by (metis n_add_op_def ts_ord_mult_isor)
  also have "... = n y  t y  n z  t y"
    using n_add_op_def local.tm3 n_comm by presburger    
  also have "... = n z  t y"
    using a_zero_def local.tm2 n_distrib2 zero_least1 by presburger
  finally show "n x  t y  n z"
    by (metis mult_t_closed n_mult_glb)
next
  assume a: "n x  t y  n z" 
  have "n x = t (n x  (n y  t y))"
    using local.mult_1_right n_t_closed n_t_compl by presburger
  also have "... = t (n x  n y  n x  t y)"
    using n_distrib1 by presburger
  also have "...   t (n y  n x  t y)"
    by (metis calculation local.mult_1_right mult_t_closed n_add_op_def n_add_ub2 n_distrib2 n_t_compl)
  finally show "n x  n y  n z"
    by (metis (no_types, opaque_lifting) a mult_t_closed ts_ord_add_isol ts_ord_trans n_add_op_def)
qed

lemma n_galois2: "n x  t y  n z  n x  n y  n z"
  by (metis n_galois1 n_t_closed)

lemma n_distrib_alt: "n x  n z = n y  n z  n x  n z = n y  n z  n x = n y"
proof -
  assume a: "n x  n z = n y  n z" and b: "n x  n z = n y  n z"
  have "n x = n x  n x  n z"
    using n_absorb1 by presburger
  also have "... = n x  n y  n z"
    using a by presburger
  also have "... = (n x  n y)  (n x  n z)"
    using n_distrib2 by blast
  also have "... = (n y  n x)  (n y  n z)"
    using n_add_op_def b n_comm by presburger 
  also have "... = n y  (n x  n z)"
    by (metis a b n_distrib1 n_distrib2 n_mult_idem)
  also have "... = n y  (n y  n z)"
    using b by presburger 
  finally show "n x = n y"
    using n_absorb2 by presburger
qed

lemma n_dist_var1: "(n x  n y)  (t x  n z) = t x  n y  n x  n z"
proof - 
  have "(n x  n y)  (t x  n z) = n x  t x  n y  t x  (n x  n z  n y  n z)" 
    using n_add_op_def n_distrib1 n_distrib1_opp by presburger
  also have "... = t x  n y  (n x  n z  (n x  t x)  t (n y  n z))"
    using n_add_op_def local.mult_1_left local.tm1 local.tm2 n_comm n_t_closed by presburger
  also have "... = t x  n y  (n x  n z  (n x  n y  n z  t x  n y  n z))"
    by (metis mult_assoc mult_t_closed n_distrib1_opp)
  also have "... = (t x  n y  t x  n y  n z)  (n x  n z  n x  n y  n z)"
proof -
  have f1: "a aa ab. n n (n (a::'a)  (n aa  n ab)) = n a  (n aa  n ab)"
    by (metis (full_types) mult_t_closed)
  have "a aa ab. n (a::'a)  (n aa  n ab) = n aa  (n ab  n a)"
    by (metis mult_assoc n_comm)
  hence "n (n (n y  n n x)  n n (n (n x  n z)  (n (n x  n y  n z)  n (n y  n n x  n z)))) = n (n (n y  n n x)  n (n y  n n x  n z)  (n (n x  n z)  n (n x  n y  n z)))"
    using f1 mult_assoc by presburger
  thus ?thesis
    using mult_t_closed n_add_op_def n_comm by presburger
qed
     also have "... = (t x  n y  t (t x  n y)  n z)  (n x  n z  t (n x  n z)  n y)"
    using mult_assoc mult_t_closed n_comm by presburger
  also have "... = (t x  n y  (1  n z))  (n x  n z  (1  n y))"
    by (metis a_zero_def n_add_op_def local.mult_1_right local.tm1 mult_t_closed n_absorb1 zero_least2)
  finally show ?thesis
    by simp
qed

lemma n_dist_var2: "n (n x  n y  t x  n z) = n x  t y  t x  t z"
  by (metis (no_types) n_add_op_def n_dist_var1 n_t_closed)

end

subsection ‹Test Near-Semirings›
 
class test_near_semiring_zerol = ab_near_semiring_one_zerol + n_op + plus_ord + 
  assumes test_one [simp]: "n n 1 = 1" 
  and test_mult [simp]: "n n (n x  n y) = n x  n y" 
  and test_mult_comp [simp]: "n x  n n x = 0"
  and test_de_morgan [simp]: "n (n n x  n n y) = n x + n y"  

begin

lemma n_zero [simp]: "n 0 = 1"
proof -
  have "n 0 = n (n 1  n n 1)"
    using local.test_mult_comp by presburger
  also have "... = n (n 1  1)"
    by simp
  finally show ?thesis
    by simp
qed

lemma n_one [simp]: "n 1 = 0"
proof -
  have "n 1 = n 1  1"
    by simp
  also have "... = n 1  n n 1"
    by simp
  finally show ?thesis
    using test_mult_comp by metis
qed

lemma one_idem [simp]: "1 + 1 = 1"
proof -
  have "1 + 1 = n n 1 + n n 1"
    by simp
  also have "... = n (n n n 1  n n n 1)"
    using local.test_de_morgan by presburger
  also have "... = n (0  n n n 1)"
    by simp
  also have "... = n 0"
    by simp
  finally show ?thesis
    by simp
qed

subclass near_dioid_one_zerol
proof 
  fix x
  have "x + x = (1 + 1)  x"
    using local.distrib_right' local.mult_onel by presburger
  also have "... = 1  x"
    by simp
  finally show "x + x = x"
    by simp
qed

lemma t_n_closed [simp]: "n n (n x) = n x"
proof -
  have "n n (n x) = n (n n x  1)"
    by simp
  also have "... = n (n n x  n n 1)"
    by simp
  also have "... = n x + n 1"
    using local.test_de_morgan by presburger
  also have "... = n x + 0"
    by simp
  finally show ?thesis 
    by simp
qed

lemma t_de_morgan_var1 [simp]: "n (n x  n y) = n n x + n n y"
  by (metis local.test_de_morgan t_n_closed)

lemma n_mult_comm: "n x  n y = n y  n x"
proof -
  have "n x  n y = n n (n x  n y)"
    by (metis local.test_mult)
  also have "... = n (n n x + n n y)"
    by simp
  also have "... = n (n n y + n n x)"
    by (metis add_commute)
  also have "... = n n (n y  n x)"
    by simp
  finally show ?thesis
    by (metis local.test_mult)
qed
  
lemma tm3': "n x  n (n n z  n n y) = n (n (n x  n y)  n (n x  n z))"
proof -
  have "n x  n (n n z  n n y) = n (n n y  n n z)  n x"
    using n_mult_comm by presburger
  also have "... = (n y + n z)  n x"
    by simp
  also have "... = n y  n x + n z  n x"
    by simp
  also have "... = n n (n x  n y) + n n (n x  n z)" 
    by (metis local.test_mult n_mult_comm)
  finally show ?thesis
    by (metis t_de_morgan_var1)
qed

subclass test_monoid
proof
  show "n n 1 = 1"
    by simp
  show "x. n x  n n x = n 1"
    by simp
  show " x z y. n x  n (n n z  n n y) = n (n (n x  n y)  n (n x  n z))"
    using tm3' by blast
qed

lemma ord_transl [simp]: "n x  n y  n x  n y"
  by (simp add: local.join.sup.absorb_iff2 local.n_add_op_def local.ts_ord_alt)

lemma add_transl [simp]: "n x + n y = n x  n y"
  by (simp add: local.n_add_op_def)

lemma zero_trans: "0 = o"
  by (metis local.a_zero_def n_one)

definition test :: "'a  bool" where
  "test p  t p = p"

notation n_op ("!_" [101] 100)

lemma test_prop: "(x. test x  P x)  (x. P (t x))"
  by (metis test_def t_n_closed)

lemma test_propI: "test x  P x  P (t x)"
  by (simp add: test_def)

lemma test_propE [elim!]: "test x  P (t x)  P x"
  by (simp add: test_def)

lemma test_comp_closed [simp]: "test p  test (!p)"
  by (simp add: test_def)

lemma test_double_comp_var: "test p  p = !(!p)"
  by auto

lemma test_mult_closed: "test p  test q  test (p  q)"
  by (metis local.test_mult test_def)

lemma t_add_closed [simp]: "t (n x + n y) = n x + n y"
  by (metis local.test_de_morgan t_n_closed)

lemma test_add_closed: "test p  test q  test (p + q)"
  by (metis t_add_closed test_def)

lemma test_mult_comm_var: "test p  test q  p  q = q  p"
  using n_mult_comm by auto

lemma t_zero [simp]: "t 0 = 0"
  by simp

lemma test_zero_var: "test 0"
  by (simp add: test_def)

lemma test_one_var: "test 1"
  by (simp add: test_def)

lemma test_preserve: "test p  test q  p  q  p = q  p"
  by auto

lemma test_preserve2: "test p  test q  p  q  !p = 0"
  by (metis local.a_zero_def local.n_preserve2 n_one test_double_comp_var)

 
lemma n_subid': "n x  1"
  using local.n_subid n_zero ord_transl by blast

lemma test_subid: "test p  p  1"
  using n_subid' by auto

lemma test_mult_idem_var [simp]: "test p  p  p = p"
  by auto

lemma n_add_comp [simp]: "n x + t x = 1"
  by simp

lemma n_add_comp_var [simp]: "t x + n x = 1"
  by (simp add: add_commute)

lemma test_add_comp [simp]: "test p  p + !p = 1"
  using n_add_comp by fastforce
 
lemma test_comp_mult1 [simp]: "test p  !p  p = 0"
  by auto

lemma test_comp_mult2 [simp]: "test p  p  !p = 0"
  using local.test_mult_comp by fastforce

lemma test_comp: "test p  q. test q  p + q = 1  p  q = 0"
  using test_add_comp test_comp_closed test_comp_mult2 by blast

lemma n_absorb1' [simp]: "n x + n x  n y = n x"
  by (metis add_transl local.de_morgan4 local.n_absorb1)

lemma test_absorb1 [simp]: "test p  test q  p + p  q = p"
  by auto

lemma n_absorb2' [simp]: "n x  (n x + n y) = n x"
  by simp

lemma test_absorb2: "test p  test q  p  (p + q) = p"
  by auto

lemma n_distrib_left: "n x  (n y + n z) = (n x  n y) + (n x  n z)"
  by (metis (no_types) add_transl local.de_morgan4 local.n_distrib1)

lemma test_distrib_left: "test p   test q  test r  p  (q + r) = p  q + p  r"
  using n_distrib_left by auto

lemma de_morgan1': "test p  test q  !p + !q = !(p  q)"
  by auto

lemma n_de_morgan_var2 [simp]: "n (n x + n y) = t x  t y"
  by (metis local.test_de_morgan local.test_mult)

lemma n_de_morgan_var3 [simp]: "n (t x + t y) = n x  n y"
  by simp

lemma de_morgan2: "test p  test q  !p  !q = !(p + q)"
  by auto

lemma de_morgan3: "test p  test q  !(!p + !q) = p  q"
  using local.de_morgan1' local.t_mult_closure test_def by auto  

lemma de_morgan4': "test p  test q  !(!p  !q) = p + q"
  by auto

lemma n_add_distr: "n x + (n y  n z) = (n x + n y)  (n x + n z)"
  by (metis add_transl local.n_distrib2 n_de_morgan_var3)

lemma test_add_distr: "test p  test q  test r  p + q  r = (p + q)  (p + r)"
  using n_add_distr by fastforce

lemma n_add_distl: "(n x  n y) + n z = (n x + n z)  (n y + n z)"
  by (simp add: add_commute n_add_distr)

lemma test_add_distl_var: "test p  test q  test r  p  q + r = (p + r)  (q + r)"
  by (simp add: add_commute test_add_distr)

lemma n_ord_def_alt: "n x  n y  n x  n y = n x"
  by (metis (no_types) local.join.sup.absorb_iff2 local.n_absorb2' local.n_mult_lb2 ord_transl)

lemma test_leq_mult_def_var: "test p  test q  p  q  p  q = p"
  using n_ord_def_alt by auto

lemma n_anti: "n x  n y  t y  t x"
  using local.ts_ord_anti ord_transl by blast

lemma n_anti_iff: "n x  n y  t y  t x"
  using n_anti by fastforce

lemma test_comp_anti_iff: "test p  test q  p  q  !q  !p"
  using n_anti_iff by auto

lemma n_restrictl: "n x  y  y"
  using local.mult_isor n_subid' by fastforce

lemma test_restrictl: "test p  p  x  x"
  by (auto simp: n_restrictl)

lemma n_mult_lb1': "n x  n y  n x"
  by (simp add: local.join.sup.orderI)

lemma test_mult_lb1: "test p  test q  p  q  p"
  by (auto simp: n_mult_lb1')

lemma n_mult_lb2': "n x  n y  n y"
  by (fact local.n_restrictl)

lemma test_mult_lb2: "test p  test q  p  q  q"
  by (rule test_restrictl)

lemma n_mult_glbI': "n z  n x   n z  n y  n z  n x  n y"
  by (metis mult_isor n_ord_def_alt)

lemma test_mult_glbI:  "test p  test q  test r  p  q  p  r  p  q  r"
  by (metis (no_types) local.mult_isor test_leq_mult_def_var)

lemma n_mult_glb': "n z  n x  n z  n y  n z  n x  n y"
  using local.order_trans n_mult_glbI' n_mult_lb1' n_mult_lb2' by blast

lemma test_mult_glb: "test p  test q  test r  p  q  p  r  p  q  r"
  using local.n_mult_glb' by force

lemma n_galois1': "n x  n y + n z  n x  t y  n z"
proof -
  have "n x  n y + n z  n x  n y  n z"
    by (metis local.test_de_morgan ord_transl n_add_op_def)
  also have "...  n x  t y  n z"
    using local.n_galois1 by auto
  also have "...  n x  t y  n z"
    by (metis local.test_mult ord_transl)
  finally show ?thesis
    by simp
qed

lemma test_galois1: "test p  test q  test r  p  q + r  p  !q  r"
  using n_galois1' by auto

lemma n_galois2': "n x  t y + n z  n x  n y  n z"
  using local.n_galois1' by auto

lemma test_galois2: "test p  test q  test r  p  !q + r  p  q  r"
  using test_galois1 by auto

lemma n_huntington2: "n (n x + t y) + n (n x + n y) = n n x"
  by simp

lemma test_huntington2: "test p  test q  !(p + q) + !(p + !q) = !p"
proof -
  assume a1: "test p"
  assume a2: "test q"
  have "p = !(!p)"
    using a1 test_double_comp_var by blast
  thus ?thesis
    using a2 by (metis (full_types) n_huntington2 test_double_comp_var)
qed

lemma n_kat_1_opp: "n x  y  n z = y  n z  t x  y  n z = 0"
proof
  assume "n x  y  n z = y  n z"
  hence "t x  y  n z = t x  n x  y  n z"
    by (simp add: mult_assoc)
  thus " t x  y  n z = 0"
    by (simp add: n_mult_comm)
next
  assume "n n x  y  n z = 0"
  hence "n x  y  n z = 1  y  n z"
    by (metis local.add_zerol local.distrib_right' n_add_comp t_n_closed)
  thus "n x  y  n z = y  n z"
    by auto
qed

lemma test_eq4: "test p  test q  !p  x  !q = x  !q  p  x  !q = 0"
  using n_kat_1_opp by auto

lemma n_kat_1_var: "t x  y  t z = y  t z  n x  y  t z = 0"
  by (simp add: n_kat_1_opp)

lemma test_kat_1: "test p  test q  p  x  q = x  q  !p  x  q = 0"
  using n_kat_1_var by auto

lemma n_kat_21_opp:  "y  n z  n x  y  n x  y  n z = y  n z"
proof -
  assume "y  n z  n x  y"
  hence "y  n z + n x  y = n x  y"
    by (meson local.join.sup_absorb2)
  hence "n x  y  n z = y  n z + (n x  (y  n z) + 0)"
    by (metis local.add_zeror local.distrib_right' local.n_mult_idem mult_assoc)
  thus ?thesis
    by (metis local.add_zeror local.distrib_right' local.join.sup_absorb2 local.join.sup_left_commute local.mult_onel local.n_subid')
qed

lemma test_kat_21_opp: "test p  test q  x  q  p  x  p  x  q = x  q"
  using n_kat_21_opp by auto

lemma  " n x  y  n z = y  n z  y  n z  n x  y"
  (*nitpick*) oops

lemma n_distrib_alt': "n x  n z = n y  n z  n x + n z = n y + n z  n x = n y"
  using local.n_distrib_alt by auto

lemma test_distrib_alt: "test p  test q  test r  p  r = q  r  p + r = q + r  p = q"
  using n_distrib_alt by auto

lemma n_eq1: "n x  y  z  t x  y  z  y  z"
proof -
  have  "n x  y  z  t x  y  z  n x  y + t x  y  z"
    by simp
  also have "...  (n x + t x)  y  z"
    using local.distrib_right' by presburger
  finally show ?thesis
    by auto
qed

lemma test_eq1: "test p  y  x  p  y  x  !p  y  x"
  using n_eq1 by auto

lemma n_dist_var1': "(n x + n y)  (t x + n z) = t x  n y + n x  n z"
  by (metis add_transl local.n_dist_var1 local.test_mult)

lemma test_dist_var1: "test p  test q  test r  (p + q)  (!p + r) = !p  q + p  r"
  using n_dist_var1' by fastforce

lemma n_dist_var2': "n (n x  n y + t x  n z) = n x  t y + t x  t z"
proof -
  have f1: "!x  !y = !(!(!x  !y))"
    using n_de_morgan_var3 t_de_morgan_var1 by presburger
  have "!(!(!x)) = !x"
    by simp
  thus ?thesis
    using f1 by (metis (no_types) n_de_morgan_var3 n_dist_var1' t_de_morgan_var1)
qed

lemma test_dist_var2: "test p  test q  test r  !(p  q + !p  r) = (p  !q + !p  !r)"
  using n_dist_var2' by auto

lemma test_restrictr: "test p  x  p  x"
  (* nitpick *) oops

lemma test_eq2: "test p  z  p  x + !p  y  p  z  p  x  !p  z  !p  y"
  (* nitpick *) oops

lemma test_eq3: "test p; test q  p  x = p  x  q  p  x  x  q"
  (* nitpick *) oops

lemma test1: "test p; test q; p  x  !q = 0  p  x = p  x  q"
  (* nitpick *) oops

lemma "test p; test q; x  !q = !p  x  !q  p  x = p  x  q"
  (* nitpick *) oops

lemma comm_add: "test p; px = xp; py = yp  p(x + y) = (x + y)p"
  (* nitpick *) oops

lemma comm_add_var: "test p; test q; test r; px = xp; py = yp  p(qx + ry) = (qx + ry)p"
  (* nitpick *) oops

lemma "test p  p  x = x  p  p  x = p  x  p  !p  x = !p  x  !p "
  (* nitpick *) oops

lemma test_distrib: "test p; test q  (p + q)(qy + !qx) = qy + !qpx"
  (* nitpick *) oops

end

subsection ‹Test Near Semirings with Distributive Tests›

text ‹
  We now make the assumption that tests distribute over finite sums of arbitrary elements from the left.
  This can be justified in models such as multirelations and probabilistic predicate transformers.
›

class test_near_semiring_zerol_distrib = test_near_semiring_zerol  +
  assumes n_left_distrib: "n x  (y + z) = n x  y + n x  z"

begin

lemma n_left_distrib_var: "test p  p  (x + y) = p  x + p  y"
  using n_left_distrib by auto

lemma n_mult_left_iso: "x  y  n z  x  n z  y"
  by (metis local.join.sup.absorb_iff1 local.n_left_distrib)

lemma test_mult_isol: "test p  x  y  p  x  p  y"
  using n_mult_left_iso by auto

lemma "test p  x  p  x"
  (* nitpick *) oops

lemma "test p; test q  p  x = p  x  q  p  x  x  q"
  (* nitpick *) oops

lemma "test p; test q; p  x  !q = 0  p  x = p  x  q"
  (* nitpick *) oops

lemma "test p; test q; x  !q = !p  x  !q  p  x = p  x  q"
  (* nitpick *) oops

text ‹Next, we study tests with commutativity conditions.›

lemma comm_add: "test p   p  x = x  p   p  y = y  p  p  (x + y) = (x + y)  p"
  by (simp add: n_left_distrib_var)

lemma comm_add_var: "test p  test q  test r  p  x = x  p  p  y = y  p  p  (q  x + r  y) = (q  x + r  y)  p"
proof -
  assume a1: "test p"
  assume a2: "test q"
  assume a3: "p  x = x  p"
  assume a4: "test r"
  assume a5: "p  y = y  p"
  have f6: "p  (q  x) = q  p  x"
    using a2 a1 local.test_mult_comm_var mult_assoc by presburger
  have "p  (r  y) = r  p  y"
    using a4 a1 by (simp add: local.test_mult_comm_var mult_assoc)
  thus ?thesis
    using f6 a5 a3 a1 by (simp add: mult_assoc n_left_distrib_var)
qed

lemma test_distrib: "test p  test q  (p + q)  (q  y + !q  x) = q  y + !q  p  x"
proof -
  assume a: "test p" and b: "test q"
  hence "(p + q)  (q  y + !q  x) = p  q  y + p  !q  x + q  q  y + q  !q  x"
    using local.add.assoc local.distrib_right' mult_assoc n_left_distrib_var by presburger
  also have "... = p  q  y + !q  p  x + q  y"
   by (simp add: a b local.test_mult_comm_var) 
  also have "... = (p + 1)  q  y + !q  p  x"
    using add_commute local.add.assoc by force
  also have "... = q  y + !q  p  x"
    by (simp add: a local.join.sup.absorb2 local.test_subid)
  finally show ?thesis
    by simp
qed

end

subsection ‹Test Predioids›

text ‹
  The following class is relevant for probabilistic Kleene algebras.
›

class test_pre_dioid_zerol = test_near_semiring_zerol_distrib + pre_dioid

begin

lemma n_restrictr: "x  n y  x"
  using local.mult_isol local.n_subid' by fastforce

lemma test_restrictr: "test p  x  p  x"
  using n_restrictr by fastforce

lemma n_kat_2: "n x  y = n x  y  n z  n x  y  y  n z"
proof
  assume "n x  y = n x  y  n z"
  thus "n x  y  y  n z"
    by (metis mult.assoc n_restrictl)
next 
  assume "n x  y  y  n z"
  hence "n x  y   n x  y  n z"
    by (metis local.mult_isol local.n_mult_idem mult_assoc)
  thus "n x  y  = n x  y  n z"
    by (simp add: local.order.antisym n_restrictr)
qed

lemma test_kat_2: "test p  test q  p  x = p  x  q  p  x  x  q"
  using n_kat_2 by auto

lemma n_kat_2_opp: "y  n z = n x  y  n z  y  n z  n x  y"
  by (metis local.n_kat_21_opp n_restrictr)

lemma test_kat_2_opp: "test p  test q  x  q  = p  x  q  x  q  p  x"
  by (metis local.test_kat_21_opp test_restrictr)

lemma "test p; test q; px!q = 0  px = pxq"
  (* nitpick *) oops

lemma "test p; test q; x!q = !px!q  px = pxq"
  (* nitpick *) oops

lemma "test p; test q  x  (p + q)  x  p + x  q"
  (* nitpick *) oops

end

text ‹
  The following class is relevant for Demonic Refinement Algebras.
›

class test_semiring_zerol = test_near_semiring_zerol + semiring_one_zerol

begin

subclass dioid_one_zerol ..

subclass test_pre_dioid_zerol
proof
show "x y z. !x  (y + z) = !x  y + !x  z"
  by (simp add: local.distrib_left)
qed

lemma n_kat_31: "n x  y  t z = 0  n x  y  n z = n x  y"
proof -
  assume a: "n x  y  t z = 0"
  have "n x  y = n x  y  (n z + t z)"
    by simp
  also have "... = n x  y  n z + n x  y  t z"
    using local.distrib_left by blast
  finally show "n x  y  n z = n x  y"
    using a  by auto
qed

lemma test_kat_31: "test p  test q  p  x  !q = 0  p  x = p  x  q"
  by (metis local.test_double_comp_var n_kat_31)

lemma n_kat_var: "t x  y  t z = y  t z  n x  y  n z = n x  y"
  using local.n_kat_1_var n_kat_31 by blast

lemma test1_var: "test p  test q  x  !q = !p  x  !q  p  x = p  x  q"
  by (metis local.test_eq4 test_kat_31)

lemma "test p; test q; px!q = 0  !pxq = 0"
  (* nitpick *) oops

lemma "test p; test q; px = pxq  x!q = !px!q"
  (* nitpick *) oops

lemma "test p; test q; px = pxq  px!q = 0"
  (* nitpick *) oops

lemma "test p; test q; px = pxq  !pxq = 0"
  (* nitpick *) oops

lemma "test p; test q; x!q = !px!q  !pxq = 0"
  (* nitpick *) oops

lemma "test p; test q; !pxq = 0  px = pxq"
  (* nitpick *) oops

lemma "test p; test q; !pxq = 0  x!q = !px!q"
  (* nitpick *) oops

lemma "test p; test q; !pxq = 0  px!q = 0"
  (* nitpick *) oops

lemma "test p  p  x = p  x  p  !p  x = !p  x  !p  p  x = x  p"
  (* nitpick *) oops

end

subsection ‹Test Semirings›

text ‹
  The following class is relevant for Kleene Algebra with Tests.
›

class test_semiring = test_semiring_zerol + semiring_one_zero

begin

lemma n_kat_1: "n x  y  t z = 0  n x  y  n z = n x  y"
  by (metis local.annir local.n_kat_31 local.test_mult_comp mult_assoc)

lemma test_kat_1': "test p  test q  p  x  !q = 0  p  x =  p  x  q"
  by (metis local.test_double_comp_var n_kat_1)

lemma n_kat_3: "n x  y  t z = 0  n x  y  y  n z"
  using local.n_kat_2 n_kat_1 by force

lemma test_kat_3: "test p  test q   p  x  !q = 0  p  x  x  q"
  using n_kat_3 by auto

lemma n_kat_prop: "n x  y  n z = n x  y  t x  y  t z = y  t z"
  by (metis local.annir local.n_kat_1_opp local.n_kat_var local.t_n_closed local.test_mult_comp mult_assoc)

lemma test_kat_prop: "test p  test q    p  x = p  x  q   x  !q = !p  x  !q"
  by (metis local.annir local.test1_var local.test_comp_mult2 local.test_eq4 mult_assoc)

lemma n_kat_3_opp: "t x  y  n z = 0  y  n z  n x  y"
  by (metis local.n_kat_1_var local.n_kat_2_opp local.t_n_closed)

lemma kat_1_var: "n x  y  n z = y  n z  y  n z  n x  y"
  using local.n_kat_2_opp by force
 
lemma "test p; test q  (px!q = 0)  (!pxq = 0)"
  (* nitpick *) oops

lemma "n x  y + t x  z = n x  y  n x  y + t x  z = t x  z"
(*nitpick*)
oops

end

end