240 lemma lfp_while: |
240 lemma lfp_while: |
241 assumes "mono f" and "!!X. X \<subseteq> C \<Longrightarrow> f X \<subseteq> C" and "finite C" |
241 assumes "mono f" and "!!X. X \<subseteq> C \<Longrightarrow> f X \<subseteq> C" and "finite C" |
242 shows "lfp f = while (\<lambda>A. f A \<noteq> A) f {}" |
242 shows "lfp f = while (\<lambda>A. f A \<noteq> A) f {}" |
243 unfolding while_def using assms by (rule lfp_the_while_option) blast |
243 unfolding while_def using assms by (rule lfp_the_while_option) blast |
244 |
244 |
|
245 |
|
246 text{* Computing the reflexive, transitive closure by iterating a successor |
|
247 function. Stops when an element is found that dos not satisfy the test. |
|
248 |
|
249 More refined (and hence more efficient) versions can be found in ITP 2011 paper |
|
250 by Nipkow (the theories are in the AFP entry Flyspeck by Nipkow) |
|
251 and the AFP article Executable Transitive Closures by René Thiemann. *} |
|
252 |
|
253 definition rtrancl_while :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a list) \<Rightarrow> 'a |
|
254 \<Rightarrow> ('a list * 'a set) option" |
|
255 where "rtrancl_while p f x = |
|
256 while_option (%(ws,_). ws \<noteq> [] \<and> p(hd ws)) |
|
257 ((%(ws,Z). |
|
258 let x = hd ws; new = filter (\<lambda>y. y \<notin> Z) (f x) |
|
259 in (new @ tl ws, insert x Z))) |
|
260 ([x],{})" |
|
261 |
|
262 lemma rtrancl_while_Some: assumes "rtrancl_while p f x = Some(ws,Z)" |
|
263 shows "if ws = [] |
|
264 then Z = {(x,y). y \<in> set(f x)}^* `` {x} \<and> (\<forall>z\<in>Z. p z) |
|
265 else \<not>p(hd ws) \<and> hd ws \<in> {(x,y). y \<in> set(f x)}^* `` {x}" |
|
266 proof- |
|
267 let ?test = "(%(ws,_). ws \<noteq> [] \<and> p(hd ws))" |
|
268 let ?step = "(%(ws,Z). |
|
269 let x = hd ws; new = filter (\<lambda>y. y \<notin> Z) (f x) |
|
270 in (new @ tl ws, insert x Z))" |
|
271 let ?R = "{(x,y). y \<in> set(f x)}" |
|
272 let ?Inv = "%(ws,Z). x \<in> set ws \<union> Z \<and> ?R `` Z \<subseteq> set ws \<union> Z \<and> |
|
273 set ws \<union> Z \<subseteq> ?R^* `` {x} \<and> (\<forall>z\<in>Z. p z)" |
|
274 { fix ws Z assume 1: "?Inv(ws,Z)" and 2: "?test(ws,Z)" |
|
275 from 2 obtain v vs where [simp]: "ws = v#vs" by (auto simp: neq_Nil_conv) |
|
276 have "?Inv(?step (ws,Z))" using 1 2 |
|
277 by (auto intro: rtrancl.rtrancl_into_rtrancl) |
|
278 } note inv = this |
|
279 hence "!!p. ?Inv p \<Longrightarrow> ?test p \<Longrightarrow> ?Inv(?step p)" |
|
280 apply(tactic {* split_all_tac @{context} 1 *}) |
|
281 using inv by iprover |
|
282 moreover have "?Inv ([x],{})" by (simp) |
|
283 ultimately have I: "?Inv (ws,Z)" |
|
284 by (rule while_option_rule[OF _ assms[unfolded rtrancl_while_def]]) |
|
285 { assume "ws = []" |
|
286 hence ?thesis using I |
|
287 by (auto simp del:Image_Collect_split dest: Image_closed_trancl) |
|
288 } moreover |
|
289 { assume "ws \<noteq> []" |
|
290 hence ?thesis using I while_option_stop[OF assms[unfolded rtrancl_while_def]] |
|
291 by (simp add: subset_iff) |
|
292 } |
|
293 ultimately show ?thesis by simp |
|
294 qed |
|
295 |
245 end |
296 end |