added equality instantiation
authorhaftmann
Wed Aug 18 11:55:27 2010 +0200 (2010-08-18)
changeset 38512ed4703b416ed
parent 38511 abf95b39d65c
child 38513 33ab01218ae1
added equality instantiation
src/HOL/Library/Dlist.thy
     1.1 --- a/src/HOL/Library/Dlist.thy	Wed Aug 18 11:18:24 2010 +0200
     1.2 +++ b/src/HOL/Library/Dlist.thy	Wed Aug 18 11:55:27 2010 +0200
     1.3 @@ -15,8 +15,8 @@
     1.4  qed
     1.5  
     1.6  lemma dlist_ext:
     1.7 -  assumes "list_of_dlist xs = list_of_dlist ys"
     1.8 -  shows "xs = ys"
     1.9 +  assumes "list_of_dlist dxs = list_of_dlist dys"
    1.10 +  shows "dxs = dys"
    1.11    using assms by (simp add: list_of_dlist_inject)
    1.12  
    1.13  
    1.14 @@ -107,6 +107,19 @@
    1.15    by simp
    1.16  
    1.17  
    1.18 +text {* Equality *}
    1.19 +
    1.20 +instantiation dlist :: (eq) eq
    1.21 +begin
    1.22 +
    1.23 +definition "HOL.eq dxs dys \<longleftrightarrow> HOL.eq (list_of_dlist dxs) (list_of_dlist dys)"
    1.24 +
    1.25 +instance proof
    1.26 +qed (simp add: eq_dlist_def eq list_of_dlist_inject)
    1.27 +
    1.28 +end
    1.29 +
    1.30 +
    1.31  section {* Induction principle and case distinction *}
    1.32  
    1.33  lemma dlist_induct [case_names empty insert, induct type: dlist]:
    1.34 @@ -283,6 +296,7 @@
    1.35  
    1.36  end
    1.37  
    1.38 +
    1.39  hide_const (open) member fold foldr empty insert remove map filter null member length fold
    1.40  
    1.41  end