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" apply (simp add: abs_wpt_def) by (simp add: assert_def Rep_Assertion_inverse) lemma [simp]: "x ∈ assertion ⟹ {⋅Abs_Assertion x} = x" apply (simp add: assert_def) by (rule Abs_Assertion_inverse, simp) lemma [simp]: "x ∈ assertion ⟹ {⋅abs_wpt x} = x" apply (simp add: abs_wpt_def assert_def) 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" by (simp add: less_eq_Assertion_def) 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" by (simp add: less_eq_Assertion_def inf_Assertion_def) fix x y :: "'a Assertion" show "x ⊓ y ≤ y" by (simp add: less_eq_Assertion_def inf_Assertion_def) next fix x y z :: "'a Assertion" assume A: "x ≤ y" assume B: "x ≤ z" from A and B show "x ≤ y ⊓ z" by (simp add: less_eq_Assertion_def inf_Assertion_def) next fix x y :: "'a Assertion" show "x ≤ x ⊔ y" by (simp add: less_eq_Assertion_def sup_Assertion_def) fix x y :: "'a Assertion" show "y ≤ x ⊔ y" by (simp add: less_eq_Assertion_def sup_Assertion_def) next fix x y z :: "'a Assertion" assume A: "y ≤ x" assume B: "z ≤ x" from A and B show "y ⊔ z ≤ x" by (simp add: less_eq_Assertion_def sup_Assertion_def) next fix x :: "'a Assertion" show "⊥ ≤ x" by (simp add: less_eq_Assertion_def bot_Assertion_def) next fix x :: "'a Assertion" show "x ≤ ⊤" by (simp add: less_eq_Assertion_def top_Assertion_def) 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" by (simp add: minus_Assertion_def) 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 (simp add: Inf_Assertion_def) 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 (simp add: Inf_Assertion_def) 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" by (simp add: top_Assertion_def) lemma assert_Sup: "{⋅Sup A} = Sup (assert ` A)" by (simp add: Sup_Assertion_def Abs_Assertion_inverse) 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: Inf_Assertion_def uminus_Assertion_def) 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: image_def uminus_Assertion_def) 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 (simp add: uminus_Assertion_def) 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) by (simp_all add: INF_lower) lemma assert_Sup_range: "{⋅Sup (range p)} = Sup (range (assert o p))" apply (subst assert_Sup) by (rule_tac f = "Sup" in arg_cong, auto) lemma assert_Sup_less: "{⋅ Sup_less p w } = Sup_less (assert o p) w" apply (simp add: Sup_less_def) apply (subst assert_Sup) by (rule_tac f = "Sup" in arg_cong, auto) end