src/HOL/Library/While_Combinator.thy
changeset 53217 1a8673a6d669
parent 50577 cfbad2d08412
child 53220 daa550823c9f
     1.1 --- a/src/HOL/Library/While_Combinator.thy	Mon Aug 26 23:39:53 2013 +0200
     1.2 +++ b/src/HOL/Library/While_Combinator.thy	Wed Aug 28 08:56:57 2013 +0200
     1.3 @@ -242,4 +242,55 @@
     1.4    shows "lfp f = while (\<lambda>A. f A \<noteq> A) f {}"
     1.5  unfolding while_def using assms by (rule lfp_the_while_option) blast
     1.6  
     1.7 +
     1.8 +text{* Computing the reflexive, transitive closure by iterating a successor
     1.9 +function. Stops when an element is found that dos not satisfy the test.
    1.10 +
    1.11 +More refined (and hence more efficient) versions can be found in ITP 2011 paper
    1.12 +by Nipkow (the theories are in the AFP entry Flyspeck by Nipkow)
    1.13 +and the AFP article Executable Transitive Closures by René Thiemann. *}
    1.14 +
    1.15 +definition rtrancl_while :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a list) \<Rightarrow> 'a
    1.16 +  \<Rightarrow> ('a list * 'a set) option"
    1.17 +where "rtrancl_while p f x =
    1.18 +  while_option (%(ws,_). ws \<noteq> [] \<and> p(hd ws))
    1.19 +    ((%(ws,Z).
    1.20 +     let x = hd ws; new = filter (\<lambda>y. y \<notin> Z) (f x)
    1.21 +     in (new @ tl ws, insert x Z)))
    1.22 +    ([x],{})"
    1.23 +
    1.24 +lemma rtrancl_while_Some: assumes "rtrancl_while p f x = Some(ws,Z)"
    1.25 +shows "if ws = []
    1.26 +       then Z = {(x,y). y \<in> set(f x)}^* `` {x} \<and> (\<forall>z\<in>Z. p z)
    1.27 +       else \<not>p(hd ws) \<and> hd ws \<in> {(x,y). y \<in> set(f x)}^* `` {x}"
    1.28 +proof-
    1.29 +  let ?test = "(%(ws,_). ws \<noteq> [] \<and> p(hd ws))"
    1.30 +  let ?step = "(%(ws,Z).
    1.31 +     let x = hd ws; new = filter (\<lambda>y. y \<notin> Z) (f x)
    1.32 +     in (new @ tl ws, insert x Z))"
    1.33 +  let ?R = "{(x,y). y \<in> set(f x)}"
    1.34 +  let ?Inv = "%(ws,Z). x \<in> set ws \<union> Z \<and> ?R `` Z \<subseteq> set ws \<union> Z \<and>
    1.35 +                       set ws \<union> Z \<subseteq> ?R^* `` {x} \<and> (\<forall>z\<in>Z. p z)"
    1.36 +  { fix ws Z assume 1: "?Inv(ws,Z)" and 2: "?test(ws,Z)"
    1.37 +    from 2 obtain v vs where [simp]: "ws = v#vs" by (auto simp: neq_Nil_conv)
    1.38 +    have "?Inv(?step (ws,Z))" using 1 2
    1.39 +      by (auto intro: rtrancl.rtrancl_into_rtrancl)
    1.40 +  } note inv = this
    1.41 +  hence "!!p. ?Inv p \<Longrightarrow> ?test p \<Longrightarrow> ?Inv(?step p)"
    1.42 +    apply(tactic {* split_all_tac @{context} 1 *})
    1.43 +    using inv by iprover
    1.44 +  moreover have "?Inv ([x],{})" by (simp)
    1.45 +  ultimately have I: "?Inv (ws,Z)"
    1.46 +    by (rule while_option_rule[OF _ assms[unfolded rtrancl_while_def]])
    1.47 +  { assume "ws = []"
    1.48 +    hence ?thesis using I
    1.49 +      by (auto simp del:Image_Collect_split dest: Image_closed_trancl)
    1.50 +  } moreover
    1.51 +  { assume "ws \<noteq> []"
    1.52 +    hence ?thesis using I while_option_stop[OF assms[unfolded rtrancl_while_def]]
    1.53 +      by (simp add: subset_iff)
    1.54 +  }
    1.55 +  ultimately show ?thesis by simp
    1.56 +qed
    1.57 +
    1.58  end