# HG changeset patch
# User bulwahn
# Date 1508602751 -7200
# Node ID d67d28254ff2e7ecf9f8385a455172142160da0c
# Parent  5ec8cd4db7e2465b4b96988fb16245949885fe5f
remove trailing whitespaces in List

diff -r 5ec8cd4db7e2 -r d67d28254ff2 src/HOL/List.thy
--- a/src/HOL/List.thy	Sat Oct 21 18:16:56 2017 +0200
+++ b/src/HOL/List.thy	Sat Oct 21 18:19:11 2017 +0200
@@ -295,7 +295,7 @@
 @{lemma "product_lists [[a,b], [c], [d,e]] = [[a,c,d], [a,c,e], [b,c,d], [b,c,e]]" by simp}\\
 @{lemma "splice [a,b,c] [x,y,z] = [a,x,b,y,c,z]" by simp}\\
 @{lemma "splice [a,b,c,d] [x,y] = [a,x,b,y,c,d]" by simp}\\
-@{lemma "shuffle [a,b] [c,d] =  {[a,b,c,d],[a,c,b,d],[a,c,d,b],[c,a,b,d],[c,a,d,b],[c,d,a,b]}" 
+@{lemma "shuffle [a,b] [c,d] =  {[a,b,c,d],[a,c,b,d],[a,c,d,b],[c,a,b,d],[c,a,d,b],[c,d,a,b]}"
     by (simp add: insert_commute)}\\
 @{lemma "take 2 [a,b,c,d] = [a,b]" by simp}\\
 @{lemma "take 6 [a,b,c,d] = [a,b,c,d]" by simp}\\
@@ -4557,13 +4557,13 @@
     (xs \<noteq> [] \<and> hd xs = z \<and> zs \<in> shuffle (tl xs) ys \<or>
      ys \<noteq> [] \<and> hd ys = z \<and> zs \<in> shuffle xs (tl ys))"
   by (induct xs ys rule: shuffle.induct) auto
-  
+
 lemma splice_in_shuffle [simp, intro]: "splice xs ys \<in> shuffle xs ys"
   by (induction xs ys rule: splice.induct) (simp_all add: Cons_in_shuffle_iff)
 
-lemma Nil_in_shuffleI: "xs = [] \<Longrightarrow> ys = [] \<Longrightarrow> [] \<in> shuffle xs ys" 
+lemma Nil_in_shuffleI: "xs = [] \<Longrightarrow> ys = [] \<Longrightarrow> [] \<in> shuffle xs ys"
   by simp
-    
+
 lemma Cons_in_shuffle_leftI: "zs \<in> shuffle xs ys \<Longrightarrow> z # zs \<in> shuffle (z # xs) ys"
   by (cases ys) auto
 
@@ -4572,10 +4572,10 @@
 
 lemma finite_shuffle [simp, intro]: "finite (shuffle xs ys)"
   by (induction xs ys rule: shuffle.induct) simp_all
-    
+
 lemma length_shuffle: "zs \<in> shuffle xs ys \<Longrightarrow> length zs = length xs + length ys"
   by (induction xs ys arbitrary: zs rule: shuffle.induct) auto
-  
+
 lemma set_shuffle: "zs \<in> shuffle xs ys \<Longrightarrow> set zs = set xs \<union> set ys"
   by (induction xs ys arbitrary: zs rule: shuffle.induct) auto
 
@@ -4594,10 +4594,10 @@
 
 lemma shuffle_commutes: "shuffle xs ys = shuffle ys xs"
   by (induction xs ys rule: shuffle.induct) (simp_all add: Un_commute)
-    
+
 lemma Cons_shuffle_subset1: "op # x ` shuffle xs ys \<subseteq> shuffle (x # xs) ys"
   by (cases ys) auto
-    
+
 lemma Cons_shuffle_subset2: "op # y ` shuffle xs ys \<subseteq> shuffle xs (y # ys)"
   by (cases xs) auto
 
@@ -4608,7 +4608,7 @@
     by (auto simp: image_image)
   show ?thesis
   by (induction xs ys rule: shuffle.induct)
-     (simp_all split: if_splits add: image_Un * Un_absorb1 Un_absorb2 
+     (simp_all split: if_splits add: image_Un * Un_absorb1 Un_absorb2
            Cons_shuffle_subset1 Cons_shuffle_subset2)
 qed
 
@@ -4638,7 +4638,7 @@
 lemma filter_shuffle_disjoint2:
   assumes "set xs \<inter> set ys = {}" "zs \<in> shuffle xs ys"
   shows   "filter (\<lambda>x. x \<in> set ys) zs = ys" "filter (\<lambda>x. x \<notin> set ys) zs = xs"
-  using filter_shuffle_disjoint1[of ys xs zs] assms 
+  using filter_shuffle_disjoint1[of ys xs zs] assms
   by (simp_all add: shuffle_commutes Int_commute)
 
 lemma partition_in_shuffle:
@@ -4669,7 +4669,7 @@
 proof (intro equalityI subsetI)
   fix zs assume zs: "zs \<in> shuffle xs ys"
   hence [simp]: "set zs = set xs \<union> set ys" by (rule set_shuffle)
-  from assms have "filter P zs = filter (\<lambda>x. x \<in> set xs) zs" 
+  from assms have "filter P zs = filter (\<lambda>x. x \<in> set xs) zs"
                   "filter (\<lambda>x. \<not>P x) zs = filter (\<lambda>x. x \<in> set ys) zs"
     by (intro filter_cong refl; force)+
   moreover from assms have "set xs \<inter> set ys = {}" by auto
@@ -4908,7 +4908,7 @@
 lemma sorted_wrt_append:
 assumes "transp P"
 shows "sorted_wrt P (xs @ ys) \<longleftrightarrow>
-  sorted_wrt P xs \<and> sorted_wrt P ys \<and> (\<forall>x\<in>set xs. \<forall>y\<in>set ys. P x y)"  
+  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_backwards:
@@ -4923,7 +4923,7 @@
   "(\<And>x y. P x y \<Longrightarrow> Q x y) \<Longrightarrow> sorted_wrt P xs \<Longrightarrow> sorted_wrt Q xs"
 by(induction xs rule: sorted_wrt_induct)(auto)
 
-text \<open>Strictly Ascending Sequences of Natural Numbers\<close>    
+text \<open>Strictly Ascending Sequences of Natural Numbers\<close>
 
 lemma sorted_wrt_upt[simp]: "sorted_wrt (op <) [0..<n]"
 by(induction n) (auto simp: sorted_wrt_append)
@@ -4938,7 +4938,7 @@
   case snoc
   thus ?case
     by (auto simp: nth_append sorted_wrt_append)
-       (metis less_antisym not_less nth_mem)  
+       (metis less_antisym not_less nth_mem)
 qed
 
 
@@ -5356,20 +5356,20 @@
   "x \<in> set xs \<Longrightarrow> [y <- sort_key f xs. f y = f x] = [y <- xs. f y = f x]"
 proof (induction xs arbitrary: x)
   case Nil thus ?case by simp
-next  
+next
   case (Cons a xs)
-  thus ?case 
+  thus ?case
   proof (cases "x \<in> set xs")
-    case True 
+    case True
     thus ?thesis
     proof (cases "f a = f x")
-      case False thus ?thesis 
+      case False thus ?thesis
         using Cons.IH by (metis (mono_tags) True filter.simps(2) filter_sort)
     next
       case True
       hence ler: "[y <- (a # xs). f y = f x] = a # [y <- xs. f y = f a]" by simp
       have "\<forall>y \<in> set (sort_key f [y <- xs. f y = f a]). f y = f a" by simp
-      hence "insort_key f a (sort_key f [y <- xs. f y = f a]) 
+      hence "insort_key f a (sort_key f [y <- xs. f y = f a])
               = a # (sort_key f [y <- xs. f y = f a])"
         by (simp add: insort_is_Cons)
       hence lel: "[y <- sort_key f (a # xs). f y = f x] = a # [y <- sort_key f xs. f y = f a]"
@@ -5381,7 +5381,7 @@
     from Cons.prems have "x = a" by (metis False set_ConsD)
     have ler: "[y <- (a # xs). f y = f a] = a # [y <- xs. f y = f a]" by simp
     have "\<forall>y \<in> set (sort_key f [y <- xs. f y = f a]). f y = f a" by simp
-    hence "insort_key f a (sort_key f [y <- xs. f y = f a]) 
+    hence "insort_key f a (sort_key f [y <- xs. f y = f a])
            = a # (sort_key f [y <- xs. f y = f a])"
       by (simp add: insort_is_Cons)
     hence lel: "[y <- sort_key f (a # xs). f y = f a] = a # [y <- sort_key f xs. f y = f a]"
@@ -5397,7 +5397,7 @@
       case True
       then obtain z where Z: "z \<in> set xs \<and> f z = f a" by auto
       hence L: "[y <- sort_key f xs. f y = f z] = [y <- sort_key f xs. f y = f a]" by simp
-      from Z have R: "[y <- xs. f y = f z] = [y <- xs. f y = f a]" by simp 
+      from Z have R: "[y <- xs. f y = f z] = [y <- xs. f y = f a]" by simp
       from L R Z show ?thesis using Cons.IH ler lel \<open>x=a\<close> by metis
     qed
   qed
@@ -7315,7 +7315,7 @@
 lemma nths_transfer [transfer_rule]:
   "(list_all2 A ===> rel_set (op =) ===> list_all2 A) nths nths"
   unfolding nths_def [abs_def] by transfer_prover
-    
+
 lemma subseqs_transfer [transfer_rule]:
   "(list_all2 A ===> list_all2 (list_all2 A)) subseqs subseqs"
   unfolding subseqs_def [abs_def] by transfer_prover
@@ -7365,7 +7365,7 @@
   apply (rule rel_funI)
   apply (erule_tac xs=x in list_all2_induct, simp, simp add: rel_fun_def)
   done
-    
+
 lemma shuffle_transfer [transfer_rule]:
   "(list_all2 A ===> list_all2 A ===> rel_set (list_all2 A)) shuffle shuffle"
 proof (intro rel_funI, goal_cases)
@@ -7384,7 +7384,7 @@
                (op # x' ` shuffle xs'' ys' \<union> op # y' ` shuffle xs' ys'')" by transfer_prover
     thus ?case by (simp add: xs' ys')
   qed (auto simp: rel_set_def)
-qed 
+qed
 
 lemma rtrancl_parametric [transfer_rule]:
   assumes [transfer_rule]: "bi_unique A" "bi_total A"