1.1 --- a/src/HOL/Library/Fset.thy	Thu May 20 16:35:54 2010 +0200
     1.2 +++ b/src/HOL/Library/Fset.thy	Thu May 20 16:40:29 2010 +0200
     1.3 @@ -4,7 +4,7 @@
     1.4  header {* Executable finite sets *}
     1.5  
     1.6  theory Fset
     1.7 -imports List_Set More_List
     1.8 +imports More_Set More_List
     1.9  begin
    1.10  
    1.11  declare mem_def [simp]
    1.12 @@ -109,7 +109,7 @@
    1.13  subsection {* Basic operations *}
    1.14  
    1.15  definition is_empty :: "'a fset \<Rightarrow> bool" where
    1.16 -  [simp]: "is_empty A \<longleftrightarrow> List_Set.is_empty (member A)"
    1.17 +  [simp]: "is_empty A \<longleftrightarrow> More_Set.is_empty (member A)"
    1.18  
    1.19  lemma is_empty_Set [code]:
    1.20    "is_empty (Set xs) \<longleftrightarrow> null xs"
    1.21 @@ -132,13 +132,13 @@
    1.22    by (simp_all add: Set_def Coset_def)
    1.23  
    1.24  definition remove :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
    1.25 -  [simp]: "remove x A = Fset (List_Set.remove x (member A))"
    1.26 +  [simp]: "remove x A = Fset (More_Set.remove x (member A))"
    1.27  
    1.28  lemma remove_Set [code]:
    1.29    "remove x (Set xs) = Set (removeAll x xs)"
    1.30    "remove x (Coset xs) = Coset (List.insert x xs)"
    1.31    by (simp_all add: Set_def Coset_def remove_set_compl)
    1.32 -    (simp add: List_Set.remove_def)
    1.33 +    (simp add: More_Set.remove_def)
    1.34  
    1.35  definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset" where
    1.36    [simp]: "map f A = Fset (image f (member A))"
    1.37 @@ -148,7 +148,7 @@
    1.38    by (simp add: Set_def)
    1.39  
    1.40  definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
    1.41 -  [simp]: "filter P A = Fset (List_Set.project P (member A))"
    1.42 +  [simp]: "filter P A = Fset (More_Set.project P (member A))"
    1.43  
    1.44  lemma filter_Set [code]:
    1.45    "filter P (Set xs) = Set (List.filter P xs)"
    1.46 @@ -211,18 +211,18 @@
    1.47  proof -
    1.48    show "inf A (Set xs) = Set (List.filter (member A) xs)"
    1.49      by (simp add: inter project_def Set_def)
    1.50 -  have *: "\<And>x::'a. remove = (\<lambda>x. Fset \<circ> List_Set.remove x \<circ> member)"
    1.51 +  have *: "\<And>x::'a. remove = (\<lambda>x. Fset \<circ> More_Set.remove x \<circ> member)"
    1.52      by (simp add: expand_fun_eq)
    1.53 -  have "member \<circ> fold (\<lambda>x. Fset \<circ> List_Set.remove x \<circ> member) xs =
    1.54 -    fold List_Set.remove xs \<circ> member"
    1.55 +  have "member \<circ> fold (\<lambda>x. Fset \<circ> More_Set.remove x \<circ> member) xs =
    1.56 +    fold More_Set.remove xs \<circ> member"
    1.57      by (rule fold_apply) (simp add: expand_fun_eq)
    1.58 -  then have "fold List_Set.remove xs (member A) = 
    1.59 -    member (fold (\<lambda>x. Fset \<circ> List_Set.remove x \<circ> member) xs A)"
    1.60 +  then have "fold More_Set.remove xs (member A) = 
    1.61 +    member (fold (\<lambda>x. Fset \<circ> More_Set.remove x \<circ> member) xs A)"
    1.62      by (simp add: expand_fun_eq)
    1.63    then have "inf A (Coset xs) = fold remove xs A"
    1.64      by (simp add: Diff_eq [symmetric] minus_set *)
    1.65    moreover have "\<And>x y :: 'a. Fset.remove y \<circ> Fset.remove x = Fset.remove x \<circ> Fset.remove y"
    1.66 -    by (auto simp add: List_Set.remove_def * intro: ext)
    1.67 +    by (auto simp add: More_Set.remove_def * intro: ext)
    1.68    ultimately show "inf A (Coset xs) = foldr remove xs A"
    1.69      by (simp add: foldr_fold)
    1.70  qed
    1.71 @@ -296,17 +296,17 @@
    1.72  
    1.73  lemma is_empty_simp [simp]:
    1.74    "is_empty A \<longleftrightarrow> member A = {}"
    1.75 -  by (simp add: List_Set.is_empty_def)
    1.76 +  by (simp add: More_Set.is_empty_def)
    1.77  declare is_empty_def [simp del]
    1.78  
    1.79  lemma remove_simp [simp]:
    1.80    "remove x A = Fset (member A - {x})"
    1.81 -  by (simp add: List_Set.remove_def)
    1.82 +  by (simp add: More_Set.remove_def)
    1.83  declare remove_def [simp del]
    1.84  
    1.85  lemma filter_simp [simp]:
    1.86    "filter P A = Fset {x \<in> member A. P x}"
    1.87 -  by (simp add: List_Set.project_def)
    1.88 +  by (simp add: More_Set.project_def)
    1.89  declare filter_def [simp del]
    1.90  
    1.91  declare mem_def [simp del]