# HG changeset patch
# User krauss
# Date 1221659963 -7200
# Node ID 703046c93ffef4ff4b297aaa47b420f421becce3
# Parent  5b2af04ec9fb016227a3c5dd3a546e0a65b89736
wf_finite_psubset[simp], in_finite_psubset[simp]

diff -r 5b2af04ec9fb -r 703046c93ffe src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Wed Sep 17 15:21:30 2008 +0200
+++ b/src/HOL/Wellfounded.thy	Wed Sep 17 15:59:23 2008 +0200
@@ -756,7 +756,7 @@
 definition finite_psubset  :: "('a set * 'a set) set"
 where "finite_psubset == {(A,B). A < B & finite B}"
 
-lemma wf_finite_psubset: "wf(finite_psubset)"
+lemma wf_finite_psubset[simp]: "wf(finite_psubset)"
 apply (unfold finite_psubset_def)
 apply (rule wf_measure [THEN wf_subset])
 apply (simp add: measure_def inv_image_def less_than_def less_eq)
@@ -766,7 +766,8 @@
 lemma trans_finite_psubset: "trans finite_psubset"
 by (simp add: finite_psubset_def less_le trans_def, blast)
 
-
+lemma in_finite_psubset[simp]: "(A, B) \<in> finite_psubset = (A < B & finite B)"
+unfolding finite_psubset_def by auto
 
 
 text {*Wellfoundedness of @{text same_fst}*}