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