summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | haftmann |

Thu, 27 Mar 2008 19:04:36 +0100 | |

changeset 26442 | 57fb6a8b099e |

parent 26441 | 7914697ff104 |

child 26443 | cae9fa186541 |

restructuring; explicit case names for rule list_induct2

src/HOL/List.thy | file | annotate | diff | comparison | revisions |

--- a/src/HOL/List.thy Thu Mar 27 19:04:35 2008 +0100 +++ b/src/HOL/List.thy Thu Mar 27 19:04:36 2008 +0100 @@ -418,17 +418,26 @@ lemma impossible_Cons: "length xs <= length ys ==> xs = x # ys = False" by (induct xs) auto -lemma list_induct2 [consumes 1]: - "\<lbrakk> length xs = length ys; - P [] []; - \<And>x xs y ys. \<lbrakk> length xs = length ys; P xs ys \<rbrakk> \<Longrightarrow> P (x#xs) (y#ys) \<rbrakk> - \<Longrightarrow> P xs ys" -apply(induct xs arbitrary: ys) - apply simp -apply(case_tac ys) - apply simp -apply simp -done +lemma list_induct2 [consumes 1, case_names Nil Cons]: + "length xs = length ys \<Longrightarrow> P [] [] \<Longrightarrow> + (\<And>x xs y ys. length xs = length ys \<Longrightarrow> P xs ys \<Longrightarrow> P (x#xs) (y#ys)) + \<Longrightarrow> P xs ys" +proof (induct xs arbitrary: ys) + case Nil then show ?case by simp +next + case (Cons x xs ys) then show ?case by (cases ys) simp_all +qed + +lemma list_induct3 [consumes 2, case_names Nil Cons]: + "length xs = length ys \<Longrightarrow> length ys = length zs \<Longrightarrow> P [] [] [] \<Longrightarrow> + (\<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)) + \<Longrightarrow> P xs ys zs" +proof (induct xs arbitrary: ys zs) + case Nil then show ?case by simp +next + case (Cons x xs ys zs) then show ?case by (cases ys, simp_all) + (cases zs, simp_all) +qed lemma list_induct2': "\<lbrakk> P [] []; @@ -951,6 +960,9 @@ lemma card_length: "card (set xs) \<le> length xs" by (induct xs) (auto simp add: card_insert_if) +lemma set_minus_filter_out: + "set xs - {y} = set (filter (\<lambda>x. \<not> (x = y)) xs)" + by (induct xs) auto subsubsection {* @{text filter} *} @@ -1092,6 +1104,41 @@ by (induct ys) simp_all +subsubsection {* List partitioning *} + +primrec partition :: "('a \<Rightarrow> bool) \<Rightarrow>'a list \<Rightarrow> 'a list \<times> 'a list" where + "partition P [] = ([], [])" + | "partition P (x # xs) = + (let (yes, no) = partition P xs + in if P x then (x # yes, no) else (yes, x # no))" + +lemma partition_filter1: + "fst (partition P xs) = filter P xs" +by (induct xs) (auto simp add: Let_def split_def) + +lemma partition_filter2: + "snd (partition P xs) = filter (Not o P) xs" +by (induct xs) (auto simp add: Let_def split_def) + +lemma partition_P: + assumes "partition P xs = (yes, no)" + shows "(\<forall>p \<in> set yes. P p) \<and> (\<forall>p \<in> set no. \<not> P p)" +proof - + from assms have "yes = fst (partition P xs)" and "no = snd (partition P xs)" + by simp_all + then show ?thesis by (simp_all add: partition_filter1 partition_filter2) +qed + +lemma partition_set: + assumes "partition P xs = (yes, no)" + shows "set yes \<union> set no = set xs" +proof - + from assms have "yes = fst (partition P xs)" and "no = snd (partition P xs)" + by simp_all + then show ?thesis by (auto simp add: partition_filter1 partition_filter2) +qed + + subsubsection {* @{text concat} *} lemma concat_append [simp]: "concat (xs @ ys) = concat xs @ concat ys" @@ -1966,17 +2013,19 @@ subsubsection {* List summation: @{const listsum} and @{text"\<Sum>"}*} -lemma listsum_append[simp]: "listsum (xs @ ys) = listsum xs + listsum ys" +lemma listsum_append [simp]: "listsum (xs @ ys) = listsum xs + listsum ys" by (induct xs) (simp_all add:add_assoc) -lemma listsum_rev[simp]: -fixes xs :: "'a::comm_monoid_add list" -shows "listsum (rev xs) = listsum xs" +lemma listsum_rev [simp]: + fixes xs :: "'a\<Colon>comm_monoid_add list" + shows "listsum (rev xs) = listsum xs" by (induct xs) (simp_all add:add_ac) -lemma listsum_foldr: - "listsum xs = foldr (op +) xs 0" -by(induct xs) auto +lemma listsum_foldr: "listsum xs = foldr (op +) xs 0" +by (induct xs) auto + +lemma length_concat: "length (concat xss) = listsum (map length xss)" +by (induct xss) simp_all text{* For efficient code generation --- @{const listsum} is not tail recursive but @{const foldl} is. *} @@ -1997,13 +2046,17 @@ "SUM x<-xs. b" == "CONST listsum (map (%x. b) xs)" "\<Sum>x\<leftarrow>xs. b" == "CONST listsum (map (%x. b) xs)" +lemma listsum_triv: "(\<Sum>x\<leftarrow>xs. r) = of_nat (length xs) * r" + by (induct xs) (simp_all add: left_distrib) + lemma listsum_0 [simp]: "(\<Sum>x\<leftarrow>xs. 0) = 0" -by (induct xs) simp_all + by (induct xs) (simp_all add: left_distrib) text{* For non-Abelian groups @{text xs} needs to be reversed on one side: *} lemma uminus_listsum_map: - "- listsum (map f xs) = (listsum (map (uminus o f) xs) :: 'a::ab_group_add)" -by(induct xs) simp_all + fixes f :: "'a \<Rightarrow> 'b\<Colon>ab_group_add" + shows "- listsum (map f xs) = (listsum (map (uminus o f) xs))" +by (induct xs) simp_all subsubsection {* @{text upt} *} @@ -3164,8 +3217,6 @@ instance nibble :: finite by default (simp add: UNIV_nibble) -declare UNIV_nibble [code func] - datatype char = Char nibble nibble -- "Note: canonical order of character encoding coincides with standard term ordering" @@ -3275,14 +3326,6 @@ subsubsection {* Generation of efficient code *} -consts - null:: "'a list \<Rightarrow> bool" - list_inter :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" - list_ex :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" - list_all :: "('a \<Rightarrow> bool) \<Rightarrow> ('a list \<Rightarrow> bool)" - filtermap :: "('a \<Rightarrow> 'b option) \<Rightarrow> 'a list \<Rightarrow> 'b list" - map_filter :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'b list" - primrec member :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" (infixl "mem" 55) where @@ -3290,34 +3333,45 @@ | "x mem (y#ys) \<longleftrightarrow> (if y = x then True else x mem ys)" primrec + null:: "'a list \<Rightarrow> bool" +where "null [] = True" - "null (x#xs) = False" + | "null (x#xs) = False" primrec + list_inter :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" +where "list_inter [] bs = []" - "list_inter (a#as) bs = + | "list_inter (a#as) bs = (if a \<in> set bs then a # list_inter as bs else list_inter as bs)" primrec + list_all :: "('a \<Rightarrow> bool) \<Rightarrow> ('a list \<Rightarrow> bool)" +where "list_all P [] = True" - "list_all P (x#xs) = (P x \<and> list_all P xs)" + | "list_all P (x#xs) = (P x \<and> list_all P xs)" primrec + list_ex :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" +where "list_ex P [] = False" - "list_ex P (x#xs) = (P x \<or> list_ex P xs)" + | "list_ex P (x#xs) = (P x \<or> list_ex P xs)" primrec + filtermap :: "('a \<Rightarrow> 'b option) \<Rightarrow> 'a list \<Rightarrow> 'b list" +where "filtermap f [] = []" - "filtermap f (x#xs) = + | "filtermap f (x#xs) = (case f x of None \<Rightarrow> filtermap f xs | Some y \<Rightarrow> y # filtermap f xs)" primrec + map_filter :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'b list" +where "map_filter f P [] = []" - "map_filter f P (x#xs) = + | "map_filter f P (x#xs) = (if P x then f x # map_filter f P xs else map_filter f P xs)" - text {* Only use @{text mem} for generating executable code. Otherwise use @{prop "x : set xs"} instead --- it is much easier to reason about. @@ -3448,65 +3502,9 @@ "(\<exists>m\<le>n\<Colon>nat. P m) \<longleftrightarrow> (\<exists>m \<in> {0..n}. P m)" by auto -lemma setsum_set_upt_conv_listsum[code unfold]: - "setsum f (set[k..<n]) = listsum (map f [k..<n])" +lemma setsum_set_upt_conv_listsum [code unfold]: + "setsum f (set [k..<n]) = listsum (map f [k..<n])" apply(subst atLeastLessThan_upt[symmetric]) by (induct n) simp_all -subsubsection {* List partitioning *} - -consts - partition :: "('a \<Rightarrow> bool) \<Rightarrow>'a list \<Rightarrow> 'a list \<times> 'a list" -primrec - "partition P [] = ([], [])" - "partition P (x # xs) = - (let (yes, no) = partition P xs - in if P x then (x # yes, no) else (yes, x # no))" - -lemma partition_P: - "partition P xs = (yes, no) \<Longrightarrow> (\<forall>p\<in> set yes. P p) \<and> (\<forall>p\<in> set no. \<not> P p)" -proof (induct xs arbitrary: yes no rule: partition.induct) - case Nil then show ?case by simp -next - case (Cons a as) - let ?p = "partition P as" - let ?p' = "partition P (a # as)" - note prem = `?p' = (yes, no)` - show ?case - proof (cases "P a") - case True - with prem have yes: "yes = a # fst ?p" and no: "no = snd ?p" - by (simp_all add: Let_def split_def) - have "(\<forall>p\<in> set (fst ?p). P p) \<and> (\<forall>p\<in> set no. \<not> P p)" - by (rule Cons.hyps) (simp add: yes no) - with True yes show ?thesis by simp - next - case False - with prem have yes: "yes = fst ?p" and no: "no = a # snd ?p" - by (simp_all add: Let_def split_def) - have "(\<forall>p\<in> set yes. P p) \<and> (\<forall>p\<in> set (snd ?p). \<not> P p)" - by (rule Cons.hyps) (simp add: yes no) - with False no show ?thesis by simp - qed -qed - -lemma partition_filter1: - "fst (partition P xs) = filter P xs" -by (induct xs rule: partition.induct) (auto simp add: Let_def split_def) - -lemma partition_filter2: - "snd (partition P xs) = filter (Not o P) xs" -by (induct xs rule: partition.induct) (auto simp add: Let_def split_def) - -lemma partition_set: - assumes "partition P xs = (yes, no)" - shows "set yes \<union> set no = set xs" -proof - - have "set xs = {x. x \<in> set xs \<and> P x} \<union> {x. x \<in> set xs \<and> \<not> P x}" by blast - also have "\<dots> = set (List.filter P xs) Un (set (List.filter (Not o P) xs))" by simp - also have "\<dots> = set (fst (partition P xs)) \<union> set (snd (partition P xs))" - using partition_filter1 [of P xs] partition_filter2 [of P xs] by simp - finally show "set yes Un set no = set xs" using assms by simp -qed - end