splitting Dlist theory in Dlist and Dlist_Cset
authorbulwahn
Thu Jun 02 08:55:08 2011 +0200 (2011-06-02)
changeset 4314609f74fda1b1d
parent 43145 faba4800b00b
child 43147 70337ff0352d
child 43150 69bc4dafcc53
splitting Dlist theory in Dlist and Dlist_Cset
src/HOL/IsaMakefile
src/HOL/Library/Dlist.thy
src/HOL/Library/Dlist_Cset.thy
src/HOL/Library/Library.thy
     1.1 --- a/src/HOL/IsaMakefile	Wed Jun 01 23:08:04 2011 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Thu Jun 02 08:55:08 2011 +0200
     1.3 @@ -443,6 +443,7 @@
     1.4    Library/Code_Prolog.thy Tools/Predicate_Compile/code_prolog.ML	\
     1.5    Library/ContNotDenum.thy Library/Continuity.thy Library/Convex.thy	\
     1.6    Library/Countable.thy Library/Diagonalize.thy Library/Dlist.thy	\
     1.7 +  Library/Dlist_Cset.thy 						\
     1.8    Library/Efficient_Nat.thy Library/Eval_Witness.thy 			\
     1.9    Library/Executable_Set.thy Library/Extended_Reals.thy			\
    1.10    Library/Float.thy Library/Formal_Power_Series.thy			\
     2.1 --- a/src/HOL/Library/Dlist.thy	Wed Jun 01 23:08:04 2011 +0200
     2.2 +++ b/src/HOL/Library/Dlist.thy	Thu Jun 02 08:55:08 2011 +0200
     2.3 @@ -3,10 +3,10 @@
     2.4  header {* Lists with elements distinct as canonical example for datatype invariants *}
     2.5  
     2.6  theory Dlist
     2.7 -imports Main Cset
     2.8 +imports Main More_List
     2.9  begin
    2.10  
    2.11 -section {* The type of distinct lists *}
    2.12 +subsection {* The type of distinct lists *}
    2.13  
    2.14  typedef (open) 'a dlist = "{xs::'a list. distinct xs}"
    2.15    morphisms list_of_dlist Abs_dlist
    2.16 @@ -80,7 +80,7 @@
    2.17    "foldr f dxs = List.foldr f (list_of_dlist dxs)"
    2.18  
    2.19  
    2.20 -section {* Executable version obeying invariant *}
    2.21 +subsection {* Executable version obeying invariant *}
    2.22  
    2.23  lemma list_of_dlist_empty [simp, code abstract]:
    2.24    "list_of_dlist empty = []"
    2.25 @@ -130,7 +130,7 @@
    2.26    by (fact equal_refl)
    2.27  
    2.28  
    2.29 -section {* Induction principle and case distinction *}
    2.30 +subsection {* Induction principle and case distinction *}
    2.31  
    2.32  lemma dlist_induct [case_names empty insert, induct type: dlist]:
    2.33    assumes empty: "P empty"
    2.34 @@ -173,146 +173,12 @@
    2.35  qed
    2.36  
    2.37  
    2.38 -section {* Functorial structure *}
    2.39 +subsection {* Functorial structure *}
    2.40  
    2.41  enriched_type map: map
    2.42    by (simp_all add: List.map.id remdups_map_remdups fun_eq_iff dlist_eq_iff)
    2.43  
    2.44  
    2.45 -section {* Implementation of sets by distinct lists -- canonical! *}
    2.46 -
    2.47 -definition Set :: "'a dlist \<Rightarrow> 'a Cset.set" where
    2.48 -  "Set dxs = Cset.set (list_of_dlist dxs)"
    2.49 -
    2.50 -definition Coset :: "'a dlist \<Rightarrow> 'a Cset.set" where
    2.51 -  "Coset dxs = Cset.coset (list_of_dlist dxs)"
    2.52 -
    2.53 -code_datatype Set Coset
    2.54 -
    2.55 -declare member_code [code del]
    2.56 -declare Cset.is_empty_set [code del]
    2.57 -declare Cset.empty_set [code del]
    2.58 -declare Cset.UNIV_set [code del]
    2.59 -declare insert_set [code del]
    2.60 -declare remove_set [code del]
    2.61 -declare compl_set [code del]
    2.62 -declare compl_coset [code del]
    2.63 -declare map_set [code del]
    2.64 -declare filter_set [code del]
    2.65 -declare forall_set [code del]
    2.66 -declare exists_set [code del]
    2.67 -declare card_set [code del]
    2.68 -declare inter_project [code del]
    2.69 -declare subtract_remove [code del]
    2.70 -declare union_insert [code del]
    2.71 -declare Infimum_inf [code del]
    2.72 -declare Supremum_sup [code del]
    2.73 -
    2.74 -lemma Set_Dlist [simp]:
    2.75 -  "Set (Dlist xs) = Cset.Set (set xs)"
    2.76 -  by (rule Cset.set_eqI) (simp add: Set_def)
    2.77 -
    2.78 -lemma Coset_Dlist [simp]:
    2.79 -  "Coset (Dlist xs) = Cset.Set (- set xs)"
    2.80 -  by (rule Cset.set_eqI) (simp add: Coset_def)
    2.81 -
    2.82 -lemma member_Set [simp]:
    2.83 -  "Cset.member (Set dxs) = List.member (list_of_dlist dxs)"
    2.84 -  by (simp add: Set_def member_set)
    2.85 -
    2.86 -lemma member_Coset [simp]:
    2.87 -  "Cset.member (Coset dxs) = Not \<circ> List.member (list_of_dlist dxs)"
    2.88 -  by (simp add: Coset_def member_set not_set_compl)
    2.89 -
    2.90 -lemma Set_dlist_of_list [code]:
    2.91 -  "Cset.set xs = Set (dlist_of_list xs)"
    2.92 -  by (rule Cset.set_eqI) simp
    2.93 -
    2.94 -lemma Coset_dlist_of_list [code]:
    2.95 -  "Cset.coset xs = Coset (dlist_of_list xs)"
    2.96 -  by (rule Cset.set_eqI) simp
    2.97 -
    2.98 -lemma is_empty_Set [code]:
    2.99 -  "Cset.is_empty (Set dxs) \<longleftrightarrow> null dxs"
   2.100 -  by (simp add: null_def List.null_def member_set)
   2.101 -
   2.102 -lemma bot_code [code]:
   2.103 -  "bot = Set empty"
   2.104 -  by (simp add: empty_def)
   2.105 -
   2.106 -lemma top_code [code]:
   2.107 -  "top = Coset empty"
   2.108 -  by (simp add: empty_def)
   2.109 -
   2.110 -lemma insert_code [code]:
   2.111 -  "Cset.insert x (Set dxs) = Set (insert x dxs)"
   2.112 -  "Cset.insert x (Coset dxs) = Coset (remove x dxs)"
   2.113 -  by (simp_all add: insert_def remove_def member_set not_set_compl)
   2.114 -
   2.115 -lemma remove_code [code]:
   2.116 -  "Cset.remove x (Set dxs) = Set (remove x dxs)"
   2.117 -  "Cset.remove x (Coset dxs) = Coset (insert x dxs)"
   2.118 -  by (auto simp add: insert_def remove_def member_set not_set_compl)
   2.119 -
   2.120 -lemma member_code [code]:
   2.121 -  "Cset.member (Set dxs) = member dxs"
   2.122 -  "Cset.member (Coset dxs) = Not \<circ> member dxs"
   2.123 -  by (simp_all add: member_def)
   2.124 -
   2.125 -lemma compl_code [code]:
   2.126 -  "- Set dxs = Coset dxs"
   2.127 -  "- Coset dxs = Set dxs"
   2.128 -  by (rule Cset.set_eqI, simp add: member_set not_set_compl)+
   2.129 -
   2.130 -lemma map_code [code]:
   2.131 -  "Cset.map f (Set dxs) = Set (map f dxs)"
   2.132 -  by (rule Cset.set_eqI) (simp add: member_set)
   2.133 -  
   2.134 -lemma filter_code [code]:
   2.135 -  "Cset.filter f (Set dxs) = Set (filter f dxs)"
   2.136 -  by (rule Cset.set_eqI) (simp add: member_set)
   2.137 -
   2.138 -lemma forall_Set [code]:
   2.139 -  "Cset.forall P (Set xs) \<longleftrightarrow> list_all P (list_of_dlist xs)"
   2.140 -  by (simp add: member_set list_all_iff)
   2.141 -
   2.142 -lemma exists_Set [code]:
   2.143 -  "Cset.exists P (Set xs) \<longleftrightarrow> list_ex P (list_of_dlist xs)"
   2.144 -  by (simp add: member_set list_ex_iff)
   2.145 -
   2.146 -lemma card_code [code]:
   2.147 -  "Cset.card (Set dxs) = length dxs"
   2.148 -  by (simp add: length_def member_set distinct_card)
   2.149 -
   2.150 -lemma inter_code [code]:
   2.151 -  "inf A (Set xs) = Set (filter (Cset.member A) xs)"
   2.152 -  "inf A (Coset xs) = foldr Cset.remove xs A"
   2.153 -  by (simp_all only: Set_def Coset_def foldr_def inter_project list_of_dlist_filter)
   2.154 -
   2.155 -lemma subtract_code [code]:
   2.156 -  "A - Set xs = foldr Cset.remove xs A"
   2.157 -  "A - Coset xs = Set (filter (Cset.member A) xs)"
   2.158 -  by (simp_all only: Set_def Coset_def foldr_def subtract_remove list_of_dlist_filter)
   2.159 -
   2.160 -lemma union_code [code]:
   2.161 -  "sup (Set xs) A = foldr Cset.insert xs A"
   2.162 -  "sup (Coset xs) A = Coset (filter (Not \<circ> Cset.member A) xs)"
   2.163 -  by (simp_all only: Set_def Coset_def foldr_def union_insert list_of_dlist_filter)
   2.164 -
   2.165 -context complete_lattice
   2.166 -begin
   2.167 -
   2.168 -lemma Infimum_code [code]:
   2.169 -  "Infimum (Set As) = foldr inf As top"
   2.170 -  by (simp only: Set_def Infimum_inf foldr_def inf.commute)
   2.171 -
   2.172 -lemma Supremum_code [code]:
   2.173 -  "Supremum (Set As) = foldr sup As bot"
   2.174 -  by (simp only: Set_def Supremum_sup foldr_def sup.commute)
   2.175 -
   2.176 -end
   2.177 -
   2.178 -
   2.179  hide_const (open) member fold foldr empty insert remove map filter null member length fold
   2.180  
   2.181  end
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Library/Dlist_Cset.thy	Thu Jun 02 08:55:08 2011 +0200
     3.3 @@ -0,0 +1,140 @@
     3.4 +(* Author: Florian Haftmann, TU Muenchen *)
     3.5 +
     3.6 +header {* Canonical implementation of sets by distinct lists *}
     3.7 +
     3.8 +theory Dlist_Cset
     3.9 +imports Dlist Cset
    3.10 +begin
    3.11 +
    3.12 +definition Set :: "'a dlist \<Rightarrow> 'a Cset.set" where
    3.13 +  "Set dxs = Cset.set (list_of_dlist dxs)"
    3.14 +
    3.15 +definition Coset :: "'a dlist \<Rightarrow> 'a Cset.set" where
    3.16 +  "Coset dxs = Cset.coset (list_of_dlist dxs)"
    3.17 +
    3.18 +code_datatype Set Coset
    3.19 +
    3.20 +declare member_code [code del]
    3.21 +declare Cset.is_empty_set [code del]
    3.22 +declare Cset.empty_set [code del]
    3.23 +declare Cset.UNIV_set [code del]
    3.24 +declare insert_set [code del]
    3.25 +declare remove_set [code del]
    3.26 +declare compl_set [code del]
    3.27 +declare compl_coset [code del]
    3.28 +declare map_set [code del]
    3.29 +declare filter_set [code del]
    3.30 +declare forall_set [code del]
    3.31 +declare exists_set [code del]
    3.32 +declare card_set [code del]
    3.33 +declare inter_project [code del]
    3.34 +declare subtract_remove [code del]
    3.35 +declare union_insert [code del]
    3.36 +declare Infimum_inf [code del]
    3.37 +declare Supremum_sup [code del]
    3.38 +
    3.39 +lemma Set_Dlist [simp]:
    3.40 +  "Set (Dlist xs) = Cset.Set (set xs)"
    3.41 +  by (rule Cset.set_eqI) (simp add: Set_def)
    3.42 +
    3.43 +lemma Coset_Dlist [simp]:
    3.44 +  "Coset (Dlist xs) = Cset.Set (- set xs)"
    3.45 +  by (rule Cset.set_eqI) (simp add: Coset_def)
    3.46 +
    3.47 +lemma member_Set [simp]:
    3.48 +  "Cset.member (Set dxs) = List.member (list_of_dlist dxs)"
    3.49 +  by (simp add: Set_def member_set)
    3.50 +
    3.51 +lemma member_Coset [simp]:
    3.52 +  "Cset.member (Coset dxs) = Not \<circ> List.member (list_of_dlist dxs)"
    3.53 +  by (simp add: Coset_def member_set not_set_compl)
    3.54 +
    3.55 +lemma Set_dlist_of_list [code]:
    3.56 +  "Cset.set xs = Set (dlist_of_list xs)"
    3.57 +  by (rule Cset.set_eqI) simp
    3.58 +
    3.59 +lemma Coset_dlist_of_list [code]:
    3.60 +  "Cset.coset xs = Coset (dlist_of_list xs)"
    3.61 +  by (rule Cset.set_eqI) simp
    3.62 +
    3.63 +lemma is_empty_Set [code]:
    3.64 +  "Cset.is_empty (Set dxs) \<longleftrightarrow> Dlist.null dxs"
    3.65 +  by (simp add: Dlist.null_def List.null_def member_set)
    3.66 +
    3.67 +lemma bot_code [code]:
    3.68 +  "bot = Set Dlist.empty"
    3.69 +  by (simp add: empty_def)
    3.70 +
    3.71 +lemma top_code [code]:
    3.72 +  "top = Coset Dlist.empty"
    3.73 +  by (simp add: empty_def)
    3.74 +
    3.75 +lemma insert_code [code]:
    3.76 +  "Cset.insert x (Set dxs) = Set (Dlist.insert x dxs)"
    3.77 +  "Cset.insert x (Coset dxs) = Coset (Dlist.remove x dxs)"
    3.78 +  by (simp_all add: Dlist.insert_def Dlist.remove_def member_set not_set_compl)
    3.79 +
    3.80 +lemma remove_code [code]:
    3.81 +  "Cset.remove x (Set dxs) = Set (Dlist.remove x dxs)"
    3.82 +  "Cset.remove x (Coset dxs) = Coset (Dlist.insert x dxs)"
    3.83 +  by (auto simp add: Dlist.insert_def Dlist.remove_def member_set not_set_compl)
    3.84 +
    3.85 +lemma member_code [code]:
    3.86 +  "Cset.member (Set dxs) = Dlist.member dxs"
    3.87 +  "Cset.member (Coset dxs) = Not \<circ> Dlist.member dxs"
    3.88 +  by (simp_all add: member_def)
    3.89 +
    3.90 +lemma compl_code [code]:
    3.91 +  "- Set dxs = Coset dxs"
    3.92 +  "- Coset dxs = Set dxs"
    3.93 +  by (rule Cset.set_eqI, simp add: member_set not_set_compl)+
    3.94 +
    3.95 +lemma map_code [code]:
    3.96 +  "Cset.map f (Set dxs) = Set (Dlist.map f dxs)"
    3.97 +  by (rule Cset.set_eqI) (simp add: member_set)
    3.98 +  
    3.99 +lemma filter_code [code]:
   3.100 +  "Cset.filter f (Set dxs) = Set (Dlist.filter f dxs)"
   3.101 +  by (rule Cset.set_eqI) (simp add: member_set)
   3.102 +
   3.103 +lemma forall_Set [code]:
   3.104 +  "Cset.forall P (Set xs) \<longleftrightarrow> list_all P (list_of_dlist xs)"
   3.105 +  by (simp add: member_set list_all_iff)
   3.106 +
   3.107 +lemma exists_Set [code]:
   3.108 +  "Cset.exists P (Set xs) \<longleftrightarrow> list_ex P (list_of_dlist xs)"
   3.109 +  by (simp add: member_set list_ex_iff)
   3.110 +
   3.111 +lemma card_code [code]:
   3.112 +  "Cset.card (Set dxs) = Dlist.length dxs"
   3.113 +  by (simp add: length_def member_set distinct_card)
   3.114 +
   3.115 +lemma inter_code [code]:
   3.116 +  "inf A (Set xs) = Set (Dlist.filter (Cset.member A) xs)"
   3.117 +  "inf A (Coset xs) = Dlist.foldr Cset.remove xs A"
   3.118 +  by (simp_all only: Set_def Coset_def foldr_def inter_project list_of_dlist_filter)
   3.119 +
   3.120 +lemma subtract_code [code]:
   3.121 +  "A - Set xs = Dlist.foldr Cset.remove xs A"
   3.122 +  "A - Coset xs = Set (Dlist.filter (Cset.member A) xs)"
   3.123 +  by (simp_all only: Set_def Coset_def foldr_def subtract_remove list_of_dlist_filter)
   3.124 +
   3.125 +lemma union_code [code]:
   3.126 +  "sup (Set xs) A = Dlist.foldr Cset.insert xs A"
   3.127 +  "sup (Coset xs) A = Coset (Dlist.filter (Not \<circ> Cset.member A) xs)"
   3.128 +  by (simp_all only: Set_def Coset_def foldr_def union_insert list_of_dlist_filter)
   3.129 +
   3.130 +context complete_lattice
   3.131 +begin
   3.132 +
   3.133 +lemma Infimum_code [code]:
   3.134 +  "Infimum (Set As) = Dlist.foldr inf As top"
   3.135 +  by (simp only: Set_def Infimum_inf foldr_def inf.commute)
   3.136 +
   3.137 +lemma Supremum_code [code]:
   3.138 +  "Supremum (Set As) = Dlist.foldr sup As bot"
   3.139 +  by (simp only: Set_def Supremum_sup foldr_def sup.commute)
   3.140 +
   3.141 +end
   3.142 +
   3.143 +end
     4.1 --- a/src/HOL/Library/Library.thy	Wed Jun 01 23:08:04 2011 +0200
     4.2 +++ b/src/HOL/Library/Library.thy	Thu Jun 02 08:55:08 2011 +0200
     4.3 @@ -13,7 +13,7 @@
     4.4    Convex
     4.5    Countable
     4.6    Diagonalize
     4.7 -  Dlist
     4.8 +  Dlist_Cset
     4.9    Eval_Witness
    4.10    Float
    4.11    Formal_Power_Series