--- 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