--- 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 \
--- 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")
--- 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]
--- 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
--- /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
--- 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