Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Order_Continuity.thy Sprache: Isabelle

Original von: Isabelle^©

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

section \<open>Continuity and iterations\<close>

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 x\Collect ((<) (0::nat)). B)) = (sup A B::'a::countable_complete_lattice)"
  apply (subst image_constant)
   apply auto
  done

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

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

named_theorems order_continuous_intros

subsection \<open>Continuity for complete lattices\<close>

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 \<open>A \<le> B\<close> have "incseq ?f"
    by (auto intro: monoI)
  with \<open>sup_continuous F\<close> have *: "F (SUP i. ?f i) = (SUP i. F (?f i))"
    by (auto dest: sup_continuousD)
  from \<open>A \<le> B\<close> 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 \<open>sup_continuous F\<close>]
  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 \<open>sup_continuous F\<close> 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 \<alpha>: "\<And>M. mono M \<Longrightarrow> (\<And>i::nat. P (M i)) \<Longrightarrow> \<alpha> (SUP i. M i) = (SUP i. \<alpha> (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 \<alpha>)
  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 \
    (\<And>x. \<alpha> bot \<le> g x) \<Longrightarrow> (\<And>x. x \<le> lfp f \<Longrightarrow> \<alpha> (f x) = g (\<alpha> x)) \<Longrightarrow> \<alpha> (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 \<open>A \<le> B\<close> have "decseq ?f"
    by (auto intro: antimonoI)
  with \<open>inf_continuous F\<close> have *: "F (INF i. ?f i) = (INF i. F (?f i))"
    by (auto dest: inf_continuousD)
  from \<open>A \<le> B\<close> 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 \<open>inf_continuous F\<close>]
  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 \<open>inf_continuous F\<close> *)
    finally show "?U \ F ?U" .
  qed
qed

lemma gfp_transfer:
  assumes \<alpha>: "inf_continuous \<alpha>" 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 \<alpha> 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 \<alpha>: "\<And>M. antimono M \<Longrightarrow> (\<And>i::nat. P (M i)) \<Longrightarrow> \<alpha> (INF i. M i) = (INF i. \<alpha> (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 "\j\UNIV. (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 "\j\UNIV. (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 \<alpha>) (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 \<open>Least fixed points in countable complete lattices\<close>

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

¤ Dauer der Verarbeitung: 0.30 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.