src/HOL/Library/Order_Continuity.thy
author wenzelm
Mon Dec 28 17:43:30 2015 +0100 (2015-12-28)
changeset 61952 546958347e05
parent 61585 a9599d3d7610
child 62373 ea7a442e9a56
permissions -rw-r--r--
prefer symbols for "Union", "Inter";
     1 (*  Title:      HOL/Library/Order_Continuity.thy
     2     Author:     David von Oheimb, TU Muenchen
     3 *)
     4 
     5 section \<open>Continuity and iterations (of set transformers)\<close>
     6 
     7 theory Order_Continuity
     8 imports Complex_Main
     9 begin
    10 
    11 (* TODO: Generalize theory to chain-complete partial orders *)
    12 
    13 lemma SUP_nat_binary:
    14   "(SUP n::nat. if n = 0 then A else B) = (sup A B::'a::complete_lattice)"
    15   apply (auto intro!: antisym SUP_least)
    16   apply (rule SUP_upper2[where i=0])
    17   apply simp_all
    18   apply (rule SUP_upper2[where i=1])
    19   apply simp_all
    20   done
    21 
    22 lemma INF_nat_binary:
    23   "(INF n::nat. if n = 0 then A else B) = (inf A B::'a::complete_lattice)"
    24   apply (auto intro!: antisym INF_greatest)
    25   apply (rule INF_lower2[where i=0])
    26   apply simp_all
    27   apply (rule INF_lower2[where i=1])
    28   apply simp_all
    29   done
    30 
    31 text \<open>
    32   The name \<open>continuous\<close> is already taken in \<open>Complex_Main\<close>, so we use
    33   \<open>sup_continuous\<close> and \<open>inf_continuous\<close>. These names appear sometimes in literature
    34   and have the advantage that these names are duals.
    35 \<close>
    36 
    37 named_theorems order_continuous_intros
    38 
    39 subsection \<open>Continuity for complete lattices\<close>
    40 
    41 definition
    42   sup_continuous :: "('a::complete_lattice \<Rightarrow> 'b::complete_lattice) \<Rightarrow> bool" where
    43   "sup_continuous F \<longleftrightarrow> (\<forall>M::nat \<Rightarrow> 'a. mono M \<longrightarrow> F (SUP i. M i) = (SUP i. F (M i)))"
    44 
    45 lemma sup_continuousD: "sup_continuous F \<Longrightarrow> mono M \<Longrightarrow> F (SUP i::nat. M i) = (SUP i. F (M i))"
    46   by (auto simp: sup_continuous_def)
    47 
    48 lemma sup_continuous_mono:
    49   assumes [simp]: "sup_continuous F" shows "mono F"
    50 proof
    51   fix A B :: "'a" assume [simp]: "A \<le> B"
    52   have "F B = F (SUP n::nat. if n = 0 then A else B)"
    53     by (simp add: sup_absorb2 SUP_nat_binary)
    54   also have "\<dots> = (SUP n::nat. if n = 0 then F A else F B)"
    55     by (auto simp: sup_continuousD mono_def intro!: SUP_cong)
    56   finally show "F A \<le> F B"
    57     by (simp add: SUP_nat_binary le_iff_sup)
    58 qed
    59 
    60 lemma [order_continuous_intros]:
    61   shows sup_continuous_const: "sup_continuous (\<lambda>x. c)"
    62     and sup_continuous_id: "sup_continuous (\<lambda>x. x)"
    63     and sup_continuous_apply: "sup_continuous (\<lambda>f. f x)"
    64     and sup_continuous_fun: "(\<And>s. sup_continuous (\<lambda>x. P x s)) \<Longrightarrow> sup_continuous P"
    65     and sup_continuous_If: "sup_continuous F \<Longrightarrow> sup_continuous G \<Longrightarrow> sup_continuous (\<lambda>f. if C then F f else G f)"
    66   by (auto simp: sup_continuous_def)
    67 
    68 lemma sup_continuous_compose:
    69   assumes f: "sup_continuous f" and g: "sup_continuous g"
    70   shows "sup_continuous (\<lambda>x. f (g x))"
    71   unfolding sup_continuous_def
    72 proof safe
    73   fix M :: "nat \<Rightarrow> 'c" assume "mono M"
    74   moreover then have "mono (\<lambda>i. g (M i))"
    75     using sup_continuous_mono[OF g] by (auto simp: mono_def)
    76   ultimately show "f (g (SUPREMUM UNIV M)) = (SUP i. f (g (M i)))"
    77     by (auto simp: sup_continuous_def g[THEN sup_continuousD] f[THEN sup_continuousD])
    78 qed
    79 
    80 lemma sup_continuous_sup[order_continuous_intros]:
    81   "sup_continuous f \<Longrightarrow> sup_continuous g \<Longrightarrow> sup_continuous (\<lambda>x. sup (f x) (g x))"
    82   by (simp add: sup_continuous_def SUP_sup_distrib)
    83 
    84 lemma sup_continuous_inf[order_continuous_intros]:
    85   fixes P Q :: "'a :: complete_lattice \<Rightarrow> 'b :: complete_distrib_lattice"
    86   assumes P: "sup_continuous P" and Q: "sup_continuous Q"
    87   shows "sup_continuous (\<lambda>x. inf (P x) (Q x))"
    88   unfolding sup_continuous_def
    89 proof (safe intro!: antisym)
    90   fix M :: "nat \<Rightarrow> 'a" assume M: "incseq M"
    91   have "inf (P (SUP i. M i)) (Q (SUP i. M i)) \<le> (SUP j i. inf (P (M i)) (Q (M j)))"
    92     unfolding sup_continuousD[OF P M] sup_continuousD[OF Q M] inf_SUP SUP_inf ..
    93   also have "\<dots> \<le> (SUP i. inf (P (M i)) (Q (M i)))"
    94   proof (intro SUP_least)
    95     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)))"
    96       by (intro SUP_upper2[of "sup i j"] inf_mono) (auto simp: mono_def)
    97   qed
    98   finally show "inf (P (SUP i. M i)) (Q (SUP i. M i)) \<le> (SUP i. inf (P (M i)) (Q (M i)))" .
    99   
   100   show "(SUP i. inf (P (M i)) (Q (M i))) \<le> inf (P (SUP i. M i)) (Q (SUP i. M i))"
   101     unfolding sup_continuousD[OF P M] sup_continuousD[OF Q M] by (intro SUP_least inf_mono SUP_upper)
   102 qed
   103 
   104 lemma sup_continuous_and[order_continuous_intros]:
   105   "sup_continuous P \<Longrightarrow> sup_continuous Q \<Longrightarrow> sup_continuous (\<lambda>x. P x \<and> Q x)"
   106   using sup_continuous_inf[of P Q] by simp
   107 
   108 lemma sup_continuous_or[order_continuous_intros]:
   109   "sup_continuous P \<Longrightarrow> sup_continuous Q \<Longrightarrow> sup_continuous (\<lambda>x. P x \<or> Q x)"
   110   by (auto simp: sup_continuous_def)
   111 
   112 lemma sup_continuous_lfp:
   113   assumes "sup_continuous F" shows "lfp F = (SUP i. (F ^^ i) bot)" (is "lfp F = ?U")
   114 proof (rule antisym)
   115   note mono = sup_continuous_mono[OF \<open>sup_continuous F\<close>]
   116   show "?U \<le> lfp F"
   117   proof (rule SUP_least)
   118     fix i show "(F ^^ i) bot \<le> lfp F"
   119     proof (induct i)
   120       case (Suc i)
   121       have "(F ^^ Suc i) bot = F ((F ^^ i) bot)" by simp
   122       also have "\<dots> \<le> F (lfp F)" by (rule monoD[OF mono Suc])
   123       also have "\<dots> = lfp F" by (simp add: lfp_unfold[OF mono, symmetric])
   124       finally show ?case .
   125     qed simp
   126   qed
   127   show "lfp F \<le> ?U"
   128   proof (rule lfp_lowerbound)
   129     have "mono (\<lambda>i::nat. (F ^^ i) bot)"
   130     proof -
   131       { fix i::nat have "(F ^^ i) bot \<le> (F ^^ (Suc i)) bot"
   132         proof (induct i)
   133           case 0 show ?case by simp
   134         next
   135           case Suc thus ?case using monoD[OF mono Suc] by auto
   136         qed }
   137       thus ?thesis by (auto simp add: mono_iff_le_Suc)
   138     qed
   139     hence "F ?U = (SUP i. (F ^^ Suc i) bot)"
   140       using \<open>sup_continuous F\<close> by (simp add: sup_continuous_def)
   141     also have "\<dots> \<le> ?U"
   142       by (fast intro: SUP_least SUP_upper)
   143     finally show "F ?U \<le> ?U" .
   144   qed
   145 qed
   146 
   147 lemma lfp_transfer_bounded:
   148   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)"
   149   assumes \<alpha>: "\<And>M. mono M \<Longrightarrow> (\<And>i::nat. P (M i)) \<Longrightarrow> \<alpha> (SUP i. M i) = (SUP i. \<alpha> (M i))"
   150   assumes f: "sup_continuous f" and g: "sup_continuous g"
   151   assumes [simp]: "\<And>x. P x \<Longrightarrow> x \<le> lfp f \<Longrightarrow> \<alpha> (f x) = g (\<alpha> x)"
   152   assumes g_bound: "\<And>x. \<alpha> bot \<le> g x"
   153   shows "\<alpha> (lfp f) = lfp g"
   154 proof (rule antisym)
   155   note mono_g = sup_continuous_mono[OF g]
   156   note mono_f = sup_continuous_mono[OF f]
   157   have lfp_bound: "\<alpha> bot \<le> lfp g"
   158     by (subst lfp_unfold[OF mono_g]) (rule g_bound)
   159 
   160   have P_pow: "P ((f ^^ i) bot)" for i
   161     by (induction i) (auto intro!: P)
   162   have incseq_pow: "mono (\<lambda>i. (f ^^ i) bot)"
   163     unfolding mono_iff_le_Suc
   164   proof
   165     fix i show "(f ^^ i) bot \<le> (f ^^ (Suc i)) bot"
   166     proof (induct i)
   167       case Suc thus ?case using monoD[OF sup_continuous_mono[OF f] Suc] by auto
   168     qed (simp add: le_fun_def)
   169   qed
   170   have P_lfp: "P (lfp f)"
   171     using P_pow unfolding sup_continuous_lfp[OF f] by (auto intro!: P)
   172 
   173   have iter_le_lfp: "(f ^^ n) bot \<le> lfp f" for n
   174     apply (induction n)
   175     apply simp
   176     apply (subst lfp_unfold[OF mono_f])
   177     apply (auto intro!: monoD[OF mono_f])
   178     done
   179 
   180   have "\<alpha> (lfp f) = (SUP i. \<alpha> ((f^^i) bot))"
   181     unfolding sup_continuous_lfp[OF f] using incseq_pow P_pow by (rule \<alpha>)
   182   also have "\<dots> \<le> lfp g"
   183   proof (rule SUP_least)
   184     fix i show "\<alpha> ((f^^i) bot) \<le> lfp g"
   185     proof (induction i)
   186       case (Suc n) then show ?case
   187         by (subst lfp_unfold[OF mono_g]) (simp add: monoD[OF mono_g] P_pow iter_le_lfp)
   188     qed (simp add: lfp_bound)
   189   qed
   190   finally show "\<alpha> (lfp f) \<le> lfp g" .
   191 
   192   show "lfp g \<le> \<alpha> (lfp f)"
   193   proof (induction rule: lfp_ordinal_induct[OF mono_g])
   194     case (1 S) then show ?case
   195       by (subst lfp_unfold[OF sup_continuous_mono[OF f]])
   196          (simp add: monoD[OF mono_g] P_lfp)
   197   qed (auto intro: Sup_least)
   198 qed
   199 
   200 lemma lfp_transfer:
   201   "sup_continuous \<alpha> \<Longrightarrow> sup_continuous f \<Longrightarrow> sup_continuous g \<Longrightarrow>
   202     (\<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"
   203   by (rule lfp_transfer_bounded[where P=top]) (auto dest: sup_continuousD)
   204 
   205 definition
   206   inf_continuous :: "('a::complete_lattice \<Rightarrow> 'b::complete_lattice) \<Rightarrow> bool" where
   207   "inf_continuous F \<longleftrightarrow> (\<forall>M::nat \<Rightarrow> 'a. antimono M \<longrightarrow> F (INF i. M i) = (INF i. F (M i)))"
   208 
   209 lemma inf_continuousD: "inf_continuous F \<Longrightarrow> antimono M \<Longrightarrow> F (INF i::nat. M i) = (INF i. F (M i))"
   210   by (auto simp: inf_continuous_def)
   211 
   212 lemma inf_continuous_mono:
   213   assumes [simp]: "inf_continuous F" shows "mono F"
   214 proof
   215   fix A B :: "'a" assume [simp]: "A \<le> B"
   216   have "F A = F (INF n::nat. if n = 0 then B else A)"
   217     by (simp add: inf_absorb2 INF_nat_binary)
   218   also have "\<dots> = (INF n::nat. if n = 0 then F B else F A)"
   219     by (auto simp: inf_continuousD antimono_def intro!: INF_cong)
   220   finally show "F A \<le> F B"
   221     by (simp add: INF_nat_binary le_iff_inf inf_commute)
   222 qed
   223 
   224 lemma [order_continuous_intros]:
   225   shows inf_continuous_const: "inf_continuous (\<lambda>x. c)"
   226     and inf_continuous_id: "inf_continuous (\<lambda>x. x)"
   227     and inf_continuous_apply: "inf_continuous (\<lambda>f. f x)"
   228     and inf_continuous_fun: "(\<And>s. inf_continuous (\<lambda>x. P x s)) \<Longrightarrow> inf_continuous P"
   229     and inf_continuous_If: "inf_continuous F \<Longrightarrow> inf_continuous G \<Longrightarrow> inf_continuous (\<lambda>f. if C then F f else G f)"
   230   by (auto simp: inf_continuous_def)
   231 
   232 lemma inf_continuous_inf[order_continuous_intros]:
   233   "inf_continuous f \<Longrightarrow> inf_continuous g \<Longrightarrow> inf_continuous (\<lambda>x. inf (f x) (g x))"
   234   by (simp add: inf_continuous_def INF_inf_distrib)
   235 
   236 lemma inf_continuous_sup[order_continuous_intros]:
   237   fixes P Q :: "'a :: complete_lattice \<Rightarrow> 'b :: complete_distrib_lattice"
   238   assumes P: "inf_continuous P" and Q: "inf_continuous Q"
   239   shows "inf_continuous (\<lambda>x. sup (P x) (Q x))"
   240   unfolding inf_continuous_def
   241 proof (safe intro!: antisym)
   242   fix M :: "nat \<Rightarrow> 'a" assume M: "decseq M"
   243   show "sup (P (INF i. M i)) (Q (INF i. M i)) \<le> (INF i. sup (P (M i)) (Q (M i)))"
   244     unfolding inf_continuousD[OF P M] inf_continuousD[OF Q M] by (intro INF_greatest sup_mono INF_lower)
   245 
   246   have "(INF i. sup (P (M i)) (Q (M i))) \<le> (INF j i. sup (P (M i)) (Q (M j)))"
   247   proof (intro INF_greatest)
   248     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)))"
   249       by (intro INF_lower2[of "sup i j"] sup_mono) (auto simp: mono_def antimono_def)
   250   qed
   251   also have "\<dots> \<le> sup (P (INF i. M i)) (Q (INF i. M i))"
   252     unfolding inf_continuousD[OF P M] inf_continuousD[OF Q M] INF_sup sup_INF ..
   253   finally show "sup (P (INF i. M i)) (Q (INF i. M i)) \<ge> (INF i. sup (P (M i)) (Q (M i)))" .
   254 qed
   255 
   256 lemma inf_continuous_and[order_continuous_intros]:
   257   "inf_continuous P \<Longrightarrow> inf_continuous Q \<Longrightarrow> inf_continuous (\<lambda>x. P x \<and> Q x)"
   258   using inf_continuous_inf[of P Q] by simp
   259 
   260 lemma inf_continuous_or[order_continuous_intros]:
   261   "inf_continuous P \<Longrightarrow> inf_continuous Q \<Longrightarrow> inf_continuous (\<lambda>x. P x \<or> Q x)"
   262   using inf_continuous_sup[of P Q] by simp
   263 
   264 lemma inf_continuous_compose:
   265   assumes f: "inf_continuous f" and g: "inf_continuous g"
   266   shows "inf_continuous (\<lambda>x. f (g x))"
   267   unfolding inf_continuous_def
   268 proof safe
   269   fix M :: "nat \<Rightarrow> 'c" assume "antimono M"
   270   moreover then have "antimono (\<lambda>i. g (M i))"
   271     using inf_continuous_mono[OF g] by (auto simp: mono_def antimono_def)
   272   ultimately show "f (g (INFIMUM UNIV M)) = (INF i. f (g (M i)))"
   273     by (auto simp: inf_continuous_def g[THEN inf_continuousD] f[THEN inf_continuousD])
   274 qed
   275 
   276 lemma inf_continuous_gfp:
   277   assumes "inf_continuous F" shows "gfp F = (INF i. (F ^^ i) top)" (is "gfp F = ?U")
   278 proof (rule antisym)
   279   note mono = inf_continuous_mono[OF \<open>inf_continuous F\<close>]
   280   show "gfp F \<le> ?U"
   281   proof (rule INF_greatest)
   282     fix i show "gfp F \<le> (F ^^ i) top"
   283     proof (induct i)
   284       case (Suc i)
   285       have "gfp F = F (gfp F)" by (simp add: gfp_unfold[OF mono, symmetric])
   286       also have "\<dots> \<le> F ((F ^^ i) top)" by (rule monoD[OF mono Suc])
   287       also have "\<dots> = (F ^^ Suc i) top" by simp
   288       finally show ?case .
   289     qed simp
   290   qed
   291   show "?U \<le> gfp F"
   292   proof (rule gfp_upperbound)
   293     have *: "antimono (\<lambda>i::nat. (F ^^ i) top)"
   294     proof -
   295       { fix i::nat have "(F ^^ Suc i) top \<le> (F ^^ i) top"
   296         proof (induct i)
   297           case 0 show ?case by simp
   298         next
   299           case Suc thus ?case using monoD[OF mono Suc] by auto
   300         qed }
   301       thus ?thesis by (auto simp add: antimono_iff_le_Suc)
   302     qed
   303     have "?U \<le> (INF i. (F ^^ Suc i) top)"
   304       by (fast intro: INF_greatest INF_lower)
   305     also have "\<dots> \<le> F ?U"
   306       by (simp add: inf_continuousD \<open>inf_continuous F\<close> *)
   307     finally show "?U \<le> F ?U" .
   308   qed
   309 qed
   310 
   311 lemma gfp_transfer:
   312   assumes \<alpha>: "inf_continuous \<alpha>" and f: "inf_continuous f" and g: "inf_continuous g"
   313   assumes [simp]: "\<alpha> top = top" "\<And>x. \<alpha> (f x) = g (\<alpha> x)"
   314   shows "\<alpha> (gfp f) = gfp g"
   315 proof -
   316   have "\<alpha> (gfp f) = (INF i. \<alpha> ((f^^i) top))"
   317     unfolding inf_continuous_gfp[OF f] by (intro f \<alpha> inf_continuousD antimono_funpow inf_continuous_mono)
   318   moreover have "\<alpha> ((f^^i) top) = (g^^i) top" for i
   319     by (induction i; simp)
   320   ultimately show ?thesis
   321     unfolding inf_continuous_gfp[OF g] by simp
   322 qed
   323 
   324 lemma gfp_transfer_bounded:
   325   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)"
   326   assumes \<alpha>: "\<And>M. antimono M \<Longrightarrow> (\<And>i::nat. P (M i)) \<Longrightarrow> \<alpha> (INF i. M i) = (INF i. \<alpha> (M i))"
   327   assumes f: "inf_continuous f" and g: "inf_continuous g"
   328   assumes [simp]: "\<And>x. P x \<Longrightarrow> \<alpha> (f x) = g (\<alpha> x)"
   329   assumes g_bound: "\<And>x. g x \<le> \<alpha> (f top)"
   330   shows "\<alpha> (gfp f) = gfp g"
   331 proof (rule antisym)
   332   note mono_g = inf_continuous_mono[OF g]
   333 
   334   have P_pow: "P ((f ^^ i) (f top))" for i
   335     by (induction i) (auto intro!: P)
   336 
   337   have antimono_pow: "antimono (\<lambda>i. (f ^^ i) top)"
   338     unfolding antimono_iff_le_Suc
   339   proof
   340     fix i show "(f ^^ Suc i) top \<le> (f ^^ i) top"
   341     proof (induct i)
   342       case Suc thus ?case using monoD[OF inf_continuous_mono[OF f] Suc] by auto
   343     qed (simp add: le_fun_def)
   344   qed
   345   have antimono_pow2: "antimono (\<lambda>i. (f ^^ i) (f top))"
   346   proof
   347     show "x \<le> y \<Longrightarrow> (f ^^ y) (f top) \<le> (f ^^ x) (f top)" for x y
   348       using antimono_pow[THEN antimonoD, of "Suc x" "Suc y"]
   349       unfolding funpow_Suc_right by simp
   350   qed
   351     
   352   have gfp_f: "gfp f = (INF i. (f ^^ i) (f top))"
   353     unfolding inf_continuous_gfp[OF f]
   354   proof (rule INF_eq)
   355     show "\<exists>j\<in>UNIV. (f ^^ j) (f top) \<le> (f ^^ i) top" for i
   356       by (intro bexI[of _ "i - 1"]) (auto simp: diff_Suc funpow_Suc_right simp del: funpow.simps(2) split: nat.split)
   357     show "\<exists>j\<in>UNIV. (f ^^ j) top \<le> (f ^^ i) (f top)" for i
   358       by (intro bexI[of _ "Suc i"]) (auto simp: funpow_Suc_right simp del: funpow.simps(2))
   359   qed
   360 
   361   have P_lfp: "P (gfp f)"
   362     unfolding gfp_f by (auto intro!: P P_pow antimono_pow2)
   363 
   364   have "\<alpha> (gfp f) = (INF i. \<alpha> ((f^^i) (f top)))"
   365     unfolding gfp_f by (rule \<alpha>) (auto intro!: P_pow antimono_pow2)
   366   also have "\<dots> \<ge> gfp g"
   367   proof (rule INF_greatest)
   368     fix i show "gfp g \<le> \<alpha> ((f^^i) (f top))"
   369     proof (induction i)
   370       case (Suc n) then show ?case
   371         by (subst gfp_unfold[OF mono_g]) (simp add: monoD[OF mono_g] P_pow)
   372     next
   373       case 0
   374       have "gfp g \<le> \<alpha> (f top)"
   375         by (subst gfp_unfold[OF mono_g]) (rule g_bound)
   376       then show ?case
   377         by simp
   378     qed
   379   qed
   380   finally show "gfp g \<le> \<alpha> (gfp f)" .
   381 
   382   show "\<alpha> (gfp f) \<le> gfp g"
   383   proof (induction rule: gfp_ordinal_induct[OF mono_g])
   384     case (1 S) then show ?case
   385       by (subst gfp_unfold[OF inf_continuous_mono[OF f]])
   386          (simp add: monoD[OF mono_g] P_lfp)
   387   qed (auto intro: Inf_greatest)
   388 qed
   389 
   390 end