# HG changeset patch
# User haftmann
# Date 1244201733 -7200
# Node ID 1ff89cc00898ee623314afce89cf44861054517e
# Parent  4b56acf24a1a64fbac2ad1b2aaa50b4992c27194# Parent  b2aca38301c4a0a6fc5defda79ad93b46fbb5cd3
merged

diff -r 4b56acf24a1a -r 1ff89cc00898 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Fri Jun 05 09:54:47 2009 +0200
+++ b/src/HOL/Finite_Set.thy	Fri Jun 05 13:35:33 2009 +0200
@@ -3266,4 +3266,109 @@
 
 end
 
+
+subsection {* Expressing set operations via @{const fold} *}
+
+lemma (in fun_left_comm) fun_left_comm_apply:
+  "fun_left_comm (\<lambda>x. f (g x))"
+proof
+qed (simp_all add: fun_left_comm)
+
+lemma (in fun_left_comm_idem) fun_left_comm_idem_apply:
+  "fun_left_comm_idem (\<lambda>x. f (g x))"
+  by (rule fun_left_comm_idem.intro, rule fun_left_comm_apply, unfold_locales)
+    (simp_all add: fun_left_idem)
+
+lemma fun_left_comm_idem_insert:
+  "fun_left_comm_idem insert"
+proof
+qed auto
+
+lemma fun_left_comm_idem_remove:
+  "fun_left_comm_idem (\<lambda>x A. A - {x})"
+proof
+qed auto
+
+lemma fun_left_comm_idem_inter:
+  "fun_left_comm_idem op \<inter>"
+proof
+qed auto
+
+lemma fun_left_comm_idem_union:
+  "fun_left_comm_idem op \<union>"
+proof
+qed auto
+
+lemma union_fold_insert:
+  assumes "finite A"
+  shows "A \<union> B = fold insert B A"
+proof -
+  interpret fun_left_comm_idem insert by (fact fun_left_comm_idem_insert)
+  from `finite A` show ?thesis by (induct A arbitrary: B) simp_all
+qed
+
+lemma minus_fold_remove:
+  assumes "finite A"
+  shows "B - A = fold (\<lambda>x A. A - {x}) B A"
+proof -
+  interpret fun_left_comm_idem "\<lambda>x A. A - {x}" by (fact fun_left_comm_idem_remove)
+  from `finite A` show ?thesis by (induct A arbitrary: B) auto
+qed
+
+lemma inter_Inter_fold_inter:
+  assumes "finite A"
+  shows "B \<inter> Inter A = fold (op \<inter>) B A"
+proof -
+  interpret fun_left_comm_idem "op \<inter>" by (fact fun_left_comm_idem_inter)
+  from `finite A` show ?thesis by (induct A arbitrary: B)
+    (simp_all add: fold_fun_comm Int_commute)
+qed
+
+lemma union_Union_fold_union:
+  assumes "finite A"
+  shows "B \<union> Union A = fold (op \<union>) B A"
+proof -
+  interpret fun_left_comm_idem "op \<union>" by (fact fun_left_comm_idem_union)
+  from `finite A` show ?thesis by (induct A arbitrary: B)
+    (simp_all add: fold_fun_comm Un_commute)
+qed
+
+lemma Inter_fold_inter:
+  assumes "finite A"
+  shows "Inter A = fold (op \<inter>) UNIV A"
+  using assms inter_Inter_fold_inter [of A UNIV] by simp
+
+lemma Union_fold_union:
+  assumes "finite A"
+  shows "Union A = fold (op \<union>) {} A"
+  using assms union_Union_fold_union [of A "{}"] by simp
+
+lemma inter_INTER_fold_inter:
+  assumes "finite A"
+  shows "B \<inter> INTER A f = fold (\<lambda>A. op \<inter> (f A)) B A" (is "?inter = ?fold") 
+proof (rule sym)
+  interpret fun_left_comm_idem "op \<inter>" by (fact fun_left_comm_idem_inter)
+  interpret fun_left_comm_idem "\<lambda>A. op \<inter> (f A)" by (fact fun_left_comm_idem_apply)
+  from `finite A` show "?fold = ?inter" by (induct A arbitrary: B) auto
+qed
+
+lemma union_UNION_fold_union:
+  assumes "finite A"
+  shows "B \<union> UNION A f = fold (\<lambda>A. op \<union> (f A)) B A" (is "?union = ?fold") 
+proof (rule sym)
+  interpret fun_left_comm_idem "op \<union>" by (fact fun_left_comm_idem_union)
+  interpret fun_left_comm_idem "\<lambda>A. op \<union> (f A)" by (fact fun_left_comm_idem_apply)
+  from `finite A` show "?fold = ?union" by (induct A arbitrary: B) auto
+qed
+
+lemma INTER_fold_inter:
+  assumes "finite A"
+  shows "INTER A f = fold (\<lambda>A. op \<inter> (f A)) UNIV A"
+  using assms inter_INTER_fold_inter [of A UNIV] by simp
+
+lemma UNION_fold_union:
+  assumes "finite A"
+  shows "UNION A f = fold (\<lambda>A. op \<union> (f A)) {} A"
+  using assms union_UNION_fold_union [of A "{}"] by simp
+
 end
diff -r 4b56acf24a1a -r 1ff89cc00898 src/HOL/Hilbert_Choice.thy
--- a/src/HOL/Hilbert_Choice.thy	Fri Jun 05 09:54:47 2009 +0200
+++ b/src/HOL/Hilbert_Choice.thy	Fri Jun 05 13:35:33 2009 +0200
@@ -12,9 +12,7 @@
 
 subsection {* Hilbert's epsilon *}
 
-axiomatization
-  Eps :: "('a => bool) => 'a"
-where
+axiomatization Eps :: "('a => bool) => 'a" where
   someI: "P x ==> P (Eps P)"
 
 syntax (epsilon)
@@ -586,74 +584,6 @@
 by blast
 
 
-text{*Many of these bindings are used by the ATP linkup, and not just by
-legacy proof scripts.*}
-ML
-{*
-val inv_def = thm "inv_def";
-val Inv_def = thm "Inv_def";
-
-val someI = thm "someI";
-val someI_ex = thm "someI_ex";
-val someI2 = thm "someI2";
-val someI2_ex = thm "someI2_ex";
-val some_equality = thm "some_equality";
-val some1_equality = thm "some1_equality";
-val some_eq_ex = thm "some_eq_ex";
-val some_eq_trivial = thm "some_eq_trivial";
-val some_sym_eq_trivial = thm "some_sym_eq_trivial";
-val choice = thm "choice";
-val bchoice = thm "bchoice";
-val inv_id = thm "inv_id";
-val inv_f_f = thm "inv_f_f";
-val inv_f_eq = thm "inv_f_eq";
-val inj_imp_inv_eq = thm "inj_imp_inv_eq";
-val inj_transfer = thm "inj_transfer";
-val inj_iff = thm "inj_iff";
-val inj_imp_surj_inv = thm "inj_imp_surj_inv";
-val f_inv_f = thm "f_inv_f";
-val surj_f_inv_f = thm "surj_f_inv_f";
-val inv_injective = thm "inv_injective";
-val inj_on_inv = thm "inj_on_inv";
-val surj_imp_inj_inv = thm "surj_imp_inj_inv";
-val surj_iff = thm "surj_iff";
-val surj_imp_inv_eq = thm "surj_imp_inv_eq";
-val bij_imp_bij_inv = thm "bij_imp_bij_inv";
-val inv_equality = thm "inv_equality";
-val inv_inv_eq = thm "inv_inv_eq";
-val o_inv_distrib = thm "o_inv_distrib";
-val image_surj_f_inv_f = thm "image_surj_f_inv_f";
-val image_inv_f_f = thm "image_inv_f_f";
-val inv_image_comp = thm "inv_image_comp";
-val bij_image_Collect_eq = thm "bij_image_Collect_eq";
-val bij_vimage_eq_inv_image = thm "bij_vimage_eq_inv_image";
-val Inv_f_f = thm "Inv_f_f";
-val f_Inv_f = thm "f_Inv_f";
-val Inv_injective = thm "Inv_injective";
-val inj_on_Inv = thm "inj_on_Inv";
-val split_paired_Eps = thm "split_paired_Eps";
-val Eps_split = thm "Eps_split";
-val Eps_split_eq = thm "Eps_split_eq";
-val wf_iff_no_infinite_down_chain = thm "wf_iff_no_infinite_down_chain";
-val Inv_mem = thm "Inv_mem";
-val Inv_f_eq = thm "Inv_f_eq";
-val Inv_comp = thm "Inv_comp";
-val tfl_some = thm "tfl_some";
-val make_neg_rule = thm "make_neg_rule";
-val make_refined_neg_rule = thm "make_refined_neg_rule";
-val make_pos_rule = thm "make_pos_rule";
-val make_neg_rule' = thm "make_neg_rule'";
-val make_pos_rule' = thm "make_pos_rule'";
-val make_neg_goal = thm "make_neg_goal";
-val make_pos_goal = thm "make_pos_goal";
-val conj_forward = thm "conj_forward";
-val disj_forward = thm "disj_forward";
-val disj_forward2 = thm "disj_forward2";
-val all_forward = thm "all_forward";
-val ex_forward = thm "ex_forward";
-*}
-
-
 subsection {* Meson package *}
 
 use "Tools/meson.ML"
@@ -668,4 +598,5 @@
 
 use "Tools/specification_package.ML"
 
+
 end
diff -r 4b56acf24a1a -r 1ff89cc00898 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Jun 05 09:54:47 2009 +0200
+++ b/src/HOL/IsaMakefile	Fri Jun 05 13:35:33 2009 +0200
@@ -349,6 +349,7 @@
   Library/Preorder.thy \
   Library/Product_plus.thy \
   Library/Product_Vector.thy \
+  Library/Tree.thy \
   Library/Enum.thy Library/Float.thy $(SRC)/Tools/float.ML $(SRC)/HOL/Tools/float_arith.ML \
   Library/reify_data.ML Library/reflection.ML \
   Library/LaTeXsugar.thy Library/OptionalSugar.thy
diff -r 4b56acf24a1a -r 1ff89cc00898 src/HOL/Library/Enum.thy
--- a/src/HOL/Library/Enum.thy	Fri Jun 05 09:54:47 2009 +0200
+++ b/src/HOL/Library/Enum.thy	Fri Jun 05 13:35:33 2009 +0200
@@ -43,8 +43,8 @@
 definition
   "eq_class.eq f g \<longleftrightarrow> (\<forall>x \<in> set enum. f x = g x)"
 
-instance by default
-  (simp_all add: eq_fun_def enum_all expand_fun_eq)
+instance proof
+qed (simp_all add: eq_fun_def enum_all expand_fun_eq)
 
 end
 
@@ -185,8 +185,8 @@
 definition
   "enum = [()]"
 
-instance by default
-  (simp_all add: enum_unit_def UNIV_unit)
+instance proof
+qed (simp_all add: enum_unit_def UNIV_unit)
 
 end
 
@@ -196,8 +196,8 @@
 definition
   "enum = [False, True]"
 
-instance by default
-  (simp_all add: enum_bool_def UNIV_bool)
+instance proof
+qed (simp_all add: enum_bool_def UNIV_bool)
 
 end
 
@@ -275,8 +275,8 @@
   "enum = [Nibble0, Nibble1, Nibble2, Nibble3, Nibble4, Nibble5, Nibble6, Nibble7,
     Nibble8, Nibble9, NibbleA, NibbleB, NibbleC, NibbleD, NibbleE, NibbleF]"
 
-instance by default
-  (simp_all add: enum_nibble_def UNIV_nibble)
+instance proof
+qed (simp_all add: enum_nibble_def UNIV_nibble)
 
 end
 
@@ -357,9 +357,9 @@
   Char NibbleF NibbleD, Char NibbleF NibbleE, Char NibbleF NibbleF]"
   unfolding enum_char_def enum_nibble_def by simp
 
-instance by default
-  (auto intro: char.exhaust injI simp add: enum_char_def product_list_set enum_all full_SetCompr_eq [symmetric]
-    distinct_map distinct_product enum_distinct)
+instance proof
+qed (auto intro: char.exhaust injI simp add: enum_char_def product_list_set enum_all full_SetCompr_eq [symmetric]
+  distinct_map distinct_product enum_distinct)
 
 end
 
@@ -369,8 +369,8 @@
 definition
   "enum = None # map Some enum"
 
-instance by default
-  (auto simp add: enum_all enum_option_def, case_tac x, auto intro: inj_onI simp add: distinct_map enum_distinct)
+instance proof
+qed (auto simp add: enum_all enum_option_def, rule option.exhaust, auto intro: simp add: distinct_map enum_distinct)
 
 end
 
diff -r 4b56acf24a1a -r 1ff89cc00898 src/HOL/Library/LaTeXsugar.thy
--- a/src/HOL/Library/LaTeXsugar.thy	Fri Jun 05 09:54:47 2009 +0200
+++ b/src/HOL/Library/LaTeXsugar.thy	Fri Jun 05 13:35:33 2009 +0200
@@ -34,7 +34,7 @@
 
 (* insert *)
 translations 
-  "{x} \<union> A" <= "insert x A"
+  "{x} \<union> A" <= "CONST insert x A"
   "{x,y}" <= "{x} \<union> {y}"
   "{x,y} \<union> A" <= "{x} \<union> ({y} \<union> A)"
   "{x}" <= "{x} \<union> \<emptyset>"
diff -r 4b56acf24a1a -r 1ff89cc00898 src/HOL/Library/Mapping.thy
--- a/src/HOL/Library/Mapping.thy	Fri Jun 05 09:54:47 2009 +0200
+++ b/src/HOL/Library/Mapping.thy	Fri Jun 05 13:35:33 2009 +0200
@@ -1,6 +1,4 @@
-(*  Title:      HOL/Library/Mapping.thy
-    Author:     Florian Haftmann, TU Muenchen
-*)
+(* Author: Florian Haftmann, TU Muenchen *)
 
 header {* An abstract view on maps for code generation. *}
 
@@ -132,4 +130,23 @@
   by (rule sym)
     (auto simp add: bulkload_def tabulate_def expand_fun_eq map_of_eq_None_iff map_compose [symmetric] comp_def)
 
+
+subsection {* Some technical code lemmas *}
+
+lemma [code]:
+  "map_case f m = f (Mapping.lookup m)"
+  by (cases m) simp
+
+lemma [code]:
+  "map_rec f m = f (Mapping.lookup m)"
+  by (cases m) simp
+
+lemma [code]:
+  "Nat.size (m :: (_, _) map) = 0"
+  by (cases m) simp
+
+lemma [code]:
+  "map_size f g m = 0"
+  by (cases m) simp
+
 end
\ No newline at end of file
diff -r 4b56acf24a1a -r 1ff89cc00898 src/HOL/Library/Topology_Euclidean_Space.thy
--- a/src/HOL/Library/Topology_Euclidean_Space.thy	Fri Jun 05 09:54:47 2009 +0200
+++ b/src/HOL/Library/Topology_Euclidean_Space.thy	Fri Jun 05 13:35:33 2009 +0200
@@ -484,25 +484,30 @@
 
 subsection{* Hausdorff and other separation properties *}
 
-axclass t0_space \<subseteq> topological_space
-  t0_space:
-    "x \<noteq> y \<Longrightarrow> \<exists>U. open U \<and> \<not> (x \<in> U \<longleftrightarrow> y \<in> U)"
-
-axclass t1_space \<subseteq> topological_space
-  t1_space:
-    "x \<noteq> y \<Longrightarrow> \<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<notin> U \<and> x \<notin> V \<and> y \<in> V"
-
-instance t1_space \<subseteq> t0_space
-by default (fast dest: t1_space)
+class t0_space =
+  assumes t0_space: "x \<noteq> y \<Longrightarrow> \<exists>U. open U \<and> \<not> (x \<in> U \<longleftrightarrow> y \<in> U)"
+
+class t1_space =
+  assumes t1_space: "x \<noteq> y \<Longrightarrow> \<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<notin> U \<and> x \<notin> V \<and> y \<in> V"
+begin
+
+subclass t0_space
+proof
+qed (fast dest: t1_space)
+
+end
 
 text {* T2 spaces are also known as Hausdorff spaces. *}
 
-axclass t2_space \<subseteq> topological_space
-  hausdorff:
-    "x \<noteq> y \<Longrightarrow> \<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {}"
-
-instance t2_space \<subseteq> t1_space
-by default (fast dest: hausdorff)
+class t2_space =
+  assumes hausdorff: "x \<noteq> y \<Longrightarrow> \<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {}"
+begin
+
+subclass t1_space
+proof
+qed (fast dest: hausdorff)
+
+end
 
 instance metric_space \<subseteq> t2_space
 proof
@@ -568,9 +573,9 @@
   using approachable_lt_le[where f="\<lambda>x'. dist x' x" and P="\<lambda>x'. \<not> (x'\<in>S \<and> x'\<noteq>x)"]
   by metis (* FIXME: VERY slow! *)
 
-axclass perfect_space \<subseteq> metric_space
+class perfect_space =
   (* FIXME: perfect_space should inherit from topological_space *)
-  islimpt_UNIV [simp, intro]: "x islimpt UNIV"
+  assumes islimpt_UNIV [simp, intro]: "(x::'a::metric_space) islimpt UNIV"
 
 lemma perfect_choose_dist:
   fixes x :: "'a::perfect_space"
diff -r 4b56acf24a1a -r 1ff89cc00898 src/HOL/Library/Tree.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Tree.thy	Fri Jun 05 13:35:33 2009 +0200
@@ -0,0 +1,142 @@
+(* Author: Florian Haftmann, TU Muenchen *)
+
+header {* Trees implementing mappings. *}
+
+theory Tree
+imports Mapping
+begin
+
+subsection {* Type definition and operations *}
+
+datatype ('a, 'b) tree = Empty
+  | Branch 'b 'a "('a, 'b) tree" "('a, 'b) tree"
+
+primrec lookup :: "('a\<Colon>linorder, 'b) tree \<Rightarrow> 'a \<rightharpoonup> 'b" where
+  "lookup Empty = (\<lambda>_. None)"
+  | "lookup (Branch v k l r) = (\<lambda>k'. if k' = k then Some v
+       else if k' \<le> k then lookup l k' else lookup r k')"
+
+primrec update :: "'a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> ('a, 'b) tree \<Rightarrow> ('a, 'b) tree" where
+  "update k v Empty = Branch v k Empty Empty"
+  | "update k' v' (Branch v k l r) = (if k' = k then
+      Branch v' k l r else if k' \<le> k
+      then Branch v k (update k' v' l) r
+      else Branch v k l (update k' v' r))"
+
+primrec keys :: "('a\<Colon>linorder, 'b) tree \<Rightarrow> 'a list" where
+  "keys Empty = []"
+  | "keys (Branch _ k l r) = k # keys l @ keys r"
+
+definition size :: "('a\<Colon>linorder, 'b) tree \<Rightarrow> nat" where
+  "size t = length (filter (\<lambda>x. x \<noteq> None) (map (lookup t) (remdups (keys t))))"
+
+fun bulkload :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) tree" where
+  [simp del]: "bulkload ks f = (case ks of [] \<Rightarrow> Empty | _ \<Rightarrow> let
+     mid = length ks div 2;
+     ys = take mid ks;
+     x = ks ! mid;
+     zs = drop (Suc mid) ks
+   in Branch (f x) x (bulkload ys f) (bulkload zs f))"
+
+
+subsection {* Properties *}
+
+lemma dom_lookup:
+  "dom (Tree.lookup t) = set (filter (\<lambda>k. lookup t k \<noteq> None) (remdups (keys t)))"
+proof -
+  have "dom (Tree.lookup t) = set (filter (\<lambda>k. lookup t k \<noteq> None) (keys t))"
+  by (induct t) (auto simp add: dom_if)
+  also have "\<dots> = set (filter (\<lambda>k. lookup t k \<noteq> None) (remdups (keys t)))"
+    by simp
+  finally show ?thesis .
+qed
+
+lemma lookup_finite:
+  "finite (dom (lookup t))"
+  unfolding dom_lookup by simp
+
+lemma lookup_update:
+  "lookup (update k v t) = (lookup t)(k \<mapsto> v)"
+  by (induct t) (simp_all add: expand_fun_eq)
+
+lemma lookup_bulkload:
+  "sorted ks \<Longrightarrow> lookup (bulkload ks f) = (Some o f) |` set ks"
+proof (induct ks f rule: bulkload.induct)
+  case (1 ks f) show ?case proof (cases ks)
+    case Nil then show ?thesis by (simp add: bulkload.simps)
+  next
+    case (Cons w ws)
+    then have case_simp: "\<And>w v::('a, 'b) tree. (case ks of [] \<Rightarrow> v | _ \<Rightarrow> w) = w"
+      by (cases ks) auto
+    from Cons have "ks \<noteq> []" by simp
+    then have "0 < length ks" by simp
+    let ?mid = "length ks div 2"
+    let ?ys = "take ?mid ks"
+    let ?x = "ks ! ?mid"
+    let ?zs = "drop (Suc ?mid) ks"
+    from `ks \<noteq> []` have ks_split: "ks = ?ys @ [?x] @ ?zs"
+      by (simp add: id_take_nth_drop)
+    then have in_ks: "\<And>x. x \<in> set ks \<longleftrightarrow> x \<in> set (?ys @ [?x] @ ?zs)"
+      by simp
+    with ks_split have ys_x: "\<And>y. y \<in> set ?ys \<Longrightarrow> y \<le> ?x"
+      and x_zs: "\<And>z. z \<in> set ?zs \<Longrightarrow> ?x \<le> z"
+    using `sorted ks` sorted_append [of "?ys" "[?x] @ ?zs"] sorted_append [of "[?x]" "?zs"]
+      by simp_all
+    have ys: "lookup (bulkload ?ys f) = (Some o f) |` set ?ys"
+      by (rule "1.hyps"(1)) (auto intro: Cons sorted_take `sorted ks`)
+    have zs: "lookup (bulkload ?zs f) = (Some o f) |` set ?zs"
+      by (rule "1.hyps"(2)) (auto intro: Cons sorted_drop `sorted ks`)
+    show ?thesis using `0 < length ks`
+      by (simp add: bulkload.simps)
+        (auto simp add: restrict_map_def in_ks case_simp Let_def ys zs expand_fun_eq
+           dest: in_set_takeD in_set_dropD ys_x x_zs)
+  qed
+qed
+
+
+subsection {* Trees as mappings *}
+
+definition Tree :: "('a\<Colon>linorder, 'b) tree \<Rightarrow> ('a, 'b) map" where
+  "Tree t = Map (Tree.lookup t)"
+
+lemma [code, code del]:
+  "(eq_class.eq :: (_, _) map \<Rightarrow> _) = eq_class.eq" ..
+
+lemma [code, code del]:
+  "Mapping.delete k m = Mapping.delete k m" ..
+
+code_datatype Tree
+
+lemma empty_Tree [code]:
+  "Mapping.empty = Tree Empty"
+  by (simp add: Tree_def Mapping.empty_def)
+
+lemma lookup_Tree [code]:
+  "Mapping.lookup (Tree t) = lookup t"
+  by (simp add: Tree_def)
+
+lemma update_Tree [code]:
+  "Mapping.update k v (Tree t) = Tree (update k v t)"
+  by (simp add: Tree_def lookup_update)
+
+lemma keys_Tree [code]:
+  "Mapping.keys (Tree t) = set (filter (\<lambda>k. lookup t k \<noteq> None) (remdups (keys t)))"
+  by (simp add: Tree_def dom_lookup)
+
+lemma size_Tree [code]:
+  "Mapping.size (Tree t) = size t"
+proof -
+  have "card (dom (Tree.lookup t)) = length (filter (\<lambda>x. x \<noteq> None) (map (lookup t) (remdups (keys t))))"
+    unfolding dom_lookup by (subst distinct_card) (auto simp add: comp_def)
+  then show ?thesis by (auto simp add: Tree_def Mapping.size_def size_def)
+qed
+
+lemma tabulate_Tree [code]:
+  "Mapping.tabulate ks f = Tree (bulkload (sort ks) f)"
+proof -
+  have "Mapping.lookup (Mapping.tabulate ks f) = Mapping.lookup (Tree (bulkload (sort ks) f))"
+    by (simp add: lookup_Tree lookup_bulkload lookup_tabulate)
+  then show ?thesis by (simp add: lookup_inject)
+qed
+
+end
diff -r 4b56acf24a1a -r 1ff89cc00898 src/HOL/List.thy
--- a/src/HOL/List.thy	Fri Jun 05 09:54:47 2009 +0200
+++ b/src/HOL/List.thy	Fri Jun 05 13:35:33 2009 +0200
@@ -2144,7 +2144,7 @@
   "\<lbrakk>Q x ; \<forall> x\<in> set xs. P x; \<forall> x y. P x \<and> Q y \<longrightarrow> Q (f y x) \<rbrakk> \<Longrightarrow> Q (foldl f x xs)"
   by (induct xs arbitrary: x, simp_all)
 
-text{* @{const foldl} and @{text concat} *}
+text {* @{const foldl} and @{const concat} *}
 
 lemma foldl_conv_concat:
   "foldl (op @) xs xss = xs @ concat xss"
@@ -2158,6 +2158,13 @@
 lemma concat_conv_foldl: "concat xss = foldl (op @) [] xss"
   by (simp add: foldl_conv_concat)
 
+text {* @{const Finite_Set.fold} and @{const foldl} *}
+
+lemma (in fun_left_comm_idem) fold_set:
+  "fold f y (set xs) = foldl (\<lambda>y x. f x y) y xs"
+  by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm)
+
+
 
 subsubsection {* List summation: @{const listsum} and @{text"\<Sum>"}*}
 
diff -r 4b56acf24a1a -r 1ff89cc00898 src/HOL/Nominal/nominal_package.ML
--- a/src/HOL/Nominal/nominal_package.ML	Fri Jun 05 09:54:47 2009 +0200
+++ b/src/HOL/Nominal/nominal_package.ML	Fri Jun 05 13:35:33 2009 +0200
@@ -732,17 +732,18 @@
       let val xs = Long_Name.explode s;
       in Long_Name.implode (Library.nth_map (length xs - i) (strip_suffix 4) xs) end;
 
-    val (descr'', ndescr) = ListPair.unzip (List.mapPartial
+    val (descr'', ndescr) = ListPair.unzip (map_filter
       (fn (i, ("Nominal.noption", _, _)) => NONE
         | (i, (s, dts, constrs)) =>
              let
                val SOME index = AList.lookup op = ty_idxs i;
-               val (constrs1, constrs2) = ListPair.unzip
-                 (map (fn (cname, cargs) => apfst (pair (strip_nth_name 2 (strip_nth_name 1 cname)))
-                   (Library.foldl_map (fn (dts, dt) =>
+               val (constrs2, constrs1) =
+                 map_split (fn (cname, cargs) =>
+                   apsnd (pair (strip_nth_name 2 (strip_nth_name 1 cname)))
+                   (fold_map (fn dt => fn dts =>
                      let val (dts', dt') = strip_option dt
-                     in (dts @ dts' @ [reindex dt'], (length dts, length dts')) end)
-                       ([], cargs))) constrs)
+                     in ((length dts, length dts'), dts @ dts' @ [reindex dt']) end)
+                       cargs [])) constrs
              in SOME ((index, (strip_nth_name 1 s,  map reindex dts, constrs1)),
                (index, constrs2))
              end) descr);
diff -r 4b56acf24a1a -r 1ff89cc00898 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Fri Jun 05 09:54:47 2009 +0200
+++ b/src/HOL/Set.thy	Fri Jun 05 13:35:33 2009 +0200
@@ -20,7 +20,6 @@
 consts
   Collect       :: "('a => bool) => 'a set"              -- "comprehension"
   "op :"        :: "'a => 'a set => bool"                -- "membership"
-  insert        :: "'a => 'a set => 'a set"
   Ball          :: "'a set => ('a => bool) => bool"      -- "bounded universal quantifiers"
   Bex           :: "'a set => ('a => bool) => bool"      -- "bounded existential quantifiers"
   Bex1          :: "'a set => ('a => bool) => bool"      -- "bounded unique existential quantifiers"
@@ -58,19 +57,6 @@
 translations
   "{x. P}"      == "Collect (%x. P)"
 
-definition empty :: "'a set" ("{}") where
-  "empty \<equiv> {x. False}"
-
-definition UNIV :: "'a set" where
-  "UNIV \<equiv> {x. True}"
-
-syntax
-  "@Finset"     :: "args => 'a set"                       ("{(_)}")
-
-translations
-  "{x, xs}"     == "insert x {xs}"
-  "{x}"         == "insert x {}"
-
 definition Int :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Int" 70) where
   "A Int B \<equiv> {x. x \<in> A \<and> x \<in> B}"
 
@@ -85,6 +71,22 @@
   "Int"  (infixl "\<inter>" 70) and
   "Un"  (infixl "\<union>" 65)
 
+definition empty :: "'a set" ("{}") where
+  "empty \<equiv> {x. False}"
+
+definition insert :: "'a \<Rightarrow> 'a set \<Rightarrow> 'a set" where
+  "insert a B \<equiv> {x. x = a} \<union> B"
+
+definition UNIV :: "'a set" where
+  "UNIV \<equiv> {x. True}"
+
+syntax
+  "@Finset"     :: "args => 'a set"                       ("{(_)}")
+
+translations
+  "{x, xs}"     == "CONST insert x {xs}"
+  "{x}"         == "CONST insert x {}"
+
 syntax
   "_Ball"       :: "pttrn => 'a set => bool => bool"      ("(3ALL _:_./ _)" [0, 0, 10] 10)
   "_Bex"        :: "pttrn => 'a set => bool => bool"      ("(3EX _:_./ _)" [0, 0, 10] 10)
@@ -408,7 +410,6 @@
 
 defs
   Pow_def:      "Pow A          == {B. B <= A}"
-  insert_def:   "insert a B     == {x. x=a} Un B"
   image_def:    "f`A            == {y. EX x:A. y = f(x)}"
 
 
@@ -811,7 +812,7 @@
 by blast
 
 
-subsubsection {* Augmenting a set -- insert *}
+subsubsection {* Augmenting a set -- @{const insert} *}
 
 lemma insert_iff [simp]: "(a : insert b A) = (a = b | a:A)"
   by (unfold insert_def) blast
diff -r 4b56acf24a1a -r 1ff89cc00898 src/HOL/TLA/Intensional.thy
--- a/src/HOL/TLA/Intensional.thy	Fri Jun 05 09:54:47 2009 +0200
+++ b/src/HOL/TLA/Intensional.thy	Fri Jun 05 13:35:33 2009 +0200
@@ -126,8 +126,8 @@
   "_liftLeq"      == "_lift2 (op <=)"
   "_liftMem"      == "_lift2 (op :)"
   "_liftNotMem x xs"   == "_liftNot (_liftMem x xs)"
-  "_liftFinset (_liftargs x xs)"  == "_lift2 insert x (_liftFinset xs)"
-  "_liftFinset x" == "_lift2 insert x (_const {})"
+  "_liftFinset (_liftargs x xs)"  == "_lift2 CONST insert x (_liftFinset xs)"
+  "_liftFinset x" == "_lift2 CONST insert x (_const {})"
   "_liftPair x (_liftargs y z)"       == "_liftPair x (_liftPair y z)"
   "_liftPair"     == "_lift2 Pair"
   "_liftCons"     == "lift2 Cons"
diff -r 4b56acf24a1a -r 1ff89cc00898 src/HOL/Tools/datatype_codegen.ML
--- a/src/HOL/Tools/datatype_codegen.ML	Fri Jun 05 09:54:47 2009 +0200
+++ b/src/HOL/Tools/datatype_codegen.ML	Fri Jun 05 13:35:33 2009 +0200
@@ -89,10 +89,10 @@
             val dts' = map (DatatypeAux.typ_of_dtyp descr sorts) dts;
             val T = Type (tname, dts');
             val rest = mk_term_of_def gr "and " xs;
-            val (_, eqs) = Library.foldl_map (fn (prfx, (cname, Ts)) =>
+            val (eqs, _) = fold_map (fn (cname, Ts) => fn prfx =>
               let val args = map (fn i =>
                 str ("x" ^ string_of_int i)) (1 upto length Ts)
-              in ("  | ", Pretty.blk (4,
+              in (Pretty.blk (4,
                 [str prfx, mk_term_of gr module' false T, Pretty.brk 1,
                  if null Ts then str (snd (get_const_id gr cname))
                  else parens (Pretty.block
@@ -100,9 +100,9 @@
                     Pretty.brk 1, mk_tuple args]),
                  str " =", Pretty.brk 1] @
                  mk_constr_term cname Ts T
-                   (map (fn (x, U) => [Pretty.block [mk_term_of gr module' false U,
-                      Pretty.brk 1, x]]) (args ~~ Ts))))
-              end) (prfx, cs')
+                   (map2 (fn x => fn U => [Pretty.block [mk_term_of gr module' false U,
+                      Pretty.brk 1, x]]) args Ts)), "  | ")
+              end) cs' prfx
           in eqs @ rest end;
 
     fun mk_gen_of_def gr prfx [] = []
diff -r 4b56acf24a1a -r 1ff89cc00898 src/HOL/Tools/datatype_realizer.ML
--- a/src/HOL/Tools/datatype_realizer.ML	Fri Jun 05 09:54:47 2009 +0200
+++ b/src/HOL/Tools/datatype_realizer.ML	Fri Jun 05 13:35:33 2009 +0200
@@ -56,17 +56,17 @@
     fun mk_all i s T t =
       if i mem is then list_all_free ([(s, T)], t) else t;
 
-    val (prems, rec_fns) = split_list (List.concat (snd (Library.foldl_map
-      (fn (j, ((i, (_, _, constrs)), T)) => Library.foldl_map (fn (j, (cname, cargs)) =>
+    val (prems, rec_fns) = split_list (flat (fst (fold_map
+      (fn ((i, (_, _, constrs)), T) => fold_map (fn (cname, cargs) => fn j =>
         let
           val Ts = map (typ_of_dtyp descr sorts) cargs;
           val tnames = Name.variant_list pnames (DatatypeProp.make_tnames Ts);
-          val recs = List.filter (is_rec_type o fst o fst) (cargs ~~ tnames ~~ Ts);
+          val recs = filter (is_rec_type o fst o fst) (cargs ~~ tnames ~~ Ts);
           val frees = tnames ~~ Ts;
 
           fun mk_prems vs [] = 
                 let
-                  val rT = List.nth (rec_result_Ts, i);
+                  val rT = nth (rec_result_Ts) i;
                   val vs' = filter_out is_unit vs;
                   val f = mk_Free "f" (map fastype_of vs' ---> rT) j;
                   val f' = Envir.eta_contract (list_abs_free
@@ -80,7 +80,7 @@
                   val k = body_index dt;
                   val (Us, U) = strip_type T;
                   val i = length Us;
-                  val rT = List.nth (rec_result_Ts, k);
+                  val rT = nth (rec_result_Ts) k;
                   val r = Free ("r" ^ s, Us ---> rT);
                   val (p, f) = mk_prems (vs @ [r]) ds
                 in (mk_all k ("r" ^ s) (Us ---> rT) (Logic.mk_implies
@@ -89,9 +89,8 @@
                       (app_bnds (Free (s, T)) i))), p)), f)
                 end
 
-        in (j + 1,
-          apfst (curry list_all_free frees) (mk_prems (map Free frees) recs))
-        end) (j, constrs)) (1, descr ~~ recTs))));
+        in (apfst (curry list_all_free frees) (mk_prems (map Free frees) recs), j + 1) end)
+          constrs) (descr ~~ recTs) 1)));
  
     fun mk_proj j [] t = t
       | mk_proj j (i :: is) t = if null is then t else
diff -r 4b56acf24a1a -r 1ff89cc00898 src/HOL/Tools/hologic.ML
--- a/src/HOL/Tools/hologic.ML	Fri Jun 05 09:54:47 2009 +0200
+++ b/src/HOL/Tools/hologic.ML	Fri Jun 05 13:35:33 2009 +0200
@@ -122,8 +122,10 @@
   val mk_typerep: typ -> term
   val mk_term_of: typ -> term -> term
   val reflect_term: term -> term
+  val mk_valtermify_app: string -> (string * typ) list -> typ -> term
   val mk_return: typ -> typ -> term -> term
   val mk_ST: ((term * typ) * (string * typ) option)  list -> term -> typ -> typ option * typ -> term
+  val mk_random: typ -> term -> term
 end;
 
 structure HOLogic: HOLOGIC =
@@ -152,13 +154,13 @@
   let
     val sT = mk_setT T;
     val empty = Const ("Set.empty", sT);
-    fun insert t u = Const ("insert", T --> sT --> sT) $ t $ u;
+    fun insert t u = Const ("Set.insert", T --> sT --> sT) $ t $ u;
   in fold_rev insert ts empty end;
 
 fun mk_UNIV T = Const ("Set.UNIV", mk_setT T);
 
-fun dest_set (Const ("Orderings.bot", _)) = []
-  | dest_set (Const ("insert", _) $ t $ u) = t :: dest_set u
+fun dest_set (Const ("Set.empty", _)) = []
+  | dest_set (Const ("Set.insert", _) $ t $ u) = t :: dest_set u
   | dest_set t = raise TERM ("dest_set", [t]);
 
 fun Collect_const T = Const ("Collect", (T --> boolT) --> mk_setT T);
@@ -617,6 +619,19 @@
   | reflect_term (Abs (v, _, t)) = Abs (v, termT, reflect_term t)
   | reflect_term t = t;
 
+fun mk_valtermify_app c vs T =
+  let
+    fun termifyT T = mk_prodT (T, unitT --> termT);
+    fun valapp T T' = Const ("Code_Eval.valapp",
+      termifyT (T --> T') --> termifyT T --> termifyT T');
+    fun mk_fTs [] _ = []
+      | mk_fTs (_ :: Ts) T = (Ts ---> T) :: mk_fTs Ts T;
+    val Ts = map snd vs;
+    val t = Const (c, Ts ---> T);
+    val tt = mk_prod (t, Abs ("u", unitT, reflect_term t));
+    fun app (t, (fT, (v, T))) = valapp T fT $ t $ Free (v, termifyT T);
+  in Library.foldl app (tt, mk_fTs Ts T ~~ vs) end;
+
 
 (* open state monads *)
 
@@ -633,4 +648,10 @@
             $ t $ t', U)
   in fold_rev mk_clause clauses (t, U) |> fst end;
 
+val code_numeralT = Type ("Code_Numeral.code_numeral", []);
+val random_seedT = mk_prodT (code_numeralT, code_numeralT);
+
+fun mk_random T t = Const ("Quickcheck.random_class.random", code_numeralT
+  --> random_seedT --> mk_prodT (mk_prodT (T, unitT --> termT), random_seedT)) $ t;
+
 end;
diff -r 4b56acf24a1a -r 1ff89cc00898 src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Fri Jun 05 09:54:47 2009 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML	Fri Jun 05 13:35:33 2009 +0200
@@ -315,16 +315,16 @@
     fun get f = (these oo Option.map) f;
     val rec_names = distinct (op =) (map (fst o dest_Const o head_of o fst o
       HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) (get #rec_thms dt_info));
-    val (_, constrss) = Library.foldl_map (fn ((recs, dummies), (s, rs)) =>
-      if s mem rsets then
+    val (constrss, _) = fold_map (fn (s, rs) => fn (recs, dummies) =>
+      if member (op =) rsets s then
         let
           val (d :: dummies') = dummies;
           val (recs1, recs2) = chop (length rs) (if d then tl recs else recs)
-        in ((recs2, dummies'), map (head_of o hd o rev o snd o strip_comb o
-          fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) recs1)
+        in (map (head_of o hd o rev o snd o strip_comb o fst o
+          HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) recs1, (recs2, dummies'))
         end
-      else ((recs, dummies), replicate (length rs) Extraction.nullt))
-        ((get #rec_thms dt_info, dummies), rss);
+      else (replicate (length rs) Extraction.nullt, (recs, dummies)))
+        rss (get #rec_thms dt_info, dummies);
     val rintrs = map (fn (intr, c) => Envir.eta_contract
       (Extraction.realizes_of thy2 vs
         (if c = Extraction.nullt then c else list_comb (c, map Var (rev
@@ -360,7 +360,7 @@
 
     (** realizer for induction rule **)
 
-    val Ps = List.mapPartial (fn _ $ M $ P => if pred_of M mem rsets then
+    val Ps = map_filter (fn _ $ M $ P => if pred_of M mem rsets then
       SOME (fst (fst (dest_Var (head_of P)))) else NONE)
         (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of raw_induct)));
 
diff -r 4b56acf24a1a -r 1ff89cc00898 src/HOL/Tools/meson.ML
--- a/src/HOL/Tools/meson.ML	Fri Jun 05 09:54:47 2009 +0200
+++ b/src/HOL/Tools/meson.ML	Fri Jun 05 13:35:33 2009 +0200
@@ -46,6 +46,19 @@
 val max_clauses_default = 60;
 val (max_clauses, setup) = Attrib.config_int "max_clauses" max_clauses_default;
 
+val disj_forward = @{thm disj_forward};
+val disj_forward2 = @{thm disj_forward2};
+val make_pos_rule = @{thm make_pos_rule};
+val make_pos_rule' = @{thm make_pos_rule'};
+val make_pos_goal = @{thm make_pos_goal};
+val make_neg_rule = @{thm make_neg_rule};
+val make_neg_rule' = @{thm make_neg_rule'};
+val make_neg_goal = @{thm make_neg_goal};
+val conj_forward = @{thm conj_forward};
+val all_forward = @{thm all_forward};
+val ex_forward = @{thm ex_forward};
+val choice = @{thm choice};
+
 val not_conjD = thm "meson_not_conjD";
 val not_disjD = thm "meson_not_disjD";
 val not_notD = thm "meson_not_notD";
diff -r 4b56acf24a1a -r 1ff89cc00898 src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Fri Jun 05 09:54:47 2009 +0200
+++ b/src/HOL/Tools/res_axioms.ML	Fri Jun 05 13:35:33 2009 +0200
@@ -258,7 +258,7 @@
       val cex = Thm.cterm_of thy (HOLogic.exists_const T)
       val ex_tm = c_mkTrueprop (Thm.capply cex cabs)
       and conc =  c_mkTrueprop (Drule.beta_conv cabs (Drule.list_comb(c,frees)));
-      fun tacf [prem] = rewrite_goals_tac [def] THEN rtac (prem RS someI_ex) 1
+      fun tacf [prem] = rewrite_goals_tac [def] THEN rtac (prem RS @{thm someI_ex}) 1
   in  Goal.prove_internal [ex_tm] conc tacf
        |> forall_intr_list frees
        |> Thm.forall_elim_vars 0  (*Introduce Vars, but don't discharge defs.*)
diff -r 4b56acf24a1a -r 1ff89cc00898 src/HOL/ex/Codegenerator_Candidates.thy
--- a/src/HOL/ex/Codegenerator_Candidates.thy	Fri Jun 05 09:54:47 2009 +0200
+++ b/src/HOL/ex/Codegenerator_Candidates.thy	Fri Jun 05 13:35:33 2009 +0200
@@ -18,6 +18,7 @@
   Primes
   Product_ord
   SetsAndFunctions
+  Tree
   While_Combinator
   Word
   "~~/src/HOL/ex/Commutative_Ring_Complete"