# HG changeset patch # User haftmann # Date 1274378142 -7200 # Node ID e29a115ba58ce92b214de7f622d6fa9d73676165 # Parent f692d6178e4e3830ab0b759f45c3b39b0f52336c# Parent d754fb55a20fc2271c585910b9c176561b429b14 merged diff -r f692d6178e4e -r e29a115ba58c NEWS --- 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. diff -r f692d6178e4e -r e29a115ba58c src/HOL/IsaMakefile --- 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 \ diff -r f692d6178e4e -r e29a115ba58c src/HOL/Library/Dlist.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 \ 'a \ bool" where - "member [] y \ False" - | "member (x#xs) y \ x = y \ member xs y" - -lemma member_set: - "member = set" -proof (rule ext)+ - fix xs :: "'a list" and x :: 'a - have "member xs x \ x \ 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 \ set xs = - set xs" - by (simp add: fun_Compl_def bool_Compl_def comp_def expand_fun_eq) - -primrec fold :: "('a \ 'b \ 'b) \ 'a list \ 'b \ '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 (\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 \ 'b \ 'b) \ 'a dlist \ 'b \ '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 \ 'b \ 'b) \ 'a dlist \ 'b \ '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 \ 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 (\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 \ 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 diff -r f692d6178e4e -r e29a115ba58c src/HOL/Library/Executable_Set.thy --- 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 \ Set xs \ member x xs" - "x \ Coset xs \ \ member x xs" + "x \ Set xs \ member xs x" + "x \ Coset xs \ \ member xs x" by (simp_all add: mem_iff) definition is_empty :: "'a set \ bool" where @@ -76,9 +76,9 @@ Code.add_signature_cmd ("is_empty", "'a set \ bool") #> Code.add_signature_cmd ("empty", "'a set") #> Code.add_signature_cmd ("insert", "'a \ 'a set \ 'a set") - #> Code.add_signature_cmd ("List_Set.remove", "'a \ 'a set \ 'a set") + #> Code.add_signature_cmd ("More_Set.remove", "'a \ 'a set \ 'a set") #> Code.add_signature_cmd ("image", "('a \ 'b) \ 'a set \ 'b set") - #> Code.add_signature_cmd ("List_Set.project", "('a \ bool) \ 'a set \ 'a set") + #> Code.add_signature_cmd ("More_Set.project", "('a \ bool) \ 'a set \ 'a set") #> Code.add_signature_cmd ("Ball", "'a set \ ('a \ bool) \ bool") #> Code.add_signature_cmd ("Bex", "'a set \ ('a \ bool) \ bool") #> Code.add_signature_cmd ("card", "'a set \ nat") @@ -232,36 +232,36 @@ lemma inter_project [code]: "inter A (Set xs) = Set (List.filter (\x. x \ A) xs)" - "inter A (Coset xs) = foldl (\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 (\A x. remove x A) A xs" + "subtract (Set xs) A = foldr remove xs A" "subtract (Coset xs) A = Set (List.filter (\x. x \ A) xs)" - by (auto simp add: minus_set) + by (auto simp add: minus_set_foldr) lemma union_insert [code]: - "union (Set xs) A = foldl (\A x. insert x A) A xs" + "union (Set xs) A = foldr insert xs A" "union (Coset xs) A = Coset (List.filter (\x. x \ 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 diff -r f692d6178e4e -r e29a115ba58c src/HOL/Library/Fset.thy --- 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 \ List.member y xs" - "member (Coset xs) y \ \ 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 \ 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 \ bool" where - [simp]: "is_empty A \ List_Set.is_empty (member A)" + [simp]: "is_empty A \ More_Set.is_empty (member A)" lemma is_empty_Set [code]: "is_empty (Set xs) \ 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 \ 'a fset \ '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 \ 'b) \ 'a fset \ 'b fset" where [simp]: "map f A = Fset (image f (member A))" @@ -147,7 +148,7 @@ by (simp add: Set_def) definition filter :: "('a \ bool) \ 'a fset \ '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 (\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 (\A x. List_Set.remove x A) (member A) xs = - member (foldl (\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 (\A x. remove x A) A xs" - by (simp add: Diff_eq [symmetric] minus_set) + have *: "\x::'a. remove = (\x. Fset \ More_Set.remove x \ member)" + by (simp add: expand_fun_eq) + have "member \ fold (\x. Fset \ More_Set.remove x \ member) xs = + fold More_Set.remove xs \ member" + by (rule fold_apply) (simp add: expand_fun_eq) + then have "fold More_Set.remove xs (member A) = + member (fold (\x. Fset \ More_Set.remove x \ 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 "\x y :: 'a. Fset.remove y \ Fset.remove x = Fset.remove x \ 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 (\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 (\A x. List_Set.remove x A) (member A) xs = - member (foldl (\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 (\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 (\A x. insert x A) A xs" + "sup (Set xs) A = foldr insert xs A" "sup (Coset xs) A = Coset (List.filter (Not \ member A) xs)" proof - - have "foldl (\A x. Set.insert x A) (member A) xs = - member (foldl (\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 (\A x. insert x A) A xs" - by (simp add: union_set) + have *: "\x::'a. insert = (\x. Fset \ Set.insert x \ member)" + by (simp add: expand_fun_eq) + have "member \ fold (\x. Fset \ Set.insert x \ member) xs = + fold Set.insert xs \ member" + by (rule fold_apply) (simp add: expand_fun_eq) + then have "fold Set.insert xs (member A) = + member (fold (\x. Fset \ Set.insert x \ 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 "\x y :: 'a. Fset.insert y \ Fset.insert x = Fset.insert x \ 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 \ 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 \ '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 \ 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 \ member A. P x}" - by (simp add: List_Set.project_def) + by (simp add: More_Set.project_def) declare filter_def [simp del] declare mem_def [simp del] diff -r f692d6178e4e -r e29a115ba58c src/HOL/Library/Library.thy --- 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 diff -r f692d6178e4e -r e29a115ba58c src/HOL/Library/List_Set.thy --- 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 \ bool" where - "is_empty A \ A = {}" - -definition remove :: "'a \ 'a set \ 'a set" where - "remove x A = A - {x}" - -lemma fun_left_comm_idem_remove: - "fun_left_comm_idem remove" -proof - - have rem: "remove = (\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 = (\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 \ bool) \ 'a set \ 'a set" where - "project P A = {a\A. P a}" - - -subsection {* Basic set operations *} - -lemma is_empty_set: - "is_empty (set xs) \ null xs" - by (simp add: is_empty_def null_empty) - -lemma ball_set: - "(\x\set xs. P x) \ list_all P xs" - by (rule list_ball_code) - -lemma bex_set: - "(\x\set xs. P x) \ 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 \ A = foldl (\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 (\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 \ A \ (\x\A. a = x)" - by simp - -lemma subset_eq: - "A \ B \ (\x\A. x \ B)" - by (fact subset_eq) - -lemma subset: - "A \ B \ A \ B \ \ B \ A" - by (fact less_le_not_le) - -lemma set_eq: - "A = B \ A \ B \ B \ A" - by (fact eq_iff) - -lemma inter: - "A \ B = project (\x. x \ A) B" - by (auto simp add: project_def) - -end \ No newline at end of file diff -r f692d6178e4e -r e29a115ba58c src/HOL/Library/Mapping.thy --- 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 \ 'b \ ('a, 'b) mapping \ ('a, 'b) mapping" where "replace k v m = (if lookup m k = None then m else update k v m)" +definition default :: "'a \ 'b \ ('a, 'b) mapping \ ('a, 'b) mapping" where + "default k v m = (if lookup m k = None then update k v m else m)" + +definition map_entry :: "'a \ ('b \ 'b) \ ('a, 'b) mapping \ ('a, 'b) mapping" where + "map_entry k f m = (case lookup m k of None \ m + | Some v \ update k (f v) m)" + +definition map_default :: "'a \ 'b \ ('b \ 'b) \ ('a, 'b) mapping \ ('a, 'b) mapping" where + "map_default k v f m = map_entry k f (default k v m)" + definition tabulate :: "'a list \ ('a \ 'b) \ ('a, 'b) mapping" where "tabulate ks f = Mapping (map_of (map (\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.. m = Mapping Map.empty" by (cases m) (simp add: is_empty_def) diff -r f692d6178e4e -r e29a115ba58c src/HOL/Library/More_List.thy --- /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 \ 'b \ 'b) \ 'a list \ 'b \ 'b" where + "fold f [] = id" + | "fold f (x # xs) = fold f xs \ f x" + +lemma foldl_fold: + "foldl f s xs = fold (\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 \ xs = ys \ (\x. x \ set xs \ f x = g x) + \ fold f xs a = fold g ys b" + by (induct ys arbitrary: a b xs) simp_all + +lemma fold_id: + assumes "\x. x \ set xs \ f x = id" + shows "fold f xs = id" + using assms by (induct xs) simp_all + +lemma fold_apply: + assumes "\x. x \ set xs \ h \ g x = f x \ h" + shows "h \ fold g xs = fold f xs \ h" + using assms by (induct xs) (simp_all add: expand_fun_eq) + +lemma fold_invariant: + assumes "\x. x \ set xs \ Q x" and "P s" + and "\x s. Q x \ P s \ 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 "\s x. x \ set xs \ P s \ 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 \ 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 "\x y. x \ set xs \ y \ set xs \ f y \ f x = f x \ 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 "\x y. x \ set xs \ y \ set xs \ f y \ f x = f x \ 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 \ set xs" "y \ set xs" + with assms have *: "f y = f x \ y = x" by (auto dest: inj_onD) + show "(insort_key f y \ insort_key f x) zs = (insort_key f x \ 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 \ []" + 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 \ 'a \ '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 \ 'a \ '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 \ 'a \ '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 \ 'a \ '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 \ 'a \ '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 \ 'a \ '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 \ 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 \ f) xs bot" + unfolding SUPR_def set_map [symmetric] Sup_set_fold fold_map .. + +text {* @{text nth_map} *} + +definition nth_map :: "nat \ ('a \ 'a) \ 'a list \ '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 \ length xs \ nth_map n f xs = xs" + by (simp add: nth_map_def) + +lemma nth_map_unfold: + "n < length xs \ 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 diff -r f692d6178e4e -r e29a115ba58c src/HOL/Library/More_Set.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/More_Set.thy Thu May 20 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 \ bool" where + "is_empty A \ A = {}" + +definition remove :: "'a \ 'a set \ 'a set" where + "remove x A = A - {x}" + +lemma fun_left_comm_idem_remove: + "fun_left_comm_idem remove" +proof - + have rem: "remove = (\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 = (\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 \ bool) \ 'a set \ 'a set" where + "project P A = {a\A. P a}" + + +subsection {* Basic set operations *} + +lemma is_empty_set: + "is_empty (set xs) \ null xs" + by (simp add: is_empty_def null_empty) + +lemma ball_set: + "(\x\set xs. P x) \ list_all P xs" + by (rule list_ball_code) + +lemma bex_set: + "(\x\set xs. P x) \ 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 \ 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 \ A = foldr Set.insert xs A" +proof - + have "\x y :: 'a. insert y \ insert x = insert x \ 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 "\x y :: 'a. remove y \ remove x = remove x \ 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 \ A \ (\x\A. a = x)" + by simp + +lemma subset_eq: + "A \ B \ (\x\A. x \ B)" + by (fact subset_eq) + +lemma subset: + "A \ B \ A \ B \ \ B \ A" + by (fact less_le_not_le) + +lemma set_eq: + "A = B \ A \ B \ B \ A" + by (fact eq_iff) + +lemma inter: + "A \ B = project (\x. x \ A) B" + by (auto simp add: project_def) + + +subsection {* Various lemmas *} + +lemma not_set_compl: + "Not \ set xs = - set xs" + by (simp add: fun_Compl_def bool_Compl_def comp_def expand_fun_eq) + +end diff -r f692d6178e4e -r e29a115ba58c src/HOL/Library/RBT.thy --- 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]: diff -r f692d6178e4e -r e29a115ba58c src/HOL/List.thy --- 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 \ 'a list \ bool" (infixl "mem" 55) -where - "x mem [] \ False" - | "x mem (y#ys) \ x = y \ x mem ys" +definition member :: "'a list \ 'a \ bool" where + mem_iff [code_post]: "member xs x \ x \ set xs" primrec null:: "'a list \ 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 "\x\set xs"} and @{text "\x\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 \ x \ set xs" -by (induct xs) auto - lemmas in_set_code [code_unfold] = mem_iff [symmetric] +lemma member_simps [simp, code]: + "member [] y \ False" + "member (x # xs) y \ x = y \ 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 \ 'a list \ bool" (infixl "mem" 55) where + "x mem xs \ member xs x" -- "for backward compatibility" + lemma empty_null: "xs = [] \ null xs" by (cases xs) simp_all diff -r f692d6178e4e -r e29a115ba58c src/HOL/MicroJava/BV/BVExample.thy --- 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 @@ (\(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 diff -r f692d6178e4e -r e29a115ba58c src/HOL/ex/Codegenerator_Candidates.thy --- 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