# HG changeset patch
# User haftmann
# Date 1274366429 -7200
# Node ID e938a0b5286ea0c5008a721e8b479202a10159f2
# Parent  efc202e1677e83731bd2f2099500c1454069fa5a
renamed List_Set to the now more appropriate More_Set

diff -r efc202e1677e -r e938a0b5286e src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Thu May 20 16:35:54 2010 +0200
+++ b/src/HOL/IsaMakefile	Thu May 20 16:40:29 2010 +0200
@@ -407,7 +407,7 @@
   Library/Fraction_Field.thy Library/Fundamental_Theorem_Algebra.thy	\
   Library/Inner_Product.thy Library/Kleene_Algebra.thy			\
   Library/Lattice_Algebras.thy Library/Lattice_Syntax.thy		\
-  Library/Library.thy Library/List_Prefix.thy Library/List_Set.thy	\
+  Library/Library.thy Library/List_Prefix.thy Library/More_Set.thy	\
   Library/More_List.thy Library/Multiset.thy Library/Permutation.thy	\
   Library/Quotient_Type.thy Library/Quicksort.thy			\
   Library/Nat_Infinity.thy Library/README.html	Library/State_Monad.thy	\
diff -r efc202e1677e -r e938a0b5286e src/HOL/Library/Executable_Set.thy
--- a/src/HOL/Library/Executable_Set.thy	Thu May 20 16:35:54 2010 +0200
+++ b/src/HOL/Library/Executable_Set.thy	Thu May 20 16:40:29 2010 +0200
@@ -6,7 +6,7 @@
 header {* A crude implementation of finite sets by lists -- avoid using this at any cost! *}
 
 theory Executable_Set
-imports List_Set
+imports More_Set
 begin
 
 declare mem_def [code del]
@@ -76,9 +76,9 @@
   Code.add_signature_cmd ("is_empty", "'a set \<Rightarrow> bool")
   #> Code.add_signature_cmd ("empty", "'a set")
   #> Code.add_signature_cmd ("insert", "'a \<Rightarrow> 'a set \<Rightarrow> 'a set")
-  #> Code.add_signature_cmd ("List_Set.remove", "'a \<Rightarrow> 'a set \<Rightarrow> 'a set")
+  #> Code.add_signature_cmd ("More_Set.remove", "'a \<Rightarrow> 'a set \<Rightarrow> 'a set")
   #> Code.add_signature_cmd ("image", "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'b set")
-  #> Code.add_signature_cmd ("List_Set.project", "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set")
+  #> Code.add_signature_cmd ("More_Set.project", "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set")
   #> Code.add_signature_cmd ("Ball", "'a set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool")
   #> Code.add_signature_cmd ("Bex", "'a set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool")
   #> Code.add_signature_cmd ("card", "'a set \<Rightarrow> nat")
diff -r efc202e1677e -r e938a0b5286e src/HOL/Library/Fset.thy
--- a/src/HOL/Library/Fset.thy	Thu May 20 16:35:54 2010 +0200
+++ b/src/HOL/Library/Fset.thy	Thu May 20 16:40:29 2010 +0200
@@ -4,7 +4,7 @@
 header {* Executable finite sets *}
 
 theory Fset
-imports List_Set More_List
+imports More_Set More_List
 begin
 
 declare mem_def [simp]
@@ -109,7 +109,7 @@
 subsection {* Basic operations *}
 
 definition is_empty :: "'a fset \<Rightarrow> bool" where
-  [simp]: "is_empty A \<longleftrightarrow> List_Set.is_empty (member A)"
+  [simp]: "is_empty A \<longleftrightarrow> More_Set.is_empty (member A)"
 
 lemma is_empty_Set [code]:
   "is_empty (Set xs) \<longleftrightarrow> null xs"
@@ -132,13 +132,13 @@
   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))"
+  [simp]: "remove x A = Fset (More_Set.remove x (member A))"
 
 lemma remove_Set [code]:
   "remove x (Set xs) = Set (removeAll x xs)"
   "remove x (Coset xs) = Coset (List.insert x xs)"
   by (simp_all add: Set_def Coset_def remove_set_compl)
-    (simp add: List_Set.remove_def)
+    (simp add: More_Set.remove_def)
 
 definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset" where
   [simp]: "map f A = Fset (image f (member A))"
@@ -148,7 +148,7 @@
   by (simp add: Set_def)
 
 definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
-  [simp]: "filter P A = Fset (List_Set.project P (member A))"
+  [simp]: "filter P A = Fset (More_Set.project P (member A))"
 
 lemma filter_Set [code]:
   "filter P (Set xs) = Set (List.filter P xs)"
@@ -211,18 +211,18 @@
 proof -
   show "inf A (Set xs) = Set (List.filter (member A) xs)"
     by (simp add: inter project_def Set_def)
-  have *: "\<And>x::'a. remove = (\<lambda>x. Fset \<circ> List_Set.remove x \<circ> member)"
+  have *: "\<And>x::'a. remove = (\<lambda>x. Fset \<circ> More_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"
+  have "member \<circ> fold (\<lambda>x. Fset \<circ> More_Set.remove x \<circ> member) xs =
+    fold More_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)"
+  then have "fold More_Set.remove xs (member A) = 
+    member (fold (\<lambda>x. Fset \<circ> More_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)
+    by (auto simp add: More_Set.remove_def * intro: ext)
   ultimately show "inf A (Coset xs) = foldr remove xs A"
     by (simp add: foldr_fold)
 qed
@@ -296,17 +296,17 @@
 
 lemma is_empty_simp [simp]:
   "is_empty A \<longleftrightarrow> member A = {}"
-  by (simp add: List_Set.is_empty_def)
+  by (simp add: More_Set.is_empty_def)
 declare is_empty_def [simp del]
 
 lemma remove_simp [simp]:
   "remove x A = Fset (member A - {x})"
-  by (simp add: List_Set.remove_def)
+  by (simp add: More_Set.remove_def)
 declare remove_def [simp del]
 
 lemma filter_simp [simp]:
   "filter P A = Fset {x \<in> member A. P x}"
-  by (simp add: List_Set.project_def)
+  by (simp add: More_Set.project_def)
 declare filter_def [simp del]
 
 declare mem_def [simp del]
diff -r efc202e1677e -r e938a0b5286e src/HOL/Library/List_Set.thy
--- a/src/HOL/Library/List_Set.thy	Thu May 20 16:35:54 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,137 +0,0 @@
-
-(* Author: Florian Haftmann, TU Muenchen *)
-
-header {* Relating (finite) sets and lists *}
-
-theory List_Set
-imports Main More_List
-begin
-
-subsection {* Various additional set functions *}
-
-definition is_empty :: "'a set \<Rightarrow> bool" where
-  "is_empty A \<longleftrightarrow> A = {}"
-
-definition remove :: "'a \<Rightarrow> 'a set \<Rightarrow> 'a set" where
-  "remove x A = A - {x}"
-
-lemma fun_left_comm_idem_remove:
-  "fun_left_comm_idem remove"
-proof -
-  have rem: "remove = (\<lambda>x A. A - {x})" by (simp add: expand_fun_eq remove_def)
-  show ?thesis by (simp only: fun_left_comm_idem_remove rem)
-qed
-
-lemma minus_fold_remove:
-  assumes "finite 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)
-qed
-
-definition project :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" where
-  "project P A = {a\<in>A. P a}"
-
-
-subsection {* Basic set operations *}
-
-lemma is_empty_set:
-  "is_empty (set xs) \<longleftrightarrow> null xs"
-  by (simp add: is_empty_def null_empty)
-
-lemma ball_set:
-  "(\<forall>x\<in>set xs. P x) \<longleftrightarrow> list_all P xs"
-  by (rule list_ball_code)
-
-lemma bex_set:
-  "(\<exists>x\<in>set xs. P x) \<longleftrightarrow> list_ex P xs"
-  by (rule list_bex_code)
-
-lemma empty_set:
-  "{} = set []"
-  by simp
-
-lemma insert_set_compl:
-  "insert x (- set xs) = - set (removeAll x xs)"
-  by auto
-
-lemma remove_set_compl:
-  "remove x (- set xs) = - set (List.insert x xs)"
-  by (auto simp del: mem_def simp add: remove_def List.insert_def)
-
-lemma image_set:
-  "image f (set xs) = set (map f xs)"
-  by simp
-
-lemma project_set:
-  "project P (set xs) = set (filter P xs)"
-  by (auto simp add: project_def)
-
-
-subsection {* Functorial set operations *}
-
-lemma union_set:
-  "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 = fold remove xs A"
-proof -
-  interpret fun_left_comm_idem remove
-    by (fact fun_left_comm_idem_remove)
-  show ?thesis
-    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 *}
-
-lemma member:
-  "a \<in> A \<longleftrightarrow> (\<exists>x\<in>A. a = x)"
-  by simp
-
-lemma subset_eq:
-  "A \<subseteq> B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
-  by (fact subset_eq)
-
-lemma subset:
-  "A \<subset> B \<longleftrightarrow> A \<subseteq> B \<and> \<not> B \<subseteq> A"
-  by (fact less_le_not_le)
-
-lemma set_eq:
-  "A = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
-  by (fact eq_iff)
-
-lemma inter:
-  "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 efc202e1677e -r e938a0b5286e src/HOL/Library/More_Set.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/More_Set.thy	Thu May 20 16:40:29 2010 +0200
@@ -0,0 +1,137 @@
+
+(* Author: Florian Haftmann, TU Muenchen *)
+
+header {* Relating (finite) sets and lists *}
+
+theory More_Set
+imports Main More_List
+begin
+
+subsection {* Various additional set functions *}
+
+definition is_empty :: "'a set \<Rightarrow> bool" where
+  "is_empty A \<longleftrightarrow> A = {}"
+
+definition remove :: "'a \<Rightarrow> 'a set \<Rightarrow> 'a set" where
+  "remove x A = A - {x}"
+
+lemma fun_left_comm_idem_remove:
+  "fun_left_comm_idem remove"
+proof -
+  have rem: "remove = (\<lambda>x A. A - {x})" by (simp add: expand_fun_eq remove_def)
+  show ?thesis by (simp only: fun_left_comm_idem_remove rem)
+qed
+
+lemma minus_fold_remove:
+  assumes "finite 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)
+qed
+
+definition project :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" where
+  "project P A = {a\<in>A. P a}"
+
+
+subsection {* Basic set operations *}
+
+lemma is_empty_set:
+  "is_empty (set xs) \<longleftrightarrow> null xs"
+  by (simp add: is_empty_def null_empty)
+
+lemma ball_set:
+  "(\<forall>x\<in>set xs. P x) \<longleftrightarrow> list_all P xs"
+  by (rule list_ball_code)
+
+lemma bex_set:
+  "(\<exists>x\<in>set xs. P x) \<longleftrightarrow> list_ex P xs"
+  by (rule list_bex_code)
+
+lemma empty_set:
+  "{} = set []"
+  by simp
+
+lemma insert_set_compl:
+  "insert x (- set xs) = - set (removeAll x xs)"
+  by auto
+
+lemma remove_set_compl:
+  "remove x (- set xs) = - set (List.insert x xs)"
+  by (auto simp del: mem_def simp add: remove_def List.insert_def)
+
+lemma image_set:
+  "image f (set xs) = set (map f xs)"
+  by simp
+
+lemma project_set:
+  "project P (set xs) = set (filter P xs)"
+  by (auto simp add: project_def)
+
+
+subsection {* Functorial set operations *}
+
+lemma union_set:
+  "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 = fold remove xs A"
+proof -
+  interpret fun_left_comm_idem remove
+    by (fact fun_left_comm_idem_remove)
+  show ?thesis
+    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 *}
+
+lemma member:
+  "a \<in> A \<longleftrightarrow> (\<exists>x\<in>A. a = x)"
+  by simp
+
+lemma subset_eq:
+  "A \<subseteq> B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
+  by (fact subset_eq)
+
+lemma subset:
+  "A \<subset> B \<longleftrightarrow> A \<subseteq> B \<and> \<not> B \<subseteq> A"
+  by (fact less_le_not_le)
+
+lemma set_eq:
+  "A = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
+  by (fact eq_iff)
+
+lemma inter:
+  "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
diff -r efc202e1677e -r e938a0b5286e src/HOL/MicroJava/BV/BVExample.thy
--- a/src/HOL/MicroJava/BV/BVExample.thy	Thu May 20 16:35:54 2010 +0200
+++ b/src/HOL/MicroJava/BV/BVExample.thy	Thu May 20 16:40:29 2010 +0200
@@ -449,7 +449,7 @@
     (\<lambda>(ss, w).
         let p = some_elem w in propa f (step p (ss ! p)) ss (w - {p}))
     (ss, w)"
-  unfolding iter_def List_Set.is_empty_def some_elem_def ..
+  unfolding iter_def More_Set.is_empty_def some_elem_def ..
 
 lemma JVM_sup_unfold [code]:
  "JVMType.sup S m n = lift2 (Opt.sup