# 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 \<Rightarrow> 'a list \<Rightarrow> 'a list"
-  partition :: "('a \<Rightarrow> bool) \<Rightarrow>'a list \<Rightarrow> (('a list) \<times> ('a list))"
   allpairs :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> '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 \<leftarrow> xs, y \<leftarrow> ys, x \<noteq> 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 "\<dots> = Suc(card(Suc ` ?S))" using fin
       by (simp add: card_image inj_Suc)
     also have "\<dots> = 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 `\<not> p x` by simp
     also have "\<dots> = card(Suc ` ?S)" using fin
       by (simp add: card_image inj_Suc)
     also have "\<dots> = card ?S'" using eq fin
@@ -3053,54 +3052,61 @@
   "set (foldl (op @) [] (map f xs)) = UNION (set xs) (\<lambda>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 \<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))))"
+  "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 (Cons a as yes no)
-  have "\<exists> 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 \<or> \<not> 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 "\<not> 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) \<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)
+    "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) \<Longrightarrow> set yes \<union> set no = set xs"
-proof-
-  fix yes no
-  assume A: "partition P xs = (yes,no)"
-  have "set xs = {x. x \<in> set xs \<and> P x} \<union> {x. x \<in> set xs \<and> \<not> P x}" by auto
-  also have "\<dots> = set (List.filter P xs) Un (set (List.filter (Not o P) xs))" by auto
-  also have "\<dots> = 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 \<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
\ No newline at end of file
+end