Session Algebraic_VCs

Theory VC_KAT_scratch

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

section ‹Two Standalone Components›

theory VC_KAT_scratch
  imports Main
begin

subsection ‹Component Based on Kleene Algebra with Tests›

text ‹This component supports the verification and step-wise refinement of simple while programs
in a partial correctness setting.›

subsubsection ‹KAT: Definition and Basic Properties›

notation times (infixl "" 70)

class plus_ord = plus + ord +
  assumes less_eq_def: "x  y  x + y = y"
  and less_def: "x < y  x  y  x  y"

class dioid = semiring + one + zero + plus_ord +
  assumes add_idem [simp]: "x + x = x"
  and mult_onel [simp]: "1  x = x"
  and mult_oner [simp]: "x  1 = x"
  and add_zerol [simp]: "0 + x = x"
  and annil [simp]: "0  x = 0"
  and annir [simp]: "x  0 = 0"

begin

subclass monoid_mult 
  by (standard, simp_all)

subclass order
  apply (standard, simp_all add: less_def less_eq_def add_commute)
  apply force
  by (metis add_assoc)

lemma mult_isol: "x  y  z  x  z  y"
  by (metis distrib_left less_eq_def)

lemma mult_isor: "x  y  x  z  y  z"
  by (metis distrib_right less_eq_def)
                                         
lemma add_iso: "x  y  x + z  y + z"
  by (metis (no_types, lifting) abel_semigroup.commute add.abel_semigroup_axioms add.semigroup_axioms add_idem less_eq_def semigroup.assoc)

lemma add_lub: "x + y  z  x  z  y  z"
  by (metis add_assoc add.left_commute add_idem less_eq_def)

end

class kleene_algebra = dioid + 
  fixes star :: "'a  'a" ("_" [101] 100)
  assumes star_unfoldl: "1 + x  x  x"  
  and star_unfoldr: "1 + x  x  x"
  and star_inductl: "z + x  y  y  x  z  y"
  and star_inductr: "z + y  x  y  z  x  y"

begin

lemma star_sim: "x  y  z  x  x  y  z  x"
proof - 
  assume "x  y  z  x"
  hence "x + z  x  y  x + z  z  x"
    by (metis add_lub distrib_left eq_refl less_eq_def mult_assoc)
  also have  "...  z  x"
    using add_lub mult_isor star_unfoldr by fastforce
  finally show ?thesis
    by (simp add: star_inductr) 
qed

end

class kat = kleene_algebra +
  fixes at :: "'a  'a" 
  assumes test_one [simp]: "at (at 1) = 1"
  and test_mult [simp]: "at (at (at (at x)  at (at y))) = at (at y)  at (at x)" 
  and test_mult_comp [simp]: "at x  at (at x) = 0"
  and test_de_morgan: "at x + at y = at (at (at x)  at (at y))"

begin

definition t_op :: "'a  'a" ("t_" [100] 101) where
  "t x = at (at x)"

lemma t_n [simp]: "t (at x) = at x"
  by (metis add_idem test_de_morgan test_mult t_op_def)

lemma t_comm: "t x  t y = t y  t x"
  by (metis add_commute test_de_morgan test_mult t_op_def)

lemma t_idem [simp]: "t x  t x = t x"
  by (metis add_idem test_de_morgan test_mult t_op_def)

lemma t_mult_closed [simp]: "t (t x  t y) = t x  t y"
  using t_comm t_op_def by auto

subsubsection‹Propositional Hoare Logic›

definition H :: "'a  'a  'a  bool" where
  "H p x q  t p  x  x  t q"

definition if_then_else :: "'a  'a  'a  'a" ("if _ then _ else _ fi" [64,64,64] 63) where
  "if p then x else y fi = t p  x + at p  y"

definition while :: "'a  'a  'a" ("while _ do _ od" [64,64] 63) where
  "while p do x od = (t p  x)  at p"

definition while_inv :: "'a  'a  'a  'a" ("while _ inv _ do _ od" [64,64,64] 63) where
  "while p inv i do x od = while p do x od"

lemma H_skip: "H p 1 p"
  by (simp add: H_def)

lemma H_cons: "t p  t p'  t q'  t q  H p' x q'  H p x q"
  by (meson H_def mult_isol mult_isor order.trans)

lemma H_seq: "H r y q  H p x r   H p (x  y) q"
proof -
  assume h1: "H p x r" and h2: "H r y q"  
  hence h3: "t p  x  x  t r" and h4: "t r  y  y  t q"
    using H_def apply  blast using H_def h2 by blast
  hence "t p  x  y  x  t r  y"
    using mult_isor by blast
  also have "...  x  y  t q"
    by (simp add: h4 mult_isol mult_assoc)
  finally show ?thesis
    by (simp add: H_def mult_assoc)
qed

lemma H_cond: "H (t p  t r) x q  H (t p  at r) y q  H p (if r then x else y fi) q"
proof -
  assume h1: "H (t p  t r) x q" and h2: "H (t p  at r) y q"
  hence h3: "t r  t p  t r  x  t r  x  t q" and h4: "at r  t p  at r  y  at r  y  t q"
    by (simp add: H_def mult_isol mult_assoc, metis H_def h2 mult_isol mult_assoc t_mult_closed t_n)
  hence h5: "t p  t r  x  t r  x  t q" and  h6: "t p  at r  y  at r  y  t q"
    by (simp add: mult_assoc t_comm, metis h4 mult_assoc t_comm t_idem t_n)
  have "t p  (t r  x + at r  y) = t p  t r  x + t p  at r  y"
    by (simp add: distrib_left mult_assoc)
  also have "...  t r  x  t q + t p  at r  y"
    using h5 add_iso by blast
  also have "...  t r  x  t q + at r  y  t q"
    by (simp add: add_commute h6 add_iso)
  finally show ?thesis
    by (simp add: H_def if_then_else_def distrib_right)
qed

lemma H_loop: "H (t p  t r) x p  H p (while r do x od) (t p  at r)"
proof - 
  assume  "H (t p  t r) x p"
  hence "t r  t p  t r  x  t r  x  t p"
    by (metis H_def distrib_left less_eq_def mult_assoc t_mult_closed)
  hence "t p  t r  x  t r  x  t p"
    by (simp add: mult_assoc t_comm)
  hence "t p  (t r  x)  at r  (t r  x)  t p  at r"
    by (metis mult_isor star_sim mult_assoc)
  hence "t p  (t r  x)  at r  (t r  x)  at r  t p  at r"
    by (metis mult_assoc t_comm t_idem t_n)
  thus ?thesis
    by (metis H_def mult_assoc t_mult_closed t_n while_def)
qed

lemma H_while_inv: "t p  t i  t i  at r  t q  H (t i  t r) x i  H p (while r inv i do x od) q"
  by (metis H_cons H_loop t_mult_closed t_n while_inv_def)

end

subsubsection‹Soundness and Relation KAT›

notation relcomp (infixl ";" 70)

interpretation rel_d: dioid Id "{}" "(∪)" "(;)" "(⊆)" "(⊂)" 
  by (standard, auto)

lemma (in dioid) power_inductl: "z + x  y  y  x ^ i  z  y"
  apply (induct i; clarsimp simp add: add_lub)
  by (metis local.dual_order.trans local.mult_isol mult_assoc)

lemma (in dioid) power_inductr: "z + y  x  y  z  x ^ i  y"
  apply (induct i; clarsimp simp add: add_lub)
  proof -
    fix i
    assume "z  x ^ i  y" "z  y" "y  x  y"
    hence "(z  x ^ i)  x  y"
      using local.dual_order.trans local.mult_isor by blast
    thus "z  (x  x ^ i)  y"
      by (simp add: mult_assoc local.power_commutes)
  qed

lemma power_is_relpow: "rel_d.power X i = X ^^ i"
  by (induct i, simp_all add: relpow_commute)

lemma rel_star_def: "X^* = (i. rel_d.power X i)"
  by (simp add: power_is_relpow rtrancl_is_UN_relpow)

lemma rel_star_contl: "X ; Y^* = (i. X ; rel_d.power Y i)"
  by (simp add: rel_star_def relcomp_UNION_distrib)

lemma rel_star_contr: "X^* ; Y = (i. (rel_d.power X i) ; Y)"
  by (simp add: rel_star_def relcomp_UNION_distrib2)

definition rel_at :: "'a rel  'a rel" where 
  "rel_at X = Id  - X"  

interpretation rel_kat: kat Id "{}" "(∪)" "(;)" "(⊆)" "(⊂)" rtrancl rel_at
  apply standard 
  apply auto[2]
  by (auto simp: rel_star_contr rel_d.power_inductl rel_star_contl  SUP_least rel_d.power_inductr rel_at_def)

subsubsection‹Embedding Predicates in Relations›

type_synonym 'a pred = "'a  bool"

abbreviation p2r :: "'a pred  'a rel" ("_") where
  "P  {(s,s) |s. P s}"

lemma t_p2r [simp]: "rel_kat.t_op P = P"
  by (auto simp add: rel_kat.t_op_def rel_at_def)
 
lemma p2r_neg_hom [simp]: "rel_at P = λs. ¬ P s" 
  by (auto simp: rel_at_def)

lemma p2r_conj_hom [simp]: "P  Q = λs.  P s  Q s"
  by auto 

lemma p2r_conj_hom_var [simp]: "P ; Q = λs. P s  Q s" 
  by auto 

lemma p2r_disj_hom [simp]: "P  Q = λs. P s  Q s"
  by auto 

lemma impl_prop [simp]: "P  Q  (s. P s   Q s)"
  by auto 

subsubsection ‹Store and Assignment›

type_synonym 'a store = "string   'a"

definition gets :: "string  ('a store  'a)  'a store rel" ("_ ::= _" [70, 65] 61) where 
  "v ::= e = {(s, s(v := e s)) |s. True}"

lemma H_assign: "rel_kat.H λs. P (s (v := e s)) (v ::= e) P"
  by (auto simp: gets_def rel_kat.H_def rel_kat.t_op_def rel_at_def)

lemma H_assign_var: "(s. P s  Q (s (v := e s)))  rel_kat.H P (v ::= e) Q"
  by (auto simp: gets_def rel_kat.H_def rel_kat.t_op_def rel_at_def)

abbreviation H_sugar :: "'a pred  'a rel  'a pred  bool" ("PRE _ _ POST _" [64,64,64] 63) where
  "PRE P X POST Q  rel_kat.H P X Q"

abbreviation if_then_else_sugar :: "'a pred  'a rel  'a rel  'a rel" ("IF _ THEN _ ELSE _ FI" [64,64,64] 63) where
  "IF P THEN X ELSE Y FI  rel_kat.if_then_else P X Y"

abbreviation while_inv_sugar :: "'a pred  'a pred  'a rel  'a rel" ("WHILE _ INV _ DO _ OD" [64,64,64] 63) where
  "WHILE P INV I DO X OD  rel_kat.while_inv P I X"

subsubsection ‹Verification Example›

lemma euclid:
  "PRE (λs::nat store. s ''x'' = x  s ''y'' = y)
   (WHILE (λs. s ''y''  0) INV (λs. gcd (s ''x'') (s ''y'') = gcd x y) 
    DO
     (''z'' ::= (λs. s ''y''));
     (''y'' ::= (λs. s ''x'' mod s ''y''));
     (''x'' ::= (λs. s ''z''))
    OD)
   POST (λs. s ''x'' = gcd x y)"
  apply (rule rel_kat.H_while_inv, simp_all, clarsimp)
  apply (intro rel_kat.H_seq)
  apply (subst H_assign, simp)+
  apply (rule H_assign_var)
  using gcd_red_nat by auto

subsubsection ‹Definition of Refinement KAT›

class rkat = kat +
  fixes R :: "'a  'a  'a"
  assumes R1: "H p (R p q) q"
  and R2: "H p x q  x  R p q"

begin

subsubsection ‹Propositional Refinement Calculus›

lemma R_skip: "1  R p p"
  by (simp add: H_skip R2)

lemma R_cons: "t p  t p'  t q'  t q  R p' q'  R p q"
  by (simp add: H_cons R2 R1)

lemma R_seq: "(R p r)  (R r q)  R p q"
  using H_seq R2 R1 by blast

lemma R_cond: "if v then (R (t v  t p) q) else (R (at v  t p) q) fi  R p q"
  by (metis H_cond R1 R2 t_comm t_n)

lemma R_loop: "while q do (R (t p  t q) p) od   R p (t p  at q)"
  by (simp add: H_loop R2 R1)

end

subsubsection ‹Soundness and Relation RKAT›

definition rel_R :: "'a rel  'a rel  'a rel" where 
  "rel_R P Q = {X. rel_kat.H P X Q}"

interpretation rel_rkat: rkat Id "{}" "(∪)"  "(;)" "(⊆)" "(⊂)" rtrancl rel_at rel_R
  by (standard, auto simp: rel_R_def rel_kat.H_def rel_kat.t_op_def rel_at_def)

subsubsection ‹Assignment Laws›

lemma R_assign: "(s. P s  Q (s (v := e s)))  (v ::= e)  rel_R P Q"
  by (simp add: H_assign_var rel_rkat.R2)

lemma R_assignr: "(s. Q' s  Q (s (v := e s)))  (rel_R P Q') ; (v ::= e)  rel_R P Q"
proof -
  assume a1: "s. Q' s  Q (s(v := e s))"
  have "p pa cs f. fa. (p fa  cs ::= f  rel_R p pa)  (¬ pa (fa(cs := f fa::'a))  cs ::= f  rel_R p pa)"
    using R_assign by blast
  hence "v ::= e  rel_R Q' Q" 
    using a1 by blast
  thus ?thesis 
    by (meson dual_order.trans rel_d.mult_isol rel_rkat.R_seq)
qed

lemma R_assignl: "(s. P s  P' (s (v := e s)))  (v ::= e) ; (rel_R P' Q)  rel_R P Q"
proof -
  assume a1: "s. P s  P' (s(v := e s))"
  have "p pa cs f. fa. (p fa  cs ::= f  rel_R p pa)  (¬ pa (fa(cs := f fa::'a))  cs ::= f  rel_R p pa)"
    using R_assign by blast
  then have "v ::= e  rel_R P P'"
    using a1 by blast
  then show ?thesis
    by (meson dual_order.trans rel_d.mult_isor rel_rkat.R_seq)
qed  

subsubsection ‹Refinement Example›

lemma var_swap_ref1: 
  "rel_R λs. s ''x'' = a  s ''y'' = b λs. s ''x'' = b  s ''y'' = a 
    (''z'' ::= (λs. s ''x'')); rel_R λs. s ''z'' = a  s ''y'' = b λs. s ''x'' = b  s ''y'' = a"
  by (rule R_assignl, auto) 

lemma var_swap_ref2: 
  "rel_R λs. s ''z'' = a  s ''y'' = b λs. s ''x'' = b  s ''y'' = a 
    (''x'' ::= (λs. s ''y'')); rel_R λs. s ''z'' = a  s ''x'' = b λs. s ''x'' = b  s ''y'' = a"
  by (rule R_assignl, auto)

lemma var_swap_ref3:  
  "rel_R λs. s ''z'' = a  s ''x'' = b λs. s ''x'' = b  s ''y'' = a 
    (''y'' ::= (λs. s ''z'')); rel_R λs. s ''x'' = b  s ''y'' = a λs. s ''x'' = b  s ''y'' = a" 
  by (rule R_assignl, auto)

lemma var_swap_ref_var: 
  "rel_R λs. s ''x'' = a  s ''y'' = b λs. s ''x'' = b  s ''y'' = a 
    (''z'' ::= (λs. s ''x'')); (''x'' ::= (λs. s ''y'')); (''y'' ::= (λs. s ''z''))"
  using var_swap_ref1 var_swap_ref2 var_swap_ref3 rel_rkat.R_skip  by fastforce

end

Theory VC_KAD_scratch

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

subsection‹Component Based on Kleene Algebra with Domain›

text ‹This component supports the verification and step-wise refinement of simple while programs
in a partial correctness setting.›

theory VC_KAD_scratch
  imports Main
begin

subsubsection ‹KAD: Definitions and Basic Properties›

notation times (infixl "" 70)

class plus_ord = plus + ord +
  assumes less_eq_def: "x  y  x + y = y"
  and less_def: "x < y  x  y  x  y"

class dioid = semiring + one + zero + plus_ord +
  assumes add_idem [simp]: "x + x = x"
  and mult_onel [simp]: "1  x = x"
  and mult_oner [simp]: "x  1 = x"
  and add_zerol [simp]: "0 + x = x"
  and annil [simp]: "0  x = 0"
  and annir [simp]: "x  0 = 0"

begin

subclass monoid_mult
  by (standard, simp_all)

subclass order
  by (standard, simp_all add: less_def less_eq_def add_commute, auto, metis add_assoc)

lemma mult_isor: "x  y  x  z  y  z"   
  by (metis distrib_right less_eq_def)

lemma mult_isol: "x  y  z  x  z  y"   
  by (metis distrib_left less_eq_def)   

lemma add_iso: "x  y  z + x  z + y"
  by (metis add.semigroup_axioms add_idem less_eq_def semigroup.assoc)

lemma add_ub: "x  x + y"
  by (metis add_assoc add_idem less_eq_def)

lemma add_lub: "x + y  z  x  z  y  z"
  by (metis add_assoc add_ub add.left_commute less_eq_def)

end

class kleene_algebra  = dioid +
  fixes star :: "'a  'a" ("_" [101] 100)
  assumes star_unfoldl: "1 + x  x  x"  
  and star_unfoldr: "1 + x  x  x"
  and star_inductl: "z + x  y  y  x  z  y"
  and star_inductr: "z + y  x  y  z  x  y"

begin

lemma star_sim: "x  y  z  x  x  y  z  x"
proof - 
  assume "x  y  z  x"
  hence "x + z  x  y  x + z  z  x"
    by (metis add_lub distrib_left eq_refl less_eq_def mult_assoc)
  also have  "...  z  x"
    using add_lub mult_isor star_unfoldr by fastforce
  finally show ?thesis
    by (simp add: star_inductr) 
qed

end

class antidomain_kleene_algebra = kleene_algebra + 
  fixes ad :: "'a  'a" ("ad")
  assumes as1 [simp]: "ad x  x = 0"
  and as2 [simp]: "ad (x  y) + ad (x  ad (ad y)) = ad (x  ad (ad y))"
  and as3 [simp]: "ad (ad x) + ad x = 1"

begin

definition dom_op :: "'a  'a" ("d") where
  "d x = ad (ad x)"

lemma a_subid_aux: "ad x  y  y"
  by (metis add_commute add_ub as3 mult_1_left mult_isor)

lemma d1_a [simp]: "d x  x = x"
  by (metis add_commute dom_op_def add_zerol as1 as3 distrib_right mult_1_left)

lemma a_mul_d [simp]: "ad x  d x = 0"
  by (metis add_commute dom_op_def add_zerol as1 as2 distrib_right mult_1_left)

lemma a_d_closed [simp]: "d (ad x) = ad x"
  by (metis d1_a dom_op_def add_zerol as1 as3 distrib_left mult_1_right)

lemma a_idem [simp]: "ad x  ad x = ad x"
  by (metis a_d_closed d1_a)

lemma meet_ord: "ad x  ad y  ad x  ad y = ad x"
  by (metis a_d_closed a_subid_aux d1_a order.antisym mult_1_right mult_isol)

lemma d_wloc: "x  y = 0  x  d y = 0"
  by (metis a_subid_aux d1_a dom_op_def add_ub order.antisym as1 as2 mult_1_right mult_assoc)

lemma gla_1: "ad x  y = 0  ad x  ad y"
  by (metis a_subid_aux d_wloc dom_op_def add_zerol as3 distrib_left mult_1_right)

lemma a2_eq [simp]: "ad (x  d y) = ad (x  y)"
  by (metis a_mul_d d1_a dom_op_def gla_1 add_ub order.antisym as1 as2 mult_assoc)

lemma a_supdist: "ad (x + y)  ad x"
  by (metis add_commute gla_1 add_ub add_zerol as1 distrib_left less_eq_def)

lemma a_antitone: "x  y  ad y  ad x"
  by (metis a_supdist less_eq_def)

lemma a_comm: "ad x  ad y = ad y  ad x"
proof -
{ fix x y
  have "ad x  ad y = d (ad x  ad y)  ad x  ad y"
    by (simp add: mult_assoc)
  also have "...  d (ad y)  ad x"
    by (metis a_antitone a_d_closed a_subid_aux mult_oner a_subid_aux dom_op_def mult_isol mult_isor meet_ord)   
  finally have "ad x  ad y  ad y  ad x"
    by simp }
  thus ?thesis
    by (simp add: order.antisym)
qed

lemma a_closed [simp]: "d (ad x  ad y) = ad x  ad y"
proof -
  have f1: "x y. ad x  ad (ad y  x)"
    by (simp add: a_antitone a_subid_aux)
  have "x y. d (ad x  y)  ad x"
    by (metis a2_eq a_antitone a_comm a_d_closed dom_op_def f1)
  hence "x y. d (ad x  y)  y = ad x  y"
    by (metis d1_a dom_op_def meet_ord mult_assoc)
  thus ?thesis
    by (metis a_comm a_idem dom_op_def)
qed

lemma a_exp [simp]: "ad (ad x  y) = d x + ad y"
proof (rule order.antisym)
  have "ad (ad x  y)  ad x  d y = 0"
    using d_wloc mult_assoc by fastforce
  hence a: "ad (ad x  y)  d y  d x"
    by (metis a_closed a_comm dom_op_def gla_1 mult_assoc)
  have "ad (ad x  y) = ad (ad x  y)  d y + ad (ad x  y)  ad y"
    by (metis dom_op_def as3 distrib_left mult_oner)
  also have "...  d x +  ad (ad x  y)  ad y"
    using a add_lub dual_order.trans by blast
  finally show "ad (ad x  y)  d x + ad y"
    by (metis a_antitone a_comm a_subid_aux meet_ord)
next
  have "ad y  ad (ad x  y)"
    by (simp add: a_antitone a_subid_aux)
  thus "d x + ad y  ad (ad x  y)"
    by (metis a2_eq a_antitone a_comm a_subid_aux dom_op_def add_lub)
qed  

lemma d1_sum_var: "x + y  (d x + d y)  (x + y)"
proof -
  have "x + y = d x  x + d y  y"
    by simp
  also have "...  (d x + d y)  x + (d x + d y)  y"
    by (metis add_commute add_lub add_ub combine_common_factor)
  finally show ?thesis
    by (simp add: distrib_left)
qed

lemma a4: "ad (x + y) = ad x  ad y"
proof (rule order.antisym)
  show "ad (x + y)  ad x  ad y"
    by (metis a_supdist add_commute mult_isor meet_ord)
  hence "ad x  ad y = ad x  ad y + ad (x + y)"
    using less_eq_def add_commute by simp
  also have "... = ad (ad (ad x  ad y)  (x + y))"
    by (metis a_closed a_exp)
  finally show "ad x  ad y  ad (x + y)"
    using a_antitone d1_sum_var dom_op_def by auto
qed

lemma kat_prop: "d x  y  y  d z  d x  y  ad z = 0"
proof
  show  "d x  y  y  d z  d x  y  ad z = 0"
    by (metis add_commute dom_op_def add_zerol annir as1 less_eq_def mult_isor mult_assoc)
next 
  assume h: "d x  y  ad z = 0"
  hence "d x  y = d x  y  d z + d x  y  ad z"
    by (metis dom_op_def as3 distrib_left mult_1_right)
  thus  "d x  y  y  d z"
    by (metis a_subid_aux add_commute dom_op_def h add_zerol mult_assoc)
qed

lemma shunt: "ad x  ad y + ad z  ad x  d y  ad z" 
proof 
  assume "ad x  ad y + ad z"
  hence "ad x  d y  ad y  d y + ad z  d y"
    by (metis distrib_right mult_isor)
  thus " ad x  d y  ad z"
    by (metis a_closed a_d_closed a_exp a_mul_d a_supdist dom_op_def dual_order.trans less_eq_def)
next 
  assume h: "ad x  d y  ad z"
  have "ad x = ad x  ad y + ad x  d y"
    by (metis add_commute dom_op_def as3 distrib_left mult_1_right)
  also have "...  ad x  ad y + ad z"
    using h add_lub dual_order.trans by blast
  also have "...  ad y + ad z"
    by (metis a_subid_aux add_commute add_lub add_ub dual_order.trans)
  finally show "ad x  ad y + ad z" 
    by simp
qed

subsubsection ‹wp Calculus›

definition if_then_else :: "'a  'a  'a  'a" ("if _ then _ else _ fi" [64,64,64] 63) where
  "if p then x else y fi = d p  x + ad p  y"

definition while :: "'a  'a  'a" ("while _ do _ od" [64,64] 63) where
  "while p do x od = (d p  x)  ad p"

definition while_inv :: "'a  'a  'a  'a" ("while _ inv _ do _ od" [64,64,64] 63) where
  "while p inv i do x od = while p do x od"

definition wp :: "'a  'a  'a" where
  "wp x p = ad (x  ad p)"

lemma demod: " d p  wp x q  d p  x  x  d q"
  by (metis as1 dom_op_def gla_1 kat_prop meet_ord mult_assoc wp_def)

lemma wp_weaken: "wp x p  wp (x  ad q) (d p  ad q)"
  by (metis a4 a_antitone a_d_closed a_mul_d dom_op_def gla_1 mult_isol mult_assoc wp_def)

lemma wp_seq [simp]: "wp (x  y) q = wp x (wp y q)"
  using a2_eq dom_op_def mult_assoc wp_def by auto

lemma wp_seq_var: "p  wp x r  r  wp y q  p  wp (x  y) q"
proof -
  assume a1: "p  wp x r"
  assume a2: "r  wp y q"
  have "z. ¬ wp x r  z  p  z"
    using a1 dual_order.trans by blast
  then show ?thesis
    using a2 a_antitone mult_isol wp_def wp_seq by auto
qed

lemma wp_cond_var [simp]: "wp (if p then x else y fi) q = (ad p + wp x q)  (d p + wp y q)"
  using a4 a_d_closed dom_op_def if_then_else_def distrib_right mult_assoc wp_def by auto

lemma wp_cond_aux1 [simp]: "d p  wp (if p then x else y fi) q = d p  wp x q"
proof -
  have "d p  wp (if p then x else y fi) q = ad (ad p)  (ad p + wp x q)  (d p + wp y q)"
    using dom_op_def mult.semigroup_axioms semigroup.assoc wp_cond_var by fastforce
  also have "... = wp x q  d p  (d p + d (wp y q))"
    using a_comm a_d_closed dom_op_def distrib_left wp_def by auto 
  also have "... = wp x q  d p"
    by (metis a_exp dom_op_def add_ub meet_ord mult_assoc)
  finally show ?thesis
    by (simp add: a_comm dom_op_def wp_def)
qed

lemma wp_cond_aux2 [simp]: "ad p  wp (if p then x else y fi) q = ad p  wp y q"
  by (metis (no_types) abel_semigroup.commute if_then_else_def a_d_closed add.abel_semigroup_axioms dom_op_def wp_cond_aux1)

lemma wp_cond [simp]: "wp (if p then x else y fi) q = (d p  wp x q) + (ad p  wp y q)"
  by (metis as3 distrib_right dom_op_def mult_1_left wp_cond_aux2 wp_cond_aux1)

lemma wp_star_induct_var: "d q  wp x q  d q  wp (x) q" 
  using demod star_sim by blast

lemma wp_while: "d p  d r  wp x p  d p  wp (while r do x od) (d p  ad r)"
proof -
  assume "d p  d r  wp x p"
  hence "d p  wp (d r  x) p"
    using dom_op_def mult.semigroup_axioms semigroup.assoc shunt wp_def by fastforce
  hence "d p  wp ((d r  x)) p"
    using wp_star_induct_var by blast
  thus ?thesis
    by (simp add: while_def) (use local.dual_order.trans wp_weaken in fastforce)
qed

lemma wp_while_inv: "d p  d i  d i  ad r  d q  d i  d r  wp x i  d p  wp (while r inv i do x od) q"
proof -
  assume a1: "d p  d i" and a2: "d i  ad r  d q" and "d i  d r  wp x i"
  hence "d i  wp (while r inv i do x od) (d i  ad r)"
    by (simp add: while_inv_def wp_while)
  also have "...   wp (while r inv i do x od) q"
    by (metis a2 a_antitone a_d_closed dom_op_def mult_isol wp_def)
  finally show ?thesis
    using a1 dual_order.trans by blast
qed

lemma wp_while_inv_break: "d p  wp y i  d i  ad r  d q  d i  d r  wp x i  d p  wp (y  (while r inv i do x od)) q"
  by (metis dom_op_def eq_refl mult_1_left mult_1_right wp_def wp_seq wp_seq_var wp_while_inv)

end

subsubsection ‹Soundness and Relation KAD›

notation relcomp (infixl ";" 70)

interpretation rel_d: dioid Id "{}" "(∪)" "(;)" "(⊆)" "(⊂)"
  by (standard, auto)

lemma (in dioid) pow_inductl: "z + x  y  y  x ^ i  z  y"
  apply (induct i; clarsimp simp add: add_lub)
  by (metis local.dual_order.trans local.mult_isol mult_assoc)

lemma (in dioid) pow_inductr: "z + y  x  y  z  x ^ i  y"
  apply (induct i; clarsimp simp add: add_lub)
  proof -
    fix i
    assume "z  x ^ i  y" "z  y" "y  x  y"
    hence "(z  x ^ i)  x  y"
      using local.dual_order.trans local.mult_isor by blast
    thus "z  (x  x ^ i)  y"
      by (simp add: mult_assoc local.power_commutes)
  qed

lemma power_is_relpow: "rel_d.power X i = X ^^ i"
  by (induct i, simp_all add: relpow_commute)

lemma rel_star_def: "X^* = (i. rel_d.power X i)"
  by (simp add: power_is_relpow rtrancl_is_UN_relpow)

lemma rel_star_contl: "X ; Y^* = (i. X ; rel_d.power Y i)"
  by (simp add: rel_star_def relcomp_UNION_distrib)

lemma rel_star_contr: "X^* ; Y = (i. (rel_d.power X i) ; Y)"
  by (simp add: rel_star_def relcomp_UNION_distrib2)

definition rel_ad :: "'a rel  'a rel" where
  "rel_ad R = {(x,x) | x. ¬ (y. (x,y)  R)}" 

interpretation rel_aka: antidomain_kleene_algebra Id "{}" "(∪)"  "(;)" "(⊆)" "(⊂)" rtrancl rel_ad
  apply standard
  apply auto[2]
  by (auto simp: rel_star_contr rel_d.pow_inductl rel_star_contl SUP_least rel_d.pow_inductr rel_ad_def)

subsubsection ‹Embedding Predicates in Relations›

type_synonym 'a pred = "'a  bool"

abbreviation p2r :: "'a pred  'a rel" ("_") where
  "P  {(s,s) |s. P s}"

lemma d_p2r [simp]: "rel_aka.dom_op P = P"
  by (auto simp: rel_aka.dom_op_def rel_ad_def)

lemma p2r_neg_hom [simp]: "rel_ad P = λs. ¬P s" 
  by (auto simp: rel_ad_def)

lemma p2r_conj_hom [simp]: "P  Q = λs. P s  Q s"
  by auto

lemma p2r_conj_hom_var [simp]: "P ; Q = λs. P s  Q s" 
  by auto

lemma p2r_disj_hom [simp]: "P  Q = λs. P s  Q s"
  by auto

subsubsection ‹Store and Assignment›

type_synonym 'a store = "string   'a"

definition gets :: "string  ('a store  'a)  'a store rel" ("_ ::= _" [70, 65] 61) where 
  "v ::= e = {(s,s (v := e s)) |s. True}"

lemma wp_assign [simp]: "rel_aka.wp (v ::= e) Q = λs. Q (s (v := e s))"
  by (auto simp: rel_aka.wp_def gets_def rel_ad_def)

abbreviation spec_sugar :: "'a pred  'a rel  'a pred  bool" ("PRE _ _ POST _" [64,64,64] 63) where
  "PRE P X POST Q  rel_aka.dom_op P  rel_aka.wp X Q"

abbreviation if_then_else_sugar :: "'a pred  'a rel  'a rel  'a rel" ("IF _ THEN _ ELSE _ FI" [64,64,64] 63) where
  "IF P THEN X ELSE Y FI  rel_aka.if_then_else P X Y"

abbreviation while_inv_sugar :: "'a pred  'a pred  'a rel  'a rel" ("WHILE _ INV _ DO _ OD" [64,64,64] 63) where
  "WHILE P INV I DO X OD  rel_aka.while_inv P I X"

subsubsection ‹Verification Example›

lemma euclid:
  "PRE (λs::nat store. s ''x'' = x  s ''y'' = y)
   (WHILE (λs. s ''y''  0) INV (λs. gcd (s ''x'') (s ''y'') = gcd x y) 
    DO
     (''z'' ::= (λs. s ''y''));
     (''y'' ::= (λs. s ''x'' mod s ''y''));
     (''x'' ::= (λs. s ''z''))
    OD)
   POST (λs. s ''x'' = gcd x y)"
  apply (rule rel_aka.wp_while_inv, simp_all) using gcd_red_nat by auto

context antidomain_kleene_algebra
begin

subsubsection‹Propositional Hoare Logic›

definition H :: "'a  'a  'a  bool" where
  "H p x q  d p  wp x q"

lemma H_skip: "H p 1 p"
  by (simp add: H_def dom_op_def wp_def)

lemma H_cons: "d p  d p'  d q'  d q  H p' x q'  H p x q"
  by (meson H_def demod mult_isol order_trans)

lemma H_seq: "H p x r  H r y q  H p (x  y) q"
  by (metis H_def a_d_closed demod dom_op_def wp_seq_var)

lemma H_cond: "H (d p  d r) x q  H (d p  ad r) y q  H p (if r then x else y fi) q"
proof -
  assume  h1: "H (d p  d r) x q" and h2: "H (d p  ad r) y q"
  hence h3: "d p  d r  wp x q" and h4: "d p  ad r  wp y q"
    using H_def a_closed dom_op_def apply auto[1]
    using H_def h2 a_closed dom_op_def by auto
  hence h5: "d p   ad r + wp x q" and h6: "d p   d r + wp y q"
    apply (simp add: dom_op_def shunt wp_def)
    using h4 a_d_closed dom_op_def shunt wp_def by auto
  hence "d p  d p   (d r + wp y q)"
    by (metis a_idem distrib_left dom_op_def less_eq_def)
  also have  "...  (ad r + wp x q)  (d r + wp y q)"
    by (simp add: h5 mult_isor)
  finally show ?thesis
    by (simp add: H_def)
qed

lemma H_loop: "H (d p  d r) x p  H p (while r do x od) (d p  ad r)"
  by (metis (full_types) H_def a_closed dom_op_def wp_while)

lemma H_while_inv: "d p  d i  d i  ad r  d q  H (d i  d r) x i  H p (while r inv i do x od) q"
  using H_def a_closed dom_op_def wp_while_inv by auto

end

subsubsection‹Definition of Refinement KAD›

class rkad = antidomain_kleene_algebra +
  fixes R :: "'a  'a  'a"
  assumes R_def: "x  R p q  d p  wp x q"

begin

subsubsection ‹Propositional Refinement Calculus›

lemma HR: "H p x q  x  R p q"
  by (simp add: H_def R_def)

lemma wp_R1: "d p  wp (R p q) q"
  using R_def by blast

lemma wp_R2: "x  R (wp x q) q"
  by (simp add: R_def wp_def)

lemma wp_R3: "d p  wp x q  x  R p q"
  by (simp add: R_def)

lemma H_R1: "H p (R p q) q"
  by (simp add: HR)

lemma H_R2: "H p x q  x  R p q"
  by (simp add: HR)

lemma R_skip: "1  R p p"
  by (simp add: H_R2 H_skip)

lemma R_cons: "d p  d p'  d q'  d q  R p' q'  R p q"
  by (simp add: H_R1 H_R2 H_cons)

lemma R_seq: "(R p r)  (R r q)  R p q"
  using H_R1 H_R2 H_seq by blast

lemma R_cond: "if v then (R (d v  d p) q) else (R (ad v  d p) q) fi  R p q"
  by (simp add: H_R1 H_R2 H_cond a_comm dom_op_def)

lemma R_loop: "while q do (R (d p  d q) p) od  R p (d p  ad q)"
  by (simp add: H_R1 H_R2 H_loop)

end

subsubsection ‹Soundness and Relation RKAD›

definition rel_R :: "'a rel  'a rel  'a rel" where 
  "rel_R P Q = {X. rel_aka.dom_op P  rel_aka.wp X Q}"

interpretation rel_rkad: rkad Id "{}" "(∪)"  "(;)" "(⊆)" "(⊂)" rtrancl rel_ad rel_R
  by (standard, auto simp: rel_R_def rel_aka.dom_op_def rel_ad_def rel_aka.wp_def, blast)

subsubsection ‹Assignment Laws›

lemma R_assign: "(s. P s  Q (s (v := e s)))  (v ::= e)  rel_R P Q"
  by (auto simp: rel_rkad.R_def)

lemma H_assign_var: "(s. P s  Q (s (v := e s)))  rel_aka.H P (v ::= e) Q"
  by (auto simp: rel_aka.H_def rel_aka.dom_op_def rel_ad_def gets_def rel_aka.wp_def)

lemma R_assignr: "(s. Q' s  Q (s (v := e s)))  (rel_R P Q') ; (v ::= e)  rel_R P Q"
  apply (subst rel_rkad.HR[symmetric], rule rel_aka.H_seq) defer 
  by (erule H_assign_var, simp add: rel_rkad.H_R1)

lemma R_assignl: "(s. P s  P' (s (v := e s)))  (v ::= e) ; (rel_R P' Q)  rel_R P Q"
  by (subst rel_rkad.HR[symmetric], rule rel_aka.H_seq, erule H_assign_var, simp add: rel_rkad.H_R1)

subsubsection ‹Refinement Example›

lemma var_swap_ref1: 
  "rel_R λs. s ''x'' = a  s ''y'' = b λs. s ''x'' = b  s ''y'' = a 
    (''z'' ::= (λs. s ''x'')); rel_R λs. s ''z'' = a  s ''y'' = b λs. s ''x'' = b  s ''y'' = a"
  by (rule R_assignl, auto) 

lemma var_swap_ref2: 
  "rel_R λs. s ''z'' = a  s ''y'' = b λs. s ''x'' = b  s ''y'' = a 
    (''x'' ::= (λs. s ''y'')); rel_R λs. s ''z'' = a  s ''x'' = b λs. s ''x'' = b  s ''y'' = a"
  by (rule R_assignl, auto)

lemma var_swap_ref3:  
  "rel_R λs. s ''z'' = a  s ''x'' = b λs. s ''x'' = b  s ''y'' = a 
    (''y'' ::= (λs. s ''z'')); rel_R λs. s ''x'' = b  s ''y'' = a λs. s ''x'' = b  s ''y'' = a" 
  by (rule R_assignl, auto)

lemma var_swap_ref_var: 
  "rel_R λs. s ''x'' = a  s ''y'' = b λs. s ''x'' = b  s ''y'' = a 
    (''z'' ::= (λs. s ''x'')); (''x'' ::= (λs. s ''y'')); (''y'' ::= (λs. s ''z''))"
  using var_swap_ref1 var_swap_ref2 var_swap_ref3 rel_rkad.R_skip  by fastforce

end

Theory P2S2R

(* Title: Isomorphisms Betweeen Predicates, Sets and Relations *}
   Author: Victor Gomes, Georg Struth
   Maintainer: Victor Gomes <victor.gomes@cl.cam.ac.uk>
               Georg Struth <g.struth@sheffield.ac.uk> 
*)

section ‹Isomorphisms Between Predicates, Sets and Relations›

theory P2S2R
imports Main

begin    

notation relcomp (infixl ";" 70)
notation inf (infixl "" 70)  
notation sup (infixl "" 65)
notation Id_on ("s2r")
notation Domain ("r2s")
notation Collect ("p2s")

definition rel_n :: "'a rel  'a rel" where 
  "rel_n   (λX. Id  - X)"  

lemma subid_meet: "R  Id  S  Id  R  S = R ; S"
  by blast

subsection‹Isomorphism Between Sets and Relations›

lemma srs: "r2s  s2r = id"
  by auto

lemma rsr: "R  Id  s2r (r2s R) = R"
  by (auto simp: Id_def Id_on_def Domain_def) 

lemma s2r_inj: "inj s2r"
  by (metis Domain_Id_on injI)

lemma r2s_inj: "R  Id  S  Id  r2s R = r2s S  R = S"
  by (metis rsr)

lemma s2r_surj: "R  Id. A. R = s2r A"
  using rsr by auto
 
lemma r2s_surj: "A. R  Id. A = r2s R"
  by (metis Domain_Id_on Id_onE pair_in_Id_conv subsetI)

lemma s2r_union_hom: "s2r (A  B) = s2r A  s2r B"
  by (simp add: Id_on_def)

lemma s2r_inter_hom: "s2r (A  B) = s2r A  s2r B"
  by (auto simp: Id_on_def)  

lemma s2r_inter_hom_var: "s2r (A  B) = s2r A ; s2r B"
  by (auto simp: Id_on_def)

lemma s2r_compl_hom: "s2r (- A) = rel_n (s2r A)"
  by (auto simp add: rel_n_def)

lemma r2s_union_hom: "r2s (R  S) = r2s R  r2s S"
  by auto

lemma r2s_inter_hom: "R  Id  S  Id  r2s (R  S) = r2s R  r2s S"
  by auto

lemma r2s_inter_hom_var: "R  Id  S  Id  r2s (R ; S) = r2s R  r2s S"
  by (metis r2s_inter_hom subid_meet)

lemma r2s_ad_hom: "R  Id  r2s (rel_n R) = - r2s R"
  by (metis r2s_surj rsr s2r_compl_hom)

subsection ‹Isomorphism Between Predicates and Sets›

type_synonym 'a pred = "'a  bool"

definition s2p :: "'a set  'a pred" where
  "s2p S = (λx. x  S)"

lemma sps [simp]: "s2p  p2s = id" 
  by (intro ext, simp add: s2p_def)

lemma psp [simp]: "p2s  s2p = id"
  by (intro ext, simp add: s2p_def)

lemma s2p_bij: "bij s2p"
  using o_bij psp sps by blast

lemma p2s_bij: "bij p2s"
  using o_bij psp sps by blast

lemma s2p_compl_hom: "s2p (- A) = - (s2p A)"
  by (metis Collect_mem_eq comp_eq_dest_lhs id_apply sps uminus_set_def)
 
lemma s2p_inter_hom: "s2p (A  B) = (s2p A)  (s2p B)"
  by (metis Collect_mem_eq comp_eq_dest_lhs id_apply inf_set_def sps)

lemma s2p_union_hom: "s2p (A  B) = (s2p A)  (s2p B)"
  by (auto simp: s2p_def)

lemma p2s_neg_hom: "p2s (- P) = - (p2s P)"
  by fastforce

lemma p2s_conj_hom: "p2s (P  Q) = p2s P  p2s Q"
  by blast

lemma p2s_disj_hom: "p2s (P  Q) = p2s P  p2s Q"
  by blast

subsection ‹Isomorphism Between Predicates and Relations›

definition p2r :: "'a pred  'a rel" where
  "p2r P = {(s,s) |s. P s}"

definition r2p :: "'a rel  'a pred" where
  "r2p R = (λx. x  Domain R)"

lemma p2r_subid: "p2r P  Id"
  by (simp add: p2r_def subset_eq)

lemma p2s2r: "p2r = s2r  p2s"
proof (intro ext)
  fix P :: "'a pred"
  have "{(a, a) |a. P a} = {(b, a). b = a  P b}"
    by blast
  thus "p2r P = (s2r  p2s) P"
    by (simp add: Id_on_def' p2r_def)
qed

lemma r2s2p: "r2p = s2p  r2s"
  by (intro ext, simp add: r2p_def s2p_def)

lemma prp [simp]: "r2p  p2r = id"
  by (intro ext, simp add: p2s2r r2p_def)

lemma rpr: "R  Id  p2r (r2p R) = R"
  by (metis comp_apply id_apply p2s2r psp r2s2p rsr)

lemma p2r_inj: "inj p2r"
  by (metis comp_eq_dest_lhs id_apply injI prp)

lemma r2p_inj: "R  Id  S  Id  r2p R = r2p S  R = S"
  by (metis rpr)

lemma p2r_surj: " R  Id. P. R = p2r P"
  using rpr by auto

lemma r2p_surj: "P. R  Id. P = r2p R"
  by (metis comp_apply id_apply p2r_subid prp)

lemma p2r_neg_hom: "p2r (- P) = rel_n (p2r P)"
  by (simp add: p2s2r p2s_neg_hom s2r_compl_hom)

lemma p2r_conj_hom [simp]: "p2r P  p2r Q = p2r (P  Q)"
  by (simp add: p2s2r p2s_conj_hom s2r_inter_hom)

lemma p2r_conj_hom_var [simp]: "p2r P ; p2r Q = p2r (P  Q)"
  by (simp add: p2s2r p2s_conj_hom s2r_inter_hom_var)

lemma p2r_id_neg [simp]: "Id  - p2r p = p2r (-p)"
  by (auto simp: p2r_def)

lemma [simp]: "p2r bot = {}"
  by (auto simp: p2r_def)

lemma p2r_disj_hom [simp]: "p2r P  p2r Q = p2r (P  Q)"
  by (simp add: p2s2r p2s_disj_hom s2r_union_hom)

lemma r2p_ad_hom: "R  Id  r2p (rel_n R) = - (r2p R)"
  by (simp add: r2s2p r2s_ad_hom s2p_compl_hom)

lemma r2p_inter_hom: "R  Id  S  Id  r2p (R  S) = (r2p R)  (r2p S)"
  by (simp add: r2s2p r2s_inter_hom s2p_inter_hom)

lemma r2p_inter_hom_var: "R  Id  S  Id  r2p (R ; S) = (r2p R)  (r2p S)"
  by (simp add: r2s2p r2s_inter_hom_var s2p_inter_hom)

lemma rel_to_pred_union_hom: "R  Id  S  Id  r2p (R  S) = (r2p R)  (r2p S)"
  by (simp add: Domain_Un_eq r2s2p s2p_union_hom)

end

Theory VC_KAT

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

section ‹Components Based on Kleene Algebra with Tests›

subsection ‹Verification Component›      

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

theory VC_KAT
imports "../P2S2R"
        KAT_and_DRA.PHL_KAT 
        KAT_and_DRA.KAT_Models

begin

text‹This first part changes some of the facts from the AFP KAT theories. It should be added to KAT in the next AFP version. 
Currently these facts provide an interface between the KAT theories and the verification component.›

no_notation if_then_else ("if _ then _ else _ fi" [64,64,64] 63)
no_notation while ("while _ do _ od" [64,64] 63)
no_notation Archimedean_Field.ceiling ("_")

notation relcomp (infixl ";" 70)               
notation p2r ("_")

context kat 
begin

subsubsection ‹Definitions of Hoare Triple›

definition H :: "'a  'a  'a  bool" where
  "H p x q  t p  x  x  t q" 

lemma H_var1: "H p x q  t p  x  n q = 0"
  by (metis H_def n_kat_3 t_n_closed)

lemma H_var2: "H p x q  t p  x = t p  x  t q"
  by (simp add: H_def n_kat_2)

subsubsection ‹Syntax for Conditionals and Loops›

definition ifthenelse :: "'a  'a  'a  'a" ("if _ then _ else _ fi" [64,64,64] 63) where
  "if p then x else y fi = (t p  x + n p  y)"

definition while :: "'a  'a  'a" ("while _ do _ od" [64,64] 63) where
  "while b do x od = (t b  x)  n b"

definition while_inv :: "'a  'a  'a  'a" ("while _ inv _ do _ od" [64,64,64] 63) where
  "while p inv i do x od = while p do x od"

subsubsection ‹Propositional Hoare Logic›

lemma H_skip:  "H p 1 p"
  by (simp add: H_def)

lemma H_cons_1: "t p  t p'  H p' x q  H p x q"
  using H_def phl_cons1 by blast

lemma H_cons_2: "t q'  t q  H p x q'  H p x q"
  using H_def phl_cons2 by blast          

lemma H_cons: "t p  t p'  t q'  t q  H p' x q'  H p x q"
  by (simp add: H_cons_1 H_cons_2)

lemma H_seq_swap: "H p x r  H r y q  H p (x  y) q"
  by (simp add: H_def phl_seq)

lemma H_seq: "H r y q  H p x r  H p (x  y) q"
  by (simp add: H_seq_swap)

lemma H_exp1: "H (t p  t r) x q  H p (t r  x) q"
  using H_def n_de_morgan_var2 phl.ht_at_phl_export1 by auto

lemma H_exp2: "H p x q  H p (x  t r) (t q  t r)"
  by (metis H_def phl.ht_at_phl_export2 test_mult)

lemma H_cond_iff: "H p (if r then x else y fi) q  H (t p  t r) x q  H (t p  n r) y q"
proof -
  have "H p (if r then x else y fi) q  t p  (t r  x + n r  y)  n q = 0"
    by (simp add: H_var1 ifthenelse_def)
  also have "...  t p  t r  x  n q + t p  n r  y  n q = 0"
    by (simp add: distrib_left mult_assoc)
  also have "...  t p  t r  x  n q = 0  t p  n r  y  n q = 0"
    by (metis add_0_left no_trivial_inverse)
  finally show ?thesis
    by (metis H_var1 test_mult)
qed

lemma H_cond: "H (t p  t r) x q  H (t p  n r) y q  H p (if r then x else y fi) q"
  by (simp add: H_cond_iff)

lemma H_loop: "H (t p  t r) x p  H p (while r do x od) (t p  n r)"
proof -
  assume a1: "H (t p  t r) x p"
  have "t (t p  n r) = n r  t p  n r"
    using n_preserve test_mult by presburger
  then show ?thesis
    using a1 H_def H_exp1 conway.phl.it_simr phl_export2 while_def by auto
qed

lemma H_while_inv: "t p  t i  t i  n r  t q  H (t i  t r) x i  H p (while r inv i do x od) q"
  by (metis H_cons H_loop test_mult while_inv_def)

text ‹Finally we prove a frame rule.›

lemma H_frame: "H p x p  H q x r  H (t p  t q) x (t p  t r)"
proof -
  assume "H p x p" and a: "H q x r"
  hence b: "t p  x  x  t p" and "t q  x  x  t r"
    using H_def apply blast using H_def a by blast
  hence "t p  t q  x  t p  x  t r"
    by (simp add: mult_assoc mult_isol)
  also have "...  x  t p  t r"
    by (simp add: b mult_isor)
  finally show ?thesis
    by (metis H_def mult_assoc test_mult)
qed
    
end

subsubsection ‹Store and Assignment›

text ‹The proper verification component starts here.›

type_synonym 'a store = "string   'a"

lemma t_p2r [simp]: "rel_dioid_tests.t P = P"
  by (auto simp: p2r_def)

lemma impl_prop [simp]: "P  Q  (s. P s   Q s)"
  by (auto simp: p2r_def)

lemma Id_simp [simp]: "Id  (- Id  X) = Id  X" 
  by auto

lemma Id_p2r [simp]: "Id  P = P"
  by (auto simp: Id_def p2r_def)

lemma Id_p2r_simp [simp]: "Id  (- Id  P) = P"
  by simp 

text ‹Next we derive the assignment command and assignment rules.›

definition gets :: "string  ('a store  'a)  'a store rel" ("_ ::= _" [70, 65] 61) where 
  "v ::= e = {(s,s (v := e s)) |s. True}"

lemma H_assign_prop: "λs. P (s (v := e s)) ; (v ::= e) = (v ::= e) ; P"
  by (auto simp: p2r_def gets_def)

lemma H_assign: "rel_kat.H λs. P (s (v := e s)) (v ::= e) P"
  by (auto simp add: rel_kat.H_def gets_def p2r_def)

lemma H_assign_var: "(s. P s  Q (s (v := e s)))  rel_kat.H P (v ::= e) Q"
  by (auto simp: p2r_def gets_def rel_kat.H_def)

lemma H_assign_iff [simp]: "rel_kat.H P (v ::= e) Q  (s. P s  Q (s (v := e s)))"
  by (auto simp: p2r_def gets_def rel_kat.H_def)

lemma H_assign_floyd: " rel_kat.H P (v ::= e) λs. w. s v = e (s(v := w))  P (s(v := w))"
  by (rule H_assign_var, metis fun_upd_same fun_upd_triv fun_upd_upd)

subsubsection ‹Simplified Hoare Rules›

lemma sH_cons_1: "s. P s  P' s  rel_kat.H P' X Q  rel_kat.H P X Q"
  by (rule rel_kat.H_cons_1, auto simp only: p2r_def)

lemma sH_cons_2: "s. Q' s  Q s  rel_kat.H P X Q'  rel_kat.H P X Q"
  by (rule rel_kat.H_cons_2, auto simp only: p2r_def)

lemma sH_cons: "s. P s  P' s  s. Q' s  Q s  rel_kat.H P' X Q'  rel_kat.H P X Q"
  by (simp add: sH_cons_1 sH_cons_2)
  
lemma sH_cond: "rel_kat.H P  T X Q  rel_kat.H P  - T Y Q   rel_kat.H P (rel_kat.ifthenelse T X Y) Q"
  by (rule rel_kat.H_cond, auto simp add: rel_kat.H_def p2r_def, blast+)

lemma sH_cond_iff: "rel_kat.H P (rel_kat.ifthenelse T X Y) Q  (rel_kat.H P  T X Q  rel_kat.H P  - T Y Q)"
  by (simp add: rel_kat.H_cond_iff)

lemma sH_while_inv: "s. P s  I s  s. I s  ¬ R s  Q s  rel_kat.H I  R X I 
                      rel_kat.H P (rel_kat.while_inv R I X) Q"
  by (rule rel_kat.H_while_inv, auto simp: p2r_def rel_kat.H_def, fastforce)

lemma sH_H: "rel_kat.H P X Q  (s s'. P s  (s,s')  X  Q s')"
  by (simp add: rel_kat.H_def, auto simp add: p2r_def)

text ‹Finally we provide additional syntax for specifications and commands.›
 
abbreviation H_sugar :: "'a pred  'a rel  'a pred  bool" ("PRE _ _ POST _" [64,64,64] 63) where
  "PRE P X POST Q  rel_kat.H P X Q"

abbreviation if_then_else_sugar :: "'a pred  'a rel  'a rel  'a rel" ("IF _ THEN _ ELSE _ FI" [64,64,64] 63) where
  "IF P THEN X ELSE Y FI  rel_kat.ifthenelse P X Y"

abbreviation while_sugar :: "'a pred  'a rel  'a rel" ("WHILE _ DO _ OD" [64,64] 63) where
  "WHILE P  DO X OD  rel_kat.while P X"

abbreviation while_inv_sugar :: "'a pred  'a pred  'a rel  'a rel" ("WHILE _ INV _ DO _ OD" [64,64,64] 63) where
  "WHILE P INV I DO X OD  rel_kat.while_inv P I X"

lemma H_cond_iff2[simp]: "PRE p (IF r THEN x ELSE y FI) POST q  (PRE (p  r) x POST q)  (PRE (p  - r) y POST q)"
  by (simp add: rel_kat.H_cond_iff)

end

Theory VC_KAT_Examples

(* Title: Verification Component Based on KAT: Examples
   Author: Victor Gomes, Georg Struth
   Maintainer: Victor Gomes <victor.gomes@cl.cam.ac.uk>
               Georg Struth <g.struth@sheffield.ac.uk> 
*)

subsubsection ‹Verification Examples›

theory VC_KAT_Examples
  imports VC_KAT
begin

lemma euclid:
  "PRE (λs::nat store. s ''x'' = x  s ''y'' = y)
   (WHILE (λs. s ''y''  0) INV (λs. gcd (s ''x'') (s ''y'') = gcd x y) 
    DO
     (''z'' ::= (λs. s ''y''));
     (''y'' ::= (λs. s ''x'' mod s ''y''));
     (''x'' ::= (λs. s ''z''))
    OD)
   POST (λs. s ''x'' = gcd x y)"
  apply (rule sH_while_inv)
  apply simp_all
  apply force
  apply (intro rel_kat.H_seq)
  apply (subst H_assign, simp)+
  apply (intro H_assign_var)
  using gcd_red_nat by auto

lemma maximum: 
  "PRE (λs:: nat store. True)
   (IF (λs. s ''x''  s ''y'') 
    THEN (''z'' ::= (λs. s ''x''))
    ELSE (''z'' ::= (λs. s ''y''))
    FI)
   POST (λs. s ''z'' = max (s ''x'') (s ''y''))"
  by auto

lemma integer_division: 
  "PRE (λs::nat store. s ''x''  0)
    (''q'' ::= (λs. 0)); 
    (''r'' ::= (λs. s ''x''));
    (WHILE (λs. s ''y''  s ''r'') INV (λs. s ''x'' = s ''q'' * s ''y'' + s ''r''  s ''r''  0)
     DO
      (''q'' ::= (λs. s ''q'' + 1));
      (''r'' ::= (λs. s ''r'' - s ''y''))
      OD)
   POST (λs. s ''x'' = s ''q'' * s ''y'' + s ''r''  s ''r''  0  s ''r'' < s ''y'')"
  apply (intro rel_kat.H_seq, subst sH_while_inv, simp_all)
  apply auto[1]
  apply (intro rel_kat.H_seq)
  by (subst H_assign, simp_all)+

lemma imp_reverse:
  "PRE (λs:: 'a list store. s ''x'' = X)
   (''y'' ::= (λs. []));
   (WHILE (λs. s ''x''  []) INV (λs. rev (s ''x'') @ s ''y'' = rev X)
    DO 
     (''y'' ::= (λs. hd (s ''x'') # s ''y'')); 
     (''x'' ::= (λs. tl (s ''x'')))
    OD) 
   POST (λs. s ''y''= rev X )"
  apply (intro rel_kat.H_seq, rule sH_while_inv)
  apply auto[2]
  apply (rule rel_kat.H_seq, rule H_assign_var)
  apply auto[1]
  apply (rule H_assign_var)
  apply (clarsimp, metis append.simps(1) append.simps(2) append_assoc hd_Cons_tl rev.simps(2))
  by simp

end

Theory VC_KAT_Examples2

(* Title: Verification Component Based on KAT: Examples with Automated VCG
   Author: Victor Gomes, Georg Struth
   Maintainer: Victor Gomes <victor.gomes@cl.cam.ac.uk>
               Georg Struth <g.struth@sheffield.ac.uk> 
*)

subsubsection ‹Verification Examples with Automated VCG›

theory VC_KAT_Examples2
  imports VC_KAT "HOL-Eisbach.Eisbach"
begin

text ‹The following simple tactic for verification condition generation has been 
implemented with the Eisbach proof methods language.›

named_theorems hl_intro

declare sH_while_inv [hl_intro]
  rel_kat.H_seq [hl_intro]
  H_assign_var [hl_intro]
  rel_kat.H_cond [hl_intro]

method hoare = (rule hl_intro; hoare?)

lemma euclid:
  "PRE (λs::nat store. s ''x'' = x  s ''y'' = y)
   (WHILE (λs. s ''y''  0) INV (λs. gcd (s ''x'') (s ''y'') = gcd x y) 
    DO
     (''z'' ::= (λs. s ''y''));
     (''y'' ::= (λs. s ''x'' mod s ''y''));
     (''x'' ::= (λs. s ''z''))
    OD)
   POST (λs. s ''x'' = gcd x y)"
   apply hoare
   using gcd_red_nat by auto

lemma integer_division: 
  "PRE (λs::nat store. s ''x''  0)
    (''q'' ::= (λs. 0)); 
    (''r'' ::= (λs. s ''x''));
    (WHILE (λs. s ''y''  s ''r'') INV (λs. s ''x'' = s ''q'' * s ''y'' + s ''r''  s ''r''  0)
     DO
      (''q'' ::= (λs. s ''q'' + 1));
      (''r'' ::= (λs. s ''r'' - s ''y''))
      OD)
   POST (λs. s ''x'' = s ''q'' * s ''y'' + s ''r''  s ''r''  0  s ''r'' < s ''y'')"
   by hoare auto

lemma imp_reverse:
  "PRE (λs:: 'a list store. s ''x'' = X)
   (''y'' ::= (λs. []));
   (WHILE (λs. s ''x''  []) INV (λs. rev (s ''x'') @ s ''y'' = rev X)
    DO 
     (''y'' ::= (λs. hd (s ''x'') # s ''y'')); 
     (''x'' ::= (λs. tl (s ''x'')))
    OD) 
   POST (λs. s ''y''= rev X )"
   apply hoare 
   apply auto[3]
   apply (clarsimp, metis (no_types, lifting) Cons_eq_appendI append_eq_append_conv2 hd_Cons_tl rev.simps(2) self_append_conv)
   by simp

end

Theory RKAT

(* Title: Refinement KAT
   Author: Victor Gomes, Georg Struth
   Maintainer: Victor Gomes <victor.gomes@cl.cam.ac.uk>
               Georg Struth <g.struth@sheffield.ac.uk> 
*)

subsection ‹Refinement Component›

theory RKAT
  imports "AVC_KAT/VC_KAT"

begin

subsubsection‹RKAT: Definition and Basic Properties›

text ‹A refinement KAT is a KAT expanded by Morgan's specification statement.›

class rkat = kat +
  fixes R :: "'a  'a  'a"
  assumes spec_def:  "x  R p q  H p x q"

begin

lemma R1: "H p (R p q) q"
  using spec_def by blast

lemma R2: "H p x q  x  R p q"
  by (simp add: spec_def)

subsubsection‹Propositional Refinement Calculus›

lemma R_skip: "1  R p p"
proof -
  have "H p 1 p"
    by (simp add: H_skip)
  thus ?thesis
    by (rule R2)
qed

lemma R_cons: "t p  t p'  t q'  t q  R p' q'  R p q"
proof -
  assume h1: "t p  t p'" and h2: "t q'  t q"
  have "H p' (R p' q') q'"
    by (simp add: R1)
  hence "H p (R p' q') q"
    using h1 h2 H_cons_1 H_cons_2 by blast
  thus ?thesis
    by (rule R2)
qed

lemma R_seq: "(R p r)  (R r q)  R p q"
proof -
  have "H p (R p r) r" and "H r (R r q) q"
    by (simp add: R1)+
  hence "H p ((R p r)  (R r q)) q"
    by (rule H_seq_swap)
  thus ?thesis
    by (rule R2)
qed

lemma R_cond: "if v then (R (t v  t p) q) else (R (n v  t p) q) fi  R p q"
proof - 
  have "H (t v  t p) (R (t v  t p) q) q" and "H (n v  t p) (R (n v  t p) q) q"
    by (simp add: R1)+
  hence "H p (if v then (R (t v  t p) q) else (R (n v  t p) q) fi) q"
    by (simp add: H_cond n_mult_comm)
 thus ?thesis
    by (rule R2)
qed

lemma R_loop: "while q do (R (t p  t q) p) od  R p (t p  n q)"
proof -
  have "H (t p  t q) (R (t p  t q) p)  p" 
    by (simp_all add: R1)
  hence "H p (while q do (R (t p  t q) p) od) (t p  n q)"
    by (simp add: H_loop)
  thus ?thesis
    by (rule R2)
  qed

lemma R_zero_one: "x  R 0 1"
proof -
  have "H 0 x 1"
    by (simp add: H_def)
  thus ?thesis
    by (rule R2)
qed

lemma R_one_zero: "R 1 0 = 0"
proof -
  have "H 1 (R 1 0) 0"
    by (simp add: R1)
  thus ?thesis
    by (simp add: H_def join.le_bot)
qed

end

end

Theory RKAT_Models

(* Title: Models of Refinement KAT
   Author: Victor Gomes, Georg Struth
   Maintainer: Victor Gomes <victor.gomes@cl.cam.ac.uk>
               Georg Struth <g.struth@sheffield.ac.uk> 
*)

subsubsection ‹Models of Refinement KAT›

theory RKAT_Models
  imports RKAT
   
begin

text ‹So far only the relational model is developed.›

definition rel_R :: "'a rel  'a rel  'a rel" where 
  "rel_R P Q = {X. rel_kat.H P X Q}"

interpretation rel_rkat: rkat "(∪)" "(;)" Id "{}" "(⊆)" "(⊂)" rtrancl "(λX. Id  - X)" rel_R
  by (standard, auto simp: rel_R_def rel_kat.H_def)

end



Theory VC_RKAT

(* Title: Refinement Component Based on KAT
   Author: Victor Gomes, Georg Struth
   Maintainer: Victor Gomes <victor.gomes@cl.cam.ac.uk>
               Georg Struth <g.struth@sheffield.ac.uk> 
*)

theory VC_RKAT
  imports "../RKAT_Models"

begin

text ‹This component supports the step-wise refinement of simple while programs
in a partial correctness setting.›

subsubsection ‹Assignment Laws›

text ‹The store model is taken from KAT›

lemma R_assign: "(s. P s  Q (s (v := e s)))  (v ::= e)  rel_R P Q"
proof - 
  assume "(s. P s  Q (s (v := e s)))"
  hence "rel_kat.H P (v ::= e) Q"
    by (rule H_assign_var)
  thus ?thesis
    by (rule rel_rkat.R2)
qed

lemma R_assignr: "(s. Q' s  Q (s (v := e s)))  (rel_R P Q') ; (v ::= e)  rel_R P Q"  
  by (metis H_assign_var rel_kat.H_seq rel_rkat.R1 rel_rkat.R2)   

lemma R_assignl: "(s. P s  P' (s (v := e s)))  (v ::= e) ; (rel_R P' Q)  rel_R P Q"
  by (metis H_assign_var rel_kat.H_seq rel_rkat.R1 rel_rkat.R2)

subsubsection ‹Simplified Refinement Laws›

lemma R_cons: "(s. P s  P' s)  (s. Q' s  Q s)  rel_R P' Q'  rel_R P Q"
  by (simp add: rel_rkat.R1 rel_rkat.R2 sH_cons_1 sH_cons_2)

lemma if_then_else_ref: "X  X'  Y  Y'  IF P THEN X ELSE Y FI  IF P THEN X' ELSE Y' FI"
  by (auto simp: rel_kat.ifthenelse_def)
                                     
lemma while_ref: "X  X'  WHILE P DO X OD  WHILE P DO X' OD"
  by (simp add: rel_kat.while_def rel_dioid.mult_isol rel_dioid.mult_isor rel_kleene_algebra.star_iso)
                                                               
end


Theory VC_RKAT_Examples

(* Title: Refinement Component Based on KAT: Examples
   Author: Victor Gomes, Georg Struth
   Maintainer: Victor Gomes <victor.gomes@cl.cam.ac.uk>
               Georg Struth <g.struth@sheffield.ac.uk> 
*)

subsubsection ‹Refinement Examples›

theory VC_RKAT_Examples 
  imports VC_RKAT
begin

text ‹Currently  there is only one example, and no tactic for automating refinement proofs is provided.›

lemma var_swap_ref1: 
  "rel_R λs. s ''x'' = a  s ''y'' = b λs. s ''x'' = b  s ''y'' = a
    (''z'' ::= (λs. s ''x'')); rel_R λs. s ''z'' = a  s ''y'' = b λs. s ''x'' = b  s ''y'' = a"
  by (rule R_assignl, auto) 

lemma var_swap_ref2: 
  "rel_R λs. s ''z'' = a  s ''y'' = b λs. s ''x'' = b  s ''y'' = a 
    (''x'' ::= (λs. s ''y'')); rel_R λs. s ''z'' = a  s ''x'' = b λs. s ''x'' = b  s ''y'' = a"
  by (rule R_assignl, auto)

lemma var_swap_ref3:  
  "rel_R λs. s ''z'' = a  s ''x'' = b λs. s ''x'' = b  s ''y'' = a
    (''y'' ::= (λs. s ''z'')); rel_R λs. s ''x'' = b  s ''y'' = a λs. s ''x'' = b  s ''y'' = a" 
  by (rule R_assignl, auto)

lemma var_swap_ref_var: 
  "rel_R λs. s ''x'' = a  s ''y'' = b λs. s ''x'' = b  s ''y'' = a
    (''z'' ::= (λs. s ''x'')); (''x'' ::= (λs. s ''y'')); (''y'' ::= (λs. s ''z''))"
  using var_swap_ref1 var_swap_ref2 var_swap_ref3 rel_rkat.R_skip by fastforce

end


Theory VC_KAD

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

section ‹Components Based on Kleene Algebra with Domain›

theory VC_KAD

imports KAD.Modal_Kleene_Algebra_Models "../P2S2R"      

begin

subsection‹Verification Component for Backward Reasoning›

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

no_notation Archimedean_Field.ceiling ("_")
no_notation Archimedean_Field.floor ("_")

notation p2r ("_")
notation r2p ("_")

context antidomain_kleene_algebra
begin

subsubsection ‹Additional Facts for KAD›

lemma fbox_shunt: "d p  d q  |x] t  d p  ad q + |x] t"
  by (metis a_6 a_antitone' a_loc add_commute addual.ars_r_def am_d_def da_shunt2 fbox_def)

subsubsection ‹Syntax for Conditionals and Loops›

definition cond :: "'a  'a  'a  'a" ("if _ then _ else _ fi" [64,64,64] 63) where
  "if p then x else y fi = d p  x + ad p  y"

definition while :: "'a  'a  'a" ("while _ do _ od" [64,64] 63) where
  "while p do x od = (d p  x)  ad p"

definition whilei :: "'a  'a  'a  'a" ("while _ inv _ do _ od" [64,64,64] 63) where
  "while p inv i do x od = while p do x od"

subsubsection ‹Basic Weakest (Liberal) Precondition Calculus›

text ‹In the setting of Kleene algebra with domain, the wlp operator is the forward modal box operator 
of antidomain Kleene algebra.›

lemma fbox_export1: "ad p + |x] q = |d p  x] q"
  using a_d_add_closure addual.ars_r_def fbox_def fbox_mult by auto

lemma fbox_export2: "|x] p  |x  ad q] (d p  ad q)"
proof -
  {fix t
   have "d t  x  x  d p  d t  x  ad q  x  ad q  d p  ad q"
     by (metis (full_types) a_comm_var a_mult_idem ads_d_def am2 ds.ddual.mult_assoc phl_export2)
   hence "d t  |x] p  d t  |x  ad q] (d p  ad q)"
     by (metis a_closure' addual.ars_r_def ans_d_def dka.dsg3 ds.ddual.mult_assoc fbox_def fbox_demodalisation3)
  }
  thus ?thesis
    by (metis a_closure' addual.ars_r_def ans_d_def fbox_def order_refl)
qed

lemma fbox_export3: "|x  ad p] q = |x] (d p + d q)"
  using a_de_morgan_var_3 ds.ddual.mult_assoc fbox_def by auto

lemma fbox_seq [simp]: "|x  y] q = |x] |y] q"
  by (simp add: fbox_mult) 

lemma fbox_seq_var: "p'  |y] q  p  |x] p'  p  |x  y] q"
proof -
  assume h1: "p  |x] p'" and h2: "p'  |y] q"
  hence "|x] p'  |x] |y] q"
    by (simp add: dka.dom_iso fbox_iso)
  thus ?thesis
    by (metis h1 dual_order.trans fbox_seq)
qed

lemma fbox_cond_var [simp]: "|if p then x else y fi] q = (ad p + |x] q)  (d p + |y] q)"  
  using cond_def a_closure' ads_d_def ans_d_def fbox_add2 fbox_export1 by auto

lemma fbox_cond_aux1 [simp]: "d p  |if p then x else y fi] q = d p  |x] q"
proof -
  have "d p  |if p then x else y fi] q = d p  |x] q  (d p + d ( |y] q))"
    using a_d_add_closure addual.ars_r_def ds.ddual.mult_assoc fbox_def fbox_cond_var by auto
  thus ?thesis
    by (metis addual.ars_r_def am2 dka.dns5 ds.ddual.mult_assoc fbox_def)
qed

lemma fbox_cond_aux2 [simp]: "ad p  |if p then x else y fi] q = ad p  |y] q"
  by (metis cond_def a_closure' add_commute addual.ars_r_def ans_d_def fbox_cond_aux1)

lemma fbox_cond [simp]: "|if p then x else y fi] q = (d p  |x] q) + (ad p  |y] q)"
proof -
  have "|if p then x else y fi] q = (d p + ad p)  |if p then x else y fi] q"
    by (simp add: addual.ars_r_def)
  thus ?thesis
    by (metis  distrib_right' fbox_cond_aux1 fbox_cond_aux2)
qed

lemma fbox_cond_var2 [simp]: "|if p then x else y fi] q = if p then |x] q else |y] q fi"
  using cond_def fbox_cond by auto

lemma fbox_while_unfold: "|while t do x od] p = (d t + d p)  (ad t + |x] |while t do x od] p)"
  by (metis fbox_export1 fbox_export3 dka.dom_add_closed fbox_star_unfold_var while_def)

lemma fbox_while_var1: "d t  |while t do x od] p = d t  |x] |while t do x od] p"
  by (metis fbox_while_unfold a_mult_add ads_d_def dka.dns5 ds.ddual.mult_assoc join.sup_commute)

lemma fbox_while_var2: "ad t  |while t do x od] p  d p"
proof - 
  have "ad t  |while t do x od] p = ad t  (d t + d p)  (ad t + |x] |while t do x od] p)"
    by (metis fbox_while_unfold ds.ddual.mult_assoc)
  also have "... =  ad t  d p  (ad t + |x] |while t do x od] p)"
    by (metis a_de_morgan_var_3 addual.ars_r_def dka.dom_add_closed s4)
  also have "...  d p  (ad t + |x] |while t do x od] p)"
    using a_subid_aux1' mult_isor by blast
  finally show ?thesis
    by (metis a_de_morgan_var_3 a_mult_idem addual.ars_r_def ans4 dka.dsr5 dpdz.domain_1'' dual_order.trans fbox_def)
qed

lemma fbox_while: "d p  d t  |x] p  d p  |while t do x od] (d p  ad t)"
proof -
  assume "d p  d t  |x] p"
  hence "d p  |d t  x] p"
    by (simp add: fbox_export1 fbox_shunt)
  hence "d p  |(d t  x)] p"
    by (simp add: fbox_star_induct_var)
  thus ?thesis
    using order_trans while_def fbox_export2 by presburger
qed

lemma fbox_while_var: "d p = |d t  x] p  d p  |while t do x od] (d p  ad t)"
  by (metis eq_refl fbox_export1 fbox_shunt fbox_while)
 
lemma fbox_whilei: "d p  d i  d i  ad t  d q  d i  d t  |x] i  d p  |while t inv i do x od] q"
proof -
  assume a1: "d p  d i" and a2: "d i  ad t  d q" and "d i  d t  |x] i"
  hence "d i  |while t inv i do x od] (d i  ad t)"
    by (simp add: fbox_while whilei_def)
  also have "...  |while t inv i do x od] q"
    using a2 dka.dom_iso fbox_iso by fastforce
  finally show ?thesis
    using a1 dual_order.trans by blast
qed

text ‹The next rule is used for dealing with while loops after a series of sequential steps.›

lemma fbox_whilei_break: "d p  |y] i  d i  ad t  d q  d i  d t  |x] i  d p  |y  (while t inv i do x od)] q"
  apply (rule fbox_seq_var, rule fbox_whilei, simp_all, blast)
  using fbox_simp by auto

text ‹Finally we derive a frame rule.›

lemma fbox_frame: "d p  x  x  d p  d q  |x] t  d p  d q  |x] (d p  d t)"    
  using dual.mult_isol_var fbox_add1 fbox_demodalisation3 fbox_simp by auto

lemma fbox_frame_var: "d p  |x] p  d q  |x] t  d p  d q  |x] (d p  d t)"
  using fbox_frame fbox_demodalisation3 fbox_simp by auto   

end

subsubsection ‹Store and Assignment›

type_synonym 'a store = "string   'a"

notation rel_antidomain_kleene_algebra.fbox ("wp")
and rel_antidomain_kleene_algebra.fdia ("relfdia")

definition gets :: "string  ('a store  'a)  'a store rel" ("_ ::= _" [70, 65] 61) where 
   "v ::= e = {(s,s (v := e s)) |s. True}"

lemma assign_prop: "λs. P (s (v := e s)) ; (v ::= e) = (v ::= e) ; P"
  by (auto simp add: p2r_def gets_def)
                                                                                 
lemma wp_assign [simp]: "wp (v ::= e) Q = λs. Q (s (v := e s))"
  by (auto simp: rel_antidomain_kleene_algebra.fbox_def gets_def rel_ad_def p2r_def)

lemma wp_assign_var [simp]: "wp (v ::= e) Q = (λs. Q (s (v := e s)))"
  by (simp, auto simp: r2p_def p2r_def)

lemma wp_assign_det: "wp (v ::= e) Q = relfdia (v ::= e) Q"
  by (auto simp add: rel_antidomain_kleene_algebra.fbox_def rel_antidomain_kleene_algebra.fdia_def gets_def p2r_def rel_ad_def, fast)
 
subsubsection ‹Simplifications›

notation rel_antidomain_kleene_algebra.ads_d ("rdom")

abbreviation spec_sugar :: "'a pred  'a rel  'a pred  bool" ("PRE _ _ POST _" [64,64,64] 63) where
  "PRE P X POST Q  rdom P  wp X Q"

abbreviation cond_sugar :: "'a pred  'a rel  'a rel  'a rel" ("IF _ THEN _ ELSE _ FI" [64,64,64] 63) where
  "IF P THEN X ELSE Y FI  rel_antidomain_kleene_algebra.cond P X Y"

abbreviation whilei_sugar :: "'a pred  'a pred  'a rel  'a rel" ("WHILE _ INV _ DO _ OD" [64,64,64] 63) where
  "WHILE P INV I DO X OD  rel_antidomain_kleene_algebra.whilei P I X"

lemma d_p2r [simp]: "rdom P = P"
  by (simp add: p2r_def rel_antidomain_kleene_algebra.ads_d_def rel_ad_def)

lemma p2r_conj_hom_var_symm [simp]: "P ; Q = P  Q"
  by (simp add: p2r_conj_hom_var)

lemma p2r_neg_hom [simp]: "rel_ad P = - P"
  by (simp add: rel_ad_def p2r_def)

lemma wp_trafo: "wp X Q = (λs. s'. (s,s')  X  Q s')"  
  by (auto simp: rel_antidomain_kleene_algebra.fbox_def rel_ad_def p2r_def r2p_def)

lemma wp_trafo_var: "wp X Q s = (s'. (s,s')  X  Q s')"
  by (simp add: wp_trafo)

lemma wp_simp: "rdom wp X Q = wp X Q"
  by (metis d_p2r rel_antidomain_kleene_algebra.a_subid' rel_antidomain_kleene_algebra.addual.bbox_def rpr)

lemma wp_simp_var [simp]: "wp P Q = - P  Q"
  by (simp add: rel_antidomain_kleene_algebra.fbox_def)

lemma impl_prop [simp]: "P  Q  (s. P s   Q s)"
  by (auto simp: p2r_def)

lemma p2r_eq_prop [simp]: "P = Q  (s. P s   Q s)"
  by (auto simp: p2r_def)

lemma impl_prop_var [simp]: "rdom P  rdom Q  (s. P s   Q s)"
  by simp     

lemma p2r_eq_prop_var [simp]: "rdom P = rdom Q  (s. P s   Q s)"
  by simp                                                     
 
lemma wp_whilei: "(s. P s  I s)  (s. (I  -T) s  Q s)  (s. (I  T) s  wp X I s) 
                   (s. P s  wp (WHILE T INV I DO X OD) Q s)"
  apply (simp only: impl_prop_var[symmetric] wp_simp)
  by (rule rel_antidomain_kleene_algebra.fbox_whilei, simp_all, simp_all add: p2r_def)

end

Theory VC_KAD_Examples

(* Title: Verification Component Based on KAD: Examples
   Author: Victor Gomes, Georg Struth
   Maintainer: Victor Gomes <victor.gomes@cl.cam.ac.uk>
               Georg Struth <g.struth@sheffield.ac.uk> 
*)

subsubsection‹Verification Examples›

theory VC_KAD_Examples
imports VC_KAD

begin

lemma euclid:
  "PRE (λs::nat store. s ''x'' = x  s ''y'' = y)
   (WHILE (λs. s ''y''  0) INV (λs. gcd (s ''x'') (s ''y'') = gcd x y) 
    DO
     (''z'' ::= (λs. s ''y''));
     (''y'' ::= (λs. s ''x'' mod s ''y''));
     (''x'' ::= (λs. s ''z''))
    OD)
   POST (λs. s ''x'' = gcd x y)"
  by (rule rel_antidomain_kleene_algebra.fbox_whilei, auto simp: gcd_non_0_nat)

lemma euclid_diff: 
   "PRE (λs::nat store. s ''x'' = x  s ''y'' = y  x > 0  y > 0)
    (WHILE (λs. s ''x'' s ''y'') INV (λs. gcd (s ''x'') (s ''y'') = gcd x y) 
     DO
        (IF (λs. s ''x'' >  s ''y'')
         THEN (''x'' ::= (λs. s ''x'' - s ''y''))
         ELSE (''y'' ::= (λs. s ''y'' - s ''x''))
         FI)
    OD)
    POST (λs. s ''x'' = gcd x y)"
  apply (rule rel_antidomain_kleene_algebra.fbox_whilei, simp_all)
  apply auto[1]
  by (metis gcd.commute gcd_diff1_nat le_cases nat_less_le)

lemma varible_swap:
  "PRE (λs. s ''x'' = a  s ''y'' = b)   
    (''z'' ::= (λs. s ''x''));
    (''x'' ::= (λs. s ''y''));
    (''y'' ::= (λs. s ''z''))
   POST (λs. s ''x'' = b  s ''y'' = a)"
  by simp

lemma maximum: 
  "PRE (λs:: nat store. True) 
   (IF (λs. s ''x''  s ''y'') 
    THEN (''z'' ::= (λs. s ''x''))
    ELSE (''z'' ::= (λs. s ''y''))
    FI)
   POST (λs. s ''z'' = max (s ''x'') (s ''y''))"
  by auto

lemma integer_division: 
  "PRE (λs::nat store. x  0)
    (''q'' ::= (λs. 0)); 
    (''r'' ::= (λs. x));
    (WHILE (λs. y  s ''r'') INV (λs. x = s ''q'' * y + s ''r''  s ''r''  0)
     DO
      (''q'' ::= (λs. s ''q'' + 1));
      (''r'' ::= (λs. s ''r'' - y))
      OD)
   POST (λs. x = s ''q'' * y + s ''r''  s ''r''  0  s ''r'' < y)"
  by (rule rel_antidomain_kleene_algebra.fbox_whilei_break, simp_all)

lemma factorial:
  "PRE (λs::nat store. True)
   (''x'' ::= (λs. 0));
   (''y'' ::= (λs. 1));
   (WHILE (λs. s ''x''  x0) INV (λs. s ''y'' = fact (s ''x''))
   DO
     (''x'' ::= (λs. s ''x'' + 1));
     (''y'' ::= (λs. s ''y''  s ''x''))
   OD)
   POST (λs. s ''y'' = fact x0)"
  by (rule rel_antidomain_kleene_algebra.fbox_whilei_break, simp_all)
 
lemma my_power:
  "PRE (λs::nat store. True)
   (''i'' ::= (λs. 0));
   (''y'' ::= (λs. 1));
   (WHILE (λs. s ''i'' < n) INV (λs. s ''y'' = x ^ (s ''i'')  s ''i''  n)
     DO
       (''y'' ::= (λs. (s ''y'') * x));
       (''i'' ::= (λs. s ''i'' + 1))
     OD)
   POST (λs. s ''y'' = x ^ n)"
  by (rule rel_antidomain_kleene_algebra.fbox_whilei_break, auto)

lemma imp_reverse:
  "PRE (λs:: 'a list store. s ''x'' = X)
   (''y'' ::= (λs. []));
   (WHILE (λs. s ''x''  []) INV (λs. rev (s ''x'') @ s ''y'' = rev X)
    DO 
     (''y'' ::= (λs. hd (s ''x'') # s ''y'')); 
     (''x'' ::= (λs. tl (s ''x'')))
    OD) 
   POST (λs. s ''y''= rev X )"
  apply (rule rel_antidomain_kleene_algebra.fbox_whilei_break, simp_all)
  apply auto[1]
  by (safe, metis append.simps append_assoc hd_Cons_tl rev.simps(2))

end

Theory VC_KAD_Examples2

(* Title: Verification Component Based on KAD: Examples with Automated VCG
   Author: Victor Gomes, Georg Struth
   Maintainer: Victor Gomes <victor.gomes@cl.cam.ac.uk>
               Georg Struth <g.struth@sheffield.ac.uk> 
*)

subsubsection‹Verification Examples with Automated VCG›

theory VC_KAD_Examples2
imports VC_KAD "HOL-Eisbach.Eisbach"
begin

text ‹We have provide a simple tactic in the Eisbach proof method language. Additional simplification
steps are sometimes needed to bring the resulting verification conditions into shape for first-order automated
theorem proving.›


named_theorems ht

declare rel_antidomain_kleene_algebra.fbox_whilei [ht]
  rel_antidomain_kleene_algebra.fbox_seq_var [ht]
  subset_refl[ht]

method hoare = (rule ht; hoare?)

lemma euclid2:
  "PRE (λs::nat store. s ''x'' = x  s ''y'' = y)
   (WHILE (λs. s ''y''  0) INV (λs. gcd (s ''x'') (s ''y'') = gcd x y) 
    DO
     (''z'' ::= (λs. s ''y''));
     (''y'' ::= (λs. s ''x'' mod s ''y''));
     (''x'' ::= (λs. s ''z''))
    OD)
   POST (λs. s ''x'' = gcd x y)"
  apply hoare
  using gcd_red_nat by auto

lemma euclid_diff2: 
   "PRE (λs::nat store. s ''x'' = x  s ''y'' = y  x > 0  y > 0)
    (WHILE (λs. s ''x'' s ''y'') INV (λs. gcd (s ''x'') (s ''y'') = gcd x y) 
     DO
        (IF (λs. s ''x'' >  s ''y'')
         THEN (''x'' ::= (λs. s ''x'' - s ''y''))
         ELSE (''y'' ::= (λs. s ''y'' - s ''x''))
         FI)
    OD)
    POST (λs. s ''x'' = gcd x y)"
  apply (hoare, simp_all) 
  apply auto[1]
  by (metis gcd.commute gcd_diff1_nat le_cases nat_less_le)

lemma integer_division2: 
  "PRE (λs::nat store. x  0)
    (''q'' ::= (λs. 0)); 
    (''r'' ::= (λs. x));
    (WHILE (λs. y  s ''r'') INV (λs. x = s ''q'' * y + s ''r''  s ''r''  0)
     DO
      (''q'' ::= (λs. s ''q'' + 1));
      (''r'' ::= (λs. s ''r'' - y))
      OD)
   POST (λs. x = s ''q'' * y + s ''r''  s ''r''  0  s ''r'' < y)"
   by hoare simp_all

lemma factorial2:
  "PRE (λs::nat store. True)
   (''x'' ::= (λs. 0));
   (''y'' ::= (λs. 1));
   (WHILE (λs. s ''x''  x0) INV (λs. s ''y'' = fact (s ''x''))
   DO
     (''x'' ::= (λs. s ''x'' + 1));
     (''y'' ::= (λs. s ''y''  s ''x''))
   OD)
   POST (λs. s ''y'' = fact x0)"
  by hoare simp_all

lemma my_power2:
  "PRE (λs::nat store. True)
   (''i'' ::= (λs. 0));
   (''y'' ::= (λs. 1));
   (WHILE (λs. s ''i'' < n) INV (λs. s ''y'' = x ^ (s ''i'')  s ''i''  n)
     DO
       (''y'' ::= (λs. (s ''y'') * x));
       (''i'' ::= (λs. s ''i'' + 1))
     OD)
   POST (λs. s ''y'' = x ^ n)"
  by hoare auto

lemma imp_reverse2:
  "PRE (λs:: 'a list store. s ''x'' = X)
   (''y'' ::= (λs. []));
   (WHILE (λs. s ''x''  []) INV (λs. rev (s ''x'') @ s ''y'' = rev X)
    DO 
     (''y'' ::= (λs. hd (s ''x'') # s ''y'')); 
     (''x'' ::= (λs. tl (s ''x'')))
    OD) 
   POST (λs. s ''y''= rev X )"
  apply (hoare, simp_all)
  apply auto[1]
  by (clarsimp, metis append.simps append_assoc hd_Cons_tl rev.simps(2))

end

Theory VC_KAD_dual

(* Title: Verification Component Based on KAD for Forward Reasoning
   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 Forward Reasoning›

theory VC_KAD_dual
  imports VC_KAD
begin

context modal_kleene_algebra
begin

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

subsubsection ‹Basic Strongest Postcondition Calculus›

text ‹In modal Kleene algebra, strongest postconditions are backward diamond operators. These
are linked with forward boxes aka weakest preconditions by a Galois connection.  This duality has been
implemented in the AFP entry for Kleene algebra with domain and is picked up automatically in
the following proofs.›

lemma r_ad [simp]: "r (ad p) = ad p"
  using a_closure addual.ars_r_def am_d_def domrangefix by auto

lemma bdia_export1: "x| (r p  r t) = r t  x| p"
  by (metis ardual.ads_d_def ardual.ds.ddual.rsr2 ardual.ds.fdia_mult bdia_def)

lemma bdia_export2: "r p  x| q = x  r p| q"
  using ardual.ads_d_def ardual.am2 ardual.fdia_export_2 bdia_def by auto

lemma bdia_seq [simp]: "x  y| q = y| x| q"
  by (simp add: ardual.ds.fdia_mult)

lemma bdia_seq_var: "x| p  p'  y| p'  q  x  y| p  q"
  by (metis ardual.ds.fd_subdist_1 ardual.ds.fdia_mult dual_order.trans join.sup_absorb2)

lemma bdia_cond_var [simp]: "if p then x else y fi| q = x| (d p  r q) + y| (ad p  r q)"
  by (metis (no_types, lifting) bdia_export1 a4' a_de_morgan a_de_morgan_var_3 a_subid_aux1' ardual.ds.fdia_add2 dka.dnso1 dka.dsg4 domrange dpdz.dnso1 cond_def join.sup.absorb_iff1 rangedom)

lemma bdia_while: "x| (d t  r p)  r p   while t do x od| p  r p  ad t"
proof -
  assume "x| (d t  r p)  r p"
  hence "d t  x| p  r p"
    by (metis bdia_export1 dka.dsg4 domrange rangedom)
  hence "(d t  x)| p  r p"
    by (meson ardual.fdemodalisation22 ardual.kat_2_equiv_opp star_sim1)
  hence "r (ad t)  (d t  x)| p  r p  ad t"
    by (metis ardual.dpdz.dsg4 ars_r_def mult_isol r_ad)
  thus ?thesis
    by (metis bdia_export2 while_def r_ad)
qed

lemma bdia_whilei: "r p  r i  r i  ad t  r q  x| (d t  r i)  r i  while t inv i do x od| p  r q"
proof -
  assume a1: "r p  r i" and a2: "r i  ad t  r q" and "x| (d t  r i)  r i"
  hence "while t inv i do x od| i  r i  ad t"
    by (simp add: bdia_while whilei_def)
  hence "while t inv i do x od| i  r q"
    using a2 dual_order.trans by blast
  hence "r i  |while t inv i do x od] r q"
    using ars_r_def box_diamond_galois_1 domrange by fastforce
  hence "r p  |while t inv i do x od] r q"
    using a1 dual_order.trans by blast
  thus ?thesis
    using ars_r_def box_diamond_galois_1 domrange by fastforce
qed

lemma bdia_whilei_break: "y| p  r i  r i  ad t  r q  x| (d t  r i)  r i  y  (while t inv i do x od)| p  r q"
  using bdia_whilei ardual.ads_d_def ardual.ds.fdia_mult bdia_def by auto
 
end

subsubsection ‹Floyd's Assignment Rule›

lemma bdia_assign [simp]: "rel_antirange_kleene_algebra.bdia (v ::= e) P = λs. w. s v = e (s(v := w))  P (s(v:=w))"
  apply (simp add: rel_antirange_kleene_algebra.bdia_def gets_def p2r_def rel_ar_def)
  apply safe
  by (metis fun_upd_apply fun_upd_triv fun_upd_upd, fastforce)

lemma d_p2r [simp]: "rel_antirange_kleene_algebra.ars_r  P = P"
  by (simp add: p2r_def rel_antirange_kleene_algebra.ars_r_def rel_ar_def)

abbreviation fspec_sugar :: "'a pred  'a rel  'a pred  bool" ("FPRE _ _ POST _" [64,64,64] 63) where
  "FPRE P X POST Q  rel_antirange_kleene_algebra.bdia X P  rel_antirange_kleene_algebra.ars_r Q"

end

Theory VC_KAD_dual_Examples

(* Title: Verification Component Based on KAD for Forward Reasoning: Examples
   Author: Victor Gomes, Georg Struth
   Maintainer: Victor Gomes <victor.gomes@cl.cam.ac.uk>
               Georg Struth <g.struth@sheffield.ac.uk> 
*)

subsubsection‹Verification Examples›

theory VC_KAD_dual_Examples
imports VC_KAD_dual

begin

text‹The proofs are essentially the same as with forward boxes.›

lemma euclid:
  "FPRE (λs::nat store. s ''x'' = x  s ''y'' = y)
   (WHILE (λs. s ''y''  0) INV (λs. gcd (s ''x'') (s ''y'') = gcd x y) 
    DO
     (''z'' ::= (λs. s ''y''));
     (''y'' ::= (λs. s ''x'' mod s ''y''));
     (''x'' ::= (λs. s ''z''))
    OD)
   POST (λs. s ''x'' = gcd x y)"
  by (rule rel_modal_kleene_algebra.bdia_whilei, auto simp: gcd_non_0_nat)

lemma euclid_diff: 
   "FPRE (λs::nat store. s ''x'' = x  s ''y'' = y  x > 0  y > 0)
    (WHILE (λs. s ''x'' s ''y'') INV (λs. gcd (s ''x'') (s ''y'') = gcd x y) 
     DO
        (IF (λs. s ''x'' >  s ''y'')
         THEN (''x'' ::= (λs. s ''x'' - s ''y''))
         ELSE (''y'' ::= (λs. s ''y'' - s ''x''))
         FI)
    OD)
    POST (λs. s ''x'' = gcd x y)"
  apply (rule rel_modal_kleene_algebra.bdia_whilei, simp_all)
  apply auto[1]
  by (metis gcd.commute gcd_diff1_nat le_cases nat_less_le)

lemma varible_swap:
  "FPRE (λs. s ''x'' = a  s ''y'' = b)   
    (''z'' ::= (λs. s ''x''));
    (''x'' ::= (λs. s ''y''));
    (''y'' ::= (λs. s ''z''))
   POST (λs. s ''x'' = b  s ''y'' = a)"
  by simp

lemma maximum: 
  "FPRE (λs:: nat store. True) 
   (IF (λs. s ''x''  s ''y'') 
    THEN (''z'' ::= (λs. s ''x''))
    ELSE (''z'' ::= (λs. s ''y''))
    FI)
   POST (λs. s ''z'' = max (s ''x'') (s ''y''))"
  by auto

lemma integer_division: 
  "FPRE (λs::nat store. x  0)
    (''q'' ::= (λs. 0)); 
    (''r'' ::= (λs. x));
    (WHILE (λs. y  s ''r'') INV (λs. x = s ''q'' * y + s ''r''  s ''r''  0)
     DO
      (''q'' ::= (λs. s ''q'' + 1));
      (''r'' ::= (λs. s ''r'' - y))
      OD)
   POST (λs. x = s ''q'' * y + s ''r''  s ''r''  0  s ''r'' < y)"
  by (rule rel_modal_kleene_algebra.bdia_whilei_break, simp_all, auto simp: p2r_def)

lemma factorial:
  "FPRE (λs::nat store. True)
   (''x'' ::= (λs. 0));
   (''y'' ::= (λs. 1));
   (WHILE (λs. s ''x''  x0) INV (λs. s ''y'' = fact (s ''x''))
   DO
     (''x'' ::= (λs. s ''x'' + 1));
     (''y'' ::= (λs. s ''y''  s ''x''))
   OD)
   POST (λs. s ''y'' = fact x0)"
  by (rule rel_modal_kleene_algebra.bdia_whilei_break, simp_all, auto simp: p2r_def)
 
lemma my_power:
  "FPRE (λs::nat store. True)
   (''i'' ::= (λs. 0));
   (''y'' ::= (λs. 1));
   (WHILE (λs. s ''i'' < n) INV (λs. s ''y'' = x ^ (s ''i'')  s ''i''  n)
     DO
       (''y'' ::= (λs. (s ''y'') * x));
       (''i'' ::= (λs. s ''i'' + 1))
     OD)
   POST (λs. s ''y'' = x ^ n)"
  by (rule rel_modal_kleene_algebra.bdia_whilei_break, simp_all, auto simp add: p2r_def)

lemma imp_reverse:
  "FPRE (λs:: 'a list store. s ''x'' = X)
   (''y'' ::= (λs. []));
   (WHILE (λs. s ''x''  []) INV (λs. rev (s ''x'') @ s ''y'' = rev X)
    DO 
     (''y'' ::= (λs. hd (s ''x'') # s ''y'')); 
     (''x'' ::= (λs. tl (s ''x'')))
    OD) 
   POST (λs. s ''y''= rev X )"
  apply (rule rel_modal_kleene_algebra.bdia_whilei_break, simp_all)
  apply auto[1]
  by (safe, metis append.simps append_assoc hd_Cons_tl rev.simps(2))

end

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

Theory VC_KAD_wf_Examples

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

subsubsection‹Verification Examples›

theory VC_KAD_wf_Examples
  imports VC_KAD_wf
begin

text ‹The example should be taken with a grain of salt. More work is needed to make 
the while rule cooperate with simplification.›

lemma euclid:
  "rel_nabla (
    λs::nat store. 0 < s ''y'' ; 
      ((''z'' ::= (λs. s ''y'')) ; 
      (''y'' ::= (λs. s ''x'' mod s ''y'')) ;
      (''x'' ::= (λs. s ''z'')))) 
    = {}
    
  PRE (λs::nat store. s ''x'' = x  s ''y'' = y)
   (WHILE (λs. s ''y''  0) INV (λs. gcd (s ''x'') (s ''y'') = gcd x y) 
    DO
     (''z'' ::= (λs. s ''y''));
     (''y'' ::= (λs. s ''x'' mod s ''y''));
     (''x'' ::= (λs. s ''z''))
    OD)
   POST (λs. s ''x'' = gcd x y)"
  apply (subst rel_fdivka.fbox_arden_whilei[symmetric], simp_all)
  using gcd_red_nat gr0I by force

text ‹The termination assumption is now explicit in the verification proof. Here it is left 
untouched. Means beyond these components are required for discharging it.›

end

Theory Path_Model_Example

(* Title: Verification Component Based on KAD: Trace Semantics
   Author: Victor Gomes, Georg Struth
   Maintainer: Victor Gomes <victor.gomes@cl.cam.ac.uk>
               Georg Struth <g.struth@sheffield.ac.uk> 
*)

subsection ‹Two Extensions›

subsubsection ‹KAD Component with Trace Semantics›

theory Path_Model_Example
  imports VC_KAD "HOL-Eisbach.Eisbach"
begin

text ‹This component supports the verification of simple while programs
in a partial correctness setting based on a program trace semantics.›

text ‹Program traces are modelled as non-empty paths or state sequences. The non-empty path model 
of Kleene algebra is taken from the AFP entry for Kleene algebra. Here we show that sets of paths form
antidomain Kleene Algebras.›

definition pp_a ::  "'a ppath set  'a ppath set" where
  "pp_a X = {(Node u) |u. ¬ (v  X. u = pp_first v)}"

interpretation ppath_aka: antidomain_kleene_algebra pp_a "(∪)" pp_prod pp_one "{}" "(⊆)" "(⊂)" pp_star
  apply standard
  apply (clarsimp simp add: pp_prod_def pp_a_def)
  apply (simp add: pp_prod_def pp_a_def, safe, metis pp_first.simps(1) pp_first_pp_fusion)
  by (auto simp: pp_a_def pp_one_def)   

text ‹A verification component can then be built with little effort, by and large reusing
parts of the relational components that are generic with respect to the store.›      

definition pp_gets :: "string  ('a store  'a)  'a store ppath set" ("_ ::= _" [70, 65] 61) where 
  "v ::= e = {Cons s (Node (s (v := e s))) | s. True}"

definition p2pp :: "'a pred  'a ppath set" where
  "p2pp P = {Node s |s. P s}"

lemma pp_a_neg [simp]: "pp_a (p2pp Q) = p2pp (-Q)"
  by (force simp add: pp_a_def p2pp_def)

lemma ppath_assign [simp]: "ppath_aka.fbox (v ::= e) (p2pp Q) = p2pp (λs. Q (s(v := e s)))"
  by (force simp: ppath_aka.fbox_def pp_a_def p2pp_def pp_prod_def pp_gets_def)      

no_notation spec_sugar ("PRE _ _ POST _" [64,64,64] 63)
   and relcomp (infixl ";" 70)
   and cond_sugar ("IF _ THEN _ ELSE _ FI" [64,64,64] 63)
   and whilei_sugar ("WHILE _ INV _ DO _ OD" [64,64,64] 63)
   and gets ("_ ::= _" [70, 65] 61)
   and rel_antidomain_kleene_algebra.fbox ("wp")
   and rel_antidomain_kleene_algebra.ads_d ("rdom")
   and p2r ("_")

notation ppath_aka.fbox ("wp")
  and ppath_aka.ads_d ("rdom")
  and p2pp ("_")
  and pp_prod (infixl ";" 70)

abbreviation spec_sugar :: "'a pred  'a ppath set  'a pred  bool" ("PRE _ _ POST _" [64,64,64] 63) where
  "PRE P X POST Q  rdom P  wp X Q"

abbreviation cond_sugar :: "'a pred  'a ppath set  'a ppath set  'a ppath set" ("IF _ THEN _ ELSE _ FI" [64,64,64] 63) where
  "IF P THEN X ELSE Y FI  ppath_aka.cond P X Y"

abbreviation whilei_sugar :: "'a pred  'a pred  'a ppath set  'a ppath set" ("WHILE _ INV _ DO _ OD" [64,64,64] 63) where
  "WHILE P INV I DO X OD  ppath_aka.whilei P I X"

lemma [simp]: "p2pp P  p2pp Q = p2pp (P  Q)"
  by (force simp: p2pp_def)

lemma [simp]: "p2pp P; p2pp Q = p2pp (P  Q)"
  by (force simp: p2pp_def pp_prod_def)

lemma [intro!]:  "P  Q  P  Q"
  by (force simp: p2pp_def)

lemma [simp]: "rdom P = P"
  by (simp add: ppath_aka.addual.ars_r_def)

lemma euclid:
  "PRE (λs::nat store. s ''x'' = x  s ''y'' = y)
   (WHILE (λs. s ''y''  0) INV (λs. gcd (s ''x'') (s ''y'') = gcd x y) 
    DO
     (''z'' ::= (λs. s ''y''));
     (''y'' ::= (λs. s ''x'' mod s ''y''));
     (''x'' ::= (λs. s ''z''))
    OD)
   POST (λs. s ''x'' = gcd x y)"
  by (rule ppath_aka.fbox_whilei, simp_all, auto simp: p2pp_def rel_ad_def gcd_non_0_nat)

lemma euclid_diff: 
   "PRE (λs::nat store. s ''x'' = x  s ''y'' = y  x > 0  y > 0)
    (WHILE (λs. s ''x'' s ''y'') INV (λs. gcd (s ''x'') (s ''y'') = gcd x y) 
     DO
        (IF (λs. s ''x'' >  s ''y'')
         THEN (''x'' ::= (λs. s ''x'' - s ''y''))
         ELSE (''y'' ::= (λs. s ''y'' - s ''x''))
         FI)
    OD)
    POST (λs. s ''x'' = gcd x y)"
  apply (rule ppath_aka.fbox_whilei, simp_all)
  apply (simp_all add: p2pp_def) 
  apply auto[2]
  by (safe, metis gcd.commute gcd_diff1_nat le_cases nat_less_le)

lemma varible_swap:
  "PRE (λs. s ''x'' = a  s ''y'' = b)   
    (''z'' ::= (λs. s ''x''));
    (''x'' ::= (λs. s ''y''));
    (''y'' ::= (λs. s ''z''))
   POST (λs. s ''x'' = b  s ''y'' = a)"
  by auto

lemma maximum: 
  "PRE (λs:: nat store. True) 
   (IF (λs. s ''x''  s ''y'') 
    THEN (''z'' ::= (λs. s ''x''))
    ELSE (''z'' ::= (λs. s ''y''))
    FI)
   POST (λs. s ''z'' = max (s ''x'') (s ''y''))"
  by auto

lemma integer_division: 
  "PRE (λs::nat store. x  0)
    (''q'' ::= (λs. 0)); 
    (''r'' ::= (λs. x));
    (WHILE (λs. y  s ''r'') INV (λs. x = s ''q'' * y + s ''r''  s ''r''  0)
     DO
      (''q'' ::= (λs. s ''q'' + 1));
      (''r'' ::= (λs. s ''r'' - y))
      OD)
   POST (λs. x = s ''q'' * y + s ''r''  s ''r''  0  s ''r'' < y)"
  by (rule ppath_aka.fbox_whilei_break, auto)
 
text ‹We now reconsider these examples with an Eisbach tactic.›

named_theorems ht

declare ppath_aka.fbox_whilei [ht]
  ppath_aka.fbox_seq_var [ht]
  subset_refl[ht]

method hoare = (rule ht; hoare?)

lemma euclid2:
  "PRE (λs::nat store. s ''x'' = x  s ''y'' = y)
   (WHILE (λs. s ''y''  0) INV (λs. gcd (s ''x'') (s ''y'') = gcd x y) 
    DO
     (''z'' ::= (λs. s ''y''));
     (''y'' ::= (λs. s ''x'' mod s ''y''));
     (''x'' ::= (λs. s ''z''))
    OD)
   POST (λs. s ''x'' = gcd x y)"
apply hoare
using gcd_red_nat by auto

lemma euclid_diff2: 
   "PRE (λs::nat store. s ''x'' = x  s ''y'' = y  x > 0  y > 0)
    (WHILE (λs. s ''x'' s ''y'') INV (λs. gcd (s ''x'') (s ''y'') = gcd x y) 
     DO
        (IF (λs. s ''x'' >  s ''y'')
         THEN (''x'' ::= (λs. s ''x'' - s ''y''))
         ELSE (''y'' ::= (λs. s ''y'' - s ''x''))
         FI)
    OD)
    POST (λs. s ''x'' = gcd x y)"
  by (hoare; clarsimp; metis gcd.commute gcd_diff1_nat le_cases nat_less_le)

lemma varible_swap2:
  "PRE (λs. s ''x'' = a  s ''y'' = b)   
    (''z'' ::= (λs. s ''x''));
    (''x'' ::= (λs. s ''y''));
    (''y'' ::= (λs. s ''z''))
   POST (λs. s ''x'' = b  s ''y'' = a)"
  by clarsimp

lemma maximum2: 
  "PRE (λs:: nat store. True) 
   (IF (λs. s ''x''  s ''y'') 
    THEN (''z'' ::= (λs. s ''x''))
    ELSE (''z'' ::= (λs. s ''y''))
    FI)
   POST (λs. s ''z'' = max (s ''x'') (s ''y''))"
   by auto

lemma integer_division2: 
  "PRE (λs::nat store. x  0)
    (''q'' ::= (λs. 0)); 
    (''r'' ::= (λs. x));
    (WHILE (λs. y  s ''r'') INV (λs. x = s ''q'' * y + s ''r''  s ''r''  0)
     DO
      (''q'' ::= (λs. s ''q'' + 1));
      (''r'' ::= (λs. s ''r'' - y))
      OD)
   POST (λs. x = s ''q'' * y + s ''r''  s ''r''  0  s ''r'' < y)"
   by hoare auto

lemma my_power2:
  "PRE (λs::nat store. True)
   (''i'' ::= (λs. 0));
   (''y'' ::= (λs. 1));
   (WHILE (λs. s ''i'' < n) INV (λs. s ''y'' = x ^ (s ''i'')  s ''i''  n)
     DO
       (''y'' ::= (λs. (s ''y'') * x));
       (''i'' ::= (λs. s ''i'' + 1))
     OD)
   POST (λs. s ''y'' = x ^ n)"
  by hoare auto

lemma imp_reverse2:
  "PRE (λs:: 'a list store. s ''x'' = X)
   (''y'' ::= (λs. []));
   (WHILE (λs. s ''x''  []) INV (λs. rev (s ''x'') @ s ''y'' = rev X)
    DO 
     (''y'' ::= (λs. hd (s ''x'') # s ''y'')); 
     (''x'' ::= (λs. tl (s ''x'')))
    OD) 
   POST (λs. s ''y''= rev X )"
  apply hoare
  apply auto
  apply (metis append.simps append_assoc hd_Cons_tl rev.simps(2))
done

end

Theory Pointer_Examples

(* Title: Verification Component Based on KAD: Programs with Pointers
   Author: Victor Gomes, Georg Struth
   Maintainer: Victor Gomes <victor.gomes@cl.cam.ac.uk>
               Georg Struth <g.struth@sheffield.ac.uk> 
*)

subsubsection‹KAD Component for Pointer Programs›

theory Pointer_Examples
  imports VC_KAD_Examples2 "HOL-Hoare.Heap"

begin

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

text‹All we do here is integrating Nipkow's implementation of pointers and heaps.›

type_synonym 'a state = "string   ('a ref + ('a  'a ref))"

lemma list_reversal:
  "PRE (λs :: 'a state. List (projr (s ''h'')) (projl (s ''p'')) Ps 
         List (projr (s ''h'')) (projl (s ''q'')) Qs 
         set Ps  set Qs = {})
    (WHILE (λs. projl (s ''p'')  Null) 
     INV (λs. ps qs. List (projr (s ''h'')) (projl (s ''p'')) ps 
               List (projr (s ''h'')) (projl (s ''q'')) qs 
               set ps  set qs = {}  rev ps @ qs = rev Ps @ Qs)
     DO
      (''r'' ::= (λs. s ''p''));
      (''p'' ::= (λs. Inl (projr (s ''h'') (addr (projl (s ''p''))))) );
      (''h'' ::= (λs. Inr ((projr (s ''h''))(addr (projl (s ''r'')) := projl (s ''q''))) ));
      (''q'' ::= (λs. s ''r''))
     OD)
  POST (λs. List (projr (s ''h'')) (projl (s ''q'')) (rev Ps @ Qs))"
  apply hoare 
  apply auto[2]
  by (clarsimp, fastforce intro: notin_List_update[THEN iffD2])

end

Theory KAD_is_KAT

(* Title: KAD is KAT
   Author: Victor Gomes, Georg Struth
   Maintainer: Victor Gomes <victor.gomes@cl.cam.ac.uk>
               Georg Struth <g.struth@sheffield.ac.uk> 
*)

section ‹Bringing KAT Components into Scope of KAD›

theory KAD_is_KAT
imports KAD.Antidomain_Semiring 
        KAT_and_DRA.KAT
        "AVC_KAD/VC_KAD"
        "AVC_KAT/VC_KAT"

begin

context antidomain_kleene_algebra
begin

text ‹Every Kleene algebra with domain is a Kleene algebra with tests. This fact should eventually move into
the AFP KAD entry.›

sublocale kat "(+)" "(⋅)" "1" "0" "(≤)" "(<)" star antidomain_op
  apply standard
  apply simp
  using a_d_mult_closure am_d_def apply auto[1]
  using dpdz.dom_weakly_local apply auto[1]
  using a_d_add_closure a_de_morgan by presburger

text ‹The next statement links the wp operator with the Hoare triple.›

lemma H_kat_to_kad: "H p x q  d p  |x] (d q)"
  using H_def addual.ars_r_def fbox_demodalisation3 by auto

end
 
lemma H_eq: "P  Id  Q  Id  rel_kat.H P X Q = rel_antidomain_kleene_algebra.H P X Q"
  apply (simp add: rel_kat.H_def rel_antidomain_kleene_algebra.H_def)
  apply (subgoal_tac "rel_antidomain_kleene_algebra.t P = Id  P")
  apply (subgoal_tac "rel_antidomain_kleene_algebra.t Q = Id  Q")
  apply simp
  apply (auto simp: rel_ad_def)
done

no_notation VC_KAD.spec_sugar ("PRE _ _ POST _" [64,64,64] 63)
and VC_KAD.cond_sugar ("IF _ THEN _ ELSE _ FI" [64,64,64] 63)
and VC_KAD.gets ("_ ::= _" [70, 65] 61)

text ‹Next we provide some syntactic sugar.›

lemma H_from_kat: "PRE p x POST q = (p  (rel_antidomain_kleene_algebra.fbox x) q)"
  apply (subst H_eq)
  apply (clarsimp simp add: p2r_def)
  apply (clarsimp simp add: p2r_def)
  apply (subst rel_antidomain_kleene_algebra.H_kat_to_kad)
  apply (subgoal_tac "rel_antidomain_kleene_algebra.ads_d p = p")
  apply (subgoal_tac "rel_antidomain_kleene_algebra.ads_d q = q")
  apply simp
  apply (auto simp: rel_antidomain_kleene_algebra.ads_d_def rel_ad_def p2r_def)
done

lemma cond_iff: "rel_kat.ifthenelse P X Y = rel_antidomain_kleene_algebra.cond P X Y"
  by (auto simp: rel_kat.ifthenelse_def rel_antidomain_kleene_algebra.cond_def)

lemma gets_iff: "v ::= e = VC_KAD.gets v e"
  by (auto simp: VC_KAT.gets_def VC_KAD.gets_def)

text ‹Finally we present two examples to test the integration.›

lemma maximum: 
  "PRE (λs:: nat store. True)
   (IF (λs. s ''x''  s ''y'') 
    THEN (''z'' ::= (λs. s ''x''))
    ELSE (''z'' ::= (λs. s ''y''))
    FI)
   POST (λs. s ''z'' = max (s ''x'') (s ''y''))"
  by (simp only: sH_cond_iff H_assign_iff, auto)

lemma maximum2: 
  "PRE (λs:: nat store. True)
   (IF (λs. s ''x''  s ''y'') 
    THEN (''z'' ::= (λs. s ''x''))
    ELSE (''z'' ::= (λs. s ''y''))
    FI)
   POST (λs. s ''z'' = max (s ''x'') (s ''y''))"
   apply (subst H_from_kat)
   apply (subst cond_iff)
   apply (subst gets_iff)
   apply (subst gets_iff)
   by auto

end

Theory Domain_Quantale

(* Title: Domain Quantales
   Author: Victor Gomes, Georg Struth
   Maintainer: Victor Gomes <victor.gomes@cl.cam.ac.uk>
               Georg Struth <g.struth@sheffield.ac.uk> 
*)

section ‹Component for Recursive Programs›

theory Domain_Quantale
  imports KAD.Modal_Kleene_Algebra

begin

text ‹This component supports the verification and step-wise refinement of recursive programs
in a partial correctness setting.›

notation
  times (infixl "" 70) and
  bot ("") and
  top ("") and
  inf (infixl "" 65) and
  sup (infixl "" 65)
(*
  Inf ("⨅_" [900] 900) and
  Sup ("⨆_" [900] 900)
*)

(*
syntax
  "_INF1"     :: "pttrns ⇒ 'b ⇒ 'b"           ("(3⨅_./ _)" [0, 10] 10)
  "_INF"      :: "pttrn ⇒ 'a set ⇒ 'b ⇒ 'b"  ("(3⨅_∈_./ _)" [0, 0, 10] 10)
  "_SUP1"     :: "pttrns ⇒ 'b ⇒ 'b"           ("(3⨆_./ _)" [0, 10] 10)
  "_SUP"      :: "pttrn ⇒ 'a set ⇒ 'b ⇒ 'b"  ("(3⨆_∈_./ _)" [0, 0, 10] 10)

*)

subsection ‹Lattice-Ordered Monoids with Domain›

class bd_lattice_ordered_monoid = bounded_lattice + distrib_lattice + monoid_mult +
  assumes left_distrib: "x  (y  z) = x  y  x  z"
  and right_distrib: "(x  y)  z = x  z  y  z"
  and bot_annil [simp]: "  x = "
  and bot_annir [simp]: "x   = "

begin

sublocale semiring_one_zero "(⊔)" "(⋅)" "1" "bot" 
  by (standard, auto simp: sup.assoc sup.commute sup_left_commute left_distrib right_distrib sup_absorb1)   

sublocale dioid_one_zero "(⊔)" "(⋅)" "1" bot "(≤)" "(<)"
  by (standard, simp add: le_iff_sup, auto)

end

no_notation ads_d ("d")
  and ars_r ("r")
  and antirange_op ("ar _" [999] 1000)

class domain_bdlo_monoid = bd_lattice_ordered_monoid +
  assumes rdv: "(z  x  top)  y = z  y  x  top"  

begin 

definition "d x = 1  x  "

sublocale ds: domain_semiring "(⊔)" "(⋅)" "1" "" "d" "(≤)" "(<)"
proof standard
  fix x y
  show "x  d x  x = d x  x"
    by (metis d_def inf_sup_absorb left_distrib mult_1_left mult_1_right rdv sup.absorb_iff1 sup.idem sup.left_commute top_greatest)
  show "d (x  d y) = d (x  y)"
    by (simp add: d_def inf_absorb2 rdv  mult_assoc)
  show "d x  1 = 1"
    by (simp add: d_def sup.commute)
  show "d bot = bot"
    by (simp add: d_def inf.absorb1 inf.commute)
  show "d (x  y) = d x  d y"
    by (simp add: d_def inf_sup_distrib1)
qed

end

subsection‹Boolean Monoids with Domain›

class boolean_monoid = boolean_algebra + monoid_mult +  
  assumes left_distrib': "x  (y  z) = x  y  x  z"
  and right_distrib': "(x  y)  z = x  z  y  z"
  and bot_annil' [simp]: "  x = "
  and bot_annir' [simp]: "x   = "

begin

subclass bd_lattice_ordered_monoid
  by (standard, simp_all add: left_distrib' right_distrib')

lemma inf_bot_iff_le: "x  y =   x  -y"
  by (metis le_iff_inf inf_sup_distrib1 inf_top_right sup_bot.left_neutral sup_compl_top compl_inf_bot inf.assoc inf_bot_right)

end

class domain_boolean_monoid = boolean_monoid + 
  assumes rdv': "(z  x  )  y = z  y  x  "     

begin

sublocale dblo: domain_bdlo_monoid "1" "(⋅)" "(⊓)" "(≤)" "(<)" "(⊔)" "" ""
  by (standard, simp add: rdv')

definition "a x = 1  -(dblo.d x)"
                                
lemma a_d_iff: "a x = 1  -(x  )"
  by (clarsimp simp: a_def dblo.d_def inf_sup_distrib1) 

lemma topr: "-(x  )   = -(x  )" 
proof (rule order.antisym)
  show "-(x  )  -(x  )  "
    by (metis mult_isol_var mult_oner order_refl top_greatest)
  have "-(x  )  (x  ) = "
    by simp
  hence "(-(x  )  (x  ))    = "
    by simp 
  hence "-(x  )    (x  )  = "
    by (metis rdv') 
  thus "-(x  )    -(x  )"
    by (simp add: inf_bot_iff_le)
qed

lemma dd_a: "dblo.d x = a (a x)"
  by (metis a_d_iff dblo.d_def double_compl inf_top.left_neutral mult_1_left rdv' topr)

lemma ad_a [simp]: "a (dblo.d x) = a x"
  by (simp add: a_def)

lemma da_a [simp]: "dblo.d (a x) = a x"
  using ad_a dd_a by auto

lemma a1 [simp]: "a x  x = "
proof -
  have "a x  x   = "
    by (metis a_d_iff inf_compl_bot mult_1_left rdv' topr)
  then show ?thesis
    by (metis (no_types) dblo.d_def dblo.ds.domain_very_strict inf_bot_right)
qed

lemma a2 [simp]: "a (x  y)  a (x  a (a y)) = a (x  a (a y))"
  by (metis a_def dblo.ds.dsr2 dd_a sup.idem)

lemma a3 [simp]: "a (a x)  a x = 1"
  by (metis a_def da_a inf.commute sup.commute sup_compl_top sup_inf_absorb sup_inf_distrib1)

subclass domain_bdlo_monoid ..

text ‹The next statement shows that every boolean monoid with domain is an antidomain semiring. 
In this setting the domain operation has been defined explicitly.›

sublocale ad: antidomain_semiring a "(⊔)" "(⋅)" "1" "" "(≤)" "(<)"
  rewrites ad_eq: "ad.ads_d x = d x"
proof -
  show "class.antidomain_semiring a (⊔) (⋅) 1  (≤) (<)"
    by (standard, simp_all)
  then interpret ad: antidomain_semiring a "(⊔)" "(⋅)" "1" "" "(≤)" "(<)" .
  show "ad.ads_d x = d x"
    by (simp add: ad.ads_d_def dd_a)
qed

end 

subsection‹Boolean Monoids with Range›

class range_boolean_monoid = boolean_monoid + 
  assumes ldv': "y  (z    x) = y  z    x"

begin

definition "r x = 1    x"

definition "ar x = 1  -(r x)"
                                
lemma ar_r_iff: "ar x = 1  -(  x)"
  by (simp add: ar_def inf_sup_distrib1 r_def)

lemma topl: "(-(  x)) = -(  x)" 
proof (rule order.antisym)
  show "  - (  x)  - (  x)"
    by (metis bot_annir' compl_inf_bot inf_bot_iff_le ldv')
  show "- (  x)    - (  x)"
    by (metis inf_le2 inf_top.right_neutral mult_1_left mult_isor)
qed

lemma r_ar: "r x = ar (ar x)"
  by (metis ar_r_iff double_compl inf.commute inf_top.right_neutral ldv' mult_1_right r_def topl)

lemma ar_ar [simp]: "ar (r x) = ar x"
  by (simp add: ar_def ldv' r_def)

lemma rar_ar [simp]: "r (ar x) = ar x"
  using r_ar ar_ar by force

lemma ar1 [simp]: "x  ar x = "
proof -
  have "  x  ar x = "
    by (metis ar_r_iff inf_compl_bot ldv' mult_oner topl)
  then show ?thesis
    by (metis inf_bot_iff_le inf_le2 inf_top.right_neutral mult_1_left mult_isor mult_oner topl)
qed

lemma ars: "r (r x  y) = r (x  y)"
  by (metis inf.commute inf_top.right_neutral ldv' mult_oner mult_assoc r_def)

lemma ar2 [simp]: "ar (x  y)  ar (ar (ar x)  y) = ar (ar (ar x)  y)"
  by (metis ar_def ars r_ar sup.idem)
                         
lemma ar3 [simp]: "ar (ar x)  ar x = 1 "
  by (metis ar_def rar_ar inf.commute sup.commute sup_compl_top sup_inf_absorb sup_inf_distrib1)

sublocale ar: antirange_semiring "(⊔)" "(⋅)" "1" "" ar "(≤)" "(<)"
  rewrites ar_eq: "ar.ars_r x = r x"
proof -
  show "class.antirange_semiring (⊔) (⋅) 1  ar (≤) (<)"
    by (standard, simp_all)
  then interpret ar: antirange_semiring "(⊔)" "(⋅)" "1" "" ar "(≤)" "(<)" .
  show "ar.ars_r x = r x"
    by (simp add: ar.ars_r_def r_ar)
qed

end

subsection ‹Quantales›

text ‹This part will eventually move into an AFP quantale entry.› 

class quantale = complete_lattice + monoid_mult +
  assumes Sup_distr: "Sup X  y = Sup {z. x  X. z = x  y}"
  and Sup_distl: "x  Sup Y = Sup {z. y  Y. z = x  y}"       

begin

lemma bot_annil'' [simp]: "  x = "
  using Sup_distr[where X="{}"] by auto

lemma bot_annirr'' [simp]: "x   = "
  using Sup_distl[where Y="{}"] by auto

lemma sup_distl: "x  (y  z) = x  y  x  z"
  using Sup_distl[where Y="{y, z}"] by (fastforce intro!: Sup_eqI)

lemma sup_distr: "(x  y)  z = x  z  y  z"
  using Sup_distr[where X="{x, y}"] by (fastforce intro!: Sup_eqI)

sublocale semiring_one_zero "(⊔)" "(⋅)" "1" "" 
  by (standard, auto simp: sup.assoc sup.commute sup_left_commute sup_distl sup_distr)     

sublocale dioid_one_zero "(⊔)" "(⋅)" "1" "" "(≤)" "(<)"
  by (standard, simp add: le_iff_sup, auto)

lemma Sup_sup_pred: "x  Sup{y. P y} = Sup{y. y = x  P y}"
  apply (rule order.antisym)
  apply (simp add: Collect_mono Sup_subset_mono Sup_upper) 
  using Sup_least Sup_upper le_supI2 by fastforce

definition star :: "'a  'a" where
  "star x = (SUP i. x ^ i)"

lemma star_def_var1: "star x = Sup{y. i. y = x ^ i}"
  by (simp add: star_def full_SetCompr_eq)

lemma star_def_var2: "star x = Sup{x ^ i |i. True}"
  by (simp add: star_def full_SetCompr_eq)

lemma star_unfoldl' [simp]: "1  x  (star x) = star x"
proof -
  have "1  x  (star x) = x ^ 0  x  Sup{y. i. y = x ^ i}"
    by (simp add: star_def_var1)
  also have "... = x ^ 0  Sup{y. i. y = x ^ (i + 1)}"
    by (simp add: Sup_distl, metis)
  also have "... = Sup{y. y = x ^ 0  (i. y = x ^ (i + 1))}"
    using Sup_sup_pred by simp
  also have "... = Sup{y. i. y = x ^ i}"
    by (metis Suc_eq_plus1 power.power.power_Suc power.power_eq_if)
  finally show ?thesis
    by (simp add: star_def_var1)
qed

lemma star_unfoldr' [simp]: "1  (star x)  x = star x"
proof -
  have "1  (star x)  x = x ^ 0  Sup{y. i. y = x ^ i}  x"
    by (simp add: star_def_var1)
  also have "... = x ^ 0  Sup{y. i. y = x ^ i  x}"
    by (simp add: Sup_distr, metis)
  also have "... = x ^ 0  Sup{y. i. y = x ^ (i + 1)}"
    using power_Suc2 by simp 
   also have "... = Sup{y. y = x ^ 0  (i. y = x ^ (i + 1))}"
    using Sup_sup_pred by simp
  also have "... = Sup{y. i. y = x ^ i}"
    by (metis Suc_eq_plus1 power.power.power_Suc power.power_eq_if)
  finally show ?thesis
    by (simp add: star_def_var1)
qed

lemma (in dioid_one_zero) power_inductl: "z + x  y  y  (x ^ n)  z  y"
proof (induct n)
  case 0 show ?case
    using "0.prems" by simp
  case Suc thus ?case
    by (simp, metis mult.assoc mult_isol order_trans)
qed

lemma (in dioid_one_zero) power_inductr: "z + y  x  y  z  (x ^ n)  y"
proof (induct n)
  case 0 show ?case
    using "0.prems" by auto
  case Suc
  {
    fix n
    assume "z + y  x  y  z  x ^ n  y"
      and "z + y  x  y"
    hence "z  x ^ n  y"
      by simp
    also have "z  x ^ Suc n = z  x  x ^ n"
      by (metis mult.assoc power_Suc)
    moreover have "... = (z  x ^ n)  x"
      by (metis mult.assoc power_commutes)
    moreover have "...  y  x"
      by (metis calculation(1) mult_isor)
    moreover have "...  y"
      using z + y  x  y by simp
    ultimately have "z  x ^ Suc n  y" by simp
  }
  thus ?case
    by (metis Suc)
qed

lemma star_inductl': "z  x  y  y  (star x)  z  y" 
proof -
  assume "z  x  y  y"
  hence "i. x ^ i  z  y"
    by (simp add: power_inductl)
  hence "Sup{w. i. w = x ^ i  z}  y"
    by (intro Sup_least, fast)
  hence "Sup{w. i. w = x ^ i}  z  y"
    using Sup_distr Sup_le_iff by auto
  thus "(star x)  z  y"
    by (simp add: star_def_var1)
qed

lemma star_inductr': "z  y  x  y  z  (star x)  y" 
proof -
  assume "z  y  x  y"
  hence "i. z  x ^ i   y"
    by (simp add: power_inductr)
  hence "Sup{w. i. w = z  x ^ i}  y"
    by (intro Sup_least, fast)
  hence "z  Sup{w. i. w = x ^ i}  y"
    using Sup_distl Sup_le_iff by auto
  thus "z  (star x)  y"
    by (simp add: star_def_var1)
qed

sublocale ka: kleene_algebra "(⊔)" "(⋅)" "1" "" "(≤)" "(<)" star
  by standard (simp_all add: star_inductl' star_inductr')

end

text ‹Distributive quantales are often assumed to satisfy infinite distributivity laws between
joins and meets, but finite ones suffice for our purposes.›

class distributive_quantale = quantale + distrib_lattice 

begin

subclass bd_lattice_ordered_monoid
  by (standard, simp_all add: distrib_left)

lemma "(1  x  )  x = x"
(* nitpick [expect=genuine]*)
oops

end 

subsection ‹Domain Quantales›

class domain_quantale = distributive_quantale +
  assumes rdv'': "(z  x  )  y = z  y  x  "  

begin

subclass domain_bdlo_monoid 
  by (standard, simp add: rdv'')

end

class range_quantale = distributive_quantale +
  assumes ldv'': "y  (z    x) = y  z    x"

class boolean_quantale = quantale + complete_boolean_algebra

begin

subclass boolean_monoid
  by (standard, simp_all add: sup_distl)

lemma "(1  x  )  x = x"
(*nitpick[expect=genuine]*)
oops

lemma "(1  -(x  ))  x = "
(*nitpick[expect=genuine]*)
oops

end

subsection‹Boolean Domain Quantales› 

class domain_boolean_quantale = domain_quantale + boolean_quantale

begin

subclass domain_boolean_monoid
  by (standard, simp add: rdv'')

lemma fbox_eq: "ad.fbox x q = Sup{d p |p. d p  x  x  d q}"
  apply (rule Sup_eqI[symmetric])
  apply clarsimp
  using ad.fbox_demodalisation3 ad.fbox_simp apply auto[1]
  apply clarsimp
  by (metis ad.fbox_def ad.fbox_demodalisation3 ad.fbox_simp da_a eq_refl)

lemma fdia_eq: "ad.fdia x p = Inf{d q |q. x  d p  d q  x}"
  apply (rule Inf_eqI[symmetric])
  apply clarsimp
  using ds.fdemodalisation2 apply auto[1]
  apply clarsimp
  by (metis ad.fd_eq_fdia ad.fdia_def da_a double_compl ds.fdemodalisation2 inf_bot_iff_le inf_compl_bot)

text ‹The specification statement can be defined explicitly.›

definition R :: "'a  'a  'a" where
  "R p q  Sup{x. (d p)  x  x  d q}"

lemma "x  R p q  d p  ad.fbox x (d q)"
proof (simp add: R_def ad.kat_1_equiv ad.kat_2_equiv)
  assume "x  Sup{x. d p  x  a q = }"
  hence "d p  x  a q  d p  Sup{x. d p  x  a q = }  a q "
    using mult_double_iso by blast
  also have "... = Sup{d p  x  a q |x. d p  x  a q = }"
    apply (subst Sup_distl)
    apply (subst Sup_distr)
    apply clarsimp
    by metis
  also have "... = "
    by (auto simp: Sup_eqI)
  finally show ?thesis
    using ad.fbox_demodalisation3 ad.kat_3 ad.kat_4 le_bot by blast
qed

lemma "d p  ad.fbox x (d q)  x  R p q"
  apply (simp add: R_def)
  apply (rule Sup_upper)
  apply simp
  using ad.fbox_demodalisation3 ad.fbox_simp apply auto[1]
done

end

subsection‹Relational Model of Boolean Domain Quantales›

interpretation rel_dbq: domain_boolean_quantale Inter Union "(∩)" "(⊆)" "(⊂)" "(∪)" "{}" UNIV minus uminus Id "(O)"
  apply (standard, simp_all add: O_assoc)
  by blast +

subsection‹Modal Boolean Quantales›

class range_boolean_quantale = range_quantale + boolean_quantale

begin

subclass range_boolean_monoid
  by (standard, simp add: ldv'')

lemma fbox_eq: "ar.bbox x (r q) = Sup{r p |p. x  r p  (r q)  x}"
  apply (rule Sup_eqI[symmetric])
  apply clarsimp
  using ar.ardual.fbox_demodalisation3 ar.ardual.fbox_simp apply auto[1]
  apply clarsimp
  by (metis ar.ardual.fbox_def ar.ardual.fbox_demodalisation3 eq_refl rar_ar)

lemma fdia_eq: "ar.bdia x (r p) = Inf{r q |q. (r p)  x  x  r q}"
  apply (rule Inf_eqI[symmetric])
  apply clarsimp
  using ar.ars_r_def ar.ardual.fdemodalisation22 ar.ardual.kat_3_equiv_opp ar.ardual.kat_4_equiv_opp apply auto[1]
  apply clarsimp
  using ar.bdia_def ar.ardual.ds.fdemodalisation2 r_ar by fastforce

end

class modal_boolean_quantale = domain_boolean_quantale + range_boolean_quantale +
  assumes domrange' [simp]: "d (r x) = r x"
  and rangedom' [simp]: "r (d x) = d x"

begin

sublocale mka: modal_kleene_algebra "(⊔)" "(⋅)" 1  "(≤)" "(<)" star a ar
  by standard (simp_all add: ar_eq ad_eq)

end

no_notation fbox ("( |_] _)" [61,81] 82)
  and antidomain_semiringl_class.fbox ("( |_] _)" [61,81] 82)

notation ad.fbox ("( |_] _)" [61,81] 82)

subsection ‹Recursion Rule›

lemma recursion: "mono (f :: 'a  'a :: domain_boolean_quantale)  
  (x. d p  |x] d q  d p  |f x] d q)   d p  |lfp f] d q"
  apply (erule lfp_ordinal_induct [where f=f], simp)
  by (auto simp: ad.addual.ardual.fbox_demodalisation3 Sup_distr Sup_distl intro: Sup_mono)

text ‹We have already tested this rule in the context of test quantales~\cite{ArmstrongGS15}, which is based
on a formalisation of quantales that is currently not in the AFP. The two theories will be merged as
soon as the quantale is available in the AFP.›

end