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)"
  by (simp add: fun_eq_iff image_comp)

lemma INF_comp_fun:
  "(⨅a∈A. g a) ∘ f = (⨅a∈A. g a ∘ f)"
  by (simp add: fun_eq_iff image_comp)

lemma Sup_comp_fun:
  "⨆M ∘ f = (⨆m∈M. m ∘ f)"
  by (simp add: fun_eq_iff image_comp)

lemma SUP_comp_fun:
  "(⨆a∈A. g a) ∘ f = (⨆a∈A. g a ∘ f)"
  by (simp add: fun_eq_iff image_comp)

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)
      apply (simp add: if_split image_def)
    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})"
    by (simp add: Inf_Sup)
qed



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

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

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))"
  by (simp add: Omega_fun_def)

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 (simp add: omega_fun_def)
  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 (simp add: mono_def) apply (auto simp add: ac_simps)
  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 (simp add: star_fun_def)
  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 (simp add: mono_def)
  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 (simp add: lfp_def)
  apply (unfold Inf_comp_fun)
  apply (rule INF_greatest)
  apply simp
  apply (rule assms)
  apply (simp add: le_fun_def)
  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 (simp add: gfp_def)
  apply (unfold Sup_comp_fun)
  apply (rule SUP_least)
  apply simp
  apply (rule assms)
  apply (simp add: le_fun_def)
  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 (simp add: lfp_def)
  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 (simp add: lfp_def)
  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 (simp add: gfp_def)
  apply (rule Sup_upper, simp)
  apply (rule gfp_omega_upperbound)
  apply simp_all
  apply (simp add: gfp_def)
  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 (simp_all add: assertion_fun_def, auto simp add: image_def)
  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"
  by (simp add: assertion_fun_def, safe, simp add: assert_fun_dual)

lemma assertion_fun_MonoTran [simp]: "x ∈ assertion_fun ⟹ mono x"
  by (unfold assertion_fun_def, auto)

lemma assertion_fun_le_one [simp]: "x ∈ assertion_fun ⟹ x ≤ id"
  by (unfold assertion_fun_def, auto)

end