src/HOL/Library/Dlist.thy
changeset 43146 09f74fda1b1d
parent 41505 6d19301074cf
child 43764 366d5726de09
     1.1 --- a/src/HOL/Library/Dlist.thy	Wed Jun 01 23:08:04 2011 +0200
     1.2 +++ b/src/HOL/Library/Dlist.thy	Thu Jun 02 08:55:08 2011 +0200
     1.3 @@ -3,10 +3,10 @@
     1.4  header {* Lists with elements distinct as canonical example for datatype invariants *}
     1.5  
     1.6  theory Dlist
     1.7 -imports Main Cset
     1.8 +imports Main More_List
     1.9  begin
    1.10  
    1.11 -section {* The type of distinct lists *}
    1.12 +subsection {* The type of distinct lists *}
    1.13  
    1.14  typedef (open) 'a dlist = "{xs::'a list. distinct xs}"
    1.15    morphisms list_of_dlist Abs_dlist
    1.16 @@ -80,7 +80,7 @@
    1.17    "foldr f dxs = List.foldr f (list_of_dlist dxs)"
    1.18  
    1.19  
    1.20 -section {* Executable version obeying invariant *}
    1.21 +subsection {* Executable version obeying invariant *}
    1.22  
    1.23  lemma list_of_dlist_empty [simp, code abstract]:
    1.24    "list_of_dlist empty = []"
    1.25 @@ -130,7 +130,7 @@
    1.26    by (fact equal_refl)
    1.27  
    1.28  
    1.29 -section {* Induction principle and case distinction *}
    1.30 +subsection {* Induction principle and case distinction *}
    1.31  
    1.32  lemma dlist_induct [case_names empty insert, induct type: dlist]:
    1.33    assumes empty: "P empty"
    1.34 @@ -173,146 +173,12 @@
    1.35  qed
    1.36  
    1.37  
    1.38 -section {* Functorial structure *}
    1.39 +subsection {* Functorial structure *}
    1.40  
    1.41  enriched_type map: map
    1.42    by (simp_all add: List.map.id remdups_map_remdups fun_eq_iff dlist_eq_iff)
    1.43  
    1.44  
    1.45 -section {* Implementation of sets by distinct lists -- canonical! *}
    1.46 -
    1.47 -definition Set :: "'a dlist \<Rightarrow> 'a Cset.set" where
    1.48 -  "Set dxs = Cset.set (list_of_dlist dxs)"
    1.49 -
    1.50 -definition Coset :: "'a dlist \<Rightarrow> 'a Cset.set" where
    1.51 -  "Coset dxs = Cset.coset (list_of_dlist dxs)"
    1.52 -
    1.53 -code_datatype Set Coset
    1.54 -
    1.55 -declare member_code [code del]
    1.56 -declare Cset.is_empty_set [code del]
    1.57 -declare Cset.empty_set [code del]
    1.58 -declare Cset.UNIV_set [code del]
    1.59 -declare insert_set [code del]
    1.60 -declare remove_set [code del]
    1.61 -declare compl_set [code del]
    1.62 -declare compl_coset [code del]
    1.63 -declare map_set [code del]
    1.64 -declare filter_set [code del]
    1.65 -declare forall_set [code del]
    1.66 -declare exists_set [code del]
    1.67 -declare card_set [code del]
    1.68 -declare inter_project [code del]
    1.69 -declare subtract_remove [code del]
    1.70 -declare union_insert [code del]
    1.71 -declare Infimum_inf [code del]
    1.72 -declare Supremum_sup [code del]
    1.73 -
    1.74 -lemma Set_Dlist [simp]:
    1.75 -  "Set (Dlist xs) = Cset.Set (set xs)"
    1.76 -  by (rule Cset.set_eqI) (simp add: Set_def)
    1.77 -
    1.78 -lemma Coset_Dlist [simp]:
    1.79 -  "Coset (Dlist xs) = Cset.Set (- set xs)"
    1.80 -  by (rule Cset.set_eqI) (simp add: Coset_def)
    1.81 -
    1.82 -lemma member_Set [simp]:
    1.83 -  "Cset.member (Set dxs) = List.member (list_of_dlist dxs)"
    1.84 -  by (simp add: Set_def member_set)
    1.85 -
    1.86 -lemma member_Coset [simp]:
    1.87 -  "Cset.member (Coset dxs) = Not \<circ> List.member (list_of_dlist dxs)"
    1.88 -  by (simp add: Coset_def member_set not_set_compl)
    1.89 -
    1.90 -lemma Set_dlist_of_list [code]:
    1.91 -  "Cset.set xs = Set (dlist_of_list xs)"
    1.92 -  by (rule Cset.set_eqI) simp
    1.93 -
    1.94 -lemma Coset_dlist_of_list [code]:
    1.95 -  "Cset.coset xs = Coset (dlist_of_list xs)"
    1.96 -  by (rule Cset.set_eqI) simp
    1.97 -
    1.98 -lemma is_empty_Set [code]:
    1.99 -  "Cset.is_empty (Set dxs) \<longleftrightarrow> null dxs"
   1.100 -  by (simp add: null_def List.null_def member_set)
   1.101 -
   1.102 -lemma bot_code [code]:
   1.103 -  "bot = Set empty"
   1.104 -  by (simp add: empty_def)
   1.105 -
   1.106 -lemma top_code [code]:
   1.107 -  "top = Coset empty"
   1.108 -  by (simp add: empty_def)
   1.109 -
   1.110 -lemma insert_code [code]:
   1.111 -  "Cset.insert x (Set dxs) = Set (insert x dxs)"
   1.112 -  "Cset.insert x (Coset dxs) = Coset (remove x dxs)"
   1.113 -  by (simp_all add: insert_def remove_def member_set not_set_compl)
   1.114 -
   1.115 -lemma remove_code [code]:
   1.116 -  "Cset.remove x (Set dxs) = Set (remove x dxs)"
   1.117 -  "Cset.remove x (Coset dxs) = Coset (insert x dxs)"
   1.118 -  by (auto simp add: insert_def remove_def member_set not_set_compl)
   1.119 -
   1.120 -lemma member_code [code]:
   1.121 -  "Cset.member (Set dxs) = member dxs"
   1.122 -  "Cset.member (Coset dxs) = Not \<circ> member dxs"
   1.123 -  by (simp_all add: member_def)
   1.124 -
   1.125 -lemma compl_code [code]:
   1.126 -  "- Set dxs = Coset dxs"
   1.127 -  "- Coset dxs = Set dxs"
   1.128 -  by (rule Cset.set_eqI, simp add: member_set not_set_compl)+
   1.129 -
   1.130 -lemma map_code [code]:
   1.131 -  "Cset.map f (Set dxs) = Set (map f dxs)"
   1.132 -  by (rule Cset.set_eqI) (simp add: member_set)
   1.133 -  
   1.134 -lemma filter_code [code]:
   1.135 -  "Cset.filter f (Set dxs) = Set (filter f dxs)"
   1.136 -  by (rule Cset.set_eqI) (simp add: member_set)
   1.137 -
   1.138 -lemma forall_Set [code]:
   1.139 -  "Cset.forall P (Set xs) \<longleftrightarrow> list_all P (list_of_dlist xs)"
   1.140 -  by (simp add: member_set list_all_iff)
   1.141 -
   1.142 -lemma exists_Set [code]:
   1.143 -  "Cset.exists P (Set xs) \<longleftrightarrow> list_ex P (list_of_dlist xs)"
   1.144 -  by (simp add: member_set list_ex_iff)
   1.145 -
   1.146 -lemma card_code [code]:
   1.147 -  "Cset.card (Set dxs) = length dxs"
   1.148 -  by (simp add: length_def member_set distinct_card)
   1.149 -
   1.150 -lemma inter_code [code]:
   1.151 -  "inf A (Set xs) = Set (filter (Cset.member A) xs)"
   1.152 -  "inf A (Coset xs) = foldr Cset.remove xs A"
   1.153 -  by (simp_all only: Set_def Coset_def foldr_def inter_project list_of_dlist_filter)
   1.154 -
   1.155 -lemma subtract_code [code]:
   1.156 -  "A - Set xs = foldr Cset.remove xs A"
   1.157 -  "A - Coset xs = Set (filter (Cset.member A) xs)"
   1.158 -  by (simp_all only: Set_def Coset_def foldr_def subtract_remove list_of_dlist_filter)
   1.159 -
   1.160 -lemma union_code [code]:
   1.161 -  "sup (Set xs) A = foldr Cset.insert xs A"
   1.162 -  "sup (Coset xs) A = Coset (filter (Not \<circ> Cset.member A) xs)"
   1.163 -  by (simp_all only: Set_def Coset_def foldr_def union_insert list_of_dlist_filter)
   1.164 -
   1.165 -context complete_lattice
   1.166 -begin
   1.167 -
   1.168 -lemma Infimum_code [code]:
   1.169 -  "Infimum (Set As) = foldr inf As top"
   1.170 -  by (simp only: Set_def Infimum_inf foldr_def inf.commute)
   1.171 -
   1.172 -lemma Supremum_code [code]:
   1.173 -  "Supremum (Set As) = foldr sup As bot"
   1.174 -  by (simp only: Set_def Supremum_sup foldr_def sup.commute)
   1.175 -
   1.176 -end
   1.177 -
   1.178 -
   1.179  hide_const (open) member fold foldr empty insert remove map filter null member length fold
   1.180  
   1.181  end