1.1 --- a/src/HOL/List.thy Thu Mar 27 19:04:35 2008 +0100
1.2 +++ b/src/HOL/List.thy Thu Mar 27 19:04:36 2008 +0100
1.3 @@ -418,17 +418,26 @@
1.4 lemma impossible_Cons: "length xs <= length ys ==> xs = x # ys = False"
1.5 by (induct xs) auto
1.6
1.7 -lemma list_induct2 [consumes 1]:
1.8 - "\<lbrakk> length xs = length ys;
1.9 - P [] [];
1.10 - \<And>x xs y ys. \<lbrakk> length xs = length ys; P xs ys \<rbrakk> \<Longrightarrow> P (x#xs) (y#ys) \<rbrakk>
1.11 - \<Longrightarrow> P xs ys"
1.12 -apply(induct xs arbitrary: ys)
1.13 - apply simp
1.14 -apply(case_tac ys)
1.15 - apply simp
1.16 -apply simp
1.17 -done
1.18 +lemma list_induct2 [consumes 1, case_names Nil Cons]:
1.19 + "length xs = length ys \<Longrightarrow> P [] [] \<Longrightarrow>
1.20 + (\<And>x xs y ys. length xs = length ys \<Longrightarrow> P xs ys \<Longrightarrow> P (x#xs) (y#ys))
1.21 + \<Longrightarrow> P xs ys"
1.22 +proof (induct xs arbitrary: ys)
1.23 + case Nil then show ?case by simp
1.24 +next
1.25 + case (Cons x xs ys) then show ?case by (cases ys) simp_all
1.26 +qed
1.27 +
1.28 +lemma list_induct3 [consumes 2, case_names Nil Cons]:
1.29 + "length xs = length ys \<Longrightarrow> length ys = length zs \<Longrightarrow> P [] [] [] \<Longrightarrow>
1.30 + (\<And>x xs y ys z zs. length xs = length ys \<Longrightarrow> length ys = length zs \<Longrightarrow> P xs ys zs \<Longrightarrow> P (x#xs) (y#ys) (z#zs))
1.31 + \<Longrightarrow> P xs ys zs"
1.32 +proof (induct xs arbitrary: ys zs)
1.33 + case Nil then show ?case by simp
1.34 +next
1.35 + case (Cons x xs ys zs) then show ?case by (cases ys, simp_all)
1.36 + (cases zs, simp_all)
1.37 +qed
1.38
1.39 lemma list_induct2':
1.40 "\<lbrakk> P [] [];
1.41 @@ -951,6 +960,9 @@
1.42 lemma card_length: "card (set xs) \<le> length xs"
1.43 by (induct xs) (auto simp add: card_insert_if)
1.44
1.45 +lemma set_minus_filter_out:
1.46 + "set xs - {y} = set (filter (\<lambda>x. \<not> (x = y)) xs)"
1.47 + by (induct xs) auto
1.48
1.49 subsubsection {* @{text filter} *}
1.50
1.51 @@ -1092,6 +1104,41 @@
1.52 by (induct ys) simp_all
1.53
1.54
1.55 +subsubsection {* List partitioning *}
1.56 +
1.57 +primrec partition :: "('a \<Rightarrow> bool) \<Rightarrow>'a list \<Rightarrow> 'a list \<times> 'a list" where
1.58 + "partition P [] = ([], [])"
1.59 + | "partition P (x # xs) =
1.60 + (let (yes, no) = partition P xs
1.61 + in if P x then (x # yes, no) else (yes, x # no))"
1.62 +
1.63 +lemma partition_filter1:
1.64 + "fst (partition P xs) = filter P xs"
1.65 +by (induct xs) (auto simp add: Let_def split_def)
1.66 +
1.67 +lemma partition_filter2:
1.68 + "snd (partition P xs) = filter (Not o P) xs"
1.69 +by (induct xs) (auto simp add: Let_def split_def)
1.70 +
1.71 +lemma partition_P:
1.72 + assumes "partition P xs = (yes, no)"
1.73 + shows "(\<forall>p \<in> set yes. P p) \<and> (\<forall>p \<in> set no. \<not> P p)"
1.74 +proof -
1.75 + from assms have "yes = fst (partition P xs)" and "no = snd (partition P xs)"
1.76 + by simp_all
1.77 + then show ?thesis by (simp_all add: partition_filter1 partition_filter2)
1.78 +qed
1.79 +
1.80 +lemma partition_set:
1.81 + assumes "partition P xs = (yes, no)"
1.82 + shows "set yes \<union> set no = set xs"
1.83 +proof -
1.84 + from assms have "yes = fst (partition P xs)" and "no = snd (partition P xs)"
1.85 + by simp_all
1.86 + then show ?thesis by (auto simp add: partition_filter1 partition_filter2)
1.87 +qed
1.88 +
1.89 +
1.90 subsubsection {* @{text concat} *}
1.91
1.92 lemma concat_append [simp]: "concat (xs @ ys) = concat xs @ concat ys"
1.93 @@ -1966,17 +2013,19 @@
1.94
1.95 subsubsection {* List summation: @{const listsum} and @{text"\<Sum>"}*}
1.96
1.97 -lemma listsum_append[simp]: "listsum (xs @ ys) = listsum xs + listsum ys"
1.98 +lemma listsum_append [simp]: "listsum (xs @ ys) = listsum xs + listsum ys"
1.99 by (induct xs) (simp_all add:add_assoc)
1.100
1.101 -lemma listsum_rev[simp]:
1.102 -fixes xs :: "'a::comm_monoid_add list"
1.103 -shows "listsum (rev xs) = listsum xs"
1.104 +lemma listsum_rev [simp]:
1.105 + fixes xs :: "'a\<Colon>comm_monoid_add list"
1.106 + shows "listsum (rev xs) = listsum xs"
1.107 by (induct xs) (simp_all add:add_ac)
1.108
1.109 -lemma listsum_foldr:
1.110 - "listsum xs = foldr (op +) xs 0"
1.111 -by(induct xs) auto
1.112 +lemma listsum_foldr: "listsum xs = foldr (op +) xs 0"
1.113 +by (induct xs) auto
1.114 +
1.115 +lemma length_concat: "length (concat xss) = listsum (map length xss)"
1.116 +by (induct xss) simp_all
1.117
1.118 text{* For efficient code generation ---
1.119 @{const listsum} is not tail recursive but @{const foldl} is. *}
1.120 @@ -1997,13 +2046,17 @@
1.121 "SUM x<-xs. b" == "CONST listsum (map (%x. b) xs)"
1.122 "\<Sum>x\<leftarrow>xs. b" == "CONST listsum (map (%x. b) xs)"
1.123
1.124 +lemma listsum_triv: "(\<Sum>x\<leftarrow>xs. r) = of_nat (length xs) * r"
1.125 + by (induct xs) (simp_all add: left_distrib)
1.126 +
1.127 lemma listsum_0 [simp]: "(\<Sum>x\<leftarrow>xs. 0) = 0"
1.128 -by (induct xs) simp_all
1.129 + by (induct xs) (simp_all add: left_distrib)
1.130
1.131 text{* For non-Abelian groups @{text xs} needs to be reversed on one side: *}
1.132 lemma uminus_listsum_map:
1.133 - "- listsum (map f xs) = (listsum (map (uminus o f) xs) :: 'a::ab_group_add)"
1.134 -by(induct xs) simp_all
1.135 + fixes f :: "'a \<Rightarrow> 'b\<Colon>ab_group_add"
1.136 + shows "- listsum (map f xs) = (listsum (map (uminus o f) xs))"
1.137 +by (induct xs) simp_all
1.138
1.139
1.140 subsubsection {* @{text upt} *}
1.141 @@ -3164,8 +3217,6 @@
1.142 instance nibble :: finite
1.143 by default (simp add: UNIV_nibble)
1.144
1.145 -declare UNIV_nibble [code func]
1.146 -
1.147 datatype char = Char nibble nibble
1.148 -- "Note: canonical order of character encoding coincides with standard term ordering"
1.149
1.150 @@ -3275,14 +3326,6 @@
1.151
1.152 subsubsection {* Generation of efficient code *}
1.153
1.154 -consts
1.155 - null:: "'a list \<Rightarrow> bool"
1.156 - list_inter :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
1.157 - list_ex :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
1.158 - list_all :: "('a \<Rightarrow> bool) \<Rightarrow> ('a list \<Rightarrow> bool)"
1.159 - filtermap :: "('a \<Rightarrow> 'b option) \<Rightarrow> 'a list \<Rightarrow> 'b list"
1.160 - map_filter :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'b list"
1.161 -
1.162 primrec
1.163 member :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" (infixl "mem" 55)
1.164 where
1.165 @@ -3290,34 +3333,45 @@
1.166 | "x mem (y#ys) \<longleftrightarrow> (if y = x then True else x mem ys)"
1.167
1.168 primrec
1.169 + null:: "'a list \<Rightarrow> bool"
1.170 +where
1.171 "null [] = True"
1.172 - "null (x#xs) = False"
1.173 + | "null (x#xs) = False"
1.174
1.175 primrec
1.176 + list_inter :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
1.177 +where
1.178 "list_inter [] bs = []"
1.179 - "list_inter (a#as) bs =
1.180 + | "list_inter (a#as) bs =
1.181 (if a \<in> set bs then a # list_inter as bs else list_inter as bs)"
1.182
1.183 primrec
1.184 + list_all :: "('a \<Rightarrow> bool) \<Rightarrow> ('a list \<Rightarrow> bool)"
1.185 +where
1.186 "list_all P [] = True"
1.187 - "list_all P (x#xs) = (P x \<and> list_all P xs)"
1.188 + | "list_all P (x#xs) = (P x \<and> list_all P xs)"
1.189
1.190 primrec
1.191 + list_ex :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
1.192 +where
1.193 "list_ex P [] = False"
1.194 - "list_ex P (x#xs) = (P x \<or> list_ex P xs)"
1.195 + | "list_ex P (x#xs) = (P x \<or> list_ex P xs)"
1.196
1.197 primrec
1.198 + filtermap :: "('a \<Rightarrow> 'b option) \<Rightarrow> 'a list \<Rightarrow> 'b list"
1.199 +where
1.200 "filtermap f [] = []"
1.201 - "filtermap f (x#xs) =
1.202 + | "filtermap f (x#xs) =
1.203 (case f x of None \<Rightarrow> filtermap f xs
1.204 | Some y \<Rightarrow> y # filtermap f xs)"
1.205
1.206 primrec
1.207 + map_filter :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'b list"
1.208 +where
1.209 "map_filter f P [] = []"
1.210 - "map_filter f P (x#xs) =
1.211 + | "map_filter f P (x#xs) =
1.212 (if P x then f x # map_filter f P xs else map_filter f P xs)"
1.213
1.214 -
1.215 text {*
1.216 Only use @{text mem} for generating executable code. Otherwise use
1.217 @{prop "x : set xs"} instead --- it is much easier to reason about.
1.218 @@ -3448,65 +3502,9 @@
1.219 "(\<exists>m\<le>n\<Colon>nat. P m) \<longleftrightarrow> (\<exists>m \<in> {0..n}. P m)"
1.220 by auto
1.221
1.222 -lemma setsum_set_upt_conv_listsum[code unfold]:
1.223 - "setsum f (set[k..<n]) = listsum (map f [k..<n])"
1.224 +lemma setsum_set_upt_conv_listsum [code unfold]:
1.225 + "setsum f (set [k..<n]) = listsum (map f [k..<n])"
1.226 apply(subst atLeastLessThan_upt[symmetric])
1.227 by (induct n) simp_all
1.228
1.229 -subsubsection {* List partitioning *}
1.230 -
1.231 -consts
1.232 - partition :: "('a \<Rightarrow> bool) \<Rightarrow>'a list \<Rightarrow> 'a list \<times> 'a list"
1.233 -primrec
1.234 - "partition P [] = ([], [])"
1.235 - "partition P (x # xs) =
1.236 - (let (yes, no) = partition P xs
1.237 - in if P x then (x # yes, no) else (yes, x # no))"
1.238 -
1.239 -lemma partition_P:
1.240 - "partition P xs = (yes, no) \<Longrightarrow> (\<forall>p\<in> set yes. P p) \<and> (\<forall>p\<in> set no. \<not> P p)"
1.241 -proof (induct xs arbitrary: yes no rule: partition.induct)
1.242 - case Nil then show ?case by simp
1.243 -next
1.244 - case (Cons a as)
1.245 - let ?p = "partition P as"
1.246 - let ?p' = "partition P (a # as)"
1.247 - note prem = `?p' = (yes, no)`
1.248 - show ?case
1.249 - proof (cases "P a")
1.250 - case True
1.251 - with prem have yes: "yes = a # fst ?p" and no: "no = snd ?p"
1.252 - by (simp_all add: Let_def split_def)
1.253 - have "(\<forall>p\<in> set (fst ?p). P p) \<and> (\<forall>p\<in> set no. \<not> P p)"
1.254 - by (rule Cons.hyps) (simp add: yes no)
1.255 - with True yes show ?thesis by simp
1.256 - next
1.257 - case False
1.258 - with prem have yes: "yes = fst ?p" and no: "no = a # snd ?p"
1.259 - by (simp_all add: Let_def split_def)
1.260 - have "(\<forall>p\<in> set yes. P p) \<and> (\<forall>p\<in> set (snd ?p). \<not> P p)"
1.261 - by (rule Cons.hyps) (simp add: yes no)
1.262 - with False no show ?thesis by simp
1.263 - qed
1.264 -qed
1.265 -
1.266 -lemma partition_filter1:
1.267 - "fst (partition P xs) = filter P xs"
1.268 -by (induct xs rule: partition.induct) (auto simp add: Let_def split_def)
1.269 -
1.270 -lemma partition_filter2:
1.271 - "snd (partition P xs) = filter (Not o P) xs"
1.272 -by (induct xs rule: partition.induct) (auto simp add: Let_def split_def)
1.273 -
1.274 -lemma partition_set:
1.275 - assumes "partition P xs = (yes, no)"
1.276 - shows "set yes \<union> set no = set xs"
1.277 -proof -
1.278 - have "set xs = {x. x \<in> set xs \<and> P x} \<union> {x. x \<in> set xs \<and> \<not> P x}" by blast
1.279 - also have "\<dots> = set (List.filter P xs) Un (set (List.filter (Not o P) xs))" by simp
1.280 - also have "\<dots> = set (fst (partition P xs)) \<union> set (snd (partition P xs))"
1.281 - using partition_filter1 [of P xs] partition_filter2 [of P xs] by simp
1.282 - finally show "set yes Un set no = set xs" using assms by simp
1.283 -qed
1.284 -
1.285 end