src/HOLCF/Ffun.thy
author huffman
Fri Jan 04 00:01:02 2008 +0100 (2008-01-04)
changeset 25827 c2adeb1bae5c
parent 25786 6b3c79acac1f
child 25906 2179c6661218
permissions -rw-r--r--
new instance proofs for classes finite_po, chfin, flat
huffman@16202
     1
(*  Title:      HOLCF/FunCpo.thy
huffman@16202
     2
    ID:         $Id$
huffman@16202
     3
    Author:     Franz Regensburger
huffman@16202
     4
huffman@16202
     5
Definition of the partial ordering for the type of all functions => (fun)
huffman@16202
     6
huffman@16202
     7
Class instance of  => (fun) for class pcpo.
huffman@16202
     8
*)
huffman@16202
     9
huffman@16202
    10
header {* Class instances for the full function space *}
huffman@16202
    11
huffman@16202
    12
theory Ffun
huffman@25786
    13
imports Cont
huffman@16202
    14
begin
huffman@16202
    15
huffman@18291
    16
subsection {* Full function space is a partial order *}
huffman@16202
    17
huffman@25758
    18
instantiation "fun"  :: (type, sq_ord) sq_ord
huffman@25758
    19
begin
huffman@16202
    20
huffman@25758
    21
definition
huffman@16202
    22
  less_fun_def: "(op \<sqsubseteq>) \<equiv> (\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x)"  
huffman@16202
    23
huffman@25758
    24
instance ..
huffman@25758
    25
end
huffman@16202
    26
huffman@25758
    27
instance "fun" :: (type, po) po
huffman@25758
    28
proof
huffman@25758
    29
  fix f :: "'a \<Rightarrow> 'b"
huffman@25758
    30
  show "f \<sqsubseteq> f"
huffman@25758
    31
    by (simp add: less_fun_def)
huffman@25758
    32
next
huffman@25758
    33
  fix f g :: "'a \<Rightarrow> 'b"
huffman@25758
    34
  assume "f \<sqsubseteq> g" and "g \<sqsubseteq> f" thus "f = g"
huffman@25758
    35
    by (simp add: less_fun_def expand_fun_eq antisym_less)
huffman@25758
    36
next
huffman@25758
    37
  fix f g h :: "'a \<Rightarrow> 'b"
huffman@25758
    38
  assume "f \<sqsubseteq> g" and "g \<sqsubseteq> h" thus "f \<sqsubseteq> h"
huffman@25758
    39
    unfolding less_fun_def by (fast elim: trans_less)
huffman@25758
    40
qed
huffman@16202
    41
huffman@16202
    42
text {* make the symbol @{text "<<"} accessible for type fun *}
huffman@16202
    43
huffman@17831
    44
lemma expand_fun_less: "(f \<sqsubseteq> g) = (\<forall>x. f x \<sqsubseteq> g x)"
huffman@16202
    45
by (simp add: less_fun_def)
huffman@16202
    46
huffman@16202
    47
lemma less_fun_ext: "(\<And>x. f x \<sqsubseteq> g x) \<Longrightarrow> f \<sqsubseteq> g"
huffman@16202
    48
by (simp add: less_fun_def)
huffman@16202
    49
huffman@18291
    50
subsection {* Full function space is chain complete *}
huffman@16202
    51
huffman@25786
    52
text {* function application is monotone *}
huffman@25786
    53
huffman@25786
    54
lemma monofun_app: "monofun (\<lambda>f. f x)"
huffman@25786
    55
by (rule monofunI, simp add: less_fun_def)
huffman@25786
    56
huffman@16202
    57
text {* chains of functions yield chains in the po range *}
huffman@16202
    58
huffman@16202
    59
lemma ch2ch_fun: "chain S \<Longrightarrow> chain (\<lambda>i. S i x)"
huffman@16202
    60
by (simp add: chain_def less_fun_def)
huffman@16202
    61
huffman@18092
    62
lemma ch2ch_lambda: "(\<And>x. chain (\<lambda>i. S i x)) \<Longrightarrow> chain S"
huffman@16202
    63
by (simp add: chain_def less_fun_def)
huffman@16202
    64
huffman@16202
    65
text {* upper bounds of function chains yield upper bound in the po range *}
huffman@16202
    66
huffman@16202
    67
lemma ub2ub_fun:
huffman@25786
    68
  "range (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::po) <| u \<Longrightarrow> range (\<lambda>i. S i x) <| u x"
huffman@16202
    69
by (auto simp add: is_ub_def less_fun_def)
huffman@16202
    70
huffman@16202
    71
text {* Type @{typ "'a::type => 'b::cpo"} is chain complete *}
huffman@16202
    72
huffman@16202
    73
lemma lub_fun:
huffman@16202
    74
  "chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo)
huffman@16202
    75
    \<Longrightarrow> range S <<| (\<lambda>x. \<Squnion>i. S i x)"
huffman@16202
    76
apply (rule is_lubI)
huffman@16202
    77
apply (rule ub_rangeI)
huffman@16202
    78
apply (rule less_fun_ext)
huffman@16202
    79
apply (rule is_ub_thelub)
huffman@16202
    80
apply (erule ch2ch_fun)
huffman@16202
    81
apply (rule less_fun_ext)
huffman@16202
    82
apply (rule is_lub_thelub)
huffman@16202
    83
apply (erule ch2ch_fun)
huffman@16202
    84
apply (erule ub2ub_fun)
huffman@16202
    85
done
huffman@16202
    86
huffman@25786
    87
lemma lub_fun':
huffman@25786
    88
  fixes S :: "('a::type \<Rightarrow> 'b::dcpo) set"
huffman@25786
    89
  assumes S: "directed S"
huffman@25786
    90
  shows "S <<| (\<lambda>x. \<Squnion>f\<in>S. f x)"
huffman@25786
    91
apply (rule is_lubI)
huffman@25786
    92
apply (rule is_ubI)
huffman@25786
    93
apply (rule less_fun_ext)
huffman@25786
    94
apply (rule is_ub_thelub')
huffman@25786
    95
apply (rule dir2dir_monofun [OF monofun_app S])
huffman@25786
    96
apply (erule imageI)
huffman@25786
    97
apply (rule less_fun_ext)
huffman@25786
    98
apply (rule is_lub_thelub')
huffman@25786
    99
apply (rule dir2dir_monofun [OF monofun_app S])
huffman@25786
   100
apply (erule ub2ub_monofun' [OF monofun_app])
huffman@25786
   101
done
huffman@25786
   102
huffman@16202
   103
lemma thelub_fun:
huffman@16202
   104
  "chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo)
huffman@16202
   105
    \<Longrightarrow> lub (range S) = (\<lambda>x. \<Squnion>i. S i x)"
huffman@16202
   106
by (rule lub_fun [THEN thelubI])
huffman@16202
   107
huffman@25786
   108
lemma thelub_fun':
huffman@25786
   109
  "directed (S::('a::type \<Rightarrow> 'b::dcpo) set)
huffman@25786
   110
    \<Longrightarrow> lub S = (\<lambda>x. \<Squnion>f\<in>S. f x)"
huffman@25786
   111
by (rule lub_fun' [THEN thelubI])
huffman@25786
   112
huffman@16202
   113
lemma cpo_fun:
huffman@16202
   114
  "chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo) \<Longrightarrow> \<exists>x. range S <<| x"
huffman@16202
   115
by (rule exI, erule lub_fun)
huffman@16202
   116
krauss@20523
   117
instance "fun"  :: (type, cpo) cpo
huffman@16202
   118
by intro_classes (rule cpo_fun)
huffman@16202
   119
huffman@25786
   120
lemma dcpo_fun:
huffman@25786
   121
  "directed (S::('a::type \<Rightarrow> 'b::dcpo) set) \<Longrightarrow> \<exists>x. S <<| x"
huffman@25786
   122
by (rule exI, erule lub_fun')
huffman@25786
   123
huffman@25786
   124
instance "fun" :: (type, dcpo) dcpo
huffman@25786
   125
by intro_classes (rule dcpo_fun)
huffman@25786
   126
huffman@25827
   127
instance "fun" :: (finite, finite_po) finite_po ..
huffman@25827
   128
huffman@25827
   129
text {* chain-finite function spaces *}
huffman@25827
   130
huffman@25827
   131
lemma maxinch2maxinch_lambda:
huffman@25827
   132
  "(\<And>x. max_in_chain n (\<lambda>i. S i x)) \<Longrightarrow> max_in_chain n S"
huffman@25827
   133
unfolding max_in_chain_def expand_fun_eq by simp
huffman@25827
   134
huffman@25827
   135
lemma maxinch_mono:
huffman@25827
   136
  "\<lbrakk>max_in_chain i Y; i \<le> j\<rbrakk> \<Longrightarrow> max_in_chain j Y"
huffman@25827
   137
unfolding max_in_chain_def
huffman@25827
   138
proof (intro allI impI)
huffman@25827
   139
  fix k
huffman@25827
   140
  assume Y: "\<forall>n\<ge>i. Y i = Y n"
huffman@25827
   141
  assume ij: "i \<le> j"
huffman@25827
   142
  assume jk: "j \<le> k"
huffman@25827
   143
  from ij jk have ik: "i \<le> k" by simp
huffman@25827
   144
  from Y ij have Yij: "Y i = Y j" by simp
huffman@25827
   145
  from Y ik have Yik: "Y i = Y k" by simp
huffman@25827
   146
  from Yij Yik show "Y j = Y k" by auto
huffman@25827
   147
qed
huffman@25827
   148
huffman@25827
   149
instance "fun" :: (finite, chfin) chfin
huffman@25827
   150
proof (intro_classes, clarify)
huffman@25827
   151
  fix Y :: "nat \<Rightarrow> 'a \<Rightarrow> 'b"
huffman@25827
   152
  let ?n = "\<lambda>x. LEAST n. max_in_chain n (\<lambda>i. Y i x)"
huffman@25827
   153
  assume "chain Y"
huffman@25827
   154
  hence "\<And>x. chain (\<lambda>i. Y i x)"
huffman@25827
   155
    by (rule ch2ch_fun)
huffman@25827
   156
  hence "\<And>x. \<exists>n. max_in_chain n (\<lambda>i. Y i x)"
huffman@25827
   157
    by (rule chfin [rule_format])
huffman@25827
   158
  hence "\<And>x. max_in_chain (?n x) (\<lambda>i. Y i x)"
huffman@25827
   159
    by (rule LeastI_ex)
huffman@25827
   160
  hence "\<And>x. max_in_chain (Max (range ?n)) (\<lambda>i. Y i x)"
huffman@25827
   161
    by (rule maxinch_mono [OF _ Max_ge], simp_all)
huffman@25827
   162
  hence "max_in_chain (Max (range ?n)) Y"
huffman@25827
   163
    by (rule maxinch2maxinch_lambda)
huffman@25827
   164
  thus "\<exists>n. max_in_chain n Y" ..
huffman@25827
   165
qed
huffman@25827
   166
huffman@18291
   167
subsection {* Full function space is pointed *}
huffman@17831
   168
huffman@17831
   169
lemma minimal_fun: "(\<lambda>x. \<bottom>) \<sqsubseteq> f"
huffman@17831
   170
by (simp add: less_fun_def)
huffman@17831
   171
huffman@25786
   172
lemma least_fun: "\<exists>x::'a::type \<Rightarrow> 'b::pcpo. \<forall>y. x \<sqsubseteq> y"
huffman@17831
   173
apply (rule_tac x = "\<lambda>x. \<bottom>" in exI)
huffman@17831
   174
apply (rule minimal_fun [THEN allI])
huffman@17831
   175
done
huffman@17831
   176
krauss@20523
   177
instance "fun"  :: (type, pcpo) pcpo
huffman@16202
   178
by intro_classes (rule least_fun)
huffman@16202
   179
huffman@16202
   180
text {* for compatibility with old HOLCF-Version *}
huffman@17831
   181
lemma inst_fun_pcpo: "\<bottom> = (\<lambda>x. \<bottom>)"
huffman@16202
   182
by (rule minimal_fun [THEN UU_I, symmetric])
huffman@16202
   183
huffman@16202
   184
text {* function application is strict in the left argument *}
huffman@16202
   185
lemma app_strict [simp]: "\<bottom> x = \<bottom>"
huffman@16202
   186
by (simp add: inst_fun_pcpo)
huffman@16202
   187
huffman@25786
   188
text {*
huffman@25786
   189
  The following results are about application for functions in @{typ "'a=>'b"}
huffman@25786
   190
*}
huffman@25786
   191
huffman@25786
   192
lemma monofun_fun_fun: "f \<sqsubseteq> g \<Longrightarrow> f x \<sqsubseteq> g x"
huffman@25786
   193
by (simp add: less_fun_def)
huffman@25786
   194
huffman@25786
   195
lemma monofun_fun_arg: "\<lbrakk>monofun f; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> f x \<sqsubseteq> f y"
huffman@25786
   196
by (rule monofunE)
huffman@25786
   197
huffman@25786
   198
lemma monofun_fun: "\<lbrakk>monofun f; monofun g; f \<sqsubseteq> g; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> f x \<sqsubseteq> g y"
huffman@25786
   199
by (rule trans_less [OF monofun_fun_arg monofun_fun_fun])
huffman@25786
   200
huffman@25786
   201
subsection {* Propagation of monotonicity and continuity *}
huffman@25786
   202
huffman@25786
   203
text {* the lub of a chain of monotone functions is monotone *}
huffman@25786
   204
huffman@25786
   205
lemma monofun_lub_fun:
huffman@25786
   206
  "\<lbrakk>chain (F::nat \<Rightarrow> 'a \<Rightarrow> 'b::cpo); \<forall>i. monofun (F i)\<rbrakk>
huffman@25786
   207
    \<Longrightarrow> monofun (\<Squnion>i. F i)"
huffman@25786
   208
apply (rule monofunI)
huffman@25786
   209
apply (simp add: thelub_fun)
huffman@25786
   210
apply (rule lub_mono [rule_format])
huffman@25786
   211
apply (erule ch2ch_fun)
huffman@25786
   212
apply (erule ch2ch_fun)
huffman@25786
   213
apply (simp add: monofunE)
huffman@25786
   214
done
huffman@25786
   215
huffman@25786
   216
text {* the lub of a chain of continuous functions is continuous *}
huffman@25786
   217
huffman@25786
   218
declare range_composition [simp del]
huffman@25786
   219
huffman@25786
   220
lemma contlub_lub_fun:
huffman@25786
   221
  "\<lbrakk>chain F; \<forall>i. cont (F i)\<rbrakk> \<Longrightarrow> contlub (\<Squnion>i. F i)"
huffman@25786
   222
apply (rule contlubI)
huffman@25786
   223
apply (simp add: thelub_fun)
huffman@25786
   224
apply (simp add: cont2contlubE)
huffman@25786
   225
apply (rule ex_lub)
huffman@25786
   226
apply (erule ch2ch_fun)
huffman@25786
   227
apply (simp add: ch2ch_cont)
huffman@25786
   228
done
huffman@25786
   229
huffman@25786
   230
lemma cont_lub_fun:
huffman@25786
   231
  "\<lbrakk>chain F; \<forall>i. cont (F i)\<rbrakk> \<Longrightarrow> cont (\<Squnion>i. F i)"
huffman@25786
   232
apply (rule monocontlub2cont)
huffman@25786
   233
apply (erule monofun_lub_fun)
huffman@25786
   234
apply (simp add: cont2mono)
huffman@25786
   235
apply (erule (1) contlub_lub_fun)
huffman@25786
   236
done
huffman@25786
   237
huffman@25786
   238
lemma cont2cont_lub:
huffman@25786
   239
  "\<lbrakk>chain F; \<And>i. cont (F i)\<rbrakk> \<Longrightarrow> cont (\<lambda>x. \<Squnion>i. F i x)"
huffman@25786
   240
by (simp add: thelub_fun [symmetric] cont_lub_fun)
huffman@25786
   241
huffman@25786
   242
lemma mono2mono_fun: "monofun f \<Longrightarrow> monofun (\<lambda>x. f x y)"
huffman@25786
   243
apply (rule monofunI)
huffman@25786
   244
apply (erule (1) monofun_fun_arg [THEN monofun_fun_fun])
huffman@25786
   245
done
huffman@25786
   246
huffman@25786
   247
lemma cont2cont_fun: "cont f \<Longrightarrow> cont (\<lambda>x. f x y)"
huffman@25786
   248
apply (rule monocontlub2cont)
huffman@25786
   249
apply (erule cont2mono [THEN mono2mono_fun])
huffman@25786
   250
apply (rule contlubI)
huffman@25786
   251
apply (simp add: cont2contlubE)
huffman@25786
   252
apply (simp add: thelub_fun ch2ch_cont)
huffman@25786
   253
done
huffman@25786
   254
huffman@25786
   255
text {* Note @{text "(\<lambda>x. \<lambda>y. f x y) = f"} *}
huffman@25786
   256
huffman@25786
   257
lemma mono2mono_lambda: "(\<And>y. monofun (\<lambda>x. f x y)) \<Longrightarrow> monofun f"
huffman@25786
   258
apply (rule monofunI)
huffman@25786
   259
apply (rule less_fun_ext)
huffman@25786
   260
apply (blast dest: monofunE)
huffman@25786
   261
done
huffman@25786
   262
huffman@25786
   263
lemma cont2cont_lambda: "(\<And>y. cont (\<lambda>x. f x y)) \<Longrightarrow> cont f"
huffman@25786
   264
apply (subgoal_tac "monofun f")
huffman@25786
   265
apply (rule monocontlub2cont)
huffman@25786
   266
apply assumption
huffman@25786
   267
apply (rule contlubI)
huffman@25786
   268
apply (rule ext)
huffman@25786
   269
apply (simp add: thelub_fun ch2ch_monofun)
huffman@25786
   270
apply (blast dest: cont2contlubE)
huffman@25786
   271
apply (simp add: mono2mono_lambda cont2mono)
huffman@25786
   272
done
huffman@25786
   273
huffman@25786
   274
text {* What D.A.Schmidt calls continuity of abstraction; never used here *}
huffman@25786
   275
huffman@25786
   276
lemma contlub_lambda:
huffman@25786
   277
  "(\<And>x::'a::type. chain (\<lambda>i. S i x::'b::cpo))
huffman@25786
   278
    \<Longrightarrow> (\<lambda>x. \<Squnion>i. S i x) = (\<Squnion>i. (\<lambda>x. S i x))"
huffman@25786
   279
by (simp add: thelub_fun ch2ch_lambda)
huffman@25786
   280
huffman@25786
   281
lemma contlub_abstraction:
huffman@25786
   282
  "\<lbrakk>chain Y; \<forall>y. cont (\<lambda>x.(c::'a::cpo\<Rightarrow>'b::type\<Rightarrow>'c::cpo) x y)\<rbrakk> \<Longrightarrow>
huffman@25786
   283
    (\<lambda>y. \<Squnion>i. c (Y i) y) = (\<Squnion>i. (\<lambda>y. c (Y i) y))"
huffman@25786
   284
apply (rule thelub_fun [symmetric])
huffman@25786
   285
apply (rule ch2ch_cont)
huffman@25786
   286
apply (simp add: cont2cont_lambda)
huffman@25786
   287
apply assumption
huffman@25786
   288
done
huffman@25786
   289
huffman@25786
   290
lemma mono2mono_app:
huffman@25786
   291
  "\<lbrakk>monofun f; \<forall>x. monofun (f x); monofun t\<rbrakk> \<Longrightarrow> monofun (\<lambda>x. (f x) (t x))"
huffman@25786
   292
apply (rule monofunI)
huffman@25786
   293
apply (simp add: monofun_fun monofunE)
huffman@25786
   294
done
huffman@25786
   295
huffman@25786
   296
lemma cont2contlub_app:
huffman@25786
   297
  "\<lbrakk>cont f; \<forall>x. cont (f x); cont t\<rbrakk> \<Longrightarrow> contlub (\<lambda>x. (f x) (t x))"
huffman@25786
   298
apply (rule contlubI)
huffman@25786
   299
apply (subgoal_tac "chain (\<lambda>i. f (Y i))")
huffman@25786
   300
apply (subgoal_tac "chain (\<lambda>i. t (Y i))")
huffman@25786
   301
apply (simp add: cont2contlubE thelub_fun)
huffman@25786
   302
apply (rule diag_lub)
huffman@25786
   303
apply (erule ch2ch_fun)
huffman@25786
   304
apply (drule spec)
huffman@25786
   305
apply (erule (1) ch2ch_cont)
huffman@25786
   306
apply (erule (1) ch2ch_cont)
huffman@25786
   307
apply (erule (1) ch2ch_cont)
huffman@25786
   308
done
huffman@25786
   309
huffman@25786
   310
lemma cont2cont_app:
huffman@25786
   311
  "\<lbrakk>cont f; \<forall>x. cont (f x); cont t\<rbrakk> \<Longrightarrow> cont (\<lambda>x. (f x) (t x))"
huffman@25786
   312
by (blast intro: monocontlub2cont mono2mono_app cont2mono cont2contlub_app)
huffman@25786
   313
huffman@25786
   314
lemmas cont2cont_app2 = cont2cont_app [rule_format]
huffman@25786
   315
huffman@25786
   316
lemma cont2cont_app3: "\<lbrakk>cont f; cont t\<rbrakk> \<Longrightarrow> cont (\<lambda>x. f (t x))"
huffman@25786
   317
by (rule cont2cont_app2 [OF cont_const])
huffman@25786
   318
huffman@16202
   319
end
huffman@16202
   320