# HG changeset patch
# User haftmann
# Date 1274366154 -7200
# Node ID efc202e1677e83731bd2f2099500c1454069fa5a
# Parent  f9681d9d1d5658b53e28d347edf1ba2a3e329ec2
added theory More_List

diff -r f9681d9d1d56 -r efc202e1677e src/HOL/Library/Executable_Set.thy
--- a/src/HOL/Library/Executable_Set.thy	Thu May 20 16:35:53 2010 +0200
+++ b/src/HOL/Library/Executable_Set.thy	Thu May 20 16:35:54 2010 +0200
@@ -50,8 +50,8 @@
   by simp
 
 lemma [code]:
-  "x \<in> Set xs \<longleftrightarrow> member x xs"
-  "x \<in> Coset xs \<longleftrightarrow> \<not> member x xs"
+  "x \<in> Set xs \<longleftrightarrow> member xs x"
+  "x \<in> Coset xs \<longleftrightarrow> \<not> member xs x"
   by (simp_all add: mem_iff)
 
 definition is_empty :: "'a set \<Rightarrow> bool" where
@@ -232,36 +232,36 @@
 
 lemma inter_project [code]:
   "inter A (Set xs) = Set (List.filter (\<lambda>x. x \<in> A) xs)"
-  "inter A (Coset xs) = foldl (\<lambda>A x. remove x A) A xs"
-  by (simp add: inter project_def, simp add: Diff_eq [symmetric] minus_set)
+  "inter A (Coset xs) = foldr remove xs A"
+  by (simp add: inter project_def) (simp add: Diff_eq [symmetric] minus_set_foldr)
 
 lemma subtract_remove [code]:
-  "subtract (Set xs) A = foldl (\<lambda>A x. remove x A) A xs"
+  "subtract (Set xs) A = foldr remove xs A"
   "subtract (Coset xs) A = Set (List.filter (\<lambda>x. x \<in> A) xs)"
-  by (auto simp add: minus_set)
+  by (auto simp add: minus_set_foldr)
 
 lemma union_insert [code]:
-  "union (Set xs) A = foldl (\<lambda>A x. insert x A) A xs"
+  "union (Set xs) A = foldr insert xs A"
   "union (Coset xs) A = Coset (List.filter (\<lambda>x. x \<notin> A) xs)"
-  by (auto simp add: union_set)
+  by (auto simp add: union_set_foldr)
 
 lemma Inf_inf [code]:
-  "Inf (Set xs) = foldl inf (top :: 'a::complete_lattice) xs"
+  "Inf (Set xs) = foldr inf xs (top :: 'a::complete_lattice)"
   "Inf (Coset []) = (bot :: 'a::complete_lattice)"
-  by (simp_all add: Inf_UNIV Inf_set_fold)
+  by (simp_all add: Inf_UNIV Inf_set_foldr)
 
 lemma Sup_sup [code]:
-  "Sup (Set xs) = foldl sup (bot :: 'a::complete_lattice) xs"
+  "Sup (Set xs) = foldr sup xs (bot :: 'a::complete_lattice)"
   "Sup (Coset []) = (top :: 'a::complete_lattice)"
-  by (simp_all add: Sup_UNIV Sup_set_fold)
+  by (simp_all add: Sup_UNIV Sup_set_foldr)
 
 lemma Inter_inter [code]:
-  "Inter (Set xs) = foldl inter (Coset []) xs"
+  "Inter (Set xs) = foldr inter xs (Coset [])"
   "Inter (Coset []) = empty"
   unfolding Inter_def Inf_inf by simp_all
 
 lemma Union_union [code]:
-  "Union (Set xs) = foldl union empty xs"
+  "Union (Set xs) = foldr union xs empty"
   "Union (Coset []) = Coset []"
   unfolding Union_def Sup_sup by simp_all
 
diff -r f9681d9d1d56 -r efc202e1677e src/HOL/Library/Fset.thy
--- a/src/HOL/Library/Fset.thy	Thu May 20 16:35:53 2010 +0200
+++ b/src/HOL/Library/Fset.thy	Thu May 20 16:35:54 2010 +0200
@@ -4,7 +4,7 @@
 header {* Executable finite sets *}
 
 theory Fset
-imports List_Set
+imports List_Set More_List
 begin
 
 declare mem_def [simp]
@@ -41,9 +41,9 @@
 code_datatype Set Coset
 
 lemma member_code [code]:
-  "member (Set xs) y \<longleftrightarrow> List.member y xs"
-  "member (Coset xs) y \<longleftrightarrow> \<not> List.member y xs"
-  by (simp_all add: mem_iff fun_Compl_def bool_Compl_def)
+  "member (Set xs) = List.member xs"
+  "member (Coset xs) = Not \<circ> List.member xs"
+  by (simp_all add: expand_fun_eq mem_iff fun_Compl_def bool_Compl_def)
 
 lemma member_image_UNIV [simp]:
   "member ` UNIV = UNIV"
@@ -105,6 +105,7 @@
 
 end
 
+
 subsection {* Basic operations *}
 
 definition is_empty :: "'a fset \<Rightarrow> bool" where
@@ -128,7 +129,7 @@
 lemma insert_Set [code]:
   "insert x (Set xs) = Set (List.insert x xs)"
   "insert x (Coset xs) = Coset (removeAll x xs)"
-  by (simp_all add: Set_def Coset_def set_insert)
+  by (simp_all add: Set_def Coset_def)
 
 definition remove :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
   [simp]: "remove x A = Fset (List_Set.remove x (member A))"
@@ -175,9 +176,17 @@
 proof -
   have "Finite_Set.card (set (remdups xs)) = length (remdups xs)"
     by (rule distinct_card) simp
-  then show ?thesis by (simp add: Set_def card_def)
+  then show ?thesis by (simp add: Set_def)
 qed
 
+lemma compl_Set [simp, code]:
+  "- Set xs = Coset xs"
+  by (simp add: Set_def Coset_def)
+
+lemma compl_Coset [simp, code]:
+  "- Coset xs = Set xs"
+  by (simp add: Set_def Coset_def)
+
 
 subsection {* Derived operations *}
 
@@ -198,39 +207,49 @@
 
 lemma inter_project [code]:
   "inf A (Set xs) = Set (List.filter (member A) xs)"
-  "inf A (Coset xs) = foldl (\<lambda>A x. remove x A) A xs"
+  "inf A (Coset xs) = foldr remove xs A"
 proof -
   show "inf A (Set xs) = Set (List.filter (member A) xs)"
     by (simp add: inter project_def Set_def)
-  have "foldl (\<lambda>A x. List_Set.remove x A) (member A) xs =
-    member (foldl (\<lambda>A x. Fset (List_Set.remove x (member A))) A xs)"
-    by (rule foldl_apply) (simp add: expand_fun_eq)
-  then show "inf A (Coset xs) = foldl (\<lambda>A x. remove x A) A xs"
-    by (simp add: Diff_eq [symmetric] minus_set)
+  have *: "\<And>x::'a. remove = (\<lambda>x. Fset \<circ> List_Set.remove x \<circ> member)"
+    by (simp add: expand_fun_eq)
+  have "member \<circ> fold (\<lambda>x. Fset \<circ> List_Set.remove x \<circ> member) xs =
+    fold List_Set.remove xs \<circ> member"
+    by (rule fold_apply) (simp add: expand_fun_eq)
+  then have "fold List_Set.remove xs (member A) = 
+    member (fold (\<lambda>x. Fset \<circ> List_Set.remove x \<circ> member) xs A)"
+    by (simp add: expand_fun_eq)
+  then have "inf A (Coset xs) = fold remove xs A"
+    by (simp add: Diff_eq [symmetric] minus_set *)
+  moreover have "\<And>x y :: 'a. Fset.remove y \<circ> Fset.remove x = Fset.remove x \<circ> Fset.remove y"
+    by (auto simp add: List_Set.remove_def * intro: ext)
+  ultimately show "inf A (Coset xs) = foldr remove xs A"
+    by (simp add: foldr_fold)
 qed
 
 lemma subtract_remove [code]:
-  "A - Set xs = foldl (\<lambda>A x. remove x A) A xs"
+  "A - Set xs = foldr remove xs A"
   "A - Coset xs = Set (List.filter (member A) xs)"
-proof -
-  have "foldl (\<lambda>A x. List_Set.remove x A) (member A) xs =
-    member (foldl (\<lambda>A x. Fset (List_Set.remove x (member A))) A xs)"
-    by (rule foldl_apply) (simp add: expand_fun_eq)
-  then show "A - Set xs = foldl (\<lambda>A x. remove x A) A xs"
-    by (simp add: minus_set)
-  show "A - Coset xs = Set (List.filter (member A) xs)"
-    by (auto simp add: Coset_def Set_def)
-qed
+  by (simp_all only: diff_eq compl_Set compl_Coset inter_project)
 
 lemma union_insert [code]:
-  "sup (Set xs) A = foldl (\<lambda>A x. insert x A) A xs"
+  "sup (Set xs) A = foldr insert xs A"
   "sup (Coset xs) A = Coset (List.filter (Not \<circ> member A) xs)"
 proof -
-  have "foldl (\<lambda>A x. Set.insert x A) (member A) xs =
-    member (foldl (\<lambda>A x. Fset (Set.insert x (member A))) A xs)"
-    by (rule foldl_apply) (simp add: expand_fun_eq)
-  then show "sup (Set xs) A = foldl (\<lambda>A x. insert x A) A xs"
-    by (simp add: union_set)
+  have *: "\<And>x::'a. insert = (\<lambda>x. Fset \<circ> Set.insert x \<circ> member)"
+    by (simp add: expand_fun_eq)
+  have "member \<circ> fold (\<lambda>x. Fset \<circ> Set.insert x \<circ> member) xs =
+    fold Set.insert xs \<circ> member"
+    by (rule fold_apply) (simp add: expand_fun_eq)
+  then have "fold Set.insert xs (member A) =
+    member (fold (\<lambda>x. Fset \<circ> Set.insert x \<circ> member) xs A)"
+    by (simp add: expand_fun_eq)
+  then have "sup (Set xs) A = fold insert xs A"
+    by (simp add: union_set *)
+  moreover have "\<And>x y :: 'a. Fset.insert y \<circ> Fset.insert x = Fset.insert x \<circ> Fset.insert y"
+    by (auto simp add: * intro: ext)
+  ultimately show "sup (Set xs) A = foldr insert xs A"
+    by (simp add: foldr_fold)
   show "sup (Coset xs) A = Coset (List.filter (Not \<circ> member A) xs)"
     by (auto simp add: Coset_def)
 qed
@@ -242,17 +261,17 @@
   [simp]: "Infimum A = Inf (member A)"
 
 lemma Infimum_inf [code]:
-  "Infimum (Set As) = foldl inf top As"
+  "Infimum (Set As) = foldr inf As top"
   "Infimum (Coset []) = bot"
-  by (simp_all add: Inf_set_fold Inf_UNIV)
+  by (simp_all add: Inf_set_foldr Inf_UNIV)
 
 definition Supremum :: "'a fset \<Rightarrow> 'a" where
   [simp]: "Supremum A = Sup (member A)"
 
 lemma Supremum_sup [code]:
-  "Supremum (Set As) = foldl sup bot As"
+  "Supremum (Set As) = foldr sup As bot"
   "Supremum (Coset []) = top"
-  by (simp_all add: Sup_set_fold Sup_UNIV)
+  by (simp_all add: Sup_set_foldr Sup_UNIV)
 
 end
 
diff -r f9681d9d1d56 -r efc202e1677e src/HOL/Library/Library.thy
--- a/src/HOL/Library/Library.thy	Thu May 20 16:35:53 2010 +0200
+++ b/src/HOL/Library/Library.thy	Thu May 20 16:35:54 2010 +0200
@@ -34,6 +34,7 @@
   ListVector
   Kleene_Algebra
   Mapping
+  More_List
   Multiset
   Nat_Infinity
   Nested_Environment
diff -r f9681d9d1d56 -r efc202e1677e src/HOL/Library/List_Set.thy
--- a/src/HOL/Library/List_Set.thy	Thu May 20 16:35:53 2010 +0200
+++ b/src/HOL/Library/List_Set.thy	Thu May 20 16:35:54 2010 +0200
@@ -4,7 +4,7 @@
 header {* Relating (finite) sets and lists *}
 
 theory List_Set
-imports Main
+imports Main More_List
 begin
 
 subsection {* Various additional set functions *}
@@ -24,7 +24,7 @@
 
 lemma minus_fold_remove:
   assumes "finite A"
-  shows "B - A = fold remove B A"
+  shows "B - A = Finite_Set.fold remove B A"
 proof -
   have rem: "remove = (\<lambda>x A. A - {x})" by (simp add: expand_fun_eq remove_def)
   show ?thesis by (simp only: rem assms minus_fold_remove)
@@ -72,15 +72,23 @@
 subsection {* Functorial set operations *}
 
 lemma union_set:
-  "set xs \<union> A = foldl (\<lambda>A x. Set.insert x A) A xs"
+  "set xs \<union> A = fold Set.insert xs A"
 proof -
   interpret fun_left_comm_idem Set.insert
     by (fact fun_left_comm_idem_insert)
   show ?thesis by (simp add: union_fold_insert fold_set)
 qed
 
+lemma union_set_foldr:
+  "set xs \<union> A = foldr Set.insert xs A"
+proof -
+  have "\<And>x y :: 'a. insert y \<circ> insert x = insert x \<circ> insert y"
+    by (auto intro: ext)
+  then show ?thesis by (simp add: union_set foldr_fold)
+qed
+
 lemma minus_set:
-  "A - set xs = foldl (\<lambda>A x. remove x A) A xs"
+  "A - set xs = fold remove xs A"
 proof -
   interpret fun_left_comm_idem remove
     by (fact fun_left_comm_idem_remove)
@@ -88,6 +96,14 @@
     by (simp add: minus_fold_remove [of _ A] fold_set)
 qed
 
+lemma minus_set_foldr:
+  "A - set xs = foldr remove xs A"
+proof -
+  have "\<And>x y :: 'a. remove y \<circ> remove x = remove x \<circ> remove y"
+    by (auto simp add: remove_def intro: ext)
+  then show ?thesis by (simp add: minus_set foldr_fold)
+qed
+
 
 subsection {* Derived set operations *}
 
@@ -111,4 +127,11 @@
   "A \<inter> B = project (\<lambda>x. x \<in> A) B"
   by (auto simp add: project_def)
 
+
+subsection {* Various lemmas *}
+
+lemma not_set_compl:
+  "Not \<circ> set xs = - set xs"
+  by (simp add: fun_Compl_def bool_Compl_def comp_def expand_fun_eq)
+
 end
\ No newline at end of file
diff -r f9681d9d1d56 -r efc202e1677e src/HOL/ex/Codegenerator_Candidates.thy
--- a/src/HOL/ex/Codegenerator_Candidates.thy	Thu May 20 16:35:53 2010 +0200
+++ b/src/HOL/ex/Codegenerator_Candidates.thy	Thu May 20 16:35:54 2010 +0200
@@ -13,6 +13,7 @@
   Fset
   Enum
   List_Prefix
+  More_List
   Nat_Infinity
   Nested_Environment
   Option_ord