src/HOLCF/Fun_Cpo.thy
author huffman
Wed Oct 13 10:56:42 2010 -0700 (2010-10-13)
changeset 40011 b974cf829099
parent 40006 116e94f9543b
child 40089 8adc57fb8454
permissions -rw-r--r--
cleaned up Fun_Cpo.thy; deprecated a few theorem names
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@40011
     9
imports Adm
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@40002
    38
lemma fun_below_iff: "f \<sqsubseteq> g \<longleftrightarrow> (\<forall>x. f x \<sqsubseteq> g x)"
huffman@31076
    39
by (simp add: below_fun_def)
huffman@16202
    40
huffman@40002
    41
lemma fun_belowI: "(\<And>x. f x \<sqsubseteq> g x) \<Longrightarrow> f \<sqsubseteq> g"
huffman@31076
    42
by (simp add: below_fun_def)
huffman@16202
    43
huffman@40011
    44
lemma fun_belowD: "f \<sqsubseteq> g \<Longrightarrow> f x \<sqsubseteq> g x"
huffman@40011
    45
by (simp add: below_fun_def)
huffman@40011
    46
huffman@18291
    47
subsection {* Full function space is chain complete *}
huffman@16202
    48
huffman@40011
    49
text {* Function application is monotone. *}
huffman@25786
    50
huffman@25786
    51
lemma monofun_app: "monofun (\<lambda>f. f x)"
huffman@31076
    52
by (rule monofunI, simp add: below_fun_def)
huffman@25786
    53
huffman@40011
    54
text {* Properties of chains of functions. *}
huffman@40011
    55
huffman@40011
    56
lemma fun_chain_iff: "chain S \<longleftrightarrow> (\<forall>x. chain (\<lambda>i. S i x))"
huffman@40011
    57
unfolding chain_def fun_below_iff by auto
huffman@16202
    58
huffman@16202
    59
lemma ch2ch_fun: "chain S \<Longrightarrow> chain (\<lambda>i. S i x)"
huffman@31076
    60
by (simp add: chain_def below_fun_def)
huffman@16202
    61
huffman@18092
    62
lemma ch2ch_lambda: "(\<And>x. chain (\<lambda>i. S i x)) \<Longrightarrow> chain S"
huffman@31076
    63
by (simp add: chain_def below_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@26028
    68
  "range S <| u \<Longrightarrow> range (\<lambda>i. S i x) <| u x"
huffman@31076
    69
by (auto simp add: is_ub_def below_fun_def)
huffman@16202
    70
huffman@16202
    71
text {* Type @{typ "'a::type => 'b::cpo"} is chain complete *}
huffman@16202
    72
huffman@26028
    73
lemma is_lub_lambda:
huffman@40011
    74
  "(\<And>x. range (\<lambda>i. Y i x) <<| f x) \<Longrightarrow> range Y <<| f"
huffman@40011
    75
unfolding is_lub_def is_ub_def below_fun_def by simp
huffman@26028
    76
huffman@16202
    77
lemma lub_fun:
huffman@16202
    78
  "chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo)
huffman@16202
    79
    \<Longrightarrow> range S <<| (\<lambda>x. \<Squnion>i. S i x)"
huffman@26028
    80
apply (rule is_lub_lambda)
huffman@26028
    81
apply (rule cpo_lubI)
huffman@16202
    82
apply (erule ch2ch_fun)
huffman@16202
    83
done
huffman@16202
    84
huffman@16202
    85
lemma thelub_fun:
huffman@16202
    86
  "chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo)
huffman@27413
    87
    \<Longrightarrow> (\<Squnion>i. S i) = (\<lambda>x. \<Squnion>i. S i x)"
huffman@16202
    88
by (rule lub_fun [THEN thelubI])
huffman@16202
    89
krauss@20523
    90
instance "fun"  :: (type, cpo) cpo
huffman@40006
    91
by intro_classes (rule exI, erule lub_fun)
huffman@16202
    92
huffman@40011
    93
subsection {* Chain-finiteness of function space *}
huffman@25827
    94
huffman@25827
    95
lemma maxinch2maxinch_lambda:
huffman@25827
    96
  "(\<And>x. max_in_chain n (\<lambda>i. S i x)) \<Longrightarrow> max_in_chain n S"
nipkow@39302
    97
unfolding max_in_chain_def fun_eq_iff by simp
huffman@25827
    98
huffman@25827
    99
lemma maxinch_mono:
huffman@25827
   100
  "\<lbrakk>max_in_chain i Y; i \<le> j\<rbrakk> \<Longrightarrow> max_in_chain j Y"
huffman@25827
   101
unfolding max_in_chain_def
huffman@25827
   102
proof (intro allI impI)
huffman@25827
   103
  fix k
huffman@25827
   104
  assume Y: "\<forall>n\<ge>i. Y i = Y n"
huffman@25827
   105
  assume ij: "i \<le> j"
huffman@25827
   106
  assume jk: "j \<le> k"
huffman@25827
   107
  from ij jk have ik: "i \<le> k" by simp
huffman@25827
   108
  from Y ij have Yij: "Y i = Y j" by simp
huffman@25827
   109
  from Y ik have Yik: "Y i = Y k" by simp
huffman@25827
   110
  from Yij Yik show "Y j = Y k" by auto
huffman@25827
   111
qed
huffman@25827
   112
huffman@25827
   113
instance "fun" :: (finite, chfin) chfin
huffman@25921
   114
proof
huffman@25827
   115
  fix Y :: "nat \<Rightarrow> 'a \<Rightarrow> 'b"
huffman@25827
   116
  let ?n = "\<lambda>x. LEAST n. max_in_chain n (\<lambda>i. Y i x)"
huffman@25827
   117
  assume "chain Y"
huffman@25827
   118
  hence "\<And>x. chain (\<lambda>i. Y i x)"
huffman@25827
   119
    by (rule ch2ch_fun)
huffman@25827
   120
  hence "\<And>x. \<exists>n. max_in_chain n (\<lambda>i. Y i x)"
huffman@25921
   121
    by (rule chfin)
huffman@25827
   122
  hence "\<And>x. max_in_chain (?n x) (\<lambda>i. Y i x)"
huffman@25827
   123
    by (rule LeastI_ex)
huffman@25827
   124
  hence "\<And>x. max_in_chain (Max (range ?n)) (\<lambda>i. Y i x)"
huffman@25827
   125
    by (rule maxinch_mono [OF _ Max_ge], simp_all)
huffman@25827
   126
  hence "max_in_chain (Max (range ?n)) Y"
huffman@25827
   127
    by (rule maxinch2maxinch_lambda)
huffman@25827
   128
  thus "\<exists>n. max_in_chain n Y" ..
huffman@25827
   129
qed
huffman@25827
   130
huffman@40011
   131
instance "fun" :: (finite, finite_po) finite_po ..
huffman@40011
   132
huffman@40011
   133
instance "fun" :: (type, discrete_cpo) discrete_cpo
huffman@40011
   134
proof
huffman@40011
   135
  fix f g :: "'a \<Rightarrow> 'b"
huffman@40011
   136
  show "f \<sqsubseteq> g \<longleftrightarrow> f = g" 
huffman@40011
   137
    unfolding fun_below_iff fun_eq_iff
huffman@40011
   138
    by simp
huffman@40011
   139
qed
huffman@40011
   140
huffman@18291
   141
subsection {* Full function space is pointed *}
huffman@17831
   142
huffman@17831
   143
lemma minimal_fun: "(\<lambda>x. \<bottom>) \<sqsubseteq> f"
huffman@31076
   144
by (simp add: below_fun_def)
huffman@17831
   145
huffman@40011
   146
instance "fun"  :: (type, pcpo) pcpo
huffman@40011
   147
by default (fast intro: minimal_fun)
huffman@17831
   148
huffman@17831
   149
lemma inst_fun_pcpo: "\<bottom> = (\<lambda>x. \<bottom>)"
huffman@16202
   150
by (rule minimal_fun [THEN UU_I, symmetric])
huffman@16202
   151
huffman@16202
   152
lemma app_strict [simp]: "\<bottom> x = \<bottom>"
huffman@16202
   153
by (simp add: inst_fun_pcpo)
huffman@16202
   154
huffman@40011
   155
lemma lambda_strict: "(\<lambda>x. \<bottom>) = \<bottom>"
huffman@40011
   156
by (rule UU_I, rule minimal_fun)
huffman@25786
   157
huffman@25786
   158
subsection {* Propagation of monotonicity and continuity *}
huffman@25786
   159
huffman@40011
   160
text {* The lub of a chain of monotone functions is monotone. *}
huffman@40011
   161
huffman@40011
   162
lemma adm_monofun: "adm monofun"
huffman@40011
   163
by (rule admI, simp add: thelub_fun fun_chain_iff monofun_def lub_mono)
huffman@25786
   164
huffman@40011
   165
text {* The lub of a chain of continuous functions is continuous. *}
huffman@25786
   166
huffman@40011
   167
lemma adm_cont: "adm cont"
huffman@40011
   168
by (rule admI, simp add: thelub_fun fun_chain_iff)
huffman@25786
   169
huffman@40011
   170
text {* Function application preserves monotonicity and continuity. *}
huffman@25786
   171
huffman@25786
   172
lemma mono2mono_fun: "monofun f \<Longrightarrow> monofun (\<lambda>x. f x y)"
huffman@40011
   173
by (simp add: monofun_def fun_below_iff)
huffman@25786
   174
huffman@25786
   175
lemma cont2cont_fun: "cont f \<Longrightarrow> cont (\<lambda>x. f x y)"
huffman@35914
   176
apply (rule contI2)
huffman@25786
   177
apply (erule cont2mono [THEN mono2mono_fun])
huffman@40011
   178
apply (simp add: cont2contlubE thelub_fun ch2ch_cont)
huffman@25786
   179
done
huffman@25786
   180
huffman@40011
   181
text {*
huffman@40011
   182
  Lambda abstraction preserves monotonicity and continuity.
huffman@40011
   183
  (Note @{text "(\<lambda>x. \<lambda>y. f x y) = f"}.)
huffman@40011
   184
*}
huffman@25786
   185
huffman@26452
   186
lemma mono2mono_lambda:
huffman@26452
   187
  assumes f: "\<And>y. monofun (\<lambda>x. f x y)" shows "monofun f"
huffman@40011
   188
using f by (simp add: monofun_def fun_below_iff)
huffman@25786
   189
huffman@26452
   190
lemma cont2cont_lambda [simp]:
huffman@26452
   191
  assumes f: "\<And>y. cont (\<lambda>x. f x y)" shows "cont f"
huffman@40011
   192
by (rule contI, rule is_lub_lambda, rule contE [OF f])
huffman@25786
   193
huffman@25786
   194
text {* What D.A.Schmidt calls continuity of abstraction; never used here *}
huffman@25786
   195
huffman@25786
   196
lemma contlub_lambda:
huffman@25786
   197
  "(\<And>x::'a::type. chain (\<lambda>i. S i x::'b::cpo))
huffman@25786
   198
    \<Longrightarrow> (\<lambda>x. \<Squnion>i. S i x) = (\<Squnion>i. (\<lambda>x. S i x))"
huffman@25786
   199
by (simp add: thelub_fun ch2ch_lambda)
huffman@25786
   200
huffman@16202
   201
end