# HG changeset patch # User haftmann # Date 1277103974 -7200 # Node ID 013f78aed840cf2fa1a3070a915ad507a94c7c86 # Parent de4a8298c6f327ae3535cbf20687f243e4b7a3c8 extensionality rule fset_eqI diff -r de4a8298c6f3 -r 013f78aed840 src/HOL/Library/Dlist.thy --- a/src/HOL/Library/Dlist.thy Sun Jun 20 22:01:22 2010 +0200 +++ b/src/HOL/Library/Dlist.thy Mon Jun 21 09:06:14 2010 +0200 @@ -3,7 +3,7 @@ header {* Lists with elements distinct as canonical example for datatype invariants *} theory Dlist -imports Main More_List Fset +imports Main Fset begin section {* The type of distinct lists *} @@ -181,11 +181,11 @@ lemma Set_Dlist [simp]: "Set (Dlist xs) = Fset (set xs)" - by (simp add: Set_def Fset.Set_def) + by (rule fset_eqI) (simp add: Set_def) lemma Coset_Dlist [simp]: "Coset (Dlist xs) = Fset (- set xs)" - by (simp add: Coset_def Fset.Coset_def) + by (rule fset_eqI) (simp add: Coset_def) lemma member_Set [simp]: "Fset.member (Set dxs) = List.member (list_of_dlist dxs)" @@ -197,11 +197,11 @@ lemma Set_dlist_of_list [code]: "Fset.Set xs = Set (dlist_of_list xs)" - by simp + by (rule fset_eqI) simp lemma Coset_dlist_of_list [code]: "Fset.Coset xs = Coset (dlist_of_list xs)" - by simp + by (rule fset_eqI) simp lemma is_empty_Set [code]: "Fset.is_empty (Set dxs) \ null dxs" @@ -233,15 +233,15 @@ lemma compl_code [code]: "- Set dxs = Coset dxs" "- Coset dxs = Set dxs" - by (simp_all add: not_set_compl member_set) + by (rule fset_eqI, simp add: member_set not_set_compl)+ lemma map_code [code]: "Fset.map f (Set dxs) = Set (map f dxs)" - by (simp add: member_set) + by (rule fset_eqI) (simp add: member_set) lemma filter_code [code]: "Fset.filter f (Set dxs) = Set (filter f dxs)" - by (simp add: member_set) + by (rule fset_eqI) (simp add: member_set) lemma forall_Set [code]: "Fset.forall P (Set xs) \ list_all P (list_of_dlist xs)" diff -r de4a8298c6f3 -r 013f78aed840 src/HOL/Library/Fset.thy --- a/src/HOL/Library/Fset.thy Sun Jun 20 22:01:22 2010 +0200 +++ b/src/HOL/Library/Fset.thy Mon Jun 21 09:06:14 2010 +0200 @@ -26,6 +26,10 @@ "Fset A = Fset B \ A = B" by (simp add: Fset_inject) +lemma fset_eqI: + "member A = member B \ A = B" + by simp + declare mem_def [simp] definition Set :: "'a list \ 'a fset" where