merged
authorwenzelm
Sun Mar 11 22:06:13 2012 +0100 (2012-03-11)
changeset 46872bad72cba8a92
parent 46871 9100e6aa9272
parent 46870 11050f8e5f8e
child 46873 7a73f181cbcf
child 46877 059d20d08ff1
child 46882 6242b4bc05bc
merged
     1.1 --- a/src/HOL/HOLCF/Deflation.thy	Sun Mar 11 20:18:38 2012 +0100
     1.2 +++ b/src/HOL/HOLCF/Deflation.thy	Sun Mar 11 22:06:13 2012 +0100
     1.3 @@ -379,9 +379,9 @@
     1.4      by simp
     1.5  qed
     1.6  
     1.7 -locale pcpo_ep_pair = ep_pair +
     1.8 -  constrains e :: "'a::pcpo \<rightarrow> 'b::pcpo"
     1.9 -  constrains p :: "'b::pcpo \<rightarrow> 'a::pcpo"
    1.10 +locale pcpo_ep_pair = ep_pair e p
    1.11 +  for e :: "'a::pcpo \<rightarrow> 'b::pcpo"
    1.12 +  and p :: "'b::pcpo \<rightarrow> 'a::pcpo"
    1.13  begin
    1.14  
    1.15  lemma e_strict [simp]: "e\<cdot>\<bottom> = \<bottom>"
     2.1 --- a/src/HOL/HOLCF/Universal.thy	Sun Mar 11 20:18:38 2012 +0100
     2.2 +++ b/src/HOL/HOLCF/Universal.thy	Sun Mar 11 22:06:13 2012 +0100
     2.3 @@ -291,8 +291,8 @@
     2.4  text {* We use a locale to parameterize the construction over a chain
     2.5  of approx functions on the type to be embedded. *}
     2.6  
     2.7 -locale bifinite_approx_chain = approx_chain +
     2.8 -  constrains approx :: "nat \<Rightarrow> 'a::bifinite \<rightarrow> 'a"
     2.9 +locale bifinite_approx_chain =
    2.10 +  approx_chain approx for approx :: "nat \<Rightarrow> 'a::bifinite \<rightarrow> 'a"
    2.11  begin
    2.12  
    2.13  subsubsection {* Choosing a maximal element from a finite set *}
     3.1 --- a/src/HOL/Hahn_Banach/Function_Norm.thy	Sun Mar 11 20:18:38 2012 +0100
     3.2 +++ b/src/HOL/Hahn_Banach/Function_Norm.thy	Sun Mar 11 22:06:13 2012 +0100
     3.3 @@ -21,7 +21,8 @@
     3.4    linear forms:
     3.5  *}
     3.6  
     3.7 -locale continuous = var_V + norm_syntax + linearform +
     3.8 +locale continuous = linearform +
     3.9 +  fixes norm :: "_ \<Rightarrow> real"    ("\<parallel>_\<parallel>")
    3.10    assumes bounded: "\<exists>c. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>"
    3.11  
    3.12  declare continuous.intro [intro?] continuous_axioms.intro [intro?]
    3.13 @@ -30,11 +31,11 @@
    3.14    fixes norm :: "_ \<Rightarrow> real"  ("\<parallel>_\<parallel>")
    3.15    assumes "linearform V f"
    3.16    assumes r: "\<And>x. x \<in> V \<Longrightarrow> \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>"
    3.17 -  shows "continuous V norm f"
    3.18 +  shows "continuous V f norm"
    3.19  proof
    3.20    show "linearform V f" by fact
    3.21    from r have "\<exists>c. \<forall>x\<in>V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" by blast
    3.22 -  then show "continuous_axioms V norm f" ..
    3.23 +  then show "continuous_axioms V f norm" ..
    3.24  qed
    3.25  
    3.26  
    3.27 @@ -71,7 +72,8 @@
    3.28    supremum exists (otherwise it is undefined).
    3.29  *}
    3.30  
    3.31 -locale fn_norm = norm_syntax +
    3.32 +locale fn_norm =
    3.33 +  fixes norm :: "_ \<Rightarrow> real"    ("\<parallel>_\<parallel>")
    3.34    fixes B defines "B V f \<equiv> {0} \<union> {\<bar>f x\<bar> / \<parallel>x\<parallel> | x. x \<noteq> 0 \<and> x \<in> V}"
    3.35    fixes fn_norm ("\<parallel>_\<parallel>\<hyphen>_" [0, 1000] 999)
    3.36    defines "\<parallel>f\<parallel>\<hyphen>V \<equiv> \<Squnion>(B V f)"
    3.37 @@ -87,10 +89,10 @@
    3.38  *}
    3.39  
    3.40  lemma (in normed_vectorspace_with_fn_norm) fn_norm_works:
    3.41 -  assumes "continuous V norm f"
    3.42 +  assumes "continuous V f norm"
    3.43    shows "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
    3.44  proof -
    3.45 -  interpret continuous V norm f by fact
    3.46 +  interpret continuous V f norm by fact
    3.47    txt {* The existence of the supremum is shown using the
    3.48      completeness of the reals. Completeness means, that every
    3.49      non-empty bounded set of reals has a supremum. *}
    3.50 @@ -154,39 +156,39 @@
    3.51  qed
    3.52  
    3.53  lemma (in normed_vectorspace_with_fn_norm) fn_norm_ub [iff?]:
    3.54 -  assumes "continuous V norm f"
    3.55 +  assumes "continuous V f norm"
    3.56    assumes b: "b \<in> B V f"
    3.57    shows "b \<le> \<parallel>f\<parallel>\<hyphen>V"
    3.58  proof -
    3.59 -  interpret continuous V norm f by fact
    3.60 +  interpret continuous V f norm by fact
    3.61    have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
    3.62 -    using `continuous V norm f` by (rule fn_norm_works)
    3.63 +    using `continuous V f norm` by (rule fn_norm_works)
    3.64    from this and b show ?thesis ..
    3.65  qed
    3.66  
    3.67  lemma (in normed_vectorspace_with_fn_norm) fn_norm_leastB:
    3.68 -  assumes "continuous V norm f"
    3.69 +  assumes "continuous V f norm"
    3.70    assumes b: "\<And>b. b \<in> B V f \<Longrightarrow> b \<le> y"
    3.71    shows "\<parallel>f\<parallel>\<hyphen>V \<le> y"
    3.72  proof -
    3.73 -  interpret continuous V norm f by fact
    3.74 +  interpret continuous V f norm by fact
    3.75    have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
    3.76 -    using `continuous V norm f` by (rule fn_norm_works)
    3.77 +    using `continuous V f norm` by (rule fn_norm_works)
    3.78    from this and b show ?thesis ..
    3.79  qed
    3.80  
    3.81  text {* The norm of a continuous function is always @{text "\<ge> 0"}. *}
    3.82  
    3.83  lemma (in normed_vectorspace_with_fn_norm) fn_norm_ge_zero [iff]:
    3.84 -  assumes "continuous V norm f"
    3.85 +  assumes "continuous V f norm"
    3.86    shows "0 \<le> \<parallel>f\<parallel>\<hyphen>V"
    3.87  proof -
    3.88 -  interpret continuous V norm f by fact
    3.89 +  interpret continuous V f norm by fact
    3.90    txt {* The function norm is defined as the supremum of @{text B}.
    3.91      So it is @{text "\<ge> 0"} if all elements in @{text B} are @{text "\<ge>
    3.92      0"}, provided the supremum exists and @{text B} is not empty. *}
    3.93    have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
    3.94 -    using `continuous V norm f` by (rule fn_norm_works)
    3.95 +    using `continuous V f norm` by (rule fn_norm_works)
    3.96    moreover have "0 \<in> B V f" ..
    3.97    ultimately show ?thesis ..
    3.98  qed
    3.99 @@ -199,11 +201,11 @@
   3.100  *}
   3.101  
   3.102  lemma (in normed_vectorspace_with_fn_norm) fn_norm_le_cong:
   3.103 -  assumes "continuous V norm f" "linearform V f"
   3.104 +  assumes "continuous V f norm" "linearform V f"
   3.105    assumes x: "x \<in> V"
   3.106    shows "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>"
   3.107  proof -
   3.108 -  interpret continuous V norm f by fact
   3.109 +  interpret continuous V f norm by fact
   3.110    interpret linearform V f by fact
   3.111    show ?thesis
   3.112    proof cases
   3.113 @@ -212,7 +214,7 @@
   3.114      also have "f 0 = 0" by rule unfold_locales
   3.115      also have "\<bar>\<dots>\<bar> = 0" by simp
   3.116      also have a: "0 \<le> \<parallel>f\<parallel>\<hyphen>V"
   3.117 -      using `continuous V norm f` by (rule fn_norm_ge_zero)
   3.118 +      using `continuous V f norm` by (rule fn_norm_ge_zero)
   3.119      from x have "0 \<le> norm x" ..
   3.120      with a have "0 \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" by (simp add: zero_le_mult_iff)
   3.121      finally show "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" .
   3.122 @@ -225,7 +227,7 @@
   3.123        from x show "0 \<le> \<parallel>x\<parallel>" ..
   3.124        from x and neq have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<in> B V f"
   3.125          by (auto simp add: B_def divide_inverse)
   3.126 -      with `continuous V norm f` show "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> \<parallel>f\<parallel>\<hyphen>V"
   3.127 +      with `continuous V f norm` show "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> \<parallel>f\<parallel>\<hyphen>V"
   3.128          by (rule fn_norm_ub)
   3.129      qed
   3.130      finally show ?thesis .
   3.131 @@ -241,11 +243,11 @@
   3.132  *}
   3.133  
   3.134  lemma (in normed_vectorspace_with_fn_norm) fn_norm_least [intro?]:
   3.135 -  assumes "continuous V norm f"
   3.136 +  assumes "continuous V f norm"
   3.137    assumes ineq: "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" and ge: "0 \<le> c"
   3.138    shows "\<parallel>f\<parallel>\<hyphen>V \<le> c"
   3.139  proof -
   3.140 -  interpret continuous V norm f by fact
   3.141 +  interpret continuous V f norm by fact
   3.142    show ?thesis
   3.143    proof (rule fn_norm_leastB [folded B_def fn_norm_def])
   3.144      fix b assume b: "b \<in> B V f"
   3.145 @@ -272,7 +274,7 @@
   3.146        qed
   3.147        finally show ?thesis .
   3.148      qed
   3.149 -  qed (insert `continuous V norm f`, simp_all add: continuous_def)
   3.150 +  qed (insert `continuous V f norm`, simp_all add: continuous_def)
   3.151  qed
   3.152  
   3.153  end
     4.1 --- a/src/HOL/Hahn_Banach/Hahn_Banach.thy	Sun Mar 11 20:18:38 2012 +0100
     4.2 +++ b/src/HOL/Hahn_Banach/Hahn_Banach.thy	Sun Mar 11 22:06:13 2012 +0100
     4.3 @@ -356,9 +356,9 @@
     4.4    fixes fn_norm ("\<parallel>_\<parallel>\<hyphen>_" [0, 1000] 999)
     4.5    defines "\<And>V f. \<parallel>f\<parallel>\<hyphen>V \<equiv> \<Squnion>(B V f)"
     4.6    assumes E_norm: "normed_vectorspace E norm" and FE: "subspace F E"
     4.7 -    and linearform: "linearform F f" and "continuous F norm f"
     4.8 +    and linearform: "linearform F f" and "continuous F f norm"
     4.9    shows "\<exists>g. linearform E g
    4.10 -     \<and> continuous E norm g
    4.11 +     \<and> continuous E g norm
    4.12       \<and> (\<forall>x \<in> F. g x = f x)
    4.13       \<and> \<parallel>g\<parallel>\<hyphen>E = \<parallel>f\<parallel>\<hyphen>F"
    4.14  proof -
    4.15 @@ -367,7 +367,7 @@
    4.16      by (auto simp: B_def fn_norm_def) intro_locales
    4.17    interpret subspace F E by fact
    4.18    interpret linearform F f by fact
    4.19 -  interpret continuous F norm f by fact
    4.20 +  interpret continuous F f norm by fact
    4.21    have E: "vectorspace E" by intro_locales
    4.22    have F: "vectorspace F" by rule intro_locales
    4.23    have F_norm: "normed_vectorspace F norm"
    4.24 @@ -375,7 +375,7 @@
    4.25    have ge_zero: "0 \<le> \<parallel>f\<parallel>\<hyphen>F"
    4.26      by (rule normed_vectorspace_with_fn_norm.fn_norm_ge_zero
    4.27        [OF normed_vectorspace_with_fn_norm.intro,
    4.28 -       OF F_norm `continuous F norm f` , folded B_def fn_norm_def])
    4.29 +       OF F_norm `continuous F f norm` , folded B_def fn_norm_def])
    4.30    txt {* We define a function @{text p} on @{text E} as follows:
    4.31      @{text "p x = \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>"} *}
    4.32    def p \<equiv> "\<lambda>x. \<parallel>f\<parallel>\<hyphen>F * \<parallel>x\<parallel>"
    4.33 @@ -422,7 +422,7 @@
    4.34    have "\<forall>x \<in> F. \<bar>f x\<bar> \<le> p x"
    4.35    proof
    4.36      fix x assume "x \<in> F"
    4.37 -    with `continuous F norm f` and linearform
    4.38 +    with `continuous F f norm` and linearform
    4.39      show "\<bar>f x\<bar> \<le> p x"
    4.40        unfolding p_def by (rule normed_vectorspace_with_fn_norm.fn_norm_le_cong
    4.41          [OF normed_vectorspace_with_fn_norm.intro,
    4.42 @@ -442,7 +442,7 @@
    4.43  
    4.44    txt {* We furthermore have to show that @{text g} is also continuous: *}
    4.45  
    4.46 -  have g_cont: "continuous E norm g" using linearformE
    4.47 +  have g_cont: "continuous E g norm" using linearformE
    4.48    proof
    4.49      fix x assume "x \<in> E"
    4.50      with b show "\<bar>g x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>F * \<parallel>x\<parallel>"
    4.51 @@ -500,7 +500,7 @@
    4.52        show "0 \<le> \<parallel>g\<parallel>\<hyphen>E"
    4.53          using g_cont
    4.54          by (rule fn_norm_ge_zero [of g, folded B_def fn_norm_def])
    4.55 -      show "continuous F norm f" by fact
    4.56 +      show "continuous F f norm" by fact
    4.57      qed
    4.58    qed
    4.59    with linearformE a g_cont show ?thesis by blast
     5.1 --- a/src/HOL/Hahn_Banach/Normed_Space.thy	Sun Mar 11 20:18:38 2012 +0100
     5.2 +++ b/src/HOL/Hahn_Banach/Normed_Space.thy	Sun Mar 11 22:06:13 2012 +0100
     5.3 @@ -16,11 +16,9 @@
     5.4    definite, absolute homogenous and subadditive.
     5.5  *}
     5.6  
     5.7 -locale norm_syntax =
     5.8 +locale seminorm =
     5.9 +  fixes V :: "'a\<Colon>{minus, plus, zero, uminus} set"
    5.10    fixes norm :: "'a \<Rightarrow> real"    ("\<parallel>_\<parallel>")
    5.11 -
    5.12 -locale seminorm = var_V + norm_syntax +
    5.13 -  constrains V :: "'a\<Colon>{minus, plus, zero, uminus} set"
    5.14    assumes ge_zero [iff?]: "x \<in> V \<Longrightarrow> 0 \<le> \<parallel>x\<parallel>"
    5.15      and abs_homogenous [iff?]: "x \<in> V \<Longrightarrow> \<parallel>a \<cdot> x\<parallel> = \<bar>a\<bar> * \<parallel>x\<parallel>"
    5.16      and subadditive [iff?]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> \<parallel>x + y\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>y\<parallel>"
     6.1 --- a/src/HOL/Hahn_Banach/Vector_Space.thy	Sun Mar 11 20:18:38 2012 +0100
     6.2 +++ b/src/HOL/Hahn_Banach/Vector_Space.thy	Sun Mar 11 22:06:13 2012 +0100
     6.3 @@ -38,9 +38,8 @@
     6.4    the neutral element of scalar multiplication.
     6.5  *}
     6.6  
     6.7 -locale var_V = fixes V
     6.8 -
     6.9 -locale vectorspace = var_V +
    6.10 +locale vectorspace =
    6.11 +  fixes V
    6.12    assumes non_empty [iff, intro?]: "V \<noteq> {}"
    6.13      and add_closed [iff]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x + y \<in> V"
    6.14      and mult_closed [iff]: "x \<in> V \<Longrightarrow> a \<cdot> x \<in> V"
     7.1 --- a/src/HOL/Library/Numeral_Type.thy	Sun Mar 11 20:18:38 2012 +0100
     7.2 +++ b/src/HOL/Library/Numeral_Type.thy	Sun Mar 11 22:06:13 2012 +0100
     7.3 @@ -135,8 +135,8 @@
     7.4  
     7.5  end
     7.6  
     7.7 -locale mod_ring = mod_type +
     7.8 -  constrains n :: int
     7.9 +locale mod_ring = mod_type n Rep Abs
    7.10 +  for n :: int
    7.11    and Rep :: "'a::{number_ring} \<Rightarrow> int"
    7.12    and Abs :: "int \<Rightarrow> 'a::{number_ring}"
    7.13  begin
     8.1 --- a/src/HOL/RealVector.thy	Sun Mar 11 20:18:38 2012 +0100
     8.2 +++ b/src/HOL/RealVector.thy	Sun Mar 11 22:06:13 2012 +0100
     8.3 @@ -954,8 +954,7 @@
     8.4  
     8.5  subsection {* Bounded Linear and Bilinear Operators *}
     8.6  
     8.7 -locale bounded_linear = additive +
     8.8 -  constrains f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
     8.9 +locale bounded_linear = additive f for f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" +
    8.10    assumes scaleR: "f (scaleR r x) = scaleR r (f x)"
    8.11    assumes bounded: "\<exists>K. \<forall>x. norm (f x) \<le> norm x * K"
    8.12  begin
     9.1 --- a/src/Pure/General/name_space.ML	Sun Mar 11 20:18:38 2012 +0100
     9.2 +++ b/src/Pure/General/name_space.ML	Sun Mar 11 22:06:13 2012 +0100
     9.3 @@ -14,6 +14,7 @@
     9.4    type T
     9.5    val empty: string -> T
     9.6    val kind_of: T -> string
     9.7 +  val defined_entry: T -> string -> bool
     9.8    val the_entry: T -> string ->
     9.9      {concealed: bool, group: serial option, theory_name: string, pos: Position.T, id: serial}
    9.10    val entry_ord: T -> string * string -> order
    9.11 @@ -117,6 +118,8 @@
    9.12  
    9.13  fun kind_of (Name_Space {kind, ...}) = kind;
    9.14  
    9.15 +fun defined_entry (Name_Space {entries, ...}) = Symtab.defined entries;
    9.16 +
    9.17  fun the_entry (Name_Space {kind, entries, ...}) name =
    9.18    (case Symtab.lookup entries name of
    9.19      NONE => error ("Unknown " ^ kind ^ " " ^ quote name)
    10.1 --- a/src/Pure/Isar/locale.ML	Sun Mar 11 20:18:38 2012 +0100
    10.2 +++ b/src/Pure/Isar/locale.ML	Sun Mar 11 22:06:13 2012 +0100
    10.3 @@ -291,7 +291,7 @@
    10.4  in
    10.5  
    10.6  (* Note that while identifiers always have the external (exported) view, activate_dep
    10.7 -  is presented with the internal view. *)
    10.8 +   is presented with the internal view. *)
    10.9  
   10.10  fun roundup thy activate_dep export (name, morph) (marked, input) =
   10.11    let
   10.12 @@ -488,13 +488,9 @@
   10.13      else
   10.14        (Idents.get context, context)
   10.15        (* add new registrations with inherited mixins *)
   10.16 -      |> roundup thy (add_reg thy export) export (name, morph)
   10.17 -      |> snd
   10.18 +      |> (snd o roundup thy (add_reg thy export) export (name, morph))
   10.19        (* add mixin *)
   10.20 -      |>
   10.21 -        (case mixin of
   10.22 -          NONE => I
   10.23 -        | SOME mixin => amend_registration (name, morph) mixin export)
   10.24 +      |> (case mixin of NONE => I | SOME mixin => amend_registration (name, morph) mixin export)
   10.25        (* activate import hierarchy as far as not already active *)
   10.26        |> activate_facts (SOME export) (name, morph)
   10.27    end;
    11.1 --- a/src/Pure/variable.ML	Sun Mar 11 20:18:38 2012 +0100
    11.2 +++ b/src/Pure/variable.ML	Sun Mar 11 22:06:13 2012 +0100
    11.3 @@ -292,8 +292,8 @@
    11.4  
    11.5  (* specialized name space *)
    11.6  
    11.7 -fun is_fixed ctxt x = can (Name_Space.the_entry (fixes_space ctxt)) x;
    11.8 -fun newly_fixed inner outer x = is_fixed inner x andalso not (is_fixed outer x);
    11.9 +val is_fixed = Name_Space.defined_entry o fixes_space;
   11.10 +fun newly_fixed inner outer = is_fixed inner andf (not o is_fixed outer);
   11.11  
   11.12  val fixed_ord = Name_Space.entry_ord o fixes_space;
   11.13  val intern_fixed = Name_Space.intern o fixes_space;
   11.14 @@ -406,7 +406,7 @@
   11.15  fun export_inst inner outer =
   11.16    let
   11.17      val declared_outer = is_declared outer;
   11.18 -    fun still_fixed x = is_fixed outer x orelse not (is_fixed inner x);
   11.19 +    val still_fixed = not o newly_fixed inner outer;
   11.20  
   11.21      val gen_fixes =
   11.22        Symtab.fold (fn (y, _) => not (is_fixed outer y) ? cons y)