added termination lemmas
authornipkow
Tue Feb 08 07:42:08 2011 +0100 (2011-02-08)
changeset 41720f749155883d7
parent 41719 91c2510e19c5
child 41721 eb5900951702
added termination lemmas
src/HOL/Library/While_Combinator.thy
src/HOL/Wellfounded.thy
     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
     2.1 --- a/src/HOL/Wellfounded.thy	Mon Feb 07 15:46:58 2011 +0100
     2.2 +++ b/src/HOL/Wellfounded.thy	Tue Feb 08 07:42:08 2011 +0100
     2.3 @@ -680,6 +680,15 @@
     2.4  apply (rule wf_less_than [THEN wf_inv_image])
     2.5  done
     2.6  
     2.7 +lemma wf_if_measure: fixes f :: "'a \<Rightarrow> nat"
     2.8 +shows "(!!x. P x \<Longrightarrow> f(g x) < f x) \<Longrightarrow> wf {(y,x). P x \<and> y = g x}"
     2.9 +apply(insert wf_measure[of f])
    2.10 +apply(simp only: measure_def inv_image_def less_than_def less_eq)
    2.11 +apply(erule wf_subset)
    2.12 +apply auto
    2.13 +done
    2.14 +
    2.15 +
    2.16  text{* Lexicographic combinations *}
    2.17  
    2.18  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