tuned proofs: avoid implicit prems;
authorwenzelm
Thu Jun 14 18:33:29 2007 +0200 (2007-06-14)
changeset 2338877645da0db85
parent 23387 7cb8faa5d4d3
child 23389 aaca6a8e5414
tuned proofs: avoid implicit prems;
tuned partition proofs;
src/HOL/List.thy
     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