Theory Monotonic_Boolean_Transformers_Instances

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

section Instances of Monotonic Boolean Transformers

theory Monotonic_Boolean_Transformers_Instances

imports Monotonic_Boolean_Transformers Pre_Post_Modal General_Refinement_Algebras

begin

sublocale mbt_algebra < mbta: bounded_idempotent_left_semiring
  apply unfold_locales
  apply (simp add: le_comp)
  apply (simp add: sup_comp)
  apply simp
  apply simp
  apply simp
  apply simp
  by (simp add: mult_assoc)

sublocale mbt_algebra < mbta_dual: bounded_idempotent_left_semiring where less = greater and less_eq = greater_eq and sup = inf and bot = top and top = bot
  apply unfold_locales
  using inf.bounded_iff inf_le1 inf_le2 mbta.mult_right_isotone apply simp
  using inf_comp apply blast
  apply simp
  apply simp
  apply simp
  apply simp
  by (simp add: mult_assoc)

sublocale mbt_algebra < mbta: bounded_general_refinement_algebra where star = dual_star and Omega = dual_omega
  apply unfold_locales
  using dual_star_fix sup_commute apply force
  apply (simp add: dual_star_least)
  using dual_omega_fix sup_commute apply force
  by (simp add: dual_omega_greatest sup_commute)

sublocale mbt_algebra < mbta_dual: bounded_general_refinement_algebra where less = greater and less_eq = greater_eq and sup = inf and bot = top and Omega = omega and top = bot
  apply unfold_locales
  using order.eq_iff star_fix apply simp
  using star_greatest apply simp
  using inf_commute omega_fix apply fastforce
  by (simp add: inf.sup_monoid.add_commute omega_least)

text Theorem 50.9(b)

sublocale mbt_algebra < mbta: left_conway_semiring_L where circ = dual_star and L = bot
  apply unfold_locales
  apply (simp add: mbta.star_one)
  by simp

text Theorem 50.8(a)

sublocale mbt_algebra < mbta_dual: left_conway_semiring_L where circ = omega and less = greater and less_eq = greater_eq and sup = inf and bot = top and L = bot
  apply unfold_locales
  apply simp
  by simp

text Theorem 50.8(b)

sublocale mbt_algebra < mbta_fix: left_conway_semiring_L where circ = dual_omega and L = top
  apply unfold_locales
  apply (simp add: mbta.Omega_one)
  by simp

text Theorem 50.9(a)

sublocale mbt_algebra < mbta_fix_dual: left_conway_semiring_L where circ = star and less = greater and less_eq = greater_eq and sup = inf and bot = top and L = top
  apply unfold_locales
  apply (simp add: mbta_dual.star_one)
  by simp

sublocale mbt_algebra < mbta: left_kleene_conway_semiring where circ = dual_star and star = dual_star ..

sublocale mbt_algebra < mbta_dual: left_kleene_conway_semiring where circ = omega and less = greater and less_eq = greater_eq and sup = inf and bot = top ..

sublocale mbt_algebra < mbta_fix: left_kleene_conway_semiring where circ = dual_omega and star = dual_star ..

sublocale mbt_algebra < mbta_fix_dual: left_kleene_conway_semiring where circ = star and less = greater and less_eq = greater_eq and sup = inf and bot = top ..

sublocale mbt_algebra < mbta: tests where uminus = neg_assert
  apply unfold_locales
  apply (simp add: mult_assoc)
  apply (metis neg_assertion assertion_inf_comp_eq inf_commute)
  subgoal for x y
  proof -
    have "(x ^ o * bot  y * top)  ((x ^ o * bot  y ^ o * bot)  1) = x ^ o * bot  1"
      by (metis inf_assoc dual_neg sup_bot_right sup_inf_distrib1)
    thus ?thesis
      by (simp add: dual_inf dual_comp inf_comp sup_comp neg_assert_def)
  qed
  apply (simp add: neg_assertion)
  using assertion_inf_comp_eq inf_uminus neg_assertion apply force
  apply (simp add: neg_assert_def)
  apply (simp add: dual_inf dual_comp sup_comp neg_assert_def inf_sup_distrib2)
  apply (simp add: assertion_inf_comp_eq inf.absorb_iff1 neg_assertion)
  using inf.less_le_not_le by blast

sublocale mbt_algebra < mbta_dual: tests where less = greater and less_eq = greater_eq and sup = inf and uminus = neg_assume and bot = top
  apply unfold_locales
  apply (simp add: mult_assoc)
  apply (metis neg_assumption assumption_sup_comp_eq sup_commute)
  subgoal for x y
  proof -
    have "(x ^ o * top  y * bot)  ((x ^ o * top  y ^ o * top)  1) = x ^ o * top  1"
      by (metis dual_dual dual_neg_top inf_sup_distrib1 inf_top_right sup_assoc)
    thus ?thesis
      by (simp add: dual_comp dual_sup inf_comp sup_comp neg_assume_def)
  qed
  using assumption_neg_assume comp_assumption neg_assumption apply blast
  using assumption_sup_comp_eq inf_uminus_assume neg_assumption apply fastforce
  apply (simp add: neg_assume_def)
  apply (simp add: dual_inf dual_comp dual_sup inf_comp sup_comp neg_assume_def sup_inf_distrib2)
  apply (simp add: assumption_sup_comp_eq neg_assumption sup.absorb_iff1)
  using inf.less_le_not_le by auto

text Theorem 51.2

sublocale mbt_algebra < mbta: bounded_relative_antidomain_semiring where d = "λx . (x * top)  1" and uminus = neg_assert and Z = bot
  apply unfold_locales
  subgoal for x
  proof -
    have "x ^ o * bot  x  bot"
      by (metis dual_neg eq_refl inf.commute inf_mono mbta.top_right_mult_increasing)
    thus ?thesis
      by (simp add: neg_assert_def inf_comp)
  qed
  apply (simp add: dual_comp dual_inf neg_assert_def sup_comp mult_assoc)
  apply simp
  apply simp
  apply (simp add: dual_inf dual_comp sup_comp neg_assert_def inf_sup_distrib2)
  apply (simp add: dual_sup inf_comp neg_assert_def inf.assoc)
  by (simp add: dual_inf dual_comp sup_comp neg_assert_def)

text Theorem 51.1

sublocale mbt_algebra < mbta_dual: bounded_relative_antidomain_semiring where d = "λx . (x * bot)  1" and less = greater and less_eq = greater_eq and sup = inf and uminus = neg_assume and bot = top and top = bot and Z = top
  apply unfold_locales
  subgoal for x
  proof -
    have "top  x ^ o * top  x"
      by (metis dual_dual dual_neg_top mbta_dual.top_right_mult_increasing sup_commute sup_left_isotone)
    thus ?thesis
      by (simp add: sup_comp neg_assume_def)
  qed
  using assume_bot dual_comp neg_assume_def sup_comp mult_assoc apply simp
  apply simp
  apply simp
  apply (simp add: dual_inf dual_comp dual_sup inf_comp sup_comp neg_assume_def sup_inf_distrib2)
  apply (simp add: dual_inf sup_comp neg_assume_def sup.assoc)
  by (simp add: dual_comp dual_sup inf_comp neg_assume_def)

sublocale mbt_algebra < mbta: relative_domain_semiring_split where d = "λx . (x * top)  1" and Z = bot
  apply unfold_locales
  by simp

sublocale mbt_algebra < mbta_dual: relative_domain_semiring_split where d = "λx . (x * bot)  1" and less = greater and less_eq = greater_eq and sup = inf and bot = top and Z = top
  apply unfold_locales
  by simp

sublocale mbt_algebra < mbta: diamond_while where box = "λx y . neg_assert (x * neg_assert y)" and circ = dual_star and d = "λx . (x * top)  1" and diamond = "λx y . (x * y * top)  1" and ite = "λx p y . (p * x)  (neg_assert p * y)" and pre = "λx y . wpt (x * y)" and uminus = neg_assert and while = "λp x . ((p * x) ^ ) * neg_assert p" and Z = bot
  apply unfold_locales
  apply simp
  apply simp
  apply (rule wpt_def)
  apply simp
  by simp

sublocale mbt_algebra < mbta_dual: box_while where box = "λx y . neg_assume (x * neg_assume y)" and circ = omega and d = "λx . (x * bot)  1" and diamond = "λx y . (x * y * bot)  1" and ite = "λx p y . (p * x)  (neg_assume p * y)" and less = greater and less_eq = greater_eq and sup = inf and pre = "λx y . wpb (x ^ o * y)" and uminus = neg_assume and while = "λp x . ((p * x) ^ ω) * neg_assume p" and bot = top and top = bot and Z = top
  apply unfold_locales
  apply simp
  apply simp
  apply (metis assume_bot dual_comp mbta_dual.a_mult_d_2 mbta_dual.d_def neg_assume_def wpb_def mult_assoc)
  apply simp
  by simp

sublocale mbt_algebra < mbta_fix: diamond_while where box = "λx y . neg_assert (x * neg_assert y)" and circ = dual_omega and d = "λx . (x * top)  1" and diamond = "λx y . (x * y * top)  1" and ite = "λx p y . (p * x)  (neg_assert p * y)" and pre = "λx y . wpt (x * y)" and uminus = neg_assert and while = "λp x . ((p * x) ^ ) * neg_assert p" and Z = bot
  apply unfold_locales
  by simp_all

sublocale mbt_algebra < mbta_fix_dual: box_while where box = "λx y . neg_assume (x * neg_assume y)" and circ = star and d = "λx . (x * bot)  1" and diamond = "λx y . (x * y * bot)  1" and ite = "λx p y . (p * x)  (neg_assume p * y)" and less = greater and less_eq = greater_eq and sup = inf and pre = "λx y . wpb (x ^ o * y)" and uminus = neg_assume and while = "λp x . ((p * x) ^ *) * neg_assume p" and bot = top and top = bot and Z = top
  apply unfold_locales
  by simp_all

sublocale mbt_algebra < mbta_pre: box_while where box = "λx y . neg_assert (x * neg_assert y)" and circ = dual_star and d = "λx . (x * top)  1" and diamond = "λx y . (x * y * top)  1" and ite = "λx p y . (p * x)  (neg_assert p * y)" and pre = "λx y . wpt (x ^ o * y)" and uminus = neg_assert and while = "λp x . ((p * x) ^ ) * neg_assert p" and Z = bot
  apply unfold_locales
  apply (metis dual_comp dual_dual dual_top inf_top_right mbta_dual.mult_right_dist_sup mult_1_left neg_assert_def top_comp wpt_def mult_assoc)
  apply simp
  by simp

sublocale mbt_algebra < mbta_pre_dual: diamond_while where box = "λx y . neg_assume (x * neg_assume y)" and circ = omega and d = "λx . (x * bot)  1" and diamond = "λx y . (x * y * bot)  1" and ite = "λx p y . (p * x)  (neg_assume p * y)" and less = greater and less_eq = greater_eq and sup = inf and pre = "λx y . wpb (x * y)" and uminus = neg_assume and while = "λp x . ((p * x) ^ ω) * neg_assume p" and bot = top and top = bot and Z = top
  apply unfold_locales
  apply (simp add: wpb_def)
  apply simp
  by simp

sublocale mbt_algebra < mbta_pre_fix: box_while where box = "λx y . neg_assert (x * neg_assert y)" and circ = dual_omega and d = "λx . (x * top)  1" and diamond = "λx y . (x * y * top)  1" and ite = "λx p y . (p * x)  (neg_assert p * y)" and pre = "λx y . wpt (x ^ o * y)" and uminus = neg_assert and while = "λp x . ((p * x) ^ ) * neg_assert p" and Z = bot
  apply unfold_locales
  by simp_all

sublocale mbt_algebra < mbta_pre_fix_dual: diamond_while where box = "λx y . neg_assume (x * neg_assume y)" and circ = star and d = "λx . (x * bot)  1" and diamond = "λx y . (x * y * bot)  1" and ite = "λx p y . (p * x)  (neg_assume p * y)" and less = greater and less_eq = greater_eq and sup = inf and pre = "λx y . wpb (x * y)" and uminus = neg_assume and while = "λp x . ((p * x) ^ *) * neg_assume p" and bot = top and top = bot and Z = top
  apply unfold_locales
  by simp_all

sublocale post_mbt_algebra < mbta: pre_post_spec_Hd where box = "λx y . neg_assert (x * neg_assert y)" and d = "λx . (x * top)  1" and diamond = "λx y . (x * y * top)  1" and pre = "λx y . wpt (x * y)" and pre_post = "λp q . p * post q" and uminus = neg_assert and Hd = "post 1" and Z = bot
  apply unfold_locales
  apply (metis mult.assoc mult.left_neutral post_1)
  apply (metis inf.commute inf_top_right mult.assoc mult.left_neutral post_2)
  apply (metis neg_assertion assertion_disjunctive disjunctiveD)
  subgoal for p x q
  proof
    let ?pt = "neg_assert p"
    let ?qt = "neg_assert q"
    assume "?pt  wpt (x * ?qt)"
    hence "?pt * post ?qt  x * ?qt * top * post ?qt  post ?qt"
      by (metis mbta.mult_left_isotone wpt_def inf_comp mult.left_neutral)
    thus "?pt * post ?qt  x"
      by (smt mbta.top_left_zero mult.assoc post_2 order_trans)
  next
    let ?pt = "neg_assert p"
    let ?qt = "neg_assert q"
    assume "?pt * post ?qt  x"
    thus "?pt  wpt (x * ?qt)"
      by (smt mbta.a_d_closed post_1 mult_assoc mbta.diamond_left_isotone wpt_def)
  qed
  by (simp add: mbta_dual.mult_right_dist_sup)

sublocale post_mbt_algebra < mbta_dual: pre_post_spec_H where box = "λx y . neg_assume (x * neg_assume y)" and d = "λx . (x * bot)  1" and diamond = "λx y . (x * y * bot)  1" and less = greater and less_eq = greater_eq and sup = inf and pre = "λx y . wpb (x ^ o * y)" and pre_post = "λp q . (p ^ o) * post (q ^ o)" and uminus = neg_assume and bot = top and H = "post 1" and top = bot and Z = top
proof
  fix p x q
  let ?pt = "neg_assume p"
  let ?qt = "neg_assume q"
  show "wpb (x ^ o * ?qt)  ?pt  ?pt ^ o * post (?qt ^ o)  x"
  proof
    assume "wpb (x ^ o * ?qt)  ?pt"
    hence "?pt ^ o * post (?qt ^ o)  (x * (?qt ^ o) * top  1) * post (?qt ^ o)"
      by (smt wpb_def dual_le dual_comp dual_dual dual_one dual_sup dual_top mbta.mult_left_isotone)
    thus "?pt ^ o * post (?qt ^ o)  x"
      by (smt inf_comp mult_assoc top_comp mult.left_neutral post_2 order_trans)
  next
    assume 1: "?pt ^ o * post (?qt ^ o)  x"
    have "?pt ^ o = ?pt ^ o * post (?qt ^ o) * (?qt ^ o) * top  1"
      by (metis assert_iff_assume assertion_prop dual_dual mult_assoc neg_assumption post_1)
    thus "wpb (x ^ o * ?qt)  ?pt"
      using 1 by (smt dual_comp dual_dual dual_le dual_one dual_sup dual_top wpb_def mbta.diamond_left_isotone)
  qed
  show "post 1 * top = top"
    by (simp add: mbta.Hd_total)
  have "x * ?qt * bot  (post 1 * neg_assume ?qt) = (x * neg_assume ?qt ^ o * top  post 1) * neg_assume ?qt"
    by (simp add: assume_bot mbta_dual.mult_right_dist_sup mult_assoc)
  also have "...  x * neg_assume ?qt ^ o"
    by (smt assumption_assertion_absorb dual_comp dual_dual mbta.mult_left_isotone mult.right_neutral mult_assoc neg_assumption post_2)
  also have "...  x"
    by (metis dual_comp dual_dual dual_le mbta.mult_left_sub_dist_sup_left mult.right_neutral neg_assume_def sup.commute)
  finally show "x * ?qt * bot  (post 1 * neg_assume ?qt)  x"
    .
qed

sublocale post_mbt_algebra < mbta_pre: pre_post_spec_H where box = "λx y . neg_assert (x * neg_assert y)" and d = "λx . (x * top)  1" and diamond = "λx y . (x * y * top)  1" and pre = "λx y . wpt (x ^ o * y)" and pre_post = "λp q . p ^ o * (post q ^ o)" and uminus = neg_assert and H = "post 1 ^ o" and Z = bot
proof
  fix p x q
  let ?pt = "neg_assert p"
  let ?qt = "neg_assert q"
  show "?pt  wpt (x ^ o * ?qt)  x  ?pt ^ o * (post ?qt ^ o)"
  proof
    assume "?pt  wpt (x ^ o * ?qt)"
    hence "?pt * post ?qt  (x ^ o * ?qt * top  1) * post ?qt"
      by (simp add: mbta_dual.mult_left_isotone wpt_def)
    also have "...  x ^ o"
      using mbta.pre_pre_post wpt_def by auto
    finally show "x  ?pt ^ o * (post ?qt ^ o)"
      by (metis dual_le dual_comp dual_dual)
  next
    assume "x  ?pt ^ o * (post ?qt ^ o)"
    hence "x * ?qt ^ o * bot  1  (?pt * post ?qt * ?qt * top  1) ^ o"
      by (smt (z3) inf.absorb_iff1 sup_inf_distrib2 dual_comp dual_inf dual_one dual_top mbta.mult_left_isotone)
    also have "... = ?pt ^ o"
      by (simp add: mbta.diamond_a_export post_1)
    finally show "?pt  wpt (x ^ o * ?qt)"
      by (smt dual_comp dual_dual dual_le dual_neg_top dual_one dual_sup dual_top wpt_def)
  qed
  show "post 1 ^ o * bot = bot"
    by (metis dual_comp dual_top mbta.Hd_total)
  have "x ^ o * ?qt ^ o * bot  (post 1 * neg_assert ?qt ^ o)  x ^ o * neg_assert ?qt * neg_assert ?qt ^ o"
    by (smt (verit, del_insts) bot_comp inf.commute inf_comp inf_top_left mbta.mult_left_isotone mult.left_neutral mult_assoc neg_assert_def post_2)
  also have "...  x ^ o"
    by (smt assert_iff_assume assumption_assertion_absorb dual_comp dual_dual le_comp mbta.a_below_one mult_assoc neg_assertion mult_1_right)
  finally show "x  x * ?qt * top  post 1 ^ o * neg_assert ?qt"
    by (smt dual_comp dual_dual dual_inf dual_le dual_top)
qed

sublocale post_mbt_algebra < mbta_pre_dual: pre_post_spec_Hd where box = "λx y . neg_assume (x * neg_assume y)" and d = "λx . (x * bot)  1" and diamond = "λx y . (x * y * bot)  1" and less = greater and less_eq = greater_eq and sup = inf and pre = "λx y . wpb (x * y)" and pre_post = "λp q . p * (post (q ^ o) ^ o)" and uminus = neg_assume and bot = top and Hd = "post 1 ^ o" and top = bot and Z = top
  apply unfold_locales
  apply (simp add: mbta_pre.H_zero_2)
  apply (simp add: mbta_pre.H_greatest_finite)
  apply (metis (no_types, lifting) dual_comp dual_dual dual_inf dual_top mbta_dual.mult_L_circ_mult mult_1_right neg_assume_def sup_commute sup_inf_distrib2)
  subgoal for p x q
  proof
    let ?pt = "neg_assume p"
    let ?qt = "neg_assume q"
    assume "wpb (x * ?qt)  ?pt"
    hence "?pt ^ o * post (?qt ^ o)  (x ^ o * ?qt ^ o * top  1) * post (?qt ^ o)"
      by (smt dual_comp dual_dual dual_le dual_one dual_sup dual_top le_comp_right wpb_def)
    also have "...  x ^ o"
      using mbta_dual.mult_right_dist_sup post_2 by force
    finally show "x  ?pt * post (?qt ^ o) ^ o"
      by (smt dual_comp dual_dual dual_le)
  next
    let ?pt = "neg_assume p"
    let ?qt = "neg_assume q"
    assume "x  ?pt * post (?qt ^ o) ^ o"
    thus "wpb (x * ?qt)  ?pt"
      by (metis dual_comp dual_dual dual_le mbta_dual.pre_post_galois)
  qed
  by (simp add: sup_comp)

sublocale post_mbt_algebra < mbta_dual: pre_post_spec_whiledo where ite = "λx p y . (p * x)  (neg_assume p * y)" and less = greater and less_eq = greater_eq and sup = inf and pre = "λx y . wpb (x ^ o * y)" and pre_post = "λp q . (p ^ o) * post (q ^ o)" and uminus = neg_assume and while = "λp x . ((p * x) ^ ω) * neg_assume p" and bot = top and top = bot ..

sublocale post_mbt_algebra < mbta_fix_dual: pre_post_spec_whiledo where ite = "λx p y . (p * x)  (neg_assume p * y)" and less = greater and less_eq = greater_eq and sup = inf and pre = "λx y . wpb (x ^ o * y)" and pre_post = "λp q . (p ^ o) * post (q ^ o)" and uminus = neg_assume and while = "λp x . ((p * x) ^ *) * neg_assume p" and bot = top and top = bot ..

sublocale post_mbt_algebra < mbta_pre: pre_post_spec_whiledo where ite = "λx p y . (p * x)  (neg_assert p * y)" and pre = "λx y . wpt (x ^ o * y)" and pre_post = "λp q . p ^ o * (post q ^ o)" and uminus = neg_assert and while = "λp x . ((p * x) ^ ) * neg_assert p" ..

sublocale post_mbt_algebra < mbta_pre_fix: pre_post_spec_whiledo where ite = "λx p y . (p * x)  (neg_assert p * y)" and pre = "λx y . wpt (x ^ o * y)" and pre_post = "λp q . p ^ o * (post q ^ o)" and uminus = neg_assert and while = "λp x . ((p * x) ^ ) * neg_assert p" ..

sublocale post_mbt_algebra < mbta_dual: pre_post_L where box = "λx y . neg_assume (x * neg_assume y)" and circ = omega and d = "λx . (x * bot)  1" and diamond = "λx y . (x * y * bot)  1" and ite = "λx p y . (p * x)  (neg_assume p * y)" and less = greater and less_eq = greater_eq and sup = inf and pre = "λx y . wpb (x ^ o * y)" and pre_post = "λp q . (p ^ o) * post (q ^ o)" and uminus = neg_assume and while = "λp x . ((p * x) ^ ω) * neg_assume p" and bot = top and L = bot and top = bot and Z = top
  apply unfold_locales
  by simp

sublocale post_mbt_algebra < mbta_fix_dual: pre_post_L where box = "λx y . neg_assume (x * neg_assume y)" and circ = star and d = "λx . (x * bot)  1" and diamond = "λx y . (x * y * bot)  1" and ite = "λx p y . (p * x)  (neg_assume p * y)" and less = greater and less_eq = greater_eq and sup = inf and pre = "λx y . wpb (x ^ o * y)" and pre_post = "λp q . (p ^ o) * post (q ^ o)" and uminus = neg_assume and while = "λp x . ((p * x) ^ *) * neg_assume p" and bot = top and L = top and top = bot and Z = top
  apply unfold_locales
  by simp

sublocale post_mbt_algebra < mbta_pre: pre_post_L where box = "λx y . neg_assert (x * neg_assert y)" and circ = dual_star and d = "λx . (x * top)  1" and diamond = "λx y . (x * y * top)  1" and ite = "λx p y . (p * x)  (neg_assert p * y)" and pre = "λx y . wpt (x ^ o * y)" and pre_post = "λp q . p ^ o * (post q ^ o)" and star = dual_star and uminus = neg_assert and while = "λp x . ((p * x) ^ ) * neg_assert p" and L = bot and Z = bot
  apply unfold_locales
  by simp

sublocale post_mbt_algebra < mbta_pre_fix: pre_post_L where box = "λx y . neg_assert (x * neg_assert y)" and circ = dual_omega and d = "λx . (x * top)  1" and diamond = "λx y . (x * y * top)  1" and ite = "λx p y . (p * x)  (neg_assert p * y)" and pre = "λx y . wpt (x ^ o * y)" and pre_post = "λp q . p ^ o * (post q ^ o)" and star = dual_star and uminus = neg_assert and while = "λp x . ((p * x) ^ ) * neg_assert p" and L = top and Z = bot
  apply unfold_locales
  by simp

sublocale complete_mbt_algebra < mbta: complete_tests where uminus = neg_assert
  apply unfold_locales
  apply (smt mbta.test_set_def neg_assertion subset_eq Sup_assertion assertion_neg_assert)
  apply (simp add: Sup_upper)
  by (simp add: Sup_least)

sublocale complete_mbt_algebra < mbta_dual: complete_tests where less = greater and less_eq = greater_eq and sup = inf and uminus = neg_assume and bot = top and Inf = Sup and Sup = Inf
  apply unfold_locales
  apply (smt mbta_dual.test_set_def neg_assumption subset_eq Inf_assumption assumption_neg_assume)
  apply (simp add: Inf_lower)
  by (simp add: Inf_greatest)

sublocale complete_mbt_algebra < mbta: complete_antidomain_semiring where d = "λx . (x * top)  1" and uminus = neg_assert and Z = bot
proof
  fix f :: "nat  'a"
  let ?F = "dual ` {f n | n . True}"
  show "ascending_chain f  neg_assert (complete_tests.Sum Sup f) = complete_tests.Prod Inf (λn. neg_assert (f n))"
  proof
    have "neg_assert (complete_tests.Sum Sup f) = 1  (x?F . x * bot)"
      using Inf_comp dual_Sup mbta.Sum_def neg_assert_def inf_commute by auto
    also have "... = (x?F . 1  x * bot)"
      apply (subst inf_Inf)
      apply blast
      by (simp add: image_image)
    also have "... = {f n ^ o * bot  1 | n . True}"
      apply (rule arg_cong[where f="Inf"])
      using inf_commute by auto
    also have "... = complete_tests.Prod Inf (λn. neg_assert (f n))"
      using mbta.Prod_def neg_assert_def by auto
    finally show "neg_assert (complete_tests.Sum Sup f) = complete_tests.Prod Inf (λn. neg_assert (f n))"
      .
  qed
  show "descending_chain f  neg_assert (complete_tests.Prod Inf f) = complete_tests.Sum Sup (λn. neg_assert (f n))"
  proof
    have "neg_assert (complete_tests.Prod Inf f) = 1  (x?F . x * bot)"
      using Sup_comp dual_Inf mbta.Prod_def neg_assert_def inf_commute by auto
    also have "... = (x?F . 1  x * bot)"
      by (simp add: inf_Sup image_image)
    also have "... = {f n ^ o * bot  1 |n. True}"
      apply (rule arg_cong[where f="Sup"])
      using inf_commute by auto
    also have "... = complete_tests.Sum Sup (λn. neg_assert (f n))"
      using mbta.Sum_def neg_assert_def by auto
    finally show "neg_assert (complete_tests.Prod Inf f) = complete_tests.Sum Sup (λn. neg_assert (f n))"
      .
  qed
qed

sublocale complete_mbt_algebra < mbta_dual: complete_antidomain_semiring where d = "λx . (x * bot)  1" and less = greater and less_eq = greater_eq and sup = inf and uminus = neg_assume and bot = top and Inf = Sup and Sup = Inf and Z = top
proof
  fix f :: "nat  'a"
  let ?F = "dual ` {f n | n . True}"
  show "ord.ascending_chain greater_eq f  neg_assume (complete_tests.Sum Inf f) = complete_tests.Prod Sup (λn. neg_assume (f n))"
  proof
    have "neg_assume (complete_tests.Sum Inf f) = 1  (x?F . x * top)"
      using mbta_dual.Sum_def neg_assume_def dual_Inf Sup_comp sup_commute by auto
    also have "... = (x?F . 1  x * top)"
      apply (subst sup_Sup)
      apply blast
      by (simp add: image_image)
    also have "... = {f n ^ o * top  1 | n . True}"
      apply (rule arg_cong[where f="Sup"])
      using sup_commute by auto
    also have "... = complete_tests.Prod Sup (λn. neg_assume (f n))"
      using mbta_dual.Prod_def neg_assume_def by auto
    finally show "neg_assume (complete_tests.Sum Inf f) = complete_tests.Prod Sup (λn. neg_assume (f n))"
      .
  qed
  show "ord.descending_chain greater_eq f  neg_assume (complete_tests.Prod Sup f) = complete_tests.Sum Inf (λn. neg_assume (f n))"
  proof
    have "neg_assume (complete_tests.Prod Sup f) = 1  (x?F . x * top)"
      using mbta_dual.Prod_def neg_assume_def dual_Inf dual_Sup Inf_comp sup_commute by auto
    also have "... = (x?F . 1  x * top)"
      by (simp add: sup_Inf image_image)
    also have "... = {f n ^ o * top  1 |n. True}"
      apply (rule arg_cong[where f="Inf"])
      using sup_commute by auto
    also have "... = complete_tests.Sum Inf (λn. neg_assume (f n))"
      using mbta_dual.Sum_def neg_assume_def by auto
    finally show "neg_assume (complete_tests.Prod Sup f) = complete_tests.Sum Inf (λn. neg_assume (f n))"
      .
  qed
qed

sublocale complete_mbt_algebra < mbta: diamond_while_program where box = "λx y . neg_assert (x * neg_assert y)" and circ = dual_star and d = "λx . (x * top)  1" and diamond = "λx y . (x <