1.1 --- a/src/HOL/Library/Executable_Set.thy	Thu May 20 16:35:53 2010 +0200
     1.2 +++ b/src/HOL/Library/Executable_Set.thy	Thu May 20 16:35:54 2010 +0200
     1.3 @@ -50,8 +50,8 @@
     1.4    by simp
     1.5  
     1.6  lemma [code]:
     1.7 -  "x \<in> Set xs \<longleftrightarrow> member x xs"
     1.8 -  "x \<in> Coset xs \<longleftrightarrow> \<not> member x xs"
     1.9 +  "x \<in> Set xs \<longleftrightarrow> member xs x"
    1.10 +  "x \<in> Coset xs \<longleftrightarrow> \<not> member xs x"
    1.11    by (simp_all add: mem_iff)
    1.12  
    1.13  definition is_empty :: "'a set \<Rightarrow> bool" where
    1.14 @@ -232,36 +232,36 @@
    1.15  
    1.16  lemma inter_project [code]:
    1.17    "inter A (Set xs) = Set (List.filter (\<lambda>x. x \<in> A) xs)"
    1.18 -  "inter A (Coset xs) = foldl (\<lambda>A x. remove x A) A xs"
    1.19 -  by (simp add: inter project_def, simp add: Diff_eq [symmetric] minus_set)
    1.20 +  "inter A (Coset xs) = foldr remove xs A"
    1.21 +  by (simp add: inter project_def) (simp add: Diff_eq [symmetric] minus_set_foldr)
    1.22  
    1.23  lemma subtract_remove [code]:
    1.24 -  "subtract (Set xs) A = foldl (\<lambda>A x. remove x A) A xs"
    1.25 +  "subtract (Set xs) A = foldr remove xs A"
    1.26    "subtract (Coset xs) A = Set (List.filter (\<lambda>x. x \<in> A) xs)"
    1.27 -  by (auto simp add: minus_set)
    1.28 +  by (auto simp add: minus_set_foldr)
    1.29  
    1.30  lemma union_insert [code]:
    1.31 -  "union (Set xs) A = foldl (\<lambda>A x. insert x A) A xs"
    1.32 +  "union (Set xs) A = foldr insert xs A"
    1.33    "union (Coset xs) A = Coset (List.filter (\<lambda>x. x \<notin> A) xs)"
    1.34 -  by (auto simp add: union_set)
    1.35 +  by (auto simp add: union_set_foldr)
    1.36  
    1.37  lemma Inf_inf [code]:
    1.38 -  "Inf (Set xs) = foldl inf (top :: 'a::complete_lattice) xs"
    1.39 +  "Inf (Set xs) = foldr inf xs (top :: 'a::complete_lattice)"
    1.40    "Inf (Coset []) = (bot :: 'a::complete_lattice)"
    1.41 -  by (simp_all add: Inf_UNIV Inf_set_fold)
    1.42 +  by (simp_all add: Inf_UNIV Inf_set_foldr)
    1.43  
    1.44  lemma Sup_sup [code]:
    1.45 -  "Sup (Set xs) = foldl sup (bot :: 'a::complete_lattice) xs"
    1.46 +  "Sup (Set xs) = foldr sup xs (bot :: 'a::complete_lattice)"
    1.47    "Sup (Coset []) = (top :: 'a::complete_lattice)"
    1.48 -  by (simp_all add: Sup_UNIV Sup_set_fold)
    1.49 +  by (simp_all add: Sup_UNIV Sup_set_foldr)
    1.50  
    1.51  lemma Inter_inter [code]:
    1.52 -  "Inter (Set xs) = foldl inter (Coset []) xs"
    1.53 +  "Inter (Set xs) = foldr inter xs (Coset [])"
    1.54    "Inter (Coset []) = empty"
    1.55    unfolding Inter_def Inf_inf by simp_all
    1.56  
    1.57  lemma Union_union [code]:
    1.58 -  "Union (Set xs) = foldl union empty xs"
    1.59 +  "Union (Set xs) = foldr union xs empty"
    1.60    "Union (Coset []) = Coset []"
    1.61    unfolding Union_def Sup_sup by simp_all
    1.62  

     2.1 --- a/src/HOL/Library/Fset.thy	Thu May 20 16:35:53 2010 +0200
     2.2 +++ b/src/HOL/Library/Fset.thy	Thu May 20 16:35:54 2010 +0200
     2.3 @@ -4,7 +4,7 @@
     2.4  header {* Executable finite sets *}
     2.5  
     2.6  theory Fset
     2.7 -imports List_Set
     2.8 +imports List_Set More_List
     2.9  begin
    2.10  
    2.11  declare mem_def [simp]
    2.12 @@ -41,9 +41,9 @@
    2.13  code_datatype Set Coset
    2.14  
    2.15  lemma member_code [code]:
    2.16 -  "member (Set xs) y \<longleftrightarrow> List.member y xs"
    2.17 -  "member (Coset xs) y \<longleftrightarrow> \<not> List.member y xs"
    2.18 -  by (simp_all add: mem_iff fun_Compl_def bool_Compl_def)
    2.19 +  "member (Set xs) = List.member xs"
    2.20 +  "member (Coset xs) = Not \<circ> List.member xs"
    2.21 +  by (simp_all add: expand_fun_eq mem_iff fun_Compl_def bool_Compl_def)
    2.22  
    2.23  lemma member_image_UNIV [simp]:
    2.24    "member ` UNIV = UNIV"
    2.25 @@ -105,6 +105,7 @@
    2.26  
    2.27  end
    2.28  
    2.29 +
    2.30  subsection {* Basic operations *}
    2.31  
    2.32  definition is_empty :: "'a fset \<Rightarrow> bool" where
    2.33 @@ -128,7 +129,7 @@
    2.34  lemma insert_Set [code]:
    2.35    "insert x (Set xs) = Set (List.insert x xs)"
    2.36    "insert x (Coset xs) = Coset (removeAll x xs)"
    2.37 -  by (simp_all add: Set_def Coset_def set_insert)
    2.38 +  by (simp_all add: Set_def Coset_def)
    2.39  
    2.40  definition remove :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
    2.41    [simp]: "remove x A = Fset (List_Set.remove x (member A))"
    2.42 @@ -175,9 +176,17 @@
    2.43  proof -
    2.44    have "Finite_Set.card (set (remdups xs)) = length (remdups xs)"
    2.45      by (rule distinct_card) simp
    2.46 -  then show ?thesis by (simp add: Set_def card_def)
    2.47 +  then show ?thesis by (simp add: Set_def)
    2.48  qed
    2.49  
    2.50 +lemma compl_Set [simp, code]:
    2.51 +  "- Set xs = Coset xs"
    2.52 +  by (simp add: Set_def Coset_def)
    2.53 +
    2.54 +lemma compl_Coset [simp, code]:
    2.55 +  "- Coset xs = Set xs"
    2.56 +  by (simp add: Set_def Coset_def)
    2.57 +
    2.58  
    2.59  subsection {* Derived operations *}
    2.60  
    2.61 @@ -198,39 +207,49 @@
    2.62  
    2.63  lemma inter_project [code]:
    2.64    "inf A (Set xs) = Set (List.filter (member A) xs)"
    2.65 -  "inf A (Coset xs) = foldl (\<lambda>A x. remove x A) A xs"
    2.66 +  "inf A (Coset xs) = foldr remove xs A"
    2.67  proof -
    2.68    show "inf A (Set xs) = Set (List.filter (member A) xs)"
    2.69      by (simp add: inter project_def Set_def)
    2.70 -  have "foldl (\<lambda>A x. List_Set.remove x A) (member A) xs =
    2.71 -    member (foldl (\<lambda>A x. Fset (List_Set.remove x (member A))) A xs)"
    2.72 -    by (rule foldl_apply) (simp add: expand_fun_eq)
    2.73 -  then show "inf A (Coset xs) = foldl (\<lambda>A x. remove x A) A xs"
    2.74 -    by (simp add: Diff_eq [symmetric] minus_set)
    2.75 +  have *: "\<And>x::'a. remove = (\<lambda>x. Fset \<circ> List_Set.remove x \<circ> member)"
    2.76 +    by (simp add: expand_fun_eq)
    2.77 +  have "member \<circ> fold (\<lambda>x. Fset \<circ> List_Set.remove x \<circ> member) xs =
    2.78 +    fold List_Set.remove xs \<circ> member"
    2.79 +    by (rule fold_apply) (simp add: expand_fun_eq)
    2.80 +  then have "fold List_Set.remove xs (member A) = 
    2.81 +    member (fold (\<lambda>x. Fset \<circ> List_Set.remove x \<circ> member) xs A)"
    2.82 +    by (simp add: expand_fun_eq)
    2.83 +  then have "inf A (Coset xs) = fold remove xs A"
    2.84 +    by (simp add: Diff_eq [symmetric] minus_set *)
    2.85 +  moreover have "\<And>x y :: 'a. Fset.remove y \<circ> Fset.remove x = Fset.remove x \<circ> Fset.remove y"
    2.86 +    by (auto simp add: List_Set.remove_def * intro: ext)
    2.87 +  ultimately show "inf A (Coset xs) = foldr remove xs A"
    2.88 +    by (simp add: foldr_fold)
    2.89  qed
    2.90  
    2.91  lemma subtract_remove [code]:
    2.92 -  "A - Set xs = foldl (\<lambda>A x. remove x A) A xs"
    2.93 +  "A - Set xs = foldr remove xs A"
    2.94    "A - Coset xs = Set (List.filter (member A) xs)"
    2.95 -proof -
    2.96 -  have "foldl (\<lambda>A x. List_Set.remove x A) (member A) xs =
    2.97 -    member (foldl (\<lambda>A x. Fset (List_Set.remove x (member A))) A xs)"
    2.98 -    by (rule foldl_apply) (simp add: expand_fun_eq)
    2.99 -  then show "A - Set xs = foldl (\<lambda>A x. remove x A) A xs"
   2.100 -    by (simp add: minus_set)
   2.101 -  show "A - Coset xs = Set (List.filter (member A) xs)"
   2.102 -    by (auto simp add: Coset_def Set_def)
   2.103 -qed
   2.104 +  by (simp_all only: diff_eq compl_Set compl_Coset inter_project)
   2.105  
   2.106  lemma union_insert [code]:
   2.107 -  "sup (Set xs) A = foldl (\<lambda>A x. insert x A) A xs"
   2.108 +  "sup (Set xs) A = foldr insert xs A"
   2.109    "sup (Coset xs) A = Coset (List.filter (Not \<circ> member A) xs)"
   2.110  proof -
   2.111 -  have "foldl (\<lambda>A x. Set.insert x A) (member A) xs =
   2.112 -    member (foldl (\<lambda>A x. Fset (Set.insert x (member A))) A xs)"
   2.113 -    by (rule foldl_apply) (simp add: expand_fun_eq)
   2.114 -  then show "sup (Set xs) A = foldl (\<lambda>A x. insert x A) A xs"
   2.115 -    by (simp add: union_set)
   2.116 +  have *: "\<And>x::'a. insert = (\<lambda>x. Fset \<circ> Set.insert x \<circ> member)"
   2.117 +    by (simp add: expand_fun_eq)
   2.118 +  have "member \<circ> fold (\<lambda>x. Fset \<circ> Set.insert x \<circ> member) xs =
   2.119 +    fold Set.insert xs \<circ> member"
   2.120 +    by (rule fold_apply) (simp add: expand_fun_eq)
   2.121 +  then have "fold Set.insert xs (member A) =
   2.122 +    member (fold (\<lambda>x. Fset \<circ> Set.insert x \<circ> member) xs A)"
   2.123 +    by (simp add: expand_fun_eq)
   2.124 +  then have "sup (Set xs) A = fold insert xs A"
   2.125 +    by (simp add: union_set *)
   2.126 +  moreover have "\<And>x y :: 'a. Fset.insert y \<circ> Fset.insert x = Fset.insert x \<circ> Fset.insert y"
   2.127 +    by (auto simp add: * intro: ext)
   2.128 +  ultimately show "sup (Set xs) A = foldr insert xs A"
   2.129 +    by (simp add: foldr_fold)
   2.130    show "sup (Coset xs) A = Coset (List.filter (Not \<circ> member A) xs)"
   2.131      by (auto simp add: Coset_def)
   2.132  qed
   2.133 @@ -242,17 +261,17 @@
   2.134    [simp]: "Infimum A = Inf (member A)"
   2.135  
   2.136  lemma Infimum_inf [code]:
   2.137 -  "Infimum (Set As) = foldl inf top As"
   2.138 +  "Infimum (Set As) = foldr inf As top"
   2.139    "Infimum (Coset []) = bot"
   2.140 -  by (simp_all add: Inf_set_fold Inf_UNIV)
   2.141 +  by (simp_all add: Inf_set_foldr Inf_UNIV)
   2.142  
   2.143  definition Supremum :: "'a fset \<Rightarrow> 'a" where
   2.144    [simp]: "Supremum A = Sup (member A)"
   2.145  
   2.146  lemma Supremum_sup [code]:
   2.147 -  "Supremum (Set As) = foldl sup bot As"
   2.148 +  "Supremum (Set As) = foldr sup As bot"
   2.149    "Supremum (Coset []) = top"
   2.150 -  by (simp_all add: Sup_set_fold Sup_UNIV)
   2.151 +  by (simp_all add: Sup_set_foldr Sup_UNIV)
   2.152  
   2.153  end
   2.154  

     3.1 --- a/src/HOL/Library/Library.thy	Thu May 20 16:35:53 2010 +0200
     3.2 +++ b/src/HOL/Library/Library.thy	Thu May 20 16:35:54 2010 +0200
     3.3 @@ -34,6 +34,7 @@
     3.4    ListVector
     3.5    Kleene_Algebra
     3.6    Mapping
     3.7 +  More_List
     3.8    Multiset
     3.9    Nat_Infinity
    3.10    Nested_Environment

     4.1 --- a/src/HOL/Library/List_Set.thy	Thu May 20 16:35:53 2010 +0200
     4.2 +++ b/src/HOL/Library/List_Set.thy	Thu May 20 16:35:54 2010 +0200
     4.3 @@ -4,7 +4,7 @@
     4.4  header {* Relating (finite) sets and lists *}
     4.5  
     4.6  theory List_Set
     4.7 -imports Main
     4.8 +imports Main More_List
     4.9  begin
    4.10  
    4.11  subsection {* Various additional set functions *}
    4.12 @@ -24,7 +24,7 @@
    4.13  
    4.14  lemma minus_fold_remove:
    4.15    assumes "finite A"
    4.16 -  shows "B - A = fold remove B A"
    4.17 +  shows "B - A = Finite_Set.fold remove B A"
    4.18  proof -
    4.19    have rem: "remove = (\<lambda>x A. A - {x})" by (simp add: expand_fun_eq remove_def)
    4.20    show ?thesis by (simp only: rem assms minus_fold_remove)
    4.21 @@ -72,15 +72,23 @@
    4.22  subsection {* Functorial set operations *}
    4.23  
    4.24  lemma union_set:
    4.25 -  "set xs \<union> A = foldl (\<lambda>A x. Set.insert x A) A xs"
    4.26 +  "set xs \<union> A = fold Set.insert xs A"
    4.27  proof -
    4.28    interpret fun_left_comm_idem Set.insert
    4.29      by (fact fun_left_comm_idem_insert)
    4.30    show ?thesis by (simp add: union_fold_insert fold_set)
    4.31  qed
    4.32  
    4.33 +lemma union_set_foldr:
    4.34 +  "set xs \<union> A = foldr Set.insert xs A"
    4.35 +proof -
    4.36 +  have "\<And>x y :: 'a. insert y \<circ> insert x = insert x \<circ> insert y"
    4.37 +    by (auto intro: ext)
    4.38 +  then show ?thesis by (simp add: union_set foldr_fold)
    4.39 +qed
    4.40 +
    4.41  lemma minus_set:
    4.42 -  "A - set xs = foldl (\<lambda>A x. remove x A) A xs"
    4.43 +  "A - set xs = fold remove xs A"
    4.44  proof -
    4.45    interpret fun_left_comm_idem remove
    4.46      by (fact fun_left_comm_idem_remove)
    4.47 @@ -88,6 +96,14 @@
    4.48      by (simp add: minus_fold_remove [of _ A] fold_set)
    4.49  qed
    4.50  
    4.51 +lemma minus_set_foldr:
    4.52 +  "A - set xs = foldr remove xs A"
    4.53 +proof -
    4.54 +  have "\<And>x y :: 'a. remove y \<circ> remove x = remove x \<circ> remove y"
    4.55 +    by (auto simp add: remove_def intro: ext)
    4.56 +  then show ?thesis by (simp add: minus_set foldr_fold)
    4.57 +qed
    4.58 +
    4.59  
    4.60  subsection {* Derived set operations *}
    4.61  
    4.62 @@ -111,4 +127,11 @@
    4.63    "A \<inter> B = project (\<lambda>x. x \<in> A) B"
    4.64    by (auto simp add: project_def)
    4.65  
    4.66 +
    4.67 +subsection {* Various lemmas *}
    4.68 +
    4.69 +lemma not_set_compl:
    4.70 +  "Not \<circ> set xs = - set xs"
    4.71 +  by (simp add: fun_Compl_def bool_Compl_def comp_def expand_fun_eq)
    4.72 +
    4.73  end
    4.74 \ No newline at end of file

     5.1 --- a/src/HOL/ex/Codegenerator_Candidates.thy	Thu May 20 16:35:53 2010 +0200
     5.2 +++ b/src/HOL/ex/Codegenerator_Candidates.thy	Thu May 20 16:35:54 2010 +0200
     5.3 @@ -13,6 +13,7 @@
     5.4    Fset
     5.5    Enum
     5.6    List_Prefix
     5.7 +  More_List
     5.8    Nat_Infinity
     5.9    Nested_Environment
    5.10    Option_ord