author | wenzelm |

Thu Jun 14 18:33:29 2007 +0200 (2007-06-14) | |

changeset 23388 | 77645da0db85 |

parent 23387 | 7cb8faa5d4d3 |

child 23389 | aaca6a8e5414 |

tuned proofs: avoid implicit prems;

tuned partition proofs;

tuned partition proofs;

1.1 --- a/src/HOL/List.thy Thu Jun 14 13:19:50 2007 +0200 1.2 +++ b/src/HOL/List.thy Thu Jun 14 18:33:29 2007 +0200 1.3 @@ -42,7 +42,6 @@ 1.4 "distinct":: "'a list => bool" 1.5 replicate :: "nat => 'a => 'a list" 1.6 splice :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" 1.7 - partition :: "('a \<Rightarrow> bool) \<Rightarrow>'a list \<Rightarrow> (('a list) \<times> ('a list))" 1.8 allpairs :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list" 1.9 1.10 abbreviation 1.11 @@ -224,7 +223,7 @@ 1.12 "allpairs f [] ys = []" 1.13 "allpairs f (x # xs) ys = map (f x) ys @ allpairs f xs ys" 1.14 1.15 -subsubsection {* List comprehehsion *} 1.16 +subsubsection {* List comprehension *} 1.17 1.18 text{* Input syntax for Haskell-like list comprehension 1.19 notation. Typical example: @{text"[(x,y). x \<leftarrow> xs, y \<leftarrow> ys, x \<noteq> y]"}, the list of all pairs of distinct elements from @{text xs} and @{text ys}. 1.20 @@ -896,7 +895,7 @@ 1.21 hence eq: "?S' = insert 0 (Suc ` ?S)" 1.22 by(auto simp add: nth_Cons image_def split:nat.split elim:lessE) 1.23 have "length (filter p (x # xs)) = Suc(card ?S)" 1.24 - using Cons by simp 1.25 + using Cons `p x` by simp 1.26 also have "\<dots> = Suc(card(Suc ` ?S))" using fin 1.27 by (simp add: card_image inj_Suc) 1.28 also have "\<dots> = card ?S'" using eq fin 1.29 @@ -907,7 +906,7 @@ 1.30 hence eq: "?S' = Suc ` ?S" 1.31 by(auto simp add: nth_Cons image_def split:nat.split elim:lessE) 1.32 have "length (filter p (x # xs)) = card ?S" 1.33 - using Cons by simp 1.34 + using Cons `\<not> p x` by simp 1.35 also have "\<dots> = card(Suc ` ?S)" using fin 1.36 by (simp add: card_image inj_Suc) 1.37 also have "\<dots> = card ?S'" using eq fin 1.38 @@ -3053,54 +3052,61 @@ 1.39 "set (foldl (op @) [] (map f xs)) = UNION (set xs) (\<lambda>x. set (f x))" 1.40 using foldl_append_map_set[where ss="[]" and xs="xs" and f="f"] by simp 1.41 1.42 + 1.43 +subsubsection {* List partitioning *} 1.44 + 1.45 +consts 1.46 + partition :: "('a \<Rightarrow> bool) \<Rightarrow>'a list \<Rightarrow> 'a list \<times> 'a list" 1.47 primrec 1.48 -"partition P [] = ([],[])" 1.49 -"partition P (x#xs) = 1.50 - (let (yes,no) = partition P xs 1.51 - in (if (P x) then ((x#yes),no) else (yes,(x#no))))" 1.52 + "partition P [] = ([], [])" 1.53 + "partition P (x # xs) = 1.54 + (let (yes, no) = partition P xs 1.55 + in if P x then (x # yes, no) else (yes, x # no))" 1.56 1.57 lemma partition_P: 1.58 - "partition P xs = (yes,no) \<Longrightarrow> (\<forall>p\<in> set yes. P p) \<and> (\<forall>p\<in> set no. \<not> P p)" 1.59 -proof(induct xs arbitrary: yes no rule: partition.induct) 1.60 - case (Cons a as yes no) 1.61 - have "\<exists> y n. partition P as = (y,n)" by auto 1.62 - then obtain "y" "n" where yn_def: "partition P as = (y,n)" by blast 1.63 - have "P a \<or> \<not> P a" by simp 1.64 - moreover 1.65 - { assume "P a" 1.66 - hence "partition P (a#as) = (a#y,n)" 1.67 - by (auto simp add: Let_def yn_def) 1.68 - hence "yes = a#y" using prems by auto 1.69 - with prems have ?case by simp 1.70 - } 1.71 - moreover 1.72 - { assume "\<not> P a" 1.73 - hence "partition P (a#as) = (y,a#n)" 1.74 - by (auto simp add: Let_def yn_def) 1.75 - hence "no = a#n" using prems by auto 1.76 - with prems have ?case by simp 1.77 - } 1.78 - ultimately show ?case by blast 1.79 -qed simp_all 1.80 + "partition P xs = (yes, no) \<Longrightarrow> (\<forall>p\<in> set yes. P p) \<and> (\<forall>p\<in> set no. \<not> P p)" 1.81 +proof (induct xs arbitrary: yes no rule: partition.induct) 1.82 + case Nil then show ?case by simp 1.83 +next 1.84 + case (Cons a as) 1.85 + let ?p = "partition P as" 1.86 + let ?p' = "partition P (a # as)" 1.87 + note prem = `?p' = (yes, no)` 1.88 + show ?case 1.89 + proof (cases "P a") 1.90 + case True 1.91 + with prem have yes: "yes = a # fst ?p" and no: "no = snd ?p" 1.92 + by (simp_all add: Let_def split_def) 1.93 + have "(\<forall>p\<in> set (fst ?p). P p) \<and> (\<forall>p\<in> set no. \<not> P p)" 1.94 + by (rule Cons.hyps) (simp add: yes no) 1.95 + with True yes show ?thesis by simp 1.96 + next 1.97 + case False 1.98 + with prem have yes: "yes = fst ?p" and no: "no = a # snd ?p" 1.99 + by (simp_all add: Let_def split_def) 1.100 + have "(\<forall>p\<in> set yes. P p) \<and> (\<forall>p\<in> set (snd ?p). \<not> P p)" 1.101 + by (rule Cons.hyps) (simp add: yes no) 1.102 + with False no show ?thesis by simp 1.103 + qed 1.104 +qed 1.105 1.106 lemma partition_filter1: 1.107 - " fst (partition P xs) = filter P xs " 1.108 -by (induct xs rule: partition.induct) (auto simp add: Let_def split_def) 1.109 + "fst (partition P xs) = filter P xs" 1.110 + by (induct xs rule: partition.induct) (auto simp add: Let_def split_def) 1.111 1.112 lemma partition_filter2: 1.113 - "snd (partition P xs) = filter (Not o P ) xs " 1.114 -by (induct xs rule: partition.induct) (auto simp add: Let_def split_def) 1.115 - 1.116 -lemma partition_set: "partition P xs = (yes,no) \<Longrightarrow> set yes \<union> set no = set xs" 1.117 -proof- 1.118 - fix yes no 1.119 - assume A: "partition P xs = (yes,no)" 1.120 - have "set xs = {x. x \<in> set xs \<and> P x} \<union> {x. x \<in> set xs \<and> \<not> P x}" by auto 1.121 - also have "\<dots> = set (List.filter P xs) Un (set (List.filter (Not o P) xs))" by auto 1.122 - also have "\<dots> = set (fst (partition P xs)) Un set (snd (partition P xs))" 1.123 - using partition_filter1[where xs="xs" and P="P"] 1.124 - partition_filter2[where xs="xs" and P="P"] by auto 1.125 - finally show "set yes Un set no = set xs" using A by simp 1.126 + "snd (partition P xs) = filter (Not o P) xs" 1.127 + by (induct xs rule: partition.induct) (auto simp add: Let_def split_def) 1.128 + 1.129 +lemma partition_set: 1.130 + assumes "partition P xs = (yes, no)" 1.131 + shows "set yes \<union> set no = set xs" 1.132 +proof - 1.133 + have "set xs = {x. x \<in> set xs \<and> P x} \<union> {x. x \<in> set xs \<and> \<not> P x}" by blast 1.134 + also have "\<dots> = set (List.filter P xs) Un (set (List.filter (Not o P) xs))" by simp 1.135 + also have "\<dots> = set (fst (partition P xs)) \<union> set (snd (partition P xs))" 1.136 + using partition_filter1 [of P xs] partition_filter2 [of P xs] by simp 1.137 + finally show "set yes Un set no = set xs" using assms by simp 1.138 qed 1.139 1.140 -end 1.141 \ No newline at end of file 1.142 +end