# 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
apply simp
apply simp
apply simp

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

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
using dual_omega_fix sup_commute apply force

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

text ‹Theorem 50.9(b)›

sublocale mbt_algebra < mbta: left_conway_semiring_L where circ = dual_star and L = bot
apply unfold_locales
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
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
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 (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
using assertion_inf_comp_eq inf_uminus neg_assertion apply force
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 (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: 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
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
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
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

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"
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"
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"
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 (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

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)

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)

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
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)"
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
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)"