src/HOL/Library/Dlist.thy
changeset 40672 abd4e7358847
parent 40603 963ee2331d20
child 40968 a6fcd305f7dc
     1.1 --- a/src/HOL/Library/Dlist.thy	Mon Nov 22 09:37:39 2010 +0100
     1.2 +++ b/src/HOL/Library/Dlist.thy	Mon Nov 22 17:46:51 2010 +0100
     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 Fset
     1.8 +imports Main Cset
     1.9  begin
    1.10  
    1.11  section {* The type of distinct lists *}
    1.12 @@ -181,27 +181,27 @@
    1.13  
    1.14  section {* Implementation of sets by distinct lists -- canonical! *}
    1.15  
    1.16 -definition Set :: "'a dlist \<Rightarrow> 'a fset" where
    1.17 -  "Set dxs = Fset.Set (list_of_dlist dxs)"
    1.18 +definition Set :: "'a dlist \<Rightarrow> 'a Cset.set" where
    1.19 +  "Set dxs = Cset.set (list_of_dlist dxs)"
    1.20  
    1.21 -definition Coset :: "'a dlist \<Rightarrow> 'a fset" where
    1.22 -  "Coset dxs = Fset.Coset (list_of_dlist dxs)"
    1.23 +definition Coset :: "'a dlist \<Rightarrow> 'a Cset.set" where
    1.24 +  "Coset dxs = Cset.coset (list_of_dlist dxs)"
    1.25  
    1.26  code_datatype Set Coset
    1.27  
    1.28  declare member_code [code del]
    1.29 -declare is_empty_Set [code del]
    1.30 -declare empty_Set [code del]
    1.31 -declare UNIV_Set [code del]
    1.32 -declare insert_Set [code del]
    1.33 -declare remove_Set [code del]
    1.34 -declare compl_Set [code del]
    1.35 -declare compl_Coset [code del]
    1.36 -declare map_Set [code del]
    1.37 -declare filter_Set [code del]
    1.38 -declare forall_Set [code del]
    1.39 -declare exists_Set [code del]
    1.40 -declare card_Set [code del]
    1.41 +declare Cset.is_empty_set [code del]
    1.42 +declare Cset.empty_set [code del]
    1.43 +declare Cset.UNIV_set [code del]
    1.44 +declare insert_set [code del]
    1.45 +declare remove_set [code del]
    1.46 +declare compl_set [code del]
    1.47 +declare compl_coset [code del]
    1.48 +declare map_set [code del]
    1.49 +declare filter_set [code del]
    1.50 +declare forall_set [code del]
    1.51 +declare exists_set [code del]
    1.52 +declare card_set [code del]
    1.53  declare inter_project [code del]
    1.54  declare subtract_remove [code del]
    1.55  declare union_insert [code del]
    1.56 @@ -209,31 +209,31 @@
    1.57  declare Supremum_sup [code del]
    1.58  
    1.59  lemma Set_Dlist [simp]:
    1.60 -  "Set (Dlist xs) = Fset (set xs)"
    1.61 -  by (rule fset_eqI) (simp add: Set_def)
    1.62 +  "Set (Dlist xs) = Cset.Set (set xs)"
    1.63 +  by (rule Cset.set_eqI) (simp add: Set_def)
    1.64  
    1.65  lemma Coset_Dlist [simp]:
    1.66 -  "Coset (Dlist xs) = Fset (- set xs)"
    1.67 -  by (rule fset_eqI) (simp add: Coset_def)
    1.68 +  "Coset (Dlist xs) = Cset.Set (- set xs)"
    1.69 +  by (rule Cset.set_eqI) (simp add: Coset_def)
    1.70  
    1.71  lemma member_Set [simp]:
    1.72 -  "Fset.member (Set dxs) = List.member (list_of_dlist dxs)"
    1.73 +  "Cset.member (Set dxs) = List.member (list_of_dlist dxs)"
    1.74    by (simp add: Set_def member_set)
    1.75  
    1.76  lemma member_Coset [simp]:
    1.77 -  "Fset.member (Coset dxs) = Not \<circ> List.member (list_of_dlist dxs)"
    1.78 +  "Cset.member (Coset dxs) = Not \<circ> List.member (list_of_dlist dxs)"
    1.79    by (simp add: Coset_def member_set not_set_compl)
    1.80  
    1.81  lemma Set_dlist_of_list [code]:
    1.82 -  "Fset.Set xs = Set (dlist_of_list xs)"
    1.83 -  by (rule fset_eqI) simp
    1.84 +  "Cset.set xs = Set (dlist_of_list xs)"
    1.85 +  by (rule Cset.set_eqI) simp
    1.86  
    1.87  lemma Coset_dlist_of_list [code]:
    1.88 -  "Fset.Coset xs = Coset (dlist_of_list xs)"
    1.89 -  by (rule fset_eqI) simp
    1.90 +  "Cset.coset xs = Coset (dlist_of_list xs)"
    1.91 +  by (rule Cset.set_eqI) simp
    1.92  
    1.93  lemma is_empty_Set [code]:
    1.94 -  "Fset.is_empty (Set dxs) \<longleftrightarrow> null dxs"
    1.95 +  "Cset.is_empty (Set dxs) \<longleftrightarrow> null dxs"
    1.96    by (simp add: null_def List.null_def member_set)
    1.97  
    1.98  lemma bot_code [code]:
    1.99 @@ -245,58 +245,58 @@
   1.100    by (simp add: empty_def)
   1.101  
   1.102  lemma insert_code [code]:
   1.103 -  "Fset.insert x (Set dxs) = Set (insert x dxs)"
   1.104 -  "Fset.insert x (Coset dxs) = Coset (remove x dxs)"
   1.105 +  "Cset.insert x (Set dxs) = Set (insert x dxs)"
   1.106 +  "Cset.insert x (Coset dxs) = Coset (remove x dxs)"
   1.107    by (simp_all add: insert_def remove_def member_set not_set_compl)
   1.108  
   1.109  lemma remove_code [code]:
   1.110 -  "Fset.remove x (Set dxs) = Set (remove x dxs)"
   1.111 -  "Fset.remove x (Coset dxs) = Coset (insert x dxs)"
   1.112 +  "Cset.remove x (Set dxs) = Set (remove x dxs)"
   1.113 +  "Cset.remove x (Coset dxs) = Coset (insert x dxs)"
   1.114    by (auto simp add: insert_def remove_def member_set not_set_compl)
   1.115  
   1.116  lemma member_code [code]:
   1.117 -  "Fset.member (Set dxs) = member dxs"
   1.118 -  "Fset.member (Coset dxs) = Not \<circ> member dxs"
   1.119 +  "Cset.member (Set dxs) = member dxs"
   1.120 +  "Cset.member (Coset dxs) = Not \<circ> member dxs"
   1.121    by (simp_all add: member_def)
   1.122  
   1.123  lemma compl_code [code]:
   1.124    "- Set dxs = Coset dxs"
   1.125    "- Coset dxs = Set dxs"
   1.126 -  by (rule fset_eqI, simp add: member_set not_set_compl)+
   1.127 +  by (rule Cset.set_eqI, simp add: member_set not_set_compl)+
   1.128  
   1.129  lemma map_code [code]:
   1.130 -  "Fset.map f (Set dxs) = Set (map f dxs)"
   1.131 -  by (rule fset_eqI) (simp add: member_set)
   1.132 +  "Cset.map f (Set dxs) = Set (map f dxs)"
   1.133 +  by (rule Cset.set_eqI) (simp add: member_set)
   1.134    
   1.135  lemma filter_code [code]:
   1.136 -  "Fset.filter f (Set dxs) = Set (filter f dxs)"
   1.137 -  by (rule fset_eqI) (simp add: member_set)
   1.138 +  "Cset.filter f (Set dxs) = Set (filter f dxs)"
   1.139 +  by (rule Cset.set_eqI) (simp add: member_set)
   1.140  
   1.141  lemma forall_Set [code]:
   1.142 -  "Fset.forall P (Set xs) \<longleftrightarrow> list_all P (list_of_dlist xs)"
   1.143 +  "Cset.forall P (Set xs) \<longleftrightarrow> list_all P (list_of_dlist xs)"
   1.144    by (simp add: member_set list_all_iff)
   1.145  
   1.146  lemma exists_Set [code]:
   1.147 -  "Fset.exists P (Set xs) \<longleftrightarrow> list_ex P (list_of_dlist xs)"
   1.148 +  "Cset.exists P (Set xs) \<longleftrightarrow> list_ex P (list_of_dlist xs)"
   1.149    by (simp add: member_set list_ex_iff)
   1.150  
   1.151  lemma card_code [code]:
   1.152 -  "Fset.card (Set dxs) = length dxs"
   1.153 +  "Cset.card (Set dxs) = length dxs"
   1.154    by (simp add: length_def member_set distinct_card)
   1.155  
   1.156  lemma inter_code [code]:
   1.157 -  "inf A (Set xs) = Set (filter (Fset.member A) xs)"
   1.158 -  "inf A (Coset xs) = foldr Fset.remove xs A"
   1.159 +  "inf A (Set xs) = Set (filter (Cset.member A) xs)"
   1.160 +  "inf A (Coset xs) = foldr Cset.remove xs A"
   1.161    by (simp_all only: Set_def Coset_def foldr_def inter_project list_of_dlist_filter)
   1.162  
   1.163  lemma subtract_code [code]:
   1.164 -  "A - Set xs = foldr Fset.remove xs A"
   1.165 -  "A - Coset xs = Set (filter (Fset.member A) xs)"
   1.166 +  "A - Set xs = foldr Cset.remove xs A"
   1.167 +  "A - Coset xs = Set (filter (Cset.member A) xs)"
   1.168    by (simp_all only: Set_def Coset_def foldr_def subtract_remove list_of_dlist_filter)
   1.169  
   1.170  lemma union_code [code]:
   1.171 -  "sup (Set xs) A = foldr Fset.insert xs A"
   1.172 -  "sup (Coset xs) A = Coset (filter (Not \<circ> Fset.member A) xs)"
   1.173 +  "sup (Set xs) A = foldr Cset.insert xs A"
   1.174 +  "sup (Coset xs) A = Coset (filter (Not \<circ> Cset.member A) xs)"
   1.175    by (simp_all only: Set_def Coset_def foldr_def union_insert list_of_dlist_filter)
   1.176  
   1.177  context complete_lattice