src/HOL/Wellfounded.thy
changeset 32244 a99723d77ae0
parent 32235 8f9b8d14fc9f
child 32263 8bc0fd4a23a0
     1.1 --- a/src/HOL/Wellfounded.thy	Tue Jul 28 08:48:48 2009 +0200
     1.2 +++ b/src/HOL/Wellfounded.thy	Tue Jul 28 08:48:56 2009 +0200
     1.3 @@ -886,30 +886,6 @@
     1.4    qed
     1.5  qed
     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  
    1.32  subsection{*Weakly decreasing sequences (w.r.t. some well-founded order) 
    1.33     stabilize.*}