# HG changeset patch
# User wenzelm
# Date 1331499973 -3600
# Node ID bad72cba8a92030ae308f7af689e3acfe4a382fe
# Parent  9100e6aa92728ceb001bb192d54d633df5396d51# Parent  11050f8e5f8e7f8925a29f3f468a68fa2d03534a
merged

diff -r 9100e6aa9272 -r bad72cba8a92 src/HOL/HOLCF/Deflation.thy
--- a/src/HOL/HOLCF/Deflation.thy	Sun Mar 11 20:18:38 2012 +0100
+++ b/src/HOL/HOLCF/Deflation.thy	Sun Mar 11 22:06:13 2012 +0100
@@ -379,9 +379,9 @@
     by simp
 qed
 
-locale pcpo_ep_pair = ep_pair +
-  constrains e :: "'a::pcpo \<rightarrow> 'b::pcpo"
-  constrains p :: "'b::pcpo \<rightarrow> 'a::pcpo"
+locale pcpo_ep_pair = ep_pair e p
+  for e :: "'a::pcpo \<rightarrow> 'b::pcpo"
+  and p :: "'b::pcpo \<rightarrow> 'a::pcpo"
 begin
 
 lemma e_strict [simp]: "e\<cdot>\<bottom> = \<bottom>"
diff -r 9100e6aa9272 -r bad72cba8a92 src/HOL/HOLCF/Universal.thy
--- a/src/HOL/HOLCF/Universal.thy	Sun Mar 11 20:18:38 2012 +0100
+++ b/src/HOL/HOLCF/Universal.thy	Sun Mar 11 22:06:13 2012 +0100
@@ -291,8 +291,8 @@
 text {* We use a locale to parameterize the construction over a chain
 of approx functions on the type to be embedded. *}
 
-locale bifinite_approx_chain = approx_chain +
-  constrains approx :: "nat \<Rightarrow> 'a::bifinite \<rightarrow> 'a"
+locale bifinite_approx_chain =
+  approx_chain approx for approx :: "nat \<Rightarrow> 'a::bifinite \<rightarrow> 'a"
 begin
 
 subsubsection {* Choosing a maximal element from a finite set *}
diff -r 9100e6aa9272 -r bad72cba8a92 src/HOL/Hahn_Banach/Function_Norm.thy
--- a/src/HOL/Hahn_Banach/Function_Norm.thy	Sun Mar 11 20:18:38 2012 +0100
+++ b/src/HOL/Hahn_Banach/Function_Norm.thy	Sun Mar 11 22:06:13 2012 +0100
@@ -21,7 +21,8 @@
   linear forms:
 *}
 
-locale continuous = var_V + norm_syntax + linearform +
+locale continuous = linearform +
+  fixes norm :: "_ \<Rightarrow> real"    ("\<parallel>_\<parallel>")
   assumes bounded: "\<exists>c. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>"
 
 declare continuous.intro [intro?] continuous_axioms.intro [intro?]
@@ -30,11 +31,11 @@
   fixes norm :: "_ \<Rightarrow> real"  ("\<parallel>_\<parallel>")
   assumes "linearform V f"
   assumes r: "\<And>x. x \<in> V \<Longrightarrow> \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>"
-  shows "continuous V norm f"
+  shows "continuous V f norm"
 proof
   show "linearform V f" by fact
   from r have "\<exists>c. \<forall>x\<in>V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" by blast
-  then show "continuous_axioms V norm f" ..
+  then show "continuous_axioms V f norm" ..
 qed
 
 
@@ -71,7 +72,8 @@
   supremum exists (otherwise it is undefined).
 *}
 
-locale fn_norm = norm_syntax +
+locale fn_norm =
+  fixes norm :: "_ \<Rightarrow> real"    ("\<parallel>_\<parallel>")
   fixes B defines "B V f \<equiv> {0} \<union> {\<bar>f x\<bar> / \<parallel>x\<parallel> | x. x \<noteq> 0 \<and> x \<in> V}"
   fixes fn_norm ("\<parallel>_\<parallel>\<hyphen>_" [0, 1000] 999)
   defines "\<parallel>f\<parallel>\<hyphen>V \<equiv> \<Squnion>(B V f)"
@@ -87,10 +89,10 @@
 *}
 
 lemma (in normed_vectorspace_with_fn_norm) fn_norm_works:
-  assumes "continuous V norm f"
+  assumes "continuous V f norm"
   shows "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
 proof -
-  interpret continuous V norm f by fact
+  interpret continuous V f norm by fact
   txt {* The existence of the supremum is shown using the
     completeness of the reals. Completeness means, that every
     non-empty bounded set of reals has a supremum. *}
@@ -154,39 +156,39 @@
 qed
 
 lemma (in normed_vectorspace_with_fn_norm) fn_norm_ub [iff?]:
-  assumes "continuous V norm f"
+  assumes "continuous V f norm"
   assumes b: "b \<in> B V f"
   shows "b \<le> \<parallel>f\<parallel>\<hyphen>V"
 proof -
-  interpret continuous V norm f by fact
+  interpret continuous V f norm by fact
   have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
-    using `continuous V norm f` by (rule fn_norm_works)
+    using `continuous V f norm` by (rule fn_norm_works)
   from this and b show ?thesis ..
 qed
 
 lemma (in normed_vectorspace_with_fn_norm) fn_norm_leastB:
-  assumes "continuous V norm f"
+  assumes "continuous V f norm"
   assumes b: "\<And>b. b \<in> B V f \<Longrightarrow> b \<le> y"
   shows "\<parallel>f\<parallel>\<hyphen>V \<le> y"
 proof -
-  interpret continuous V norm f by fact
+  interpret continuous V f norm by fact
   have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
-    using `continuous V norm f` by (rule fn_norm_works)
+    using `continuous V f norm` by (rule fn_norm_works)
   from this and b show ?thesis ..
 qed
 
 text {* The norm of a continuous function is always @{text "\<ge> 0"}. *}
 
 lemma (in normed_vectorspace_with_fn_norm) fn_norm_ge_zero [iff]:
-  assumes "continuous V norm f"
+  assumes "continuous V f norm"
   shows "0 \<le> \<parallel>f\<parallel>\<hyphen>V"
 proof -
-  interpret continuous V norm f by fact
+  interpret continuous V f norm by fact
   txt {* The function norm is defined as the supremum of @{text B}.
     So it is @{text "\<ge> 0"} if all elements in @{text B} are @{text "\<ge>
     0"}, provided the supremum exists and @{text B} is not empty. *}
   have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
-    using `continuous V norm f` by (rule fn_norm_works)
+    using `continuous V f norm` by (rule fn_norm_works)
   moreover have "0 \<in> B V f" ..
   ultimately show ?thesis ..
 qed
@@ -199,11 +201,11 @@
 *}
 
 lemma (in normed_vectorspace_with_fn_norm) fn_norm_le_cong:
-  assumes "continuous V norm f" "linearform V f"
+  assumes "continuous V f norm" "linearform V f"
   assumes x: "x \<in> V"
   shows "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>"
 proof -
-  interpret continuous V norm f by fact
+  interpret continuous V f norm by fact
   interpret linearform V f by fact
   show ?thesis
   proof cases
@@ -212,7 +214,7 @@
     also have "f 0 = 0" by rule unfold_locales
     also have "\<bar>\<dots>\<bar> = 0" by simp
     also have a: "0 \<le> \<parallel>f\<parallel>\<hyphen>V"
-      using `continuous V norm f` by (rule fn_norm_ge_zero)
+      using `continuous V f norm` by (rule fn_norm_ge_zero)
     from x have "0 \<le> norm x" ..
     with a have "0 \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" by (simp add: zero_le_mult_iff)
     finally show "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" .
@@ -225,7 +227,7 @@
       from x show "0 \<le> \<parallel>x\<parallel>" ..
       from x and neq have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<in> B V f"
         by (auto simp add: B_def divide_inverse)
-      with `continuous V norm f` show "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> \<parallel>f\<parallel>\<hyphen>V"
+      with `continuous V f norm` show "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> \<parallel>f\<parallel>\<hyphen>V"
         by (rule fn_norm_ub)
     qed
     finally show ?thesis .
@@ -241,11 +243,11 @@
 *}
 
 lemma (in normed_vectorspace_with_fn_norm) fn_norm_least [intro?]:
-  assumes "continuous V norm f"
+  assumes "continuous V f norm"
   assumes ineq: "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" and ge: "0 \<le> c"
   shows "\<parallel>f\<parallel>\<hyphen>V \<le> c"
 proof -
-  interpret continuous V norm f by fact
+  interpret continuous V f norm by fact
   show ?thesis
   proof (rule fn_norm_leastB [folded B_def fn_norm_def])
     fix b assume b: "b \<in> B V f"
@@ -272,7 +274,7 @@
       qed
       finally show ?thesis .
     qed
-  qed (insert `continuous V norm f`, simp_all add: continuous_def)
+  qed (insert `continuous V f norm`, simp_all add: continuous_def)
 qed
 
 end
diff -r 9100e6aa9272 -r bad72cba8a92 src/HOL/Hahn_Banach/Hahn_Banach.thy
--- a/src/HOL/Hahn_Banach/Hahn_Banach.thy	Sun Mar 11 20:18:38 2012 +0100
+++ b/src/HOL/Hahn_Banach/Hahn_Banach.thy	Sun Mar 11 22:06:13 2012 +0100
@@ -356,9 +356,9 @@
   fixes fn_norm ("\<parallel>_\<parallel>\<hyphen>_" [0, 1000] 999)
   defines "\<And>V f. \<parallel>f\<parallel>\<hyphen>V \<equiv> \<Squnion>(B V f)"
   assumes E_norm: "normed_vectorspace E norm" and FE: "subspace F E"
-    and linearform: "linearform F f" and "continuous F norm f"
+    and linearform: "linearform F f" and "continuous F f norm"
   shows "\<exists>g. linearform E g
-     \<and> continuous E norm g
+     \<and> continuous E g norm
      \<and> (\<forall>x \<in> F. g x = f x)
      \<and> \<parallel>g\<parallel>\<hyphen>E = \<parallel>f\<parallel>\<hyphen>F"
 proof -
@@ -367,7 +367,7 @@
     by (auto simp: B_def fn_norm_def) intro_locales
   interpret subspace F E by fact
   interpret linearform F f by fact
-  interpret continuous F norm f by fact
+  interpret continuous F f norm by fact
   have E: "vectorspace E" by intro_locales
   have F: "vectorspace F" by rule intro_locales
   have F_norm: "normed_vectorspace F norm"
@@ -375,7 +375,7 @@
   have ge_zero: "0 \<le> \<parallel>f\<parallel>\<hyphen>F"
     by (rule normed_vectorspace_with_fn_norm.fn_norm_ge_zero
       [OF normed_vectorspace_with_fn_norm.intro,
-       OF F_norm `continuous F norm f` , folded B_def fn_norm_def])
+       OF F_norm `continuous F f norm` , folded B_def fn_norm_def])
   txt {* We define a function @{text p} on @{text E} as follows:
     @{text "p x = \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>"} *}
   def p \<equiv> "\<lambda>x. \<parallel>f\<parallel>\<hyphen>F * \<parallel>x\<parallel>"
@@ -422,7 +422,7 @@
   have "\<forall>x \<in> F. \<bar>f x\<bar> \<le> p x"
   proof
     fix x assume "x \<in> F"
-    with `continuous F norm f` and linearform
+    with `continuous F f norm` and linearform
     show "\<bar>f x\<bar> \<le> p x"
       unfolding p_def by (rule normed_vectorspace_with_fn_norm.fn_norm_le_cong
         [OF normed_vectorspace_with_fn_norm.intro,
@@ -442,7 +442,7 @@
 
   txt {* We furthermore have to show that @{text g} is also continuous: *}
 
-  have g_cont: "continuous E norm g" using linearformE
+  have g_cont: "continuous E g norm" using linearformE
   proof
     fix x assume "x \<in> E"
     with b show "\<bar>g x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>F * \<parallel>x\<parallel>"
@@ -500,7 +500,7 @@
       show "0 \<le> \<parallel>g\<parallel>\<hyphen>E"
         using g_cont
         by (rule fn_norm_ge_zero [of g, folded B_def fn_norm_def])
-      show "continuous F norm f" by fact
+      show "continuous F f norm" by fact
     qed
   qed
   with linearformE a g_cont show ?thesis by blast
diff -r 9100e6aa9272 -r bad72cba8a92 src/HOL/Hahn_Banach/Normed_Space.thy
--- a/src/HOL/Hahn_Banach/Normed_Space.thy	Sun Mar 11 20:18:38 2012 +0100
+++ b/src/HOL/Hahn_Banach/Normed_Space.thy	Sun Mar 11 22:06:13 2012 +0100
@@ -16,11 +16,9 @@
   definite, absolute homogenous and subadditive.
 *}
 
-locale norm_syntax =
+locale seminorm =
+  fixes V :: "'a\<Colon>{minus, plus, zero, uminus} set"
   fixes norm :: "'a \<Rightarrow> real"    ("\<parallel>_\<parallel>")
-
-locale seminorm = var_V + norm_syntax +
-  constrains V :: "'a\<Colon>{minus, plus, zero, uminus} set"
   assumes ge_zero [iff?]: "x \<in> V \<Longrightarrow> 0 \<le> \<parallel>x\<parallel>"
     and abs_homogenous [iff?]: "x \<in> V \<Longrightarrow> \<parallel>a \<cdot> x\<parallel> = \<bar>a\<bar> * \<parallel>x\<parallel>"
     and subadditive [iff?]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> \<parallel>x + y\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>y\<parallel>"
diff -r 9100e6aa9272 -r bad72cba8a92 src/HOL/Hahn_Banach/Vector_Space.thy
--- a/src/HOL/Hahn_Banach/Vector_Space.thy	Sun Mar 11 20:18:38 2012 +0100
+++ b/src/HOL/Hahn_Banach/Vector_Space.thy	Sun Mar 11 22:06:13 2012 +0100
@@ -38,9 +38,8 @@
   the neutral element of scalar multiplication.
 *}
 
-locale var_V = fixes V
-
-locale vectorspace = var_V +
+locale vectorspace =
+  fixes V
   assumes non_empty [iff, intro?]: "V \<noteq> {}"
     and add_closed [iff]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x + y \<in> V"
     and mult_closed [iff]: "x \<in> V \<Longrightarrow> a \<cdot> x \<in> V"
diff -r 9100e6aa9272 -r bad72cba8a92 src/HOL/Library/Numeral_Type.thy
--- a/src/HOL/Library/Numeral_Type.thy	Sun Mar 11 20:18:38 2012 +0100
+++ b/src/HOL/Library/Numeral_Type.thy	Sun Mar 11 22:06:13 2012 +0100
@@ -135,8 +135,8 @@
 
 end
 
-locale mod_ring = mod_type +
-  constrains n :: int
+locale mod_ring = mod_type n Rep Abs
+  for n :: int
   and Rep :: "'a::{number_ring} \<Rightarrow> int"
   and Abs :: "int \<Rightarrow> 'a::{number_ring}"
 begin
diff -r 9100e6aa9272 -r bad72cba8a92 src/HOL/RealVector.thy
--- a/src/HOL/RealVector.thy	Sun Mar 11 20:18:38 2012 +0100
+++ b/src/HOL/RealVector.thy	Sun Mar 11 22:06:13 2012 +0100
@@ -954,8 +954,7 @@
 
 subsection {* Bounded Linear and Bilinear Operators *}
 
-locale bounded_linear = additive +
-  constrains f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
+locale bounded_linear = additive f for f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" +
   assumes scaleR: "f (scaleR r x) = scaleR r (f x)"
   assumes bounded: "\<exists>K. \<forall>x. norm (f x) \<le> norm x * K"
 begin
diff -r 9100e6aa9272 -r bad72cba8a92 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Sun Mar 11 20:18:38 2012 +0100
+++ b/src/Pure/General/name_space.ML	Sun Mar 11 22:06:13 2012 +0100
@@ -14,6 +14,7 @@
   type T
   val empty: string -> T
   val kind_of: T -> string
+  val defined_entry: T -> string -> bool
   val the_entry: T -> string ->
     {concealed: bool, group: serial option, theory_name: string, pos: Position.T, id: serial}
   val entry_ord: T -> string * string -> order
@@ -117,6 +118,8 @@
 
 fun kind_of (Name_Space {kind, ...}) = kind;
 
+fun defined_entry (Name_Space {entries, ...}) = Symtab.defined entries;
+
 fun the_entry (Name_Space {kind, entries, ...}) name =
   (case Symtab.lookup entries name of
     NONE => error ("Unknown " ^ kind ^ " " ^ quote name)
diff -r 9100e6aa9272 -r bad72cba8a92 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Sun Mar 11 20:18:38 2012 +0100
+++ b/src/Pure/Isar/locale.ML	Sun Mar 11 22:06:13 2012 +0100
@@ -291,7 +291,7 @@
 in
 
 (* Note that while identifiers always have the external (exported) view, activate_dep
-  is presented with the internal view. *)
+   is presented with the internal view. *)
 
 fun roundup thy activate_dep export (name, morph) (marked, input) =
   let
@@ -488,13 +488,9 @@
     else
       (Idents.get context, context)
       (* add new registrations with inherited mixins *)
-      |> roundup thy (add_reg thy export) export (name, morph)
-      |> snd
+      |> (snd o roundup thy (add_reg thy export) export (name, morph))
       (* add mixin *)
-      |>
-        (case mixin of
-          NONE => I
-        | SOME mixin => amend_registration (name, morph) mixin export)
+      |> (case mixin of NONE => I | SOME mixin => amend_registration (name, morph) mixin export)
       (* activate import hierarchy as far as not already active *)
       |> activate_facts (SOME export) (name, morph)
   end;
diff -r 9100e6aa9272 -r bad72cba8a92 src/Pure/variable.ML
--- a/src/Pure/variable.ML	Sun Mar 11 20:18:38 2012 +0100
+++ b/src/Pure/variable.ML	Sun Mar 11 22:06:13 2012 +0100
@@ -292,8 +292,8 @@
 
 (* specialized name space *)
 
-fun is_fixed ctxt x = can (Name_Space.the_entry (fixes_space ctxt)) x;
-fun newly_fixed inner outer x = is_fixed inner x andalso not (is_fixed outer x);
+val is_fixed = Name_Space.defined_entry o fixes_space;
+fun newly_fixed inner outer = is_fixed inner andf (not o is_fixed outer);
 
 val fixed_ord = Name_Space.entry_ord o fixes_space;
 val intern_fixed = Name_Space.intern o fixes_space;
@@ -406,7 +406,7 @@
 fun export_inst inner outer =
   let
     val declared_outer = is_declared outer;
-    fun still_fixed x = is_fixed outer x orelse not (is_fixed inner x);
+    val still_fixed = not o newly_fixed inner outer;
 
     val gen_fixes =
       Symtab.fold (fn (y, _) => not (is_fixed outer y) ? cons y)