Theory FolkTheorem

(* Title:      Kleene algebra with tests
   Author:     Alasdair Armstrong, Victor B. F. Gomes, Georg Struth
   Maintainer: Georg Struth <g.struth at sheffield.ac.uk>
*)

section ‹Transformation Theorem for while Loops›

theory FolkTheorem
  imports Conway_Tests KAT DRAT
begin

text ‹
  We prove Kozen's transformation theorem for while loops \<^cite>‹"Kozen97"› in a weak setting that unifies
  previous proofs in Kleene algebra with tests, demonic refinement algebras and a variant of probabilistic
  Kleene algebra.
›

context test_pre_conway
begin

abbreviation pres :: "'a ⇒ 'a ⇒ bool" where
  "pres x y ≡ y ⋅ x = y ⋅ x ⋅ y"

lemma pres_comp: "pres y z ⟹ pres x z ⟹ pres (x ⋅ y) z"
  by (metis mult_assoc)

lemma test_pres1: "test p ⟹ test q ⟹ pres p q"
  by (simp add: local.test_mult_comm_var mult_assoc)

lemma test_pres2: "test p ⟹ test q ⟹ pres x q ⟹ pres (p ⋅ x) q"
  using pres_comp test_pres1 by blast

lemma cond_helper1:
assumes "test p" and "pres x p" 
shows "p ⋅ (p ⋅ x + !p ⋅ y)⇧^† ⋅ (p ⋅ z + !p ⋅ w) = p ⋅ x⇧^† ⋅ z"
proof -
  have "p ⋅ (p ⋅ z + !p ⋅ w) = p ⋅ z"
    by (metis assms(1) local.add_zerol local.annil local.join.sup_commute local.n_left_distrib_var local.test_comp_mult2 local.test_mult_idem_var mult_assoc)
  hence "p ⋅ (p ⋅ x + !p ⋅ y)⇧^† ⋅ (p ⋅ z + !p ⋅ w) = (p ⋅ x)⇧^† ⋅ p ⋅ z"
    using assms(1) assms(2) local.test_preserve1 mult_assoc by auto
  thus ?thesis
   using assms(1) assms(2) local.test_preserve mult_assoc by auto
qed

lemma cond_helper2: 
assumes "test p" and "pres y (!p)" 
shows "!p ⋅ (p ⋅ x + !p ⋅ y)⇧^† ⋅ (p ⋅ z + !p ⋅ w) = !p ⋅ y⇧^† ⋅ w"
proof -
  have "!p ⋅ (!p ⋅ y + !(!p) ⋅ x)⇧^† ⋅ (!p ⋅ w + !(!p) ⋅ z) = !p ⋅ y⇧^† ⋅ w"
    using assms(1) local.test_comp_closed assms(2) cond_helper1 by blast
  thus ?thesis
    using add_commute assms(1) by auto
qed

lemma cond_distr_var: 
  assumes "test p" and "test q" and "test r"
  shows "(q ⋅ p + r ⋅ !p) ⋅ (p ⋅ x + !p ⋅ y) = q ⋅ p ⋅ x + r ⋅ !p ⋅ y" 
proof -
  have "(q ⋅ p + r ⋅ !p) ⋅ (p ⋅ x + !p ⋅ y) = q ⋅ p ⋅ p ⋅ x + q ⋅ p ⋅ !p ⋅ y + r ⋅ !p ⋅ p ⋅ x + r ⋅ !p ⋅ !p ⋅ y"
    using assms(1) assms(2) assms(3) local.distrib_right' local.join.sup_assoc local.n_left_distrib_var local.test_comp_closed mult_assoc by presburger
  also have "... = q ⋅ p ⋅ x + q ⋅ 0 ⋅ y + r ⋅ 0 ⋅ x + r ⋅ !p  ⋅ y"
    by (simp add: assms(1) mult_assoc)
  finally show ?thesis
    by (metis assms(2) assms(3) local.add_zerol local.annil local.join.sup_commute local.test_mult_comm_var local.test_zero_var)
qed

lemma cond_distr: 
  assumes "test p" and "test q" and "test r"
  shows "(p ⋅ q + !p ⋅ r) ⋅ (p ⋅ x + !p ⋅ y) = p ⋅ q ⋅ x + !p ⋅ r ⋅ y" 
    using  assms(1) assms(2) assms(3) local.test_mult_comm_var assms(1) assms(2) assms(3) cond_distr_var local.test_mult_comm_var by auto

theorem conditional: 
assumes "test p" and "test q" and "test r1" and "test r2"
and "pres x1 q" and "pres y1 q" and "pres x2 (!q)" and "pres y2 (!q)"
shows "(p ⋅ q + !p ⋅ !q) ⋅ (q ⋅ x1 + !q ⋅ x2) ⋅ ((q ⋅ r1 + !q ⋅ r2) ⋅ (q ⋅ y1 + !q ⋅ y2))⇧^† ⋅ !(q ⋅ r1 + !q ⋅ r2) =     
(p ⋅ q + !p ⋅ !q) ⋅ (p ⋅ x1 ⋅ (r1 ⋅ y1)⇧^† ⋅ !r1 + !p ⋅ x2 ⋅ (r2 ⋅ y2)⇧^† ⋅ !r2)"
proof -
  have a: "p ⋅ q ⋅ x1 ⋅ q ⋅ (q ⋅ r1 ⋅ y1 + !q ⋅ r2 ⋅ y2)⇧^† ⋅ (q ⋅ !r1 + !q ⋅ !r2) = p ⋅ q ⋅ x1 ⋅ q ⋅ (r1 ⋅ y1)⇧^† ⋅ !r1"
    by (metis assms(2) assms(3)  assms(6) cond_helper1 mult_assoc test_pres2)
  have b: "!q ⋅ (q ⋅ r1 ⋅ y1 + !q ⋅ r2 ⋅ y2)⇧^† ⋅ (q ⋅ !r1 + !q ⋅ !r2) = !q ⋅ (r2 ⋅ y2)⇧^† ⋅ !r2"
    by (metis assms(2) assms(4) assms(8) local.test_comp_closed cond_helper2 mult_assoc test_pres2)
  have "(p ⋅ q + !p ⋅ !q) ⋅ (q ⋅ x1 + !q ⋅ x2) ⋅ ((q ⋅ r1 + !q ⋅ r2) ⋅ (q ⋅ y1 + !q ⋅ y2))⇧^† ⋅ !(q ⋅ r1 + !q ⋅ r2) =
        p ⋅ q ⋅ x1 ⋅ q ⋅ (q ⋅ r1 ⋅ y1 + !q ⋅ r2 ⋅ y2)⇧^† ⋅ (q ⋅ !r1 + !q ⋅ !r2) + !p ⋅ !q ⋅ x2 ⋅ !q ⋅ (q ⋅ r1 ⋅ y1 + !q ⋅ r2 ⋅ y2)⇧^† ⋅ (q ⋅ !r1 + !q ⋅ !r2)"
    using assms(1) assms(2) assms(3) assms(4) assms(5) assms(7) cond_distr cond_distr_var local.test_dist_var2 mult_assoc by auto
  also have "... =  p ⋅ q ⋅ x1 ⋅ (r1 ⋅ y1)⇧^† ⋅ !r1 + !p ⋅ !q ⋅  x2 ⋅ (r2 ⋅ y2)⇧^† ⋅ !r2"
    by (metis a assms(5) assms(7) b mult_assoc)
  finally show ?thesis
    using assms(1) assms(2) cond_distr mult_assoc by auto
qed

theorem nested_loops: 
  assumes "test p" and "test q"
  shows "p ⋅ x ⋅ ((p + q) ⋅ (q ⋅ y + !q ⋅ x))⇧^† ⋅ !(p + q) + !p = (p ⋅ x ⋅ (q ⋅ y)⇧^† ⋅ !q)⇧^† ⋅ !p"
proof -
  have "p ⋅ x ⋅ ((p + q) ⋅ (q ⋅ y + !q ⋅ x))⇧^† ⋅ !(p + q) + !p = p ⋅ x ⋅ (q ⋅ y)⇧^† ⋅ (!q ⋅ p ⋅ x ⋅ (q ⋅ y)⇧^†)⇧^† ⋅ !q ⋅ !p + !p"
    using assms(1) assms(2) local.dagger_denest2 local.test_distrib mult_assoc test_mult_comm_var by auto
  also have "... =  p ⋅ x ⋅ (q ⋅ y)⇧^† ⋅ !q ⋅ (p ⋅ x ⋅ (q ⋅ y)⇧^† ⋅ !q)⇧^†  ⋅ !p + !p"
    by (metis local.dagger_slide mult_assoc)
  finally show ?thesis
    using add_commute by force
qed

lemma postcomputation:
  assumes "test p" and "pres y (!p)"
  shows "!p ⋅ y + p ⋅ (p ⋅ x ⋅ (!p ⋅ y + p))⇧^† ⋅ !p = (p ⋅ x)⇧^† ⋅ !p ⋅ y"
proof -
  have "p ⋅ (p ⋅ x ⋅ (!p ⋅ y + p))⇧^† ⋅ !p = p ⋅ (1 + p ⋅ x ⋅ ((!p ⋅ y + p) ⋅ p ⋅ x)⇧^† ⋅ (!p ⋅ y + p)) ⋅ !p"
    by (metis dagger_prod_unfold mult.assoc)
  also have "... = (p + p ⋅ p ⋅ x ⋅ ((!p ⋅ y + p) ⋅ p ⋅ x)⇧^† ⋅ (!p ⋅ y + p)) ⋅ !p"
    using assms(1) local.mult_oner local.n_left_distrib_var mult_assoc by presburger 
  also have "... = p ⋅ x ⋅ (!p ⋅ y ⋅ p ⋅ x + p ⋅ x)⇧^† ⋅ !p ⋅ y ⋅ !p"
    by (simp add: assms(1) mult_assoc)
  also have "... = p ⋅ x ⋅ (!p ⋅ y ⋅ 0 + p ⋅ x)⇧^† ⋅ !p ⋅ y"
    by (metis assms(1) assms(2) local.annil local.test_comp_mult1 mult_assoc)
  also have "... = p ⋅ x  ⋅ (p  ⋅ x)⇧^† ⋅ (!p ⋅ y ⋅ 0 ⋅ (p ⋅ x)⇧^†)⇧^† ⋅ !p ⋅ y"
    by (metis mult.assoc add.commute dagger_denest2)
  finally have "p ⋅ (p ⋅ x ⋅ (!p ⋅ y + p))⇧^† ⋅ !p = p ⋅ x ⋅ (p ⋅ x)⇧^† ⋅ !p ⋅ y"
    by (metis local.add_zeror local.annil local.dagger_prod_unfold local.dagger_slide local.mult_oner mult_assoc)
  thus ?thesis
    by (metis dagger_unfoldl_distr mult.assoc)
qed

lemma composition_helper: 
  assumes "test p" and "test q"
  and "pres x p"
  shows "p ⋅ (q ⋅ x)⇧^† ⋅ !q ⋅ p = p ⋅ (q ⋅ x)⇧^† ⋅ !q"
proof (rule order.antisym)
  show "p ⋅ (q ⋅ x)⇧^† ⋅ !q ⋅ p ≤ p ⋅ (q ⋅ x)⇧^† ⋅ !q"
    by (simp add: assms(1) local.test_restrictr)
next
  have "p ⋅ q ⋅ x ≤ q ⋅ x ⋅ p"
    by (metis assms(1) assms(2) assms(3) local.test_kat_2 mult_assoc test_pres2)
  hence "p ⋅ (q ⋅ x)⇧^† ≤ (q ⋅ x)⇧^† ⋅ p"
    by (simp add: local.dagger_simr mult_assoc)
  thus "p ⋅ (q ⋅ x)⇧^† ⋅ !q ≤ p ⋅ (q ⋅ x)⇧^† ⋅ !q ⋅ p"
    by (metis assms(1) assms(2) order.eq_iff local.test_comp_closed local.test_kat_2 local.test_mult_comm_var mult_assoc)
qed

theorem composition:
  assumes "test p" and "test q" 
  and "pres y p" and "pres y (!p)"
  shows "(p ⋅ x)⇧^† ⋅ !p ⋅ (q ⋅ y)⇧^† ⋅ !q = !p ⋅ (q ⋅ y)⇧^† ⋅ !q + p ⋅ (p ⋅ x ⋅ (!p ⋅ (q ⋅ y)⇧^† ⋅ !q + p))⇧^† ⋅ !p"
    by (metis assms(1) assms(2) assms(4) composition_helper local.test_comp_closed mult_assoc postcomputation)
end

text ‹
  Kleene algebras with tests form pre-Conway algebras, therefore the transformation theorem is valid for KAT as well.
›

sublocale kat ⊆ pre_conway star ..

text ‹
  Demonic refinement algebras form pre-Conway algebras, therefore the transformation theorem is valid for DRA as well.
›
sublocale drat ⊆ pre_conway strong_iteration
  apply standard
  apply (simp add: local.iteration_denest local.iteration_slide)
  apply (metis local.iteration_prod_unfold)
  by (simp add: local.iteration_sim)
 
text ‹
  We do not currently consider an expansion of probabilistic Kleene algebra.
›

end