1.1 --- a/src/HOL/Library/Dlist.thy	Thu May 20 16:35:53 2010 +0200
     1.2 +++ b/src/HOL/Library/Dlist.thy	Thu May 20 16:35:53 2010 +0200
     1.3 @@ -3,42 +3,9 @@
     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 More_List Fset
     1.9  begin
    1.10  
    1.11 -section {* Prelude *}
    1.12 -
    1.13 -text {* Without canonical argument order, higher-order things tend to get confusing quite fast: *}
    1.14 -
    1.15 -setup {* Sign.map_naming (Name_Space.add_path "List") *}
    1.16 -
    1.17 -primrec member :: "'a list \<Rightarrow> 'a \<Rightarrow> bool" where
    1.18 -    "member [] y \<longleftrightarrow> False"
    1.19 -  | "member (x#xs) y \<longleftrightarrow> x = y \<or> member xs y"
    1.20 -
    1.21 -lemma member_set:
    1.22 -  "member = set"
    1.23 -proof (rule ext)+
    1.24 -  fix xs :: "'a list" and x :: 'a
    1.25 -  have "member xs x \<longleftrightarrow> x \<in> set xs" by (induct xs) auto
    1.26 -  then show "member xs x = set xs x" by (simp add: mem_def)
    1.27 -qed
    1.28 -
    1.29 -lemma not_set_compl:
    1.30 -  "Not \<circ> set xs = - set xs"
    1.31 -  by (simp add: fun_Compl_def bool_Compl_def comp_def expand_fun_eq)
    1.32 -
    1.33 -primrec fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where
    1.34 -    "fold f [] s = s"
    1.35 -  | "fold f (x#xs) s = fold f xs (f x s)"
    1.36 -
    1.37 -lemma foldl_fold:
    1.38 -  "foldl f s xs = List.fold (\<lambda>x s. f s x) xs s"
    1.39 -  by (induct xs arbitrary: s) simp_all
    1.40 -
    1.41 -setup {* Sign.map_naming Name_Space.parent_path *}
    1.42 -
    1.43 -
    1.44  section {* The type of distinct lists *}
    1.45  
    1.46  typedef (open) 'a dlist = "{xs::'a list. distinct xs}"
    1.47 @@ -101,7 +68,10 @@
    1.48    "length dxs = List.length (list_of_dlist dxs)"
    1.49  
    1.50  definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b \<Rightarrow> 'b" where
    1.51 -  "fold f dxs = List.fold f (list_of_dlist dxs)"
    1.52 +  "fold f dxs = More_List.fold f (list_of_dlist dxs)"
    1.53 +
    1.54 +definition foldr :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b \<Rightarrow> 'b" where
    1.55 +  "foldr f dxs = List.foldr f (list_of_dlist dxs)"
    1.56  
    1.57  
    1.58  section {* Executable version obeying invariant *}
    1.59 @@ -235,38 +205,34 @@
    1.60    "Fset.card (Set dxs) = length dxs"
    1.61    by (simp add: length_def member_set distinct_card)
    1.62  
    1.63 -lemma foldl_list_of_dlist:
    1.64 -  "foldl f s (list_of_dlist dxs) = fold (\<lambda>x s. f s x) dxs s"
    1.65 -  by (simp add: foldl_fold fold_def)
    1.66 -
    1.67  lemma inter_code [code]:
    1.68    "inf A (Set xs) = Set (filter (Fset.member A) xs)"
    1.69 -  "inf A (Coset xs) = fold Fset.remove xs A"
    1.70 -  by (simp_all only: Set_def Coset_def foldl_list_of_dlist inter_project list_of_dlist_filter)
    1.71 +  "inf A (Coset xs) = foldr Fset.remove xs A"
    1.72 +  by (simp_all only: Set_def Coset_def foldr_def inter_project list_of_dlist_filter)
    1.73  
    1.74  lemma subtract_code [code]:
    1.75 -  "A - Set xs = fold Fset.remove xs A"
    1.76 +  "A - Set xs = foldr Fset.remove xs A"
    1.77    "A - Coset xs = Set (filter (Fset.member A) xs)"
    1.78 -  by (simp_all only: Set_def Coset_def foldl_list_of_dlist subtract_remove list_of_dlist_filter)
    1.79 +  by (simp_all only: Set_def Coset_def foldr_def subtract_remove list_of_dlist_filter)
    1.80  
    1.81  lemma union_code [code]:
    1.82 -  "sup (Set xs) A = fold Fset.insert xs A"
    1.83 +  "sup (Set xs) A = foldr Fset.insert xs A"
    1.84    "sup (Coset xs) A = Coset (filter (Not \<circ> Fset.member A) xs)"
    1.85 -  by (simp_all only: Set_def Coset_def foldl_list_of_dlist union_insert list_of_dlist_filter)
    1.86 +  by (simp_all only: Set_def Coset_def foldr_def union_insert list_of_dlist_filter)
    1.87  
    1.88  context complete_lattice
    1.89  begin
    1.90  
    1.91  lemma Infimum_code [code]:
    1.92 -  "Infimum (Set As) = fold inf As top"
    1.93 -  by (simp only: Set_def Infimum_inf foldl_list_of_dlist inf.commute)
    1.94 +  "Infimum (Set As) = foldr inf As top"
    1.95 +  by (simp only: Set_def Infimum_inf foldr_def inf.commute)
    1.96  
    1.97  lemma Supremum_code [code]:
    1.98 -  "Supremum (Set As) = fold sup As bot"
    1.99 -  by (simp only: Set_def Supremum_sup foldl_list_of_dlist sup.commute)
   1.100 +  "Supremum (Set As) = foldr sup As bot"
   1.101 +  by (simp only: Set_def Supremum_sup foldr_def sup.commute)
   1.102  
   1.103  end
   1.104  
   1.105 -hide_const (open) member fold empty insert remove map filter null member length fold
   1.106 +hide_const (open) member fold foldr empty insert remove map filter null member length fold
   1.107  
   1.108  end