Theory Kleene_Algebra.PHL_KA

(* Title:      Generalised Hoare Logic for Kleene Algebra
   Author:     Georg Struth
   Maintainer: Georg Struth <g.struth at sheffield.ac.uk>
               Tjark Weber <tjark.weber at it.uu.se>
*)

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