--- 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 \
--- 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 \<times> '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 \<Longrightarrow> xs = ys"
-by(simp add: impl_of_inject)
-
-lemma alist_eq_iff: "xs = ys \<longleftrightarrow> 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 \<Rightarrow> 'key \<Rightarrow> 'value option"
-where [code]: "lookup xs = map_of (impl_of xs)"
-
-definition empty :: "('key, 'value) alist"
-where [code del]: "empty = Alist []"
-
-definition update :: "'key \<Rightarrow> 'value \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('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 \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
-where [code del]: "delete k xs = Alist (AList_Impl.delete k (impl_of xs))"
-
-definition map_entry :: "'key \<Rightarrow> ('value \<Rightarrow> 'value) \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
-where [code del]: "map_entry k f xs = Alist (AList_Impl.map_entry k f (impl_of xs))"
-
-definition filter :: "('key \<times> 'value \<Rightarrow> bool) \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('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 "\<circ>>" 60)
-notation scomp (infixl "\<circ>\<rightarrow>" 60)
-
-definition (in term_syntax)
- valterm_empty :: "('key :: typerep, 'value :: typerep) alist \<times> (unit \<Rightarrow> Code_Evaluation.term)"
-where
- "valterm_empty = Code_Evaluation.valtermify empty"
-
-definition (in term_syntax)
- valterm_update :: "'key :: typerep \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow>
- 'value :: typerep \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow>
- ('key, 'value) alist \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow>
- ('key, 'value) alist \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
- [code_unfold]: "valterm_update k v a = Code_Evaluation.valtermify update {\<cdot>} k {\<cdot>} v {\<cdot>}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 \<circ>\<rightarrow> (%k. Quickcheck.random j \<circ>\<rightarrow> (%v. random_aux_alist (i - 1) j \<circ>\<rightarrow> (%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 "\<circ>>" 60)
-no_notation scomp (infixl "\<circ>\<rightarrow>" 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
--- /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 \<times> '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 \<Longrightarrow> xs = ys"
+by(simp add: impl_of_inject)
+
+lemma alist_eq_iff: "xs = ys \<longleftrightarrow> 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 \<Rightarrow> 'key \<Rightarrow> 'value option"
+where [code]: "lookup xs = map_of (impl_of xs)"
+
+definition empty :: "('key, 'value) alist"
+where [code del]: "empty = Alist []"
+
+definition update :: "'key \<Rightarrow> 'value \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('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 \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
+where [code del]: "delete k xs = Alist (AList_Impl.delete k (impl_of xs))"
+
+definition map_entry :: "'key \<Rightarrow> ('value \<Rightarrow> 'value) \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
+where [code del]: "map_entry k f xs = Alist (AList_Impl.map_entry k f (impl_of xs))"
+
+definition filter :: "('key \<times> 'value \<Rightarrow> bool) \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('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 "\<circ>>" 60)
+notation scomp (infixl "\<circ>\<rightarrow>" 60)
+
+definition (in term_syntax)
+ valterm_empty :: "('key :: typerep, 'value :: typerep) alist \<times> (unit \<Rightarrow> Code_Evaluation.term)"
+where
+ "valterm_empty = Code_Evaluation.valtermify empty"
+
+definition (in term_syntax)
+ valterm_update :: "'key :: typerep \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow>
+ 'value :: typerep \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow>
+ ('key, 'value) alist \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow>
+ ('key, 'value) alist \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
+ [code_unfold]: "valterm_update k v a = Code_Evaluation.valtermify update {\<cdot>} k {\<cdot>} v {\<cdot>}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 \<circ>\<rightarrow> (%k. Quickcheck.random j \<circ>\<rightarrow> (%v. random_aux_alist (i - 1) j \<circ>\<rightarrow> (%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 "\<circ>>" 60)
+no_notation scomp (infixl "\<circ>\<rightarrow>" 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
--- 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 \<Rightarrow> '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 \<circ> fst) xs)"
+ "Multiset.filter P (Bag xs) = Bag (DAList.filter (P \<circ> fst) xs)"
by (rule multiset_eqI) (simp add: count_of_filter impl_of_filter)
lemma mset_less_eq_Bag [code]:
- "Bag xs \<le> A \<longleftrightarrow> (\<forall>(x, n) \<in> set (AList.impl_of xs). count_of (AList.impl_of xs) x \<le> count A x)"
+ "Bag xs \<le> A \<longleftrightarrow> (\<forall>(x, n) \<in> set (DAList.impl_of xs). count_of (DAList.impl_of xs) x \<le> count A x)"
(is "?lhs \<longleftrightarrow> ?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 \<le> count A x"
- by (cases "x \<in> fst ` set (AList.impl_of xs)") (auto simp add: count_of_empty)
+ from `?rhs` have "count_of (DAList.impl_of xs) x \<le> count A x"
+ by (cases "x \<in> fst ` set (DAList.impl_of xs)") (auto simp add: count_of_empty)
then show "count (Bag xs) x \<le> count A x"
by (simp add: mset_le_def count_Bag)
qed