# HG changeset patch
# User nipkow
# Date 1377702688 -7200
# Node ID daa550823c9f562eac0807ecbd04755ee6353e9b
# Parent  ca237b9e4542ad77a6dd2e74fcaf43cbde07f917
tuned

diff -r ca237b9e4542 -r daa550823c9f src/HOL/Library/While_Combinator.thy
--- a/src/HOL/Library/While_Combinator.thy	Wed Aug 28 14:37:35 2013 +0200
+++ b/src/HOL/Library/While_Combinator.thy	Wed Aug 28 17:11:28 2013 +0200
@@ -256,8 +256,8 @@
   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],{})"
+     in (new @ tl ws, set new \<union> insert x Z)))
+    ([x],{x})"
 
 lemma rtrancl_while_Some: assumes "rtrancl_while p f x = Some(ws,Z)"
 shows "if ws = []
@@ -267,10 +267,10 @@
   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))"
+     in (new @ tl ws, set new \<union> 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)"
+  let ?Inv = "%(ws,Z). x \<in> Z \<and> set ws \<subseteq> Z \<and> ?R `` (Z - set ws) \<subseteq> Z \<and>
+                       Z \<subseteq> ?R^* `` {x} \<and> (\<forall>z\<in>Z - set ws. 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
@@ -279,7 +279,7 @@
   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)
+  moreover have "?Inv ([x],{x})" by (simp)
   ultimately have I: "?Inv (ws,Z)"
     by (rule while_option_rule[OF _ assms[unfolded rtrancl_while_def]])
   { assume "ws = []"