1(* Title: HOL/HOLCF/Cont.thy 2 Author: Franz Regensburger 3 Author: Brian Huffman 4*) 5 6section \<open>Continuity and monotonicity\<close> 7 8theory Cont 9 imports Pcpo 10begin 11 12text \<open> 13 Now we change the default class! Form now on all untyped type variables are 14 of default class po 15\<close> 16 17default_sort po 18 19subsection \<open>Definitions\<close> 20 21definition monofun :: "('a \<Rightarrow> 'b) \<Rightarrow> bool" \<comment> \<open>monotonicity\<close> 22 where "monofun f \<longleftrightarrow> (\<forall>x y. x \<sqsubseteq> y \<longrightarrow> f x \<sqsubseteq> f y)" 23 24definition cont :: "('a::cpo \<Rightarrow> 'b::cpo) \<Rightarrow> bool" 25 where "cont f = (\<forall>Y. chain Y \<longrightarrow> range (\<lambda>i. f (Y i)) <<| f (\<Squnion>i. Y i))" 26 27lemma contI: "(\<And>Y. chain Y \<Longrightarrow> range (\<lambda>i. f (Y i)) <<| f (\<Squnion>i. Y i)) \<Longrightarrow> cont f" 28 by (simp add: cont_def) 29 30lemma contE: "cont f \<Longrightarrow> chain Y \<Longrightarrow> range (\<lambda>i. f (Y i)) <<| f (\<Squnion>i. Y i)" 31 by (simp add: cont_def) 32 33lemma monofunI: "(\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y) \<Longrightarrow> monofun f" 34 by (simp add: monofun_def) 35 36lemma monofunE: "monofun f \<Longrightarrow> x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y" 37 by (simp add: monofun_def) 38 39 40subsection \<open>Equivalence of alternate definition\<close> 41 42text \<open>monotone functions map chains to chains\<close> 43 44lemma ch2ch_monofun: "monofun f \<Longrightarrow> chain Y \<Longrightarrow> chain (\<lambda>i. f (Y i))" 45 apply (rule chainI) 46 apply (erule monofunE) 47 apply (erule chainE) 48 done 49 50text \<open>monotone functions map upper bound to upper bounds\<close> 51 52lemma ub2ub_monofun: "monofun f \<Longrightarrow> range Y <| u \<Longrightarrow> range (\<lambda>i. f (Y i)) <| f u" 53 apply (rule ub_rangeI) 54 apply (erule monofunE) 55 apply (erule ub_rangeD) 56 done 57 58text \<open>a lemma about binary chains\<close> 59 60lemma binchain_cont: "cont f \<Longrightarrow> x \<sqsubseteq> y \<Longrightarrow> range (\<lambda>i::nat. f (if i = 0 then x else y)) <<| f y" 61 apply (subgoal_tac "f (\<Squnion>i::nat. if i = 0 then x else y) = f y") 62 apply (erule subst) 63 apply (erule contE) 64 apply (erule bin_chain) 65 apply (rule_tac f=f in arg_cong) 66 apply (erule is_lub_bin_chain [THEN lub_eqI]) 67 done 68 69text \<open>continuity implies monotonicity\<close> 70 71lemma cont2mono: "cont f \<Longrightarrow> monofun f" 72 apply (rule monofunI) 73 apply (drule (1) binchain_cont) 74 apply (drule_tac i=0 in is_lub_rangeD1) 75 apply simp 76 done 77 78lemmas cont2monofunE = cont2mono [THEN monofunE] 79 80lemmas ch2ch_cont = cont2mono [THEN ch2ch_monofun] 81 82text \<open>continuity implies preservation of lubs\<close> 83 84lemma cont2contlubE: "cont f \<Longrightarrow> chain Y \<Longrightarrow> f (\<Squnion>i. Y i) = (\<Squnion>i. f (Y i))" 85 apply (rule lub_eqI [symmetric]) 86 apply (erule (1) contE) 87 done 88 89lemma contI2: 90 fixes f :: "'a::cpo \<Rightarrow> 'b::cpo" 91 assumes mono: "monofun f" 92 assumes below: "\<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. f (Y i))\<rbrakk> \<Longrightarrow> f (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. f (Y i))" 93 shows "cont f" 94proof (rule contI) 95 fix Y :: "nat \<Rightarrow> 'a" 96 assume Y: "chain Y" 97 with mono have fY: "chain (\<lambda>i. f (Y i))" 98 by (rule ch2ch_monofun) 99 have "(\<Squnion>i. f (Y i)) = f (\<Squnion>i. Y i)" 100 apply (rule below_antisym) 101 apply (rule lub_below [OF fY]) 102 apply (rule monofunE [OF mono]) 103 apply (rule is_ub_thelub [OF Y]) 104 apply (rule below [OF Y fY]) 105 done 106 with fY show "range (\<lambda>i. f (Y i)) <<| f (\<Squnion>i. Y i)" 107 by (rule thelubE) 108qed 109 110 111subsection \<open>Collection of continuity rules\<close> 112 113named_theorems cont2cont "continuity intro rule" 114 115 116subsection \<open>Continuity of basic functions\<close> 117 118text \<open>The identity function is continuous\<close> 119 120lemma cont_id [simp, cont2cont]: "cont (\<lambda>x. x)" 121 apply (rule contI) 122 apply (erule cpo_lubI) 123 done 124 125text \<open>constant functions are continuous\<close> 126 127lemma cont_const [simp, cont2cont]: "cont (\<lambda>x. c)" 128 using is_lub_const by (rule contI) 129 130text \<open>application of functions is continuous\<close> 131 132lemma cont_apply: 133 fixes f :: "'a::cpo \<Rightarrow> 'b::cpo \<Rightarrow> 'c::cpo" and t :: "'a \<Rightarrow> 'b" 134 assumes 1: "cont (\<lambda>x. t x)" 135 assumes 2: "\<And>x. cont (\<lambda>y. f x y)" 136 assumes 3: "\<And>y. cont (\<lambda>x. f x y)" 137 shows "cont (\<lambda>x. (f x) (t x))" 138proof (rule contI2 [OF monofunI]) 139 fix x y :: "'a" 140 assume "x \<sqsubseteq> y" 141 then show "f x (t x) \<sqsubseteq> f y (t y)" 142 by (auto intro: cont2monofunE [OF 1] 143 cont2monofunE [OF 2] 144 cont2monofunE [OF 3] 145 below_trans) 146next 147 fix Y :: "nat \<Rightarrow> 'a" 148 assume "chain Y" 149 then show "f (\<Squnion>i. Y i) (t (\<Squnion>i. Y i)) \<sqsubseteq> (\<Squnion>i. f (Y i) (t (Y i)))" 150 by (simp only: cont2contlubE [OF 1] ch2ch_cont [OF 1] 151 cont2contlubE [OF 2] ch2ch_cont [OF 2] 152 cont2contlubE [OF 3] ch2ch_cont [OF 3] 153 diag_lub below_refl) 154qed 155 156lemma cont_compose: "cont c \<Longrightarrow> cont (\<lambda>x. f x) \<Longrightarrow> cont (\<lambda>x. c (f x))" 157 by (rule cont_apply [OF _ _ cont_const]) 158 159text \<open>Least upper bounds preserve continuity\<close> 160 161lemma cont2cont_lub [simp]: 162 assumes chain: "\<And>x. chain (\<lambda>i. F i x)" 163 and cont: "\<And>i. cont (\<lambda>x. F i x)" 164 shows "cont (\<lambda>x. \<Squnion>i. F i x)" 165 apply (rule contI2) 166 apply (simp add: monofunI cont2monofunE [OF cont] lub_mono chain) 167 apply (simp add: cont2contlubE [OF cont]) 168 apply (simp add: diag_lub ch2ch_cont [OF cont] chain) 169 done 170 171text \<open>if-then-else is continuous\<close> 172 173lemma cont_if [simp, cont2cont]: "cont f \<Longrightarrow> cont g \<Longrightarrow> cont (\<lambda>x. if b then f x else g x)" 174 by (induct b) simp_all 175 176 177subsection \<open>Finite chains and flat pcpos\<close> 178 179text \<open>Monotone functions map finite chains to finite chains.\<close> 180 181lemma monofun_finch2finch: "monofun f \<Longrightarrow> finite_chain Y \<Longrightarrow> finite_chain (\<lambda>n. f (Y n))" 182 by (force simp add: finite_chain_def ch2ch_monofun max_in_chain_def) 183 184text \<open>The same holds for continuous functions.\<close> 185 186lemma cont_finch2finch: "cont f \<Longrightarrow> finite_chain Y \<Longrightarrow> finite_chain (\<lambda>n. f (Y n))" 187 by (rule cont2mono [THEN monofun_finch2finch]) 188 189text \<open>All monotone functions with chain-finite domain are continuous.\<close> 190 191lemma chfindom_monofun2cont: "monofun f \<Longrightarrow> cont f" 192 for f :: "'a::chfin \<Rightarrow> 'b::cpo" 193 apply (erule contI2) 194 apply (frule chfin2finch) 195 apply (clarsimp simp add: finite_chain_def) 196 apply (subgoal_tac "max_in_chain i (\<lambda>i. f (Y i))") 197 apply (simp add: maxinch_is_thelub ch2ch_monofun) 198 apply (force simp add: max_in_chain_def) 199 done 200 201text \<open>All strict functions with flat domain are continuous.\<close> 202 203lemma flatdom_strict2mono: "f \<bottom> = \<bottom> \<Longrightarrow> monofun f" 204 for f :: "'a::flat \<Rightarrow> 'b::pcpo" 205 apply (rule monofunI) 206 apply (drule ax_flat) 207 apply auto 208 done 209 210lemma flatdom_strict2cont: "f \<bottom> = \<bottom> \<Longrightarrow> cont f" 211 for f :: "'a::flat \<Rightarrow> 'b::pcpo" 212 by (rule flatdom_strict2mono [THEN chfindom_monofun2cont]) 213 214text \<open>All functions with discrete domain are continuous.\<close> 215 216lemma cont_discrete_cpo [simp, cont2cont]: "cont f" 217 for f :: "'a::discrete_cpo \<Rightarrow> 'b::cpo" 218 apply (rule contI) 219 apply (drule discrete_chain_const, clarify) 220 apply simp 221 done 222 223end 224