# HG changeset patch
# User nipkow
# Date 1297147328 -3600
# Node ID f749155883d79e73592ebc1672c961eb3723ff60
# Parent  91c2510e19c5263d4480fb42d963f75bd354b8df
added termination lemmas

diff -r 91c2510e19c5 -r f749155883d7 src/HOL/Library/While_Combinator.thy
--- 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
diff -r 91c2510e19c5 -r f749155883d7 src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Mon Feb 07 15:46:58 2011 +0100
+++ b/src/HOL/Wellfounded.thy	Tue Feb 08 07:42:08 2011 +0100
@@ -680,6 +680,15 @@
 apply (rule wf_less_than [THEN wf_inv_image])
 done
 
+lemma wf_if_measure: fixes f :: "'a \<Rightarrow> nat"
+shows "(!!x. P x \<Longrightarrow> f(g x) < f x) \<Longrightarrow> wf {(y,x). P x \<and> y = g x}"
+apply(insert wf_measure[of f])
+apply(simp only: measure_def inv_image_def less_than_def less_eq)
+apply(erule wf_subset)
+apply auto
+done
+
+
 text{* Lexicographic combinations *}
 
 definition lex_prod :: "('a \<times>'a) set \<Rightarrow> ('b \<times> 'b) set \<Rightarrow> (('a \<times> 'b) \<times> ('a \<times> 'b)) set" (infixr "<*lex*>" 80) where