# HG changeset patch
# User nipkow
# Date 1314350567 -7200
# Node ID 5e580115dfcd1f2e83e38af2cce98d267b690392
# Parent  e08158671ef4b8668cf73dec6cffb0f282e23757
added lemma

diff -r e08158671ef4 -r 5e580115dfcd src/HOL/List.thy
--- a/src/HOL/List.thy	Fri Aug 26 01:18:48 2011 +0200
+++ b/src/HOL/List.thy	Fri Aug 26 11:22:47 2011 +0200
@@ -4703,7 +4703,7 @@
 qed
 
 
-text{* Accessible part of @{term listrel1} relations: *}
+text{* Accessible part and wellfoundedness: *}
 
 lemma Cons_acc_listrel1I [intro!]:
   "x \<in> acc r \<Longrightarrow> xs \<in> acc (listrel1 r) \<Longrightarrow> (x # xs) \<in> acc (listrel1 r)"
@@ -4729,6 +4729,9 @@
 apply (fastsimp dest!: in_set_conv_decomp[THEN iffD1] simp: listrel1_def)
 done
 
+lemma wf_listrel1_iff[simp]: "wf(listrel1 r) = wf r"
+by(metis wf_acc_iff in_lists_conv_set lists_accI lists_accD Cons_in_lists_iff)
+
 
 subsubsection {* Lifting Relations to Lists: all elements *}