# HG changeset patch
# User haftmann
# Date 1248155756 -7200
# Node ID 045e7ca3ea74c7d36a028a0c45e2077d6ccdb2fd
# Parent  2110fcd86efbea48f4ab5bbcc97d620c547d4695# Parent  8f10fb3bb46e3beeb2a092ee5a4d3569b5274ad0
merged

diff -r 2110fcd86efb -r 045e7ca3ea74 src/HOL/PReal.thy
--- a/src/HOL/PReal.thy	Mon Jul 20 20:03:19 2009 +0200
+++ b/src/HOL/PReal.thy	Tue Jul 21 07:55:56 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 2110fcd86efb -r 045e7ca3ea74 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Mon Jul 20 20:03:19 2009 +0200
+++ b/src/HOL/Set.thy	Tue Jul 21 07:55:56 2009 +0200
@@ -1136,10 +1136,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 +1210,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 \<equiv> \<Union>x\<in>S. x"
+  by (simp add: UNION_eq_Union_image image_def)
+
+lemma UNION_def [noatp]:
+  "UNION A B \<equiv> {y. \<exists>x\<in>A. y \<in> B x}"
+  by (rule eq_reflection) (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 +1249,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 +1320,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 \<equiv> INTER S (\<lambda>x. x)"
+  by (simp add: INTER_eq_Inter_image image_def)
+
+lemma INTER_def:
+  "INTER A B \<equiv> {y. \<forall>x\<in>A. y \<in> B x}"
+  by (rule eq_reflection) (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 +1354,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
diff -r 2110fcd86efb -r 045e7ca3ea74 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Mon Jul 20 20:03:19 2009 +0200
+++ b/src/Pure/Isar/class.ML	Tue Jul 21 07:55:56 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 2110fcd86efb -r 045e7ca3ea74 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Mon Jul 20 20:03:19 2009 +0200
+++ b/src/Pure/Isar/locale.ML	Tue Jul 21 07:55:56 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;