# HG changeset patch # User bulwahn # Date 1326789510 -3600 # Node ID 99c80c2f841a53a480d382d30c97a125a11ae69d # Parent ae79f2978a67e901d5d0c4913047c9517a029b80 renamed theory AList to DAList diff -r ae79f2978a67 -r 99c80c2f841a src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Mon Jan 16 21:50:15 2012 +0100 +++ b/src/HOL/IsaMakefile Tue Jan 17 09:38:30 2012 +0100 @@ -436,7 +436,7 @@ $(OUT)/HOL-Library: $(OUT)/HOL Library/ROOT.ML \ $(SRC)/HOL/Tools/float_arith.ML $(SRC)/Tools/float.ML \ Library/Abstract_Rat.thy $(SRC)/Tools/Adhoc_Overloading.thy \ - Library/AList_Impl.thy Library/AList.thy Library/AList_Mapping.thy \ + Library/AList_Impl.thy Library/AList_Mapping.thy \ Library/BigO.thy Library/Binomial.thy \ Library/Bit.thy Library/Boolean_Algebra.thy Library/Cardinality.thy \ Library/Char_nat.thy Library/Code_Char.thy Library/Code_Char_chr.thy \ @@ -446,8 +446,8 @@ Tools/Predicate_Compile/code_prolog.ML Library/ContNotDenum.thy \ Library/Cset.thy Library/Cset_Monad.thy Library/Continuity.thy \ Library/Convex.thy Library/Countable.thy \ - Library/Dlist.thy Library/Dlist_Cset.thy Library/Efficient_Nat.thy \ - Library/Eval_Witness.thy \ + Library/DAList.thy Library/Dlist.thy Library/Dlist_Cset.thy \ + Library/Efficient_Nat.thy Library/Eval_Witness.thy \ Library/Extended_Real.thy Library/Extended_Nat.thy Library/Float.thy \ Library/Formal_Power_Series.thy Library/Fraction_Field.thy \ Library/FrechetDeriv.thy Library/Cset.thy Library/FuncSet.thy \ diff -r ae79f2978a67 -r 99c80c2f841a src/HOL/Library/AList.thy --- a/src/HOL/Library/AList.thy Mon Jan 16 21:50:15 2012 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,179 +0,0 @@ -(* Title: HOL/Library/AList.thy - Author: Lukas Bulwahn, TU Muenchen *) - -header {* Abstract type of association lists with unique keys *} - -theory AList -imports AList_Impl -begin - -text {* This was based on some existing fragments in the AFP-Collection framework. *} - -subsection {* Type @{text "('key, 'value) alist" } *} - -typedef (open) ('key, 'value) alist = "{xs :: ('key \ 'value) list. distinct (map fst xs)}" -morphisms impl_of Alist -by(rule exI[where x="[]"]) simp - -lemma alist_ext: "impl_of xs = impl_of ys \ xs = ys" -by(simp add: impl_of_inject) - -lemma alist_eq_iff: "xs = ys \ impl_of xs = impl_of ys" -by(simp add: impl_of_inject) - -lemma impl_of_distinct [simp, intro]: "distinct (map fst (impl_of xs))" -using impl_of[of xs] by simp - -lemma Alist_impl_of [code abstype]: "Alist (impl_of xs) = xs" -by(rule impl_of_inverse) - -subsection {* Primitive operations *} - -definition lookup :: "('key, 'value) alist \ 'key \ 'value option" -where [code]: "lookup xs = map_of (impl_of xs)" - -definition empty :: "('key, 'value) alist" -where [code del]: "empty = Alist []" - -definition update :: "'key \ 'value \ ('key, 'value) alist \ ('key, 'value) alist" -where [code del]: "update k v xs = Alist (AList_Impl.update k v (impl_of xs))" - -(* FIXME: we use an unoptimised delete operation. *) -definition delete :: "'key \ ('key, 'value) alist \ ('key, 'value) alist" -where [code del]: "delete k xs = Alist (AList_Impl.delete k (impl_of xs))" - -definition map_entry :: "'key \ ('value \ 'value) \ ('key, 'value) alist \ ('key, 'value) alist" -where [code del]: "map_entry k f xs = Alist (AList_Impl.map_entry k f (impl_of xs))" - -definition filter :: "('key \ 'value \ bool) \ ('key, 'value) alist \ ('key, 'value) alist" -where [code del]: "filter P xs = Alist (List.filter P (impl_of xs))" - -definition map_default :: "'key => 'value => ('value => 'value) => ('key, 'value) alist => ('key, 'value) alist" -where - "map_default k v f xs = Alist (AList_Impl.map_default k v f (impl_of xs))" - -lemma impl_of_empty [code abstract]: "impl_of empty = []" -by (simp add: empty_def Alist_inverse) - -lemma impl_of_update [code abstract]: "impl_of (update k v xs) = AList_Impl.update k v (impl_of xs)" -by (simp add: update_def Alist_inverse distinct_update) - -lemma impl_of_delete [code abstract]: - "impl_of (delete k al) = AList_Impl.delete k (impl_of al)" -unfolding delete_def by (simp add: Alist_inverse distinct_delete) - -lemma impl_of_map_entry [code abstract]: - "impl_of (map_entry k f xs) = AList_Impl.map_entry k f (impl_of xs)" -unfolding map_entry_def by (simp add: Alist_inverse distinct_map_entry) - -lemma distinct_map_fst_filter: - "distinct (map fst xs) ==> distinct (map fst (List.filter P xs))" -by (induct xs) auto - -lemma impl_of_filter [code abstract]: - "impl_of (filter P xs) = List.filter P (impl_of xs)" -unfolding filter_def by (simp add: Alist_inverse distinct_map_fst_filter) - -lemma impl_of_map_default [code abstract]: - "impl_of (map_default k v f xs) = AList_Impl.map_default k v f (impl_of xs)" -by (auto simp add: map_default_def Alist_inverse distinct_map_default) - -subsection {* Abstract operation properties *} - -(* FIXME: to be completed *) - -lemma lookup_empty [simp]: "lookup empty k = None" -by(simp add: empty_def lookup_def Alist_inverse) - -lemma lookup_delete [simp]: "lookup (delete k al) = (lookup al)(k := None)" -by (simp add: lookup_def delete_def Alist_inverse distinct_delete delete_conv') - -subsection {* Further operations *} - -subsubsection {* Equality *} - -instantiation alist :: (equal, equal) equal begin - -definition "HOL.equal (xs :: ('a, 'b) alist) ys == impl_of xs = impl_of ys" - -instance -proof -qed (simp add: equal_alist_def impl_of_inject) - -end - -subsubsection {* Size *} - -instantiation alist :: (type, type) size begin - -definition "size (al :: ('a, 'b) alist) = length (impl_of al)" - -instance .. - -end - -subsection {* Quickcheck generators *} - -notation fcomp (infixl "\>" 60) -notation scomp (infixl "\\" 60) - -definition (in term_syntax) - valterm_empty :: "('key :: typerep, 'value :: typerep) alist \ (unit \ Code_Evaluation.term)" -where - "valterm_empty = Code_Evaluation.valtermify empty" - -definition (in term_syntax) - valterm_update :: "'key :: typerep \ (unit \ Code_Evaluation.term) \ - 'value :: typerep \ (unit \ Code_Evaluation.term) \ - ('key, 'value) alist \ (unit \ Code_Evaluation.term) \ - ('key, 'value) alist \ (unit \ Code_Evaluation.term)" where - [code_unfold]: "valterm_update k v a = Code_Evaluation.valtermify update {\} k {\} v {\}a" - -fun (in term_syntax) random_aux_alist -where - "random_aux_alist i j = (if i = 0 then Pair valterm_empty else Quickcheck.collapse (Random.select_weight [(i, Quickcheck.random j \\ (%k. Quickcheck.random j \\ (%v. random_aux_alist (i - 1) j \\ (%a. Pair (valterm_update k v a))))), (1, Pair valterm_empty)]))" - -instantiation alist :: (random, random) random -begin - -definition random_alist -where - "random_alist i = random_aux_alist i i" - -instance .. - -end - -no_notation fcomp (infixl "\>" 60) -no_notation scomp (infixl "\\" 60) - -instantiation alist :: (exhaustive, exhaustive) exhaustive -begin - -fun exhaustive_alist :: "(('a, 'b) alist => (bool * term list) option) => code_numeral => (bool * term list) option" -where - "exhaustive_alist f i = (if i = 0 then None else case f empty of Some ts => Some ts | None => - exhaustive_alist (%a. Quickcheck_Exhaustive.exhaustive (%k. Quickcheck_Exhaustive.exhaustive (%v. f (update k v a)) (i - 1)) (i - 1)) (i - 1))" - -instance .. - -end - -instantiation alist :: (full_exhaustive, full_exhaustive) full_exhaustive -begin - -fun full_exhaustive_alist :: "(('a, 'b) alist * (unit => term) => (bool * term list) option) => code_numeral => (bool * term list) option" -where - "full_exhaustive_alist f i = (if i = 0 then None else case f valterm_empty of Some ts => Some ts | None => - full_exhaustive_alist (%a. Quickcheck_Exhaustive.full_exhaustive (%k. Quickcheck_Exhaustive.full_exhaustive (%v. f (valterm_update k v a)) (i - 1)) (i - 1)) (i - 1))" - -instance .. - -end - -hide_const valterm_empty valterm_update random_aux_alist - -hide_fact (open) lookup_def empty_def update_def delete_def map_entry_def filter_def map_default_def -hide_const (open) impl_of lookup empty update delete map_entry filter map_default - -end \ No newline at end of file diff -r ae79f2978a67 -r 99c80c2f841a src/HOL/Library/DAList.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/DAList.thy Tue Jan 17 09:38:30 2012 +0100 @@ -0,0 +1,179 @@ +(* Title: HOL/Library/DAList.thy + Author: Lukas Bulwahn, TU Muenchen *) + +header {* Abstract type of association lists with unique keys *} + +theory DAList +imports AList_Impl +begin + +text {* This was based on some existing fragments in the AFP-Collection framework. *} + +subsection {* Type @{text "('key, 'value) alist" } *} + +typedef (open) ('key, 'value) alist = "{xs :: ('key \ 'value) list. distinct (map fst xs)}" +morphisms impl_of Alist +by(rule exI[where x="[]"]) simp + +lemma alist_ext: "impl_of xs = impl_of ys \ xs = ys" +by(simp add: impl_of_inject) + +lemma alist_eq_iff: "xs = ys \ impl_of xs = impl_of ys" +by(simp add: impl_of_inject) + +lemma impl_of_distinct [simp, intro]: "distinct (map fst (impl_of xs))" +using impl_of[of xs] by simp + +lemma Alist_impl_of [code abstype]: "Alist (impl_of xs) = xs" +by(rule impl_of_inverse) + +subsection {* Primitive operations *} + +definition lookup :: "('key, 'value) alist \ 'key \ 'value option" +where [code]: "lookup xs = map_of (impl_of xs)" + +definition empty :: "('key, 'value) alist" +where [code del]: "empty = Alist []" + +definition update :: "'key \ 'value \ ('key, 'value) alist \ ('key, 'value) alist" +where [code del]: "update k v xs = Alist (AList_Impl.update k v (impl_of xs))" + +(* FIXME: we use an unoptimised delete operation. *) +definition delete :: "'key \ ('key, 'value) alist \ ('key, 'value) alist" +where [code del]: "delete k xs = Alist (AList_Impl.delete k (impl_of xs))" + +definition map_entry :: "'key \ ('value \ 'value) \ ('key, 'value) alist \ ('key, 'value) alist" +where [code del]: "map_entry k f xs = Alist (AList_Impl.map_entry k f (impl_of xs))" + +definition filter :: "('key \ 'value \ bool) \ ('key, 'value) alist \ ('key, 'value) alist" +where [code del]: "filter P xs = Alist (List.filter P (impl_of xs))" + +definition map_default :: "'key => 'value => ('value => 'value) => ('key, 'value) alist => ('key, 'value) alist" +where + "map_default k v f xs = Alist (AList_Impl.map_default k v f (impl_of xs))" + +lemma impl_of_empty [code abstract]: "impl_of empty = []" +by (simp add: empty_def Alist_inverse) + +lemma impl_of_update [code abstract]: "impl_of (update k v xs) = AList_Impl.update k v (impl_of xs)" +by (simp add: update_def Alist_inverse distinct_update) + +lemma impl_of_delete [code abstract]: + "impl_of (delete k al) = AList_Impl.delete k (impl_of al)" +unfolding delete_def by (simp add: Alist_inverse distinct_delete) + +lemma impl_of_map_entry [code abstract]: + "impl_of (map_entry k f xs) = AList_Impl.map_entry k f (impl_of xs)" +unfolding map_entry_def by (simp add: Alist_inverse distinct_map_entry) + +lemma distinct_map_fst_filter: + "distinct (map fst xs) ==> distinct (map fst (List.filter P xs))" +by (induct xs) auto + +lemma impl_of_filter [code abstract]: + "impl_of (filter P xs) = List.filter P (impl_of xs)" +unfolding filter_def by (simp add: Alist_inverse distinct_map_fst_filter) + +lemma impl_of_map_default [code abstract]: + "impl_of (map_default k v f xs) = AList_Impl.map_default k v f (impl_of xs)" +by (auto simp add: map_default_def Alist_inverse distinct_map_default) + +subsection {* Abstract operation properties *} + +(* FIXME: to be completed *) + +lemma lookup_empty [simp]: "lookup empty k = None" +by(simp add: empty_def lookup_def Alist_inverse) + +lemma lookup_delete [simp]: "lookup (delete k al) = (lookup al)(k := None)" +by (simp add: lookup_def delete_def Alist_inverse distinct_delete delete_conv') + +subsection {* Further operations *} + +subsubsection {* Equality *} + +instantiation alist :: (equal, equal) equal begin + +definition "HOL.equal (xs :: ('a, 'b) alist) ys == impl_of xs = impl_of ys" + +instance +proof +qed (simp add: equal_alist_def impl_of_inject) + +end + +subsubsection {* Size *} + +instantiation alist :: (type, type) size begin + +definition "size (al :: ('a, 'b) alist) = length (impl_of al)" + +instance .. + +end + +subsection {* Quickcheck generators *} + +notation fcomp (infixl "\>" 60) +notation scomp (infixl "\\" 60) + +definition (in term_syntax) + valterm_empty :: "('key :: typerep, 'value :: typerep) alist \ (unit \ Code_Evaluation.term)" +where + "valterm_empty = Code_Evaluation.valtermify empty" + +definition (in term_syntax) + valterm_update :: "'key :: typerep \ (unit \ Code_Evaluation.term) \ + 'value :: typerep \ (unit \ Code_Evaluation.term) \ + ('key, 'value) alist \ (unit \ Code_Evaluation.term) \ + ('key, 'value) alist \ (unit \ Code_Evaluation.term)" where + [code_unfold]: "valterm_update k v a = Code_Evaluation.valtermify update {\} k {\} v {\}a" + +fun (in term_syntax) random_aux_alist +where + "random_aux_alist i j = (if i = 0 then Pair valterm_empty else Quickcheck.collapse (Random.select_weight [(i, Quickcheck.random j \\ (%k. Quickcheck.random j \\ (%v. random_aux_alist (i - 1) j \\ (%a. Pair (valterm_update k v a))))), (1, Pair valterm_empty)]))" + +instantiation alist :: (random, random) random +begin + +definition random_alist +where + "random_alist i = random_aux_alist i i" + +instance .. + +end + +no_notation fcomp (infixl "\>" 60) +no_notation scomp (infixl "\\" 60) + +instantiation alist :: (exhaustive, exhaustive) exhaustive +begin + +fun exhaustive_alist :: "(('a, 'b) alist => (bool * term list) option) => code_numeral => (bool * term list) option" +where + "exhaustive_alist f i = (if i = 0 then None else case f empty of Some ts => Some ts | None => + exhaustive_alist (%a. Quickcheck_Exhaustive.exhaustive (%k. Quickcheck_Exhaustive.exhaustive (%v. f (update k v a)) (i - 1)) (i - 1)) (i - 1))" + +instance .. + +end + +instantiation alist :: (full_exhaustive, full_exhaustive) full_exhaustive +begin + +fun full_exhaustive_alist :: "(('a, 'b) alist * (unit => term) => (bool * term list) option) => code_numeral => (bool * term list) option" +where + "full_exhaustive_alist f i = (if i = 0 then None else case f valterm_empty of Some ts => Some ts | None => + full_exhaustive_alist (%a. Quickcheck_Exhaustive.full_exhaustive (%k. Quickcheck_Exhaustive.full_exhaustive (%v. f (valterm_update k v a)) (i - 1)) (i - 1)) (i - 1))" + +instance .. + +end + +hide_const valterm_empty valterm_update random_aux_alist + +hide_fact (open) lookup_def empty_def update_def delete_def map_entry_def filter_def map_default_def +hide_const (open) impl_of lookup empty update delete map_entry filter map_default + +end \ No newline at end of file diff -r ae79f2978a67 -r 99c80c2f841a src/HOL/Library/Multiset.thy --- a/src/HOL/Library/Multiset.thy Mon Jan 16 21:50:15 2012 +0100 +++ b/src/HOL/Library/Multiset.thy Tue Jan 17 09:38:30 2012 +0100 @@ -5,7 +5,7 @@ header {* (Finite) multisets *} theory Multiset -imports Main AList +imports Main DAList begin subsection {* The type of multisets *} @@ -1101,18 +1101,18 @@ definition join where - "join f xs ys = AList.Alist (join_raw f (AList.impl_of xs) (AList.impl_of ys))" + "join f xs ys = DAList.Alist (join_raw f (DAList.impl_of xs) (DAList.impl_of ys))" lemma [code abstract]: - "AList.impl_of (join f xs ys) = join_raw f (AList.impl_of xs) (AList.impl_of ys)" + "DAList.impl_of (join f xs ys) = join_raw f (DAList.impl_of xs) (DAList.impl_of ys)" unfolding join_def by (simp add: Alist_inverse distinct_join_raw) definition subtract_entries where - "subtract_entries xs ys = AList.Alist (subtract_entries_raw (AList.impl_of xs) (AList.impl_of ys))" + "subtract_entries xs ys = DAList.Alist (subtract_entries_raw (DAList.impl_of xs) (DAList.impl_of ys))" lemma [code abstract]: - "AList.impl_of (subtract_entries xs ys) = subtract_entries_raw (AList.impl_of xs) (AList.impl_of ys)" + "DAList.impl_of (subtract_entries xs ys) = subtract_entries_raw (DAList.impl_of xs) (DAList.impl_of ys)" unfolding subtract_entries_def by (simp add: Alist_inverse distinct_subtract_entries_raw) text {* Implementing multisets by means of association lists *} @@ -1166,12 +1166,12 @@ text {* Code equations for multiset operations *} definition Bag :: "('a, nat) alist \ 'a multiset" where - "Bag xs = Abs_multiset (count_of (AList.impl_of xs))" + "Bag xs = Abs_multiset (count_of (DAList.impl_of xs))" code_datatype Bag lemma count_Bag [simp, code]: - "count (Bag xs) = count_of (AList.impl_of xs)" + "count (Bag xs) = count_of (DAList.impl_of xs)" by (simp add: Bag_def count_of_multiset Abs_multiset_inverse) lemma Mempty_Bag [code]: @@ -1192,11 +1192,11 @@ (simp add: count_of_subtract_entries_raw alist.Alist_inverse distinct_subtract_entries_raw subtract_entries_def) lemma filter_Bag [code]: - "Multiset.filter P (Bag xs) = Bag (AList.filter (P \ fst) xs)" + "Multiset.filter P (Bag xs) = Bag (DAList.filter (P \ fst) xs)" by (rule multiset_eqI) (simp add: count_of_filter impl_of_filter) lemma mset_less_eq_Bag [code]: - "Bag xs \ A \ (\(x, n) \ set (AList.impl_of xs). count_of (AList.impl_of xs) x \ count A x)" + "Bag xs \ A \ (\(x, n) \ set (DAList.impl_of xs). count_of (DAList.impl_of xs) x \ count A x)" (is "?lhs \ ?rhs") proof assume ?lhs then show ?rhs @@ -1206,8 +1206,8 @@ show ?lhs proof (rule mset_less_eqI) fix x - from `?rhs` have "count_of (AList.impl_of xs) x \ count A x" - by (cases "x \ fst ` set (AList.impl_of xs)") (auto simp add: count_of_empty) + from `?rhs` have "count_of (DAList.impl_of xs) x \ count A x" + by (cases "x \ fst ` set (DAList.impl_of xs)") (auto simp add: count_of_empty) then show "count (Bag xs) x \ count A x" by (simp add: mset_le_def count_Bag) qed