Theory VC_KAD_wf

(* Title: Verification Component Based on Divergence Kleene Algebra for Total Correctness
   Author: Victor Gomes, Georg Struth
   Maintainer: Victor Gomes <victor.gomes@cl.cam.ac.uk>
               Georg Struth <g.struth@sheffield.ac.uk> 
*)

subsection‹Verification Component for Total Correctness›

theory VC_KAD_wf

imports VC_KAD KAD.Modal_Kleene_Algebra_Applications

begin

text ‹This component supports the verification of simple while programs
in a total correctness setting.›

subsubsection ‹Relation Divergence Kleene Algebras›

text‹Divergence Kleene algebras have been formalised in the AFP entry for Kleene algebra with domain.
The nabla or divergence operation models those states of a relation from which infinitely ascending chains
may start.›

definition rel_nabla :: "'a rel ⇒ 'a rel" where 
  "rel_nabla X = ⋃ {P. P ⊆ relfdia X P}"

definition rel_nabla_bin :: "'a rel ⇒ 'a rel ⇒ 'a rel" where 
  "rel_nabla_bin X Q = ⋃ {P. P ⊆ relfdia X P ∪ rdom Q}"

lemma rel_nabla_d_closed [simp]:  "rdom (rel_nabla x) = rel_nabla x"
  by (auto simp: rel_nabla_def rel_antidomain_kleene_algebra.fdia_def rel_antidomain_kleene_algebra.ads_d_def rel_ad_def)

lemma rel_nabla_bin_d_closed [simp]:  "rdom (rel_nabla_bin x q) = rel_nabla_bin x q"
  by (auto simp: rel_nabla_bin_def rel_antidomain_kleene_algebra.fdia_def rel_antidomain_kleene_algebra.ads_d_def rel_ad_def)

lemma rel_nabla_unfold: "rel_nabla X ⊆ relfdia X (rel_nabla X)"
  by (simp add: rel_nabla_def rel_ad_def rel_antidomain_kleene_algebra.fdia_def, blast)

lemma rel_nabla_bin_unfold: "rel_nabla_bin X Q ⊆ relfdia X (rel_nabla_bin X Q) ∪ rdom Q"
  by (simp add: rel_nabla_bin_def rel_ad_def rel_antidomain_kleene_algebra.fdia_def, blast)

lemma rel_nabla_coinduct_var: "P ⊆ relfdia X P ⟹ P ⊆ rel_nabla X"
  by (simp add: rel_nabla_def rel_antidomain_kleene_algebra.fdia_def rel_ad_def, blast)

lemma rel_nabla_bin_coinduct: "P ⊆ relfdia X P ∪ rdom Q ⟹ P ⊆ rel_nabla_bin X Q"
  by (simp add: rel_nabla_bin_def rel_antidomain_kleene_algebra.fdia_def rel_ad_def, blast)

text ‹The two fusion lemmas are, in fact, hard-coded fixpoint fusion proofs. They might be replaced
by more generic fusion proofs eventually.›

lemma nabla_fusion1: "rel_nabla X ∪ relfdia (X⇧*) Q ⊆ rel_nabla_bin X Q"  
proof -
  have "rel_nabla X ∪ relfdia (X⇧*) Q ⊆ relfdia X (rel_nabla X) ∪ relfdia X (relfdia (X⇧*) Q) ∪ rdom Q"
    by (metis (no_types, lifting) Un_mono inf_sup_aci(6) order_refl rel_antidomain_kleene_algebra.dka.fdia_star_unfold_var rel_nabla_unfold sup.commute)
  also have "... = relfdia X (rel_nabla X ∪ relfdia (X⇧*) Q) ∪ rdom Q"
    by (simp add: rel_antidomain_kleene_algebra.dka.fdia_add1)
  finally show ?thesis
    using rel_nabla_bin_coinduct by blast
qed

lemma rel_ad_inter_seq: "rel_ad X ∩ rel_ad Y = rel_ad X ; rel_ad Y"
  by (auto simp: rel_ad_def)

lemma fusion2_aux2: "rdom (rel_nabla_bin X Q) ⊆ rdom (rel_nabla_bin X Q ∩ rel_ad (relfdia (X⇧*) Q) ∪ relfdia (X⇧*) Q)"
  apply (auto simp: rel_antidomain_kleene_algebra.ads_d_def rel_ad_def)
  by (metis pair_in_Id_conv r_into_rtrancl rel_antidomain_kleene_algebra.a_one rel_antidomain_kleene_algebra.a_star rel_antidomain_kleene_algebra.addual.ars_r_def rel_antidomain_kleene_algebra.dka.dns1'' rel_antidomain_kleene_algebra.dpdz.dom_one rel_antidomain_kleene_algebra.ds.ddual.rsr5 rel_antidomain_kleene_algebra.dual.conway.dagger_unfoldr_eq rel_antidomain_kleene_algebra.dual.tc_eq rel_nabla_bin_d_closed)  

lemma nabla_fusion2: "rel_nabla_bin X Q ⊆ rel_nabla X ∪ relfdia (X⇧*) Q"
proof -
  have "rel_nabla_bin X Q ∩ rel_ad (relfdia (X⇧*) Q)  ⊆ (relfdia X (rel_nabla_bin X Q) ∪ rdom Q) ∩ rel_ad (relfdia (X⇧*) Q)"
    by (meson Int_mono equalityD1 rel_nabla_bin_unfold)
  also have "... ⊆ (relfdia X (rel_nabla_bin X Q ∩ rel_ad (relfdia (X⇧*) Q) ∪ relfdia (X⇧*) Q) ∪ rdom Q) ∩ rel_ad (relfdia (X⇧*) Q)"  
    using fusion2_aux2 rel_antidomain_kleene_algebra.dka.fd_iso1 by blast
  also have "... = (relfdia X (rel_nabla_bin X Q ∩ rel_ad (relfdia (X⇧*) Q)) ∪ relfdia X (relfdia (X⇧*) Q) ∪ rdom Q) ∩ rel_ad (relfdia (X⇧*) Q)"
    by (simp add: rel_antidomain_kleene_algebra.dka.fdia_add1)
  also have "... = (relfdia X (rel_nabla_bin X Q ∩ rel_ad (relfdia (X⇧*) Q)) ∪ relfdia (X⇧*) Q) ∩ rel_ad (relfdia (X⇧*) Q)"
    using rel_antidomain_kleene_algebra.dka.fdia_star_unfold_var by blast
  finally have "rel_nabla_bin X Q ∩ rel_ad (relfdia (X⇧*) Q) ⊆ relfdia X ((rel_nabla_bin X Q) ∩ rel_ad (relfdia (X⇧*) Q))"
    by (metis (no_types, lifting) inf_commute order_trans_rules(23) rel_ad_inter_seq rel_antidomain_kleene_algebra.a_mult_add rel_antidomain_kleene_algebra.a_subid_aux1' rel_antidomain_kleene_algebra.addual.bdia_def rel_antidomain_kleene_algebra.ds.ddual.rsr5)
  hence "rdom (rel_nabla_bin X Q) ; rel_ad (relfdia (X⇧*) Q) ⊆ rdom (rel_nabla X)"
    by (metis rel_ad_inter_seq rel_antidomain_kleene_algebra.addual.ars_r_def rel_nabla_bin_d_closed rel_nabla_coinduct_var rel_nabla_d_closed)
  thus ?thesis
    by (metis rel_antidomain_kleene_algebra.addual.ars_r_def rel_antidomain_kleene_algebra.addual.bdia_def rel_antidomain_kleene_algebra.d_a_galois1 rel_antidomain_kleene_algebra.dpdz.domain_invol rel_nabla_bin_d_closed rel_nabla_d_closed)
qed

lemma rel_nabla_coinduct: "P ⊆ relfdia X P ∪ rdom Q ⟹ P ⊆ rel_nabla X ∪ relfdia (rtrancl X) Q"
  by (meson nabla_fusion2 order_trans rel_nabla_bin_coinduct)

interpretation rel_fdivka: fdivergence_kleene_algebra rel_ad "(∪)" "(;) " Id "{}" "(⊆)" "(⊂)" rtrancl rel_nabla
proof 
  fix x y z:: "'a rel"
  show "rdom (rel_nabla x) = rel_nabla x"
    by simp
  show "rel_nabla x ⊆ relfdia x (rel_nabla x)"
    by (simp add: rel_nabla_unfold)
  show "rdom y ⊆ relfdia x y ∪ rdom z ⟹ rdom y ⊆ rel_nabla x ∪ relfdia (x⇧*) z"
    by (simp add: rel_nabla_coinduct)
qed

subsubsection ‹Meta-Equational Loop  Rule›

context fdivergence_kleene_algebra
begin

text ‹The rule below is inspired by Arden' rule from language theory. It can be used in total correctness proofs.›

lemma fdia_arden: "∇x = 0 ⟹ d p ≤ d q + |x⟩ p ⟹ d p ≤ |x⇧⋆⟩ q"
proof -
  assume a1: "∇x = zero_class.zero"
  assume "d p ≤ d q + |x⟩ p"
  then have "ad (ad p) ≤ zero_class.zero + ad (ad (x⇧⋆ ⋅ q))"
    using a1 add_commute ads_d_def dka.fd_def nabla_coinduction by force
  then show ?thesis
    by (simp add: ads_d_def dka.fd_def)
qed

lemma fdia_arden_eq: "∇x = 0 ⟹ d p = d q + |x⟩ p ⟹ d p = |x⇧⋆⟩ q"
  by (simp add: fdia_arden dka.fdia_star_induct_eq order.eq_iff)

lemma fdia_arden_iff: "∇x = 0 ⟹ (d p = d q + |x⟩ p ⟷ d p = |x⇧⋆⟩ q)"
  by (metis fdia_arden_eq dka.fdia_d_simp dka.fdia_star_unfold_var)

lemma "|x⇧⋆] p ≤ |x] p"
  by (simp add: fbox_antitone_var)

lemma fbox_arden: "∇x = 0 ⟹ d q ⋅ |x] p ≤ d p ⟹ |x⇧⋆] q ≤ d p"
proof -
  assume h1: "∇x = 0" and "d q ⋅ |x] p ≤ d p"
  hence "ad p ≤ ad (d q ⋅ |x] p)"
    by (metis a_antitone' a_subid addual.ars_r_def dpdz.domain_subid dual_order.trans)
  hence "ad p ≤ ad q + |x⟩ ad p"
    by (simp add: a_6 addual.bbox_def ds.fd_def) 
  hence "ad p ≤ |x⇧⋆⟩ ad q"
    by (metis fdia_arden h1 a_4 ads_d_def dpdz.dsg1  fdia_def meet_ord_def)
  thus ?thesis
    by (metis a_antitone' ads_d_def fbox_simp fdia_fbox_de_morgan_2)
qed

lemma fbox_arden_eq: "∇x = 0 ⟹ d q ⋅ |x] p = d p ⟹ |x⇧⋆] q = d p"
  by (simp add: fbox_arden order.antisym fbox_star_induct_eq)

lemma fbox_arden_iff: "∇x = 0 ⟹ (d p = d q ⋅ |x] p ⟷ d p = |x⇧⋆] q)"  
  by (metis fbox_arden_eq fbox_simp fbox_star_unfold_var)

lemma fbox_arden_while_iff: "∇ (d t ⋅ x) = 0 ⟹ (d p = (d t + d q) ⋅ |d t ⋅ x] p ⟷ d p = |while t do x od] q)"
  by (metis fbox_arden_iff dka.dom_add_closed fbox_export3 while_def)  

lemma fbox_arden_whilei: "∇ (d t ⋅ x) = 0 ⟹ (d i = (d t + d q) ⋅ |d t ⋅ x] i ⟹ d i = |while t inv i do x od] q)"
  using fbox_arden_while_iff whilei_def by auto

lemma fbox_arden_whilei_iff: "∇ (d t ⋅ x) = 0 ⟹ (d i = (d t + d q) ⋅ |d t ⋅ x] i ⟷ d i = |while t inv i do x od] q)"
  using fbox_arden_while_iff whilei_def by auto

subsubsection ‹Noethericity and Absence of Divergence›

text ‹Noetherian elements have been defined in the AFP entry for Kleene algebra with domain. First we show 
that noethericity and absence of divergence coincide. Then we turn to the relational model and 
show that noetherian relations model terminating programs.›

lemma noether_nabla: "Noetherian x ⟹ ∇ x = 0"
  by (metis nabla_closure nabla_unfold noetherian_alt)

lemma nabla_noether_iff: "Noetherian x ⟷ ∇ x = 0"
  using nabla_noether noether_nabla by blast

lemma nabla_preloeb_iff: "∇ x = 0 ⟷ PreLoebian x"
  using Noetherian_iff_PreLoebian nabla_noether noether_nabla by blast

end

lemma rel_nabla_prop: "rel_nabla R = {} ⟷ (∀P. P ⊆ relfdia R P ⟶ P = {})"
  by (metis bot.extremum_uniqueI rel_nabla_coinduct_var rel_nabla_unfold)

lemma fdia_rel_im1: "s2r ((converse R) `` P) = relfdia R (s2r P)"
  by (auto simp: Id_on_def rel_antidomain_kleene_algebra.ads_d_def rel_ad_def rel_antidomain_kleene_algebra.fdia_def Image_def converse_def)

lemma fdia_rel_im2: "s2r ((converse R) `` (r2s (rdom P))) = relfdia R P"
  by (simp add: fdia_rel_im1 rsr)

lemma wf_nabla_aux: "(P ⊆ (converse R) `` P ⟶ P = {}) ⟷ (s2r P ⊆ relfdia R (s2r P) ⟶ s2r P = {})"
  apply (standard, metis Domain_Id_on Domain_mono Id_on_empty fdia_rel_im1)
  using fdia_rel_im1 by fastforce

text ‹A relation is noeterian if its converse is wellfounded. Hence a relation is noetherian if and only if its 
divergence is empty. In the relational program semantics, noetherian programs terminate.›

lemma wf_nabla: "wf (converse R) ⟷ rel_nabla R = {}"
  by (metis (no_types, lifting) fdia_rel_im2 rel_fdivka.nabla_unfold_eq rel_nabla_prop rel_nabla_unfold wfE_pf wfI_pf wf_nabla_aux)

end