1.1 --- a/src/HOL/IsaMakefile Thu May 20 16:35:54 2010 +0200
1.2 +++ b/src/HOL/IsaMakefile Thu May 20 16:40:29 2010 +0200
1.3 @@ -407,7 +407,7 @@
1.4 Library/Fraction_Field.thy Library/Fundamental_Theorem_Algebra.thy \
1.5 Library/Inner_Product.thy Library/Kleene_Algebra.thy \
1.6 Library/Lattice_Algebras.thy Library/Lattice_Syntax.thy \
1.7 - Library/Library.thy Library/List_Prefix.thy Library/List_Set.thy \
1.8 + Library/Library.thy Library/List_Prefix.thy Library/More_Set.thy \
1.9 Library/More_List.thy Library/Multiset.thy Library/Permutation.thy \
1.10 Library/Quotient_Type.thy Library/Quicksort.thy \
1.11 Library/Nat_Infinity.thy Library/README.html Library/State_Monad.thy \
2.1 --- a/src/HOL/Library/Executable_Set.thy Thu May 20 16:35:54 2010 +0200
2.2 +++ b/src/HOL/Library/Executable_Set.thy Thu May 20 16:40:29 2010 +0200
2.3 @@ -6,7 +6,7 @@
2.4 header {* A crude implementation of finite sets by lists -- avoid using this at any cost! *}
2.5
2.6 theory Executable_Set
2.7 -imports List_Set
2.8 +imports More_Set
2.9 begin
2.10
2.11 declare mem_def [code del]
2.12 @@ -76,9 +76,9 @@
2.13 Code.add_signature_cmd ("is_empty", "'a set \<Rightarrow> bool")
2.14 #> Code.add_signature_cmd ("empty", "'a set")
2.15 #> Code.add_signature_cmd ("insert", "'a \<Rightarrow> 'a set \<Rightarrow> 'a set")
2.16 - #> Code.add_signature_cmd ("List_Set.remove", "'a \<Rightarrow> 'a set \<Rightarrow> 'a set")
2.17 + #> Code.add_signature_cmd ("More_Set.remove", "'a \<Rightarrow> 'a set \<Rightarrow> 'a set")
2.18 #> Code.add_signature_cmd ("image", "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'b set")
2.19 - #> Code.add_signature_cmd ("List_Set.project", "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set")
2.20 + #> Code.add_signature_cmd ("More_Set.project", "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set")
2.21 #> Code.add_signature_cmd ("Ball", "'a set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool")
2.22 #> Code.add_signature_cmd ("Bex", "'a set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool")
2.23 #> Code.add_signature_cmd ("card", "'a set \<Rightarrow> nat")
3.1 --- a/src/HOL/Library/Fset.thy Thu May 20 16:35:54 2010 +0200
3.2 +++ b/src/HOL/Library/Fset.thy Thu May 20 16:40:29 2010 +0200
3.3 @@ -4,7 +4,7 @@
3.4 header {* Executable finite sets *}
3.5
3.6 theory Fset
3.7 -imports List_Set More_List
3.8 +imports More_Set More_List
3.9 begin
3.10
3.11 declare mem_def [simp]
3.12 @@ -109,7 +109,7 @@
3.13 subsection {* Basic operations *}
3.14
3.15 definition is_empty :: "'a fset \<Rightarrow> bool" where
3.16 - [simp]: "is_empty A \<longleftrightarrow> List_Set.is_empty (member A)"
3.17 + [simp]: "is_empty A \<longleftrightarrow> More_Set.is_empty (member A)"
3.18
3.19 lemma is_empty_Set [code]:
3.20 "is_empty (Set xs) \<longleftrightarrow> null xs"
3.21 @@ -132,13 +132,13 @@
3.22 by (simp_all add: Set_def Coset_def)
3.23
3.24 definition remove :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
3.25 - [simp]: "remove x A = Fset (List_Set.remove x (member A))"
3.26 + [simp]: "remove x A = Fset (More_Set.remove x (member A))"
3.27
3.28 lemma remove_Set [code]:
3.29 "remove x (Set xs) = Set (removeAll x xs)"
3.30 "remove x (Coset xs) = Coset (List.insert x xs)"
3.31 by (simp_all add: Set_def Coset_def remove_set_compl)
3.32 - (simp add: List_Set.remove_def)
3.33 + (simp add: More_Set.remove_def)
3.34
3.35 definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset" where
3.36 [simp]: "map f A = Fset (image f (member A))"
3.37 @@ -148,7 +148,7 @@
3.38 by (simp add: Set_def)
3.39
3.40 definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
3.41 - [simp]: "filter P A = Fset (List_Set.project P (member A))"
3.42 + [simp]: "filter P A = Fset (More_Set.project P (member A))"
3.43
3.44 lemma filter_Set [code]:
3.45 "filter P (Set xs) = Set (List.filter P xs)"
3.46 @@ -211,18 +211,18 @@
3.47 proof -
3.48 show "inf A (Set xs) = Set (List.filter (member A) xs)"
3.49 by (simp add: inter project_def Set_def)
3.50 - have *: "\<And>x::'a. remove = (\<lambda>x. Fset \<circ> List_Set.remove x \<circ> member)"
3.51 + have *: "\<And>x::'a. remove = (\<lambda>x. Fset \<circ> More_Set.remove x \<circ> member)"
3.52 by (simp add: expand_fun_eq)
3.53 - have "member \<circ> fold (\<lambda>x. Fset \<circ> List_Set.remove x \<circ> member) xs =
3.54 - fold List_Set.remove xs \<circ> member"
3.55 + have "member \<circ> fold (\<lambda>x. Fset \<circ> More_Set.remove x \<circ> member) xs =
3.56 + fold More_Set.remove xs \<circ> member"
3.57 by (rule fold_apply) (simp add: expand_fun_eq)
3.58 - then have "fold List_Set.remove xs (member A) =
3.59 - member (fold (\<lambda>x. Fset \<circ> List_Set.remove x \<circ> member) xs A)"
3.60 + then have "fold More_Set.remove xs (member A) =
3.61 + member (fold (\<lambda>x. Fset \<circ> More_Set.remove x \<circ> member) xs A)"
3.62 by (simp add: expand_fun_eq)
3.63 then have "inf A (Coset xs) = fold remove xs A"
3.64 by (simp add: Diff_eq [symmetric] minus_set *)
3.65 moreover have "\<And>x y :: 'a. Fset.remove y \<circ> Fset.remove x = Fset.remove x \<circ> Fset.remove y"
3.66 - by (auto simp add: List_Set.remove_def * intro: ext)
3.67 + by (auto simp add: More_Set.remove_def * intro: ext)
3.68 ultimately show "inf A (Coset xs) = foldr remove xs A"
3.69 by (simp add: foldr_fold)
3.70 qed
3.71 @@ -296,17 +296,17 @@
3.72
3.73 lemma is_empty_simp [simp]:
3.74 "is_empty A \<longleftrightarrow> member A = {}"
3.75 - by (simp add: List_Set.is_empty_def)
3.76 + by (simp add: More_Set.is_empty_def)
3.77 declare is_empty_def [simp del]
3.78
3.79 lemma remove_simp [simp]:
3.80 "remove x A = Fset (member A - {x})"
3.81 - by (simp add: List_Set.remove_def)
3.82 + by (simp add: More_Set.remove_def)
3.83 declare remove_def [simp del]
3.84
3.85 lemma filter_simp [simp]:
3.86 "filter P A = Fset {x \<in> member A. P x}"
3.87 - by (simp add: List_Set.project_def)
3.88 + by (simp add: More_Set.project_def)
3.89 declare filter_def [simp del]
3.90
3.91 declare mem_def [simp del]
4.1 --- a/src/HOL/Library/List_Set.thy Thu May 20 16:35:54 2010 +0200
4.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
4.3 @@ -1,137 +0,0 @@
4.4 -
4.5 -(* Author: Florian Haftmann, TU Muenchen *)
4.6 -
4.7 -header {* Relating (finite) sets and lists *}
4.8 -
4.9 -theory List_Set
4.10 -imports Main More_List
4.11 -begin
4.12 -
4.13 -subsection {* Various additional set functions *}
4.14 -
4.15 -definition is_empty :: "'a set \<Rightarrow> bool" where
4.16 - "is_empty A \<longleftrightarrow> A = {}"
4.17 -
4.18 -definition remove :: "'a \<Rightarrow> 'a set \<Rightarrow> 'a set" where
4.19 - "remove x A = A - {x}"
4.20 -
4.21 -lemma fun_left_comm_idem_remove:
4.22 - "fun_left_comm_idem remove"
4.23 -proof -
4.24 - have rem: "remove = (\<lambda>x A. A - {x})" by (simp add: expand_fun_eq remove_def)
4.25 - show ?thesis by (simp only: fun_left_comm_idem_remove rem)
4.26 -qed
4.27 -
4.28 -lemma minus_fold_remove:
4.29 - assumes "finite A"
4.30 - shows "B - A = Finite_Set.fold remove B A"
4.31 -proof -
4.32 - have rem: "remove = (\<lambda>x A. A - {x})" by (simp add: expand_fun_eq remove_def)
4.33 - show ?thesis by (simp only: rem assms minus_fold_remove)
4.34 -qed
4.35 -
4.36 -definition project :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" where
4.37 - "project P A = {a\<in>A. P a}"
4.38 -
4.39 -
4.40 -subsection {* Basic set operations *}
4.41 -
4.42 -lemma is_empty_set:
4.43 - "is_empty (set xs) \<longleftrightarrow> null xs"
4.44 - by (simp add: is_empty_def null_empty)
4.45 -
4.46 -lemma ball_set:
4.47 - "(\<forall>x\<in>set xs. P x) \<longleftrightarrow> list_all P xs"
4.48 - by (rule list_ball_code)
4.49 -
4.50 -lemma bex_set:
4.51 - "(\<exists>x\<in>set xs. P x) \<longleftrightarrow> list_ex P xs"
4.52 - by (rule list_bex_code)
4.53 -
4.54 -lemma empty_set:
4.55 - "{} = set []"
4.56 - by simp
4.57 -
4.58 -lemma insert_set_compl:
4.59 - "insert x (- set xs) = - set (removeAll x xs)"
4.60 - by auto
4.61 -
4.62 -lemma remove_set_compl:
4.63 - "remove x (- set xs) = - set (List.insert x xs)"
4.64 - by (auto simp del: mem_def simp add: remove_def List.insert_def)
4.65 -
4.66 -lemma image_set:
4.67 - "image f (set xs) = set (map f xs)"
4.68 - by simp
4.69 -
4.70 -lemma project_set:
4.71 - "project P (set xs) = set (filter P xs)"
4.72 - by (auto simp add: project_def)
4.73 -
4.74 -
4.75 -subsection {* Functorial set operations *}
4.76 -
4.77 -lemma union_set:
4.78 - "set xs \<union> A = fold Set.insert xs A"
4.79 -proof -
4.80 - interpret fun_left_comm_idem Set.insert
4.81 - by (fact fun_left_comm_idem_insert)
4.82 - show ?thesis by (simp add: union_fold_insert fold_set)
4.83 -qed
4.84 -
4.85 -lemma union_set_foldr:
4.86 - "set xs \<union> A = foldr Set.insert xs A"
4.87 -proof -
4.88 - have "\<And>x y :: 'a. insert y \<circ> insert x = insert x \<circ> insert y"
4.89 - by (auto intro: ext)
4.90 - then show ?thesis by (simp add: union_set foldr_fold)
4.91 -qed
4.92 -
4.93 -lemma minus_set:
4.94 - "A - set xs = fold remove xs A"
4.95 -proof -
4.96 - interpret fun_left_comm_idem remove
4.97 - by (fact fun_left_comm_idem_remove)
4.98 - show ?thesis
4.99 - by (simp add: minus_fold_remove [of _ A] fold_set)
4.100 -qed
4.101 -
4.102 -lemma minus_set_foldr:
4.103 - "A - set xs = foldr remove xs A"
4.104 -proof -
4.105 - have "\<And>x y :: 'a. remove y \<circ> remove x = remove x \<circ> remove y"
4.106 - by (auto simp add: remove_def intro: ext)
4.107 - then show ?thesis by (simp add: minus_set foldr_fold)
4.108 -qed
4.109 -
4.110 -
4.111 -subsection {* Derived set operations *}
4.112 -
4.113 -lemma member:
4.114 - "a \<in> A \<longleftrightarrow> (\<exists>x\<in>A. a = x)"
4.115 - by simp
4.116 -
4.117 -lemma subset_eq:
4.118 - "A \<subseteq> B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
4.119 - by (fact subset_eq)
4.120 -
4.121 -lemma subset:
4.122 - "A \<subset> B \<longleftrightarrow> A \<subseteq> B \<and> \<not> B \<subseteq> A"
4.123 - by (fact less_le_not_le)
4.124 -
4.125 -lemma set_eq:
4.126 - "A = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
4.127 - by (fact eq_iff)
4.128 -
4.129 -lemma inter:
4.130 - "A \<inter> B = project (\<lambda>x. x \<in> A) B"
4.131 - by (auto simp add: project_def)
4.132 -
4.133 -
4.134 -subsection {* Various lemmas *}
4.135 -
4.136 -lemma not_set_compl:
4.137 - "Not \<circ> set xs = - set xs"
4.138 - by (simp add: fun_Compl_def bool_Compl_def comp_def expand_fun_eq)
4.139 -
4.140 -end
4.141 \ No newline at end of file
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/src/HOL/Library/More_Set.thy Thu May 20 16:40:29 2010 +0200
5.3 @@ -0,0 +1,137 @@
5.4 +
5.5 +(* Author: Florian Haftmann, TU Muenchen *)
5.6 +
5.7 +header {* Relating (finite) sets and lists *}
5.8 +
5.9 +theory More_Set
5.10 +imports Main More_List
5.11 +begin
5.12 +
5.13 +subsection {* Various additional set functions *}
5.14 +
5.15 +definition is_empty :: "'a set \<Rightarrow> bool" where
5.16 + "is_empty A \<longleftrightarrow> A = {}"
5.17 +
5.18 +definition remove :: "'a \<Rightarrow> 'a set \<Rightarrow> 'a set" where
5.19 + "remove x A = A - {x}"
5.20 +
5.21 +lemma fun_left_comm_idem_remove:
5.22 + "fun_left_comm_idem remove"
5.23 +proof -
5.24 + have rem: "remove = (\<lambda>x A. A - {x})" by (simp add: expand_fun_eq remove_def)
5.25 + show ?thesis by (simp only: fun_left_comm_idem_remove rem)
5.26 +qed
5.27 +
5.28 +lemma minus_fold_remove:
5.29 + assumes "finite A"
5.30 + shows "B - A = Finite_Set.fold remove B A"
5.31 +proof -
5.32 + have rem: "remove = (\<lambda>x A. A - {x})" by (simp add: expand_fun_eq remove_def)
5.33 + show ?thesis by (simp only: rem assms minus_fold_remove)
5.34 +qed
5.35 +
5.36 +definition project :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" where
5.37 + "project P A = {a\<in>A. P a}"
5.38 +
5.39 +
5.40 +subsection {* Basic set operations *}
5.41 +
5.42 +lemma is_empty_set:
5.43 + "is_empty (set xs) \<longleftrightarrow> null xs"
5.44 + by (simp add: is_empty_def null_empty)
5.45 +
5.46 +lemma ball_set:
5.47 + "(\<forall>x\<in>set xs. P x) \<longleftrightarrow> list_all P xs"
5.48 + by (rule list_ball_code)
5.49 +
5.50 +lemma bex_set:
5.51 + "(\<exists>x\<in>set xs. P x) \<longleftrightarrow> list_ex P xs"
5.52 + by (rule list_bex_code)
5.53 +
5.54 +lemma empty_set:
5.55 + "{} = set []"
5.56 + by simp
5.57 +
5.58 +lemma insert_set_compl:
5.59 + "insert x (- set xs) = - set (removeAll x xs)"
5.60 + by auto
5.61 +
5.62 +lemma remove_set_compl:
5.63 + "remove x (- set xs) = - set (List.insert x xs)"
5.64 + by (auto simp del: mem_def simp add: remove_def List.insert_def)
5.65 +
5.66 +lemma image_set:
5.67 + "image f (set xs) = set (map f xs)"
5.68 + by simp
5.69 +
5.70 +lemma project_set:
5.71 + "project P (set xs) = set (filter P xs)"
5.72 + by (auto simp add: project_def)
5.73 +
5.74 +
5.75 +subsection {* Functorial set operations *}
5.76 +
5.77 +lemma union_set:
5.78 + "set xs \<union> A = fold Set.insert xs A"
5.79 +proof -
5.80 + interpret fun_left_comm_idem Set.insert
5.81 + by (fact fun_left_comm_idem_insert)
5.82 + show ?thesis by (simp add: union_fold_insert fold_set)
5.83 +qed
5.84 +
5.85 +lemma union_set_foldr:
5.86 + "set xs \<union> A = foldr Set.insert xs A"
5.87 +proof -
5.88 + have "\<And>x y :: 'a. insert y \<circ> insert x = insert x \<circ> insert y"
5.89 + by (auto intro: ext)
5.90 + then show ?thesis by (simp add: union_set foldr_fold)
5.91 +qed
5.92 +
5.93 +lemma minus_set:
5.94 + "A - set xs = fold remove xs A"
5.95 +proof -
5.96 + interpret fun_left_comm_idem remove
5.97 + by (fact fun_left_comm_idem_remove)
5.98 + show ?thesis
5.99 + by (simp add: minus_fold_remove [of _ A] fold_set)
5.100 +qed
5.101 +
5.102 +lemma minus_set_foldr:
5.103 + "A - set xs = foldr remove xs A"
5.104 +proof -
5.105 + have "\<And>x y :: 'a. remove y \<circ> remove x = remove x \<circ> remove y"
5.106 + by (auto simp add: remove_def intro: ext)
5.107 + then show ?thesis by (simp add: minus_set foldr_fold)
5.108 +qed
5.109 +
5.110 +
5.111 +subsection {* Derived set operations *}
5.112 +
5.113 +lemma member:
5.114 + "a \<in> A \<longleftrightarrow> (\<exists>x\<in>A. a = x)"
5.115 + by simp
5.116 +
5.117 +lemma subset_eq:
5.118 + "A \<subseteq> B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
5.119 + by (fact subset_eq)
5.120 +
5.121 +lemma subset:
5.122 + "A \<subset> B \<longleftrightarrow> A \<subseteq> B \<and> \<not> B \<subseteq> A"
5.123 + by (fact less_le_not_le)
5.124 +
5.125 +lemma set_eq:
5.126 + "A = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
5.127 + by (fact eq_iff)
5.128 +
5.129 +lemma inter:
5.130 + "A \<inter> B = project (\<lambda>x. x \<in> A) B"
5.131 + by (auto simp add: project_def)
5.132 +
5.133 +
5.134 +subsection {* Various lemmas *}
5.135 +
5.136 +lemma not_set_compl:
5.137 + "Not \<circ> set xs = - set xs"
5.138 + by (simp add: fun_Compl_def bool_Compl_def comp_def expand_fun_eq)
5.139 +
5.140 +end
6.1 --- a/src/HOL/MicroJava/BV/BVExample.thy Thu May 20 16:35:54 2010 +0200
6.2 +++ b/src/HOL/MicroJava/BV/BVExample.thy Thu May 20 16:40:29 2010 +0200
6.3 @@ -449,7 +449,7 @@
6.4 (\<lambda>(ss, w).
6.5 let p = some_elem w in propa f (step p (ss ! p)) ss (w - {p}))
6.6 (ss, w)"
6.7 - unfolding iter_def List_Set.is_empty_def some_elem_def ..
6.8 + unfolding iter_def More_Set.is_empty_def some_elem_def ..
6.9
6.10 lemma JVM_sup_unfold [code]:
6.11 "JVMType.sup S m n = lift2 (Opt.sup