--- a/NEWS Thu May 20 16:25:22 2010 +0200
+++ b/NEWS Thu May 20 19:55:42 2010 +0200
@@ -143,6 +143,9 @@
*** HOL ***
+* List membership infix mem operation is only an input abbreviation.
+INCOMPATIBILITY.
+
* Theory Library/Word.thy has been removed. Use library Word/Word.thy for
future developements; former Library/Word.thy is still present in the AFP
entry RSAPPS.
--- a/src/HOL/IsaMakefile Thu May 20 16:25:22 2010 +0200
+++ b/src/HOL/IsaMakefile Thu May 20 19:55:42 2010 +0200
@@ -401,16 +401,16 @@
Library/Efficient_Nat.thy Library/Sum_Of_Squares.thy \
Library/Dlist.thy Library/Sum_Of_Squares/sos_wrapper.ML \
Library/Sum_Of_Squares/sum_of_squares.ML Library/Fset.thy \
- Library/Glbs.thy Library/Executable_Set.thy \
+ Library/Glbs.thy Library/Executable_Set.thy \
Library/Infinite_Set.thy Library/FuncSet.thy \
Library/Permutations.thy Library/Bit.thy Library/FrechetDeriv.thy \
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/State_Monad.thy Library/Multiset.thy Library/Permutation.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/Nat_Infinity.thy Library/README.html Library/State_Monad.thy \
Library/Continuity.thy Library/Order_Relation.thy \
Library/Nested_Environment.thy Library/Ramsey.thy Library/Zorn.thy \
Library/Library/ROOT.ML Library/Library/document/root.tex \
@@ -433,7 +433,7 @@
Library/Nat_Bijection.thy $(SRC)/Tools/float.ML \
$(SRC)/HOL/Tools/float_arith.ML Library/positivstellensatz.ML \
Library/reify_data.ML Library/reflection.ML Library/LaTeXsugar.thy \
- Library/OptionalSugar.thy Library/Convex.thy \
+ Library/OptionalSugar.thy Library/Convex.thy \
Library/Predicate_Compile_Quickcheck.thy Library/SML_Quickcheck.thy
@cd Library; $(ISABELLE_TOOL) usedir $(OUT)/HOL Library
@@ -586,17 +586,18 @@
HOL-Old_Number_Theory: HOL $(LOG)/HOL-Old_Number_Theory.gz
-$(LOG)/HOL-Old_Number_Theory.gz: $(OUT)/HOL Library/Permutation.thy \
- Old_Number_Theory/Primes.thy Old_Number_Theory/Fib.thy \
- Old_Number_Theory/Factorization.thy Old_Number_Theory/BijectionRel.thy \
- Old_Number_Theory/Chinese.thy Old_Number_Theory/EulerFermat.thy \
- Old_Number_Theory/IntFact.thy Old_Number_Theory/IntPrimes.thy \
- Old_Number_Theory/WilsonBij.thy Old_Number_Theory/WilsonRuss.thy \
- Old_Number_Theory/Finite2.thy Old_Number_Theory/Int2.thy \
- Old_Number_Theory/EvenOdd.thy Old_Number_Theory/Residues.thy \
- Old_Number_Theory/Euler.thy Old_Number_Theory/Gauss.thy \
+$(LOG)/HOL-Old_Number_Theory.gz: $(OUT)/HOL Library/Permutation.thy \
+ Old_Number_Theory/Primes.thy Old_Number_Theory/Fib.thy \
+ Old_Number_Theory/Factorization.thy Old_Number_Theory/BijectionRel.thy\
+ Old_Number_Theory/Chinese.thy Old_Number_Theory/EulerFermat.thy \
+ Old_Number_Theory/IntFact.thy Old_Number_Theory/IntPrimes.thy \
+ Old_Number_Theory/WilsonBij.thy Old_Number_Theory/WilsonRuss.thy \
+ Old_Number_Theory/Finite2.thy Old_Number_Theory/Int2.thy \
+ Old_Number_Theory/EvenOdd.thy Old_Number_Theory/Residues.thy \
+ Old_Number_Theory/Euler.thy Old_Number_Theory/Gauss.thy \
Old_Number_Theory/Quadratic_Reciprocity.thy Library/Infinite_Set.thy \
- Old_Number_Theory/Legacy_GCD.thy Old_Number_Theory/Pocklington.thy Old_Number_Theory/ROOT.ML
+ Old_Number_Theory/Legacy_GCD.thy Old_Number_Theory/Pocklington.thy \
+ Old_Number_Theory/ROOT.ML
@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Old_Number_Theory
@@ -711,9 +712,9 @@
HOL-Auth: HOL $(LOG)/HOL-Auth.gz
$(LOG)/HOL-Auth.gz: $(OUT)/HOL \
- Auth/Auth_Shared.thy Auth/Auth_Public.thy Auth/All_Symmetric.thy \
- Auth/Guard/Auth_Guard_Shared.thy \
- Auth/Guard/Auth_Guard_Public.thy \
+ Auth/Auth_Shared.thy Auth/Auth_Public.thy Auth/All_Symmetric.thy \
+ Auth/Guard/Auth_Guard_Shared.thy \
+ Auth/Guard/Auth_Guard_Public.thy \
Auth/Smartcard/Auth_Smartcard.thy Auth/All_Symmetric.thy \
Auth/CertifiedEmail.thy Auth/Event.thy Auth/Message.thy \
Auth/NS_Public.thy Auth/NS_Public_Bad.thy Auth/NS_Shared.thy \
--- a/src/HOL/Library/Dlist.thy Thu May 20 16:25:22 2010 +0200
+++ b/src/HOL/Library/Dlist.thy Thu May 20 19:55:42 2010 +0200
@@ -3,42 +3,9 @@
header {* Lists with elements distinct as canonical example for datatype invariants *}
theory Dlist
-imports Main Fset
+imports Main More_List Fset
begin
-section {* Prelude *}
-
-text {* Without canonical argument order, higher-order things tend to get confusing quite fast: *}
-
-setup {* Sign.map_naming (Name_Space.add_path "List") *}
-
-primrec member :: "'a list \<Rightarrow> 'a \<Rightarrow> bool" where
- "member [] y \<longleftrightarrow> False"
- | "member (x#xs) y \<longleftrightarrow> x = y \<or> member xs y"
-
-lemma member_set:
- "member = set"
-proof (rule ext)+
- fix xs :: "'a list" and x :: 'a
- have "member xs x \<longleftrightarrow> x \<in> set xs" by (induct xs) auto
- then show "member xs x = set xs x" by (simp add: mem_def)
-qed
-
-lemma not_set_compl:
- "Not \<circ> set xs = - set xs"
- by (simp add: fun_Compl_def bool_Compl_def comp_def expand_fun_eq)
-
-primrec fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where
- "fold f [] s = s"
- | "fold f (x#xs) s = fold f xs (f x s)"
-
-lemma foldl_fold:
- "foldl f s xs = List.fold (\<lambda>x s. f s x) xs s"
- by (induct xs arbitrary: s) simp_all
-
-setup {* Sign.map_naming Name_Space.parent_path *}
-
-
section {* The type of distinct lists *}
typedef (open) 'a dlist = "{xs::'a list. distinct xs}"
@@ -101,7 +68,10 @@
"length dxs = List.length (list_of_dlist dxs)"
definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b \<Rightarrow> 'b" where
- "fold f dxs = List.fold f (list_of_dlist dxs)"
+ "fold f dxs = More_List.fold f (list_of_dlist dxs)"
+
+definition foldr :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b \<Rightarrow> 'b" where
+ "foldr f dxs = List.foldr f (list_of_dlist dxs)"
section {* Executable version obeying invariant *}
@@ -153,6 +123,8 @@
declare UNIV_Set [code del]
declare insert_Set [code del]
declare remove_Set [code del]
+declare compl_Set [code del]
+declare compl_Coset [code del]
declare map_Set [code del]
declare filter_Set [code del]
declare forall_Set [code del]
@@ -215,6 +187,11 @@
"Fset.member (Coset dxs) = Not \<circ> member dxs"
by (simp_all add: member_def)
+lemma compl_code [code]:
+ "- Set dxs = Coset dxs"
+ "- Coset dxs = Set dxs"
+ by (simp_all add: not_set_compl member_set)
+
lemma map_code [code]:
"Fset.map f (Set dxs) = Set (map f dxs)"
by (simp add: member_set)
@@ -235,38 +212,34 @@
"Fset.card (Set dxs) = length dxs"
by (simp add: length_def member_set distinct_card)
-lemma foldl_list_of_dlist:
- "foldl f s (list_of_dlist dxs) = fold (\<lambda>x s. f s x) dxs s"
- by (simp add: foldl_fold fold_def)
-
lemma inter_code [code]:
"inf A (Set xs) = Set (filter (Fset.member A) xs)"
- "inf A (Coset xs) = fold Fset.remove xs A"
- by (simp_all only: Set_def Coset_def foldl_list_of_dlist inter_project list_of_dlist_filter)
+ "inf A (Coset xs) = foldr Fset.remove xs A"
+ by (simp_all only: Set_def Coset_def foldr_def inter_project list_of_dlist_filter)
lemma subtract_code [code]:
- "A - Set xs = fold Fset.remove xs A"
+ "A - Set xs = foldr Fset.remove xs A"
"A - Coset xs = Set (filter (Fset.member A) xs)"
- by (simp_all only: Set_def Coset_def foldl_list_of_dlist subtract_remove list_of_dlist_filter)
+ by (simp_all only: Set_def Coset_def foldr_def subtract_remove list_of_dlist_filter)
lemma union_code [code]:
- "sup (Set xs) A = fold Fset.insert xs A"
+ "sup (Set xs) A = foldr Fset.insert xs A"
"sup (Coset xs) A = Coset (filter (Not \<circ> Fset.member A) xs)"
- by (simp_all only: Set_def Coset_def foldl_list_of_dlist union_insert list_of_dlist_filter)
+ by (simp_all only: Set_def Coset_def foldr_def union_insert list_of_dlist_filter)
context complete_lattice
begin
lemma Infimum_code [code]:
- "Infimum (Set As) = fold inf As top"
- by (simp only: Set_def Infimum_inf foldl_list_of_dlist inf.commute)
+ "Infimum (Set As) = foldr inf As top"
+ by (simp only: Set_def Infimum_inf foldr_def inf.commute)
lemma Supremum_code [code]:
- "Supremum (Set As) = fold sup As bot"
- by (simp only: Set_def Supremum_sup foldl_list_of_dlist sup.commute)
+ "Supremum (Set As) = foldr sup As bot"
+ by (simp only: Set_def Supremum_sup foldr_def sup.commute)
end
-hide_const (open) member fold empty insert remove map filter null member length fold
+hide_const (open) member fold foldr empty insert remove map filter null member length fold
end
--- a/src/HOL/Library/Executable_Set.thy Thu May 20 16:25:22 2010 +0200
+++ b/src/HOL/Library/Executable_Set.thy Thu May 20 19:55:42 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]
@@ -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
@@ -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")
@@ -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
--- a/src/HOL/Library/Fset.thy Thu May 20 16:25:22 2010 +0200
+++ b/src/HOL/Library/Fset.thy Thu May 20 19:55:42 2010 +0200
@@ -4,7 +4,7 @@
header {* Executable finite sets *}
theory Fset
-imports List_Set
+imports More_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,10 +105,11 @@
end
+
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"
@@ -128,16 +129,16 @@
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))"
+ [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))"
@@ -147,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)"
@@ -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> More_Set.remove x \<circ> member)"
+ by (simp add: expand_fun_eq)
+ 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 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: More_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
@@ -277,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/Library.thy Thu May 20 16:25:22 2010 +0200
+++ b/src/HOL/Library/Library.thy Thu May 20 19:55:42 2010 +0200
@@ -34,6 +34,7 @@
ListVector
Kleene_Algebra
Mapping
+ More_List
Multiset
Nat_Infinity
Nested_Environment
--- a/src/HOL/Library/List_Set.thy Thu May 20 16:25:22 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,114 +0,0 @@
-
-(* Author: Florian Haftmann, TU Muenchen *)
-
-header {* Relating (finite) sets and lists *}
-
-theory List_Set
-imports Main
-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 = 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 = foldl (\<lambda>A x. Set.insert x A) A xs"
-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 minus_set:
- "A - set xs = foldl (\<lambda>A x. remove x A) A xs"
-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
-
-
-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)
-
-end
\ No newline at end of file
--- a/src/HOL/Library/Mapping.thy Thu May 20 16:25:22 2010 +0200
+++ b/src/HOL/Library/Mapping.thy Thu May 20 19:55:42 2010 +0200
@@ -40,6 +40,16 @@
definition replace :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" where
"replace k v m = (if lookup m k = None then m else update k v m)"
+definition default :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" where
+ "default k v m = (if lookup m k = None then update k v m else m)"
+
+definition map_entry :: "'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" where
+ "map_entry k f m = (case lookup m k of None \<Rightarrow> m
+ | Some v \<Rightarrow> update k (f v) m)"
+
+definition map_default :: "'a \<Rightarrow> 'b \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" where
+ "map_default k v f m = map_entry k f (default k v m)"
+
definition tabulate :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) mapping" where
"tabulate ks f = Mapping (map_of (map (\<lambda>k. (k, f k)) ks))"
@@ -70,6 +80,10 @@
"lookup (delete k m) = (lookup m) (k := None)"
by (cases m) simp
+lemma lookup_map_entry [simp]:
+ "lookup (map_entry k f m) = (lookup m) (k := Option.map f (lookup m k))"
+ by (cases "lookup m k") (simp_all add: map_entry_def expand_fun_eq)
+
lemma lookup_tabulate [simp]:
"lookup (tabulate ks f) = (Some o f) |` set ks"
by (induct ks) (auto simp add: tabulate_def restrict_map_def expand_fun_eq)
@@ -122,6 +136,14 @@
"bulkload xs = tabulate [0..<length xs] (nth xs)"
by (rule mapping_eqI) (simp add: expand_fun_eq)
+lemma keys_tabulate:
+ "keys (tabulate ks f) = set ks"
+ by (simp add: tabulate_def keys_def map_of_map_restrict o_def)
+
+lemma keys_bulkload:
+ "keys (bulkload xs) = {0..<length xs}"
+ by (simp add: keys_tabulate bulkload_tabulate)
+
lemma is_empty_empty:
"is_empty m \<longleftrightarrow> m = Mapping Map.empty"
by (cases m) (simp add: is_empty_def)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/More_List.thy Thu May 20 19:55:42 2010 +0200
@@ -0,0 +1,267 @@
+(* Author: Florian Haftmann, TU Muenchen *)
+
+header {* Operations on lists beyond the standard List theory *}
+
+theory More_List
+imports Main
+begin
+
+hide_const (open) Finite_Set.fold
+
+text {* Repairing code generator setup *}
+
+declare (in lattice) Inf_fin_set_fold [code_unfold del]
+declare (in lattice) Sup_fin_set_fold [code_unfold del]
+declare (in linorder) Min_fin_set_fold [code_unfold del]
+declare (in linorder) Max_fin_set_fold [code_unfold del]
+declare (in complete_lattice) Inf_set_fold [code_unfold del]
+declare (in complete_lattice) Sup_set_fold [code_unfold del]
+declare rev_foldl_cons [code del]
+
+text {* Fold combinator with canonical argument order *}
+
+primrec fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where
+ "fold f [] = id"
+ | "fold f (x # xs) = fold f xs \<circ> f x"
+
+lemma foldl_fold:
+ "foldl f s xs = fold (\<lambda>x s. f s x) xs s"
+ by (induct xs arbitrary: s) simp_all
+
+lemma foldr_fold_rev:
+ "foldr f xs = fold f (rev xs)"
+ by (simp add: foldr_foldl foldl_fold expand_fun_eq)
+
+lemma fold_rev_conv [code_unfold]:
+ "fold f (rev xs) = foldr f xs"
+ by (simp add: foldr_fold_rev)
+
+lemma fold_cong [fundef_cong, recdef_cong]:
+ "a = b \<Longrightarrow> xs = ys \<Longrightarrow> (\<And>x. x \<in> set xs \<Longrightarrow> f x = g x)
+ \<Longrightarrow> fold f xs a = fold g ys b"
+ by (induct ys arbitrary: a b xs) simp_all
+
+lemma fold_id:
+ assumes "\<And>x. x \<in> set xs \<Longrightarrow> f x = id"
+ shows "fold f xs = id"
+ using assms by (induct xs) simp_all
+
+lemma fold_apply:
+ assumes "\<And>x. x \<in> set xs \<Longrightarrow> h \<circ> g x = f x \<circ> h"
+ shows "h \<circ> fold g xs = fold f xs \<circ> h"
+ using assms by (induct xs) (simp_all add: expand_fun_eq)
+
+lemma fold_invariant:
+ assumes "\<And>x. x \<in> set xs \<Longrightarrow> Q x" and "P s"
+ and "\<And>x s. Q x \<Longrightarrow> P s \<Longrightarrow> P (f x s)"
+ shows "P (fold f xs s)"
+ using assms by (induct xs arbitrary: s) simp_all
+
+lemma fold_weak_invariant:
+ assumes "P s"
+ and "\<And>s x. x \<in> set xs \<Longrightarrow> P s \<Longrightarrow> P (f x s)"
+ shows "P (fold f xs s)"
+ using assms by (induct xs arbitrary: s) simp_all
+
+lemma fold_append [simp]:
+ "fold f (xs @ ys) = fold f ys \<circ> fold f xs"
+ by (induct xs) simp_all
+
+lemma fold_map [code_unfold]:
+ "fold g (map f xs) = fold (g o f) xs"
+ by (induct xs) simp_all
+
+lemma fold_rev:
+ assumes "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f y \<circ> f x = f x \<circ> f y"
+ shows "fold f (rev xs) = fold f xs"
+ using assms by (induct xs) (simp_all del: o_apply add: fold_apply)
+
+lemma foldr_fold:
+ assumes "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f y \<circ> f x = f x \<circ> f y"
+ shows "foldr f xs = fold f xs"
+ using assms unfolding foldr_fold_rev by (rule fold_rev)
+
+lemma fold_Cons_rev:
+ "fold Cons xs = append (rev xs)"
+ by (induct xs) simp_all
+
+lemma rev_conv_fold [code]:
+ "rev xs = fold Cons xs []"
+ by (simp add: fold_Cons_rev)
+
+lemma fold_append_concat_rev:
+ "fold append xss = append (concat (rev xss))"
+ by (induct xss) simp_all
+
+lemma concat_conv_foldr [code]:
+ "concat xss = foldr append xss []"
+ by (simp add: fold_append_concat_rev foldr_fold_rev)
+
+lemma fold_plus_listsum_rev:
+ "fold plus xs = plus (listsum (rev xs))"
+ by (induct xs) (simp_all add: add.assoc)
+
+lemma listsum_conv_foldr [code]:
+ "listsum xs = foldr plus xs 0"
+ by (fact listsum_foldr)
+
+lemma sort_key_conv_fold:
+ assumes "inj_on f (set xs)"
+ shows "sort_key f xs = fold (insort_key f) xs []"
+proof -
+ have "fold (insort_key f) (rev xs) = fold (insort_key f) xs"
+ proof (rule fold_rev, rule ext)
+ fix zs
+ fix x y
+ assume "x \<in> set xs" "y \<in> set xs"
+ with assms have *: "f y = f x \<Longrightarrow> y = x" by (auto dest: inj_onD)
+ show "(insort_key f y \<circ> insort_key f x) zs = (insort_key f x \<circ> insort_key f y) zs"
+ by (induct zs) (auto dest: *)
+ qed
+ then show ?thesis by (simp add: sort_key_def foldr_fold_rev)
+qed
+
+lemma sort_conv_fold:
+ "sort xs = fold insort xs []"
+ by (rule sort_key_conv_fold) simp
+
+text {* @{const Finite_Set.fold} and @{const fold} *}
+
+lemma (in fun_left_comm) fold_set_remdups:
+ "Finite_Set.fold f y (set xs) = fold f (remdups xs) y"
+ by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm insert_absorb)
+
+lemma (in fun_left_comm_idem) fold_set:
+ "Finite_Set.fold f y (set xs) = fold f xs y"
+ by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm)
+
+lemma (in ab_semigroup_idem_mult) fold1_set:
+ assumes "xs \<noteq> []"
+ shows "Finite_Set.fold1 times (set xs) = fold times (tl xs) (hd xs)"
+proof -
+ interpret fun_left_comm_idem times by (fact fun_left_comm_idem)
+ from assms obtain y ys where xs: "xs = y # ys"
+ by (cases xs) auto
+ show ?thesis
+ proof (cases "set ys = {}")
+ case True with xs show ?thesis by simp
+ next
+ case False
+ then have "fold1 times (insert y (set ys)) = Finite_Set.fold times y (set ys)"
+ by (simp only: finite_set fold1_eq_fold_idem)
+ with xs show ?thesis by (simp add: fold_set mult_commute)
+ qed
+qed
+
+lemma (in lattice) Inf_fin_set_fold:
+ "Inf_fin (set (x # xs)) = fold inf xs x"
+proof -
+ interpret ab_semigroup_idem_mult "inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
+ by (fact ab_semigroup_idem_mult_inf)
+ show ?thesis
+ by (simp add: Inf_fin_def fold1_set del: set.simps)
+qed
+
+lemma (in lattice) Inf_fin_set_foldr [code_unfold]:
+ "Inf_fin (set (x # xs)) = foldr inf xs x"
+ by (simp add: Inf_fin_set_fold ac_simps foldr_fold expand_fun_eq del: set.simps)
+
+lemma (in lattice) Sup_fin_set_fold:
+ "Sup_fin (set (x # xs)) = fold sup xs x"
+proof -
+ interpret ab_semigroup_idem_mult "sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
+ by (fact ab_semigroup_idem_mult_sup)
+ show ?thesis
+ by (simp add: Sup_fin_def fold1_set del: set.simps)
+qed
+
+lemma (in lattice) Sup_fin_set_foldr [code_unfold]:
+ "Sup_fin (set (x # xs)) = foldr sup xs x"
+ by (simp add: Sup_fin_set_fold ac_simps foldr_fold expand_fun_eq del: set.simps)
+
+lemma (in linorder) Min_fin_set_fold:
+ "Min (set (x # xs)) = fold min xs x"
+proof -
+ interpret ab_semigroup_idem_mult "min :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
+ by (fact ab_semigroup_idem_mult_min)
+ show ?thesis
+ by (simp add: Min_def fold1_set del: set.simps)
+qed
+
+lemma (in linorder) Min_fin_set_foldr [code_unfold]:
+ "Min (set (x # xs)) = foldr min xs x"
+ by (simp add: Min_fin_set_fold ac_simps foldr_fold expand_fun_eq del: set.simps)
+
+lemma (in linorder) Max_fin_set_fold:
+ "Max (set (x # xs)) = fold max xs x"
+proof -
+ interpret ab_semigroup_idem_mult "max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
+ by (fact ab_semigroup_idem_mult_max)
+ show ?thesis
+ by (simp add: Max_def fold1_set del: set.simps)
+qed
+
+lemma (in linorder) Max_fin_set_foldr [code_unfold]:
+ "Max (set (x # xs)) = foldr max xs x"
+ by (simp add: Max_fin_set_fold ac_simps foldr_fold expand_fun_eq del: set.simps)
+
+lemma (in complete_lattice) Inf_set_fold:
+ "Inf (set xs) = fold inf xs top"
+proof -
+ interpret fun_left_comm_idem "inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
+ by (fact fun_left_comm_idem_inf)
+ show ?thesis by (simp add: Inf_fold_inf fold_set inf_commute)
+qed
+
+lemma (in complete_lattice) Inf_set_foldr [code_unfold]:
+ "Inf (set xs) = foldr inf xs top"
+ by (simp add: Inf_set_fold ac_simps foldr_fold expand_fun_eq)
+
+lemma (in complete_lattice) Sup_set_fold:
+ "Sup (set xs) = fold sup xs bot"
+proof -
+ interpret fun_left_comm_idem "sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
+ by (fact fun_left_comm_idem_sup)
+ show ?thesis by (simp add: Sup_fold_sup fold_set sup_commute)
+qed
+
+lemma (in complete_lattice) Sup_set_foldr [code_unfold]:
+ "Sup (set xs) = foldr sup xs bot"
+ by (simp add: Sup_set_fold ac_simps foldr_fold expand_fun_eq)
+
+lemma (in complete_lattice) INFI_set_fold:
+ "INFI (set xs) f = fold (inf \<circ> f) xs top"
+ unfolding INFI_def set_map [symmetric] Inf_set_fold fold_map ..
+
+lemma (in complete_lattice) SUPR_set_fold:
+ "SUPR (set xs) f = fold (sup \<circ> f) xs bot"
+ unfolding SUPR_def set_map [symmetric] Sup_set_fold fold_map ..
+
+text {* @{text nth_map} *}
+
+definition nth_map :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+ "nth_map n f xs = (if n < length xs then
+ take n xs @ [f (xs ! n)] @ drop (Suc n) xs
+ else xs)"
+
+lemma nth_map_id:
+ "n \<ge> length xs \<Longrightarrow> nth_map n f xs = xs"
+ by (simp add: nth_map_def)
+
+lemma nth_map_unfold:
+ "n < length xs \<Longrightarrow> nth_map n f xs = take n xs @ [f (xs ! n)] @ drop (Suc n) xs"
+ by (simp add: nth_map_def)
+
+lemma nth_map_Nil [simp]:
+ "nth_map n f [] = []"
+ by (simp add: nth_map_def)
+
+lemma nth_map_zero [simp]:
+ "nth_map 0 f (x # xs) = f x # xs"
+ by (simp add: nth_map_def)
+
+lemma nth_map_Suc [simp]:
+ "nth_map (Suc n) f (x # xs) = x # nth_map n f xs"
+ by (simp add: nth_map_def)
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/More_Set.thy Thu May 20 19:55:42 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/Library/RBT.thy Thu May 20 16:25:22 2010 +0200
+++ b/src/HOL/Library/RBT.thy Thu May 20 19:55:42 2010 +0200
@@ -136,7 +136,7 @@
lemma lookup_map_entry [simp]:
"lookup (map_entry k f t) = (lookup t)(k := Option.map f (lookup t k))"
- by (simp add: map_entry_def lookup_RBT lookup_map_entry lookup_impl_of)
+ by (simp add: map_entry_def lookup_RBT RBT_Impl.lookup_map_entry lookup_impl_of)
lemma lookup_map [simp]:
"lookup (map f t) k = Option.map (f k) (lookup t k)"
@@ -191,7 +191,11 @@
by (rule mapping_eqI) simp
lemma delete_Mapping [code]:
- "Mapping.delete k (Mapping xs) = Mapping (delete k xs)"
+ "Mapping.delete k (Mapping t) = Mapping (delete k t)"
+ by (rule mapping_eqI) simp
+
+lemma map_entry_Mapping [code]:
+ "Mapping.map_entry k f (Mapping t) = Mapping (map_entry k f t)"
by (rule mapping_eqI) simp
lemma keys_Mapping [code]:
--- a/src/HOL/List.thy Thu May 20 16:25:22 2010 +0200
+++ b/src/HOL/List.thy Thu May 20 19:55:42 2010 +0200
@@ -4491,11 +4491,8 @@
subsubsection {* Generation of efficient code *}
-primrec
- member :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" (infixl "mem" 55)
-where
- "x mem [] \<longleftrightarrow> False"
- | "x mem (y#ys) \<longleftrightarrow> x = y \<or> x mem ys"
+definition member :: "'a list \<Rightarrow> 'a \<Rightarrow> bool" where
+ mem_iff [code_post]: "member xs x \<longleftrightarrow> x \<in> set xs"
primrec
null:: "'a list \<Rightarrow> bool"
@@ -4551,7 +4548,7 @@
| "concat_map f (x#xs) = f x @ concat_map f xs"
text {*
- Only use @{text mem} for generating executable code. Otherwise use
+ Only use @{text member} for generating executable code. Otherwise use
@{prop "x : set xs"} instead --- it is much easier to reason about.
The same is true for @{const list_all} and @{const list_ex}: write
@{text "\<forall>x\<in>set xs"} and @{text "\<exists>x\<in>set xs"} instead because the HOL
@@ -4583,12 +4580,20 @@
show ?case by (induct xs) (auto simp add: Cons aux)
qed
-lemma mem_iff [code_post]:
- "x mem xs \<longleftrightarrow> x \<in> set xs"
-by (induct xs) auto
-
lemmas in_set_code [code_unfold] = mem_iff [symmetric]
+lemma member_simps [simp, code]:
+ "member [] y \<longleftrightarrow> False"
+ "member (x # xs) y \<longleftrightarrow> x = y \<or> member xs y"
+ by (auto simp add: mem_iff)
+
+lemma member_set:
+ "member = set"
+ by (simp add: expand_fun_eq mem_iff mem_def)
+
+abbreviation (input) mem :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" (infixl "mem" 55) where
+ "x mem xs \<equiv> member xs x" -- "for backward compatibility"
+
lemma empty_null:
"xs = [] \<longleftrightarrow> null xs"
by (cases xs) simp_all
--- a/src/HOL/MicroJava/BV/BVExample.thy Thu May 20 16:25:22 2010 +0200
+++ b/src/HOL/MicroJava/BV/BVExample.thy Thu May 20 19:55:42 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
--- a/src/HOL/ex/Codegenerator_Candidates.thy Thu May 20 16:25:22 2010 +0200
+++ b/src/HOL/ex/Codegenerator_Candidates.thy Thu May 20 19:55:42 2010 +0200
@@ -13,6 +13,7 @@
Fset
Enum
List_Prefix
+ More_List
Nat_Infinity
Nested_Environment
Option_ord