Theory 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 = (mM. m  f)"
  by (simp add: fun_eq_iff image_comp)

lemma INF_comp_fun:
  "(aA. g a)  f = (aA. g a  f)"
  by (simp add: fun_eq_iff image_comp)

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

lemma SUP_comp_fun:
  "(aA. g a)  f = (aA. 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 "(fA. f a)  (fA. 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 "(fA. f a)  (fA. 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 " AA. Ball A mono"
  from this have [simp]: "{f ` A |f. YA. f Y  Y} = {x. (f. (x. (xx. mono x)  mono (f x))  x = f ` A  (YA. f Y  Y))  (xx. 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. (fCollect (pred_fun (λA. Ball A mono) mono). x = f ` A  (YA. 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