# HG changeset patch
# User nipkow
# Date 1404925040 -7200
# Node ID da5038b3886c5650cee6cb8f54d535cdeca155be
# Parent  5e8317c5b689b0c7c6edd8d70821e9f8bc83873c# Parent  810bc6c41ebd09373d2b08745766bccaa55efc51
merged

diff -r 5e8317c5b689 -r da5038b3886c src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Jul 09 18:48:37 2014 +0200
+++ b/src/HOL/List.thy	Wed Jul 09 18:57:20 2014 +0200
@@ -1835,9 +1835,9 @@
 lemma list_update_swap:
   "i \<noteq> i' \<Longrightarrow> xs [i := x, i' := x'] = xs [i' := x', i := x]"
 apply (induct xs arbitrary: i i')
-apply simp
+ apply simp
 apply (case_tac i, case_tac i')
-apply auto
+  apply auto
 apply (case_tac i')
 apply auto
 done
@@ -3278,6 +3278,17 @@
   set(xs[n := x]) = insert x (set xs - {xs!n})"
 by(auto simp: set_eq_iff in_set_conv_nth nth_list_update nth_eq_iff_index_eq)
 
+lemma distinct_swap[simp]: "\<lbrakk> i < size xs; j < size xs \<rbrakk> \<Longrightarrow>
+  distinct(xs[i := xs!j, j := xs!i]) = distinct xs"
+apply (simp add: distinct_conv_nth nth_list_update)
+apply safe
+apply metis+
+done
+
+lemma set_swap[simp]:
+  "\<lbrakk> i < size xs; j < size xs \<rbrakk> \<Longrightarrow> set(xs[i := xs!j, j := xs!i]) = set xs"
+by(simp add: set_conv_nth nth_list_update) metis
+
 lemma distinct_card: "distinct xs ==> card (set xs) = size xs"
 by (induct xs) auto