Added transpose_rectangle, when the input list is rectangular.

--- a/src/HOL/List.thy	Tue Jan 19 16:52:01 2010 +0100
+++ b/src/HOL/List.thy	Tue Jan 19 17:53:11 2010 +0100
@@ -3696,6 +3696,24 @@
        (simp_all add: len nth_transpose transpose_column[OF sorted] * takeWhile_nth)
 qed
 
+theorem transpose_rectangle:
+  assumes "xs = [] \<Longrightarrow> n = 0"
+  assumes rect: "\<And> i. i < length xs \<Longrightarrow> length (xs ! i) = n"
+  shows "transpose xs = map (\<lambda> i. map (\<lambda> j. xs ! j ! i) [0..<length xs]) [0..<n]"
+    (is "?trans = ?map")
+proof (rule nth_equalityI)
+  have "sorted (rev (map length xs))"
+    by (auto simp: rev_nth rect intro!: sorted_nth_monoI)
+  from foldr_max_sorted[OF this] assms
+  show len: "length ?trans = length ?map"
+    by (simp_all add: length_transpose foldr_map comp_def)
+  moreover
+  { fix i assume "i < n" hence "[ys\<leftarrow>xs . i < length ys] = xs"
+      using rect by (auto simp: in_set_conv_nth intro!: filter_True) }
+  ultimately show "\<forall>i < length ?trans. ?trans ! i = ?map ! i"
+    by (auto simp: nth_transpose intro: nth_equalityI)
+qed
+
 subsubsection {* @{text sorted_list_of_set} *}
 
 text{* This function maps (finite) linearly ordered sets to sorted