--- a/src/HOL/Library/Order_Continuity.thy Thu Jul 02 16:14:20 2015 +0200
+++ b/src/HOL/Library/Order_Continuity.thy Fri Jul 03 08:26:34 2015 +0200
@@ -5,7 +5,7 @@
section \<open>Continuity and iterations (of set transformers)\<close>
theory Order_Continuity
-imports Main
+imports Complex_Main
begin
(* TODO: Generalize theory to chain-complete partial orders *)
@@ -34,6 +34,8 @@
and have the advantage that these names are duals.
\<close>
+named_theorems order_continuous_intros
+
subsection \<open>Continuity for complete lattices\<close>
definition
@@ -55,12 +57,13 @@
by (simp add: SUP_nat_binary le_iff_sup)
qed
-lemma sup_continuous_intros:
+lemma [order_continuous_intros]:
shows sup_continuous_const: "sup_continuous (\<lambda>x. c)"
and sup_continuous_id: "sup_continuous (\<lambda>x. x)"
and sup_continuous_apply: "sup_continuous (\<lambda>f. f x)"
and sup_continuous_fun: "(\<And>s. sup_continuous (\<lambda>x. P x s)) \<Longrightarrow> sup_continuous P"
- by (auto simp: sup_continuous_def)
+ and sup_continuous_If: "sup_continuous F \<Longrightarrow> sup_continuous G \<Longrightarrow> sup_continuous (\<lambda>f. if C then F f else G f)"
+ by (auto simp: sup_continuous_def)
lemma sup_continuous_compose:
assumes f: "sup_continuous f" and g: "sup_continuous g"
@@ -74,6 +77,38 @@
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 \<Longrightarrow> sup_continuous g \<Longrightarrow> sup_continuous (\<lambda>x. sup (f x) (g x))"
+ by (simp add: sup_continuous_def SUP_sup_distrib)
+
+lemma sup_continuous_inf[order_continuous_intros]:
+ fixes P Q :: "'a :: complete_lattice \<Rightarrow> 'b :: complete_distrib_lattice"
+ assumes P: "sup_continuous P" and Q: "sup_continuous Q"
+ shows "sup_continuous (\<lambda>x. inf (P x) (Q x))"
+ unfolding sup_continuous_def
+proof (safe intro!: antisym)
+ fix M :: "nat \<Rightarrow> 'a" assume M: "incseq M"
+ have "inf (P (SUP i. M i)) (Q (SUP i. M i)) \<le> (SUP j i. inf (P (M i)) (Q (M j)))"
+ unfolding sup_continuousD[OF P M] sup_continuousD[OF Q M] inf_SUP SUP_inf ..
+ also have "\<dots> \<le> (SUP i. inf (P (M i)) (Q (M i)))"
+ proof (intro SUP_least)
+ fix i j from M assms[THEN sup_continuous_mono] show "inf (P (M i)) (Q (M j)) \<le> (SUP i. inf (P (M i)) (Q (M i)))"
+ by (intro SUP_upper2[of "sup i j"] inf_mono) (auto simp: mono_def)
+ qed
+ finally show "inf (P (SUP i. M i)) (Q (SUP i. M i)) \<le> (SUP i. inf (P (M i)) (Q (M i)))" .
+
+ show "(SUP i. inf (P (M i)) (Q (M i))) \<le> inf (P (SUP i. M i)) (Q (SUP i. M i))"
+ unfolding sup_continuousD[OF P M] sup_continuousD[OF Q M] by (intro SUP_least inf_mono SUP_upper)
+qed
+
+lemma sup_continuous_and[order_continuous_intros]:
+ "sup_continuous P \<Longrightarrow> sup_continuous Q \<Longrightarrow> sup_continuous (\<lambda>x. P x \<and> Q x)"
+ using sup_continuous_inf[of P Q] by simp
+
+lemma sup_continuous_or[order_continuous_intros]:
+ "sup_continuous P \<Longrightarrow> sup_continuous Q \<Longrightarrow> sup_continuous (\<lambda>x. P x \<or> 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)
@@ -122,6 +157,51 @@
unfolding sup_continuous_lfp[OF g] by simp
qed
+lemma lfp_transfer_bounded:
+ assumes P: "P bot" "\<And>x. P x \<Longrightarrow> P (f x)" "\<And>M. (\<And>i. P (M i)) \<Longrightarrow> 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]: "\<And>x. P x \<Longrightarrow> \<alpha> (f x) = g (\<alpha> x)"
+ assumes g_bound: "\<And>x. \<alpha> bot \<le> g x"
+ shows "\<alpha> (lfp f) = lfp g"
+proof (rule antisym)
+ note mono_g = sup_continuous_mono[OF g]
+ have lfp_bound: "\<alpha> bot \<le> 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 (\<lambda>i. (f ^^ i) bot)"
+ unfolding mono_iff_le_Suc
+ proof
+ fix i show "(f ^^ i) bot \<le> (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 "\<alpha> (lfp f) = (SUP i. \<alpha> ((f^^i) bot))"
+ unfolding sup_continuous_lfp[OF f] using incseq_pow P_pow by (rule \<alpha>)
+ also have "\<dots> \<le> lfp g"
+ proof (rule SUP_least)
+ fix i show "\<alpha> ((f^^i) bot) \<le> 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)
+ qed (simp add: lfp_bound)
+ qed
+ finally show "\<alpha> (lfp f) \<le> lfp g" .
+
+ show "lfp g \<le> \<alpha> (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
+
definition
inf_continuous :: "('a::complete_lattice \<Rightarrow> 'b::complete_lattice) \<Rightarrow> bool" where
"inf_continuous F \<longleftrightarrow> (\<forall>M::nat \<Rightarrow> 'a. antimono M \<longrightarrow> F (INF i. M i) = (INF i. F (M i)))"
@@ -141,12 +221,45 @@
by (simp add: INF_nat_binary le_iff_inf inf_commute)
qed
-lemma inf_continuous_intros:
+lemma [order_continuous_intros]:
shows inf_continuous_const: "inf_continuous (\<lambda>x. c)"
and inf_continuous_id: "inf_continuous (\<lambda>x. x)"
and inf_continuous_apply: "inf_continuous (\<lambda>f. f x)"
and inf_continuous_fun: "(\<And>s. inf_continuous (\<lambda>x. P x s)) \<Longrightarrow> inf_continuous P"
- by (auto simp: inf_continuous_def)
+ and inf_continuous_If: "inf_continuous F \<Longrightarrow> inf_continuous G \<Longrightarrow> inf_continuous (\<lambda>f. if C then F f else G f)"
+ by (auto simp: inf_continuous_def)
+
+lemma inf_continuous_inf[order_continuous_intros]:
+ "inf_continuous f \<Longrightarrow> inf_continuous g \<Longrightarrow> inf_continuous (\<lambda>x. inf (f x) (g x))"
+ by (simp add: inf_continuous_def INF_inf_distrib)
+
+lemma inf_continuous_sup[order_continuous_intros]:
+ fixes P Q :: "'a :: complete_lattice \<Rightarrow> 'b :: complete_distrib_lattice"
+ assumes P: "inf_continuous P" and Q: "inf_continuous Q"
+ shows "inf_continuous (\<lambda>x. sup (P x) (Q x))"
+ unfolding inf_continuous_def
+proof (safe intro!: antisym)
+ fix M :: "nat \<Rightarrow> 'a" assume M: "decseq M"
+ show "sup (P (INF i. M i)) (Q (INF i. M i)) \<le> (INF i. sup (P (M i)) (Q (M i)))"
+ unfolding inf_continuousD[OF P M] inf_continuousD[OF Q M] by (intro INF_greatest sup_mono INF_lower)
+
+ have "(INF i. sup (P (M i)) (Q (M i))) \<le> (INF j i. sup (P (M i)) (Q (M j)))"
+ proof (intro INF_greatest)
+ fix i j from M assms[THEN inf_continuous_mono] show "sup (P (M i)) (Q (M j)) \<ge> (INF i. sup (P (M i)) (Q (M i)))"
+ by (intro INF_lower2[of "sup i j"] sup_mono) (auto simp: mono_def antimono_def)
+ qed
+ also have "\<dots> \<le> sup (P (INF i. M i)) (Q (INF i. M i))"
+ unfolding inf_continuousD[OF P M] inf_continuousD[OF Q M] INF_sup sup_INF ..
+ finally show "sup (P (INF i. M i)) (Q (INF i. M i)) \<ge> (INF i. sup (P (M i)) (Q (M i)))" .
+qed
+
+lemma inf_continuous_and[order_continuous_intros]:
+ "inf_continuous P \<Longrightarrow> inf_continuous Q \<Longrightarrow> inf_continuous (\<lambda>x. P x \<and> Q x)"
+ using inf_continuous_inf[of P Q] by simp
+
+lemma inf_continuous_or[order_continuous_intros]:
+ "inf_continuous P \<Longrightarrow> inf_continuous Q \<Longrightarrow> inf_continuous (\<lambda>x. P x \<or> 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"
@@ -208,4 +321,70 @@
unfolding inf_continuous_gfp[OF g] by simp
qed
+lemma gfp_transfer_bounded:
+ assumes P: "P (f top)" "\<And>x. P x \<Longrightarrow> P (f x)" "\<And>M. antimono M \<Longrightarrow> (\<And>i. P (M i)) \<Longrightarrow> 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]: "\<And>x. P x \<Longrightarrow> \<alpha> (f x) = g (\<alpha> x)"
+ assumes g_bound: "\<And>x. g x \<le> \<alpha> (f top)"
+ shows "\<alpha> (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 (\<lambda>i. (f ^^ i) top)"
+ unfolding antimono_iff_le_Suc
+ proof
+ fix i show "(f ^^ Suc i) top \<le> (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 (\<lambda>i. (f ^^ i) (f top))"
+ proof
+ show "x \<le> y \<Longrightarrow> (f ^^ y) (f top) \<le> (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 "\<exists>j\<in>UNIV. (f ^^ j) (f top) \<le> (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 "\<exists>j\<in>UNIV. (f ^^ j) top \<le> (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 "\<alpha> (gfp f) = (INF i. \<alpha> ((f^^i) (f top)))"
+ unfolding gfp_f by (rule \<alpha>) (auto intro!: P_pow antimono_pow2)
+ also have "\<dots> \<ge> gfp g"
+ proof (rule INF_greatest)
+ fix i show "gfp g \<le> \<alpha> ((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 \<le> \<alpha> (f top)"
+ by (subst gfp_unfold[OF mono_g]) (rule g_bound)
+ then show ?case
+ by simp
+ qed
+ qed
+ finally show "gfp g \<le> \<alpha> (gfp f)" .
+
+ show "\<alpha> (gfp f) \<le> 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
+
end