author | wenzelm |
Thu, 03 Jan 2008 23:01:51 +0100 | |
changeset 25821 | 2e565f8275f5 |
parent 25786 | 6b3c79acac1f |
child 25827 | c2adeb1bae5c |
permissions | -rw-r--r-- |
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 |
|
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
66 |
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
|
67 |
|
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
68 |
lemma ub2ub_fun: |
25786 | 69 |
"range (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::po) <| 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
|
70 |
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
|
71 |
|
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
72 |
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
|
73 |
|
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
74 |
lemma lub_fun: |
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) |
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
76 |
\<Longrightarrow> 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
|
77 |
apply (rule is_lubI) |
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
78 |
apply (rule ub_rangeI) |
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
79 |
apply (rule less_fun_ext) |
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
80 |
apply (rule is_ub_thelub) |
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
81 |
apply (erule ch2ch_fun) |
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
82 |
apply (rule less_fun_ext) |
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
83 |
apply (rule is_lub_thelub) |
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
84 |
apply (erule ch2ch_fun) |
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
85 |
apply (erule ub2ub_fun) |
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
86 |
done |
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
87 |
|
25786 | 88 |
lemma lub_fun': |
89 |
fixes S :: "('a::type \<Rightarrow> 'b::dcpo) set" |
|
90 |
assumes S: "directed S" |
|
91 |
shows "S <<| (\<lambda>x. \<Squnion>f\<in>S. f x)" |
|
92 |
apply (rule is_lubI) |
|
93 |
apply (rule is_ubI) |
|
94 |
apply (rule less_fun_ext) |
|
95 |
apply (rule is_ub_thelub') |
|
96 |
apply (rule dir2dir_monofun [OF monofun_app S]) |
|
97 |
apply (erule imageI) |
|
98 |
apply (rule less_fun_ext) |
|
99 |
apply (rule is_lub_thelub') |
|
100 |
apply (rule dir2dir_monofun [OF monofun_app S]) |
|
101 |
apply (erule ub2ub_monofun' [OF monofun_app]) |
|
102 |
done |
|
103 |
||
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
104 |
lemma thelub_fun: |
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
105 |
"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
|
106 |
\<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
|
107 |
by (rule lub_fun [THEN thelubI]) |
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
108 |
|
25786 | 109 |
lemma thelub_fun': |
110 |
"directed (S::('a::type \<Rightarrow> 'b::dcpo) set) |
|
111 |
\<Longrightarrow> lub S = (\<lambda>x. \<Squnion>f\<in>S. f x)" |
|
112 |
by (rule lub_fun' [THEN thelubI]) |
|
113 |
||
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
114 |
lemma cpo_fun: |
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
115 |
"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
|
116 |
by (rule exI, erule lub_fun) |
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
117 |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
18291
diff
changeset
|
118 |
instance "fun" :: (type, cpo) cpo |
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
119 |
by intro_classes (rule cpo_fun) |
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
120 |
|
25786 | 121 |
lemma dcpo_fun: |
122 |
"directed (S::('a::type \<Rightarrow> 'b::dcpo) set) \<Longrightarrow> \<exists>x. S <<| x" |
|
123 |
by (rule exI, erule lub_fun') |
|
124 |
||
125 |
instance "fun" :: (type, dcpo) dcpo |
|
126 |
by intro_classes (rule dcpo_fun) |
|
127 |
||
18291 | 128 |
subsection {* Full function space is pointed *} |
17831 | 129 |
|
130 |
lemma minimal_fun: "(\<lambda>x. \<bottom>) \<sqsubseteq> f" |
|
131 |
by (simp add: less_fun_def) |
|
132 |
||
25786 | 133 |
lemma least_fun: "\<exists>x::'a::type \<Rightarrow> 'b::pcpo. \<forall>y. x \<sqsubseteq> y" |
17831 | 134 |
apply (rule_tac x = "\<lambda>x. \<bottom>" in exI) |
135 |
apply (rule minimal_fun [THEN allI]) |
|
136 |
done |
|
137 |
||
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
18291
diff
changeset
|
138 |
instance "fun" :: (type, pcpo) pcpo |
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
139 |
by intro_classes (rule least_fun) |
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
140 |
|
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
141 |
text {* for compatibility with old HOLCF-Version *} |
17831 | 142 |
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
|
143 |
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
|
144 |
|
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
145 |
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
|
146 |
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
|
147 |
by (simp add: inst_fun_pcpo) |
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
148 |
|
25786 | 149 |
text {* |
150 |
The following results are about application for functions in @{typ "'a=>'b"} |
|
151 |
*} |
|
152 |
||
153 |
lemma monofun_fun_fun: "f \<sqsubseteq> g \<Longrightarrow> f x \<sqsubseteq> g x" |
|
154 |
by (simp add: less_fun_def) |
|
155 |
||
156 |
lemma monofun_fun_arg: "\<lbrakk>monofun f; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> f x \<sqsubseteq> f y" |
|
157 |
by (rule monofunE) |
|
158 |
||
159 |
lemma monofun_fun: "\<lbrakk>monofun f; monofun g; f \<sqsubseteq> g; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> f x \<sqsubseteq> g y" |
|
160 |
by (rule trans_less [OF monofun_fun_arg monofun_fun_fun]) |
|
161 |
||
162 |
subsection {* Propagation of monotonicity and continuity *} |
|
163 |
||
164 |
text {* the lub of a chain of monotone functions is monotone *} |
|
165 |
||
166 |
lemma monofun_lub_fun: |
|
167 |
"\<lbrakk>chain (F::nat \<Rightarrow> 'a \<Rightarrow> 'b::cpo); \<forall>i. monofun (F i)\<rbrakk> |
|
168 |
\<Longrightarrow> monofun (\<Squnion>i. F i)" |
|
169 |
apply (rule monofunI) |
|
170 |
apply (simp add: thelub_fun) |
|
171 |
apply (rule lub_mono [rule_format]) |
|
172 |
apply (erule ch2ch_fun) |
|
173 |
apply (erule ch2ch_fun) |
|
174 |
apply (simp add: monofunE) |
|
175 |
done |
|
176 |
||
177 |
text {* the lub of a chain of continuous functions is continuous *} |
|
178 |
||
179 |
declare range_composition [simp del] |
|
180 |
||
181 |
lemma contlub_lub_fun: |
|
182 |
"\<lbrakk>chain F; \<forall>i. cont (F i)\<rbrakk> \<Longrightarrow> contlub (\<Squnion>i. F i)" |
|
183 |
apply (rule contlubI) |
|
184 |
apply (simp add: thelub_fun) |
|
185 |
apply (simp add: cont2contlubE) |
|
186 |
apply (rule ex_lub) |
|
187 |
apply (erule ch2ch_fun) |
|
188 |
apply (simp add: ch2ch_cont) |
|
189 |
done |
|
190 |
||
191 |
lemma cont_lub_fun: |
|
192 |
"\<lbrakk>chain F; \<forall>i. cont (F i)\<rbrakk> \<Longrightarrow> cont (\<Squnion>i. F i)" |
|
193 |
apply (rule monocontlub2cont) |
|
194 |
apply (erule monofun_lub_fun) |
|
195 |
apply (simp add: cont2mono) |
|
196 |
apply (erule (1) contlub_lub_fun) |
|
197 |
done |
|
198 |
||
199 |
lemma cont2cont_lub: |
|
200 |
"\<lbrakk>chain F; \<And>i. cont (F i)\<rbrakk> \<Longrightarrow> cont (\<lambda>x. \<Squnion>i. F i x)" |
|
201 |
by (simp add: thelub_fun [symmetric] cont_lub_fun) |
|
202 |
||
203 |
lemma mono2mono_fun: "monofun f \<Longrightarrow> monofun (\<lambda>x. f x y)" |
|
204 |
apply (rule monofunI) |
|
205 |
apply (erule (1) monofun_fun_arg [THEN monofun_fun_fun]) |
|
206 |
done |
|
207 |
||
208 |
lemma cont2cont_fun: "cont f \<Longrightarrow> cont (\<lambda>x. f x y)" |
|
209 |
apply (rule monocontlub2cont) |
|
210 |
apply (erule cont2mono [THEN mono2mono_fun]) |
|
211 |
apply (rule contlubI) |
|
212 |
apply (simp add: cont2contlubE) |
|
213 |
apply (simp add: thelub_fun ch2ch_cont) |
|
214 |
done |
|
215 |
||
216 |
text {* Note @{text "(\<lambda>x. \<lambda>y. f x y) = f"} *} |
|
217 |
||
218 |
lemma mono2mono_lambda: "(\<And>y. monofun (\<lambda>x. f x y)) \<Longrightarrow> monofun f" |
|
219 |
apply (rule monofunI) |
|
220 |
apply (rule less_fun_ext) |
|
221 |
apply (blast dest: monofunE) |
|
222 |
done |
|
223 |
||
224 |
lemma cont2cont_lambda: "(\<And>y. cont (\<lambda>x. f x y)) \<Longrightarrow> cont f" |
|
225 |
apply (subgoal_tac "monofun f") |
|
226 |
apply (rule monocontlub2cont) |
|
227 |
apply assumption |
|
228 |
apply (rule contlubI) |
|
229 |
apply (rule ext) |
|
230 |
apply (simp add: thelub_fun ch2ch_monofun) |
|
231 |
apply (blast dest: cont2contlubE) |
|
232 |
apply (simp add: mono2mono_lambda cont2mono) |
|
233 |
done |
|
234 |
||
235 |
text {* What D.A.Schmidt calls continuity of abstraction; never used here *} |
|
236 |
||
237 |
lemma contlub_lambda: |
|
238 |
"(\<And>x::'a::type. chain (\<lambda>i. S i x::'b::cpo)) |
|
239 |
\<Longrightarrow> (\<lambda>x. \<Squnion>i. S i x) = (\<Squnion>i. (\<lambda>x. S i x))" |
|
240 |
by (simp add: thelub_fun ch2ch_lambda) |
|
241 |
||
242 |
lemma contlub_abstraction: |
|
243 |
"\<lbrakk>chain Y; \<forall>y. cont (\<lambda>x.(c::'a::cpo\<Rightarrow>'b::type\<Rightarrow>'c::cpo) x y)\<rbrakk> \<Longrightarrow> |
|
244 |
(\<lambda>y. \<Squnion>i. c (Y i) y) = (\<Squnion>i. (\<lambda>y. c (Y i) y))" |
|
245 |
apply (rule thelub_fun [symmetric]) |
|
246 |
apply (rule ch2ch_cont) |
|
247 |
apply (simp add: cont2cont_lambda) |
|
248 |
apply assumption |
|
249 |
done |
|
250 |
||
251 |
lemma mono2mono_app: |
|
252 |
"\<lbrakk>monofun f; \<forall>x. monofun (f x); monofun t\<rbrakk> \<Longrightarrow> monofun (\<lambda>x. (f x) (t x))" |
|
253 |
apply (rule monofunI) |
|
254 |
apply (simp add: monofun_fun monofunE) |
|
255 |
done |
|
256 |
||
257 |
lemma cont2contlub_app: |
|
258 |
"\<lbrakk>cont f; \<forall>x. cont (f x); cont t\<rbrakk> \<Longrightarrow> contlub (\<lambda>x. (f x) (t x))" |
|
259 |
apply (rule contlubI) |
|
260 |
apply (subgoal_tac "chain (\<lambda>i. f (Y i))") |
|
261 |
apply (subgoal_tac "chain (\<lambda>i. t (Y i))") |
|
262 |
apply (simp add: cont2contlubE thelub_fun) |
|
263 |
apply (rule diag_lub) |
|
264 |
apply (erule ch2ch_fun) |
|
265 |
apply (drule spec) |
|
266 |
apply (erule (1) ch2ch_cont) |
|
267 |
apply (erule (1) ch2ch_cont) |
|
268 |
apply (erule (1) ch2ch_cont) |
|
269 |
done |
|
270 |
||
271 |
lemma cont2cont_app: |
|
272 |
"\<lbrakk>cont f; \<forall>x. cont (f x); cont t\<rbrakk> \<Longrightarrow> cont (\<lambda>x. (f x) (t x))" |
|
273 |
by (blast intro: monocontlub2cont mono2mono_app cont2mono cont2contlub_app) |
|
274 |
||
275 |
lemmas cont2cont_app2 = cont2cont_app [rule_format] |
|
276 |
||
277 |
lemma cont2cont_app3: "\<lbrakk>cont f; cont t\<rbrakk> \<Longrightarrow> cont (\<lambda>x. f (t x))" |
|
278 |
by (rule cont2cont_app2 [OF cont_const]) |
|
279 |
||
16202
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
280 |
end |
61811f31ce5a
renamed FunCpo theory to Ffun; added theorems ch2ch_fun_rev and app_strict
huffman
parents:
diff
changeset
|
281 |