Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
Order_Continuity.thy
Sprache: Unknown
(* 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.4 Sekunden
(vorverarbeitet)
]
|
|
