author  huffman 
Mon, 06 Dec 2010 10:08:33 0800  
changeset 41030  ff7d177128ef 
parent 40774  0437dbc127b3 
child 41032  75b4ff66781c 
permissions  rwrr 
40001  1 
(* Title: HOLCF/Fun_Cpo.thy 
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

2 
Author: Franz Regensburger 
40001  3 
Author: Brian Huffman 
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

4 
*) 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

5 

61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

6 
header {* Class instances for the full function space *} 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

7 

40001  8 
theory Fun_Cpo 
40011
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset

9 
imports Adm 
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

10 
begin 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

11 

18291  12 
subsection {* Full function space is a partial order *} 
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

13 

31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
29138
diff
changeset

14 
instantiation "fun" :: (type, below) below 
25758  15 
begin 
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

16 

25758  17 
definition 
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
29138
diff
changeset

18 
below_fun_def: "(op \<sqsubseteq>) \<equiv> (\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x)" 
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

19 

25758  20 
instance .. 
21 
end 

16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

22 

25758  23 
instance "fun" :: (type, po) po 
24 
proof 

25 
fix f :: "'a \<Rightarrow> 'b" 

26 
show "f \<sqsubseteq> f" 

31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
29138
diff
changeset

27 
by (simp add: below_fun_def) 
25758  28 
next 
29 
fix f g :: "'a \<Rightarrow> 'b" 

30 
assume "f \<sqsubseteq> g" and "g \<sqsubseteq> f" thus "f = g" 

39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39199
diff
changeset

31 
by (simp add: below_fun_def fun_eq_iff below_antisym) 
25758  32 
next 
33 
fix f g h :: "'a \<Rightarrow> 'b" 

34 
assume "f \<sqsubseteq> g" and "g \<sqsubseteq> h" thus "f \<sqsubseteq> h" 

31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
29138
diff
changeset

35 
unfolding below_fun_def by (fast elim: below_trans) 
25758  36 
qed 
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

37 

40002
c5b5f7a3a3b1
new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI
huffman
parents:
40001
diff
changeset

38 
lemma fun_below_iff: "f \<sqsubseteq> g \<longleftrightarrow> (\<forall>x. f x \<sqsubseteq> g x)" 
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
29138
diff
changeset

39 
by (simp add: below_fun_def) 
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

40 

40002
c5b5f7a3a3b1
new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI
huffman
parents:
40001
diff
changeset

41 
lemma fun_belowI: "(\<And>x. f x \<sqsubseteq> g x) \<Longrightarrow> f \<sqsubseteq> g" 
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
29138
diff
changeset

42 
by (simp add: below_fun_def) 
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

43 

40011
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset

44 
lemma fun_belowD: "f \<sqsubseteq> g \<Longrightarrow> f x \<sqsubseteq> g x" 
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset

45 
by (simp add: below_fun_def) 
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset

46 

18291  47 
subsection {* Full function space is chain complete *} 
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

48 

40011
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset

49 
text {* Properties of chains of functions. *} 
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset

50 

b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset

51 
lemma fun_chain_iff: "chain S \<longleftrightarrow> (\<forall>x. chain (\<lambda>i. S i x))" 
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset

52 
unfolding chain_def fun_below_iff by auto 
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

53 

61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

54 
lemma ch2ch_fun: "chain S \<Longrightarrow> chain (\<lambda>i. S i x)" 
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
29138
diff
changeset

55 
by (simp add: chain_def below_fun_def) 
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

56 

18092
2c5d5da79a1e
renamed and added ch2ch, cont2cont, mono2mono theorems ending in _fun, _lambda, _LAM
huffman
parents:
17831
diff
changeset

57 
lemma ch2ch_lambda: "(\<And>x. chain (\<lambda>i. S i x)) \<Longrightarrow> chain S" 
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
29138
diff
changeset

58 
by (simp add: chain_def below_fun_def) 
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

59 

61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

60 
text {* Type @{typ "'a::type => 'b::cpo"} is chain complete *} 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

61 

26028  62 
lemma is_lub_lambda: 
40011
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset

63 
"(\<And>x. range (\<lambda>i. Y i x) << f x) \<Longrightarrow> range Y << f" 
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset

64 
unfolding is_lub_def is_ub_def below_fun_def by simp 
26028  65 

41030
ff7d177128ef
rename lub_fun > is_lub_fun, thelub_fun > lub_fun
huffman
parents:
40774
diff
changeset

66 
lemma is_lub_fun: 
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

67 
"chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo) 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

68 
\<Longrightarrow> range S << (\<lambda>x. \<Squnion>i. S i x)" 
26028  69 
apply (rule is_lub_lambda) 
70 
apply (rule cpo_lubI) 

16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

71 
apply (erule ch2ch_fun) 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

72 
done 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

73 

41030
ff7d177128ef
rename lub_fun > is_lub_fun, thelub_fun > lub_fun
huffman
parents:
40774
diff
changeset

74 
lemma lub_fun: 
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

75 
"chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo) 
27413  76 
\<Longrightarrow> (\<Squnion>i. S i) = (\<lambda>x. \<Squnion>i. S i x)" 
41030
ff7d177128ef
rename lub_fun > is_lub_fun, thelub_fun > lub_fun
huffman
parents:
40774
diff
changeset

77 
by (rule is_lub_fun [THEN lub_eqI]) 
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

78 

20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
18291
diff
changeset

79 
instance "fun" :: (type, cpo) cpo 
41030
ff7d177128ef
rename lub_fun > is_lub_fun, thelub_fun > lub_fun
huffman
parents:
40774
diff
changeset

80 
by intro_classes (rule exI, erule is_lub_fun) 
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

81 

40011
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset

82 
subsection {* Chainfiniteness of function space *} 
25827
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset

83 

c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset

84 
lemma maxinch2maxinch_lambda: 
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset

85 
"(\<And>x. max_in_chain n (\<lambda>i. S i x)) \<Longrightarrow> max_in_chain n S" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39199
diff
changeset

86 
unfolding max_in_chain_def fun_eq_iff by simp 
25827
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset

87 

c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset

88 
lemma maxinch_mono: 
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset

89 
"\<lbrakk>max_in_chain i Y; i \<le> j\<rbrakk> \<Longrightarrow> max_in_chain j Y" 
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset

90 
unfolding max_in_chain_def 
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset

91 
proof (intro allI impI) 
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset

92 
fix k 
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset

93 
assume Y: "\<forall>n\<ge>i. Y i = Y n" 
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset

94 
assume ij: "i \<le> j" 
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset

95 
assume jk: "j \<le> k" 
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset

96 
from ij jk have ik: "i \<le> k" by simp 
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset

97 
from Y ij have Yij: "Y i = Y j" by simp 
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset

98 
from Y ik have Yik: "Y i = Y k" by simp 
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset

99 
from Yij Yik show "Y j = Y k" by auto 
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset

100 
qed 
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset

101 

40011
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset

102 
instance "fun" :: (type, discrete_cpo) discrete_cpo 
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset

103 
proof 
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset

104 
fix f g :: "'a \<Rightarrow> 'b" 
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset

105 
show "f \<sqsubseteq> g \<longleftrightarrow> f = g" 
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset

106 
unfolding fun_below_iff fun_eq_iff 
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset

107 
by simp 
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset

108 
qed 
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset

109 

18291  110 
subsection {* Full function space is pointed *} 
17831  111 

112 
lemma minimal_fun: "(\<lambda>x. \<bottom>) \<sqsubseteq> f" 

31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
29138
diff
changeset

113 
by (simp add: below_fun_def) 
17831  114 

40011
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset

115 
instance "fun" :: (type, pcpo) pcpo 
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset

116 
by default (fast intro: minimal_fun) 
17831  117 

118 
lemma inst_fun_pcpo: "\<bottom> = (\<lambda>x. \<bottom>)" 

16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

119 
by (rule minimal_fun [THEN UU_I, symmetric]) 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

120 

61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

121 
lemma app_strict [simp]: "\<bottom> x = \<bottom>" 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

122 
by (simp add: inst_fun_pcpo) 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

123 

40011
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset

124 
lemma lambda_strict: "(\<lambda>x. \<bottom>) = \<bottom>" 
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset

125 
by (rule UU_I, rule minimal_fun) 
25786  126 

127 
subsection {* Propagation of monotonicity and continuity *} 

128 

40011
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset

129 
text {* The lub of a chain of monotone functions is monotone. *} 
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset

130 

b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset

131 
lemma adm_monofun: "adm monofun" 
41030
ff7d177128ef
rename lub_fun > is_lub_fun, thelub_fun > lub_fun
huffman
parents:
40774
diff
changeset

132 
by (rule admI, simp add: lub_fun fun_chain_iff monofun_def lub_mono) 
25786  133 

40011
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset

134 
text {* The lub of a chain of continuous functions is continuous. *} 
25786  135 

40011
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset

136 
lemma adm_cont: "adm cont" 
41030
ff7d177128ef
rename lub_fun > is_lub_fun, thelub_fun > lub_fun
huffman
parents:
40774
diff
changeset

137 
by (rule admI, simp add: lub_fun fun_chain_iff) 
25786  138 

40011
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset

139 
text {* Function application preserves monotonicity and continuity. *} 
25786  140 

141 
lemma mono2mono_fun: "monofun f \<Longrightarrow> monofun (\<lambda>x. f x y)" 

40011
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset

142 
by (simp add: monofun_def fun_below_iff) 
25786  143 

144 
lemma cont2cont_fun: "cont f \<Longrightarrow> cont (\<lambda>x. f x y)" 

35914  145 
apply (rule contI2) 
25786  146 
apply (erule cont2mono [THEN mono2mono_fun]) 
41030
ff7d177128ef
rename lub_fun > is_lub_fun, thelub_fun > lub_fun
huffman
parents:
40774
diff
changeset

147 
apply (simp add: cont2contlubE lub_fun ch2ch_cont) 
25786  148 
done 
149 

40622
e40e9e9769f4
add lemma cont_fun; remove unused lemma monofun_app
huffman
parents:
40091
diff
changeset

150 
lemma cont_fun: "cont (\<lambda>f. f x)" 
e40e9e9769f4
add lemma cont_fun; remove unused lemma monofun_app
huffman
parents:
40091
diff
changeset

151 
using cont_id by (rule cont2cont_fun) 
e40e9e9769f4
add lemma cont_fun; remove unused lemma monofun_app
huffman
parents:
40091
diff
changeset

152 

40011
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset

153 
text {* 
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset

154 
Lambda abstraction preserves monotonicity and continuity. 
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset

155 
(Note @{text "(\<lambda>x. \<lambda>y. f x y) = f"}.) 
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset

156 
*} 
25786  157 

26452
ed657432b8b9
declare cont_lemmas_ext as simp rules individually
huffman
parents:
26028
diff
changeset

158 
lemma mono2mono_lambda: 
ed657432b8b9
declare cont_lemmas_ext as simp rules individually
huffman
parents:
26028
diff
changeset

159 
assumes f: "\<And>y. monofun (\<lambda>x. f x y)" shows "monofun f" 
40011
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset

160 
using f by (simp add: monofun_def fun_below_iff) 
25786  161 

26452
ed657432b8b9
declare cont_lemmas_ext as simp rules individually
huffman
parents:
26028
diff
changeset

162 
lemma cont2cont_lambda [simp]: 
ed657432b8b9
declare cont_lemmas_ext as simp rules individually
huffman
parents:
26028
diff
changeset

163 
assumes f: "\<And>y. cont (\<lambda>x. f x y)" shows "cont f" 
40011
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40006
diff
changeset

164 
by (rule contI, rule is_lub_lambda, rule contE [OF f]) 
25786  165 

166 
text {* What D.A.Schmidt calls continuity of abstraction; never used here *} 

167 

168 
lemma contlub_lambda: 

169 
"(\<And>x::'a::type. chain (\<lambda>i. S i x::'b::cpo)) 

170 
\<Longrightarrow> (\<lambda>x. \<Squnion>i. S i x) = (\<Squnion>i. (\<lambda>x. S i x))" 

41030
ff7d177128ef
rename lub_fun > is_lub_fun, thelub_fun > lub_fun
huffman
parents:
40774
diff
changeset

171 
by (simp add: lub_fun ch2ch_lambda) 
25786  172 

16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

173 
end 