# HG changeset patch # User wenzelm # Date 1181838809 -7200 # Node ID 77645da0db85b3949c73b34f4b56c10a9b7342c3 # Parent 7cb8faa5d4d3d5d7a779d06b36f80c9867a0a5a5 tuned proofs: avoid implicit prems; tuned partition proofs; diff -r 7cb8faa5d4d3 -r 77645da0db85 src/HOL/List.thy --- a/src/HOL/List.thy Thu Jun 14 13:19:50 2007 +0200 +++ b/src/HOL/List.thy Thu Jun 14 18:33:29 2007 +0200 @@ -42,7 +42,6 @@ "distinct":: "'a list => bool" replicate :: "nat => 'a => 'a list" splice :: "'a list \ 'a list \ 'a list" - partition :: "('a \ bool) \'a list \ (('a list) \ ('a list))" allpairs :: "('a \ 'b \ 'c) \ 'a list \ 'b list \ 'c list" abbreviation @@ -224,7 +223,7 @@ "allpairs f [] ys = []" "allpairs f (x # xs) ys = map (f x) ys @ allpairs f xs ys" -subsubsection {* List comprehehsion *} +subsubsection {* List comprehension *} text{* Input syntax for Haskell-like list comprehension notation. Typical example: @{text"[(x,y). x \ xs, y \ ys, x \ y]"}, the list of all pairs of distinct elements from @{text xs} and @{text ys}. @@ -896,7 +895,7 @@ hence eq: "?S' = insert 0 (Suc ` ?S)" by(auto simp add: nth_Cons image_def split:nat.split elim:lessE) have "length (filter p (x # xs)) = Suc(card ?S)" - using Cons by simp + using Cons `p x` by simp also have "\ = Suc(card(Suc ` ?S))" using fin by (simp add: card_image inj_Suc) also have "\ = card ?S'" using eq fin @@ -907,7 +906,7 @@ hence eq: "?S' = Suc ` ?S" by(auto simp add: nth_Cons image_def split:nat.split elim:lessE) have "length (filter p (x # xs)) = card ?S" - using Cons by simp + using Cons `\ p x` by simp also have "\ = card(Suc ` ?S)" using fin by (simp add: card_image inj_Suc) also have "\ = card ?S'" using eq fin @@ -3053,54 +3052,61 @@ "set (foldl (op @) [] (map f xs)) = UNION (set xs) (\x. set (f x))" using foldl_append_map_set[where ss="[]" and xs="xs" and f="f"] by simp + +subsubsection {* List partitioning *} + +consts + partition :: "('a \ bool) \'a list \ 'a list \ '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))))" + "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) \ (\p\ set yes. P p) \ (\p\ set no. \ P p)" -proof(induct xs arbitrary: yes no rule: partition.induct) - case (Cons a as yes no) - have "\ y n. partition P as = (y,n)" by auto - then obtain "y" "n" where yn_def: "partition P as = (y,n)" by blast - have "P a \ \ P a" by simp - moreover - { assume "P a" - hence "partition P (a#as) = (a#y,n)" - by (auto simp add: Let_def yn_def) - hence "yes = a#y" using prems by auto - with prems have ?case by simp - } - moreover - { assume "\ P a" - hence "partition P (a#as) = (y,a#n)" - by (auto simp add: Let_def yn_def) - hence "no = a#n" using prems by auto - with prems have ?case by simp - } - ultimately show ?case by blast -qed simp_all + "partition P xs = (yes, no) \ (\p\ set yes. P p) \ (\p\ set no. \ 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 "(\p\ set (fst ?p). P p) \ (\p\ set no. \ 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 "(\p\ set yes. P p) \ (\p\ set (snd ?p). \ 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) + "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: "partition P xs = (yes,no) \ set yes \ set no = set xs" -proof- - fix yes no - assume A: "partition P xs = (yes,no)" - have "set xs = {x. x \ set xs \ P x} \ {x. x \ set xs \ \ P x}" by auto - also have "\ = set (List.filter P xs) Un (set (List.filter (Not o P) xs))" by auto - also have "\ = set (fst (partition P xs)) Un set (snd (partition P xs))" - using partition_filter1[where xs="xs" and P="P"] - partition_filter2[where xs="xs" and P="P"] by auto - finally show "set yes Un set no = set xs" using A by simp + "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 \ set no = set xs" +proof - + have "set xs = {x. x \ set xs \ P x} \ {x. x \ set xs \ \ P x}" by blast + also have "\ = set (List.filter P xs) Un (set (List.filter (Not o P) xs))" by simp + also have "\ = set (fst (partition P xs)) \ 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 \ No newline at end of file +end