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