Theory Order_Continuity

(*  Title:      HOL/Library/Order_Continuity.thy
    Author:     David von Oheimb, TU München
    Author:     Johannes Hölzl, TU München
*)

section ‹Continuity and iterations›

theory Order_Continuity
imports Complex_Main Countable_Complete_Lattices
begin

(* TODO: Generalize theory to chain-complete partial orders *)

lemma SUP_nat_binary:
  "(sup A (SUP xCollect ((<) (0::nat)). B)) = (sup A B::'a::countable_complete_lattice)"
  apply (subst image_constant)
   apply auto
  done

lemma INF_nat_binary:
  "inf A (INF xCollect ((<) (0::nat)). B) = (inf A B::'a::countable_complete_lattice)"
  apply (subst image_constant)
   apply auto
  done

text ‹
  The name continuous› is already taken in Complex_Main›, so we use
  sup_continuous› and inf_continuous›. These names appear sometimes in literature
  and have the advantage that these names are duals.
›

named_theorems order_continuous_intros

subsection ‹Continuity for complete lattices›

definition
  sup_continuous :: "('a::countable_complete_lattice  'b::countable_complete_lattice)  bool"
where
  "sup_continuous F  (M::nat  'a. mono M  F (SUP i. M i) = (SUP i. F (M i)))"

lemma sup_continuousD: "sup_continuous F  mono M  F (SUP i::nat. M i) = (SUP i. F (M i))"
  by (auto simp: sup_continuous_def)

lemma sup_continuous_mono:
  "mono F" if "sup_continuous F"
proof
  fix A B :: "'a"
  assume "A  B"
  let ?f = "λn::nat. if n = 0 then A else B"
  from A  B have "incseq ?f"
    by (auto intro: monoI)
  with sup_continuous F have *: "F (SUP i. ?f i) = (SUP i. F (?f i))"
    by (auto dest: sup_continuousD)
  from A  B have "B = sup A B"
    by (simp add: le_iff_sup)
  then have "F B = F (sup A B)"
    by simp
  also have " = sup (F A) (F B)"
    using * by (simp add: if_distrib SUP_nat_binary cong del: SUP_cong)
  finally show "F A  F B"
    by (simp add: le_iff_sup)
qed

lemma [order_continuous_intros]:
  shows sup_continuous_const: "sup_continuous (λx. c)"
    and sup_continuous_id: "sup_continuous (λx. x)"
    and sup_continuous_apply: "sup_continuous (λf. f x)"
    and sup_continuous_fun: "(s. sup_continuous (λx. P x s))  sup_continuous P"
    and sup_continuous_If: "sup_continuous F  sup_continuous G  sup_continuous (λf. if C then F f else G f)"
  by (auto simp: sup_continuous_def image_comp)

lemma sup_continuous_compose:
  assumes f: "sup_continuous f" and g: "sup_continuous g"
  shows "sup_continuous (λx. f (g x))"
  unfolding sup_continuous_def
proof safe
  fix M :: "nat  'c"
  assume M: "mono M"
  then have "mono (λi. g (M i))"
    using sup_continuous_mono[OF g] by (auto simp: mono_def)
  with M show "f (g (Sup (M ` UNIV))) = (SUP i. f (g (M i)))"
    by (auto simp: sup_continuous_def g[THEN sup_continuousD] f[THEN sup_continuousD])
qed

lemma sup_continuous_sup[order_continuous_intros]:
  "sup_continuous f  sup_continuous g  sup_continuous (λx. sup (f x) (g x))"
  by (simp add: sup_continuous_def ccSUP_sup_distrib)

lemma sup_continuous_inf[order_continuous_intros]:
  fixes P Q :: "'a :: countable_complete_lattice  'b :: countable_complete_distrib_lattice"
  assumes P: "sup_continuous P" and Q: "sup_continuous Q"
  shows "sup_continuous (λx. inf (P x) (Q x))"
  unfolding sup_continuous_def
proof (safe intro!: antisym)
  fix M :: "nat  'a" assume M: "incseq M"
  have "inf (P (SUP i. M i)) (Q (SUP i. M i))  (SUP j i. inf (P (M i)) (Q (M j)))"
    by (simp add: sup_continuousD[OF P M] sup_continuousD[OF Q M] inf_ccSUP ccSUP_inf)
  also have "  (SUP i. inf (P (M i)) (Q (M i)))"
  proof (intro ccSUP_least)
    fix i j from M assms[THEN sup_continuous_mono] show "inf (P (M i)) (Q (M j))  (SUP i. inf (P (M i)) (Q (M i)))"
      by (intro ccSUP_upper2[of _ "sup i j"] inf_mono) (auto simp: mono_def)
  qed auto
  finally show "inf (P (SUP i. M i)) (Q (SUP i. M i))  (SUP i. inf (P (M i)) (Q (M i)))" .

  show "(SUP i. inf (P (M i)) (Q (M i)))  inf (P (SUP i. M i)) (Q (SUP i. M i))"
    unfolding sup_continuousD[OF P M] sup_continuousD[OF Q M] by (intro ccSUP_least inf_mono ccSUP_upper) auto
qed

lemma sup_continuous_and[order_continuous_intros]:
  "sup_continuous P  sup_continuous Q  sup_continuous (λx. P x  Q x)"
  using sup_continuous_inf[of P Q] by simp

lemma sup_continuous_or[order_continuous_intros]:
  "sup_continuous P  sup_continuous Q  sup_continuous (λx. P x  Q x)"
  by (auto simp: sup_continuous_def)

lemma sup_continuous_lfp:
  assumes "sup_continuous F" shows "lfp F = (SUP i. (F ^^ i) bot)" (is "lfp F = ?U")
proof (rule antisym)
  note mono = sup_continuous_mono[OF sup_continuous F]
  show "?U  lfp F"
  proof (rule SUP_least)
    fix i show "(F ^^ i) bot  lfp F"
    proof (induct i)
      case (Suc i)
      have "(F ^^ Suc i) bot = F ((F ^^ i) bot)" by simp
      also have "  F (lfp F)" by (rule monoD[OF mono Suc])
      also have " = lfp F" by (simp add: lfp_fixpoint[OF mono])
      finally show ?case .
    qed simp
  qed
  show "lfp F  ?U"
  proof (rule lfp_lowerbound)
    have "mono (λi::nat. (F ^^ i) bot)"
    proof -
      { fix i::nat have "(F ^^ i) bot  (F ^^ (Suc i)) bot"
        proof (induct i)
          case 0 show ?case by simp
        next
          case Suc thus ?case using monoD[OF mono Suc] by auto
        qed }
      thus ?thesis by (auto simp add: mono_iff_le_Suc)
    qed
    hence "F ?U = (SUP i. (F ^^ Suc i) bot)"
      using sup_continuous F by (simp add: sup_continuous_def)
    also have "  ?U"
      by (fast intro: SUP_least SUP_upper)
    finally show "F ?U  ?U" .
  qed
qed

lemma lfp_transfer_bounded:
  assumes P: "P bot" "x. P x  P (f x)" "M. (i. P (M i))  P (SUP i::nat. M i)"
  assumes α: "M. mono M  (i::nat. P (M i))  α (SUP i. M i) = (SUP i. α (M i))"
  assumes f: "sup_continuous f" and g: "sup_continuous g"
  assumes [simp]: "x. P x  x  lfp f  α (f x) = g (α x)"
  assumes g_bound: "x. α bot  g x"
  shows "α (lfp f) = lfp g"
proof (rule antisym)
  note mono_g = sup_continuous_mono[OF g]
  note mono_f = sup_continuous_mono[OF f]
  have lfp_bound: "α bot  lfp g"
    by (subst lfp_unfold[OF mono_g]) (rule g_bound)

  have P_pow: "P ((f ^^ i) bot)" for i
    by (induction i) (auto intro!: P)
  have incseq_pow: "mono (λi. (f ^^ i) bot)"
    unfolding mono_iff_le_Suc
  proof
    fix i show "(f ^^ i) bot  (f ^^ (Suc i)) bot"
    proof (induct i)
      case Suc thus ?case using monoD[OF sup_continuous_mono[OF f] Suc] by auto
    qed (simp add: le_fun_def)
  qed
  have P_lfp: "P (lfp f)"
    using P_pow unfolding sup_continuous_lfp[OF f] by (auto intro!: P)

  have iter_le_lfp: "(f ^^ n) bot  lfp f" for n
    apply (induction n)
    apply simp
    apply (subst lfp_unfold[OF mono_f])
    apply (auto intro!: monoD[OF mono_f])
    done

  have "α (lfp f) = (SUP i. α ((f^^i) bot))"
    unfolding sup_continuous_lfp[OF f] using incseq_pow P_pow by (rule α)
  also have "  lfp g"
  proof (rule SUP_least)
    fix i show "α ((f^^i) bot)  lfp g"
    proof (induction i)
      case (Suc n) then show ?case
        by (subst lfp_unfold[OF mono_g]) (simp add: monoD[OF mono_g] P_pow iter_le_lfp)
    qed (simp add: lfp_bound)
  qed
  finally show "α (lfp f)  lfp g" .

  show "lfp g  α (lfp f)"
  proof (induction rule: lfp_ordinal_induct[OF mono_g])
    case (1 S) then show ?case
      by (subst lfp_unfold[OF sup_continuous_mono[OF f]])
         (simp add: monoD[OF mono_g] P_lfp)
  qed (auto intro: Sup_least)
qed

lemma lfp_transfer:
  "sup_continuous α  sup_continuous f  sup_continuous g 
    (x. α bot  g x)  (x. x  lfp f  α (f x) = g (α x))  α (lfp f) = lfp g"
  by (rule lfp_transfer_bounded[where P=top]) (auto dest: sup_continuousD)

definition
  inf_continuous :: "('a::countable_complete_lattice  'b::countable_complete_lattice)  bool"
where
  "inf_continuous F  (M::nat  'a. antimono M  F (INF i. M i) = (INF i. F (M i)))"

lemma inf_continuousD: "inf_continuous F  antimono M  F (INF i::nat. M i) = (INF i. F (M i))"
  by (auto simp: inf_continuous_def)

lemma inf_continuous_mono:
  "mono F" if "inf_continuous F"
proof
  fix A B :: "'a"
  assume "A  B"
  let ?f = "λn::nat. if n = 0 then B else A"
  from A  B have "decseq ?f"
    by (auto intro: antimonoI)
  with inf_continuous F have *: "F (INF i. ?f i) = (INF i. F (?f i))"
    by (auto dest: inf_continuousD)
  from A  B have "A = inf B A"
    by (simp add: inf.absorb_iff2)
  then have "F A = F (inf B A)"
    by simp
  also have " = inf (F B) (F A)"
    using * by (simp add: if_distrib INF_nat_binary cong del: INF_cong)
  finally show "F A  F B"
    by (simp add: inf.absorb_iff2)
qed

lemma [order_continuous_intros]:
  shows inf_continuous_const: "inf_continuous (λx. c)"
    and inf_continuous_id: "inf_continuous (λx. x)"
    and inf_continuous_apply: "inf_continuous (λf. f x)"
    and inf_continuous_fun: "(s. inf_continuous (λx. P x s))  inf_continuous P"
    and inf_continuous_If: "inf_continuous F  inf_continuous G  inf_continuous (λf. if C then F f else G f)"
  by (auto simp: inf_continuous_def image_comp)

lemma inf_continuous_inf[order_continuous_intros]:
  "inf_continuous f  inf_continuous g  inf_continuous (λx. inf (f x) (g x))"
  by (simp add: inf_continuous_def ccINF_inf_distrib)

lemma inf_continuous_sup[order_continuous_intros]:
  fixes P Q :: "'a :: countable_complete_lattice  'b :: countable_complete_distrib_lattice"
  assumes P: "inf_continuous P" and Q: "inf_continuous Q"
  shows "inf_continuous (λx. sup (P x) (Q x))"
  unfolding inf_continuous_def
proof (safe intro!: antisym)
  fix M :: "nat  'a" assume M: "decseq M"
  show "sup (P (INF i. M i)) (Q (INF i. M i))  (INF i. sup (P (M i)) (Q (M i)))"
    unfolding inf_continuousD[OF P M] inf_continuousD[OF Q M] by (intro ccINF_greatest sup_mono ccINF_lower) auto

  have "(INF i. sup (P (M i)) (Q (M i)))  (INF j i. sup (P (M i)) (Q (M j)))"
  proof (intro ccINF_greatest)
    fix i j from M assms[THEN inf_continuous_mono] show "sup (P (M i)) (Q (M j))  (INF i. sup (P (M i)) (Q (M i)))"
      by (intro ccINF_lower2[of _ "sup i j"] sup_mono) (auto simp: mono_def antimono_def)
  qed auto
  also have "  sup (P (INF i. M i)) (Q (INF i. M i))"
    by (simp add: inf_continuousD[OF P M] inf_continuousD[OF Q M] ccINF_sup sup_ccINF)
  finally show "sup (P (INF i. M i)) (Q (INF i. M i))  (INF i. sup (P (M i)) (Q (M i)))" .
qed

lemma inf_continuous_and[order_continuous_intros]:
  "inf_continuous P  inf_continuous Q  inf_continuous (λx. P x  Q x)"
  using inf_continuous_inf[of P Q] by simp

lemma inf_continuous_or[order_continuous_intros]:
  "inf_continuous P  inf_continuous Q  inf_continuous (λx. P x  Q x)"
  using inf_continuous_sup[of P Q] by simp

lemma inf_continuous_compose:
  assumes f: "inf_continuous f" and g: "inf_continuous g"
  shows "inf_continuous (λx. f (g x))"
  unfolding inf_continuous_def
proof safe
  fix M :: "nat  'c"
  assume M: "antimono M"
  then have "antimono (λi. g (M i))"
    using inf_continuous_mono[OF g] by (auto simp: mono_def antimono_def)
  with M show "f (g (Inf (M ` UNIV))) = (INF i. f (g (M i)))"
    by (auto simp: inf_continuous_def g[THEN inf_continuousD] f[THEN inf_continuousD])
qed

lemma inf_continuous_gfp:
  assumes "inf_continuous F" shows "gfp F = (INF i. (F ^^ i) top)" (is "gfp F = ?U")
proof (rule antisym)
  note mono = inf_continuous_mono[OF inf_continuous F]
  show "gfp F  ?U"
  proof (rule INF_greatest)
    fix i show "gfp F  (F ^^ i) top"
    proof (induct i)
      case (Suc i)
      have "gfp F = F (gfp F)" by (simp add: gfp_fixpoint[OF mono])
      also have "  F ((F ^^ i) top)" by (rule monoD[OF mono Suc])
      also have " = (F ^^ Suc i) top" by simp
      finally show ?case .
    qed simp
  qed
  show "?U  gfp F"
  proof (rule gfp_upperbound)
    have *: "antimono (λi::nat. (F ^^ i) top)"
    proof -
      { fix i::nat have "(F ^^ Suc i) top  (F ^^ i) top"
        proof (induct i)
          case 0 show ?case by simp
        next
          case Suc thus ?case using monoD[OF mono Suc] by auto
        qed }
      thus ?thesis by (auto simp add: antimono_iff_le_Suc)
    qed
    have "?U  (INF i. (F ^^ Suc i) top)"
      by (fast intro: INF_greatest INF_lower)
    also have "  F ?U"
      by (simp add: inf_continuousD inf_continuous F *)
    finally show "?U  F ?U" .
  qed
qed

lemma gfp_transfer:
  assumes α: "inf_continuous α" and f: "inf_continuous f" and g: "inf_continuous g"
  assumes [simp]: "α top = top" "x. α (f x) = g (α x)"
  shows "α (gfp f) = gfp g"
proof -
  have "α (gfp f) = (INF i. α ((f^^i) top))"
    unfolding inf_continuous_gfp[OF f] by (intro f α inf_continuousD antimono_funpow inf_continuous_mono)
  moreover have "α ((f^^i) top) = (g^^i) top" for i
    by (induction i; simp)
  ultimately show ?thesis
    unfolding inf_continuous_gfp[OF g] by simp
qed

lemma gfp_transfer_bounded:
  assumes P: "P (f top)" "x. P x  P (f x)" "M. antimono M  (i. P (M i))  P (INF i::nat. M i)"
  assumes α: "M. antimono M  (i::nat. P (M i))  α (INF i. M i) = (INF i. α (M i))"
  assumes f: "inf_continuous f" and g: "inf_continuous g"
  assumes [simp]: "x. P x  α (f x) = g (α x)"
  assumes g_bound: "x. g x  α (f top)"
  shows "α (gfp f) = gfp g"
proof (rule antisym)
  note mono_g = inf_continuous_mono[OF g]

  have P_pow: "P ((f ^^ i) (f top))" for i
    by (induction i) (auto intro!: P)

  have antimono_pow: "antimono (λi. (f ^^ i) top)"
    unfolding antimono_iff_le_Suc
  proof
    fix i show "(f ^^ Suc i) top  (f ^^ i) top"
    proof (induct i)
      case Suc thus ?case using monoD[OF inf_continuous_mono[OF f] Suc] by auto
    qed (simp add: le_fun_def)
  qed
  have antimono_pow2: "antimono (λi. (f ^^ i) (f top))"
  proof
    show "x  y  (f ^^ y) (f top)  (f ^^ x) (f top)" for x y
      using antimono_pow[THEN antimonoD, of "Suc x" "Suc y"]
      unfolding funpow_Suc_right by simp
  qed

  have gfp_f: "gfp f = (INF i. (f ^^ i) (f top))"
    unfolding inf_continuous_gfp[OF f]
  proof (rule INF_eq)
    show "jUNIV. (f ^^ j) (f top)  (f ^^ i) top" for i
      by (intro bexI[of _ "i - 1"]) (auto simp: diff_Suc funpow_Suc_right simp del: funpow.simps(2) split: nat.split)
    show "jUNIV. (f ^^ j) top  (f ^^ i) (f top)" for i
      by (intro bexI[of _ "Suc i"]) (auto simp: funpow_Suc_right simp del: funpow.simps(2))
  qed

  have P_lfp: "P (gfp f)"
    unfolding gfp_f by (auto intro!: P P_pow antimono_pow2)

  have "α (gfp f) = (INF i. α ((f^^i) (f top)))"
    unfolding gfp_f by (rule α) (auto intro!: P_pow antimono_pow2)
  also have "  gfp g"
  proof (rule INF_greatest)
    fix i show "gfp g  α ((f^^i) (f top))"
    proof (induction i)
      case (Suc n) then show ?case
        by (subst gfp_unfold[OF mono_g]) (simp add: monoD[OF mono_g] P_pow)
    next
      case 0
      have "gfp g  α (f top)"
        by (subst gfp_unfold[OF mono_g]) (rule g_bound)
      then show ?case
        by simp
    qed
  qed
  finally show "gfp g  α (gfp f)" .

  show "α (gfp f)  gfp g"
  proof (induction rule: gfp_ordinal_induct[OF mono_g])
    case (1 S) then show ?case
      by (subst gfp_unfold[OF inf_continuous_mono[OF f]])
         (simp add: monoD[OF mono_g] P_lfp)
  qed (auto intro: Inf_greatest)
qed

subsubsection ‹Least fixed points in countable complete lattices›

definition (in countable_complete_lattice) cclfp :: "('a  'a)  'a"
  where "cclfp f = (SUP i. (f ^^ i) bot)"

lemma cclfp_unfold:
  assumes "sup_continuous F" shows "cclfp F = F (cclfp F)"
proof -
  have "cclfp F = (SUP i. F ((F ^^ i) bot))"
    unfolding cclfp_def
    by (subst UNIV_nat_eq) (simp add: image_comp)
  also have " = F (cclfp F)"
    unfolding cclfp_def
    by (intro sup_continuousD[symmetric] assms mono_funpow sup_continuous_mono)
  finally show ?thesis .
qed

lemma cclfp_lowerbound: assumes f: "mono f" and A: "f A  A" shows "cclfp f  A"
  unfolding cclfp_def
proof (intro ccSUP_least)
  fix i show "(f ^^ i) bot  A"
  proof (induction i)
    case (Suc i) from monoD[OF f this] A show ?case
      by auto
  qed simp
qed simp

lemma cclfp_transfer:
  assumes "sup_continuous α" "mono f"
  assumes "α bot = bot" "x. α (f x) = g (α x)"
  shows "α (cclfp f) = cclfp g"
proof -
  have "α (cclfp f) = (SUP i. α ((f ^^ i) bot))"
    unfolding cclfp_def by (intro sup_continuousD assms mono_funpow sup_continuous_mono)
  moreover have "α ((f ^^ i) bot) = (g ^^ i) bot" for i
    by (induction i) (simp_all add: assms)
  ultimately show ?thesis
    by (simp add: cclfp_def)
qed

end