Theory KAT_and_DRA.PHL_KAT
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)"
oops
lemma (in kat) "test p ⟹ test q ⟹ p ⋅ x ⋅ y ⋅ !q = 0 ⟹(∃r. test r ∧ p ⋅ x ⋅ !r = 0 ∧ r ⋅ y ⋅ !q = 0)"
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⦈"
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