# HG changeset patch
# User nipkow
# Date 1377681314 -7200
# Node ID 9ddc3bf9f5dfebc187d350674f6fdf7643902d97
# Parent  ad2e09c30aa83ffa00e773abfd5b18815eb2581f# Parent  1a8673a6d6698323f52fe78e098ce1c9b3b086b5
merged

diff -r ad2e09c30aa8 -r 9ddc3bf9f5df src/HOL/Library/While_Combinator.thy
--- a/src/HOL/Library/While_Combinator.thy	Tue Aug 27 16:06:27 2013 +0200
+++ b/src/HOL/Library/While_Combinator.thy	Wed Aug 28 11:15:14 2013 +0200
@@ -242,4 +242,55 @@
   shows "lfp f = while (\<lambda>A. f A \<noteq> A) f {}"
 unfolding while_def using assms by (rule lfp_the_while_option) blast
 
+
+text{* Computing the reflexive, transitive closure by iterating a successor
+function. Stops when an element is found that dos not satisfy the test.
+
+More refined (and hence more efficient) versions can be found in ITP 2011 paper
+by Nipkow (the theories are in the AFP entry Flyspeck by Nipkow)
+and the AFP article Executable Transitive Closures by René Thiemann. *}
+
+definition rtrancl_while :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a list) \<Rightarrow> 'a
+  \<Rightarrow> ('a list * 'a set) option"
+where "rtrancl_while p f x =
+  while_option (%(ws,_). ws \<noteq> [] \<and> p(hd ws))
+    ((%(ws,Z).
+     let x = hd ws; new = filter (\<lambda>y. y \<notin> Z) (f x)
+     in (new @ tl ws, insert x Z)))
+    ([x],{})"
+
+lemma rtrancl_while_Some: assumes "rtrancl_while p f x = Some(ws,Z)"
+shows "if ws = []
+       then Z = {(x,y). y \<in> set(f x)}^* `` {x} \<and> (\<forall>z\<in>Z. p z)
+       else \<not>p(hd ws) \<and> hd ws \<in> {(x,y). y \<in> set(f x)}^* `` {x}"
+proof-
+  let ?test = "(%(ws,_). ws \<noteq> [] \<and> p(hd ws))"
+  let ?step = "(%(ws,Z).
+     let x = hd ws; new = filter (\<lambda>y. y \<notin> Z) (f x)
+     in (new @ tl ws, insert x Z))"
+  let ?R = "{(x,y). y \<in> set(f x)}"
+  let ?Inv = "%(ws,Z). x \<in> set ws \<union> Z \<and> ?R `` Z \<subseteq> set ws \<union> Z \<and>
+                       set ws \<union> Z \<subseteq> ?R^* `` {x} \<and> (\<forall>z\<in>Z. p z)"
+  { fix ws Z assume 1: "?Inv(ws,Z)" and 2: "?test(ws,Z)"
+    from 2 obtain v vs where [simp]: "ws = v#vs" by (auto simp: neq_Nil_conv)
+    have "?Inv(?step (ws,Z))" using 1 2
+      by (auto intro: rtrancl.rtrancl_into_rtrancl)
+  } note inv = this
+  hence "!!p. ?Inv p \<Longrightarrow> ?test p \<Longrightarrow> ?Inv(?step p)"
+    apply(tactic {* split_all_tac @{context} 1 *})
+    using inv by iprover
+  moreover have "?Inv ([x],{})" by (simp)
+  ultimately have I: "?Inv (ws,Z)"
+    by (rule while_option_rule[OF _ assms[unfolded rtrancl_while_def]])
+  { assume "ws = []"
+    hence ?thesis using I
+      by (auto simp del:Image_Collect_split dest: Image_closed_trancl)
+  } moreover
+  { assume "ws \<noteq> []"
+    hence ?thesis using I while_option_stop[OF assms[unfolded rtrancl_while_def]]
+      by (simp add: subset_iff)
+  }
+  ultimately show ?thesis by simp
+qed
+
 end