# HG changeset patch
# User haftmann
# Date 1290550266 -3600
# Node ID 23904fa13e0389a9cc51f47ed59fe278be2377fa
# Parent  c059d550afecd98c6c8df00333d8a8724f7b814f# Parent  05f4885cbbe073ac6ef1cbf0101e78c839bf669c
merged

diff -r c059d550afec -r 23904fa13e03 NEWS
--- a/NEWS	Tue Nov 23 23:10:13 2010 +0100
+++ b/NEWS	Tue Nov 23 23:11:06 2010 +0100
@@ -89,6 +89,9 @@
 
 *** HOL ***
 
+* Renamed theory Fset to Cset, type Fset.fset to Cset.set, in order to
+avoid confusion with finite sets.  INCOMPATIBILITY.
+
 * Quickcheck's generator for random generation is renamed from "code" to
 "random". INCOMPATIBILITY. 
 
diff -r c059d550afec -r 23904fa13e03 src/HOL/Imperative_HOL/Array.thy
--- a/src/HOL/Imperative_HOL/Array.thy	Tue Nov 23 23:10:13 2010 +0100
+++ b/src/HOL/Imperative_HOL/Array.thy	Tue Nov 23 23:11:06 2010 +0100
@@ -170,16 +170,16 @@
   "success (new n x) h"
   by (auto intro: success_intros simp add: new_def)
 
-lemma crel_newI [crel_intros]:
+lemma effect_newI [effect_intros]:
   assumes "(a, h') = alloc (replicate n x) h"
-  shows "crel (new n x) h h' a"
-  by (rule crelI) (simp add: assms execute_simps)
+  shows "effect (new n x) h h' a"
+  by (rule effectI) (simp add: assms execute_simps)
 
-lemma crel_newE [crel_elims]:
-  assumes "crel (new n x) h h' r"
+lemma effect_newE [effect_elims]:
+  assumes "effect (new n x) h h' r"
   obtains "r = fst (alloc (replicate n x) h)" "h' = snd (alloc (replicate n x) h)" 
     "get h' r = replicate n x" "present h' r" "\<not> present h r"
-  using assms by (rule crelE) (simp add: get_alloc execute_simps)
+  using assms by (rule effectE) (simp add: get_alloc execute_simps)
 
 lemma execute_of_list [execute_simps]:
   "execute (of_list xs) h = Some (alloc xs h)"
@@ -189,16 +189,16 @@
   "success (of_list xs) h"
   by (auto intro: success_intros simp add: of_list_def)
 
-lemma crel_of_listI [crel_intros]:
+lemma effect_of_listI [effect_intros]:
   assumes "(a, h') = alloc xs h"
-  shows "crel (of_list xs) h h' a"
-  by (rule crelI) (simp add: assms execute_simps)
+  shows "effect (of_list xs) h h' a"
+  by (rule effectI) (simp add: assms execute_simps)
 
-lemma crel_of_listE [crel_elims]:
-  assumes "crel (of_list xs) h h' r"
+lemma effect_of_listE [effect_elims]:
+  assumes "effect (of_list xs) h h' r"
   obtains "r = fst (alloc xs h)" "h' = snd (alloc xs h)" 
     "get h' r = xs" "present h' r" "\<not> present h r"
-  using assms by (rule crelE) (simp add: get_alloc execute_simps)
+  using assms by (rule effectE) (simp add: get_alloc execute_simps)
 
 lemma execute_make [execute_simps]:
   "execute (make n f) h = Some (alloc (map f [0 ..< n]) h)"
@@ -208,16 +208,16 @@
   "success (make n f) h"
   by (auto intro: success_intros simp add: make_def)
 
-lemma crel_makeI [crel_intros]:
+lemma effect_makeI [effect_intros]:
   assumes "(a, h') = alloc (map f [0 ..< n]) h"
-  shows "crel (make n f) h h' a"
-  by (rule crelI) (simp add: assms execute_simps)
+  shows "effect (make n f) h h' a"
+  by (rule effectI) (simp add: assms execute_simps)
 
-lemma crel_makeE [crel_elims]:
-  assumes "crel (make n f) h h' r"
+lemma effect_makeE [effect_elims]:
+  assumes "effect (make n f) h h' r"
   obtains "r = fst (alloc (map f [0 ..< n]) h)" "h' = snd (alloc (map f [0 ..< n]) h)" 
     "get h' r = map f [0 ..< n]" "present h' r" "\<not> present h r"
-  using assms by (rule crelE) (simp add: get_alloc execute_simps)
+  using assms by (rule effectE) (simp add: get_alloc execute_simps)
 
 lemma execute_len [execute_simps]:
   "execute (len a) h = Some (length h a, h)"
@@ -227,15 +227,15 @@
   "success (len a) h"
   by (auto intro: success_intros simp add: len_def)
 
-lemma crel_lengthI [crel_intros]:
+lemma effect_lengthI [effect_intros]:
   assumes "h' = h" "r = length h a"
-  shows "crel (len a) h h' r"
-  by (rule crelI) (simp add: assms execute_simps)
+  shows "effect (len a) h h' r"
+  by (rule effectI) (simp add: assms execute_simps)
 
-lemma crel_lengthE [crel_elims]:
-  assumes "crel (len a) h h' r"
+lemma effect_lengthE [effect_elims]:
+  assumes "effect (len a) h h' r"
   obtains "r = length h' a" "h' = h" 
-  using assms by (rule crelE) (simp add: execute_simps)
+  using assms by (rule effectE) (simp add: execute_simps)
 
 lemma execute_nth [execute_simps]:
   "i < length h a \<Longrightarrow>
@@ -247,15 +247,15 @@
   "i < length h a \<Longrightarrow> success (nth a i) h"
   by (auto intro: success_intros simp add: nth_def)
 
-lemma crel_nthI [crel_intros]:
+lemma effect_nthI [effect_intros]:
   assumes "i < length h a" "h' = h" "r = get h a ! i"
-  shows "crel (nth a i) h h' r"
-  by (rule crelI) (insert assms, simp add: execute_simps)
+  shows "effect (nth a i) h h' r"
+  by (rule effectI) (insert assms, simp add: execute_simps)
 
-lemma crel_nthE [crel_elims]:
-  assumes "crel (nth a i) h h' r"
+lemma effect_nthE [effect_elims]:
+  assumes "effect (nth a i) h h' r"
   obtains "i < length h a" "r = get h a ! i" "h' = h"
-  using assms by (rule crelE)
+  using assms by (rule effectE)
     (erule successE, cases "i < length h a", simp_all add: execute_simps)
 
 lemma execute_upd [execute_simps]:
@@ -268,15 +268,15 @@
   "i < length h a \<Longrightarrow> success (upd i x a) h"
   by (auto intro: success_intros simp add: upd_def)
 
-lemma crel_updI [crel_intros]:
+lemma effect_updI [effect_intros]:
   assumes "i < length h a" "h' = update a i v h"
-  shows "crel (upd i v a) h h' a"
-  by (rule crelI) (insert assms, simp add: execute_simps)
+  shows "effect (upd i v a) h h' a"
+  by (rule effectI) (insert assms, simp add: execute_simps)
 
-lemma crel_updE [crel_elims]:
-  assumes "crel (upd i v a) h h' r"
+lemma effect_updE [effect_elims]:
+  assumes "effect (upd i v a) h h' r"
   obtains "r = a" "h' = update a i v h" "i < length h a"
-  using assms by (rule crelE)
+  using assms by (rule effectE)
     (erule successE, cases "i < length h a", simp_all add: execute_simps)
 
 lemma execute_map_entry [execute_simps]:
@@ -290,15 +290,15 @@
   "i < length h a \<Longrightarrow> success (map_entry i f a) h"
   by (auto intro: success_intros simp add: map_entry_def)
 
-lemma crel_map_entryI [crel_intros]:
+lemma effect_map_entryI [effect_intros]:
   assumes "i < length h a" "h' = update a i (f (get h a ! i)) h" "r = a"
-  shows "crel (map_entry i f a) h h' r"
-  by (rule crelI) (insert assms, simp add: execute_simps)
+  shows "effect (map_entry i f a) h h' r"
+  by (rule effectI) (insert assms, simp add: execute_simps)
 
-lemma crel_map_entryE [crel_elims]:
-  assumes "crel (map_entry i f a) h h' r"
+lemma effect_map_entryE [effect_elims]:
+  assumes "effect (map_entry i f a) h h' r"
   obtains "r = a" "h' = update a i (f (get h a ! i)) h" "i < length h a"
-  using assms by (rule crelE)
+  using assms by (rule effectE)
     (erule successE, cases "i < length h a", simp_all add: execute_simps)
 
 lemma execute_swap [execute_simps]:
@@ -312,15 +312,15 @@
   "i < length h a \<Longrightarrow> success (swap i x a) h"
   by (auto intro: success_intros simp add: swap_def)
 
-lemma crel_swapI [crel_intros]:
+lemma effect_swapI [effect_intros]:
   assumes "i < length h a" "h' = update a i x h" "r = get h a ! i"
-  shows "crel (swap i x a) h h' r"
-  by (rule crelI) (insert assms, simp add: execute_simps)
+  shows "effect (swap i x a) h h' r"
+  by (rule effectI) (insert assms, simp add: execute_simps)
 
-lemma crel_swapE [crel_elims]:
-  assumes "crel (swap i x a) h h' r"
+lemma effect_swapE [effect_elims]:
+  assumes "effect (swap i x a) h h' r"
   obtains "r = get h a ! i" "h' = update a i x h" "i < length h a"
-  using assms by (rule crelE)
+  using assms by (rule effectE)
     (erule successE, cases "i < length h a", simp_all add: execute_simps)
 
 lemma execute_freeze [execute_simps]:
@@ -331,15 +331,15 @@
   "success (freeze a) h"
   by (auto intro: success_intros simp add: freeze_def)
 
-lemma crel_freezeI [crel_intros]:
+lemma effect_freezeI [effect_intros]:
   assumes "h' = h" "r = get h a"
-  shows "crel (freeze a) h h' r"
-  by (rule crelI) (insert assms, simp add: execute_simps)
+  shows "effect (freeze a) h h' r"
+  by (rule effectI) (insert assms, simp add: execute_simps)
 
-lemma crel_freezeE [crel_elims]:
-  assumes "crel (freeze a) h h' r"
+lemma effect_freezeE [effect_elims]:
+  assumes "effect (freeze a) h h' r"
   obtains "h' = h" "r = get h a"
-  using assms by (rule crelE) (simp add: execute_simps)
+  using assms by (rule effectE) (simp add: execute_simps)
 
 lemma upd_return:
   "upd i x a \<guillemotright> return a = upd i x a"
diff -r c059d550afec -r 23904fa13e03 src/HOL/Imperative_HOL/Heap_Monad.thy
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Tue Nov 23 23:10:13 2010 +0100
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Tue Nov 23 23:11:06 2010 +0100
@@ -122,25 +122,25 @@
 subsubsection {* Predicate for a simple relational calculus *}
 
 text {*
-  The @{text crel} predicate states that when a computation @{text c}
+  The @{text effect} predicate states that when a computation @{text c}
   runs with the heap @{text h} will result in return value @{text r}
   and a heap @{text "h'"}, i.e.~no exception occurs.
 *}  
 
-definition crel :: "'a Heap \<Rightarrow> heap \<Rightarrow> heap \<Rightarrow> 'a \<Rightarrow> bool" where
-  crel_def: "crel c h h' r \<longleftrightarrow> execute c h = Some (r, h')"
+definition effect :: "'a Heap \<Rightarrow> heap \<Rightarrow> heap \<Rightarrow> 'a \<Rightarrow> bool" where
+  effect_def: "effect c h h' r \<longleftrightarrow> execute c h = Some (r, h')"
 
-lemma crelI:
-  "execute c h = Some (r, h') \<Longrightarrow> crel c h h' r"
-  by (simp add: crel_def)
+lemma effectI:
+  "execute c h = Some (r, h') \<Longrightarrow> effect c h h' r"
+  by (simp add: effect_def)
 
-lemma crelE:
-  assumes "crel c h h' r"
+lemma effectE:
+  assumes "effect c h h' r"
   obtains "r = fst (the (execute c h))"
     and "h' = snd (the (execute c h))"
     and "success c h"
 proof (rule that)
-  from assms have *: "execute c h = Some (r, h')" by (simp add: crel_def)
+  from assms have *: "execute c h = Some (r, h')" by (simp add: effect_def)
   then show "success c h" by (simp add: success_def)
   from * have "fst (the (execute c h)) = r" and "snd (the (execute c h)) = h'"
     by simp_all
@@ -148,84 +148,84 @@
     and "h' = snd (the (execute c h))" by simp_all
 qed
 
-lemma crel_success:
-  "crel c h h' r \<Longrightarrow> success c h"
-  by (simp add: crel_def success_def)
+lemma effect_success:
+  "effect c h h' r \<Longrightarrow> success c h"
+  by (simp add: effect_def success_def)
 
-lemma success_crelE:
+lemma success_effectE:
   assumes "success c h"
-  obtains r h' where "crel c h h' r"
-  using assms by (auto simp add: crel_def success_def)
+  obtains r h' where "effect c h h' r"
+  using assms by (auto simp add: effect_def success_def)
 
-lemma crel_deterministic:
-  assumes "crel f h h' a"
-    and "crel f h h'' b"
+lemma effect_deterministic:
+  assumes "effect f h h' a"
+    and "effect f h h'' b"
   shows "a = b" and "h' = h''"
-  using assms unfolding crel_def by auto
+  using assms unfolding effect_def by auto
 
 ML {* structure Crel_Intros = Named_Thms(
-  val name = "crel_intros"
-  val description = "introduction rules for crel"
+  val name = "effect_intros"
+  val description = "introduction rules for effect"
 ) *}
 
 ML {* structure Crel_Elims = Named_Thms(
-  val name = "crel_elims"
-  val description = "elimination rules for crel"
+  val name = "effect_elims"
+  val description = "elimination rules for effect"
 ) *}
 
 setup "Crel_Intros.setup #> Crel_Elims.setup"
 
-lemma crel_LetI [crel_intros]:
-  assumes "x = t" "crel (f x) h h' r"
-  shows "crel (let x = t in f x) h h' r"
+lemma effect_LetI [effect_intros]:
+  assumes "x = t" "effect (f x) h h' r"
+  shows "effect (let x = t in f x) h h' r"
   using assms by simp
 
-lemma crel_LetE [crel_elims]:
-  assumes "crel (let x = t in f x) h h' r"
-  obtains "crel (f t) h h' r"
+lemma effect_LetE [effect_elims]:
+  assumes "effect (let x = t in f x) h h' r"
+  obtains "effect (f t) h h' r"
   using assms by simp
 
-lemma crel_ifI:
-  assumes "c \<Longrightarrow> crel t h h' r"
-    and "\<not> c \<Longrightarrow> crel e h h' r"
-  shows "crel (if c then t else e) h h' r"
+lemma effect_ifI:
+  assumes "c \<Longrightarrow> effect t h h' r"
+    and "\<not> c \<Longrightarrow> effect e h h' r"
+  shows "effect (if c then t else e) h h' r"
   by (cases c) (simp_all add: assms)
 
-lemma crel_ifE:
-  assumes "crel (if c then t else e) h h' r"
-  obtains "c" "crel t h h' r"
-    | "\<not> c" "crel e h h' r"
+lemma effect_ifE:
+  assumes "effect (if c then t else e) h h' r"
+  obtains "c" "effect t h h' r"
+    | "\<not> c" "effect e h h' r"
   using assms by (cases c) simp_all
 
-lemma crel_tapI [crel_intros]:
+lemma effect_tapI [effect_intros]:
   assumes "h' = h" "r = f h"
-  shows "crel (tap f) h h' r"
-  by (rule crelI) (simp add: assms execute_simps)
+  shows "effect (tap f) h h' r"
+  by (rule effectI) (simp add: assms execute_simps)
 
-lemma crel_tapE [crel_elims]:
-  assumes "crel (tap f) h h' r"
+lemma effect_tapE [effect_elims]:
+  assumes "effect (tap f) h h' r"
   obtains "h' = h" and "r = f h"
-  using assms by (rule crelE) (auto simp add: execute_simps)
+  using assms by (rule effectE) (auto simp add: execute_simps)
 
-lemma crel_heapI [crel_intros]:
+lemma effect_heapI [effect_intros]:
   assumes "h' = snd (f h)" "r = fst (f h)"
-  shows "crel (heap f) h h' r"
-  by (rule crelI) (simp add: assms execute_simps)
+  shows "effect (heap f) h h' r"
+  by (rule effectI) (simp add: assms execute_simps)
 
-lemma crel_heapE [crel_elims]:
-  assumes "crel (heap f) h h' r"
+lemma effect_heapE [effect_elims]:
+  assumes "effect (heap f) h h' r"
   obtains "h' = snd (f h)" and "r = fst (f h)"
-  using assms by (rule crelE) (simp add: execute_simps)
+  using assms by (rule effectE) (simp add: execute_simps)
 
-lemma crel_guardI [crel_intros]:
+lemma effect_guardI [effect_intros]:
   assumes "P h" "h' = snd (f h)" "r = fst (f h)"
-  shows "crel (guard P f) h h' r"
-  by (rule crelI) (simp add: assms execute_simps)
+  shows "effect (guard P f) h h' r"
+  by (rule effectI) (simp add: assms execute_simps)
 
-lemma crel_guardE [crel_elims]:
-  assumes "crel (guard P f) h h' r"
+lemma effect_guardE [effect_elims]:
+  assumes "effect (guard P f) h h' r"
   obtains "h' = snd (f h)" "r = fst (f h)" "P h"
-  using assms by (rule crelE)
+  using assms by (rule effectE)
     (auto simp add: execute_simps elim!: successE, cases "P h", auto simp add: execute_simps)
 
 
@@ -242,14 +242,14 @@
   "success (return x) h"
   by (rule successI) (simp add: execute_simps)
 
-lemma crel_returnI [crel_intros]:
-  "h = h' \<Longrightarrow> crel (return x) h h' x"
-  by (rule crelI) (simp add: execute_simps)
+lemma effect_returnI [effect_intros]:
+  "h = h' \<Longrightarrow> effect (return x) h h' x"
+  by (rule effectI) (simp add: execute_simps)
 
-lemma crel_returnE [crel_elims]:
-  assumes "crel (return x) h h' r"
+lemma effect_returnE [effect_elims]:
+  assumes "effect (return x) h h' r"
   obtains "r = x" "h' = h"
-  using assms by (rule crelE) (simp add: execute_simps)
+  using assms by (rule effectE) (simp add: execute_simps)
 
 definition raise :: "string \<Rightarrow> 'a Heap" where -- {* the string is just decoration *}
   [code del]: "raise s = Heap (\<lambda>_. None)"
@@ -258,10 +258,10 @@
   "execute (raise s) = (\<lambda>_. None)"
   by (simp add: raise_def)
 
-lemma crel_raiseE [crel_elims]:
-  assumes "crel (raise x) h h' r"
+lemma effect_raiseE [effect_elims]:
+  assumes "effect (raise x) h h' r"
   obtains "False"
-  using assms by (rule crelE) (simp add: success_def execute_simps)
+  using assms by (rule effectE) (simp add: success_def execute_simps)
 
 definition bind :: "'a Heap \<Rightarrow> ('a \<Rightarrow> 'b Heap) \<Rightarrow> 'b Heap" where
   [code del]: "bind f g = Heap (\<lambda>h. case execute f h of
@@ -291,22 +291,22 @@
   "execute f h = Some (x, h') \<Longrightarrow> success (g x) h' \<Longrightarrow> success (f \<guillemotright>= g) h"
   by (auto intro!: successI elim!: successE simp add: bind_def)
 
-lemma success_bind_crelI [success_intros]:
-  "crel f h h' x \<Longrightarrow> success (g x) h' \<Longrightarrow> success (f \<guillemotright>= g) h"
-  by (auto simp add: crel_def success_def bind_def)
+lemma success_bind_effectI [success_intros]:
+  "effect f h h' x \<Longrightarrow> success (g x) h' \<Longrightarrow> success (f \<guillemotright>= g) h"
+  by (auto simp add: effect_def success_def bind_def)
 
-lemma crel_bindI [crel_intros]:
-  assumes "crel f h h' r" "crel (g r) h' h'' r'"
-  shows "crel (f \<guillemotright>= g) h h'' r'"
+lemma effect_bindI [effect_intros]:
+  assumes "effect f h h' r" "effect (g r) h' h'' r'"
+  shows "effect (f \<guillemotright>= g) h h'' r'"
   using assms
-  apply (auto intro!: crelI elim!: crelE successE)
+  apply (auto intro!: effectI elim!: effectE successE)
   apply (subst execute_bind, simp_all)
   done
 
-lemma crel_bindE [crel_elims]:
-  assumes "crel (f \<guillemotright>= g) h h'' r'"
-  obtains h' r where "crel f h h' r" "crel (g r) h' h'' r'"
-  using assms by (auto simp add: crel_def bind_def split: option.split_asm)
+lemma effect_bindE [effect_elims]:
+  assumes "effect (f \<guillemotright>= g) h h'' r'"
+  obtains h' r where "effect f h h' r" "effect (g r) h' h'' r'"
+  using assms by (auto simp add: effect_def bind_def split: option.split_asm)
 
 lemma execute_bind_eq_SomeI:
   assumes "execute f h = Some (x, h')"
@@ -343,14 +343,14 @@
   "P x \<Longrightarrow> success (assert P x) h"
   by (rule successI) (simp add: execute_assert)
 
-lemma crel_assertI [crel_intros]:
-  "P x \<Longrightarrow> h' = h \<Longrightarrow> r = x \<Longrightarrow> crel (assert P x) h h' r"
-  by (rule crelI) (simp add: execute_assert)
+lemma effect_assertI [effect_intros]:
+  "P x \<Longrightarrow> h' = h \<Longrightarrow> r = x \<Longrightarrow> effect (assert P x) h h' r"
+  by (rule effectI) (simp add: execute_assert)
  
-lemma crel_assertE [crel_elims]:
-  assumes "crel (assert P x) h h' r"
+lemma effect_assertE [effect_elims]:
+  assumes "effect (assert P x) h h' r"
   obtains "P x" "r = x" "h' = h"
-  using assms by (rule crelE) (cases "P x", simp_all add: execute_assert success_def)
+  using assms by (rule effectE) (cases "P x", simp_all add: execute_assert success_def)
 
 lemma assert_cong [fundef_cong]:
   assumes "P = P'"
diff -r c059d550afec -r 23904fa13e03 src/HOL/Imperative_HOL/Mrec.thy
--- a/src/HOL/Imperative_HOL/Mrec.thy	Tue Nov 23 23:10:13 2010 +0100
+++ b/src/HOL/Imperative_HOL/Mrec.thy	Tue Nov 23 23:11:06 2010 +0100
@@ -145,20 +145,20 @@
 lemmas MREC_pinduct = mrec.MREC_pinduct
 
 lemma MREC_induct:
-  assumes "crel (MREC f g x) h h' r"
-  assumes "\<And> x h h' r. crel (f x) h h' (Inl r) \<Longrightarrow> P x h h' r"
-  assumes "\<And> x h h1 h2 h' s z r. crel (f x) h h1 (Inr s) \<Longrightarrow> crel (MREC f g s) h1 h2 z \<Longrightarrow> P s h1 h2 z
-    \<Longrightarrow> crel (g x s z) h2 h' r \<Longrightarrow> P x h h' r"
+  assumes "effect (MREC f g x) h h' r"
+  assumes "\<And> x h h' r. effect (f x) h h' (Inl r) \<Longrightarrow> P x h h' r"
+  assumes "\<And> x h h1 h2 h' s z r. effect (f x) h h1 (Inr s) \<Longrightarrow> effect (MREC f g s) h1 h2 z \<Longrightarrow> P s h1 h2 z
+    \<Longrightarrow> effect (g x s z) h2 h' r \<Longrightarrow> P x h h' r"
   shows "P x h h' r"
-proof (rule MREC_pinduct[OF assms(1) [unfolded crel_def]])
+proof (rule MREC_pinduct[OF assms(1) [unfolded effect_def]])
   fix x h h1 h2 h' s z r
   assume "Heap_Monad.execute (f x) h = Some (Inr s, h1)"
     "Heap_Monad.execute (MREC f g s) h1 = Some (z, h2)"
     "P s h1 h2 z"
     "Heap_Monad.execute (g x s z) h2 = Some (r, h')"
-  from assms(3) [unfolded crel_def, OF this(1) this(2) this(3) this(4)]
+  from assms(3) [unfolded effect_def, OF this(1) this(2) this(3) this(4)]
   show "P x h h' r" .
 next
-qed (auto simp add: assms(2)[unfolded crel_def])
+qed (auto simp add: assms(2)[unfolded effect_def])
 
 end
diff -r c059d550afec -r 23904fa13e03 src/HOL/Imperative_HOL/Overview.thy
--- a/src/HOL/Imperative_HOL/Overview.thy	Tue Nov 23 23:10:13 2010 +0100
+++ b/src/HOL/Imperative_HOL/Overview.thy	Tue Nov 23 23:11:06 2010 +0100
@@ -96,13 +96,13 @@
   To establish correctness of imperative programs, predicate
 
   \begin{quote}
-    @{term_type crel}
+    @{term_type effect}
   \end{quote}
 
   provides a simple relational calculus.  Primitive rules are @{text
-  crelI} and @{text crelE}, rules appropriate for reasoning about
-  imperative operations are available in the @{text crel_intros} and
-  @{text crel_elims} fact collections.
+  effectI} and @{text effectE}, rules appropriate for reasoning about
+  imperative operations are available in the @{text effect_intros} and
+  @{text effect_elims} fact collections.
 
   Often non-failure of imperative computations does not depend
   on the heap at all;  reasoning then can be easier using predicate
@@ -114,10 +114,10 @@
   Introduction rules for @{const success} are available in the
   @{text success_intro} fact collection.
 
-  @{const execute}, @{const crel}, @{const success} and @{const bind}
+  @{const execute}, @{const effect}, @{const success} and @{const bind}
   are related by rules @{text execute_bind_success}, @{text
-  success_bind_executeI}, @{text success_bind_crelI}, @{text
-  crel_bindI}, @{text crel_bindE} and @{text execute_bind_eq_SomeI}.
+  success_bind_executeI}, @{text success_bind_effectI}, @{text
+  effect_bindI}, @{text effect_bindE} and @{text execute_bind_eq_SomeI}.
 *}
 
 
@@ -235,7 +235,7 @@
       
     \item Whether one should prefer equational reasoning (fact
       collection @{text execute_simps} or relational reasoning (fact
-      collections @{text crel_intros} and @{text crel_elims}) depends
+      collections @{text effect_intros} and @{text effect_elims}) depends
       on the problems to solve.  For complex expressions or
       expressions involving binders, the relation style usually is
       superior but requires more proof text.
diff -r c059d550afec -r 23904fa13e03 src/HOL/Imperative_HOL/Ref.thy
--- a/src/HOL/Imperative_HOL/Ref.thy	Tue Nov 23 23:10:13 2010 +0100
+++ b/src/HOL/Imperative_HOL/Ref.thy	Tue Nov 23 23:11:06 2010 +0100
@@ -143,15 +143,15 @@
   "success (ref v) h"
   by (auto intro: success_intros simp add: ref_def)
 
-lemma crel_refI [crel_intros]:
+lemma effect_refI [effect_intros]:
   assumes "(r, h') = alloc v h"
-  shows "crel (ref v) h h' r"
-  by (rule crelI) (insert assms, simp add: execute_simps)
+  shows "effect (ref v) h h' r"
+  by (rule effectI) (insert assms, simp add: execute_simps)
 
-lemma crel_refE [crel_elims]:
-  assumes "crel (ref v) h h' r"
+lemma effect_refE [effect_elims]:
+  assumes "effect (ref v) h h' r"
   obtains "get h' r = v" and "present h' r" and "\<not> present h r"
-  using assms by (rule crelE) (simp add: execute_simps)
+  using assms by (rule effectE) (simp add: execute_simps)
 
 lemma execute_lookup [execute_simps]:
   "Heap_Monad.execute (lookup r) h = Some (get h r, h)"
@@ -161,15 +161,15 @@
   "success (lookup r) h"
   by (auto intro: success_intros  simp add: lookup_def)
 
-lemma crel_lookupI [crel_intros]:
+lemma effect_lookupI [effect_intros]:
   assumes "h' = h" "x = get h r"
-  shows "crel (!r) h h' x"
-  by (rule crelI) (insert assms, simp add: execute_simps)
+  shows "effect (!r) h h' x"
+  by (rule effectI) (insert assms, simp add: execute_simps)
 
-lemma crel_lookupE [crel_elims]:
-  assumes "crel (!r) h h' x"
+lemma effect_lookupE [effect_elims]:
+  assumes "effect (!r) h h' x"
   obtains "h' = h" "x = get h r"
-  using assms by (rule crelE) (simp add: execute_simps)
+  using assms by (rule effectE) (simp add: execute_simps)
 
 lemma execute_update [execute_simps]:
   "Heap_Monad.execute (update r v) h = Some ((), set r v h)"
@@ -179,15 +179,15 @@
   "success (update r v) h"
   by (auto intro: success_intros  simp add: update_def)
 
-lemma crel_updateI [crel_intros]:
+lemma effect_updateI [effect_intros]:
   assumes "h' = set r v h"
-  shows "crel (r := v) h h' x"
-  by (rule crelI) (insert assms, simp add: execute_simps)
+  shows "effect (r := v) h h' x"
+  by (rule effectI) (insert assms, simp add: execute_simps)
 
-lemma crel_updateE [crel_elims]:
-  assumes "crel (r' := v) h h' r"
+lemma effect_updateE [effect_elims]:
+  assumes "effect (r' := v) h h' r"
   obtains "h' = set r' v h"
-  using assms by (rule crelE) (simp add: execute_simps)
+  using assms by (rule effectE) (simp add: execute_simps)
 
 lemma execute_change [execute_simps]:
   "Heap_Monad.execute (change f r) h = Some (f (get h r), set r (f (get h r)) h)"
@@ -195,17 +195,17 @@
 
 lemma success_changeI [success_intros]:
   "success (change f r) h"
-  by (auto intro!: success_intros crel_intros simp add: change_def)
+  by (auto intro!: success_intros effect_intros simp add: change_def)
 
-lemma crel_changeI [crel_intros]: 
+lemma effect_changeI [effect_intros]: 
   assumes "h' = set r (f (get h r)) h" "x = f (get h r)"
-  shows "crel (change f r) h h' x"
-  by (rule crelI) (insert assms, simp add: execute_simps)  
+  shows "effect (change f r) h h' x"
+  by (rule effectI) (insert assms, simp add: execute_simps)  
 
-lemma crel_changeE [crel_elims]:
-  assumes "crel (change f r') h h' r"
+lemma effect_changeE [effect_elims]:
+  assumes "effect (change f r') h h' r"
   obtains "h' = set r' (f (get h r')) h" "r = f (get h r')"
-  using assms by (rule crelE) (simp add: execute_simps)
+  using assms by (rule effectE) (simp add: execute_simps)
 
 lemma lookup_chain:
   "(!r \<guillemotright> f) = f"
diff -r c059d550afec -r 23904fa13e03 src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy
--- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Tue Nov 23 23:10:13 2010 +0100
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Tue Nov 23 23:11:06 2010 +0100
@@ -21,20 +21,20 @@
        return ()
      }"
 
-lemma crel_swapI [crel_intros]:
+lemma effect_swapI [effect_intros]:
   assumes "i < Array.length h a" "j < Array.length h a"
     "x = Array.get h a ! i" "y = Array.get h a ! j"
     "h' = Array.update a j x (Array.update a i y h)"
-  shows "crel (swap a i j) h h' r"
-  unfolding swap_def using assms by (auto intro!: crel_intros)
+  shows "effect (swap a i j) h h' r"
+  unfolding swap_def using assms by (auto intro!: effect_intros)
 
 lemma swap_permutes:
-  assumes "crel (swap a i j) h h' rs"
+  assumes "effect (swap a i j) h h' rs"
   shows "multiset_of (Array.get h' a) 
   = multiset_of (Array.get h a)"
   using assms
   unfolding swap_def
-  by (auto simp add: Array.length_def multiset_of_swap dest: sym [of _ "h'"] elim!: crel_bindE crel_nthE crel_returnE crel_updE)
+  by (auto simp add: Array.length_def multiset_of_swap dest: sym [of _ "h'"] elim!: effect_bindE effect_nthE effect_returnE effect_updE)
 
 function part1 :: "nat array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat Heap"
 where
@@ -54,7 +54,7 @@
 declare part1.simps[simp del]
 
 lemma part_permutes:
-  assumes "crel (part1 a l r p) h h' rs"
+  assumes "effect (part1 a l r p) h h' rs"
   shows "multiset_of (Array.get h' a) 
   = multiset_of (Array.get h a)"
   using assms
@@ -62,23 +62,23 @@
   case (1 a l r p h h' rs)
   thus ?case
     unfolding part1.simps [of a l r p]
-    by (elim crel_bindE crel_ifE crel_returnE crel_nthE) (auto simp add: swap_permutes)
+    by (elim effect_bindE effect_ifE effect_returnE effect_nthE) (auto simp add: swap_permutes)
 qed
 
 lemma part_returns_index_in_bounds:
-  assumes "crel (part1 a l r p) h h' rs"
+  assumes "effect (part1 a l r p) h h' rs"
   assumes "l \<le> r"
   shows "l \<le> rs \<and> rs \<le> r"
 using assms
 proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
   case (1 a l r p h h' rs)
-  note cr = `crel (part1 a l r p) h h' rs`
+  note cr = `effect (part1 a l r p) h h' rs`
   show ?case
   proof (cases "r \<le> l")
     case True (* Terminating case *)
     with cr `l \<le> r` show ?thesis
       unfolding part1.simps[of a l r p]
-      by (elim crel_bindE crel_ifE crel_returnE crel_nthE) auto
+      by (elim effect_bindE effect_ifE effect_returnE effect_nthE) auto
   next
     case False (* recursive case *)
     note rec_condition = this
@@ -87,19 +87,19 @@
     proof (cases "?v \<le> p")
       case True
       with cr False
-      have rec1: "crel (part1 a (l + 1) r p) h h' rs"
+      have rec1: "effect (part1 a (l + 1) r p) h h' rs"
         unfolding part1.simps[of a l r p]
-        by (elim crel_bindE crel_nthE crel_ifE crel_returnE) auto
+        by (elim effect_bindE effect_nthE effect_ifE effect_returnE) auto
       from rec_condition have "l + 1 \<le> r" by arith
       from 1(1)[OF rec_condition True rec1 `l + 1 \<le> r`]
       show ?thesis by simp
     next
       case False
       with rec_condition cr
-      obtain h1 where swp: "crel (swap a l r) h h1 ()"
-        and rec2: "crel (part1 a l (r - 1) p) h1 h' rs"
+      obtain h1 where swp: "effect (swap a l r) h h1 ()"
+        and rec2: "effect (part1 a l (r - 1) p) h1 h' rs"
         unfolding part1.simps[of a l r p]
-        by (elim crel_bindE crel_nthE crel_ifE crel_returnE) auto
+        by (elim effect_bindE effect_nthE effect_ifE effect_returnE) auto
       from rec_condition have "l \<le> r - 1" by arith
       from 1(2) [OF rec_condition False rec2 `l \<le> r - 1`] show ?thesis by fastsimp
     qed
@@ -107,41 +107,41 @@
 qed
 
 lemma part_length_remains:
-  assumes "crel (part1 a l r p) h h' rs"
+  assumes "effect (part1 a l r p) h h' rs"
   shows "Array.length h a = Array.length h' a"
 using assms
 proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
   case (1 a l r p h h' rs)
-  note cr = `crel (part1 a l r p) h h' rs`
+  note cr = `effect (part1 a l r p) h h' rs`
   
   show ?case
   proof (cases "r \<le> l")
     case True (* Terminating case *)
     with cr show ?thesis
       unfolding part1.simps[of a l r p]
-      by (elim crel_bindE crel_ifE crel_returnE crel_nthE) auto
+      by (elim effect_bindE effect_ifE effect_returnE effect_nthE) auto
   next
     case False (* recursive case *)
     with cr 1 show ?thesis
       unfolding part1.simps [of a l r p] swap_def
-      by (auto elim!: crel_bindE crel_ifE crel_nthE crel_returnE crel_updE) fastsimp
+      by (auto elim!: effect_bindE effect_ifE effect_nthE effect_returnE effect_updE) fastsimp
   qed
 qed
 
 lemma part_outer_remains:
-  assumes "crel (part1 a l r p) h h' rs"
+  assumes "effect (part1 a l r p) h h' rs"
   shows "\<forall>i. i < l \<or> r < i \<longrightarrow> Array.get h (a::nat array) ! i = Array.get h' a ! i"
   using assms
 proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
   case (1 a l r p h h' rs)
-  note cr = `crel (part1 a l r p) h h' rs`
+  note cr = `effect (part1 a l r p) h h' rs`
   
   show ?case
   proof (cases "r \<le> l")
     case True (* Terminating case *)
     with cr show ?thesis
       unfolding part1.simps[of a l r p]
-      by (elim crel_bindE crel_ifE crel_returnE crel_nthE) auto
+      by (elim effect_bindE effect_ifE effect_returnE effect_nthE) auto
   next
     case False (* recursive case *)
     note rec_condition = this
@@ -150,22 +150,22 @@
     proof (cases "?v \<le> p")
       case True
       with cr False
-      have rec1: "crel (part1 a (l + 1) r p) h h' rs"
+      have rec1: "effect (part1 a (l + 1) r p) h h' rs"
         unfolding part1.simps[of a l r p]
-        by (elim crel_bindE crel_nthE crel_ifE crel_returnE) auto
+        by (elim effect_bindE effect_nthE effect_ifE effect_returnE) auto
       from 1(1)[OF rec_condition True rec1]
       show ?thesis by fastsimp
     next
       case False
       with rec_condition cr
-      obtain h1 where swp: "crel (swap a l r) h h1 ()"
-        and rec2: "crel (part1 a l (r - 1) p) h1 h' rs"
+      obtain h1 where swp: "effect (swap a l r) h h1 ()"
+        and rec2: "effect (part1 a l (r - 1) p) h1 h' rs"
         unfolding part1.simps[of a l r p]
-        by (elim crel_bindE crel_nthE crel_ifE crel_returnE) auto
+        by (elim effect_bindE effect_nthE effect_ifE effect_returnE) auto
       from swp rec_condition have
         "\<forall>i. i < l \<or> r < i \<longrightarrow> Array.get h a ! i = Array.get h1 a ! i"
         unfolding swap_def
-        by (elim crel_bindE crel_nthE crel_updE crel_returnE) auto
+        by (elim effect_bindE effect_nthE effect_updE effect_returnE) auto
       with 1(2) [OF rec_condition False rec2] show ?thesis by fastsimp
     qed
   qed
@@ -173,20 +173,20 @@
 
 
 lemma part_partitions:
-  assumes "crel (part1 a l r p) h h' rs"
+  assumes "effect (part1 a l r p) h h' rs"
   shows "(\<forall>i. l \<le> i \<and> i < rs \<longrightarrow> Array.get h' (a::nat array) ! i \<le> p)
   \<and> (\<forall>i. rs < i \<and> i \<le> r \<longrightarrow> Array.get h' a ! i \<ge> p)"
   using assms
 proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
   case (1 a l r p h h' rs)
-  note cr = `crel (part1 a l r p) h h' rs`
+  note cr = `effect (part1 a l r p) h h' rs`
   
   show ?case
   proof (cases "r \<le> l")
     case True (* Terminating case *)
     with cr have "rs = r"
       unfolding part1.simps[of a l r p]
-      by (elim crel_bindE crel_ifE crel_returnE crel_nthE) auto
+      by (elim effect_bindE effect_ifE effect_returnE effect_nthE) auto
     with True
     show ?thesis by auto
   next
@@ -197,9 +197,9 @@
     proof (cases "?v \<le> p")
       case True
       with lr cr
-      have rec1: "crel (part1 a (l + 1) r p) h h' rs"
+      have rec1: "effect (part1 a (l + 1) r p) h h' rs"
         unfolding part1.simps[of a l r p]
-        by (elim crel_bindE crel_nthE crel_ifE crel_returnE) auto
+        by (elim effect_bindE effect_nthE effect_ifE effect_returnE) auto
       from True part_outer_remains[OF rec1] have a_l: "Array.get h' a ! l \<le> p"
         by fastsimp
       have "\<forall>i. (l \<le> i = (l = i \<or> Suc l \<le> i))" by arith
@@ -208,13 +208,13 @@
     next
       case False
       with lr cr
-      obtain h1 where swp: "crel (swap a l r) h h1 ()"
-        and rec2: "crel (part1 a l (r - 1) p) h1 h' rs"
+      obtain h1 where swp: "effect (swap a l r) h h1 ()"
+        and rec2: "effect (part1 a l (r - 1) p) h1 h' rs"
         unfolding part1.simps[of a l r p]
-        by (elim crel_bindE crel_nthE crel_ifE crel_returnE) auto
+        by (elim effect_bindE effect_nthE effect_ifE effect_returnE) auto
       from swp False have "Array.get h1 a ! r \<ge> p"
         unfolding swap_def
-        by (auto simp add: Array.length_def elim!: crel_bindE crel_nthE crel_updE crel_returnE)
+        by (auto simp add: Array.length_def elim!: effect_bindE effect_nthE effect_updE effect_returnE)
       with part_outer_remains [OF rec2] lr have a_r: "Array.get h' a ! r \<ge> p"
         by fastsimp
       have "\<forall>i. (i \<le> r = (i = r \<or> i \<le> r - 1))" by arith
@@ -239,70 +239,70 @@
 declare partition.simps[simp del]
 
 lemma partition_permutes:
-  assumes "crel (partition a l r) h h' rs"
+  assumes "effect (partition a l r) h h' rs"
   shows "multiset_of (Array.get h' a) 
   = multiset_of (Array.get h a)"
 proof -
     from assms part_permutes swap_permutes show ?thesis
       unfolding partition.simps
-      by (elim crel_bindE crel_returnE crel_nthE crel_ifE crel_updE) auto
+      by (elim effect_bindE effect_returnE effect_nthE effect_ifE effect_updE) auto
 qed
 
 lemma partition_length_remains:
-  assumes "crel (partition a l r) h h' rs"
+  assumes "effect (partition a l r) h h' rs"
   shows "Array.length h a = Array.length h' a"
 proof -
   from assms part_length_remains show ?thesis
     unfolding partition.simps swap_def
-    by (elim crel_bindE crel_returnE crel_nthE crel_ifE crel_updE) auto
+    by (elim effect_bindE effect_returnE effect_nthE effect_ifE effect_updE) auto
 qed
 
 lemma partition_outer_remains:
-  assumes "crel (partition a l r) h h' rs"
+  assumes "effect (partition a l r) h h' rs"
   assumes "l < r"
   shows "\<forall>i. i < l \<or> r < i \<longrightarrow> Array.get h (a::nat array) ! i = Array.get h' a ! i"
 proof -
   from assms part_outer_remains part_returns_index_in_bounds show ?thesis
     unfolding partition.simps swap_def
-    by (elim crel_bindE crel_returnE crel_nthE crel_ifE crel_updE) fastsimp
+    by (elim effect_bindE effect_returnE effect_nthE effect_ifE effect_updE) fastsimp
 qed
 
 lemma partition_returns_index_in_bounds:
-  assumes crel: "crel (partition a l r) h h' rs"
+  assumes effect: "effect (partition a l r) h h' rs"
   assumes "l < r"
   shows "l \<le> rs \<and> rs \<le> r"
 proof -
-  from crel obtain middle h'' p where part: "crel (part1 a l (r - 1) p) h h'' middle"
+  from effect obtain middle h'' p where part: "effect (part1 a l (r - 1) p) h h'' middle"
     and rs_equals: "rs = (if Array.get h'' a ! middle \<le> Array.get h a ! r then middle + 1
          else middle)"
     unfolding partition.simps
-    by (elim crel_bindE crel_returnE crel_nthE crel_ifE crel_updE) simp 
+    by (elim effect_bindE effect_returnE effect_nthE effect_ifE effect_updE) simp 
   from `l < r` have "l \<le> r - 1" by arith
   from part_returns_index_in_bounds[OF part this] rs_equals `l < r` show ?thesis by auto
 qed
 
 lemma partition_partitions:
-  assumes crel: "crel (partition a l r) h h' rs"
+  assumes effect: "effect (partition a l r) h h' rs"
   assumes "l < r"
   shows "(\<forall>i. l \<le> i \<and> i < rs \<longrightarrow> Array.get h' (a::nat array) ! i \<le> Array.get h' a ! rs) \<and>
   (\<forall>i. rs < i \<and> i \<le> r \<longrightarrow> Array.get h' a ! rs \<le> Array.get h' a ! i)"
 proof -
   let ?pivot = "Array.get h a ! r" 
-  from crel obtain middle h1 where part: "crel (part1 a l (r - 1) ?pivot) h h1 middle"
-    and swap: "crel (swap a rs r) h1 h' ()"
+  from effect obtain middle h1 where part: "effect (part1 a l (r - 1) ?pivot) h h1 middle"
+    and swap: "effect (swap a rs r) h1 h' ()"
     and rs_equals: "rs = (if Array.get h1 a ! middle \<le> ?pivot then middle + 1
          else middle)"
     unfolding partition.simps
-    by (elim crel_bindE crel_returnE crel_nthE crel_ifE crel_updE) simp
+    by (elim effect_bindE effect_returnE effect_nthE effect_ifE effect_updE) simp
   from swap have h'_def: "h' = Array.update a r (Array.get h1 a ! rs)
     (Array.update a rs (Array.get h1 a ! r) h1)"
     unfolding swap_def
-    by (elim crel_bindE crel_returnE crel_nthE crel_updE) simp
+    by (elim effect_bindE effect_returnE effect_nthE effect_updE) simp
   from swap have in_bounds: "r < Array.length h1 a \<and> rs < Array.length h1 a"
     unfolding swap_def
-    by (elim crel_bindE crel_returnE crel_nthE crel_updE) simp
+    by (elim effect_bindE effect_returnE effect_nthE effect_updE) simp
   from swap have swap_length_remains: "Array.length h1 a = Array.length h' a"
-    unfolding swap_def by (elim crel_bindE crel_returnE crel_nthE crel_updE) auto
+    unfolding swap_def by (elim effect_bindE effect_returnE effect_nthE effect_updE) auto
   from `l < r` have "l \<le> r - 1" by simp
   note middle_in_bounds = part_returns_index_in_bounds[OF part this]
   from part_outer_remains[OF part] `l < r`
@@ -311,7 +311,7 @@
   with swap
   have right_remains: "Array.get h a ! r = Array.get h' a ! rs"
     unfolding swap_def
-    by (auto simp add: Array.length_def elim!: crel_bindE crel_returnE crel_nthE crel_updE) (cases "r = rs", auto)
+    by (auto simp add: Array.length_def elim!: effect_bindE effect_returnE effect_nthE effect_updE) (cases "r = rs", auto)
   from part_partitions [OF part]
   show ?thesis
   proof (cases "Array.get h1 a ! middle \<le> ?pivot")
@@ -419,7 +419,7 @@
 
 
 lemma quicksort_permutes:
-  assumes "crel (quicksort a l r) h h' rs"
+  assumes "effect (quicksort a l r) h h' rs"
   shows "multiset_of (Array.get h' a) 
   = multiset_of (Array.get h a)"
   using assms
@@ -427,41 +427,41 @@
   case (1 a l r h h' rs)
   with partition_permutes show ?case
     unfolding quicksort.simps [of a l r]
-    by (elim crel_ifE crel_bindE crel_assertE crel_returnE) auto
+    by (elim effect_ifE effect_bindE effect_assertE effect_returnE) auto
 qed
 
 lemma length_remains:
-  assumes "crel (quicksort a l r) h h' rs"
+  assumes "effect (quicksort a l r) h h' rs"
   shows "Array.length h a = Array.length h' a"
 using assms
 proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
   case (1 a l r h h' rs)
   with partition_length_remains show ?case
     unfolding quicksort.simps [of a l r]
-    by (elim crel_ifE crel_bindE crel_assertE crel_returnE) auto
+    by (elim effect_ifE effect_bindE effect_assertE effect_returnE) auto
 qed
 
 lemma quicksort_outer_remains:
-  assumes "crel (quicksort a l r) h h' rs"
+  assumes "effect (quicksort a l r) h h' rs"
    shows "\<forall>i. i < l \<or> r < i \<longrightarrow> Array.get h (a::nat array) ! i = Array.get h' a ! i"
   using assms
 proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
   case (1 a l r h h' rs)
-  note cr = `crel (quicksort a l r) h h' rs`
+  note cr = `effect (quicksort a l r) h h' rs`
   thus ?case
   proof (cases "r > l")
     case False
     with cr have "h' = h"
       unfolding quicksort.simps [of a l r]
-      by (elim crel_ifE crel_returnE) auto
+      by (elim effect_ifE effect_returnE) auto
     thus ?thesis by simp
   next
   case True
    { 
       fix h1 h2 p ret1 ret2 i
-      assume part: "crel (partition a l r) h h1 p"
-      assume qs1: "crel (quicksort a l (p - 1)) h1 h2 ret1"
-      assume qs2: "crel (quicksort a (p + 1) r) h2 h' ret2"
+      assume part: "effect (partition a l r) h h1 p"
+      assume qs1: "effect (quicksort a l (p - 1)) h1 h2 ret1"
+      assume qs2: "effect (quicksort a (p + 1) r) h2 h' ret2"
       assume pivot: "l \<le> p \<and> p \<le> r"
       assume i_outer: "i < l \<or> r < i"
       from  partition_outer_remains [OF part True] i_outer
@@ -476,25 +476,25 @@
     }
     with cr show ?thesis
       unfolding quicksort.simps [of a l r]
-      by (elim crel_ifE crel_bindE crel_assertE crel_returnE) auto
+      by (elim effect_ifE effect_bindE effect_assertE effect_returnE) auto
   qed
 qed
 
 lemma quicksort_is_skip:
-  assumes "crel (quicksort a l r) h h' rs"
+  assumes "effect (quicksort a l r) h h' rs"
   shows "r \<le> l \<longrightarrow> h = h'"
   using assms
   unfolding quicksort.simps [of a l r]
-  by (elim crel_ifE crel_returnE) auto
+  by (elim effect_ifE effect_returnE) auto
  
 lemma quicksort_sorts:
-  assumes "crel (quicksort a l r) h h' rs"
+  assumes "effect (quicksort a l r) h h' rs"
   assumes l_r_length: "l < Array.length h a" "r < Array.length h a" 
   shows "sorted (subarray l (r + 1) a h')"
   using assms
 proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
   case (1 a l r h h' rs)
-  note cr = `crel (quicksort a l r) h h' rs`
+  note cr = `effect (quicksort a l r) h h' rs`
   thus ?case
   proof (cases "r > l")
     case False
@@ -505,9 +505,9 @@
     case True
     { 
       fix h1 h2 p
-      assume part: "crel (partition a l r) h h1 p"
-      assume qs1: "crel (quicksort a l (p - 1)) h1 h2 ()"
-      assume qs2: "crel (quicksort a (p + 1) r) h2 h' ()"
+      assume part: "effect (partition a l r) h h1 p"
+      assume qs1: "effect (quicksort a l (p - 1)) h1 h2 ()"
+      assume qs2: "effect (quicksort a (p + 1) r) h2 h' ()"
       from partition_returns_index_in_bounds [OF part True]
       have pivot: "l\<le> p \<and> p \<le> r" .
      note length_remains = length_remains[OF qs2] length_remains[OF qs1] partition_length_remains[OF part]
@@ -557,25 +557,25 @@
     }
     with True cr show ?thesis
       unfolding quicksort.simps [of a l r]
-      by (elim crel_ifE crel_returnE crel_bindE crel_assertE) auto
+      by (elim effect_ifE effect_returnE effect_bindE effect_assertE) auto
   qed
 qed
 
 
 lemma quicksort_is_sort:
-  assumes crel: "crel (quicksort a 0 (Array.length h a - 1)) h h' rs"
+  assumes effect: "effect (quicksort a 0 (Array.length h a - 1)) h h' rs"
   shows "Array.get h' a = sort (Array.get h a)"
 proof (cases "Array.get h a = []")
   case True
-  with quicksort_is_skip[OF crel] show ?thesis
+  with quicksort_is_skip[OF effect] show ?thesis
   unfolding Array.length_def by simp
 next
   case False
-  from quicksort_sorts [OF crel] False have "sorted (sublist' 0 (List.length (Array.get h a)) (Array.get h' a))"
+  from quicksort_sorts [OF effect] False have "sorted (sublist' 0 (List.length (Array.get h a)) (Array.get h' a))"
     unfolding Array.length_def subarray_def by auto
-  with length_remains[OF crel] have "sorted (Array.get h' a)"
+  with length_remains[OF effect] have "sorted (Array.get h' a)"
     unfolding Array.length_def by simp
-  with quicksort_permutes [OF crel] properties_for_sort show ?thesis by fastsimp
+  with quicksort_permutes [OF effect] properties_for_sort show ?thesis by fastsimp
 qed
 
 subsection {* No Errors in quicksort *}
@@ -590,26 +590,26 @@
   case (1 a l r p)
   thus ?case unfolding part1.simps [of a l r]
   apply (auto intro!: success_intros del: success_ifI simp add: not_le)
-  apply (auto intro!: crel_intros crel_swapI)
+  apply (auto intro!: effect_intros effect_swapI)
   done
 qed
 
 lemma success_bindI' [success_intros]: (*FIXME move*)
   assumes "success f h"
-  assumes "\<And>h' r. crel f h h' r \<Longrightarrow> success (g r) h'"
+  assumes "\<And>h' r. effect f h h' r \<Longrightarrow> success (g r) h'"
   shows "success (f \<guillemotright>= g) h"
-using assms(1) proof (rule success_crelE)
+using assms(1) proof (rule success_effectE)
   fix h' r
-  assume "crel f h h' r"
+  assume "effect f h h' r"
   moreover with assms(2) have "success (g r) h'" .
-  ultimately show "success (f \<guillemotright>= g) h" by (rule success_bind_crelI)
+  ultimately show "success (f \<guillemotright>= g) h" by (rule success_bind_effectI)
 qed
 
 lemma success_partitionI:
   assumes "l < r" "l < Array.length h a" "r < Array.length h a"
   shows "success (partition a l r) h"
 using assms unfolding partition.simps swap_def
-apply (auto intro!: success_bindI' success_ifI success_returnI success_nthI success_updI success_part1I elim!: crel_bindE crel_updE crel_nthE crel_returnE simp add:)
+apply (auto intro!: success_bindI' success_ifI success_returnI success_nthI success_updI success_part1I elim!: effect_bindE effect_updE effect_nthE effect_returnE simp add:)
 apply (frule part_length_remains)
 apply (frule part_returns_index_in_bounds)
 apply auto
@@ -633,7 +633,7 @@
     apply auto
     apply (frule partition_returns_index_in_bounds)
     apply auto
-    apply (auto elim!: crel_assertE dest!: partition_length_remains length_remains)
+    apply (auto elim!: effect_assertE dest!: partition_length_remains length_remains)
     apply (subgoal_tac "Suc r \<le> ri \<or> r = ri") 
     apply (erule disjE)
     apply auto
diff -r c059d550afec -r 23904fa13e03 src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy
--- a/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy	Tue Nov 23 23:10:13 2010 +0100
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy	Tue Nov 23 23:11:06 2010 +0100
@@ -26,15 +26,15 @@
 
 declare swap.simps [simp del] rev.simps [simp del]
 
-lemma swap_pointwise: assumes "crel (swap a i j) h h' r"
+lemma swap_pointwise: assumes "effect (swap a i j) h h' r"
   shows "Array.get h' a ! k = (if k = i then Array.get h a ! j
       else if k = j then Array.get h a ! i
       else Array.get h a ! k)"
 using assms unfolding swap.simps
-by (elim crel_elims)
+by (elim effect_elims)
  (auto simp: length_def)
 
-lemma rev_pointwise: assumes "crel (rev a i j) h h' r"
+lemma rev_pointwise: assumes "effect (rev a i j) h h' r"
   shows "Array.get h' a ! k = (if k < i then Array.get h a ! k
       else if j < k then Array.get h a ! k
       else Array.get h a ! (j - (k - i)))" (is "?P a i j h h'")
@@ -45,9 +45,9 @@
     case True
     with 1[unfolded rev.simps[of a i j]]
     obtain h' where
-      swp: "crel (swap a i j) h h' ()"
-      and rev: "crel (rev a (i + 1) (j - 1)) h' h'' ()"
-      by (auto elim: crel_elims)
+      swp: "effect (swap a i j) h h' ()"
+      and rev: "effect (rev a (i + 1) (j - 1)) h' h'' ()"
+      by (auto elim: effect_elims)
     from rev 1 True
     have eq: "?P a (i + 1) (j - 1) h' h''" by auto
 
@@ -58,12 +58,12 @@
     case False
     with 1[unfolded rev.simps[of a i j]]
     show ?thesis
-      by (cases "k = j") (auto elim: crel_elims)
+      by (cases "k = j") (auto elim: effect_elims)
   qed
 qed
 
 lemma rev_length:
-  assumes "crel (rev a i j) h h' r"
+  assumes "effect (rev a i j) h h' r"
   shows "Array.length h a = Array.length h' a"
 using assms
 proof (induct a i j arbitrary: h h' rule: rev.induct)
@@ -73,21 +73,21 @@
     case True
     with 1[unfolded rev.simps[of a i j]]
     obtain h' where
-      swp: "crel (swap a i j) h h' ()"
-      and rev: "crel (rev a (i + 1) (j - 1)) h' h'' ()"
-      by (auto elim: crel_elims)
+      swp: "effect (swap a i j) h h' ()"
+      and rev: "effect (rev a (i + 1) (j - 1)) h' h'' ()"
+      by (auto elim: effect_elims)
     from swp rev 1 True show ?thesis
       unfolding swap.simps
-      by (elim crel_elims) fastsimp
+      by (elim effect_elims) fastsimp
   next
     case False
     with 1[unfolded rev.simps[of a i j]]
     show ?thesis
-      by (auto elim: crel_elims)
+      by (auto elim: effect_elims)
   qed
 qed
 
-lemma rev2_rev': assumes "crel (rev a i j) h h' u"
+lemma rev2_rev': assumes "effect (rev a i j) h h' u"
   assumes "j < Array.length h a"
   shows "subarray i (j + 1) a h' = List.rev (subarray i (j + 1) a h)"
 proof - 
@@ -103,11 +103,11 @@
 qed
 
 lemma rev2_rev: 
-  assumes "crel (rev a 0 (Array.length h a - 1)) h h' u"
+  assumes "effect (rev a 0 (Array.length h a - 1)) h h' u"
   shows "Array.get h' a = List.rev (Array.get h a)"
   using rev2_rev'[OF assms] rev_length[OF assms] assms
     by (cases "Array.length h a = 0", auto simp add: Array.length_def
-      subarray_def sublist'_all rev.simps[where j=0] elim!: crel_elims)
+      subarray_def sublist'_all rev.simps[where j=0] elim!: effect_elims)
   (drule sym[of "List.length (Array.get h a)"], simp)
 
 definition "example = (Array.make 10 id \<guillemotright>= (\<lambda>a. rev a 0 9))"
diff -r c059d550afec -r 23904fa13e03 src/HOL/Imperative_HOL/ex/Linked_Lists.thy
--- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Tue Nov 23 23:10:13 2010 +0100
+++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Tue Nov 23 23:11:06 2010 +0100
@@ -448,8 +448,8 @@
     by simp
 qed
 
-lemma crel_ref:
-  assumes "crel (ref v) h h' x"
+lemma effect_ref:
+  assumes "effect (ref v) h h' x"
   obtains "Ref.get h' x = v"
   and "\<not> Ref.present h x"
   and "Ref.present h' x"
@@ -458,7 +458,7 @@
   and "\<forall>y. Ref.present h y \<longrightarrow> Ref.present h' y"
   using assms
   unfolding Ref.ref_def
-  apply (elim crel_heapE)
+  apply (elim effect_heapE)
   unfolding Ref.alloc_def
   apply (simp add: Let_def)
   unfolding Ref.present_def
@@ -468,56 +468,56 @@
   done
 
 lemma make_llist:
-assumes "crel (make_llist xs) h h' r"
+assumes "effect (make_llist xs) h h' r"
 shows "list_of h' r xs \<and> (\<forall>rs. refs_of h' r rs \<longrightarrow> (\<forall>ref \<in> (set rs). Ref.present h' ref))"
 using assms 
 proof (induct xs arbitrary: h h' r)
-  case Nil thus ?case by (auto elim: crel_returnE simp add: make_llist.simps)
+  case Nil thus ?case by (auto elim: effect_returnE simp add: make_llist.simps)
 next
   case (Cons x xs')
-  from Cons.prems obtain h1 r1 r' where make_llist: "crel (make_llist xs') h h1 r1"
-    and crel_refnew:"crel (ref r1) h1 h' r'" and Node: "r = Node x r'"
+  from Cons.prems obtain h1 r1 r' where make_llist: "effect (make_llist xs') h h1 r1"
+    and effect_refnew:"effect (ref r1) h1 h' r'" and Node: "r = Node x r'"
     unfolding make_llist.simps
-    by (auto elim!: crel_bindE crel_returnE)
+    by (auto elim!: effect_bindE effect_returnE)
   from Cons.hyps[OF make_llist] have list_of_h1: "list_of h1 r1 xs'" ..
   from Cons.hyps[OF make_llist] obtain rs' where rs'_def: "refs_of h1 r1 rs'" by (auto intro: list_of_refs_of)
   from Cons.hyps[OF make_llist] rs'_def have refs_present: "\<forall>ref\<in>set rs'. Ref.present h1 ref" by simp
-  from crel_refnew rs'_def refs_present have refs_unchanged: "\<forall>refs. refs_of h1 r1 refs \<longrightarrow>
+  from effect_refnew rs'_def refs_present have refs_unchanged: "\<forall>refs. refs_of h1 r1 refs \<longrightarrow>
          (\<forall>ref\<in>set refs. Ref.present h1 ref \<and> Ref.present h' ref \<and> Ref.get h1 ref = Ref.get h' ref)"
-    by (auto elim!: crel_ref dest: refs_of_is_fun)
-  with list_of_invariant[OF list_of_h1 refs_unchanged] Node crel_refnew have fstgoal: "list_of h' r (x # xs')"
+    by (auto elim!: effect_ref dest: refs_of_is_fun)
+  with list_of_invariant[OF list_of_h1 refs_unchanged] Node effect_refnew have fstgoal: "list_of h' r (x # xs')"
     unfolding list_of.simps
-    by (auto elim!: crel_refE)
+    by (auto elim!: effect_refE)
   from refs_unchanged rs'_def have refs_still_present: "\<forall>ref\<in>set rs'. Ref.present h' ref" by auto
-  from refs_of_invariant[OF rs'_def refs_unchanged] refs_unchanged Node crel_refnew refs_still_present
+  from refs_of_invariant[OF rs'_def refs_unchanged] refs_unchanged Node effect_refnew refs_still_present
   have sndgoal: "\<forall>rs. refs_of h' r rs \<longrightarrow> (\<forall>ref\<in>set rs. Ref.present h' ref)"
-    by (fastsimp elim!: crel_refE dest: refs_of_is_fun)
+    by (fastsimp elim!: effect_refE dest: refs_of_is_fun)
   from fstgoal sndgoal show ?case ..
 qed
 
-lemma traverse: "list_of h n r \<Longrightarrow> crel (traverse n) h h r"
+lemma traverse: "list_of h n r \<Longrightarrow> effect (traverse n) h h r"
 proof (induct r arbitrary: n)
   case Nil
   thus ?case
-    by (auto intro: crel_returnI)
+    by (auto intro: effect_returnI)
 next
   case (Cons x xs)
   thus ?case
   apply (cases n, auto)
-  by (auto intro!: crel_bindI crel_returnI crel_lookupI)
+  by (auto intro!: effect_bindI effect_returnI effect_lookupI)
 qed
 
 lemma traverse_make_llist':
-  assumes crel: "crel (make_llist xs \<guillemotright>= traverse) h h' r"
+  assumes effect: "effect (make_llist xs \<guillemotright>= traverse) h h' r"
   shows "r = xs"
 proof -
-  from crel obtain h1 r1
-    where makell: "crel (make_llist xs) h h1 r1"
-    and trav: "crel (traverse r1) h1 h' r"
-    by (auto elim!: crel_bindE)
+  from effect obtain h1 r1
+    where makell: "effect (make_llist xs) h h1 r1"
+    and trav: "effect (traverse r1) h1 h' r"
+    by (auto elim!: effect_bindE)
   from make_llist[OF makell] have "list_of h1 r1 xs" ..
   from traverse [OF this] trav show ?thesis
-    using crel_deterministic by fastsimp
+    using effect_deterministic by fastsimp
 qed
 
 section {* Proving correctness of in-place reversal *}
@@ -546,7 +546,7 @@
 subsection {* Correctness Proof *}
 
 lemma rev'_invariant:
-  assumes "crel (rev' q p) h h' v"
+  assumes "effect (rev' q p) h h' v"
   assumes "list_of' h q qs"
   assumes "list_of' h p ps"
   assumes "\<forall>qrs prs. refs_of' h q qrs \<and> refs_of' h p prs \<longrightarrow> set prs \<inter> set qrs = {}"
@@ -556,7 +556,7 @@
   case Nil
   thus ?case
     unfolding rev'.simps[of q p] list_of'_def
-    by (auto elim!: crel_bindE crel_lookupE crel_returnE)
+    by (auto elim!: effect_bindE effect_lookupE effect_returnE)
 next
   case (Cons x xs)
   (*"LinkedList.list_of h' (get_ref v h') (List.rev xs @ x # qsa)"*)
@@ -565,8 +565,8 @@
     (*and "ref_present ref h"*)
     and list_of'_ref: "list_of' h ref xs"
     unfolding list_of'_def by (cases "Ref.get h p", auto)
-  from p_is_Node Cons(2) have crel_rev': "crel (rev' p ref) (Ref.set p (Node x q) h) h' v"
-    by (auto simp add: rev'.simps [of q p] elim!: crel_bindE crel_lookupE crel_updateE)
+  from p_is_Node Cons(2) have effect_rev': "effect (rev' p ref) (Ref.set p (Node x q) h) h' v"
+    by (auto simp add: rev'.simps [of q p] elim!: effect_bindE effect_lookupE effect_updateE)
   from Cons(3) obtain qrs where qrs_def: "refs_of' h q qrs" by (elim list_of'_refs_of')
   from Cons(4) obtain prs where prs_def: "refs_of' h p prs" by (elim list_of'_refs_of')
   from qrs_def prs_def Cons(5) have distinct_pointers: "set qrs \<inter> set prs = {}" by fastsimp
@@ -594,60 +594,60 @@
     apply (drule refs_of'_is_fun) back back apply assumption
     apply (drule refs_of'_is_fun) back back apply assumption
     apply auto done
-  from Cons.hyps [OF crel_rev' 1 2 3] show ?case by simp
+  from Cons.hyps [OF effect_rev' 1 2 3] show ?case by simp
 qed
 
 
 lemma rev_correctness:
   assumes list_of_h: "list_of h r xs"
   assumes validHeap: "\<forall>refs. refs_of h r refs \<longrightarrow> (\<forall>r \<in> set refs. Ref.present h r)"
-  assumes crel_rev: "crel (rev r) h h' r'"
+  assumes effect_rev: "effect (rev r) h h' r'"
   shows "list_of h' r' (List.rev xs)"
 using assms
 proof (cases r)
   case Empty
-  with list_of_h crel_rev show ?thesis
-    by (auto simp add: list_of_Empty elim!: crel_returnE)
+  with list_of_h effect_rev show ?thesis
+    by (auto simp add: list_of_Empty elim!: effect_returnE)
 next
   case (Node x ps)
-  with crel_rev obtain p q h1 h2 h3 v where
-    init: "crel (ref Empty) h h1 q"
-    "crel (ref (Node x ps)) h1 h2 p"
-    and crel_rev':"crel (rev' q p) h2 h3 v"
-    and lookup: "crel (!v) h3 h' r'"
+  with effect_rev obtain p q h1 h2 h3 v where
+    init: "effect (ref Empty) h h1 q"
+    "effect (ref (Node x ps)) h1 h2 p"
+    and effect_rev':"effect (rev' q p) h2 h3 v"
+    and lookup: "effect (!v) h3 h' r'"
     using rev.simps
-    by (auto elim!: crel_bindE)
+    by (auto elim!: effect_bindE)
   from init have a1:"list_of' h2 q []"
     unfolding list_of'_def
-    by (auto elim!: crel_ref)
+    by (auto elim!: effect_ref)
   from list_of_h obtain refs where refs_def: "refs_of h r refs" by (rule list_of_refs_of)
   from validHeap init refs_def have heap_eq: "\<forall>refs. refs_of h r refs \<longrightarrow> (\<forall>ref\<in>set refs. Ref.present h ref \<and> Ref.present h2 ref \<and> Ref.get h ref = Ref.get h2 ref)"
-    by (fastsimp elim!: crel_ref dest: refs_of_is_fun)
+    by (fastsimp elim!: effect_ref dest: refs_of_is_fun)
   from list_of_invariant[OF list_of_h heap_eq] have "list_of h2 r xs" .
   from init this Node have a2: "list_of' h2 p xs"
     apply -
     unfolding list_of'_def
-    apply (auto elim!: crel_refE)
+    apply (auto elim!: effect_refE)
     done
   from init have refs_of_q: "refs_of' h2 q [q]"
-    by (auto elim!: crel_ref)
+    by (auto elim!: effect_ref)
   from refs_def Node have refs_of'_ps: "refs_of' h ps refs"
     by (auto simp add: refs_of'_def'[symmetric])
   from validHeap refs_def have all_ref_present: "\<forall>r\<in>set refs. Ref.present h r" by simp
   from init refs_of'_ps this
     have heap_eq: "\<forall>refs. refs_of' h ps refs \<longrightarrow> (\<forall>ref\<in>set refs. Ref.present h ref \<and> Ref.present h2 ref \<and> Ref.get h ref = Ref.get h2 ref)"
-    by (auto elim!: crel_ref [where ?'a="'a node", where ?'b="'a node", where ?'c="'a node"] dest: refs_of'_is_fun)
+    by (auto elim!: effect_ref [where ?'a="'a node", where ?'b="'a node", where ?'c="'a node"] dest: refs_of'_is_fun)
   from refs_of'_invariant[OF refs_of'_ps this] have "refs_of' h2 ps refs" .
   with init have refs_of_p: "refs_of' h2 p (p#refs)"
-    by (auto elim!: crel_refE simp add: refs_of'_def')
+    by (auto elim!: effect_refE simp add: refs_of'_def')
   with init all_ref_present have q_is_new: "q \<notin> set (p#refs)"
-    by (auto elim!: crel_refE intro!: Ref.noteq_I)
+    by (auto elim!: effect_refE intro!: Ref.noteq_I)
   from refs_of_p refs_of_q q_is_new have a3: "\<forall>qrs prs. refs_of' h2 q qrs \<and> refs_of' h2 p prs \<longrightarrow> set prs \<inter> set qrs = {}"
     by (fastsimp simp only: set.simps dest: refs_of'_is_fun)
-  from rev'_invariant [OF crel_rev' a1 a2 a3] have "list_of h3 (Ref.get h3 v) (List.rev xs)" 
+  from rev'_invariant [OF effect_rev' a1 a2 a3] have "list_of h3 (Ref.get h3 v) (List.rev xs)" 
     unfolding list_of'_def by auto
   with lookup show ?thesis
-    by (auto elim: crel_lookupE)
+    by (auto elim: effect_lookupE)
 qed
 
 
@@ -780,21 +780,21 @@
 qed
 
 
-text {* secondly, we add the crel statement in the premise, and derive the crel statements for the single cases which we then eliminate with our crel elim rules. *}
+text {* secondly, we add the effect statement in the premise, and derive the effect statements for the single cases which we then eliminate with our effect elim rules. *}
   
 lemma merge_induct3: 
 assumes  "list_of' h p xs"
 assumes  "list_of' h q ys"
-assumes  "crel (merge p q) h h' r"
+assumes  "effect (merge p q) h h' r"
 assumes  "\<And> ys p q. \<lbrakk> list_of' h p []; list_of' h q ys; Ref.get h p = Empty \<rbrakk> \<Longrightarrow> P p q h h q [] ys"
 assumes  "\<And> x xs' p q pn. \<lbrakk> list_of' h p (x#xs'); list_of' h q []; Ref.get h p = Node x pn; Ref.get h q = Empty \<rbrakk> \<Longrightarrow> P p q h h p (x#xs') []"
 assumes  "\<And> x xs' y ys' p q pn qn h1 r1 h'.
   \<lbrakk> list_of' h p (x#xs'); list_of' h q (y#ys');Ref.get h p = Node x pn; Ref.get h q = Node y qn;
-  x \<le> y; crel (merge pn q) h h1 r1 ; P pn q h h1 r1 xs' (y#ys'); h' = Ref.set p (Node x r1) h1 \<rbrakk>
+  x \<le> y; effect (merge pn q) h h1 r1 ; P pn q h h1 r1 xs' (y#ys'); h' = Ref.set p (Node x r1) h1 \<rbrakk>
   \<Longrightarrow> P p q h h' p (x#xs') (y#ys')"
 assumes "\<And> x xs' y ys' p q pn qn h1 r1 h'.
   \<lbrakk> list_of' h p (x#xs'); list_of' h q (y#ys'); Ref.get h p = Node x pn; Ref.get h q = Node y qn;
-  \<not> x \<le> y; crel (merge p qn) h h1 r1; P p qn h h1 r1 (x#xs') ys'; h' = Ref.set q (Node y r1) h1 \<rbrakk>
+  \<not> x \<le> y; effect (merge p qn) h h1 r1; P p qn h h1 r1 (x#xs') ys'; h' = Ref.set q (Node y r1) h1 \<rbrakk>
   \<Longrightarrow> P p q h h' q (x#xs') (y#ys')"
 shows "P p q h h' r xs ys"
 using assms(3)
@@ -802,29 +802,29 @@
   case (1 ys p q)
   from 1(3-4) have "h = h' \<and> r = q"
     unfolding merge_simps[of p q]
-    by (auto elim!: crel_lookupE crel_bindE crel_returnE)
+    by (auto elim!: effect_lookupE effect_bindE effect_returnE)
   with assms(4)[OF 1(1) 1(2) 1(3)] show ?case by simp
 next
   case (2 x xs' p q pn)
   from 2(3-5) have "h = h' \<and> r = p"
     unfolding merge_simps[of p q]
-    by (auto elim!: crel_lookupE crel_bindE crel_returnE)
+    by (auto elim!: effect_lookupE effect_bindE effect_returnE)
   with assms(5)[OF 2(1-4)] show ?case by simp
 next
   case (3 x xs' y ys' p q pn qn)
   from 3(3-5) 3(7) obtain h1 r1 where
-    1: "crel (merge pn q) h h1 r1" 
+    1: "effect (merge pn q) h h1 r1" 
     and 2: "h' = Ref.set p (Node x r1) h1 \<and> r = p"
     unfolding merge_simps[of p q]
-    by (auto elim!: crel_lookupE crel_bindE crel_returnE crel_ifE crel_updateE)
+    by (auto elim!: effect_lookupE effect_bindE effect_returnE effect_ifE effect_updateE)
   from 3(6)[OF 1] assms(6) [OF 3(1-5)] 1 2 show ?case by simp
 next
   case (4 x xs' y ys' p q pn qn)
   from 4(3-5) 4(7) obtain h1 r1 where
-    1: "crel (merge p qn) h h1 r1" 
+    1: "effect (merge p qn) h h1 r1" 
     and 2: "h' = Ref.set q (Node y r1) h1 \<and> r = q"
     unfolding merge_simps[of p q]
-    by (auto elim!: crel_lookupE crel_bindE crel_returnE crel_ifE crel_updateE)
+    by (auto elim!: effect_lookupE effect_bindE effect_returnE effect_ifE effect_updateE)
   from 4(6)[OF 1] assms(7) [OF 4(1-5)] 1 2 show ?case by simp
 qed
 
@@ -837,7 +837,7 @@
 lemma merge_unchanged:
   assumes "refs_of' h p xs"
   assumes "refs_of' h q ys"  
-  assumes "crel (merge p q) h h' r'"
+  assumes "effect (merge p q) h h' r'"
   assumes "set xs \<inter> set ys = {}"
   assumes "r \<notin> set xs \<union> set ys"
   shows "Ref.get h r = Ref.get h' r"
@@ -882,7 +882,7 @@
 lemma refs_of'_merge:
   assumes "refs_of' h p xs"
   assumes "refs_of' h q ys"
-  assumes "crel (merge p q) h h' r"
+  assumes "effect (merge p q) h h' r"
   assumes "set xs \<inter> set ys = {}"
   assumes "refs_of' h' r rs"
   shows "set rs \<subseteq> set xs \<union> set ys"
@@ -930,7 +930,7 @@
 lemma
   assumes "list_of' h p xs"
   assumes "list_of' h q ys"
-  assumes "crel (merge p q) h h' r"
+  assumes "effect (merge p q) h h' r"
   assumes "\<forall>qrs prs. refs_of' h q qrs \<and> refs_of' h p prs \<longrightarrow> set prs \<inter> set qrs = {}"
   shows "list_of' h' r (Lmerge xs ys)"
 using assms(4)
diff -r c059d550afec -r 23904fa13e03 src/HOL/Imperative_HOL/ex/SatChecker.thy
--- a/src/HOL/Imperative_HOL/ex/SatChecker.thy	Tue Nov 23 23:10:13 2010 +0100
+++ b/src/HOL/Imperative_HOL/ex/SatChecker.thy	Tue Nov 23 23:11:06 2010 +0100
@@ -212,33 +212,33 @@
 subsection {* Proofs about these functions *}
 
 lemma res_mem:
-assumes "crel (res_mem l xs) h h' r"
+assumes "effect (res_mem l xs) h h' r"
   shows "l \<in> set xs \<and> r = remove1 l xs"
 using assms
 proof (induct xs arbitrary: r)
   case Nil
-  thus ?case unfolding res_mem.simps by (auto elim: crel_raiseE)
+  thus ?case unfolding res_mem.simps by (auto elim: effect_raiseE)
 next
   case (Cons x xs')
   thus ?case
     unfolding res_mem.simps
-    by (elim crel_raiseE crel_returnE crel_ifE crel_bindE) auto
+    by (elim effect_raiseE effect_returnE effect_ifE effect_bindE) auto
 qed
 
 lemma resolve1_Inv:
-assumes "crel (resolve1 l xs ys) h h' r"
+assumes "effect (resolve1 l xs ys) h h' r"
   shows "l \<in> set xs \<and> r = merge (remove1 l xs) ys"
 using assms
 proof (induct xs ys arbitrary: r rule: resolve1.induct)
   case (1 l x xs y ys r)
   thus ?case
     unfolding resolve1.simps
-    by (elim crel_bindE crel_ifE crel_returnE) auto
+    by (elim effect_bindE effect_ifE effect_returnE) auto
 next
   case (2 l ys r)
   thus ?case
     unfolding resolve1.simps
-    by (elim crel_raiseE) auto
+    by (elim effect_raiseE) auto
 next
   case (3 l v va r)
   thus ?case
@@ -247,19 +247,19 @@
 qed
 
 lemma resolve2_Inv: 
-  assumes "crel (resolve2 l xs ys) h h' r"
+  assumes "effect (resolve2 l xs ys) h h' r"
   shows "l \<in> set ys \<and> r = merge xs (remove1 l ys)"
 using assms
 proof (induct xs ys arbitrary: r rule: resolve2.induct)
   case (1 l x xs y ys r)
   thus ?case
     unfolding resolve2.simps
-    by (elim crel_bindE crel_ifE crel_returnE) auto
+    by (elim effect_bindE effect_ifE effect_returnE) auto
 next
   case (2 l ys r)
   thus ?case
     unfolding resolve2.simps
-    by (elim crel_raiseE) auto
+    by (elim effect_raiseE) auto
 next
   case (3 l v va r)
   thus ?case
@@ -268,7 +268,7 @@
 qed
 
 lemma res_thm'_Inv:
-assumes "crel (res_thm' l xs ys) h h' r"
+assumes "effect (res_thm' l xs ys) h h' r"
 shows "\<exists>l'. (l' \<in> set xs \<and> compl l' \<in> set ys \<and> (l' = compl l \<or> l' = l)) \<and> r = merge (remove1 l' xs) (remove1 (compl l') ys)"
 using assms
 proof (induct xs ys arbitrary: r rule: res_thm'.induct)
@@ -276,14 +276,14 @@
 (* There are five cases for res_thm: We will consider them one after another: *) 
   {
     assume cond: "x = l \<or> x = compl l"
-    assume resolve2: "crel (resolve2 (compl x) xs (y # ys)) h h' r"   
+    assume resolve2: "effect (resolve2 (compl x) xs (y # ys)) h h' r"   
     from resolve2_Inv [OF resolve2] cond have ?case
       apply -
       by (rule exI[of _ "x"]) fastsimp
   } moreover
   {
     assume cond: "\<not> (x = l \<or> x = compl l)" "y = l \<or> y = compl l" 
-    assume resolve1: "crel (resolve1 (compl y) (x # xs) ys) h h' r"
+    assume resolve1: "effect (resolve1 (compl y) (x # xs) ys) h h' r"
     from resolve1_Inv [OF resolve1] cond have ?case
       apply -
       by (rule exI[of _ "compl y"]) fastsimp
@@ -291,28 +291,28 @@
   {
     fix r'
     assume cond: "\<not> (x = l \<or> x = compl l)" "\<not> (y = l \<or> y = compl l)" "x < y"
-    assume res_thm: "crel (res_thm' l xs (y # ys)) h h' r'"
+    assume res_thm: "effect (res_thm' l xs (y # ys)) h h' r'"
     assume return: "r = x # r'"
     from "1.hyps"(1) [OF cond res_thm] cond return have ?case by auto
   } moreover
   {
     fix r'
     assume cond: "\<not> (x = l \<or> x = compl l)" "\<not> (y = l \<or> y = compl l)" "\<not> x < y" "y < x"
-    assume res_thm: "crel (res_thm' l (x # xs) ys) h h' r'"
+    assume res_thm: "effect (res_thm' l (x # xs) ys) h h' r'"
     assume return: "r = y # r'"
     from "1.hyps"(2) [OF cond res_thm] cond return have ?case by auto
   } moreover
   {
     fix r'
     assume cond: "\<not> (x = l \<or> x = compl l)" "\<not> (y = l \<or> y = compl l)" "\<not> x < y" "\<not> y < x"
-    assume res_thm: "crel (res_thm' l xs ys) h h' r'"
+    assume res_thm: "effect (res_thm' l xs ys) h h' r'"
     assume return: "r = x # r'"
     from "1.hyps"(3) [OF cond res_thm] cond return have ?case by auto
   } moreover
   note "1.prems"
   ultimately show ?case
     unfolding res_thm'.simps
-    apply (elim crel_bindE crel_ifE crel_returnE)
+    apply (elim effect_bindE effect_ifE effect_returnE)
     apply simp
     apply simp
     apply simp
@@ -323,72 +323,72 @@
   case (2 l ys r)
   thus ?case
     unfolding res_thm'.simps
-    by (elim crel_raiseE) auto
+    by (elim effect_raiseE) auto
 next
   case (3 l v va r)
   thus ?case
     unfolding res_thm'.simps
-    by (elim crel_raiseE) auto
+    by (elim effect_raiseE) auto
 qed
 
 lemma res_mem_no_heap:
-assumes "crel (res_mem l xs) h h' r"
+assumes "effect (res_mem l xs) h h' r"
   shows "h = h'"
 using assms
 apply (induct xs arbitrary: r)
 unfolding res_mem.simps
-apply (elim crel_raiseE)
+apply (elim effect_raiseE)
 apply auto
-apply (elim crel_ifE crel_bindE crel_raiseE crel_returnE)
+apply (elim effect_ifE effect_bindE effect_raiseE effect_returnE)
 apply auto
 done
 
 lemma resolve1_no_heap:
-assumes "crel (resolve1 l xs ys) h h' r"
+assumes "effect (resolve1 l xs ys) h h' r"
   shows "h = h'"
 using assms
 apply (induct xs ys arbitrary: r rule: resolve1.induct)
 unfolding resolve1.simps
-apply (elim crel_bindE crel_ifE crel_returnE crel_raiseE)
+apply (elim effect_bindE effect_ifE effect_returnE effect_raiseE)
 apply (auto simp add: res_mem_no_heap)
-by (elim crel_raiseE) auto
+by (elim effect_raiseE) auto
 
 lemma resolve2_no_heap:
-assumes "crel (resolve2 l xs ys) h h' r"
+assumes "effect (resolve2 l xs ys) h h' r"
   shows "h = h'"
 using assms
 apply (induct xs ys arbitrary: r rule: resolve2.induct)
 unfolding resolve2.simps
-apply (elim crel_bindE crel_ifE crel_returnE crel_raiseE)
+apply (elim effect_bindE effect_ifE effect_returnE effect_raiseE)
 apply (auto simp add: res_mem_no_heap)
-by (elim crel_raiseE) auto
+by (elim effect_raiseE) auto
 
 
 lemma res_thm'_no_heap:
-  assumes "crel (res_thm' l xs ys) h h' r"
+  assumes "effect (res_thm' l xs ys) h h' r"
   shows "h = h'"
   using assms
 proof (induct xs ys arbitrary: r rule: res_thm'.induct)
   case (1 l x xs y ys r)
   thus ?thesis
     unfolding res_thm'.simps
-    by (elim crel_bindE crel_ifE crel_returnE)
+    by (elim effect_bindE effect_ifE effect_returnE)
   (auto simp add: resolve1_no_heap resolve2_no_heap)
 next
   case (2 l ys r)
   thus ?case
     unfolding res_thm'.simps
-    by (elim crel_raiseE) auto
+    by (elim effect_raiseE) auto
 next
   case (3 l v va r)
   thus ?case
     unfolding res_thm'.simps
-    by (elim crel_raiseE) auto
+    by (elim effect_raiseE) auto
 qed
 
 
 lemma res_thm'_Inv2:
-  assumes res_thm: "crel (res_thm' l xs ys) h h' rcl"
+  assumes res_thm: "effect (res_thm' l xs ys) h h' rcl"
   assumes l_not_null: "l \<noteq> 0"
   assumes ys: "correctClause r ys \<and> sorted ys \<and> distinct ys"
   assumes xs: "correctClause r xs \<and> sorted xs \<and> distinct xs"
@@ -459,20 +459,20 @@
                 else raise(''No empty clause''))
   }"
 
-lemma crel_option_case:
-  assumes "crel (case x of None \<Rightarrow> n | Some y \<Rightarrow> s y) h h' r"
-  obtains "x = None" "crel n h h' r"
-         | y where "x = Some y" "crel (s y) h h' r" 
-  using assms unfolding crel_def by (auto split: option.splits)
+lemma effect_option_case:
+  assumes "effect (case x of None \<Rightarrow> n | Some y \<Rightarrow> s y) h h' r"
+  obtains "x = None" "effect n h h' r"
+         | y where "x = Some y" "effect (s y) h h' r" 
+  using assms unfolding effect_def by (auto split: option.splits)
 
 lemma res_thm2_Inv:
-  assumes res_thm: "crel (res_thm2 a (l, j) cli) h h' rs"
+  assumes res_thm: "effect (res_thm2 a (l, j) cli) h h' rs"
   assumes correct_a: "correctArray r a h"
   assumes correct_cli: "correctClause r cli \<and> sorted cli \<and> distinct cli"
   shows "h = h' \<and> correctClause r rs \<and> sorted rs \<and> distinct rs"
 proof -
   from res_thm have l_not_zero: "l \<noteq> 0" 
-    by (auto elim: crel_raiseE)
+    by (auto elim: effect_raiseE)
   {
     fix clj
     let ?rs = "merge (remove l cli) (remove (compl l) clj)"
@@ -494,17 +494,17 @@
     assume "Some clj = Array.get h a ! j" "j < Array.length h a"
     with correct_a have clj: "correctClause r clj \<and> sorted clj \<and> distinct clj"
       unfolding correctArray_def by (auto intro: array_ranI)
-    assume "crel (res_thm' l cli clj) h h' rs"
+    assume "effect (res_thm' l cli clj) h h' rs"
     from res_thm'_no_heap[OF this] res_thm'_Inv2[OF this l_not_zero clj correct_cli]
     have "h = h' \<and> correctClause r rs \<and> sorted rs \<and> distinct rs" by simp
   }
   with assms show ?thesis
     unfolding res_thm2.simps get_clause_def
-    by (elim crel_bindE crel_ifE crel_nthE crel_raiseE crel_returnE crel_option_case) auto
+    by (elim effect_bindE effect_ifE effect_nthE effect_raiseE effect_returnE effect_option_case) auto
 qed
 
 lemma foldM_Inv2:
-  assumes "crel (foldM (res_thm2 a) rs cli) h h' rcl"
+  assumes "effect (foldM (res_thm2 a) rs cli) h h' rcl"
   assumes correct_a: "correctArray r a h"
   assumes correct_cli: "correctClause r cli \<and> sorted cli \<and> distinct cli"
   shows "h = h' \<and> correctClause r rcl \<and> sorted rcl \<and> distinct rcl"
@@ -512,39 +512,39 @@
 proof (induct rs arbitrary: h h' cli)
   case Nil thus ?case
     unfolding foldM.simps
-    by (elim crel_returnE) auto
+    by (elim effect_returnE) auto
 next
   case (Cons x xs)
   {
     fix h1 ret
     obtain l j where x_is: "x = (l, j)" by fastsimp
-    assume res_thm2: "crel (res_thm2 a x cli) h h1 ret"
-    with x_is have res_thm2': "crel (res_thm2 a (l, j) cli) h h1 ret" by simp
+    assume res_thm2: "effect (res_thm2 a x cli) h h1 ret"
+    with x_is have res_thm2': "effect (res_thm2 a (l, j) cli) h h1 ret" by simp
     note step = res_thm2_Inv [OF res_thm2' Cons.prems(2) Cons.prems(3)]
     from step have ret: "correctClause r ret \<and> sorted ret \<and> distinct ret" by simp
     from step Cons.prems(2) have correct_a: "correctArray r a h1"  by simp
-    assume foldM: "crel (foldM (res_thm2 a) xs ret) h1 h' rcl"
+    assume foldM: "effect (foldM (res_thm2 a) xs ret) h1 h' rcl"
     from step Cons.hyps [OF foldM correct_a ret] have
     "h = h' \<and> correctClause r rcl \<and> sorted rcl \<and> distinct rcl" by auto
   }
   with Cons show ?case
     unfolding foldM.simps
-    by (elim crel_bindE) auto
+    by (elim effect_bindE) auto
 qed
 
 
 lemma step_correct2:
-  assumes crel: "crel (doProofStep2 a step rcs) h h' res"
+  assumes effect: "effect (doProofStep2 a step rcs) h h' res"
   assumes correctArray: "correctArray rcs a h"
   shows "correctArray res a h'"
 proof (cases "(a,step,rcs)" rule: doProofStep2.cases)
   case (1 a saveTo i rs rcs)
-  with crel correctArray
+  with effect correctArray
   show ?thesis
     apply auto
-    apply (auto simp: get_clause_def elim!: crel_bindE crel_nthE)
-    apply (auto elim!: crel_bindE crel_nthE crel_option_case crel_raiseE
-      crel_returnE crel_updE)
+    apply (auto simp: get_clause_def elim!: effect_bindE effect_nthE)
+    apply (auto elim!: effect_bindE effect_nthE effect_option_case effect_raiseE
+      effect_returnE effect_updE)
     apply (frule foldM_Inv2)
     apply assumption
     apply (simp add: correctArray_def)
@@ -553,42 +553,42 @@
     by (auto intro: correctArray_update)
 next
   case (2 a cid rcs)
-  with crel correctArray
+  with effect correctArray
   show ?thesis
-    by (auto simp: correctArray_def elim!: crel_bindE crel_updE crel_returnE
+    by (auto simp: correctArray_def elim!: effect_bindE effect_updE effect_returnE
      dest: array_ran_upd_array_None)
 next
   case (3 a cid c rcs)
-  with crel correctArray
+  with effect correctArray
   show ?thesis
-    apply (auto elim!: crel_bindE crel_updE crel_returnE)
+    apply (auto elim!: effect_bindE effect_updE effect_returnE)
     apply (auto simp: correctArray_def dest!: array_ran_upd_array_Some)
     apply (auto intro: correctClause_mono)
     by (auto simp: correctClause_def)
 next
   case 4
-  with crel correctArray
-  show ?thesis by (auto elim: crel_raiseE)
+  with effect correctArray
+  show ?thesis by (auto elim: effect_raiseE)
 next
   case 5
-  with crel correctArray
-  show ?thesis by (auto elim: crel_raiseE)
+  with effect correctArray
+  show ?thesis by (auto elim: effect_raiseE)
 qed
   
 
 theorem fold_steps_correct:
-  assumes "crel (foldM (doProofStep2 a) steps rcs) h h' res"
+  assumes "effect (foldM (doProofStep2 a) steps rcs) h h' res"
   assumes "correctArray rcs a h"
   shows "correctArray res a h'"
 using assms
 by (induct steps arbitrary: rcs h h' res)
- (auto elim!: crel_bindE crel_returnE dest:step_correct2)
+ (auto elim!: effect_bindE effect_returnE dest:step_correct2)
 
 theorem checker_soundness:
-  assumes "crel (checker n p i) h h' cs"
+  assumes "effect (checker n p i) h h' cs"
   shows "inconsistent cs"
 using assms unfolding checker_def
-apply (elim crel_bindE crel_nthE crel_ifE crel_returnE crel_raiseE crel_newE)
+apply (elim effect_bindE effect_nthE effect_ifE effect_returnE effect_raiseE effect_newE)
 prefer 2 apply simp
 apply auto
 apply (drule fold_steps_correct)
diff -r c059d550afec -r 23904fa13e03 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue Nov 23 23:10:13 2010 +0100
+++ b/src/HOL/IsaMakefile	Tue Nov 23 23:11:06 2010 +0100
@@ -422,7 +422,7 @@
   Library/Efficient_Nat.thy Library/Eval_Witness.thy 			\
   Library/Executable_Set.thy Library/Float.thy				\
   Library/Formal_Power_Series.thy Library/Fraction_Field.thy		\
-  Library/FrechetDeriv.thy Library/Fset.thy Library/FuncSet.thy		\
+  Library/FrechetDeriv.thy Library/Cset.thy Library/FuncSet.thy		\
   Library/Function_Algebras.thy						\
   Library/Fundamental_Theorem_Algebra.thy Library/Glbs.thy		\
   Library/Indicator_Function.thy Library/Infinite_Set.thy		\
diff -r c059d550afec -r 23904fa13e03 src/HOL/Library/Cset.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Cset.thy	Tue Nov 23 23:11:06 2010 +0100
@@ -0,0 +1,357 @@
+
+(* Author: Florian Haftmann, TU Muenchen *)
+
+header {* A dedicated set type which is executable on its finite part *}
+
+theory Cset
+imports More_Set More_List
+begin
+
+subsection {* Lifting *}
+
+typedef (open) 'a set = "UNIV :: 'a set set"
+  morphisms member Set by rule+
+hide_type (open) set
+
+lemma member_Set [simp]:
+  "member (Set A) = A"
+  by (rule Set_inverse) rule
+
+lemma Set_member [simp]:
+  "Set (member A) = A"
+  by (fact member_inverse)
+
+lemma Set_inject [simp]:
+  "Set A = Set B \<longleftrightarrow> A = B"
+  by (simp add: Set_inject)
+
+lemma set_eq_iff:
+  "A = B \<longleftrightarrow> member A = member B"
+  by (simp add: member_inject)
+hide_fact (open) set_eq_iff
+
+lemma set_eqI:
+  "member A = member B \<Longrightarrow> A = B"
+  by (simp add: Cset.set_eq_iff)
+hide_fact (open) set_eqI
+
+declare mem_def [simp]
+
+definition set :: "'a list \<Rightarrow> 'a Cset.set" where
+  "set xs = Set (List.set xs)"
+hide_const (open) set
+
+lemma member_set [simp]:
+  "member (Cset.set xs) = set xs"
+  by (simp add: set_def)
+hide_fact (open) member_set
+
+definition coset :: "'a list \<Rightarrow> 'a Cset.set" where
+  "coset xs = Set (- set xs)"
+hide_const (open) coset
+
+lemma member_coset [simp]:
+  "member (Cset.coset xs) = - set xs"
+  by (simp add: coset_def)
+hide_fact (open) member_coset
+
+code_datatype Cset.set Cset.coset
+
+lemma member_code [code]:
+  "member (Cset.set xs) = List.member xs"
+  "member (Cset.coset xs) = Not \<circ> List.member xs"
+  by (simp_all add: fun_eq_iff member_def fun_Compl_def bool_Compl_def)
+
+lemma member_image_UNIV [simp]:
+  "member ` UNIV = UNIV"
+proof -
+  have "\<And>A \<Colon> 'a set. \<exists>B \<Colon> 'a Cset.set. A = member B"
+  proof
+    fix A :: "'a set"
+    show "A = member (Set A)" by simp
+  qed
+  then show ?thesis by (simp add: image_def)
+qed
+
+definition (in term_syntax)
+  setify :: "'a\<Colon>typerep list \<times> (unit \<Rightarrow> Code_Evaluation.term)
+    \<Rightarrow> 'a Cset.set \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
+  [code_unfold]: "setify xs = Code_Evaluation.valtermify Cset.set {\<cdot>} xs"
+
+notation fcomp (infixl "\<circ>>" 60)
+notation scomp (infixl "\<circ>\<rightarrow>" 60)
+
+instantiation Cset.set :: (random) random
+begin
+
+definition
+  "Quickcheck.random i = Quickcheck.random i \<circ>\<rightarrow> (\<lambda>xs. Pair (setify xs))"
+
+instance ..
+
+end
+
+no_notation fcomp (infixl "\<circ>>" 60)
+no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
+
+
+subsection {* Lattice instantiation *}
+
+instantiation Cset.set :: (type) boolean_algebra
+begin
+
+definition less_eq_set :: "'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> bool" where
+  [simp]: "A \<le> B \<longleftrightarrow> member A \<subseteq> member B"
+
+definition less_set :: "'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> bool" where
+  [simp]: "A < B \<longleftrightarrow> member A \<subset> member B"
+
+definition inf_set :: "'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
+  [simp]: "inf A B = Set (member A \<inter> member B)"
+
+definition sup_set :: "'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
+  [simp]: "sup A B = Set (member A \<union> member B)"
+
+definition bot_set :: "'a Cset.set" where
+  [simp]: "bot = Set {}"
+
+definition top_set :: "'a Cset.set" where
+  [simp]: "top = Set UNIV"
+
+definition uminus_set :: "'a Cset.set \<Rightarrow> 'a Cset.set" where
+  [simp]: "- A = Set (- (member A))"
+
+definition minus_set :: "'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
+  [simp]: "A - B = Set (member A - member B)"
+
+instance proof
+qed (auto intro: Cset.set_eqI)
+
+end
+
+instantiation Cset.set :: (type) complete_lattice
+begin
+
+definition Inf_set :: "'a Cset.set set \<Rightarrow> 'a Cset.set" where
+  [simp]: "Inf_set As = Set (Inf (image member As))"
+
+definition Sup_set :: "'a Cset.set set \<Rightarrow> 'a Cset.set" where
+  [simp]: "Sup_set As = Set (Sup (image member As))"
+
+instance proof
+qed (auto simp add: le_fun_def le_bool_def)
+
+end
+
+
+subsection {* Basic operations *}
+
+definition is_empty :: "'a Cset.set \<Rightarrow> bool" where
+  [simp]: "is_empty A \<longleftrightarrow> More_Set.is_empty (member A)"
+
+lemma is_empty_set [code]:
+  "is_empty (Cset.set xs) \<longleftrightarrow> List.null xs"
+  by (simp add: is_empty_set)
+hide_fact (open) is_empty_set
+
+lemma empty_set [code]:
+  "bot = Cset.set []"
+  by (simp add: set_def)
+hide_fact (open) empty_set
+
+lemma UNIV_set [code]:
+  "top = Cset.coset []"
+  by (simp add: coset_def)
+hide_fact (open) UNIV_set
+
+definition insert :: "'a \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
+  [simp]: "insert x A = Set (Set.insert x (member A))"
+
+lemma insert_set [code]:
+  "insert x (Cset.set xs) = Cset.set (List.insert x xs)"
+  "insert x (Cset.coset xs) = Cset.coset (removeAll x xs)"
+  by (simp_all add: set_def coset_def)
+
+definition remove :: "'a \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
+  [simp]: "remove x A = Set (More_Set.remove x (member A))"
+
+lemma remove_set [code]:
+  "remove x (Cset.set xs) = Cset.set (removeAll x xs)"
+  "remove x (Cset.coset xs) = Cset.coset (List.insert x xs)"
+  by (simp_all add: set_def coset_def remove_set_compl)
+    (simp add: More_Set.remove_def)
+
+definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a Cset.set \<Rightarrow> 'b Cset.set" where
+  [simp]: "map f A = Set (image f (member A))"
+
+lemma map_set [code]:
+  "map f (Cset.set xs) = Cset.set (remdups (List.map f xs))"
+  by (simp add: set_def)
+
+type_mapper map
+  by (simp_all add: image_image)
+
+definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
+  [simp]: "filter P A = Set (More_Set.project P (member A))"
+
+lemma filter_set [code]:
+  "filter P (Cset.set xs) = Cset.set (List.filter P xs)"
+  by (simp add: set_def project_set)
+
+definition forall :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Cset.set \<Rightarrow> bool" where
+  [simp]: "forall P A \<longleftrightarrow> Ball (member A) P"
+
+lemma forall_set [code]:
+  "forall P (Cset.set xs) \<longleftrightarrow> list_all P xs"
+  by (simp add: set_def list_all_iff)
+
+definition exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Cset.set \<Rightarrow> bool" where
+  [simp]: "exists P A \<longleftrightarrow> Bex (member A) P"
+
+lemma exists_set [code]:
+  "exists P (Cset.set xs) \<longleftrightarrow> list_ex P xs"
+  by (simp add: set_def list_ex_iff)
+
+definition card :: "'a Cset.set \<Rightarrow> nat" where
+  [simp]: "card A = Finite_Set.card (member A)"
+
+lemma card_set [code]:
+  "card (Cset.set xs) = length (remdups xs)"
+proof -
+  have "Finite_Set.card (set (remdups xs)) = length (remdups xs)"
+    by (rule distinct_card) simp
+  then show ?thesis by (simp add: set_def)
+qed
+
+lemma compl_set [simp, code]:
+  "- Cset.set xs = Cset.coset xs"
+  by (simp add: set_def coset_def)
+
+lemma compl_coset [simp, code]:
+  "- Cset.coset xs = Cset.set xs"
+  by (simp add: set_def coset_def)
+
+
+subsection {* Derived operations *}
+
+lemma subset_eq_forall [code]:
+  "A \<le> B \<longleftrightarrow> forall (member B) A"
+  by (simp add: subset_eq)
+
+lemma subset_subset_eq [code]:
+  "A < B \<longleftrightarrow> A \<le> B \<and> \<not> B \<le> (A :: 'a Cset.set)"
+  by (fact less_le_not_le)
+
+instantiation Cset.set :: (type) equal
+begin
+
+definition [code]:
+  "HOL.equal A B \<longleftrightarrow> A \<le> B \<and> B \<le> (A :: 'a Cset.set)"
+
+instance proof
+qed (simp add: equal_set_def set_eq [symmetric] Cset.set_eq_iff)
+
+end
+
+lemma [code nbe]:
+  "HOL.equal (A :: 'a Cset.set) A \<longleftrightarrow> True"
+  by (fact equal_refl)
+
+
+subsection {* Functorial operations *}
+
+lemma inter_project [code]:
+  "inf A (Cset.set xs) = Cset.set (List.filter (member A) xs)"
+  "inf A (Cset.coset xs) = foldr remove xs A"
+proof -
+  show "inf A (Cset.set xs) = Cset.set (List.filter (member A) xs)"
+    by (simp add: inter project_def set_def)
+  have *: "\<And>x::'a. remove = (\<lambda>x. Set \<circ> More_Set.remove x \<circ> member)"
+    by (simp add: fun_eq_iff)
+  have "member \<circ> fold (\<lambda>x. Set \<circ> More_Set.remove x \<circ> member) xs =
+    fold More_Set.remove xs \<circ> member"
+    by (rule fold_commute) (simp add: fun_eq_iff)
+  then have "fold More_Set.remove xs (member A) = 
+    member (fold (\<lambda>x. Set \<circ> More_Set.remove x \<circ> member) xs A)"
+    by (simp add: fun_eq_iff)
+  then have "inf A (Cset.coset xs) = fold remove xs A"
+    by (simp add: Diff_eq [symmetric] minus_set *)
+  moreover have "\<And>x y :: 'a. Cset.remove y \<circ> Cset.remove x = Cset.remove x \<circ> Cset.remove y"
+    by (auto simp add: More_Set.remove_def * intro: ext)
+  ultimately show "inf A (Cset.coset xs) = foldr remove xs A"
+    by (simp add: foldr_fold)
+qed
+
+lemma subtract_remove [code]:
+  "A - Cset.set xs = foldr remove xs A"
+  "A - Cset.coset xs = Cset.set (List.filter (member A) xs)"
+  by (simp_all only: diff_eq compl_set compl_coset inter_project)
+
+lemma union_insert [code]:
+  "sup (Cset.set xs) A = foldr insert xs A"
+  "sup (Cset.coset xs) A = Cset.coset (List.filter (Not \<circ> member A) xs)"
+proof -
+  have *: "\<And>x::'a. insert = (\<lambda>x. Set \<circ> Set.insert x \<circ> member)"
+    by (simp add: fun_eq_iff)
+  have "member \<circ> fold (\<lambda>x. Set \<circ> Set.insert x \<circ> member) xs =
+    fold Set.insert xs \<circ> member"
+    by (rule fold_commute) (simp add: fun_eq_iff)
+  then have "fold Set.insert xs (member A) =
+    member (fold (\<lambda>x. Set \<circ> Set.insert x \<circ> member) xs A)"
+    by (simp add: fun_eq_iff)
+  then have "sup (Cset.set xs) A = fold insert xs A"
+    by (simp add: union_set *)
+  moreover have "\<And>x y :: 'a. Cset.insert y \<circ> Cset.insert x = Cset.insert x \<circ> Cset.insert y"
+    by (auto simp add: * intro: ext)
+  ultimately show "sup (Cset.set xs) A = foldr insert xs A"
+    by (simp add: foldr_fold)
+  show "sup (Cset.coset xs) A = Cset.coset (List.filter (Not \<circ> member A) xs)"
+    by (auto simp add: coset_def)
+qed
+
+context complete_lattice
+begin
+
+definition Infimum :: "'a Cset.set \<Rightarrow> 'a" where
+  [simp]: "Infimum A = Inf (member A)"
+
+lemma Infimum_inf [code]:
+  "Infimum (Cset.set As) = foldr inf As top"
+  "Infimum (Cset.coset []) = bot"
+  by (simp_all add: Inf_set_foldr Inf_UNIV)
+
+definition Supremum :: "'a Cset.set \<Rightarrow> 'a" where
+  [simp]: "Supremum A = Sup (member A)"
+
+lemma Supremum_sup [code]:
+  "Supremum (Cset.set As) = foldr sup As bot"
+  "Supremum (Cset.coset []) = top"
+  by (simp_all add: Sup_set_foldr Sup_UNIV)
+
+end
+
+
+subsection {* Simplified simprules *}
+
+lemma is_empty_simp [simp]:
+  "is_empty A \<longleftrightarrow> member A = {}"
+  by (simp add: More_Set.is_empty_def)
+declare is_empty_def [simp del]
+
+lemma remove_simp [simp]:
+  "remove x A = Set (member A - {x})"
+  by (simp add: More_Set.remove_def)
+declare remove_def [simp del]
+
+lemma filter_simp [simp]:
+  "filter P A = Set {x \<in> member A. P x}"
+  by (simp add: More_Set.project_def)
+declare filter_def [simp del]
+
+declare mem_def [simp del]
+
+
+hide_const (open) setify is_empty insert remove map filter forall exists card
+  Inter Union
+
+end
diff -r c059d550afec -r 23904fa13e03 src/HOL/Library/Dlist.thy
--- a/src/HOL/Library/Dlist.thy	Tue Nov 23 23:10:13 2010 +0100
+++ b/src/HOL/Library/Dlist.thy	Tue Nov 23 23:11:06 2010 +0100
@@ -3,7 +3,7 @@
 header {* Lists with elements distinct as canonical example for datatype invariants *}
 
 theory Dlist
-imports Main Fset
+imports Main Cset
 begin
 
 section {* The type of distinct lists *}
@@ -181,27 +181,27 @@
 
 section {* Implementation of sets by distinct lists -- canonical! *}
 
-definition Set :: "'a dlist \<Rightarrow> 'a fset" where
-  "Set dxs = Fset.Set (list_of_dlist dxs)"
+definition Set :: "'a dlist \<Rightarrow> 'a Cset.set" where
+  "Set dxs = Cset.set (list_of_dlist dxs)"
 
-definition Coset :: "'a dlist \<Rightarrow> 'a fset" where
-  "Coset dxs = Fset.Coset (list_of_dlist dxs)"
+definition Coset :: "'a dlist \<Rightarrow> 'a Cset.set" where
+  "Coset dxs = Cset.coset (list_of_dlist dxs)"
 
 code_datatype Set Coset
 
 declare member_code [code del]
-declare is_empty_Set [code del]
-declare empty_Set [code del]
-declare UNIV_Set [code del]
-declare insert_Set [code del]
-declare remove_Set [code del]
-declare compl_Set [code del]
-declare compl_Coset [code del]
-declare map_Set [code del]
-declare filter_Set [code del]
-declare forall_Set [code del]
-declare exists_Set [code del]
-declare card_Set [code del]
+declare Cset.is_empty_set [code del]
+declare Cset.empty_set [code del]
+declare Cset.UNIV_set [code del]
+declare insert_set [code del]
+declare remove_set [code del]
+declare compl_set [code del]
+declare compl_coset [code del]
+declare map_set [code del]
+declare filter_set [code del]
+declare forall_set [code del]
+declare exists_set [code del]
+declare card_set [code del]
 declare inter_project [code del]
 declare subtract_remove [code del]
 declare union_insert [code del]
@@ -209,31 +209,31 @@
 declare Supremum_sup [code del]
 
 lemma Set_Dlist [simp]:
-  "Set (Dlist xs) = Fset (set xs)"
-  by (rule fset_eqI) (simp add: Set_def)
+  "Set (Dlist xs) = Cset.Set (set xs)"
+  by (rule Cset.set_eqI) (simp add: Set_def)
 
 lemma Coset_Dlist [simp]:
-  "Coset (Dlist xs) = Fset (- set xs)"
-  by (rule fset_eqI) (simp add: Coset_def)
+  "Coset (Dlist xs) = Cset.Set (- set xs)"
+  by (rule Cset.set_eqI) (simp add: Coset_def)
 
 lemma member_Set [simp]:
-  "Fset.member (Set dxs) = List.member (list_of_dlist dxs)"
+  "Cset.member (Set dxs) = List.member (list_of_dlist dxs)"
   by (simp add: Set_def member_set)
 
 lemma member_Coset [simp]:
-  "Fset.member (Coset dxs) = Not \<circ> List.member (list_of_dlist dxs)"
+  "Cset.member (Coset dxs) = Not \<circ> List.member (list_of_dlist dxs)"
   by (simp add: Coset_def member_set not_set_compl)
 
 lemma Set_dlist_of_list [code]:
-  "Fset.Set xs = Set (dlist_of_list xs)"
-  by (rule fset_eqI) simp
+  "Cset.set xs = Set (dlist_of_list xs)"
+  by (rule Cset.set_eqI) simp
 
 lemma Coset_dlist_of_list [code]:
-  "Fset.Coset xs = Coset (dlist_of_list xs)"
-  by (rule fset_eqI) simp
+  "Cset.coset xs = Coset (dlist_of_list xs)"
+  by (rule Cset.set_eqI) simp
 
 lemma is_empty_Set [code]:
-  "Fset.is_empty (Set dxs) \<longleftrightarrow> null dxs"
+  "Cset.is_empty (Set dxs) \<longleftrightarrow> null dxs"
   by (simp add: null_def List.null_def member_set)
 
 lemma bot_code [code]:
@@ -245,58 +245,58 @@
   by (simp add: empty_def)
 
 lemma insert_code [code]:
-  "Fset.insert x (Set dxs) = Set (insert x dxs)"
-  "Fset.insert x (Coset dxs) = Coset (remove x dxs)"
+  "Cset.insert x (Set dxs) = Set (insert x dxs)"
+  "Cset.insert x (Coset dxs) = Coset (remove x dxs)"
   by (simp_all add: insert_def remove_def member_set not_set_compl)
 
 lemma remove_code [code]:
-  "Fset.remove x (Set dxs) = Set (remove x dxs)"
-  "Fset.remove x (Coset dxs) = Coset (insert x dxs)"
+  "Cset.remove x (Set dxs) = Set (remove x dxs)"
+  "Cset.remove x (Coset dxs) = Coset (insert x dxs)"
   by (auto simp add: insert_def remove_def member_set not_set_compl)
 
 lemma member_code [code]:
-  "Fset.member (Set dxs) = member dxs"
-  "Fset.member (Coset dxs) = Not \<circ> member dxs"
+  "Cset.member (Set dxs) = member dxs"
+  "Cset.member (Coset dxs) = Not \<circ> member dxs"
   by (simp_all add: member_def)
 
 lemma compl_code [code]:
   "- Set dxs = Coset dxs"
   "- Coset dxs = Set dxs"
-  by (rule fset_eqI, simp add: member_set not_set_compl)+
+  by (rule Cset.set_eqI, simp add: member_set not_set_compl)+
 
 lemma map_code [code]:
-  "Fset.map f (Set dxs) = Set (map f dxs)"
-  by (rule fset_eqI) (simp add: member_set)
+  "Cset.map f (Set dxs) = Set (map f dxs)"
+  by (rule Cset.set_eqI) (simp add: member_set)
   
 lemma filter_code [code]:
-  "Fset.filter f (Set dxs) = Set (filter f dxs)"
-  by (rule fset_eqI) (simp add: member_set)
+  "Cset.filter f (Set dxs) = Set (filter f dxs)"
+  by (rule Cset.set_eqI) (simp add: member_set)
 
 lemma forall_Set [code]:
-  "Fset.forall P (Set xs) \<longleftrightarrow> list_all P (list_of_dlist xs)"
+  "Cset.forall P (Set xs) \<longleftrightarrow> list_all P (list_of_dlist xs)"
   by (simp add: member_set list_all_iff)
 
 lemma exists_Set [code]:
-  "Fset.exists P (Set xs) \<longleftrightarrow> list_ex P (list_of_dlist xs)"
+  "Cset.exists P (Set xs) \<longleftrightarrow> list_ex P (list_of_dlist xs)"
   by (simp add: member_set list_ex_iff)
 
 lemma card_code [code]:
-  "Fset.card (Set dxs) = length dxs"
+  "Cset.card (Set dxs) = length dxs"
   by (simp add: length_def member_set distinct_card)
 
 lemma inter_code [code]:
-  "inf A (Set xs) = Set (filter (Fset.member A) xs)"
-  "inf A (Coset xs) = foldr Fset.remove xs A"
+  "inf A (Set xs) = Set (filter (Cset.member A) xs)"
+  "inf A (Coset xs) = foldr Cset.remove xs A"
   by (simp_all only: Set_def Coset_def foldr_def inter_project list_of_dlist_filter)
 
 lemma subtract_code [code]:
-  "A - Set xs = foldr Fset.remove xs A"
-  "A - Coset xs = Set (filter (Fset.member A) xs)"
+  "A - Set xs = foldr Cset.remove xs A"
+  "A - Coset xs = Set (filter (Cset.member A) xs)"
   by (simp_all only: Set_def Coset_def foldr_def subtract_remove list_of_dlist_filter)
 
 lemma union_code [code]:
-  "sup (Set xs) A = foldr Fset.insert xs A"
-  "sup (Coset xs) A = Coset (filter (Not \<circ> Fset.member A) xs)"
+  "sup (Set xs) A = foldr Cset.insert xs A"
+  "sup (Coset xs) A = Coset (filter (Not \<circ> Cset.member A) xs)"
   by (simp_all only: Set_def Coset_def foldr_def union_insert list_of_dlist_filter)
 
 context complete_lattice
diff -r c059d550afec -r 23904fa13e03 src/HOL/Library/Executable_Set.thy
--- a/src/HOL/Library/Executable_Set.thy	Tue Nov 23 23:10:13 2010 +0100
+++ b/src/HOL/Library/Executable_Set.thy	Tue Nov 23 23:11:06 2010 +0100
@@ -12,7 +12,7 @@
 text {*
   This is just an ad-hoc hack which will rarely give you what you want.
   For the moment, whenever you need executable sets, consider using
-  type @{text fset} from theory @{text Fset}.
+  type @{text fset} from theory @{text Cset}.
 *}
 
 declare mem_def [code del]
diff -r c059d550afec -r 23904fa13e03 src/HOL/Library/Fset.thy
--- a/src/HOL/Library/Fset.thy	Tue Nov 23 23:10:13 2010 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,347 +0,0 @@
-
-(* Author: Florian Haftmann, TU Muenchen *)
-
-header {* A set type which is executable on its finite part *}
-
-theory Fset
-imports More_Set More_List
-begin
-
-subsection {* Lifting *}
-
-typedef (open) 'a fset = "UNIV :: 'a set set"
-  morphisms member Fset by rule+
-
-lemma member_Fset [simp]:
-  "member (Fset A) = A"
-  by (rule Fset_inverse) rule
-
-lemma Fset_member [simp]:
-  "Fset (member A) = A"
-  by (fact member_inverse)
-
-lemma Fset_inject [simp]:
-  "Fset A = Fset B \<longleftrightarrow> A = B"
-  by (simp add: Fset_inject)
-
-lemma fset_eq_iff:
-  "A = B \<longleftrightarrow> member A = member B"
-  by (simp add: member_inject)
-
-lemma fset_eqI:
-  "member A = member B \<Longrightarrow> A = B"
-  by (simp add: fset_eq_iff)
-
-declare mem_def [simp]
-
-definition Set :: "'a list \<Rightarrow> 'a fset" where
-  "Set xs = Fset (set xs)"
-
-lemma member_Set [simp]:
-  "member (Set xs) = set xs"
-  by (simp add: Set_def)
-
-definition Coset :: "'a list \<Rightarrow> 'a fset" where
-  "Coset xs = Fset (- set xs)"
-
-lemma member_Coset [simp]:
-  "member (Coset xs) = - set xs"
-  by (simp add: Coset_def)
-
-code_datatype Set Coset
-
-lemma member_code [code]:
-  "member (Set xs) = List.member xs"
-  "member (Coset xs) = Not \<circ> List.member xs"
-  by (simp_all add: fun_eq_iff member_def fun_Compl_def bool_Compl_def)
-
-lemma member_image_UNIV [simp]:
-  "member ` UNIV = UNIV"
-proof -
-  have "\<And>A \<Colon> 'a set. \<exists>B \<Colon> 'a fset. A = member B"
-  proof
-    fix A :: "'a set"
-    show "A = member (Fset A)" by simp
-  qed
-  then show ?thesis by (simp add: image_def)
-qed
-
-definition (in term_syntax)
-  setify :: "'a\<Colon>typerep list \<times> (unit \<Rightarrow> Code_Evaluation.term)
-    \<Rightarrow> 'a fset \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
-  [code_unfold]: "setify xs = Code_Evaluation.valtermify Set {\<cdot>} xs"
-
-notation fcomp (infixl "\<circ>>" 60)
-notation scomp (infixl "\<circ>\<rightarrow>" 60)
-
-instantiation fset :: (random) random
-begin
-
-definition
-  "Quickcheck.random i = Quickcheck.random i \<circ>\<rightarrow> (\<lambda>xs. Pair (setify xs))"
-
-instance ..
-
-end
-
-no_notation fcomp (infixl "\<circ>>" 60)
-no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
-
-
-subsection {* Lattice instantiation *}
-
-instantiation fset :: (type) boolean_algebra
-begin
-
-definition less_eq_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" where
-  [simp]: "A \<le> B \<longleftrightarrow> member A \<subseteq> member B"
-
-definition less_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" where
-  [simp]: "A < B \<longleftrightarrow> member A \<subset> member B"
-
-definition inf_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
-  [simp]: "inf A B = Fset (member A \<inter> member B)"
-
-definition sup_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
-  [simp]: "sup A B = Fset (member A \<union> member B)"
-
-definition bot_fset :: "'a fset" where
-  [simp]: "bot = Fset {}"
-
-definition top_fset :: "'a fset" where
-  [simp]: "top = Fset UNIV"
-
-definition uminus_fset :: "'a fset \<Rightarrow> 'a fset" where
-  [simp]: "- A = Fset (- (member A))"
-
-definition minus_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
-  [simp]: "A - B = Fset (member A - member B)"
-
-instance proof
-qed (auto intro: fset_eqI)
-
-end
-
-instantiation fset :: (type) complete_lattice
-begin
-
-definition Inf_fset :: "'a fset set \<Rightarrow> 'a fset" where
-  [simp]: "Inf_fset As = Fset (Inf (image member As))"
-
-definition Sup_fset :: "'a fset set \<Rightarrow> 'a fset" where
-  [simp]: "Sup_fset As = Fset (Sup (image member As))"
-
-instance proof
-qed (auto simp add: le_fun_def le_bool_def)
-
-end
-
-
-subsection {* Basic operations *}
-
-definition is_empty :: "'a fset \<Rightarrow> bool" where
-  [simp]: "is_empty A \<longleftrightarrow> More_Set.is_empty (member A)"
-
-lemma is_empty_Set [code]:
-  "is_empty (Set xs) \<longleftrightarrow> List.null xs"
-  by (simp add: is_empty_set)
-
-lemma empty_Set [code]:
-  "bot = Set []"
-  by (simp add: Set_def)
-
-lemma UNIV_Set [code]:
-  "top = Coset []"
-  by (simp add: Coset_def)
-
-definition insert :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
-  [simp]: "insert x A = Fset (Set.insert x (member A))"
-
-lemma insert_Set [code]:
-  "insert x (Set xs) = Set (List.insert x xs)"
-  "insert x (Coset xs) = Coset (removeAll x xs)"
-  by (simp_all add: Set_def Coset_def)
-
-definition remove :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
-  [simp]: "remove x A = Fset (More_Set.remove x (member A))"
-
-lemma remove_Set [code]:
-  "remove x (Set xs) = Set (removeAll x xs)"
-  "remove x (Coset xs) = Coset (List.insert x xs)"
-  by (simp_all add: Set_def Coset_def remove_set_compl)
-    (simp add: More_Set.remove_def)
-
-definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset" where
-  [simp]: "map f A = Fset (image f (member A))"
-
-lemma map_Set [code]:
-  "map f (Set xs) = Set (remdups (List.map f xs))"
-  by (simp add: Set_def)
-
-type_mapper map
-  by (simp_all add: image_image)
-
-definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
-  [simp]: "filter P A = Fset (More_Set.project P (member A))"
-
-lemma filter_Set [code]:
-  "filter P (Set xs) = Set (List.filter P xs)"
-  by (simp add: Set_def project_set)
-
-definition forall :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> bool" where
-  [simp]: "forall P A \<longleftrightarrow> Ball (member A) P"
-
-lemma forall_Set [code]:
-  "forall P (Set xs) \<longleftrightarrow> list_all P xs"
-  by (simp add: Set_def list_all_iff)
-
-definition exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> bool" where
-  [simp]: "exists P A \<longleftrightarrow> Bex (member A) P"
-
-lemma exists_Set [code]:
-  "exists P (Set xs) \<longleftrightarrow> list_ex P xs"
-  by (simp add: Set_def list_ex_iff)
-
-definition card :: "'a fset \<Rightarrow> nat" where
-  [simp]: "card A = Finite_Set.card (member A)"
-
-lemma card_Set [code]:
-  "card (Set xs) = length (remdups xs)"
-proof -
-  have "Finite_Set.card (set (remdups xs)) = length (remdups xs)"
-    by (rule distinct_card) simp
-  then show ?thesis by (simp add: Set_def)
-qed
-
-lemma compl_Set [simp, code]:
-  "- Set xs = Coset xs"
-  by (simp add: Set_def Coset_def)
-
-lemma compl_Coset [simp, code]:
-  "- Coset xs = Set xs"
-  by (simp add: Set_def Coset_def)
-
-
-subsection {* Derived operations *}
-
-lemma subfset_eq_forall [code]:
-  "A \<le> B \<longleftrightarrow> forall (member B) A"
-  by (simp add: subset_eq)
-
-lemma subfset_subfset_eq [code]:
-  "A < B \<longleftrightarrow> A \<le> B \<and> \<not> B \<le> (A :: 'a fset)"
-  by (fact less_le_not_le)
-
-instantiation fset :: (type) equal
-begin
-
-definition [code]:
-  "HOL.equal A B \<longleftrightarrow> A \<le> B \<and> B \<le> (A :: 'a fset)"
-
-instance proof
-qed (simp add: equal_fset_def set_eq [symmetric] fset_eq_iff)
-
-end
-
-lemma [code nbe]:
-  "HOL.equal (A :: 'a fset) A \<longleftrightarrow> True"
-  by (fact equal_refl)
-
-
-subsection {* Functorial operations *}
-
-lemma inter_project [code]:
-  "inf A (Set xs) = Set (List.filter (member A) xs)"
-  "inf A (Coset xs) = foldr remove xs A"
-proof -
-  show "inf A (Set xs) = Set (List.filter (member A) xs)"
-    by (simp add: inter project_def Set_def)
-  have *: "\<And>x::'a. remove = (\<lambda>x. Fset \<circ> More_Set.remove x \<circ> member)"
-    by (simp add: fun_eq_iff)
-  have "member \<circ> fold (\<lambda>x. Fset \<circ> More_Set.remove x \<circ> member) xs =
-    fold More_Set.remove xs \<circ> member"
-    by (rule fold_commute) (simp add: fun_eq_iff)
-  then have "fold More_Set.remove xs (member A) = 
-    member (fold (\<lambda>x. Fset \<circ> More_Set.remove x \<circ> member) xs A)"
-    by (simp add: fun_eq_iff)
-  then have "inf A (Coset xs) = fold remove xs A"
-    by (simp add: Diff_eq [symmetric] minus_set *)
-  moreover have "\<And>x y :: 'a. Fset.remove y \<circ> Fset.remove x = Fset.remove x \<circ> Fset.remove y"
-    by (auto simp add: More_Set.remove_def * intro: ext)
-  ultimately show "inf A (Coset xs) = foldr remove xs A"
-    by (simp add: foldr_fold)
-qed
-
-lemma subtract_remove [code]:
-  "A - Set xs = foldr remove xs A"
-  "A - Coset xs = Set (List.filter (member A) xs)"
-  by (simp_all only: diff_eq compl_Set compl_Coset inter_project)
-
-lemma union_insert [code]:
-  "sup (Set xs) A = foldr insert xs A"
-  "sup (Coset xs) A = Coset (List.filter (Not \<circ> member A) xs)"
-proof -
-  have *: "\<And>x::'a. insert = (\<lambda>x. Fset \<circ> Set.insert x \<circ> member)"
-    by (simp add: fun_eq_iff)
-  have "member \<circ> fold (\<lambda>x. Fset \<circ> Set.insert x \<circ> member) xs =
-    fold Set.insert xs \<circ> member"
-    by (rule fold_commute) (simp add: fun_eq_iff)
-  then have "fold Set.insert xs (member A) =
-    member (fold (\<lambda>x. Fset \<circ> Set.insert x \<circ> member) xs A)"
-    by (simp add: fun_eq_iff)
-  then have "sup (Set xs) A = fold insert xs A"
-    by (simp add: union_set *)
-  moreover have "\<And>x y :: 'a. Fset.insert y \<circ> Fset.insert x = Fset.insert x \<circ> Fset.insert y"
-    by (auto simp add: * intro: ext)
-  ultimately show "sup (Set xs) A = foldr insert xs A"
-    by (simp add: foldr_fold)
-  show "sup (Coset xs) A = Coset (List.filter (Not \<circ> member A) xs)"
-    by (auto simp add: Coset_def)
-qed
-
-context complete_lattice
-begin
-
-definition Infimum :: "'a fset \<Rightarrow> 'a" where
-  [simp]: "Infimum A = Inf (member A)"
-
-lemma Infimum_inf [code]:
-  "Infimum (Set As) = foldr inf As top"
-  "Infimum (Coset []) = bot"
-  by (simp_all add: Inf_set_foldr Inf_UNIV)
-
-definition Supremum :: "'a fset \<Rightarrow> 'a" where
-  [simp]: "Supremum A = Sup (member A)"
-
-lemma Supremum_sup [code]:
-  "Supremum (Set As) = foldr sup As bot"
-  "Supremum (Coset []) = top"
-  by (simp_all add: Sup_set_foldr Sup_UNIV)
-
-end
-
-
-subsection {* Simplified simprules *}
-
-lemma is_empty_simp [simp]:
-  "is_empty A \<longleftrightarrow> member A = {}"
-  by (simp add: More_Set.is_empty_def)
-declare is_empty_def [simp del]
-
-lemma remove_simp [simp]:
-  "remove x A = Fset (member A - {x})"
-  by (simp add: More_Set.remove_def)
-declare remove_def [simp del]
-
-lemma filter_simp [simp]:
-  "filter P A = Fset {x \<in> member A. P x}"
-  by (simp add: More_Set.project_def)
-declare filter_def [simp del]
-
-declare mem_def [simp del]
-
-
-hide_const (open) setify is_empty insert remove map filter forall exists card
-  Inter Union
-
-end
diff -r c059d550afec -r 23904fa13e03 src/HOL/Library/Library.thy
--- a/src/HOL/Library/Library.thy	Tue Nov 23 23:10:13 2010 +0100
+++ b/src/HOL/Library/Library.thy	Tue Nov 23 23:11:06 2010 +0100
@@ -19,7 +19,7 @@
   Formal_Power_Series
   Fraction_Field
   FrechetDeriv
-  Fset
+  Cset
   FuncSet
   Function_Algebras
   Fundamental_Theorem_Algebra
diff -r c059d550afec -r 23904fa13e03 src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Tue Nov 23 23:10:13 2010 +0100
+++ b/src/HOL/Predicate.thy	Tue Nov 23 23:11:06 2010 +0100
@@ -476,15 +476,15 @@
   by (simp add: single_def)
 
 definition bind :: "'a pred \<Rightarrow> ('a \<Rightarrow> 'b pred) \<Rightarrow> 'b pred" (infixl "\<guillemotright>=" 70) where
-  "P \<guillemotright>= f = (SUPR (Predicate.eval P) f)"
+  "P \<guillemotright>= f = (SUPR {x. Predicate.eval P x} f)"
 
 lemma eval_bind [simp]:
-  "eval (P \<guillemotright>= f) = Predicate.eval (SUPR (Predicate.eval P) f)"
+  "eval (P \<guillemotright>= f) = Predicate.eval (SUPR {x. Predicate.eval P x} f)"
   by (simp add: bind_def)
 
 lemma bind_bind:
   "(P \<guillemotright>= Q) \<guillemotright>= R = P \<guillemotright>= (\<lambda>x. Q x \<guillemotright>= R)"
-  by (rule pred_eqI) simp
+  by (rule pred_eqI) auto
 
 lemma bind_single:
   "P \<guillemotright>= single = P"
@@ -496,15 +496,15 @@
 
 lemma bottom_bind:
   "\<bottom> \<guillemotright>= P = \<bottom>"
-  by (rule pred_eqI) simp
+  by (rule pred_eqI) auto
 
 lemma sup_bind:
   "(P \<squnion> Q) \<guillemotright>= R = P \<guillemotright>= R \<squnion> Q \<guillemotright>= R"
-  by (rule pred_eqI) simp
+  by (rule pred_eqI) auto
 
 lemma Sup_bind:
   "(\<Squnion>A \<guillemotright>= f) = \<Squnion>((\<lambda>x. x \<guillemotright>= f) ` A)"
-  by (rule pred_eqI) simp
+  by (rule pred_eqI) auto
 
 lemma pred_iffI:
   assumes "\<And>x. eval A x \<Longrightarrow> eval B x"
@@ -933,8 +933,12 @@
 where
   "the A = (THE x. eval A x)"
 
-lemma the_eq[code]: "the A = singleton (\<lambda>x. not_unique A) A"
-by (auto simp add: the_def singleton_def not_unique_def)
+lemma the_eqI:
+  "(THE x. Predicate.eval P x) = x \<Longrightarrow> Predicate.the P = x"
+  by (simp add: the_def)
+
+lemma the_eq [code]: "the A = singleton (\<lambda>x. not_unique A) A"
+  by (rule the_eqI) (simp add: singleton_def not_unique_def)
 
 code_abort not_unique
 
diff -r c059d550afec -r 23904fa13e03 src/HOL/Quotient_Examples/FSet.thy
--- a/src/HOL/Quotient_Examples/FSet.thy	Tue Nov 23 23:10:13 2010 +0100
+++ b/src/HOL/Quotient_Examples/FSet.thy	Tue Nov 23 23:11:06 2010 +0100
@@ -25,7 +25,7 @@
   unfolding reflp_def symp_def transp_def
   by auto
 
-text {* Fset type *}
+text {* Cset type *}
 
 quotient_type
   'a fset = "'a list" / "list_eq"