1.1 --- a/NEWS Sat Jan 16 21:14:15 2010 +0100
1.2 +++ b/NEWS Tue Jan 19 16:52:01 2010 +0100
1.3 @@ -38,6 +38,7 @@
1.4 INTER_fold_inter ~> INFI_fold_inf
1.5 UNION_fold_union ~> SUPR_fold_sup
1.6
1.7 +* Added transpose to List.thy.
1.8
1.9 *** ML ***
1.10
2.1 --- a/src/HOL/List.thy Sat Jan 16 21:14:15 2010 +0100
2.2 +++ b/src/HOL/List.thy Tue Jan 19 16:52:01 2010 +0100
2.3 @@ -2383,7 +2383,6 @@
2.4 unfolding SUPR_def set_map [symmetric] Sup_set_fold foldl_map
2.5 by (simp add: sup_commute)
2.6
2.7 -
2.8 subsubsection {* List summation: @{const listsum} and @{text"\<Sum>"}*}
2.9
2.10 lemma listsum_append [simp]: "listsum (xs @ ys) = listsum xs + listsum ys"
2.11 @@ -3195,6 +3194,117 @@
2.12 apply auto
2.13 done
2.14
2.15 +subsubsection{*Transpose*}
2.16 +
2.17 +function transpose where
2.18 +"transpose [] = []" |
2.19 +"transpose ([] # xss) = transpose xss" |
2.20 +"transpose ((x#xs) # xss) =
2.21 + (x # [h. (h#t) \<leftarrow> xss]) # transpose (xs # [t. (h#t) \<leftarrow> xss])"
2.22 +by pat_completeness auto
2.23 +
2.24 +lemma transpose_aux_filter_head:
2.25 + "concat (map (list_case [] (\<lambda>h t. [h])) xss) =
2.26 + map (\<lambda>xs. hd xs) [ys\<leftarrow>xss . ys \<noteq> []]"
2.27 + by (induct xss) (auto split: list.split)
2.28 +
2.29 +lemma transpose_aux_filter_tail:
2.30 + "concat (map (list_case [] (\<lambda>h t. [t])) xss) =
2.31 + map (\<lambda>xs. tl xs) [ys\<leftarrow>xss . ys \<noteq> []]"
2.32 + by (induct xss) (auto split: list.split)
2.33 +
2.34 +lemma transpose_aux_max:
2.35 + "max (Suc (length xs)) (foldr (\<lambda>xs. max (length xs)) xss 0) =
2.36 + Suc (max (length xs) (foldr (\<lambda>x. max (length x - Suc 0)) [ys\<leftarrow>xss . ys\<noteq>[]] 0))"
2.37 + (is "max _ ?foldB = Suc (max _ ?foldA)")
2.38 +proof (cases "[ys\<leftarrow>xss . ys\<noteq>[]] = []")
2.39 + case True
2.40 + hence "foldr (\<lambda>xs. max (length xs)) xss 0 = 0"
2.41 + proof (induct xss)
2.42 + case (Cons x xs)
2.43 + moreover hence "x = []" by (cases x) auto
2.44 + ultimately show ?case by auto
2.45 + qed simp
2.46 + thus ?thesis using True by simp
2.47 +next
2.48 + case False
2.49 +
2.50 + have foldA: "?foldA = foldr (\<lambda>x. max (length x)) [ys\<leftarrow>xss . ys \<noteq> []] 0 - 1"
2.51 + by (induct xss) auto
2.52 + have foldB: "?foldB = foldr (\<lambda>x. max (length x)) [ys\<leftarrow>xss . ys \<noteq> []] 0"
2.53 + by (induct xss) auto
2.54 +
2.55 + have "0 < ?foldB"
2.56 + proof -
2.57 + from False
2.58 + obtain z zs where zs: "[ys\<leftarrow>xss . ys \<noteq> []] = z#zs" by (auto simp: neq_Nil_conv)
2.59 + hence "z \<in> set ([ys\<leftarrow>xss . ys \<noteq> []])" by auto
2.60 + hence "z \<noteq> []" by auto
2.61 + thus ?thesis
2.62 + unfolding foldB zs
2.63 + by (auto simp: max_def intro: less_le_trans)
2.64 + qed
2.65 + thus ?thesis
2.66 + unfolding foldA foldB max_Suc_Suc[symmetric]
2.67 + by simp
2.68 +qed
2.69 +
2.70 +termination transpose
2.71 + by (relation "measure (\<lambda>xs. foldr (\<lambda>xs. max (length xs)) xs 0 + length xs)")
2.72 + (auto simp: transpose_aux_filter_tail foldr_map comp_def transpose_aux_max less_Suc_eq_le)
2.73 +
2.74 +lemma transpose_empty: "(transpose xs = []) \<longleftrightarrow> (\<forall>x \<in> set xs. x = [])"
2.75 + by (induct rule: transpose.induct) simp_all
2.76 +
2.77 +lemma length_transpose:
2.78 + fixes xs :: "'a list list"
2.79 + shows "length (transpose xs) = foldr (\<lambda>xs. max (length xs)) xs 0"
2.80 + by (induct rule: transpose.induct)
2.81 + (auto simp: transpose_aux_filter_tail foldr_map comp_def transpose_aux_max
2.82 + max_Suc_Suc[symmetric] simp del: max_Suc_Suc)
2.83 +
2.84 +lemma nth_transpose:
2.85 + fixes xs :: "'a list list"
2.86 + assumes "i < length (transpose xs)"
2.87 + shows "transpose xs ! i = map (\<lambda>xs. xs ! i) [ys \<leftarrow> xs. i < length ys]"
2.88 +using assms proof (induct arbitrary: i rule: transpose.induct)
2.89 + case (3 x xs xss)
2.90 + def XS == "(x # xs) # xss"
2.91 + hence [simp]: "XS \<noteq> []" by auto
2.92 + thus ?case
2.93 + proof (cases i)
2.94 + case 0
2.95 + thus ?thesis by (simp add: transpose_aux_filter_head hd_conv_nth)
2.96 + next
2.97 + case (Suc j)
2.98 + have *: "\<And>xss. xs # map tl xss = map tl ((x#xs)#xss)" by simp
2.99 + have **: "\<And>xss. (x#xs) # filter (\<lambda>ys. ys \<noteq> []) xss = filter (\<lambda>ys. ys \<noteq> []) ((x#xs)#xss)" by simp
2.100 + { fix x have "Suc j < length x \<longleftrightarrow> x \<noteq> [] \<and> j < length x - Suc 0"
2.101 + by (cases x) simp_all
2.102 + } note *** = this
2.103 +
2.104 + have j_less: "j < length (transpose (xs # concat (map (list_case [] (\<lambda>h t. [t])) xss)))"
2.105 + using "3.prems" by (simp add: transpose_aux_filter_tail length_transpose Suc)
2.106 +
2.107 + show ?thesis
2.108 + unfolding transpose.simps `i = Suc j` nth_Cons_Suc "3.hyps"[OF j_less]
2.109 + apply (auto simp: transpose_aux_filter_tail filter_map comp_def length_transpose * ** *** XS_def[symmetric])
2.110 + apply (rule_tac y=x in list.exhaust)
2.111 + by auto
2.112 + qed
2.113 +qed simp_all
2.114 +
2.115 +lemma transpose_map_map:
2.116 + "transpose (map (map f) xs) = map (map f) (transpose xs)"
2.117 +proof (rule nth_equalityI, safe)
2.118 + have [simp]: "length (transpose (map (map f) xs)) = length (transpose xs)"
2.119 + by (simp add: length_transpose foldr_map comp_def)
2.120 + show "length (transpose (map (map f) xs)) = length (map (map f) (transpose xs))" by simp
2.121 +
2.122 + fix i assume "i < length (transpose (map (map f) xs))"
2.123 + thus "transpose (map (map f) xs) ! i = map (map f) (transpose xs) ! i"
2.124 + by (simp add: nth_transpose filter_map comp_def)
2.125 +qed
2.126
2.127 subsubsection {* (In)finiteness *}
2.128
2.129 @@ -3406,6 +3516,45 @@
2.130 lemma sorted_takeWhile: "sorted xs \<Longrightarrow> sorted (takeWhile P xs)"
2.131 apply (subst takeWhile_eq_take) by (rule sorted_take)
2.132
2.133 +lemma sorted_filter:
2.134 + "sorted (map f xs) \<Longrightarrow> sorted (map f (filter P xs))"
2.135 + by (induct xs) (simp_all add: sorted_Cons)
2.136 +
2.137 +lemma foldr_max_sorted:
2.138 + assumes "sorted (rev xs)"
2.139 + shows "foldr max xs y = (if xs = [] then y else max (xs ! 0) y)"
2.140 +using assms proof (induct xs)
2.141 + case (Cons x xs)
2.142 + moreover hence "sorted (rev xs)" using sorted_append by auto
2.143 + ultimately show ?case
2.144 + by (cases xs, auto simp add: sorted_append max_def)
2.145 +qed simp
2.146 +
2.147 +lemma filter_equals_takeWhile_sorted_rev:
2.148 + assumes sorted: "sorted (rev (map f xs))"
2.149 + shows "[x \<leftarrow> xs. t < f x] = takeWhile (\<lambda> x. t < f x) xs"
2.150 + (is "filter ?P xs = ?tW")
2.151 +proof (rule takeWhile_eq_filter[symmetric])
2.152 + let "?dW" = "dropWhile ?P xs"
2.153 + fix x assume "x \<in> set ?dW"
2.154 + then obtain i where i: "i < length ?dW" and nth_i: "x = ?dW ! i"
2.155 + unfolding in_set_conv_nth by auto
2.156 + hence "length ?tW + i < length (?tW @ ?dW)"
2.157 + unfolding length_append by simp
2.158 + hence i': "length (map f ?tW) + i < length (map f xs)" by simp
2.159 + have "(map f ?tW @ map f ?dW) ! (length (map f ?tW) + i) \<le>
2.160 + (map f ?tW @ map f ?dW) ! (length (map f ?tW) + 0)"
2.161 + using sorted_rev_nth_mono[OF sorted _ i', of "length ?tW"]
2.162 + unfolding map_append[symmetric] by simp
2.163 + hence "f x \<le> f (?dW ! 0)"
2.164 + unfolding nth_append_length_plus nth_i
2.165 + using i preorder_class.le_less_trans[OF le0 i] by simp
2.166 + also have "... \<le> t"
2.167 + using hd_dropWhile[of "?P" xs] le0[THEN preorder_class.le_less_trans, OF i]
2.168 + using hd_conv_nth[of "?dW"] by simp
2.169 + finally show "\<not> t < f x" by simp
2.170 +qed
2.171 +
2.172 end
2.173
2.174 lemma sorted_upt[simp]: "sorted[i..<j]"
2.175 @@ -3417,6 +3566,135 @@
2.176 apply(simp add:sorted_Cons)
2.177 done
2.178
2.179 +subsubsection {*@{const transpose} on sorted lists*}
2.180 +
2.181 +lemma sorted_transpose[simp]:
2.182 + shows "sorted (rev (map length (transpose xs)))"
2.183 + by (auto simp: sorted_equals_nth_mono rev_nth nth_transpose
2.184 + length_filter_conv_card intro: card_mono)
2.185 +
2.186 +lemma transpose_max_length:
2.187 + "foldr (\<lambda>xs. max (length xs)) (transpose xs) 0 = length [x \<leftarrow> xs. x \<noteq> []]"
2.188 + (is "?L = ?R")
2.189 +proof (cases "transpose xs = []")
2.190 + case False
2.191 + have "?L = foldr max (map length (transpose xs)) 0"
2.192 + by (simp add: foldr_map comp_def)
2.193 + also have "... = length (transpose xs ! 0)"
2.194 + using False sorted_transpose by (simp add: foldr_max_sorted)
2.195 + finally show ?thesis
2.196 + using False by (simp add: nth_transpose)
2.197 +next
2.198 + case True
2.199 + hence "[x \<leftarrow> xs. x \<noteq> []] = []"
2.200 + by (auto intro!: filter_False simp: transpose_empty)
2.201 + thus ?thesis by (simp add: transpose_empty True)
2.202 +qed
2.203 +
2.204 +lemma length_transpose_sorted:
2.205 + fixes xs :: "'a list list"
2.206 + assumes sorted: "sorted (rev (map length xs))"
2.207 + shows "length (transpose xs) = (if xs = [] then 0 else length (xs ! 0))"
2.208 +proof (cases "xs = []")
2.209 + case False
2.210 + thus ?thesis
2.211 + using foldr_max_sorted[OF sorted] False
2.212 + unfolding length_transpose foldr_map comp_def
2.213 + by simp
2.214 +qed simp
2.215 +
2.216 +lemma nth_nth_transpose_sorted[simp]:
2.217 + fixes xs :: "'a list list"
2.218 + assumes sorted: "sorted (rev (map length xs))"
2.219 + and i: "i < length (transpose xs)"
2.220 + and j: "j < length [ys \<leftarrow> xs. i < length ys]"
2.221 + shows "transpose xs ! i ! j = xs ! j ! i"
2.222 + using j filter_equals_takeWhile_sorted_rev[OF sorted, of i]
2.223 + nth_transpose[OF i] nth_map[OF j]
2.224 + by (simp add: takeWhile_nth)
2.225 +
2.226 +lemma transpose_column_length:
2.227 + fixes xs :: "'a list list"
2.228 + assumes sorted: "sorted (rev (map length xs))" and "i < length xs"
2.229 + shows "length (filter (\<lambda>ys. i < length ys) (transpose xs)) = length (xs ! i)"
2.230 +proof -
2.231 + have "xs \<noteq> []" using `i < length xs` by auto
2.232 + note filter_equals_takeWhile_sorted_rev[OF sorted, simp]
2.233 + { fix j assume "j \<le> i"
2.234 + note sorted_rev_nth_mono[OF sorted, of j i, simplified, OF this `i < length xs`]
2.235 + } note sortedE = this[consumes 1]
2.236 +
2.237 + have "{j. j < length (transpose xs) \<and> i < length (transpose xs ! j)}
2.238 + = {..< length (xs ! i)}"
2.239 + proof safe
2.240 + fix j
2.241 + assume "j < length (transpose xs)" and "i < length (transpose xs ! j)"
2.242 + with this(2) nth_transpose[OF this(1)]
2.243 + have "i < length (takeWhile (\<lambda>ys. j < length ys) xs)" by simp
2.244 + from nth_mem[OF this] takeWhile_nth[OF this]
2.245 + show "j < length (xs ! i)" by (auto dest: set_takeWhileD)
2.246 + next
2.247 + fix j assume "j < length (xs ! i)"
2.248 + thus "j < length (transpose xs)"
2.249 + using foldr_max_sorted[OF sorted] `xs \<noteq> []` sortedE[OF le0]
2.250 + by (auto simp: length_transpose comp_def foldr_map)
2.251 +
2.252 + have "Suc i \<le> length (takeWhile (\<lambda>ys. j < length ys) xs)"
2.253 + using `i < length xs` `j < length (xs ! i)` less_Suc_eq_le
2.254 + by (auto intro!: length_takeWhile_less_P_nth dest!: sortedE)
2.255 + with nth_transpose[OF `j < length (transpose xs)`]
2.256 + show "i < length (transpose xs ! j)" by simp
2.257 + qed
2.258 + thus ?thesis by (simp add: length_filter_conv_card)
2.259 +qed
2.260 +
2.261 +lemma transpose_column:
2.262 + fixes xs :: "'a list list"
2.263 + assumes sorted: "sorted (rev (map length xs))" and "i < length xs"
2.264 + shows "map (\<lambda>ys. ys ! i) (filter (\<lambda>ys. i < length ys) (transpose xs))
2.265 + = xs ! i" (is "?R = _")
2.266 +proof (rule nth_equalityI, safe)
2.267 + show length: "length ?R = length (xs ! i)"
2.268 + using transpose_column_length[OF assms] by simp
2.269 +
2.270 + fix j assume j: "j < length ?R"
2.271 + note * = less_le_trans[OF this, unfolded length_map, OF length_filter_le]
2.272 + from j have j_less: "j < length (xs ! i)" using length by simp
2.273 + have i_less_tW: "Suc i \<le> length (takeWhile (\<lambda>ys. Suc j \<le> length ys) xs)"
2.274 + proof (rule length_takeWhile_less_P_nth)
2.275 + show "Suc i \<le> length xs" using `i < length xs` by simp
2.276 + fix k assume "k < Suc i"
2.277 + hence "k \<le> i" by auto
2.278 + with sorted_rev_nth_mono[OF sorted this] `i < length xs`
2.279 + have "length (xs ! i) \<le> length (xs ! k)" by simp
2.280 + thus "Suc j \<le> length (xs ! k)" using j_less by simp
2.281 + qed
2.282 + have i_less_filter: "i < length [ys\<leftarrow>xs . j < length ys]"
2.283 + unfolding filter_equals_takeWhile_sorted_rev[OF sorted, of j]
2.284 + using i_less_tW by (simp_all add: Suc_le_eq)
2.285 + from j show "?R ! j = xs ! i ! j"
2.286 + unfolding filter_equals_takeWhile_sorted_rev[OF sorted_transpose, of i]
2.287 + by (simp add: takeWhile_nth nth_nth_transpose_sorted[OF sorted * i_less_filter])
2.288 +qed
2.289 +
2.290 +lemma transpose_transpose:
2.291 + fixes xs :: "'a list list"
2.292 + assumes sorted: "sorted (rev (map length xs))"
2.293 + shows "transpose (transpose xs) = takeWhile (\<lambda>x. x \<noteq> []) xs" (is "?L = ?R")
2.294 +proof -
2.295 + have len: "length ?L = length ?R"
2.296 + unfolding length_transpose transpose_max_length
2.297 + using filter_equals_takeWhile_sorted_rev[OF sorted, of 0]
2.298 + by simp
2.299 +
2.300 + { fix i assume "i < length ?R"
2.301 + with less_le_trans[OF _ length_takeWhile_le[of _ xs]]
2.302 + have "i < length xs" by simp
2.303 + } note * = this
2.304 + show ?thesis
2.305 + by (rule nth_equalityI)
2.306 + (simp_all add: len nth_transpose transpose_column[OF sorted] * takeWhile_nth)
2.307 +qed
2.308
2.309 subsubsection {* @{text sorted_list_of_set} *}
2.310
2.311 @@ -3449,7 +3727,6 @@
2.312
2.313 end
2.314
2.315 -
2.316 subsubsection {* @{text lists}: the list-forming operator over sets *}
2.317
2.318 inductive_set
2.319 @@ -3548,7 +3825,6 @@
2.320 "listset [] = {[]}"
2.321 "listset(A#As) = set_Cons A (listset As)"
2.322
2.323 -
2.324 subsection{*Relations on Lists*}
2.325
2.326 subsubsection {* Length Lexicographic Ordering *}