src/HOL/Library/Order_Continuity.thy
author wenzelm
Wed Jun 17 11:03:05 2015 +0200 (2015-06-17)
changeset 60500 903bb1495239
parent 60427 b4b672f09270
child 60614 e39e6881985c
permissions -rw-r--r--
isabelle update_cartouches;
     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 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 @{text continuous} is already taken in @{text "Complex_Main"}, so we use
    33   @{text "sup_continuous"} and @{text "inf_continuous"}. These names appear sometimes in literature
    34   and have the advantage that these names are duals.
    35 \<close>
    36 
    37 subsection \<open>Continuity for complete lattices\<close>
    38 
    39 definition
    40   sup_continuous :: "('a::complete_lattice \<Rightarrow> 'a::complete_lattice) \<Rightarrow> bool" where
    41   "sup_continuous F \<longleftrightarrow> (\<forall>M::nat \<Rightarrow> 'a. mono M \<longrightarrow> F (SUP i. M i) = (SUP i. F (M i)))"
    42 
    43 lemma sup_continuousD: "sup_continuous F \<Longrightarrow> mono M \<Longrightarrow> F (SUP i::nat. M i) = (SUP i. F (M i))"
    44   by (auto simp: sup_continuous_def)
    45 
    46 lemma sup_continuous_mono:
    47   fixes F :: "'a::complete_lattice \<Rightarrow> 'a::complete_lattice"
    48   assumes [simp]: "sup_continuous F" shows "mono F"
    49 proof
    50   fix A B :: "'a" assume [simp]: "A \<le> B"
    51   have "F B = F (SUP n::nat. if n = 0 then A else B)"
    52     by (simp add: sup_absorb2 SUP_nat_binary)
    53   also have "\<dots> = (SUP n::nat. if n = 0 then F A else F B)"
    54     by (auto simp: sup_continuousD mono_def intro!: SUP_cong)
    55   finally show "F A \<le> F B"
    56     by (simp add: SUP_nat_binary le_iff_sup)
    57 qed
    58 
    59 lemma sup_continuous_lfp:
    60   assumes "sup_continuous F" shows "lfp F = (SUP i. (F ^^ i) bot)" (is "lfp F = ?U")
    61 proof (rule antisym)
    62   note mono = sup_continuous_mono[OF \<open>sup_continuous F\<close>]
    63   show "?U \<le> lfp F"
    64   proof (rule SUP_least)
    65     fix i show "(F ^^ i) bot \<le> lfp F"
    66     proof (induct i)
    67       case (Suc i)
    68       have "(F ^^ Suc i) bot = F ((F ^^ i) bot)" by simp
    69       also have "\<dots> \<le> F (lfp F)" by (rule monoD[OF mono Suc])
    70       also have "\<dots> = lfp F" by (simp add: lfp_unfold[OF mono, symmetric])
    71       finally show ?case .
    72     qed simp
    73   qed
    74   show "lfp F \<le> ?U"
    75   proof (rule lfp_lowerbound)
    76     have "mono (\<lambda>i::nat. (F ^^ i) bot)"
    77     proof -
    78       { fix i::nat have "(F ^^ i) bot \<le> (F ^^ (Suc i)) bot"
    79         proof (induct i)
    80           case 0 show ?case by simp
    81         next
    82           case Suc thus ?case using monoD[OF mono Suc] by auto
    83         qed }
    84       thus ?thesis by (auto simp add: mono_iff_le_Suc)
    85     qed
    86     hence "F ?U = (SUP i. (F ^^ Suc i) bot)"
    87       using \<open>sup_continuous F\<close> by (simp add: sup_continuous_def)
    88     also have "\<dots> \<le> ?U"
    89       by (fast intro: SUP_least SUP_upper)
    90     finally show "F ?U \<le> ?U" .
    91   qed
    92 qed
    93 
    94 lemma lfp_transfer:
    95   assumes \<alpha>: "sup_continuous \<alpha>" and f: "sup_continuous f" and g: "sup_continuous g"
    96   assumes [simp]: "\<alpha> bot = bot" "\<And>x. \<alpha> (f x) = g (\<alpha> x)"
    97   shows "\<alpha> (lfp f) = lfp g"
    98 proof -
    99   have "\<alpha> (lfp f) = (SUP i. \<alpha> ((f^^i) bot))"
   100     unfolding sup_continuous_lfp[OF f] by (intro f \<alpha> sup_continuousD mono_funpow sup_continuous_mono)
   101   moreover have "\<alpha> ((f^^i) bot) = (g^^i) bot" for i
   102     by (induction i; simp)
   103   ultimately show ?thesis
   104     unfolding sup_continuous_lfp[OF g] by simp
   105 qed
   106 
   107 definition
   108   inf_continuous :: "('a::complete_lattice \<Rightarrow> 'a::complete_lattice) \<Rightarrow> bool" where
   109   "inf_continuous F \<longleftrightarrow> (\<forall>M::nat \<Rightarrow> 'a. antimono M \<longrightarrow> F (INF i. M i) = (INF i. F (M i)))"
   110 
   111 lemma inf_continuousD: "inf_continuous F \<Longrightarrow> antimono M \<Longrightarrow> F (INF i::nat. M i) = (INF i. F (M i))"
   112   by (auto simp: inf_continuous_def)
   113 
   114 lemma inf_continuous_mono:
   115   fixes F :: "'a::complete_lattice \<Rightarrow> 'a::complete_lattice"
   116   assumes [simp]: "inf_continuous F" shows "mono F"
   117 proof
   118   fix A B :: "'a" assume [simp]: "A \<le> B"
   119   have "F A = F (INF n::nat. if n = 0 then B else A)"
   120     by (simp add: inf_absorb2 INF_nat_binary)
   121   also have "\<dots> = (INF n::nat. if n = 0 then F B else F A)"
   122     by (auto simp: inf_continuousD antimono_def intro!: INF_cong)
   123   finally show "F A \<le> F B"
   124     by (simp add: INF_nat_binary le_iff_inf inf_commute)
   125 qed
   126 
   127 lemma inf_continuous_gfp:
   128   assumes "inf_continuous F" shows "gfp F = (INF i. (F ^^ i) top)" (is "gfp F = ?U")
   129 proof (rule antisym)
   130   note mono = inf_continuous_mono[OF \<open>inf_continuous F\<close>]
   131   show "gfp F \<le> ?U"
   132   proof (rule INF_greatest)
   133     fix i show "gfp F \<le> (F ^^ i) top"
   134     proof (induct i)
   135       case (Suc i)
   136       have "gfp F = F (gfp F)" by (simp add: gfp_unfold[OF mono, symmetric])
   137       also have "\<dots> \<le> F ((F ^^ i) top)" by (rule monoD[OF mono Suc])
   138       also have "\<dots> = (F ^^ Suc i) top" by simp
   139       finally show ?case .
   140     qed simp
   141   qed
   142   show "?U \<le> gfp F"
   143   proof (rule gfp_upperbound)
   144     have *: "antimono (\<lambda>i::nat. (F ^^ i) top)"
   145     proof -
   146       { fix i::nat have "(F ^^ Suc i) top \<le> (F ^^ i) top"
   147         proof (induct i)
   148           case 0 show ?case by simp
   149         next
   150           case Suc thus ?case using monoD[OF mono Suc] by auto
   151         qed }
   152       thus ?thesis by (auto simp add: antimono_iff_le_Suc)
   153     qed
   154     have "?U \<le> (INF i. (F ^^ Suc i) top)"
   155       by (fast intro: INF_greatest INF_lower)
   156     also have "\<dots> \<le> F ?U"
   157       by (simp add: inf_continuousD \<open>inf_continuous F\<close> *)
   158     finally show "?U \<le> F ?U" .
   159   qed
   160 qed
   161 
   162 lemma gfp_transfer:
   163   assumes \<alpha>: "inf_continuous \<alpha>" and f: "inf_continuous f" and g: "inf_continuous g"
   164   assumes [simp]: "\<alpha> top = top" "\<And>x. \<alpha> (f x) = g (\<alpha> x)"
   165   shows "\<alpha> (gfp f) = gfp g"
   166 proof -
   167   have "\<alpha> (gfp f) = (INF i. \<alpha> ((f^^i) top))"
   168     unfolding inf_continuous_gfp[OF f] by (intro f \<alpha> inf_continuousD antimono_funpow inf_continuous_mono)
   169   moreover have "\<alpha> ((f^^i) top) = (g^^i) top" for i
   170     by (induction i; simp)
   171   ultimately show ?thesis
   172     unfolding inf_continuous_gfp[OF g] by simp
   173 qed
   174 
   175 end