src/HOL/Library/While_Combinator.thy
changeset 41720 f749155883d7
parent 37760 8380686be5cd
child 41764 5268aef2fe83
     1.1 --- a/src/HOL/Library/While_Combinator.thy	Mon Feb 07 15:46:58 2011 +0100
     1.2 +++ b/src/HOL/Library/While_Combinator.thy	Tue Feb 08 07:42:08 2011 +0100
     1.3 @@ -127,5 +127,21 @@
     1.4    apply blast
     1.5    done
     1.6  
     1.7 +text{* Proving termination: *}
     1.8 +
     1.9 +theorem wf_while_option_Some:
    1.10 +  assumes wf: "wf {(t, s). b s \<and> t = c s}"
    1.11 +  shows "EX t. while_option b c s = Some t"
    1.12 +using wf
    1.13 +apply (induct s)
    1.14 +apply simp
    1.15 +apply (subst while_option_unfold)
    1.16 +apply simp
    1.17 +done
    1.18 +
    1.19 +theorem measure_while_option_Some: fixes f :: "'s \<Rightarrow> nat"
    1.20 +shows "(!!s. b s \<Longrightarrow> f(c s) < f s) \<Longrightarrow> EX t. while_option b c s = Some t"
    1.21 +by(erule wf_while_option_Some[OF wf_if_measure])
    1.22 +
    1.23  
    1.24  end