# Theory MonoBoolTranAlgebra.Assertion_Algebra

```section ‹Boolean Algebra of Assertions›

theory  Assertion_Algebra
imports Mono_Bool_Tran_Algebra
begin

text‹
This section introduces the boolean algebra of assertions. The
type \$\mathsf{Assertion}\$ and the boolean operation are instroduced
based on the set \$\mathsf{assertion}\$ and the operations on the monotonic
boolean transformers algebra. The type \$\mathsf{Assertion}\$ over
a complete monotonic boolean transformers algebra is a complete boolean
algebra.
›

typedef (overloaded) ('a::mbt_algebra) Assertion = "assertion::'a set"
apply (rule_tac x = "⊥" in exI)
by (unfold assertion_def, simp)

definition
assert :: "'a::mbt_algebra Assertion ⇒ 'a"  ("{⋅ _ }" [0] 1000) where
"{⋅p} =  Rep_Assertion p"

definition
"abs_wpt x = Abs_Assertion (wpt x)"

lemma [simp]: "{⋅p} ∈ assertion"
by (unfold assert_def, cut_tac x = p in Rep_Assertion, simp)

lemma [simp]: "abs_wpt ({⋅p}) = p"

lemma [simp]: "x ∈ assertion ⟹ {⋅Abs_Assertion x} = x"
by (rule Abs_Assertion_inverse, simp)

lemma [simp]: "x ∈ assertion ⟹ {⋅abs_wpt x} = x"
by (rule Abs_Assertion_inverse, simp)

lemma assert_injective: "{⋅p} = {⋅q} ⟹ p = q"
proof -
assume A: "{⋅ p } = {⋅ q } "
have "p = abs_wpt ({⋅p})" by simp
also have "... = q" by (subst A, simp)
finally show ?thesis .
qed

instantiation Assertion :: (mbt_algebra) boolean_algebra
begin
definition
uminus_Assertion_def: "- p = abs_wpt(neg_assert {⋅p})"

definition
bot_Assertion_def: "⊥ = abs_wpt ⊥"

definition
top_Assertion_def: "⊤ = abs_wpt 1"

definition
inf_Assertion_def: "p ⊓ q = abs_wpt ({⋅p} ⊓ {⋅q})"

definition
sup_Assertion_def: "p ⊔ q = abs_wpt ({⋅p} ⊔ {⋅q})"

definition
less_eq_Assertion_def: "(p ≤ q) = ({⋅p} ≤  {⋅q})"

definition
less_Assertion_def: "(p < q) = ({⋅p} < {⋅q})"

definition
minus_Assertion_def: "(p::'a Assertion) - q = p ⊓ - q"

instance
proof
fix x y :: "'a Assertion" show "(x < y) = (x ≤ y ∧ ¬ y ≤ x)"
by (simp add: less_Assertion_def less_eq_Assertion_def less_le_not_le)
next
fix x ::"'a Assertion" show "x ≤ x" by (simp add: less_eq_Assertion_def)
next
fix x y z :: "'a Assertion" assume A: "x ≤ y" assume B: "y ≤ z" from A and B show "x ≤ z"
next
fix x y :: "'a Assertion" assume A: "x ≤ y" assume B: "y ≤ x" from A and B show "x = y"
apply (cut_tac p = x and q = y in assert_injective)
by (rule antisym, simp_all add: less_eq_Assertion_def)
next
fix x y :: "'a Assertion" show "x ⊓ y ≤ x"
fix x y :: "'a Assertion" show "x ⊓ y ≤ y"
next
fix x y z :: "'a Assertion" assume A: "x ≤ y" assume B: "x ≤ z" from A and B show "x ≤ y ⊓ z"
next
fix x y :: "'a Assertion" show "x ≤ x ⊔ y"
fix x y :: "'a Assertion" show "y ≤ x ⊔ y"
next
fix x y z :: "'a Assertion" assume A: "y ≤ x" assume B: "z ≤ x" from A and B show "y ⊔ z ≤ x"
next
fix x :: "'a Assertion" show "⊥ ≤ x"
next
fix x :: "'a Assertion" show "x ≤ ⊤"
next
fix x y z :: "'a Assertion" show "x ⊔ y ⊓ z = (x ⊔ y) ⊓ (x ⊔ z)"
by (simp add: less_eq_Assertion_def sup_Assertion_def inf_Assertion_def sup_inf_distrib)
next
fix x :: "'a Assertion" show "x ⊓ - x = ⊥"
by (simp add: inf_Assertion_def uminus_Assertion_def bot_Assertion_def)
next
fix x :: "'a Assertion" show "x ⊔ - x = ⊤"
by (simp add: sup_Assertion_def uminus_Assertion_def top_Assertion_def)
next
fix x y :: "'a Assertion" show "x - y = x ⊓ - y"
qed

end

lemma assert_image [simp]: "assert ` A ⊆ assertion"
by auto

instantiation Assertion :: (complete_mbt_algebra) complete_lattice
begin
definition
Sup_Assertion_def: "Sup A = abs_wpt (Sup (assert ` A))"

definition
Inf_Assertion_def: "Inf (A::('a Assertion) set) = - (Sup (uminus ` A))"

lemma Sup1: "(x::'a Assertion) ∈ A ⟹ x ≤ Sup A"
apply (simp add: Sup_Assertion_def less_eq_Assertion_def Abs_Assertion_inverse)
by (rule Sup_upper, simp)

lemma Sup2: "(⋀x::'a Assertion . x ∈ A ⟹ x ≤ z) ⟹ Sup A ≤ z"
apply (simp add: Sup_Assertion_def less_eq_Assertion_def Abs_Assertion_inverse)
apply (rule Sup_least)
by blast

instance
proof
fix x :: "'a Assertion" fix A assume A: "x ∈ A" from A show "Inf A ≤ x"
apply (subst compl_le_compl_iff [THEN sym], simp)
by (rule Sup1, simp)
next
fix z :: "'a Assertion" fix A assume A: "⋀x . x ∈ A ⟹ z ≤ x" from A show "z ≤ Inf A"
apply (subst compl_le_compl_iff [THEN sym], simp)
apply (rule Sup2)
apply safe
by simp
next
fix x :: "'a Assertion" fix A assume A: "x ∈ A" from A show "x ≤ Sup A"
by (rule Sup1)
next
fix z :: "'a Assertion" fix A assume A: "⋀x . x ∈ A ⟹ x ≤ z" from A show "Sup A ≤ z"
by (rule Sup2)
next
show "Inf {} = (⊤::'a Assertion)"
by (auto simp: Inf_Assertion_def Sup_Assertion_def compl_bot_eq [symmetric] bot_Assertion_def)
next
show "Sup {} = (⊥::'a Assertion)"
by (auto simp: Sup_Assertion_def bot_Assertion_def)
qed
end

lemma assert_top [simp]: "{⋅⊤} = 1"

lemma assert_Sup: "{⋅Sup A} = Sup (assert ` A)"

lemma assert_Inf: "{⋅Inf A} = (Inf (assert ` A)) ⊓ 1"
proof (cases "A = {}")
case True then show ?thesis by simp
next
note image_cong_simp [cong del]
case False then show ?thesis
apply (simp add: neg_assert_def assert_Sup dual_Sup Inf_comp inf_commute inf_Inf comp_def)
apply (rule_tac f = Inf in arg_cong)
apply safe
apply simp
apply (subst inf_commute)
apply (simp add: neg_assert_def dual_comp dual_inf sup_comp assertion_prop)
apply auto [1]
apply (simp)
apply (subst image_def, simp)
apply (subst inf_commute)
apply (simp add: neg_assert_def dual_comp dual_inf sup_comp assertion_prop)
apply auto
done
qed

lemma assert_Inf_ne: "A ≠ {} ⟹ {⋅Inf A} = Inf (assert ` A)"
apply (unfold assert_Inf)
apply (rule antisym)
apply simp_all
apply safe
apply (erule notE)
apply (rule_tac y = "{⋅x}" in order_trans)