--- a/NEWS Fri Jan 06 20:18:49 2012 +0100
+++ b/NEWS Fri Jan 06 20:48:52 2012 +0100
@@ -101,10 +101,15 @@
INCOMPATIBILITY.
* 'set' is now a proper type constructor. Definitions mem_def and Collect_def
-have disappeared. INCOMPATIBILITY, rephrase sets S used as predicates by
-"%x. x : S" and predicates P used as sets by "{x. P x}". For typical proofs,
-it is often sufficent to prune any tinkering with former theorems mem_def
+have disappeared. INCOMPATIBILITY.
+For developments keeping predicates and sets
+separate, it is often sufficient to rephrase sets S accidentally used as predicates by
+"%x. x : S" and predicates P accidentally used as sets by "{x. P x}". Corresponding
+proofs in a first step should be pruned from any tinkering with former theorems mem_def
and Collect_def.
+For developments which deliberately mixed predicates and sets, a planning step is
+necessary to determine what should become a predicate and what a set. It can be helpful
+to carry out that step in Isabelle 2011-1 before jumping to the current release.
* Theory HOL/Library/AList has been renamed to AList_Impl. INCOMPATIBILITY.
--- a/src/HOL/IsaMakefile Fri Jan 06 20:18:49 2012 +0100
+++ b/src/HOL/IsaMakefile Fri Jan 06 20:48:52 2012 +0100
@@ -286,7 +286,6 @@
List.thy \
Main.thy \
Map.thy \
- More_List.thy \
More_Set.thy \
Nat_Numeral.thy \
Nat_Transfer.thy \
--- a/src/HOL/Library/Monad_Syntax.thy Fri Jan 06 20:18:49 2012 +0100
+++ b/src/HOL/Library/Monad_Syntax.thy Fri Jan 06 20:48:52 2012 +0100
@@ -74,7 +74,7 @@
#> Adhoc_Overloading.add_variant @{const_name bind} @{const_name Set.bind}
#> Adhoc_Overloading.add_variant @{const_name bind} @{const_name Predicate.bind}
#> Adhoc_Overloading.add_variant @{const_name bind} @{const_name Option.bind}
- #> Adhoc_Overloading.add_variant @{const_name bind} @{const_name More_List.bind}
+ #> Adhoc_Overloading.add_variant @{const_name bind} @{const_name List.bind}
*}
end
--- a/src/HOL/List.thy Fri Jan 06 20:18:49 2012 +0100
+++ b/src/HOL/List.thy Fri Jan 06 20:48:52 2012 +0100
@@ -5109,6 +5109,19 @@
by (induct xs) force+
+subsection {* Monad operation *}
+
+definition bind :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b list) \<Rightarrow> 'b list" where
+ "bind xs f = concat (map f xs)"
+
+hide_const (open) bind
+
+lemma bind_simps [simp]:
+ "List.bind [] f = []"
+ "List.bind (x # xs) f = f x @ List.bind xs f"
+ by (simp_all add: bind_def)
+
+
subsection {* Transfer *}
definition
--- a/src/HOL/More_List.thy Fri Jan 06 20:18:49 2012 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,47 +0,0 @@
-(* Author: Florian Haftmann, TU Muenchen *)
-
-header {* Operations on lists beyond the standard List theory *}
-
-theory More_List
-imports List
-begin
-
-text {* @{text nth_map} *}
-
-definition nth_map :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
- "nth_map n f xs = (if n < length xs then
- take n xs @ [f (xs ! n)] @ drop (Suc n) xs
- else xs)"
-
-lemma nth_map_id:
- "n \<ge> length xs \<Longrightarrow> nth_map n f xs = xs"
- by (simp add: nth_map_def)
-
-lemma nth_map_unfold:
- "n < length xs \<Longrightarrow> nth_map n f xs = take n xs @ [f (xs ! n)] @ drop (Suc n) xs"
- by (simp add: nth_map_def)
-
-lemma nth_map_Nil [simp]:
- "nth_map n f [] = []"
- by (simp add: nth_map_def)
-
-lemma nth_map_zero [simp]:
- "nth_map 0 f (x # xs) = f x # xs"
- by (simp add: nth_map_def)
-
-lemma nth_map_Suc [simp]:
- "nth_map (Suc n) f (x # xs) = x # nth_map n f xs"
- by (simp add: nth_map_def)
-
-
-text {* monad operation *}
-
-definition bind :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b list) \<Rightarrow> 'b list" where
- "bind xs f = concat (map f xs)"
-
-lemma bind_simps [simp]:
- "bind [] f = []"
- "bind (x # xs) f = f x @ bind xs f"
- by (simp_all add: bind_def)
-
-end
--- a/src/HOL/More_Set.thy Fri Jan 06 20:18:49 2012 +0100
+++ b/src/HOL/More_Set.thy Fri Jan 06 20:48:52 2012 +0100
@@ -4,7 +4,7 @@
header {* Relating (finite) sets and lists *}
theory More_Set
-imports More_List
+imports List
begin
lemma comp_fun_idem_remove: