# HG changeset patch
# User traytel
# Date 1382601800 -7200
# Node ID 0c188a3c671a598d25e1b85373a8e1aed2d04ebc
# Parent  1e685123926d8be15a3b1e11fde6552854dfdd93
refactored rtrancl_while; prove termination for finite rtrancl

diff -r 1e685123926d -r 0c188a3c671a src/HOL/Library/While_Combinator.thy
--- a/src/HOL/Library/While_Combinator.thy	Wed Oct 23 21:12:20 2013 +0200
+++ b/src/HOL/Library/While_Combinator.thy	Thu Oct 24 10:03:20 2013 +0200
@@ -307,37 +307,44 @@
 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, set new \<union> Z)))
-    ([x],{x})"
+context
+fixes p :: "'a \<Rightarrow> bool"
+and f :: "'a \<Rightarrow> 'a list"
+and x :: 'a
+begin
+
+fun rtrancl_while_test :: "'a list \<times> 'a set \<Rightarrow> bool"
+where "rtrancl_while_test (ws,_) = (ws \<noteq> [] \<and> p(hd ws))"
+
+fun rtrancl_while_step :: "'a list \<times> 'a set \<Rightarrow> 'a list \<times> 'a set"
+where "rtrancl_while_step (ws, Z) =
+  (let x = hd ws; new = remdups (filter (\<lambda>y. y \<notin> Z) (f x))
+  in (new @ tl ws, set new \<union> Z))"
 
-lemma rtrancl_while_Some: assumes "rtrancl_while p f x = Some(ws,Z)"
+definition rtrancl_while :: "('a list * 'a set) option"
+where "rtrancl_while = while_option rtrancl_while_test rtrancl_while_step ([x],{x})"
+
+fun rtrancl_while_invariant :: "'a list \<times> 'a set \<Rightarrow> bool"
+where "rtrancl_while_invariant (ws, Z) =
+   (x \<in> Z \<and> set ws \<subseteq> Z \<and> distinct ws \<and> {(x,y). y \<in> set(f x)} `` (Z - set ws) \<subseteq> Z \<and>
+    Z \<subseteq> {(x,y). y \<in> set(f x)}^* `` {x} \<and> (\<forall>z\<in>Z - set ws. p z))"
+
+lemma rtrancl_while_invariant: 
+  assumes inv: "rtrancl_while_invariant st" and test: "rtrancl_while_test st"
+  shows   "rtrancl_while_invariant (rtrancl_while_step st)"
+proof (cases st)
+  fix ws Z assume st: "st = (ws, Z)"
+  with test obtain h t where "ws = h # t" "p h" by (cases ws) auto
+  with inv st show ?thesis by (auto intro: rtrancl.rtrancl_into_rtrancl)
+qed
+
+lemma rtrancl_while_Some: assumes "rtrancl_while = 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, set new \<union> Z))"
-  let ?R = "{(x,y). y \<in> set(f x)}"
-  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
-      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],{x})" by (simp)
-  ultimately have I: "?Inv (ws,Z)"
+proof -
+  have "rtrancl_while_invariant ([x],{x})" by simp
+  with rtrancl_while_invariant have I: "rtrancl_while_invariant (ws,Z)"
     by (rule while_option_rule[OF _ assms[unfolded rtrancl_while_def]])
   { assume "ws = []"
     hence ?thesis using I
@@ -350,4 +357,41 @@
   ultimately show ?thesis by simp
 qed
 
+lemma rtrancl_while_finite_Some:
+  assumes "finite ({(x, y). y \<in> set (f x)}\<^sup>* `` {x})" (is "finite ?Cl")
+  shows "\<exists>y. rtrancl_while = Some y"
+proof -
+  let ?R = "(\<lambda>(_, Z). card (?Cl - Z)) <*mlex*> (\<lambda>(ws, _). length ws) <*mlex*> {}"
+  have "wf ?R" by (blast intro: wf_mlex)
+  then show ?thesis unfolding rtrancl_while_def
+  proof (rule wf_rel_while_option_Some[of ?R rtrancl_while_invariant])
+    fix st assume *: "rtrancl_while_invariant st \<and> rtrancl_while_test st"
+    hence I: "rtrancl_while_invariant (rtrancl_while_step st)"
+      by (blast intro: rtrancl_while_invariant)
+    show "(rtrancl_while_step st, st) \<in> ?R"
+    proof (cases st)
+      fix ws Z let ?ws = "fst (rtrancl_while_step st)" and ?Z = "snd (rtrancl_while_step st)"
+      assume st: "st = (ws, Z)"
+      with * obtain h t where ws: "ws = h # t" "p h" by (cases ws) auto
+      { assume "remdups (filter (\<lambda>y. y \<notin> Z) (f h)) \<noteq> []"
+        then obtain z where "z \<in> set (remdups (filter (\<lambda>y. y \<notin> Z) (f h)))" by fastforce
+        with st ws I have "Z \<subset> ?Z" "Z \<subseteq> ?Cl" "?Z \<subseteq> ?Cl" by auto
+        with assms have "card (?Cl - ?Z) < card (?Cl - Z)" by (blast intro: psubset_card_mono)
+        with st ws have ?thesis unfolding mlex_prod_def by simp
+      }
+      moreover
+      { assume "remdups (filter (\<lambda>y. y \<notin> Z) (f h)) = []"
+        with st ws have "?Z = Z" "?ws = t"  by (auto simp: filter_empty_conv)
+        with st ws have ?thesis unfolding mlex_prod_def by simp
+      }
+      ultimately show ?thesis by blast
+    qed
+  qed (simp_all add: rtrancl_while_invariant)
+qed
+
 end
+
+hide_const (open) rtrancl_while_test rtrancl_while_step rtrancl_while_invariant
+hide_fact (open) rtrancl_while_invariant
+
+end