Theory Kleene_Algebra.PHL_KA
section ‹Propositional Hoare Logic for Conway and Kleene Algebra›
theory PHL_KA
imports Kleene_Algebra
begin
text ‹This is a minimalist Hoare logic developed in the context of pre-dioids. In near-dioids, the sequencing rule would not be derivable.
Iteration is modelled by a function that needs to satisfy a simulation law.
The main assumtions on pre-dioid elements needed to derive the Hoare rules are preservation properties; an additional distributivity propery is needed
for the conditional rule.
This Hoare logic can be instantated in various ways. It covers notions of
finite and possibly infinite iteration. In this theory, it it specialised to Conway and Kleene algebras.›
class it_pre_dioid = pre_dioid_one +
fixes it :: "'a ⇒ 'a"
assumes it_simr: "y ⋅ x ≤ x ⋅ y ⟹ y ⋅ it x ≤ it x ⋅ y"
begin
lemma phl_while:
assumes "p ⋅ s ≤ s ⋅ p ⋅ s" and "p ⋅ w ≤ w ⋅ p ⋅ w"
and "(p ⋅ s) ⋅ x ≤ x ⋅ p"
shows "p ⋅ (it (s ⋅ x) ⋅ w) ≤ it (s ⋅ x) ⋅ w ⋅ (p ⋅ w)"
proof -
have "p ⋅ s ⋅ x ≤ s ⋅ x ⋅ p"
by (metis assms(1) assms(3) mult.assoc phl_export1)
hence "p ⋅ it (s ⋅ x) ≤ it (s ⋅ x) ⋅ p"
by (simp add: it_simr mult.assoc)
thus ?thesis
using assms(2) phl_export2 by blast
qed
end
text ‹Next we define a Hoare triple to make the format of the rules more explicit.›
context pre_dioid_one
begin
abbreviation (in near_dioid) ht :: "'a ⇒ 'a ⇒ 'a ⇒ bool" ("⦃_⦄_⦃_⦄") where
"⦃x⦄ y ⦃z⦄ ≡ x ⋅ y ≤ y ⋅ z"
lemma ht_phl_skip: "⦃x⦄ 1 ⦃x⦄"
by simp
lemma ht_phl_cons1: "x ≤ w ⟹ ⦃w⦄ y ⦃z⦄ ⟹ ⦃x⦄ y ⦃z⦄"
by (fact phl_cons1)
lemma ht_phl_cons2: "w ≤ x ⟹ ⦃z⦄ y ⦃w⦄ ⟹ ⦃z⦄ y ⦃x⦄"
by (fact phl_cons2)
lemma ht_phl_seq: "⦃p⦄ x ⦃r⦄ ⟹ ⦃r⦄ y ⦃q⦄ ⟹ ⦃p⦄ x ⋅ y ⦃q⦄"
by (fact phl_seq)
lemma ht_phl_cond:
assumes "u ⋅ v ≤ v ⋅ u ⋅ v" and "u ⋅ w ≤ w ⋅ u ⋅ w"
and "⋀x y. u ⋅ (x + y) ≤ u ⋅ x + u ⋅ y"
and "⦃u ⋅ v⦄ x ⦃z⦄" and "⦃u ⋅ w⦄ y ⦃z⦄"
shows "⦃u⦄ (v ⋅ x + w ⋅ y) ⦃z⦄"
using assms by (fact phl_cond)
lemma ht_phl_export1:
assumes "x ⋅ y ≤ y ⋅ x ⋅ y"
and "⦃x ⋅ y⦄ z ⦃w⦄"
shows "⦃x⦄ y ⋅ z ⦃w⦄"
using assms by (fact phl_export1)
lemma ht_phl_export2:
assumes "z ⋅ w ≤ w ⋅ z ⋅ w"
and "⦃x⦄ y ⦃z⦄"
shows "⦃x⦄ y ⋅ w ⦃z ⋅ w⦄"
using assms by (fact phl_export2)
end
context it_pre_dioid begin
lemma ht_phl_while:
assumes "p ⋅ s ≤ s ⋅ p ⋅ s" and "p ⋅ w ≤ w ⋅ p ⋅ w"
and "⦃p ⋅ s⦄ x ⦃p⦄"
shows "⦃p⦄ it (s ⋅ x) ⋅ w ⦃p ⋅ w⦄"
using assms by (fact phl_while)
end
sublocale pre_conway < phl: it_pre_dioid where it = dagger
by standard (simp add: local.dagger_simr)
sublocale kleene_algebra < phl: it_pre_dioid where it = star ..
end