# Theory MonoBoolTranAlgebra.Mono_Bool_Tran

```section ‹Monotonic Boolean Transformers›

theory Mono_Bool_Tran
imports
LatticeProperties.Complete_Lattice_Prop
LatticeProperties.Conj_Disj
begin

text‹
The type of monotonic transformers is the type associated to the set of monotonic
functions from a partially ordered set (poset) to itself. The type of monotonic
transformers with the pointwise extended order is also a poset.
The monotonic transformers with composition and identity
form a monoid, and the monoid operation is compatible with the order.

Gradually we extend the algebraic structure of monotonic transformers to
lattices, and complete lattices. We also introduce a dual operator
(\$(\mathsf{dual}\;f) p = - f (-p)\$) on monotonic transformers over
a boolean algebra. However the monotonic transformers over a boolean
algebra are not closed to the pointwise extended negation operator.

Finally we introduce an iteration operator on monotonic transformers
over a complete lattice.
›

unbundle lattice_syntax

lemma Inf_comp_fun:
"⨅M ∘ f = (⨅m∈M. m ∘ f)"

lemma INF_comp_fun:
"(⨅a∈A. g a) ∘ f = (⨅a∈A. g a ∘ f)"

lemma Sup_comp_fun:
"⨆M ∘ f = (⨆m∈M. m ∘ f)"

lemma SUP_comp_fun:
"(⨆a∈A. g a) ∘ f = (⨆a∈A. g a ∘ f)"

lemma (in order) mono_const [simp]:
"mono (λ_. c)"
by (auto intro: monoI)

lemma (in order) mono_id [simp]:
"mono id"
by (auto intro: order_class.monoI)

lemma (in order) mono_comp [simp]:
"mono f ⟹ mono g ⟹ mono (f ∘ g)"
by (auto intro!: monoI elim!: monoE order_class.monoE)

lemma (in bot) mono_bot [simp]:
"mono ⊥"
by (auto intro: monoI)

lemma (in top) mono_top [simp]:
"mono ⊤"
by (auto intro: monoI)

lemma (in semilattice_inf) mono_inf [simp]:
assumes "mono f" and "mono g"
shows "mono (f ⊓ g)"
proof
fix a b
assume "a ≤ b"
have "f a ⊓ g a ≤ f a" by simp
also from ‹mono f› ‹a ≤ b› have "… ≤ f b" by (auto elim: monoE)
finally have *: "f a ⊓ g a ≤ f b" .
have "f a ⊓ g a ≤ g a" by simp
also from ‹mono g› ‹a ≤ b› have "… ≤ g b" by (auto elim: monoE)
finally have **: "f a ⊓ g a ≤ g b" .
from * ** show "(f ⊓ g) a ≤ (f ⊓ g) b" by auto
qed

lemma (in semilattice_sup) mono_sup [simp]:
assumes "mono f" and "mono g"
shows "mono (f ⊔ g)"
proof
fix a b
assume "a ≤ b"
from ‹mono f› ‹a ≤ b› have "f a ≤ f b" by (auto elim: monoE)
also have "f b ≤ f b ⊔ g b" by simp
finally have *: "f a ≤ f b ⊔ g b" .
from ‹mono g› ‹a ≤ b› have "g a ≤ g b" by (auto elim: monoE)
also have "g b ≤ f b ⊔ g b" by simp
finally have **: "g a ≤ f b ⊔ g b" .
from * ** show "(f ⊔ g) a ≤ (f ⊔ g) b" by auto
qed

lemma (in complete_lattice) mono_Inf [simp]:
assumes "A ⊆ {f :: 'a ⇒ 'b:: complete_lattice. mono f}"
shows "mono (⨅A)"
proof
fix a b
assume "a ≤ b"
{ fix f
assume "f ∈ A"
with assms have "mono f" by auto
with ‹a ≤ b› have "f a ≤ f b" by (auto elim: monoE)
}
then have "(⨅f∈A. f a) ≤ (⨅f∈A. f b)"
by (auto intro: complete_lattice_class.INF_greatest complete_lattice_class.INF_lower2)
then show "(⨅A) a ≤ (⨅A) b" by simp
qed

lemma (in complete_lattice) mono_Sup [simp]:
assumes "A ⊆ {f :: 'a ⇒ 'b:: complete_lattice. mono f}"
shows "mono (⨆A)"
proof
fix a b
assume "a ≤ b"
{ fix f
assume "f ∈ A"
with assms have "mono f" by auto
with ‹a ≤ b› have "f a ≤ f b" by (auto elim: monoE)
}
then have "(⨆f∈A. f a) ≤ (⨆f∈A. f b)"
by (auto intro: complete_lattice_class.SUP_least complete_lattice_class.SUP_upper2)
then show "(⨆A) a ≤ (⨆A) b" by simp
qed

typedef (overloaded) 'a MonoTran = "{f::'a::order ⇒ 'a . mono f}"
proof
show "id ∈ ?MonoTran" by simp
qed

lemma [simp]:
"mono (Rep_MonoTran f)"
using Rep_MonoTran [of f] by simp

setup_lifting type_definition_MonoTran

instantiation MonoTran :: (order) order
begin

lift_definition less_eq_MonoTran :: "'a MonoTran ⇒ 'a MonoTran ⇒ bool"
is less_eq .

lift_definition less_MonoTran :: "'a MonoTran ⇒ 'a MonoTran ⇒ bool"
is less .

instance
by intro_classes (transfer, auto intro: order_antisym)+

end

instantiation MonoTran :: (order) monoid_mult
begin

lift_definition one_MonoTran :: "'a MonoTran"
is id
by (fact mono_id)

lift_definition times_MonoTran :: "'a MonoTran ⇒ 'a MonoTran ⇒ 'a MonoTran"
is comp
by (fact mono_comp)

instance
by intro_classes (transfer, auto)+

end

instantiation MonoTran :: (order_bot) order_bot
begin

lift_definition bot_MonoTran :: "'a MonoTran"
is ⊥
by (fact mono_bot)

instance
by intro_classes (transfer, simp)

end

instantiation MonoTran :: (order_top) order_top
begin

lift_definition top_MonoTran :: "'a MonoTran"
is ⊤
by (fact mono_top)

instance
by intro_classes (transfer, simp)

end

instantiation MonoTran :: (lattice) lattice
begin

lift_definition inf_MonoTran :: "'a MonoTran ⇒ 'a MonoTran ⇒ 'a MonoTran"
is inf
by (fact mono_inf)

lift_definition sup_MonoTran :: "'a MonoTran ⇒ 'a MonoTran ⇒ 'a MonoTran"
is sup
by (fact mono_sup)

instance
by intro_classes (transfer, simp)+

end

instance MonoTran :: (distrib_lattice) distrib_lattice
by intro_classes (transfer, rule sup_inf_distrib1)

instantiation MonoTran :: (complete_lattice) complete_lattice
begin

lift_definition Inf_MonoTran :: "'a MonoTran set ⇒ 'a MonoTran"
is Inf
by (rule mono_Inf) auto

lift_definition Sup_MonoTran :: "'a MonoTran set ⇒ 'a MonoTran"
is Sup
by (rule mono_Sup) auto

instance
by intro_classes (transfer, simp add: Inf_lower Sup_upper Inf_greatest Sup_least)+

end

context includes lifting_syntax
begin

lemma [transfer_rule]:
"(rel_set A ===> (A ===> pcr_MonoTran HOL.eq) ===> pcr_MonoTran HOL.eq) (λA f. ⨅(f ` A)) (λA f. ⨅(f ` A))"
by transfer_prover

lemma [transfer_rule]:
"(rel_set A ===> (A ===> pcr_MonoTran HOL.eq) ===> pcr_MonoTran HOL.eq) (λA f. ⨆(f ` A)) (λA f. ⨆(f ` A))"
by transfer_prover

end

instance MonoTran :: (complete_distrib_lattice) complete_distrib_lattice
proof (intro_classes, transfer)
fix A :: "('a ⇒ 'a) set set"
assume " ∀A∈A. Ball A mono"
from this have [simp]: "{f ` A |f. ∀Y∈A. f Y ∈ Y} = {x. (∃f. (∀x. (∀x∈x. mono x) ⟶ mono (f x)) ∧ x = f ` A ∧ (∀Y∈A. f Y ∈ Y)) ∧ (∀x∈x. mono x)}"
apply safe
apply (rule_tac x = "λ x . if x ∈ A then f x else ⊥" in exI)
by blast+

show " ⨅(Sup ` A) ≤ ⨆(Inf ` {x. (∃f∈Collect (pred_fun (λA. Ball A mono) mono). x = f ` A ∧ (∀Y∈A. f Y ∈ Y)) ∧ Ball x mono})"
qed

definition
"dual_fun (f::'a::boolean_algebra ⇒ 'a) = uminus ∘ f ∘ uminus"

lemma dual_fun_apply [simp]:
"dual_fun f p = - f (- p)"

lemma mono_dual_fun [simp]:
"mono f ⟹ mono (dual_fun f)"
apply (rule monoI)
apply (erule monoE)
apply auto
done

lemma (in order) mono_inf_fun [simp]:
fixes x :: "'b::semilattice_inf"
shows "mono (inf x)"
by (auto intro!: order_class.monoI semilattice_inf_class.inf_mono)

lemma (in order) mono_sup_fun [simp]:
fixes x :: "'b::semilattice_sup"
shows "mono (sup x)"
by (auto intro!: order_class.monoI semilattice_sup_class.sup_mono)

lemma mono_comp_fun:
fixes f :: "'a::order ⇒ 'b::order"
shows "mono f ⟹ mono ((∘) f)"
by (rule monoI) (auto simp add: le_fun_def elim: monoE)

definition
"Omega_fun f g = inf g ∘ comp f"

lemma Omega_fun_apply [simp]:
"Omega_fun f g h p = (g p ⊓ f (h p))"

lemma mono_Omega_fun [simp]:
"mono f ⟹ mono (Omega_fun f g)"
unfolding Omega_fun_def
by (auto intro: mono_comp mono_comp_fun)

lemma mono_mono_Omega_fun [simp]:
fixes f :: "'b::order ⇒ 'a::semilattice_inf" and g :: "'c::semilattice_inf ⇒ 'a"
shows "mono f ⟹ mono g ⟹ mono_mono (Omega_fun f g)"
apply (auto simp add: mono_mono_def Omega_fun_def)
apply (rule mono_comp)
apply (rule mono_inf_fun)
apply (rule mono_comp_fun)
apply assumption
done

definition
"omega_fun f = lfp (Omega_fun f id)"

definition
"star_fun f = gfp (Omega_fun f id)"

lemma mono_omega_fun [simp]:
fixes f :: "'a::complete_lattice ⇒ 'a"
assumes "mono f"
shows "mono (omega_fun f)"
proof
fix a b :: 'a
assume "a ≤ b"
from assms have "mono (lfp (Omega_fun f id))"
by (auto intro: mono_mono_Omega_fun)
with ‹a ≤ b› show "omega_fun f a ≤ omega_fun f b"
by (auto simp add: omega_fun_def elim: monoE)
qed

lemma mono_star_fun [simp]:
fixes f :: "'a::complete_lattice ⇒ 'a"
assumes "mono f"
shows "mono (star_fun f)"
proof
fix a b :: 'a
assume "a ≤ b"
from assms have "mono (gfp (Omega_fun f id))"
by (auto intro: mono_mono_Omega_fun)
with ‹a ≤ b› show "star_fun f a ≤ star_fun f b"
by (auto simp add: star_fun_def elim: monoE)
qed

lemma lfp_omega_lowerbound:
"mono f ⟹ Omega_fun f g A ≤ A ⟹ omega_fun f ∘ g ≤ A"
apply (rule_tac P = "λ x . x ∘ g ≤ A" and f = "Omega_fun f id" in lfp_ordinal_induct)
apply simp_all
apply (simp add: le_fun_def o_def inf_fun_def id_def Omega_fun_def)
apply auto
apply (rule_tac y = "f (A x) ⊓ g x" in order_trans)
apply simp_all
apply (rule_tac y = "f (S (g x))" in order_trans)
apply simp_all
apply (unfold Sup_comp_fun)
apply (rule SUP_least)
by auto

lemma gfp_omega_upperbound:
"mono f ⟹ A ≤ Omega_fun f g A ⟹ A ≤ star_fun f ∘ g"
apply (rule_tac P = "λ x . A ≤ x ∘ g" and f = "Omega_fun f id" in gfp_ordinal_induct)
apply simp_all
apply (simp add: le_fun_def o_def inf_fun_def id_def Omega_fun_def)
apply auto
apply (rule_tac y = "f (A x) ⊓ g x" in order_trans)
apply simp_all
apply (rule_tac y = "f (A x)" in order_trans)
apply simp_all
apply (unfold Inf_comp_fun)
apply (rule INF_greatest)
by auto

lemma lfp_omega_greatest:
assumes "⋀u. Omega_fun f g u ≤ u ⟹ A ≤ u"
shows "A ≤ omega_fun f ∘ g"
apply (unfold omega_fun_def)
apply (unfold Inf_comp_fun)
apply (rule INF_greatest)
apply simp
apply (rule assms)
done

lemma gfp_star_least:
assumes "⋀u. u ≤ Omega_fun f g u ⟹ u ≤ A"
shows "star_fun f ∘ g ≤ A"
apply (unfold star_fun_def)
apply (unfold Sup_comp_fun)
apply (rule SUP_least)
apply simp
apply (rule assms)
done

lemma lfp_omega:
"mono f ⟹ omega_fun f ∘ g = lfp (Omega_fun f g)"
apply (rule antisym)
apply (rule lfp_omega_lowerbound)
apply simp_all
apply (rule Inf_greatest)
apply safe
apply (rule_tac y = "Omega_fun f g x" in order_trans)
apply simp_all
apply (rule_tac f = " Omega_fun f g" in monoD)
apply simp_all
apply (rule Inf_lower)
apply simp
apply (rule lfp_omega_greatest)
apply (rule Inf_lower)
by simp

lemma gfp_star:
"mono f ⟹ star_fun f ∘ g = gfp (Omega_fun f g)"
apply (rule antisym)
apply (rule gfp_star_least)
apply (rule Sup_upper, simp)
apply (rule gfp_omega_upperbound)
apply simp_all
apply (rule Sup_least)
apply safe
apply (rule_tac y = "Omega_fun f g x" in order_trans)
apply simp_all
apply (rule_tac f = " Omega_fun f g" in monoD)
apply simp_all
apply (rule Sup_upper)
by simp

definition
"assert_fun p q = (p ⊓ q :: 'a::semilattice_inf)"

lemma mono_assert_fun [simp]:
"mono (assert_fun p)"
apply (simp add: assert_fun_def mono_def, safe)
by (rule_tac y = x in order_trans, simp_all)

lemma assert_fun_le_id [simp]: "assert_fun p ≤ id"
by (simp add: assert_fun_def id_def le_fun_def)

lemma assert_fun_disjunctive [simp]: "assert_fun (p::'a::distrib_lattice) ∈ Apply.disjunctive"
by (simp add: assert_fun_def Apply.disjunctive_def inf_sup_distrib)

definition
"assertion_fun = range assert_fun"

lemma assert_cont:
"(x :: 'a::boolean_algebra ⇒ 'a)  ≤ id ⟹ x ∈ Apply.disjunctive ⟹ x = assert_fun (x ⊤)"
apply (rule antisym)
apply (simp_all add: le_fun_def assert_fun_def, safe)
apply (rule_tac f = x in  monoD, simp_all)
apply (subgoal_tac "x top = sup (x xa) (x (-xa))")
apply simp
apply (subst inf_sup_distrib)
apply simp
apply (rule_tac y = "inf (- xa) xa" in order_trans)
supply [[simproc del: boolean_algebra_cancel_inf]]
apply (simp del: compl_inf_bot)
apply (rule_tac y = "x (- xa)" in order_trans)
apply simp
apply simp
apply simp
apply (cut_tac x = x and y = xa and z = "-xa" in Apply.disjunctiveD, simp)
apply (subst (asm) sup_commute)
apply (subst (asm) compl_sup_top)
by simp

lemma assertion_fun_disj_less_one: "assertion_fun = Apply.disjunctive ∩ {x::'a::boolean_algebra ⇒ 'a . x ≤ id}"
apply safe
apply (rule_tac x = "x ⊤" in exI)
by (rule assert_cont, simp_all)

lemma assert_fun_dual: "((assert_fun p) o ⊤) ⊓ (dual_fun (assert_fun p)) = assert_fun p"
by (simp add: fun_eq_iff inf_fun_def dual_fun_def o_def assert_fun_def top_fun_def inf_sup_distrib)

lemma assertion_fun_dual: "x ∈ assertion_fun ⟹ (x o ⊤) ⊓ (dual_fun x) = x"