Theory Monotonic_Boolean_Transformers
section ‹Monotonic Boolean Transformers›
theory Monotonic_Boolean_Transformers
imports MonoBoolTranAlgebra.Assertion_Algebra Base
begin
no_notation inf (infixl ‹⊓› 70)
unbundle no uminus_syntax
context mbt_algebra
begin
lemma directed_left_mult:
"directed Y ⟹ directed ((*) x ` Y)"
apply (unfold directed_def)
using le_comp by blast
lemma neg_assertion:
"neg_assert x ∈ assertion"
by (metis bot_comp neg_assert_def wpt_def wpt_is_assertion mult_assoc)
lemma assertion_neg_assert:
"x ∈ assertion ⟷ x = neg_assert (neg_assert x)"
by (metis neg_assertion uminus_uminus)
text ‹extend and dualise part of Viorel Preoteasa's theory›
definition "assumption ≡ {x . 1 ≤ x ∧ (x * bot) ⊔ (x ^ o) = x}"
definition "neg_assume (x::'a) ≡ (x ^ o * top) ⊔ 1"
lemma neg_assume_assert:
"neg_assume x = (neg_assert (x ^ o)) ^ o"
using dual_bot dual_comp dual_dual dual_inf dual_one neg_assert_def neg_assume_def by auto
lemma assert_iff_assume:
"x ∈ assertion ⟷ x ^ o ∈ assumption"
by (smt assertion_def assumption_def dual_bot dual_comp dual_dual dual_inf dual_le dual_one mem_Collect_eq)
lemma assertion_iff_assumption_subseteq:
"X ⊆ assertion ⟷ dual ` X ⊆ assumption"
using assert_iff_assume by blast
lemma assumption_iff_assertion_subseteq:
"X ⊆ assumption ⟷ dual ` X ⊆ assertion"
using assert_iff_assume by auto
lemma assumption_prop:
"x ∈ assumption ⟹ (x * bot) ⊔ 1 = x"
by (smt assert_iff_assume assertion_prop dual_comp dual_dual dual_neg_top dual_one dual_sup dual_top)
lemma neg_assumption:
"neg_assume x ∈ assumption"
using assert_iff_assume neg_assertion neg_assume_assert by auto
lemma assumption_neg_assume:
"x ∈ assumption ⟷ x = neg_assume (neg_assume x)"
by (smt assert_iff_assume assertion_neg_assert dual_dual neg_assume_assert)
lemma assumption_sup_comp_eq:
"x ∈ assumption ⟹ y ∈ assumption ⟹ x ⊔ y = x * y"
by (smt assert_iff_assume assertion_inf_comp_eq dual_comp dual_dual dual_sup)
lemma sup_uminus_assume[simp]:
"x ∈ assumption ⟹ x ⊓ neg_assume x = 1"
by (smt assert_iff_assume dual_dual dual_one dual_sup neg_assume_assert sup_uminus)
lemma inf_uminus_assume[simp]:
"x ∈ assumption ⟹ x ⊔ neg_assume x = top"
by (smt assert_iff_assume dual_dual dual_sup dual_top inf_uminus neg_assume_assert sup_bot_right)
lemma uminus_assumption[simp]:
"x ∈ assumption ⟹ neg_assume x ∈ assumption"
by (simp add: neg_assumption)
lemma uminus_uminus_assume[simp]:
"x ∈ assumption ⟹ neg_assume (neg_assume x) = x"
by (simp add: assumption_neg_assume)
lemma sup_assumption[simp]:
"x ∈ assumption ⟹ y ∈ assumption ⟹ x ⊔ y ∈ assumption"
by (smt assert_iff_assume dual_dual dual_sup inf_assertion)
lemma comp_assumption[simp]:
"x ∈ assumption ⟹ y ∈ assumption ⟹ x * y ∈ assumption"
using assumption_sup_comp_eq sup_assumption by auto
lemma inf_assumption[simp]:
"x ∈ assumption ⟹ y ∈ assumption ⟹ x ⊓ y ∈ assumption"
by (smt assert_iff_assume dual_dual dual_inf sup_assertion)
lemma assumption_comp_idempotent[simp]:
"x ∈ assumption ⟹ x * x = x"
using assumption_sup_comp_eq by fastforce
lemma assumption_comp_idempotent_dual[simp]:
"x ∈ assumption ⟹ (x ^ o) * (x ^ o) = x ^ o"
by (metis assumption_comp_idempotent dual_comp)
lemma top_assumption[simp]:
"top ∈ assumption"
by (simp add: assumption_def)
lemma one_assumption[simp]:
"1 ∈ assumption"
by (simp add: assumption_def)
lemma assert_top:
"neg_assert (neg_assert p) ^ o * bot = neg_assert p * top"
by (smt bot_comp dual_comp dual_dual dual_top inf_comp inf_top_right mult.assoc mult.left_neutral neg_assert_def)
lemma assume_bot:
"neg_assume (neg_assume p) ^ o * top = neg_assume p * bot"
by (smt assert_top dual_bot dual_comp dual_dual neg_assume_assert)
definition "wpb x ≡ (x * bot) ⊔ 1"
lemma wpt_iff_wpb:
"wpb x = wpt (x ^ o) ^ o"
using dual_comp dual_dual dual_inf dual_one dual_top wpt_def wpb_def by auto
lemma wpb_is_assumption[simp]:
"wpb x ∈ assumption"
using assert_iff_assume wpt_is_assertion wpt_iff_wpb by auto
lemma wpb_comp:
"(wpb x) * x = x"
by (smt dual_comp dual_dual dual_neg_top dual_sup wpt_comp wpt_iff_wpb)
lemma wpb_comp_2:
"wpb (x * y) = wpb (x * (wpb y))"
by (simp add: sup_comp mult_assoc wpb_def)
lemma wpb_assumption[simp]:
"x ∈ assumption ⟹ wpb x = x"
by (simp add: assumption_prop wpb_def)
lemma wpb_choice:
"wpb (x ⊔ y) = wpb x ⊔ wpb y"
using sup_assoc sup_commute sup_comp wpb_def by auto
lemma wpb_dual_assumption:
"x ∈ assumption ⟹ wpb (x ^ o) = 1"
by (smt assert_iff_assume dual_dual dual_one wpt_dual_assertion wpt_iff_wpb)
lemma wpb_mono:
"x ≤ y ⟹ wpb x ≤ wpb y"
by (metis le_iff_sup wpb_choice)
lemma assumption_disjunctive:
"x ∈ assumption ⟹ x ∈ disjunctive"
by (smt assert_iff_assume assertion_conjunctive dual_comp dual_conjunctive dual_dual)
lemma assumption_conjunctive:
"x ∈ assumption ⟹ x ∈ conjunctive"
by (smt assert_iff_assume assertion_disjunctive dual_comp dual_disjunctive dual_dual)
lemma wpb_le_assumption:
"x ∈ assumption ⟹ x * y = y ⟹ x ≤ wpb y"
by (metis assumption_prop bot_least le_comp sup_commute sup_right_isotone mult_assoc wpb_def)
definition dual_omega :: "'a ⇒ 'a" (‹(_ ^ ℧)› [81] 80)
where "(x ^ ℧) ≡ (((x ^ o) ^ ω) ^ o)"
lemma dual_omega_fix:
"x^℧ = (x * (x^℧)) ⊔ 1"
by (smt dual_comp dual_dual dual_omega_def dual_one dual_sup omega_fix)
lemma dual_omega_comp_fix:
"x^℧ * y = (x * (x^℧) * y) ⊔ y"
by (metis dual_omega_fix mult_1_left sup_comp)
lemma dual_omega_greatest:
"z ≤ (x * z) ⊔ y ⟹ z ≤ (x^℧) * y"
by (smt dual_comp dual_dual dual_le dual_neg_top dual_omega_def dual_sup omega_least)
end
context post_mbt_algebra
begin
lemma post_antitone:
assumes "x ≤ y"
shows "post y ≤ post x"
proof -
have "post y ≤ post x * y * top ⊓ post y"
by (metis assms inf_top_left post_1 inf_mono le_comp_left_right order_refl)
thus ?thesis
using order_lesseq_imp post_2 by blast
qed
lemma post_assumption_below_one:
"q ∈ assumption ⟹ post q ≤ post 1"
by (simp add: assumption_def post_antitone)
lemma post_assumption_above_one:
"q ∈ assumption ⟹ post 1 ≤ post (q ^ o)"
by (metis dual_le dual_one post_antitone sup.commute sup_ge1 wpb_assumption wpb_def)
lemma post_assumption_below_dual:
"q ∈ assumption ⟹ post q ≤ post (q ^ o)"
using order_trans post_assumption_above_one post_assumption_below_one by blast
lemma assumption_assertion_absorb:
"q ∈ assumption ⟹ q * (q ^ o) = q"
by (smt CollectE assumption_def assumption_prop bot_comp mult.left_neutral mult_assoc sup_comp)
lemma post_dual_below_post_one:
assumes "q ∈ assumption"
shows "post (q ^ o) ≤ post 1 * q"
proof -
have "post (q ^ o) ≤ post 1 * q * (q ^ o) * top ⊓ post (q ^ o)"
by (metis assms assumption_assertion_absorb gt_one_comp inf_le1 inf_top_left mult_assoc order_refl post_1 sup_uminus_assume top_unique)
thus ?thesis
using order_lesseq_imp post_2 by blast
qed
lemma post_below_post_one:
"q ∈ assumption ⟹ post q ≤ post 1 * q"
using order.trans post_assumption_below_dual post_dual_below_post_one by blast
end
context complete_mbt_algebra
begin
lemma Inf_assumption[simp]:
"X ⊆ assumption ⟹ Inf X ∈ assumption"
by (metis Sup_assertion assert_iff_assume assumption_iff_assertion_subseteq dual_Inf dual_dual)
definition "continuous x ≡ (∀Y . directed Y ⟶ x * (SUP y∈Y . y) = (SUP y∈Y . x * y))"
definition "Continuous ≡ { x . continuous x }"
lemma continuous_Continuous:
"continuous x ⟷ x ∈ Continuous"
by (simp add: Continuous_def)
text ‹Theorem 53.1›
lemma one_continuous:
"1 ∈ Continuous"
by (simp add: Continuous_def continuous_def image_def)
lemma continuous_dist_ascending_chain:
assumes "x ∈ Continuous"
and "ascending_chain f"
shows "x * (SUP n::nat . f n) = (SUP n::nat . x * f n)"
proof -
have "directed (range f)"
by (simp add: assms(2) ascending_chain_directed)
hence "x * (SUP n::nat . f n) = (SUP y∈range f . x * y)"
using assms(1) continuous_Continuous continuous_def by auto
thus ?thesis
by (simp add: range_composition)
qed
text ‹Theorem 53.1›
lemma assertion_continuous:
assumes "x ∈ assertion"
shows "x ∈ Continuous"
proof -
have 1: "x = (x * top) ⊓ 1"
using assms assertion_prop by auto
have "∀Y . directed Y ⟶ x * (SUP y∈Y . y) = (SUP y∈Y . x * y)"
proof (rule allI, rule impI)
fix Y
assume "directed Y"
have "x * (SUP y∈Y . y) = (x * top) ⊓ (SUP y∈Y . y)"
using 1 by (smt inf_comp mult.assoc mult.left_neutral top_comp)
also have "... = (SUP y∈Y . (x * top) ⊓ y)"
by (simp add: inf_Sup)
finally show "x * (SUP y∈Y . y) = (SUP y∈Y . x * y)"
using 1 by (smt inf_comp mult.left_neutral mult.assoc top_comp SUP_cong)
qed
thus ?thesis
by (simp add: continuous_def Continuous_def)
qed
text ‹Theorem 53.1›
lemma assumption_continuous:
assumes "x ∈ assumption"
shows "x ∈ Continuous"
proof -
have 1: "x = (x * bot) ⊔ 1"
by (simp add: assms assumption_prop)
have "∀Y . directed Y ⟶ x * (SUP y∈Y . y) = (SUP y∈Y . x * y)"
proof (rule allI, rule impI)
fix Y
assume 2: "directed Y"
have "x * (SUP y∈Y . y) = (x * bot) ⊔ (SUP y∈Y . y)"
using 1 by (smt sup_comp mult.assoc mult.left_neutral bot_comp)
also have "... = (SUP y∈Y . (x * bot) ⊔ y)"
using 2 by (smt (verit, ccfv_threshold) sup_SUP SUP_cong directed_def)
finally show "x * (SUP y∈Y . y) = (SUP y∈Y . x * y)"
using 1 by (metis sup_comp mult.left_neutral mult.assoc bot_comp SUP_cong)
qed
thus ?thesis
by (simp add: continuous_def Continuous_def)
qed
text ‹Theorem 53.1›
lemma mult_continuous:
assumes "x ∈ Continuous"
and "y ∈ Continuous"
shows "x * y ∈ Continuous"
proof -
have "∀Y. directed Y ⟶ x * y * (SUP y∈Y . y) = (SUP z∈Y . x * y * z)"
proof (rule allI, rule impI)
fix Y
assume "directed Y"
hence "x * y * (SUP w∈Y . w) = (SUP z∈Y . x * (y * z))"
by (metis assms continuous_Continuous continuous_def directed_left_mult image_ident image_image mult_assoc)
thus "x * y * (SUP y∈Y . y) = (SUP z∈Y . x * y * z)"
using mult_assoc by auto
qed
thus ?thesis
using Continuous_def continuous_def by blast
qed
text ‹Theorem 53.1›
lemma sup_continuous:
"x ∈ Continuous ⟹ y ∈ Continuous ⟹ x ⊔ y ∈ Continuous"
by (smt SUP_cong SUP_sup_distrib continuous_Continuous continuous_def sup_comp)
text ‹Theorem 53.1›
lemma inf_continuous:
assumes "x ∈ Continuous"
and "y ∈ Continuous"
shows "x ⊓ y ∈ Continuous"
proof -
have "∀Y. directed Y ⟶ (x ⊓ y) * (SUP y∈Y . y) = (SUP z∈Y . (x ⊓ y) * z)"
proof (rule allI, rule impI)
fix Y
assume 1: "directed Y"
have 2: "(SUP w∈Y . SUP z∈Y . (x * w) ⊓ (y * z)) ≤ (SUP z∈Y . (x * z) ⊓ (y * z))"
proof (intro SUP_least)
fix w z
assume "w ∈ Y" and "z ∈ Y"
from this obtain v where 3: "v∈Y ∧ w ≤ v ∧ z ≤ v"
using 1 by (meson directed_def)
hence "x * w ⊓ (y * z) ≤ (x * v) ⊓ (y * v)"
by (meson inf.sup_mono le_comp)
thus "x * w ⊓ (y * z) ≤ (SUP z∈Y . (x * z) ⊓ (y * z))"
using 3 by (meson SUP_upper2)
qed
have "(SUP z∈Y . (x * z) ⊓ (y * z)) ≤ (SUP w∈Y . SUP z∈Y . (x * w) ⊓ (y * z))"
apply (rule SUP_least)
by (meson SUP_upper SUP_upper2)
hence "(SUP w∈Y . SUP z∈Y . (x * w) ⊓ (y * z)) = (SUP z∈Y . (x ⊓ y) * z)"
using 2 order.antisym inf_comp by auto
thus "(x ⊓ y) * (SUP y∈Y . y) = (SUP z∈Y . (x ⊓ y) * z)"
using 1 by (metis assms inf_comp continuous_Continuous continuous_def SUP_inf_distrib2)
qed
thus ?thesis
using Continuous_def continuous_def by blast
qed
text ‹Theorem 53.1›
lemma dual_star_continuous:
assumes "x ∈ Continuous"
shows "x ^ ⊗ ∈ Continuous"
proof -
have "∀Y. directed Y ⟶ (x ^ ⊗) * (SUP y∈Y . y) = (SUP z∈Y . (x ^ ⊗) * z)"
proof (rule allI, rule impI)
fix Y
assume "directed Y"
hence "directed ((*) (x ^ ⊗) ` Y)"
by (simp add: directed_left_mult)
hence "x * (SUP y∈Y . (x ^ ⊗) * y) = (SUP y∈Y . x * ((x ^ ⊗) * y))"
by (metis assms continuous_Continuous continuous_def image_ident image_image)
also have "... = (SUP y∈Y . x * (x ^ ⊗) * y)"
using mult_assoc by auto
also have "... ≤ (SUP y∈Y . (x ^ ⊗) * y)"
apply (rule SUP_least)
by (simp add: SUP_upper2 dual_star_comp_fix)
finally have "x * (SUP y∈Y . (x ^ ⊗) * y) ⊔ (SUP y∈Y . y) ≤ (SUP y∈Y . (x ^ ⊗) * y)"
apply (rule sup_least)
by (metis SUP_mono' dual_star_comp_fix sup.cobounded1 sup_commute)
thus "(x ^ ⊗) * (SUP y∈Y . y) = (SUP z∈Y . (x ^ ⊗) * z)"
by (meson SUP_least SUP_upper order.antisym dual_star_least le_comp)
qed
thus ?thesis
using Continuous_def continuous_def by blast
qed
text ‹Theorem 53.1›
lemma omega_continuous:
assumes "x ∈ Continuous"
shows "x ^ ω ∈ Continuous"
proof -
have "∀Y. directed Y ⟶ (x ^ ω) * (SUP y∈Y . y) = (SUP z∈Y . (x ^ ω) * z)"
proof (rule allI, rule impI)
fix Y
assume 1: "directed Y"
hence "directed ((*) (x ^ ω) ` Y)"
using directed_left_mult by auto
hence "x * (SUP y∈Y . (x ^ ω) * y) = (SUP y∈Y . x * ((x ^ ω) * y))"
by (metis assms continuous_Continuous continuous_def image_ident image_image)
hence 2: "x * (SUP y∈Y . (x ^ ω) * y) = (SUP y∈Y . x * (x ^ ω) * y)"
by (simp add: mult_assoc)
have "(SUP y∈Y . x * (x ^ ω) * y) ⊓ (SUP y∈Y . y) = (SUP w∈Y . SUP z∈Y . (x * (x ^ ω) * w) ⊓ z)"
using SUP_inf_distrib2 by blast
hence "x * (SUP y∈Y . (x ^ ω) * y) ⊓ (SUP y∈Y . y) = (SUP w∈Y . SUP z∈Y . (x * (x ^ ω) * w) ⊓ z)"
using 2 by auto
also have "... ≤ (SUP y∈Y . (x ^ ω) * y)"
proof (intro SUP_least)
fix w z
assume "w ∈ Y" and "z ∈ Y"
from this obtain v where 3: "v∈Y ∧ w ≤ v ∧ z ≤ v"
using 1 by (meson directed_def)
hence "x * x ^ ω * w ⊓ z ≤ x ^ ω * v"
using inf.sup_mono le_comp omega_comp_fix by auto
thus "x * x ^ ω * w ⊓ z ≤ (SUP y∈Y . (x ^ ω) * y)"
using 3 by (meson SUP_upper2)
qed
finally show "(x ^ ω) * (SUP y∈Y . y) = (SUP z∈Y . (x ^ ω) * z)"
by (meson SUP_least SUP_upper order.antisym omega_least le_comp)
qed
thus ?thesis
using Continuous_def continuous_def by blast
qed
definition "co_continuous x ≡ (∀Y . co_directed Y ⟶ x * (INF y∈Y . y) = (INF y∈Y . x * y))"
definition "Co_continuous ≡ { x . co_continuous x }"
lemma directed_dual:
"directed X ⟷ co_directed (dual ` X)"
by (simp add: directed_def co_directed_def dual_le[THEN sym])
lemma dual_dual_image:
"dual ` dual ` X = X"
by (simp add: image_comp)
lemma continuous_dual:
"continuous x ⟷ co_continuous (x ^ o)"
proof (unfold continuous_def co_continuous_def, rule iffI)
assume 1: "∀Y. directed Y ⟶ x * (SUP y∈Y . y) = (SUP y∈Y . x * y)"
show "∀Y. co_directed Y ⟶ x ^ o * (INF y∈Y . y) = (INF y∈Y . x ^ o * y)"
proof (rule allI, rule impI)
fix Y
assume "co_directed Y"
hence "x ^ o * (INF y∈Y . y) = (INF y∈(dual ` Y) . (x * y) ^ o)"
using 1 by (metis dual_dual_image dual_SUP image_ident image_image dual_comp directed_dual)
also have "... = (INF y∈(dual ` Y) . x ^ o * y ^ o)"
by (meson dual_comp)
also have "... = (INF y∈Y . x ^ o * y)"
by (simp add: image_image)
finally show "x ^ o * (INF y∈Y . y) = (INF y∈Y . x ^ o * y)"
.
qed
next
assume 2: "∀Y. co_directed Y ⟶ x ^ o * (INF y∈Y . y) = (INF y∈Y . x ^ o * y)"
show "∀Y. directed Y ⟶ x * (SUP y∈Y . y) = (SUP y∈Y . x * y)"
proof (rule allI, rule impI)
fix Y
assume "directed Y"
hence "x * (SUP y∈Y . y) = (SUP y∈(dual ` Y) . (x ^ o * y) ^ o)"
using 2 by (metis directed_dual dual_dual_image image_ident image_image dual_SUP dual_comp dual_dual)
also have "... = (SUP y∈(dual ` Y) . x * y ^ o)"
using dual_comp dual_dual by auto
also have "... = (SUP y∈Y . x * y)"
by (simp add: image_image)
finally show "x * (SUP y∈Y . y) = (SUP y∈Y . x * y)"
.
qed
qed
lemma co_continuous_Co_continuous:
"co_continuous x ⟷ x ∈ Co_continuous"
by (simp add: Co_continuous_def)
text ‹Theorem 53.1 and Theorem 53.2›
lemma Continuous_dual:
"x ∈ Continuous ⟷ x ^ o ∈ Co_continuous"
by (simp add: Co_continuous_def Continuous_def continuous_dual)
text ‹Theorem 53.2›
lemma one_co_continuous:
"1 ∈ Co_continuous"
using Continuous_dual one_continuous by auto
lemma ascending_chain_dual:
"ascending_chain f ⟷ descending_chain (dual o f)"
using ascending_chain_def descending_chain_def dual_le by auto
lemma co_continuous_dist_descending_chain:
assumes "x ∈ Co_continuous"
and "descending_chain f"
shows "x * (INF n::nat . f n) = (INF n::nat . x * f n)"
proof -
have "x ^ o * (SUP n::nat . (dual o f) n) = (SUP n::nat . x ^ o * (dual o f) n)"
by (smt assms Continuous_dual SUP_cong ascending_chain_dual continuous_dist_ascending_chain descending_chain_def dual_dual o_def)
thus ?thesis
by (smt INF_cong dual_SUP dual_comp dual_dual o_def)
qed
text ‹Theorem 53.2›
lemma assertion_co_continuous:
"x ∈ assertion ⟹ x ∈ Co_continuous"
by (smt Continuous_dual assert_iff_assume assumption_continuous dual_dual)
text ‹Theorem 53.2›
lemma assumption_co_continuous:
"x ∈ assumption ⟹ x ∈ Co_continuous"
by (smt Continuous_dual assert_iff_assume assertion_continuous dual_dual)
text ‹Theorem 53.2›
lemma mult_co_continuous:
"x ∈ Co_continuous ⟹ y ∈ Co_continuous ⟹ x * y ∈ Co_continuous"
by (smt Continuous_dual dual_comp dual_dual mult_continuous)
text ‹Theorem 53.2›
lemma sup_co_continuous:
"x ∈ Co_continuous ⟹ y ∈ Co_continuous ⟹ x ⊔ y ∈ Co_continuous"
by (smt Continuous_dual dual_sup dual_dual inf_continuous)
text ‹Theorem 53.2›
lemma inf_co_continuous:
"x ∈ Co_continuous ⟹ y ∈ Co_continuous ⟹ x ⊓ y ∈ Co_continuous"
by (smt Continuous_dual dual_inf dual_dual sup_continuous)
text ‹Theorem 53.2›
lemma dual_omega_co_continuous:
"x ∈ Co_continuous ⟹ x ^ ℧ ∈ Co_continuous"
by (smt Continuous_dual dual_omega_def dual_dual omega_continuous)
text ‹Theorem 53.2›
lemma star_co_continuous:
"x ∈ Co_continuous ⟹ x ^ * ∈ Co_continuous"
by (smt Continuous_dual dual_star_def dual_dual dual_star_continuous)
lemma dual_omega_iterate:
assumes "y ∈ Co_continuous"
shows "y ^ ℧ * z = (INF n::nat . ((λx . y * x ⊔ z) ^ n) top)"
proof (rule order.antisym)
show "y ^ ℧ * z ≤ (INF n::nat . ((λx . y * x ⊔ z) ^ n) top)"
proof (rule INF_greatest)
fix n
show "y ^ ℧ * z ≤ ((λx. y * x ⊔ z) ^ n) top"
apply (induct n)
apply (metis power_zero_id id_def top_greatest)
by (smt dual_omega_comp_fix le_comp mult_assoc order_refl sup_mono power_succ_unfold_ext)
qed
next
have 1: "descending_chain (λn . ((λx. y * x ⊔ z) ^ n) top)"
proof (unfold descending_chain_def, rule allI)
fix n
show "((λx. y * x ⊔ z) ^ Suc n) top ≤ ((λx. y * x ⊔ z) ^ n) top"
apply (induct n)
apply (metis power_zero_id id_def top_greatest)
by (smt power_succ_unfold_ext sup_mono order_refl le_comp)
qed
have "(INF n. ((λx. y * x ⊔ z) ^ n) top) ≤ (INF n. ((λx. y * x ⊔ z) ^ Suc n) top)"
apply (rule INF_greatest)
apply (unfold power_succ_unfold_ext)
by (smt power_succ_unfold_ext INF_lower UNIV_I)
thus "(INF n. ((λx. y * x ⊔ z) ^ n) top) ≤ y ^ ℧ * z"
using 1 by (smt assms INF_cong co_continuous_dist_descending_chain power_succ_unfold_ext sup_INF sup_commute dual_omega_greatest)
qed
lemma dual_omega_iterate_one:
"y ∈ Co_continuous ⟹ y ^ ℧ = (INF n::nat . ((λx . y * x ⊔ 1) ^ n) top)"
by (metis dual_omega_iterate mult.right_neutral)
subclass ccpo
apply unfold_locales
apply (simp add: Sup_upper)
using Sup_least by auto
end
class post_mbt_algebra_ext = post_mbt_algebra +
assumes post_sub_fusion: "post 1 * neg_assume q ≤ post (neg_assume q ^ o)"
begin
lemma post_fusion:
"post (neg_assume q ^ o) = post 1 * neg_assume q"
using order.antisym neg_assumption post_dual_below_post_one post_sub_fusion by auto
lemma post_dual_post_one:
"q ∈ assumption ⟹ post 1 * q ≤ post (q ^ o)"
by (metis assumption_neg_assume post_sub_fusion)
end
instance MonoTran :: (complete_boolean_algebra) post_mbt_algebra_ext
proof
fix q :: "'a MonoTran"
show "post 1 * neg_assume q ≤ post (neg_assume q ^ o)"
proof (unfold neg_assume_def, transfer)
fix f :: "'a ⇒ 'a"
assume "mono f"
have "∀x. top ≤ -f bot ⊔ x ⟶ ¬ f bot ≤ x ⟶ top ≤ bot"
by (metis (no_types, lifting) double_compl inf.sup_bot_left inf_compl_bot sup.order_iff sup_bot_left sup_commute sup_inf_distrib1 top.extremum_uniqueI)
hence "post_fun top ∘ (dual_fun f ∘ top) ⊔ id ≤ post_fun (f bot)"
by (simp add: dual_fun_def le_fun_def post_fun_def)
thus "post_fun (id top) ∘ (dual_fun f ∘ top) ⊔ id ≤ post_fun (dual_fun ((dual_fun f ∘ top) ⊔ id) top)"
by simp
qed
qed
class complete_mbt_algebra_ext = complete_mbt_algebra + post_mbt_algebra_ext
instance MonoTran :: (complete_boolean_algebra) complete_mbt_algebra_ext ..
end