summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | haftmann |

Sat, 24 Dec 2011 15:53:11 +0100 | |

changeset 45973 | 204f34a99ceb |

parent 45972 | deda685ba210 |

child 45974 | 2b043ed911ac |

moved `sublists` to theory Enum

--- a/src/HOL/Library/More_List.thy Sat Dec 24 15:53:11 2011 +0100 +++ b/src/HOL/Library/More_List.thy Sat Dec 24 15:53:11 2011 +0100 @@ -1,4 +1,4 @@ -(* Author: Florian Haftmann, TU Muenchen *) +(* Author: Florian Haftmann, TU Muenchen *) header {* Operations on lists beyond the standard List theory *} @@ -299,40 +299,6 @@ by (simp add: nth_map_def) -text {* Enumeration of all sublists of a list *} - -primrec sublists :: "'a list \<Rightarrow> 'a list list" where - "sublists [] = [[]]" - | "sublists (x#xs) = (let xss = sublists xs in map (Cons x) xss @ xss)" - -lemma length_sublists: - "length (sublists xs) = Suc (Suc (0\<Colon>nat)) ^ length xs" - by (induct xs) (simp_all add: Let_def) - -lemma sublists_powset: - "set ` set (sublists xs) = Pow (set xs)" -proof - - have aux: "\<And>x A. set ` Cons x ` A = insert x ` set ` A" - by (auto simp add: image_def) - have "set (map set (sublists xs)) = Pow (set xs)" - by (induct xs) - (simp_all add: aux Let_def Pow_insert Un_commute comp_def del: map_map) - then show ?thesis by simp -qed - -lemma distinct_set_sublists: - assumes "distinct xs" - shows "distinct (map set (sublists xs))" -proof (rule card_distinct) - have "finite (set xs)" by rule - then have "card (Pow (set xs)) = Suc (Suc 0) ^ card (set xs)" by (rule card_Pow) - with assms distinct_card [of xs] - have "card (Pow (set xs)) = Suc (Suc 0) ^ length xs" by simp - then show "card (set (map set (sublists xs))) = length (map set (sublists xs))" - by (simp add: sublists_powset length_sublists) -qed - - text {* monad operation *} definition bind :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b list) \<Rightarrow> 'b list" where