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

author | nipkow |

Mon, 10 Sep 2007 19:21:03 +0200 | |

changeset 24566 | 2bfa0215904c |

parent 24565 | 08578e380a41 |

child 24567 | 4970fb01aa01 |

added lemma

src/HOL/List.thy | file | annotate | diff | comparison | revisions |

--- a/src/HOL/List.thy Mon Sep 10 16:09:01 2007 +0200 +++ b/src/HOL/List.thy Mon Sep 10 19:21:03 2007 +0200 @@ -2030,6 +2030,15 @@ lemma distinct_remdups [iff]: "distinct (remdups xs)" by (induct xs) auto +lemma finite_distinct_list: "finite A \<Longrightarrow> EX xs. set xs = A & distinct xs" +proof - + assume "finite A" + then obtain xs where "set xs = A" by(auto dest!:finite_list) + hence "set(remdups xs) = A & distinct(remdups xs)" by simp + thus ?thesis .. +qed +(* by (metis distinct_remdups finite_list set_remdups) *) + lemma remdups_eq_nil_iff [simp]: "(remdups x = []) = (x = [])" by (induct x, auto)