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;
 src/HOL/List.thy file | annotate | diff | revisions
```     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
```