Add transpose to the List-theory.

--- a/NEWS	Sat Jan 16 21:14:15 2010 +0100
+++ b/NEWS	Tue Jan 19 16:52:01 2010 +0100
@@ -38,6 +38,7 @@
   INTER_fold_inter              ~> INFI_fold_inf
   UNION_fold_union              ~> SUPR_fold_sup
 
+* Added transpose to List.thy.
 
 *** ML ***
 

--- a/src/HOL/List.thy	Sat Jan 16 21:14:15 2010 +0100
+++ b/src/HOL/List.thy	Tue Jan 19 16:52:01 2010 +0100
@@ -2383,7 +2383,6 @@
   unfolding SUPR_def set_map [symmetric] Sup_set_fold foldl_map
     by (simp add: sup_commute)
 
-
 subsubsection {* List summation: @{const listsum} and @{text"\<Sum>"}*}
 
 lemma listsum_append [simp]: "listsum (xs @ ys) = listsum xs + listsum ys"
@@ -3195,6 +3194,117 @@
  apply auto
 done
 
+subsubsection{*Transpose*}
+
+function transpose where
+"transpose []             = []" |
+"transpose ([]     # xss) = transpose xss" |
+"transpose ((x#xs) # xss) =
+  (x # [h. (h#t) \<leftarrow> xss]) # transpose (xs # [t. (h#t) \<leftarrow> xss])"
+by pat_completeness auto
+
+lemma transpose_aux_filter_head:
+  "concat (map (list_case [] (\<lambda>h t. [h])) xss) =
+  map (\<lambda>xs. hd xs) [ys\<leftarrow>xss . ys \<noteq> []]"
+  by (induct xss) (auto split: list.split)
+
+lemma transpose_aux_filter_tail:
+  "concat (map (list_case [] (\<lambda>h t. [t])) xss) =
+  map (\<lambda>xs. tl xs) [ys\<leftarrow>xss . ys \<noteq> []]"
+  by (induct xss) (auto split: list.split)
+
+lemma transpose_aux_max:
+  "max (Suc (length xs)) (foldr (\<lambda>xs. max (length xs)) xss 0) =
+  Suc (max (length xs) (foldr (\<lambda>x. max (length x - Suc 0)) [ys\<leftarrow>xss . ys\<noteq>[]] 0))"
+  (is "max _ ?foldB = Suc (max _ ?foldA)")
+proof (cases "[ys\<leftarrow>xss . ys\<noteq>[]] = []")
+  case True
+  hence "foldr (\<lambda>xs. max (length xs)) xss 0 = 0"
+  proof (induct xss)
+    case (Cons x xs)
+    moreover hence "x = []" by (cases x) auto
+    ultimately show ?case by auto
+  qed simp
+  thus ?thesis using True by simp
+next
+  case False
+
+  have foldA: "?foldA = foldr (\<lambda>x. max (length x)) [ys\<leftarrow>xss . ys \<noteq> []] 0 - 1"
+    by (induct xss) auto
+  have foldB: "?foldB = foldr (\<lambda>x. max (length x)) [ys\<leftarrow>xss . ys \<noteq> []] 0"
+    by (induct xss) auto
+
+  have "0 < ?foldB"
+  proof -
+    from False
+    obtain z zs where zs: "[ys\<leftarrow>xss . ys \<noteq> []] = z#zs" by (auto simp: neq_Nil_conv)
+    hence "z \<in> set ([ys\<leftarrow>xss . ys \<noteq> []])" by auto
+    hence "z \<noteq> []" by auto
+    thus ?thesis
+      unfolding foldB zs
+      by (auto simp: max_def intro: less_le_trans)
+  qed
+  thus ?thesis
+    unfolding foldA foldB max_Suc_Suc[symmetric]
+    by simp
+qed
+
+termination transpose
+  by (relation "measure (\<lambda>xs. foldr (\<lambda>xs. max (length xs)) xs 0 + length xs)")
+     (auto simp: transpose_aux_filter_tail foldr_map comp_def transpose_aux_max less_Suc_eq_le)
+
+lemma transpose_empty: "(transpose xs = []) \<longleftrightarrow> (\<forall>x \<in> set xs. x = [])"
+  by (induct rule: transpose.induct) simp_all
+
+lemma length_transpose:
+  fixes xs :: "'a list list"
+  shows "length (transpose xs) = foldr (\<lambda>xs. max (length xs)) xs 0"
+  by (induct rule: transpose.induct)
+    (auto simp: transpose_aux_filter_tail foldr_map comp_def transpose_aux_max
+                max_Suc_Suc[symmetric] simp del: max_Suc_Suc)
+
+lemma nth_transpose:
+  fixes xs :: "'a list list"
+  assumes "i < length (transpose xs)"
+  shows "transpose xs ! i = map (\<lambda>xs. xs ! i) [ys \<leftarrow> xs. i < length ys]"
+using assms proof (induct arbitrary: i rule: transpose.induct)
+  case (3 x xs xss)
+  def XS == "(x # xs) # xss"
+  hence [simp]: "XS \<noteq> []" by auto
+  thus ?case
+  proof (cases i)
+    case 0
+    thus ?thesis by (simp add: transpose_aux_filter_head hd_conv_nth)
+  next
+    case (Suc j)
+    have *: "\<And>xss. xs # map tl xss = map tl ((x#xs)#xss)" by simp
+    have **: "\<And>xss. (x#xs) # filter (\<lambda>ys. ys \<noteq> []) xss = filter (\<lambda>ys. ys \<noteq> []) ((x#xs)#xss)" by simp
+    { fix x have "Suc j < length x \<longleftrightarrow> x \<noteq> [] \<and> j < length x - Suc 0"
+      by (cases x) simp_all
+    } note *** = this
+
+    have j_less: "j < length (transpose (xs # concat (map (list_case [] (\<lambda>h t. [t])) xss)))"
+      using "3.prems" by (simp add: transpose_aux_filter_tail length_transpose Suc)
+
+    show ?thesis
+      unfolding transpose.simps `i = Suc j` nth_Cons_Suc "3.hyps"[OF j_less]
+      apply (auto simp: transpose_aux_filter_tail filter_map comp_def length_transpose * ** *** XS_def[symmetric])
+      apply (rule_tac y=x in list.exhaust)
+      by auto
+  qed
+qed simp_all
+
+lemma transpose_map_map:
+  "transpose (map (map f) xs) = map (map f) (transpose xs)"
+proof (rule nth_equalityI, safe)
+  have [simp]: "length (transpose (map (map f) xs)) = length (transpose xs)"
+    by (simp add: length_transpose foldr_map comp_def)
+  show "length (transpose (map (map f) xs)) = length (map (map f) (transpose xs))" by simp
+
+  fix i assume "i < length (transpose (map (map f) xs))"
+  thus "transpose (map (map f) xs) ! i = map (map f) (transpose xs) ! i"
+    by (simp add: nth_transpose filter_map comp_def)
+qed
 
 subsubsection {* (In)finiteness *}
 
@@ -3406,6 +3516,45 @@
 lemma sorted_takeWhile: "sorted xs \<Longrightarrow> sorted (takeWhile P xs)"
   apply (subst takeWhile_eq_take) by (rule sorted_take)
 
+lemma sorted_filter:
+  "sorted (map f xs) \<Longrightarrow> sorted (map f (filter P xs))"
+  by (induct xs) (simp_all add: sorted_Cons)
+
+lemma foldr_max_sorted:
+  assumes "sorted (rev xs)"
+  shows "foldr max xs y = (if xs = [] then y else max (xs ! 0) y)"
+using assms proof (induct xs)
+  case (Cons x xs)
+  moreover hence "sorted (rev xs)" using sorted_append by auto
+  ultimately show ?case
+    by (cases xs, auto simp add: sorted_append max_def)
+qed simp
+
+lemma filter_equals_takeWhile_sorted_rev:
+  assumes sorted: "sorted (rev (map f xs))"
+  shows "[x \<leftarrow> xs. t < f x] = takeWhile (\<lambda> x. t < f x) xs"
+    (is "filter ?P xs = ?tW")
+proof (rule takeWhile_eq_filter[symmetric])
+  let "?dW" = "dropWhile ?P xs"
+  fix x assume "x \<in> set ?dW"
+  then obtain i where i: "i < length ?dW" and nth_i: "x = ?dW ! i"
+    unfolding in_set_conv_nth by auto
+  hence "length ?tW + i < length (?tW @ ?dW)"
+    unfolding length_append by simp
+  hence i': "length (map f ?tW) + i < length (map f xs)" by simp
+  have "(map f ?tW @ map f ?dW) ! (length (map f ?tW) + i) \<le>
+        (map f ?tW @ map f ?dW) ! (length (map f ?tW) + 0)"
+    using sorted_rev_nth_mono[OF sorted _ i', of "length ?tW"]
+    unfolding map_append[symmetric] by simp
+  hence "f x \<le> f (?dW ! 0)"
+    unfolding nth_append_length_plus nth_i
+    using i preorder_class.le_less_trans[OF le0 i] by simp
+  also have "... \<le> t"
+    using hd_dropWhile[of "?P" xs] le0[THEN preorder_class.le_less_trans, OF i]
+    using hd_conv_nth[of "?dW"] by simp
+  finally show "\<not> t < f x" by simp
+qed
+
 end
 
 lemma sorted_upt[simp]: "sorted[i..<j]"
@@ -3417,6 +3566,135 @@
 apply(simp add:sorted_Cons)
 done
 
+subsubsection {*@{const transpose} on sorted lists*}
+
+lemma sorted_transpose[simp]:
+  shows "sorted (rev (map length (transpose xs)))"
+  by (auto simp: sorted_equals_nth_mono rev_nth nth_transpose
+    length_filter_conv_card intro: card_mono)
+
+lemma transpose_max_length:
+  "foldr (\<lambda>xs. max (length xs)) (transpose xs) 0 = length [x \<leftarrow> xs. x \<noteq> []]"
+  (is "?L = ?R")
+proof (cases "transpose xs = []")
+  case False
+  have "?L = foldr max (map length (transpose xs)) 0"
+    by (simp add: foldr_map comp_def)
+  also have "... = length (transpose xs ! 0)"
+    using False sorted_transpose by (simp add: foldr_max_sorted)
+  finally show ?thesis
+    using False by (simp add: nth_transpose)
+next
+  case True
+  hence "[x \<leftarrow> xs. x \<noteq> []] = []"
+    by (auto intro!: filter_False simp: transpose_empty)
+  thus ?thesis by (simp add: transpose_empty True)
+qed
+
+lemma length_transpose_sorted:
+  fixes xs :: "'a list list"
+  assumes sorted: "sorted (rev (map length xs))"
+  shows "length (transpose xs) = (if xs = [] then 0 else length (xs ! 0))"
+proof (cases "xs = []")
+  case False
+  thus ?thesis
+    using foldr_max_sorted[OF sorted] False
+    unfolding length_transpose foldr_map comp_def
+    by simp
+qed simp
+
+lemma nth_nth_transpose_sorted[simp]:
+  fixes xs :: "'a list list"
+  assumes sorted: "sorted (rev (map length xs))"
+  and i: "i < length (transpose xs)"
+  and j: "j < length [ys \<leftarrow> xs. i < length ys]"
+  shows "transpose xs ! i ! j = xs ! j  ! i"
+  using j filter_equals_takeWhile_sorted_rev[OF sorted, of i]
+    nth_transpose[OF i] nth_map[OF j]
+  by (simp add: takeWhile_nth)
+
+lemma transpose_column_length:
+  fixes xs :: "'a list list"
+  assumes sorted: "sorted (rev (map length xs))" and "i < length xs"
+  shows "length (filter (\<lambda>ys. i < length ys) (transpose xs)) = length (xs ! i)"
+proof -
+  have "xs \<noteq> []" using `i < length xs` by auto
+  note filter_equals_takeWhile_sorted_rev[OF sorted, simp]
+  { fix j assume "j \<le> i"
+    note sorted_rev_nth_mono[OF sorted, of j i, simplified, OF this `i < length xs`]
+  } note sortedE = this[consumes 1]
+
+  have "{j. j < length (transpose xs) \<and> i < length (transpose xs ! j)}
+    = {..< length (xs ! i)}"
+  proof safe
+    fix j
+    assume "j < length (transpose xs)" and "i < length (transpose xs ! j)"
+    with this(2) nth_transpose[OF this(1)]
+    have "i < length (takeWhile (\<lambda>ys. j < length ys) xs)" by simp
+    from nth_mem[OF this] takeWhile_nth[OF this]
+    show "j < length (xs ! i)" by (auto dest: set_takeWhileD)
+  next
+    fix j assume "j < length (xs ! i)"
+    thus "j < length (transpose xs)"
+      using foldr_max_sorted[OF sorted] `xs \<noteq> []` sortedE[OF le0]
+      by (auto simp: length_transpose comp_def foldr_map)
+
+    have "Suc i \<le> length (takeWhile (\<lambda>ys. j < length ys) xs)"
+      using `i < length xs` `j < length (xs ! i)` less_Suc_eq_le
+      by (auto intro!: length_takeWhile_less_P_nth dest!: sortedE)
+    with nth_transpose[OF `j < length (transpose xs)`]
+    show "i < length (transpose xs ! j)" by simp
+  qed
+  thus ?thesis by (simp add: length_filter_conv_card)
+qed
+
+lemma transpose_column:
+  fixes xs :: "'a list list"
+  assumes sorted: "sorted (rev (map length xs))" and "i < length xs"
+  shows "map (\<lambda>ys. ys ! i) (filter (\<lambda>ys. i < length ys) (transpose xs))
+    = xs ! i" (is "?R = _")
+proof (rule nth_equalityI, safe)
+  show length: "length ?R = length (xs ! i)"
+    using transpose_column_length[OF assms] by simp
+
+  fix j assume j: "j < length ?R"
+  note * = less_le_trans[OF this, unfolded length_map, OF length_filter_le]
+  from j have j_less: "j < length (xs ! i)" using length by simp
+  have i_less_tW: "Suc i \<le> length (takeWhile (\<lambda>ys. Suc j \<le> length ys) xs)"
+  proof (rule length_takeWhile_less_P_nth)
+    show "Suc i \<le> length xs" using `i < length xs` by simp
+    fix k assume "k < Suc i"
+    hence "k \<le> i" by auto
+    with sorted_rev_nth_mono[OF sorted this] `i < length xs`
+    have "length (xs ! i) \<le> length (xs ! k)" by simp
+    thus "Suc j \<le> length (xs ! k)" using j_less by simp
+  qed
+  have i_less_filter: "i < length [ys\<leftarrow>xs . j < length ys]"
+    unfolding filter_equals_takeWhile_sorted_rev[OF sorted, of j]
+    using i_less_tW by (simp_all add: Suc_le_eq)
+  from j show "?R ! j = xs ! i ! j"
+    unfolding filter_equals_takeWhile_sorted_rev[OF sorted_transpose, of i]
+    by (simp add: takeWhile_nth nth_nth_transpose_sorted[OF sorted * i_less_filter])
+qed
+
+lemma transpose_transpose:
+  fixes xs :: "'a list list"
+  assumes sorted: "sorted (rev (map length xs))"
+  shows "transpose (transpose xs) = takeWhile (\<lambda>x. x \<noteq> []) xs" (is "?L = ?R")
+proof -
+  have len: "length ?L = length ?R"
+    unfolding length_transpose transpose_max_length
+    using filter_equals_takeWhile_sorted_rev[OF sorted, of 0]
+    by simp
+
+  { fix i assume "i < length ?R"
+    with less_le_trans[OF _ length_takeWhile_le[of _ xs]]
+    have "i < length xs" by simp
+  } note * = this
+  show ?thesis
+    by (rule nth_equalityI)
+       (simp_all add: len nth_transpose transpose_column[OF sorted] * takeWhile_nth)
+qed
 
 subsubsection {* @{text sorted_list_of_set} *}
 
@@ -3449,7 +3727,6 @@
 
 end
 
-
 subsubsection {* @{text lists}: the list-forming operator over sets *}
 
 inductive_set
@@ -3548,7 +3825,6 @@
    "listset []    = {[]}"
    "listset(A#As) = set_Cons A (listset As)"
 
-
 subsection{*Relations on Lists*}
 
 subsubsection {* Length Lexicographic Ordering *}