added two lemmas about "distinct" to help Sledgehammer
authorblanchet
Thu Sep 01 13:18:27 2011 +0200 (2011-09-01 ago)
changeset 446353d046864ebe6
parent 44634 2ac4ff398bc3
child 44636 9a8de0397f65
added two lemmas about "distinct" to help Sledgehammer
src/HOL/List.thy
     1.1 --- a/src/HOL/List.thy	Thu Sep 01 13:18:27 2011 +0200
     1.2 +++ b/src/HOL/List.thy	Thu Sep 01 13:18:27 2011 +0200
     1.3 @@ -2929,6 +2929,14 @@
     1.4      by (induct xs' ys' rule: list_induct2) (auto elim: in_set_zipE)
     1.5  qed
     1.6  
     1.7 +(* The next two lemmas help Sledgehammer. *)
     1.8 +
     1.9 +lemma distinct_singleton: "distinct [x]" by simp
    1.10 +
    1.11 +lemma distinct_length_2_or_more:
    1.12 +"distinct (a # b # xs) \<longleftrightarrow> (a \<noteq> b \<and> distinct (a # xs) \<and> distinct (b # xs))"
    1.13 +by (metis distinct.simps(2) hd.simps hd_in_set list.simps(2) set_ConsD set_rev_mp set_subset_Cons)
    1.14 +
    1.15  
    1.16  subsubsection {* List summation: @{const listsum} and @{text"\<Sum>"}*}
    1.17