author | kleing |
Mon, 21 Jun 2004 10:25:57 +0200 | |
changeset 14981 | e73f8140af78 |
parent 14706 | 71590b7733b7 |
child 15131 | c69542757a4d |
permissions | -rw-r--r-- |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
1 |
(* Title: HOL/Library/Continuity.thy |
11355 | 2 |
ID: $Id$ |
3 |
Author: David von Oheimb, TU Muenchen |
|
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
4 |
*) |
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
5 |
|
14706 | 6 |
header {* Continuity and iterations (of set transformers) *} |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
7 |
|
11355 | 8 |
theory Continuity = Main: |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
9 |
|
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
10 |
subsection "Chains" |
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
11 |
|
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
12 |
constdefs |
11355 | 13 |
up_chain :: "(nat => 'a set) => bool" |
14 |
"up_chain F == \<forall>i. F i \<subseteq> F (Suc i)" |
|
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
15 |
|
11355 | 16 |
lemma up_chainI: "(!!i. F i \<subseteq> F (Suc i)) ==> up_chain F" |
17 |
by (simp add: up_chain_def) |
|
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
18 |
|
11355 | 19 |
lemma up_chainD: "up_chain F ==> F i \<subseteq> F (Suc i)" |
20 |
by (simp add: up_chain_def) |
|
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
21 |
|
11355 | 22 |
lemma up_chain_less_mono [rule_format]: |
23 |
"up_chain F ==> x < y --> F x \<subseteq> F y" |
|
24 |
apply (induct_tac y) |
|
25 |
apply (blast dest: up_chainD elim: less_SucE)+ |
|
26 |
done |
|
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
27 |
|
11355 | 28 |
lemma up_chain_mono: "up_chain F ==> x \<le> y ==> F x \<subseteq> F y" |
29 |
apply (drule le_imp_less_or_eq) |
|
30 |
apply (blast dest: up_chain_less_mono) |
|
31 |
done |
|
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
32 |
|
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
33 |
|
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
34 |
constdefs |
11355 | 35 |
down_chain :: "(nat => 'a set) => bool" |
36 |
"down_chain F == \<forall>i. F (Suc i) \<subseteq> F i" |
|
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
37 |
|
11355 | 38 |
lemma down_chainI: "(!!i. F (Suc i) \<subseteq> F i) ==> down_chain F" |
39 |
by (simp add: down_chain_def) |
|
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
40 |
|
11355 | 41 |
lemma down_chainD: "down_chain F ==> F (Suc i) \<subseteq> F i" |
42 |
by (simp add: down_chain_def) |
|
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
43 |
|
11355 | 44 |
lemma down_chain_less_mono [rule_format]: |
45 |
"down_chain F ==> x < y --> F y \<subseteq> F x" |
|
46 |
apply (induct_tac y) |
|
47 |
apply (blast dest: down_chainD elim: less_SucE)+ |
|
48 |
done |
|
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
49 |
|
11355 | 50 |
lemma down_chain_mono: "down_chain F ==> x \<le> y ==> F y \<subseteq> F x" |
51 |
apply (drule le_imp_less_or_eq) |
|
52 |
apply (blast dest: down_chain_less_mono) |
|
53 |
done |
|
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
54 |
|
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
55 |
|
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
56 |
subsection "Continuity" |
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
57 |
|
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
58 |
constdefs |
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
59 |
up_cont :: "('a set => 'a set) => bool" |
11355 | 60 |
"up_cont f == \<forall>F. up_chain F --> f (\<Union>(range F)) = \<Union>(f ` range F)" |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
61 |
|
11355 | 62 |
lemma up_contI: |
63 |
"(!!F. up_chain F ==> f (\<Union>(range F)) = \<Union>(f ` range F)) ==> up_cont f" |
|
64 |
apply (unfold up_cont_def) |
|
65 |
apply blast |
|
66 |
done |
|
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
67 |
|
11355 | 68 |
lemma up_contD: |
69 |
"up_cont f ==> up_chain F ==> f (\<Union>(range F)) = \<Union>(f ` range F)" |
|
70 |
apply (unfold up_cont_def) |
|
71 |
apply auto |
|
72 |
done |
|
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
73 |
|
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
74 |
|
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
75 |
lemma up_cont_mono: "up_cont f ==> mono f" |
11355 | 76 |
apply (rule monoI) |
77 |
apply (drule_tac F = "\<lambda>i. if i = 0 then A else B" in up_contD) |
|
78 |
apply (rule up_chainI) |
|
79 |
apply simp+ |
|
80 |
apply (drule Un_absorb1) |
|
11461 | 81 |
apply (auto simp add: nat_not_singleton) |
11355 | 82 |
done |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
83 |
|
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
84 |
|
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
85 |
constdefs |
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
86 |
down_cont :: "('a set => 'a set) => bool" |
11355 | 87 |
"down_cont f == |
88 |
\<forall>F. down_chain F --> f (Inter (range F)) = Inter (f ` range F)" |
|
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
89 |
|
11355 | 90 |
lemma down_contI: |
91 |
"(!!F. down_chain F ==> f (Inter (range F)) = Inter (f ` range F)) ==> |
|
92 |
down_cont f" |
|
93 |
apply (unfold down_cont_def) |
|
94 |
apply blast |
|
95 |
done |
|
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
96 |
|
11355 | 97 |
lemma down_contD: "down_cont f ==> down_chain F ==> |
98 |
f (Inter (range F)) = Inter (f ` range F)" |
|
99 |
apply (unfold down_cont_def) |
|
100 |
apply auto |
|
101 |
done |
|
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
102 |
|
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
103 |
lemma down_cont_mono: "down_cont f ==> mono f" |
11355 | 104 |
apply (rule monoI) |
105 |
apply (drule_tac F = "\<lambda>i. if i = 0 then B else A" in down_contD) |
|
106 |
apply (rule down_chainI) |
|
107 |
apply simp+ |
|
108 |
apply (drule Int_absorb1) |
|
11461 | 109 |
apply (auto simp add: nat_not_singleton) |
11355 | 110 |
done |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
111 |
|
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
112 |
|
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
113 |
subsection "Iteration" |
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
114 |
|
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
115 |
constdefs |
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
116 |
up_iterate :: "('a set => 'a set) => nat => 'a set" |
11355 | 117 |
"up_iterate f n == (f^n) {}" |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
118 |
|
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
119 |
lemma up_iterate_0 [simp]: "up_iterate f 0 = {}" |
11355 | 120 |
by (simp add: up_iterate_def) |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
121 |
|
11355 | 122 |
lemma up_iterate_Suc [simp]: "up_iterate f (Suc i) = f (up_iterate f i)" |
123 |
by (simp add: up_iterate_def) |
|
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
124 |
|
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
125 |
lemma up_iterate_chain: "mono F ==> up_chain (up_iterate F)" |
11355 | 126 |
apply (rule up_chainI) |
127 |
apply (induct_tac i) |
|
128 |
apply simp+ |
|
129 |
apply (erule (1) monoD) |
|
130 |
done |
|
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
131 |
|
11355 | 132 |
lemma UNION_up_iterate_is_fp: |
133 |
"up_cont F ==> |
|
134 |
F (UNION UNIV (up_iterate F)) = UNION UNIV (up_iterate F)" |
|
135 |
apply (frule up_cont_mono [THEN up_iterate_chain]) |
|
136 |
apply (drule (1) up_contD) |
|
137 |
apply simp |
|
138 |
apply (auto simp del: up_iterate_Suc simp add: up_iterate_Suc [symmetric]) |
|
139 |
apply (case_tac xa) |
|
140 |
apply auto |
|
141 |
done |
|
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
142 |
|
11355 | 143 |
lemma UNION_up_iterate_lowerbound: |
144 |
"mono F ==> F P = P ==> UNION UNIV (up_iterate F) \<subseteq> P" |
|
145 |
apply (subgoal_tac "(!!i. up_iterate F i \<subseteq> P)") |
|
146 |
apply fast |
|
147 |
apply (induct_tac i) |
|
148 |
prefer 2 apply (drule (1) monoD) |
|
149 |
apply auto |
|
150 |
done |
|
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
151 |
|
11355 | 152 |
lemma UNION_up_iterate_is_lfp: |
153 |
"up_cont F ==> lfp F = UNION UNIV (up_iterate F)" |
|
154 |
apply (rule set_eq_subset [THEN iffD2]) |
|
155 |
apply (rule conjI) |
|
156 |
prefer 2 |
|
157 |
apply (drule up_cont_mono) |
|
158 |
apply (rule UNION_up_iterate_lowerbound) |
|
159 |
apply assumption |
|
160 |
apply (erule lfp_unfold [symmetric]) |
|
161 |
apply (rule lfp_lowerbound) |
|
162 |
apply (rule set_eq_subset [THEN iffD1, THEN conjunct2]) |
|
163 |
apply (erule UNION_up_iterate_is_fp [symmetric]) |
|
164 |
done |
|
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
165 |
|
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
166 |
|
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
167 |
constdefs |
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
168 |
down_iterate :: "('a set => 'a set) => nat => 'a set" |
11355 | 169 |
"down_iterate f n == (f^n) UNIV" |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
170 |
|
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
171 |
lemma down_iterate_0 [simp]: "down_iterate f 0 = UNIV" |
11355 | 172 |
by (simp add: down_iterate_def) |
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
173 |
|
11355 | 174 |
lemma down_iterate_Suc [simp]: |
175 |
"down_iterate f (Suc i) = f (down_iterate f i)" |
|
176 |
by (simp add: down_iterate_def) |
|
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
177 |
|
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
178 |
lemma down_iterate_chain: "mono F ==> down_chain (down_iterate F)" |
11355 | 179 |
apply (rule down_chainI) |
180 |
apply (induct_tac i) |
|
181 |
apply simp+ |
|
182 |
apply (erule (1) monoD) |
|
183 |
done |
|
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
184 |
|
11355 | 185 |
lemma INTER_down_iterate_is_fp: |
186 |
"down_cont F ==> |
|
187 |
F (INTER UNIV (down_iterate F)) = INTER UNIV (down_iterate F)" |
|
188 |
apply (frule down_cont_mono [THEN down_iterate_chain]) |
|
189 |
apply (drule (1) down_contD) |
|
190 |
apply simp |
|
191 |
apply (auto simp del: down_iterate_Suc simp add: down_iterate_Suc [symmetric]) |
|
192 |
apply (case_tac xa) |
|
193 |
apply auto |
|
194 |
done |
|
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
195 |
|
11355 | 196 |
lemma INTER_down_iterate_upperbound: |
197 |
"mono F ==> F P = P ==> P \<subseteq> INTER UNIV (down_iterate F)" |
|
198 |
apply (subgoal_tac "(!!i. P \<subseteq> down_iterate F i)") |
|
199 |
apply fast |
|
200 |
apply (induct_tac i) |
|
201 |
prefer 2 apply (drule (1) monoD) |
|
202 |
apply auto |
|
203 |
done |
|
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
204 |
|
11355 | 205 |
lemma INTER_down_iterate_is_gfp: |
206 |
"down_cont F ==> gfp F = INTER UNIV (down_iterate F)" |
|
207 |
apply (rule set_eq_subset [THEN iffD2]) |
|
208 |
apply (rule conjI) |
|
209 |
apply (drule down_cont_mono) |
|
210 |
apply (rule INTER_down_iterate_upperbound) |
|
211 |
apply assumption |
|
212 |
apply (erule gfp_unfold [symmetric]) |
|
213 |
apply (rule gfp_upperbound) |
|
214 |
apply (rule set_eq_subset [THEN iffD1, THEN conjunct2]) |
|
215 |
apply (erule INTER_down_iterate_is_fp) |
|
216 |
done |
|
11351
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
217 |
|
c5c403d30c77
added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents:
diff
changeset
|
218 |
end |