1.1 --- a/NEWS Thu May 20 16:25:22 2010 +0200
1.2 +++ b/NEWS Thu May 20 19:55:42 2010 +0200
1.3 @@ -143,6 +143,9 @@
1.4
1.5 *** HOL ***
1.6
1.7 +* List membership infix mem operation is only an input abbreviation.
1.8 +INCOMPATIBILITY.
1.9 +
1.10 * Theory Library/Word.thy has been removed. Use library Word/Word.thy for
1.11 future developements; former Library/Word.thy is still present in the AFP
1.12 entry RSAPPS.
2.1 --- a/src/HOL/IsaMakefile Thu May 20 16:25:22 2010 +0200
2.2 +++ b/src/HOL/IsaMakefile Thu May 20 19:55:42 2010 +0200
2.3 @@ -401,16 +401,16 @@
2.4 Library/Efficient_Nat.thy Library/Sum_Of_Squares.thy \
2.5 Library/Dlist.thy Library/Sum_Of_Squares/sos_wrapper.ML \
2.6 Library/Sum_Of_Squares/sum_of_squares.ML Library/Fset.thy \
2.7 - Library/Glbs.thy Library/Executable_Set.thy \
2.8 + Library/Glbs.thy Library/Executable_Set.thy \
2.9 Library/Infinite_Set.thy Library/FuncSet.thy \
2.10 Library/Permutations.thy Library/Bit.thy Library/FrechetDeriv.thy \
2.11 Library/Fraction_Field.thy Library/Fundamental_Theorem_Algebra.thy \
2.12 Library/Inner_Product.thy Library/Kleene_Algebra.thy \
2.13 Library/Lattice_Algebras.thy Library/Lattice_Syntax.thy \
2.14 - Library/Library.thy Library/List_Prefix.thy Library/List_Set.thy \
2.15 - Library/State_Monad.thy Library/Multiset.thy Library/Permutation.thy \
2.16 + Library/Library.thy Library/List_Prefix.thy Library/More_Set.thy \
2.17 + Library/More_List.thy Library/Multiset.thy Library/Permutation.thy \
2.18 Library/Quotient_Type.thy Library/Quicksort.thy \
2.19 - Library/Nat_Infinity.thy Library/README.html \
2.20 + Library/Nat_Infinity.thy Library/README.html Library/State_Monad.thy \
2.21 Library/Continuity.thy Library/Order_Relation.thy \
2.22 Library/Nested_Environment.thy Library/Ramsey.thy Library/Zorn.thy \
2.23 Library/Library/ROOT.ML Library/Library/document/root.tex \
2.24 @@ -433,7 +433,7 @@
2.25 Library/Nat_Bijection.thy $(SRC)/Tools/float.ML \
2.26 $(SRC)/HOL/Tools/float_arith.ML Library/positivstellensatz.ML \
2.27 Library/reify_data.ML Library/reflection.ML Library/LaTeXsugar.thy \
2.28 - Library/OptionalSugar.thy Library/Convex.thy \
2.29 + Library/OptionalSugar.thy Library/Convex.thy \
2.30 Library/Predicate_Compile_Quickcheck.thy Library/SML_Quickcheck.thy
2.31 @cd Library; $(ISABELLE_TOOL) usedir $(OUT)/HOL Library
2.32
2.33 @@ -586,17 +586,18 @@
2.34
2.35 HOL-Old_Number_Theory: HOL $(LOG)/HOL-Old_Number_Theory.gz
2.36
2.37 -$(LOG)/HOL-Old_Number_Theory.gz: $(OUT)/HOL Library/Permutation.thy \
2.38 - Old_Number_Theory/Primes.thy Old_Number_Theory/Fib.thy \
2.39 - Old_Number_Theory/Factorization.thy Old_Number_Theory/BijectionRel.thy \
2.40 - Old_Number_Theory/Chinese.thy Old_Number_Theory/EulerFermat.thy \
2.41 - Old_Number_Theory/IntFact.thy Old_Number_Theory/IntPrimes.thy \
2.42 - Old_Number_Theory/WilsonBij.thy Old_Number_Theory/WilsonRuss.thy \
2.43 - Old_Number_Theory/Finite2.thy Old_Number_Theory/Int2.thy \
2.44 - Old_Number_Theory/EvenOdd.thy Old_Number_Theory/Residues.thy \
2.45 - Old_Number_Theory/Euler.thy Old_Number_Theory/Gauss.thy \
2.46 +$(LOG)/HOL-Old_Number_Theory.gz: $(OUT)/HOL Library/Permutation.thy \
2.47 + Old_Number_Theory/Primes.thy Old_Number_Theory/Fib.thy \
2.48 + Old_Number_Theory/Factorization.thy Old_Number_Theory/BijectionRel.thy\
2.49 + Old_Number_Theory/Chinese.thy Old_Number_Theory/EulerFermat.thy \
2.50 + Old_Number_Theory/IntFact.thy Old_Number_Theory/IntPrimes.thy \
2.51 + Old_Number_Theory/WilsonBij.thy Old_Number_Theory/WilsonRuss.thy \
2.52 + Old_Number_Theory/Finite2.thy Old_Number_Theory/Int2.thy \
2.53 + Old_Number_Theory/EvenOdd.thy Old_Number_Theory/Residues.thy \
2.54 + Old_Number_Theory/Euler.thy Old_Number_Theory/Gauss.thy \
2.55 Old_Number_Theory/Quadratic_Reciprocity.thy Library/Infinite_Set.thy \
2.56 - Old_Number_Theory/Legacy_GCD.thy Old_Number_Theory/Pocklington.thy Old_Number_Theory/ROOT.ML
2.57 + Old_Number_Theory/Legacy_GCD.thy Old_Number_Theory/Pocklington.thy \
2.58 + Old_Number_Theory/ROOT.ML
2.59 @$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Old_Number_Theory
2.60
2.61
2.62 @@ -711,9 +712,9 @@
2.63 HOL-Auth: HOL $(LOG)/HOL-Auth.gz
2.64
2.65 $(LOG)/HOL-Auth.gz: $(OUT)/HOL \
2.66 - Auth/Auth_Shared.thy Auth/Auth_Public.thy Auth/All_Symmetric.thy \
2.67 - Auth/Guard/Auth_Guard_Shared.thy \
2.68 - Auth/Guard/Auth_Guard_Public.thy \
2.69 + Auth/Auth_Shared.thy Auth/Auth_Public.thy Auth/All_Symmetric.thy \
2.70 + Auth/Guard/Auth_Guard_Shared.thy \
2.71 + Auth/Guard/Auth_Guard_Public.thy \
2.72 Auth/Smartcard/Auth_Smartcard.thy Auth/All_Symmetric.thy \
2.73 Auth/CertifiedEmail.thy Auth/Event.thy Auth/Message.thy \
2.74 Auth/NS_Public.thy Auth/NS_Public_Bad.thy Auth/NS_Shared.thy \
3.1 --- a/src/HOL/Library/Dlist.thy Thu May 20 16:25:22 2010 +0200
3.2 +++ b/src/HOL/Library/Dlist.thy Thu May 20 19:55:42 2010 +0200
3.3 @@ -3,42 +3,9 @@
3.4 header {* Lists with elements distinct as canonical example for datatype invariants *}
3.5
3.6 theory Dlist
3.7 -imports Main Fset
3.8 +imports Main More_List Fset
3.9 begin
3.10
3.11 -section {* Prelude *}
3.12 -
3.13 -text {* Without canonical argument order, higher-order things tend to get confusing quite fast: *}
3.14 -
3.15 -setup {* Sign.map_naming (Name_Space.add_path "List") *}
3.16 -
3.17 -primrec member :: "'a list \<Rightarrow> 'a \<Rightarrow> bool" where
3.18 - "member [] y \<longleftrightarrow> False"
3.19 - | "member (x#xs) y \<longleftrightarrow> x = y \<or> member xs y"
3.20 -
3.21 -lemma member_set:
3.22 - "member = set"
3.23 -proof (rule ext)+
3.24 - fix xs :: "'a list" and x :: 'a
3.25 - have "member xs x \<longleftrightarrow> x \<in> set xs" by (induct xs) auto
3.26 - then show "member xs x = set xs x" by (simp add: mem_def)
3.27 -qed
3.28 -
3.29 -lemma not_set_compl:
3.30 - "Not \<circ> set xs = - set xs"
3.31 - by (simp add: fun_Compl_def bool_Compl_def comp_def expand_fun_eq)
3.32 -
3.33 -primrec fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where
3.34 - "fold f [] s = s"
3.35 - | "fold f (x#xs) s = fold f xs (f x s)"
3.36 -
3.37 -lemma foldl_fold:
3.38 - "foldl f s xs = List.fold (\<lambda>x s. f s x) xs s"
3.39 - by (induct xs arbitrary: s) simp_all
3.40 -
3.41 -setup {* Sign.map_naming Name_Space.parent_path *}
3.42 -
3.43 -
3.44 section {* The type of distinct lists *}
3.45
3.46 typedef (open) 'a dlist = "{xs::'a list. distinct xs}"
3.47 @@ -101,7 +68,10 @@
3.48 "length dxs = List.length (list_of_dlist dxs)"
3.49
3.50 definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b \<Rightarrow> 'b" where
3.51 - "fold f dxs = List.fold f (list_of_dlist dxs)"
3.52 + "fold f dxs = More_List.fold f (list_of_dlist dxs)"
3.53 +
3.54 +definition foldr :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b \<Rightarrow> 'b" where
3.55 + "foldr f dxs = List.foldr f (list_of_dlist dxs)"
3.56
3.57
3.58 section {* Executable version obeying invariant *}
3.59 @@ -153,6 +123,8 @@
3.60 declare UNIV_Set [code del]
3.61 declare insert_Set [code del]
3.62 declare remove_Set [code del]
3.63 +declare compl_Set [code del]
3.64 +declare compl_Coset [code del]
3.65 declare map_Set [code del]
3.66 declare filter_Set [code del]
3.67 declare forall_Set [code del]
3.68 @@ -215,6 +187,11 @@
3.69 "Fset.member (Coset dxs) = Not \<circ> member dxs"
3.70 by (simp_all add: member_def)
3.71
3.72 +lemma compl_code [code]:
3.73 + "- Set dxs = Coset dxs"
3.74 + "- Coset dxs = Set dxs"
3.75 + by (simp_all add: not_set_compl member_set)
3.76 +
3.77 lemma map_code [code]:
3.78 "Fset.map f (Set dxs) = Set (map f dxs)"
3.79 by (simp add: member_set)
3.80 @@ -235,38 +212,34 @@
3.81 "Fset.card (Set dxs) = length dxs"
3.82 by (simp add: length_def member_set distinct_card)
3.83
3.84 -lemma foldl_list_of_dlist:
3.85 - "foldl f s (list_of_dlist dxs) = fold (\<lambda>x s. f s x) dxs s"
3.86 - by (simp add: foldl_fold fold_def)
3.87 -
3.88 lemma inter_code [code]:
3.89 "inf A (Set xs) = Set (filter (Fset.member A) xs)"
3.90 - "inf A (Coset xs) = fold Fset.remove xs A"
3.91 - by (simp_all only: Set_def Coset_def foldl_list_of_dlist inter_project list_of_dlist_filter)
3.92 + "inf A (Coset xs) = foldr Fset.remove xs A"
3.93 + by (simp_all only: Set_def Coset_def foldr_def inter_project list_of_dlist_filter)
3.94
3.95 lemma subtract_code [code]:
3.96 - "A - Set xs = fold Fset.remove xs A"
3.97 + "A - Set xs = foldr Fset.remove xs A"
3.98 "A - Coset xs = Set (filter (Fset.member A) xs)"
3.99 - by (simp_all only: Set_def Coset_def foldl_list_of_dlist subtract_remove list_of_dlist_filter)
3.100 + by (simp_all only: Set_def Coset_def foldr_def subtract_remove list_of_dlist_filter)
3.101
3.102 lemma union_code [code]:
3.103 - "sup (Set xs) A = fold Fset.insert xs A"
3.104 + "sup (Set xs) A = foldr Fset.insert xs A"
3.105 "sup (Coset xs) A = Coset (filter (Not \<circ> Fset.member A) xs)"
3.106 - by (simp_all only: Set_def Coset_def foldl_list_of_dlist union_insert list_of_dlist_filter)
3.107 + by (simp_all only: Set_def Coset_def foldr_def union_insert list_of_dlist_filter)
3.108
3.109 context complete_lattice
3.110 begin
3.111
3.112 lemma Infimum_code [code]:
3.113 - "Infimum (Set As) = fold inf As top"
3.114 - by (simp only: Set_def Infimum_inf foldl_list_of_dlist inf.commute)
3.115 + "Infimum (Set As) = foldr inf As top"
3.116 + by (simp only: Set_def Infimum_inf foldr_def inf.commute)
3.117
3.118 lemma Supremum_code [code]:
3.119 - "Supremum (Set As) = fold sup As bot"
3.120 - by (simp only: Set_def Supremum_sup foldl_list_of_dlist sup.commute)
3.121 + "Supremum (Set As) = foldr sup As bot"
3.122 + by (simp only: Set_def Supremum_sup foldr_def sup.commute)
3.123
3.124 end
3.125
3.126 -hide_const (open) member fold empty insert remove map filter null member length fold
3.127 +hide_const (open) member fold foldr empty insert remove map filter null member length fold
3.128
3.129 end
4.1 --- a/src/HOL/Library/Executable_Set.thy Thu May 20 16:25:22 2010 +0200
4.2 +++ b/src/HOL/Library/Executable_Set.thy Thu May 20 19:55:42 2010 +0200
4.3 @@ -6,7 +6,7 @@
4.4 header {* A crude implementation of finite sets by lists -- avoid using this at any cost! *}
4.5
4.6 theory Executable_Set
4.7 -imports List_Set
4.8 +imports More_Set
4.9 begin
4.10
4.11 declare mem_def [code del]
4.12 @@ -50,8 +50,8 @@
4.13 by simp
4.14
4.15 lemma [code]:
4.16 - "x \<in> Set xs \<longleftrightarrow> member x xs"
4.17 - "x \<in> Coset xs \<longleftrightarrow> \<not> member x xs"
4.18 + "x \<in> Set xs \<longleftrightarrow> member xs x"
4.19 + "x \<in> Coset xs \<longleftrightarrow> \<not> member xs x"
4.20 by (simp_all add: mem_iff)
4.21
4.22 definition is_empty :: "'a set \<Rightarrow> bool" where
4.23 @@ -76,9 +76,9 @@
4.24 Code.add_signature_cmd ("is_empty", "'a set \<Rightarrow> bool")
4.25 #> Code.add_signature_cmd ("empty", "'a set")
4.26 #> Code.add_signature_cmd ("insert", "'a \<Rightarrow> 'a set \<Rightarrow> 'a set")
4.27 - #> Code.add_signature_cmd ("List_Set.remove", "'a \<Rightarrow> 'a set \<Rightarrow> 'a set")
4.28 + #> Code.add_signature_cmd ("More_Set.remove", "'a \<Rightarrow> 'a set \<Rightarrow> 'a set")
4.29 #> Code.add_signature_cmd ("image", "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'b set")
4.30 - #> Code.add_signature_cmd ("List_Set.project", "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set")
4.31 + #> Code.add_signature_cmd ("More_Set.project", "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set")
4.32 #> Code.add_signature_cmd ("Ball", "'a set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool")
4.33 #> Code.add_signature_cmd ("Bex", "'a set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool")
4.34 #> Code.add_signature_cmd ("card", "'a set \<Rightarrow> nat")
4.35 @@ -232,36 +232,36 @@
4.36
4.37 lemma inter_project [code]:
4.38 "inter A (Set xs) = Set (List.filter (\<lambda>x. x \<in> A) xs)"
4.39 - "inter A (Coset xs) = foldl (\<lambda>A x. remove x A) A xs"
4.40 - by (simp add: inter project_def, simp add: Diff_eq [symmetric] minus_set)
4.41 + "inter A (Coset xs) = foldr remove xs A"
4.42 + by (simp add: inter project_def) (simp add: Diff_eq [symmetric] minus_set_foldr)
4.43
4.44 lemma subtract_remove [code]:
4.45 - "subtract (Set xs) A = foldl (\<lambda>A x. remove x A) A xs"
4.46 + "subtract (Set xs) A = foldr remove xs A"
4.47 "subtract (Coset xs) A = Set (List.filter (\<lambda>x. x \<in> A) xs)"
4.48 - by (auto simp add: minus_set)
4.49 + by (auto simp add: minus_set_foldr)
4.50
4.51 lemma union_insert [code]:
4.52 - "union (Set xs) A = foldl (\<lambda>A x. insert x A) A xs"
4.53 + "union (Set xs) A = foldr insert xs A"
4.54 "union (Coset xs) A = Coset (List.filter (\<lambda>x. x \<notin> A) xs)"
4.55 - by (auto simp add: union_set)
4.56 + by (auto simp add: union_set_foldr)
4.57
4.58 lemma Inf_inf [code]:
4.59 - "Inf (Set xs) = foldl inf (top :: 'a::complete_lattice) xs"
4.60 + "Inf (Set xs) = foldr inf xs (top :: 'a::complete_lattice)"
4.61 "Inf (Coset []) = (bot :: 'a::complete_lattice)"
4.62 - by (simp_all add: Inf_UNIV Inf_set_fold)
4.63 + by (simp_all add: Inf_UNIV Inf_set_foldr)
4.64
4.65 lemma Sup_sup [code]:
4.66 - "Sup (Set xs) = foldl sup (bot :: 'a::complete_lattice) xs"
4.67 + "Sup (Set xs) = foldr sup xs (bot :: 'a::complete_lattice)"
4.68 "Sup (Coset []) = (top :: 'a::complete_lattice)"
4.69 - by (simp_all add: Sup_UNIV Sup_set_fold)
4.70 + by (simp_all add: Sup_UNIV Sup_set_foldr)
4.71
4.72 lemma Inter_inter [code]:
4.73 - "Inter (Set xs) = foldl inter (Coset []) xs"
4.74 + "Inter (Set xs) = foldr inter xs (Coset [])"
4.75 "Inter (Coset []) = empty"
4.76 unfolding Inter_def Inf_inf by simp_all
4.77
4.78 lemma Union_union [code]:
4.79 - "Union (Set xs) = foldl union empty xs"
4.80 + "Union (Set xs) = foldr union xs empty"
4.81 "Union (Coset []) = Coset []"
4.82 unfolding Union_def Sup_sup by simp_all
4.83
5.1 --- a/src/HOL/Library/Fset.thy Thu May 20 16:25:22 2010 +0200
5.2 +++ b/src/HOL/Library/Fset.thy Thu May 20 19:55:42 2010 +0200
5.3 @@ -4,7 +4,7 @@
5.4 header {* Executable finite sets *}
5.5
5.6 theory Fset
5.7 -imports List_Set
5.8 +imports More_Set More_List
5.9 begin
5.10
5.11 declare mem_def [simp]
5.12 @@ -41,9 +41,9 @@
5.13 code_datatype Set Coset
5.14
5.15 lemma member_code [code]:
5.16 - "member (Set xs) y \<longleftrightarrow> List.member y xs"
5.17 - "member (Coset xs) y \<longleftrightarrow> \<not> List.member y xs"
5.18 - by (simp_all add: mem_iff fun_Compl_def bool_Compl_def)
5.19 + "member (Set xs) = List.member xs"
5.20 + "member (Coset xs) = Not \<circ> List.member xs"
5.21 + by (simp_all add: expand_fun_eq mem_iff fun_Compl_def bool_Compl_def)
5.22
5.23 lemma member_image_UNIV [simp]:
5.24 "member ` UNIV = UNIV"
5.25 @@ -105,10 +105,11 @@
5.26
5.27 end
5.28
5.29 +
5.30 subsection {* Basic operations *}
5.31
5.32 definition is_empty :: "'a fset \<Rightarrow> bool" where
5.33 - [simp]: "is_empty A \<longleftrightarrow> List_Set.is_empty (member A)"
5.34 + [simp]: "is_empty A \<longleftrightarrow> More_Set.is_empty (member A)"
5.35
5.36 lemma is_empty_Set [code]:
5.37 "is_empty (Set xs) \<longleftrightarrow> null xs"
5.38 @@ -128,16 +129,16 @@
5.39 lemma insert_Set [code]:
5.40 "insert x (Set xs) = Set (List.insert x xs)"
5.41 "insert x (Coset xs) = Coset (removeAll x xs)"
5.42 - by (simp_all add: Set_def Coset_def set_insert)
5.43 + by (simp_all add: Set_def Coset_def)
5.44
5.45 definition remove :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
5.46 - [simp]: "remove x A = Fset (List_Set.remove x (member A))"
5.47 + [simp]: "remove x A = Fset (More_Set.remove x (member A))"
5.48
5.49 lemma remove_Set [code]:
5.50 "remove x (Set xs) = Set (removeAll x xs)"
5.51 "remove x (Coset xs) = Coset (List.insert x xs)"
5.52 by (simp_all add: Set_def Coset_def remove_set_compl)
5.53 - (simp add: List_Set.remove_def)
5.54 + (simp add: More_Set.remove_def)
5.55
5.56 definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset" where
5.57 [simp]: "map f A = Fset (image f (member A))"
5.58 @@ -147,7 +148,7 @@
5.59 by (simp add: Set_def)
5.60
5.61 definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
5.62 - [simp]: "filter P A = Fset (List_Set.project P (member A))"
5.63 + [simp]: "filter P A = Fset (More_Set.project P (member A))"
5.64
5.65 lemma filter_Set [code]:
5.66 "filter P (Set xs) = Set (List.filter P xs)"
5.67 @@ -175,9 +176,17 @@
5.68 proof -
5.69 have "Finite_Set.card (set (remdups xs)) = length (remdups xs)"
5.70 by (rule distinct_card) simp
5.71 - then show ?thesis by (simp add: Set_def card_def)
5.72 + then show ?thesis by (simp add: Set_def)
5.73 qed
5.74
5.75 +lemma compl_Set [simp, code]:
5.76 + "- Set xs = Coset xs"
5.77 + by (simp add: Set_def Coset_def)
5.78 +
5.79 +lemma compl_Coset [simp, code]:
5.80 + "- Coset xs = Set xs"
5.81 + by (simp add: Set_def Coset_def)
5.82 +
5.83
5.84 subsection {* Derived operations *}
5.85
5.86 @@ -198,39 +207,49 @@
5.87
5.88 lemma inter_project [code]:
5.89 "inf A (Set xs) = Set (List.filter (member A) xs)"
5.90 - "inf A (Coset xs) = foldl (\<lambda>A x. remove x A) A xs"
5.91 + "inf A (Coset xs) = foldr remove xs A"
5.92 proof -
5.93 show "inf A (Set xs) = Set (List.filter (member A) xs)"
5.94 by (simp add: inter project_def Set_def)
5.95 - have "foldl (\<lambda>A x. List_Set.remove x A) (member A) xs =
5.96 - member (foldl (\<lambda>A x. Fset (List_Set.remove x (member A))) A xs)"
5.97 - by (rule foldl_apply) (simp add: expand_fun_eq)
5.98 - then show "inf A (Coset xs) = foldl (\<lambda>A x. remove x A) A xs"
5.99 - by (simp add: Diff_eq [symmetric] minus_set)
5.100 + have *: "\<And>x::'a. remove = (\<lambda>x. Fset \<circ> More_Set.remove x \<circ> member)"
5.101 + by (simp add: expand_fun_eq)
5.102 + have "member \<circ> fold (\<lambda>x. Fset \<circ> More_Set.remove x \<circ> member) xs =
5.103 + fold More_Set.remove xs \<circ> member"
5.104 + by (rule fold_apply) (simp add: expand_fun_eq)
5.105 + then have "fold More_Set.remove xs (member A) =
5.106 + member (fold (\<lambda>x. Fset \<circ> More_Set.remove x \<circ> member) xs A)"
5.107 + by (simp add: expand_fun_eq)
5.108 + then have "inf A (Coset xs) = fold remove xs A"
5.109 + by (simp add: Diff_eq [symmetric] minus_set *)
5.110 + moreover have "\<And>x y :: 'a. Fset.remove y \<circ> Fset.remove x = Fset.remove x \<circ> Fset.remove y"
5.111 + by (auto simp add: More_Set.remove_def * intro: ext)
5.112 + ultimately show "inf A (Coset xs) = foldr remove xs A"
5.113 + by (simp add: foldr_fold)
5.114 qed
5.115
5.116 lemma subtract_remove [code]:
5.117 - "A - Set xs = foldl (\<lambda>A x. remove x A) A xs"
5.118 + "A - Set xs = foldr remove xs A"
5.119 "A - Coset xs = Set (List.filter (member A) xs)"
5.120 -proof -
5.121 - have "foldl (\<lambda>A x. List_Set.remove x A) (member A) xs =
5.122 - member (foldl (\<lambda>A x. Fset (List_Set.remove x (member A))) A xs)"
5.123 - by (rule foldl_apply) (simp add: expand_fun_eq)
5.124 - then show "A - Set xs = foldl (\<lambda>A x. remove x A) A xs"
5.125 - by (simp add: minus_set)
5.126 - show "A - Coset xs = Set (List.filter (member A) xs)"
5.127 - by (auto simp add: Coset_def Set_def)
5.128 -qed
5.129 + by (simp_all only: diff_eq compl_Set compl_Coset inter_project)
5.130
5.131 lemma union_insert [code]:
5.132 - "sup (Set xs) A = foldl (\<lambda>A x. insert x A) A xs"
5.133 + "sup (Set xs) A = foldr insert xs A"
5.134 "sup (Coset xs) A = Coset (List.filter (Not \<circ> member A) xs)"
5.135 proof -
5.136 - have "foldl (\<lambda>A x. Set.insert x A) (member A) xs =
5.137 - member (foldl (\<lambda>A x. Fset (Set.insert x (member A))) A xs)"
5.138 - by (rule foldl_apply) (simp add: expand_fun_eq)
5.139 - then show "sup (Set xs) A = foldl (\<lambda>A x. insert x A) A xs"
5.140 - by (simp add: union_set)
5.141 + have *: "\<And>x::'a. insert = (\<lambda>x. Fset \<circ> Set.insert x \<circ> member)"
5.142 + by (simp add: expand_fun_eq)
5.143 + have "member \<circ> fold (\<lambda>x. Fset \<circ> Set.insert x \<circ> member) xs =
5.144 + fold Set.insert xs \<circ> member"
5.145 + by (rule fold_apply) (simp add: expand_fun_eq)
5.146 + then have "fold Set.insert xs (member A) =
5.147 + member (fold (\<lambda>x. Fset \<circ> Set.insert x \<circ> member) xs A)"
5.148 + by (simp add: expand_fun_eq)
5.149 + then have "sup (Set xs) A = fold insert xs A"
5.150 + by (simp add: union_set *)
5.151 + moreover have "\<And>x y :: 'a. Fset.insert y \<circ> Fset.insert x = Fset.insert x \<circ> Fset.insert y"
5.152 + by (auto simp add: * intro: ext)
5.153 + ultimately show "sup (Set xs) A = foldr insert xs A"
5.154 + by (simp add: foldr_fold)
5.155 show "sup (Coset xs) A = Coset (List.filter (Not \<circ> member A) xs)"
5.156 by (auto simp add: Coset_def)
5.157 qed
5.158 @@ -242,17 +261,17 @@
5.159 [simp]: "Infimum A = Inf (member A)"
5.160
5.161 lemma Infimum_inf [code]:
5.162 - "Infimum (Set As) = foldl inf top As"
5.163 + "Infimum (Set As) = foldr inf As top"
5.164 "Infimum (Coset []) = bot"
5.165 - by (simp_all add: Inf_set_fold Inf_UNIV)
5.166 + by (simp_all add: Inf_set_foldr Inf_UNIV)
5.167
5.168 definition Supremum :: "'a fset \<Rightarrow> 'a" where
5.169 [simp]: "Supremum A = Sup (member A)"
5.170
5.171 lemma Supremum_sup [code]:
5.172 - "Supremum (Set As) = foldl sup bot As"
5.173 + "Supremum (Set As) = foldr sup As bot"
5.174 "Supremum (Coset []) = top"
5.175 - by (simp_all add: Sup_set_fold Sup_UNIV)
5.176 + by (simp_all add: Sup_set_foldr Sup_UNIV)
5.177
5.178 end
5.179
5.180 @@ -277,17 +296,17 @@
5.181
5.182 lemma is_empty_simp [simp]:
5.183 "is_empty A \<longleftrightarrow> member A = {}"
5.184 - by (simp add: List_Set.is_empty_def)
5.185 + by (simp add: More_Set.is_empty_def)
5.186 declare is_empty_def [simp del]
5.187
5.188 lemma remove_simp [simp]:
5.189 "remove x A = Fset (member A - {x})"
5.190 - by (simp add: List_Set.remove_def)
5.191 + by (simp add: More_Set.remove_def)
5.192 declare remove_def [simp del]
5.193
5.194 lemma filter_simp [simp]:
5.195 "filter P A = Fset {x \<in> member A. P x}"
5.196 - by (simp add: List_Set.project_def)
5.197 + by (simp add: More_Set.project_def)
5.198 declare filter_def [simp del]
5.199
5.200 declare mem_def [simp del]
6.1 --- a/src/HOL/Library/Library.thy Thu May 20 16:25:22 2010 +0200
6.2 +++ b/src/HOL/Library/Library.thy Thu May 20 19:55:42 2010 +0200
6.3 @@ -34,6 +34,7 @@
6.4 ListVector
6.5 Kleene_Algebra
6.6 Mapping
6.7 + More_List
6.8 Multiset
6.9 Nat_Infinity
6.10 Nested_Environment
7.1 --- a/src/HOL/Library/List_Set.thy Thu May 20 16:25:22 2010 +0200
7.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
7.3 @@ -1,114 +0,0 @@
7.4 -
7.5 -(* Author: Florian Haftmann, TU Muenchen *)
7.6 -
7.7 -header {* Relating (finite) sets and lists *}
7.8 -
7.9 -theory List_Set
7.10 -imports Main
7.11 -begin
7.12 -
7.13 -subsection {* Various additional set functions *}
7.14 -
7.15 -definition is_empty :: "'a set \<Rightarrow> bool" where
7.16 - "is_empty A \<longleftrightarrow> A = {}"
7.17 -
7.18 -definition remove :: "'a \<Rightarrow> 'a set \<Rightarrow> 'a set" where
7.19 - "remove x A = A - {x}"
7.20 -
7.21 -lemma fun_left_comm_idem_remove:
7.22 - "fun_left_comm_idem remove"
7.23 -proof -
7.24 - have rem: "remove = (\<lambda>x A. A - {x})" by (simp add: expand_fun_eq remove_def)
7.25 - show ?thesis by (simp only: fun_left_comm_idem_remove rem)
7.26 -qed
7.27 -
7.28 -lemma minus_fold_remove:
7.29 - assumes "finite A"
7.30 - shows "B - A = fold remove B A"
7.31 -proof -
7.32 - have rem: "remove = (\<lambda>x A. A - {x})" by (simp add: expand_fun_eq remove_def)
7.33 - show ?thesis by (simp only: rem assms minus_fold_remove)
7.34 -qed
7.35 -
7.36 -definition project :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" where
7.37 - "project P A = {a\<in>A. P a}"
7.38 -
7.39 -
7.40 -subsection {* Basic set operations *}
7.41 -
7.42 -lemma is_empty_set:
7.43 - "is_empty (set xs) \<longleftrightarrow> null xs"
7.44 - by (simp add: is_empty_def null_empty)
7.45 -
7.46 -lemma ball_set:
7.47 - "(\<forall>x\<in>set xs. P x) \<longleftrightarrow> list_all P xs"
7.48 - by (rule list_ball_code)
7.49 -
7.50 -lemma bex_set:
7.51 - "(\<exists>x\<in>set xs. P x) \<longleftrightarrow> list_ex P xs"
7.52 - by (rule list_bex_code)
7.53 -
7.54 -lemma empty_set:
7.55 - "{} = set []"
7.56 - by simp
7.57 -
7.58 -lemma insert_set_compl:
7.59 - "insert x (- set xs) = - set (removeAll x xs)"
7.60 - by auto
7.61 -
7.62 -lemma remove_set_compl:
7.63 - "remove x (- set xs) = - set (List.insert x xs)"
7.64 - by (auto simp del: mem_def simp add: remove_def List.insert_def)
7.65 -
7.66 -lemma image_set:
7.67 - "image f (set xs) = set (map f xs)"
7.68 - by simp
7.69 -
7.70 -lemma project_set:
7.71 - "project P (set xs) = set (filter P xs)"
7.72 - by (auto simp add: project_def)
7.73 -
7.74 -
7.75 -subsection {* Functorial set operations *}
7.76 -
7.77 -lemma union_set:
7.78 - "set xs \<union> A = foldl (\<lambda>A x. Set.insert x A) A xs"
7.79 -proof -
7.80 - interpret fun_left_comm_idem Set.insert
7.81 - by (fact fun_left_comm_idem_insert)
7.82 - show ?thesis by (simp add: union_fold_insert fold_set)
7.83 -qed
7.84 -
7.85 -lemma minus_set:
7.86 - "A - set xs = foldl (\<lambda>A x. remove x A) A xs"
7.87 -proof -
7.88 - interpret fun_left_comm_idem remove
7.89 - by (fact fun_left_comm_idem_remove)
7.90 - show ?thesis
7.91 - by (simp add: minus_fold_remove [of _ A] fold_set)
7.92 -qed
7.93 -
7.94 -
7.95 -subsection {* Derived set operations *}
7.96 -
7.97 -lemma member:
7.98 - "a \<in> A \<longleftrightarrow> (\<exists>x\<in>A. a = x)"
7.99 - by simp
7.100 -
7.101 -lemma subset_eq:
7.102 - "A \<subseteq> B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
7.103 - by (fact subset_eq)
7.104 -
7.105 -lemma subset:
7.106 - "A \<subset> B \<longleftrightarrow> A \<subseteq> B \<and> \<not> B \<subseteq> A"
7.107 - by (fact less_le_not_le)
7.108 -
7.109 -lemma set_eq:
7.110 - "A = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
7.111 - by (fact eq_iff)
7.112 -
7.113 -lemma inter:
7.114 - "A \<inter> B = project (\<lambda>x. x \<in> A) B"
7.115 - by (auto simp add: project_def)
7.116 -
7.117 -end
7.118 \ No newline at end of file
8.1 --- a/src/HOL/Library/Mapping.thy Thu May 20 16:25:22 2010 +0200
8.2 +++ b/src/HOL/Library/Mapping.thy Thu May 20 19:55:42 2010 +0200
8.3 @@ -40,6 +40,16 @@
8.4 definition replace :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" where
8.5 "replace k v m = (if lookup m k = None then m else update k v m)"
8.6
8.7 +definition default :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" where
8.8 + "default k v m = (if lookup m k = None then update k v m else m)"
8.9 +
8.10 +definition map_entry :: "'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" where
8.11 + "map_entry k f m = (case lookup m k of None \<Rightarrow> m
8.12 + | Some v \<Rightarrow> update k (f v) m)"
8.13 +
8.14 +definition map_default :: "'a \<Rightarrow> 'b \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" where
8.15 + "map_default k v f m = map_entry k f (default k v m)"
8.16 +
8.17 definition tabulate :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) mapping" where
8.18 "tabulate ks f = Mapping (map_of (map (\<lambda>k. (k, f k)) ks))"
8.19
8.20 @@ -70,6 +80,10 @@
8.21 "lookup (delete k m) = (lookup m) (k := None)"
8.22 by (cases m) simp
8.23
8.24 +lemma lookup_map_entry [simp]:
8.25 + "lookup (map_entry k f m) = (lookup m) (k := Option.map f (lookup m k))"
8.26 + by (cases "lookup m k") (simp_all add: map_entry_def expand_fun_eq)
8.27 +
8.28 lemma lookup_tabulate [simp]:
8.29 "lookup (tabulate ks f) = (Some o f) |` set ks"
8.30 by (induct ks) (auto simp add: tabulate_def restrict_map_def expand_fun_eq)
8.31 @@ -122,6 +136,14 @@
8.32 "bulkload xs = tabulate [0..<length xs] (nth xs)"
8.33 by (rule mapping_eqI) (simp add: expand_fun_eq)
8.34
8.35 +lemma keys_tabulate:
8.36 + "keys (tabulate ks f) = set ks"
8.37 + by (simp add: tabulate_def keys_def map_of_map_restrict o_def)
8.38 +
8.39 +lemma keys_bulkload:
8.40 + "keys (bulkload xs) = {0..<length xs}"
8.41 + by (simp add: keys_tabulate bulkload_tabulate)
8.42 +
8.43 lemma is_empty_empty:
8.44 "is_empty m \<longleftrightarrow> m = Mapping Map.empty"
8.45 by (cases m) (simp add: is_empty_def)
9.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
9.2 +++ b/src/HOL/Library/More_List.thy Thu May 20 19:55:42 2010 +0200
9.3 @@ -0,0 +1,267 @@
9.4 +(* Author: Florian Haftmann, TU Muenchen *)
9.5 +
9.6 +header {* Operations on lists beyond the standard List theory *}
9.7 +
9.8 +theory More_List
9.9 +imports Main
9.10 +begin
9.11 +
9.12 +hide_const (open) Finite_Set.fold
9.13 +
9.14 +text {* Repairing code generator setup *}
9.15 +
9.16 +declare (in lattice) Inf_fin_set_fold [code_unfold del]
9.17 +declare (in lattice) Sup_fin_set_fold [code_unfold del]
9.18 +declare (in linorder) Min_fin_set_fold [code_unfold del]
9.19 +declare (in linorder) Max_fin_set_fold [code_unfold del]
9.20 +declare (in complete_lattice) Inf_set_fold [code_unfold del]
9.21 +declare (in complete_lattice) Sup_set_fold [code_unfold del]
9.22 +declare rev_foldl_cons [code del]
9.23 +
9.24 +text {* Fold combinator with canonical argument order *}
9.25 +
9.26 +primrec fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where
9.27 + "fold f [] = id"
9.28 + | "fold f (x # xs) = fold f xs \<circ> f x"
9.29 +
9.30 +lemma foldl_fold:
9.31 + "foldl f s xs = fold (\<lambda>x s. f s x) xs s"
9.32 + by (induct xs arbitrary: s) simp_all
9.33 +
9.34 +lemma foldr_fold_rev:
9.35 + "foldr f xs = fold f (rev xs)"
9.36 + by (simp add: foldr_foldl foldl_fold expand_fun_eq)
9.37 +
9.38 +lemma fold_rev_conv [code_unfold]:
9.39 + "fold f (rev xs) = foldr f xs"
9.40 + by (simp add: foldr_fold_rev)
9.41 +
9.42 +lemma fold_cong [fundef_cong, recdef_cong]:
9.43 + "a = b \<Longrightarrow> xs = ys \<Longrightarrow> (\<And>x. x \<in> set xs \<Longrightarrow> f x = g x)
9.44 + \<Longrightarrow> fold f xs a = fold g ys b"
9.45 + by (induct ys arbitrary: a b xs) simp_all
9.46 +
9.47 +lemma fold_id:
9.48 + assumes "\<And>x. x \<in> set xs \<Longrightarrow> f x = id"
9.49 + shows "fold f xs = id"
9.50 + using assms by (induct xs) simp_all
9.51 +
9.52 +lemma fold_apply:
9.53 + assumes "\<And>x. x \<in> set xs \<Longrightarrow> h \<circ> g x = f x \<circ> h"
9.54 + shows "h \<circ> fold g xs = fold f xs \<circ> h"
9.55 + using assms by (induct xs) (simp_all add: expand_fun_eq)
9.56 +
9.57 +lemma fold_invariant:
9.58 + assumes "\<And>x. x \<in> set xs \<Longrightarrow> Q x" and "P s"
9.59 + and "\<And>x s. Q x \<Longrightarrow> P s \<Longrightarrow> P (f x s)"
9.60 + shows "P (fold f xs s)"
9.61 + using assms by (induct xs arbitrary: s) simp_all
9.62 +
9.63 +lemma fold_weak_invariant:
9.64 + assumes "P s"
9.65 + and "\<And>s x. x \<in> set xs \<Longrightarrow> P s \<Longrightarrow> P (f x s)"
9.66 + shows "P (fold f xs s)"
9.67 + using assms by (induct xs arbitrary: s) simp_all
9.68 +
9.69 +lemma fold_append [simp]:
9.70 + "fold f (xs @ ys) = fold f ys \<circ> fold f xs"
9.71 + by (induct xs) simp_all
9.72 +
9.73 +lemma fold_map [code_unfold]:
9.74 + "fold g (map f xs) = fold (g o f) xs"
9.75 + by (induct xs) simp_all
9.76 +
9.77 +lemma fold_rev:
9.78 + assumes "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f y \<circ> f x = f x \<circ> f y"
9.79 + shows "fold f (rev xs) = fold f xs"
9.80 + using assms by (induct xs) (simp_all del: o_apply add: fold_apply)
9.81 +
9.82 +lemma foldr_fold:
9.83 + assumes "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f y \<circ> f x = f x \<circ> f y"
9.84 + shows "foldr f xs = fold f xs"
9.85 + using assms unfolding foldr_fold_rev by (rule fold_rev)
9.86 +
9.87 +lemma fold_Cons_rev:
9.88 + "fold Cons xs = append (rev xs)"
9.89 + by (induct xs) simp_all
9.90 +
9.91 +lemma rev_conv_fold [code]:
9.92 + "rev xs = fold Cons xs []"
9.93 + by (simp add: fold_Cons_rev)
9.94 +
9.95 +lemma fold_append_concat_rev:
9.96 + "fold append xss = append (concat (rev xss))"
9.97 + by (induct xss) simp_all
9.98 +
9.99 +lemma concat_conv_foldr [code]:
9.100 + "concat xss = foldr append xss []"
9.101 + by (simp add: fold_append_concat_rev foldr_fold_rev)
9.102 +
9.103 +lemma fold_plus_listsum_rev:
9.104 + "fold plus xs = plus (listsum (rev xs))"
9.105 + by (induct xs) (simp_all add: add.assoc)
9.106 +
9.107 +lemma listsum_conv_foldr [code]:
9.108 + "listsum xs = foldr plus xs 0"
9.109 + by (fact listsum_foldr)
9.110 +
9.111 +lemma sort_key_conv_fold:
9.112 + assumes "inj_on f (set xs)"
9.113 + shows "sort_key f xs = fold (insort_key f) xs []"
9.114 +proof -
9.115 + have "fold (insort_key f) (rev xs) = fold (insort_key f) xs"
9.116 + proof (rule fold_rev, rule ext)
9.117 + fix zs
9.118 + fix x y
9.119 + assume "x \<in> set xs" "y \<in> set xs"
9.120 + with assms have *: "f y = f x \<Longrightarrow> y = x" by (auto dest: inj_onD)
9.121 + show "(insort_key f y \<circ> insort_key f x) zs = (insort_key f x \<circ> insort_key f y) zs"
9.122 + by (induct zs) (auto dest: *)
9.123 + qed
9.124 + then show ?thesis by (simp add: sort_key_def foldr_fold_rev)
9.125 +qed
9.126 +
9.127 +lemma sort_conv_fold:
9.128 + "sort xs = fold insort xs []"
9.129 + by (rule sort_key_conv_fold) simp
9.130 +
9.131 +text {* @{const Finite_Set.fold} and @{const fold} *}
9.132 +
9.133 +lemma (in fun_left_comm) fold_set_remdups:
9.134 + "Finite_Set.fold f y (set xs) = fold f (remdups xs) y"
9.135 + by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm insert_absorb)
9.136 +
9.137 +lemma (in fun_left_comm_idem) fold_set:
9.138 + "Finite_Set.fold f y (set xs) = fold f xs y"
9.139 + by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm)
9.140 +
9.141 +lemma (in ab_semigroup_idem_mult) fold1_set:
9.142 + assumes "xs \<noteq> []"
9.143 + shows "Finite_Set.fold1 times (set xs) = fold times (tl xs) (hd xs)"
9.144 +proof -
9.145 + interpret fun_left_comm_idem times by (fact fun_left_comm_idem)
9.146 + from assms obtain y ys where xs: "xs = y # ys"
9.147 + by (cases xs) auto
9.148 + show ?thesis
9.149 + proof (cases "set ys = {}")
9.150 + case True with xs show ?thesis by simp
9.151 + next
9.152 + case False
9.153 + then have "fold1 times (insert y (set ys)) = Finite_Set.fold times y (set ys)"
9.154 + by (simp only: finite_set fold1_eq_fold_idem)
9.155 + with xs show ?thesis by (simp add: fold_set mult_commute)
9.156 + qed
9.157 +qed
9.158 +
9.159 +lemma (in lattice) Inf_fin_set_fold:
9.160 + "Inf_fin (set (x # xs)) = fold inf xs x"
9.161 +proof -
9.162 + interpret ab_semigroup_idem_mult "inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
9.163 + by (fact ab_semigroup_idem_mult_inf)
9.164 + show ?thesis
9.165 + by (simp add: Inf_fin_def fold1_set del: set.simps)
9.166 +qed
9.167 +
9.168 +lemma (in lattice) Inf_fin_set_foldr [code_unfold]:
9.169 + "Inf_fin (set (x # xs)) = foldr inf xs x"
9.170 + by (simp add: Inf_fin_set_fold ac_simps foldr_fold expand_fun_eq del: set.simps)
9.171 +
9.172 +lemma (in lattice) Sup_fin_set_fold:
9.173 + "Sup_fin (set (x # xs)) = fold sup xs x"
9.174 +proof -
9.175 + interpret ab_semigroup_idem_mult "sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
9.176 + by (fact ab_semigroup_idem_mult_sup)
9.177 + show ?thesis
9.178 + by (simp add: Sup_fin_def fold1_set del: set.simps)
9.179 +qed
9.180 +
9.181 +lemma (in lattice) Sup_fin_set_foldr [code_unfold]:
9.182 + "Sup_fin (set (x # xs)) = foldr sup xs x"
9.183 + by (simp add: Sup_fin_set_fold ac_simps foldr_fold expand_fun_eq del: set.simps)
9.184 +
9.185 +lemma (in linorder) Min_fin_set_fold:
9.186 + "Min (set (x # xs)) = fold min xs x"
9.187 +proof -
9.188 + interpret ab_semigroup_idem_mult "min :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
9.189 + by (fact ab_semigroup_idem_mult_min)
9.190 + show ?thesis
9.191 + by (simp add: Min_def fold1_set del: set.simps)
9.192 +qed
9.193 +
9.194 +lemma (in linorder) Min_fin_set_foldr [code_unfold]:
9.195 + "Min (set (x # xs)) = foldr min xs x"
9.196 + by (simp add: Min_fin_set_fold ac_simps foldr_fold expand_fun_eq del: set.simps)
9.197 +
9.198 +lemma (in linorder) Max_fin_set_fold:
9.199 + "Max (set (x # xs)) = fold max xs x"
9.200 +proof -
9.201 + interpret ab_semigroup_idem_mult "max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
9.202 + by (fact ab_semigroup_idem_mult_max)
9.203 + show ?thesis
9.204 + by (simp add: Max_def fold1_set del: set.simps)
9.205 +qed
9.206 +
9.207 +lemma (in linorder) Max_fin_set_foldr [code_unfold]:
9.208 + "Max (set (x # xs)) = foldr max xs x"
9.209 + by (simp add: Max_fin_set_fold ac_simps foldr_fold expand_fun_eq del: set.simps)
9.210 +
9.211 +lemma (in complete_lattice) Inf_set_fold:
9.212 + "Inf (set xs) = fold inf xs top"
9.213 +proof -
9.214 + interpret fun_left_comm_idem "inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
9.215 + by (fact fun_left_comm_idem_inf)
9.216 + show ?thesis by (simp add: Inf_fold_inf fold_set inf_commute)
9.217 +qed
9.218 +
9.219 +lemma (in complete_lattice) Inf_set_foldr [code_unfold]:
9.220 + "Inf (set xs) = foldr inf xs top"
9.221 + by (simp add: Inf_set_fold ac_simps foldr_fold expand_fun_eq)
9.222 +
9.223 +lemma (in complete_lattice) Sup_set_fold:
9.224 + "Sup (set xs) = fold sup xs bot"
9.225 +proof -
9.226 + interpret fun_left_comm_idem "sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
9.227 + by (fact fun_left_comm_idem_sup)
9.228 + show ?thesis by (simp add: Sup_fold_sup fold_set sup_commute)
9.229 +qed
9.230 +
9.231 +lemma (in complete_lattice) Sup_set_foldr [code_unfold]:
9.232 + "Sup (set xs) = foldr sup xs bot"
9.233 + by (simp add: Sup_set_fold ac_simps foldr_fold expand_fun_eq)
9.234 +
9.235 +lemma (in complete_lattice) INFI_set_fold:
9.236 + "INFI (set xs) f = fold (inf \<circ> f) xs top"
9.237 + unfolding INFI_def set_map [symmetric] Inf_set_fold fold_map ..
9.238 +
9.239 +lemma (in complete_lattice) SUPR_set_fold:
9.240 + "SUPR (set xs) f = fold (sup \<circ> f) xs bot"
9.241 + unfolding SUPR_def set_map [symmetric] Sup_set_fold fold_map ..
9.242 +
9.243 +text {* @{text nth_map} *}
9.244 +
9.245 +definition nth_map :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
9.246 + "nth_map n f xs = (if n < length xs then
9.247 + take n xs @ [f (xs ! n)] @ drop (Suc n) xs
9.248 + else xs)"
9.249 +
9.250 +lemma nth_map_id:
9.251 + "n \<ge> length xs \<Longrightarrow> nth_map n f xs = xs"
9.252 + by (simp add: nth_map_def)
9.253 +
9.254 +lemma nth_map_unfold:
9.255 + "n < length xs \<Longrightarrow> nth_map n f xs = take n xs @ [f (xs ! n)] @ drop (Suc n) xs"
9.256 + by (simp add: nth_map_def)
9.257 +
9.258 +lemma nth_map_Nil [simp]:
9.259 + "nth_map n f [] = []"
9.260 + by (simp add: nth_map_def)
9.261 +
9.262 +lemma nth_map_zero [simp]:
9.263 + "nth_map 0 f (x # xs) = f x # xs"
9.264 + by (simp add: nth_map_def)
9.265 +
9.266 +lemma nth_map_Suc [simp]:
9.267 + "nth_map (Suc n) f (x # xs) = x # nth_map n f xs"
9.268 + by (simp add: nth_map_def)
9.269 +
9.270 +end
10.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
10.2 +++ b/src/HOL/Library/More_Set.thy Thu May 20 19:55:42 2010 +0200
10.3 @@ -0,0 +1,137 @@
10.4 +
10.5 +(* Author: Florian Haftmann, TU Muenchen *)
10.6 +
10.7 +header {* Relating (finite) sets and lists *}
10.8 +
10.9 +theory More_Set
10.10 +imports Main More_List
10.11 +begin
10.12 +
10.13 +subsection {* Various additional set functions *}
10.14 +
10.15 +definition is_empty :: "'a set \<Rightarrow> bool" where
10.16 + "is_empty A \<longleftrightarrow> A = {}"
10.17 +
10.18 +definition remove :: "'a \<Rightarrow> 'a set \<Rightarrow> 'a set" where
10.19 + "remove x A = A - {x}"
10.20 +
10.21 +lemma fun_left_comm_idem_remove:
10.22 + "fun_left_comm_idem remove"
10.23 +proof -
10.24 + have rem: "remove = (\<lambda>x A. A - {x})" by (simp add: expand_fun_eq remove_def)
10.25 + show ?thesis by (simp only: fun_left_comm_idem_remove rem)
10.26 +qed
10.27 +
10.28 +lemma minus_fold_remove:
10.29 + assumes "finite A"
10.30 + shows "B - A = Finite_Set.fold remove B A"
10.31 +proof -
10.32 + have rem: "remove = (\<lambda>x A. A - {x})" by (simp add: expand_fun_eq remove_def)
10.33 + show ?thesis by (simp only: rem assms minus_fold_remove)
10.34 +qed
10.35 +
10.36 +definition project :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" where
10.37 + "project P A = {a\<in>A. P a}"
10.38 +
10.39 +
10.40 +subsection {* Basic set operations *}
10.41 +
10.42 +lemma is_empty_set:
10.43 + "is_empty (set xs) \<longleftrightarrow> null xs"
10.44 + by (simp add: is_empty_def null_empty)
10.45 +
10.46 +lemma ball_set:
10.47 + "(\<forall>x\<in>set xs. P x) \<longleftrightarrow> list_all P xs"
10.48 + by (rule list_ball_code)
10.49 +
10.50 +lemma bex_set:
10.51 + "(\<exists>x\<in>set xs. P x) \<longleftrightarrow> list_ex P xs"
10.52 + by (rule list_bex_code)
10.53 +
10.54 +lemma empty_set:
10.55 + "{} = set []"
10.56 + by simp
10.57 +
10.58 +lemma insert_set_compl:
10.59 + "insert x (- set xs) = - set (removeAll x xs)"
10.60 + by auto
10.61 +
10.62 +lemma remove_set_compl:
10.63 + "remove x (- set xs) = - set (List.insert x xs)"
10.64 + by (auto simp del: mem_def simp add: remove_def List.insert_def)
10.65 +
10.66 +lemma image_set:
10.67 + "image f (set xs) = set (map f xs)"
10.68 + by simp
10.69 +
10.70 +lemma project_set:
10.71 + "project P (set xs) = set (filter P xs)"
10.72 + by (auto simp add: project_def)
10.73 +
10.74 +
10.75 +subsection {* Functorial set operations *}
10.76 +
10.77 +lemma union_set:
10.78 + "set xs \<union> A = fold Set.insert xs A"
10.79 +proof -
10.80 + interpret fun_left_comm_idem Set.insert
10.81 + by (fact fun_left_comm_idem_insert)
10.82 + show ?thesis by (simp add: union_fold_insert fold_set)
10.83 +qed
10.84 +
10.85 +lemma union_set_foldr:
10.86 + "set xs \<union> A = foldr Set.insert xs A"
10.87 +proof -
10.88 + have "\<And>x y :: 'a. insert y \<circ> insert x = insert x \<circ> insert y"
10.89 + by (auto intro: ext)
10.90 + then show ?thesis by (simp add: union_set foldr_fold)
10.91 +qed
10.92 +
10.93 +lemma minus_set:
10.94 + "A - set xs = fold remove xs A"
10.95 +proof -
10.96 + interpret fun_left_comm_idem remove
10.97 + by (fact fun_left_comm_idem_remove)
10.98 + show ?thesis
10.99 + by (simp add: minus_fold_remove [of _ A] fold_set)
10.100 +qed
10.101 +
10.102 +lemma minus_set_foldr:
10.103 + "A - set xs = foldr remove xs A"
10.104 +proof -
10.105 + have "\<And>x y :: 'a. remove y \<circ> remove x = remove x \<circ> remove y"
10.106 + by (auto simp add: remove_def intro: ext)
10.107 + then show ?thesis by (simp add: minus_set foldr_fold)
10.108 +qed
10.109 +
10.110 +
10.111 +subsection {* Derived set operations *}
10.112 +
10.113 +lemma member:
10.114 + "a \<in> A \<longleftrightarrow> (\<exists>x\<in>A. a = x)"
10.115 + by simp
10.116 +
10.117 +lemma subset_eq:
10.118 + "A \<subseteq> B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
10.119 + by (fact subset_eq)
10.120 +
10.121 +lemma subset:
10.122 + "A \<subset> B \<longleftrightarrow> A \<subseteq> B \<and> \<not> B \<subseteq> A"
10.123 + by (fact less_le_not_le)
10.124 +
10.125 +lemma set_eq:
10.126 + "A = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
10.127 + by (fact eq_iff)
10.128 +
10.129 +lemma inter:
10.130 + "A \<inter> B = project (\<lambda>x. x \<in> A) B"
10.131 + by (auto simp add: project_def)
10.132 +
10.133 +
10.134 +subsection {* Various lemmas *}
10.135 +
10.136 +lemma not_set_compl:
10.137 + "Not \<circ> set xs = - set xs"
10.138 + by (simp add: fun_Compl_def bool_Compl_def comp_def expand_fun_eq)
10.139 +
10.140 +end
11.1 --- a/src/HOL/Library/RBT.thy Thu May 20 16:25:22 2010 +0200
11.2 +++ b/src/HOL/Library/RBT.thy Thu May 20 19:55:42 2010 +0200
11.3 @@ -136,7 +136,7 @@
11.4
11.5 lemma lookup_map_entry [simp]:
11.6 "lookup (map_entry k f t) = (lookup t)(k := Option.map f (lookup t k))"
11.7 - by (simp add: map_entry_def lookup_RBT lookup_map_entry lookup_impl_of)
11.8 + by (simp add: map_entry_def lookup_RBT RBT_Impl.lookup_map_entry lookup_impl_of)
11.9
11.10 lemma lookup_map [simp]:
11.11 "lookup (map f t) k = Option.map (f k) (lookup t k)"
11.12 @@ -191,7 +191,11 @@
11.13 by (rule mapping_eqI) simp
11.14
11.15 lemma delete_Mapping [code]:
11.16 - "Mapping.delete k (Mapping xs) = Mapping (delete k xs)"
11.17 + "Mapping.delete k (Mapping t) = Mapping (delete k t)"
11.18 + by (rule mapping_eqI) simp
11.19 +
11.20 +lemma map_entry_Mapping [code]:
11.21 + "Mapping.map_entry k f (Mapping t) = Mapping (map_entry k f t)"
11.22 by (rule mapping_eqI) simp
11.23
11.24 lemma keys_Mapping [code]:
12.1 --- a/src/HOL/List.thy Thu May 20 16:25:22 2010 +0200
12.2 +++ b/src/HOL/List.thy Thu May 20 19:55:42 2010 +0200
12.3 @@ -4491,11 +4491,8 @@
12.4
12.5 subsubsection {* Generation of efficient code *}
12.6
12.7 -primrec
12.8 - member :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" (infixl "mem" 55)
12.9 -where
12.10 - "x mem [] \<longleftrightarrow> False"
12.11 - | "x mem (y#ys) \<longleftrightarrow> x = y \<or> x mem ys"
12.12 +definition member :: "'a list \<Rightarrow> 'a \<Rightarrow> bool" where
12.13 + mem_iff [code_post]: "member xs x \<longleftrightarrow> x \<in> set xs"
12.14
12.15 primrec
12.16 null:: "'a list \<Rightarrow> bool"
12.17 @@ -4551,7 +4548,7 @@
12.18 | "concat_map f (x#xs) = f x @ concat_map f xs"
12.19
12.20 text {*
12.21 - Only use @{text mem} for generating executable code. Otherwise use
12.22 + Only use @{text member} for generating executable code. Otherwise use
12.23 @{prop "x : set xs"} instead --- it is much easier to reason about.
12.24 The same is true for @{const list_all} and @{const list_ex}: write
12.25 @{text "\<forall>x\<in>set xs"} and @{text "\<exists>x\<in>set xs"} instead because the HOL
12.26 @@ -4583,12 +4580,20 @@
12.27 show ?case by (induct xs) (auto simp add: Cons aux)
12.28 qed
12.29
12.30 -lemma mem_iff [code_post]:
12.31 - "x mem xs \<longleftrightarrow> x \<in> set xs"
12.32 -by (induct xs) auto
12.33 -
12.34 lemmas in_set_code [code_unfold] = mem_iff [symmetric]
12.35
12.36 +lemma member_simps [simp, code]:
12.37 + "member [] y \<longleftrightarrow> False"
12.38 + "member (x # xs) y \<longleftrightarrow> x = y \<or> member xs y"
12.39 + by (auto simp add: mem_iff)
12.40 +
12.41 +lemma member_set:
12.42 + "member = set"
12.43 + by (simp add: expand_fun_eq mem_iff mem_def)
12.44 +
12.45 +abbreviation (input) mem :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" (infixl "mem" 55) where
12.46 + "x mem xs \<equiv> member xs x" -- "for backward compatibility"
12.47 +
12.48 lemma empty_null:
12.49 "xs = [] \<longleftrightarrow> null xs"
12.50 by (cases xs) simp_all
13.1 --- a/src/HOL/MicroJava/BV/BVExample.thy Thu May 20 16:25:22 2010 +0200
13.2 +++ b/src/HOL/MicroJava/BV/BVExample.thy Thu May 20 19:55:42 2010 +0200
13.3 @@ -449,7 +449,7 @@
13.4 (\<lambda>(ss, w).
13.5 let p = some_elem w in propa f (step p (ss ! p)) ss (w - {p}))
13.6 (ss, w)"
13.7 - unfolding iter_def List_Set.is_empty_def some_elem_def ..
13.8 + unfolding iter_def More_Set.is_empty_def some_elem_def ..
13.9
13.10 lemma JVM_sup_unfold [code]:
13.11 "JVMType.sup S m n = lift2 (Opt.sup
14.1 --- a/src/HOL/ex/Codegenerator_Candidates.thy Thu May 20 16:25:22 2010 +0200
14.2 +++ b/src/HOL/ex/Codegenerator_Candidates.thy Thu May 20 19:55:42 2010 +0200
14.3 @@ -13,6 +13,7 @@
14.4 Fset
14.5 Enum
14.6 List_Prefix
14.7 + More_List
14.8 Nat_Infinity
14.9 Nested_Environment
14.10 Option_ord