src/HOL/Wellfounded.thy
changeset 28260 703046c93ffe
parent 27823 52971512d1a2
child 28524 644b62cf678f
     1.1 --- a/src/HOL/Wellfounded.thy	Wed Sep 17 15:21:30 2008 +0200
     1.2 +++ b/src/HOL/Wellfounded.thy	Wed Sep 17 15:59:23 2008 +0200
     1.3 @@ -756,7 +756,7 @@
     1.4  definition finite_psubset  :: "('a set * 'a set) set"
     1.5  where "finite_psubset == {(A,B). A < B & finite B}"
     1.6  
     1.7 -lemma wf_finite_psubset: "wf(finite_psubset)"
     1.8 +lemma wf_finite_psubset[simp]: "wf(finite_psubset)"
     1.9  apply (unfold finite_psubset_def)
    1.10  apply (rule wf_measure [THEN wf_subset])
    1.11  apply (simp add: measure_def inv_image_def less_than_def less_eq)
    1.12 @@ -766,7 +766,8 @@
    1.13  lemma trans_finite_psubset: "trans finite_psubset"
    1.14  by (simp add: finite_psubset_def less_le trans_def, blast)
    1.15  
    1.16 -
    1.17 +lemma in_finite_psubset[simp]: "(A, B) \<in> finite_psubset = (A < B & finite B)"
    1.18 +unfolding finite_psubset_def by auto
    1.19  
    1.20  
    1.21  text {*Wellfoundedness of @{text same_fst}*}