equal
deleted
inserted
replaced
1477 done |
1477 done |
1478 |
1478 |
1479 lemma distinct_filter [simp]: "distinct xs ==> distinct (filter P xs)" |
1479 lemma distinct_filter [simp]: "distinct xs ==> distinct (filter P xs)" |
1480 by (induct xs) auto |
1480 by (induct xs) auto |
1481 |
1481 |
|
1482 lemma distinct_map_filterI: |
|
1483 "distinct(map f xs) \<Longrightarrow> distinct(map f (filter P xs))" |
|
1484 apply(induct xs) |
|
1485 apply simp |
|
1486 apply force |
|
1487 done |
|
1488 |
1482 text {* |
1489 text {* |
1483 It is best to avoid this indexed version of distinct, but sometimes |
1490 It is best to avoid this indexed version of distinct, but sometimes |
1484 it is useful. *} |
1491 it is useful. *} |
1485 lemma distinct_conv_nth: |
1492 lemma distinct_conv_nth: |
1486 "distinct xs = (\<forall>i j. i < size xs \<and> j < size xs \<and> i \<noteq> j --> xs!i \<noteq> xs!j)" |
1493 "distinct xs = (\<forall>i j. i < size xs \<and> j < size xs \<and> i \<noteq> j --> xs!i \<noteq> xs!j)" |