# 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 _"  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)"
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"

lemma add_assoc: "n x ⊕ (n y ⊕ n z) = (n x ⊕ n y) ⊕ n z"

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"

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"

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"

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"

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"

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"

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"

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"
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"

lemma ts_ord_anti: "n x ⊑ n y ⟹ t y ⊑ t x"

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"

lemma n_subid: "n x ⊑ 1"

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"

lemma n_add_lubI: "n x ⊑ n z ⟹ n y ⊑ n z ⟹ n x ⊕ n y ⊑ n z"

lemma n_add_lub: "n x ⊑ n z ∧ n y ⊑ n z ⟷ n x ⊕ n y ⊑ n z"

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"
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)"
finally show "n x ⊑ n y ⊕ n z"
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)"
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"

lemma add_transl [simp]: "n x + n y = n x ⊕ n y"

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 ("!_"  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)"

lemma test_propE [elim!]: "test x ⟹ P (t x) ⟹ P x"

lemma test_comp_closed [simp]: "test p ⟹ test (!p)"

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)"

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"

lemma test_one_var: "test 1"

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"

lemma test_add_comp [simp]: "test p ⟹ p + !p = 1"

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"

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)"

lemma test_add_distr: "test p ⟹ test q ⟹ test r ⟹ p + q ⋅ r = (p + q) ⋅ (p + r)"

lemma n_add_distl: "(n x ⋅ n y) + n z = (n x + n z) ⋅ (n y + n z)"

lemma test_add_distl_var: "test p ⟹ test q ⟹ test r ⟹ p ⋅ q + r = (p + r) ⋅ (q + r)"

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"

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"
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"
thus " t x ⋅ y ⋅ n z = 0"
next
assume "n n x ⋅ y ⋅ n z = 0"
hence "n x ⋅ y ⋅ n z = 1 ⋅ y ⋅ n z"
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"

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"

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; p⋅x = x⋅p; p⋅y = y⋅p⟧ ⟹ p⋅(x + y) = (x + y)⋅p"
(* nitpick *) oops

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"
(* 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)⋅(q⋅y + !q⋅x) = q⋅y + !q⋅p⋅x"
(* 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"

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"
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"
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; 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 "⟦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"
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; p⋅x⋅!q = 0⟧ ⟹ !p⋅x⋅q = 0"
(* nitpick *) oops

lemma "⟦test p; test q; p⋅x = p⋅x⋅q⟧ ⟹ x⋅!q = !p⋅x⋅!q"
(* nitpick *) oops

lemma "⟦test p; test q; p⋅x = p⋅x⋅q⟧ ⟹ p⋅x⋅!q = 0"
(* nitpick *) oops

lemma "⟦test p; test q; p⋅x = p⋅x⋅q⟧ ⟹ !p⋅x⋅q = 0"
(* nitpick *) oops

lemma "⟦test p; test q; x⋅!q = !p⋅x⋅!q⟧ ⟹ !p⋅x⋅q = 0"
(* nitpick *) oops

lemma "⟦test p; test q; !p⋅x⋅q = 0⟧ ⟹ p⋅x = p⋅x⋅q"
(* nitpick *) oops

lemma "⟦test p; test q; !p⋅x⋅q = 0⟧ ⟹ x⋅!q = !p⋅x⋅!q"
(* nitpick *) oops

lemma "⟦test p; test q; !p⋅x⋅q = 0⟧ ⟹ p⋅x⋅!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⟧ ⟹ (p⋅x⋅!q = 0) ⟹ (!p⋅x⋅q = 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"
thus " n x ⋅ (n x ⋅ y + t x ⋅ z)⇧† ≤ (n x ⋅ y)⇧† ⋅ n x"
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⇧⋆"

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"
thus "x⇧⋆ ⋅ n y ≤ n y ⋅ (x ⋅ n y)⇧⋆"
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"

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)⇧⋆"
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"  100) where
"test p ⟹ p⇧o = !p⋅⊤ + 1"

lemma asg: "⟦test p; test q⟧ ⟹ q ≤ 1 ∧ 1 ≤ p⇧o"

lemma assertion_isol: "test p ⟹ y ≤ p⇧o⋅x ⟷ p⋅y ≤ x"
proof
assume assms: "test p" "y ≤ p⇧o⋅x"
hence "p⋅y ≤ p⋅!p⋅⊤⋅x + p⋅x"
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"
finally show "p⋅y ≤ x"
by metis
next
assume assms: "test p" "p⋅y ≤ x"
hence "p⇧o⋅p⋅y = !p⋅⊤⋅p⋅y + p⋅y"
by (metis assertion_def distrib_right' mult_1_left mult.assoc)
also have "... = !p⋅⊤ + p⋅y"
by (metis mult.assoc top_mult_annil)
moreover have "p⇧o⋅p⋅y ≤ p⇧o⋅x"
by (metis assms(2) mult.assoc mult_isol)
moreover have "!p⋅y + p⋅y ≤ !p⋅⊤ + p⋅y"
ultimately show "y ≤ p⇧o⋅x"
qed

lemma assertion_isor: "test p ⟹ y ≤ x⋅p ⟷ y⋅p⇧o ≤ x"
proof
assume assms: "test p" "y ≤ x⋅p"
hence "y⋅p⇧o ≤ x⋅p⋅!p⋅⊤ + x⋅p"
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 "y⋅p⇧o ≤ x"
by metis
next
assume assms: "test p" "y⋅p⇧o ≤ x"
have "y ≤ y⋅(!p⋅⊤ + p)"
also have "... = y⋅p⇧o⋅p"
by (metis assertion_def assms(1) distrib_right' mult_1_left mult.assoc top_mult_annil)
finally show "y ≤ x⋅p"
by (metis assms(2) mult_isor order_trans)
qed

lemma assertion_iso: "⟦test p; test q⟧ ⟹ x⋅q⇧o ≤ p⇧o⋅x ⟷ p⋅x ≤ x⋅q"
by (metis assertion_isol assertion_isor mult.assoc)

lemma total_correctness: "⟦test p; test q⟧ ⟹ p⋅x⋅!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; p⋅x ≤ x⋅p⟧ ⟹ p⋅x⇧∞ ≤ x⇧∞⋅p"
by (metis iteration_sim)

lemma test_iteration_annir: "test p ⟹ !p⋅(p⋅x)⇧∞ = !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⟧ ⟹ (p⋅x)⇧∞⋅!p ≤ (p⋅q⋅x)⇧∞⋅!(p⋅q)⋅(p⋅x)⇧∞⋅!p"
proof -
assume assms: "test p" "test q"
hence "(p⋅x)⇧∞⋅!p = ((p⋅q) + !(p⋅q))⋅(p⋅x)⇧∞⋅!p"
also have "... = (p⋅q)⋅(p⋅x)⇧∞⋅!p + !(p⋅q)⋅(p⋅x)⇧∞⋅!p"
by (metis distrib_right')
also have "... = (p⋅q)⋅!p + (p⋅q)⋅(p⋅x)⋅(p⋅x)⇧∞⋅!p + !(p⋅q)⋅(p⋅x)⇧∞⋅!p"
by (metis iteration_unfoldr_distr mult.assoc iteration_unfold_eq distrib_left mult.assoc)
also have "... = (p⋅q)⋅(p⋅x)⋅(p⋅x)⇧∞⋅!p + !(p⋅q)⋅(p⋅x)⇧∞⋅!p"
by (metis assms less_eq_def test_preserve2 join.bot_least)
finally have "(p⋅x)⇧∞⋅!p ≤ p⋅q⋅x⋅(p⋅x)⇧∞⋅!p + !(p⋅q)⋅(p⋅x)⇧∞⋅!p"
by (metis assms(1) assms(2) order.eq_iff local.test_mult_comm_var local.test_preserve mult_assoc)
thus ?thesis
qed

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

lemma atom_step1: "r⋅b ≤ b⋅r ⟹ (a + b + r)⇧∞ = b⇧∞⋅r⇧∞⋅(a⋅b⇧∞⋅r⇧∞)⇧∞"
apply (subgoal_tac "(a + b + r)⇧∞ = (b + r)⇧∞⋅(a⋅(b + r)⇧∞)⇧∞")
apply (metis iteration_sep mult.assoc)

lemma atom_step2:
assumes "s = s⋅q" "q⋅b = 0" "r⋅q ≤ q⋅r" "q⋅l ≤ l⋅q" "r⇧∞ = r⇧⋆" "test q"
shows "s⋅l⇧∞⋅b⇧∞⋅r⇧∞⋅q⋅(a⋅b⇧∞⋅r⇧∞⋅q)⇧∞ ≤ s⋅l⇧∞⋅r⇧∞⋅(a⋅b⇧∞⋅q⋅r⇧∞)⇧∞"
proof -
have "s⋅l⇧∞⋅b⇧∞⋅r⇧∞⋅q⋅(a⋅b⇧∞⋅r⇧∞⋅q)⇧∞ ≤ s⋅l⇧∞⋅b⇧∞⋅r⇧∞⋅q⋅(a⋅b⇧∞⋅q⋅r⇧∞)⇧∞"
by (metis assms(3) assms(5) star_sim1 mult.assoc mult_isol iteration_iso)
also have "... ≤ s⋅q⋅l⇧∞⋅b⇧∞⋅r⇧∞⋅(a⋅b⇧∞⋅q⋅r⇧∞)⇧∞"
using assms(1) assms(6) local.mult_isor local.test_restrictr by auto
also have "... ≤ s⋅l⇧∞⋅q⋅b⇧∞⋅r⇧∞⋅(a⋅b⇧∞⋅q⋅r⇧∞)⇧∞"
by (metis assms(4) iteration_sim mult.assoc mult_double_iso mult_double_iso)
also have "... ≤ s⋅l⇧∞⋅r⇧∞⋅q⋅r⇧∞⋅(a⋅b⇧∞⋅q⋅r⇧∞)⇧∞"
by (metis assms(2) join.bot_least iteration_sim mult.assoc mult_double_iso)
also have "... ≤ s⋅l⇧∞⋅r⇧∞⋅(a⋅b⇧∞⋅q⋅r⇧∞)⇧∞"
by (metis assms(6) mult.assoc mult_isol test_restrictl iteration_idem mult.assoc)
finally show "s⋅l⇧∞⋅b⇧∞⋅r⇧∞⋅q⋅(a⋅b⇧∞⋅r⇧∞⋅q)⇧∞ ≤ s⋅l⇧∞⋅r⇧∞⋅(a⋅b⇧∞⋅q⋅r⇧∞)⇧∞"
by metis
qed

lemma atom_step3:
assumes "r⋅l ≤ l⋅r" "a⋅l ≤ l⋅a" "b⋅l ≤ l⋅b" "q⋅l ≤ l⋅q" "b⇧∞ = b⇧⋆"
shows "l⇧∞⋅r⇧∞⋅(a⋅b⇧∞⋅q⋅r⇧∞)⇧∞ = (a⋅b⇧∞⋅q + l + r)⇧∞"
proof -
have "(a⋅b⇧∞⋅q + r)⋅l ≤ a⋅b⇧∞⋅l⋅q + l⋅r"
by (metis distrib_right join.sup_mono assms(1,4) mult.assoc mult_isol)
also have "... ≤ a⋅l⋅b⇧∞⋅q + l⋅r"
by (metis assms(3) assms(5) star_sim1 add_iso mult.assoc mult_double_iso)
also have "... ≤ l⋅(a⋅b⇧∞⋅q + r)"
by (metis add_iso assms(2) mult_isor distrib_left mult.assoc)
finally have "(a⋅b⇧∞⋅q + r)⋅l ≤ l⋅(a⋅b⇧∞⋅q + r)"
by metis
moreover have "l⇧∞⋅r⇧∞⋅(a⋅b⇧∞⋅q⋅r⇧∞)⇧∞ = l⇧∞⋅(a⋅b⇧∞⋅q + r)⇧∞"
ultimately show ?thesis
qed

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

theorem atom_ref_back:
assumes "s = s⋅q" "a = q⋅a" "q⋅b = 0"
"r⋅b ≤ b⋅r" "r⋅l ≤ l⋅r" "r⋅q ≤ q⋅r"
"a⋅l ≤ l⋅a" "b⋅l ≤ l⋅b" "q⋅l ≤ l⋅q"
"r⇧∞ = r⇧⋆" "b⇧∞ = b⇧⋆" "test q"
shows "s⋅(a + b + r + l)⇧∞⋅q ≤ s⋅(a⋅b⇧∞⋅q + 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 = s⋅l⇧∞⋅(a + b + r)⇧∞⋅q"
also have "... ≤ s⋅l⇧∞⋅b⇧∞⋅r⇧∞⋅q⋅(a⋅b⇧∞⋅r⇧∞⋅q)⇧∞"
by (metis assms(2,4,10,11) atom_step1 iteration_slide eq_refl mult.assoc)
also have "... ≤ s⋅l⇧∞⋅r⇧∞⋅(a⋅b⇧∞⋅q⋅r⇧∞)⇧∞"
by (metis assms(1) assms(10) assms(12) assms(3) assms(6) assms(9) atom_step2)
also have "... ≤ s⋅(a⋅b⇧∞⋅q + l + r)⇧∞"
by (metis assms(11) assms(5) assms(7) assms(8) assms(9) atom_step3 eq_refl mult.assoc)
finally show ?thesis
qed

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

theorem atom_ref_back_struth:
assumes "s ≤ s⋅q" "a ≤ q⋅a" "q⋅b = 0"
"r⋅b ≤ b⋅r" "r⋅q ≤ q⋅r"
"(a + r + b)⋅l ≤ l⋅(a + r + b)" "q⋅l ≤ l⋅q"
"r⇧∞ = r⇧⋆" "q ≤ 1"
shows "s⋅(a + b + r + l)⇧∞⋅q ≤ s⋅(a⋅b⇧∞⋅q + r + l)⇧∞"
proof -
have "s⋅(a + b + r + l)⇧∞⋅q = s⋅l⇧∞⋅(a + b + r)⇧∞⋅q"
also have "... = s⋅l⇧∞⋅(b + r)⇧∞⋅(a⋅(b + r)⇧∞)⇧∞⋅q"
also have "... = s⋅l⇧∞⋅b⇧∞⋅r⇧∞⋅(a⋅b⇧∞⋅r⇧∞)⇧∞⋅q"
by (metis assms(4) iteration_sep mult.assoc)
also have "... ≤ s⋅l⇧∞⋅b⇧∞⋅r⇧∞⋅(q⋅a⋅b⇧∞⋅r⇧∞)⇧∞⋅q"
by (metis assms(2) iteration_iso mult_isol_var eq_refl order_refl)
also have "... = s⋅l⇧∞⋅b⇧∞⋅r⇧∞⋅q⋅(a⋅b⇧∞⋅r⇧∞⋅q)⇧∞"
by (metis iteration_slide mult.assoc)
also have "... ≤ s⋅q⋅l⇧∞⋅b⇧∞⋅r⇧∞⋅q⋅(a⋅b⇧∞⋅r⇧∞⋅q)⇧∞"
by (metis assms(1) mult_isor)
also have "... ≤ s⋅l⇧∞⋅q⋅b⇧∞⋅r⇧∞⋅q⋅(a⋅b⇧∞⋅r⇧∞⋅q)⇧∞"
by (metis assms(7) iteration_sim mult.assoc mult_double_iso)
also have "... ≤ s⋅l⇧∞⋅q⋅r⇧∞⋅q⋅(a⋅b⇧∞⋅r⇧∞⋅q)⇧∞"
by (metis assms(3) iteration_idep mult.assoc order_refl)
also have "... ≤ s⋅l⇧∞⋅q⋅r⇧∞⋅q⋅(a⋅b⇧∞⋅r⇧⋆⋅q)⇧∞"
by (metis assms(8) eq_refl)
also have "... ≤ s⋅l⇧∞⋅q⋅r⇧∞⋅q⋅(a⋅b⇧∞⋅q⋅r⇧⋆)⇧∞"
by (metis assms(5) iteration_iso mult.assoc mult_isol star_sim1)
also have "... = s⋅l⇧∞⋅q⋅r⇧∞⋅q⋅(a⋅b⇧∞⋅q⋅r⇧∞)⇧∞"
by (metis assms(8))
also have "... ≤ s⋅l⇧∞⋅r⇧∞⋅q⋅(a⋅b⇧∞⋅q⋅r⇧∞)⇧∞"
by (metis assms(9) mult_1_right mult_double_iso mult_isor)
also have "... ≤ s⋅l⇧∞⋅r⇧∞⋅(a⋅b⇧∞⋅q⋅r⇧∞)⇧∞"
by (metis assms(9) mult_1_right mult_double_iso)
also have "... = s⋅l⇧∞⋅(a⋅b⇧∞⋅q + r)⇧∞"
also have "... ≤ s⋅(a⋅b⇧∞⋅q + 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 "r⋅p⋅y ≤ y⋅r" "y⋅p⋅l ≤ l⋅y" "r⋅p⋅l ≤ l⋅r"
"p⋅r⋅!p = 0" "p⋅l⋅!p = 0" "!p⋅l⋅p = 0"
"y⋅0 = 0" "r⋅0 = 0" "test p"
shows "(y + r + l)⇧∞ = (p⋅l)⇧∞⋅(y + !p⋅l + r⋅!p)⇧∞⋅(r⋅p)⇧∞"
proof -
have "(y + r)⋅p⋅l ≤ l⋅y + l⋅r"
by (metis distrib_right' join.sup_mono assms(2) assms(3))
hence stepA: "(y + r)⋅p⋅l ≤ (p⋅l + !p⋅l)⋅(y + r)⇧⋆"
by (metis assms(9) distrib_left distrib_right' mult_1_left mult_isol order_trans star_ext test_add_comp)
have subStepB: "(!p⋅l + y + p⋅r + !p⋅r)⇧∞ = (!p⋅l + y + r⋅p + 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 "r⋅p⋅(y + r⋅!p + !p⋅l) ≤ y⋅(r⋅p + r⋅!p)"
also have "... ≤ (y + r⋅!p + !p⋅l)⋅(r⋅p + (y + r⋅!p + !p⋅l))"
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 "r⋅p⋅(y + r⋅!p + !p⋅l) ≤ (y + r⋅!p + !p⋅l)⋅(y + r⋅!p + !p⋅l + r⋅p)"
hence stepB: "(!p⋅l + y + p⋅r + !p⋅r)⇧∞ = (y + !p⋅l + r⋅!p)⇧∞⋅(r⋅p)⇧∞"
by (metis subStepB iteration_sep3[of "r⋅p" "y + r⋅!p + !p⋅l"]  add_assoc' add.commute)
have "(y + r + l)⇧∞ = (p⋅l + !p⋅l + y + r)⇧∞"
also have "... = (p⋅l)⇧∞⋅(!p⋅l + y + r)⇧∞" using stepA
also have "... = (p⋅l)⇧∞⋅(!p⋅l + y + p⋅r + !p⋅r)⇧∞"
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_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)

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 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)
apply (transfer, simp)
apply (transfer, simp)
apply (transfer, simp)
apply (transfer, simp)
apply (transfer, simp)
apply (transfer, simp)
apply (transfer, simp)
apply (transfer, simp)
apply (transfer, simp)
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"

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
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"
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
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"
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"
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"
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"
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 (metis local.iteration_prod_unfold)

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"
show "⋀x y z. t x ⋅ (y + z) ≤ t x ⋅ y + t x ⋅ z"
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"
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)"
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"
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⦈"

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"

(* 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"

(* 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⦄ ≡ p⋅c ≤ c⋅q"

declare hoare_triple_def[iff]

lemma hoare_triple_def_var: "p⋅c ≤ c⋅q ⟷ p⋅c⋅!q = 0"
apply (intro iffI antisym)
apply (rule order_trans[of _ "c ⋅ q ⋅ !q"])
apply (rule mult_isor[rule_format])
apply (rule order_trans[of _ "p⋅c⋅(!q + q)"])
apply simp
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⦄ x⋅y ⦃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 = (t⋅c)⇧⋆⋅!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 ≡ p⋅c1 + !p⋅c2"

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"

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 ⟷ p⋅y ≤ x ∧ !p⋅y ≤ 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 "p⋅x = p⋅x⋅q ⟹ p⋅x⋅!q = 0"
nitpick oops

lemma test1: "p⋅x⋅!q = 0 ⟹ p⋅x = p⋅x⋅q"

lemma test2: "p⋅q⋅p = p⋅q"
by (metis inf.commute inf.left_idem test_inf)

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

lemma test4: "!p⋅q⋅p = 0"
by (metis double_compl test3 test_not)

lemma total_correctness: "p⋅x⋅!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: "p⋅x ≤ x⋅p ⟹ p⋅x⇧∞ ≤ x⇧∞⋅p"
by (metis iteration_sim)

lemma test_iteration_annir: "!p⋅(p⋅x)⇧∞ = !p"
by (metis annil iteration_idep mult.assoc test_comp_mult1)

end

end