# Theory Statements

Up to index of Isabelle/HOL/LatticeProperties/MonoBoolTranAlgebra

theory Statements
imports Assertion_Algebra
header {* Program statements, Hoare and refinement rules *}

theory Statements
imports Assertion_Algebra
begin

text {*In this section we introduce assume, if, and while program statements
as well as Hoare triples, and data refienment. We prove Hoare correctness
rules for the program statements and we prove some theorems linking Hoare
correctness statement to (data) refinement. Most of the theorems assume
a monotonic boolean transformers algebra. The theorem stating the
equivalence between a Hoare
correctness triple and a refinement statement holds under the
assumption that we have a monotonic boolean transformers algebra with
post condition statement.*}

definition
"assume" :: "'a::mbt_algebra Assertion => 'a" ("[· _ ]" [0] 1000) where
"[·p] = {·p} ^ o"

lemma [simp]: "{·p} * \<top> \<sqinter> [·p] = {·p}"
apply (subgoal_tac "{·p} ∈ assertion")
apply (subst (asm) assertion_def, simp add: assume_def)
by simp

lemma [simp]: "[·p] * x \<squnion> {·-p} * \<top> = [·p] * x"

lemma [simp]: "{·p} * \<top> \<squnion> [·-p] * x = [·-p] * x"

lemma assert_sup: "{·p \<squnion> q} = {·p} \<squnion> {·q}"

lemma assert_inf: "{·p \<sqinter> q} = {·p} \<sqinter> {·q}"

lemma assert_neg: "{·-p} = neg_assert {·p}"

lemma assert_false [simp]: "{·⊥} = ⊥"

lemma if_Assertion_assumption: "({·p} * x) \<squnion> ({·-p} * y) = ([·p] * x) \<sqinter> ([·-p] * y)"
proof -
have "({·p} * x) \<squnion> {·-p} * y = ({·p} * \<top> \<sqinter> [·p]) * x \<squnion> ({·-p} * \<top> \<sqinter> [·-p]) * y" by simp
also have "… = ({·p} * \<top> \<sqinter> ([·p] * x)) \<squnion> ({·-p} * \<top> \<sqinter> ([·-p] * y))" by (unfold inf_comp, simp)
also have "… = (({·p} * \<top> \<sqinter> ([·p] * x)) \<squnion> ({·-p} * \<top>)) \<sqinter> (({·p} * \<top> \<sqinter> ([·p] * x)) \<squnion> ([·-p] * y))" by (simp add: sup_inf_distrib)
also have "… = (({·p} * \<top> \<squnion> ({·-p} * \<top>)) \<sqinter> (([·p] * x))) \<sqinter> (([·-p] * y) \<sqinter> (([·p] * x) \<squnion> ([·-p] * y)))"
also have "… = ([·p] * x) \<sqinter> ([·-p] * y) \<sqinter> (([·p] * x) \<squnion> ([·-p] * y))"
apply (simp add: sup_comp [THEN sym] )
by (simp add: assert_sup [THEN sym] inf_assoc sup_compl_top)
also have "… = ([·p] * x) \<sqinter> ([·-p] * y)"
by (rule antisym, simp_all add: inf_assoc)
finally show ?thesis .
qed

definition
"wp x p = abs_wpt (x * {·p})"

lemma wp_assume: "wp [·p] q = -p \<squnion> q"
apply (rule assert_injective)
apply simp
by (simp add: assert_sup assert_neg assume_def wpt_dual_assertion_comp)

lemma assert_commute: "y ∈ conjunctive ==> y * {·p} = {· wp y p } * y"
by (rule assertion_commute, simp_all)

lemma wp_assert: "wp {·p} q = p \<sqinter> q"
by (simp add: wp_def assertion_inf_comp_eq [THEN sym] assert_inf [THEN sym])

lemma wp_mono [simp]: "mono (wp x)"
apply (simp add: le_fun_def wp_def abs_wpt_def less_eq_Assertion_def mono_def)
apply (rule_tac y = " x * {· xa } * \<top>" in order_trans, simp_all)
apply (rule le_comp_right)
by (rule le_comp, simp)

lemma wp_mono2: "p ≤ q ==> wp x p ≤ wp x q"
apply (cut_tac x = x in wp_mono)
apply (unfold mono_def)
by blast

lemma wp_fun_mono [simp]: "mono wp"
apply (simp add: le_fun_def wp_def abs_wpt_def less_eq_Assertion_def mono_def)
apply (rule_tac y = " x * {· xa } * \<top>" in order_trans, simp_all)
apply (rule le_comp_right)
by (rule le_comp_right, simp)

lemma wp_fun_mono2: "x ≤ y ==> wp x p ≤ wp y p"
apply (cut_tac wp_fun_mono)
apply (unfold mono_def)
by blast

lemma wp_comp: "wp (x * y) p = wp x (wp y p)"
by (unfold wpt_comp_2 [THEN sym] mult_assoc, simp)

lemma wp_choice: "wp (x \<sqinter> y) = wp x \<sqinter> wp y"
apply (simp add: fun_eq_iff wp_def inf_fun_def inf_comp inf_Assertion_def abs_wpt_def)

lemma [simp]: "wp 1 = id"
apply (unfold fun_eq_iff, safe)
apply (rule assert_injective)

lemma wp_omega_fix: "wp (x ^ ω) p = wp x (wp (x ^ ω) p) \<sqinter> p"
apply (subst omega_fix)

lemma wp_omega_least: "(wp x r) \<sqinter> p ≤ r ==> wp (x ^ ω) p ≤ r"
apply (simp add: wp_def abs_wpt_def inf_Assertion_def less_eq_Assertion_def)
apply (rule_tac y = "{·r} * \<top> \<sqinter> 1" in order_trans)
apply simp
apply (rule_tac y = "x ^ ω * {· p } * \<top>" in order_trans, simp)
apply (rule omega_least)
apply (drule_tac z = \<top> in le_comp_right)
apply (simp add: inf_comp mult_assoc [THEN sym])

lemma Assertion_wp: "{·wp x p} = (x * {·p} * \<top>) \<sqinter> 1"

definition
"hoare p S q = (p ≤ wp S q)"

definition
"grd x = - (wp x ⊥)"

lemma grd_comp: "[·grd x] * x = x"
apply (simp add: grd_def wp_def uminus_Assertion_def assume_def neg_assert_def abs_wpt_def dual_sup sup_comp)
apply (simp add: wpt_def dual_inf sup_comp dual_comp bot_Assertion_def)
by (rule antisym, simp_all)

lemma assert_assume: "{·p} * [·p] = {· p}"

lemma dual_assume: "[·p] ^ o = {·p}"

lemma assume_prop: "([·p] * ⊥) \<squnion> 1 = [·p]"

text{*An alternative definition of a Hoare triple*}

definition "hoare1 p S q = ([· p ] * S * [· -q ] = \<top>)"

lemma "hoare1 p S q = hoare p S q"
apply (simp add: hoare1_def dual_inf dual_comp)
apply (simp add: hoare_def wp_def less_eq_Assertion_def abs_wpt_def)
apply safe
proof -
assume A: "[· p ] * S * [· - q ] = \<top>"
have "{·p} ≤ {·p} * \<top>" by simp
also have "... ≤ {·p} * \<top> * ⊥" by (unfold mult_assoc, simp)
also have "... = {·p} * [· p ] * S * [· - q ] * ⊥" by (subst A [THEN sym], simp add: mult_assoc)
also have "... = {·p} * S * [· - q ] * ⊥" by (simp add: assert_assume)
also have "... ≤ {·p} * S * {· q } * \<top>"
apply (rule le_comp, rule le_comp)
by (simp add: neg_assert_def dual_inf dual_comp sup_comp)
also have "... ≤ S * {· q } * \<top>" by (simp add: mult_assoc)
finally show "{·p} ≤ S * {· q } * \<top>" .
next
assume A: "{· p } ≤ S * {· q } * \<top>"
have "\<top> = ((S * {·q}) ^ o) * ⊥ \<squnion> S * {·q} * \<top>" by simp
also have "… ≤ [·p] * ⊥ \<squnion> S * {·q} * \<top>"
apply (simp del: dual_neg_top)
apply (rule_tac y = "[·p] * ⊥" in order_trans, simp_all)
apply (subst dual_le)
apply (cut_tac x = "{·p}" and y = "S * {·q} * \<top>" and z = \<top> in le_comp_right)
apply (rule A)
also have "… = [·p] * S * ({·q} * \<top>)"
apply (subst (2) assume_prop [THEN sym])
also have "… ≤ [·p] * S * ({·q} * \<top> \<squnion> 1)"
by (rule le_comp, simp)
also have "… = [·p] * S * [·-q]"
by (simp add: neg_assert_def dual_inf dual_comp)
finally show "[·p] * S * [· - q] = \<top>"
by (rule_tac antisym, simp_all)
qed

lemma hoare_choice: "hoare p (x \<sqinter> y) q = ((hoare p) x q & (hoare p y q))"
apply (unfold hoare_def wp_choice inf_fun_def)
by auto

definition
if_stm:: "'a::mbt_algebra Assertion => 'a => 'a => 'a" ("(If (_)/ then (_)/ else (_))" [0, 0, 10] 10) where
"if_stm b x y = (([· b ] * x) \<sqinter> ([· -b ] * y))"

lemma if_assertion: "(If p then x else y) = {·p} * x \<squnion> {· -p} * y"

lemma (in boolean_algebra) sup_neg_inf:
"(p ≤ q \<squnion> r) = (p \<sqinter> -q ≤ r)"
apply (safe)
apply(cut_tac a = p and c = "q \<squnion> r" and b = "-q" and d = "-q" in inf_mono)
apply simp apply simp apply (simp add: inf_sup_distrib2 inf_compl_bot)
apply(cut_tac b = "p \<sqinter> - q" and d = "r" and a = "q" and c = "q" in sup_mono)
apply simp apply simp by (simp add: sup_inf_distrib sup_compl_top)

lemma hoare_if: "hoare p (If b then x else y) q = (hoare (p \<sqinter> b) x q ∧ hoare (p \<sqinter> -b) y q)"
by (simp add: hoare_def if_stm_def wp_choice inf_fun_def wp_comp wp_assume sup_neg_inf)

lemma hoare_comp: "hoare p (x * y) q = (∃ r . (hoare p x r) ∧ (hoare r y q))"
apply safe
apply (rule_tac x = "wp y q" in exI, simp)
apply (rule_tac y = "wp x r" in order_trans, simp)
apply (rule_tac f = "wp x" in monoD)
by simp_all

lemma hoare_refinement: "hoare p S q = ({·p} * (post {·q}) ≤ S)"
apply (simp add: hoare_def less_eq_Assertion_def Assertion_wp)
proof
assume A: "{·p} ≤ S * {·q} * \<top>"
have "{·p} * post {·q} = ({·p} * \<top> \<sqinter> 1) * post {·q}" by (simp add: assertion_prop)
also have "… = {·p} * \<top> \<sqinter> post {·q}" by (simp add: inf_comp)
also have "… ≤ S * {·q} * \<top> \<sqinter> post {·q}" apply simp
apply (rule_tac y = "{·p} * \<top>" in order_trans, simp_all)
apply (cut_tac x = "{·p}" and y = "S * {·q} * \<top>" and z = \<top> in le_comp_right)
by (rule A, simp)
also have "… ≤ S" by (simp add: post_2)
finally show "{·p} * post {·q} ≤ S".
next
assume A: "{·p} * post {·q} ≤ S"
have "{·p} = {·p} * \<top> \<sqinter> 1" by (simp add: assertion_prop)
also have "… = {·p} * ((post {·q}) * {·q} * \<top>) \<sqinter> 1" by (simp add: post_1)
also have "… ≤ {·p} * ((post {·q}) * {·q} * \<top>)" by simp
also have "… ≤ S * {·q} * \<top>"
apply (cut_tac x = "{·p} * post {·q}" and y = S and z = "{·q} * \<top>" in le_comp_right)
finally show "{·p} ≤ S * {·q} * \<top>" .
qed

theorem hoare_fixpoint_mbt:
"F x = x
==> (!! (w::'a::well_founded) f . (!!v. v < w ==> hoare (p v) f q) ==> hoare (p w) (F f) q)
==> hoare (p u) x q"

apply (rule less_induct1)
proof -
fix xa
assume A: "!! w f. (!! v . v < w ==> hoare (p v) f q) ==> hoare (p w) (F f) q"
assume B: "F x = x"
assume C: "!!y . y < xa ==> hoare (p y) x q"
have D: "hoare (p xa) (F x) q"
apply (rule A)
by (rule C, simp)
show "hoare (p xa) x q"
by (cut_tac D, simp add: B)
qed

lemma hoare_Sup: "hoare (Sup P) x q = (∀ p ∈ P . hoare p x q)"
apply auto
apply (rule_tac y = "Sup P" in order_trans, simp_all add: Sup_upper)
apply (rule Sup_least)
by simp

theorem hoare_fixpoint_complete_mbt:
"F x = x
==> (!! w f . hoare (Sup_less p w) f q ==> hoare (p w) (F f) q)
==> hoare (Sup (range p)) x q"

apply (simp add: hoare_Sup Sup_less_def, safe)
apply (rule_tac F = F in hoare_fixpoint_mbt)
by auto

definition
while:: "'a::mbt_algebra Assertion => 'a => 'a" ("(While (_)/ do (_))" [0, 10] 10) where
"while p x = ([· p] * x) ^ ω * [· -p ]"

lemma while_false: "(While ⊥ do x) = 1"
apply (unfold while_def)
apply (subst omega_fix)

lemma while_true: "(While \<top> do 1) = ⊥"
apply (unfold while_def)
by (rule antisym, simp_all add: assume_def)

lemma hoare_wp [simp]: "hoare (wp x q) x q"

lemma hoare_comp_wp: "hoare p (x * y) q = hoare p x (wp y q)"
apply (unfold hoare_comp, safe)
apply (rule_tac y = "wp x r" in order_trans, simp)
apply (rule wp_mono2, simp)
by (rule_tac x = "wp y q" in exI, simp)

lemma (in mbt_algebra) hoare_assume: "hoare p [·b] q = (p \<sqinter> b ≤ q)"
by (simp add: hoare_def wp_assume sup_neg_inf)

lemma (in mbt_algebra) hoare_assume_comp: "hoare p ([·b] * x) q = hoare (p \<sqinter> b) x q"

lemma hoare_while_mbt:
"(∀ (w::'b::well_founded) r . (∀ v . v < w --> p v ≤ r) --> hoare ((p w) \<sqinter> b) x r) ==>
(∀ u . p u ≤ q) ==> hoare (p w) (While b do x) (q \<sqinter> -b)"

apply (unfold while_def)
apply (rule_tac F = "λz. [· b ] * x * z \<sqinter> [· - b ]" in hoare_fixpoint_mbt)
apply (simp add: mult_assoc [THEN sym])
apply (unfold hoare_choice)
apply safe
apply (subst hoare_comp_wp)
apply (subst hoare_assume_comp)
apply (drule_tac x = w in spec)
apply (drule_tac x = "wp f (q \<sqinter> - b)" in spec)
apply (auto simp add: hoare_def) [1]
apply (rule_tac y = "p w" in order_trans)
by simp_all

lemma hoare_while_complete_mbt:
"(∀ w::'b::well_founded . hoare ((p w) \<sqinter> b) x (Sup_less p w)) ==>
hoare (Sup (range p)) (While b do x) ((Sup (range p)) \<sqinter> -b)"

apply (rule hoare_while_mbt)
apply safe
apply (drule_tac x = w in spec)
apply (rule_tac y = "wp x (Sup_less p w)" in order_trans, simp_all)
apply (rule wp_mono2)
apply (rule Sup_least, auto)
by (rule Sup_upper, simp)

definition
"datarefin S S1 D D1 = (D * S ≤ S1 * D1)"

lemma "hoare p S q ==> datarefin S S1 D D1 ==> hoare (wp D p) S1 (wp D1 q)"
apply (simp add: wp_comp [THEN sym] mult_assoc [THEN sym])
apply (rule_tac y = "wp (D * S) q" in order_trans)
apply (subst wp_comp)
apply (rule monoD, simp_all)
by (rule wp_fun_mono2, simp_all)

lemma "hoare p S q ==> datarefin ({·p} * S) S1 D D1 ==> hoare (wp D p) S1 (wp D1 q)"
apply (rule_tac y = "wp (D * {·p} * S) q" in order_trans)
apply (subst wp_comp)
apply (rule monoD, simp_all)
apply (subst wp_comp)
apply (unfold wp_assert, simp)
apply (unfold wp_comp [THEN sym])
apply (rule wp_fun_mono2)

lemma inf_pres_conj: "x ∈ conjunctive ==> y ∈ conjunctive ==> x \<sqinter> y ∈ conjunctive"
apply (subst conjunctive_def, safe)
by (metis (hide_lams, no_types) inf_assoc inf_left_commute)

lemma sup_pres_disj: "x ∈ disjunctive ==> y ∈ disjunctive ==> x \<squnion> y ∈ disjunctive"
apply (subst disjunctive_def, safe)
by (metis (hide_lams, no_types) sup_assoc sup_left_commute)

lemma assumption_conjuncive [simp]: "[·p] ∈ conjunctive"
by (simp add: assume_def dual_disjunctive assertion_disjunctive)

lemma assumption_disjuncive [simp]: "[·p] ∈ disjunctive"
by (simp add: assume_def dual_conjunctive assertion_conjunctive)

lemma if_pres_conj: "x ∈ conjunctive ==> y ∈ conjunctive ==> (If p then x else y) ∈ conjunctive"
apply (unfold if_stm_def)

lemma if_pres_disj: "x ∈ disjunctive ==> y ∈ disjunctive ==> (If p then x else y) ∈ disjunctive"
apply (unfold if_assertion)
by (simp add: sup_pres_disj comp_pres_disj assertion_disjunctive)

lemma while_dual_star: "(While p do (x::'a::mbt_algebra)) = (({· p} * x)^⊗ * {· -p })"
apply (rule antisym)
apply (rule omega_least)
proof -
have "([· p] * x * (({· p} * x)^⊗ * {·-p}) \<sqinter> [·-p]) = ({· p} * x * (({· p} * x)^⊗ * {·-p})) \<squnion> {·-p}"
apply (unfold mult_assoc)
by (cut_tac p = p and x = "(x * (({· p } * x)^⊗ * {· -p }))" and y = 1 in if_Assertion_assumption, simp)
also have "… = ({· p} * x)^⊗ * {·-p}"
finally show "[· p ] * x * (({· p } * x)^⊗ * {· - p }) \<sqinter> [· - p ] ≤ ({· p } * x)^⊗ * {· - p }" by simp
next
show "({· p } * x)^⊗ * {· - p } ≤ ([· p ] * x) ^ ω * [· - p ]"
apply (rule dual_star_least)
proof -
have "{· p } * x * (([· p ] * x) ^ ω * [· - p ]) \<squnion> {· - p } = [· p ] * x * (([· p ] * x) ^ ω * [· - p ]) \<sqinter> [· - p ]"
apply (unfold mult_assoc)
by (cut_tac p = p and x = "(x * (([·p] * x)^ω * [·-p]))" and y = 1 in if_Assertion_assumption, simp)
also have "... = ([· p ] * x) ^ ω * [· - p ]"
apply (simp add: mult_assoc [THEN sym])
by (metis omega_comp_fix)
finally show "{· p } * x * (([· p ] * x) ^ ω * [· - p ]) \<squnion> {· - p } ≤ ([· p ] * x) ^ ω * [· - p ] " by simp
qed
qed

lemma while_pres_disj: "(x::'a::mbt_algebra) ∈ disjunctive ==> (While p do x) ∈ disjunctive"
apply (unfold while_dual_star)
apply (rule comp_pres_disj)
apply (rule dual_star_pres_disj)
by (rule comp_pres_disj, simp_all add: assertion_disjunctive)

lemma while_pres_conj: "(x::'a::mbt_algebra_fusion) ∈ conjunctive ==> (While p do x) ∈ conjunctive"
apply(unfold while_def)