src/HOL/Library/Order_Continuity.thy
 author hoelzl Mon May 04 17:35:31 2015 +0200 (2015-05-04) changeset 60172 423273355b55 parent 58881 b9556a055632 child 60427 b4b672f09270 permissions -rw-r--r--
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
```     1 (*  Title:      HOL/Library/Order_Continuity.thy
```
```     2     Author:     David von Oheimb, TU Muenchen
```
```     3 *)
```
```     4
```
```     5 section {* Continuity and iterations (of set transformers) *}
```
```     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 {* Continuity for complete lattices *}
```
```    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 `sup_continuous F`]
```
```    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 `sup_continuous F` 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 definition
```
```    95   inf_continuous :: "('a::complete_lattice \<Rightarrow> 'a::complete_lattice) \<Rightarrow> bool" where
```
```    96   "inf_continuous F \<longleftrightarrow> (\<forall>M::nat \<Rightarrow> 'a. antimono M \<longrightarrow> F (INF i. M i) = (INF i. F (M i)))"
```
```    97
```
```    98 lemma inf_continuousD: "inf_continuous F \<Longrightarrow> antimono M \<Longrightarrow> F (INF i::nat. M i) = (INF i. F (M i))"
```
```    99   by (auto simp: inf_continuous_def)
```
```   100
```
```   101 lemma inf_continuous_mono:
```
```   102   fixes F :: "'a::complete_lattice \<Rightarrow> 'a::complete_lattice"
```
```   103   assumes [simp]: "inf_continuous F" shows "mono F"
```
```   104 proof
```
```   105   fix A B :: "'a" assume [simp]: "A \<le> B"
```
```   106   have "F A = F (INF n::nat. if n = 0 then B else A)"
```
```   107     by (simp add: inf_absorb2 INF_nat_binary)
```
```   108   also have "\<dots> = (INF n::nat. if n = 0 then F B else F A)"
```
```   109     by (auto simp: inf_continuousD antimono_def intro!: INF_cong)
```
```   110   finally show "F A \<le> F B"
```
```   111     by (simp add: INF_nat_binary le_iff_inf inf_commute)
```
```   112 qed
```
```   113
```
```   114 lemma inf_continuous_gfp:
```
```   115   assumes "inf_continuous F" shows "gfp F = (INF i. (F ^^ i) top)" (is "gfp F = ?U")
```
```   116 proof (rule antisym)
```
```   117   note mono = inf_continuous_mono[OF `inf_continuous F`]
```
```   118   show "gfp F \<le> ?U"
```
```   119   proof (rule INF_greatest)
```
```   120     fix i show "gfp F \<le> (F ^^ i) top"
```
```   121     proof (induct i)
```
```   122       case (Suc i)
```
```   123       have "gfp F = F (gfp F)" by (simp add: gfp_unfold[OF mono, symmetric])
```
```   124       also have "\<dots> \<le> F ((F ^^ i) top)" by (rule monoD[OF mono Suc])
```
```   125       also have "\<dots> = (F ^^ Suc i) top" by simp
```
```   126       finally show ?case .
```
```   127     qed simp
```
```   128   qed
```
```   129   show "?U \<le> gfp F"
```
```   130   proof (rule gfp_upperbound)
```
```   131     have *: "antimono (\<lambda>i::nat. (F ^^ i) top)"
```
```   132     proof -
```
```   133       { fix i::nat have "(F ^^ Suc i) top \<le> (F ^^ i) top"
```
```   134         proof (induct i)
```
```   135           case 0 show ?case by simp
```
```   136         next
```
```   137           case Suc thus ?case using monoD[OF mono Suc] by auto
```
```   138         qed }
```
```   139       thus ?thesis by (auto simp add: antimono_iff_le_Suc)
```
```   140     qed
```
```   141     have "?U \<le> (INF i. (F ^^ Suc i) top)"
```
```   142       by (fast intro: INF_greatest INF_lower)
```
```   143     also have "\<dots> \<le> F ?U"
```
```   144       by (simp add: inf_continuousD `inf_continuous F` *)
```
```   145     finally show "?U \<le> F ?U" .
```
```   146   qed
```
```   147 qed
```
```   148
```
```   149 end
```