Theory Monotonic_Boolean_Transformers

(* Title:      Monotonic Boolean Transformers
   Author:     Walter Guttmann
   Maintainer: Walter Guttmann <walter.guttmann at canterbury.ac.nz>
*)

section Monotonic Boolean Transformers

theory Monotonic_Boolean_Transformers

imports MonoBoolTranAlgebra.Assertion_Algebra Base

begin

no_notation inf (infixl "" 70)
no_notation uminus ("- _" [81] 80)

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 yY . y) = (SUP yY . 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 yrange 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 yY . y) = (SUP yY . x * y)"
  proof (rule allI, rule impI)
    fix Y
    assume "directed Y" (* assumption not used *)
    have "x * (SUP yY . y) = (x * top)  (SUP yY . y)"
      using 1 by (smt inf_comp mult.assoc mult.left_neutral top_comp)
    also have "... = (SUP yY . (x * top)  y)"
      by (simp add: inf_Sup)
    finally show "x * (SUP yY . y) = (SUP yY . 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 yY . y) = (SUP yY . x * y)"
  proof (rule allI, rule impI)
    fix Y
    assume 2: "directed Y"
    have "x * (SUP yY . y) = (x * bot)  (SUP yY . y)"
      using 1 by (smt sup_comp mult.assoc mult.left_neutral bot_comp)
    also have "... = (SUP yY . (x * bot)  y)"
      using 2 by (smt (verit, ccfv_threshold) sup_SUP SUP_cong directed_def)
    finally show "x * (SUP yY . y) = (SUP yY . 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 yY . y) = (SUP zY . x * y * z)"
  proof (rule allI, rule impI)
    fix Y
    assume "directed Y"
    hence "x * y * (SUP wY . w) = (SUP zY . x * (y * z))"
      by (metis assms continuous_Continuous continuous_def directed_left_mult image_ident image_image mult_assoc)
    thus "x * y * (SUP yY . y) = (SUP zY . 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 yY . y) = (SUP zY . (x  y) * z)"
  proof (rule allI, rule impI)
    fix Y
    assume 1: "directed Y"
    have 2: "(SUP wY . SUP zY . (x * w)  (y * z))  (SUP zY . (x * z)  (y * z))"
    proof (intro SUP_least)
      fix w z
      assume "w  Y" and "z  Y"
      from this obtain v where 3: "vY  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 zY . (x * z)  (y * z))"
        using 3 by (meson SUP_upper2)
    qed
    have "(SUP zY . (x * z)  (y * z))  (SUP wY . SUP zY . (x * w)  (y * z))"
      apply (rule SUP_least)
      by (meson SUP_upper SUP_upper2)
    hence "(SUP wY . SUP zY . (x * w)  (y * z)) = (SUP zY . (x  y) * z)"
      using 2 order.antisym inf_comp by auto
    thus "(x  y) * (SUP yY . y) = (SUP zY . (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 yY . y) = (SUP zY . (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 yY . (x ^ ) * y) = (SUP yY . x * ((x ^ ) * y))"
      by (metis assms continuous_Continuous continuous_def image_ident image_image)
    also have "... = (SUP yY . x * (x ^ ) * y)"
      using mult_assoc by auto
    also have "...  (SUP yY . (x ^ ) * y)"
      apply (rule SUP_least)
      by (simp add: SUP_upper2 dual_star_comp_fix)
    finally have "x * (SUP yY . (x ^ ) * y)  (SUP yY . y)  (SUP yY . (x ^ ) * y)"
      apply (rule sup_least)
      by (metis SUP_mono' dual_star_comp_fix sup.cobounded1 sup_commute)
    thus "(x ^ ) * (SUP yY . y) = (SUP zY . (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 yY . y) = (SUP zY . (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 yY . (x ^ ω) * y) = (SUP yY . x * ((x ^ ω) * y))"
      by (metis assms continuous_Continuous continuous_def image_ident image_image)
    hence 2: "x * (SUP yY . (x ^ ω) * y) = (SUP yY . x * (x ^ ω) * y)"
      by (simp add: mult_assoc)
    have "(SUP yY . x * (x ^ ω) * y)  (SUP yY . y) = (SUP wY . SUP zY . (x * (x ^ ω) * w)  z)"
      using SUP_inf_distrib2 by blast
    hence "x * (SUP yY . (x ^ ω) * y)  (SUP yY . y) = (SUP wY . SUP zY . (x * (x ^ ω) * w)  z)"
      using 2 by auto
    also have "...  (SUP yY . (x ^ ω) * y)"
    proof (intro SUP_least)
      fix w z
      assume "w  Y" and "z  Y"
      from this obtain v where 3: "vY  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 yY . (x ^ ω) * y)"
        using 3 by (meson SUP_upper2)
    qed
    finally show "(x ^ ω) * (SUP yY . y) = (SUP zY . (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 yY . y) = (INF yY . 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 yY . y) = (SUP yY . x * y)"
  show "Y. co_directed Y  x ^ o * (INF yY . y) = (INF yY . x ^ o * y)"
  proof (rule allI, rule impI)
    fix Y
    assume "co_directed Y"
    hence "x ^ o * (INF yY . 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 yY . x ^ o * y)"
      by (simp add: image_image)
    finally show "x ^ o * (INF yY . y) = (INF yY . x ^ o * y)"
      .
 qed
next
  assume 2: "Y. co_directed Y  x ^ o * (INF yY . y) = (INF yY . x ^ o * y)"
  show "Y. directed Y  x * (SUP yY . y) = (SUP yY . x * y)"
  proof (rule allI, rule impI)
    fix Y
    assume "directed Y"
    hence "x * (SUP yY . 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 yY . x * y)"
      by (simp add: image_image)
    finally show "x * (SUP yY . y) = (SUP yY . 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