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 force

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"

lemma add_lub: "x + y ≤ z ⟷ x ≤ z ∧ y ≤ z"

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
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"

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
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"
also have "... ≤ t r ⋅ x ⋅ t q + t p ⋅ at r ⋅ y"
also have "... ≤ t r ⋅ x ⋅ t q + at r ⋅ y ⋅ t q"
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"
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"
by (metis local.dual_order.trans local.mult_isol mult_assoc)

lemma (in dioid) power_inductr: "z + y ⋅ x ≤ y ⟹ z ⋅ x ^ i ≤ y"
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"
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)"

lemma rel_star_contl: "X ; Y^* = (⋃i. X ; rel_d.power Y i)"

lemma rel_star_contr: "X^* ; Y = (⋃i. (rel_d.power X i) ; Y)"

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"

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⌉"

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


(* 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.›

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

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"

lemma add_ub: "x ≤ x + y"

lemma add_lub: "x + y ≤ z ⟷ x ≤ z ∧ y ≤ z"

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
qed

end

class antidomain_kleene_algebra = kleene_algebra +
assumes as1 [simp]: "ad x ⋅ x = 0"

begin

definition dom_op :: "'a ⇒ 'a" ("d") where

lemma a_subid_aux: "ad x ⋅ y ≤ y"

lemma d1_a [simp]: "d x ⋅ x = x"

lemma a_mul_d [simp]: "ad x ⋅ d x = 0"

by (metis d1_a dom_op_def add_zerol as1 as3 distrib_left mult_1_right)

by (metis a_d_closed d1_a)

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)

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)

by (metis a_supdist less_eq_def)

proof -
{ fix x y
by (metis a_antitone a_d_closed a_subid_aux mult_oner a_subid_aux dom_op_def mult_isol mult_isor meet_ord)
by simp }
thus ?thesis
qed

proof -
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

proof (rule order.antisym)
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)
by (metis dom_op_def as3 distrib_left mult_oner)
using a add_lub dual_order.trans by blast
by (metis a_antitone a_comm a_subid_aux meet_ord)
next
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"
finally show ?thesis
qed

proof (rule order.antisym)
by (metis a_supdist add_commute mult_isor meet_ord)
by (metis a_closed a_exp)
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"
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"
qed

proof
hence "ad x ⋅ d y ≤ ad y ⋅ d y + ad z ⋅ d y"
by (metis distrib_right mult_isor)
by (metis a_closed a_d_closed a_exp a_mul_d a_supdist dom_op_def dual_order.trans less_eq_def)
next
by (metis add_commute dom_op_def as3 distrib_left mult_1_right)
using h add_lub dual_order.trans by blast
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

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)"
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

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"
by (metis local.dual_order.trans local.mult_isol mult_assoc)

lemma (in dioid) pow_inductr: "z + y ⋅ x ≤ y ⟹ z ⋅ x ^ i ≤ y"
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"
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)"

lemma rel_star_contl: "X ; Y^* = (⋃i. X ; rel_d.power Y i)"

lemma rel_star_contr: "X^* ; Y = (⋃i. (rel_d.power X i) ; Y)"

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⌉"

lemma p2r_neg_hom [simp]: "rel_ad ⌈P⌉ = ⌈λs. ¬P s⌉"

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)"
finally show ?thesis
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

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"

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

lemma wp_R2: "x ≤ R (wp x q) q"

lemma wp_R3: "d p ≤ wp x q ⟹ x ≤ R p q"

lemma H_R1: "H p (R p q) q"

lemma H_R2: "H p x q ⟹ x ≤ R p q"

lemma R_skip: "1 ≤ R p p"

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

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}"

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⌉"

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

lemma R_assignl: "(∀s. P s ⟶ P' (s (v := e s))) ⟹ (v ::= e) ; (rel_R ⌈P'⌉ ⌈Q⌉) ⊆ rel_R ⌈P⌉ ⌈Q⌉"

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"

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)"

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"

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"
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)"

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"

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"

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"

lemma H_seq_swap: "H p x r ⟹ H r y q ⟹ H p (x ⋅ y) q"

lemma H_seq: "H r y q ⟹ H p x r ⟹ H p (x ⋅ y) q"

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"
also have "... ⟷ t p ⋅ t r ⋅ x ⋅ n q + t p ⋅ n r ⋅ y ⋅ n q = 0"
also have "... ⟷ t p ⋅ t r ⋅ x ⋅ n q = 0 ∧ t p ⋅ n r ⋅ y ⋅ n q = 0"
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"

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"
also have "... ≤ x ⋅ t p ⋅ t r"
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⌉"

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⌉)"

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')"

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)"

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"

subsubsection‹Propositional Refinement Calculus›

lemma R_skip: "1 ≤ R p p"
proof -
have "H p 1 p"
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'"
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"
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"
hence "H p (if v then (R (t v ⋅ t p) q) else (R (n v ⋅ t p) q) fi) q"
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"
hence "H p (while q do (R (t p ⋅ t q) p) od) (t p ⋅ n q)"
thus ?thesis
by (rule R2)
qed

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

lemma R_one_zero: "R 1 0 = 0"
proof -
have "H 1 (R 1 0) 0"
thus ?thesis
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



(* 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›

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

lemma fbox_shunt: "d p ⋅ d q ≤ |x] t ⟷ d p ≤ ad q + |x] t"

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"

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"

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"
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)"

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))"
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"

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"
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"

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)"
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"
hence "d p ≤ |(d t ⋅ x)⇧⋆] p"
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)"
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⌉"

subsubsection ‹Simplifications›

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⌉"

lemma p2r_conj_hom_var_symm [simp]: "⌈P⌉ ; ⌈Q⌉ = ⌈P ⊓ Q⌉"

lemma p2r_neg_hom [simp]: "rel_ad ⌈P⌉ = ⌈- P⌉"

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')"

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⌉"

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


(* 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›

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


(* 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›

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


(* 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›

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.›

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"

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
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"
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


(* 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›

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


(* 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›

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"

lemma rel_nabla_bin_d_closed [simp]:  "rdom (rel_nabla_bin x q) = rel_nabla_bin x q"

lemma rel_nabla_unfold: "rel_nabla X ⊆ relfdia X (rel_nabla X)"

lemma rel_nabla_bin_unfold: "rel_nabla_bin X Q ⊆ relfdia X (rel_nabla_bin X Q) ∪ rdom Q"

lemma rel_nabla_coinduct_var: "P ⊆ relfdia X P ⟹ P ⊆ rel_nabla X"

lemma rel_nabla_bin_coinduct: "P ⊆ relfdia X P ∪ rdom Q ⟹ P ⊆ rel_nabla_bin X Q"

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"
finally show ?thesis
using rel_nabla_bin_coinduct by blast
qed

lemma fusion2_aux2: "rdom (rel_nabla_bin X Q) ⊆ rdom (rel_nabla_bin X Q ∩ rel_ad (relfdia (X⇧*) Q) ∪ relfdia (X⇧*) Q)"
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)"
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))"
hence "rdom (rel_nabla_bin X Q) ; rel_ad (relfdia (X⇧*) Q) ⊆ rdom (rel_nabla X)"
thus ?thesis
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)"
show "rdom y ⊆ relfdia x y ∪ rdom z ⟹ rdom y ⊆ rel_nabla x ∪ relfdia (x⇧*) z"
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 show ?thesis
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"

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"
by (metis a_antitone' a_subid addual.ars_r_def dpdz.domain_subid dual_order.trans)
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)"

lemma fdia_rel_im2: "s2r ((converse R)  (r2s (rdom P))) = relfdia R P"

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


(* 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›

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
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 p2r ("⌈_⌉")

notation ppath_aka.fbox ("wp")
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⌉"

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 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>
*)

theory Pointer_Examples

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


(* 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›

KAT_and_DRA.KAT
"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

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]

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 (subgoal_tac "rel_antidomain_kleene_algebra.t P = Id ∩ P")
apply (subgoal_tac "rel_antidomain_kleene_algebra.t Q = Id ∩ Q")
apply simp
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 (subgoal_tac "rel_antidomain_kleene_algebra.ads_d ⌈p⌉ = ⌈p⌉")
apply (subgoal_tac "rel_antidomain_kleene_algebra.ads_d ⌈q⌉ = ⌈q⌉")
apply simp
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"

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

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

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"
show "d bot = bot"
by (simp add: d_def inf.absorb1 inf.commute)
show "d (x ⊔ y) = d x ⊔ d y"
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" "(⋅)" "(⊓)" "(≤)" "(<)" "(⊔)" "⊥" "⊤"

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 ⋅ ⊤)"
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"

lemma da_a [simp]: "dblo.d (a x) = a x"

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" "⊥" "(≤)" "(<)"
proof -
show "class.antidomain_semiring a (⊔) (⋅) 1 ⊥ (≤) (<)"
by (standard, simp_all)
then interpret ad: antidomain_semiring a "(⊔)" "(⋅)" "1" "⊥" "(≤)" "(<)" .
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"
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}"

lemma star_def_var2: "star x = Sup{x ^ i |i. True}"

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}"
also have "... = x ^ 0 ⊔ Sup{y. ∃i. y = x ^ (i + 1)}"
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
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"
also have "... = x ^ 0 ⊔ Sup{y. ∃i. y = x ^ i ⋅ x}"
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
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"
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"
qed

lemma star_inductr': "z ⊔ y ⋅ x ≤ y ⟹ z ⋅ (star x) ≤ y"
proof -
assume "z ⊔ y ⋅ x ≤ y"
hence "∀i. z ⋅ x ^ i  ≤ y"
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"
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

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

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

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

lemma fbox_eq: "ad.fbox x q = Sup{d p |p. d p ⋅ x ≤ x ⋅ d q}"
apply (rule Sup_eqI[symmetric])
apply clarsimp
apply clarsimp

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

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)"
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
qed

lemma "d p ≤ ad.fbox x (d q) ⟹ x ≤ R p q"
apply (rule Sup_upper)
apply simp
done

end

subsection‹Relational Model of Boolean Domain Quantales›

interpretation rel_dbq: domain_boolean_quantale Inter Union "(∩)" "(⊆)" "(⊂)" "(∪)" "{}" UNIV minus uminus Id "(O)"
by blast +

subsection‹Modal Boolean Quantales›

class range_boolean_quantale = range_quantale + boolean_quantale

begin

subclass range_boolean_monoid

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

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)

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