# HG changeset patch
# User haftmann
# Date 1248167627 -7200
# Node ID 1c9a3fc45141e66f19425424d4ccec7c8c122278
# Parent  7c39fcfffd6172937cd321c5e320cd9bafceb65b# Parent  0762b9ad83df00c46c702b79e0660307ae60088f
merged

diff -r 7c39fcfffd61 -r 1c9a3fc45141 src/HOL/Auth/Message.thy
--- a/src/HOL/Auth/Message.thy	Tue Jul 21 11:01:07 2009 +0200
+++ b/src/HOL/Auth/Message.thy	Tue Jul 21 11:13:47 2009 +0200
@@ -856,6 +856,8 @@
   Abstraction over i is ESSENTIAL: it delays the dereferencing of claset
   DEPENDS UPON "X" REFERRING TO THE FRADULENT MESSAGE *)
 
+fun impOfSubs th = th RSN (2, @{thm rev_subsetD})
+
 (*Apply rules to break down assumptions of the form
   Y \<in> parts(insert X H)  and  Y \<in> analz(insert X H)
 *)
diff -r 7c39fcfffd61 -r 1c9a3fc45141 src/HOL/PReal.thy
--- a/src/HOL/PReal.thy	Tue Jul 21 11:01:07 2009 +0200
+++ b/src/HOL/PReal.thy	Tue Jul 21 11:13:47 2009 +0200
@@ -52,7 +52,7 @@
 
 definition
   psup :: "preal set => preal" where
-  "psup P = Abs_preal (\<Union>X \<in> P. Rep_preal X)"
+  [code del]: "psup P = Abs_preal (\<Union>X \<in> P. Rep_preal X)"
 
 definition
   add_set :: "[rat set,rat set] => rat set" where
diff -r 7c39fcfffd61 -r 1c9a3fc45141 src/HOL/SET-Protocol/MessageSET.thy
--- a/src/HOL/SET-Protocol/MessageSET.thy	Tue Jul 21 11:01:07 2009 +0200
+++ b/src/HOL/SET-Protocol/MessageSET.thy	Tue Jul 21 11:13:47 2009 +0200
@@ -854,6 +854,8 @@
   Abstraction over i is ESSENTIAL: it delays the dereferencing of claset
   DEPENDS UPON "X" REFERRING TO THE FRADULENT MESSAGE *)
 
+fun impOfSubs th = th RSN (2, @{thm rev_subsetD})
+
 (*Apply rules to break down assumptions of the form
   Y \<in> parts(insert X H)  and  Y \<in> analz(insert X H)
 *)
diff -r 7c39fcfffd61 -r 1c9a3fc45141 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Tue Jul 21 11:01:07 2009 +0200
+++ b/src/HOL/Set.thy	Tue Jul 21 11:13:47 2009 +0200
@@ -80,12 +80,30 @@
 lemma Collect_cong: "(!!x. P x = Q x) ==> {x. P(x)} = {x. Q(x)}"
   by simp
 
+text {*
+Simproc for pulling @{text "x=t"} in @{text "{x. \<dots> & x=t & \<dots>}"}
+to the front (and similarly for @{text "t=x"}):
+*}
+
+setup {*
+let
+  val Coll_perm_tac = rtac @{thm Collect_cong} 1 THEN rtac @{thm iffI} 1 THEN
+    ALLGOALS(EVERY'[REPEAT_DETERM o (etac @{thm conjE}),
+                    DEPTH_SOLVE_1 o (ares_tac [@{thm conjI}])])
+  val defColl_regroup = Simplifier.simproc @{theory}
+    "defined Collect" ["{x. P x & Q x}"]
+    (Quantifier1.rearrange_Coll Coll_perm_tac)
+in
+  Simplifier.map_simpset (fn ss => ss addsimprocs [defColl_regroup])
+end
+*}
+
 lemmas CollectE = CollectD [elim_format]
 
 text {* Set enumerations *}
 
 definition empty :: "'a set" ("{}") where
-  "empty \<equiv> {x. False}"
+  "empty = {x. False}"
 
 definition insert :: "'a \<Rightarrow> 'a set \<Rightarrow> 'a set" where
   insert_compr: "insert a B = {x. x = a \<or> x \<in> B}"
@@ -311,6 +329,23 @@
   in [("Collect", setcompr_tr')] end;
 *}
 
+setup {*
+let
+  val unfold_bex_tac = unfold_tac @{thms "Bex_def"};
+  fun prove_bex_tac ss = unfold_bex_tac ss THEN Quantifier1.prove_one_point_ex_tac;
+  val rearrange_bex = Quantifier1.rearrange_bex prove_bex_tac;
+  val unfold_ball_tac = unfold_tac @{thms "Ball_def"};
+  fun prove_ball_tac ss = unfold_ball_tac ss THEN Quantifier1.prove_one_point_all_tac;
+  val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac;
+  val defBEX_regroup = Simplifier.simproc @{theory}
+    "defined BEX" ["EX x:A. P x & Q x"] rearrange_bex;
+  val defBALL_regroup = Simplifier.simproc @{theory}
+    "defined BALL" ["ALL x:A. P x --> Q x"] rearrange_ball;
+in
+  Simplifier.map_simpset (fn ss => ss addsimprocs [defBALL_regroup, defBEX_regroup])
+end
+*}
+
 lemma ballI [intro!]: "(!!x. x:A ==> P x) ==> ALL x:A. P x"
   by (simp add: Ball_def)
 
@@ -319,20 +354,6 @@
 lemma bspec [dest?]: "ALL x:A. P x ==> x:A ==> P x"
   by (simp add: Ball_def)
 
-lemma ballE [elim]: "ALL x:A. P x ==> (P x ==> Q) ==> (x ~: A ==> Q) ==> Q"
-  by (unfold Ball_def) blast
-
-ML {* bind_thm ("rev_ballE", Thm.permute_prems 1 1 @{thm ballE}) *}
-
-text {*
-  \medskip This tactic takes assumptions @{prop "ALL x:A. P x"} and
-  @{prop "a:A"}; creates assumption @{prop "P a"}.
-*}
-
-ML {*
-  fun ball_tac i = etac @{thm ballE} i THEN contr_tac (i + 1)
-*}
-
 text {*
   Gives better instantiation for bound:
 *}
@@ -341,6 +362,26 @@
   Classical.map_cs (fn cs => cs addbefore ("bspec", datac @{thm bspec} 1))
 *}
 
+ML {*
+structure Simpdata =
+struct
+
+open Simpdata;
+
+val mksimps_pairs = [(@{const_name Ball}, @{thms bspec})] @ mksimps_pairs;
+
+end;
+
+open Simpdata;
+*}
+
+declaration {* fn _ =>
+  Simplifier.map_ss (fn ss => ss setmksimps (mksimps mksimps_pairs))
+*}
+
+lemma ballE [elim]: "ALL x:A. P x ==> (P x ==> Q) ==> (x ~: A ==> Q) ==> Q"
+  by (unfold Ball_def) blast
+
 lemma bexI [intro]: "P x ==> x:A ==> EX x:A. P x"
   -- {* Normally the best argument order: @{prop "P x"} constrains the
     choice of @{prop "x:A"}. *}
@@ -382,24 +423,6 @@
 lemma ball_one_point2 [simp]: "(ALL x:A. a = x --> P x) = (a:A --> P a)"
   by blast
 
-ML {*
-  local
-    val unfold_bex_tac = unfold_tac @{thms "Bex_def"};
-    fun prove_bex_tac ss = unfold_bex_tac ss THEN Quantifier1.prove_one_point_ex_tac;
-    val rearrange_bex = Quantifier1.rearrange_bex prove_bex_tac;
-
-    val unfold_ball_tac = unfold_tac @{thms "Ball_def"};
-    fun prove_ball_tac ss = unfold_ball_tac ss THEN Quantifier1.prove_one_point_all_tac;
-    val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac;
-  in
-    val defBEX_regroup = Simplifier.simproc @{theory}
-      "defined BEX" ["EX x:A. P x & Q x"] rearrange_bex;
-    val defBALL_regroup = Simplifier.simproc @{theory}
-      "defined BALL" ["ALL x:A. P x --> Q x"] rearrange_ball;
-  end;
-
-  Addsimprocs [defBALL_regroup, defBEX_regroup];
-*}
 
 text {* Congruence rules *}
 
@@ -450,25 +473,12 @@
   \medskip Converts @{prop "A \<subseteq> B"} to @{prop "x \<in> A ==> x \<in> B"}.
 *}
 
-ML {*
-  fun impOfSubs th = th RSN (2, @{thm rev_subsetD})
-*}
-
 lemma subsetCE [elim]: "A \<subseteq>  B ==> (c \<notin> A ==> P) ==> (c \<in> B ==> P) ==> P"
   -- {* Classical elimination rule. *}
   by (unfold mem_def) blast
 
 lemma subset_eq: "A \<le> B = (\<forall>x\<in>A. x \<in> B)" by blast
 
-text {*
-  \medskip Takes assumptions @{prop "A \<subseteq> B"}; @{prop "c \<in> A"} and
-  creates the assumption @{prop "c \<in> B"}.
-*}
-
-ML {*
-  fun set_mp_tac i = etac @{thm subsetCE} i THEN mp_tac i
-*}
-
 lemma contra_subsetD: "A \<subseteq> B ==> c \<notin> B ==> c \<notin> A"
   by blast
 
@@ -538,7 +548,7 @@
 subsubsection {* The universal set -- UNIV *}
 
 definition UNIV :: "'a set" where
-  "UNIV \<equiv> {x. True}"
+  "UNIV = {x. True}"
 
 lemma UNIV_I [simp]: "x : UNIV"
   by (simp add: UNIV_def)
@@ -647,7 +657,7 @@
 subsubsection {* Binary union -- Un *}
 
 definition Un :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Un" 65) where
-  "A Un B \<equiv> {x. x \<in> A \<or> x \<in> B}"
+  "A Un B = {x. x \<in> A \<or> x \<in> B}"
 
 notation (xsymbols)
   "Un"  (infixl "\<union>" 65)
@@ -678,7 +688,7 @@
 lemma UnE [elim!]: "c : A Un B ==> (c:A ==> P) ==> (c:B ==> P) ==> P"
   by (unfold Un_def) blast
 
-lemma insert_def: "insert a B \<equiv> {x. x = a} \<union> B"
+lemma insert_def: "insert a B = {x. x = a} \<union> B"
   by (simp add: Collect_def mem_def insert_compr Un_def)
 
 lemma mono_Un: "mono f \<Longrightarrow> f A \<union> f B \<subseteq> f (A \<union> B)"
@@ -690,7 +700,7 @@
 subsubsection {* Binary intersection -- Int *}
 
 definition Int :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Int" 70) where
-  "A Int B \<equiv> {x. x \<in> A \<and> x \<in> B}"
+  "A Int B = {x. x \<in> A \<and> x \<in> B}"
 
 notation (xsymbols)
   "Int"  (infixl "\<inter>" 70)
@@ -883,34 +893,15 @@
   by blast
 
 
-subsubsection {* Some proof tools *}
+subsubsection {* Some rules with @{text "if"} *}
 
 text{* Elimination of @{text"{x. \<dots> & x=t & \<dots>}"}. *}
 
 lemma Collect_conv_if: "{x. x=a & P x} = (if P a then {a} else {})"
-by auto
+  by auto
 
 lemma Collect_conv_if2: "{x. a=x & P x} = (if P a then {a} else {})"
-by auto
-
-text {*
-Simproc for pulling @{text "x=t"} in @{text "{x. \<dots> & x=t & \<dots>}"}
-to the front (and similarly for @{text "t=x"}):
-*}
-
-ML{*
-  local
-    val Coll_perm_tac = rtac @{thm Collect_cong} 1 THEN rtac @{thm iffI} 1 THEN
-    ALLGOALS(EVERY'[REPEAT_DETERM o (etac @{thm conjE}),
-                    DEPTH_SOLVE_1 o (ares_tac [@{thm conjI}])])
-  in
-    val defColl_regroup = Simplifier.simproc @{theory}
-      "defined Collect" ["{x. P x & Q x}"]
-      (Quantifier1.rearrange_Coll Coll_perm_tac)
-  end;
-
-  Addsimprocs [defColl_regroup];
-*}
+  by auto
 
 text {*
   Rewrite rules for boolean case-splitting: faster than @{text
@@ -945,13 +936,6 @@
    ("Collect", [CollectD]), ("Inter", [InterD]), ("INTER", [INT_D])]
  *)
 
-ML {*
-  val mksimps_pairs = [(@{const_name Ball}, @{thms bspec})] @ mksimps_pairs;
-*}
-declaration {* fn _ =>
-  Simplifier.map_ss (fn ss => ss setmksimps (mksimps mksimps_pairs))
-*}
-
 
 subsection {* Complete lattices *}
 
@@ -1029,10 +1013,10 @@
   using top_greatest [of x] by (simp add: le_iff_inf inf_commute)
 
 definition SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
-  "SUPR A f == \<Squnion> (f ` A)"
+  "SUPR A f = \<Squnion> (f ` A)"
 
 definition INFI :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
-  "INFI A f == \<Sqinter> (f ` A)"
+  "INFI A f = \<Sqinter> (f ` A)"
 
 end
 
@@ -1136,10 +1120,43 @@
   by rule (simp add: Sup_fun_def, simp add: empty_def)
 
 
+subsubsection {* Union *}
+
+definition Union :: "'a set set \<Rightarrow> 'a set" where
+  Union_eq [code del]: "Union A = {x. \<exists>B \<in> A. x \<in> B}"
+
+notation (xsymbols)
+  Union  ("\<Union>_" [90] 90)
+
+lemma Sup_set_eq:
+  "\<Squnion>S = \<Union>S"
+proof (rule set_ext)
+  fix x
+  have "(\<exists>Q\<in>{P. \<exists>A\<in>S. P \<longleftrightarrow> x \<in> A}. Q) \<longleftrightarrow> (\<exists>A\<in>S. x \<in> A)"
+    by auto
+  then show "x \<in> \<Squnion>S \<longleftrightarrow> x \<in> \<Union>S"
+    by (simp add: Sup_fun_def Sup_bool_def Union_eq) (simp add: mem_def)
+qed
+
+lemma Union_iff [simp, noatp]:
+  "A \<in> \<Union>C \<longleftrightarrow> (\<exists>X\<in>C. A\<in>X)"
+  by (unfold Union_eq) blast
+
+lemma UnionI [intro]:
+  "X \<in> C \<Longrightarrow> A \<in> X \<Longrightarrow> A \<in> \<Union>C"
+  -- {* The order of the premises presupposes that @{term C} is rigid;
+    @{term A} may be flexible. *}
+  by auto
+
+lemma UnionE [elim!]:
+  "A \<in> \<Union>C \<Longrightarrow> (\<And>X. A\<in>X \<Longrightarrow> X\<in>C \<Longrightarrow> R) \<Longrightarrow> R"
+  by auto
+
+
 subsubsection {* Unions of families *}
 
 definition UNION :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
-  "UNION A B \<equiv> {y. \<exists>x\<in>A. y \<in> B x}"
+  UNION_eq_Union_image: "UNION A B = \<Union>(B`A)"
 
 syntax
   "@UNION1"     :: "pttrns => 'b set => 'b set"           ("(3UN _./ _)" [0, 10] 10)
@@ -1177,8 +1194,22 @@
 in [(@{const_syntax UNION}, btr' "@UNION")] end
 *}
 
-declare UNION_def [noatp]
-
+lemma SUPR_set_eq:
+  "(SUP x:S. f x) = (\<Union>x\<in>S. f x)"
+  by (simp add: SUPR_def UNION_eq_Union_image Sup_set_eq)
+
+lemma Union_def:
+  "\<Union>S = (\<Union>x\<in>S. x)"
+  by (simp add: UNION_eq_Union_image image_def)
+
+lemma UNION_def [noatp]:
+  "UNION A B = {y. \<exists>x\<in>A. y \<in> B x}"
+  by (auto simp add: UNION_eq_Union_image Union_eq)
+  
+lemma Union_image_eq [simp]:
+  "\<Union>(B`A) = (\<Union>x\<in>A. B x)"
+  by (rule sym) (fact UNION_eq_Union_image)
+  
 lemma UN_iff [simp]: "(b: (UN x:A. B x)) = (EX x:A. b: B x)"
   by (unfold UNION_def) blast
 
@@ -1202,10 +1233,49 @@
   by blast
 
 
+subsubsection {* Inter *}
+
+definition Inter :: "'a set set \<Rightarrow> 'a set" where
+  Inter_eq [code del]: "Inter A = {x. \<forall>B \<in> A. x \<in> B}"
+
+notation (xsymbols)
+  Inter  ("\<Inter>_" [90] 90)
+
+lemma Inf_set_eq:
+  "\<Sqinter>S = \<Inter>S"
+proof (rule set_ext)
+  fix x
+  have "(\<forall>Q\<in>{P. \<exists>A\<in>S. P \<longleftrightarrow> x \<in> A}. Q) \<longleftrightarrow> (\<forall>A\<in>S. x \<in> A)"
+    by auto
+  then show "x \<in> \<Sqinter>S \<longleftrightarrow> x \<in> \<Inter>S"
+    by (simp add: Inter_eq Inf_fun_def Inf_bool_def) (simp add: mem_def)
+qed
+
+lemma Inter_iff [simp,noatp]: "(A : Inter C) = (ALL X:C. A:X)"
+  by (unfold Inter_eq) blast
+
+lemma InterI [intro!]: "(!!X. X:C ==> A:X) ==> A : Inter C"
+  by (simp add: Inter_eq)
+
+text {*
+  \medskip A ``destruct'' rule -- every @{term X} in @{term C}
+  contains @{term A} as an element, but @{prop "A:X"} can hold when
+  @{prop "X:C"} does not!  This rule is analogous to @{text spec}.
+*}
+
+lemma InterD [elim]: "A : Inter C ==> X:C ==> A:X"
+  by auto
+
+lemma InterE [elim]: "A : Inter C ==> (X~:C ==> R) ==> (A:X ==> R) ==> R"
+  -- {* ``Classical'' elimination rule -- does not require proving
+    @{prop "X:C"}. *}
+  by (unfold Inter_eq) blast
+
+
 subsubsection {* Intersections of families *}
 
 definition INTER :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
-  "INTER A B \<equiv> {y. \<forall>x\<in>A. y \<in> B x}"
+  INTER_eq_Inter_image: "INTER A B = \<Inter>(B`A)"
 
 syntax
   "@INTER1"     :: "pttrns => 'b set => 'b set"           ("(3INT _./ _)" [0, 10] 10)
@@ -1234,6 +1304,22 @@
 in [(@{const_syntax INTER}, btr' "@INTER")] end
 *}
 
+lemma INFI_set_eq:
+  "(INF x:S. f x) = (\<Inter>x\<in>S. f x)"
+  by (simp add: INFI_def INTER_eq_Inter_image Inf_set_eq)
+
+lemma Inter_def:
+  "Inter S = INTER S (\<lambda>x. x)"
+  by (simp add: INTER_eq_Inter_image image_def)
+
+lemma INTER_def:
+  "INTER A B = {y. \<forall>x\<in>A. y \<in> B x}"
+  by (auto simp add: INTER_eq_Inter_image Inter_eq)
+
+lemma Inter_image_eq [simp]:
+  "\<Inter>(B`A) = (\<Inter>x\<in>A. B x)"
+  by (rule sym) (fact INTER_eq_Inter_image)
+
 lemma INT_iff [simp]: "(b: (INT x:A. B x)) = (ALL x:A. b: B x)"
   by (unfold INTER_def) blast
 
@@ -1252,99 +1338,6 @@
   by (simp add: INTER_def)
 
 
-subsubsection {* Union *}
-
-definition Union :: "'a set set \<Rightarrow> 'a set" where
-  "Union S \<equiv> UNION S (\<lambda>x. x)"
-
-notation (xsymbols)
-  Union  ("\<Union>_" [90] 90)
-
-lemma Union_image_eq [simp]:
-  "\<Union>(B`A) = (\<Union>x\<in>A. B x)"
-  by (auto simp add: Union_def UNION_def image_def)
-
-lemma Union_eq:
-  "\<Union>A = {x. \<exists>B \<in> A. x \<in> B}"
-  by (simp add: Union_def UNION_def)
-
-lemma Sup_set_eq:
-  "\<Squnion>S = \<Union>S"
-proof (rule set_ext)
-  fix x
-  have "(\<exists>Q\<in>{P. \<exists>A\<in>S. P \<longleftrightarrow> x \<in> A}. Q) \<longleftrightarrow> (\<exists>A\<in>S. x \<in> A)"
-    by auto
-  then show "x \<in> \<Squnion>S \<longleftrightarrow> x \<in> \<Union>S"
-    by (simp add: Union_eq Sup_fun_def Sup_bool_def) (simp add: mem_def)
-qed
-
-lemma SUPR_set_eq:
-  "(SUP x:S. f x) = (\<Union>x\<in>S. f x)"
-  by (simp add: SUPR_def Sup_set_eq)
-
-lemma Union_iff [simp,noatp]: "(A : Union C) = (EX X:C. A:X)"
-  by (unfold Union_def) blast
-
-lemma UnionI [intro]: "X:C ==> A:X ==> A : Union C"
-  -- {* The order of the premises presupposes that @{term C} is rigid;
-    @{term A} may be flexible. *}
-  by auto
-
-lemma UnionE [elim!]: "A : Union C ==> (!!X. A:X ==> X:C ==> R) ==> R"
-  by (unfold Union_def) blast
-
-
-subsubsection {* Inter *}
-
-definition Inter :: "'a set set \<Rightarrow> 'a set" where
-  "Inter S \<equiv> INTER S (\<lambda>x. x)"
-
-notation (xsymbols)
-  Inter  ("\<Inter>_" [90] 90)
-
-lemma Inter_image_eq [simp]:
-  "\<Inter>(B`A) = (\<Inter>x\<in>A. B x)"
-  by (auto simp add: Inter_def INTER_def image_def)
-
-lemma Inter_eq:
-  "\<Inter>A = {x. \<forall>B \<in> A. x \<in> B}"
-  by (simp add: Inter_def INTER_def)
-
-lemma Inf_set_eq:
-  "\<Sqinter>S = \<Inter>S"
-proof (rule set_ext)
-  fix x
-  have "(\<forall>Q\<in>{P. \<exists>A\<in>S. P \<longleftrightarrow> x \<in> A}. Q) \<longleftrightarrow> (\<forall>A\<in>S. x \<in> A)"
-    by auto
-  then show "x \<in> \<Sqinter>S \<longleftrightarrow> x \<in> \<Inter>S"
-    by (simp add: Inter_eq Inf_fun_def Inf_bool_def) (simp add: mem_def)
-qed
-
-lemma INFI_set_eq:
-  "(INF x:S. f x) = (\<Inter>x\<in>S. f x)"
-  by (simp add: INFI_def Inf_set_eq)
-
-lemma Inter_iff [simp,noatp]: "(A : Inter C) = (ALL X:C. A:X)"
-  by (unfold Inter_def) blast
-
-lemma InterI [intro!]: "(!!X. X:C ==> A:X) ==> A : Inter C"
-  by (simp add: Inter_def)
-
-text {*
-  \medskip A ``destruct'' rule -- every @{term X} in @{term C}
-  contains @{term A} as an element, but @{prop "A:X"} can hold when
-  @{prop "X:C"} does not!  This rule is analogous to @{text spec}.
-*}
-
-lemma InterD [elim]: "A : Inter C ==> X:C ==> A:X"
-  by auto
-
-lemma InterE [elim]: "A : Inter C ==> (X~:C ==> R) ==> (A:X ==> R) ==> R"
-  -- {* ``Classical'' elimination rule -- does not require proving
-    @{prop "X:C"}. *}
-  by (unfold Inter_def) blast
-
-
 no_notation
   less_eq  (infix "\<sqsubseteq>" 50) and
   less (infix "\<sqsubset>" 50) and
@@ -2467,23 +2460,24 @@
 
 text {* Rudimentary code generation *}
 
-lemma empty_code [code]: "{} x \<longleftrightarrow> False"
-  unfolding empty_def Collect_def ..
-
-lemma UNIV_code [code]: "UNIV x \<longleftrightarrow> True"
-  unfolding UNIV_def Collect_def ..
+lemma [code]: "{} = bot"
+  by (rule sym) (fact bot_set_eq)
+
+lemma [code]: "UNIV = top"
+  by (rule sym) (fact top_set_eq)
+
+lemma [code]: "op \<inter> = inf"
+  by (rule ext)+ (simp add: inf_set_eq)
+
+lemma [code]: "op \<union> = sup"
+  by (rule ext)+ (simp add: sup_set_eq)
 
 lemma insert_code [code]: "insert y A x \<longleftrightarrow> y = x \<or> A x"
-  unfolding insert_def Collect_def mem_def Un_def by auto
-
-lemma inter_code [code]: "(A \<inter> B) x \<longleftrightarrow> A x \<and> B x"
-  unfolding Int_def Collect_def mem_def ..
-
-lemma union_code [code]: "(A \<union> B) x \<longleftrightarrow> A x \<or> B x"
-  unfolding Un_def Collect_def mem_def ..
+  by (auto simp add: insert_compr Collect_def mem_def)
 
 lemma vimage_code [code]: "(f -` A) x = A (f x)"
-  unfolding vimage_def Collect_def mem_def ..
+  by (simp add: vimage_def Collect_def mem_def)
+
 
 text {* Misc theorem and ML bindings *}
 
diff -r 7c39fcfffd61 -r 1c9a3fc45141 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Tue Jul 21 11:01:07 2009 +0200
+++ b/src/Pure/Isar/class.ML	Tue Jul 21 11:13:47 2009 +0200
@@ -68,9 +68,8 @@
     val base_morph = inst_morph
       $> Morphism.binding_morphism (Binding.prefix false (class_prefix class))
       $> Element.satisfy_morphism (the_list wit);
-    val defs = these_defs thy sups;
-    val eq_morph = Element.eq_morphism thy defs;
-    val morph = base_morph $> eq_morph;
+    val eqs = these_defs thy sups;
+    val eq_morph = Element.eq_morphism thy eqs;
 
     (* assm_intro *)
     fun prove_assm_intro thm =
@@ -97,7 +96,7 @@
            ORELSE' Tactic.assume_tac));
     val of_class = SkipProof.prove_global thy [] [] of_class_prop (K tac);
 
-  in (base_morph, morph, export_morph, axiom, assm_intro, of_class) end;
+  in (base_morph, eqs, export_morph, axiom, assm_intro, of_class) end;
 
 
 (* reading and processing class specifications *)
@@ -284,9 +283,8 @@
     ||> Theory.checkpoint
     |-> (fn (param_map, params, assm_axiom) =>
        `(fn thy => calculate thy class sups base_sort param_map assm_axiom)
-    #-> (fn (base_morph, morph, export_morph, axiom, assm_intro, of_class) =>
-       Locale.add_registration (class, (morph, export_morph))
-    #> Context.theory_map (Locale.activate_facts (class, morph $> export_morph))
+    #-> (fn (base_morph, eqs, export_morph, axiom, assm_intro, of_class) =>
+       Locale.add_registration_eqs (class, base_morph) eqs export_morph
     #> register class sups params base_sort base_morph axiom assm_intro of_class))
     |> TheoryTarget.init (SOME class)
     |> pair class
diff -r 7c39fcfffd61 -r 1c9a3fc45141 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Tue Jul 21 11:01:07 2009 +0200
+++ b/src/Pure/Isar/locale.ML	Tue Jul 21 11:13:47 2009 +0200
@@ -68,9 +68,8 @@
   val intro_locales_tac: bool -> Proof.context -> thm list -> tactic
 
   (* Registrations and dependencies *)
-  val add_registration: string * (morphism * morphism) -> theory -> theory
+  val add_registration_eqs: string * morphism -> thm list -> morphism -> theory -> theory
   val amend_registration: morphism -> string * morphism -> theory -> theory
-  val add_registration_eqs: string * morphism -> thm list -> morphism -> theory -> theory
   val add_dependency: string -> string * morphism -> morphism -> theory -> theory
 
   (* Diagnostic *)
@@ -295,8 +294,7 @@
 fun activate_declarations dep = Context.proof_map (fn context =>
   let
     val thy = Context.theory_of context;
-    val context' = roundup thy activate_decls dep (get_idents context, context) |-> put_idents;
-  in context' end);
+  in roundup thy activate_decls dep (get_idents context, context) |-> put_idents end);
 
 fun activate_facts dep context =
   let
@@ -346,11 +344,6 @@
 fun all_registrations thy = Registrations.get thy
   |> map reg_morph;
 
-fun add_registration (name, (base_morph, export)) thy =
-  roundup thy (fn (name', morph') => Registrations.map (cons ((name', (morph', export)), stamp ())))
-    (name, base_morph) (get_idents (Context.Theory thy), thy)
-  (* FIXME |-> (Context.theory_map o put_idents_diag)*) |> snd;
-
 fun amend_registration morph (name, base_morph) thy =
   let
     val regs = map #1 (Registrations.get thy);
@@ -373,8 +366,10 @@
     val morph = if null eqns then proto_morph
       else proto_morph $> Element.eq_morphism thy eqns;
   in
-    thy
-    |> add_registration (dep, (morph, export))
+    (get_idents (Context.Theory thy), thy)
+    |> roundup thy (fn (dep', morph') =>
+        Registrations.map (cons ((dep', (morph', export)), stamp ()))) (dep, morph)
+    |> snd
     |> Context.theory_map (activate_facts (dep, morph $> export))
   end;