summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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