# HG changeset patch
# User bulwahn
# Date 1267605226 -3600
# Node ID 67879e5d695ce44da5fe05f33e7a3595901a1d41
# Parent  94170181a842f21de0eac1942744cd9b363b7d5f# Parent  00f3bbadbb2dd616d8e73742cff765d0a603970f
merged

diff -r 94170181a842 -r 67879e5d695c src/HOL/Library/RBT.thy
--- a/src/HOL/Library/RBT.thy	Tue Mar 02 22:13:39 2010 +0100
+++ b/src/HOL/Library/RBT.thy	Wed Mar 03 09:33:46 2010 +0100
@@ -11,135 +11,151 @@
 begin
 
 datatype color = R | B
-datatype ('a,'b)"rbt" = Empty | Tr color "('a,'b)rbt" 'a 'b "('a,'b)rbt"
+datatype ('a, 'b) rbt = Empty | Branch color "('a, 'b) rbt" 'a 'b "('a, 'b) rbt"
+
+lemma rbt_cases:
+  obtains (Empty) "t = Empty" 
+  | (Red) l k v r where "t = Branch R l k v r" 
+  | (Black) l k v r where "t = Branch B l k v r"
+proof (cases t)
+  case Empty with that show thesis by blast
+next
+  case (Branch c) with that show thesis by (cases c) blast+
+qed
+
+text {* Content of a tree *}
+
+primrec entries
+where 
+  "entries Empty = []"
+| "entries (Branch _ l k v r) = entries l @ (k,v) # entries r"
 
 text {* Search tree properties *}
 
-primrec
-  pin_tree :: "'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> bool"
+primrec entry_in_tree :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) rbt \<Rightarrow> bool"
 where
-  "pin_tree k v Empty = False"
-| "pin_tree k v (Tr c l x y r) = (k = x \<and> v = y \<or> pin_tree k v l \<or> pin_tree k v r)"
+  "entry_in_tree k v Empty = False"
+| "entry_in_tree k v (Branch c l x y r) \<longleftrightarrow> k = x \<and> v = y \<or> entry_in_tree k v l \<or> entry_in_tree k v r"
 
-primrec
-  keys :: "('k,'v) rbt \<Rightarrow> 'k set"
+primrec keys :: "('k, 'v) rbt \<Rightarrow> 'k set"
 where
   "keys Empty = {}"
-| "keys (Tr _ l k _ r) = { k } \<union> keys l \<union> keys r"
+| "keys (Branch _ l k _ r) = { k } \<union> keys l \<union> keys r"
 
-lemma pint_keys: "pin_tree k v t \<Longrightarrow> k \<in> keys t" by (induct t) auto
+lemma entry_in_tree_keys:
+  "entry_in_tree k v t \<Longrightarrow> k \<in> keys t"
+  by (induct t) auto
 
-primrec tlt :: "'a\<Colon>order \<Rightarrow> ('a,'b) rbt \<Rightarrow> bool"
+definition tree_less :: "'a\<Colon>order \<Rightarrow> ('a, 'b) rbt \<Rightarrow> bool"
 where
-  "tlt k Empty = True"
-| "tlt k (Tr c lt kt v rt) = (kt < k \<and> tlt k lt \<and> tlt k rt)"
+  tree_less_prop: "tree_less k t \<longleftrightarrow> (\<forall>x\<in>keys t. x < k)"
+
+abbreviation tree_less_symbol (infix "|\<guillemotleft>" 50)
+where "t |\<guillemotleft> x \<equiv> tree_less x t"
 
-abbreviation tllt (infix "|\<guillemotleft>" 50)
-where "t |\<guillemotleft> x == tlt x t"
+definition tree_greater :: "'a\<Colon>order \<Rightarrow> ('a, 'b) rbt \<Rightarrow> bool" (infix "\<guillemotleft>|" 50) 
+where
+  tree_greater_prop: "tree_greater k t = (\<forall>x\<in>keys t. k < x)"
 
-primrec tgt :: "'a\<Colon>order \<Rightarrow> ('a,'b) rbt \<Rightarrow> bool" (infix "\<guillemotleft>|" 50) 
-where
-  "tgt k Empty = True"
-| "tgt k (Tr c lt kt v rt) = (k < kt \<and> tgt k lt \<and> tgt k rt)"
+lemma tree_less_simps [simp]:
+  "tree_less k Empty = True"
+  "tree_less k (Branch c lt kt v rt) \<longleftrightarrow> kt < k \<and> tree_less k lt \<and> tree_less k rt"
+  by (auto simp add: tree_less_prop)
 
-lemma tlt_prop: "(t |\<guillemotleft> k) = (\<forall>x\<in>keys t. x < k)" by (induct t) auto
-lemma tgt_prop: "(k \<guillemotleft>| t) = (\<forall>x\<in>keys t. k < x)" by (induct t) auto
-lemmas tlgt_props = tlt_prop tgt_prop
+lemma tree_greater_simps [simp]:
+  "tree_greater k Empty = True"
+  "tree_greater k (Branch c lt kt v rt) \<longleftrightarrow> k < kt \<and> tree_greater k lt \<and> tree_greater k rt"
+  by (auto simp add: tree_greater_prop)
 
-lemmas tgt_nit = tgt_prop pint_keys
-lemmas tlt_nit = tlt_prop pint_keys
+lemmas tree_ord_props = tree_less_prop tree_greater_prop
 
-lemma tlt_trans: "\<lbrakk> t |\<guillemotleft> x; x < y \<rbrakk> \<Longrightarrow> t |\<guillemotleft> y"
-  and tgt_trans: "\<lbrakk> x < y; y \<guillemotleft>| t\<rbrakk> \<Longrightarrow> x \<guillemotleft>| t"
-by (auto simp: tlgt_props)
-
+lemmas tree_greater_nit = tree_greater_prop entry_in_tree_keys
+lemmas tree_less_nit = tree_less_prop entry_in_tree_keys
 
-primrec st :: "('a::linorder, 'b) rbt \<Rightarrow> bool"
-where
-  "st Empty = True"
-| "st (Tr c l k v r) = (l |\<guillemotleft> k \<and> k \<guillemotleft>| r \<and> st l \<and> st r)"
+lemma tree_less_trans: "t |\<guillemotleft> x \<Longrightarrow> x < y \<Longrightarrow> t |\<guillemotleft> y"
+  and tree_greater_trans: "x < y \<Longrightarrow> y \<guillemotleft>| t \<Longrightarrow> x \<guillemotleft>| t"
+by (auto simp: tree_ord_props)
 
-primrec map_of :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a \<rightharpoonup> 'b"
+primrec sorted :: "('a::linorder, 'b) rbt \<Rightarrow> bool"
 where
-  "map_of Empty k = None"
-| "map_of (Tr _ l x y r) k = (if k < x then map_of l k else if x < k then map_of r k else Some y)"
+  "sorted Empty = True"
+| "sorted (Branch c l k v r) = (l |\<guillemotleft> k \<and> k \<guillemotleft>| r \<and> sorted l \<and> sorted r)"
 
-lemma map_of_tlt[simp]: "t |\<guillemotleft> k \<Longrightarrow> map_of t k = None" 
+primrec lookup :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a \<rightharpoonup> 'b"
+where
+  "lookup Empty k = None"
+| "lookup (Branch _ l x y r) k = (if k < x then lookup l k else if x < k then lookup r k else Some y)"
+
+lemma lookup_tree_less[simp]: "t |\<guillemotleft> k \<Longrightarrow> lookup t k = None" 
 by (induct t) auto
 
-lemma map_of_tgt[simp]: "k \<guillemotleft>| t \<Longrightarrow> map_of t k = None"
+lemma lookup_tree_greater[simp]: "k \<guillemotleft>| t \<Longrightarrow> lookup t k = None"
 by (induct t) auto
 
-lemma mapof_keys: "st t \<Longrightarrow> dom (map_of t) = keys t"
-by (induct t) (auto simp: dom_def tgt_prop tlt_prop)
+lemma lookup_keys: "sorted t \<Longrightarrow> dom (lookup t) = keys t"
+by (induct t) (auto simp: dom_def tree_greater_prop tree_less_prop)
 
-lemma mapof_pit: "st t \<Longrightarrow> (map_of t k = Some v) = pin_tree k v t"
-by (induct t) (auto simp: tlt_prop tgt_prop pint_keys)
+lemma lookup_pit: "sorted t \<Longrightarrow> (lookup t k = Some v) = entry_in_tree k v t"
+by (induct t) (auto simp: tree_less_prop tree_greater_prop entry_in_tree_keys)
 
-lemma map_of_Empty: "map_of Empty = empty"
+lemma lookup_Empty: "lookup Empty = empty"
 by (rule ext) simp
 
 (* a kind of extensionality *)
-lemma mapof_from_pit: 
-  assumes st: "st t1" "st t2" 
-  and eq: "\<And>v. pin_tree (k\<Colon>'a\<Colon>linorder) v t1 = pin_tree k v t2" 
-  shows "map_of t1 k = map_of t2 k"
-proof (cases "map_of t1 k")
+lemma lookup_from_pit: 
+  assumes sorted: "sorted t1" "sorted t2" 
+  and eq: "\<And>v. entry_in_tree (k\<Colon>'a\<Colon>linorder) v t1 = entry_in_tree k v t2" 
+  shows "lookup t1 k = lookup t2 k"
+proof (cases "lookup t1 k")
   case None
-  then have "\<And>v. \<not> pin_tree k v t1"
-    by (simp add: mapof_pit[symmetric] st)
+  then have "\<And>v. \<not> entry_in_tree k v t1"
+    by (simp add: lookup_pit[symmetric] sorted)
   with None show ?thesis
-    by (cases "map_of t2 k") (auto simp: mapof_pit st eq)
+    by (cases "lookup t2 k") (auto simp: lookup_pit sorted eq)
 next
   case (Some a)
   then show ?thesis
-    apply (cases "map_of t2 k")
-    apply (auto simp: mapof_pit st eq)
-    by (auto simp add: mapof_pit[symmetric] st Some)
+    apply (cases "lookup t2 k")
+    apply (auto simp: lookup_pit sorted eq)
+    by (auto simp add: lookup_pit[symmetric] sorted Some)
 qed
 
 subsection {* Red-black properties *}
 
-primrec treec :: "('a,'b) rbt \<Rightarrow> color"
+primrec color_of :: "('a, 'b) rbt \<Rightarrow> color"
 where
-  "treec Empty = B"
-| "treec (Tr c _ _ _ _) = c"
+  "color_of Empty = B"
+| "color_of (Branch c _ _ _ _) = c"
 
-primrec inv1 :: "('a,'b) rbt \<Rightarrow> bool"
+primrec bheight :: "('a,'b) rbt \<Rightarrow> nat"
+where
+  "bheight Empty = 0"
+| "bheight (Branch c lt k v rt) = (if c = B then Suc (bheight lt) else bheight lt)"
+
+primrec inv1 :: "('a, 'b) rbt \<Rightarrow> bool"
 where
   "inv1 Empty = True"
-| "inv1 (Tr c lt k v rt) = (inv1 lt \<and> inv1 rt \<and> (c = B \<or> treec lt = B \<and> treec rt = B))"
+| "inv1 (Branch c lt k v rt) \<longleftrightarrow> inv1 lt \<and> inv1 rt \<and> (c = B \<or> color_of lt = B \<and> color_of rt = B)"
 
-(* Weaker version *)
-primrec inv1l :: "('a,'b) rbt \<Rightarrow> bool"
+primrec inv1l :: "('a, 'b) rbt \<Rightarrow> bool" -- {* Weaker version *}
 where
   "inv1l Empty = True"
-| "inv1l (Tr c l k v r) = (inv1 l \<and> inv1 r)"
+| "inv1l (Branch c l k v r) = (inv1 l \<and> inv1 r)"
 lemma [simp]: "inv1 t \<Longrightarrow> inv1l t" by (cases t) simp+
 
-primrec bh :: "('a,'b) rbt \<Rightarrow> nat"
-where
-  "bh Empty = 0"
-| "bh (Tr c lt k v rt) = (if c = B then Suc (bh lt) else bh lt)"
-
-primrec inv2 :: "('a,'b) rbt \<Rightarrow> bool"
+primrec inv2 :: "('a, 'b) rbt \<Rightarrow> bool"
 where
   "inv2 Empty = True"
-| "inv2 (Tr c lt k v rt) = (inv2 lt \<and> inv2 rt \<and> bh lt = bh rt)"
+| "inv2 (Branch c lt k v rt) = (inv2 lt \<and> inv2 rt \<and> bheight lt = bheight rt)"
 
-definition
-  "isrbt t = (inv1 t \<and> inv2 t \<and> treec t = B \<and> st t)"
-
-lemma isrbt_st[simp]: "isrbt t \<Longrightarrow> st t" by (simp add: isrbt_def)
+definition is_rbt :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> bool" where
+  "is_rbt t \<longleftrightarrow> inv1 t \<and> inv2 t \<and> color_of t = B \<and> sorted t"
 
-lemma rbt_cases:
-  obtains (Empty) "t = Empty" 
-  | (Red) l k v r where "t = Tr R l k v r" 
-  | (Black) l k v r where "t = Tr B l k v r" 
-by (cases t, simp) (case_tac "color", auto)
+lemma is_rbt_sorted [simp]:
+  "is_rbt t \<Longrightarrow> sorted t" by (simp add: is_rbt_def)
 
-theorem Empty_isrbt[simp]: "isrbt Empty"
-unfolding isrbt_def by simp
+theorem Empty_is_rbt [simp]:
+  "is_rbt Empty" by (simp add: is_rbt_def)
 
 
 subsection {* Insertion *}
@@ -147,80 +163,80 @@
 fun (* slow, due to massive case splitting *)
   balance :: "('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
 where
-  "balance (Tr R a w x b) s t (Tr R c y z d) = Tr R (Tr B a w x b) s t (Tr B c y z d)" |
-  "balance (Tr R (Tr R a w x b) s t c) y z d = Tr R (Tr B a w x b) s t (Tr B c y z d)" |
-  "balance (Tr R a w x (Tr R b s t c)) y z d = Tr R (Tr B a w x b) s t (Tr B c y z d)" |
-  "balance a w x (Tr R b s t (Tr R c y z d)) = Tr R (Tr B a w x b) s t (Tr B c y z d)" |
-  "balance a w x (Tr R (Tr R b s t c) y z d) = Tr R (Tr B a w x b) s t (Tr B c y z d)" |
-  "balance a s t b = Tr B a s t b"
+  "balance (Branch R a w x b) s t (Branch R c y z d) = Branch R (Branch B a w x b) s t (Branch B c y z d)" |
+  "balance (Branch R (Branch R a w x b) s t c) y z d = Branch R (Branch B a w x b) s t (Branch B c y z d)" |
+  "balance (Branch R a w x (Branch R b s t c)) y z d = Branch R (Branch B a w x b) s t (Branch B c y z d)" |
+  "balance a w x (Branch R b s t (Branch R c y z d)) = Branch R (Branch B a w x b) s t (Branch B c y z d)" |
+  "balance a w x (Branch R (Branch R b s t c) y z d) = Branch R (Branch B a w x b) s t (Branch B c y z d)" |
+  "balance a s t b = Branch B a s t b"
 
 lemma balance_inv1: "\<lbrakk>inv1l l; inv1l r\<rbrakk> \<Longrightarrow> inv1 (balance l k v r)" 
   by (induct l k v r rule: balance.induct) auto
 
-lemma balance_bh: "bh l = bh r \<Longrightarrow> bh (balance l k v r) = Suc (bh l)"
+lemma balance_bheight: "bheight l = bheight r \<Longrightarrow> bheight (balance l k v r) = Suc (bheight l)"
   by (induct l k v r rule: balance.induct) auto
 
 lemma balance_inv2: 
-  assumes "inv2 l" "inv2 r" "bh l = bh r"
+  assumes "inv2 l" "inv2 r" "bheight l = bheight r"
   shows "inv2 (balance l k v r)"
   using assms
   by (induct l k v r rule: balance.induct) auto
 
-lemma balance_tgt[simp]: "(v \<guillemotleft>| balance a k x b) = (v \<guillemotleft>| a \<and> v \<guillemotleft>| b \<and> v < k)" 
+lemma balance_tree_greater[simp]: "(v \<guillemotleft>| balance a k x b) = (v \<guillemotleft>| a \<and> v \<guillemotleft>| b \<and> v < k)" 
   by (induct a k x b rule: balance.induct) auto
 
-lemma balance_tlt[simp]: "(balance a k x b |\<guillemotleft> v) = (a |\<guillemotleft> v \<and> b |\<guillemotleft> v \<and> k < v)"
+lemma balance_tree_less[simp]: "(balance a k x b |\<guillemotleft> v) = (a |\<guillemotleft> v \<and> b |\<guillemotleft> v \<and> k < v)"
   by (induct a k x b rule: balance.induct) auto
 
-lemma balance_st: 
+lemma balance_sorted: 
   fixes k :: "'a::linorder"
-  assumes "st l" "st r" "l |\<guillemotleft> k" "k \<guillemotleft>| r"
-  shows "st (balance l k v r)"
+  assumes "sorted l" "sorted r" "l |\<guillemotleft> k" "k \<guillemotleft>| r"
+  shows "sorted (balance l k v r)"
 using assms proof (induct l k v r rule: balance.induct)
   case ("2_2" a x w b y t c z s va vb vd vc)
-  hence "y < z \<and> z \<guillemotleft>| Tr B va vb vd vc" 
-    by (auto simp add: tlgt_props)
-  hence "tgt y (Tr B va vb vd vc)" by (blast dest: tgt_trans)
+  hence "y < z \<and> z \<guillemotleft>| Branch B va vb vd vc" 
+    by (auto simp add: tree_ord_props)
+  hence "tree_greater y (Branch B va vb vd vc)" by (blast dest: tree_greater_trans)
   with "2_2" show ?case by simp
 next
   case ("3_2" va vb vd vc x w b y s c z)
-  from "3_2" have "x < y \<and> tlt x (Tr B va vb vd vc)" 
-    by (simp add: tlt.simps tgt.simps)
-  hence "tlt y (Tr B va vb vd vc)" by (blast dest: tlt_trans)
+  from "3_2" have "x < y \<and> tree_less x (Branch B va vb vd vc)" 
+    by simp
+  hence "tree_less y (Branch B va vb vd vc)" by (blast dest: tree_less_trans)
   with "3_2" show ?case by simp
 next
   case ("3_3" x w b y s c z t va vb vd vc)
-  from "3_3" have "y < z \<and> tgt z (Tr B va vb vd vc)" by simp
-  hence "tgt y (Tr B va vb vd vc)" by (blast dest: tgt_trans)
+  from "3_3" have "y < z \<and> tree_greater z (Branch B va vb vd vc)" by simp
+  hence "tree_greater y (Branch B va vb vd vc)" by (blast dest: tree_greater_trans)
   with "3_3" show ?case by simp
 next
   case ("3_4" vd ve vg vf x w b y s c z t va vb vii vc)
-  hence "x < y \<and> tlt x (Tr B vd ve vg vf)" by simp
-  hence 1: "tlt y (Tr B vd ve vg vf)" by (blast dest: tlt_trans)
-  from "3_4" have "y < z \<and> tgt z (Tr B va vb vii vc)" by simp
-  hence "tgt y (Tr B va vb vii vc)" by (blast dest: tgt_trans)
+  hence "x < y \<and> tree_less x (Branch B vd ve vg vf)" by simp
+  hence 1: "tree_less y (Branch B vd ve vg vf)" by (blast dest: tree_less_trans)
+  from "3_4" have "y < z \<and> tree_greater z (Branch B va vb vii vc)" by simp
+  hence "tree_greater y (Branch B va vb vii vc)" by (blast dest: tree_greater_trans)
   with 1 "3_4" show ?case by simp
 next
   case ("4_2" va vb vd vc x w b y s c z t dd)
-  hence "x < y \<and> tlt x (Tr B va vb vd vc)" by simp
-  hence "tlt y (Tr B va vb vd vc)" by (blast dest: tlt_trans)
+  hence "x < y \<and> tree_less x (Branch B va vb vd vc)" by simp
+  hence "tree_less y (Branch B va vb vd vc)" by (blast dest: tree_less_trans)
   with "4_2" show ?case by simp
 next
   case ("5_2" x w b y s c z t va vb vd vc)
-  hence "y < z \<and> tgt z (Tr B va vb vd vc)" by simp
-  hence "tgt y (Tr B va vb vd vc)" by (blast dest: tgt_trans)
+  hence "y < z \<and> tree_greater z (Branch B va vb vd vc)" by simp
+  hence "tree_greater y (Branch B va vb vd vc)" by (blast dest: tree_greater_trans)
   with "5_2" show ?case by simp
 next
   case ("5_3" va vb vd vc x w b y s c z t)
-  hence "x < y \<and> tlt x (Tr B va vb vd vc)" by simp
-  hence "tlt y (Tr B va vb vd vc)" by (blast dest: tlt_trans)
+  hence "x < y \<and> tree_less x (Branch B va vb vd vc)" by simp
+  hence "tree_less y (Branch B va vb vd vc)" by (blast dest: tree_less_trans)
   with "5_3" show ?case by simp
 next
   case ("5_4" va vb vg vc x w b y s c z t vd ve vii vf)
-  hence "x < y \<and> tlt x (Tr B va vb vg vc)" by simp
-  hence 1: "tlt y (Tr B va vb vg vc)" by (blast dest: tlt_trans)
-  from "5_4" have "y < z \<and> tgt z (Tr B vd ve vii vf)" by simp
-  hence "tgt y (Tr B vd ve vii vf)" by (blast dest: tgt_trans)
+  hence "x < y \<and> tree_less x (Branch B va vb vg vc)" by simp
+  hence 1: "tree_less y (Branch B va vb vg vc)" by (blast dest: tree_less_trans)
+  from "5_4" have "y < z \<and> tree_greater z (Branch B vd ve vii vf)" by simp
+  hence "tree_greater y (Branch B vd ve vii vf)" by (blast dest: tree_greater_trans)
   with 1 "5_4" show ?case by simp
 qed simp+
 
@@ -229,62 +245,62 @@
 by (induct l k v r rule: balance.induct) auto
 
 lemma balance_pit:  
-  "pin_tree k x (balance l v y r) = (pin_tree k x l \<or> k = v \<and> x = y \<or> pin_tree k x r)" 
+  "entry_in_tree k x (balance l v y r) = (entry_in_tree k x l \<or> k = v \<and> x = y \<or> entry_in_tree k x r)" 
 by (induct l v y r rule: balance.induct) auto
 
-lemma map_of_balance[simp]: 
+lemma lookup_balance[simp]: 
 fixes k :: "'a::linorder"
-assumes "st l" "st r" "l |\<guillemotleft> k" "k \<guillemotleft>| r"
-shows "map_of (balance l k v r) x = map_of (Tr B l k v r) x"
-by (rule mapof_from_pit) (auto simp:assms balance_pit balance_st)
+assumes "sorted l" "sorted r" "l |\<guillemotleft> k" "k \<guillemotleft>| r"
+shows "lookup (balance l k v r) x = lookup (Branch B l k v r) x"
+by (rule lookup_from_pit) (auto simp:assms balance_pit balance_sorted)
 
 primrec paint :: "color \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
 where
   "paint c Empty = Empty"
-| "paint c (Tr _ l k v r) = Tr c l k v r"
+| "paint c (Branch _ l k v r) = Branch c l k v r"
 
 lemma paint_inv1l[simp]: "inv1l t \<Longrightarrow> inv1l (paint c t)" by (cases t) auto
 lemma paint_inv1[simp]: "inv1l t \<Longrightarrow> inv1 (paint B t)" by (cases t) auto
 lemma paint_inv2[simp]: "inv2 t \<Longrightarrow> inv2 (paint c t)" by (cases t) auto
-lemma paint_treec[simp]: "treec (paint B t) = B" by (cases t) auto
-lemma paint_st[simp]: "st t \<Longrightarrow> st (paint c t)" by (cases t) auto
-lemma paint_pit[simp]: "pin_tree k x (paint c t) = pin_tree k x t" by (cases t) auto
-lemma paint_mapof[simp]: "map_of (paint c t) = map_of t" by (rule ext) (cases t, auto)
-lemma paint_tgt[simp]: "(v \<guillemotleft>| paint c t) = (v \<guillemotleft>| t)" by (cases t) auto
-lemma paint_tlt[simp]: "(paint c t |\<guillemotleft> v) = (t |\<guillemotleft> v)" by (cases t) auto
+lemma paint_color_of[simp]: "color_of (paint B t) = B" by (cases t) auto
+lemma paint_sorted[simp]: "sorted t \<Longrightarrow> sorted (paint c t)" by (cases t) auto
+lemma paint_pit[simp]: "entry_in_tree k x (paint c t) = entry_in_tree k x t" by (cases t) auto
+lemma paint_lookup[simp]: "lookup (paint c t) = lookup t" by (rule ext) (cases t, auto)
+lemma paint_tree_greater[simp]: "(v \<guillemotleft>| paint c t) = (v \<guillemotleft>| t)" by (cases t) auto
+lemma paint_tree_less[simp]: "(paint c t |\<guillemotleft> v) = (t |\<guillemotleft> v)" by (cases t) auto
 
 fun
   ins :: "('a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
 where
-  "ins f k v Empty = Tr R Empty k v Empty" |
-  "ins f k v (Tr B l x y r) = (if k < x then balance (ins f k v l) x y r
+  "ins f k v Empty = Branch R Empty k v Empty" |
+  "ins f k v (Branch B l x y r) = (if k < x then balance (ins f k v l) x y r
                                else if k > x then balance l x y (ins f k v r)
-                               else Tr B l x (f k y v) r)" |
-  "ins f k v (Tr R l x y r) = (if k < x then Tr R (ins f k v l) x y r
-                               else if k > x then Tr R l x y (ins f k v r)
-                               else Tr R l x (f k y v) r)"
+                               else Branch B l x (f k y v) r)" |
+  "ins f k v (Branch R l x y r) = (if k < x then Branch R (ins f k v l) x y r
+                               else if k > x then Branch R l x y (ins f k v r)
+                               else Branch R l x (f k y v) r)"
 
 lemma ins_inv1_inv2: 
   assumes "inv1 t" "inv2 t"
-  shows "inv2 (ins f k x t)" "bh (ins f k x t) = bh t" 
-  "treec t = B \<Longrightarrow> inv1 (ins f k x t)" "inv1l (ins f k x t)"
+  shows "inv2 (ins f k x t)" "bheight (ins f k x t) = bheight t" 
+  "color_of t = B \<Longrightarrow> inv1 (ins f k x t)" "inv1l (ins f k x t)"
   using assms
-  by (induct f k x t rule: ins.induct) (auto simp: balance_inv1 balance_inv2 balance_bh)
+  by (induct f k x t rule: ins.induct) (auto simp: balance_inv1 balance_inv2 balance_bheight)
 
-lemma ins_tgt[simp]: "(v \<guillemotleft>| ins f k x t) = (v \<guillemotleft>| t \<and> k > v)"
+lemma ins_tree_greater[simp]: "(v \<guillemotleft>| ins f k x t) = (v \<guillemotleft>| t \<and> k > v)"
   by (induct f k x t rule: ins.induct) auto
-lemma ins_tlt[simp]: "(ins f k x t |\<guillemotleft> v) = (t |\<guillemotleft> v \<and> k < v)"
+lemma ins_tree_less[simp]: "(ins f k x t |\<guillemotleft> v) = (t |\<guillemotleft> v \<and> k < v)"
   by (induct f k x t rule: ins.induct) auto
-lemma ins_st[simp]: "st t \<Longrightarrow> st (ins f k x t)"
-  by (induct f k x t rule: ins.induct) (auto simp: balance_st)
+lemma ins_sorted[simp]: "sorted t \<Longrightarrow> sorted (ins f k x t)"
+  by (induct f k x t rule: ins.induct) (auto simp: balance_sorted)
 
 lemma keys_ins: "keys (ins f k v t) = { k } \<union> keys t"
 by (induct f k v t rule: ins.induct) auto
 
-lemma map_of_ins: 
+lemma lookup_ins: 
   fixes k :: "'a::linorder"
-  assumes "st t"
-  shows "map_of (ins f k v t) x = ((map_of t)(k |-> case map_of t k of None \<Rightarrow> v 
+  assumes "sorted t"
+  shows "lookup (ins f k v t) x = ((lookup t)(k |-> case lookup t k of None \<Rightarrow> v 
                                                        | Some w \<Rightarrow> f k w v)) x"
 using assms by (induct f k v t rule: ins.induct) auto
 
@@ -293,98 +309,97 @@
 where
   "insertwithkey f k v t = paint B (ins f k v t)"
 
-lemma insertwk_st: "st t \<Longrightarrow> st (insertwithkey f k x t)"
+lemma insertwk_sorted: "sorted t \<Longrightarrow> sorted (insertwithkey f k x t)"
   by (auto simp: insertwithkey_def)
 
-theorem insertwk_isrbt: 
-  assumes inv: "isrbt t" 
-  shows "isrbt (insertwithkey f k x t)"
+theorem insertwk_is_rbt: 
+  assumes inv: "is_rbt t" 
+  shows "is_rbt (insertwithkey f k x t)"
 using assms
-unfolding insertwithkey_def isrbt_def
+unfolding insertwithkey_def is_rbt_def
 by (auto simp: ins_inv1_inv2)
 
-lemma map_of_insertwk: 
-  assumes "st t"
-  shows "map_of (insertwithkey f k v t) x = ((map_of t)(k |-> case map_of t k of None \<Rightarrow> v 
+lemma lookup_insertwk: 
+  assumes "sorted t"
+  shows "lookup (insertwithkey f k v t) x = ((lookup t)(k |-> case lookup t k of None \<Rightarrow> v 
                                                        | Some w \<Rightarrow> f k w v)) x"
 unfolding insertwithkey_def using assms
-by (simp add:map_of_ins)
+by (simp add:lookup_ins)
 
 definition
   insertw_def: "insertwith f = insertwithkey (\<lambda>_. f)"
 
-lemma insertw_st: "st t \<Longrightarrow> st (insertwith f k v t)" by (simp add: insertwk_st insertw_def)
-theorem insertw_isrbt: "isrbt t \<Longrightarrow> isrbt (insertwith f k v t)" by (simp add: insertwk_isrbt insertw_def)
+lemma insertw_sorted: "sorted t \<Longrightarrow> sorted (insertwith f k v t)" by (simp add: insertwk_sorted insertw_def)
+theorem insertw_is_rbt: "is_rbt t \<Longrightarrow> is_rbt (insertwith f k v t)" by (simp add: insertwk_is_rbt insertw_def)
 
-lemma map_of_insertw:
-  assumes "isrbt t"
-  shows "map_of (insertwith f k v t) = (map_of t)(k \<mapsto> (if k:dom (map_of t) then f (the (map_of t k)) v else v))"
+lemma lookup_insertw:
+  assumes "is_rbt t"
+  shows "lookup (insertwith f k v t) = (lookup t)(k \<mapsto> (if k:dom (lookup t) then f (the (lookup t k)) v else v))"
 using assms
 unfolding insertw_def
-by (rule_tac ext) (cases "map_of t k", auto simp:map_of_insertwk dom_def)
-
+by (rule_tac ext) (cases "lookup t k", auto simp:lookup_insertwk dom_def)
 
-definition
-  "insrt k v t = insertwithkey (\<lambda>_ _ nv. nv) k v t"
+definition insert :: "'a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" where
+  "insert k v t = insertwithkey (\<lambda>_ _ nv. nv) k v t"
 
-lemma insrt_st: "st t \<Longrightarrow> st (insrt k v t)" by (simp add: insertwk_st insrt_def)
-theorem insrt_isrbt: "isrbt t \<Longrightarrow> isrbt (insrt k v t)" by (simp add: insertwk_isrbt insrt_def)
+lemma insert_sorted: "sorted t \<Longrightarrow> sorted (insert k v t)" by (simp add: insertwk_sorted insert_def)
+theorem insert_is_rbt: "is_rbt t \<Longrightarrow> is_rbt (insert k v t)" by (simp add: insertwk_is_rbt insert_def)
 
-lemma map_of_insert: 
-  assumes "isrbt t"
-  shows "map_of (insrt k v t) = (map_of t)(k\<mapsto>v)"
-unfolding insrt_def
+lemma lookup_insert: 
+  assumes "is_rbt t"
+  shows "lookup (insert k v t) = (lookup t)(k\<mapsto>v)"
+unfolding insert_def
 using assms
-by (rule_tac ext) (simp add: map_of_insertwk split:option.split)
+by (rule_tac ext) (simp add: lookup_insertwk split:option.split)
 
 
 subsection {* Deletion *}
 
-lemma bh_paintR'[simp]: "treec t = B \<Longrightarrow> bh (paint R t) = bh t - 1"
+lemma bheight_paintR'[simp]: "color_of t = B \<Longrightarrow> bheight (paint R t) = bheight t - 1"
 by (cases t rule: rbt_cases) auto
 
 fun
   balleft :: "('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
 where
-  "balleft (Tr R a k x b) s y c = Tr R (Tr B a k x b) s y c" |
-  "balleft bl k x (Tr B a s y b) = balance bl k x (Tr R a s y b)" |
-  "balleft bl k x (Tr R (Tr B a s y b) t z c) = Tr R (Tr B bl k x a) s y (balance b t z (paint R c))" |
+  "balleft (Branch R a k x b) s y c = Branch R (Branch B a k x b) s y c" |
+  "balleft bl k x (Branch B a s y b) = balance bl k x (Branch R a s y b)" |
+  "balleft bl k x (Branch R (Branch B a s y b) t z c) = Branch R (Branch B bl k x a) s y (balance b t z (paint R c))" |
   "balleft t k x s = Empty"
 
 lemma balleft_inv2_with_inv1:
-  assumes "inv2 lt" "inv2 rt" "bh lt + 1 = bh rt" "inv1 rt"
-  shows "bh (balleft lt k v rt) = bh lt + 1"
+  assumes "inv2 lt" "inv2 rt" "bheight lt + 1 = bheight rt" "inv1 rt"
+  shows "bheight (balleft lt k v rt) = bheight lt + 1"
   and   "inv2 (balleft lt k v rt)"
 using assms 
-by (induct lt k v rt rule: balleft.induct) (auto simp: balance_inv2 balance_bh)
+by (induct lt k v rt rule: balleft.induct) (auto simp: balance_inv2 balance_bheight)
 
 lemma balleft_inv2_app: 
-  assumes "inv2 lt" "inv2 rt" "bh lt + 1 = bh rt" "treec rt = B"
+  assumes "inv2 lt" "inv2 rt" "bheight lt + 1 = bheight rt" "color_of rt = B"
   shows "inv2 (balleft lt k v rt)" 
-        "bh (balleft lt k v rt) = bh rt"
+        "bheight (balleft lt k v rt) = bheight rt"
 using assms 
-by (induct lt k v rt rule: balleft.induct) (auto simp add: balance_inv2 balance_bh)+ 
+by (induct lt k v rt rule: balleft.induct) (auto simp add: balance_inv2 balance_bheight)+ 
 
-lemma balleft_inv1: "\<lbrakk>inv1l a; inv1 b; treec b = B\<rbrakk> \<Longrightarrow> inv1 (balleft a k x b)"
+lemma balleft_inv1: "\<lbrakk>inv1l a; inv1 b; color_of b = B\<rbrakk> \<Longrightarrow> inv1 (balleft a k x b)"
   by (induct a k x b rule: balleft.induct) (simp add: balance_inv1)+
 
 lemma balleft_inv1l: "\<lbrakk> inv1l lt; inv1 rt \<rbrakk> \<Longrightarrow> inv1l (balleft lt k x rt)"
 by (induct lt k x rt rule: balleft.induct) (auto simp: balance_inv1)
 
-lemma balleft_st: "\<lbrakk> st l; st r; tlt k l; tgt k r \<rbrakk> \<Longrightarrow> st (balleft l k v r)"
+lemma balleft_sorted: "\<lbrakk> sorted l; sorted r; tree_less k l; tree_greater k r \<rbrakk> \<Longrightarrow> sorted (balleft l k v r)"
 apply (induct l k v r rule: balleft.induct)
-apply (auto simp: balance_st)
-apply (unfold tgt_prop tlt_prop)
+apply (auto simp: balance_sorted)
+apply (unfold tree_greater_prop tree_less_prop)
 by force+
 
-lemma balleft_tgt: 
+lemma balleft_tree_greater: 
   fixes k :: "'a::order"
   assumes "k \<guillemotleft>| a" "k \<guillemotleft>| b" "k < x" 
   shows "k \<guillemotleft>| balleft a x t b"
 using assms 
 by (induct a x t b rule: balleft.induct) auto
 
-lemma balleft_tlt: 
+lemma balleft_tree_less: 
   fixes k :: "'a::order"
   assumes "a |\<guillemotleft> k" "b |\<guillemotleft> k" "x < k" 
   shows "balleft a x t b |\<guillemotleft> k"
@@ -392,52 +407,52 @@
 by (induct a x t b rule: balleft.induct) auto
 
 lemma balleft_pit: 
-  assumes "inv1l l" "inv1 r" "bh l + 1 = bh r"
-  shows "pin_tree k v (balleft l a b r) = (pin_tree k v l \<or> k = a \<and> v = b \<or> pin_tree k v r)"
+  assumes "inv1l l" "inv1 r" "bheight l + 1 = bheight r"
+  shows "entry_in_tree k v (balleft l a b r) = (entry_in_tree k v l \<or> k = a \<and> v = b \<or> entry_in_tree k v r)"
 using assms 
 by (induct l k v r rule: balleft.induct) (auto simp: balance_pit)
 
 fun
   balright :: "('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
 where
-  "balright a k x (Tr R b s y c) = Tr R a k x (Tr B b s y c)" |
-  "balright (Tr B a k x b) s y bl = balance (Tr R a k x b) s y bl" |
-  "balright (Tr R a k x (Tr B b s y c)) t z bl = Tr R (balance (paint R a) k x b) s y (Tr B c t z bl)" |
+  "balright a k x (Branch R b s y c) = Branch R a k x (Branch B b s y c)" |
+  "balright (Branch B a k x b) s y bl = balance (Branch R a k x b) s y bl" |
+  "balright (Branch R a k x (Branch B b s y c)) t z bl = Branch R (balance (paint R a) k x b) s y (Branch B c t z bl)" |
   "balright t k x s = Empty"
 
 lemma balright_inv2_with_inv1:
-  assumes "inv2 lt" "inv2 rt" "bh lt = bh rt + 1" "inv1 lt"
-  shows "inv2 (balright lt k v rt) \<and> bh (balright lt k v rt) = bh lt"
+  assumes "inv2 lt" "inv2 rt" "bheight lt = bheight rt + 1" "inv1 lt"
+  shows "inv2 (balright lt k v rt) \<and> bheight (balright lt k v rt) = bheight lt"
 using assms
-by (induct lt k v rt rule: balright.induct) (auto simp: balance_inv2 balance_bh)
+by (induct lt k v rt rule: balright.induct) (auto simp: balance_inv2 balance_bheight)
 
-lemma balright_inv1: "\<lbrakk>inv1 a; inv1l b; treec a = B\<rbrakk> \<Longrightarrow> inv1 (balright a k x b)"
+lemma balright_inv1: "\<lbrakk>inv1 a; inv1l b; color_of a = B\<rbrakk> \<Longrightarrow> inv1 (balright a k x b)"
 by (induct a k x b rule: balright.induct) (simp add: balance_inv1)+
 
 lemma balright_inv1l: "\<lbrakk> inv1 lt; inv1l rt \<rbrakk> \<Longrightarrow>inv1l (balright lt k x rt)"
 by (induct lt k x rt rule: balright.induct) (auto simp: balance_inv1)
 
-lemma balright_st: "\<lbrakk> st l; st r; tlt k l; tgt k r \<rbrakk> \<Longrightarrow> st (balright l k v r)"
+lemma balright_sorted: "\<lbrakk> sorted l; sorted r; tree_less k l; tree_greater k r \<rbrakk> \<Longrightarrow> sorted (balright l k v r)"
 apply (induct l k v r rule: balright.induct)
-apply (auto simp:balance_st)
-apply (unfold tlt_prop tgt_prop)
+apply (auto simp:balance_sorted)
+apply (unfold tree_less_prop tree_greater_prop)
 by force+
 
-lemma balright_tgt: 
+lemma balright_tree_greater: 
   fixes k :: "'a::order"
   assumes "k \<guillemotleft>| a" "k \<guillemotleft>| b" "k < x" 
   shows "k \<guillemotleft>| balright a x t b"
 using assms by (induct a x t b rule: balright.induct) auto
 
-lemma balright_tlt: 
+lemma balright_tree_less: 
   fixes k :: "'a::order"
   assumes "a |\<guillemotleft> k" "b |\<guillemotleft> k" "x < k" 
   shows "balright a x t b |\<guillemotleft> k"
 using assms by (induct a x t b rule: balright.induct) auto
 
 lemma balright_pit:
-  assumes "inv1 l" "inv1l r" "bh l = bh r + 1" "inv2 l" "inv2 r"
-  shows "pin_tree x y (balright l k v r) = (pin_tree x y l \<or> x = k \<and> y = v \<or> pin_tree x y r)"
+  assumes "inv1 l" "inv1l r" "bheight l = bheight r + 1" "inv2 l" "inv2 r"
+  shows "entry_in_tree x y (balright l k v r) = (entry_in_tree x y l \<or> x = k \<and> y = v \<or> entry_in_tree x y r)"
 using assms by (induct l k v r rule: balright.induct) (auto simp: balance_pit)
 
 
@@ -448,50 +463,50 @@
 where
   "app Empty x = x" 
 | "app x Empty = x" 
-| "app (Tr R a k x b) (Tr R c s y d) = (case (app b c) of
-                                      Tr R b2 t z c2 \<Rightarrow> (Tr R (Tr R a k x b2) t z (Tr R c2 s y d)) |
-                                      bc \<Rightarrow> Tr R a k x (Tr R bc s y d))" 
-| "app (Tr B a k x b) (Tr B c s y d) = (case (app b c) of
-                                      Tr R b2 t z c2 \<Rightarrow> Tr R (Tr B a k x b2) t z (Tr B c2 s y d) |
-                                      bc \<Rightarrow> balleft a k x (Tr B bc s y d))" 
-| "app a (Tr R b k x c) = Tr R (app a b) k x c" 
-| "app (Tr R a k x b) c = Tr R a k x (app b c)" 
+| "app (Branch R a k x b) (Branch R c s y d) = (case (app b c) of
+                                      Branch R b2 t z c2 \<Rightarrow> (Branch R (Branch R a k x b2) t z (Branch R c2 s y d)) |
+                                      bc \<Rightarrow> Branch R a k x (Branch R bc s y d))" 
+| "app (Branch B a k x b) (Branch B c s y d) = (case (app b c) of
+                                      Branch R b2 t z c2 \<Rightarrow> Branch R (Branch B a k x b2) t z (Branch B c2 s y d) |
+                                      bc \<Rightarrow> balleft a k x (Branch B bc s y d))" 
+| "app a (Branch R b k x c) = Branch R (app a b) k x c" 
+| "app (Branch R a k x b) c = Branch R a k x (app b c)" 
 
 lemma app_inv2:
-  assumes "inv2 lt" "inv2 rt" "bh lt = bh rt"
-  shows "bh (app lt rt) = bh lt" "inv2 (app lt rt)"
+  assumes "inv2 lt" "inv2 rt" "bheight lt = bheight rt"
+  shows "bheight (app lt rt) = bheight lt" "inv2 (app lt rt)"
 using assms 
 by (induct lt rt rule: app.induct) 
    (auto simp: balleft_inv2_app split: rbt.splits color.splits)
 
 lemma app_inv1: 
   assumes "inv1 lt" "inv1 rt"
-  shows "treec lt = B \<Longrightarrow> treec rt = B \<Longrightarrow> inv1 (app lt rt)"
+  shows "color_of lt = B \<Longrightarrow> color_of rt = B \<Longrightarrow> inv1 (app lt rt)"
          "inv1l (app lt rt)"
 using assms 
 by (induct lt rt rule: app.induct)
    (auto simp: balleft_inv1 split: rbt.splits color.splits)
 
-lemma app_tgt[simp]: 
+lemma app_tree_greater[simp]: 
   fixes k :: "'a::linorder"
   assumes "k \<guillemotleft>| l" "k \<guillemotleft>| r" 
   shows "k \<guillemotleft>| app l r"
 using assms 
 by (induct l r rule: app.induct)
-   (auto simp: balleft_tgt split:rbt.splits color.splits)
+   (auto simp: balleft_tree_greater split:rbt.splits color.splits)
 
-lemma app_tlt[simp]: 
+lemma app_tree_less[simp]: 
   fixes k :: "'a::linorder"
   assumes "l |\<guillemotleft> k" "r |\<guillemotleft> k" 
   shows "app l r |\<guillemotleft> k"
 using assms 
 by (induct l r rule: app.induct)
-   (auto simp: balleft_tlt split:rbt.splits color.splits)
+   (auto simp: balleft_tree_less split:rbt.splits color.splits)
 
-lemma app_st: 
+lemma app_sorted: 
   fixes k :: "'a::linorder"
-  assumes "st l" "st r" "l |\<guillemotleft> k" "k \<guillemotleft>| r"
-  shows "st (app l r)"
+  assumes "sorted l" "sorted r" "l |\<guillemotleft> k" "k \<guillemotleft>| r"
+  shows "sorted (app l r)"
 using assms proof (induct l r rule: app.induct)
   case (3 a x v b c y w d)
   hence ineqs: "a |\<guillemotleft> x" "x \<guillemotleft>| b" "b |\<guillemotleft> k" "k \<guillemotleft>| c" "c |\<guillemotleft> y" "y \<guillemotleft>| d"
@@ -500,55 +515,55 @@
   show ?case
     apply (cases "app b c" rule: rbt_cases)
     apply auto
-    by (metis app_tgt app_tlt ineqs ineqs tlt.simps(2) tgt.simps(2) tgt_trans tlt_trans)+
+    by (metis app_tree_greater app_tree_less ineqs ineqs tree_less_simps(2) tree_greater_simps(2) tree_greater_trans tree_less_trans)+
 next
   case (4 a x v b c y w d)
-  hence "x < k \<and> tgt k c" by simp
-  hence "tgt x c" by (blast dest: tgt_trans)
-  with 4 have 2: "tgt x (app b c)" by (simp add: app_tgt)
-  from 4 have "k < y \<and> tlt k b" by simp
-  hence "tlt y b" by (blast dest: tlt_trans)
-  with 4 have 3: "tlt y (app b c)" by (simp add: app_tlt)
+  hence "x < k \<and> tree_greater k c" by simp
+  hence "tree_greater x c" by (blast dest: tree_greater_trans)
+  with 4 have 2: "tree_greater x (app b c)" by (simp add: app_tree_greater)
+  from 4 have "k < y \<and> tree_less k b" by simp
+  hence "tree_less y b" by (blast dest: tree_less_trans)
+  with 4 have 3: "tree_less y (app b c)" by (simp add: app_tree_less)
   show ?case
   proof (cases "app b c" rule: rbt_cases)
     case Empty
-    from 4 have "x < y \<and> tgt y d" by auto
-    hence "tgt x d" by (blast dest: tgt_trans)
-    with 4 Empty have "st a" and "st (Tr B Empty y w d)" and "tlt x a" and "tgt x (Tr B Empty y w d)" by auto
-    with Empty show ?thesis by (simp add: balleft_st)
+    from 4 have "x < y \<and> tree_greater y d" by auto
+    hence "tree_greater x d" by (blast dest: tree_greater_trans)
+    with 4 Empty have "sorted a" and "sorted (Branch B Empty y w d)" and "tree_less x a" and "tree_greater x (Branch B Empty y w d)" by auto
+    with Empty show ?thesis by (simp add: balleft_sorted)
   next
     case (Red lta va ka rta)
-    with 2 4 have "x < va \<and> tlt x a" by simp
-    hence 5: "tlt va a" by (blast dest: tlt_trans)
-    from Red 3 4 have "va < y \<and> tgt y d" by simp
-    hence "tgt va d" by (blast dest: tgt_trans)
+    with 2 4 have "x < va \<and> tree_less x a" by simp
+    hence 5: "tree_less va a" by (blast dest: tree_less_trans)
+    from Red 3 4 have "va < y \<and> tree_greater y d" by simp
+    hence "tree_greater va d" by (blast dest: tree_greater_trans)
     with Red 2 3 4 5 show ?thesis by simp
   next
     case (Black lta va ka rta)
-    from 4 have "x < y \<and> tgt y d" by auto
-    hence "tgt x d" by (blast dest: tgt_trans)
-    with Black 2 3 4 have "st a" and "st (Tr B (app b c) y w d)" and "tlt x a" and "tgt x (Tr B (app b c) y w d)" by auto
-    with Black show ?thesis by (simp add: balleft_st)
+    from 4 have "x < y \<and> tree_greater y d" by auto
+    hence "tree_greater x d" by (blast dest: tree_greater_trans)
+    with Black 2 3 4 have "sorted a" and "sorted (Branch B (app b c) y w d)" and "tree_less x a" and "tree_greater x (Branch B (app b c) y w d)" by auto
+    with Black show ?thesis by (simp add: balleft_sorted)
   qed
 next
   case (5 va vb vd vc b x w c)
-  hence "k < x \<and> tlt k (Tr B va vb vd vc)" by simp
-  hence "tlt x (Tr B va vb vd vc)" by (blast dest: tlt_trans)
-  with 5 show ?case by (simp add: app_tlt)
+  hence "k < x \<and> tree_less k (Branch B va vb vd vc)" by simp
+  hence "tree_less x (Branch B va vb vd vc)" by (blast dest: tree_less_trans)
+  with 5 show ?case by (simp add: app_tree_less)
 next
   case (6 a x v b va vb vd vc)
-  hence "x < k \<and> tgt k (Tr B va vb vd vc)" by simp
-  hence "tgt x (Tr B va vb vd vc)" by (blast dest: tgt_trans)
-  with 6 show ?case by (simp add: app_tgt)
+  hence "x < k \<and> tree_greater k (Branch B va vb vd vc)" by simp
+  hence "tree_greater x (Branch B va vb vd vc)" by (blast dest: tree_greater_trans)
+  with 6 show ?case by (simp add: app_tree_greater)
 qed simp+
 
 lemma app_pit: 
-  assumes "inv2 l" "inv2 r" "bh l = bh r" "inv1 l" "inv1 r"
-  shows "pin_tree k v (app l r) = (pin_tree k v l \<or> pin_tree k v r)"
+  assumes "inv2 l" "inv2 r" "bheight l = bheight r" "inv1 l" "inv1 r"
+  shows "entry_in_tree k v (app l r) = (entry_in_tree k v l \<or> entry_in_tree k v r)"
 using assms 
 proof (induct l r rule: app.induct)
   case (4 _ _ _ b c)
-  hence a: "bh (app b c) = bh b" by (simp add: app_inv2)
+  hence a: "bheight (app b c) = bheight b" by (simp add: app_inv2)
   from 4 have b: "inv1l (app b c)" by (simp add: app_inv1)
 
   show ?case
@@ -570,21 +585,21 @@
   del :: "('a\<Colon>linorder) \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
 where
   "del x Empty = Empty" |
-  "del x (Tr c a y s b) = (if x < y then delformLeft x a y s b else (if x > y then delformRight x a y s b else app a b))" |
-  "delformLeft x (Tr B lt z v rt) y s b = balleft (del x (Tr B lt z v rt)) y s b" |
-  "delformLeft x a y s b = Tr R (del x a) y s b" |
-  "delformRight x a y s (Tr B lt z v rt) = balright a y s (del x (Tr B lt z v rt))" | 
-  "delformRight x a y s b = Tr R a y s (del x b)"
+  "del x (Branch c a y s b) = (if x < y then delformLeft x a y s b else (if x > y then delformRight x a y s b else app a b))" |
+  "delformLeft x (Branch B lt z v rt) y s b = balleft (del x (Branch B lt z v rt)) y s b" |
+  "delformLeft x a y s b = Branch R (del x a) y s b" |
+  "delformRight x a y s (Branch B lt z v rt) = balright a y s (del x (Branch B lt z v rt))" | 
+  "delformRight x a y s b = Branch R a y s (del x b)"
 
 lemma 
   assumes "inv2 lt" "inv1 lt"
   shows
-  "\<lbrakk>inv2 rt; bh lt = bh rt; inv1 rt\<rbrakk> \<Longrightarrow>
-  inv2 (delformLeft x lt k v rt) \<and> bh (delformLeft x lt k v rt) = bh lt \<and> (treec lt = B \<and> treec rt = B \<and> inv1 (delformLeft x lt k v rt) \<or> (treec lt \<noteq> B \<or> treec rt \<noteq> B) \<and> inv1l (delformLeft x lt k v rt))"
-  and "\<lbrakk>inv2 rt; bh lt = bh rt; inv1 rt\<rbrakk> \<Longrightarrow>
-  inv2 (delformRight x lt k v rt) \<and> bh (delformRight x lt k v rt) = bh lt \<and> (treec lt = B \<and> treec rt = B \<and> inv1 (delformRight x lt k v rt) \<or> (treec lt \<noteq> B \<or> treec rt \<noteq> B) \<and> inv1l (delformRight x lt k v rt))"
-  and del_inv1_inv2: "inv2 (del x lt) \<and> (treec lt = R \<and> bh (del x lt) = bh lt \<and> inv1 (del x lt) 
-  \<or> treec lt = B \<and> bh (del x lt) = bh lt - 1 \<and> inv1l (del x lt))"
+  "\<lbrakk>inv2 rt; bheight lt = bheight rt; inv1 rt\<rbrakk> \<Longrightarrow>
+  inv2 (delformLeft x lt k v rt) \<and> bheight (delformLeft x lt k v rt) = bheight lt \<and> (color_of lt = B \<and> color_of rt = B \<and> inv1 (delformLeft x lt k v rt) \<or> (color_of lt \<noteq> B \<or> color_of rt \<noteq> B) \<and> inv1l (delformLeft x lt k v rt))"
+  and "\<lbrakk>inv2 rt; bheight lt = bheight rt; inv1 rt\<rbrakk> \<Longrightarrow>
+  inv2 (delformRight x lt k v rt) \<and> bheight (delformRight x lt k v rt) = bheight lt \<and> (color_of lt = B \<and> color_of rt = B \<and> inv1 (delformRight x lt k v rt) \<or> (color_of lt \<noteq> B \<or> color_of rt \<noteq> B) \<and> inv1l (delformRight x lt k v rt))"
+  and del_inv1_inv2: "inv2 (del x lt) \<and> (color_of lt = R \<and> bheight (del x lt) = bheight lt \<and> inv1 (del x lt) 
+  \<or> color_of lt = B \<and> bheight (del x lt) = bheight lt - 1 \<and> inv1l (del x lt))"
 using assms
 proof (induct x lt k v rt and x lt k v rt and x lt rule: delformLeft_delformRight_del.induct)
 case (2 y c _ y')
@@ -601,55 +616,55 @@
   qed
 next
   case (3 y lt z v rta y' ss bb) 
-  thus ?case by (cases "treec (Tr B lt z v rta) = B \<and> treec bb = B") (simp add: balleft_inv2_with_inv1 balleft_inv1 balleft_inv1l)+
+  thus ?case by (cases "color_of (Branch B lt z v rta) = B \<and> color_of bb = B") (simp add: balleft_inv2_with_inv1 balleft_inv1 balleft_inv1l)+
 next
   case (5 y a y' ss lt z v rta)
-  thus ?case by (cases "treec a = B \<and> treec (Tr B lt z v rta) = B") (simp add: balright_inv2_with_inv1 balright_inv1 balright_inv1l)+
+  thus ?case by (cases "color_of a = B \<and> color_of (Branch B lt z v rta) = B") (simp add: balright_inv2_with_inv1 balright_inv1 balright_inv1l)+
 next
-  case ("6_1" y a y' ss) thus ?case by (cases "treec a = B \<and> treec Empty = B") simp+
+  case ("6_1" y a y' ss) thus ?case by (cases "color_of a = B \<and> color_of Empty = B") simp+
 qed auto
 
 lemma 
-  delformLeft_tlt: "\<lbrakk>tlt v lt; tlt v rt; k < v\<rbrakk> \<Longrightarrow> tlt v (delformLeft x lt k y rt)"
-  and delformRight_tlt: "\<lbrakk>tlt v lt; tlt v rt; k < v\<rbrakk> \<Longrightarrow> tlt v (delformRight x lt k y rt)"
-  and del_tlt: "tlt v lt \<Longrightarrow> tlt v (del x lt)"
+  delformLeft_tree_less: "\<lbrakk>tree_less v lt; tree_less v rt; k < v\<rbrakk> \<Longrightarrow> tree_less v (delformLeft x lt k y rt)"
+  and delformRight_tree_less: "\<lbrakk>tree_less v lt; tree_less v rt; k < v\<rbrakk> \<Longrightarrow> tree_less v (delformRight x lt k y rt)"
+  and del_tree_less: "tree_less v lt \<Longrightarrow> tree_less v (del x lt)"
 by (induct x lt k y rt and x lt k y rt and x lt rule: delformLeft_delformRight_del.induct) 
-   (auto simp: balleft_tlt balright_tlt)
+   (auto simp: balleft_tree_less balright_tree_less)
 
-lemma delformLeft_tgt: "\<lbrakk>tgt v lt; tgt v rt; k > v\<rbrakk> \<Longrightarrow> tgt v (delformLeft x lt k y rt)"
-  and delformRight_tgt: "\<lbrakk>tgt v lt; tgt v rt; k > v\<rbrakk> \<Longrightarrow> tgt v (delformRight x lt k y rt)"
-  and del_tgt: "tgt v lt \<Longrightarrow> tgt v (del x lt)"
+lemma delformLeft_tree_greater: "\<lbrakk>tree_greater v lt; tree_greater v rt; k > v\<rbrakk> \<Longrightarrow> tree_greater v (delformLeft x lt k y rt)"
+  and delformRight_tree_greater: "\<lbrakk>tree_greater v lt; tree_greater v rt; k > v\<rbrakk> \<Longrightarrow> tree_greater v (delformRight x lt k y rt)"
+  and del_tree_greater: "tree_greater v lt \<Longrightarrow> tree_greater v (del x lt)"
 by (induct x lt k y rt and x lt k y rt and x lt rule: delformLeft_delformRight_del.induct)
-   (auto simp: balleft_tgt balright_tgt)
+   (auto simp: balleft_tree_greater balright_tree_greater)
 
-lemma "\<lbrakk>st lt; st rt; tlt k lt; tgt k rt\<rbrakk> \<Longrightarrow> st (delformLeft x lt k y rt)"
-  and "\<lbrakk>st lt; st rt; tlt k lt; tgt k rt\<rbrakk> \<Longrightarrow> st (delformRight x lt k y rt)"
-  and del_st: "st lt \<Longrightarrow> st (del x lt)"
+lemma "\<lbrakk>sorted lt; sorted rt; tree_less k lt; tree_greater k rt\<rbrakk> \<Longrightarrow> sorted (delformLeft x lt k y rt)"
+  and "\<lbrakk>sorted lt; sorted rt; tree_less k lt; tree_greater k rt\<rbrakk> \<Longrightarrow> sorted (delformRight x lt k y rt)"
+  and del_sorted: "sorted lt \<Longrightarrow> sorted (del x lt)"
 proof (induct x lt k y rt and x lt k y rt and x lt rule: delformLeft_delformRight_del.induct)
   case (3 x lta zz v rta yy ss bb)
-  from 3 have "tlt yy (Tr B lta zz v rta)" by simp
-  hence "tlt yy (del x (Tr B lta zz v rta))" by (rule del_tlt)
-  with 3 show ?case by (simp add: balleft_st)
+  from 3 have "tree_less yy (Branch B lta zz v rta)" by simp
+  hence "tree_less yy (del x (Branch B lta zz v rta))" by (rule del_tree_less)
+  with 3 show ?case by (simp add: balleft_sorted)
 next
   case ("4_2" x vaa vbb vdd vc yy ss bb)
-  hence "tlt yy (Tr R vaa vbb vdd vc)" by simp
-  hence "tlt yy (del x (Tr R vaa vbb vdd vc))" by (rule del_tlt)
+  hence "tree_less yy (Branch R vaa vbb vdd vc)" by simp
+  hence "tree_less yy (del x (Branch R vaa vbb vdd vc))" by (rule del_tree_less)
   with "4_2" show ?case by simp
 next
   case (5 x aa yy ss lta zz v rta) 
-  hence "tgt yy (Tr B lta zz v rta)" by simp
-  hence "tgt yy (del x (Tr B lta zz v rta))" by (rule del_tgt)
-  with 5 show ?case by (simp add: balright_st)
+  hence "tree_greater yy (Branch B lta zz v rta)" by simp
+  hence "tree_greater yy (del x (Branch B lta zz v rta))" by (rule del_tree_greater)
+  with 5 show ?case by (simp add: balright_sorted)
 next
   case ("6_2" x aa yy ss vaa vbb vdd vc)
-  hence "tgt yy (Tr R vaa vbb vdd vc)" by simp
-  hence "tgt yy (del x (Tr R vaa vbb vdd vc))" by (rule del_tgt)
+  hence "tree_greater yy (Branch R vaa vbb vdd vc)" by simp
+  hence "tree_greater yy (del x (Branch R vaa vbb vdd vc))" by (rule del_tree_greater)
   with "6_2" show ?case by simp
-qed (auto simp: app_st)
+qed (auto simp: app_sorted)
 
-lemma "\<lbrakk>st lt; st rt; tlt kt lt; tgt kt rt; inv1 lt; inv1 rt; inv2 lt; inv2 rt; bh lt = bh rt; x < kt\<rbrakk> \<Longrightarrow> pin_tree k v (delformLeft x lt kt y rt) = (False \<or> (x \<noteq> k \<and> pin_tree k v (Tr c lt kt y rt)))"
-  and "\<lbrakk>st lt; st rt; tlt kt lt; tgt kt rt; inv1 lt; inv1 rt; inv2 lt; inv2 rt; bh lt = bh rt; x > kt\<rbrakk> \<Longrightarrow> pin_tree k v (delformRight x lt kt y rt) = (False \<or> (x \<noteq> k \<and> pin_tree k v (Tr c lt kt y rt)))"
-  and del_pit: "\<lbrakk>st t; inv1 t; inv2 t\<rbrakk> \<Longrightarrow> pin_tree k v (del x t) = (False \<or> (x \<noteq> k \<and> pin_tree k v t))"
+lemma "\<lbrakk>sorted lt; sorted rt; tree_less kt lt; tree_greater kt rt; inv1 lt; inv1 rt; inv2 lt; inv2 rt; bheight lt = bheight rt; x < kt\<rbrakk> \<Longrightarrow> entry_in_tree k v (delformLeft x lt kt y rt) = (False \<or> (x \<noteq> k \<and> entry_in_tree k v (Branch c lt kt y rt)))"
+  and "\<lbrakk>sorted lt; sorted rt; tree_less kt lt; tree_greater kt rt; inv1 lt; inv1 rt; inv2 lt; inv2 rt; bheight lt = bheight rt; x > kt\<rbrakk> \<Longrightarrow> entry_in_tree k v (delformRight x lt kt y rt) = (False \<or> (x \<noteq> k \<and> entry_in_tree k v (Branch c lt kt y rt)))"
+  and del_pit: "\<lbrakk>sorted t; inv1 t; inv2 t\<rbrakk> \<Longrightarrow> entry_in_tree k v (del x t) = (False \<or> (x \<noteq> k \<and> entry_in_tree k v t))"
 proof (induct x lt kt y rt and x lt kt y rt and x t rule: delformLeft_delformRight_del.induct)
   case (2 xx c aa yy ss bb)
   have "xx = yy \<or> xx < yy \<or> xx > yy" by auto
@@ -657,68 +672,68 @@
     assume "xx = yy"
     with 2 show ?thesis proof (cases "xx = k")
       case True
-      from 2 `xx = yy` `xx = k` have "st (Tr c aa yy ss bb) \<and> k = yy" by simp
-      hence "\<not> pin_tree k v aa" "\<not> pin_tree k v bb" by (auto simp: tlt_nit tgt_prop)
+      from 2 `xx = yy` `xx = k` have "sorted (Branch c aa yy ss bb) \<and> k = yy" by simp
+      hence "\<not> entry_in_tree k v aa" "\<not> entry_in_tree k v bb" by (auto simp: tree_less_nit tree_greater_prop)
       with `xx = yy` 2 `xx = k` show ?thesis by (simp add: app_pit)
     qed (simp add: app_pit)
   qed simp+
 next    
   case (3 xx lta zz vv rta yy ss bb)
-  def mt[simp]: mt == "Tr B lta zz vv rta"
+  def mt[simp]: mt == "Branch B lta zz vv rta"
   from 3 have "inv2 mt \<and> inv1 mt" by simp
-  hence "inv2 (del xx mt) \<and> (treec mt = R \<and> bh (del xx mt) = bh mt \<and> inv1 (del xx mt) \<or> treec mt = B \<and> bh (del xx mt) = bh mt - 1 \<and> inv1l (del xx mt))" by (blast dest: del_inv1_inv2)
-  with 3 have 4: "pin_tree k v (delformLeft xx mt yy ss bb) = (False \<or> xx \<noteq> k \<and> pin_tree k v mt \<or> (k = yy \<and> v = ss) \<or> pin_tree k v bb)" by (simp add: balleft_pit)
+  hence "inv2 (del xx mt) \<and> (color_of mt = R \<and> bheight (del xx mt) = bheight mt \<and> inv1 (del xx mt) \<or> color_of mt = B \<and> bheight (del xx mt) = bheight mt - 1 \<and> inv1l (del xx mt))" by (blast dest: del_inv1_inv2)
+  with 3 have 4: "entry_in_tree k v (delformLeft xx mt yy ss bb) = (False \<or> xx \<noteq> k \<and> entry_in_tree k v mt \<or> (k = yy \<and> v = ss) \<or> entry_in_tree k v bb)" by (simp add: balleft_pit)
   thus ?case proof (cases "xx = k")
     case True
-    from 3 True have "tgt yy bb \<and> yy > k" by simp
-    hence "tgt k bb" by (blast dest: tgt_trans)
-    with 3 4 True show ?thesis by (auto simp: tgt_nit)
+    from 3 True have "tree_greater yy bb \<and> yy > k" by simp
+    hence "tree_greater k bb" by (blast dest: tree_greater_trans)
+    with 3 4 True show ?thesis by (auto simp: tree_greater_nit)
   qed auto
 next
   case ("4_1" xx yy ss bb)
   show ?case proof (cases "xx = k")
     case True
-    with "4_1" have "tgt yy bb \<and> k < yy" by simp
-    hence "tgt k bb" by (blast dest: tgt_trans)
+    with "4_1" have "tree_greater yy bb \<and> k < yy" by simp
+    hence "tree_greater k bb" by (blast dest: tree_greater_trans)
     with "4_1" `xx = k` 
-   have "pin_tree k v (Tr R Empty yy ss bb) = pin_tree k v Empty" by (auto simp: tgt_nit)
+   have "entry_in_tree k v (Branch R Empty yy ss bb) = entry_in_tree k v Empty" by (auto simp: tree_greater_nit)
     thus ?thesis by auto
   qed simp+
 next
   case ("4_2" xx vaa vbb vdd vc yy ss bb)
   thus ?case proof (cases "xx = k")
     case True
-    with "4_2" have "k < yy \<and> tgt yy bb" by simp
-    hence "tgt k bb" by (blast dest: tgt_trans)
-    with True "4_2" show ?thesis by (auto simp: tgt_nit)
+    with "4_2" have "k < yy \<and> tree_greater yy bb" by simp
+    hence "tree_greater k bb" by (blast dest: tree_greater_trans)
+    with True "4_2" show ?thesis by (auto simp: tree_greater_nit)
   qed simp
 next
   case (5 xx aa yy ss lta zz vv rta)
-  def mt[simp]: mt == "Tr B lta zz vv rta"
+  def mt[simp]: mt == "Branch B lta zz vv rta"
   from 5 have "inv2 mt \<and> inv1 mt" by simp
-  hence "inv2 (del xx mt) \<and> (treec mt = R \<and> bh (del xx mt) = bh mt \<and> inv1 (del xx mt) \<or> treec mt = B \<and> bh (del xx mt) = bh mt - 1 \<and> inv1l (del xx mt))" by (blast dest: del_inv1_inv2)
-  with 5 have 3: "pin_tree k v (delformRight xx aa yy ss mt) = (pin_tree k v aa \<or> (k = yy \<and> v = ss) \<or> False \<or> xx \<noteq> k \<and> pin_tree k v mt)" by (simp add: balright_pit)
+  hence "inv2 (del xx mt) \<and> (color_of mt = R \<and> bheight (del xx mt) = bheight mt \<and> inv1 (del xx mt) \<or> color_of mt = B \<and> bheight (del xx mt) = bheight mt - 1 \<and> inv1l (del xx mt))" by (blast dest: del_inv1_inv2)
+  with 5 have 3: "entry_in_tree k v (delformRight xx aa yy ss mt) = (entry_in_tree k v aa \<or> (k = yy \<and> v = ss) \<or> False \<or> xx \<noteq> k \<and> entry_in_tree k v mt)" by (simp add: balright_pit)
   thus ?case proof (cases "xx = k")
     case True
-    from 5 True have "tlt yy aa \<and> yy < k" by simp
-    hence "tlt k aa" by (blast dest: tlt_trans)
-    with 3 5 True show ?thesis by (auto simp: tlt_nit)
+    from 5 True have "tree_less yy aa \<and> yy < k" by simp
+    hence "tree_less k aa" by (blast dest: tree_less_trans)
+    with 3 5 True show ?thesis by (auto simp: tree_less_nit)
   qed auto
 next
   case ("6_1" xx aa yy ss)
   show ?case proof (cases "xx = k")
     case True
-    with "6_1" have "tlt yy aa \<and> k > yy" by simp
-    hence "tlt k aa" by (blast dest: tlt_trans)
-    with "6_1" `xx = k` show ?thesis by (auto simp: tlt_nit)
+    with "6_1" have "tree_less yy aa \<and> k > yy" by simp
+    hence "tree_less k aa" by (blast dest: tree_less_trans)
+    with "6_1" `xx = k` show ?thesis by (auto simp: tree_less_nit)
   qed simp
 next
   case ("6_2" xx aa yy ss vaa vbb vdd vc)
   thus ?case proof (cases "xx = k")
     case True
-    with "6_2" have "k > yy \<and> tlt yy aa" by simp
-    hence "tlt k aa" by (blast dest: tlt_trans)
-    with True "6_2" show ?thesis by (auto simp: tlt_nit)
+    with "6_2" have "k > yy \<and> tree_less yy aa" by simp
+    hence "tree_less k aa" by (blast dest: tree_less_trans)
+    with True "6_2" show ?thesis by (auto simp: tree_less_nit)
   qed simp
 qed simp
 
@@ -726,36 +741,36 @@
 definition delete where
   delete_def: "delete k t = paint B (del k t)"
 
-theorem delete_isrbt[simp]: assumes "isrbt t" shows "isrbt (delete k t)"
+theorem delete_is_rbt[simp]: assumes "is_rbt t" shows "is_rbt (delete k t)"
 proof -
-  from assms have "inv2 t" and "inv1 t" unfolding isrbt_def by auto 
-  hence "inv2 (del k t) \<and> (treec t = R \<and> bh (del k t) = bh t \<and> inv1 (del k t) \<or> treec t = B \<and> bh (del k t) = bh t - 1 \<and> inv1l (del k t))" by (rule del_inv1_inv2)
-  hence "inv2 (del k t) \<and> inv1l (del k t)" by (cases "treec t") auto
+  from assms have "inv2 t" and "inv1 t" unfolding is_rbt_def by auto 
+  hence "inv2 (del k t) \<and> (color_of t = R \<and> bheight (del k t) = bheight t \<and> inv1 (del k t) \<or> color_of t = B \<and> bheight (del k t) = bheight t - 1 \<and> inv1l (del k t))" by (rule del_inv1_inv2)
+  hence "inv2 (del k t) \<and> inv1l (del k t)" by (cases "color_of t") auto
   with assms show ?thesis
-    unfolding isrbt_def delete_def
-    by (auto intro: paint_st del_st)
+    unfolding is_rbt_def delete_def
+    by (auto intro: paint_sorted del_sorted)
 qed
 
 lemma delete_pit: 
-  assumes "isrbt t" 
-  shows "pin_tree k v (delete x t) = (x \<noteq> k \<and> pin_tree k v t)"
-  using assms unfolding isrbt_def delete_def
+  assumes "is_rbt t" 
+  shows "entry_in_tree k v (delete x t) = (x \<noteq> k \<and> entry_in_tree k v t)"
+  using assms unfolding is_rbt_def delete_def
   by (auto simp: del_pit)
 
-lemma map_of_delete:
-  assumes isrbt: "isrbt t"
-  shows "map_of (delete k t) = (map_of t)|`(-{k})"
+lemma lookup_delete:
+  assumes is_rbt: "is_rbt t"
+  shows "lookup (delete k t) = (lookup t)|`(-{k})"
 proof
   fix x
-  show "map_of (delete k t) x = (map_of t |` (-{k})) x" 
+  show "lookup (delete k t) x = (lookup t |` (-{k})) x" 
   proof (cases "x = k")
     assume "x = k" 
-    with isrbt show ?thesis
-      by (cases "map_of (delete k t) k") (auto simp: mapof_pit delete_pit)
+    with is_rbt show ?thesis
+      by (cases "lookup (delete k t) k") (auto simp: lookup_pit delete_pit)
   next
     assume "x \<noteq> k"
     thus ?thesis
-      by auto (metis isrbt delete_isrbt delete_pit isrbt_st mapof_from_pit)
+      by auto (metis is_rbt delete_is_rbt delete_pit is_rbt_sorted lookup_from_pit)
   qed
 qed
 
@@ -765,43 +780,43 @@
   unionwithkey :: "('a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
 where
   "unionwithkey f t Empty = t"
-| "unionwithkey f t (Tr c lt k v rt) = unionwithkey f (unionwithkey f (insertwithkey f k v t) lt) rt"
+| "unionwithkey f t (Branch c lt k v rt) = unionwithkey f (unionwithkey f (insertwithkey f k v t) lt) rt"
 
-lemma unionwk_st: "st lt \<Longrightarrow> st (unionwithkey f lt rt)" 
-  by (induct rt arbitrary: lt) (auto simp: insertwk_st)
-theorem unionwk_isrbt[simp]: "isrbt lt \<Longrightarrow> isrbt (unionwithkey f lt rt)" 
-  by (induct rt arbitrary: lt) (simp add: insertwk_isrbt)+
+lemma unionwk_sorted: "sorted lt \<Longrightarrow> sorted (unionwithkey f lt rt)" 
+  by (induct rt arbitrary: lt) (auto simp: insertwk_sorted)
+theorem unionwk_is_rbt[simp]: "is_rbt lt \<Longrightarrow> is_rbt (unionwithkey f lt rt)" 
+  by (induct rt arbitrary: lt) (simp add: insertwk_is_rbt)+
 
 definition
   unionwith where
   "unionwith f = unionwithkey (\<lambda>_. f)"
 
-theorem unionw_isrbt: "isrbt lt \<Longrightarrow> isrbt (unionwith f lt rt)" unfolding unionwith_def by simp
+theorem unionw_is_rbt: "is_rbt lt \<Longrightarrow> is_rbt (unionwith f lt rt)" unfolding unionwith_def by simp
 
 definition union where
   "union = unionwithkey (%_ _ rv. rv)"
 
-theorem union_isrbt: "isrbt lt \<Longrightarrow> isrbt (union lt rt)" unfolding union_def by simp
+theorem union_is_rbt: "is_rbt lt \<Longrightarrow> is_rbt (union lt rt)" unfolding union_def by simp
 
-lemma union_Tr[simp]:
-  "union t (Tr c lt k v rt) = union (union (insrt k v t) lt) rt"
-  unfolding union_def insrt_def
+lemma union_Branch[simp]:
+  "union t (Branch c lt k v rt) = union (union (insert k v t) lt) rt"
+  unfolding union_def insert_def
   by simp
 
-lemma map_of_union:
-  assumes "isrbt s" "st t"
-  shows "map_of (union s t) = map_of s ++ map_of t"
+lemma lookup_union:
+  assumes "is_rbt s" "sorted t"
+  shows "lookup (union s t) = lookup s ++ lookup t"
 using assms
 proof (induct t arbitrary: s)
   case Empty thus ?case by (auto simp: union_def)
 next
-  case (Tr c l k v r s)
-  hence strl: "st r" "st l" "l |\<guillemotleft> k" "k \<guillemotleft>| r" by auto
+  case (Branch c l k v r s)
+  hence sortedrl: "sorted r" "sorted l" "l |\<guillemotleft> k" "k \<guillemotleft>| r" by auto
 
-  have meq: "map_of s(k \<mapsto> v) ++ map_of l ++ map_of r =
-    map_of s ++
-    (\<lambda>a. if a < k then map_of l a
-    else if k < a then map_of r a else Some v)" (is "?m1 = ?m2")
+  have meq: "lookup s(k \<mapsto> v) ++ lookup l ++ lookup r =
+    lookup s ++
+    (\<lambda>a. if a < k then lookup l a
+    else if k < a then lookup r a else Some v)" (is "?m1 = ?m2")
   proof (rule ext)
     fix a
 
@@ -809,7 +824,7 @@
     thus "?m1 a = ?m2 a"
     proof (elim disjE)
       assume "k < a"
-      with `l |\<guillemotleft> k` have "l |\<guillemotleft> a" by (rule tlt_trans)
+      with `l |\<guillemotleft> k` have "l |\<guillemotleft> a" by (rule tree_less_trans)
       with `k < a` show ?thesis
         by (auto simp: map_add_def split: option.splits)
     next
@@ -818,20 +833,20 @@
       show ?thesis by (auto simp: map_add_def)
     next
       assume "a < k"
-      from this `k \<guillemotleft>| r` have "a \<guillemotleft>| r" by (rule tgt_trans)
+      from this `k \<guillemotleft>| r` have "a \<guillemotleft>| r" by (rule tree_greater_trans)
       with `a < k` show ?thesis
         by (auto simp: map_add_def split: option.splits)
     qed
   qed
 
-  from Tr
+  from Branch
   have IHs:
-    "map_of (union (union (insrt k v s) l) r) = map_of (union (insrt k v s) l) ++ map_of r"
-    "map_of (union (insrt k v s) l) = map_of (insrt k v s) ++ map_of l"
-    by (auto intro: union_isrbt insrt_isrbt)
+    "lookup (union (union (insert k v s) l) r) = lookup (union (insert k v s) l) ++ lookup r"
+    "lookup (union (insert k v s) l) = lookup (insert k v s) ++ lookup l"
+    by (auto intro: union_is_rbt insert_is_rbt)
   
   with meq show ?case
-    by (auto simp: map_of_insert[OF Tr(3)])
+    by (auto simp: lookup_insert[OF Branch(3)])
 qed
 
 subsection {* Adjust *}
@@ -840,33 +855,33 @@
   adjustwithkey :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder) \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
 where
   "adjustwithkey f k Empty = Empty"
-| "adjustwithkey f k (Tr c lt x v rt) = (if k < x then (Tr c (adjustwithkey f k lt) x v rt) else if k > x then (Tr c lt x v (adjustwithkey f k rt)) else (Tr c lt x (f x v) rt))"
+| "adjustwithkey f k (Branch c lt x v rt) = (if k < x then (Branch c (adjustwithkey f k lt) x v rt) else if k > x then (Branch c lt x v (adjustwithkey f k rt)) else (Branch c lt x (f x v) rt))"
 
-lemma adjustwk_treec: "treec (adjustwithkey f k t) = treec t" by (induct t) simp+
-lemma adjustwk_inv1: "inv1 (adjustwithkey f k t) = inv1 t" by (induct t) (simp add: adjustwk_treec)+
-lemma adjustwk_inv2: "inv2 (adjustwithkey f k t) = inv2 t" "bh (adjustwithkey f k t) = bh t" by (induct t) simp+
-lemma adjustwk_tgt: "tgt k (adjustwithkey f kk t) = tgt k t" by (induct t) simp+
-lemma adjustwk_tlt: "tlt k (adjustwithkey f kk t) = tlt k t" by (induct t) simp+
-lemma adjustwk_st: "st (adjustwithkey f k t) = st t" by (induct t) (simp add: adjustwk_tlt adjustwk_tgt)+
+lemma adjustwk_color_of: "color_of (adjustwithkey f k t) = color_of t" by (induct t) simp+
+lemma adjustwk_inv1: "inv1 (adjustwithkey f k t) = inv1 t" by (induct t) (simp add: adjustwk_color_of)+
+lemma adjustwk_inv2: "inv2 (adjustwithkey f k t) = inv2 t" "bheight (adjustwithkey f k t) = bheight t" by (induct t) simp+
+lemma adjustwk_tree_greater: "tree_greater k (adjustwithkey f kk t) = tree_greater k t" by (induct t) simp+
+lemma adjustwk_tree_less: "tree_less k (adjustwithkey f kk t) = tree_less k t" by (induct t) simp+
+lemma adjustwk_sorted: "sorted (adjustwithkey f k t) = sorted t" by (induct t) (simp add: adjustwk_tree_less adjustwk_tree_greater)+
 
-theorem adjustwk_isrbt[simp]: "isrbt (adjustwithkey f k t) = isrbt t" 
-unfolding isrbt_def by (simp add: adjustwk_inv2 adjustwk_treec adjustwk_st adjustwk_inv1 )
+theorem adjustwk_is_rbt[simp]: "is_rbt (adjustwithkey f k t) = is_rbt t" 
+unfolding is_rbt_def by (simp add: adjustwk_inv2 adjustwk_color_of adjustwk_sorted adjustwk_inv1 )
 
 theorem adjustwithkey_map[simp]:
-  "map_of (adjustwithkey f k t) x = 
-  (if x = k then case map_of t x of None \<Rightarrow> None | Some y \<Rightarrow> Some (f k y)
-            else map_of t x)"
+  "lookup (adjustwithkey f k t) x = 
+  (if x = k then case lookup t x of None \<Rightarrow> None | Some y \<Rightarrow> Some (f k y)
+            else lookup t x)"
 by (induct t arbitrary: x) (auto split:option.splits)
 
 definition adjust where
   "adjust f = adjustwithkey (\<lambda>_. f)"
 
-theorem adjust_isrbt[simp]: "isrbt (adjust f k t) = isrbt t" unfolding adjust_def by simp
+theorem adjust_is_rbt[simp]: "is_rbt (adjust f k t) = is_rbt t" unfolding adjust_def by simp
 
 theorem adjust_map[simp]:
-  "map_of (adjust f k t) x = 
-  (if x = k then case map_of t x of None \<Rightarrow> None | Some y \<Rightarrow> Some (f y)
-            else map_of t x)"
+  "lookup (adjust f k t) x = 
+  (if x = k then case lookup t x of None \<Rightarrow> None | Some y \<Rightarrow> Some (f y)
+            else lookup t x)"
 unfolding adjust_def by simp
 
 subsection {* Map *}
@@ -875,27 +890,27 @@
   mapwithkey :: "('a::linorder \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'c) rbt"
 where
   "mapwithkey f Empty = Empty"
-| "mapwithkey f (Tr c lt k v rt) = Tr c (mapwithkey f lt) k (f k v) (mapwithkey f rt)"
+| "mapwithkey f (Branch c lt k v rt) = Branch c (mapwithkey f lt) k (f k v) (mapwithkey f rt)"
 
 theorem mapwk_keys[simp]: "keys (mapwithkey f t) = keys t" by (induct t) auto
-lemma mapwk_tgt: "tgt k (mapwithkey f t) = tgt k t" by (induct t) simp+
-lemma mapwk_tlt: "tlt k (mapwithkey f t) = tlt k t" by (induct t) simp+
-lemma mapwk_st: "st (mapwithkey f t) = st t"  by (induct t) (simp add: mapwk_tlt mapwk_tgt)+
-lemma mapwk_treec: "treec (mapwithkey f t) = treec t" by (induct t) simp+
-lemma mapwk_inv1: "inv1 (mapwithkey f t) = inv1 t" by (induct t) (simp add: mapwk_treec)+
-lemma mapwk_inv2: "inv2 (mapwithkey f t) = inv2 t" "bh (mapwithkey f t) = bh t" by (induct t) simp+
-theorem mapwk_isrbt[simp]: "isrbt (mapwithkey f t) = isrbt t" 
-unfolding isrbt_def by (simp add: mapwk_inv1 mapwk_inv2 mapwk_st mapwk_treec)
+lemma mapwk_tree_greater: "tree_greater k (mapwithkey f t) = tree_greater k t" by (induct t) simp+
+lemma mapwk_tree_less: "tree_less k (mapwithkey f t) = tree_less k t" by (induct t) simp+
+lemma mapwk_sorted: "sorted (mapwithkey f t) = sorted t"  by (induct t) (simp add: mapwk_tree_less mapwk_tree_greater)+
+lemma mapwk_color_of: "color_of (mapwithkey f t) = color_of t" by (induct t) simp+
+lemma mapwk_inv1: "inv1 (mapwithkey f t) = inv1 t" by (induct t) (simp add: mapwk_color_of)+
+lemma mapwk_inv2: "inv2 (mapwithkey f t) = inv2 t" "bheight (mapwithkey f t) = bheight t" by (induct t) simp+
+theorem mapwk_is_rbt[simp]: "is_rbt (mapwithkey f t) = is_rbt t" 
+unfolding is_rbt_def by (simp add: mapwk_inv1 mapwk_inv2 mapwk_sorted mapwk_color_of)
 
-theorem map_of_mapwk[simp]: "map_of (mapwithkey f t) x = Option.map (f x) (map_of t x)"
+theorem lookup_mapwk[simp]: "lookup (mapwithkey f t) x = Option.map (f x) (lookup t x)"
 by (induct t) auto
 
 definition map
 where map_def: "map f == mapwithkey (\<lambda>_. f)"
 
 theorem map_keys[simp]: "keys (map f t) = keys t" unfolding map_def by simp
-theorem map_isrbt[simp]: "isrbt (map f t) = isrbt t" unfolding map_def by simp
-theorem map_of_map[simp]: "map_of (map f t) = Option.map f o map_of t"
+theorem map_is_rbt[simp]: "is_rbt (map f t) = is_rbt t" unfolding map_def by simp
+theorem lookup_map[simp]: "lookup (map f t) = Option.map f o lookup t"
   by (rule ext) (simp add:map_def)
 
 subsection {* Fold *}
@@ -906,62 +921,57 @@
   foldwithkey :: "('a::linorder \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a,'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c"
 where
   "foldwithkey f Empty v = v"
-| "foldwithkey f (Tr c lt k x rt) v = foldwithkey f rt (f k x (foldwithkey f lt v))"
+| "foldwithkey f (Branch c lt k x rt) v = foldwithkey f rt (f k x (foldwithkey f lt v))"
 
-primrec alist_of
-where 
-  "alist_of Empty = []"
-| "alist_of (Tr _ l k v r) = alist_of l @ (k,v) # alist_of r"
-
-lemma map_of_alist_of_aux: "st (Tr c t1 k v t2) \<Longrightarrow> RBT.map_of (Tr c t1 k v t2) = RBT.map_of t2 ++ [k\<mapsto>v] ++ RBT.map_of t1"
+lemma lookup_entries_aux: "sorted (Branch c t1 k v t2) \<Longrightarrow> RBT.lookup (Branch c t1 k v t2) = RBT.lookup t2 ++ [k\<mapsto>v] ++ RBT.lookup t1"
 proof (rule ext)
   fix x
-  assume ST: "st (Tr c t1 k v t2)"
-  let ?thesis = "RBT.map_of (Tr c t1 k v t2) x = (RBT.map_of t2 ++ [k \<mapsto> v] ++ RBT.map_of t1) x"
+  assume SORTED: "sorted (Branch c t1 k v t2)"
+  let ?thesis = "RBT.lookup (Branch c t1 k v t2) x = (RBT.lookup t2 ++ [k \<mapsto> v] ++ RBT.lookup t1) x"
 
-  have DOM_T1: "!!k'. k'\<in>dom (RBT.map_of t1) \<Longrightarrow> k>k'"
+  have DOM_T1: "!!k'. k'\<in>dom (RBT.lookup t1) \<Longrightarrow> k>k'"
   proof -
     fix k'
-    from ST have "t1 |\<guillemotleft> k" by simp
-    with tlt_prop have "\<forall>k'\<in>keys t1. k>k'" by auto
-    moreover assume "k'\<in>dom (RBT.map_of t1)"
-    ultimately show "k>k'" using RBT.mapof_keys ST by auto
+    from SORTED have "t1 |\<guillemotleft> k" by simp
+    with tree_less_prop have "\<forall>k'\<in>keys t1. k>k'" by auto
+    moreover assume "k'\<in>dom (RBT.lookup t1)"
+    ultimately show "k>k'" using RBT.lookup_keys SORTED by auto
   qed
 
-  have DOM_T2: "!!k'. k'\<in>dom (RBT.map_of t2) \<Longrightarrow> k<k'"
+  have DOM_T2: "!!k'. k'\<in>dom (RBT.lookup t2) \<Longrightarrow> k<k'"
   proof -
     fix k'
-    from ST have "k \<guillemotleft>| t2" by simp
-    with tgt_prop have "\<forall>k'\<in>keys t2. k<k'" by auto
-    moreover assume "k'\<in>dom (RBT.map_of t2)"
-    ultimately show "k<k'" using RBT.mapof_keys ST by auto
+    from SORTED have "k \<guillemotleft>| t2" by simp
+    with tree_greater_prop have "\<forall>k'\<in>keys t2. k<k'" by auto
+    moreover assume "k'\<in>dom (RBT.lookup t2)"
+    ultimately show "k<k'" using RBT.lookup_keys SORTED by auto
   qed
 
   {
     assume C: "x<k"
-    hence "RBT.map_of (Tr c t1 k v t2) x = RBT.map_of t1 x" by simp
+    hence "RBT.lookup (Branch c t1 k v t2) x = RBT.lookup t1 x" by simp
     moreover from C have "x\<notin>dom [k\<mapsto>v]" by simp
-    moreover have "x\<notin>dom (RBT.map_of t2)" proof
-      assume "x\<in>dom (RBT.map_of t2)"
+    moreover have "x\<notin>dom (RBT.lookup t2)" proof
+      assume "x\<in>dom (RBT.lookup t2)"
       with DOM_T2 have "k<x" by blast
       with C show False by simp
     qed
     ultimately have ?thesis by (simp add: map_add_upd_left map_add_dom_app_simps)
   } moreover {
     assume [simp]: "x=k"
-    hence "RBT.map_of (Tr c t1 k v t2) x = [k \<mapsto> v] x" by simp
-    moreover have "x\<notin>dom (RBT.map_of t1)" proof
-      assume "x\<in>dom (RBT.map_of t1)"
+    hence "RBT.lookup (Branch c t1 k v t2) x = [k \<mapsto> v] x" by simp
+    moreover have "x\<notin>dom (RBT.lookup t1)" proof
+      assume "x\<in>dom (RBT.lookup t1)"
       with DOM_T1 have "k>x" by blast
       thus False by simp
     qed
     ultimately have ?thesis by (simp add: map_add_upd_left map_add_dom_app_simps)
   } moreover {
     assume C: "x>k"
-    hence "RBT.map_of (Tr c t1 k v t2) x = RBT.map_of t2 x" by (simp add: less_not_sym[of k x])
+    hence "RBT.lookup (Branch c t1 k v t2) x = RBT.lookup t2 x" by (simp add: less_not_sym[of k x])
     moreover from C have "x\<notin>dom [k\<mapsto>v]" by simp
-    moreover have "x\<notin>dom (RBT.map_of t1)" proof
-      assume "x\<in>dom (RBT.map_of t1)"
+    moreover have "x\<notin>dom (RBT.lookup t1)" proof
+      assume "x\<in>dom (RBT.lookup t1)"
       with DOM_T1 have "k>x" by simp
       with C show False by simp
     qed
@@ -969,35 +979,38 @@
   } ultimately show ?thesis using less_linear by blast
 qed
 
-lemma map_of_alist_of:
-  shows "st t \<Longrightarrow> Map.map_of (alist_of t) = map_of t"
+lemma map_of_entries:
+  shows "sorted t \<Longrightarrow> map_of (entries t) = lookup t"
 proof (induct t)
-  case Empty thus ?case by (simp add: RBT.map_of_Empty)
+  case Empty thus ?case by (simp add: RBT.lookup_Empty)
 next
-  case (Tr c t1 k v t2)
-  hence "Map.map_of (alist_of (Tr c t1 k v t2)) = RBT.map_of t2 ++ [k \<mapsto> v] ++ RBT.map_of t1" by simp
-  also note map_of_alist_of_aux[OF Tr.prems,symmetric]
+  case (Branch c t1 k v t2)
+  hence "map_of (entries (Branch c t1 k v t2)) = RBT.lookup t2 ++ [k \<mapsto> v] ++ RBT.lookup t1" by simp
+  also note lookup_entries_aux [OF Branch.prems,symmetric]
   finally show ?case .
 qed
 
-lemma fold_alist_fold:
-  "foldwithkey f t x = foldl (\<lambda>x (k,v). f k v x) x (alist_of t)"
+lemma fold_entries_fold:
+  "foldwithkey f t x = foldl (\<lambda>x (k,v). f k v x) x (entries t)"
 by (induct t arbitrary: x) auto
 
-lemma alist_pit[simp]: "(k, v) \<in> set (alist_of t) = pin_tree k v t"
+lemma entries_pit[simp]: "(k, v) \<in> set (entries t) = entry_in_tree k v t"
 by (induct t) auto
 
-lemma sorted_alist:
-  "st t \<Longrightarrow> sorted (List.map fst (alist_of t))"
+lemma sorted_entries:
+  "sorted t \<Longrightarrow> List.sorted (List.map fst (entries t))"
 by (induct t) 
-  (force simp: sorted_append sorted_Cons tlgt_props 
-      dest!:pint_keys)+
+  (force simp: sorted_append sorted_Cons tree_ord_props 
+      dest!: entry_in_tree_keys)+
 
-lemma distinct_alist:
-  "st t \<Longrightarrow> distinct (List.map fst (alist_of t))"
+lemma distinct_entries:
+  "sorted t \<Longrightarrow> distinct (List.map fst (entries t))"
 by (induct t) 
-  (force simp: sorted_append sorted_Cons tlgt_props 
-      dest!:pint_keys)+
+  (force simp: sorted_append sorted_Cons tree_ord_props 
+      dest!: entry_in_tree_keys)+
+
+hide (open) const Empty insert delete entries lookup map fold union adjust sorted
+
 (*>*)
 
 text {* 
@@ -1010,20 +1023,20 @@
 text {*
   The type @{typ "('k, 'v) rbt"} denotes red-black trees with keys of
   type @{typ "'k"} and values of type @{typ "'v"}. To function
-  properly, the key type must belong to the @{text "linorder"} class.
+  properly, the key type musorted belong to the @{text "linorder"} class.
 
   A value @{term t} of this type is a valid red-black tree if it
-  satisfies the invariant @{text "isrbt t"}.
+  satisfies the invariant @{text "is_rbt t"}.
   This theory provides lemmas to prove that the invariant is
   satisfied throughout the computation.
 
-  The interpretation function @{const "map_of"} returns the partial
+  The interpretation function @{const "RBT.lookup"} returns the partial
   map represented by a red-black tree:
-  @{term_type[display] "map_of"}
+  @{term_type[display] "RBT.lookup"}
 
   This function should be used for reasoning about the semantics of the RBT
   operations. Furthermore, it implements the lookup functionality for
-  the data structure: It is executable and the lookup is performed in
+  the data sortedructure: It is executable and the lookup is performed in
   $O(\log n)$.  
 *}
 
@@ -1032,19 +1045,19 @@
 text {*
   Currently, the following operations are supported:
 
-  @{term_type[display] "Empty"}
+  @{term_type[display] "RBT.Empty"}
   Returns the empty tree. $O(1)$
 
-  @{term_type[display] "insrt"}
+  @{term_type[display] "RBT.insert"}
   Updates the map at a given position. $O(\log n)$
 
-  @{term_type[display] "delete"}
+  @{term_type[display] "RBT.delete"}
   Deletes a map entry at a given position. $O(\log n)$
 
-  @{term_type[display] "union"}
+  @{term_type[display] "RBT.union"}
   Forms the union of two trees, preferring entries from the first one.
 
-  @{term_type[display] "map"}
+  @{term_type[display] "RBT.map"}
   Maps a function over the values of a map. $O(n)$
 *}
 
@@ -1053,47 +1066,47 @@
 
 text {*
   \noindent
-  @{thm Empty_isrbt}\hfill(@{text "Empty_isrbt"})
+  @{thm Empty_is_rbt}\hfill(@{text "Empty_is_rbt"})
 
   \noindent
-  @{thm insrt_isrbt}\hfill(@{text "insrt_isrbt"})
+  @{thm insert_is_rbt}\hfill(@{text "insert_is_rbt"})
 
   \noindent
-  @{thm delete_isrbt}\hfill(@{text "delete_isrbt"})
+  @{thm delete_is_rbt}\hfill(@{text "delete_is_rbt"})
 
   \noindent
-  @{thm union_isrbt}\hfill(@{text "union_isrbt"})
+  @{thm union_is_rbt}\hfill(@{text "union_is_rbt"})
 
   \noindent
-  @{thm map_isrbt}\hfill(@{text "map_isrbt"})
+  @{thm map_is_rbt}\hfill(@{text "map_is_rbt"})
 *}
 
 subsection {* Map Semantics *}
 
 text {*
   \noindent
-  \underline{@{text "map_of_Empty"}}
-  @{thm[display] map_of_Empty}
+  \underline{@{text "lookup_Empty"}}
+  @{thm[display] lookup_Empty}
   \vspace{1ex}
 
   \noindent
-  \underline{@{text "map_of_insert"}}
-  @{thm[display] map_of_insert}
+  \underline{@{text "lookup_insert"}}
+  @{thm[display] lookup_insert}
   \vspace{1ex}
 
   \noindent
-  \underline{@{text "map_of_delete"}}
-  @{thm[display] map_of_delete}
+  \underline{@{text "lookup_delete"}}
+  @{thm[display] lookup_delete}
   \vspace{1ex}
 
   \noindent
-  \underline{@{text "map_of_union"}}
-  @{thm[display] map_of_union}
+  \underline{@{text "lookup_union"}}
+  @{thm[display] lookup_union}
   \vspace{1ex}
 
   \noindent
-  \underline{@{text "map_of_map"}}
-  @{thm[display] map_of_map}
+  \underline{@{text "lookup_map"}}
+  @{thm[display] lookup_map}
   \vspace{1ex}
 *}
 
diff -r 94170181a842 -r 67879e5d695c src/HOLCF/Bifinite.thy
--- a/src/HOLCF/Bifinite.thy	Tue Mar 02 22:13:39 2010 +0100
+++ b/src/HOLCF/Bifinite.thy	Wed Mar 03 09:33:46 2010 +0100
@@ -295,7 +295,7 @@
     by (rule finite_range_imp_finite_fixes)
 qed
 
-instantiation "->" :: (profinite, profinite) profinite
+instantiation cfun :: (profinite, profinite) profinite
 begin
 
 definition
@@ -325,7 +325,7 @@
 
 end
 
-instance "->" :: (profinite, bifinite) bifinite ..
+instance cfun :: (profinite, bifinite) bifinite ..
 
 lemma approx_cfun: "approx n\<cdot>f\<cdot>x = approx n\<cdot>(f\<cdot>(approx n\<cdot>x))"
 by (simp add: approx_cfun_def)
diff -r 94170181a842 -r 67879e5d695c src/HOLCF/Cfun.thy
--- a/src/HOLCF/Cfun.thy	Tue Mar 02 22:13:39 2010 +0100
+++ b/src/HOLCF/Cfun.thy	Wed Mar 03 09:33:46 2010 +0100
@@ -20,11 +20,11 @@
 lemma adm_cont: "adm cont"
 by (rule admI, rule cont_lub_fun)
 
-cpodef (CFun)  ('a, 'b) "->" (infixr "->" 0) = "{f::'a => 'b. cont f}"
+cpodef (CFun)  ('a, 'b) cfun (infixr "->" 0) = "{f::'a => 'b. cont f}"
 by (simp_all add: Ex_cont adm_cont)
 
-syntax (xsymbols)
-  "->"     :: "[type, type] => type"      ("(_ \<rightarrow>/ _)" [1,0]0)
+type_notation (xsymbols)
+  cfun  ("(_ \<rightarrow>/ _)" [1, 0] 0)
 
 notation
   Rep_CFun  ("(_$/_)" [999,1000] 999)
@@ -103,16 +103,16 @@
 lemma UU_CFun: "\<bottom> \<in> CFun"
 by (simp add: CFun_def inst_fun_pcpo cont_const)
 
-instance "->" :: (finite_po, finite_po) finite_po
+instance cfun :: (finite_po, finite_po) finite_po
 by (rule typedef_finite_po [OF type_definition_CFun])
 
-instance "->" :: (finite_po, chfin) chfin
+instance cfun :: (finite_po, chfin) chfin
 by (rule typedef_chfin [OF type_definition_CFun below_CFun_def])
 
-instance "->" :: (cpo, discrete_cpo) discrete_cpo
+instance cfun :: (cpo, discrete_cpo) discrete_cpo
 by intro_classes (simp add: below_CFun_def Rep_CFun_inject)
 
-instance "->" :: (cpo, pcpo) pcpo
+instance cfun :: (cpo, pcpo) pcpo
 by (rule typedef_pcpo [OF type_definition_CFun below_CFun_def UU_CFun])
 
 lemmas Rep_CFun_strict =
diff -r 94170181a842 -r 67879e5d695c src/HOLCF/Domain.thy
--- a/src/HOLCF/Domain.thy	Tue Mar 02 22:13:39 2010 +0100
+++ b/src/HOLCF/Domain.thy	Wed Mar 03 09:33:46 2010 +0100
@@ -11,7 +11,6 @@
   ("Tools/cont_proc.ML")
   ("Tools/Domain/domain_constructors.ML")
   ("Tools/Domain/domain_library.ML")
-  ("Tools/Domain/domain_syntax.ML")
   ("Tools/Domain/domain_axioms.ML")
   ("Tools/Domain/domain_theorems.ML")
   ("Tools/Domain/domain_extender.ML")
@@ -274,7 +273,6 @@
 use "Tools/cont_consts.ML"
 use "Tools/cont_proc.ML"
 use "Tools/Domain/domain_library.ML"
-use "Tools/Domain/domain_syntax.ML"
 use "Tools/Domain/domain_axioms.ML"
 use "Tools/Domain/domain_constructors.ML"
 use "Tools/Domain/domain_theorems.ML"
diff -r 94170181a842 -r 67879e5d695c src/HOLCF/FOCUS/Fstream.thy
--- a/src/HOLCF/FOCUS/Fstream.thy	Tue Mar 02 22:13:39 2010 +0100
+++ b/src/HOLCF/FOCUS/Fstream.thy	Wed Mar 03 09:33:46 2010 +0100
@@ -83,7 +83,7 @@
 by (simp add: fscons_def2)
 
 lemma fstream_prefix: "a~> s << t ==> ? tt. t = a~> tt &  s << tt"
-apply (rule_tac x="t" in stream.casedist)
+apply (cases t)
 apply (cut_tac fscons_not_empty)
 apply (fast dest: eq_UU_iff [THEN iffD2])
 apply (simp add: fscons_def2)
diff -r 94170181a842 -r 67879e5d695c src/HOLCF/Fixrec.thy
--- a/src/HOLCF/Fixrec.thy	Tue Mar 02 22:13:39 2010 +0100
+++ b/src/HOLCF/Fixrec.thy	Wed Mar 03 09:33:46 2010 +0100
@@ -6,7 +6,9 @@
 
 theory Fixrec
 imports Sprod Ssum Up One Tr Fix
-uses ("Tools/fixrec.ML")
+uses
+  ("Tools/holcf_library.ML")
+  ("Tools/fixrec.ML")
 begin
 
 subsection {* Maybe monad type *}
@@ -603,6 +605,7 @@
 
 subsection {* Initializing the fixrec package *}
 
+use "Tools/holcf_library.ML"
 use "Tools/fixrec.ML"
 
 setup {* Fixrec.setup *}
diff -r 94170181a842 -r 67879e5d695c src/HOLCF/IOA/meta_theory/Seq.thy
--- a/src/HOLCF/IOA/meta_theory/Seq.thy	Tue Mar 02 22:13:39 2010 +0100
+++ b/src/HOLCF/IOA/meta_theory/Seq.thy	Wed Mar 03 09:33:46 2010 +0100
@@ -191,7 +191,7 @@
 by simp
 
 lemma nil_less_is_nil: "nil<<x ==> nil=x"
-apply (rule_tac x="x" in seq.casedist)
+apply (cases x)
 apply simp
 apply simp
 apply simp
@@ -286,8 +286,8 @@
 
 lemma Finite_upward: "\<lbrakk>Finite x; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> Finite y"
 apply (induct arbitrary: y set: Finite)
-apply (rule_tac x=y in seq.casedist, simp, simp, simp)
-apply (rule_tac x=y in seq.casedist, simp, simp)
+apply (case_tac y, simp, simp, simp)
+apply (case_tac y, simp, simp)
 apply simp
 done
 
diff -r 94170181a842 -r 67879e5d695c src/HOLCF/IOA/meta_theory/Sequence.thy
--- a/src/HOLCF/IOA/meta_theory/Sequence.thy	Tue Mar 02 22:13:39 2010 +0100
+++ b/src/HOLCF/IOA/meta_theory/Sequence.thy	Wed Mar 03 09:33:46 2010 +0100
@@ -163,8 +163,7 @@
 
 lemma Last_cons: "Last$(x>>xs)= (if xs=nil then Def x else Last$xs)"
 apply (simp add: Last_def Consq_def)
-apply (rule_tac x="xs" in seq.casedist)
-apply simp
+apply (cases xs)
 apply simp_all
 done
 
@@ -208,7 +207,7 @@
 lemma Zip_UU2: "x~=nil ==> Zip$x$UU =UU"
 apply (subst Zip_unfold)
 apply simp
-apply (rule_tac x="x" in seq.casedist)
+apply (cases x)
 apply simp_all
 done
 
diff -r 94170181a842 -r 67879e5d695c src/HOLCF/IsaMakefile
--- a/src/HOLCF/IsaMakefile	Tue Mar 02 22:13:39 2010 +0100
+++ b/src/HOLCF/IsaMakefile	Wed Mar 03 09:33:46 2010 +0100
@@ -70,7 +70,7 @@
   Tools/Domain/domain_constructors.ML \
   Tools/Domain/domain_isomorphism.ML \
   Tools/Domain/domain_library.ML \
-  Tools/Domain/domain_syntax.ML \
+  Tools/Domain/domain_take_proofs.ML \
   Tools/Domain/domain_theorems.ML \
   Tools/fixrec.ML \
   Tools/pcpodef.ML \
diff -r 94170181a842 -r 67879e5d695c src/HOLCF/Representable.thy
--- a/src/HOLCF/Representable.thy	Tue Mar 02 22:13:39 2010 +0100
+++ b/src/HOLCF/Representable.thy	Wed Mar 03 09:33:46 2010 +0100
@@ -8,7 +8,7 @@
 imports Algebraic Universal Ssum Sprod One Fixrec
 uses
   ("Tools/repdef.ML")
-  ("Tools/holcf_library.ML")
+  ("Tools/Domain/domain_take_proofs.ML")
   ("Tools/Domain/domain_isomorphism.ML")
 begin
 
@@ -415,7 +415,7 @@
 
 text "Functions between representable types are representable."
 
-instantiation "->" :: (rep, rep) rep
+instantiation cfun :: (rep, rep) rep
 begin
 
 definition emb_cfun_def: "emb = udom_emb oo cfun_map\<cdot>prj\<cdot>emb"
@@ -430,7 +430,7 @@
 
 text "Strict products of representable types are representable."
 
-instantiation "**" :: (rep, rep) rep
+instantiation sprod :: (rep, rep) rep
 begin
 
 definition emb_sprod_def: "emb = udom_emb oo sprod_map\<cdot>emb\<cdot>emb"
@@ -445,7 +445,7 @@
 
 text "Strict sums of representable types are representable."
 
-instantiation "++" :: (rep, rep) rep
+instantiation ssum :: (rep, rep) rep
 begin
 
 definition emb_ssum_def: "emb = udom_emb oo ssum_map\<cdot>emb\<cdot>emb"
@@ -777,18 +777,18 @@
 
 subsection {* Constructing Domain Isomorphisms *}
 
-use "Tools/holcf_library.ML"
+use "Tools/Domain/domain_take_proofs.ML"
 use "Tools/Domain/domain_isomorphism.ML"
 
 setup {*
   fold Domain_Isomorphism.add_type_constructor
-    [(@{type_name "->"}, @{term cfun_defl}, @{const_name cfun_map}, @{thm REP_cfun},
+    [(@{type_name cfun}, @{term cfun_defl}, @{const_name cfun_map}, @{thm REP_cfun},
         @{thm isodefl_cfun}, @{thm cfun_map_ID}, @{thm deflation_cfun_map}),
 
-     (@{type_name "++"}, @{term ssum_defl}, @{const_name ssum_map}, @{thm REP_ssum},
+     (@{type_name ssum}, @{term ssum_defl}, @{const_name ssum_map}, @{thm REP_ssum},
         @{thm isodefl_ssum}, @{thm ssum_map_ID}, @{thm deflation_ssum_map}),
 
-     (@{type_name "**"}, @{term sprod_defl}, @{const_name sprod_map}, @{thm REP_sprod},
+     (@{type_name sprod}, @{term sprod_defl}, @{const_name sprod_map}, @{thm REP_sprod},
         @{thm isodefl_sprod}, @{thm sprod_map_ID}, @{thm deflation_sprod_map}),
 
      (@{type_name "*"}, @{term cprod_defl}, @{const_name cprod_map}, @{thm REP_cprod},
diff -r 94170181a842 -r 67879e5d695c src/HOLCF/Sprod.thy
--- a/src/HOLCF/Sprod.thy	Tue Mar 02 22:13:39 2010 +0100
+++ b/src/HOLCF/Sprod.thy	Wed Mar 03 09:33:46 2010 +0100
@@ -12,20 +12,20 @@
 
 subsection {* Definition of strict product type *}
 
-pcpodef (Sprod)  ('a, 'b) "**" (infixr "**" 20) =
+pcpodef (Sprod)  ('a, 'b) sprod (infixr "**" 20) =
         "{p::'a \<times> 'b. p = \<bottom> \<or> (fst p \<noteq> \<bottom> \<and> snd p \<noteq> \<bottom>)}"
 by simp_all
 
-instance "**" :: ("{finite_po,pcpo}", "{finite_po,pcpo}") finite_po
+instance sprod :: ("{finite_po,pcpo}", "{finite_po,pcpo}") finite_po
 by (rule typedef_finite_po [OF type_definition_Sprod])
 
-instance "**" :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin
+instance sprod :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin
 by (rule typedef_chfin [OF type_definition_Sprod below_Sprod_def])
 
 syntax (xsymbols)
-  "**"          :: "[type, type] => type"        ("(_ \<otimes>/ _)" [21,20] 20)
+  sprod          :: "[type, type] => type"        ("(_ \<otimes>/ _)" [21,20] 20)
 syntax (HTML output)
-  "**"          :: "[type, type] => type"        ("(_ \<otimes>/ _)" [21,20] 20)
+  sprod          :: "[type, type] => type"        ("(_ \<otimes>/ _)" [21,20] 20)
 
 lemma spair_lemma:
   "(strictify\<cdot>(\<Lambda> b. a)\<cdot>b, strictify\<cdot>(\<Lambda> a. b)\<cdot>a) \<in> Sprod"
@@ -80,11 +80,11 @@
 apply fast
 done
 
-lemma sprodE [cases type: **]:
+lemma sprodE [cases type: sprod]:
   "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; \<And>x y. \<lbrakk>p = (:x, y:); x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
 by (cut_tac z=p in Exh_Sprod, auto)
 
-lemma sprod_induct [induct type: **]:
+lemma sprod_induct [induct type: sprod]:
   "\<lbrakk>P \<bottom>; \<And>x y. \<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> P (:x, y:)\<rbrakk> \<Longrightarrow> P x"
 by (cases x, simp_all)
 
@@ -221,7 +221,7 @@
 
 subsection {* Strict product preserves flatness *}
 
-instance "**" :: (flat, flat) flat
+instance sprod :: (flat, flat) flat
 proof
   fix x y :: "'a \<otimes> 'b"
   assume "x \<sqsubseteq> y" thus "x = \<bottom> \<or> x = y"
@@ -312,7 +312,7 @@
 
 subsection {* Strict product is a bifinite domain *}
 
-instantiation "**" :: (bifinite, bifinite) bifinite
+instantiation sprod :: (bifinite, bifinite) bifinite
 begin
 
 definition
diff -r 94170181a842 -r 67879e5d695c src/HOLCF/Ssum.thy
--- a/src/HOLCF/Ssum.thy	Tue Mar 02 22:13:39 2010 +0100
+++ b/src/HOLCF/Ssum.thy	Wed Mar 03 09:33:46 2010 +0100
@@ -12,22 +12,22 @@
 
 subsection {* Definition of strict sum type *}
 
-pcpodef (Ssum)  ('a, 'b) "++" (infixr "++" 10) = 
+pcpodef (Ssum)  ('a, 'b) ssum (infixr "++" 10) = 
   "{p :: tr \<times> ('a \<times> 'b).
     (fst p \<sqsubseteq> TT \<longleftrightarrow> snd (snd p) = \<bottom>) \<and>
     (fst p \<sqsubseteq> FF \<longleftrightarrow> fst (snd p) = \<bottom>)}"
 by simp_all
 
-instance "++" :: ("{finite_po,pcpo}", "{finite_po,pcpo}") finite_po
+instance ssum :: ("{finite_po,pcpo}", "{finite_po,pcpo}") finite_po
 by (rule typedef_finite_po [OF type_definition_Ssum])
 
-instance "++" :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin
+instance ssum :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin
 by (rule typedef_chfin [OF type_definition_Ssum below_Ssum_def])
 
 syntax (xsymbols)
-  "++"          :: "[type, type] => type"       ("(_ \<oplus>/ _)" [21, 20] 20)
+  ssum          :: "[type, type] => type"       ("(_ \<oplus>/ _)" [21, 20] 20)
 syntax (HTML output)
-  "++"          :: "[type, type] => type"       ("(_ \<oplus>/ _)" [21, 20] 20)
+  ssum          :: "[type, type] => type"       ("(_ \<oplus>/ _)" [21, 20] 20)
 
 subsection {* Definitions of constructors *}
 
@@ -150,13 +150,13 @@
 apply (simp add: sinr_Abs_Ssum Ssum_def)
 done
 
-lemma ssumE [cases type: ++]:
+lemma ssumE [cases type: ssum]:
   "\<lbrakk>p = \<bottom> \<Longrightarrow> Q;
    \<And>x. \<lbrakk>p = sinl\<cdot>x; x \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> Q;
    \<And>y. \<lbrakk>p = sinr\<cdot>y; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
 by (cut_tac z=p in Exh_Ssum, auto)
 
-lemma ssum_induct [induct type: ++]:
+lemma ssum_induct [induct type: ssum]:
   "\<lbrakk>P \<bottom>;
    \<And>x. x \<noteq> \<bottom> \<Longrightarrow> P (sinl\<cdot>x);
    \<And>y. y \<noteq> \<bottom> \<Longrightarrow> P (sinr\<cdot>y)\<rbrakk> \<Longrightarrow> P x"
@@ -203,7 +203,7 @@
 
 subsection {* Strict sum preserves flatness *}
 
-instance "++" :: (flat, flat) flat
+instance ssum :: (flat, flat) flat
 apply (intro_classes, clarify)
 apply (case_tac x, simp)
 apply (case_tac y, simp_all add: flat_below_iff)
@@ -296,7 +296,7 @@
 
 subsection {* Strict sum is a bifinite domain *}
 
-instantiation "++" :: (bifinite, bifinite) bifinite
+instantiation ssum :: (bifinite, bifinite) bifinite
 begin
 
 definition
diff -r 94170181a842 -r 67879e5d695c src/HOLCF/Tools/Domain/domain_axioms.ML
--- a/src/HOLCF/Tools/Domain/domain_axioms.ML	Tue Mar 02 22:13:39 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_axioms.ML	Wed Mar 03 09:33:46 2010 +0100
@@ -1,24 +1,22 @@
 (*  Title:      HOLCF/Tools/Domain/domain_axioms.ML
     Author:     David von Oheimb
+    Author:     Brian Huffman
 
 Syntax generator for domain command.
 *)
 
 signature DOMAIN_AXIOMS =
 sig
+  val axiomatize_isomorphism :
+      binding * (typ * typ) ->
+      theory -> Domain_Take_Proofs.iso_info * theory
+
   val copy_of_dtyp :
       string Symtab.table -> (int -> term) -> Datatype.dtyp -> term
 
-  val calc_axioms :
-      bool -> string Symtab.table ->
-      Domain_Library.eq list -> int -> Domain_Library.eq ->
-      string * (string * term) list * (string * term) list
-
   val add_axioms :
-      bool ->
-      ((string * typ list) *
-       (binding * (bool * binding option * typ) list * mixfix) list) list ->
-      Domain_Library.eq list -> theory -> theory
+      (binding * (typ * typ)) list ->
+      theory -> theory
 end;
 
 
@@ -33,9 +31,9 @@
 
 (* FIXME: use theory data for this *)
 val copy_tab : string Symtab.table =
-    Symtab.make [(@{type_name "->"}, @{const_name "cfun_map"}),
-                 (@{type_name "++"}, @{const_name "ssum_map"}),
-                 (@{type_name "**"}, @{const_name "sprod_map"}),
+    Symtab.make [(@{type_name cfun}, @{const_name "cfun_map"}),
+                 (@{type_name ssum}, @{const_name "ssum_map"}),
+                 (@{type_name sprod}, @{const_name "sprod_map"}),
                  (@{type_name "*"}, @{const_name "cprod_map"}),
                  (@{type_name "u"}, @{const_name "u_map"})];
 
@@ -48,39 +46,57 @@
       SOME f => list_ccomb (%%:f, map (copy_of_dtyp tab r) ds)
     | NONE => (warning ("copy_of_dtyp: unknown type constructor " ^ c); ID);
 
-fun calc_axioms
-    (definitional : bool)
-    (map_tab : string Symtab.table)
-    (eqs : eq list)
-    (n : int)
-    (eqn as ((dname,_),cons) : eq)
-    : string * (string * term) list * (string * term) list =
+local open HOLCF_Library in
+
+fun axiomatize_isomorphism
+    (dbind : binding, (lhsT, rhsT))
+    (thy : theory)
+    : Domain_Take_Proofs.iso_info * theory =
   let
+    val dname = Long_Name.base_name (Binding.name_of dbind);
 
-(* ----- axioms and definitions concerning the isomorphism ------------------ *)
+    val abs_bind = Binding.suffix_name "_abs" dbind;
+    val rep_bind = Binding.suffix_name "_rep" dbind;
 
-    val dc_abs = %%:(dname^"_abs");
-    val dc_rep = %%:(dname^"_rep");
-    val x_name'= "x";
-    val x_name = idx_name eqs x_name' (n+1);
-    val dnam = Long_Name.base_name dname;
+    val (abs_const, thy) =
+        Sign.declare_const ((abs_bind, rhsT ->> lhsT), NoSyn) thy;
+    val (rep_const, thy) =
+        Sign.declare_const ((rep_bind, lhsT ->> rhsT), NoSyn) thy;
+
+    val x = Free ("x", lhsT);
+    val y = Free ("y", rhsT);
+
+    val abs_iso_eqn =
+        Logic.all y (mk_trp (mk_eq (rep_const ` (abs_const ` y), y)));
+    val rep_iso_eqn =
+        Logic.all x (mk_trp (mk_eq (abs_const ` (rep_const ` x), x)));
 
-    val abs_iso_ax = ("abs_iso", mk_trp(dc_rep`(dc_abs`%x_name') === %:x_name'));
-    val rep_iso_ax = ("rep_iso", mk_trp(dc_abs`(dc_rep`%x_name') === %:x_name'));
+    val thy = Sign.add_path dname thy;
+
+    val (abs_iso_thm, thy) =
+        yield_singleton PureThy.add_axioms
+        ((Binding.name "abs_iso", abs_iso_eqn), []) thy;
 
-(* ----- axiom and definitions concerning induction ------------------------- *)
+    val (rep_iso_thm, thy) =
+        yield_singleton PureThy.add_axioms
+        ((Binding.name "rep_iso", rep_iso_eqn), []) thy;
+
+    val thy = Sign.parent_path thy;
 
-    val finite_def =
-        ("finite_def",
-         %%:(dname^"_finite") ==
-            mk_lam(x_name,
-                   mk_ex("n",(%%:(dname^"_take") $ Bound 0)`Bound 1 === Bound 1)));
+    val result =
+        {
+          absT = lhsT,
+          repT = rhsT,
+          abs_const = abs_const,
+          rep_const = rep_const,
+          abs_inverse = abs_iso_thm,
+          rep_inverse = rep_iso_thm
+        };
+  in
+    (result, thy)
+  end;
 
-  in (dnam,
-      (if definitional then [] else [abs_iso_ax, rep_iso_ax]),
-      [finite_def])
-  end; (* let (calc_axioms) *)
-
+end;
 
 (* legacy type inference *)
 
@@ -95,78 +111,46 @@
 fun add_axioms_i x = snd o PureThy.add_axioms (map (Thm.no_attributes o apfst Binding.name) x);
 fun add_axioms_infer axms thy = add_axioms_i (infer_props thy axms) thy;
 
-fun add_defs_i x = snd o (PureThy.add_defs false) (map (Thm.no_attributes o apfst Binding.name) x);
-fun add_defs_infer defs thy = add_defs_i (infer_props thy defs) thy;
-
-fun add_axioms definitional eqs' (eqs : eq list) thy' =
+fun add_axioms
+    (dom_eqns : (binding * (typ * typ)) list)
+    (thy : theory) =
   let
-    val dnames = map (fst o fst) eqs;
-    val x_name = idx_name dnames "x"; 
 
-    fun add_one (dnam, axs, dfs) =
+    (* declare and axiomatize abs/rep *)
+    val (iso_infos, thy) =
+        fold_map axiomatize_isomorphism dom_eqns thy;
+
+    fun add_one (dnam, axs) =
         Sign.add_path dnam
           #> add_axioms_infer axs
           #> Sign.parent_path;
 
-    val map_tab = Domain_Isomorphism.get_map_tab thy';
-    val axs = mapn (calc_axioms definitional map_tab eqs) 0 eqs;
-    val thy = thy' |> fold add_one axs;
-
-    fun get_iso_info ((dname, tyvars), cons') =
-      let
-        fun opt_lazy (lazy,_,t) = if lazy then mk_uT t else t
-        fun prod     (_,args,_) =
-            case args of [] => oneT
-                       | _ => foldr1 mk_sprodT (map opt_lazy args);
-        val ax_abs_iso = PureThy.get_thm thy (dname ^ ".abs_iso");
-        val ax_rep_iso = PureThy.get_thm thy (dname ^ ".rep_iso");
-        val lhsT = Type(dname,tyvars);
-        val rhsT = foldr1 mk_ssumT (map prod cons');
-        val rep_const = Const(dname^"_rep", lhsT ->> rhsT);
-        val abs_const = Const(dname^"_abs", rhsT ->> lhsT);
-      in
-        {
-          absT = lhsT,
-          repT = rhsT,
-          abs_const = abs_const,
-          rep_const = rep_const,
-          abs_inverse = ax_abs_iso,
-          rep_inverse = ax_rep_iso
-        }
-      end;
-    val dom_binds = map (Binding.name o Long_Name.base_name) dnames;
-    val thy =
-        if definitional then thy
-        else snd (Domain_Isomorphism.define_take_functions
-                    (dom_binds ~~ map get_iso_info eqs') thy);
-
-    fun add_one' (dnam, axs, dfs) =
-        Sign.add_path dnam
-          #> add_defs_infer dfs
-          #> Sign.parent_path;
-    val thy = fold add_one' axs thy;
+    (* define take function *)
+    val (take_info, thy) =
+        Domain_Take_Proofs.define_take_functions
+          (map fst dom_eqns ~~ iso_infos) thy;
 
     (* declare lub_take axioms *)
     local
-      fun ax_lub_take dname =
+      fun ax_lub_take (dbind, take_const) =
         let
-          val dnam : string = Long_Name.base_name dname;
-          val take_const = %%:(dname^"_take");
+          val dnam = Long_Name.base_name (Binding.name_of dbind);
           val lub = %%: @{const_name lub};
           val image = %%: @{const_name image};
           val UNIV = @{term "UNIV :: nat set"};
           val lhs = lub $ (image $ take_const $ UNIV);
           val ax = mk_trp (lhs === ID);
         in
-          add_one (dnam, [("lub_take", ax)], [])
+          add_one (dnam, [("lub_take", ax)])
         end
+      val dbinds = map fst dom_eqns;
+      val take_consts = #take_consts take_info;
     in
-      val thy =
-          if definitional then thy
-          else fold ax_lub_take dnames thy
+      val thy = fold ax_lub_take (dbinds ~~ take_consts) thy
     end;
+
   in
-    thy
-  end; (* let (add_axioms) *)
+    thy (* TODO: also return iso_infos, take_info, lub_take_thms *)
+  end;
 
 end; (* struct *)
diff -r 94170181a842 -r 67879e5d695c src/HOLCF/Tools/Domain/domain_constructors.ML
--- a/src/HOLCF/Tools/Domain/domain_constructors.ML	Tue Mar 02 22:13:39 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_constructors.ML	Wed Mar 03 09:33:46 2010 +0100
@@ -10,7 +10,7 @@
   val add_domain_constructors :
       string
       -> (binding * (bool * binding option * typ) list * mixfix) list
-      -> Domain_Isomorphism.iso_info
+      -> Domain_Take_Proofs.iso_info
       -> theory
       -> { con_consts : term list,
            con_betas : thm list,
@@ -190,15 +190,15 @@
       val thm2 = rewrite_rule (map mk_meta_eq @{thms ex_defined_iffs}) thm1;
       val thm3 = rewrite_rule [mk_meta_eq @{thm conj_assoc}] thm2;
 
-      val x = Free ("x", lhsT);
+      val y = Free ("y", lhsT);
       fun one_con (con, args) =
         let
-          val (vs, nonlazy) = get_vars_avoiding ["x"] args;
-          val eqn = mk_eq (x, list_ccomb (con, vs));
+          val (vs, nonlazy) = get_vars_avoiding ["y"] args;
+          val eqn = mk_eq (y, list_ccomb (con, vs));
           val conj = foldr1 mk_conj (eqn :: map mk_defined nonlazy);
         in Library.foldr mk_ex (vs, conj) end;
-      val goal = mk_trp (foldr1 mk_disj (mk_undef x :: map one_con spec'));
-      (* first 3 rules replace "x = UU \/ P" with "rep$x = UU \/ P" *)
+      val goal = mk_trp (foldr1 mk_disj (mk_undef y :: map one_con spec'));
+      (* first 3 rules replace "y = UU \/ P" with "rep$y = UU \/ P" *)
       val tacs = [
           rtac (iso_locale RS @{thm iso.casedist_rule}) 1,
           rewrite_goals_tac [mk_meta_eq (iso_locale RS @{thm iso.iso_swap})],
@@ -1011,7 +1011,7 @@
 fun add_domain_constructors
     (dname : string)
     (spec : (binding * (bool * binding option * typ) list * mixfix) list)
-    (iso_info : Domain_Isomorphism.iso_info)
+    (iso_info : Domain_Take_Proofs.iso_info)
     (thy : theory) =
   let
 
diff -r 94170181a842 -r 67879e5d695c src/HOLCF/Tools/Domain/domain_extender.ML
--- a/src/HOLCF/Tools/Domain/domain_extender.ML	Tue Mar 02 22:13:39 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_extender.ML	Wed Mar 03 09:33:46 2010 +0100
@@ -79,7 +79,9 @@
           | rm_sorts (Type(s,ts)) = Type(s,remove_sorts ts)
           | rm_sorts (TVar(s,_))  = TVar(s,[])
         and remove_sorts l = map rm_sorts l;
-        val indirect_ok = ["*","Cfun.->","Ssum.++","Sprod.**","Up.u"]
+        val indirect_ok =
+            [@{type_name "*"}, @{type_name cfun}, @{type_name ssum},
+             @{type_name sprod}, @{type_name u}];
         fun analyse indirect (TFree(v,s))  =
             (case AList.lookup (op =) tvars v of 
                NONE => error ("Free type variable " ^ quote v ^ " on rhs.")
@@ -127,44 +129,63 @@
     (comp_dnam : string)
     (eqs''' : ((string * string option) list * binding * mixfix *
                (binding * (bool * binding option * 'a) list * mixfix) list) list)
-    (thy''' : theory) =
+    (thy : theory) =
   let
-    fun readS (SOME s) = Syntax.read_sort_global thy''' s
-      | readS NONE = Sign.defaultS thy''';
-    fun readTFree (a, s) = TFree (a, readS s);
+    val dtnvs : (binding * typ list * mixfix) list =
+      let
+        fun readS (SOME s) = Syntax.read_sort_global thy s
+          | readS NONE = Sign.defaultS thy;
+        fun readTFree (a, s) = TFree (a, readS s);
+      in
+        map (fn (vs,dname:binding,mx,_) =>
+                (dname, map readTFree vs, mx)) eqs'''
+      end;
 
-    val dtnvs = map (fn (vs,dname:binding,mx,_) => 
-                        (dname, map readTFree vs, mx)) eqs''';
-    val cons''' = map (fn (_,_,_,cons) => cons) eqs''';
-    fun thy_type  (dname,tvars,mx) = (dname, length tvars, mx);
-    fun thy_arity (dname,tvars,mx) =
-        (Sign.full_name thy''' dname, map (snd o dest_TFree) tvars, pcpoS);
-    val thy'' =
-      thy'''
-      |> Sign.add_types (map thy_type dtnvs)
-      |> fold (AxClass.axiomatize_arity o thy_arity) dtnvs;
-    val cons'' =
-      map (map (upd_second (map (upd_third (prep_typ thy''))))) cons''';
-    val dtnvs' =
-      map (fn (dname,vs,mx) => (Sign.full_name thy''' dname,vs)) dtnvs;
+    (* declare new types *)
+    val thy =
+      let
+        fun thy_type  (dname,tvars,mx) = (dname, length tvars, mx);
+        fun thy_arity (dname,tvars,mx) =
+            (Sign.full_name thy dname, map (snd o dest_TFree) tvars, pcpoS);
+      in
+        thy
+          |> Sign.add_types (map thy_type dtnvs)
+          |> fold (AxClass.axiomatize_arity o thy_arity) dtnvs
+      end;
+
+    val dbinds : binding list =
+        map (fn (_,dbind,_,_) => dbind) eqs''';
+    val cons''' :
+        (binding * (bool * binding option * 'a) list * mixfix) list list =
+        map (fn (_,_,_,cons) => cons) eqs''';
+    val cons'' :
+        (binding * (bool * binding option * typ) list * mixfix) list list =
+        map (map (upd_second (map (upd_third (prep_typ thy))))) cons''';
+    val dtnvs' : (string * typ list) list =
+      map (fn (dname,vs,mx) => (Sign.full_name thy dname,vs)) dtnvs;
     val eqs' : ((string * typ list) *
         (binding * (bool * binding option * typ) list * mixfix) list) list =
-      check_and_sort_domain false dtnvs' cons'' thy'';
-    val thy' = thy'' |> Domain_Syntax.add_syntax false eqs';
-    val dts  = map (Type o fst) eqs';
-    val new_dts = map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
-    fun strip ss = drop (find_index (fn s => s = "'") ss + 1) ss;
-    fun one_con (con,args,mx) =
+        check_and_sort_domain false dtnvs' cons'' thy;
+(*    val thy = Domain_Syntax.add_syntax eqs' thy; *)
+    val dts : typ list = map (Type o fst) eqs';
+    val new_dts : (string * string list) list =
+        map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
+    fun one_con (con,args,mx) : cons =
         (Binding.name_of con,  (* FIXME preverse binding (!?) *)
-         mx,
          ListPair.map (fn ((lazy,sel,tp),vn) =>
-           mk_arg ((lazy, Datatype_Aux.dtyp_of_typ new_dts tp),
-                   Option.map Binding.name_of sel,vn))
-                      (args, Datatype_Prop.make_tnames (map third args))
-        ) : cons;
+           mk_arg ((lazy, Datatype_Aux.dtyp_of_typ new_dts tp), vn))
+                      (args, Datatype_Prop.make_tnames (map third args)));
     val eqs : eq list =
         map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs';
-    val thy = thy' |> Domain_Axioms.add_axioms false eqs' eqs;
+
+    fun mk_arg_typ (lazy, dest_opt, T) = if lazy then mk_uT T else T;
+    fun mk_con_typ (bind, args, mx) =
+        if null args then oneT else foldr1 mk_sprodT (map mk_arg_typ args);
+    fun mk_eq_typ (_, cons) = foldr1 mk_ssumT (map mk_con_typ cons);
+    val repTs : typ list = map mk_eq_typ eqs';
+    val dom_eqns : (binding * (typ * typ)) list = dbinds ~~ (dts ~~ repTs);
+    val thy = Domain_Axioms.add_axioms dom_eqns thy;
+
     val ((rewss, take_rews), theorems_thy) =
         thy
           |> fold_map (fn (eq, (x,cs)) =>
@@ -185,59 +206,62 @@
     (comp_dnam : string)
     (eqs''' : ((string * string option) list * binding * mixfix *
                (binding * (bool * binding option * 'a) list * mixfix) list) list)
-    (thy''' : theory) =
+    (thy : theory) =
   let
-    fun readS (SOME s) = Syntax.read_sort_global thy''' s
-      | readS NONE = Sign.defaultS thy''';
-    fun readTFree (a, s) = TFree (a, readS s);
+    val dtnvs : (binding * typ list * mixfix) list =
+      let
+        fun readS (SOME s) = Syntax.read_sort_global thy s
+          | readS NONE = Sign.defaultS thy;
+        fun readTFree (a, s) = TFree (a, readS s);
+      in
+        map (fn (vs,dname:binding,mx,_) =>
+                (dname, map readTFree vs, mx)) eqs'''
+      end;
 
-    val dtnvs = map (fn (vs,dname:binding,mx,_) => 
-                        (dname, map readTFree vs, mx)) eqs''';
-    val cons''' = map (fn (_,_,_,cons) => cons) eqs''';
     fun thy_type  (dname,tvars,mx) = (dname, length tvars, mx);
     fun thy_arity (dname,tvars,mx) =
-      (Sign.full_name thy''' dname, map (snd o dest_TFree) tvars, @{sort rep});
+      (Sign.full_name thy dname, map (snd o dest_TFree) tvars, @{sort rep});
 
     (* this theory is used just for parsing and error checking *)
-    val tmp_thy = thy'''
+    val tmp_thy = thy
       |> Theory.copy
       |> Sign.add_types (map thy_type dtnvs)
       |> fold (AxClass.axiomatize_arity o thy_arity) dtnvs;
 
-    val cons'' : (binding * (bool * binding option * typ) list * mixfix) list list =
-      map (map (upd_second (map (upd_third (prep_typ tmp_thy))))) cons''';
+    val cons''' :
+        (binding * (bool * binding option * 'a) list * mixfix) list list =
+        map (fn (_,_,_,cons) => cons) eqs''';
+    val cons'' :
+        (binding * (bool * binding option * typ) list * mixfix) list list =
+        map (map (upd_second (map (upd_third (prep_typ tmp_thy))))) cons''';
     val dtnvs' : (string * typ list) list =
-      map (fn (dname,vs,mx) => (Sign.full_name thy''' dname,vs)) dtnvs;
+        map (fn (dname,vs,mx) => (Sign.full_name thy dname,vs)) dtnvs;
     val eqs' : ((string * typ list) *
         (binding * (bool * binding option * typ) list * mixfix) list) list =
-      check_and_sort_domain true dtnvs' cons'' tmp_thy;
+        check_and_sort_domain true dtnvs' cons'' tmp_thy;
 
     fun mk_arg_typ (lazy, dest_opt, T) = if lazy then mk_uT T else T;
     fun mk_con_typ (bind, args, mx) =
         if null args then oneT else foldr1 mk_sprodT (map mk_arg_typ args);
     fun mk_eq_typ (_, cons) = foldr1 mk_ssumT (map mk_con_typ cons);
     
-    val (iso_infos, thy'') = thy''' |>
+    val (iso_infos, thy) = thy |>
       Domain_Isomorphism.domain_isomorphism
         (map (fn ((vs, dname, mx, _), eq) =>
                  (map fst vs, dname, mx, mk_eq_typ eq, NONE))
              (eqs''' ~~ eqs'))
 
-    val thy' = thy'' |> Domain_Syntax.add_syntax true eqs';
-    val dts  = map (Type o fst) eqs';
-    val new_dts = map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
-    fun strip ss = drop (find_index (fn s => s = "'") ss + 1) ss;
-    fun one_con (con,args,mx) =
+    val dts : typ list = map (Type o fst) eqs';
+    val new_dts : (string * string list) list =
+        map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
+    fun one_con (con,args,mx) : cons =
         (Binding.name_of con,   (* FIXME preverse binding (!?) *)
-         mx,
          ListPair.map (fn ((lazy,sel,tp),vn) =>
-           mk_arg ((lazy, Datatype_Aux.dtyp_of_typ new_dts tp),
-                   Option.map Binding.name_of sel,vn))
+           mk_arg ((lazy, Datatype_Aux.dtyp_of_typ new_dts tp), vn))
                       (args, Datatype_Prop.make_tnames (map third args))
-        ) : cons;
+        );
     val eqs : eq list =
         map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs';
-    val thy = thy' |> Domain_Axioms.add_axioms true eqs' eqs;
     val ((rewss, take_rews), theorems_thy) =
         thy
           |> fold_map (fn (eq, (x,cs)) =>
diff -r 94170181a842 -r 67879e5d695c src/HOLCF/Tools/Domain/domain_isomorphism.ML
--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Tue Mar 02 22:13:39 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Wed Mar 03 09:33:46 2010 +0100
@@ -6,37 +6,17 @@
 
 signature DOMAIN_ISOMORPHISM =
 sig
-  type iso_info =
-    {
-      repT : typ,
-      absT : typ,
-      rep_const : term,
-      abs_const : term,
-      rep_inverse : thm,
-      abs_inverse : thm
-    }
   val domain_isomorphism :
     (string list * binding * mixfix * typ * (binding * binding) option) list
-      -> theory -> iso_info list * theory
+      -> theory -> Domain_Take_Proofs.iso_info list * theory
   val domain_isomorphism_cmd :
     (string list * binding * mixfix * string * (binding * binding) option) list
       -> theory -> theory
   val add_type_constructor :
     (string * term * string * thm  * thm * thm * thm) -> theory -> theory
-  val get_map_tab :
-    theory -> string Symtab.table
-  val define_take_functions :
-    (binding * iso_info) list -> theory ->
-    { take_consts : term list,
-      take_defs : thm list,
-      chain_take_thms : thm list,
-      take_0_thms : thm list,
-      take_Suc_thms : thm list,
-      deflation_take_thms : thm list
-    } * theory;
 end;
 
-structure Domain_Isomorphism :> DOMAIN_ISOMORPHISM =
+structure Domain_Isomorphism : DOMAIN_ISOMORPHISM =
 struct
 
 val beta_ss =
@@ -53,47 +33,51 @@
 
 structure DeflData = Theory_Data
 (
+  (* terms like "foo_defl" *)
   type T = term Symtab.table;
   val empty = Symtab.empty;
   val extend = I;
   fun merge data = Symtab.merge (K true) data;
 );
 
-structure MapData = Theory_Data
+structure RepData = Theory_Data
 (
-  type T = string Symtab.table;
-  val empty = Symtab.empty;
-  val extend = I;
-  fun merge data = Symtab.merge (K true) data;
-);
-
-structure Thm_List : THEORY_DATA_ARGS =
-struct
+  (* theorems like "REP('a foo) = foo_defl$REP('a)" *)
   type T = thm list;
   val empty = [];
   val extend = I;
   val merge = Thm.merge_thms;
-end;
-
-structure RepData = Theory_Data (Thm_List);
+);
 
-structure IsodeflData = Theory_Data (Thm_List);
+structure MapIdData = Theory_Data
+(
+  (* theorems like "foo_map$ID = ID" *)
+  type T = thm list;
+  val empty = [];
+  val extend = I;
+  val merge = Thm.merge_thms;
+);
 
-structure MapIdData = Theory_Data (Thm_List);
-
-structure DeflMapData = Theory_Data (Thm_List);
+structure IsodeflData = Theory_Data
+(
+  (* theorems like "isodefl d t ==> isodefl (foo_map$d) (foo_defl$t)" *)
+  type T = thm list;
+  val empty = [];
+  val extend = I;
+  val merge = Thm.merge_thms;
+);
 
 fun add_type_constructor
   (tname, defl_const, map_name, REP_thm,
    isodefl_thm, map_ID_thm, defl_map_thm) =
     DeflData.map (Symtab.insert (K true) (tname, defl_const))
-    #> MapData.map (Symtab.insert (K true) (tname, map_name))
+    #> Domain_Take_Proofs.add_map_function (tname, map_name, defl_map_thm)
     #> RepData.map (Thm.add_thm REP_thm)
     #> IsodeflData.map (Thm.add_thm isodefl_thm)
-    #> MapIdData.map (Thm.add_thm map_ID_thm)
-    #> DeflMapData.map (Thm.add_thm defl_map_thm);
+    #> MapIdData.map (Thm.add_thm map_ID_thm);
 
-val get_map_tab = MapData.get;
+
+(* val get_map_tab = MapData.get; *)
 
 
 (******************************************************************************)
@@ -142,17 +126,7 @@
 (****************************** isomorphism info ******************************)
 (******************************************************************************)
 
-type iso_info =
-  {
-    absT : typ,
-    repT : typ,
-    abs_const : term,
-    rep_const : term,
-    abs_inverse : thm,
-    rep_inverse : thm
-  }
-
-fun deflation_abs_rep (info : iso_info) : thm =
+fun deflation_abs_rep (info : Domain_Take_Proofs.iso_info) : thm =
   let
     val abs_iso = #abs_inverse info;
     val rep_iso = #rep_inverse info;
@@ -250,22 +224,6 @@
                   else error ("defl_of_typ: type variable under unsupported type constructor " ^ c);
   in defl_of T end;
 
-fun map_of_typ
-    (tab : string Symtab.table)
-    (T : typ) : term =
-  let
-    fun is_closed_typ (Type (_, Ts)) = forall is_closed_typ Ts
-      | is_closed_typ _ = false;
-    fun map_of (T as TFree (a, _)) = Free (Library.unprefix "'" a, T ->> T)
-      | map_of (T as TVar _) = error ("map_of_typ: TVar")
-      | map_of (T as Type (c, Ts)) =
-        case Symtab.lookup tab c of
-          SOME t => list_ccomb (Const (t, mapT T), map map_of Ts)
-        | NONE => if is_closed_typ T
-                  then mk_ID T
-                  else error ("map_of_typ: type variable under unsupported type constructor " ^ c);
-  in map_of T end;
-
 
 (******************************************************************************)
 (********************* declaring definitions and theorems *********************)
@@ -293,217 +251,6 @@
     ||> Sign.parent_path;
 
 (******************************************************************************)
-(************************** defining take functions ***************************)
-(******************************************************************************)
-
-fun define_take_functions
-    (spec : (binding * iso_info) list)
-    (thy : theory) =
-  let
-
-    (* retrieve components of spec *)
-    val dom_binds = map fst spec;
-    val iso_infos = map snd spec;
-    val dom_eqns = map (fn x => (#absT x, #repT x)) iso_infos;
-    val rep_abs_consts = map (fn x => (#rep_const x, #abs_const x)) iso_infos;
-    val dnames = map Binding.name_of dom_binds;
-
-    (* get table of map functions *)
-    val map_tab = MapData.get thy;
-
-    fun mk_projs []      t = []
-      | mk_projs (x::[]) t = [(x, t)]
-      | mk_projs (x::xs) t = (x, mk_fst t) :: mk_projs xs (mk_snd t);
-
-    fun mk_cfcomp2 ((rep_const, abs_const), f) =
-        mk_cfcomp (abs_const, mk_cfcomp (f, rep_const));
-
-    (* defining map functions over dtyps *)
-    fun copy_of_dtyp recs (T, dt) =
-        if Datatype_Aux.is_rec_type dt
-        then copy_of_dtyp' recs (T, dt)
-        else mk_ID T
-    and copy_of_dtyp' recs (T, Datatype_Aux.DtRec i) = nth recs i
-      | copy_of_dtyp' recs (T, Datatype_Aux.DtTFree a) = mk_ID T
-      | copy_of_dtyp' recs (T, Datatype_Aux.DtType (c, ds)) =
-        case Symtab.lookup map_tab c of
-          SOME f =>
-          list_ccomb
-            (Const (f, mapT T),
-             map (copy_of_dtyp recs) (snd (dest_Type T) ~~ ds))
-        | NONE =>
-          (warning ("copy_of_dtyp: unknown type constructor " ^ c); mk_ID T);
-
-    (* define take functional *)
-    val new_dts : (string * string list) list =
-      map (apsnd (map (fst o dest_TFree)) o dest_Type o fst) dom_eqns;
-    val copy_arg_type = mk_tupleT (map (fn (T, _) => T ->> T) dom_eqns);
-    val copy_arg = Free ("f", copy_arg_type);
-    val copy_args = map snd (mk_projs dom_binds copy_arg);
-    fun one_copy_rhs (rep_abs, (lhsT, rhsT)) =
-      let
-        val dtyp = Datatype_Aux.dtyp_of_typ new_dts rhsT;
-        val body = copy_of_dtyp copy_args (rhsT, dtyp);
-      in
-        mk_cfcomp2 (rep_abs, body)
-      end;
-    val take_functional =
-        big_lambda copy_arg
-          (mk_tuple (map one_copy_rhs (rep_abs_consts ~~ dom_eqns)));
-    val take_rhss =
-      let
-        val i = Free ("i", HOLogic.natT);
-        val rhs = mk_iterate (i, take_functional)
-      in
-        map (Term.lambda i o snd) (mk_projs dom_binds rhs)
-      end;
-
-    (* define take constants *)
-    fun define_take_const ((tbind, take_rhs), (lhsT, rhsT)) thy =
-      let
-        val take_type = HOLogic.natT --> lhsT ->> lhsT;
-        val take_bind = Binding.suffix_name "_take" tbind;
-        val (take_const, thy) =
-          Sign.declare_const ((take_bind, take_type), NoSyn) thy;
-        val take_eqn = Logic.mk_equals (take_const, take_rhs);
-        val (take_def_thm, thy) =
-          thy
-          |> Sign.add_path (Binding.name_of tbind)
-          |> yield_singleton
-              (PureThy.add_defs false o map Thm.no_attributes)
-              (Binding.name "take_def", take_eqn)
-          ||> Sign.parent_path;
-      in ((take_const, take_def_thm), thy) end;
-    val ((take_consts, take_defs), thy) = thy
-      |> fold_map define_take_const (dom_binds ~~ take_rhss ~~ dom_eqns)
-      |>> ListPair.unzip;
-
-    (* prove chain_take lemmas *)
-    fun prove_chain_take (take_const, dname) thy =
-      let
-        val goal = mk_trp (mk_chain take_const);
-        val rules = take_defs @ @{thms chain_iterate ch2ch_fst ch2ch_snd};
-        val tac = simp_tac (HOL_basic_ss addsimps rules) 1;
-        val chain_take_thm = Goal.prove_global thy [] [] goal (K tac);
-      in
-        add_qualified_thm "chain_take" (dname, chain_take_thm) thy
-      end;
-    val (chain_take_thms, thy) =
-      fold_map prove_chain_take (take_consts ~~ dnames) thy;
-
-    (* prove take_0 lemmas *)
-    fun prove_take_0 ((take_const, dname), (lhsT, rhsT)) thy =
-      let
-        val lhs = take_const $ @{term "0::nat"};
-        val goal = mk_eqs (lhs, mk_bottom (lhsT ->> lhsT));
-        val rules = take_defs @ @{thms iterate_0 fst_strict snd_strict};
-        val tac = simp_tac (HOL_basic_ss addsimps rules) 1;
-        val take_0_thm = Goal.prove_global thy [] [] goal (K tac);
-      in
-        add_qualified_thm "take_0" (dname, take_0_thm) thy
-      end;
-    val (take_0_thms, thy) =
-      fold_map prove_take_0 (take_consts ~~ dnames ~~ dom_eqns) thy;
-
-    (* prove take_Suc lemmas *)
-    val i = Free ("i", natT);
-    val take_is = map (fn t => t $ i) take_consts;
-    fun prove_take_Suc
-          (((take_const, rep_abs), dname), (lhsT, rhsT)) thy =
-      let
-        val lhs = take_const $ (@{term Suc} $ i);
-        val dtyp = Datatype_Aux.dtyp_of_typ new_dts rhsT;
-        val body = copy_of_dtyp take_is (rhsT, dtyp);
-        val rhs = mk_cfcomp2 (rep_abs, body);
-        val goal = mk_eqs (lhs, rhs);
-        val simps = @{thms iterate_Suc fst_conv snd_conv}
-        val rules = take_defs @ simps;
-        val tac = simp_tac (beta_ss addsimps rules) 1;
-        val take_Suc_thm = Goal.prove_global thy [] [] goal (K tac);
-      in
-        add_qualified_thm "take_Suc" (dname, take_Suc_thm) thy
-      end;
-    val (take_Suc_thms, thy) =
-      fold_map prove_take_Suc
-        (take_consts ~~ rep_abs_consts ~~ dnames ~~ dom_eqns) thy;
-
-    (* prove deflation theorems for take functions *)
-    val deflation_abs_rep_thms = map deflation_abs_rep iso_infos;
-    val deflation_take_thm =
-      let
-        val i = Free ("i", natT);
-        fun mk_goal take_const = mk_deflation (take_const $ i);
-        val goal = mk_trp (foldr1 mk_conj (map mk_goal take_consts));
-        val adm_rules =
-          @{thms adm_conj adm_subst [OF _ adm_deflation]
-                 cont2cont_fst cont2cont_snd cont_id};
-        val bottom_rules =
-          take_0_thms @ @{thms deflation_UU simp_thms};
-        val deflation_rules =
-          @{thms conjI deflation_ID}
-          @ deflation_abs_rep_thms
-          @ DeflMapData.get thy;
-      in
-        Goal.prove_global thy [] [] goal (fn _ =>
-         EVERY
-          [rtac @{thm nat.induct} 1,
-           simp_tac (HOL_basic_ss addsimps bottom_rules) 1,
-           asm_simp_tac (HOL_basic_ss addsimps take_Suc_thms) 1,
-           REPEAT (etac @{thm conjE} 1
-                   ORELSE resolve_tac deflation_rules 1
-                   ORELSE atac 1)])
-      end;
-    fun conjuncts [] thm = []
-      | conjuncts (n::[]) thm = [(n, thm)]
-      | conjuncts (n::ns) thm = let
-          val thmL = thm RS @{thm conjunct1};
-          val thmR = thm RS @{thm conjunct2};
-        in (n, thmL):: conjuncts ns thmR end;
-    val (deflation_take_thms, thy) =
-      fold_map (add_qualified_thm "deflation_take")
-        (map (apsnd Drule.export_without_context)
-          (conjuncts dnames deflation_take_thm)) thy;
-
-    (* prove strictness of take functions *)
-    fun prove_take_strict (take_const, dname) thy =
-      let
-        val goal = mk_trp (mk_strict (take_const $ Free ("i", natT)));
-        val tac = rtac @{thm deflation_strict} 1
-                  THEN resolve_tac deflation_take_thms 1;
-        val take_strict_thm = Goal.prove_global thy [] [] goal (K tac);
-      in
-        add_qualified_thm "take_strict" (dname, take_strict_thm) thy
-      end;
-    val (take_strict_thms, thy) =
-      fold_map prove_take_strict (take_consts ~~ dnames) thy;
-
-    (* prove take/take rules *)
-    fun prove_take_take ((chain_take, deflation_take), dname) thy =
-      let
-        val take_take_thm =
-            @{thm deflation_chain_min} OF [chain_take, deflation_take];
-      in
-        add_qualified_thm "take_take" (dname, take_take_thm) thy
-      end;
-    val (take_take_thms, thy) =
-      fold_map prove_take_take
-        (chain_take_thms ~~ deflation_take_thms ~~ dnames) thy;
-
-    val result =
-      {
-        take_consts = take_consts,
-        take_defs = take_defs,
-        chain_take_thms = chain_take_thms,
-        take_0_thms = take_0_thms,
-        take_Suc_thms = take_Suc_thms,
-        deflation_take_thms = deflation_take_thms
-      };
-
-  in
-    (result, thy)
-  end;
-
-(******************************************************************************)
 (******************************* main function ********************************)
 (******************************************************************************)
 
@@ -529,7 +276,7 @@
     (prep_typ: theory -> 'a -> (string * sort) list -> typ * (string * sort) list)
     (doms_raw: (string list * binding * mixfix * 'a * (binding * binding) option) list)
     (thy: theory)
-    : iso_info list * theory =
+    : Domain_Take_Proofs.iso_info list * theory =
   let
     val _ = Theory.requires thy "Representable" "domain isomorphisms";
 
@@ -669,7 +416,7 @@
       |>> ListPair.unzip;
 
     (* collect info about rep/abs *)
-    val iso_infos : iso_info list =
+    val iso_infos : Domain_Take_Proofs.iso_info list =
       let
         fun mk_info (((lhsT, rhsT), (repC, absC)), (rep_iso, abs_iso)) =
           {
@@ -696,19 +443,24 @@
       fold_map declare_map_const (dom_binds ~~ dom_eqns);
 
     (* defining equations for map functions *)
-    val map_tab1 = MapData.get thy;
-    val map_tab2 =
-      Symtab.make (map (fst o dest_Type o fst) dom_eqns
-                   ~~ map (fst o dest_Const) map_consts);
-    val map_tab' = Symtab.merge (K true) (map_tab1, map_tab2);
-    val thy = MapData.put map_tab' thy;
-    fun mk_map_spec ((rep_const, abs_const), (lhsT, rhsT)) =
-      let
-        val lhs = map_of_typ map_tab' lhsT;
-        val body = map_of_typ map_tab' rhsT;
-        val rhs = mk_cfcomp (abs_const, mk_cfcomp (body, rep_const));
-      in mk_eqs (lhs, rhs) end;
-    val map_specs = map mk_map_spec (rep_abs_consts ~~ dom_eqns);
+    local
+      fun unprime a = Library.unprefix "'" a;
+      fun mapvar T = Free (unprime (fst (dest_TFree T)), T ->> T);
+      fun map_lhs (map_const, lhsT) =
+          (lhsT, list_ccomb (map_const, map mapvar (snd (dest_Type lhsT))));
+      val tab1 = map map_lhs (map_consts ~~ map fst dom_eqns);
+      val Ts = (snd o dest_Type o fst o hd) dom_eqns;
+      val tab = (Ts ~~ map mapvar Ts) @ tab1;
+      fun mk_map_spec (((rep_const, abs_const), map_const), (lhsT, rhsT)) =
+        let
+          val lhs = Domain_Take_Proofs.map_of_typ thy tab lhsT;
+          val body = Domain_Take_Proofs.map_of_typ thy tab rhsT;
+          val rhs = mk_cfcomp (abs_const, mk_cfcomp (body, rep_const));
+        in mk_eqs (lhs, rhs) end;
+    in
+      val map_specs =
+          map mk_map_spec (rep_abs_consts ~~ map_consts ~~ dom_eqns);
+    end;
 
     (* register recursive definition of map functions *)
     val map_binds = map (Binding.suffix_name "_map") dom_binds;
@@ -816,7 +568,7 @@
         val deflation_rules =
           @{thms conjI deflation_ID}
           @ deflation_abs_rep_thms
-          @ DeflMapData.get thy;
+          @ Domain_Take_Proofs.get_deflation_thms thy;
       in
         Goal.prove_global thy [] assms goal (fn {prems, ...} =>
          EVERY
@@ -834,13 +586,25 @@
     val (deflation_map_thms, thy) = thy |>
       (PureThy.add_thms o map (Thm.no_attributes o apsnd Drule.export_without_context))
         (conjuncts deflation_map_binds deflation_map_thm);
-    val thy = DeflMapData.map (fold Thm.add_thm deflation_map_thms) thy;
+
+    (* register map functions in theory data *)
+    local
+      fun register_map ((dname, map_name), defl_thm) =
+          Domain_Take_Proofs.add_map_function (dname, map_name, defl_thm);
+      val dnames = map (fst o dest_Type o fst) dom_eqns;
+      val map_names = map (fst o dest_Const) map_consts;
+    in
+      val thy =
+          fold register_map (dnames ~~ map_names ~~ deflation_map_thms) thy;
+    end;
 
     (* definitions and proofs related to take functions *)
     val (take_info, thy) =
-      define_take_functions (dom_binds ~~ iso_infos) thy;
-    val {take_consts, take_defs, chain_take_thms, take_0_thms,
-         take_Suc_thms, deflation_take_thms} = take_info;
+        Domain_Take_Proofs.define_take_functions
+          (dom_binds ~~ iso_infos) thy;
+    val { take_consts, take_defs, chain_take_thms, take_0_thms,
+          take_Suc_thms, deflation_take_thms,
+          finite_consts, finite_defs } = take_info;
 
     (* least-upper-bound lemma for take functions *)
     val lub_take_lemma =
diff -r 94170181a842 -r 67879e5d695c src/HOLCF/Tools/Domain/domain_library.ML
--- a/src/HOLCF/Tools/Domain/domain_library.ML	Tue Mar 02 22:13:39 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_library.ML	Wed Mar 03 09:33:46 2010 +0100
@@ -93,13 +93,12 @@
 
       (* Domain specifications *)
       eqtype arg;
-  type cons = string * mixfix * arg list;
+  type cons = string * arg list;
   type eq = (string * typ list) * cons list;
-  val mk_arg : (bool * Datatype.dtyp) * string option * string -> arg;
+  val mk_arg : (bool * Datatype.dtyp) * string -> arg;
   val is_lazy : arg -> bool;
   val rec_of : arg -> int;
   val dtyp_of : arg -> Datatype.dtyp;
-  val sel_of : arg -> string option;
   val vname : arg -> string;
   val upd_vname : (string -> string) -> arg -> arg;
   val is_rec : arg -> bool;
@@ -108,8 +107,6 @@
   val nonlazy_rec : arg list -> string list;
   val %# : arg -> term;
   val /\# : arg * term -> term;
-  val when_body : cons list -> (int * int -> term) -> term;
-  val when_funs : 'a list -> string list;
   val bound_arg : ''a list -> ''a -> term; (* ''a = arg or string *)
   val idx_name : 'a list -> string -> int -> string;
   val app_rec_arg : (int -> term) -> arg -> term;
@@ -186,12 +183,10 @@
 
 type arg =
      (bool * Datatype.dtyp) *   (*  (lazy, recursive element) *)
-     string option *               (*   selector name    *)
      string;                       (*   argument name    *)
 
 type cons =
      string *         (* operator name of constr *)
-     mixfix *         (* mixfix syntax of constructor *)
      arg list;        (* argument list      *)
 
 type eq =
@@ -201,15 +196,14 @@
 
 val mk_arg = I;
 
-fun rec_of ((_,dtyp),_,_) =
+fun rec_of ((_,dtyp),_) =
     case dtyp of Datatype_Aux.DtRec i => i | _ => ~1;
 (* FIXME: what about indirect recursion? *)
 
-fun is_lazy arg = fst (first arg);
-fun dtyp_of arg = snd (first arg);
-val sel_of    =       second;
-val     vname =       third;
-val upd_vname =   upd_third;
+fun is_lazy arg = fst (fst arg);
+fun dtyp_of arg = snd (fst arg);
+val     vname =       snd;
+val upd_vname =   apsnd;
 fun is_rec         arg = rec_of arg >=0;
 fun is_nonlazy_rec arg = is_rec arg andalso not (is_lazy arg);
 fun nonlazy     args   = map vname (filter_out is_lazy args);
@@ -219,8 +213,8 @@
 (* ----- combinators for making dtyps ----- *)
 
 fun mk_uD T = Datatype_Aux.DtType(@{type_name "u"}, [T]);
-fun mk_sprodD (T, U) = Datatype_Aux.DtType(@{type_name "**"}, [T, U]);
-fun mk_ssumD (T, U) = Datatype_Aux.DtType(@{type_name "++"}, [T, U]);
+fun mk_sprodD (T, U) = Datatype_Aux.DtType(@{type_name sprod}, [T, U]);
+fun mk_ssumD (T, U) = Datatype_Aux.DtType(@{type_name ssum}, [T, U]);
 fun mk_liftD T = Datatype_Aux.DtType(@{type_name "lift"}, [T]);
 val unitD = Datatype_Aux.DtType(@{type_name "unit"}, []);
 val boolD = Datatype_Aux.DtType(@{type_name "bool"}, []);
@@ -229,17 +223,17 @@
 fun big_sprodD ds = case ds of [] => oneD | _ => foldr1 mk_sprodD ds;
 fun big_ssumD ds = case ds of [] => unitD | _ => foldr1 mk_ssumD ds;
 
-fun dtyp_of_arg ((lazy, D), _, _) = if lazy then mk_uD D else D;
-fun dtyp_of_cons (_, _, args) = big_sprodD (map dtyp_of_arg args);
+fun dtyp_of_arg ((lazy, D), _) = if lazy then mk_uD D else D;
+fun dtyp_of_cons (_, args) = big_sprodD (map dtyp_of_arg args);
 fun dtyp_of_eq (_, cons) = big_ssumD (map dtyp_of_cons cons);
 
 
 (* ----- support for type and mixfix expressions ----- *)
 
 fun mk_uT T = Type(@{type_name "u"}, [T]);
-fun mk_cfunT (T, U) = Type(@{type_name "->"}, [T, U]);
-fun mk_sprodT (T, U) = Type(@{type_name "**"}, [T, U]);
-fun mk_ssumT (T, U) = Type(@{type_name "++"}, [T, U]);
+fun mk_cfunT (T, U) = Type(@{type_name cfun}, [T, U]);
+fun mk_sprodT (T, U) = Type(@{type_name sprod}, [T, U]);
+fun mk_ssumT (T, U) = Type(@{type_name ssum}, [T, U]);
 val oneT = @{typ one};
 
 val op ->> = mk_cfunT;
@@ -330,23 +324,5 @@
   | cont_eta_contract t    = t;
 
 fun idx_name dnames s n = s^(if length dnames = 1 then "" else string_of_int n);
-fun when_funs cons = if length cons = 1 then ["f"] 
-                     else mapn (fn n => K("f"^(string_of_int n))) 1 cons;
-fun when_body cons funarg =
-    let
-      fun one_fun n (_,_,[]  ) = /\ "dummy" (funarg(1,n))
-        | one_fun n (_,_,args) = let
-            val l2 = length args;
-            fun idxs m arg = (if is_lazy arg then (fn t => mk_fup (ID, t))
-                              else I) (Bound(l2-m));
-          in cont_eta_contract
-               (foldr'' 
-                  (fn (a,t) => mk_ssplit (/\# (a,t)))
-                  (args,
-                fn a=> /\#(a,(list_ccomb(funarg(l2,n),mapn idxs 1 args))))
-               ) end;
-    in (if length cons = 1 andalso length(third(hd cons)) <= 1
-        then mk_strictify else I)
-         (foldr1 mk_sscase (mapn one_fun 1 cons)) end;
 
 end; (* struct *)
diff -r 94170181a842 -r 67879e5d695c src/HOLCF/Tools/Domain/domain_syntax.ML
--- a/src/HOLCF/Tools/Domain/domain_syntax.ML	Tue Mar 02 22:13:39 2010 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,72 +0,0 @@
-(*  Title:      HOLCF/Tools/Domain/domain_syntax.ML
-    Author:     David von Oheimb
-
-Syntax generator for domain command.
-*)
-
-signature DOMAIN_SYNTAX =
-sig
-  val calc_syntax:
-      theory ->
-      bool ->
-      (string * typ list) *
-      (binding * (bool * binding option * typ) list * mixfix) list ->
-      (binding * typ * mixfix) list
-
-  val add_syntax:
-      bool ->
-      ((string * typ list) *
-       (binding * (bool * binding option * typ) list * mixfix) list) list ->
-      theory -> theory
-end;
-
-
-structure Domain_Syntax :> DOMAIN_SYNTAX =
-struct
-
-open Domain_Library;
-infixr 5 -->; infixr 6 ->>;
-
-fun calc_syntax thy
-    (definitional : bool)
-    ((dname : string, typevars : typ list), 
-     (cons': (binding * (bool * binding option * typ) list * mixfix) list))
-    : (binding * typ * mixfix) list =
-  let
-(* ----- constants concerning the isomorphism ------------------------------- *)
-    local
-      fun opt_lazy (lazy,_,t) = if lazy then mk_uT t else t
-      fun prod     (_,args,_) = case args of [] => oneT
-                                           | _ => foldr1 mk_sprodT (map opt_lazy args);
-    in
-    val dtype  = Type(dname,typevars);
-    val dtype2 = foldr1 mk_ssumT (map prod cons');
-    val dnam = Long_Name.base_name dname;
-    fun dbind s = Binding.name (dnam ^ s);
-    val const_rep  = (dbind "_rep" ,              dtype  ->> dtype2, NoSyn);
-    val const_abs  = (dbind "_abs" ,              dtype2 ->> dtype , NoSyn);
-    end;
-
-    val const_finite = (dbind "_finite", dtype-->HOLogic.boolT       , NoSyn);
-
-    val optional_consts =
-        if definitional then [] else [const_rep, const_abs];
-
-  in (optional_consts @ [const_finite])
-  end; (* let *)
-
-(* ----- putting all the syntax stuff together ------------------------------ *)
-
-fun add_syntax
-    (definitional : bool)
-    (eqs' : ((string * typ list) *
-             (binding * (bool * binding option * typ) list * mixfix) list) list)
-    (thy'' : theory) =
-  let
-    val ctt : (binding * typ * mixfix) list list =
-        map (calc_syntax thy'' definitional) eqs';
-  in thy''
-       |> Cont_Consts.add_consts (flat ctt)
-  end; (* let *)
-
-end; (* struct *)
diff -r 94170181a842 -r 67879e5d695c src/HOLCF/Tools/Domain/domain_take_proofs.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Tools/Domain/domain_take_proofs.ML	Wed Mar 03 09:33:46 2010 +0100
@@ -0,0 +1,421 @@
+(*  Title:      HOLCF/Tools/domain/domain_take_proofs.ML
+    Author:     Brian Huffman
+
+Defines take functions for the given domain equation
+and proves related theorems.
+*)
+
+signature DOMAIN_TAKE_PROOFS =
+sig
+  type iso_info =
+    {
+      absT : typ,
+      repT : typ,
+      abs_const : term,
+      rep_const : term,
+      abs_inverse : thm,
+      rep_inverse : thm
+    }
+
+  val define_take_functions :
+    (binding * iso_info) list -> theory ->
+    { take_consts : term list,
+      take_defs : thm list,
+      chain_take_thms : thm list,
+      take_0_thms : thm list,
+      take_Suc_thms : thm list,
+      deflation_take_thms : thm list,
+      finite_consts : term list,
+      finite_defs : thm list
+    } * theory
+
+  val map_of_typ :
+    theory -> (typ * term) list -> typ -> term
+
+  val add_map_function :
+    (string * string * thm) -> theory -> theory
+
+  val get_map_tab : theory -> string Symtab.table
+  val get_deflation_thms : theory -> thm list
+end;
+
+structure Domain_Take_Proofs : DOMAIN_TAKE_PROOFS =
+struct
+
+type iso_info =
+  {
+    absT : typ,
+    repT : typ,
+    abs_const : term,
+    rep_const : term,
+    abs_inverse : thm,
+    rep_inverse : thm
+  };
+
+val beta_ss =
+  HOL_basic_ss
+    addsimps simp_thms
+    addsimps [@{thm beta_cfun}]
+    addsimprocs [@{simproc cont_proc}];
+
+val beta_tac = simp_tac beta_ss;
+
+(******************************************************************************)
+(******************************** theory data *********************************)
+(******************************************************************************)
+
+structure MapData = Theory_Data
+(
+  (* constant names like "foo_map" *)
+  type T = string Symtab.table;
+  val empty = Symtab.empty;
+  val extend = I;
+  fun merge data = Symtab.merge (K true) data;
+);
+
+structure DeflMapData = Theory_Data
+(
+  (* theorems like "deflation a ==> deflation (foo_map$a)" *)
+  type T = thm list;
+  val empty = [];
+  val extend = I;
+  val merge = Thm.merge_thms;
+);
+
+fun add_map_function (tname, map_name, deflation_map_thm) =
+    MapData.map (Symtab.insert (K true) (tname, map_name))
+    #> DeflMapData.map (Thm.add_thm deflation_map_thm);
+
+val get_map_tab = MapData.get;
+val get_deflation_thms = DeflMapData.get;
+
+(******************************************************************************)
+(************************** building types and terms **************************)
+(******************************************************************************)
+
+open HOLCF_Library;
+
+infixr 6 ->>;
+infix -->>;
+infix 9 `;
+
+val deflT = @{typ "udom alg_defl"};
+
+fun mapT (T as Type (_, Ts)) =
+    (map (fn T => T ->> T) Ts) -->> (T ->> T)
+  | mapT T = T ->> T;
+
+fun mk_Rep_of T =
+  Const (@{const_name Rep_of}, Term.itselfT T --> deflT) $ Logic.mk_type T;
+
+fun coerce_const T = Const (@{const_name coerce}, T);
+
+fun isodefl_const T =
+  Const (@{const_name isodefl}, (T ->> T) --> deflT --> HOLogic.boolT);
+
+fun mk_deflation t =
+  Const (@{const_name deflation}, Term.fastype_of t --> boolT) $ t;
+
+fun mk_lub t =
+  let
+    val T = Term.range_type (Term.fastype_of t);
+    val lub_const = Const (@{const_name lub}, (T --> boolT) --> T);
+    val UNIV_const = @{term "UNIV :: nat set"};
+    val image_type = (natT --> T) --> (natT --> boolT) --> T --> boolT;
+    val image_const = Const (@{const_name image}, image_type);
+  in
+    lub_const $ (image_const $ t $ UNIV_const)
+  end;
+
+(* splits a cterm into the right and lefthand sides of equality *)
+fun dest_eqs t = HOLogic.dest_eq (HOLogic.dest_Trueprop t);
+
+fun mk_eqs (t, u) = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u));
+
+(******************************************************************************)
+(****************************** isomorphism info ******************************)
+(******************************************************************************)
+
+fun deflation_abs_rep (info : iso_info) : thm =
+  let
+    val abs_iso = #abs_inverse info;
+    val rep_iso = #rep_inverse info;
+    val thm = @{thm deflation_abs_rep} OF [abs_iso, rep_iso];
+  in
+    Drule.export_without_context thm
+  end
+
+(******************************************************************************)
+(********************* building map functions over types **********************)
+(******************************************************************************)
+
+fun map_of_typ (thy : theory) (sub : (typ * term) list) (T : typ) : term =
+  let
+    val map_tab = get_map_tab thy;
+    fun auto T = T ->> T;
+    fun map_of T =
+        case AList.lookup (op =) sub T of
+          SOME m => (m, true) | NONE => map_of' T
+    and map_of' (T as (Type (c, Ts))) =
+        (case Symtab.lookup map_tab c of
+          SOME map_name =>
+          let
+            val map_type = map auto Ts -->> auto T;
+            val (ms, bs) = map_split map_of Ts;
+          in
+            if exists I bs
+            then (list_ccomb (Const (map_name, map_type), ms), true)
+            else (mk_ID T, false)
+          end
+        | NONE => (mk_ID T, false))
+      | map_of' T = (mk_ID T, false);
+  in
+    fst (map_of T)
+  end;
+
+
+(******************************************************************************)
+(********************* declaring definitions and theorems *********************)
+(******************************************************************************)
+
+fun define_const
+    (bind : binding, rhs : term)
+    (thy : theory)
+    : (term * thm) * theory =
+  let
+    val typ = Term.fastype_of rhs;
+    val (const, thy) = Sign.declare_const ((bind, typ), NoSyn) thy;
+    val eqn = Logic.mk_equals (const, rhs);
+    val def = Thm.no_attributes (Binding.suffix_name "_def" bind, eqn);
+    val (def_thm, thy) = yield_singleton (PureThy.add_defs false) def thy;
+  in
+    ((const, def_thm), thy)
+  end;
+
+fun add_qualified_thm name (path, thm) thy =
+    thy
+    |> Sign.add_path path
+    |> yield_singleton PureThy.add_thms
+        (Thm.no_attributes (Binding.name name, thm))
+    ||> Sign.parent_path;
+
+(******************************************************************************)
+(************************** defining take functions ***************************)
+(******************************************************************************)
+
+fun define_take_functions
+    (spec : (binding * iso_info) list)
+    (thy : theory) =
+  let
+
+    (* retrieve components of spec *)
+    val dom_binds = map fst spec;
+    val iso_infos = map snd spec;
+    val dom_eqns = map (fn x => (#absT x, #repT x)) iso_infos;
+    val rep_abs_consts = map (fn x => (#rep_const x, #abs_const x)) iso_infos;
+    val dnames = map Binding.name_of dom_binds;
+
+    (* get table of map functions *)
+    val map_tab = MapData.get thy;
+
+    fun mk_projs []      t = []
+      | mk_projs (x::[]) t = [(x, t)]
+      | mk_projs (x::xs) t = (x, mk_fst t) :: mk_projs xs (mk_snd t);
+
+    fun mk_cfcomp2 ((rep_const, abs_const), f) =
+        mk_cfcomp (abs_const, mk_cfcomp (f, rep_const));
+
+    (* define take functional *)
+    val newTs : typ list = map fst dom_eqns;
+    val copy_arg_type = mk_tupleT (map (fn T => T ->> T) newTs);
+    val copy_arg = Free ("f", copy_arg_type);
+    val copy_args = map snd (mk_projs dom_binds copy_arg);
+    fun one_copy_rhs (rep_abs, (lhsT, rhsT)) =
+      let
+        val body = map_of_typ thy (newTs ~~ copy_args) rhsT;
+      in
+        mk_cfcomp2 (rep_abs, body)
+      end;
+    val take_functional =
+        big_lambda copy_arg
+          (mk_tuple (map one_copy_rhs (rep_abs_consts ~~ dom_eqns)));
+    val take_rhss =
+      let
+        val i = Free ("i", HOLogic.natT);
+        val rhs = mk_iterate (i, take_functional)
+      in
+        map (Term.lambda i o snd) (mk_projs dom_binds rhs)
+      end;
+
+    (* define take constants *)
+    fun define_take_const ((tbind, take_rhs), (lhsT, rhsT)) thy =
+      let
+        val take_type = HOLogic.natT --> lhsT ->> lhsT;
+        val take_bind = Binding.suffix_name "_take" tbind;
+        val (take_const, thy) =
+          Sign.declare_const ((take_bind, take_type), NoSyn) thy;
+        val take_eqn = Logic.mk_equals (take_const, take_rhs);
+        val (take_def_thm, thy) =
+          thy
+          |> Sign.add_path (Binding.name_of tbind)
+          |> yield_singleton
+              (PureThy.add_defs false o map Thm.no_attributes)
+              (Binding.name "take_def", take_eqn)
+          ||> Sign.parent_path;
+      in ((take_const, take_def_thm), thy) end;
+    val ((take_consts, take_defs), thy) = thy
+      |> fold_map define_take_const (dom_binds ~~ take_rhss ~~ dom_eqns)
+      |>> ListPair.unzip;
+
+    (* prove chain_take lemmas *)
+    fun prove_chain_take (take_const, dname) thy =
+      let
+        val goal = mk_trp (mk_chain take_const);
+        val rules = take_defs @ @{thms chain_iterate ch2ch_fst ch2ch_snd};
+        val tac = simp_tac (HOL_basic_ss addsimps rules) 1;
+        val chain_take_thm = Goal.prove_global thy [] [] goal (K tac);
+      in
+        add_qualified_thm "chain_take" (dname, chain_take_thm) thy
+      end;
+    val (chain_take_thms, thy) =
+      fold_map prove_chain_take (take_consts ~~ dnames) thy;
+
+    (* prove take_0 lemmas *)
+    fun prove_take_0 ((take_const, dname), (lhsT, rhsT)) thy =
+      let
+        val lhs = take_const $ @{term "0::nat"};
+        val goal = mk_eqs (lhs, mk_bottom (lhsT ->> lhsT));
+        val rules = take_defs @ @{thms iterate_0 fst_strict snd_strict};
+        val tac = simp_tac (HOL_basic_ss addsimps rules) 1;
+        val take_0_thm = Goal.prove_global thy [] [] goal (K tac);
+      in
+        add_qualified_thm "take_0" (dname, take_0_thm) thy
+      end;
+    val (take_0_thms, thy) =
+      fold_map prove_take_0 (take_consts ~~ dnames ~~ dom_eqns) thy;
+
+    (* prove take_Suc lemmas *)
+    val i = Free ("i", natT);
+    val take_is = map (fn t => t $ i) take_consts;
+    fun prove_take_Suc
+          (((take_const, rep_abs), dname), (lhsT, rhsT)) thy =
+      let
+        val lhs = take_const $ (@{term Suc} $ i);
+        val body = map_of_typ thy (newTs ~~ take_is) rhsT;
+        val rhs = mk_cfcomp2 (rep_abs, body);
+        val goal = mk_eqs (lhs, rhs);
+        val simps = @{thms iterate_Suc fst_conv snd_conv}
+        val rules = take_defs @ simps;
+        val tac = simp_tac (beta_ss addsimps rules) 1;
+        val take_Suc_thm = Goal.prove_global thy [] [] goal (K tac);
+      in
+        add_qualified_thm "take_Suc" (dname, take_Suc_thm) thy
+      end;
+    val (take_Suc_thms, thy) =
+      fold_map prove_take_Suc
+        (take_consts ~~ rep_abs_consts ~~ dnames ~~ dom_eqns) thy;
+
+    (* prove deflation theorems for take functions *)
+    val deflation_abs_rep_thms = map deflation_abs_rep iso_infos;
+    val deflation_take_thm =
+      let
+        val i = Free ("i", natT);
+        fun mk_goal take_const = mk_deflation (take_const $ i);
+        val goal = mk_trp (foldr1 mk_conj (map mk_goal take_consts));
+        val adm_rules =
+          @{thms adm_conj adm_subst [OF _ adm_deflation]
+                 cont2cont_fst cont2cont_snd cont_id};
+        val bottom_rules =
+          take_0_thms @ @{thms deflation_UU simp_thms};
+        val deflation_rules =
+          @{thms conjI deflation_ID}
+          @ deflation_abs_rep_thms
+          @ DeflMapData.get thy;
+      in
+        Goal.prove_global thy [] [] goal (fn _ =>
+         EVERY
+          [rtac @{thm nat.induct} 1,
+           simp_tac (HOL_basic_ss addsimps bottom_rules) 1,
+           asm_simp_tac (HOL_basic_ss addsimps take_Suc_thms) 1,
+           REPEAT (etac @{thm conjE} 1
+                   ORELSE resolve_tac deflation_rules 1
+                   ORELSE atac 1)])
+      end;
+    fun conjuncts [] thm = []
+      | conjuncts (n::[]) thm = [(n, thm)]
+      | conjuncts (n::ns) thm = let
+          val thmL = thm RS @{thm conjunct1};
+          val thmR = thm RS @{thm conjunct2};
+        in (n, thmL):: conjuncts ns thmR end;
+    val (deflation_take_thms, thy) =
+      fold_map (add_qualified_thm "deflation_take")
+        (map (apsnd Drule.export_without_context)
+          (conjuncts dnames deflation_take_thm)) thy;
+
+    (* prove strictness of take functions *)
+    fun prove_take_strict (take_const, dname) thy =
+      let
+        val goal = mk_trp (mk_strict (take_const $ Free ("i", natT)));
+        val tac = rtac @{thm deflation_strict} 1
+                  THEN resolve_tac deflation_take_thms 1;
+        val take_strict_thm = Goal.prove_global thy [] [] goal (K tac);
+      in
+        add_qualified_thm "take_strict" (dname, take_strict_thm) thy
+      end;
+    val (take_strict_thms, thy) =
+      fold_map prove_take_strict (take_consts ~~ dnames) thy;
+
+    (* prove take/take rules *)
+    fun prove_take_take ((chain_take, deflation_take), dname) thy =
+      let
+        val take_take_thm =
+            @{thm deflation_chain_min} OF [chain_take, deflation_take];
+      in
+        add_qualified_thm "take_take" (dname, take_take_thm) thy
+      end;
+    val (take_take_thms, thy) =
+      fold_map prove_take_take
+        (chain_take_thms ~~ deflation_take_thms ~~ dnames) thy;
+
+    (* define finiteness predicates *)
+    fun define_finite_const ((tbind, take_const), (lhsT, rhsT)) thy =
+      let
+        val finite_type = lhsT --> boolT;
+        val finite_bind = Binding.suffix_name "_finite" tbind;
+        val (finite_const, thy) =
+          Sign.declare_const ((finite_bind, finite_type), NoSyn) thy;
+        val x = Free ("x", lhsT);
+        val i = Free ("i", natT);
+        val finite_rhs =
+          lambda x (HOLogic.exists_const natT $
+            (lambda i (mk_eq (mk_capply (take_const $ i, x), x))));
+        val finite_eqn = Logic.mk_equals (finite_const, finite_rhs);
+        val (finite_def_thm, thy) =
+          thy
+          |> Sign.add_path (Binding.name_of tbind)
+          |> yield_singleton
+              (PureThy.add_defs false o map Thm.no_attributes)
+              (Binding.name "finite_def", finite_eqn)
+          ||> Sign.parent_path;
+      in ((finite_const, finite_def_thm), thy) end;
+    val ((finite_consts, finite_defs), thy) = thy
+      |> fold_map define_finite_const (dom_binds ~~ take_consts ~~ dom_eqns)
+      |>> ListPair.unzip;
+
+    val result =
+      {
+        take_consts = take_consts,
+        take_defs = take_defs,
+        chain_take_thms = chain_take_thms,
+        take_0_thms = take_0_thms,
+        take_Suc_thms = take_Suc_thms,
+        deflation_take_thms = deflation_take_thms,
+        finite_consts = finite_consts,
+        finite_defs = finite_defs
+      };
+
+  in
+    (result, thy)
+  end;
+
+end;
diff -r 94170181a842 -r 67879e5d695c src/HOLCF/Tools/Domain/domain_theorems.ML
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Tue Mar 02 22:13:39 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Wed Mar 03 09:33:46 2010 +0100
@@ -95,10 +95,6 @@
   InductTacs.case_tac ctxt (v^"=UU") i THEN
   asm_simp_tac (HOLCF_ss addsimps rews) i;
 
-val chain_tac =
-  REPEAT_DETERM o resolve_tac 
-    [chain_iterate, ch2ch_Rep_CFunR, ch2ch_Rep_CFunL, ch2ch_fst, ch2ch_snd];
-
 (* ----- general proofs ----------------------------------------------------- *)
 
 val all2E = @{lemma "!x y . P x y ==> (P x y ==> R) ==> R" by simp}
@@ -110,7 +106,7 @@
 let
 
 val _ = message ("Proving isomorphism properties of domain "^dname^" ...");
-val map_tab = Domain_Isomorphism.get_map_tab thy;
+val map_tab = Domain_Take_Proofs.get_map_tab thy;
 
 
 (* ----- getting the axioms and definitions --------------------------------- *)
@@ -143,7 +139,7 @@
 
 val abs_const = Const(dname^"_abs", rhsT ->> lhsT);
 
-val iso_info : Domain_Isomorphism.iso_info =
+val iso_info : Domain_Take_Proofs.iso_info =
   {
     absT = lhsT,
     repT = rhsT,
@@ -171,8 +167,6 @@
 
 val pg = pg' thy;
 
-val dc_copy = %%:(dname^"_copy");
-
 val abs_strict = ax_rep_iso RS (allI RS retraction_strict);
 val rep_strict = ax_abs_iso RS (allI RS retraction_strict);
 val iso_rews = map Drule.export_without_context [ax_abs_iso, ax_rep_iso, abs_strict, rep_strict];
@@ -182,10 +176,11 @@
 local
   fun dc_take dn = %%:(dn^"_take");
   val dnames = map (fst o fst) eqs;
-  fun get_take_strict dn = PureThy.get_thm thy (dn ^ ".take_strict");
-  val axs_take_strict = map get_take_strict dnames;
+  val deflation_thms = Domain_Take_Proofs.get_deflation_thms thy;
+  fun get_deflation_take dn = PureThy.get_thm thy (dn ^ ".deflation_take");
+  val axs_deflation_take = map get_deflation_take dnames;
 
-  fun one_take_app (con, _, args) =
+  fun one_take_app (con, args) =
     let
       fun mk_take n = dc_take (List.nth (dnames, n)) $ %:"n";
       fun one_rhs arg =
@@ -195,13 +190,11 @@
           else (%# arg);
       val lhs = (dc_take dname $ (%%:"Suc" $ %:"n"))`(con_app con args);
       val rhs = con_app2 con one_rhs args;
-      fun is_rec arg = Datatype_Aux.is_rec_type (dtyp_of arg);
-      fun is_nonlazy_rec arg = is_rec arg andalso not (is_lazy arg);
-      fun nonlazy_rec args = map vname (filter is_nonlazy_rec args);
-      val goal = lift_defined %: (nonlazy_rec args, mk_trp (lhs === rhs));
       val goal = mk_trp (lhs === rhs);
       val rules = [ax_take_Suc, ax_abs_iso, @{thm cfcomp2}];
-      val rules2 = @{thms take_con_rules ID1} @ axs_take_strict;
+      val rules2 =
+          @{thms take_con_rules ID1 deflation_strict}
+          @ deflation_thms @ axs_deflation_take;
       val tacs =
           [simp_tac (HOL_basic_ss addsimps rules) 1,
            asm_simp_tac (HOL_basic_ss addsimps rules2) 1];
@@ -239,7 +232,7 @@
 
 fun comp_theorems (comp_dnam, eqs: eq list) thy =
 let
-val map_tab = Domain_Isomorphism.get_map_tab thy;
+val map_tab = Domain_Take_Proofs.get_map_tab thy;
 
 val dnames = map (fst o fst) eqs;
 val conss  = map  snd        eqs;
@@ -273,7 +266,7 @@
   val dnames = map (fst o fst) eqs;
   val x_name = idx_name dnames "x"; 
 
-  fun one_con (con, _, args) =
+  fun one_con (con, args) =
     let
       val nonrec_args = filter_out is_rec args;
       val    rec_args = filter is_rec args;
@@ -353,7 +346,7 @@
     maps (fn dn => PureThy.get_thms thy (dn ^ ".take_rews")) dnames;
 
 local
-  fun one_con p (con, _, args) =
+  fun one_con p (con, args) =
     let
       val P_names = map P_name (1 upto (length dnames));
       val vns = Name.variant_list P_names (map vname args);
@@ -377,7 +370,7 @@
   fun ind_prems_tac prems = EVERY
     (maps (fn cons =>
       (resolve_tac prems 1 ::
-        maps (fn (_,_,args) => 
+        maps (fn (_,args) => 
           resolve_tac prems 1 ::
           map (K(atac 1)) (nonlazy args) @
           map (K(atac 1)) (filter is_rec args))
@@ -392,7 +385,7 @@
           ((rec_of arg =  n andalso nfn(lazy_rec orelse is_lazy arg)) orelse 
             rec_of arg <> n andalso rec_to quant nfn rfn (rec_of arg::ns) 
               (lazy_rec orelse is_lazy arg) (n, (List.nth(conss,rec_of arg))))
-          ) o third) cons;
+          ) o snd) cons;
     fun all_rec_to ns  = rec_to forall not all_rec_to  ns;
     fun warn (n,cons) =
       if all_rec_to [] false (n,cons)
@@ -424,14 +417,14 @@
                         (* FIXME! case_UU_tac *)
             case_UU_tac context (prems @ con_rews) 1
               (List.nth (dnames, rec_of arg) ^ "_take n$" ^ vname arg);
-          fun con_tacs (con, _, args) = 
+          fun con_tacs (con, args) = 
             asm_simp_tac take_ss 1 ::
             map arg_tac (filter is_nonlazy_rec args) @
             [resolve_tac prems 1] @
             map (K (atac 1)) (nonlazy args) @
             map (K (etac spec 1)) (filter is_rec args);
           fun cases_tacs (cons, cases) =
-            res_inst_tac context [(("x", 0), "x")] cases 1 ::
+            res_inst_tac context [(("y", 0), "x")] cases 1 ::
             asm_simp_tac (take_ss addsimps prems) 1 ::
             maps con_tacs cons;
         in
@@ -500,13 +493,13 @@
               etac disjE 1,
               asm_simp_tac (HOL_ss addsimps con_rews) 1,
               asm_simp_tac take_ss 1];
-            fun con_tacs ctxt (con, _, args) =
+            fun con_tacs ctxt (con, args) =
               asm_simp_tac take_ss 1 ::
               maps (arg_tacs ctxt) (nonlazy_rec args);
             fun foo_tacs ctxt n (cons, cases) =
               simp_tac take_ss 1 ::
               rtac allI 1 ::
-              res_inst_tac ctxt [(("x", 0), x_name n)] cases 1 ::
+              res_inst_tac ctxt [(("y", 0), x_name n)] cases 1 ::
               asm_simp_tac take_ss 1 ::
               maps (con_tacs ctxt) cons;
             fun tacs ctxt =
diff -r 94170181a842 -r 67879e5d695c src/HOLCF/Tools/cont_consts.ML
--- a/src/HOLCF/Tools/cont_consts.ML	Tue Mar 02 22:13:39 2010 +0100
+++ b/src/HOLCF/Tools/cont_consts.ML	Wed Mar 03 09:33:46 2010 +0100
@@ -56,7 +56,7 @@
       trans_rules (syntax c2) (syntax c1) n mx)
   end;
 
-fun cfun_arity (Type (n, [_, T])) = if n = @{type_name "->"} then 1 + cfun_arity T else 0
+fun cfun_arity (Type (n, [_, T])) = if n = @{type_name cfun} then 1 + cfun_arity T else 0
   | cfun_arity _ = 0;
 
 fun is_contconst (_, _, NoSyn) = false
diff -r 94170181a842 -r 67879e5d695c src/HOLCF/Tools/fixrec.ML
--- a/src/HOLCF/Tools/fixrec.ML	Tue Mar 02 22:13:39 2010 +0100
+++ b/src/HOLCF/Tools/fixrec.ML	Wed Mar 03 09:33:46 2010 +0100
@@ -22,10 +22,15 @@
 structure Fixrec :> FIXREC =
 struct
 
+open HOLCF_Library;
+
+infixr 6 ->>;
+infix -->>;
+infix 9 `;
+
 val def_cont_fix_eq = @{thm def_cont_fix_eq};
 val def_cont_fix_ind = @{thm def_cont_fix_ind};
 
-
 fun fixrec_err s = error ("fixrec definition error:\n" ^ s);
 fun fixrec_eq_err thy s eq =
   fixrec_err (s ^ "\nin\n" ^ quote (Syntax.string_of_term_global thy eq));
@@ -34,42 +39,23 @@
 (***************************** building types ****************************)
 (*************************************************************************)
 
-(* ->> is taken from holcf_logic.ML *)
-fun cfunT (T, U) = Type(@{type_name "->"}, [T, U]);
-
-infixr 6 ->>; val (op ->>) = cfunT;
-
-fun dest_cfunT (Type(@{type_name "->"}, [T, U])) = (T, U)
-  | dest_cfunT T = raise TYPE ("dest_cfunT", [T], []);
-
-fun maybeT T = Type(@{type_name "maybe"}, [T]);
-
-fun dest_maybeT (Type(@{type_name "maybe"}, [T])) = T
-  | dest_maybeT T = raise TYPE ("dest_maybeT", [T], []);
-
-fun tupleT [] = HOLogic.unitT
-  | tupleT [T] = T
-  | tupleT (T :: Ts) = HOLogic.mk_prodT (T, tupleT Ts);
-
 local
 
-fun binder_cfun (Type(@{type_name "->"},[T, U])) = T :: binder_cfun U
+fun binder_cfun (Type(@{type_name cfun},[T, U])) = T :: binder_cfun U
   | binder_cfun (Type(@{type_name "fun"},[T, U])) = T :: binder_cfun U
   | binder_cfun _   =  [];
 
-fun body_cfun (Type(@{type_name "->"},[T, U])) = body_cfun U
+fun body_cfun (Type(@{type_name cfun},[T, U])) = body_cfun U
   | body_cfun (Type(@{type_name "fun"},[T, U])) = body_cfun U
   | body_cfun T   =  T;
 
 fun strip_cfun T : typ list * typ =
   (binder_cfun T, body_cfun T);
 
-fun cfunsT (Ts, U) = List.foldr cfunT U Ts;
-
 in
 
-fun matchT (T, U) =
-  body_cfun T ->> cfunsT (binder_cfun T, U) ->> U;
+fun matcherT (T, U) =
+  body_cfun T ->> (binder_cfun T -->> U) ->> U;
 
 end
 
@@ -86,43 +72,8 @@
 fun chead_of (Const(@{const_name Rep_CFun},_)$f$t) = chead_of f
   | chead_of u = u;
 
-fun capply_const (S, T) =
-  Const(@{const_name Rep_CFun}, (S ->> T) --> (S --> T));
-
-fun cabs_const (S, T) =
-  Const(@{const_name Abs_CFun}, (S --> T) --> (S ->> T));
-
-fun mk_cabs t =
-  let val T = Term.fastype_of t
-  in cabs_const (Term.domain_type T, Term.range_type T) $ t end
-
-fun mk_capply (t, u) =
-  let val (S, T) =
-    case Term.fastype_of t of
-        Type(@{type_name "->"}, [S, T]) => (S, T)
-      | _ => raise TERM ("mk_capply " ^ ML_Syntax.print_list ML_Syntax.print_term [t, u], [t, u]);
-  in capply_const (S, T) $ t $ u end;
-
 infix 0 ==;  val (op ==) = Logic.mk_equals;
 infix 1 ===; val (op ===) = HOLogic.mk_eq;
-infix 9 `  ; val (op `) = mk_capply;
-
-(* builds the expression (LAM v. rhs) *)
-fun big_lambda v rhs =
-  cabs_const (Term.fastype_of v, Term.fastype_of rhs) $ Term.lambda v rhs;
-
-(* builds the expression (LAM v1 v2 .. vn. rhs) *)
-fun big_lambdas [] rhs = rhs
-  | big_lambdas (v::vs) rhs = big_lambda v (big_lambdas vs rhs);
-
-fun mk_return t =
-  let val T = Term.fastype_of t
-  in Const(@{const_name Fixrec.return}, T ->> maybeT T) ` t end;
-
-fun mk_bind (t, u) =
-  let val (T, mU) = dest_cfunT (Term.fastype_of u);
-      val bindT = maybeT T ->> (T ->> mU) ->> mU;
-  in Const(@{const_name Fixrec.bind}, bindT) ` t ` u end;
 
 fun mk_mplus (t, u) =
   let val mT = Term.fastype_of t
@@ -130,31 +81,9 @@
 
 fun mk_run t =
   let val mT = Term.fastype_of t
-      val T = dest_maybeT mT
+      val T = dest_matchT mT
   in Const(@{const_name Fixrec.run}, mT ->> T) ` t end;
 
-fun mk_fix t =
-  let val (T, _) = dest_cfunT (Term.fastype_of t)
-  in Const(@{const_name fix}, (T ->> T) ->> T) ` t end;
-
-fun mk_cont t =
-  let val T = Term.fastype_of t
-  in Const(@{const_name cont}, T --> HOLogic.boolT) $ t end;
-
-val mk_fst = HOLogic.mk_fst
-val mk_snd = HOLogic.mk_snd
-
-(* builds the expression (v1,v2,..,vn) *)
-fun mk_tuple [] = HOLogic.unit
-|   mk_tuple (t::[]) = t
-|   mk_tuple (t::ts) = HOLogic.mk_prod (t, mk_tuple ts);
-
-(* builds the expression (%(v1,v2,..,vn). rhs) *)
-fun lambda_tuple [] rhs = Term.lambda (Free("unit", HOLogic.unitT)) rhs
-  | lambda_tuple (v::[]) rhs = Term.lambda v rhs
-  | lambda_tuple (v::vs) rhs =
-      HOLogic.mk_split (Term.lambda v (lambda_tuple vs rhs));
-
 
 (*************************************************************************)
 (************* fixed-point definitions and unfolding theorems ************)
@@ -288,11 +217,11 @@
   | Const(c,T) =>
       let
         val n = Name.variant taken "v";
-        fun result_type (Type(@{type_name "->"},[_,T])) (x::xs) = result_type T xs
+        fun result_type (Type(@{type_name cfun},[_,T])) (x::xs) = result_type T xs
           | result_type (Type (@{type_name "fun"},[_,T])) (x::xs) = result_type T xs
           | result_type T _ = T;
         val v = Free(n, result_type T vs);
-        val m = Const(match_name c, matchT (T, fastype_of rhs));
+        val m = Const(match_name c, matcherT (T, fastype_of rhs));
         val k = big_lambdas vs rhs;
       in
         (m`v`k, v, n::taken)
@@ -340,7 +269,7 @@
     val msum = foldr1 mk_mplus (map (unLAM arity) ms);
     val (Ts, U) = LAM_Ts arity (hd ms)
   in
-    reLAM (rev Ts, dest_maybeT U) (mk_run msum)
+    reLAM (rev Ts, dest_matchT U) (mk_run msum)
   end;
 
 (* this is the pattern-matching compiler function *)
diff -r 94170181a842 -r 67879e5d695c src/HOLCF/Tools/holcf_library.ML
--- a/src/HOLCF/Tools/holcf_library.ML	Tue Mar 02 22:13:39 2010 +0100
+++ b/src/HOLCF/Tools/holcf_library.ML	Wed Mar 03 09:33:46 2010 +0100
@@ -51,12 +51,12 @@
 (*** Continuous function space ***)
 
 (* ->> is taken from holcf_logic.ML *)
-fun mk_cfunT (T, U) = Type(@{type_name "->"}, [T, U]);
+fun mk_cfunT (T, U) = Type(@{type_name cfun}, [T, U]);
 
 val (op ->>) = mk_cfunT;
 val (op -->>) = Library.foldr mk_cfunT;
 
-fun dest_cfunT (Type(@{type_name "->"}, [T, U])) = (T, U)
+fun dest_cfunT (Type(@{type_name cfun}, [T, U])) = (T, U)
   | dest_cfunT T = raise TYPE ("dest_cfunT", [T], []);
 
 fun capply_const (S, T) =
@@ -84,7 +84,7 @@
 fun mk_capply (t, u) =
   let val (S, T) =
     case fastype_of t of
-        Type(@{type_name "->"}, [S, T]) => (S, T)
+        Type(@{type_name cfun}, [S, T]) => (S, T)
       | _ => raise TERM ("mk_capply " ^ ML_Syntax.print_list ML_Syntax.print_term [t, u], [t, u]);
   in capply_const (S, T) $ t $ u end;
 
@@ -153,9 +153,9 @@
 
 val oneT = @{typ "one"};
 
-fun mk_sprodT (T, U) = Type(@{type_name "**"}, [T, U]);
+fun mk_sprodT (T, U) = Type(@{type_name sprod}, [T, U]);
 
-fun dest_sprodT (Type(@{type_name "**"}, [T, U])) = (T, U)
+fun dest_sprodT (Type(@{type_name sprod}, [T, U])) = (T, U)
   | dest_sprodT T = raise TYPE ("dest_sprodT", [T], []);
 
 fun spair_const (T, U) =
@@ -179,9 +179,9 @@
 
 (*** Strict sum type ***)
 
-fun mk_ssumT (T, U) = Type(@{type_name "++"}, [T, U]);
+fun mk_ssumT (T, U) = Type(@{type_name ssum}, [T, U]);
 
-fun dest_ssumT (Type(@{type_name "++"}, [T, U])) = (T, U)
+fun dest_ssumT (Type(@{type_name ssum}, [T, U])) = (T, U)
   | dest_ssumT T = raise TYPE ("dest_ssumT", [T], []);
 
 fun sinl_const (T, U) = Const(@{const_name sinl}, T ->> mk_ssumT (T, U));
diff -r 94170181a842 -r 67879e5d695c src/HOLCF/Tools/repdef.ML
--- a/src/HOLCF/Tools/repdef.ML	Tue Mar 02 22:13:39 2010 +0100
+++ b/src/HOLCF/Tools/repdef.ML	Wed Mar 03 09:33:46 2010 +0100
@@ -20,32 +20,28 @@
 structure Repdef :> REPDEF =
 struct
 
+open HOLCF_Library;
+
+infixr 6 ->>;
+infix -->>;
+
 (** type definitions **)
 
 type rep_info =
   { emb_def: thm, prj_def: thm, approx_def: thm, REP: thm };
 
-(* building terms *)
+(* building types and terms *)
 
-fun adm_const T = Const (@{const_name adm}, (T --> HOLogic.boolT) --> HOLogic.boolT);
-fun mk_adm (x, T, P) = adm_const T $ absfree (x, T, P);
-
-fun below_const T = Const (@{const_name below}, T --> T --> HOLogic.boolT);
-
-val natT = @{typ nat};
 val udomT = @{typ udom};
 fun alg_deflT T = Type (@{type_name alg_defl}, [T]);
-fun cfunT (T, U) = Type (@{type_name "->"}, [T, U]);
-fun emb_const T = Const (@{const_name emb}, cfunT (T, udomT));
-fun prj_const T = Const (@{const_name prj}, cfunT (udomT, T));
-fun approx_const T = Const (@{const_name approx}, natT --> cfunT (T, T));
+fun emb_const T = Const (@{const_name emb}, T ->> udomT);
+fun prj_const T = Const (@{const_name prj}, udomT ->> T);
+fun approx_const T = Const (@{const_name approx}, natT --> (T ->> T));
 
-fun LAM_const (T, U) = Const (@{const_name Abs_CFun}, (T --> U) --> cfunT (T, U));
-fun APP_const (T, U) = Const (@{const_name Rep_CFun}, cfunT (T, U) --> (T --> U));
-fun cast_const T = Const (@{const_name cast}, cfunT (alg_deflT T, cfunT (T, T)));
+fun cast_const T = Const (@{const_name cast}, alg_deflT T ->> T ->> T);
 fun mk_cast (t, x) =
-  APP_const (udomT, udomT)
-  $ (APP_const (alg_deflT udomT, cfunT (udomT, udomT)) $ cast_const udomT $ t)
+  capply_const (udomT, udomT)
+  $ (capply_const (alg_deflT udomT, udomT ->> udomT) $ cast_const udomT $ t)
   $ x;
 
 (* manipulating theorems *)
@@ -99,12 +95,12 @@
     (*definitions*)
     val Rep_const = Const (#Rep_name info, newT --> udomT);
     val Abs_const = Const (#Abs_name info, udomT --> newT);
-    val emb_eqn = Logic.mk_equals (emb_const newT, LAM_const (newT, udomT) $ Rep_const);
-    val prj_eqn = Logic.mk_equals (prj_const newT, LAM_const (udomT, newT) $
+    val emb_eqn = Logic.mk_equals (emb_const newT, cabs_const (newT, udomT) $ Rep_const);
+    val prj_eqn = Logic.mk_equals (prj_const newT, cabs_const (udomT, newT) $
       Abs ("x", udomT, Abs_const $ mk_cast (defl, Bound 0)));
     val repdef_approx_const =
       Const (@{const_name repdef_approx}, (newT --> udomT) --> (udomT --> newT)
-        --> alg_deflT udomT --> natT --> cfunT (newT, newT));
+        --> alg_deflT udomT --> natT --> (newT ->> newT));
     val approx_eqn = Logic.mk_equals (approx_const newT,
       repdef_approx_const $ Rep_const $ Abs_const $ defl);
 
diff -r 94170181a842 -r 67879e5d695c src/HOLCF/ex/Dnat.thy
--- a/src/HOLCF/ex/Dnat.thy	Tue Mar 02 22:13:39 2010 +0100
+++ b/src/HOLCF/ex/Dnat.thy	Wed Mar 03 09:33:46 2010 +0100
@@ -55,12 +55,12 @@
   apply (induct_tac x rule: dnat.ind)
     apply fast
    apply (rule allI)
-   apply (rule_tac x = y in dnat.casedist)
+   apply (case_tac y)
      apply simp
     apply simp
    apply simp
   apply (rule allI)
-  apply (rule_tac x = y in dnat.casedist)
+  apply (case_tac y)
     apply (fast intro!: UU_I)
    apply (thin_tac "ALL y. dnat << y --> dnat = UU | dnat = y")
    apply simp
diff -r 94170181a842 -r 67879e5d695c src/HOLCF/ex/Stream.thy
--- a/src/HOLCF/ex/Stream.thy	Tue Mar 02 22:13:39 2010 +0100
+++ b/src/HOLCF/ex/Stream.thy	Wed Mar 03 09:33:46 2010 +0100
@@ -290,12 +290,12 @@
 
 lemma stream_finite_lemma1: "stream_finite xs ==> stream_finite (x && xs)"
 apply (simp add: stream.finite_def,auto)
-apply (rule_tac x="Suc n" in exI)
+apply (rule_tac x="Suc i" in exI)
 by (simp add: stream_take_lemma4)
 
 lemma stream_finite_lemma2: "[| x ~= UU; stream_finite (x && xs) |] ==> stream_finite xs"
 apply (simp add: stream.finite_def, auto)
-apply (rule_tac x="n" in exI)
+apply (rule_tac x="i" in exI)
 by (erule stream_take_lemma3,simp)
 
 lemma stream_finite_rt_eq: "stream_finite (rt$s) = stream_finite s"