Session KAT_and_DRA

Theory 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, hide_lams) 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

Theory 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

Theory 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

Theory DRAT

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

section ‹Demonic Refinement Algebra with Tests›

theory DRAT
  imports KAT Kleene_Algebra.DRA
begin

text ‹
  In this section, we define demonic refinement algebras with tests and prove the most important theorems from
  the literature. In this context, tests are also known as guards.
›

class drat = dra + test_semiring_zerol
begin

subclass kat_zerol ..

text ‹
  An assertion is a mapping from a guard to a subset similar to tests, but it aborts if the predicate does
  not hold.
›

definition assertion :: "'a  'a" ("_o" [101] 100) where
  "test p  po = !p + 1"

lemma asg: "test p; test q  q  1  1  po"
  by (simp add: assertion_def local.test_subid)

lemma assertion_isol: "test p  y  pox  py  x"
proof
  assume assms: "test p" "y  pox"
  hence "py  p!px + px"
    by (metis add_commute assertion_def local.distrib_left local.iteration_prod_unfold local.iteration_unfoldl_distr local.mult_isol local.top_mult_annil mult_assoc)
  also have "...  x"
    by (simp add: assms(1) local.test_restrictl)
  finally show "py  x"
    by metis
next
  assume assms: "test p" "py  x"
  hence "popy = !ppy + py"
    by (metis assertion_def distrib_right' mult_1_left mult.assoc)
  also have "... = !p + py"
    by (metis mult.assoc top_mult_annil)
  moreover have "popy  pox"
    by (metis assms(2) mult.assoc mult_isol)
  moreover have "!py + py  !p + py"
    using local.add_iso local.top_elim by blast
  ultimately show "y  pox"    
    by (metis add.commute assms(1) distrib_right' mult_1_left order_trans test_add_comp)
qed

lemma assertion_isor: "test p  y  xp  ypo  x"
proof
  assume assms: "test p" "y  xp"
  hence "ypo  xp!p + xp"
    by (metis mult_isor assertion_def assms(1) distrib_left mult_1_right mult.assoc)
  also have "...  x"
    by (metis assms(1) local.iteration_idep local.join.sup.absorb_iff1 local.join.sup_commute local.join.sup_ge2 local.mult_1_right local.mult_isol_var local.mult_isor local.mult_onel local.test_add_comp local.test_comp_mult2 mult_assoc)
  finally show "ypo  x"
    by metis
next
  assume assms: "test p" "ypo  x"
  have "y  y(!p + p)"
    by (metis join.sup_mono mult_isol order_refl order_refl top_elim add.commute assms(1) mult_1_right test_add_comp)
  also have "... = ypop"
    by (metis assertion_def assms(1) distrib_right' mult_1_left mult.assoc top_mult_annil)
  finally show "y  xp"
    by (metis assms(2) mult_isor order_trans)
qed

lemma assertion_iso: "test p; test q  xqo  pox  px  xq"
  by (metis assertion_isol assertion_isor mult.assoc)

lemma total_correctness: "test p; test q  px!q = 0  x!q  !p"
  apply standard
  apply (metis local.test_eq4 local.top_elim mult_assoc)
  by (metis annil order.antisym test_comp_mult2 join.bot_least mult_assoc mult_isol)

lemma test_iteration_sim: "test p; px  xp  px  xp"
  by (metis iteration_sim)

lemma test_iteration_annir: "test p  !p(px) = !p"
  by (metis annil test_comp_mult1 iteration_idep mult.assoc)

text ‹Next we give an example of a program transformation from von Wright~\cite{Wright02}.›

lemma loop_refinement: "test p; test q  (px)!p  (pqx)!(pq)(px)!p"
proof -
  assume assms: "test p" "test q"
  hence "(px)!p = ((pq) + !(pq))(px)!p"
    by (simp add: local.test_mult_closed)
  also have "... = (pq)(px)!p + !(pq)(px)!p"
    by (metis distrib_right')
  also have "... = (pq)!p + (pq)(px)(px)!p + !(pq)(px)!p"
    by (metis iteration_unfoldr_distr mult.assoc iteration_unfold_eq distrib_left mult.assoc)
  also have "... = (pq)(px)(px)!p + !(pq)(px)!p"
    by (metis assms less_eq_def test_preserve2 join.bot_least)
  finally have "(px)!p  pqx(px)!p + !(pq)(px)!p"
    by (metis assms(1) assms(2) order.eq_iff local.test_mult_comm_var local.test_preserve mult_assoc)
  thus ?thesis
    by (metis coinduction add.commute mult.assoc)
qed

text ‹Finally, we prove different versions of Back's atomicity refinement theorem for action systems.›

lemma atom_step1: "rb  br  (a + b + r) = br(abr)"
  apply (subgoal_tac "(a + b + r) = (b + r)(a(b + r))")
  apply (metis iteration_sep mult.assoc)
  by (metis add_assoc' add.commute iteration_denest)

 
lemma atom_step2: 
  assumes "s = sq" "qb = 0" "rq  qr" "ql  lq" "r = r" "test q"
  shows "slbrq(abrq)  slr(abqr)"
proof -
  have "slbrq(abrq)  slbrq(abqr)"
    by (metis assms(3) assms(5) star_sim1 mult.assoc mult_isol iteration_iso)
  also have "...  sqlbr(abqr)"
    using assms(1) assms(6) local.mult_isor local.test_restrictr by auto
  also have "...  slqbr(abqr)"
    by (metis assms(4) iteration_sim mult.assoc mult_double_iso mult_double_iso)
  also have "...  slrqr(abqr)" 
    by (metis assms(2) join.bot_least iteration_sim mult.assoc mult_double_iso)
  also have "...  slr(abqr)"
    by (metis assms(6) mult.assoc mult_isol test_restrictl iteration_idem mult.assoc)
  finally show "slbrq(abrq)  slr(abqr)"
    by metis
qed

lemma atom_step3: 
  assumes "rl  lr" "al  la" "bl  lb" "ql  lq" "b = b"
  shows "lr(abqr) = (abq + l + r)"
proof -
  have "(abq + r)l  ablq + lr"
    by (metis distrib_right join.sup_mono assms(1,4) mult.assoc mult_isol)
  also have "...  albq + lr"
    by (metis assms(3) assms(5) star_sim1 add_iso mult.assoc mult_double_iso)
  also have "...  l(abq + r)"
    by (metis add_iso assms(2) mult_isor distrib_left mult.assoc)
  finally have "(abq + r)l  l(abq + r)"
    by metis
  moreover have "lr(abqr) = l(abq + r)"
    by (metis add.commute mult.assoc iteration_denest)
  ultimately show ?thesis
    by (metis add.commute add.left_commute iteration_sep)
qed

text ‹
  This is Back's atomicity refinement theorem, as specified by von Wright~\cite {Wright02}.
›

theorem atom_ref_back: 
  assumes "s = sq" "a = qa" "qb = 0"
          "rb  br" "rl  lr" "rq  qr"
          "al  la" "bl  lb" "ql  lq"
          "r = r" "b = b" "test q"
  shows "s(a + b + r + l)q  s(abq + r + l)"
proof -
  have "(a + b + r)l  l(a + b + r)"
    by (metis join.sup_mono distrib_right' assms(5) assms(7) assms(8) distrib_left)
  hence "s(l + a + b + r)q = sl(a + b + r)q"
    by (metis add.commute add.left_commute mult.assoc iteration_sep)
  also have "...  slbrq(abrq)"
    by (metis assms(2,4,10,11) atom_step1 iteration_slide eq_refl mult.assoc)
  also have "...  slr(abqr)" 
    by (metis assms(1) assms(10) assms(12) assms(3) assms(6) assms(9) atom_step2)
  also have "...  s(abq + l + r)"
    by (metis assms(11) assms(5) assms(7) assms(8) assms(9) atom_step3 eq_refl mult.assoc)
  finally show ?thesis
    by (metis add.commute add.left_commute)
qed

text ‹
  This variant is due to H\"ofner, Struth and Sutcliffe~\cite{HofnerSS09}.
›

theorem atom_ref_back_struth: 
  assumes "s  sq" "a  qa" "qb = 0"
          "rb  br" "rq  qr"
          "(a + r + b)l  l(a + r + b)" "ql  lq"
          "r = r" "q  1"
  shows "s(a + b + r + l)q  s(abq + r + l)"
proof -
  have "s(a + b + r + l)q = sl(a + b + r)q"
    by (metis add.commute add.left_commute assms(6) iteration_sep mult.assoc)
  also have "... = sl(b + r)(a(b + r))q"
    by (metis add_assoc' add.commute iteration_denest add.commute mult.assoc)
  also have "... = slbr(abr)q"
    by (metis assms(4) iteration_sep mult.assoc)
  also have "...  slbr(qabr)q"
    by (metis assms(2) iteration_iso mult_isol_var eq_refl order_refl)
  also have "... = slbrq(abrq)"
    by (metis iteration_slide mult.assoc)
  also have "...  sqlbrq(abrq)"
    by (metis assms(1) mult_isor)
  also have "...  slqbrq(abrq)"
    by (metis assms(7) iteration_sim mult.assoc mult_double_iso)
  also have "...  slqrq(abrq)"
    by (metis assms(3) iteration_idep mult.assoc order_refl)
  also have "...  slqrq(abrq)"
    by (metis assms(8) eq_refl)
  also have "...  slqrq(abqr)"
    by (metis assms(5) iteration_iso mult.assoc mult_isol star_sim1)
  also have "... = slqrq(abqr)"
    by (metis assms(8))
  also have "...  slrq(abqr)"
    by (metis assms(9) mult_1_right mult_double_iso mult_isor)
  also have "...  slr(abqr)"
    by (metis assms(9) mult_1_right mult_double_iso)
  also have "... = sl(abq + r)"
    by (metis add.commute mult.assoc iteration_denest)
  also have "...  s(abq + r + l)"
    by (metis add.commute iteration_subdenest mult.assoc mult_isol)
  finally show ?thesis .
qed
    

text ‹Finally, we prove Cohen's~\cite{Cohen00} variation of the atomicity refinement theorem.›

lemma atom_ref_cohen: 
  assumes "rpy  yr" "ypl  ly" "rpl  lr"
          "pr!p = 0" "pl!p = 0" "!plp = 0"
          "y0 = 0" "r0 = 0" "test p"
  shows "(y + r + l) = (pl)(y + !pl + r!p)(rp)"
proof -    
  have "(y + r)pl  ly + lr"
    by (metis distrib_right' join.sup_mono assms(2) assms(3))
  hence stepA: "(y + r)pl  (pl + !pl)(y + r)"
    by (metis assms(9) distrib_left distrib_right' mult_1_left mult_isol order_trans star_ext test_add_comp)
  have subStepB: "(!pl + y + pr + !pr) = (!pl + y + rp + r!p)"
    by (metis add_assoc' annil assms(8) assms(9) distrib_left distrib_right' star_slide star_subid test_add_comp join.bot_least)
  have "rp(y + r!p + !pl)  y(rp + r!p)"
    by (metis assms(1,4,9) distrib_left add_0_left add.commute annil mult.assoc test_comp_mult2 distrib_left mult_oner test_add_comp)
  also have "...  (y + r!p + !pl)(rp + (y + r!p + !pl))"
    by (meson local.eq_refl local.join.sup_ge1 local.join.sup_ge2 local.join.sup_mono local.mult_isol_var local.order_trans)
  finally have "rp(y + r!p + !pl)  (y + r!p + !pl)(y + r!p + !pl + rp)" 
    by (metis add.commute)
  hence stepB: "(!pl + y + pr + !pr) = (y + !pl + r!p)(rp)" 
    by (metis subStepB iteration_sep3[of "rp" "y + r!p + !pl"]  add_assoc' add.commute)
  have "(y + r + l) = (pl + !pl + y + r)"
    by (metis add_comm add.left_commute assms(9) distrib_right' mult_onel test_add_comp)
  also have "... = (pl)(!pl + y + r)" using stepA
    by (metis assms(6-8) annil add.assoc add_0_left distrib_right' add.commute mult.assoc iteration_sep4[of "y+r" "!pl" "pl"])
  also have "... = (pl)(!pl + y + pr + !pr)"
    by (metis add.commute assms(9) combine_common_factor mult_1_left test_add_comp)
  finally show ?thesis using stepB
    by (metis mult.assoc)
qed
end

end

Theory DRA_Models

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

section ‹Models for Demonic Refinement Algebra with Tests›

theory DRA_Models
  imports DRAT
begin

text ‹
  We formalise the predicate transformer model of demonic refinement algebra.
  Predicate transformers are formalised as strict and additive functions over a field of sets,
  or alternatively as costrict and multiplicative functions. 
  In the future, this should be merged with Preoteasa's more abstract formalisation~\cite{Preoteasa11}.
›

no_notation 
  plus (infixl "+" 65) and 
  less_eq  ("'(≤')") and
  less_eq  ("(_/  _)"  [51, 51] 50)

notation comp (infixl "" 55)

type_synonym 'a bfun = "'a set  'a set"

text ‹
  Definitions of signature:
›

definition top :: "'a bfun" where "top  λx. UNIV"
definition bot :: "'a bfun" where "bot  λx. {}"
definition adjoint :: "'a bfun  'a bfun" where "adjoint f  (λp. - f (-p))"

definition fun_inter :: "'a bfun  'a bfun  'a bfun" (infix "" 51) where
  "f  g  λp. f p  g p"

definition fun_union :: "'a bfun  'a bfun  'a bfun" (infix "+" 52) where
  "f + g  λp. f p  g p"

definition fun_order :: "'a bfun  'a bfun  bool" (infix "" 50) where
  "f  g  p. f p  g p"

definition fun_strict_order :: "'a bfun  'a bfun  bool" (infix "<." 50) where
  "f <. g  f  g  f  g"

definition N :: "'a bfun  'a bfun" where
  "N f  ((adjoint f o bot)  id)"

lemma top_max: "f  top"
  by (auto simp: top_def fun_order_def)

lemma bot_min: "bot  f"
  by (auto simp: bot_def fun_order_def)

lemma oder_def: "f  g = f  f  g"
  by (metis fun_inter_def fun_order_def le_iff_inf)

lemma order_def_var: "f  g  f  g = f"
  by (auto simp: fun_inter_def fun_order_def)

lemma adjoint_idem [simp]: "adjoint (adjoint f) = f"
  by (auto simp: adjoint_def)

lemma adjoint_prop1[simp]: "(f o top)  (adjoint f o bot) = bot"
  by (auto simp: fun_inter_def adjoint_def bot_def top_def)

lemma adjoint_prop2[simp]: "(f o top) + (adjoint f o bot) = top"
  by (auto simp: fun_union_def adjoint_def bot_def top_def)

lemma adjoint_mult: "adjoint (f o g) = adjoint f o adjoint g"
  by (auto simp: adjoint_def)

lemma adjoint_top[simp]: "adjoint top = bot"
  by (auto simp: adjoint_def bot_def top_def)

lemma N_comp1: "(N (N f)) + N f = id"
  by (auto simp: fun_union_def N_def fun_inter_def adjoint_def bot_def)

lemma N_comp2: "(N (N f)) o N f = bot"
  by (auto simp: N_def fun_inter_def adjoint_def bot_def)

lemma N_comp3: "N f o (N (N f)) = bot"
  by (auto simp: N_def fun_inter_def adjoint_def bot_def)

lemma N_de_morgan: "N (N f) o N (N g) = N (N f)  N (N g)"
  by (auto simp: fun_union_def N_def fun_inter_def adjoint_def bot_def)

lemma conj_pred_aux [simp]: "(λp. x p  y p) = y  p. x p  y p"
  by (metis Un_upper1)

text ‹
  Next, we define a type for conjuctive or multiplicative predicate transformers.
›

typedef 'a bool_op = "{f::'a bfun. (g h. mono f  f  g + f  h = f  (g + h)  bot o f = bot)}"
  apply (rule_tac x="λx. x" in exI)
  apply auto
  apply (metis monoI)
  by (auto simp: fun_order_def fun_union_def)

setup_lifting type_definition_bool_op

text ‹
  Conjuctive predicate transformers form a dioid with tests without right annihilator.
›

instantiation bool_op :: (type) dioid_one_zerol 
begin
  lift_definition less_eq_bool_op :: "'a bool_op  'a bool_op  bool" is fun_order .

  lift_definition less_bool_op :: "'a bool_op  'a bool_op  bool" is "(<.)" .

  lift_definition zero_bool_op :: "'a bool_op" is "bot"
    by (auto simp: bot_def fun_union_def fun_order_def mono_def)

  lift_definition one_bool_op :: "'a bool_op" is "id"
    by (auto simp: fun_union_def fun_order_def mono_def)

  lift_definition times_bool_op :: "'a bool_op  'a bool_op  'a bool_op" is "(o)" 
    by (auto simp: o_def fun_union_def fun_order_def bot_def mono_def) metis

  lift_definition plus_bool_op :: "'a bool_op  'a bool_op  'a bool_op" is "(+)"
    apply (auto simp: o_def fun_union_def fun_order_def bot_def mono_def)
    apply (metis subsetD)
    apply (metis subsetD)
    apply (rule ext)
    by (metis (no_types, lifting) semilattice_sup_class.sup.assoc semilattice_sup_class.sup.left_commute)

  instance
    by standard (transfer, auto simp: fun_order_def fun_strict_order_def fun_union_def bot_def)+

end

instantiation bool_op :: (type) test_semiring_zerol 
begin
  lift_definition n_op_bool_op :: "'a bool_op  'a bool_op" is "N"
    by (auto simp: N_def fun_inter_def adjoint_def bot_def fun_union_def mono_def)

  instance
  apply standard
  apply (transfer, clarsimp simp add: N_def adjoint_def bot_def id_def comp_def fun_inter_def)
  apply (transfer, clarsimp simp add: N_def adjoint_def bot_def id_def comp_def fun_inter_def fun_union_def mono_def, blast)
  apply (transfer, clarsimp simp add: N_def adjoint_def bot_def comp_def mono_def fun_union_def fun_inter_def)
  by (transfer, clarsimp simp add: N_def adjoint_def bot_def comp_def mono_def fun_union_def fun_inter_def, blast)

end

definition fun_star :: "'a bfun  'a bfun" where
  "fun_star f = lfp (λr. f o r + id)"

definition fun_iteration :: "'a bfun  'a bfun" where
  "fun_iteration f = gfp (λg. f o g + id)"
  
text ‹
  Verifying the iteration laws is left for future work. This could be obtained by integrating
  Preoteasa's approach~\cite{Preoteasa11}.
›

end

Theory KAT_Models

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

section ‹Models for Kleene Algebra with Tests›

theory KAT_Models
  imports Kleene_Algebra.Kleene_Algebra_Models KAT
begin

text ‹
  We show that binary relations under the obvious definitions form a Kleene algebra with tests.
›

interpretation rel_dioid_tests: test_semiring "(∪)" "(O)" Id "{}" "(⊆)" "(⊂)" "λx. Id  ( - x)"
  by (standard, auto)

interpretation rel_kat: kat "(∪)" "(O)" Id "{}" "(⊆)" "(⊂)" rtrancl "λx. Id  ( - x)"
  by (unfold_locales)


typedef 'a relation = "UNIV::'a rel set" by auto

setup_lifting type_definition_relation

instantiation relation :: (type) kat
begin

  lift_definition n_op_relation :: "'a relation  'a relation" is "λx. Id  ( - x)" done
  lift_definition zero_relation :: "'a relation" is "{}" done
  lift_definition star_relation :: "'a relation  'a relation" is "rtrancl" done
  lift_definition less_eq_relation :: "'a relation  'a relation  bool" is "(⊆)" done
  lift_definition less_relation :: "'a relation  'a relation  bool" is "(⊂)" done
  lift_definition one_relation :: "'a relation" is "Id" done
  lift_definition times_relation :: "'a relation  'a relation  'a relation" is "(O)" done
  lift_definition plus_relation :: "'a relation  'a relation  'a relation" is "(∪)" done

  instance
  apply standard
  apply (transfer, simp add: Un_assoc)
  apply (transfer, simp add: Un_commute)
  apply (transfer, simp add: rel_dioid.mult_assoc)
  apply (transfer, simp)
  apply (transfer, simp)
  apply (transfer, simp)
  apply (transfer, simp)
  apply (transfer, simp)
  apply (transfer, simp)
  apply (transfer, simp add: rel_dioid.less_eq_def)
  apply (transfer, simp add: rel_dioid.less_def)
  apply (transfer, simp)
  apply (transfer, simp)
  apply (transfer, simp)
  apply (transfer, simp)
  apply (transfer, simp add: rel_kleene_algebra.star_inductl)
  apply (transfer, simp add: rel_kleene_algebra.star_inductr)
  apply (transfer, simp)
  apply (transfer, blast)
  apply (transfer, blast)
  by (transfer, blast)

end


end

Theory FolkTheorem

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

section ‹Transformation Theorem for while Loops›

theory FolkTheorem
  imports Conway_Tests KAT DRAT
begin

text ‹
  We prove Kozen's transformation theorem for while loops \cite{Kozen97} in a weak setting that unifies
  previous proofs in Kleene algebra with tests, demonic refinement algebras and a variant of probabilistic
  Kleene algebra.
›

context test_pre_conway
begin

abbreviation pres :: "'a  'a  bool" where
  "pres x y  y  x = y  x  y"

lemma pres_comp: "pres y z  pres x z  pres (x  y) z"
  by (metis mult_assoc)

lemma test_pres1: "test p  test q  pres p q"
  by (simp add: local.test_mult_comm_var mult_assoc)

lemma test_pres2: "test p  test q  pres x q  pres (p  x) q"
  using pres_comp test_pres1 by blast

lemma cond_helper1:
assumes "test p" and "pres x p" 
shows "p  (p  x + !p  y)  (p  z + !p  w) = p  x  z"
proof -
  have "p  (p  z + !p  w) = p  z"
    by (metis assms(1) local.add_zerol local.annil local.join.sup_commute local.n_left_distrib_var local.test_comp_mult2 local.test_mult_idem_var mult_assoc)
  hence "p  (p  x + !p  y)  (p  z + !p  w) = (p  x)  p  z"
    using assms(1) assms(2) local.test_preserve1 mult_assoc by auto
  thus ?thesis
   using assms(1) assms(2) local.test_preserve mult_assoc by auto
qed

lemma cond_helper2: 
assumes "test p" and "pres y (!p)" 
shows "!p  (p  x + !p  y)  (p  z + !p  w) = !p  y  w"
proof -
  have "!p  (!p  y + !(!p)  x)  (!p  w + !(!p)  z) = !p  y  w"
    using assms(1) local.test_comp_closed assms(2) cond_helper1 by blast
  thus ?thesis
    using add_commute assms(1) by auto
qed

lemma cond_distr_var: 
  assumes "test p" and "test q" and "test r"
  shows "(q  p + r  !p)  (p  x + !p  y) = q  p  x + r  !p  y" 
proof -
  have "(q  p + r  !p)  (p  x + !p  y) = q  p  p  x + q  p  !p  y + r  !p  p  x + r  !p  !p  y"
    using assms(1) assms(2) assms(3) local.distrib_right' local.join.sup_assoc local.n_left_distrib_var local.test_comp_closed mult_assoc by presburger
  also have "... = q  p  x + q  0  y + r  0  x + r  !p   y"
    by (simp add: assms(1) mult_assoc)
  finally show ?thesis
    by (metis assms(2) assms(3) local.add_zerol local.annil local.join.sup_commute local.test_mult_comm_var local.test_zero_var)
qed

lemma cond_distr: 
  assumes "test p" and "test q" and "test r"
  shows "(p  q + !p  r)  (p  x + !p  y) = p  q  x + !p  r  y" 
    using  assms(1) assms(2) assms(3) local.test_mult_comm_var assms(1) assms(2) assms(3) cond_distr_var local.test_mult_comm_var by auto

theorem conditional: 
assumes "test p" and "test q" and "test r1" and "test r2"
and "pres x1 q" and "pres y1 q" and "pres x2 (!q)" and "pres y2 (!q)"
shows "(p  q + !p  !q)  (q  x1 + !q  x2)  ((q  r1 + !q  r2)  (q  y1 + !q  y2))  !(q  r1 + !q  r2) =     
(p  q + !p  !q)  (p  x1  (r1  y1)  !r1 + !p  x2  (r2  y2)  !r2)"
proof -
  have a: "p  q  x1  q  (q  r1  y1 + !q  r2  y2)  (q  !r1 + !q  !r2) = p  q  x1  q  (r1  y1)  !r1"
    by (metis assms(2) assms(3)  assms(6) cond_helper1 mult_assoc test_pres2)
  have b: "!q  (q  r1  y1 + !q  r2  y2)  (q  !r1 + !q  !r2) = !q  (r2  y2)  !r2"
    by (metis assms(2) assms(4) assms(8) local.test_comp_closed cond_helper2 mult_assoc test_pres2)
  have "(p  q + !p  !q)  (q  x1 + !q  x2)  ((q  r1 + !q  r2)  (q  y1 + !q  y2))  !(q  r1 + !q  r2) =
        p  q  x1  q  (q  r1  y1 + !q  r2  y2)  (q  !r1 + !q  !r2) + !p  !q  x2  !q  (q  r1  y1 + !q  r2  y2)  (q  !r1 + !q  !r2)"
    using assms(1) assms(2) assms(3) assms(4) assms(5) assms(7) cond_distr cond_distr_var local.test_dist_var2 mult_assoc by auto
  also have "... =  p  q  x1  (r1  y1)  !r1 + !p  !q   x2  (r2  y2)  !r2"
    by (metis a assms(5) assms(7) b mult_assoc)
  finally show ?thesis
    using assms(1) assms(2) cond_distr mult_assoc by auto
qed

theorem nested_loops: 
  assumes "test p" and "test q"
  shows "p  x  ((p + q)  (q  y + !q  x))  !(p + q) + !p = (p  x  (q  y)  !q)  !p"
proof -
  have "p  x  ((p + q)  (q  y + !q  x))  !(p + q) + !p = p  x  (q  y)  (!q  p  x  (q  y))  !q  !p + !p"
    using assms(1) assms(2) local.dagger_denest2 local.test_distrib mult_assoc test_mult_comm_var by auto
  also have "... =  p  x  (q  y)  !q  (p  x  (q  y)  !q)   !p + !p"
    by (metis local.dagger_slide mult_assoc)
  finally show ?thesis
    using add_commute by force
qed

lemma postcomputation:
  assumes "test p" and "pres y (!p)"
  shows "!p  y + p  (p  x  (!p  y + p))  !p = (p  x)  !p  y"
proof -
  have "p  (p  x  (!p  y + p))  !p = p  (1 + p  x  ((!p  y + p)  p  x)  (!p  y + p))  !p"
    by (metis dagger_prod_unfold mult.assoc)
  also have "... = (p + p  p  x  ((!p  y + p)  p  x)  (!p  y + p))  !p"
    using assms(1) local.mult_oner local.n_left_distrib_var mult_assoc by presburger 
  also have "... = p  x  (!p  y  p  x + p  x)  !p  y  !p"
    by (simp add: assms(1) mult_assoc)
  also have "... = p  x  (!p  y  0 + p  x)  !p  y"
    by (metis assms(1) assms(2) local.annil local.test_comp_mult1 mult_assoc)
  also have "... = p  x   (p   x)  (!p  y  0  (p  x))  !p  y"
    by (metis mult.assoc add.commute dagger_denest2)
  finally have "p  (p  x  (!p  y + p))  !p = p  x  (p  x)  !p  y"
    by (metis local.add_zeror local.annil local.dagger_prod_unfold local.dagger_slide local.mult_oner mult_assoc)
  thus ?thesis
    by (metis dagger_unfoldl_distr mult.assoc)
qed

lemma composition_helper: 
  assumes "test p" and "test q"
  and "pres x p"
  shows "p  (q  x)  !q  p = p  (q  x)  !q"
proof (rule order.antisym)
  show "p  (q  x)  !q  p  p  (q  x)  !q"
    by (simp add: assms(1) local.test_restrictr)
next
  have "p  q  x  q  x  p"
    by (metis assms(1) assms(2) assms(3) local.test_kat_2 mult_assoc test_pres2)
  hence "p  (q  x)  (q  x)  p"
    by (simp add: local.dagger_simr mult_assoc)
  thus "p  (q  x)  !q  p  (q  x)  !q  p"
    by (metis assms(1) assms(2) order.eq_iff local.test_comp_closed local.test_kat_2 local.test_mult_comm_var mult_assoc)
qed

theorem composition:
  assumes "test p" and "test q" 
  and "pres y p" and "pres y (!p)"
  shows "(p  x)  !p  (q  y)  !q = !p  (q  y)  !q + p  (p  x  (!p  (q  y)  !q + p))  !p"
    by (metis assms(1) assms(2) assms(4) composition_helper local.test_comp_closed mult_assoc postcomputation)
end

text ‹
  Kleene algebras with tests form pre-Conway algebras, therefore the transformation theorem is valid for KAT as well.
›

sublocale kat  pre_conway star ..

text ‹
  Demonic refinement algebras form pre-Conway algebras, therefore the transformation theorem is valid for DRA as well.
›
sublocale drat  pre_conway strong_iteration
  apply standard
  apply (simp add: local.iteration_denest local.iteration_slide)
  apply (metis local.iteration_prod_unfold)
  by (simp add: local.iteration_sim)
 
text ‹
  We do not currently consider an expansion of probabilistic Kleene algebra.
›

end

Theory PHL_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 ‹Propositional Hoare Logic›

theory PHL_KAT
  imports KAT Kleene_Algebra.PHL_KA
begin

text ‹We define a class of pre-dioids with notions of assertions, tests and iteration. The above rules of PHL are derivable in that class.›

class at_pre_dioid = pre_dioid_one +
  fixes alpha :: "'a  'a" ("α")
  and tau :: "'a  'a" ("τ")
  assumes at_pres: "α x  τ y  τ y  α x  τ y"
  and as_left_supdistl: "α x  (y + z)  α x  y + α x  z"

begin

text ‹Only the conditional and the iteration rule need to be considered (in addition to the export laws. 
In this context, they no longer depend on external assumptions. The other ones do not depend on any assumptions anyway.›

lemma at_phl_cond: 
assumes "α u  τ v  x  x  z" and "α u  τ w  y  y  z" 
shows "α u  (τ v  x + τ w  y)  (τ v  x + τ w  y)  z"
  using assms as_left_supdistl at_pres phl_cond by blast

lemma ht_at_phl_cond: 
assumes "α u  τ v x z" and "α u  τ w y z" 
shows "α u (τ v  x + τ w  y) z"
  using assms by (fact at_phl_cond)

lemma  ht_at_phl_export1: 
assumes "α x  τ y z w"
shows "α x τ y  z w"
  by (simp add: assms at_pres ht_phl_export1)

lemma ht_at_phl_export2: 
assumes "x y α z"
shows "x y  τ w α z  τ w"
  using assms at_pres ht_phl_export2 by auto

end

class at_it_pre_dioid = at_pre_dioid + it_pre_dioid
begin

lemma at_phl_while:  
assumes "α p  τ s  x  x  α p"
shows "α p  (it (τ s  x)  τ w)   it (τ s  x)  τ w  (α p  τ w)"
  by (simp add: assms at_pres it_simr phl_while)

lemma ht_at_phl_while:  
assumes "α p  τ s x α p"
shows "α p it (τ s  x)  τ w α p  τ w"
  using assms by (fact at_phl_while)

end

text ‹The following statements show that pre-Conway algebras, Kleene algebras with tests
and demonic refinement algebras form pre-dioids with test and assertions. This automatically
generates propositional Hoare logics for these structures.›

sublocale test_pre_dioid_zerol < phl: at_pre_dioid where alpha = t and tau = t
proof 
  show "x y. t x  t y  t y  t x  t y"
    by (simp add: n_mult_comm mult_assoc)
  show "x y z. t x  (y + z)  t x  y + t x  z"
    by (simp add: n_left_distrib)
qed

sublocale test_pre_conway < phl: at_it_pre_dioid where alpha = t and tau = t and it = dagger ..

sublocale kat_zerol < phl: at_it_pre_dioid where alpha = t and tau = t and it = star ..

context test_pre_dioid_zerol begin

abbreviation if_then_else :: "'a  'a  'a  'a" ("if _ then _ else _ fi" [64,64,64] 63) where
  "if p then x else y fi  (p  x + !p  y)"
 
lemma phl_n_cond: 
  "n v  n w x z  n v  t w y z  n v n w  x + t w  y z"
  by (metis phl.ht_at_phl_cond t_n_closed)

lemma phl_test_cond: 
  assumes "test p" and "test b"
  and "p  b x q" and "p  !b y q" 
  shows "p b  x + !b  y q"
  by (metis assms local.test_double_comp_var phl_n_cond)

lemma phl_cond_syntax: 
  assumes "test p" and "test b"
  and "p  b x q" and "p  !b y q" 
  shows "p if b then x else y fi q"
  using assms by (fact phl_test_cond)

lemma phl_cond_syntax_iff: 
  assumes "test p" and "test b"
  shows "p  b x q  p  !b y q  p if b then x else y fi q"
proof
  assume a: "p  b x q  p  !b y q"
  show "p if b then x else y fi q"
    using a assms(1) assms(2) phl_test_cond by auto
next
  assume a: "p if b then x else y fi q"
  have "p  b  x  b  p  (b  x + !b  y)"
    by (metis assms(1) assms(2) local.mult.assoc local.subdistl local.test_preserve)
  also have "...  b  (b  x + !b  y)  q"
    using a local.mult_isol mult_assoc by auto
  also have "...  = (b  b  x + b  !b  y)  q"
    using assms(2) local.n_left_distrib_var mult_assoc by presburger
  also have "... = b  x  q"
    by (simp add: assms(2))
  finally have b: "p  b  x  x  q"
    by (metis assms(2) local.order_trans local.test_restrictl mult_assoc)
  have "p  !b  y = !b  p  !b  y"
    by (simp add: assms(1) assms(2) local.test_preserve)
  also have "...  !b  p  (b  x + !b  y)"
    by (simp add: local.mult_isol mult_assoc)
  also have "...  !b  (b  x + !b  y)  q"
    using a local.mult_isol mult_assoc by auto
  also have "... = (!b  b  x + !b  !b  y)  q"
    using local.n_left_distrib mult_assoc by presburger
  also have "... = !b  y  q"
    by (simp add: assms(2))
  finally have c: "p  !b  y  y  q"
    by (metis local.dual_order.trans local.n_restrictl mult_assoc)
  show "p  b x q  p  !b y q"
    using b c by auto
qed

end

context test_pre_conway
begin

lemma  phl_n_while: 
  assumes "n x   n y z n x"
  shows "n x (n y  z)  t y n x  t y"
  by (metis assms phl.ht_at_phl_while t_n_closed)

end

context kat_zerol
begin

abbreviation while :: "'a  'a  'a" ("while _ do _ od" [64,64] 63) where
  "while b do x od  (b  x)  !b"

lemma  phl_n_while: 
  assumes "n x   n y z n x"
  shows "n x (n y  z)  t y n x  t y"
  by (metis assms phl.ht_at_phl_while t_n_closed)

lemma phl_test_while: 
  assumes "test p" and "test b" 
  and "p  b x p"
  shows "p (b  x)  !b p  !b"
  by (metis assms phl_n_while test_double_comp_var)

lemma phl_while_syntax: 
  assumes "test p" and "test b" and "p  b x p"
  shows "p while b do x od p  !b"
  by (metis assms phl_test_while)

end

lemma (in kat) "test p  p  x  x  p  p  x  x  p"
  oops

lemma (in kat) "test p  test b  p  (b  x)  !b  (b  x)  !b  p  !b  p  b  x  x  p"
  oops

lemma (in kat) "test p  test q   p  x  y  x  y  q (r. test r  p  x  x  r  r  y   y  q)"
  (* nitpick *)  oops

lemma (in kat) "test p  test q   p  x  y  !q = 0 (r. test r  p  x  !r = 0  r  y  !q = 0)"
  (* nitpick *) oops

text ‹The following facts should be moved. They show that the rules of Hoare logic based on Tarlecki triples are invertible.›

abbreviation (in near_dioid) tt :: "'a  'a  'a  bool" ("___") where
  "x y z  x  y  z" 

lemma (in near_dioid_one) tt_skip: "p 1 p"
  by simp

lemma (in near_dioid) tt_cons1: "(q'. p x q'  q' q)  p x q"
  using local.order_trans by blast

lemma (in near_dioid) tt_cons2:  "(p'. p' x q  p  p')  p x q"
  using local.dual_order.trans local.mult_isor by blast

lemma (in near_dioid) tt_seq: "(r. p x r  r y q)  p x  y q"
  by (metis local.tt_cons2 mult_assoc)

lemma (in dioid) tt_cond: "p  v x q  p  w y q  p (v  x + w  y)q"
  by (simp add: local.distrib_left mult_assoc)

lemma (in kleene_algebra) tt_while: "w  1  p  v x p  p (v  x)  w p"
  by (metis local.star_inductr_var_equiv local.star_subid local.tt_seq local.tt_skip mult_assoc)

text ‹The converse implication can be refuted. The situation is similar to the ht case.›

lemma (in kat) tt_while: "test v   p (v  x)  !v p  p  v x p"
  (* nitpick *) oops

lemma (in kat) tt_while: "test v   p (v  x)  p  p  v x p"
  using local.star_inductr_var_equiv mult_assoc by auto

text ‹Perhaps this holds with possibly infinite loops in DRA...›

text ‹wlp in KAT›

lemma (in kat) "test y  ( z. test z  z  x  !y = 0)"
  by (metis local.annil local.test_zero_var)

end                                                                                             

Theory PHL_DRAT

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

section ‹Propositional Hoare Logic›

theory PHL_DRAT
  imports DRAT Kleene_Algebra.PHL_DRA PHL_KAT
begin

sublocale drat < phl: at_it_pre_dioid where alpha = t and tau = t and it = strong_iteration ..

context drat
begin

no_notation while ("while _ do _ od" [64,64] 63)

abbreviation while :: "'a  'a  'a" ("while _ do _ od" [64,64] 63) where
  "while b do x od  (b  x)  !b"

lemma  phl_n_while: 
  assumes "n x   n y z n x"
  shows "n x (n y  z)  t y n x  t y"
  by (metis assms phl.ht_at_phl_while t_n_closed)

lemma phl_test_while: 
  assumes "test p" and "test b" 
  and "p  b x p"
  shows "p (b  x)  !b p  !b"
  by (metis assms phl_n_while test_double_comp_var)

lemma phl_while_syntax: 
  assumes "test p" and "test b" and "p  b x p"
  shows "p while b do x od p  !b"
  by (metis assms phl_test_while)

end

end

Theory KAT2

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

section ‹Two sorted Kleene Algebra with Tests›

theory KAT2
  imports Kleene_Algebra.Kleene_Algebra
begin

text ‹
  As an alternative to the one-sorted implementation of tests, we provide a two-sorted, more 
  conventional one. In this setting, Isabelle's Boolean algebra theory can be used.
  This alternative can be developed further along the lines of the one-sorted implementation.
›

syntax "_kat" :: "'a  'a" ("`_`")

ML val kat_test_vars = ["p","q","r","s","t","p'","q'","r'","s'","t'","p''","q''","r''","s''","t''"]

fun map_ast_variables ast =
  case ast of
    (Ast.Variable v) =>
      if exists (fn tv => tv = v) kat_test_vars
      then Ast.Appl [Ast.Variable "test", Ast.Variable v]
      else Ast.Variable v
  | (Ast.Constant c) => Ast.Constant c
  | (Ast.Appl []) => Ast.Appl []
  | (Ast.Appl (f :: xs)) => Ast.Appl (f :: map map_ast_variables xs)

structure KATHomRules = Named_Thms
  (val name = @{binding "kat_hom"}
   val description = "KAT test homomorphism rules")

fun kat_hom_tac ctxt n =
  let
    val rev_rules = map (fn thm => thm RS @{thm sym}) (KATHomRules.get ctxt)
  in
    asm_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps rev_rules) n
  end

setup KATHomRules.setup

method_setup kat_hom = ‹
Scan.succeed (fn ctxt => SIMPLE_METHOD (CHANGED (kat_hom_tac ctxt 1)))

parse_ast_translation let
  fun kat_tr ctxt [t] = map_ast_variables t
in [(@{syntax_const "_kat"}, kat_tr)] end

ML structure VCGRules = Named_Thms
  (val name = @{binding "vcg"}
   val description = "verification condition generator rules")

fun vcg_tac ctxt n =
  let
    fun vcg' [] = no_tac
      | vcg' (r :: rs) = resolve_tac ctxt [r] n ORELSE vcg' rs;
  in REPEAT (CHANGED
       (kat_hom_tac ctxt n
        THEN REPEAT (vcg' (VCGRules.get ctxt))
        THEN kat_hom_tac ctxt n
        THEN TRY (resolve_tac ctxt @{thms order_refl} n ORELSE asm_full_simp_tac (put_simpset HOL_basic_ss ctxt) n)))
  end

method_setup vcg = ‹
Scan.succeed (fn ctxt => SIMPLE_METHOD (CHANGED (vcg_tac ctxt 1)))

setup VCGRules.setup

locale dioid_tests =
  fixes test :: "'a::boolean_algebra  'b::dioid_one_zerol"
  and not :: "'b::dioid_one_zerol  'b::dioid_one_zerol" ("-")
  assumes test_sup [simp,kat_hom]: "test (sup p q) = `p + q`"
  and test_inf [simp,kat_hom]: "test (inf p q) = `p  q`"
  and test_top [simp,kat_hom]: "test top = 1"
  and test_bot [simp,kat_hom]: "test bot = 0"
  and test_not [simp,kat_hom]: "test (- p) = `-p`"
  and test_iso_eq [kat_hom]: "p  q  `p  q`"
begin

notation test ("ι")

lemma test_eq [kat_hom]: "p = q  `p = q`"
  by (metis eq_iff test_iso_eq)

ML_val ‹map (fn thm => thm RS @{thm sym}) (KATHomRules.get @{context})

lemma test_iso: "p  q  `p  q`"
  by (simp add: test_iso_eq)

(* Import lemmas and modify them to fit KAT syntax *)

lemma test_meet_comm: "`p  q = q  p`"
  by kat_hom (fact inf_commute)

lemmas test_one_top[simp] = test_iso[OF top_greatest, simplified]

lemma [simp]: "`-p + p = 1`"
  by kat_hom (metis compl_sup_top)

lemma [simp]: "`p + (-p) = 1`"
  by kat_hom (metis sup_compl_top)

lemma [simp]: "`(-p)  p = 0`"
  by (metis inf.commute inf_compl_bot test_bot test_inf test_not)

lemma [simp]: "`p  (-p) = 0`"
  by (metis inf_compl_bot test_bot test_inf test_not)

end

locale kat = 
  fixes test :: "'a::boolean_algebra  'b::kleene_algebra"
  and not :: "'b::kleene_algebra  'b::kleene_algebra" ("!")
  assumes is_dioid_tests: "dioid_tests test not"

sublocale kat  dioid_tests using is_dioid_tests .

context kat
begin

notation test ("ι")

lemma test_eq [kat_hom]: "p = q  `p = q`"
  by (metis eq_iff test_iso_eq)

ML_val ‹map (fn thm => thm RS @{thm sym}) (KATHomRules.get @{context})

lemma test_iso: "p  q  `p  q`"
  by (simp add: test_iso_eq)

(* Import lemmas and modify them to fit KAT syntax *)

lemma test_meet_comm: "`p  q = q  p`"
  by kat_hom (fact inf_commute)

lemmas test_one_top[simp] = test_iso[OF top_greatest, simplified]

lemma test_star [simp]: "`p = 1`"
  by (metis star_subid test_iso test_top top_greatest)

lemmas [kat_hom] = test_star[symmetric]

lemma [simp]: "`!p + p = 1`"
  by kat_hom (metis compl_sup_top)

lemma [simp]: "`p + !p = 1`"
  by kat_hom (metis sup_compl_top)

lemma [simp]: "`!p  p = 0`"
  by (metis inf.commute inf_compl_bot test_bot test_inf test_not)

lemma [simp]: "`p  !p = 0`"
  by (metis inf_compl_bot test_bot test_inf test_not)

definition hoare_triple :: "'b  'b  'b  bool" ("_ _ _") where
  "p c q  pc  cq"

declare hoare_triple_def[iff]

lemma hoare_triple_def_var: "`pc  cq  pc!q = 0`"
  apply (intro iffI antisym)
  apply (rule order_trans[of _ "`c  q  !q`"])
  apply (rule mult_isor[rule_format])
  apply (simp add: mult.assoc)+
  apply (simp add: mult.assoc[symmetric])
  apply (rule order_trans[of _ "`pc(!q + q)`"])
  apply simp
  apply (simp only: distrib_left add_zerol)
  apply (rule order_trans[of _ "`1  c  q`"])
  apply (simp only: mult.assoc)
  apply (rule mult_isor[rule_format])
  by simp_all

lemmas [intro!] = star_sim2[rule_format]

lemma hoare_weakening: "p  p'  q'  q  `p' c q'`  `p c q`"
  by auto (metis mult_isol mult_isor order_trans test_iso)

lemma hoare_star: "`p c p`  `p c p`"
  by auto

lemmas [vcg] = hoare_weakening[OF order_refl _ hoare_star]

lemma hoare_test [vcg]: "`p  t  q`  `p t q`"
  by auto (metis inf_le2 le_inf_iff test_inf test_iso_eq)

lemma hoare_mult [vcg]: "`p x r`  `r y q`  `p xy q`"
proof auto
  assume [simp]: "`p  x  x  r`" and [simp]: "`r  y  y  q`"
  have "`p  (x  y)  x  r  y`"
    by (auto simp add: mult.assoc[symmetric] intro!: mult_isor[rule_format])
  also have "`...  x  y  q`"
    by (auto simp add: mult.assoc intro!: mult_isol[rule_format])
  finally show "`p  (x  y)  x  y  q`" .
qed

lemma [simp]: "`!p  !p = !p`"
  by (metis inf.idem test_inf test_not)

lemma hoare_plus [vcg]: "`p x q`  `p y q`  `p x + y q`"
proof -
  assume a1: "ι p x ι q"
  assume "ι p y ι q"
  hence "ι p  (x + y)  x  ι q + y  ι q"
    using a1 by (metis (no_types) distrib_left hoare_triple_def join.sup.mono)
  thus ?thesis
    by force
qed

definition While :: "'b  'b  'b" ("While _ Do _ End" [50,50] 51) where
  "While t Do c End = (tc)!t"

lemma hoare_while: "`p  t c p`  `p While t Do c End !t  p`"
  unfolding While_def by vcg (metis inf_commute order_refl)

lemma [vcg]: "`p  t c p`  `!t  p  q`  `p While t Do c End q`"
  by (metis hoare_weakening hoare_while order_refl test_inf test_iso_eq test_not)

definition If :: "'b  'b  'b  'b" ("If _ Then _ Else _" [50,50,50] 51) where
  "If p Then c1 Else c2  pc1 + !pc2"

lemma hoare_if [vcg]: "`p  t c1 q`  `p  !t c2 q`  `p If t Then c1 Else c2 q`"
  unfolding If_def by vcg assumption

end

end

Theory DRAT2

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

section ‹Two sorted Demonic Refinement Algebras›

theory DRAT2
  imports Kleene_Algebra.DRA
begin

text ‹
  As an alternative to the one-sorted implementation of demonic refinement algebra with tests, 
  we provide a two-sorted, more conventional one.
  This alternative can be developed further along the lines of the one-sorted implementation.
›

syntax "_dra" :: "'a  'a" ("`_`")

ML val dra_test_vars = ["p","q","r","s","t","p'","q'","r'","s'","t'","p''","q''","r''","s''","t''"]

fun map_ast_variables ast =
  case ast of
    (Ast.Variable v) =>
      if exists (fn tv => tv = v) dra_test_vars
      then Ast.Appl [Ast.Variable "test", Ast.Variable v]
      else Ast.Variable v
  | (Ast.Constant c) => Ast.Constant c
  | (Ast.Appl []) => Ast.Appl []
  | (Ast.Appl (f :: xs)) => Ast.Appl (f :: map map_ast_variables xs)

structure DRAHomRules = Named_Thms
  (val name = @{binding "kat_hom"}
   val description = "KAT test homomorphism rules")

fun dra_hom_tac ctxt n =
  let
    val rev_rules = map (fn thm => thm RS @{thm sym}) (DRAHomRules.get ctxt)
  in
    asm_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps rev_rules) n
  end

setup DRAHomRules.setup

method_setup kat_hom = ‹
  Scan.succeed (fn ctxt => SIMPLE_METHOD (CHANGED (dra_hom_tac ctxt 1)))

parse_ast_translation let
  fun dra_tr ctxt [t] = map_ast_variables t
in [(@{syntax_const "_dra"}, dra_tr)] end

ML structure VCGRules = Named_Thms
  (val name = @{binding "vcg"}
   val description = "verification condition generator rules")

fun vcg_tac ctxt n =
  let
    fun vcg' [] = no_tac
      | vcg' (r :: rs) = resolve_tac ctxt [r] n ORELSE vcg' rs;
  in REPEAT (CHANGED
       (dra_hom_tac ctxt n
        THEN REPEAT (vcg' (VCGRules.get ctxt))
        THEN dra_hom_tac ctxt n
        THEN TRY (resolve_tac ctxt @{thms order_refl} n ORELSE asm_full_simp_tac (put_simpset HOL_basic_ss ctxt) n)))
  end

method_setup vcg = ‹
  Scan.succeed (fn ctxt => SIMPLE_METHOD (CHANGED (vcg_tac ctxt 1)))

setup VCGRules.setup

locale drat =
  fixes test :: "'a::boolean_algebra  'b::dra"
  and not :: "'b::dra  'b::dra" ("!")
  assumes test_sup [simp,kat_hom]: "test (sup p q) = `p + q`"
  and test_inf [simp,kat_hom]: "test (inf p q) = `p  q`"
  and test_top [simp,kat_hom]: "test top = 1"
  and test_bot [simp,kat_hom]: "test bot = 0"
  and test_not [simp,kat_hom]: "test (- p) = `!p`"
  and test_iso_eq [kat_hom]: "p  q  `p  q`"

begin

notation test ("ι")

lemma test_eq [kat_hom]: "p = q  `p = q`"
  by (metis eq_iff test_iso_eq)

ML_val ‹map (fn thm => thm RS @{thm sym}) (DRAHomRules.get @{context})

lemma test_iso: "p  q  `p  q`"
  by (simp add: test_iso_eq)

lemma test_meet_comm: "`p  q = q  p`"
  by kat_hom (fact inf_commute)

lemmas test_one_top[simp] = test_iso[OF top_greatest, simplified]

lemma test_star [simp]: "`p = 1`"
  by (metis star_subid test_iso test_top top_greatest)

lemmas [kat_hom] = test_star[symmetric]

lemma test_comp_add1 [simp]: "`!p + p = 1`"
  by kat_hom (metis compl_sup_top)

lemma test_comp_add2 [simp]: "`p + !p = 1`"
  by kat_hom (metis sup_compl_top)

lemma test_comp_mult1 [simp]: "`!p  p = 0`"
  by (metis inf.commute inf_compl_bot test_bot test_inf test_not)

lemma test_comp_mult2 [simp]: "`p  !p = 0`"
  by (metis inf_compl_bot test_bot test_inf test_not)

lemma test_eq1: "`y  x`  `py  x`  `!py  x`"
  apply standard
  apply (metis mult_isol_var mult_onel test_not test_one_top)
  apply (subgoal_tac "`(p + !p)y  x`")
  apply (metis mult_onel sup_compl_top test_not test_sup test_top)
  by (metis distrib_right' join.sup.bounded_iff)

lemma "`px = pxq`  `px!q = 0`"
  nitpick oops

lemma test1: "`px!q = 0`  `px = pxq`"
  by (metis add_0_left distrib_left mult_oner test_comp_add1)

lemma test2: "`pqp = pq`"
  by (metis inf.commute inf.left_idem test_inf)

lemma test3: "`pq!p = 0`"
  by (metis inf.assoc inf.idem inf.left_commute inf_compl_bot test_bot test_inf test_not)

lemma test4: "`!pqp = 0`"
  by (metis double_compl test3 test_not)

lemma total_correctness: "`px!q = 0`  `x!q  !p`"
  apply standard
  apply (metis join.bot.extremum mult.assoc test_eq1 top_elim)
  by (metis (no_types, hide_lams) add_zeror annil less_eq_def mult.assoc mult_isol test_comp_mult2)

lemma test_iteration_sim: "`px  xp`  `px  xp`"
  by (metis iteration_sim)

lemma test_iteration_annir: "`!p(px) = !p`"
  by (metis annil iteration_idep mult.assoc test_comp_mult1)

end

end