# HG changeset patch
# User ballarin
# Date 1229276751 -3600
# Node ID ce6d35a0bed644fce70241b11ddc7a2df0f063e6
# Parent  712c5281d4a4b5196ddea8c0d07699d683ec716f
Ported HOL and HOL-Library to new locales.

diff -r 712c5281d4a4 -r ce6d35a0bed6 src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Sun Dec 14 18:45:16 2008 +0100
+++ b/src/HOL/Complex.thy	Sun Dec 14 18:45:51 2008 +0100
@@ -345,13 +345,13 @@
 
 subsection {* Completeness of the Complexes *}
 
-interpretation Re: bounded_linear ["Re"]
+interpretation Re!: bounded_linear "Re"
 apply (unfold_locales, simp, simp)
 apply (rule_tac x=1 in exI)
 apply (simp add: complex_norm_def)
 done
 
-interpretation Im: bounded_linear ["Im"]
+interpretation Im!: bounded_linear "Im"
 apply (unfold_locales, simp, simp)
 apply (rule_tac x=1 in exI)
 apply (simp add: complex_norm_def)
@@ -513,7 +513,7 @@
 lemma complex_mod_mult_cnj: "cmod (z * cnj z) = (cmod z)\<twosuperior>"
 by (simp add: norm_mult power2_eq_square)
 
-interpretation cnj: bounded_linear ["cnj"]
+interpretation cnj!: bounded_linear "cnj"
 apply (unfold_locales)
 apply (rule complex_cnj_add)
 apply (rule complex_cnj_scaleR)
diff -r 712c5281d4a4 -r ce6d35a0bed6 src/HOL/FrechetDeriv.thy
--- a/src/HOL/FrechetDeriv.thy	Sun Dec 14 18:45:16 2008 +0100
+++ b/src/HOL/FrechetDeriv.thy	Sun Dec 14 18:45:51 2008 +0100
@@ -65,8 +65,8 @@
   assumes "bounded_linear g"
   shows "bounded_linear (\<lambda>x. f x + g x)"
 proof -
-  interpret f: bounded_linear [f] by fact
-  interpret g: bounded_linear [g] by fact
+  interpret f: bounded_linear f by fact
+  interpret g: bounded_linear g by fact
   show ?thesis apply (unfold_locales)
     apply (simp only: f.add g.add add_ac)
     apply (simp only: f.scaleR g.scaleR scaleR_right_distrib)
@@ -124,7 +124,7 @@
   assumes "bounded_linear f"
   shows "bounded_linear (\<lambda>x. - f x)"
 proof -
-  interpret f: bounded_linear [f] by fact
+  interpret f: bounded_linear f by fact
   show ?thesis apply (unfold_locales)
     apply (simp add: f.add)
     apply (simp add: f.scaleR)
@@ -151,7 +151,7 @@
   assumes f: "FDERIV f x :> F"
   shows "isCont f x"
 proof -
-  from f interpret F: bounded_linear ["F"] by (rule FDERIV_bounded_linear)
+  from f interpret F: bounded_linear "F" by (rule FDERIV_bounded_linear)
   have "(\<lambda>h. norm (f (x + h) - f x - F h) / norm h) -- 0 --> 0"
     by (rule FDERIV_D [OF f])
   hence "(\<lambda>h. norm (f (x + h) - f x - F h) / norm h * norm h) -- 0 --> 0"
@@ -180,8 +180,8 @@
   assumes "bounded_linear g"
   shows "bounded_linear (\<lambda>x. f (g x))"
 proof -
-  interpret f: bounded_linear [f] by fact
-  interpret g: bounded_linear [g] by fact
+  interpret f: bounded_linear f by fact
+  interpret g: bounded_linear g by fact
   show ?thesis proof (unfold_locales)
     fix x y show "f (g (x + y)) = f (g x) + f (g y)"
       by (simp only: f.add g.add)
@@ -223,8 +223,8 @@
   let ?k = "\<lambda>h. f (x + h) - f x"
   let ?Nf = "\<lambda>h. norm (?Rf h) / norm h"
   let ?Ng = "\<lambda>h. norm (?Rg (?k h)) / norm (?k h)"
-  from f interpret F: bounded_linear ["F"] by (rule FDERIV_bounded_linear)
-  from g interpret G: bounded_linear ["G"] by (rule FDERIV_bounded_linear)
+  from f interpret F!: bounded_linear "F" by (rule FDERIV_bounded_linear)
+  from g interpret G!: bounded_linear "G" by (rule FDERIV_bounded_linear)
   from F.bounded obtain kF where kF: "\<And>x. norm (F x) \<le> norm x * kF" by fast
   from G.bounded obtain kG where kG: "\<And>x. norm (G x) \<le> norm x * kG" by fast
 
@@ -375,9 +375,9 @@
     by (simp only: FDERIV_lemma)
 qed
 
-lemmas FDERIV_mult = bounded_bilinear_locale.mult.prod.FDERIV
+lemmas FDERIV_mult = mult.FDERIV
 
-lemmas FDERIV_scaleR = bounded_bilinear_locale.scaleR.prod.FDERIV
+lemmas FDERIV_scaleR = scaleR.FDERIV
 
 
 subsection {* Powers *}
@@ -409,10 +409,10 @@
 by (simp add: right_diff_distrib left_diff_distrib mult_assoc)
 
 lemmas bounded_linear_mult_const =
-  bounded_bilinear_locale.mult.prod.bounded_linear_left [THEN bounded_linear_compose]
+  mult.bounded_linear_left [THEN bounded_linear_compose]
 
 lemmas bounded_linear_const_mult =
-  bounded_bilinear_locale.mult.prod.bounded_linear_right [THEN bounded_linear_compose]
+  mult.bounded_linear_right [THEN bounded_linear_compose]
 
 lemma FDERIV_inverse:
   fixes x :: "'a::real_normed_div_algebra"
@@ -492,7 +492,7 @@
   fixes x :: "'a::real_normed_field" shows
   "FDERIV f x :> (\<lambda>h. h * D) = (\<lambda>h. (f (x + h) - f x) / h) -- 0 --> D"
  apply (unfold fderiv_def)
- apply (simp add: bounded_bilinear_locale.mult.prod.bounded_linear_left)
+ apply (simp add: mult.bounded_linear_left)
  apply (simp cong: LIM_cong add: nonzero_norm_divide [symmetric])
  apply (subst diff_divide_distrib)
  apply (subst times_divide_eq_left [symmetric])
diff -r 712c5281d4a4 -r ce6d35a0bed6 src/HOL/Groebner_Basis.thy
--- a/src/HOL/Groebner_Basis.thy	Sun Dec 14 18:45:16 2008 +0100
+++ b/src/HOL/Groebner_Basis.thy	Sun Dec 14 18:45:51 2008 +0100
@@ -163,7 +163,7 @@
 
 end
 
-interpretation class_semiring: gb_semiring
+interpretation class_semiring!: gb_semiring
     "op +" "op *" "op ^" "0::'a::{comm_semiring_1, recpower}" "1"
   proof qed (auto simp add: ring_simps power_Suc)
 
@@ -242,7 +242,7 @@
 end
 
 
-interpretation class_ring: gb_ring "op +" "op *" "op ^"
+interpretation class_ring!: gb_ring "op +" "op *" "op ^"
     "0::'a::{comm_semiring_1,recpower,number_ring}" 1 "op -" "uminus"
   proof qed simp_all
 
@@ -343,7 +343,7 @@
   thus "b = 0" by blast
 qed
 
-interpretation class_ringb: ringb
+interpretation class_ringb!: ringb
   "op +" "op *" "op ^" "0::'a::{idom,recpower,number_ring}" "1" "op -" "uminus"
 proof(unfold_locales, simp add: ring_simps power_Suc, auto)
   fix w x y z ::"'a::{idom,recpower,number_ring}"
@@ -359,7 +359,7 @@
 
 declaration {* normalizer_funs @{thm class_ringb.ringb_axioms'} *}
 
-interpretation natgb: semiringb
+interpretation natgb!: semiringb
   "op +" "op *" "op ^" "0::nat" "1"
 proof (unfold_locales, simp add: ring_simps power_Suc)
   fix w x y z ::"nat"
@@ -464,7 +464,7 @@
 
 subsection{* Groebner Bases for fields *}
 
-interpretation class_fieldgb:
+interpretation class_fieldgb!:
   fieldgb "op +" "op *" "op ^" "0::'a::{field,recpower,number_ring}" "1" "op -" "uminus" "op /" "inverse" apply (unfold_locales) by (simp_all add: divide_inverse)
 
 lemma divide_Numeral1: "(x::'a::{field,number_ring}) / Numeral1 = x" by simp
diff -r 712c5281d4a4 -r ce6d35a0bed6 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Sun Dec 14 18:45:16 2008 +0100
+++ b/src/HOL/Library/Multiset.thy	Sun Dec 14 18:45:51 2008 +0100
@@ -1080,15 +1080,15 @@
 apply simp
 done
 
-interpretation mset_order: order ["op \<le>#" "op <#"]
+class_interpretation mset_order: order ["op \<le>#" "op <#"]
 proof qed (auto intro: order.intro mset_le_refl mset_le_antisym
   mset_le_trans simp: mset_less_def)
 
-interpretation mset_order_cancel_semigroup:
+class_interpretation mset_order_cancel_semigroup:
   pordered_cancel_ab_semigroup_add ["op +" "op \<le>#" "op <#"]
 proof qed (erule mset_le_mono_add [OF mset_le_refl])
 
-interpretation mset_order_semigroup_cancel:
+class_interpretation mset_order_semigroup_cancel:
   pordered_ab_semigroup_add_imp_le ["op +" "op \<le>#" "op <#"]
 proof qed simp
 
@@ -1404,7 +1404,7 @@
   assumes "left_commutative g"
   shows "(\<And>x y. h (g x y) = f x (h y)) \<Longrightarrow> h (fold_mset g w A) = fold_mset f (h w) A" (is "PROP ?P")
 proof -
-  interpret left_commutative [g] by fact
+  interpret left_commutative g by fact
   show "PROP ?P" by (induct A) auto
 qed
 
@@ -1436,7 +1436,7 @@
 definition [code del]:
  "image_mset f = fold_mset (op + o single o f) {#}"
 
-interpretation image_left_comm: left_commutative ["op + o single o f"]
+interpretation image_left_comm!: left_commutative "op + o single o f"
   proof qed (simp add:union_ac)
 
 lemma image_mset_empty [simp]: "image_mset f {#} = {#}"
diff -r 712c5281d4a4 -r ce6d35a0bed6 src/HOL/Library/SetsAndFunctions.thy
--- a/src/HOL/Library/SetsAndFunctions.thy	Sun Dec 14 18:45:16 2008 +0100
+++ b/src/HOL/Library/SetsAndFunctions.thy	Sun Dec 14 18:45:51 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Library/SetsAndFunctions.thy
-    ID:         $Id$
     Author:     Jeremy Avigad and Kevin Donnelly
 *)
 
@@ -108,26 +107,26 @@
   apply simp
   done
 
-interpretation set_semigroup_add: semigroup_add ["op \<oplus> :: ('a::semigroup_add) set => 'a set => 'a set"]
+class_interpretation set_semigroup_add: semigroup_add ["op \<oplus> :: ('a::semigroup_add) set => 'a set => 'a set"]
   apply default
   apply (unfold set_plus_def)
   apply (force simp add: add_assoc)
   done
 
-interpretation set_semigroup_mult: semigroup_mult ["op \<otimes> :: ('a::semigroup_mult) set => 'a set => 'a set"]
+class_interpretation set_semigroup_mult: semigroup_mult ["op \<otimes> :: ('a::semigroup_mult) set => 'a set => 'a set"]
   apply default
   apply (unfold set_times_def)
   apply (force simp add: mult_assoc)
   done
 
-interpretation set_comm_monoid_add: comm_monoid_add ["{0}" "op \<oplus> :: ('a::comm_monoid_add) set => 'a set => 'a set"]
+class_interpretation set_comm_monoid_add: comm_monoid_add ["{0}" "op \<oplus> :: ('a::comm_monoid_add) set => 'a set => 'a set"]
   apply default
    apply (unfold set_plus_def)
    apply (force simp add: add_ac)
   apply force
   done
 
-interpretation set_comm_monoid_mult: comm_monoid_mult ["{1}" "op \<otimes> :: ('a::comm_monoid_mult) set => 'a set => 'a set"]
+class_interpretation set_comm_monoid_mult: comm_monoid_mult ["{1}" "op \<otimes> :: ('a::comm_monoid_mult) set => 'a set => 'a set"]
   apply default
    apply (unfold set_times_def)
    apply (force simp add: mult_ac)
diff -r 712c5281d4a4 -r ce6d35a0bed6 src/HOL/ROOT.ML
--- a/src/HOL/ROOT.ML	Sun Dec 14 18:45:16 2008 +0100
+++ b/src/HOL/ROOT.ML	Sun Dec 14 18:45:51 2008 +0100
@@ -3,6 +3,7 @@
 Classical Higher-order Logic -- batteries included.
 *)
 
+set new_locales;
 use_thy "Complex_Main";
 
 val HOL_proofs = ! Proofterm.proofs;
diff -r 712c5281d4a4 -r ce6d35a0bed6 src/HOL/Real/RealVector.thy
--- a/src/HOL/Real/RealVector.thy	Sun Dec 14 18:45:16 2008 +0100
+++ b/src/HOL/Real/RealVector.thy	Sun Dec 14 18:45:51 2008 +0100
@@ -151,7 +151,7 @@
   and scaleR_scaleR [simp]: "scaleR a (scaleR b x) = scaleR (a * b) x"
   and scaleR_one [simp]: "scaleR 1 x = x"
 
-interpretation real_vector:
+interpretation real_vector!:
   vector_space "scaleR :: real \<Rightarrow> 'a \<Rightarrow> 'a::real_vector"
 apply unfold_locales
 apply (rule scaleR_right_distrib)
@@ -195,10 +195,10 @@
 apply (rule mult_left_commute)
 done
 
-interpretation scaleR_left: additive "(\<lambda>a. scaleR a x::'a::real_vector)"
+interpretation scaleR_left!: additive "(\<lambda>a. scaleR a x::'a::real_vector)"
 proof qed (rule scaleR_left_distrib)
 
-interpretation scaleR_right: additive "(\<lambda>x. scaleR a x::'a::real_vector)"
+interpretation scaleR_right!: additive "(\<lambda>x. scaleR a x::'a::real_vector)"
 proof qed (rule scaleR_right_distrib)
 
 lemma nonzero_inverse_scaleR_distrib:
@@ -796,7 +796,7 @@
 
 end
 
-interpretation mult:
+interpretation mult!:
   bounded_bilinear "op * :: 'a \<Rightarrow> 'a \<Rightarrow> 'a::real_normed_algebra"
 apply (rule bounded_bilinear.intro)
 apply (rule left_distrib)
@@ -807,19 +807,19 @@
 apply (simp add: norm_mult_ineq)
 done
 
-interpretation mult_left:
+interpretation mult_left!:
   bounded_linear "(\<lambda>x::'a::real_normed_algebra. x * y)"
 by (rule mult.bounded_linear_left)
 
-interpretation mult_right:
+interpretation mult_right!:
   bounded_linear "(\<lambda>y::'a::real_normed_algebra. x * y)"
 by (rule mult.bounded_linear_right)
 
-interpretation divide:
+interpretation divide!:
   bounded_linear "(\<lambda>x::'a::real_normed_field. x / y)"
 unfolding divide_inverse by (rule mult.bounded_linear_left)
 
-interpretation scaleR: bounded_bilinear "scaleR"
+interpretation scaleR!: bounded_bilinear "scaleR"
 apply (rule bounded_bilinear.intro)
 apply (rule scaleR_left_distrib)
 apply (rule scaleR_right_distrib)
@@ -829,13 +829,13 @@
 apply (simp add: norm_scaleR)
 done
 
-interpretation scaleR_left: bounded_linear "\<lambda>r. scaleR r x"
+interpretation scaleR_left!: bounded_linear "\<lambda>r. scaleR r x"
 by (rule scaleR.bounded_linear_left)
 
-interpretation scaleR_right: bounded_linear "\<lambda>x. scaleR r x"
+interpretation scaleR_right!: bounded_linear "\<lambda>x. scaleR r x"
 by (rule scaleR.bounded_linear_right)
 
-interpretation of_real: bounded_linear "\<lambda>r. of_real r"
+interpretation of_real!: bounded_linear "\<lambda>r. of_real r"
 unfolding of_real_def by (rule scaleR.bounded_linear_left)
 
 end
diff -r 712c5281d4a4 -r ce6d35a0bed6 src/HOL/ex/LocaleTest2.thy
--- a/src/HOL/ex/LocaleTest2.thy	Sun Dec 14 18:45:16 2008 +0100
+++ b/src/HOL/ex/LocaleTest2.thy	Sun Dec 14 18:45:51 2008 +0100
@@ -468,7 +468,7 @@
 
 subsubsection {* Total order @{text "<="} on @{typ int} *}
 
-interpretation int: dpo "op <= :: [int, int] => bool"
+interpretation int!: dpo "op <= :: [int, int] => bool"
   where "(dpo.less (op <=) (x::int) y) = (x < y)"
   txt {* We give interpretation for less, but not @{text is_inf} and @{text is_sub}. *}
 proof -
@@ -487,7 +487,7 @@
 lemma "(op < :: [int, int] => bool) = op <"
   apply (rule int.abs_test) done
 
-interpretation int: dlat "op <= :: [int, int] => bool"
+interpretation int!: dlat "op <= :: [int, int] => bool"
   where meet_eq: "dlat.meet (op <=) (x::int) y = min x y"
     and join_eq: "dlat.join (op <=) (x::int) y = max x y"
 proof -
@@ -511,7 +511,7 @@
     by auto
 qed
 
-interpretation int: dlo "op <= :: [int, int] => bool"
+interpretation int!: dlo "op <= :: [int, int] => bool"
   proof qed arith
 
 text {* Interpreted theorems from the locales, involving defined terms. *}
@@ -524,7 +524,7 @@
 
 subsubsection {* Total order @{text "<="} on @{typ nat} *}
 
-interpretation nat: dpo "op <= :: [nat, nat] => bool"
+interpretation nat!: dpo "op <= :: [nat, nat] => bool"
   where "dpo.less (op <=) (x::nat) y = (x < y)"
   txt {* We give interpretation for less, but not @{text is_inf} and @{text is_sub}. *}
 proof -
@@ -538,7 +538,7 @@
     done
 qed
 
-interpretation nat: dlat "op <= :: [nat, nat] => bool"
+interpretation nat!: dlat "op <= :: [nat, nat] => bool"
   where "dlat.meet (op <=) (x::nat) y = min x y"
     and "dlat.join (op <=) (x::nat) y = max x y"
 proof -
@@ -562,7 +562,7 @@
     by auto
 qed
 
-interpretation nat: dlo "op <= :: [nat, nat] => bool"
+interpretation nat!: dlo "op <= :: [nat, nat] => bool"
   proof qed arith
 
 text {* Interpreted theorems from the locales, involving defined terms. *}
@@ -575,7 +575,7 @@
 
 subsubsection {* Lattice @{text "dvd"} on @{typ nat} *}
 
-interpretation nat_dvd: dpo "op dvd :: [nat, nat] => bool"
+interpretation nat_dvd!: dpo "op dvd :: [nat, nat] => bool"
   where "dpo.less (op dvd) (x::nat) y = (x dvd y & x ~= y)"
   txt {* We give interpretation for less, but not @{text is_inf} and @{text is_sub}. *}
 proof -
@@ -589,7 +589,7 @@
     done
 qed
 
-interpretation nat_dvd: dlat "op dvd :: [nat, nat] => bool"
+interpretation nat_dvd!: dlat "op dvd :: [nat, nat] => bool"
   where "dlat.meet (op dvd) (x::nat) y = gcd x y"
     and "dlat.join (op dvd) (x::nat) y = lcm x y"
 proof -
@@ -837,7 +837,7 @@
 
 subsubsection {* Interpretation of Functions *}
 
-interpretation Dfun: Dmonoid "op o" "id :: 'a => 'a"
+interpretation Dfun!: Dmonoid "op o" "id :: 'a => 'a"
   where "Dmonoid.unit (op o) id f = bij (f::'a => 'a)"
 (*    and "Dmonoid.inv (op o) id" = "inv :: ('a => 'a) => ('a => 'a)" *)
 proof -
@@ -887,7 +887,7 @@
   "(f :: unit => unit) = id"
   by rule simp
 
-interpretation Dfun: Dgrp "op o" "id :: unit => unit"
+interpretation Dfun!: Dgrp "op o" "id :: unit => unit"
   where "Dmonoid.inv (op o) id f = inv (f :: unit => unit)"
 proof -
   have "Dmonoid op o (id :: 'a => 'a)" ..