# HG changeset patch
# User bulwahn
# Date 1508602499 -7200
# Node ID e92d48a42a01a663cf2e01c3a988eac13b4353e9
# Parent  7fe528893a6c79d70f6e17f6e201ba1125b316da
drop a superfluous assumption that was found by the find_unused_assms command and tune proof

diff -r 7fe528893a6c -r e92d48a42a01 src/HOL/List.thy
--- a/src/HOL/List.thy	Sat Oct 21 18:11:29 2017 +0200
+++ b/src/HOL/List.thy	Sat Oct 21 18:14:59 2017 +0200
@@ -4911,13 +4911,13 @@
   sorted_wrt P xs \<and> sorted_wrt P ys \<and> (\<forall>x\<in>set xs. \<forall>y\<in>set ys. P x y)"  
 by (induction xs) (auto simp: sorted_wrt_Cons[OF assms])
 
-lemma sorted_wrt_rev: assumes "transp P"
-shows "sorted_wrt P (rev xs) = sorted_wrt (\<lambda>x y. P y x) xs"
-proof(induction xs rule: sorted_wrt_induct)
-  case 3 thus ?case
-    by(simp add: sorted_wrt_append sorted_wrt_Cons assms)
-      (meson assms transpD)
-qed simp_all
+lemma sorted_wrt_backwards:
+  "sorted_wrt P (xs @ [y, z]) = (P y z \<and> sorted_wrt P (xs @ [y]))"
+by (induction xs rule: sorted_wrt_induct) auto
+
+lemma sorted_wrt_rev:
+  "sorted_wrt P (rev xs) = sorted_wrt (\<lambda>x y. P y x) xs"
+by (induction xs rule: sorted_wrt_induct) (simp_all add: sorted_wrt_backwards)
 
 lemma sorted_wrt_mono:
   "(\<And>x y. P x y \<Longrightarrow> Q x y) \<Longrightarrow> sorted_wrt P xs \<Longrightarrow> sorted_wrt Q xs"