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