author  huffman 
Thu, 27 Mar 2008 19:49:24 +0100  
changeset 26452  ed657432b8b9 
parent 26028  74668c3a8f70 
child 27413  3154f3765cc7 
permissions  rwrr 
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

1 
(* Title: HOLCF/FunCpo.thy 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

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

3 
Author: Franz Regensburger 
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 
Definition of the partial ordering for the type of all functions => (fun) 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

6 

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

7 
Class instance of => (fun) for class pcpo. 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

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

9 

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

10 
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

11 

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

12 
theory Ffun 
25786  13 
imports Cont 
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

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

15 

18291  16 
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

17 

25758  18 
instantiation "fun" :: (type, sq_ord) sq_ord 
19 
begin 

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

20 

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

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

23 

25758  24 
instance .. 
25 
end 

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

26 

25758  27 
instance "fun" :: (type, po) po 
28 
proof 

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

30 
show "f \<sqsubseteq> f" 

31 
by (simp add: less_fun_def) 

32 
next 

33 
fix f g :: "'a \<Rightarrow> 'b" 

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

35 
by (simp add: less_fun_def expand_fun_eq antisym_less) 

36 
next 

37 
fix f g h :: "'a \<Rightarrow> 'b" 

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

39 
unfolding less_fun_def by (fast elim: trans_less) 

40 
qed 

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

41 

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

42 
text {* make the symbol @{text "<<"} accessible for type fun *} 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

43 

17831  44 
lemma expand_fun_less: "(f \<sqsubseteq> 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

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

46 

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

47 
lemma less_fun_ext: "(\<And>x. f x \<sqsubseteq> g x) \<Longrightarrow> f \<sqsubseteq> g" 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

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

49 

18291  50 
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

51 

25786  52 
text {* function application is monotone *} 
53 

54 
lemma monofun_app: "monofun (\<lambda>f. f x)" 

55 
by (rule monofunI, simp add: less_fun_def) 

56 

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

57 
text {* chains of functions yield chains in the po range *} 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

58 

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

59 
lemma ch2ch_fun: "chain S \<Longrightarrow> chain (\<lambda>i. S i x)" 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

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

61 

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

62 
lemma ch2ch_lambda: "(\<And>x. chain (\<lambda>i. S i x)) \<Longrightarrow> chain S" 
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

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

64 

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

65 
text {* upper bounds of function chains yield upper bound in the po range *} 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

66 

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

67 
lemma ub2ub_fun: 
26028  68 
"range S < u \<Longrightarrow> range (\<lambda>i. S i x) < u x" 
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

69 
by (auto simp add: is_ub_def less_fun_def) 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

70 

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

71 
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

72 

26028  73 
lemma is_lub_lambda: 
74 
assumes f: "\<And>x. range (\<lambda>i. Y i x) << f x" 

75 
shows "range Y << f" 

76 
apply (rule is_lubI) 

77 
apply (rule ub_rangeI) 

78 
apply (rule less_fun_ext) 

79 
apply (rule is_ub_lub [OF f]) 

80 
apply (rule less_fun_ext) 

81 
apply (rule is_lub_lub [OF f]) 

82 
apply (erule ub2ub_fun) 

83 
done 

84 

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

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

86 
"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

87 
\<Longrightarrow> range S << (\<lambda>x. \<Squnion>i. S i x)" 
26028  88 
apply (rule is_lub_lambda) 
89 
apply (rule cpo_lubI) 

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

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

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

92 

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

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

94 
"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

95 
\<Longrightarrow> lub (range S) = (\<lambda>x. \<Squnion>i. S i x)" 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

96 
by (rule lub_fun [THEN thelubI]) 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

97 

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

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

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

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

101 

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

102 
instance "fun" :: (type, cpo) cpo 
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

103 
by intro_classes (rule cpo_fun) 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

104 

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

105 
instance "fun" :: (finite, finite_po) finite_po .. 
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset

106 

26025  107 
instance "fun" :: (type, discrete_cpo) discrete_cpo 
108 
proof 

109 
fix f g :: "'a \<Rightarrow> 'b" 

110 
show "f \<sqsubseteq> g \<longleftrightarrow> f = g" 

111 
unfolding expand_fun_less expand_fun_eq 

112 
by simp 

113 
qed 

114 

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

115 
text {* chainfinite function spaces *} 
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset

116 

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

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

118 
"(\<And>x. max_in_chain n (\<lambda>i. S i x)) \<Longrightarrow> max_in_chain n S" 
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset

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

120 

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

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

122 
"\<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

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

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

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

126 
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

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

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

129 
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

130 
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

131 
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

132 
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

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

134 

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

135 
instance "fun" :: (finite, chfin) chfin 
25921  136 
proof 
25827
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset

137 
fix Y :: "nat \<Rightarrow> 'a \<Rightarrow> 'b" 
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset

138 
let ?n = "\<lambda>x. LEAST n. max_in_chain n (\<lambda>i. Y i x)" 
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset

139 
assume "chain Y" 
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset

140 
hence "\<And>x. chain (\<lambda>i. Y i x)" 
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset

141 
by (rule ch2ch_fun) 
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset

142 
hence "\<And>x. \<exists>n. max_in_chain n (\<lambda>i. Y i x)" 
25921  143 
by (rule chfin) 
25827
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset

144 
hence "\<And>x. max_in_chain (?n x) (\<lambda>i. Y i x)" 
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset

145 
by (rule LeastI_ex) 
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset

146 
hence "\<And>x. max_in_chain (Max (range ?n)) (\<lambda>i. Y i x)" 
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset

147 
by (rule maxinch_mono [OF _ Max_ge], simp_all) 
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset

148 
hence "max_in_chain (Max (range ?n)) Y" 
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset

149 
by (rule maxinch2maxinch_lambda) 
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset

150 
thus "\<exists>n. max_in_chain n Y" .. 
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25786
diff
changeset

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

152 

18291  153 
subsection {* Full function space is pointed *} 
17831  154 

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

156 
by (simp add: less_fun_def) 

157 

25786  158 
lemma least_fun: "\<exists>x::'a::type \<Rightarrow> 'b::pcpo. \<forall>y. x \<sqsubseteq> y" 
17831  159 
apply (rule_tac x = "\<lambda>x. \<bottom>" in exI) 
160 
apply (rule minimal_fun [THEN allI]) 

161 
done 

162 

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

163 
instance "fun" :: (type, pcpo) pcpo 
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

164 
by intro_classes (rule least_fun) 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

165 

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

166 
text {* for compatibility with old HOLCFVersion *} 
17831  167 
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

168 
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

169 

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

170 
text {* function application is strict in the left argument *} 
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset

171 
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

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

173 

25786  174 
text {* 
175 
The following results are about application for functions in @{typ "'a=>'b"} 

176 
*} 

177 

178 
lemma monofun_fun_fun: "f \<sqsubseteq> g \<Longrightarrow> f x \<sqsubseteq> g x" 

179 
by (simp add: less_fun_def) 

180 

181 
lemma monofun_fun_arg: "\<lbrakk>monofun f; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> f x \<sqsubseteq> f y" 

182 
by (rule monofunE) 

183 

184 
lemma monofun_fun: "\<lbrakk>monofun f; monofun g; f \<sqsubseteq> g; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> f x \<sqsubseteq> g y" 

185 
by (rule trans_less [OF monofun_fun_arg monofun_fun_fun]) 

186 

187 
subsection {* Propagation of monotonicity and continuity *} 

188 

189 
text {* the lub of a chain of monotone functions is monotone *} 

190 

191 
lemma monofun_lub_fun: 

192 
"\<lbrakk>chain (F::nat \<Rightarrow> 'a \<Rightarrow> 'b::cpo); \<forall>i. monofun (F i)\<rbrakk> 

193 
\<Longrightarrow> monofun (\<Squnion>i. F i)" 

194 
apply (rule monofunI) 

195 
apply (simp add: thelub_fun) 

25923  196 
apply (rule lub_mono) 
25786  197 
apply (erule ch2ch_fun) 
198 
apply (erule ch2ch_fun) 

199 
apply (simp add: monofunE) 

200 
done 

201 

202 
text {* the lub of a chain of continuous functions is continuous *} 

203 

204 
declare range_composition [simp del] 

205 

206 
lemma contlub_lub_fun: 

207 
"\<lbrakk>chain F; \<forall>i. cont (F i)\<rbrakk> \<Longrightarrow> contlub (\<Squnion>i. F i)" 

208 
apply (rule contlubI) 

209 
apply (simp add: thelub_fun) 

210 
apply (simp add: cont2contlubE) 

211 
apply (rule ex_lub) 

212 
apply (erule ch2ch_fun) 

213 
apply (simp add: ch2ch_cont) 

214 
done 

215 

216 
lemma cont_lub_fun: 

217 
"\<lbrakk>chain F; \<forall>i. cont (F i)\<rbrakk> \<Longrightarrow> cont (\<Squnion>i. F i)" 

218 
apply (rule monocontlub2cont) 

219 
apply (erule monofun_lub_fun) 

220 
apply (simp add: cont2mono) 

221 
apply (erule (1) contlub_lub_fun) 

222 
done 

223 

224 
lemma cont2cont_lub: 

225 
"\<lbrakk>chain F; \<And>i. cont (F i)\<rbrakk> \<Longrightarrow> cont (\<lambda>x. \<Squnion>i. F i x)" 

226 
by (simp add: thelub_fun [symmetric] cont_lub_fun) 

227 

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

229 
apply (rule monofunI) 

230 
apply (erule (1) monofun_fun_arg [THEN monofun_fun_fun]) 

231 
done 

232 

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

234 
apply (rule monocontlub2cont) 

235 
apply (erule cont2mono [THEN mono2mono_fun]) 

236 
apply (rule contlubI) 

237 
apply (simp add: cont2contlubE) 

238 
apply (simp add: thelub_fun ch2ch_cont) 

239 
done 

240 

241 
text {* Note @{text "(\<lambda>x. \<lambda>y. f x y) = f"} *} 

242 

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

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

244 
assumes f: "\<And>y. monofun (\<lambda>x. f x y)" shows "monofun f" 
25786  245 
apply (rule monofunI) 
246 
apply (rule less_fun_ext) 

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

247 
apply (erule monofunE [OF f]) 
25786  248 
done 
249 

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

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

251 
assumes f: "\<And>y. cont (\<lambda>x. f x y)" shows "cont f" 
25786  252 
apply (subgoal_tac "monofun f") 
253 
apply (rule monocontlub2cont) 

254 
apply assumption 

255 
apply (rule contlubI) 

256 
apply (rule ext) 

257 
apply (simp add: thelub_fun ch2ch_monofun) 

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

258 
apply (erule cont2contlubE [OF f]) 
ed657432b8b9
declare cont_lemmas_ext as simp rules individually
huffman
parents:
26028
diff
changeset

259 
apply (simp add: mono2mono_lambda cont2mono f) 
25786  260 
done 
261 

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

263 

264 
lemma contlub_lambda: 

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

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

267 
by (simp add: thelub_fun ch2ch_lambda) 

268 

269 
lemma contlub_abstraction: 

270 
"\<lbrakk>chain Y; \<forall>y. cont (\<lambda>x.(c::'a::cpo\<Rightarrow>'b::type\<Rightarrow>'c::cpo) x y)\<rbrakk> \<Longrightarrow> 

271 
(\<lambda>y. \<Squnion>i. c (Y i) y) = (\<Squnion>i. (\<lambda>y. c (Y i) y))" 

272 
apply (rule thelub_fun [symmetric]) 

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

273 
apply (simp add: ch2ch_cont) 
25786  274 
done 
275 

276 
lemma mono2mono_app: 

277 
"\<lbrakk>monofun f; \<forall>x. monofun (f x); monofun t\<rbrakk> \<Longrightarrow> monofun (\<lambda>x. (f x) (t x))" 

278 
apply (rule monofunI) 

279 
apply (simp add: monofun_fun monofunE) 

280 
done 

281 

282 
lemma cont2contlub_app: 

283 
"\<lbrakk>cont f; \<forall>x. cont (f x); cont t\<rbrakk> \<Longrightarrow> contlub (\<lambda>x. (f x) (t x))" 

284 
apply (rule contlubI) 

285 
apply (subgoal_tac "chain (\<lambda>i. f (Y i))") 

286 
apply (subgoal_tac "chain (\<lambda>i. t (Y i))") 

287 
apply (simp add: cont2contlubE thelub_fun) 

288 
apply (rule diag_lub) 

289 
apply (erule ch2ch_fun) 

290 
apply (drule spec) 

291 
apply (erule (1) ch2ch_cont) 

292 
apply (erule (1) ch2ch_cont) 

293 
apply (erule (1) ch2ch_cont) 

294 
done 

295 

296 
lemma cont2cont_app: 

297 
"\<lbrakk>cont f; \<forall>x. cont (f x); cont t\<rbrakk> \<Longrightarrow> cont (\<lambda>x. (f x) (t x))" 

298 
by (blast intro: monocontlub2cont mono2mono_app cont2mono cont2contlub_app) 

299 

300 
lemmas cont2cont_app2 = cont2cont_app [rule_format] 

301 

302 
lemma cont2cont_app3: "\<lbrakk>cont f; cont t\<rbrakk> \<Longrightarrow> cont (\<lambda>x. f (t x))" 

303 
by (rule cont2cont_app2 [OF cont_const]) 

304 

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

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

306 