Theory KAT_and_DRA.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"
    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)"
  (* 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"
  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"
  (* 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