Theory Statements

section ‹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} * ⊤ ⊓ [⋅p] = {⋅p}"
  apply (subgoal_tac "{⋅p} ∈ assertion")
  apply (subst (asm) assertion_def, simp add: assume_def)
  by simp

lemma [simp]: "[⋅p] * x ⊔ {⋅-p} * ⊤ = [⋅p] * x"
  by (simp add: assume_def  uminus_Assertion_def)

lemma [simp]: "{⋅p} * ⊤ ⊔ [⋅-p] * x = [⋅-p] * x"
  by (simp add: assume_def  uminus_Assertion_def)

lemma assert_sup: "{⋅p ⊔ q} = {⋅p} ⊔ {⋅q}"
  by (simp add: sup_Assertion_def)

lemma assert_inf: "{⋅p ⊓ q} = {⋅p} ⊓ {⋅q}"
  by (simp add: inf_Assertion_def)

lemma assert_neg: "{⋅-p} = neg_assert {⋅p}"
  by (simp add: uminus_Assertion_def)

lemma assert_false [simp]: "{⋅⊥} = ⊥"
  by (simp add: bot_Assertion_def)

lemma if_Assertion_assumption: "({⋅p} * x) ⊔ ({⋅-p} * y) = ([⋅p] * x) ⊓ ([⋅-p] * y)"
proof -
    have "({⋅p} * x) ⊔ {⋅-p} * y = ({⋅p} * ⊤ ⊓ [⋅p]) * x ⊔ ({⋅-p} * ⊤ ⊓ [⋅-p]) * y" by simp
    also have "… = ({⋅p} * ⊤ ⊓ ([⋅p] * x)) ⊔ ({⋅-p} * ⊤ ⊓ ([⋅-p] * y))" by (unfold inf_comp, simp)
    also have "… = (({⋅p} * ⊤ ⊓ ([⋅p] * x)) ⊔ ({⋅-p} * ⊤)) ⊓ (({⋅p} * ⊤ ⊓ ([⋅p] * x)) ⊔ ([⋅-p] * y))" by (simp add: sup_inf_distrib)
    also have "… = (({⋅p} * ⊤  ⊔ ({⋅-p} * ⊤)) ⊓ (([⋅p] * x))) ⊓ (([⋅-p] * y) ⊓ (([⋅p] * x) ⊔ ([⋅-p] * y)))"
      by (simp add: sup_inf_distrib2)
    also have "… = ([⋅p] * x) ⊓  ([⋅-p] * y) ⊓ (([⋅p] * x) ⊔ ([⋅-p] * y))"
      apply (simp add: sup_comp [THEN sym] )
      by (simp add: assert_sup [THEN sym] inf_assoc)
    also have "… = ([⋅p] * x) ⊓  ([⋅-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 ⊔ q"
  apply (simp add: wp_def abs_wpt_def)
  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"
  apply (simp add: wp_def abs_wpt_def)
  by (rule assertion_commute, simp_all)

lemma wp_assert: "wp {⋅p} q = p ⊓ 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 (simp add: wpt_def, safe)
  apply (rule_tac y = " x * {⋅ xa } * ⊤" 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 (simp add: wpt_def, safe)
  apply (rule_tac y = " x * {⋅ xa } * ⊤" 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)
  apply (simp add: le_fun_def)
  by blast


lemma wp_comp: "wp (x * y) p = wp x (wp y p)"
  apply (simp add: wp_def abs_wpt_def)
  by (unfold wpt_comp_2 [THEN sym] mult.assoc, simp)

lemma wp_choice: "wp (x ⊓ y) = wp x ⊓ wp y"
  apply (simp add: fun_eq_iff wp_def inf_fun_def inf_comp inf_Assertion_def abs_wpt_def)
  by (simp add: wpt_choice)

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

lemma wp_omega_fix: "wp (x ^ ω) p = wp x (wp (x ^ ω) p) ⊓ p"
  apply (subst omega_fix)
  by (simp add: wp_choice wp_comp)

lemma wp_omega_least: "(wp x r) ⊓ p ≤ r ⟹ wp (x ^ ω) p ≤ r"
  apply (simp add: wp_def abs_wpt_def inf_Assertion_def less_eq_Assertion_def)
  apply (simp add: wpt_def)
  apply (rule_tac y = "{⋅r} * ⊤ ⊓ 1" in order_trans)
  apply simp
  apply (rule_tac y = "x ^ ω * {⋅ p } * ⊤" in order_trans, simp)
  apply (simp add: mult.assoc)
  apply (rule omega_least)
  apply (drule_tac z = ⊤ in le_comp_right)
  apply (simp add: inf_comp mult.assoc [THEN sym])
  by (simp add: assertion_prop)

lemma Assertion_wp: "{⋅wp x p} = (x * {⋅p} * ⊤) ⊓ 1"
  apply (simp add: wp_def abs_wpt_def)
  by (simp add: wpt_def)

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}"
  by (simp add: assume_def)

lemma dual_assume: "[⋅p] ^ o = {⋅p}"
  by (simp add: assume_def)

lemma assume_prop: "([⋅p] * ⊥) ⊔ 1 = [⋅p]"
  by (simp add: assume_def dual_assertion_prop)

text‹An alternative definition of a Hoare triple›

definition "hoare1 p S q = ([⋅ p ] * S * [⋅ -q ] = ⊤)"

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 (simp add: wpt_def)
  apply safe
  proof -
    assume A: "[⋅ p ] * S * [⋅ - q ] = ⊤"
    have "{⋅p} ≤ {⋅p} * ⊤" by simp
    also have "... ≤ {⋅p} * ⊤ * ⊥" 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 } * ⊤"
      apply (simp add: mult.assoc)
      apply (rule le_comp, rule le_comp)
      apply (simp add: assume_def uminus_Assertion_def)
      by (simp add: neg_assert_def dual_inf dual_comp sup_comp)
    also have "... ≤ S * {⋅ q } * ⊤" by (simp add: mult.assoc)
    finally show "{⋅p} ≤ S * {⋅ q } * ⊤" .
  next
    assume A: "{⋅ p } ≤ S * {⋅ q } * ⊤"
    have "⊤ = ((S * {⋅q}) ^ o) * ⊥ ⊔ S * {⋅q} * ⊤" by simp
    also have "… ≤ [⋅p] * ⊥ ⊔ S * {⋅q} * ⊤"
      apply (simp del: dual_neg_top)
      apply (rule_tac y = "[⋅p] * ⊥" in order_trans, simp_all)
      apply (subst dual_le)
      apply (simp add: dual_comp dual_assume)
      apply (cut_tac x = "{⋅p}" and y = "S * {⋅q} * ⊤" and z = ⊤ in le_comp_right)
      apply (rule A)
      by (simp add: mult.assoc)
    also have "… = [⋅p] * S * ({⋅q} * ⊤)"
      apply (subst (2) assume_prop [THEN sym])
      by (simp_all add: sup_comp mult.assoc)
    also have "… ≤ [⋅p] * S * ({⋅q} * ⊤ ⊔ 1)"
      by (rule le_comp, simp)
    also have "… = [⋅p] * S * [⋅-q]"
      apply (simp add: assume_def uminus_Assertion_def)
      by (simp add: neg_assert_def dual_inf dual_comp)
    finally show "[⋅p] * S * [⋅ - q] = ⊤"
      by (rule_tac antisym, simp_all)
  qed

lemma hoare_choice: "hoare p (x ⊓ 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) ⊓ ([⋅ -b ] * y))"

lemma if_assertion: "(If p then x else y) = {⋅p} * x ⊔ {⋅ -p} * y"
  by (simp add: if_stm_def if_Assertion_assumption)

lemma hoare_if: "hoare p (If b then x else y) q = (hoare (p ⊓ b) x q ∧ hoare (p ⊓ -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 (simp add: hoare_def wp_comp)
   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} * ⊤"
    have "{⋅p} * post {⋅q} = ({⋅p} * ⊤ ⊓ 1) * post {⋅q}" by (simp add: assertion_prop)
    also have "… = {⋅p} * ⊤ ⊓ post {⋅q}" by (simp add: inf_comp)
    also have "… ≤ S * {⋅q} * ⊤ ⊓ post {⋅q}" apply simp
      apply (rule_tac y = "{⋅p} * ⊤" in order_trans, simp_all)
      apply (cut_tac x = "{⋅p}" and y = "S * {⋅q} * ⊤" and z = ⊤ 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} * ⊤ ⊓ 1" by (simp add: assertion_prop)
    also have "… = {⋅p} * ((post {⋅q}) * {⋅q} * ⊤) ⊓ 1" by (simp add: post_1)
    also have "… ≤ {⋅p} * ((post {⋅q}) * {⋅q} * ⊤)" by simp
    also have "… ≤ S * {⋅q} * ⊤" 
      apply (cut_tac x = "{⋅p} * post {⋅q}" and y = S and z = "{⋅q} * ⊤" in le_comp_right)
      apply (simp add: A)
      by (simp add: mult.assoc)
    finally show "{⋅p} ≤ S * {⋅q} * ⊤" .
  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 (simp add: hoare_def)
  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)
  by (simp_all add: assume_def)

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

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

lemma hoare_comp_wp: "hoare p (x * y) q = hoare p x (wp y q)"
  apply (unfold hoare_comp, safe)
  apply (simp add: hoare_def)
  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 ⊓ 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 ⊓ b) x q"
  apply (simp add: hoare_comp_wp hoare_assume)
  by (simp add: hoare_def)

lemma hoare_while_mbt:
  "(∀ (w::'b::well_founded) r . (∀ v . v < w ⟶ p v ≤ r) ⟶ hoare ((p w) ⊓ b) x r) ⟹ 
       (∀ u . p u ≤ q) ⟹ hoare  (p w) (While b do x) (q ⊓ -b)"
  apply (unfold while_def)
  apply (rule_tac F = "λz. [⋅ b ] * x * z ⊓ [⋅ - b ]" in hoare_fixpoint_mbt)
  apply (simp add: mult.assoc [THEN sym])
  apply (simp add: omega_comp_fix)
  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 ⊓ - b)" in spec)
  apply (auto simp add: hoare_def) [1]
  apply (auto simp add: hoare_assume)
  apply (rule_tac y = "p w" in order_trans)
  by simp_all

lemma hoare_while_complete_mbt:
  "(∀ w::'b::well_founded . hoare ((p w) ⊓ b) x (Sup_less p w)) ⟹ 
       hoare  (Sup (range p)) (While b do x) ((Sup (range p)) ⊓ -b)"
  apply (simp add: hoare_Sup, safe)
  apply (rule hoare_while_mbt)
  apply safe
  apply (drule_tac x = w in spec)
  apply (simp add: hoare_def)
  apply (rule_tac y = "wp x (Sup_less p w)" in order_trans, simp_all)
  apply (rule wp_mono2)
  apply (simp add: Sup_less_def)
  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: hoare_def datarefin_def)
  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 (simp add: hoare_def datarefin_def)
  apply (rule_tac y = "wp (D * {⋅p} * S) q" in order_trans)
  apply (simp add: mult.assoc)
  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)
  by (simp add: mult.assoc)

lemma inf_pres_conj: "x ∈ conjunctive ⟹ y ∈ conjunctive ⟹ x ⊓ y ∈ conjunctive"
  apply (subst conjunctive_def, safe)
  apply (simp add: inf_comp conjunctiveD)
  by (metis (opaque_lifting, no_types) inf_assoc inf_left_commute)

lemma sup_pres_disj: "x ∈ disjunctive ⟹ y ∈ disjunctive ⟹ x ⊔ y ∈ disjunctive"
  apply (subst disjunctive_def, safe)
  apply (simp add: sup_comp disjunctiveD)
  by (metis (opaque_lifting, 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)
  by (simp add: inf_pres_conj comp_pres_conj)

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 (simp add: while_def)
  apply (rule antisym)
  apply (rule omega_least)
   proof -
     have "([⋅ p] * x * (({⋅ p} * x)^⊗ * {⋅-p}) ⊓ [⋅-p]) = ({⋅ p} * x * (({⋅ p} * x)^⊗ * {⋅-p})) ⊔ {⋅-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}"
        by (simp add: mult.assoc [THEN sym], simp add: dual_star_comp_fix [THEN sym])
     finally show "[⋅ p ] * x * (({⋅ p } * x)^⊗ * {⋅ - p }) ⊓ [⋅ - 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 ]) ⊔ {⋅ - p } = [⋅ p ] * x * (([⋅ p ] * x) ^ ω * [⋅ - p ]) ⊓ [⋅ - 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 ]) ⊔ {⋅ - 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)
  by (simp add: comp_pres_conj omega_pres_conj)

unbundle no lattice_syntax

end