extensionality rule fset_eqI
authorhaftmann
Mon Jun 21 09:06:14 2010 +0200 (2010-06-21)
changeset 37473013f78aed840
parent 37472 de4a8298c6f3
child 37474 ce943f9edf5e
extensionality rule fset_eqI
src/HOL/Library/Dlist.thy
src/HOL/Library/Fset.thy
     1.1 --- a/src/HOL/Library/Dlist.thy	Sun Jun 20 22:01:22 2010 +0200
     1.2 +++ b/src/HOL/Library/Dlist.thy	Mon Jun 21 09:06:14 2010 +0200
     1.3 @@ -3,7 +3,7 @@
     1.4  header {* Lists with elements distinct as canonical example for datatype invariants *}
     1.5  
     1.6  theory Dlist
     1.7 -imports Main More_List Fset
     1.8 +imports Main Fset
     1.9  begin
    1.10  
    1.11  section {* The type of distinct lists *}
    1.12 @@ -181,11 +181,11 @@
    1.13  
    1.14  lemma Set_Dlist [simp]:
    1.15    "Set (Dlist xs) = Fset (set xs)"
    1.16 -  by (simp add: Set_def Fset.Set_def)
    1.17 +  by (rule fset_eqI) (simp add: Set_def)
    1.18  
    1.19  lemma Coset_Dlist [simp]:
    1.20    "Coset (Dlist xs) = Fset (- set xs)"
    1.21 -  by (simp add: Coset_def Fset.Coset_def)
    1.22 +  by (rule fset_eqI) (simp add: Coset_def)
    1.23  
    1.24  lemma member_Set [simp]:
    1.25    "Fset.member (Set dxs) = List.member (list_of_dlist dxs)"
    1.26 @@ -197,11 +197,11 @@
    1.27  
    1.28  lemma Set_dlist_of_list [code]:
    1.29    "Fset.Set xs = Set (dlist_of_list xs)"
    1.30 -  by simp
    1.31 +  by (rule fset_eqI) simp
    1.32  
    1.33  lemma Coset_dlist_of_list [code]:
    1.34    "Fset.Coset xs = Coset (dlist_of_list xs)"
    1.35 -  by simp
    1.36 +  by (rule fset_eqI) simp
    1.37  
    1.38  lemma is_empty_Set [code]:
    1.39    "Fset.is_empty (Set dxs) \<longleftrightarrow> null dxs"
    1.40 @@ -233,15 +233,15 @@
    1.41  lemma compl_code [code]:
    1.42    "- Set dxs = Coset dxs"
    1.43    "- Coset dxs = Set dxs"
    1.44 -  by (simp_all add: not_set_compl member_set)
    1.45 +  by (rule fset_eqI, simp add: member_set not_set_compl)+
    1.46  
    1.47  lemma map_code [code]:
    1.48    "Fset.map f (Set dxs) = Set (map f dxs)"
    1.49 -  by (simp add: member_set)
    1.50 +  by (rule fset_eqI) (simp add: member_set)
    1.51    
    1.52  lemma filter_code [code]:
    1.53    "Fset.filter f (Set dxs) = Set (filter f dxs)"
    1.54 -  by (simp add: member_set)
    1.55 +  by (rule fset_eqI) (simp add: member_set)
    1.56  
    1.57  lemma forall_Set [code]:
    1.58    "Fset.forall P (Set xs) \<longleftrightarrow> list_all P (list_of_dlist xs)"
     2.1 --- a/src/HOL/Library/Fset.thy	Sun Jun 20 22:01:22 2010 +0200
     2.2 +++ b/src/HOL/Library/Fset.thy	Mon Jun 21 09:06:14 2010 +0200
     2.3 @@ -26,6 +26,10 @@
     2.4    "Fset A = Fset B \<longleftrightarrow> A = B"
     2.5    by (simp add: Fset_inject)
     2.6  
     2.7 +lemma fset_eqI:
     2.8 +  "member A = member B \<Longrightarrow> A = B"
     2.9 +  by simp
    2.10 +
    2.11  declare mem_def [simp]
    2.12  
    2.13  definition Set :: "'a list \<Rightarrow> 'a fset" where