src/HOL/Library/Dlist.thy
changeset 39380 5a2662c1e44a
parent 38857 97775f3e8722
child 39727 5dab9549c80d
     1.1 --- a/src/HOL/Library/Dlist.thy	Mon Sep 13 16:43:23 2010 +0200
     1.2 +++ b/src/HOL/Library/Dlist.thy	Mon Sep 13 16:43:23 2010 +0200
     1.3 @@ -14,18 +14,20 @@
     1.4    show "[] \<in> ?dlist" by simp
     1.5  qed
     1.6  
     1.7 -lemma dlist_ext:
     1.8 -  assumes "list_of_dlist dxs = list_of_dlist dys"
     1.9 -  shows "dxs = dys"
    1.10 -  using assms by (simp add: list_of_dlist_inject)
    1.11 +lemma dlist_eq_iff:
    1.12 +  "dxs = dys \<longleftrightarrow> list_of_dlist dxs = list_of_dlist dys"
    1.13 +  by (simp add: list_of_dlist_inject)
    1.14  
    1.15 +lemma dlist_eqI:
    1.16 +  "list_of_dlist dxs = list_of_dlist dys \<Longrightarrow> dxs = dys"
    1.17 +  by (simp add: dlist_eq_iff)
    1.18  
    1.19  text {* Formal, totalized constructor for @{typ "'a dlist"}: *}
    1.20  
    1.21  definition Dlist :: "'a list \<Rightarrow> 'a dlist" where
    1.22    "Dlist xs = Abs_dlist (remdups xs)"
    1.23  
    1.24 -lemma distinct_list_of_dlist [simp]:
    1.25 +lemma distinct_list_of_dlist [simp, intro]:
    1.26    "distinct (list_of_dlist dxs)"
    1.27    using list_of_dlist [of dxs] by simp
    1.28