```section ‹{Assert and Assume}›
theory RefineG_Assert
imports RefineG_Transfer
begin

definition "iASSERT return Φ ≡ if Φ then return () else top"
definition "iASSUME return Φ ≡ if Φ then return () else bot"

locale generic_Assert =
fixes bind ::
"('mu::complete_lattice) ⇒ (unit ⇒ ('ma::complete_lattice)) ⇒ 'ma"
fixes return :: "unit ⇒ 'mu"
fixes ASSERT
fixes ASSUME
assumes ibind_strict:
"bind bot f = bot"
"bind top f = top"
assumes imonad1: "bind (return u) f = f u"
assumes ASSERT_eq: "ASSERT ≡ iASSERT return"
assumes ASSUME_eq: "ASSUME ≡ iASSUME return"
begin
lemma ASSERT_simps[simp,code]:
"ASSERT True = return ()"
"ASSERT False = top"
unfolding ASSERT_eq iASSERT_def by auto

lemma ASSUME_simps[simp,code]:
"ASSUME True = return ()"
"ASSUME False = bot"
unfolding ASSUME_eq iASSUME_def by auto

lemma le_ASSERTI: "⟦ Φ ⟹ M≤M' ⟧ ⟹ M ≤ bind (ASSERT Φ) (λ_. M')"
apply (cases Φ) by (auto simp: ibind_strict imonad1)

lemma le_ASSERTI_pres: "⟦ Φ ⟹ M≤bind (ASSERT Φ) (λ_. M') ⟧
⟹ M ≤ bind (ASSERT Φ) (λ_. M')"
apply (cases Φ) by (auto simp: ibind_strict imonad1)

lemma ASSERT_leI: "⟦ Φ; Φ ⟹ M≤M' ⟧ ⟹ bind (ASSERT Φ) (λ_. M) ≤ M'"
apply (cases Φ) by (auto simp: ibind_strict imonad1)

lemma ASSUME_leI: "⟦ Φ ⟹ M≤M' ⟧ ⟹ bind (ASSUME Φ) (λ_. M) ≤ M'"
apply (cases Φ) by (auto simp: ibind_strict imonad1)
lemma ASSUME_leI_pres: "⟦ Φ ⟹ bind (ASSUME Φ) (λ_. M)≤M' ⟧
⟹ bind (ASSUME Φ) (λ_. M) ≤ M'"
apply (cases Φ) by (auto simp: ibind_strict imonad1)
lemma le_ASSUMEI: "⟦ Φ; Φ ⟹ M≤M' ⟧ ⟹ M ≤ bind (ASSUME Φ) (λ_. M')"
apply (cases Φ) by (auto simp: ibind_strict imonad1)

text ‹The order of these declarations does matter!›
lemmas [intro?] = ASSERT_leI le_ASSUMEI
lemmas [intro?] = le_ASSERTI ASSUME_leI

lemma ASSERT_le_iff:
"bind (ASSERT Φ) (λ_. S) ≤ S' ⟷ (S'≠top ⟶ Φ) ∧ S≤S'"
by (cases Φ) (auto simp: ibind_strict imonad1 simp: top_unique)

lemma ASSUME_le_iff:
"bind (ASSUME Φ) (λ_. S) ≤ S' ⟷ (Φ ⟶ S≤S')"
by (cases Φ) (auto simp: ibind_strict imonad1)

lemma le_ASSERT_iff:
"S ≤ bind (ASSERT Φ) (λ_. S') ⟷ (Φ ⟶ S≤S')"
by (cases Φ) (auto simp: ibind_strict imonad1)

lemma le_ASSUME_iff:
"S ≤ bind (ASSUME Φ) (λ_. S') ⟷ (S≠bot ⟶ Φ) ∧ S≤S'"
by (cases Φ) (auto simp: ibind_strict imonad1 simp: bot_unique)
end

text ‹
This locale transfer's asserts and assumes.
To remove them, use the next locale.
›
locale transfer_generic_Assert =
c: generic_Assert cbind creturn cASSERT cASSUME +
a: generic_Assert abind areturn aASSERT aASSUME +
ordered_transfer α
for cbind :: "('muc::complete_lattice)
⇒ (unit⇒'mac) ⇒ ('mac::complete_lattice)"
and creturn :: "unit ⇒ 'muc" and cASSERT and cASSUME
and abind :: "('mua::complete_lattice)
⇒ (unit⇒'maa) ⇒ ('maa::complete_lattice)"
and areturn :: "unit ⇒ 'mua" and aASSERT and aASSUME
and α :: "'mac ⇒ 'maa"
begin
lemma transfer_ASSERT[refine_transfer]:
"⟦Φ ⟹ α M ≤ M'⟧
⟹ α (cbind (cASSERT Φ) (λ_. M)) ≤ (abind (aASSERT Φ) (λ_. M'))"
apply (cases Φ)
done

lemma transfer_ASSUME[refine_transfer]:
"⟦Φ; Φ ⟹ α M ≤ M'⟧
⟹ α (cbind (cASSUME Φ) (λ_. M)) ≤ (abind (aASSUME Φ) (λ_. M'))"
done

end

locale transfer_generic_Assert_remove =
a: generic_Assert abind areturn aASSERT aASSUME +
transfer α
for abind :: "('mua::complete_lattice)
⇒ (unit⇒'maa) ⇒ ('maa::complete_lattice)"
and areturn :: "unit ⇒ 'mua" and aASSERT and aASSUME
and α :: "'mac ⇒ 'maa"
begin
lemma transfer_ASSERT_remove[refine_transfer]:
"⟦ Φ ⟹ α M ≤ M' ⟧ ⟹ α M ≤ abind (aASSERT Φ) (λ_. M')"
by (rule a.le_ASSERTI)

lemma transfer_ASSUME_remove[refine_transfer]:
"⟦ Φ; Φ ⟹ α M ≤ M' ⟧ ⟹ α M ≤ abind (aASSUME Φ) (λ_. M')"
by (rule a.le_ASSUMEI)
end

end
```