# HG changeset patch
# User nipkow
# Date 1297704516 -3600
# Node ID 5268aef2fe83da7359ce7ce12230ebf33cb5ca69
# Parent  8ce56536fda76d36d4d1af8f32373c1be6955c60
generalized termination lemmas

diff -r 8ce56536fda7 -r 5268aef2fe83 src/HOL/Library/While_Combinator.thy
--- a/src/HOL/Library/While_Combinator.thy	Mon Feb 14 15:27:23 2011 +0100
+++ b/src/HOL/Library/While_Combinator.thy	Mon Feb 14 18:28:36 2011 +0100
@@ -130,18 +130,19 @@
 text{* Proving termination: *}
 
 theorem wf_while_option_Some:
-  assumes wf: "wf {(t, s). b s \<and> t = c s}"
+  assumes "wf {(t, s). (P s \<and> b s) \<and> t = c s}"
+  and "!!s. P s \<Longrightarrow> b s \<Longrightarrow> P(c s)" and "P s"
   shows "EX t. while_option b c s = Some t"
-using wf
+using assms(1,3)
 apply (induct s)
-apply simp
+using assms(2)
 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])
-
+shows "(!!s. P s \<Longrightarrow> b s \<Longrightarrow> P(c s) \<and> f(c s) < f s)
+  \<Longrightarrow> P s \<Longrightarrow> EX t. while_option b c s = Some t"
+by(blast intro: wf_while_option_Some[OF wf_if_measure, of P b f])
 
 end