author | haftmann |

Fri Oct 14 18:55:59 2011 +0200 (2011-10-14) | |

changeset 45144 | 3f4742ce4629 |

parent 45143 | aed8f14bf562 |

child 45146 | 5465824c1c8d |

moved sublists to More_List.thy

src/HOL/Enum.thy | file | annotate | diff | revisions | |

src/HOL/Library/More_List.thy | file | annotate | diff | revisions |

1.1 --- a/src/HOL/Enum.thy Fri Oct 14 18:55:29 2011 +0200 1.2 +++ b/src/HOL/Enum.thy Fri Oct 14 18:55:59 2011 +0200 1.3 @@ -370,37 +370,6 @@ 1.4 1.5 end 1.6 1.7 -primrec sublists :: "'a list \<Rightarrow> 'a list list" where 1.8 - "sublists [] = [[]]" 1.9 - | "sublists (x#xs) = (let xss = sublists xs in map (Cons x) xss @ xss)" 1.10 - 1.11 -lemma length_sublists: 1.12 - "length (sublists xs) = Suc (Suc (0\<Colon>nat)) ^ length xs" 1.13 - by (induct xs) (simp_all add: Let_def) 1.14 - 1.15 -lemma sublists_powset: 1.16 - "set ` set (sublists xs) = Pow (set xs)" 1.17 -proof - 1.18 - have aux: "\<And>x A. set ` Cons x ` A = insert x ` set ` A" 1.19 - by (auto simp add: image_def) 1.20 - have "set (map set (sublists xs)) = Pow (set xs)" 1.21 - by (induct xs) 1.22 - (simp_all add: aux Let_def Pow_insert Un_commute comp_def del: map_map) 1.23 - then show ?thesis by simp 1.24 -qed 1.25 - 1.26 -lemma distinct_set_sublists: 1.27 - assumes "distinct xs" 1.28 - shows "distinct (map set (sublists xs))" 1.29 -proof (rule card_distinct) 1.30 - have "finite (set xs)" by rule 1.31 - then have "card (Pow (set xs)) = Suc (Suc 0) ^ card (set xs)" by (rule card_Pow) 1.32 - with assms distinct_card [of xs] 1.33 - have "card (Pow (set xs)) = Suc (Suc 0) ^ length xs" by simp 1.34 - then show "card (set (map set (sublists xs))) = length (map set (sublists xs))" 1.35 - by (simp add: sublists_powset length_sublists) 1.36 -qed 1.37 - 1.38 instantiation nibble :: enum 1.39 begin 1.40

2.1 --- a/src/HOL/Library/More_List.thy Fri Oct 14 18:55:29 2011 +0200 2.2 +++ b/src/HOL/Library/More_List.thy Fri Oct 14 18:55:59 2011 +0200 2.3 @@ -295,4 +295,37 @@ 2.4 "nth_map (Suc n) f (x # xs) = x # nth_map n f xs" 2.5 by (simp add: nth_map_def) 2.6 2.7 +text {* Enumeration of all sublists of a list *} 2.8 + 2.9 +primrec sublists :: "'a list \<Rightarrow> 'a list list" where 2.10 + "sublists [] = [[]]" 2.11 + | "sublists (x#xs) = (let xss = sublists xs in map (Cons x) xss @ xss)" 2.12 + 2.13 +lemma length_sublists: 2.14 + "length (sublists xs) = Suc (Suc (0\<Colon>nat)) ^ length xs" 2.15 + by (induct xs) (simp_all add: Let_def) 2.16 + 2.17 +lemma sublists_powset: 2.18 + "set ` set (sublists xs) = Pow (set xs)" 2.19 +proof - 2.20 + have aux: "\<And>x A. set ` Cons x ` A = insert x ` set ` A" 2.21 + by (auto simp add: image_def) 2.22 + have "set (map set (sublists xs)) = Pow (set xs)" 2.23 + by (induct xs) 2.24 + (simp_all add: aux Let_def Pow_insert Un_commute comp_def del: map_map) 2.25 + then show ?thesis by simp 2.26 +qed 2.27 + 2.28 +lemma distinct_set_sublists: 2.29 + assumes "distinct xs" 2.30 + shows "distinct (map set (sublists xs))" 2.31 +proof (rule card_distinct) 2.32 + have "finite (set xs)" by rule 2.33 + then have "card (Pow (set xs)) = Suc (Suc 0) ^ card (set xs)" by (rule card_Pow) 2.34 + with assms distinct_card [of xs] 2.35 + have "card (Pow (set xs)) = Suc (Suc 0) ^ length xs" by simp 2.36 + then show "card (set (map set (sublists xs))) = length (map set (sublists xs))" 2.37 + by (simp add: sublists_powset length_sublists) 2.38 +qed 2.39 + 2.40 end