src/HOL/Library/Order_Continuity.thy
changeset 60636 ee18efe9b246
parent 60614 e39e6881985c
child 60714 ff8aa76d6d1c
     1.1 --- a/src/HOL/Library/Order_Continuity.thy	Thu Jul 02 16:14:20 2015 +0200
     1.2 +++ b/src/HOL/Library/Order_Continuity.thy	Fri Jul 03 08:26:34 2015 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  section \<open>Continuity and iterations (of set transformers)\<close>
     1.5  
     1.6  theory Order_Continuity
     1.7 -imports Main
     1.8 +imports Complex_Main
     1.9  begin
    1.10  
    1.11  (* TODO: Generalize theory to chain-complete partial orders *)
    1.12 @@ -34,6 +34,8 @@
    1.13    and have the advantage that these names are duals.
    1.14  \<close>
    1.15  
    1.16 +named_theorems order_continuous_intros
    1.17 +
    1.18  subsection \<open>Continuity for complete lattices\<close>
    1.19  
    1.20  definition
    1.21 @@ -55,12 +57,13 @@
    1.22      by (simp add: SUP_nat_binary le_iff_sup)
    1.23  qed
    1.24  
    1.25 -lemma sup_continuous_intros:
    1.26 +lemma [order_continuous_intros]:
    1.27    shows sup_continuous_const: "sup_continuous (\<lambda>x. c)"
    1.28      and sup_continuous_id: "sup_continuous (\<lambda>x. x)"
    1.29      and sup_continuous_apply: "sup_continuous (\<lambda>f. f x)"
    1.30      and sup_continuous_fun: "(\<And>s. sup_continuous (\<lambda>x. P x s)) \<Longrightarrow> sup_continuous P"
    1.31 - by (auto simp: sup_continuous_def)
    1.32 +    and sup_continuous_If: "sup_continuous F \<Longrightarrow> sup_continuous G \<Longrightarrow> sup_continuous (\<lambda>f. if C then F f else G f)"
    1.33 +  by (auto simp: sup_continuous_def)
    1.34  
    1.35  lemma sup_continuous_compose:
    1.36    assumes f: "sup_continuous f" and g: "sup_continuous g"
    1.37 @@ -74,6 +77,38 @@
    1.38      by (auto simp: sup_continuous_def g[THEN sup_continuousD] f[THEN sup_continuousD])
    1.39  qed
    1.40  
    1.41 +lemma sup_continuous_sup[order_continuous_intros]:
    1.42 +  "sup_continuous f \<Longrightarrow> sup_continuous g \<Longrightarrow> sup_continuous (\<lambda>x. sup (f x) (g x))"
    1.43 +  by (simp add: sup_continuous_def SUP_sup_distrib)
    1.44 +
    1.45 +lemma sup_continuous_inf[order_continuous_intros]:
    1.46 +  fixes P Q :: "'a :: complete_lattice \<Rightarrow> 'b :: complete_distrib_lattice"
    1.47 +  assumes P: "sup_continuous P" and Q: "sup_continuous Q"
    1.48 +  shows "sup_continuous (\<lambda>x. inf (P x) (Q x))"
    1.49 +  unfolding sup_continuous_def
    1.50 +proof (safe intro!: antisym)
    1.51 +  fix M :: "nat \<Rightarrow> 'a" assume M: "incseq M"
    1.52 +  have "inf (P (SUP i. M i)) (Q (SUP i. M i)) \<le> (SUP j i. inf (P (M i)) (Q (M j)))"
    1.53 +    unfolding sup_continuousD[OF P M] sup_continuousD[OF Q M] inf_SUP SUP_inf ..
    1.54 +  also have "\<dots> \<le> (SUP i. inf (P (M i)) (Q (M i)))"
    1.55 +  proof (intro SUP_least)
    1.56 +    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)))"
    1.57 +      by (intro SUP_upper2[of "sup i j"] inf_mono) (auto simp: mono_def)
    1.58 +  qed
    1.59 +  finally show "inf (P (SUP i. M i)) (Q (SUP i. M i)) \<le> (SUP i. inf (P (M i)) (Q (M i)))" .
    1.60 +  
    1.61 +  show "(SUP i. inf (P (M i)) (Q (M i))) \<le> inf (P (SUP i. M i)) (Q (SUP i. M i))"
    1.62 +    unfolding sup_continuousD[OF P M] sup_continuousD[OF Q M] by (intro SUP_least inf_mono SUP_upper)
    1.63 +qed
    1.64 +
    1.65 +lemma sup_continuous_and[order_continuous_intros]:
    1.66 +  "sup_continuous P \<Longrightarrow> sup_continuous Q \<Longrightarrow> sup_continuous (\<lambda>x. P x \<and> Q x)"
    1.67 +  using sup_continuous_inf[of P Q] by simp
    1.68 +
    1.69 +lemma sup_continuous_or[order_continuous_intros]:
    1.70 +  "sup_continuous P \<Longrightarrow> sup_continuous Q \<Longrightarrow> sup_continuous (\<lambda>x. P x \<or> Q x)"
    1.71 +  by (auto simp: sup_continuous_def)
    1.72 +
    1.73  lemma sup_continuous_lfp:
    1.74    assumes "sup_continuous F" shows "lfp F = (SUP i. (F ^^ i) bot)" (is "lfp F = ?U")
    1.75  proof (rule antisym)
    1.76 @@ -122,6 +157,51 @@
    1.77      unfolding sup_continuous_lfp[OF g] by simp
    1.78  qed
    1.79  
    1.80 +lemma lfp_transfer_bounded:
    1.81 +  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)"
    1.82 +  assumes \<alpha>: "\<And>M. mono M \<Longrightarrow> (\<And>i::nat. P (M i)) \<Longrightarrow> \<alpha> (SUP i. M i) = (SUP i. \<alpha> (M i))"
    1.83 +  assumes f: "sup_continuous f" and g: "sup_continuous g"
    1.84 +  assumes [simp]: "\<And>x. P x \<Longrightarrow> \<alpha> (f x) = g (\<alpha> x)"
    1.85 +  assumes g_bound: "\<And>x. \<alpha> bot \<le> g x"
    1.86 +  shows "\<alpha> (lfp f) = lfp g"
    1.87 +proof (rule antisym)
    1.88 +  note mono_g = sup_continuous_mono[OF g]
    1.89 +  have lfp_bound: "\<alpha> bot \<le> lfp g"
    1.90 +    by (subst lfp_unfold[OF mono_g]) (rule g_bound)
    1.91 +
    1.92 +  have P_pow: "P ((f ^^ i) bot)" for i
    1.93 +    by (induction i) (auto intro!: P)
    1.94 +  have incseq_pow: "mono (\<lambda>i. (f ^^ i) bot)"
    1.95 +    unfolding mono_iff_le_Suc
    1.96 +  proof
    1.97 +    fix i show "(f ^^ i) bot \<le> (f ^^ (Suc i)) bot"
    1.98 +    proof (induct i)
    1.99 +      case Suc thus ?case using monoD[OF sup_continuous_mono[OF f] Suc] by auto
   1.100 +    qed (simp add: le_fun_def)
   1.101 +  qed
   1.102 +  have P_lfp: "P (lfp f)"
   1.103 +    using P_pow unfolding sup_continuous_lfp[OF f] by (auto intro!: P)
   1.104 +
   1.105 +  have "\<alpha> (lfp f) = (SUP i. \<alpha> ((f^^i) bot))"
   1.106 +    unfolding sup_continuous_lfp[OF f] using incseq_pow P_pow by (rule \<alpha>)
   1.107 +  also have "\<dots> \<le> lfp g"
   1.108 +  proof (rule SUP_least)
   1.109 +    fix i show "\<alpha> ((f^^i) bot) \<le> lfp g"
   1.110 +    proof (induction i)
   1.111 +      case (Suc n) then show ?case
   1.112 +        by (subst lfp_unfold[OF mono_g]) (simp add: monoD[OF mono_g] P_pow)
   1.113 +    qed (simp add: lfp_bound)
   1.114 +  qed
   1.115 +  finally show "\<alpha> (lfp f) \<le> lfp g" .
   1.116 +
   1.117 +  show "lfp g \<le> \<alpha> (lfp f)"
   1.118 +  proof (induction rule: lfp_ordinal_induct[OF mono_g])
   1.119 +    case (1 S) then show ?case
   1.120 +      by (subst lfp_unfold[OF sup_continuous_mono[OF f]])
   1.121 +         (simp add: monoD[OF mono_g] P_lfp)
   1.122 +  qed (auto intro: Sup_least)
   1.123 +qed
   1.124 +
   1.125  definition
   1.126    inf_continuous :: "('a::complete_lattice \<Rightarrow> 'b::complete_lattice) \<Rightarrow> bool" where
   1.127    "inf_continuous F \<longleftrightarrow> (\<forall>M::nat \<Rightarrow> 'a. antimono M \<longrightarrow> F (INF i. M i) = (INF i. F (M i)))"
   1.128 @@ -141,12 +221,45 @@
   1.129      by (simp add: INF_nat_binary le_iff_inf inf_commute)
   1.130  qed
   1.131  
   1.132 -lemma inf_continuous_intros:
   1.133 +lemma [order_continuous_intros]:
   1.134    shows inf_continuous_const: "inf_continuous (\<lambda>x. c)"
   1.135      and inf_continuous_id: "inf_continuous (\<lambda>x. x)"
   1.136      and inf_continuous_apply: "inf_continuous (\<lambda>f. f x)"
   1.137      and inf_continuous_fun: "(\<And>s. inf_continuous (\<lambda>x. P x s)) \<Longrightarrow> inf_continuous P"
   1.138 - by (auto simp: inf_continuous_def)
   1.139 +    and inf_continuous_If: "inf_continuous F \<Longrightarrow> inf_continuous G \<Longrightarrow> inf_continuous (\<lambda>f. if C then F f else G f)"
   1.140 +  by (auto simp: inf_continuous_def)
   1.141 +
   1.142 +lemma inf_continuous_inf[order_continuous_intros]:
   1.143 +  "inf_continuous f \<Longrightarrow> inf_continuous g \<Longrightarrow> inf_continuous (\<lambda>x. inf (f x) (g x))"
   1.144 +  by (simp add: inf_continuous_def INF_inf_distrib)
   1.145 +
   1.146 +lemma inf_continuous_sup[order_continuous_intros]:
   1.147 +  fixes P Q :: "'a :: complete_lattice \<Rightarrow> 'b :: complete_distrib_lattice"
   1.148 +  assumes P: "inf_continuous P" and Q: "inf_continuous Q"
   1.149 +  shows "inf_continuous (\<lambda>x. sup (P x) (Q x))"
   1.150 +  unfolding inf_continuous_def
   1.151 +proof (safe intro!: antisym)
   1.152 +  fix M :: "nat \<Rightarrow> 'a" assume M: "decseq M"
   1.153 +  show "sup (P (INF i. M i)) (Q (INF i. M i)) \<le> (INF i. sup (P (M i)) (Q (M i)))"
   1.154 +    unfolding inf_continuousD[OF P M] inf_continuousD[OF Q M] by (intro INF_greatest sup_mono INF_lower)
   1.155 +
   1.156 +  have "(INF i. sup (P (M i)) (Q (M i))) \<le> (INF j i. sup (P (M i)) (Q (M j)))"
   1.157 +  proof (intro INF_greatest)
   1.158 +    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)))"
   1.159 +      by (intro INF_lower2[of "sup i j"] sup_mono) (auto simp: mono_def antimono_def)
   1.160 +  qed
   1.161 +  also have "\<dots> \<le> sup (P (INF i. M i)) (Q (INF i. M i))"
   1.162 +    unfolding inf_continuousD[OF P M] inf_continuousD[OF Q M] INF_sup sup_INF ..
   1.163 +  finally show "sup (P (INF i. M i)) (Q (INF i. M i)) \<ge> (INF i. sup (P (M i)) (Q (M i)))" .
   1.164 +qed
   1.165 +
   1.166 +lemma inf_continuous_and[order_continuous_intros]:
   1.167 +  "inf_continuous P \<Longrightarrow> inf_continuous Q \<Longrightarrow> inf_continuous (\<lambda>x. P x \<and> Q x)"
   1.168 +  using inf_continuous_inf[of P Q] by simp
   1.169 +
   1.170 +lemma inf_continuous_or[order_continuous_intros]:
   1.171 +  "inf_continuous P \<Longrightarrow> inf_continuous Q \<Longrightarrow> inf_continuous (\<lambda>x. P x \<or> Q x)"
   1.172 +  using inf_continuous_sup[of P Q] by simp
   1.173  
   1.174  lemma inf_continuous_compose:
   1.175    assumes f: "inf_continuous f" and g: "inf_continuous g"
   1.176 @@ -208,4 +321,70 @@
   1.177      unfolding inf_continuous_gfp[OF g] by simp
   1.178  qed
   1.179  
   1.180 +lemma gfp_transfer_bounded:
   1.181 +  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)"
   1.182 +  assumes \<alpha>: "\<And>M. antimono M \<Longrightarrow> (\<And>i::nat. P (M i)) \<Longrightarrow> \<alpha> (INF i. M i) = (INF i. \<alpha> (M i))"
   1.183 +  assumes f: "inf_continuous f" and g: "inf_continuous g"
   1.184 +  assumes [simp]: "\<And>x. P x \<Longrightarrow> \<alpha> (f x) = g (\<alpha> x)"
   1.185 +  assumes g_bound: "\<And>x. g x \<le> \<alpha> (f top)"
   1.186 +  shows "\<alpha> (gfp f) = gfp g"
   1.187 +proof (rule antisym)
   1.188 +  note mono_g = inf_continuous_mono[OF g]
   1.189 +
   1.190 +  have P_pow: "P ((f ^^ i) (f top))" for i
   1.191 +    by (induction i) (auto intro!: P)
   1.192 +
   1.193 +  have antimono_pow: "antimono (\<lambda>i. (f ^^ i) top)"
   1.194 +    unfolding antimono_iff_le_Suc
   1.195 +  proof
   1.196 +    fix i show "(f ^^ Suc i) top \<le> (f ^^ i) top"
   1.197 +    proof (induct i)
   1.198 +      case Suc thus ?case using monoD[OF inf_continuous_mono[OF f] Suc] by auto
   1.199 +    qed (simp add: le_fun_def)
   1.200 +  qed
   1.201 +  have antimono_pow2: "antimono (\<lambda>i. (f ^^ i) (f top))"
   1.202 +  proof
   1.203 +    show "x \<le> y \<Longrightarrow> (f ^^ y) (f top) \<le> (f ^^ x) (f top)" for x y
   1.204 +      using antimono_pow[THEN antimonoD, of "Suc x" "Suc y"]
   1.205 +      unfolding funpow_Suc_right by simp
   1.206 +  qed
   1.207 +    
   1.208 +  have gfp_f: "gfp f = (INF i. (f ^^ i) (f top))"
   1.209 +    unfolding inf_continuous_gfp[OF f]
   1.210 +  proof (rule INF_eq)
   1.211 +    show "\<exists>j\<in>UNIV. (f ^^ j) (f top) \<le> (f ^^ i) top" for i
   1.212 +      by (intro bexI[of _ "i - 1"]) (auto simp: diff_Suc funpow_Suc_right simp del: funpow.simps(2) split: nat.split)
   1.213 +    show "\<exists>j\<in>UNIV. (f ^^ j) top \<le> (f ^^ i) (f top)" for i
   1.214 +      by (intro bexI[of _ "Suc i"]) (auto simp: funpow_Suc_right simp del: funpow.simps(2))
   1.215 +  qed
   1.216 +
   1.217 +  have P_lfp: "P (gfp f)"
   1.218 +    unfolding gfp_f by (auto intro!: P P_pow antimono_pow2)
   1.219 +
   1.220 +  have "\<alpha> (gfp f) = (INF i. \<alpha> ((f^^i) (f top)))"
   1.221 +    unfolding gfp_f by (rule \<alpha>) (auto intro!: P_pow antimono_pow2)
   1.222 +  also have "\<dots> \<ge> gfp g"
   1.223 +  proof (rule INF_greatest)
   1.224 +    fix i show "gfp g \<le> \<alpha> ((f^^i) (f top))"
   1.225 +    proof (induction i)
   1.226 +      case (Suc n) then show ?case
   1.227 +        by (subst gfp_unfold[OF mono_g]) (simp add: monoD[OF mono_g] P_pow)
   1.228 +    next
   1.229 +      case 0
   1.230 +      have "gfp g \<le> \<alpha> (f top)"
   1.231 +        by (subst gfp_unfold[OF mono_g]) (rule g_bound)
   1.232 +      then show ?case
   1.233 +        by simp
   1.234 +    qed
   1.235 +  qed
   1.236 +  finally show "gfp g \<le> \<alpha> (gfp f)" .
   1.237 +
   1.238 +  show "\<alpha> (gfp f) \<le> gfp g"
   1.239 +  proof (induction rule: gfp_ordinal_induct[OF mono_g])
   1.240 +    case (1 S) then show ?case
   1.241 +      by (subst gfp_unfold[OF inf_continuous_mono[OF f]])
   1.242 +         (simp add: monoD[OF mono_g] P_lfp)
   1.243 +  qed (auto intro: Inf_greatest)
   1.244 +qed
   1.245 +
   1.246  end