--- a/src/HOL/Library/While_Combinator.thy Mon Feb 07 15:46:58 2011 +0100
+++ b/src/HOL/Library/While_Combinator.thy Tue Feb 08 07:42:08 2011 +0100
@@ -127,5 +127,21 @@
apply blast
done
+text{* Proving termination: *}
+
+theorem wf_while_option_Some:
+ assumes wf: "wf {(t, s). b s \<and> t = c s}"
+ shows "EX t. while_option b c s = Some t"
+using wf
+apply (induct s)
+apply simp
+apply (subst while_option_unfold)
+apply simp
+done
+
+theorem measure_while_option_Some: fixes f :: "'s \<Rightarrow> nat"
+shows "(!!s. b s \<Longrightarrow> f(c s) < f s) \<Longrightarrow> EX t. while_option b c s = Some t"
+by(erule wf_while_option_Some[OF wf_if_measure])
+
end