1.1 --- a/src/HOL/Recdef.thy	Tue Jul 28 08:48:48 2009 +0200
     1.2 +++ b/src/HOL/Recdef.thy	Tue Jul 28 08:48:56 2009 +0200
     1.3 @@ -79,6 +79,32 @@
     1.4  use "Tools/recdef.ML"
     1.5  setup Recdef.setup
     1.6  
     1.7 +text {*Wellfoundedness of @{text same_fst}*}
     1.8 +
     1.9 +definition
    1.10 + same_fst :: "('a => bool) => ('a => ('b * 'b)set) => (('a*'b)*('a*'b))set"
    1.11 +where
    1.12 +    "same_fst P R == {((x',y'),(x,y)) . x'=x & P x & (y',y) : R x}"
    1.13 +   --{*For @{text rec_def} declarations where the first n parameters
    1.14 +       stay unchanged in the recursive call. *}
    1.15 +
    1.16 +lemma same_fstI [intro!]:
    1.17 +     "[| P x; (y',y) : R x |] ==> ((x,y'),(x,y)) : same_fst P R"
    1.18 +by (simp add: same_fst_def)
    1.19 +
    1.20 +lemma wf_same_fst:
    1.21 +  assumes prem: "(!!x. P x ==> wf(R x))"
    1.22 +  shows "wf(same_fst P R)"
    1.23 +apply (simp cong del: imp_cong add: wf_def same_fst_def)
    1.24 +apply (intro strip)
    1.25 +apply (rename_tac a b)
    1.26 +apply (case_tac "wf (R a)")
    1.27 + apply (erule_tac a = b in wf_induct, blast)
    1.28 +apply (blast intro: prem)
    1.29 +done
    1.30 +
    1.31 +text {*Rule setup*}
    1.32 +
    1.33  lemmas [recdef_simp] =
    1.34    inv_image_def
    1.35    measure_def