src/HOLCF/Fun_Cpo.thy
author huffman
Mon Oct 11 16:24:44 2010 -0700 (2010-10-11)
changeset 40001 666c3751227c
parent 39302 src/HOLCF/Ffun.thy@d7728f65b353
child 40002 c5b5f7a3a3b1
permissions -rw-r--r--
rename Ffun.thy to Fun_Cpo.thy
huffman@40001
     1
(*  Title:      HOLCF/Fun_Cpo.thy
huffman@16202
     2
    Author:     Franz Regensburger
huffman@40001
     3
    Author:     Brian Huffman
huffman@16202
     4
*)
huffman@16202
     5
huffman@16202
     6
header {* Class instances for the full function space *}
huffman@16202
     7
huffman@40001
     8
theory Fun_Cpo
huffman@25786
     9
imports Cont
huffman@16202
    10
begin
huffman@16202
    11
huffman@18291
    12
subsection {* Full function space is a partial order *}
huffman@16202
    13
huffman@31076
    14
instantiation "fun"  :: (type, below) below
huffman@25758
    15
begin
huffman@16202
    16
huffman@25758
    17
definition
huffman@31076
    18
  below_fun_def: "(op \<sqsubseteq>) \<equiv> (\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x)"
huffman@16202
    19
huffman@25758
    20
instance ..
huffman@25758
    21
end
huffman@16202
    22
huffman@25758
    23
instance "fun" :: (type, po) po
huffman@25758
    24
proof
huffman@25758
    25
  fix f :: "'a \<Rightarrow> 'b"
huffman@25758
    26
  show "f \<sqsubseteq> f"
huffman@31076
    27
    by (simp add: below_fun_def)
huffman@25758
    28
next
huffman@25758
    29
  fix f g :: "'a \<Rightarrow> 'b"
huffman@25758
    30
  assume "f \<sqsubseteq> g" and "g \<sqsubseteq> f" thus "f = g"
nipkow@39302
    31
    by (simp add: below_fun_def fun_eq_iff below_antisym)
huffman@25758
    32
next
huffman@25758
    33
  fix f g h :: "'a \<Rightarrow> 'b"
huffman@25758
    34
  assume "f \<sqsubseteq> g" and "g \<sqsubseteq> h" thus "f \<sqsubseteq> h"
huffman@31076
    35
    unfolding below_fun_def by (fast elim: below_trans)
huffman@25758
    36
qed
huffman@16202
    37
huffman@16202
    38
text {* make the symbol @{text "<<"} accessible for type fun *}
huffman@16202
    39
huffman@31076
    40
lemma expand_fun_below: "(f \<sqsubseteq> g) = (\<forall>x. f x \<sqsubseteq> g x)"
huffman@31076
    41
by (simp add: below_fun_def)
huffman@16202
    42
huffman@31076
    43
lemma below_fun_ext: "(\<And>x. f x \<sqsubseteq> g x) \<Longrightarrow> f \<sqsubseteq> g"
huffman@31076
    44
by (simp add: below_fun_def)
huffman@16202
    45
huffman@18291
    46
subsection {* Full function space is chain complete *}
huffman@16202
    47
huffman@25786
    48
text {* function application is monotone *}
huffman@25786
    49
huffman@25786
    50
lemma monofun_app: "monofun (\<lambda>f. f x)"
huffman@31076
    51
by (rule monofunI, simp add: below_fun_def)
huffman@25786
    52
huffman@16202
    53
text {* chains of functions yield chains in the po range *}
huffman@16202
    54
huffman@16202
    55
lemma ch2ch_fun: "chain S \<Longrightarrow> chain (\<lambda>i. S i x)"
huffman@31076
    56
by (simp add: chain_def below_fun_def)
huffman@16202
    57
huffman@18092
    58
lemma ch2ch_lambda: "(\<And>x. chain (\<lambda>i. S i x)) \<Longrightarrow> chain S"
huffman@31076
    59
by (simp add: chain_def below_fun_def)
huffman@16202
    60
huffman@16202
    61
text {* upper bounds of function chains yield upper bound in the po range *}
huffman@16202
    62
huffman@16202
    63
lemma ub2ub_fun:
huffman@26028
    64
  "range S <| u \<Longrightarrow> range (\<lambda>i. S i x) <| u x"
huffman@31076
    65
by (auto simp add: is_ub_def below_fun_def)
huffman@16202
    66
huffman@16202
    67
text {* Type @{typ "'a::type => 'b::cpo"} is chain complete *}
huffman@16202
    68
huffman@26028
    69
lemma is_lub_lambda:
huffman@26028
    70
  assumes f: "\<And>x. range (\<lambda>i. Y i x) <<| f x"
huffman@26028
    71
  shows "range Y <<| f"
huffman@26028
    72
apply (rule is_lubI)
huffman@26028
    73
apply (rule ub_rangeI)
huffman@31076
    74
apply (rule below_fun_ext)
huffman@26028
    75
apply (rule is_ub_lub [OF f])
huffman@31076
    76
apply (rule below_fun_ext)
huffman@26028
    77
apply (rule is_lub_lub [OF f])
huffman@26028
    78
apply (erule ub2ub_fun)
huffman@26028
    79
done
huffman@26028
    80
huffman@16202
    81
lemma lub_fun:
huffman@16202
    82
  "chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo)
huffman@16202
    83
    \<Longrightarrow> range S <<| (\<lambda>x. \<Squnion>i. S i x)"
huffman@26028
    84
apply (rule is_lub_lambda)
huffman@26028
    85
apply (rule cpo_lubI)
huffman@16202
    86
apply (erule ch2ch_fun)
huffman@16202
    87
done
huffman@16202
    88
huffman@16202
    89
lemma thelub_fun:
huffman@16202
    90
  "chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo)
huffman@27413
    91
    \<Longrightarrow> (\<Squnion>i. S i) = (\<lambda>x. \<Squnion>i. S i x)"
huffman@16202
    92
by (rule lub_fun [THEN thelubI])
huffman@16202
    93
huffman@16202
    94
lemma cpo_fun:
huffman@16202
    95
  "chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo) \<Longrightarrow> \<exists>x. range S <<| x"
huffman@16202
    96
by (rule exI, erule lub_fun)
huffman@16202
    97
krauss@20523
    98
instance "fun"  :: (type, cpo) cpo
huffman@16202
    99
by intro_classes (rule cpo_fun)
huffman@16202
   100
huffman@25827
   101
instance "fun" :: (finite, finite_po) finite_po ..
huffman@25827
   102
huffman@26025
   103
instance "fun" :: (type, discrete_cpo) discrete_cpo
huffman@26025
   104
proof
huffman@26025
   105
  fix f g :: "'a \<Rightarrow> 'b"
huffman@26025
   106
  show "f \<sqsubseteq> g \<longleftrightarrow> f = g" 
nipkow@39302
   107
    unfolding expand_fun_below fun_eq_iff
huffman@26025
   108
    by simp
huffman@26025
   109
qed
huffman@26025
   110
huffman@25827
   111
text {* chain-finite function spaces *}
huffman@25827
   112
huffman@25827
   113
lemma maxinch2maxinch_lambda:
huffman@25827
   114
  "(\<And>x. max_in_chain n (\<lambda>i. S i x)) \<Longrightarrow> max_in_chain n S"
nipkow@39302
   115
unfolding max_in_chain_def fun_eq_iff by simp
huffman@25827
   116
huffman@25827
   117
lemma maxinch_mono:
huffman@25827
   118
  "\<lbrakk>max_in_chain i Y; i \<le> j\<rbrakk> \<Longrightarrow> max_in_chain j Y"
huffman@25827
   119
unfolding max_in_chain_def
huffman@25827
   120
proof (intro allI impI)
huffman@25827
   121
  fix k
huffman@25827
   122
  assume Y: "\<forall>n\<ge>i. Y i = Y n"
huffman@25827
   123
  assume ij: "i \<le> j"
huffman@25827
   124
  assume jk: "j \<le> k"
huffman@25827
   125
  from ij jk have ik: "i \<le> k" by simp
huffman@25827
   126
  from Y ij have Yij: "Y i = Y j" by simp
huffman@25827
   127
  from Y ik have Yik: "Y i = Y k" by simp
huffman@25827
   128
  from Yij Yik show "Y j = Y k" by auto
huffman@25827
   129
qed
huffman@25827
   130
huffman@25827
   131
instance "fun" :: (finite, chfin) chfin
huffman@25921
   132
proof
huffman@25827
   133
  fix Y :: "nat \<Rightarrow> 'a \<Rightarrow> 'b"
huffman@25827
   134
  let ?n = "\<lambda>x. LEAST n. max_in_chain n (\<lambda>i. Y i x)"
huffman@25827
   135
  assume "chain Y"
huffman@25827
   136
  hence "\<And>x. chain (\<lambda>i. Y i x)"
huffman@25827
   137
    by (rule ch2ch_fun)
huffman@25827
   138
  hence "\<And>x. \<exists>n. max_in_chain n (\<lambda>i. Y i x)"
huffman@25921
   139
    by (rule chfin)
huffman@25827
   140
  hence "\<And>x. max_in_chain (?n x) (\<lambda>i. Y i x)"
huffman@25827
   141
    by (rule LeastI_ex)
huffman@25827
   142
  hence "\<And>x. max_in_chain (Max (range ?n)) (\<lambda>i. Y i x)"
huffman@25827
   143
    by (rule maxinch_mono [OF _ Max_ge], simp_all)
huffman@25827
   144
  hence "max_in_chain (Max (range ?n)) Y"
huffman@25827
   145
    by (rule maxinch2maxinch_lambda)
huffman@25827
   146
  thus "\<exists>n. max_in_chain n Y" ..
huffman@25827
   147
qed
huffman@25827
   148
huffman@18291
   149
subsection {* Full function space is pointed *}
huffman@17831
   150
huffman@17831
   151
lemma minimal_fun: "(\<lambda>x. \<bottom>) \<sqsubseteq> f"
huffman@31076
   152
by (simp add: below_fun_def)
huffman@17831
   153
huffman@25786
   154
lemma least_fun: "\<exists>x::'a::type \<Rightarrow> 'b::pcpo. \<forall>y. x \<sqsubseteq> y"
huffman@17831
   155
apply (rule_tac x = "\<lambda>x. \<bottom>" in exI)
huffman@17831
   156
apply (rule minimal_fun [THEN allI])
huffman@17831
   157
done
huffman@17831
   158
krauss@20523
   159
instance "fun"  :: (type, pcpo) pcpo
huffman@16202
   160
by intro_classes (rule least_fun)
huffman@16202
   161
huffman@16202
   162
text {* for compatibility with old HOLCF-Version *}
huffman@17831
   163
lemma inst_fun_pcpo: "\<bottom> = (\<lambda>x. \<bottom>)"
huffman@16202
   164
by (rule minimal_fun [THEN UU_I, symmetric])
huffman@16202
   165
huffman@16202
   166
text {* function application is strict in the left argument *}
huffman@16202
   167
lemma app_strict [simp]: "\<bottom> x = \<bottom>"
huffman@16202
   168
by (simp add: inst_fun_pcpo)
huffman@16202
   169
huffman@25786
   170
text {*
huffman@25786
   171
  The following results are about application for functions in @{typ "'a=>'b"}
huffman@25786
   172
*}
huffman@25786
   173
huffman@25786
   174
lemma monofun_fun_fun: "f \<sqsubseteq> g \<Longrightarrow> f x \<sqsubseteq> g x"
huffman@31076
   175
by (simp add: below_fun_def)
huffman@25786
   176
huffman@25786
   177
lemma monofun_fun_arg: "\<lbrakk>monofun f; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> f x \<sqsubseteq> f y"
huffman@25786
   178
by (rule monofunE)
huffman@25786
   179
huffman@25786
   180
lemma monofun_fun: "\<lbrakk>monofun f; monofun g; f \<sqsubseteq> g; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> f x \<sqsubseteq> g y"
huffman@31076
   181
by (rule below_trans [OF monofun_fun_arg monofun_fun_fun])
huffman@25786
   182
huffman@25786
   183
subsection {* Propagation of monotonicity and continuity *}
huffman@25786
   184
huffman@25786
   185
text {* the lub of a chain of monotone functions is monotone *}
huffman@25786
   186
huffman@25786
   187
lemma monofun_lub_fun:
huffman@25786
   188
  "\<lbrakk>chain (F::nat \<Rightarrow> 'a \<Rightarrow> 'b::cpo); \<forall>i. monofun (F i)\<rbrakk>
huffman@25786
   189
    \<Longrightarrow> monofun (\<Squnion>i. F i)"
huffman@25786
   190
apply (rule monofunI)
huffman@25786
   191
apply (simp add: thelub_fun)
huffman@25923
   192
apply (rule lub_mono)
huffman@25786
   193
apply (erule ch2ch_fun)
huffman@25786
   194
apply (erule ch2ch_fun)
huffman@25786
   195
apply (simp add: monofunE)
huffman@25786
   196
done
huffman@25786
   197
huffman@25786
   198
text {* the lub of a chain of continuous functions is continuous *}
huffman@25786
   199
huffman@25786
   200
lemma cont_lub_fun:
huffman@25786
   201
  "\<lbrakk>chain F; \<forall>i. cont (F i)\<rbrakk> \<Longrightarrow> cont (\<Squnion>i. F i)"
huffman@35914
   202
apply (rule contI2)
huffman@25786
   203
apply (erule monofun_lub_fun)
huffman@25786
   204
apply (simp add: cont2mono)
huffman@35914
   205
apply (simp add: thelub_fun cont2contlubE)
huffman@35914
   206
apply (simp add: diag_lub ch2ch_fun ch2ch_cont)
huffman@25786
   207
done
huffman@25786
   208
huffman@25786
   209
lemma cont2cont_lub:
huffman@25786
   210
  "\<lbrakk>chain F; \<And>i. cont (F i)\<rbrakk> \<Longrightarrow> cont (\<lambda>x. \<Squnion>i. F i x)"
huffman@25786
   211
by (simp add: thelub_fun [symmetric] cont_lub_fun)
huffman@25786
   212
huffman@25786
   213
lemma mono2mono_fun: "monofun f \<Longrightarrow> monofun (\<lambda>x. f x y)"
huffman@25786
   214
apply (rule monofunI)
huffman@25786
   215
apply (erule (1) monofun_fun_arg [THEN monofun_fun_fun])
huffman@25786
   216
done
huffman@25786
   217
huffman@25786
   218
lemma cont2cont_fun: "cont f \<Longrightarrow> cont (\<lambda>x. f x y)"
huffman@35914
   219
apply (rule contI2)
huffman@25786
   220
apply (erule cont2mono [THEN mono2mono_fun])
huffman@25786
   221
apply (simp add: cont2contlubE)
huffman@25786
   222
apply (simp add: thelub_fun ch2ch_cont)
huffman@25786
   223
done
huffman@25786
   224
huffman@25786
   225
text {* Note @{text "(\<lambda>x. \<lambda>y. f x y) = f"} *}
huffman@25786
   226
huffman@26452
   227
lemma mono2mono_lambda:
huffman@26452
   228
  assumes f: "\<And>y. monofun (\<lambda>x. f x y)" shows "monofun f"
huffman@25786
   229
apply (rule monofunI)
huffman@31076
   230
apply (rule below_fun_ext)
huffman@26452
   231
apply (erule monofunE [OF f])
huffman@25786
   232
done
huffman@25786
   233
huffman@26452
   234
lemma cont2cont_lambda [simp]:
huffman@26452
   235
  assumes f: "\<And>y. cont (\<lambda>x. f x y)" shows "cont f"
huffman@35914
   236
apply (rule contI2)
huffman@26452
   237
apply (simp add: mono2mono_lambda cont2mono f)
huffman@35914
   238
apply (rule below_fun_ext)
huffman@35914
   239
apply (simp add: thelub_fun cont2contlubE [OF f])
huffman@25786
   240
done
huffman@25786
   241
huffman@25786
   242
text {* What D.A.Schmidt calls continuity of abstraction; never used here *}
huffman@25786
   243
huffman@25786
   244
lemma contlub_lambda:
huffman@25786
   245
  "(\<And>x::'a::type. chain (\<lambda>i. S i x::'b::cpo))
huffman@25786
   246
    \<Longrightarrow> (\<lambda>x. \<Squnion>i. S i x) = (\<Squnion>i. (\<lambda>x. S i x))"
huffman@25786
   247
by (simp add: thelub_fun ch2ch_lambda)
huffman@25786
   248
huffman@25786
   249
lemma contlub_abstraction:
huffman@25786
   250
  "\<lbrakk>chain Y; \<forall>y. cont (\<lambda>x.(c::'a::cpo\<Rightarrow>'b::type\<Rightarrow>'c::cpo) x y)\<rbrakk> \<Longrightarrow>
huffman@25786
   251
    (\<lambda>y. \<Squnion>i. c (Y i) y) = (\<Squnion>i. (\<lambda>y. c (Y i) y))"
huffman@25786
   252
apply (rule thelub_fun [symmetric])
huffman@26452
   253
apply (simp add: ch2ch_cont)
huffman@25786
   254
done
huffman@25786
   255
huffman@25786
   256
lemma mono2mono_app:
huffman@25786
   257
  "\<lbrakk>monofun f; \<forall>x. monofun (f x); monofun t\<rbrakk> \<Longrightarrow> monofun (\<lambda>x. (f x) (t x))"
huffman@25786
   258
apply (rule monofunI)
huffman@25786
   259
apply (simp add: monofun_fun monofunE)
huffman@25786
   260
done
huffman@25786
   261
huffman@25786
   262
lemma cont2cont_app:
huffman@25786
   263
  "\<lbrakk>cont f; \<forall>x. cont (f x); cont t\<rbrakk> \<Longrightarrow> cont (\<lambda>x. (f x) (t x))"
huffman@35914
   264
apply (erule cont_apply [where t=t])
huffman@35914
   265
apply (erule spec)
huffman@35914
   266
apply (erule cont2cont_fun)
huffman@35914
   267
done
huffman@25786
   268
huffman@25786
   269
lemmas cont2cont_app2 = cont2cont_app [rule_format]
huffman@25786
   270
huffman@25786
   271
lemma cont2cont_app3: "\<lbrakk>cont f; cont t\<rbrakk> \<Longrightarrow> cont (\<lambda>x. f (t x))"
huffman@25786
   272
by (rule cont2cont_app2 [OF cont_const])
huffman@25786
   273
huffman@16202
   274
end